[ltree] More supporting theorems for rose trees

[binghe]

Hi,

This PR adds some useful definitions and theorems for the "rose tree" inside ltreeTheory.

In ltreeTheory, there's a "rose tree" [*] inductively defined by a regular use of the datatype package:

Datatype:
  rose_tree = Rose 'a (rose_tree list)
End

and the constant from_rose is defined to map any rose tree into a corresponding ltree (this is always possible):

   [from_rose_def]  Theorem (ltreeTheory)      
      ⊢ ∀ts a.
          from_rose (Rose a ts) =
          Branch a (fromList (MAP (λa'. from_rose a') ts))

On the other hand, for any ltree which is finite (ltree_finite), there exists a corresponding rose tree:

   [ltree_finite_from_rose]  Theorem
      ⊢ ltree_finite t ⇔ ∃r. from_rose r = t

This is basically all we had before for the rose trees.

In this PR, first, I proved that the mapping from_rose is injective (by induction on one of the two rose trees):

   [from_rose_11]  Theorem      
      ⊢ ∀r1 r2. from_rose r1 = from_rose r2 ⇔ r1 = r2

Then, using the injective result and the above ltree_finite_from_rose theorem, I defined the constant to_rose for mapping ltree to rose tree (this is only possible when the ltree is finite) and proved the from/to relationships:

   [to_rose_def]  Definition      
      ⊢ ∀t. ltree_finite t ⇒ from_rose (to_rose t) = t

   [to_rose_thm]  Theorem      
      ⊢ ∀r. to_rose (from_rose r) = r

Then, I added the following accessor contants for easy accessing rose tree components (ltree has them too):

   [rose_children_def]  Definition      
      ⊢ ∀a ts. rose_children (Rose a ts) = ts
   
   [rose_node_def]  Definition      
      ⊢ ∀a ts. rose_node (Rose a ts) = a

And I prove what happens if these accessors were put on a rose tree converted from a (finite) ltree:

   [rose_node_to_rose]  Theorem      
      ⊢ ∀t. ltree_finite t ⇒ rose_node (to_rose t) = ltree_node t

   [rose_children_to_rose]  Theorem      
      ⊢ ∀t. ltree_finite t ⇒
            rose_children (to_rose t) =
            MAP to_rose (THE (toList (ltree_children t)))
   
   [rose_children_to_rose']  Theorem      
      ⊢ ∀t. ltree_finite t ⇒
            rose_children (to_rose t) =
            THE (toList (LMAP to_rose (ltree_children t)))

Finally, I added the following rose_reduce function as a general recursive function on rose trees:

   [rose_reduce_def]  Theorem      
      ⊢ ∀ts f a.
          rose_reduce f (Rose a ts) = f a (MAP (λa'. rose_reduce f a') ts)

There's no other supporting theorems for this rose_reduce, but I'm using it to re-construct lambda-terms from their Boehm trees (when they are finite and are mapped to rose trees).

--Chun

[*] But, according to Wikipedia [1], "rose tree" a term for the value of a tree data structure with a variable and unbounded number of branches per node. Our "rose tree" here is only finite branching.
[1] https://en.wikipedia.org/wiki/Rose_tree

[mn200]

Thanks! I suspect the wikipedia page doesn't really allow for unbounded up to infinitely wide (certainly all of its examples involve finite branching).