1 (* Title: HOL/Library/Quotient_Type.thy |
1 (* Title: HOL/Library/Quotient_Type.thy |
2 Author: Markus Wenzel, TU Muenchen |
2 Author: Markus Wenzel, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 section {* Quotient types *} |
5 section \<open>Quotient types\<close> |
6 |
6 |
7 theory Quotient_Type |
7 theory Quotient_Type |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text \<open>We introduce the notion of quotient types over equivalence relations |
12 We introduce the notion of quotient types over equivalence relations |
12 via type classes.\<close> |
13 via type classes. |
|
14 *} |
|
15 |
13 |
16 subsection {* Equivalence relations and quotient types *} |
|
17 |
14 |
18 text {* |
15 subsection \<open>Equivalence relations and quotient types\<close> |
19 \medskip Type class @{text equiv} models equivalence relations @{text |
16 |
20 "\<sim> :: 'a => 'a => bool"}. |
17 text \<open>Type class @{text equiv} models equivalence relations |
21 *} |
18 @{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close> |
22 |
19 |
23 class eqv = |
20 class eqv = |
24 fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50) |
21 fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50) |
25 |
22 |
26 class equiv = eqv + |
23 class equiv = eqv + |
27 assumes equiv_refl [intro]: "x \<sim> x" |
24 assumes equiv_refl [intro]: "x \<sim> x" |
28 assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z" |
25 and equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z" |
29 assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x" |
26 and equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x" |
|
27 begin |
30 |
28 |
31 lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))" |
29 lemma equiv_not_sym [sym]: "\<not> x \<sim> y \<Longrightarrow> \<not> y \<sim> x" |
32 proof - |
30 proof - |
33 assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)" |
31 assume "\<not> x \<sim> y" |
34 by (rule contrapos_nn) (rule equiv_sym) |
32 then show "\<not> y \<sim> x" by (rule contrapos_nn) (rule equiv_sym) |
35 qed |
33 qed |
36 |
34 |
37 lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))" |
35 lemma not_equiv_trans1 [trans]: "\<not> x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> \<not> x \<sim> z" |
38 proof - |
36 proof - |
39 assume "\<not> (x \<sim> y)" and "y \<sim> z" |
37 assume "\<not> x \<sim> y" and "y \<sim> z" |
40 show "\<not> (x \<sim> z)" |
38 show "\<not> x \<sim> z" |
41 proof |
39 proof |
42 assume "x \<sim> z" |
40 assume "x \<sim> z" |
43 also from `y \<sim> z` have "z \<sim> y" .. |
41 also from \<open>y \<sim> z\<close> have "z \<sim> y" .. |
44 finally have "x \<sim> y" . |
42 finally have "x \<sim> y" . |
45 with `\<not> (x \<sim> y)` show False by contradiction |
43 with \<open>\<not> x \<sim> y\<close> show False by contradiction |
46 qed |
44 qed |
47 qed |
45 qed |
48 |
46 |
49 lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))" |
47 lemma not_equiv_trans2 [trans]: "x \<sim> y \<Longrightarrow> \<not> y \<sim> z \<Longrightarrow> \<not> x \<sim> z" |
50 proof - |
48 proof - |
51 assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" .. |
49 assume "\<not> y \<sim> z" |
52 also assume "x \<sim> y" then have "y \<sim> x" .. |
50 then have "\<not> z \<sim> y" .. |
53 finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" .. |
51 also |
|
52 assume "x \<sim> y" |
|
53 then have "y \<sim> x" .. |
|
54 finally have "\<not> z \<sim> x" . |
|
55 then show "\<not> x \<sim> z" .. |
54 qed |
56 qed |
55 |
57 |
56 text {* |
58 end |
57 \medskip The quotient type @{text "'a quot"} consists of all |
|
58 \emph{equivalence classes} over elements of the base type @{typ 'a}. |
|
59 *} |
|
60 |
59 |
61 definition "quot = {{x. a \<sim> x} | a::'a::eqv. True}" |
60 text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence |
|
61 classes} over elements of the base type @{typ 'a}.\<close> |
|
62 |
|
63 definition (in eqv) "quot = {{x. a \<sim> x} | a. True}" |
62 |
64 |
63 typedef 'a quot = "quot :: 'a::eqv set set" |
65 typedef 'a quot = "quot :: 'a::eqv set set" |
64 unfolding quot_def by blast |
66 unfolding quot_def by blast |
65 |
67 |
66 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
68 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
67 unfolding quot_def by blast |
69 unfolding quot_def by blast |
68 |
70 |
69 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" |
71 lemma quotE [elim]: |
70 unfolding quot_def by blast |
72 assumes "R \<in> quot" |
|
73 obtains a where "R = {x. a \<sim> x}" |
|
74 using assms unfolding quot_def by blast |
71 |
75 |
72 text {* |
76 text \<open>Abstracted equivalence classes are the canonical representation of |
73 \medskip Abstracted equivalence classes are the canonical |
77 elements of a quotient type.\<close> |
74 representation of elements of a quotient type. |
|
75 *} |
|
76 |
78 |
77 definition |
79 definition "class" :: "'a::equiv \<Rightarrow> 'a quot" ("\<lfloor>_\<rfloor>") |
78 "class" :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") where |
80 where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}" |
79 "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}" |
|
80 |
81 |
81 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" |
82 theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" |
82 proof (cases A) |
83 proof (cases A) |
83 fix R assume R: "A = Abs_quot R" |
84 fix R |
84 assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast |
85 assume R: "A = Abs_quot R" |
|
86 assume "R \<in> quot" |
|
87 then have "\<exists>a. R = {x. a \<sim> x}" by blast |
85 with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
88 with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
86 then show ?thesis unfolding class_def . |
89 then show ?thesis unfolding class_def . |
87 qed |
90 qed |
88 |
91 |
89 lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" |
92 lemma quot_cases [cases type: quot]: |
|
93 obtains a where "A = \<lfloor>a\<rfloor>" |
90 using quot_exhaust by blast |
94 using quot_exhaust by blast |
91 |
95 |
92 |
96 |
93 subsection {* Equality on quotients *} |
97 subsection \<open>Equality on quotients\<close> |
94 |
98 |
95 text {* |
99 text \<open>Equality of canonical quotient elements coincides with the original |
96 Equality of canonical quotient elements coincides with the original |
100 relation.\<close> |
97 relation. |
|
98 *} |
|
99 |
101 |
100 theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" |
102 theorem quot_equality [iff?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b" |
101 proof |
103 proof |
102 assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
104 assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
103 show "a \<sim> b" |
105 show "a \<sim> b" |
104 proof - |
106 proof - |
105 from eq have "{x. a \<sim> x} = {x. b \<sim> x}" |
107 from eq have "{x. a \<sim> x} = {x. b \<sim> x}" |
129 then show ?thesis by (simp only: class_def) |
131 then show ?thesis by (simp only: class_def) |
130 qed |
132 qed |
131 qed |
133 qed |
132 |
134 |
133 |
135 |
134 subsection {* Picking representing elements *} |
136 subsection \<open>Picking representing elements\<close> |
135 |
137 |
136 definition |
138 definition pick :: "'a::equiv quot \<Rightarrow> 'a" |
137 pick :: "'a::equiv quot => 'a" where |
139 where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)" |
138 "pick A = (SOME a. A = \<lfloor>a\<rfloor>)" |
|
139 |
140 |
140 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a" |
141 theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a" |
141 proof (unfold pick_def) |
142 proof (unfold pick_def) |
142 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |
143 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |
143 proof (rule someI2) |
144 proof (rule someI2) |
144 show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. |
145 show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. |
145 fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" |
146 fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" |
146 then have "a \<sim> x" .. then show "x \<sim> a" .. |
147 then have "a \<sim> x" .. |
|
148 then show "x \<sim> a" .. |
147 qed |
149 qed |
148 qed |
150 qed |
149 |
151 |
150 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A" |
152 theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A" |
151 proof (cases A) |
153 proof (cases A) |
153 then have "pick A \<sim> a" by (simp only: pick_equiv) |
155 then have "pick A \<sim> a" by (simp only: pick_equiv) |
154 then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. |
156 then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. |
155 with a show ?thesis by simp |
157 with a show ?thesis by simp |
156 qed |
158 qed |
157 |
159 |
158 text {* |
160 text \<open>The following rules support canonical function definitions on quotient |
159 \medskip The following rules support canonical function definitions |
161 types (with up to two arguments). Note that the stripped-down version |
160 on quotient types (with up to two arguments). Note that the |
162 without additional conditions is sufficient most of the time.\<close> |
161 stripped-down version without additional conditions is sufficient |
|
162 most of the time. |
|
163 *} |
|
164 |
163 |
165 theorem quot_cond_function: |
164 theorem quot_cond_function: |
166 assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)" |
165 assumes eq: "\<And>X Y. P X Y \<Longrightarrow> f X Y \<equiv> g (pick X) (pick Y)" |
167 and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> |
166 and cong: "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> |
168 ==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'" |
167 \<Longrightarrow> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> \<Longrightarrow> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'" |
169 and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" |
168 and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" |
170 shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
169 shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
171 proof - |
170 proof - |
172 from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) |
171 from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) |
173 also have "... = g a b" |
172 also have "... = g a b" |
181 qed |
180 qed |
182 finally show ?thesis . |
181 finally show ?thesis . |
183 qed |
182 qed |
184 |
183 |
185 theorem quot_function: |
184 theorem quot_function: |
186 assumes "!!X Y. f X Y == g (pick X) (pick Y)" |
185 assumes "\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)" |
187 and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'" |
186 and "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'" |
188 shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
187 shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
189 using assms and TrueI |
188 using assms and TrueI |
190 by (rule quot_cond_function) |
189 by (rule quot_cond_function) |
191 |
190 |
192 theorem quot_function': |
191 theorem quot_function': |
193 "(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
192 "(\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)) \<Longrightarrow> |
194 (!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==> |
193 (\<And>x x' y y'. x \<sim> x' \<Longrightarrow> y \<sim> y' \<Longrightarrow> g x y = g x' y') \<Longrightarrow> |
195 f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
194 f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
196 by (rule quot_function) (simp_all only: quot_equality) |
195 by (rule quot_function) (simp_all only: quot_equality) |
197 |
196 |
198 end |
197 end |