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 ORL_bt_curried : thm
    val ORL_bt_lb_curried : thm
    val ORL_bt_lb_tupled_primitive : thm
    val ORL_bt_lb_ub_curried : thm
    val ORL_bt_lb_ub_tupled_primitive : thm
    val ORL_bt_tupled_primitive : thm
    val ORL_bt_ub_curried : thm
    val ORL_bt_ub_tupled_primitive : thm
    val ORL_curried : thm
    val ORL_sublists_curried : thm
    val ORL_sublists_tupled_primitive : thm
    val ORL_tupled_primitive : thm
    val ORWL : thm
    val UFO : thm
    val assocv_curried : thm
    val assocv_tupled_primitive : thm
    val bl_to_fmap_curried : thm
    val bl_to_fmap_tupled_primitive : thm
    val bt_map : thm
    val bt_rplacv_cn_curried : thm
    val bt_rplacv_cn_tupled_primitive : thm
    val bt_to_fmap_curried : thm
    val bt_to_fmap_lb : thm
    val bt_to_fmap_lb_ub : thm
    val bt_to_fmap_tupled_primitive : thm
    val bt_to_fmap_ub : thm
    val bt_to_orl_ac_curried : thm
    val bt_to_orl_ac_tupled_primitive : thm
    val bt_to_orl_curried : thm
    val bt_to_orl_lb_ac_curried : thm
    val bt_to_orl_lb_ac_tupled_primitive : thm
    val bt_to_orl_lb_curried : thm
    val bt_to_orl_lb_tupled_primitive : thm
    val bt_to_orl_lb_ub_ac_curried : thm
    val bt_to_orl_lb_ub_ac_tupled_AUX : thm
    val bt_to_orl_lb_ub_ac_tupled_primitive : thm
    val bt_to_orl_lb_ub_curried : thm
    val bt_to_orl_lb_ub_tupled_primitive : thm
    val bt_to_orl_tupled_primitive : thm
    val bt_to_orl_ub_ac_curried : thm
    val bt_to_orl_ub_ac_tupled_primitive : thm
    val bt_to_orl_ub_curried : thm
    val bt_to_orl_ub_tupled_primitive : thm
    val diff_merge_curried : thm
    val diff_merge_tupled_primitive : thm
    val fmap : thm
    val incr_build : thm
    val incr_flat : thm
    val incr_merge_curried : thm
    val incr_merge_tupled_primitive : thm
    val incr_sort : thm
    val inter_merge_curried : thm
    val inter_merge_tupled_primitive : thm
    val list_rplacv_cn_curried : thm
    val list_rplacv_cn_tupled_primitive : thm
    val merge_curried : thm
    val merge_out_curried : thm
    val merge_out_tupled_primitive : thm
    val merge_tupled_primitive : thm
    val optry : thm
    val optry_list_curried : thm
    val optry_list_tupled_primitive : 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)

   [ORL_bt_curried]  Definition

      |- !x x1. ORL_bt x x1 <=> ORL_bt_tupled (x,x1)

   [ORL_bt_lb_curried]  Definition

      |- !x x1 x2. ORL_bt_lb x x1 x2 <=> ORL_bt_lb_tupled (x,x1,x2)

   [ORL_bt_lb_tupled_primitive]  Definition

      |- ORL_bt_lb_tupled =
         WFREC
           (@R.
              WF R /\ !y l lb r x cmp. R (cmp,x,r) (cmp,lb,node l (x,y) r))
           (\ORL_bt_lb_tupled a.
              case a of
                (cmp,lb,nt) => I T
              | (cmp,lb,node l (x,y) r) =>
                  I
                    (ORL_bt_lb_ub cmp lb l x /\
                     ORL_bt_lb_tupled (cmp,x,r)))

   [ORL_bt_lb_ub_curried]  Definition

      |- !x x1 x2 x3.
           ORL_bt_lb_ub x x1 x2 x3 <=> ORL_bt_lb_ub_tupled (x,x1,x2,x3)

   [ORL_bt_lb_ub_tupled_primitive]  Definition

      |- ORL_bt_lb_ub_tupled =
         WFREC
           (@R.
              WF R /\
              (!ub r y x l lb cmp.
                 R (cmp,lb,l,x) (cmp,lb,node l (x,y) r,ub)) /\
              !y l lb ub r x cmp.
                R (cmp,x,r,ub) (cmp,lb,node l (x,y) r,ub))
           (\ORL_bt_lb_ub_tupled a.
              case a of
                (cmp,lb,nt,ub) => I (apto cmp lb ub = LESS)
              | (cmp,lb,node l (x,y) r,ub) =>
                  I
                    (ORL_bt_lb_ub_tupled (cmp,lb,l,x) /\
                     ORL_bt_lb_ub_tupled (cmp,x,r,ub)))

   [ORL_bt_tupled_primitive]  Definition

      |- ORL_bt_tupled =
         WFREC (@R. WF R)
           (\ORL_bt_tupled a.
              case a of
                (cmp,nt) => I T
              | (cmp,node l (x,y) r) =>
                  I (ORL_bt_ub cmp l x /\ ORL_bt_lb cmp x r))

   [ORL_bt_ub_curried]  Definition

      |- !x x1 x2. ORL_bt_ub x x1 x2 <=> ORL_bt_ub_tupled (x,x1,x2)

   [ORL_bt_ub_tupled_primitive]  Definition

      |- ORL_bt_ub_tupled =
         WFREC
           (@R.
              WF R /\ !ub r y x l cmp. R (cmp,l,x) (cmp,node l (x,y) r,ub))
           (\ORL_bt_ub_tupled a.
              case a of
                (cmp,nt,ub) => I T
              | (cmp,node l (x,y) r,ub) =>
                  I
                    (ORL_bt_ub_tupled (cmp,l,x) /\
                     ORL_bt_lb_ub cmp x r ub))

   [ORL_curried]  Definition

      |- !x x1. ORL x x1 <=> ORL_tupled (x,x1)

   [ORL_sublists_curried]  Definition

      |- !x x1. ORL_sublists x x1 <=> ORL_sublists_tupled (x,x1)

   [ORL_sublists_tupled_primitive]  Definition

      |- ORL_sublists_tupled =
         WFREC
           (@R.
              WF R /\ (!lol cmp. R (cmp,lol) (cmp,NONE::lol)) /\
              !m lol cmp. R (cmp,lol) (cmp,SOME m::lol))
           (\ORL_sublists_tupled a.
              case a of
                (cmp,[]) => I T
              | (cmp,NONE::lol) => I (ORL_sublists_tupled (cmp,lol))
              | (cmp,SOME m::lol) =>
                  I (ORL cmp m /\ ORL_sublists_tupled (cmp,lol)))

   [ORL_tupled_primitive]  Definition

      |- ORL_tupled =
         WFREC (@R. WF R /\ !b a l cmp. R (cmp,l) (cmp,(a,b)::l))
           (\ORL_tupled a'.
              case a' of
                (cmp,[]) => I T
              | (cmp,(a,b)::l) =>
                  I
                    (ORL_tupled (cmp,l) /\
                     !p q. MEM (p,q) l ==> (apto cmp a p = LESS)))

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

   [assocv_curried]  Definition

      |- !x x1. assocv x x1 = assocv_tupled (x,x1)

   [assocv_tupled_primitive]  Definition

      |- assocv_tupled =
         WFREC (@R. WF R /\ !y l x a. a <> x ==> R (l,a) ((x,y)::l,a))
           (\assocv_tupled a'.
              case a' of
                ([],a) => I NONE
              | ((x,y)::l,a) =>
                  I (if a = x then SOME y else assocv_tupled (l,a)))

   [bl_to_fmap_curried]  Definition

      |- !x x1. bl_to_fmap x x1 = bl_to_fmap_tupled (x,x1)

   [bl_to_fmap_tupled_primitive]  Definition

      |- bl_to_fmap_tupled =
         WFREC
           (@R.
              WF R /\ (!b cmp. R (cmp,b) (cmp,zerbl b)) /\
              !t y x b cmp. R (cmp,b) (cmp,onebl (x,y) t b))
           (\bl_to_fmap_tupled a.
              case a of
                (cmp,nbl) => I FEMPTY
              | (cmp,zerbl b) => I (bl_to_fmap_tupled (cmp,b))
              | (cmp,onebl (x,y) t b') =>
                  I
                    (OFU cmp
                       (FEMPTY |+ (x,y) FUNION
                        DRESTRICT (FMAPAL cmp t) {z | apto cmp x z = LESS})
                       (bl_to_fmap_tupled (cmp,b'))))

   [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_rplacv_cn_curried]  Definition

      |- !x x1 x2 x3.
           bt_rplacv_cn x x1 x2 x3 = bt_rplacv_cn_tupled (x,x1,x2,x3)

   [bt_rplacv_cn_tupled_primitive]  Definition

      |- bt_rplacv_cn_tupled =
         WFREC
           (@R.
              WF R /\
              (!z l cn r y w x cmp.
                 (apto cmp x w = GREATER) ==>
                 R (cmp,(x,y),r,(\m. cn (node l (w,z) m)))
                   (cmp,(x,y),node l (w,z) r,cn)) /\
              !r z cn l y w x cmp.
                (apto cmp x w = LESS) ==>
                R (cmp,(x,y),l,(\m. cn (node m (w,z) r)))
                  (cmp,(x,y),node l (w,z) r,cn))
           (\bt_rplacv_cn_tupled a.
              case a of
                (cmp,(x,y),nt,cn) => I nt
              | (cmp,(x,y),node l (w,z) r,cn) =>
                  I
                    (case apto cmp x w of
                       LESS =>
                         bt_rplacv_cn_tupled
                           (cmp,(x,y),l,(\m. cn (node m (w,z) r)))
                     | EQUAL => cn (node l (x,y) r)
                     | GREATER =>
                         bt_rplacv_cn_tupled
                           (cmp,(x,y),r,(\m. cn (node l (w,z) m)))))

   [bt_to_fmap_curried]  Definition

      |- !x x1. FMAPAL x x1 = bt_to_fmap_tupled (x,x1)

   [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_tupled_primitive]  Definition

      |- bt_to_fmap_tupled =
         WFREC
           (@R.
              WF R /\ (!r v x l cmp. R (cmp,l) (cmp,node l (x,v) r)) /\
              !v x l r cmp. R (cmp,r) (cmp,node l (x,v) r))
           (\bt_to_fmap_tupled a.
              case a of
                (cmp,nt) => I FEMPTY
              | (cmp,node l (x,v) r) =>
                  I
                    (DRESTRICT (bt_to_fmap_tupled (cmp,l))
                       {y | apto cmp y x = LESS} FUNION
                     FEMPTY |+ (x,v) FUNION
                     DRESTRICT (bt_to_fmap_tupled (cmp,r))
                       {z | apto cmp x z = 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_ac_curried]  Definition

      |- !x x1 x2. bt_to_orl_ac x x1 x2 = bt_to_orl_ac_tupled (x,x1,x2)

   [bt_to_orl_ac_tupled_primitive]  Definition

      |- bt_to_orl_ac_tupled =
         WFREC (@R. WF R)
           (\bt_to_orl_ac_tupled a.
              case a of
                (cmp,nt,m) => I m
              | (cmp,node l (x,y) r,m) =>
                  I
                    (bt_to_orl_ub_ac cmp l x
                       ((x,y)::bt_to_orl_lb_ac cmp x r m)))

   [bt_to_orl_curried]  Definition

      |- !x x1. bt_to_orl x x1 = bt_to_orl_tupled (x,x1)

   [bt_to_orl_lb_ac_curried]  Definition

      |- !x x1 x2 x3.
           bt_to_orl_lb_ac x x1 x2 x3 = bt_to_orl_lb_ac_tupled (x,x1,x2,x3)

   [bt_to_orl_lb_ac_tupled_primitive]  Definition

      |- bt_to_orl_lb_ac_tupled =
         WFREC
           (@R.
              WF R /\
              (!y l m r x lb cmp.
                 apto cmp lb x <> LESS ==>
                 R (cmp,lb,r,m) (cmp,lb,node l (x,y) r,m)) /\
              !y l m r x lb cmp.
                (apto cmp lb x = LESS) ==>
                R (cmp,x,r,m) (cmp,lb,node l (x,y) r,m))
           (\bt_to_orl_lb_ac_tupled a.
              case a of
                (cmp,lb,nt,m) => I m
              | (cmp,lb,node l (x,y) r,m) =>
                  I
                    (if apto cmp lb x = LESS then
                       bt_to_orl_lb_ub_ac cmp lb l x
                         ((x,y)::bt_to_orl_lb_ac_tupled (cmp,x,r,m))
                     else bt_to_orl_lb_ac_tupled (cmp,lb,r,m)))

   [bt_to_orl_lb_curried]  Definition

      |- !x x1 x2. bt_to_orl_lb x x1 x2 = bt_to_orl_lb_tupled (x,x1,x2)

   [bt_to_orl_lb_tupled_primitive]  Definition

      |- bt_to_orl_lb_tupled =
         WFREC
           (@R.
              WF R /\
              (!y l r x lb cmp.
                 apto cmp lb x <> LESS ==>
                 R (cmp,lb,r) (cmp,lb,node l (x,y) r)) /\
              !y l r x lb cmp.
                (apto cmp lb x = LESS) ==>
                R (cmp,x,r) (cmp,lb,node l (x,y) r))
           (\bt_to_orl_lb_tupled a.
              case a of
                (cmp,lb,nt) => I []
              | (cmp,lb,node l (x,y) r) =>
                  I
                    (if apto cmp lb x = LESS then
                       bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++
                       bt_to_orl_lb_tupled (cmp,x,r)
                     else bt_to_orl_lb_tupled (cmp,lb,r)))

   [bt_to_orl_lb_ub_ac_curried]  Definition

      |- !x x1 x2 x3 x4.
           bt_to_orl_lb_ub_ac x x1 x2 x3 x4 =
           bt_to_orl_lb_ub_ac_tupled (x,x1,x2,x3,x4)

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

   [bt_to_orl_lb_ub_ac_tupled_primitive]  Definition

      |- bt_to_orl_lb_ub_ac_tupled =
         bt_to_orl_lb_ub_ac_tupled_aux
           (@R.
              WF R /\
              (!y l m ub r x lb cmp.
                 apto cmp lb x <> LESS ==>
                 R (cmp,lb,r,ub,m) (cmp,lb,node l (x,y) r,ub,m)) /\
              (!r y m l ub x lb cmp.
                 (apto cmp lb x = LESS) /\ apto cmp x ub <> LESS ==>
                 R (cmp,lb,l,ub,m) (cmp,lb,node l (x,y) r,ub,m)) /\
              (!m r y l ub x lb cmp.
                 (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS) ==>
                 R
                   (cmp,lb,l,x,
                    (x,y)::bt_to_orl_lb_ub_ac_tupled_aux R (cmp,x,r,ub,m))
                   (cmp,lb,node l (x,y) r,ub,m)) /\
              !y l m r ub x lb cmp.
                (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS) ==>
                R (cmp,x,r,ub,m) (cmp,lb,node l (x,y) r,ub,m))

   [bt_to_orl_lb_ub_curried]  Definition

      |- !x x1 x2 x3.
           bt_to_orl_lb_ub x x1 x2 x3 = bt_to_orl_lb_ub_tupled (x,x1,x2,x3)

   [bt_to_orl_lb_ub_tupled_primitive]  Definition

      |- bt_to_orl_lb_ub_tupled =
         WFREC
           (@R.
              WF R /\
              (!y l ub r x lb cmp.
                 apto cmp lb x <> LESS ==>
                 R (cmp,lb,r,ub) (cmp,lb,node l (x,y) r,ub)) /\
              (!r y l ub x lb cmp.
                 (apto cmp lb x = LESS) /\ apto cmp x ub <> LESS ==>
                 R (cmp,lb,l,ub) (cmp,lb,node l (x,y) r,ub)) /\
              (!r y l ub x lb cmp.
                 (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS) ==>
                 R (cmp,lb,l,x) (cmp,lb,node l (x,y) r,ub)) /\
              !y l r ub x lb cmp.
                (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS) ==>
                R (cmp,x,r,ub) (cmp,lb,node l (x,y) r,ub))
           (\bt_to_orl_lb_ub_tupled a.
              case a of
                (cmp,lb,nt,ub) => I []
              | (cmp,lb,node l (x,y) r,ub) =>
                  I
                    (if apto cmp lb x = LESS then
                       if apto cmp x ub = LESS then
                         bt_to_orl_lb_ub_tupled (cmp,lb,l,x) ++ [(x,y)] ++
                         bt_to_orl_lb_ub_tupled (cmp,x,r,ub)
                       else bt_to_orl_lb_ub_tupled (cmp,lb,l,ub)
                     else bt_to_orl_lb_ub_tupled (cmp,lb,r,ub)))

   [bt_to_orl_tupled_primitive]  Definition

      |- bt_to_orl_tupled =
         WFREC (@R. WF R)
           (\bt_to_orl_tupled a.
              case a of
                (cmp,nt) => I []
              | (cmp,node l (x,y) r) =>
                  I
                    (bt_to_orl_ub cmp l x ++ [(x,y)] ++
                     bt_to_orl_lb cmp x r))

   [bt_to_orl_ub_ac_curried]  Definition

      |- !x x1 x2 x3.
           bt_to_orl_ub_ac x x1 x2 x3 = bt_to_orl_ub_ac_tupled (x,x1,x2,x3)

   [bt_to_orl_ub_ac_tupled_primitive]  Definition

      |- bt_to_orl_ub_ac_tupled =
         WFREC
           (@R.
              WF R /\
              (!r y m l ub x cmp.
                 apto cmp x ub <> LESS ==>
                 R (cmp,l,ub,m) (cmp,node l (x,y) r,ub,m)) /\
              !m r y l ub x cmp.
                (apto cmp x ub = LESS) ==>
                R (cmp,l,x,(x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)
                  (cmp,node l (x,y) r,ub,m))
           (\bt_to_orl_ub_ac_tupled a.
              case a of
                (cmp,nt,ub,m) => I m
              | (cmp,node l (x,y) r,ub,m) =>
                  I
                    (if apto cmp x ub = LESS then
                       bt_to_orl_ub_ac_tupled
                         (cmp,l,x,(x,y)::bt_to_orl_lb_ub_ac cmp x r ub m)
                     else bt_to_orl_ub_ac_tupled (cmp,l,ub,m)))

   [bt_to_orl_ub_curried]  Definition

      |- !x x1 x2. bt_to_orl_ub x x1 x2 = bt_to_orl_ub_tupled (x,x1,x2)

   [bt_to_orl_ub_tupled_primitive]  Definition

      |- bt_to_orl_ub_tupled =
         WFREC
           (@R.
              WF R /\
              (!r y l ub x cmp.
                 apto cmp x ub <> LESS ==>
                 R (cmp,l,ub) (cmp,node l (x,y) r,ub)) /\
              !r y l ub x cmp.
                (apto cmp x ub = LESS) ==>
                R (cmp,l,x) (cmp,node l (x,y) r,ub))
           (\bt_to_orl_ub_tupled a.
              case a of
                (cmp,nt,ub) => I []
              | (cmp,node l (x,y) r,ub) =>
                  I
                    (if apto cmp x ub = LESS then
                       bt_to_orl_ub_tupled (cmp,l,x) ++ [(x,y)] ++
                       bt_to_orl_lb_ub cmp x r ub
                     else bt_to_orl_ub_tupled (cmp,l,ub)))

   [diff_merge_curried]  Definition

      |- !x x1 x2. diff_merge x x1 x2 = diff_merge_tupled (x,x1,x2)

   [diff_merge_tupled_primitive]  Definition

      |- diff_merge_tupled =
         WFREC
           (@R.
              WF R /\
              (!b m l y a cmp.
                 (apto cmp a y = EQUAL) ==>
                 R (cmp,l,m) (cmp,(a,b)::l,y::m)) /\
              (!m l b y a cmp.
                 (apto cmp a y = GREATER) ==>
                 R (cmp,(a,b)::l,m) (cmp,(a,b)::l,y::m)) /\
              !b m l y a cmp.
                (apto cmp a y = LESS) ==>
                R (cmp,l,y::m) (cmp,(a,b)::l,y::m))
           (\diff_merge_tupled a'.
              case a' of
                (cmp,[],v3) => I []
              | (cmp,(a,b)::l,[]) => I ((a,b)::l)
              | (cmp,(a,b)::l,y::m) =>
                  I
                    (case apto cmp a y of
                       LESS => (a,b)::diff_merge_tupled (cmp,l,y::m)
                     | EQUAL => diff_merge_tupled (cmp,l,m)
                     | GREATER => diff_merge_tupled (cmp,(a,b)::l,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_merge_curried]  Definition

      |- !x x1 x2. incr_merge x x1 x2 = incr_merge_tupled (x,x1,x2)

   [incr_merge_tupled_primitive]  Definition

      |- incr_merge_tupled =
         WFREC
           (@R.
              WF R /\
              !lol m l cmp. R (cmp,merge cmp l m,lol) (cmp,l,SOME m::lol))
           (\incr_merge_tupled a.
              case a of
                (cmp,l,[]) => I [SOME l]
              | (cmp,l,NONE::lol) => I (SOME l::lol)
              | (cmp,l,SOME m::lol) =>
                  I (NONE::incr_merge_tupled (cmp,merge cmp l m,lol)))

   [incr_sort]  Definition

      |- !cmp l. incr_sort cmp l = merge_out cmp [] (incr_build cmp l)

   [inter_merge_curried]  Definition

      |- !x x1 x2. inter_merge x x1 x2 = inter_merge_tupled (x,x1,x2)

   [inter_merge_tupled_primitive]  Definition

      |- inter_merge_tupled =
         WFREC
           (@R.
              WF R /\
              (!b m l y a cmp.
                 (apto cmp a y = EQUAL) ==>
                 R (cmp,l,m) (cmp,(a,b)::l,y::m)) /\
              (!m l b y a cmp.
                 (apto cmp a y = GREATER) ==>
                 R (cmp,(a,b)::l,m) (cmp,(a,b)::l,y::m)) /\
              !b m l y a cmp.
                (apto cmp a y = LESS) ==>
                R (cmp,l,y::m) (cmp,(a,b)::l,y::m))
           (\inter_merge_tupled a'.
              case a' of
                (cmp,(a,b)::l,y::m) =>
                  I
                    (case apto cmp a y of
                       LESS => inter_merge_tupled (cmp,l,y::m)
                     | EQUAL => (a,b)::inter_merge_tupled (cmp,l,m)
                     | GREATER => inter_merge_tupled (cmp,(a,b)::l,m))
              | _ => I [])

   [list_rplacv_cn_curried]  Definition

      |- !x x1 x2. list_rplacv_cn x x1 x2 = list_rplacv_cn_tupled (x,x1,x2)

   [list_rplacv_cn_tupled_primitive]  Definition

      |- list_rplacv_cn_tupled =
         WFREC
           (@R.
              WF R /\
              !z cn l y w x.
                x <> w ==>
                R ((x,y),l,(\m. cn ((w,z)::m))) ((x,y),(w,z)::l,cn))
           (\list_rplacv_cn_tupled a.
              case a of
                ((x,y),[],cn) => I []
              | ((x,y),(w,z)::l,cn) =>
                  I
                    (if x = w then cn ((x,y)::l)
                     else
                       list_rplacv_cn_tupled
                         ((x,y),l,(\m. cn ((w,z)::m)))))

   [merge_curried]  Definition

      |- !x x1 x2. merge x x1 x2 = merge_tupled (x,x1,x2)

   [merge_out_curried]  Definition

      |- !x x1 x2. merge_out x x1 x2 = merge_out_tupled (x,x1,x2)

   [merge_out_tupled_primitive]  Definition

      |- merge_out_tupled =
         WFREC
           (@R.
              WF R /\ (!lol l cmp. R (cmp,l,lol) (cmp,l,NONE::lol)) /\
              !lol m l cmp. R (cmp,merge cmp l m,lol) (cmp,l,SOME m::lol))
           (\merge_out_tupled a.
              case a of
                (cmp,l,[]) => I l
              | (cmp,l,NONE::lol) => I (merge_out_tupled (cmp,l,lol))
              | (cmp,l,SOME m::lol) =>
                  I (merge_out_tupled (cmp,merge cmp l m,lol)))

   [merge_tupled_primitive]  Definition

      |- merge_tupled =
         WFREC
           (@R.
              WF R /\
              (!b2 b1 l2 l1 a2 a1 cmp.
                 (apto cmp a1 a2 = EQUAL) ==>
                 R (cmp,l1,l2) (cmp,(a1,b1)::l1,(a2,b2)::l2)) /\
              (!b2 l2 l1 b1 a2 a1 cmp.
                 (apto cmp a1 a2 = GREATER) ==>
                 R (cmp,(a1,b1)::l1,l2) (cmp,(a1,b1)::l1,(a2,b2)::l2)) /\
              !b1 l2 b2 l1 a2 a1 cmp.
                (apto cmp a1 a2 = LESS) ==>
                R (cmp,l1,(a2,b2)::l2) (cmp,(a1,b1)::l1,(a2,b2)::l2))
           (\merge_tupled a.
              case a of
                (cmp,[],l) => I l
              | (cmp,v6::l1,[]) => I (v6::l1)
              | (cmp,(a1,b1)::l1,(a2,b2)::l2) =>
                  I
                    (case apto cmp a1 a2 of
                       LESS => (a1,b1)::merge_tupled (cmp,l1,(a2,b2)::l2)
                     | EQUAL => (a1,b1)::merge_tupled (cmp,l1,l2)
                     | GREATER =>
                         (a2,b2)::merge_tupled (cmp,(a1,b1)::l1,l2)))

   [optry]  Definition

      |- (!p q. optry (SOME p) q = SOME p) /\ !q. optry NONE q = q

   [optry_list_curried]  Definition

      |- !x x1. optry_list x x1 = optry_list_tupled (x,x1)

   [optry_list_tupled_primitive]  Definition

      |- optry_list_tupled =
         WFREC
           (@R.
              WF R /\ (!l f. R (f,l) (f,NONE::l)) /\
              !z l f. R (f,l) (f,SOME z::l))
           (\optry_list_tupled a.
              case a of
                (f,[]) => I NONE
              | (f,NONE::l) => I (optry_list_tupled (f,l))
              | (f,SOME z::l) => I (optry (f z) (optry_list_tupled (f,l))))

   [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-10