10250

1 
(* Title: HOL/Library/Quotient.thy


2 
ID: $Id$


3 
Author: Gertrud Bauer and Markus Wenzel, TU Muenchen


4 
*)


5 


6 
header {*


7 
\title{Quotients}


8 
\author{Gertrud Bauer and Markus Wenzel}


9 
*}


10 


11 
theory Quotient = Main:


12 


13 
text {*


14 
Higherorder quotients are defined over partial equivalence relations


15 
(PERs) instead of total ones. We provide axiomatic type classes


16 
@{text "equiv < partial_equiv"} and a type constructor


17 
@{text "'a quot"} with basic operations. Note that conventional


18 
quotient constructions emerge as a special case. This development is


19 
loosely based on \cite{Slotosch:1997}.


20 
*}


21 


22 


23 
subsection {* Equivalence relations *}


24 


25 
subsubsection {* Partial equivalence *}


26 


27 
text {*


28 
Type class @{text partial_equiv} models partial equivalence relations


29 
(PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation,


30 
which is required to be symmetric and transitive, but not necessarily


31 
reflexive.


32 
*}


33 


34 
consts


35 
eqv :: "'a => 'a => bool" (infixl "\<sim>" 50)


36 


37 
axclass partial_equiv < "term"


38 
eqv_sym [elim?]: "x \<sim> y ==> y \<sim> x"


39 
eqv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"


40 


41 
text {*


42 
\medskip The domain of a partial equivalence relation is the set of


43 
reflexive elements. Due to symmetry and transitivity this


44 
characterizes exactly those elements that are connected with


45 
\emph{any} other one.


46 
*}


47 


48 
constdefs


49 
domain :: "'a::partial_equiv set"


50 
"domain == {x. x \<sim> x}"


51 


52 
lemma domainI [intro]: "x \<sim> x ==> x \<in> domain"


53 
by (unfold domain_def) blast


54 


55 
lemma domainD [dest]: "x \<in> domain ==> x \<sim> x"


56 
by (unfold domain_def) blast


57 


58 
theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain"


59 
proof


60 
assume xy: "x \<sim> y"


61 
also from xy have "y \<sim> x" ..


62 
finally show "x \<sim> x" .


63 
qed


64 


65 


66 
subsubsection {* Equivalence on function spaces *}


67 


68 
text {*


69 
The @{text \<sim>} relation is lifted to function spaces. It is


70 
important to note that this is \emph{not} the direct product, but a


71 
structural one corresponding to the congruence property.


72 
*}


73 


74 
defs (overloaded)


75 
eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y > f x \<sim> g y"


76 


77 
lemma partial_equiv_funI [intro?]:


78 
"(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g"


79 
by (unfold eqv_fun_def) blast


80 


81 
lemma partial_equiv_funD [dest?]:


82 
"f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y"


83 
by (unfold eqv_fun_def) blast


84 


85 
text {*


86 
The class of partial equivalence relations is closed under function


87 
spaces (in \emph{both} argument positions).


88 
*}


89 


90 
instance fun :: (partial_equiv, partial_equiv) partial_equiv


91 
proof intro_classes


92 
fix f g h :: "'a::partial_equiv => 'b::partial_equiv"


93 
assume fg: "f \<sim> g"


94 
show "g \<sim> f"


95 
proof


96 
fix x y :: 'a


97 
assume x: "x \<in> domain" and y: "y \<in> domain"


98 
assume "x \<sim> y" hence "y \<sim> x" ..


99 
with fg y x have "f y \<sim> g x" ..


100 
thus "g x \<sim> f y" ..


101 
qed


102 
assume gh: "g \<sim> h"


103 
show "f \<sim> h"


104 
proof


105 
fix x y :: 'a


106 
assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y"


107 
with fg have "f x \<sim> g y" ..


108 
also from y have "y \<sim> y" ..


109 
with gh y y have "g y \<sim> h y" ..


110 
finally show "f x \<sim> h y" .


111 
qed


112 
qed


113 


114 


115 
subsubsection {* Total equivalence *}


116 


117 
text {*


118 
The class of total equivalence relations on top of PERs. It


119 
coincides with the standard notion of equivalence, i.e.\


120 
@{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive


121 
and symmetric.


122 
*}


123 


124 
axclass equiv < partial_equiv


125 
eqv_refl [intro]: "x \<sim> x"


126 


127 
text {*


128 
On total equivalences all elements are reflexive, and congruence


129 
holds unconditionally.


130 
*}


131 


132 
theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain"


133 
proof


134 
show "x \<sim> x" ..


135 
qed


136 


137 
theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)"


138 
proof 


139 
assume "f \<sim> g"


140 
moreover have "x \<in> domain" ..


141 
moreover have "y \<in> domain" ..


142 
moreover assume "x \<sim> y"


143 
ultimately show ?thesis ..


144 
qed


145 


146 


147 
subsection {* Quotient types *}


148 


149 
subsubsection {* General quotients and equivalence classes *}


150 


151 
text {*


152 
The quotient type @{text "'a quot"} consists of all \emph{equivalence


153 
classes} over elements of the base type @{typ 'a}.


154 
*}


155 


156 
typedef 'a quot = "{{x. a \<sim> x} a::'a. True}"


157 
by blast


158 


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


160 
by (unfold quot_def) blast


161 


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


163 
by (unfold quot_def) blast


164 


165 


166 
text {*


167 
\medskip Standard properties of typedefinitions.\footnote{(FIXME)


168 
Better incorporate these into the typedef package?}


169 
*}


170 


171 
theorem Rep_quot_inject: "(Rep_quot x = Rep_quot y) = (x = y)"


172 
proof


173 
assume "Rep_quot x = Rep_quot y"


174 
hence "Abs_quot (Rep_quot x) = Abs_quot (Rep_quot y)" by (simp only:)


175 
thus "x = y" by (simp only: Rep_quot_inverse)


176 
next


177 
assume "x = y"


178 
thus "Rep_quot x = Rep_quot y" by simp


179 
qed


180 


181 
theorem Abs_quot_inject:


182 
"x \<in> quot ==> y \<in> quot ==> (Abs_quot x = Abs_quot y) = (x = y)"


183 
proof


184 
assume "Abs_quot x = Abs_quot y"


185 
hence "Rep_quot (Abs_quot x) = Rep_quot (Abs_quot y)" by simp


186 
also assume "x \<in> quot" hence "Rep_quot (Abs_quot x) = x" by (rule Abs_quot_inverse)


187 
also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)


