1open HolKernel boolLib bossLib BasicProvers; 2open optionTheory pairTheory stringTheory; 3open arithmeticTheory pred_setTheory listTheory finite_mapTheory alistTheory sortingTheory; 4open comparisonTheory; 5open lcsymtacs; 6 7val _ = new_theory "balanced_map"; 8 9(* ------------------------ Preliminaries ------------------------ *) 10 11val _ = temp_tight_equality (); 12val _ = numLib.prefer_num(); 13 14val list_rel_lem1 = Q.prove ( 15`!f l l'. 16 ~LIST_REL f l l' 17 ��� 18 ���n. n ��� LENGTH l ��� n ��� LENGTH l' ��� LIST_REL f (TAKE n l) (TAKE n l') ��� 19 ((n = LENGTH l ��� n ��� LENGTH l') ��� 20 (n ��� LENGTH l ��� n = LENGTH l') ��� 21 (n ��� LENGTH l ��� n ��� LENGTH l' ��� ~f (EL n l) (EL n l')))`, 22 srw_tac[][] >> 23 `FINITE { n | n ��� LENGTH l ��� n ��� LENGTH l' ��� LIST_REL f (TAKE n l) (TAKE n l') }` 24 by (rw [GSPEC_AND, LE_LT1] >> 25 match_mp_tac FINITE_INTER >> 26 disj1_tac >> 27 rw [GSYM count_def]) >> 28 qabbrev_tac `nset = { n | n ��� LENGTH l ��� n ��� LENGTH l' ��� LIST_REL f (TAKE n l) (TAKE n l') }` >> 29 Cases_on `nset = {}` >> 30 srw_tac[] [] 31 >- (full_simp_tac (srw_ss()) [markerTheory.Abbrev_def, EXTENSION] >> 32 qexists_tac `0` >> 33 srw_tac[][] >> 34 Cases_on `l` >> 35 Cases_on `l'` >> 36 full_simp_tac (srw_ss()) [] >> 37 pop_assum (qspecl_then [`0`] mp_tac) >> 38 srw_tac[][]) 39 >- (imp_res_tac MAX_SET_DEF >> 40 qexists_tac `MAX_SET nset` >> 41 qabbrev_tac `max_nset = MAX_SET nset` >> 42 qunabbrev_tac `nset` >> 43 imp_res_tac in_max_set >> 44 REV_FULL_SIMP_TAC (srw_ss()) [] >> 45 srw_tac[] [] >> 46 full_simp_tac (srw_ss()) [LESS_OR_EQ] >> 47 srw_tac [ARITH_ss] [] >> 48 full_simp_tac (srw_ss()) [TAKE_LENGTH_ID] >> 49 CCONTR_TAC >> 50 full_simp_tac (srw_ss()) [] >> 51 `LIST_REL f (TAKE (max_nset + 1) l) (TAKE (max_nset + 1) l')` 52 by (full_simp_tac (srw_ss()) 53 [rich_listTheory.TAKE_EL_SNOC, SNOC_APPEND, 54 rich_listTheory.LIST_REL_APPEND_SING]) >> 55 `max_nset + 1 ��� {n | (n < LENGTH l ��� n = LENGTH l) ��� (n < LENGTH l' ��� n = LENGTH l') ��� LIST_REL f (TAKE n l) (TAKE n l')}` 56 by srw_tac [ARITH_ss] [] >> 57 imp_res_tac in_max_set >> 58 unabbrev_all_tac >> 59 decide_tac)); 60 61val _ = augment_srw_ss [rewrites [listTheory.TAKE_def]] 62val list_rel_lem2 = Q.prove ( 63`!l l'. 64 LIST_REL f l l' 65 ��� 66 �����n. n ��� LENGTH l ��� n ��� LENGTH l' ��� LIST_REL f (TAKE n l) (TAKE n l') ��� 67 ((n = LENGTH l ��� n ��� LENGTH l') ��� 68 (n ��� LENGTH l ��� n = LENGTH l') ��� 69 (n ��� LENGTH l ��� n ��� LENGTH l' ��� ~f (EL n l) (EL n l')))`, 70 ho_match_mp_tac LIST_REL_ind >> 71 srw_tac[] [] >> 72 CCONTR_TAC >> 73 full_simp_tac (srw_ss()) [] >> 74 EVERY_CASE_TAC >> 75 full_simp_tac (srw_ss()) [] >> 76 srw_tac[] [] 77 >- (first_x_assum (qspecl_then [`LENGTH l`] mp_tac) >> 78 srw_tac[] []) 79 >- (first_x_assum (qspecl_then [`LENGTH l'`] mp_tac) >> 80 srw_tac[] []) 81 >- (first_x_assum (qspecl_then [`n-1`] mp_tac) >> 82 srw_tac[] [] >> 83 fs[] >> 84 full_simp_tac (srw_ss()) [LIST_REL_EL_EQN] >> 85 `n - 1 ��� LENGTH l ��� n - 1 ��� LENGTH l'` by decide_tac >> 86 `n ��� LENGTH l ��� n ��� LENGTH l'` by decide_tac >> 87 full_simp_tac (srw_ss()) [LENGTH_TAKE, rich_listTheory.EL_TAKE] >> 88 srw_tac[] [] >> 89 `0 < n` by decide_tac >> 90 full_simp_tac (srw_ss()++ARITH_ss) [rich_listTheory.EL_CONS] >> 91 `PRE n = n - 1` by decide_tac >> 92 full_simp_tac (srw_ss()) [])); 93 94val list_rel_thm = Q.prove ( 95`!f l l'. 96 LIST_REL f l l' ��� 97 !n. 98 ��(n ��� LENGTH l) ��� ��(n ��� LENGTH l') ��� ��LIST_REL f (TAKE n l) (TAKE n l') ��� 99 (n ��� LENGTH l ��� n = LENGTH l') ��� 100 (n = LENGTH l ��� n ��� LENGTH l') ��� 101 (n = LENGTH l ��� n = LENGTH l' ��� f (EL n l) (EL n l'))`, 102 rw [] >> 103 eq_tac >> 104 rw [] >> 105 imp_res_tac list_rel_lem2 >> 106 fs [] >> 107 metis_tac [list_rel_lem1]); 108 109val list_rel_thm = Q.prove ( 110`!f l l'. 111 LIST_REL f l l' ��� 112 !n. 113 n ��� LENGTH l ��� n ��� LENGTH l' ��� LIST_REL f (TAKE n l) (TAKE n l') ��� 114 (n ��� LENGTH l ��� n ��� LENGTH l') ��� 115 (n ��� LENGTH l ��� n ��� LENGTH l' ��� f (EL n l) (EL n l'))`, 116 metis_tac [list_rel_thm]); 117 118val _ = bossLib.augment_srw_ss [rewrites 119 [FUNION_FUPDATE_1,FUNION_ASSOC,FUNION_FEMPTY_2,FUNION_FEMPTY_1,FDOM_DRESTRICT, 120 DRESTRICT_UNIV]] 121 122fun fs x = full_simp_tac (srw_ss()++ARITH_ss) x; 123fun rfs x = REV_FULL_SIMP_TAC (srw_ss()++ARITH_ss) x; 124val rw = srw_tac [ARITH_ss]; 125 126val fmrw = srw_tac [ARITH_ss, rewrites [FLOOKUP_UPDATE,FLOOKUP_FUNION,FLOOKUP_DRESTRICT, 127 FUNION_FUPDATE_2,FAPPLY_FUPDATE_THM,FUNION_DEF, DRESTRICT_DEF]]; 128 129fun inv_to_front_tac tm (g as (asl,w)) = let 130 val tms = strip_conj w 131 val (tms1,tms2) = List.partition (fn x => can (find_term (can (match_term tm))) x) tms 132 val tms = tms1@tms2 133 val thm = prove (``^w ��� ^(list_mk_conj tms)``, SIMP_TAC (std_ss) [AC CONJ_COMM CONJ_ASSOC]) 134in 135 ONCE_REWRITE_TAC [thm] g 136end 137 138val inv_mp_tac = let 139 val lemma = PROVE [] ``!A B C D. (A ��� B ��� C) ��� (A ��� (B ��� C ��� D)) ��� (B ��� D)`` 140in 141 fn th => fn (g as (asl,w)) => let 142 val c = th |> concl 143 val (xs,b) = strip_forall c 144 val tm = b |> dest_imp |> snd |> strip_conj |> hd 145 val tm2 = hd (strip_conj w) 146 val s = fst (match_term tm tm2) 147 val th2 = SPECL (map (Term.subst s) xs) th 148 val th3 = MATCH_MP lemma th2 149 in 150 MATCH_MP_TAC (GEN_ALL th3) g 151 end 152end 153 154val fdom_eq = PROVE [] ``m1 = m2 ��� FDOM m1 = FDOM m2``; 155 156val TIMES_MIN = Q.prove ( 157`!x y z. x * MIN y z = MIN (x * y) (x * z)`, 158 rw [MIN_DEF] >> 159 fs []); 160 161val FCARD_DISJOINT_UNION = Q.prove ( 162`!m1 m2. 163 DISJOINT (FDOM m1) (FDOM m2) ��� DISJOINT (FDOM m2) (FDOM m1) 164 ��� 165 FCARD (FUNION m1 m2) = FCARD m1 + FCARD m2`, 166 rw [DISJOINT_DEF, FCARD_DEF] >> 167 metis_tac [CARD_UNION, FDOM_FINITE, CARD_DEF, ADD_0, INTER_COMM]); 168 169val CARD_DISJOINT_UNION = Q.prove ( 170`!s1 s2. 171 FINITE s1 ��� FINITE s2 172 ��� 173 DISJOINT s1 s2 ��� DISJOINT s2 s1 174 ��� 175 CARD (s1 ��� s2) = CARD s1 + CARD s2`, 176 rw [DISJOINT_DEF] >> 177 metis_tac [CARD_UNION, CARD_DEF, ADD_0, INTER_COMM]); 178 179val FCARD_DRESTRICT = Q.prove ( 180`���m s. FCARD (DRESTRICT m s) = CARD (FDOM m ��� s)`, 181 rw [FCARD_DEF, FDOM_DRESTRICT]); 182 183val DELETE_INTER2 = Q.prove ( 184`���s t x. t ��� (s DELETE x) = s ��� t DELETE x`, 185 metis_tac [DELETE_INTER, INTER_COMM]); 186 187val POS_CARD_HAS_MEM = Q.prove ( 188`!s. FINITE s ��� 0 < CARD s ��� ?x. x ��� s`, 189 Cases_on `s` >> 190 rw [CARD_INSERT] >> 191 metis_tac []); 192 193val all_distinct_up_to_def = Define ` 194(all_distinct_up_to cmp [] ��� T) ��� 195(all_distinct_up_to cmp (k::t) ��� 196 (���k'. cmp k k' = Equal ��� ~MEM k' t) ��� all_distinct_up_to cmp t)`; 197 198val every_case_tac = BasicProvers.EVERY_CASE_TAC; 199 200(* ------------------------ Finite maps up to key equivalence ------------------------ *) 201 202val key_set_def = Define ` 203key_set cmp k = { k' | cmp k k' = Equal }`; 204 205val key_set_equiv = Q.store_thm ("key_set_equiv", 206`!cmp. 207 good_cmp cmp 208 ��� 209 (!k. k ��� key_set cmp k) ��� 210 (!k1 k2. k1 ��� key_set cmp k2 ��� k2 ��� key_set cmp k1) ��� 211 (!k1 k2 k3. k1 ��� key_set cmp k2 ��� k2 ��� key_set cmp k3 ��� k1 ��� key_set cmp k3)`, 212 rw [key_set_def] >> 213 metis_tac [good_cmp_def]); 214 215val key_set_partition = Q.store_thm ("key_set_partition", 216`!cmp k1 k2. 217 good_cmp cmp ��� 218 key_set cmp k1 ��� key_set cmp k2 219 ��� 220 DISJOINT (key_set cmp k1) (key_set cmp k2)`, 221 rw [DISJOINT_DEF, EXTENSION] >> 222 metis_tac [key_set_equiv]); 223 224val key_set_eq = Q.store_thm ("key_set_eq", 225`!cmp k1 k2. 226 good_cmp cmp 227 ��� 228 (key_set cmp k1 = key_set cmp k2 ��� cmp k1 k2 = Equal)`, 229 rw [key_set_def, EXTENSION] >> 230 metis_tac [cmp_thms, key_set_equiv]); 231 232val key_set_cmp_def = Define ` 233key_set_cmp cmp k ks res ��� 234 !k'. k' ��� ks ��� cmp k k' = res`; 235 236val key_set_cmp_thm = Q.store_thm ("key_set_cmp_thm", 237`!cmp k k' res. 238 good_cmp cmp 239 ��� 240 (key_set_cmp cmp k (key_set cmp k') res ��� cmp k k' = res)`, 241 rw [key_set_cmp_def, key_set_def] >> 242 metis_tac [cmp_thms]); 243 244val key_set_cmp2_def = Define ` 245key_set_cmp2 cmp ks1 ks2 res ��� 246 !k1 k2. k1 ��� ks1 ��� k2 ��� ks2 ��� cmp k1 k2 = res`; 247 248val key_set_cmp2_thm = Q.store_thm ("key_set_cmp2_thm", 249`!cmp k k' res. 250 good_cmp cmp 251 ��� 252 (key_set_cmp2 cmp (key_set cmp k) (key_set cmp k') res ��� cmp k k' = res)`, 253 rw [key_set_cmp2_def, key_set_def] >> 254 metis_tac [cmp_thms]); 255 256(* Maps based on balanced binary trees. Copied from ghc-7.8.3 257 * libraries/containers/Data/Map/Base.hs. It starts with the following comment: 258 259----------------------------------------------------------------------------- 260-- | 261-- Module : Data.Map.Base 262-- Copyright : (c) Daan Leijen 2002 263-- (c) Andriy Palamarchuk 2008 264-- License : BSD-style 265-- Maintainer : libraries@haskell.org 266-- Stability : provisional 267-- Portability : portable 268-- 269-- An efficient implementation of maps from keys to values (dictionaries). 270-- 271-- Since many function names (but not the type name) clash with 272-- "Prelude" names, this module is usually imported @qualified@, e.g. 273-- 274-- > import Data.Map (Map) 275-- > import qualified Data.Map as Map 276-- 277-- The implementation of 'Map' is based on /size balanced/ binary trees (or 278-- trees of /bounded balance/) as described by: 279-- 280-- * Stephen Adams, \"/Efficient sets: a balancing act/\", 281-- Journal of Functional Programming 3(4):553-562, October 1993, 282-- <http://www.swiss.ai.mit.edu/~adams/BB/>. 283-- 284-- * J. Nievergelt and E.M. Reingold, 285-- \"/Binary search trees of bounded balance/\", 286-- SIAM journal of computing 2(1), March 1973. 287-- 288-- Note that the implementation is /left-biased/ -- the elements of a 289-- first argument are always preferred to the second, for example in 290-- 'union' or 'insert'. 291-- 292-- Operation comments contain the operation time complexity in 293-- the Big-O notation <http://en.wikipedia.org/wiki/Big_O_notation>. 294----------------------------------------------------------------------------- 295 296*) 297 298val _ = Datatype ` 299balanced_map = Tip | Bin num 'k 'v balanced_map balanced_map`; 300 301val ratio_def = Define ` 302ratio = 2`; 303 304val delta_def = Define ` 305delta = 3:num`; 306 307val size_def = Define ` 308(size Tip = 0) ��� 309(size (Bin s k v l r) = s)`; 310 311val bin_def = Define ` 312bin k x l r = Bin (size l + size r + 1) k x l r`; 313 314val null_def = Define ` 315(null Tip = T) ��� 316(null (Bin s k v m1 m2) = F)`; 317 318val lookup_def = Define ` 319(lookup cmp k Tip = NONE) ��� 320(lookup cmp k (Bin s k' v l r) = 321 case cmp k k' of 322 | Less => lookup cmp k l 323 | Greater => lookup cmp k r 324 | Equal => SOME v)`; 325 326val member_def = Define ` 327(member cmp k Tip = F) ��� 328(member cmp k (Bin s k' v l r) = 329 case cmp k k' of 330 | Less => member cmp k l 331 | Greater => member cmp k r 332 | Equal => T)`; 333 334val empty_def = Define ` 335empty = Tip`; 336 337val singleton_def = Define ` 338singleton k x = Bin 1 k x Tip Tip`; 339 340(* Just like the Haskell, but w/o @ patterns *) 341val balanceL'_def = Define ` 342balanceL' k x l r = 343 case r of 344 | Tip => 345 (case l of 346 | Tip => Bin 1 k x Tip Tip 347 | (Bin _ _ _ Tip Tip) => Bin 2 k x l Tip 348 | (Bin _ lk lx Tip (Bin _ lrk lrx _ _)) => Bin 3 lrk lrx (Bin 1 lk lx Tip Tip) (Bin 1 k x Tip Tip) 349 | (Bin _ lk lx (Bin s' k' v' l' r') Tip) => Bin 3 lk lx (Bin s' k' v' l' r') (Bin 1 k x Tip Tip) 350 | (Bin ls lk lx (Bin lls k' v' l' r') (Bin lrs lrk lrx lrl lrr)) => 351 if lrs < ratio*lls then Bin (1+ls) lk lx (Bin lls k' v' l' r') (Bin (1+lrs) k x (Bin lrs lrk lrx lrl lrr) Tip) 352 else Bin (1+ls) lrk lrx (Bin (1+lls+size lrl) lk lx (Bin lls k' v' l' r') lrl) (Bin (1+size lrr) k x lrr Tip)) 353 | (Bin rs _ _ _ _) => 354 case l of 355 | Tip => Bin (1+rs) k x Tip r 356 | (Bin ls lk lx ll lr) => 357 if ls > delta*rs then 358 case (ll, lr) of 359 | (Bin lls _ _ _ _, Bin lrs lrk lrx lrl lrr) => 360 if lrs < ratio*lls then Bin (1+ls+rs) lk lx ll (Bin (1+rs+lrs) k x lr r) 361 else Bin (1+ls+rs) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) (Bin (1+rs+size lrr) k x lrr r) 362 | (_, _) => Tip (* error "Failure in Data.Map.balanceL" *) 363 else Bin (1+ls+rs) k x l r`; 364 365val balanceR'_def = Define ` 366balanceR' k x l r = 367 case l of 368 | Tip => 369 (case r of 370 | Tip => Bin 1 k x Tip Tip 371 | (Bin _ _ _ Tip Tip) => Bin 2 k x Tip r 372 | (Bin _ rk rx Tip (Bin s' k' v' l' r')) => Bin 3 rk rx (Bin 1 k x Tip Tip) (Bin s' k' v' l' r') 373 | (Bin _ rk rx (Bin _ rlk rlx _ _) Tip) => Bin 3 rlk rlx (Bin 1 k x Tip Tip) (Bin 1 rk rx Tip Tip) 374 | (Bin rs rk rx (Bin rls rlk rlx rll rlr) (Bin rrs k' v' l' r')) => 375 if rls < ratio*rrs then Bin (1+rs) rk rx (Bin (1+rls) k x Tip (Bin rls rlk rlx rll rlr)) (Bin rrs k' v' l' r') 376 else Bin (1+rs) rlk rlx (Bin (1+size rll) k x Tip rll) (Bin (1+rrs+size rlr) rk rx rlr (Bin rrs k' v' l' r'))) 377 | (Bin ls _ _ _ _) => 378 case r of 379 | Tip => Bin (1+ls) k x l Tip 380 | (Bin rs rk rx rl rr) => 381 if rs > delta*ls then 382 case (rl, rr) of 383 | (Bin rls rlk rlx rll rlr, Bin rrs _ _ _ _) => 384 if rls < ratio*rrs then Bin (1+ls+rs) rk rx (Bin (1+ls+rls) k x l rl) rr 385 else Bin (1+ls+rs) rlk rlx (Bin (1+ls+size rll) k x l rll) (Bin (1+rrs+size rlr) rk rx rlr rr) 386 | (_, _) => Tip (* error "Failure in Data.Map.balanceR" *) 387 else Bin (1+ls+rs) k x l r`; 388 389val balanceL_def = Define ` 390(balanceL k x Tip Tip = 391 Bin 1 k x Tip Tip) ��� 392(balanceL k x (Bin s' k' v' Tip Tip) Tip = 393 Bin 2 k x (Bin s' k' v' Tip Tip) Tip) ��� 394(balanceL k x (Bin _ lk lx Tip (Bin _ lrk lrx _ _)) Tip = 395 Bin 3 lrk lrx (Bin 1 lk lx Tip Tip) (Bin 1 k x Tip Tip)) ��� 396(balanceL k x (Bin _ lk lx (Bin s' k' v' l' r') Tip) Tip = 397 Bin 3 lk lx (Bin s' k' v' l' r') (Bin 1 k x Tip Tip)) ��� 398(balanceL k x (Bin ls lk lx (Bin lls k' v' l' r') (Bin lrs lrk lrx lrl lrr)) Tip = 399 if lrs < ratio*lls then 400 Bin (1+ls) lk lx (Bin lls k' v' l' r') 401 (Bin (1+lrs) k x (Bin lrs lrk lrx lrl lrr) Tip) 402 else 403 Bin (1+ls) lrk lrx (Bin (1+lls+size lrl) lk lx (Bin lls k' v' l' r') lrl) 404 (Bin (1+size lrr) k x lrr Tip)) ��� 405(balanceL k x Tip (Bin rs k' v' l' r') = 406 Bin (1+rs) k x Tip (Bin rs k' v' l' r')) ��� 407(balanceL k x (Bin ls lk lx ll lr) (Bin rs k' v' l' r') = 408 if ls > delta*rs then 409 case (ll, lr) of 410 | (Bin lls _ _ _ _, Bin lrs lrk lrx lrl lrr) => 411 if lrs < ratio*lls then 412 Bin (1+ls+rs) lk lx ll (Bin (1+rs+lrs) k x lr (Bin rs k' v' l' r')) 413 else 414 Bin (1+ls+rs) lrk lrx (Bin (1+lls+size lrl) lk lx ll lrl) 415 (Bin (1+rs+size lrr) k x lrr (Bin rs k' v' l' r')) 416 | (_, _) => Tip (* error "Failure in Data.Map.balanceL" *) 417 else 418 Bin (1+ls+rs) k x (Bin ls lk lx ll lr) (Bin rs k' v' l' r'))`; 419 420val balanceR_def = Define ` 421(balanceR k x Tip Tip = 422 Bin 1 k x Tip Tip) ��� 423(balanceR k x Tip (Bin s' k' v' Tip Tip) = 424 Bin 2 k x Tip (Bin s' k' v' Tip Tip)) ��� 425(balanceR k x Tip (Bin _ rk rx Tip (Bin s' k' v' l' r')) = 426 Bin 3 rk rx (Bin 1 k x Tip Tip) (Bin s' k' v' l' r')) ��� 427(balanceR k x Tip (Bin _ rk rx (Bin _ rlk rlx _ _) Tip) = 428 Bin 3 rlk rlx (Bin 1 k x Tip Tip) (Bin 1 rk rx Tip Tip)) ��� 429(balanceR k x Tip (Bin rs rk rx (Bin rls rlk rlx rll rlr) (Bin rrs k' v' l' r')) = 430 if rls < ratio*rrs then 431 Bin (1+rs) rk rx (Bin (1+rls) k x Tip (Bin rls rlk rlx rll rlr)) (Bin rrs k' v' l' r') 432 else 433 Bin (1+rs) rlk rlx (Bin (1+size rll) k x Tip rll) 434 (Bin (1+rrs+size rlr) rk rx rlr (Bin rrs k' v' l' r'))) ��� 435(balanceR k x (Bin ls k' v' l' r') Tip = 436 Bin (1+ls) k x (Bin ls k' v' l' r') Tip) ��� 437(balanceR k x (Bin ls k' v' l' r') (Bin rs rk rx rl rr) = 438 if rs > delta*ls then 439 case (rl, rr) of 440 | (Bin rls rlk rlx rll rlr, Bin rrs _ _ _ _) => 441 if rls < ratio*rrs then 442 Bin (1+ls+rs) rk rx (Bin (1+ls+rls) k x (Bin ls k' v' l' r') rl) rr 443 else 444 Bin (1+ls+rs) rlk rlx (Bin (1+ls+size rll) k x (Bin ls k' v' l' r') rll) 445 (Bin (1+rrs+size rlr) rk rx rlr rr) 446 | (_, _) => Tip (* error "Failure in Data.Map.balanceR" *) 447 else 448 Bin (1+ls+rs) k x (Bin ls k' v' l' r') (Bin rs rk rx rl rr))`; 449 450val insert_def = Define ` 451(insert cmp k v Tip = singleton k v) ��� 452(insert cmp k v (Bin s k' v' l r) = 453 case cmp k k' of 454 | Less => balanceL k' v' (insert cmp k v l) r 455 | Greater => balanceR k' v' l (insert cmp k v r) 456 | Equal => Bin s k v l r)`; 457 458val insertR_def = Define ` 459(insertR cmp k v Tip = singleton k v) ��� 460(insertR cmp k v (Bin s k' v' l r) = 461 case cmp k k' of 462 | Less => balanceL k' v' (insertR cmp k v l) r 463 | Greater => balanceR k' v' l (insertR cmp k v r) 464 | Equal => Bin s k' v' l r)`; 465 466val insertMax_def = Define ` 467(insertMax k v Tip = singleton k v) ��� 468(insertMax k v (Bin s k' v' l r) = balanceR k' v' l (insertMax k v r))`; 469 470val insertMin_def = Define ` 471(insertMin k v Tip = singleton k v) ��� 472(insertMin k v (Bin s k' v' l r) = balanceL k' v' (insertMin k v l) r)`; 473 474val deleteFindMax_def = Define ` 475(deleteFindMax (Bin s k x l Tip) = ((k,x),l)) ��� 476(deleteFindMax (Bin s k x l r) = 477 let (km,r') = deleteFindMax r in 478 (km,balanceL k x l r')) ��� 479(deleteFindMax Tip = 480 (ARB,Tip))`; (*(error "Map.deleteFindMax: can not return the maximal element of an empty map", Tip)*) 481 482val deleteFindMin_def = Define ` 483(deleteFindMin (Bin s k x Tip r) = ((k,x),r)) ��� 484(deleteFindMin (Bin s k x l r) = 485 let (km,l') = deleteFindMin l in 486 (km,balanceR k x l' r)) ��� 487(deleteFindMin Tip = 488 (ARB,Tip))`; (*(error "Map.deleteFindMin: can not return the maximal element of an empty map", Tip)*) 489 490val glue_def = Define ` 491(glue Tip r = r) ��� 492(glue l Tip = l) ��� 493(glue l r = 494 if size l > size r then 495 let ((km,m),l') = deleteFindMax l in 496 balanceR km m l' r 497 else 498 let ((km,m),r') = deleteFindMin r in 499 balanceL km m l r')`; 500 501val delete_def = Define ` 502(delete cmp k Tip = Tip) ��� 503(delete cmp k (Bin s k' v l r) = 504 case cmp k k' of 505 | Less => balanceR k' v (delete cmp k l) r 506 | Greater => balanceL k' v l (delete cmp k r) 507 | Eq => glue l r)`; 508 509val trim_help_greater_def = Define ` 510(trim_help_greater cmp lo (Bin s' k v' l' r) = 511 if cmp k lo = Less ��� cmp k lo = Equal then 512 trim_help_greater cmp lo r 513 else 514 Bin s' k v' l' r) ��� 515(trim_help_greater cmp lo Tip = Tip)`; 516 517val trim_help_lesser_def = Define ` 518(trim_help_lesser cmp hi (Bin s' k v' l r') = 519 if cmp k hi = Greater ��� cmp k hi = Equal then 520 trim_help_lesser cmp hi l 521 else 522 Bin s' k v' l r') ��� 523(trim_help_lesser cmp lo Tip = Tip)`; 524 525val trim_help_middle_def = Define ` 526(trim_help_middle cmp lo hi (Bin s' k v' l r) = 527 if cmp k lo = Less ��� cmp k lo = Equal then 528 trim_help_middle cmp lo hi r 529 else if cmp k hi = Greater ��� cmp k hi = Equal then 530 trim_help_middle cmp lo hi l 531 else 532 Bin s' k v' l r) ��� 533(trim_help_middle lo cmp hi Tip = Tip)`; 534 535val trim_def = Define ` 536(trim cmp NONE NONE t = t) ��� 537(trim cmp (SOME lk) NONE t = trim_help_greater cmp lk t) ��� 538(trim cmp NONE (SOME hk) t = trim_help_lesser cmp hk t) ��� 539(trim cmp (SOME lk) (SOME hk) t = trim_help_middle cmp lk hk t)`; 540 541val link_def = Define ` 542(link k v Tip r = insertMin k v r) ��� 543(link k v l Tip = insertMax k v l) ��� 544(link k v (Bin sizeL ky y ly ry) (Bin sizeR kz z lz rz) = 545 if delta*sizeL < sizeR then 546 balanceL kz z (link k v (Bin sizeL ky y ly ry) lz) rz 547 else if delta*sizeR < sizeL then 548 balanceR ky y ly (link k v ry (Bin sizeR kz z lz rz)) 549 else 550 bin k v (Bin sizeL ky y ly ry) (Bin sizeR kz z lz rz))`; 551 552val filterLt_help_def = Define ` 553(filterLt_help cmp b Tip = Tip) ��� 554(filterLt_help cmp b' (Bin s kx x l r) = 555 case cmp kx b' of 556 | Less => link kx x l (filterLt_help cmp b' r) 557 | Equal => l 558 | Greater => filterLt_help cmp b' l)`; 559 560val filterLt_def = Define ` 561(filterLt cmp NONE t = t) ��� 562(filterLt cmp (SOME b) t = filterLt_help cmp b t)`; 563 564val filterGt_help_def = Define ` 565(filterGt_help cmp b Tip = Tip) ��� 566(filterGt_help cmp b' (Bin s kx x l r) = 567 case cmp b' kx of 568 | Less => link kx x (filterGt_help cmp b' l) r 569 | Equal => r 570 | Greater => filterGt_help cmp b' r)`; 571 572val filterGt_def = Define ` 573(filterGt cmp NONE t = t) ��� 574(filterGt cmp (SOME b) t = filterGt_help cmp b t)`; 575 576val hedgeUnion_def = Define ` 577(hedgeUnion cmp blo bhi t1 Tip = t1) ��� 578(hedgeUnion cmp blo bhi Tip (Bin _ kx x l r) = 579 link kx x (filterGt cmp blo l) (filterLt cmp bhi r)) ��� 580(hedgeUnion cmp blo bhi t1 (Bin _ kx x Tip Tip) = insertR cmp kx x t1) ��� 581(hedgeUnion cmp blo bhi (Bin s kx x l r) t2 = 582 link kx x (hedgeUnion cmp blo (SOME kx) l (trim cmp blo (SOME kx) t2)) 583 (hedgeUnion cmp (SOME kx) bhi r (trim cmp (SOME kx) bhi t2)))`; 584 585val union_def = Define ` 586(union cmp Tip t2 = t2) ��� 587(union cmp t1 Tip = t1) ��� 588(union cmp t1 t2 = hedgeUnion cmp NONE NONE t1 t2)`; 589 590val foldrWithKey_def = Define ` 591(foldrWithKey f z' Tip = z') ��� 592(foldrWithKey f z' (Bin _ kx x l r) = 593 foldrWithKey f (f kx x (foldrWithKey f z' r)) l)`; 594 595val toAscList_def = Define ` 596toAscList t = foldrWithKey (\k x xs. (k,x)::xs) [] t`; 597 598val compare_def = Define ` 599compare cmp1 cmp2 t1 t2 = list_cmp (pair_cmp cmp1 cmp2) (toAscList t1) (toAscList t2)`; 600 601val map_def = Define ` 602(map _ Tip ��� Tip) ��� 603(map f (Bin sx kx x l r) ��� Bin sx kx (f x) (map f l) (map f r))`; 604 605val splitLookup_def = Define ` 606(splitLookup cmp k Tip = (Tip,NONE,Tip)) ��� 607(splitLookup cmp k (Bin _ kx x l r) = 608 case cmp k kx of 609 | Less => 610 let (lt,z,gt) = splitLookup cmp k l in 611 let gt' = link kx x gt r in 612 (lt,z,gt') 613 | Greater => 614 let (lt,z,gt) = splitLookup cmp k r in 615 let lt' = link kx x l lt in 616 (lt',z,gt) 617 | Equal => 618 (l,SOME x,r))`; 619 620val submap'_def = Define ` 621(submap' cmp _ Tip _ = T) ��� 622(submap' cmp _ _ Tip = F) ��� 623(submap' cmp f (Bin _ kx x l r) t = 624 case splitLookup cmp kx t of 625 | (lt,NONE,gt) => F 626 | (lt,SOME y,gt) => f x y ��� submap' cmp f l lt ��� submap' cmp f r gt)`; 627 628val isSubmapOfBy_def = Define ` 629isSubmapOfBy cmp f t1 t2 ��� size t1 ��� size t2 ��� submap' cmp f t1 t2`; 630 631val isSubmapOf_def = Define ` 632isSubmapOf cmp t1 t2 ��� isSubmapOfBy cmp (=) t1 t2`; 633 634(* TODO: The ghc implementation is more complex and efficient *) 635val fromList_def = Define ` 636fromList cmp l = FOLDR (��(k,v) t. insert cmp k v t) empty l`; 637 638(* ----------------------- proofs ------------------------ *) 639 640val balanceL_ind = fetch "-" "balanceL_ind"; 641val balanceR_ind = fetch "-" "balanceR_ind"; 642 643val balanceL'_thm = Q.prove ( 644`!k v l r. balanceL k v l r = balanceL' k v l r`, 645 ho_match_mp_tac balanceL_ind >> 646 rw [balanceL_def, balanceL'_def]); 647 648val balanceR'_thm = Q.prove ( 649`!k v l r. balanceR k v l r = balanceR' k v l r`, 650 ho_match_mp_tac balanceR_ind >> 651 rw [balanceR_def, balanceR'_def]); 652 653val to_fmap_def = Define ` 654(to_fmap cmp Tip = FEMPTY) ��� 655(to_fmap cmp (Bin s k v l r) = 656 (FUNION (to_fmap cmp l) (to_fmap cmp r)) |+ (key_set cmp k,v))`; 657 658val to_fmap_key_set = Q.store_thm ("to_fmap_key_set", 659`!cmp ks t. 660 ks ��� FDOM (to_fmap cmp t) ��� ?k. ks = key_set cmp k`, 661 Induct_on `t` >> 662 rw [to_fmap_def] >> 663 metis_tac []); 664 665val balanced_def = Define ` 666balanced l r ��� 667 l + r ��� 1 ��� MAX l r ��� delta * MIN l r`; 668 669val structure_size_def = Define ` 670(structure_size Tip = 0) ��� 671(structure_size (Bin n k v l r) = 1 + structure_size l + structure_size r)`; 672 673val key_ordered_def = Define ` 674(key_ordered cmp k Tip res ��� T) ��� 675(key_ordered cmp k (Bin n k' v l r) res ��� 676 cmp k k' = res ��� 677 key_ordered cmp k l res ��� 678 key_ordered cmp k r res)`; 679 680val key_ordered_to_fmap = Q.prove ( 681`!cmp k t res. 682 good_cmp cmp ��� 683 (key_ordered cmp k t res 684 ��� 685 (!ks. ks ��� FDOM (to_fmap cmp t) ��� key_set_cmp cmp k ks res))`, 686 Induct_on `t` >> 687 rw [key_ordered_def, to_fmap_def] >> 688 eq_tac >> 689 rw [] >> 690 metis_tac [key_set_cmp_thm]); 691 692val invariant_def = Define ` 693(invariant cmp Tip ��� T) ��� 694(invariant cmp (Bin s k v l r) ��� 695 s = 1 + structure_size l + structure_size r ��� 696 key_ordered cmp k l Greater ��� 697 key_ordered cmp k r Less ��� 698 balanced (size l) (size r) ��� 699 invariant cmp l ��� 700 invariant cmp r)`; 701 702val invariant_eq = Q.store_thm ("invariant_eq", 703`(invariant cmp Tip ��� T) ��� 704 (invariant cmp (Bin s k v l r) ��� 705 (good_cmp cmp ��� DISJOINT (FDOM (to_fmap cmp l)) (FDOM (to_fmap cmp r))) ��� 706 (good_cmp cmp ��� key_set cmp k ��� FDOM (to_fmap cmp l)) ��� 707 (good_cmp cmp ��� key_set cmp k ��� FDOM (to_fmap cmp r)) ��� 708 s = 1 + structure_size l + structure_size r ��� 709 key_ordered cmp k l Greater ��� 710 key_ordered cmp k r Less ��� 711 balanced (size l) (size r) ��� 712 invariant cmp l ��� 713 invariant cmp r)`, 714 rw [invariant_def] >> 715 eq_tac >> 716 rw [DISJOINT_DEF, EXTENSION] >> 717 CCONTR_TAC >> 718 fs [] >> 719 imp_res_tac key_ordered_to_fmap >> 720 fs [] >> 721 imp_res_tac to_fmap_key_set >> 722 rw [] >> 723 rfs [key_set_cmp_thm] >> 724 metis_tac [cmp_thms]); 725 726val inv_props = Q.prove ( 727`!cmp s k v l r. 728 good_cmp cmp ��� 729 invariant cmp (Bin s k v l r) 730 ��� 731 DISJOINT (FDOM (to_fmap cmp l)) (FDOM (to_fmap cmp r)) ��� 732 (!x. key_set cmp x ��� FDOM (to_fmap cmp l) ��� cmp k x = Greater) ��� 733 (!x. key_set cmp x ��� FDOM (to_fmap cmp r) ��� cmp k x = Less)`, 734 rw [invariant_eq] >> 735 imp_res_tac key_ordered_to_fmap >> 736 rfs [key_set_cmp_thm]); 737 738val structure_size_thm = Q.prove ( 739`!cmp t. invariant cmp t ��� size t = structure_size t`, 740 Cases_on `t` >> 741 rw [size_def, invariant_def, structure_size_def]); 742 743val structure_size_to_fmap = Q.prove ( 744`!cmp t. good_cmp cmp ��� invariant cmp t ��� FCARD (to_fmap cmp t) = structure_size t`, 745 Induct_on `t` >> 746 rw [invariant_eq, structure_size_def, to_fmap_def, FCARD_FEMPTY] >> 747 rw [FCARD_FUPDATE, FCARD_DISJOINT_UNION]); 748 749val size_thm = Q.store_thm ("size_thm", 750`!cmp t. good_cmp cmp ��� invariant cmp t ��� size t = FCARD (to_fmap cmp t)`, 751 metis_tac [structure_size_thm, structure_size_to_fmap]); 752 753val null_thm = Q.store_thm ("null_thm", 754`!cmp t. null t ��� (to_fmap cmp t = FEMPTY)`, 755 Cases_on `t` >> 756 rw [null_def, to_fmap_def]); 757 758val lookup_thm = Q.store_thm ("lookup_thm", 759`!cmp k t. 760 good_cmp cmp ��� 761 invariant cmp t 762 ��� 763 lookup cmp k t = FLOOKUP (to_fmap cmp t) (key_set cmp k)`, 764 Induct_on `t` >> 765 rw [lookup_def, to_fmap_def] >> 766 imp_res_tac inv_props >> 767 every_case_tac >> 768 fs [invariant_eq, FLOOKUP_UPDATE, FLOOKUP_FUNION] >> 769 every_case_tac >> 770 fs [] >> 771 rw [] >> 772 rfs [key_set_eq] >> 773 fs [FLOOKUP_DEF] >> 774 metis_tac [cmp_thms]); 775 776val member_thm = Q.store_thm ("member_thm", 777`!cmp k t. 778 good_cmp cmp ��� 779 invariant cmp t 780 ��� 781 (member cmp k t ��� key_set cmp k ��� FDOM (to_fmap cmp t))`, 782 Induct_on `t` >> 783 rw [member_def, to_fmap_def] >> 784 imp_res_tac inv_props >> 785 every_case_tac >> 786 fs [invariant_def, FLOOKUP_UPDATE, FLOOKUP_FUNION] >> 787 every_case_tac >> 788 fs [] >> 789 rw [] >> 790 rfs [key_set_eq] >> 791 fs [FLOOKUP_DEF] >> 792 metis_tac [cmp_thms]); 793 794val empty_thm = Q.store_thm ("empty_thm", 795`!cmp. invariant cmp empty ��� to_fmap cmp empty = FEMPTY`, 796 rw [invariant_def, empty_def, to_fmap_def, FCARD_DEF]); 797 798val singleton_thm = Q.store_thm ("singleton_thm", 799`!cmp k v. invariant cmp (singleton k v) ��� to_fmap cmp (singleton k v) = FEMPTY |+ (key_set cmp k,v)`, 800 rw [balanced_def, invariant_def, singleton_def, to_fmap_def, size_def, structure_size_def, 801 key_ordered_def]); 802 803(* The balance routine from the comments in the Haskell file *) 804 805val singleL_def = Define ` 806singleL k1 x1 t1 (Bin _ k2 x2 t2 t3) = bin k2 x2 (bin k1 x1 t1 t2) t3`; 807 808val singleR_def = Define ` 809singleR k1 x1 (Bin _ k2 x2 t1 t2) t3 = bin k2 x2 t1 (bin k1 x1 t2 t3)`; 810 811val doubleL_def = Define ` 812doubleL k1 x1 t1 (Bin _ k2 x2 (Bin _ k3 x3 t2 t3) t4) = 813 bin k3 x3 (bin k1 x1 t1 t2) (bin k2 x2 t3 t4)`; 814 815val doubleR_def = Define ` 816doubleR k1 x1 (Bin _ k2 x2 t1 (Bin _ k3 x3 t2 t3)) t4 = 817 bin k3 x3 (bin k2 x2 t1 t2) (bin k1 x1 t3 t4)`; 818 819val rotateL_def = Define ` 820(rotateL k x l (Bin s' k' x' ly ry) = 821 if size ly < ratio * size ry then 822 singleL k x l (Bin s' k' x' ly ry) 823 else 824 doubleL k x l (Bin s' k' x' ly ry)) ��� 825(rotateL k x l Tip = 826 doubleL k x l Tip)`; 827 828val rotateR_def = Define ` 829(rotateR k x (Bin s' k' x' ly ry) r = 830 if size ry < ratio * size ly then 831 singleR k x (Bin s' k' x' ly ry) r 832 else 833 doubleR k x (Bin s' k' x' ly ry) r) ��� 834(rotateR k x Tip r = 835 doubleR k x Tip r)`; 836 837val bal_def = Define ` 838bal k x l r = 839 if size l + size r ��� 1 then 840 Bin (size l + size r + 1) k x l r 841 else if size r > delta * size l then 842 rotateL k x l r 843 else if size l > delta * size r then 844 rotateR k x l r 845 else 846 Bin (size l + size r + 1) k x l r`; 847 848val balL_def = Define ` 849balL k x l r = 850 if size l + size r ��� 1 then 851 Bin (size l + size r + 1) k x l r 852 else if size l > delta * size r then 853 rotateR k x l r 854 else 855 Bin (size l + size r + 1) k x l r`; 856 857val balR_def = Define ` 858balR k x l r = 859 if size l + size r ��� 1 then 860 Bin (size l + size r + 1) k x l r 861 else if size r > delta * size l then 862 rotateL k x l r 863 else 864 Bin (size l + size r + 1) k x l r`; 865 866(* We want a formula that states how unbalanced two trees can be 867 * and still be re-balanced by the balancer. It also has to allow the 868 * trees to be as unbalanced as the link, insert and delete functions need. The 869 * formula below is the result of guesswork. *) 870val almost_balancedL_def = Define ` 871almost_balancedL l r = 872 if l + r ��� 1 ��� l ��� delta * r then 873 balanced l r 874 else if r = 0 then 875 l < 5 876 else if r = 1 then 877 l < 8 878 else 879 2 * l < (2 * delta + 3) * r + 2`; 880 881val almost_balancedR_def = Define ` 882almost_balancedR l r = 883 if l + r ��� 1 ��� r ��� delta * l then 884 balanced l r 885 else if l = 0 then 886 r < 5 887 else if l = 1 then 888 r < 8 889 else 890 2 * r < (2 * delta + 3) * l + 2`; 891 892val balanced_lem1 = Q.prove ( 893`!l r. l + r ��� 1 ��� balanced l r`, 894 rw [balanced_def]); 895 896val balanced_lem2 = Q.prove ( 897`!l r. 898 ��(l > delta * r) ��� 899 almost_balancedL l r ��� 900 ��(l + r ��� 1) 901 ��� 902 balanced l r`, 903 rw [almost_balancedL_def, balanced_def, NOT_LESS_EQUAL, NOT_GREATER, TIMES_MIN, delta_def]); 904 905val balanced_lem3 = Q.prove ( 906`!b b0 r. 907 almost_balancedL (b + b0 + 1) r ��� 908 b + b0 + 1 > delta * r ��� 909 b0 < ratio * b ��� 910 balanced b b0 911 ��� 912 balanced b (b0 + r + 1) ��� 913 balanced b0 r`, 914 rw [almost_balancedL_def, balanced_def, TIMES_MIN, delta_def, ratio_def] >> 915 fs [MIN_DEF]); 916 917val balanced_lem4 = Q.prove ( 918`!b b' b0' r. 919 almost_balancedL (b + b' + b0' + 2) r ��� 920 b + b' + b0' + 2 > delta * r ��� 921 ��(b' + b0' + 1 < ratio * b) ��� 922 balanced b (b' + b0' + 1) ��� 923 balanced b' b0' 924 ��� 925 balanced (b + b' + 1) (b0' + r + 1) ��� 926 balanced b b' ��� 927 balanced b0' r`, 928 rw [almost_balancedL_def, balanced_def, TIMES_MIN, delta_def, ratio_def] >> 929 fs [MIN_DEF]); 930 931val balanced_lem5 = Q.prove ( 932`!l r. 933 ��(r > delta * l) ��� 934 almost_balancedR l r 935 ��� 936 balanced l r`, 937 rw [almost_balancedR_def, balanced_def, NOT_LESS_EQUAL, NOT_GREATER, TIMES_MIN, delta_def]); 938 939val balanced_lem6 = Q.prove ( 940`!b b0 l. 941 almost_balancedR l (b + b0 + 1) ��� 942 b + b0 + 1 > delta * l ��� 943 b < ratio * b0 ��� 944 balanced b b0 945 ��� 946 balanced (b + l + 1) b0 ��� balanced l b`, 947 rw [almost_balancedR_def, balanced_def, TIMES_MIN, delta_def, ratio_def] >> 948 fs [MIN_DEF]); 949 950val balanced_lem7 = Q.prove ( 951`!b b0 b0' l b'. 952 almost_balancedR l (b' + b0 + b0' + 2) ��� 953 b' + b0 + b0' + 2 > delta * l ��� 954 ��(b' + b0' + 1 < ratio * b0) ��� 955 balanced (b' + b0' + 1) b0 ��� 956 balanced b' b0' 957 ��� 958 balanced (b' + l + 1) (b0 + b0' + 1) ��� 959 balanced l b' ��� 960 balanced b0' b0`, 961 rw [almost_balancedR_def, balanced_def, TIMES_MIN, delta_def, ratio_def] >> 962 fs [MIN_DEF]); 963 964val singleR_thm = Q.prove ( 965`!k v r cmp n k' v' b b0. 966 good_cmp cmp ��� 967 key_ordered cmp k (Bin n k' v' b b0) Greater ��� 968 key_ordered cmp k r Less ��� 969 almost_balancedL n (size r) ��� 970 ��(size r + n ��� 1) ��� 971 n > delta * size r ��� 972 size b0 < ratio * size b ��� 973 invariant cmp (Bin n k' v' b b0) ��� 974 invariant cmp r 975 ��� 976 invariant cmp (singleR k v (Bin n k' v' b b0) r) ��� 977 to_fmap cmp (singleR k v (Bin n k' v' b b0) r) = 978 (FUNION (to_fmap cmp (Bin n k' v' b b0)) (to_fmap cmp r)) |+ (key_set cmp k,v)`, 979 rw [singleR_def] >> 980 imp_res_tac inv_props 981 >- (fs [invariant_def, bin_def, size_def, structure_size_def, bin_def, key_ordered_def] >> 982 imp_res_tac structure_size_thm >> 983 rw [size_def] >> 984 rfs [size_def, key_ordered_to_fmap] >> 985 rw [] >> 986 metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms, balanced_lem3, ADD_ASSOC]) 987 >- (rw [to_fmap_def, bin_def, FUNION_FUPDATE_2, FUNION_FUPDATE_1] >> 988 fs [to_fmap_def, invariant_def, key_ordered_def] >> 989 metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms, FUPDATE_COMMUTES, FUNION_ASSOC])); 990 991val doubleR_thm = Q.prove ( 992`!k v r cmp n k' v' b b0. 993 good_cmp cmp ��� 994 key_ordered cmp k (Bin n k' v' b b0) Greater ��� 995 key_ordered cmp k r Less ��� 996 almost_balancedL n (size r) ��� 997 ��(size r + n ��� 1) ��� 998 n > delta * size r ��� 999 ��(size b0 < ratio * size b) ��� 1000 invariant cmp (Bin n k' v' b b0) ��� 1001 invariant cmp r 1002 ��� 1003 invariant cmp (doubleR k v (Bin n k' v' b b0) r) ��� 1004 to_fmap cmp (doubleR k v (Bin n k' v' b b0) r) = 1005 (FUNION (to_fmap cmp (Bin n k' v' b b0)) (to_fmap cmp r)) |+ (key_set cmp k,v)`, 1006 rw [] >> 1007 `structure_size b0 ��� 0` 1008 by (fs [delta_def, ratio_def, invariant_def, size_def, 1009 NOT_LESS_EQUAL, NOT_LESS, NOT_GREATER] >> 1010 imp_res_tac structure_size_thm >> 1011 fs []) >> 1012 Cases_on `b0` >> 1013 fs [structure_size_def, doubleR_def, bin_def] >> 1014 imp_res_tac inv_props >> 1015 fs [Once invariant_def] >> 1016 imp_res_tac inv_props >> 1017 fs [invariant_def, to_fmap_def] 1018 >- (fs [size_def, bin_def, to_fmap_def] >> 1019 imp_res_tac structure_size_thm >> 1020 simp [structure_size_def, key_ordered_def] >> 1021 fs [structure_size_def, to_fmap_def, key_ordered_def] >> 1022 rfs [key_ordered_to_fmap] >> 1023 rw [] 1024 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1025 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1026 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1027 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] >> 1028 metis_tac [ADD_ASSOC, balanced_lem4]) 1029 >- (rw [FUNION_FUPDATE_2, FUNION_FUPDATE_1] >> 1030 fs [key_ordered_def] >> 1031 rfs [key_ordered_to_fmap] 1032 >- metis_tac [cmp_thms] 1033 >- metis_tac [cmp_thms] >> 1034 `key_set cmp k' ��� key_set cmp k'' ��� 1035 key_set cmp k ��� key_set cmp k' ��� 1036 key_set cmp k ��� key_set cmp k''` 1037 by metis_tac [key_set_eq, cmp_thms] >> 1038 metis_tac [FUPDATE_COMMUTES, FUNION_ASSOC])); 1039val _ = print "Proved doubleR_thm\n"; 1040 1041val rotateR_thm = Q.prove ( 1042`!k v l r cmp. 1043 good_cmp cmp ��� 1044 key_ordered cmp k l Greater ��� 1045 key_ordered cmp k r Less ��� 1046 ��(size l + size r ��� 1) ��� 1047 size l > delta * size r ��� 1048 almost_balancedL (size l) (size r) ��� 1049 invariant cmp l ��� 1050 invariant cmp r 1051 ��� 1052 invariant cmp (rotateR k v l r) ��� 1053 to_fmap cmp (rotateR k v l r) = 1054 (FUNION (to_fmap cmp l) (to_fmap cmp r)) |+ (key_set cmp k,v)`, 1055 Cases_on `l` 1056 >- fs [size_def] >> 1057 rw [size_def, rotateR_def] >> 1058 metis_tac [singleR_thm, doubleR_thm, ADD_COMM, NOT_ZERO_LT_ZERO, GREATER_DEF]); 1059val _ = print "Proved rotateR_thm\n"; 1060 1061val balanceL_balL = Q.prove ( 1062`!k v l r cmp. 1063 good_cmp cmp ��� 1064 invariant cmp l ��� 1065 invariant cmp r 1066 ��� 1067 balanceL k v l r = balL k v l r`, 1068 ho_match_mp_tac balanceL_ind >> 1069 rw [] >> 1070 rw [balanceL_def, balL_def, rotateR_def, doubleR_def, bin_def, singleR_def] >> 1071 imp_res_tac structure_size_thm >> 1072 fs [size_def, invariant_def, structure_size_def] >> 1073 imp_res_tac structure_size_thm >> 1074 fs [balanced_def] >> 1075 TRY (Cases_on `l` >> fs [structure_size_def, size_def] >> NO_TAC) >> 1076 TRY (Cases_on `r` >> fs [structure_size_def, size_def] >> NO_TAC) >> 1077 TRY (fs [ratio_def] >> NO_TAC) >> 1078 every_case_tac >> 1079 fs [size_def, structure_size_def, ratio_def, delta_def] >> 1080 imp_res_tac structure_size_thm >> 1081 fs [invariant_def, doubleR_def, bin_def, size_def] >> 1082 imp_res_tac structure_size_thm >> 1083 rw []); 1084val _ = print "Proved balanceL_balL\n"; 1085 1086val balanceL_thm = Q.prove ( 1087`!k v l r cmp. 1088 good_cmp cmp ��� 1089 key_ordered cmp k l Greater ��� 1090 key_ordered cmp k r Less ��� 1091 almost_balancedL (size l) (size r) ��� 1092 invariant cmp l ��� 1093 invariant cmp r 1094 ��� 1095 invariant cmp (balanceL k v l r) ��� 1096 to_fmap cmp (balanceL k v l r) = 1097 (FUNION (to_fmap cmp l) (to_fmap cmp r)) |+ (key_set cmp k,v)`, 1098 rw [] >> 1099 `balanceL k v l r = balL k v l r` by metis_tac [balanceL_balL] >> 1100 rw [] >> 1101 rw [balL_def, invariant_def] >> 1102 imp_res_tac structure_size_thm >> 1103 rw [balanced_lem1, balanced_lem2, to_fmap_def] >> 1104 metis_tac [rotateR_thm]); 1105 1106val singleL_thm = Q.prove ( 1107`!k v l cmp n k' v' b b0. 1108 good_cmp cmp ��� 1109 key_ordered cmp k (Bin n k' v' b b0) Less ��� 1110 key_ordered cmp k l Greater ��� 1111 almost_balancedR (size l) n ��� 1112 ��(size l + n ��� 1) ��� 1113 n > delta * size l ��� 1114 size b < ratio * size b0 ��� 1115 invariant cmp (Bin n k' v' b b0) ��� 1116 invariant cmp l 1117 ��� 1118 invariant cmp (singleL k v l (Bin n k' v' b b0)) ��� 1119 to_fmap cmp (singleL k v l (Bin n k' v' b b0)) = 1120 (FUNION (to_fmap cmp l) (to_fmap cmp (Bin n k' v' b b0))) |+ (key_set cmp k,v)`, 1121 rw [singleL_def] >> 1122 imp_res_tac inv_props 1123 >- (fs [invariant_def, bin_def, size_def, structure_size_def, bin_def, key_ordered_def] >> 1124 imp_res_tac structure_size_thm >> 1125 rw [size_def] >> 1126 rfs [size_def, key_ordered_to_fmap] >> 1127 rw [] >> 1128 metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms, balanced_lem6, ADD_ASSOC]) 1129 >- (rw [to_fmap_def, bin_def, FUNION_FUPDATE_2, FUNION_FUPDATE_1] >> 1130 fs [to_fmap_def, invariant_def, key_ordered_def] >> 1131 rfs [key_ordered_to_fmap] >> 1132 metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms, FUPDATE_COMMUTES, FUNION_ASSOC])); 1133 1134val doubleL_thm = Q.prove ( 1135`!k v l cmp n k' v' b b0. 1136 good_cmp cmp ��� 1137 key_ordered cmp k (Bin n k' v' b b0) Less ��� 1138 key_ordered cmp k l Greater ��� 1139 almost_balancedR (size l) n ��� 1140 ��(n + size l ��� 1) ��� 1141 n > delta * size l ��� 1142 ��(size b < ratio * size b0) ��� 1143 invariant cmp (Bin n k' v' b b0) ��� 1144 invariant cmp l 1145 ��� 1146 invariant cmp (doubleL k v l (Bin n k' v' b b0)) ��� 1147 to_fmap cmp (doubleL k v l (Bin n k' v' b b0)) = 1148 (FUNION (to_fmap cmp l) (to_fmap cmp (Bin n k' v' b b0))) |+ (key_set cmp k,v)`, 1149 rw [] >> 1150 `structure_size b ��� 0` 1151 by (fs [delta_def, ratio_def, invariant_def, size_def, 1152 NOT_LESS_EQUAL, NOT_LESS, NOT_GREATER] >> 1153 imp_res_tac structure_size_thm >> 1154 fs []) >> 1155 Cases_on `b` >> 1156 fs [structure_size_def, doubleL_def, bin_def] >> 1157 imp_res_tac inv_props >> 1158 fs [Once invariant_def] >> 1159 imp_res_tac inv_props >> 1160 fs [invariant_def, to_fmap_def] 1161 >- (fs [size_def, bin_def, to_fmap_def] >> 1162 imp_res_tac structure_size_thm >> 1163 simp [structure_size_def, key_ordered_def] >> 1164 fs [structure_size_def, to_fmap_def, key_ordered_def] >> 1165 rfs [key_ordered_to_fmap] >> 1166 rw [] 1167 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1168 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1169 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1170 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] >> 1171 metis_tac [ADD_ASSOC, balanced_lem7]) 1172 >- (rw [FUNION_FUPDATE_2, FUNION_FUPDATE_1] >> 1173 fs [key_ordered_def] >> 1174 rfs [key_ordered_to_fmap] 1175 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1176 >- metis_tac [cmp_thms] 1177 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1178 >- metis_tac [cmp_thms] 1179 >- metis_tac [cmp_thms] 1180 >- metis_tac [cmp_thms] 1181 >- metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1182 >- (`key_set cmp k' ��� key_set cmp k'' ��� 1183 key_set cmp k ��� key_set cmp k' ��� 1184 key_set cmp k ��� key_set cmp k''` 1185 by metis_tac [key_set_eq, cmp_thms] >> 1186 metis_tac [FUPDATE_COMMUTES, FUNION_ASSOC]))); 1187 1188val rotateL_thm = Q.prove ( 1189`!k v l r cmp. 1190 good_cmp cmp ��� 1191 key_ordered cmp k r Less ��� 1192 key_ordered cmp k l Greater ��� 1193 ��(size l + size r ��� 1) ��� 1194 size r > delta * size l ��� 1195 almost_balancedR (size l) (size r) ��� 1196 invariant cmp l ��� 1197 invariant cmp r 1198 ��� 1199 invariant cmp (rotateL k v l r) ��� 1200 to_fmap cmp (rotateL k v l r) = 1201 (FUNION (to_fmap cmp l) (to_fmap cmp r)) |+ (key_set cmp k,v)`, 1202 Cases_on `r` 1203 >- fs [size_def] >> 1204 rw [size_def, rotateL_def] >> 1205 metis_tac [singleL_thm, doubleL_thm, ADD_COMM, NOT_ZERO_LT_ZERO, GREATER_DEF]); 1206 1207val balanceR_balR = Q.prove ( 1208`!k v l r cmp. 1209 good_cmp cmp ��� 1210 invariant cmp l ��� 1211 invariant cmp r 1212 ��� 1213 balanceR k v l r = balR k v l r`, 1214 ho_match_mp_tac balanceR_ind >> 1215 rw [] >> 1216 rw [balanceR_def, balR_def, rotateL_def, doubleL_def, bin_def, singleL_def] >> 1217 imp_res_tac structure_size_thm >> 1218 fs [size_def, invariant_def, structure_size_def] >> 1219 imp_res_tac structure_size_thm >> 1220 fs [balanced_def] >> 1221 TRY (Cases_on `l` >> fs [structure_size_def, size_def] >> NO_TAC) >> 1222 TRY (Cases_on `r` >> fs [structure_size_def, size_def] >> NO_TAC) >> 1223 TRY (Cases_on `v4` >> fs [structure_size_def, size_def] >> NO_TAC) >> 1224 TRY (fs [ratio_def] >> NO_TAC) >> 1225 every_case_tac >> 1226 fs [size_def, structure_size_def, ratio_def, delta_def] >> 1227 imp_res_tac structure_size_thm >> 1228 fs [invariant_def, doubleL_def, bin_def, size_def] >> 1229 imp_res_tac structure_size_thm >> 1230 rw []); 1231 1232val balanceR_thm = Q.prove ( 1233`!k v l r cmp. 1234 good_cmp cmp ��� 1235 key_ordered cmp k r Less ��� 1236 key_ordered cmp k l Greater ��� 1237 almost_balancedR (size l) (size r) ��� 1238 invariant cmp l ��� 1239 invariant cmp r 1240 ��� 1241 invariant cmp (balanceR k v l r) ��� 1242 to_fmap cmp (balanceR k v l r) = 1243 (FUNION (to_fmap cmp l) (to_fmap cmp r)) |+ (key_set cmp k,v)`, 1244 rw [] >> 1245 `balanceR k v l r = balR k v l r` by metis_tac [balanceR_balR] >> 1246 rw [balR_def, invariant_def] >> 1247 imp_res_tac structure_size_thm >> 1248 rw [balanced_lem1, balanced_lem5, to_fmap_def] >> 1249 metis_tac [rotateL_thm]); 1250 1251val almost_balancedL_thm = Q.prove ( 1252`!l r. 1253 balanced l r ��� 1254 almost_balancedL l r ��� almost_balancedL (l + 1) r ��� almost_balancedL l (r - 1)`, 1255 rw [almost_balancedL_def] >> 1256 fs [balanced_def, NOT_LESS_EQUAL, TIMES_MIN] >> 1257 rw [] >> 1258 CCONTR_TAC >> 1259 fs [] >> 1260 fs [NOT_LESS_EQUAL] >> 1261 fs [delta_def, MIN_DEF]); 1262 1263val almost_balancedR_thm = Q.prove ( 1264`!l r. 1265 balanced l r ��� 1266 almost_balancedR l r ��� almost_balancedR l (r + 1) ��� almost_balancedR (l - 1) r`, 1267 rw [almost_balancedR_def] >> 1268 fs [balanced_def, NOT_LESS_EQUAL, TIMES_MIN] >> 1269 rw [] >> 1270 CCONTR_TAC >> 1271 fs [] >> 1272 fs [NOT_LESS_EQUAL] >> 1273 fs [delta_def, MIN_DEF] >> 1274 fs [NOT_LESS, LESS_OR_EQ] >> 1275 rw [] >> 1276 decide_tac); 1277 1278val insert_thm = Q.store_thm ("insert_thm", 1279`���t. 1280 good_cmp cmp ��� 1281 invariant cmp t 1282 ��� 1283 invariant cmp (insert cmp k v t) ��� 1284 to_fmap cmp (insert cmp k v t) = to_fmap cmp t |+ (key_set cmp k,v)`, 1285 Induct_on `t` 1286 >- fs [insert_def, singleton_def, to_fmap_def, invariant_eq, 1287 structure_size_def, balanced_def, size_def, key_ordered_def] >> 1288 simp [invariant_eq] >> 1289 rpt gen_tac >> 1290 strip_tac >> 1291 fs [insert_def] >> 1292 Cases_on `cmp k k'` >> 1293 fs [] >> 1294 simp [] >> 1295 TRY (inv_mp_tac balanceL_thm) >> 1296 TRY (inv_mp_tac balanceR_thm) >> 1297 conj_asm1_tac >> 1298 rw [to_fmap_def] 1299 >- (rfs [key_ordered_to_fmap] >> 1300 rw [] >> 1301 imp_res_tac to_fmap_key_set >> 1302 rw [key_set_cmp_thm] >> 1303 metis_tac [cmp_thms]) 1304 >- (imp_res_tac size_thm >> 1305 rw [FCARD_FUPDATE] >> 1306 fs [key_ordered_to_fmap] >> 1307 metis_tac [almost_balancedL_thm]) 1308 >- (rfs [key_ordered_to_fmap] >> 1309 rw [] >> 1310 `key_set cmp k ��� key_set cmp k'` by metis_tac [key_set_eq, cmp_thms] >> 1311 metis_tac [FUPDATE_COMMUTES]) 1312 >- (fs [invariant_def] >> 1313 rfs [key_ordered_to_fmap] >> 1314 metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms]) 1315 >- metis_tac [key_set_eq, FUPDATE_EQ] 1316 >- (rfs [key_ordered_to_fmap] >> 1317 rw [] >> 1318 imp_res_tac to_fmap_key_set >> 1319 rw [key_set_cmp_thm] >> 1320 metis_tac [cmp_thms]) 1321 >- (imp_res_tac size_thm >> 1322 rw [FCARD_FUPDATE] >> 1323 fs [key_ordered_to_fmap] >> 1324 metis_tac [almost_balancedR_thm]) 1325 >- (rw [FUNION_FUPDATE_2, to_fmap_def] >> 1326 rfs [key_ordered_to_fmap] >> 1327 rw [] >> 1328 metis_tac [FUPDATE_COMMUTES, cmp_thms, to_fmap_key_set, key_set_cmp_thm])); 1329 1330val lookup_insert = Q.store_thm("lookup_insert", 1331 `good_cmp cmp ��� invariant cmp t ��� 1332 lookup cmp k (insert cmp k' v t) = 1333 if cmp k k' = Equal then SOME v else lookup cmp k t`, 1334 rw[] \\ rw[lookup_thm,insert_thm,FLOOKUP_UPDATE] \\ 1335 metis_tac[key_set_eq,comparisonTheory.cmp_thms]); 1336 1337val comparison_distinct = TypeBase.distinct_of ``:ordering`` 1338 1339val insertR_thm = Q.store_thm ("insertR_thm", 1340`���t. 1341 good_cmp cmp ��� 1342 invariant cmp t 1343 ��� 1344 invariant cmp (insertR cmp k v t) ��� 1345 to_fmap cmp (insertR cmp k v t) = 1346 if key_set cmp k ��� FDOM (to_fmap cmp t) then to_fmap cmp t else to_fmap cmp t |+ (key_set cmp k,v)`, 1347 Induct_on `t` 1348 >- fs [insertR_def, singleton_def, to_fmap_def, invariant_def, 1349 structure_size_def, balanced_def, size_def, key_ordered_def] >> 1350 rpt gen_tac >> 1351 strip_tac >> 1352 imp_res_tac inv_props >> 1353 fs [insertR_def, invariant_def] >> 1354 Cases_on `cmp k k'` >> 1355 fs [] >> 1356 simp [to_fmap_def] 1357 >- (`almost_balancedL (size (insertR cmp k v t)) (size t')` 1358 by (imp_res_tac size_thm >> 1359 rw [FCARD_FUPDATE] >> 1360 fs [key_ordered_to_fmap] >> 1361 metis_tac [almost_balancedL_thm]) >> 1362 `key_ordered cmp k' (insertR cmp k v t) Greater` 1363 by (rfs [key_ordered_to_fmap] >> 1364 rw [] >> 1365 rw [key_set_cmp_thm] >> 1366 metis_tac [good_cmp_def]) >> 1367 rw [balanceL_thm] >> 1368 imp_res_tac balanceL_thm >> 1369 rw [FUNION_FUPDATE_1] >> 1370 metis_tac [FUPDATE_COMMUTES, good_cmp_def, comparison_distinct]) 1371 >- (fs [invariant_def] >> 1372 rfs [key_ordered_to_fmap] >> 1373 metis_tac [to_fmap_key_set, key_set_cmp_thm, cmp_thms,key_set_eq, FUPDATE_EQ]) 1374 >- (`almost_balancedR (size t) (size (insertR cmp k v t'))` 1375 by (imp_res_tac size_thm >> 1376 rw [FCARD_FUPDATE] >> 1377 fs [key_ordered_to_fmap] >> 1378 metis_tac [almost_balancedR_thm]) >> 1379 `key_ordered cmp k' (insertR cmp k v t') Less` 1380 by (fs [key_ordered_to_fmap] >> 1381 rw [] >> 1382 imp_res_tac to_fmap_key_set >> 1383 rw [key_set_cmp_thm] >> 1384 metis_tac [cmp_thms]) >> 1385 rw [balanceR_thm] >> 1386 imp_res_tac balanceR_thm >> 1387 rw [FUNION_FUPDATE_2] >> 1388 rfs [key_ordered_to_fmap] >> 1389 metis_tac [FUPDATE_COMMUTES, good_cmp_def, comparison_distinct])); 1390 1391val insertMax_thm = Q.store_thm ("insertMax_thm", 1392`���t. 1393 good_cmp cmp ��� 1394 invariant cmp t ��� 1395 (!k1. k1 ��� FDOM (to_fmap cmp t) ��� key_set_cmp cmp k k1 Greater) 1396 ��� 1397 invariant cmp (insertMax k v t) ��� 1398 to_fmap cmp (insertMax k v t) = to_fmap cmp t |+ (key_set cmp k,v)`, 1399 Induct_on `t` 1400 >- fs [insertMax_def, singleton_def, to_fmap_def, invariant_def, 1401 structure_size_def, balanced_def, size_def, key_ordered_def] >> 1402 rpt gen_tac >> 1403 strip_tac >> 1404 fs [insertMax_def, invariant_def, to_fmap_def] >> 1405 inv_mp_tac balanceR_thm >> 1406 conj_asm1_tac >> 1407 simp [] 1408 >- (rfs [key_ordered_to_fmap] >> 1409 imp_res_tac size_thm >> 1410 rw [FCARD_FUPDATE] >> 1411 fs [] >> 1412 metis_tac [almost_balancedR_thm, good_cmp_def, key_set_cmp_thm]) >> 1413 rw [FUNION_FUPDATE_2] >> 1414 rfs [key_ordered_to_fmap] >> 1415 metis_tac [FUPDATE_COMMUTES, cmp_thms, key_set_cmp_thm]); 1416 1417val insertMin_thm = Q.store_thm ("insertMin_thm", 1418`���t. 1419 good_cmp cmp ��� 1420 invariant cmp t ��� 1421 (!k1. k1 ��� FDOM (to_fmap cmp t) ��� key_set_cmp cmp k k1 Less) 1422 ��� 1423 invariant cmp (insertMin k v t) ��� 1424 to_fmap cmp (insertMin k v t) = to_fmap cmp t |+ (key_set cmp k,v)`, 1425 Induct_on `t` 1426 >- fs [insertMin_def, singleton_def, to_fmap_def, invariant_def, 1427 structure_size_def, balanced_def, size_def, key_ordered_def] >> 1428 rpt gen_tac >> 1429 strip_tac >> 1430 fs [insertMin_def, invariant_def, to_fmap_def] >> 1431 simp [] >> 1432 `almost_balancedL (size (insertMin k v t)) (size t')` 1433 by (imp_res_tac size_thm >> 1434 rw [FCARD_FUPDATE] >> 1435 fs [key_ordered_to_fmap] >> 1436 metis_tac [almost_balancedL_thm]) >> 1437 `key_ordered cmp k' (insertMin k v t) Greater` 1438 by (rfs [key_ordered_to_fmap] >> 1439 rw [] >> 1440 imp_res_tac to_fmap_key_set >> 1441 rw [key_set_cmp_thm] >> 1442 metis_tac [cmp_thms, key_set_cmp_thm]) >> 1443 rw [balanceL_thm] >> 1444 imp_res_tac balanceL_thm >> 1445 rw [FUNION_FUPDATE_1] >> 1446 metis_tac [FUPDATE_COMMUTES, cmp_thms, key_set_cmp_thm]); 1447 1448val deleteFindMin_thm = Q.store_thm ("deleteFindMin", 1449`���t t' k v. 1450 good_cmp cmp ��� 1451 invariant cmp t ��� 1452 ~null t ��� 1453 deleteFindMin t = ((k,v),t') 1454 ��� 1455 invariant cmp t' ��� 1456 key_ordered cmp k t' Less ��� 1457 FLOOKUP (to_fmap cmp t) (key_set cmp k) = SOME v ��� 1458 to_fmap cmp t' = 1459 DRESTRICT (to_fmap cmp t) (FDOM (to_fmap cmp t) DELETE key_set cmp k)`, 1460 ho_match_mp_tac (fetch "-" "deleteFindMin_ind") >> 1461 rpt conj_tac >> 1462 rpt gen_tac >> 1463 strip_tac >> 1464 rpt gen_tac >> 1465 TRY DISCH_TAC >> 1466 fs [deleteFindMin_def, invariant_eq, to_fmap_def] >> 1467 fs [null_def, to_fmap_def, FUNION_FEMPTY_1, deleteFindMin_def] >> 1468 BasicProvers.VAR_EQ_TAC >> 1469 fs [to_fmap_def, FLOOKUP_UPDATE, key_ordered_def, LET_THM, null_def] 1470 >- (rw [] >> 1471 fs [key_ordered_to_fmap] >> 1472 rw [FLOOKUP_EXT, FLOOKUP_UPDATE, FLOOKUP_DRESTRICT, FUN_EQ_THM] >> 1473 rw [flookup_thm] >> 1474 fs [] >> 1475 metis_tac [comparison_distinct, good_cmp_def]) >> 1476 `?km l. deleteFindMin (Bin (structure_size v8 + (structure_size v9 + 1)) v6 v7 v8 v9) = (km,l)` 1477 by metis_tac [pairTheory.pair_CASES] >> 1478 fs [] >> 1479 rpt BasicProvers.VAR_EQ_TAC >> 1480 inv_mp_tac balanceR_thm >> 1481 simp [] >> 1482 Cases_on `key_set cmp v6 = key_set cmp k'` >> 1483 fs [] 1484 >- (`FDOM (to_fmap cmp l) = FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9)` 1485 by (FIRST_ASSUM (assume_tac o MATCH_MP (METIS_PROVE [] ``m1 = m2 ��� FDOM m1 = FDOM m2``)) >> 1486 fs [FDOM_DRESTRICT, EXTENSION] >> 1487 rfs [key_ordered_to_fmap] >> 1488 metis_tac [cmp_thms]) >> 1489 conj_asm1_tac 1490 >- (rw [] 1491 >- (rfs [key_ordered_to_fmap] >> 1492 metis_tac []) 1493 >- (fs [size_def] >> 1494 imp_res_tac size_thm >> 1495 rw [DELETE_INSERT, FCARD_DRESTRICT] >> 1496 `key_set cmp k' ��� FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9)` 1497 by (fs [key_ordered_to_fmap] >> 1498 metis_tac [good_cmp_def, comparison_distinct]) >> 1499 imp_res_tac DELETE_NON_ELEMENT >> 1500 rw [CARD_DISJOINT_UNION] >> 1501 imp_res_tac almost_balancedR_thm >> 1502 fs [] >> 1503 metis_tac [FCARD_DEF, structure_size_thm, size_thm])) >> 1504 strip_tac >> 1505 simp [] >> 1506 rw [FLOOKUP_EXT, FLOOKUP_UPDATE, FLOOKUP_DRESTRICT, FLOOKUP_FUNION, 1507 FUN_EQ_THM] 1508 >- (rfs [key_ordered_to_fmap, FDOM_DRESTRICT] >> 1509 fs [key_ordered_to_fmap, FDOM_DRESTRICT] >> 1510 rw [] >> 1511 imp_res_tac to_fmap_key_set >> 1512 rw [key_set_cmp_thm] >> 1513 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm]) >> 1514 every_case_tac >> 1515 fs [flookup_thm,key_ordered_to_fmap] >> 1516 rfs [key_ordered_to_fmap] >> 1517 rw [] >> 1518 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm]) 1519 >- (`key_set cmp k' ��� FDOM (to_fmap cmp v8 ��� to_fmap cmp v9)` 1520 by (every_case_tac >> 1521 fs [FLOOKUP_DEF]) >> 1522 `key_set cmp k ��� key_set cmp k' ��� cmp k' k = Less` 1523 by (rfs [key_ordered_to_fmap] >> 1524 fs [key_ordered_to_fmap] >> 1525 metis_tac [cmp_thms, to_fmap_key_set, key_set_cmp_thm]) >> 1526 simp [] >> 1527 `FDOM (to_fmap cmp l) = (key_set cmp v6 INSERT FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9)) DELETE key_set cmp k'` 1528 by (FIRST_ASSUM (assume_tac o MATCH_MP (METIS_PROVE [] ``m1 = m2 ��� FDOM m1 = FDOM m2``)) >> 1529 fs [FDOM_DRESTRICT, EXTENSION] >> 1530 rfs [key_ordered_to_fmap] >> 1531 metis_tac [cmp_thms]) >> 1532 conj_asm1_tac 1533 >- (rw [] 1534 >- (rfs [key_ordered_to_fmap] >> 1535 fs [key_ordered_to_fmap] >> 1536 rw [key_set_cmp_thm] >> 1537 metis_tac [key_set_cmp_thm, to_fmap_key_set]) 1538 >- (imp_res_tac size_thm >> 1539 rw [FCARD_FUPDATE, FDOM_DRESTRICT] >> 1540 rw [FCARD_DRESTRICT, DELETE_INSERT] >> 1541 `(FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9)) ��� 1542 (key_set cmp v6 INSERT FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9) DELETE key_set cmp k') 1543 = 1544 FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9) DELETE key_set cmp k'` 1545 by (rw [EXTENSION] >> 1546 metis_tac [key_set_eq, EXTENSION]) >> 1547 simp [CARD_UNION_EQN] >> 1548 fs [DISJOINT_DEF] >| 1549 [`CARD (FDOM (to_fmap cmp v8)) ��� 0` 1550 by (rw [CARD_EQ_0, EXTENSION] >> 1551 metis_tac []) >> 1552 `0 < CARD (FDOM (to_fmap cmp v8))` by decide_tac, 1553 `CARD (FDOM (to_fmap cmp v9)) ��� 0` 1554 by (rw [CARD_EQ_0, EXTENSION] >> 1555 metis_tac []) >> 1556 `0 < CARD (FDOM (to_fmap cmp v9))` by decide_tac] >> 1557 rw [] >> 1558 imp_res_tac almost_balancedR_thm >> 1559 fs [size_def] >> 1560 metis_tac [FCARD_DEF, structure_size_thm, size_thm])) >> 1561 strip_tac >> 1562 simp [] >> 1563 rw [FLOOKUP_EXT, FLOOKUP_UPDATE, FLOOKUP_DRESTRICT, FLOOKUP_FUNION, 1564 FUN_EQ_THM] 1565 >- (rfs [key_ordered_to_fmap, FDOM_DRESTRICT] >> 1566 fs [key_ordered_to_fmap, FDOM_DRESTRICT] >> 1567 rw [] >> 1568 imp_res_tac to_fmap_key_set >> 1569 rw [key_set_cmp_thm] >> 1570 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm]) >> 1571 every_case_tac >> 1572 fs [flookup_thm,key_ordered_to_fmap] >> 1573 rfs [key_ordered_to_fmap] >> 1574 rw [] >> 1575 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm])); 1576 1577val deleteFindMax_thm = Q.store_thm ("deleteFindMax", 1578`���t t' k v. 1579 good_cmp cmp ��� 1580 invariant cmp t ��� 1581 ~null t ��� 1582 deleteFindMax t = ((k,v),t') 1583 ��� 1584 invariant cmp t' ��� 1585 key_ordered cmp k t' Greater ��� 1586 FLOOKUP (to_fmap cmp t) (key_set cmp k) = SOME v ��� 1587 to_fmap cmp t' = 1588 DRESTRICT (to_fmap cmp t) (FDOM (to_fmap cmp t) DELETE key_set cmp k)`, 1589 ho_match_mp_tac (fetch "-" "deleteFindMax_ind") >> 1590 rpt conj_tac >> 1591 rpt gen_tac >> 1592 strip_tac >> 1593 rpt gen_tac >> 1594 TRY DISCH_TAC >> 1595 fs [deleteFindMax_def, invariant_eq, to_fmap_def] >> 1596 fs [null_def, to_fmap_def, FUNION_FEMPTY_2, deleteFindMax_def] >> 1597 BasicProvers.VAR_EQ_TAC >> 1598 fs [to_fmap_def, FLOOKUP_UPDATE, key_ordered_def, LET_THM, null_def] 1599 >- (rw [] >> 1600 fs [key_ordered_to_fmap] >> 1601 rw [FLOOKUP_EXT, FLOOKUP_UPDATE, FLOOKUP_DRESTRICT, FUN_EQ_THM] >> 1602 rw [flookup_thm] >> 1603 fs [] >> 1604 metis_tac [comparison_distinct, good_cmp_def]) >> 1605 `?km l. deleteFindMax (Bin (structure_size v8 + (structure_size v9 + 1)) v6 v7 v8 v9) = (km,l)` 1606 by metis_tac [pairTheory.pair_CASES] >> 1607 fs [] >> 1608 rpt BasicProvers.VAR_EQ_TAC >> 1609 inv_mp_tac balanceL_thm >> 1610 simp [] >> 1611 Cases_on `key_set cmp v6 = key_set cmp k'` >> 1612 fs [] 1613 >- (`FDOM (to_fmap cmp l') = FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9)` 1614 by (FIRST_ASSUM (assume_tac o MATCH_MP (METIS_PROVE [] ``m1 = m2 ��� FDOM m1 = FDOM m2``)) >> 1615 fs [FDOM_DRESTRICT, EXTENSION] >> 1616 rfs [key_ordered_to_fmap] >> 1617 metis_tac [cmp_thms]) >> 1618 conj_asm1_tac 1619 >- (rw [] 1620 >- (rfs [key_ordered_to_fmap] >> 1621 metis_tac []) 1622 >- (fs [size_def] >> 1623 imp_res_tac size_thm >> 1624 rw [DELETE_INSERT, FCARD_DRESTRICT] >> 1625 `key_set cmp k' ��� FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9)` 1626 by (fs [key_ordered_to_fmap] >> 1627 metis_tac [good_cmp_def, comparison_distinct]) >> 1628 imp_res_tac DELETE_NON_ELEMENT >> 1629 rw [CARD_DISJOINT_UNION] >> 1630 imp_res_tac almost_balancedL_thm >> 1631 fs [] >> 1632 metis_tac [FCARD_DEF, structure_size_thm, size_thm])) >> 1633 strip_tac >> 1634 simp [] >> 1635 rw [FLOOKUP_EXT, FLOOKUP_UPDATE, FLOOKUP_DRESTRICT, FLOOKUP_FUNION, 1636 FUN_EQ_THM] 1637 >- (rfs [key_ordered_to_fmap, FDOM_DRESTRICT] >> 1638 fs [key_ordered_to_fmap, FDOM_DRESTRICT] >> 1639 rw [] >> 1640 imp_res_tac to_fmap_key_set >> 1641 rw [key_set_cmp_thm] >> 1642 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm]) >> 1643 every_case_tac >> 1644 fs [flookup_thm,key_ordered_to_fmap] >> 1645 rfs [key_ordered_to_fmap] >> 1646 rw [] >> 1647 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm]) 1648 >- (`key_set cmp k' ��� FDOM (to_fmap cmp v8 ��� to_fmap cmp v9)` 1649 by (every_case_tac >> 1650 fs [FLOOKUP_DEF]) >> 1651 `key_set cmp k' ��� key_set cmp k ��� cmp k' k = Greater` 1652 by (rfs [key_ordered_to_fmap] >> 1653 fs [key_ordered_to_fmap] >> 1654 metis_tac [cmp_thms, to_fmap_key_set, key_set_cmp_thm]) >> 1655 simp [] >> 1656 `FDOM (to_fmap cmp l') = (key_set cmp v6 INSERT FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9)) DELETE key_set cmp k'` 1657 by (FIRST_ASSUM (assume_tac o MATCH_MP (METIS_PROVE [] ``m1 = m2 ��� FDOM m1 = FDOM m2``)) >> 1658 fs [FDOM_DRESTRICT, EXTENSION] >> 1659 metis_tac [comparison_distinct, key_ordered_to_fmap, good_cmp_def]) >> 1660 conj_asm1_tac 1661 >- (rw [] 1662 >- (rfs [key_ordered_to_fmap] >> 1663 fs [key_ordered_to_fmap] >> 1664 rw [key_set_cmp_thm] >> 1665 metis_tac [key_set_cmp_thm, to_fmap_key_set]) 1666 >- (imp_res_tac size_thm >> 1667 rw [FCARD_FUPDATE, FDOM_DRESTRICT] >> 1668 rw [FCARD_DRESTRICT, DELETE_INSERT] >> 1669 `(FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9)) ��� 1670 (key_set cmp v6 INSERT FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9) DELETE key_set cmp k') 1671 = 1672 FDOM (to_fmap cmp v8) ��� FDOM (to_fmap cmp v9) DELETE key_set cmp k'` 1673 by (rw [EXTENSION] >> 1674 metis_tac [key_set_eq, EXTENSION]) >> 1675 simp [CARD_UNION_EQN] >> 1676 fs [DISJOINT_DEF] >| 1677 [`CARD (FDOM (to_fmap cmp v8)) ��� 0` 1678 by (rw [CARD_EQ_0, EXTENSION] >> 1679 metis_tac []) >> 1680 `0 < CARD (FDOM (to_fmap cmp v8))` by decide_tac, 1681 `CARD (FDOM (to_fmap cmp v9)) ��� 0` 1682 by (rw [CARD_EQ_0, EXTENSION] >> 1683 metis_tac []) >> 1684 `0 < CARD (FDOM (to_fmap cmp v9))` by decide_tac] >> 1685 rw [] >> 1686 imp_res_tac almost_balancedL_thm >> 1687 fs [size_def] >> 1688 metis_tac [FCARD_DEF, structure_size_thm, size_thm])) >> 1689 strip_tac >> 1690 simp [] >> 1691 rw [FLOOKUP_EXT, FLOOKUP_UPDATE, FLOOKUP_DRESTRICT, FLOOKUP_FUNION, 1692 FUN_EQ_THM] 1693 >- (rfs [key_ordered_to_fmap, FDOM_DRESTRICT] >> 1694 fs [key_ordered_to_fmap, FDOM_DRESTRICT] >> 1695 rw [] >> 1696 imp_res_tac to_fmap_key_set >> 1697 rw [key_set_cmp_thm] >> 1698 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm]) >> 1699 every_case_tac >> 1700 fs [flookup_thm,key_ordered_to_fmap] >> 1701 rfs [key_ordered_to_fmap] >> 1702 rw [] >> 1703 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm])); 1704 1705 1706val FLOOKUP_EXT' = FLOOKUP_EXT |> SIMP_RULE (srw_ss()) [FUN_EQ_THM] 1707val glue_thm = Q.store_thm ("glue_thm", 1708`!l r. 1709 good_cmp cmp ��� 1710 invariant cmp l ��� 1711 invariant cmp r ��� 1712 (!ks ks'. ks ��� FDOM (to_fmap cmp l) ��� ks' ��� FDOM (to_fmap cmp r) ��� key_set_cmp2 cmp ks ks' Less) ��� 1713 balanced (size l) (size r) 1714 ��� 1715 invariant cmp (glue l r) ��� 1716 to_fmap cmp (glue l r) = FUNION (to_fmap cmp l) (to_fmap cmp r)`, 1717 Cases_on `l` >> 1718 Cases_on `r` >> 1719 simp [size_def, glue_def] >> 1720 TRY (simp [to_fmap_def, FUNION_FEMPTY_2, FUNION_FEMPTY_1] >> NO_TAC) >> 1721 strip_tac >> 1722 Cases_on `n > n'` >> 1723 simp [] 1724 >- (`?k' v' l. deleteFindMax (Bin n k v b b0) = ((k',v'),l)` 1725 by metis_tac [pairTheory.pair_CASES] >> 1726 simp [] >> 1727 inv_mp_tac balanceR_thm >> 1728 simp [] >> 1729 inv_to_front_tac ``invariant`` >> 1730 inv_mp_tac deleteFindMax_thm >> 1731 simp [Once SWAP_EXISTS_THM] >> 1732 qexists_tac `Bin n k v b b0` >> 1733 simp [null_def] >> 1734 strip_tac >> 1735 imp_res_tac fdom_eq >> 1736 fs [FDOM_DRESTRICT, DELETE_INSERT, FLOOKUP_UPDATE] >> 1737 fs [DELETE_INTER2] >> 1738 rw [] 1739 >- (rw [FLOOKUP_EXT', FLOOKUP_FUNION, FLOOKUP_UPDATE, FLOOKUP_DRESTRICT] >> 1740 every_case_tac >> 1741 fs [invariant_eq, FLOOKUP_DEF] >> 1742 metis_tac [good_cmp_def, comparison_distinct]) 1743 >- (rfs [key_ordered_to_fmap] >> 1744 fs [FLOOKUP_DEF] >> 1745 rw [] >> 1746 imp_res_tac to_fmap_key_set >> 1747 rw [key_set_cmp_thm] >> 1748 metis_tac [cmp_thms, key_set_cmp2_thm]) 1749 >- (fs [invariant_eq] >> 1750 `size l = size (Bin n k v b b0) - 1` 1751 by (rw [size_def] >> 1752 imp_res_tac size_thm >> 1753 rw [FCARD_DEF, FDOM_FUPDATE, FDOM_DRESTRICT, to_fmap_def, 1754 CARD_DISJOINT_UNION, DELETE_INTER2] >> 1755 fs [to_fmap_def, FLOOKUP_DEF] >> 1756 metis_tac [structure_size_thm, FCARD_DEF]) >> 1757 imp_res_tac almost_balancedR_thm >> 1758 fs [size_def] >> 1759 rw [] >> 1760 FULL_SIMP_TAC (srw_ss()++ARITH_ss) [])) 1761 >- (`?k v l. deleteFindMin (Bin n' k' v' b' b0') = ((k,v),l)` 1762 by metis_tac [pairTheory.pair_CASES] >> 1763 simp [] >> 1764 inv_mp_tac balanceL_thm >> 1765 simp [] >> 1766 inv_to_front_tac ``invariant`` >> 1767 inv_mp_tac deleteFindMin_thm >> 1768 simp [Once SWAP_EXISTS_THM] >> 1769 qexists_tac `Bin n' k' v' b' b0'` >> 1770 simp [null_def] >> 1771 strip_tac >> 1772 imp_res_tac fdom_eq >> 1773 fs [FDOM_DRESTRICT, DELETE_INSERT, FLOOKUP_UPDATE] >> 1774 fs [DELETE_INTER2] >> 1775 rw [] 1776 >- (rw [FLOOKUP_EXT', FLOOKUP_FUNION, FLOOKUP_UPDATE, FLOOKUP_DRESTRICT] >> 1777 every_case_tac 1778 >- metis_tac [] >> 1779 fs [invariant_eq, FLOOKUP_DEF] 1780 >- metis_tac [cmp_thms, key_set_cmp2_thm]) 1781 >- (rfs [key_ordered_to_fmap] >> 1782 fs [FLOOKUP_DEF] >> 1783 rw [] >> 1784 imp_res_tac to_fmap_key_set >> 1785 rw [key_set_cmp_thm] >> 1786 metis_tac [cmp_thms, key_set_cmp2_thm]) 1787 >- (fs [invariant_eq] >> 1788 `size l = size (Bin n' k' v' b' b0') - 1` 1789 by (rw [size_def] >> 1790 imp_res_tac size_thm >> 1791 rw [FCARD_DEF, FDOM_FUPDATE, FDOM_DRESTRICT, to_fmap_def, 1792 CARD_DISJOINT_UNION, DELETE_INTER2] >> 1793 fs [to_fmap_def, FLOOKUP_DEF] >> 1794 metis_tac [structure_size_thm, FCARD_DEF]) >> 1795 imp_res_tac almost_balancedL_thm >> 1796 fs [size_def] >> 1797 rw [] >> 1798 FULL_SIMP_TAC (srw_ss()++ARITH_ss) []))); 1799 1800val to_fmap_tac = 1801 rw [to_fmap_def] >> 1802 rw [FLOOKUP_EXT', FLOOKUP_DRESTRICT, FLOOKUP_UPDATE, FLOOKUP_FUNION] >> 1803 BasicProvers.EVERY_CASE_TAC >> 1804 fs [FLOOKUP_DEF] >> 1805 fs [to_fmap_def] >> 1806 fs [key_ordered_to_fmap] >> 1807 rfs [key_ordered_to_fmap] >> 1808 metis_tac [cmp_thms, to_fmap_key_set, key_set_eq, key_set_cmp_thm]; 1809 1810val delete_thm = Q.store_thm ("delete_thm", 1811`!t. 1812 good_cmp cmp ��� 1813 invariant cmp t 1814 ��� 1815 invariant cmp (delete cmp k t) ��� 1816 to_fmap cmp (delete cmp k t) = 1817 DRESTRICT (to_fmap cmp t) (FDOM (to_fmap cmp t) DELETE key_set cmp k)`, 1818 Induct_on `t` 1819 >- rw [delete_def, to_fmap_def] >> 1820 rpt gen_tac >> 1821 strip_tac >> 1822 simp [delete_def] >> 1823 fs [invariant_eq] >> 1824 Cases_on `cmp k k'` >> 1825 simp [] 1826 >- (inv_mp_tac balanceR_thm >> 1827 simp [] >> 1828 rw [] 1829 >- (fs [key_ordered_to_fmap] >> 1830 rfs [key_ordered_to_fmap] >> 1831 rw [FDOM_DRESTRICT] >> 1832 metis_tac [to_fmap_key_set, key_set_cmp_thm]) 1833 >- (imp_res_tac size_thm >> 1834 rw [FCARD_DRESTRICT, DELETE_INTER2] >> 1835 imp_res_tac almost_balancedR_thm >> 1836 metis_tac [FCARD_DEF]) 1837 >- to_fmap_tac) 1838 >- (inv_mp_tac glue_thm >> 1839 rw [] >> 1840 rfs [key_ordered_to_fmap] 1841 >- metis_tac [key_set_cmp2_thm, to_fmap_key_set, key_set_cmp_thm, cmp_thms] 1842 >- to_fmap_tac) 1843 >- (inv_mp_tac balanceL_thm >> 1844 simp [] >> 1845 rw [] 1846 >- (fs [key_ordered_to_fmap] >> 1847 rfs [key_ordered_to_fmap] >> 1848 rw [FDOM_DRESTRICT] >> 1849 metis_tac [to_fmap_key_set, key_set_cmp_thm]) 1850 >- (imp_res_tac size_thm >> 1851 rw [FCARD_DRESTRICT, DELETE_INTER2] >> 1852 imp_res_tac almost_balancedL_thm >> 1853 metis_tac [FCARD_DEF]) 1854 >- to_fmap_tac)); 1855 1856val restrict_set_def = Define ` 1857restrict_set cmp lo hi = 1858{ k | option_cmp cmp lo (SOME k) = Less ��� 1859 option_cmp2 cmp (SOME k) hi = Less }`; 1860 1861val restrict_domain_def = Define ` 1862 restrict_domain cmp lo hi m = 1863 DRESTRICT m (IMAGE (key_set cmp) (restrict_set cmp lo hi))`; 1864 1865val restrict_domain_union = Q.prove ( 1866`restrict_domain cmp lo hi (FUNION m1 m2) = 1867 FUNION (restrict_domain cmp lo hi m1) (restrict_domain cmp lo hi m2)`, 1868 rw [restrict_domain_def, FLOOKUP_EXT', FLOOKUP_DRESTRICT, FLOOKUP_FUNION] >> 1869 rw [FLOOKUP_DRESTRICT, FLOOKUP_FUNION]); 1870 1871val restrict_domain_update = Q.prove ( 1872`good_cmp cmp 1873 ��� 1874 restrict_domain cmp lo hi (m1 |+ (key_set cmp k,v)) = 1875 if k ��� restrict_set cmp lo hi then 1876 restrict_domain cmp lo hi m1 |+ (key_set cmp k,v) 1877 else 1878 restrict_domain cmp lo hi m1`, 1879 rw [restrict_domain_def, FLOOKUP_EXT', FLOOKUP_DRESTRICT, FLOOKUP_FUNION] >> 1880 rfs [key_set_eq] >> 1881 fs [restrict_set_def] >> 1882 Cases_on `hi` >> 1883 Cases_on `lo` >> 1884 fs [option_cmp_def, option_cmp2_def] >> 1885 metis_tac [cmp_thms]); 1886 1887val bounded_root_def = Define ` 1888 bounded_root cmp lk hk t ��� 1889 !s k v l r. t = Bin s k v l r ��� k ��� restrict_set cmp lk hk`; 1890 1891val trim_thm = Q.prove ( 1892`!t lk hk cmp. 1893 good_cmp cmp ��� 1894 invariant cmp t 1895 ��� 1896 invariant cmp (trim cmp lk hk t) ��� 1897 bounded_root cmp lk hk (trim cmp lk hk t) ��� 1898 to_fmap cmp (trim cmp lk hk t) SUBMAP to_fmap cmp t ��� 1899 restrict_domain cmp lk hk (to_fmap cmp (trim cmp lk hk t)) = 1900 restrict_domain cmp lk hk (to_fmap cmp t)`, 1901 Cases_on `lk` >> 1902 Cases_on `hk` >> 1903 simp [bounded_root_def, trim_def, restrict_set_def, option_cmp_def, option_cmp2_def] >> 1904 Induct_on `t` >> 1905 simp [trim_help_lesser_def, trim_help_greater_def, trim_help_middle_def, key_ordered_def] >> 1906 fs [invariant_eq] >> 1907 rpt gen_tac >> 1908 strip_tac >> 1909 every_case_tac >> 1910 fs [] >> 1911 simp [to_fmap_def] >> 1912 fs [SUBMAP_DEF, restrict_domain_def, DRESTRICTED_FUNION, DRESTRICT_FUPDATE] >> 1913 rw [invariant_def] >> 1914 rw [FAPPLY_FUPDATE_THM, FUNION_DEF, FLOOKUP_EXT', FLOOKUP_DRESTRICT, 1915 FLOOKUP_FUNION, FLOOKUP_UPDATE] >> 1916 rw [] >> 1917 every_case_tac >> 1918 fs [flookup_thm, key_ordered_to_fmap, restrict_set_def, option_cmp_def, option_cmp2_def] >> 1919 rfs [key_ordered_to_fmap] >> 1920 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm, to_fmap_key_set]); 1921val _ = print "Proved trim_thm\n"; 1922 1923val link_balanced_lem1 = Q.prove ( 1924`!r rz l. 1925 balanced r rz ��� 1926 delta * (l + 1) < r + (rz + 1) 1927 ��� 1928 almost_balancedL (l + (r + 2)) rz`, 1929 fs [almost_balancedL_def, balanced_def, TIMES_MIN, LESS_OR_EQ, delta_def, LEFT_ADD_DISTRIB] >> 1930 CCONTR_TAC >> 1931 fs [NOT_LESS, LESS_OR_EQ] >> 1932 fs [MIN_DEF] >> 1933 rw [] >> 1934 every_case_tac >> 1935 fs [NOT_LESS, LESS_OR_EQ]); 1936 1937val link_balanced_lem2 = Q.prove ( 1938`!r l ly. 1939 balanced ly l ��� 1940 ��(delta * (l + (ly + 1)) < r + 1) ��� 1941 delta * (r + 1) < l + (ly + 1) 1942 ��� 1943 almost_balancedR ly (SUC (l + r) + 1)`, 1944 fs [ADD1, almost_balancedR_def, balanced_def, TIMES_MIN, LESS_OR_EQ, delta_def, LEFT_ADD_DISTRIB] >> 1945 CCONTR_TAC >> 1946 fs [NOT_LESS, LESS_OR_EQ] >> 1947 fs [MIN_DEF] >> 1948 rw [] >> 1949 every_case_tac >> 1950 fs [NOT_LESS, LESS_OR_EQ]); 1951 1952val link_balanced_lem3 = Q.prove ( 1953`!r l. 1954 ��(delta * (l + 1) < r + 1) ��� 1955 ��(delta * (r + 1) < l + 1) 1956 ��� 1957 balanced (l + 1) (r + 1)`, 1958 fs [ADD1, balanced_def, TIMES_MIN, LESS_OR_EQ, delta_def, LEFT_ADD_DISTRIB] >> 1959 CCONTR_TAC >> 1960 fs [NOT_LESS, LESS_OR_EQ, MIN_DEF]); 1961 1962val link_thm = Q.prove ( 1963`!k v l r. 1964 good_cmp cmp ��� 1965 invariant cmp l ��� 1966 invariant cmp r ��� 1967 key_ordered cmp k l Greater ��� 1968 key_ordered cmp k r Less 1969 ��� 1970 invariant cmp (link k v l r) ��� 1971 to_fmap cmp (link k v l r) = 1972 (FUNION (to_fmap cmp l) (to_fmap cmp r)) |+ (key_set cmp k,v)`, 1973 ho_match_mp_tac (fetch "-" "link_ind") >> 1974 rpt conj_tac >> 1975 simp [link_def] >> 1976 rpt conj_tac >> 1977 rpt gen_tac >> 1978 strip_tac 1979 >- (inv_mp_tac insertMin_thm >> 1980 rw [] 1981 >- metis_tac [key_ordered_to_fmap] >> 1982 rw [to_fmap_def, FUNION_FEMPTY_1]) 1983 >- (inv_mp_tac insertMax_thm >> 1984 rw [] 1985 >- metis_tac [key_ordered_to_fmap] >> 1986 rw [to_fmap_def, FUNION_FEMPTY_2]) >> 1987 Cases_on `sizeL * delta < sizeR` >> 1988 simp [] >> 1989 fs [] 1990 >- (strip_tac >> 1991 fs [invariant_eq, link_def, key_ordered_def] >> 1992 inv_mp_tac balanceL_thm >> 1993 simp [] >> 1994 rw [] 1995 >- (rfs [key_ordered_to_fmap, to_fmap_def] >> 1996 rw [] >> 1997 rw [key_set_cmp_thm] >> 1998 metis_tac [cmp_thms, key_set_cmp_thm, to_fmap_key_set]) 1999 >- (imp_res_tac size_thm >> 2000 rw [to_fmap_def] >> 2001 fs [] >> 2002 rfs [key_ordered_to_fmap] >> 2003 simp [FCARD_FUPDATE, key_set_eq] >> 2004 `key_set cmp k ��� FDOM (to_fmap cmp ly) ��� 2005 key_set cmp k ��� FDOM (to_fmap cmp l) ��� 2006 key_set cmp ky ��� FDOM (to_fmap cmp r) ��� 2007 key_set cmp k ��� FDOM (to_fmap cmp r)` 2008 by metis_tac [cmp_thms, key_set_cmp_thm] >> 2009 simp [FCARD_DEF] >> 2010 `DISJOINT (FDOM (to_fmap cmp ly) ��� FDOM (to_fmap cmp l)) (FDOM (to_fmap cmp r))` 2011 by (rw [DISJOINT_UNION] >> 2012 rw [DISJOINT_DEF, EXTENSION] >> 2013 metis_tac [cmp_thms, key_set_cmp_thm, to_fmap_key_set]) >> 2014 rw [CARD_DISJOINT_UNION] >> 2015 imp_res_tac structure_size_to_fmap >> 2016 fs [GSYM FCARD_DEF] >> 2017 metis_tac [link_balanced_lem1, ADD_ASSOC]) 2018 >- to_fmap_tac) >> 2019 Cases_on `sizeR * delta < sizeL` >> 2020 simp [] >> 2021 fs [] 2022 >- (strip_tac >> 2023 fs [invariant_eq, link_def, key_ordered_def] >> 2024 inv_mp_tac balanceR_thm >> 2025 simp [] >> 2026 rw [] 2027 >- (rfs [key_ordered_to_fmap, to_fmap_def] >> 2028 rw [] >> 2029 rw [key_set_cmp_thm] >> 2030 metis_tac [cmp_thms, key_set_cmp_thm, to_fmap_key_set]) 2031 >- (imp_res_tac size_thm >> 2032 rw [to_fmap_def] >> 2033 fs [] >> 2034 rfs [key_ordered_to_fmap] >> 2035 simp [FUNION_FUPDATE_2, FCARD_FUPDATE, key_set_eq] >> 2036 `key_set cmp k ��� FDOM (to_fmap cmp rz) ��� 2037 key_set cmp k ��� FDOM (to_fmap cmp l) ��� 2038 key_set cmp kz ��� FDOM (to_fmap cmp l) ��� 2039 key_set cmp k ��� FDOM (to_fmap cmp r)` 2040 by metis_tac [cmp_thms, key_set_cmp_thm] >> 2041 simp [FCARD_DEF] >> 2042 `DISJOINT (FDOM (to_fmap cmp l) ��� FDOM (to_fmap cmp r)) (FDOM (to_fmap cmp rz))` 2043 by (rw [DISJOINT_UNION] >> 2044 rw [DISJOINT_DEF, EXTENSION] >> 2045 metis_tac [cmp_thms, key_set_cmp_thm, to_fmap_key_set]) >> 2046 `DISJOINT (FDOM (to_fmap cmp l)) (FDOM (to_fmap cmp r))` 2047 by (rw [DISJOINT_UNION] >> 2048 rw [DISJOINT_DEF, EXTENSION] >> 2049 metis_tac [cmp_thms, key_set_cmp_thm, to_fmap_key_set]) >> 2050 rw [CARD_DISJOINT_UNION] >> 2051 imp_res_tac structure_size_to_fmap >> 2052 fs [GSYM FCARD_DEF] >> 2053 metis_tac [link_balanced_lem2, ADD_ASSOC]) 2054 >- to_fmap_tac) 2055 >- (simp [bin_def, size_def] >> 2056 rw [invariant_def, structure_size_def] >> 2057 fs [invariant_eq, size_def] 2058 >- metis_tac [link_balanced_lem3, structure_size_thm, ADD_ASSOC] >> 2059 to_fmap_tac)); 2060val _ = print "Proved link_thm\n" 2061 2062val filter_lt_help_thm = Q.prove ( 2063`!cmp bound t. 2064 good_cmp cmp ��� 2065 invariant cmp t 2066 ��� 2067 invariant cmp (filterLt_help cmp bound t) ��� 2068 to_fmap cmp (filterLt_help cmp bound t) = restrict_domain cmp NONE (SOME bound) (to_fmap cmp t)`, 2069 Induct_on `t` >> 2070 simp [to_fmap_def, filterLt_help_def, restrict_domain_union, restrict_domain_update] >> 2071 simp [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def] >> 2072 rpt gen_tac >> 2073 strip_tac >> 2074 Cases_on `cmp k bound` >> 2075 simp [] 2076 >- (inv_mp_tac link_thm >> 2077 conj_asm1_tac >> 2078 rw [] >> 2079 fs [invariant_eq] 2080 >- (rfs [key_ordered_to_fmap] >> 2081 rw [restrict_domain_def]) >> 2082 rw [restrict_domain_def, restrict_set_def, option_cmp_def, option_cmp2_def] >> 2083 to_fmap_tac) 2084 >- (fs [invariant_eq] >> 2085 rw [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def] >> 2086 to_fmap_tac) 2087 >- (first_x_assum inv_mp_tac >> 2088 fs [invariant_eq] >> 2089 rw [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def] >> 2090 to_fmap_tac)); 2091val _ = print "Proved filter_lt_help_thm\n" 2092 2093val filterLt_thm = Q.prove ( 2094`!cmp bound t. 2095 good_cmp cmp ��� 2096 invariant cmp t 2097 ��� 2098 invariant cmp (filterLt cmp bound t) ��� 2099 to_fmap cmp (filterLt cmp bound t) = restrict_domain cmp NONE bound (to_fmap cmp t)`, 2100 Cases_on `bound` >> 2101 simp [to_fmap_def, filterLt_def, restrict_domain_union, restrict_domain_update] >> 2102 simp [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def] >> 2103 rw [] >> 2104 imp_res_tac filter_lt_help_thm 2105 >- (rw [FLOOKUP_EXT', FLOOKUP_DRESTRICT] >> 2106 rw [] >> 2107 fs [FLOOKUP_DEF] >> 2108 metis_tac [to_fmap_key_set]) >> 2109 rw [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def]); 2110val _ = print "Proved filterLt_thm\n"; 2111 2112val filter_gt_help_thm = Q.prove ( 2113`!cmp bound t. 2114 good_cmp cmp ��� 2115 invariant cmp t 2116 ��� 2117 invariant cmp (filterGt_help cmp bound t) ��� 2118 to_fmap cmp (filterGt_help cmp bound t) = restrict_domain cmp (SOME bound) NONE (to_fmap cmp t)`, 2119 Induct_on `t` >> 2120 simp [to_fmap_def, filterGt_help_def, restrict_domain_union, restrict_domain_update] >> 2121 simp [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def] >> 2122 rpt gen_tac >> 2123 strip_tac >> 2124 Cases_on `cmp bound k` >> 2125 simp [] 2126 >- (inv_mp_tac link_thm >> 2127 conj_asm1_tac >> 2128 rw [] >> 2129 fs [invariant_eq] 2130 >- (rfs [key_ordered_to_fmap] >> 2131 rw [restrict_domain_def]) >> 2132 rw [restrict_domain_def, restrict_set_def, option_cmp_def, option_cmp2_def] >> 2133 to_fmap_tac) 2134 >- (fs [invariant_eq] >> 2135 rw [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def] >> 2136 to_fmap_tac) 2137 >- (first_x_assum inv_mp_tac >> 2138 fs [invariant_eq] >> 2139 rw [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def] >> 2140 to_fmap_tac)); 2141val _ = print "Proved filter_gt_help_thm\n"; 2142 2143val filterGt_thm = Q.prove ( 2144`!cmp bound t. 2145 good_cmp cmp ��� 2146 invariant cmp t 2147 ��� 2148 invariant cmp (filterGt cmp bound t) ��� 2149 to_fmap cmp (filterGt cmp bound t) = restrict_domain cmp bound NONE (to_fmap cmp t)`, 2150 Cases_on `bound` >> 2151 simp [to_fmap_def, filterGt_def, restrict_domain_union, restrict_domain_update] >> 2152 simp [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def] >> 2153 rw [] >> 2154 imp_res_tac filter_gt_help_thm 2155 >- (rw [FLOOKUP_EXT', FLOOKUP_DRESTRICT] >> 2156 rw [] >> 2157 fs [FLOOKUP_DEF] >> 2158 metis_tac [to_fmap_key_set]) >> 2159 rw [restrict_domain_def, restrict_set_def, option_cmp2_def, option_cmp_def]); 2160val _ = print "Proved filterGt_thm\n"; 2161 2162val restrict_domain_partition = Q.prove ( 2163`!cmp x l h t1 t2. 2164 good_cmp cmp ��� 2165 x ��� restrict_set cmp l h ��� 2166 restrict_domain cmp l (SOME x) t2 SUBMAP t1 ��� 2167 restrict_domain cmp (SOME x) h t1 SUBMAP t2 ��� 2168 key_set cmp x ��� FDOM t1 ��� 2169 key_set cmp x ��� FDOM t2 2170 ��� 2171 FUNION (restrict_domain cmp l h t1) (restrict_domain cmp l h t2) = 2172 FUNION (restrict_domain cmp l (SOME x) t1) (restrict_domain cmp (SOME x) h t2)`, 2173 rw [restrict_domain_def, FLOOKUP_EXT'] >> 2174 every_case_tac >> 2175 rw [] >> 2176 fs [restrict_set_def] >> 2177 `h = NONE ��� ?h'. h = SOME h'` by (Cases_on `h` >> simp[]) >> 2178 `l = NONE ��� ?l'. l = SOME l'` by (Cases_on `l` >> simp[]) >> 2179 fs [option_cmp_def, option_cmp2_def, SUBMAP_DEF, EXTENSION, FDOM_DRESTRICT, FLOOKUP_DEF, 2180 DRESTRICT_DEF, FAPPLY_FUPDATE_THM] >> 2181 fmrw [] >> 2182 metis_tac [cmp_thms, EXTENSION, key_set_eq]); 2183val _ = print "Proved restrict_domain_partition\n"; 2184 2185val restrict_domain_union_swap = Q.prove ( 2186` good_cmp cmp 2187 ��� 2188 a ��� 2189 restrict_domain cmp blo (SOME kx) (to_fmap cmp r2) ��� 2190 restrict_domain cmp (SOME kx) bhi (to_fmap cmp t1') 2191 = 2192 a ��� 2193 restrict_domain cmp (SOME kx) bhi (to_fmap cmp t1') ��� 2194 restrict_domain cmp blo (SOME kx) (to_fmap cmp r2)`, 2195 rw [restrict_domain_def] >> 2196 Cases_on `blo` >> 2197 Cases_on `bhi` >> 2198 rw [restrict_set_def, FLOOKUP_EXT'] >> 2199 fmrw [] >> 2200 fs [option_cmp_def, option_cmp2_def] >> 2201 every_case_tac >> 2202 rw [] >> 2203 metis_tac [cmp_thms, key_set_eq]); 2204val _ = print "Proved restrict_domain_union_swap\n" 2205 2206val restrict_domain_extend = Q.prove ( 2207` good_cmp cmp ��� 2208 invariant cmp (Bin s kx x t1 t1') ��� 2209 kx ��� restrict_set cmp blo bhi 2210 ��� 2211 restrict_domain cmp blo (SOME kx) (to_fmap cmp t1) = 2212 restrict_domain cmp blo bhi (to_fmap cmp t1) ��� 2213 restrict_domain cmp (SOME kx) bhi (to_fmap cmp t1') = 2214 restrict_domain cmp blo bhi (to_fmap cmp t1')`, 2215 rw [invariant_eq, restrict_domain_def] >> 2216 rfs [key_ordered_to_fmap] >> 2217 Cases_on `blo` >> 2218 Cases_on `bhi` >> 2219 rw [restrict_set_def, FLOOKUP_EXT'] >> 2220 fmrw [] >> 2221 fs [option_cmp_def, option_cmp2_def, restrict_set_def] >> 2222 every_case_tac >> 2223 rw [FLOOKUP_DEF] >> 2224 metis_tac [cmp_thms, key_set_eq, key_set_cmp_thm, to_fmap_key_set]); 2225val _ = print "Proved restrict_domain_extend\n"; 2226 2227val restrict_domain_combine = Q.prove ( 2228` good_cmp cmp ��� 2229 key_set cmp kx ��� k ��� 2230 kx ��� restrict_set cmp blo bhi 2231 ��� 2232 FLOOKUP (restrict_domain cmp (SOME kx) bhi (to_fmap cmp r2) ��� 2233 restrict_domain cmp blo (SOME kx) (to_fmap cmp r2)) k = 2234 FLOOKUP (restrict_domain cmp blo bhi (to_fmap cmp r2)) k`, 2235 fmrw [restrict_domain_def] >> 2236 every_case_tac >> 2237 rw [] >> 2238 Cases_on `blo` >> 2239 Cases_on `bhi` >> 2240 fs [restrict_set_def, option_cmp2_def, option_cmp_def, FLOOKUP_DEF] >> 2241 metis_tac [key_set_eq, cmp_thms, to_fmap_key_set, key_set_cmp_thm]); 2242val _ = print "Proved restrict_domain_combine\n"; 2243 2244val bounded_all_def = Define ` 2245(bounded_all cmp lk hk Tip ��� T) ��� 2246(bounded_all cmp lk hk (Bin s k v t1 t2) ��� 2247 k ��� restrict_set cmp lk hk ��� 2248 bounded_all cmp lk hk t1 ��� 2249 bounded_all cmp lk hk t2)`; 2250 2251val bounded_all_shrink1 = Q.prove ( 2252`!t blo bhi. 2253 good_cmp cmp ��� 2254 bounded_all cmp blo bhi t ��� 2255 key_ordered cmp kx t Greater 2256 ��� 2257 bounded_all cmp blo (SOME kx) t`, 2258 Induct_on `t` >> 2259 rw [bounded_all_def, key_ordered_def] 2260 >- (Cases_on `blo` >> 2261 fs [restrict_set_def, option_cmp_def, option_cmp2_def] >> 2262 metis_tac [good_cmp_def, comparison_distinct]) >> 2263 metis_tac []); 2264 2265val bounded_all_shrink2 = Q.prove ( 2266`!t blo bhi. 2267 good_cmp cmp ��� 2268 bounded_all cmp blo bhi t ��� 2269 key_ordered cmp kx t Less 2270 ��� 2271 bounded_all cmp (SOME kx) bhi t`, 2272 Induct_on `t` >> 2273 rw [bounded_all_def, key_ordered_def] 2274 >- (Cases_on `bhi` >> 2275 fs [restrict_set_def, option_cmp_def, option_cmp2_def] >> 2276 metis_tac [good_cmp_def, comparison_distinct]) >> 2277 metis_tac []); 2278 2279val bounded_restrict_id = Q.prove ( 2280`!t. 2281 good_cmp cmp ��� 2282 bounded_all cmp blo bhi t 2283 ��� 2284 restrict_domain cmp blo bhi (to_fmap cmp t) = to_fmap cmp t`, 2285 Induct_on `t` >> 2286 rw [bounded_all_def, to_fmap_def, restrict_domain_union, restrict_domain_update] >> 2287 Cases_on `blo` >> 2288 Cases_on `bhi` >> 2289 fs [restrict_domain_def, restrict_set_def, option_cmp_def, option_cmp2_def]); 2290 2291val restrict_domain_empty = Q.prove ( 2292`good_cmp cmp ��� 2293 restrict_domain cmp blo (SOME kx) (restrict_domain cmp (SOME kx) bhi t) = FEMPTY ��� 2294 restrict_domain cmp (SOME kx) bhi (restrict_domain cmp blo (SOME kx) t) = FEMPTY`, 2295 Cases_on `blo` >> 2296 Cases_on `bhi` >> 2297 fmrw [restrict_domain_def, restrict_set_def, option_cmp_def, option_cmp2_def, FLOOKUP_EXT'] >> 2298 metis_tac [good_cmp_def, comparison_distinct, key_set_eq]); 2299 2300val hedgeUnion_thm = Q.prove ( 2301`!cmp blo bhi t1 t2. 2302 good_cmp cmp ��� 2303 invariant cmp t1 ��� 2304 invariant cmp t2 ��� 2305 bounded_all cmp blo bhi t1 ��� 2306 bounded_root cmp blo bhi t2 2307 ��� 2308 invariant cmp (hedgeUnion cmp blo bhi t1 t2) ��� 2309 to_fmap cmp (hedgeUnion cmp blo bhi t1 t2) = 2310 restrict_domain cmp blo bhi (to_fmap cmp t1 ��� to_fmap cmp t2)`, 2311 ho_match_mp_tac (fetch "-" "hedgeUnion_ind") >> 2312 rpt conj_tac >> 2313 simp [hedgeUnion_def] >> 2314 rpt conj_tac >> 2315 rpt gen_tac >> 2316 strip_tac 2317 >- rw [to_fmap_def, FUNION_FEMPTY_2, bounded_restrict_id] 2318 >- (inv_mp_tac link_thm >> 2319 simp [GSYM CONJ_ASSOC] >> 2320 inv_mp_tac filterGt_thm >> 2321 simp [] >> 2322 fs [invariant_eq] >> 2323 strip_tac >> 2324 inv_mp_tac filterLt_thm >> 2325 simp [] >> 2326 strip_tac >> 2327 conj_tac 2328 >- (rfs [key_ordered_to_fmap, restrict_domain_def] >> 2329 Cases_on `blo` >> 2330 fs [restrict_set_def, option_cmp_def, option_cmp2_def]) >> 2331 conj_tac 2332 >- (rfs [key_ordered_to_fmap, restrict_domain_def] >> 2333 Cases_on `bhi` >> 2334 fs [restrict_set_def, option_cmp_def, option_cmp2_def]) >> 2335 `restrict_domain cmp blo bhi FEMPTY = FEMPTY` by rw [restrict_domain_def] >> 2336 rw [to_fmap_def, restrict_domain_union, restrict_domain_update] >> 2337 fmrw [restrict_domain_def, FLOOKUP_EXT'] >> 2338 rw [] >> 2339 Cases_on `blo` >> 2340 Cases_on `bhi` >> 2341 fs [restrict_set_def, option_cmp_def, option_cmp2_def, bounded_root_def] >> 2342 fs [] >> 2343 rw [FLOOKUP_DEF] >> 2344 metis_tac [key_ordered_to_fmap, cmp_thms, to_fmap_key_set, key_set_cmp_thm]) 2345 >- (inv_mp_tac insertR_thm >> 2346 imp_res_tac bounded_restrict_id >> 2347 rw [restrict_domain_union, to_fmap_def, restrict_domain_update] >> 2348 rw [restrict_domain_def, FLOOKUP_EXT'] >> 2349 fmrw [] >> 2350 every_case_tac >> 2351 fs [FLOOKUP_DEF, bounded_root_def]) >| 2352 [qabbrev_tac `r1 = Bin v39 v40 v41 v42 v43` >> 2353 qabbrev_tac `r2 = Bin v9 v10 v11 Tip r1`, 2354 qabbrev_tac `r1 = Bin v29 v30 v31 v32 v33` >> 2355 qabbrev_tac `r2 = Bin v9 v10 v11 r1 v13`] >> 2356(simp [bounded_all_def] >> 2357 strip_tac >> 2358 inv_mp_tac link_thm >> 2359 `invariant cmp t1'` by metis_tac [invariant_def] >> 2360 `invariant cmp t1` by metis_tac [invariant_def] >> 2361 simp [bounded_all_def, GSYM CONJ_ASSOC] >> 2362 FIRST_X_ASSUM inv_mp_tac >> 2363 simp [GSYM CONJ_ASSOC] >> 2364 inv_mp_tac trim_thm >> 2365 simp [bounded_all_def] >> 2366 strip_tac >> 2367 conj_tac 2368 >- (fs [invariant_eq] >> 2369 metis_tac [bounded_all_shrink1]) >> 2370 strip_tac >> 2371 FIRST_X_ASSUM inv_mp_tac >> 2372 simp [GSYM CONJ_ASSOC] >> 2373 inv_mp_tac trim_thm >> 2374 simp [bounded_all_def] >> 2375 strip_tac >> 2376 conj_tac 2377 >- (fs [invariant_eq] >> 2378 metis_tac [bounded_all_shrink2]) >> 2379 strip_tac >> 2380 qabbrev_tac `m1 = hedgeUnion cmp blo (SOME kx) t1 (trim cmp blo (SOME kx) r2)` >> 2381 qabbrev_tac `m2 = hedgeUnion cmp (SOME kx) bhi t1' (trim cmp (SOME kx) bhi r2)` >> 2382 conj_asm1_tac 2383 >- (rw [key_ordered_to_fmap, restrict_domain_union] >> 2384 Cases_on `blo` >> 2385 fs [restrict_domain_def, restrict_set_def, option_cmp_def, option_cmp2_def] >> 2386 metis_tac [good_cmp_def, comparison_distinct, key_set_cmp_thm]) >> 2387 conj_asm1_tac 2388 >- (rw [key_ordered_to_fmap, restrict_domain_union] >> 2389 Cases_on `bhi` >> 2390 fs [restrict_domain_def, restrict_set_def, option_cmp_def, option_cmp2_def] >> 2391 metis_tac [good_cmp_def, comparison_distinct, key_set_cmp_thm]) >> 2392 rw [restrict_domain_union, restrict_domain_update] >> 2393 `key_set cmp kx ��� FDOM (to_fmap cmp m1) ��� key_set cmp kx ��� FDOM (to_fmap cmp m2)` 2394 by metis_tac [key_ordered_to_fmap, cmp_thms, to_fmap_key_set, key_set_cmp_thm] >> 2395 `restrict_domain cmp blo (SOME kx) (to_fmap cmp m2) SUBMAP (to_fmap cmp m1) ��� 2396 restrict_domain cmp (SOME kx) bhi (to_fmap cmp m1) SUBMAP (to_fmap cmp m2)` 2397 by (qunabbrev_tac `m1` >> 2398 qunabbrev_tac `m2` >> 2399 rw [restrict_domain_union, SUBMAP_DEF, restrict_domain_empty]) >> 2400 `restrict_domain cmp blo bhi (to_fmap cmp m1) ��� 2401 restrict_domain cmp blo bhi (to_fmap cmp m2) = 2402 restrict_domain cmp blo (SOME kx) (to_fmap cmp m1) ��� 2403 restrict_domain cmp (SOME kx) bhi (to_fmap cmp m2)` 2404 by metis_tac [restrict_domain_partition] >> 2405 simp [restrict_domain_union, restrict_domain_update, to_fmap_def] >> 2406 rw [restrict_domain_union_swap] >> 2407 imp_res_tac restrict_domain_extend >> 2408 rw [] >> 2409 simp [FLOOKUP_EXT'] >> 2410 rw [FLOOKUP_UPDATE] >> 2411 REWRITE_TAC [GSYM FUNION_ASSOC] >> 2412 ONCE_REWRITE_TAC [FLOOKUP_FUNION] >> 2413 every_case_tac >> 2414 ONCE_REWRITE_TAC [FLOOKUP_FUNION] >> 2415 every_case_tac >> 2416 metis_tac [restrict_domain_combine])); 2417 2418val bounded_all_NONE = Q.prove ( 2419`!cmp t. bounded_all cmp NONE NONE t`, 2420 Induct_on `t` >> 2421 rw [bounded_all_def, restrict_set_def, option_cmp_def, option_cmp2_def]); 2422 2423val union_thm = Q.store_thm ("union_thm", 2424`!cmp blo bhi t1 t2. 2425 good_cmp cmp ��� 2426 invariant cmp t1 ��� 2427 invariant cmp t2 2428 ��� 2429 invariant cmp (union cmp t1 t2) ��� 2430 to_fmap cmp (union cmp t1 t2) = (to_fmap cmp t1 ��� to_fmap cmp t2)`, 2431 Cases_on `t1` >> 2432 Cases_on `t2` >> 2433 simp [union_def, to_fmap_def] >> 2434 gen_tac >> 2435 strip_tac >> 2436 inv_mp_tac hedgeUnion_thm >> 2437 rw [bounded_all_NONE, bounded_root_def, restrict_set_def, option_cmp_def, 2438 restrict_domain_def, option_cmp2_def, to_fmap_def] >> 2439 rw [FLOOKUP_EXT'] >> 2440 fmrw [] >> 2441 every_case_tac >> 2442 fs [FLOOKUP_DEF, invariant_eq] >> 2443 rfs [key_ordered_to_fmap] >> 2444 metis_tac [cmp_thms, to_fmap_key_set]); 2445 2446val EXT2 = Q.prove ( 2447`!s1 s2. s1 = s2 ��� (!k v. (k,v) ��� s1 ��� (k,v) ��� s2)`, 2448 rw [EXTENSION] >> 2449 EQ_TAC >> 2450 rw [] >> 2451 PairCases_on `x` >> 2452 rw []); 2453 2454val lift_key_def = Define ` 2455lift_key cmp kvs = IMAGE (\(k,v). (key_set cmp k, v)) kvs`; 2456 2457val toAscList_helper = Q.prove ( 2458`!cmp l t. 2459 good_cmp cmp ��� 2460 invariant cmp t ��� 2461 SORTED (\(x,y) (x',y'). cmp x x' = Less) l ��� 2462 (!k1 v1 k2 v2. MEM (k1,v1) l ��� FLOOKUP (to_fmap cmp t) (key_set cmp k2) = SOME v2 ��� cmp k2 k1 = Less) 2463 ��� 2464 SORTED (\(x,y) (x',y'). cmp x x' = Less) (foldrWithKey (��k x xs. (k,x)::xs) l t) ��� 2465 lift_key cmp (set (foldrWithKey (��k x xs. (k,x)::xs) l t)) = 2466 set (fmap_to_alist (to_fmap cmp t)) ��� lift_key cmp (set l)`, 2467 Induct_on `t` >> 2468 simp [foldrWithKey_def, to_fmap_def] >> 2469 fs [invariant_eq, EXT2] >> 2470 rpt gen_tac >> 2471 strip_tac >> 2472 simp [FLOOKUP_UPDATE, FLOOKUP_FUNION, PULL_FORALL] >> 2473 rpt gen_tac >> 2474 first_x_assum (qspecl_then [`cmp`, `l`] mp_tac) >> 2475 first_x_assum (qspecl_then [`cmp`, `(k,v)::foldrWithKey (��k x xs. (k,x)::xs) l t'`] mp_tac) >> 2476 simp [] >> 2477 strip_tac >> 2478 strip_tac >> 2479 fs [FLOOKUP_UPDATE, FLOOKUP_FUNION] >> 2480 `SORTED (��(x,y) (x',y'). cmp x x' = Less) (foldrWithKey (��k x xs. (k,x)::xs) l t') ��� 2481 ���k v. 2482 (k,v) ��� lift_key cmp (set (foldrWithKey (��k x xs. (k,x)::xs) l t')) ��� 2483 FLOOKUP (to_fmap cmp t') k = SOME v ��� (k,v) ��� lift_key cmp (set l)` 2484 by (first_x_assum match_mp_tac >> 2485 rw [] >> 2486 last_x_assum match_mp_tac >> 2487 rw [] 2488 >- metis_tac [] >> 2489 qexists_tac `v1` >> 2490 rw [] >> 2491 qexists_tac `v2` >> 2492 rw [] >> 2493 every_case_tac >> 2494 fs [DISJOINT_DEF, EXTENSION, FLOOKUP_DEF] >> 2495 metis_tac []) >> 2496 `SORTED (��(x,y) (x',y'). cmp x x' = Less) 2497 (foldrWithKey (��k x xs. (k,x)::xs) 2498 ((k,v)::foldrWithKey (��k x xs. (k,x)::xs) l t') t) ��� 2499 ���k' v'. 2500 (k',v') ��� lift_key cmp (set (foldrWithKey (��k x xs. (k,x)::xs) ((k,v)::foldrWithKey (��k x xs. (k,x)::xs) l t') t)) ��� 2501 FLOOKUP (to_fmap cmp t) k' = SOME v' ��� 2502 (k',v') ��� lift_key cmp ((k,v) INSERT set (foldrWithKey (��k x xs. (k,x)::xs) l t'))` 2503 by (first_x_assum match_mp_tac >> 2504 simp [good_cmp_trans, SORTED_EQ, FORALL_PROD] >> 2505 rw [] 2506 >- (`(key_set cmp p_1, p_2) ��� lift_key cmp (set (foldrWithKey (��k x xs. (k,x)::xs) l t'))` 2507 by (fs [lift_key_def, LAMBDA_PROD, EXISTS_PROD] >> 2508 metis_tac []) >> 2509 rfs [FLOOKUP_DEF] >> 2510 rfs [key_ordered_to_fmap] 2511 >- metis_tac [cmp_thms, key_set_cmp_thm] >> 2512 fs [lift_key_def, LAMBDA_PROD, EXISTS_PROD] >> 2513 metis_tac [cmp_thms, key_set_eq]) 2514 >- (rfs [key_ordered_to_fmap, FLOOKUP_DEF] >> 2515 metis_tac [cmp_thms, key_set_cmp_thm]) 2516 >- (`(key_set cmp k1, v1) ��� lift_key cmp (set (foldrWithKey (��k x xs. (k,x)::xs) l t'))` 2517 by (fs [lift_key_def, LAMBDA_PROD, EXISTS_PROD] >> 2518 metis_tac []) >> 2519 rfs [FLOOKUP_DEF] >> 2520 rfs [key_ordered_to_fmap] 2521 >- metis_tac [cmp_thms, key_set_cmp_thm] >> 2522 fs [lift_key_def, LAMBDA_PROD, EXISTS_PROD] >> 2523 metis_tac [cmp_thms, key_set_cmp_thm, key_set_eq])) >> 2524 simp [] >> 2525 eq_tac >> 2526 rw [] >> 2527 fs [FLOOKUP_DEF, DISJOINT_DEF, EXTENSION, FLOOKUP_DEF] >> 2528 every_case_tac >> 2529 rw [] >> 2530 fs [lift_key_def, LAMBDA_PROD, EXISTS_PROD] >> 2531 metis_tac []); 2532 2533val toAscList_thm = Q.store_thm ("toAscList_thm", 2534`!cmp t. 2535 good_cmp cmp ��� 2536 invariant cmp t 2537 ��� 2538 SORTED (\(x,y) (x',y'). cmp x x' = Less) (toAscList t) ��� 2539 lift_key cmp (set (toAscList t)) = set (fmap_to_alist (to_fmap cmp t))`, 2540 rpt gen_tac >> 2541 strip_tac >> 2542 qspecl_then [`cmp`, `[]`, `t`] mp_tac toAscList_helper >> 2543 simp [toAscList_def, lift_key_def]); 2544 2545(* some useful specialisations of the above theorem *) 2546 2547val MAP_FST_toAscList = Q.store_thm("MAP_FST_toAscList", 2548 `good_cmp cmp ��� invariant cmp t ��� 2549 SORTED (��x y. cmp x y = Less) (MAP FST (toAscList t)) ��� 2550 FDOM (to_fmap cmp t) = IMAGE (key_set cmp) (set (MAP FST (toAscList t)))`, 2551 rw[] \\ imp_res_tac toAscList_thm 2552 >- ( 2553 qmatch_goalsub_abbrev_tac`SORTED R` \\ 2554 imp_res_tac comparisonTheory.good_cmp_trans \\ 2555 `transitive R` by ( 2556 fs[relationTheory.transitive_def,FORALL_PROD,Abbr`R`] \\ 2557 metis_tac[] ) \\ 2558 rw[sorted_map] \\ 2559 rw[Abbr`R`,relationTheory.inv_image_def,LAMBDA_PROD] ) \\ 2560 fs[Once EXTENSION,lift_key_def,MEM_MAP,EXISTS_PROD,FORALL_PROD,FLOOKUP_DEF] \\ 2561 metis_tac[]); 2562 2563val MEM_toAscList = Q.store_thm("MEM_toAscList", 2564 `good_cmp cmp ��� invariant cmp t ��� MEM (k,v) (toAscList t) ��� 2565 FLOOKUP (to_fmap cmp t) (key_set cmp k) = SOME v`, 2566 rw[] \\ 2567 imp_res_tac toAscList_thm \\ 2568 `(key_set cmp k,v) ��� lift_key cmp (set (toAscList t))` 2569 by (simp_tac std_ss [lift_key_def] \\ simp[EXISTS_PROD] \\ metis_tac[]) 2570 \\ rfs[]); 2571 2572val compare_good_cmp = Q.store_thm ("compare_good_cmp", 2573`!cmp1 cmp2. good_cmp cmp1 ��� good_cmp cmp2 ��� good_cmp (compare cmp1 cmp2)`, 2574 rw [] >> 2575 imp_res_tac pair_cmp_good >> 2576 imp_res_tac list_cmp_good >> 2577 rpt (pop_assum mp_tac) >> 2578 REWRITE_TAC [good_cmp_def, compare_def] >> 2579 metis_tac []); 2580 2581val compare_thm1 = Q.prove ( 2582`!cmp1 cmp2 t1 t2. 2583 good_cmp cmp1 ��� 2584 good_cmp cmp2 ��� 2585 invariant cmp1 t1 ��� 2586 invariant cmp1 t2 ��� 2587 compare cmp1 cmp2 t1 t2 = Equal 2588 ��� 2589 fmap_rel (\x y. cmp2 x y = Equal) (to_fmap cmp1 t1) (to_fmap cmp1 t2)`, 2590 rw [compare_def, fmap_rel_OPTREL_FLOOKUP, OPTREL_def] >> 2591 imp_res_tac toAscList_thm >> 2592 fs [lift_key_def, list_cmp_equal_list_rel, pair_cmp_def] >> 2593 fs [key_set_def, EXTENSION, LAMBDA_PROD, FORALL_PROD, EXISTS_PROD] >> 2594 fs [LIST_REL_EL_EQN] >> 2595 pop_assum (mp_tac o GSYM) >> 2596 pop_assum (mp_tac o GSYM) >> 2597 rw [] >> 2598 Cases_on `FLOOKUP (to_fmap cmp1 t1) k` >> 2599 rw [] 2600 >- (disj1_tac >> 2601 Cases_on `FLOOKUP (to_fmap cmp1 t2) k` >> 2602 fs [] >> 2603 rfs [] >> 2604 fs [MEM_EL] >> 2605 res_tac >> 2606 Cases_on `EL n (toAscList t1)` >> 2607 Cases_on `EL n (toAscList t2)` >> 2608 fs [] >> 2609 every_case_tac >> 2610 fs [] >> 2611 rw [] >> 2612 first_x_assum (qspecl_then [`k`] mp_tac) >> 2613 strip_tac >> 2614 rfs [] >> 2615 pop_assum (qspecl_then [`r`, `q`] mp_tac) >> 2616 rw [] >> 2617 metis_tac [NOT_SOME_NONE, cmp_thms]) 2618 >- (rfs [] >> 2619 fs [MEM_EL] >> 2620 rfs [] >> 2621 res_tac >> 2622 Cases_on `EL n (toAscList t1)` >> 2623 Cases_on `EL n (toAscList t2)` >> 2624 fs [] >> 2625 every_case_tac >> 2626 fs [] >> 2627 rw [] >> 2628 MAP_EVERY qexists_tac [`r`, `r'`] >> 2629 rw [] 2630 >- metis_tac [] >> 2631 qexists_tac `q'` >> 2632 rw [] >> 2633 metis_tac [cmp_thms])); 2634val _ = print "Proved compare_thm1"; 2635 2636 2637val NONE_lem = Q.prove ( 2638`x = NONE ��� ��?y. x = SOME y`, 2639 Cases_on `x` >> 2640 rw []); 2641 2642val pair_cmp_lem = Q.prove ( 2643`!cmp1 cmp2. pair_cmp cmp1 cmp2 (x1,x2) (y1,y2) = Equal ��� cmp1 x1 y1 = Equal ��� cmp2 x2 y2 = Equal`, 2644 rw [pair_cmp_def] >> 2645 every_case_tac); 2646 2647val strict_sorted_unique = Q.prove ( 2648`!cmp l x1 y1 x2 y2. 2649 good_cmp cmp ��� 2650 SORTED (��(x,y) (x',y'). cmp x x' = Less) l ��� 2651 MEM (x1,y1) l ��� 2652 MEM (x2,y2) l ��� 2653 cmp x1 x2 = Equal 2654 ��� 2655 x1 = x2 ��� y1 = y2`, 2656 Induct_on `l` >> 2657 rw [] >> 2658 `transitive (��(x,y) (x',y'). cmp x x' = Less)` by metis_tac [good_cmp_trans] >> 2659 fs [SORTED_EQ, LAMBDA_PROD, FORALL_PROD] 2660 >- metis_tac [cmp_thms] 2661 >- metis_tac [cmp_thms] 2662 >- metis_tac [cmp_thms] 2663 >- metis_tac [cmp_thms] >> 2664 Cases_on `h` >> 2665 fs [] >> 2666 res_tac); 2667val _ = print "Proved strict_sorted_unique\n" 2668 2669val strict_sorted_eq_el = Q.prove ( 2670`!cmp l m n. 2671 good_cmp cmp ��� 2672 SORTED (��(x,y) (x',y'). cmp x x' = Less) l ��� 2673 cmp (FST (EL m l)) (FST (EL n l)) = Equal ��� 2674 m < LENGTH l ��� 2675 n < LENGTH l 2676 ��� 2677 m = n`, 2678 Induct_on `l` >> 2679 rw [] >> 2680 `transitive (��(x,y) (x',y'). cmp x x' = Less)` by metis_tac [good_cmp_trans] >> 2681 fs [SORTED_EQ, LAMBDA_PROD, FORALL_PROD] >> 2682 Cases_on `h` >> 2683 fs [] >> 2684 Cases_on `0 < n` >> 2685 Cases_on `0 < m` >> 2686 fs [rich_listTheory.EL_CONS] >> 2687 full_simp_tac (srw_ss()++ARITH_ss) [] >> 2688 rw [] 2689 >- (res_tac >> 2690 full_simp_tac (srw_ss()++ARITH_ss) []) 2691 >- (`PRE n < LENGTH l` by decide_tac >> 2692 `MEM (EL (PRE n) l) l` by metis_tac [MEM_EL] >> 2693 Cases_on `EL (PRE n) l` >> 2694 fs [] >> 2695 metis_tac [cmp_thms]) 2696 >- (`PRE m < LENGTH l` by decide_tac >> 2697 `MEM (EL (PRE m) l) l` by metis_tac [MEM_EL] >> 2698 Cases_on `EL (PRE m) l` >> 2699 fs [] >> 2700 metis_tac [cmp_thms])); 2701val _ = print "Proved strict_sorted_eq_el\n"; 2702 2703val compare_lem2 = Q.prove ( 2704`!cmp1 cmp2 n l1 l2. 2705 good_cmp cmp1 ��� 2706 good_cmp cmp2 ��� 2707 (���k. 2708 (���y p_1' y' p_1''. 2709 (k ��� key_set cmp1 p_1' ��� ��MEM (p_1',y) l1) ��� 2710 (k ��� key_set cmp1 p_1'' ��� ��MEM (p_1'',y') l2)) ��� 2711 ���x y p_1' p_1''. 2712 (k = key_set cmp1 p_1' ��� MEM (p_1',x) l1) ��� 2713 (k = key_set cmp1 p_1'' ��� MEM (p_1'',y) l2) ��� cmp2 x y = Equal) ��� 2714 SORTED (��(x,y) (x',y'). cmp1 x x' = Less) l2 ��� 2715 SORTED (��(x,y) (x',y'). cmp1 x x' = Less) l1 ��� 2716 n ��� LENGTH l1 ��� 2717 n ��� LENGTH l2 ��� 2718 LIST_REL (��(p1,p2) (p1',p2'). pair_cmp cmp1 cmp2 (p1,p2) (p1',p2') = Equal) 2719 (TAKE n l1) (TAKE n l2) ��� 2720 n ��� LENGTH l1 2721 ��� 2722 n ��� LENGTH l2 ��� 2723 (��(p1,p2) (p1',p2'). pair_cmp cmp1 cmp2 (p1,p2) (p1',p2') = Equal) 2724 (EL n l1) (EL n l2)`, 2725 rpt GEN_TAC >> 2726 rpt DISCH_TAC >> 2727 fs [] >> 2728 `?kn1 vn1. EL n l1 = (kn1,vn1)` by metis_tac [pair_CASES] >> 2729 simp [] >> 2730 `?kn2 vn2. MEM (kn2,vn2) l2 ��� cmp1 kn1 kn2 = Equal ��� cmp2 vn1 vn2 = Equal` 2731 by (first_assum (qspecl_then [`key_set cmp1 kn1`] assume_tac) >> 2732 `MEM (EL n l1) l1` by metis_tac [PAIR, rich_listTheory.EL_MEM, LESS_OR_EQ] >> 2733 fs [] >> 2734 rfs [key_set_eq] 2735 >- metis_tac [PAIR, cmp_thms] >> 2736 `p_1' = kn1 ��� x = vn1` 2737 by (match_mp_tac strict_sorted_unique >> 2738 rw [] >> 2739 metis_tac [cmp_thms]) >> 2740 rw [] >> 2741 metis_tac []) >> 2742 fs [MEM_EL] >> 2743 `n' < n ��� n = n' ��� n < n'` by decide_tac >> 2744 fs [] 2745 >- (fs [LIST_REL_EL_EQN] >> 2746 first_x_assum (qspecl_then [`n'`] mp_tac) >> 2747 simp [rich_listTheory.EL_TAKE] >> 2748 DISCH_TAC >> 2749 fs [] >> 2750 Cases_on `EL n' l1` >> 2751 Cases_on `EL n' l2` >> 2752 fs [pair_cmp_lem] >> 2753 `n' < LENGTH l1 ��� n < LENGTH l1` by decide_tac >> 2754 imp_res_tac strict_sorted_eq_el >> 2755 `n' = n` by metis_tac [FST, PAIR, cmp_thms] >> 2756 fs []) 2757 >- (rw [pair_cmp_lem] >> 2758 Cases_on `EL n l2` >> 2759 rw [] >> 2760 metis_tac []) 2761 >- (`?kn3 vn3. EL n l2 = (kn3,vn3)` by metis_tac [pair_CASES] >> 2762 simp [] >> 2763 `?kn4 vn4. MEM (kn4,vn4) l1 ��� cmp1 kn3 kn4 = Equal ��� cmp2 vn3 vn4 = Equal` 2764 by (first_assum (qspecl_then [`key_set cmp1 kn3`] assume_tac) >> 2765 `n < LENGTH l2` by decide_tac >> 2766 `n < LENGTH l1` by decide_tac >> 2767 `MEM (EL n l2) l2` by metis_tac [PAIR, rich_listTheory.EL_MEM, LESS_OR_EQ] >> 2768 fs [] >> 2769 rfs [key_set_eq] >> 2770 `n < LENGTH l2` by decide_tac >> 2771 `n < LENGTH l1` by decide_tac 2772 >- metis_tac [PAIR, cmp_thms] >> 2773 rw [] >> 2774 `p_1'' = kn3 ��� y = vn3` 2775 by (match_mp_tac strict_sorted_unique >> 2776 rw [] >> 2777 metis_tac [rich_listTheory.EL_MEM, cmp_thms]) >> 2778 rw [] >> 2779 MAP_EVERY qexists_tac [`p_1'`, `x`] >> 2780 rw [rich_listTheory.EL_MEM] >> 2781 metis_tac [cmp_thms]) >> 2782 fs [MEM_EL] >> 2783 `n < n'' ��� n = n'' ��� n'' < n` by decide_tac >> 2784 fs [] >> 2785 `cmp1 kn3 kn2 = Less` 2786 by (`transitive (��(x,y) (x',y'). cmp1 x x' = Less)` by metis_tac [good_cmp_trans] >> 2787 `(��(x,y) (x',y'). cmp1 x x' = Less) (EL n l2) (EL n' l2)` 2788 by metis_tac [SORTED_EL_LESS] >> 2789 rfs [] >> 2790 Cases_on `EL n' l2` >> 2791 fs []) 2792 >- (`cmp1 kn1 kn4 = Less` 2793 by (`transitive (��(x,y) (x',y'). cmp1 x x' = Less)` by metis_tac [good_cmp_trans] >> 2794 `(��(x,y) (x',y'). cmp1 x x' = Less) (EL n l1) (EL n'' l1)` 2795 by metis_tac [SORTED_EL_LESS] >> 2796 rfs [] >> 2797 Cases_on `EL n'' l1` >> 2798 fs []) >> 2799 metis_tac [cmp_thms]) 2800 >- (rw [] >> 2801 rfs [] >> 2802 metis_tac [cmp_thms]) 2803 >- (fs [LIST_REL_EL_EQN] >> 2804 first_x_assum (qspecl_then [`n''`] mp_tac) >> 2805 simp [rich_listTheory.EL_TAKE] >> 2806 DISCH_TAC >> 2807 fs [] >> 2808 Cases_on `EL n'' l1` >> 2809 Cases_on `EL n'' l2` >> 2810 fs [pair_cmp_lem] >> 2811 rfs [] >> 2812 `n < LENGTH l2` by decide_tac >> 2813 `cmp1 kn1 kn4 = Less` 2814 by (`transitive (��(x,y) (x',y'). cmp1 x x' = Less)` by metis_tac [good_cmp_trans] >> 2815 `(��(x,y) (x',y'). cmp1 x x' = Less) (EL n'' l2) (EL n l2)` 2816 by metis_tac [SORTED_EL_LESS] >> 2817 rfs [] >> 2818 Cases_on `EL n'' l2` >> 2819 fs [] >> 2820 metis_tac [cmp_thms]) >> 2821 metis_tac [cmp_thms]))); 2822val _ = print "Proved compare_lem2\n"; 2823 2824val compare_thm2 = Q.prove ( 2825`!cmp1 cmp2 t1 t2. 2826 good_cmp cmp1 ��� 2827 good_cmp cmp2 ��� 2828 invariant cmp1 t1 ��� 2829 invariant cmp1 t2 ��� 2830 fmap_rel (\x y. cmp2 x y = Equal) (to_fmap cmp1 t1) (to_fmap cmp1 t2) 2831 ��� 2832 compare cmp1 cmp2 t1 t2 = Equal`, 2833 rw [compare_def, fmap_rel_OPTREL_FLOOKUP, OPTREL_def, list_cmp_equal_list_rel] >> 2834 imp_res_tac toAscList_thm >> 2835 fs [EXTENSION] >> 2836 simp [] >> 2837 fs [lift_key_def, PULL_EXISTS, LAMBDA_PROD, FORALL_PROD, EXISTS_PROD] >> 2838 pop_assum (mp_tac o GSYM) >> 2839 pop_assum (mp_tac o GSYM) >> 2840 DISCH_TAC >> 2841 DISCH_TAC >> 2842 fs [NONE_lem] >> 2843 ntac 3 (pop_assum (fn _ => all_tac)) >> 2844 pop_assum mp_tac >> 2845 pop_assum mp_tac >> 2846 pop_assum (fn _ => all_tac) >> 2847 pop_assum mp_tac >> 2848 ntac 2 (pop_assum (fn _ => all_tac)) >> 2849 Q.SPEC_TAC (`toAscList t1`, `l1`) >> 2850 Q.SPEC_TAC (`toAscList t2`, `l2`) >> 2851 fs [PULL_FORALL, PULL_EXISTS] >> 2852 rw [] >> 2853 ONCE_REWRITE_TAC [list_rel_thm] >> 2854 gen_tac >> 2855 DISCH_TAC >> 2856 fs [] 2857 >- (match_mp_tac compare_lem2 >> 2858 rw []) 2859 >- (`n ��� LENGTH l1 ��� (��(p1,p2) (p1',p2'). pair_cmp cmp1 cmp2 (p1,p2) (p1',p2') = Equal) (EL n l2) (EL n l1)` 2860 by (match_mp_tac compare_lem2 >> 2861 rw [] 2862 >- (first_x_assum (qspecl_then [`k`] mp_tac) >> 2863 rw [] >> 2864 metis_tac [good_cmp_def]) 2865 >- (match_mp_tac (SIMP_RULE (srw_ss()) [AND_IMP_INTRO, PULL_FORALL] (GEN_ALL EVERY2_sym)) >> 2866 qexists_tac `(��(p1,p2) (p1',p2'). pair_cmp cmp1 cmp2 (p1,p2) (p1',p2') = Equal)` >> 2867 rw [] >> 2868 PairCases_on `y'` >> 2869 PairCases_on `x'` >> 2870 fs [] >> 2871 metis_tac [good_cmp_def, pair_cmp_good])) >> 2872 Cases_on `EL n l1` >> 2873 Cases_on `EL n l2` >> 2874 fs [] >> 2875 metis_tac [good_cmp_def, pair_cmp_good])); 2876val _ = print "Proved compare_thm2\n"; 2877 2878val compare_thm = Q.store_thm ("compare_thm", 2879`!cmp1 cmp2 t1 t2. 2880 good_cmp cmp1 ��� 2881 good_cmp cmp2 ��� 2882 invariant cmp1 t1 ��� 2883 invariant cmp1 t2 2884 ��� 2885 (compare cmp1 cmp2 t1 t2 = Equal 2886 ��� 2887 fmap_rel (\x y. cmp2 x y = Equal) (to_fmap cmp1 t1) (to_fmap cmp1 t2))`, 2888 metis_tac [compare_thm1, compare_thm2]); 2889 2890val map_thm = Q.store_thm ("map_thm", 2891`!t. 2892 good_cmp cmp ��� 2893 invariant cmp t 2894 ��� 2895 invariant cmp (map f t) ��� 2896 to_fmap cmp (map f t) = f o_f to_fmap cmp t`, 2897 Induct_on `t` >> 2898 simp [map_def, to_fmap_def] 2899 >- rw [invariant_def] >> 2900 rpt gen_tac >> 2901 strip_tac >> 2902 simp [invariant_def, GSYM CONJ_ASSOC] >> 2903 inv_to_front_tac ``invariant`` >> 2904 first_x_assum inv_mp_tac >> 2905 simp [] >> 2906 fs [invariant_eq] >> 2907 strip_tac >> 2908 imp_res_tac (GSYM structure_size_thm) >> 2909 imp_res_tac size_thm >> 2910 simp [FCARD_DEF] >> 2911 rw [] 2912 >- rfs [key_ordered_to_fmap] 2913 >- rfs [key_ordered_to_fmap] 2914 >- fs [FCARD_DEF] 2915 >- (fmrw [FLOOKUP_EXT'] >> 2916 fmrw [FLOOKUP_o_f, DOMSUB_FLOOKUP_THM] >> 2917 every_case_tac >> 2918 fs [])); 2919 2920val splitLookup_thm = Q.store_thm ("splitLookup_thm", 2921`!t lt v gt. 2922 good_cmp cmp ��� 2923 invariant cmp t ��� 2924 (lt,v,gt) = splitLookup cmp k t 2925 ��� 2926 invariant cmp lt ��� 2927 invariant cmp gt ��� 2928 FLOOKUP (to_fmap cmp t) (key_set cmp k) = v ��� 2929 key_ordered cmp k lt Greater ��� 2930 key_ordered cmp k gt Less ��� 2931 to_fmap cmp t = 2932 case v of 2933 | NONE => FUNION (to_fmap cmp lt) (to_fmap cmp gt) 2934 | SOME v => (FUNION (to_fmap cmp lt) (to_fmap cmp gt)) |+ (key_set cmp k, v)`, 2935 Induct_on `t` >> 2936 simp [splitLookup_def, to_fmap_def, key_ordered_to_fmap] >> 2937 rpt gen_tac >> 2938 strip_tac >> 2939 Cases_on `cmp k k'` >> 2940 fs [] 2941 >- (`?lt v gt. splitLookup cmp k t = (lt,v,gt)` by metis_tac [pair_CASES] >> 2942 fs [] >> 2943 last_x_assum inv_mp_tac >> 2944 simp [] >> 2945 fs [invariant_eq] >> 2946 strip_tac >> 2947 inv_mp_tac link_thm >> 2948 simp [] >> 2949 conj_asm1_tac 2950 >- (rfs [key_ordered_to_fmap] >> 2951 rw [] >> 2952 first_x_assum match_mp_tac >> 2953 rw [] >> 2954 every_case_tac >> 2955 fs []) >> 2956 strip_tac >> 2957 Cases_on `v''` >> 2958 fs [] >> 2959 fmrw [] >> 2960 rfs [FLOOKUP_FUNION] >> 2961 every_case_tac >> 2962 fs [] >> 2963 TRY (match_mp_tac FUPDATE_COMMUTES) >> 2964 rfs [key_ordered_to_fmap, flookup_thm] >> 2965 res_tac >> 2966 metis_tac [cmp_thms, key_set_cmp_def, key_set_cmp_thm]) 2967 >- (fs [invariant_eq] >> 2968 fmrw [key_set_eq] >> 2969 rfs [key_ordered_to_fmap] >> 2970 res_tac >> 2971 fs [key_set_cmp_def] >> 2972 fmrw [FLOOKUP_EXT'] >> 2973 every_case_tac >> 2974 fs [] >> 2975 rw [] >> 2976 rfs [key_set_eq] >> 2977 metis_tac [cmp_thms]) 2978 >- (`?lt v gt. splitLookup cmp k t' = (lt,v,gt)` by metis_tac [pair_CASES] >> 2979 fs [] >> 2980 fs [invariant_eq] >> 2981 inv_mp_tac link_thm >> 2982 simp [] >> 2983 conj_asm1_tac 2984 >- (rfs [key_ordered_to_fmap] >> 2985 rw [] >> 2986 first_x_assum match_mp_tac >> 2987 rw [] >> 2988 every_case_tac >> 2989 fs []) >> 2990 strip_tac >> 2991 Cases_on `v''` >> 2992 fs [] >> 2993 fmrw [] >> 2994 rfs [FLOOKUP_FUNION] >> 2995 every_case_tac >> 2996 fs [] >> 2997 TRY (match_mp_tac FUPDATE_COMMUTES) >> 2998 rfs [key_ordered_to_fmap, flookup_thm] >> 2999 fs [key_ordered_to_fmap, flookup_thm] >> 3000 res_tac >> 3001 metis_tac [cmp_thms, key_set_cmp_def, key_set_cmp_thm])); 3002 3003val submap'_thm = Q.prove ( 3004`!cmp f t1 t2. 3005 good_cmp cmp ��� 3006 invariant cmp t1 ��� 3007 invariant cmp t2 3008 ��� 3009 (submap' cmp f t1 t2 ��� !k v. lookup cmp k t1 = SOME v ��� ?v'. lookup cmp k t2 = SOME v' ��� f v v')`, 3010 ho_match_mp_tac (fetch "-" "submap'_ind") >> 3011 rpt conj_tac 3012 >- rw [lookup_def, submap'_def] 3013 >- (rw [lookup_def, submap'_def, invariant_eq] >> 3014 qexists_tac `v11` >> 3015 qexists_tac `v12` >> 3016 every_case_tac >> 3017 fs [] >> 3018 metis_tac [cmp_thms]) >> 3019 rw [] >> 3020 qabbrev_tac `t = Bin v20 v21 v22 v23 v24` >> 3021 `?lt v gt. splitLookup cmp kx t = (lt,v,gt)` by metis_tac [pair_CASES] >> 3022 fs [] >> 3023 `invariant cmp lt ��� invariant cmp gt ��� 3024 FLOOKUP (to_fmap cmp t) (key_set cmp kx) = v ��� 3025 key_ordered cmp kx lt Greater ��� key_ordered cmp kx gt Less ��� 3026 to_fmap cmp t = 3027 case v of 3028 NONE => to_fmap cmp lt ��� to_fmap cmp gt 3029 | SOME v' => (to_fmap cmp lt ��� to_fmap cmp gt) |+ (key_set cmp kx,v')` 3030 by metis_tac [splitLookup_thm] >> 3031 unabbrev_all_tac >> 3032 Cases_on `v` >> 3033 fs [] 3034 >- (rw [submap'_def, lookup_def] >> 3035 qexists_tac `kx` >> 3036 qexists_tac `x` >> 3037 rw [] 3038 >- metis_tac [cmp_thms] >> 3039 every_case_tac >> 3040 fs [] >> 3041 CCONTR_TAC >> 3042 fs [] >> 3043 imp_res_tac lookup_thm >> 3044 fs [lookup_def, to_fmap_def] >> 3045 metis_tac [cmp_thms, NOT_SOME_NONE]) 3046 >- (simp [submap'_def] >> 3047 qabbrev_tac `t = Bin v20 v21 v22 v23 v24` >> 3048 pop_assum (fn _ => all_tac) >> 3049 fs [invariant_eq] >> 3050 rw [lookup_def] >> 3051 eq_tac >> 3052 simp [] 3053 >- (rw [] >> 3054 imp_res_tac lookup_thm >> 3055 rw [FLOOKUP_UPDATE] >> 3056 rfs [key_set_eq] >> 3057 fs [] 3058 >- (`cmp k kx = Equal` by metis_tac [cmp_thms] >> 3059 fs []) >> 3060 rw [FLOOKUP_FUNION] >> 3061 Cases_on `cmp k kx` >> 3062 fs [] >> 3063 res_tac 3064 >- (qexists_tac `v''` >> 3065 rw []) 3066 >- metis_tac [cmp_thms] 3067 >- (rfs [key_ordered_to_fmap] >> 3068 `FLOOKUP (to_fmap cmp lt) (key_set cmp k) = NONE` 3069 by (fs [FLOOKUP_DEF] >> 3070 CCONTR_TAC >> 3071 fs [] >> 3072 res_tac >> 3073 fs [key_set_cmp_def, key_set_def] >> 3074 metis_tac [cmp_thms]) >> 3075 rw [])) >> 3076 rw [] 3077 >- (first_assum (qspecl_then [`kx`, `x`] assume_tac) >> 3078 every_case_tac >> 3079 fs [] 3080 >- metis_tac [cmp_thms] 3081 >- (imp_res_tac lookup_thm >> 3082 fs [] >> 3083 rfs [] >> 3084 rw []) 3085 >- metis_tac [cmp_thms]) 3086 >- (imp_res_tac lookup_thm >> 3087 fs [] >> 3088 rfs [FLOOKUP_UPDATE] >> 3089 rw [] >> 3090 last_assum (qspecl_then [`k`] assume_tac) >> 3091 Cases_on `cmp k kx` >> 3092 fs [] >> 3093 rfs [key_set_eq] 3094 >- (`cmp kx k ��� Equal` by metis_tac [cmp_thms] >> 3095 fs [FLOOKUP_FUNION] >> 3096 Cases_on `FLOOKUP (to_fmap cmp lt) (key_set cmp k)` >> 3097 fs [FLOOKUP_DEF] >> 3098 rfs [key_ordered_to_fmap] >> 3099 res_tac >> 3100 fs [key_set_cmp_def, key_set_def] >> 3101 metis_tac [cmp_thms]) 3102 >- (`cmp kx k = Equal` by metis_tac [cmp_thms] >> 3103 fs [FLOOKUP_DEF] >> 3104 rfs [key_ordered_to_fmap] >> 3105 res_tac >> 3106 fs [key_set_cmp_def, key_set_def] >> 3107 metis_tac [cmp_thms]) 3108 >- (`cmp kx k ��� Equal` by metis_tac [cmp_thms] >> 3109 fs [FLOOKUP_DEF] >> 3110 rfs [key_ordered_to_fmap] >> 3111 res_tac >> 3112 fs [key_set_cmp_def, key_set_def] >> 3113 metis_tac [cmp_thms])) 3114 >- (imp_res_tac lookup_thm >> 3115 fs [] >> 3116 rfs [FLOOKUP_UPDATE] >> 3117 rw [] >> 3118 last_assum (qspecl_then [`k`] assume_tac) >> 3119 Cases_on `cmp k kx` >> 3120 fs [] >> 3121 rfs [key_set_eq] 3122 >- (`cmp kx k ��� Equal` by metis_tac [cmp_thms] >> 3123 fs [FLOOKUP_DEF] >> 3124 rfs [key_ordered_to_fmap] >> 3125 res_tac >> 3126 fs [key_set_cmp_def, key_set_def] >> 3127 metis_tac [cmp_thms]) 3128 >- (`cmp kx k = Equal` by metis_tac [cmp_thms] >> 3129 fs [FLOOKUP_DEF] >> 3130 rfs [key_ordered_to_fmap] >> 3131 res_tac >> 3132 fs [key_set_cmp_def, key_set_def] >> 3133 metis_tac [cmp_thms]) 3134 >- (`cmp kx k ��� Equal` by metis_tac [cmp_thms] >> 3135 fs [FLOOKUP_FUNION] >> 3136 Cases_on `FLOOKUP (to_fmap cmp lt) (key_set cmp k)` >> 3137 fs [FLOOKUP_DEF] >> 3138 rfs [key_ordered_to_fmap] >> 3139 res_tac >> 3140 fs [key_set_cmp_def, key_set_def] >> 3141 metis_tac [cmp_thms])))); 3142 3143val isSubmapOfBy_thm = Q.store_thm ("isSubmapOfBy_thm", 3144`!cmp f t1 t2. 3145 good_cmp cmp ��� 3146 invariant cmp t1 ��� 3147 invariant cmp t2 3148 ��� 3149 (isSubmapOfBy cmp f t1 t2 ��� !k v. lookup cmp k t1 = SOME v ��� ?v'. lookup cmp k t2 = SOME v' ��� f v v')`, 3150 rw [isSubmapOfBy_def] >> 3151 Cases_on `size t1 ��� size t2` >> 3152 rw [submap'_thm] >> 3153 fs [NOT_LESS_EQUAL] >> 3154 imp_res_tac size_thm >> 3155 imp_res_tac lookup_thm >> 3156 fs [FCARD_DEF] >> 3157 `FINITE (FDOM (to_fmap cmp t1)) ��� FINITE (FDOM (to_fmap cmp t2))` by rw [] >> 3158 imp_res_tac LESS_CARD_DIFF >> 3159 full_simp_tac std_ss [] >> 3160 `FINITE (FDOM (to_fmap cmp t1) DIFF FDOM (to_fmap cmp t2))` by rw [] >> 3161 imp_res_tac POS_CARD_HAS_MEM >> 3162 fs [] >> 3163 rw [FLOOKUP_DEF] >> 3164 imp_res_tac to_fmap_key_set >> 3165 rw [] >> 3166 qexists_tac `k` >> 3167 rw []); 3168 3169val isSubmapOf_thm = Q.store_thm ("isSubmapOf_thm", 3170`!cmp t1 t2. 3171 good_cmp cmp ��� 3172 invariant cmp t1 ��� 3173 invariant cmp t2 3174 ��� 3175 (isSubmapOf cmp t1 t2 ��� !k v. lookup cmp k t1 = SOME v ��� lookup cmp k t2 = SOME v)`, 3176 rw [isSubmapOf_def, isSubmapOfBy_thm]); 3177 3178val fromList_thm = Q.store_thm ("fromList_thm", 3179`!cmp l. 3180 good_cmp cmp 3181 ��� 3182 invariant cmp (fromList cmp l) ��� 3183 to_fmap cmp (fromList cmp l) = alist_to_fmap (MAP (\(k,v). (key_set cmp k, v)) l)`, 3184 Induct_on `l` >> 3185 simp [fromList_def, empty_thm] >> 3186 rpt gen_tac >> 3187 strip_tac >> 3188 PairCases_on `h` >> 3189 simp [] >> 3190 inv_mp_tac insert_thm >> 3191 strip_tac >> 3192 simp [] >> 3193 fs [fromList_def]); 3194 3195(* ------------------------ Extra stuff, not from ghc ----------------- *) 3196 3197val map_keys_def = Define ` 3198map_keys cmp f t = fromList cmp (MAP (\(k,v). (f k, v)) (toAscList t))`; 3199 3200val in_lift_key = Q.prove ( 3201`!cmp k v l. 3202 good_cmp cmp ��� 3203 SORTED (��(x,y:'a) (x',y':'a). cmp x x' = Less) l ��� 3204 transitive (��(x,y:'a) (x',y':'a). cmp x x' = Less) 3205 ��� 3206 ((k,v) ��� lift_key cmp (set l) ��� ALOOKUP (MAP (��(x,y). (key_set cmp x, y)) l) k = SOME v)`, 3207 Induct_on `l` >> 3208 fs [lift_key_def, key_set_def, LAMBDA_PROD, EXISTS_PROD, EXTENSION, FORALL_PROD] >> 3209 rw [] >> 3210 fs [] >> 3211 eq_tac >> 3212 rw [] >> 3213 fs [SORTED_EQ] >> 3214 res_tac >> 3215 fs [] >> 3216 metis_tac [cmp_thms]); 3217 3218 (* 3219val alookup_unit_lem = Q.prove ( 3220`!cmp1 cmp2 f k l x. 3221 good_cmp cmp1 ��� 3222 good_cmp cmp2 ��� 3223 resp_equiv2 cmp1 cmp2 f 3224 ��� 3225 (ALOOKUP (MAP (\(k,v). (key_set cmp1 k, ())) l) (key_set cmp1 x') = 3226 ALOOKUP (MAP (\(k,v). (key_set cmp2 (f k), ())) l) (key_set cmp2 (f x')))`, 3227 3228 Induct_on `l` >> 3229 rw [] >> 3230 PairCases_on `h` >> 3231 rw [] >> 3232 rfs [key_set_eq, resp_equiv2_def] >> 3233 >- (rfs [] >> 3234 fs [EXTENSION, key_set_def] >> 3235 match_mp_tac (METIS_PROVE [] ``F���x``) >> 3236 rw [] >> 3237 pop_assum mp_tac >> 3238 simp [] >> 3239 eq_tac >> 3240 rw [] >> 3241 fs [resp_equiv2_def] 3242 >- (qexists_tac `key_set cmp2 (f h0)` >> 3243 rw [key_set_def] >> 3244 metis_tac [cmp_thms]) 3245 >- metis_tac [cmp_thms]) 3246 >- (rfs [] >> 3247 rw [] >> 3248 fs [EXTENSION, key_set_def] >> 3249 Cases_on `x ��� k` >> 3250 fs [resp_equiv2_def] >> 3251 first_x_assum (qspecl_then [`f x`] assume_tac) >> 3252 fs [] >> 3253 Cases_on `cmp2 (f h0) (f x) = Equal` >> 3254 fs [] 3255metis_tac [cmp_thms] 3256 3257 3258 rfs [key_set_eq] >> 3259 `IMAGE f (key_set cmp1 h0) ��� key_set cmp2 (f h0)` by metis_tac [key_set_map] >> 3260 fs [SUBSET_DEF, EXTENSION] >> 3261 `x ��� key_set cmp2 (f h0) ��� ��?x'. x = f x' ��� x' ��� key_set cmp1 h0` by metis_tac [] 3262 fs [] 3263 3264 fs [key_set_def, resp_equiv2_def, EXTENSION] >> 3265 rw [] >> 3266 rfs [] >> 3267 Cases_on `h1 = v` >> 3268 rw [] >> 3269 3270 pop_assum mp_tac >> 3271 match_mp_tac (METIS_PROVE [] ``x ��� (~x ��� y)``) >> 3272 eq_tac >> 3273 rw [] 3274 3275 metis_tac [cmp_thms] 3276 >- (`IMAGE f k ��� {}` by cheat >> 3277 imp_res_tac CHOICE_DEF >> 3278 fs [] >> 3279 fs [] >> 3280 3281 rfs [key_set_eq] >> 3282 fs [key_set_def, resp_equiv2_def] >> 3283 metis_tac [cmp_thms]) 3284 3285 fs [resp_equiv2_def, key_set_def, EXTENSION] >> 3286 rfs [] 3287 metis_tac [] 3288 *) 3289 3290val bigunion_key_sets = Q.prove ( 3291`!cmp1. 3292 good_cmp cmp1 ��� 3293 good_cmp cmp2 ��� 3294 resp_equiv2 cmp1 cmp2 f 3295 ��� 3296 BIGUNION (IMAGE (\x. key_set cmp2 (f x)) (key_set cmp1 x)) = 3297 key_set cmp2 (CHOICE (IMAGE f (key_set cmp1 x)))`, 3298 rw [EXTENSION] >> 3299 `IMAGE f (key_set cmp1 x) ��� {}` by (rw [EXTENSION, key_set_def] >> metis_tac [cmp_thms]) >> 3300 imp_res_tac CHOICE_DEF >> 3301 fs [key_set_def] >> 3302 eq_tac >> 3303 rw [] >> 3304 rfs [resp_equiv2_def] 3305 >- metis_tac [cmp_thms] >> 3306 qexists_tac `key_set cmp2 (f x)` >> 3307 rw [key_set_def] >> 3308 metis_tac [cmp_thms]); 3309 3310val image_lem = Q.prove ( 3311`good_cmp cmp1 3312 ��� 3313 IMAGE (��x. key_set cmp2 (f x)) (key_set cmp1 k'') = 3314 { key_set cmp2 (f x) | x | cmp1 x k'' = Equal }`, 3315 rw [EXTENSION,key_set_def] >> 3316 metis_tac [cmp_thms]); 3317 3318 (* 3319val map_keys_thm = Q.store_thm ("map_keys_thm", 3320`!cmp1 cmp2 f t. 3321 good_cmp cmp1 ��� 3322 good_cmp cmp2 ��� 3323 invariant cmp1 t ��� 3324 resp_equiv2 cmp1 cmp2 f ��� 3325 equiv_inj cmp1 cmp2 f 3326 ��� 3327 invariant cmp2 (map_keys cmp2 f t) ��� 3328 to_fmap cmp2 (map_keys cmp2 f t) = MAP_KEYS (BIGUNION o IMAGE (key_set cmp2 o f)) (to_fmap cmp1 t)`, 3329 3330 simp [map_keys_def] >> 3331 rpt gen_tac >> 3332 DISCH_TAC >> 3333 inv_mp_tac fromList_thm >> 3334 rw [MAP_MAP_o, combinTheory.o_DEF] >> 3335 rw [FLOOKUP_EXT'] >> 3336 `SORTED (��(x,y) (x',y'). cmp1 x x' = Less) (toAscList t) ��� 3337 lift_key cmp1 (set (toAscList t)) = set (fmap_to_alist (to_fmap cmp1 t))` 3338 by metis_tac [toAscList_thm] >> 3339 pop_assum mp_tac >> 3340 simp [EXTENSION, MEM_MAP, LAMBDA_PROD, EXISTS_PROD, FORALL_PROD] >> 3341 `transitive (��(x,y:'c) (x',y':'c). cmp1 x x' = Less)` by metis_tac [good_cmp_trans] >> 3342 rw [in_lift_key] >> 3343 fs [] >> 3344 rw [FLOOKUP_DEF] >> 3345 `INJ (��x. BIGUNION (IMAGE (��x. key_set cmp2 (f x)) x)) (FDOM (to_fmap cmp1 t)) UNIV` 3346 by rw [INJ_DEF] >> 3347 imp_res_tac to_fmap_key_set 3348 rw [] >> 3349 CCONTR_TAC >> 3350 fs [equiv_inj_def] >> 3351 rfs [key_set_eq] >> 3352 `cmp2 (f k'') (f k') ��� Equal` by metis_tac [] 3353 rfs [image_lem] 3354 3355 fs [EXTENSION] 3356 fs [PULL_EXISTS, PULL_FORALL] 3357 3358 3359 rfs [bigunion_key_sets] 3360 3361 fs [resp_equiv2_def, equiv_inj_def] 3362 3363 rw [key_set_def] 3364 fs [key_set_def] 3365 CCONTR_TAC 3366 Cases_on `cmp1 k' k'' = Equal` >> 3367 fs [] 3368 `cmp2 (f k') (f k'') ��� Equal` by metis_tac [cmp_thms] 3369metis_tac [cmp_thms] 3370 3371 Cases_on `ALOOKUP (MAP (��(p1,p2). (key_set cmp2 (f p1),())) (toAscList t)) k = NONE` >> 3372 fs [] 3373 3374 Cases_on `?x. k = key_set cmp2 x` >> 3375 fs [] 3376 >- (Cases_on `?x'. x = f x'` >> 3377 fs [] 3378 >- (first_x_assum (qspecl_then [`key_set cmp1 x'`] mp_tac) >> 3379 rw [] 3380 3381 rw [] >> 3382 3383 3384 fs [lift_key_def] 3385 3386 Cases_on `FLOOKUP (MAP_KEYS (IMAGE f) (to_fmap cmp1 t)) k` 3387 >- (fs [ALOOKUP_NONE, MEM_MAP, LAMBDA_PROD, EXISTS_PROD] >> 3388 CCONTR_TAC >> 3389 fs [] >> 3390 rw [] >> 3391 fs [lift_key_def, resp_equiv2_def, EXTENSION, LAMBDA_PROD,EXISTS_PROD, FORALL_PROD, 3392 PULL_FORALL, PULL_EXISTS]>> 3393 3394 fs [PULL_EXISTS, PULL_FORALL, key_set_def, EXTENSION] 3395 3396 first_x_assum (qspecl_then [`key_set cmp1 p_1'`, `p_2`] assume_tac) >> 3397 fs [FLOOKUP_DEF, MAP_KEYS_def] >> 3398 fs [EXTENSION, key_set_def] >> 3399 metis_tac [cmp_thms] 3400 3401val key_set_map = Q.prove ( 3402`!cmp1 cmp2 f k. 3403 resp_equiv2 cmp1 cmp2 f ��� 3404 IMAGE f (key_set cmp1 k) SUBSET key_set cmp2 (f k)`, 3405 rw [key_set_def, SUBSET_DEF, resp_equiv2_def] >> 3406 metis_tac []); 3407 3408`good_cmp cmp1 ��� good_cmp cmp2 ��� (!x y. cmp1 x y = Equal ��� x = y) /\ (!x y. cmp2 x y = Equal ��� x = y) ��� (!x y. f x = f y ��� x = y) ��� resp_equiv2 cmp1 cmp2 f` 3409 rw [resp_equiv2_def] >> 3410 metis_tac [cmp_thms] 3411 3412 3413val flookup_lem = Q.prove ( 3414`!cmp1 cmp2 m k v f. 3415 (FLOOKUP m k = 3416 FLOOKUP (MAP_KEYS (BIGUNION o IMAGE (��x. key_set cmp2 (f x))) m) (BIGUNION o IMAGE (��x. key_set cmp2 (f k))))`, 3417 3418 rw [FLOOKUP_DEF, MAP_KEYS_def] >> 3419 eq_tac >> 3420 rw [] 3421 3422 3423val map_keys_thm = Q.store_thm ("map_keys_thm", 3424`!cmp1 cmp2 f t. 3425 good_cmp cmp1 ��� 3426 good_cmp cmp2 ��� 3427 invariant cmp1 t ��� 3428 resp_equiv2 cmp1 cmp2 f 3429 ��� 3430 invariant cmp2 (map_keys cmp2 f t) ��� 3431 to_fmap cmp2 (map_keys cmp2 f t) = MAP_KEYS (IMAGE f) (to_fmap cmp1 t)`, 3432 3433 simp [map_keys_def] >> 3434 rpt gen_tac >> 3435 DISCH_TAC >> 3436 inv_mp_tac fromList_thm >> 3437 rw [MAP_MAP_o, combinTheory.o_DEF] >> 3438 rw [LAMBDA_PROD] >> 3439 rw [FLOOKUP_EXT'] >> 3440 `SORTED (��(x,y) (x',y'). cmp1 x x' = Less) (toAscList t) ��� 3441 lift_key cmp1 (set (toAscList t)) = set (fmap_to_alist (to_fmap cmp1 t))` 3442 by metis_tac [toAscList_thm] >> 3443 pop_assum mp_tac >> 3444 simp [EXTENSION, MEM_MAP, LAMBDA_PROD, EXISTS_PROD, FORALL_PROD] >> 3445 `transitive (��(x,y:'c) (x',y':'c). cmp1 x x' = Less)` by metis_tac [good_cmp_trans] >> 3446 rw [in_lift_key] >> 3447 fs [] 3448 3449 3450 fs [lift_key_def] 3451 3452 Cases_on `FLOOKUP (MAP_KEYS (IMAGE f) (to_fmap cmp1 t)) k` 3453 >- (rw [ALOOKUP_NONE, MEM_MAP, LAMBDA_PROD, EXISTS_PROD] >> 3454 CCONTR_TAC >> 3455 fs [] >> 3456 rw [] >> 3457 fs [lift_key_def, resp_equiv2_def, EXTENSION, LAMBDA_PROD,EXISTS_PROD, FORALL_PROD, 3458 PULL_FORALL, PULL_EXISTS]>> 3459 3460 fs [PULL_EXISTS, PULL_FORALL, key_set_def, EXTENSION] 3461 3462 first_x_assum (qspecl_then [`key_set cmp1 p_1'`, `p_2`] assume_tac) >> 3463 fs [FLOOKUP_DEF, MAP_KEYS_def] >> 3464 fs [EXTENSION, key_set_def] >> 3465 metis_tac [cmp_thms] 3466 *) 3467 3468val every_def = Define ` 3469(every f Tip = T) ��� 3470(every f (Bin _ kx x l r) = 3471 if f kx x then 3472 if every f l then 3473 if every f r then T else F 3474 else F 3475 else F)`; 3476 3477val every_thm = Q.store_thm ("every_thm", 3478`!f t cmp. 3479 good_cmp cmp ��� 3480 invariant cmp t ��� 3481 resp_equiv cmp f 3482 ��� 3483 (every f t ��� (!k v. lookup cmp k t = SOME v ��� f k v))`, 3484 Induct_on `t` >> 3485 rw [every_def, lookup_def] >> 3486 fs [invariant_eq, resp_equiv_def] >> 3487 first_x_assum (qspecl_then [`f`, `cmp`] assume_tac) >> 3488 first_x_assum (qspecl_then [`f`, `cmp`] assume_tac) >> 3489 rfs [] >> 3490 eq_tac >> 3491 rw [] 3492 >- (EVERY_CASE_TAC >> 3493 fs [] >> 3494 metis_tac []) 3495 >- (first_x_assum (qspecl_then [`k`] assume_tac) >> 3496 rfs [] >> 3497 EVERY_CASE_TAC >> 3498 fs [] >> 3499 metis_tac [cmp_thms]) 3500 >- (first_x_assum (qspecl_then [`k'`] assume_tac) >> 3501 EVERY_CASE_TAC >> 3502 fs [] >> 3503 rfs [lookup_thm, flookup_thm] >> 3504 rfs [key_ordered_to_fmap] >> 3505 res_tac >> 3506 imp_res_tac key_set_cmp_thm >> 3507 metis_tac [cmp_thms]) 3508 >- (first_x_assum (qspecl_then [`k'`] assume_tac) >> 3509 EVERY_CASE_TAC >> 3510 fs [] >> 3511 rfs [lookup_thm, flookup_thm] >> 3512 rfs [key_ordered_to_fmap] >> 3513 res_tac >> 3514 imp_res_tac key_set_cmp_thm >> 3515 metis_tac [cmp_thms])); 3516 3517val exists_def = Define ` 3518(exists f Tip = F) ��� 3519(exists f (Bin _ kx x l r) = 3520 if f kx x then 3521 T 3522 else if exists f l then 3523 T 3524 else if exists f r then 3525 T 3526 else 3527 F)`; 3528 3529val exists_thm = Q.store_thm ("exists_thm", 3530`!f t cmp. 3531 good_cmp cmp ��� 3532 invariant cmp t ��� 3533 resp_equiv cmp f 3534 ��� 3535 (exists f t ��� (?k v. lookup cmp k t = SOME v ��� f k v))`, 3536 Induct_on `t` >> 3537 rw [exists_def, lookup_def] >> 3538 fs [invariant_eq, resp_equiv_def] >> 3539 first_x_assum (qspecl_then [`f`, `cmp`] assume_tac) >> 3540 first_x_assum (qspecl_then [`f`, `cmp`] assume_tac) >> 3541 rfs [] >> 3542 eq_tac >> 3543 rw [] 3544 >- metis_tac [cmp_thms] 3545 >- (qexists_tac `k'` >> 3546 rw [] >> 3547 EVERY_CASE_TAC >> 3548 fs [] >> 3549 rfs [lookup_thm, flookup_thm] >> 3550 rfs [key_ordered_to_fmap] >> 3551 res_tac >> 3552 imp_res_tac key_set_cmp_thm >> 3553 metis_tac [cmp_thms]) 3554 >- (qexists_tac `k'` >> 3555 rw [] >> 3556 EVERY_CASE_TAC >> 3557 fs [] >> 3558 rfs [lookup_thm, flookup_thm] >> 3559 rfs [key_ordered_to_fmap] >> 3560 res_tac >> 3561 imp_res_tac key_set_cmp_thm >> 3562 metis_tac [cmp_thms]) 3563 >- (EVERY_CASE_TAC >> 3564 fs [] >> 3565 metis_tac [])); 3566 3567val _ = export_theory (); 3568