equal
deleted
inserted
replaced
290 |
290 |
291 lemma is_empty_map_default [simp]: |
291 lemma is_empty_map_default [simp]: |
292 "\<not> is_empty (map_default k v f m)" |
292 "\<not> is_empty (map_default k v f m)" |
293 by (simp add: map_default_def) |
293 by (simp add: map_default_def) |
294 |
294 |
|
295 lemma keys_dom_lookup: |
|
296 "keys m = dom (Mapping.lookup m)" |
|
297 by transfer rule |
|
298 |
295 lemma keys_empty [simp]: |
299 lemma keys_empty [simp]: |
296 "keys empty = {}" |
300 "keys empty = {}" |
297 by transfer simp |
301 by transfer simp |
298 |
302 |
299 lemma keys_update [simp]: |
303 lemma keys_update [simp]: |