519 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
519 fun equiv_solver_tac ss = equiv_tac (Simplifier.the_context ss) |
520 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
520 val equiv_solver = Simplifier.mk_solver' "Equivalence goal solver" equiv_solver_tac |
521 *} |
521 *} |
522 |
522 |
523 ML {* |
523 ML {* |
524 fun ball_reg_eqv_simproc ss redex = |
|
525 let |
|
526 val ctxt = Simplifier.the_context ss |
|
527 val thy = ProofContext.theory_of ctxt |
|
528 in |
|
529 case redex of |
|
530 (ogl as ((Const (@{const_name "Ball"}, _)) $ |
|
531 ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => |
|
532 (let |
|
533 val gl = Const (@{const_name "equivp"}, dummyT) $ R; |
|
534 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
|
535 val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) |
|
536 val thm = (@{thm eq_reflection} OF [@{thm ball_reg_eqv} OF [eqv]]); |
|
537 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) |
|
538 in |
|
539 SOME thm |
|
540 end |
|
541 handle _ => NONE |
|
542 ) |
|
543 | _ => NONE |
|
544 end |
|
545 *} |
|
546 |
|
547 ML {* |
|
548 fun bex_reg_eqv_simproc ss redex = |
|
549 let |
|
550 val ctxt = Simplifier.the_context ss |
|
551 val thy = ProofContext.theory_of ctxt |
|
552 in |
|
553 case redex of |
|
554 (ogl as ((Const (@{const_name "Bex"}, _)) $ |
|
555 ((Const (@{const_name "Respects"}, _)) $ R) $ P1)) => |
|
556 (let |
|
557 val gl = Const (@{const_name "equivp"}, dummyT) $ R; |
|
558 val glc = HOLogic.mk_Trueprop (Syntax.check_term ctxt gl); |
|
559 val eqv = Goal.prove ctxt [] [] glc (fn {context,...} => equiv_tac context 1) |
|
560 val thm = (@{thm eq_reflection} OF [@{thm bex_reg_eqv} OF [eqv]]); |
|
561 (* val _ = tracing (Syntax.string_of_term ctxt (prop_of thm)); *) |
|
562 in |
|
563 SOME thm |
|
564 end |
|
565 handle _ => NONE |
|
566 ) |
|
567 | _ => NONE |
|
568 end |
|
569 *} |
|
570 |
|
571 ML {* |
|
572 fun prep_trm thy (x, (T, t)) = |
524 fun prep_trm thy (x, (T, t)) = |
573 (cterm_of thy (Var (x, T)), cterm_of thy t) |
525 (cterm_of thy (Var (x, T)), cterm_of thy t) |
574 |
526 |
575 fun prep_ty thy (x, (S, ty)) = |
527 fun prep_ty thy (x, (S, ty)) = |
576 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
528 (ctyp_of thy (TVar (x, S)), ctyp_of thy ty) |
656 *} |
608 *} |
657 |
609 |
658 lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
610 lemma eq_imp_rel: "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b" |
659 by (simp add: equivp_reflp) |
611 by (simp add: equivp_reflp) |
660 |
612 |
661 (* does not work yet |
|
662 ML {* |
613 ML {* |
663 fun regularize_tac ctxt = |
614 fun regularize_tac ctxt = |
664 let |
615 let |
665 val pat1 = [@{term "Ball (Respects R) P"}]; |
616 val pat1 = [@{term "Ball (Respects R) P"}]; |
666 val pat2 = [@{term "Bex (Respects R) P"}]; |
617 val pat2 = [@{term "Bex (Respects R) P"}]; |
667 val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
618 val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
668 val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; |
619 val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; |
669 val thy = ProofContext.theory_of ctxt |
620 val thy = ProofContext.theory_of ctxt |
670 val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc)) |
|
671 val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc)) |
|
672 val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc)) |
621 val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc)) |
673 val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc)) |
622 val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc)) |
674 val simp_set = HOL_basic_ss addsimps @{thms ball_reg_eqv bex_reg_eqv} |
623 val simp_set = (mk_minimal_ss ctxt) |
675 addsimprocs [simproc3, simproc4] |
624 addsimps @{thms ball_reg_eqv bex_reg_eqv} |
676 addSolver equiv_solver |
625 addsimprocs [simproc3, simproc4] |
677 * TODO: Make sure that there are no list_rel, pair_rel etc involved * |
626 addSolver equiv_solver |
|
627 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
678 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) |
628 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) |
679 in |
629 in |
680 ObjectLogic.full_atomize_tac THEN' |
630 ObjectLogic.full_atomize_tac THEN' |
681 simp_tac simp_set THEN' |
631 simp_tac simp_set THEN' |
682 REPEAT_ALL_NEW (FIRST' [ |
632 REPEAT_ALL_NEW (FIRST' [ |
687 rtac @{thm bex_ex_comm}, |
637 rtac @{thm bex_ex_comm}, |
688 resolve_tac eq_eqvs, |
638 resolve_tac eq_eqvs, |
689 simp_tac simp_set |
639 simp_tac simp_set |
690 ]) |
640 ]) |
691 end |
641 end |
692 *}*) |
|
693 |
|
694 ML {* |
|
695 fun regularize_tac ctxt = |
|
696 let |
|
697 val pat1 = [@{term "Ball (Respects R) P"}]; |
|
698 val pat2 = [@{term "Bex (Respects R) P"}]; |
|
699 val pat3 = [@{term "Ball (Respects (R1 ===> R2)) P"}]; |
|
700 val pat4 = [@{term "Bex (Respects (R1 ===> R2)) P"}]; |
|
701 val thy = ProofContext.theory_of ctxt |
|
702 val simproc1 = Simplifier.simproc_i thy "" pat1 (K (ball_reg_eqv_simproc)) |
|
703 val simproc2 = Simplifier.simproc_i thy "" pat2 (K (bex_reg_eqv_simproc)) |
|
704 val simproc3 = Simplifier.simproc_i thy "" pat3 (K (ball_reg_eqv_range_simproc)) |
|
705 val simproc4 = Simplifier.simproc_i thy "" pat4 (K (bex_reg_eqv_range_simproc)) |
|
706 val simp_ctxt = (mk_minimal_ss ctxt) addsimprocs [simproc1, simproc2, simproc3, simproc4] |
|
707 (* TODO: Make sure that there are no list_rel, pair_rel etc involved *) |
|
708 val eq_eqvs = map (fn x => @{thm eq_imp_rel} OF [x]) (equiv_rules_get ctxt) |
|
709 in |
|
710 ObjectLogic.full_atomize_tac THEN' |
|
711 simp_tac simp_ctxt THEN' |
|
712 REPEAT_ALL_NEW (FIRST' [ |
|
713 rtac @{thm ball_reg_right}, |
|
714 rtac @{thm bex_reg_left}, |
|
715 resolve_tac (Inductive.get_monos ctxt), |
|
716 rtac @{thm ball_all_comm}, |
|
717 rtac @{thm bex_ex_comm}, |
|
718 resolve_tac eq_eqvs, |
|
719 simp_tac simp_ctxt]) |
|
720 end |
|
721 *} |
642 *} |
722 |
643 |
723 section {* Injections of rep and abses *} |
644 section {* Injections of rep and abses *} |
724 |
645 |
725 (* |
646 (* |