825 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
825 (_ $ (_ $ _ $ (Abs _))) => rtac @{thm FUN_REL_I} 1 |
826 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
826 | (_ $ (_ $ (Abs _) $ _)) => rtac @{thm FUN_REL_I} 1 |
827 | _ => no_tac) |
827 | _ => no_tac) |
828 *} |
828 *} |
829 |
829 |
|
830 ML {* |
|
831 val ball_rsp_tac = |
|
832 Subgoal.FOCUS (fn {concl, ...} => |
|
833 case (term_of concl) of |
|
834 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
|
835 rtac @{thm FUN_REL_I} 1 |
|
836 |_ => no_tac) |
|
837 *} |
|
838 |
|
839 ML {* |
|
840 val bex_rsp_tac = |
|
841 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
842 case (term_of concl) of |
|
843 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
|
844 rtac @{thm FUN_REL_I} 1 |
|
845 | _ => no_tac) |
|
846 *} |
|
847 |
830 ML {* (* Legacy *) |
848 ML {* (* Legacy *) |
831 fun needs_lift (rty as Type (rty_s, _)) ty = |
849 fun needs_lift (rty as Type (rty_s, _)) ty = |
832 case ty of |
850 case ty of |
833 Type (s, tys) => |
851 Type (s, tys) => |
834 (s = rty_s) orelse (exists (needs_lift rty) tys) |
852 (s = rty_s) orelse (exists (needs_lift rty) tys) |
848 if needs_lift rty (fastype_of f) |
866 if needs_lift rty (fastype_of f) |
849 then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
867 then rtac (Drule.instantiate insts @{thm APPLY_RSP}) 1 |
850 else no_tac |
868 else no_tac |
851 end |
869 end |
852 | _ => no_tac) |
870 | _ => no_tac) |
853 *} |
|
854 |
|
855 ML {* |
|
856 val ball_rsp_tac = |
|
857 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
858 case (term_of concl) of |
|
859 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
|
860 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
861 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
862 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
863 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
864 |_ => no_tac) |
|
865 *} |
|
866 |
|
867 ML {* |
|
868 val bex_rsp_tac = |
|
869 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
870 case (term_of concl) of |
|
871 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
|
872 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
873 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
874 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
875 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
876 | _ => no_tac) |
|
877 *} |
871 *} |
878 |
872 |
879 ML {* |
873 ML {* |
880 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
874 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
881 *} |
875 *} |
939 DT ctxt "1" (resolve_tac trans2), |
933 DT ctxt "1" (resolve_tac trans2), |
940 |
934 |
941 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
935 (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) |
942 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
936 DT ctxt "2" (LAMBDA_RES_TAC ctxt), |
943 |
937 |
944 (* R (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> R (\<dots>) (\<dots>) *) |
938 (* = (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *) |
945 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
939 DT ctxt "3" (rtac @{thm RES_FORALL_RSP}), |
946 |
940 |
|
941 (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *) |
947 DT ctxt "4" (ball_rsp_tac ctxt), |
942 DT ctxt "4" (ball_rsp_tac ctxt), |
|
943 |
|
944 (* = (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *) |
948 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
945 DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}), |
|
946 |
|
947 (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *) |
949 DT ctxt "6" (bex_rsp_tac ctxt), |
948 DT ctxt "6" (bex_rsp_tac ctxt), |
950 |
949 |
951 (* respectfulness of ops *) |
950 (* respectfulness of ops *) |
952 DT ctxt "7" (resolve_tac rsp_thms), |
951 DT ctxt "7" (resolve_tac rsp_thms), |
953 |
952 |