|
1 (* Title: HOL/ex/PER.thy |
|
2 ID: $Id$ |
|
3 Author: Oscar Slotosch and Markus Wenzel, TU Muenchen |
|
4 *) |
|
5 |
|
6 header {* Partial equivalence relations *} |
|
7 |
|
8 theory PER = Main: |
|
9 |
|
10 text {* |
|
11 Higher-order quotients are defined over partial equivalence relations |
|
12 (PERs) instead of total ones. We provide axiomatic type classes |
|
13 @{text "equiv < partial_equiv"} and a type constructor |
|
14 @{text "'a quot"} with basic operations. This development is based |
|
15 on: |
|
16 |
|
17 Oscar Slotosch: \emph{Higher Order Quotients and their Implementation |
|
18 in Isabelle HOL.} Elsa L. Gunter and Amy Felty, editors, Theorem |
|
19 Proving in Higher Order Logics: TPHOLs '97, Springer LNCS 1275, 1997. |
|
20 *} |
|
21 |
|
22 |
|
23 subsection {* Partial equivalence *} |
|
24 |
|
25 text {* |
|
26 Type class @{text partial_equiv} models partial equivalence relations |
|
27 (PERs) using the polymorphic @{text "\<sim> :: 'a => 'a => bool"} relation, |
|
28 which is required to be symmetric and transitive, but not necessarily |
|
29 reflexive. |
|
30 *} |
|
31 |
|
32 consts |
|
33 eqv :: "'a => 'a => bool" (infixl "\<sim>" 50) |
|
34 |
|
35 axclass partial_equiv < "term" |
|
36 partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x" |
|
37 partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z" |
|
38 |
|
39 text {* |
|
40 \medskip The domain of a partial equivalence relation is the set of |
|
41 reflexive elements. Due to symmetry and transitivity this |
|
42 characterizes exactly those elements that are connected with |
|
43 \emph{any} other one. |
|
44 *} |
|
45 |
|
46 constdefs |
|
47 domain :: "'a::partial_equiv set" |
|
48 "domain == {x. x \<sim> x}" |
|
49 |
|
50 lemma domainI [intro]: "x \<sim> x ==> x \<in> domain" |
|
51 by (unfold domain_def) blast |
|
52 |
|
53 lemma domainD [dest]: "x \<in> domain ==> x \<sim> x" |
|
54 by (unfold domain_def) blast |
|
55 |
|
56 theorem domainI' [elim?]: "x \<sim> y ==> x \<in> domain" |
|
57 proof |
|
58 assume xy: "x \<sim> y" |
|
59 also from xy have "y \<sim> x" .. |
|
60 finally show "x \<sim> x" . |
|
61 qed |
|
62 |
|
63 |
|
64 subsection {* Equivalence on function spaces *} |
|
65 |
|
66 text {* |
|
67 The @{text \<sim>} relation is lifted to function spaces. It is |
|
68 important to note that this is \emph{not} the direct product, but a |
|
69 structural one corresponding to the congruence property. |
|
70 *} |
|
71 |
|
72 defs (overloaded) |
|
73 eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y" |
|
74 |
|
75 lemma partial_equiv_funI [intro?]: |
|
76 "(!!x y. x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y) ==> f \<sim> g" |
|
77 by (unfold eqv_fun_def) blast |
|
78 |
|
79 lemma partial_equiv_funD [dest?]: |
|
80 "f \<sim> g ==> x \<in> domain ==> y \<in> domain ==> x \<sim> y ==> f x \<sim> g y" |
|
81 by (unfold eqv_fun_def) blast |
|
82 |
|
83 text {* |
|
84 The class of partial equivalence relations is closed under function |
|
85 spaces (in \emph{both} argument positions). |
|
86 *} |
|
87 |
|
88 instance fun :: (partial_equiv, partial_equiv) partial_equiv |
|
89 proof |
|
90 fix f g h :: "'a::partial_equiv => 'b::partial_equiv" |
|
91 assume fg: "f \<sim> g" |
|
92 show "g \<sim> f" |
|
93 proof |
|
94 fix x y :: 'a |
|
95 assume x: "x \<in> domain" and y: "y \<in> domain" |
|
96 assume "x \<sim> y" hence "y \<sim> x" .. |
|
97 with fg y x have "f y \<sim> g x" .. |
|
98 thus "g x \<sim> f y" .. |
|
99 qed |
|
100 assume gh: "g \<sim> h" |
|
101 show "f \<sim> h" |
|
102 proof |
|
103 fix x y :: 'a |
|
104 assume x: "x \<in> domain" and y: "y \<in> domain" and "x \<sim> y" |
|
105 with fg have "f x \<sim> g y" .. |
|
106 also from y have "y \<sim> y" .. |
|
107 with gh y y have "g y \<sim> h y" .. |
|
108 finally show "f x \<sim> h y" . |
|
109 qed |
|
110 qed |
|
111 |
|
112 |
|
113 subsection {* Total equivalence *} |
|
114 |
|
115 text {* |
|
116 The class of total equivalence relations on top of PERs. It |
|
117 coincides with the standard notion of equivalence, i.e.\ |
|
118 @{text "\<sim> :: 'a => 'a => bool"} is required to be reflexive, transitive |
|
119 and symmetric. |
|
120 *} |
|
121 |
|
122 axclass equiv < partial_equiv |
|
123 eqv_refl [intro]: "x \<sim> x" |
|
124 |
|
125 text {* |
|
126 On total equivalences all elements are reflexive, and congruence |
|
127 holds unconditionally. |
|
128 *} |
|
129 |
|
130 theorem equiv_domain [intro]: "(x::'a::equiv) \<in> domain" |
|
131 proof |
|
132 show "x \<sim> x" .. |
|
133 qed |
|
134 |
|
135 theorem equiv_cong [dest?]: "f \<sim> g ==> x \<sim> y ==> f x \<sim> g (y::'a::equiv)" |
|
136 proof - |
|
137 assume "f \<sim> g" |
|
138 moreover have "x \<in> domain" .. |
|
139 moreover have "y \<in> domain" .. |
|
140 moreover assume "x \<sim> y" |
|
141 ultimately show ?thesis .. |
|
142 qed |
|
143 |
|
144 |
|
145 subsection {* Quotient types *} |
|
146 |
|
147 text {* |
|
148 The quotient type @{text "'a quot"} consists of all \emph{equivalence |
|
149 classes} over elements of the base type @{typ 'a}. |
|
150 *} |
|
151 |
|
152 typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}" |
|
153 by blast |
|
154 |
|
155 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot" |
|
156 by (unfold quot_def) blast |
|
157 |
|
158 lemma quotE [elim]: "R \<in> quot ==> (!!a. R = {x. a \<sim> x} ==> C) ==> C" |
|
159 by (unfold quot_def) blast |
|
160 |
|
161 text {* |
|
162 \medskip Abstracted equivalence classes are the canonical |
|
163 representation of elements of a quotient type. |
|
164 *} |
|
165 |
|
166 constdefs |
|
167 eqv_class :: "('a::partial_equiv) => 'a quot" ("\<lfloor>_\<rfloor>") |
|
168 "\<lfloor>a\<rfloor> == Abs_quot {x. a \<sim> x}" |
|
169 |
|
170 theorem quot_rep: "\<exists>a. A = \<lfloor>a\<rfloor>" |
|
171 proof (cases A) |
|
172 fix R assume R: "A = Abs_quot R" |
|
173 assume "R \<in> quot" hence "\<exists>a. R = {x. a \<sim> x}" by blast |
|
174 with R have "\<exists>a. A = Abs_quot {x. a \<sim> x}" by blast |
|
175 thus ?thesis by (unfold eqv_class_def) |
|
176 qed |
|
177 |
|
178 lemma quot_cases [case_names rep, cases type: quot]: |
|
179 "(!!a. A = \<lfloor>a\<rfloor> ==> C) ==> C" |
|
180 by (insert quot_rep) blast |
|
181 |
|
182 |
|
183 subsection {* Equality on quotients *} |
|
184 |
|
185 text {* |
|
186 Equality of canonical quotient elements corresponds to the original |
|
187 relation as follows. |
|
188 *} |
|
189 |
|
190 theorem eqv_class_eqI [intro]: "a \<sim> b ==> \<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>" |
|
191 proof - |
|
192 assume ab: "a \<sim> b" |
|
193 have "{x. a \<sim> x} = {x. b \<sim> x}" |
|
194 proof (rule Collect_cong) |
|
195 fix x show "(a \<sim> x) = (b \<sim> x)" |
|
196 proof |
|
197 from ab have "b \<sim> a" .. |
|
198 also assume "a \<sim> x" |
|
199 finally show "b \<sim> x" . |
|
200 next |
|
201 note ab |
|
202 also assume "b \<sim> x" |
|
203 finally show "a \<sim> x" . |
|
204 qed |
|
205 qed |
|
206 thus ?thesis by (simp only: eqv_class_def) |
|
207 qed |
|
208 |
|
209 theorem eqv_class_eqD' [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<in> domain ==> a \<sim> b" |
|
210 proof (unfold eqv_class_def) |
|
211 assume "Abs_quot {x. a \<sim> x} = Abs_quot {x. b \<sim> x}" |
|
212 hence "{x. a \<sim> x} = {x. b \<sim> x}" by (simp only: Abs_quot_inject quotI) |
|
213 moreover assume "a \<in> domain" hence "a \<sim> a" .. |
|
214 ultimately have "a \<in> {x. b \<sim> x}" by blast |
|
215 hence "b \<sim> a" by blast |
|
216 thus "a \<sim> b" .. |
|
217 qed |
|
218 |
|
219 theorem eqv_class_eqD [dest?]: "\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor> ==> a \<sim> (b::'a::equiv)" |
|
220 proof (rule eqv_class_eqD') |
|
221 show "a \<in> domain" .. |
|
222 qed |
|
223 |
|
224 lemma eqv_class_eq' [simp]: "a \<in> domain ==> (\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> b)" |
|
225 by (insert eqv_class_eqI eqv_class_eqD') blast |
|
226 |
|
227 lemma eqv_class_eq [simp]: "(\<lfloor>a\<rfloor> = \<lfloor>b\<rfloor>) = (a \<sim> (b::'a::equiv))" |
|
228 by (insert eqv_class_eqI eqv_class_eqD) blast |
|
229 |
|
230 |
|
231 subsection {* Picking representing elements *} |
|
232 |
|
233 constdefs |
|
234 pick :: "'a::partial_equiv quot => 'a" |
|
235 "pick A == SOME a. A = \<lfloor>a\<rfloor>" |
|
236 |
|
237 theorem pick_eqv' [intro?, simp]: "a \<in> domain ==> pick \<lfloor>a\<rfloor> \<sim> a" |
|
238 proof (unfold pick_def) |
|
239 assume a: "a \<in> domain" |
|
240 show "(SOME x. \<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>) \<sim> a" |
|
241 proof (rule someI2) |
|
242 show "\<lfloor>a\<rfloor> = \<lfloor>a\<rfloor>" .. |
|
243 fix x assume "\<lfloor>a\<rfloor> = \<lfloor>x\<rfloor>" |
|
244 hence "a \<sim> x" .. |
|
245 thus "x \<sim> a" .. |
|
246 qed |
|
247 qed |
|
248 |
|
249 theorem pick_eqv [intro, simp]: "pick \<lfloor>a\<rfloor> \<sim> (a::'a::equiv)" |
|
250 proof (rule pick_eqv') |
|
251 show "a \<in> domain" .. |
|
252 qed |
|
253 |
|
254 theorem pick_inverse: "\<lfloor>pick A\<rfloor> = (A::'a::equiv quot)" |
|
255 proof (cases A) |
|
256 fix a assume a: "A = \<lfloor>a\<rfloor>" |
|
257 hence "pick A \<sim> a" by simp |
|
258 hence "\<lfloor>pick A\<rfloor> = \<lfloor>a\<rfloor>" by simp |
|
259 with a show ?thesis by simp |
|
260 qed |
|
261 |
|
262 end |