author  wenzelm 
Fri, 17 Nov 2000 18:48:50 +0100  
changeset 10483  eb93ace45a6e 
parent 10477  c21bee84cefe 
child 10491  e4a408728012 
permissions  rwrr 
10250  1 
(* Title: HOL/Library/Quotient.thy 
2 
ID: $Id$ 

10483  3 
Author: Markus Wenzel, TU Muenchen 
10250  4 
*) 
5 

6 
header {* 

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

7 
\title{Quotient types} 
10483  8 
\author{Markus Wenzel} 
10250  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 

10483  163 
theorem pick_inverse [intro]: "\<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 

10483  173 
on quotient types (with up to two arguments). Note that the 
174 
strippeddown version without additional conditions is sufficient 

175 
most of the time. 

10285  176 
*} 
177 

10483  178 
theorem quot_cond_function: 
179 
"(!!X Y. f X Y == g (pick X) (pick Y)) ==> 

180 
(!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y ==> P x' y' 

181 
==> g x y = g x' y') ==> 

182 
(!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> P x y = P x' y') ==> 

183 
P a b ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" 

184 
(is "PROP ?eq ==> PROP ?cong_g ==> PROP ?cong_P ==> _ ==> _") 

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

185 
proof  
10483  186 
assume cong_g: "PROP ?cong_g" 
187 
and cong_P: "PROP ?cong_P" and P: "P a b" 

188 
assume "PROP ?eq" 

189 
hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" 

190 
by (simp only:) 

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

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

192 
proof (rule cong_g) 
10483  193 
show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" .. 
194 
moreover 

195 
show "\<lfloor>pick \<lfloor>b\<rfloor>\<rfloor> = \<lfloor>b\<rfloor>" .. 

196 
ultimately 

197 
have "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>) = P a b" 

198 
by (rule cong_P) 

199 
also show \<dots> . 

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

200 
finally show "P (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" . 
10285  201 
qed 
202 
finally show ?thesis . 

203 
qed 

204 

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

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

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

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

210 
case antecedent from this refl TrueI 
10483  211 
show ?thesis by (rule quot_cond_function) 
10285  212 
qed 
213 

10250  214 
end 