1(* ====================================================================== 2 THEORY: finite_map 3 FILE: finite_mapScript.sml 4 DESCRIPTION: A theory of finite maps 5 6 AUTHOR: Graham Collins and Donald Syme 7 8 ====================================================================== 9 There is little documentation in this file but a discussion of this 10 theory is available as: 11 12 @inproceedings{P-Collins-FMAP, 13 author = {Graham Collins and Donald Syme}, 14 editor = {E. Thomas Schubert and Phillip J. Windley 15 and James Alves-Foss}, 16 booktitle={Higher Order Logic Theorem Proving and its Applications} 17 publisher = {Springer-Verlag}, 18 series = {Lecture Notes in Computer Science}, 19 title = {A Theory of Finite Maps}, 20 volume = {971}, 21 year = {1995}, 22 pages = {122--137} 23 } 24 25 Updated for HOL4 in 2002 by Michael Norrish. 26 27 ===================================================================== *) 28 29open HolKernel Parse boolLib IndDefLib numLib pred_setTheory 30 sumTheory pairTheory BasicProvers bossLib metisLib simpLib; 31 32local open pred_setLib listTheory rich_listTheory in end 33 34val _ = new_theory "finite_map"; 35 36val _ = ParseExtras.temp_tight_equality() 37 38(*---------------------------------------------------------------------------*) 39(* Special notation. fmap application is set at the same level as function *) 40(* application, meaning that *) 41(* *) 42(* * SOME (f ' x) prints as SOME (f ' x) *) 43(* * (f x) ' y prints as f x ' y *) 44(* * (f ' x) y prints as f ' x y *) 45(* * f ' (x y) prints as f ' (x y) *) 46(* *) 47(* I think this is clearly best. *) 48(*---------------------------------------------------------------------------*) 49 50val _ = set_fixity "'" (Infixl 2000); (* fmap application *) 51 52val _ = set_fixity "|+" (Infixl 600); (* fmap update *) 53val _ = set_fixity "|++" (Infixl 500); (* iterated update *) 54 55 56(*--------------------------------------------------------------------------- 57 Definition of a finite map 58 59 The representation is the type 'a -> ('b + one) where only a finite 60 number of the 'a map to a 'b and the rest map to one. We define a 61 notion of finiteness inductively. 62 --------------------------------------------------------------------------- *) 63 64val (rules,ind,cases) = 65 Hol_reln `is_fmap (\a. INR one) 66 /\ (!f a b. is_fmap f ==> is_fmap (\x. if x=a then INL b else f x))`; 67 68 69val rule_list as [is_fmap_empty, is_fmap_update] = CONJUNCTS rules; 70 71val strong_ind = derive_strong_induction(rules, ind); 72 73 74(*--------------------------------------------------------------------------- 75 Existence theorem; type definition 76 ---------------------------------------------------------------------------*) 77 78val EXISTENCE_THM = Q.prove 79(`?x:'a -> 'b + one. is_fmap x`, 80EXISTS_TAC (Term`\x:'a. (INR one):'b + one`) 81 THEN REWRITE_TAC [is_fmap_empty]); 82 83val fmap_TY_DEF = new_type_definition("fmap", EXISTENCE_THM); 84 85val _ = add_infix_type 86 {Prec = 50, 87 ParseName = SOME "|->", 88 Assoc = RIGHT, 89 Name = "fmap"}; 90val _ = TeX_notation {hol = "|->", TeX = ("\\HOLTokenMapto{}", 1)} 91 92(* --------------------------------------------------------------------- *) 93(* Define bijections *) 94(* --------------------------------------------------------------------- *) 95 96val fmap_ISO_DEF = 97 define_new_type_bijections 98 {name = "fmap_ISO_DEF", 99 ABS = "fmap_ABS", 100 REP = "fmap_REP", 101 tyax = fmap_TY_DEF}; 102 103(* --------------------------------------------------------------------- *) 104(* Prove that REP is one-to-one. *) 105(* --------------------------------------------------------------------- *) 106 107val fmap_REP_11 = prove_rep_fn_one_one fmap_ISO_DEF 108val fmap_REP_onto = prove_rep_fn_onto fmap_ISO_DEF 109val fmap_ABS_11 = prove_abs_fn_one_one fmap_ISO_DEF 110val fmap_ABS_onto = prove_abs_fn_onto fmap_ISO_DEF; 111 112val (fmap_ABS_REP_THM,fmap_REP_ABS_THM) = 113 let val thms = CONJUNCTS fmap_ISO_DEF 114 val [t1,t2] = map (GEN_ALL o SYM o SPEC_ALL) thms 115 in (t1,t2) 116 end; 117 118 119(*--------------------------------------------------------------------------- 120 CANCELLATION THEOREMS 121 ---------------------------------------------------------------------------*) 122 123val is_fmap_REP = Q.prove 124(`!f:'a |-> 'b. is_fmap (fmap_REP f)`, 125 REWRITE_TAC [fmap_REP_onto] 126 THEN GEN_TAC THEN Q.EXISTS_TAC `f` 127 THEN REWRITE_TAC [fmap_REP_11]); 128 129val REP_ABS_empty = Q.prove 130(`fmap_REP (fmap_ABS ((\a. INR one):'a -> 'b + one)) = \a. INR one`, 131 REWRITE_TAC [fmap_REP_ABS_THM] 132 THEN REWRITE_TAC [is_fmap_empty]); 133 134val REP_ABS_update = Q.prove 135(`!(f:'a |-> 'b) x y. 136 fmap_REP (fmap_ABS (\a. if a=x then INL y else fmap_REP f a)) 137 = 138 \a. if a=x then INL y else fmap_REP f a`, 139 REPEAT GEN_TAC 140 THEN REWRITE_TAC [fmap_REP_ABS_THM] 141 THEN MATCH_MP_TAC is_fmap_update 142 THEN REWRITE_TAC [is_fmap_REP]); 143 144val is_fmap_REP_ABS = Q.prove 145(`!f:'a -> 'b + one. is_fmap f ==> (fmap_REP (fmap_ABS f) = f)`, 146 REPEAT STRIP_TAC 147 THEN REWRITE_TAC [fmap_REP_ABS_THM] 148 THEN ASM_REWRITE_TAC []); 149 150 151(*--------------------------------------------------------------------------- 152 DEFINITIONS OF UPDATE, EMPTY, APPLY and DOMAIN 153 ---------------------------------------------------------------------------*) 154 155val FUPDATE_DEF = Q.new_definition 156("FUPDATE_DEF", 157 `FUPDATE (f:'a |-> 'b) (x,y) 158 = fmap_ABS (\a. if a=x then INL y else fmap_REP f a)`); 159 160val _ = overload_on ("|+", ``FUPDATE``); 161 162val FEMPTY_DEF = Q.new_definition 163("FEMPTY_DEF", 164 `(FEMPTY:'a |-> 'b) = fmap_ABS (\a. INR one)`); 165 166val FAPPLY_DEF = Q.new_definition 167("FAPPLY_DEF", 168 `FAPPLY (f:'a |-> 'b) x = OUTL (fmap_REP f x)`); 169 170val _ = overload_on ("'", ``FAPPLY``); 171 172val FDOM_DEF = Q.new_definition 173("FDOM_DEF", 174 `FDOM (f:'a |-> 'b) x = ISL (fmap_REP f x)`); 175 176val update_rep = Term`\(f:'a->'b+one) x y. \a. if a=x then INL y else f a`; 177 178val empty_rep = Term`(\a. INR one):'a -> 'b + one`; 179 180 181(*--------------------------------------------------------------------------- 182 Now some theorems 183 --------------------------------------------------------------------------- *) 184 185val FAPPLY_FUPDATE = Q.store_thm ("FAPPLY_FUPDATE", 186`!(f:'a |-> 'b) x y. FAPPLY (FUPDATE f (x,y)) x = y`, 187 REWRITE_TAC [FUPDATE_DEF, FAPPLY_DEF] 188 THEN REPEAT GEN_TAC 189 THEN REWRITE_TAC [REP_ABS_update] THEN BETA_TAC 190 THEN REWRITE_TAC [sumTheory.OUTL]); 191 192val _ = export_rewrites ["FAPPLY_FUPDATE"] 193 194val NOT_EQ_FAPPLY = Q.store_thm ("NOT_EQ_FAPPLY", 195`!(f:'a|-> 'b) a x y . ~(a=x) ==> (FAPPLY (FUPDATE f (x,y)) a = FAPPLY f a)`, 196REPEAT STRIP_TAC 197 THEN REWRITE_TAC [FUPDATE_DEF, FAPPLY_DEF, REP_ABS_update] THEN BETA_TAC 198 THEN ASM_REWRITE_TAC []); 199 200val update_commutes_rep = (BETA_RULE o BETA_RULE) (Q.prove 201(`!(f:'a -> 'b + one) a b c d. 202 ~(a = c) 203 ==> 204 (^update_rep (^update_rep f a b) c d = ^update_rep (^update_rep f c d) a b)`, 205REPEAT STRIP_TAC THEN BETA_TAC 206 THEN MATCH_MP_TAC EQ_EXT 207 THEN GEN_TAC 208 THEN Q.ASM_CASES_TAC `x = a` THEN BETA_TAC 209 THEN ASM_REWRITE_TAC [])); 210 211 212val FUPDATE_COMMUTES = Q.store_thm ("FUPDATE_COMMUTES", 213`!(f:'a |-> 'b) a b c d. 214 ~(a = c) 215 ==> 216 (FUPDATE (FUPDATE f (a,b)) (c,d) = FUPDATE (FUPDATE f (c,d)) (a,b))`, 217REPEAT STRIP_TAC 218 THEN REWRITE_TAC [FUPDATE_DEF, REP_ABS_update] THEN BETA_TAC 219 THEN AP_TERM_TAC 220 THEN MATCH_MP_TAC EQ_EXT 221 THEN GEN_TAC 222 THEN Q.ASM_CASES_TAC `x = a` THEN BETA_TAC 223 THEN ASM_REWRITE_TAC []); 224 225val update_same_rep = (BETA_RULE o BETA_RULE) (Q.prove 226(`!(f:'a -> 'b+one) a b c. 227 ^update_rep (^update_rep f a b) a c = ^update_rep f a c`, 228BETA_TAC THEN REPEAT GEN_TAC 229 THEN MATCH_MP_TAC EQ_EXT 230 THEN GEN_TAC 231 THEN Q.ASM_CASES_TAC `x = a` THEN BETA_TAC 232 THEN ASM_REWRITE_TAC [])); 233 234val FUPDATE_EQ = Q.store_thm ("FUPDATE_EQ", 235`!(f:'a |-> 'b) a b c. FUPDATE (FUPDATE f (a,b)) (a,c) = FUPDATE f (a,c)`, 236REPEAT STRIP_TAC 237 THEN REWRITE_TAC [FUPDATE_DEF, REP_ABS_update] THEN BETA_TAC 238 THEN AP_TERM_TAC 239 THEN MATCH_MP_TAC EQ_EXT 240 THEN GEN_TAC 241 THEN Q.ASM_CASES_TAC `x = a` THEN BETA_TAC 242 THEN ASM_REWRITE_TAC []); 243 244val _ = export_rewrites ["FUPDATE_EQ"] 245 246val lemma1 = Q.prove 247(`~((ISL :'b + one -> bool) ((INR :one -> 'b + one) one))`, 248 REWRITE_TAC [sumTheory.ISL]); 249 250val FDOM_FEMPTY = Q.store_thm ("FDOM_FEMPTY", 251`FDOM (FEMPTY:'a |-> 'b) = {}`, 252REWRITE_TAC [EXTENSION, NOT_IN_EMPTY] THEN 253REWRITE_TAC [SPECIFICATION, FDOM_DEF, FEMPTY_DEF, REP_ABS_empty, 254 sumTheory.ISL]); 255 256val _ = export_rewrites ["FDOM_FEMPTY"] 257 258val dom_update_rep = BETA_RULE (Q.prove 259(`!f a b x. ISL(^update_rep (f:'a -> 'b+one ) a b x) = ((x=a) \/ ISL (f x))`, 260REPEAT GEN_TAC THEN BETA_TAC 261 THEN Q.ASM_CASES_TAC `x = a` 262 THEN ASM_REWRITE_TAC [sumTheory.ISL])); 263 264val FDOM_FUPDATE = Q.store_thm( 265 "FDOM_FUPDATE", 266 `!f a b. FDOM (FUPDATE (f:'a |-> 'b) (a,b)) = a INSERT FDOM f`, 267 REPEAT GEN_TAC THEN 268 REWRITE_TAC [EXTENSION, IN_INSERT] THEN 269 REWRITE_TAC [SPECIFICATION, FDOM_DEF,FUPDATE_DEF, REP_ABS_update] THEN 270 BETA_TAC THEN GEN_TAC THEN Q.ASM_CASES_TAC `x = a` THEN 271 ASM_REWRITE_TAC [sumTheory.ISL]); 272 273val _ = export_rewrites ["FDOM_FUPDATE"] 274 275val FAPPLY_FUPDATE_THM = Q.store_thm("FAPPLY_FUPDATE_THM", 276`!(f:'a |-> 'b) a b x. 277 FAPPLY(FUPDATE f (a,b)) x = if x=a then b else FAPPLY f x`, 278REPEAT STRIP_TAC 279 THEN COND_CASES_TAC 280 THEN ASM_REWRITE_TAC [FAPPLY_FUPDATE] 281 THEN IMP_RES_TAC NOT_EQ_FAPPLY 282 THEN ASM_REWRITE_TAC []); 283 284val not_eq_empty_update_rep = BETA_RULE (Q.prove 285(`!(f:'a -> 'b + one) a b. ~(^empty_rep = ^update_rep f a b)`, 286REPEAT GEN_TAC THEN BETA_TAC 287 THEN CONV_TAC (DEPTH_CONV FUN_EQ_CONV) 288 THEN CONV_TAC NOT_FORALL_CONV 289 THEN Q.EXISTS_TAC `a` THEN BETA_TAC 290 THEN DISCH_THEN (fn th => REWRITE_TAC [REWRITE_RULE [sumTheory.ISL] 291 (REWRITE_RULE [th] lemma1)]))); 292 293val fmap_EQ_1 = Q.prove 294(`!(f:'a |-> 'b) g. (f=g) ==> (FDOM f = FDOM g) /\ (FAPPLY f = FAPPLY g)`, 295REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []); 296 297val NOT_EQ_FEMPTY_FUPDATE = Q.store_thm ( 298 "NOT_EQ_FEMPTY_FUPDATE", 299 `!(f:'a |-> 'b) a b. ~(FEMPTY = FUPDATE f (a,b))`, 300 REPEAT GEN_TAC THEN 301 DISCH_THEN (MP_TAC o Q.AP_TERM `FDOM`) THEN 302 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE, EXTENSION, EXISTS_OR_THM]); 303 304val _ = export_rewrites ["NOT_EQ_FEMPTY_FUPDATE"] 305 306val FDOM_EQ_FDOM_FUPDATE = Q.store_thm( 307 "FDOM_EQ_FDOM_FUPDATE", 308 `!(f:'a |-> 'b) x. x IN FDOM f ==> (!y. FDOM (FUPDATE f (x,y)) = FDOM f)`, 309 SRW_TAC [][FDOM_FUPDATE, EXTENSION, EQ_IMP_THM] THEN 310 ASM_REWRITE_TAC []); 311 312(*--------------------------------------------------------------------------- 313 Simple induction 314 ---------------------------------------------------------------------------*) 315 316val fmap_SIMPLE_INDUCT = Q.store_thm ("fmap_SIMPLE_INDUCT", 317`!P:('a |-> 'b) -> bool. 318 P FEMPTY /\ 319 (!f. P f ==> !x y. P (FUPDATE f (x,y))) 320 ==> 321 !f. P f`, 322REWRITE_TAC [FUPDATE_DEF, FEMPTY_DEF] 323 THEN GEN_TAC THEN STRIP_TAC THEN GEN_TAC 324 THEN CHOOSE_THEN(CONJUNCTS_THEN2 SUBST1_TAC MP_TAC) (Q.SPEC`f` fmap_ABS_onto) 325 THEN Q.ID_SPEC_TAC `r` 326 THEN HO_MATCH_MP_TAC strong_ind 327 THEN ASM_REWRITE_TAC [] 328 THEN Q.PAT_X_ASSUM `P x` (K ALL_TAC) 329 THEN REPEAT STRIP_TAC THEN RES_TAC 330 THEN IMP_RES_THEN SUBST_ALL_TAC is_fmap_REP_ABS 331 THEN ASM_REWRITE_TAC[]); 332 333val FDOM_EQ_EMPTY = store_thm( 334 "FDOM_EQ_EMPTY", 335 ``!f. (FDOM f = {}) = (f = FEMPTY)``, 336 SIMP_TAC (srw_ss())[EQ_IMP_THM, FDOM_FEMPTY] THEN 337 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN 338 SRW_TAC [][FDOM_FUPDATE, EXTENSION] THEN PROVE_TAC []); 339 340val FDOM_EQ_EMPTY_SYM = save_thm( 341"FDOM_EQ_EMPTY_SYM", 342CONV_RULE (QUANT_CONV (LAND_CONV SYM_CONV)) FDOM_EQ_EMPTY) 343 344val FUPDATE_ABSORB_THM = Q.prove ( 345 `!(f:'a |-> 'b) x y. 346 x IN FDOM f /\ (FAPPLY f x = y) ==> (FUPDATE f (x,y) = f)`, 347 INDUCT_THEN fmap_SIMPLE_INDUCT STRIP_ASSUME_TAC THEN 348 ASM_SIMP_TAC (srw_ss()) [FDOM_FEMPTY, FDOM_FUPDATE, DISJ_IMP_THM, 349 FORALL_AND_THM] THEN 350 REPEAT STRIP_TAC THEN 351 Q.ASM_CASES_TAC `x = x'` THENL [ 352 ASM_SIMP_TAC (srw_ss()) [], 353 ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM] THEN 354 FIRST_ASSUM (FREEZE_THEN (fn th => REWRITE_TAC [th]) o 355 MATCH_MP FUPDATE_COMMUTES) THEN 356 AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 357 ASM_REWRITE_TAC [] 358 ]); 359 360val FDOM_FAPPLY = Q.prove 361(`!(f:'a |-> 'b) x. x IN FDOM f ==> ?y. FAPPLY f x = y`, 362 INDUCT_THEN fmap_SIMPLE_INDUCT ASSUME_TAC THEN 363 SRW_TAC [][FDOM_FUPDATE, FDOM_FEMPTY]); 364 365val FDOM_FUPDATE_ABSORB = Q.prove 366(`!(f:'a |-> 'b) x. x IN FDOM f ==> ?y. FUPDATE f (x,y) = f`, 367 REPEAT STRIP_TAC 368 THEN IMP_RES_TAC FDOM_FAPPLY 369 THEN Q.EXISTS_TAC `y` 370 THEN MATCH_MP_TAC FUPDATE_ABSORB_THM 371 THEN ASM_REWRITE_TAC []); 372 373val FDOM_F_FEMPTY = Q.store_thm 374("FDOM_F_FEMPTY1", 375 `!f:'a |-> 'b. (!a. ~(a IN FDOM f)) = (f = FEMPTY)`, 376 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN 377 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE, NOT_EQ_FEMPTY_FUPDATE, EXISTS_OR_THM]); 378 379val FDOM_FINITE = store_thm( 380 "FDOM_FINITE", 381 ``!fm. FINITE (FDOM fm)``, 382 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN 383 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE]); 384 385val _ = export_rewrites ["FDOM_FINITE"] 386 387(* ===================================================================== *) 388(* Cardinality *) 389(* *) 390(* Define cardinality as the cardinality of the domain of the map *) 391(* ===================================================================== *) 392 393val FCARD_DEF = new_definition("FCARD_DEF", ``FCARD fm = CARD (FDOM fm)``); 394 395(* --------------------------------------------------------------------- *) 396(* Basic cardinality results. *) 397(* --------------------------------------------------------------------- *) 398 399val FCARD_FEMPTY = store_thm( 400 "FCARD_FEMPTY", 401 ``FCARD FEMPTY = 0``, 402 SRW_TAC [][FCARD_DEF, FDOM_FEMPTY]); 403 404val FCARD_FUPDATE = store_thm( 405 "FCARD_FUPDATE", 406 ``!fm a b. FCARD (FUPDATE fm (a, b)) = if a IN FDOM fm then FCARD fm 407 else 1 + FCARD fm``, 408 SRW_TAC [numSimps.ARITH_ss][FCARD_DEF, FDOM_FUPDATE, FDOM_FINITE]); 409 410val FCARD_0_FEMPTY_LEMMA = Q.prove 411(`!f. (FCARD f = 0) ==> (f = FEMPTY)`, 412 INDUCT_THEN fmap_SIMPLE_INDUCT ASSUME_TAC THEN 413 SRW_TAC [numSimps.ARITH_ss][NOT_EQ_FEMPTY_FUPDATE, FCARD_FUPDATE] THEN 414 STRIP_TAC THEN RES_TAC THEN 415 FULL_SIMP_TAC (srw_ss()) [FDOM_FEMPTY]); 416 417val fmap = ``f : 'a |-> 'b`` 418 419val FCARD_0_FEMPTY = Q.store_thm("FCARD_0_FEMPTY", 420`!^fmap. (FCARD f = 0) = (f = FEMPTY)`, 421GEN_TAC THEN EQ_TAC THENL 422[REWRITE_TAC [FCARD_0_FEMPTY_LEMMA], 423 DISCH_THEN (fn th => ASM_REWRITE_TAC [th, FCARD_FEMPTY])]); 424 425val FCARD_SUC = store_thm( 426 "FCARD_SUC", 427 ``!f n. (FCARD f = SUC n) = (?f' x y. ~(x IN FDOM f') /\ (FCARD f' = n) /\ 428 (f = FUPDATE f' (x, y)))``, 429 SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss) 430 [EQ_IMP_THM, FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM, 431 FCARD_FUPDATE] THEN 432 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN 433 SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss)[FCARD_FUPDATE, FCARD_FEMPTY] THEN 434 GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN 435 COND_CASES_TAC THEN STRIP_TAC THENL [ 436 RES_THEN (EVERY_TCL 437 (map Q.X_CHOOSE_THEN [`g`, `u`, `v`]) STRIP_ASSUME_TAC) THEN 438 Q.ASM_CASES_TAC `x = u` THENL [ 439 MAP_EVERY Q.EXISTS_TAC [`g`, `u`, `y`] THEN 440 ASM_SIMP_TAC (srw_ss()) [], 441 MAP_EVERY Q.EXISTS_TAC [`FUPDATE g (x, y)`, `u`, `v`] THEN 442 `x IN FDOM g` by FULL_SIMP_TAC (srw_ss()) [FDOM_FUPDATE] THEN 443 ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, FCARD_FUPDATE, FUPDATE_COMMUTES] 444 ], 445 MAP_EVERY Q.EXISTS_TAC [`f`, `x`, `y`] THEN 446 SRW_TAC [numSimps.ARITH_ss][] 447 ]); 448 449(*--------------------------------------------------------------------------- 450 A more useful induction theorem 451 ---------------------------------------------------------------------------*) 452 453val fmap_INDUCT = Q.store_thm( 454 "fmap_INDUCT", 455 `!P. P FEMPTY /\ 456 (!f. P f ==> !x y. ~(x IN FDOM f) ==> P (FUPDATE f (x,y))) 457 ==> 458 !f. P f`, 459 REPEAT STRIP_TAC THEN Induct_on `FCARD f` THEN REPEAT STRIP_TAC THENL [ 460 PROVE_TAC [FCARD_0_FEMPTY], 461 `?g u w. ~(u IN FDOM g) /\ (f = FUPDATE g (u, w)) /\ (FCARD g = v)` by 462 PROVE_TAC [FCARD_SUC] THEN 463 PROVE_TAC [] 464 ]); 465 466(* splitting a finite map on a key *) 467val FM_PULL_APART = store_thm( 468 "FM_PULL_APART", 469 ``!fm k. k IN FDOM fm ==> ?fm0 v. (fm = fm0 |+ (k, v)) /\ 470 ~(k IN FDOM fm0)``, 471 HO_MATCH_MP_TAC fmap_INDUCT THEN SRW_TAC [][] THENL [ 472 PROVE_TAC [], 473 RES_TAC THEN 474 MAP_EVERY Q.EXISTS_TAC [`fm0 |+ (x,y)`, `v`] THEN 475 `~(k = x)` by PROVE_TAC [] THEN 476 SRW_TAC [][FUPDATE_COMMUTES] 477 ]); 478 479 480(*--------------------------------------------------------------------------- 481 Equality of finite maps 482 ---------------------------------------------------------------------------*) 483 484val update_eq_not_x = Q.prove 485(`!(f:'a |-> 'b) x. 486 ?f'. !y. (FUPDATE f (x,y) = FUPDATE f' (x,y)) /\ ~(x IN FDOM f')`, 487 HO_MATCH_MP_TAC fmap_INDUCT THEN SRW_TAC [][] THENL [ 488 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][], 489 FIRST_X_ASSUM (Q.SPEC_THEN `x'` STRIP_ASSUME_TAC) THEN 490 Cases_on `x = x'` THEN SRW_TAC [][] THENL [ 491 Q.EXISTS_TAC `f` THEN SRW_TAC [][], 492 Q.EXISTS_TAC `f' |+ (x,y)` THEN 493 SRW_TAC [][] THEN METIS_TAC [FUPDATE_COMMUTES] 494 ] 495 ]) 496 497val lemma9 = BETA_RULE (Q.prove 498(`!x y (f1:('a,'b)fmap) f2. 499 (f1 = f2) ==> 500 ((\f.FUPDATE f (x,y)) f1 = (\f. FUPDATE f (x,y)) f2)`, 501 REPEAT STRIP_TAC 502 THEN AP_TERM_TAC 503 THEN ASM_REWRITE_TAC [])); 504 505val NOT_FDOM_FAPPLY_FEMPTY = Q.store_thm 506("NOT_FDOM_FAPPLY_FEMPTY", 507 `!^fmap x. ~(x IN FDOM f) ==> (FAPPLY f x = FAPPLY FEMPTY x)`, 508 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL 509 [REWRITE_TAC [], 510 REPEAT GEN_TAC 511 THEN STRIP_TAC 512 THEN GEN_TAC 513 THEN Q.ASM_CASES_TAC `x' = x` THENL 514 [ASM_REWRITE_TAC [FDOM_FUPDATE, IN_INSERT], 515 IMP_RES_TAC NOT_EQ_FAPPLY 516 THEN ASM_REWRITE_TAC [FDOM_FUPDATE, IN_INSERT]]]); 517 518val fmap_EQ_2 = Q.prove( 519 `!(f:'a |-> 'b) g. (FDOM f = FDOM g) /\ (FAPPLY f = FAPPLY g) ==> (f = g)`, 520 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL [ 521 SRW_TAC [][FDOM_FEMPTY] THEN 522 PROVE_TAC [FCARD_0_FEMPTY, CARD_EMPTY, FCARD_DEF], 523 SRW_TAC [][FDOM_FUPDATE] THEN 524 `?h. (FUPDATE g (x, g ' x) = FUPDATE h (x, g ' x)) /\ ~(x IN FDOM h)` 525 by PROVE_TAC [update_eq_not_x] THEN 526 `x IN FDOM g` by PROVE_TAC [IN_INSERT] THEN 527 `FUPDATE g (x, g ' x) = g` by PROVE_TAC [FUPDATE_ABSORB_THM] THEN 528 POP_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN 529 `!v. (f |+ (x, y)) ' v = (h |+ (x, FAPPLY g x)) ' v` 530 by SRW_TAC [][] THEN 531 `y = g ' x` by PROVE_TAC [FAPPLY_FUPDATE] THEN 532 ASM_REWRITE_TAC [] THEN AP_THM_TAC THEN AP_TERM_TAC THEN 533 FIRST_X_ASSUM MATCH_MP_TAC THEN CONJ_TAC THENL [ 534 FULL_SIMP_TAC (srw_ss()) [EXTENSION, FDOM_FUPDATE] THEN PROVE_TAC [], 535 SIMP_TAC (srw_ss()) [FUN_EQ_THM] THEN Q.X_GEN_TAC `z` THEN 536 Cases_on `x = z` THENL [ 537 PROVE_TAC [NOT_FDOM_FAPPLY_FEMPTY], 538 FIRST_X_ASSUM (Q.SPEC_THEN `z` MP_TAC) THEN 539 ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM] 540 ] 541 ] 542 ]); 543 544val fmap_EQ = Q.store_thm 545("fmap_EQ", 546 `!(f:'a |-> 'b) g. (FDOM f = FDOM g) /\ (FAPPLY f = FAPPLY g) <=> (f = g)`, 547 REPEAT STRIP_TAC THEN EQ_TAC THEN REWRITE_TAC [fmap_EQ_1, fmap_EQ_2]); 548 549(*--------------------------------------------------------------------------- 550 A more useful equality 551 ---------------------------------------------------------------------------*) 552 553val fmap_EQ_THM = Q.store_thm 554("fmap_EQ_THM", 555 `!(f:'a |-> 'b) g. 556 (FDOM f = FDOM g) /\ (!x. x IN FDOM f ==> (FAPPLY f x = FAPPLY g x)) 557 <=> 558 (f = g)`, 559 REPEAT STRIP_TAC THEN EQ_TAC THENL [ 560 STRIP_TAC THEN ASM_REWRITE_TAC [GSYM fmap_EQ] THEN 561 MATCH_MP_TAC EQ_EXT THEN GEN_TAC THEN 562 Q.ASM_CASES_TAC `x IN FDOM f` THEN PROVE_TAC [NOT_FDOM_FAPPLY_FEMPTY], 563 STRIP_TAC THEN ASM_REWRITE_TAC [] 564 ]); 565 566(* and it's more useful still if the main equality is the other way 'round *) 567val fmap_EXT = save_thm("fmap_EXT", GSYM fmap_EQ_THM) 568 569(*--------------------------------------------------------------------------- 570 Submaps 571 ---------------------------------------------------------------------------*) 572 573val SUBMAP_DEF = new_definition ( 574 "SUBMAP_DEF", 575 ``!^fmap g. 576 $SUBMAP f g = 577 !x. x IN FDOM f ==> x IN FDOM g /\ (FAPPLY f x = FAPPLY g x)``) 578val _ = set_fixity "SUBMAP" (Infix(NONASSOC, 450)); 579val _ = Unicode.unicode_version { u = UTF8.chr 0x2291, tmnm = "SUBMAP"} 580val _ = TeX_notation {hol = "SUBMAP", TeX = ("\\HOLTokenSubmap{}", 1)} 581val _ = TeX_notation {hol = UTF8.chr 0x2291, TeX = ("\\HOLTokenSubmap{}", 1)} 582 583 584val SUBMAP_FEMPTY = Q.store_thm 585("SUBMAP_FEMPTY", 586 `!(f : ('a,'b) fmap). FEMPTY SUBMAP f`, 587 SRW_TAC [][SUBMAP_DEF, FDOM_FEMPTY]); 588 589val SUBMAP_REFL = Q.store_thm 590("SUBMAP_REFL", 591 `!(f:('a,'b) fmap). f SUBMAP f`, 592 REWRITE_TAC [SUBMAP_DEF]); 593val _ = export_rewrites["SUBMAP_REFL"]; 594 595val SUBMAP_ANTISYM = Q.store_thm 596("SUBMAP_ANTISYM", 597 `!(f:('a,'b) fmap) g. (f SUBMAP g /\ g SUBMAP f) = (f = g)`, 598 GEN_TAC THEN GEN_TAC THEN EQ_TAC THENL [ 599 REWRITE_TAC[SUBMAP_DEF, GSYM fmap_EQ_THM, EXTENSION] THEN PROVE_TAC [], 600 STRIP_TAC THEN ASM_REWRITE_TAC [SUBMAP_REFL] 601 ]); 602 603val SUBMAP_TRANS = store_thm( 604 "SUBMAP_TRANS", 605 ``!f g h. f SUBMAP g /\ g SUBMAP h ==> f SUBMAP h``, 606 SRW_TAC [][SUBMAP_DEF]); 607 608val SUBMAP_FUPDATE = store_thm( 609 "SUBMAP_FUPDATE", 610 ``k NOTIN FDOM f ==> f SUBMAP f |+ (k,v)``, 611 SRW_TAC [][SUBMAP_DEF] THEN METIS_TAC [FAPPLY_FUPDATE_THM]); 612 613val EQ_FDOM_SUBMAP = Q.store_thm( 614"EQ_FDOM_SUBMAP", 615`(f = g) <=> f SUBMAP g /\ (FDOM f = FDOM g)`, 616SIMP_TAC (srw_ss()) [fmap_EXT, SUBMAP_DEF] THEN METIS_TAC []); 617 618val SUBMAP_FUPDATE_EQN = Q.store_thm( 619 "SUBMAP_FUPDATE_EQN", 620 `f SUBMAP f |+ (x,y) <=> x NOTIN FDOM f \/ (f ' x = y) /\ x IN FDOM f`, 621 SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss ++ boolSimps.COND_elim_ss) 622 [FAPPLY_FUPDATE_THM,SUBMAP_DEF,EQ_IMP_THM] THEN 623 METIS_TAC []); 624val _ = export_rewrites ["SUBMAP_FUPDATE_EQN"] 625 626(*--------------------------------------------------------------------------- 627 Restriction 628 ---------------------------------------------------------------------------*) 629 630val res_lemma = Q.prove 631(`!^fmap r. 632 ?res. (FDOM res = FDOM f INTER r) 633 /\ (!x. res ' x = if x IN FDOM f INTER r then f ' x else FEMPTY ' x)`, 634 CONV_TAC SWAP_VARS_CONV THEN GEN_TAC THEN 635 INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [ 636 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][FDOM_FEMPTY], 637 REPEAT STRIP_TAC THEN 638 Cases_on `x IN r` THENL [ 639 Q.EXISTS_TAC `FUPDATE res (x,y)` THEN 640 ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN 641 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [], 642 643 Q.EXISTS_TAC `res` THEN 644 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN 645 FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [] 646 ] 647 ]); 648 649val DRESTRICT_DEF = new_specification 650 ("DRESTRICT_DEF", ["DRESTRICT"], 651 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) res_lemma); 652 653 654val DRESTRICT_FEMPTY = Q.store_thm 655("DRESTRICT_FEMPTY", 656 `!r. DRESTRICT FEMPTY r = FEMPTY`, 657 SRW_TAC [][GSYM fmap_EQ_THM, DRESTRICT_DEF, FDOM_FEMPTY]); 658val _ = export_rewrites ["DRESTRICT_FEMPTY"] 659 660val DRESTRICT_FUPDATE = Q.store_thm 661("DRESTRICT_FUPDATE", 662 `!^fmap r x y. 663 DRESTRICT (FUPDATE f (x,y)) r = 664 if x IN r then FUPDATE (DRESTRICT f r) (x,y) else DRESTRICT f r`, 665 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, DRESTRICT_DEF, FAPPLY_FUPDATE_THM, 666 EXTENSION] THEN PROVE_TAC []); 667val _ = export_rewrites ["DRESTRICT_FUPDATE"] 668 669 670val STRONG_DRESTRICT_FUPDATE = Q.store_thm 671("STRONG_DRESTRICT_FUPDATE", 672 `!^fmap r x y. 673 x IN r ==> (DRESTRICT (FUPDATE f (x,y)) r 674 = 675 FUPDATE (DRESTRICT f (r DELETE x)) (x,y))`, 676 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, DRESTRICT_DEF, 677 FAPPLY_FUPDATE_THM, EXTENSION] THEN PROVE_TAC []); 678 679val FDOM_DRESTRICT = Q.store_thm ( 680 "FDOM_DRESTRICT", 681 `!^fmap r x. FDOM (DRESTRICT f r) = FDOM f INTER r`, 682 SRW_TAC [][DRESTRICT_DEF]); 683 684val NOT_FDOM_DRESTRICT = Q.store_thm 685("NOT_FDOM_DRESTRICT", 686 `!^fmap x. ~(x IN FDOM f) ==> (DRESTRICT f (COMPL {x}) = f)`, 687 SRW_TAC [][GSYM fmap_EQ_THM, DRESTRICT_DEF, EXTENSION] THEN PROVE_TAC []); 688 689val DRESTRICT_SUBMAP = Q.store_thm 690("DRESTRICT_SUBMAP", 691 `!^fmap r. (DRESTRICT f r) SUBMAP f`, 692 INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [ 693 REWRITE_TAC [DRESTRICT_FEMPTY, SUBMAP_FEMPTY], 694 POP_ASSUM MP_TAC THEN 695 SIMP_TAC (srw_ss()) [DRESTRICT_DEF, SUBMAP_DEF, FDOM_FUPDATE] 696 ]); 697val _ = export_rewrites ["DRESTRICT_SUBMAP"] 698 699val DRESTRICT_DRESTRICT = Q.store_thm 700("DRESTRICT_DRESTRICT", 701 `!^fmap P Q. DRESTRICT (DRESTRICT f P) Q = DRESTRICT f (P INTER Q)`, 702 HO_MATCH_MP_TAC fmap_INDUCT 703 THEN SRW_TAC [][DRESTRICT_FEMPTY, DRESTRICT_FUPDATE] 704 THEN Q.ASM_CASES_TAC `x IN P` 705 THEN Q.ASM_CASES_TAC `x IN Q` 706 THEN ASM_REWRITE_TAC [DRESTRICT_FUPDATE]); 707val _ = export_rewrites ["DRESTRICT_DRESTRICT"] 708 709val DRESTRICT_IS_FEMPTY = Q.store_thm 710("DRESTRICT_IS_FEMPTY", 711 `!f. DRESTRICT f {} = FEMPTY`, 712 GEN_TAC THEN 713 `FDOM (DRESTRICT f {}) = {}` by SRW_TAC [][FDOM_DRESTRICT] THEN 714 PROVE_TAC [FDOM_EQ_EMPTY]); 715 716val FUPDATE_DRESTRICT = Q.store_thm 717("FUPDATE_DRESTRICT", 718 `!^fmap x y. FUPDATE f (x,y) = FUPDATE (DRESTRICT f (COMPL {x})) (x,y)`, 719 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, EXTENSION, DRESTRICT_DEF, 720 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []); 721 722val STRONG_DRESTRICT_FUPDATE_THM = Q.store_thm 723("STRONG_DRESTRICT_FUPDATE_THM", 724 `!^fmap r x y. 725 DRESTRICT (FUPDATE f (x,y)) r 726 = 727 if x IN r then FUPDATE (DRESTRICT f (COMPL {x} INTER r)) (x,y) 728 else DRESTRICT f (COMPL {x} INTER r)`, 729 SRW_TAC [][GSYM fmap_EQ_THM, DRESTRICT_DEF, FDOM_FUPDATE, EXTENSION, 730 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []); 731 732val DRESTRICT_UNIV = Q.store_thm 733("DRESTRICT_UNIV", 734 `!^fmap. DRESTRICT f UNIV = f`, 735 SRW_TAC [][DRESTRICT_DEF, GSYM fmap_EQ_THM]); 736 737val SUBMAP_DRESTRICT = Q.store_thm( 738 "SUBMAP_DRESTRICT", 739 `DRESTRICT f P SUBMAP f`, 740 SRW_TAC [][DRESTRICT_DEF, SUBMAP_DEF]); 741val _ = export_rewrites ["SUBMAP_DRESTRICT"] 742 743val DRESTRICT_EQ_DRESTRICT = store_thm( 744"DRESTRICT_EQ_DRESTRICT", 745``!f1 f2 s1 s2. 746 (DRESTRICT f1 s1 = DRESTRICT f2 s2) = 747 (DRESTRICT f1 s1 SUBMAP f2 /\ DRESTRICT f2 s2 SUBMAP f1 /\ 748 (s1 INTER FDOM f1 = s2 INTER FDOM f2))``, 749SRW_TAC[][GSYM fmap_EQ_THM,DRESTRICT_DEF,SUBMAP_DEF,EXTENSION] THEN 750METIS_TAC[]) 751 752(*--------------------------------------------------------------------------- 753 Union of finite maps 754 ---------------------------------------------------------------------------*) 755 756val union_lemma = Q.prove 757(`!^fmap g. 758 ?union. 759 (FDOM union = FDOM f UNION FDOM g) /\ 760 (!x. FAPPLY union x = if x IN FDOM f then FAPPLY f x else FAPPLY g x)`, 761 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL [ 762 GEN_TAC THEN Q.EXISTS_TAC `g` THEN SRW_TAC [][FDOM_FEMPTY], 763 REPEAT STRIP_TAC THEN 764 FIRST_X_ASSUM (Q.SPEC_THEN `g` STRIP_ASSUME_TAC) THEN 765 Q.EXISTS_TAC `FUPDATE union (x,y)` THEN 766 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN 767 PROVE_TAC [] 768 ]); 769 770val FUNION_DEF = new_specification 771 ("FUNION_DEF", ["FUNION"], 772 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) union_lemma); 773val _ = set_mapped_fixity {term_name = "FUNION", tok = UTF8.chr 0x228C, 774 fixity = Infixl 500} 775 776val FDOM_FUNION = save_thm("FDOM_FUNION", FUNION_DEF |> SPEC_ALL |> CONJUNCT1) 777val _ = export_rewrites ["FDOM_FUNION"] 778 779val FUNION_FEMPTY_1 = Q.store_thm 780("FUNION_FEMPTY_1[simp]", 781 `!g. FUNION FEMPTY g = g`, 782 SRW_TAC [][GSYM fmap_EQ_THM, FUNION_DEF, FDOM_FEMPTY]); 783 784val FUNION_FEMPTY_2 = Q.store_thm 785("FUNION_FEMPTY_2[simp]", 786 `!f. FUNION f FEMPTY = f`, 787 SRW_TAC [][GSYM fmap_EQ_THM, FUNION_DEF, FDOM_FEMPTY]); 788 789val FUNION_FUPDATE_1 = Q.store_thm 790("FUNION_FUPDATE_1", 791 `!^fmap g x y. 792 FUNION (FUPDATE f (x,y)) g = FUPDATE (FUNION f g) (x,y)`, 793 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, FUNION_DEF, FAPPLY_FUPDATE_THM, 794 EXTENSION] THEN PROVE_TAC []); 795 796val FUNION_FUPDATE_2 = Q.store_thm 797("FUNION_FUPDATE_2", 798 `!^fmap g x y. 799 FUNION f (FUPDATE g (x,y)) = 800 if x IN FDOM f then FUNION f g 801 else FUPDATE (FUNION f g) (x,y)`, 802 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, FUNION_DEF, FAPPLY_FUPDATE_THM, 803 EXTENSION] THEN PROVE_TAC []); 804 805val FDOM_FUNION = Q.store_thm 806("FDOM_FUNION", 807 `!^fmap g x. FDOM (FUNION f g) = FDOM f UNION FDOM g`, 808 REWRITE_TAC [FUNION_DEF]); 809 810val DRESTRICT_FUNION = Q.store_thm 811("DRESTRICT_FUNION", 812 `!^fmap r q. 813 DRESTRICT f (r UNION q) = FUNION (DRESTRICT f r) (DRESTRICT f q)`, 814 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, FUNION_DEF, FAPPLY_FUPDATE_THM, 815 EXTENSION, DRESTRICT_DEF] THEN PROVE_TAC []); 816 817val FUNION_IDEMPOT = store_thm("FUNION_IDEMPOT", 818``FUNION fm fm = fm``, 819 SRW_TAC[][GSYM fmap_EQ_THM,FUNION_DEF]) 820val _ = export_rewrites["FUNION_IDEMPOT"] 821 822(*--------------------------------------------------------------------------- 823 Merging of finite maps (added 17 March 2009 by Thomas Tuerk) 824 ---------------------------------------------------------------------------*) 825 826 827val fmerge_exists = prove ( 828 ���!m f g. 829 ?merge. 830 (FDOM merge = FDOM f UNION FDOM g) /\ 831 (!x. FAPPLY merge x = if ~(x IN FDOM f) then FAPPLY g x 832 else 833 if ~(x IN FDOM g) then FAPPLY f x 834 else 835 (m (FAPPLY f x) (FAPPLY g x)))���, 836 GEN_TAC THEN GEN_TAC THEN 837 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL [ 838 Q.EXISTS_TAC `f` THEN 839 SIMP_TAC std_ss [FDOM_FEMPTY, UNION_EMPTY, NOT_IN_EMPTY] THEN 840 PROVE_TAC[NOT_FDOM_FAPPLY_FEMPTY], 841 842 FULL_SIMP_TAC std_ss [] THEN REPEAT STRIP_TAC THEN 843 Cases_on `x IN FDOM f` THENL [ 844 Q.EXISTS_TAC `merge |+ (x, m (f ' x) y)`, 845 Q.EXISTS_TAC `merge |+ (x, y)` 846 ] THEN ( 847 ASM_SIMP_TAC std_ss [FDOM_FUPDATE] THEN 848 REPEAT STRIP_TAC THEN1 ( 849 SIMP_TAC std_ss [EXTENSION, IN_INSERT, IN_UNION] THEN 850 PROVE_TAC[] 851 ) THEN 852 Cases_on `x' = x` THEN ( 853 ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM, IN_INSERT] 854 ) 855 ) 856 ]); 857 858val FMERGE_DEF = new_specification 859 ("FMERGE_DEF", ["FMERGE"], 860 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) fmerge_exists); 861 862 863val FMERGE_FEMPTY = store_thm ("FMERGE_FEMPTY", 864 ``(FMERGE m f FEMPTY = f) /\ 865 (FMERGE m FEMPTY f = f)``, 866 867SIMP_TAC std_ss [GSYM fmap_EQ_THM] THEN 868SIMP_TAC std_ss [FMERGE_DEF, FDOM_FEMPTY, NOT_IN_EMPTY, 869 UNION_EMPTY]); 870 871val FDOM_FMERGE = store_thm( 872"FDOM_FMERGE", 873``!m f g. FDOM (FMERGE m f g) = FDOM f UNION FDOM g``, 874SRW_TAC[][FMERGE_DEF]) 875val _ = export_rewrites["FDOM_FMERGE"]; 876 877val FMERGE_FUNION = store_thm ("FMERGE_FUNION", 878 ``FUNION = FMERGE (\x y. x)``, 879 SIMP_TAC std_ss [FUN_EQ_THM, FMERGE_DEF, 880 GSYM fmap_EQ_THM, FUNION_DEF, 881 IN_UNION, DISJ_IMP_THM] THEN 882 METIS_TAC[]); 883 884 885val FUNION_FMERGE = store_thm ("FUNION_FMERGE", 886 ``!f1 f2 m. DISJOINT (FDOM f1) (FDOM f2) ==> 887 (FMERGE m f1 f2 = FUNION f1 f2)``, 888 SIMP_TAC std_ss [FUN_EQ_THM, FMERGE_DEF, 889 GSYM fmap_EQ_THM, FUNION_DEF, 890 IN_UNION, DISJ_IMP_THM] THEN 891 SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY, 892 IN_INTER] THEN 893 METIS_TAC[]); 894 895val FORALL_EQ_I = Q.prove( 896 ���(!x. P x <=> Q x) ==> ((!x. P x) <=> (!x. Q x))���, 897 metis_tac[]); 898 899val FMERGE_NO_CHANGE = store_thm ( 900 "FMERGE_NO_CHANGE", 901 ``(FMERGE m f1 f2 = f1 <=> 902 !x. x IN FDOM f2 ==> x IN FDOM f1 /\ m (f1 ' x) (f2 ' x) = f1 ' x) /\ 903 (FMERGE m f1 f2 = f2 <=> 904 !x. x IN FDOM f1 ==> x IN FDOM f2 /\ (m (f1 ' x) (f2 ' x) = f2 ' x))``, 905 SIMP_TAC std_ss [GSYM fmap_EQ_THM] THEN 906 SIMP_TAC std_ss [EXTENSION, FMERGE_DEF, IN_UNION, GSYM FORALL_AND_THM] THEN 907 STRIP_TAC THENL [ 908 HO_MATCH_MP_TAC FORALL_EQ_I THEN GEN_TAC THEN 909 Cases_on `x IN FDOM f2` THEN (ASM_SIMP_TAC std_ss [] THEN METIS_TAC[]), 910 911 HO_MATCH_MP_TAC FORALL_EQ_I THEN GEN_TAC THEN 912 Cases_on `x IN FDOM f1` THEN (ASM_SIMP_TAC std_ss [] THEN METIS_TAC[]) 913 ]); 914 915val FMERGE_COMM = store_thm ( 916 "FMERGE_COMM", 917 ``COMM (FMERGE m) = COMM m``, 918 SIMP_TAC std_ss [combinTheory.COMM_DEF, GSYM fmap_EQ_THM] THEN 919 SIMP_TAC std_ss [FMERGE_DEF] THEN 920 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 921 POP_ASSUM MP_TAC THEN 922 SIMP_TAC std_ss [GSYM LEFT_EXISTS_IMP_THM] THEN 923 Q.EXISTS_TAC `FEMPTY |+ (z, x)` THEN 924 Q.EXISTS_TAC `FEMPTY |+ (z, y)` THEN 925 926 SIMP_TAC std_ss [FDOM_FUPDATE, FDOM_FEMPTY, IN_UNION] THEN 927 SIMP_TAC std_ss [IN_SING, FAPPLY_FUPDATE_THM], 928 929 PROVE_TAC [UNION_COMM], 930 931 FULL_SIMP_TAC std_ss [IN_UNION] 932 ]); 933 934val FMERGE_ASSOC = store_thm ( 935 "FMERGE_ASSOC", 936 ``ASSOC (FMERGE m) = ASSOC m``, 937 SIMP_TAC std_ss [combinTheory.ASSOC_DEF, GSYM fmap_EQ_THM] THEN 938 SIMP_TAC std_ss [FMERGE_DEF, UNION_ASSOC, IN_UNION] THEN 939 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 940 POP_ASSUM MP_TAC THEN 941 SIMP_TAC std_ss [GSYM LEFT_EXISTS_IMP_THM] THEN 942 Q.EXISTS_TAC `FEMPTY |+ (e, x)` THEN 943 Q.EXISTS_TAC `FEMPTY |+ (e, y)` THEN 944 Q.EXISTS_TAC `FEMPTY |+ (e, z)` THEN 945 Q.EXISTS_TAC `e` THEN 946 SIMP_TAC std_ss [FDOM_FUPDATE, FDOM_FEMPTY, IN_UNION] THEN 947 SIMP_TAC std_ss [IN_SING, FAPPLY_FUPDATE_THM], 948 949 ASM_SIMP_TAC std_ss [] THEN METIS_TAC[], 950 951 ASM_SIMP_TAC std_ss [] THEN METIS_TAC[], 952 953 ASM_SIMP_TAC std_ss [] THEN METIS_TAC[] 954 ]); 955 956val FMERGE_DRESTRICT = store_thm ( 957 "FMERGE_DRESTRICT", 958 ``DRESTRICT (FMERGE f st1 st2) vs = 959 FMERGE f (DRESTRICT st1 vs) (DRESTRICT st2 vs)``, 960 SIMP_TAC std_ss [GSYM fmap_EQ_THM, DRESTRICT_DEF, FMERGE_DEF, EXTENSION, 961 IN_INTER, IN_UNION] THEN 962 METIS_TAC[]); 963 964val FMERGE_EQ_FEMPTY = store_thm ( 965 "FMERGE_EQ_FEMPTY", 966 ``(FMERGE m f g = FEMPTY) <=> (f = FEMPTY) /\ (g = FEMPTY)``, 967 SIMP_TAC std_ss [GSYM fmap_EQ_THM] THEN 968 SIMP_TAC (std_ss++boolSimps.CONJ_ss) [FMERGE_DEF, FDOM_FEMPTY, NOT_IN_EMPTY, 969 EMPTY_UNION, IN_UNION]); 970 971(*--------------------------------------------------------------------------- 972 "assoc" for finite maps 973 ---------------------------------------------------------------------------*) 974 975val FLOOKUP_DEF = Q.new_definition 976("FLOOKUP_DEF", 977 `FLOOKUP ^fmap x = if x IN FDOM f then SOME (FAPPLY f x) else NONE`); 978 979val FLOOKUP_EMPTY = store_thm( 980 "FLOOKUP_EMPTY", 981 ``FLOOKUP FEMPTY k = NONE``, 982 SRW_TAC [][FLOOKUP_DEF]); 983val _ = export_rewrites ["FLOOKUP_EMPTY"] 984 985val FLOOKUP_UPDATE = store_thm( 986 "FLOOKUP_UPDATE", 987 ``FLOOKUP (fm |+ (k1,v)) k2 = if k1 = k2 then SOME v else FLOOKUP fm k2``, 988 SRW_TAC [][FLOOKUP_DEF, FAPPLY_FUPDATE_THM] THEN 989 FULL_SIMP_TAC (srw_ss()) []); 990(* don't export this because of the if, though this is pretty paranoid *) 991 992val FLOOKUP_SUBMAP = store_thm( 993 "FLOOKUP_SUBMAP", 994 ``f SUBMAP g /\ (FLOOKUP f k = SOME v) ==> (FLOOKUP g k = SOME v)``, 995 SRW_TAC [][FLOOKUP_DEF, SUBMAP_DEF] THEN METIS_TAC []); 996 997val SUBMAP_FUPDATE_FLOOKUP = store_thm( 998 "SUBMAP_FUPDATE_FLOOKUP", 999 ``f SUBMAP (f |+ (x,y)) <=> (FLOOKUP f x = NONE) \/ (FLOOKUP f x = SOME y)``, 1000 SRW_TAC [][FLOOKUP_DEF, AC CONJ_ASSOC CONJ_COMM]); 1001 1002val FLOOKUP_FUNION = Q.store_thm( 1003"FLOOKUP_FUNION", 1004`FLOOKUP (FUNION f1 f2) k = 1005 case FLOOKUP f1 k of 1006 NONE => FLOOKUP f2 k 1007 | SOME v => SOME v`, 1008SRW_TAC [][FLOOKUP_DEF,FUNION_DEF] THEN FULL_SIMP_TAC (srw_ss()) []); 1009 1010val FLOOKUP_EXT = store_thm 1011("FLOOKUP_EXT", 1012 ``(f1 = f2) = (FLOOKUP f1 = FLOOKUP f2)``, 1013 SRW_TAC [][fmap_EXT,FUN_EQ_THM,IN_DEF,FLOOKUP_DEF] THEN 1014 PROVE_TAC [optionTheory.SOME_11,optionTheory.NOT_SOME_NONE]); 1015 1016val fmap_eq_flookup = save_thm( 1017 "fmap_eq_flookup", 1018 FLOOKUP_EXT |> REWRITE_RULE[FUN_EQ_THM]); 1019 1020val FLOOKUP_DRESTRICT = store_thm("FLOOKUP_DRESTRICT", 1021 ``!fm s k. FLOOKUP (DRESTRICT fm s) k = if k IN s then FLOOKUP fm k else NONE``, 1022 SRW_TAC[][FLOOKUP_DEF,DRESTRICT_DEF] THEN FULL_SIMP_TAC std_ss []); 1023 1024(*--------------------------------------------------------------------------- 1025 Universal quantifier on finite maps 1026 ---------------------------------------------------------------------------*) 1027 1028val FEVERY_DEF = Q.new_definition 1029("FEVERY_DEF", 1030 `FEVERY P ^fmap = !x. x IN FDOM f ==> P (x, FAPPLY f x)`); 1031 1032val FEVERY_FEMPTY = Q.store_thm 1033("FEVERY_FEMPTY", 1034 `!P:'a#'b -> bool. FEVERY P FEMPTY`, 1035 SRW_TAC [][FEVERY_DEF, FDOM_FEMPTY]); 1036 1037val FEVERY_FUPDATE = Q.store_thm 1038("FEVERY_FUPDATE", 1039 `!P ^fmap x y. 1040 FEVERY P (FUPDATE f (x,y)) 1041 <=> 1042 P (x,y) /\ FEVERY P (DRESTRICT f (COMPL {x}))`, 1043 SRW_TAC [][FEVERY_DEF, FDOM_FUPDATE, FAPPLY_FUPDATE_THM, 1044 DRESTRICT_DEF, EQ_IMP_THM] THEN PROVE_TAC []); 1045 1046val FEVERY_FLOOKUP = Q.store_thm( 1047"FEVERY_FLOOKUP", 1048`FEVERY P f /\ (FLOOKUP f k = SOME v) ==> P (k,v)`, 1049SRW_TAC [][FEVERY_DEF,FLOOKUP_DEF] THEN RES_TAC); 1050 1051(*--------------------------------------------------------------------------- 1052 Composition of finite maps 1053 ---------------------------------------------------------------------------*) 1054 1055val f_o_f_lemma = Q.prove 1056(`!f:'b |-> 'c. 1057 !g:'a |-> 'b. 1058 ?comp. (FDOM comp = FDOM g INTER { x | FAPPLY g x IN FDOM f }) 1059 /\ (!x. x IN FDOM comp ==> 1060 (FAPPLY comp x = (FAPPLY f (FAPPLY g x))))`, 1061 GEN_TAC THEN INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [ 1062 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][FDOM_FEMPTY], 1063 REPEAT STRIP_TAC THEN 1064 Cases_on `y IN FDOM f` THENL [ 1065 Q.EXISTS_TAC `FUPDATE comp (x, FAPPLY f y)` THEN 1066 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN 1067 PROVE_TAC [], 1068 Q.EXISTS_TAC `comp` THEN 1069 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN 1070 PROVE_TAC [] 1071 ] 1072 ]); 1073 1074val f_o_f_DEF = new_specification 1075 ("f_o_f_DEF", ["f_o_f"], 1076 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) f_o_f_lemma); 1077 1078val _ = set_fixity "f_o_f" (Infixr 800); 1079 1080val f_o_f_FEMPTY_1 = Q.store_thm 1081("f_o_f_FEMPTY_1", 1082 `!^fmap. (FEMPTY:('b,'c)fmap) f_o_f f = FEMPTY`, 1083 SRW_TAC [][GSYM fmap_EQ_THM, f_o_f_DEF, FDOM_FEMPTY, EXTENSION]); 1084 1085val f_o_f_FEMPTY_2 = Q.store_thm ( 1086 "f_o_f_FEMPTY_2", 1087 `!f:'b|->'c. f f_o_f (FEMPTY:('a,'b)fmap) = FEMPTY`, 1088 SRW_TAC [][GSYM fmap_EQ_THM, f_o_f_DEF, FDOM_FEMPTY]); 1089 1090val _ = export_rewrites["f_o_f_FEMPTY_1","f_o_f_FEMPTY_2"]; 1091 1092val o_f_lemma = Q.prove 1093(`!f:'b->'c. 1094 !g:'a|->'b. 1095 ?comp. (FDOM comp = FDOM g) 1096 /\ (!x. x IN FDOM comp ==> (FAPPLY comp x = f (FAPPLY g x)))`, 1097 GEN_TAC THEN INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [ 1098 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][FDOM_FEMPTY], 1099 REPEAT STRIP_TAC THEN Q.EXISTS_TAC `FUPDATE comp (x, f y)` THEN 1100 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM] 1101 ]); 1102 1103val o_f_DEF = new_specification 1104 ("o_f_DEF", ["o_f"], 1105 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) o_f_lemma); 1106 1107val _ = set_fixity "o_f" (Infixr 800); 1108 1109val o_f_FDOM = Q.store_thm 1110("o_f_FDOM", 1111 `!f:'b -> 'c. !g:'a |->'b. FDOM g = FDOM (f o_f g)`, 1112REWRITE_TAC [o_f_DEF]); 1113 1114val FDOM_o_f = save_thm("FDOM_o_f", GSYM o_f_FDOM); 1115val _ = export_rewrites ["FDOM_o_f"] 1116 1117val o_f_FAPPLY = Q.store_thm 1118("o_f_FAPPLY", 1119 `!f:'b->'c. !g:('a,'b) fmap. 1120 !x. x IN FDOM g ==> (FAPPLY (f o_f g) x = f (FAPPLY g x))`, 1121 SRW_TAC [][o_f_DEF]); 1122val _ = export_rewrites ["o_f_FAPPLY"] 1123 1124val o_f_FEMPTY = store_thm( 1125 "o_f_FEMPTY", 1126 ``f o_f FEMPTY = FEMPTY``, 1127 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_o_f]) 1128val _ = export_rewrites ["o_f_FEMPTY"] 1129 1130val FEVERY_o_f = store_thm ( 1131 "FEVERY_o_f", 1132 ``!m P f. FEVERY P (f o_f m) = FEVERY (\x. P (FST x, (f (SND x)))) m``, 1133 SIMP_TAC std_ss [FEVERY_DEF, FDOM_FEMPTY, NOT_IN_EMPTY, o_f_DEF]); 1134 1135val o_f_o_f = store_thm( 1136 "o_f_o_f", 1137 ``(f o_f (g o_f h)) = (f o g) o_f h``, 1138 SRW_TAC [][GSYM fmap_EQ_THM, o_f_FAPPLY]); 1139val _ = export_rewrites ["o_f_o_f"] 1140 1141val FLOOKUP_o_f = Q.store_thm( 1142"FLOOKUP_o_f", 1143`FLOOKUP (f o_f fm) k = case FLOOKUP fm k of NONE => NONE | SOME v => SOME (f v)`, 1144SRW_TAC [][FLOOKUP_DEF,o_f_FAPPLY]); 1145 1146(*--------------------------------------------------------------------------- 1147 Range of a finite map 1148 ---------------------------------------------------------------------------*) 1149 1150val FRANGE_DEF = Q.new_definition 1151("FRANGE_DEF", 1152 `FRANGE ^fmap = { y | ?x. x IN FDOM f /\ (FAPPLY f x = y)}`); 1153 1154val FRANGE_FEMPTY = Q.store_thm 1155("FRANGE_FEMPTY", 1156 `FRANGE FEMPTY = {}`, 1157 SRW_TAC [][FRANGE_DEF, FDOM_FEMPTY, EXTENSION]); 1158val _ = export_rewrites ["FRANGE_FEMPTY"] 1159 1160val FRANGE_FUPDATE = Q.store_thm 1161("FRANGE_FUPDATE", 1162 `!^fmap x y. 1163 FRANGE (FUPDATE f (x,y)) 1164 = 1165 y INSERT FRANGE (DRESTRICT f (COMPL {x}))`, 1166 SRW_TAC [][FRANGE_DEF, FDOM_FUPDATE, DRESTRICT_DEF, EXTENSION, 1167 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []); 1168 1169val SUBMAP_FRANGE = Q.store_thm 1170("SUBMAP_FRANGE", 1171 `!^fmap g. f SUBMAP g ==> FRANGE f SUBSET FRANGE g`, 1172 SRW_TAC [][SUBMAP_DEF,FRANGE_DEF, SUBSET_DEF] THEN PROVE_TAC []); 1173 1174val FINITE_FRANGE = store_thm( 1175 "FINITE_FRANGE", 1176 ``!fm. FINITE (FRANGE fm)``, 1177 HO_MATCH_MP_TAC fmap_INDUCT THEN 1178 SRW_TAC [][FRANGE_FUPDATE] THEN 1179 Q_TAC SUFF_TAC `DRESTRICT fm (COMPL {x}) = fm` THEN1 SRW_TAC [][] THEN 1180 SRW_TAC [][GSYM fmap_EQ_THM, DRESTRICT_DEF, EXTENSION] THEN 1181 PROVE_TAC []); 1182val _ = export_rewrites ["FINITE_FRANGE"] 1183 1184val o_f_FRANGE = store_thm( 1185 "o_f_FRANGE", 1186 ``x IN FRANGE g ==> f x IN FRANGE (f o_f g)``, 1187 SRW_TAC [][FRANGE_DEF] THEN METIS_TAC [o_f_FAPPLY]); 1188val _ = export_rewrites ["o_f_FRANGE"] 1189 1190val FRANGE_FLOOKUP = store_thm( 1191 "FRANGE_FLOOKUP", 1192 ``v IN FRANGE f <=> ?k. FLOOKUP f k = SOME v``, 1193 SRW_TAC [][FLOOKUP_DEF,FRANGE_DEF]); 1194 1195val FRANGE_FUNION = store_thm( 1196 "FRANGE_FUNION", 1197 ``DISJOINT (FDOM fm1) (FDOM fm2) ==> 1198 (FRANGE (FUNION fm1 fm2) = FRANGE fm1 UNION FRANGE fm2)``, 1199 STRIP_TAC THEN 1200 `!x. x IN FDOM fm2 ==> x NOTIN FDOM fm1` 1201 by (FULL_SIMP_TAC (srw_ss()) [DISJOINT_DEF, EXTENSION] THEN 1202 METIS_TAC []) THEN 1203 ASM_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss ++ boolSimps.CONJ_ss) 1204 [FRANGE_DEF, FUNION_DEF, EXTENSION]); 1205 1206(*--------------------------------------------------------------------------- 1207 Range restriction 1208 ---------------------------------------------------------------------------*) 1209 1210val ranres_lemma = Q.prove 1211(`!^fmap (r:'b set). 1212 ?res. (FDOM res = { x | x IN FDOM f /\ FAPPLY f x IN r}) 1213 /\ (!x. FAPPLY res x = 1214 if x IN FDOM f /\ FAPPLY f x IN r 1215 then FAPPLY f x 1216 else FAPPLY FEMPTY x)`, 1217 CONV_TAC SWAP_VARS_CONV THEN GEN_TAC THEN 1218 INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [ 1219 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][FDOM_FEMPTY, EXTENSION], 1220 REPEAT STRIP_TAC THEN 1221 Cases_on `y IN r` THENL [ 1222 Q.EXISTS_TAC `FUPDATE res (x,y)` THEN 1223 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN 1224 PROVE_TAC [], 1225 Q.EXISTS_TAC `res` THEN 1226 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN 1227 PROVE_TAC [] 1228 ] 1229 ]); 1230 1231val RRESTRICT_DEF = new_specification 1232 ("RRESTRICT_DEF", ["RRESTRICT"], 1233 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) ranres_lemma); 1234 1235val RRESTRICT_FEMPTY = Q.store_thm 1236("RRESTRICT_FEMPTY", 1237 `!r. RRESTRICT FEMPTY r = FEMPTY`, 1238 SRW_TAC [][GSYM fmap_EQ_THM, RRESTRICT_DEF, FDOM_FEMPTY, EXTENSION]); 1239 1240val RRESTRICT_FUPDATE = Q.store_thm 1241("RRESTRICT_FUPDATE", 1242`!^fmap r x y. 1243 RRESTRICT (FUPDATE f (x,y)) r = 1244 if y IN r then FUPDATE (RRESTRICT f r) (x,y) 1245 else RRESTRICT (DRESTRICT f (COMPL {x})) r`, 1246 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, RRESTRICT_DEF, DRESTRICT_DEF, 1247 EXTENSION, FAPPLY_FUPDATE_THM] THEN PROVE_TAC []); 1248 1249(*--------------------------------------------------------------------------- 1250 Functions as finite maps. 1251 1252 ---------------------------------------------------------------------------*) 1253 1254val ffmap_lemma = Q.prove 1255(`!(f:'a -> 'b) (P: 'a set). 1256 FINITE P ==> 1257 ?ffmap. (FDOM ffmap = P) 1258 /\ (!x. x IN P ==> (FAPPLY ffmap x = f x))`, 1259 GEN_TAC THEN HO_MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL [ 1260 Q.EXISTS_TAC `FEMPTY` THEN BETA_TAC THEN 1261 REWRITE_TAC [FDOM_FEMPTY, NOT_IN_EMPTY], 1262 REPEAT STRIP_TAC THEN Q.EXISTS_TAC `FUPDATE ffmap (e, f e)` THEN 1263 ASM_REWRITE_TAC [FDOM_FUPDATE, IN_INSERT, FAPPLY_FUPDATE_THM] THEN 1264 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN 1265 COND_CASES_TAC THENL [ 1266 POP_ASSUM SUBST_ALL_TAC THEN RES_TAC, 1267 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC [] 1268 ] 1269 ]); 1270 1271val FUN_FMAP_DEF = new_specification 1272 ("FUN_FMAP_DEF", ["FUN_FMAP"], 1273 CONV_RULE (ONCE_DEPTH_CONV RIGHT_IMP_EXISTS_CONV THENC 1274 ONCE_DEPTH_CONV SKOLEM_CONV) ffmap_lemma); 1275 1276val FUN_FMAP_EMPTY = store_thm( 1277 "FUN_FMAP_EMPTY", 1278 ``FUN_FMAP f {} = FEMPTY``, 1279 SRW_TAC [][GSYM fmap_EQ_THM, FUN_FMAP_DEF]); 1280val _ = export_rewrites ["FUN_FMAP_EMPTY"] 1281 1282val FRANGE_FMAP = store_thm( 1283 "FRANGE_FMAP", 1284 ``FINITE P ==> (FRANGE (FUN_FMAP f P) = IMAGE f P)``, 1285 SRW_TAC [boolSimps.CONJ_ss][EXTENSION, FRANGE_DEF, FUN_FMAP_DEF] THEN 1286 PROVE_TAC []); 1287val _ = export_rewrites ["FRANGE_FMAP"] 1288 1289val FDOM_FMAP = store_thm( 1290"FDOM_FMAP", 1291``!f s. FINITE s ==> (FDOM (FUN_FMAP f s) = s)``, 1292SRW_TAC[][FUN_FMAP_DEF]) 1293val _ = export_rewrites ["FDOM_FMAP"] 1294 1295val FLOOKUP_FUN_FMAP = Q.store_thm( 1296 "FLOOKUP_FUN_FMAP", 1297 `FINITE P ==> 1298 (FLOOKUP (FUN_FMAP f P) k = if k IN P then SOME (f k) else NONE)`, 1299 SRW_TAC [][FUN_FMAP_DEF,FLOOKUP_DEF]); 1300 1301(*--------------------------------------------------------------------------- 1302 Composition of finite map and function 1303 ---------------------------------------------------------------------------*) 1304 1305val f_o_DEF = new_infixr_definition 1306("f_o_DEF", 1307Term`$f_o (f:('b,'c)fmap) (g:'a->'b) 1308 = f f_o_f (FUN_FMAP g { x | g x IN FDOM f})`, 800); 1309 1310val FDOM_f_o = Q.store_thm 1311("FDOM_f_o", 1312 `!(f:'b|->'c) (g:'a->'b). 1313 FINITE {x | g x IN FDOM f } 1314 ==> 1315 (FDOM (f f_o g) = { x | g x IN FDOM f})`, 1316 SRW_TAC [][f_o_DEF, f_o_f_DEF, EXTENSION, FUN_FMAP_DEF, EQ_IMP_THM]); 1317val _ = export_rewrites["FDOM_f_o"]; 1318 1319val f_o_FEMPTY = store_thm( 1320"f_o_FEMPTY", 1321``!g. FEMPTY f_o g = FEMPTY``, 1322SRW_TAC[][f_o_DEF]) 1323val _ = export_rewrites["f_o_FEMPTY"] 1324 1325val f_o_FUPDATE = store_thm( 1326 "f_o_FUPDATE", 1327 ``!fm k v g. 1328 FINITE {x | g x IN FDOM fm} /\ 1329 FINITE {x | (g x = k)} ==> 1330 ((fm |+ (k,v)) f_o g = 1331 FMERGE (combin$C K) (fm f_o g) (FUN_FMAP (K v) {x | g x = k}))``, 1332 SRW_TAC[][] THEN 1333 `FINITE {x | (g x = k) \/ g x IN FDOM fm}` by ( 1334 REPEAT (POP_ASSUM MP_TAC) THEN 1335 Q.MATCH_ABBREV_TAC `FINITE s1 ==> FINITE s2 ==> FINITE s` THEN 1336 Q_TAC SUFF_TAC `s = s1 UNION s2` THEN1 SRW_TAC[][] THEN 1337 UNABBREV_ALL_TAC THEN 1338 SRW_TAC[][EXTENSION,EQ_IMP_THM] THEN 1339 SRW_TAC[][]) THEN 1340 SRW_TAC[][GSYM fmap_EQ_THM] THEN1 ( 1341 SRW_TAC[][EXTENSION,EQ_IMP_THM] THEN 1342 SRW_TAC[][]) THEN 1343 SRW_TAC[][FMERGE_DEF,FUN_FMAP_DEF,f_o_DEF,f_o_f_DEF ,FAPPLY_FUPDATE_THM]) 1344 1345val FAPPLY_f_o = Q.store_thm 1346("FAPPLY_f_o", 1347 `!(f:'b |-> 'c) (g:'a-> 'b). 1348 FINITE { x | g x IN FDOM f } 1349 ==> 1350 !x. x IN FDOM (f f_o g) ==> (FAPPLY (f f_o g) x = FAPPLY f (g x))`, 1351 SRW_TAC [][FDOM_f_o, FUN_FMAP_DEF, f_o_DEF, f_o_f_DEF]); 1352 1353 1354val FINITE_PRED_11 = Q.store_thm 1355("FINITE_PRED_11", 1356 `!(g:'a -> 'b). 1357 (!x y. (g x = g y) = (x = y)) 1358 ==> 1359 !f:'b|->'c. FINITE { x | g x IN FDOM f}`, 1360 GEN_TAC THEN STRIP_TAC THEN 1361 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL [ 1362 SRW_TAC [][FDOM_FEMPTY, GSPEC_F], 1363 SRW_TAC [][FDOM_FUPDATE, GSPEC_OR] THEN 1364 Cases_on `?y. g y = x` THENL [ 1365 POP_ASSUM (STRIP_THM_THEN SUBST_ALL_TAC o GSYM) THEN 1366 SRW_TAC [][GSPEC_EQ], 1367 POP_ASSUM MP_TAC THEN SRW_TAC [][GSPEC_F] 1368 ] 1369 ]); 1370 1371val f_o_ASSOC = Q.store_thm( 1372 "f_o_ASSOC", 1373 `(!x y. (g x = g y) <=> (x = y)) /\ (!x y. (h x = h y) <=> (x = y)) ==> 1374 ((f f_o g) f_o h = f f_o (g o h))`, 1375 simp[FDOM_f_o, FINITE_PRED_11, FAPPLY_f_o, fmap_EXT]) 1376 1377(* ---------------------------------------------------------------------- 1378 Domain subtraction (at a single point) 1379 ---------------------------------------------------------------------- *) 1380 1381val fmap_domsub = new_definition( 1382 "fmap_domsub", 1383 ``fdomsub fm k = DRESTRICT fm (COMPL {k})``); 1384val _ = overload_on ("\\\\", ``fdomsub``); 1385(* this has been set up as an infix in relationTheory *) 1386 1387val DOMSUB_FEMPTY = store_thm( 1388 "DOMSUB_FEMPTY", 1389 ``!k. FEMPTY \\ k = FEMPTY``, 1390 SRW_TAC [][GSYM fmap_EQ_THM, fmap_domsub, FDOM_DRESTRICT]); 1391 1392val DOMSUB_FUPDATE = store_thm( 1393 "DOMSUB_FUPDATE", 1394 ``!fm k v. fm |+ (k,v) \\ k = fm \\ k``, 1395 SRW_TAC [][GSYM fmap_EQ_THM, fmap_domsub, 1396 pred_setTheory.EXTENSION, DRESTRICT_DEF, 1397 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []); 1398 1399val DOMSUB_FUPDATE_NEQ = store_thm( 1400 "DOMSUB_FUPDATE_NEQ", 1401 ``!fm k1 k2 v. ~(k1 = k2) ==> (fm |+ (k1, v) \\ k2 = fm \\ k2 |+ (k1, v))``, 1402 SRW_TAC [][GSYM fmap_EQ_THM, fmap_domsub, 1403 pred_setTheory.EXTENSION, DRESTRICT_DEF, 1404 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []); 1405 1406val DOMSUB_FUPDATE_THM = store_thm( 1407 "DOMSUB_FUPDATE_THM", 1408 ``!fm k1 k2 v. fm |+ (k1,v) \\ k2 = if k1 = k2 then fm \\ k2 1409 else (fm \\ k2) |+ (k1, v)``, 1410 SRW_TAC [][GSYM fmap_EQ_THM, fmap_domsub, 1411 pred_setTheory.EXTENSION, DRESTRICT_DEF, 1412 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []); 1413 1414val FDOM_DOMSUB = store_thm( 1415 "FDOM_DOMSUB", 1416 ``!fm k. FDOM (fm \\ k) = FDOM fm DELETE k``, 1417 SRW_TAC [][fmap_domsub, FDOM_DRESTRICT, pred_setTheory.EXTENSION]); 1418 1419val DOMSUB_FAPPLY = store_thm( 1420 "DOMSUB_FAPPLY", 1421 ``!fm k. (fm \\ k) ' k = FEMPTY ' k``, 1422 SRW_TAC [][fmap_domsub, DRESTRICT_DEF]); 1423 1424val DOMSUB_FAPPLY_NEQ = store_thm( 1425 "DOMSUB_FAPPLY_NEQ", 1426 ``!fm k1 k2. ~(k1 = k2) ==> ((fm \\ k1) ' k2 = fm ' k2)``, 1427 SRW_TAC [][fmap_domsub, DRESTRICT_DEF, NOT_FDOM_FAPPLY_FEMPTY]); 1428 1429val DOMSUB_FAPPLY_THM = store_thm( 1430 "DOMSUB_FAPPLY_THM", 1431 ``!fm k1 k2. (fm \\ k1) ' k2 = if k1 = k2 then FEMPTY ' k2 else fm ' k2``, 1432 SRW_TAC [] [DOMSUB_FAPPLY, DOMSUB_FAPPLY_NEQ]); 1433 1434val DOMSUB_FLOOKUP = store_thm( 1435 "DOMSUB_FLOOKUP", 1436 ``!fm k. FLOOKUP (fm \\ k) k = NONE``, 1437 SRW_TAC [][FLOOKUP_DEF, FDOM_DOMSUB]); 1438 1439val DOMSUB_FLOOKUP_NEQ = store_thm( 1440 "DOMSUB_FLOOKUP_NEQ", 1441 ``!fm k1 k2. ~(k1 = k2) ==> (FLOOKUP (fm \\ k1) k2 = FLOOKUP fm k2)``, 1442 SRW_TAC [][FLOOKUP_DEF, FDOM_DOMSUB, DOMSUB_FAPPLY_NEQ]); 1443 1444val DOMSUB_FLOOKUP_THM = store_thm( 1445 "DOMSUB_FLOOKUP_THM", 1446 ``!fm k1 k2. FLOOKUP (fm \\ k1) k2 = if k1 = k2 then NONE else FLOOKUP fm k2``, 1447 SRW_TAC [][DOMSUB_FLOOKUP, DOMSUB_FLOOKUP_NEQ]); 1448 1449val FRANGE_FUPDATE_DOMSUB = store_thm( 1450 "FRANGE_FUPDATE_DOMSUB", 1451 ``!fm k v. FRANGE (fm |+ (k,v)) = v INSERT FRANGE (fm \\ k)``, 1452 SRW_TAC [][FRANGE_FUPDATE, fmap_domsub]); 1453 1454val _ = export_rewrites ["DOMSUB_FEMPTY", "DOMSUB_FUPDATE", "FDOM_DOMSUB", 1455 "DOMSUB_FAPPLY", "DOMSUB_FLOOKUP", "FRANGE_FUPDATE_DOMSUB"] 1456 1457val o_f_DOMSUB = store_thm( 1458 "o_f_DOMSUB", 1459 ``(g o_f fm) \\ k = g o_f (fm \\ k)``, 1460 SRW_TAC [][GSYM fmap_EQ_THM, DOMSUB_FAPPLY_THM, o_f_FAPPLY]); 1461val _ = export_rewrites ["o_f_DOMSUB"] 1462 1463val DOMSUB_IDEM = store_thm( 1464 "DOMSUB_IDEM", 1465 ``(fm \\ k) \\ k = fm \\ k``, 1466 SRW_TAC [][GSYM fmap_EQ_THM, DOMSUB_FAPPLY_THM]); 1467val _ = export_rewrites ["DOMSUB_IDEM"] 1468 1469val DOMSUB_COMMUTES = store_thm( 1470 "DOMSUB_COMMUTES", 1471 ``fm \\ k1 \\ k2 = fm \\ k2 \\ k1``, 1472 SRW_TAC [][GSYM fmap_EQ,DELETE_COMM] THEN 1473 SRW_TAC [][FUN_EQ_THM,DOMSUB_FAPPLY_THM] THEN 1474 SRW_TAC [][]); 1475 1476val o_f_FUPDATE = store_thm( 1477 "o_f_FUPDATE", 1478 ``f o_f (fm |+ (k,v)) = (f o_f fm) |+ (k, f v)``, 1479 SRW_TAC [][fmap_EXT] 1480 THENL [ 1481 SRW_TAC [][o_f_FAPPLY, FDOM_o_f], 1482 SRW_TAC [][FAPPLY_FUPDATE_THM] 1483 ]); 1484val _ = export_rewrites ["o_f_FUPDATE"] 1485 1486val DOMSUB_NOT_IN_DOM = store_thm( 1487 "DOMSUB_NOT_IN_DOM", 1488 ``~(k IN FDOM fm) ==> (fm \\ k = fm)``, 1489 SRW_TAC [][GSYM fmap_EQ_THM, DOMSUB_FAPPLY_THM, 1490 EXTENSION] THEN PROVE_TAC []); 1491 1492val fmap_CASES = Q.store_thm 1493("fmap_CASES", 1494 `!f:'a |-> 'b. (f = FEMPTY) \/ ?g x y. f = g |+ (x,y)`, 1495 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN METIS_TAC []); 1496 1497val IN_DOMSUB_NOT_EQUAL = Q.prove 1498(`!f:'a |->'b. !x1 x2. x2 IN FDOM (f \\ x1) ==> ~(x2 = x1)`, 1499 RW_TAC std_ss [FDOM_DOMSUB,IN_DELETE]); 1500 1501val SUBMAP_DOMSUB = store_thm( 1502 "SUBMAP_DOMSUB", 1503 ``(f \\ k) SUBMAP f``, 1504 SRW_TAC [][fmap_domsub]); 1505 1506val FMERGE_DOMSUB = store_thm( 1507"FMERGE_DOMSUB", 1508``!m m1 m2 k. (FMERGE m m1 m2) \\ k = FMERGE m (m1 \\ k) (m2 \\ k)``, 1509SRW_TAC[][fmap_domsub,FMERGE_DRESTRICT]) 1510 1511 1512(*---------------------------------------------------------------------------*) 1513(* Is there a better statement of this? *) 1514(*---------------------------------------------------------------------------*) 1515 1516val SUBMAP_FUPDATE = Q.store_thm 1517("SUBMAP_FUPDATE", 1518 `!(f:'a |->'b) g x y. 1519 (f |+ (x,y)) SUBMAP g <=> 1520 x IN FDOM(g) /\ g ' x = y /\ (f\\x) SUBMAP (g\\x)`, 1521 SRW_TAC [boolSimps.DNF_ss][SUBMAP_DEF, DOMSUB_FAPPLY_THM, 1522 FAPPLY_FUPDATE_THM] THEN 1523 METIS_TAC []); 1524 1525(* ---------------------------------------------------------------------- 1526 Iterated updates 1527 ---------------------------------------------------------------------- *) 1528 1529val FUPDATE_LIST = 1530 new_definition 1531 ("FUPDATE_LIST", 1532 ``FUPDATE_LIST = FOLDL FUPDATE``); 1533 1534val _ = overload_on ("|++", ``FUPDATE_LIST``); 1535 1536val FUPDATE_LIST_THM = store_thm( 1537 "FUPDATE_LIST_THM", 1538 ``!f. (f |++ [] = f) /\ 1539 (!h t. f |++ (h::t) = (FUPDATE f h) |++ t)``, 1540 SRW_TAC [][FUPDATE_LIST]); 1541 1542val FUPDATE_LIST_APPLY_NOT_MEM = store_thm( 1543 "FUPDATE_LIST_APPLY_NOT_MEM", 1544 ``!kvl f k. ~MEM k (MAP FST kvl) ==> ((f |++ kvl) ' k = f ' k)``, 1545 Induct THEN SRW_TAC [][FUPDATE_LIST_THM] THEN 1546 Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM]); 1547 1548val FUPDATE_LIST_APPEND = Q.store_thm( 1549"FUPDATE_LIST_APPEND", 1550`fm |++ (kvl1 ++ kvl2) = fm |++ kvl1 |++ kvl2`, 1551Q.ID_SPEC_TAC `fm` THEN Induct_on `kvl1` THEN SRW_TAC [][FUPDATE_LIST_THM]); 1552 1553val FUPDATE_FUPDATE_LIST_COMMUTES = Q.store_thm( 1554"FUPDATE_FUPDATE_LIST_COMMUTES", 1555`~MEM k (MAP FST kvl) ==> (fm |+ (k,v) |++ kvl = (fm |++ kvl) |+ (k,v))`, 1556let open rich_listTheory in 1557Q.ID_SPEC_TAC `kvl` THEN 1558HO_MATCH_MP_TAC SNOC_INDUCT THEN 1559SRW_TAC [][FUPDATE_LIST_THM] THEN 1560FULL_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM,MAP_SNOC,SNOC_APPEND,FUPDATE_LIST_APPEND] THEN 1561Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [FUPDATE_COMMUTES] 1562end); 1563 1564val FUPDATE_FUPDATE_LIST_MEM = Q.store_thm( 1565"FUPDATE_FUPDATE_LIST_MEM", 1566`MEM k (MAP FST kvl) ==> (fm |+ (k,v) |++ kvl = fm |++ kvl)`, 1567Q.ID_SPEC_TAC `fm` THEN 1568Induct_on `kvl` THEN SRW_TAC [][FUPDATE_LIST_THM] THEN 1569Cases_on `h` THEN SRW_TAC [][] THEN 1570FULL_SIMP_TAC (srw_ss()) [] THEN 1571Cases_on `k = q` THEN SRW_TAC [][] THEN 1572METIS_TAC [FUPDATE_COMMUTES]); 1573 1574val FEVERY_FUPDATE_LIST = Q.store_thm( 1575"FEVERY_FUPDATE_LIST", 1576`ALL_DISTINCT (MAP FST kvl) ==> 1577 (FEVERY P (fm |++ kvl) <=> EVERY P kvl /\ FEVERY P (DRESTRICT fm (COMPL (set (MAP FST kvl)))))`, 1578Q.ID_SPEC_TAC `fm` THEN 1579Induct_on `kvl` THEN SRW_TAC [][FUPDATE_LIST_THM,DRESTRICT_UNIV] THEN 1580Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1581SRW_TAC [][FUPDATE_FUPDATE_LIST_COMMUTES,FEVERY_FUPDATE] THEN 1582FULL_SIMP_TAC (srw_ss()) [GSYM COMPL_UNION] THEN 1583SRW_TAC [][Once UNION_COMM] THEN 1584SRW_TAC [][Once (GSYM INSERT_SING_UNION)] THEN 1585SRW_TAC [][EQ_IMP_THM]); 1586 1587local open listTheory in 1588val FUPDATE_LIST_APPLY_MEM = store_thm( 1589"FUPDATE_LIST_APPLY_MEM", 1590``!kvl f k v n. n < LENGTH kvl /\ (k = EL n (MAP FST kvl)) /\ (v = EL n (MAP SND kvl)) /\ 1591 (!m. n < m /\ m < LENGTH kvl ==> (EL m (MAP FST kvl) <> k)) 1592 ==> ((f |++ kvl) ' k = v)``, 1593Induct THEN1 SRW_TAC[][] THEN 1594Cases THEN NTAC 3 GEN_TAC THEN 1595Cases THEN1 ( 1596 Q.MATCH_RENAME_TAC `0 < LENGTH ((q,r)::kvl) /\ _ ==> _` THEN 1597 Q.ISPECL_THEN [`kvl`,`f |+ (k,r)`,`k`] MP_TAC FUPDATE_LIST_APPLY_NOT_MEM THEN 1598 SRW_TAC[][FUPDATE_LIST_THM] THEN 1599 FIRST_X_ASSUM MATCH_MP_TAC THEN 1600 SRW_TAC[][MEM_MAP,MEM_EL,pairTheory.EXISTS_PROD] THEN 1601 Q.MATCH_RENAME_TAC `_ \/ _ <> EL n kvl` THEN 1602 FIRST_X_ASSUM (Q.SPEC_THEN `SUC n` MP_TAC) THEN 1603 SRW_TAC[][EL_MAP] THEN 1604 METIS_TAC[pairTheory.FST]) THEN 1605SRW_TAC[][] THEN 1606Q.MATCH_RENAME_TAC `(f |++ ((q,r)::kvl)) ' _ = _` THEN 1607Q.ISPECL_THEN [`(q,r)`,`kvl`] SUBST1_TAC rich_listTheory.CONS_APPEND THEN 1608REWRITE_TAC [FUPDATE_LIST_APPEND] THEN 1609FIRST_X_ASSUM MATCH_MP_TAC THEN 1610Q.MATCH_ASSUM_RENAME_TAC `n < LENGTH kvl` THEN 1611Q.EXISTS_TAC `n` THEN 1612SRW_TAC[][] THEN 1613Q.MATCH_RENAME_TAC `EL m (MAP FST kvl) <> _` THEN 1614FIRST_X_ASSUM (Q.SPEC_THEN `SUC m` MP_TAC) THEN 1615SRW_TAC[][]) 1616end 1617 1618val FOLDL_FUPDATE_LIST = store_thm("FOLDL_FUPDATE_LIST", 1619 ``!f1 f2 ls a. FOLDL (\fm k. fm |+ (f1 k, f2 k)) a ls = 1620 a |++ MAP (\k. (f1 k, f2 k)) ls``, 1621 SRW_TAC[][FUPDATE_LIST,rich_listTheory.FOLDL_MAP]) 1622 1623val FUPDATE_LIST_SNOC = store_thm("FUPDATE_LIST_SNOC", 1624 ``!xs x fm. fm |++ SNOC x xs = (fm |++ xs) |+ x``, 1625 Induct THEN SRW_TAC[][FUPDATE_LIST_THM]) 1626 1627(* ---------------------------------------------------------------------- 1628 More theorems 1629 ---------------------------------------------------------------------- *) 1630 1631val FAPPLY_FUPD_EQ = prove( 1632 ``!fmap k1 v1 k2 v2. 1633 ((fmap |+ (k1, v1)) ' k2 = v2) <=> 1634 k1 = k2 /\ v1 = v2 \/ k1 <> k2 /\ fmap ' k2 = v2``, 1635 SRW_TAC [][FAPPLY_FUPDATE_THM, EQ_IMP_THM]); 1636 1637 1638(* (pseudo) injectivity results about fupdate *) 1639 1640val FUPD11_SAME_KEY_AND_BASE = store_thm( 1641 "FUPD11_SAME_KEY_AND_BASE", 1642 ``!f k v1 v2. (f |+ (k, v1) = f |+ (k, v2)) <=> (v1 = v2)``, 1643 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, DISJ_IMP_THM, 1644 FAPPLY_FUPDATE_THM, FORALL_AND_THM, EQ_IMP_THM]); 1645 1646val FUPD11_SAME_NEW_KEY = store_thm( 1647 "FUPD11_SAME_NEW_KEY", 1648 ``!f1 f2 k v1 v2. 1649 ~(k IN FDOM f1) /\ ~(k IN FDOM f2) ==> 1650 ((f1 |+ (k, v1) = f2 |+ (k, v2)) <=> (f1 = f2) /\ (v1 = v2))``, 1651 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, DISJ_IMP_THM, 1652 FAPPLY_FUPDATE_THM, FORALL_AND_THM, EQ_IMP_THM, EXTENSION] THEN 1653 PROVE_TAC []); 1654 1655val SAME_KEY_UPDATES_DIFFER = store_thm( 1656 "SAME_KEY_UPDATES_DIFFER", 1657 ``!f1 f2 k v1 v2. v1 <> v2 ==> ~(f1 |+ (k, v1) = f2 |+ (k, v2))``, 1658 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, RIGHT_AND_OVER_OR, 1659 EXISTS_OR_THM]); 1660 1661val FUPD11_SAME_BASE = store_thm( 1662 "FUPD11_SAME_BASE", 1663 ``!f k1 v1 k2 v2. 1664 (f |+ (k1, v1) = f |+ (k2, v2)) <=> 1665 (k1 = k2) /\ (v1 = v2) \/ 1666 ~(k1 = k2) /\ k1 IN FDOM f /\ k2 IN FDOM f /\ 1667 (f |+ (k1, v1) = f) /\ (f |+ (k2, v2) = f)``, 1668 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE, GSYM fmap_EQ_THM, 1669 DISJ_IMP_THM, FORALL_AND_THM, FAPPLY_FUPDATE_THM, 1670 EXTENSION] THEN PROVE_TAC[]); 1671 1672val FUPD_SAME_KEY_UNWIND = store_thm( 1673 "FUPD_SAME_KEY_UNWIND", 1674 ``!f1 f2 k v1 v2. 1675 (f1 |+ (k, v1) = f2 |+ (k, v2)) ==> 1676 (v1 = v2) /\ (!v. f1 |+ (k, v) = f2 |+ (k, v))``, 1677 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE, GSYM fmap_EQ_THM, 1678 DISJ_IMP_THM, FORALL_AND_THM, FAPPLY_FUPDATE_THM, 1679 EXTENSION] THEN PROVE_TAC[]); 1680 1681val FUPD11_SAME_UPDATE = store_thm( 1682 "FUPD11_SAME_UPDATE", 1683 ``!f1 f2 k v. (f1 |+ (k,v) = f2 |+ (k,v)) = 1684 (DRESTRICT f1 (COMPL {k}) = DRESTRICT f2 (COMPL {k}))``, 1685 SRW_TAC [][GSYM fmap_EQ_THM, EXTENSION, DRESTRICT_DEF, FDOM_FUPDATE, 1686 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []); 1687 1688val FDOM_FUPDATE_LIST = store_thm( 1689 "FDOM_FUPDATE_LIST", 1690 ``!kvl fm. FDOM (fm |++ kvl) = 1691 FDOM fm UNION set (MAP FST kvl)``, 1692 Induct THEN 1693 ASM_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM, 1694 FDOM_FUPDATE, pairTheory.FORALL_PROD, 1695 EXTENSION] THEN PROVE_TAC []); 1696 1697val FUPDATE_LIST_SAME_UPDATE = store_thm( 1698 "FUPDATE_LIST_SAME_UPDATE", 1699 ``!kvl f1 f2. (f1 |++ kvl = f2 |++ kvl) = 1700 (DRESTRICT f1 (COMPL (set (MAP FST kvl))) = 1701 DRESTRICT f2 (COMPL (set (MAP FST kvl))))``, 1702 Induct THENL [ 1703 SRW_TAC [][GSYM fmap_EQ_THM, FUPDATE_LIST_THM, DRESTRICT_DEF] THEN 1704 PROVE_TAC [], 1705 ASM_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM, pairTheory.FORALL_PROD] THEN 1706 POP_ASSUM (K ALL_TAC) THEN 1707 SRW_TAC [][GSYM fmap_EQ_THM, FUPDATE_LIST_THM, DRESTRICT_DEF, 1708 FDOM_FUPDATE, FDOM_FUPDATE_LIST, EXTENSION, 1709 FAPPLY_FUPDATE_THM] THEN 1710 EQ_TAC THEN REPEAT STRIP_TAC THEN REPEAT COND_CASES_TAC THEN 1711 SRW_TAC [][] THEN PROVE_TAC [] 1712 ]); 1713 1714val FUPDATE_LIST_SAME_KEYS_UNWIND = store_thm( 1715 "FUPDATE_LIST_SAME_KEYS_UNWIND", 1716 ``!f1 f2 kvl1 kvl2. 1717 (f1 |++ kvl1 = f2 |++ kvl2) /\ 1718 (MAP FST kvl1 = MAP FST kvl2) /\ ALL_DISTINCT (MAP FST kvl1) ==> 1719 (kvl1 = kvl2) /\ 1720 !kvl. (MAP FST kvl = MAP FST kvl1) ==> 1721 (f1 |++ kvl = f2 |++ kvl)``, 1722 CONV_TAC (BINDER_CONV SWAP_VARS_CONV THENC SWAP_VARS_CONV) THEN 1723 Induct THEN ASM_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM] THEN 1724 REPEAT GEN_TAC THEN 1725 `?k v. h = (k,v)` by PROVE_TAC [pair_CASES] THEN 1726 POP_ASSUM SUBST_ALL_TAC THEN SIMP_TAC (srw_ss()) [] THEN 1727 `(kvl2 = []) \/ ?k2 v2 t2. kvl2 = (k2,v2) :: t2` by 1728 PROVE_TAC [pair_CASES, listTheory.list_CASES] THEN 1729 POP_ASSUM SUBST_ALL_TAC THEN SIMP_TAC (srw_ss()) [] THEN 1730 SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM] THEN STRIP_TAC THEN 1731 `kvl1 = t2` by PROVE_TAC [] THEN POP_ASSUM SUBST_ALL_TAC THEN 1732 `v = v2` by (FIRST_X_ASSUM (MP_TAC o C Q.AP_THM `k` o Q.AP_TERM `(')`) THEN 1733 SRW_TAC [][FUPDATE_LIST_APPLY_NOT_MEM]) THEN 1734 SRW_TAC [][] THEN 1735 `(kvl = []) \/ (?k' v' t. kvl = (k',v') :: t)` by 1736 PROVE_TAC [pair_CASES, listTheory.list_CASES] THEN 1737 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1738 Q.PAT_X_ASSUM `fm : 'a |-> 'b = fm1` MP_TAC THEN 1739 SIMP_TAC (srw_ss()) [GSYM FUPDATE_LIST_THM] THEN 1740 ASM_SIMP_TAC (srw_ss()) [FUPDATE_LIST_SAME_UPDATE]); 1741 1742val lemma = prove( 1743 ``!kvl k fm. MEM k (MAP FST kvl) ==> 1744 MEM (k, (fm |++ kvl) ' k) kvl``, 1745 Induct THEN 1746 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, FUPDATE_LIST_THM, 1747 DISJ_IMP_THM, FORALL_AND_THM] THEN 1748 REPEAT STRIP_TAC THEN 1749 Cases_on `MEM p_1 (MAP FST kvl)` THEN 1750 SRW_TAC [][FUPDATE_LIST_APPLY_NOT_MEM]); 1751 1752val FM_CONCRETE_EQ_ENUMERATE_CASES = store_thm( 1753 "FMEQ_ENUMERATE_CASES", 1754 ``!f1 kvl p. (f1 |+ p = FEMPTY |++ kvl) ==> MEM p kvl``, 1755 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, GSYM fmap_EQ_THM, 1756 FDOM_FUPDATE, FDOM_FUPDATE_LIST, DISJ_IMP_THM, 1757 FORALL_AND_THM, FDOM_FEMPTY] THEN 1758 REPEAT STRIP_TAC THEN 1759 FULL_SIMP_TAC (srw_ss()) [pred_setTheory.EXTENSION] THEN 1760 PROVE_TAC [lemma]); 1761 1762val FMEQ_SINGLE_SIMPLE_ELIM = store_thm( 1763 "FMEQ_SINGLE_SIMPLE_ELIM", 1764 ``!P k v ck cv nv. (?fm. (fm |+ (k, v) = FEMPTY |+ (ck, cv)) /\ 1765 P (fm |+ (k, nv))) <=> 1766 (k = ck) /\ (v = cv) /\ P (FEMPTY |+ (ck, nv))``, 1767 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 1768 `FEMPTY |+ (ck, cv) = FEMPTY |++ [(ck,cv)]` 1769 by SRW_TAC [][FUPDATE_LIST_THM] THEN 1770 `MEM (k,v) [(ck, cv)]` by PROVE_TAC [FM_CONCRETE_EQ_ENUMERATE_CASES] THEN 1771 FULL_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM] THEN 1772 PROVE_TAC [FUPD_SAME_KEY_UNWIND], 1773 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][] 1774 ]); 1775 1776val FMEQ_SINGLE_SIMPLE_DISJ_ELIM = store_thm( 1777 "FMEQ_SINGLE_SIMPLE_DISJ_ELIM", 1778 ``!fm k v ck cv. 1779 (fm |+ (k,v) = FEMPTY |+ (ck, cv)) <=> 1780 (k = ck) /\ (v = cv) /\ 1781 ((fm = FEMPTY) \/ (?v'. fm = FEMPTY |+ (k, v')))``, 1782 REPEAT GEN_TAC THEN EQ_TAC THEN 1783 SIMP_TAC (srw_ss()) [DISJ_IMP_THM, LEFT_AND_OVER_OR, 1784 GSYM RIGHT_EXISTS_AND_THM, 1785 GSYM LEFT_FORALL_IMP_THM] THEN 1786 SIMP_TAC (srw_ss() ++ boolSimps.CONJ_ss) 1787 [GSYM fmap_EQ_THM, DISJ_IMP_THM, FORALL_AND_THM] THEN 1788 SIMP_TAC (srw_ss()) [EXTENSION] THEN 1789 PROVE_TAC [FAPPLY_FUPDATE]); 1790 1791 1792val FUPDATE_PURGE = Q.store_thm 1793("FUPDATE_PURGE", 1794 `!f x y. f |+ (x,y) = (f \\ x) |+ (x,y)`, 1795 SRW_TAC [] [fmap_EXT,EXTENSION,FAPPLY_FUPDATE_THM,DOMSUB_FAPPLY_THM] THEN 1796 METIS_TAC[]); 1797 1798(*---------------------------------------------------------------------------*) 1799(* For EVAL on terms with finite map expressions. *) 1800(*---------------------------------------------------------------------------*) 1801 1802val _ = 1803 computeLib.add_persistent_funs 1804 ["FUPDATE_LIST_THM", 1805 "DOMSUB_FUPDATE_THM", 1806 "DOMSUB_FEMPTY", 1807 "FDOM_FUPDATE", 1808 "FAPPLY_FUPDATE_THM", 1809 "FDOM_FEMPTY", 1810 "FLOOKUP_EMPTY", 1811 "FLOOKUP_UPDATE"]; 1812 1813 1814(*---------------------------------------------------------------------------*) 1815(* Mapping for finite maps with two arguments, compare to o_f *) 1816(* added 17 March 2009 by Thomas Tuerk, updated 26 March *) 1817(*---------------------------------------------------------------------------*) 1818 1819val FMAP_MAP2_def = Define 1820`FMAP_MAP2 f m = FUN_FMAP (\x. f (x,m ' x)) (FDOM m)`; 1821 1822 1823val FMAP_MAP2_THM = store_thm ("FMAP_MAP2_THM", 1824``(FDOM (FMAP_MAP2 f m) = FDOM m) /\ 1825 (!x. x IN FDOM m ==> ((FMAP_MAP2 f m) ' x = f (x,m ' x)))``, 1826 1827SIMP_TAC std_ss [FMAP_MAP2_def, 1828 FUN_FMAP_DEF, FDOM_FINITE]); 1829 1830 1831 1832val FMAP_MAP2_FEMPTY = store_thm ("FMAP_MAP2_FEMPTY", 1833``FMAP_MAP2 f FEMPTY = FEMPTY``, 1834 1835SIMP_TAC std_ss [GSYM fmap_EQ_THM, FMAP_MAP2_THM, 1836 FDOM_FEMPTY, NOT_IN_EMPTY]); 1837 1838 1839val FMAP_MAP2_FUPDATE = store_thm ("FMAP_MAP2_FUPDATE", 1840``FMAP_MAP2 f (m |+ (x, v)) = 1841 (FMAP_MAP2 f m) |+ (x, f (x,v))``, 1842 1843SIMP_TAC std_ss [GSYM fmap_EQ_THM, FMAP_MAP2_THM, 1844 FDOM_FUPDATE, IN_INSERT, 1845 FAPPLY_FUPDATE_THM, 1846 COND_RAND, COND_RATOR, 1847 DISJ_IMP_THM]); 1848 1849(*---------------------------------------------------------------------------*) 1850(* Some general stuff *) 1851(* added 17 March 2009 by Thomas Tuerk *) 1852(*---------------------------------------------------------------------------*) 1853 1854val FEVERY_STRENGTHEN_THM = 1855store_thm ("FEVERY_STRENGTHEN_THM", 1856``FEVERY P FEMPTY /\ 1857 ((FEVERY P f /\ P (x,y)) ==> FEVERY P (f |+ (x,y)))``, 1858 1859SIMP_TAC std_ss [FEVERY_DEF, FDOM_FEMPTY, 1860 NOT_IN_EMPTY, FAPPLY_FUPDATE_THM, 1861 FDOM_FUPDATE, IN_INSERT] THEN 1862METIS_TAC[]); 1863 1864 1865 1866val FUPDATE_ELIM = store_thm ("FUPDATE_ELIM", 1867``!k v f. 1868 ((k IN FDOM f) /\ (f ' k = v)) ==> (f |+ (k,v) = f)``, 1869 1870REPEAT STRIP_TAC THEN 1871ONCE_REWRITE_TAC[GSYM fmap_EQ_THM] THEN 1872SIMP_TAC std_ss [FDOM_FUPDATE, IN_INSERT, EXTENSION, 1873 FAPPLY_FUPDATE_THM] THEN 1874PROVE_TAC[]); 1875 1876 1877 1878val FEVERY_DRESTRICT_COMPL = store_thm( 1879"FEVERY_DRESTRICT_COMPL", 1880``FEVERY P (DRESTRICT (f |+ (k, v)) (COMPL s)) = 1881 ((~(k IN s) ==> P (k,v)) /\ 1882 (FEVERY P (DRESTRICT f (COMPL (k INSERT s)))))``, 1883 1884SIMP_TAC std_ss [FEVERY_DEF, IN_INTER, 1885 FDOM_DRESTRICT, 1886 DRESTRICT_DEF, FAPPLY_FUPDATE_THM, 1887 FDOM_FUPDATE, IN_INSERT, 1888 RIGHT_AND_OVER_OR, IN_COMPL, 1889 DISJ_IMP_THM, FORALL_AND_THM] THEN 1890PROVE_TAC[]); 1891 1892 1893(*--------------------------------------------------------------------------- 1894 Merging of finite maps (added 17 March 2009 by Thomas Tuerk) 1895 ---------------------------------------------------------------------------*) 1896 1897val FUNION_EQ_FEMPTY = store_thm ("FUNION_EQ_FEMPTY", 1898``!h1 h2. (FUNION h1 h2 = FEMPTY) = ((h1 = FEMPTY) /\ (h2 = FEMPTY))``, 1899 1900 SIMP_TAC std_ss [GSYM fmap_EQ_THM, EXTENSION, FDOM_FEMPTY, FUNION_DEF, 1901 NOT_IN_EMPTY, IN_UNION, DISJ_IMP_THM, FORALL_AND_THM] THEN 1902 METIS_TAC[]); 1903 1904 1905 1906val SUBMAP_FUNION_EQ = store_thm ("SUBMAP_FUNION_EQ", 1907``(!f1 f2 f3. DISJOINT (FDOM f1) (FDOM f2) ==> 1908 ((f1 SUBMAP (FUNION f2 f3) <=> f1 SUBMAP f3))) /\ 1909 (!f1 f2 f3. DISJOINT (FDOM f1) (FDOM f3 DIFF (FDOM f2)) ==> 1910 ((f1 SUBMAP (FUNION f2 f3) <=> f1 SUBMAP f2)))``, 1911 1912 SIMP_TAC std_ss [SUBMAP_DEF, FUNION_DEF, IN_UNION, DISJOINT_DEF, EXTENSION, 1913 NOT_IN_EMPTY, IN_INTER, IN_DIFF] THEN 1914 METIS_TAC[]) 1915 1916 1917val SUBMAP_FUNION = store_thm ("SUBMAP_FUNION", 1918``!f1 f2 f3. f1 SUBMAP f2 \/ (DISJOINT (FDOM f1) (FDOM f2) /\ f1 SUBMAP f3) ==> 1919 f1 SUBMAP FUNION f2 f3``, 1920 1921SIMP_TAC std_ss [SUBMAP_DEF, FUNION_DEF, IN_UNION, DISJOINT_DEF, EXTENSION, 1922 NOT_IN_EMPTY, IN_INTER] THEN 1923METIS_TAC[]); 1924 1925val SUBMAP_FUNION_ID = store_thm ("SUBMAP_FUNION_ID", 1926``(!f1 f2. f1 SUBMAP FUNION f1 f2) /\ 1927 (!f1 f2. DISJOINT (FDOM f1) (FDOM f2) ==> f2 SUBMAP (FUNION f1 f2))``, 1928 1929METIS_TAC[SUBMAP_REFL, SUBMAP_FUNION, DISJOINT_SYM]); 1930 1931val FEMPTY_SUBMAP = store_thm ("FEMPTY_SUBMAP", 1932 ``!h. h SUBMAP FEMPTY <=> (h = FEMPTY)``, 1933 1934 SIMP_TAC std_ss [SUBMAP_DEF, FDOM_FEMPTY, NOT_IN_EMPTY, GSYM fmap_EQ_THM, 1935 EXTENSION] THEN 1936 METIS_TAC[]); 1937 1938 1939val FUNION_EQ = store_thm ("FUNION_EQ", 1940``!f1 f2 f3. DISJOINT (FDOM f1) (FDOM f2) /\ DISJOINT (FDOM f1) (FDOM f3) ==> 1941 ((FUNION f1 f2 = FUNION f1 f3) <=> (f2 = f3))``, 1942 1943 SIMP_TAC std_ss [GSYM SUBMAP_ANTISYM, SUBMAP_DEF, FUNION_DEF, IN_UNION, DISJOINT_DEF, EXTENSION, 1944 NOT_IN_EMPTY, IN_INTER, IN_DIFF] THEN 1945 METIS_TAC[]) 1946 1947val FUNION_EQ_IMPL = store_thm ("FUNION_EQ_IMPL", 1948``!f1 f2 f3. 1949 DISJOINT (FDOM f1) (FDOM f2) /\ 1950 DISJOINT (FDOM f1) (FDOM f3) /\ 1951 (f2 = f3) 1952 ==> 1953 ((FUNION f1 f2) = (FUNION f1 f3))``, 1954 SIMP_TAC std_ss []); 1955 1956 1957val DOMSUB_FUNION = store_thm ("DOMSUB_FUNION", 1958``(FUNION f g) \\ k = FUNION (f \\ k) (g \\ k)``, 1959SIMP_TAC std_ss [GSYM fmap_EQ_THM, FDOM_DOMSUB, FUNION_DEF, EXTENSION, 1960 IN_UNION, IN_DELETE] THEN 1961REPEAT STRIP_TAC THENL [ 1962 METIS_TAC[], 1963 ASM_SIMP_TAC std_ss [DOMSUB_FAPPLY_NEQ, FUNION_DEF], 1964 ASM_SIMP_TAC std_ss [DOMSUB_FAPPLY_NEQ, FUNION_DEF] 1965]); 1966 1967 1968val FUNION_COMM = store_thm ("FUNION_COMM", 1969``!f g. (DISJOINT (FDOM f) (FDOM g)) ==> ((FUNION f g) = (FUNION g f))``, 1970 SIMP_TAC std_ss [GSYM fmap_EQ_THM, FUNION_DEF, IN_UNION, DISJOINT_DEF, 1971 EXTENSION, NOT_IN_EMPTY, IN_INTER] THEN 1972 METIS_TAC[]); 1973 1974val FUNION_ASSOC = store_thm ("FUNION_ASSOC", 1975``!f g h. ((FUNION f (FUNION g h)) = (FUNION (FUNION f g) h))``, 1976 SIMP_TAC std_ss [GSYM fmap_EQ_THM, FUNION_DEF, IN_UNION, EXTENSION] THEN 1977 METIS_TAC[]); 1978 1979val DRESTRICT_FUNION = store_thm ("DRESTRICT_FUNION", 1980 ``!h s1 s2. FUNION (DRESTRICT h s1) (DRESTRICT h s2) = 1981 DRESTRICT h (s1 UNION s2)``, 1982 SIMP_TAC std_ss [DRESTRICT_DEF, GSYM fmap_EQ_THM, EXTENSION, 1983 FUNION_DEF, IN_INTER, IN_UNION, DISJ_IMP_THM, 1984 LEFT_AND_OVER_OR]); 1985 1986 1987val DRESTRICT_EQ_FUNION = store_thm ("DRESTRICT_EQ_FUNION", 1988 ``!h h1 h2. DISJOINT (FDOM h1) (FDOM h2) /\ (FUNION h1 h2 = h) ==> 1989 (h2 = DRESTRICT h (COMPL (FDOM h1)))``, 1990 SIMP_TAC std_ss [DRESTRICT_DEF, GSYM fmap_EQ_THM, EXTENSION, 1991 FUNION_DEF, IN_INTER, IN_UNION, IN_COMPL, DISJOINT_DEF, 1992 NOT_IN_EMPTY] THEN 1993 METIS_TAC[]); 1994 1995 1996val IN_FDOM_FOLDR_UNION = store_thm ( 1997 "IN_FDOM_FOLDR_UNION", 1998 ``!x hL. x IN FDOM (FOLDR FUNION FEMPTY hL) <=> ?h. MEM h hL /\ x IN FDOM h``, 1999 Induct_on `hL` THENL [ 2000 SIMP_TAC list_ss [FDOM_FEMPTY, NOT_IN_EMPTY], 2001 2002 FULL_SIMP_TAC list_ss [FDOM_FUNION, IN_UNION, DISJ_IMP_THM] THEN 2003 METIS_TAC[] 2004 ]); 2005 2006 2007val DRESTRICT_FUNION_DRESTRICT_COMPL = store_thm ( 2008"DRESTRICT_FUNION_DRESTRICT_COMPL", 2009``FUNION (DRESTRICT f s) (DRESTRICT f (COMPL s)) = f ``, 2010 2011SIMP_TAC std_ss [GSYM fmap_EQ_THM, FUNION_DEF, DRESTRICT_DEF, 2012 EXTENSION, IN_INTER, IN_UNION, IN_COMPL] THEN 2013METIS_TAC[]); 2014 2015 2016 2017val DRESTRICT_IDEMPOT = store_thm ("DRESTRICT_IDEMPOT", 2018``!s vs. DRESTRICT (DRESTRICT s vs) vs = DRESTRICT s vs``, 2019SRW_TAC [][]); 2020val _ = export_rewrites ["DRESTRICT_IDEMPOT"] 2021 2022val SUBMAP_FUNION_ABSORPTION = store_thm( 2023"SUBMAP_FUNION_ABSORPTION", 2024``!f g. f SUBMAP g <=> (FUNION f g = g)``, 2025SRW_TAC[][SUBMAP_DEF,GSYM fmap_EQ_THM,EXTENSION,FUNION_DEF,EQ_IMP_THM] 2026THEN PROVE_TAC[]) 2027 2028(*--------------------------------------------------------------------------- 2029mapping an injective function over the keys of a finite map 2030 ---------------------------------------------------------------------------*) 2031 2032val MAP_KEYS_q =` 2033\f fm. if INJ f (FDOM fm) UNIV then 2034fm f_o_f (FUN_FMAP (LINV f (FDOM fm)) (IMAGE f (FDOM fm))) 2035else FUN_FMAP ARB (IMAGE f (FDOM fm))` 2036 2037val MAP_KEYS_witness = store_thm( 2038"MAP_KEYS_witness", 2039``let m = ^(Term MAP_KEYS_q) in 2040!f fm. (FDOM (m f fm) = IMAGE f (FDOM fm)) /\ 2041 ((INJ f (FDOM fm) UNIV) ==> 2042 (!x. x IN FDOM fm ==> (((m f fm) ' (f x)) = (fm ' x))))``, 2043SIMP_TAC (srw_ss()) [LET_THM] THEN 2044REPEAT GEN_TAC THEN 2045CONJ_ASM1_TAC THEN1 ( 2046 SRW_TAC[][f_o_f_DEF, 2047 GSYM SUBSET_INTER_ABSORPTION, 2048 SUBSET_DEF,FUN_FMAP_DEF] THEN 2049 IMP_RES_TAC LINV_DEF THEN 2050 SRW_TAC[][] ) THEN 2051SRW_TAC[][] THEN 2052FULL_SIMP_TAC (srw_ss()) [] THEN 2053Q.MATCH_ABBREV_TAC `(fm f_o_f z) ' (f x) = fm ' x` THEN 2054`f x IN FDOM (fm f_o_f z)` by ( 2055 SRW_TAC[][] THEN PROVE_TAC[] ) THEN 2056SRW_TAC[][f_o_f_DEF] THEN 2057Q.UNABBREV_TAC `z` THEN 2058Q.MATCH_ABBREV_TAC `fm ' ((FUN_FMAP z s) ' (f x)) = fm ' x` THEN 2059`f x IN s` by ( 2060 SRW_TAC[][Abbr`s`] THEN PROVE_TAC[] ) THEN 2061`FINITE s` by SRW_TAC[][Abbr`s`] THEN 2062SRW_TAC[][FUN_FMAP_DEF,Abbr`z`] THEN 2063IMP_RES_TAC LINV_DEF THEN 2064SRW_TAC[][]) 2065 2066val MAP_KEYS_exists = 2067Q.EXISTS (`$? ^(rand(rator(concl(MAP_KEYS_witness))))`,MAP_KEYS_q) 2068(BETA_RULE (PURE_REWRITE_RULE [LET_THM] MAP_KEYS_witness)) 2069 2070val MAP_KEYS_def = new_specification( 2071"MAP_KEYS_def",["MAP_KEYS"],MAP_KEYS_exists) 2072 2073val MAP_KEYS_FEMPTY = store_thm( 2074"MAP_KEYS_FEMPTY", 2075``!f. MAP_KEYS f FEMPTY = FEMPTY``, 2076SRW_TAC[][GSYM FDOM_EQ_EMPTY,MAP_KEYS_def]) 2077val _ = export_rewrites["MAP_KEYS_FEMPTY"] 2078 2079val MAP_KEYS_FUPDATE = store_thm( 2080"MAP_KEYS_FUPDATE", 2081``!f fm k v. (INJ f (k INSERT FDOM fm) UNIV) ==> 2082 (MAP_KEYS f (fm |+ (k,v)) = (MAP_KEYS f fm) |+ (f k,v))``, 2083SRW_TAC[][GSYM fmap_EQ_THM,MAP_KEYS_def] THEN 2084SRW_TAC[][MAP_KEYS_def,FAPPLY_FUPDATE_THM] THEN1 ( 2085 FULL_SIMP_TAC (srw_ss()) [INJ_DEF] THEN 2086 PROVE_TAC[] ) THEN 2087FULL_SIMP_TAC (srw_ss()) [INJ_INSERT] THEN 2088SRW_TAC[][MAP_KEYS_def]) 2089 2090val MAP_KEYS_using_LINV = store_thm( 2091"MAP_KEYS_using_LINV", 2092``!f fm. INJ f (FDOM fm) UNIV ==> 2093 (MAP_KEYS f fm = fm f_o_f (FUN_FMAP (LINV f (FDOM fm)) (IMAGE f (FDOM fm))))``, 2094SRW_TAC[][GSYM fmap_EQ_THM,MAP_KEYS_def] THEN 2095MP_TAC MAP_KEYS_witness THEN 2096SRW_TAC[][LET_THM] THEN 2097POP_ASSUM (Q.SPECL_THEN [`f`,`fm`] MP_TAC) THEN 2098SRW_TAC[][MAP_KEYS_def]) 2099 2100val MAP_KEYS_BIJ_LINV = Q.store_thm("MAP_KEYS_BIJ_LINV", 2101 `BIJ (f:num->num) UNIV UNIV ==> (MAP_KEYS f (MAP_KEYS (LINV f UNIV) t) = t)`, 2102 srw_tac[][fmap_EXT,MAP_KEYS_def,PULL_EXISTS,GSYM IMAGE_COMPOSE] 2103 \\ `f o LINV f UNIV = I` by 2104 (imp_res_tac BIJ_LINV_INV \\ full_simp_tac(srw_ss())[combinTheory.o_DEF,FUN_EQ_THM]) 2105 \\ full_simp_tac(srw_ss())[] \\ full_simp_tac(srw_ss())[combinTheory.o_DEF,FUN_EQ_THM] 2106 \\ imp_res_tac BIJ_LINV_BIJ \\ full_simp_tac(srw_ss())[BIJ_DEF] 2107 \\ `INJ f (FDOM (MAP_KEYS (LINV f UNIV) t)) UNIV` by full_simp_tac(srw_ss())[INJ_DEF] 2108 \\ first_assum(mp_tac o MATCH_MP (ONCE_REWRITE_RULE[GSYM AND_IMP_INTRO] 2109 (MAP_KEYS_def |> SPEC_ALL |> CONJUNCT2 |> MP_CANON))) 2110 \\ `?y. x' = f y` by (full_simp_tac(srw_ss())[SURJ_DEF] \\ metis_tac []) \\ srw_tac[][] 2111 \\ pop_assum (qspec_then `y` mp_tac) 2112 \\ impl_tac THEN1 2113 (full_simp_tac(srw_ss())[MAP_KEYS_def] \\ qexists_tac `f y` \\ full_simp_tac(srw_ss())[] 2114 \\ imp_res_tac LINV_DEF \\ full_simp_tac(srw_ss())[]) \\ srw_tac[][] 2115 \\ `INJ (LINV f UNIV) (FDOM t) UNIV` by 2116 (qpat_x_assum `INJ (LINV f UNIV) UNIV UNIV` mp_tac \\ simp [INJ_DEF]) 2117 \\ imp_res_tac (MAP_KEYS_def |> SPEC_ALL |> CONJUNCT2 |> MP_CANON) 2118 \\ imp_res_tac LINV_DEF \\ full_simp_tac(srw_ss())[]); 2119 2120val FLOOKUP_MAP_KEYS = Q.store_thm("FLOOKUP_MAP_KEYS", 2121 `INJ f (FDOM m) UNIV ==> 2122 (FLOOKUP (MAP_KEYS f m) k = 2123 OPTION_BIND (some x. (k = f x) /\ x IN FDOM m) (FLOOKUP m))`, 2124 strip_tac >> DEEP_INTRO_TAC optionTheory.some_intro >> 2125 simp[FLOOKUP_DEF,MAP_KEYS_def]); 2126 2127val FLOOKUP_MAP_KEYS_MAPPED = Q.store_thm("FLOOKUP_MAP_KEYS_MAPPED", 2128 `INJ f UNIV UNIV ==> 2129 (FLOOKUP (MAP_KEYS f m) (f k) = FLOOKUP m k)`, 2130 strip_tac >> 2131 `INJ f (FDOM m) UNIV` by metis_tac[INJ_SUBSET,SUBSET_UNIV,SUBSET_REFL] >> 2132 simp[FLOOKUP_MAP_KEYS] >> 2133 DEEP_INTRO_TAC optionTheory.some_intro >> srw_tac[][] >> 2134 full_simp_tac(srw_ss())[INJ_DEF] >> full_simp_tac(srw_ss())[FLOOKUP_DEF] >> metis_tac[]); 2135 2136val DRESTRICT_MAP_KEYS_IMAGE = Q.store_thm("DRESTRICT_MAP_KEYS_IMAGE", 2137 `INJ f UNIV UNIV ==> 2138 (DRESTRICT (MAP_KEYS f fm) (IMAGE f s) = MAP_KEYS f (DRESTRICT fm s))`, 2139 srw_tac[][FLOOKUP_EXT,FLOOKUP_DRESTRICT,FUN_EQ_THM] >> 2140 dep_rewrite.DEP_REWRITE_TAC[FLOOKUP_MAP_KEYS,FDOM_DRESTRICT] >> 2141 conj_tac >- ( metis_tac[IN_INTER,IN_UNIV,INJ_DEF] ) >> 2142 DEEP_INTRO_TAC optionTheory.some_intro >> 2143 DEEP_INTRO_TAC optionTheory.some_intro >> 2144 srw_tac[][FLOOKUP_DRESTRICT] >> srw_tac[][] >> full_simp_tac(srw_ss())[] >> 2145 metis_tac[INJ_DEF,IN_UNIV]); 2146 2147val DOMSUB_MAP_KEYS = Q.store_thm("DOMSUB_MAP_KEYS", 2148 `BIJ f UNIV UNIV ==> 2149 ((MAP_KEYS f fm) \\ (f s) = MAP_KEYS f (fm \\ s))`, 2150 srw_tac[][fmap_domsub] >> 2151 dep_rewrite.DEP_REWRITE_TAC[GSYM DRESTRICT_MAP_KEYS_IMAGE] >> 2152 srw_tac[][] >- full_simp_tac(srw_ss())[BIJ_DEF] >> 2153 AP_TERM_TAC >> 2154 srw_tac[][EXTENSION] >> 2155 full_simp_tac(srw_ss())[BIJ_DEF,INJ_DEF,SURJ_DEF] >> 2156 metis_tac[]); 2157 2158(* Relate the values in two finite maps *) 2159 2160val fmap_rel_def = Define` 2161 fmap_rel R f1 f2 <=> 2162 FDOM f2 = FDOM f1 /\ (!x. x IN FDOM f1 ==> R (f1 ' x) (f2 ' x))` 2163 2164val fmap_rel_FUPDATE_same = store_thm( 2165"fmap_rel_FUPDATE_same", 2166``fmap_rel R f1 f2 /\ R v1 v2 ==> fmap_rel R (f1 |+ (k,v1)) (f2 |+ (k,v2))``, 2167SRW_TAC[][fmap_rel_def,FAPPLY_FUPDATE_THM] THEN SRW_TAC[][]) 2168 2169val fmap_rel_FUPDATE_LIST_same = store_thm( 2170"fmap_rel_FUPDATE_LIST_same", 2171``!R ls1 ls2 f1 f2. 2172 fmap_rel R f1 f2 /\ (MAP FST ls1 = MAP FST ls2) /\ (LIST_REL R (MAP SND ls1) (MAP SND ls2)) 2173 ==> fmap_rel R (f1 |++ ls1) (f2 |++ ls2)``, 2174GEN_TAC THEN 2175Induct THEN Cases THEN SRW_TAC[][FUPDATE_LIST_THM,listTheory.LIST_REL_CONS1] THEN 2176Cases_on `ls2` THEN FULL_SIMP_TAC(srw_ss())[FUPDATE_LIST_THM] THEN 2177FIRST_X_ASSUM MATCH_MP_TAC THEN FULL_SIMP_TAC(srw_ss())[] THEN SRW_TAC[][] THEN 2178Q.MATCH_ASSUM_RENAME_TAC `R a (SND b)` THEN 2179Cases_on `b` THEN FULL_SIMP_TAC(srw_ss())[] THEN 2180SRW_TAC[][fmap_rel_FUPDATE_same]) 2181 2182val fmap_rel_FEMPTY = store_thm( 2183"fmap_rel_FEMPTY", 2184``fmap_rel R FEMPTY FEMPTY``, 2185SRW_TAC[][fmap_rel_def]) 2186val _ = export_rewrites["fmap_rel_FEMPTY"] 2187 2188val fmap_rel_FEMPTY2 = store_thm( 2189 "fmap_rel_FEMPTY2", 2190 ``(fmap_rel R FEMPTY f <=> (f = FEMPTY)) /\ 2191 (fmap_rel R f FEMPTY <=> (f = FEMPTY))``, 2192 SRW_TAC [][fmap_rel_def, FDOM_EQ_EMPTY, EQ_IMP_THM] THEN 2193 METIS_TAC [FDOM_EQ_EMPTY]); 2194val _ = export_rewrites ["fmap_rel_FEMPTY2"] 2195 2196val fmap_rel_refl = store_thm( 2197"fmap_rel_refl", 2198``(!x. R x x) ==> fmap_rel R x x``, 2199SRW_TAC[][fmap_rel_def]) 2200val _ = export_rewrites["fmap_rel_refl"] 2201 2202val fmap_rel_FUNION_rels = store_thm( 2203"fmap_rel_FUNION_rels", 2204``fmap_rel R f1 f2 /\ fmap_rel R f3 f4 ==> fmap_rel R (FUNION f1 f3) (FUNION f2 f4)``, 2205SRW_TAC[][fmap_rel_def,FUNION_DEF] THEN SRW_TAC[][]) 2206 2207val fmap_rel_FUPDATE_I = store_thm( 2208 "fmap_rel_FUPDATE_I", 2209 ``fmap_rel R (f1 \\ k) (f2 \\ k) /\ R v1 v2 ==> 2210 fmap_rel R (f1 |+ (k,v1)) (f2 |+ (k,v2))``, 2211 SRW_TAC[][fmap_rel_def] THENL [ 2212 Q.PAT_X_ASSUM `FDOM X DELETE EE = FDOM Y DELETE FF` MP_TAC THEN 2213 SRW_TAC [][EXTENSION] THEN METIS_TAC [], 2214 SRW_TAC [][], 2215 FULL_SIMP_TAC (srw_ss()) [DOMSUB_FAPPLY_THM] THEN 2216 SRW_TAC[][FAPPLY_FUPDATE_THM] 2217 ]); 2218 2219val fmap_rel_mono = store_thm( 2220 "fmap_rel_mono", 2221 ``(!x y. R1 x y ==> R2 x y) ==> fmap_rel R1 f1 f2 ==> fmap_rel R2 f1 f2``, 2222 SRW_TAC [][fmap_rel_def]); 2223val _ = export_mono "fmap_rel_mono" 2224 2225val fmap_rel_OPTREL_FLOOKUP = store_thm("fmap_rel_OPTREL_FLOOKUP", 2226 ``fmap_rel R f1 f2 = !k. OPTREL R (FLOOKUP f1 k) (FLOOKUP f2 k)``, 2227 rw[fmap_rel_def,optionTheory.OPTREL_def,FLOOKUP_DEF,EXTENSION] >> 2228 PROVE_TAC[]); 2229 2230val fmap_rel_FLOOKUP_E = Q.store_thm("fmap_rel_FLOOKUP_imp", 2231 `fmap_rel R f1 f2 ==> 2232 (!k. FLOOKUP f1 k = NONE ==> FLOOKUP f2 k = NONE) /\ 2233 (!k v1. FLOOKUP f1 k = SOME v1 ==> ?v2. FLOOKUP f2 k = SOME v2 /\ R v1 v2)`, 2234 rw[fmap_rel_OPTREL_FLOOKUP,optionTheory.OPTREL_def] >> 2235 first_x_assum(qspec_then`k`mp_tac) >> rw[]); 2236 2237(*--------------------------------------------------------------------------- 2238 Some helpers for fupdate_NORMALISE_CONV 2239 ---------------------------------------------------------------------------*) 2240 2241val fmap_EQ_UPTO_def = Define ` 2242 fmap_EQ_UPTO f1 f2 vs <=> 2243 (FDOM f1 INTER (COMPL vs) = FDOM f2 INTER (COMPL vs)) /\ 2244 (!x. x IN FDOM f1 INTER (COMPL vs) ==> (f1 ' x = f2 ' x))` 2245 2246val fmap_EQ_UPTO___EMPTY = store_thm ( 2247 "fmap_EQ_UPTO___EMPTY", 2248 ``!f1 f2. (fmap_EQ_UPTO f1 f2 EMPTY) = (f1 = f2)``, 2249 SIMP_TAC std_ss [fmap_EQ_UPTO_def, COMPL_EMPTY, INTER_UNIV, fmap_EQ_THM]); 2250val _ = export_rewrites ["fmap_EQ_UPTO___EMPTY"] 2251 2252val fmap_EQ_UPTO___EQ = store_thm ("fmap_EQ_UPTO___EQ", 2253``!vs f. (fmap_EQ_UPTO f f vs)``,SIMP_TAC std_ss [fmap_EQ_UPTO_def]) 2254val _ = export_rewrites ["fmap_EQ_UPTO___EQ"] 2255 2256val fmap_EQ_UPTO___FUPDATE_BOTH = store_thm ("fmap_EQ_UPTO___FUPDATE_BOTH", 2257``!f1 f2 ks k v. 2258 (fmap_EQ_UPTO f1 f2 ks) ==> 2259 (fmap_EQ_UPTO (f1 |+ (k,v)) (f2 |+ (k,v)) (ks DELETE k))``, 2260SIMP_TAC std_ss [fmap_EQ_UPTO_def, EXTENSION, IN_INTER, 2261 FDOM_FUPDATE, IN_COMPL, IN_INSERT, IN_DELETE] THEN 2262REPEAT GEN_TAC THEN STRIP_TAC THEN 2263CONJ_TAC THEN GEN_TAC THENL [ 2264 Cases_on `x = k` THEN ASM_REWRITE_TAC[], 2265 Cases_on `x = k` THEN ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM] 2266]); 2267 2268 2269val fmap_EQ_UPTO___FUPDATE_BOTH___NO_DELETE = store_thm ( 2270"fmap_EQ_UPTO___FUPDATE_BOTH___NO_DELETE", 2271``!f1 f2 ks k v. 2272 (fmap_EQ_UPTO f1 f2 ks) ==> 2273 (fmap_EQ_UPTO (f1 |+ (k,v)) (f2 |+ (k,v)) ks)``, 2274 2275SIMP_TAC std_ss [fmap_EQ_UPTO_def, EXTENSION, IN_INTER, 2276 FDOM_FUPDATE, IN_COMPL, IN_INSERT] THEN 2277REPEAT GEN_TAC THEN STRIP_TAC THEN 2278CONJ_TAC THEN GEN_TAC THENL [ 2279 Cases_on `x = k` THEN ASM_REWRITE_TAC[], 2280 Cases_on `x = k` THEN ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM] 2281]); 2282 2283 2284val fmap_EQ_UPTO___FUPDATE_SING = store_thm ("fmap_EQ_UPTO___FUPDATE_SING", 2285``!f1 f2 ks k v. 2286 (fmap_EQ_UPTO f1 f2 ks) ==> 2287 (fmap_EQ_UPTO (f1 |+ (k,v)) f2 (k INSERT ks))``, 2288 2289SIMP_TAC std_ss [fmap_EQ_UPTO_def, EXTENSION, IN_INTER, 2290 FDOM_FUPDATE, IN_COMPL, IN_INSERT, IN_DELETE] THEN 2291REPEAT GEN_TAC THEN STRIP_TAC THEN 2292CONJ_TAC THEN GEN_TAC THENL [ 2293 Cases_on `x = k` THEN ASM_REWRITE_TAC[], 2294 Cases_on `x = k` THEN ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM] 2295]); 2296 2297(*---------------------------------------------------------------------------*) 2298(* From Ramana Kumar *) 2299(*---------------------------------------------------------------------------*) 2300 2301val fmap_size_def = 2302 Define 2303 `fmap_size kz vz fm = SIGMA (\k. kz k + vz (fm ' k)) (FDOM fm)`; 2304 2305(*---------------------------------------------------------------------------*) 2306(* Various lemmas from the CakeML project https://cakeml.org *) 2307(*---------------------------------------------------------------------------*) 2308 2309local 2310 open optionTheory rich_listTheory listTheory boolSimps sortingTheory 2311in 2312 2313val o_f_FUNION = store_thm("o_f_FUNION", 2314 ``f o_f (FUNION f1 f2) = FUNION (f o_f f1) (f o_f f2)``, 2315 simp[GSYM fmap_EQ_THM,FUNION_DEF] >> 2316 rw[o_f_FAPPLY]); 2317 2318val FDOM_FOLDR_DOMSUB = store_thm("FDOM_FOLDR_DOMSUB", 2319 ``!ls fm. FDOM (FOLDR (\k m. m \\ k) fm ls) = FDOM fm DIFF set ls``, 2320 Induct >> simp[] >> 2321 ONCE_REWRITE_TAC[EXTENSION] >> 2322 simp[] >> metis_tac[]); 2323 2324val FEVERY_SUBMAP = store_thm("FEVERY_SUBMAP", 2325 ``FEVERY P fm /\ fm0 SUBMAP fm ==> FEVERY P fm0``, 2326 SRW_TAC[][FEVERY_DEF,SUBMAP_DEF]); 2327 2328val FEVERY_ALL_FLOOKUP = store_thm("FEVERY_ALL_FLOOKUP", 2329 ``!P f. FEVERY P f <=> !k v. (FLOOKUP f k = SOME v) ==> P (k,v)``, 2330 SRW_TAC[][FEVERY_DEF,FLOOKUP_DEF]); 2331 2332val FUPDATE_LIST_CANCEL = store_thm("FUPDATE_LIST_CANCEL", 2333 ``!ls1 fm ls2. 2334 (!k. MEM k (MAP FST ls1) ==> MEM k (MAP FST ls2)) 2335 ==> (fm |++ ls1 |++ ls2 = fm |++ ls2)``, 2336 Induct THEN SRW_TAC[][FUPDATE_LIST_THM] THEN 2337 Cases_on`h` THEN 2338 MATCH_MP_TAC FUPDATE_FUPDATE_LIST_MEM THEN 2339 FULL_SIMP_TAC(srw_ss())[]); 2340 2341val FUPDATE_EQ_FUNION = store_thm("FUPDATE_EQ_FUNION", 2342 ``!fm kv. fm |+ kv = FUNION (FEMPTY |+ kv) fm``, 2343 gen_tac >> Cases >> 2344 simp[GSYM fmap_EQ_THM,FDOM_FUPDATE,FAPPLY_FUPDATE_THM,FUNION_DEF] >> 2345 simp[EXTENSION]); 2346 2347val FUPDATE_LIST_APPEND_COMMUTES = store_thm("FUPDATE_LIST_APPEND_COMMUTES", 2348 ``!l1 l2 fm. DISJOINT (set (MAP FST l1)) (set (MAP FST l2)) ==> 2349 (fm |++ l1 |++ l2 = fm |++ l2 |++ l1)``, 2350 Induct >- rw[FUPDATE_LIST_THM] >> 2351 Cases >> rw[FUPDATE_LIST_THM] >> 2352 metis_tac[FUPDATE_FUPDATE_LIST_COMMUTES]); 2353 2354val FUPDATE_LIST_ALL_DISTINCT_PERM = store_thm("FUPDATE_LIST_ALL_DISTINCT_PERM", 2355 ``!ls ls' fm. ALL_DISTINCT (MAP FST ls) /\ PERM ls ls' ==> (fm |++ ls = fm |++ ls')``, 2356 Induct >> rw[] >> 2357 fs[sortingTheory.PERM_CONS_EQ_APPEND] >> 2358 rw[FUPDATE_LIST_THM] >> 2359 PairCases_on`h` >> fs[] >> 2360 imp_res_tac FUPDATE_FUPDATE_LIST_COMMUTES >> 2361 match_mp_tac EQ_TRANS >> 2362 qexists_tac `(fm |++ (M ++ N)) |+ (h0,h1)` >> 2363 conj_tac >- metis_tac[sortingTheory.ALL_DISTINCT_PERM,sortingTheory.PERM_MAP] >> 2364 rw[FUPDATE_LIST_APPEND] >> 2365 `h0 NOTIN set (MAP FST N)` 2366 by metis_tac[sortingTheory.PERM_MEM_EQ,MEM_MAP,MEM_APPEND] >> 2367 imp_res_tac FUPDATE_FUPDATE_LIST_COMMUTES >> 2368 rw[FUPDATE_LIST_THM]); 2369 2370val IMAGE_FRANGE = store_thm("IMAGE_FRANGE", 2371 ``!f fm. IMAGE f (FRANGE fm) = FRANGE (f o_f fm)``, 2372 SRW_TAC[][EXTENSION] THEN 2373 EQ_TAC THEN1 PROVE_TAC[o_f_FRANGE] THEN 2374 SRW_TAC[][FRANGE_DEF] THEN 2375 SRW_TAC[][o_f_FAPPLY] THEN 2376 PROVE_TAC[]); 2377 2378val SUBMAP_mono_FUPDATE = store_thm("SUBMAP_mono_FUPDATE", 2379 ``!f g x y. f \\ x SUBMAP g \\ x ==> f |+ (x,y) SUBMAP g |+ (x,y)``, 2380 SRW_TAC[][SUBMAP_FUPDATE]); 2381 2382val SUBMAP_DOMSUB_gen = store_thm("SUBMAP_DOMSUB_gen", 2383 ``!f g k. f \\ k SUBMAP g <=> f \\ k SUBMAP g \\ k``, 2384 SRW_TAC[][SUBMAP_DEF,EQ_IMP_THM,DOMSUB_FAPPLY_THM]); 2385 2386val DOMSUB_SUBMAP = store_thm("DOMSUB_SUBMAP", 2387 ``!f g x. f SUBMAP g /\ x NOTIN FDOM f ==> f SUBMAP g \\ x``, 2388 SRW_TAC[][SUBMAP_DEF,DOMSUB_FAPPLY_THM] THEN 2389 SRW_TAC[][] THEN METIS_TAC[]); 2390 2391val DRESTRICT_DOMSUB = store_thm("DRESTRICT_DOMSUB", 2392 ``!f s k. DRESTRICT f s \\ k = DRESTRICT f (s DELETE k)``, 2393 SRW_TAC[][GSYM fmap_EQ_THM,FDOM_DRESTRICT] THEN1 ( 2394 SRW_TAC[][EXTENSION] THEN METIS_TAC[] ) THEN 2395 SRW_TAC[][DOMSUB_FAPPLY_THM] THEN 2396 SRW_TAC[][DRESTRICT_DEF]); 2397 2398val DRESTRICT_SUBSET_SUBMAP_gen = store_thm("DRESTRICT_SUBSET_SUBMAP_gen", 2399 ``!f1 f2 s t. 2400 DRESTRICT f1 s SUBMAP DRESTRICT f2 s /\ t SUBSET s ==> 2401 DRESTRICT f1 t SUBMAP DRESTRICT f2 t``, 2402 rw[SUBMAP_DEF,DRESTRICT_DEF,SUBSET_DEF]) 2403 2404 2405val DRESTRICT_FUNION_SAME = store_thm("DRESTRICT_FUNION_SAME", 2406 ``!fm s. FUNION (DRESTRICT fm s) fm = fm``, 2407 SRW_TAC[][GSYM SUBMAP_FUNION_ABSORPTION]) 2408 2409val DRESTRICT_EQ_DRESTRICT_SAME = store_thm("DRESTRICT_EQ_DRESTRICT_SAME", 2410 ``(DRESTRICT f1 s = DRESTRICT f2 s) <=> 2411 (s INTER FDOM f1 = s INTER FDOM f2) /\ 2412 (!x. x IN FDOM f1 /\ x IN s ==> (f1 ' x = f2 ' x))``, 2413 SRW_TAC[][DRESTRICT_EQ_DRESTRICT,SUBMAP_DEF,DRESTRICT_DEF,EXTENSION] THEN 2414 PROVE_TAC[]) 2415 2416val FOLDL2_FUPDATE_LIST = store_thm( 2417"FOLDL2_FUPDATE_LIST", 2418``!f1 f2 bs cs a. (LENGTH bs = LENGTH cs) ==> 2419 (FOLDL2 (\fm b c. fm |+ (f1 b c, f2 b c)) a bs cs = 2420 a |++ ZIP (MAP2 f1 bs cs, MAP2 f2 bs cs))``, 2421SRW_TAC[][FUPDATE_LIST,FOLDL2_FOLDL,MAP2_MAP,ZIP_MAP,MAP_ZIP, 2422 rich_listTheory.FOLDL_MAP,listTheory.LENGTH_MAP2, 2423 LENGTH_ZIP,pairTheory.LAMBDA_PROD]) 2424 2425val FOLDL2_FUPDATE_LIST_paired = store_thm( 2426"FOLDL2_FUPDATE_LIST_paired", 2427``!f1 f2 bs cs a. (LENGTH bs = LENGTH cs) ==> 2428 (FOLDL2 (\fm b (c,d). fm |+ (f1 b c d, f2 b c d)) a bs cs = 2429 a |++ ZIP (MAP2 (\b. UNCURRY (f1 b)) bs cs, MAP2 (\b. UNCURRY (f2 b)) bs cs))``, 2430rw[FOLDL2_FOLDL,MAP2_MAP,ZIP_MAP,MAP_ZIP,LENGTH_ZIP, 2431 pairTheory.UNCURRY,pairTheory.LAMBDA_PROD,FUPDATE_LIST, 2432 rich_listTheory.FOLDL_MAP]) 2433 2434val DRESTRICT_FUNION_SUBSET = store_thm("DRESTRICT_FUNION_SUBSET", 2435 ``s2 SUBSET s1 ==> 2436 ?h. (FUNION (DRESTRICT f s1) g = FUNION (DRESTRICT f s2) h)``, 2437 strip_tac >> 2438 qexists_tac `FUNION (DRESTRICT f s1) g` >> 2439 match_mp_tac EQ_SYM >> 2440 REWRITE_TAC[GSYM SUBMAP_FUNION_ABSORPTION] >> 2441 rw[SUBMAP_DEF,DRESTRICT_DEF,FUNION_DEF] >> 2442 fs[SUBSET_DEF]) 2443 2444val FUPDATE_LIST_APPLY_NOT_MEM_matchable = store_thm( 2445"FUPDATE_LIST_APPLY_NOT_MEM_matchable", 2446``!kvl f k v. ~MEM k (MAP FST kvl) /\ (v = f ' k) ==> ((f |++ kvl) ' k = v)``, 2447PROVE_TAC[FUPDATE_LIST_APPLY_NOT_MEM]) 2448 2449val FUPDATE_LIST_APPLY_HO_THM = store_thm( 2450"FUPDATE_LIST_APPLY_HO_THM", 2451``!P f kvl k. 2452(?n. n < LENGTH kvl /\ (k = EL n (MAP FST kvl)) /\ P (EL n (MAP SND kvl)) /\ 2453 (!m. n < m /\ m < LENGTH kvl ==> EL m (MAP FST kvl) <> k)) \/ 2454(~MEM k (MAP FST kvl) /\ P (f ' k)) 2455==> (P ((f |++ kvl) ' k))``, 2456metis_tac[FUPDATE_LIST_APPLY_MEM,FUPDATE_LIST_APPLY_NOT_MEM]) 2457 2458val FUPDATE_SAME_APPLY = store_thm( 2459"FUPDATE_SAME_APPLY", 2460``(x = FST kv) \/ (fm1 ' x = fm2 ' x) ==> ((fm1 |+ kv) ' x = (fm2 |+ kv) ' x)``, 2461Cases_on `kv` >> rw[FAPPLY_FUPDATE_THM]) 2462 2463val FUPDATE_SAME_LIST_APPLY = store_thm( 2464"FUPDATE_SAME_LIST_APPLY", 2465``!kvl fm1 fm2 x. MEM x (MAP FST kvl) ==> ((fm1 |++ kvl) ' x = (fm2 |++ kvl) ' x)``, 2466ho_match_mp_tac SNOC_INDUCT >> 2467conj_tac >- rw[] >> 2468rw[FUPDATE_LIST,FOLDL_SNOC] >> 2469match_mp_tac FUPDATE_SAME_APPLY >> 2470qmatch_rename_tac `(y = FST p) \/ _` >> 2471Cases_on `y = FST p` >> rw[] >> 2472first_x_assum match_mp_tac >> 2473fs[MEM_MAP] >> 2474PROVE_TAC[]) 2475 2476val FUPDATE_LIST_ALL_DISTINCT_APPLY_MEM = store_thm( 2477"FUPDATE_LIST_ALL_DISTINCT_APPLY_MEM", 2478``!P ls k v fm. ALL_DISTINCT (MAP FST ls) /\ 2479 MEM (k,v) ls /\ 2480 P v ==> 2481 P ((fm |++ ls) ' k)``, 2482rw[] >> 2483ho_match_mp_tac FUPDATE_LIST_APPLY_HO_THM >> 2484disj1_tac >> 2485fs[EL_ALL_DISTINCT_EL_EQ,MEM_EL] >> 2486qpat_x_assum `(k,v) = X` (assume_tac o SYM) >> 2487qexists_tac `n` >> rw[EL_MAP] >> 2488first_x_assum (qspecl_then [`n`,`m`] mp_tac) >> 2489rw[EL_MAP] >> spose_not_then strip_assume_tac >> 2490rw[] >> fs[]) 2491 2492val FUPDATE_LIST_ALL_DISTINCT_REVERSE = store_thm("FUPDATE_LIST_ALL_DISTINCT_REVERSE", 2493 ``!ls. ALL_DISTINCT (MAP FST ls) ==> !fm. fm |++ (REVERSE ls) = fm |++ ls``, 2494 Induct >- rw[] >> 2495 qx_gen_tac `p` >> PairCases_on `p` >> 2496 rw[FUPDATE_LIST_APPEND,FUPDATE_LIST_THM] >> 2497 fs[] >> 2498 rw[FUPDATE_FUPDATE_LIST_COMMUTES]) 2499 2500(* FRANGE subset stuff *) 2501 2502val IN_FRANGE = store_thm( 2503"IN_FRANGE", 2504``!f v. v IN FRANGE f <=> ?k. k IN FDOM f /\ (f ' k = v)``, 2505SRW_TAC[][FRANGE_DEF]) 2506 2507val IN_FRANGE_FLOOKUP = store_thm("IN_FRANGE_FLOOKUP", 2508``!f v. v IN FRANGE f <=> ?k. FLOOKUP f k = SOME v``, 2509rw[IN_FRANGE,FLOOKUP_DEF]) 2510 2511val FRANGE_FUPDATE_LIST_SUBSET = store_thm( 2512"FRANGE_FUPDATE_LIST_SUBSET", 2513``!ls fm. FRANGE (fm |++ ls) SUBSET FRANGE fm UNION (set (MAP SND ls))``, 2514Induct >- rw[FUPDATE_LIST_THM] >> 2515qx_gen_tac `p` >> qx_gen_tac `fm` >> 2516pop_assum (qspec_then `fm |+ p` mp_tac) >> 2517srw_tac[DNF_ss][SUBSET_DEF] >> 2518first_x_assum (qspec_then `x` mp_tac) >> fs[FUPDATE_LIST_THM] >> 2519rw[] >> fs[] >> 2520PairCases_on `p` >> 2521fsrw_tac[DNF_ss][FRANGE_FLOOKUP,FLOOKUP_UPDATE] >> 2522pop_assum mp_tac >> rw[] >> 2523PROVE_TAC[]) 2524 2525val IN_FRANGE_FUPDATE_LIST_suff = store_thm( 2526"IN_FRANGE_FUPDATE_LIST_suff", 2527``(!v. v IN FRANGE fm ==> P v) /\ (!v. MEM v (MAP SND ls) ==> P v) ==> 2528 !v. v IN FRANGE (fm |++ ls) ==> P v``, 2529rw[] >> 2530imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_FUPDATE_LIST_SUBSET) >> 2531PROVE_TAC[]) 2532 2533val FRANGE_FUNION_SUBSET = store_thm( 2534"FRANGE_FUNION_SUBSET", 2535``FRANGE (FUNION f1 f2) SUBSET FRANGE f1 UNION FRANGE f2``, 2536srw_tac[DNF_ss][FRANGE_DEF,SUBSET_DEF,FUNION_DEF] >> 2537PROVE_TAC[]) 2538 2539val IN_FRANGE_FUNION_suff = store_thm( 2540"IN_FRANGE_FUNION_suff", 2541``(!v. v IN FRANGE f1 ==> P v) /\ (!v. v IN FRANGE f2 ==> P v) ==> 2542 (!v. v IN FRANGE (FUNION f1 f2) ==> P v)``, 2543rw[] >> 2544imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_FUNION_SUBSET) >> 2545PROVE_TAC[]) 2546 2547val FRANGE_DOMSUB_SUBSET = store_thm( 2548"FRANGE_DOMSUB_SUBSET", 2549``FRANGE (fm \\ k) SUBSET FRANGE fm``, 2550srw_tac[DNF_ss][FRANGE_DEF,SUBSET_DEF,DOMSUB_FAPPLY_THM] >> 2551PROVE_TAC[]) 2552 2553val IN_FRANGE_DOMSUB_suff = store_thm( 2554"IN_FRANGE_DOMSUB_suff", 2555``(!v. v IN FRANGE fm ==> P v) ==> (!v. v IN FRANGE (fm \\ k) ==> P v)``, 2556rw[] >> 2557imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_DOMSUB_SUBSET) >> 2558PROVE_TAC[]) 2559 2560val FRANGE_DRESTRICT_SUBSET = store_thm( 2561"FRANGE_DRESTRICT_SUBSET", 2562``FRANGE (DRESTRICT fm s) SUBSET FRANGE fm``, 2563srw_tac[DNF_ss][FRANGE_DEF,SUBSET_DEF,DRESTRICT_DEF] >> 2564PROVE_TAC[]) 2565 2566val IN_FRANGE_DRESTRICT_suff = store_thm( 2567"IN_FRANGE_DRESTRICT_suff", 2568``(!v. v IN FRANGE fm ==> P v) ==> (!v. v IN FRANGE (DRESTRICT fm s) ==> P v)``, 2569rw[] >> 2570imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_DRESTRICT_SUBSET) >> 2571PROVE_TAC[]) 2572 2573val FRANGE_FUPDATE_SUBSET = store_thm( 2574"FRANGE_FUPDATE_SUBSET", 2575``FRANGE (fm |+ kv) SUBSET FRANGE fm UNION {SND kv}``, 2576Cases_on `kv` >> 2577rw[FRANGE_DEF,SUBSET_DEF,DOMSUB_FAPPLY_THM] >> 2578rw[] >> PROVE_TAC[]) 2579 2580val IN_FRANGE_FUPDATE_suff = store_thm( 2581"IN_FRANGE_FUPDATE_suff", 2582`` (!v. v IN FRANGE fm ==> P v) /\ (P (SND kv)) 2583==> (!v. v IN FRANGE (fm |+ kv) ==> P v)``, 2584rw[] >> 2585imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_FUPDATE_SUBSET) >> 2586fs[]) 2587 2588val IN_FRANGE_o_f_suff = store_thm("IN_FRANGE_o_f_suff", 2589 ``(!v. v IN FRANGE fm ==> P (f v)) ==> !v. v IN FRANGE (f o_f fm) ==> P v``, 2590 rw[IN_FRANGE] >> rw[] >> first_x_assum match_mp_tac >> PROVE_TAC[]) 2591 2592(* DRESTRICT stuff *) 2593 2594val DRESTRICT_SUBMAP_gen = store_thm( 2595"DRESTRICT_SUBMAP_gen", 2596``f SUBMAP g ==> DRESTRICT f P SUBMAP g``, 2597SRW_TAC[][SUBMAP_DEF,DRESTRICT_DEF]) 2598 2599val DRESTRICT_SUBSET_SUBMAP = store_thm( 2600"DRESTRICT_SUBSET_SUBMAP", 2601``s1 SUBSET s2 ==> DRESTRICT f s1 SUBMAP DRESTRICT f s2``, 2602SRW_TAC[][SUBMAP_DEF,SUBSET_DEF,DRESTRICT_DEF]) 2603 2604val DRESTRICTED_FUNION = store_thm( 2605"DRESTRICTED_FUNION", 2606``!f1 f2 s. DRESTRICT (FUNION f1 f2) s = FUNION (DRESTRICT f1 s) (DRESTRICT f2 (s DIFF FDOM f1))``, 2607rw[GSYM fmap_EQ_THM,DRESTRICT_DEF,FUNION_DEF] >> rw[] >> 2608rw[EXTENSION] >> PROVE_TAC[]) 2609 2610val FRANGE_DRESTRICT_SUBSET = store_thm( 2611"FRANGE_DRESTRICT_SUBSET", 2612``FRANGE (DRESTRICT fm s) SUBSET FRANGE fm``, 2613SRW_TAC[][FRANGE_DEF,SUBSET_DEF,DRESTRICT_DEF] THEN 2614SRW_TAC[][] THEN PROVE_TAC[]) 2615 2616val DRESTRICT_FDOM = store_thm( 2617"DRESTRICT_FDOM", 2618``!f. DRESTRICT f (FDOM f) = f``, 2619SRW_TAC[][GSYM fmap_EQ_THM,DRESTRICT_DEF]) 2620 2621val DRESTRICT_SUBSET = store_thm("DRESTRICT_SUBSET", 2622 ``!f1 f2 s t. 2623 (DRESTRICT f1 s = DRESTRICT f2 s) /\ t SUBSET s ==> 2624 (DRESTRICT f1 t = DRESTRICT f2 t)``, 2625 rw[DRESTRICT_EQ_DRESTRICT] 2626 >- metis_tac[DRESTRICT_SUBSET_SUBMAP,SUBMAP_TRANS] 2627 >- metis_tac[DRESTRICT_SUBSET_SUBMAP,SUBMAP_TRANS] >> 2628 fsrw_tac[DNF_ss][SUBSET_DEF,EXTENSION] >> 2629 metis_tac[]) 2630 2631val f_o_f_FUPDATE_compose = store_thm("f_o_f_FUPDATE_compose", 2632 ``!f1 f2 k x v. x NOTIN FDOM f1 /\ x NOTIN FRANGE f2 ==> 2633 ((f1 |+ (x,v)) f_o_f (f2 |+ (k,x)) = (f1 f_o_f f2) |+ (k,v))``, 2634 rw[GSYM fmap_EQ_THM,f_o_f_DEF,FAPPLY_FUPDATE_THM] >> 2635 simp[] >> rw[] >> fs[] >> rw[EXTENSION] >> 2636 fs[IN_FRANGE] >> rw[] 2637 >- PROVE_TAC[] 2638 >- PROVE_TAC[] >> 2639 qmatch_assum_rename_tac`y <> k` >> 2640 `y IN FDOM (f1 f_o_f f2)` by rw[f_o_f_DEF] >> 2641 rw[f_o_f_DEF]) 2642 2643val fmap_rel_trans = store_thm("fmap_rel_trans", 2644 ``(!x y z. R x y /\ R y z ==> R x z) ==> 2645 !x y z. fmap_rel R x y /\ fmap_rel R y z ==> 2646 fmap_rel R x z``, 2647 SRW_TAC[][fmap_rel_def] THEN METIS_TAC[]) 2648 2649val fmap_rel_sym = store_thm("fmap_rel_sym", 2650 ``(!x y. R x y ==> R y x) ==> 2651 !x y. fmap_rel R x y ==> fmap_rel R y x``, 2652 SRW_TAC[][fmap_rel_def]) 2653 2654val fupdate_list_map = Q.store_thm ("fupdate_list_map", 2655`!l f x y. 2656 x IN FDOM (FEMPTY |++ l) 2657 ==> 2658 ((FEMPTY |++ MAP (\(a,b). (a, f b)) l) ' x = f ((FEMPTY |++ l) ' x))`, 2659 rpt gen_tac >> 2660 Q.ISPECL_THEN[`FST`,`f o SND`,`l`,`FEMPTY:'a|->'c`]mp_tac(GSYM FOLDL_FUPDATE_LIST) >> 2661 simp[LAMBDA_PROD] >> 2662 disch_then kall_tac >> 2663 qid_spec_tac`l` >> 2664 ho_match_mp_tac SNOC_INDUCT >> 2665 simp[FUPDATE_LIST_THM] >> 2666 simp[FOLDL_SNOC,FORALL_PROD,FAPPLY_FUPDATE_THM,FDOM_FUPDATE_LIST,MAP_SNOC,FUPDATE_LIST_SNOC] >> 2667 rw[] >> rw[]) 2668 2669val fdom_fupdate_list2 = Q.store_thm ("fdom_fupdate_list2", 2670`!kvl fm. FDOM (fm |++ kvl) = (FDOM fm DIFF set (MAP FST kvl)) UNION set (MAP FST kvl)`, 2671rw [FDOM_FUPDATE_LIST, EXTENSION] >> 2672metis_tac []); 2673 2674val flookup_thm = Q.store_thm ("flookup_thm", 2675`!f x v. ((FLOOKUP f x = NONE) = (x NOTIN FDOM f)) /\ 2676 ((FLOOKUP f x = SOME v) = (x IN FDOM f /\ (f ' x = v)))`, 2677rw [FLOOKUP_DEF]); 2678 2679val FUPDATE_EQ_FUPDATE_LIST = store_thm("FUPDATE_EQ_FUPDATE_LIST", 2680 ``!fm kv. fm |+ kv = fm |++ [kv]``, 2681 rw[FUPDATE_LIST_THM]); 2682 2683val fmap_inverse_def = Define ` 2684fmap_inverse m1 m2 = 2685 !k. k IN FDOM m1 ==> ?v. (FLOOKUP m1 k = SOME v) /\ (FLOOKUP m2 v = SOME k)`; 2686 2687val fupdate_list_foldr = Q.store_thm ("fupdate_list_foldr", 2688`!m l. FOLDR (\(k,v) env. env |+ (k,v)) m l = m |++ REVERSE l`, 2689 Induct_on `l` >> 2690 rw [FUPDATE_LIST] >> 2691 PairCases_on `h` >> 2692 rw [FOLDL_APPEND]); 2693 2694val fupdate_list_foldl = Q.store_thm ("fupdate_list_foldl", 2695`!m l. FOLDL (\env (k,v). env |+ (k,v)) m l = m |++ l`, 2696 Induct_on `l` >> 2697 rw [FUPDATE_LIST] >> 2698 PairCases_on `h` >> 2699 rw []); 2700 2701val fmap_to_list = Q.store_thm ("fmap_to_list", 2702`!m. ?l. ALL_DISTINCT (MAP FST l) /\ (m = FEMPTY |++ l)`, 2703ho_match_mp_tac fmap_INDUCT >> 2704rw [FUPDATE_LIST_THM] >| 2705[qexists_tac `[]` >> 2706 rw [FUPDATE_LIST_THM], 2707 qexists_tac `(x,y)::l` >> 2708 rw [FUPDATE_LIST_THM] >> 2709 fs [FDOM_FUPDATE_LIST] >> 2710 rw [FUPDATE_FUPDATE_LIST_COMMUTES] >> 2711 fs [LIST_TO_SET_MAP] >> 2712 metis_tac [FST]]); 2713 2714val disjoint_drestrict = Q.store_thm ("disjoint_drestrict", 2715`!s m. DISJOINT s (FDOM m) ==> (DRESTRICT m (COMPL s) = m)`, 2716 rw [FLOOKUP_EXT, FLOOKUP_DRESTRICT, FUN_EQ_THM] >> 2717 Cases_on `k NOTIN s` >> 2718 rw [] >> 2719 fs [DISJOINT_DEF, EXTENSION, FLOOKUP_DEF] >> 2720 metis_tac []); 2721 2722val drestrict_iter_list = Q.store_thm ("drestrict_iter_list", 2723`!m l. FOLDR (\k m. m \\ k) m l = DRESTRICT m (COMPL (set l))`, 2724 Induct_on `l` >> 2725 rw [DRESTRICT_UNIV, DRESTRICT_DOMSUB] >> 2726 match_mp_tac (PROVE [] ``(y = y') ==> (f x y = f x y')``) >> 2727 rw [EXTENSION] >> 2728 metis_tac []); 2729 2730val fevery_funion = Q.store_thm ("fevery_funion", 2731`!P m1 m2. FEVERY P m1 /\ FEVERY P m2 ==> FEVERY P (FUNION m1 m2)`, 2732 rw [FEVERY_ALL_FLOOKUP, FLOOKUP_FUNION] >> 2733 BasicProvers.EVERY_CASE_TAC >> 2734 fs []); 2735 2736 (* Sorting stuff *) 2737 2738val FUPDATE_LIST_ALL_DISTINCT_PERM = store_thm("FUPDATE_LIST_ALL_DISTINCT_PERM", 2739 ``!ls ls' fm. ALL_DISTINCT (MAP FST ls) /\ PERM ls ls' ==> (fm |++ ls = fm |++ ls')``, 2740 Induct >> rw[] >> 2741 fs[PERM_CONS_EQ_APPEND] >> 2742 rw[FUPDATE_LIST_THM] >> 2743 PairCases_on`h` >> fs[] >> 2744 imp_res_tac FUPDATE_FUPDATE_LIST_COMMUTES >> 2745 match_mp_tac EQ_TRANS >> 2746 qexists_tac `(fm |++ (M ++ N)) |+ (h0,h1)` >> 2747 conj_tac >- metis_tac[ALL_DISTINCT_PERM,PERM_MAP] >> 2748 rw[FUPDATE_LIST_APPEND] >> 2749 `h0 NOTIN set (MAP FST N)` by metis_tac[PERM_MEM_EQ,MEM_MAP,MEM_APPEND] >> 2750 imp_res_tac FUPDATE_FUPDATE_LIST_COMMUTES >> 2751 rw[FUPDATE_LIST_THM]); 2752 2753 2754end 2755(* end CakeML lemmas *) 2756 2757(*---------------------------------------------------------------------------*) 2758(* Add fmap type to the TypeBase. Notice that we treat keys as being of size *) 2759(* zero, and make sure to add one to the size of each mapped value. This *) 2760(* ought to handle the case where the map points to something of size 0: *) 2761(* deleting it from the map will then make the map smaller. *) 2762(*---------------------------------------------------------------------------*) 2763 2764val _ = adjoin_to_theory 2765 {sig_ps = NONE, 2766 struct_ps = SOME (fn _ => 2767 PP.block PP.CONSISTENT 0 ( 2768 PP.pr_list PP.add_string [PP.NL] [ 2769 "val _ = ", 2770 " TypeBase.write", 2771 " [TypeBasePure.mk_nondatatype_info", 2772 " (mk_type(\"fmap\",[alpha,beta]),", 2773 " {nchotomy = SOME fmap_CASES,", 2774 " induction = SOME fmap_INDUCT,", 2775 " size = SOME(Parse.Term`\\(ksize:'a->num) (vsize:'b->num). \ 2776 \fmap_size (\\k:'a. 0) (\\v. 1 + vsize v)`,", 2777 " fmap_size_def),", 2778 " encode=NONE})];" 2779 ] 2780 ))} 2781 2782(* ---------------------------------------------------------------------- 2783 to close... 2784 ---------------------------------------------------------------------- *) 2785 2786val _ = export_theory(); 2787