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

src/HOL/Map.thy

changeset 39379 | ab1b070aa412 |

parent 39302 | d7728f65b353 |

child 39992 | f225a499a8e5 |

1.1 --- a/src/HOL/Map.thy Mon Sep 13 16:15:12 2010 +0200 1.2 +++ b/src/HOL/Map.thy Mon Sep 13 16:43:23 2010 +0200 1.3 @@ -568,6 +568,31 @@ 1.4 "set xs = dom m \<Longrightarrow> map_of (map (\<lambda>k. (k, the (m k))) xs) = m" 1.5 by (rule ext) (auto simp add: map_of_map_restrict restrict_map_def) 1.6 1.7 +lemma map_of_eqI: 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: 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 1.33 subsection {* @{term [source] ran} *} 1.34