src/HOL/Library/AList_Mapping.thy
 changeset 57850 34382a1f37d6 parent 51161 6ed12ae3b3e1 child 58881 b9556a055632
equal inserted replaced
57849:6d8f97d555d8 57850:34382a1f37d6
`    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"`
`    68   by (fact equal_refl)`
`    68   by (fact equal_refl)`