summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Mon, 13 Sep 2010 16:43:23 +0200 | |

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 | comparison | revisions | |

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

--- 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)

--- 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} *}