more work on CASC setup
authorblanchet
Wed Apr 25 22:00:33 2012 +0200 (2012-04-25)
changeset 4776518f37b7aa6a6
parent 47763 15936c7b2fa3
child 47766 9f7cdd5fff7c
more work on CASC setup
src/HOL/TPTP/ATP_Problem_Import.thy
src/HOL/TPTP/atp_problem_import.ML
     1.1 --- a/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 25 20:08:33 2012 +0200
     1.2 +++ b/src/HOL/TPTP/ATP_Problem_Import.thy	Wed Apr 25 22:00:33 2012 +0200
     1.3 @@ -9,7 +9,10 @@
     1.4  uses ("atp_problem_import.ML")
     1.5  begin
     1.6  
     1.7 +ML {* Proofterm.proofs := 0 *}
     1.8 +
     1.9  declare [[show_consts]] (* for Refute *)
    1.10 +declare [[smt_oracle]]
    1.11  
    1.12  use "atp_problem_import.ML"
    1.13  
     2.1 --- a/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 25 20:08:33 2012 +0200
     2.2 +++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Apr 25 22:00:33 2012 +0200
     2.3 @@ -7,10 +7,10 @@
     2.4  
     2.5  signature ATP_PROBLEM_IMPORT =
     2.6  sig
     2.7 -  val isabelle_tptp_file : int -> string -> unit
     2.8    val nitpick_tptp_file : int -> string -> unit
     2.9    val refute_tptp_file : int -> string -> unit
    2.10    val sledgehammer_tptp_file : int -> string -> unit
    2.11 +  val isabelle_tptp_file : int -> string -> unit
    2.12    val translate_tptp_file : string -> string -> string -> unit
    2.13  end;
    2.14  
    2.15 @@ -49,11 +49,6 @@
    2.16       Theory.checkpoint thy)
    2.17    end
    2.18  
    2.19 -(** Isabelle (combination of provers) **)
    2.20 -
    2.21 -fun isabelle_tptp_file timeout file_name = ()
    2.22 -
    2.23 -
    2.24  (** Nitpick (alias Nitrox) **)
    2.25  
    2.26  fun aptrueprop f ((t0 as @{const Trueprop}) $ t1) = t0 $ f t1
    2.27 @@ -121,8 +116,25 @@
    2.28  
    2.29  (** Sledgehammer **)
    2.30  
    2.31 -fun sledgehammer_tptp_file timeout file_name = ()
    2.32 +fun apply_tactic_to_tptp_file tactic timeout file_name =
    2.33 +  let
    2.34 +    val (conjs, (defs, nondefs), thy) = read_tptp_file @{theory} file_name
    2.35 +    val ctxt = Proof_Context.init_global thy
    2.36 +  in
    2.37 +    Goal.prove ctxt [] (defs @ nondefs) (hd conjs) (fn _ => tactic ctxt
    2.38 +  end
    2.39  
    2.40 +val sledgehammer_tptp_file =
    2.41 +  apply_tactic_to_tptp_file Sledgehammer_Tactics.sledgehammer_as_oracle_tac
    2.42 +
    2.43 +
    2.44 +(** Isabelle (combination of provers) **)
    2.45 +
    2.46 +val isabelle_tac =
    2.47 +  ...
    2.48 +
    2.49 +val isabelle_tptp_file =
    2.50 +  ...
    2.51  
    2.52  (** Translator between TPTP(-like) file formats **)
    2.53