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