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