66 shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)" |
66 shows "E r r \<Longrightarrow> E s s \<Longrightarrow> E r s = (Abs r = Abs s)" |
67 using a unfolding QUOTIENT_def |
67 using a unfolding QUOTIENT_def |
68 by blast |
68 by blast |
69 |
69 |
70 lemma QUOTIENT_REL_REP: |
70 lemma QUOTIENT_REL_REP: |
71 assumes a: "QUOTIENT E Abs Rep" |
71 assumes a: "QUOTIENT R Abs Rep" |
72 shows "E (Rep a) (Rep b) = (a = b)" |
72 shows "R (Rep a) (Rep b) = (a = b)" |
73 using a unfolding QUOTIENT_def |
73 using a unfolding QUOTIENT_def |
74 by metis |
74 by metis |
75 |
75 |
76 lemma QUOTIENT_REP_ABS: |
76 lemma QUOTIENT_REP_ABS: |
77 assumes a: "QUOTIENT E Abs Rep" |
77 assumes a: "QUOTIENT R Abs Rep" |
78 shows "E r r \<Longrightarrow> E (Rep (Abs r)) r" |
78 shows "R r r \<Longrightarrow> R (Rep (Abs r)) r" |
79 using a unfolding QUOTIENT_def |
79 using a unfolding QUOTIENT_def |
80 by blast |
80 by blast |
81 |
81 |
82 lemma IDENTITY_EQUIV: |
82 lemma IDENTITY_EQUIV: |
83 shows "EQUIV (op =)" |
83 shows "EQUIV (op =)" |
258 and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" |
258 and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" |
259 shows "R1 x y \<Longrightarrow> R2 (f x) (g y)" |
259 shows "R1 x y \<Longrightarrow> R2 (f x) (g y)" |
260 using q1 q2 r1 r2 a |
260 using q1 q2 r1 r2 a |
261 by (simp add: FUN_REL_EQUALS) |
261 by (simp add: FUN_REL_EQUALS) |
262 |
262 |
|
263 (* We don't use it, it is exactly the same as QUOTIENT_REL_REP but wrong way *) |
263 lemma EQUALS_PRS: |
264 lemma EQUALS_PRS: |
264 assumes q: "QUOTIENT R Abs Rep" |
265 assumes q: "QUOTIENT R Abs Rep" |
265 shows "(x = y) = R (Rep x) (Rep y)" |
266 shows "(x = y) = R (Rep x) (Rep y)" |
266 by (simp add: QUOTIENT_REL_REP[OF q]) |
267 by (rule QUOTIENT_REL_REP[OF q, symmetric]) |
267 |
268 |
268 lemma EQUALS_RSP: |
269 lemma EQUALS_RSP: |
269 assumes q: "QUOTIENT R Abs Rep" |
270 assumes q: "QUOTIENT R Abs Rep" |
270 and a: "R x1 x2" "R y1 y2" |
271 and a: "R x1 x2" "R y1 y2" |
271 shows "R x1 y1 = R x2 y2" |
272 shows "R x1 y1 = R x2 y2" |
284 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
285 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
285 and q2: "QUOTIENT R2 Abs2 Rep2" |
286 and q2: "QUOTIENT R2 Abs2 Rep2" |
286 shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)" |
287 shows "(\<lambda>x. f x) = (Rep1 ---> Abs2) (\<lambda>x. (Abs1 ---> Rep2) f x)" |
287 unfolding expand_fun_eq |
288 unfolding expand_fun_eq |
288 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
289 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
289 by (simp) |
290 by simp |
290 |
291 |
|
292 (* Not used since applic_prs proves a version for an arbitrary number of arguments *) |
291 lemma APP_PRS: |
293 lemma APP_PRS: |
292 assumes q1: "QUOTIENT R1 abs1 rep1" |
294 assumes q1: "QUOTIENT R1 abs1 rep1" |
293 and q2: "QUOTIENT R2 abs2 rep2" |
295 and q2: "QUOTIENT R2 abs2 rep2" |
294 shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" |
296 shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" |
295 unfolding expand_fun_eq |
297 unfolding expand_fun_eq |
319 |
321 |
320 lemma REP_ABS_RSP: |
322 lemma REP_ABS_RSP: |
321 assumes q: "QUOTIENT R Abs Rep" |
323 assumes q: "QUOTIENT R Abs Rep" |
322 and a: "R x1 x2" |
324 and a: "R x1 x2" |
323 shows "R x1 (Rep (Abs x2))" |
325 shows "R x1 (Rep (Abs x2))" |
|
326 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) |
|
327 |
|
328 (* Not used *) |
|
329 lemma REP_ABS_RSP_LEFT: |
|
330 assumes q: "QUOTIENT R Abs Rep" |
|
331 and a: "R x1 x2" |
324 and "R (Rep (Abs x1)) x2" |
332 and "R (Rep (Abs x1)) x2" |
325 proof - |
333 shows "R x1 (Rep (Abs x2))" |
326 show "R x1 (Rep (Abs x2))" |
334 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q]) |
327 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) |
|
328 next |
|
329 show "R (Rep (Abs x1)) x2" |
|
330 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q]) |
|
331 qed |
|
332 |
335 |
333 (* ----------------------------------------------------- *) |
336 (* ----------------------------------------------------- *) |
334 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
337 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
335 (* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) |
338 (* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) |
336 (* ----------------------------------------------------- *) |
339 (* ----------------------------------------------------- *) |
337 |
|
338 (* what is RES_FORALL *) |
|
339 (*--`!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
340 !f. $! f = RES_FORALL (respects R) ((abs --> I) f)`--*) |
|
341 (*as peter here *) |
|
342 |
340 |
343 (* bool theory: COND, LET *) |
341 (* bool theory: COND, LET *) |
344 |
342 |
345 lemma IF_PRS: |
343 lemma IF_PRS: |
346 assumes q: "QUOTIENT R Abs Rep" |
344 assumes q: "QUOTIENT R Abs Rep" |
397 using a by (rule FUN_REL_IMP) |
395 using a by (rule FUN_REL_IMP) |
398 |
396 |
399 |
397 |
400 (* combinators: I, K, o, C, W *) |
398 (* combinators: I, K, o, C, W *) |
401 |
399 |
|
400 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) |
402 lemma I_PRS: |
401 lemma I_PRS: |
403 assumes q: "QUOTIENT R Abs Rep" |
402 assumes q: "QUOTIENT R Abs Rep" |
404 shows "id e = Abs (id (Rep e))" |
403 shows "id e = Abs (id (Rep e))" |
405 using QUOTIENT_ABS_REP[OF q] by auto |
404 using QUOTIENT_ABS_REP[OF q] by auto |
406 |
405 |