1open HolKernel Parse boolLib bossLib; 2 3open finite_mapTheory sptreeTheory transferTheory pred_setTheory 4 5val _ = new_theory "fmsp"; 6 7val FMSP_def = Define��� 8 FMSP AN BC fm sp <=> 9 (* wf sp /\ *) !a n. AN a n ==> OPTREL BC (FLOOKUP fm a) (lookup n sp)���; 10 11val FMSP_FDOM = Q.store_thm( 12 "FMSP_FDOM", 13 ���(FMSP AN BC |==> (AN |==> (<=>))) FDOM domain���, 14 simp[FMSP_def, FUN_REL_def] >> rpt strip_tac >> res_tac >> 15 rename [���OPTREL BC (FLOOKUP fm a) (lookup n sp)���] >> pop_assum mp_tac >> 16 map_every Cases_on [���FLOOKUP fm a���, ���lookup n sp���] >> 17 simp[optionTheory.OPTREL_def] 18 >- (fs[sptreeTheory.lookup_NONE_domain, finite_mapTheory.flookup_thm] >> 19 fs[IN_DEF]) >> 20 ���n IN domain sp��� by metis_tac[sptreeTheory.domain_lookup] >> 21 fs[IN_DEF, finite_mapTheory.flookup_thm]) 22 23val FMSP_FEMPTY = Q.store_thm( 24 "FMSP_FEMPTY", 25 ���FMSP AN BC FEMPTY LN���, 26 simp[FMSP_def, lookup_def, optionTheory.OPTREL_def, wf_def]); 27 28val FMSP_FUPDATE = Q.store_thm( 29 "FMSP_FUPDATE", 30 ���bi_unique AN ==> 31 (FMSP AN BC |==> (AN ### BC) |==> FMSP AN BC) 32 FUPDATE 33 (\sp (n,v). insert n v sp)���, 34 simp[FMSP_def, FUN_REL_def, PAIR_REL_def, pairTheory.FORALL_PROD, 35 wf_insert] >> 36 rpt strip_tac >> 37 rename [���FLOOKUP (fm |+ (k1,v)) k2���, ���lookup m (insert n spv sp)���] >> 38 Cases_on ���k1 = k2��� >> fs[finite_mapTheory.FLOOKUP_DEF] 39 >- (���m = n��� by metis_tac[bi_unique_def, right_unique_def] >> 40 fs[optionTheory.OPTREL_def]) >> 41 simp[FAPPLY_FUPDATE_THM] >> 42 ���m <> n��� by metis_tac[bi_unique_def, left_unique_def] >> 43 simp[lookup_insert]); 44 45Theorem FMSP_surj : 46 bi_unique AN /\ surj BC ==> surj (FMSP AN BC) 47Proof 48 rw[surj_def, FMSP_def, left_unique_def, bi_unique_def, right_unique_def] >> 49 rename [���lookup _ sp���] >> 50 qexists_tac ��� 51 FUN_FMAP (\a. @b. BC b (THE (lookup (@n. AN a n) sp))) 52 { a | ?n. AN a n /\ n IN domain sp }��� >> 53 rw[optionTheory.OPTREL_def, finite_mapTheory.FLOOKUP_DEF] >> 54 qmatch_abbrev_tac ���_ NOTIN FDOM (FUN_FMAP FF FD) /\ _ \/ _��� >> 55 qabbrev_tac ���n2a = \n. @a. AN a n��� >> 56 ���!a n. AN a n ==> n2a n = a��� 57 by (rw[Abbr���n2a���] >> SELECT_ELIM_TAC >> metis_tac[]) >> 58 ���FINITE FD��� 59 by (���FD = IMAGE n2a { n | n IN domain sp /\ ?a. AN a n}��� 60 by (simp[Abbr���FD���, EXTENSION, PULL_EXISTS] >> metis_tac[]) >> 61 ���FINITE { n | n IN domain sp /\ ?a. AN a n}��� 62 suffices_by simp[IMAGE_FINITE] >> 63 irule SUBSET_FINITE_I >> qexists_tac ���domain sp��� >> 64 simp[SUBSET_DEF]) >> 65 csimp[FUN_FMAP_DEF] >> 66 ���!a. a IN FD <=> ?n. AN a n /\ n IN domain sp��� by simp[Abbr���FD���] >> 67 simp[] >> ���!m. AN a m <=> m = n��� by metis_tac[] >> 68 simp[lookup_NONE_domain] >> Cases_on ���n IN domain sp��� >> simp[] >> 69 pop_assum mp_tac >> simp[domain_lookup, PULL_EXISTS] >> 70 simp[Abbr���FF���] >> rw[] >> SELECT_ELIM_TAC >> metis_tac[] 71QED 72 73Theorem FMSP_bitotal: 74 bitotal BC /\ bi_unique AN ==> bitotal (FMSP AN BC) 75Proof 76 simp[bitotal_def, FMSP_surj] >> 77 simp[total_def, surj_def] >> strip_tac >> 78 ho_match_mp_tac fmap_INDUCT >> conj_tac >- metis_tac[FMSP_FEMPTY] >> 79 rw[] >> rename [���FMSP AN BC fm sp���, ���fm |+ (k,v)���] >> 80 fs[FMSP_def] >> 81 reverse (Cases_on ���?n. AN k n���) 82 >- (fs[FAPPLY_FUPDATE_THM, FLOOKUP_DEF] >> 83 ���!a n. AN a n ==> a <> k��� by metis_tac[] >> 84 asm_simp_tac (srw_ss() ++ SatisfySimps.SATISFY_ss) [] >> 85 metis_tac[]) >> 86 fs[] >> 87 ���(?v'. BC v v')��� 88 by metis_tac[bitotal_def, total_def] >> 89 fs[GSYM FMSP_def] >> 90 qexists_tac ���(\sp (n,v). insert n v sp) sp (n,v')��� >> 91 irule FUN_REL_COMB >> qexists_tac ���AN ### BC��� >> 92 conj_tac >- simp[PAIR_REL_def] >> 93 irule FUN_REL_COMB >> qexists_tac ���FMSP AN BC��� >> 94 simp[FMSP_FUPDATE] 95QED 96 97val FMSP_FUNION = Q.store_thm( 98 "FMSP_FUNION", 99 ���(FMSP AN BC |==> FMSP AN BC |==> FMSP AN BC) FUNION union���, 100 simp[FUN_REL_def, FMSP_def, FLOOKUP_DEF, lookup_union, FUNION_DEF] >> 101 rpt strip_tac >> 102 rename [���k IN FDOM fm1 \/ k IN FDOM fm2���, ���AN k n���, 103 ���option_CASE (lookup n sp1)���] >> 104 Cases_on ���k IN FDOM fm1��� >> simp[] 105 >- (Q_TAC (fn t => first_x_assum (qspecl_then [���k���, ���n���] mp_tac o 106 assert (free_in t o concl))) `fm1` >> 107 dsimp[optionTheory.OPTREL_def]) >> 108 Q_TAC (fn t => first_x_assum (qspecl_then [���k���, ���n���] mp_tac o 109 assert (free_in t o concl))) `fm1` >> 110 dsimp[optionTheory.OPTREL_def] >> 111 first_x_assum (qspecl_then [���k���, ���n���] mp_tac) >> 112 dsimp[optionTheory.OPTREL_def]) 113 114val FMSP_FDOMSUB = Q.store_thm( 115 "FMSP_FDOMSUB", 116 ���bi_unique AN ==> 117 (FMSP AN BC |==> AN |==> FMSP AN BC) (\\) (combin$C delete)���, 118 simp[FUN_REL_def, FMSP_def] >> rpt strip_tac >> 119 rename [���FLOOKUP (fm \\ k1) k2���, ���lookup m (delete n sp)���] >> 120 Cases_on ���k1 = k2��� >> simp[FLOOKUP_DEF, lookup_delete] 121 >- (���m = n��� by metis_tac[bi_unique_def, right_unique_def] >> 122 simp[optionTheory.OPTREL_def]) >> 123 ���m <> n��� by metis_tac[bi_unique_def, left_unique_def] >> 124 simp[DOMSUB_FAPPLY_THM] >> fs[FLOOKUP_DEF]); 125 126val _ = export_theory(); 127