isabelle: src/HOL/Tools/res_atp_methods.ML@e9d99744e40c (annotated)

17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	1	(* ID: $Id$
17907 c20e4bddcb11 * empty log message * mengj parents: 17905 diff changeset	2	Author: Jia Meng, NICTA
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	3	*)
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	4
24321 e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	5	signature RES_ATP_METHODS =
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	6	sig
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	7	val vampire_tac: Proof.context -> thm list -> int -> tactic
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	8	val eprover_tac: Proof.context -> thm list -> int -> tactic
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	9	val spass_tac: Proof.context -> thm list -> int -> tactic
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	10	val vampireF_tac: Proof.context -> thm list -> int -> tactic
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	11	val vampireH_tac: Proof.context -> thm list -> int -> tactic
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	12	val eproverF_tac: Proof.context -> thm list -> int -> tactic
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	13	val eproverH_tac: Proof.context -> thm list -> int -> tactic
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	14	val spassF_tac: Proof.context -> thm list -> int -> tactic
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	15	val spassH_tac: Proof.context -> thm list -> int -> tactic
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	16	val setup: theory -> theory
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	17	end
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	18
1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	19	structure ResAtpMethods =
24321 e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	20	struct
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	21
19193 45c8db82893d When ATP methods call ATPs, all input clauses from one subgoal are written to one file. mengj parents: 19128 diff changeset	22	(* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
24321 e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	23	fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms i st =
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	24	(EVERY'
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	25	[rtac ccontr,
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	26	ObjectLogic.atomize_prems_tac,
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	27	Meson.skolemize_tac,
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	28	METAHYPS (fn negs =>
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	29	HEADGOAL (Tactic.rtac
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	30	(res_atp_oracle (ProofContext.theory_of ctxt)
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	31	(ResAtp.write_subgoal_file dfg mode ctxt negs user_thms i, timeLimit))))] i st) handle Fail _ => Seq.empty;
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	32
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	33
7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	34	(* vampire, eprover and spass tactics *)
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	35
24215 5458fbf18276 removal of some refs paulson parents: 23590 diff changeset	36	fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.time_limit) st;
5458fbf18276 removal of some refs paulson parents: 23590 diff changeset	37	fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.time_limit) st;
5458fbf18276 removal of some refs paulson parents: 23590 diff changeset	38	fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.time_limit) st;
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	39
18271 0e9a851db989 Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. mengj parents: 18195 diff changeset	40
24215 5458fbf18276 removal of some refs paulson parents: 23590 diff changeset	41	fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.time_limit) st;
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	42
24215 5458fbf18276 removal of some refs paulson parents: 23590 diff changeset	43	fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.time_limit) st;
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	44
24215 5458fbf18276 removal of some refs paulson parents: 23590 diff changeset	45	fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.time_limit) st;
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	46
24215 5458fbf18276 removal of some refs paulson parents: 23590 diff changeset	47	fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.time_limit) st;
18271 0e9a851db989 Added two methods "vampire" and "eprover" that handle both HOL and FOL proofs. mengj parents: 18195 diff changeset	48
24215 5458fbf18276 removal of some refs paulson parents: 23590 diff changeset	49	fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.time_limit) st;
19723 7602f74c914b A new "spass" method. mengj parents: 19193 diff changeset	50
24215 5458fbf18276 removal of some refs paulson parents: 23590 diff changeset	51	fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.time_limit) st;
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	52
24321 e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	53
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	54	fun atp_method tac =
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	55	Method.thms_ctxt_args (fn ths => fn ctxt => Method.SIMPLE_METHOD' (tac ctxt ths));
17905 1574533861b1 Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover"). mengj parents: diff changeset	56
24321 e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	57	val setup =
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	58	Method.add_methods
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	59	[("vampireF", atp_method vampireF_tac, "Vampire for FOL problems"),
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	60	("eproverF", atp_method eproverF_tac, "E prover for FOL problems"),
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	61	("vampireH", atp_method vampireH_tac, "Vampire for HOL problems"),
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	62	("eproverH", atp_method eproverH_tac, "E prover for HOL problems"),
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	63	("eprover", atp_method eprover_tac, "E prover for FOL and HOL problems"),
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	64	("vampire", atp_method vampire_tac, "Vampire for FOL and HOL problems"),
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	65	("spassF", atp_method spassF_tac, "SPASS for FOL problems"),
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	66	("spassH", atp_method spassH_tac, "SPASS for HOL problems"),
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	67	("spass", atp_method spass_tac, "SPASS for FOL and HOL problems")];
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	68
e9d99744e40c proper signature; wenzelm parents: 24300 diff changeset	69	end;

author	wenzelm
	Sat, 18 Aug 2007 13:32:22 +0200
changeset 24321	e9d99744e40c
parent 24300	e170cee91c66
child 28290	4cc2b6046258
permissions	-rw-r--r--