author  haftmann 
Mon, 07 Jul 2008 08:47:17 +0200  
changeset 27487  c8a6ce181805 
parent 27368  9f90ac19e32b 
child 29608  564ea783ace8 
permissions  rwrr 
10250  1 
(* Title: HOL/Library/Quotient.thy 
2 
ID: $Id$ 

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

14706  6 
header {* Quotient types *} 
10250  7 

15131  8 
theory Quotient 
27487  9 
imports Plain "~~/src/HOL/Hilbert_Choice" 
15131  10 
begin 
10250  11 

12 
text {* 

10285  13 
We introduce the notion of quotient types over equivalence relations 
22390  14 
via type classes. 
10250  15 
*} 
16 

10285  17 
subsection {* Equivalence relations and quotient types *} 
10250  18 

19 
text {* 

10390  20 
\medskip Type class @{text equiv} models equivalence relations @{text 
21 
"\<sim> :: 'a => 'a => bool"}. 

10250  22 
*} 
23 

22473  24 
class eqv = type + 
25062  25 
fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50) 
10250  26 

22390  27 
class equiv = eqv + 
25062  28 
assumes equiv_refl [intro]: "x \<sim> x" 
29 
assumes equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z" 

30 
assumes equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x" 

10250  31 

12371  32 
lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))" 
10477  33 
proof  
23373  34 
assume "\<not> (x \<sim> y)" then show "\<not> (y \<sim> x)" 
10477  35 
by (rule contrapos_nn) (rule equiv_sym) 
36 
qed 

37 

38 
lemma not_equiv_trans1 [trans]: "\<not> (x \<sim> y) ==> y \<sim> z ==> \<not> (x \<sim> (z::'a::equiv))" 

39 
proof  

23373  40 
assume "\<not> (x \<sim> y)" and "y \<sim> z" 
10477  41 
show "\<not> (x \<sim> z)" 
42 
proof 

43 
assume "x \<sim> z" 

23373  44 
also from `y \<sim> z` have "z \<sim> y" .. 
10477  45 
finally have "x \<sim> y" . 
23373  46 
with `\<not> (x \<sim> y)` show False by contradiction 
10477  47 
qed 
48 
qed 

49 

50 
lemma not_equiv_trans2 [trans]: "x \<sim> y ==> \<not> (y \<sim> z) ==> \<not> (x \<sim> (z::'a::equiv))" 

51 
proof  

23373  52 
assume "\<not> (y \<sim> z)" then have "\<not> (z \<sim> y)" .. 
53 
also assume "x \<sim> y" then have "y \<sim> x" .. 

54 
finally have "\<not> (z \<sim> x)" . then show "(\<not> x \<sim> z)" .. 

10477  55 
qed 
56 

10250  57 
text {* 
10285  58 
\medskip The quotient type @{text "'a quot"} consists of all 
59 
\emph{equivalence classes} over elements of the base type @{typ 'a}. 

10250  60 
*} 
61 

10392  62 
typedef 'a quot = "{{x. a \<sim> x}  a::'a::eqv. True}" 
10250  63 
by blast 
64 

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

18730  66 
unfolding quot_def by blast 
10250  67 

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

18730  69 
unfolding quot_def by blast 
10250  70 

71 
text {* 

72 
\medskip Abstracted equivalence classes are the canonical 

73 
representation of elements of a quotient type. 

74 
*} 

75 

19086  76 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19086
diff
changeset

77 
"class" :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") where 
19086  78 
"\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}" 
10250  79 

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

23373  83 
assume "R \<in> quot" then have "\<exists>a. R = {x. a \<sim> x}" by blast 
10278  84 
with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast 
23373  85 
then show ?thesis unfolding class_def . 
10250  86 
qed 
87 

10311  88 
lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" 
18730  89 
using quot_exhaust by blast 
10250  90 

91 

10285  92 
subsection {* Equality on quotients *} 
10250  93 

94 
text {* 

10286  95 
Equality of canonical quotient elements coincides with the original 
96 
relation. 

10250  97 
*} 
98 

12371  99 
theorem quot_equality [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" 
10285  100 
proof 
101 
assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" 

102 
show "a \<sim> b" 

103 
proof  

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

10551  105 
by (simp only: class_def Abs_quot_inject quotI) 
10285  106 
moreover have "a \<sim> a" .. 
107 
ultimately have "a \<in> {x. b \<sim> x}" by blast 

23373  108 
then have "b \<sim> a" by blast 
109 
then show ?thesis .. 

10285  110 
qed 
111 
next 

10250  112 
assume ab: "a \<sim> b" 
10285  113 
show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" 
114 
proof  

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

116 
proof (rule Collect_cong) 

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

118 
proof 

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

120 
also assume "a \<sim> x" 

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

122 
next 

123 
note ab 

124 
also assume "b \<sim> x" 

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

126 
qed 

10250  127 
qed 
23373  128 
then show ?thesis by (simp only: class_def) 
10250  129 
qed 
130 
qed 

131 

132 

10285  133 
subsection {* Picking representing elements *} 
10250  134 

19086  135 
definition 
21404
eb85850d3eb7
more robust syntax for definition/abbreviation/notation;
wenzelm
parents:
19086
diff
changeset

136 
pick :: "'a::equiv quot => 'a" where 
19086  137 
"pick A = (SOME a. A = \<lfloor>a\<rfloor>)" 
10250  138 

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

142 
proof (rule someI2) 

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

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

23373  145 
then have "a \<sim> x" .. then show "x \<sim> a" .. 
10250  146 
qed 
147 
qed 

148 

10483  149 
theorem pick_inverse [intro]: "\<lfloor>pick A\<rfloor> = A" 
10250  150 
proof (cases A) 
151 
fix a assume a: "A = \<lfloor>a\<rfloor>" 

23373  152 
then have "pick A \<sim> a" by (simp only: pick_equiv) 
153 
then have "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. 

10250  154 
with a show ?thesis by simp 
155 
qed 

156 

10285  157 
text {* 
158 
\medskip The following rules support canonical function definitions 

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

161 
most of the time. 

10285  162 
*} 
163 

10483  164 
theorem quot_cond_function: 
18372  165 
assumes eq: "!!X Y. P X Y ==> f X Y == g (pick X) (pick Y)" 
166 
and cong: "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> 

167 
==> P \<lfloor>x\<rfloor> \<lfloor>y\<rfloor> ==> P \<lfloor>x'\<rfloor> \<lfloor>y'\<rfloor> ==> g x y = g x' y'" 

168 
and P: "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" 

169 
shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" 

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

170 
proof  
18372  171 
from eq and P have "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:) 
10505  172 
also have "... = g a b" 
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

173 
proof (rule cong) 
10483  174 
show "\<lfloor>pick \<lfloor>a\<rfloor>\<rfloor> = \<lfloor>a\<rfloor>" .. 
175 
moreover 

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

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

177 
moreover 
23373  178 
show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" by (rule P) 
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

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

182 
qed 

183 

10483  184 
theorem quot_function: 
18372  185 
assumes "!!X Y. f X Y == g (pick X) (pick Y)" 
186 
and "!!x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> ==> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> ==> g x y = g x' y'" 

187 
shows "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b" 

23394  188 
using assms and TrueI 
18372  189 
by (rule quot_cond_function) 
10285  190 

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

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

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

18372  195 
by (rule quot_function) (simp_all only: quot_equality) 
10499  196 

10250  197 
end 