author | wenzelm |
Thu, 16 Nov 2000 19:03:26 +0100 | |
changeset 10477 | c21bee84cefe |
parent 10473 | 4f15b844fea6 |
child 10483 | eb93ace45a6e |
permissions | -rw-r--r-- |
10250 | 1 |
(* Title: HOL/Library/Quotient.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen |
|
4 |
*) |
|
5 |
||
6 |
header {* |
|
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
7 |
\title{Quotient types} |
10250 | 8 |
\author{Gertrud Bauer and Markus Wenzel} |
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 |
||
10285 | 163 |
theorem pick_inverse: "\<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 |
|
173 |
on quotient types. |
|
174 |
*} |
|
175 |
||
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
176 |
theorem quot_cond_function1: |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
177 |
"(!!X. f X == g (pick X)) ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
178 |
(!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x = g x') ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
179 |
(!!x x'. x \<sim> x' ==> P x = P x') ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
180 |
P a ==> f \<lfloor>a\<rfloor> = g a" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
181 |
proof - |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
182 |
assume cong_g: "!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x = g x'" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
183 |
assume cong_P: "!!x x'. x \<sim> x' ==> P x = P x'" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
184 |
assume P: "P a" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
185 |
assume "!!X. f X == g (pick X)" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
186 |
hence "f \<lfloor>a\<rfloor> = g (pick \<lfloor>a\<rfloor>)" by (simp only:) |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
187 |
also have "\<dots> = g a" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
188 |
proof (rule cong_g) |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
189 |
show "pick \<lfloor>a\<rfloor> \<sim> a" .. |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
190 |
hence "P (pick \<lfloor>a\<rfloor>) = P a" by (rule cong_P) |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
191 |
also note P |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
192 |
finally show "P (pick \<lfloor>a\<rfloor>)" . |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
193 |
qed |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
194 |
finally show ?thesis . |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
195 |
qed |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
196 |
|
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
197 |
theorem quot_function1: |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
198 |
"(!!X. f X == g (pick X)) ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
199 |
(!!x x'. x \<sim> x' ==> g x = g x') ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
200 |
f \<lfloor>a\<rfloor> = g a" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
201 |
proof - |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
202 |
case antecedent from this refl TrueI |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
203 |
show ?thesis by (rule quot_cond_function1) |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
204 |
qed |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
205 |
|
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
206 |
theorem quot_cond_operation1: |
10459 | 207 |
"(!!X. f X == \<lfloor>g (pick X)\<rfloor>) ==> |
208 |
(!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x \<sim> g x') ==> |
|
209 |
(!!x x'. x \<sim> x' ==> P x = P x') ==> |
|
210 |
P a ==> f \<lfloor>a\<rfloor> = \<lfloor>g a\<rfloor>" |
|
211 |
proof - |
|
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
212 |
assume defn: "!!X. f X == \<lfloor>g (pick X)\<rfloor>" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
213 |
assume "!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x \<sim> g x'" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
214 |
hence cong_g: "!!x x'. x \<sim> x' ==> P x ==> P x' ==> \<lfloor>g x\<rfloor> = \<lfloor>g x'\<rfloor>" .. |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
215 |
assume "!!x x'. x \<sim> x' ==> P x = P x'" and "P a" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
216 |
with defn cong_g show ?thesis by (rule quot_cond_function1) |
10459 | 217 |
qed |
218 |
||
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
219 |
theorem quot_operation1: |
10437 | 220 |
"(!!X. f X == \<lfloor>g (pick X)\<rfloor>) ==> |
221 |
(!!x x'. x \<sim> x' ==> g x \<sim> g x') ==> |
|
222 |
f \<lfloor>a\<rfloor> = \<lfloor>g a\<rfloor>" |
|
10285 | 223 |
proof - |
10459 | 224 |
case antecedent from this refl TrueI |
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
225 |
show ?thesis by (rule quot_cond_operation1) |
10459 | 226 |
qed |
227 |
||
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
228 |
theorem quot_cond_function2: |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
229 |
"(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
230 |
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
231 |
==> g x y = g x' y') ==> |
10459 | 232 |
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y') ==> |
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
233 |
P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
10459 | 234 |
proof - |
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
235 |
assume cong_g: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
236 |
==> g x y = g x' y'" |
10459 | 237 |
assume cong_P: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y'" |
238 |
assume P: "P a b" |
|
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
239 |
assume "!!X Y. f X Y == g (pick X) (pick Y)" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
240 |
hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
241 |
also have "\<dots> = g a b" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
242 |
proof (rule cong_g) |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
243 |
show "pick \<lfloor>a\<rfloor> \<sim> a" .. |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
244 |
moreover show "pick \<lfloor>b\<rfloor> \<sim> b" .. |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
245 |
ultimately have "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) = P a b" by (rule cong_P) |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
246 |
also show "P a b" . |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
247 |
finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" . |
10285 | 248 |
qed |
249 |
finally show ?thesis . |
|
250 |
qed |
|
251 |
||
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
252 |
theorem quot_function2: |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
253 |
"(!!X Y. f X Y == g (pick X) (pick Y)) ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
254 |
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
255 |
f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
256 |
proof - |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
257 |
case antecedent from this refl TrueI |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
258 |
show ?thesis by (rule quot_cond_function2) |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
259 |
qed |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
260 |
|
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
261 |
theorem quot_cond_operation2: |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
262 |
"(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
263 |
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
264 |
==> g x y \<sim> g x' y') ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
265 |
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y') ==> |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
266 |
P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g a b\<rfloor>" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
267 |
proof - |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
268 |
assume defn: "!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
269 |
assume "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
270 |
==> g x y \<sim> g x' y'" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
271 |
hence cong_g: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y ==> P x' y' |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
272 |
==> \<lfloor>g x y\<rfloor> = \<lfloor>g x' y'\<rfloor>" .. |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
273 |
assume "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y'" and "P a b" |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
274 |
with defn cong_g show ?thesis by (rule quot_cond_function2) |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
275 |
qed |
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
276 |
|
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
277 |
theorem quot_operation2: |
10437 | 278 |
"(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==> |
279 |
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y \<sim> g x' y') ==> |
|
280 |
f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g a b\<rfloor>" |
|
10285 | 281 |
proof - |
10459 | 282 |
case antecedent from this refl TrueI |
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset
|
283 |
show ?thesis by (rule quot_cond_operation2) |
10285 | 284 |
qed |
285 |
||
10437 | 286 |
text {* |
287 |
\medskip HOL's collection of overloaded standard operations is lifted |
|
288 |
to quotient types in the canonical manner. |
|
289 |
*} |
|
290 |
||
291 |
instance quot :: (zero) zero .. |
|
292 |
instance quot :: (plus) plus .. |
|
293 |
instance quot :: (minus) minus .. |
|
294 |
instance quot :: (times) times .. |
|
295 |
instance quot :: (inverse) inverse .. |
|
296 |
instance quot :: (power) power .. |
|
297 |
instance quot :: (number) number .. |
|
10459 | 298 |
instance quot :: (ord) ord .. |
10437 | 299 |
|
300 |
defs (overloaded) |
|
301 |
zero_quot_def: "0 == \<lfloor>0\<rfloor>" |
|
302 |
add_quot_def: "X + Y == \<lfloor>pick X + pick Y\<rfloor>" |
|
303 |
diff_quot_def: "X - Y == \<lfloor>pick X - pick Y\<rfloor>" |
|
304 |
minus_quot_def: "- X == \<lfloor>- pick X\<rfloor>" |
|
305 |
abs_quot_def: "abs X == \<lfloor>abs (pick X)\<rfloor>" |
|
306 |
mult_quot_def: "X * Y == \<lfloor>pick X * pick Y\<rfloor>" |
|
307 |
inverse_quot_def: "inverse X == \<lfloor>inverse (pick X)\<rfloor>" |
|
308 |
divide_quot_def: "X / Y == \<lfloor>pick X / pick Y\<rfloor>" |
|
309 |
power_quot_def: "X^n == \<lfloor>(pick X)^n\<rfloor>" |
|
310 |
number_of_quot_def: "number_of b == \<lfloor>number_of b\<rfloor>" |
|
10459 | 311 |
le_quot_def: "X \<le> Y == pick X \<le> pick Y" |
312 |
less_quot_def: "X < Y == pick X < pick Y" |
|
10437 | 313 |
|
10250 | 314 |
end |