author  wenzelm 
Sun, 28 Dec 2014 12:37:03 +0100  
changeset 59192  a1d6d6db781b 
parent 58881  b9556a055632 
child 61260  e6f03fae14d5 
permissions  rwrr 
35100
53754ec7360b
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents:
30738
diff
changeset

1 
(* Title: HOL/Library/Quotient_Type.thy 
10483  2 
Author: Markus Wenzel, TU Muenchen 
10250  3 
*) 
4 

59192  5 
section \<open>Quotient types\<close> 
10250  6 

35100
53754ec7360b
renamed Library/Quotient.thy to Library/Quotient_Type.thy to avoid clash with new theory Quotient in Main HOL;
wenzelm
parents:
30738
diff
changeset

7 
theory Quotient_Type 
30738  8 
imports Main 
15131  9 
begin 
10250  10 

59192  11 
text \<open>We introduce the notion of quotient types over equivalence relations 
12 
via type classes.\<close> 

13 

10250  14 

59192  15 
subsection \<open>Equivalence relations and quotient types\<close> 
10250  16 

59192  17 
text \<open>Type class @{text equiv} models equivalence relations 
18 
@{text "\<sim> :: 'a \<Rightarrow> 'a \<Rightarrow> bool"}.\<close> 

10250  19 

29608  20 
class eqv = 
59192  21 
fixes eqv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "\<sim>" 50) 
10250  22 

22390  23 
class equiv = eqv + 
25062  24 
assumes equiv_refl [intro]: "x \<sim> x" 
59192  25 
and equiv_trans [trans]: "x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> x \<sim> z" 
26 
and equiv_sym [sym]: "x \<sim> y \<Longrightarrow> y \<sim> x" 

27 
begin 

10250  28 

59192  29 
lemma equiv_not_sym [sym]: "\<not> x \<sim> y \<Longrightarrow> \<not> y \<sim> x" 
10477  30 
proof  
59192  31 
assume "\<not> x \<sim> y" 
32 
then show "\<not> y \<sim> x" by (rule contrapos_nn) (rule equiv_sym) 

10477  33 
qed 
34 

59192  35 
lemma not_equiv_trans1 [trans]: "\<not> x \<sim> y \<Longrightarrow> y \<sim> z \<Longrightarrow> \<not> x \<sim> z" 
10477  36 
proof  
59192  37 
assume "\<not> x \<sim> y" and "y \<sim> z" 
38 
show "\<not> x \<sim> z" 

10477  39 
proof 
40 
assume "x \<sim> z" 

59192  41 
also from \<open>y \<sim> z\<close> have "z \<sim> y" .. 
10477  42 
finally have "x \<sim> y" . 
59192  43 
with \<open>\<not> x \<sim> y\<close> show False by contradiction 
10477  44 
qed 
45 
qed 

46 

59192  47 
lemma not_equiv_trans2 [trans]: "x \<sim> y \<Longrightarrow> \<not> y \<sim> z \<Longrightarrow> \<not> x \<sim> z" 
10477  48 
proof  
59192  49 
assume "\<not> y \<sim> z" 
50 
then have "\<not> z \<sim> y" .. 

51 
also 

52 
assume "x \<sim> y" 

53 
then have "y \<sim> x" .. 

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

55 
then show "\<not> x \<sim> z" .. 

10477  56 
qed 
57 

59192  58 
end 
10250  59 

59192  60 
text \<open>The quotient type @{text "'a quot"} consists of all \emph{equivalence 
61 
classes} over elements of the base type @{typ 'a}.\<close> 

62 

63 
definition (in eqv) "quot = {{x. a \<sim> x}  a. True}" 

45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
35100
diff
changeset

64 

49834  65 
typedef 'a quot = "quot :: 'a::eqv set set" 
45694
4a8743618257
prefer typedef without extra definition and alternative name;
wenzelm
parents:
35100
diff
changeset

66 
unfolding quot_def by blast 
10250  67 

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

18730  69 
unfolding quot_def by blast 
10250  70 

59192  71 
lemma quotE [elim]: 
72 
assumes "R \<in> quot" 

73 
obtains a where "R = {x. a \<sim> x}" 

74 
using assms unfolding quot_def by blast 

10250  75 

59192  76 
text \<open>Abstracted equivalence classes are the canonical representation of 
77 
elements of a quotient type.\<close> 

10250  78 

59192  79 
definition "class" :: "'a::equiv \<Rightarrow> 'a quot" ("\<lfloor>_\<rfloor>") 
80 
where "\<lfloor>a\<rfloor> = Abs_quot {x. a \<sim> x}" 

10250  81 

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

86 
assume "R \<in> quot" 

87 
then have "\<exists>a. R = {x. a \<sim> x}" by blast 

10278  88 
with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast 
23373  89 
then show ?thesis unfolding class_def . 
10250  90 
qed 
91 

59192  92 
lemma quot_cases [cases type: quot]: 
93 
obtains a where "A = \<lfloor>a\<rfloor>" 

18730  94 
using quot_exhaust by blast 
10250  95 

96 

59192  97 
subsection \<open>Equality on quotients\<close> 
10250  98 

59192  99 
text \<open>Equality of canonical quotient elements coincides with the original 
100 
relation.\<close> 

10250  101 

59192  102 
theorem quot_equality [iff?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> \<longleftrightarrow> a \<sim> b" 
10285  103 
proof 
104 
assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" 

105 
show "a \<sim> b" 

106 
proof  

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

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

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

10285  113 
qed 
114 
next 

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

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

119 
proof (rule Collect_cong) 

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

121 
proof 

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

123 
also assume "a \<sim> x" 

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

125 
next 

126 
note ab 

127 
also assume "b \<sim> x" 

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

129 
qed 

10250  130 
qed 
23373  131 
then show ?thesis by (simp only: class_def) 
10250  132 
qed 
133 
qed 

134 

135 

59192  136 
subsection \<open>Picking representing elements\<close> 
10250  137 

59192  138 
definition pick :: "'a::equiv quot \<Rightarrow> 'a" 
139 
where "pick A = (SOME a. A = \<lfloor>a\<rfloor>)" 

10250  140 

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

144 
proof (rule someI2) 

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

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

59192  147 
then have "a \<sim> x" .. 
148 
then show "x \<sim> a" .. 

10250  149 
qed 
150 
qed 

151 

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

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

10250  157 
with a show ?thesis by simp 
158 
qed 

159 

59192  160 
text \<open>The following rules support canonical function definitions on quotient 
161 
types (with up to two arguments). Note that the strippeddown version 

162 
without additional conditions is sufficient most of the time.\<close> 

10285  163 

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

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

18372  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: 
59192  185 
assumes "\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)" 
186 
and "\<And>x x' y y'. \<lfloor>x\<rfloor> = \<lfloor>x'\<rfloor> \<Longrightarrow> \<lfloor>y\<rfloor> = \<lfloor>y'\<rfloor> \<Longrightarrow> g x y = g x' y'" 

18372  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': 
59192  192 
"(\<And>X Y. f X Y \<equiv> g (pick X) (pick Y)) \<Longrightarrow> 
193 
(\<And>x x' y y'. x \<sim> x' \<Longrightarrow> y \<sim> y' \<Longrightarrow> g x y = g x' y') \<Longrightarrow> 

10499  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 