author  haftmann 
Tue, 20 Mar 2007 08:27:15 +0100  
changeset 22473  753123c89d72 
parent 22390  378f34b1e380 
child 23373  ead82c82da9e 
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 
15140  9 
imports Main 
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 + 
22390  25 
fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<^loc>\<sim>" 50) 
10250  26 

22390  27 
class equiv = eqv + 
28 
assumes equiv_refl [intro]: "x \<^loc>\<sim> x" 

29 
assumes equiv_trans [trans]: "x \<^loc>\<sim> y \<Longrightarrow> y \<^loc>\<sim> z \<Longrightarrow> x \<^loc>\<sim> z" 

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

10250  31 

12371  32 
lemma equiv_not_sym [sym]: "\<not> (x \<sim> y) ==> \<not> (y \<sim> (x::'a::equiv))" 
10477  33 
proof  
34 
assume "\<not> (x \<sim> y)" thus "\<not> (y \<sim> x)" 

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  

40 
assume "\<not> (x \<sim> y)" and yz: "y \<sim> z" 

41 
show "\<not> (x \<sim> z)" 

42 
proof 

43 
assume "x \<sim> z" 

44 
also from yz have "z \<sim> y" .. 

45 
finally have "x \<sim> y" . 

46 
thus False by contradiction 

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  

52 
assume "\<not> (y \<sim> z)" hence "\<not> (z \<sim> y)" .. 

53 
also assume "x \<sim> y" hence "y \<sim> x" .. 

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

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" 

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

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

18730  85 
thus ?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 

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

109 
thus ?thesis .. 

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 
10551  128 
thus ?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>" 

10285  145 
hence "a \<sim> x" .. thus "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>" 

10285  152 
hence "pick A \<sim> a" by (simp only: pick_equiv) 
153 
hence "\<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 
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

178 
show "P \<lfloor>a\<rfloor> \<lfloor>b\<rfloor>" . 
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" 

188 
using prems and TrueI 

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 