src/HOL/Library/AList_Mapping.thy
 changeset 51161 6ed12ae3b3e1 parent 49929 70300f1b6835 child 57850 34382a1f37d6
equal inserted replaced
51160:599ff65b85e2 51161:6ed12ae3b3e1
`    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"`