author | haftmann |

Mon Sep 13 16:43:23 2010 +0200 (2010-09-13) | |

changeset 39379 | ab1b070aa412 |

parent 39378 | df86b1b4ce10 |

child 39380 | 5a2662c1e44a |

moved lemmas map_of_eqI and map_of_eq_dom to Map.thy

src/HOL/Library/AssocList.thy | file | annotate | diff | revisions | |

src/HOL/Map.thy | file | annotate | diff | revisions |

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