finite_mapScript.sml
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
29Theory finite_map
30Ancestors
31 pred_set sum pair relation list[qualified] rich_list[qualified]
32 option[qualified] sorting[qualified]
33Libs
34 IndDefLib numLib metisLib simpLib BasicProvers bnfBase
35 pred_setLib[qualified] boolSimps[qualified]
36
37(* the bound is a cardinality, and cardinalityCoreTheory makes no
38 grammar of its own; this is kept to itself so that a theory
39 declaring a datatype does not inherit the notation *)
40Overload "<<="[local] = “cardleq”
41
42
43(*---------------------------------------------------------------------------*)
44(* Special notation. fmap application is set at the same level as function *)
45(* application, meaning that *)
46(* *)
47(* * SOME (f ' x) prints as SOME (f ' x) *)
48(* * (f x) ' y prints as f x ' y *)
49(* * (f ' x) y prints as f ' x y *)
50(* * f ' (x y) prints as f ' (x y) *)
51(* *)
52(* I think this is clearly best. *)
53(*---------------------------------------------------------------------------*)
54
55val _ = set_fixity "'" (Infixl 2000); (* fmap application *)
56
57val _ = set_fixity "|+" (Infixl 600); (* fmap update *)
58val _ = set_fixity "|++" (Infixl 500); (* iterated update *)
59
60
61(*---------------------------------------------------------------------------
62 Definition of a finite map
63
64 The representation is the type 'a -> ('b + one) where only a finite
65 number of the 'a map to a 'b and the rest map to one. We define a
66 notion of finiteness inductively.
67 --------------------------------------------------------------------------- *)
68
69val (rules,ind,cases) =
70 Hol_reln `is_fmap (\a. INR one)
71 /\ (!f a b. is_fmap f ==> is_fmap (\x. if x=a then INL b else f x))`;
72
73
74val rule_list as [is_fmap_empty, is_fmap_update] = CONJUNCTS rules;
75
76val strong_ind = derive_strong_induction(rules, ind);
77
78
79(*---------------------------------------------------------------------------
80 Existence theorem; type definition
81 ---------------------------------------------------------------------------*)
82
83Theorem EXISTENCE_THM[local]:
84 ?x:'a -> 'b + one. is_fmap x
85Proof
86EXISTS_TAC (Term`\x:'a. (INR one):'b + one`)
87 THEN REWRITE_TAC [is_fmap_empty]
88QED
89
90val fmap_TY_DEF = new_type_definition("fmap", EXISTENCE_THM);
91
92val _ = add_infix_type
93 {Prec = 50,
94 ParseName = SOME "|->",
95 Assoc = RIGHT,
96 Name = "fmap"};
97
98(* --------------------------------------------------------------------- *)
99(* Define bijections *)
100(* --------------------------------------------------------------------- *)
101
102val fmap_ISO_DEF =
103 define_new_type_bijections
104 {name = "fmap_ISO_DEF",
105 ABS = "fmap_ABS",
106 REP = "fmap_REP",
107 tyax = fmap_TY_DEF};
108
109(* --------------------------------------------------------------------- *)
110(* Prove that REP is one-to-one. *)
111(* --------------------------------------------------------------------- *)
112
113val fmap_REP_11 = prove_rep_fn_one_one fmap_ISO_DEF
114val fmap_REP_onto = prove_rep_fn_onto fmap_ISO_DEF
115val fmap_ABS_11 = prove_abs_fn_one_one fmap_ISO_DEF
116val fmap_ABS_onto = prove_abs_fn_onto fmap_ISO_DEF;
117
118val (fmap_ABS_REP_THM,fmap_REP_ABS_THM) =
119 let val thms = CONJUNCTS fmap_ISO_DEF
120 val [t1,t2] = map (GEN_ALL o SYM o SPEC_ALL) thms
121 in (t1,t2)
122 end;
123
124
125(*---------------------------------------------------------------------------
126 CANCELLATION THEOREMS
127 ---------------------------------------------------------------------------*)
128
129Theorem is_fmap_REP[local]:
130 !f:'a |-> 'b. is_fmap (fmap_REP f)
131Proof
132 REWRITE_TAC [fmap_REP_onto]
133 THEN GEN_TAC THEN Q.EXISTS_TAC `f`
134 THEN REWRITE_TAC [fmap_REP_11]
135QED
136
137Theorem REP_ABS_empty[local]:
138 fmap_REP (fmap_ABS ((\a. INR one):'a -> 'b + one)) = \a. INR one
139Proof
140 REWRITE_TAC [fmap_REP_ABS_THM]
141 THEN REWRITE_TAC [is_fmap_empty]
142QED
143
144Theorem REP_ABS_update[local]:
145 !(f:'a |-> 'b) x y.
146 fmap_REP (fmap_ABS (\a. if a=x then INL y else fmap_REP f a))
147 =
148 \a. if a=x then INL y else fmap_REP f a
149Proof
150 REPEAT GEN_TAC
151 THEN REWRITE_TAC [fmap_REP_ABS_THM]
152 THEN MATCH_MP_TAC is_fmap_update
153 THEN REWRITE_TAC [is_fmap_REP]
154QED
155
156Theorem is_fmap_REP_ABS[local]:
157 !f:'a -> 'b + one. is_fmap f ==> (fmap_REP (fmap_ABS f) = f)
158Proof
159 REPEAT STRIP_TAC
160 THEN REWRITE_TAC [fmap_REP_ABS_THM]
161 THEN ASM_REWRITE_TAC []
162QED
163
164
165(*---------------------------------------------------------------------------
166 DEFINITIONS OF UPDATE, EMPTY, APPLY and DOMAIN
167 ---------------------------------------------------------------------------*)
168
169Definition FUPDATE_DEF[nocompute]:
170 FUPDATE (f:'a |-> 'b) (x,y)
171 = fmap_ABS (\a. if a=x then INL y else fmap_REP f a)
172End
173
174Overload "|+" = “FUPDATE”
175
176Definition FEMPTY_DEF[nocompute]:
177 (FEMPTY:'a |-> 'b) = fmap_ABS (\a. INR one)
178End
179
180Definition FAPPLY_DEF[nocompute]:
181 FAPPLY (f:'a |-> 'b) x = OUTL (fmap_REP f x)
182End
183
184Overload "'" = “FAPPLY”
185Overload FAPPLY = “FAPPLY”
186
187Definition FDOM_DEF[nocompute]:
188 FDOM (f:'a |-> 'b) x = ISL (fmap_REP f x)
189End
190
191val update_rep = Term`\(f:'a->'b+one) x y. \a. if a=x then INL y else f a`;
192
193val empty_rep = Term`(\a. INR one):'a -> 'b + one`;
194
195Overload fmupdate = “λk v fm. fm |+ (k,v)”
196val _ = combinpp.new_form {
197 left = "⟨", right = "⟩", upd_term_name = (“FUPDATE f (k,v)”, "fmupdate"),
198 lookup_term_name = SOME (“fm ' k”, "FAPPLY")
199 };
200
201
202
203(*---------------------------------------------------------------------------
204 Now some theorems
205 --------------------------------------------------------------------------- *)
206
207Theorem FAPPLY_FUPDATE[simp]:
208 !(f:'a |-> 'b) x y. FAPPLY (FUPDATE f (x,y)) x = y
209Proof
210 REWRITE_TAC [FUPDATE_DEF, FAPPLY_DEF]
211 THEN REPEAT GEN_TAC
212 THEN REWRITE_TAC [REP_ABS_update] THEN BETA_TAC
213 THEN REWRITE_TAC [sumTheory.OUTL]
214QED
215
216
217Theorem NOT_EQ_FAPPLY:
218 !(f:'a|-> 'b) a x y . ~(a=x) ==> (FAPPLY (FUPDATE f (x,y)) a = FAPPLY f a)
219Proof
220REPEAT STRIP_TAC
221 THEN REWRITE_TAC [FUPDATE_DEF, FAPPLY_DEF, REP_ABS_update] THEN BETA_TAC
222 THEN ASM_REWRITE_TAC []
223QED
224
225val update_commutes_rep = (BETA_RULE o BETA_RULE) (Q.prove
226(`!(f:'a -> 'b + one) a b c d.
227 ~(a = c)
228 ==>
229 (^update_rep (^update_rep f a b) c d = ^update_rep (^update_rep f c d) a b)`,
230REPEAT STRIP_TAC THEN BETA_TAC
231 THEN MATCH_MP_TAC EQ_EXT
232 THEN GEN_TAC
233 THEN Q.ASM_CASES_TAC `x = a` THEN BETA_TAC
234 THEN ASM_REWRITE_TAC []));
235
236
237Theorem FUPDATE_COMMUTES:
238 !(f:'a |-> 'b) a b c d.
239 ~(a = c)
240 ==>
241 (FUPDATE (FUPDATE f (a,b)) (c,d) = FUPDATE (FUPDATE f (c,d)) (a,b))
242Proof
243REPEAT STRIP_TAC
244 THEN REWRITE_TAC [FUPDATE_DEF, REP_ABS_update] THEN BETA_TAC
245 THEN AP_TERM_TAC
246 THEN MATCH_MP_TAC EQ_EXT
247 THEN GEN_TAC
248 THEN Q.ASM_CASES_TAC `x = a` THEN BETA_TAC
249 THEN ASM_REWRITE_TAC []
250QED
251
252val update_same_rep = (BETA_RULE o BETA_RULE) (Q.prove
253(`!(f:'a -> 'b+one) a b c.
254 ^update_rep (^update_rep f a b) a c = ^update_rep f a c`,
255BETA_TAC THEN REPEAT GEN_TAC
256 THEN MATCH_MP_TAC EQ_EXT
257 THEN GEN_TAC
258 THEN Q.ASM_CASES_TAC `x = a` THEN BETA_TAC
259 THEN ASM_REWRITE_TAC []));
260
261Theorem FUPDATE_EQ[simp]:
262 !(f:'a |-> 'b) a b c. FUPDATE (FUPDATE f (a,b)) (a,c) = FUPDATE f (a,c)
263Proof
264REPEAT STRIP_TAC
265 THEN REWRITE_TAC [FUPDATE_DEF, REP_ABS_update] THEN BETA_TAC
266 THEN AP_TERM_TAC
267 THEN MATCH_MP_TAC EQ_EXT
268 THEN GEN_TAC
269 THEN Q.ASM_CASES_TAC `x = a` THEN BETA_TAC
270 THEN ASM_REWRITE_TAC []
271QED
272
273
274Theorem lemma1[local]:
275 ~((ISL :'b + one -> bool) ((INR :one -> 'b + one) one))
276Proof
277 REWRITE_TAC [sumTheory.ISL]
278QED
279
280Theorem FDOM_FEMPTY[simp]:
281 FDOM (FEMPTY:'a |-> 'b) = {}
282Proof
283REWRITE_TAC [EXTENSION, NOT_IN_EMPTY] THEN
284REWRITE_TAC [SPECIFICATION, FDOM_DEF, FEMPTY_DEF, REP_ABS_empty,
285 sumTheory.ISL]
286QED
287
288
289val dom_update_rep = BETA_RULE (Q.prove
290(`!f a b x. ISL(^update_rep (f:'a -> 'b+one ) a b x) = ((x=a) \/ ISL (f x))`,
291REPEAT GEN_TAC THEN BETA_TAC
292 THEN Q.ASM_CASES_TAC `x = a`
293 THEN ASM_REWRITE_TAC [sumTheory.ISL]));
294
295Theorem FDOM_FUPDATE[simp]:
296 !f a b. FDOM (FUPDATE (f:'a |-> 'b) (a,b)) = a INSERT FDOM f
297Proof
298 REPEAT GEN_TAC THEN
299 REWRITE_TAC [EXTENSION, IN_INSERT] THEN
300 REWRITE_TAC [SPECIFICATION, FDOM_DEF,FUPDATE_DEF, REP_ABS_update] THEN
301 BETA_TAC THEN GEN_TAC THEN Q.ASM_CASES_TAC `x = a` THEN
302 ASM_REWRITE_TAC [sumTheory.ISL]
303QED
304
305
306Theorem FAPPLY_FUPDATE_THM:
307 !(f:'a |-> 'b) a b x.
308 FAPPLY(FUPDATE f (a,b)) x = if x=a then b else FAPPLY f x
309Proof
310REPEAT STRIP_TAC
311 THEN COND_CASES_TAC
312 THEN ASM_REWRITE_TAC [FAPPLY_FUPDATE]
313 THEN IMP_RES_TAC NOT_EQ_FAPPLY
314 THEN ASM_REWRITE_TAC []
315QED
316
317val not_eq_empty_update_rep = BETA_RULE (Q.prove
318(`!(f:'a -> 'b + one) a b. ~(^empty_rep = ^update_rep f a b)`,
319REPEAT GEN_TAC THEN BETA_TAC
320 THEN CONV_TAC (DEPTH_CONV FUN_EQ_CONV)
321 THEN CONV_TAC NOT_FORALL_CONV
322 THEN Q.EXISTS_TAC `a` THEN BETA_TAC
323 THEN DISCH_THEN (fn th => REWRITE_TAC [REWRITE_RULE [sumTheory.ISL]
324 (REWRITE_RULE [th] lemma1)])));
325
326Theorem fmap_EQ_1[local]:
327 !(f:'a |-> 'b) g. (f=g) ==> (FDOM f = FDOM g) /\ (FAPPLY f = FAPPLY g)
328Proof
329REPEAT STRIP_TAC THEN ASM_REWRITE_TAC []
330QED
331
332Theorem NOT_EQ_FEMPTY_FUPDATE[simp]:
333 !(f:'a |-> 'b) a b. ~(FEMPTY = FUPDATE f (a,b))
334Proof
335 REPEAT GEN_TAC THEN
336 DISCH_THEN (MP_TAC o Q.AP_TERM `FDOM`) THEN
337 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE, EXTENSION, EXISTS_OR_THM]
338QED
339
340
341Theorem FDOM_EQ_FDOM_FUPDATE:
342 !(f:'a |-> 'b) x. x IN FDOM f ==> (!y. FDOM (FUPDATE f (x,y)) = FDOM f)
343Proof
344 SRW_TAC [][FDOM_FUPDATE, EXTENSION, EQ_IMP_THM] THEN
345 ASM_REWRITE_TAC []
346QED
347
348(*---------------------------------------------------------------------------
349 Simple induction
350 ---------------------------------------------------------------------------*)
351
352Theorem fmap_SIMPLE_INDUCT:
353 !P:('a |-> 'b) -> bool.
354 P FEMPTY /\
355 (!f. P f ==> !x y. P (FUPDATE f (x,y)))
356 ==>
357 !f. P f
358Proof
359REWRITE_TAC [FUPDATE_DEF, FEMPTY_DEF]
360 THEN GEN_TAC THEN STRIP_TAC THEN GEN_TAC
361 THEN CHOOSE_THEN(CONJUNCTS_THEN2 SUBST1_TAC MP_TAC) (Q.SPEC`f` fmap_ABS_onto)
362 THEN Q.ID_SPEC_TAC `r`
363 THEN HO_MATCH_MP_TAC strong_ind
364 THEN ASM_REWRITE_TAC []
365 THEN Q.PAT_X_ASSUM `P x` (K ALL_TAC)
366 THEN REPEAT STRIP_TAC THEN RES_TAC
367 THEN IMP_RES_THEN SUBST_ALL_TAC is_fmap_REP_ABS
368 THEN ASM_REWRITE_TAC[]
369QED
370
371Theorem FDOM_EQ_EMPTY:
372 !f. (FDOM f = {}) = (f = FEMPTY)
373Proof
374 SIMP_TAC (srw_ss())[EQ_IMP_THM, FDOM_FEMPTY] THEN
375 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN
376 SRW_TAC [][FDOM_FUPDATE, EXTENSION] THEN PROVE_TAC []
377QED
378
379Theorem FDOM_EQ_EMPTY_SYM =
380CONV_RULE (QUANT_CONV (LAND_CONV SYM_CONV)) FDOM_EQ_EMPTY
381
382Theorem FUPDATE_ABSORB_THM[local]:
383 !(f:'a |-> 'b) x y.
384 x IN FDOM f /\ (FAPPLY f x = y) ==> (FUPDATE f (x,y) = f)
385Proof
386 INDUCT_THEN fmap_SIMPLE_INDUCT STRIP_ASSUME_TAC THEN
387 ASM_SIMP_TAC (srw_ss()) [FDOM_FEMPTY, FDOM_FUPDATE, DISJ_IMP_THM,
388 FORALL_AND_THM] THEN
389 REPEAT STRIP_TAC THEN
390 Q.ASM_CASES_TAC `x = x'` THENL [
391 ASM_SIMP_TAC (srw_ss()) [],
392 ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM] THEN
393 FIRST_ASSUM (FREEZE_THEN (fn th => REWRITE_TAC [th]) o
394 MATCH_MP FUPDATE_COMMUTES) THEN
395 AP_THM_TAC THEN AP_TERM_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
396 ASM_REWRITE_TAC []
397 ]
398QED
399
400Theorem FDOM_FAPPLY[local]:
401 !(f:'a |-> 'b) x. x IN FDOM f ==> ?y. FAPPLY f x = y
402Proof
403 INDUCT_THEN fmap_SIMPLE_INDUCT ASSUME_TAC THEN
404 SRW_TAC [][FDOM_FUPDATE, FDOM_FEMPTY]
405QED
406
407Theorem FDOM_FUPDATE_ABSORB[local]:
408 !(f:'a |-> 'b) x. x IN FDOM f ==> ?y. FUPDATE f (x,y) = f
409Proof
410 REPEAT STRIP_TAC
411 THEN IMP_RES_TAC FDOM_FAPPLY
412 THEN Q.EXISTS_TAC `y`
413 THEN MATCH_MP_TAC FUPDATE_ABSORB_THM
414 THEN ASM_REWRITE_TAC []
415QED
416
417Theorem FDOM_F_FEMPTY1:
418 !f:'a |-> 'b. (!a. ~(a IN FDOM f)) = (f = FEMPTY)
419Proof
420 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN
421 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE, NOT_EQ_FEMPTY_FUPDATE, EXISTS_OR_THM]
422QED
423
424Theorem FDOM_FINITE[simp]:
425 !fm. FINITE (FDOM fm)
426Proof
427 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN
428 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE]
429QED
430
431
432(* ===================================================================== *)
433(* Cardinality *)
434(* *)
435(* Define cardinality as the cardinality of the domain of the map *)
436(* ===================================================================== *)
437
438Definition FCARD_DEF[nocompute]: FCARD fm = CARD (FDOM fm)
439End
440
441(* --------------------------------------------------------------------- *)
442(* Basic cardinality results. *)
443(* --------------------------------------------------------------------- *)
444
445Theorem FCARD_FEMPTY:
446 FCARD FEMPTY = 0
447Proof
448 SRW_TAC [][FCARD_DEF, FDOM_FEMPTY]
449QED
450
451Theorem FCARD_FUPDATE:
452 !fm a b. FCARD (FUPDATE fm (a, b)) = if a IN FDOM fm then FCARD fm
453 else 1 + FCARD fm
454Proof
455 SRW_TAC [numSimps.ARITH_ss][FCARD_DEF, FDOM_FUPDATE, FDOM_FINITE]
456QED
457
458Theorem FCARD_0_FEMPTY_LEMMA[local]:
459 !f. (FCARD f = 0) ==> (f = FEMPTY)
460Proof
461 INDUCT_THEN fmap_SIMPLE_INDUCT ASSUME_TAC THEN
462 SRW_TAC [numSimps.ARITH_ss][NOT_EQ_FEMPTY_FUPDATE, FCARD_FUPDATE] THEN
463 STRIP_TAC THEN RES_TAC THEN
464 FULL_SIMP_TAC (srw_ss()) [FDOM_FEMPTY]
465QED
466
467val fmap = ``f : 'a |-> 'b``
468
469Theorem FCARD_0_FEMPTY:
470 !^fmap. (FCARD f = 0) = (f = FEMPTY)
471Proof
472GEN_TAC THEN EQ_TAC THENL
473[REWRITE_TAC [FCARD_0_FEMPTY_LEMMA],
474 DISCH_THEN (fn th => ASM_REWRITE_TAC [th, FCARD_FEMPTY])]
475QED
476
477Theorem FCARD_SUC:
478 !f n. (FCARD f = SUC n) = (?f' x y. ~(x IN FDOM f') /\ (FCARD f' = n) /\
479 (f = FUPDATE f' (x, y)))
480Proof
481 SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss)
482 [EQ_IMP_THM, FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM,
483 FCARD_FUPDATE] THEN
484 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN
485 SIMP_TAC (srw_ss() ++ numSimps.ARITH_ss)[FCARD_FUPDATE, FCARD_FEMPTY] THEN
486 GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
487 COND_CASES_TAC THEN STRIP_TAC THENL [
488 RES_THEN (EVERY_TCL
489 (map Q.X_CHOOSE_THEN [`g`, `u`, `v`]) STRIP_ASSUME_TAC) THEN
490 Q.ASM_CASES_TAC `x = u` THENL [
491 MAP_EVERY Q.EXISTS_TAC [`g`, `u`, `y`] THEN
492 ASM_SIMP_TAC (srw_ss()) [],
493 MAP_EVERY Q.EXISTS_TAC [`FUPDATE g (x, y)`, `u`, `v`] THEN
494 `x IN FDOM g` by FULL_SIMP_TAC (srw_ss()) [FDOM_FUPDATE] THEN
495 ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, FCARD_FUPDATE, FUPDATE_COMMUTES]
496 ],
497 MAP_EVERY Q.EXISTS_TAC [`f`, `x`, `y`] THEN
498 SRW_TAC [numSimps.ARITH_ss][]
499 ]
500QED
501
502(*---------------------------------------------------------------------------
503 A more useful induction theorem
504 ---------------------------------------------------------------------------*)
505
506Theorem fmap_INDUCT:
507 !P. P FEMPTY /\
508 (!f. P f ==> !x y. ~(x IN FDOM f) ==> P (FUPDATE f (x,y)))
509 ==>
510 !f. P f
511Proof
512 REPEAT STRIP_TAC THEN Induct_on `FCARD f` THEN REPEAT STRIP_TAC THENL [
513 PROVE_TAC [FCARD_0_FEMPTY],
514 `?g u w. ~(u IN FDOM g) /\ (f = FUPDATE g (u, w)) /\ (FCARD g = v)` by
515 PROVE_TAC [FCARD_SUC] THEN
516 PROVE_TAC []
517 ]
518QED
519
520(* splitting a finite map on a key *)
521Theorem FM_PULL_APART:
522 !fm k. k IN FDOM fm ==> ?fm0 v. (fm = fm0 |+ (k, v)) /\
523 ~(k IN FDOM fm0)
524Proof
525 HO_MATCH_MP_TAC fmap_INDUCT THEN SRW_TAC [][] THENL [
526 PROVE_TAC [],
527 RES_TAC THEN
528 MAP_EVERY Q.EXISTS_TAC [`fm0 |+ (x,y)`, `v`] THEN
529 `~(k = x)` by PROVE_TAC [] THEN
530 SRW_TAC [][FUPDATE_COMMUTES]
531 ]
532QED
533
534
535(*---------------------------------------------------------------------------
536 Equality of finite maps
537 ---------------------------------------------------------------------------*)
538
539Theorem update_eq_not_x[local]:
540 !(f:'a |-> 'b) x.
541 ?f'. !y. (FUPDATE f (x,y) = FUPDATE f' (x,y)) /\ ~(x IN FDOM f')
542Proof
543 HO_MATCH_MP_TAC fmap_INDUCT THEN SRW_TAC [][] THENL [
544 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][],
545 FIRST_X_ASSUM (Q.SPEC_THEN `x'` STRIP_ASSUME_TAC) THEN
546 Cases_on `x = x'` THEN SRW_TAC [][] THENL [
547 Q.EXISTS_TAC `f` THEN SRW_TAC [][],
548 Q.EXISTS_TAC `f' |+ (x,y)` THEN
549 SRW_TAC [][] THEN METIS_TAC [FUPDATE_COMMUTES]
550 ]
551 ]
552QED
553
554val lemma9 = BETA_RULE (Q.prove
555(`!x y (f1:('a,'b)fmap) f2.
556 (f1 = f2) ==>
557 ((\f.FUPDATE f (x,y)) f1 = (\f. FUPDATE f (x,y)) f2)`,
558 REPEAT STRIP_TAC
559 THEN AP_TERM_TAC
560 THEN ASM_REWRITE_TAC []));
561
562Theorem NOT_FDOM_FAPPLY_FEMPTY:
563 !^fmap x. ~(x IN FDOM f) ==> (FAPPLY f x = FAPPLY FEMPTY x)
564Proof
565 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL
566 [REWRITE_TAC [],
567 REPEAT GEN_TAC
568 THEN STRIP_TAC
569 THEN GEN_TAC
570 THEN Q.ASM_CASES_TAC `x' = x` THENL
571 [ASM_REWRITE_TAC [FDOM_FUPDATE, IN_INSERT],
572 IMP_RES_TAC NOT_EQ_FAPPLY
573 THEN ASM_REWRITE_TAC [FDOM_FUPDATE, IN_INSERT]]]
574QED
575
576Theorem fmap_EQ_2[local]:
577 !(f:'a |-> 'b) g. (FDOM f = FDOM g) /\ (FAPPLY f = FAPPLY g) ==> (f = g)
578Proof
579 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL [
580 SRW_TAC [][FDOM_FEMPTY] THEN
581 PROVE_TAC [FCARD_0_FEMPTY, CARD_EMPTY, FCARD_DEF],
582 SRW_TAC [][FDOM_FUPDATE] THEN
583 `?h. (FUPDATE g (x, g ' x) = FUPDATE h (x, g ' x)) /\ ~(x IN FDOM h)`
584 by PROVE_TAC [update_eq_not_x] THEN
585 `x IN FDOM g` by PROVE_TAC [IN_INSERT] THEN
586 `FUPDATE g (x, g ' x) = g` by PROVE_TAC [FUPDATE_ABSORB_THM] THEN
587 POP_ASSUM SUBST_ALL_TAC THEN FIRST_X_ASSUM SUBST_ALL_TAC THEN
588 `!v. (f |+ (x, y)) ' v = (h |+ (x, FAPPLY g x)) ' v`
589 by SRW_TAC [][] THEN
590 `y = g ' x` by PROVE_TAC [FAPPLY_FUPDATE] THEN
591 ASM_REWRITE_TAC [] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
592 FIRST_X_ASSUM MATCH_MP_TAC THEN CONJ_TAC THENL [
593 FULL_SIMP_TAC (srw_ss()) [EXTENSION, FDOM_FUPDATE] THEN PROVE_TAC [],
594 SIMP_TAC (srw_ss()) [FUN_EQ_THM] THEN Q.X_GEN_TAC `z` THEN
595 Cases_on `x = z` THENL [
596 PROVE_TAC [NOT_FDOM_FAPPLY_FEMPTY],
597 FIRST_X_ASSUM (Q.SPEC_THEN `z` MP_TAC) THEN
598 ASM_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM]
599 ]
600 ]
601 ]
602QED
603
604Theorem fmap_EQ:
605 !(f:'a |-> 'b) g. (FDOM f = FDOM g) /\ (FAPPLY f = FAPPLY g) <=> (f = g)
606Proof
607 REPEAT STRIP_TAC THEN EQ_TAC THEN REWRITE_TAC [fmap_EQ_1, fmap_EQ_2]
608QED
609
610(*---------------------------------------------------------------------------
611 A more useful equality
612 ---------------------------------------------------------------------------*)
613
614Theorem fmap_EQ_THM:
615 !(f:'a |-> 'b) g.
616 (FDOM f = FDOM g) /\ (!x. x IN FDOM f ==> (FAPPLY f x = FAPPLY g x))
617 <=>
618 (f = g)
619Proof
620 REPEAT STRIP_TAC THEN EQ_TAC THENL [
621 STRIP_TAC THEN ASM_REWRITE_TAC [GSYM fmap_EQ] THEN
622 MATCH_MP_TAC EQ_EXT THEN GEN_TAC THEN
623 Q.ASM_CASES_TAC `x IN FDOM f` THEN PROVE_TAC [NOT_FDOM_FAPPLY_FEMPTY],
624 STRIP_TAC THEN ASM_REWRITE_TAC []
625 ]
626QED
627
628(* and it's more useful still if the main equality is the other way 'round *)
629Theorem fmap_EXT = GSYM fmap_EQ_THM
630
631(*---------------------------------------------------------------------------
632 Submaps
633 ---------------------------------------------------------------------------*)
634
635Definition SUBMAP_DEF[nocompute]:
636 $SUBMAP ^fmap g =
637 !x. x IN FDOM f ==> x IN FDOM g /\ (FAPPLY f x = FAPPLY g x)
638End
639val _ = set_fixity "SUBMAP" (Infix(NONASSOC, 450));
640val _ = Unicode.unicode_version { u = UTF8.chr 0x2291, tmnm = "SUBMAP"}
641val _ = TeX_notation {hol = "SUBMAP", TeX = ("\\HOLTokenSubmap{}", 1)}
642val _ = TeX_notation {hol = UTF8.chr 0x2291, TeX = ("\\HOLTokenSubmap{}", 1)}
643
644
645Theorem SUBMAP_FEMPTY[simp]:
646 !(f : ('a,'b) fmap). FEMPTY SUBMAP f
647Proof SRW_TAC [][SUBMAP_DEF, FDOM_FEMPTY]
648QED
649
650Theorem SUBMAP_REFL[simp]:
651 !(f:('a,'b) fmap). f SUBMAP f
652Proof
653 REWRITE_TAC [SUBMAP_DEF]
654QED
655
656Theorem SUBMAP_ANTISYM:
657 !(f:('a,'b) fmap) g. (f SUBMAP g /\ g SUBMAP f) = (f = g)
658Proof
659 GEN_TAC THEN GEN_TAC THEN EQ_TAC THENL [
660 REWRITE_TAC[SUBMAP_DEF, GSYM fmap_EQ_THM, EXTENSION] THEN PROVE_TAC [],
661 STRIP_TAC THEN ASM_REWRITE_TAC [SUBMAP_REFL]
662 ]
663QED
664
665Theorem SUBMAP_TRANS:
666 !f g h. f SUBMAP g /\ g SUBMAP h ==> f SUBMAP h
667Proof
668 SRW_TAC [][SUBMAP_DEF]
669QED
670
671Theorem SUBMAP_FUPDATE_EXTENDED:
672 k NOTIN FDOM f ==> f SUBMAP f |+ (k,v)
673Proof
674 SRW_TAC [][SUBMAP_DEF] THEN METIS_TAC [FAPPLY_FUPDATE_THM]
675QED
676
677Theorem EQ_FDOM_SUBMAP:
678 (f = g) <=> f SUBMAP g /\ (FDOM f = FDOM g)
679Proof
680SIMP_TAC (srw_ss()) [fmap_EXT, SUBMAP_DEF] THEN METIS_TAC []
681QED
682
683Theorem SUBMAP_FUPDATE_EQN[simp]:
684 f SUBMAP f |+ (x,y) <=> x NOTIN FDOM f \/ (f ' x = y) /\ x IN FDOM f
685Proof
686 SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss ++ boolSimps.COND_elim_ss)
687 [FAPPLY_FUPDATE_THM,SUBMAP_DEF,EQ_IMP_THM] THEN
688 METIS_TAC []
689QED
690
691Theorem SUBMAP_FDOM_SUBSET:
692 f1 SUBMAP f2 ==> FDOM f1 SUBSET FDOM f2
693Proof srw_tac[][SUBMAP_DEF,SUBSET_DEF]
694QED
695
696(*---------------------------------------------------------------------------
697 Restriction
698 ---------------------------------------------------------------------------*)
699
700Theorem res_lemma[local]:
701 !^fmap r.
702 ?res. (FDOM res = FDOM f INTER r)
703 /\ (!x. res ' x = if x IN FDOM f INTER r then f ' x else FEMPTY ' x)
704Proof
705 CONV_TAC SWAP_VARS_CONV THEN GEN_TAC THEN
706 INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [
707 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][FDOM_FEMPTY],
708 REPEAT STRIP_TAC THEN
709 Cases_on `x IN r` THENL [
710 Q.EXISTS_TAC `FUPDATE res (x,y)` THEN
711 ASM_SIMP_TAC (srw_ss()) [FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN
712 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [],
713
714 Q.EXISTS_TAC `res` THEN
715 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN
716 FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC []
717 ]
718 ]
719QED
720
721val DRESTRICT_DEF = new_specification
722 ("DRESTRICT_DEF", ["DRESTRICT"],
723 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) res_lemma);
724
725
726Theorem DRESTRICT_FEMPTY[simp]:
727 !r. DRESTRICT FEMPTY r = FEMPTY
728Proof
729 SRW_TAC [][GSYM fmap_EQ_THM, DRESTRICT_DEF, FDOM_FEMPTY]
730QED
731
732Theorem DRESTRICT_FUPDATE[simp]:
733 !^fmap r x y.
734 DRESTRICT (FUPDATE f (x,y)) r =
735 if x IN r then FUPDATE (DRESTRICT f r) (x,y) else DRESTRICT f r
736Proof
737 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, DRESTRICT_DEF, FAPPLY_FUPDATE_THM,
738 EXTENSION] THEN PROVE_TAC []
739QED
740
741Theorem DRESTRICT_EQ_FEMPTY:
742 !m s. DISJOINT s (FDOM m) <=> DRESTRICT m s = FEMPTY
743Proof
744 ho_match_mp_tac fmap_SIMPLE_INDUCT >> rw[] >> eq_tac >> rw[]
745QED
746
747Theorem STRONG_DRESTRICT_FUPDATE:
748 !^fmap r x y.
749 x IN r ==> (DRESTRICT (FUPDATE f (x,y)) r
750 =
751 FUPDATE (DRESTRICT f (r DELETE x)) (x,y))
752Proof
753 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, DRESTRICT_DEF,
754 FAPPLY_FUPDATE_THM, EXTENSION] THEN PROVE_TAC []
755QED
756
757Theorem FDOM_DRESTRICT:
758 !^fmap r x. FDOM (DRESTRICT f r) = FDOM f INTER r
759Proof
760 SRW_TAC [][DRESTRICT_DEF]
761QED
762
763Theorem NOT_FDOM_DRESTRICT:
764 !^fmap x. ~(x IN FDOM f) ==> (DRESTRICT f (COMPL {x}) = f)
765Proof
766 SRW_TAC [][GSYM fmap_EQ_THM, DRESTRICT_DEF, EXTENSION] THEN PROVE_TAC []
767QED
768
769Theorem DRESTRICT_SUBMAP[simp]:
770 !^fmap r. (DRESTRICT f r) SUBMAP f
771Proof
772 INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [
773 REWRITE_TAC [DRESTRICT_FEMPTY, SUBMAP_FEMPTY],
774 POP_ASSUM MP_TAC THEN
775 SIMP_TAC (srw_ss()) [DRESTRICT_DEF, SUBMAP_DEF, FDOM_FUPDATE]
776 ]
777QED
778
779Theorem DRESTRICT_DRESTRICT[simp]:
780 !^fmap P Q. DRESTRICT (DRESTRICT f P) Q = DRESTRICT f (P INTER Q)
781Proof
782 HO_MATCH_MP_TAC fmap_INDUCT
783 THEN SRW_TAC [][DRESTRICT_FEMPTY, DRESTRICT_FUPDATE]
784 THEN Q.ASM_CASES_TAC `x IN P`
785 THEN Q.ASM_CASES_TAC `x IN Q`
786 THEN ASM_REWRITE_TAC [DRESTRICT_FUPDATE]
787QED
788
789Theorem DRESTRICT_IS_FEMPTY:
790 !f. DRESTRICT f {} = FEMPTY
791Proof
792 GEN_TAC THEN
793 `FDOM (DRESTRICT f {}) = {}` by SRW_TAC [][FDOM_DRESTRICT] THEN
794 PROVE_TAC [FDOM_EQ_EMPTY]
795QED
796
797Theorem FUPDATE_DRESTRICT:
798 !^fmap x y. FUPDATE f (x,y) = FUPDATE (DRESTRICT f (COMPL {x})) (x,y)
799Proof
800 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, EXTENSION, DRESTRICT_DEF,
801 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []
802QED
803
804Theorem STRONG_DRESTRICT_FUPDATE_THM:
805 !^fmap r x y.
806 DRESTRICT (FUPDATE f (x,y)) r
807 =
808 if x IN r then FUPDATE (DRESTRICT f (COMPL {x} INTER r)) (x,y)
809 else DRESTRICT f (COMPL {x} INTER r)
810Proof
811 SRW_TAC [][GSYM fmap_EQ_THM, DRESTRICT_DEF, FDOM_FUPDATE, EXTENSION,
812 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []
813QED
814
815Theorem DRESTRICT_UNIV:
816 !^fmap. DRESTRICT f UNIV = f
817Proof
818 SRW_TAC [][DRESTRICT_DEF, GSYM fmap_EQ_THM]
819QED
820
821Theorem SUBMAP_DRESTRICT[simp]:
822 DRESTRICT f P SUBMAP f
823Proof
824 SRW_TAC [][DRESTRICT_DEF, SUBMAP_DEF]
825QED
826
827Theorem SUBMAP_DRESTRICT_MONOTONE:
828 f1 SUBMAP f2 /\ s1 SUBSET s2
829 ==>
830 DRESTRICT f1 s1 SUBMAP DRESTRICT f2 s2
831Proof
832 rw[SUBMAP_DEF,FDOM_DRESTRICT,SUBSET_DEF,DRESTRICT_DEF]
833QED
834
835Theorem DRESTRICT_EQ_DRESTRICT:
836 !f1 f2 s1 s2.
837 (DRESTRICT f1 s1 = DRESTRICT f2 s2) =
838 (DRESTRICT f1 s1 SUBMAP f2 /\ DRESTRICT f2 s2 SUBMAP f1 /\
839 (s1 INTER FDOM f1 = s2 INTER FDOM f2))
840Proof
841SRW_TAC[][GSYM fmap_EQ_THM,DRESTRICT_DEF,SUBMAP_DEF,EXTENSION] THEN
842METIS_TAC[]
843QED
844
845(*---------------------------------------------------------------------------
846 Union of finite maps
847 ---------------------------------------------------------------------------*)
848
849Theorem union_lemma[local]:
850 !^fmap g.
851 ?union.
852 (FDOM union = FDOM f UNION FDOM g) /\
853 (!x. FAPPLY union x = if x IN FDOM f then FAPPLY f x else FAPPLY g x)
854Proof
855 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL [
856 GEN_TAC THEN Q.EXISTS_TAC `g` THEN SRW_TAC [][FDOM_FEMPTY],
857 REPEAT STRIP_TAC THEN
858 FIRST_X_ASSUM (Q.SPEC_THEN `g` STRIP_ASSUME_TAC) THEN
859 Q.EXISTS_TAC `FUPDATE union (x,y)` THEN
860 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN
861 PROVE_TAC []
862 ]
863QED
864
865val FUNION_DEF = new_specification
866 ("FUNION_DEF", ["FUNION"],
867 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) union_lemma);
868val _ = set_mapped_fixity {term_name = "FUNION", tok = UTF8.chr 0x228C,
869 fixity = Infixl 500}
870val _ = TeX_notation {hol = UTF8.chr 0x228C, TeX = ("\\HOLTokenFUNION{}", 1)}
871
872
873Theorem FDOM_FUNION[simp] = FUNION_DEF |> SPEC_ALL |> CONJUNCT1
874
875Theorem FUNION_FEMPTY_1[simp]:
876 !g. FUNION FEMPTY g = g
877Proof
878 SRW_TAC [][GSYM fmap_EQ_THM, FUNION_DEF, FDOM_FEMPTY]
879QED
880
881Theorem FUNION_FEMPTY_2[simp]:
882 !f. FUNION f FEMPTY = f
883Proof
884 SRW_TAC [][GSYM fmap_EQ_THM, FUNION_DEF, FDOM_FEMPTY]
885QED
886
887Theorem FUNION_FUPDATE_1:
888 !^fmap g x y.
889 FUNION (FUPDATE f (x,y)) g = FUPDATE (FUNION f g) (x,y)
890Proof
891 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, FUNION_DEF, FAPPLY_FUPDATE_THM,
892 EXTENSION] THEN PROVE_TAC []
893QED
894
895Theorem FUNION_FUPDATE_2:
896 !^fmap g x y.
897 FUNION f (FUPDATE g (x,y)) =
898 if x IN FDOM f then FUNION f g
899 else FUPDATE (FUNION f g) (x,y)
900Proof
901 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, FUNION_DEF, FAPPLY_FUPDATE_THM,
902 EXTENSION] THEN PROVE_TAC []
903QED
904
905Theorem FUNION_IDEMPOT[simp]:
906 FUNION fm fm = fm
907Proof
908 SRW_TAC[][GSYM fmap_EQ_THM,FUNION_DEF]
909QED
910
911(*---------------------------------------------------------------------------
912 Merging of finite maps (added 17 March 2009 by Thomas Tuerk)
913 ---------------------------------------------------------------------------*)
914
915
916Theorem fmerge_exists[local]:
917 !m f g.
918 ?merge.
919 (FDOM merge = FDOM f UNION FDOM g) /\
920 (!x. FAPPLY merge x = if ~(x IN FDOM f) then FAPPLY g x
921 else
922 if ~(x IN FDOM g) then FAPPLY f x
923 else
924 (m (FAPPLY f x) (FAPPLY g x)))
925Proof
926 GEN_TAC THEN GEN_TAC THEN
927 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL [
928 Q.EXISTS_TAC `f` THEN
929 SIMP_TAC std_ss [FDOM_FEMPTY, UNION_EMPTY, NOT_IN_EMPTY] THEN
930 PROVE_TAC[NOT_FDOM_FAPPLY_FEMPTY],
931
932 FULL_SIMP_TAC std_ss [] THEN REPEAT STRIP_TAC THEN
933 Cases_on `x IN FDOM f` THENL [
934 Q.EXISTS_TAC `merge |+ (x, m (f ' x) y)`,
935 Q.EXISTS_TAC `merge |+ (x, y)`
936 ] THEN (
937 ASM_SIMP_TAC std_ss [FDOM_FUPDATE] THEN
938 REPEAT STRIP_TAC THEN1 (
939 SIMP_TAC std_ss [EXTENSION, IN_INSERT, IN_UNION] THEN
940 PROVE_TAC[]
941 ) THEN
942 Cases_on `x' = x` THEN (
943 ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM, IN_INSERT]
944 )
945 )
946 ]
947QED
948
949val FMERGE_DEF = new_specification
950 ("FMERGE_DEF", ["FMERGE"],
951 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) fmerge_exists);
952
953
954Theorem FMERGE_FEMPTY:
955 (FMERGE m f FEMPTY = f) /\
956 (FMERGE m FEMPTY f = f)
957Proof
958
959SIMP_TAC std_ss [GSYM fmap_EQ_THM] THEN
960SIMP_TAC std_ss [FMERGE_DEF, FDOM_FEMPTY, NOT_IN_EMPTY,
961 UNION_EMPTY]
962QED
963
964Theorem FDOM_FMERGE[simp]:
965 !m f g. FDOM (FMERGE m f g) = FDOM f UNION FDOM g
966Proof
967SRW_TAC[][FMERGE_DEF]
968QED
969
970Theorem FMERGE_FUNION:
971 FUNION = FMERGE (\x y. x)
972Proof
973 SIMP_TAC std_ss [FUN_EQ_THM, FMERGE_DEF,
974 GSYM fmap_EQ_THM, FUNION_DEF,
975 IN_UNION, DISJ_IMP_THM] THEN
976 METIS_TAC[]
977QED
978
979
980Theorem FUNION_FMERGE:
981 !f1 f2 m. DISJOINT (FDOM f1) (FDOM f2) ==>
982 (FMERGE m f1 f2 = FUNION f1 f2)
983Proof
984 SIMP_TAC std_ss [FUN_EQ_THM, FMERGE_DEF,
985 GSYM fmap_EQ_THM, FUNION_DEF,
986 IN_UNION, DISJ_IMP_THM] THEN
987 SIMP_TAC std_ss [DISJOINT_DEF, EXTENSION, NOT_IN_EMPTY,
988 IN_INTER] THEN
989 METIS_TAC[]
990QED
991
992Theorem FORALL_EQ_I[local]:
993 (!x. P x <=> Q x) ==> ((!x. P x) <=> (!x. Q x))
994Proof
995 metis_tac[]
996QED
997
998Theorem FMERGE_NO_CHANGE:
999 (FMERGE m f1 f2 = f1 <=>
1000 !x. x IN FDOM f2 ==> x IN FDOM f1 /\ m (f1 ' x) (f2 ' x) = f1 ' x) /\
1001 (FMERGE m f1 f2 = f2 <=>
1002 !x. x IN FDOM f1 ==> x IN FDOM f2 /\ (m (f1 ' x) (f2 ' x) = f2 ' x))
1003Proof
1004 SIMP_TAC std_ss [GSYM fmap_EQ_THM] THEN
1005 SIMP_TAC std_ss [EXTENSION, FMERGE_DEF, IN_UNION, GSYM FORALL_AND_THM] THEN
1006 STRIP_TAC THENL [
1007 HO_MATCH_MP_TAC FORALL_EQ_I THEN GEN_TAC THEN
1008 Cases_on `x IN FDOM f2` THEN (ASM_SIMP_TAC std_ss [] THEN METIS_TAC[]),
1009
1010 HO_MATCH_MP_TAC FORALL_EQ_I THEN GEN_TAC THEN
1011 Cases_on `x IN FDOM f1` THEN (ASM_SIMP_TAC std_ss [] THEN METIS_TAC[])
1012 ]
1013QED
1014
1015Theorem FMERGE_COMM:
1016 COMM (FMERGE m) = COMM m
1017Proof
1018 SIMP_TAC std_ss [combinTheory.COMM_DEF, GSYM fmap_EQ_THM] THEN
1019 SIMP_TAC std_ss [FMERGE_DEF] THEN
1020 EQ_TAC THEN REPEAT STRIP_TAC THENL [
1021 POP_ASSUM MP_TAC THEN
1022 SIMP_TAC std_ss [GSYM LEFT_EXISTS_IMP_THM] THEN
1023 Q.EXISTS_TAC `FEMPTY |+ (z, x)` THEN
1024 Q.EXISTS_TAC `FEMPTY |+ (z, y)` THEN
1025
1026 SIMP_TAC std_ss [FDOM_FUPDATE, FDOM_FEMPTY, IN_UNION] THEN
1027 SIMP_TAC std_ss [IN_SING, FAPPLY_FUPDATE_THM],
1028
1029 PROVE_TAC [UNION_COMM],
1030
1031 FULL_SIMP_TAC std_ss [IN_UNION]
1032 ]
1033QED
1034
1035Theorem FMERGE_ASSOC:
1036 ASSOC (FMERGE m) = ASSOC m
1037Proof
1038 SIMP_TAC std_ss [combinTheory.ASSOC_DEF, GSYM fmap_EQ_THM] THEN
1039 SIMP_TAC std_ss [FMERGE_DEF, UNION_ASSOC, IN_UNION] THEN
1040 EQ_TAC THEN REPEAT STRIP_TAC THENL [
1041 POP_ASSUM MP_TAC THEN
1042 SIMP_TAC std_ss [GSYM LEFT_EXISTS_IMP_THM] THEN
1043 Q.EXISTS_TAC `FEMPTY |+ (e, x)` THEN
1044 Q.EXISTS_TAC `FEMPTY |+ (e, y)` THEN
1045 Q.EXISTS_TAC `FEMPTY |+ (e, z)` THEN
1046 Q.EXISTS_TAC `e` THEN
1047 SIMP_TAC std_ss [FDOM_FUPDATE, FDOM_FEMPTY, IN_UNION] THEN
1048 SIMP_TAC std_ss [IN_SING, FAPPLY_FUPDATE_THM],
1049
1050 ASM_SIMP_TAC std_ss [] THEN METIS_TAC[],
1051
1052 ASM_SIMP_TAC std_ss [] THEN METIS_TAC[],
1053
1054 ASM_SIMP_TAC std_ss [] THEN METIS_TAC[]
1055 ]
1056QED
1057
1058Theorem FMERGE_DRESTRICT:
1059 DRESTRICT (FMERGE f st1 st2) vs =
1060 FMERGE f (DRESTRICT st1 vs) (DRESTRICT st2 vs)
1061Proof
1062 SIMP_TAC std_ss [GSYM fmap_EQ_THM, DRESTRICT_DEF, FMERGE_DEF, EXTENSION,
1063 IN_INTER, IN_UNION] THEN
1064 METIS_TAC[]
1065QED
1066
1067Theorem FMERGE_EQ_FEMPTY:
1068 (FMERGE m f g = FEMPTY) <=> (f = FEMPTY) /\ (g = FEMPTY)
1069Proof
1070 SIMP_TAC std_ss [GSYM fmap_EQ_THM] THEN
1071 SIMP_TAC (std_ss++boolSimps.CONJ_ss) [FMERGE_DEF, FDOM_FEMPTY, NOT_IN_EMPTY,
1072 EMPTY_UNION, IN_UNION]
1073QED
1074
1075(*---------------------------------------------------------------------------
1076 "assoc" for finite maps
1077 ---------------------------------------------------------------------------*)
1078
1079Definition FLOOKUP_DEF[nocompute]:
1080 FLOOKUP ^fmap x = if x IN FDOM f then SOME (FAPPLY f x) else NONE
1081End
1082
1083Theorem FLOOKUP_EMPTY[simp]:
1084 FLOOKUP FEMPTY k = NONE
1085Proof
1086 SRW_TAC [][FLOOKUP_DEF]
1087QED
1088
1089Theorem FLOOKUP_UPDATE:
1090 FLOOKUP (fm |+ (k1,v)) k2 = if k1 = k2 then SOME v else FLOOKUP fm k2
1091Proof
1092 SRW_TAC [][FLOOKUP_DEF, FAPPLY_FUPDATE_THM] THEN
1093 FULL_SIMP_TAC (srw_ss()) []
1094QED
1095(* don't export this because of the if, though this is pretty paranoid *)
1096
1097Theorem FLOOKUP_UPDATE_SAME: FLOOKUP (fm |+ (a:'a, b)) a = SOME b
1098Proof REWRITE_TAC [FLOOKUP_UPDATE]
1099QED
1100
1101Theorem FLOOKUP_UPDATE_DIFF:
1102 a <> x ==> (FLOOKUP (fm |+ (a, b)) x = FLOOKUP fm x)
1103Proof SIMP_TAC std_ss [FLOOKUP_UPDATE]
1104QED
1105
1106Theorem FLOOKUP_SUBMAP:
1107 f SUBMAP g /\ (FLOOKUP f k = SOME v) ==> (FLOOKUP g k = SOME v)
1108Proof
1109 SRW_TAC [][FLOOKUP_DEF, SUBMAP_DEF] THEN METIS_TAC []
1110QED
1111
1112Theorem SUBMAP_FLOOKUP_EQN:
1113 f SUBMAP g <=> !x y. (FLOOKUP f x = SOME y) ==> (FLOOKUP g x = SOME y)
1114Proof rw[SUBMAP_DEF,FLOOKUP_DEF] \\ METIS_TAC[]
1115QED
1116
1117Theorem SUBMAP_FUPDATE_FLOOKUP:
1118 f SUBMAP (f |+ (x,y)) <=> (FLOOKUP f x = NONE) \/ (FLOOKUP f x = SOME y)
1119Proof
1120 SRW_TAC [][FLOOKUP_DEF, AC CONJ_ASSOC CONJ_COMM]
1121QED
1122
1123Theorem FLOOKUP_FUNION:
1124 FLOOKUP (FUNION f1 f2) k =
1125 case FLOOKUP f1 k of
1126 NONE => FLOOKUP f2 k
1127 | SOME v => SOME v
1128Proof
1129SRW_TAC [][FLOOKUP_DEF,FUNION_DEF] THEN FULL_SIMP_TAC (srw_ss()) []
1130QED
1131
1132Theorem FLOOKUP_EXT:
1133 (f1 = f2) = (FLOOKUP f1 = FLOOKUP f2)
1134Proof
1135 SRW_TAC [][fmap_EXT,FUN_EQ_THM,IN_DEF,FLOOKUP_DEF] THEN
1136 PROVE_TAC [optionTheory.SOME_11,optionTheory.NOT_SOME_NONE]
1137QED
1138
1139Theorem fmap_eq_flookup =
1140 FLOOKUP_EXT |> REWRITE_RULE[FUN_EQ_THM];
1141
1142Theorem FLOOKUP_DRESTRICT:
1143 !fm s k. FLOOKUP (DRESTRICT fm s) k = if k IN s then FLOOKUP fm k else NONE
1144Proof
1145 SRW_TAC[][FLOOKUP_DEF,DRESTRICT_DEF] THEN FULL_SIMP_TAC std_ss []
1146QED
1147
1148Theorem FLOOKUP_FMERGE:
1149 FLOOKUP (FMERGE f m1 m2) k =
1150 case (FLOOKUP m1 k, FLOOKUP m2 k) of
1151 | (SOME v1, SOME v2) => SOME $ f v1 v2
1152 | (f1, f2) => OPTION_CHOICE f1 f2
1153Proof
1154 rw[FLOOKUP_DEF, FMERGE_DEF] >> gvs[]
1155QED
1156
1157Theorem FLOOKUP_FMERGE[allow_rebind] =
1158 FLOOKUP_FMERGE |> SIMP_RULE (srw_ss()) [];
1159
1160
1161(*---------------------------------------------------------------------------
1162 Merge with key
1163 ---------------------------------------------------------------------------*)
1164
1165Theorem FMERGE_WITH_KEY_EXISTS[local]:
1166 !f m1 m2. ?u.
1167 FDOM u = FDOM m1 UNION FDOM m2 /\
1168 !x. u ' x =
1169 if x IN FDOM m1 /\ x IN FDOM m2 then f x (m1 ' x) (m2 ' x)
1170 else if x IN FDOM m1 then m1 ' x else m2 ' x
1171Proof
1172 gen_tac >> ho_match_mp_tac fmap_SIMPLE_INDUCT >> rw[]
1173 >- (qexists_tac `m2` >> simp[]) >>
1174 first_x_assum $ qspec_then `m2` assume_tac >> gvs[] >>
1175 Cases_on `x IN FDOM m2` >> gvs[]
1176 >- (
1177 qexists_tac `u |+ (x, f x y (m2 ' x))` >>
1178 gvs[INSERT_UNION_EQ, FAPPLY_FUPDATE_THM] >> rw[] >> gvs[]
1179 )
1180 >- (
1181 qexists_tac `u |+ (x, y)` >>
1182 gvs[INSERT_UNION_EQ, FAPPLY_FUPDATE_THM] >> rw[] >> gvs[]
1183 )
1184QED
1185
1186val FMERGE_WITH_KEY_DEF = new_specification
1187 ("FMERGE_WITH_KEY_DEF", ["FMERGE_WITH_KEY"],
1188 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) FMERGE_WITH_KEY_EXISTS);
1189
1190Theorem FLOOKUP_FMERGE_WITH_KEY[local]:
1191 FLOOKUP (FMERGE_WITH_KEY f m1 m2) k =
1192 case (FLOOKUP m1 k, FLOOKUP m2 k) of
1193 | (SOME v1, SOME v2) => SOME $ f k v1 v2
1194 | (f1, f2) => OPTION_CHOICE f1 f2
1195Proof
1196 rw[FLOOKUP_DEF, FMERGE_WITH_KEY_DEF] >> gvs[]
1197QED
1198
1199Theorem FLOOKUP_FMERGE_WITH_KEY =
1200 FLOOKUP_FMERGE_WITH_KEY |> SIMP_RULE (srw_ss()) [];
1201
1202Theorem FMERGE_WITH_KEY_FEMPTY[simp]:
1203 FMERGE_WITH_KEY f FEMPTY m2 = m2 /\
1204 FMERGE_WITH_KEY f m1 FEMPTY = m1
1205Proof
1206 rw[fmap_eq_flookup, FLOOKUP_FMERGE_WITH_KEY] >> CASE_TAC >> simp[]
1207QED
1208
1209Theorem FLOOKUP_FMERGE_WITH_KEY_COMM:
1210 COMM (FMERGE_WITH_KEY f) = !k. COMM (f k)
1211Proof
1212 rw[combinTheory.COMM_DEF, fmap_eq_flookup, FLOOKUP_FMERGE_WITH_KEY] >>
1213 eq_tac >> rw[]
1214 >- (
1215 pop_assum $ qspecl_then [`FEMPTY |+ (k,x)`,`FEMPTY |+ (k,y)`,`k`] mp_tac >>
1216 simp[FLOOKUP_UPDATE]
1217 ) >>
1218 rename1 `FLOOKUP _ k` >> Cases_on `FLOOKUP x k` >> Cases_on `FLOOKUP y k`
1219 >- simp[] >- simp[] >- simp[] >>
1220 qmatch_assum_abbrev_tac `FLOOKUP x _ = SOME a` >>
1221 qmatch_assum_abbrev_tac `FLOOKUP y _ = SOME b` >>
1222 last_x_assum $ qspecl_then [`k`,`a`,`b`] assume_tac >> simp[] >> gvs[]
1223QED
1224
1225Theorem FLOOKUP_FMERGE_WITH_KEY_ASSOC:
1226 ASSOC (FMERGE_WITH_KEY f) = !k. ASSOC (f k)
1227Proof
1228 rw[combinTheory.ASSOC_DEF, fmap_eq_flookup, FLOOKUP_FMERGE_WITH_KEY] >>
1229 eq_tac >> rw[]
1230 >- (
1231 pop_assum $ qspecl_then
1232 [`FEMPTY |+ (k,x)`,`FEMPTY |+ (k,y)`,`FEMPTY |+ (k,z)`,`k`] mp_tac >>
1233 simp[FLOOKUP_UPDATE]
1234 ) >>
1235 rename1 `FLOOKUP _ k` >>
1236 Cases_on `FLOOKUP x k` >> Cases_on `FLOOKUP y k` >> Cases_on `FLOOKUP z k`
1237 >- simp[] >- simp[] >- simp[] >- simp[] >- simp[] >- simp[] >- simp[] >>
1238 qmatch_assum_abbrev_tac `FLOOKUP x _ = SOME a` >>
1239 qmatch_assum_abbrev_tac `FLOOKUP y _ = SOME b` >>
1240 qmatch_assum_abbrev_tac `FLOOKUP z _ = SOME c` >>
1241 last_x_assum $ qspecl_then [`k`,`a`,`b`,`c`] assume_tac >> simp[] >> gvs[]
1242QED
1243
1244Theorem FMERGE_WITH_KEY_FUPDATE:
1245 FMERGE_WITH_KEY f (m1 |+ (k,v1)) m2 =
1246 (FMERGE_WITH_KEY f m1 m2) |+
1247 (k, case FLOOKUP m2 k of NONE => v1 | SOME v2 => f k v1 v2)
1248Proof
1249 rw[fmap_eq_flookup, FLOOKUP_FMERGE_WITH_KEY, FLOOKUP_UPDATE] >>
1250 IF_CASES_TAC >> gvs[] >> CASE_TAC >> gvs[]
1251QED
1252
1253Theorem FMERGE_WITH_KEY_FUNION:
1254 FMERGE_WITH_KEY f (FUNION m1 m2) m3 =
1255 FUNION
1256 (FMERGE_WITH_KEY f m1 (DRESTRICT m3 (FDOM m1)))
1257 (FMERGE_WITH_KEY f m2 m3)
1258Proof
1259 rw[fmap_eq_flookup, FLOOKUP_FMERGE_WITH_KEY, FLOOKUP_FUNION, FLOOKUP_DRESTRICT] >>
1260 every_case_tac >> gvs[FLOOKUP_DEF]
1261QED
1262
1263Theorem FMERGE_WITH_KEY_FMERGE:
1264 FMERGE f = FMERGE_WITH_KEY (\k v1 v2. f v1 v2)
1265Proof
1266 rw[FUN_EQ_THM, fmap_eq_flookup, FLOOKUP_FMERGE, FLOOKUP_FMERGE_WITH_KEY]
1267QED
1268
1269Theorem FUNION_FMERGE_WITH_KEY:
1270 !m1 m2 f. DISJOINT (FDOM m1) (FDOM m2) ==>
1271 FMERGE_WITH_KEY f m1 m2 = FUNION m1 m2
1272Proof
1273 rw[fmap_eq_flookup, FLOOKUP_FMERGE_WITH_KEY, FLOOKUP_FUNION] >>
1274 CASE_TAC >> simp[] >> CASE_TAC >> simp[] >> gvs[FLOOKUP_DEF, DISJOINT_ALT]
1275QED
1276
1277Theorem FMERGE_WITH_KEY_NO_CHANGE:
1278 (FMERGE_WITH_KEY f m1 m2 = m1 <=>
1279 !x. x IN FDOM m2 ==> x IN FDOM m1 /\ (f x (m1 ' x) (m2 ' x) = m1 ' x)) /\
1280 (FMERGE_WITH_KEY f m1 m2 = m2 <=>
1281 !x. x IN FDOM m1 ==> x IN FDOM m2 /\ (f x (m1 ' x) (m2 ' x) = m2 ' x))
1282Proof
1283 rw[fmap_eq_flookup, FLOOKUP_FMERGE_WITH_KEY] >> eq_tac >> rw[] >>
1284 gvs[FLOOKUP_DEF] >>
1285 last_x_assum $ qspec_then `x` assume_tac >> gvs[] >>
1286 every_case_tac >> gvs[]
1287QED
1288
1289Theorem FMERGE_WITH_KEY_DRESTRICT:
1290 DRESTRICT (FMERGE_WITH_KEY f m1 m2) vs =
1291 FMERGE_WITH_KEY f (DRESTRICT m1 vs) (DRESTRICT m2 vs)
1292Proof
1293 rw[fmap_eq_flookup, FLOOKUP_DRESTRICT, FLOOKUP_FMERGE_WITH_KEY] >>
1294 every_case_tac >> gvs[]
1295QED
1296
1297Theorem FMERGE_WITH_KEY_EQ_EMPTY[simp]:
1298 (FMERGE_WITH_KEY f m1 m2 = FEMPTY) <=> (m1 = FEMPTY) /\ (m2 = FEMPTY)
1299Proof
1300 rw[fmap_eq_flookup, FLOOKUP_FMERGE_WITH_KEY] >>
1301 eq_tac >> rw[] >>
1302 pop_assum $ qspec_then `x` assume_tac >> every_case_tac >> gvs[]
1303QED
1304
1305
1306(*---------------------------------------------------------------------------
1307 Universal quantifier on finite maps
1308 ---------------------------------------------------------------------------*)
1309
1310Definition FEVERY_DEF[nocompute]:
1311 FEVERY P ^fmap = !x. x IN FDOM f ==> P (x, FAPPLY f x)
1312End
1313
1314Theorem FEVERY_FEMPTY:
1315 !P:'a#'b -> bool. FEVERY P FEMPTY
1316Proof
1317 SRW_TAC [][FEVERY_DEF, FDOM_FEMPTY]
1318QED
1319
1320Theorem FEVERY_FUPDATE:
1321 !P ^fmap x y.
1322 FEVERY P (FUPDATE f (x,y))
1323 <=>
1324 P (x,y) /\ FEVERY P (DRESTRICT f (COMPL {x}))
1325Proof
1326 SRW_TAC [][FEVERY_DEF, FDOM_FUPDATE, FAPPLY_FUPDATE_THM,
1327 DRESTRICT_DEF, EQ_IMP_THM] THEN PROVE_TAC []
1328QED
1329
1330Theorem FEVERY_FLOOKUP:
1331 FEVERY P f /\ (FLOOKUP f k = SOME v) ==> P (k,v)
1332Proof
1333SRW_TAC [][FEVERY_DEF,FLOOKUP_DEF] THEN RES_TAC
1334QED
1335
1336(*---------------------------------------------------------------------------
1337 Composition of finite maps
1338 ---------------------------------------------------------------------------*)
1339
1340Theorem f_o_f_lemma[local]:
1341 !f:'b |-> 'c.
1342 !g:'a |-> 'b.
1343 ?comp. (FDOM comp = FDOM g INTER { x | FAPPLY g x IN FDOM f })
1344 /\ (!x. x IN FDOM comp ==>
1345 (FAPPLY comp x = (FAPPLY f (FAPPLY g x))))
1346Proof
1347 GEN_TAC THEN INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [
1348 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][FDOM_FEMPTY],
1349 REPEAT STRIP_TAC THEN
1350 Cases_on `y IN FDOM f` THENL [
1351 Q.EXISTS_TAC `FUPDATE comp (x, FAPPLY f y)` THEN
1352 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN
1353 PROVE_TAC [],
1354 Q.EXISTS_TAC `comp` THEN
1355 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN
1356 PROVE_TAC []
1357 ]
1358 ]
1359QED
1360
1361val f_o_f_DEF = new_specification
1362 ("f_o_f_DEF", ["f_o_f"],
1363 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) f_o_f_lemma);
1364
1365val _ = set_fixity "f_o_f" (Infixr 800);
1366
1367Theorem f_o_f_FEMPTY_1[simp]:
1368 !^fmap. (FEMPTY:('b,'c)fmap) f_o_f f = FEMPTY
1369Proof
1370 SRW_TAC [][GSYM fmap_EQ_THM, f_o_f_DEF, FDOM_FEMPTY, EXTENSION]
1371QED
1372
1373Theorem f_o_f_FEMPTY_2[simp]:
1374 !f:'b|->'c. f f_o_f (FEMPTY:('a,'b)fmap) = FEMPTY
1375Proof
1376 SRW_TAC [][GSYM fmap_EQ_THM, f_o_f_DEF, FDOM_FEMPTY]
1377QED
1378
1379
1380Theorem o_f_lemma[local]:
1381 !f:'b->'c.
1382 !g:'a|->'b.
1383 ?comp. (FDOM comp = FDOM g)
1384 /\ (!x. x IN FDOM comp ==> (FAPPLY comp x = f (FAPPLY g x)))
1385Proof
1386 GEN_TAC THEN INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [
1387 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][FDOM_FEMPTY],
1388 REPEAT STRIP_TAC THEN Q.EXISTS_TAC `FUPDATE comp (x, f y)` THEN
1389 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM]
1390 ]
1391QED
1392
1393val o_f_DEF = new_specification
1394 ("o_f_DEF", ["o_f"],
1395 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) o_f_lemma);
1396
1397val _ = set_fixity "o_f" (Infixr 800);
1398
1399Theorem o_f_FDOM:
1400 !f:'b -> 'c. !g:'a |->'b. FDOM g = FDOM (f o_f g)
1401Proof
1402REWRITE_TAC [o_f_DEF]
1403QED
1404
1405Theorem FDOM_o_f[simp] = GSYM o_f_FDOM;
1406
1407Theorem o_f_FAPPLY[simp]:
1408 !f:'b->'c. !g:('a,'b) fmap.
1409 !x. x IN FDOM g ==> (FAPPLY (f o_f g) x = f (FAPPLY g x))
1410Proof
1411 SRW_TAC [][o_f_DEF]
1412QED
1413
1414Theorem o_f_FEMPTY[simp]:
1415 f o_f FEMPTY = FEMPTY
1416Proof
1417 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_o_f]
1418QED
1419
1420Theorem o_f_id[simp]:
1421 !m. (\x.x) o_f m = m
1422Proof rw [fmap_EXT]
1423QED
1424
1425Theorem FEVERY_o_f:
1426 !m P f. FEVERY P (f o_f m) = FEVERY (\x. P (FST x, (f (SND x)))) m
1427Proof
1428 SIMP_TAC std_ss [FEVERY_DEF, FDOM_FEMPTY, NOT_IN_EMPTY, o_f_DEF]
1429QED
1430
1431Theorem o_f_o_f[simp]:
1432 (f o_f (g o_f h)) = (f o g) o_f h
1433Proof
1434 SRW_TAC [][GSYM fmap_EQ_THM, o_f_FAPPLY]
1435QED
1436
1437Theorem FLOOKUP_o_f:
1438 FLOOKUP (f o_f fm) k = case FLOOKUP fm k of NONE => NONE | SOME v => SOME (f v)
1439Proof
1440SRW_TAC [][FLOOKUP_DEF,o_f_FAPPLY]
1441QED
1442
1443(*---------------------------------------------------------------------------
1444 Range of a finite map
1445 ---------------------------------------------------------------------------*)
1446
1447Definition FRANGE_DEF[nocompute]:
1448 FRANGE ^fmap = { y | ?x. x IN FDOM f /\ (FAPPLY f x = y)}
1449End
1450
1451Theorem FRANGE_FEMPTY[simp]:
1452 FRANGE FEMPTY = {}
1453Proof
1454 SRW_TAC [][FRANGE_DEF, FDOM_FEMPTY, EXTENSION]
1455QED
1456
1457Theorem FRANGE_FUPDATE:
1458 !^fmap x y.
1459 FRANGE (FUPDATE f (x,y))
1460 =
1461 y INSERT FRANGE (DRESTRICT f (COMPL {x}))
1462Proof
1463 SRW_TAC [][FRANGE_DEF, FDOM_FUPDATE, DRESTRICT_DEF, EXTENSION,
1464 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []
1465QED
1466
1467Theorem SUBMAP_FRANGE:
1468 !^fmap g. f SUBMAP g ==> FRANGE f SUBSET FRANGE g
1469Proof
1470 SRW_TAC [][SUBMAP_DEF,FRANGE_DEF, SUBSET_DEF] THEN PROVE_TAC []
1471QED
1472
1473Theorem FINITE_FRANGE[simp]:
1474 !fm. FINITE (FRANGE fm)
1475Proof
1476 HO_MATCH_MP_TAC fmap_INDUCT THEN
1477 SRW_TAC [][FRANGE_FUPDATE] THEN
1478 Q_TAC SUFF_TAC `DRESTRICT fm (COMPL {x}) = fm` THEN1 SRW_TAC [][] THEN
1479 SRW_TAC [][GSYM fmap_EQ_THM, DRESTRICT_DEF, EXTENSION] THEN
1480 PROVE_TAC []
1481QED
1482
1483Theorem o_f_FRANGE[simp]:
1484 x IN FRANGE g ==> f x IN FRANGE (f o_f g)
1485Proof
1486 SRW_TAC [][FRANGE_DEF] THEN METIS_TAC [o_f_FAPPLY]
1487QED
1488
1489Theorem FRANGE_FLOOKUP:
1490 v IN FRANGE f <=> ?k. FLOOKUP f k = SOME v
1491Proof
1492 SRW_TAC [][FLOOKUP_DEF,FRANGE_DEF]
1493QED
1494
1495Theorem FRANGE_FUNION:
1496 DISJOINT (FDOM fm1) (FDOM fm2) ==>
1497 (FRANGE (FUNION fm1 fm2) = FRANGE fm1 UNION FRANGE fm2)
1498Proof
1499 STRIP_TAC THEN
1500 `!x. x IN FDOM fm2 ==> x NOTIN FDOM fm1`
1501 by (FULL_SIMP_TAC (srw_ss()) [DISJOINT_DEF, EXTENSION] THEN
1502 METIS_TAC []) THEN
1503 ASM_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss ++ boolSimps.CONJ_ss)
1504 [FRANGE_DEF, FUNION_DEF, EXTENSION]
1505QED
1506
1507Theorem o_f_cong[defncong]:
1508 !f fm f' fm'.
1509 (fm = fm') /\ (!v. v IN FRANGE fm ==> (f v = f' v)) ==>
1510 (f o_f fm = f' o_f fm')
1511Proof SRW_TAC[boolSimps.DNF_ss][fmap_EXT,FRANGE_DEF]
1512QED
1513
1514(*---------------------------------------------------------------------------
1515 Range restriction
1516 ---------------------------------------------------------------------------*)
1517
1518Theorem ranres_lemma[local]:
1519 !^fmap (r:'b set).
1520 ?res. (FDOM res = { x | x IN FDOM f /\ FAPPLY f x IN r})
1521 /\ (!x. FAPPLY res x =
1522 if x IN FDOM f /\ FAPPLY f x IN r
1523 then FAPPLY f x
1524 else FAPPLY FEMPTY x)
1525Proof
1526 CONV_TAC SWAP_VARS_CONV THEN GEN_TAC THEN
1527 INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [
1528 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][FDOM_FEMPTY, EXTENSION],
1529 REPEAT STRIP_TAC THEN
1530 Cases_on `y IN r` THENL [
1531 Q.EXISTS_TAC `FUPDATE res (x,y)` THEN
1532 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN
1533 PROVE_TAC [],
1534 Q.EXISTS_TAC `res` THEN
1535 SRW_TAC [][FDOM_FUPDATE, FAPPLY_FUPDATE_THM, EXTENSION] THEN
1536 PROVE_TAC []
1537 ]
1538 ]
1539QED
1540
1541val RRESTRICT_DEF = new_specification
1542 ("RRESTRICT_DEF", ["RRESTRICT"],
1543 CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) ranres_lemma);
1544
1545Theorem RRESTRICT_FEMPTY:
1546 !r. RRESTRICT FEMPTY r = FEMPTY
1547Proof
1548 SRW_TAC [][GSYM fmap_EQ_THM, RRESTRICT_DEF, FDOM_FEMPTY, EXTENSION]
1549QED
1550
1551Theorem RRESTRICT_FUPDATE:
1552 !^fmap r x y.
1553 RRESTRICT (FUPDATE f (x,y)) r =
1554 if y IN r then FUPDATE (RRESTRICT f r) (x,y)
1555 else RRESTRICT (DRESTRICT f (COMPL {x})) r
1556Proof
1557 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, RRESTRICT_DEF, DRESTRICT_DEF,
1558 EXTENSION, FAPPLY_FUPDATE_THM] THEN PROVE_TAC []
1559QED
1560
1561(*---------------------------------------------------------------------------
1562 Functions as finite maps.
1563
1564 ---------------------------------------------------------------------------*)
1565
1566Theorem ffmap_lemma[local]:
1567 !(f:'a -> 'b) (P: 'a set).
1568 FINITE P ==>
1569 ?ffmap. (FDOM ffmap = P)
1570 /\ (!x. x IN P ==> (FAPPLY ffmap x = f x))
1571Proof
1572 GEN_TAC THEN HO_MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THENL [
1573 Q.EXISTS_TAC `FEMPTY` THEN BETA_TAC THEN
1574 REWRITE_TAC [FDOM_FEMPTY, NOT_IN_EMPTY],
1575 REPEAT STRIP_TAC THEN Q.EXISTS_TAC `FUPDATE ffmap (e, f e)` THEN
1576 ASM_REWRITE_TAC [FDOM_FUPDATE, IN_INSERT, FAPPLY_FUPDATE_THM] THEN
1577 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [] THEN
1578 COND_CASES_TAC THENL [
1579 POP_ASSUM SUBST_ALL_TAC THEN RES_TAC,
1580 FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC []
1581 ]
1582 ]
1583QED
1584
1585val FUN_FMAP_DEF = new_specification
1586 ("FUN_FMAP_DEF", ["FUN_FMAP"],
1587 CONV_RULE (ONCE_DEPTH_CONV RIGHT_IMP_EXISTS_CONV THENC
1588 ONCE_DEPTH_CONV SKOLEM_CONV) ffmap_lemma);
1589
1590Theorem FUN_FMAP_EMPTY[simp]:
1591 FUN_FMAP f {} = FEMPTY
1592Proof
1593 SRW_TAC [][GSYM fmap_EQ_THM, FUN_FMAP_DEF]
1594QED
1595
1596Theorem FRANGE_FMAP[simp]:
1597 FINITE P ==> (FRANGE (FUN_FMAP f P) = IMAGE f P)
1598Proof
1599 SRW_TAC [boolSimps.CONJ_ss][EXTENSION, FRANGE_DEF, FUN_FMAP_DEF] THEN
1600 PROVE_TAC []
1601QED
1602
1603Theorem FDOM_FMAP[simp]:
1604 !f s. FINITE s ==> (FDOM (FUN_FMAP f s) = s)
1605Proof
1606SRW_TAC[][FUN_FMAP_DEF]
1607QED
1608
1609Theorem FLOOKUP_FUN_FMAP:
1610 FINITE P ==>
1611 (FLOOKUP (FUN_FMAP f P) k = if k IN P then SOME (f k) else NONE)
1612Proof
1613 SRW_TAC [][FUN_FMAP_DEF,FLOOKUP_DEF]
1614QED
1615
1616Theorem FUN_FMAP_INSERT :
1617 !f e s. FINITE s /\ e NOTIN s ==>
1618 FUN_FMAP f (e INSERT s) = FUN_FMAP f s |+ (e,f e)
1619Proof
1620 rw [fmap_EXT]
1621 >- rw [FUN_FMAP_DEF]
1622 >> ‘x IN e INSERT s’ by ASM_SET_TAC []
1623 >> ‘x <> e’ by METIS_TAC []
1624 >> rw [FAPPLY_FUPDATE_THM, FUN_FMAP_DEF]
1625QED
1626
1627(*---------------------------------------------------------------------------
1628 Composition of finite map and function
1629 ---------------------------------------------------------------------------*)
1630
1631val f_o_DEF = new_infixr_definition
1632("f_o_DEF",
1633Term`$f_o (f:('b,'c)fmap) (g:'a->'b)
1634 = f f_o_f (FUN_FMAP g { x | g x IN FDOM f})`, 800);
1635
1636Theorem FDOM_f_o[simp]:
1637 !(f:'b|->'c) (g:'a->'b).
1638 FINITE {x | g x IN FDOM f }
1639 ==>
1640 (FDOM (f f_o g) = { x | g x IN FDOM f})
1641Proof
1642 SRW_TAC [][f_o_DEF, f_o_f_DEF, EXTENSION, FUN_FMAP_DEF, EQ_IMP_THM]
1643QED
1644
1645Theorem f_o_FEMPTY[simp]:
1646 !g. FEMPTY f_o g = FEMPTY
1647Proof
1648SRW_TAC[][f_o_DEF]
1649QED
1650
1651Theorem f_o_FUPDATE:
1652 !fm k v g.
1653 FINITE {x | g x IN FDOM fm} /\
1654 FINITE {x | (g x = k)} ==>
1655 ((fm |+ (k,v)) f_o g =
1656 FMERGE (combin$C K) (fm f_o g) (FUN_FMAP (K v) {x | g x = k}))
1657Proof
1658 SRW_TAC[][] THEN
1659 `FINITE {x | (g x = k) \/ g x IN FDOM fm}` by (
1660 REPEAT (POP_ASSUM MP_TAC) THEN
1661 Q.MATCH_ABBREV_TAC `FINITE s1 ==> FINITE s2 ==> FINITE s` THEN
1662 Q_TAC SUFF_TAC `s = s1 UNION s2` THEN1 SRW_TAC[][] THEN
1663 UNABBREV_ALL_TAC THEN
1664 SRW_TAC[][EXTENSION,EQ_IMP_THM] THEN
1665 SRW_TAC[][]) THEN
1666 SRW_TAC[][GSYM fmap_EQ_THM] THEN1 (
1667 SRW_TAC[][EXTENSION,EQ_IMP_THM] THEN
1668 SRW_TAC[][]) THEN
1669 SRW_TAC[][FMERGE_DEF,FUN_FMAP_DEF,f_o_DEF,f_o_f_DEF ,FAPPLY_FUPDATE_THM]
1670QED
1671
1672Theorem FAPPLY_f_o:
1673 !(f:'b |-> 'c) (g:'a-> 'b).
1674 FINITE { x | g x IN FDOM f }
1675 ==>
1676 !x. x IN FDOM (f f_o g) ==> (FAPPLY (f f_o g) x = FAPPLY f (g x))
1677Proof
1678 SRW_TAC [][FDOM_f_o, FUN_FMAP_DEF, f_o_DEF, f_o_f_DEF]
1679QED
1680
1681
1682Theorem FINITE_PRED_11:
1683 !(g:'a -> 'b).
1684 (!x y. (g x = g y) = (x = y))
1685 ==>
1686 !f:'b|->'c. FINITE { x | g x IN FDOM f}
1687Proof
1688 GEN_TAC THEN STRIP_TAC THEN
1689 INDUCT_THEN fmap_INDUCT ASSUME_TAC THENL [
1690 SRW_TAC [][FDOM_FEMPTY, GSPEC_F],
1691 SRW_TAC [][FDOM_FUPDATE, GSPEC_OR] THEN
1692 Cases_on `?y. g y = x` THENL [
1693 POP_ASSUM (STRIP_THM_THEN SUBST_ALL_TAC o GSYM) THEN
1694 SRW_TAC [][GSPEC_EQ],
1695 POP_ASSUM MP_TAC THEN SRW_TAC [][GSPEC_F]
1696 ]
1697 ]
1698QED
1699
1700Theorem f_o_ASSOC:
1701 (!x y. (g x = g y) <=> (x = y)) /\ (!x y. (h x = h y) <=> (x = y)) ==>
1702 ((f f_o g) f_o h = f f_o (g o h))
1703Proof
1704 simp[FDOM_f_o, FINITE_PRED_11, FAPPLY_f_o, fmap_EXT]
1705QED
1706
1707(* ----------------------------------------------------------------------
1708 Domain subtraction (at a single point)
1709 ---------------------------------------------------------------------- *)
1710
1711Definition fmap_domsub:
1712 fdomsub fm k = DRESTRICT fm (COMPL {k})
1713End
1714Overload "\\\\" = “fdomsub”
1715(* this has been set up as an infix in relationTheory *)
1716
1717Theorem DOMSUB_FEMPTY[simp]:
1718 !k. FEMPTY \\ k = FEMPTY
1719Proof
1720 SRW_TAC [][GSYM fmap_EQ_THM, fmap_domsub, FDOM_DRESTRICT]
1721QED
1722
1723Theorem DOMSUB_FUPDATE[simp]:
1724 !fm k v. fm |+ (k,v) \\ k = fm \\ k
1725Proof
1726 SRW_TAC [][GSYM fmap_EQ_THM, fmap_domsub,
1727 pred_setTheory.EXTENSION, DRESTRICT_DEF,
1728 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []
1729QED
1730
1731Theorem DOMSUB_FUPDATE_NEQ:
1732 !fm k1 k2 v. ~(k1 = k2) ==> (fm |+ (k1, v) \\ k2 = fm \\ k2 |+ (k1, v))
1733Proof
1734 SRW_TAC [][GSYM fmap_EQ_THM, fmap_domsub,
1735 pred_setTheory.EXTENSION, DRESTRICT_DEF,
1736 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []
1737QED
1738
1739Theorem DOMSUB_FUPDATE_THM:
1740 !fm k1 k2 v. fm |+ (k1,v) \\ k2 = if k1 = k2 then fm \\ k2
1741 else (fm \\ k2) |+ (k1, v)
1742Proof
1743 SRW_TAC [][GSYM fmap_EQ_THM, fmap_domsub,
1744 pred_setTheory.EXTENSION, DRESTRICT_DEF,
1745 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []
1746QED
1747
1748Theorem FDOM_DOMSUB[simp]:
1749 !fm k. FDOM (fm \\ k) = FDOM fm DELETE k
1750Proof
1751 SRW_TAC [][fmap_domsub, FDOM_DRESTRICT, pred_setTheory.EXTENSION]
1752QED
1753
1754Theorem DOMSUB_FAPPLY[simp]:
1755 !fm k. (fm \\ k) ' k = FEMPTY ' k
1756Proof
1757 SRW_TAC [][fmap_domsub, DRESTRICT_DEF]
1758QED
1759
1760Theorem DOMSUB_FAPPLY_NEQ:
1761 !fm k1 k2. ~(k1 = k2) ==> ((fm \\ k1) ' k2 = fm ' k2)
1762Proof
1763 SRW_TAC [][fmap_domsub, DRESTRICT_DEF, NOT_FDOM_FAPPLY_FEMPTY]
1764QED
1765
1766Theorem DOMSUB_FAPPLY_THM:
1767 !fm k1 k2. (fm \\ k1) ' k2 = if k1 = k2 then FEMPTY ' k2 else fm ' k2
1768Proof
1769 SRW_TAC [] [DOMSUB_FAPPLY, DOMSUB_FAPPLY_NEQ]
1770QED
1771
1772Theorem DOMSUB_FLOOKUP[simp]:
1773 !fm k. FLOOKUP (fm \\ k) k = NONE
1774Proof
1775 SRW_TAC [][FLOOKUP_DEF, FDOM_DOMSUB]
1776QED
1777
1778Theorem DOMSUB_FLOOKUP_NEQ:
1779 !fm k1 k2. ~(k1 = k2) ==> (FLOOKUP (fm \\ k1) k2 = FLOOKUP fm k2)
1780Proof
1781 SRW_TAC [][FLOOKUP_DEF, FDOM_DOMSUB, DOMSUB_FAPPLY_NEQ]
1782QED
1783
1784Theorem DOMSUB_FLOOKUP_THM:
1785 !fm k1 k2. FLOOKUP (fm \\ k1) k2 = if k1 = k2 then NONE else FLOOKUP fm k2
1786Proof
1787 SRW_TAC [][DOMSUB_FLOOKUP, DOMSUB_FLOOKUP_NEQ]
1788QED
1789
1790Theorem FRANGE_FUPDATE_DOMSUB[simp]:
1791 !fm k v. FRANGE (fm |+ (k,v)) = v INSERT FRANGE (fm \\ k)
1792Proof
1793 SRW_TAC [][FRANGE_FUPDATE, fmap_domsub]
1794QED
1795
1796
1797Theorem o_f_DOMSUB[simp]:
1798 (g o_f fm) \\ k = g o_f (fm \\ k)
1799Proof
1800 SRW_TAC [][GSYM fmap_EQ_THM, DOMSUB_FAPPLY_THM, o_f_FAPPLY]
1801QED
1802
1803Theorem DOMSUB_IDEM[simp]:
1804 (fm \\ k) \\ k = fm \\ k
1805Proof
1806 SRW_TAC [][GSYM fmap_EQ_THM, DOMSUB_FAPPLY_THM]
1807QED
1808
1809Theorem DOMSUB_COMMUTES:
1810 fm \\ k1 \\ k2 = fm \\ k2 \\ k1
1811Proof
1812 SRW_TAC [][GSYM fmap_EQ,DELETE_COMM] THEN
1813 SRW_TAC [][FUN_EQ_THM,DOMSUB_FAPPLY_THM] THEN
1814 SRW_TAC [][]
1815QED
1816
1817Theorem o_f_FUPDATE[simp]:
1818 f o_f (fm |+ (k,v)) = (f o_f fm) |+ (k, f v)
1819Proof
1820 SRW_TAC [][fmap_EXT]
1821 THENL [
1822 SRW_TAC [][o_f_FAPPLY, FDOM_o_f],
1823 SRW_TAC [][FAPPLY_FUPDATE_THM]
1824 ]
1825QED
1826
1827Theorem DOMSUB_NOT_IN_DOM:
1828 ~(k IN FDOM fm) ==> (fm \\ k = fm)
1829Proof
1830 SRW_TAC [][GSYM fmap_EQ_THM, DOMSUB_FAPPLY_THM,
1831 EXTENSION] THEN PROVE_TAC []
1832QED
1833
1834Theorem fmap_CASES:
1835 !f:'a |-> 'b. (f = FEMPTY) \/ ?g x y. f = g |+ (x,y)
1836Proof
1837 HO_MATCH_MP_TAC fmap_SIMPLE_INDUCT THEN METIS_TAC []
1838QED
1839
1840Theorem IN_DOMSUB_NOT_EQUAL[local]:
1841 !f:'a |->'b. !x1 x2. x2 IN FDOM (f \\ x1) ==> ~(x2 = x1)
1842Proof
1843 RW_TAC std_ss [FDOM_DOMSUB,IN_DELETE]
1844QED
1845
1846Theorem SUBMAP_DOMSUB[simp]:
1847 (f \\ k) SUBMAP f
1848Proof SRW_TAC [][fmap_domsub]
1849QED
1850
1851Theorem FMERGE_DOMSUB:
1852 !m m1 m2 k. (FMERGE m m1 m2) \\ k = FMERGE m (m1 \\ k) (m2 \\ k)
1853Proof
1854SRW_TAC[][fmap_domsub,FMERGE_DRESTRICT]
1855QED
1856
1857
1858(*---------------------------------------------------------------------------*)
1859(* Is there a better statement of this? *)
1860(*---------------------------------------------------------------------------*)
1861
1862Theorem SUBMAP_FUPDATE:
1863 !(f:'a |->'b) g x y.
1864 (f |+ (x,y)) SUBMAP g <=>
1865 x IN FDOM(g) /\ g ' x = y /\ (f\\x) SUBMAP (g\\x)
1866Proof
1867 SRW_TAC [boolSimps.DNF_ss][SUBMAP_DEF, DOMSUB_FAPPLY_THM,
1868 FAPPLY_FUPDATE_THM] THEN
1869 METIS_TAC []
1870QED
1871
1872(* ----------------------------------------------------------------------
1873 Iterated updates
1874 ---------------------------------------------------------------------- *)
1875
1876Definition FUPDATE_LIST:
1877 FUPDATE_LIST = FOLDL FUPDATE
1878End
1879
1880Overload "|++" = “FUPDATE_LIST”
1881
1882Theorem FUPDATE_LIST_THM:
1883 !f. (f |++ [] = f) /\
1884 (!h t. f |++ (h::t) = (FUPDATE f h) |++ t)
1885Proof
1886 SRW_TAC [][FUPDATE_LIST]
1887QED
1888
1889Theorem FUPDATE_LIST_APPLY_NOT_MEM:
1890 !kvl f k. ~MEM k (MAP FST kvl) ==> ((f |++ kvl) ' k = f ' k)
1891Proof
1892 Induct THEN SRW_TAC [][FUPDATE_LIST_THM] THEN
1893 Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [FAPPLY_FUPDATE_THM]
1894QED
1895
1896Theorem FUPDATE_LIST_APPEND:
1897 fm |++ (kvl1 ++ kvl2) = fm |++ kvl1 |++ kvl2
1898Proof
1899Q.ID_SPEC_TAC `fm` THEN Induct_on `kvl1` THEN SRW_TAC [][FUPDATE_LIST_THM]
1900QED
1901
1902Theorem FUPDATE_FUPDATE_LIST_COMMUTES:
1903 ~MEM k (MAP FST kvl) ==> (fm |+ (k,v) |++ kvl = (fm |++ kvl) |+ (k,v))
1904Proof
1905let open rich_listTheory in
1906Q.ID_SPEC_TAC `kvl` THEN
1907HO_MATCH_MP_TAC SNOC_INDUCT THEN
1908SRW_TAC [][FUPDATE_LIST_THM] THEN
1909FULL_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM,MAP_SNOC,SNOC_APPEND,FUPDATE_LIST_APPEND] THEN
1910Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [FUPDATE_COMMUTES]
1911end
1912QED
1913
1914Theorem FUPDATE_FUPDATE_LIST_MEM:
1915 MEM k (MAP FST kvl) ==> (fm |+ (k,v) |++ kvl = fm |++ kvl)
1916Proof
1917Q.ID_SPEC_TAC `fm` THEN
1918Induct_on `kvl` THEN SRW_TAC [][FUPDATE_LIST_THM] THEN
1919Cases_on `h` THEN SRW_TAC [][] THEN
1920FULL_SIMP_TAC (srw_ss()) [] THEN
1921Cases_on `k = q` THEN SRW_TAC [][] THEN
1922METIS_TAC [FUPDATE_COMMUTES]
1923QED
1924
1925Theorem FEVERY_FUPDATE_LIST:
1926 ALL_DISTINCT (MAP FST kvl) ==>
1927 (FEVERY P (fm |++ kvl) <=> EVERY P kvl /\ FEVERY P (DRESTRICT fm (COMPL (set (MAP FST kvl)))))
1928Proof
1929Q.ID_SPEC_TAC `fm` THEN
1930Induct_on `kvl` THEN SRW_TAC [][FUPDATE_LIST_THM,DRESTRICT_UNIV] THEN
1931Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1932SRW_TAC [][FUPDATE_FUPDATE_LIST_COMMUTES,FEVERY_FUPDATE] THEN
1933FULL_SIMP_TAC (srw_ss()) [GSYM COMPL_UNION] THEN
1934SRW_TAC [][Once UNION_COMM] THEN
1935SRW_TAC [][Once (GSYM INSERT_SING_UNION)] THEN
1936SRW_TAC [][EQ_IMP_THM]
1937QED
1938
1939Theorem FUPDATE_LIST_APPLY_MEM:
1940 !kvl f k v n.
1941 n < LENGTH kvl /\ (k = EL n (MAP FST kvl)) /\ (v = EL n (MAP SND kvl)) /\
1942 (!m. n < m /\ m < LENGTH kvl ==> (EL m (MAP FST kvl) <> k))
1943 ==>
1944 ((f |++ kvl) ' k = v)
1945Proof
1946 Induct THEN1 SRW_TAC[][] THEN
1947 Cases THEN NTAC 3 GEN_TAC THEN
1948 Cases THEN1 (
1949 Q.MATCH_RENAME_TAC `0 < LENGTH ((q,r)::kvl) /\ _ ==> _` >>
1950 Q.ISPECL_THEN [`kvl`,`f |+ (k,r)`,`k`] MP_TAC FUPDATE_LIST_APPLY_NOT_MEM >>
1951 SRW_TAC[][FUPDATE_LIST_THM] >> FIRST_X_ASSUM MATCH_MP_TAC >>
1952 SRW_TAC[][listTheory.MEM_MAP,listTheory.MEM_EL,pairTheory.EXISTS_PROD] >>
1953 STRIP_TAC >> rename [‘(k,v) = EL n kvl’] >>
1954 FIRST_X_ASSUM (Q.SPEC_THEN `SUC n` MP_TAC) THEN
1955 SRW_TAC[][listTheory.EL_MAP] THEN
1956 METIS_TAC[pairTheory.FST]) THEN
1957 SRW_TAC[][] THEN
1958 Q.MATCH_RENAME_TAC `(f |++ ((q,r)::kvl)) ' _ = _` THEN
1959 Q.ISPECL_THEN [`(q,r)`,`kvl`] SUBST1_TAC rich_listTheory.CONS_APPEND THEN
1960 REWRITE_TAC [FUPDATE_LIST_APPEND] THEN
1961 FIRST_X_ASSUM MATCH_MP_TAC THEN
1962 Q.MATCH_ASSUM_RENAME_TAC `n < LENGTH kvl` THEN
1963 Q.EXISTS_TAC `n` THEN
1964 SRW_TAC[][] THEN
1965 Q.MATCH_RENAME_TAC `EL m (MAP FST kvl) <> _` THEN
1966 FIRST_X_ASSUM (Q.SPEC_THEN `SUC m` MP_TAC) THEN
1967 SRW_TAC[][]
1968QED
1969
1970Theorem FOLDL_FUPDATE_LIST:
1971 !f1 f2 ls a. FOLDL (\fm k. fm |+ (f1 k, f2 k)) a ls =
1972 a |++ MAP (\k. (f1 k, f2 k)) ls
1973Proof
1974 SRW_TAC[][FUPDATE_LIST,rich_listTheory.FOLDL_MAP]
1975QED
1976
1977Theorem FUPDATE_LIST_SNOC:
1978 !xs x fm. fm |++ SNOC x xs = (fm |++ xs) |+ x
1979Proof
1980 Induct THEN SRW_TAC[][FUPDATE_LIST_THM]
1981QED
1982
1983Theorem DOMSUB_FUPDATE_LIST:
1984 !l m x. (m |++ l) \\ x = (m \\ x) |++ (FILTER ($<> x o FST) l)
1985Proof
1986 Induct >> rw[FUPDATE_LIST_THM, fmap_eq_flookup] >>
1987 PairCases_on `h` >> gvs[] >> simp[DOMSUB_FUPDATE_THM]
1988QED
1989
1990
1991
1992(* ----------------------------------------------------------------------
1993 More theorems
1994 ---------------------------------------------------------------------- *)
1995
1996Theorem FAPPLY_FUPD_EQ[local]:
1997 !fmap k1 v1 k2 v2.
1998 ((fmap |+ (k1, v1)) ' k2 = v2) <=>
1999 k1 = k2 /\ v1 = v2 \/ k1 <> k2 /\ fmap ' k2 = v2
2000Proof
2001 SRW_TAC [][FAPPLY_FUPDATE_THM, EQ_IMP_THM]
2002QED
2003
2004
2005(* (pseudo) injectivity results about fupdate *)
2006Theorem FEMPTY_FUPDATE_EQ:
2007 !x y. (FEMPTY |+ x = FEMPTY |+ y) <=> (x = y)
2008Proof
2009 Cases >> Cases >> srw_tac[][fmap_eq_flookup,FDOM_FUPDATE,FLOOKUP_UPDATE] >>
2010 Cases_on`q=q'`>>srw_tac[][] >- (
2011 srw_tac[][EQ_IMP_THM] >>
2012 pop_assum(qspec_then`q`mp_tac) >> srw_tac[][] ) >>
2013 qexists_tac`q`>>srw_tac[][]
2014QED
2015
2016Theorem FUPD11_SAME_KEY_AND_BASE:
2017 !f k v1 v2. (f |+ (k, v1) = f |+ (k, v2)) <=> (v1 = v2)
2018Proof
2019 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, DISJ_IMP_THM,
2020 FAPPLY_FUPDATE_THM, FORALL_AND_THM, EQ_IMP_THM]
2021QED
2022
2023Theorem FUPD11_SAME_NEW_KEY:
2024 !f1 f2 k v1 v2.
2025 ~(k IN FDOM f1) /\ ~(k IN FDOM f2) ==>
2026 ((f1 |+ (k, v1) = f2 |+ (k, v2)) <=> (f1 = f2) /\ (v1 = v2))
2027Proof
2028 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, DISJ_IMP_THM,
2029 FAPPLY_FUPDATE_THM, FORALL_AND_THM, EQ_IMP_THM, EXTENSION] THEN
2030 PROVE_TAC []
2031QED
2032
2033Theorem SAME_KEY_UPDATES_DIFFER:
2034 !f1 f2 k v1 v2. v1 <> v2 ==> ~(f1 |+ (k, v1) = f2 |+ (k, v2))
2035Proof
2036 SRW_TAC [][GSYM fmap_EQ_THM, FDOM_FUPDATE, RIGHT_AND_OVER_OR,
2037 EXISTS_OR_THM]
2038QED
2039
2040Theorem FUPD11_SAME_BASE:
2041 !f k1 v1 k2 v2.
2042 (f |+ (k1, v1) = f |+ (k2, v2)) <=>
2043 (k1 = k2) /\ (v1 = v2) \/
2044 ~(k1 = k2) /\ k1 IN FDOM f /\ k2 IN FDOM f /\
2045 (f |+ (k1, v1) = f) /\ (f |+ (k2, v2) = f)
2046Proof
2047 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE, GSYM fmap_EQ_THM,
2048 DISJ_IMP_THM, FORALL_AND_THM, FAPPLY_FUPDATE_THM,
2049 EXTENSION] THEN PROVE_TAC[]
2050QED
2051
2052Theorem FUPD_SAME_KEY_UNWIND:
2053 !f1 f2 k v1 v2.
2054 (f1 |+ (k, v1) = f2 |+ (k, v2)) ==>
2055 (v1 = v2) /\ (!v. f1 |+ (k, v) = f2 |+ (k, v))
2056Proof
2057 SRW_TAC [][FDOM_FEMPTY, FDOM_FUPDATE, GSYM fmap_EQ_THM,
2058 DISJ_IMP_THM, FORALL_AND_THM, FAPPLY_FUPDATE_THM,
2059 EXTENSION] THEN PROVE_TAC[]
2060QED
2061
2062Theorem FUPD11_SAME_UPDATE:
2063 !f1 f2 k v. (f1 |+ (k,v) = f2 |+ (k,v)) =
2064 (DRESTRICT f1 (COMPL {k}) = DRESTRICT f2 (COMPL {k}))
2065Proof
2066 SRW_TAC [][GSYM fmap_EQ_THM, EXTENSION, DRESTRICT_DEF, FDOM_FUPDATE,
2067 FAPPLY_FUPDATE_THM] THEN PROVE_TAC []
2068QED
2069
2070Theorem FDOM_FUPDATE_LIST:
2071 !kvl fm. FDOM (fm |++ kvl) =
2072 FDOM fm UNION set (MAP FST kvl)
2073Proof
2074 Induct THEN
2075 ASM_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM,
2076 FDOM_FUPDATE, pairTheory.FORALL_PROD,
2077 EXTENSION] THEN PROVE_TAC []
2078QED
2079
2080Theorem FUPDATE_LIST_EQ_FEMPTY:
2081 !fm ls. (fm |++ ls = FEMPTY) <=> (fm = FEMPTY) /\ (ls = [])
2082Proof
2083 srw_tac[][EQ_IMP_THM,FUPDATE_LIST_THM] >>
2084 full_simp_tac(srw_ss())[GSYM fmap_EQ_THM,FDOM_FUPDATE_LIST]
2085QED
2086
2087Theorem FUPDATE_LIST_SAME_UPDATE:
2088 !kvl f1 f2. (f1 |++ kvl = f2 |++ kvl) =
2089 (DRESTRICT f1 (COMPL (set (MAP FST kvl))) =
2090 DRESTRICT f2 (COMPL (set (MAP FST kvl))))
2091Proof
2092 Induct THENL [
2093 SRW_TAC [][GSYM fmap_EQ_THM, FUPDATE_LIST_THM, DRESTRICT_DEF] THEN
2094 PROVE_TAC [],
2095 ASM_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM, pairTheory.FORALL_PROD] THEN
2096 POP_ASSUM (K ALL_TAC) THEN
2097 SRW_TAC [][GSYM fmap_EQ_THM, FUPDATE_LIST_THM, DRESTRICT_DEF,
2098 FDOM_FUPDATE, FDOM_FUPDATE_LIST, EXTENSION,
2099 FAPPLY_FUPDATE_THM] THEN
2100 EQ_TAC THEN REPEAT STRIP_TAC THEN REPEAT COND_CASES_TAC THEN
2101 SRW_TAC [][] THEN PROVE_TAC []
2102 ]
2103QED
2104
2105Theorem FUPDATE_LIST_SAME_KEYS_UNWIND:
2106 !f1 f2 kvl1 kvl2.
2107 (f1 |++ kvl1 = f2 |++ kvl2) /\
2108 (MAP FST kvl1 = MAP FST kvl2) /\ ALL_DISTINCT (MAP FST kvl1) ==>
2109 (kvl1 = kvl2) /\
2110 !kvl. (MAP FST kvl = MAP FST kvl1) ==>
2111 (f1 |++ kvl = f2 |++ kvl)
2112Proof
2113 CONV_TAC (BINDER_CONV SWAP_VARS_CONV THENC SWAP_VARS_CONV) THEN
2114 Induct THEN ASM_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM] THEN
2115 REPEAT GEN_TAC THEN
2116 `?k v. h = (k,v)` by PROVE_TAC [pair_CASES] THEN
2117 POP_ASSUM SUBST_ALL_TAC THEN SIMP_TAC (srw_ss()) [] THEN
2118 `(kvl2 = []) \/ ?k2 v2 t2. kvl2 = (k2,v2) :: t2` by
2119 PROVE_TAC [pair_CASES, listTheory.list_CASES] THEN
2120 POP_ASSUM SUBST_ALL_TAC THEN SIMP_TAC (srw_ss()) [] THEN
2121 SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM] THEN STRIP_TAC THEN
2122 `kvl1 = t2` by PROVE_TAC [] THEN POP_ASSUM SUBST_ALL_TAC THEN
2123 `v = v2` by (FIRST_X_ASSUM (MP_TAC o C Q.AP_THM `k` o Q.AP_TERM `(')`) THEN
2124 SRW_TAC [][FUPDATE_LIST_APPLY_NOT_MEM]) THEN
2125 SRW_TAC [][] THEN
2126 `(kvl = []) \/ (?k' v' t. kvl = (k',v') :: t)` by
2127 PROVE_TAC [pair_CASES, listTheory.list_CASES] THEN
2128 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN
2129 Q.PAT_X_ASSUM `fm : 'a |-> 'b = fm1` MP_TAC THEN
2130 SIMP_TAC (srw_ss()) [GSYM FUPDATE_LIST_THM] THEN
2131 ASM_SIMP_TAC (srw_ss()) [FUPDATE_LIST_SAME_UPDATE]
2132QED
2133
2134Theorem lemma[local]:
2135 !kvl k fm. MEM k (MAP FST kvl) ==>
2136 MEM (k, (fm |++ kvl) ' k) kvl
2137Proof
2138 Induct THEN
2139 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, FUPDATE_LIST_THM,
2140 DISJ_IMP_THM, FORALL_AND_THM] THEN
2141 REPEAT STRIP_TAC THEN
2142 Cases_on `MEM p_1 (MAP FST kvl)` THEN
2143 SRW_TAC [][FUPDATE_LIST_APPLY_NOT_MEM]
2144QED
2145
2146Theorem FMEQ_ENUMERATE_CASES:
2147 !f1 kvl p. (f1 |+ p = FEMPTY |++ kvl) ==> MEM p kvl
2148Proof
2149 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, GSYM fmap_EQ_THM,
2150 FDOM_FUPDATE, FDOM_FUPDATE_LIST, DISJ_IMP_THM,
2151 FORALL_AND_THM, FDOM_FEMPTY] THEN
2152 REPEAT STRIP_TAC THEN
2153 FULL_SIMP_TAC (srw_ss()) [pred_setTheory.EXTENSION] THEN
2154 PROVE_TAC [lemma]
2155QED
2156
2157Theorem FMEQ_SINGLE_SIMPLE_ELIM:
2158 !P k v ck cv nv. (?fm. (fm |+ (k, v) = FEMPTY |+ (ck, cv)) /\
2159 P (fm |+ (k, nv))) <=>
2160 (k = ck) /\ (v = cv) /\ P (FEMPTY |+ (ck, nv))
2161Proof
2162 REPEAT GEN_TAC THEN EQ_TAC THEN STRIP_TAC THENL [
2163 `FEMPTY |+ (ck, cv) = FEMPTY |++ [(ck,cv)]`
2164 by SRW_TAC [][FUPDATE_LIST_THM] THEN
2165 `MEM (k,v) [(ck, cv)]` by PROVE_TAC [FMEQ_ENUMERATE_CASES] THEN
2166 FULL_SIMP_TAC (srw_ss()) [FUPDATE_LIST_THM] THEN
2167 PROVE_TAC [FUPD_SAME_KEY_UNWIND],
2168 Q.EXISTS_TAC `FEMPTY` THEN SRW_TAC [][]
2169 ]
2170QED
2171
2172Theorem FMEQ_SINGLE_SIMPLE_DISJ_ELIM:
2173 !fm k v ck cv.
2174 (fm |+ (k,v) = FEMPTY |+ (ck, cv)) <=>
2175 (k = ck) /\ (v = cv) /\
2176 ((fm = FEMPTY) \/ (?v'. fm = FEMPTY |+ (k, v')))
2177Proof
2178 REPEAT GEN_TAC THEN EQ_TAC THEN
2179 SIMP_TAC (srw_ss()) [DISJ_IMP_THM, LEFT_AND_OVER_OR,
2180 GSYM RIGHT_EXISTS_AND_THM,
2181 GSYM LEFT_FORALL_IMP_THM] THEN
2182 SIMP_TAC (srw_ss() ++ boolSimps.CONJ_ss)
2183 [GSYM fmap_EQ_THM, DISJ_IMP_THM, FORALL_AND_THM] THEN
2184 SIMP_TAC (srw_ss()) [EXTENSION] THEN
2185 PROVE_TAC [FAPPLY_FUPDATE]
2186QED
2187
2188
2189(* ----------------------------------------------------------------------
2190 folding over a finite map : ITFMAP (named by analogy with ITSET and
2191 ITBAG)
2192 ---------------------------------------------------------------------- *)
2193
2194Inductive ITFMAPR:
2195 (!A. ITFMAPR f FEMPTY A A) /\
2196 (!A1 A2 k v fm.
2197 k NOTIN FDOM fm /\ ITFMAPR f fm A1 A2 ==>
2198 ITFMAPR f (fm |+ (k,v)) A1 (f k v A2))
2199End
2200
2201Theorem ITFMAPR_FEMPTY[simp]:
2202 ITFMAPR f FEMPTY A1 A2 <=> A1 = A2
2203Proof
2204 simp[Once ITFMAPR_cases] >> metis_tac[]
2205QED
2206
2207Theorem ITFMAPR_total:
2208 !fm r0. ?r. ITFMAPR f fm r0 r
2209Proof
2210 ho_match_mp_tac fmap_INDUCT >> metis_tac[ITFMAPR_rules, DOMSUB_NOT_IN_DOM]
2211QED
2212
2213Theorem FUPDATE_PURGE'[simp]:
2214 !f x y. (f \\ x) |+ (x,y) = f |+ (x,y)
2215Proof
2216 SRW_TAC [] [fmap_EXT,EXTENSION,FAPPLY_FUPDATE_THM,DOMSUB_FAPPLY_THM] THEN
2217 METIS_TAC[]
2218QED
2219
2220Theorem FUPDATE_PURGE:
2221 !f x y. f |+ (x,y) = (f \\ x) |+ (x, y)
2222Proof
2223 simp[]
2224QED
2225
2226Theorem fmap_cases_NOTIN:
2227 !fm. fm = FEMPTY \/ ?k v fm0. k NOTIN FDOM fm0 /\ fm = fm0 |+ (k,v)
2228Proof
2229 gen_tac >> qspec_then ‘fm’ strip_assume_tac fmap_CASES >> fs[] >>
2230 rename [‘fm = fm0 |+ (k,v)’] >>
2231 map_every qexists_tac [‘k’, ‘v’, ‘fm0 \\ k’] >> simp[]
2232QED
2233
2234Theorem ITFMAPR_unique:
2235 (!k1 k2 v1 v2 A. k1 <> k2 ==> f k1 v1 (f k2 v2 A) = f k2 v2 (f k1 v1 A)) ==>
2236 !fm A0 A1 A2. ITFMAPR f fm A0 A1 /\ ITFMAPR f fm A0 A2 ==> A1 = A2
2237Proof
2238 strip_tac >> gen_tac >> completeInduct_on ‘CARD (FDOM fm)’ >> rw[] >>
2239 Cases_on ‘fm = FEMPTY’ >> fs[] >>
2240 qpat_x_assum ‘ITFMAPR _ _ _ A2’ mp_tac >>
2241 simp[Once ITFMAPR_cases] >>
2242 qpat_x_assum ‘ITFMAPR _ _ _ A1’ mp_tac >>
2243 simp[Once ITFMAPR_cases] >>
2244 disch_then (qx_choosel_then [‘A1a’, ‘k1’, ‘v1’, ‘fm1’] strip_assume_tac) >>
2245 disch_then (qx_choosel_then [‘A1b’, ‘k2’, ‘v2’, ‘fm2’] strip_assume_tac) >>
2246 Cases_on ‘k1 = k2’ >> fs[]
2247 >- (‘v1 = v2 /\ fm1 = fm2’ by metis_tac[FUPD11_SAME_NEW_KEY] >> rw[] >>
2248 fs[PULL_FORALL] >> metis_tac[DECIDE “x < SUC x”]) >>
2249 ‘?A0'. ITFMAPR f (fm1 \\ k2) A0 A0'’ by metis_tac[ITFMAPR_total] >>
2250 ‘fm1 \\ k2 = fm2 \\ k1’
2251 by (rw[fmap_EXT]
2252 >- (simp[EXTENSION] >> fs[fmap_EXT, EXTENSION] >> metis_tac[]) >>
2253 rw[DOMSUB_FAPPLY_THM] >> fs[] >>
2254 fs[fmap_EXT, FAPPLY_FUPDATE_THM, EXTENSION] >> metis_tac[]) >>
2255 fs[PULL_FORALL] >>
2256 ‘ITFMAPR f ((fm2 \\ k1) |+ (k2,v2)) A0 (f k2 v2 A0')’
2257 by metis_tac[ITFMAPR_rules, FDOM_DOMSUB, IN_DELETE] >>
2258 qabbrev_tac ‘base = fm2 \\ k1’ >>
2259 ‘fm1 = base |+ (k2,v2) /\ fm2 = base |+ (k1,v1)’
2260 by (rw[Abbr‘base’] >>
2261 fs[fmap_EXT, EXTENSION, FAPPLY_FUPDATE_THM, DOMSUB_FAPPLY_THM] >>
2262 PROVE_TAC[]) >>
2263 ‘k1 NOTIN FDOM base /\ k2 NOTIN FDOM base’
2264 by metis_tac[FDOM_DOMSUB, IN_DELETE] >>
2265 markerLib.RM_ABBREV_TAC "base" >>
2266 qpat_x_assum ‘_ = base’ (K ALL_TAC) >> rw[] >> fs[] >>
2267 ‘CARD (FDOM (base |+ (k2,v2))) < SUC (SUC (CARD (FDOM base)))’ by simp[] >>
2268 first_assum drule >> strip_tac >> ‘f k2 v2 A0' = A1a’ by metis_tac[] >>
2269 pop_assum (SUBST_ALL_TAC o GSYM) >> pop_assum (K ALL_TAC) >>
2270 ‘ITFMAPR f (base |+ (k1,v1)) A0 (f k1 v1 A0')’ by metis_tac[ITFMAPR_rules] >>
2271 ‘CARD (FDOM (base |+ (k1,v1))) < SUC (SUC (CARD (FDOM base)))’ by simp[] >>
2272 first_x_assum drule >>
2273 disch_then (qspecl_then [‘A0’, ‘A1b’, ‘f k1 v1 A0'’] mp_tac) >> simp[]
2274QED
2275
2276Definition ITFMAP_def:
2277 ITFMAP f fm A0 = @A. ITFMAPR f fm A0 A
2278End
2279
2280Theorem ITFMAP_thm:
2281 (ITFMAP f FEMPTY A = A) /\
2282 ((!k1 k2 v1 v2 A. k1 <> k2 ==> f k1 v1 (f k2 v2 A) = f k2 v2 (f k1 v1 A))
2283 ==>
2284 ITFMAP f (fm |+ (k,v)) A = f k v (ITFMAP f (fm\\k) A))
2285Proof
2286 simp[ITFMAP_def] >>
2287 strip_tac >> qabbrev_tac ‘b = @A'. ITFMAPR f (fm\\k) A A'’ >>
2288 ‘ITFMAPR f (fm \\ k) A b’
2289 by (simp[Abbr‘b’] >> SELECT_ELIM_TAC >> metis_tac[ITFMAPR_total]) >>
2290 ‘ITFMAPR f ((fm\\k) |+ (k,v)) A (f k v b)’
2291 by simp[FDOM_DOMSUB, ITFMAPR_rules] >>
2292 fs[] >> SELECT_ELIM_TAC >> metis_tac[ITFMAPR_unique]
2293QED
2294
2295Theorem ITFMAP_FEMPTY[simp]:
2296 ITFMAP f FEMPTY A = A
2297Proof
2298 simp[ITFMAP_thm]
2299QED
2300
2301(*---------------------------------------------------------------------------*)
2302(* For EVAL on terms with finite map expressions. *)
2303(*---------------------------------------------------------------------------*)
2304
2305val _ =
2306 computeLib.add_persistent_funs
2307 ["FUPDATE_LIST_THM",
2308 "DOMSUB_FUPDATE_THM",
2309 "DOMSUB_FEMPTY",
2310 "FDOM_FUPDATE",
2311 "FAPPLY_FUPDATE_THM",
2312 "FDOM_FEMPTY",
2313 "FLOOKUP_EMPTY",
2314 "FLOOKUP_UPDATE"];
2315
2316
2317(*---------------------------------------------------------------------------*)
2318(* Mapping for finite maps with two arguments, compare to o_f *)
2319(* added 17 March 2009 by Thomas Tuerk, updated 26 March *)
2320(*---------------------------------------------------------------------------*)
2321
2322Definition FMAP_MAP2_def:
2323 FMAP_MAP2 f m = FUN_FMAP (\x. f (x,m ' x)) (FDOM m)
2324End
2325
2326
2327Theorem FMAP_MAP2_THM:
2328 (FDOM (FMAP_MAP2 f m) = FDOM m) /\
2329 (!x. x IN FDOM m ==> ((FMAP_MAP2 f m) ' x = f (x,m ' x)))
2330Proof
2331
2332SIMP_TAC std_ss [FMAP_MAP2_def,
2333 FUN_FMAP_DEF, FDOM_FINITE]
2334QED
2335
2336
2337
2338Theorem FMAP_MAP2_FEMPTY:
2339 FMAP_MAP2 f FEMPTY = FEMPTY
2340Proof
2341
2342SIMP_TAC std_ss [GSYM fmap_EQ_THM, FMAP_MAP2_THM,
2343 FDOM_FEMPTY, NOT_IN_EMPTY]
2344QED
2345
2346
2347Theorem FMAP_MAP2_FUPDATE:
2348 FMAP_MAP2 f (m |+ (x, v)) =
2349 (FMAP_MAP2 f m) |+ (x, f (x,v))
2350Proof
2351
2352SIMP_TAC std_ss [GSYM fmap_EQ_THM, FMAP_MAP2_THM,
2353 FDOM_FUPDATE, IN_INSERT,
2354 FAPPLY_FUPDATE_THM,
2355 COND_RAND, COND_RATOR,
2356 DISJ_IMP_THM]
2357QED
2358
2359Theorem FLOOKUP_FMAP_MAP2:
2360 !f m k. FLOOKUP (FMAP_MAP2 f m) k = OPTION_MAP (\v. f (k,v)) (FLOOKUP m k)
2361Proof
2362 rw[FLOOKUP_DEF, FMAP_MAP2_def, FUN_FMAP_DEF]
2363QED
2364
2365Theorem DOMSUB_FMAP_MAP2:
2366 !f m s. (FMAP_MAP2 f m) \\ s = FMAP_MAP2 f (m \\ s)
2367Proof
2368 rw[fmap_eq_flookup, DOMSUB_FLOOKUP_THM, FLOOKUP_FMAP_MAP2] >>
2369 IF_CASES_TAC >> simp[]
2370QED
2371
2372Theorem FMAP_MAP2_FUPDATE_LIST:
2373 !l m f.
2374 FMAP_MAP2 f (m |++ l) = FMAP_MAP2 f m |++ MAP (\(k,v). (k, f (k,v))) l
2375Proof
2376 Induct >> rw[FUPDATE_LIST_THM] >>
2377 PairCases_on `h` >> simp[FMAP_MAP2_FUPDATE]
2378QED
2379
2380
2381(*---------------------------------------------------------------------------*)
2382(* Some general stuff *)
2383(* added 17 March 2009 by Thomas Tuerk *)
2384(*---------------------------------------------------------------------------*)
2385
2386Theorem FEVERY_STRENGTHEN_THM:
2387 FEVERY P FEMPTY /\
2388 ((FEVERY P f /\ P (x,y)) ==> FEVERY P (f |+ (x,y)))
2389Proof
2390
2391SIMP_TAC std_ss [FEVERY_DEF, FDOM_FEMPTY,
2392 NOT_IN_EMPTY, FAPPLY_FUPDATE_THM,
2393 FDOM_FUPDATE, IN_INSERT] THEN
2394METIS_TAC[]
2395QED
2396
2397
2398
2399Theorem FUPDATE_ELIM:
2400 !k v f.
2401 ((k IN FDOM f) /\ (f ' k = v)) ==> (f |+ (k,v) = f)
2402Proof
2403
2404REPEAT STRIP_TAC THEN
2405ONCE_REWRITE_TAC[GSYM fmap_EQ_THM] THEN
2406SIMP_TAC std_ss [FDOM_FUPDATE, IN_INSERT, EXTENSION,
2407 FAPPLY_FUPDATE_THM] THEN
2408PROVE_TAC[]
2409QED
2410
2411
2412
2413Theorem FEVERY_DRESTRICT_COMPL:
2414 FEVERY P (DRESTRICT (f |+ (k, v)) (COMPL s)) =
2415 ((~(k IN s) ==> P (k,v)) /\
2416 (FEVERY P (DRESTRICT f (COMPL (k INSERT s)))))
2417Proof
2418
2419SIMP_TAC std_ss [FEVERY_DEF, IN_INTER,
2420 FDOM_DRESTRICT,
2421 DRESTRICT_DEF, FAPPLY_FUPDATE_THM,
2422 FDOM_FUPDATE, IN_INSERT,
2423 RIGHT_AND_OVER_OR, IN_COMPL,
2424 DISJ_IMP_THM, FORALL_AND_THM] THEN
2425PROVE_TAC[]
2426QED
2427
2428
2429(*---------------------------------------------------------------------------
2430 Merging of finite maps (added 17 March 2009 by Thomas Tuerk)
2431 ---------------------------------------------------------------------------*)
2432
2433Theorem FUNION_EQ_FEMPTY:
2434 !h1 h2. (FUNION h1 h2 = FEMPTY) = ((h1 = FEMPTY) /\ (h2 = FEMPTY))
2435Proof
2436
2437 SIMP_TAC std_ss [GSYM fmap_EQ_THM, EXTENSION, FDOM_FEMPTY, FUNION_DEF,
2438 NOT_IN_EMPTY, IN_UNION, DISJ_IMP_THM, FORALL_AND_THM] THEN
2439 METIS_TAC[]
2440QED
2441
2442
2443
2444Theorem SUBMAP_FUNION_EQ:
2445 (!f1 f2 f3. DISJOINT (FDOM f1) (FDOM f2) ==>
2446 ((f1 SUBMAP (FUNION f2 f3) <=> f1 SUBMAP f3))) /\
2447 (!f1 f2 f3. DISJOINT (FDOM f1) (FDOM f3 DIFF (FDOM f2)) ==>
2448 ((f1 SUBMAP (FUNION f2 f3) <=> f1 SUBMAP f2)))
2449Proof
2450
2451 SIMP_TAC std_ss [SUBMAP_DEF, FUNION_DEF, IN_UNION, DISJOINT_DEF, EXTENSION,
2452 NOT_IN_EMPTY, IN_INTER, IN_DIFF] THEN
2453 METIS_TAC[]
2454QED
2455
2456
2457Theorem SUBMAP_FUNION:
2458 !f1 f2 f3. f1 SUBMAP f2 \/ (DISJOINT (FDOM f1) (FDOM f2) /\ f1 SUBMAP f3) ==>
2459 f1 SUBMAP FUNION f2 f3
2460Proof
2461
2462SIMP_TAC std_ss [SUBMAP_DEF, FUNION_DEF, IN_UNION, DISJOINT_DEF, EXTENSION,
2463 NOT_IN_EMPTY, IN_INTER] THEN
2464METIS_TAC[]
2465QED
2466
2467Theorem SUBMAP_FUNION_ID:
2468 (!f1 f2. f1 SUBMAP FUNION f1 f2) /\
2469 (!f1 f2. DISJOINT (FDOM f1) (FDOM f2) ==> f2 SUBMAP (FUNION f1 f2))
2470Proof
2471
2472METIS_TAC[SUBMAP_REFL, SUBMAP_FUNION, DISJOINT_SYM]
2473QED
2474
2475Theorem FEMPTY_SUBMAP:
2476 !h. h SUBMAP FEMPTY <=> (h = FEMPTY)
2477Proof
2478
2479 SIMP_TAC std_ss [SUBMAP_DEF, FDOM_FEMPTY, NOT_IN_EMPTY, GSYM fmap_EQ_THM,
2480 EXTENSION] THEN
2481 METIS_TAC[]
2482QED
2483
2484
2485Theorem FUNION_EQ:
2486 !f1 f2 f3. DISJOINT (FDOM f1) (FDOM f2) /\ DISJOINT (FDOM f1) (FDOM f3) ==>
2487 ((FUNION f1 f2 = FUNION f1 f3) <=> (f2 = f3))
2488Proof
2489
2490 SIMP_TAC std_ss [GSYM SUBMAP_ANTISYM, SUBMAP_DEF, FUNION_DEF, IN_UNION, DISJOINT_DEF, EXTENSION,
2491 NOT_IN_EMPTY, IN_INTER, IN_DIFF] THEN
2492 METIS_TAC[]
2493QED
2494
2495Theorem FUNION_EQ_IMPL:
2496 !f1 f2 f3.
2497 DISJOINT (FDOM f1) (FDOM f2) /\
2498 DISJOINT (FDOM f1) (FDOM f3) /\
2499 (f2 = f3)
2500 ==>
2501 ((FUNION f1 f2) = (FUNION f1 f3))
2502Proof
2503 SIMP_TAC std_ss []
2504QED
2505
2506
2507Theorem DOMSUB_FUNION:
2508 (FUNION f g) \\ k = FUNION (f \\ k) (g \\ k)
2509Proof
2510SIMP_TAC std_ss [GSYM fmap_EQ_THM, FDOM_DOMSUB, FUNION_DEF, EXTENSION,
2511 IN_UNION, IN_DELETE] THEN
2512REPEAT STRIP_TAC THENL [
2513 METIS_TAC[],
2514 ASM_SIMP_TAC std_ss [DOMSUB_FAPPLY_NEQ, FUNION_DEF],
2515 ASM_SIMP_TAC std_ss [DOMSUB_FAPPLY_NEQ, FUNION_DEF]
2516]
2517QED
2518
2519
2520Theorem FUNION_COMM:
2521 !f g. (DISJOINT (FDOM f) (FDOM g)) ==> ((FUNION f g) = (FUNION g f))
2522Proof
2523 SIMP_TAC std_ss [GSYM fmap_EQ_THM, FUNION_DEF, IN_UNION, DISJOINT_DEF,
2524 EXTENSION, NOT_IN_EMPTY, IN_INTER] THEN
2525 METIS_TAC[]
2526QED
2527
2528Theorem FUNION_ASSOC:
2529 !f g h. ((FUNION f (FUNION g h)) = (FUNION (FUNION f g) h))
2530Proof
2531 SIMP_TAC std_ss [GSYM fmap_EQ_THM, FUNION_DEF, IN_UNION, EXTENSION] THEN
2532 METIS_TAC[]
2533QED
2534
2535Theorem DRESTRICT_FUNION:
2536 !h s1 s2. FUNION (DRESTRICT h s1) (DRESTRICT h s2) =
2537 DRESTRICT h (s1 UNION s2)
2538Proof
2539 SIMP_TAC std_ss [DRESTRICT_DEF, GSYM fmap_EQ_THM, EXTENSION,
2540 FUNION_DEF, IN_INTER, IN_UNION, DISJ_IMP_THM,
2541 LEFT_AND_OVER_OR]
2542QED
2543
2544
2545Theorem DRESTRICT_EQ_FUNION:
2546 !h h1 h2. DISJOINT (FDOM h1) (FDOM h2) /\ (FUNION h1 h2 = h) ==>
2547 (h2 = DRESTRICT h (COMPL (FDOM h1)))
2548Proof
2549 SIMP_TAC std_ss [DRESTRICT_DEF, GSYM fmap_EQ_THM, EXTENSION,
2550 FUNION_DEF, IN_INTER, IN_UNION, IN_COMPL, DISJOINT_DEF,
2551 NOT_IN_EMPTY] THEN
2552 METIS_TAC[]
2553QED
2554
2555
2556Theorem IN_FDOM_FOLDR_UNION:
2557 !x hL. x IN FDOM (FOLDR FUNION FEMPTY hL) <=> ?h. MEM h hL /\ x IN FDOM h
2558Proof
2559 Induct_on `hL` THENL [
2560 SIMP_TAC list_ss [FDOM_FEMPTY, NOT_IN_EMPTY],
2561
2562 FULL_SIMP_TAC list_ss [FDOM_FUNION, IN_UNION, DISJ_IMP_THM] THEN
2563 METIS_TAC[]
2564 ]
2565QED
2566
2567
2568Theorem DRESTRICT_FUNION_DRESTRICT_COMPL:
2569 FUNION (DRESTRICT f s) (DRESTRICT f (COMPL s)) = f
2570Proof
2571
2572SIMP_TAC std_ss [GSYM fmap_EQ_THM, FUNION_DEF, DRESTRICT_DEF,
2573 EXTENSION, IN_INTER, IN_UNION, IN_COMPL] THEN
2574METIS_TAC[]
2575QED
2576
2577
2578
2579Theorem DRESTRICT_IDEMPOT[simp]:
2580 !s vs. DRESTRICT (DRESTRICT s vs) vs = DRESTRICT s vs
2581Proof
2582SRW_TAC [][]
2583QED
2584
2585Theorem SUBMAP_FUNION_ABSORPTION:
2586 !f g. f SUBMAP g <=> (FUNION f g = g)
2587Proof
2588SRW_TAC[][SUBMAP_DEF,GSYM fmap_EQ_THM,EXTENSION,FUNION_DEF,EQ_IMP_THM]
2589THEN PROVE_TAC[]
2590QED
2591
2592(*---------------------------------------------------------------------------
2593mapping an injective function over the keys of a finite map
2594 ---------------------------------------------------------------------------*)
2595
2596val MAP_KEYS_q =`
2597\f fm. if INJ f (FDOM fm) UNIV then
2598fm f_o_f (FUN_FMAP (LINV f (FDOM fm)) (IMAGE f (FDOM fm)))
2599else FUN_FMAP ARB (IMAGE f (FDOM fm))`
2600
2601Theorem MAP_KEYS_witness:
2602 let m = ^(Term MAP_KEYS_q) in
2603!f fm. (FDOM (m f fm) = IMAGE f (FDOM fm)) /\
2604 ((INJ f (FDOM fm) UNIV) ==>
2605 (!x. x IN FDOM fm ==> (((m f fm) ' (f x)) = (fm ' x))))
2606Proof
2607SIMP_TAC (srw_ss()) [LET_THM] THEN
2608REPEAT GEN_TAC THEN
2609CONJ_ASM1_TAC THEN1 (
2610 SRW_TAC[][f_o_f_DEF,
2611 GSYM SUBSET_INTER_ABSORPTION,
2612 SUBSET_DEF,FUN_FMAP_DEF] THEN
2613 IMP_RES_TAC LINV_DEF THEN
2614 SRW_TAC[][] ) THEN
2615SRW_TAC[][] THEN
2616FULL_SIMP_TAC (srw_ss()) [] THEN
2617Q.MATCH_ABBREV_TAC `(fm f_o_f z) ' (f x) = fm ' x` THEN
2618`f x IN FDOM (fm f_o_f z)` by (
2619 SRW_TAC[][] THEN PROVE_TAC[] ) THEN
2620SRW_TAC[][f_o_f_DEF] THEN
2621Q.UNABBREV_TAC `z` THEN
2622Q.MATCH_ABBREV_TAC `fm ' ((FUN_FMAP z s) ' (f x)) = fm ' x` THEN
2623`f x IN s` by (
2624 SRW_TAC[][Abbr`s`] THEN PROVE_TAC[] ) THEN
2625`FINITE s` by SRW_TAC[][Abbr`s`] THEN
2626SRW_TAC[][FUN_FMAP_DEF,Abbr`z`] THEN
2627IMP_RES_TAC LINV_DEF THEN
2628SRW_TAC[][]
2629QED
2630
2631val MAP_KEYS_exists =
2632Q.EXISTS (`$? ^(rand(rator(concl(MAP_KEYS_witness))))`,MAP_KEYS_q)
2633(BETA_RULE (PURE_REWRITE_RULE [LET_THM] MAP_KEYS_witness))
2634
2635val MAP_KEYS_def = new_specification(
2636"MAP_KEYS_def",["MAP_KEYS"],MAP_KEYS_exists)
2637
2638Theorem MAP_KEYS_FEMPTY[simp]:
2639 !f. MAP_KEYS f FEMPTY = FEMPTY
2640Proof
2641SRW_TAC[][GSYM FDOM_EQ_EMPTY,MAP_KEYS_def]
2642QED
2643
2644Theorem MAP_KEYS_FUPDATE:
2645 !f fm k v. (INJ f (k INSERT FDOM fm) UNIV) ==>
2646 (MAP_KEYS f (fm |+ (k,v)) = (MAP_KEYS f fm) |+ (f k,v))
2647Proof
2648SRW_TAC[][GSYM fmap_EQ_THM,MAP_KEYS_def] THEN
2649SRW_TAC[][MAP_KEYS_def,FAPPLY_FUPDATE_THM] THEN1 (
2650 FULL_SIMP_TAC (srw_ss()) [INJ_DEF] THEN
2651 PROVE_TAC[] ) THEN
2652FULL_SIMP_TAC (srw_ss()) [INJ_INSERT] THEN
2653SRW_TAC[][MAP_KEYS_def]
2654QED
2655
2656Theorem MAP_KEYS_using_LINV:
2657 !f fm. INJ f (FDOM fm) UNIV ==>
2658 (MAP_KEYS f fm = fm f_o_f (FUN_FMAP (LINV f (FDOM fm)) (IMAGE f (FDOM fm))))
2659Proof
2660SRW_TAC[][GSYM fmap_EQ_THM,MAP_KEYS_def] THEN
2661MP_TAC MAP_KEYS_witness THEN
2662SRW_TAC[][LET_THM] THEN
2663POP_ASSUM (Q.SPECL_THEN [`f`,`fm`] MP_TAC) THEN
2664SRW_TAC[][MAP_KEYS_def]
2665QED
2666
2667Theorem MAP_KEYS_BIJ_LINV:
2668 BIJ (f:num->num) UNIV UNIV ==> (MAP_KEYS f (MAP_KEYS (LINV f UNIV) t) = t)
2669Proof
2670 srw_tac[][fmap_EXT,MAP_KEYS_def,PULL_EXISTS,GSYM IMAGE_COMPOSE]
2671 \\ `f o LINV f UNIV = I` by
2672 (imp_res_tac BIJ_LINV_INV \\ full_simp_tac(srw_ss())[combinTheory.o_DEF,FUN_EQ_THM])
2673 \\ full_simp_tac(srw_ss())[] \\ full_simp_tac(srw_ss())[combinTheory.o_DEF,FUN_EQ_THM]
2674 \\ imp_res_tac BIJ_LINV_BIJ \\ full_simp_tac(srw_ss())[BIJ_DEF]
2675 \\ `INJ f (FDOM (MAP_KEYS (LINV f UNIV) t)) UNIV` by full_simp_tac(srw_ss())[INJ_DEF]
2676 \\ first_assum(mp_tac o MATCH_MP (ONCE_REWRITE_RULE[GSYM AND_IMP_INTRO]
2677 (MAP_KEYS_def |> SPEC_ALL |> CONJUNCT2 |> MP_CANON)))
2678 \\ `?y. x' = f y` by (full_simp_tac(srw_ss())[SURJ_DEF] \\ metis_tac []) \\ srw_tac[][]
2679 \\ pop_assum (qspec_then `y` mp_tac)
2680 \\ impl_tac THEN1
2681 (full_simp_tac(srw_ss())[MAP_KEYS_def] \\ qexists_tac `f y` \\ full_simp_tac(srw_ss())[]
2682 \\ imp_res_tac LINV_DEF \\ full_simp_tac(srw_ss())[]) \\ srw_tac[][]
2683 \\ `INJ (LINV f UNIV) (FDOM t) UNIV` by
2684 (qpat_x_assum `INJ (LINV f UNIV) UNIV UNIV` mp_tac \\ simp [INJ_DEF])
2685 \\ imp_res_tac (MAP_KEYS_def |> SPEC_ALL |> CONJUNCT2 |> MP_CANON)
2686 \\ imp_res_tac LINV_DEF \\ full_simp_tac(srw_ss())[]
2687QED
2688
2689Theorem FLOOKUP_MAP_KEYS:
2690 INJ f (FDOM m) UNIV ==>
2691 (FLOOKUP (MAP_KEYS f m) k =
2692 OPTION_BIND (some x. (k = f x) /\ x IN FDOM m) (FLOOKUP m))
2693Proof
2694 strip_tac >> DEEP_INTRO_TAC optionTheory.some_intro >>
2695 simp[FLOOKUP_DEF,MAP_KEYS_def]
2696QED
2697
2698Theorem FLOOKUP_MAP_KEYS_MAPPED:
2699 INJ f UNIV UNIV ==>
2700 (FLOOKUP (MAP_KEYS f m) (f k) = FLOOKUP m k)
2701Proof
2702 strip_tac >>
2703 `INJ f (FDOM m) UNIV` by metis_tac[INJ_SUBSET,SUBSET_UNIV,SUBSET_REFL] >>
2704 simp[FLOOKUP_MAP_KEYS] >>
2705 DEEP_INTRO_TAC optionTheory.some_intro >> srw_tac[][] >>
2706 full_simp_tac(srw_ss())[INJ_DEF] >> full_simp_tac(srw_ss())[FLOOKUP_DEF] >> metis_tac[]
2707QED
2708
2709Theorem DRESTRICT_MAP_KEYS_IMAGE:
2710 INJ f UNIV UNIV ==>
2711 (DRESTRICT (MAP_KEYS f fm) (IMAGE f s) = MAP_KEYS f (DRESTRICT fm s))
2712Proof
2713 srw_tac[][FLOOKUP_EXT,FLOOKUP_DRESTRICT,FUN_EQ_THM] >>
2714 dep_rewrite.DEP_REWRITE_TAC[FLOOKUP_MAP_KEYS,FDOM_DRESTRICT] >>
2715 conj_tac >- ( metis_tac[IN_INTER,IN_UNIV,INJ_DEF] ) >>
2716 DEEP_INTRO_TAC optionTheory.some_intro >>
2717 DEEP_INTRO_TAC optionTheory.some_intro >>
2718 srw_tac[][FLOOKUP_DRESTRICT] >> srw_tac[][] >> full_simp_tac(srw_ss())[] >>
2719 metis_tac[INJ_DEF,IN_UNIV]
2720QED
2721
2722Theorem DOMSUB_MAP_KEYS:
2723 BIJ f UNIV UNIV ==>
2724 ((MAP_KEYS f fm) \\ (f s) = MAP_KEYS f (fm \\ s))
2725Proof
2726 srw_tac[][fmap_domsub] >>
2727 dep_rewrite.DEP_REWRITE_TAC[GSYM DRESTRICT_MAP_KEYS_IMAGE] >>
2728 srw_tac[][] >- full_simp_tac(srw_ss())[BIJ_DEF] >>
2729 AP_TERM_TAC >>
2730 srw_tac[][EXTENSION] >>
2731 full_simp_tac(srw_ss())[BIJ_DEF,INJ_DEF,SURJ_DEF] >>
2732 metis_tac[]
2733QED
2734
2735(* Relate the values in two finite maps *)
2736
2737Definition fmap_rel_def:
2738 fmap_rel R f1 f2 <=>
2739 FDOM f2 = FDOM f1 /\ (!x. x IN FDOM f1 ==> R (f1 ' x) (f2 ' x))
2740End
2741
2742Theorem fmap_rel_FUPDATE_same:
2743 fmap_rel R f1 f2 /\ R v1 v2 ==> fmap_rel R (f1 |+ (k,v1)) (f2 |+ (k,v2))
2744Proof
2745SRW_TAC[][fmap_rel_def,FAPPLY_FUPDATE_THM] THEN SRW_TAC[][]
2746QED
2747
2748Theorem fmap_rel_FUPDATE_LIST_same:
2749 !R ls1 ls2 f1 f2.
2750 fmap_rel R f1 f2 /\ (MAP FST ls1 = MAP FST ls2) /\ (LIST_REL R (MAP SND ls1) (MAP SND ls2))
2751 ==> fmap_rel R (f1 |++ ls1) (f2 |++ ls2)
2752Proof
2753GEN_TAC THEN
2754Induct THEN Cases THEN SRW_TAC[][FUPDATE_LIST_THM,listTheory.LIST_REL_CONS1] THEN
2755Cases_on `ls2` THEN FULL_SIMP_TAC(srw_ss())[FUPDATE_LIST_THM] THEN
2756FIRST_X_ASSUM MATCH_MP_TAC THEN FULL_SIMP_TAC(srw_ss())[] THEN SRW_TAC[][] THEN
2757Q.MATCH_ASSUM_RENAME_TAC `R a (SND b)` THEN
2758Cases_on `b` THEN FULL_SIMP_TAC(srw_ss())[] THEN
2759SRW_TAC[][fmap_rel_FUPDATE_same]
2760QED
2761
2762Theorem fmap_rel_FEMPTY[simp]:
2763 (fmap_rel (R : 'a -> 'b -> bool) FEMPTY (f2 : 'c |-> 'b) <=> f2 = FEMPTY) /\
2764 (fmap_rel R (f1 : 'c |-> 'a) FEMPTY <=> f1 = FEMPTY)
2765Proof
2766 rw[fmap_rel_def] >> simp[FDOM_EQ_EMPTY] >> eq_tac >> rw[]
2767QED
2768
2769Theorem fmap_rel_refl[simp]:
2770 (!x. R x x) ==> fmap_rel R x x
2771Proof
2772SRW_TAC[][fmap_rel_def]
2773QED
2774
2775Theorem fmap_rel_FUNION_rels:
2776 fmap_rel R f1 f2 /\ fmap_rel R f3 f4 ==> fmap_rel R (FUNION f1 f3) (FUNION f2 f4)
2777Proof
2778SRW_TAC[][fmap_rel_def,FUNION_DEF] THEN SRW_TAC[][]
2779QED
2780
2781Theorem fmap_rel_FUPDATE_I:
2782 fmap_rel R (f1 \\ k) (f2 \\ k) /\ R v1 v2 ==>
2783 fmap_rel R (f1 |+ (k,v1)) (f2 |+ (k,v2))
2784Proof
2785 SRW_TAC[][fmap_rel_def] THENL [
2786 Q.PAT_X_ASSUM `FDOM X DELETE EE = FDOM Y DELETE FF` MP_TAC THEN
2787 SRW_TAC [][EXTENSION] THEN METIS_TAC [],
2788 SRW_TAC [][],
2789 FULL_SIMP_TAC (srw_ss()) [DOMSUB_FAPPLY_THM] THEN
2790 SRW_TAC[][FAPPLY_FUPDATE_THM]
2791 ]
2792QED
2793
2794Theorem fmap_rel_mono:
2795 (!x y. R1 x y ==> R2 x y) ==> fmap_rel R1 f1 f2 ==> fmap_rel R2 f1 f2
2796Proof
2797 SRW_TAC [][fmap_rel_def]
2798QED
2799val _ = export_mono "fmap_rel_mono"
2800
2801Theorem fmap_rel_OPTREL_FLOOKUP:
2802 fmap_rel R f1 f2 = !k. OPTREL R (FLOOKUP f1 k) (FLOOKUP f2 k)
2803Proof
2804 rw[fmap_rel_def,optionTheory.OPTREL_def,FLOOKUP_DEF,EXTENSION] >>
2805 PROVE_TAC[]
2806QED
2807
2808Theorem fmap_rel_FLOOKUP_imp:
2809 fmap_rel R f1 f2 ==>
2810 (!k. FLOOKUP f1 k = NONE ==> FLOOKUP f2 k = NONE) /\
2811 (!k v1. FLOOKUP f1 k = SOME v1 ==> ?v2. FLOOKUP f2 k = SOME v2 /\ R v1 v2)
2812Proof
2813 rw[fmap_rel_OPTREL_FLOOKUP,optionTheory.OPTREL_def] >>
2814 first_x_assum(qspec_then`k`mp_tac) >> rw[]
2815QED
2816
2817Theorem fmap_rel_FUPDATE_EQN:
2818 fmap_rel R (f1 \\ k) (f2 \\ k) /\ R v1 v2 <=>
2819 fmap_rel R (f1 |+ (k,v1)) (f2 |+ (k,v2))
2820Proof
2821 gvs[fmap_rel_OPTREL_FLOOKUP, FLOOKUP_UPDATE, DOMSUB_FLOOKUP_THM] >>
2822 reverse (eq_tac >> rw[])
2823 >- (pop_assum (qspec_then `k` mp_tac) >> simp[]) >>
2824 first_x_assum (qspec_then `k'` mp_tac) >> simp[] >>
2825 every_case_tac >> gvs[]
2826QED
2827
2828Theorem fmap_rel_ind[rule_induction]:
2829 !R FR.
2830 FR FEMPTY FEMPTY /\
2831 (!k v1 v2 f1 f2.
2832 R v1 v2 /\ FR (f1 \\ k) (f2 \\ k) ==> FR (f1 |+ (k,v1)) (f2 |+ (k,v2)))
2833 ==> !f1 f2. fmap_rel R f1 f2 ==> FR f1 f2
2834Proof
2835 rpt gen_tac >> strip_tac >>
2836 ho_match_mp_tac fmap_INDUCT >> rw[] >>
2837 `x IN FDOM f2` by gvs[fmap_rel_def] >>
2838 imp_res_tac FM_PULL_APART >> gvs[] >>
2839 last_x_assum irule >> gvs[DOMSUB_NOT_IN_DOM] >>
2840 gvs[GSYM fmap_rel_FUPDATE_EQN] >>
2841 first_x_assum irule >> gvs[DOMSUB_NOT_IN_DOM]
2842QED
2843
2844
2845(*---------------------------------------------------------------------------
2846 Some helpers for fupdate_NORMALISE_CONV
2847 ---------------------------------------------------------------------------*)
2848
2849Definition fmap_EQ_UPTO_def:
2850 fmap_EQ_UPTO f1 f2 vs <=>
2851 (FDOM f1 INTER (COMPL vs) = FDOM f2 INTER (COMPL vs)) /\
2852 (!x. x IN FDOM f1 INTER (COMPL vs) ==> (f1 ' x = f2 ' x))
2853End
2854
2855Theorem fmap_EQ_UPTO___EMPTY[simp]:
2856 !f1 f2. (fmap_EQ_UPTO f1 f2 EMPTY) = (f1 = f2)
2857Proof
2858 SIMP_TAC std_ss [fmap_EQ_UPTO_def, COMPL_EMPTY, INTER_UNIV, fmap_EQ_THM]
2859QED
2860
2861Theorem fmap_EQ_UPTO___EQ[simp]:
2862 !vs f. (fmap_EQ_UPTO f f vs)
2863Proof
2864 SIMP_TAC std_ss [fmap_EQ_UPTO_def]
2865QED
2866
2867Theorem fmap_EQ_UPTO___FUPDATE_BOTH:
2868 !f1 f2 ks k v.
2869 (fmap_EQ_UPTO f1 f2 ks) ==>
2870 (fmap_EQ_UPTO (f1 |+ (k,v)) (f2 |+ (k,v)) (ks DELETE k))
2871Proof
2872SIMP_TAC std_ss [fmap_EQ_UPTO_def, EXTENSION, IN_INTER,
2873 FDOM_FUPDATE, IN_COMPL, IN_INSERT, IN_DELETE] THEN
2874REPEAT GEN_TAC THEN STRIP_TAC THEN
2875CONJ_TAC THEN GEN_TAC THENL [
2876 Cases_on `x = k` THEN ASM_REWRITE_TAC[],
2877 Cases_on `x = k` THEN ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM]
2878]
2879QED
2880
2881
2882Theorem fmap_EQ_UPTO___FUPDATE_BOTH___NO_DELETE:
2883 !f1 f2 ks k v.
2884 (fmap_EQ_UPTO f1 f2 ks) ==>
2885 (fmap_EQ_UPTO (f1 |+ (k,v)) (f2 |+ (k,v)) ks)
2886Proof
2887
2888SIMP_TAC std_ss [fmap_EQ_UPTO_def, EXTENSION, IN_INTER,
2889 FDOM_FUPDATE, IN_COMPL, IN_INSERT] THEN
2890REPEAT GEN_TAC THEN STRIP_TAC THEN
2891CONJ_TAC THEN GEN_TAC THENL [
2892 Cases_on `x = k` THEN ASM_REWRITE_TAC[],
2893 Cases_on `x = k` THEN ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM]
2894]
2895QED
2896
2897
2898Theorem fmap_EQ_UPTO___FUPDATE_SING:
2899 !f1 f2 ks k v.
2900 (fmap_EQ_UPTO f1 f2 ks) ==>
2901 (fmap_EQ_UPTO (f1 |+ (k,v)) f2 (k INSERT ks))
2902Proof
2903
2904SIMP_TAC std_ss [fmap_EQ_UPTO_def, EXTENSION, IN_INTER,
2905 FDOM_FUPDATE, IN_COMPL, IN_INSERT, IN_DELETE] THEN
2906REPEAT GEN_TAC THEN STRIP_TAC THEN
2907CONJ_TAC THEN GEN_TAC THENL [
2908 Cases_on `x = k` THEN ASM_REWRITE_TAC[],
2909 Cases_on `x = k` THEN ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM]
2910]
2911QED
2912
2913(*---------------------------------------------------------------------------*)
2914(* From Ramana Kumar *)
2915(*---------------------------------------------------------------------------*)
2916
2917Definition fmap_size_def:
2918 fmap_size kz vz fm = SIGMA (\k. kz k + vz (fm ' k)) (FDOM fm)
2919End
2920
2921(*---------------------------------------------------------------------------*)
2922(* Various lemmas from the CakeML project https://cakeml.org *)
2923(*---------------------------------------------------------------------------*)
2924
2925local
2926 open optionTheory rich_listTheory listTheory boolSimps sortingTheory
2927in
2928
2929Theorem o_f_FUNION:
2930 f o_f (FUNION f1 f2) = FUNION (f o_f f1) (f o_f f2)
2931Proof
2932 simp[GSYM fmap_EQ_THM,FUNION_DEF] >>
2933 rw[o_f_FAPPLY]
2934QED
2935
2936Theorem FDOM_FOLDR_DOMSUB:
2937 !ls fm. FDOM (FOLDR (\k m. m \\ k) fm ls) = FDOM fm DIFF set ls
2938Proof
2939 Induct >> simp[] >>
2940 ONCE_REWRITE_TAC[EXTENSION] >>
2941 simp[] >> metis_tac[]
2942QED
2943
2944Theorem FEVERY_SUBMAP:
2945 FEVERY P fm /\ fm0 SUBMAP fm ==> FEVERY P fm0
2946Proof
2947 SRW_TAC[][FEVERY_DEF,SUBMAP_DEF]
2948QED
2949
2950Theorem FEVERY_ALL_FLOOKUP:
2951 !P f. FEVERY P f <=> !k v. (FLOOKUP f k = SOME v) ==> P (k,v)
2952Proof
2953 SRW_TAC[][FEVERY_DEF,FLOOKUP_DEF]
2954QED
2955
2956Theorem FUPDATE_LIST_CANCEL:
2957 !ls1 fm ls2.
2958 (!k. MEM k (MAP FST ls1) ==> MEM k (MAP FST ls2))
2959 ==> (fm |++ ls1 |++ ls2 = fm |++ ls2)
2960Proof
2961 Induct THEN SRW_TAC[][FUPDATE_LIST_THM] THEN
2962 Cases_on`h` THEN
2963 MATCH_MP_TAC FUPDATE_FUPDATE_LIST_MEM THEN
2964 FULL_SIMP_TAC(srw_ss())[]
2965QED
2966
2967Theorem FUPDATE_EQ_FUNION:
2968 !fm kv. fm |+ kv = FUNION (FEMPTY |+ kv) fm
2969Proof
2970 gen_tac >> Cases >>
2971 simp[GSYM fmap_EQ_THM,FDOM_FUPDATE,FAPPLY_FUPDATE_THM,FUNION_DEF] >>
2972 simp[EXTENSION]
2973QED
2974
2975Theorem FUPDATE_LIST_APPEND_COMMUTES:
2976 !l1 l2 fm. DISJOINT (set (MAP FST l1)) (set (MAP FST l2)) ==>
2977 (fm |++ l1 |++ l2 = fm |++ l2 |++ l1)
2978Proof
2979 Induct >- rw[FUPDATE_LIST_THM] >>
2980 Cases >> rw[FUPDATE_LIST_THM] >>
2981 metis_tac[FUPDATE_FUPDATE_LIST_COMMUTES]
2982QED
2983
2984Theorem FUPDATE_LIST_ALL_DISTINCT_PERM:
2985 !ls ls' fm.
2986 ALL_DISTINCT (MAP FST ls) /\ PERM ls ls' ==> (fm |++ ls = fm |++ ls')
2987Proof
2988 Induct >> rw[] >>
2989 fs[sortingTheory.PERM_CONS_EQ_APPEND] >>
2990 rw[FUPDATE_LIST_THM] >>
2991 PairCases_on`h` >> fs[] >>
2992 imp_res_tac FUPDATE_FUPDATE_LIST_COMMUTES >>
2993 match_mp_tac EQ_TRANS >>
2994 qexists_tac `(fm |++ (M ++ N)) |+ (h0,h1)` >>
2995 conj_tac
2996 >- metis_tac[sortingTheory.ALL_DISTINCT_PERM,sortingTheory.PERM_MAP] >>
2997 rw[FUPDATE_LIST_APPEND] >>
2998 `h0 NOTIN set (MAP FST N)`
2999 by metis_tac[sortingTheory.PERM_MEM_EQ,MEM_MAP,MEM_APPEND] >>
3000 imp_res_tac FUPDATE_FUPDATE_LIST_COMMUTES >>
3001 rw[FUPDATE_LIST_THM]
3002QED
3003
3004Theorem IMAGE_FRANGE:
3005 !f fm. IMAGE f (FRANGE fm) = FRANGE (f o_f fm)
3006Proof
3007 SRW_TAC[][EXTENSION] THEN
3008 EQ_TAC THEN1 PROVE_TAC[o_f_FRANGE] THEN
3009 SRW_TAC[][FRANGE_DEF] THEN
3010 SRW_TAC[][o_f_FAPPLY] THEN
3011 PROVE_TAC[]
3012QED
3013
3014Theorem SUBMAP_mono_FUPDATE:
3015 !f g x y. f \\ x SUBMAP g \\ x ==> f |+ (x,y) SUBMAP g |+ (x,y)
3016Proof
3017 SRW_TAC[][SUBMAP_FUPDATE]
3018QED
3019
3020Theorem SUBMAP_DOMSUB_gen:
3021 !f g k. f \\ k SUBMAP g <=> f \\ k SUBMAP g \\ k
3022Proof
3023 SRW_TAC[][SUBMAP_DEF,EQ_IMP_THM,DOMSUB_FAPPLY_THM]
3024QED
3025
3026Theorem DOMSUB_SUBMAP:
3027 !f g x. f SUBMAP g /\ x NOTIN FDOM f ==> f SUBMAP g \\ x
3028Proof
3029 SRW_TAC[][SUBMAP_DEF,DOMSUB_FAPPLY_THM] THEN
3030 SRW_TAC[][] THEN METIS_TAC[]
3031QED
3032
3033Theorem DRESTRICT_DOMSUB:
3034 !f s k. DRESTRICT f s \\ k = DRESTRICT f (s DELETE k)
3035Proof
3036 SRW_TAC[][GSYM fmap_EQ_THM,FDOM_DRESTRICT] THEN1 (
3037 SRW_TAC[][EXTENSION] THEN METIS_TAC[] ) THEN
3038 SRW_TAC[][DOMSUB_FAPPLY_THM] THEN
3039 SRW_TAC[][DRESTRICT_DEF]
3040QED
3041
3042Theorem DRESTRICT_SUBSET_SUBMAP_gen:
3043 !f1 f2 s t.
3044 DRESTRICT f1 s SUBMAP DRESTRICT f2 s /\ t SUBSET s ==>
3045 DRESTRICT f1 t SUBMAP DRESTRICT f2 t
3046Proof
3047 rw[SUBMAP_DEF,DRESTRICT_DEF,SUBSET_DEF]
3048QED
3049
3050
3051Theorem DRESTRICT_FUNION_SAME:
3052 !fm s. FUNION (DRESTRICT fm s) fm = fm
3053Proof
3054 SRW_TAC[][GSYM SUBMAP_FUNION_ABSORPTION]
3055QED
3056
3057Theorem DRESTRICT_EQ_DRESTRICT_SAME:
3058 (DRESTRICT f1 s = DRESTRICT f2 s) <=>
3059 (s INTER FDOM f1 = s INTER FDOM f2) /\
3060 (!x. x IN FDOM f1 /\ x IN s ==> (f1 ' x = f2 ' x))
3061Proof
3062 SRW_TAC[][DRESTRICT_EQ_DRESTRICT,SUBMAP_DEF,DRESTRICT_DEF,EXTENSION] THEN
3063 PROVE_TAC[]
3064QED
3065
3066Theorem FOLDL2_FUPDATE_LIST:
3067 !f1 f2 bs cs a. (LENGTH bs = LENGTH cs) ==>
3068 (FOLDL2 (\fm b c. fm |+ (f1 b c, f2 b c)) a bs cs =
3069 a |++ ZIP (MAP2 f1 bs cs, MAP2 f2 bs cs))
3070Proof
3071SRW_TAC[][FUPDATE_LIST,FOLDL2_FOLDL,MAP2_MAP,ZIP_MAP,MAP_ZIP,
3072 rich_listTheory.FOLDL_MAP,listTheory.LENGTH_MAP2,
3073 LENGTH_ZIP,pairTheory.LAMBDA_PROD]
3074QED
3075
3076Theorem FOLDL2_FUPDATE_LIST_paired:
3077 !f1 f2 bs cs a. (LENGTH bs = LENGTH cs) ==>
3078 (FOLDL2 (\fm b (c,d). fm |+ (f1 b c d, f2 b c d)) a bs cs =
3079 a |++ ZIP (MAP2 (\b. UNCURRY (f1 b)) bs cs, MAP2 (\b. UNCURRY (f2 b)) bs cs))
3080Proof
3081rw[FOLDL2_FOLDL,MAP2_MAP,ZIP_MAP,MAP_ZIP,LENGTH_ZIP,
3082 pairTheory.UNCURRY,pairTheory.LAMBDA_PROD,FUPDATE_LIST,
3083 rich_listTheory.FOLDL_MAP]
3084QED
3085
3086Theorem DRESTRICT_FUNION_SUBSET:
3087 s2 SUBSET s1 ==>
3088 ?h. (FUNION (DRESTRICT f s1) g = FUNION (DRESTRICT f s2) h)
3089Proof
3090 strip_tac >>
3091 qexists_tac `FUNION (DRESTRICT f s1) g` >>
3092 match_mp_tac EQ_SYM >>
3093 REWRITE_TAC[GSYM SUBMAP_FUNION_ABSORPTION] >>
3094 rw[SUBMAP_DEF,DRESTRICT_DEF,FUNION_DEF] >>
3095 fs[SUBSET_DEF]
3096QED
3097
3098Theorem FUPDATE_LIST_APPLY_NOT_MEM_matchable:
3099 !kvl f k v. ~MEM k (MAP FST kvl) /\ (v = f ' k) ==> ((f |++ kvl) ' k = v)
3100Proof
3101PROVE_TAC[FUPDATE_LIST_APPLY_NOT_MEM]
3102QED
3103
3104Theorem FUPDATE_LIST_APPLY_HO_THM:
3105 !P f kvl k.
3106(?n. n < LENGTH kvl /\ (k = EL n (MAP FST kvl)) /\ P (EL n (MAP SND kvl)) /\
3107 (!m. n < m /\ m < LENGTH kvl ==> EL m (MAP FST kvl) <> k)) \/
3108(~MEM k (MAP FST kvl) /\ P (f ' k))
3109==> (P ((f |++ kvl) ' k))
3110Proof
3111metis_tac[FUPDATE_LIST_APPLY_MEM,FUPDATE_LIST_APPLY_NOT_MEM]
3112QED
3113
3114Theorem FUPDATE_SAME_APPLY:
3115 (x = FST kv) \/ (fm1 ' x = fm2 ' x) ==> ((fm1 |+ kv) ' x = (fm2 |+ kv) ' x)
3116Proof
3117Cases_on `kv` >> rw[FAPPLY_FUPDATE_THM]
3118QED
3119
3120Theorem FUPDATE_SAME_LIST_APPLY:
3121 !kvl fm1 fm2 x. MEM x (MAP FST kvl) ==> ((fm1 |++ kvl) ' x = (fm2 |++ kvl) ' x)
3122Proof
3123ho_match_mp_tac SNOC_INDUCT >>
3124conj_tac >- rw[] >>
3125rw[FUPDATE_LIST,FOLDL_SNOC] >>
3126match_mp_tac FUPDATE_SAME_APPLY >>
3127qmatch_rename_tac `(y = FST p) \/ _` >>
3128Cases_on `y = FST p` >> rw[] >>
3129first_x_assum match_mp_tac >>
3130fs[MEM_MAP] >>
3131PROVE_TAC[]
3132QED
3133
3134Theorem FUPDATE_LIST_ALL_DISTINCT_APPLY_MEM:
3135 !P ls k v fm. ALL_DISTINCT (MAP FST ls) /\
3136 MEM (k,v) ls /\
3137 P v ==>
3138 P ((fm |++ ls) ' k)
3139Proof
3140rw[] >>
3141ho_match_mp_tac FUPDATE_LIST_APPLY_HO_THM >>
3142disj1_tac >>
3143fs[EL_ALL_DISTINCT_EL_EQ,MEM_EL] >>
3144qpat_x_assum `(k,v) = X` (assume_tac o SYM) >>
3145qexists_tac `n` >> rw[EL_MAP] >>
3146first_x_assum (qspecl_then [`n`,`m`] mp_tac) >>
3147rw[EL_MAP] >> spose_not_then strip_assume_tac >>
3148rw[] >> fs[]
3149QED
3150
3151Theorem FUPDATE_LIST_ALL_DISTINCT_REVERSE:
3152 !ls. ALL_DISTINCT (MAP FST ls) ==> !fm. fm |++ (REVERSE ls) = fm |++ ls
3153Proof
3154 Induct >- rw[] >>
3155 qx_gen_tac `p` >> PairCases_on `p` >>
3156 rw[FUPDATE_LIST_APPEND,FUPDATE_LIST_THM] >>
3157 fs[] >>
3158 rw[FUPDATE_FUPDATE_LIST_COMMUTES]
3159QED
3160
3161(* FRANGE subset stuff *)
3162
3163Theorem IN_FRANGE:
3164 !f v. v IN FRANGE f <=> ?k. k IN FDOM f /\ (f ' k = v)
3165Proof
3166SRW_TAC[][FRANGE_DEF]
3167QED
3168
3169Theorem IN_FRANGE_FLOOKUP:
3170 !f v. v IN FRANGE f <=> ?k. FLOOKUP f k = SOME v
3171Proof
3172rw[IN_FRANGE,FLOOKUP_DEF]
3173QED
3174
3175Theorem FRANGE_FUPDATE_LIST_SUBSET:
3176 !ls fm. FRANGE (fm |++ ls) SUBSET FRANGE fm UNION (set (MAP SND ls))
3177Proof
3178Induct >- rw[FUPDATE_LIST_THM] >>
3179qx_gen_tac `p` >> qx_gen_tac `fm` >>
3180pop_assum (qspec_then `fm |+ p` mp_tac) >>
3181srw_tac[DNF_ss][SUBSET_DEF] >>
3182first_x_assum (qspec_then `x` mp_tac) >> fs[FUPDATE_LIST_THM] >>
3183rw[] >> fs[] >>
3184PairCases_on `p` >>
3185fsrw_tac[DNF_ss][FRANGE_FLOOKUP,FLOOKUP_UPDATE] >>
3186pop_assum mp_tac >> rw[] >>
3187PROVE_TAC[]
3188QED
3189
3190Theorem IN_FRANGE_FUPDATE_LIST_suff:
3191 (!v. v IN FRANGE fm ==> P v) /\ (!v. MEM v (MAP SND ls) ==> P v) ==>
3192 !v. v IN FRANGE (fm |++ ls) ==> P v
3193Proof
3194rw[] >>
3195imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_FUPDATE_LIST_SUBSET) >>
3196PROVE_TAC[]
3197QED
3198
3199Theorem FRANGE_FUNION_SUBSET:
3200 FRANGE (FUNION f1 f2) SUBSET FRANGE f1 UNION FRANGE f2
3201Proof
3202srw_tac[DNF_ss][FRANGE_DEF,SUBSET_DEF,FUNION_DEF] >>
3203PROVE_TAC[]
3204QED
3205
3206Theorem IN_FRANGE_FUNION_suff:
3207 (!v. v IN FRANGE f1 ==> P v) /\ (!v. v IN FRANGE f2 ==> P v) ==>
3208 (!v. v IN FRANGE (FUNION f1 f2) ==> P v)
3209Proof
3210rw[] >>
3211imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_FUNION_SUBSET) >>
3212PROVE_TAC[]
3213QED
3214
3215Theorem FRANGE_DOMSUB_SUBSET:
3216 FRANGE (fm \\ k) SUBSET FRANGE fm
3217Proof
3218srw_tac[DNF_ss][FRANGE_DEF,SUBSET_DEF,DOMSUB_FAPPLY_THM] >>
3219PROVE_TAC[]
3220QED
3221
3222Theorem IN_FRANGE_DOMSUB_suff:
3223 (!v. v IN FRANGE fm ==> P v) ==> (!v. v IN FRANGE (fm \\ k) ==> P v)
3224Proof
3225rw[] >>
3226imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_DOMSUB_SUBSET) >>
3227PROVE_TAC[]
3228QED
3229
3230Theorem FRANGE_DRESTRICT_SUBSET:
3231 FRANGE (DRESTRICT fm s) SUBSET FRANGE fm
3232Proof
3233 srw_tac[DNF_ss][FRANGE_DEF,SUBSET_DEF,DRESTRICT_DEF] >> PROVE_TAC[]
3234QED
3235
3236Theorem IN_FRANGE_DRESTRICT_suff:
3237 (!v. v IN FRANGE fm ==> P v) ==> (!v. v IN FRANGE (DRESTRICT fm s) ==> P v)
3238Proof
3239rw[] >>
3240imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_DRESTRICT_SUBSET) >>
3241PROVE_TAC[]
3242QED
3243
3244Theorem FRANGE_FUPDATE_SUBSET:
3245 FRANGE (fm |+ kv) SUBSET FRANGE fm UNION {SND kv}
3246Proof
3247Cases_on `kv` >>
3248rw[FRANGE_DEF,SUBSET_DEF,DOMSUB_FAPPLY_THM] >>
3249rw[] >> PROVE_TAC[]
3250QED
3251
3252Theorem IN_FRANGE_FUPDATE_suff:
3253 (!v. v IN FRANGE fm ==> P v) /\ (P (SND kv))
3254==> (!v. v IN FRANGE (fm |+ kv) ==> P v)
3255Proof
3256rw[] >>
3257imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_FUPDATE_SUBSET) >>
3258fs[]
3259QED
3260
3261Theorem IN_FRANGE_o_f_suff:
3262 (!v. v IN FRANGE fm ==> P (f v)) ==> !v. v IN FRANGE (f o_f fm) ==> P v
3263Proof
3264 rw[IN_FRANGE] >> rw[] >> first_x_assum match_mp_tac >> PROVE_TAC[]
3265QED
3266
3267(* DRESTRICT stuff *)
3268
3269Theorem DRESTRICT_SUBMAP_gen:
3270 f SUBMAP g ==> DRESTRICT f P SUBMAP g
3271Proof
3272SRW_TAC[][SUBMAP_DEF,DRESTRICT_DEF]
3273QED
3274
3275Theorem DRESTRICT_SUBSET_SUBMAP:
3276 s1 SUBSET s2 ==> DRESTRICT f s1 SUBMAP DRESTRICT f s2
3277Proof
3278SRW_TAC[][SUBMAP_DEF,SUBSET_DEF,DRESTRICT_DEF]
3279QED
3280
3281Theorem DRESTRICTED_FUNION:
3282 !f1 f2 s. DRESTRICT (FUNION f1 f2) s = FUNION (DRESTRICT f1 s) (DRESTRICT f2 (s DIFF FDOM f1))
3283Proof
3284rw[GSYM fmap_EQ_THM,DRESTRICT_DEF,FUNION_DEF] >> rw[] >>
3285rw[EXTENSION] >> PROVE_TAC[]
3286QED
3287
3288Theorem DRESTRICT_FDOM:
3289 !f. DRESTRICT f (FDOM f) = f
3290Proof
3291SRW_TAC[][GSYM fmap_EQ_THM,DRESTRICT_DEF]
3292QED
3293
3294Theorem DRESTRICT_SUBSET:
3295 !f1 f2 s t.
3296 (DRESTRICT f1 s = DRESTRICT f2 s) /\ t SUBSET s ==>
3297 (DRESTRICT f1 t = DRESTRICT f2 t)
3298Proof
3299 rw[DRESTRICT_EQ_DRESTRICT]
3300 >- metis_tac[DRESTRICT_SUBSET_SUBMAP,SUBMAP_TRANS]
3301 >- metis_tac[DRESTRICT_SUBSET_SUBMAP,SUBMAP_TRANS] >>
3302 fsrw_tac[DNF_ss][SUBSET_DEF,EXTENSION] >>
3303 metis_tac[]
3304QED
3305
3306Theorem f_o_f_FUPDATE_compose:
3307 !f1 f2 k x v. x NOTIN FDOM f1 /\ x NOTIN FRANGE f2 ==>
3308 ((f1 |+ (x,v)) f_o_f (f2 |+ (k,x)) = (f1 f_o_f f2) |+ (k,v))
3309Proof
3310 rw[GSYM fmap_EQ_THM,f_o_f_DEF,FAPPLY_FUPDATE_THM] >>
3311 simp[] >> rw[] >> fs[] >> rw[EXTENSION] >>
3312 fs[IN_FRANGE] >> rw[]
3313 >- PROVE_TAC[]
3314 >- PROVE_TAC[] >>
3315 qmatch_assum_rename_tac`y <> k` >>
3316 `y IN FDOM (f1 f_o_f f2)` by rw[f_o_f_DEF] >>
3317 rw[f_o_f_DEF]
3318QED
3319
3320Theorem fmap_rel_trans:
3321 (!x y z. R x y /\ R y z ==> R x z) ==>
3322 !x y z. fmap_rel R x y /\ fmap_rel R y z ==>
3323 fmap_rel R x z
3324Proof
3325 SRW_TAC[][fmap_rel_def] THEN METIS_TAC[]
3326QED
3327
3328Theorem fmap_rel_sym:
3329 (!x y. R x y ==> R y x) ==>
3330 !x y. fmap_rel R x y ==> fmap_rel R y x
3331Proof
3332 SRW_TAC[][fmap_rel_def]
3333QED
3334
3335Theorem fupdate_list_map:
3336 !l f x y.
3337 x IN FDOM (FEMPTY |++ l)
3338 ==>
3339 ((FEMPTY |++ MAP (\(a,b). (a, f b)) l) ' x = f ((FEMPTY |++ l) ' x))
3340Proof
3341 rpt gen_tac >>
3342 Q.ISPECL_THEN[`FST`,`f o SND`,`l`,`FEMPTY:'a|->'c`]mp_tac(GSYM FOLDL_FUPDATE_LIST) >>
3343 simp[LAMBDA_PROD] >>
3344 disch_then kall_tac >>
3345 qid_spec_tac`l` >>
3346 ho_match_mp_tac SNOC_INDUCT >>
3347 simp[FUPDATE_LIST_THM] >>
3348 simp[FOLDL_SNOC,FORALL_PROD,FAPPLY_FUPDATE_THM,FDOM_FUPDATE_LIST,MAP_SNOC,FUPDATE_LIST_SNOC] >>
3349 rw[] >> rw[]
3350QED
3351
3352Theorem fdom_fupdate_list2:
3353 !kvl fm. FDOM (fm |++ kvl) = (FDOM fm DIFF set (MAP FST kvl)) UNION set (MAP FST kvl)
3354Proof
3355rw [FDOM_FUPDATE_LIST, EXTENSION] >>
3356metis_tac []
3357QED
3358
3359Theorem flookup_thm:
3360 !f x v. ((FLOOKUP f x = NONE) = (x NOTIN FDOM f)) /\
3361 ((FLOOKUP f x = SOME v) = (x IN FDOM f /\ (f ' x = v)))
3362Proof
3363rw [FLOOKUP_DEF]
3364QED
3365
3366Theorem FINITE_MAP_LOOKUP_RANGE:
3367 (!f x y. FLOOKUP f x = SOME y ==> y IN FRANGE f) /\
3368 (!f x. x IN FDOM f ==> FAPPLY f x IN FRANGE f)
3369Proof
3370 metis_tac [FRANGE_FLOOKUP, flookup_thm]
3371QED
3372
3373Theorem FUPDATE_EQ_FUPDATE_LIST:
3374 !fm kv. fm |+ kv = fm |++ [kv]
3375Proof
3376 rw[FUPDATE_LIST_THM]
3377QED
3378
3379val fmap_inverse_def = Define `
3380fmap_inverse m1 m2 =
3381 !k. k IN FDOM m1 ==> ?v. (FLOOKUP m1 k = SOME v) /\ (FLOOKUP m2 v = SOME k)`;
3382
3383Theorem fupdate_list_foldr:
3384 !m l. FOLDR (\(k,v) env. env |+ (k,v)) m l = m |++ REVERSE l
3385Proof
3386 Induct_on `l` >>
3387 rw [FUPDATE_LIST] >>
3388 PairCases_on `h` >>
3389 rw [FOLDL_APPEND]
3390QED
3391
3392Theorem fupdate_list_foldl:
3393 !m l. FOLDL (\env (k,v). env |+ (k,v)) m l = m |++ l
3394Proof
3395 Induct_on `l` >>
3396 rw [FUPDATE_LIST] >>
3397 PairCases_on `h` >>
3398 rw []
3399QED
3400
3401Theorem fmap_to_list:
3402 !m. ?l. ALL_DISTINCT (MAP FST l) /\ (m = FEMPTY |++ l)
3403Proof
3404ho_match_mp_tac fmap_INDUCT >>
3405rw [FUPDATE_LIST_THM] >|
3406[qexists_tac `[]` >>
3407 rw [FUPDATE_LIST_THM],
3408 qexists_tac `(x,y)::l` >>
3409 rw [FUPDATE_LIST_THM] >>
3410 fs [FDOM_FUPDATE_LIST] >>
3411 rw [FUPDATE_FUPDATE_LIST_COMMUTES] >>
3412 fs [LIST_TO_SET_MAP] >>
3413 metis_tac [FST]]
3414QED
3415
3416Theorem disjoint_drestrict:
3417 !s m. DISJOINT s (FDOM m) ==> (DRESTRICT m (COMPL s) = m)
3418Proof
3419 rw [FLOOKUP_EXT, FLOOKUP_DRESTRICT, FUN_EQ_THM] >>
3420 Cases_on `k NOTIN s` >>
3421 rw [] >>
3422 fs [DISJOINT_DEF, EXTENSION, FLOOKUP_DEF] >>
3423 metis_tac []
3424QED
3425
3426Theorem drestrict_iter_list:
3427 !m l. FOLDR (\k m. m \\ k) m l = DRESTRICT m (COMPL (set l))
3428Proof
3429 Induct_on `l` >>
3430 rw [DRESTRICT_UNIV, DRESTRICT_DOMSUB] >>
3431 match_mp_tac (PROVE [] ``(y = y') ==> (f x y = f x y')``) >>
3432 rw [EXTENSION] >>
3433 metis_tac []
3434QED
3435
3436Theorem fevery_funion:
3437 !P m1 m2. FEVERY P m1 /\ FEVERY P m2 ==> FEVERY P (FUNION m1 m2)
3438Proof
3439 rw [FEVERY_ALL_FLOOKUP, FLOOKUP_FUNION] >>
3440 BasicProvers.EVERY_CASE_TAC >>
3441 fs []
3442QED
3443
3444Theorem DISJOINT_FEVERY_FUNION:
3445 DISJOINT (FDOM m1) (FDOM m2) ==>
3446 (FEVERY P (FUNION m1 m2) <=> FEVERY P m1 /\ FEVERY P m2)
3447Proof
3448 rw[EQ_IMP_THM,fevery_funion]
3449 \\ fs[FEVERY_ALL_FLOOKUP,FLOOKUP_FUNION,IN_DISJOINT] \\ rw[]
3450 \\ first_x_assum match_mp_tac
3451 \\ CASE_TAC
3452 \\ fs[FLOOKUP_DEF]
3453 \\ metis_tac[]
3454QED
3455
3456end
3457(* end CakeML lemmas *)
3458
3459(* ----------------------------------------------------------------------
3460 FDIFF
3461
3462 Removes a whole bunch of keys at once
3463 ---------------------------------------------------------------------- *)
3464
3465Definition FDIFF_def: FDIFF f1 s = DRESTRICT f1 (COMPL s)
3466End
3467
3468Theorem FDOM_FDIFF[simp]:
3469 x IN FDOM (FDIFF refs f2) <=> x IN FDOM refs /\ x NOTIN f2
3470Proof full_simp_tac(srw_ss())[FDIFF_def,DRESTRICT_DEF]
3471QED
3472
3473Theorem FDOM_F_COMP_G_SUBSET_FDOM_G:
3474 !f g. FDOM (f f_o_f g) SUBSET (FDOM g)
3475Proof
3476 fs[f_o_f_DEF]
3477QED
3478
3479Theorem FRANGE_SUBSET_FDOM_COMP_FDOM_EQUALITY:
3480 !f g. FRANGE g SUBSET FDOM f ==> FDOM (f f_o_f g) = FDOM g
3481Proof
3482 rpt strip_tac
3483 \\ rw [SET_EQ_SUBSET]
3484 >- rw[FDOM_F_COMP_G_SUBSET_FDOM_G]
3485 >- ( fs[f_o_f_DEF, SUBSET_DEF]
3486 \\ metis_tac [FINITE_MAP_LOOKUP_RANGE]
3487 )
3488QED
3489
3490Theorem NUM_NOT_IN_FDOM =
3491 MATCH_MP IN_INFINITE_NOT_FINITE (CONJ INFINITE_NUM_UNIV
3492 (Q.ISPEC `f:num|->'a` FDOM_FINITE))
3493 |> SIMP_RULE std_ss [IN_UNIV]
3494
3495Theorem EXISTS_NOT_IN_FDOM_LEMMA[local]:
3496 ?x. ~(x IN FDOM (refs:num|->'a))
3497Proof
3498 METIS_TAC [NUM_NOT_IN_FDOM]
3499QED
3500
3501Theorem LEAST_NOTIN_FDOM:
3502 (LEAST ptr. ptr NOTIN FDOM (refs:num|->'a)) NOTIN FDOM refs
3503Proof
3504 ASSUME_TAC
3505 (EXISTS_NOT_IN_FDOM_LEMMA |> SIMP_RULE std_ss [WhileTheory.LEAST_EXISTS])>>
3506 fs[]
3507QED
3508
3509Theorem FLOOKUP_FDIFF:
3510 FLOOKUP (FDIFF fm s) k = if k IN s then NONE else FLOOKUP fm k
3511Proof
3512 rw[FDIFF_def, FLOOKUP_DRESTRICT] >> gvs[]
3513QED
3514
3515Theorem FDIFF_FDIFF:
3516 !fm s1 s2. FDIFF (FDIFF fm s1) s2 = FDIFF fm (s1 UNION s2)
3517Proof
3518 rw[FDIFF_def, DRESTRICT_DRESTRICT, fmap_eq_flookup, FLOOKUP_DRESTRICT]
3519QED
3520
3521Theorem FDIFF_FUNION:
3522 !fm1 fm2 s. FDIFF (FUNION fm1 fm2) s = FUNION (FDIFF fm1 s) (FDIFF fm2 s)
3523Proof
3524 rw[FDIFF_def, DRESTRICTED_FUNION] >>
3525 rw[fmap_eq_flookup] >>
3526 rw[FLOOKUP_DRESTRICT, FLOOKUP_FUNION] >> fs[] >>
3527 rw[FLOOKUP_DEF]
3528QED
3529
3530Theorem FDIFF_FDOMSUB:
3531 FDIFF (f \\ x) p = FDIFF f p \\ x
3532Proof
3533 rw[fmap_eq_flookup,FDIFF_def,FLOOKUP_DRESTRICT,DOMSUB_FLOOKUP_THM] >> rw[]
3534QED
3535
3536Theorem FDIFF_FDOMSUB_INSERT:
3537 FDIFF (f \\ x) p = FDIFF f (x INSERT p)
3538Proof
3539 rw[fmap_eq_flookup,FDIFF_def,FLOOKUP_DRESTRICT,DOMSUB_FLOOKUP_THM] >>
3540 rw[] >> gvs[]
3541QED
3542
3543Theorem FDIFF_BOUND:
3544 FDIFF f p = FDIFF f (p INTER FDOM f)
3545Proof
3546 rw[FDIFF_def,fmap_eq_flookup,FLOOKUP_DRESTRICT] >>
3547 rw[] >> gvs[flookup_thm]
3548QED
3549
3550Theorem FDIFF_FUPDATE:
3551 FDIFF (fm |+ (k,v)) s =
3552 if k IN s then FDIFF fm s else (FDIFF fm s) |+ (k,v)
3553Proof
3554 rw[fmap_eq_flookup, FLOOKUP_FDIFF, FLOOKUP_UPDATE] >>
3555 EVERY_CASE_TAC >> gvs[]
3556QED
3557
3558Theorem FDIFF_FEMPTY[simp]:
3559 FDIFF FEMPTY s = FEMPTY
3560Proof
3561 rw[fmap_eq_flookup, FLOOKUP_FDIFF]
3562QED
3563
3564Theorem FDIFF_EMPTY[simp]:
3565 !f. FDIFF f {} = f
3566Proof
3567 rw[fmap_eq_flookup, FLOOKUP_FDIFF]
3568QED
3569
3570Theorem FDIFF_FMAP_MAP2:
3571 !f m s. FDIFF (FMAP_MAP2 f m) s = FMAP_MAP2 f (FDIFF m s)
3572Proof
3573 rw[fmap_eq_flookup, FLOOKUP_FDIFF, FLOOKUP_FMAP_MAP2] >> rw[]
3574QED
3575
3576(* ----------------------------------------------------------------------
3577 FMINUS : ('a |-> 'b) -> ('a |-> 'c) -> ('a |-> 'b)
3578
3579 a variation on FDIFF where the set of keys to be removed from the
3580 first argument is the domain (i.e., FDOM) of the second argument.
3581 ---------------------------------------------------------------------- *)
3582
3583Definition FMINUS_def:
3584 FMINUS fm1 fm2 = FDIFF fm1 (FDOM fm2)
3585End
3586
3587Theorem FLOOKUP_FMINUS:
3588 FLOOKUP (FMINUS f1 f2) k =
3589 case FLOOKUP f2 k of
3590 NONE => FLOOKUP f1 k
3591 | SOME v => NONE
3592Proof
3593 rw[FMINUS_def, FDIFF_def, FLOOKUP_DRESTRICT] >>
3594 Cases_on ‘FLOOKUP f2 k’ >> gvs[FLOOKUP_DEF]
3595QED
3596
3597(* ----------------------------------------------------------------------
3598 FINTER : ('a |-> 'b) -> ('a |-> 'c) -> ('a |-> 'b)
3599
3600 Keeps the entries of the first map whose keys are in the domain of
3601 the second map.
3602 ----------------------------------------------------------------------- *)
3603
3604Definition FINTER_def:
3605 FINTER f1 f2 = DRESTRICT f1 (FDOM f2)
3606End
3607
3608Theorem FLOOKUP_FINTER:
3609 FLOOKUP (FINTER f1 f2) k =
3610 case FLOOKUP f2 k of
3611 NONE => NONE
3612 | SOME v => FLOOKUP f1 k
3613Proof
3614 rw[FINTER_def, FLOOKUP_DRESTRICT] >>
3615 Cases_on ‘FLOOKUP f2 k’ >> gvs[FLOOKUP_DEF]
3616QED
3617
3618
3619Theorem FMERGE_WITH_KEY_FUNION_ALT:
3620 FMERGE_WITH_KEY f (FUNION m1 m2) m3 =
3621 FUNION
3622 (FMERGE_WITH_KEY f m1 (DRESTRICT m3 (FDOM m1)))
3623 (FMERGE_WITH_KEY f m2 (FDIFF m3 (FDOM m1)))
3624Proof
3625 rw[fmap_eq_flookup, FLOOKUP_FMERGE_WITH_KEY,
3626 FLOOKUP_FUNION, FLOOKUP_DRESTRICT, FLOOKUP_FDIFF] >>
3627 every_case_tac >> gvs[FLOOKUP_DEF]
3628QED
3629
3630
3631(* ----------------------------------------------------------------------
3632 fixpoint calculations over finite maps
3633 ---------------------------------------------------------------------- *)
3634
3635Inductive fmlfpR:
3636 (!A0 A1.
3637 A0 = A1 ==> fmlfpR f fm0 A0 FEMPTY A1 A0) /\
3638 (!A0 A1 A2.
3639 fmlfpR f fm0 A1 fm0 A1 A2 /\ A0 <> A1 ==>
3640 fmlfpR f fm0 A0 FEMPTY A1 A2) /\
3641 (!A0 A1 A2 fm k v.
3642 fmlfpR f fm0 A0 (fm \\ k) (f k v A1) A2 ==>
3643 fmlfpR f fm0 A0 (fm |+ (k,v)) A1 A2)
3644End
3645
3646(* the above is super generic "recursion" over finite maps.
3647 Proving termination super-generically involves lots of worry about partial
3648 orders and well-foundedness.
3649 *)
3650
3651Definition lbound_def:
3652 lbound l R x y <=> RTC R l x /\ RTC R l y /\ R x y
3653End
3654
3655Theorem WF_lbound_inv_SUBSET:
3656 FINITE s ==> WF (lbound s (inv (PSUBSET)))
3657Proof
3658 simp[WF_DEF, lbound_def,
3659 inv_MOVES_OUT] >> strip_tac >>
3660 qx_gen_tac ‘B’ >> strip_tac >>
3661 qabbrev_tac ‘B' = { s0 | s0 IN B /\ s0 SUBSET s}’ >>
3662 Cases_on ‘B' = {}’
3663 >- (qexists_tac ‘w’ >>
3664 ‘~(w SUBSET s)’ suffices_by simp[] >> strip_tac >>
3665 ‘w IN B'’ by (simp[Abbr‘B'’] >> simp[IN_DEF]) >> gs[]) >>
3666 ‘FINITE B'’
3667 by (irule SUBSET_FINITE >> qexists_tac ‘POW s’ >> simp[Abbr‘B'’] >>
3668 simp[SUBSET_DEF, IN_POW]) >>
3669 ‘?e. is_measure_maximal CARD B' e’ by simp[FINITE_is_measure_maximal] >>
3670 gs[is_measure_maximal_def] >> qexists_tac ‘e’ >> rpt strip_tac
3671 >- (gs[Abbr‘B'’] >> gs[IN_DEF]) >>
3672 rename [‘c PSUBSET b’, ‘b SUBSET s’] >>
3673 ‘FINITE b’ by metis_tac[SUBSET_FINITE] >>
3674 ‘CARD c < CARD b’ by metis_tac[CARD_PSUBSET] >>
3675 pop_assum mp_tac >> simp[arithmeticTheory.NOT_LESS] >> first_x_assum irule >>
3676 simp[Abbr‘B'’] >> simp[IN_DEF]
3677QED
3678
3679Theorem FLOOKUP_FOLDR_UPDATE:
3680 ALL_DISTINCT (MAP FST kvl) /\ DISJOINT (set (MAP FST kvl)) (FDOM fm) ==>
3681 (FLOOKUP (FOLDR (flip $|+) fm kvl) k = SOME v <=>
3682 MEM (k,v) kvl \/ FLOOKUP fm k = SOME v)
3683Proof
3684 Induct_on ‘kvl’ >>
3685 simp[FORALL_PROD, FLOOKUP_UPDATE, AllCaseEqs(), listTheory.MEM_MAP] >>
3686 qx_genl_tac [‘kk’, ‘vv’] >> strip_tac >> gvs[] >>
3687 Cases_on ‘MEM (k,v) kvl’ >> simp[] >- metis_tac[] >>
3688 Cases_on ‘FLOOKUP fm k = SOME v’ >> simp[]
3689 >- (gvs[FLOOKUP_DEF] >> metis_tac[]) >>
3690 metis_tac[]
3691QED
3692
3693Theorem RC_XX[simp,local]:
3694 RC R x x
3695Proof
3696 simp[RC_DEF]
3697QED
3698
3699Theorem fmlfpR_lastpass:
3700 (!k v. FLOOKUP fm k = SOME v ==> f k v A = A)
3701 ==>
3702 (fmlfpR f fm A fm A B <=> A = B)
3703Proof
3704 strip_tac >> eq_tac
3705 >- (‘!fm0 B A0 A1. fmlfpR f fm A0 fm0 A1 B ==>
3706 A1 = A /\ A0 = A /\ fm0 SUBMAP fm ==> A = B’
3707 suffices_by metis_tac[SUBMAP_REFL] >>
3708 Induct_on ‘fmlfpR’ >> simp[] >> rw[] >>
3709 gs[SUBMAP_FUPDATE] >>
3710 ‘FLOOKUP fm k = SOME v’ by simp[FLOOKUP_DEF] >>
3711 first_x_assum irule >> simp[] >>
3712 fs[GSYM SUBMAP_DOMSUB_gen]) >>
3713 rw[] >>
3714 ‘!gm. gm SUBMAP fm ==> fmlfpR f fm A gm A A’
3715 suffices_by metis_tac[SUBMAP_REFL]>>
3716 ho_match_mp_tac fmap_INDUCT >> rw[] >> simp[fmlfpR_rules] >>
3717 irule (cj 3 fmlfpR_rules) >>
3718 rename [‘gm \\ k’, ‘f k v A’] >>
3719 fs[SUBMAP_FUPDATE, GSYM SUBMAP_DOMSUB_gen] >>
3720 ‘gm \\ k = gm’ by simp[DOMSUB_NOT_IN_DOM] >>
3721 ‘f k v A = A’ suffices_by metis_tac[] >>
3722 first_x_assum irule >> simp[FLOOKUP_DEF]
3723QED
3724
3725Theorem FOLDR_FUPDATE_DOMSUB[local]:
3726 ALL_DISTINCT (MAP FST kvl) /\ DISJOINT (set (MAP FST kvl)) (FDOM fm) /\
3727 k IN FDOM fm ==>
3728 FOLDR (flip $|+) (fm \\ k) kvl |+ (k, fm ' k) =
3729 FOLDR (flip $|+) fm kvl
3730Proof
3731 Induct_on ‘kvl’ >> simp[FUPDATE_ELIM, listTheory.MEM_MAP, FORALL_PROD] >>
3732 metis_tac[FUPDATE_COMMUTES]
3733QED
3734
3735val mkAbbr = CONV_RULE (REWR_CONV (GSYM markerTheory.Abbrev_def))
3736
3737Definition fp_soluble_def:
3738 fp_soluble R P fm f <=>
3739 transitive R /\ WF (lbound P (inv R)) /\
3740 (!k v A. FLOOKUP fm k = SOME v /\ RC R A P ==>
3741 RC R A (f k v A) /\ RC R (f k v A) P) /\
3742 (* (!k v. FLOOKUP fm k = SOME v ==> f k v P = P) /\ *)
3743 !A. R A P ==> ?k v. FLOOKUP fm k = SOME v /\ f k v A <> A
3744End
3745
3746Theorem fp_soluble_FOLDR1:
3747 fp_soluble R P fm0 f /\
3748 fm0 = FOLDR (flip $|+) fm kvl /\
3749 DISJOINT (set (MAP FST kvl)) (FDOM fm) /\
3750 ALL_DISTINCT (MAP FST kvl) ==>
3751 (!s A. IS_SUFFIX kvl s /\ RC R A P ==>
3752 RC R A (FOLDR (UNCURRY f) A s) /\
3753 RC R (FOLDR (UNCURRY f) A s) P) /\
3754 !s A k v. IS_SUFFIX kvl s /\ RC R A P /\ MEM (k,v) s /\
3755 f k v A <> A ==>
3756 FOLDR (UNCURRY f) A s <> A
3757Proof
3758 simp[fp_soluble_def] >> strip_tac >>
3759 conj_asm1_tac
3760 >- (Induct >> simp[FORALL_PROD] >>
3761 qx_genl_tac [‘k’, ‘v’, ‘A’] >> strip_tac >>
3762 ‘transitive (RC R)’ by metis_tac[transitive_RC] >>
3763 drule_then assume_tac rich_listTheory.IS_SUFFIX_CONS2_E >>
3764 first_x_assum $ drule_all_then strip_assume_tac >>
3765 fs[transitive_def] >> conj_tac >> first_x_assum irule
3766 >- (first_assum (goal_assum o resolve_then Any mp_tac) >>
3767 first_x_assum (irule o cj 1) >> simp[FLOOKUP_FOLDR_UPDATE] >>
3768 fs[rich_listTheory.IS_SUFFIX_APPEND] >> gvs[]) >>
3769 goal_assum (resolve_then (Pos last) mp_tac RC_XX) >>
3770 first_x_assum (irule o cj 2) >> simp[FLOOKUP_FOLDR_UPDATE] >>
3771 gvs[rich_listTheory.IS_SUFFIX_APPEND]) >>
3772 Induct >> simp[FORALL_PROD] >> rpt strip_tac
3773 >- (qpat_x_assum ‘k = _’ (SUBST_ALL_TAC o SYM) >>
3774 qpat_x_assum ‘v = _’ (SUBST_ALL_TAC o SYM) >>
3775 qabbrev_tac ‘AA = FOLDR (UNCURRY f) A s’ >>
3776 ‘AA <> A’ by metis_tac[] >>
3777 drule_then assume_tac rich_listTheory.IS_SUFFIX_CONS2_E >>
3778 ‘RC R A AA /\ RC R AA P’ by metis_tac[] >>
3779 ‘R A AA’ by metis_tac[RC_DEF] >>
3780 ‘MEM (k,v) kvl’ by gvs[rich_listTheory.IS_SUFFIX_APPEND] >>
3781 ‘RC R AA (f k v AA)’ by metis_tac[FLOOKUP_FOLDR_UPDATE] >>
3782 ‘R A A’ by metis_tac[transitive_def, RC_DEF] >>
3783 ‘lbound P (inv R) A A’
3784 by (simp[lbound_def, inv_MOVES_OUT] >> rpt strip_tac >>
3785 metis_tac[RC_DEF, RTC_SUBSET, RTC_RULES]) >>
3786 metis_tac[WF_NOT_REFL]) >>
3787 qabbrev_tac ‘AA = FOLDR (UNCURRY f) A s’ >>
3788 drule_then assume_tac rich_listTheory.IS_SUFFIX_CONS2_E >>
3789 first_x_assum (drule_then $ drule_then $ drule_then $
3790 drule_then assume_tac) >> rfs[] >>
3791 rename [‘IS_SUFFIX _ ((kk,vv)::sfx)’] >>
3792 ‘MEM (kk,vv) kvl’ by gvs[rich_listTheory.IS_SUFFIX_APPEND] >>
3793 ‘FLOOKUP fm0 kk = SOME vv’ by metis_tac[FLOOKUP_FOLDR_UPDATE] >>
3794 ‘RC R A AA /\ RC R AA (f kk vv AA)’ by metis_tac[] >>
3795 ‘R A A’ by metis_tac[RC_DEF, transitive_def] >>
3796 ‘lbound P (inv R) A A’
3797 by (simp[lbound_def, inv_MOVES_OUT] >> rpt strip_tac >>
3798 metis_tac[RC_DEF, RTC_SUBSET, RTC_RULES]) >>
3799 metis_tac[WF_NOT_REFL]
3800QED
3801
3802Theorem FOLDR_FUPDATE_DOMSUB'[local]:
3803 ALL_DISTINCT (MAP FST kvl) /\ DISJOINT (set (MAP FST kvl)) (FDOM fm) /\
3804 ~MEM k (MAP FST kvl) ==>
3805 FOLDR (flip $|+) (fm \\ k) kvl |+ (k,v) =
3806 FOLDR (flip $|+) (fm |+ (k,v)) kvl
3807Proof
3808 Induct_on ‘kvl’ >> simp[FORALL_PROD, listTheory.MEM_MAP] >> rpt strip_tac >>
3809 gvs[listTheory.MEM_MAP, FORALL_PROD] >>
3810 metis_tac[FUPDATE_COMMUTES]
3811QED
3812
3813Theorem fmlfpR_total_lemma:
3814 fp_soluble R P fm0 f
3815 ==>
3816 RC R A0 A1 /\ RC R A1 P /\ (fm : 'b |-> 'c) SUBMAP fm0 /\
3817 A1 = FOLDR (UNCURRY f) A0 kvl /\
3818 DISJOINT (set (MAP FST kvl)) (FDOM fm) /\
3819 ALL_DISTINCT (MAP FST kvl) /\
3820 fm0 = FOLDR (flip $|+) fm kvl
3821==>
3822 (fmlfpR f fm0 A0 fm A1 A2 <=> A2 = P)
3823Proof
3824 strip_tac >> REWRITE_TAC[EQ_IMP_THM, IMP_CONJ_THM] >> conj_tac
3825 >- (map_every qid_spec_tac [‘A0’, ‘A1’, ‘A2’, ‘fm’, ‘kvl’] >>
3826 Induct_on ‘fmlfpR’ >>
3827 rpt strip_tac
3828 >- (qpat_x_assum ‘A0 = A1’ SUBST_ALL_TAC >>
3829 qpat_x_assum ‘RC R A1 P’ mp_tac >>
3830 simp[RC_DEF, DISJ_IMP_THM] >> strip_tac >>
3831 drule_all_then strip_assume_tac fp_soluble_FOLDR1 >>
3832 ‘?k v. FLOOKUP fm0 k = SOME v /\ f k v A1 <> A1’
3833 by metis_tac[fp_soluble_def] >>
3834 pop_assum (first_x_assum o resolve_then (Pos last) mp_tac) >>
3835 rw[] >> rfs[FLOOKUP_FOLDR_UPDATE] >>
3836 metis_tac[rich_listTheory.IS_SUFFIX_REFL, RC_DEF])
3837 >- (first_x_assum $ qspec_then ‘[]’ mp_tac >> simp[]) >>
3838 first_x_assum irule >> rpt conj_tac
3839 >- (qexists_tac ‘(k,v)::kvl’ >> simp[] >> gs[] >>
3840 simp[FOLDR_FUPDATE_DOMSUB'] >>
3841 gvs[DISJOINT_DEF, EXTENSION, listTheory.MEM_MAP, FORALL_PROD] >>
3842 metis_tac[])
3843 >- gs[SUBMAP_FUPDATE, GSYM SUBMAP_DOMSUB_gen]
3844 >- (qpat_x_assum ‘fm0 = _’ (assume_tac o mkAbbr) >>
3845 qpat_x_assum ‘A1 = _’ (assume_tac o mkAbbr) >>
3846 gs[SUBMAP_FUPDATE, GSYM SUBMAP_DOMSUB_gen] >>
3847 ‘FLOOKUP fm0 k = SOME v’ by simp[FLOOKUP_DEF] >>
3848 metis_tac[transitive_def, transitive_RC, fp_soluble_def]) >>
3849 qpat_x_assum ‘fm0 = _’ (assume_tac o mkAbbr) >>
3850 qpat_x_assum ‘A1 = _’ (assume_tac o mkAbbr) >>
3851 gs[SUBMAP_FUPDATE, GSYM SUBMAP_DOMSUB_gen] >>
3852 ‘FLOOKUP fm0 k = SOME v’ by simp[FLOOKUP_DEF] >>
3853 metis_tac[transitive_def, transitive_RC, fp_soluble_def]) >>
3854 Cases_on ‘A2 = P’ >> ASM_REWRITE_TAC [] >> pop_assum (K ALL_TAC) >>
3855 map_every qid_spec_tac [‘A0’, ‘kvl’] >>
3856 ‘WF (lbound P (inv R) LEX measure (FCARD : ('b |-> 'c) -> num))’
3857 by gs[WF_LEX, fp_soluble_def] >>
3858 ‘?p. p = (A1,fm)’ by simp[] >> pop_assum mp_tac >>
3859 map_every qid_spec_tac [‘A1’, ‘fm’, ‘p’] >>
3860 drule WF_INDUCTION_THM >>
3861 simp[SimpL “$==>”, lbound_def, inv_MOVES_OUT, GSYM PULL_FORALL] >>
3862 disch_then ho_match_mp_tac >> simp[FORALL_PROD] >>
3863 qx_genl_tac [‘A1’, ‘fm’] >> strip_tac >>
3864 qx_genl_tac [‘kvl’, ‘A0’] >> strip_tac >>
3865 Cases_on ‘fm = FEMPTY’
3866 >- (pop_assum SUBST_ALL_TAC >> Cases_on ‘A0 = A1’
3867 >- (pop_assum SUBST_ALL_TAC >> simp[Once fmlfpR_cases] >>
3868 qpat_x_assum ‘A1 = FOLDR _ A1 kvl’ (assume_tac o SYM) >>
3869 qpat_x_assum ‘fm0 = FOLDR _ _ _’ (assume_tac o SYM) >>
3870 gs[] >>
3871 qpat_x_assum ‘RC R A1 P’ mp_tac >>
3872 simp[RC_DEF, DISJ_IMP_THM] >> strip_tac >>
3873 first_x_assum $ qspecl_then [‘ARB’, ‘ARB’] $ K ALL_TAC >>
3874 ‘?k v. FLOOKUP fm0 k = SOME v /\ f k v A1 <> A1’
3875 by metis_tac[fp_soluble_def] >>
3876 drule_then (qspecl_then [‘kvl’, ‘FEMPTY’] mp_tac)
3877 fp_soluble_FOLDR1 >> simp[] >> strip_tac >>
3878 pop_assum (drule_at_then (Pos last) $ qspec_then ‘kvl’ mp_tac) >>
3879 simp[RC_DEF] >> gvs[FLOOKUP_FOLDR_UPDATE]) >>
3880 qpat_x_assum ‘A1 = FOLDR _ A0 kvl’ (assume_tac o SYM) >>
3881 qpat_x_assum ‘fm0 = FOLDR _ _ _’ (assume_tac o SYM) >> simp[] >> gs[] >>
3882 irule (cj 2 fmlfpR_rules) >> simp[] >>
3883 Cases_on ‘!k v. FLOOKUP fm0 k = SOME v ==> f k v A1 = A1’
3884 >- (simp[fmlfpR_lastpass] >>
3885 qpat_x_assum ‘RC R A1 P’ mp_tac >> simp[RC_DEF, DISJ_IMP_THM] >>
3886 metis_tac[fp_soluble_def]) >>
3887 gs[] >>
3888 ‘(fm0 \\ k) |+ (k,v) = fm0’
3889 by (simp[FUPDATE_PURGE'] >> gs[FLOOKUP_DEF, FUPDATE_ELIM]) >>
3890 ‘fmlfpR f fm0 A1 fm0 A1 = fmlfpR f fm0 A1 ((fm0\\k)|+(k,v)) A1’
3891 by simp[] >>
3892 pop_assum SUBST1_TAC >>
3893 goal_assum (resolve_then (Pos hd) mp_tac (cj 3 fmlfpR_rules)) >>
3894 simp[] >> first_x_assum $ qspecl_then [‘f k v A1’, ‘fm0 \\ k’] mp_tac >>
3895 impl_tac
3896 >- (simp[LEX_DEF, lbound_def, inv_MOVES_OUT] >> rpt conj_tac
3897 >- (‘RC R (f k v A1) P’ by metis_tac[fp_soluble_def] >>
3898 gvs[RC_DEF])
3899 >- gvs[RC_DEF] >>
3900 ‘RC R A1 (f k v A1)’ by metis_tac[fp_soluble_def] >> gvs[RC_DEF]) >>
3901 disch_then $ qspecl_then [‘[(k,v)]’, ‘A1’] mp_tac >>
3902 simp[] >> gs[fp_soluble_def]) >>
3903 qpat_x_assum ‘A1 = _’ (assume_tac o mkAbbr) >>
3904 qpat_x_assum ‘fm0 = _’ (assume_tac o mkAbbr) >>
3905 simp[] >>
3906 ‘?k. k IN FDOM fm’ by metis_tac[FDOM_F_FEMPTY1] >>
3907 ‘fm = fm \\ k |+ (k, fm ' k)’ by simp[FUPDATE_PURGE', FUPDATE_ELIM] >>
3908 pop_assum SUBST1_TAC >>
3909 irule (cj 3 fmlfpR_rules) >>
3910 simp[] >>
3911 first_x_assum $ qspecl_then [‘f k (fm ' k) A1’, ‘fm \\ k’] mp_tac >>
3912 impl_tac
3913 >- (simp[LEX_DEF, lbound_def, inv_MOVES_OUT] >>
3914 simp[FCARD_DEF] >>
3915 ‘0 < CARD (FDOM fm)’
3916 by (‘fm = fm \\ k |+ (k, fm ' k)’
3917 by simp[FUPDATE_PURGE', FUPDATE_ELIM] >>
3918 pop_assum SUBST1_TAC >> REWRITE_TAC [FDOM_FUPDATE] >>
3919 simp[]) >> simp[] >>
3920 ‘FLOOKUP fm0 k = SOME (fm ' k)’ by metis_tac[SUBMAP_DEF, FLOOKUP_DEF] >>
3921 ‘RC R A1 (f k (fm ' k) A1)’ by metis_tac[fp_soluble_def] >>
3922 pop_assum mp_tac >> simp[RC_DEF, DISJ_IMP_THM] >>
3923 gs[fp_soluble_def] >> metis_tac[RC_DEF, RTC_RULES, RTC_SUBSET]) >>
3924 qabbrev_tac ‘v = fm ' k’ >>
3925 disch_then $ qspecl_then [‘(k,v)::kvl’, ‘A0’] mp_tac >> simp[] >>
3926 ‘FOLDR (flip $|+) (fm \\ k) kvl |+ (k,v) = fm0’
3927 by (simp[Abbr‘fm0’] >> simp[FOLDR_FUPDATE_DOMSUB, Abbr‘v’]) >>
3928 simp[] >> disch_then irule >>
3929 simp[listTheory.MEM_MAP, FORALL_PROD] >>
3930 gs[DISJOINT_DEF, EXTENSION, listTheory.MEM_MAP, FORALL_PROD] >> rpt conj_tac
3931 >- metis_tac[]
3932 >- metis_tac[]
3933 >- metis_tac[SUBMAP_TRANS, SUBMAP_DOMSUB]
3934 >- (‘FLOOKUP fm0 k = SOME v’ by metis_tac[SUBMAP_DEF, FLOOKUP_DEF] >>
3935 gs[fp_soluble_def] >>
3936 metis_tac[transitive_def, RC_DEF, RTC_RULES, transitive_RC])
3937 >- (‘FLOOKUP fm0 k = SOME v’ by metis_tac[SUBMAP_DEF, FLOOKUP_DEF] >>
3938 gs[fp_soluble_def] >>
3939 metis_tac[transitive_def, RC_DEF, RTC_RULES, transitive_RC])
3940QED
3941
3942Theorem fmlfpR_total =
3943 fmlfpR_total_lemma |> Q.INST[‘kvl’ |-> ‘[]’] |> GEN_ALL
3944 |> SIMP_RULE(srw_ss()) []
3945
3946(* collection theorems *)
3947
3948Theorem TO_FLOOKUP:
3949 (x IN FDOM m <=> FLOOKUP (m:'a |-> 'b) x <> NONE) /\
3950 (y IN FRANGE m <=> ?k. FLOOKUP m k = SOME y) /\
3951 (FLOOKUP m x <> NONE ==> m ' x = THE (FLOOKUP m x)) /\
3952 (m = m' <=> FLOOKUP m = FLOOKUP m') /\
3953 (m SUBMAP m' <=> !k v. FLOOKUP m k = SOME v ==> FLOOKUP m' k = SOME v) /\
3954 (FEVERY P m <=> !k v. FLOOKUP m k = SOME v ==> P (k, v))
3955Proof
3956 fs [SUBMAP_FLOOKUP_EQN,FLOOKUP_DEF,FRANGE_DEF,FEVERY_DEF]
3957 \\ fs [fmap_eq_flookup] \\ fs [FUN_EQ_THM]
3958QED
3959
3960Theorem FLOOKUP_FDIFF[local]:
3961 FLOOKUP (FDIFF m d) k = if k IN d then NONE else FLOOKUP m k
3962Proof
3963 fs [FDIFF_def,FLOOKUP_DRESTRICT] \\ rw [] \\ gvs []
3964QED
3965
3966Theorem FLOOKUP_SIMP =
3967 [FLOOKUP_EMPTY, FLOOKUP_UPDATE, FDIFF_def, FLOOKUP_FMAP_MAP2,
3968 FLOOKUP_DRESTRICT, FLOOKUP_FDIFF, FLOOKUP_FUNION, FLOOKUP_FUN_FMAP,
3969 FLOOKUP_FMAP_MAP2, FLOOKUP_FMERGE, FLOOKUP_FMINUS, FLOOKUP_FINTER]
3970 |> map SPEC_ALL |> LIST_CONJ;
3971
3972(*---------------------------------------------------------------------------*)
3973(* Add fmap type to the TypeBase. Notice that we treat keys as being of size *)
3974(* zero, and make sure to add one to the size of each mapped value. This *)
3975(* ought to handle the case where the map points to something of size 0: *)
3976(* deleting it from the map will then make the map smaller. *)
3977(*---------------------------------------------------------------------------*)
3978
3979val _ = TypeBase.export [
3980 TypeBasePure.mk_nondatatype_info (
3981 “:'a |-> 'b”,
3982 {encode = NONE,
3983 size = SOME (“λ(ksize:'a -> num) (vsize:'b -> num).
3984 fmap_size (λk:'a. 0) (λv. 1 + vsize v)”,
3985 fmap_size_def),
3986 induction = SOME fmap_INDUCT,
3987 nchotomy = SOME fmap_CASES}
3988 )
3989 ]
3990
3991
3992(* ----------------------------------------------------------------------
3993 Finite maps as a bounded natural functor in their range, so that a
3994 datatype specification can recurse through one: o_f is the map,
3995 FRANGE the set function, fmap_rel the relator, and a finite map
3996 holds no more values than there are numbers.
3997 ---------------------------------------------------------------------- *)
3998
3999fun bnm s : KernelSig.kernelname = {Thy = "finite_map", Name = s}
4000
4001Theorem fmapMap_ID:
4002 $o_f (I:'a1 -> 'a1) = (I : ('b1 |-> 'a1) -> ('b1 |-> 'a1))
4003Proof
4004 simp[FUN_EQ_THM, combinTheory.I_EQ_IDABS]
4005QED
4006
4007Theorem fmapMap_O:
4008 $o_f (f1:'c1 -> 'd1) o $o_f (g1:'a1 -> 'c1) =
4009 ($o_f (f1 o g1) : ('b1 |-> 'a1) -> ('b1 |-> 'd1))
4010Proof
4011 simp[FUN_EQ_THM]
4012QED
4013
4014Theorem fmapMapIMAGE1:
4015 !(f1:'a1 -> 'c1) (m:'b1 |-> 'a1). FRANGE (f1 o_f m) = IMAGE f1 (FRANGE m)
4016Proof
4017 simp[IMAGE_FRANGE]
4018QED
4019
4020Theorem fmapMapCONG:
4021 (!a1. a1 IN FRANGE (m : 'b1 |-> 'a1) ==> (f1:'a1 -> 'c1) a1 = g1 a1) ==>
4022 f1 o_f m = g1 o_f m
4023Proof
4024 strip_tac >> irule o_f_cong >> simp[]
4025QED
4026
4027Theorem fmap_bnd1:
4028 !m : 'b1 |-> 'a1. FRANGE m <<= univ(:num)
4029Proof
4030 gen_tac >> ONCE_REWRITE_TAC[cardinalityCoreTheory.cardleq_lteq] >>
4031 disj1_tac >> simp[GSYM cardinalityCoreTheory.FINITE_CARD_LT]
4032QED
4033
4034Theorem fmap_wit1:
4035 !a1:'a1. FRANGE (K FEMPTY a1 : 'b1 |-> 'a1) SUBSET {}
4036Proof
4037 simp[]
4038QED
4039
4040Theorem fmap_inh1:
4041 !v:'a1. v IN FRANGE ((FUPDATE FEMPTY o $, (ARB:'b1)) v)
4042Proof
4043 simp[FRANGE_FUPDATE]
4044QED
4045
4046val _ = bnfBase.updateDB (
4047 {Thy = "finite_map", Name = "fmap"},
4048 bnfBase.bI {
4049 canontype = “:'b1 |-> 'a1”,
4050
4051 map = “$o_f : ('a1 -> 'c1) -> ('b1 |-> 'a1) -> ('b1 |-> 'c1)”,
4052 set = [“FRANGE : ('b1 |-> 'a1) -> 'a1 set”],
4053 mapID = bnm "fmapMap_ID",
4054 mapO = bnm "fmapMap_O",
4055 mapIMAGE = [bnm "fmapMapIMAGE1"],
4056 mapCONG = bnm "fmapMapCONG",
4057
4058 relator = “fmap_rel : ('a1 -> 'c1 -> bool) ->
4059 ('b1 |-> 'a1) -> ('b1 |-> 'c1) -> bool”,
4060 bnd = “univ(:num)”,
4061 bndthms = [bnm "fmap_bnd1"],
4062
4063 wits = [(“K FEMPTY : 'a1 -> ('b1 |-> 'a1)”, bnm "fmap_wit1")],
4064 inhabits = [(“(FUPDATE FEMPTY o $, (ARB:'b1)) : 'a1 -> ('b1 |-> 'a1)”,
4065 bnm "fmap_inh1")]
4066 }
4067)