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 {*

10285

14 
We introduce the notion of quotient types over equivalence relations


15 
via axiomatic type classes.

10250

16 
*}


17 

10285

18 
subsection {* Equivalence relations and quotient types *}

10250

19 


20 
text {*

10285

21 
\medskip Type class @{text equiv} models equivalence relations using


22 
the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation.

10250

23 
*}


24 

10285

25 
axclass eqv < "term"


26 
consts


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

10250

28 

10285

29 
axclass equiv < eqv


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


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


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

10250

33 


34 
text {*

10285

35 
\medskip The quotient type @{text "'a quot"} consists of all


36 
\emph{equivalence classes} over elements of the base type @{typ 'a}.

10250

37 
*}


38 

10285

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

10250

40 
by blast


41 


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


43 
by (unfold quot_def) blast


44 


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


46 
by (unfold quot_def) blast


47 


48 
text {*


49 
\medskip Abstracted equivalence classes are the canonical


50 
representation of elements of a quotient type.


51 
*}


52 


53 
constdefs

10285

54 
equivalence_class :: "'a::equiv => 'a quot" ("\<lfloor>_\<rfloor>")

10250

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


56 


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

10278

58 
proof (cases A)


59 
fix R assume R: "A = Abs_quot R"


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


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

10285

62 
thus ?thesis by (unfold equivalence_class_def)

10250

63 
qed


64 


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


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


67 
by (insert quot_rep) blast


68 


69 

10285

70 
subsection {* Equality on quotients *}

10250

71 


72 
text {*

10286

73 
Equality of canonical quotient elements coincides with the original


74 
relation.

10250

75 
*}


76 

10285

77 
theorem equivalence_class_eq [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"


78 
proof


79 
assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"


80 
show "a \<sim> b"


81 
proof 


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


83 
by (simp only: equivalence_class_def Abs_quot_inject quotI)


84 
moreover have "a \<sim> a" ..


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


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


87 
thus ?thesis ..


88 
qed


89 
next

10250

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

10285

91 
show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"


92 
proof 


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


94 
proof (rule Collect_cong)


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


96 
proof


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


98 
also assume "a \<sim> x"


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


100 
next


101 
note ab


102 
also assume "b \<sim> x"


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


104 
qed

10250

105 
qed

10285

106 
thus ?thesis by (simp only: equivalence_class_def)

10250

107 
qed


108 
qed


109 


110 

10285

111 
subsection {* Picking representing elements *}

10250

112 


113 
constdefs

10285

114 
pick :: "'a::equiv quot => 'a"

10250

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


116 

10285

117 
theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"

10250

118 
proof (unfold pick_def)


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


120 
proof (rule someI2)


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


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

10285

123 
hence "a \<sim> x" .. thus "x \<sim> a" ..

10250

124 
qed


125 
qed


126 

10285

127 
theorem pick_inverse: "\<lfloor>pick A\<rfloor> = A"

10250

128 
proof (cases A)


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

10285

130 
hence "pick A \<sim> a" by (simp only: pick_equiv)


131 
hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..

10250

132 
with a show ?thesis by simp


133 
qed


134 

10285

135 
text {*


136 
\medskip The following rules support canonical function definitions


137 
on quotient types.


138 
*}


139 


140 
theorem cong_definition1:


141 
"(!!X. f X == g (pick X)) ==>


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


143 
f \<lfloor>a\<rfloor> = g a"


144 
proof 


145 
assume cong: "!!x x'. x \<sim> x' ==> g x = g x'"


146 
assume "!!X. f X == g (pick X)"


147 
hence "f \<lfloor>a\<rfloor> = g (pick \<lfloor>a\<rfloor>)" by (simp only:)


148 
also have "\<dots> = g a"


149 
proof (rule cong)


150 
show "pick \<lfloor>a\<rfloor> \<sim> a" ..


151 
qed


152 
finally show ?thesis .


153 
qed


154 


155 
theorem cong_definition2:


156 
"(!!X Y. f X Y == g (pick X) (pick Y)) ==>


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


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


159 
proof 


160 
assume cong: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y'"


161 
assume "!!X Y. f X Y == g (pick X) (pick Y)"


162 
hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)


163 
also have "\<dots> = g a b"


164 
proof (rule cong)


165 
show "pick \<lfloor>a\<rfloor> \<sim> a" ..


166 
show "pick \<lfloor>b\<rfloor> \<sim> b" ..


167 
qed


168 
finally show ?thesis .


169 
qed


170 

10250

171 
end
