Structure lbtreeTheory
signature lbtreeTheory =
sig
type thm = Thm.thm
(* Definitions *)
val Lf_def : thm
val Lfrep_def : thm
val Nd_def : thm
val Ndrep_def : thm
val bf_flatten_def : thm
val is_lbtree_def : thm
val is_mmindex_def : thm
val lbtree_TY_DEF : thm
val lbtree_absrep : thm
val lbtree_case_def : thm
val map_def : thm
val mindepth_def : thm
val path_follow_def : thm
(* Theorems *)
val EXISTS_FIRST : thm
val Lf_NOT_Nd : thm
val Nd_11 : thm
val bf_flatten_append : thm
val bf_flatten_eq_lnil : thm
val depth_cases : thm
val depth_ind : thm
val depth_mem : thm
val depth_rules : thm
val depth_strongind : thm
val exists_bf_flatten : thm
val finite_cases : thm
val finite_ind : thm
val finite_map : thm
val finite_rules : thm
val finite_strongind : thm
val finite_thm : thm
val lbtree_bisimulation : thm
val lbtree_case_thm : thm
val lbtree_cases : thm
val lbtree_strong_bisimulation : thm
val lbtree_ue_Axiom : thm
val map_eq_Lf : thm
val map_eq_Nd : thm
val mem_bf_flatten : thm
val mem_cases : thm
val mem_depth : thm
val mem_ind : thm
val mem_mindepth : thm
val mem_rules : thm
val mem_strongind : thm
val mem_thm : thm
val mindepth_depth : thm
val mindepth_thm : thm
val mmindex_EXISTS : thm
val mmindex_unique : thm
val optmin_def : thm
val optmin_ind : thm
val lbtree_grammars : type_grammar.grammar * term_grammar.grammar
(*
[llist] Parent theory of "lbtree"
[Lf_def] Definition
⊢ Lf = lbtree_abs Lfrep
[Lfrep_def] Definition
⊢ Lfrep = (λl. NONE)
[Nd_def] Definition
⊢ ∀a t1 t2.
Nd a t1 t2 = lbtree_abs (Ndrep a (lbtree_rep t1) (lbtree_rep t2))
[Ndrep_def] Definition
⊢ ∀a t1 t2.
Ndrep a t1 t2 =
(λl. case l of [] => SOME a | T::xs => t1 xs | F::xs => t2 xs)
[bf_flatten_def] Definition
⊢ bf_flatten [] = [||] ∧ (∀ts. bf_flatten (Lf::ts) = bf_flatten ts) ∧
∀a t1 t2 ts.
bf_flatten (Nd a t1 t2::ts) = a:::bf_flatten (ts ⧺ [t1; t2])
[is_lbtree_def] Definition
⊢ ∀t. is_lbtree t ⇔
∃P. (∀t. P t ⇒
t = Lfrep ∨ ∃a t1 t2. P t1 ∧ P t2 ∧ t = Ndrep a t1 t2) ∧
P t
[is_mmindex_def] Definition
⊢ ∀f l n d.
lbtree$is_mmindex f l n d ⇔
n < LENGTH l ∧ f (EL n l) = SOME d ∧
∀i. i < LENGTH l ⇒
f (EL i l) = NONE ∨
∃d'. f (EL i l) = SOME d' ∧ d ≤ d' ∧ (i < n ⇒ d < d')
[lbtree_TY_DEF] Definition
⊢ ∃rep. TYPE_DEFINITION is_lbtree rep
[lbtree_absrep] Definition
⊢ (∀a. lbtree_abs (lbtree_rep a) = a) ∧
∀r. is_lbtree r ⇔ lbtree_rep (lbtree_abs r) = r
[lbtree_case_def] Definition
⊢ ∀e f t.
lbtree_case e f t =
if t = Lf then e
else
f (@a. ∃t1 t2. t = Nd a t1 t2) (@t1. ∃a t2. t = Nd a t1 t2)
(@t2. ∃a t1. t = Nd a t1 t2)
[map_def] Definition
⊢ ∀f. map f Lf = Lf ∧
∀a t1 t2. map f (Nd a t1 t2) = Nd (f a) (map f t1) (map f t2)
[mindepth_def] Definition
⊢ ∀x t.
lbtree$mindepth x t =
if mem x t then SOME (LEAST n. lbtree$depth x t n) else NONE
[path_follow_def] Definition
⊢ (∀g x. path_follow g x [] = OPTION_MAP FST (g x)) ∧
∀g x h t.
path_follow g x (h::t) =
case g x of
NONE => NONE
| SOME (a,y,z) => path_follow g (if h then y else z) t
[EXISTS_FIRST] Theorem
⊢ ∀l. EXISTS P l ⇒ ∃l1 x l2. l = l1 ⧺ x::l2 ∧ EVERY ($¬ ∘ P) l1 ∧ P x
[Lf_NOT_Nd] Theorem
⊢ Lf ≠ Nd a t1 t2
[Nd_11] Theorem
⊢ Nd a1 t1 u1 = Nd a2 t2 u2 ⇔ a1 = a2 ∧ t1 = t2 ∧ u1 = u2
[bf_flatten_append] Theorem
⊢ ∀l1. EVERY ($= Lf) l1 ⇒ bf_flatten (l1 ⧺ l2) = bf_flatten l2
[bf_flatten_eq_lnil] Theorem
⊢ ∀l. bf_flatten l = [||] ⇔ EVERY ($= Lf) l
[depth_cases] Theorem
⊢ ∀a0 a1 a2.
lbtree$depth a0 a1 a2 ⇔
(∃t1 t2. a1 = Nd a0 t1 t2 ∧ a2 = 0) ∨
(∃m a t1 t2. a1 = Nd a t1 t2 ∧ a2 = SUC m ∧ lbtree$depth a0 t1 m) ∨
∃m a t1 t2. a1 = Nd a t1 t2 ∧ a2 = SUC m ∧ lbtree$depth a0 t2 m
[depth_ind] Theorem
⊢ ∀depth'.
(∀x t1 t2. depth' x (Nd x t1 t2) 0) ∧
(∀m x a t1 t2. depth' x t1 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ∧
(∀m x a t1 t2. depth' x t2 m ⇒ depth' x (Nd a t1 t2) (SUC m)) ⇒
∀a0 a1 a2. lbtree$depth a0 a1 a2 ⇒ depth' a0 a1 a2
[depth_mem] Theorem
⊢ ∀x t n. lbtree$depth x t n ⇒ mem x t
[depth_rules] Theorem
⊢ (∀x t1 t2. lbtree$depth x (Nd x t1 t2) 0) ∧
(∀m x a t1 t2.
lbtree$depth x t1 m ⇒ lbtree$depth x (Nd a t1 t2) (SUC m)) ∧
∀m x a t1 t2.
lbtree$depth x t2 m ⇒ lbtree$depth x (Nd a t1 t2) (SUC m)
[depth_strongind] Theorem
⊢ ∀depth'.
(∀x t1 t2. depth' x (Nd x t1 t2) 0) ∧
(∀m x a t1 t2.
lbtree$depth x t1 m ∧ depth' x t1 m ⇒
depth' x (Nd a t1 t2) (SUC m)) ∧
(∀m x a t1 t2.
lbtree$depth x t2 m ∧ depth' x t2 m ⇒
depth' x (Nd a t1 t2) (SUC m)) ⇒
∀a0 a1 a2. lbtree$depth a0 a1 a2 ⇒ depth' a0 a1 a2
[exists_bf_flatten] Theorem
⊢ exists ($= x) (bf_flatten tlist) ⇒ EXISTS (mem x) tlist
[finite_cases] Theorem
⊢ ∀a0.
finite a0 ⇔
a0 = Lf ∨ ∃a t1 t2. a0 = Nd a t1 t2 ∧ finite t1 ∧ finite t2
[finite_ind] Theorem
⊢ ∀finite'.
finite' Lf ∧
(∀a t1 t2. finite' t1 ∧ finite' t2 ⇒ finite' (Nd a t1 t2)) ⇒
∀a0. finite a0 ⇒ finite' a0
[finite_map] Theorem
⊢ finite (map f t) ⇔ finite t
[finite_rules] Theorem
⊢ finite Lf ∧ ∀a t1 t2. finite t1 ∧ finite t2 ⇒ finite (Nd a t1 t2)
[finite_strongind] Theorem
⊢ ∀finite'.
finite' Lf ∧
(∀a t1 t2.
finite t1 ∧ finite' t1 ∧ finite t2 ∧ finite' t2 ⇒
finite' (Nd a t1 t2)) ⇒
∀a0. finite a0 ⇒ finite' a0
[finite_thm] Theorem
⊢ (finite Lf ⇔ T) ∧ (finite (Nd a t1 t2) ⇔ finite t1 ∧ finite t2)
[lbtree_bisimulation] Theorem
⊢ ∀t u.
t = u ⇔
∃R. R t u ∧
∀t u.
R t u ⇒
t = Lf ∧ u = Lf ∨
∃a t1 u1 t2 u2.
R t1 u1 ∧ R t2 u2 ∧ t = Nd a t1 t2 ∧ u = Nd a u1 u2
[lbtree_case_thm] Theorem
⊢ lbtree_case e f Lf = e ∧ lbtree_case e f (Nd a t1 t2) = f a t1 t2
[lbtree_cases] Theorem
⊢ ∀t. t = Lf ∨ ∃a t1 t2. t = Nd a t1 t2
[lbtree_strong_bisimulation] Theorem
⊢ ∀t u.
t = u ⇔
∃R. R t u ∧
∀t u.
R t u ⇒
t = u ∨
∃a t1 u1 t2 u2.
R t1 u1 ∧ R t2 u2 ∧ t = Nd a t1 t2 ∧ u = Nd a u1 u2
[lbtree_ue_Axiom] Theorem
⊢ ∀f. ∃!g. ∀x.
g x = case f x of NONE => Lf | SOME (b,y,z) => Nd b (g y) (g z)
[map_eq_Lf] Theorem
⊢ (map f t = Lf ⇔ t = Lf) ∧ (Lf = map f t ⇔ t = Lf)
[map_eq_Nd] Theorem
⊢ map f t = Nd a t1 t2 ⇔
∃a' t1' t2'.
t = Nd a' t1' t2' ∧ a = f a' ∧ t1 = map f t1' ∧ t2 = map f t2'
[mem_bf_flatten] Theorem
⊢ exists ($= x) (bf_flatten tlist) ⇔ EXISTS (mem x) tlist
[mem_cases] Theorem
⊢ ∀a0 a1.
mem a0 a1 ⇔
(∃t1 t2. a1 = Nd a0 t1 t2) ∨
(∃b t1 t2. a1 = Nd b t1 t2 ∧ mem a0 t1) ∨
∃b t1 t2. a1 = Nd b t1 t2 ∧ mem a0 t2
[mem_depth] Theorem
⊢ ∀x t. mem x t ⇒ ∃n. lbtree$depth x t n
[mem_ind] Theorem
⊢ ∀mem'.
(∀a t1 t2. mem' a (Nd a t1 t2)) ∧
(∀a b t1 t2. mem' a t1 ⇒ mem' a (Nd b t1 t2)) ∧
(∀a b t1 t2. mem' a t2 ⇒ mem' a (Nd b t1 t2)) ⇒
∀a0 a1. mem a0 a1 ⇒ mem' a0 a1
[mem_mindepth] Theorem
⊢ ∀x t. mem x t ⇒ ∃n. lbtree$mindepth x t = SOME n
[mem_rules] Theorem
⊢ (∀a t1 t2. mem a (Nd a t1 t2)) ∧
(∀a b t1 t2. mem a t1 ⇒ mem a (Nd b t1 t2)) ∧
∀a b t1 t2. mem a t2 ⇒ mem a (Nd b t1 t2)
[mem_strongind] Theorem
⊢ ∀mem'.
(∀a t1 t2. mem' a (Nd a t1 t2)) ∧
(∀a b t1 t2. mem a t1 ∧ mem' a t1 ⇒ mem' a (Nd b t1 t2)) ∧
(∀a b t1 t2. mem a t2 ∧ mem' a t2 ⇒ mem' a (Nd b t1 t2)) ⇒
∀a0 a1. mem a0 a1 ⇒ mem' a0 a1
[mem_thm] Theorem
⊢ (mem a Lf ⇔ F) ∧ (mem a (Nd b t1 t2) ⇔ a = b ∨ mem a t1 ∨ mem a t2)
[mindepth_depth] Theorem
⊢ lbtree$mindepth x t = SOME n ⇒ lbtree$depth x t n
[mindepth_thm] Theorem
⊢ lbtree$mindepth x Lf = NONE ∧
lbtree$mindepth x (Nd a t1 t2) =
if x = a then SOME 0
else
OPTION_MAP SUC
(lbtree$optmin (lbtree$mindepth x t1) (lbtree$mindepth x t2))
[mmindex_EXISTS] Theorem
⊢ EXISTS (λe. ∃n. f e = SOME n) l ⇒ ∃i m. lbtree$is_mmindex f l i m
[mmindex_unique] Theorem
⊢ lbtree$is_mmindex f l i m ⇒
∀j n. lbtree$is_mmindex f l j n ⇔ j = i ∧ n = m
[optmin_def] Theorem
⊢ lbtree$optmin NONE NONE = NONE ∧
lbtree$optmin (SOME x) NONE = SOME x ∧
lbtree$optmin NONE (SOME y) = SOME y ∧
lbtree$optmin (SOME x) (SOME y) = SOME (MIN x y)
[optmin_ind] Theorem
⊢ ∀P. P NONE NONE ∧ (∀x. P (SOME x) NONE) ∧ (∀y. P NONE (SOME y)) ∧
(∀x y. P (SOME x) (SOME y)) ⇒
∀v v1. P v v1
*)
end
HOL 4, Trindemossen-1