summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/AssocList.thy

changeset 39379 | ab1b070aa412 |

parent 39302 | d7728f65b353 |

child 39921 | 45f95e4de831 |

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)