equal
deleted
inserted
replaced
12 via type classes.\<close> |
12 via type classes.\<close> |
13 |
13 |
14 |
14 |
15 subsection \<open>Equivalence relations and quotient types\<close> |
15 subsection \<open>Equivalence relations and quotient types\<close> |
16 |
16 |
17 text \<open>Type class @{text equiv} models equivalence relations |
17 text \<open>Type class \<open>equiv\<close> models equivalence relations |
18 @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close> |
18 \<open>\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.\<close> |
19 |
19 |
20 class eqv = |
20 class eqv = |
21 fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50) |
21 fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50) |
22 |
22 |
23 class equiv = eqv + |
23 class equiv = eqv + |
55 then show "\<not> x \<sim> z" .. |
55 then show "\<not> x \<sim> z" .. |
56 qed |
56 qed |
57 |
57 |
58 end |
58 end |
59 |
59 |
60 text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence |
60 text \<open>The quotient type \<open>'a quot\<close> consists of all \emph{equivalence |
61 classes} over elements of the base type @{typ 'a}.\<close> |
61 classes} over elements of the base type @{typ 'a}.\<close> |
62 |
62 |
63 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}" |
63 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}" |
64 |
64 |
65 typedef (overloaded) 'a quot = "quot :: 'a::eqv set set" |
65 typedef (overloaded) 'a quot = "quot :: 'a::eqv set set" |