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_mapper map |
53 type_lifting map |
54 by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity) |
54 by (auto intro!: mapping_eqI ext simp add: Option.map.compositionality Option.map.identity) |
55 |
55 |
56 |
56 |
57 subsection {* Derived operations *} |
57 subsection {* Derived operations *} |
58 |
58 |