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 |
|
10311
|
57 |
theorem quot_exhaust: "\<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 |
|
10311
|
65 |
lemma quot_cases [cases type: quot]: "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C"
|
|
66 |
by (insert quot_exhaust) blast
|
10250
|
67 |
|
|
68 |
|
10285
|
69 |
subsection {* Equality on quotients *}
|
10250
|
70 |
|
|
71 |
text {*
|
10286
|
72 |
Equality of canonical quotient elements coincides with the original
|
|
73 |
relation.
|
10250
|
74 |
*}
|
|
75 |
|
10285
|
76 |
theorem equivalence_class_eq [iff?]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)"
|
|
77 |
proof
|
|
78 |
assume eq: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
|
|
79 |
show "a \<sim> b"
|
|
80 |
proof -
|
|
81 |
from eq have "{x. a \<sim> x} = {x. b \<sim> x}"
|
|
82 |
by (simp only: equivalence_class_def Abs_quot_inject quotI)
|
|
83 |
moreover have "a \<sim> a" ..
|
|
84 |
ultimately have "a \<in> {x. b \<sim> x}" by blast
|
|
85 |
hence "b \<sim> a" by blast
|
|
86 |
thus ?thesis ..
|
|
87 |
qed
|
|
88 |
next
|
10250
|
89 |
assume ab: "a \<sim> b"
|
10285
|
90 |
show "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>"
|
|
91 |
proof -
|
|
92 |
have "{x. a \<sim> x} = {x. b \<sim> x}"
|
|
93 |
proof (rule Collect_cong)
|
|
94 |
fix x show "(a \<sim> x) = (b \<sim> x)"
|
|
95 |
proof
|
|
96 |
from ab have "b \<sim> a" ..
|
|
97 |
also assume "a \<sim> x"
|
|
98 |
finally show "b \<sim> x" .
|
|
99 |
next
|
|
100 |
note ab
|
|
101 |
also assume "b \<sim> x"
|
|
102 |
finally show "a \<sim> x" .
|
|
103 |
qed
|
10250
|
104 |
qed
|
10285
|
105 |
thus ?thesis by (simp only: equivalence_class_def)
|
10250
|
106 |
qed
|
|
107 |
qed
|
|
108 |
|
|
109 |
|
10285
|
110 |
subsection {* Picking representing elements *}
|
10250
|
111 |
|
|
112 |
constdefs
|
10285
|
113 |
pick :: "'a::equiv quot => 'a"
|
10250
|
114 |
"pick A == SOME a. A = \<lfloor>a\<rfloor>"
|
|
115 |
|
10285
|
116 |
theorem pick_equiv [intro]: "pick \<lfloor>a\<rfloor> \<sim> a"
|
10250
|
117 |
proof (unfold pick_def)
|
|
118 |
show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a"
|
|
119 |
proof (rule someI2)
|
|
120 |
show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" ..
|
|
121 |
fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>"
|
10285
|
122 |
hence "a \<sim> x" .. thus "x \<sim> a" ..
|
10250
|
123 |
qed
|
|
124 |
qed
|
|
125 |
|
10285
|
126 |
theorem pick_inverse: "\<lfloor>pick A\<rfloor> = A"
|
10250
|
127 |
proof (cases A)
|
|
128 |
fix a assume a: "A = \<lfloor>a\<rfloor>"
|
10285
|
129 |
hence "pick A \<sim> a" by (simp only: pick_equiv)
|
|
130 |
hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" ..
|
10250
|
131 |
with a show ?thesis by simp
|
|
132 |
qed
|
|
133 |
|
10285
|
134 |
text {*
|
|
135 |
\medskip The following rules support canonical function definitions
|
|
136 |
on quotient types.
|
|
137 |
*}
|
|
138 |
|
|
139 |
theorem cong_definition1:
|
|
140 |
"(!!X. f X == g (pick X)) ==>
|
|
141 |
(!!x x'. x \<sim> x' ==> g x = g x') ==>
|
|
142 |
f \<lfloor>a\<rfloor> = g a"
|
|
143 |
proof -
|
|
144 |
assume cong: "!!x x'. x \<sim> x' ==> g x = g x'"
|
|
145 |
assume "!!X. f X == g (pick X)"
|
|
146 |
hence "f \<lfloor>a\<rfloor> = g (pick \<lfloor>a\<rfloor>)" by (simp only:)
|
|
147 |
also have "\<dots> = g a"
|
|
148 |
proof (rule cong)
|
|
149 |
show "pick \<lfloor>a\<rfloor> \<sim> a" ..
|
|
150 |
qed
|
|
151 |
finally show ?thesis .
|
|
152 |
qed
|
|
153 |
|
|
154 |
theorem cong_definition2:
|
|
155 |
"(!!X Y. f X Y == g (pick X) (pick Y)) ==>
|
|
156 |
(!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y') ==>
|
|
157 |
f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g a b"
|
|
158 |
proof -
|
|
159 |
assume cong: "!!x x' y y'. x \<sim> x' ==> y \<sim> y' ==> g x y = g x' y'"
|
|
160 |
assume "!!X Y. f X Y == g (pick X) (pick Y)"
|
|
161 |
hence "f \<lfloor>a\<rfloor> \<lfloor>b\<rfloor> = g (pick \<lfloor>a\<rfloor>) (pick \<lfloor>b\<rfloor>)" by (simp only:)
|
|
162 |
also have "\<dots> = g a b"
|
|
163 |
proof (rule cong)
|
|
164 |
show "pick \<lfloor>a\<rfloor> \<sim> a" ..
|
|
165 |
show "pick \<lfloor>b\<rfloor> \<sim> b" ..
|
|
166 |
qed
|
|
167 |
finally show ?thesis .
|
|
168 |
qed
|
|
169 |
|
10250
|
170 |
end
|