author  wenzelm 
Tue, 21 Nov 2000 19:03:06 +0100  
changeset 10505  b89e6cc963e3 
parent 10499  2f33d0fd242e 
child 10551  ec9fab41b3a0 
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: 
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

179 
"(!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)) ==> 
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

180 
(!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> 
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

181 
==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y') ==> 
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

182 
P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> ==> f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" 
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

183 
(is "PROP ?eq ==> PROP ?cong ==> _ ==> _") 
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

184 
proof  
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

185 
assume cong: "PROP ?cong" 
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

186 
assume "PROP ?eq" and "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" 
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

187 
hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) 
10505  188 
also have "... = g a b" 
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

189 
proof (rule cong) 
10483  190 
show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" .. 
191 
moreover 

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

10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

193 
moreover 
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

194 
show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" . 
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

195 
ultimately show "P \<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> \<lfloor>pick \<lfloor>b\<rfloor>\<rfloor>" by (simp only:) 
10285  196 
qed 
197 
finally show ?thesis . 

198 
qed 

199 

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

201 
"(!!X Y. f X Y == g (pick X) (pick Y)) ==> 
10483  202 
(!!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

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

204 
proof  
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

205 
case antecedent from this TrueI 
10483  206 
show ?thesis by (rule quot_cond_function) 
10285  207 
qed 
208 

10499  209 
theorem quot_function': 
210 
"(!!X Y. f X Y == g (pick X) (pick Y)) ==> 

211 
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==> 

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

213 
by (rule quot_function) (simp only: quot_equality)+ 

214 

10250  215 
end 