Structure ltreeTheory

signature ltreeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val finite_branching_def : thm
    val ltree_TY_DEF : thm
    val ltree_children_def_primitive : thm
    val ltree_map_def : thm
    val ltree_node_def_primitive : thm
    val ltree_paths_def : thm
    val ltree_rel_def : thm
    val ltree_set_def : thm
    val rose_tree_TY_DEF : thm
    val rose_tree_case_def : thm
    val rose_tree_size_def : thm
    val subtrees_def : thm
  
  (*  Theorems  *)
    val Branch_11 : thm
    val IN_ltree_lookup : thm
    val NIL_IN_ltree_paths : thm
    val datatype_ltree : thm
    val datatype_rose_tree : thm
    val finite_branching_cases : thm
    val finite_branching_cases' : thm
    val finite_branching_coind : thm
    val finite_branching_coind' : thm
    val finite_branching_rewrite : thm
    val finite_branching_rules : thm
    val finite_branching_rules' : thm
    val from_rose_def : thm
    val from_rose_ind : thm
    val gen_ltree : thm
    val gen_ltree_LNIL : thm
    val ltree_CASE : thm
    val ltree_CASE_cong : thm
    val ltree_CASE_elim : thm
    val ltree_CASE_eq : thm
    val ltree_bisimulation : thm
    val ltree_cases : thm
    val ltree_children_def : thm
    val ltree_children_ind : thm
    val ltree_el : thm
    val ltree_el_def : thm
    val ltree_el_eqv : thm
    val ltree_el_valid : thm
    val ltree_el_valid_inclusive : thm
    val ltree_every_cases : thm
    val ltree_every_coind : thm
    val ltree_every_rewrite : thm
    val ltree_every_rules : thm
    val ltree_finite : thm
    val ltree_finite_cases : thm
    val ltree_finite_from_rose : thm
    val ltree_finite_imp_finite_branching : thm
    val ltree_finite_ind : thm
    val ltree_finite_rules : thm
    val ltree_finite_strongind : thm
    val ltree_lookup : thm
    val ltree_lookup_def : thm
    val ltree_lookup_valid : thm
    val ltree_lookup_valid_inclusive : thm
    val ltree_map : thm
    val ltree_map_id : thm
    val ltree_map_map : thm
    val ltree_node_children_reduce : thm
    val ltree_node_def : thm
    val ltree_node_ind : thm
    val ltree_paths_alt : thm
    val ltree_paths_inclusive : thm
    val ltree_rel : thm
    val ltree_rel_O : thm
    val ltree_rel_eq : thm
    val ltree_set : thm
    val ltree_set_map : thm
    val ltree_unfold : thm
    val rose_tree_11 : thm
    val rose_tree_Axiom : thm
    val rose_tree_case_cong : thm
    val rose_tree_case_eq : thm
    val rose_tree_induction : thm
    val rose_tree_nchotomy : thm
    val rose_tree_size_eq : thm
    val subtrees : thm
  
  val ltree_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [alist] Parent theory of "ltree"
   
   [llist] Parent theory of "ltree"
   
   [res_quan] Parent theory of "ltree"
   
   [finite_branching_def]  Definition
      
      ⊢ finite_branching = ltree_every (λa ts. LFINITE ts)
   
   [ltree_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION ltree_rep_ok rep
   
   [ltree_children_def_primitive]  Definition
      
      ⊢ ltree_children =
        WFREC (@R. WF R)
          (λltree_children a'. case a' of Branch a ts => I ts)
   
   [ltree_map_def]  Definition
      
      ⊢ ∀f. ltree_map f =
            ltree_unfold (λt. case t of Branch a ts => (f a,ts))
   
   [ltree_node_def_primitive]  Definition
      
      ⊢ ltree_node =
        WFREC (@R. WF R) (λltree_node a'. case a' of Branch a ts => I a)
   
   [ltree_paths_def]  Definition
      
      ⊢ ∀t. ltree_paths t = {p | ltree_lookup t p ≠ NONE}
   
   [ltree_rel_def]  Definition
      
      ⊢ ∀R x y.
          ltree_rel R x y ⇔
          ∀path.
            OPTREL (λx y. R (FST x) (FST y) ∧ SND x = SND y)
              (ltree_el x path) (ltree_el y path)
   
   [ltree_set_def]  Definition
      
      ⊢ ∀t. ltree_set t = {a | ∃ts. Branch a ts ∈ subtrees t}
   
   [rose_tree_TY_DEF]  Definition
      
      ⊢ ∃rep.
          TYPE_DEFINITION
            (λa0'.
                 ∀ $var$('rose_tree') $var$('@temp@ind_typeltree0list').
                   (∀a0'.
                      (∃a0 a1.
                         a0' =
                         (λa0 a1.
                              ind_type$CONSTR 0 a0
                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
                           a0 a1 ∧ $var$('@temp@ind_typeltree0list') a1) ⇒
                      $var$('rose_tree') a0') ∧
                   (∀a1'.
                      a1' =
                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ∨
                      (∃a0 a1.
                         a1' =
                         (λa0 a1.
                              ind_type$CONSTR (SUC (SUC 0)) ARB
                                (ind_type$FCONS a0
                                   (ind_type$FCONS a1 (λn. ind_type$BOTTOM))))
                           a0 a1 ∧ $var$('rose_tree') a0 ∧
                         $var$('@temp@ind_typeltree0list') a1) ⇒
                      $var$('@temp@ind_typeltree0list') a1') ⇒
                   $var$('rose_tree') a0') rep
   
   [rose_tree_case_def]  Definition
      
      ⊢ ∀a0 a1 f. rose_tree_CASE (Rose a0 a1) f = f a0 a1
   
   [rose_tree_size_def]  Definition
      
      ⊢ (∀f a0 a1.
           rose_tree_size f (Rose a0 a1) =
           1 + (f a0 + rose_tree1_size f a1)) ∧
        (∀f. rose_tree1_size f [] = 0) ∧
        ∀f a0 a1.
          rose_tree1_size f (a0::a1) =
          1 + (rose_tree_size f a0 + rose_tree1_size f a1)
   
   [subtrees_def]  Definition
      
      ⊢ ∀t. subtrees t = {u | ∃path. ltree_lookup t path = SOME u}
   
   [Branch_11]  Theorem
      
      ⊢ ∀a1 a2 ts1 ts2. Branch a1 ts1 = Branch a2 ts2 ⇔ a1 = a2 ∧ ts1 = ts2
   
   [IN_ltree_lookup]  Theorem
      
      ⊢ ∀p t. p ∈ ltree_paths t ⇔ ltree_lookup t p ≠ NONE
   
   [NIL_IN_ltree_paths]  Theorem
      
      ⊢ [] ∈ ltree_paths t
   
   [datatype_ltree]  Theorem
      
      ⊢ DATATYPE (ltree Branch)
   
   [datatype_rose_tree]  Theorem
      
      ⊢ DATATYPE (rose_tree Rose)
   
   [finite_branching_cases]  Theorem
      
      ⊢ ∀t. finite_branching t ⇔
            ∃a ts. t = Branch a (fromList ts) ∧ EVERY finite_branching ts
   
   [finite_branching_cases']  Theorem
      
      ⊢ ∀t. finite_branching t ⇔
            ∃a ts. t = Branch a ts ∧ LFINITE ts ∧ every finite_branching ts
   
   [finite_branching_coind]  Theorem
      
      ⊢ ∀P. (∀t. P t ⇒ ∃a ts. t = Branch a (fromList ts) ∧ EVERY P ts) ⇒
            ∀t. P t ⇒ finite_branching t
   
   [finite_branching_coind']  Theorem
      
      ⊢ ∀P. (∀t. P t ⇒ ∃a ts. t = Branch a ts ∧ LFINITE ts ∧ every P ts) ⇒
            ∀t. P t ⇒ finite_branching t
   
   [finite_branching_rewrite]  Theorem
      
      ⊢ finite_branching (Branch a ts) ⇔
        LFINITE ts ∧ every finite_branching ts
   
   [finite_branching_rules]  Theorem
      
      ⊢ ∀a ts.
          EVERY finite_branching ts ⇒
          finite_branching (Branch a (fromList ts))
   
   [finite_branching_rules']  Theorem
      
      ⊢ ∀a ts.
          LFINITE ts ∧ every finite_branching ts ⇒
          finite_branching (Branch a ts)
   
   [from_rose_def]  Theorem
      
      ⊢ ∀ts a.
          from_rose (Rose a ts) =
          Branch a (fromList (MAP (λa'. from_rose a') ts))
   
   [from_rose_ind]  Theorem
      
      ⊢ ∀P. (∀a ts. (∀a'. MEM a' ts ⇒ P a') ⇒ P (Rose a ts)) ⇒ ∀v. P v
   
   [gen_ltree]  Theorem
      
      ⊢ gen_ltree f =
        (let
           (a,len) = f []
         in
           Branch a (LGENLIST (λn. gen_ltree (λpath. f (n::path))) len))
   
   [gen_ltree_LNIL]  Theorem
      
      ⊢ gen_ltree f = Branch a [||] ⇔ f [] = (a,SOME 0)
   
   [ltree_CASE]  Theorem
      
      ⊢ ltree_CASE (Branch a ts) f = f a ts
   
   [ltree_CASE_cong]  Theorem
      
      ⊢ ∀M M' f f'.
          M = M' ∧ (∀a ts. M' = Branch a ts ⇒ f a ts = f' a ts) ⇒
          ltree_CASE M f = ltree_CASE M' f'
   
   [ltree_CASE_elim]  Theorem
      
      ⊢ ∀f'. f' (ltree_CASE t f) ⇔ ∃a ts. t = Branch a ts ∧ f' (f a ts)
   
   [ltree_CASE_eq]  Theorem
      
      ⊢ ltree_CASE t f = v ⇔ ∃a ts. t = Branch a ts ∧ f a ts = v
   
   [ltree_bisimulation]  Theorem
      
      ⊢ ∀t1 t2.
          t1 = t2 ⇔
          ∃R. R t1 t2 ∧
              ∀a ts a' ts'.
                R (Branch a ts) (Branch a' ts') ⇒
                a = a' ∧ llist_rel R ts ts'
   
   [ltree_cases]  Theorem
      
      ⊢ ∀t. ∃a ts. t = Branch a ts
   
   [ltree_children_def]  Theorem
      
      ⊢ ltree_children (Branch a ts) = ts
   
   [ltree_children_ind]  Theorem
      
      ⊢ ∀P. (∀a ts. P (Branch a ts)) ⇒ ∀v. P v
   
   [ltree_el]  Theorem
      
      ⊢ ltree_el t [] = SOME (ltree_node t,LLENGTH (ltree_children t)) ∧
        ltree_el t (n::ns) =
        case LNTH n (ltree_children t) of
          NONE => NONE
        | SOME a => ltree_el a ns
   
   [ltree_el_def]  Theorem
      
      ⊢ ltree_el (Branch a ts) [] = SOME (a,LLENGTH ts) ∧
        ltree_el (Branch a ts) (n::ns) =
        case LNTH n ts of NONE => NONE | SOME t => ltree_el t ns
   
   [ltree_el_eqv]  Theorem
      
      ⊢ ∀t1 t2. t1 = t2 ⇔ ∀path. ltree_el t1 path = ltree_el t2 path
   
   [ltree_el_valid]  Theorem
      
      ⊢ ∀p t. p ∈ ltree_paths t ⇔ ltree_el t p ≠ NONE
   
   [ltree_el_valid_inclusive]  Theorem
      
      ⊢ ∀p t. p ∈ ltree_paths t ⇔ ∀p'. p' ≼ p ⇒ ltree_el t p' ≠ NONE
   
   [ltree_every_cases]  Theorem
      
      ⊢ ∀P a0.
          ltree_every P a0 ⇔
          ∃a ts. a0 = Branch a ts ∧ P a ts ∧ every (ltree_every P) ts
   
   [ltree_every_coind]  Theorem
      
      ⊢ ∀P ltree_every'.
          (∀a0.
             ltree_every' a0 ⇒
             ∃a ts. a0 = Branch a ts ∧ P a ts ∧ every ltree_every' ts) ⇒
          ∀a0. ltree_every' a0 ⇒ ltree_every P a0
   
   [ltree_every_rewrite]  Theorem
      
      ⊢ ltree_every P (Branch a ts) ⇔ P a ts ∧ every (ltree_every P) ts
   
   [ltree_every_rules]  Theorem
      
      ⊢ ∀P a ts.
          P a ts ∧ every (ltree_every P) ts ⇒ ltree_every P (Branch a ts)
   
   [ltree_finite]  Theorem
      
      ⊢ ltree_finite (Branch a ts) ⇔
        LFINITE ts ∧ ∀t. t ∈ LSET ts ⇒ ltree_finite t
   
   [ltree_finite_cases]  Theorem
      
      ⊢ ∀a0.
          ltree_finite a0 ⇔
          ∃a ts. a0 = Branch a (fromList ts) ∧ EVERY ltree_finite ts
   
   [ltree_finite_from_rose]  Theorem
      
      ⊢ ltree_finite t ⇔ ∃r. from_rose r = t
   
   [ltree_finite_imp_finite_branching]  Theorem
      
      ⊢ ∀t. ltree_finite t ⇒ finite_branching t
   
   [ltree_finite_ind]  Theorem
      
      ⊢ ∀P. (∀a ts. EVERY P ts ⇒ P (Branch a (fromList ts))) ⇒
            ∀t. ltree_finite t ⇒ P t
   
   [ltree_finite_rules]  Theorem
      
      ⊢ ∀a ts.
          EVERY ltree_finite ts ⇒ ltree_finite (Branch a (fromList ts))
   
   [ltree_finite_strongind]  Theorem
      
      ⊢ ∀P. (∀a ts.
               EVERY (λa0. ltree_finite a0 ∧ P a0) ts ⇒
               P (Branch a (fromList ts))) ⇒
            ∀t. ltree_finite t ⇒ P t
   
   [ltree_lookup]  Theorem
      
      ⊢ ltree_lookup t [] = SOME t ∧
        ltree_lookup t (n::ns) =
        case LNTH n (ltree_children t) of
          NONE => NONE
        | SOME a => ltree_lookup a ns
   
   [ltree_lookup_def]  Theorem
      
      ⊢ ltree_lookup t [] = SOME t ∧
        ltree_lookup (Branch a ts) (n::ns) =
        case LNTH n ts of NONE => NONE | SOME t => ltree_lookup t ns
   
   [ltree_lookup_valid]  Theorem
      
      ⊢ ∀p t. p ∈ ltree_paths t ⇔ ltree_lookup t p ≠ NONE
   
   [ltree_lookup_valid_inclusive]  Theorem
      
      ⊢ ∀p t. p ∈ ltree_paths t ⇔ ∀p'. p' ≼ p ⇒ ltree_lookup t p' ≠ NONE
   
   [ltree_map]  Theorem
      
      ⊢ ltree_map f (Branch a xs) = Branch (f a) (LMAP (ltree_map f) xs)
   
   [ltree_map_id]  Theorem
      
      ⊢ ltree_map I t = t
   
   [ltree_map_map]  Theorem
      
      ⊢ ltree_map f (ltree_map g t) = ltree_map (f ∘ g) t
   
   [ltree_node_children_reduce]  Theorem
      
      ⊢ Branch (ltree_node t) (ltree_children t) = t
   
   [ltree_node_def]  Theorem
      
      ⊢ ltree_node (Branch a ts) = a
   
   [ltree_node_ind]  Theorem
      
      ⊢ ∀P. (∀a ts. P (Branch a ts)) ⇒ ∀v. P v
   
   [ltree_paths_alt]  Theorem
      
      ⊢ ∀t. ltree_paths A = {p | ltree_el A p ≠ NONE}
   
   [ltree_paths_inclusive]  Theorem
      
      ⊢ ∀l1 l2 t. l1 ≼ l2 ∧ l2 ∈ ltree_paths t ⇒ l1 ∈ ltree_paths t
   
   [ltree_rel]  Theorem
      
      ⊢ ltree_rel R (Branch a ts) (Branch b us) ⇔
        R a b ∧ llist_rel (ltree_rel R) ts us
   
   [ltree_rel_O]  Theorem
      
      ⊢ ltree_rel R1 ∘ᵣ ltree_rel R2 ⊆ᵣ ltree_rel (R1 ∘ᵣ R2)
   
   [ltree_rel_eq]  Theorem
      
      ⊢ ltree_rel $= x y ⇔ x = y
   
   [ltree_set]  Theorem
      
      ⊢ ltree_set (Branch a ts) =
        a INSERT BIGUNION (IMAGE ltree_set (LSET ts))
   
   [ltree_set_map]  Theorem
      
      ⊢ ltree_set (ltree_map f t) = IMAGE f (ltree_set t)
   
   [ltree_unfold]  Theorem
      
      ⊢ ltree_unfold f seed =
        (let (a,seeds) = f seed in Branch a (LMAP (ltree_unfold f) seeds))
   
   [rose_tree_11]  Theorem
      
      ⊢ ∀a0 a1 a0' a1'. Rose a0 a1 = Rose a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
   
   [rose_tree_Axiom]  Theorem
      
      ⊢ ∀f0 f1 f2. ∃fn0 fn1.
          (∀a0 a1. fn0 (Rose a0 a1) = f0 a0 a1 (fn1 a1)) ∧ fn1 [] = f1 ∧
          ∀a0 a1. fn1 (a0::a1) = f2 a0 a1 (fn0 a0) (fn1 a1)
   
   [rose_tree_case_cong]  Theorem
      
      ⊢ ∀M M' f.
          M = M' ∧ (∀a0 a1. M' = Rose a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒
          rose_tree_CASE M f = rose_tree_CASE M' f'
   
   [rose_tree_case_eq]  Theorem
      
      ⊢ rose_tree_CASE x f = v ⇔ ∃a l. x = Rose a l ∧ f a l = v
   
   [rose_tree_induction]  Theorem
      
      ⊢ ∀P. (∀a ts. (∀a'. MEM a' ts ⇒ P a') ⇒ P (Rose a ts)) ⇒ ∀v. P v
   
   [rose_tree_nchotomy]  Theorem
      
      ⊢ ∀rr. ∃a l. rr = Rose a l
   
   [rose_tree_size_eq]  Theorem
      
      ⊢ rose_tree1_size f = list_size (rose_tree_size f)
   
   [subtrees]  Theorem
      
      ⊢ subtrees (Branch a ts) =
        Branch a ts INSERT BIGUNION (IMAGE subtrees (LSET ts))
   
   
*)
end

HOL 4, Trindemossen-1