699 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
699 (EqSubst.eqsubst_tac ctxt [0] @{thms FUN_REL.simps}) THEN' |
700 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
700 (rtac @{thm allI}) THEN' (rtac @{thm allI}) THEN' (rtac @{thm impI}) |
701 | _ => fn _ => no_tac) i st |
701 | _ => fn _ => no_tac) i st |
702 *} |
702 *} |
703 |
703 |
704 |
704 ML {* |
705 ML {* |
705 fun APPLY_RSP_TAC rty = Subgoal.FOCUS (fn {concl, ...} => |
706 fun r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms = |
706 let |
|
707 val (_ $ (R $ (f $ _) $ (_ $ _))) = term_of concl; |
|
708 val pat = Drule.strip_imp_concl (cprop_of @{thm APPLY_RSP}); |
|
709 val insts = Thm.match (pat, concl) |
|
710 in |
|
711 if needs_lift rty (type_of f) then |
|
712 rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
|
713 else no_tac |
|
714 end |
|
715 handle _ => no_tac) |
|
716 *} |
|
717 |
|
718 ML {* |
|
719 fun r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms = |
707 (FIRST' [ |
720 (FIRST' [ |
708 rtac @{thm FUN_QUOTIENT}, |
721 rtac @{thm FUN_QUOTIENT}, |
709 rtac quot_thm, |
722 rtac quot_thm, |
710 rtac @{thm IDENTITY_QUOTIENT}, |
723 rtac @{thm IDENTITY_QUOTIENT}, |
711 rtac @{thm ext}, |
|
712 rtac trans_thm, |
724 rtac trans_thm, |
713 LAMBDA_RES_TAC ctxt, |
725 LAMBDA_RES_TAC ctxt, |
714 res_forall_rsp_tac ctxt, |
726 res_forall_rsp_tac ctxt, |
715 res_exists_rsp_tac ctxt, |
727 res_exists_rsp_tac ctxt, |
716 ( |
728 ( |
717 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
729 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps rsp_thms)) |
718 THEN_ALL_NEW (fn _ => no_tac) |
730 THEN_ALL_NEW (fn _ => no_tac) |
719 ), |
731 ), |
720 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
732 (instantiate_tac @{thm REP_ABS_RSP(1)} ctxt THEN' (RANGE [quotient_tac quot_thm])), |
721 rtac refl, |
733 rtac refl, |
722 rtac @{thm arg_cong2[of _ _ _ _ "op ="]}, |
734 (* rtac @{thm arg_cong2[of _ _ _ _ "op ="]},*) |
723 (instantiate_tac @{thm APPLY_RSP} ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
735 (APPLY_RSP_TAC rty ctxt THEN' (RANGE [quotient_tac quot_thm, quotient_tac quot_thm])), |
|
736 Cong_Tac.cong_tac @{thm cong}, |
|
737 rtac @{thm ext}, |
724 rtac reflex_thm, |
738 rtac reflex_thm, |
725 atac, |
739 atac, |
726 ( |
740 ( |
727 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
741 (simp_tac ((Simplifier.context ctxt HOL_ss) addsimps @{thms FUN_REL.simps})) |
728 THEN_ALL_NEW (fn _ => no_tac) |
742 THEN_ALL_NEW (fn _ => no_tac) |
735 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
749 fun repabs_eq lthy thm constructors rty qty quot_thm reflex_thm trans_thm rsp_thms = |
736 let |
750 let |
737 val rt = build_repabs_term lthy thm constructors rty qty; |
751 val rt = build_repabs_term lthy thm constructors rty qty; |
738 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
752 val rg = Logic.mk_equals ((Thm.prop_of thm), rt); |
739 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
753 fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' |
740 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt quot_thm reflex_thm trans_thm rsp_thms)); |
754 (REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thm reflex_thm trans_thm rsp_thms)); |
741 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
755 val cthm = Goal.prove lthy [] [] rg (fn x => tac (#context x) 1); |
742 in |
756 in |
743 (rt, cthm, thm) |
757 (rt, cthm, thm) |
744 end |
758 end |
745 *} |
759 *} |