869 end |
869 end |
870 | _ => no_tac) |
870 | _ => no_tac) |
871 *} |
871 *} |
872 |
872 |
873 ML {* |
873 ML {* |
874 <<<<<<< variant A |
|
875 >>>>>>> variant B |
|
876 val ball_rsp_tac = |
|
877 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
878 case (term_of concl) of |
|
879 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
|
880 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
881 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
882 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
883 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
884 |_ => no_tac) |
|
885 *} |
|
886 |
|
887 ML {* |
|
888 val bex_rsp_tac = |
|
889 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
890 case (term_of concl) of |
|
891 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
|
892 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
893 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
894 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
895 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
896 | _ => no_tac) |
|
897 *} |
|
898 |
|
899 ML {* |
|
900 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
874 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac) |
901 *} |
875 *} |
902 |
876 |
903 ML {* |
877 ML {* |
904 ####### Ancestor |
|
905 val ball_rsp_tac = |
|
906 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
907 case (term_of concl) of |
|
908 (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) $ (Const (@{const_name Ball}, _) $ _))) => |
|
909 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
910 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
911 THEN' instantiate_tac @{thm RES_FORALL_RSP} ctxt THEN' |
|
912 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
913 |_ => no_tac) |
|
914 *} |
|
915 |
|
916 ML {* |
|
917 val bex_rsp_tac = |
|
918 Subgoal.FOCUS (fn {concl, context = ctxt, ...} => |
|
919 case (term_of concl) of |
|
920 (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) $ (Const (@{const_name Bex}, _) $ _))) => |
|
921 ((simp_tac (HOL_ss addsimps @{thms FUN_REL.simps})) |
|
922 THEN' rtac @{thm allI} THEN' rtac @{thm allI} THEN' rtac @{thm impI} |
|
923 THEN' instantiate_tac @{thm RES_EXISTS_RSP} ctxt THEN' |
|
924 (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))) 1 |
|
925 | _ => no_tac) |
|
926 *} |
|
927 |
|
928 ML {* |
|
929 ======= end |
|
930 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
878 fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms = |
931 (FIRST' [resolve_tac trans2, |
879 (FIRST' [resolve_tac trans2, |
932 LAMBDA_RES_TAC ctxt, |
880 LAMBDA_RES_TAC ctxt, |
933 rtac @{thm RES_FORALL_RSP}, |
881 rtac @{thm RES_FORALL_RSP}, |
934 ball_rsp_tac ctxt, |
882 ball_rsp_tac ctxt, |