equal
deleted
inserted
replaced
57 (let ks = map fst xs; ls = map fst ys |
57 (let ks = map fst xs; ls = map fst ys |
58 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))" |
58 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))" |
59 proof - |
59 proof - |
60 have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" |
60 have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs" |
61 by (auto simp add: image_def intro!: bexI) |
61 by (auto simp add: image_def intro!: bexI) |
62 show ?thesis apply transfer |
62 show ?thesis apply transfer |
63 by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux) |
63 by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux) |
64 qed |
64 qed |
65 |
65 |
66 lemma [code nbe]: |
66 lemma [code nbe]: |
67 "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" |
67 "HOL.equal (x :: ('a, 'b) mapping) x \<longleftrightarrow> True" |