1(*---------------------------------------------------------------------------*)
2(* The balanced_map theory constructs balanced binary trees as a model for   *)
3(* finite maps. Lookup of elements is done by use of a comparison function   *)
4(* returning elements in {Less, Equal, Greater}. As a consequence, if a node *)
5(* in the b-b-tree associates key k with value v, it is in actuality mapping *)
6(* v from any k' such that cmp k k' = Equal (cmp is the comparison fn). Thus *)
7(* the domain of such a map is made of *sets* of things equal to some key in *)
8(* the tree.                                                                 *)
9(*                                                                           *)
10(* The specifications of b-b-tree operations are phrased in terms of the     *)
11(* corresponding operations in finite_map theory. This seems to require a    *)
12(* map from ('a,'b) balanced_map to 'a|->'b. But that isn't possible by the  *)
13(* discussion above, and actually we have                                    *)
14(*                                                                           *)
15(*  to_fmap : ('a,'b) balanced_map -> (('a->bool) |-> 'b).                   *)
16(*                                                                           *)
17(* The major operations on b-b-trees are characterized in terms of to_fmap   *)
18(* in balanced_mapTheory. However, to support refinement scenarios, whereby  *)
19(* theorems phrased in terms of finite maps are converted to be over         *)
20(* b-b-trees, there is a need to translate from finite_map to b-b-trees.     *)
21(*                                                                           *)
22(* This translation is based on the requirement that                         *)
23(*                                                                           *)
24(*  (cmp x y = Equal) ==> (x = y)                                            *)
25(*                                                                           *)
26(* This is useful for settings where there is no derived equality at work,   *)
27(* for example regexp_compare.                                               *)
28(*---------------------------------------------------------------------------*)
29
30open HolKernel Parse boolLib bossLib lcsymtacs;
31open optionTheory listTheory pred_setTheory comparisonTheory
32     balanced_mapTheory finite_mapTheory;
33
34fun pat_elim q = Q.PAT_ASSUM q (K ALL_TAC);
35val comparison_distinct = TypeBase.distinct_of ``:ordering``
36val comparison_nchotomy = TypeBase.nchotomy_of ``:ordering``
37
38val SET_EQ_THM = Q.prove
39(`!s1 s2. (s1 = s2) = !x. s1 x = s2 x`,
40 METIS_TAC [EXTENSION,IN_DEF]);
41
42val LENGTH_NIL_SYM =
43   GEN_ALL (CONV_RULE (LHS_CONV SYM_CONV) (SPEC_ALL LENGTH_NIL));
44
45val list_ss = list_ss ++ rewrites [LENGTH_NIL, LENGTH_NIL_SYM];
46
47val set_ss = list_ss ++ pred_setLib.PRED_SET_ss ++ rewrites [SET_EQ_THM,IN_DEF]
48
49val _ = new_theory "eq_cmp_bmap";
50
51val eq_cmp_def =
52 Define
53  `eq_cmp cmp = good_cmp cmp /\ !x y. (cmp x y = Equal) <=> (x=y)`;
54
55val [frange_def,fdom_def] =
56 TotalDefn.multiDefine
57   `(fdom cmp bmap   = {a | ?x. lookup cmp a bmap = SOME x}) /\
58    (frange cmp bmap = {x | ?a. lookup cmp a bmap = SOME x})`;
59
60val bmap_of_list_def =
61  Define
62   `bmap_of_list cmp (fmap:'a|->'b) list =
63        FOLDR (\k bmap. balanced_map$insert cmp k (fmap ' k) bmap)
64              Tip list`;
65
66val fdom_bmap_def =
67 Define
68   `bmap_of cmp fmap = bmap_of_list cmp fmap (SET_TO_LIST (FDOM fmap))`;
69
70val bmap_of_def = Q.prove
71(`bmap_of cmp fmap =
72        FOLDR (\k bmap. balanced_map$insert cmp k (fmap ' k) bmap)
73              Tip
74              (SET_TO_LIST (FDOM fmap))`,
75 metis_tac [bmap_of_list_def, fdom_bmap_def]);
76
77val invariant_insert_list = Q.prove
78(`!(list:'a list) fmap cmp.
79   good_cmp cmp ==>
80   invariant cmp (FOLDR (\k bmap. balanced_map$insert cmp k (fmap ' k) bmap) Tip list)`,
81Induct >> rw [invariant_def] >> metis_tac [insert_thm])
82
83val invariant_bmap_of = Q.store_thm
84("invariant_bmap_of",
85 `!fmap cmp. good_cmp cmp ==> invariant cmp (bmap_of cmp fmap)`,
86 rw [bmap_of_def,invariant_insert_list]);
87
88val eq_cmp_singleton_keyset = Q.store_thm
89("eq_cmp_singleton_keyset",
90 `!cmp k. eq_cmp cmp ==> (key_set cmp k = {k})`,
91 rw_tac set_ss [eq_cmp_def,key_set_def]);
92
93val eq_cmp_keyset = Q.store_thm
94("eq_cmp_keyset",
95 `!cmp k j. eq_cmp cmp ==> (key_set cmp k j <=> (k=j))`,
96 rw_tac set_ss [eq_cmp_def,key_set_def] >> metis_tac[]);
97
98val eq_cmp_lookup_thm = Q.store_thm
99("eq_cmp_lookup_thm",
100 `!bmap cmp.
101    invariant cmp bmap /\ eq_cmp cmp
102   ==>
103       !x. lookup cmp x bmap = FLOOKUP (to_fmap cmp bmap) {x}`,
104 rw [] >> `good_cmp cmp` by metis_tac [eq_cmp_def]
105       >> rw [lookup_thm]
106       >> metis_tac [eq_cmp_singleton_keyset]);
107
108val lookup_insert_equal = Q.prove
109(`!bmap a b y. good_cmp cmp /\ invariant cmp bmap /\ (cmp a b = Equal)
110             ==> (lookup cmp b (insert cmp a y bmap) = SOME y)`,
111rw [insert_thm,lookup_thm,FLOOKUP_UPDATE]
112 >> fs [key_set_def,EXTENSION]
113 >> metis_tac [good_cmp_def,comparison_distinct]);
114
115val lookup_insert_notequal = Q.prove
116(`!bmap a b y.
117     good_cmp cmp /\ invariant cmp bmap /\
118     ((cmp a b = Less) \/ (cmp a b = Greater))
119    ==> (lookup cmp b (insert cmp a y bmap) = lookup cmp b bmap)`,
120rw [insert_thm,lookup_thm,FLOOKUP_UPDATE]
121 >> fs [key_set_def,EXTENSION]
122 >> metis_tac [good_cmp_def,comparison_distinct]);
123
124val lookup_insert_thm = Q.store_thm
125("lookup_insert_thm",
126 `!bmap a b y.
127     good_cmp cmp /\ invariant cmp bmap
128    ==>
129     (lookup cmp b (insert cmp a y bmap) =
130        if cmp a b = Equal
131          then SOME y
132          else lookup cmp b bmap)`,
133 metis_tac [lookup_insert_equal,lookup_insert_notequal,comparison_nchotomy]);
134
135val lookup_bmap_of_list = Q.prove
136(`!list fmap x.
137   eq_cmp cmp /\ MEM x list
138   ==>
139    (lookup cmp x (bmap_of_list cmp fmap list) = SOME (fmap ' x))`,
140Induct >> rw [bmap_of_list_def] >> `good_cmp cmp` by metis_tac [eq_cmp_def]
141 >- metis_tac [invariant_insert_list,good_cmp_thm,lookup_insert_equal]
142 >- (rw [Once lookup_insert_thm,invariant_insert_list,GSYM bmap_of_list_def]
143     >> metis_tac [eq_cmp_def]));
144
145val lookup_bmap_of_list_notin = Q.prove
146(`!list fmap x.
147   eq_cmp cmp /\ ~MEM x list
148   ==>
149    (lookup cmp x (bmap_of_list cmp fmap list) = NONE)`,
150Induct >> rw [bmap_of_list_def] >> `good_cmp cmp` by metis_tac [eq_cmp_def]
151 >- rw [lookup_def]
152 >- (rw [Once lookup_insert_thm,invariant_insert_list,GSYM bmap_of_list_def]
153     >> metis_tac [eq_cmp_def]));
154
155val lookup_bmap_of = Q.store_thm
156("lookup_bmap_of",
157 `!list fmap x.
158   eq_cmp cmp
159   ==>
160    (lookup cmp x (bmap_of cmp fmap) =
161       if x IN FDOM fmap
162          then SOME (fmap ' x)
163          else NONE)`,
164metis_tac [fdom_bmap_def,lookup_bmap_of_list,lookup_bmap_of_list_notin,
165           MEM_SET_TO_LIST,FDOM_FINITE]);
166
167val FLOOKUP_lookup = Q.store_thm
168("FLOOKUP_lookup",
169`!fmap. eq_cmp cmp ==> !x. FLOOKUP fmap x = lookup cmp x (bmap_of cmp fmap)`,
170 metis_tac [FLOOKUP_DEF,lookup_bmap_of]);
171
172val inj_lem = Q.prove
173(`!fmap x. INJ (\x.{x}) (x INSERT FDOM fmap) (UNIV:('a->bool)->bool)`,
174 rw[INJ_DEF]);
175
176val map_keys_fupdate = MATCH_MP (SPEC_ALL MAP_KEYS_FUPDATE) (SPEC_ALL inj_lem);
177
178val fdom_map_keys = Q.prove
179(`!fmap. FDOM(MAP_KEYS (\x. {x}) fmap) = IMAGE (\x. {x}) (FDOM fmap)`,
180 Induct >> rw[map_keys_fupdate]);
181
182val FLOOKUP_MAP_KEYS = Q.prove
183(`!fmap x. FLOOKUP (MAP_KEYS (\x. {x}) fmap) {x} = FLOOKUP fmap x`,
184 Induct >> rw [map_keys_fupdate,FLOOKUP_UPDATE]);
185
186val to_fmap_empty = Q.prove
187(`!(bmap:('a,'b)balanced_map) (cmp:'a->'a->ordering).
188     good_cmp cmp ==> (FLOOKUP (to_fmap cmp bmap) {} = NONE)`,
189Induct >> rw [to_fmap_def,FLOOKUP_UPDATE,FLOOKUP_FUNION,key_set_def,EXTENSION]
190       >> metis_tac [good_cmp_thm])
191
192val to_fmap_two = Q.prove
193(`!(bmap:('a,'b)balanced_map) (cmp:'a->'a->ordering) a b s.
194     eq_cmp cmp /\ a IN s /\ b IN s /\ ~(a=b) ==>
195      (FLOOKUP (to_fmap cmp bmap) s = NONE)`,
196Induct >> rw [to_fmap_def,FLOOKUP_UPDATE,FLOOKUP_FUNION,key_set_def,EXTENSION,
197              eq_cmp_def,GSYM IMP_DISJ_THM]
198       >- metis_tac []
199       >- (BasicProvers.CASE_TAC >> metis_tac[eq_cmp_def,NOT_SOME_NONE]));
200
201val flookup_map_keys_empty = Q.prove
202(`!fmap. FLOOKUP (MAP_KEYS (��x. {x}) fmap) {} = NONE`,
203Induct >> rw [MAP_KEYS_FEMPTY,map_keys_fupdate,FLOOKUP_UPDATE,FLOOKUP_FUNION]);
204
205val flookup_map_keys_two = Q.prove
206(`!fmap a b s.
207     ~(a=b) /\ a IN s /\ b IN s
208       ==>
209      (FLOOKUP (MAP_KEYS (��x. {x}) fmap) s = NONE)`,
210Induct
211  >> rw [MAP_KEYS_FEMPTY,map_keys_fupdate,FLOOKUP_UPDATE]
212  >> `FLOOKUP (MAP_KEYS (��x. {x}) fmap) s = NONE` by metis_tac[]
213  >> rw[]
214  >> metis_tac [IN_SING]);
215
216(*
217val fmap_bmap = Q.store_thm
218("fmap_bmap",
219 `!fmap cmp. eq_cmp cmp ==> (to_fmap cmp (bmap_of cmp fmap) = MAP_KEYS (\x. {x}) fmap)`,
220  rw [fmap_eq_flookup]
221   >> `good_cmp cmp` by metis_tac[eq_cmp_def]
222   >> STRIP_ASSUME_TAC (SPEC ``k:'a->bool`` SET_CASES)
223       >- rw [to_fmap_empty,flookup_map_keys_empty]
224       >- (STRIP_ASSUME_TAC (SPEC ``t:'a->bool`` SET_CASES)
225            >> rw[FLOOKUP_MAP_KEYS]
226               >- (pop_assum (K all_tac)
227                    >> `invariant cmp (bmap_of cmp fmap)` by metis_tac [invariant_bmap_of]
228                    >> rw [GSYM eq_cmp_lookup_thm]
229                    >> metis_tac [FLOOKUP_lookup])
230               >- metis_tac [IN_INSERT,flookup_map_keys_two,to_fmap_two]));
231*)
232
233val fdom_insert = Q.store_thm
234("fdom_insert",
235 `!bmap cmp k v.
236      eq_cmp cmp /\
237      invariant cmp bmap
238     ==>
239     (fdom cmp (insert cmp k v bmap) = $INSERT k (fdom cmp bmap))`,
240rw_tac set_ss [fdom_def]
241 >> `good_cmp cmp` by metis_tac [eq_cmp_def]
242 >> rw_tac set_ss [Once lookup_insert_thm]
243 >> metis_tac [eq_cmp_def]);
244
245val FDOM_fdom = Q.store_thm
246("FDOM_fdom",
247 `!fmap. eq_cmp cmp ==> (FDOM fmap = fdom cmp (bmap_of cmp fmap))`,
248rw [fdom_def,lookup_bmap_of])
249
250val FRANGE_frange = Q.store_thm
251("FRANGE_frange",
252 `!fmap cmp. eq_cmp cmp ==> (FRANGE fmap = frange cmp (bmap_of cmp fmap))`,
253 rw [frange_def,lookup_bmap_of,FRANGE_DEF]);
254
255
256val _ = export_theory();
257