merged
authorblanchet
Thu, 25 Mar 2010 17:56:31 +0100 (2010-03-25)
changeset 35972 142c3784a42b
parent 35959 b88e061754a1 (current diff)
parent 35971 4f24a4e9af4a (diff)
child 35973 71620f11dbbb
merged
src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/IsaMakefile	Thu Mar 25 17:56:31 2010 +0100
@@ -322,6 +322,7 @@
   Tools/Sledgehammer/sledgehammer_hol_clause.ML \
   Tools/Sledgehammer/sledgehammer_isar.ML \
   Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
+  Tools/Sledgehammer/sledgehammer_util.ML \
   Tools/string_code.ML \
   Tools/string_syntax.ML \
   Tools/transfer.ML \
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -280,7 +280,8 @@
 
 fun get_atp thy args =
   let
-    fun default_atp_name () = hd (ATP_Manager.get_atps ())
+    fun default_atp_name () =
+      hd (#atps (Sledgehammer_Isar.default_params thy []))
       handle Empty => error "No ATP available."
     fun get_prover name =
       (case ATP_Manager.get_prover thy name of
@@ -302,22 +303,28 @@
 fun run_sh prover hard_timeout timeout dir st =
   let
     val {context = ctxt, facts, goal} = Proof.goal st
+    val thy = ProofContext.theory_of ctxt
     val change_dir = (fn SOME d => Config.put ATP_Wrapper.destdir d | _ => I)
     val ctxt' =
       ctxt
       |> change_dir dir
       |> Config.put ATP_Wrapper.measure_runtime true
-    val problem = ATP_Manager.problem_of_goal (! ATP_Manager.full_types) 1 (ctxt', (facts, goal));
-
+    val params = Sledgehammer_Isar.default_params thy []
+    val problem =
+      {subgoal = 1, goal = (ctxt', (facts, goal)),
+       relevance_override = {add = [], del = [], only = false},
+       axiom_clauses = NONE, filtered_clauses = NONE}
     val time_limit =
       (case hard_timeout of
         NONE => I
       | SOME secs => TimeLimit.timeLimit (Time.fromSeconds secs))
-    val ({success, message, theorem_names, runtime=time_atp, ...}: ATP_Manager.prover_result,
-        time_isa) = time_limit (Mirabelle.cpu_time (fn t => prover t problem)) timeout
+    val ({success, message, relevant_thm_names,
+          atp_run_time_in_msecs = time_atp, ...}: ATP_Manager.prover_result,
+        time_isa) = time_limit (Mirabelle.cpu_time
+                      (prover params (Time.fromSeconds timeout))) problem
   in
-    if success then (message, SH_OK (time_isa, time_atp, theorem_names))
-    else (message, SH_FAIL(time_isa, time_atp))
+    if success then (message, SH_OK (time_isa, time_atp, relevant_thm_names))
+    else (message, SH_FAIL (time_isa, time_atp))
   end
   handle Sledgehammer_HOL_Clause.TRIVIAL => ("trivial", SH_OK (0, 0, []))
        | ERROR msg => ("error: " ^ msg, SH_ERROR)
@@ -375,16 +382,19 @@
 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
     open ATP_Minimal
+    open Sledgehammer_Isar
+    val thy = Proof.theory_of st
     val n0 = length (these (!named_thms))
-    val (prover_name, prover) = get_atp (Proof.theory_of st) args
-    val minimize = minimize_theorems linear_minimize prover prover_name
+    val (prover_name, prover) = get_atp thy args
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o explode)
       |> the_default 5
+    val params = default_params thy [("minimize_timeout", Int.toString timeout)]
+    val minimize = minimize_theorems params linear_minimize prover prover_name
     val _ = log separator
   in
-    case minimize timeout st (these (!named_thms)) of
+    case minimize st (these (!named_thms)) of
       (SOME named_thms', msg) =>
         (change_data id inc_min_succs;
          change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
--- a/src/HOL/Sledgehammer.thy	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Sledgehammer.thy	Thu Mar 25 17:56:31 2010 +0100
@@ -12,6 +12,7 @@
 uses
   "Tools/polyhash.ML"
   "~~/src/Tools/Metis/metis.ML"
+  "Tools/Sledgehammer/sledgehammer_util.ML"
   ("Tools/Sledgehammer/sledgehammer_fol_clause.ML")
   ("Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML")
   ("Tools/Sledgehammer/sledgehammer_hol_clause.ML")
--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -1,71 +1,92 @@
 (*  Title:      HOL/Tools/ATP_Manager/atp_manager.ML
     Author:     Fabian Immler, TU Muenchen
     Author:     Makarius
+    Author:     Jasmin Blanchette, TU Muenchen
 
 Central manager component for ATP threads.
 *)
 
 signature ATP_MANAGER =
 sig
+  type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+  type params =
+    {debug: bool,
+     verbose: bool,
+     atps: string list,
+     full_types: bool,
+     relevance_threshold: real,
+     higher_order: bool option,
+     respect_no_atp: bool,
+     follow_defs: bool,
+     isar_proof: bool,
+     timeout: Time.time,
+     minimize_timeout: Time.time}
   type problem =
-   {with_full_types: bool,
-    subgoal: int,
-    goal: Proof.context * (thm list * thm),
-    axiom_clauses: (thm * (string * int)) list option,
-    filtered_clauses: (thm * (string * int)) list option}
-  val problem_of_goal: bool -> int -> Proof.context * (thm list * thm) -> problem
+    {subgoal: int,
+     goal: Proof.context * (thm list * thm),
+     relevance_override: relevance_override,
+     axiom_clauses: (thm * (string * int)) list option,
+     filtered_clauses: (thm * (string * int)) list option}
   type prover_result =
-   {success: bool,
-    message: string,
-    theorem_names: string list,
-    runtime: int,
-    proof: string,
-    internal_thm_names: string Vector.vector,
-    filtered_clauses: (thm * (string * int)) list}
-  type prover = int -> problem -> prover_result
+    {success: bool,
+     message: string,
+     relevant_thm_names: string list,
+     atp_run_time_in_msecs: int,
+     proof: string,
+     internal_thm_names: string Vector.vector,
+     filtered_clauses: (thm * (string * int)) list}
+  type prover = params -> Time.time -> problem -> prover_result
 
   val atps: string Unsynchronized.ref
-  val get_atps: unit -> string list
   val timeout: int Unsynchronized.ref
   val full_types: bool Unsynchronized.ref
-  val kill: unit -> unit
-  val info: unit -> unit
+  val kill_atps: unit -> unit
+  val running_atps: unit -> unit
   val messages: int option -> unit
   val add_prover: string * prover -> theory -> theory
   val get_prover: theory -> string -> prover option
-  val print_provers: theory -> unit
-  val sledgehammer: string list -> Proof.state -> unit
+  val available_atps: theory -> unit
+  val sledgehammer: params -> int -> relevance_override -> Proof.state -> unit
 end;
 
 structure ATP_Manager : ATP_MANAGER =
 struct
 
-(** problems, results, and provers **)
+type relevance_override = Sledgehammer_Fact_Filter.relevance_override
+
+(** parameters, problems, results, and provers **)
+
+(* TODO: "theory_const", "blacklist_filter", "convergence" *)
+type params =
+  {debug: bool,
+   verbose: bool,
+   atps: string list,
+   full_types: bool,
+   relevance_threshold: real,
+   higher_order: bool option,
+   respect_no_atp: bool,
+   follow_defs: bool,
+   isar_proof: bool,
+   timeout: Time.time,
+   minimize_timeout: Time.time}
 
 type problem =
- {with_full_types: bool,
-  subgoal: int,
-  goal: Proof.context * (thm list * thm),
-  axiom_clauses: (thm * (string * int)) list option,
-  filtered_clauses: (thm * (string * int)) list option};
-
-fun problem_of_goal with_full_types subgoal goal : problem =
- {with_full_types = with_full_types,
-  subgoal = subgoal,
-  goal = goal,
-  axiom_clauses = NONE,
-  filtered_clauses = NONE};
+  {subgoal: int,
+   goal: Proof.context * (thm list * thm),
+   relevance_override: relevance_override,
+   axiom_clauses: (thm * (string * int)) list option,
+   filtered_clauses: (thm * (string * int)) list option};
 
 type prover_result =
- {success: bool,
-  message: string,
-  theorem_names: string list,  (*relevant theorems*)
-  runtime: int,  (*user time of the ATP, in milliseconds*)
-  proof: string,
-  internal_thm_names: string Vector.vector,
-  filtered_clauses: (thm * (string * int)) list};
+  {success: bool,
+   message: string,
+   relevant_thm_names: string list,
+   atp_run_time_in_msecs: int,
+   proof: string,
+   internal_thm_names: string Vector.vector,
+   filtered_clauses: (thm * (string * int)) list};
 
-type prover = int -> problem -> prover_result;
+type prover = params -> Time.time -> problem -> prover_result;
 
 
 (** preferences **)
@@ -74,8 +95,6 @@
 val message_display_limit = 5;
 
 val atps = Unsynchronized.ref "e spass remote_vampire";
-fun get_atps () = String.tokens (Symbol.is_ascii_blank o String.str) (! atps);
-
 val timeout = Unsynchronized.ref 60;
 val full_types = Unsynchronized.ref false;
 
@@ -218,9 +237,9 @@
 
 (** user commands **)
 
-(* kill *)
+(* kill ATPs *)
 
-fun kill () = Synchronized.change global_state
+fun kill_atps () = Synchronized.change global_state
   (fn {manager, timeout_heap, active, cancelling, messages, store} =>
     let
       val killing = map (fn (th, (_, _, desc)) => (th, (Time.now (), desc))) active;
@@ -228,11 +247,11 @@
     in state' end);
 
 
-(* info *)
+(* running_atps *)
 
 fun seconds time = string_of_int (Time.toSeconds time) ^ "s";
 
-fun info () =
+fun running_atps () =
   let
     val {active, cancelling, ...} = Synchronized.value global_state;
 
@@ -287,44 +306,51 @@
 fun get_prover thy name =
   Option.map #1 (Symtab.lookup (Provers.get thy) name);
 
-fun print_provers thy = Pretty.writeln
-  (Pretty.strs ("external provers:" :: sort_strings (Symtab.keys (Provers.get thy))));
+fun available_atps thy = Pretty.writeln
+  (Pretty.strs ("ATPs:" :: sort_strings (Symtab.keys (Provers.get thy))));
 
 
 (* start prover thread *)
 
-fun start_prover name birth_time death_time i proof_state =
+fun start_prover (params as {timeout, ...}) birth_time death_time i
+                 relevance_override proof_state name =
   (case get_prover (Proof.theory_of proof_state) name of
-    NONE => warning ("Unknown external prover: " ^ quote name)
+    NONE => warning ("Unknown ATP: " ^ quote name)
   | SOME prover =>
       let
         val {context = ctxt, facts, goal} = Proof.goal proof_state;
         val desc =
-          "external prover " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
+          "ATP " ^ quote name ^ " for subgoal " ^ string_of_int i ^ ":\n" ^
             Syntax.string_of_term ctxt (Thm.term_of (Thm.cprem_of goal i));
 
         val _ = Toplevel.thread true (fn () =>
           let
             val _ = register birth_time death_time (Thread.self (), desc);
-            val problem = problem_of_goal (! full_types) i (ctxt, (facts, goal));
-            val message = #message (prover (! timeout) problem)
+            val problem =
+              {subgoal = i, goal = (ctxt, (facts, goal)),
+               relevance_override = relevance_override, axiom_clauses = NONE,
+               filtered_clauses = NONE}
+            val message = #message (prover params timeout problem)
               handle Sledgehammer_HOL_Clause.TRIVIAL =>   (* FIXME !? *)
-                  "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis"
+                  "Try this command: " ^
+                  Markup.markup Markup.sendback "by metis" ^ "."
                 | ERROR msg => ("Error: " ^ msg);
             val _ = unregister message (Thread.self ());
           in () end);
       in () end);
 
 
-(* sledghammer for first subgoal *)
+(* Sledgehammer the given subgoal *)
 
-fun sledgehammer names proof_state =
+fun sledgehammer (params as {atps, timeout, ...}) i relevance_override
+                 proof_state =
   let
-    val provers = if null names then get_atps () else names;
-    val birth_time = Time.now ();
-    val death_time = Time.+ (birth_time, Time.fromSeconds (! timeout));
-    val _ = kill ();   (*RACE wrt. other invocations of sledgehammer*)
-    val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
-  in () end;
+    val birth_time = Time.now ()
+    val death_time = Time.+ (birth_time, timeout)
+    val _ = kill_atps () (* RACE w.r.t. other invocations of Sledgehammer *)
+    val _ = priority "Sledgehammering..."
+    val _ = List.app (start_prover params birth_time death_time i
+                                   relevance_override proof_state) atps
+  in () end
 
 end;
--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -6,6 +6,7 @@
 
 signature ATP_MINIMAL =
 sig
+  type params = ATP_Manager.params
   type prover = ATP_Manager.prover
   type prover_result = ATP_Manager.prover_result
   type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
@@ -13,7 +14,7 @@
   val linear_minimize : 'a minimize_fun
   val binary_minimize : 'a minimize_fun
   val minimize_theorems :
-    (string * thm list) minimize_fun -> prover -> string -> int
+    params -> (string * thm list) minimize_fun -> prover -> string
     -> Proof.state -> (string * thm list) list
     -> (string * thm list) list option * string
 end;
@@ -109,8 +110,8 @@
 
 (* wrapper for calling external prover *)
 
-fun sledgehammer_test_theorems prover time_limit subgoalno state filtered
-                               name_thms_pairs =
+fun sledgehammer_test_theorems (params as {full_types, ...} : params) prover
+        timeout subgoalno state filtered name_thms_pairs =
   let
     val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^
                       " theorems... ")
@@ -118,26 +119,26 @@
     val axclauses = cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
     val {context = ctxt, facts, goal} = Proof.goal state
     val problem =
-     {with_full_types = ! ATP_Manager.full_types,
-      subgoal = subgoalno,
-      goal = (ctxt, (facts, goal)),
-      axiom_clauses = SOME axclauses,
-      filtered_clauses = filtered}
-    val (result, proof) = produce_answer (prover time_limit problem)
+     {subgoal = subgoalno, goal = (ctxt, (facts, goal)),
+      relevance_override = {add = [], del = [], only = false},
+      axiom_clauses = SOME axclauses, filtered_clauses = filtered}
+    val (result, proof) = produce_answer (prover params timeout problem)
     val _ = priority (string_of_result result)
   in (result, proof) end
 
 
 (* minimalization of thms *)
 
-fun minimize_theorems gen_min prover prover_name time_limit state
-                      name_thms_pairs =
+fun minimize_theorems (params as {minimize_timeout, ...}) gen_min prover
+                      prover_name state name_thms_pairs =
   let
+    val msecs = Time.toMilliseconds minimize_timeout
     val _ =
       priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
-        " theorems, prover: " ^ prover_name ^
-        ", time limit: " ^ string_of_int time_limit ^ " seconds")
-    val test_thms_fun = sledgehammer_test_theorems prover time_limit 1 state
+        " theorems, ATP: " ^ prover_name ^
+        ", time limit: " ^ string_of_int msecs ^ " ms")
+    val test_thms_fun =
+      sledgehammer_test_theorems params prover minimize_timeout 1 state
     fun test_thms filtered thms =
       case test_thms_fun filtered thms of (Success _, _) => true | _ => false
   in
@@ -157,18 +158,22 @@
           val _ = priority (cat_lines
             ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
         in
-          (SOME min_thms, "Try this command: " ^
-            Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
+          (SOME min_thms,
+           "Try this command: " ^
+           Markup.markup Markup.sendback
+                         ("by (metis " ^ space_implode " " min_names ^ ")")
+           ^ ".")
         end
     | (Timeout, _) =>
         (NONE, "Timeout: You may need to increase the time limit of " ^
-          string_of_int time_limit ^ " seconds. Call atp_minimize [time=...] ")
+          string_of_int msecs ^ " ms. Invoke \"atp_minimize [time=...]\".")
     | (Error, msg) =>
         (NONE, "Error in prover: " ^ msg)
     | (Failure, _) =>
         (NONE, "Failure: No proof with the theorems supplied"))
     handle Sledgehammer_HOL_Clause.TRIVIAL =>
-        (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+        (SOME [], "Trivial: Try this command: " ^
+                  Markup.markup Markup.sendback "by metis" ^ ".")
       | ERROR msg => (NONE, "Error: " ^ msg)
   end
 
--- a/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_wrapper.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -20,6 +20,7 @@
 structure ATP_Wrapper : ATP_WRAPPER =
 struct
 
+open Sledgehammer_Fact_Preprocessor
 open Sledgehammer_HOL_Clause
 open Sledgehammer_Fact_Filter
 open Sledgehammer_Proof_Reconstruct
@@ -43,11 +44,11 @@
 
 type prover_config =
  {command: Path.T,
-  arguments: int -> string,
+  arguments: Time.time -> string,
   failure_strs: string list,
   max_new_clauses: int,
-  insert_theory_const: bool,
-  emit_structured_proof: bool};
+  add_theory_const: bool,
+  supports_isar_proofs: bool};
 
 
 (* basic template *)
@@ -64,24 +65,25 @@
           else SOME "Ill-formed ATP output"
   | (failure :: _) => SOME failure
 
-fun external_prover relevance_filter prepare write cmd args failure_strs
-        produce_answer name ({with_full_types, subgoal, goal, axiom_clauses,
-                              filtered_clauses}: problem) =
+fun generic_prover get_facts prepare write cmd args failure_strs produce_answer
+        name ({full_types, ...} : params)
+        ({subgoal, goal, relevance_override, axiom_clauses, filtered_clauses}
+         : problem) =
   let
     (* get clauses and prepare them for writing *)
     val (ctxt, (chain_ths, th)) = goal;
     val thy = ProofContext.theory_of ctxt;
     val chain_ths = map (Thm.put_name_hint chained_hint) chain_ths;
-    val goal_cls = #1 (Sledgehammer_Fact_Preprocessor.neg_conjecture_clauses ctxt th subgoal);
+    val goal_cls = #1 (neg_conjecture_clauses ctxt th subgoal);
     val the_filtered_clauses =
       (case filtered_clauses of
-        NONE => relevance_filter goal goal_cls
+        NONE => get_facts relevance_override goal goal_cls
       | SOME fcls => fcls);
     val the_axiom_clauses =
       (case axiom_clauses of
         NONE => the_filtered_clauses
       | SOME axcls => axcls);
-    val (thm_names, clauses) =
+    val (internal_thm_names, clauses) =
       prepare goal_cls chain_ths the_axiom_clauses the_filtered_clauses thy;
 
     (* path to unique problem file *)
@@ -121,7 +123,7 @@
       if Config.get ctxt measure_runtime then split_time s else (s, 0)
     fun run_on probfile =
       if File.exists cmd then
-        write with_full_types probfile clauses
+        write full_types probfile clauses
         |> pair (apfst split_time' (bash_output (cmd_line probfile)))
       else error ("Bad executable: " ^ Path.implode cmd);
 
@@ -131,21 +133,24 @@
       if destdir' = "" then ()
       else File.write (Path.explode (Path.implode probfile ^ "_proof")) proof;
 
-    val (((proof, time), rc), conj_pos) =
+    val (((proof, atp_run_time_in_msecs), rc), conj_pos) =
       with_path cleanup export run_on (prob_pathname subgoal);
 
     (* check for success and print out some information on failure *)
     val failure = find_failure failure_strs proof;
     val success = rc = 0 andalso is_none failure;
-    val (message, real_thm_names) =
+    val (message, relevant_thm_names) =
       if is_some failure then ("External prover failed.", [])
       else if rc <> 0 then ("External prover failed: " ^ proof, [])
-      else apfst (fn s => "Try this command: " ^ s)
-        (produce_answer name (proof, thm_names, conj_pos, ctxt, th, subgoal));
+      else
+        (produce_answer name (proof, internal_thm_names, conj_pos, ctxt, th,
+                              subgoal));
   in
     {success = success, message = message,
-      theorem_names = real_thm_names, runtime = time, proof = proof,
-      internal_thm_names = thm_names, filtered_clauses = the_filtered_clauses}
+     relevant_thm_names = relevant_thm_names,
+     atp_run_time_in_msecs = atp_run_time_in_msecs, proof = proof,
+     internal_thm_names = internal_thm_names,
+     filtered_clauses = the_filtered_clauses}
   end;
 
 
@@ -153,96 +158,87 @@
 
 fun generic_tptp_prover
         (name, {command, arguments, failure_strs, max_new_clauses,
-                insert_theory_const, emit_structured_proof}) timeout =
-  external_prover (get_relevant_facts max_new_clauses insert_theory_const)
-      (prepare_clauses false) write_tptp_file command (arguments timeout)
-      failure_strs
-      (if emit_structured_proof then structured_isar_proof
-       else metis_lemma_list false) name;
+                add_theory_const, supports_isar_proofs})
+        (params as {relevance_threshold, higher_order, follow_defs, isar_proof,
+                    ...}) timeout =
+  generic_prover
+      (get_relevant_facts relevance_threshold higher_order follow_defs
+                          max_new_clauses add_theory_const)
+      (prepare_clauses higher_order false) write_tptp_file command
+      (arguments timeout) failure_strs
+      (if supports_isar_proofs andalso isar_proof then structured_isar_proof
+       else metis_lemma_list false) name params;
 
-fun tptp_prover (name, p) = (name, generic_tptp_prover (name, p));
+fun tptp_prover name p = (name, generic_tptp_prover (name, p));
 
 
 (** common provers **)
 
 (* Vampire *)
 
-(*NB: Vampire does not work without explicit timelimit*)
-
-val vampire_failure_strs =
-  ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"];
-val vampire_max_new_clauses = 60;
-val vampire_insert_theory_const = false;
+(* NB: Vampire does not work without explicit time limit. *)
 
-fun vampire_prover_config isar : prover_config =
- {command = Path.explode "$VAMPIRE_HOME/vampire",
-  arguments = (fn timeout => "--output_syntax tptp --mode casc" ^
-    " -t " ^ string_of_int timeout),
-  failure_strs = vampire_failure_strs,
-  max_new_clauses = vampire_max_new_clauses,
-  insert_theory_const = vampire_insert_theory_const,
-  emit_structured_proof = isar};
-
-val vampire = tptp_prover ("vampire", vampire_prover_config false);
-val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true);
+val vampire_config : prover_config =
+  {command = Path.explode "$VAMPIRE_HOME/vampire",
+   arguments = (fn timeout => "--output_syntax tptp --mode casc -t " ^
+                              string_of_int (Time.toSeconds timeout)),
+   failure_strs =
+     ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"],
+   max_new_clauses = 60,
+   add_theory_const = false,
+   supports_isar_proofs = true}
+val vampire = tptp_prover "vampire" vampire_config
 
 
 (* E prover *)
 
