author  wenzelm 
Thu, 16 Nov 2000 19:03:26 +0100  
changeset 10477  c21bee84cefe 
parent 10473  4f15b844fea6 
child 10483  eb93ace45a6e 
permissions  rwrr 
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 