1(* file HS/PIN/fmapalScript.sml, created 6/2/13 F.L. Morris *) 2(* tree-based finite function representation; name a homage to numeralTheory *) 3(* Uses bt, bl basics from enumeralScript, puts 'a#'b in place of 'a. *) 4(* Revised 13 Dec. 2013 for HOL_Kananaskis 9. *) 5 6open HolKernel boolLib Parse; 7 8(* app load ["totoTheory", "res_quanLib", "enumeralTheory", 9 "finite_mapTheory", "combinTheory"]; *) 10(* comment out above load when Holmaking *) 11val _ = set_trace "Unicode" 0; 12open pred_setLib pred_setTheory relationTheory res_quanTheory res_quanLib; 13open pairTheory PairRules optionTheory finite_mapTheory; 14open totoTheory bossLib listTheory enumeralTheory; 15 16val _ = new_theory "fmapal"; 17 18val _ = ParseExtras.temp_loose_equality() 19val cpn_case_def = TypeBase.case_def_of ``:ordering`` 20val cpn_distinct = TypeBase.distinct_of ``:ordering`` 21val cpn_nchotomy = TypeBase.nchotomy_of ``:ordering`` 22 23(* "fmapal" for "numeral-ish finite map", wordplay on "NUMERAL", "enumeral". *) 24(* Temptation to call it "funeralTheory" reluctantly resisted. *) 25 26(* My habitual abbreviations: *) 27 28val AR = ASM_REWRITE_TAC []; 29fun ulist x = [x]; 30fun rrs th = REWRITE_RULE [SPECIFICATION] th; 31 32(* ****** Make FUNION infix. ********* *) 33 34val _ = set_fixity "FUNION" (Infixl 500); 35 36val _ = Defn.def_suffix := ""; (* replacing default "_def" *) 37 38(* ***************************************************************** *) 39(* Following switch, BigSig, allows "maybe_thm" to act either as *) 40(* store_thm or as prove, thus maximizing or minimizing the output *) 41(* from print_theory and the stuff known to DB.match, DB.find *) 42(* ***************************************************************** *) 43 44val BigSig = false; 45 46fun maybe_thm (s, tm, tac) = if BigSig then store_thm (s, tm, tac) 47 else prove (tm, tac); 48 49val ORL = Define`(ORL (cmp:'a toto) ([]:('a#'b)list) = T) /\ 50 (ORL cmp ((a,b) :: l) = ORL cmp l /\ 51 (!p q. MEM (p,q) l ==> (apto cmp a p = LESS)))`; 52 53val ORL_LEM = maybe_thm ("ORL_LEM", Term 54`!cmp l:('a#'b)list m. ORL cmp (l ++ m) ==> ORL cmp l /\ ORL cmp m`, 55GEN_TAC THEN Induct THEN REWRITE_TAC [APPEND, ORL] THEN 56P_PGEN_TAC (Term`x:'a,y:'b`) THEN ASM_REWRITE_TAC [ORL] THEN 57REWRITE_TAC [MEM_APPEND] THEN REPEAT STRIP_TAC THEN RES_TAC THEN AR); 58 59val MEM_FST = maybe_thm ("MEM_FST", 60``!x l:('a#'b)list. (?y. MEM (x,y) l) <=> MEM x (MAP FST l)``, 61GEN_TAC THEN Induct THENL 62[REWRITE_TAC [MEM, MAP] 63,P_PGEN_TAC ``a:'a, b:'b`` THEN SRW_TAC [] [MAP,MEM] THEN 64 METIS_TAC [MEM] 65]); 66 67val ORL_OL_FST = maybe_thm ("ORL_OL_FST", 68``!cmp:'a toto l:('a#'b) list. ORL cmp l <=> OL cmp (MAP FST l)``, 69GEN_TAC THEN Induct THENL 70[REWRITE_TAC [ORL, OL, MAP] 71,P_PGEN_TAC ``a:'a, b:'b`` THEN SRW_TAC [] [MAP, ORL, OL] THEN 72 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV FORALL_IMP_CONV)) THEN 73 REWRITE_TAC [MEM_FST] 74]); 75 76(* A useful way of combining option values, that I don't find premade: *) 77 78val optry = Define`(optry (SOME p) (q:'z option) = SOME p) 79 /\ (optry NONE q = q)`; 80 81val optry_case = maybe_thm ("optry_case", Term 82`!p q:'z option. optry p q = case p of SOME x => SOME x | NONE => q`, 83REPEAT GEN_TAC THEN Cases_on `p` THEN REWRITE_TAC [optry, option_CLAUSES] THEN 84BETA_TAC THEN REFL_TAC); 85 86val optry_ASSOC = maybe_thm ("optry_ASSOC", Term 87`!p q r:'z option. optry p (optry q r) = optry (optry p q) r`, 88REPEAT GEN_TAC THEN 89Cases_on `p` THEN REWRITE_TAC [option_case_def, optry]); 90 91val optry_ID = maybe_thm ("optry_ID", Term 92`(!p:'z option. optry p NONE = p) /\ (!p:'z option. optry NONE p = p)`, 93REWRITE_TAC [optry] THEN Cases THEN REWRITE_TAC [optry]); 94 95val IS_SOME_optry = maybe_thm ("IS_SOME_optry", 96``!a b:'a option. IS_SOME a ==> (optry a b = a)``, 97REPEAT GEN_TAC THEN Cases_on `a` THEN 98ASM_REWRITE_TAC [optry, option_CLAUSES]); 99 100val optry_list = Define 101 `(optry_list (f:'z->'g option) ([]:'z option list) = NONE) 102/\ (optry_list f ((NONE:'z option) :: l) = optry_list f l) 103/\ (optry_list f (SOME (z:'z) :: l) = optry (f z) (optry_list f l))`; 104 105(* We define the following function, assocv, to give the option-valued 106function embodied by an association list. The name is chosen both to 107avoid confusion with the usual contraction for "associative" and to 108indicate departure from the Lisp-ML tradition of assoc's that return 109the argument-value pair; "v" is for "value [only]". *) 110 111val assocv = Define`(assocv ([]:('a#'b)list) (a:'a) = NONE) 112 /\ (assocv ((x:'a, y:'b) :: l) a = 113 if a = x then SOME y else assocv l a)`; 114 115(* But for more convenient partial application below at incr_merge_lem: *) 116 117val vcossa = Define`vcossa a (l:('a#'b)list) = assocv l a`; 118 119(* Define an update-like binary operation on option valued functions: *) 120 121val OPTION_UPDATE = Define 122`OPTION_UPDATE (f:'a->'b option) g x = optry (f x) (g x)`; 123 124val IS_SOME_OPTION_UPDATE = prove ( 125``!u (v:'a -> 'b option). IS_SOME o OPTION_UPDATE u v = 126 IS_SOME o u UNION IS_SOME o v``, 127REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN 128REWRITE_TAC [rrs IN_UNION, combinTheory.o_THM, OPTION_UPDATE, optry_case] THEN 129Cases_on `u x` THEN REWRITE_TAC [option_CLAUSES] THEN 130BETA_TAC THEN REWRITE_TAC [option_CLAUSES]); 131 132(* ***************************************************************** *) 133(* merge sorting for functions (as association lists here. We call *) 134(* the basic list-combining function, which gives priority to the *) 135(* first argument, just "merge". This corresponds to FUNION in fmap,*) 136(* not to FMERGE. Corresponding set functions use "smerge", etc. *) 137(* ***************************************************************** *) 138 139val merge = Define`(merge (cmp:'a toto) [] (l:('a#'b)list) = l) 140 /\ (merge (cmp:'a toto) l [] = l) 141 /\ (merge (cmp:'a toto) ((a1, b1) :: l1) ((a2, b2) :: l2) = 142 case apto cmp a1 a2 of 143 LESS => (a1, b1) :: merge cmp l1 ((a2, b2) :: l2) 144 | EQUAL => (a1, b1:'b) :: merge cmp l1 l2 145 | GREATER => (a2, b2) :: merge cmp ((a1, b1) :: l1) l2)`; 146 147val merge_ind = theorem "merge_ind"; 148 149(* merge_ind = |- !P. 150 (!cmp l. P cmp [] l) /\ (!cmp v4 v5. P cmp (v4::v5) []) /\ 151 (!cmp a1 b1 l1 a2 b2 l2. 152 ((apto cmp a1 a2 = EQUAL) ==> P cmp l1 l2) /\ 153 ((apto cmp a1 a2 = GREATER) ==> P cmp ((a1,b1)::l1) l2) /\ 154 ((apto cmp a1 a2 = LESS) ==> P cmp l1 ((a2,b2)::l2)) ==> 155 P cmp ((a1,b1)::l1) ((a2,b2)::l2)) ==> 156 !v v1 v2. P v v1 v2 *) 157 158val merge_thm = maybe_thm ("merge_thm", Term 159`!cmp:'a toto. (!m:('a#'b)list. merge cmp [] m = m) 160 /\ (!l:('a#'b)list. merge cmp l [] = l) 161 /\ (!a1:'a b1:'b a2:'a b2:'b l1 l2. 162 merge cmp ((a1, b1) :: l1) ((a2, b2) :: l2) = 163 case apto cmp a1 a2 of 164 LESS => (a1, b1) :: merge cmp l1 ((a2, b2) :: l2) 165 | EQUAL => (a1, b1:'b) :: merge cmp l1 l2 166 | GREATER => (a2, b2) :: merge cmp ((a1, b1) :: l1) l2)`, 167GEN_TAC THEN REWRITE_TAC [merge] THEN 168Cases_on `l:('a#'b)list` THENL 169[REWRITE_TAC [merge] 170,PURE_ONCE_REWRITE_TAC [GSYM PAIR] THEN REWRITE_TAC [merge]]); 171 172(* If we are to use incr_sort, we doubtless will need to prove that its 173ouput is sorted and contains the pairs that assocv would find from its 174argument. *) 175 176(* Possibly better imitate enumeral more: _ORL thms might come from 177 lemmas like MAP FST (merge cmp l m) = smerge cmp (MAP FST l) (MAP FST m), 178 and corresponding to _set thms might be _assocv thms, or direct to fmaps.*) 179 180val merge_FST_smerge = maybe_thm ("merge_FST_smerge", 181``!cmp:'a toto l m:('a#'b)list. 182 MAP FST (merge cmp l m) = smerge cmp (MAP FST l) (MAP FST m)``, 183GEN_TAC THEN Induct THENL 184[REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [merge_thm, smerge_nil, MAP] 185,P_PGEN_TAC (Term`(a:'a,b:'b)`) THEN Induct THENL 186 [REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [merge_thm, smerge_nil, MAP] 187 ,P_PGEN_TAC (Term`(a':'a,b':'b)`) THEN 188 SRW_TAC [] [merge_thm, smerge, MAP, FST] THEN 189 Cases_on `apto cmp a a'` THEN 190 SRW_TAC [] [] 191]]); 192 193val merge_ORL = maybe_thm ("merge_ORL", ``!cmp:'a toto l m:('a#'b)list. 194 ORL cmp l /\ ORL cmp m ==> ORL cmp (merge cmp l m)``, 195METIS_TAC [smerge_OL, merge_FST_smerge, ORL_OL_FST]); 196 197(* **** We need to show that assocv is preserved by sorting **** *) 198 199val merge_subset_union = maybe_thm ("merge_subset_union", 200``!cmp:'a toto l m:('a#'b)list h. 201 MEM h (merge cmp l m) ==> MEM h l \/ MEM h m``, 202HO_MATCH_MP_TAC merge_ind THEN 203REPEAT CONJ_TAC THEN REPEAT GEN_TAC THENL 204[REWRITE_TAC [MEM, merge] 205,REWRITE_TAC [MEM, merge] 206,CONV_TAC (RAND_CONV (REWRITE_CONV [merge])) THEN 207 Cases_on `apto cmp a1 a2` THEN 208 REWRITE_TAC [all_cpn_distinct] THEN 209 STRIP_TAC THEN GEN_TAC THEN REWRITE_TAC [cpn_case_def] THEN 210 CONV_TAC (LAND_CONV (REWRITE_CONV [MEM])) THEN 211 STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC [MEM]]); 212 213val MEM_MEM_merge = maybe_thm ("MEM_MEM_merge", 214``!cmp:'a toto l m:('a#'b)list x y. 215 MEM (x,y) l ==> MEM (x,y) (merge cmp l m)``, 216HO_MATCH_MP_TAC merge_ind THEN 217REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [MEM, merge] THEN 218Cases_on `apto cmp a1 a2` THEN 219REWRITE_TAC [all_cpn_distinct] THEN 220REPEAT STRIP_TAC THEN REWRITE_TAC [cpn_case_def, MEM] THEN RES_TAC THEN AR); 221 222val NOT_MEM_merge = maybe_thm ("NOT_MEM_merge", 223``!cmp:'a toto l m:('a#'b)list x y. (!z.~MEM (x,z) l) ==> 224 (MEM (x,y) (merge cmp l m) <=> MEM (x,y) m)``, 225HO_MATCH_MP_TAC merge_ind THEN 226REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [MEM, merge] THENL 227[DISCH_TAC THEN AR 228,REWRITE_TAC [DE_MORGAN_THM] THEN CONV_TAC (DEPTH_CONV FORALL_AND_CONV) THEN 229 Cases_on `apto cmp a1 a2` THEN 230 REWRITE_TAC [cpn_distinct, GSYM cpn_distinct] THEN 231 REPEAT STRIP_TAC THEN 232 REWRITE_TAC [cpn_case_def, MEM] THENL 233 [RES_TAC THEN AR 234 ,IMP_RES_THEN (REWRITE_TAC o ulist o SYM) toto_equal_imp_eq THEN 235 RES_TAC THEN UNDISCH_TAC (Term`!z. (x:'a,z:'b) <> (a1,b1)`) THEN 236 ASM_REWRITE_TAC [PAIR_EQ, DE_MORGAN_THM] THEN 237 CONV_TAC (LAND_CONV (FORALL_OR_CONV THENC (RAND_CONV FORALL_NOT_CONV))) THEN 238 SUBGOAL_THEN (Term`?z:'b.z=b1`) (REWRITE_TAC o ulist) THENL 239 [EXISTS_TAC (Term`b1:'b`) THEN REFL_TAC 240 ,DISCH_TAC THEN AR 241 ] 242 ,RES_TAC THEN AR 243]]); 244 245(* By good fortune, the previous three lemmas about merge (including 246 merge_subset_union) did not care if the lists were sorted or not. *) 247 248(* ****** more lemmas that do need an ORL hypothesis ****** *) 249 250val ORL_single_valued = prove (Term`!cmp l. ORL cmp l ==> 251 !x:'a y:'b z. MEM (x,y) l /\ MEM (x,z) l ==> (z = y)`, 252GEN_TAC THEN Induct THENL 253[REWRITE_TAC [MEM] 254,P_PGEN_TAC (Term`p:'a,q:'b`) THEN 255 DISCH_TAC THEN IMP_RES_TAC ORL THEN REPEAT GEN_TAC THEN 256 Cases_on `apto cmp x p` THEN 257 IMP_RES_TAC toto_glneq THEN IMP_RES_TAC toto_equal_imp_eq THEN 258 ASM_REWRITE_TAC [MEM, PAIR_EQ] THEN STRIP_TAC THEN RES_TAC THENL 259 [AR 260 ,IMP_RES_THEN MP_TAC toto_glneq THEN REWRITE_TAC [] 261 ,IMP_RES_THEN MP_TAC toto_glneq THEN REWRITE_TAC [] 262 ]]); 263 264val merge_MEM_thm = maybe_thm ("merge_MEM_thm", 265``!cmp:'a toto l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==> 266 (!x y. MEM (x,y) (merge cmp l m) 267 <=> MEM (x,y) l \/ MEM (x,y) m /\ !z.~MEM (x,z) l)``, 268REPEAT STRIP_TAC THEN EQ_TAC THENL 269[Cases_on `!z. ~MEM (x,z) l` THENL 270 [DISCH_TAC THEN IMP_RES_TAC merge_subset_union THEN AR 271 ,DISCH_TAC THEN 272 UNDISCH_TAC (Term`~!z. ~MEM (x:'a,z:'b) l`) THEN 273 CONV_TAC (LAND_CONV NOT_FORALL_CONV) THEN REWRITE_TAC [] THEN STRIP_TAC THEN 274 SUBGOAL_THEN (Term`MEM (x:'a,z:'b) (merge cmp l m)`) ASSUME_TAC THENL 275 [IMP_RES_TAC MEM_MEM_merge THEN AR 276 ,SUBGOAL_THEN (Term`ORL cmp (merge cmp (l:('a#'b)list) m)`) 277 (MP_TAC o MATCH_MP ORL_single_valued) THENL 278 [MATCH_MP_TAC merge_ORL THEN AR 279 ,DISCH_THEN (fn imp => 280 SUBGOAL_THEN (Term`y:'b = z`) (ASM_REWRITE_TAC o ulist) THEN 281 MATCH_MP_TAC imp) THEN 282 EXISTS_TAC (Term`x:'a`) THEN AR 283 ]]] 284,STRIP_TAC THENL 285 [IMP_RES_TAC MEM_MEM_merge THEN AR 286 ,IMP_RES_TAC NOT_MEM_merge THEN AR 287]]); 288 289val ORL_TL = maybe_thm ("ORL_TL", Term 290`!cmp ab:('a#'b) l. ORL cmp (ab::l) ==> ORL cmp l`, 291GEN_TAC THEN P_PGEN_TAC (Term`a:'a,b:'b`) THEN 292REWRITE_TAC [ORL] THEN REPEAT STRIP_TAC THEN AR); 293 294val assocv_MEM_thm = maybe_thm ("assocv_MEM_thm", 295``!cmp l. ORL cmp l ==> (!x:'a y:'b. (assocv l x = SOME y) <=> MEM (x,y) l)``, 296GEN_TAC THEN Induct THENL 297[REWRITE_TAC [assocv, MEM, option_CLAUSES] 298,P_PGEN_TAC (Term`p:'a,q:'b`) THEN 299 DISCH_TAC THEN REPEAT GEN_TAC THEN IMP_RES_TAC ORL_TL THEN RES_TAC THEN 300 Cases_on `x = p` THENL 301 [EQ_TAC THENL 302 [ASM_REWRITE_TAC [assocv, MEM, PAIR_EQ, option_CLAUSES] THEN 303 DISCH_TAC THEN AR 304 ,SUBGOAL_THEN (Term`MEM (x:'a,q:'b) ((p,q)::l)`) ASSUME_TAC THENL 305 [ASM_REWRITE_TAC [MEM] 306 ,DISCH_TAC THEN SUBGOAL_THEN (Term`q:'b = y`) 307 (fn eq => ASSUME_TAC eq THEN 308 ASM_REWRITE_TAC [assocv, option_CLAUSES]) THEN 309 IMP_RES_TAC ORL_single_valued]] 310 ,ASM_REWRITE_TAC [MEM, assocv, PAIR_EQ] 311]]); 312 313(* Following 2 lemmas can be proved with hypothesis ORL cmp l from 314 assoc_MEM_thm, but are easier to use without the hypothesis. *) 315 316val assocv_NOT_MEM = maybe_thm ("assocv_NOT_MEM", Term 317`!x:'a l. (assocv l x = NONE) <=> !y:'b. ~MEM (x,y) l`, 318GEN_TAC THEN Induct THEN REWRITE_TAC [assocv, MEM] THEN 319P_PGEN_TAC (Term`a:'a,b:'b`) THEN 320ASM_REWRITE_TAC [assocv, PAIR_EQ] THEN COND_CASES_TAC THENL 321[REWRITE_TAC [option_CLAUSES] THEN CONV_TAC NOT_FORALL_CONV THEN 322 EXISTS_TAC (Term`b:'b`) THEN REWRITE_TAC [] 323,AR]); 324 325val NOT_MEM_merge = maybe_thm ("NOT_MEM_merge", 326``!cmp:'a toto l m. ORL cmp l /\ ORL cmp m ==> 327 !a. (!z. ~MEM (a:'a,z:'b) (merge cmp l m)) ==> 328 (!z. ~MEM (a,z) l) /\ (!z. ~MEM (a,z) m)``, 329REPEAT GEN_TAC THEN DISCH_THEN (fn conj => GEN_TAC THEN 330 ASSUME_TAC (MATCH_MP merge_ORL conj) THEN 331CONV_TAC (RAND_CONV (AND_FORALL_CONV THENC 332 QUANT_CONV (REWRITE_CONV [GSYM DE_MORGAN_THM])) THENC 333 BINOP_CONV FORALL_NOT_CONV THENC 334 CONTRAPOS_CONV THENC REWRITE_CONV [NOT_CLAUSES]) THEN 335STRIP_TAC THEN MP_TAC (MATCH_MP merge_MEM_thm conj)) THENL 336[DISCH_TAC THEN EXISTS_TAC (Term`z:'b`) THEN 337 MATCH_MP_TAC MEM_MEM_merge THEN AR 338,DISCH_THEN (REWRITE_TAC o ulist) THEN 339 Cases_on `?y. MEM (a,y) l` THENL 340 [UNDISCH_TAC (Term`?y. MEM (a:'a,y:'b) l`) THEN STRIP_TAC THEN 341 EXISTS_TAC (Term`y:'b`) THEN AR 342 ,UNDISCH_TAC (Term`~?y. MEM (a:'a,y:'b) l`) THEN 343 CONV_TAC (LAND_CONV NOT_EXISTS_CONV) THEN DISCH_TAC THEN 344 EXISTS_TAC (Term`z:'b`) THEN AR 345]]); 346 347val assocv_merge = maybe_thm ("assocv_merge", Term`!cmp l m:('a#'b)list a. 348 ORL cmp l /\ ORL cmp m ==> 349 (assocv (merge cmp l m) a = optry (assocv l a) (assocv m a))`, 350REPEAT GEN_TAC THEN DISCH_THEN (fn conj => 351 ASSUME_TAC (MATCH_MP merge_ORL conj) THEN 352 MP_TAC (MATCH_MP merge_MEM_thm conj) THEN 353 ASSUME_TAC conj) THEN 354Cases_on `assocv (merge cmp l m) a` THEN 355REWRITE_TAC [optry_case] THENL 356[DISCH_THEN (fn th => ALL_TAC) THEN IMP_RES_TAC assocv_NOT_MEM THEN 357 SUBGOAL_THEN (Term`(!b. ~MEM (a:'a,b:'b) l) /\ !b. ~MEM (a:'a,b:'b) m`) 358 MP_TAC THENL 359 [CONJ_TAC THEN IMP_RES_TAC (MATCH_MP NOT_MEM_merge 360 (ASSUME (Term`ORL cmp (l:('a#'b)list) /\ 361 ORL cmp (m:('a#'b)list)`))) 362 ,REWRITE_TAC [GSYM assocv_NOT_MEM] THEN STRIP_TAC THEN 363 ASM_REWRITE_TAC [option_CLAUSES] 364 ] 365,IMP_RES_TAC assocv_MEM_thm THEN 366 DISCH_THEN (IMP_RES_THEN MP_TAC) THEN 367 UNDISCH_TAC (Term`ORL cmp (l:('a#'b)list) /\ 368 ORL cmp (m:('a#'b)list)`) THEN STRIP_TAC THEN 369 STRIP_TAC THENL 370 [IMP_RES_TAC assocv_MEM_thm THEN ASM_REWRITE_TAC [option_CLAUSES] THEN 371 BETA_TAC THEN REFL_TAC 372 ,IMP_RES_TAC assocv_NOT_MEM THEN 373 IMP_RES_TAC assocv_MEM_thm THEN ASM_REWRITE_TAC [option_CLAUSES] 374 ]]); 375 376val merge_fun = maybe_thm ("merge_fun", 377``!cmp:'a toto l:('a#'b)list m. ORL cmp l /\ ORL cmp m ==> 378(assocv (merge cmp l m) = OPTION_UPDATE (assocv l) (assocv m))``, 379REPEAT STRIP_TAC THEN 380CONV_TAC FUN_EQ_CONV THEN REWRITE_TAC [OPTION_UPDATE] THEN 381MATCH_MP_TAC assocv_merge THEN AR); 382 383(* Continue development of sorting in same imitative style as for merge. *) 384 385val incr_merge = Define` 386 (incr_merge cmp (l:('a#'b)list) [] = [SOME l]) 387/\ (incr_merge cmp (l:('a#'b)list) (NONE :: lol) = SOME l :: lol) 388/\ (incr_merge cmp (l:('a#'b)list) (SOME m :: lol) = 389 NONE :: incr_merge cmp (merge cmp l m) lol)`; 390 391val ORL_sublists = Define`(ORL_sublists cmp ([]:('a#'b)list option list) = T) 392 /\ (ORL_sublists cmp (NONE :: (lol:('a#'b)list option list)) = 393 ORL_sublists cmp lol) 394 /\ (ORL_sublists cmp (SOME m :: (lol:('a#'b)list option list)) = 395 ORL cmp m /\ ORL_sublists cmp lol)`; 396 397val ORL_sublists_ind = theorem"ORL_sublists_ind"; 398 399(* ORL_sublists_ind = 400 |- !P. (!cmp. P cmp []) /\ (!cmp lol. P cmp lol ==> P cmp (NONE::lol)) /\ 401 (!cmp m lol. P cmp lol ==> P cmp (SOME m::lol)) ==> 402 !v v1. P v v1 *) 403 404val ORL_OL_FST_sublists = maybe_thm ("ORL_OL_FST_sublists", 405``!cmp lol:('a#'b)list option list. ORL_sublists cmp lol = 406 OL_sublists cmp (MAP (OPTION_MAP (MAP FST)) lol)``, 407GEN_TAC THEN Induct THENL 408[RW_TAC (srw_ss()) [ORL_sublists, OL_sublists, MAP] 409,Cases THEN 410 SRW_TAC [] [ORL_sublists, OL_sublists, MAP, OPTION_MAP_DEF] THEN 411 ASM_REWRITE_TAC [ORL_OL_FST] 412]); 413 414val incr_merge_FST_smerge = maybe_thm ("incr_merge_FST_smerge", 415``!cmp lol l:('a#'b)list. MAP (OPTION_MAP (MAP FST)) (incr_merge cmp l lol) = 416incr_smerge cmp (MAP FST l) (MAP (OPTION_MAP (MAP FST)) lol)``, 417GEN_TAC THEN Induct THENL 418[RW_TAC (srw_ss()) [incr_merge, incr_smerge, MAP] 419,Cases THEN 420 SRW_TAC [] [incr_merge, incr_smerge, MAP, OPTION_MAP_DEF] THEN 421 REWRITE_TAC [merge_FST_smerge] 422]); 423 424val incr_merge_ORL = maybe_thm ("incr_merge_ORL", 425``!cmp:'a toto l:('a#'b)list lol. ORL cmp l /\ 426 ORL_sublists cmp lol ==> ORL_sublists cmp (incr_merge cmp l lol)``, 427METIS_TAC [smerge_OL, incr_smerge_OL, merge_ORL, merge_FST_smerge, 428 incr_merge_FST_smerge, ORL_OL_FST, ORL_OL_FST_sublists]); 429 430val NOT_MEM_NIL = maybe_thm ("NOT_MEM_NIL", 431``(!x:'c. ~MEM x l) <=> (l = [])``, 432EQ_TAC THENL 433[CONV_TAC (CONTRAPOS_CONV THENC (RAND_CONV (NOT_FORALL_CONV))) THEN 434 Cases_on `l` THEN SRW_TAC [] [] THEN 435 Q.EXISTS_TAC `h` THEN REWRITE_TAC [] 436,RW_TAC bool_ss [MEM]]); 437 438val SOME_MEM_NOT_NIL = maybe_thm ("SOME_MEM_NOT_NIL", 439``~(!ab:'a#'b. MEM ab ((x,y)::l) <=> MEM ab [])``, 440RW_TAC (srw_ss()) [MEM] THEN Q.EXISTS_TAC `x,y` THEN REWRITE_TAC []); 441 442val ORL_NOT_MEM = maybe_thm ("ORL_NOT_MEM", Term 443`(!cmp (b:'b) x y l. ORL cmp ((x:'a,y)::l) ==> ~MEM (x,b) l) /\ 444 (!cmp (a:'a) (b:'b) x y l. ORL cmp ((x,y)::l) /\ (apto cmp a x = LESS) ==> 445 ~MEM (a,b) ((x,y)::l))`, 446CONJ_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [ORL] THEN STRIP_TAC THENL 447[DISCH_TAC THEN RES_THEN MP_TAC 448,REWRITE_TAC [MEM, DE_MORGAN_THM, PAIR_EQ] THEN 449 IMP_RES_TAC toto_glneq THEN AR THEN 450 STRIP_TAC THEN RES_TAC THEN IMP_RES_TAC totoLLtrans THEN 451 UNDISCH_TAC (Term`apto cmp a (a:'a) = LESS`)] THEN 452REWRITE_TAC [toto_refl, all_cpn_distinct]); 453 454val ORL_MEM_FST = maybe_thm ("ORL_MEM_FST", 455``!cmp l:('a#'b)list. ORL cmp l ==> 456 !x y p q. MEM (x,y) l /\ MEM (p,q) l /\ (x = p) ==> (y = q)``, 457GEN_TAC THEN Induct THENL 458[REWRITE_TAC [MEM] 459,P_PGEN_TAC ``g:'a,h:'b`` THEN SRW_TAC [] [] THENL 460[`~MEM (g,q) l` 461 by (MATCH_MP_TAC (CONJUNCT1 ORL_NOT_MEM) THEN 462 Q.EXISTS_TAC `cmp` THEN Q.EXISTS_TAC `h` THEN AR) 463,`~MEM (g,y) l` by (MATCH_MP_TAC (CONJUNCT1 ORL_NOT_MEM) THEN 464 Q.EXISTS_TAC `cmp` THEN Q.EXISTS_TAC `h` THEN AR) 465,IMP_RES_TAC ORL_TL THEN `p = p` by REFL_TAC THEN RES_TAC 466]]); 467 468val ORL_MEM_EQ = maybe_thm ("ORL_MEM_EQ", 469``!cmp l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==> 470 ((!ab. MEM ab l <=> MEM ab m) <=> (l = m))``, 471GEN_TAC THEN Induct THENL 472[SRW_TAC [] [GSYM NOT_MEM_NIL] 473,P_PGEN_TAC ``x:'a,y:'b`` THEN Induct THENL 474 [RW_TAC (srw_ss()) [SOME_MEM_NOT_NIL] 475 ,P_PGEN_TAC ``p:'a,q:'b`` THEN 476 STRIP_TAC THEN IMP_RES_TAC ORL_NOT_MEM THEN 477 EQ_TAC THENL 478 [Cases_on `apto cmp x p` THENL 479 [CONV_TAC LEFT_IMP_FORALL_CONV THEN 480 Q.EXISTS_TAC `x,y` THEN 481 `~MEM (x,y) ((p,q)::m)` by (RES_TAC THEN AR) THEN ASM_REWRITE_TAC [MEM] 482 ,REWRITE_TAC [list_11, PAIR_EQ] THEN 483 Q.SUBGOAL_THEN `(!ab. MEM ab l <=> MEM ab m) <=> (l = m)` (SUBST1_TAC o SYM) 484 THEN1 (IMP_RES_TAC ORL_TL THEN RES_TAC) THEN 485 `x = p` by IMP_RES_TAC toto_equal_eq THEN 486 `MEM (x,y) ((x,y)::l)` by REWRITE_TAC [MEM] THEN 487 `MEM (p,q) ((p,q)::m)` by REWRITE_TAC [MEM] THEN 488 DISCH_THEN (fn eq => `MEM (p,q) ((x,y)::l)` by ASM_REWRITE_TAC [eq] THEN 489 ASSUME_TAC eq) THEN 490 `y = q` by IMP_RES_TAC ORL_MEM_FST THEN 491 AR THEN P_PGEN_TAC ``g:'a,h:'b`` THEN 492 Cases_on `(g = x) /\ (h = y)` THENL 493 [METIS_TAC [PAIR_EQ] 494 ,Q.SUBGOAL_THEN `MEM (g,h) l = MEM (g,h) ((x,y)::l)` SUBST1_TAC 495 THEN1 (REWRITE_TAC [MEM, PAIR_EQ] THEN METIS_TAC []) THEN 496 Q.SUBGOAL_THEN `MEM (g,h) m = MEM (g,h) ((p,q)::m)` SUBST1_TAC 497 THEN1 (REWRITE_TAC [MEM, PAIR_EQ] THEN METIS_TAC []) THEN AR 498 ] 499 ,`apto cmp p x = LESS` by IMP_RES_TAC toto_antisym THEN 500 CONV_TAC LEFT_IMP_FORALL_CONV THEN 501 Q.EXISTS_TAC `p,q` THEN 502 `~MEM (p,q) ((x,y)::l)` by (RES_TAC THEN AR) THEN ASM_REWRITE_TAC [MEM] 503 ] 504 ,DISCH_TAC THEN AR 505]]]); 506 507val merge_ASSOC = maybe_thm ("merge_ASSOC", 508``!cmp:'a toto k l m:('a#'b)list. ORL cmp k /\ ORL cmp l /\ ORL cmp m ==> 509 (merge cmp k (merge cmp l m) = merge cmp (merge cmp k l) m)``, 510REPEAT STRIP_TAC THEN 511`ORL cmp (merge cmp l m) /\ ORL cmp (merge cmp k l)` by 512 (CONJ_TAC THEN MATCH_MP_TAC merge_ORL THEN AR) THEN 513Q.SUBGOAL_THEN `ORL cmp (merge cmp k (merge cmp l m)) /\ 514 ORL cmp (merge cmp (merge cmp k l) m)` 515(fn cj => REWRITE_TAC [GSYM (MATCH_MP ORL_MEM_EQ cj)] THEN STRIP_ASSUME_TAC cj) 516THEN1 (CONJ_TAC THEN MATCH_MP_TAC merge_ORL THEN AR) THEN 517P_PGEN_TAC ``x:'a,y:'b`` THEN 518REWRITE_TAC [MATCH_MP merge_MEM_thm (CONJ (Q.ASSUME `ORL cmp k`) 519 (Q.ASSUME `ORL cmp (merge cmp l m)`))] 520 THEN 521REWRITE_TAC [MATCH_MP merge_MEM_thm (CONJ (Q.ASSUME `ORL cmp l`) 522 (Q.ASSUME `ORL cmp m`))] THEN 523REWRITE_TAC [MATCH_MP merge_MEM_thm (CONJ (Q.ASSUME `ORL cmp 524 (merge cmp k l)`) (Q.ASSUME `ORL cmp m`))] THEN 525REWRITE_TAC [MATCH_MP merge_MEM_thm (CONJ (Q.ASSUME `ORL cmp k`) 526 (Q.ASSUME `ORL cmp l`))] THEN 527METIS_TAC []); 528 529(* Now to figure out how to use merge_ASSOC. Idea, I think, is to show 530 that assocv o merge_out is preserved throughout. *) 531 532val OPTION_UPDATE_ASSOC = maybe_thm ("OPTION_UPDATE_ASSOC", 533``!f g h:'a -> 'b option. OPTION_UPDATE f (OPTION_UPDATE g h) = 534 OPTION_UPDATE (OPTION_UPDATE f g) h``, 535REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN 536REWRITE_TAC [OPTION_UPDATE, optry_ASSOC]); 537 538val incr_build = Define`(incr_build cmp [] = []) 539 /\ (incr_build cmp (ab:('a#'b) :: l) = 540 incr_merge cmp [ab] (incr_build cmp l))`; 541 542val incr_build_ORL = maybe_thm ("incr_build_ORL", 543 ``!cmp l:('a#'b)list. ORL_sublists cmp (incr_build cmp l)``, 544GEN_TAC THEN Induct THEN REWRITE_TAC [incr_build] THENL 545[REWRITE_TAC [ORL_sublists] 546,P_PGEN_TAC (Term`a:'a,b:'b`) THEN MATCH_MP_TAC incr_merge_ORL THEN 547 ASM_REWRITE_TAC [ORL, MEM]]); 548 549val merge_out = Define 550 `(merge_out (cmp:'a toto) (l:('a#'b)list) ([]:('a#'b)list option list) = l) 551/\ (merge_out cmp (l:('a#'b)list) (NONE :: lol) = merge_out cmp l lol) 552/\ (merge_out cmp (l:('a#'b)list) ((SOME (m:('a#'b)list)) :: lol) = 553 merge_out cmp (merge cmp l m) lol)`; 554 555val merge_out_ORL = maybe_thm ("merge_out_ORL", 556``!cmp lol:('a#'b)list option list l. ORL cmp l /\ 557 ORL_sublists cmp lol ==> ORL cmp (merge_out cmp l lol)``, 558HO_MATCH_MP_TAC ORL_sublists_ind THEN REPEAT STRIP_TAC THEN 559ASM_REWRITE_TAC [merge_out] THEN 560IMP_RES_TAC ORL_sublists THEN RES_TAC THEN 561SUBGOAL_THEN (Term`ORL cmp (merge cmp l m:('a#'b)list)`) 562 (fn th => ASSUME_TAC th THEN RES_TAC) THEN 563IMP_RES_TAC merge_ORL); 564 565val incr_flat = Define`incr_flat 566 (cmp:'a toto) (lol:('a#'b)list option list) = merge_out cmp [] lol`; 567 568(* by not utilizing incr_flat in incr_sort, we ease writing conversions. *) 569 570val incr_sort = Define`incr_sort (cmp:'a toto) (l:('a#'b)list) = 571 merge_out cmp [] (incr_build cmp l)`; 572 573val incr_sort_ORL = maybe_thm ("incr_sort_ORL", Term 574`!cmp l:('a#'b)list. ORL cmp (incr_sort cmp l)`, 575REPEAT GEN_TAC THEN REWRITE_TAC [incr_sort, incr_flat] THEN 576MATCH_MP_TAC merge_out_ORL THEN 577REWRITE_TAC [ORL, incr_build_ORL]); 578 579(* ************ work up to incr_sort_fun *********** *) 580 581val OPTION_FLAT = Define 582`(OPTION_FLAT ([]:'z list option list) = []) /\ 583 (OPTION_FLAT (NONE:'z list option :: l) = OPTION_FLAT l) /\ 584 (OPTION_FLAT (SOME a :: l) = a ++ OPTION_FLAT l)`; 585 586val OPTION_FLAT_ind = theorem "OPTION_FLAT_ind"; 587 588(* OPTION_FLAT_ind = |- !P. P [] /\ (!l. P l ==> P (NONE::l)) /\ 589 (!a l. P l ==> P (SOME a::l)) ==> !v. P v *) 590 591val assocv_optry_lem = maybe_thm ("assocv_optry_lem", Term 592`!x l:('a#'b)list m. assocv (l ++ m) x = optry (assocv l x) (assocv m x)`, 593GEN_TAC THEN Induct THEN REWRITE_TAC [APPEND, optry_ID, assocv] THEN 594P_PGEN_TAC (Term`p:'a,q:'b`) THEN 595REWRITE_TAC [assocv] THEN Cases_on `x = p` THEN AR THEN REWRITE_TAC [optry]); 596 597val assocv_APPEND = maybe_thm ("assocv_APPEND", 598``!l:('a#'b)list m. assocv (l ++ m) = OPTION_UPDATE (assocv l) (assocv m)``, 599REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN 600REWRITE_TAC [OPTION_UPDATE, assocv_optry_lem]); 601 602val assocv_merge_out = maybe_thm ("assocv_merge_out", 603``!cmp lol:('a#'b)list option list l. ORL cmp l /\ ORL_sublists cmp lol ==> 604 (assocv (merge_out cmp l lol) = assocv (l ++ OPTION_FLAT lol))``, 605GEN_TAC THEN 606HO_MATCH_MP_TAC OPTION_FLAT_ind THEN 607SRW_TAC [] [OPTION_FLAT, merge_out] THENL 608[`ORL_sublists cmp lol` by (ONCE_REWRITE_TAC [GSYM ORL_sublists] THEN AR) THEN 609 RES_TAC 610,`ORL cmp a /\ ORL_sublists cmp lol` by REWRITE_TAC [REWRITE_RULE 611 [ORL_sublists] (Q.ASSUME `ORL_sublists cmp (SOME a ::lol)`)] THEN 612 `ORL cmp (merge cmp l a)` by 613 (MATCH_MP_TAC merge_ORL THEN AR) THEN 614 RES_TAC THEN IMP_RES_TAC merge_fun THEN ASM_REWRITE_TAC [assocv_APPEND] 615]); 616 617val assocv_incr_flat = maybe_thm ("assocv_incr_flat", 618``!cmp lol:('a#'b)list option list. ORL_sublists cmp lol ==> 619 (assocv (incr_flat cmp lol) = assocv (OPTION_FLAT lol))``, 620REPEAT STRIP_TAC THEN `ORL cmp []` by REWRITE_TAC [ORL] THEN 621IMP_RES_TAC assocv_merge_out THEN POP_ASSUM MP_TAC THEN 622REWRITE_TAC [incr_flat, APPEND]); 623 624val assocv_incr_merge = maybe_thm ("assocv_incr_merge", 625``!cmp lol:('a#'b)list option list l m. ORL cmp l /\ ORL cmp m /\ 626 ORL_sublists cmp lol ==> 627 (assocv (merge_out cmp l (incr_merge cmp m lol)) = 628 assocv (merge_out cmp (merge cmp l m) lol))``, 629GEN_TAC THEN Induct THEN SRW_TAC [] 630 [assocv_merge_out, OPTION_FLAT, merge_out, incr_merge, assocv_APPEND] THEN 631Cases_on `h` THEN SRW_TAC [] [incr_merge, merge_out] THEN 632`ORL cmp x /\ ORL_sublists cmp lol` by METIS_TAC [ORL_sublists] THEN 633Q.SUBGOAL_THEN `merge cmp (merge cmp l m) x = merge cmp l (merge cmp m x)` 634SUBST1_TAC THEN1 (MATCH_MP_TAC (GSYM merge_ASSOC) THEN AR) THEN 635`ORL cmp (merge cmp m x)` by (MATCH_MP_TAC merge_ORL THEN AR) THEN 636`ORL_sublists cmp (incr_merge cmp (merge cmp m x) lol)` by 637 (MATCH_MP_TAC incr_merge_ORL THEN AR) THEN 638METIS_TAC [assocv_merge_out]); 639 640val assocv_NIL = maybe_thm ("assocv_NIL", 641``assocv ([]:('a#'b)list) = K NONE``, 642CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] [assocv]); 643 644val OPTION_UPDATE_K_NONE = maybe_thm ("OPTION_UPDATE_K_NONE", 645``!f:'a->'b option. (OPTION_UPDATE f (K NONE) = f) /\ 646 (OPTION_UPDATE (K NONE) f = f)``, 647CONV_TAC (ONCE_DEPTH_CONV FUN_EQ_CONV) THEN 648SRW_TAC [] [OPTION_UPDATE, optry_ID]); 649 650val ORL_SING = maybe_thm ("ORL_SING", 651``!cmp x:('a#'b). ORL cmp [x]``, 652GEN_TAC THEN P_PGEN_TAC ``a:'a,b:'b`` THEN REWRITE_TAC [ORL, MEM]); 653 654val assocv_incr_build = maybe_thm ("assocv_incr_build", 655``!cmp:'a toto m l:('a#'b)list. ORL cmp l ==> 656 (assocv (merge_out cmp l (incr_build cmp m)) = assocv (l ++ m))``, 657GEN_TAC THEN Induct THEN 658SRW_TAC [] [assocv_APPEND, incr_build, merge_out] THENL 659[REWRITE_TAC [OPTION_UPDATE_K_NONE, assocv_NIL, merge_thm] 660,Q.SUBGOAL_THEN 661 `OPTION_UPDATE (assocv l) (assocv (h::m)) = assocv ((l ++ [h]) ++ m)` 662 SUBST1_TAC THENL 663 [Q.SUBGOAL_THEN `h::m = [h] ++ m` SUBST1_TAC THEN1 REWRITE_TAC [APPEND] THEN 664 SRW_TAC [] [assocv_APPEND, OPTION_UPDATE_ASSOC] 665 ,`ORL cmp [h]` by MATCH_ACCEPT_TAC ORL_SING THEN 666 `ORL_sublists cmp (incr_build cmp m)` by MATCH_ACCEPT_TAC incr_build_ORL THEN 667 Q.SUBGOAL_THEN 668 `assocv (merge_out cmp l (incr_merge cmp [h] (incr_build cmp m))) = 669 assocv (merge_out cmp (merge cmp l [h]) (incr_build cmp m))` 670 SUBST1_TAC THEN1 (MATCH_MP_TAC assocv_incr_merge THEN AR) THEN 671 `ORL cmp (merge cmp l [h])` by (MATCH_MP_TAC merge_ORL THEN AR) THEN 672 RES_THEN SUBST1_TAC THEN 673 METIS_TAC [merge_fun, assocv_APPEND] 674]]); 675 676(* at last: incr_sort not only sorts, but it is stable in the sense that 677 the list coming out (with guaranteed only one entry for any key) has the 678 same behavior under assocv as the (possibly duplicitous) list going in. *) 679 680val incr_sort_fun = maybe_thm ("incr_sort_fun", 681``!cmp: 'a toto l:('a#'b)list. assocv (incr_sort cmp l) = assocv l``, 682REPEAT GEN_TAC THEN REWRITE_TAC [incr_sort, incr_flat] THEN 683Q.SUBGOAL_THEN `assocv l = assocv ([] ++ l)` SUBST1_TAC 684THEN1 REWRITE_TAC [APPEND] THEN 685MATCH_MP_TAC assocv_incr_build THEN REWRITE_TAC [ORL]); 686 687(* ********** Relating association lists to finite maps ************ *) 688(* Define "unlookup", sending an option-valued function to an fmap. *) 689(* ***************************************************************** *) 690 691val unlookup = Define`unlookup (f:'a -> 'b option) = 692 FUN_FMAP (THE o f) (IS_SOME o f)`; 693 694(* and prove that unlookup sends OPTION_UPDATE to FUNION *) 695 696(* ********* We require a short interlude relating option-valued ******** *) 697(* ********* and finite functions, via FLOOKUP and unlookup. ******** *) 698 699val FUPDATE_ALT = prove ( 700``!f:'a |-> 'b l. f |++ REVERSE l = FOLDR (combin$C FUPDATE) f l``, 701REPEAT GEN_TAC THEN REWRITE_TAC [FUPDATE_LIST, combinTheory.C_DEF] 702THEN BETA_TAC THEN REWRITE_TAC [rich_listTheory.FOLDL_REVERSE]); 703 704val IS_SOME_FDOM = maybe_thm ("IS_SOME_FDOM", 705``!f:'a |-> 'b. IS_SOME o FLOOKUP f = FDOM f``, 706Induct THEN CONJ_TAC THENL 707[REWRITE_TAC [EXTENSION, FDOM_FEMPTY, NOT_IN_EMPTY] THEN 708 REWRITE_TAC [SPECIFICATION, combinTheory.o_THM, option_CLAUSES, FLOOKUP_EMPTY] 709,GEN_TAC THEN DISCH_THEN (ASSUME_TAC o REWRITE_RULE [combinTheory.o_THM] o 710 CONV_RULE FUN_EQ_CONV) THEN 711 REPEAT STRIP_TAC THEN 712 ASM_REWRITE_TAC [FDOM_FUPDATE, EXTENSION, IN_INSERT] THEN GEN_TAC THEN 713 REWRITE_TAC [SPECIFICATION, combinTheory.o_THM, FLOOKUP_UPDATE] THEN 714 Cases_on `x = x'` THEN ASM_REWRITE_TAC [option_CLAUSES] THEN 715 REWRITE_TAC [GSYM (ASSUME ``x:'a <> x'``)]]); 716 717val FINITE_FLOOKUP = maybe_thm ("FINITE_FLOOKUP", 718``!f:'a |-> 'b. FINITE (IS_SOME o FLOOKUP f)``, 719REWRITE_TAC [IS_SOME_FDOM, FDOM_FINITE]); 720 721val FLOOKUP_unlookup_FDOM = maybe_thm ("FLOOKUP_unlookup_FDOM", 722``!f:'a |-> 'b. FDOM (unlookup (FLOOKUP f)) = FDOM f``, 723REWRITE_TAC [unlookup] THEN ASSUME_TAC (SPEC_ALL FINITE_FLOOKUP) THEN 724IMP_RES_TAC FUN_FMAP_DEF THEN ASM_REWRITE_TAC [IS_SOME_FDOM] THEN 725GEN_TAC THEN ASSUME_TAC (SPEC ``f':'a |-> 'b`` FDOM_FINITE) THEN 726IMP_RES_TAC FUN_FMAP_DEF THEN AR); 727 728val FLOOKUP_unlookup_ID = maybe_thm ("FLOOKUP_unlookup_ID", 729``!f:'a |-> 'b. unlookup (FLOOKUP f) = f``, 730GEN_TAC THEN REWRITE_TAC [fmap_EXT] THEN CONJ_TAC THEN 731REWRITE_TAC [FLOOKUP_unlookup_FDOM] THEN REPEAT STRIP_TAC THEN 732REWRITE_TAC [unlookup] THEN ASSUME_TAC (SPEC_ALL FINITE_FLOOKUP) THEN 733IMP_RES_THEN 734 (STRIP_ASSUME_TAC o REWRITE_RULE [IS_SOME_FDOM]) FUN_FMAP_DEF THEN 735ASM_REWRITE_TAC [IS_SOME_FDOM] THEN RES_TAC THEN 736ASM_REWRITE_TAC [option_CLAUSES, FLOOKUP_DEF, combinTheory.o_THM]); 737 738val unlookup_FLOOKUP_ID = maybe_thm ("unlookup_FLOOKUP_ID",``!g:'a->'b option. 739 FINITE (IS_SOME o g) ==> (FLOOKUP (unlookup g) = g)``, 740GEN_TAC THEN REWRITE_TAC [unlookup] THEN DISCH_TAC THEN 741IMP_RES_TAC (REWRITE_RULE [SPECIFICATION] FUN_FMAP_DEF) THEN 742CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN 743ASM_REWRITE_TAC [FLOOKUP_DEF, SPECIFICATION] THEN 744Cases_on `(IS_SOME o g) x` THEN 745ASM_REWRITE_TAC [option_CLAUSES] THEN REWRITE_TAC [combinTheory.o_THM] THENL 746[RES_TAC THEN AR THEN 747 UNDISCH_TAC ``(IS_SOME o (g:'a->'b option)) x`` THEN 748 ASM_REWRITE_TAC [combinTheory.o_THM, option_CLAUSES] 749,UNDISCH_TAC ``~(IS_SOME o (g:'a->'b option)) x`` THEN 750 ASM_REWRITE_TAC [combinTheory.o_THM, option_CLAUSES] THEN 751 DISCH_THEN SUBST1_TAC THEN REFL_TAC]); 752 753val unlookup_FDOM = maybe_thm ("unlookup_FDOM", ``!g:'a->'b option. 754 FINITE (IS_SOME o g) ==> (FDOM (unlookup g) = IS_SOME o g)``, 755GEN_TAC THEN 756DISCH_THEN (SUBST1_TAC o SYM o MATCH_MP unlookup_FLOOKUP_ID) THEN 757REWRITE_TAC [IS_SOME_FDOM, FLOOKUP_unlookup_ID]); 758 759val unlookup_11 = maybe_thm ("unlookup_11", 760``!f g:'a ->'b option. FINITE (IS_SOME o f) /\ FINITE (IS_SOME o g) ==> 761 (unlookup f = unlookup g) ==> (f = g)``, 762REPEAT STRIP_TAC THEN 763IMP_RES_THEN 764 (PURE_ONCE_REWRITE_TAC o ulist o SYM) unlookup_FLOOKUP_ID THEN AR); 765 766(* ******* end of interlude as described above; still more ********* *) 767(* ******* lemmas to come, adjusting to finite_mapTheory. ********* *) 768 769val unlookup_FUNION = maybe_thm ("unlookup_FUNION", 770``!u (v:'a -> 'b option). FINITE (IS_SOME o u) /\ FINITE (IS_SOME o v) ==> 771 (unlookup u FUNION unlookup v = unlookup (OPTION_UPDATE u v))``, 772REPEAT STRIP_TAC THEN 773SUBGOAL_THEN ``FINITE (IS_SOME o OPTION_UPDATE u (v:'a -> 'b option))`` 774 ASSUME_TAC 775THEN1 ASM_REWRITE_TAC [IS_SOME_OPTION_UPDATE, FINITE_UNION] THEN 776REWRITE_TAC [fmap_EXT] THEN CONJ_TAC THEN 777IMP_RES_TAC unlookup_FDOM THEN 778ASM_REWRITE_TAC [FUNION_DEF, IS_SOME_OPTION_UPDATE, IN_UNION] THEN 779REPEAT STRIP_TAC THEN 780(SUBGOAL_THEN ``x IN (IS_SOME o OPTION_UPDATE (u:'a->'b option) v)`` ASSUME_TAC 781 THEN1 ASM_REWRITE_TAC [IS_SOME_OPTION_UPDATE, IN_UNION]) THEN 782REWRITE_TAC [unlookup] THENL 783[ALL_TAC, Cases_on `x IN IS_SOME o u` THEN AR] THEN 784IMP_RES_TAC FUN_FMAP_DEF THEN 785ASM_REWRITE_TAC [combinTheory.o_THM] THEN 786IMP_RES_TAC (fst (EQ_IMP_RULE (SPEC_ALL SPECIFICATION))) THEN 787ASM_REWRITE_TAC [OPTION_UPDATE, option_CLAUSES, optry] THEN 788AP_TERM_TAC THEN 789IMP_RES_TAC (fst (EQ_IMP_RULE (INST_TYPE [beta |-> ``:bool``] 790 (SPEC_ALL combinTheory.o_THM)))) THEN 791IMP_RES_THEN (REWRITE_TAC o ulist) IS_SOME_optry THEN 792UNDISCH_TAC ``x NOTIN IS_SOME o (u:'a -> 'b option)`` THEN 793REWRITE_TAC [SPECIFICATION, combinTheory.o_THM] THEN 794Cases_on `u x` THEN REWRITE_TAC [optry, option_CLAUSES]); 795 796(* ****** Get back to imitating enumeralTheory with a constant FMAPAL ***** *) 797(* ****** of type ('a#'b)bt -> ('a |-> 'b) (but call the definition ***** *) 798(* ****** bt_to_fmap, like the bt_to_set of enumeralTheory). ***** *) 799 800val bt_to_fmap = xDefine "bt_to_fmap" 801`(FMAPAL (cmp:'a toto) nt = (FEMPTY:'a|->'b)) /\ 802 (FMAPAL (cmp:'a toto) (node l (x:'a,v:'b) r) = 803 DRESTRICT (FMAPAL cmp l) {y | apto cmp y x = LESS} FUNION 804 FEMPTY |+ (x,v) FUNION 805 DRESTRICT (FMAPAL cmp r) {z | apto cmp x z = LESS})`; 806 807val bt_to_fmap_ind = theorem "bt_to_fmap_ind"; 808 809(* bt_to_fmap_ind = |- !P. 810 (!cmp. P cmp nt) /\ 811 (!cmp l x v r. P cmp l /\ P cmp r ==> P cmp (node l (x,v) r)) 812 ==> !v v1. P v v1 *) 813 814(* lemmas to help with FAPPLY_node, various _mut_rec's *) 815 816val FUNION_DRESTRICT = maybe_thm ("FUNION_DRESTRICT", (*cf. DRESTRICT_FUNION*) 817``!f:'a|->'b g s. 818 DRESTRICT (f FUNION g) s = DRESTRICT f s FUNION DRESTRICT g s``, 819REPEAT GEN_TAC THEN REWRITE_TAC [fmap_EXT, FDOM_DRESTRICT, FDOM_FUNION] THEN 820CONJ_TAC THENL 821[ONCE_REWRITE_TAC [INTER_COMM] THEN MATCH_ACCEPT_TAC UNION_OVER_INTER 822,GEN_TAC THEN Cases_on `x IN FDOM f` THEN ASM_REWRITE_TAC [DRESTRICT_DEF] THEN 823 ASM_REWRITE_TAC [IN_UNION, IN_INTER] THEN 824 SRW_TAC [] [FDOM_FUNION, FDOM_DRESTRICT, FUNION_DEF, DRESTRICT_DEF]]); 825 826val DRESTRICT_SING = maybe_thm ("DRESTRICT_SING", 827``!x:'a y:'b s. x IN s ==> (DRESTRICT (FEMPTY |+ (x,y)) s = FEMPTY |+ (x,y))``, 828SRW_TAC [] [DRESTRICT_DEF]); 829 830val DRESTRICT_SING_FEMPTY = maybe_thm ("DRESTRICT_SING_FEMPTY", 831``!x:'a y:'b s. x NOTIN s ==> (DRESTRICT (FEMPTY |+ (x,y)) s = FEMPTY)``, 832SRW_TAC [] [DRESTRICT_DEF]); 833 834val DRESTRICT_IN = maybe_thm ("DRESTRICT_IN", 835``!s x f:'a|->'b. x IN s ==> (DRESTRICT f s ' x = f ' x)``, 836GEN_TAC THEN GEN_TAC THEN Induct THEN 837SRW_TAC [] [DRESTRICT_DEF, IN_INTER, FAPPLY_FUPDATE_THM]); 838 839val DRESTRICT_NOT_IN = maybe_thm ("DRESTRICT_NOT_IN", 840``!s x f:'a|->'b. x NOTIN s ==> (DRESTRICT f s ' x = FEMPTY ' x)``, 841SRW_TAC [] [DRESTRICT_DEF, IN_INTER]); 842 843val IN_FDOM_DRESTRICT_IMP = maybe_thm ("IN_FDOM_DRESTRICT_IMP", 844``!f:'a|->'b s x. x IN FDOM (DRESTRICT f s) ==> x IN s``, 845METIS_TAC [FDOM_DRESTRICT, IN_INTER]); 846 847(* Following two theorems should be used by application conversion. *) 848 849val FAPPLY_nt = store_thm ("FAPPLY_nt", 850``!cmp x. FMAPAL cmp (nt:('a#'b)bt) ' x = FEMPTY ' x``, 851REWRITE_TAC [bt_to_fmap]); 852 853val FAPPLY_node = store_thm ("FAPPLY_node", 854``!cmp x l a:'a b:'b r. FMAPAL cmp (node l (a,b) r) ' x = 855 case apto cmp x a of LESS => FMAPAL cmp l ' x 856 | EQUAL => b 857 | GREATER => FMAPAL cmp r ' x``, 858SRW_TAC [] [bt_to_fmap, FUNION_DEF] THENL 859[Q.SUBGOAL_THEN `x IN {y | apto cmp y a = LESS}` 860 (fn xin => SRW_TAC [] [MATCH_MP DRESTRICT_IN xin, 861 CONV_RULE SET_SPEC_CONV xin]) THEN 862 METIS_TAC [IN_INTER, FDOM_DRESTRICT] 863,`apto cmp a a = LESS` by IMP_RES_THEN 864 (MATCH_ACCEPT_TAC o CONV_RULE SET_SPEC_CONV) IN_FDOM_DRESTRICT_IMP THEN 865 METIS_TAC [toto_refl, all_cpn_distinct] 866,SRW_TAC [] [toto_refl, FAPPLY_FUPDATE_THM] 867,POP_ASSUM (MP_TAC o CONV_RULE (ONCE_DEPTH_CONV SET_SPEC_CONV) o 868 REWRITE_RULE [FDOM_DRESTRICT, IN_INTER]) THEN 869 SRW_TAC [] [] THENL 870 [Cases_on `apto cmp x a` THEN SRW_TAC [] [] THENL 871 [IMP_RES_THEN SUBST1_TAC NOT_FDOM_FAPPLY_FEMPTY THEN 872 Q.SUBGOAL_THEN `x NOTIN {z | apto cmp a z = LESS}` 873 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_NOT_IN) THEN 874 CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN 875 SRW_TAC [] [GSYM toto_antisym] 876 ,METIS_TAC [toto_equal_eq] 877 ,Q.SUBGOAL_THEN `x IN {z | apto cmp a z = LESS}` 878 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_IN) THEN 879 CONV_TAC SET_SPEC_CONV THEN ASM_REWRITE_TAC [GSYM toto_antisym] 880 ] 881 ,Q.SUBGOAL_THEN `x IN {z | apto cmp a z = LESS}` 882 (fn xin => SRW_TAC [] [MATCH_MP DRESTRICT_IN xin, 883 REWRITE_RULE [GSYM toto_antisym] (CONV_RULE SET_SPEC_CONV xin)]) THEN 884 CONV_TAC SET_SPEC_CONV THEN 885 REWRITE_TAC [GSYM toto_antisym] THEN 886 `apto cmp x a <> EQUAL` by ASM_REWRITE_TAC [toto_equal_eq] THEN 887 METIS_TAC [cpn_nchotomy] 888]]); 889 890(* Following theorems prepare for converting bt's to association lists. *) 891 892val bt_to_fmap_lb = Define`bt_to_fmap_lb cmp lb (t:('a#'b)bt) = 893 DRESTRICT (FMAPAL cmp t) {x | apto cmp lb x = LESS}`; 894 895val bt_to_fmap_ub = Define`bt_to_fmap_ub cmp (t:('a#'b)bt) ub = 896 DRESTRICT (FMAPAL cmp t) {x | apto cmp x ub = LESS}`; 897 898val bt_to_fmap_mut_rec = maybe_thm ("bt_to_fmap_mut_rec", 899``!cmp:'a toto l x y r. FMAPAL cmp (node l (x:'a,y:'b) r) = 900 bt_to_fmap_ub cmp l x FUNION FEMPTY |+ (x,y) FUNION bt_to_fmap_lb cmp x r``, 901 REWRITE_TAC [bt_to_fmap_lb, bt_to_fmap_ub, bt_to_fmap]); 902 903val bt_to_fmap_lb_ub = Define`bt_to_fmap_lb_ub cmp lb (t:('a#'b)bt) ub = 904DRESTRICT (FMAPAL cmp t) {x | (apto cmp lb x = LESS) /\ 905 (apto cmp x ub = LESS)}`; 906 907(* ******** Interlude defining bt_map and connecting it with ENUMERAL, FST, 908 FMAPAL, and FDOM. bt_map will be used by o_f_CONV. ****** *) 909 910val bt_map = Define 911`(bt_map (f:'a ->'b) (nt:'a bt) = (nt:'b bt)) /\ 912 (bt_map f (node l x r) = node (bt_map f l) (f x) (bt_map f r))`; 913 914val bt_FST_FDOM = store_thm ("bt_FST_FDOM", 915``!cmp t:('a#'b)bt. FDOM (FMAPAL cmp t) = ENUMERAL cmp (bt_map FST t)``, 916GEN_TAC THEN Induct THENL 917[SRW_TAC [] [bt_to_set, bt_to_fmap, bt_map] 918,P_PGEN_TAC ``x:'a,y:'b`` THEN 919 SRW_TAC [] [bt_to_set, bt_to_fmap, bt_map, FDOM_DRESTRICT] THEN 920 REWRITE_TAC [EXTENSION, IN_INTER, IN_UNION] THEN 921 GEN_TAC THEN CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REFL_TAC]); 922 923val bt_fst_lb_FDOM = maybe_thm ("bt_fst_lb_FDOM", ``!cmp lb t:('a#'b)bt. 924 FDOM (bt_to_fmap_lb cmp lb t) = bt_to_set_lb cmp lb (bt_map FST t)``, 925SRW_TAC [] [bt_to_set_lb, bt_to_fmap_lb, bt_FST_FDOM, FDOM_DRESTRICT] 926THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN 927CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REFL_TAC); 928 929val bt_fst_ub_FDOM = maybe_thm ("bt_fst_ub_FDOM", ``!cmp t:('a#'b)bt ub. 930 FDOM (bt_to_fmap_ub cmp t ub) = bt_to_set_ub cmp (bt_map FST t) ub``, 931SRW_TAC [] [bt_to_set_ub, bt_to_fmap_ub, bt_FST_FDOM, FDOM_DRESTRICT] 932THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN 933CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REFL_TAC); 934 935val bt_fst_lb_ub_FDOM = maybe_thm ("bt_fst_lb_ub_FDOM", 936``!cmp lb t:('a#'b)bt ub. FDOM (bt_to_fmap_lb_ub cmp lb t ub) = 937 bt_to_set_lb_ub cmp lb (bt_map FST t) ub``, 938SRW_TAC [] 939 [bt_to_set_lb_ub, bt_to_fmap_lb_ub, bt_FST_FDOM, FDOM_DRESTRICT] 940THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN 941CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REFL_TAC); 942 943val IN_lb_ub_imp = maybe_thm ("IN_lb_ub_imp", 944``!cmp x lb t:'a bt ub. x IN bt_to_set_lb_ub cmp lb t ub ==> 945 (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)``, 946SRW_TAC [] [bt_to_set_lb_ub]); 947 948val IN_lb_imp = maybe_thm ("IN_lb_imp", 949``!cmp x lb t:'a bt. x IN bt_to_set_lb cmp lb t ==> (apto cmp lb x = LESS)``, 950SRW_TAC [] [bt_to_set_lb]); 951 952val IN_ub_imp = maybe_thm ("IN_ub_imp", 953``!cmp x t:'a bt ub. x IN bt_to_set_ub cmp t ub ==> (apto cmp x ub = LESS)``, 954SRW_TAC [] [bt_to_set_ub]); 955 956val piecewise_FUNION = prove ( 957``!a b c x y z:'a|->'b.(a=x)/\(b=y)/\(c=z)==> 958 (a FUNION b FUNION c = x FUNION y FUNION z)``, 959METIS_TAC []); 960 961val bt_to_fmap_lb_ub_mut_rec = maybe_thm ("bt_to_fmap_lb_ub_mut_rec", 962``!cmp lb l x:'a y:'b r ub. bt_to_fmap_lb_ub cmp lb (node l (x,y) r) ub = 963 if apto cmp lb x = LESS then 964 if apto cmp x ub = LESS then 965 bt_to_fmap_lb_ub cmp lb l x FUNION FEMPTY |+ (x,y) FUNION 966 bt_to_fmap_lb_ub cmp x r ub 967 else 968 bt_to_fmap_lb_ub cmp lb l ub 969 else 970 bt_to_fmap_lb_ub cmp lb r ub``, 971SRW_TAC [] [fmap_EXT, bt_fst_lb_ub_FDOM] THEN 972SRW_TAC [] [bt_to_fmap_lb_ub, bt_to_set_lb_ub, bt_map] THENL 973[REWRITE_TAC [EXTENSION, IN_UNION, bt_to_set] THEN GEN_TAC THEN 974 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN 975 METIS_TAC [totoLLtrans, IN_SING] 976,IMP_RES_TAC IN_lb_ub_imp THEN 977 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN 978 AP_THM_TAC THEN AP_TERM_TAC THEN 979 MATCH_MP_TAC piecewise_FUNION THEN 980 REPEAT CONJ_TAC THENL 981 [AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN 982 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 983 ,MATCH_MP_TAC DRESTRICT_SING THEN 984 CONV_TAC SET_SPEC_CONV THEN AR 985 ,AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN 986 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 987 ] 988,REWRITE_TAC [bt_to_set, EXTENSION, IN_UNION] THEN GEN_TAC THEN 989 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN EQ_TAC THEN STRIP_TAC THEN AR THEN 990 METIS_TAC [totoLLtrans, IN_SING, NOT_EQ_LESS_IMP] 991,IMP_RES_TAC IN_lb_ub_imp THEN 992 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN 993 Q.SUBGOAL_THEN `({z | apto cmp x z = LESS} INTER 994 {x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}) = {}` SUBST1_TAC THENL 995 [REWRITE_TAC [EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN GEN_TAC THEN 996 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 997 ,Q.SUBGOAL_THEN 998 `x NOTIN {x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}` 999 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_SING_FEMPTY) THENL 1000 [CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1001 ,REWRITE_TAC [DRESTRICT_IS_FEMPTY, FUNION_FEMPTY_2] THEN 1002 Q.SUBGOAL_THEN `{x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)} 1003 SUBSET {y | apto cmp y x = LESS}` 1004 (SUBST1_TAC o REWRITE_RULE [SYM (CONJUNCT2 INTER_SUBSET_EQN)]) THENL 1005 [REWRITE_TAC [SUBSET_DEF] THEN GEN_TAC THEN 1006 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 1007 METIS_TAC [totoLLtrans, NOT_EQ_LESS_IMP] 1008 ,REFL_TAC 1009 ]]] 1010,REWRITE_TAC [bt_to_set, EXTENSION, IN_UNION] THEN GEN_TAC THEN 1011 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN EQ_TAC THEN STRIP_TAC THEN AR THEN 1012 METIS_TAC [totoLLtrans, IN_SING, NOT_EQ_LESS_IMP] 1013,IMP_RES_TAC IN_lb_ub_imp THEN 1014 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN 1015 Q.SUBGOAL_THEN `({y | apto cmp y x = LESS} INTER 1016 {x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}) = {}` SUBST1_TAC THENL 1017 [REWRITE_TAC [EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN GEN_TAC THEN 1018 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1019 ,Q.SUBGOAL_THEN 1020 `x NOTIN {x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}` 1021 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_SING_FEMPTY) THENL 1022 [CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1023 ,REWRITE_TAC [DRESTRICT_IS_FEMPTY, FUNION_FEMPTY_1] THEN 1024 Q.SUBGOAL_THEN `{x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)} 1025 SUBSET {z | apto cmp x z = LESS}` 1026 (SUBST1_TAC o REWRITE_RULE [SYM (CONJUNCT2 INTER_SUBSET_EQN)]) THENL 1027 [REWRITE_TAC [SUBSET_DEF] THEN GEN_TAC THEN 1028 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 1029 METIS_TAC [totoLLtrans, NOT_EQ_LESS_IMP] 1030 ,REFL_TAC 1031 ]]] 1032]); 1033 1034val bt_to_fmap_lb_mut_rec = maybe_thm ("bt_to_fmap_lb_mut_rec", 1035``!cmp lb l x:'a y:'b r. bt_to_fmap_lb cmp lb (node l (x,y) r) = 1036 if apto cmp lb x = LESS then 1037 bt_to_fmap_lb_ub cmp lb l x FUNION FEMPTY |+ (x,y) FUNION 1038 bt_to_fmap_lb cmp x r 1039 else 1040 bt_to_fmap_lb cmp lb r``, 1041SRW_TAC [] [fmap_EXT, bt_fst_lb_ub_FDOM, bt_fst_lb_FDOM] THEN 1042SRW_TAC [] [bt_to_fmap_lb_ub, bt_to_set_lb_ub, bt_map, 1043 bt_to_fmap_lb, bt_to_set_lb] THENL 1044[REWRITE_TAC [EXTENSION, IN_UNION, bt_to_set] THEN GEN_TAC THEN 1045 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN 1046 METIS_TAC [totoLLtrans, IN_SING] 1047,IMP_RES_TAC IN_lb_imp THEN 1048 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN 1049 AP_THM_TAC THEN AP_TERM_TAC THEN 1050 MATCH_MP_TAC piecewise_FUNION THEN 1051 REPEAT CONJ_TAC THENL 1052 [AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN 1053 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1054 ,MATCH_MP_TAC DRESTRICT_SING THEN 1055 CONV_TAC SET_SPEC_CONV THEN AR 1056 ,AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN 1057 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1058 ] 1059,REWRITE_TAC [bt_to_set, EXTENSION, IN_UNION] THEN GEN_TAC THEN 1060 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN EQ_TAC THEN STRIP_TAC THEN AR THEN 1061 METIS_TAC [totoLLtrans, IN_SING, NOT_EQ_LESS_IMP] 1062,IMP_RES_TAC IN_lb_imp THEN 1063 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN 1064 Q.SUBGOAL_THEN `({y | apto cmp y x = LESS} INTER 1065 {x | (apto cmp lb x = LESS)}) = {}` SUBST1_TAC THENL 1066 [REWRITE_TAC [EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN GEN_TAC THEN 1067 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1068 ,Q.SUBGOAL_THEN 1069 `x NOTIN {x | (apto cmp lb x = LESS)}` 1070 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_SING_FEMPTY) THENL 1071 [CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1072 ,REWRITE_TAC [DRESTRICT_IS_FEMPTY, FUNION_FEMPTY_1] THEN 1073 Q.SUBGOAL_THEN `{x | (apto cmp lb x = LESS)} 1074 SUBSET {z | apto cmp x z = LESS}` 1075 (SUBST1_TAC o REWRITE_RULE [SYM (CONJUNCT2 INTER_SUBSET_EQN)]) THENL 1076 [REWRITE_TAC [SUBSET_DEF] THEN GEN_TAC THEN 1077 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 1078 METIS_TAC [totoLLtrans, NOT_EQ_LESS_IMP] 1079 ,REFL_TAC 1080 ]]] 1081]); 1082 1083val bt_to_fmap_ub_mut_rec = maybe_thm ("bt_to_fmap_ub_mut_rec", 1084``!cmp l x:'a y:'b r ub. bt_to_fmap_ub cmp (node l (x,y) r) ub = 1085 if apto cmp x ub = LESS then 1086 bt_to_fmap_ub cmp l x FUNION FEMPTY |+ (x,y) FUNION 1087 bt_to_fmap_lb_ub cmp x r ub 1088 else 1089 bt_to_fmap_ub cmp l ub``, 1090SRW_TAC [] [fmap_EXT, bt_fst_lb_ub_FDOM, bt_fst_ub_FDOM] THEN 1091SRW_TAC [] [bt_to_fmap_lb_ub, bt_to_set_lb_ub, bt_map, 1092 bt_to_fmap_ub, bt_to_set_ub] THENL 1093[REWRITE_TAC [EXTENSION, IN_UNION, bt_to_set] THEN GEN_TAC THEN 1094 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN 1095 METIS_TAC [totoLLtrans, IN_SING] 1096,IMP_RES_TAC IN_ub_imp THEN 1097 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN 1098 AP_THM_TAC THEN AP_TERM_TAC THEN 1099 MATCH_MP_TAC piecewise_FUNION THEN 1100 REPEAT CONJ_TAC THENL 1101 [AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN 1102 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1103 ,MATCH_MP_TAC DRESTRICT_SING THEN 1104 CONV_TAC SET_SPEC_CONV THEN AR 1105 ,AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN 1106 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1107 ] 1108,REWRITE_TAC [bt_to_set, EXTENSION, IN_UNION] THEN GEN_TAC THEN 1109 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN EQ_TAC THEN STRIP_TAC THEN AR THEN 1110 METIS_TAC [totoLLtrans, IN_SING, NOT_EQ_LESS_IMP] 1111,IMP_RES_TAC IN_ub_imp THEN 1112 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN 1113 Q.SUBGOAL_THEN `{z | apto cmp x z = LESS} INTER {x | apto cmp x ub = LESS} 1114 = {}` SUBST1_TAC THENL 1115 [REWRITE_TAC [EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN GEN_TAC THEN 1116 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1117 ,Q.SUBGOAL_THEN 1118 `x NOTIN {x | (apto cmp x ub = LESS)}` 1119 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_SING_FEMPTY) THENL 1120 [CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans] 1121 ,REWRITE_TAC [DRESTRICT_IS_FEMPTY, FUNION_FEMPTY_2] THEN 1122 Q.SUBGOAL_THEN `{x | (apto cmp x ub = LESS)} 1123 SUBSET {y | apto cmp y x = LESS}` 1124 (SUBST1_TAC o REWRITE_RULE [SYM (CONJUNCT2 INTER_SUBSET_EQN)]) THENL 1125 [REWRITE_TAC [SUBSET_DEF] THEN GEN_TAC THEN 1126 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN 1127 METIS_TAC [totoLLtrans, NOT_EQ_LESS_IMP] 1128 ,REFL_TAC 1129 ]]] 1130]); 1131 1132(* ******************************************************************* *) 1133(* Continue to imitate enumeralTheory with conversion to ordered lists *) 1134(* As with sets, we supply a general translation, good for any junky *) 1135(* tree. As far as can be foreseen, only the better_bt_to_orl, which *) 1136(* checks by ORL_bt that the tree is ordered and then uses bt_to_list, *) 1137(* will be needed in practice. *) 1138(* ******************************************************************* *) 1139 1140val bt_to_orl_lb_ub = Define 1141`(bt_to_orl_lb_ub (cmp:'a toto) lb nt ub = []) /\ 1142 (bt_to_orl_lb_ub cmp lb (node l (x:'a,y:'b) r) ub = 1143 if apto cmp lb x = LESS then 1144 if apto cmp x ub = LESS then 1145 bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++ bt_to_orl_lb_ub cmp x r ub 1146 else bt_to_orl_lb_ub cmp lb l ub 1147 else bt_to_orl_lb_ub cmp lb r ub)`; 1148 1149val bt_to_orl_lb = Define 1150`(bt_to_orl_lb (cmp:'a toto) lb nt = []) /\ 1151 (bt_to_orl_lb cmp lb (node l (x:'a,y:'b) r) = 1152 if apto cmp lb x = LESS then 1153 bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++ bt_to_orl_lb cmp x r 1154 else bt_to_orl_lb cmp lb r)`; 1155 1156val bt_to_orl_ub = Define 1157`(bt_to_orl_ub (cmp:'a toto) nt ub = []) /\ 1158 (bt_to_orl_ub cmp (node l (x:'a,y:'b) r) ub = 1159 if apto cmp x ub = LESS then 1160 bt_to_orl_ub cmp l x ++ [(x,y)] ++ bt_to_orl_lb_ub cmp x r ub 1161 else bt_to_orl_ub cmp l ub)`; 1162 1163val bt_to_orl = Define 1164`(bt_to_orl (cmp:'a toto) nt = []) /\ 1165 (bt_to_orl cmp (node l (x:'a,y:'b) r) = 1166 bt_to_orl_ub cmp l x ++ [(x,y)] ++ bt_to_orl_lb cmp x r)`; 1167 1168(* Analogous to "set" as a constant denoting conversion from 'a list to 1169 'a set, we use "fmap" for conversion from association list to ('a,'b)fmap. *) 1170 1171val fmap = Define 1172`fmap (l:('a#'b)list) = FEMPTY |++ REVERSE l`; 1173 1174val FUPDATE_LIST_FUNION = maybe_thm ("FUPDATE_LIST_FUNION", 1175``!f l:('a#'b)list g. g |++ l FUNION f = (g FUNION f) |++ l``, 1176GEN_TAC THEN Induct THENL 1177[REWRITE_TAC [FUPDATE_LIST_THM] 1178,P_PGEN_TAC ``x:'a,y:'b`` THEN 1179 SRW_TAC [] [FUPDATE_LIST_THM, FUNION_FUPDATE_1] 1180]); 1181 1182val fmap_rec = maybe_thm ("fmap_rec", 1183``(fmap ([]:('a#'b)list) = FEMPTY) /\ 1184 (!h:'a#'b l. fmap (h::l) = fmap l |+ h)``, 1185CONJ_TAC THEN REWRITE_TAC [fmap, REVERSE_DEF, FUPDATE_LIST_THM] THEN 1186REWRITE_TAC [FUPDATE_LIST_APPEND, FUPDATE_LIST_THM]); 1187 1188val fmap_NIL = maybe_thm ("fmap_NIL", 1189``fmap ([]:('a#'b)list) = FEMPTY``, 1190REWRITE_TAC [fmap_rec]); 1191 1192val fmap_UNIT = maybe_thm ("fmap_UNIT", 1193``!h:'a#'b. fmap [h] = FEMPTY |+ h``, 1194REWRITE_TAC [fmap_rec]); 1195 1196val fmap_APPEND = maybe_thm ("fmap_APPEND", 1197``!m n:('a#'b)list. fmap (m ++ n) = fmap m FUNION fmap n``, 1198SRW_TAC [] [fmap, FUPDATE_LIST_APPEND, REVERSE_APPEND] THEN 1199REWRITE_TAC [FUPDATE_LIST_FUNION, FUNION_FEMPTY_1]); 1200 1201(* Show ordered lists represent the right finite maps. *) 1202 1203val orl_fmap_lb_ub = maybe_thm ("orl_fmap_lb_ub",``!cmp t:('a#'b)bt lb ub. 1204 bt_to_fmap_lb_ub cmp lb t ub = fmap (bt_to_orl_lb_ub cmp lb t ub)``, 1205GEN_TAC THEN Induct THENL 1206[SRW_TAC [] [bt_to_orl_lb_ub, fmap_NIL, bt_to_fmap_lb_ub, 1207 bt_to_fmap, DRESTRICT_FEMPTY] 1208,P_PGEN_TAC ``x:'a,y:'b`` THEN 1209 SRW_TAC [] [bt_to_fmap_lb_ub_mut_rec, bt_to_orl_lb_ub, 1210 fmap_APPEND, fmap_UNIT] 1211]); 1212 1213val orl_fmap_lb = maybe_thm ("orl_fmap_lb",``!cmp t:('a#'b)bt lb. 1214 bt_to_fmap_lb cmp lb t = fmap (bt_to_orl_lb cmp lb t)``, 1215GEN_TAC THEN Induct THENL 1216[SRW_TAC [] [bt_to_orl_lb, fmap_NIL, bt_to_fmap_lb, 1217 bt_to_fmap, DRESTRICT_FEMPTY] 1218,P_PGEN_TAC ``x:'a,y:'b`` THEN 1219 SRW_TAC [] [bt_to_fmap_lb_mut_rec, bt_to_orl_lb, 1220 fmap_APPEND, fmap_UNIT, orl_fmap_lb_ub] 1221]); 1222 1223val orl_fmap_ub = maybe_thm ("orl_fmap_ub",``!cmp t:('a#'b)bt ub. 1224 bt_to_fmap_ub cmp t ub = fmap (bt_to_orl_ub cmp t ub)``, 1225GEN_TAC THEN Induct THENL 1226[SRW_TAC [] [bt_to_orl_ub, fmap_NIL, bt_to_fmap_ub, 1227 bt_to_fmap, DRESTRICT_FEMPTY] 1228,P_PGEN_TAC ``x:'a,y:'b`` THEN 1229 SRW_TAC [] [bt_to_fmap_ub_mut_rec, bt_to_orl_ub, 1230 fmap_APPEND, fmap_UNIT, orl_fmap_lb_ub] 1231]); 1232 1233val orl_fmap = maybe_thm ("orl_fmap", 1234``!cmp t:('a#'b)bt. FMAPAL cmp t = fmap (bt_to_orl cmp t)``, 1235GEN_TAC THEN Induct THENL 1236[SRW_TAC [] [bt_to_orl, fmap_NIL, bt_to_fmap, 1237 bt_to_fmap, DRESTRICT_FEMPTY] 1238,P_PGEN_TAC ``x:'a,y:'b`` THEN 1239 SRW_TAC [] [bt_to_fmap_mut_rec, bt_to_orl, fmap_APPEND, 1240 fmap_UNIT, orl_fmap_lb, orl_fmap_ub] 1241]); 1242 1243(* But we must prove that results from bt_to_orl etc. satisfy ORL cmp. *) 1244 1245val MEM_MAP_FST_LEM = maybe_thm ("MEM_MAP_FST_LEM", 1246``!x l:('a#'b)list. MEM x (MAP FST l) <=> ?y. (MEM (x,y) l)``, 1247GEN_TAC THEN Induct THEN REWRITE_TAC [MAP, MEM] THEN 1248P_PGEN_TAC ``a:'a,b:'b`` THEN REWRITE_TAC [PAIR_EQ] THEN 1249EQ_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN AR THENL 1250[Q.EXISTS_TAC `b` THEN REWRITE_TAC [] 1251,RES_TAC THEN Q.EXISTS_TAC `y` THEN AR 1252,DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN AR 1253]); 1254 1255val ORL_ALT = maybe_thm ("ORL_ALT", 1256``(!cmp. ORL cmp ([]:('a#'b)list) = T) /\ 1257 (!cmp b a l. ORL cmp ((a:'a,b:'b)::l) <=> ORL cmp l /\ 1258 !p. MEM p (MAP FST l) ==> (apto cmp a p = LESS))``, 1259REWRITE_TAC [ORL, MEM_MAP_FST_LEM] THEN 1260CONV_TAC (ONCE_DEPTH_CONV LEFT_IMP_EXISTS_CONV) THEN 1261REPEAT GEN_TAC THEN REFL_TAC); 1262 1263val ORL_split_lem = maybe_thm ("ORL_split_lem", 1264``!cmp l x:'a y:'b r. ORL cmp (l ++ [(x,y)] ++ r) <=> 1265 ORL cmp l /\ (!a. a IN set (MAP FST l) ==> (apto cmp a x = LESS)) /\ 1266 ORL cmp r /\ (!z. z IN set (MAP FST r) ==> (apto cmp x z = LESS))``, 1267GEN_TAC THEN Induct THENL 1268[SRW_TAC [] [ORL_ALT] 1269,P_PGEN_TAC ``p:'a,q:'b`` THEN SRW_TAC [] [ORL_ALT] THEN EQ_TAC THEN 1270 SRW_TAC [] [] THENL 1271 [POP_ASSUM MATCH_MP_TAC THEN REWRITE_TAC [] 1272 ,RES_TAC 1273 ,RES_TAC 1274 ,Q.UNDISCH_THEN `!a. (a = p) \/ MEM a (MAP FST l) ==> (apto cmp a p' = LESS)` 1275 MATCH_MP_TAC THEN REWRITE_TAC [] 1276 ,MATCH_MP_TAC totoLLtrans THEN Q.EXISTS_TAC `x` THEN CONJ_TAC THENL 1277 [Q.UNDISCH_THEN `!a. (a = p) \/ MEM a (MAP FST l) ==> (apto cmp a x = LESS)` 1278 MATCH_MP_TAC THEN REWRITE_TAC [] 1279 ,RES_TAC 1280]]]); 1281 1282val bt_orl_ol_lb_ub = maybe_thm ("bt_orl_ol_lb_ub", 1283``!cmp t:('a#'b)bt lb ub. MAP FST (bt_to_orl_lb_ub cmp lb t ub) = 1284 bt_to_ol_lb_ub cmp lb (bt_map FST t) ub``, 1285GEN_TAC THEN Induct THENL 1286[REWRITE_TAC [bt_to_ol_lb_ub, bt_to_orl_lb_ub, bt_map, MAP] 1287,P_PGEN_TAC ``x:'a,y:'b`` THEN 1288 RW_TAC (srw_ss()) [bt_to_ol_lb_ub, bt_to_orl_lb_ub, bt_map, MAP] 1289]); 1290 1291val ORL_bt_to_orl_lb_ub = maybe_thm ("ORL_bt_to_orl_lb_ub", 1292``!cmp t:('a#'b)bt lb ub. ORL cmp (bt_to_orl_lb_ub cmp lb t ub)``, 1293REWRITE_TAC [ORL_OL_FST, bt_orl_ol_lb_ub, OL_bt_to_ol_lb_ub]); 1294 1295val bt_orl_ol_lb = maybe_thm ("bt_orl_ol_lb", 1296``!cmp t:('a#'b)bt lb. MAP FST (bt_to_orl_lb cmp lb t) = 1297 bt_to_ol_lb cmp lb (bt_map FST t)``, 1298GEN_TAC THEN Induct THENL 1299[REWRITE_TAC [bt_to_ol_lb, bt_to_orl_lb, bt_map, MAP] 1300,P_PGEN_TAC ``x:'a,y:'b`` THEN RW_TAC (srw_ss()) 1301 [bt_to_ol_lb, bt_to_orl_lb, bt_orl_ol_lb_ub, bt_map, MAP] 1302]); 1303 1304val ORL_bt_to_orl_lb = maybe_thm ("ORL_bt_to_orl_lb", 1305``!cmp t:('a#'b)bt lb. ORL cmp (bt_to_orl_lb cmp lb t)``, 1306REWRITE_TAC [ORL_OL_FST, bt_orl_ol_lb, OL_bt_to_ol_lb]); 1307 1308val bt_orl_ol_ub = maybe_thm ("bt_orl_ol_ub", 1309``!cmp t:('a#'b)bt ub. MAP FST (bt_to_orl_ub cmp t ub) = 1310 bt_to_ol_ub cmp (bt_map FST t) ub``, 1311GEN_TAC THEN Induct THENL 1312[REWRITE_TAC [bt_to_ol_ub, bt_to_orl_ub, bt_map, MAP] 1313,P_PGEN_TAC ``x:'a,y:'b`` THEN RW_TAC (srw_ss()) 1314 [bt_to_ol_ub, bt_to_orl_ub, bt_orl_ol_lb_ub, bt_map, MAP] 1315]); 1316 1317val ORL_bt_to_orl_ub = maybe_thm ("ORL_bt_to_orl_ub", 1318``!cmp t:('a#'b)bt ub. ORL cmp (bt_to_orl_ub cmp t ub)``, 1319REWRITE_TAC [ORL_OL_FST, bt_orl_ol_ub, OL_bt_to_ol_ub]); 1320 1321val bt_orl_ol = maybe_thm ("bt_orl_ol", 1322``!cmp t:('a#'b)bt. MAP FST (bt_to_orl cmp t) = 1323 bt_to_ol cmp (bt_map FST t)``, 1324GEN_TAC THEN Induct THENL 1325[REWRITE_TAC [bt_to_ol, bt_to_orl, bt_map, MAP] 1326,P_PGEN_TAC ``x:'a,y:'b`` THEN RW_TAC (srw_ss()) 1327 [bt_to_ol, bt_to_orl, bt_orl_ol_lb, bt_orl_ol_ub, bt_map, MAP] 1328]); 1329 1330val ORL_bt_to_orl = maybe_thm ("ORL_bt_to_orl", 1331``!cmp t:('a#'b)bt. ORL cmp (bt_to_orl cmp t)``, 1332REWRITE_TAC [ORL_OL_FST, bt_orl_ol, OL_bt_to_ol]); 1333 1334(* Now, still imitating enumeralTheory, to remove the APPENDs. *) 1335 1336val bt_to_orl_lb_ub_ac = Define 1337`(bt_to_orl_lb_ub_ac cmp lb (nt:('a#'b)bt) ub m = m) /\ 1338 (bt_to_orl_lb_ub_ac cmp lb (node l (x:'a,y:'b) r) ub m = 1339 if apto cmp lb x = LESS then 1340 if apto cmp x ub = LESS then 1341 bt_to_orl_lb_ub_ac cmp lb l x ((x,y) :: bt_to_orl_lb_ub_ac cmp x r ub m) 1342 else bt_to_orl_lb_ub_ac cmp lb l ub m 1343 else bt_to_orl_lb_ub_ac cmp lb r ub m)`; 1344 1345val orl_lb_ub_ac_thm = maybe_thm ("orl_lb_ub_ac_thm", 1346``!cmp t:('a#'b)bt lb ub m. bt_to_orl_lb_ub_ac cmp lb t ub m = 1347 bt_to_orl_lb_ub cmp lb t ub ++ m``, 1348GEN_TAC THEN Induct THENL 1349[SRW_TAC [][bt_to_orl_lb_ub, bt_to_orl_lb_ub_ac] 1350,P_PGEN_TAC ``x:'a,y:'b`` THEN 1351 SRW_TAC [][bt_to_orl_lb_ub, bt_to_orl_lb_ub_ac] 1352]); 1353 1354val bt_to_orl_lb_ac = Define 1355`(bt_to_orl_lb_ac cmp lb (nt:('a#'b)bt) m = m) /\ 1356 (bt_to_orl_lb_ac cmp lb (node l (x:'a,y:'b) r) m = 1357 if apto cmp lb x = LESS then 1358 bt_to_orl_lb_ub_ac cmp lb l x ((x,y) :: bt_to_orl_lb_ac cmp x r m) 1359 else bt_to_orl_lb_ac cmp lb r m)`; 1360 1361val orl_lb_ac_thm = maybe_thm ("orl_lb_ac_thm", 1362``!cmp t:('a#'b)bt lb m. bt_to_orl_lb_ac cmp lb t m = 1363 bt_to_orl_lb cmp lb t ++ m``, 1364GEN_TAC THEN Induct THENL 1365[SRW_TAC [][bt_to_orl_lb, bt_to_orl_lb_ac] 1366,P_PGEN_TAC ``x:'a,y:'b`` THEN 1367 SRW_TAC [][bt_to_orl_lb, bt_to_orl_lb_ac, orl_lb_ub_ac_thm] 1368]); 1369 1370val bt_to_orl_ub_ac = Define 1371`(bt_to_orl_ub_ac cmp (nt:('a#'b)bt) ub m = m) /\ 1372 (bt_to_orl_ub_ac cmp (node l (x:'a,y:'b) r) ub m = 1373 if apto cmp x ub = LESS then 1374 bt_to_orl_ub_ac cmp l x ((x,y) :: bt_to_orl_lb_ub_ac cmp x r ub m) 1375 else bt_to_orl_ub_ac cmp l ub m)`; 1376 1377val orl_ub_ac_thm = maybe_thm ("orl_ub_ac_thm", 1378``!cmp t:('a#'b)bt ub m. bt_to_orl_ub_ac cmp t ub m = 1379 bt_to_orl_ub cmp t ub ++ m``, 1380GEN_TAC THEN Induct THENL 1381[SRW_TAC [][bt_to_orl_ub, bt_to_orl_ub_ac] 1382,P_PGEN_TAC ``x:'a,y:'b`` THEN 1383 SRW_TAC [][bt_to_orl_ub, bt_to_orl_ub_ac, orl_lb_ub_ac_thm] 1384]); 1385 1386val bt_to_orl_ac = Define 1387`(bt_to_orl_ac cmp (nt:('a#'b)bt) m = m) /\ 1388 (bt_to_orl_ac cmp (node l (x:'a,y:'b) r) m = 1389 bt_to_orl_ub_ac cmp l x ((x,y) :: bt_to_orl_lb_ac cmp x r m))`; 1390 1391val orl_ac_thm = maybe_thm ("orl_ac_thm", 1392``!cmp t:('a#'b)bt m. bt_to_orl_ac cmp t m = bt_to_orl cmp t ++ m``, 1393GEN_TAC THEN Induct THENL 1394[SRW_TAC [][bt_to_orl, bt_to_orl_ac] 1395,P_PGEN_TAC ``x:'a,y:'b`` THEN 1396 SRW_TAC [][bt_to_orl, bt_to_orl_ac, orl_lb_ac_thm, orl_ub_ac_thm] 1397]); 1398 1399(* ********* "ORWL" for (fmap) ORdered With List ************ *) 1400 1401val ORWL = Define `ORWL cmp (f:'a|->'b) l = (f = fmap l) /\ ORL cmp l`; 1402 1403val MEM_IN_DOM_fmap = maybe_thm ("MEM_IN_DOM_fmap", 1404``!cmp l:('a#'b)list. ORL cmp l ==> (!a b. MEM (a,b) l <=> 1405 a IN FDOM (fmap l) /\ (b = fmap l ' a))``, 1406GEN_TAC THEN Induct THENL 1407[REWRITE_TAC [FDOM_FEMPTY, fmap_rec, NOT_IN_EMPTY, MEM] 1408,P_PGEN_TAC ``x:'a,y:'b`` THEN 1409 DISCH_THEN (fn orlc => 1410 STRIP_ASSUME_TAC (MATCH_MP (CONJUNCT1 ORL_NOT_MEM) orlc) THEN 1411 STRIP_ASSUME_TAC (REWRITE_RULE [ORL] orlc)) THEN 1412 SRW_TAC [] [fmap_rec, FAPPLY_FUPDATE_THM, FDOM_FUPDATE] THEN 1413 METIS_TAC [] 1414]); 1415 1416val ORWL_unique = maybe_thm ("ORWL_unique", 1417``!cmp f:'a|->'b l m. ORWL cmp f l /\ ORWL cmp f m ==> (l = m)``, 1418RW_TAC bool_ss [ORWL] THEN 1419Q.SUBGOAL_THEN `ORL cmp l /\ ORL cmp m` 1420 (SUBST1_TAC o SYM o MATCH_MP ORL_MEM_EQ) THEN1 AR THEN 1421P_PGEN_TAC ``a:'a,b:'b`` THEN METIS_TAC [MEM_IN_DOM_fmap]); 1422 1423val assocv_fmap_thm = maybe_thm ("assocv_fmap_thm", 1424``!l:('a#'b)list. assocv l = FLOOKUP (fmap l)``, 1425Induct THEN CONV_TAC (ONCE_DEPTH_CONV FUN_EQ_CONV) THENL 1426[RW_TAC (srw_ss()) [assocv, FLOOKUP_DEF, fmap_rec, FDOM_FEMPTY] 1427,P_PGEN_TAC ``a:'a,b:'b`` THEN 1428 SRW_TAC [] [assocv, FLOOKUP_DEF, fmap_rec] THENL 1429 [METIS_TAC [] 1430 ,METIS_TAC [FAPPLY_FUPDATE_THM] 1431 ,METIS_TAC [] 1432]]); 1433 1434val fmap_ALT = maybe_thm ("fmap_ALT", 1435``!l:('a#'b)list. fmap l = unlookup (assocv l)``, 1436SRW_TAC [] [assocv_fmap_thm, FLOOKUP_unlookup_ID]); 1437 1438val incr_sort_fmap = maybe_thm ("incr_sort_fmap", 1439``!cmp l:('a#'b)list. fmap (incr_sort cmp l) = fmap l``, 1440REWRITE_TAC [fmap_ALT, incr_sort_fun]); 1441 1442val ORWL_bt_to_orl = store_thm ("ORWL_bt_to_orl", 1443``!cmp t:('a#'b)bt. ORWL cmp (FMAPAL cmp t) (bt_to_orl cmp t)``, 1444RW_TAC bool_ss [ORWL, orl_fmap, ORL_bt_to_orl]); 1445 1446(* We already have the two separate pieces of the above: 1447 ORL_bt_to_orl = |- !cmp t. ORL cmp (bt_to_orl cmp t) 1448 orl_fmap = |- !cmp t. FMAPAL cmp t = fmap (bt_to_orl cmp t) *) 1449 1450val IS_SOME_assocv_rec = maybe_thm ("IS_SOME_assocv_rec", 1451``(IS_SOME o assocv ([]:('a#'b)list) = {}) /\ 1452 (!a:'a b:'b l. IS_SOME o assocv ((a,b)::l) = a INSERT IS_SOME o assocv l)``, 1453SRW_TAC [] [assocv, combinTheory.o_THM, EXTENSION, SPECIFICATION] THEN 1454Cases_on `x = a` THEN SRW_TAC [] []); 1455 1456val FINITE_assocv = maybe_thm ("FINITE_assocv", 1457``!l:('a#'b)list. FINITE (IS_SOME o assocv l)``, 1458Induct THENL 1459[REWRITE_TAC [FINITE_EMPTY, IS_SOME_assocv_rec] 1460,P_PGEN_TAC ``x:'a,y:'b`` THEN 1461 ASM_REWRITE_TAC [FINITE_INSERT, IS_SOME_assocv_rec] 1462]); 1463 1464val assocv_one_to_one = maybe_thm ("assocv_one_to_one", Term 1465`!cmp l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==> 1466 (assocv l = assocv m) ==> (l = m)`, 1467REPEAT GEN_TAC THEN 1468DISCH_THEN (fn cj => REWRITE_TAC [SYM (MATCH_MP ORL_MEM_EQ cj)] 1469 THEN STRIP_ASSUME_TAC cj) THEN 1470REPEAT STRIP_TAC THEN 1471Q.SPEC_TAC (`ab`,`ab`) THEN P_PGEN_TAC ``a:'a,b:'b`` THEN 1472IMP_RES_THEN (REWRITE_TAC o ulist o GSYM) assocv_MEM_thm THEN AR); 1473 1474(* Prove bt_to_orl inverts list_to_bt for ordered lists, using above lemmas. *) 1475 1476val ORL_fmap_EQ = maybe_thm ("ORL_fmap_EQ", 1477``!cmp l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==> 1478 ((fmap l = fmap m) <=> (l = m))``, 1479REPEAT GEN_TAC THEN 1480DISCH_THEN (ASSUME_TAC o MATCH_MP assocv_one_to_one) THEN EQ_TAC THENL 1481[REWRITE_TAC [fmap_ALT] THEN METIS_TAC [FINITE_assocv, unlookup_11] 1482,STRIP_TAC THEN AR 1483]); 1484 1485(* OFU, UFO imitate OU, UO from enumeralTheory respectively *) 1486 1487val OFU = Define`OFU cmp (f:'a|->'b) (g:'a|->'b) = 1488 DRESTRICT f {x | LESS_ALL cmp x (FDOM g)} FUNION g`; 1489 1490val UFO = Define`UFO cmp (f:'a|->'b) (g:'a|->'b) = 1491 f FUNION DRESTRICT g {y | !z. z IN FDOM f ==> (apto cmp z y = LESS)}`; 1492 1493val FDOM_OFU = maybe_thm ("FDOM_OFU", 1494``!cmp (f:'a|->'b) (g:'a|->'b). FDOM (OFU cmp f g) = OU cmp (FDOM f) (FDOM g)``, 1495RW_TAC (srw_ss()) 1496 [OFU, OU, LESS_ALL, FDOM_DRESTRICT, EXTENSION, IN_UNION, IN_INTER]); 1497 1498val FDOM_UFO = maybe_thm ("FDOM_UFO", 1499``!cmp (f:'a|->'b) (g:'a|->'b). FDOM (UFO cmp f g) = UO cmp (FDOM f) (FDOM g)``, 1500RW_TAC (srw_ss()) 1501 [UFO, UO, FDOM_DRESTRICT, EXTENSION, IN_UNION, IN_INTER]); 1502 1503val sing_UFO = maybe_thm ("sing_UFO", 1504``!cmp x:'a y:'b t:'a|->'b. UFO cmp (FEMPTY |+ (x,y)) t = 1505 (FEMPTY |+ (x,y)) FUNION (DRESTRICT t {z | apto cmp x z = LESS})``, 1506SRW_TAC [] [UFO]); 1507 1508val bt_to_fmap_OFU_UFO = maybe_thm ("bt_to_fmap_OFU_UFO", 1509``!cmp l x:'a y:'b r. FMAPAL cmp (node l (x,y) r) = 1510 OFU cmp (FMAPAL cmp l) (UFO cmp (FEMPTY |+ (x,y)) (FMAPAL cmp r))``, 1511SRW_TAC [] [OFU, bt_to_fmap, LESS_UO_LEM, FDOM_OFU, FDOM_UFO] THEN 1512REWRITE_TAC [GSYM FUNION_ASSOC] THEN 1513ONCE_REWRITE_TAC [GSYM sing_UFO] THEN AP_THM_TAC THEN AP_TERM_TAC THEN 1514AP_TERM_TAC THEN SRW_TAC [] [UO, LESS_ALL, EXTENSION] THEN 1515METIS_TAC [totoLLtrans]); 1516 1517val FAPPLY_OFU = maybe_thm ("FAPPLY_OFU", 1518``!cmp x u:'a|->'b v:'a|->'b. OFU cmp u v ' x = 1519 if LESS_ALL cmp x (FDOM v) then u ' x else v ' x``, 1520SRW_TAC [] [OFU, FDOM_OFU, FUNION_DEF, DRESTRICT_DEF] THEN 1521`x NOTIN FDOM u` by METIS_TAC [] THEN 1522`x NOTIN FDOM v` by METIS_TAC [LESS_ALL, all_cpn_distinct, toto_equal_eq] THEN 1523IMP_RES_THEN SUBST1_TAC NOT_FDOM_FAPPLY_FEMPTY THEN REFL_TAC); 1524 1525val OFU_FEMPTY = maybe_thm ("OFU_FEMPTY", 1526``!cmp t:'a|->'b. OFU cmp t FEMPTY = t``, 1527SRW_TAC [] [fmap_EXT, OU_EMPTY, FDOM_OFU, FAPPLY_OFU, LESS_ALL]); 1528 1529val FEMPTY_OFU = maybe_thm ("FEMPTY_OFU", 1530``!cmp f:'a|->'b. OFU cmp FEMPTY f = f``, 1531SRW_TAC [] [fmap_EXT, EMPTY_OU, FDOM_OFU, FAPPLY_OFU] THEN 1532`~LESS_ALL cmp x (FDOM f)` 1533 by (SRW_TAC [] [LESS_ALL] THEN 1534 Q.EXISTS_TAC `x` THEN SRW_TAC [] [toto_refl]) THEN 1535AR); 1536 1537val LESS_ALL_OFU = maybe_thm ("LESS_ALL_OFU", 1538``!cmp x u:'a|->'b v:'a|->'b. LESS_ALL cmp x (FDOM (OFU cmp u v)) <=> 1539 LESS_ALL cmp x (FDOM u) /\ LESS_ALL cmp x (FDOM v)``, 1540METIS_TAC [FDOM_OFU, LESS_ALL_OU]); 1541 1542val OFU_ASSOC = maybe_thm ("OFU_ASSOC", 1543``!cmp f g h:'a|->'b. OFU cmp f (OFU cmp g h) = OFU cmp (OFU cmp f g) h``, 1544RW_TAC bool_ss [fmap_EXT, FDOM_OFU, OU_ASSOC] THEN 1545RW_TAC bool_ss [FAPPLY_OFU, FUNION_DEF, OFU, LESS_ALL_OFU] THEN METIS_TAC []); 1546 1547val bl_to_fmap = Define 1548`(bl_to_fmap cmp (nbl:('a#'b)bl) = FEMPTY) /\ 1549 (bl_to_fmap cmp (zerbl b) = bl_to_fmap cmp b) /\ 1550 (bl_to_fmap cmp (onebl (x,y) t b) = 1551 OFU cmp (FEMPTY |+ (x,y) FUNION 1552 DRESTRICT (FMAPAL cmp t) {z | apto cmp x z = LESS}) 1553 (bl_to_fmap cmp b))`; 1554 1555val bl_to_fmap_OFU_UFO = maybe_thm ("bl_to_fmap_OFU_UFO", 1556``!cmp x:'a y:'b t b. bl_to_fmap cmp (onebl (x,y) t b) = 1557 OFU cmp (UFO cmp (FEMPTY |+ (x,y)) (FMAPAL cmp t)) (bl_to_fmap cmp b)``, 1558REWRITE_TAC [bl_to_fmap, sing_UFO]); 1559 1560val bl_rev_fmap_lem = maybe_thm ("bl_rev_fmap_lem", ``!cmp b t:('a#'b)bt. 1561 FMAPAL cmp (bl_rev t b) = OFU cmp (FMAPAL cmp t) (bl_to_fmap cmp b)``, 1562GEN_TAC THEN Induct THEN TRY (GEN_TAC THEN P_PGEN_TAC ``x:'a,y:'b``) THEN 1563SRW_TAC [] [bl_rev, bl_to_fmap_OFU_UFO] THEN 1564REWRITE_TAC [bl_to_fmap, OFU_FEMPTY, bt_to_fmap_OFU_UFO, OFU_ASSOC]); 1565 1566(* Converting a bl to a bt preserves the represented fmap. *) 1567 1568val bl_to_bt_fmap = maybe_thm ("bl_to_bt_fmap", 1569``!cmp b:('a#'b)bl. FMAPAL cmp (bl_to_bt b) = bl_to_fmap cmp b``, 1570REWRITE_TAC [bl_to_bt, bl_rev_fmap_lem, bt_to_fmap, FEMPTY_OFU]); 1571 1572(* Imitating enumeralTheory as usual, we next aim to show that building a 1573 bl from a list does the same, and to begin with that 1574 1575 LESS_ALL cmp x (FDOM (bl_to_fmap cmp b)) ==> 1576 (bl_to_fmap cmp (BL_CONS (x,y) b) = bl_to_fmap cmp b |+ (x,y), 1577 1578 or generalizing to suit BL_ACCUM, that 1579 1580 LESS_ALL cmp x (FDOM (FMAPAL cmp t)) /\ 1581 LESS_ALL cmp x (FDOM (bl_to_fmap cmp b)) ==> 1582 (bl_to_fmap cmp (BL_ACCUM (x,y) t b) = 1583 (OFU cmp (FMAPAL cmp t) (bl_to_fmap cmp b)) |+ (x,y) . *) 1584 1585val LESS_ALL_UFO_LEM = maybe_thm ("LESS_ALL_UFO_LEM", 1586``!cmp x:'a y:'b f. LESS_ALL cmp x (FDOM f) ==> 1587 (UFO cmp (FEMPTY |+ (x,y)) f = f |+ (x,y))``, 1588SRW_TAC [] [LESS_ALL, UFO, fmap_EXT, FUNION_DEF, DRESTRICT_DEF, 1589 EXTENSION, FAPPLY_FUPDATE_THM] THEN 1590METIS_TAC []); 1591 1592val LESS_ALL_OFU_UFO_LEM = maybe_thm ("LESS_ALL_OFU_UFO_LEM", 1593``!cmp x:'a y:'b f g. LESS_ALL cmp x (FDOM f) /\ LESS_ALL cmp x (FDOM g) ==> 1594(OFU cmp (UFO cmp (FEMPTY |+ (x,y)) f) g = (OFU cmp f g) |+ (x,y))``, 1595REPEAT STRIP_TAC THEN IMP_RES_THEN (REWRITE_TAC o ulist) LESS_ALL_UFO_LEM THEN 1596SRW_TAC [] [fmap_EXT] THENL 1597[REWRITE_TAC [FDOM_OFU, FDOM_FUPDATE] THEN 1598 IMP_RES_THEN SUBST1_TAC (GSYM LESS_ALL_UO_LEM) THEN 1599 IMP_RES_TAC LESS_ALL_OU_UO_LEM 1600,SRW_TAC [] [FAPPLY_OFU, FAPPLY_FUPDATE_THM] THEN RES_TAC 1601]); 1602 1603val DRESTRICT_SUPERSET = maybe_thm ("DRESTRICT_SUPERSET", 1604``!f:'a|->'b s. FDOM f SUBSET s ==> (DRESTRICT f s = f)``, 1605SRW_TAC [] [DRESTRICT_DEF, SUBSET_DEF, fmap_EXT] THEN 1606METIS_TAC [EXTENSION, IN_INTER]); 1607 1608val SING_FUNION = maybe_thm ("SING_FUNION", 1609``!f x:'a y:'b. FEMPTY |+ (x,y) FUNION f = f |+ (x,y)``, 1610SRW_TAC [] 1611 [fmap_EXT, FUNION_DEF, FAPPLY_FUPDATE_THM, GSYM INSERT_SING_UNION]); 1612 1613val BL_ACCUM_fmap = maybe_thm ("BL_ACCUM_fmap", 1614``!cmp x:'a y:'b b t. LESS_ALL cmp x (FDOM (FMAPAL cmp t)) /\ 1615 LESS_ALL cmp x (FDOM (bl_to_fmap cmp b)) ==> 1616 (bl_to_fmap cmp (BL_ACCUM (x,y) t b) = 1617 OFU cmp (FMAPAL cmp t) (bl_to_fmap cmp b) |+ (x,y))``, 1618GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN Induct THEN 1619TRY (GEN_TAC THEN P_PGEN_TAC ``p:'a,q:'b``) THEN 1620SRW_TAC [] [BL_ACCUM, bl_to_fmap_OFU_UFO, bt_to_fmap_OFU_UFO] THENL 1621[METIS_TAC [LESS_ALL_UFO_LEM, LESS_ALL_OFU_UFO_LEM, bl_to_fmap] 1622,METIS_TAC [LESS_ALL_UFO_LEM, LESS_ALL_OFU_UFO_LEM, bl_to_fmap] 1623,REWRITE_TAC [bl_to_fmap] THEN 1624 `LESS_ALL cmp x (FDOM (UFO cmp (FEMPTY |+ (p,q)) (FMAPAL cmp b0))) /\ 1625 LESS_ALL cmp x (FDOM (bl_to_fmap cmp b))` by 1626 ASM_REWRITE_TAC [GSYM LESS_ALL_OFU] THEN 1627 `LESS_ALL cmp x (FDOM (FMAPAL cmp (node t (p,q) b0)))` 1628 by ASM_REWRITE_TAC [bt_to_fmap_OFU_UFO, LESS_ALL_OFU] THEN 1629 RES_TAC THEN ASM_REWRITE_TAC [bt_to_fmap_OFU_UFO, OFU_ASSOC] 1630]); 1631 1632val BL_CONS_fmap = maybe_thm ("BL_CONS_fmap", 1633``!cmp x:'a y:'b b. LESS_ALL cmp x (FDOM (bl_to_fmap cmp b)) ==> 1634 (bl_to_fmap cmp (BL_CONS (x,y) b) = bl_to_fmap cmp b |+ (x,y))``, 1635REPEAT STRIP_TAC THEN REWRITE_TAC [BL_CONS] THEN 1636Q.SUBGOAL_THEN `OFU cmp (FMAPAL cmp nt) (bl_to_fmap cmp b) = bl_to_fmap cmp b` 1637(SUBST1_TAC o SYM) 1638THEN1 REWRITE_TAC [bt_to_fmap, FEMPTY_OFU] THEN 1639`LESS_ALL cmp x (FDOM (FMAPAL cmp nt))` 1640by REWRITE_TAC [LESS_ALL, NOT_IN_EMPTY, bt_to_fmap, FDOM_FEMPTY] THEN 1641IMP_RES_TAC BL_ACCUM_fmap THEN AR); 1642 1643val list_to_bl_fmap = maybe_thm ("list_to_bl_fmap", 1644``!cmp l:('a#'b)list. ORL cmp l ==> 1645 (bl_to_fmap cmp (list_to_bl l) = fmap l)``, 1646GEN_TAC THEN Induct THEN TRY (P_PGEN_TAC ``x:'a, y:'b``) THEN 1647SRW_TAC [] [bl_to_fmap, list_to_bl, fmap_rec, ORL] THEN 1648RES_THEN (SUBST1_TAC o SYM) THEN MATCH_MP_TAC BL_CONS_fmap THEN 1649RES_THEN SUBST1_TAC THEN METIS_TAC [MEM_IN_DOM_fmap, LESS_ALL]); 1650 1651val bt_to_orl_ID = maybe_thm ("bt_to_orl_ID", 1652``!cmp. !l::ORL cmp. bt_to_orl cmp (list_to_bt l) = (l:('a#'b)list)``, 1653GEN_TAC THEN CONV_TAC RES_FORALL_CONV THEN 1654REWRITE_TAC [SPECIFICATION] THEN GEN_TAC THEN DISCH_TAC THEN 1655Q.SUBGOAL_THEN `ORL cmp (bt_to_orl cmp (list_to_bt l)) /\ ORL cmp l` 1656(REWRITE_TAC o ulist o GSYM o MATCH_MP ORL_fmap_EQ) 1657THEN1 ASM_REWRITE_TAC [ORL_bt_to_orl] THEN 1658IMP_RES_THEN (SUBST1_TAC o SYM) list_to_bl_fmap THEN 1659REWRITE_TAC [GSYM bl_to_bt_fmap, list_to_bt, orl_fmap]); 1660 1661val bt_to_orl_ID_IMP = save_thm ("bt_to_orl_ID_IMP", REWRITE_RULE 1662 [SPECIFICATION] (CONV_RULE (ONCE_DEPTH_CONV RES_FORALL_CONV) bt_to_orl_ID)); 1663 1664(* bt_to_orl_ID_IMP = !cmp l. ORL cmp l ==> (bt_to_orl cmp (list_to_bt l) = l)*) 1665 1666val orl_to_bt_ID = maybe_thm ("orl_to_bt_ID", ``!cmp t:('a#'b)bt. 1667 FMAPAL cmp (list_to_bt (bt_to_orl cmp t)) = FMAPAL cmp t``, 1668METIS_TAC [bt_to_orl_ID_IMP, orl_fmap, ORL_bt_to_orl]); 1669 1670(* ************************************************************************* *) 1671(* *********************** Now to prove merge_fmap ************************* *) 1672(* ************************************************************************* *) 1673 1674val assocv_MEM_MAP_THE = maybe_thm ("assocv_MEM_MAP_THE", 1675``!x f:'a->'b option l. MEM x l /\ ALL_DISTINCT l /\ IS_SOME (f x) ==> 1676 (assocv (MAP (\x. (x, THE (f x))) l) x = f x)``, 1677GEN_TAC THEN GEN_TAC THEN Induct THEN 1678REWRITE_TAC [MEM, ALL_DISTINCT, MAP] THEN BETA_TAC THEN 1679REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [assocv] THENL 1680[UNDISCH_TAC (Term`IS_SOME ((f:'a->'b option) x)`) THEN 1681 ASM_REWRITE_TAC [option_CLAUSES] 1682,COND_CASES_TAC THENL 1683 [UNDISCH_TAC (Term`MEM (x:'a) l`) THEN AR 1684 ,RES_TAC]]); 1685 1686(* ********* merge_smerge not used, but seems hygienic *********** *) 1687 1688val merge_smerge = maybe_thm ("merge_smerge", ``!cmp l m:('a#'b)list. 1689 MAP FST (merge cmp l m) = smerge cmp (MAP FST l) (MAP FST m)``, 1690GEN_TAC THEN Induct THEN TRY (P_PGEN_TAC ``a:'a,b:'b``) THEN 1691SRW_TAC [] [merge_thm] THEN 1692Induct_on `m` THEN TRY (P_PGEN_TAC ``c:'a,d:'b``) THEN 1693Cases_on `apto cmp a c` THEN 1694SRW_TAC [] [smerge, smerge_nil, merge_thm, MAP]); 1695 1696val IS_SOME_assocv = maybe_thm ("IS_SOME_assocv", 1697``!l:('a#'b)list. IS_SOME o (assocv l) = set (MAP FST l)``, 1698CONV_TAC (QUANT_CONV FUN_EQ_CONV) THEN 1699REWRITE_TAC [combinTheory.o_THM] THEN Induct THENL 1700[SRW_TAC [] [assocv, LIST_TO_SET, combinTheory.C_THM] 1701,P_PGEN_TAC (Term`y:'a,z:'b`) THEN GEN_TAC THEN 1702 ASM_REWRITE_TAC [assocv, LIST_TO_SET_THM, MAP, FST, HD] THEN 1703 CONV_TAC (RAND_CONV (REWR_CONV (GSYM SPECIFICATION))) THEN 1704 REWRITE_TAC [IN_INSERT] THEN Cases_on `x = y` THEN AR THENL 1705 [REWRITE_TAC [option_CLAUSES] 1706 ,REWRITE_TAC [SPECIFICATION] 1707]]); 1708 1709val FDOM_assocv = maybe_thm ("FDOM_assocv", 1710``!l:('a#'b)list. FDOM (unlookup (assocv l)) = set (MAP FST l)``, 1711GEN_TAC THEN 1712MP_TAC (ISPEC ``MAP FST (l:('a#'b)list)`` FINITE_LIST_TO_SET) THEN 1713REWRITE_TAC [GSYM IS_SOME_assocv] THEN 1714MATCH_ACCEPT_TAC unlookup_FDOM); 1715 1716val fmap_FDOM = store_thm ("fmap_FDOM", 1717``!l:('a#'b)list. FDOM (fmap l) = set (MAP FST l)``, 1718REWRITE_TAC [fmap, FDOM_FUPDATE_LIST, 1719 LIST_TO_SET_REVERSE, FDOM_FEMPTY, UNION_EMPTY, 1720 rich_listTheory.MAP_REVERSE]); 1721 1722val FUPDATE_LIST_SNOC = maybe_thm ("FUPDATE_LIST_SNOC", 1723``!l:('a#'b)list fm xy. fm |++ (l ++ [xy]) = (fm |++ l) |+ xy``, 1724REWRITE_TAC [FUPDATE_LIST_APPEND, FUPDATE_LIST, FOLDL]); 1725 1726val FINITE_IS_SOME_assocv = maybe_thm ("FINITE_IS_SOME_assocv", 1727``!l:('a#'b)list. FINITE (IS_SOME o assocv l)``, 1728REWRITE_TAC [IS_SOME_assocv, FINITE_LIST_TO_SET]); 1729 1730val fmap_ALT = maybe_thm ("fmap_ALT", 1731``!l:('a#'b)list. fmap l = unlookup (assocv l)``, 1732REWRITE_TAC [FUPDATE_ALT, fmap_EXT] THEN GEN_TAC THEN CONJ_TAC THENL 1733[REWRITE_TAC [fmap_FDOM, FDOM_assocv] 1734,GEN_TAC THEN 1735 REWRITE_TAC [fmap_FDOM, fmap, SPECIFICATION] THEN 1736 Induct_on `l` THENL 1737 [REWRITE_TAC [MAP, LIST_TO_SET_THM, rrs NOT_IN_EMPTY] 1738 ,P_PGEN_TAC ``y:'a,v:'b`` THEN 1739 ASSUME_TAC (ISPEC ``(y:'a,v:'b)::l`` FINITE_IS_SOME_assocv) THEN 1740 ASSUME_TAC (SPEC_ALL FINITE_IS_SOME_assocv) THEN 1741 IMP_RES_THEN (ASSUME_TAC o 1742 REWRITE_RULE [IS_SOME_assocv, SPECIFICATION]) FUN_FMAP_DEF THEN 1743 DISCH_THEN (fn ins => MP_TAC ins THEN ASSUME_TAC ins) THEN 1744 REWRITE_TAC [MAP, FST, LIST_TO_SET_THM, rrs IN_INSERT] THEN 1745 REWRITE_TAC [REVERSE_DEF, FUPDATE_LIST_SNOC, unlookup] THEN 1746 Cases_on `x = y` THEN ASM_REWRITE_TAC [FAPPLY_FUPDATE_THM] THENL 1747 [SUBGOAL_THEN ``set (MAP FST ((y:'a,v:'b)::l)) y`` ASSUME_TAC 1748 THEN1 REWRITE_TAC [MAP, FST, LIST_TO_SET_THM, rrs IN_INSERT] THEN 1749 REWRITE_TAC [IS_SOME_assocv] THEN 1750 RES_THEN (REWRITE_TAC o ulist) THEN 1751 REWRITE_TAC [THE_DEF, assocv, combinTheory.o_THM] 1752 ,DISCH_TAC THEN RES_THEN (REWRITE_TAC o ulist) THEN 1753 ASM_REWRITE_TAC [unlookup, IS_SOME_assocv] THEN 1754 RES_THEN (REWRITE_TAC o ulist) THEN 1755 ASM_REWRITE_TAC [combinTheory.o_THM, assocv] 1756]]]); 1757 1758val merge_fmap = maybe_thm ("merge_fmap", 1759``!cmp l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==> 1760 (fmap (merge cmp l m) = fmap l FUNION fmap m)``, 1761RW_TAC bool_ss [fmap_ALT] THEN 1762SUBST1_TAC (MATCH_MP unlookup_FUNION (CONJ 1763 (Q.SPEC `l` FINITE_IS_SOME_assocv) (Q.SPEC `m` FINITE_IS_SOME_assocv))) THEN 1764AP_TERM_TAC THEN IMP_RES_TAC merge_fun); 1765 1766(* *** Summary theorems, with and without restricted quantification: **** *) 1767 1768val ORL_FUNION = maybe_thm ("ORL_FUNION", 1769``!cmp. !l:('a#'b)list m::ORL cmp. ORL cmp (merge cmp l m) /\ 1770 (fmap (merge cmp l m) = fmap l FUNION fmap m)``, 1771CONV_TAC (DEPTH_CONV RES_FORALL_CONV) THEN 1772SRW_TAC [] [SPECIFICATION, merge_ORL, merge_fmap]); 1773 1774val ORL_FUNION_IMP = save_thm ("ORL_FUNION_IMP", REWRITE_RULE [SPECIFICATION] 1775 (CONV_RULE (DEPTH_CONV RES_FORALL_CONV) ORL_FUNION)); 1776 1777(* ORL_FUNION_IMP = |- !cmp l. ORL cmp l ==> !m. ORL cmp m ==> 1778 ORL cmp (merge cmp l m) /\ (fmap (merge cmp l m) = fmap l FUNION fmap m) *) 1779 1780val FMAPAL_FUNION = maybe_thm ("FMAPAL_FUNION", 1781``!cmp f g:('a#'b)bt. 1782 FMAPAL cmp (list_to_bt (merge cmp (bt_to_orl cmp f) (bt_to_orl cmp g))) = 1783 FMAPAL cmp f FUNION FMAPAL cmp g``, 1784RW_TAC bool_ss [orl_fmap] THEN 1785`ORL cmp (bt_to_orl cmp f) /\ ORL cmp (bt_to_orl cmp g)` 1786by REWRITE_TAC [ORL_bt_to_orl] THEN 1787`ORL cmp (merge cmp (bt_to_orl cmp f) (bt_to_orl cmp g))` 1788by IMP_RES_TAC merge_ORL THEN 1789IMP_RES_THEN SUBST1_TAC bt_to_orl_ID_IMP THEN 1790IMP_RES_TAC merge_fmap); 1791 1792(* We really need a merge-like computation rule for DRESTRICT. It might 1793 be that and a logarithmic rule for IN FDOM wd. be enough for now. *) 1794 1795val FMAPAL_FDOM_THM = store_thm ("FMAPAL_FDOM_THM", 1796``(!cmp x:'a. x IN FDOM (FMAPAL cmp (nt:('a#'b)bt)) = F) /\ 1797 (!cmp x a:'a b:'b l r. x IN FDOM (FMAPAL cmp (node l (a,b) r)) = 1798 case apto cmp x a of 1799 LESS => x IN FDOM (FMAPAL cmp l) 1800 | EQUAL => T 1801 | GREATER => x IN FDOM (FMAPAL cmp r))``, 1802SRW_TAC [] [IN_bt_to_set, bt_FST_FDOM, bt_map] THEN 1803Q.SUBGOAL_THEN `(x = a) <=> (apto cmp x a = EQUAL)` SUBST1_TAC 1804THEN1 MATCH_ACCEPT_TAC (GSYM toto_equal_eq) THEN 1805Cases_on `apto cmp x a` THEN 1806SRW_TAC [] [GSYM toto_antisym]); 1807 1808(* *********************************************************************** *) 1809(* inter_merge, for domain restriction, followed by diff_merge, for *) 1810(* domain restriction to the complement, are shown to implement DRESTRICT. *) 1811(* *********************************************************************** *) 1812 1813val inter_merge = Define 1814`(inter_merge cmp [] [] = []) /\ 1815 (inter_merge cmp ((a:'a,b:'b)::l) ([]:'a list) = []) /\ 1816 (inter_merge cmp [] (y:'a::m) = []) /\ 1817 (inter_merge cmp ((a,b)::l) (y::m) = case apto cmp a y of 1818 LESS => inter_merge cmp l (y::m) 1819 | EQUAL => (a,b) :: inter_merge cmp l m 1820 | GREATER => inter_merge cmp ((a,b)::l) m)`; 1821 1822val inter_merge_ind = theorem "inter_merge_ind"; 1823 1824(* inter_merge_ind = |- !P. 1825 (!cmp. P cmp [] []) /\ (!cmp a b l. P cmp ((a,b)::l) []) /\ 1826 (!cmp y m. P cmp [] (y::m)) /\ 1827 (!cmp a b l y m. 1828 ((apto cmp a y = EQUAL) ==> P cmp l m) /\ 1829 ((apto cmp a y = GREATER) ==> P cmp ((a,b)::l) m) /\ 1830 ((apto cmp a y = LESS) ==> P cmp l (y::m)) ==> 1831 P cmp ((a,b)::l) (y::m)) ==> 1832 !v v1 v2. P v v1 v2 *) 1833 1834val inter_merge_subset_inter = maybe_thm ("inter_merge_subset_inter", 1835``!cmp:'a toto l:('a#'b)list m. 1836 !x z. MEM (x,z) (inter_merge cmp l m) ==> MEM (x,z) l /\ MEM x m``, 1837HO_MATCH_MP_TAC inter_merge_ind THEN 1838REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN 1839REWRITE_TAC [inter_merge, MEM] THEN 1840Cases_on `apto cmp a y` THEN 1841REWRITE_TAC [all_cpn_distinct] THEN 1842STRIP_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [cpn_case_def] THENL 1843[METIS_TAC [MEM] 1844,`a = y` by IMP_RES_TAC toto_equal_eq THEN 1845 RW_TAC bool_ss [MEM] THEN DISJ2_TAC THEN RES_TAC 1846,METIS_TAC [MEM] 1847]); 1848 1849val LESS_NOT_MEM = maybe_thm ("LESS_NOT_MEM", 1850``!cmp x m y:'a. (apto cmp x y = LESS) /\ OL cmp (y::m) ==> ~MEM x m``, 1851GEN_TAC THEN GEN_TAC THEN Induct THEN SRW_TAC [] [MEM] THENL 1852[METIS_TAC [OL, MEM, totoLLtrans, toto_glneq] 1853,IMP_RES_TAC OL THEN 1854 `apto cmp x h = LESS` by (MATCH_MP_TAC totoLLtrans THEN 1855 Q.EXISTS_TAC `y` THEN AR THEN 1856 METIS_TAC [OL, MEM]) THEN 1857 RES_TAC 1858]); 1859 1860val inter_subset_inter_merge = maybe_thm ("inter_subset_inter_merge", 1861``!cmp:'a toto l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 1862 !x z. MEM (x,z) l /\ MEM x m ==> MEM (x,z) (inter_merge cmp l m)``, 1863HO_MATCH_MP_TAC inter_merge_ind THEN 1864REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN 1865REWRITE_TAC [inter_merge, MEM] THEN 1866Cases_on `apto cmp a y` THEN 1867REWRITE_TAC [all_cpn_distinct, MEM] THEN STRIP_TAC THEN 1868STRIP_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [cpn_case_def] THENL 1869[`a <> y` by IMP_RES_TAC toto_glneq THEN ASM_REWRITE_TAC [PAIR_EQ] THEN 1870 IMP_RES_TAC LESS_NOT_MEM THEN 1871 `ORL cmp l` by IMP_RES_TAC ORL THEN METIS_TAC [] 1872,`a = y` by IMP_RES_TAC toto_equal_eq THEN ASM_REWRITE_TAC [MEM, PAIR_EQ] THEN 1873 `OL cmp m` by IMP_RES_TAC OL THEN 1874 `ORL cmp l` by IMP_RES_TAC ORL THEN 1875 IMP_RES_TAC ORL_NOT_MEM THEN METIS_TAC [] 1876,`a <> y` by IMP_RES_TAC toto_glneq THEN 1877 IMP_RES_TAC LESS_NOT_MEM THEN 1878 `OL cmp m` by IMP_RES_TAC OL THEN 1879 IMP_RES_TAC toto_antisym THEN IMP_RES_TAC ORL_NOT_MEM THEN 1880 `y <> a` by IMP_RES_TAC toto_glneq THEN 1881 REPEAT STRIP_TAC THENL 1882 [METIS_TAC [PAIR_EQ] 1883 ,METIS_TAC [] 1884 ,METIS_TAC [MEM, ORL_NOT_MEM] 1885 ,METIS_TAC [] 1886]]); 1887 1888val inter_merge_MEM_thm = maybe_thm ("inter_merge_MEM_thm", 1889``!cmp:'a toto l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 1890 (!x y. MEM (x,y) (inter_merge cmp l m) <=> MEM (x,y) l /\ MEM x m)``, 1891REPEAT STRIP_TAC THEN EQ_TAC THENL 1892[MATCH_ACCEPT_TAC inter_merge_subset_inter 1893,IMP_RES_TAC inter_subset_inter_merge THEN STRIP_TAC THEN RES_TAC 1894]); 1895 1896val FST_inter_merge = maybe_thm ("FST_inter_merge", 1897``!cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 1898 (set (MAP FST (inter_merge cmp l m)) = set (MAP FST l) INTER set m)``, 1899SRW_TAC [] 1900 [inter_merge_MEM_thm, EXTENSION, MEM_MAP_FST_LEM] THEN 1901CONV_TAC (LAND_CONV EXISTS_AND_CONV) THEN REFL_TAC); 1902 1903val inter_merge_ORL = maybe_thm ("inter_merge_ORL", 1904``!cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 1905 ORL cmp (inter_merge cmp l m)``, 1906GEN_TAC THEN Induct THEN TRY (P_PGEN_TAC ``x:'a,y:'b``) THEN Induct THEN 1907SRW_TAC [] [inter_merge] THEN REWRITE_TAC [ORL] THEN 1908IMP_RES_TAC ORL THEN IMP_RES_TAC OL THEN 1909Cases_on `apto cmp x h` THEN SRW_TAC [] [] THEN 1910RW_TAC bool_ss [ORL] THEN IMP_RES_TAC inter_merge_subset_inter THEN RES_TAC); 1911 1912val IN_IS_SOME_NOT_NONE = maybe_thm ("IN_IS_SOME_NOT_NONE", 1913``!x f:'a->'b option. (f x = NONE) ==> ~(x IN IS_SOME o f)``, 1914REWRITE_TAC [SPECIFICATION, combinTheory.o_THM] THEN 1915METIS_TAC [option_CLAUSES]); 1916 1917val inter_merge_fmap = maybe_thm ("inter_merge_fmap", 1918``!cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 1919 (fmap (inter_merge cmp l m) = DRESTRICT (fmap l) (set m))``, 1920RW_TAC bool_ss 1921 [fmap_ALT, fmap_EXT, FDOM_assocv, DRESTRICT_DEF, FST_inter_merge] THEN 1922REWRITE_TAC [unlookup] THEN 1923`x IN set (MAP FST (inter_merge cmp l m))` 1924 by (IMP_RES_TAC FST_inter_merge THEN AR) THEN 1925`x IN set (MAP FST l)` by IMP_RES_TAC IN_INTER THEN 1926`x IN IS_SOME o assocv (inter_merge cmp l m) /\ x IN IS_SOME o assocv l` 1927 by ASM_REWRITE_TAC [IS_SOME_assocv] THEN 1928`FINITE (IS_SOME o assocv (inter_merge cmp l m)) /\ FINITE (IS_SOME o assocv l)` 1929 by REWRITE_TAC [FINITE_IS_SOME_assocv] THEN 1930IMP_RES_TAC FUN_FMAP_DEF THEN ASM_REWRITE_TAC [combinTheory.o_THM] THEN 1931AP_TERM_TAC THEN 1932STRIP_ASSUME_TAC (ISPEC ``assocv (l:('a#'b)list) x`` option_nchotomy) THENL 1933[METIS_TAC [IN_IS_SOME_NOT_NONE] 1934,AR THEN 1935 Q.SUBGOAL_THEN `ORL cmp (inter_merge cmp l m)` 1936 (REWRITE_TAC o ulist o MATCH_MP assocv_MEM_thm) 1937 THEN1 IMP_RES_TAC inter_merge_ORL THEN 1938 REWRITE_TAC [MATCH_MP inter_merge_MEM_thm 1939 (CONJ (Q.ASSUME `ORL cmp l`) (Q.ASSUME `OL cmp m`))] THEN 1940 CONJ_TAC THENL 1941 [METIS_TAC [assocv_MEM_thm] 1942 ,METIS_TAC [IN_INTER] 1943]]); 1944 1945(* *** Summary theorems, with and without restricted quantification: **** *) 1946 1947val ORL_DRESTRICT = maybe_thm ("ORL_DRESTRICT", 1948``!cmp. !l:('a#'b)list::ORL cmp. !m::OL cmp. ORL cmp (inter_merge cmp l m) /\ 1949 (fmap (inter_merge cmp l m) = DRESTRICT (fmap l) (set m))``, 1950CONV_TAC (DEPTH_CONV RES_FORALL_CONV) THEN 1951SRW_TAC [] [SPECIFICATION, inter_merge_ORL, inter_merge_fmap]); 1952 1953val ORL_DRESTRICT_IMP = save_thm ("ORL_DRESTRICT_IMP", 1954REWRITE_RULE [SPECIFICATION] 1955 (CONV_RULE (DEPTH_CONV RES_FORALL_CONV) ORL_DRESTRICT)); 1956 1957(* ORL_DRESTRICT_IMP = |- !cmp l. ORL cmp l ==> !m. OL cmp m ==> 1958 ORL cmp (inter_merge cmp l m) /\ 1959 (fmap (inter_merge cmp l m) = DRESTRICT (fmap l) (set m)) *) 1960 1961val FMAPAL_DRESTRICT = maybe_thm ("FMAPAL_DRESTRICT", 1962``!cmp f:('a#'b)bt s:'a bt. 1963 FMAPAL cmp (list_to_bt (inter_merge cmp (bt_to_orl cmp f) (bt_to_ol cmp s))) = 1964 DRESTRICT (FMAPAL cmp f) (ENUMERAL cmp s)``, 1965RW_TAC bool_ss [orl_fmap, ol_set] THEN 1966`ORL cmp (bt_to_orl cmp f) /\ OL cmp (bt_to_ol cmp s)` 1967by REWRITE_TAC [ORL_bt_to_orl, OL_bt_to_ol] THEN 1968`ORL cmp (inter_merge cmp (bt_to_orl cmp f) (bt_to_ol cmp s))` 1969by IMP_RES_TAC inter_merge_ORL THEN 1970IMP_RES_THEN SUBST1_TAC bt_to_orl_ID_IMP THEN 1971IMP_RES_TAC inter_merge_fmap); 1972 1973(* ********* Do the corresponding stuff for diff_merge ******* *) 1974 1975val diff_merge = Define 1976`(diff_merge cmp [] [] = []) /\ 1977 (diff_merge cmp ((a:'a,b:'b)::l) ([]:'a list) = (a,b)::l) /\ 1978 (diff_merge cmp [] (y:'a::m) = []) /\ 1979 (diff_merge cmp ((a,b)::l) (y::m) = case apto cmp a y of 1980 LESS => (a,b) :: diff_merge cmp l (y::m) 1981 | EQUAL => diff_merge cmp l m 1982 | GREATER => diff_merge cmp ((a,b)::l) m)`; 1983 1984val diff_merge_ind = theorem "diff_merge_ind"; 1985 1986(* diff_merge_ind = |- !P. 1987 (!cmp. P cmp [] []) /\ (!cmp a b l. P cmp ((a,b)::l) []) /\ 1988 (!cmp y m. P cmp [] (y::m)) /\ 1989 (!cmp a b l y m. 1990 ((apto cmp a y = EQUAL) ==> P cmp l m) /\ 1991 ((apto cmp a y = GREATER) ==> P cmp ((a,b)::l) m) /\ 1992 ((apto cmp a y = LESS) ==> P cmp l (y::m)) ==> 1993 P cmp ((a,b)::l) (y::m)) ==> 1994 !v v1 v2. P v v1 v2 *) 1995 1996val inter_subset_diff_merge = maybe_thm ("inter_subset_diff_merge", 1997``!cmp:'a toto l:('a#'b)list m. 1998 !x z. MEM (x,z) l /\ ~MEM x m ==> MEM (x,z) (diff_merge cmp l m)``, 1999HO_MATCH_MP_TAC diff_merge_ind THEN 2000REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN 2001REWRITE_TAC [diff_merge, MEM] THEN 2002Cases_on `apto cmp a y` THEN 2003REWRITE_TAC [all_cpn_distinct] THEN 2004STRIP_TAC THEN REPEAT GEN_TAC THEN ASM_REWRITE_TAC [cpn_case_def] THENL 2005[METIS_TAC [MEM] 2006,`a = y` by IMP_RES_TAC toto_equal_eq THEN 2007 RW_TAC bool_ss [MEM] THEN RES_TAC 2008,METIS_TAC [MEM] 2009]); 2010 2011val diff_merge_subset_inter = maybe_thm ("diff_merge_subset_inter", 2012``!cmp:'a toto l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 2013 !x z. MEM (x,z) (diff_merge cmp l m) ==> MEM (x,z) l /\ ~MEM x m``, 2014HO_MATCH_MP_TAC diff_merge_ind THEN 2015REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN 2016REWRITE_TAC [diff_merge, MEM] THEN 2017Cases_on `apto cmp a y` THEN 2018REWRITE_TAC [all_cpn_distinct, MEM] THEN STRIP_TAC THEN 2019STRIP_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [cpn_case_def] THENL 2020[`a <> y` by IMP_RES_TAC toto_glneq THEN 2021 IMP_RES_TAC LESS_NOT_MEM THEN 2022 `OL cmp m` by IMP_RES_TAC OL THEN 2023 IMP_RES_TAC ORL_NOT_MEM THEN 2024 IMP_RES_TAC toto_antisym THEN `y <> a` by IMP_RES_TAC toto_glneq THEN 2025 IMP_RES_TAC ORL THEN 2026 REPEAT STRIP_TAC THENL 2027 [IMP_RES_TAC MEM THENL 2028 [ASM_REWRITE_TAC [GSYM PAIR_EQ] 2029 ,DISJ2_TAC THEN RES_TAC 2030 ] 2031 ,METIS_TAC [MEM] 2032 ,METIS_TAC [MEM, PAIR_EQ] 2033 ] 2034,`a = y` by IMP_RES_TAC toto_equal_eq THEN ASM_REWRITE_TAC [MEM, PAIR_EQ] THEN 2035 `OL cmp m` by IMP_RES_TAC OL THEN 2036 `ORL cmp l` by IMP_RES_TAC ORL THEN 2037 IMP_RES_TAC ORL_NOT_MEM THEN METIS_TAC [] 2038,`a <> y` by IMP_RES_TAC toto_glneq THEN ASM_REWRITE_TAC [PAIR_EQ] THEN 2039 IMP_RES_TAC toto_antisym THEN IMP_RES_TAC LESS_NOT_MEM THEN 2040 `OL cmp m` by IMP_RES_TAC OL THEN 2041 METIS_TAC [MEM, PAIR_EQ, ORL_NOT_MEM] 2042]); 2043 2044val diff_merge_MEM_thm = maybe_thm ("diff_merge_MEM_thm", 2045``!cmp:'a toto l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 2046 (!x y. MEM (x,y) (diff_merge cmp l m) <=> MEM (x,y) l /\ ~MEM x m)``, 2047REPEAT STRIP_TAC THEN EQ_TAC THENL 2048[STRIP_TAC THEN IMP_RES_TAC diff_merge_subset_inter THEN AR 2049,MATCH_ACCEPT_TAC inter_subset_diff_merge 2050]); 2051 2052val FST_diff_merge = maybe_thm ("FST_diff_merge", 2053``!cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 2054 (set (MAP FST (diff_merge cmp l m)) = set (MAP FST l) DIFF set m)``, 2055SRW_TAC [] 2056 [diff_merge_MEM_thm, EXTENSION, MEM_MAP_FST_LEM] THEN 2057CONV_TAC (LAND_CONV EXISTS_AND_CONV) THEN REFL_TAC); 2058 2059val diff_merge_ORL = maybe_thm ("diff_merge_ORL", 2060``!cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 2061 ORL cmp (diff_merge cmp l m)``, 2062GEN_TAC THEN Induct THEN TRY (P_PGEN_TAC ``x:'a,y:'b``) THEN Induct THEN 2063SRW_TAC [] [diff_merge] THEN REWRITE_TAC [ORL] THEN 2064IMP_RES_TAC ORL THEN IMP_RES_TAC OL THEN 2065Cases_on `apto cmp x h` THEN SRW_TAC [] [] THEN 2066RW_TAC bool_ss [ORL] THEN IMP_RES_TAC diff_merge_subset_inter THEN RES_TAC); 2067 2068val INTER_OVER_DIFF = maybe_thm ("INTER_OVER_DIFF", 2069``!a b c:'a set. a INTER (b DIFF c) = a INTER b DIFF a INTER c``, 2070RW_TAC bool_ss [EXTENSION, IN_INTER, IN_DIFF] THEN tautLib.TAUT_TAC); 2071 2072val INTER_COMPL_DIFF = maybe_thm ("INTER_COMPL_DIFF", 2073``!a b:'a set. a INTER (COMPL b) = a DIFF b``, 2074RW_TAC bool_ss [EXTENSION, IN_INTER, IN_DIFF, IN_COMPL]); 2075 2076val diff_merge_fmap = maybe_thm ("diff_merge_fmap", 2077``!cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==> 2078 (fmap (diff_merge cmp l m) = DRESTRICT (fmap l) (COMPL (set m)))``, 2079RW_TAC bool_ss [fmap_ALT, fmap_EXT, FDOM_assocv, DRESTRICT_DEF, 2080 FST_diff_merge, INTER_COMPL_DIFF] THEN 2081REWRITE_TAC [unlookup] THEN 2082`x IN set (MAP FST (diff_merge cmp l m))` 2083 by (IMP_RES_TAC FST_diff_merge THEN AR) THEN 2084`x IN set (MAP FST l)` by IMP_RES_TAC IN_DIFF THEN 2085`x IN IS_SOME o assocv (diff_merge cmp l m) /\ x IN IS_SOME o assocv l` 2086 by ASM_REWRITE_TAC [IS_SOME_assocv] THEN 2087`FINITE (IS_SOME o assocv (diff_merge cmp l m)) /\ FINITE (IS_SOME o assocv l)` 2088 by REWRITE_TAC [FINITE_IS_SOME_assocv] THEN 2089IMP_RES_TAC FUN_FMAP_DEF THEN ASM_REWRITE_TAC [combinTheory.o_THM] THEN 2090AP_TERM_TAC THEN 2091STRIP_ASSUME_TAC (ISPEC ``assocv (l:('a#'b)list) x`` option_nchotomy) THENL 2092[METIS_TAC [IN_IS_SOME_NOT_NONE] 2093,AR THEN 2094 Q.SUBGOAL_THEN `ORL cmp (diff_merge cmp l m)` 2095 (REWRITE_TAC o ulist o MATCH_MP assocv_MEM_thm) 2096 THEN1 IMP_RES_TAC diff_merge_ORL THEN 2097 REWRITE_TAC [MATCH_MP diff_merge_MEM_thm 2098 (CONJ (Q.ASSUME `ORL cmp l`) (Q.ASSUME `OL cmp m`))] THEN 2099 CONJ_TAC THENL 2100 [METIS_TAC [assocv_MEM_thm] 2101 ,METIS_TAC [IN_DIFF] 2102]]); 2103 2104(* *** Summary theorems, with and without restricted quantification: **** *) 2105 2106val ORL_DRESTRICT_COMPL = maybe_thm ("ORL_DRESTRICT_COMPL", 2107``!cmp. !l:('a#'b)list::ORL cmp. !m::OL cmp. ORL cmp (diff_merge cmp l m) /\ 2108(fmap (diff_merge cmp l m) = DRESTRICT (fmap l) (COMPL (set m)))``, 2109CONV_TAC (DEPTH_CONV RES_FORALL_CONV) THEN 2110SRW_TAC [] [SPECIFICATION, diff_merge_ORL, diff_merge_fmap]); 2111 2112val ORL_DRESTRICT_COMPL_IMP = save_thm ("ORL_DRESTRICT_COMPL_IMP", 2113REWRITE_RULE [SPECIFICATION] 2114 (CONV_RULE (DEPTH_CONV RES_FORALL_CONV) ORL_DRESTRICT_COMPL)); 2115 2116(* ORL_DRESTRICT_COMPL_IMP = |- !cmp l. ORL cmp l ==> !m. OL cmp m ==> 2117 ORL cmp (diff_merge cmp l m) /\ 2118 (fmap (diff_merge cmp l m) = DRESTRICT (fmap l) (COMPL (set m))) *) 2119 2120val FMAPAL_DRESTRICT_COMPL = maybe_thm ("FMAPAL_DRESTRICT_COMPL", 2121``!cmp f:('a#'b)bt s:'a bt. 2122FMAPAL cmp (list_to_bt (diff_merge cmp (bt_to_orl cmp f) (bt_to_ol cmp s))) = 2123DRESTRICT (FMAPAL cmp f) (COMPL (ENUMERAL cmp s))``, 2124RW_TAC bool_ss [orl_fmap, ol_set] THEN 2125`ORL cmp (bt_to_orl cmp f) /\ OL cmp (bt_to_ol cmp s)` 2126by REWRITE_TAC [ORL_bt_to_orl, OL_bt_to_ol] THEN 2127`ORL cmp (diff_merge cmp (bt_to_orl cmp f) (bt_to_ol cmp s))` 2128by IMP_RES_TAC diff_merge_ORL THEN 2129IMP_RES_THEN SUBST1_TAC bt_to_orl_ID_IMP THEN 2130IMP_RES_TAC diff_merge_fmap); 2131 2132(* ********************************************************************* *) 2133(* Theorems to assist conversions *) 2134(* ********************************************************************* *) 2135 2136val FMAPAL_fmap = store_thm ("FMAPAL_fmap", 2137``!cmp l:('a#'b)list. fmap l = FMAPAL cmp (list_to_bt (incr_sort cmp l))``, 2138REPEAT GEN_TAC THEN CONV_TAC (LAND_CONV (REWR_CONV (GSYM incr_sort_fmap))) THEN 2139Q.SUBGOAL_THEN 2140`incr_sort cmp l = bt_to_orl cmp (list_to_bt (incr_sort cmp l))` 2141SUBST1_TAC THENL 2142[MATCH_MP_TAC (GSYM bt_to_orl_ID_IMP) THEN MATCH_ACCEPT_TAC incr_sort_ORL 2143,REWRITE_TAC [orl_to_bt_ID, orl_fmap] 2144]); 2145 2146val ORL_FMAPAL = store_thm ("ORL_FMAPAL", 2147``!cmp l:('a#'b)list. ORL cmp l ==> (fmap l = FMAPAL cmp (list_to_bt l))``, 2148REPEAT STRIP_TAC THEN 2149Q.SUBGOAL_THEN 2150`l = bt_to_orl cmp (list_to_bt l)` SUBST1_TAC THENL 2151[MATCH_MP_TAC (GSYM bt_to_orl_ID_IMP) THEN AR 2152,REWRITE_TAC [orl_to_bt_ID, orl_fmap] 2153]); 2154 2155val bt_to_orl_thm = maybe_thm ("bt_to_orl_thm", 2156``!cmp t:('a#'b)bt. bt_to_orl cmp t = bt_to_orl_ac cmp t []``, 2157SRW_TAC [] [orl_ac_thm]); 2158 2159val ORWL_FUNION_THM = store_thm ("ORWL_FUNION_THM", ``!cmp s:'a|->'b l t m. 2160 ORWL cmp s l /\ ORWL cmp t m ==> ORWL cmp (s FUNION t) (merge cmp l m)``, 2161METIS_TAC [ORWL, ORL_FUNION_IMP]); 2162 2163val ORWL_DRESTRICT_THM = store_thm ("ORWL_DRESTRICT_THM",``!cmp s:'a|->'b l t m. 2164ORWL cmp s l /\ OWL cmp t m ==> ORWL cmp (DRESTRICT s t)(inter_merge cmp l m)``, 2165METIS_TAC [OWL, ORWL, ORL_DRESTRICT_IMP]); 2166 2167val ORWL_DRESTRICT_COMPL_THM = store_thm ("ORWL_DRESTRICT_COMPL_THM", 2168``!cmp s:'a|->'b l t m. ORWL cmp s l /\ OWL cmp t m ==> 2169 ORWL cmp (DRESTRICT s (COMPL t)) (diff_merge cmp l m)``, 2170METIS_TAC [OWL, ORWL, ORL_DRESTRICT_COMPL_IMP]); 2171 2172val bt_map_ACTION = maybe_thm ("bt_map_ACTION", 2173``!f:'b->'c g:'a->'b t:'a bt. bt_map f (bt_map g t) = bt_map (f o g) t``, 2174GEN_TAC THEN GEN_TAC THEN Induct THEN SRW_TAC [] [bt_map]); 2175 2176(* The following may be useful for o_f_CONV, and more so for tc_CONV. *) 2177 2178val AP_SND = Define`AP_SND (f:'b->'c) (a:'a,b:'b) = (a, f b)`; 2179 2180val FST_two_ways = prove ( 2181``!f:'b->'c. FST o AP_SND f = (FST:'a#'b->'a)``, 2182GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN 2183P_PGEN_TAC ``a:'a,b:'b`` THEN SRW_TAC [] [combinTheory.o_THM, AP_SND]); 2184 2185val o_f_bt_map = store_thm ("o_f_bt_map", 2186``!cmp f:'b -> 'c t:('a#'b)bt. 2187 f o_f FMAPAL cmp t = FMAPAL cmp (bt_map (AP_SND f) t)``, 2188REPEAT GEN_TAC THEN REWRITE_TAC [fmap_EXT, FDOM_o_f] THEN CONJ_TAC THENL 2189[REWRITE_TAC [bt_FST_FDOM, bt_map_ACTION, FST_two_ways] 2190,GEN_TAC THEN ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN 2191 Induct_on `t` THENL 2192 [REWRITE_TAC [bt_FST_FDOM, bt_to_set, bt_map, NOT_IN_EMPTY] 2193 ,P_PGEN_TAC ``a:'a,b:'b`` THEN 2194 DISCH_THEN (fn infd => ASSUME_TAC infd THEN 2195 IMP_RES_THEN (REWRITE_TAC o ulist) 2196 (REWRITE_RULE [GSYM o_f_FDOM] o_f_DEF) THEN 2197 MP_TAC (REWRITE_RULE [FMAPAL_FDOM_THM] infd)) THEN 2198 REWRITE_TAC [bt_map, AP_SND, FAPPLY_node] THEN 2199 Cases_on `apto cmp x a` THEN SRW_TAC [] [] 2200]]); 2201 2202(* **** following is for INSERT - {} sets, adapted to fmap etc. **** *) 2203 2204val FAPPLY_fmap_NIL = store_thm ("FAPPLY_fmap_NIL", 2205``!x:'a. fmap ([]:('a#'b)list) ' x = FEMPTY ' x``, 2206SRW_TAC [] [fmap, FUPDATE_LIST_THM]); 2207 2208val FAPPLY_fmap_CONS = store_thm ("FAPPLY_fmap_CONS", 2209``!x y:'a z:'b l. fmap ((y,z)::l) ' x = 2210 if x = y then z else fmap l ' x``, 2211SRW_TAC [] [fmap, FUPDATE_LIST_SNOC, FAPPLY_FUPDATE_THM]); 2212 2213val fmap_CONS = maybe_thm ("fmap_CONS", 2214``!x:'a y:'b l. fmap ((x,y)::l) = fmap l |+ (x,y)``, 2215SRW_TAC [] [fmap, FUPDATE_LIST_SNOC, FAPPLY_FUPDATE_THM]); 2216 2217val o_f_FUPDATE_ALT = maybe_thm ("o_f_FUPDATE_ALT", 2218``!f:'b->'c fm:'a|->'b k v. f o_f (fm |+ (k,v)) = (f o_f fm) |+ (k,f v)``, 2219REPEAT GEN_TAC THEN 2220REWRITE_TAC [fmap_EXT, FDOM_o_f, FDOM_FUPDATE] THEN 2221GEN_TAC THEN REWRITE_TAC [IN_INSERT, FAPPLY_FUPDATE_THM, o_f_FAPPLY] THEN 2222ASM_REWRITE_TAC [o_f_FUPDATE, FAPPLY_FUPDATE_THM] THEN 2223Cases_on `x = k` THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN 2224`x IN FDOM (fm \\ k)` by METIS_TAC [FDOM_DOMSUB, IN_DELETE] THEN 2225IMP_RES_TAC o_f_FAPPLY THEN ASM_REWRITE_TAC [DOMSUB_FAPPLY_THM] THEN 2226`k <> x` by METIS_TAC [] THEN AR); 2227 2228val o_f_fmap = store_thm ("o_f_fmap", 2229``!f:'b->'c l:('a#'b)list. f o_f fmap l = fmap (MAP (AP_SND f) l)``, 2230GEN_TAC THEN Induct THENL 2231[SRW_TAC [] [fmap, FUPDATE_LIST_THM] 2232,P_PGEN_TAC ``y:'a, z:'b`` THEN 2233 RW_TAC bool_ss [MAP, fmap_CONS, AP_SND, o_f_FUPDATE_ALT] 2234]); 2235 2236(* ******************************************************************* *) 2237(* Test for a bt with no spurious nodes, as should be invariably the *) 2238(* case, and justify quicker bt_to_orl for bt's passing the test, *) 2239(* makes exactly n - 1 comparisons in passing a tree with n nodes. *) 2240(* (A carbon copy of what is done with bt_to_ol in enumeralTheory.) *) 2241(* ******************************************************************* *) 2242 2243val ORL_bt_lb_ub = Define 2244`(ORL_bt_lb_ub cmp lb (nt:('a#'b) bt) ub = (apto cmp lb ub = LESS)) /\ 2245 (ORL_bt_lb_ub cmp lb (node l (x,y) r) ub = ORL_bt_lb_ub cmp lb l x /\ 2246 ORL_bt_lb_ub cmp x r ub)`; 2247 2248val ORL_bt_lb = Define 2249`(ORL_bt_lb cmp lb (nt:('a#'b) bt) = T) /\ 2250 (ORL_bt_lb cmp lb (node l (x,y) r) = ORL_bt_lb_ub cmp lb l x /\ 2251 ORL_bt_lb cmp x r)`; 2252 2253val ORL_bt_ub = Define 2254`(ORL_bt_ub cmp (nt:('a#'b) bt) ub = T) /\ 2255 (ORL_bt_ub cmp (node l (x,y) r) ub = ORL_bt_ub cmp l x /\ 2256 ORL_bt_lb_ub cmp x r ub)`; 2257 2258val ORL_bt = Define 2259`(ORL_bt cmp (nt:('a#'b) bt) = T) /\ 2260 (ORL_bt cmp (node l (x,y) r) = ORL_bt_ub cmp l x /\ ORL_bt_lb cmp x r)`; 2261 2262val ORL_bt_lb_ub_lem = maybe_thm ("ORL_bt_lb_ub_lem", 2263``!cmp t lb ub. ORL_bt_lb_ub cmp lb t ub ==> (apto cmp lb ub = LESS)``, 2264GEN_TAC THEN Induct THENL 2265[SRW_TAC [] [ORL_bt_lb_ub] 2266,P_PGEN_TAC ``x:'a,y:'b`` THEN 2267 SRW_TAC [] [ORL_bt_lb_ub] THEN METIS_TAC [totoLLtrans] 2268]); 2269 2270val ORL_bt_lb_ub_thm = maybe_thm ("ORL_bt_lb_ub_thm", 2271``!cmp t:('a#'b) bt lb ub. ORL_bt_lb_ub cmp lb t ub ==> 2272 (bt_to_orl_lb_ub cmp lb t ub = bt_to_list t)``, 2273GEN_TAC THEN Induct THENL 2274[REWRITE_TAC [bt_to_orl_lb_ub, bt_to_list] 2275,P_PGEN_TAC ``a:'a,b:'b`` THEN 2276 SRW_TAC [] [ORL_bt_lb_ub, bt_to_orl_lb_ub, bt_to_list] THEN 2277 METIS_TAC [ORL_bt_lb_ub_lem] 2278]); 2279 2280val ORL_bt_lb_thm = maybe_thm ("ORL_bt_lb_thm", 2281``!cmp t:('a#'b) bt lb. ORL_bt_lb cmp lb t ==> 2282 (bt_to_orl_lb cmp lb t = bt_to_list t)``, 2283GEN_TAC THEN Induct THENL 2284[REWRITE_TAC [bt_to_orl_lb, bt_to_list] 2285,P_PGEN_TAC ``a:'a,b:'b`` THEN 2286 SRW_TAC [] [ORL_bt_lb, bt_to_orl_lb, ORL_bt_lb_ub_thm, bt_to_list] THEN 2287 METIS_TAC [ORL_bt_lb_ub_lem] 2288]); 2289 2290val ORL_bt_ub_thm = maybe_thm ("ORL_bt_ub_thm", 2291``!cmp t:('a#'b) bt ub. ORL_bt_ub cmp t ub ==> 2292 (bt_to_orl_ub cmp t ub = bt_to_list t)``, 2293GEN_TAC THEN Induct THENL 2294[REWRITE_TAC [bt_to_orl_ub, bt_to_list] 2295,P_PGEN_TAC ``a:'a,b:'b`` THEN 2296 SRW_TAC [] [ORL_bt_ub, bt_to_orl_ub, ORL_bt_lb_ub_thm, bt_to_list] THEN 2297 METIS_TAC [ORL_bt_lb_ub_lem] 2298]); 2299 2300val ORL_bt_thm = maybe_thm ("ORL_bt_thm", 2301``!cmp t:('a#'b) bt. ORL_bt cmp t ==> (bt_to_orl cmp t = bt_to_list t)``, 2302GEN_TAC THEN Induct THENL (* really Cases, but need !a to use P_PGEN_TAC *) 2303[REWRITE_TAC [bt_to_orl, bt_to_list] 2304,P_PGEN_TAC ``a:'a,b:'b`` THEN SRW_TAC [] 2305 [ORL_bt, bt_to_orl, ORL_bt_lb_thm, ORL_bt_ub_thm, bt_to_list]]); 2306 2307val better_bt_to_orl = store_thm ("better_bt_to_orl", 2308``!cmp t:('a#'b) bt. bt_to_orl cmp t = if ORL_bt cmp t then bt_to_list_ac t [] 2309 else bt_to_orl_ac cmp t []``, 2310METIS_TAC [ORL_bt_thm, bt_to_list_thm, bt_to_orl_thm]); 2311 2312(* ****************************************************************** *) 2313(* Theorems to support FUPDATE_CONV, for both FMAPAL and fmap terms. *) 2314(* *** NOTE: FUPDATE_CONV will fail if it is asked to extend the *** *) 2315(* *** domain, that is convert f |+ (x,y) where x NOTIN FDOM f, *** *) 2316(* *** which could not be done efficiently for a FMAPAL, and *** *) 2317(* *** has no clearly best implementation for fmap [ ... ]'s. *** *) 2318(* ****************************************************************** *) 2319 2320(* Making list_rplacv_cn exit directly on its error condition (not finding 2321 x) and use a continuation otherwise seems like reasonable programming; 2322 however, encoding the error condition as a return of the empty list 2323 (since that can never be a successful answer) is a hack, into which I 2324 am lured to save the bother of using an option type. *) 2325 2326val list_rplacv_cn = Define 2327`(list_rplacv_cn (x:'a,y:'b) [] (cn:('a#'b)list -> ('a#'b)list) = []) /\ 2328 (list_rplacv_cn (x,y) ((w,z)::l) cn = 2329 if x = w then cn ((x,y)::l) 2330 else list_rplacv_cn (x,y) l (\m. cn ((w,z)::m)))`; 2331 2332val fmap_FDOM_rec = store_thm ("fmap_FDOM_rec", 2333``(!x:'a. x IN FDOM (fmap ([]:('a#'b)list)) = F) /\ 2334 (!x w:'a z:'b l. x IN FDOM (fmap ((w,z)::l)) = 2335 (x = w) \/ x IN FDOM (fmap l))``, 2336SRW_TAC [] [fmap_FDOM]); 2337 2338val list_rplacv_NIL = maybe_thm ("list_rplacv_NIL", 2339``!x:'a y:'b l cn. (!m. cn m <> []) ==> 2340 ((list_rplacv_cn (x,y) l cn = []) <=> x NOTIN FDOM (fmap l))``, 2341GEN_TAC THEN GEN_TAC THEN Induct THENL 2342[RW_TAC (srw_ss()) [list_rplacv_cn, fmap_FDOM_rec] 2343,P_PGEN_TAC ``w:'a,z:'b`` THEN 2344 RW_TAC (srw_ss()) [list_rplacv_cn, fmap_FDOM_rec] 2345]); 2346 2347val list_rplacv_cont_lem = maybe_thm ("list_rplacv_cont_lem", 2348``!x:'a y:'b l cn cn'. list_rplacv_cn (x,y) l cn <> [] ==> 2349 (list_rplacv_cn (x,y) l (cn' o cn) = 2350 cn' (list_rplacv_cn (x,y) l cn))``, 2351GEN_TAC THEN GEN_TAC THEN Induct THENL 2352[SRW_TAC [] [list_rplacv_cn] 2353,P_PGEN_TAC ``w:'a,z:'b`` THEN 2354 SRW_TAC [] [list_rplacv_cn] THEN RES_TAC THEN 2355 Q.SUBGOAL_THEN `(\m. cn' (cn ((w,z)::m))) = (cn' o (\m. cn ((w,z)::m)))` 2356 (ASM_REWRITE_TAC o ulist) THEN 2357 CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] [] 2358]); 2359 2360val bool_lem = prove (``!P Q.(if ~P then ~P else P /\ Q) <=> P ==> Q``, 2361RW_TAC bool_ss [IMP_DISJ_THM]); 2362 2363val list_rplacv_thm = store_thm ("list_rplacv_thm", 2364``!x:'a y:'b l. 2365let ans = list_rplacv_cn (x,y) l (\m.m) 2366in if ans = [] then x NOTIN FDOM (fmap l) 2367 else x IN FDOM (fmap l) /\ (fmap l |+ (x,y) = fmap ans)``, 2368GEN_TAC THEN GEN_TAC THEN REWRITE_TAC [LET_THM] THEN BETA_TAC THEN 2369Induct THENL 2370[SRW_TAC [] [list_rplacv_cn, fmap_FDOM, MAP] 2371,P_PGEN_TAC ``w:'a,z:'b`` THEN 2372 REWRITE_TAC [list_rplacv_cn, fmap_FDOM_rec] THEN Cases_on `x = w` THEN AR THENL 2373 [SRW_TAC [] [fmap_CONS] 2374 ,`!m.(\m. (\m.m) ((w,z)::m)) m <> []` by SRW_TAC [] [] THEN 2375 IMP_RES_THEN (REWRITE_TAC o ulist) list_rplacv_NIL THEN 2376 REWRITE_TAC [bool_lem] THEN DISCH_TAC THEN 2377 `(fmap (list_rplacv_cn (x,y) l (\m.m)) = fmap l |+ (x,y)) /\ 2378 list_rplacv_cn (x,y) l (\m.m) <> []` by METIS_TAC [] THEN 2379 Q.SUBGOAL_THEN `(\m. (\m.m)((w,z)::m)) = (\m. ((w,z)::m)) o (\m.m)` SUBST1_TAC 2380 THEN1 (CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] []) THEN 2381 IMP_RES_THEN (REWRITE_TAC o ulist) list_rplacv_cont_lem THEN BETA_TAC THEN 2382 ASM_REWRITE_TAC [fmap_CONS] THEN MATCH_MP_TAC FUPDATE_COMMUTES THEN 2383 CONV_TAC (RAND_CONV (REWR_CONV EQ_SYM_EQ)) THEN AR 2384]]); 2385 2386(* *************************************************************** *) 2387(* Now to treat similarly terms of the form *) 2388(* FMAPAL cmp (node ... ) |+ (x,y), with similar provision that *) 2389(* domain will not be extended. *) 2390(* *************************************************************** *) 2391 2392val bt_rplacv_cn = Define 2393`(bt_rplacv_cn cmp (x:'a,y:'b) nt (cn:('a#'b)bt -> ('a#'b)bt) = nt) /\ 2394 (bt_rplacv_cn cmp (x,y) (node l (w,z) r) cn = 2395 case apto cmp x w of 2396 LESS => bt_rplacv_cn cmp (x,y) l (\m. cn (node m (w,z) r)) 2397 | EQUAL => cn (node l (x,y) r) 2398 | GREATER => bt_rplacv_cn cmp (x,y) r (\m. cn (node l (w,z) m)))`; 2399 2400(* FMAPAL_FDOM_THM (corresp. to fmap_FDOM_rec) has already been proved. *) 2401 2402val bt_rplacv_nt = maybe_thm ("bt_rplacv_nt", 2403``!cmp x:'a y:'b t cn. (!m. cn m <> nt) ==> 2404 ((bt_rplacv_cn cmp (x,y) t cn = nt) <=> x NOTIN FDOM (FMAPAL cmp t))``, 2405GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN Induct THENL 2406[RW_TAC (srw_ss()) [bt_rplacv_cn, FMAPAL_FDOM_THM] 2407,P_PGEN_TAC ``w:'a,z:'b`` THEN 2408 RW_TAC (srw_ss()) [bt_rplacv_cn, FMAPAL_FDOM_THM] THEN 2409 Cases_on `apto cmp x w` THEN SRW_TAC [] [] 2410]); 2411 2412val bt_rplacv_cont_lem = maybe_thm ("bt_rplacv_cont_lem", 2413``!cmp x:'a y:'b t cn cn'. bt_rplacv_cn cmp (x,y) t cn <> nt ==> 2414 (bt_rplacv_cn cmp (x,y) t (cn' o cn) = 2415 cn' (bt_rplacv_cn cmp (x,y) t cn))``, 2416GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN Induct THENL 2417[SRW_TAC [] [bt_rplacv_cn] 2418,P_PGEN_TAC ``w:'a,z:'b`` THEN Cases_on `apto cmp x w` THEN 2419 SRW_TAC [] [bt_rplacv_cn] THEN RES_TAC THENL 2420 [Q.SUBGOAL_THEN `(\m. cn' (cn (node m (w,z) t'))) = 2421 (cn' o (\m. cn (node m (w,z) t')))` 2422 (ASM_REWRITE_TAC o ulist) 2423 ,Q.SUBGOAL_THEN `(\m. cn' (cn (node t (w,z) m))) = 2424 (cn' o (\m. cn (node t (w,z) m)))` 2425 (ASM_REWRITE_TAC o ulist) 2426 ] THEN 2427 CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] [] 2428]); 2429 2430(* FUNION_FUPDATE_1 = 2431 |- !f g x y. f |+ (x,y) FUNION g = (f FUNION g) |+ (x,y) 2432 FUNION_FUPDATE_2 = 2433 (|- !f g x y. f FUNION g |+ (x,y) = 2434 if x IN FDOM f then f FUNION g else (f FUNION g) |+ (x,y) *) 2435 2436val FUNION_FUPDATE_HALF_2 = maybe_thm ("FUNION_FUPDATE_HALF_2", 2437``!f:'a|->'b g x y. x NOTIN FDOM f ==> 2438 ((f FUNION g) |+ (x,y) = f FUNION g |+ (x,y))``, 2439METIS_TAC [FUNION_FUPDATE_2]); 2440 2441val bt_rplacv_thm = store_thm ("bt_rplacv_thm", 2442``!cmp x:'a y:'b t. 2443let ans = bt_rplacv_cn cmp (x,y) t (\m.m) 2444in if ans = nt then x NOTIN FDOM (FMAPAL cmp t) 2445else x IN FDOM (FMAPAL cmp t) /\ (FMAPAL cmp t |+ (x,y) = FMAPAL cmp ans)``, 2446GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN REWRITE_TAC [LET_THM] THEN BETA_TAC THEN 2447Induct THENL 2448[SRW_TAC [] [bt_rplacv_cn, FMAPAL_FDOM_THM] 2449,P_PGEN_TAC ``w:'a,z:'b`` THEN 2450 REWRITE_TAC [bt_rplacv_cn, FMAPAL_FDOM_THM] THEN 2451 Cases_on `apto cmp x w` THEN ASM_REWRITE_TAC [cpn_case_def] THENL 2452 [`!m.(\m. (\m.m) (node m (w,z) t')) m <> nt` by SRW_TAC [] [] THEN 2453 IMP_RES_THEN (REWRITE_TAC o ulist) bt_rplacv_nt THEN 2454 REWRITE_TAC [bool_lem] THEN DISCH_TAC THEN 2455 `(FMAPAL cmp (bt_rplacv_cn cmp (x,y) t (\m.m)) = FMAPAL cmp t |+ (x,y)) /\ 2456 bt_rplacv_cn cmp (x,y) t (\m.m) <> nt` by METIS_TAC [] THEN 2457 Q.SUBGOAL_THEN 2458 `(\m. (\m.m)(node m (w,z) t')) = (\m. (node m (w,z) t')) o (\m.m)` SUBST1_TAC 2459 THEN1 (CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] []) THEN 2460 IMP_RES_THEN (REWRITE_TAC o ulist) bt_rplacv_cont_lem THEN BETA_TAC THEN 2461 ASM_REWRITE_TAC [bt_to_fmap, DRESTRICT_FUPDATE] THEN 2462 Q.SUBGOAL_THEN `x IN {z | apto cmp z w = LESS}` (REWRITE_TAC o ulist) 2463 THEN1 (CONV_TAC SET_SPEC_CONV THEN AR) THEN 2464 REWRITE_TAC [FUNION_FUPDATE_1] 2465 ,SRW_TAC [] [bt_to_fmap] THEN 2466 ONCE_REWRITE_TAC [GSYM FUNION_FUPDATE_1] THEN 2467 Q.SUBGOAL_THEN 2468 `x NOTIN FDOM (DRESTRICT (FMAPAL cmp t) {y | apto cmp y w = LESS})` 2469 (REWRITE_TAC o ulist o MATCH_MP FUNION_FUPDATE_HALF_2) THENL 2470 [REWRITE_TAC [FDOM_DRESTRICT, IN_INTER, DE_MORGAN_THM] THEN 2471 DISJ2_TAC THEN CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN SRW_TAC [] [] 2472 ,IMP_RES_TAC toto_equal_imp_eq THEN ASM_REWRITE_TAC [FUPDATE_EQ] 2473 ] 2474 ,`!m.(\m. (\m.m) (node t (w,z) m)) m <> nt` by SRW_TAC [] [] THEN 2475 IMP_RES_THEN (REWRITE_TAC o ulist) bt_rplacv_nt THEN 2476 REWRITE_TAC [bool_lem] THEN DISCH_TAC THEN 2477 `(FMAPAL cmp (bt_rplacv_cn cmp (x,y) t' (\m.m)) = FMAPAL cmp t' |+ (x,y)) /\ 2478 bt_rplacv_cn cmp (x,y) t' (\m.m) <> nt` by METIS_TAC [] THEN 2479 Q.SUBGOAL_THEN 2480 `(\m. (\m.m) (node t (w,z) m)) = (\m. (node t (w,z) m)) o (\m.m)` SUBST1_TAC 2481 THEN1 (CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] []) THEN 2482 IMP_RES_THEN (REWRITE_TAC o ulist) bt_rplacv_cont_lem THEN BETA_TAC THEN 2483 ASM_REWRITE_TAC [bt_to_fmap, DRESTRICT_FUPDATE] THEN 2484 Q.SUBGOAL_THEN `x IN {z | apto cmp w z = LESS}` (REWRITE_TAC o ulist) 2485 THEN1 (CONV_TAC SET_SPEC_CONV THEN ASM_REWRITE_TAC [GSYM toto_antisym]) THEN 2486 Q.SUBGOAL_THEN 2487 `x NOTIN FDOM (DRESTRICT (FMAPAL cmp t) {y | apto cmp y w = LESS} FUNION 2488 FEMPTY |+ (w,z))` 2489 (REWRITE_TAC o ulist o MATCH_MP FUNION_FUPDATE_HALF_2) THEN 2490 REWRITE_TAC [FDOM_FUNION, IN_UNION, FDOM_DRESTRICT, IN_INTER, DE_MORGAN_THM, 2491 FDOM_FUPDATE, IN_INSERT, FDOM_FEMPTY, NOT_IN_EMPTY] THEN 2492 CONJ_TAC THENL 2493 [DISJ2_TAC THEN CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN SRW_TAC [] [] 2494 ,IMP_RES_TAC (CONJUNCT2 toto_glneq) 2495]]]); 2496 2497(* ***************************************************************** *) 2498(* Theorems to support FUN_fmap_CONV *) 2499(* ***************************************************************** *) 2500 2501val FST_PAIR_ID = prove (``!f:'a->'b. FST o (\x. (x,f x)) = I``, 2502GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN SRW_TAC [][combinTheory.o_THM]); 2503 2504val FUN_fmap_thm = store_thm ("FUN_fmap_thm", 2505``!f:'a->'b l:'a list. fmap (MAP (\x. (x, f x)) l) = FUN_FMAP f (set l)``, 2506GEN_TAC THEN Induct THENL 2507[RW_TAC (srw_ss()) [LIST_TO_SET_THM, FUN_FMAP_DEF, fmap_NIL] 2508,RW_TAC (srw_ss()) [LIST_TO_SET_THM, FUN_FMAP_DEF, fmap_CONS, fmap_EXT] THENL 2509 [REWRITE_TAC [FAPPLY_FUPDATE] 2510 ,REWRITE_TAC [FAPPLY_FUPDATE_THM] THEN 2511 Cases_on `x = h` THEN AR THEN 2512 `FINITE (set l)` by MATCH_ACCEPT_TAC FINITE_LIST_TO_SET THEN 2513 `x IN set l` by ASM_REWRITE_TAC [] THEN 2514 IMP_RES_TAC FUN_FMAP_DEF THEN AR 2515]]); 2516 2517(* ******************* Theorem to support fmap_TO_ORWL ********************* *) 2518 2519val fmap_ORWL_thm = store_thm ("fmap_ORWL_thm", 2520``!cmp l:('a#'b)list. ORWL cmp (fmap l) (incr_sort cmp l)``, 2521REWRITE_TAC [ORWL, incr_sort_fmap, incr_sort_ORL]); 2522 2523val _ = export_theory (); 2524