Theory: enumeral

Type operators

bl : 'a bl
bt : 'a bt

Constants

BL_ACCUM : 'a -> 'a bt -> 'a bl -> 'a bl
BL_CONS : 'a -> 'a bl -> 'a bl
ENUMERAL : 'a toto -> 'a bt -> 'a -> bool
K2 : 'a -> num
LESS_ALL : 'a toto -> 'a -> ('a -> bool) -> bool
OL : 'a toto -> 'a list -> bool
OL_bt : 'a toto -> 'a bt -> bool
OL_bt_lb : 'a toto -> 'a -> 'a bt -> bool
OL_bt_lb_ub : 'a toto -> 'a -> 'a bt -> 'a -> bool
OL_bt_ub : 'a toto -> 'a bt -> 'a -> bool
OL_sublists : 'a toto -> 'a list option list -> bool
OU : 'a toto -> ('a -> bool) -> ('a -> bool) -> 'a -> bool
OWL : 'a toto -> ('a -> bool) -> 'a list -> bool
UO : 'a toto -> ('a -> bool) -> ('a -> bool) -> 'a -> bool
blMAP : ('a -> 'b) -> 'a bl -> 'b bl
blREL : ('a -> 'b -> bool) -> 'a bl -> 'b bl -> bool
blSET : 'a bl -> 'a -> bool
bl_CASE : 'a bl -> 'b -> ('a bl -> 'b) -> ('a -> 'a bt -> 'a bl -> 'b) -> 'b
bl_CONS : unit + 'b1 bl + 'b1 # 'b1 bt # 'b1 bl -> 'b1 bl
bl_rev : 'a bt -> 'a bl -> 'a bt
bl_size : ('a -> num) -> 'a bl -> num
bl_to_bt : 'a bl -> 'a bt
bl_to_set : 'a toto -> 'a bl -> 'a -> bool
btMAP : ('a -> 'b) -> 'a bt -> 'b bt
btREL : ('a -> 'b -> bool) -> 'a bt -> 'b bt -> bool
btSET : 'a bt -> 'a -> bool
bt_CASE : 'a bt -> 'b -> ('a bt -> 'a -> 'a bt -> 'b) -> 'b
bt_CONS : unit + 'b1 bt # 'b1 # 'b1 bt -> 'b1 bt
bt_rev : 'a bt -> 'a bl -> 'a bl
bt_size : ('a -> num) -> 'a bt -> num
bt_to_bl : 'a bt -> 'a bl
bt_to_list : 'a bt -> 'a list
bt_to_list_ac : 'a bt -> 'a list -> 'a list
bt_to_ol : 'a toto -> 'a bt -> 'a list
bt_to_ol_ac : 'a toto -> 'a bt -> 'a list -> 'a list
bt_to_ol_lb : 'a toto -> 'a -> 'a bt -> 'a list
bt_to_ol_lb_ac : 'a toto -> 'a -> 'a bt -> 'a list -> 'a list
bt_to_ol_lb_ub : 'a toto -> 'a -> 'a bt -> 'a -> 'a list
bt_to_ol_lb_ub_ac : 'a toto -> 'a -> 'a bt -> 'a -> 'a list -> 'a list
bt_to_ol_ub : 'a toto -> 'a bt -> 'a -> 'a list
bt_to_ol_ub_ac : 'a toto -> 'a bt -> 'a -> 'a list -> 'a list
bt_to_set_lb : 'a toto -> 'a -> 'a bt -> 'a -> bool
bt_to_set_lb_ub : 'a toto -> 'a -> 'a bt -> 'a -> 'a -> bool
bt_to_set_ub : 'a toto -> 'a bt -> 'a -> 'a -> bool
incr_sbuild : 'a toto -> 'a list -> 'a list option list
incr_smerge : 'a toto -> 'a list -> 'a list option list -> 'a list option list
incr_ssort : 'a toto -> 'a list -> 'a list
list_to_bl : 'a list -> 'a bl
list_to_bt : 'c list -> 'c bt
lol_set : 'a list option list -> 'a -> bool
nbl : 'a bl
node : 'a bt -> 'a -> 'a bt -> 'a bt
nt : 'a bt
onebl : 'a -> 'a bt -> 'a bl -> 'a bl
sdiff : 'a toto -> 'a list -> 'a list -> 'a list
sinter : 'a toto -> 'a list -> 'a list -> 'a list
smerge : 'a toto -> 'a list -> 'a list -> 'a list
smerge_out : 'a toto -> 'a list -> 'a list option list -> 'a list
zerbl : 'a bl -> 'a bl

Definitions

Theorems

AND_CONV_conj EMPTY_OU ENUMERAL_set EQUAL_F EQ_EQUAL_REWR EQ_GREATER_REWR EQ_LESS_REWR GREATER_F IN_bt_to_set IN_node LESS_ALL_OU LESS_ALL_OU_UO_LEM LESS_ALL_UO_LEM LESS_UO_LEM LIST_TO_SET_CONS LIST_TO_SET_NIL NOT_IN_nt OL_DIFF_IMP OL_ENUMERAL OL_INTER_IMP OL_UNION_IMP OL_bt_to_ol OL_bt_to_ol_lb OL_bt_to_ol_lb_ub OL_bt_to_ol_ub OL_sublists OL_sublists_ind OU_ASSOC OU_EMPTY OWL_DIFF_THM OWL_INTER_THM OWL_UNION_THM OWL_bt_to_ol better_bt_to_ol blMAP_ind blMAP_thm blSET_ind blSET_thm bl_11 bl_Axiom bl_MAP_CONG bl_MAP_ID bl_MAP_IMAGE bl_MAP_O bl_bnd bl_case_cong bl_case_eq bl_distinct bl_induction bl_inh bl_nchotomy bl_wit btMAP_ind btMAP_thm btSET_ind btSET_thm bt_11 bt_Axiom bt_MAP_CONG bt_MAP_ID bt_MAP_IMAGE bt_MAP_O bt_bnd bt_case_cong bt_case_eq bt_distinct bt_induction bt_inh bt_nchotomy bt_to_list_thm bt_to_ol_ID_IMP bt_wit datatype_bl datatype_bt incr_smerge incr_smerge_OL incr_smerge_ind lol_set lol_set_ind ol_set sdiff sdiff_ind set_OWL_thm sinter sinter_ind smerge smerge_OL smerge_ind smerge_nil smerge_out smerge_out_ind

Definitions

BL_ACCUM

|- (!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)

BL_CONS

|- !a bl. BL_CONS a bl = BL_ACCUM a nt bl

K2

|- !a. K2 a = 2

LESS_ALL

|- !cmp x s. LESS_ALL cmp x s <=> !y. y IN s ==> (apto cmp x y = LESS)

OL

|- (!cmp. OL cmp [] <=> T) /\
   !cmp a l.
     OL cmp (a::l) <=> OL cmp l /\ !p. MEM p l ==> (apto cmp a p = LESS)

OL_bt

|- (!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

OL_bt_lb

|- (!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

OL_bt_lb_ub

|- (!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

OL_bt_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

OU

|- !cmp t u.
     OU cmp t u =
     {x | x IN t /\ !z. z IN u ==> (apto cmp x z = LESS)} UNION u

OWL

|- !cmp s l. OWL cmp s l <=> (s = set l) /\ OL cmp l

UO

|- !cmp s t.
     UO cmp s t =
     s UNION {y | y IN t /\ !z. z IN s ==> (apto cmp z y = LESS)}

blMAP_def

|- !f af.
     blMAP f (bl_CONS af) =
     bl_CONS (SUM_MAP I (SUM_MAP (blMAP f) (f ## btMAP f ## blMAP f)) af)

blREL_def

|- blREL =
   (\R x y.
      ?z. (!p. p IN blSET z ==> R (FST p) (SND p)) /\ (blMAP FST z = x) /\
          (blMAP SND z = y))

blSET_def

|- !af.
     blSET (bl_CONS af) =
     S ($UNION o BIMG (K {}) o setL)
       (BIMG
          (S ($UNION o BIMG (K {}) o setL)
             (BIMG
                (S ($UNION o BIMG $= o setFST)
                   (BIMG
                      (S ($UNION o BIMG (BIMG $= o btSET) o setFST)
                         (BIMG (K {}) o setSND)) o setSND)) o setR)) o setR)
       af UNION
     BIGUNION
       (IMAGE blSET
          (S ($UNION o BIMG (K {}) o setL)
             (BIMG
                (S ($UNION o BIMG $= o setL)
                   (BIMG
                      (S ($UNION o BIMG (K {}) o setFST)
                         (BIMG
                            (S
                               ($UNION o BIMG (BIMG (K {}) o btSET) o
                                setFST) (BIMG $= o setSND)) o setSND)) o
                    setR)) o setR) af))

bl_case_def

|- (!v f f0. bl_CASE nbl v f f0 = v) /\
   (!a0 v f f0. bl_CASE (zerbl a0) v f f0 = f a0) /\
   !a0 a1 a2 v f f0. bl_CASE (onebl a0 a1 a2) v f f0 = f0 a0 a1 a2

bl_rev

|- (!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

|- (!f0. bl_size f0 nbl = 0) /\
   (!f0 a0. bl_size f0 (zerbl a0) = 1 + bl_size f0 a0) /\
   !f0 a0 a1 a2.
     bl_size f0 (onebl a0 a1 a2) =
     1 + (f0 a0 + (bt_size f0 a1 + bl_size f0 a2))

bl_to_bt

|- bl_to_bt = bl_rev nt

bl_to_set

|- (!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)

btMAP_def

|- !f af.
     btMAP f (bt_CONS af) =
     bt_CONS (SUM_MAP I (btMAP f ## f ## btMAP f) af)

btREL_def

|- btREL =
   (\R x y.
      ?z. (!p. p IN btSET z ==> R (FST p) (SND p)) /\ (btMAP FST z = x) /\
          (btMAP SND z = y))

btSET_def

|- !af.
     btSET (bt_CONS af) =
     S ($UNION o BIMG (K {}) o setL)
       (BIMG
          (S ($UNION o BIMG (K {}) o setFST)
             (BIMG (S ($UNION o BIMG $= o setFST) (BIMG (K {}) o setSND)) o
              setSND)) o setR) af UNION
     BIGUNION
       (IMAGE btSET
          (S ($UNION o BIMG (K {}) o setL)
             (BIMG
                (S ($UNION o BIMG $= o setFST)
                   (BIMG
                      (S ($UNION o BIMG (K {}) o setFST) (BIMG $= o setSND)) o
                    setSND)) o setR) af))

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

bt_rev

|- (!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

|- (!f0. bt_size f0 nt = 0) /\
   !f0 a0 a1 a2.
     bt_size f0 (node a0 a1 a2) =
     1 + (bt_size f0 a0 + (f0 a1 + bt_size f0 a2))

bt_to_bl

|- !t. bt_to_bl t = bt_rev t nbl

bt_to_list

|- (bt_to_list nt = []) /\
   !l x r. bt_to_list (node l x r) = bt_to_list l ++ [x] ++ bt_to_list r

bt_to_list_ac

|- (!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)

bt_to_ol

|- (!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

bt_to_ol_ac

|- (!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)

bt_to_ol_lb

|- (!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

bt_to_ol_lb_ac

|- (!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

bt_to_ol_lb_ub

|- (!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

bt_to_ol_lb_ub_ac

|- (!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

bt_to_ol_ub

|- (!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

bt_to_ol_ub_ac

|- (!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

bt_to_set

|- (!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)}

bt_to_set_lb

|- !cmp lb t.
     bt_to_set_lb cmp lb t =
     {x | x IN ENUMERAL cmp t /\ (apto cmp lb x = LESS)}

bt_to_set_lb_ub

|- !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)}

bt_to_set_ub

|- !cmp t ub.
     bt_to_set_ub cmp t ub =
     {x | x IN ENUMERAL cmp t /\ (apto cmp x ub = LESS)}

incr_sbuild

|- (!cmp. incr_sbuild cmp [] = []) /\
   !cmp x l.
     incr_sbuild cmp (x::l) = incr_smerge cmp [x] (incr_sbuild cmp l)

incr_ssort

|- !cmp l. incr_ssort cmp l = smerge_out cmp [] (incr_sbuild cmp l)

list_to_bl

|- (list_to_bl [] = nbl) /\
   !a l. list_to_bl (a::l) = BL_CONS a (list_to_bl l)

list_to_bt

|- !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

AND_CONV_conj

|- (T /\ T <=> T) /\ (T /\ F <=> F) /\ (F /\ T <=> F) /\ (F /\ F <=> F)

EMPTY_OU

|- !cmp sl. OU cmp {} sl = sl

ENUMERAL_set

|- !cmp l. set l = ENUMERAL cmp (list_to_bt (incr_ssort cmp l))

EQUAL_F

|- (EQUAL = LESS) <=> F

EQ_EQUAL_REWR

|- !v0 v1. (if EQUAL = LESS then v0 else v1) = v1

EQ_GREATER_REWR

|- !v0 v1. (if GREATER = LESS then v0 else v1) = v1

EQ_LESS_REWR

|- !v0 v1. (if LESS = LESS then v0 else v1) = v0

GREATER_F

|- (GREATER = LESS) <=> F

IN_bt_to_set

|- (!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)

IN_node

|- !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

LESS_ALL_OU

|- !cmp x u v.
     LESS_ALL cmp x (OU cmp u v) <=> LESS_ALL cmp x u /\ LESS_ALL cmp x v

LESS_ALL_OU_UO_LEM

|- !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)

LESS_ALL_UO_LEM

|- !cmp a s. LESS_ALL cmp a s ==> (UO cmp {a} s = a INSERT s)

LESS_UO_LEM

|- !cmp x y s.
     (!z. z IN UO cmp {x} s ==> (apto cmp y z = LESS)) <=>
     (apto cmp y x = LESS)

LIST_TO_SET_CONS

|- !a l s. (s = set l) ==> (a INSERT s = set (a::l))

LIST_TO_SET_NIL

|- {} = set []

NOT_IN_nt

|- !cmp y. y IN ENUMERAL cmp nt <=> F

OL_DIFF_IMP

|- !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)

OL_ENUMERAL

|- !cmp l. OL cmp l ==> (set l = ENUMERAL cmp (list_to_bt l))

OL_INTER_IMP

|- !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)

OL_UNION_IMP

|- !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)

OL_bt_to_ol

|- !cmp t. OL cmp (bt_to_ol cmp t)

OL_bt_to_ol_lb

|- !cmp t lb. OL cmp (bt_to_ol_lb cmp lb t)

OL_bt_to_ol_lb_ub

|- !cmp t lb ub. OL cmp (bt_to_ol_lb_ub cmp lb t ub)

OL_bt_to_ol_ub

|- !cmp t ub. OL cmp (bt_to_ol_ub cmp t ub)

OL_sublists

|- (!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

OL_sublists_ind

|- !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

OU_ASSOC

|- !cmp a b c. OU cmp a (OU cmp b c) = OU cmp (OU cmp a b) c

OU_EMPTY

|- !cmp t. OU cmp t {} = t

OWL_DIFF_THM

|- !cmp s l t m.
     OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s DIFF t) (sdiff cmp l m)

OWL_INTER_THM

|- !cmp s l t m.
     OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s INTER t) (sinter cmp l m)

OWL_UNION_THM

|- !cmp s l t m.
     OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s UNION t) (smerge cmp l m)

OWL_bt_to_ol

|- !cmp t. OWL cmp (ENUMERAL cmp t) (bt_to_ol cmp t)

better_bt_to_ol

|- !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 []

blMAP_ind

|- !P'.
     (!f. P' f nbl /\ (!b. P' f b ==> P' f (zerbl b)) /\
          !b. P' f b ==> !b0 a. P' f (onebl a b0 b)) ==>
     !f b. P' f b

blMAP_thm

|- (blMAP f nbl = nbl) /\ (blMAP f (zerbl a0) = zerbl (blMAP f a0)) /\
   (blMAP f (onebl a0 a1 a2) = onebl (f a0) (btMAP f a1) (blMAP f a2))

blSET_ind

|- !P'.
     P' nbl /\ (!b. P' b ==> P' (zerbl b)) /\
     (!b. P' b ==> !b0 a. P' (onebl a b0 b)) ==>
     !b. P' b

blSET_thm

|- (blSET nbl = {}) /\ (blSET (zerbl a0) = blSET a0) /\
   (blSET (onebl a0 a1 a2) = a0 INSERT btSET a1 UNION blSET a2)

bl_11

|- (!a0 a0'. (zerbl a0 = zerbl a0') <=> (a0 = a0')) /\
   !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. ?h.
     (h nbl = f0) /\ (!a0. h (zerbl a0) = f1 a0 (h a0)) /\
     !a0 a1 a2. h (onebl a0 a1 a2) = f2 a0 a1 a2 (h a2)

bl_MAP_CONG

|- !f g x. (!a. a IN blSET x ==> (f a = g a)) ==> (blMAP f x = blMAP g x)

bl_MAP_ID

|- blMAP I = I

bl_MAP_IMAGE

|- !f n. blSET (blMAP f n) = IMAGE f (blSET n)

bl_MAP_O

|- blMAP f o blMAP g = blMAP (f o g)

bl_bnd

|- !n. cardleq (blSET n) univ(:num)

bl_case_cong

|- !M M' v f f0.
     (M = M') /\ ((M' = nbl) ==> (v = v')) /\
     (!a0. (M' = zerbl a0) ==> (f a0 = f' a0)) /\
     (!a0 a1 a2. (M' = onebl a0 a1 a2) ==> (f0 a0 a1 a2 = f0' a0 a1 a2)) ==>
     (bl_CASE M v f f0 = bl_CASE M' v' f' f0')

bl_case_eq

|- (bl_CASE x v f f0 = v') <=>
   (x = nbl) /\ (v = v') \/ (?b. (x = zerbl b) /\ (f b = v')) \/
   ?a b0 b. (x = onebl a b0 b) /\ (f0 a b0 b = v')

bl_distinct

|- (!a0. nbl <> zerbl a0) /\ (!a2 a1 a0. nbl <> onebl a0 a1 a2) /\
   !a2 a1 a0' a0. zerbl a0 <> 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_inh

|- !a2. a2 IN blSET ((\a2. bl_CONS (INR (INR (flip $, ARB a2)))) a2)

bl_nchotomy

|- !bb. (bb = nbl) \/ (?b. bb = zerbl b) \/ ?a b0 b. bb = onebl a b0 b

bl_wit

|- !a. blSET ((\a. bl_CONS ((K o INL) ARB ARB)) a) SUBSET {}

btMAP_ind

|- !P'.
     (!f. P' f nt /\ !b b0. P' f b /\ P' f b0 ==> !a. P' f (node b a b0)) ==>
     !f b. P' f b

btMAP_thm

|- (btMAP f nt = nt) /\
   (btMAP f (node a0 a1 a2) = node (btMAP f a0) (f a1) (btMAP f a2))

btSET_ind

|- !P'.
     P' nt /\ (!b b0. P' b /\ P' b0 ==> !a. P' (node b a b0)) ==> !b. P' b

btSET_thm

|- (btSET nt = {}) /\
   (btSET (node a0 a1 a2) = a1 INSERT btSET a0 UNION btSET a2)

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. ?h.
     (h nt = f0) /\
     !a0 a1 a2. h (node a0 a1 a2) = f1 a1 a0 a2 (h a0) (h a2)

bt_MAP_CONG

|- !f g x. (!a. a IN btSET x ==> (f a = g a)) ==> (btMAP f x = btMAP g x)

bt_MAP_ID

|- btMAP I = I

bt_MAP_IMAGE

|- !f n. btSET (btMAP f n) = IMAGE f (btSET n)

bt_MAP_O

|- btMAP f o btMAP g = btMAP (f o g)

bt_bnd

|- !n. cardleq (btSET n) univ(:num)

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_inh

|- !a2. a2 IN btSET ((\a2. bt_CONS (INR (ARB,flip $, ARB a2))) a2)

bt_nchotomy

|- !bb. (bb = nt) \/ ?b a b0. bb = node b a b0

bt_to_list_thm

|- !t. bt_to_list t = bt_to_list_ac t []

bt_to_ol_ID_IMP

|- !cmp l. OL cmp l ==> (bt_to_ol cmp (list_to_bt l) = l)

bt_wit

|- !a. btSET ((\a. bt_CONS ((K o INL) ARB ARB)) a) SUBSET {}

datatype_bl

|- DATATYPE (bl nbl zerbl onebl)

datatype_bt

|- DATATYPE (bt nt node)

incr_smerge

|- (!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

incr_smerge_OL

|- !cmp lol l.
     OL_sublists cmp lol /\ OL cmp l ==>
     OL_sublists cmp (incr_smerge cmp l lol)

incr_smerge_ind

|- !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_set [] = {}) /\ (!lol. lol_set (NONE::lol) = lol_set lol) /\
   !m lol. lol_set (SOME m::lol) = set m UNION lol_set lol

lol_set_ind

|- !P. P [] /\ (!lol. P lol ==> P (NONE::lol)) /\
       (!m lol. P lol ==> P (SOME m::lol)) ==>
       !v. P v

ol_set

|- !cmp t. ENUMERAL cmp t = set (bt_to_ol cmp t)

sdiff

|- (!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

sdiff_ind

|- !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

set_OWL_thm

|- !cmp l. OWL cmp (set l) (incr_ssort cmp l)

sinter

|- (!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

sinter_ind

|- !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

smerge

|- (!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

smerge_OL

|- !cmp l m. OL cmp l /\ OL cmp m ==> OL cmp (smerge cmp l m)

smerge_ind

|- !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

smerge_nil

|- !cmp l. (smerge cmp l [] = l) /\ (smerge cmp [] l = l)

smerge_out

|- (!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

smerge_out_ind

|- !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

Theory enumeral

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems