author  nipkow 
Wed, 18 Aug 2004 11:09:40 +0200  
changeset 15140  322485b816ac 
parent 15131  c69542757a4d 
child 18372  2bffdf62fe7f 
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" 

67 
by (unfold quot_def) blast 

68 

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

70 
by (unfold quot_def) blast 

71 

72 
text {* 

73 
\medskip Abstracted equivalence classes are the canonical 

74 
representation of elements of a quotient type. 

75 
*} 

76 

77 
constdefs 

10551  78 
class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>") 
10250  79 
"\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" 
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 

10551  86 
thus ?thesis by (unfold class_def) 
10250  87 
qed 
88 

10311  89 
lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" 
90 
by (insert quot_exhaust) 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 

136 
constdefs 

10285  137 
pick :: "'a::equiv quot => 'a" 
10250  138 
"pick A == SOME a. A = \<lfloor>a\<rfloor>" 
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: 
10491
e4a408728012
quot_cond_function: simplified, support conditional definition;
wenzelm
parents:
10483
diff
changeset

166 
"(!!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

167 
(!!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

168 
==> 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

169 
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

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

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

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

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

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

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

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

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

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

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

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

185 
qed 

186 

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

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

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

191 
proof  
11549  192 
case rule_context from this TrueI 
10483  193 
show ?thesis by (rule quot_cond_function) 
10285  194 
qed 
195 

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

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

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

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

201 

10250  202 
end 