--- a/src/HOL/Library/Mapping.thy Fri Feb 15 11:47:33 2013 +0100
+++ b/src/HOL/Library/Mapping.thy Fri Feb 15 11:47:34 2013 +0100
@@ -34,11 +34,13 @@
lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" is
"\<lambda>f g m. (Option.map g \<circ> m \<circ> f)" .
+
subsection {* Functorial structure *}
enriched_type map: map
by (transfer, auto simp add: fun_eq_iff Option.map.compositionality Option.map.id)+
+
subsection {* Derived operations *}
definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
@@ -67,6 +69,22 @@
definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
"map_default k v f m = map_entry k f (default k v m)"
+instantiation mapping :: (type, type) equal
+begin
+
+definition
+ "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
+
+instance proof
+qed (unfold equal_mapping_def, transfer, auto)
+
+end
+
+lemma [transfer_rule]:
+ "fun_rel cr_mapping (fun_rel cr_mapping HOL.iff) HOL.eq HOL.equal"
+ by (unfold equal) transfer_prover
+
+
subsection {* Properties *}
lemma lookup_update: "lookup (update k v m) k = Some v"
@@ -258,18 +276,8 @@
code_datatype empty update
-instantiation mapping :: (type, type) equal
-begin
-
-lift_definition equal_mapping :: "('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping \<Rightarrow> bool" is "op=" .
-
-instance proof
-qed(transfer, rule)
-
-end
-
-
hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size
replace default map_entry map_default tabulate bulkload map
end
+