Structure enumeralTheory


Source File Identifier index Theory binding index

signature enumeralTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val BL_ACCUM : thm
    val BL_CONS : thm
    val K2 : thm
    val LESS_ALL : thm
    val OL : thm
    val OL_bt : thm
    val OL_bt_lb : thm
    val OL_bt_lb_ub : thm
    val OL_bt_ub : thm
    val OU : thm
    val OWL : thm
    val UO : thm
    val bl_TY_DEF : thm
    val bl_case_def : thm
    val bl_rev : thm
    val bl_size_def : thm
    val bl_to_bt : thm
    val bl_to_set : thm
    val bt_TY_DEF : thm
    val bt_rev : thm
    val bt_size_def : thm
    val bt_to_bl : thm
    val bt_to_list : thm
    val bt_to_list_ac : thm
    val bt_to_ol : thm
    val bt_to_ol_ac : thm
    val bt_to_ol_lb : thm
    val bt_to_ol_lb_ac : thm
    val bt_to_ol_lb_ub : thm
    val bt_to_ol_lb_ub_ac : thm
    val bt_to_ol_ub : thm
    val bt_to_ol_ub_ac : thm
    val bt_to_set : thm
    val bt_to_set_lb : thm
    val bt_to_set_lb_ub : thm
    val bt_to_set_ub : thm
    val incr_sbuild : thm
    val incr_ssort : thm
    val list_to_bl : thm
    val list_to_bt : thm
    val lol_set_primitive : thm
  
  (*  Theorems  *)
    val EMPTY_OU : thm
    val ENUMERAL_set : thm
    val IN_bt_to_set : thm
    val IN_node : thm
    val LESS_ALL_OU : thm
    val LESS_ALL_OU_UO_LEM : thm
    val LESS_ALL_UO_LEM : thm
    val LESS_UO_LEM : thm
    val NOT_IN_nt : thm
    val OL_DIFF_IMP : thm
    val OL_ENUMERAL : thm
    val OL_INTER_IMP : thm
    val OL_UNION_IMP : thm
    val OL_bt_to_ol : thm
    val OL_bt_to_ol_lb : thm
    val OL_bt_to_ol_lb_ub : thm
    val OL_bt_to_ol_ub : thm
    val OL_sublists : thm
    val OL_sublists_ind : thm
    val OU_ASSOC : thm
    val OU_EMPTY : thm
    val OWL_DIFF_THM : thm
    val OWL_INTER_THM : thm
    val OWL_UNION_THM : thm
    val OWL_bt_to_ol : thm
    val better_bt_to_ol : thm
    val bl_11 : thm
    val bl_Axiom : thm
    val bl_case_cong : thm
    val bl_case_eq : thm
    val bl_distinct : thm
    val bl_induction : thm
    val bl_nchotomy : thm
    val bt_11 : thm
    val bt_Axiom : thm
    val bt_case_cong : thm
    val bt_case_def : thm
    val bt_case_eq : thm
    val bt_distinct : thm
    val bt_induction : thm
    val bt_nchotomy : thm
    val bt_to_list_thm : thm
    val bt_to_ol_ID_IMP : thm
    val datatype_bl : thm
    val datatype_bt : thm
    val incr_smerge : thm
    val incr_smerge_OL : thm
    val incr_smerge_ind : thm
    val lol_set : thm
    val lol_set_ind : thm
    val ol_set : thm
    val sdiff : thm
    val sdiff_ind : thm
    val set_OWL_thm : thm
    val sinter : thm
    val sinter_ind : thm
    val smerge : thm
    val smerge_OL : thm
    val smerge_ind : thm
    val smerge_nil : thm
    val smerge_out : thm
    val smerge_out_ind : thm
  
  val enumeral_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [res_quan] Parent theory of "enumeral"
   
   [toto] Parent theory of "enumeral"
   
   [BL_ACCUM]  Definition
      
      |- (!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]  Definition
      
      |- !a bl. BL_CONS a bl = BL_ACCUM a nt bl
   
   [K2]  Definition
      
      |- !a. K2 a = 2
   
   [LESS_ALL]  Definition
      
      |- !cmp x s.
           LESS_ALL cmp x s <=> !y. y IN s ==> (apto cmp x y = LESS)
   
   [OL]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- !cmp t u.
           OU cmp t u =
           {x | x IN t /\ !z. z IN u ==> (apto cmp x z = LESS)} UNION u
   
   [OWL]  Definition
      
      |- !cmp s l. OWL cmp s l <=> (s = set l) /\ OL cmp l
   
   [UO]  Definition
      
      |- !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]  Definition
      
      |- ?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]  Definition
      
      |- (!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
   
   [bl_rev]  Definition
      
      |- (!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]  Definition
      
      |- (!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))
   
   [bl_to_bt]  Definition
      
      |- bl_to_bt = bl_rev nt
   
   [bl_to_set]  Definition
      
      |- (!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]  Definition
      
      |- ?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_rev]  Definition
      
      |- (!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]  Definition
      
      |- (!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))
   
   [bt_to_bl]  Definition
      
      |- !t. bt_to_bl t = bt_rev t nbl
   
   [bt_to_list]  Definition
      
      |- (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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- (!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]  Definition
      
      |- !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]  Definition
      
      |- !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]  Definition
      
      |- !cmp t ub.
           bt_to_set_ub cmp t ub =
           {x | x IN ENUMERAL cmp t /\ (apto cmp x ub = LESS)}
   
   [incr_sbuild]  Definition
      
      |- (!cmp. incr_sbuild cmp [] = []) /\
         !cmp x l.
           incr_sbuild cmp (x::l) = incr_smerge cmp [x] (incr_sbuild cmp l)
   
   [incr_ssort]  Definition
      
      |- !cmp l. incr_ssort cmp l = smerge_out cmp [] (incr_sbuild cmp l)
   
   [list_to_bl]  Definition
      
      |- (list_to_bl [] = nbl) /\
         !a l. list_to_bl (a::l) = BL_CONS a (list_to_bl l)
   
   [list_to_bt]  Definition
      
      |- !l. list_to_bt l = bl_to_bt (list_to_bl l)
   
   [lol_set_primitive]  Definition
      
      |- 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))
   
   [EMPTY_OU]  Theorem
      
      |- !cmp sl. OU cmp {} sl = sl
   
   [ENUMERAL_set]  Theorem
      
      |- !cmp l. set l = ENUMERAL cmp (list_to_bt (incr_ssort cmp l))
   
   [IN_bt_to_set]  Theorem
      
      |- (!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]  Theorem
      
      |- !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]  Theorem
      
      |- !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]  Theorem
      
      |- !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]  Theorem
      
      |- !cmp a s. LESS_ALL cmp a s ==> (UO cmp {a} s = a INSERT s)
   
   [LESS_UO_LEM]  Theorem
      
      |- !cmp x y s.
           (!z. z IN UO cmp {x} s ==> (apto cmp y z = LESS)) <=>
           (apto cmp y x = LESS)
   
   [NOT_IN_nt]  Theorem
      
      |- !cmp y. y IN ENUMERAL cmp nt <=> F
   
   [OL_DIFF_IMP]  Theorem
      
      |- !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]  Theorem
      
      |- !cmp l. OL cmp l ==> (set l = ENUMERAL cmp (list_to_bt l))
   
   [OL_INTER_IMP]  Theorem
      
      |- !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]  Theorem
      
      |- !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]  Theorem
      
      |- !cmp t. OL cmp (bt_to_ol cmp t)
   
   [OL_bt_to_ol_lb]  Theorem
      
      |- !cmp t lb. OL cmp (bt_to_ol_lb cmp lb t)
   
   [OL_bt_to_ol_lb_ub]  Theorem
      
      |- !cmp t lb ub. OL cmp (bt_to_ol_lb_ub cmp lb t ub)
   
   [OL_bt_to_ol_ub]  Theorem
      
      |- !cmp t ub. OL cmp (bt_to_ol_ub cmp t ub)
   
   [OL_sublists]  Theorem
      
      |- (!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]  Theorem
      
      |- !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]  Theorem
      
      |- !cmp a b c. OU cmp a (OU cmp b c) = OU cmp (OU cmp a b) c
   
   [OU_EMPTY]  Theorem
      
      |- !cmp t. OU cmp t {} = t
   
   [OWL_DIFF_THM]  Theorem
      
      |- !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]  Theorem
      
      |- !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]  Theorem
      
      |- !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]  Theorem
      
      |- !cmp t. OWL cmp (ENUMERAL cmp t) (bt_to_ol cmp t)
   
   [better_bt_to_ol]  Theorem
      
      |- !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]  Theorem
      
      |- (!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]  Theorem
      
      |- !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]  Theorem
      
      |- !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]  Theorem
      
      |- (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]  Theorem
      
      |- (!a. nbl <> zerbl a) /\ (!a2 a1 a0. nbl <> onebl a0 a1 a2) /\
         !a2 a1 a0 a. zerbl a <> onebl a0 a1 a2
   
   [bl_induction]  Theorem
      
      |- !P. P nbl /\ (!b. P b ==> P (zerbl b)) /\
             (!b. P b ==> !b0 a. P (onebl a b0 b)) ==>
             !b. P b
   
   [bl_nchotomy]  Theorem
      
      |- !bb.
           (bb = nbl) \/ (?b. bb = zerbl b) \/ ?a b0 b. bb = onebl a b0 b
   
   [bt_11]  Theorem
      
      |- !a0 a1 a2 a0' a1' a2'.
           (node a0 a1 a2 = node a0' a1' a2') <=>
           (a0 = a0') /\ (a1 = a1') /\ (a2 = a2')
   
   [bt_Axiom]  Theorem
      
      |- !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]  Theorem
      
      |- !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_def]  Theorem
      
      |- (!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_case_eq]  Theorem
      
      |- (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]  Theorem
      
      |- !a2 a1 a0. nt <> node a0 a1 a2
   
   [bt_induction]  Theorem
      
      |- !P. P nt /\ (!b b0. P b /\ P b0 ==> !a. P (node b a b0)) ==>
             !b. P b
   
   [bt_nchotomy]  Theorem
      
      |- !bb. (bb = nt) \/ ?b a b0. bb = node b a b0
   
   [bt_to_list_thm]  Theorem
      
      |- !t. bt_to_list t = bt_to_list_ac t []
   
   [bt_to_ol_ID_IMP]  Theorem
      
      |- !cmp l. OL cmp l ==> (bt_to_ol cmp (list_to_bt l) = l)
   
   [datatype_bl]  Theorem
      
      |- DATATYPE (bl nbl zerbl onebl)
   
   [datatype_bt]  Theorem
      
      |- DATATYPE (bt nt node)
   
   [incr_smerge]  Theorem
      
      |- (!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]  Theorem
      
      |- !cmp lol l.
           OL_sublists cmp lol /\ OL cmp l ==>
           OL_sublists cmp (incr_smerge cmp l lol)
   
   [incr_smerge_ind]  Theorem
      
      |- !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]  Theorem
      
      |- (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]  Theorem
      
      |- !P. P [] /\ (!lol. P lol ==> P (NONE::lol)) /\
             (!m lol. P lol ==> P (SOME m::lol)) ==>
             !v. P v
   
   [ol_set]  Theorem
      
      |- !cmp t. ENUMERAL cmp t = set (bt_to_ol cmp t)
   
   [sdiff]  Theorem
      
      |- (!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]  Theorem
      
      |- !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]  Theorem
      
      |- !cmp l. OWL cmp (set l) (incr_ssort cmp l)
   
   [sinter]  Theorem
      
      |- (!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]  Theorem
      
      |- !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]  Theorem
      
      |- (!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]  Theorem
      
      |- !cmp l m. OL cmp l /\ OL cmp m ==> OL cmp (smerge cmp l m)
   
   [smerge_ind]  Theorem
      
      |- !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]  Theorem
      
      |- !cmp l. (smerge cmp l [] = l) /\ (smerge cmp [] l = l)
   
   [smerge_out]  Theorem
      
      |- (!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]  Theorem
      
      |- !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
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14