Definitions
|- (!a ac. BL_ACCUM a ac nbl = onebl a ac nbl) /\
(!a ac bl. BL_ACCUM a ac (zerbl bl) = onebl a ac bl) /\
!a ac r rft bl.
BL_ACCUM a ac (onebl r rft bl) = zerbl (BL_ACCUM a (node ac r rft) bl)
|- !a bl. BL_CONS a bl = BL_ACCUM a nt bl
|- !cmp x s. LESS_ALL cmp x s <=> !y. y IN s ==> (apto cmp x y = LESS)
|- (!cmp. OL cmp [] <=> T) /\
!cmp a l.
OL cmp (a::l) <=> OL cmp l /\ !p. MEM p l ==> (apto cmp a p = LESS)
|- (!cmp. OL_bt cmp nt <=> T) /\
!cmp l x r.
OL_bt cmp (node l x r) <=> OL_bt_ub cmp l x /\ OL_bt_lb cmp x r
|- (!cmp lb. OL_bt_lb cmp lb nt <=> T) /\
!cmp lb l x r.
OL_bt_lb cmp lb (node l x r) <=>
OL_bt_lb_ub cmp lb l x /\ OL_bt_lb cmp x r
|- (!cmp lb ub. OL_bt_lb_ub cmp lb nt ub <=> (apto cmp lb ub = LESS)) /\
!cmp lb l x r ub.
OL_bt_lb_ub cmp lb (node l x r) ub <=>
OL_bt_lb_ub cmp lb l x /\ OL_bt_lb_ub cmp x r ub
|- (!cmp ub. OL_bt_ub cmp nt ub <=> T) /\
!cmp l x r ub.
OL_bt_ub cmp (node l x r) ub <=>
OL_bt_ub cmp l x /\ OL_bt_lb_ub cmp x r ub
|- !cmp t u.
OU cmp t u =
{x | x IN t /\ !z. z IN u ==> (apto cmp x z = LESS)} UNION u
|- !cmp s l. OWL cmp s l <=> (s = set l) /\ OL cmp l
|- !cmp s t.
UO cmp s t =
s UNION {y | y IN t /\ !z. z IN s ==> (apto cmp z y = LESS)}
bl_TY_DEF
|- ?rep.
TYPE_DEFINITION
(\a0'.
! $var$('bl').
(!a0'.
(a0' = ind_type$CONSTR 0 (ARB,ARB) (\n. ind_type$BOTTOM)) \/
(?a. (a0' =
(\a.
ind_type$CONSTR (SUC 0) (ARB,ARB)
(ind_type$FCONS a (\n. ind_type$BOTTOM))) a) /\
$var$('bl') a) \/
(?a0 a1 a2.
(a0' =
(\a0 a1 a2.
ind_type$CONSTR (SUC (SUC 0)) (a0,a1)
(ind_type$FCONS a2 (\n. ind_type$BOTTOM))) a0
a1 a2) /\ $var$('bl') a2) ==>
$var$('bl') a0') ==>
$var$('bl') a0') rep
bl_case_def
|- (!v f f1. bl_CASE nbl v f f1 = v) /\
(!a v f f1. bl_CASE (zerbl a) v f f1 = f a) /\
!a0 a1 a2 v f f1. bl_CASE (onebl a0 a1 a2) v f f1 = f1 a0 a1 a2
|- (!ft. bl_rev ft nbl = ft) /\
(!ft b. bl_rev ft (zerbl b) = bl_rev ft b) /\
!ft a f b. bl_rev ft (onebl a f b) = bl_rev (node ft a f) b
bl_size_def
|- (!f. bl_size f nbl = 0) /\
(!f a. bl_size f (zerbl a) = 1 + bl_size f a) /\
!f a0 a1 a2.
bl_size f (onebl a0 a1 a2) =
1 + (f a0 + (bt_size f a1 + bl_size f a2))
|- (!cmp. bl_to_set cmp nbl = {}) /\
(!cmp b. bl_to_set cmp (zerbl b) = bl_to_set cmp b) /\
!cmp x t b.
bl_to_set cmp (onebl x t b) =
OU cmp ({x} UNION {y | y IN ENUMERAL cmp t /\ (apto cmp x y = LESS)})
(bl_to_set cmp b)
bt_TY_DEF
|- ?rep.
TYPE_DEFINITION
(\a0'.
! $var$('bt').
(!a0'.
(a0' = ind_type$CONSTR 0 ARB (\n. ind_type$BOTTOM)) \/
(?a0 a1 a2.
(a0' =
(\a0 a1 a2.
ind_type$CONSTR (SUC 0) a1
(ind_type$FCONS a0
(ind_type$FCONS a2 (\n. ind_type$BOTTOM))))
a0 a1 a2) /\ $var$('bt') a0 /\ $var$('bt') a2) ==>
$var$('bt') a0') ==>
$var$('bt') a0') rep
bt_case_def
|- (!v f. bt_CASE nt v f = v) /\
!a0 a1 a2 v f. bt_CASE (node a0 a1 a2) v f = f a0 a1 a2
|- (!bl. bt_rev nt bl = bl) /\
!lft r rft bl. bt_rev (node lft r rft) bl = bt_rev lft (onebl r rft bl)
bt_size_def
|- (!f. bt_size f nt = 0) /\
!f a0 a1 a2.
bt_size f (node a0 a1 a2) = 1 + (bt_size f a0 + (f a1 + bt_size f a2))
|- !t. bt_to_bl t = bt_rev t nbl
|- (bt_to_list nt = []) /\
!l x r. bt_to_list (node l x r) = bt_to_list l ++ [x] ++ bt_to_list r
|- (!m. bt_to_list_ac nt m = m) /\
!l x r m.
bt_to_list_ac (node l x r) m = bt_to_list_ac l (x::bt_to_list_ac r m)
|- (!cmp. bt_to_ol cmp nt = []) /\
!cmp l x r.
bt_to_ol cmp (node l x r) =
bt_to_ol_ub cmp l x ++ [x] ++ bt_to_ol_lb cmp x r
|- (!cmp m. bt_to_ol_ac cmp nt m = m) /\
!cmp l x r m.
bt_to_ol_ac cmp (node l x r) m =
bt_to_ol_ub_ac cmp l x (x::bt_to_ol_lb_ac cmp x r m)
|- (!cmp lb. bt_to_ol_lb cmp lb nt = []) /\
!cmp lb l x r.
bt_to_ol_lb cmp lb (node l x r) =
if apto cmp lb x = LESS then
bt_to_ol_lb_ub cmp lb l x ++ [x] ++ bt_to_ol_lb cmp x r
else bt_to_ol_lb cmp lb r
|- (!cmp lb m. bt_to_ol_lb_ac cmp lb nt m = m) /\
!cmp lb l x r m.
bt_to_ol_lb_ac cmp lb (node l x r) m =
if apto cmp lb x = LESS then
bt_to_ol_lb_ub_ac cmp lb l x (x::bt_to_ol_lb_ac cmp x r m)
else bt_to_ol_lb_ac cmp lb r m
|- (!cmp lb ub. bt_to_ol_lb_ub cmp lb nt ub = []) /\
!cmp lb l x r ub.
bt_to_ol_lb_ub cmp lb (node l x r) ub =
if apto cmp lb x = LESS then
if apto cmp x ub = LESS then
bt_to_ol_lb_ub cmp lb l x ++ [x] ++ bt_to_ol_lb_ub cmp x r ub
else bt_to_ol_lb_ub cmp lb l ub
else bt_to_ol_lb_ub cmp lb r ub
|- (!cmp lb ub m. bt_to_ol_lb_ub_ac cmp lb nt ub m = m) /\
!cmp lb l x r ub m.
bt_to_ol_lb_ub_ac cmp lb (node l x r) ub m =
if apto cmp lb x = LESS then
if apto cmp x ub = LESS then
bt_to_ol_lb_ub_ac cmp lb l x (x::bt_to_ol_lb_ub_ac cmp x r ub m)
else bt_to_ol_lb_ub_ac cmp lb l ub m
else bt_to_ol_lb_ub_ac cmp lb r ub m
|- (!cmp ub. bt_to_ol_ub cmp nt ub = []) /\
!cmp l x r ub.
bt_to_ol_ub cmp (node l x r) ub =
if apto cmp x ub = LESS then
bt_to_ol_ub cmp l x ++ [x] ++ bt_to_ol_lb_ub cmp x r ub
else bt_to_ol_ub cmp l ub
|- (!cmp ub m. bt_to_ol_ub_ac cmp nt ub m = m) /\
!cmp l x r ub m.
bt_to_ol_ub_ac cmp (node l x r) ub m =
if apto cmp x ub = LESS then
bt_to_ol_ub_ac cmp l x (x::bt_to_ol_lb_ub_ac cmp x r ub m)
else bt_to_ol_ub_ac cmp l ub m
|- (!cmp. ENUMERAL cmp nt = {}) /\
!cmp l x r.
ENUMERAL cmp (node l x r) =
{y | y IN ENUMERAL cmp l /\ (apto cmp y x = LESS)} UNION {x} UNION
{z | z IN ENUMERAL cmp r /\ (apto cmp x z = LESS)}
|- !cmp lb t.
bt_to_set_lb cmp lb t =
{x | x IN ENUMERAL cmp t /\ (apto cmp lb x = LESS)}
|- !cmp lb t ub.
bt_to_set_lb_ub cmp lb t ub =
{x |
x IN ENUMERAL cmp t /\ (apto cmp lb x = LESS) /\
(apto cmp x ub = LESS)}
|- !cmp t ub.
bt_to_set_ub cmp t ub =
{x | x IN ENUMERAL cmp t /\ (apto cmp x ub = LESS)}
|- (!cmp. incr_sbuild cmp [] = []) /\
!cmp x l.
incr_sbuild cmp (x::l) = incr_smerge cmp [x] (incr_sbuild cmp l)
|- !cmp l. incr_ssort cmp l = smerge_out cmp [] (incr_sbuild cmp l)
|- (list_to_bl [] = nbl) /\
!a l. list_to_bl (a::l) = BL_CONS a (list_to_bl l)
|- !l. list_to_bt l = bl_to_bt (list_to_bl l)
lol_set_primitive
|- lol_set =
WFREC
(@R. WF R /\ (!lol. R lol (NONE::lol)) /\ !m lol. R lol (SOME m::lol))
(\lol_set a.
case a of
[] => I {}
| NONE::lol => I (lol_set lol)
| SOME m::lol => I (set m UNION lol_set lol))
Theorems
|- !cmp sl. OU cmp {} sl = sl
|- !cmp l. set l = ENUMERAL cmp (list_to_bt (incr_ssort cmp l))
|- (!cmp y. y IN ENUMERAL cmp nt <=> F) /\
!cmp l x r y.
y IN ENUMERAL cmp (node l x r) <=>
y IN ENUMERAL cmp l /\ (apto cmp y x = LESS) \/ (y = x) \/
y IN ENUMERAL cmp r /\ (apto cmp x y = LESS)
|- !cmp x l y r.
x IN ENUMERAL cmp (node l y r) <=>
case apto cmp x y of
LESS => x IN ENUMERAL cmp l
| EQUAL => T
| GREATER => x IN ENUMERAL cmp r
|- !cmp x u v.
LESS_ALL cmp x (OU cmp u v) <=> LESS_ALL cmp x u /\ LESS_ALL cmp x v
|- !cmp a s t.
LESS_ALL cmp a s /\ LESS_ALL cmp a t ==>
(OU cmp (UO cmp {a} s) t = a INSERT OU cmp s t)
|- !cmp a s. LESS_ALL cmp a s ==> (UO cmp {a} s = a INSERT s)
|- !cmp x y s.
(!z. z IN UO cmp {x} s ==> (apto cmp y z = LESS)) <=>
(apto cmp y x = LESS)
|- !cmp y. y IN ENUMERAL cmp nt <=> F
|- !cmp l.
OL cmp l ==>
!m. OL cmp m ==>
OL cmp (sdiff cmp l m) /\ (set (sdiff cmp l m) = set l DIFF set m)
|- !cmp l. OL cmp l ==> (set l = ENUMERAL cmp (list_to_bt l))
|- !cmp l.
OL cmp l ==>
!m. OL cmp m ==>
OL cmp (sinter cmp l m) /\
(set (sinter cmp l m) = set l INTER set m)
|- !cmp l.
OL cmp l ==>
!m. OL cmp m ==>
OL cmp (smerge cmp l m) /\
(set (smerge cmp l m) = set l UNION set m)
|- !cmp t. OL cmp (bt_to_ol cmp t)
|- !cmp t lb. OL cmp (bt_to_ol_lb cmp lb t)
|- !cmp t lb ub. OL cmp (bt_to_ol_lb_ub cmp lb t ub)
|- !cmp t ub. OL cmp (bt_to_ol_ub cmp t ub)
|- (!cmp. OL_sublists cmp [] <=> T) /\
(!lol cmp. OL_sublists cmp (NONE::lol) <=> OL_sublists cmp lol) /\
!m lol cmp.
OL_sublists cmp (SOME m::lol) <=> OL cmp m /\ OL_sublists cmp lol
|- !P. (!cmp. P cmp []) /\ (!cmp lol. P cmp lol ==> P cmp (NONE::lol)) /\
(!cmp m lol. P cmp lol ==> P cmp (SOME m::lol)) ==>
!v v1. P v v1
|- !cmp a b c. OU cmp a (OU cmp b c) = OU cmp (OU cmp a b) c
|- !cmp t. OU cmp t {} = t
|- !cmp s l t m.
OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s DIFF t) (sdiff cmp l m)
|- !cmp s l t m.
OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s INTER t) (sinter cmp l m)
|- !cmp s l t m.
OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s UNION t) (smerge cmp l m)
|- !cmp t. OWL cmp (ENUMERAL cmp t) (bt_to_ol cmp t)
|- !cmp t.
bt_to_ol cmp t =
if OL_bt cmp t then bt_to_list_ac t [] else bt_to_ol_ac cmp t []
bl_11
|- (!a a'. (zerbl a = zerbl a') <=> (a = a')) /\
!a0 a1 a2 a0' a1' a2'.
(onebl a0 a1 a2 = onebl a0' a1' a2') <=>
(a0 = a0') /\ (a1 = a1') /\ (a2 = a2')
bl_Axiom
|- !f0 f1 f2. ?fn.
(fn nbl = f0) /\ (!a. fn (zerbl a) = f1 a (fn a)) /\
!a0 a1 a2. fn (onebl a0 a1 a2) = f2 a0 a1 a2 (fn a2)
bl_case_cong
|- !M M' v f f1.
(M = M') /\ ((M' = nbl) ==> (v = v')) /\
(!a. (M' = zerbl a) ==> (f a = f' a)) /\
(!a0 a1 a2. (M' = onebl a0 a1 a2) ==> (f1 a0 a1 a2 = f1' a0 a1 a2)) ==>
(bl_CASE M v f f1 = bl_CASE M' v' f' f1')
bl_case_eq
|- (bl_CASE x v f f1 = v') <=>
(x = nbl) /\ (v = v') \/ (?b. (x = zerbl b) /\ (f b = v')) \/
?a b0 b. (x = onebl a b0 b) /\ (f1 a b0 b = v')
bl_distinct
|- (!a. nbl <> zerbl a) /\ (!a2 a1 a0. nbl <> onebl a0 a1 a2) /\
!a2 a1 a0 a. zerbl a <> onebl a0 a1 a2
bl_induction
|- !P. P nbl /\ (!b. P b ==> P (zerbl b)) /\
(!b. P b ==> !b0 a. P (onebl a b0 b)) ==>
!b. P b
bl_nchotomy
|- !bb. (bb = nbl) \/ (?b. bb = zerbl b) \/ ?a b0 b. bb = onebl a b0 b
bt_11
|- !a0 a1 a2 a0' a1' a2'.
(node a0 a1 a2 = node a0' a1' a2') <=>
(a0 = a0') /\ (a1 = a1') /\ (a2 = a2')
bt_Axiom
|- !f0 f1. ?fn.
(fn nt = f0) /\
!a0 a1 a2. fn (node a0 a1 a2) = f1 a1 a0 a2 (fn a0) (fn a2)
bt_case_cong
|- !M M' v f.
(M = M') /\ ((M' = nt) ==> (v = v')) /\
(!a0 a1 a2. (M' = node a0 a1 a2) ==> (f a0 a1 a2 = f' a0 a1 a2)) ==>
(bt_CASE M v f = bt_CASE M' v' f')
bt_case_eq
|- (bt_CASE x v f = v') <=>
(x = nt) /\ (v = v') \/ ?b a b0. (x = node b a b0) /\ (f b a b0 = v')
bt_distinct
|- !a2 a1 a0. nt <> node a0 a1 a2
bt_induction
|- !P. P nt /\ (!b b0. P b /\ P b0 ==> !a. P (node b a b0)) ==> !b. P b
bt_nchotomy
|- !bb. (bb = nt) \/ ?b a b0. bb = node b a b0
|- !t. bt_to_list t = bt_to_list_ac t []
|- !cmp l. OL cmp l ==> (bt_to_ol cmp (list_to_bt l) = l)
datatype_bl
|- DATATYPE (bl nbl zerbl onebl)
datatype_bt
|- DATATYPE (bt nt node)
|- (!l cmp. incr_smerge cmp l [] = [SOME l]) /\
(!lol l cmp. incr_smerge cmp l (NONE::lol) = SOME l::lol) /\
!m lol l cmp.
incr_smerge cmp l (SOME m::lol) =
NONE::incr_smerge cmp (smerge cmp l m) lol
|- !cmp lol l.
OL_sublists cmp lol /\ OL cmp l ==>
OL_sublists cmp (incr_smerge cmp l lol)
|- !P. (!cmp l. P cmp l []) /\ (!cmp l lol. P cmp l (NONE::lol)) /\
(!cmp l m lol. P cmp (smerge cmp l m) lol ==> P cmp l (SOME m::lol)) ==>
!v v1 v2. P v v1 v2
|- (lol_set [] = {}) /\ (!lol. lol_set (NONE::lol) = lol_set lol) /\
!m lol. lol_set (SOME m::lol) = set m UNION lol_set lol
|- !P. P [] /\ (!lol. P lol ==> P (NONE::lol)) /\
(!m lol. P lol ==> P (SOME m::lol)) ==>
!v. P v
|- !cmp t. ENUMERAL cmp t = set (bt_to_ol cmp t)
|- (!cmp. sdiff cmp [] [] = []) /\
(!x l cmp. sdiff cmp (x::l) [] = x::l) /\
(!y m cmp. sdiff cmp [] (y::m) = []) /\
!y x m l cmp.
sdiff cmp (x::l) (y::m) =
case apto cmp x y of
LESS => x::sdiff cmp l (y::m)
| EQUAL => sdiff cmp l m
| GREATER => sdiff cmp (x::l) m
|- !P. (!cmp. P cmp [] []) /\ (!cmp x l. P cmp (x::l) []) /\
(!cmp y m. P cmp [] (y::m)) /\
(!cmp x l y m.
((apto cmp x y = EQUAL) ==> P cmp l m) /\
((apto cmp x y = GREATER) ==> P cmp (x::l) m) /\
((apto cmp x y = LESS) ==> P cmp l (y::m)) ==>
P cmp (x::l) (y::m)) ==>
!v v1 v2. P v v1 v2
|- !cmp l. OWL cmp (set l) (incr_ssort cmp l)
|- (!cmp. sinter cmp [] [] = []) /\
(!x l cmp. sinter cmp (x::l) [] = []) /\
(!y m cmp. sinter cmp [] (y::m) = []) /\
!y x m l cmp.
sinter cmp (x::l) (y::m) =
case apto cmp x y of
LESS => sinter cmp l (y::m)
| EQUAL => x::sinter cmp l m
| GREATER => sinter cmp (x::l) m
|- !P. (!cmp. P cmp [] []) /\ (!cmp x l. P cmp (x::l) []) /\
(!cmp y m. P cmp [] (y::m)) /\
(!cmp x l y m.
((apto cmp x y = EQUAL) ==> P cmp l m) /\
((apto cmp x y = GREATER) ==> P cmp (x::l) m) /\
((apto cmp x y = LESS) ==> P cmp l (y::m)) ==>
P cmp (x::l) (y::m)) ==>
!v v1 v2. P v v1 v2
|- (!cmp. smerge cmp [] [] = []) /\
(!x l cmp. smerge cmp (x::l) [] = x::l) /\
(!y m cmp. smerge cmp [] (y::m) = y::m) /\
!y x m l cmp.
smerge cmp (x::l) (y::m) =
case apto cmp x y of
LESS => x::smerge cmp l (y::m)
| EQUAL => x::smerge cmp l m
| GREATER => y::smerge cmp (x::l) m
|- !cmp l m. OL cmp l /\ OL cmp m ==> OL cmp (smerge cmp l m)
|- !P. (!cmp. P cmp [] []) /\ (!cmp x l. P cmp (x::l) []) /\
(!cmp y m. P cmp [] (y::m)) /\
(!cmp x l y m.
((apto cmp x y = EQUAL) ==> P cmp l m) /\
((apto cmp x y = GREATER) ==> P cmp (x::l) m) /\
((apto cmp x y = LESS) ==> P cmp l (y::m)) ==>
P cmp (x::l) (y::m)) ==>
!v v1 v2. P v v1 v2
|- !cmp l. (smerge cmp l [] = l) /\ (smerge cmp [] l = l)
|- (!l cmp. smerge_out cmp l [] = l) /\
(!lol l cmp. smerge_out cmp l (NONE::lol) = smerge_out cmp l lol) /\
!m lol l cmp.
smerge_out cmp l (SOME m::lol) = smerge_out cmp (smerge cmp l m) lol
|- !P. (!cmp l. P cmp l []) /\
(!cmp l lol. P cmp l lol ==> P cmp l (NONE::lol)) /\
(!cmp l m lol. P cmp (smerge cmp l m) lol ==> P cmp l (SOME m::lol)) ==>
!v v1 v2. P v v1 v2