-val eprover_failure_strs =
-  ["SZS status: Satisfiable", "SZS status Satisfiable",
-   "SZS status: ResourceOut", "SZS status ResourceOut",
-   "# Cannot determine problem status"];
-val eprover_max_new_clauses = 100;
-val eprover_insert_theory_const = false;
-
-fun eprover_config isar : prover_config =
- {command = Path.explode "$E_HOME/eproof",
-  arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^
-    " --silent --cpu-limit=" ^ string_of_int timeout),
-  failure_strs = eprover_failure_strs,
-  max_new_clauses = eprover_max_new_clauses,
-  insert_theory_const = eprover_insert_theory_const,
-  emit_structured_proof = isar};
-
-val eprover = tptp_prover ("e", eprover_config false);
-val eprover_isar = tptp_prover ("e_isar", eprover_config true);
+val e_config : prover_config =
+  {command = Path.explode "$E_HOME/eproof",
+   arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev \
+                              \-tAutoDev --silent --cpu-limit=" ^
+                              string_of_int (Time.toSeconds timeout)),
+   failure_strs =
+       ["SZS status: Satisfiable", "SZS status Satisfiable",
+        "SZS status: ResourceOut", "SZS status ResourceOut",
+        "# Cannot determine problem status"],
+   max_new_clauses = 100,
+   add_theory_const = false,
+   supports_isar_proofs = true}
+val e = tptp_prover "e" e_config
 
 
 (* SPASS *)
 
