727 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
727 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
728 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
728 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
729 | _ => no_tac) |
729 | _ => no_tac) |
730 *} |
730 *} |
731 |
731 |
|
732 ML {* |
|
733 val ball_rsp_tac = |
|
734 Subgoal.FOCUS (fn {concl, ...} => |
|
735 case (term_of concl) of |
|
736 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
|
737 rtac @{thm FUN_REL_I} 1 |
|
738 |_ => no_tac) |
|
739 *} |
|
740 |
|
741 ML {* |
|
742 val bex_rsp_tac = |
|
743 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
744 case (term_of concl) of |
|
745 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
|
746 rtac @{thm FUN_REL_I} 1 |
|
747 | _ => no_tac) |
|
748 *} |
|
749 |
732 ML {* (* Legacy *) |
750 ML {* (* Legacy *) |
733 fun needs_lift (rty as Type (rty_s, _)) ty = |
751 fun needs_lift (rty as Type (rty_s, _)) ty = |
734 case ty of |
752 case ty of |
735 Type (s, tys) => |
753 Type (s, tys) => |
736 (s = rty_s) orelse (exists (needs_lift rty) tys) |
754 (s = rty_s) orelse (exists (needs_lift rty) tys) |
750 if needs_lift rty (fastype_of f) |
768 if needs_lift rty (fastype_of f) |
751 then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
769 then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
752 else no_tac |
770 else no_tac |
753 end |
771 end |
754 | _ => no_tac) |
772 | _ => no_tac) |
755 *} |
|
756 |
|
757 ML {* |
|
758 val ball_rsp_tac = |
|
759 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
760 case (term_of concl) of |
|
761 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
|
762 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
763 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
764 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
765 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
766 |_ => no_tac) |
|
767 *} |
|
768 |
|
769 ML {* |
|
770 val bex_rsp_tac = |
|
771 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
772 case (term_of concl) of |
|
773 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
|
774 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
775 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
776 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
777 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
778 | _ => no_tac) |
|
779 *} |
773 *} |
780 |
774 |
781 ML {* |
775 ML {* |
782 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
776 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
783 (FIRST' [resolve_tac trans2, |
777 (FIRST' [resolve_tac trans2, |
837 DT ctxt "1" (resolve_tac trans2), |
831 DT ctxt "1" (resolve_tac trans2), |
838 |
832 |
839 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
833 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
840 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
834 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
841 |
835 |
842 (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
836 (* = (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *) |
843 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
837 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
844 |
838 |
|
839 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
845 DT ctxt "4" (ball_rsp_tac ctxt), |
840 DT ctxt "4" (ball_rsp_tac ctxt), |
|
841 |
|
842 (* = (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *) |
846 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
843 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
|
844 |
|
845 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
847 DT ctxt "6" (bex_rsp_tac ctxt), |
846 DT ctxt "6" (bex_rsp_tac ctxt), |
848 |
847 |
849 (* respectfulness of ops *) |
848 (* respectfulness of ops *) |
850 DT ctxt "7" (resolve_tac rsp_thms), |
849 DT ctxt "7" (resolve_tac rsp_thms), |
851 |
850 |