summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Library/Quotient.thy

author | wenzelm |

Wed Oct 18 23:29:13 2000 +0200 (2000-10-18) | |

changeset 10250 | ca93fe25a84b |

child 10278 | ea1bf4b6255c |

permissions | -rw-r--r-- |

Quotient types;

1 (* Title: HOL/Library/Quotient.thy

2 ID: $Id$

3 Author: Gertrud Bauer and Markus Wenzel, TU Muenchen

4 *)

6 header {*

7 \title{Quotients}

8 \author{Gertrud Bauer and Markus Wenzel}

9 *}

11 theory Quotient = Main:

13 text {*

14 Higher-order quotients are defined over partial equivalence relations

15 (PERs) instead of total ones. We provide axiomatic type classes

16 @{text "equiv < partial_equiv"} and a type constructor

17 @{text "'a quot"} with basic operations. Note that conventional

18 quotient constructions emerge as a special case. This development is

19 loosely based on \cite{Slotosch:1997}.

20 *}

23 subsection {* Equivalence relations *}

25 subsubsection {* Partial equivalence *}

27 text {*

28 Type class @{text partial_equiv} models partial equivalence relations

29 (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,

30 which is required to be symmetric and transitive, but not necessarily

31 reflexive.

32 *}

34 consts

35 eqv :: "'a => 'a => bool" (infixl "\<sim>" 50)

37 axclass partial_equiv < "term"

38 eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"

39 eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"

41 text {*

42 \medskip The domain of a partial equivalence relation is the set of

43 reflexive elements. Due to symmetry and transitivity this

44 characterizes exactly those elements that are connected with

45 \emph{any} other one.

46 *}

48 constdefs

49 domain :: "'a::partial_equiv set"

50 "domain == {x. x \<sim> x}"

52 lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"

53 by (unfold domain_def) blast

55 lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"

56 by (unfold domain_def) blast

58 theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"

59 proof

60 assume xy: "x \<sim> y"

61 also from xy have "y \<sim> x" ..

62 finally show "x \<sim> x" .

63 qed

66 subsubsection {* Equivalence on function spaces *}

68 text {*

69 The @{text \<sim>} relation is lifted to function spaces. It is

70 important to note that this is \emph{not} the direct product, but a

71 structural one corresponding to the congruence property.

72 *}

74 defs (overloaded)

75 eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"

77 lemma partial_equiv_funI [intro?]:

78 "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"

79 by (unfold eqv_fun_def) blast

81 lemma partial_equiv_funD [dest?]:

82 "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"

83 by (unfold eqv_fun_def) blast

85 text {*

86 The class of partial equivalence relations is closed under function

87 spaces (in \emph{both} argument positions).

88 *}

90 instance fun :: (partial_equiv, partial_equiv) partial_equiv

91 proof intro_classes

92 fix f g h :: "'a::partial_equiv => 'b::partial_equiv"

93 assume fg: "f \<sim> g"

94 show "g \<sim> f"

95 proof

96 fix x y :: 'a

97 assume x: "x \<in> domain" and y: "y \<in> domain"

98 assume "x \<sim> y" hence "y \<sim> x" ..

99 with fg y x have "f y \<sim> g x" ..

100 thus "g x \<sim> f y" ..

101 qed

102 assume gh: "g \<sim> h"

103 show "f \<sim> h"

104 proof

105 fix x y :: 'a

106 assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y"

107 with fg have "f x \<sim> g y" ..

108 also from y have "y \<sim> y" ..

109 with gh y y have "g y \<sim> h y" ..

110 finally show "f x \<sim> h y" .

111 qed

112 qed

115 subsubsection {* Total equivalence *}

117 text {*

118 The class of total equivalence relations on top of PERs. It

119 coincides with the standard notion of equivalence, i.e.\

120 @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive

121 and symmetric.

122 *}

124 axclass equiv < partial_equiv

125 eqv_refl [intro]: "x \<sim> x"

127 text {*

128 On total equivalences all elements are reflexive, and congruence

129 holds unconditionally.

130 *}

132 theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"

133 proof

134 show "x \<sim> x" ..

135 qed

137 theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"

138 proof -

139 assume "f \<sim> g"

140 moreover have "x \<in> domain" ..

141 moreover have "y \<in> domain" ..

142 moreover assume "x \<sim> y"

143 ultimately show ?thesis ..

144 qed

147 subsection {* Quotient types *}

149 subsubsection {* General quotients and equivalence classes *}

151 text {*

152 The quotient type @{text "'a quot"} consists of all \emph{equivalence

153 classes} over elements of the base type @{typ 'a}.

154 *}

156 typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"

157 by blast

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

160 by (unfold quot_def) blast

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

163 by (unfold quot_def) blast

166 text {*

167 \medskip Standard properties of type-definitions.\footnote{(FIXME)

168 Better incorporate these into the typedef package?}

169 *}

171 theorem Rep_quot_inject: "(Rep_quot x = Rep_quot y) = (x = y)"

172 proof

173 assume "Rep_quot x = Rep_quot y"

174 hence "Abs_quot (Rep_quot x) = Abs_quot (Rep_quot y)" by (simp only:)

175 thus "x = y" by (simp only: Rep_quot_inverse)

176 next

177 assume "x = y"

178 thus "Rep_quot x = Rep_quot y" by simp

179 qed

181 theorem Abs_quot_inject:

182 "x \<in> quot ==> y \<in> quot ==> (Abs_quot x = Abs_quot y) = (x = y)"

183 proof

184 assume "Abs_quot x = Abs_quot y"

185 hence "Rep_quot (Abs_quot x) = Rep_quot (Abs_quot y)" by simp

186 also assume "x \<in> quot" hence "Rep_quot (Abs_quot x) = x" by (rule Abs_quot_inverse)

187 also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)

188 finally show "x = y" .

189 next

190 assume "x = y"

191 thus "Abs_quot x = Abs_quot y" by simp

192 qed

194 theorem Rep_quot_induct: "y \<in> quot ==> (!!x. P (Rep_quot x)) ==> P y"

195 proof -

196 assume "!!x. P (Rep_quot x)" hence "P (Rep_quot (Abs_quot y))" .

197 also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)

