author | wenzelm |
Fri, 17 Nov 2000 18:48:50 +0100 | |
changeset 10483 | eb93ace45a6e |
parent 10477 | c21bee84cefe |
child 10491 | e4a408728012 |
permissions | -rw-r--r-- |
10250 | 1 |
(* Title: HOL/Library/Quotient.thy |
2 |
ID: $Id$ |
|
10483 | 3 |
Author: Markus Wenzel, TU Muenchen |
10250 | 4 |
*) |
5 |
||
6 |
header {* |
|
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
7 |
\title{Quotient types} |
10483 | 8 |
\author{Markus Wenzel} |
10250 | 9 |
*} |
10 |
||
11 |
theory Quotient = Main: |
|
12 |
||
13 |
text {* |
|
10285 | 14 |
We introduce the notion of quotient types over equivalence relations |
15 |
via axiomatic type classes. |
|
10250 | 16 |
*} |
17 |
||
10285 | 18 |
subsection {* Equivalence relations and quotient types *} |
10250 | 19 |
|
20 |
text {* |
|
10390 | 21 |
\medskip Type class @{text equiv} models equivalence relations @{text |
22 |
"\<sim> :: 'a => 'a => bool"}. |
|
10250 | 23 |
*} |
24 |
||
10285 | 25 |
axclass eqv < "term" |
26 |
consts |
|
27 |
eqv :: "('a::eqv) => 'a => bool" (infixl "\<sim>" 50) |
|
10250 | 28 |
|
10285 | 29 |
axclass equiv < eqv |
10333 | 30 |
equiv_refl [intro]: "x \<sim> x" |
31 |
equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z" |
|
32 |
equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x" |
|
10250 | 33 |
|
10477 | 34 |
lemma not_equiv_sym [elim?]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))" |
35 |
proof - |
|
36 |
assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)" |
|
37 |
by (rule contrapos_nn) (rule equiv_sym) |
|
38 |
qed |
|
39 |
||
40 |
lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))" |
|
41 |
proof - |
|
42 |
assume "\<not> (x \<sim> y)" and yz: "y \<sim> z" |
|
43 |
show "\<not> (x \<sim> z)" |
|
44 |
proof |
|
45 |
assume "x \<sim> z" |
|
46 |
also from yz have "z \<sim> y" .. |
|
47 |
finally have "x \<sim> y" . |
|
48 |
thus False by contradiction |
|
49 |
qed |
|
50 |
qed |
|
51 |
||
52 |
lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))" |
|
53 |
proof - |
|
54 |
assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" .. |
|
55 |
also assume "x \<sim> y" hence "y \<sim> x" .. |
|
56 |
finally have "\<not> (z \<sim> x)" . thus "(\<not> x \<sim> z)" .. |
|
57 |
qed |
|
58 |
||
10250 | 59 |
text {* |
10285 | 60 |
\medskip The quotient type @{text "'a quot"} consists of all |
61 |
\emph{equivalence classes} over elements of the base type @{typ 'a}. |
|
10250 | 62 |
*} |
63 |
||
10392 | 64 |
typedef 'a quot = "{{x. a \<sim> x} | a::'a::eqv. True}" |
10250 | 65 |
by blast |
66 |
||
67 |
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
|
68 |
by (unfold quot_def) blast |
|
69 |
||
70 |
lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" |
|
71 |
by (unfold quot_def) blast |
|
72 |
||
73 |
text {* |
|
74 |
\medskip Abstracted equivalence classes are the canonical |
|
75 |
representation of elements of a quotient type. |
|
76 |
*} |
|
77 |
||
78 |
constdefs |
|
10285 | 79 |
equivalence_class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") |
10250 | 80 |
"\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" |
81 |
||
10311 | 82 |
theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" |
10278 | 83 |
proof (cases A) |
84 |
fix R assume R: "A = Abs_quot R" |
|
85 |
assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast |
|
86 |
with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
|
10285 | 87 |
thus ?thesis by (unfold equivalence_class_def) |
10250 | 88 |
qed |
89 |
||
10311 | 90 |
lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" |
91 |
by (insert quot_exhaust) blast |
|
10250 | 92 |
|
93 |
||
10285 | 94 |
subsection {* Equality on quotients *} |
10250 | 95 |
|
96 |
text {* |
|
10286 | 97 |
Equality of canonical quotient elements coincides with the original |
98 |
relation. |
|
10250 | 99 |
*} |
100 |
||
10477 | 101 |
theorem quot_equality: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" |
10285 | 102 |
proof |
103 |
assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
|
104 |
show "a \<sim> b" |
|
105 |
proof - |
|
106 |
from eq have "{x. a \<sim> x} = {x. b \<sim> x}" |
|
107 |
by (simp only: equivalence_class_def Abs_quot_inject quotI) |
|
108 |
moreover have "a \<sim> a" .. |
|
109 |
ultimately have "a \<in> {x. b \<sim> x}" by blast |
|
110 |
hence "b \<sim> a" by blast |
|
111 |
thus ?thesis .. |
|
112 |
qed |
|
113 |
next |
|
10250 | 114 |
assume ab: "a \<sim> b" |
10285 | 115 |
show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
116 |
proof - |
|
117 |
have "{x. a \<sim> x} = {x. b \<sim> x}" |
|
118 |
proof (rule Collect_cong) |
|
119 |
fix x show "(a \<sim> x) = (b \<sim> x)" |
|
120 |
proof |
|
121 |
from ab have "b \<sim> a" .. |
|
122 |
also assume "a \<sim> x" |
|
123 |
finally show "b \<sim> x" . |
|
124 |
next |
|
125 |
note ab |
|
126 |
also assume "b \<sim> x" |
|
127 |
finally show "a \<sim> x" . |
|
128 |
qed |
|
10250 | 129 |
qed |
10285 | 130 |
thus ?thesis by (simp only: equivalence_class_def) |
10250 | 131 |
qed |
132 |
qed |
|
133 |
||
10477 | 134 |
lemma quot_equalI [intro?]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
135 |
by (simp only: quot_equality) |
|
136 |
||
137 |
lemma quot_equalD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> b" |
|
138 |
by (simp only: quot_equality) |
|
139 |
||
140 |
lemma quot_not_equalI [intro?]: "\<not> (a \<sim> b) ==> \<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor>" |
|
141 |
by (simp add: quot_equality) |
|
142 |
||
143 |
lemma quot_not_equalD [dest?]: "\<lfloor>a\<rfloor> \<noteq> \<lfloor>b\<rfloor> ==> \<not> (a \<sim> b)" |
|
144 |
by (simp add: quot_equality) |
|
145 |
||
10250 | 146 |
|
10285 | 147 |
subsection {* Picking representing elements *} |
10250 | 148 |
|
149 |
constdefs |
|
10285 | 150 |
pick :: "'a::equiv quot => 'a" |
10250 | 151 |
"pick A == SOME a. A = \<lfloor>a\<rfloor>" |
152 |
||
10285 | 153 |
theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a" |
10250 | 154 |
proof (unfold pick_def) |
155 |
show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |
|
156 |
proof (rule someI2) |
|
157 |
show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. |
|
158 |
fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" |
|
10285 | 159 |
hence "a \<sim> x" .. thus "x \<sim> a" .. |
10250 | 160 |
qed |
161 |
qed |
|
162 |
||
10483 | 163 |
theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A" |
10250 | 164 |
proof (cases A) |
165 |
fix a assume a: "A = \<lfloor>a\<rfloor>" |
|
10285 | 166 |
hence "pick A \<sim> a" by (simp only: pick_equiv) |
167 |
hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. |
|
10250 | 168 |
with a show ?thesis by simp |
169 |
qed |
|
170 |
||
10285 | 171 |
text {* |
172 |
\medskip The following rules support canonical function definitions |
|
10483 | 173 |
on quotient types (with up to two arguments). Note that the |
174 |
stripped-down version without additional conditions is sufficient |
|
175 |
most of the time. |
|
10285 | 176 |
*} |
177 |
||
10483 | 178 |
theorem quot_cond_function: |
179 |
"(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
|
180 |
(!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y ==> P x' y' |
|
181 |
==> g x y = g x' y') ==> |
|
182 |
(!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y = P x' y') ==> |
|
183 |
P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
|
184 |
(is "PROP ?eq ==> PROP ?cong_g ==> PROP ?cong_P ==> _ ==> _") |
|
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
185 |
proof - |
10483 | 186 |
assume cong_g: "PROP ?cong_g" |
187 |
and cong_P: "PROP ?cong_P" and P: "P a b" |
|
188 |
assume "PROP ?eq" |
|
189 |
hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" |
|
190 |
by (simp only:) |
|
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
191 |
also have "\<dots> = g a b" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
192 |
proof (rule cong_g) |
10483 | 193 |
show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" .. |
194 |
moreover |
|
195 |
show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" .. |
|
196 |
ultimately |
|
197 |
have "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) = P a b" |
|
198 |
by (rule cong_P) |
|
199 |
also show \<dots> . |
|
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
200 |
finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" . |
10285 | 201 |
qed |
202 |
finally show ?thesis . |
|
203 |
qed |
|
204 |
||
10483 | 205 |
theorem quot_function: |
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
206 |
"(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
10483 | 207 |
(!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==> |
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
208 |
f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
209 |
proof - |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
210 |
case antecedent from this refl TrueI |
10483 | 211 |
show ?thesis by (rule quot_cond_function) |
10285 | 212 |
qed |
213 |
||
10250 | 214 |
end |