move the Sledgehammer Isar commands together into one file;
this will make easier to add options and reorganize them later

--- a/src/HOL/IsaMakefile	Fri Mar 19 13:02:18 2010 +0100
+++ b/src/HOL/IsaMakefile	Fri Mar 19 15:07:44 2010 +0100
@@ -320,6 +320,7 @@
   Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML \
   Tools/Sledgehammer/sledgehammer_fol_clause.ML \
   Tools/Sledgehammer/sledgehammer_hol_clause.ML \
+  Tools/Sledgehammer/sledgehammer_isar.ML \
   Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML \
   Tools/string_code.ML \
   Tools/string_syntax.ML \

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 19 13:02:18 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 19 15:07:44 2010 +0100
@@ -42,8 +42,7 @@
 
 datatype min_data = MinData of {
   succs: int,
-  ab_ratios: int,
-  it_ratios: int
+  ab_ratios: int
   }
 
 fun make_sh_data
@@ -51,8 +50,8 @@
   ShData{calls=calls, success=success, lemmas=lemmas, max_lems=max_lems,
          time_isa=time_isa, time_atp=time_atp, time_atp_fail=time_atp_fail}
 
-fun make_min_data (succs, ab_ratios, it_ratios) =
-  MinData{succs=succs, ab_ratios=ab_ratios, it_ratios=it_ratios}
+fun make_min_data (succs, ab_ratios) =
+  MinData{succs=succs, ab_ratios=ab_ratios}
 
 fun make_me_data (calls,success,proofs,time,timeout,lemmas,posns) =
   MeData{calls=calls, success=success, proofs=proofs, time=time,
@@ -66,8 +65,7 @@
   time_atp, time_atp_fail}) = (calls, success, lemmas, max_lems, time_isa,
   time_atp, time_atp_fail)
 
-fun tuple_of_min_data (MinData {succs, ab_ratios, it_ratios}) =
-  (succs, ab_ratios, it_ratios)
+fun tuple_of_min_data (MinData {succs, ab_ratios}) = (succs, ab_ratios)
 
 fun tuple_of_me_data (MeData {calls, success, proofs, time, timeout, lemmas,
   posns}) = (calls, success, proofs, time, timeout, lemmas, posns)
@@ -147,13 +145,10 @@
     => (calls,success,lemmas,max_lems,time_isa,time_atp,time_atp_fail + t))
 
 val inc_min_succs = map_min_data
-  (fn (succs,ab_ratios,it_ratios) => (succs+1, ab_ratios, it_ratios))
+  (fn (succs,ab_ratios) => (succs+1, ab_ratios))
 
 fun inc_min_ab_ratios r = map_min_data
-  (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios+r, it_ratios))
-
-fun inc_min_it_ratios r = map_min_data
-  (fn (succs, ab_ratios, it_ratios) => (succs, ab_ratios, it_ratios+r))
+  (fn (succs, ab_ratios) => (succs, ab_ratios+r))
 
 val inc_metis_calls = map_me_data
   (fn (calls,success,proofs,time,timeout,lemmas,posns)
@@ -234,10 +229,9 @@
   else ()
  )
 
-fun log_min_data log (succs, ab_ratios, it_ratios) =
+fun log_min_data log (succs, ab_ratios) =
   (log ("Number of successful minimizations: " ^ string_of_int succs);
-   log ("After/before ratios: " ^ string_of_int ab_ratios);
-   log ("Iterations ratios: " ^ string_of_int it_ratios)
+   log ("After/before ratios: " ^ string_of_int ab_ratios)
   )
 
 in
@@ -380,9 +374,10 @@
 
 fun run_minimize args named_thms id ({pre=st, log, ...}: Mirabelle.run_args) =
   let
+    open ATP_Minimal
     val n0 = length (these (!named_thms))
     val (prover_name, prover) = get_atp (Proof.theory_of st) args
-    val minimize = ATP_Minimal.minimalize prover prover_name
+    val minimize = minimize_theorems linear_minimize prover prover_name
     val timeout =
       AList.lookup (op =) args minimize_timeoutK
       |> Option.map (fst o read_int o explode)
