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)" |
425 and a1: "(R2 ===> R3) f1 f2" |
426 and a1: "(R2 ===> R3) f1 f2" |
426 and a2: "(R1 ===> R2) g1 g2" |
427 and a2: "(R1 ===> R2) g1 g2" |
427 shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" |
428 shows "(R1 ===> R3) (f1 o g1) (f2 o g2)" |
428 using a1 a2 unfolding o_def expand_fun_eq |
429 using a1 a2 unfolding o_def expand_fun_eq |
429 by (auto) |
430 by (auto) |
|
431 |
|
432 |
|
433 |
|
434 |
|
435 |
|
436 lemma COND_PRS: |
|
437 assumes a: "QUOTIENT R absf repf" |
|
438 shows "(if a then b else c) = absf (if a then repf b else repf c)" |
|
439 using a unfolding QUOTIENT_def by auto |
|
440 |
|
441 |
430 |
442 |
431 |
443 |
432 |
444 |
433 (* Set of lemmas for regularisation of ball and bex *) |
445 (* Set of lemmas for regularisation of ball and bex *) |
434 lemma ball_reg_eqv: |
446 lemma ball_reg_eqv: |
523 |
535 |
524 lemma bex_ex_comm: |
536 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))" |
537 "((\<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 |
538 by auto |
527 |
539 |
528 |
540 (* 2 lemmas needed for proving repabs_inj *) |
529 |
541 lemma ball_rsp: |
530 (* TODO: Add similar *) |
542 assumes a: "(R ===> (op =)) f g" |
531 lemma RES_FORALL_RSP: |
543 shows "Ball (Respects R) f = Ball (Respects R) g" |
532 shows "\<And>f g. (R ===> (op =)) f g ==> |
544 using a by (simp add: Ball_def IN_RESPECTS) |
533 (Ball (Respects R) f = Ball (Respects R) g)" |
545 |
534 apply (simp add: FUN_REL.simps Ball_def IN_RESPECTS) |
546 lemma bex_rsp: |
535 done |
547 assumes a: "(R ===> (op =)) f g" |
536 |
548 shows "(Bex (Respects R) f = Bex (Respects R) g)" |
537 lemma RES_EXISTS_RSP: |
549 using a by (simp add: Bex_def IN_RESPECTS) |
538 shows "\<And>f g. (R ===> (op =)) f g ==> |
550 |
539 (Bex (Respects R) f = Bex (Respects R) g)" |
551 (* 2 lemmas needed for cleaning of quantifiers *) |
540 apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS) |
552 lemma all_prs: |
541 done |
|
542 |
|
543 |
|
544 lemma FORALL_PRS: |
|
545 assumes a: "QUOTIENT R absf repf" |
553 assumes a: "QUOTIENT R absf repf" |
546 shows "All f = Ball (Respects R) ((absf ---> id) f)" |
554 shows "Ball (Respects R) ((absf ---> id) f) = All f" |
547 using a |
555 using a unfolding QUOTIENT_def |
548 unfolding QUOTIENT_def |
|
549 by (metis IN_RESPECTS fun_map.simps id_apply) |
556 by (metis IN_RESPECTS fun_map.simps id_apply) |
550 |
557 |
551 lemma EXISTS_PRS: |
558 lemma ex_prs: |
552 assumes a: "QUOTIENT R absf repf" |
559 assumes a: "QUOTIENT R absf repf" |
553 shows "Ex f = Bex (Respects R) ((absf ---> id) f)" |
560 shows "Bex (Respects R) ((absf ---> id) f) = Ex f" |
554 using a |
561 using a unfolding QUOTIENT_def |
555 unfolding QUOTIENT_def |
562 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 |
563 |
572 end |
564 end |
573 |
565 |