198 finally show "P y" .

199 qed

201 theorem Abs_quot_induct: "(!!y. y \<in> quot ==> P (Abs_quot y)) ==> P x"

202 proof -

203 assume r: "!!y. y \<in> quot ==> P (Abs_quot y)"

204 have "Rep_quot x \<in> quot" by (rule Rep_quot)

205 hence "P (Abs_quot (Rep_quot x))" by (rule r)

206 also have "Abs_quot (Rep_quot x) = x" by (rule Rep_quot_inverse)

207 finally show "P x" .

208 qed

210 text {*

211 \medskip Abstracted equivalence classes are the canonical

212 representation of elements of a quotient type.

213 *}

215 constdefs

216 eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>")

217 "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"

219 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"

220 proof (unfold eqv_class_def)

221 show "\<exists>a. A = Abs_quot {x. a \<sim> x}"

222 proof (induct A rule: Abs_quot_induct)

223 fix R assume "R \<in> quot"

224 hence "\<exists>a. R = {x. a \<sim> x}" by blast

225 thus "\<exists>a. Abs_quot R = Abs_quot {x. a \<sim> x}" by blast

226 qed

227 qed

229 lemma quot_cases [case_names rep, cases type: quot]:

230 "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"

231 by (insert quot_rep) blast

234 subsubsection {* Equality on quotients *}

236 text {*

237 Equality of canonical quotient elements corresponds to the original

238 relation as follows.

239 *}

241 theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"

242 proof -

243 assume ab: "a \<sim> b"

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

245 proof (rule Collect_cong)

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

247 proof

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

249 also assume "a \<sim> x"

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

251 next

252 note ab

253 also assume "b \<sim> x"

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

255 qed

256 qed

257 thus ?thesis by (simp only: eqv_class_def)

258 qed

260 theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b" (* FIXME [dest] would cause trouble with blast due to overloading *)

261 proof (unfold eqv_class_def)

262 assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"

263 hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)

264 moreover assume "a \<in> domain" hence "a \<sim> a" ..

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

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

267 thus "a \<sim> b" ..

268 qed

270 theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)" (* FIXME [dest] would cause trouble with blast due to overloading *)

271 proof (rule eqv_class_eqD')

272 show "a \<in> domain" ..

273 qed

275 lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"

276 by (insert eqv_class_eqI eqv_class_eqD') blast

278 lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"

279 by (insert eqv_class_eqI eqv_class_eqD) blast

282 subsubsection {* Picking representing elements *}

284 constdefs

285 pick :: "'a::partial_equiv quot => 'a"

286 "pick A == SOME a. A = \<lfloor>a\<rfloor>"

288 theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" (* FIXME [intro] !? *)

289 proof (unfold pick_def)

290 assume a: "a \<in> domain"

291 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"

292 proof (rule someI2)

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

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

295 hence "a \<sim> x" ..

296 thus "x \<sim> a" ..

297 qed

298 qed

300 theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)"

301 proof (rule pick_eqv')

302 show "a \<in> domain" ..

303 qed

305 theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)" (* FIXME tune proof *)

306 proof (cases A)

307 fix a assume a: "A = \<lfloor>a\<rfloor>"

308 hence "pick A \<sim> a" by (simp only: pick_eqv)

309 hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp

310 with a show ?thesis by simp

311 qed

313 end