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 |
249 apply(rule_tac iffI) |
249 apply(rule_tac iffI) |
250 using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
250 using fun_quotient[OF q1 q2] r1 r2 unfolding Quotient_def Respects_def |
251 apply(metis fun_rel_IMP) |
251 apply(metis fun_rel_IMP) |
252 using r1 unfolding Respects_def expand_fun_eq |
252 using r1 unfolding Respects_def expand_fun_eq |
253 apply(simp (no_asm_use)) |
253 apply(simp (no_asm_use)) |
254 apply(metis Quotient_REL[OF q2] Quotient_REL_REP[OF q1]) |
254 apply(metis Quotient_rel[OF q2] Quotient_REL_REP[OF q1]) |
255 done |
255 done |
256 |
256 |
257 (* ask Peter: fun_rel_IMP used twice *) |
257 (* ask Peter: fun_rel_IMP used twice *) |
258 lemma fun_rel_IMP2: |
258 lemma fun_rel_IMP2: |
259 assumes q1: "Quotient R1 Abs1 Rep1" |
259 assumes q1: "Quotient R1 Abs1 Rep1" |
326 |
326 |
327 lemma REP_ABS_RSP: |
327 lemma REP_ABS_RSP: |
328 assumes q: "Quotient R Abs Rep" |
328 assumes q: "Quotient R Abs Rep" |
329 and a: "R x1 x2" |
329 and a: "R x1 x2" |
330 shows "R x1 (Rep (Abs x2))" |
330 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]) |
331 using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q]) |
332 |
332 |
333 (* Not used *) |
333 (* Not used *) |
334 lemma REP_ABS_RSP_LEFT: |
334 lemma REP_ABS_RSP_LEFT: |
335 assumes q: "Quotient R Abs Rep" |
335 assumes q: "Quotient R Abs Rep" |
336 and a: "R x1 x2" |
336 and a: "R x1 x2" |
337 shows "R x1 (Rep (Abs x2))" |
337 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]) |
338 using q a by (metis Quotient_rel[OF q] Quotient_ABS_REP[OF q] Quotient_REP_reflp[OF q]) |
339 |
339 |
340 (* ----------------------------------------------------- *) |
340 (* ----------------------------------------------------- *) |
341 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
341 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
342 (* Ball, Bex, RES_EXISTS_EQUIV *) |
342 (* Ball, Bex, RES_EXISTS_EQUIV *) |
343 (* ----------------------------------------------------- *) |
343 (* ----------------------------------------------------- *) |