@@ -393,7 +388,6 @@
       (SOME (named_thms',its), msg) =>
         (change_data id inc_min_succs;
          change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
-         change_data id (inc_min_it_ratios ((100*its) div n0));
          if length named_thms' = n0
          then log (minimize_tag id ^ "already minimal")
          else (named_thms := SOME named_thms';

--- a/src/HOL/Sledgehammer.thy	Fri Mar 19 13:02:18 2010 +0100
+++ b/src/HOL/Sledgehammer.thy	Fri Mar 19 15:07:44 2010 +0100
@@ -20,6 +20,7 @@
   ("Tools/ATP_Manager/atp_manager.ML")
   ("Tools/ATP_Manager/atp_wrapper.ML")
   ("Tools/ATP_Manager/atp_minimal.ML")
+  ("Tools/Sledgehammer/sledgehammer_isar.ML")
   ("Tools/Sledgehammer/meson_tactic.ML")
   ("Tools/Sledgehammer/metis_tactics.ML")
 begin
@@ -90,6 +91,7 @@
 apply (simp add: COMBC_def) 
 done
 
+
 subsection {* Setup of external ATPs *}
 
 use "Tools/Sledgehammer/sledgehammer_fol_clause.ML"
@@ -122,6 +124,8 @@
 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_spass *}
 setup {* ATP_Manager.add_prover ATP_Wrapper.remote_eprover *}
 
+use "Tools/Sledgehammer/sledgehammer_isar.ML"
+
 
 subsection {* The MESON prover *}
 

--- a/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 19 13:02:18 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML	Fri Mar 19 15:07:44 2010 +0100
@@ -282,36 +282,4 @@
     val _ = List.app (fn name => start_prover name birth_time death_time 1 proof_state) provers;
   in () end;
 
-
-
-(** Isar command syntax **)
-
-local structure K = OuterKeyword and P = OuterParse in
-
-val _ =
-  OuterSyntax.improper_command "atp_kill" "kill all managed provers" K.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
-
-val _ =
-  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
-    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
-
-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 (print_provers o Toplevel.theory_of)));
-
-val _ =
-  OuterSyntax.command "sledgehammer" "call all 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)));
-
 end;
-
-end;
-

--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Fri Mar 19 13:02:18 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML	Fri Mar 19 15:07:44 2010 +0100
@@ -6,27 +6,31 @@
 
 signature ATP_MINIMAL =
 sig
-  val minimize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
-    (string * thm list) list -> ((string * thm list) list * int) option * string
-  (* To be removed once TN has finished his measurements;
-     the int component of the result should then be removed: *)
-  val minimalize: ATP_Wrapper.prover -> string -> int -> Proof.state ->
-    (string * thm list) list -> ((string * thm list) list * int) option * string
-end
+  type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
+  val linear_minimize : 'a minimize_fun
+  val binary_minimize : 'a minimize_fun
+  val minimize_theorems :
+    (string * thm list) minimize_fun -> ATP_Wrapper.prover -> string -> int
+    -> Proof.state -> (string * thm list) list
+    -> (string * thm list) list option * string
+end;
 
 structure ATP_Minimal : ATP_MINIMAL =
 struct
 
-(* Linear minimization *)
+open Sledgehammer_Fact_Preprocessor
+
+type 'a minimize_fun = ('a list -> bool) -> 'a list -> 'a list
+
+(* Linear minimization algorithm *)
 
-fun lin_gen_minimize p s =
-let
-  fun min [] needed = needed
-    | min (x::xs) needed =
-        if p(xs @ needed) then min xs needed else min xs (x::needed)
-in (min s [], length s) end;
+fun linear_minimize p s =
+  let
+    fun aux [] needed = needed
+      | aux (x :: xs) needed = aux xs (needed |> not (p (xs @ needed)) ? cons x)
+  in aux s [] end;
 
-(* Clever minimalization algorithm *)
+(* Binary minimalization *)
 
 local
   fun isplit (l, r) [] = (l, r)
