author  kleing 
Mon, 21 Jun 2004 10:25:57 +0200  
changeset 14981  e73f8140af78 
parent 14706  71590b7733b7 
child 15131  c69542757a4d 
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 

8 
theory Quotient = Main: 

9 

10 
text {* 

10285  11 
We introduce the notion of quotient types over equivalence relations 
12 
via axiomatic type classes. 

10250  13 
*} 
14 

10285  15 
subsection {* Equivalence relations and quotient types *} 
10250  16 

17 
text {* 

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

10250  20 
*} 
21 

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

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

10250  25 

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

12371  29 
equiv_sym [sym]: "x \<sim> y ==> y \<sim> x" 
10250  30 

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

34 
by (rule contrapos_nn) (rule equiv_sym) 

35 
qed 

36 

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

38 
proof  

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

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

41 
proof 

42 
assume "x \<sim> z" 

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

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

45 
thus False by contradiction 

46 
qed 

47 
qed 

48 

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

50 
proof  

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

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

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

54 
qed 

55 

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

10250  59 
*} 
60 

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

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

65 
by (unfold quot_def) blast 

66 

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

68 
by (unfold quot_def) blast 

69 

70 
text {* 

71 
\medskip Abstracted equivalence classes are the canonical 

72 
representation of elements of a quotient type. 

73 
*} 

74 

75 
constdefs 

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

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

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

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

10551  84 
thus ?thesis by (unfold class_def) 
10250  85 
qed 
86 

10311  87 
lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" 
88 
by (insert quot_exhaust) blast 

10250  89 

90 

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

93 
text {* 

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

10250  96 
*} 
97 

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

101 
show "a \<sim> b" 

102 
proof  

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

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

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

108 
thus ?thesis .. 

109 
qed 

110 
next 

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

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

115 
proof (rule Collect_cong) 

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

117 
proof 

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

119 
also assume "a \<sim> x" 

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

121 
next 

122 
note ab 

123 
also assume "b \<sim> x" 

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

125 
qed 

10250  126 
qed 
10551  127 
thus ?thesis by (simp only: class_def) 
10250  128 
qed 
129 
qed 

130 

131 

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

134 
constdefs 

10285  135 
pick :: "'a::equiv quot => 'a" 
10250  136 
"pick A == SOME a. A = \<lfloor>a\<rfloor>" 
137 

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

141 
proof (rule someI2) 

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

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

10285  144 
hence "a \<sim> x" .. thus "x \<sim> a" .. 
10250  145 
qed 
146 
qed 

147 

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

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

10250  153 
with a show ?thesis by simp 
154 
qed 

155 

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

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

160 
most of the time. 

10285  161 
*} 
162 

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

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

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

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

167 
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

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

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

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

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

172 
hence "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: 
10473
4f15b844fea6
separate rules for function/operation definitions;
wenzelm
parents:
10459
diff
changeset

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

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

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

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

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

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

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

199 

10250  200 
end 