Structure ltreeTheory
signature ltreeTheory =
sig
type thm = Thm.thm
(* Definitions *)
val ltree_TY_DEF : thm
val ltree_map_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 datatype_ltree : thm
val datatype_rose_tree : 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_eq : thm
val ltree_bisimulation : thm
val ltree_cases : thm
val ltree_el_def : thm
val ltree_el_eqv : thm
val ltree_finite : thm
val ltree_finite_cases : thm
val ltree_finite_from_rose : thm
val ltree_finite_ind : thm
val ltree_finite_rules : thm
val ltree_finite_strongind : thm
val ltree_lookup_def : thm
val ltree_map : thm
val ltree_map_id : thm
val ltree_map_map : 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 subtrees : thm
val ltree_grammars : type_grammar.grammar * term_grammar.grammar
(*
[alist] Parent theory of "ltree"
[llist] Parent theory of "ltree"
[ltree_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION ltree_rep_ok rep
[ltree_map_def] Definition
⊢ ∀f. ltree_map f =
ltree_unfold (λt. case t of Branch a ts => (f a,ts))
[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
[datatype_ltree] Theorem
⊢ DATATYPE (ltree Branch)
[datatype_rose_tree] Theorem
⊢ DATATYPE (rose_tree Rose)
[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_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_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_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_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_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_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_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
[subtrees] Theorem
⊢ subtrees (Branch a ts) =
Branch a ts INSERT BIGUNION (IMAGE subtrees (LSET ts))
*)
end
HOL 4, Kananaskis-14