@@ -37,24 +41,21 @@
 end
 
 local
-  fun min p sup [] = raise Empty
-    | min p sup [s0] = [s0]
+  fun min _ _ [] = raise Empty
+    | min _ _ [s0] = [s0]
     | min p sup s =
       let
         val (l0, r0) = split s
       in
-        if p (sup @ l0)
-        then min p sup l0
+        if p (sup @ l0) then
+          min p sup l0
+        else if p (sup @ r0) then
+          min p sup r0
         else
-          if p (sup @ r0)
-          then min p sup r0
-          else
-            let
-              val l = min p (sup @ r0) l0
-              val r = min p (sup @ l) r0
-            in
-              l @ r
-            end
+          let
+            val l = min p (sup @ r0) l0
+            val r = min p (sup @ l) r0
+          in l @ r end
       end
 in
   (* return a minimal subset v of s that satisfies p
@@ -62,15 +63,10 @@
    @post v subset s & p(v) &
          forall e in v. ~p(v \ e)
    *)
-  fun minimal p s =
-    let
-      val count = Unsynchronized.ref 0
-      fun p_count xs = (Unsynchronized.inc count; p xs)
-      val v =
-        (case min p_count [] s of
-          [x] => if p_count [] then [] else [x]
-        | m => m);
-    in (v, ! count) end
+  fun binary_minimize p s =
+    case min p [] s of
+      [x] => if p [] then [] else [x]
+    | m => m
 end
 
 
@@ -91,7 +87,7 @@
    ("# Cannot determine problem status within resource limit", Timeout),
    ("Error", Error)]
 
-fun produce_answer (result: ATP_Wrapper.prover_result) =
+fun produce_answer (result : ATP_Wrapper.prover_result) =
   let
     val {success, proof = result_string, internal_thm_names = thm_name_vec,
       filtered_clauses = filtered, ...} = result
@@ -116,7 +112,7 @@
   let
     val _ = priority ("Testing " ^ string_of_int (length name_thms_pairs) ^ " theorems... ")
     val name_thm_pairs = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
-    val axclauses = Sledgehammer_Fact_Preprocessor.cnf_rules_pairs (Proof.theory_of state) name_thm_pairs
+    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,
@@ -133,7 +129,8 @@
 
 (* minimalization of thms *)
 