188 
finally show "x = y" .


189 
next


190 
assume "x = y"


191 
thus "Abs_quot x = Abs_quot y" by simp


192 
qed


193 


194 
theorem Rep_quot_induct: "y \<in> quot ==> (!!x. P (Rep_quot x)) ==> P y"


195 
proof 


196 
assume "!!x. P (Rep_quot x)" hence "P (Rep_quot (Abs_quot y))" .


197 
also assume "y \<in> quot" hence "Rep_quot (Abs_quot y) = y" by (rule Abs_quot_inverse)


198 
finally show "P y" .


199 
qed


200 


201 
theorem Abs_quot_induct: "(!!y. y \<in> quot ==> P (Abs_quot y)) ==> P x"


202 
proof 


203 
assume r: "!!y. y \<in> quot ==> P (Abs_quot y)"


204 
have "Rep_quot x \<in> quot" by (rule Rep_quot)


205 
hence "P (Abs_quot (Rep_quot x))" by (rule r)


206 
also have "Abs_quot (Rep_quot x) = x" by (rule Rep_quot_inverse)


207 
finally show "P x" .


208 
qed


209 


210 
text {*


211 
\medskip Abstracted equivalence classes are the canonical


212 
representation of elements of a quotient type.


213 
*}


214 


215 
constdefs


216 
eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>")


217 
"\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}"


218 


219 
theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>"


220 
proof (unfold eqv_class_def)


221 
show "\<exists>a. A = Abs_quot {x. a \<sim> x}"


222 
proof (induct A rule: Abs_quot_induct)


223 
fix R assume "R \<in> quot"


224 
hence "\<exists>a. R = {x. a \<sim> x}" by blast


225 
thus "\<exists>a. Abs_quot R = Abs_quot {x. a \<sim> x}" by blast


226 
qed


227 
qed


228 


229 
lemma quot_cases [case_names rep, cases type: quot]:


230 
"(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"


231 
by (insert quot_rep) blast


232 


233 


234 
subsubsection {* Equality on quotients *}


235 


236 
text {*


237 
Equality of canonical quotient elements corresponds to the original


238 
relation as follows.


239 
*}


240 


241 
theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"


242 
proof 


243 
assume ab: "a \<sim> b"


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


245 
proof (rule Collect_cong)


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


247 
proof


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


249 
also assume "a \<sim> x"


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


251 
next


252 
note ab


253 
also assume "b \<sim> x"


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


255 
qed


256 
qed


257 
thus ?thesis by (simp only: eqv_class_def)


258 
qed


259 


260 
theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b" (* FIXME [dest] would cause trouble with blast due to overloading *)


261 
proof (unfold eqv_class_def)


262 
assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}"


263 
hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI)


264 
moreover assume "a \<in> domain" hence "a \<sim> a" ..


265 
ultimately have "a \<in> {x. b \<sim> x}" by blast


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


267 
thus "a \<sim> b" ..


268 
qed


269 


270 
theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)" (* FIXME [dest] would cause trouble with blast due to overloading *)


271 
proof (rule eqv_class_eqD')


272 
show "a \<in> domain" ..


273 
qed


274 


275 
lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"


276 
by (insert eqv_class_eqI eqv_class_eqD') blast


277 


278 
lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))"


279 
by (insert eqv_class_eqI eqv_class_eqD) blast


280 


281 


282 
subsubsection {* Picking representing elements *}


283 


284 
constdefs


285 
pick :: "'a::partial_equiv quot => 'a"


286 
"pick A == SOME a. A = \<lfloor>a\<rfloor>"


287 


288 
theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" (* FIXME [intro] !? *)


289 
proof (unfold pick_def)


290 
assume a: "a \<in> domain"


291 
show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"


292 
proof (rule someI2)


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


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


295 
hence "a \<sim> x" ..


296 
thus "x \<sim> a" ..


297 
qed


298 
qed


299 


300 
theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)"


301 
proof (rule pick_eqv')


302 
show "a \<in> domain" ..


303 
qed


304 


305 
theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)" (* FIXME tune proof *)


306 
proof (cases A)


307 
fix a assume a: "A = \<lfloor>a\<rfloor>"


308 
hence "pick A \<sim> a" by (simp only: pick_eqv)


309 
hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp


310 
with a show ?thesis by simp


311 
qed


312 


313 
end
