472 - Ball (Respects ?E) ?P = All ?P |
472 - Ball (Respects ?E) ?P = All ?P |
473 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
473 - (\<And>x. ?R x \<Longrightarrow> ?P x \<longrightarrow> ?Q x) \<Longrightarrow> All ?P \<longrightarrow> Ball ?R ?Q |
474 |
474 |
475 *) |
475 *) |
476 |
476 |
477 lemma my_equiv_res_forall2: |
477 lemma my_equiv_res_forallR: |
478 fixes P::"'a \<Rightarrow> bool" |
478 fixes P::"'a \<Rightarrow> bool" |
479 fixes Q::"'b \<Rightarrow> bool" |
479 fixes Q::"'b \<Rightarrow> bool" |
480 assumes a: "(All Q) \<longrightarrow> (All P)" |
480 assumes b: "(All Q) \<longrightarrow> (All P)" |
481 shows "(All Q) \<longrightarrow> Ball (Respects E) P" |
481 shows "(All Q) \<longrightarrow> Ball (Respects E) P" |
482 using a by auto |
482 using b by auto |
483 |
483 |
484 lemma my_equiv_res_exists: |
484 lemma my_equiv_res_forallL: |
|
485 fixes P::"'a \<Rightarrow> bool" |
|
486 fixes Q::"'b \<Rightarrow> bool" |
|
487 assumes a: "EQUIV E" |
|
488 assumes b: "(All Q) \<longrightarrow> (All P)" |
|
489 shows "Ball (Respects E) P \<longrightarrow> (All P)" |
|
490 using a b |
|
491 unfolding EQUIV_def |
|
492 by (metis IN_RESPECTS) |
|
493 |
|
494 lemma my_equiv_res_existsR: |
485 fixes P::"'a \<Rightarrow> bool" |
495 fixes P::"'a \<Rightarrow> bool" |
486 fixes Q::"'b \<Rightarrow> bool" |
496 fixes Q::"'b \<Rightarrow> bool" |
487 assumes a: "EQUIV E" |
497 assumes a: "EQUIV E" |
488 and b: "(Ex Q) \<longrightarrow> (Ex P)" |
498 and b: "(Ex Q) \<longrightarrow> (Ex P)" |
489 shows "(Ex Q) \<longrightarrow> Bex (Respects E) P" |
499 shows "(Ex Q) \<longrightarrow> Bex (Respects E) P" |
490 apply(subst equiv_res_exists) |
500 using a b |
491 apply(rule a) |
501 unfolding EQUIV_def |
492 apply(rule b) |
502 by (metis IN_RESPECTS) |
493 done |
503 |
|
504 lemma my_equiv_res_existsL: |
|
505 fixes P::"'a \<Rightarrow> bool" |
|
506 fixes Q::"'b \<Rightarrow> bool" |
|
507 assumes b: "(Ex Q) \<longrightarrow> (Ex P)" |
|
508 shows "Bex (Respects E) Q \<longrightarrow> (Ex P)" |
|
509 using b |
|
510 by (auto) |
494 |
511 |
495 lemma universal_twice: |
512 lemma universal_twice: |
496 assumes *: "\<And>x. (P x \<longrightarrow> Q x)" |
513 assumes *: "\<And>x. (P x \<longrightarrow> Q x)" |
497 shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)" |
514 shows "(\<forall>x. P x) \<longrightarrow> (\<forall>x. Q x)" |
498 using * by auto |
515 using * by auto |
499 |
516 |
500 lemma implication_twice: |
517 lemma implication_twice: |
501 assumes a: "c \<longrightarrow> a" |
518 assumes a: "c \<longrightarrow> a" |
502 assumes b: "a \<Longrightarrow> b \<longrightarrow> d" |
519 assumes b: "b \<longrightarrow> d" |
503 shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
520 shows "(a \<longrightarrow> b) \<longrightarrow> (c \<longrightarrow> d)" |
504 using a b by auto |
521 using a b by auto |
505 |
|
506 ML {* |
|
507 (* FIXME: get_rid of rel_refl rel_eqv *) |
|
508 fun REGULARIZE_tac lthy rel_refl rel_eqv = |
|
509 (REPEAT1 o FIRST1) |
|
510 [rtac rel_refl, |
|
511 atac, |
|
512 rtac @{thm universal_twice}, |
|
513 rtac @{thm impI} THEN' atac, |
|
514 rtac @{thm implication_twice}, |
|
515 rtac @{thm my_equiv_res_forall2}, |
|
516 rtac (rel_eqv RS @{thm my_equiv_res_exists}), |
|
517 (* For a = b \<longrightarrow> a \<approx> b *) |
|
518 rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl, |
|
519 rtac @{thm RIGHT_RES_FORALL_REGULAR}] |
|
520 *} |
|
521 |
522 |
522 (* version of REGULARIZE_tac including debugging information *) |
523 (* version of REGULARIZE_tac including debugging information *) |
523 ML {* |
524 ML {* |
524 fun my_print_tac ctxt s thm = |
525 fun my_print_tac ctxt s thm = |
525 let |
526 let |
541 DT lthy "1" (rtac rel_refl), |
542 DT lthy "1" (rtac rel_refl), |
542 DT lthy "2" atac, |
543 DT lthy "2" atac, |
543 DT lthy "3" (rtac @{thm universal_twice}), |
544 DT lthy "3" (rtac @{thm universal_twice}), |
544 DT lthy "4" (rtac @{thm impI} THEN' atac), |
545 DT lthy "4" (rtac @{thm impI} THEN' atac), |
545 DT lthy "5" (rtac @{thm implication_twice}), |
546 DT lthy "5" (rtac @{thm implication_twice}), |
546 DT lthy "6" (rtac @{thm my_equiv_res_forall2}), |
547 DT lthy "6" (rtac @{thm my_equiv_res_forallR}), |
547 DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_exists})), |
548 DT lthy "7" (rtac (rel_eqv RS @{thm my_equiv_res_existsR})), |
548 (* For a = b \<longrightarrow> a \<approx> b *) |
549 (* For a = b \<longrightarrow> a \<approx> b *) |
549 DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
550 DT lthy "8" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
550 DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})] |
551 DT lthy "9" (rtac @{thm RIGHT_RES_FORALL_REGULAR})] |
551 *} |
552 *} |
552 |
553 |
555 (ObjectLogic.full_atomize_tac) THEN' |
556 (ObjectLogic.full_atomize_tac) THEN' |
556 REPEAT_ALL_NEW (FIRST' [ |
557 REPEAT_ALL_NEW (FIRST' [ |
557 rtac rel_refl, |
558 rtac rel_refl, |
558 atac, |
559 atac, |
559 rtac @{thm universal_twice}, |
560 rtac @{thm universal_twice}, |
560 (rtac @{thm impI} THEN' atac), |
561 rtac @{thm impI} THEN' atac, |
561 rtac @{thm implication_twice}, |
562 rtac @{thm implication_twice}, |
562 EqSubst.eqsubst_tac ctxt [0] |
563 EqSubst.eqsubst_tac ctxt [0] |
563 [(@{thm equiv_res_forall} OF [rel_eqv]), |
564 [(@{thm equiv_res_forall} OF [rel_eqv]), |
564 (@{thm equiv_res_exists} OF [rel_eqv])], |
565 (@{thm equiv_res_exists} OF [rel_eqv])], |
565 (* For a = b \<longrightarrow> a \<approx> b *) |
566 (* For a = b \<longrightarrow> a \<approx> b *) |
566 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
567 (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
567 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
568 (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
568 ]); |
569 ]); |
569 *} |
570 *} |
570 |
571 |
|
572 ML {* |
|
573 fun regularize_tac ctxt rel_eqv rel_refl = |
|
574 (ObjectLogic.full_atomize_tac) THEN' |
|
575 REPEAT_ALL_NEW (FIRST' |
|
576 [(K (print_tac "start")) THEN' (K no_tac), |
|
577 DT ctxt "1" (rtac rel_refl), |
|
578 DT ctxt "2" atac, |
|
579 DT ctxt "3" (rtac @{thm universal_twice}), |
|
580 DT ctxt "4" (rtac @{thm impI} THEN' atac), |
|
581 DT ctxt "5" (rtac @{thm implication_twice}), |
|
582 DT ctxt "6" (EqSubst.eqsubst_tac ctxt [0] |
|
583 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
584 (@{thm equiv_res_exists} OF [rel_eqv])]), |
|
585 (* For a = b \<longrightarrow> a \<approx> b *) |
|
586 DT ctxt "7" (rtac @{thm impI} THEN' (asm_full_simp_tac HOL_ss) THEN' rtac rel_refl), |
|
587 DT ctxt "8" (rtac @{thm RIGHT_RES_FORALL_REGULAR}) |
|
588 ]); |
|
589 *} |
|
590 |
|
591 thm RIGHT_RES_FORALL_REGULAR |
|
592 |
|
593 section {* Injections of REP and ABSes *} |
571 |
594 |
572 (* |
595 (* |
573 Injections of REP and Abses |
|
574 *************************** |
|
575 |
|
576 Injecting REPABS means: |
596 Injecting REPABS means: |
577 |
597 |
578 For abstractions: |
598 For abstractions: |
579 * If the type of the abstraction doesn't need lifting we recurse. |
599 * If the type of the abstraction doesn't need lifting we recurse. |
580 * If it does we add RepAbs around the whole term and check if the |
600 * If it does we add RepAbs around the whole term and check if the |