Lines Matching refs:rw
81 Induct >> rw [invariant_def] >> metis_tac [insert_thm])
86 rw [bmap_of_def,invariant_insert_list]);
104 rw [] >> `good_cmp cmp` by metis_tac [eq_cmp_def]
105 >> rw [lookup_thm]
111 rw [insert_thm,lookup_thm,FLOOKUP_UPDATE]
120 rw [insert_thm,lookup_thm,FLOOKUP_UPDATE]
140 Induct >> rw [bmap_of_list_def] >> `good_cmp cmp` by metis_tac [eq_cmp_def]
142 >- (rw [Once lookup_insert_thm,invariant_insert_list,GSYM bmap_of_list_def]
150 Induct >> 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]
174 rw[INJ_DEF]);
180 Induct >> rw[map_keys_fupdate]);
184 Induct >> rw [map_keys_fupdate,FLOOKUP_UPDATE]);
189 Induct >> rw [to_fmap_def,FLOOKUP_UPDATE,FLOOKUP_FUNION,key_set_def,EXTENSION]
196 Induct >> rw [to_fmap_def,FLOOKUP_UPDATE,FLOOKUP_FUNION,key_set_def,EXTENSION,
203 Induct >> rw [MAP_KEYS_FEMPTY,map_keys_fupdate,FLOOKUP_UPDATE,FLOOKUP_FUNION]);
211 >> rw [MAP_KEYS_FEMPTY,map_keys_fupdate,FLOOKUP_UPDATE]
213 >> rw[]
220 rw [fmap_eq_flookup]
223 >- rw [to_fmap_empty,flookup_map_keys_empty]
225 >> rw[FLOOKUP_MAP_KEYS]
228 >> rw [GSYM eq_cmp_lookup_thm]
248 rw [fdom_def,lookup_bmap_of])
253 rw [frange_def,lookup_bmap_of,FRANGE_DEF]);