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