-val spass_failure_strs =
-  ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
-   "SPASS beiseite: Maximal number of loops exceeded."];
-val spass_max_new_clauses = 40;
-val spass_insert_theory_const = true;
-
-fun spass_config insert_theory_const: prover_config =
- {command = Path.explode "$SPASS_HOME/SPASS",
-  arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
-    " -FullRed=0 -DocProof -TimeLimit=" ^ string_of_int timeout),
-  failure_strs = spass_failure_strs,
-  max_new_clauses = spass_max_new_clauses,
-  insert_theory_const = insert_theory_const,
-  emit_structured_proof = false};
-
 fun generic_dfg_prover
         (name, ({command, arguments, failure_strs, max_new_clauses,
-                 insert_theory_const, ...} : prover_config)) timeout =
-  external_prover
-    (get_relevant_facts max_new_clauses insert_theory_const)
-    (prepare_clauses true)
-    write_dfg_file
-    command
-    (arguments timeout)
-    failure_strs
-    (metis_lemma_list true)
-    name;
+                 add_theory_const, ...} : prover_config))
+        (params as {relevance_threshold, higher_order, follow_defs, ...})
+        timeout =
+  generic_prover
+      (get_relevant_facts relevance_threshold higher_order follow_defs
+                          max_new_clauses add_theory_const)
+      (prepare_clauses higher_order true) write_dfg_file command
+      (arguments timeout) failure_strs (metis_lemma_list true) name params;
 
 fun dfg_prover (name, p) = (name, generic_dfg_prover (name, p));
 
-val spass = dfg_prover ("spass", spass_config spass_insert_theory_const);
-val spass_no_tc = dfg_prover ("spass_no_tc", spass_config false);
+fun spass_config_for add_theory_const : prover_config =
+ {command = Path.explode "$SPASS_HOME/SPASS",
+  arguments = (fn timeout => "-Auto -SOS=1 -PGiven=0 -PProblem=0 -Splits=0" ^
+    " -FullRed=0 -DocProof -TimeLimit=" ^
+    string_of_int (Time.toSeconds timeout)),
+  failure_strs =
+    ["SPASS beiseite: Completion found.", "SPASS beiseite: Ran out of time.",
+     "SPASS beiseite: Maximal number of loops exceeded."],
+  max_new_clauses = 40,
+  add_theory_const = add_theory_const,
+  supports_isar_proofs = false};
+
+val spass_config = spass_config_for true
+val spass = dfg_prover ("spass", spass_config)
+
+val spass_no_tc_config = spass_config_for false
+val spass_no_tc = dfg_prover ("spass_no_tc", spass_no_tc_config)
 
 
 (* remote prover invocation via SystemOnTPTP *)
@@ -251,10 +247,12 @@
 
 fun get_systems () =
   let
-    val (answer, rc) = bash_output ("\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w")
+    val (answer, rc) = bash_output "\"$ISABELLE_ATP_MANAGER/SystemOnTPTP\" -w"
   in
-    if rc <> 0 then error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
-    else split_lines answer
+    if rc <> 0 then
+      error ("Failed to get available systems at SystemOnTPTP:\n" ^ answer)
+    else
+      split_lines answer
   end;
 
 fun refresh_systems_on_tptp () =
@@ -271,27 +269,34 @@
 
 val remote_failure_strs = ["Remote-script could not extract proof"];
 
-fun remote_prover_config prover_prefix args max_new insert_tc: prover_config =
- {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
-  arguments = (fn timeout =>
-    args ^ " -t " ^ string_of_int timeout ^ " -s " ^ the_system prover_prefix),
-  failure_strs = remote_failure_strs,
-  max_new_clauses = max_new,
-  insert_theory_const = insert_tc,
-  emit_structured_proof = false};
+fun remote_prover_config prover_prefix args max_new_clauses add_theory_const
+                         : prover_config =
+  {command = Path.explode "$ISABELLE_ATP_MANAGER/SystemOnTPTP",
+   arguments = (fn timeout =>
+     args ^ " -t " ^ string_of_int (Time.toSeconds timeout) ^ " -s " ^
+     the_system prover_prefix),
+   failure_strs = remote_failure_strs,
+   max_new_clauses = max_new_clauses,
+   add_theory_const = add_theory_const,
+   supports_isar_proofs = false}
 
