Structure ltreeTheory
signature ltreeTheory =
sig
type thm = Thm.thm
(* Definitions *)
val finite_branching_def : thm
val ltree_TY_DEF : thm
val ltree_branching_def : thm
val ltree_children_def_primitive : thm
val ltree_delete_def : thm
val ltree_insert_def : 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 parent_inclusive_def : thm
val path_index_def : thm
val rose_children_def : thm
val rose_node_def : thm
val rose_tree_TY_DEF : thm
val rose_tree_case_def : thm
val rose_tree_size_def : thm
val sibling_inclusive_def : thm
val subtrees_def : thm
val to_rose_def : thm
(* Theorems *)
val Branch_11 : thm
val IN_ltree_paths : 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_ltree_el_cases : thm
val finite_branching_rewrite : thm
val finite_branching_rules : thm
val finite_branching_rules' : thm
val from_rose : thm
val from_rose_11 : thm
val from_rose_def : thm
val from_rose_ind : thm
val gen_ltree : thm
val gen_ltree_LNIL : thm
val gen_ltree_unchanged : thm
val gen_ltree_unchanged_extra : 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_branching_CONS : thm
val ltree_branching_NIL : thm
val ltree_branching_alt_ltree_lookup : thm
val ltree_branching_ltree_paths : thm
val ltree_cases : thm
val ltree_children_def : thm
val ltree_children_ind : thm
val ltree_delete_CONS : thm
val ltree_delete_NIL : thm
val ltree_delete_path_stable : thm
val ltree_delete_paths : thm
val ltree_el : thm
val ltree_el_alt_ltree_lookup : thm
val ltree_el_def : thm
val ltree_el_eqv : thm
val ltree_el_ltree_delete : thm
val ltree_el_ltree_delete' : thm
val ltree_el_ltree_insert : thm
val ltree_el_ltree_insert' : 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_alt_ltree_paths : thm
val ltree_finite_by_unfolding : thm
val ltree_finite_by_unfolding' : thm
val ltree_finite_cases : thm
val ltree_finite_from_rose : thm
val ltree_finite_imp_finite_branching : thm
val ltree_finite_imp_finite_ltree_paths : thm
val ltree_finite_ind : thm
val ltree_finite_ltree_insert : thm
val ltree_finite_rules : thm
val ltree_finite_strongind : thm
val ltree_insert_CONS : thm
val ltree_insert_NIL : thm
val ltree_insert_delete : thm
val ltree_insert_delete' : thm
val ltree_insert_path_stable : thm
val ltree_insert_paths : thm
val ltree_lookup : thm
val ltree_lookup_SNOC : thm
val ltree_lookup_append : 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_path_le_total : thm
val ltree_path_lt : thm
val ltree_path_lt_antisymmetric : thm
val ltree_path_lt_irreflexive : thm
val ltree_path_lt_sibling : thm
val ltree_path_lt_sibling' : thm
val ltree_path_lt_transitive : thm
val ltree_paths_alt_ltree_el : thm
val ltree_paths_inclusive : thm
val ltree_paths_map_cong : 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 parent_inclusive_ltree_paths : thm
val parent_inclusive_union : thm
val path_index_in_paths : thm
val path_index_thm : thm
val rose_children_to_rose : thm
val rose_children_to_rose' : thm
val rose_node_to_rose : thm
val rose_reduce : thm
val rose_reduce_def : thm
val rose_reduce_ind : 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 sibling_inclusive_ltree_paths : thm
val sibling_inclusive_union : thm
val subtrees : thm
val to_rose_thm : thm
(*
[alist] Parent theory of "ltree"
[iterate] Parent theory of "ltree"
[llist] 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_branching_def] Definition
⊢ ∀t p. ltree_branching t p = SND (THE (ltree_el t p))
[ltree_children_def_primitive] Definition
⊢ ltree_children =
WFREC (@R. WF R)
(λltree_children a'. case a' of Branch a ts => I ts)
[ltree_delete_def] Definition
⊢ ∀f t p.
ltree_delete f t p =
gen_ltree
(λns.
(let
(d,len) = THE (ltree_el t ns);
m = THE len
in
if ns = p ∧ len ≠ NONE ∧ 0 < m then (f d,SOME (m − 1))
else (d,len)))
[ltree_insert_def] Definition
⊢ ∀f t p t0.
ltree_insert f t p t0 =
gen_ltree
(λns.
if ltree_el t ns ≠ NONE then
(let
(d,len) = THE (ltree_el t ns);
m = THE len
in
if ns = p ∧ len ≠ NONE then (f d,SOME (m + 1))
else (d,len))
else THE (ltree_el t0 (DROP (LENGTH p + 1) ns)))
[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}
[parent_inclusive_def] Definition
⊢ ∀s. parent_inclusive s ⇔ ∀p q. p ∈ s ∧ q ≼ p ⇒ q ∈ s
[path_index_def] Definition
⊢ ∀s. FINITE s ⇒
s = IMAGE (path_index s) (count (CARD s)) ∧
∀j k.
j < CARD s ∧ k < CARD s ∧ j < k ⇒
¬ltree_path_lt (path_index s k) (path_index s j)
[rose_children_def] Definition
⊢ ∀a ts. rose_children (Rose a ts) = ts
[rose_node_def] Definition
⊢ ∀a ts. rose_node (Rose a ts) = a
[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)
[sibling_inclusive_def] Definition
⊢ ∀s. sibling_inclusive s ⇔
∀p q.
p ∈ s ∧ p ≠ [] ∧ q ≠ [] ∧ FRONT q = FRONT p ∧ LAST q < LAST p ⇒
q ∈ s
[subtrees_def] Definition
⊢ ∀t. subtrees t = {u | ∃path. ltree_lookup t path = SOME u}
[to_rose_def] Definition
⊢ ∀t. ltree_finite t ⇒ from_rose (to_rose t) = t
[Branch_11] Theorem
⊢ ∀a1 a2 ts1 ts2. Branch a1 ts1 = Branch a2 ts2 ⇔ a1 = a2 ∧ ts1 = ts2
[IN_ltree_paths] 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_ltree_el_cases] Theorem
⊢ ∀p t.
finite_branching t ∧ p ∈ ltree_paths t ⇒
∃d m. ltree_el t p = SOME (d,SOME m)
[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] Theorem
⊢ ∀t. from_rose t =
Branch (rose_node t)
(fromList (MAP from_rose (rose_children t)))
[from_rose_11] Theorem
⊢ ∀r1 r2. from_rose r1 = from_rose r2 ⇔ r1 = r2
[from_rose_def] Theorem
⊢ ∀ts a.
from_rose (Rose a ts) = Branch a (fromList (MAP from_rose 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)
[gen_ltree_unchanged] Theorem
⊢ ∀t. gen_ltree (λp. THE (ltree_el t p)) = t
[gen_ltree_unchanged_extra] Theorem
⊢ ∀t f.
gen_ltree
(λp. if ltree_el t p ≠ NONE then THE (ltree_el t p) else f p) =
t
[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_branching_CONS] Theorem
⊢ ∀h p a ts.
h::p ∈ ltree_paths (Branch a ts) ⇒
ltree_branching (Branch a ts) (h::p) =
ltree_branching (THE (LNTH h ts)) p
[ltree_branching_NIL] Theorem
⊢ ∀a ts. ltree_branching (Branch a ts) [] = LLENGTH ts
[ltree_branching_alt_ltree_lookup] Theorem
⊢ ∀p t.
p ∈ ltree_paths t ⇒
ltree_branching t p =
LLENGTH (ltree_children (THE (ltree_lookup t p)))
[ltree_branching_ltree_paths] Theorem
⊢ ∀p t m.
p ∈ ltree_paths t ∧ ltree_branching t p = SOME m ⇒
∀h. h < m ⇔ SNOC h p ∈ ltree_paths t
[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_delete_CONS] Theorem
⊢ ∀f a ts h p t.
LNTH h ts = SOME t ∧ ltree_el t p ≠ NONE ⇒
ltree_delete f (Branch a ts) (h::p) =
Branch a
(LGENLIST
(λi.
if i = h then ltree_delete f (THE (LNTH h ts)) p
else THE (LNTH i ts)) (LLENGTH ts))
[ltree_delete_NIL] Theorem
⊢ ∀f a ts.
ltree_delete f (Branch a ts) [] =
if LFINITE ts ∧ 0 < THE (LLENGTH ts) then
Branch (f a)
(LGENLIST (λi. THE (LNTH i ts)) (SOME (THE (LLENGTH ts) − 1)))
else Branch a ts
[ltree_delete_path_stable] Theorem
⊢ ∀f p t. p ∈ ltree_paths t ⇒ p ∈ ltree_paths (ltree_delete f t p)
[ltree_delete_paths] Theorem
⊢ ∀f p t n.
p ∈ ltree_paths t ∧ ltree_branching t p = SOME (SUC n) ⇒
ltree_paths (ltree_delete f t p) =
ltree_paths t DIFF
IMAGE (λq. SNOC n p ⧺ q)
(ltree_paths (THE (ltree_lookup t (SNOC n p))))
[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_alt_ltree_lookup] Theorem
⊢ ∀p t.
p ∈ ltree_paths t ⇒
ltree_el t p =
do
t' <- ltree_lookup t p;
SOME (ltree_node t',LLENGTH (ltree_children t'))
od
[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_ltree_delete] Theorem
⊢ ∀f p t.
ltree_el t p = SOME (a,SOME (SUC n)) ⇒
ltree_el (ltree_delete f t p) p = SOME (f a,SOME n)
[ltree_el_ltree_delete'] Theorem
⊢ ∀p t.
ltree_el t p = SOME (a,SOME (SUC n)) ⇒
ltree_el (ltree_delete' t p) p = SOME (a,SOME n)
[ltree_el_ltree_insert] Theorem
⊢ ∀f p t t0.
ltree_el t p = SOME (a,SOME n) ⇒
ltree_el (ltree_insert f t p t0) p = SOME (f a,SOME (SUC n))
[ltree_el_ltree_insert'] Theorem
⊢ ∀p t t0.
ltree_el t p = SOME (a,SOME n) ⇒
ltree_el (ltree_insert' t p t0) p = SOME (a,SOME (SUC n))
[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_alt_ltree_paths] Theorem
⊢ ∀t. ltree_finite t ⇔ FINITE (ltree_paths t)
[ltree_finite_by_unfolding] Theorem
⊢ ∀P f.
(∃m. ∀seed.
P seed ⇒
(let
(a,seeds) = f seed
in
LFINITE seeds ∧ every (λe. P e ∧ m e < m seed) seeds)) ⇒
∀seed. P seed ⇒ ltree_finite (ltree_unfold f seed)
[ltree_finite_by_unfolding'] Theorem
⊢ ∀f. (∃m. ∀seed.
(let
(a,seeds) = f seed
in
LFINITE seeds ∧ every (λe. m e < m seed) seeds)) ⇒
∀seed. ltree_finite (ltree_unfold f seed)
[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_imp_finite_ltree_paths] Theorem
⊢ ∀t. ltree_finite t ⇒ FINITE (ltree_paths t)
[ltree_finite_ind] Theorem
⊢ ∀P. (∀a ts. EVERY P ts ⇒ P (Branch a (fromList ts))) ⇒
∀t. ltree_finite t ⇒ P t
[ltree_finite_ltree_insert] Theorem
⊢ ∀f p t t0.
ltree_finite t ∧ p ∈ ltree_paths t ∧ ltree_finite t0 ⇒
ltree_finite (ltree_insert f t p t0)
[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_insert_CONS] Theorem
⊢ ∀f a ts h p t t0.
LNTH h ts = SOME t ∧ ltree_el t p ≠ NONE ⇒
ltree_insert f (Branch a ts) (h::p) t0 =
Branch a
(LGENLIST
(λi.
if i = h then ltree_insert f (THE (LNTH h ts)) p t0
else THE (LNTH i ts)) (LLENGTH ts))
[ltree_insert_NIL] Theorem
⊢ ∀f a ts t0.
ltree_insert f (Branch a ts) [] t0 =
if LFINITE ts then
Branch (f a)
(LGENLIST
(λi. if i < THE (LLENGTH ts) then THE (LNTH i ts) else t0)
(SOME (THE (LLENGTH ts) + 1)))
else Branch a ts
[ltree_insert_delete] Theorem
⊢ ∀n p t t0 f g d len.
ltree_branching t p = SOME (SUC n) ∧
ltree_lookup t (SNOC n p) = SOME t0 ∧
ltree_el t p = SOME (d,len) ∧ f (g d) = d ⇒
ltree_insert f (ltree_delete g t p) p t0 = t
[ltree_insert_delete'] Theorem
⊢ ∀n p t t0.
ltree_branching t p = SOME (SUC n) ∧
ltree_lookup t (SNOC n p) = SOME t0 ⇒
ltree_insert' (ltree_delete' t p) p t0 = t
[ltree_insert_path_stable] Theorem
⊢ ∀f p t t0.
p ∈ ltree_paths t ⇒ p ∈ ltree_paths (ltree_insert f t p t0)
[ltree_insert_paths] Theorem
⊢ ∀f p t n t0.
p ∈ ltree_paths t ∧ ltree_branching t p = SOME n ⇒
ltree_paths (ltree_insert f t p t0) =
ltree_paths t ∪ IMAGE (λq. SNOC n p ⧺ q) (ltree_paths t0)
[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_SNOC] Theorem
⊢ ∀t x xs.
ltree_lookup t xs ≠ NONE ⇒
ltree_lookup t (SNOC x xs) =
ltree_lookup (THE (ltree_lookup t xs)) [x]
[ltree_lookup_append] Theorem
⊢ ∀l1 l2 t.
ltree_lookup t l1 ≠ NONE ⇒
ltree_lookup t (l1 ⧺ l2) =
ltree_lookup (THE (ltree_lookup t l1)) l2
[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_path_le_total] Theorem
⊢ total ltree_path_le
[ltree_path_lt] Theorem
⊢ (¬ltree_path_lt [] [] ∧ ¬ltree_path_lt (h1::t1) []) ∧
ltree_path_lt [] (h2::t2) ∧
(ltree_path_lt (h1::t1) (h2::t2) ⇔
LENGTH t1 < LENGTH t2 ∨
LENGTH t1 = LENGTH t2 ∧ (h1 < h2 ∨ h1 = h2 ∧ ltree_path_lt t1 t2))
[ltree_path_lt_antisymmetric] Theorem
⊢ antisymmetric ltree_path_lt
[ltree_path_lt_irreflexive] Theorem
⊢ irreflexive ltree_path_lt
[ltree_path_lt_sibling] Theorem
⊢ ∀p q.
p ≠ [] ∧ q ≠ [] ∧ FRONT p = FRONT q ∧ LAST p < LAST q ⇒
ltree_path_lt p q
[ltree_path_lt_sibling'] Theorem
⊢ ∀x y xs. x < y ⇒ ltree_path_lt (SNOC x xs) (SNOC y xs)
[ltree_path_lt_transitive] Theorem
⊢ transitive ltree_path_lt
[ltree_paths_alt_ltree_el] Theorem
⊢ ∀t. ltree_paths t = {p | ltree_el t p ≠ NONE}
[ltree_paths_inclusive] Theorem
⊢ ∀l1 l2 t. l1 ≼ l2 ∧ l2 ∈ ltree_paths t ⇒ l1 ∈ ltree_paths t
[ltree_paths_map_cong] Theorem
⊢ ∀f t. ltree_paths (ltree_map f t) = 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))
[parent_inclusive_ltree_paths] Theorem
⊢ ∀t. parent_inclusive (ltree_paths t)
[parent_inclusive_union] Theorem
⊢ ∀s1 s2.
parent_inclusive s1 ∧ parent_inclusive s2 ⇒
parent_inclusive (s1 ∪ s2)
[path_index_in_paths] Theorem
⊢ ∀s i. FINITE s ∧ i < CARD s ⇒ path_index s i ∈ s
[path_index_thm] Theorem
⊢ ∀s n.
s HAS_SIZE n ⇒
BIJ (path_index s) (count n) s ∧
∀j k.
j < n ∧ k < n ⇒
(ltree_path_lt (path_index s j) (path_index s k) ⇔ j < k)
[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)))
[rose_node_to_rose] Theorem
⊢ ∀t. ltree_finite t ⇒ rose_node (to_rose t) = ltree_node t
[rose_reduce] Theorem
⊢ ∀f t.
rose_reduce f t =
f (rose_node t) (MAP (rose_reduce f) (rose_children t))
[rose_reduce_def] Theorem
⊢ ∀f a ts. rose_reduce f (Rose a ts) = f a (MAP (rose_reduce f) ts)
[rose_reduce_ind] Theorem
⊢ ∀P. (∀f a ts. (∀a'. MEM a' ts ⇒ P f a') ⇒ P f (Rose a ts)) ⇒
∀v v1. P v v1
[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
[sibling_inclusive_ltree_paths] Theorem
⊢ ∀t. sibling_inclusive (ltree_paths t)
[sibling_inclusive_union] Theorem
⊢ ∀s1 s2.
sibling_inclusive s1 ∧ sibling_inclusive s2 ⇒
sibling_inclusive (s1 ∪ s2)
[subtrees] Theorem
⊢ subtrees (Branch a ts) =
Branch a ts INSERT BIGUNION (IMAGE subtrees (LSET ts))
[to_rose_thm] Theorem
⊢ ∀r. to_rose (from_rose r) = r
*)
end
HOL 4, Trindemossen-2