author | Manuel Eberl <eberlm@in.tum.de> |
Fri, 29 Mar 2024 19:28:59 +0100 | |
changeset 80061 | 4c1347e172b1 |
parent 69593 | 3dda49e08b9d |
permissions | -rw-r--r-- |
35100
53754ec7360b
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents:
30738
diff
changeset
|
1 |
(* Title: HOL/Library/Quotient_Type.thy |
10483 | 2 |
Author: Markus Wenzel, TU Muenchen |
10250 | 3 |
*) |
4 |
||
59192 | 5 |
section \<open>Quotient types\<close> |
10250 | 6 |
|
35100
53754ec7360b
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents:
30738
diff
changeset
|
7 |
theory Quotient_Type |
30738 | 8 |
imports Main |
15131 | 9 |
begin |
10250 | 10 |
|
59192 | 11 |
text \<open>We introduce the notion of quotient types over equivalence relations |
12 |
via type classes.\<close> |
|
13 |
||
10250 | 14 |
|
59192 | 15 |
subsection \<open>Equivalence relations and quotient types\<close> |
10250 | 16 |
|
61585 | 17 |
text \<open>Type class \<open>equiv\<close> models equivalence relations |
18 |
\<open>\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool\<close>.\<close> |
|
10250 | 19 |
|
29608 | 20 |
class eqv = |
59192 | 21 |
fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50) |
10250 | 22 |
|
22390 | 23 |
class equiv = eqv + |
25062 | 24 |
assumes equiv_refl [intro]: "x \<sim> x" |
59192 | 25 |
and equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z" |
26 |
and equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x" |
|
27 |
begin |
|
10250 | 28 |
|
59192 | 29 |
lemma equiv_not_sym [sym]: "\<not> x \<sim> y \<Longrightarrow> \<not> y \<sim> x" |
10477 | 30 |
proof - |
59192 | 31 |
assume "\<not> x \<sim> y" |
32 |
then show "\<not> y \<sim> x" by (rule contrapos_nn) (rule equiv_sym) |
|
10477 | 33 |
qed |
34 |
||
59192 | 35 |
lemma not_equiv_trans1 [trans]: "\<not> x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> \<not> x \<sim> z" |
10477 | 36 |
proof - |
59192 | 37 |
assume "\<not> x \<sim> y" and "y \<sim> z" |
38 |
show "\<not> x \<sim> z" |
|
10477 | 39 |
proof |
40 |
assume "x \<sim> z" |
|
59192 | 41 |
also from \<open>y \<sim> z\<close> have "z \<sim> y" .. |
10477 | 42 |
finally have "x \<sim> y" . |
59192 | 43 |
with \<open>\<not> x \<sim> y\<close> show False by contradiction |
10477 | 44 |
qed |
45 |
qed |
|
46 |
||
59192 | 47 |
lemma not_equiv_trans2 [trans]: "x \<sim> y \<Longrightarrow> \<not> y \<sim> z \<Longrightarrow> \<not> x \<sim> z" |
10477 | 48 |
proof - |
59192 | 49 |
assume "\<not> y \<sim> z" |
50 |
then have "\<not> z \<sim> y" .. |
|
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" .. |
|
10477 | 56 |
qed |
57 |
||
59192 | 58 |
end |
10250 | 59 |
|
61585 | 60 |
text \<open>The quotient type \<open>'a quot\<close> consists of all \emph{equivalence |
69593 | 61 |
classes} over elements of the base type \<^typ>\<open>'a\<close>.\<close> |
59192 | 62 |
|
63 |
definition (in eqv) "quot = {{x. a \<sim> x} | a. True}" |
|
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
35100
diff
changeset
|
64 |
|
61260 | 65 |
typedef (overloaded) 'a quot = "quot :: 'a::eqv set set" |
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
35100
diff
changeset
|
66 |
unfolding quot_def by blast |
10250 | 67 |
|
68 |
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
|
18730 | 69 |
unfolding quot_def by blast |
10250 | 70 |
|
59192 | 71 |
lemma quotE [elim]: |
72 |
assumes "R \<in> quot" |
|
73 |
obtains a where "R = {x. a \<sim> x}" |
|
74 |
using assms unfolding quot_def by blast |
|
10250 | 75 |
|
59192 | 76 |
text \<open>Abstracted equivalence classes are the canonical representation of |
77 |
elements of a quotient type.\<close> |
|
10250 | 78 |
|
59192 | 79 |
definition "class" :: "'a::equiv \<Rightarrow> 'a quot" ("\<lfloor>_\<rfloor>") |
80 |
where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}" |
|
10250 | 81 |
|
10311 | 82 |
theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" |
10278 | 83 |
proof (cases A) |
59192 | 84 |
fix R |
85 |
assume R: "A = Abs_quot R" |
|
86 |
assume "R \<in> quot" |
|
87 |
then have "\<exists>a. R = {x. a \<sim> x}" by blast |
|
10278 | 88 |
with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
23373 | 89 |
then show ?thesis unfolding class_def . |
10250 | 90 |
qed |
91 |
||
59192 | 92 |
lemma quot_cases [cases type: quot]: |
93 |
obtains a where "A = \<lfloor>a\<rfloor>" |
|
18730 | 94 |
using quot_exhaust by blast |
10250 | 95 |
|
96 |
||
59192 | 97 |
subsection \<open>Equality on quotients\<close> |
10250 | 98 |
|
59192 | 99 |
text \<open>Equality of canonical quotient elements coincides with the original |
100 |
relation.\<close> |
|
10250 | 101 |
|
59192 | 102 |
theorem quot_equality [iff?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b" |
10285 | 103 |
proof |
104 |
assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
|
105 |
show "a \<sim> b" |
|
106 |
proof - |
|
107 |
from eq have "{x. a \<sim> x} = {x. b \<sim> x}" |
|
10551 | 108 |
by (simp only: class_def Abs_quot_inject quotI) |
10285 | 109 |
moreover have "a \<sim> a" .. |
110 |
ultimately have "a \<in> {x. b \<sim> x}" by blast |
|
23373 | 111 |
then have "b \<sim> a" by blast |
112 |
then show ?thesis .. |
|
10285 | 113 |
qed |
114 |
next |
|
10250 | 115 |
assume ab: "a \<sim> b" |
10285 | 116 |
show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
117 |
proof - |
|
118 |
have "{x. a \<sim> x} = {x. b \<sim> x}" |
|
119 |
proof (rule Collect_cong) |
|
120 |
fix x show "(a \<sim> x) = (b \<sim> x)" |
|
121 |
proof |
|
122 |
from ab have "b \<sim> a" .. |
|
123 |
also assume "a \<sim> x" |
|
124 |
finally show "b \<sim> x" . |
|
125 |
next |
|
126 |
note ab |
|
127 |
also assume "b \<sim> x" |
|
128 |
finally show "a \<sim> x" . |
|
129 |
qed |
|
10250 | 130 |
qed |
23373 | 131 |
then show ?thesis by (simp only: class_def) |
10250 | 132 |
qed |
133 |
qed |
|
134 |
||
135 |
||
59192 | 136 |
subsection \<open>Picking representing elements\<close> |
10250 | 137 |
|
59192 | 138 |
definition pick :: "'a::equiv quot \<Rightarrow> 'a" |
139 |
where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)" |
|
10250 | 140 |
|
10285 | 141 |
theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a" |
10250 | 142 |
proof (unfold pick_def) |
143 |
show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |
|
144 |
proof (rule someI2) |
|
145 |
show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. |
|
146 |
fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" |
|
59192 | 147 |
then have "a \<sim> x" .. |
148 |
then show "x \<sim> a" .. |
|
10250 | 149 |
qed |
150 |
qed |
|
151 |
||
10483 | 152 |
theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A" |
10250 | 153 |
proof (cases A) |
154 |
fix a assume a: "A = \<lfloor>a\<rfloor>" |
|
23373 | 155 |
then have "pick A \<sim> a" by (simp only: pick_equiv) |
156 |
then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. |
|
10250 | 157 |
with a show ?thesis by simp |
158 |
qed |
|
159 |
||
59192 | 160 |
text \<open>The following rules support canonical function definitions on quotient |
161 |
types (with up to two arguments). Note that the stripped-down version |
|
162 |
without additional conditions is sufficient most of the time.\<close> |
|
10285 | 163 |
|
10483 | 164 |
theorem quot_cond_function: |
59192 | 165 |
assumes eq: "\<And>X Y. P X Y \<Longrightarrow> f X Y \<equiv> g (pick X) (pick Y)" |
166 |
and cong: "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> |
|
167 |
\<Longrightarrow> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> \<Longrightarrow> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'" |
|
18372 | 168 |
and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" |
169 |
shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
|
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
170 |
proof - |
18372 | 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:) |
10505 | 172 |
also have "... = g a b" |
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset
|
173 |
proof (rule cong) |
10483 | 174 |
show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" .. |
175 |
moreover |
|
176 |
show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" .. |
|
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset
|
177 |
moreover |
23373 | 178 |
show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P) |
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset
|
179 |
ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:) |
10285 | 180 |
qed |
181 |
finally show ?thesis . |
|
182 |
qed |
|
183 |
||
10483 | 184 |
theorem quot_function: |
59192 | 185 |
assumes "\<And>X Y. f X Y \<equiv> g (pick X) (pick 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'" |
|
18372 | 187 |
shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
23394 | 188 |
using assms and TrueI |
18372 | 189 |
by (rule quot_cond_function) |
10285 | 190 |
|
10499 | 191 |
theorem quot_function': |
59192 | 192 |
"(\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)) \<Longrightarrow> |
193 |
(\<And>x x' y y'. x \<sim> x' \<Longrightarrow> y \<sim> y' \<Longrightarrow> g x y = g x' y') \<Longrightarrow> |
|
10499 | 194 |
f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
18372 | 195 |
by (rule quot_function) (simp_all only: quot_equality) |
10499 | 196 |
|
10250 | 197 |
end |