-val remote_vampire = tptp_prover ("remote_vampire", remote_prover_config
-  "Vampire---9" "" vampire_max_new_clauses vampire_insert_theory_const);
+val remote_vampire =
+  tptp_prover "remote_vampire"
+      (remote_prover_config "Vampire---9" ""
+           (#max_new_clauses vampire_config) (#add_theory_const vampire_config))
 
-val remote_eprover = tptp_prover ("remote_e", remote_prover_config
-  "EP---" "" eprover_max_new_clauses eprover_insert_theory_const);
+val remote_e =
+  tptp_prover "remote_e"
+      (remote_prover_config "EP---" ""
+           (#max_new_clauses e_config) (#add_theory_const e_config))
 
-val remote_spass = tptp_prover ("remote_spass", remote_prover_config
-  "SPASS---" "-x" spass_max_new_clauses spass_insert_theory_const);
+val remote_spass =
+  tptp_prover "remote_spass"
+      (remote_prover_config "SPASS---" "-x"
+           (#max_new_clauses spass_config) (#add_theory_const spass_config))
 
 val provers =
-  [spass, vampire, eprover, vampire_isar, eprover_isar, spass_no_tc,
-   remote_vampire, remote_spass, remote_eprover]
+  [spass, vampire, e, spass_no_tc, remote_vampire, remote_spass, remote_e]
 val prover_setup = fold add_prover provers
 
 val setup =
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -346,7 +346,7 @@
     fun monotonicity_message Ts extra =
       let val ss = map (quote o string_for_type ctxt) Ts in
         "The type" ^ plural_s_for_list ss ^ " " ^
-        space_implode " " (serial_commas "and" ss) ^ " " ^
+        space_implode " " (Sledgehammer_Util.serial_commas "and" ss) ^ " " ^
         (if none_true monos then
            "passed the monotonicity test"
          else
@@ -684,7 +684,8 @@
                         options
                 in
                   print ("Try again with " ^
-                         space_implode " " (serial_commas "and" ss) ^
+                         space_implode " "
+                             (Sledgehammer_Util.serial_commas "and" ss) ^
                          " to confirm that the " ^ das_wort_model ^
                          " is genuine.")
                 end
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -24,6 +24,8 @@
 open Nitpick_Nut
 open Nitpick
 
+structure K = OuterKeyword and P = OuterParse
+
 val auto = Unsynchronized.ref false;
 
 val _ =
@@ -34,48 +36,48 @@
 type raw_param = string * string list
 
 val default_default_params =
-  [("card", ["1\<midarrow>8"]),
-   ("iter", ["0,1,2,4,8,12,16,24"]),
-   ("bits", ["1,2,3,4,6,8,10,12"]),
-   ("bisim_depth", ["7"]),
-   ("box", ["smart"]),
-   ("finitize", ["smart"]),
-   ("mono", ["smart"]),
-   ("std", ["true"]),
-   ("wf", ["smart"]),
-   ("sat_solver", ["smart"]),
-   ("batch_size", ["smart"]),
-   ("blocking", ["true"]),
-   ("falsify", ["true"]),
-   ("user_axioms", ["smart"]),
-   ("assms", ["true"]),
-   ("merge_type_vars", ["false"]),
-   ("binary_ints", ["smart"]),
-   ("destroy_constrs", ["true"]),
-   ("specialize", ["true"]),
-   ("skolemize", ["true"]),
-   ("star_linear_preds", ["true"]),
-   ("uncurry", ["true"]),
-   ("fast_descrs", ["true"]),
-   ("peephole_optim", ["true"]),
-   ("timeout", ["30 s"]),
-   ("tac_timeout", ["500 ms"]),
-   ("sym_break", ["20"]),
-   ("sharing_depth", ["3"]),
-   ("flatten_props", ["false"]),
-   ("max_threads", ["0"]),
-   ("verbose", ["false"]),
-   ("debug", ["false"]),
-   ("overlord", ["false"]),
-   ("show_all", ["false"]),
-   ("show_skolems", ["true"]),
-   ("show_datatypes", ["false"]),
-   ("show_consts", ["false"]),
-   ("format", ["1"]),
-   ("max_potential", ["1"]),
-   ("max_genuine", ["1"]),
-   ("check_potential", ["false"]),
-   ("check_genuine", ["false"])]
+  [("card", "1\<midarrow>8"),
+   ("iter", "0,1,2,4,8,12,16,24"),
+   ("bits", "1,2,3,4,6,8,10,12"),
+   ("bisim_depth", "7"),
+   ("box", "smart"),
+   ("finitize", "smart"),
+   ("mono", "smart"),
+   ("std", "true"),
+   ("wf", "smart"),
+   ("sat_solver", "smart"),
+   ("batch_size", "smart"),
+   ("blocking", "true"),
+   ("falsify", "true"),
+   ("user_axioms", "smart"),
+   ("assms", "true"),
+   ("merge_type_vars", "false"),
+   ("binary_ints", "smart"),
+   ("destroy_constrs", "true"),
+   ("specialize", "true"),
+   ("skolemize", "true"),
+   ("star_linear_preds", "true"),
+   ("uncurry", "true"),
+   ("fast_descrs", "true"),
+   ("peephole_optim", "true"),
+   ("timeout", "30 s"),
+   ("tac_timeout", "500 ms"),
+   ("sym_break", "20"),
+   ("sharing_depth", "3"),
+   ("flatten_props", "false"),
+   ("max_threads", "0"),
+   ("debug", "false"),
+   ("verbose", "false"),
+   ("overlord", "false"),
+   ("show_all", "false"),
+   ("show_skolems", "true"),
+   ("show_datatypes", "false"),
+   ("show_consts", "false"),
+   ("format", "1"),
+   ("max_potential", "1"),
+   ("max_genuine", "1"),
+   ("check_potential", "false"),
+   ("check_genuine", "false")]
 
 val negated_params =
   [("dont_box", "box"),
@@ -97,8 +99,8 @@
    ("full_descrs", "fast_descrs"),
    ("no_peephole_optim", "peephole_optim"),
    ("dont_flatten_props", "flatten_props"),
+   ("no_debug", "debug"),
    ("quiet", "verbose"),
-   ("no_debug", "debug"),
    ("no_overlord", "overlord"),
    ("dont_show_all", "show_all"),
    ("hide_skolems", "show_skolems"),
@@ -119,7 +121,7 @@
 (* string * 'a -> unit *)
 fun check_raw_param (s, _) =
   if is_known_raw_param s then ()
-  else error ("Unknown parameter " ^ quote s ^ ".")  
+  else error ("Unknown parameter: " ^ quote s ^ ".")  
 
 (* string -> string option *)
 fun unnegate_param_name name =
@@ -139,20 +141,15 @@
   | NONE => (name, value)
 
 structure Data = Theory_Data(
-  type T = {params: raw_param list}
-  val empty = {params = rev default_default_params}
+  type T = raw_param list
+  val empty = default_default_params |> map (apsnd single)
   val extend = I
-  fun merge ({params = ps1}, {params = ps2}) : T =
-    {params = AList.merge (op =) (K true) (ps1, ps2)})
+  fun merge p : T = AList.merge (op =) (K true) p)
 
 (* raw_param -> theory -> theory *)
-fun set_default_raw_param param thy =
-  let val {params} = Data.get thy in
-    Data.put {params = AList.update (op =) (unnegate_raw_param param) params}
-             thy
-  end
+val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
 (* theory -> raw_param list *)
-val default_raw_params = #params o Data.get
+val default_raw_params = Data.get
 
 (* string -> bool *)
 fun is_punctuation s = (s = "," orelse s = "-" orelse s = "\<midarrow>")
@@ -164,26 +161,6 @@
     s1 ^ (if is_punctuation s1 orelse is_punctuation s2 then "" else " ") ^
     stringify_raw_param_value (s2 :: ss)
 
-(* bool -> string -> string -> bool option *)
-fun bool_option_from_string option name s =
-  (case s of
-     "smart" => if option then NONE else raise Option
-   | "false" => SOME false
-   | "true" => SOME true
-   | "" => SOME true
-   | _ => raise Option)
-  handle Option.Option =>
-         let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
-           error ("Parameter " ^ quote name ^ " must be assigned " ^
-                  space_implode " " (serial_commas "or" ss) ^ ".")
-         end
-(* bool -> raw_param list -> bool option -> string -> bool option *)
-fun general_lookup_bool option raw_params default_value name =
-  case AList.lookup (op =) raw_params name of
-    SOME s => s |> stringify_raw_param_value
-                |> bool_option_from_string option name
-  | NONE => default_value
-
 (* int -> string -> int *)
 fun maxed_int_from_string min_int s = Int.max (min_int, the (Int.fromString s))
 
@@ -192,14 +169,19 @@
   let
     val override_params = map unnegate_raw_param override_params
     val raw_params = rev override_params @ rev default_params
+    (* string -> string *)
     val lookup =
       Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
-    (* string -> string *)
-    fun lookup_string name = the_default "" (lookup name)
+    val lookup_string = the_default "" o lookup
+    (* bool -> bool option -> string -> bool option *)
+    fun general_lookup_bool option default_value name =
+      case lookup name of
+        SOME s => Sledgehammer_Util.parse_bool_option option name s
+      | NONE => default_value
     (* string -> bool *)
-    val lookup_bool = the o general_lookup_bool false raw_params (SOME false)
+    val lookup_bool = the o general_lookup_bool false (SOME false)
     (* string -> bool option *)
-    val lookup_bool_option = general_lookup_bool true raw_params NONE
+    val lookup_bool_option = general_lookup_bool true NONE
     (* string -> string option -> int *)
     fun do_int name value =
       case value of
@@ -253,7 +235,8 @@
       :: map (fn (name, value) =>
                  (SOME (read (String.extract (name, size prefix + 1, NONE))),
                   value |> stringify_raw_param_value
-                        |> bool_option_from_string false name |> the))
+                        |> Sledgehammer_Util.parse_bool_option false name
+                        |> the))
              (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
     (* (string -> 'a) -> string -> ('a option * bool option) list *)
     fun lookup_bool_option_assigns read prefix =
@@ -261,28 +244,13 @@
       :: map (fn (name, value) =>
                  (SOME (read (String.extract (name, size prefix + 1, NONE))),
                   value |> stringify_raw_param_value
-                        |> bool_option_from_string true name))
+                        |> Sledgehammer_Util.parse_bool_option true name))
              (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
     (* string -> Time.time option *)
     fun lookup_time name =
       case lookup name of
         NONE => NONE
-      | SOME "none" => NONE
-      | SOME s =>
-        let
-          val msecs =
-            case space_explode " " s of
-              [s1, "min"] => 60000 * the (Int.fromString s1)
-            | [s1, "s"] => 1000 * the (Int.fromString s1)
-            | [s1, "ms"] => the (Int.fromString s1)
-            | _ => 0
-        in
-          if msecs <= 0 then
-            error ("Parameter " ^ quote name ^ " must be assigned a positive \
-                   \time value (e.g., \"60 s\", \"200 ms\") or \"none\".")
-          else
-            SOME (Time.fromMilliseconds msecs)
-        end
+      | SOME s => Sledgehammer_Util.parse_time_option name s
     (* string -> term list *)
     val lookup_term_list =
       AList.lookup (op =) raw_params #> these #> Syntax.read_terms ctxt
@@ -368,22 +336,18 @@
   extract_params (ProofContext.init thy) false (default_raw_params thy)
   o map (apsnd single)
 
-(* OuterParse.token list -> string * OuterParse.token list *)
-val scan_key = Scan.repeat1 OuterParse.typ_group >> space_implode " "
-
-(* OuterParse.token list -> string list * OuterParse.token list *)
-val scan_value =
-  Scan.repeat1 (OuterParse.minus >> single
-                || Scan.repeat1 (Scan.unless OuterParse.minus OuterParse.name)
-                || OuterParse.$$$ "," |-- OuterParse.number >> prefix ","
-                   >> single) >> flat
-
-(* OuterParse.token list -> raw_param * OuterParse.token list *)
-val scan_param =
-  scan_key -- (Scan.option (OuterParse.$$$ "=" |-- scan_value) >> these)
-(* OuterParse.token list -> raw_param list option * OuterParse.token list *)
-val scan_params = Scan.option (OuterParse.$$$ "[" |-- OuterParse.list scan_param
-                               --| OuterParse.$$$ "]")
+(* P.token list -> string * P.token list *)
+val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+(* P.token list -> string list * P.token list *)
+val parse_value =
+  Scan.repeat1 (P.minus >> single
+                || Scan.repeat1 (Scan.unless P.minus P.name)
+                || P.$$$ "," |-- P.number >> prefix "," >> single) >> flat
+(* P.token list -> raw_param * P.token list *)
+val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
+(* P.token list -> raw_param list * P.token list *)
+val parse_params =
+  Scan.optional (P.$$$ "[" |-- P.list parse_param --| P.$$$ "]") []
 
 (* Proof.context -> ('a -> 'a) -> 'a -> 'a *)
 fun handle_exceptions ctxt f x =
@@ -423,7 +387,6 @@
        | Refute.REFUTE (loc, details) =>
          error ("Unhandled Refute error (" ^ quote loc ^ "): " ^ details ^ ".")
 
-
 (* raw_param list -> bool -> int -> int -> Proof.state -> bool * Proof.state *)
 fun pick_nits override_params auto i step state =
   let
@@ -445,21 +408,20 @@
     else (Toplevel.thread true (fn () => (go (); ())); (false, state))
   end
 
-(* raw_param list option * int option -> Toplevel.transition
-   -> Toplevel.transition *)
-fun nitpick_trans (opt_params, opt_i) =
+(* raw_param list * int -> Toplevel.transition -> Toplevel.transition *)
+fun nitpick_trans (params, i) =
   Toplevel.keep (fn st =>
-      (pick_nits (these opt_params) false (the_default 1 opt_i)
-                 (Toplevel.proof_position_of st) (Toplevel.proof_of st); ()))
+      (pick_nits params false i (Toplevel.proof_position_of st)
+                 (Toplevel.proof_of st); ()))
 
 (* raw_param -> string *)
 fun string_for_raw_param (name, value) =
   name ^ " = " ^ stringify_raw_param_value value
 
-(* raw_param list option -> Toplevel.transition -> Toplevel.transition *)
-fun nitpick_params_trans opt_params =
+(* raw_param list -> Toplevel.transition -> Toplevel.transition *)
+fun nitpick_params_trans params =
   Toplevel.theory
-      (fold set_default_raw_param (these opt_params)
+      (fold set_default_raw_param params
        #> tap (fn thy => 
                   writeln ("Default parameters for Nitpick:\n" ^
                            (case rev (default_raw_params thy) of
@@ -469,18 +431,18 @@
                                params |> map string_for_raw_param
                                       |> sort_strings |> cat_lines)))))
 
-(* OuterParse.token list
-   -> (Toplevel.transition -> Toplevel.transition) * OuterParse.token list *)
-val scan_nitpick_command =
-  (scan_params -- Scan.option OuterParse.nat) #>> nitpick_trans
-val scan_nitpick_params_command = scan_params #>> nitpick_params_trans
+(* P.token list
+   -> (Toplevel.transition -> Toplevel.transition) * P.token list *)
+val parse_nitpick_command =
+  (parse_params -- Scan.optional P.nat 1) #>> nitpick_trans
+val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
 
 val _ = OuterSyntax.improper_command "nitpick"
             "try to find a counterexample for a given subgoal using Kodkod"
-            OuterKeyword.diag scan_nitpick_command
+            K.diag parse_nitpick_command
 val _ = OuterSyntax.command "nitpick_params"
             "set and display the default parameters for Nitpick"
-            OuterKeyword.thy_decl scan_nitpick_params_command
+            K.thy_decl parse_nitpick_params_command
 
 (* Proof.state -> bool * Proof.state *)
 fun auto_nitpick state =
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -194,8 +194,11 @@
               else
                 [])
   in
-    if null ss then []
-    else serial_commas "and" ss |> map Pretty.str |> Pretty.breaks
+    if null ss then
+      []
+    else
+      Sledgehammer_Util.serial_commas "and" ss
+      |> map Pretty.str |> Pretty.breaks
   end
 
 (* scope -> string *)
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -46,7 +46,6 @@
   val triple_lookup :
     (''a * ''a -> bool) -> (''a option * 'b) list -> ''a -> 'b option
   val is_substring_of : string -> string -> bool
-  val serial_commas : string -> string list -> string list
   val plural_s : int -> string
   val plural_s_for_list : 'a list -> string
   val flip_polarity : polarity -> polarity
@@ -233,13 +232,6 @@
   not (Substring.isEmpty (snd (Substring.position needle
                                                   (Substring.full stack))))
 
-(* string -> string list -> string list *)
-fun serial_commas _ [] = ["??"]
-  | serial_commas _ [s] = [s]
-  | serial_commas conj [s1, s2] = [s1, conj, s2]
-  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
-  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
-
 (* int -> string *)
 fun plural_s n = if n = 1 then "" else "s"
 (* 'a list -> string *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_filter.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -9,12 +9,19 @@
   type axiom_name = Sledgehammer_HOL_Clause.axiom_name
   type hol_clause = Sledgehammer_HOL_Clause.hol_clause
   type hol_clause_id = Sledgehammer_HOL_Clause.hol_clause_id
+  type relevance_override =
+    {add: Facts.ref list,
+     del: Facts.ref list,
+     only: bool}
+
   val tvar_classes_of_terms : term list -> string list
   val tfree_classes_of_terms : term list -> string list
   val type_consts_of_terms : theory -> term list -> string list
-  val get_relevant_facts : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
-    (thm * (string * int)) list
-  val prepare_clauses : bool -> thm list -> thm list ->
+  val get_relevant_facts :
+    real -> bool option -> bool -> int -> bool -> relevance_override
+    -> Proof.context * (thm list * 'a) -> thm list
+    -> (thm * (string * int)) list
+  val prepare_clauses : bool option -> bool -> thm list -> thm list ->
     (thm * (axiom_name * hol_clause_id)) list ->
     (thm * (axiom_name * hol_clause_id)) list -> theory ->
     axiom_name vector *
@@ -29,29 +36,21 @@
 open Sledgehammer_Fact_Preprocessor
 open Sledgehammer_HOL_Clause
 
-type axiom_name = axiom_name
-type hol_clause = hol_clause
-type hol_clause_id = hol_clause_id
+type relevance_override =
+  {add: Facts.ref list,
+   del: Facts.ref list,
+   only: bool}
 
 (********************************************************************)
 (* some settings for both background automatic ATP calling procedure*)
 (* and also explicit ATP invocation methods                         *)
 (********************************************************************)
 
-(* Translation mode can be auto-detected, or forced to be first-order or
-   higher-order *)
-datatype mode = Auto | Fol | Hol;
-
-val translation_mode = Auto;
-
 (*** background linkup ***)
 val run_blacklist_filter = true;
 
 (*** relevance filter parameters ***)
-val run_relevance_filter = true;
-val pass_mark = 0.5;
 val convergence = 3.2;    (*Higher numbers allow longer inference chains*)
-val follow_defs = false;  (*Follow definitions. Makes problems bigger.*)
   
 (***************************************************************)
 (* Relevance Filtering                                         *)
@@ -139,8 +138,8 @@
 
 (*Inserts a dummy "constant" referring to the theory name, so that relevance
   takes the given theory into account.*)
-fun const_prop_of theory_const th =
- if theory_const then
+fun const_prop_of add_theory_const th =
+ if add_theory_const then
   let val name = Context.theory_name (theory_of_thm th)
       val t = Const (name ^ ". 1", HOLogic.boolT)
   in  t $ prop_of th  end
@@ -169,7 +168,7 @@
 
 structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
 
-fun count_axiom_consts theory_const thy ((thm,_), tab) = 
+fun count_axiom_consts add_theory_const thy ((thm,_), tab) = 
   let fun count_const (a, T, tab) =
         let val (c, cts) = const_with_typ thy (a,T)
         in  (*Two-dimensional table update. Constant maps to types maps to count.*)
@@ -182,7 +181,7 @@
             count_term_consts (t, count_term_consts (u, tab))
         | count_term_consts (Abs(_,_,t), tab) = count_term_consts (t, tab)
         | count_term_consts (_, tab) = tab
-  in  count_term_consts (const_prop_of theory_const thm, tab)  end;
+  in  count_term_consts (const_prop_of add_theory_const thm, tab)  end;
 
 
 (**** Actual Filtering Code ****)
@@ -214,8 +213,8 @@
   let val tab = add_term_consts_typs_rm thy (t, null_const_tab)
   in  Symtab.fold add_expand_pairs tab []  end;
 
-fun pair_consts_typs_axiom theory_const thy (thm,name) =
-    ((thm,name), (consts_typs_of_term thy (const_prop_of theory_const thm)));
+fun pair_consts_typs_axiom add_theory_const thy (p as (thm, _)) =
+  (p, (consts_typs_of_term thy (const_prop_of add_theory_const thm)));
 
 exception ConstFree;
 fun dest_ConstFree (Const aT) = aT
@@ -234,9 +233,10 @@
             end
             handle ConstFree => false
     in    
-        case tm of @{const Trueprop} $ (Const(@{const_name "op ="}, _) $ lhs $ rhs) => 
-                   defs lhs rhs 
-                 | _ => false
+        case tm of
+          @{const Trueprop} $ (Const (@{const_name "op ="}, _) $ lhs $ rhs) => 
+            defs lhs rhs 
+        | _ => false
     end;
 
 type annotd_cls = (thm * (string * int)) * ((string * const_typ list) list);
@@ -263,8 +263,12 @@
       end
   end;
 
-fun relevant_clauses max_new thy ctab p rel_consts =
-  let fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
+fun relevant_clauses ctxt follow_defs max_new
+                     (relevance_override as {add, del, only}) thy ctab p
+                     rel_consts =
+  let val add_thms = maps (ProofContext.get_fact ctxt) add
+      val del_thms = maps (ProofContext.get_fact ctxt) del
+      fun relevant ([],_) [] = [] : (thm * (string * int)) list  (*Nothing added this iteration*)
         | relevant (newpairs,rejects) [] =
             let val (newrels,more_rejects) = take_best max_new newpairs
                 val new_consts = maps #2 newrels
@@ -272,11 +276,17 @@
                 val newp = p + (1.0-p) / convergence
             in
               trace_msg (fn () => "relevant this iteration: " ^ Int.toString (length newrels));
-               (map #1 newrels) @ 
-               (relevant_clauses max_new thy ctab newp rel_consts' (more_rejects@rejects))
+                map #1 newrels @ 
+                relevant_clauses ctxt follow_defs max_new relevance_override thy ctab
+                                 newp rel_consts' (more_rejects @ rejects)
             end
-        | relevant (newrels,rejects) ((ax as (clsthm as (_,(name,n)),consts_typs)) :: axs) =
-            let val weight = clause_weight ctab rel_consts consts_typs
+        | relevant (newrels, rejects)
+                   ((ax as (clsthm as (thm, (name, n)), consts_typs)) :: axs) =
+            let
+              val weight = if member Thm.eq_thm del_thms thm then 0.0
+                           else if member Thm.eq_thm add_thms thm then 1.0
+                           else if only then 0.0
+                           else clause_weight ctab rel_consts consts_typs
             in
               if p <= weight orelse (follow_defs andalso defines thy (#1 clsthm) rel_consts)
               then (trace_msg (fn () => (name ^ " clause " ^ Int.toString n ^ 
@@ -285,23 +295,30 @@
               else relevant (newrels, ax::rejects) axs
             end
     in  trace_msg (fn () => ("relevant_clauses, current pass mark = " ^ Real.toString p));
-        relevant ([],[]) 
+        relevant ([],[])
     end;
         
-fun relevance_filter max_new theory_const thy axioms goals = 
- if run_relevance_filter andalso pass_mark >= 0.1
- then
-  let val const_tab = List.foldl (count_axiom_consts theory_const thy) Symtab.empty axioms
+fun relevance_filter ctxt relevance_threshold follow_defs max_new
+                     add_theory_const relevance_override thy axioms goals = 
+  if relevance_threshold > 0.0 then
+    let
+      val const_tab = List.foldl (count_axiom_consts add_theory_const thy)
+                                 Symtab.empty axioms
       val goal_const_tab = get_goal_consts_typs thy goals
-      val _ = trace_msg (fn () => ("Initial constants: " ^
-                                 space_implode ", " (Symtab.keys goal_const_tab)));
-      val rels = relevant_clauses max_new thy const_tab (pass_mark) 
-                   goal_const_tab  (map (pair_consts_typs_axiom theory_const thy) axioms)
-  in
-      trace_msg (fn () => ("Total relevant: " ^ Int.toString (length rels)));
-      rels
-  end
- else axioms;
+      val _ =
+        trace_msg (fn () => "Initial constants: " ^
+                            commas (Symtab.keys goal_const_tab))
+      val relevant =
+        relevant_clauses ctxt follow_defs max_new relevance_override thy
+                         const_tab relevance_threshold goal_const_tab
+                         (map (pair_consts_typs_axiom add_theory_const thy)
+                              axioms)
+    in
+      trace_msg (fn () => "Total relevant: " ^ Int.toString (length relevant));
+      relevant
+    end
+  else
+    axioms;
 
 (***************************************************************)
 (* Retrieving and filtering lemmas                             *)
@@ -526,34 +543,37 @@
   likely to lead to unsound proofs.*)
 fun remove_unwanted_clauses cls = filter (not o unwanted o prop_of o fst) cls;
 
-fun is_first_order thy goal_cls =
-  case translation_mode of
-    Auto => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
-  | Fol => true
-  | Hol => false
+fun is_first_order thy higher_order goal_cls =
+  case higher_order of
+    NONE => forall (Meson.is_fol_term thy) (map prop_of goal_cls)
+  | SOME b => not b
 
-fun get_relevant_facts max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
+fun get_relevant_facts relevance_threshold higher_order follow_defs max_new
+                       add_theory_const relevance_override
+                       (ctxt, (chain_ths, th)) goal_cls =
   let
     val thy = ProofContext.theory_of ctxt
-    val is_FO = is_first_order thy goal_cls
+    val is_FO = is_first_order thy higher_order goal_cls
     val included_cls = get_all_lemmas ctxt
       |> cnf_rules_pairs thy |> make_unique
       |> restrict_to_logic thy is_FO
       |> remove_unwanted_clauses
   in
-    relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls) 
+    relevance_filter ctxt relevance_threshold follow_defs max_new
+                     add_theory_const relevance_override thy included_cls
+                     (map prop_of goal_cls)
   end;
 
 (* prepare for passing to writer,
    create additional clauses based on the information from extra_cls *)
-fun prepare_clauses dfg goal_cls chain_ths axcls extra_cls thy =
+fun prepare_clauses higher_order dfg goal_cls chain_ths axcls extra_cls thy =
   let
     (* add chain thms *)
     val chain_cls =
       cnf_rules_pairs thy (filter check_named (map pairname chain_ths))
     val axcls = chain_cls @ axcls
     val extra_cls = chain_cls @ extra_cls
-    val is_FO = is_first_order thy goal_cls
+    val is_FO = is_first_order thy higher_order goal_cls
     val ccls = subtract_cls goal_cls extra_cls
     val _ = app (fn th => trace_msg (fn _ => Display.string_of_thm_global thy th)) ccls
     val ccltms = map prop_of ccls
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -51,9 +51,9 @@
   conclusion variable to False.*)
 fun transform_elim th =
   case concl_of th of    (*conclusion variable*)
-       Const("Trueprop",_) $ (v as Var(_,Type("bool",[]))) =>
+       @{const Trueprop} $ (v as Var (_, @{typ bool})) =>
            Thm.instantiate ([], [(cterm_of @{theory HOL} v, cfalse)]) th
-    | v as Var(_, Type("prop",[])) =>
+    | v as Var(_, @{typ prop}) =>
            Thm.instantiate ([], [(cterm_of @{theory HOL} v, ctp_false)]) th
     | _ => th;
 
@@ -76,7 +76,7 @@
 fun declare_skofuns s th =
   let
     val nref = Unsynchronized.ref 0    (* FIXME ??? *)
-    fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
+    fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs (_, T, p))) (axs, thy) =
           (*Existential: declare a Skolem function, then insert into body and continue*)
           let
             val cname = skolem_prefix ^ s ^ "_" ^ Int.toString (Unsynchronized.inc nref)
@@ -95,20 +95,20 @@
               Theory.add_defs_i true false [(Binding.name cdef, Logic.mk_equals (c, rhs))] thy'
             val ax = Thm.axiom thy'' (Sign.full_bname thy'' cdef)
           in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
-      | dec_sko (Const ("All", _) $ (Abs (a, T, p))) thx =
+      | dec_sko (Const (@{const_name All}, _) $ (Abs (a, T, p))) thx =
           (*Universal quant: insert a free variable into body and continue*)
           let val fname = Name.variant (OldTerm.add_term_names (p, [])) a
           in dec_sko (subst_bound (Free (fname, T), p)) thx end
-      | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
-      | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
-      | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
+      | dec_sko (@{const "op &"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+      | dec_sko (@{const "op |"} $ p $ q) thx = dec_sko q (dec_sko p thx)
+      | dec_sko (@{const Trueprop} $ p) thx = dec_sko p thx
       | dec_sko t thx = thx (*Do nothing otherwise*)
   in fn thy => dec_sko (Thm.prop_of th) ([], thy) end;
 
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun assume_skofuns s th =
   let val sko_count = Unsynchronized.ref 0   (* FIXME ??? *)
-      fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) defs =
+      fun dec_sko (Const (@{const_name Ex}, _) $ (xtp as Abs(_,T,p))) defs =
             (*Existential: declare a Skolem function, then insert into body and continue*)
             let val skos = map (#1 o Logic.dest_equals) defs  (*existing sko fns*)
                 val args = subtract (op =) skos (OldTerm.term_frees xtp) (*the formal parameters*)
@@ -123,13 +123,13 @@
             in dec_sko (subst_bound (list_comb(c,args), p))
                        (def :: defs)
             end
-        | dec_sko (Const ("All",_) $ Abs (a, T, p)) defs =
+        | dec_sko (Const (@{const_name All},_) $ Abs (a, T, p)) defs =
             (*Universal quant: insert a free variable into body and continue*)
             let val fname = Name.variant (OldTerm.add_term_names (p,[])) a
             in dec_sko (subst_bound (Free(fname,T), p)) defs end
-        | dec_sko (Const ("op &", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
-        | dec_sko (Const ("op |", _) $ p $ q) defs = dec_sko q (dec_sko p defs)
-        | dec_sko (Const ("Trueprop", _) $ p) defs = dec_sko p defs
+        | dec_sko (@{const "op &"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+        | dec_sko (@{const "op |"} $ p $ q) defs = dec_sko q (dec_sko p defs)
+        | dec_sko (@{const Trueprop} $ p) defs = dec_sko p defs
         | dec_sko t defs = defs (*Do nothing otherwise*)
   in  dec_sko (prop_of th) []  end;
 
@@ -156,7 +156,7 @@
 fun strip_lambdas 0 th = th
   | strip_lambdas n th =
       case prop_of th of
-          _ $ (Const ("op =", _) $ _ $ Abs (x,_,_)) =>
+          _ $ (Const (@{const_name "op ="}, _) $ _ $ Abs (x, _, _)) =>
               strip_lambdas (n-1) (freeze_thm (th RS xfun_cong x))
         | _ => th;
 
@@ -171,7 +171,7 @@
   let
       val thy = theory_of_cterm ct
       val Abs(x,_,body) = term_of ct
-      val Type("fun",[xT,bodyT]) = typ_of (ctyp_of_term ct)
+      val Type(@{type_name fun}, [xT,bodyT]) = typ_of (ctyp_of_term ct)
       val cxT = ctyp_of thy xT and cbodyT = ctyp_of thy bodyT
       fun makeK() = instantiate' [SOME cxT, SOME cbodyT] [SOME (cterm_of thy body)] @{thm abs_K}
   in
@@ -262,8 +262,9 @@
       val (chilbert,cabs) = Thm.dest_comb ch
       val thy = Thm.theory_of_cterm chilbert
       val t = Thm.term_of chilbert
-      val T = case t of Const ("Hilbert_Choice.Eps", Type("fun",[_,T])) => T
-                      | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
+      val T = case t of
+                Const (@{const_name Eps}, Type (@{type_name fun},[_,T])) => T
+              | _ => raise THM ("skolem_of_def: expected Eps", 0, [def])
       val cex = Thm.cterm_of thy (HOLogic.exists_const T)
       val ex_tm = c_mkTrueprop (Thm.capply cex cabs)
       and conc =  c_mkTrueprop (Drule.beta_conv cabs (Drule.list_comb(c,frees)));
@@ -289,7 +290,7 @@
   map (skolem_of_def o assume o (cterm_of (theory_of_thm th))) (assume_skofuns s th);
 
 
-(*** Blacklisting (duplicated in "Sledgehammer_Fact_Filter"?) ***)
+(*** Blacklisting (FIXME: duplicated in "Sledgehammer_Fact_Filter"?) ***)
 
 val max_lambda_nesting = 3;
 
@@ -320,7 +321,8 @@
 
 fun is_strange_thm th =
   case head_of (concl_of th) of
-      Const (a, _) => (a <> "Trueprop" andalso a <> "==")
+      Const (a, _) => (a <> @{const_name Trueprop} andalso
+                       a <> @{const_name "=="})
     | _ => false;
 
 fun bad_for_atp th =
@@ -328,9 +330,10 @@
   orelse exists_type type_has_topsort (prop_of th)
   orelse is_strange_thm th;
 
+(* FIXME: put other record thms here, or declare as "no_atp" *)
 val multi_base_blacklist =
-  ["defs","select_defs","update_defs","induct","inducts","split","splits","split_asm",
-   "cases","ext_cases"];  (* FIXME put other record thms here, or declare as "no_atp" *)
+  ["defs", "select_defs", "update_defs", "induct", "inducts", "split", "splits",
+   "split_asm", "cases", "ext_cases"];
 
 (*Keep the full complexity of the original name*)
 fun flatten_name s = space_implode "_X" (Long_Name.explode s);
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -48,7 +48,7 @@
 open Sledgehammer_FOL_Clause
 open Sledgehammer_Fact_Preprocessor
 
-(* Parameter t_full below indicates that full type information is to be
+(* Parameter "full_types" below indicates that full type information is to be
 exported *)
 
 (* If true, each function will be directly applied to as many arguments as
@@ -210,10 +210,8 @@
 fun head_needs_hBOOL const_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL const_needs_hBOOL c
   | head_needs_hBOOL _ _ = true;
 
-fun wrap_type t_full (s, tp) =
-  if t_full then
-      type_wrapper ^ paren_pack [s, string_of_fol_type tp]
-  else s;
+fun wrap_type full_types (s, tp) =
+  if full_types then type_wrapper ^ paren_pack [s, string_of_fol_type tp] else s;
 
 fun apply ss = "hAPP" ^ paren_pack ss;
 
@@ -224,7 +222,7 @@
 
 (*Apply an operator to the argument strings, using either the "apply" operator or
   direct function application.*)
-fun string_of_applic t_full cma (CombConst (c, _, tvars), args) =
+fun string_of_applic full_types cma (CombConst (c, _, tvars), args) =
       let val c = if c = "equal" then "c_fequal" else c
           val nargs = min_arity_of cma c
           val args1 = List.take(args, nargs)
@@ -232,21 +230,22 @@
                                          Int.toString nargs ^ " but is applied to " ^
                                          space_implode ", " args)
           val args2 = List.drop(args, nargs)
-          val targs = if not t_full then map string_of_fol_type tvars else []
+          val targs = if full_types then [] else map string_of_fol_type tvars
       in
           string_apply (c ^ paren_pack (args1@targs), args2)
       end
   | string_of_applic _ _ (CombVar (v, _), args) = string_apply (v, args)
   | string_of_applic _ _ _ = error "string_of_applic";
 
-fun wrap_type_if t_full cnh (head, s, tp) =
-  if head_needs_hBOOL cnh head then wrap_type t_full (s, tp) else s;
+fun wrap_type_if full_types cnh (head, s, tp) =
+  if head_needs_hBOOL cnh head then wrap_type full_types (s, tp) else s;
 
-fun string_of_combterm (params as (t_full, cma, cnh)) t =
+fun string_of_combterm (params as (full_types, cma, cnh)) t =
   let val (head, args) = strip_combterm_comb t
-  in  wrap_type_if t_full cnh (head,
-                    string_of_applic t_full cma (head, map (string_of_combterm (params)) args),
-                    type_of_combterm t)
+  in  wrap_type_if full_types cnh (head,
+          string_of_applic full_types cma
+                           (head, map (string_of_combterm (params)) args),
+          type_of_combterm t)
   end;
 
 (*Boolean-valued terms are here converted to literals.*)
@@ -318,11 +317,11 @@
 
 fun addtypes tvars tab = List.foldl add_foltype_funcs tab tvars;
 
-fun add_decls (t_full, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
+fun add_decls (full_types, cma, cnh) (CombConst (c, _, tvars), (funcs, preds)) =
       if c = "equal" then (addtypes tvars funcs, preds)
       else
         let val arity = min_arity_of cma c
-            val ntys = if not t_full then length tvars else 0
+            val ntys = if not full_types then length tvars else 0
             val addit = Symtab.update(c, arity+ntys)
         in
             if needs_hBOOL cnh c then (addtypes tvars (addit funcs), preds)
@@ -452,12 +451,12 @@
 
 (* TPTP format *)
 
-fun write_tptp_file t_full file clauses =
+fun write_tptp_file full_types file clauses =
   let
     val (conjectures, axclauses, _, helper_clauses,
       classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
-    val params = (t_full, cma, cnh)
+    val params = (full_types, cma, cnh)
     val (tptp_clss,tfree_litss) = ListPair.unzip (map (clause2tptp params) conjectures)
     val tfree_clss = map tptp_tfree_clause (List.foldl (uncurry (union (op =))) [] tfree_litss)
     val _ =
@@ -474,12 +473,12 @@
 
 (* DFG format *)
 
-fun write_dfg_file t_full file clauses =
+fun write_dfg_file full_types file clauses =
   let
     val (conjectures, axclauses, _, helper_clauses,
       classrel_clauses, arity_clauses) = clauses
     val (cma, cnh) = count_constants clauses
-    val params = (t_full, cma, cnh)
+    val params = (full_types, cma, cnh)
     val (dfg_clss, tfree_litss) = ListPair.unzip (map (clause2dfg params) conjectures)
     and probname = Path.implode (Path.base file)
     val axstrs = map (#1 o (clause2dfg params)) axclauses
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -4,84 +4,292 @@
 Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
 *)
 
-structure Sledgehammer_Isar : sig end =
+signature SLEDGEHAMMER_ISAR =
+sig
+  type params = ATP_Manager.params
+
+  val default_params : theory -> (string * string) list -> params
+end;
+
+structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
 struct
 
+open Sledgehammer_Util
 open ATP_Manager
 open ATP_Minimal
+open ATP_Wrapper
 
 structure K = OuterKeyword and P = OuterParse
 
-val _ =
-  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
+fun add_to_relevance_override ns : relevance_override =
+  {add = ns, del = [], only = false}
+fun del_from_relevance_override ns : relevance_override =
+  {add = [], del = ns, only = false}
+fun only_relevance_override ns : relevance_override =
+  {add = ns, del = [], only = true}
+val default_relevance_override = add_to_relevance_override []
+fun merge_relevance_override_pairwise r1 r2 : relevance_override =
+  {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
+   only = #only r1 orelse #only r2} 
+fun merge_relevance_overrides rs =
+  fold merge_relevance_override_pairwise rs default_relevance_override
 
-val _ =
-  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
+type raw_param = string * string list
+
+val default_default_params =
+  [("debug", "false"),
+   ("verbose", "false"),
+   ("relevance_threshold", "50"),
+   ("higher_order", "smart"),
+   ("respect_no_atp", "true"),
+   ("follow_defs", "false"),
+   ("isar_proof", "false"),
+   ("minimize_timeout", "5 s")]
 
-val _ =
-  OuterSyntax.improper_command "atp_messages" "print recent messages issued by managed provers" K.diag
-    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
-      (fn limit => Toplevel.no_timing o Toplevel.imperative (fn () => messages limit)));
+val negated_params =
+  [("no_debug", "debug"),
+   ("quiet", "verbose"),
+   ("partial_types", "full_types"),
+   ("first_order", "higher_order"),
+   ("ignore_no_atp", "respect_no_atp"),
+   ("dont_follow_defs", "follow_defs"),
+   ("metis_proof", "isar_proof")]
+
+val property_dependent_params = ["atps", "full_types", "timeout"]
+
+fun is_known_raw_param s =
+  AList.defined (op =) default_default_params s orelse
+  AList.defined (op =) negated_params s orelse
+  member (op =) property_dependent_params s
 
-val _ =
-  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
-      Toplevel.keep (print_provers o Toplevel.theory_of)));
+fun check_raw_param (s, _) =
+  if is_known_raw_param s then ()
+  else error ("Unknown parameter: " ^ quote s ^ ".")
+
+fun unnegate_raw_param (name, value) =
+  case AList.lookup (op =) negated_params name of
+    SOME name' => (name', case value of
+                            ["false"] => ["true"]
+                          | ["true"] => ["false"]
+                          | [] => ["false"]
+                          | _ => value)
+  | NONE => (name, value)
+
+structure Data = Theory_Data(
+  type T = raw_param list
+  val empty = default_default_params |> map (apsnd single)
+  val extend = I
+  fun merge p : T = AList.merge (op =) (K true) p)
 
-val _ =
-  OuterSyntax.command "sledgehammer"
-    "search for first-order proof using automatic theorem provers" K.diag
-    (Scan.repeat P.xname >> (fn names => Toplevel.no_timing o Toplevel.unknown_proof o
-      Toplevel.keep (sledgehammer names o Toplevel.proof_of)));
+val set_default_raw_param = Data.map o AList.update (op =) o unnegate_raw_param
+fun default_raw_params thy =
+  [("atps", [!atps]),
+   ("full_types", [if !full_types then "true" else "false"]),
+   ("timeout", [string_of_int (!timeout) ^ " s"])] @
+  Data.get thy
 
-val default_minimize_prover = "remote_vampire"
-val default_minimize_time_limit = 5
+val infinity_time_in_secs = 60 * 60 * 24 * 365
+val the_timeout = the_default (Time.fromSeconds infinity_time_in_secs)
 
-fun atp_minimize_command args thm_names state =
+fun extract_params thy default_params override_params =
   let
-    fun theorems_from_names ctxt =
-      map (fn (name, interval) =>
+    val override_params = map unnegate_raw_param override_params
+    val raw_params = rev override_params @ rev default_params
+    val lookup = Option.map (space_implode " ") o AList.lookup (op =) raw_params
+    val lookup_string = the_default "" o lookup
+    fun general_lookup_bool option default_value name =
+      case lookup name of
+        SOME s => parse_bool_option option name s
+      | NONE => default_value
+    val lookup_bool = the o general_lookup_bool false (SOME false)
+    val lookup_bool_option = general_lookup_bool true NONE
+    fun lookup_time name =
+      the_timeout (case lookup name of
+                     NONE => NONE
+                   | SOME s => parse_time_option name s)
+    fun lookup_int name =
+      case lookup name of
+        NONE => 0
+      | SOME s => case Int.fromString s of
+                    SOME n => n
+                  | NONE => error ("Parameter " ^ quote name ^
+                                   " must be assigned an integer value.")
+    val debug = lookup_bool "debug"
+    val verbose = debug orelse lookup_bool "verbose"
+    val atps = lookup_string "atps" |> space_explode " "
+    val full_types = lookup_bool "full_types"
+    val relevance_threshold =
+      0.01 * Real.fromInt (lookup_int "relevance_threshold")
+    val higher_order = lookup_bool_option "higher_order"
+    val respect_no_atp = lookup_bool "respect_no_atp"
+    val follow_defs = lookup_bool "follow_defs"
+    val isar_proof = lookup_bool "isar_proof"
+    val timeout = lookup_time "timeout"
+    val minimize_timeout = lookup_time "minimize_timeout"
+  in
+    {debug = debug, verbose = verbose, atps = atps, full_types = full_types,
+     relevance_threshold = relevance_threshold, higher_order = higher_order,
+     respect_no_atp = respect_no_atp, follow_defs = follow_defs,
+     isar_proof = isar_proof, timeout = timeout,
+     minimize_timeout = minimize_timeout}
+  end
+
+fun get_params thy = extract_params thy (default_raw_params thy)
+fun default_params thy = get_params thy o map (apsnd single)
+
+fun atp_minimize_command override_params old_style_args fact_refs state =
+  let
+    val thy = Proof.theory_of state
+    val ctxt = Proof.context_of state
+    fun theorems_from_refs ctxt =
+      map (fn fact_ref =>
               let
-                val thmref = Facts.Named ((name, Position.none), interval)
-                val ths = ProofContext.get_fact ctxt thmref
-                val name' = Facts.string_of_ref thmref
+                val ths = ProofContext.get_fact ctxt fact_ref
+                val name' = Facts.string_of_ref fact_ref
               in (name', ths) end)
-    fun get_time_limit_arg time_string =
-      (case Int.fromString time_string of
-        SOME t => t
-      | NONE => error ("Invalid time limit: " ^ quote time_string))
+    fun get_time_limit_arg s =
+      (case Int.fromString s of
+        SOME t => Time.fromSeconds t
+      | NONE => error ("Invalid time limit: " ^ quote s))
     fun get_opt (name, a) (p, t) =
       (case name of
         "time" => (p, get_time_limit_arg a)
       | "atp" => (a, t)
       | n => error ("Invalid argument: " ^ n))
-    fun get_options args =
-      fold get_opt args (default_minimize_prover, default_minimize_time_limit)
-    val (prover_name, time_limit) = get_options args
+    val {atps, minimize_timeout, ...} = get_params thy override_params
+    val (atp, timeout) = fold get_opt old_style_args (hd atps, minimize_timeout)
+    val params =
+      get_params thy
+          [("atps", [atp]),
+           ("minimize_timeout",
+            [string_of_int (Time.toSeconds timeout) ^ " s"])]
     val prover =
-      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
+      (case get_prover thy atp of
         SOME prover => prover
-      | NONE => error ("Unknown prover: " ^ quote prover_name))
-    val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
+      | NONE => error ("Unknown ATP: " ^ quote atp))
+    val name_thms_pairs = theorems_from_refs ctxt fact_refs
   in
-    writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
-                                   state name_thms_pairs))
+    writeln (#2 (minimize_theorems params linear_minimize prover atp state
+                                   name_thms_pairs))
+  end
+
+val runN = "run"
+val minimizeN = "minimize"
+val messagesN = "messages"
+val available_atpsN = "available_atps"
+val running_atpsN = "running_atps"
+val kill_atpsN = "kill_atps"
+val refresh_tptpN = "refresh_tptp"
+val helpN = "help"
+
+val addN = "add"
+val delN = "del"
+val onlyN = "only"
+
+fun hammer_away override_params subcommand opt_i relevance_override state =
+  let
+    val thy = Proof.theory_of state
+    val _ = List.app check_raw_param override_params
+  in
+    if subcommand = runN then
+      sledgehammer (get_params thy override_params) (the_default 1 opt_i)
+                   relevance_override state
+    else if subcommand = minimizeN then
+      atp_minimize_command override_params [] (#add relevance_override) state
+    else if subcommand = messagesN then
+      messages opt_i
+    else if subcommand = available_atpsN then
+      available_atps thy
+    else if subcommand = running_atpsN then
+      running_atps ()
+    else if subcommand = kill_atpsN then
+      kill_atps ()
+    else if subcommand = refresh_tptpN then
+      refresh_systems_on_tptp ()
+    else
+      error ("Unknown subcommand: " ^ quote subcommand ^ ".")
   end
 
-local structure K = OuterKeyword and P = OuterParse in
+fun sledgehammer_trans (((subcommand, params), relevance_override), opt_i) =
+  Toplevel.keep (hammer_away params subcommand opt_i relevance_override
+                 o Toplevel.proof_of)
+
+fun string_for_raw_param (name, value) = name ^ " = " ^ space_implode " " value
+
+fun sledgehammer_params_trans params =
+  Toplevel.theory
+      (fold set_default_raw_param params
+       #> tap (fn thy => 
+                  writeln ("Default parameters for Sledgehammer:\n" ^
+                           (case rev (default_raw_params thy) of
+                              [] => "none"
+                            | params =>
+                              (map check_raw_param params;
+                               params |> map string_for_raw_param
+                                      |> sort_strings |> cat_lines)))))
 
-val parse_args =
-  Scan.optional (Args.bracks (P.list (P.xname --| P.$$$ "=" -- P.xname))) []
-val parse_thm_names = Scan.repeat (P.xname -- Scan.option Attrib.thm_sel)
+val parse_key = Scan.repeat1 P.typ_group >> space_implode " "
+val parse_value = Scan.repeat1 P.xname
+val parse_param = parse_key -- Scan.optional (P.$$$ "=" |-- parse_value) []
+val parse_params = Scan.optional (Args.bracks (P.list parse_param)) []
+val parse_fact_refs =
+  Scan.repeat1 (Scan.unless (P.name -- Args.colon)
+                            (P.xname -- Scan.option Attrib.thm_sel)
+                >> (fn (name, interval) =>
+                       Facts.Named ((name, Position.none), interval)))
+val parse_relevance_chunk =
+  (Args.add |-- Args.colon |-- parse_fact_refs >> add_to_relevance_override)
+  || (Args.del |-- Args.colon |-- parse_fact_refs
+      >> del_from_relevance_override)
+  || (P.$$$ onlyN |-- Args.colon |-- parse_fact_refs >> only_relevance_override)
+val parse_relevance_override =
+  Scan.optional (Args.parens
+      (Scan.optional (parse_fact_refs >> only_relevance_override)
+                     default_relevance_override
+       -- Scan.repeat parse_relevance_chunk)
+       >> op :: >> merge_relevance_overrides)
+      default_relevance_override
+val parse_sledgehammer_command =
+  (Scan.optional P.short_ident runN -- parse_params -- parse_relevance_override
+   -- Scan.option P.nat) #>> sledgehammer_trans
+val parse_sledgehammer_params_command =
+  parse_params #>> sledgehammer_params_trans
+
+val parse_minimize_args =
+  Scan.optional (Args.bracks (P.list (P.short_ident --| P.$$$ "=" -- P.xname)))
+                []
+val _ =
+  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill_atps))
+val _ =
+  OuterSyntax.improper_command "atp_info"
+    "print information about managed provers" K.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative running_atps))
+val _ =
+  OuterSyntax.improper_command "atp_messages"
+    "print recent messages issued by managed provers" K.diag
+    (Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >>
+      (fn limit => Toplevel.no_timing
+                   o Toplevel.imperative (fn () => messages limit)))
+val _ =
+  OuterSyntax.improper_command "print_atps" "print external provers" K.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
+      Toplevel.keep (available_atps o Toplevel.theory_of)))
+val _ =
+  OuterSyntax.improper_command "atp_minimize"
+    "minimize theorem list with external prover" K.diag
+    (parse_minimize_args -- parse_fact_refs >> (fn (args, fact_refs) =>
+      Toplevel.no_timing o Toplevel.unknown_proof o
+        Toplevel.keep (atp_minimize_command [] args fact_refs
+                       o Toplevel.proof_of)))
 
 val _ =
-  OuterSyntax.command "atp_minimize" "minimize theorem list with external prover" K.diag
-    (parse_args -- parse_thm_names >> (fn (args, thm_names) =>
-      Toplevel.no_timing o Toplevel.unknown_proof o
-        Toplevel.keep (atp_minimize_command args thm_names o Toplevel.proof_of)))
-
-end
+  OuterSyntax.improper_command "sledgehammer"
+    "search for first-order proof using automatic theorem provers" K.diag
+    parse_sledgehammer_command
+val _ =
+  OuterSyntax.command "sledgehammer_params"
+    "set and display the default parameters for Sledgehammer" K.thy_decl
+    parse_sledgehammer_params_command
 
 end;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Wed Mar 24 22:30:33 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -339,18 +339,18 @@
   let
     val _ = trace_proof_msg (K "\n\nisar_proof_body: start\n")
     val string_of_term = PrintMode.setmp [] (Syntax.string_of_term ctxt)
-    fun have_or_show "show" _ = "show \""
-      | have_or_show have lname = have ^ " " ^ lname ^ ": \""
+    fun have_or_show "show" _ = "  show \""
+      | have_or_show have lname = "  " ^ have ^ " " ^ lname ^ ": \""
     fun do_line _ (lname, t, []) =
        (* No deps: it's a conjecture clause, with no proof. *)
        (case permuted_clause t ctms of
-          SOME u => "assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
+          SOME u => "  assume " ^ lname ^ ": \"" ^ string_of_term u ^ "\"\n"
         | NONE => raise TERM ("Sledgehammer_Proof_Reconstruct.isar_proof_body",
                               [t]))
       | do_line have (lname, t, deps) =
         have_or_show have lname ^
         string_of_term (gen_all_vars (HOLogic.mk_Trueprop t)) ^
-        "\"\n  by (metis " ^ space_implode " " deps ^ ")\n"
+        "\"\n    by (metis " ^ space_implode " " deps ^ ")\n"
     fun do_lines [(lname, t, deps)] = [do_line "show" (lname, t, deps)]
       | do_lines ((lname, t, deps) :: lines) =
         do_line "have" (lname, t, deps) :: do_lines lines
@@ -535,18 +535,20 @@
 val kill_chained = filter_out (curry (op =) chained_hint)
 
 (* metis-command *)
-fun metis_line [] = "apply metis"
-  | metis_line xs = "apply (metis " ^ space_implode " " xs ^ ")"
+fun metis_line [] = "by metis"
+  | metis_line xs = "by (metis " ^ space_implode " " xs ^ ")"
 
-(* atp_minimize [atp=<prover>] <lemmas> *)
 fun minimize_line _ [] = ""
-  | minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
-        Markup.markup Markup.sendback ("atp_minimize [atp = " ^ name ^ "] " ^
-                                       space_implode " " (kill_chained lemmas))
+  | minimize_line name lemmas =
+      "To minimize the number of lemmas, try this command:\n" ^
+      Markup.markup Markup.sendback
+                    ("sledgehammer minimize [atps = " ^ name ^ "] (" ^
+                     space_implode " " (kill_chained lemmas) ^ ")") ^ "."
 
 fun metis_lemma_list dfg name result =
   let val (lemmas, used_conj) = extract_lemmas (get_step_nums dfg) result in
-    (Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ "\n" ^
+    ("Try this command: " ^
+     Markup.markup Markup.sendback (metis_line (kill_chained lemmas)) ^ ".\n" ^
      minimize_line name lemmas ^
      (if used_conj then
         ""
@@ -570,8 +572,11 @@
       if member (op =) tokens chained_hint then ""
       else isar_proof_from_tstp_file cnfs ctxt goal subgoalno thm_names
   in
-    (one_line_proof ^ "\n\n" ^ Markup.markup Markup.sendback isar_proof,
-     lemma_names)
+    (* Hack: The " \n" shouldn't be part of the markup. This is a workaround
+       for a strange ProofGeneral bug, whereby the first two letters of the word
+       "proof" are not highlighted. *)
+    (one_line_proof ^ "\n\nStructured proof:" ^
+     Markup.markup Markup.sendback (" \n" ^ isar_proof), lemma_names)
   end
 
 end;
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Mar 25 17:56:31 2010 +0100
@@ -0,0 +1,53 @@
+(*  Title:      HOL/Sledgehammer/sledgehammer_util.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+
+General-purpose functions used by the Sledgehammer modules.
+*)
+
+signature SLEDGEHAMMER_UTIL =
+sig
+  val serial_commas : string -> string list -> string list
+  val parse_bool_option : bool -> string -> string -> bool option
+  val parse_time_option : string -> string -> Time.time option
+end;
+
+structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
+struct
+
+fun serial_commas _ [] = ["??"]
+  | serial_commas _ [s] = [s]
+  | serial_commas conj [s1, s2] = [s1, conj, s2]
+  | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
+  | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
+
+fun parse_bool_option option name s =
+  (case s of
+     "smart" => if option then NONE else raise Option
+   | "false" => SOME false
+   | "true" => SOME true
+   | "" => SOME true
+   | _ => raise Option)
+  handle Option.Option =>
+         let val ss = map quote ((option ? cons "smart") ["true", "false"]) in
+           error ("Parameter " ^ quote name ^ " must be assigned " ^
+                  space_implode " " (serial_commas "or" ss) ^ ".")
+         end
+
+fun parse_time_option _ "none" = NONE
+  | parse_time_option name s =
+    let
+      val msecs =
+        case space_explode " " s of
+          [s1, "min"] => 60000 * the (Int.fromString s1)
+        | [s1, "s"] => 1000 * the (Int.fromString s1)
+        | [s1, "ms"] => the (Int.fromString s1)
+        | _ => 0
+    in
+      if msecs <= 0 then
+        error ("Parameter " ^ quote name ^ " must be assigned a positive time \
+               \value (e.g., \"60 s\", \"200 ms\") or \"none\".")
+      else
+        SOME (Time.fromMilliseconds msecs)
+    end
+
+end;