src/HOL/Map.thy
changeset 67051 e7e54a0b9197
parent 66584 acb02fa48ef3
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Map.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Map.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -782,6 +782,20 @@
     1.4    with * \<open>x = (k, v)\<close> show ?case by simp
     1.5  qed
     1.6  
     1.7 +lemma eq_key_imp_eq_value:
     1.8 +  "v1 = v2"
     1.9 +  if "distinct (map fst xs)" "(k, v1) \<in> set xs" "(k, v2) \<in> set xs"
    1.10 +proof -
    1.11 +  from that have "inj_on fst (set xs)"
    1.12 +    by (simp add: distinct_map)
    1.13 +  moreover have "fst (k, v1) = fst (k, v2)"
    1.14 +    by simp
    1.15 +  ultimately have "(k, v1) = (k, v2)"
    1.16 +    by (rule inj_onD) (fact that)+
    1.17 +  then show ?thesis
    1.18 +    by simp
    1.19 +qed
    1.20 +
    1.21  lemma map_of_inject_set:
    1.22    assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
    1.23    shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys" (is "?lhs \<longleftrightarrow> ?rhs")