-fun gen_minimalize gen_min prover prover_name time_limit state name_thms_pairs =
+fun minimize_theorems gen_min prover prover_name time_limit state
+                      name_thms_pairs =
   let
     val _ =
       priority ("Minimize called with " ^ string_of_int (length name_thms_pairs) ^
@@ -152,15 +149,14 @@
             if length ordered_used < length name_thms_pairs then
               filter (fn (name1, _) => List.exists (equal name1) ordered_used) name_thms_pairs
             else name_thms_pairs
-          val (min_thms, n) =
-            if null to_use then ([], 0)
+          val min_thms =
+            if null to_use then []
             else gen_min (test_thms (SOME filtered)) to_use
           val min_names = sort_distinct string_ord (map fst min_thms)
           val _ = priority (cat_lines
-            ["Iterations: " ^ string_of_int n (* FIXME TN remove later *),
-             "Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
+            ["Minimal " ^ string_of_int (length min_thms) ^ " theorems"])
         in
-          (SOME (min_thms, n), "Try this command: " ^
+          (SOME min_thms, "Try this command: " ^
             Markup.markup Markup.sendback ("apply (metis " ^ space_implode " " min_names ^ ")"))
         end
     | (Timeout, _) =>
@@ -171,67 +167,8 @@
     | (Failure, _) =>
         (NONE, "Failure: No proof with the theorems supplied"))
     handle Sledgehammer_HOL_Clause.TRIVIAL =>
-        (SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+        (SOME [], "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
       | ERROR msg => (NONE, "Error: " ^ msg)
   end
 
-
-(* Isar command and parsing input *)
-
-local structure K = OuterKeyword and P = OuterParse and T = OuterLex in
-
-fun get_thms context =
-  map (fn (name, interval) =>
-    let
-      val thmref = Facts.Named ((name, Position.none), interval)
-      val ths = ProofContext.get_fact context thmref
-      val name' = Facts.string_of_ref thmref
-    in
-      (name', ths)
-    end)
-
-val default_prover = "remote_vampire"
-val default_time_limit = 5
-
-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_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_prover, default_time_limit)
-
-val minimize = gen_minimalize lin_gen_minimize
-
-val minimalize = gen_minimalize minimal
-
-fun sh_min_command args thm_names state =
-  let
-    val (prover_name, time_limit) = get_options args
-    val prover =
-      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
-        SOME prover => prover
-      | NONE => error ("Unknown prover: " ^ quote prover_name))
-    val name_thms_pairs = get_thms (Proof.context_of state) thm_names
-  in
-    writeln (#2 (minimize prover prover_name time_limit state name_thms_pairs))
-  end
-
-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 _ =
-  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 (sh_min_command args thm_names o Toplevel.proof_of)))
-
-end
-
-end
+end;

--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Mar 19 13:02:18 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML	Fri Mar 19 15:07:44 2010 +0100
@@ -13,7 +13,7 @@
   val auto: bool Unsynchronized.ref
   val default_params : theory -> (string * string) list -> params
   val setup : theory -> theory
-end
+end;
 
 structure Nitpick_Isar : NITPICK_ISAR =
 struct

--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 19 13:02:18 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 19 15:07:44 2010 +0100
@@ -12,7 +12,7 @@
     hol_context -> (typ option * bool option) list
     -> (typ option * bool option) list -> term
     -> term list * term list * bool * bool * bool
-end
+end;
 
 structure Nitpick_Preproc : NITPICK_PREPROC =
 struct

--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Mar 19 13:02:18 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Fri Mar 19 15:07:44 2010 +0100
@@ -8,7 +8,7 @@
 signature NITPICK_TESTS =
 sig
   val run_all_tests : unit -> unit
-end
+end;
 
 structure Nitpick_Tests =
 struct

--- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Mar 19 13:02:18 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Fri Mar 19 15:07:44 2010 +0100
@@ -62,7 +62,7 @@
   val pstrs : string -> Pretty.T list
   val unyxml : string -> string
   val maybe_quote : string -> string
-end
+end;
 
 structure Nitpick_Util : NITPICK_UTIL =
 struct

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Mar 19 15:07:44 2010 +0100
@@ -0,0 +1,87 @@
+(*  Title:      HOL/Sledgehammer/sledgehammer_isar.ML
+    Author:     Jasmin Blanchette, TU Muenchen
+
+Adds "sledgehammer" and related commands to Isabelle/Isar's outer syntax.
+*)
+
+structure Sledgehammer_Isar : sig end =
+struct
+
+open ATP_Manager
+open ATP_Minimal
+
+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));
+
+val _ =
+  OuterSyntax.improper_command "atp_info" "print information about managed provers" K.diag
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative info));
+
+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 (print_provers o Toplevel.theory_of)));
+
+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 default_minimize_prover = "remote_vampire"
+val default_minimize_time_limit = 5
+
+fun atp_minimize_command args thm_names state =
+  let
+    fun theorems_from_names ctxt =
+      map (fn (name, interval) =>
+              let
+                val thmref = Facts.Named ((name, Position.none), interval)
+                val ths = ProofContext.get_fact ctxt thmref
+                val name' = Facts.string_of_ref thmref
+              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_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 prover =
+      (case ATP_Manager.get_prover (Proof.theory_of state) prover_name of
+        SOME prover => prover
+      | NONE => error ("Unknown prover: " ^ quote prover_name))
+    val name_thms_pairs = theorems_from_names (Proof.context_of state) thm_names
+  in
+    writeln (#2 (minimize_theorems linear_minimize prover prover_name time_limit
+                                   state name_thms_pairs))
+  end
+
+local structure K = OuterKeyword and P = OuterParse in
+
+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 _ =
+  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
+
+end;