src/HOL/Tools/res_atp_methods.ML
author krauss
Fri Nov 24 13:44:51 2006 +0100 (2006-11-24)
changeset 21512 3786eb1b69d6
parent 19723 7602f74c914b
child 23590 ad95084a5c63
permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
     1 (* ID: $Id$
     2    Author: Jia Meng, NICTA
     3 *)
     4 
     5 
     6 structure ResAtpMethods =
     7 
     8 struct
     9   
    10 (* convert the negated 1st subgoal into CNF, write to file and call an ATP oracle *)
    11 fun res_atp_tac dfg res_atp_oracle mode timeLimit ctxt user_thms n thm =
    12     (EVERY' [rtac ccontr,ObjectLogic.atomize_tac, skolemize_tac, 
    13 		  METAHYPS(fn negs =>
    14 			      HEADGOAL(Tactic.rtac 
    15 					   (res_atp_oracle (ProofContext.theory_of ctxt) 
    16 							   (ResAtp.write_subgoal_file dfg mode ctxt negs user_thms n, timeLimit))))] n thm) handle (Fail _) => Seq.empty;
    17 
    18 (* vampire, eprover and spass tactics *)
    19 
    20 fun vampire_tac st = res_atp_tac false vampire_oracle ResAtp.Auto (!ResAtp.vampire_time) st;
    21 fun eprover_tac st = res_atp_tac false eprover_oracle ResAtp.Auto (!ResAtp.eprover_time) st;
    22 fun spass_tac st = res_atp_tac true spass_oracle ResAtp.Auto (!ResAtp.spass_time) st;
    23 
    24 
    25 fun vampireF_tac st = res_atp_tac false vampire_oracle ResAtp.Fol (!ResAtp.vampire_time) st;
    26 
    27 fun vampireH_tac st = res_atp_tac false vampire_oracle ResAtp.Hol (!ResAtp.vampire_time) st;
    28 
    29 fun eproverF_tac st = res_atp_tac false eprover_oracle ResAtp.Fol (!ResAtp.eprover_time) st;
    30 
    31 fun eproverH_tac st = res_atp_tac false eprover_oracle ResAtp.Hol (!ResAtp.eprover_time) st;
    32 
    33 fun spassF_tac st = res_atp_tac true spass_oracle ResAtp.Fol (!ResAtp.spass_time) st;
    34 
    35 fun spassH_tac st = res_atp_tac true spass_oracle ResAtp.Hol (!ResAtp.spass_time) st;
    36 
    37 val ResAtps_setup =
    38   Method.add_methods 
    39     [("vampireF", ResAtp.atp_method vampireF_tac, "Vampire for FOL problems"),
    40      ("eproverF", ResAtp.atp_method eproverF_tac, "E prover for FOL problems"),
    41      ("vampireH", ResAtp.atp_method vampireH_tac, "Vampire for HOL problems"),
    42      ("eproverH", ResAtp.atp_method eproverH_tac, "E prover for HOL problems"),
    43      ("eprover", ResAtp.atp_method eprover_tac, "E prover for FOL and HOL problems"),
    44      ("vampire", ResAtp.atp_method vampire_tac, "Vampire for FOL and HOL problems"),
    45      ("spassF", ResAtp.atp_method spassF_tac, "SPASS for FOL problems"),
    46      ("spassH", ResAtp.atp_method spassH_tac, "SPASS for HOL problems"),
    47      ("spass", ResAtp.atp_method spass_tac, "SPASS for FOL and HOL problems")];
    48 
    49 end