alistScript.sml

1Theory alist
2Ancestors
3  finite_map list rich_list pred_set sorting pair relation
4Libs
5  boolSimps
6
7val _ = diminish_srw_ss ["NORMEQ"]
8
9Type alist = ``:(('a # 'b) list)``
10
11Definition fmap_to_alist_def:
12  fmap_to_alist s = MAP (\k.(k,s ' k)) (SET_TO_LIST (FDOM s))
13End
14
15Theorem fmap_to_alist_FEMPTY[simp]:
16    (fmap_to_alist FEMPTY = [])
17Proof
18  SRW_TAC [][fmap_to_alist_def]
19QED
20
21Definition alist_to_fmap_def:
22  alist_to_fmap s = FOLDR (\(k,v) f.f|+(k,v)) FEMPTY s
23End
24
25Theorem alist_to_fmap_thm[simp]:
26    (alist_to_fmap [] = FEMPTY) /\
27    (alist_to_fmap ((k,v)::t) = alist_to_fmap t |+ (k,v))
28Proof
29  SRW_TAC [][alist_to_fmap_def]
30QED
31
32Definition ALOOKUP_def[simp]:
33  (ALOOKUP [] q = NONE) /\
34  (ALOOKUP ((x,y)::t) q = if x = q then SOME y else ALOOKUP t q)
35End
36val ALOOKUP_ind = theorem"ALOOKUP_ind";
37
38Theorem lemma[local]:
39 MAP (\k.(k,fm ' k)) (SET_TO_LIST (REST (FDOM fm))) =
40 fmap_to_alist (fm \\ (CHOICE (FDOM fm)))
41Proof
42SRW_TAC [][fmap_to_alist_def,REST_DEF] THEN
43MATCH_MP_TAC MAP_CONG THEN SRW_TAC [][DOMSUB_FAPPLY_THM]
44QED
45
46Theorem ALOOKUP_FAILS:
47    (ALOOKUP l x = NONE) <=> !k v. MEM (k,v) l ==> k <> x
48Proof
49  Induct_on `l` THEN SRW_TAC [][] THEN
50  Cases_on `h` THEN SRW_TAC [][] THEN METIS_TAC []
51QED
52
53Theorem ALOOKUP_NONE:
54  !l x. (ALOOKUP l x = NONE) = ~MEM x (MAP FST l)
55Proof
56SRW_TAC[][ALOOKUP_FAILS,MEM_MAP,pairTheory.FORALL_PROD]
57QED
58
59Theorem ALOOKUP_TABULATE:
60    MEM x l ==>
61    (ALOOKUP (MAP (\k. (k, f k)) l) x = SOME (f x))
62Proof
63  Induct_on `l` THEN SRW_TAC [][]
64QED
65
66Theorem ALOOKUP_EQ_FLOOKUP[simp]:
67 (FLOOKUP (alist_to_fmap al) = ALOOKUP al) /\
68 (ALOOKUP (fmap_to_alist fm) = FLOOKUP fm)
69Proof
70SRW_TAC [][FUN_EQ_THM] THEN Q.ID_SPEC_TAC `x` THENL [
71  Q.ID_SPEC_TAC `al` THEN
72  HO_MATCH_MP_TAC ALOOKUP_ind THEN
73  SRW_TAC [][alist_to_fmap_def,ALOOKUP_def,FLOOKUP_UPDATE],
74
75  SRW_TAC [][fmap_to_alist_def] THEN
76  Cases_on `x IN FDOM fm` THEN SRW_TAC [][FLOOKUP_DEF] THENL [
77    MATCH_MP_TAC ALOOKUP_TABULATE THEN SRW_TAC [][],
78    SRW_TAC [][ALOOKUP_FAILS, MEM_MAP]
79  ]
80]
81QED
82
83Theorem MEM_fmap_to_alist:
84    MEM (x,y) (fmap_to_alist fm) <=> x IN FDOM fm /\ (fm ' x = y)
85Proof
86  SRW_TAC [][fmap_to_alist_def, MEM_MAP] THEN METIS_TAC []
87QED
88
89Theorem MEM_fmap_to_alist_FLOOKUP:
90  !p fm. MEM p (fmap_to_alist fm) = (FLOOKUP fm (FST p) = SOME (SND p))
91Proof
92Cases >> rw[MEM_fmap_to_alist,FLOOKUP_DEF]
93QED
94
95Theorem MEM_pair_fmap_to_alist_FLOOKUP[simp]:
96  !x y fm. MEM (x,y) (fmap_to_alist fm) = (FLOOKUP fm x = SOME y)
97Proof
98rw[MEM_fmap_to_alist_FLOOKUP]
99QED
100
101Theorem LENGTH_fmap_to_alist[simp]:
102  !fm. LENGTH (fmap_to_alist fm) = CARD (FDOM fm)
103Proof
104rw[fmap_to_alist_def,SET_TO_LIST_CARD]
105QED
106
107Theorem fmap_to_alist_to_fmap[simp]:
108    alist_to_fmap (fmap_to_alist fm) = fm
109Proof
110  SRW_TAC [][FLOOKUP_EXT]
111QED
112
113Theorem ALOOKUP_MEM:
114 !al k v.(ALOOKUP al k = SOME v) ==> MEM (k,v) al
115Proof
116Induct THEN SRW_TAC [][] THEN
117Cases_on `h` THEN POP_ASSUM MP_TAC THEN
118SRW_TAC [][]
119QED
120
121Theorem ALOOKUP_SOME_FAPPLY_alist_to_fmap[simp]:
122  !al k v. (ALOOKUP al k = SOME v) ==> (alist_to_fmap al ' k = v)
123Proof
124REPEAT STRIP_TAC THEN
125Q_TAC SUFF_TAC `FLOOKUP (alist_to_fmap al) k = SOME v` THEN1
126  SRW_TAC[][FLOOKUP_DEF,MEM_MAP] THEN
127SRW_TAC[][]
128QED
129
130Theorem alist_to_fmap_FAPPLY_MEM:
131  !al z. z IN FDOM (alist_to_fmap al) ==> MEM (z, (alist_to_fmap al) ' z) al
132Proof
133rpt strip_tac >>
134match_mp_tac ALOOKUP_MEM >>
135ONCE_REWRITE_TAC[SYM(CONJUNCT1 ALOOKUP_EQ_FLOOKUP)] >>
136REWRITE_TAC[FLOOKUP_DEF] >> rw[]
137QED
138
139Theorem ALOOKUP_MAP:
140  !f al. ALOOKUP (MAP (\(x,y). (x,f y)) al) = OPTION_MAP f o (ALOOKUP al)
141Proof
142gen_tac >> Induct >- rw[FUN_EQ_THM] >> Cases >> rw[FUN_EQ_THM] >> rw[]
143QED
144
145Theorem ALOOKUP_MAP_2:
146  !f al x.
147    ALOOKUP (MAP (\ (x,y). (x,f x y)) al) x =
148    OPTION_MAP (f x) (ALOOKUP al x)
149Proof
150  gen_tac >> Induct >> simp[] >> Cases >> simp[] >> srw_tac[][]
151QED
152
153Theorem FDOM_alist_to_fmap[simp]:
154 !al.FDOM (alist_to_fmap al) = set (MAP FST al)
155Proof
156Induct THEN SRW_TAC [][alist_to_fmap_def] THEN
157Cases_on `h` THEN FULL_SIMP_TAC (srw_ss()) [alist_to_fmap_def]
158QED
159
160Theorem alist_to_fmap_prefix:
161 !ls l1 l2.
162 (alist_to_fmap l1 = alist_to_fmap l2) ==>
163 (alist_to_fmap (ls ++ l1) = alist_to_fmap (ls ++ l2))
164Proof
165Induct THEN SRW_TAC [][] THEN
166Cases_on `h` THEN SRW_TAC [][] THEN METIS_TAC []
167QED
168
169Theorem alist_to_fmap_APPEND[simp]:
170  !l1 l2. alist_to_fmap (l1 ++ l2) = FUNION (alist_to_fmap l1) (alist_to_fmap l2)
171Proof
172Induct >- rw[FUNION_FEMPTY_1] >>
173Cases >> rw[FUNION_FUPDATE_1]
174QED
175
176Theorem ALOOKUP_prefix:
177 !ls k ls2.
178 ((ALOOKUP ls k = SOME v) ==>
179  (ALOOKUP (ls ++ ls2) k = SOME v)) /\
180 ((ALOOKUP ls k = NONE) ==>
181  (ALOOKUP (ls ++ ls2) k = ALOOKUP ls2 k))
182Proof
183HO_MATCH_MP_TAC ALOOKUP_ind THEN
184SRW_TAC [][]
185QED
186
187Theorem ALOOKUP_APPEND:
188  !l1 l2 k. ALOOKUP (l1 ++ l2) k = case ALOOKUP l1 k of SOME v => SOME v | NONE => ALOOKUP l2 k
189Proof
190rw[] >> Cases_on `ALOOKUP l1 k` >> rw[ALOOKUP_prefix]
191QED
192
193Theorem FUPDATE_LIST_EQ_APPEND_REVERSE:
194 !ls fm. fm |++ ls = alist_to_fmap (REVERSE ls ++ fmap_to_alist fm)
195Proof
196Induct THEN1 SRW_TAC [][FUPDATE_LIST_THM,FUNION_FEMPTY_1] THEN
197Cases THEN FULL_SIMP_TAC(srw_ss())[FUPDATE_LIST_THM] THEN
198SRW_TAC[][FUNION_ASSOC,FUNION_FUPDATE_2,FUNION_FEMPTY_2,FUNION_FUPDATE_1]
199QED
200
201Theorem FLOOKUP_FUPDATE_LIST_ALOOKUP_SOME:
202 (ALOOKUP ls k = SOME v) ==> (FLOOKUP (fm |++ (REVERSE ls)) k = SOME v)
203Proof
204SRW_TAC [][FUPDATE_LIST_EQ_APPEND_REVERSE,FLOOKUP_DEF,FUNION_DEF,ALOOKUP_SOME_FAPPLY_alist_to_fmap,MEM_MAP,pairTheory.EXISTS_PROD] THEN
205METIS_TAC [ALOOKUP_MEM]
206QED
207
208Theorem FLOOKUP_FUPDATE_LIST_ALOOKUP_NONE:
209 (ALOOKUP ls k = NONE) ==> (FLOOKUP (fm |++ (REVERSE ls)) k = FLOOKUP fm k)
210Proof
211SRW_TAC [][FUPDATE_LIST_EQ_APPEND_REVERSE,FLOOKUP_DEF,FUNION_DEF,ALOOKUP_FAILS,MEM_MAP,pairTheory.EXISTS_PROD]
212QED
213
214Theorem FUNION_alist_to_fmap:
215    !ls fm. FUNION (alist_to_fmap ls) fm = fm |++ (REVERSE ls)
216Proof
217  Induct THEN1 SRW_TAC[][FUNION_FEMPTY_1,FUPDATE_LIST] THEN
218  Q.X_GEN_TAC `p` THEN PairCases_on `p` THEN
219  SRW_TAC[][FUPDATE_LIST_THM,alist_to_fmap_thm,FUPDATE_LIST_APPEND] THEN
220  SRW_TAC[][FUNION_FUPDATE_1]
221QED
222
223Theorem alist_to_fmap_MAP:
224  !f1 f2 al. INJ f1 (set (MAP FST al)) UNIV ==>
225 (alist_to_fmap (MAP (\ (x,y). (f1 x, f2 y)) al) =
226  MAP_KEYS f1 (f2 o_f alist_to_fmap al))
227Proof
228NTAC 2 GEN_TAC THEN
229Induct THEN1 SRW_TAC[][] THEN
230Cases THEN SRW_TAC[][INJ_INSERT] THEN
231Q.MATCH_ABBREV_TAC `x = MAP_KEYS f1 ((f o_f a) |+ b)` THEN
232UNABBREV_ALL_TAC THEN
233SRW_TAC[][GSYM FUPDATE_PURGE] THEN
234Q.MATCH_ABBREV_TAC `x = MAP_KEYS f1 (fm |+ (k,v))` THEN
235`INJ f1 (k INSERT FDOM fm) UNIV` by (
236  SRW_TAC[][Abbr`fm`,INJ_INSERT] ) THEN
237SRW_TAC[][MAP_KEYS_FUPDATE]
238QED
239
240Theorem alist_to_fmap_to_alist:
241  !al. fmap_to_alist (alist_to_fmap al) =
242       MAP (\k. (k, THE (ALOOKUP al k))) (SET_TO_LIST (set (MAP FST al)))
243Proof
244SRW_TAC[][fmap_to_alist_def,MAP_EQ_f,MEM_MAP] THEN
245Q.MATCH_ASSUM_RENAME_TAC `MEM p al` THEN
246PairCases_on `p` THEN SRW_TAC[][] THEN
247Cases_on `ALOOKUP al p0` THEN
248IMP_RES_TAC ALOOKUP_FAILS THEN
249SRW_TAC[][]
250QED
251
252Theorem alist_to_fmap_to_alist_PERM:
253  !al. ALL_DISTINCT (MAP FST al) ==>
254       PERM (fmap_to_alist (alist_to_fmap al)) al
255Proof
256SRW_TAC[][alist_to_fmap_to_alist,ALL_DISTINCT_PERM_LIST_TO_SET_TO_LIST] THEN
257MATCH_MP_TAC PERM_TRANS THEN
258Q.EXISTS_TAC `MAP (\k. (k, THE (ALOOKUP al k))) (MAP FST al)` THEN
259CONJ_TAC THEN1 (
260  MATCH_MP_TAC PERM_MAP THEN
261  SRW_TAC[][PERM_SYM] ) THEN
262SRW_TAC[][MAP_MAP_o] THEN
263FULL_SIMP_TAC (srw_ss()) [GSYM ALL_DISTINCT_PERM_LIST_TO_SET_TO_LIST] THEN
264Q.MATCH_ABBREV_TAC `PERM ll al` THEN
265Q_TAC SUFF_TAC `ll = al` THEN1 SRW_TAC[][] THEN
266UNABBREV_ALL_TAC THEN
267Induct_on `al` THEN1 SRW_TAC[][] THEN
268Cases THEN SRW_TAC[][MEM_MAP] THEN
269FULL_SIMP_TAC (srw_ss()) [] THEN
270Q.MATCH_ASSUM_ABBREV_TAC `MAP f1 al = al` THEN
271Q.MATCH_ABBREV_TAC `MAP f2 al = al` THEN
272Q_TAC SUFF_TAC `!x. MEM x al ==> (f1 x = f2 x)` THEN1 PROVE_TAC[MAP_EQ_f] THEN
273SRW_TAC[][Abbr`f1`,Abbr`f2`] THEN
274PROVE_TAC[]
275QED
276
277Theorem ALOOKUP_LEAST_EL:
278  !ls k. ALOOKUP ls k = if MEM k (MAP FST ls) then
279         SOME (EL (LEAST n. EL n (MAP FST ls) = k) (MAP SND ls))
280         else NONE
281Proof
282Induct THEN1 SRW_TAC[][] THEN
283Cases THEN SRW_TAC[][] THEN
284FULL_SIMP_TAC(srw_ss())[MEM_MAP] THEN1 (
285  numLib.LEAST_ELIM_TAC THEN
286  SRW_TAC[][] THEN1
287    (Q.EXISTS_TAC `0` THEN SRW_TAC[][]) THEN
288  Cases_on `n` THEN SRW_TAC[][] THEN
289  FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN
290  SRW_TAC[][] ) THEN
291numLib.LEAST_ELIM_TAC THEN
292FULL_SIMP_TAC (srw_ss()) [MEM_EL] THEN
293SRW_TAC[][] THEN1 (
294  Q.EXISTS_TAC `n` THEN
295  SRW_TAC[][EL_MAP] ) THEN
296numLib.LEAST_ELIM_TAC THEN
297SRW_TAC[][] THEN
298Q.MATCH_ASSUM_RENAME_TAC `EL m (MAP FST ls) = FST (EL n ls)` THEN1 (
299  Q.EXISTS_TAC `SUC m` THEN
300  SRW_TAC[][] ) THEN
301Cases_on `n < m` THEN1 METIS_TAC[EL_MAP] THEN
302`m < LENGTH ls` by DECIDE_TAC THEN
303FULL_SIMP_TAC(srw_ss())[EL_MAP] THEN
304Q.MATCH_ASSUM_RENAME_TAC `EL z (h::MAP FST ls) = FST (EL n ls)` THEN
305Cases_on `SUC n < z` THEN1 (
306  RES_TAC THEN
307  FULL_SIMP_TAC(srw_ss())[] THEN
308  METIS_TAC[EL_MAP]) THEN
309`z < SUC (LENGTH ls)` by DECIDE_TAC THEN
310Cases_on `z` THEN FULL_SIMP_TAC (srw_ss()) [EL_MAP] THEN
311Q.MATCH_RENAME_TAC `SND (EL m ls) = SND (EL z ls)` THEN
312Cases_on `m < z` THEN1 (
313  `SUC m < SUC z` by DECIDE_TAC THEN
314  RES_TAC THEN
315  FULL_SIMP_TAC(srw_ss())[] THEN
316  METIS_TAC[EL_MAP] ) THEN
317Cases_on `z < m` THEN1 METIS_TAC[EL_MAP] THEN
318`m = z` by DECIDE_TAC THEN
319SRW_TAC[][]
320QED
321
322Theorem ALOOKUP_ALL_DISTINCT_MEM:
323  ALL_DISTINCT (MAP FST al) /\ MEM (k,v) al ==>
324  (ALOOKUP al k = SOME v)
325Proof
326rw[ALOOKUP_LEAST_EL] >- (
327  rw[MEM_MAP,pairTheory.EXISTS_PROD] >>
328  PROVE_TAC[]) >>
329fs[MEM_EL] >>
330pop_assum (assume_tac o SYM) >>
331qho_match_abbrev_tac `EL ($LEAST P) (MAP SND al) = v` >>
332`P n` by (
333  unabbrev_all_tac >> rw[EL_MAP] ) >>
334qspecl_then [`P`,`n`] mp_tac WhileTheory.LESS_LEAST >> rw[] >>
335numLib.LEAST_ELIM_TAC >>
336conj_tac >- (
337  qexists_tac `n` >> rw[] ) >>
338rw[] >>
339qmatch_rename_tac `EL m (MAP SND al) = v` >>
340`~(n < m)` by PROVE_TAC[] >>
341`m < LENGTH al` by DECIDE_TAC >>
342fs[EL_ALL_DISTINCT_EL_EQ] >>
343unabbrev_all_tac >> fs[] >>
344`m = n` by PROVE_TAC[] >>
345fs[EL_MAP]
346QED
347
348Theorem ALL_DISTINCT_fmap_to_alist_keys[simp]:
349  !fm. ALL_DISTINCT (MAP FST (fmap_to_alist fm))
350Proof
351qsuff_tac `!s fm. (s = FDOM fm) ==> ALL_DISTINCT (MAP FST (fmap_to_alist fm))`
352  >- rw[] >>
353ho_match_mp_tac SET_TO_LIST_IND >> rw[] >>
354fs[fmap_to_alist_def] >>
355Cases_on `FDOM fm = {}` >- rw[] >> fs[] >>
356rw[Once SET_TO_LIST_THM] >- (
357  rw[MEM_MAP,CHOICE_NOT_IN_REST,MAP_MAP_o,pairTheory.EXISTS_PROD] ) >>
358first_x_assum (qspec_then `fm \\ (CHOICE (FDOM fm))` mp_tac) >>
359rw[REST_DEF,MAP_MAP_o] >>
360qmatch_assum_abbrev_tac `ALL_DISTINCT (MAP f1 ls)` >>
361qmatch_abbrev_tac `ALL_DISTINCT (MAP f2 ls)` >>
362qsuff_tac `MAP f2 ls = MAP f1 ls` >- rw[] >>
363rw[MAP_EQ_f,Abbr`f1`,Abbr`f2`,Abbr`ls`,DOMSUB_FAPPLY_THM]
364QED
365
366Theorem fmap_to_alist_inj:
367  !f1 f2. (fmap_to_alist f1 = fmap_to_alist f2) ==> (f1 = f2)
368Proof
369rw[] >>
370qmatch_assum_abbrev_tac `af1 = af2` >>
371qsuff_tac `alist_to_fmap af1 = alist_to_fmap af2` >- metis_tac[fmap_to_alist_to_fmap] >>
372simp[GSYM fmap_EQ_THM,pairTheory.EXISTS_PROD,MEM_MAP,MEM_fmap_to_alist]
373QED
374
375Theorem fmap_to_alist_preserves_FDOM:
376  !fm1 fm2. (FDOM fm1 = FDOM fm2) ==> (MAP FST (fmap_to_alist fm1) = MAP FST (fmap_to_alist fm2))
377Proof
378qsuff_tac `
379  !s fm1 fm2. (FDOM fm1 = s) /\ (FDOM fm2 = s) ==>
380              (MAP FST (fmap_to_alist fm1) = MAP FST (fmap_to_alist fm2))`
381  >- rw[] >>
382ho_match_mp_tac SET_TO_LIST_IND >> rw[] >>
383fs[fmap_to_alist_def] >>
384Cases_on `FDOM fm2 = {}` >- rw[] >> fs[] >>
385`FDOM fm1 <> {}` by rw[] >>
386rw[Once SET_TO_LIST_THM,SimpLHS] >>
387rw[Once SET_TO_LIST_THM,SimpRHS] >>
388first_x_assum (qspec_then `fm1 \\ (CHOICE (FDOM fm2))` mp_tac) >>
389disch_then (qspec_then `fm2 \\ (CHOICE (FDOM fm2))` mp_tac) >>
390rw[REST_DEF,MAP_MAP_o] >>
391qmatch_assum_abbrev_tac `MAP f1 ls = MAP f2 ls` >>
392qmatch_abbrev_tac `MAP f3 ls = MAP f4 ls` >>
393qsuff_tac `(MAP f3 ls = MAP f1 ls) /\ (MAP f4 ls = MAP f2 ls)` >- rw[] >>
394rw[MAP_EQ_f,Abbr`f1`,Abbr`f2`,Abbr`f3`,Abbr`f4`,Abbr`ls`,DOMSUB_FAPPLY_THM]
395QED
396
397Theorem PERM_fmap_to_alist:
398  PERM (fmap_to_alist fm1) (fmap_to_alist fm2) = (fm1 = fm2)
399Proof
400rw[EQ_IMP_THM] >>
401qmatch_assum_abbrev_tac `PERM af1 af2` >>
402qsuff_tac `alist_to_fmap af1 = alist_to_fmap af2` >-
403  metis_tac[fmap_to_alist_to_fmap] >>
404`FDOM (alist_to_fmap af1) = FDOM (alist_to_fmap af2)` by (
405  rw[] >>
406  match_mp_tac PERM_LIST_TO_SET >>
407  match_mp_tac sortingTheory.PERM_MAP >>
408  rw[] ) >>
409qmatch_abbrev_tac `ff1 = ff2` >>
410qsuff_tac `fmap_to_alist ff1 = fmap_to_alist ff2` >-
411  metis_tac[fmap_to_alist_inj] >>
412Q.ISPEC_THEN `FST` match_mp_tac INJ_MAP_EQ >>
413reverse conj_tac >- (
414  match_mp_tac fmap_to_alist_preserves_FDOM >>
415  rw[Abbr`ff1`,Abbr`ff2`]) >>
416rw[INJ_DEF,Abbr`ff1`,Abbr`ff2`,MEM_fmap_to_alist_FLOOKUP] >>
417Cases_on `x` >> Cases_on `y` >> fs[] >>
418imp_res_tac ALOOKUP_MEM >>
419imp_res_tac MEM_PERM >>
420`ALL_DISTINCT (MAP FST af1) /\ ALL_DISTINCT (MAP FST af2)`
421  by rw[ALL_DISTINCT_fmap_to_alist_keys,Abbr`af1`,Abbr`af2`] >>
422fs[EL_ALL_DISTINCT_EL_EQ,MEM_EL,EL_MAP] >>
423rw[] >>
424qmatch_rename_tac `r1 = r2` >>
425qmatch_assum_rename_tac `(q,r1) = EL n1 afx` >>
426qmatch_assum_rename_tac `(q,r2) = EL n2 afy` >>
427rpt (qpat_x_assum `(X,Y) = EL N Z` (assume_tac o SYM)) >>
428`LENGTH afy = LENGTH afx` by rw[PERM_LENGTH] >> fs[] >>
429metis_tac[pairTheory.PAIR_EQ,pairTheory.FST]
430QED
431
432Theorem alist_to_fmap_PERM:
433  !l1 l2. PERM l1 l2 /\ ALL_DISTINCT (MAP FST l1) ==> (alist_to_fmap l1 = alist_to_fmap l2)
434Proof
435rpt strip_tac >>
436match_mp_tac (fst (EQ_IMP_RULE PERM_fmap_to_alist)) >>
437metis_tac[PERM_TRANS,PERM_SYM,ALL_DISTINCT_PERM,PERM_MAP,alist_to_fmap_to_alist_PERM]
438QED
439
440(*---------------------------------------------------------------------------*)
441(* Various lemmas from the CakeML project https://cakeml.org                 *)
442(*---------------------------------------------------------------------------*)
443
444Theorem ALOOKUP_ALL_DISTINCT_EL:
445    !ls n. n < LENGTH ls /\ ALL_DISTINCT (MAP FST ls) ==>
446           (ALOOKUP ls (FST (EL n ls)) = SOME (SND (EL n ls)))
447Proof
448  Induct >> simp[] >>
449  Cases >> simp[] >>
450  Cases >> simp[] >>
451  rw[] >> fs[MEM_MAP] >>
452  metis_tac[MEM_EL]
453QED
454
455Theorem ALOOKUP_ZIP_MAP_SND:
456    !l1 l2 k f.
457      (LENGTH l1 = LENGTH l2) ==>
458      (ALOOKUP (ZIP(l1,MAP f l2)) = OPTION_MAP f o (ALOOKUP (ZIP(l1,l2))))
459Proof
460  Induct >> simp[LENGTH_NIL,LENGTH_NIL_SYM,FUN_EQ_THM] >>
461  gen_tac >> Cases >> simp[] >> rw[] >> rw[]
462QED
463
464Theorem ALOOKUP_FILTER:
465    !ls x. ALOOKUP (FILTER (\(k,v). P k) ls) x =
466           if P x then ALOOKUP ls x else NONE
467Proof
468  Induct >> simp[] >> Cases >> simp[] >> rw[] >> fs[] >> metis_tac[]
469QED
470
471Theorem ALOOKUP_APPEND_same:
472    !l1 l2 l.
473      (ALOOKUP l1 = ALOOKUP l2) ==> (ALOOKUP (l1 ++ l) = ALOOKUP (l2 ++ l))
474Proof
475  rw[ALOOKUP_APPEND,FUN_EQ_THM]
476QED
477
478Theorem ALOOKUP_IN_FRANGE:
479    !ls k v. (ALOOKUP ls k = SOME v) ==> v IN FRANGE (alist_to_fmap ls)
480Proof
481  Induct >> simp[] >> Cases >> simp[] >> rw[] >>
482  simp[IN_FRANGE,DOMSUB_FAPPLY_THM] >>
483  full_simp_tac std_ss [Once(SYM (CONJUNCT1 ALOOKUP_EQ_FLOOKUP)),FLOOKUP_DEF] >>
484  fs[] >> METIS_TAC[]
485QED
486
487Theorem FRANGE_alist_to_fmap_SUBSET:
488  FRANGE (alist_to_fmap ls) SUBSET IMAGE SND (set ls)
489Proof
490srw_tac[DNF_ss][FRANGE_DEF,SUBSET_DEF,pairTheory.EXISTS_PROD] >>
491qmatch_assum_rename_tac `MEM z (MAP FST ls)` >>
492qexists_tac `z` >>
493match_mp_tac alist_to_fmap_FAPPLY_MEM >>
494rw[]
495QED
496
497Theorem IN_FRANGE_alist_to_fmap_suff:
498  (!v. MEM v (MAP SND ls) ==> P v) ==>
499  (!v. v IN FRANGE (alist_to_fmap ls) ==> P v)
500Proof
501rw[] >>
502imp_res_tac(SIMP_RULE(srw_ss())[SUBSET_DEF]FRANGE_alist_to_fmap_SUBSET) >>
503fs[MEM_MAP] >>
504PROVE_TAC[]
505QED
506
507Theorem alist_to_fmap_MAP_matchable:
508  !f1 f2 al mal v. INJ f1 (set (MAP FST al)) UNIV /\
509  (mal = MAP (\(x,y). (f1 x,f2 y)) al) /\
510  (v = MAP_KEYS f1 (f2 o_f alist_to_fmap al)) ==>
511  (alist_to_fmap mal = v)
512Proof
513METIS_TAC[alist_to_fmap_MAP]
514QED
515
516Theorem MAP_values_fmap_to_alist:
517  !f fm. MAP (\(k,v). (k, f v)) (fmap_to_alist fm) = fmap_to_alist (f o_f fm)
518Proof
519rw[fmap_to_alist_def,MAP_MAP_o,MAP_EQ_f]
520QED
521
522Theorem INJ_I[local]:
523  !s t. INJ I s t <=> s SUBSET t
524Proof
525SRW_TAC[][INJ_DEF,SUBSET_DEF]
526QED
527
528Theorem MAP_KEYS_I[simp]:
529  !fm. MAP_KEYS I fm = fm
530Proof
531rw[GSYM fmap_EQ_THM,MAP_KEYS_def,EXTENSION] >>
532metis_tac[MAP_KEYS_def,INJ_I,SUBSET_UNIV,combinTheory.I_THM]
533QED
534
535Theorem alist_to_fmap_MAP_values:
536  !f (al:('c,'a) alist).
537   alist_to_fmap (MAP (\(k,v). (k, f v)) al) = f o_f (alist_to_fmap al)
538Proof
539rw[] >>
540Q.ISPECL_THEN [`I:'c->'c`,`f`,`al`] match_mp_tac alist_to_fmap_MAP_matchable >>
541SRW_TAC[][INJ_DEF,SUBSET_DEF,MAP_KEYS_I]
542QED
543
544Theorem set_MAP_FST_fmap_to_alist[simp]:
545  set (MAP FST (fmap_to_alist fm)) = FDOM fm
546Proof
547METIS_TAC[fmap_to_alist_to_fmap,FDOM_alist_to_fmap]
548QED
549
550Theorem alookup_distinct_reverse:
551 !l k. ALL_DISTINCT (MAP FST l) ==> (ALOOKUP (REVERSE l) k = ALOOKUP l k)
552Proof
553 Induct_on `l` >>
554 rw [] >>
555 PairCases_on `h` >>
556 fs [] >>
557 BasicProvers.EVERY_CASE_TAC >>
558 fs [ALOOKUP_APPEND] >>
559 rw [] >>
560 BasicProvers.EVERY_CASE_TAC >>
561 fs [] >>
562 imp_res_tac ALOOKUP_MEM >>
563 fs [MEM_MAP] >>
564 metis_tac [FST]
565QED
566
567Theorem flookup_fupdate_list:
568 !l k m.
569  FLOOKUP (m |++ l) k =
570  case ALOOKUP (REVERSE l) k of
571     | SOME v => SOME v
572     | NONE => FLOOKUP m k
573Proof
574 ho_match_mp_tac ALOOKUP_ind >>
575 rw [FUPDATE_LIST_THM, ALOOKUP_def, FLOOKUP_UPDATE] >>
576 BasicProvers.FULL_CASE_TAC >>
577 fs [ALOOKUP_APPEND] >>
578 BasicProvers.EVERY_CASE_TAC >>
579 fs [FLOOKUP_UPDATE] >>
580 rw [] >>
581 imp_res_tac FLOOKUP_FUPDATE_LIST_ALOOKUP_NONE >>
582 imp_res_tac FLOOKUP_FUPDATE_LIST_ALOOKUP_SOME >>
583 fs [FLOOKUP_UPDATE]
584QED
585
586Theorem fupdate_list_funion:
587  !m l. m|++l = FUNION (FEMPTY |++l) m
588Proof
589 Induct_on `l`
590 >- rw [FUPDATE_LIST, FUNION_FEMPTY_1] >>
591 REWRITE_TAC [FUPDATE_LIST_THM] >>
592 rpt GEN_TAC >>
593 pop_assum (qspecl_then [`m|+h`] mp_tac) >>
594 rw [] >>
595 rw [FLOOKUP_EXT, FUN_EQ_THM, FLOOKUP_FUNION] >>
596 BasicProvers.EVERY_CASE_TAC >>
597 PairCases_on `h` >>
598 fs [FLOOKUP_UPDATE, flookup_fupdate_list] >>
599 BasicProvers.EVERY_CASE_TAC >>
600 fs []
601QED
602
603Theorem mem_to_flookup:
604 !x y l. ALL_DISTINCT (MAP FST l) /\ MEM (x,y) l ==> (FLOOKUP (FEMPTY |++ l) x = SOME y)
605Proof
606 Induct_on `l` >>
607 rw [] >>
608 fs [flookup_fupdate_list] >>
609 BasicProvers.EVERY_CASE_TAC >>
610 fs [ALOOKUP_APPEND] >>
611 BasicProvers.EVERY_CASE_TAC >>
612 fs [] >>
613 imp_res_tac ALOOKUP_MEM >>
614 imp_res_tac alookup_distinct_reverse >>
615 fs [] >>
616 res_tac >>
617 BasicProvers.EVERY_CASE_TAC >>
618 fs [MEM_MAP] >>
619 rw [] >>
620 metis_tac [FST]
621QED
622
623Theorem alookup_filter:
624 !f l x. ALOOKUP l x = ALOOKUP (FILTER (\(x',y). x = x') l) x
625Proof
626 Induct_on `l` >>
627 rw [ALOOKUP_def] >>
628 PairCases_on `h` >>
629 fs []
630QED
631
632Definition alist_range_def:
633alist_range m = { v | ?k. ALOOKUP m k = SOME v }
634End
635
636(* Sorting and permutation based stuff *)
637
638Theorem alookup_stable_sorted:
639 !R sort x l.
640  transitive R /\ total R /\
641  STABLE sort (inv_image R FST)
642  ==>
643  (ALOOKUP (sort (inv_image R FST) l) x = ALOOKUP l x)
644Proof
645 rw [] >>
646 ONCE_REWRITE_TAC [alookup_filter] >>
647 fs [STABLE_DEF, SORTS_DEF] >>
648 pop_assum (mp_tac o GSYM o Q.SPEC `(\(x',y). x = x')`) >>
649 rw [] >>
650 match_mp_tac (METIS_PROVE [] ``(x = x') ==> (f x y = f x' y)``) >>
651 pop_assum match_mp_tac >>
652 rw [] >>
653 PairCases_on `x'` >>
654 PairCases_on `y` >>
655 fs [transitive_def, total_def] >>
656 metis_tac []
657QED
658
659Theorem ALOOKUP_ALL_DISTINCT_PERM_same:
660    !l1 l2. ALL_DISTINCT (MAP FST l1) /\ PERM (MAP FST l1) (MAP FST l2) /\
661            (set l1 = set l2) ==> (ALOOKUP l1 = ALOOKUP l2)
662Proof
663  simp[EXTENSION] >>
664  rw[FUN_EQ_THM] >>
665  Cases_on`ALOOKUP l2 x` >- (
666    imp_res_tac ALOOKUP_FAILS >>
667    imp_res_tac MEM_PERM >>
668    fs[FORALL_PROD,MEM_MAP,EXISTS_PROD] >>
669    metis_tac[ALOOKUP_FAILS] ) >>
670  qmatch_assum_rename_tac`ALOOKUP l2 x = SOME p` >>
671  imp_res_tac ALOOKUP_MEM >>
672  `ALL_DISTINCT (MAP FST l2)` by (
673    metis_tac[ALL_DISTINCT_PERM]) >>
674  imp_res_tac ALOOKUP_ALL_DISTINCT_MEM >>
675  metis_tac[]
676QED
677
678Theorem FEVERY_alist_to_fmap:
679  EVERY P ls ==> FEVERY P (alist_to_fmap ls)
680Proof
681  Induct_on`ls` \\ simp[FORALL_PROD]
682  \\ rw[FEVERY_ALL_FLOOKUP,FLOOKUP_UPDATE]
683  \\ pop_assum mp_tac \\ rw[] \\ fs[]
684  \\ imp_res_tac ALOOKUP_MEM \\ fs[EVERY_MEM]
685QED
686
687Theorem ALL_DISTINCT_FEVERY_alist_to_fmap:
688  ALL_DISTINCT (MAP FST ls) ==>
689   (FEVERY P (alist_to_fmap ls) <=> EVERY P ls)
690Proof
691  Induct_on`ls` \\ simp[FORALL_PROD]
692  \\ rw[FEVERY_ALL_FLOOKUP,FLOOKUP_UPDATE] \\ fs[FEVERY_ALL_FLOOKUP]
693  \\ rw[EQ_IMP_THM]
694  \\ pop_assum mp_tac \\ rw[] \\ fs[MEM_MAP,EXISTS_PROD]
695  \\ metis_tac[ALOOKUP_MEM]
696QED
697
698Definition AFUPDKEY_def:
699  (AFUPDKEY k f [] = []) /\
700  (AFUPDKEY k f ((k',v)::rest) =
701     if k = k' then (k,f v)::rest
702     else (k',v) :: AFUPDKEY k f rest)
703End
704
705val AFUPDKEY_ind = theorem"AFUPDKEY_ind";
706
707Theorem AFUPDKEY_ALOOKUP:
708  ALOOKUP (AFUPDKEY k2 f al) k1 =
709    case ALOOKUP al k1 of
710        NONE => NONE
711      | SOME v => if k1 = k2 then SOME (f v) else SOME v
712Proof
713  Induct_on `al` >> simp[AFUPDKEY_def, FORALL_PROD] >> rw[]
714  >- (Cases_on `ALOOKUP al k1` >> simp[]) >>
715  simp[]
716QED
717
718Theorem MAP_FST_AFUPDKEY[simp]:
719  MAP FST (AFUPDKEY f k alist) = MAP FST alist
720Proof
721  Induct_on `alist` >> simp[AFUPDKEY_def, FORALL_PROD] >> rw[]
722QED
723
724Theorem AFUPDKEY_unchanged:
725  !k f alist.
726   (!v. (ALOOKUP alist k = SOME v) ==> (f v = v))
727   ==> (AFUPDKEY k f alist = alist)
728Proof
729  ho_match_mp_tac AFUPDKEY_ind
730  \\ rw[AFUPDKEY_def]
731QED
732
733Theorem AFUPDKEY_o:
734  AFUPDKEY k f1 (AFUPDKEY k f2 al) = AFUPDKEY k (f1 o f2) al
735Proof
736  Induct_on `al` >> simp[AFUPDKEY_def, FORALL_PROD] >>
737  rw[AFUPDKEY_def]
738QED
739
740Theorem AFUPDKEY_eq:
741  !k f1 l f2.
742   (!v. (ALOOKUP l k = SOME v) ==> (f1 v = f2 v))
743   ==> (AFUPDKEY k f1 l = AFUPDKEY k f2 l)
744Proof
745  ho_match_mp_tac AFUPDKEY_ind \\ rw[AFUPDKEY_def]
746QED
747
748Theorem AFUPDKEY_I:
749  AFUPDKEY n I = I
750Proof
751  simp[FUN_EQ_THM]
752  \\ Induct
753  \\ simp[AFUPDKEY_def,FORALL_PROD]
754QED
755
756Theorem LENGTH_AFUPDKEY[simp]:
757  !ls. LENGTH (AFUPDKEY k f ls) = LENGTH ls
758Proof
759  Induct \\ simp[AFUPDKEY_def]
760  \\ Cases \\ rw[AFUPDKEY_def]
761QED
762
763Theorem AFUPDKEY_comm:
764 !k1 k2 f1 f2 l. k1 <> k2 ==>
765  (AFUPDKEY k2 f2 (AFUPDKEY k1 f1 l) =
766   AFUPDKEY k1 f1 (AFUPDKEY k2 f2 l))
767Proof
768  Induct_on`l` >> rw[] >> fs[AFUPDKEY_def] >>
769  Cases_on`h`>> fs[AFUPDKEY_def] >>
770  CASE_TAC >> fs[AFUPDKEY_def] >>
771  CASE_TAC >> fs[AFUPDKEY_def]
772QED
773
774Definition ADELKEY_def:
775  ADELKEY k alist = FILTER (\p. FST p <> k) alist
776End
777
778Theorem MEM_ADELKEY[simp]:
779  !al. MEM (k1,v) (ADELKEY k2 al) <=> k1 <> k2 /\ MEM (k1,v) al
780Proof
781  Induct >> simp[ADELKEY_def, FORALL_PROD] >>
782  rw[MEM_FILTER] >> metis_tac[]
783QED
784
785Theorem ALOOKUP_ADELKEY:
786  !al. ALOOKUP (ADELKEY k1 al) k2
787       = if k1 = k2 then NONE else ALOOKUP al k2
788Proof
789  simp[ADELKEY_def] >> Induct >>
790  simp[FORALL_PROD] >> rw[] >> simp[]
791QED
792
793Theorem ADELKEY_AFUPDKEY_same[simp]:
794  !fd f ls. ADELKEY fd (AFUPDKEY fd f ls) = ADELKEY fd ls
795Proof
796  ho_match_mp_tac AFUPDKEY_ind
797  \\ rw[AFUPDKEY_def,ADELKEY_def]
798QED
799
800Theorem ADELKEY_unchanged:
801  !x ls. ((ADELKEY x ls = ls) <=> ~MEM x (MAP FST ls))
802Proof
803  simp[MEM_MAP, ADELKEY_def, FORALL_PROD] >>
804  Induct_on‘ls’ >> simp[AllCaseEqs(), FORALL_PROD] >>
805  ‘!P h. FILTER P ls <> h::ls’
806    by (rpt strip_tac >>
807        ‘LENGTH (h::ls) <= LENGTH ls’ by metis_tac[LENGTH_FILTER_LEQ] >>
808        fs[]) >>
809  simp[] >> metis_tac[]
810QED
811
812Theorem ADELKEY_AFUPDKEY:
813  !ls f x y. x <> y ==>
814    (ADELKEY x (AFUPDKEY y f ls) = (AFUPDKEY y f (ADELKEY x ls)))
815Proof
816  Induct >>  rw[ADELKEY_def,AFUPDKEY_def] >>
817  Cases_on`h` >> fs[AFUPDKEY_def] >> TRY CASE_TAC >> fs[ADELKEY_def]
818QED
819
820Theorem FLOOKUP_FUPDATE_LIST:
821  !xs k m. FLOOKUP (m |++ xs) k =
822           case ALOOKUP (REVERSE xs) k of
823           | NONE => FLOOKUP m k
824           | SOME x => SOME x
825Proof
826  Induct \\ fs [FUPDATE_LIST,pairTheory.FORALL_PROD,ALOOKUP_APPEND]
827  \\ fs [FLOOKUP_UPDATE] \\ rw [] \\ fs []
828  \\ Cases_on ‘ALOOKUP (REVERSE xs) k’ \\ fs []
829QED