diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Map.thy
--- a/src/HOL/Map.thy Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Map.thy Sat Nov 11 18:41:08 2017 +0000
@@ -782,6 +782,20 @@
with * \x = (k, v)\ show ?case by simp
qed
+lemma eq_key_imp_eq_value:
+ "v1 = v2"
+ if "distinct (map fst xs)" "(k, v1) \ set xs" "(k, v2) \ set xs"
+proof -
+ from that have "inj_on fst (set xs)"
+ by (simp add: distinct_map)
+ moreover have "fst (k, v1) = fst (k, v2)"
+ by simp
+ ultimately have "(k, v1) = (k, v2)"
+ by (rule inj_onD) (fact that)+
+ then show ?thesis
+ by simp
+qed
+
lemma map_of_inject_set:
assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
shows "map_of xs = map_of ys \ set xs = set ys" (is "?lhs \ ?rhs")