author  wenzelm 
Wed, 15 Nov 2000 19:43:42 +0100  
changeset 10473  4f15b844fea6 
parent 10459  df3cd3e76046 
child 10477  c21bee84cefe 
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 

34 
text {* 

10285  35 
\medskip The quotient type @{text "'a quot"} consists of all 
36 
\emph{equivalence classes} over elements of the base type @{typ 'a}. 

10250  37 
*} 
38 

10392  39 
typedef 'a quot = "{{x. a \<sim> x}  a::'a::eqv. True}" 
10250  40 
by blast 
41 

42 
lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" 

43 
by (unfold quot_def) blast 

44 

45 
lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" 

46 
by (unfold quot_def) blast 

47 

48 
text {* 

49 
\medskip Abstracted equivalence classes are the canonical 

50 
representation of elements of a quotient type. 

51 
*} 

52 

53 
constdefs 

10285  54 
equivalence_class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") 
10250  55 
"\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" 
56 

10311  57 
theorem quot_exhaust: "\<exists>a. A = \<lfloor>a\<rfloor>" 
10278  58 
proof (cases A) 
59 
fix R assume R: "A = Abs_quot R" 

60 
assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast 

61 
with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast 

10285  62 
thus ?thesis by (unfold equivalence_class_def) 
10250  63 
qed 
64 

10311  65 
lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" 
66 
by (insert quot_exhaust) blast 

10250  67 

68 

10285  69 
subsection {* Equality on quotients *} 
10250  70 

71 
text {* 

10286  72 
Equality of canonical quotient elements coincides with the original 
73 
relation. 

10250  74 
*} 
75 

