# HG changeset patch
# User haftmann
# Date 1284389003 -7200
# Node ID ab1b070aa412ab5082e53bb9a6e250c1b7c8b0b9
# Parent  df86b1b4ce10d29fb459eab09ca664cdb26dcd76
moved lemmas map_of_eqI and map_of_eq_dom to Map.thy

diff -r df86b1b4ce10 -r ab1b070aa412 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Mon Sep 13 16:15:12 2010 +0200
+++ b/src/HOL/Library/AssocList.thy	Mon Sep 13 16:43:23 2010 +0200
@@ -701,37 +701,13 @@
   "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
   by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
 
-lemma map_of_eqI: (*FIXME move to Map.thy*)
-  assumes set_eq: "set (map fst xs) = set (map fst ys)"
-  assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
-  shows "map_of xs = map_of ys"
-proof (rule ext)
-  fix k show "map_of xs k = map_of ys k"
-  proof (cases "map_of xs k")
-    case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
-    with set_eq have "k \<notin> set (map fst ys)" by simp
-    then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
-    with None show ?thesis by simp
-  next
-    case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
-    with map_eq show ?thesis by auto
-  qed
-qed
-
-lemma map_of_eq_dom: (*FIXME move to Map.thy*)
-  assumes "map_of xs = map_of ys"
-  shows "fst ` set xs = fst ` set ys"
-proof -
-  from assms have "dom (map_of xs) = dom (map_of ys)" by simp
-  then show ?thesis by (simp add: dom_map_of_conv_image_fst)
-qed
-
 lemma equal_Mapping [code]:
   "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
     (let ks = map fst xs; ls = map fst ys
     in (\<forall>l\<in>set ls. l \<in> set ks) \<and> (\<forall>k\<in>set ks. k \<in> set ls \<and> map_of xs k = map_of ys k))"
 proof -
-  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" by (auto simp add: image_def intro!: bexI)
+  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
+    by (auto simp add: image_def intro!: bexI)
   show ?thesis
     by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
       (auto dest!: map_of_eq_dom intro: aux)
diff -r df86b1b4ce10 -r ab1b070aa412 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Mon Sep 13 16:15:12 2010 +0200
+++ b/src/HOL/Map.thy	Mon Sep 13 16:43:23 2010 +0200
@@ -568,6 +568,31 @@
   "set xs = dom m \<Longrightarrow> map_of (map (\<lambda>k. (k, the (m k))) xs) = m"
   by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def)
 
+lemma map_of_eqI:
+  assumes set_eq: "set (map fst xs) = set (map fst ys)"
+  assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
+  shows "map_of xs = map_of ys"
+proof (rule ext)
+  fix k show "map_of xs k = map_of ys k"
+  proof (cases "map_of xs k")
+    case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
+    with set_eq have "k \<notin> set (map fst ys)" by simp
+    then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
+    with None show ?thesis by simp
+  next
+    case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
+    with map_eq show ?thesis by auto
+  qed
+qed
+
+lemma map_of_eq_dom:
+  assumes "map_of xs = map_of ys"
+  shows "fst ` set xs = fst ` set ys"
+proof -
+  from assms have "dom (map_of xs) = dom (map_of ys)" by simp
+  then show ?thesis by (simp add: dom_map_of_conv_image_fst)
+qed
+
 
 subsection {* @{term [source] ran} *}