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