equal
deleted
inserted
replaced
37 "Mapping.delete k (Mapping t) = Mapping (delete k t)" |
37 "Mapping.delete k (Mapping t) = Mapping (delete k t)" |
38 by (transfer fixing: t) simp |
38 by (transfer fixing: t) simp |
39 |
39 |
40 lemma map_entry_Mapping [code]: |
40 lemma map_entry_Mapping [code]: |
41 "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)" |
41 "Mapping.map_entry k f (Mapping t) = Mapping (map_entry k f t)" |
42 apply (transfer fixing: t) by (case_tac "lookup t k") auto |
42 by (transfer fixing: t, case_tac "lookup t k") auto |
43 |
43 |
44 lemma keys_Mapping [code]: |
44 lemma keys_Mapping [code]: |
45 "Mapping.keys (Mapping t) = set (keys t)" |
45 "Mapping.keys (Mapping t) = set (keys t)" |
46 by (transfer fixing: t) (simp add: lookup_keys) |
46 by (transfer fixing: t) (simp add: lookup_keys) |
47 |
47 |