|
1 theory Quotients |
|
2 imports Main |
|
3 begin |
|
4 |
|
5 definition |
|
6 "REFL E \<equiv> \<forall>x. E x x" |
|
7 |
|
8 definition |
|
9 "SYM E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x" |
|
10 |
|
11 definition |
|
12 "TRANS E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z" |
|
13 |
|
14 definition |
|
15 "NONEMPTY E \<equiv> \<exists>x. E x x" |
|
16 |
|
17 definition |
|
18 "EQUIV E \<equiv> REFL E \<and> SYM E \<and> TRANS E" |
|
19 |
|
20 definition |
|
21 "EQUIV_PROP E \<equiv> (\<forall>x y. E x y = (E x = E y))" |
|
22 |
|
23 lemma EQUIV_PROP_EQUALITY: |
|
24 shows "EQUIV_PROP (op =)" |
|
25 unfolding EQUIV_PROP_def expand_fun_eq |
|
26 by (blast) |
|
27 |
|
28 lemma EQUIV_implies_EQUIV_PROP: |
|
29 assumes a: "REFL E" |
|
30 and b: "SYM E" |
|
31 and c: "TRANS E" |
|
32 shows "EQUIV_PROP E" |
|
33 using a b c |
|
34 unfolding EQUIV_PROP_def REFL_def SYM_def TRANS_def expand_fun_eq |
|
35 by (metis) |
|
36 |
|
37 lemma EQUIV_PROP_implies_REFL: |
|
38 assumes a: "EQUIV_PROP E" |
|
39 shows "REFL E" |
|
40 using a |
|
41 unfolding EQUIV_PROP_def REFL_def expand_fun_eq |
|
42 by (metis) |
|
43 |
|
44 lemma EQUIV_PROP_implies_SYM: |
|
45 assumes a: "EQUIV_PROP E" |
|
46 shows "SYM E" |
|
47 using a |
|
48 unfolding EQUIV_PROP_def SYM_def expand_fun_eq |
|
49 by (metis) |
|
50 |
|
51 lemma EQUIV_PROP_implies_TRANS: |
|
52 assumes a: "EQUIV_PROP E" |
|
53 shows "TRANS E" |
|
54 using a |
|
55 unfolding EQUIV_PROP_def TRANS_def expand_fun_eq |
|
56 by (blast) |
|
57 |
|
58 ML {* |
|
59 fun equiv_refl thm = thm RS @{thm EQUIV_PROP_implies_REFL} |
|
60 fun equiv_sym thm = thm RS @{thm EQUIV_PROP_implies_SYM} |
|
61 fun equiv_trans thm = thm RS @{thm EQUIV_PROP_implies_TRANS} |
|
62 |
|
63 fun refl_sym_trans_equiv thm1 thm2 thm3 = [thm1,thm2,thm3] MRS @{thm EQUIV_implies_EQUIV_PROP} |
|
64 *} |
|
65 |
|
66 |
|
67 fun |
|
68 LIST_REL |
|
69 where |
|
70 "LIST_REL R [] [] = True" |
|
71 | "LIST_REL R (x#xs) [] = False" |
|
72 | "LIST_REL R [] (x#xs) = False" |
|
73 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)" |
|
74 |
|
75 fun |
|
76 OPTION_REL |
|
77 where |
|
78 "OPTION_REL R None None = True" |
|
79 | "OPTION_REL R (Some x) None = False" |
|
80 | "OPTION_REL R None (Some x) = False" |
|
81 | "OPTION_REL R (Some x) (Some y) = R x y" |
|
82 |
|
83 fun |
|
84 option_map |
|
85 where |
|
86 "option_map f None = None" |
|
87 | "option_map f (Some x) = Some (f x)" |
|
88 |
|
89 fun |
|
90 PROD_REL |
|
91 where |
|
92 "PROD_REL R1 R2 (a1,a2) (b1,b2) = (R1 a1 b1 \<and> R2 a2 b2)" |
|
93 |
|
94 fun |
|
95 prod_map |
|
96 where |
|
97 "prod_map f1 f2 (a,b) = (f1 a, f2 b)" |
|
98 |
|
99 fun |
|
100 SUM_REL |
|
101 where |
|
102 "SUM_REL R1 R2 (Inl a1) (Inl b1) = R1 a1 b1" |
|
103 | "SUM_REL R1 R2 (Inl a1) (Inr b2) = False" |
|
104 | "SUM_REL R1 R2 (Inr a2) (Inl b1) = False" |
|
105 | "SUM_REL R1 R2 (Inr a2) (Inr b2) = R2 a2 b2" |
|
106 |
|
107 fun |
|
108 sum_map |
|
109 where |
|
110 "sum_map f1 f2 (Inl a) = Inl (f1 a)" |
|
111 | "sum_map f1 f2 (Inr a) = Inr (f2 a)" |
|
112 |
|
113 fun |
|
114 FUN_REL |
|
115 where |
|
116 "FUN_REL R1 R2 f g = (\<forall>x y. R1 x y \<longrightarrow> R2 (f x) (g y))" |
|
117 |
|
118 fun |
|
119 fun_map |
|
120 where |
|
121 "fun_map f g h x = g (h (f x))" |
|
122 |
|
123 definition |
|
124 "QUOTIENT_ABS_REP Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a)" |
|
125 |
|
126 |
|
127 |
|
128 definition |
|
129 "QUOTIENT R Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> |
|
130 (\<forall>a. R (Rep a) (Rep a)) \<and> |
|
131 (\<forall>r s. R r s = (R r r \<and> R s s \<and> (Abs r = Abs s)))" |
|
132 |
|
133 lemma QUOTIENT_ID: |
|
134 shows "QUOTIENT (op =) id id" |
|
135 unfolding QUOTIENT_def id_def |
|
136 by (blast) |
|
137 |
|
138 lemma QUOTIENT_PROD: |
|
139 assumes a: "QUOTIENT E1 Abs1 Rep1" |
|
140 and b: "QUOTIENT E2 Abs2 Rep2" |
|
141 shows "QUOTIENT (PROD_REL E1 e2) (prod_map Abs1 Abs2) (prod_map Rep1 rep2)" |
|
142 using a b unfolding QUOTIENT_def |
|
143 oops |
|
144 |
|
145 lemma QUOTIENT_ABS_REP_LIST: |
|
146 assumes a: "QUOTIENT_ABS_REP Abs Rep" |
|
147 shows "QUOTIENT_ABS_REP (map Abs) (map Rep)" |
|
148 using a |
|
149 unfolding QUOTIENT_ABS_REP_def |
|
150 apply(rule_tac allI) |
|
151 apply(induct_tac a rule: list.induct) |
|
152 apply(auto) |
|
153 done |
|
154 |
|
155 definition |
|
156 eqclass ("[_]_") |
|
157 where |
|
158 "[x]E \<equiv> E x" |
|
159 |
|
160 definition |
|
161 QUOTIENT_SET :: "'a set \<Rightarrow> ('a \<Rightarrow>'a\<Rightarrow>bool) \<Rightarrow> ('a set) set" ("_'/#'/_") |
|
162 where |
|
163 "S/#/E = {[x]E | x. x\<in>S}" |
|
164 |
|
165 definition |
|
166 QUOTIENT_UNIV |
|
167 where |
|
168 "QUOTIENT_UNIV TYPE('a) E \<equiv> (UNIV::'a set)/#/E" |
|
169 |
|
170 consts MY::"'a\<Rightarrow>'a\<Rightarrow>bool" |
|
171 axioms my1: "REFL MY" |
|
172 axioms my2: "SYM MY" |
|
173 axioms my3: "TRANS MY" |
|
174 |
|
175 term "QUOTIENT_UNIV TYPE('a) MY" |
|
176 term "\<lambda>f. \<exists>x. f = [x]MY" |
|
177 |
|
178 typedef 'a quot = "\<lambda>f::'a\<Rightarrow>bool. \<exists>x. f = [x]MY" |
|
179 by (auto simp add: mem_def) |
|
180 |
|
181 thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot |
|
182 thm Abs_quot_cases Rep_quot_cases Abs_quot_induct Rep_quot_induct |
|
183 |
|
184 lemma lem2: |
|
185 shows "([x]MY = [y]MY) = MY x y" |
|
186 apply(rule iffI) |
|
187 apply(simp add: eqclass_def) |
|
188 using my1 |
|
189 apply(auto simp add: REFL_def)[1] |
|
190 apply(simp add: eqclass_def expand_fun_eq) |
|
191 apply(rule allI) |
|
192 apply(rule iffI) |
|
193 apply(subgoal_tac "MY y x") |
|
194 using my3 |
|
195 apply(simp add: TRANS_def)[1] |
|
196 apply(drule_tac x="y" in spec) |
|
197 apply(drule_tac x="x" in spec) |
|
198 apply(drule_tac x="xa" in spec) |
|
199 apply(simp) |
|
200 using my2 |
|
201 apply(simp add: SYM_def)[1] |
|
202 oops |
|
203 |
|
204 lemma lem6: |
|
205 "\<forall>a. \<exists>r. Rep_quot a = [r]MY" |
|
206 apply(rule allI) |
|
207 apply(subgoal_tac "Rep_quot a \<in> quot") |
|
208 apply(simp add: quot_def mem_def) |
|
209 apply(rule Rep_quot) |
|
210 done |
|
211 |
|
212 lemma lem7: |
|
213 "\<forall>x y. (Abs_quot ([x]MY) = Abs_quot ([y]MY)) = ([x]MY = [y]MY)" |
|
214 apply(subst Abs_quot_inject) |
|
215 apply(unfold quot_def mem_def) |
|
216 apply(auto) |
|
217 done |
|
218 |
|
219 definition |
|
220 "Abs x = Abs_quot ([x]MY)" |
|
221 |
|
222 definition |
|
223 "Rep a = Eps (Rep_quot a)" |
|
224 |
|
225 lemma lem9: |
|
226 "\<forall>r. [(Eps [r]MY)]MY = [r]MY" |
|
227 apply(rule allI) |
|
228 apply(subgoal_tac "MY r r \<Longrightarrow> MY r (Eps (MY r))") |
|
229 apply(drule meta_mp) |
|
230 apply(rule eq1[THEN spec]) |
|
231 |
|
232 |
|
233 apply(rule_tac x="MY r" in someI) |
|
234 |
|
235 lemma |
|
236 "(f \<in> UNIV/#/MY) = (Rep_quot (Abs_quot f) = f)" |
|
237 apply(simp add: QUOTIENT_SET_def) |
|
238 apply(auto) |
|
239 apply(subgoal_tac "[x]MY \<in> quot") |
|
240 apply(simp add: Abs_quot_inverse) |
|
241 apply(simp add: quot_def) |
|
242 apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def) |
|
243 apply(auto)[1] |
|
244 apply(subgoal_tac "[x]MY \<in> quot") |
|
245 apply(simp add: Abs_quot_inverse) |
|
246 apply(simp add: quot_def) |
|
247 apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def) |
|
248 apply(auto)[1] |
|
249 apply(subst expand_set_eq) |
|
250 thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot |
|
251 |
|
252 lemma |
|
253 "\<forall>a. \<exists>r. Rep_quot a = [r]MY" |
|
254 apply(rule allI) |
|
255 apply(subst Abs_quot_inject[symmetric]) |
|
256 apply(rule Rep_quot) |
|
257 apply(simp add: quot_def) |
|
258 apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def) |
|
259 apply(auto)[1] |
|
260 apply(simp add: Rep_quot_inverse) |
|
261 thm Abs_quot_inverse Rep_quot_inverse Abs_quot_inject Rep_quot_inject Rep_quot |
|
262 apply(subst Abs_quot_inject[symmetric]) |
|
263 proof - |
|
264 have "[r]MY \<in> quot" |
|
265 apply(simp add: quot_def) |
|
266 apply(simp add: QUOTIENT_UNIV_def QUOTIENT_SET_def) |
|
267 apply(auto) |
|
268 |
|
269 thm Abs_quot_inverse |
|
270 |
|
271 |
|
272 thm Abs_quot_inverse |
|
273 apply(simp add: Rep_quot_inverse) |
|
274 |
|
275 |
|
276 thm Rep_quot_inverse |
|
277 |
|
278 term "" |
|
279 |
|
280 lemma |
|
281 assumes a: "EQUIV2 E" |
|
282 shows "([x]E = [y]E) = E x y" |
|
283 using a |
|
284 by (simp add: eqclass_def EQUIV2_def) |
|
285 |
|
286 |
|
287 |
|
288 |
|
289 |
|
290 lemma |
|
291 shows "QUOTIENT (op =) (\<lambda>x. x) (\<lambda>x. x)" |
|
292 apply(unfold QUOTIENT_def) |
|
293 apply(blast) |
|
294 done |
|
295 |
|
296 definition |
|
297 fun_app ("_ ---> _") |
|
298 where |
|
299 "f ---> g \<equiv> \<lambda>h x. g (h (f x))" |
|
300 |
|
301 lemma helper: |
|
302 assumes q: "QUOTIENT R ab re" |
|
303 and a: "R z z" |
|
304 shows "R (re (ab z)) z" |
|
305 using q a |
|
306 apply(unfold QUOTIENT_def)[1] |
|
307 apply(blast) |
|
308 done |
|
309 |
|
310 |
|
311 lemma |
|
312 assumes q1: "QUOTIENT R1 abs1 rep1" |
|
313 and q2: "QUOTIENT R2 abs2 rep2" |
|
314 shows "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
|
315 proof - |
|
316 have "\<forall>a. (rep1 ---> abs2) ((abs1 ---> rep2) a) = a" |
|
317 apply(simp add: expand_fun_eq) |
|
318 apply(simp add: fun_app_def) |
|
319 using q1 q2 |
|
320 apply(simp add: QUOTIENT_def) |
|
321 done |
|
322 moreover |
|
323 have "\<forall>a. (R1 ===> R2) ((abs1 ---> rep2) a) ((abs1 ---> rep2) a)" |
|
324 apply(simp add: FUN_REL_def) |
|
325 apply(auto) |
|
326 apply(simp add: fun_app_def) |
|
327 using q1 q2 |
|
328 apply(unfold QUOTIENT_def) |
|
329 apply(metis) |
|
330 done |
|
331 moreover |
|
332 have "\<forall>r s. (R1 ===> R2) r s = ((R1 ===> R2) r r \<and> (R1 ===> R2) s s \<and> |
|
333 (rep1 ---> abs2) r = (rep1 ---> abs2) s)" |
|
334 apply(simp add: expand_fun_eq) |
|
335 apply(rule allI)+ |
|
336 apply(rule iffI) |
|
337 using q1 q2 |
|
338 apply(unfold QUOTIENT_def)[1] |
|
339 apply(unfold fun_app_def)[1] |
|
340 apply(unfold FUN_REL_def)[1] |
|
341 apply(rule conjI) |
|
342 apply(metis) |
|
343 apply(rule conjI) |
|
344 apply(metis) |
|
345 apply(metis) |
|
346 apply(erule conjE) |
|
347 apply(simp (no_asm) add: FUN_REL_def) |
|
348 apply(rule allI impI)+ |
|
349 apply(subgoal_tac "R1 x x \<and> R1 y y \<and> abs1 x = abs1 y")(*A*) |
|
350 using q2 |
|
351 apply(unfold QUOTIENT_def)[1] |
|
352 apply(unfold fun_app_def)[1] |
|
353 apply(unfold FUN_REL_def)[1] |
|
354 apply(subgoal_tac "R2 (r x) (r x)")(*B*) |
|
355 apply(subgoal_tac "R2 (s y) (s y)")(*C*) |
|
356 apply(subgoal_tac "abs2 (r x) = abs2 (s y)")(*D*) |
|
357 apply(blast) |
|
358 (*D*) |
|
359 apply(metis helper q1) |
|
360 (*C*) |
|
361 apply(blast) |
|
362 (*B*) |
|
363 apply(blast) |
|
364 (*A*) |
|
365 using q1 |
|
366 apply(unfold QUOTIENT_def)[1] |
|
367 apply(unfold fun_app_def)[1] |
|
368 apply(unfold FUN_REL_def)[1] |
|
369 apply(metis) |
|
370 done |
|
371 ultimately |
|
372 show "QUOTIENT (R1 ===> R2) (rep1 ---> abs2) (abs1 ---> rep2)" |
|
373 apply(unfold QUOTIENT_def)[1] |
|
374 apply(blast) |
|
375 done |
|
376 qed |
|
377 |
|
378 |
|
379 |
|
380 |
|
381 |
|
382 |
|
383 |
|
384 definition |
|
385 "USER R \<equiv> NONEMPTY R \<and> |
|
386 |
|
387 |
|
388 |
|
389 typedecl tau |
|
390 consts R::"tau \<Rightarrow> tau \<Rightarrow> bool" |
|
391 |
|
392 |
|
393 |
|
394 definition |
|
395 FACTOR :: "'a set \<Rightarrow> ('a \<times>'a \<Rightarrow> bool) \<Rightarrow> ('a set) set" ("_ '/'/'/ _") |
|
396 where |
|
397 "A /// r \<equiv> \<Union>x\<in>A. {r``{x}}" |
|
398 |
|
399 typedef qtau = "\<lambda>c::tau\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))" |
|
400 apply(rule exI) |
|
401 |
|
402 apply(rule_tac x="R x" in exI) |
|
403 apply(auto) |
|
404 |
|
405 definition |
|
406 "QUOT TYPE('a) R \<equiv> \<lambda>c::'a\<Rightarrow>bool. (\<exists>x. R x x \<and> (c = R x))" |
|
407 |
|
408 |
|
409 |
|
410 |
|
411 |
|
412 |