545 Logic.mk_implies |
545 Logic.mk_implies |
546 ((prop_of thm), |
546 ((prop_of thm), |
547 (regularise (prop_of thm) rty rel lthy)) |
547 (regularise (prop_of thm) rty rel lthy)) |
548 *} |
548 *} |
549 |
549 |
|
550 ML {* |
|
551 fun regularize thm rty rel rel_eqv lthy = |
|
552 let |
|
553 val g = build_regularize_goal thm rty rel lthy; |
|
554 fun tac ctxt = |
|
555 (asm_full_simp_tac ((Simplifier.context ctxt HOL_ss) addsimps |
|
556 [(@{thm equiv_res_forall} OF [rel_eqv]), |
|
557 (@{thm equiv_res_exists} OF [rel_eqv])])) THEN_ALL_NEW |
|
558 (((rtac @{thm RIGHT_RES_FORALL_REGULAR}) THEN' (RANGE [fn _ => all_tac, atac]) THEN' |
|
559 (MetisTools.metis_tac ctxt [])) ORELSE' (MetisTools.metis_tac ctxt [])); |
|
560 val cthm = Goal.prove lthy [] [] g (fn x => tac (#context x) 1); |
|
561 in |
|
562 cthm OF [thm] |
|
563 end |
|
564 *} |
|
565 |
550 section {* RepAbs injection *} |
566 section {* RepAbs injection *} |
551 |
567 |
552 (* Needed to have a meta-equality *) |
568 (* Needed to have a meta-equality *) |
553 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id" |
569 lemma id_def_sym: "(\<lambda>x. x) \<equiv> id" |
554 by (simp add: id_def) |
570 by (simp add: id_def) |
614 ML {* |
630 ML {* |
615 fun build_repabs_goal ctxt thm cons rty qty = |
631 fun build_repabs_goal ctxt thm cons rty qty = |
616 Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) |
632 Logic.mk_equals ((Thm.prop_of thm), (build_repabs_term ctxt thm cons rty qty)) |
617 *} |
633 *} |
618 |
634 |
|
635 ML {* |
|
636 fun instantiate_tac thm = Subgoal.FOCUS (fn {concl, ...} => |
|
637 let |
|
638 val pat = Drule.strip_imp_concl (cprop_of thm) |
|
639 val insts = Thm.match (pat, concl) |
|
640 in |
|
641 rtac (Drule.instantiate insts thm) 1 |
619 end |
642 end |
|
643 handle _ => no_tac |
|
644 ) |
|
645 *} |
|
646 |
|
647 ML {* |
|
648 fun res_forall_rsp_tac ctxt = |
|
649 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
650 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
651 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
652 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
653 *} |
|
654 |
|
655 ML {* |
|
656 fun res_exists_rsp_tac ctxt = |
|
657 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
658 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
659 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
660 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
661 *} |
|
662 |
|
663 |
|
664 ML {* |
|
665 fun quotient_tac quot_thm = |
|
666 REPEAT_ALL_NEW (FIRST' [ |
|
667 rtac @{thm FUN_QUOTIENT}, |
|
668 rtac quot_thm, |
|
669 rtac @{thm IDENTITY_QUOTIENT} |
|
670 ]) |
|
671 *} |
|
672 |
|
673 ML {* |
|
674 fun LAMBDA_RES_TAC ctxt i st = |
|
675 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
|
676 (_ $ (_ $ (Abs(_,_,_))$(Abs(_,_,_)))) => |
|
677 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
678 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
679 | _ => fn _ => no_tac) i st |
|
680 *} |
|
681 |
|
682 ML {* |
|
683 fun WEAK_LAMBDA_RES_TAC ctxt i st = |
|
684 (case (term_of o #concl o fst) (Subgoal.focus ctxt i st) of |
|
685 (_ $ (_ $ _$(Abs(_,_,_)))) => |
|
686 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
687 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
688 | (_ $ (_ $ (Abs(_,_,_))$_)) => |
|
689 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
|
690 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
|
691 | _ => fn _ => no_tac) i st |
|
692 *} |
|
693 |
|
694 |
|
695 ML {* |
|
696 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms = |
|
697 (FIRST' [ |
|
698 rtac @{thm FUN_QUOTIENT}, |
|
699 rtac quot_thm, |
|
700 rtac @{thm IDENTITY_QUOTIENT}, |
|
701 rtac @{thm ext}, |
|
702 rtac trans_thm, |
|
703 LAMBDA_RES_TAC ctxt, |
|
704 res_forall_rsp_tac ctxt, |
|
705 res_exists_rsp_tac ctxt, |
|
706 ( |
|
707 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
|
708 THEN_ALL_NEW (fn _ => no_tac) |
|
709 ), |
|
710 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
|
711 rtac refl, |
|
712 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
713 rtac reflex_thm, |
|
714 atac, |
|
715 ( |
|
716 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
|
717 THEN_ALL_NEW (fn _ => no_tac) |
|
718 ), |
|
719 WEAK_LAMBDA_RES_TAC ctxt |
|
720 ]) |
|
721 *} |
|
722 |
|
723 section {* Cleaning the goal *} |
|
724 |
|
725 text {* Does the same as 'subst' in a given theorem *} |
|
726 ML {* |
|
727 fun eqsubst_thm ctxt thms thm = |
|
728 let |
|
729 val goalstate = Goal.init (Thm.cprop_of thm) |
|
730 val a' = case (SINGLE (EqSubst.eqsubst_tac ctxt [0] thms 1) goalstate) of |
|
731 NONE => error "eqsubst_thm" |
|
732 | SOME th => cprem_of th 1 |
|
733 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
|
734 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
|
735 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
|
736 in |
|
737 Simplifier.rewrite_rule [rt] thm |
|
738 end |
|
739 *} |
|
740 |
|
741 end |