Theory fmapal

|- !f a b. AP_SND f (a,b) = (a,f b)

|- !cmp f g.
     OFU cmp f g = DRESTRICT f {x | LESS_ALL cmp x (FDOM g)} FUNION g

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

|- !f g x. OPTION_UPDATE f g x = optry (f x) (g x)

|- !cmp f l. ORWL cmp f l <=> (f = fmap l) /\ ORL cmp l

|- !cmp f g.
     UFO cmp f g =
     f FUNION DRESTRICT g {y | (!z. z IN FDOM f ==> (apto cmp z y = LESS))}

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

|- !cmp lb t.
     bt_to_fmap_lb cmp lb t =
     DRESTRICT (FMAPAL cmp t) {x | apto cmp lb x = LESS}

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

|- !cmp t ub.
     bt_to_fmap_ub cmp t ub =
     DRESTRICT (FMAPAL cmp t) {x | apto cmp x ub = LESS}

|- !l. fmap l = FEMPTY |++ REVERSE l

|- (!cmp. incr_build cmp [] = []) /\
   !cmp ab l.
     incr_build cmp (ab::l) = incr_merge cmp [ab] (incr_build cmp l)

|- !cmp lol. incr_flat cmp lol = merge_out cmp [] lol

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

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

|- !f. unlookup f = FUN_FMAP (THE o f) (IS_SOME o f)

|- !a l. vcossa a l = assocv l a

|- !x y z l.
     FAPPLY (fmap ((y,z)::l)) x = if x = y then z else FAPPLY (fmap l) x

|- !x. FAPPLY (fmap []) x = FAPPLY FEMPTY x

|- !cmp x l a b r.
     FAPPLY (FMAPAL cmp (node l (a,b) r)) x =
     case apto cmp x a of
       LESS => FAPPLY (FMAPAL cmp l) x
     | EQUAL => b
     | GREATER => FAPPLY (FMAPAL cmp r) x

|- !cmp x. FAPPLY (FMAPAL cmp nt) x = FAPPLY FEMPTY x

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

|- !cmp l. fmap l = FMAPAL cmp (list_to_bt (incr_sort cmp l))

|- !f l. fmap (MAP (\x. (x,f x)) l) = FUN_FMAP f (set l)

|- (OPTION_FLAT [] = []) /\ (!l. OPTION_FLAT (NONE::l) = OPTION_FLAT l) /\
   !l a. OPTION_FLAT (SOME a::l) = a ++ OPTION_FLAT l

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

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

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

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

|- !cmp l. ORL cmp l ==> (fmap l = FMAPAL cmp (list_to_bt l))

|- !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 cmp nt <=> T) /\
   (ORL_bt cmp (node l (x,y) r) <=> ORL_bt_ub cmp l x /\ ORL_bt_lb cmp x r)

|- !P. (!cmp. P cmp nt) /\ (!cmp l x y r. P cmp (node l (x,y) r)) ==>
       !v v1. P v v1

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

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

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

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

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

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

|- !P. (!cmp. P cmp []) /\ (!cmp a b l. P cmp l ==> P cmp ((a,b)::l)) ==>
       !v v1. P v v1

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

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

|- !cmp s l t m.
     ORWL cmp s l /\ OWL cmp t m ==>
     ORWL cmp (DRESTRICT s (COMPL t)) (diff_merge cmp l m)

|- !cmp s l t m.
     ORWL cmp s l /\ OWL cmp t m ==>
     ORWL cmp (DRESTRICT s t) (inter_merge cmp l m)

|- !cmp s l t m.
     ORWL cmp s l /\ ORWL cmp t m ==> ORWL cmp (s FUNION t) (merge cmp l m)

|- !cmp t. ORWL cmp (FMAPAL cmp t) (bt_to_orl cmp t)

|- (!a. assocv [] a = NONE) /\
   !y x l a. assocv ((x,y)::l) a = if a = x then SOME y else assocv l a

|- !P. (!a. P [] a) /\ (!x y l a. (a <> x ==> P l a) ==> P ((x,y)::l) a) ==>
       !v v1. P v v1

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

|- (!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
       (fmupdate x y FEMPTY FUNION
        DRESTRICT (FMAPAL cmp t) {z | apto cmp x z = LESS})
       (bl_to_fmap cmp b)

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

|- !cmp t. FDOM (FMAPAL cmp t) = ENUMERAL cmp (bt_map FST t)

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

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

|- !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) /\
          (fmupdate x y (FMAPAL cmp t) = FMAPAL cmp ans))

|- (!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
     fmupdate x v FEMPTY FUNION
     DRESTRICT (FMAPAL cmp r) {z | apto cmp x z = LESS}

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

|- !cmp l. ORL cmp l ==> (bt_to_orl cmp (list_to_bt l) = l)

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

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

|- !P. (!cmp. P cmp nt) /\ (!cmp l x y r. P cmp (node l (x,y) r)) ==>
       !v v1. P v v1

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

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

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

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

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

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

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

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

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

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

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

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

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

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

|- !l. FDOM (fmap l) = set (MAP FST l)

|- (!x. x IN FDOM (fmap []) <=> F) /\
   !x w z l. x IN FDOM (fmap ((w,z)::l)) <=> (x = w) \/ x IN FDOM (fmap l)

|- !cmp l. ORWL cmp (fmap l) (incr_sort cmp l)

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

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

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

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

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

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

|- !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) /\ (fmupdate x y (fmap l) = fmap ans))

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

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

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

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

|- !cmp f t. f o_f FMAPAL cmp t = FMAPAL cmp (bt_map (AP_SND f) t)

|- !f l. f o_f fmap l = fmap (MAP (AP_SND f) l)

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

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