--- a/src/HOL/Tools/res_atp_methods.ML Sat Aug 18 13:32:21 2007 +0200
+++ b/src/HOL/Tools/res_atp_methods.ML Sat Aug 18 13:32:22 2007 +0200
@@ -2,18 +2,34 @@
Author: Jia Meng, NICTA
*)
+signature RES_ATP_METHODS =
+sig
+ val vampire_tac: Proof.context -> thm list -> int -> tactic
+ val eprover_tac: Proof.context -> thm list -> int -> tactic
+ val spass_tac: Proof.context -> thm list -> int -> tactic
+ val vampireF_tac: Proof.context -> thm list -> int -> tactic
+ val vampireH_tac: Proof.context -> thm list -> int -> tactic
+ val eproverF_tac: Proof.context -> thm list -> int -> tactic
+ val eproverH_tac: Proof.context -> thm list -> int -> tactic
+ val spassF_tac: Proof.context -> thm list -> int -> tactic
+ val spassH_tac: Proof.context -> thm list -> int -> tactic
+ val setup: theory -> theory
+end
structure ResAtpMethods =
+struct
-struct
-
(* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
-fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
- (EVERY' [rtac ccontr, ObjectLogic.atomize_prems_tac, Meson.skolemize_tac,
- METAHYPS(fn negs =>
- HEADGOAL(Tactic.rtac
- (res_atp_oracle (ProofContext.theory_of ctxt)
- (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
+fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms i st =
+ (EVERY'
+ [rtac ccontr,
+ ObjectLogic.atomize_prems_tac,
+ Meson.skolemize_tac,
+ METAHYPS (fn negs =>
+ HEADGOAL (Tactic.rtac
+ (res_atp_oracle (ProofContext.theory_of ctxt)
+ (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty;
+
(* vampire, eprover and spass tactics *)
@@ -34,16 +50,20 @@
fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st;
-val ResAtps_setup =
- Method.add_methods
- [("vampireF", ResAtp.atp_method vampireF_tac, "Vampire for FOL problems"),
- ("eproverF", ResAtp.atp_method eproverF_tac, "E prover for FOL problems"),
- ("vampireH", ResAtp.atp_method vampireH_tac, "Vampire for HOL problems"),
- ("eproverH", ResAtp.atp_method eproverH_tac, "E prover for HOL problems"),
- ("eprover", ResAtp.atp_method eprover_tac, "E prover for FOL and HOL problems"),
- ("vampire", ResAtp.atp_method vampire_tac, "Vampire for FOL and HOL problems"),
- ("spassF", ResAtp.atp_method spassF_tac, "SPASS for FOL problems"),
- ("spassH", ResAtp.atp_method spassH_tac, "SPASS for HOL problems"),
- ("spass", ResAtp.atp_method spass_tac, "SPASS for FOL and HOL problems")];
+
+fun atp_method tac =
+ Method.thms_ctxt_args (fn ths => fn ctxt => Method.SIMPLE_METHOD' (tac ctxt ths));
-end
+val setup =
+ Method.add_methods
+ [("vampireF", atp_method vampireF_tac, "Vampire for FOL problems"),
+ ("eproverF", atp_method eproverF_tac, "E prover for FOL problems"),
+ ("vampireH", atp_method vampireH_tac, "Vampire for HOL problems"),
+ ("eproverH", atp_method eproverH_tac, "E prover for HOL problems"),
+ ("eprover", atp_method eprover_tac, "E prover for FOL and HOL problems"),
+ ("vampire", atp_method vampire_tac, "Vampire for FOL and HOL problems"),
+ ("spassF", atp_method spassF_tac, "SPASS for FOL problems"),
+ ("spassH", atp_method spassH_tac, "SPASS for HOL problems"),
+ ("spass", atp_method spass_tac, "SPASS for FOL and HOL problems")];
+
+end;