equal
deleted
inserted
replaced
10 text {* This was based on some existing fragments in the AFP-Collection framework. *} |
10 text {* This was based on some existing fragments in the AFP-Collection framework. *} |
11 |
11 |
12 subsection {* Type @{text "('key, 'value) alist" } *} |
12 subsection {* Type @{text "('key, 'value) alist" } *} |
13 |
13 |
14 typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}" |
14 typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}" |
15 morphisms impl_of Alist |
15 morphisms impl_of Alist |
16 by(rule exI[where x="[]"]) simp |
16 proof |
|
17 show "[] \<in> {xs. distinct (map fst xs)}" by simp |
|
18 qed |
17 |
19 |
18 lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys" |
20 lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys" |
19 by(simp add: impl_of_inject) |
21 by(simp add: impl_of_inject) |
20 |
22 |
21 lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys" |
23 lemma alist_eq_iff: "xs = ys \<longleftrightarrow> impl_of xs = impl_of ys" |