Add ltree_every and ltree_finite_branching

[binghe]

Currently in ltreeTheory (co-inductive lazy tree, which allows for both infinite depth
and infinite breadth), there's no predicate asserting the tree is "finite branching" (either finite or infinite depth). The existing ltree_finite states for both finite depth and breadth, i.e. the number of subtrees is finite.

It seems that, a every predicate for each subtree (thus both the node data and children are accessible) of a ltree can be simply defined like this by CoInductive:

CoInductive ltree_every :
    P a ts /\ every (ltree_every P) ts ==> (ltree_every P (Branch a ts))
End

And then ltree_finite_branching simply says that each subtree has finite number of directly children:

   [ltree_finite_branching_def]  Definition
      
      ⊢ ltree_finite_branching = ltree_every (λa ts. LFINITE ts)

To ease the use of ltree_finite_branching, just like it's co-inductively defined by CoInductive, the following 3 theorems (rules, cases, and coind) are manually proved (while the 3 for ltree_every are auto-generated):

   [ltree_finite_branching_cases]  Theorem      
      ⊢ ∀t. ltree_finite_branching t ⇔
            ∃a ts.
              t = Branch a (fromList ts) ∧ EVERY ltree_finite_branching ts
   
   [ltree_finite_branching_coind]  Theorem      
      ⊢ ∀P. (∀t. P t ⇒ ∃a ts. t = Branch a (fromList ts) ∧ EVERY P ts) ⇒
            ∀t. P t ⇒ ltree_finite_branching t
   
   [ltree_finite_branching_rules]  Theorem      
      ⊢ ∀a ts.
          EVERY ltree_finite_branching ts ⇒
          ltree_finite_branching (Branch a (fromList ts))

Please review the correctness (of the definitions).

[mn200]

These definitions look nice, but it would be nice to have iff (and probably [simp]) theorems for both new constants as well if possible. I guess something like

ltree_every P (Branch a ts) <=> P a /\ every (ltree_every P ts)

for ltree_every and something similar for finitely branching.

[binghe]

Thanks. I have now added:

   [ltree_every_rewrite]  Theorem      
      ⊢ ltree_every P (Branch a ts) ⇔ P a ts ∧ every (ltree_every P) ts

   [ltree_finite_branching_rewrite]  Theorem      
      ⊢ ltree_finite_branching (Branch a ts) ⇔
        LFINITE ts ∧ every ltree_finite_branching ts

[binghe]

By the way, is there a shorter way to write GEN_REWRITE_TAC (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites []? I have used tactics like this many times when I needed to rewrite only the L part of a term like L = R (replacing RATOR_CONV with RAND_CONV I can do the R-part)

[mn200]

The SimpLHS and SimpRHS (documented in the DESCRIPTION manual) special forms can help with this sort of thing, when using the simplifier.

[binghe]

The SimpLHS and SimpRHS (documented in the DESCRIPTION manual) special forms can help with this sort of thing, when using the simplifier.

Thanks. I have simplified the two proofs involving GEN_REWRITE_TAC (and it turns out that even SimpLHS, etc. is not needed...) I think you can squash all commits in this PR.

[mn200]

Thanks!