26 lemma equivp_reflp: |
26 lemma equivp_reflp: |
27 shows "equivp E \<Longrightarrow> (\<And>x. E x x)" |
27 shows "equivp E \<Longrightarrow> (\<And>x. E x x)" |
28 by (simp add: equivp_reflp_symp_transp reflp_def) |
28 by (simp add: equivp_reflp_symp_transp reflp_def) |
29 |
29 |
30 definition |
30 definition |
31 "PART_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
31 "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))" |
32 |
32 |
33 lemma equivp_IMP_PART_equivp: |
33 lemma equivp_IMP_part_equivp: |
34 assumes a: "equivp E" |
34 assumes a: "equivp E" |
35 shows "PART_equivp E" |
35 shows "part_equivp E" |
36 using a unfolding equivp_def PART_equivp_def |
36 using a unfolding equivp_def part_equivp_def |
37 by auto |
37 by auto |
38 |
38 |
39 definition |
39 definition |
40 "Quotient E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> |
40 "Quotient E Abs Rep \<equiv> (\<forall>a. Abs (Rep a) = a) \<and> |
41 (\<forall>a. E (Rep a) (Rep a)) \<and> |
41 (\<forall>a. E (Rep a) (Rep a)) \<and> |
45 assumes a: "Quotient E Abs Rep" |
45 assumes a: "Quotient E Abs Rep" |
46 shows "Abs (Rep a) = a" |
46 shows "Abs (Rep a) = a" |
47 using a unfolding Quotient_def |
47 using a unfolding Quotient_def |
48 by simp |
48 by simp |
49 |
49 |
50 lemma Quotient_REP_reflp: |
50 lemma Quotient_rep_reflp: |
51 assumes a: "Quotient E Abs Rep" |
51 assumes a: "Quotient E Abs Rep" |
52 shows "E (Rep a) (Rep a)" |
52 shows "E (Rep a) (Rep a)" |
53 using a unfolding Quotient_def |
53 using a unfolding Quotient_def |
54 by blast |
54 by blast |
55 |
55 |
56 lemma Quotient_rel: |
56 lemma Quotient_rel: |
57 assumes a: "Quotient E Abs Rep" |
57 assumes a: "Quotient E Abs Rep" |
58 shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))" |
58 shows " E r s = (E r r \<and> E s s \<and> (Abs r = Abs s))" |
59 using a unfolding Quotient_def |
59 using a unfolding Quotient_def |
60 by blast |
60 by blast |
61 |
61 |
62 lemma Quotient_REL_ABS: |
62 lemma Quotient_rel_rep: |
63 assumes a: "Quotient E Abs Rep" |
|
64 shows "E r s \<Longrightarrow> Abs r = Abs s" |
|
65 using a unfolding Quotient_def |
|
66 by blast |
|
67 |
|
68 lemma Quotient_REL_ABS_EQ: |
|
69 assumes a: "Quotient E Abs Rep" |
|
70 shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)" |
|
71 using a unfolding Quotient_def |
|
72 by blast |
|
73 |
|
74 lemma Quotient_REL_REP: |
|
75 assumes a: "Quotient R Abs Rep" |
63 assumes a: "Quotient R Abs Rep" |
76 shows "R (Rep a) (Rep b) = (a = b)" |
64 shows "R (Rep a) (Rep b) \<equiv> (a = b)" |
|
65 apply (rule eq_reflection) |
77 using a unfolding Quotient_def |
66 using a unfolding Quotient_def |
78 by metis |
67 by metis |
79 |
68 |
80 lemma Quotient_rep_abs: |
69 lemma Quotient_rep_abs: |
81 assumes a: "Quotient R Abs Rep" |
70 assumes a: "Quotient R Abs Rep" |
249 apply(rule_tac iffI) |
238 apply(rule_tac iffI) |
250 using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
239 using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
251 apply(metis fun_rel_IMP) |
240 apply(metis fun_rel_IMP) |
252 using r1 unfolding Respects_def expand_fun_eq |
241 using r1 unfolding Respects_def expand_fun_eq |
253 apply(simp (no_asm_use)) |
242 apply(simp (no_asm_use)) |
254 apply(metis Quotient_rel[OF q2] Quotient_REL_REP[OF q1]) |
243 apply(metis Quotient_rel[OF q2] Quotient_rel_rep[OF q1]) |
255 done |
244 done |
256 |
245 |
257 (* ask Peter: fun_rel_IMP used twice *) |
246 (* ask Peter: fun_rel_IMP used twice *) |
258 lemma fun_rel_IMP2: |
247 lemma fun_rel_IMP2: |
259 assumes q1: "Quotient R1 Abs1 Rep1" |
248 assumes q1: "Quotient R1 Abs1 Rep1" |
262 and r2: "Respects (R1 ===> R2) g" |
251 and r2: "Respects (R1 ===> R2) g" |
263 and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" |
252 and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" |
264 shows "R1 x y \<Longrightarrow> R2 (f x) (g y)" |
253 shows "R1 x y \<Longrightarrow> R2 (f x) (g y)" |
265 using q1 q2 r1 r2 a |
254 using q1 q2 r1 r2 a |
266 by (simp add: fun_rel_EQUALS) |
255 by (simp add: fun_rel_EQUALS) |
267 |
|
268 (* We don't use it, it is exactly the same as Quotient_REL_REP but wrong way *) |
|
269 lemma EQUALS_PRS: |
|
270 assumes q: "Quotient R Abs Rep" |
|
271 shows "(x = y) = R (Rep x) (Rep y)" |
|
272 by (rule Quotient_REL_REP[OF q, symmetric]) |
|
273 |
256 |
274 lemma equals_rsp: |
257 lemma equals_rsp: |
275 assumes q: "Quotient R Abs Rep" |
258 assumes q: "Quotient R Abs Rep" |
276 and a: "R xa xb" "R ya yb" |
259 and a: "R xa xb" "R ya yb" |
277 shows "R xa ya = R xb yb" |
260 shows "R xa ya = R xb yb" |
326 |
309 |
327 lemma REP_ABS_RSP: |
310 lemma REP_ABS_RSP: |
328 assumes q: "Quotient R Abs Rep" |
311 assumes q: "Quotient R Abs Rep" |
329 and a: "R x1 x2" |
312 and a: "R x1 x2" |
330 shows "R x1 (Rep (Abs x2))" |
313 shows "R x1 (Rep (Abs x2))" |
331 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q]) |
314 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
332 |
315 |
333 (* Not used *) |
316 (* Not used *) |
334 lemma REP_ABS_RSP_LEFT: |
317 lemma REP_ABS_RSP_LEFT: |
335 assumes q: "Quotient R Abs Rep" |
318 assumes q: "Quotient R Abs Rep" |
336 and a: "R x1 x2" |
319 and a: "R x1 x2" |
337 shows "R x1 (Rep (Abs x2))" |
320 shows "R x1 (Rep (Abs x2))" |
338 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_REP_reflp[OF q]) |
321 using q a by (metis Quotient_rel[OF q] Quotient_abs_rep[OF q] Quotient_rep_reflp[OF q]) |
339 |
322 |
340 (* ----------------------------------------------------- *) |
323 (* ----------------------------------------------------- *) |
341 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
324 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
342 (* Ball, Bex, RES_EXISTS_EQUIV *) |
325 (* Ball, Bex, RES_EXISTS_EQUIV *) |
343 (* ----------------------------------------------------- *) |
326 (* ----------------------------------------------------- *) |
565 assumes a: "Quotient R absf repf" |
548 assumes a: "Quotient R absf repf" |
566 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
549 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
567 using a unfolding Quotient_def |
550 using a unfolding Quotient_def |
568 by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply) |
551 by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply) |
569 |
552 |
|
553 |
|
554 (* UNUSED *) |
|
555 lemma Quotient_rel_abs: |
|
556 assumes a: "Quotient E Abs Rep" |
|
557 shows "E r s \<Longrightarrow> Abs r = Abs s" |
|
558 using a unfolding Quotient_def |
|
559 by blast |
|
560 |
|
561 lemma Quotient_rel_abs_eq: |
|
562 assumes a: "Quotient E Abs Rep" |
|
563 shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)" |
|
564 using a unfolding Quotient_def |
|
565 by blast |
|
566 |
|
567 |
|
568 |
570 end |
569 end |
571 |
570 |