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