Structure fmapalTheory


Source File Identifier index Theory binding index

signature fmapalTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val AP_SND : thm
    val OFU : thm
    val OPTION_FLAT_primitive : thm
    val OPTION_UPDATE : thm
    val ORWL : thm
    val UFO : thm
    val bt_map : thm
    val bt_to_fmap_lb : thm
    val bt_to_fmap_lb_ub : thm
    val bt_to_fmap_ub : thm
    val bt_to_orl_lb_ub_ac_tupled_AUX : thm
    val fmap : thm
    val incr_build : thm
    val incr_flat : thm
    val incr_sort : thm
    val optry : thm
    val unlookup : thm
    val vcossa : thm
  
  (*  Theorems  *)
    val FAPPLY_fmap_CONS : thm
    val FAPPLY_fmap_NIL : thm
    val FAPPLY_node : thm
    val FAPPLY_nt : thm
    val FMAPAL_FDOM_THM : thm
    val FMAPAL_fmap : thm
    val FUN_fmap_thm : thm
    val OPTION_FLAT : thm
    val OPTION_FLAT_ind : thm
    val ORL : thm
    val ORL_DRESTRICT_COMPL_IMP : thm
    val ORL_DRESTRICT_IMP : thm
    val ORL_FMAPAL : thm
    val ORL_FUNION_IMP : thm
    val ORL_bt : thm
    val ORL_bt_ind : thm
    val ORL_bt_lb : thm
    val ORL_bt_lb_ind : thm
    val ORL_bt_lb_ub : thm
    val ORL_bt_lb_ub_ind : thm
    val ORL_bt_ub : thm
    val ORL_bt_ub_ind : thm
    val ORL_ind : thm
    val ORL_sublists : thm
    val ORL_sublists_ind : thm
    val ORWL_DRESTRICT_COMPL_THM : thm
    val ORWL_DRESTRICT_THM : thm
    val ORWL_FUNION_THM : thm
    val ORWL_bt_to_orl : thm
    val assocv : thm
    val assocv_ind : thm
    val better_bt_to_orl : thm
    val bl_to_fmap : thm
    val bl_to_fmap_ind : thm
    val bt_FST_FDOM : thm
    val bt_rplacv_cn : thm
    val bt_rplacv_cn_ind : thm
    val bt_rplacv_thm : thm
    val bt_to_fmap : thm
    val bt_to_fmap_ind : thm
    val bt_to_orl : thm
    val bt_to_orl_ID_IMP : thm
    val bt_to_orl_ac : thm
    val bt_to_orl_ac_ind : thm
    val bt_to_orl_ind : thm
    val bt_to_orl_lb : thm
    val bt_to_orl_lb_ac : thm
    val bt_to_orl_lb_ac_ind : thm
    val bt_to_orl_lb_ind : thm
    val bt_to_orl_lb_ub : thm
    val bt_to_orl_lb_ub_ac : thm
    val bt_to_orl_lb_ub_ac_ind : thm
    val bt_to_orl_lb_ub_ind : thm
    val bt_to_orl_ub : thm
    val bt_to_orl_ub_ac : thm
    val bt_to_orl_ub_ac_ind : thm
    val bt_to_orl_ub_ind : thm
    val diff_merge : thm
    val diff_merge_ind : thm
    val fmap_FDOM : thm
    val fmap_FDOM_rec : thm
    val fmap_ORWL_thm : thm
    val incr_merge : thm
    val incr_merge_ind : thm
    val inter_merge : thm
    val inter_merge_ind : thm
    val list_rplacv_cn : thm
    val list_rplacv_cn_ind : thm
    val list_rplacv_thm : thm
    val merge : thm
    val merge_ind : thm
    val merge_out : thm
    val merge_out_ind : thm
    val o_f_bt_map : thm
    val o_f_fmap : thm
    val optry_list : thm
    val optry_list_ind : thm
  
  val fmapal_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [enumeral] Parent theory of "fmapal"
   
   [finite_map] Parent theory of "fmapal"
   
   [AP_SND]  Definition
      
      |- !f a b. AP_SND f (a,b) = (a,f b)
   
   [OFU]  Definition
      
      |- !cmp f g.
             OFU cmp f g =
             DRESTRICT f {x | LESS_ALL cmp x (FDOM g)} FUNION g
   
   [OPTION_FLAT_primitive]  Definition
      
      |- OPTION_FLAT =
         WFREC (@R. WF R /\ (!l. R l (NONE::l)) /\ !a l. R l (SOME a::l))
           (\OPTION_FLAT a'.
                case a' of
                  [] => I []
                | NONE::l => I (OPTION_FLAT l)
                | SOME a::l => I (a ++ OPTION_FLAT l))
   
   [OPTION_UPDATE]  Definition
      
      |- !f g x. OPTION_UPDATE f g x = optry (f x) (g x)
   
   [ORWL]  Definition
      
      |- !cmp f l. ORWL cmp f l <=> (f = fmap l) /\ ORL cmp l
   
   [UFO]  Definition
      
      |- !cmp f g.
             UFO cmp f g =
             f FUNION
             DRESTRICT g {y | (!z. z IN FDOM f ==> (apto cmp z y = LESS))}
   
   [bt_map]  Definition
      
      |- (!f. bt_map f nt = nt) /\
         !f l x r.
             bt_map f (node l x r) = node (bt_map f l) (f x) (bt_map f r)
   
   [bt_to_fmap_lb]  Definition
      
      |- !cmp lb t.
             bt_to_fmap_lb cmp lb t =
             DRESTRICT (FMAPAL cmp t) {x | apto cmp lb x = LESS}
   
   [bt_to_fmap_lb_ub]  Definition
      
      |- !cmp lb t ub.
             bt_to_fmap_lb_ub cmp lb t ub =
             DRESTRICT (FMAPAL cmp t)
               {x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}
   
   [bt_to_fmap_ub]  Definition
      
      |- !cmp t ub.
             bt_to_fmap_ub cmp t ub =
             DRESTRICT (FMAPAL cmp t) {x | apto cmp x ub = LESS}
   
   [bt_to_orl_lb_ub_ac_tupled_AUX]  Definition
      
      |- !R.
             bt_to_orl_lb_ub_ac_tupled_aux R =
             WFREC R
               (\bt_to_orl_lb_ub_ac_tupled a.
                    case a of
                      (cmp,lb,nt,ub,m) => I m
                    | (cmp,lb,node l (x,y) r,ub,m) =>
                      I
                        (if apto cmp lb x = LESS then
                           if apto cmp x ub = LESS then
                             bt_to_orl_lb_ub_ac_tupled
                               (cmp,lb,l,x,
                                (x,y)::
                                    bt_to_orl_lb_ub_ac_tupled
                                      (cmp,x,r,ub,m))
                           else bt_to_orl_lb_ub_ac_tupled (cmp,lb,l,ub,m)
                         else bt_to_orl_lb_ub_ac_tupled (cmp,lb,r,ub,m)))
   
   [fmap]  Definition
      
      |- !l. fmap l = FEMPTY |++ REVERSE l
   
   [incr_build]  Definition
      
      |- (!cmp. incr_build cmp [] = []) /\
         !cmp ab l.
             incr_build cmp (ab::l) =
             incr_merge cmp [ab] (incr_build cmp l)
   
   [incr_flat]  Definition
      
      |- !cmp lol. incr_flat cmp lol = merge_out cmp [] lol
   
   [incr_sort]  Definition
      
      |- !cmp l. incr_sort cmp l = merge_out cmp [] (incr_build cmp l)
   
   [optry]  Definition
      
      |- (!p q. optry (SOME p) q = SOME p) /\ !q. optry NONE q = q
   
   [unlookup]  Definition
      
      |- !f. unlookup f = FUN_FMAP (THE o f) (IS_SOME o f)
   
   [vcossa]  Definition
      
      |- !a l. vcossa a l = assocv l a
   
   [FAPPLY_fmap_CONS]  Theorem
      
      |- !x y z l. fmap ((y,z)::l) ' x = if x = y then z else fmap l ' x
   
   [FAPPLY_fmap_NIL]  Theorem
      
      |- !x. fmap [] ' x = FEMPTY ' x
   
   [FAPPLY_node]  Theorem
      
      |- !cmp x l a b r.
             FMAPAL cmp (node l (a,b) r) ' x =
             case apto cmp x a of
               LESS => FMAPAL cmp l ' x
             | EQUAL => b
             | GREATER => FMAPAL cmp r ' x
   
   [FAPPLY_nt]  Theorem
      
      |- !cmp x. FMAPAL cmp nt ' x = FEMPTY ' x
   
   [FMAPAL_FDOM_THM]  Theorem
      
      |- (!cmp x. x IN FDOM (FMAPAL cmp nt) <=> F) /\
         !cmp x a b l r.
             x IN FDOM (FMAPAL cmp (node l (a,b) r)) <=>
             case apto cmp x a of
               LESS => x IN FDOM (FMAPAL cmp l)
             | EQUAL => T
             | GREATER => x IN FDOM (FMAPAL cmp r)
   
   [FMAPAL_fmap]  Theorem
      
      |- !cmp l. fmap l = FMAPAL cmp (list_to_bt (incr_sort cmp l))
   
   [FUN_fmap_thm]  Theorem
      
      |- !f l. fmap (MAP (\x. (x,f x)) l) = FUN_FMAP f (set l)
   
   [OPTION_FLAT]  Theorem
      
      |- (OPTION_FLAT [] = []) /\
         (!l. OPTION_FLAT (NONE::l) = OPTION_FLAT l) /\
         !l a. OPTION_FLAT (SOME a::l) = a ++ OPTION_FLAT l
   
   [OPTION_FLAT_ind]  Theorem
      
      |- !P.
             P [] /\ (!l. P l ==> P (NONE::l)) /\
             (!a l. P l ==> P (SOME a::l)) ==>
             !v. P v
   
   [ORL]  Theorem
      
      |- (!cmp. ORL cmp [] <=> T) /\
         !l cmp b a.
             ORL cmp ((a,b)::l) <=>
             ORL cmp l /\ !p q. MEM (p,q) l ==> (apto cmp a p = LESS)
   
   [ORL_DRESTRICT_COMPL_IMP]  Theorem
      
      |- !cmp l.
             ORL cmp l ==>
             !m.
                 OL cmp m ==>
                 ORL cmp (diff_merge cmp l m) /\
                 (fmap (diff_merge cmp l m) =
                  DRESTRICT (fmap l) (COMPL (set m)))
   
   [ORL_DRESTRICT_IMP]  Theorem
      
      |- !cmp l.
             ORL cmp l ==>
             !m.
                 OL cmp m ==>
                 ORL cmp (inter_merge cmp l m) /\
                 (fmap (inter_merge cmp l m) = DRESTRICT (fmap l) (set m))
   
   [ORL_FMAPAL]  Theorem
      
      |- !cmp l. ORL cmp l ==> (fmap l = FMAPAL cmp (list_to_bt l))
   
   [ORL_FUNION_IMP]  Theorem
      
      |- !cmp l.
             ORL cmp l ==>
             !m.
                 ORL cmp m ==>
                 ORL cmp (merge cmp l m) /\
                 (fmap (merge cmp l m) = fmap l FUNION fmap m)
   
   [ORL_bt]  Theorem
      
      |- (ORL_bt cmp nt <=> T) /\
         (ORL_bt cmp (node l (x,y) r) <=>
          ORL_bt_ub cmp l x /\ ORL_bt_lb cmp x r)
   
   [ORL_bt_ind]  Theorem
      
      |- !P.
             (!cmp. P cmp nt) /\ (!cmp l x y r. P cmp (node l (x,y) r)) ==>
             !v v1. P v v1
   
   [ORL_bt_lb]  Theorem
      
      |- (!lb cmp. ORL_bt_lb cmp lb nt <=> T) /\
         !y x r lb l cmp.
             ORL_bt_lb cmp lb (node l (x,y) r) <=>
             ORL_bt_lb_ub cmp lb l x /\ ORL_bt_lb cmp x r
   
   [ORL_bt_lb_ind]  Theorem
      
      |- !P.
             (!cmp lb. P cmp lb nt) /\
             (!cmp lb l x y r. P cmp x r ==> P cmp lb (node l (x,y) r)) ==>
             !v v1 v2. P v v1 v2
   
   [ORL_bt_lb_ub]  Theorem
      
      |- (!ub lb cmp. ORL_bt_lb_ub cmp lb nt ub <=> (apto cmp lb ub = LESS)) /\
         !y x ub r lb l cmp.
             ORL_bt_lb_ub cmp lb (node l (x,y) r) ub <=>
             ORL_bt_lb_ub cmp lb l x /\ ORL_bt_lb_ub cmp x r ub
   
   [ORL_bt_lb_ub_ind]  Theorem
      
      |- !P.
             (!cmp lb ub. P cmp lb nt ub) /\
             (!cmp lb l x y r ub.
                  P cmp lb l x /\ P cmp x r ub ==>
                  P cmp lb (node l (x,y) r) ub) ==>
             !v v1 v2 v3. P v v1 v2 v3
   
   [ORL_bt_ub]  Theorem
      
      |- (!ub cmp. ORL_bt_ub cmp nt ub <=> T) /\
         !y x ub r l cmp.
             ORL_bt_ub cmp (node l (x,y) r) ub <=>
             ORL_bt_ub cmp l x /\ ORL_bt_lb_ub cmp x r ub
   
   [ORL_bt_ub_ind]  Theorem
      
      |- !P.
             (!cmp ub. P cmp nt ub) /\
             (!cmp l x y r ub. P cmp l x ==> P cmp (node l (x,y) r) ub) ==>
             !v v1 v2. P v v1 v2
   
   [ORL_ind]  Theorem
      
      |- !P.
             (!cmp. P cmp []) /\ (!cmp a b l. P cmp l ==> P cmp ((a,b)::l)) ==>
             !v v1. P v v1
   
   [ORL_sublists]  Theorem
      
      |- (!cmp. ORL_sublists cmp [] <=> T) /\
         (!lol cmp. ORL_sublists cmp (NONE::lol) <=> ORL_sublists cmp lol) /\
         !m lol cmp.
             ORL_sublists cmp (SOME m::lol) <=>
             ORL cmp m /\ ORL_sublists cmp lol
   
   [ORL_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
   
   [ORWL_DRESTRICT_COMPL_THM]  Theorem
      
      |- !cmp s l t m.
             ORWL cmp s l /\ OWL cmp t m ==>
             ORWL cmp (DRESTRICT s (COMPL t)) (diff_merge cmp l m)
   
   [ORWL_DRESTRICT_THM]  Theorem
      
      |- !cmp s l t m.
             ORWL cmp s l /\ OWL cmp t m ==>
             ORWL cmp (DRESTRICT s t) (inter_merge cmp l m)
   
   [ORWL_FUNION_THM]  Theorem
      
      |- !cmp s l t m.
             ORWL cmp s l /\ ORWL cmp t m ==>
             ORWL cmp (s FUNION t) (merge cmp l m)
   
   [ORWL_bt_to_orl]  Theorem
      
      |- !cmp t. ORWL cmp (FMAPAL cmp t) (bt_to_orl cmp t)
   
   [assocv]  Theorem
      
      |- (!a. assocv [] a = NONE) /\
         !y x l a.
             assocv ((x,y)::l) a = if a = x then SOME y else assocv l a
   
   [assocv_ind]  Theorem
      
      |- !P.
             (!a. P [] a) /\
             (!x y l a. (a <> x ==> P l a) ==> P ((x,y)::l) a) ==>
             !v v1. P v v1
   
   [better_bt_to_orl]  Theorem
      
      |- !cmp t.
             bt_to_orl cmp t =
             if ORL_bt cmp t then bt_to_list_ac t []
             else bt_to_orl_ac cmp t []
   
   [bl_to_fmap]  Theorem
      
      |- (!cmp. bl_to_fmap cmp nbl = FEMPTY) /\
         (!cmp b. bl_to_fmap cmp (zerbl b) = bl_to_fmap cmp b) /\
         !y x t cmp b.
             bl_to_fmap cmp (onebl (x,y) t b) =
             OFU cmp
               (FEMPTY |+ (x,y) FUNION
                DRESTRICT (FMAPAL cmp t) {z | apto cmp x z = LESS})
               (bl_to_fmap cmp b)
   
   [bl_to_fmap_ind]  Theorem
      
      |- !P.
             (!cmp. P cmp nbl) /\ (!cmp b. P cmp b ==> P cmp (zerbl b)) /\
             (!cmp x y t b. P cmp b ==> P cmp (onebl (x,y) t b)) ==>
             !v v1. P v v1
   
   [bt_FST_FDOM]  Theorem
      
      |- !cmp t. FDOM (FMAPAL cmp t) = ENUMERAL cmp (bt_map FST t)
   
   [bt_rplacv_cn]  Theorem
      
      |- (!y x cn cmp. bt_rplacv_cn cmp (x,y) nt cn = nt) /\
         !z y x w r l cn cmp.
             bt_rplacv_cn cmp (x,y) (node l (w,z) r) cn =
             case apto cmp x w of
               LESS => bt_rplacv_cn cmp (x,y) l (\m. cn (node m (w,z) r))
             | EQUAL => cn (node l (x,y) r)
             | GREATER =>
               bt_rplacv_cn cmp (x,y) r (\m. cn (node l (w,z) m))
   
   [bt_rplacv_cn_ind]  Theorem
      
      |- !P.
             (!cmp x y cn. P cmp (x,y) nt cn) /\
             (!cmp x y l w z r cn.
                  ((apto cmp x w = GREATER) ==>
                   P cmp (x,y) r (\m. cn (node l (w,z) m))) /\
                  ((apto cmp x w = LESS) ==>
                   P cmp (x,y) l (\m. cn (node m (w,z) r))) ==>
                  P cmp (x,y) (node l (w,z) r) cn) ==>
             !v v1 v2 v3 v4. P v (v1,v2) v3 v4
   
   [bt_rplacv_thm]  Theorem
      
      |- !cmp x y t.
             (let
                ans = bt_rplacv_cn cmp (x,y) t (\m. m)
              in
                if ans = nt then x NOTIN FDOM (FMAPAL cmp t)
                else
                  x IN FDOM (FMAPAL cmp t) /\
                  (FMAPAL cmp t |+ (x,y) = FMAPAL cmp ans))
   
   [bt_to_fmap]  Theorem
      
      |- (!cmp. FMAPAL cmp nt = FEMPTY) /\
         !x v r l cmp.
             FMAPAL cmp (node l (x,v) r) =
             DRESTRICT (FMAPAL cmp l) {y | apto cmp y x = LESS} FUNION
             FEMPTY |+ (x,v) FUNION
             DRESTRICT (FMAPAL cmp r) {z | apto cmp x z = LESS}
   
   [bt_to_fmap_ind]  Theorem
      
      |- !P.
             (!cmp. P cmp nt) /\
             (!cmp l x v r. P cmp l /\ P cmp r ==> P cmp (node l (x,v) r)) ==>
             !v v1. P v v1
   
   [bt_to_orl]  Theorem
      
      |- (bt_to_orl cmp nt = []) /\
         (bt_to_orl cmp (node l (x,y) r) =
          bt_to_orl_ub cmp l x ++ [(x,y)] ++ bt_to_orl_lb cmp x r)
   
   [bt_to_orl_ID_IMP]  Theorem
      
      |- !cmp l. ORL cmp l ==> (bt_to_orl cmp (list_to_bt l) = l)
   
   [bt_to_orl_ac]  Theorem
      
      |- (bt_to_orl_ac cmp nt m = m) /\
         (bt_to_orl_ac cmp (node l (x,y) r) m =
          bt_to_orl_ub_ac cmp l x ((x,y)::bt_to_orl_lb_ac cmp x r m))
   
   [bt_to_orl_ac_ind]  Theorem
      
      |- !P.
             (!cmp m. P cmp nt m) /\
             (!cmp l x y r m. P cmp (node l (x,y) r) m) ==>
             !v v1 v2. P v v1 v2
   
   [bt_to_orl_ind]  Theorem
      
      |- !P.
             (!cmp. P cmp nt) /\ (!cmp l x y r. P cmp (node l (x,y) r)) ==>
             !v v1. P v v1
   
   [bt_to_orl_lb]  Theorem
      
      |- (!lb cmp. bt_to_orl_lb cmp lb nt = []) /\
         !y x r lb l cmp.
             bt_to_orl_lb cmp lb (node l (x,y) r) =
             if apto cmp lb x = LESS then
               bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++
               bt_to_orl_lb cmp x r
             else bt_to_orl_lb cmp lb r
   
   [bt_to_orl_lb_ac]  Theorem
      
      |- (!m lb cmp. bt_to_orl_lb_ac cmp lb nt m = m) /\
         !y x r m lb l cmp.
             bt_to_orl_lb_ac cmp lb (node l (x,y) r) m =
             if apto cmp lb x = LESS then
               bt_to_orl_lb_ub_ac cmp lb l x
                 ((x,y)::bt_to_orl_lb_ac cmp x r m)
             else bt_to_orl_lb_ac cmp lb r m
   
   [bt_to_orl_lb_ac_ind]  Theorem
      
      |- !P.
             (!cmp lb m. P cmp lb nt m) /\
             (!cmp lb l x y r m.
                  (apto cmp lb x <> LESS ==> P cmp lb r m) /\
                  ((apto cmp lb x = LESS) ==> P cmp x r m) ==>
                  P cmp lb (node l (x,y) r) m) ==>
             !v v1 v2 v3. P v v1 v2 v3
   
   [bt_to_orl_lb_ind]  Theorem
      
      |- !P.
             (!cmp lb. P cmp lb nt) /\
             (!cmp lb l x y r.
                  (apto cmp lb x <> LESS ==> P cmp lb r) /\
                  ((apto cmp lb x = LESS) ==> P cmp x r) ==>
                  P cmp lb (node l (x,y) r)) ==>
             !v v1 v2. P v v1 v2
   
   [bt_to_orl_lb_ub]  Theorem
      
      |- (!ub lb cmp. bt_to_orl_lb_ub cmp lb nt ub = []) /\
         !y x ub r lb l cmp.
             bt_to_orl_lb_ub cmp lb (node l (x,y) r) ub =
             if apto cmp lb x = LESS then
               if apto cmp x ub = LESS then
                 bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++
                 bt_to_orl_lb_ub cmp x r ub
               else bt_to_orl_lb_ub cmp lb l ub
             else bt_to_orl_lb_ub cmp lb r ub
   
   [bt_to_orl_lb_ub_ac]  Theorem
      
      |- (!ub m lb cmp. bt_to_orl_lb_ub_ac cmp lb nt ub m = m) /\
         !y x ub r m lb l cmp.
             bt_to_orl_lb_ub_ac cmp lb (node l (x,y) r) ub m =
             if apto cmp lb x = LESS then
               if apto cmp x ub = LESS then
                 bt_to_orl_lb_ub_ac cmp lb l x
                   ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)
               else bt_to_orl_lb_ub_ac cmp lb l ub m
             else bt_to_orl_lb_ub_ac cmp lb r ub m
   
   [bt_to_orl_lb_ub_ac_ind]  Theorem
      
      |- !P.
             (!cmp lb ub m. P cmp lb nt ub m) /\
             (!cmp lb l x y r ub m.
                  (apto cmp lb x <> LESS ==> P cmp lb r ub m) /\
                  ((apto cmp lb x = LESS) /\ apto cmp x ub <> LESS ==>
                   P cmp lb l ub m) /\
                  ((apto cmp lb x = LESS) /\ (apto cmp x ub = LESS) ==>
                   P cmp lb l x ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)) /\
                  ((apto cmp lb x = LESS) /\ (apto cmp x ub = LESS) ==>
                   P cmp x r ub m) ==>
                  P cmp lb (node l (x,y) r) ub m) ==>
             !v v1 v2 v3 v4. P v v1 v2 v3 v4
   
   [bt_to_orl_lb_ub_ind]  Theorem
      
      |- !P.
             (!cmp lb ub. P cmp lb nt ub) /\
             (!cmp lb l x y r ub.
                  (apto cmp lb x <> LESS ==> P cmp lb r ub) /\
                  ((apto cmp lb x = LESS) /\ apto cmp x ub <> LESS ==>
                   P cmp lb l ub) /\
                  ((apto cmp lb x = LESS) /\ (apto cmp x ub = LESS) ==>
                   P cmp lb l x) /\
                  ((apto cmp lb x = LESS) /\ (apto cmp x ub = LESS) ==>
                   P cmp x r ub) ==>
                  P cmp lb (node l (x,y) r) ub) ==>
             !v v1 v2 v3. P v v1 v2 v3
   
   [bt_to_orl_ub]  Theorem
      
      |- (!ub cmp. bt_to_orl_ub cmp nt ub = []) /\
         !y x ub r l cmp.
             bt_to_orl_ub cmp (node l (x,y) r) ub =
             if apto cmp x ub = LESS then
               bt_to_orl_ub cmp l x ++ [(x,y)] ++
               bt_to_orl_lb_ub cmp x r ub
             else bt_to_orl_ub cmp l ub
   
   [bt_to_orl_ub_ac]  Theorem
      
      |- (!ub m cmp. bt_to_orl_ub_ac cmp nt ub m = m) /\
         !y x ub r m l cmp.
             bt_to_orl_ub_ac cmp (node l (x,y) r) ub m =
             if apto cmp x ub = LESS then
               bt_to_orl_ub_ac cmp l x
                 ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)
             else bt_to_orl_ub_ac cmp l ub m
   
   [bt_to_orl_ub_ac_ind]  Theorem
      
      |- !P.
             (!cmp ub m. P cmp nt ub m) /\
             (!cmp l x y r ub m.
                  (apto cmp x ub <> LESS ==> P cmp l ub m) /\
                  ((apto cmp x ub = LESS) ==>
                   P cmp l x ((x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)) ==>
                  P cmp (node l (x,y) r) ub m) ==>
             !v v1 v2 v3. P v v1 v2 v3
   
   [bt_to_orl_ub_ind]  Theorem
      
      |- !P.
             (!cmp ub. P cmp nt ub) /\
             (!cmp l x y r ub.
                  (apto cmp x ub <> LESS ==> P cmp l ub) /\
                  ((apto cmp x ub = LESS) ==> P cmp l x) ==>
                  P cmp (node l (x,y) r) ub) ==>
             !v v1 v2. P v v1 v2
   
   [diff_merge]  Theorem
      
      |- (!cmp. diff_merge cmp [] [] = []) /\
         (!l cmp b a. diff_merge cmp ((a,b)::l) [] = (a,b)::l) /\
         (!y m cmp. diff_merge cmp [] (y::m) = []) /\
         !y m l cmp b a.
             diff_merge cmp ((a,b)::l) (y::m) =
             case apto cmp a y of
               LESS => (a,b)::diff_merge cmp l (y::m)
             | EQUAL => diff_merge cmp l m
             | GREATER => diff_merge cmp ((a,b)::l) m
   
   [diff_merge_ind]  Theorem
      
      |- !P.
             (!cmp. P cmp [] []) /\ (!cmp a b l. P cmp ((a,b)::l) []) /\
             (!cmp y m. P cmp [] (y::m)) /\
             (!cmp a b l y m.
                  ((apto cmp a y = EQUAL) ==> P cmp l m) /\
                  ((apto cmp a y = GREATER) ==> P cmp ((a,b)::l) m) /\
                  ((apto cmp a y = LESS) ==> P cmp l (y::m)) ==>
                  P cmp ((a,b)::l) (y::m)) ==>
             !v v1 v2. P v v1 v2
   
   [fmap_FDOM]  Theorem
      
      |- !l. FDOM (fmap l) = set (MAP FST l)
   
   [fmap_FDOM_rec]  Theorem
      
      |- (!x. x IN FDOM (fmap []) <=> F) /\
         !x w z l.
             x IN FDOM (fmap ((w,z)::l)) <=> (x = w) \/ x IN FDOM (fmap l)
   
   [fmap_ORWL_thm]  Theorem
      
      |- !cmp l. ORWL cmp (fmap l) (incr_sort cmp l)
   
   [incr_merge]  Theorem
      
      |- (!l cmp. incr_merge cmp l [] = [SOME l]) /\
         (!lol l cmp. incr_merge cmp l (NONE::lol) = SOME l::lol) /\
         !m lol l cmp.
             incr_merge cmp l (SOME m::lol) =
             NONE::incr_merge cmp (merge cmp l m) lol
   
   [incr_merge_ind]  Theorem
      
      |- !P.
             (!cmp l. P cmp l []) /\ (!cmp l lol. P cmp l (NONE::lol)) /\
             (!cmp l m lol.
                  P cmp (merge cmp l m) lol ==> P cmp l (SOME m::lol)) ==>
             !v v1 v2. P v v1 v2
   
   [inter_merge]  Theorem
      
      |- (!cmp. inter_merge cmp [] [] = []) /\
         (!l cmp b a. inter_merge cmp ((a,b)::l) [] = []) /\
         (!y m cmp. inter_merge cmp [] (y::m) = []) /\
         !y m l cmp b a.
             inter_merge cmp ((a,b)::l) (y::m) =
             case apto cmp a y of
               LESS => inter_merge cmp l (y::m)
             | EQUAL => (a,b)::inter_merge cmp l m
             | GREATER => inter_merge cmp ((a,b)::l) m
   
   [inter_merge_ind]  Theorem
      
      |- !P.
             (!cmp. P cmp [] []) /\ (!cmp a b l. P cmp ((a,b)::l) []) /\
             (!cmp y m. P cmp [] (y::m)) /\
             (!cmp a b l y m.
                  ((apto cmp a y = EQUAL) ==> P cmp l m) /\
                  ((apto cmp a y = GREATER) ==> P cmp ((a,b)::l) m) /\
                  ((apto cmp a y = LESS) ==> P cmp l (y::m)) ==>
                  P cmp ((a,b)::l) (y::m)) ==>
             !v v1 v2. P v v1 v2
   
   [list_rplacv_cn]  Theorem
      
      |- (!y x cn. list_rplacv_cn (x,y) [] cn = []) /\
         !z y x w l cn.
             list_rplacv_cn (x,y) ((w,z)::l) cn =
             if x = w then cn ((x,y)::l)
             else list_rplacv_cn (x,y) l (\m. cn ((w,z)::m))
   
   [list_rplacv_cn_ind]  Theorem
      
      |- !P.
             (!x y cn. P (x,y) [] cn) /\
             (!x y w z l cn.
                  (x <> w ==> P (x,y) l (\m. cn ((w,z)::m))) ==>
                  P (x,y) ((w,z)::l) cn) ==>
             !v v1 v2 v3. P (v,v1) v2 v3
   
   [list_rplacv_thm]  Theorem
      
      |- !x y l.
             (let
                ans = list_rplacv_cn (x,y) l (\m. m)
              in
                if ans = [] then x NOTIN FDOM (fmap l)
                else x IN FDOM (fmap l) /\ (fmap l |+ (x,y) = fmap ans))
   
   [merge]  Theorem
      
      |- (!l cmp. merge cmp [] l = l) /\
         (!v5 v4 cmp. merge cmp (v4::v5) [] = v4::v5) /\
         !l2 l1 cmp b2 b1 a2 a1.
             merge cmp ((a1,b1)::l1) ((a2,b2)::l2) =
             case apto cmp a1 a2 of
               LESS => (a1,b1)::merge cmp l1 ((a2,b2)::l2)
             | EQUAL => (a1,b1)::merge cmp l1 l2
             | GREATER => (a2,b2)::merge cmp ((a1,b1)::l1) l2
   
   [merge_ind]  Theorem
      
      |- !P.
             (!cmp l. P cmp [] l) /\ (!cmp v4 v5. P cmp (v4::v5) []) /\
             (!cmp a1 b1 l1 a2 b2 l2.
                  ((apto cmp a1 a2 = EQUAL) ==> P cmp l1 l2) /\
                  ((apto cmp a1 a2 = GREATER) ==> P cmp ((a1,b1)::l1) l2) /\
                  ((apto cmp a1 a2 = LESS) ==> P cmp l1 ((a2,b2)::l2)) ==>
                  P cmp ((a1,b1)::l1) ((a2,b2)::l2)) ==>
             !v v1 v2. P v v1 v2
   
   [merge_out]  Theorem
      
      |- (!l cmp. merge_out cmp l [] = l) /\
         (!lol l cmp. merge_out cmp l (NONE::lol) = merge_out cmp l lol) /\
         !m lol l cmp.
             merge_out cmp l (SOME m::lol) =
             merge_out cmp (merge cmp l m) lol
   
   [merge_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 (merge cmp l m) lol ==> P cmp l (SOME m::lol)) ==>
             !v v1 v2. P v v1 v2
   
   [o_f_bt_map]  Theorem
      
      |- !cmp f t. f o_f FMAPAL cmp t = FMAPAL cmp (bt_map (AP_SND f) t)
   
   [o_f_fmap]  Theorem
      
      |- !f l. f o_f fmap l = fmap (MAP (AP_SND f) l)
   
   [optry_list]  Theorem
      
      |- (!f. optry_list f [] = NONE) /\
         (!l f. optry_list f (NONE::l) = optry_list f l) /\
         !z l f. optry_list f (SOME z::l) = optry (f z) (optry_list f l)
   
   [optry_list_ind]  Theorem
      
      |- !P.
             (!f. P f []) /\ (!f l. P f l ==> P f (NONE::l)) /\
             (!f z l. P f l ==> P f (SOME z::l)) ==>
             !v v1. P v v1
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13