706 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
706 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
707 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
707 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
708 | _ => fn _ => no_tac) i st |
708 | _ => fn _ => no_tac) i st |
709 *} |
709 *} |
710 |
710 |
711 |
711 ML {* |
712 ML {* |
712 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} => |
713 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms = |
713 let |
|
714 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; |
|
715 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
|
716 val insts = Thm.match (pat, concl) |
|
717 in |
|
718 if needs_lift rty (type_of f) then |
|
719 rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
|
720 else no_tac |
|
721 end |
|
722 handle _ => no_tac) |
|
723 *} |
|
724 |
|
725 ML {* |
|
726 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
714 (FIRST' [ |
727 (FIRST' [ |
715 rtac @{thm FUN_QUOTIENT}, |
728 rtac @{thm FUN_QUOTIENT}, |
716 rtac quot_thm, |
729 rtac quot_thm, |
717 rtac @{thm IDENTITY_QUOTIENT}, |
730 rtac @{thm IDENTITY_QUOTIENT}, |
718 rtac @{thm ext}, |
|
719 rtac trans_thm, |
731 rtac trans_thm, |
720 LAMBDA_RES_TAC ctxt, |
732 LAMBDA_RES_TAC ctxt, |
721 res_forall_rsp_tac ctxt, |
733 res_forall_rsp_tac ctxt, |
722 res_exists_rsp_tac ctxt, |
734 res_exists_rsp_tac ctxt, |
723 ( |
735 ( |
724 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
736 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
725 THEN_ALL_NEW (fn _ => no_tac) |
737 THEN_ALL_NEW (fn _ => no_tac) |
726 ), |
738 ), |
727 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
739 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
728 rtac refl, |
740 rtac refl, |
729 rtac @{thm arg_cong2[of _ _ _ _ "op ="]}, |
741 (* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*) |
730 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
742 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
743 Cong_Tac.cong_tac @{thm cong}, |
|
744 rtac @{thm ext}, |
731 rtac reflex_thm, |
745 rtac reflex_thm, |
732 atac, |
746 atac, |
733 ( |
747 ( |
734 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
748 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
735 THEN_ALL_NEW (fn _ => no_tac) |
749 THEN_ALL_NEW (fn _ => no_tac) |
737 WEAK_LAMBDA_RES_TAC ctxt |
751 WEAK_LAMBDA_RES_TAC ctxt |
738 ]) |
752 ]) |
739 *} |
753 *} |
740 |
754 |
741 ML {* |
755 ML {* |
742 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
756 fun repabs lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
743 let |
757 let |
744 val rt = build_repabs_term lthy thm constructors rty qty; |
758 val rt = build_repabs_term lthy thm constructors rty qty; |
745 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
759 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
746 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
760 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
747 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms)); |
761 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); |
748 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
762 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
749 in |
763 in |
750 (rt, cthm, thm) |
764 @{thm Pure.equal_elim_rule1} OF [cthm, thm] |
751 end |
|
752 *} |
|
753 |
|
754 ML {* |
|
755 fun repabs_eq2 lthy (rt, thm, othm) = |
|
756 let |
|
757 fun tac2 ctxt = |
|
758 (simp_tac ((Simplifier.context ctxt empty_ss) addsimps [symmetric thm])) |
|
759 THEN' (rtac othm); |
|
760 val cthm = Goal.prove lthy [] [] rt (fn x => tac2 (#context x) 1); |
|
761 in |
|
762 cthm |
|
763 end |
765 end |
764 *} |
766 *} |
765 |
767 |
766 section {* Cleaning the goal *} |
768 section {* Cleaning the goal *} |
767 |
769 |
775 | SOME th => cprem_of th 1 |
777 | SOME th => cprem_of th 1 |
776 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
778 val tac = (EqSubst.eqsubst_tac ctxt [0] thms 1) THEN simp_tac HOL_ss 1 |
777 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
779 val cgoal = cterm_of (ProofContext.theory_of ctxt) (Logic.mk_equals (term_of (Thm.cprop_of thm), term_of a')) |
778 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
780 val rt = Toplevel.program (fn () => Goal.prove_internal [] cgoal (fn _ => tac)); |
779 in |
781 in |
780 Simplifier.rewrite_rule [rt] thm |
782 @{thm Pure.equal_elim_rule1} OF [rt,thm] |
781 end |
783 end |
|
784 *} |
|
785 |
|
786 ML {* |
|
787 fun repeat_eqsubst_thm ctxt thms thm = |
|
788 repeat_eqsubst_thm ctxt thms (eqsubst_thm ctxt thms thm) |
|
789 handle _ => thm |
782 *} |
790 *} |
783 |
791 |
784 text {* expects atomized definition *} |
792 text {* expects atomized definition *} |
785 ML {* |
793 ML {* |
786 fun add_lower_defs_aux ctxt thm = |
794 fun add_lower_defs_aux ctxt thm = |
787 let |
795 let |
788 val e1 = @{thm fun_cong} OF [thm] |
796 val e1 = @{thm fun_cong} OF [thm]; |
789 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1 |
797 val f = eqsubst_thm ctxt @{thms fun_map.simps} e1; |
|
798 val g = MetaSimplifier.rewrite_rule @{thms id_def_sym} f; |
|
799 val h = repeat_eqsubst_thm ctxt @{thms FUN_MAP_I} g; |
|
800 val i = MetaSimplifier.rewrite_rule [@{thm eq_reflection} OF @{thms id_apply}] h |
790 in |
801 in |
791 thm :: (add_lower_defs_aux ctxt f) |
802 thm :: (add_lower_defs_aux ctxt i) |
792 end |
803 end |
793 handle _ => [thm] |
804 handle _ => [thm] |
794 *} |
805 *} |
795 |
806 |
796 ML {* |
807 ML {* |
853 |
864 |
854 ML {* |
865 ML {* |
855 fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let |
866 fun lift_thm lthy consts rty qty rel rel_eqv rel_refl quot rsp_thms trans2 reps_same t_defs t = let |
856 val t_a = atomize_thm t; |
867 val t_a = atomize_thm t; |
857 val t_r = regularize t_a rty rel rel_eqv lthy; |
868 val t_r = regularize t_a rty rel rel_eqv lthy; |
858 val t_t1 = repabs_eq lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
869 val t_t = repabs lthy t_r consts rty qty quot rel_refl trans2 rsp_thms; |
859 val t_t2 = repabs_eq2 lthy t_t1; |
|
860 val abs = findabs rty (prop_of t_a); |
870 val abs = findabs rty (prop_of t_a); |
861 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
871 val simp_lam_prs_thms = map (make_simp_lam_prs_thm lthy quot) abs; |
862 fun simp_lam_prs lthy thm = |
872 fun simp_lam_prs lthy thm = |
863 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
873 simp_lam_prs lthy (eqsubst_thm lthy simp_lam_prs_thms thm) |
864 handle _ => thm |
874 handle _ => thm |
865 val t_l = simp_lam_prs lthy t_t2; |
875 val t_l = simp_lam_prs lthy t_t; |
866 val t_a = simp_allex_prs lthy quot t_l; |
876 val t_a = simp_allex_prs lthy quot t_l; |
867 val t_defs_sym = add_lower_defs lthy t_defs; |
877 val t_defs_sym = add_lower_defs lthy t_defs; |
868 val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a; |
878 val t_d = MetaSimplifier.rewrite_rule t_defs_sym t_a; |
869 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
879 val t_r = MetaSimplifier.rewrite_rule [reps_same] t_d; |
870 in |
880 in |