Structure sptreeTheory
signature sptreeTheory =
sig
type thm = Thm.thm
(* Definitions *)
val delete_def : thm
val difference_def : thm
val domain_def : thm
val filter_v_def : thm
val foldi_def : thm
val fromAList_primitive_def : thm
val fromList_def : thm
val inter_def : thm
val inter_eq_def : thm
val list_insert_def : thm
val list_to_num_set_def : thm
val lrnext_primitive_def : thm
val map_def : thm
val mapi0_def : thm
val mapi_def : thm
val mk_wf_def : thm
val size_def : thm
val spt_TY_DEF : thm
val spt_case_def : thm
val spt_center_primitive_def : thm
val spt_centers_def : thm
val spt_fold_def : thm
val spt_left_def : thm
val spt_right_def : thm
val spt_size_alt_def : thm
val spt_size_def : thm
val toAList_def : thm
val toListA_def : thm
val toList_def : thm
val toSortedAList_def : thm
val union_def : thm
val wf_def : thm
(* Theorems *)
val ADD_1_SUC : thm
val ALL_DISTINCT_MAP_FST_toAList : thm
val ALOOKUP_aux_alist : thm
val ALOOKUP_spt_centers : thm
val ALOOKUP_toAList : thm
val ALOOKUP_toSortedAList : thm
val DIV_MOD_TIMES_2 : thm
val EL_CONS_IF : thm
val FINITE_domain : thm
val GREATER_EQ_alist_aux : thm
val IMP_size_LESS_size : thm
val IN_domain : thm
val LESS_spt_centers : thm
val MAP_foldi : thm
val MEM_FST_ALOOKUP_SOME : thm
val MEM_toAList : thm
val MEM_toList : thm
val MEM_toSortedAList : thm
val SORTED_MAP_FST_alist_aux : thm
val SORTED_MAP_FST_toSortedAList : thm
val SORTED_spt_centers : thm
val alist_insert_REVERSE : thm
val alist_insert_append : thm
val alist_insert_def : thm
val alist_insert_ind : thm
val alist_insert_pull_insert : thm
val aux_alist_def : thm
val aux_alist_ind : thm
val datatype_spt : thm
val delete_compute : thm
val delete_fail : thm
val delete_mk_wf : thm
val difference_sub : thm
val domain_FOLDR_delete : thm
val domain_alist_insert : thm
val domain_delete : thm
val domain_difference : thm
val domain_empty : thm
val domain_eq : thm
val domain_foldi : thm
val domain_fromAList : thm
val domain_fromList : thm
val domain_insert : thm
val domain_inter : thm
val domain_list_insert : thm
val domain_list_to_num_set : thm
val domain_lookup : thm
val domain_map : thm
val domain_mapi : thm
val domain_mk_wf : thm
val domain_sing : thm
val domain_union : thm
val foldi_FOLDR_toAList : thm
val fromAList_append : thm
val fromAList_def : thm
val fromAList_ind : thm
val fromAList_toAList : thm
val insert_compute : thm
val insert_def : thm
val insert_ind : thm
val insert_insert : thm
val insert_mk_wf : thm
val insert_notEmpty : thm
val insert_shadow : thm
val insert_swap : thm
val insert_unchanged : thm
val insert_union : thm
val inter_LN : thm
val inter_assoc : thm
val inter_eq : thm
val inter_eq_LN : thm
val inter_mk_wf : thm
val isEmpty_toList : thm
val isEmpty_toListA : thm
val isEmpty_union : thm
val list_size_APPEND : thm
val list_to_num_set_append : thm
val lookup_0_spt_center : thm
val lookup_FOLDL_union : thm
val lookup_NONE_domain : thm
val lookup_alist_insert : thm
val lookup_compute : thm
val lookup_def : thm
val lookup_delete : thm
val lookup_difference : thm
val lookup_filter_v : thm
val lookup_fromAList : thm
val lookup_fromAList_toAList : thm
val lookup_fromList : thm
val lookup_fromList_outside : thm
val lookup_ind : thm
val lookup_insert : thm
val lookup_insert1 : thm
val lookup_inter : thm
val lookup_inter_EQ : thm
val lookup_inter_alt : thm
val lookup_inter_assoc : thm
val lookup_inter_eq : thm
val lookup_list_to_num_set : thm
val lookup_map : thm
val lookup_map_K : thm
val lookup_mapi : thm
val lookup_mapi0 : thm
val lookup_mk_BN : thm
val lookup_mk_wf : thm
val lookup_spt_left : thm
val lookup_spt_right : thm
val lookup_union : thm
val lrnext_def : thm
val lrnext_ind : thm
val lrnext_thm : thm
val map_LN : thm
val map_fromAList : thm
val map_insert : thm
val map_map_K : thm
val map_map_o : thm
val map_union : thm
val mapi_Alist : thm
val mk_BN_def : thm
val mk_BN_ind : thm
val mk_BS_def : thm
val mk_BS_ind : thm
val mk_wf_eq : thm
val num_set_domain_eq : thm
val set_foldi_keys : thm
val size_delete : thm
val size_diff_less : thm
val size_domain : thm
val size_insert : thm
val spt_11 : thm
val spt_Axiom : thm
val spt_acc_0 : thm
val spt_acc_compute : thm
val spt_acc_def : thm
val spt_acc_eqn : thm
val spt_acc_ind : thm
val spt_acc_thm : thm
val spt_case_cong : thm
val spt_case_eq : thm
val spt_center_def : thm
val spt_center_ind : thm
val spt_centers_add_lemma : thm
val spt_centers_eq_map : thm
val spt_distinct : thm
val spt_eq_thm : thm
val spt_induction : thm
val spt_nchotomy : thm
val subspt_FOLDL_union : thm
val subspt_LN : thm
val subspt_def : thm
val subspt_domain : thm
val subspt_eq : thm
val subspt_lookup : thm
val subspt_refl : thm
val subspt_trans : thm
val subspt_union : thm
val sum_spt_size_alt_lemma : thm
val sum_spt_size_less : thm
val toListA_append : thm
val toList_map : thm
val union_LN : thm
val union_assoc : thm
val union_insert_LN : thm
val union_mk_wf : thm
val union_num_set_sym : thm
val wf_LN : thm
val wf_delete : thm
val wf_difference : thm
val wf_filter_v : thm
val wf_fromAList : thm
val wf_insert : thm
val wf_inter : thm
val wf_map : thm
val wf_mapi : thm
val wf_mk_BN : thm
val wf_mk_BS : thm
val wf_mk_id : thm
val wf_mk_wf : thm
val wf_union : thm
val sptree_grammars : type_grammar.grammar * term_grammar.grammar
(*
[alist] Parent theory of "sptree"
[logroot] Parent theory of "sptree"
[delete_def] Definition
⊢ (∀k. isEmpty (delete k LN)) ∧
(∀k a. delete k (LS a) = if k = 0 then LN else LS a) ∧
(∀k t1 t2.
delete k (BN t1 t2) =
if k = 0 then BN t1 t2
else if EVEN k then mk_BN (delete ((k − 1) DIV 2) t1) t2
else mk_BN t1 (delete ((k − 1) DIV 2) t2)) ∧
∀k t1 a t2.
delete k (BS t1 a t2) =
if k = 0 then BN t1 t2
else if EVEN k then mk_BS (delete ((k − 1) DIV 2) t1) a t2
else mk_BS t1 a (delete ((k − 1) DIV 2) t2)
[difference_def] Definition
⊢ (∀t. isEmpty (difference LN t)) ∧
(∀a t.
difference (LS a) t =
case t of
LN => LS a
| LS b => LN
| BN t1 t2 => LS a
| BS t1' b' t2' => LN) ∧
(∀t1 t2 t.
difference (BN t1 t2) t =
case t of
LN => BN t1 t2
| LS a => BN t1 t2
| BN t1' t2' => mk_BN (difference t1 t1') (difference t2 t2')
| BS t1'' a'' t2'' =>
mk_BN (difference t1 t1'') (difference t2 t2'')) ∧
∀t1 a t2 t.
difference (BS t1 a t2) t =
case t of
LN => BS t1 a t2
| LS a' => BN t1 t2
| BN t1' t2' => mk_BS (difference t1 t1') a (difference t2 t2')
| BS t1'' a'³' t2'' =>
mk_BN (difference t1 t1'') (difference t2 t2'')
[domain_def] Definition
⊢ domain LN = ∅ ∧ (∀v0. domain (LS v0) = {0}) ∧
(∀t1 t2.
domain (BN t1 t2) =
IMAGE (λn. 2 * n + 2) (domain t1) ∪
IMAGE (λn. 2 * n + 1) (domain t2)) ∧
∀t1 v1 t2.
domain (BS t1 v1 t2) =
{0} ∪ IMAGE (λn. 2 * n + 2) (domain t1) ∪
IMAGE (λn. 2 * n + 1) (domain t2)
[filter_v_def] Definition
⊢ (∀f. isEmpty (filter_v f LN)) ∧
(∀f x. filter_v f (LS x) = if f x then LS x else LN) ∧
(∀f l r. filter_v f (BN l r) = mk_BN (filter_v f l) (filter_v f r)) ∧
∀f l x r.
filter_v f (BS l x r) =
if f x then mk_BS (filter_v f l) x (filter_v f r)
else mk_BN (filter_v f l) (filter_v f r)
[foldi_def] Definition
⊢ (∀f i acc. foldi f i acc LN = acc) ∧
(∀f i acc a. foldi f i acc (LS a) = f i a acc) ∧
(∀f i acc t1 t2.
foldi f i acc (BN t1 t2) =
(let
inc = sptree$lrnext i
in
foldi f (i + inc) (foldi f (i + 2 * inc) acc t1) t2)) ∧
∀f i acc t1 a t2.
foldi f i acc (BS t1 a t2) =
(let
inc = sptree$lrnext i
in
foldi f (i + inc) (f i a (foldi f (i + 2 * inc) acc t1)) t2)
[fromAList_primitive_def] Definition
⊢ fromAList =
WFREC (@R. WF R ∧ ∀y x xs. R xs ((x,y)::xs))
(λfromAList a.
case a of
[] => I LN
| (x,y)::xs => I (insert x y (fromAList xs)))
[fromList_def] Definition
⊢ ∀l.
fromList l =
SND (FOLDL (λ(i,t) a. (i + 1,insert i a t)) (0,LN) l)
[inter_def] Definition
⊢ (∀t. isEmpty (inter LN t)) ∧
(∀a t.
inter (LS a) t =
case t of
LN => LN
| LS b => LS a
| BN t1 t2 => LN
| BS t1' v4 t2' => LS a) ∧
(∀t1 t2 t.
inter (BN t1 t2) t =
case t of
LN => LN
| LS a => LN
| BN t1' t2' => mk_BN (inter t1 t1') (inter t2 t2')
| BS t1'' a'' t2'' => mk_BN (inter t1 t1'') (inter t2 t2'')) ∧
∀t1 a t2 t.
inter (BS t1 a t2) t =
case t of
LN => LN
| LS a' => LS a
| BN t1' t2' => mk_BN (inter t1 t1') (inter t2 t2')
| BS t1'' a'³' t2'' => mk_BS (inter t1 t1'') a (inter t2 t2'')
[inter_eq_def] Definition
⊢ (∀t. isEmpty (inter_eq LN t)) ∧
(∀a t.
inter_eq (LS a) t =
case t of
LN => LN
| LS b => if a = b then LS a else LN
| BN t1 t2 => LN
| BS t1' b' t2' => if a = b' then LS a else LN) ∧
(∀t1 t2 t.
inter_eq (BN t1 t2) t =
case t of
LN => LN
| LS a => LN
| BN t1' t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2')
| BS t1'' a'' t2'' =>
mk_BN (inter_eq t1 t1'') (inter_eq t2 t2'')) ∧
∀t1 a t2 t.
inter_eq (BS t1 a t2) t =
case t of
LN => LN
| LS a' => if a' = a then LS a else LN
| BN t1' t2' => mk_BN (inter_eq t1 t1') (inter_eq t2 t2')
| BS t1'' a'³' t2'' =>
if a'³' = a then
mk_BS (inter_eq t1 t1'') a (inter_eq t2 t2'')
else mk_BN (inter_eq t1 t1'') (inter_eq t2 t2'')
[list_insert_def] Definition
⊢ (∀t. list_insert [] t = t) ∧
∀n ns t. list_insert (n::ns) t = list_insert ns (insert n () t)
[list_to_num_set_def] Definition
⊢ isEmpty (list_to_num_set []) ∧
∀n ns. list_to_num_set (n::ns) = insert n () (list_to_num_set ns)
[lrnext_primitive_def] Definition
⊢ sptree$lrnext =
WFREC (@R. WF R ∧ ∀n. n ≠ 0 ⇒ R ((n − 1) DIV 2) n)
(λlrnext a. I (if a = 0 then 1 else 2 * lrnext ((a − 1) DIV 2)))
[map_def] Definition
⊢ (∀f. isEmpty (map f LN)) ∧ (∀f a. map f (LS a) = LS (f a)) ∧
(∀f t1 t2. map f (BN t1 t2) = BN (map f t1) (map f t2)) ∧
∀f t1 a t2. map f (BS t1 a t2) = BS (map f t1) (f a) (map f t2)
[mapi0_def] Definition
⊢ (∀f i. isEmpty (mapi0 f i LN)) ∧
(∀f i a. mapi0 f i (LS a) = LS (f i a)) ∧
(∀f i t1 t2.
mapi0 f i (BN t1 t2) =
(let
inc = sptree$lrnext i
in
mk_BN (mapi0 f (i + 2 * inc) t1) (mapi0 f (i + inc) t2))) ∧
∀f i t1 a t2.
mapi0 f i (BS t1 a t2) =
(let
inc = sptree$lrnext i
in
mk_BS (mapi0 f (i + 2 * inc) t1) (f i a)
(mapi0 f (i + inc) t2))
[mapi_def] Definition
⊢ ∀f pt. mapi f pt = mapi0 f 0 pt
[mk_wf_def] Definition
⊢ isEmpty (mk_wf LN) ∧ (∀x. mk_wf (LS x) = LS x) ∧
(∀t1 t2. mk_wf (BN t1 t2) = mk_BN (mk_wf t1) (mk_wf t2)) ∧
∀t1 x t2. mk_wf (BS t1 x t2) = mk_BS (mk_wf t1) x (mk_wf t2)
[size_def] Definition
⊢ size LN = 0 ∧ (∀a. size (LS a) = 1) ∧
(∀t1 t2. size (BN t1 t2) = size t1 + size t2) ∧
∀t1 a t2. size (BS t1 a t2) = size t1 + size t2 + 1
[spt_TY_DEF] Definition
⊢ ∃rep.
TYPE_DEFINITION
(λa0'.
∀ $var$('spt').
(∀a0'.
a0' =
ind_type$CONSTR 0 ARB (λn. ind_type$BOTTOM) ∨
(∃a.
a0' =
(λa.
ind_type$CONSTR (SUC 0) a
(λn. ind_type$BOTTOM)) a) ∨
(∃a0 a1.
a0' =
(λa0 a1.
ind_type$CONSTR (SUC (SUC 0)) ARB
(ind_type$FCONS a0
(ind_type$FCONS a1
(λn. ind_type$BOTTOM)))) a0
a1 ∧ $var$('spt') a0 ∧ $var$('spt') a1) ∨
(∃a0 a1 a2.
a0' =
(λa0 a1 a2.
ind_type$CONSTR (SUC (SUC (SUC 0)))
a1
(ind_type$FCONS a0
(ind_type$FCONS a2
(λn. ind_type$BOTTOM)))) a0
a1 a2 ∧ $var$('spt') a0 ∧
$var$('spt') a2) ⇒
$var$('spt') a0') ⇒
$var$('spt') a0') rep
[spt_case_def] Definition
⊢ (∀v f f1 f2. spt_CASE LN v f f1 f2 = v) ∧
(∀a v f f1 f2. spt_CASE (LS a) v f f1 f2 = f a) ∧
(∀a0 a1 v f f1 f2. spt_CASE (BN a0 a1) v f f1 f2 = f1 a0 a1) ∧
∀a0 a1 a2 v f f1 f2. spt_CASE (BS a0 a1 a2) v f f1 f2 = f2 a0 a1 a2
[spt_center_primitive_def] Definition
⊢ spt_center =
WFREC (@R. WF R)
(λspt_center a.
case a of
LN => I NONE
| LS x => I (SOME x)
| BN v7 v8 => I NONE
| BS t1 x' t2 => I (SOME x'))
[spt_centers_def] Definition
⊢ (∀i. spt_centers i [] = []) ∧
∀i x xs.
spt_centers i (x::xs) =
(case spt_center x of NONE => [] | SOME y => [(i,y)]) ⧺
spt_centers (SUC i) xs
[spt_fold_def] Definition
⊢ (∀f acc. spt_fold f acc LN = acc) ∧
(∀f acc a. spt_fold f acc (LS a) = f a acc) ∧
(∀f acc t1 t2.
spt_fold f acc (BN t1 t2) = spt_fold f (spt_fold f acc t1) t2) ∧
∀f acc t1 a t2.
spt_fold f acc (BS t1 a t2) =
spt_fold f (f a (spt_fold f acc t1)) t2
[spt_left_def] Definition
⊢ isEmpty (spt_left LN) ∧ (∀x. isEmpty (spt_left (LS x))) ∧
(∀t1 t2. spt_left (BN t1 t2) = t1) ∧
∀t1 x t2. spt_left (BS t1 x t2) = t1
[spt_right_def] Definition
⊢ isEmpty (spt_right LN) ∧ (∀x. isEmpty (spt_right (LS x))) ∧
(∀t1 t2. spt_right (BN t1 t2) = t2) ∧
∀t1 x t2. spt_right (BS t1 x t2) = t2
[spt_size_alt_def] Definition
⊢ spt_size_alt LN = 0 ∧ (∀a. spt_size_alt (LS a) = 1) ∧
(∀t1 t2.
spt_size_alt (BN t1 t2) =
spt_size_alt t1 + spt_size_alt t2 + 1) ∧
∀t1 a t2.
spt_size_alt (BS t1 a t2) =
spt_size_alt t1 + spt_size_alt t2 + 1
[spt_size_def] Definition
⊢ (∀f. spt_size f LN = 0) ∧ (∀f a. spt_size f (LS a) = 1 + f a) ∧
(∀f a0 a1.
spt_size f (BN a0 a1) = 1 + (spt_size f a0 + spt_size f a1)) ∧
∀f a0 a1 a2.
spt_size f (BS a0 a1 a2) =
1 + (spt_size f a0 + (f a1 + spt_size f a2))
[toAList_def] Definition
⊢ toAList = foldi (λk v a. (k,v)::a) 0 []
[toListA_def] Definition
⊢ (∀acc. toListA acc LN = acc) ∧
(∀acc a. toListA acc (LS a) = a::acc) ∧
(∀acc t1 t2. toListA acc (BN t1 t2) = toListA (toListA acc t2) t1) ∧
∀acc t1 a t2.
toListA acc (BS t1 a t2) = toListA (a::toListA acc t2) t1
[toList_def] Definition
⊢ ∀m. toList m = toListA [] m
[toSortedAList_def] Definition
⊢ ∀spt. toSortedAList spt = aux_alist 0 [spt]
[union_def] Definition
⊢ (∀t. union LN t = t) ∧
(∀a t.
union (LS a) t =
case t of
LN => LS a
| LS b => LS a
| BN t1 t2 => BS t1 a t2
| BS t1' v4 t2' => BS t1' a t2') ∧
(∀t1 t2 t.
union (BN t1 t2) t =
case t of
LN => BN t1 t2
| LS a => BS t1 a t2
| BN t1' t2' => BN (union t1 t1') (union t2 t2')
| BS t1'' a'' t2'' => BS (union t1 t1'') a'' (union t2 t2'')) ∧
∀t1 a t2 t.
union (BS t1 a t2) t =
case t of
LN => BS t1 a t2
| LS a' => BS t1 a t2
| BN t1' t2' => BS (union t1 t1') a (union t2 t2')
| BS t1'' a'³' t2'' => BS (union t1 t1'') a (union t2 t2'')
[wf_def] Definition
⊢ (wf LN ⇔ T) ∧ (∀a. wf (LS a) ⇔ T) ∧
(∀t1 t2. wf (BN t1 t2) ⇔ wf t1 ∧ wf t2 ∧ ¬(isEmpty t1 ∧ isEmpty t2)) ∧
∀t1 a t2.
wf (BS t1 a t2) ⇔ wf t1 ∧ wf t2 ∧ ¬(isEmpty t1 ∧ isEmpty t2)
[ADD_1_SUC] Theorem
⊢ N + 1 = SUC N ∧ 1 + N = SUC N
[ALL_DISTINCT_MAP_FST_toAList] Theorem
⊢ ∀t. ALL_DISTINCT (MAP FST (toAList t))
[ALOOKUP_aux_alist] Theorem
⊢ ∀i j.
LENGTH xs > 0 ⇒
ALOOKUP (aux_alist j xs) i =
if i < j then NONE
else
lookup ((i − j) DIV LENGTH xs)
(EL ((i − j) MOD LENGTH xs) xs)
[ALOOKUP_spt_centers] Theorem
⊢ ∀i j.
ALOOKUP (spt_centers j xs) i =
if j ≤ i ∧ i − j < LENGTH xs then spt_center (EL (i − j) xs)
else NONE
[ALOOKUP_toAList] Theorem
⊢ ∀t x. ALOOKUP (toAList t) x = lookup x t
[ALOOKUP_toSortedAList] Theorem
⊢ ALOOKUP (toSortedAList t) k = lookup k t
[DIV_MOD_TIMES_2] Theorem
⊢ ∀n i.
0 < n ⇒
i DIV n =
2 * (i DIV (2 * n)) + (if i MOD (2 * n) < n then 0 else 1) ∧
i MOD n = i MOD (2 * n) − if i MOD (2 * n) < n then 0 else n
[EL_CONS_IF] Theorem
⊢ EL n (x::xs) = if n = 0 then x else EL (PRE n) xs
[FINITE_domain] Theorem
⊢ FINITE (domain t)
[GREATER_EQ_alist_aux] Theorem
⊢ MEM x (aux_alist i xs) ⇒ i ≤ FST x
[IMP_size_LESS_size] Theorem
⊢ ∀x y. subspt x y ∧ domain x ≠ domain y ⇒ size x < size y
[IN_domain] Theorem
⊢ ∀n x t1 t2.
(n ∈ domain LN ⇔ F) ∧ (n ∈ domain (LS x) ⇔ n = 0) ∧
(n ∈ domain (BN t1 t2) ⇔
n ≠ 0 ∧
if EVEN n then (n − 1) DIV 2 ∈ domain t1
else (n − 1) DIV 2 ∈ domain t2) ∧
(n ∈ domain (BS t1 x t2) ⇔
n = 0 ∨
if EVEN n then (n − 1) DIV 2 ∈ domain t1
else (n − 1) DIV 2 ∈ domain t2)
[LESS_spt_centers] Theorem
⊢ ∀xs i. MEM p (spt_centers i xs) ⇒ FST p < i + LENGTH xs
[MAP_foldi] Theorem
⊢ ∀n acc.
MAP f (foldi (λk v a. (k,v)::a) n acc pt) =
foldi (λk v a. f (k,v)::a) n (MAP f acc) pt
[MEM_FST_ALOOKUP_SOME] Theorem
⊢ MEM x xs ⇒ ∃y. ALOOKUP xs (FST x) = SOME y
[MEM_toAList] Theorem
⊢ ∀t k v. MEM (k,v) (toAList t) ⇔ lookup k t = SOME v
[MEM_toList] Theorem
⊢ ∀x t. MEM x (toList t) ⇔ ∃k. lookup k t = SOME x
[MEM_toSortedAList] Theorem
⊢ ∀t k v. MEM (k,v) (toSortedAList t) ⇔ lookup k t = SOME v
[SORTED_MAP_FST_alist_aux] Theorem
⊢ ∀i. SORTED $< (MAP FST (aux_alist i xs))
[SORTED_MAP_FST_toSortedAList] Theorem
⊢ SORTED $< (MAP FST (toSortedAList t))
[SORTED_spt_centers] Theorem
⊢ ∀xs i. SORTED $< (MAP FST (spt_centers i xs))
[alist_insert_REVERSE] Theorem
⊢ ∀xs ys s.
ALL_DISTINCT xs ∧ LENGTH xs = LENGTH ys ⇒
alist_insert (REVERSE xs) (REVERSE ys) s = alist_insert xs ys s
[alist_insert_append] Theorem
⊢ ∀a1 a2 s b1 b2.
LENGTH a1 = LENGTH a2 ⇒
alist_insert (a1 ⧺ b1) (a2 ⧺ b2) s =
alist_insert a1 a2 (alist_insert b1 b2 s)
[alist_insert_def] Theorem
⊢ (∀xs t. alist_insert [] xs t = t) ∧
(∀v6 v5 t. alist_insert (v5::v6) [] t = t) ∧
∀xs x vs v t.
alist_insert (v::vs) (x::xs) t =
insert v x (alist_insert vs xs t)
[alist_insert_ind] Theorem
⊢ ∀P.
(∀xs t. P [] xs t) ∧ (∀v5 v6 t. P (v5::v6) [] t) ∧
(∀v vs x xs t. P vs xs t ⇒ P (v::vs) (x::xs) t) ⇒
∀v v1 v2. P v v1 v2
[alist_insert_pull_insert] Theorem
⊢ ∀xs ys z.
¬MEM x xs ⇒
alist_insert xs ys (insert x y z) =
insert x y (alist_insert xs ys z)
[aux_alist_def] Theorem
⊢ ∀xs i.
aux_alist i xs =
if EVERY (λx. isEmpty x) xs then []
else
spt_centers i xs ⧺
aux_alist (LENGTH xs + i)
(MAP spt_right xs ⧺ MAP spt_left xs)
[aux_alist_ind] Theorem
⊢ ∀P.
(∀i xs.
(¬EVERY (λx. isEmpty x) xs ⇒
P (LENGTH xs + i) (MAP spt_right xs ⧺ MAP spt_left xs)) ⇒
P i xs) ⇒
∀v v1. P v v1
[datatype_spt] Theorem
⊢ DATATYPE (spt LN LS BN BS)
[delete_compute] Theorem
⊢ delete (NUMERAL n) t = delete n t ∧ isEmpty (delete 0 LN) ∧
isEmpty (delete 0 (LS a)) ∧ delete 0 (BN t1 t2) = BN t1 t2 ∧
delete 0 (BS t1 a t2) = BN t1 t2 ∧ isEmpty (delete ZERO LN) ∧
isEmpty (delete ZERO (LS a)) ∧ delete ZERO (BN t1 t2) = BN t1 t2 ∧
delete ZERO (BS t1 a t2) = BN t1 t2 ∧
isEmpty (delete (BIT1 n) LN) ∧ delete (BIT1 n) (LS a) = LS a ∧
delete (BIT1 n) (BN t1 t2) = mk_BN t1 (delete n t2) ∧
delete (BIT1 n) (BS t1 a t2) = mk_BS t1 a (delete n t2) ∧
isEmpty (delete (BIT2 n) LN) ∧ delete (BIT2 n) (LS a) = LS a ∧
delete (BIT2 n) (BN t1 t2) = mk_BN (delete n t1) t2 ∧
delete (BIT2 n) (BS t1 a t2) = mk_BS (delete n t1) a t2
[delete_fail] Theorem
⊢ ∀n t. wf t ⇒ (n ∉ domain t ⇔ delete n t = t)
[delete_mk_wf] Theorem
⊢ ∀x t. delete x (mk_wf t) = mk_wf (delete x t)
[difference_sub] Theorem
⊢ isEmpty (difference a b) ⇒ domain a ⊆ domain b
[domain_FOLDR_delete] Theorem
⊢ ∀ls live. domain (FOLDR delete live ls) = domain live DIFF set ls
[domain_alist_insert] Theorem
⊢ ∀a b locs.
LENGTH a = LENGTH b ⇒
domain (alist_insert a b locs) = domain locs ∪ set a
[domain_delete] Theorem
⊢ domain (delete k t) = domain t DELETE k
[domain_difference] Theorem
⊢ ∀t1 t2. domain (difference t1 t2) = domain t1 DIFF domain t2
[domain_empty] Theorem
⊢ ∀t. wf t ⇒ (isEmpty t ⇔ domain t = ∅)
[domain_eq] Theorem
⊢ ∀t1 t2.
domain t1 = domain t2 ⇔
∀k. lookup k t1 = NONE ⇔ lookup k t2 = NONE
[domain_foldi] Theorem
⊢ domain t = foldi (λk v a. k INSERT a) 0 ∅ t
[domain_fromAList] Theorem
⊢ ∀ls. domain (fromAList ls) = set (MAP FST ls)
[domain_fromList] Theorem
⊢ domain (fromList l) = count (LENGTH l)
[domain_insert] Theorem
⊢ domain (insert k v t) = k INSERT domain t
[domain_inter] Theorem
⊢ domain (inter t1 t2) = domain t1 ∩ domain t2
[domain_list_insert] Theorem
⊢ ∀xs x t. x ∈ domain (list_insert xs t) ⇔ MEM x xs ∨ x ∈ domain t
[domain_list_to_num_set] Theorem
⊢ ∀xs. x ∈ domain (list_to_num_set xs) ⇔ MEM x xs
[domain_lookup] Theorem
⊢ ∀t k. k ∈ domain t ⇔ ∃v. lookup k t = SOME v
[domain_map] Theorem
⊢ ∀s. domain (map f s) = domain s
[domain_mapi] Theorem
⊢ domain (mapi f x) = domain x
[domain_mk_wf] Theorem
⊢ ∀t. domain (mk_wf t) = domain t
[domain_sing] Theorem
⊢ domain (insert k v LN) = {k}
[domain_union] Theorem
⊢ domain (union t1 t2) = domain t1 ∪ domain t2
[foldi_FOLDR_toAList] Theorem
⊢ ∀f a t. foldi f 0 a t = FOLDR (UNCURRY f) a (toAList t)
[fromAList_append] Theorem
⊢ ∀l1 l2. fromAList (l1 ⧺ l2) = union (fromAList l1) (fromAList l2)
[fromAList_def] Theorem
⊢ isEmpty (fromAList []) ∧
∀y xs x. fromAList ((x,y)::xs) = insert x y (fromAList xs)
[fromAList_ind] Theorem
⊢ ∀P. P [] ∧ (∀x y xs. P xs ⇒ P ((x,y)::xs)) ⇒ ∀v. P v
[fromAList_toAList] Theorem
⊢ ∀t. wf t ⇒ fromAList (toAList t) = t
[insert_compute] Theorem
⊢ insert (NUMERAL n) a t = insert n a t ∧ insert 0 a LN = LS a ∧
insert 0 a (LS a') = LS a ∧ insert 0 a (BN t1 t2) = BS t1 a t2 ∧
insert 0 a (BS t1 a' t2) = BS t1 a t2 ∧ insert ZERO a LN = LS a ∧
insert ZERO a (LS a') = LS a ∧
insert ZERO a (BN t1 t2) = BS t1 a t2 ∧
insert ZERO a (BS t1 a' t2) = BS t1 a t2 ∧
insert (BIT1 n) a LN = BN LN (insert n a LN) ∧
insert (BIT1 n) a (LS a') = BS LN a' (insert n a LN) ∧
insert (BIT1 n) a (BN t1 t2) = BN t1 (insert n a t2) ∧
insert (BIT1 n) a (BS t1 a' t2) = BS t1 a' (insert n a t2) ∧
insert (BIT2 n) a LN = BN (insert n a LN) LN ∧
insert (BIT2 n) a (LS a') = BS (insert n a LN) a' LN ∧
insert (BIT2 n) a (BN t1 t2) = BN (insert n a t1) t2 ∧
insert (BIT2 n) a (BS t1 a' t2) = BS (insert n a t1) a' t2
[insert_def] Theorem
⊢ (∀k a.
insert k a LN =
if k = 0 then LS a
else if EVEN k then BN (insert ((k − 1) DIV 2) a LN) LN
else BN LN (insert ((k − 1) DIV 2) a LN)) ∧
(∀k a' a.
insert k a (LS a') =
if k = 0 then LS a
else if EVEN k then BS (insert ((k − 1) DIV 2) a LN) a' LN
else BS LN a' (insert ((k − 1) DIV 2) a LN)) ∧
(∀t2 t1 k a.
insert k a (BN t1 t2) =
if k = 0 then BS t1 a t2
else if EVEN k then BN (insert ((k − 1) DIV 2) a t1) t2
else BN t1 (insert ((k − 1) DIV 2) a t2)) ∧
∀t2 t1 k a' a.
insert k a (BS t1 a' t2) =
if k = 0 then BS t1 a t2
else if EVEN k then BS (insert ((k − 1) DIV 2) a t1) a' t2
else BS t1 a' (insert ((k − 1) DIV 2) a t2)
[insert_ind] Theorem
⊢ ∀P.
(∀k a.
(k ≠ 0 ∧ EVEN k ⇒ P ((k − 1) DIV 2) a LN) ∧
(k ≠ 0 ∧ ¬EVEN k ⇒ P ((k − 1) DIV 2) a LN) ⇒
P k a LN) ∧
(∀k a a'.
(k ≠ 0 ∧ EVEN k ⇒ P ((k − 1) DIV 2) a LN) ∧
(k ≠ 0 ∧ ¬EVEN k ⇒ P ((k − 1) DIV 2) a LN) ⇒
P k a (LS a')) ∧
(∀k a t1 t2.
(k ≠ 0 ∧ EVEN k ⇒ P ((k − 1) DIV 2) a t1) ∧
(k ≠ 0 ∧ ¬EVEN k ⇒ P ((k − 1) DIV 2) a t2) ⇒
P k a (BN t1 t2)) ∧
(∀k a t1 a' t2.
(k ≠ 0 ∧ EVEN k ⇒ P ((k − 1) DIV 2) a t1) ∧
(k ≠ 0 ∧ ¬EVEN k ⇒ P ((k − 1) DIV 2) a t2) ⇒
P k a (BS t1 a' t2)) ⇒
∀v v1 v2. P v v1 v2
[insert_insert] Theorem
⊢ ∀x1 x2 v1 v2 t.
insert x1 v1 (insert x2 v2 t) =
if x1 = x2 then insert x1 v1 t
else insert x2 v2 (insert x1 v1 t)
[insert_mk_wf] Theorem
⊢ ∀x v t. insert x v (mk_wf t) = mk_wf (insert x v t)
[insert_notEmpty] Theorem
⊢ insert k a t ≠ LN
[insert_shadow] Theorem
⊢ ∀t a b c. insert a b (insert a c t) = insert a b t
[insert_swap] Theorem
⊢ ∀t a b c d.
a ≠ c ⇒ insert a b (insert c d t) = insert c d (insert a b t)
[insert_unchanged] Theorem
⊢ ∀t x. lookup x t = SOME y ⇒ insert x y t = t
[insert_union] Theorem
⊢ ∀k v s. insert k v s = union (insert k v LN) s
[inter_LN] Theorem
⊢ ∀t. isEmpty (inter t LN) ∧ isEmpty (inter LN t)
[inter_assoc] Theorem
⊢ ∀t1 t2 t3. inter t1 (inter t2 t3) = inter (inter t1 t2) t3
[inter_eq] Theorem
⊢ ∀t1 t2 t3 t4.
inter t1 t2 = inter t3 t4 ⇔
∀x. lookup x (inter t1 t2) = lookup x (inter t3 t4)
[inter_eq_LN] Theorem
⊢ ∀x y. isEmpty (inter x y) ⇔ DISJOINT (domain x) (domain y)
[inter_mk_wf] Theorem
⊢ ∀t1 t2. inter (mk_wf t1) (mk_wf t2) = mk_wf (inter t1 t2)
[isEmpty_toList] Theorem
⊢ ∀t. wf t ⇒ (isEmpty t ⇔ toList t = [])
[isEmpty_toListA] Theorem
⊢ ∀t acc. wf t ⇒ (isEmpty t ⇔ toListA acc t = acc)
[isEmpty_union] Theorem
⊢ isEmpty (union m1 m2) ⇔ isEmpty m1 ∧ isEmpty m2
[list_size_APPEND] Theorem
⊢ list_size f (xs ⧺ ys) = list_size f xs + list_size f ys
[list_to_num_set_append] Theorem
⊢ ∀l1 l2.
list_to_num_set (l1 ⧺ l2) =
union (list_to_num_set l1) (list_to_num_set l2)
[lookup_0_spt_center] Theorem
⊢ ∀spt. lookup 0 spt = spt_center spt
[lookup_FOLDL_union] Theorem
⊢ lookup k (FOLDL union t ls) =
FOLDL OPTION_CHOICE (lookup k t) (MAP (lookup k) ls)
[lookup_NONE_domain] Theorem
⊢ lookup k t = NONE ⇔ k ∉ domain t
[lookup_alist_insert] Theorem
⊢ ∀x y t z.
LENGTH x = LENGTH y ⇒
lookup z (alist_insert x y t) =
case ALOOKUP (ZIP (x,y)) z of
NONE => lookup z t
| SOME a => SOME a
[lookup_compute] Theorem
⊢ lookup (NUMERAL n) t = lookup n t ∧ lookup 0 LN = NONE ∧
lookup 0 (LS a) = SOME a ∧ lookup 0 (BN t1 t2) = NONE ∧
lookup 0 (BS t1 a t2) = SOME a ∧ lookup ZERO LN = NONE ∧
lookup ZERO (LS a) = SOME a ∧ lookup ZERO (BN t1 t2) = NONE ∧
lookup ZERO (BS t1 a t2) = SOME a ∧ lookup (BIT1 n) LN = NONE ∧
lookup (BIT1 n) (LS a) = NONE ∧
lookup (BIT1 n) (BN t1 t2) = lookup n t2 ∧
lookup (BIT1 n) (BS t1 a t2) = lookup n t2 ∧
lookup (BIT2 n) LN = NONE ∧ lookup (BIT2 n) (LS a) = NONE ∧
lookup (BIT2 n) (BN t1 t2) = lookup n t1 ∧
lookup (BIT2 n) (BS t1 a t2) = lookup n t1
[lookup_def] Theorem
⊢ (∀k. lookup k LN = NONE) ∧
(∀k a. lookup k (LS a) = if k = 0 then SOME a else NONE) ∧
(∀t2 t1 k.
lookup k (BN t1 t2) =
if k = 0 then NONE
else lookup ((k − 1) DIV 2) (if EVEN k then t1 else t2)) ∧
∀t2 t1 k a.
lookup k (BS t1 a t2) =
if k = 0 then SOME a
else lookup ((k − 1) DIV 2) (if EVEN k then t1 else t2)
[lookup_delete] Theorem
⊢ ∀t k1 k2.
lookup k1 (delete k2 t) = if k1 = k2 then NONE else lookup k1 t
[lookup_difference] Theorem
⊢ ∀m1 m2 k.
lookup k (difference m1 m2) =
if lookup k m2 = NONE then lookup k m1 else NONE
[lookup_filter_v] Theorem
⊢ ∀k t f.
lookup k (filter_v f t) =
case lookup k t of
NONE => NONE
| SOME v => if f v then SOME v else NONE
[lookup_fromAList] Theorem
⊢ ∀ls x. lookup x (fromAList ls) = ALOOKUP ls x
[lookup_fromAList_toAList] Theorem
⊢ ∀t x. lookup x (fromAList (toAList t)) = lookup x t
[lookup_fromList] Theorem
⊢ lookup n (fromList l) =
if n < LENGTH l then SOME (EL n l) else NONE
[lookup_fromList_outside] Theorem
⊢ ∀k. LENGTH args ≤ k ⇒ lookup k (fromList args) = NONE
[lookup_ind] Theorem
⊢ ∀P.
(∀k. P k LN) ∧ (∀k a. P k (LS a)) ∧
(∀k t1 t2.
(k ≠ 0 ⇒ P ((k − 1) DIV 2) (if EVEN k then t1 else t2)) ⇒
P k (BN t1 t2)) ∧
(∀k t1 a t2.
(k ≠ 0 ⇒ P ((k − 1) DIV 2) (if EVEN k then t1 else t2)) ⇒
P k (BS t1 a t2)) ⇒
∀v v1. P v v1
[lookup_insert] Theorem
⊢ ∀k2 v t k1.
lookup k1 (insert k2 v t) =
if k1 = k2 then SOME v else lookup k1 t
[lookup_insert1] Theorem
⊢ ∀k a t. lookup k (insert k a t) = SOME a
[lookup_inter] Theorem
⊢ ∀m1 m2 k.
lookup k (inter m1 m2) =
case (lookup k m1,lookup k m2) of
(NONE,v4) => NONE
| (SOME v,NONE) => NONE
| (SOME v,SOME w) => SOME v
[lookup_inter_EQ] Theorem
⊢ (lookup x (inter t1 t2) = SOME y ⇔
lookup x t1 = SOME y ∧ lookup x t2 ≠ NONE) ∧
(lookup x (inter t1 t2) = NONE ⇔
lookup x t1 = NONE ∨ lookup x t2 = NONE)
[lookup_inter_alt] Theorem
⊢ lookup x (inter t1 t2) =
if x ∈ domain t2 then lookup x t1 else NONE
[lookup_inter_assoc] Theorem
⊢ lookup x (inter t1 (inter t2 t3)) =
lookup x (inter (inter t1 t2) t3)
[lookup_inter_eq] Theorem
⊢ ∀m1 m2 k.
lookup k (inter_eq m1 m2) =
case lookup k m1 of
NONE => NONE
| SOME v => if lookup k m2 = SOME v then SOME v else NONE
[lookup_list_to_num_set] Theorem
⊢ ∀xs.
lookup x (list_to_num_set xs) =
if MEM x xs then SOME () else NONE
[lookup_map] Theorem
⊢ ∀s x. lookup x (map f s) = OPTION_MAP f (lookup x s)
[lookup_map_K] Theorem
⊢ ∀t n.
lookup n (map (K x) t) = if n ∈ domain t then SOME x else NONE
[lookup_mapi] Theorem
⊢ lookup k (mapi f pt) = OPTION_MAP (f k) (lookup k pt)
[lookup_mapi0] Theorem
⊢ ∀pt i k.
lookup k (mapi0 f i pt) =
case lookup k pt of
NONE => NONE
| SOME v => SOME (f (spt_acc i k) v)
[lookup_mk_BN] Theorem
⊢ lookup i (mk_BN t1 t2) =
if i = 0 then NONE
else lookup ((i − 1) DIV 2) (if EVEN i then t1 else t2)
[lookup_mk_wf] Theorem
⊢ ∀x t. lookup x (mk_wf t) = lookup x t
[lookup_spt_left] Theorem
⊢ lookup i (spt_left spt) = lookup (i * 2 + 2) spt
[lookup_spt_right] Theorem
⊢ lookup i (spt_right spt) = lookup (i * 2 + 1) spt
[lookup_union] Theorem
⊢ ∀m1 m2 k.
lookup k (union m1 m2) =
case lookup k m1 of NONE => lookup k m2 | SOME v => SOME v
[lrnext_def] Theorem
⊢ ∀n.
sptree$lrnext n =
if n = 0 then 1 else 2 * sptree$lrnext ((n − 1) DIV 2)
[lrnext_ind] Theorem
⊢ ∀P. (∀n. (n ≠ 0 ⇒ P ((n − 1) DIV 2)) ⇒ P n) ⇒ ∀v. P v
[lrnext_thm] Theorem
⊢ (∀a. sptree$lrnext 0 = 1) ∧
(∀n a. sptree$lrnext (NUMERAL n) = sptree$lrnext n) ∧
sptree$lrnext ZERO = 1 ∧
(∀n. sptree$lrnext (BIT1 n) = 2 * sptree$lrnext n) ∧
∀n. sptree$lrnext (BIT2 n) = 2 * sptree$lrnext n
[map_LN] Theorem
⊢ ∀t. isEmpty (map f t) ⇔ isEmpty t
[map_fromAList] Theorem
⊢ map f (fromAList ls) = fromAList (MAP (λ(k,v). (k,f v)) ls)
[map_insert] Theorem
⊢ ∀f x y z. map f (insert x y z) = insert x (f y) (map f z)
[map_map_K] Theorem
⊢ ∀t. map (K a) (map f t) = map (K a) t
[map_map_o] Theorem
⊢ ∀t f g. map f (map g t) = map (f ∘ g) t
[map_union] Theorem
⊢ ∀t1 t2. map f (union t1 t2) = union (map f t1) (map f t2)
[mapi_Alist] Theorem
⊢ mapi f pt =
fromAList (MAP (λkv. (FST kv,f (FST kv) (SND kv))) (toAList pt))
[mk_BN_def] Theorem
⊢ isEmpty (mk_BN LN LN) ∧ mk_BN LN (LS v14) = BN LN (LS v14) ∧
mk_BN LN (BN v15 v16) = BN LN (BN v15 v16) ∧
mk_BN LN (BS v17 v18 v19) = BN LN (BS v17 v18 v19) ∧
mk_BN (LS v2) t2 = BN (LS v2) t2 ∧
mk_BN (BN v3 v4) t2 = BN (BN v3 v4) t2 ∧
mk_BN (BS v5 v6 v7) t2 = BN (BS v5 v6 v7) t2
[mk_BN_ind] Theorem
⊢ ∀P.
P LN LN ∧ (∀v14. P LN (LS v14)) ∧
(∀v15 v16. P LN (BN v15 v16)) ∧
(∀v17 v18 v19. P LN (BS v17 v18 v19)) ∧
(∀v2 t2. P (LS v2) t2) ∧ (∀v3 v4 t2. P (BN v3 v4) t2) ∧
(∀v5 v6 v7 t2. P (BS v5 v6 v7) t2) ⇒
∀v v1. P v v1
[mk_BS_def] Theorem
⊢ mk_BS LN x LN = LS x ∧ mk_BS (LS v16) x LN = BS (LS v16) x LN ∧
mk_BS (BN v17 v18) x LN = BS (BN v17 v18) x LN ∧
mk_BS (BS v19 v20 v21) x LN = BS (BS v19 v20 v21) x LN ∧
mk_BS t1 x (LS v4) = BS t1 x (LS v4) ∧
mk_BS t1 x (BN v5 v6) = BS t1 x (BN v5 v6) ∧
mk_BS t1 x (BS v7 v8 v9) = BS t1 x (BS v7 v8 v9)
[mk_BS_ind] Theorem
⊢ ∀P.
(∀x. P LN x LN) ∧ (∀v16 x. P (LS v16) x LN) ∧
(∀v17 v18 x. P (BN v17 v18) x LN) ∧
(∀v19 v20 v21 x. P (BS v19 v20 v21) x LN) ∧
(∀t1 x v4. P t1 x (LS v4)) ∧ (∀t1 x v5 v6. P t1 x (BN v5 v6)) ∧
(∀t1 x v7 v8 v9. P t1 x (BS v7 v8 v9)) ⇒
∀v v1 v2. P v v1 v2
[mk_wf_eq] Theorem
⊢ ∀t1 t2. mk_wf t1 = mk_wf t2 ⇔ ∀x. lookup x t1 = lookup x t2
[num_set_domain_eq] Theorem
⊢ ∀t1 t2. wf t1 ∧ wf t2 ⇒ (domain t1 = domain t2 ⇔ t1 = t2)
[set_foldi_keys] Theorem
⊢ ∀t a i.
foldi (λk v a. k INSERT a) i a t =
a ∪ IMAGE (λn. i + sptree$lrnext i * n) (domain t)
[size_delete] Theorem
⊢ ∀n t.
size (delete n t) =
if lookup n t = NONE then size t else size t − 1
[size_diff_less] Theorem
⊢ ∀x y z t.
domain z ⊆ domain y ∧ t ∈ domain y ∧ t ∉ domain z ∧
t ∈ domain x ⇒
size (difference x y) < size (difference x z)
[size_domain] Theorem
⊢ ∀t. size t = CARD (domain t)
[size_insert] Theorem
⊢ ∀k v m.
size (insert k v m) =
if k ∈ domain m then size m else size m + 1
[spt_11] Theorem
⊢ (∀a a'. LS a = LS a' ⇔ a = a') ∧
(∀a0 a1 a0' a1'. BN a0 a1 = BN a0' a1' ⇔ a0 = a0' ∧ a1 = a1') ∧
∀a0 a1 a2 a0' a1' a2'.
BS a0 a1 a2 = BS a0' a1' a2' ⇔ a0 = a0' ∧ a1 = a1' ∧ a2 = a2'
[spt_Axiom] Theorem
⊢ ∀f0 f1 f2 f3.
∃fn.
fn LN = f0 ∧ (∀a. fn (LS a) = f1 a) ∧
(∀a0 a1. fn (BN a0 a1) = f2 a0 a1 (fn a0) (fn a1)) ∧
∀a0 a1 a2. fn (BS a0 a1 a2) = f3 a1 a0 a2 (fn a0) (fn a2)
[spt_acc_0] Theorem
⊢ ∀k. spt_acc 0 k = k
[spt_acc_compute] Theorem
⊢ (∀i. spt_acc i 0 = i) ∧
(∀k i.
spt_acc i (NUMERAL (BIT1 k)) =
spt_acc
(i +
if EVEN (NUMERAL (BIT1 k)) then 2 * sptree$lrnext i
else sptree$lrnext i) ((NUMERAL (BIT1 k) − 1) DIV 2)) ∧
∀k i.
spt_acc i (NUMERAL (BIT2 k)) =
spt_acc
(i +
if EVEN (NUMERAL (BIT2 k)) then 2 * sptree$lrnext i
else sptree$lrnext i) (NUMERAL (BIT1 k) DIV 2)
[spt_acc_def] Theorem
⊢ (∀i. spt_acc i 0 = i) ∧
∀k i.
spt_acc i (SUC k) =
spt_acc
(i +
if EVEN (SUC k) then 2 * sptree$lrnext i
else sptree$lrnext i) (k DIV 2)
[spt_acc_eqn] Theorem
⊢ ∀k i. spt_acc i k = sptree$lrnext i * k + i
[spt_acc_ind] Theorem
⊢ ∀P.
(∀i. P i 0) ∧
(∀i k.
P
(i +
if EVEN (SUC k) then 2 * sptree$lrnext i
else sptree$lrnext i) (k DIV 2) ⇒
P i (SUC k)) ⇒
∀v v1. P v v1
[spt_acc_thm] Theorem
⊢ spt_acc i k =
if k = 0 then i
else
spt_acc
(i + if EVEN k then 2 * sptree$lrnext i else sptree$lrnext i)
((k − 1) DIV 2)
[spt_case_cong] Theorem
⊢ ∀M M' v f f1 f2.
M = M' ∧ (isEmpty M' ⇒ v = v') ∧ (∀a. M' = LS a ⇒ f a = f' a) ∧
(∀a0 a1. M' = BN a0 a1 ⇒ f1 a0 a1 = f1' a0 a1) ∧
(∀a0 a1 a2. M' = BS a0 a1 a2 ⇒ f2 a0 a1 a2 = f2' a0 a1 a2) ⇒
spt_CASE M v f f1 f2 = spt_CASE M' v' f' f1' f2'
[spt_case_eq] Theorem
⊢ spt_CASE x v f f1 f2 = v' ⇔
isEmpty x ∧ v = v' ∨ (∃a. x = LS a ∧ f a = v') ∨
(∃s s0. x = BN s s0 ∧ f1 s s0 = v') ∨
∃s a s0. x = BS s a s0 ∧ f2 s a s0 = v'
[spt_center_def] Theorem
⊢ spt_center (LS x) = SOME x ∧ spt_center (BS t1 x t2) = SOME x ∧
spt_center LN = NONE ∧ spt_center (BN v1 v2) = NONE
[spt_center_ind] Theorem
⊢ ∀P.
(∀x. P (LS x)) ∧ (∀t1 x t2. P (BS t1 x t2)) ∧ P LN ∧
(∀v1 v2. P (BN v1 v2)) ⇒
∀v. P v
[spt_centers_add_lemma] Theorem
⊢ ∀xs i j.
MAP (λ(j,v). (i + j,v)) (spt_centers j xs) =
spt_centers (i + j) xs
[spt_centers_eq_map] Theorem
⊢ ∀xs i.
spt_centers i xs =
MAP THE
(FILTER (λx. x ≠ NONE)
(MAPi
(λj t.
case spt_center t of
NONE => NONE
| SOME x => SOME (i + j,x)) xs))
[spt_distinct] Theorem
⊢ (∀a. LN ≠ LS a) ∧ (∀a1 a0. LN ≠ BN a0 a1) ∧
(∀a2 a1 a0. LN ≠ BS a0 a1 a2) ∧ (∀a1 a0 a. LS a ≠ BN a0 a1) ∧
(∀a2 a1 a0 a. LS a ≠ BS a0 a1 a2) ∧
∀a2 a1' a1 a0' a0. BN a0 a1 ≠ BS a0' a1' a2
[spt_eq_thm] Theorem
⊢ ∀t1 t2. wf t1 ∧ wf t2 ⇒ (t1 = t2 ⇔ ∀n. lookup n t1 = lookup n t2)
[spt_induction] Theorem
⊢ ∀P.
P LN ∧ (∀a. P (LS a)) ∧ (∀s s0. P s ∧ P s0 ⇒ P (BN s s0)) ∧
(∀s s0. P s ∧ P s0 ⇒ ∀a. P (BS s a s0)) ⇒
∀s. P s
[spt_nchotomy] Theorem
⊢ ∀ss.
isEmpty ss ∨ (∃a. ss = LS a) ∨ (∃s s0. ss = BN s s0) ∨
∃s a s0. ss = BS s a s0
[subspt_FOLDL_union] Theorem
⊢ ∀ls t. subspt t (FOLDL union t ls)
[subspt_LN] Theorem
⊢ (subspt LN sp ⇔ T) ∧ (subspt sp LN ⇔ domain sp = ∅)
[subspt_def] Theorem
⊢ ∀sp1 sp2.
subspt sp1 sp2 ⇔
∀k.
k ∈ domain sp1 ⇒
k ∈ domain sp2 ∧ lookup k sp2 = lookup k sp1
[subspt_domain] Theorem
⊢ ∀t1 t2. subspt t1 t2 ⇔ domain t1 ⊆ domain t2
[subspt_eq] Theorem
⊢ (∀t. subspt LN t ⇔ T) ∧
(∀x t. subspt (LS x) t ⇔ spt_center t = SOME x) ∧
(∀t1 t2 t.
subspt (BN t1 t2) t ⇔
subspt t1 (spt_left t) ∧ subspt t2 (spt_right t)) ∧
∀t1 x t2 t.
subspt (BS t1 x t2) t ⇔
spt_center t = SOME x ∧ subspt t1 (spt_left t) ∧
subspt t2 (spt_right t)
[subspt_lookup] Theorem
⊢ ∀t1 t2.
subspt t1 t2 ⇔
∀x y. lookup x t1 = SOME y ⇒ lookup x t2 = SOME y
[subspt_refl] Theorem
⊢ subspt sp sp
[subspt_trans] Theorem
⊢ subspt sp1 sp2 ∧ subspt sp2 sp3 ⇒ subspt sp1 sp3
[subspt_union] Theorem
⊢ subspt s (union s t)
[sum_spt_size_alt_lemma] Theorem
⊢ let
mksum f = SUM (MAP (spt_size_alt ∘ f) xs) ;
tsum = mksum spt_left + mksum spt_right
in
tsum ≤ mksum I ∧
(EXISTS ($~ ∘ (λx. isEmpty x)) xs ⇒ tsum < mksum I)
[sum_spt_size_less] Theorem
⊢ EXISTS ($~ ∘ (λx. isEmpty x)) xs ⇒
SUM (MAP (spt_size_alt ∘ spt_left) xs) +
SUM (MAP (spt_size_alt ∘ spt_right) xs) < SUM (MAP spt_size_alt xs)
[toListA_append] Theorem
⊢ ∀t acc. toListA acc t = toListA [] t ⧺ acc
[toList_map] Theorem
⊢ ∀s. toList (map f s) = MAP f (toList s)
[union_LN] Theorem
⊢ ∀t. union t LN = t ∧ union LN t = t
[union_assoc] Theorem
⊢ ∀t1 t2 t3. union t1 (union t2 t3) = union (union t1 t2) t3
[union_insert_LN] Theorem
⊢ ∀x y t2. union (insert x y LN) t2 = insert x y t2
[union_mk_wf] Theorem
⊢ ∀t1 t2. union (mk_wf t1) (mk_wf t2) = mk_wf (union t1 t2)
[union_num_set_sym] Theorem
⊢ ∀t1 t2. union t1 t2 = union t2 t1
[wf_LN] Theorem
⊢ wf LN
[wf_delete] Theorem
⊢ ∀t k. wf t ⇒ wf (delete k t)
[wf_difference] Theorem
⊢ ∀t1 t2. wf t1 ∧ wf t2 ⇒ wf (difference t1 t2)
[wf_filter_v] Theorem
⊢ ∀t f. wf t ⇒ wf (filter_v f t)
[wf_fromAList] Theorem
⊢ ∀ls. wf (fromAList ls)
[wf_insert] Theorem
⊢ ∀k a t. wf t ⇒ wf (insert k a t)
[wf_inter] Theorem
⊢ ∀m1 m2. wf (inter m1 m2)
[wf_map] Theorem
⊢ ∀t f. wf (map f t) ⇔ wf t
[wf_mapi] Theorem
⊢ wf (mapi f pt)
[wf_mk_BN] Theorem
⊢ wf t1 ∧ wf t2 ⇒ wf (mk_BN t1 t2)
[wf_mk_BS] Theorem
⊢ wf t1 ∧ wf t2 ⇒ wf (mk_BS t1 a t2)
[wf_mk_id] Theorem
⊢ ∀t. wf t ⇒ mk_wf t = t
[wf_mk_wf] Theorem
⊢ ∀t. wf (mk_wf t)
[wf_union] Theorem
⊢ ∀m1 m2. wf m1 ∧ wf m2 ⇒ wf (union m1 m2)
*)
end
HOL 4, Kananaskis-13