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 =)" |
221 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
221 shows "(R1 ===> R2) f g = ((Respects (R1 ===> R2) f) \<and> (Respects (R1 ===> R2) g) |
222 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |
222 \<and> ((Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g))" |
223 using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq |
223 using FUN_QUOTIENT[OF q1 q2] unfolding Respects_def QUOTIENT_def expand_fun_eq |
224 by blast |
224 by blast |
225 |
225 |
|
226 (* TODO: it is the same as APPLY_RSP *) |
226 (* q1 and q2 not used; see next lemma *) |
227 (* q1 and q2 not used; see next lemma *) |
227 lemma FUN_REL_MP: |
228 lemma FUN_REL_MP: |
228 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
229 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
229 and q2: "QUOTIENT R2 Abs2 Rep2" |
230 and q2: "QUOTIENT R2 Abs2 Rep2" |
230 shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)" |
231 shows "(R1 ===> R2) f g \<Longrightarrow> R1 x y \<Longrightarrow> R2 (f x) (g y)" |
257 and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" |
258 and a: "(Rep1 ---> Abs2) f = (Rep1 ---> Abs2) g" |
258 shows "R1 x y \<Longrightarrow> R2 (f x) (g y)" |
259 shows "R1 x y \<Longrightarrow> R2 (f x) (g y)" |
259 using q1 q2 r1 r2 a |
260 using q1 q2 r1 r2 a |
260 by (simp add: FUN_REL_EQUALS) |
261 by (simp add: FUN_REL_EQUALS) |
261 |
262 |
|
263 (* We don't use it, it is exactly the same as QUOTIENT_REL_REP but wrong way *) |
262 lemma EQUALS_PRS: |
264 lemma EQUALS_PRS: |
263 assumes q: "QUOTIENT R Abs Rep" |
265 assumes q: "QUOTIENT R Abs Rep" |
264 shows "(x = y) = R (Rep x) (Rep y)" |
266 shows "(x = y) = R (Rep x) (Rep y)" |
265 by (simp add: QUOTIENT_REL_REP[OF q]) |
267 by (rule QUOTIENT_REL_REP[OF q, symmetric]) |
266 |
268 |
267 lemma EQUALS_RSP: |
269 lemma EQUALS_RSP: |
268 assumes q: "QUOTIENT R Abs Rep" |
270 assumes q: "QUOTIENT R Abs Rep" |
269 and a: "R x1 x2" "R y1 y2" |
271 and a: "R x1 x2" "R y1 y2" |
270 shows "R x1 y1 = R x2 y2" |
272 shows "R x1 y1 = R x2 y2" |
283 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
285 assumes q1: "QUOTIENT R1 Abs1 Rep1" |
284 and q2: "QUOTIENT R2 Abs2 Rep2" |
286 and q2: "QUOTIENT R2 Abs2 Rep2" |
285 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)" |
286 unfolding expand_fun_eq |
288 unfolding expand_fun_eq |
287 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
289 using QUOTIENT_ABS_REP[OF q1] QUOTIENT_ABS_REP[OF q2] |
288 by (simp) |
290 by simp |
289 |
291 |
|
292 (* Not used since applic_prs proves a version for an arbitrary number of arguments *) |
290 lemma APP_PRS: |
293 lemma APP_PRS: |
291 assumes q1: "QUOTIENT R1 abs1 rep1" |
294 assumes q1: "QUOTIENT R1 abs1 rep1" |
292 and q2: "QUOTIENT R2 abs2 rep2" |
295 and q2: "QUOTIENT R2 abs2 rep2" |
293 shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" |
296 shows "abs2 ((abs1 ---> rep2) f (rep1 x)) = f x" |
294 unfolding expand_fun_eq |
297 unfolding expand_fun_eq |
318 |
321 |
319 lemma REP_ABS_RSP: |
322 lemma REP_ABS_RSP: |
320 assumes q: "QUOTIENT R Abs Rep" |
323 assumes q: "QUOTIENT R Abs Rep" |
321 and a: "R x1 x2" |
324 and a: "R x1 x2" |
322 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" |
323 and "R (Rep (Abs x1)) x2" |
332 and "R (Rep (Abs x1)) x2" |
324 proof - |
333 shows "R x1 (Rep (Abs x2))" |
325 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]) |
326 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q]) |
|
327 next |
|
328 show "R (Rep (Abs x1)) x2" |
|
329 using q a by (metis QUOTIENT_REL[OF q] QUOTIENT_ABS_REP[OF q] QUOTIENT_REP_REFL[OF q] QUOTIENT_SYM[of q]) |
|
330 qed |
|
331 |
335 |
332 (* ----------------------------------------------------- *) |
336 (* ----------------------------------------------------- *) |
333 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
337 (* Quantifiers: FORALL, EXISTS, EXISTS_UNIQUE, *) |
334 (* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) |
338 (* RES_FORALL, RES_EXISTS, RES_EXISTS_EQUIV *) |
335 (* ----------------------------------------------------- *) |
339 (* ----------------------------------------------------- *) |
336 |
|
337 (* what is RES_FORALL *) |
|
338 (*--`!R (abs:'a -> 'b) rep. QUOTIENT R abs rep ==> |
|
339 !f. $! f = RES_FORALL (respects R) ((abs --> I) f)`--*) |
|
340 (*as peter here *) |
|
341 |
340 |
342 (* bool theory: COND, LET *) |
341 (* bool theory: COND, LET *) |
343 |
342 |
344 lemma IF_PRS: |
343 lemma IF_PRS: |
345 assumes q: "QUOTIENT R Abs Rep" |
344 assumes q: "QUOTIENT R Abs Rep" |
396 using a by (rule FUN_REL_IMP) |
395 using a by (rule FUN_REL_IMP) |
397 |
396 |
398 |
397 |
399 (* combinators: I, K, o, C, W *) |
398 (* combinators: I, K, o, C, W *) |
400 |
399 |
|
400 (* We use id_simps which includes id_apply; so these 2 theorems can be removed *) |
401 lemma I_PRS: |
401 lemma I_PRS: |
402 assumes q: "QUOTIENT R Abs Rep" |
402 assumes q: "QUOTIENT R Abs Rep" |
403 shows "id e = Abs (id (Rep e))" |
403 shows "id e = Abs (id (Rep e))" |
404 using QUOTIENT_ABS_REP[OF q] by auto |
404 using QUOTIENT_ABS_REP[OF q] by auto |
405 |
405 |
425 and a1: "(R2 ===> R3) f1 f2" |
425 and a1: "(R2 ===> R3) f1 f2" |
426 and a2: "(R1 ===> R2) g1 g2" |
426 and a2: "(R1 ===> R2) g1 g2" |
427 shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" |
427 shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" |
428 using a1 a2 unfolding o_def expand_fun_eq |
428 using a1 a2 unfolding o_def expand_fun_eq |
429 by (auto) |
429 by (auto) |
|
430 |
|
431 |
|
432 |
|
433 |
|
434 |
|
435 lemma COND_PRS: |
|
436 assumes a: "QUOTIENT R absf repf" |
|
437 shows "(if a then b else c) = absf (if a then repf b else repf c)" |
|
438 using a unfolding QUOTIENT_def by auto |
|
439 |
|
440 |
430 |
441 |
431 |
442 |
432 |
443 |
433 (* Set of lemmas for regularisation of ball and bex *) |
444 (* Set of lemmas for regularisation of ball and bex *) |
434 lemma ball_reg_eqv: |
445 lemma ball_reg_eqv: |
523 |
534 |
524 lemma bex_ex_comm: |
535 lemma bex_ex_comm: |
525 "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))" |
536 "((\<exists>y. \<exists>x. A x y) \<longrightarrow> (\<exists>y. \<exists>x\<in>P. B x y)) \<Longrightarrow> ((\<exists>x. \<exists>y. A x y) \<longrightarrow> (\<exists>x\<in>P. \<exists>y. B x y))" |
526 by auto |
537 by auto |
527 |
538 |
528 |
539 (* 2 lemmas needed for proving repabs_inj *) |
529 |
540 lemma ball_rsp: |
530 (* TODO: Add similar *) |
541 assumes a: "(R ===> (op =)) f g" |
531 lemma RES_FORALL_RSP: |
542 shows "Ball (Respects R) f = Ball (Respects R) g" |
532 shows "\<And>f g. (R ===> (op =)) f g ==> |
543 using a by (simp add: Ball_def IN_RESPECTS) |
533 (Ball (Respects R) f = Ball (Respects R) g)" |
544 |
534 apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS) |
545 lemma bex_rsp: |
535 done |
546 assumes a: "(R ===> (op =)) f g" |
536 |
547 shows "(Bex (Respects R) f = Bex (Respects R) g)" |
537 lemma RES_EXISTS_RSP: |
548 using a by (simp add: Bex_def IN_RESPECTS) |
538 shows "\<And>f g. (R ===> (op =)) f g ==> |
549 |
539 (Bex (Respects R) f = Bex (Respects R) g)" |
550 (* 2 lemmas needed for cleaning of quantifiers *) |
540 apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS) |
551 lemma all_prs: |
541 done |
|
542 |
|
543 |
|
544 lemma FORALL_PRS: |
|
545 assumes a: "QUOTIENT R absf repf" |
552 assumes a: "QUOTIENT R absf repf" |
546 shows "All f = Ball (Respects R) ((absf ---> id) f)" |
553 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
547 using a |
554 using a unfolding QUOTIENT_def |
548 unfolding QUOTIENT_def |
|
549 by (metis IN_RESPECTS fun_map.simps id_apply) |
555 by (metis IN_RESPECTS fun_map.simps id_apply) |
550 |
556 |
551 lemma EXISTS_PRS: |
557 lemma ex_prs: |
552 assumes a: "QUOTIENT R absf repf" |
558 assumes a: "QUOTIENT R absf repf" |
553 shows "Ex f = Bex (Respects R) ((absf ---> id) f)" |
559 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
554 using a |
560 using a unfolding QUOTIENT_def |
555 unfolding QUOTIENT_def |
561 by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply) |
556 by (metis COMBC_def Collect_def Collect_mem_eq IN_RESPECTS fun_map.simps id_apply mem_def) |
|
557 |
|
558 lemma COND_PRS: |
|
559 assumes a: "QUOTIENT R absf repf" |
|
560 shows "(if a then b else c) = absf (if a then repf b else repf c)" |
|
561 using a unfolding QUOTIENT_def by auto |
|
562 |
|
563 (* These are the fixed versions, general ones need to be proved. *) |
|
564 lemma ho_all_prs: |
|
565 shows "((op = ===> op =) ===> op =) All All" |
|
566 by auto |
|
567 |
|
568 lemma ho_ex_prs: |
|
569 shows "((op = ===> op =) ===> op =) Ex Ex" |
|
570 by auto |
|
571 |
562 |
572 end |
563 end |
573 |
564 |