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

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