equal
deleted
inserted
replaced
48 |
48 |
49 lemma lookup_map [simp]: |
49 lemma lookup_map [simp]: |
50 "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f" |
50 "lookup (map f g m) = Option.map g \<circ> lookup m \<circ> f" |
51 by (simp add: map_def) |
51 by (simp add: map_def) |
52 |
52 |
53 type_lifting map |
53 type_lifting map: map |
54 by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity) |
54 by (simp_all add: mapping_eq_iff fun_eq_iff Option.map.compositionality Option.map.id) |
55 |
55 |
56 |
56 |
57 subsection {* Derived operations *} |
57 subsection {* Derived operations *} |
58 |
58 |
59 definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where |
59 definition keys :: "('a, 'b) mapping \<Rightarrow> 'a set" where |