src/finite_map/alistScript.sml

81 Cases >> rw[MEM_fmap_to_alist,FLOOKUP_DEF])
86 rw[MEM_fmap_to_alist_FLOOKUP])
92 rw[fmap_to_alist_def,SET_TO_LIST_CARD])
123 REWRITE_TAC[FLOOKUP_DEF] >> rw[])
128 gen_tac >> Induct >- rw[FUN_EQ_THM] >> Cases >> rw[FUN_EQ_THM] >> rw[])
148 Induct >- rw[FUNION_FEMPTY_1] >>
149 Cases >> rw[FUNION_FUPDATE_1])
165 rw[] >> Cases_on `ALOOKUP l1 k` >> rw[ALOOKUP_prefix])
291 rw[ALOOKUP_LEAST_EL] >- (
292   rw[MEM_MAP,pairTheory.EXISTS_PROD] >>
298   unabbrev_all_tac >> rw[EL_MAP] ) >>
299 qspecl_then [`P`,`n`] mp_tac whileTheory.LESS_LEAST >> rw[] >>
302   qexists_tac `n` >> rw[] ) >>
303 rw[] >>
316   >- rw[] >>
317 ho_match_mp_tac SET_TO_LIST_IND >> rw[] >>
319 Cases_on `FDOM fm = {}` >- rw[] >> fs[] >>
320 rw[Once SET_TO_LIST_THM] >- (
321   rw[MEM_MAP,CHOICE_NOT_IN_REST,MAP_MAP_o,pairTheory.EXISTS_PROD] ) >>
323 rw[REST_DEF,MAP_MAP_o] >>
326 qsuff_tac `MAP f2 ls = MAP f1 ls` >- rw[] >>
327 rw[MAP_EQ_f,Abbr`f1`,Abbr`f2`,Abbr`ls`,DOMSUB_FAPPLY_THM])
333 rw[] >>
336 rw[GSYM fmap_EQ_THM,pairTheory.EXISTS_PROD,MEM_MAP,MEM_fmap_to_alist])
344   >- rw[] >>
345 ho_match_mp_tac SET_TO_LIST_IND >> rw[] >>
347 Cases_on `FDOM fm2 = {}` >- rw[] >> fs[] >>
348 `FDOM fm1 <> {}` by rw[] >>
349 rw[Once SET_TO_LIST_THM,SimpLHS] >>
350 rw[Once SET_TO_LIST_THM,SimpRHS] >>
353 rw[REST_DEF,MAP_MAP_o] >>
356 qsuff_tac `(MAP f3 ls = MAP f1 ls) /\ (MAP f4 ls = MAP f2 ls)` >- rw[] >>
357 rw[MAP_EQ_f,Abbr`f1`,Abbr`f2`,Abbr`f3`,Abbr`f4`,Abbr`ls`,DOMSUB_FAPPLY_THM])
362 rw[EQ_IMP_THM] >>
367   rw[] >>
370   rw[] ) >>
377   rw[Abbr`ff1`,Abbr`ff2`]) >>
378 rw[INJ_DEF,Abbr`ff1`,Abbr`ff2`,MEM_fmap_to_alist_FLOOKUP] >>
383   by rw[ALL_DISTINCT_fmap_to_alist_keys,Abbr`af1`,Abbr`af2`] >>
385 rw[] >>
390 `LENGTH afy = LENGTH afx` by rw[PERM_LENGTH] >> fs[] >>
410   rw[] >> fs[MEM_MAP] >>
418   gen_tac >> Cases >> simp[] >> rw[] >> rw[])
423   Induct >> simp[] >> Cases >> simp[] >> rw[] >> fs[] >> metis_tac[])
428   rw[ALOOKUP_APPEND,FUN_EQ_THM])
432   Induct >> simp[] >> Cases >> simp[] >> rw[] >>
444 rw[])
450 rw[] >>
466 rw[fmap_to_alist_def,MAP_MAP_o,MAP_EQ_f])
475 rw[GSYM fmap_EQ_THM,MAP_KEYS_def,EXTENSION] >>
482 rw[] >>
494  rw [] >>
499  rw [] >>
513  rw [FUPDATE_LIST_THM, ALOOKUP_def, FLOOKUP_UPDATE] >>
518  rw [] >>
526  >- rw [FUPDATE_LIST, FUNION_FEMPTY_1] >>
530  rw [] >>
531  rw [FLOOKUP_EXT, FUN_EQ_THM, FLOOKUP_FUNION] >>
541  rw [] >>
553  rw [] >>
559  rw [ALOOKUP_def] >>
574  rw [] >>
578  rw [] >>
581  rw [] >>
591   rw[FUN_EQ_THM] >>