author  wenzelm 
Thu, 16 Feb 2006 21:12:00 +0100  
changeset 19086  1b3780be6cc2 
parent 18730  843da46f89ac 
child 21404  eb85850d3eb7 
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 
14 
via axiomatic 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 

12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11549
diff
changeset

24 
axclass eqv \<subseteq> type 
10285  25 
consts 
26 
eqv :: "('a::eqv) => 'a => bool" (infixl "\<sim>" 50) 

10250  27 

11099  28 
axclass equiv \<subseteq> eqv 
10333  29 
equiv_refl [intro]: "x \<sim> x" 
30 
equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z" 

12371  31 
equiv_sym [sym]: "x \<sim> y ==> y \<sim> x" 
10250  32 

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

36 
by (rule contrapos_nn) (rule equiv_sym) 

37 
qed 

38 

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

40 
proof  

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

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

43 
proof 

44 
assume "x \<sim> z" 

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

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

47 
thus False by contradiction 

48 
qed 

49 
qed 

50 

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

52 
proof  

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

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

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

56 
qed 

57 

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

10250  61 
*} 
62 

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

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

18730  67 
unfolding quot_def by blast 
10250  68 

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

18730  70 
unfolding quot_def by blast 
10250  71 

72 
text {* 

73 
\medskip Abstracted equivalence classes are the canonical 

74 
representation of elements of a quotient type. 

75 
*} 

76 

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

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

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

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

18730  86 
thus ?thesis unfolding class_def . 
10250  87 
qed 
88 

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

92 

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

95 
text {* 

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

10250  98 
*} 
99 

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

103 
show "a \<sim> b" 

104 
proof  

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

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

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

110 
thus ?thesis .. 

111 
qed 

112 
next 

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

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

117 
proof (rule Collect_cong) 

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

119 
proof 

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

121 
also assume "a \<sim> x" 

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

123 
next 

124 
note ab 

125 
also assume "b \<sim> x" 

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

127 
qed 

10250  128 
qed 
10551  129 
thus ?thesis by (simp only: class_def) 
10250  130 
qed 
131 
qed 

132 

133 

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

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

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

143 
proof (rule someI2) 

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

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

10285  146 
hence "a \<sim> x" .. thus "x \<sim> a" .. 
10250  147 
qed 
148 
qed 

149 

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

10285  153 
hence "pick A \<sim> a" by (simp only: pick_equiv) 
154 
hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" .. 

10250  155 
with a show ?thesis by simp 
156 
qed 

157 

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

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

162 
most of the time. 

10285  163 
*} 
164 

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

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

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

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

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

171 
proof  
18372  172 
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  173 
also have "... = g a b" 
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

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

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

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

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

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

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

183 
qed 

184 

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

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

189 
using prems and TrueI 

190 
by (rule quot_cond_function) 

10285  191 

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

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

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

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

10250  198 
end 