10459  76 
theorem equivalence_class_iff [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" 
10285  77 
proof 
78 
assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" 

79 
show "a \<sim> b" 

80 
proof  

81 
from eq have "{x. a \<sim> x} = {x. b \<sim> x}" 

82 
by (simp only: equivalence_class_def Abs_quot_inject quotI) 

83 
moreover have "a \<sim> a" .. 

84 
ultimately have "a \<in> {x. b \<sim> x}" by blast 

85 
hence "b \<sim> a" by blast 

86 
thus ?thesis .. 

87 
qed 

88 
next 

10250  89 
assume ab: "a \<sim> b" 
10285  90 
show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" 
91 
proof  

92 
have "{x. a \<sim> x} = {x. b \<sim> x}" 

93 
proof (rule Collect_cong) 

94 
fix x show "(a \<sim> x) = (b \<sim> x)" 

95 
proof 

96 
from ab have "b \<sim> a" .. 

97 
also assume "a \<sim> x" 

98 
finally show "b \<sim> x" . 

99 
next 

100 
note ab 

101 
also assume "b \<sim> x" 

102 
finally show "a \<sim> x" . 

103 
qed 

10250  104 
qed 
10285  105 
thus ?thesis by (simp only: equivalence_class_def) 
10250  106 
qed 
107 
qed 

108 

109 

10285  110 
subsection {* Picking representing elements *} 
10250  111 

112 
constdefs 

10285  113 
pick :: "'a::equiv quot => 'a" 
10250  114 
"pick A == SOME a. A = \<lfloor>a\<rfloor>" 
115 

10285  116 
theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a" 
10250  117 
proof (unfold pick_def) 
118 
show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" 

119 
proof (rule someI2) 

120 
show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. 

121 
fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" 

10285  122 
hence "a \<sim> x" .. thus "x \<sim> a" .. 
10250  123 
qed 
124 
qed 

125 

10285  126 
theorem pick_inverse: "\<lfloor>pick A\<rfloor> = A" 
10250  127 
proof (cases A) 
128 
fix a assume a: "A = \<lfloor>a\<rfloor>" 

10285  129 
hence "pick A \<sim> a" by (simp only: pick_equiv) 
130 
hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. 

10250  131 
with a show ?thesis by simp 
132 
qed 

133 

10285  134 
text {* 
135 
\medskip The following rules support canonical function definitions 

136 
on quotient types. 

137 
*} 

138 

10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

139 
theorem quot_cond_function1: 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

140 
"(!!X. f X == g (pick X)) ==> 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

141 
(!!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

142 
(!!x x'. x \<sim> x' ==> P x = P x') ==> 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

143 
P a ==> f \<lfloor>a\<rfloor> = g a" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

144 
proof  
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

145 
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

146 
assume cong_P: "!!x x'. x \<sim> x' ==> P x = P x'" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

147 
assume P: "P a" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

148 
assume "!!X. f X == g (pick X)" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

149 
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

150 
also have "\<dots> = g a" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

151 
proof (rule cong_g) 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

152 
show "pick \<lfloor>a\<rfloor> \<sim> a" .. 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

153 
hence "P (pick \<lfloor>a\<rfloor>) = P a" by (rule cong_P) 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

154 
also note P 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

155 
finally show "P (pick \<lfloor>a\<rfloor>)" . 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

156 
qed 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

157 
finally show ?thesis . 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

158 
qed 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

159 

4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

160 
theorem quot_function1: 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

161 
"(!!X. f X == g (pick X)) ==> 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

162 
(!!x x'. x \<sim> x' ==> g x = g x') ==> 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

163 
f \<lfloor>a\<rfloor> = g a" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

164 
proof  
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

165 
case antecedent from this refl TrueI 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

166 
show ?thesis by (rule quot_cond_function1) 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

167 
qed 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

168 

4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

169 
theorem quot_cond_operation1: 
10459  170 
"(!!X. f X == \<lfloor>g (pick X)\<rfloor>) ==> 
171 
(!!x x'. x \<sim> x' ==> P x ==> P x' ==> g x \<sim> g x') ==> 

172 
(!!x x'. x \<sim> x' ==> P x = P x') ==> 

173 
P a ==> f \<lfloor>a\<rfloor> = \<lfloor>g a\<rfloor>" 

174 
proof  

10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

175 
assume defn: "!!X. f X == \<lfloor>g (pick X)\<rfloor>" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

176 
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

177 
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

178 
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

179 
with defn cong_g show ?thesis by (rule quot_cond_function1) 
10459  180 
qed 
181 

10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

182 
theorem quot_operation1: 
10437  183 
"(!!X. f X == \<lfloor>g (pick X)\<rfloor>) ==> 
184 
(!!x x'. x \<sim> x' ==> g x \<sim> g x') ==> 

185 
f \<lfloor>a\<rfloor> = \<lfloor>g a\<rfloor>" 

10285  186 
proof  
10459  187 
case antecedent from this refl TrueI 
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

188 
show ?thesis by (rule quot_cond_operation1) 
10459  189 
qed 
190 

10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

191 
theorem quot_cond_function2: 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

192 
"(!!X Y. f X Y == g (pick X) (pick Y)) ==> 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

193 
(!!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

194 
==> g x y = g x' y') ==> 
10459  195 
(!!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

196 
P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" 
10459  197 
proof  
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

198 
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

199 
==> g x y = g x' y'" 
10459  200 
assume cong_P: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> P x y = P x' y'" 
201 
assume P: "P a b" 

10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

202 
assume "!!X Y. f X Y == g (pick X) (pick Y)" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

203 
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

204 
also have "\<dots> = g a b" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

205 
proof (rule cong_g) 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

206 
show "pick \<lfloor>a\<rfloor> \<sim> a" .. 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

207 
moreover show "pick \<lfloor>b\<rfloor> \<sim> b" .. 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

208 
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

209 
also show "P a b" . 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

210 
finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" . 
10285  211 
qed 
212 
finally show ?thesis . 

213 
qed 

214 

10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

215 
theorem quot_function2: 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

216 
"(!!X Y. f X Y == g (pick X) (pick Y)) ==> 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

217 
(!!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

218 
f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

219 
proof  
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

220 
case antecedent from this refl TrueI 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

221 
show ?thesis by (rule quot_cond_function2) 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

222 
qed 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

223 

4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

224 
theorem quot_cond_operation2: 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

225 
"(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==> 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

226 
(!!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

227 
==> g x y \<sim> g x' y') ==> 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

228 
(!!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

229 
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

230 
proof  
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

231 
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

232 
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

233 
==> g x y \<sim> g x' y'" 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

234 
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

235 
==> \<lfloor>g x y\<rfloor> = \<lfloor>g x' y'\<rfloor>" .. 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

236 
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

237 
with defn cong_g show ?thesis by (rule quot_cond_function2) 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

238 
qed 
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

239 

4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

240 
theorem quot_operation2: 
10437  241 
"(!!X Y. f X Y == \<lfloor>g (pick X) (pick Y)\<rfloor>) ==> 
242 
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y \<sim> g x' y') ==> 

243 
f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = \<lfloor>g a b\<rfloor>" 

10285  244 
proof  
10459  245 
case antecedent from this refl TrueI 
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

246 
show ?thesis by (rule quot_cond_operation2) 
10285  247 
qed 
248 

10437  249 
text {* 
250 
\medskip HOL's collection of overloaded standard operations is lifted 

251 
to quotient types in the canonical manner. 

252 
*} 

253 

254 
instance quot :: (zero) zero .. 

255 
instance quot :: (plus) plus .. 

256 
instance quot :: (minus) minus .. 

257 
instance quot :: (times) times .. 

258 
instance quot :: (inverse) inverse .. 

259 
instance quot :: (power) power .. 

260 
instance quot :: (number) number .. 

10459  261 
instance quot :: (ord) ord .. 
10437  262 

263 
defs (overloaded) 

264 
zero_quot_def: "0 == \<lfloor>0\<rfloor>" 

265 
add_quot_def: "X + Y == \<lfloor>pick X + pick Y\<rfloor>" 

266 
diff_quot_def: "X  Y == \<lfloor>pick X  pick Y\<rfloor>" 

267 
minus_quot_def: " X == \<lfloor> pick X\<rfloor>" 

268 
abs_quot_def: "abs X == \<lfloor>abs (pick X)\<rfloor>" 

269 
mult_quot_def: "X * Y == \<lfloor>pick X * pick Y\<rfloor>" 

270 
inverse_quot_def: "inverse X == \<lfloor>inverse (pick X)\<rfloor>" 

271 
divide_quot_def: "X / Y == \<lfloor>pick X / pick Y\<rfloor>" 

272 
power_quot_def: "X^n == \<lfloor>(pick X)^n\<rfloor>" 

273 
number_of_quot_def: "number_of b == \<lfloor>number_of b\<rfloor>" 

10459  274 
le_quot_def: "X \<le> Y == pick X \<le> pick Y" 
275 
less_quot_def: "X < Y == pick X < pick Y" 

10437  276 

10250  277 
end 