moved lemmas map_of_eqI and map_of_eq_dom to Map.thy
authorhaftmann
Mon Sep 13 16:43:23 2010 +0200 (2010-09-13)
changeset 39379ab1b070aa412
parent 39378 df86b1b4ce10
child 39380 5a2662c1e44a
moved lemmas map_of_eqI and map_of_eq_dom to Map.thy
src/HOL/Library/AssocList.thy
src/HOL/Map.thy
     1.1 --- a/src/HOL/Library/AssocList.thy	Mon Sep 13 16:15:12 2010 +0200
     1.2 +++ b/src/HOL/Library/AssocList.thy	Mon Sep 13 16:43:23 2010 +0200
     1.3 @@ -701,37 +701,13 @@
     1.4    "Mapping.bulkload vs = Mapping (map (\<lambda>n. (n, vs ! n)) [0..<length vs])"
     1.5    by (rule mapping_eqI) (simp add: map_of_map_restrict fun_eq_iff)
     1.6  
     1.7 -lemma map_of_eqI: (*FIXME move to Map.thy*)
     1.8 -  assumes set_eq: "set (map fst xs) = set (map fst ys)"
     1.9 -  assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
    1.10 -  shows "map_of xs = map_of ys"
    1.11 -proof (rule ext)
    1.12 -  fix k show "map_of xs k = map_of ys k"
    1.13 -  proof (cases "map_of xs k")
    1.14 -    case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
    1.15 -    with set_eq have "k \<notin> set (map fst ys)" by simp
    1.16 -    then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
    1.17 -    with None show ?thesis by simp
    1.18 -  next
    1.19 -    case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
    1.20 -    with map_eq show ?thesis by auto
    1.21 -  qed
    1.22 -qed
    1.23 -
    1.24 -lemma map_of_eq_dom: (*FIXME move to Map.thy*)
    1.25 -  assumes "map_of xs = map_of ys"
    1.26 -  shows "fst ` set xs = fst ` set ys"
    1.27 -proof -
    1.28 -  from assms have "dom (map_of xs) = dom (map_of ys)" by simp
    1.29 -  then show ?thesis by (simp add: dom_map_of_conv_image_fst)
    1.30 -qed
    1.31 -
    1.32  lemma equal_Mapping [code]:
    1.33    "HOL.equal (Mapping xs) (Mapping ys) \<longleftrightarrow>
    1.34      (let ks = map fst xs; ls = map fst ys
    1.35      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))"
    1.36  proof -
    1.37 -  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)
    1.38 +  have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
    1.39 +    by (auto simp add: image_def intro!: bexI)
    1.40    show ?thesis
    1.41      by (auto intro!: map_of_eqI simp add: Let_def equal Mapping_def)
    1.42        (auto dest!: map_of_eq_dom intro: aux)
     2.1 --- a/src/HOL/Map.thy	Mon Sep 13 16:15:12 2010 +0200
     2.2 +++ b/src/HOL/Map.thy	Mon Sep 13 16:43:23 2010 +0200
     2.3 @@ -568,6 +568,31 @@
     2.4    "set xs = dom m \<Longrightarrow> map_of (map (\<lambda>k. (k, the (m k))) xs) = m"
     2.5    by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def)
     2.6  
     2.7 +lemma map_of_eqI:
     2.8 +  assumes set_eq: "set (map fst xs) = set (map fst ys)"
     2.9 +  assumes map_eq: "\<forall>k\<in>set (map fst xs). map_of xs k = map_of ys k"
    2.10 +  shows "map_of xs = map_of ys"
    2.11 +proof (rule ext)
    2.12 +  fix k show "map_of xs k = map_of ys k"
    2.13 +  proof (cases "map_of xs k")
    2.14 +    case None then have "k \<notin> set (map fst xs)" by (simp add: map_of_eq_None_iff)
    2.15 +    with set_eq have "k \<notin> set (map fst ys)" by simp
    2.16 +    then have "map_of ys k = None" by (simp add: map_of_eq_None_iff)
    2.17 +    with None show ?thesis by simp
    2.18 +  next
    2.19 +    case (Some v) then have "k \<in> set (map fst xs)" by (auto simp add: dom_map_of_conv_image_fst [symmetric])
    2.20 +    with map_eq show ?thesis by auto
    2.21 +  qed
    2.22 +qed
    2.23 +
    2.24 +lemma map_of_eq_dom:
    2.25 +  assumes "map_of xs = map_of ys"
    2.26 +  shows "fst ` set xs = fst ` set ys"
    2.27 +proof -
    2.28 +  from assms have "dom (map_of xs) = dom (map_of ys)" by simp
    2.29 +  then show ?thesis by (simp add: dom_map_of_conv_image_fst)
    2.30 +qed
    2.31 +
    2.32  
    2.33  subsection {* @{term [source] ran} *}
    2.34