merged 'reconstructors' and 'proof methods'
authorblanchet
Mon, 03 Feb 2014 15:19:07 +0100
changeset 55285 e88ad20035f4
parent 55284 bd27ac6ad1c3
child 55286 7bbbd9393ce0
merged 'reconstructors' and 'proof methods'
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
src/HOL/Tools/ATP/atp_proof_reconstruct.ML
src/HOL/Tools/Metis/metis_tactic.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -19,7 +19,7 @@
                            (*refers to minimization attempted by Mirabelle*)
 val minimize_timeoutK = "minimize_timeout" (*=TIME: timeout for each minimization step (seconds of*)
 
-val reconstructorK = "reconstructor" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
+val proof_methodK = "proof_method" (*=NAME: how to reconstruct proofs (ie. using metis/smt)*)
 val metis_ftK = "metis_ft" (*: apply metis with fully-typed encoding to the theorems found by sledgehammer*)
 
 val max_factsK = "max_facts" (*=NUM: max. relevant clauses to use*)
@@ -43,8 +43,7 @@
 
 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
-fun reconstructor_tag reconstructor id =
-  "#" ^ string_of_int id ^ " " ^ (!reconstructor) ^ " (sledgehammer): "
+fun proof_method_tag meth id = "#" ^ string_of_int id ^ " " ^ (!meth) ^ " (sledgehammer): "
 
 val separator = "-----"
 
@@ -130,16 +129,16 @@
   proofs, time, timeout, lemmas, posns}) = (calls, success, nontriv_calls,
   nontriv_success, proofs, time, timeout, lemmas, posns)
 
-datatype reconstructor_mode =
+datatype proof_method_mode =
   Unminimized | Minimized | UnminimizedFT | MinimizedFT
 
 datatype data = Data of {
   sh: sh_data,
   min: min_data,
-  re_u: re_data, (* reconstructor with unminimized set of lemmas *)
-  re_m: re_data, (* reconstructor with minimized set of lemmas *)
-  re_uft: re_data, (* reconstructor with unminimized set of lemmas and fully-typed *)
-  re_mft: re_data, (* reconstructor with minimized set of lemmas and fully-typed *)
+  re_u: re_data, (* proof method with unminimized set of lemmas *)
+  re_m: re_data, (* proof method with minimized set of lemmas *)
+  re_uft: re_data, (* proof method with unminimized set of lemmas and fully-typed *)
+  re_mft: re_data, (* proof method with minimized set of lemmas and fully-typed *)
   mini: bool   (* with minimization *)
   }
 
@@ -218,39 +217,39 @@
 fun inc_min_ab_ratios r = map_min_data
   (fn (succs, ab_ratios) => (succs, ab_ratios+r))
 
-val inc_reconstructor_calls = map_re_data
+val inc_proof_method_calls = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls + 1, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
 
-val inc_reconstructor_success = map_re_data
+val inc_proof_method_success = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success + 1, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas,posns))
 
-val inc_reconstructor_nontriv_calls = map_re_data
+val inc_proof_method_nontriv_calls = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls + 1, nontriv_success, proofs, time, timeout, lemmas,posns))
 
-val inc_reconstructor_nontriv_success = map_re_data
+val inc_proof_method_nontriv_success = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success + 1, proofs, time, timeout, lemmas,posns))
 
-val inc_reconstructor_proofs = map_re_data
+val inc_proof_method_proofs = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success, proofs + 1, time, timeout, lemmas,posns))
 
-fun inc_reconstructor_time m t = map_re_data
+fun inc_proof_method_time m t = map_re_data
  (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
   => (calls, success, nontriv_calls, nontriv_success, proofs, time + t, timeout, lemmas,posns)) m
 
-val inc_reconstructor_timeout = map_re_data
+val inc_proof_method_timeout = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout + 1, lemmas,posns))
 
-fun inc_reconstructor_lemmas m n = map_re_data
+fun inc_proof_method_lemmas m n = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, inc_max n lemmas, posns)) m
 
-fun inc_reconstructor_posns m pos = map_re_data
+fun inc_proof_method_posns m pos = map_re_data
   (fn (calls,success,nontriv_calls, nontriv_success, proofs,time,timeout,lemmas,posns)
     => (calls, success, nontriv_calls, nontriv_success, proofs, time, timeout, lemmas, pos::posns)) m
 
@@ -292,19 +291,19 @@
 fun log_re_data log tag sh_calls (re_calls, re_success, re_nontriv_calls,
      re_nontriv_success, re_proofs, re_time, re_timeout,
     (lemmas, lems_sos, lems_max), re_posns) =
- (log ("Total number of " ^ tag ^ "reconstructor calls: " ^ str re_calls);
-  log ("Number of successful " ^ tag ^ "reconstructor calls: " ^ str re_success ^
+ (log ("Total number of " ^ tag ^ "proof method calls: " ^ str re_calls);
+  log ("Number of successful " ^ tag ^ "proof method calls: " ^ str re_success ^
     " (proof: " ^ str re_proofs ^ ")");
-  log ("Number of " ^ tag ^ "reconstructor timeouts: " ^ str re_timeout);
+  log ("Number of " ^ tag ^ "proof method timeouts: " ^ str re_timeout);
   log ("Success rate: " ^ percentage re_success sh_calls ^ "%");
-  log ("Total number of nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_calls);
-  log ("Number of successful nontrivial " ^ tag ^ "reconstructor calls: " ^ str re_nontriv_success ^
+  log ("Total number of nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_calls);
+  log ("Number of successful nontrivial " ^ tag ^ "proof method calls: " ^ str re_nontriv_success ^
     " (proof: " ^ str re_proofs ^ ")");
-  log ("Number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lemmas);
-  log ("SOS of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_sos);
-  log ("Max number of successful " ^ tag ^ "reconstructor lemmas: " ^ str lems_max);
-  log ("Total time for successful " ^ tag ^ "reconstructor calls: " ^ str3 (time re_time));
-  log ("Average time for successful " ^ tag ^ "reconstructor calls: " ^
+  log ("Number of successful " ^ tag ^ "proof method lemmas: " ^ str lemmas);
+  log ("SOS of successful " ^ tag ^ "proof method lemmas: " ^ str lems_sos);
+  log ("Max number of successful " ^ tag ^ "proof method lemmas: " ^ str lems_max);
+  log ("Total time for successful " ^ tag ^ "proof method calls: " ^ str3 (time re_time));
+  log ("Average time for successful " ^ tag ^ "proof method calls: " ^
     str3 (avg_time re_time re_success));
   if tag=""
   then log ("Proved: " ^ space_implode " " (map str_of_pos re_posns))
@@ -325,7 +324,7 @@
     fun app_if (ReData {calls, ...}) f = if calls > 0 then f () else ()
     fun log_re tag m =
       log_re_data log tag sh_calls (tuple_of_re_data m)
-    fun log_reconstructor (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
+    fun log_proof_method (tag1, m1) (tag2, m2) = app_if m1 (fn () =>
       (log_re tag1 m1; log ""; app_if m2 (fn () => log_re tag2 m2)))
   in
     if sh_calls > 0
@@ -334,14 +333,14 @@
       log_sh_data log (tuple_of_sh_data sh);
       log "";
       if not mini
-      then log_reconstructor ("", re_u) ("fully-typed ", re_uft)
+      then log_proof_method ("", re_u) ("fully-typed ", re_uft)
       else
         app_if re_u (fn () =>
-         (log_reconstructor ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
+         (log_proof_method ("unminimized ", re_u) ("unminimized fully-typed ", re_uft);
           log "";
           app_if re_m (fn () =>
             (log_min_data log (tuple_of_min_data min); log "";
-             log_reconstructor ("", re_m) ("fully-typed ", re_mft))))))
+             log_proof_method ("", re_m) ("fully-typed ", re_mft))))))
     else ()
   end
 
@@ -385,8 +384,8 @@
   andalso not (String.isSubstring "may fail" s)
 
 (* Fragile hack *)
-fun reconstructor_from_msg args msg =
-  (case AList.lookup (op =) args reconstructorK of
+fun proof_method_from_msg args msg =
+  (case AList.lookup (op =) args proof_methodK of
     SOME name => name
   | NONE =>
     if exists good_line (split_lines msg) then
@@ -460,7 +459,7 @@
     fun failed failure =
       ({outcome = SOME failure, used_facts = [], used_from = [],
         run_time = Time.zeroTime,
-        preplay = Lazy.value (Sledgehammer_Prover.plain_metis,
+        preplay = Lazy.value (Sledgehammer_Reconstructor.Metis_Method (NONE, NONE),
           Sledgehammer_Reconstructor.Play_Failed),
         message = K "", message_tail = ""}, ~1)
     val ({outcome, used_facts, run_time, preplay, message, message_tail, ...}
@@ -501,7 +500,7 @@
 
 in
 
-fun run_sledgehammer trivial args reconstructor named_thms id
+fun run_sledgehammer trivial args proof_method named_thms id
       ({pre=st, log, pos, ...}: Mirabelle.run_args) =
   let
     val thy = Proof.theory_of st
@@ -557,7 +556,7 @@
           change_data id (inc_sh_max_lems (length names));
           change_data id (inc_sh_time_isa time_isa);
           change_data id (inc_sh_time_prover time_prover);
-          reconstructor := reconstructor_from_msg args msg;
+          proof_method := proof_method_from_msg args msg;
           named_thms := SOME (map_filter get_thms names);
           log (sh_tag id ^ triv_str ^ "succeeded (" ^ string_of_int time_isa ^ "+" ^
             string_of_int time_prover ^ ") [" ^ prover_name ^ "]:\n" ^ msg)
@@ -572,7 +571,7 @@
 
 end
 
-fun run_minimize args reconstructor named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
+fun run_minimize args meth named_thms id ({pre = st, log, ...} : Mirabelle.run_args) =
   let
     val thy = Proof.theory_of st
     val {goal, ...} = Proof.goal st
@@ -614,7 +613,7 @@
          change_data id (inc_min_ab_ratios ((100 * length named_thms') div n0));
          if length named_thms' = n0
          then log (minimize_tag id ^ "already minimal")
-         else (reconstructor := reconstructor_from_msg args msg;
+         else (meth := proof_method_from_msg args msg;
                named_thms := SOME named_thms';
                log (minimize_tag id ^ "succeeded:\n" ^ msg))
         )
@@ -629,10 +628,10 @@
    ("slice", "false"),
    ("timeout", timeout |> Time.toSeconds |> string_of_int)]
 
-fun run_reconstructor trivial full m name reconstructor named_thms id
+fun run_proof_method trivial full m name meth named_thms id
     ({pre=st, timeout, log, pos, ...}: Mirabelle.run_args) =
   let
-    fun do_reconstructor named_thms ctxt =
+    fun do_method named_thms ctxt =
       let
         val ref_of_str =
           suffix ";" #> Outer_Syntax.scan Position.none #> Parse_Spec.xthm
@@ -646,56 +645,56 @@
           Sledgehammer_Tactics.sledgehammer_as_oracle_tac ctxt
             (override_params prover type_enc (my_timeout time_slice)) fact_override
       in
-        if !reconstructor = "sledgehammer_tac" then
+        if !meth = "sledgehammer_tac" then
           sledge_tac 0.2 ATP_Systems.vampireN "mono_native"
           ORELSE' sledge_tac 0.2 ATP_Systems.eN "poly_guards??"
           ORELSE' sledge_tac 0.2 ATP_Systems.spassN "mono_native"
           ORELSE' sledge_tac 0.2 ATP_Systems.z3_tptpN "poly_tags??"
           ORELSE' SMT_Solver.smt_tac ctxt thms
-        else if !reconstructor = "smt" then
+        else if !meth = "smt" then
           SMT_Solver.smt_tac ctxt thms
         else if full then
           Metis_Tactic.metis_tac [ATP_Proof_Reconstruct.full_typesN]
             ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
-        else if String.isPrefix "metis (" (!reconstructor) then
+        else if String.isPrefix "metis (" (!meth) then
           let
             val (type_encs, lam_trans) =
-              !reconstructor
+              !meth
               |> Outer_Syntax.scan Position.start
               |> filter Token.is_proper |> tl
               |> Metis_Tactic.parse_metis_options |> fst
               |>> the_default [ATP_Proof_Reconstruct.partial_typesN]
               ||> the_default ATP_Proof_Reconstruct.default_metis_lam_trans
           in Metis_Tactic.metis_tac type_encs lam_trans ctxt thms end
-        else if !reconstructor = "metis" then
+        else if !meth = "metis" then
           Metis_Tactic.metis_tac [] ATP_Proof_Reconstruct.default_metis_lam_trans ctxt thms
         else
           K all_tac
       end
-    fun apply_reconstructor named_thms =
-      Mirabelle.can_apply timeout (do_reconstructor named_thms) st
+    fun apply_method named_thms =
+      Mirabelle.can_apply timeout (do_method named_thms) st
 
     fun with_time (false, t) = "failed (" ^ string_of_int t ^ ")"
-      | with_time (true, t) = (change_data id (inc_reconstructor_success m);
+      | with_time (true, t) = (change_data id (inc_proof_method_success m);
           if trivial then ()
-          else change_data id (inc_reconstructor_nontriv_success m);
-          change_data id (inc_reconstructor_lemmas m (length named_thms));
-          change_data id (inc_reconstructor_time m t);
-          change_data id (inc_reconstructor_posns m (pos, trivial));
-          if name = "proof" then change_data id (inc_reconstructor_proofs m) else ();
+          else change_data id (inc_proof_method_nontriv_success m);
+          change_data id (inc_proof_method_lemmas m (length named_thms));
+          change_data id (inc_proof_method_time m t);
+          change_data id (inc_proof_method_posns m (pos, trivial));
+          if name = "proof" then change_data id (inc_proof_method_proofs m) else ();
           "succeeded (" ^ string_of_int t ^ ")")
-    fun timed_reconstructor named_thms =
-      (with_time (Mirabelle.cpu_time apply_reconstructor named_thms), true)
-      handle TimeLimit.TimeOut => (change_data id (inc_reconstructor_timeout m); ("timeout", false))
+    fun timed_method named_thms =
+      (with_time (Mirabelle.cpu_time apply_method named_thms), true)
+      handle TimeLimit.TimeOut => (change_data id (inc_proof_method_timeout m); ("timeout", false))
            | ERROR msg => ("error: " ^ msg, false)
 
     val _ = log separator
-    val _ = change_data id (inc_reconstructor_calls m)
-    val _ = if trivial then () else change_data id (inc_reconstructor_nontriv_calls m)
+    val _ = change_data id (inc_proof_method_calls m)
+    val _ = if trivial then () else change_data id (inc_proof_method_nontriv_calls m)
   in
     named_thms
-    |> timed_reconstructor
-    |>> log o prefix (reconstructor_tag reconstructor id)
+    |> timed_method
+    |>> log o prefix (proof_method_tag meth id)
     |> snd
   end
 
@@ -717,7 +716,7 @@
       if !num_sledgehammer_calls > max_calls then ()
       else
         let
-          val reconstructor = Unsynchronized.ref ""
+          val meth = Unsynchronized.ref ""
           val named_thms =
             Unsynchronized.ref (NONE : ((string * stature) * thm list) list option)
           val minimize = AList.defined (op =) args minimizeK
@@ -728,33 +727,28 @@
               Try0.try0 (SOME try_timeout) ([], [], [], []) pre
               handle TimeLimit.TimeOut => false
             else false
-          fun apply_reconstructor m1 m2 =
+          fun apply_method m1 m2 =
             if metis_ft
             then
-              if not (Mirabelle.catch_result (reconstructor_tag reconstructor) false
-                  (run_reconstructor trivial false m1 name reconstructor
-                       (these (!named_thms))) id st)
+              if not (Mirabelle.catch_result (proof_method_tag meth) false
+                  (run_proof_method trivial false m1 name meth (these (!named_thms))) id st)
               then
-                (Mirabelle.catch_result (reconstructor_tag reconstructor) false
-                  (run_reconstructor trivial true m2 name reconstructor
-                       (these (!named_thms))) id st; ())
+                (Mirabelle.catch_result (proof_method_tag meth) false
+                  (run_proof_method trivial true m2 name meth (these (!named_thms))) id st; ())
               else ()
             else
-              (Mirabelle.catch_result (reconstructor_tag reconstructor) false
-                (run_reconstructor trivial false m1 name reconstructor
-                     (these (!named_thms))) id st; ())
+              (Mirabelle.catch_result (proof_method_tag meth) false
+                (run_proof_method trivial false m1 name meth (these (!named_thms))) id st; ())
         in
           change_data id (set_mini minimize);
-          Mirabelle.catch sh_tag (run_sledgehammer trivial args reconstructor
-                                                   named_thms) id st;
+          Mirabelle.catch sh_tag (run_sledgehammer trivial args meth named_thms) id st;
           if is_some (!named_thms)
           then
-           (apply_reconstructor Unminimized UnminimizedFT;
+           (apply_method Unminimized UnminimizedFT;
             if minimize andalso not (null (these (!named_thms)))
             then
-             (Mirabelle.catch minimize_tag
-                  (run_minimize args reconstructor named_thms) id st;
-              apply_reconstructor Minimized MinimizedFT)
+             (Mirabelle.catch minimize_tag (run_minimize args meth named_thms) id st;
+              apply_method Minimized MinimizedFT)
             else ())
           else ()
         end
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -28,9 +28,9 @@
   val partial_type_encs : string list
   val default_metis_lam_trans : string
 
-  val metis_call : string -> string -> string
   val forall_of : term -> term -> term
   val exists_of : term -> term -> term
+  val type_enc_aliases : (string * string list) list
   val unalias_type_enc : string -> string list
   val term_of_atp : Proof.context -> bool -> int Symtab.table -> typ option ->
     (string, string atp_type) atp_term -> term
@@ -84,17 +84,6 @@
 
 val default_metis_lam_trans = combsN
 
-fun metis_call type_enc lam_trans =
-  let
-    val type_enc =
-      (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
-        [alias] => alias
-      | _ => type_enc)
-    val opts =
-      [] |> type_enc <> partial_typesN ? cons type_enc
-         |> lam_trans <> default_metis_lam_trans ? cons lam_trans
-  in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
-
 fun term_name' (Var ((s, _), _)) = perhaps (try Name.dest_skolem) s
   | term_name' _ = ""
 
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -129,6 +129,17 @@
       | ord => ord
   in {weight = weight, precedence = precedence} end
 
+fun metis_call type_enc lam_trans =
+  let
+    val type_enc =
+      (case AList.find (fn (enc, encs) => enc = hd encs) type_enc_aliases type_enc of
+        [alias] => alias
+      | _ => type_enc)
+    val opts =
+      [] |> type_enc <> partial_typesN ? cons type_enc
+         |> lam_trans <> default_metis_lam_trans ? cons lam_trans
+  in metisN ^ (if null opts then "" else " (" ^ commas opts ^ ")") end
+
 exception METIS_UNPROVABLE of unit
 
 (* Main function to start Metis proof and reconstruction *)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -286,7 +286,7 @@
 
         val ctxt = ctxt
           |> enrich_context_with_local_facts canonical_isar_proof
-          |> silence_reconstructors debug
+          |> silence_proof_methods debug
 
         val preplay_data = Unsynchronized.ref Canonical_Label_Tab.empty
 
@@ -354,9 +354,9 @@
           if isar_proofs = SOME true then "\nWarning: The Isar proof construction failed." else "")
   in one_line_proof ^ isar_proof end
 
-fun isar_proof_would_be_a_good_idea (reconstr, play) =
+fun isar_proof_would_be_a_good_idea (meth, play) =
   (case play of
-    Played _ => reconstr = SMT
+    Played _ => meth = SMT_Method
   | Play_Timed_Out _ => true
   | Play_Failed => true
   | Not_Played => false)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -100,27 +100,6 @@
     |> Skip_Proof.make_thm thy
   end
 
-fun tac_of_method ctxt (local_facts, global_facts) meth =
-  Method.insert_tac local_facts THEN'
-  (case meth of
-    Metis_Method (type_enc_opt, lam_trans_opt) =>
-    Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
-      (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
-  | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
-  | Meson_Method => Meson.meson_tac ctxt global_facts
-  | _ =>
-    Method.insert_tac global_facts THEN'
-    (case meth of
-      Simp_Method => Simplifier.asm_full_simp_tac ctxt
-    | Simp_Size_Method =>
-      Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
-    | Auto_Method => K (Clasimp.auto_tac ctxt)
-    | Fastforce_Method => Clasimp.fast_force_tac ctxt
-    | Force_Method => Clasimp.force_tac ctxt
-    | Arith_Method => Arith_Data.arith_tac ctxt
-    | Blast_Method => blast_tac ctxt
-    | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
-
 (* main function for preplaying Isar steps; may throw exceptions *)
 fun raw_preplay_step_for_method ctxt timeout meth (Prove (_, xs, _, t, subproofs, fact_names, _)) =
   let
@@ -149,7 +128,7 @@
 
     fun prove () =
       Goal.prove ctxt [] [] goal (fn {context = ctxt, ...} =>
-        HEADGOAL (tac_of_method ctxt facts meth))
+        HEADGOAL (tac_of_proof_method ctxt facts meth))
       handle ERROR msg => error ("Preplay error: " ^ msg)
 
     val play_outcome = take_time timeout prove ()
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -8,24 +8,13 @@
 
 signature SLEDGEHAMMER_ISAR_PROOF =
 sig
+  type proof_method = Sledgehammer_Reconstructor.proof_method
+
   type label = string * int
   type facts = label list * string list (* local and global facts *)
 
   datatype isar_qualifier = Show | Then
 
-  datatype proof_method =
-    Metis_Method of string option * string option |
-    Meson_Method |
-    SMT_Method |
-    Simp_Method |
-    Simp_Size_Method |
-    Auto_Method |
-    Fastforce_Method |
-    Force_Method |
-    Arith_Method |
-    Blast_Method |
-    Algebra_Method
-
   datatype isar_proof =
     Proof of (string * typ) list * (label * term) list * isar_step list
   and isar_step =
@@ -38,8 +27,6 @@
   val label_ord : label * label -> order
   val string_of_label : label -> string
 
-  val string_of_proof_method : proof_method -> string
-
   val steps_of_isar_proof : isar_proof -> isar_step list
 
   val label_of_isar_step : isar_step -> label option
@@ -79,19 +66,6 @@
 
 datatype isar_qualifier = Show | Then
 
-datatype proof_method =
-  Metis_Method of string option * string option |
-  Meson_Method |
-  SMT_Method |
-  Simp_Method |
-  Simp_Size_Method |
-  Auto_Method |
-  Fastforce_Method |
-  Force_Method |
-  Arith_Method |
-  Blast_Method |
-  Algebra_Method
-
 datatype isar_proof =
   Proof of (string * typ) list * (label * term) list * isar_step list
 and isar_step =
@@ -105,22 +79,6 @@
 
 fun string_of_label (s, num) = s ^ string_of_int num
 
-fun string_of_proof_method meth =
-  (case meth of
-    Metis_Method (NONE, NONE) => "metis"
-  | Metis_Method (type_enc_opt, lam_trans_opt) =>
-    "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
-  | Meson_Method => "meson"
-  | SMT_Method => "smt"
-  | Simp_Method => "simp"
-  | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
-  | Auto_Method => "auto"
-  | Fastforce_Method => "fastforce"
-  | Force_Method => "force"
-  | Arith_Method => "arith"
-  | Blast_Method => "blast"
-  | Algebra_Method => "algebra")
-
 fun steps_of_isar_proof (Proof (_, _, steps)) = steps
 
 fun label_of_isar_step (Prove (_, _, l, _, _, _, _)) = SOME l
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -12,7 +12,7 @@
   type stature = ATP_Problem_Generate.stature
   type type_enc = ATP_Problem_Generate.type_enc
   type fact = Sledgehammer_Fact.fact
-  type reconstructor = Sledgehammer_Reconstructor.reconstructor
+  type proof_method = Sledgehammer_Reconstructor.proof_method
   type play_outcome = Sledgehammer_Reconstructor.play_outcome
   type minimize_command = Sledgehammer_Reconstructor.minimize_command
 
@@ -57,8 +57,8 @@
      used_facts : (string * stature) list,
      used_from : fact list,
      run_time : Time.time,
-     preplay : (reconstructor * play_outcome) Lazy.lazy,
-     message : reconstructor * play_outcome -> string,
+     preplay : (proof_method * play_outcome) Lazy.lazy,
+     message : proof_method * play_outcome -> string,
      message_tail : string}
 
   type prover =
@@ -66,23 +66,22 @@
     -> prover_problem -> prover_result
 
   val SledgehammerN : string
-  val plain_metis : reconstructor
   val overlord_file_location_of_prover : string -> string * string
   val proof_banner : mode -> string -> string
-  val extract_reconstructor : params -> reconstructor -> string * (string * string list) list
-  val is_reconstructor : string -> bool
+  val extract_proof_method : params -> proof_method -> string * (string * string list) list
+  val is_proof_method : string -> bool
   val is_atp : theory -> string -> bool
-  val bunch_of_reconstructors : bool -> (bool -> string) -> reconstructor list
+  val bunch_of_proof_methods : bool -> string -> proof_method list
   val is_fact_chained : (('a * stature) * 'b) -> bool
   val filter_used_facts :
     bool -> (''a * stature) list -> ((''a * stature) * 'b) list ->
     ((''a * stature) * 'b) list
   val play_one_line_proof : mode -> bool -> bool -> Time.time -> ((string * 'a) * thm) list ->
-    Proof.state -> int -> reconstructor -> reconstructor list -> reconstructor * play_outcome
+    Proof.state -> int -> proof_method -> proof_method list -> proof_method * play_outcome
   val remotify_atp_if_not_installed : theory -> string -> string option
   val isar_supported_prover_of : theory -> string -> string
   val choose_minimize_command : theory -> params -> ((string * string list) list -> string -> 'a) ->
-    string -> reconstructor * play_outcome -> 'a
+    string -> proof_method * play_outcome -> 'a
   val repair_monomorph_context : int option -> int -> int option -> int -> Proof.context ->
     Proof.context
 
@@ -110,9 +109,8 @@
    "Async_Manager". *)
 val SledgehammerN = "Sledgehammer"
 
-val reconstructor_names = [metisN, smtN]
-val plain_metis = Metis (hd partial_type_encs, combsN)
-val is_reconstructor = member (op =) reconstructor_names
+val proof_method_names = [metisN, smtN]
+val is_proof_method = member (op =) proof_method_names
 
 val is_atp = member (op =) o supported_atps
 
@@ -167,8 +165,8 @@
    used_facts : (string * stature) list,
    used_from : fact list,
    run_time : Time.time,
-   preplay : (reconstructor * play_outcome) Lazy.lazy,
-   message : reconstructor * play_outcome -> string,
+   preplay : (proof_method * play_outcome) Lazy.lazy,
+   message : proof_method * play_outcome -> string,
    message_tail : string}
 
 type prover =
@@ -183,29 +181,30 @@
   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   | _ => "Try this")
 
-fun bunch_of_reconstructors needs_full_types lam_trans =
+fun bunch_of_proof_methods needs_full_types desperate_lam_trans =
   if needs_full_types then
-    [Metis (full_type_enc, lam_trans false),
-     Metis (really_full_type_enc, lam_trans false),
-     Metis (full_type_enc, lam_trans true),
-     Metis (really_full_type_enc, lam_trans true),
-     SMT]
+    [Metis_Method (SOME full_type_enc, NONE),
+     Metis_Method (SOME really_full_type_enc, NONE),
+     Metis_Method (SOME full_type_enc, SOME desperate_lam_trans),
+     Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
+     SMT_Method]
   else
-    [Metis (partial_type_enc, lam_trans false),
-     Metis (full_type_enc, lam_trans false),
-     Metis (no_typesN, lam_trans true),
-     Metis (really_full_type_enc, lam_trans true),
-     SMT]
+    [Metis_Method (NONE, NONE),
+     Metis_Method (SOME full_type_enc, NONE),
+     Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
+     Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans),
+     SMT_Method]
 
-fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) =
+fun extract_proof_method ({type_enc, lam_trans, ...} : params)
+      (Metis_Method (type_enc', lam_trans')) =
     let
       val override_params =
-        (if is_none type_enc andalso type_enc' = hd partial_type_encs then []
-         else [("type_enc", [hd (unalias_type_enc type_enc')])]) @
-        (if is_none lam_trans andalso lam_trans' = default_metis_lam_trans then []
-         else [("lam_trans", [lam_trans'])])
+        (if is_none type_enc' andalso is_none type_enc then []
+         else [("type_enc", [hd (unalias_type_enc (type_enc' |> the_default partial_typesN))])]) @
+        (if is_none lam_trans' andalso is_none lam_trans then []
+         else [("lam_trans", [lam_trans' |> the_default default_metis_lam_trans])])
     in (metisN, override_params) end
-  | extract_reconstructor _ SMT = (smtN, [])
+  | extract_proof_method _ SMT_Method = (smtN, [])
 
 (* based on "Mirabelle.can_apply" and generalized *)
 fun timed_apply timeout tac state i =
@@ -216,49 +215,46 @@
     TimeLimit.timeLimit timeout (try (Seq.pull o full_tac)) goal
   end
 
-fun tac_of_reconstructor (Metis (type_enc, lam_trans)) = metis_tac [type_enc] lam_trans
-  | tac_of_reconstructor SMT = SMT_Solver.smt_tac
-
-fun timed_reconstructor reconstr debug timeout ths =
-  timed_apply timeout (silence_reconstructors debug
-    #> (fn ctxt => tac_of_reconstructor reconstr ctxt ths))
+(* FIXME *)
+fun timed_proof_method meth debug timeout ths =
+  timed_apply timeout (silence_proof_methods debug
+    #> (fn ctxt => tac_of_proof_method ctxt ([], ths) meth))
 
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 
 fun filter_used_facts keep_chained used =
   filter ((member (op =) used o fst) orf (if keep_chained then is_fact_chained else K false))
 
-fun play_one_line_proof mode debug verbose timeout pairs state i preferred reconstrs =
+fun play_one_line_proof mode debug verbose timeout pairs state i preferred meths =
   let
-    fun get_preferred reconstrs =
-      if member (op =) reconstrs preferred then preferred
-      else List.last reconstrs
+    fun get_preferred meths =
+      if member (op =) meths preferred then preferred else List.last meths
   in
     if timeout = Time.zeroTime then
-      (get_preferred reconstrs, Not_Played)
+      (get_preferred meths, Not_Played)
     else
       let
         val _ = if mode = Minimize then Output.urgent_message "Preplaying proof..." else ()
         val ths = pairs |> sort_wrt (fst o fst) |> map snd
-        fun play [] [] = (get_preferred reconstrs, Play_Failed)
+        fun play [] [] = (get_preferred meths, Play_Failed)
           | play timed_outs [] = (get_preferred timed_outs, Play_Timed_Out timeout)
-          | play timed_out (reconstr :: reconstrs) =
+          | play timed_out (meth :: meths) =
             let
               val _ =
                 if verbose then
-                  Output.urgent_message ("Trying \"" ^ string_of_reconstructor reconstr ^
+                  Output.urgent_message ("Trying \"" ^ string_of_proof_method meth ^
                     "\" for " ^ string_of_time timeout ^ "...")
                 else
                   ()
               val timer = Timer.startRealTimer ()
             in
-              case timed_reconstructor reconstr debug timeout ths state i of
-                SOME (SOME _) => (reconstr, Played (Timer.checkRealTimer timer))
-              | _ => play timed_out reconstrs
+              case timed_proof_method meth debug timeout ths state i of
+                SOME (SOME _) => (meth, Played (Timer.checkRealTimer timer))
+              | _ => play timed_out meths
             end
-            handle TimeLimit.TimeOut => play (reconstr :: timed_out) reconstrs
+            handle TimeLimit.TimeOut => play (meth :: timed_out) meths
       in
-        play [] reconstrs
+        play [] meths
       end
   end
 
@@ -275,9 +271,8 @@
     val maybe_isar_name = name |> isar_proofs = SOME true ? isar_supported_prover_of thy
     val (min_name, override_params) =
       (case preplay of
-        (reconstr, Played _) =>
-        if isar_proofs = SOME true then (maybe_isar_name, [])
-        else extract_reconstructor params reconstr
+        (meth, Played _) =>
+        if isar_proofs = SOME true then (maybe_isar_name, []) else extract_proof_method params meth
       | _ => (maybe_isar_name, []))
   in minimize_command override_params min_name end
 
@@ -293,7 +288,7 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val (remote_provers, local_provers) =
-      reconstructor_names @
+      proof_method_names @
       sort_strings (supported_atps thy) @
       sort_strings (SMT_Solver.available_solvers_of ctxt)
       |> List.partition (String.isPrefix remote_prefix)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -346,18 +346,15 @@
         let
           val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
-          val reconstrs =
-            bunch_of_reconstructors needs_full_types (fn desperate =>
-              if desperate then
-                if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN
-              else
-                default_metis_lam_trans)
+          val meths =
+            bunch_of_proof_methods needs_full_types
+              (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
         in
           (used_facts,
            Lazy.lazy (fn () =>
              let val used_pairs = used_from |> filter_used_facts false used_facts in
                play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
-                 (hd reconstrs) reconstrs
+                 (hd meths) meths
              end),
            fn preplay =>
               let
@@ -392,7 +389,8 @@
               ""))
         end
       | SOME failure =>
-        ([], Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
+        ([], Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
+         fn _ => string_of_atp_failure failure, ""))
   in
     {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
      preplay = preplay, message = message, message_tail = message_tail}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -8,7 +8,7 @@
 signature SLEDGEHAMMER_PROVER_MINIMIZE =
 sig
   type stature = ATP_Problem_Generate.stature
-  type reconstructor = Sledgehammer_Reconstructor.reconstructor
+  type proof_method = Sledgehammer_Reconstructor.proof_method
   type play_outcome = Sledgehammer_Reconstructor.play_outcome
   type mode = Sledgehammer_Prover.mode
   type params = Sledgehammer_Prover.params
@@ -23,11 +23,11 @@
   val auto_minimize_min_facts : int Config.T
   val auto_minimize_max_time : real Config.T
   val minimize_facts : (thm list -> unit) -> string -> params -> bool -> int -> int ->
-    Proof.state -> thm -> (reconstructor * play_outcome) Lazy.lazy option ->
+    Proof.state -> thm -> (proof_method * play_outcome) Lazy.lazy option ->
     ((string * stature) * thm list) list ->
     ((string * stature) * thm list) list option
-    * ((reconstructor * play_outcome) Lazy.lazy * ((reconstructor * play_outcome) -> string)
-       * string)
+      * ((proof_method * play_outcome) Lazy.lazy * ((proof_method * play_outcome) -> string)
+         * string)
   val get_minimizing_prover : Proof.context -> mode -> (thm list -> unit) -> string -> prover
 
   val run_minimize : params -> (thm list -> unit) -> int -> (Facts.ref * Attrib.src list) list ->
@@ -50,29 +50,25 @@
 open Sledgehammer_Prover_ATP
 open Sledgehammer_Prover_SMT
 
-fun run_reconstructor mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
+fun run_proof_method mode name (params as {debug, verbose, timeout, type_enc, lam_trans, ...})
     minimize_command
     ({state, subgoal, subgoal_count, factss = (_, facts) :: _, ...} : prover_problem) =
   let
-    val reconstr =
-      if name = metisN then
-        Metis (type_enc |> the_default (hd partial_type_encs),
-               lam_trans |> the_default default_metis_lam_trans)
-      else if name = smtN then
-        SMT
-      else
-        raise Fail ("unknown reconstructor: " ^ quote name)
+    val meth =
+      if name = metisN then Metis_Method (type_enc, lam_trans)
+      else if name = smtN then SMT_Method
+      else raise Fail ("unknown proof_method: " ^ quote name)
     val used_facts = facts |> map fst
   in
     (case play_one_line_proof (if mode = Minimize then Normal else mode) debug verbose timeout facts
-       state subgoal reconstr [reconstr] of
+       state subgoal meth [meth] of
       play as (_, Played time) =>
       {outcome = NONE, used_facts = used_facts, used_from = facts, run_time = time,
        preplay = Lazy.value play,
        message =
          fn play =>
             let
-              val (_, override_params) = extract_reconstructor params reconstr
+              val (_, override_params) = extract_proof_method params meth
               val one_line_params =
                 (play, proof_banner mode name, used_facts, minimize_command override_params name,
                  subgoal, subgoal_count)
@@ -93,18 +89,18 @@
 
 fun is_prover_supported ctxt =
   let val thy = Proof_Context.theory_of ctxt in
-    is_reconstructor orf is_atp thy orf is_smt_prover ctxt
+    is_proof_method orf is_atp thy orf is_smt_prover ctxt
   end
 
 fun is_prover_installed ctxt =
-  is_reconstructor orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
+  is_proof_method orf is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
 
-val reconstructor_default_max_facts = 20
+val proof_method_default_max_facts = 20
 
 fun default_max_facts_of_prover ctxt name =
   let val thy = Proof_Context.theory_of ctxt in
-    if is_reconstructor name then
-      reconstructor_default_max_facts
+    if is_proof_method name then
+      proof_method_default_max_facts
     else if is_atp thy name then
       fold (Integer.max o fst o #1 o fst o snd) (#best_slices (get_atp thy name ()) ctxt) 0
     else (* is_smt_prover ctxt name *)
@@ -113,7 +109,7 @@
 
 fun get_prover ctxt mode name =
   let val thy = Proof_Context.theory_of ctxt in
-    if is_reconstructor name then run_reconstructor mode name
+    if is_proof_method name then run_proof_method mode name
     else if is_atp thy name then run_atp mode name
     else if is_smt_prover ctxt name then run_smt_solver mode name
     else error ("No such prover: " ^ name ^ ".")
@@ -286,10 +282,11 @@
           "Timeout: You can increase the time limit using the \"timeout\" option (e.g., \
           \timeout = " ^ string_of_int (10 + Time.toMilliseconds timeout div 1000) ^ "\").", ""))
      | {preplay, message, ...} => (NONE, (preplay, prefix "Prover error: " o message, ""))))
-    handle ERROR msg => (NONE, (Lazy.value (plain_metis, Play_Failed), fn _ => "Error: " ^ msg, ""))
+    handle ERROR msg =>
+      (NONE, (Lazy.value (Metis_Method (NONE, NONE), Play_Failed), fn _ => "Error: " ^ msg, ""))
   end
 
-fun adjust_reconstructor_params override_params
+fun adjust_proof_method_params override_params
     ({debug, verbose, overlord, spy, blocking, provers, type_enc, strict, lam_trans,
       uncurried_aliases, learn, fact_filter, max_facts, fact_thresholds, max_mono_iters,
       max_new_mono_instances, isar_proofs, compress_isar, try0_isar, slice, minimize, timeout,
@@ -299,7 +296,7 @@
       (case AList.lookup (op =) override_params name of
         SOME [s] => SOME s
       | _ => default_value)
-    (* Only those options that reconstructors are interested in are considered here. *)
+    (* Only those options that proof_methods are interested in are considered here. *)
     val type_enc = lookup_override "type_enc" type_enc
     val lam_trans = lookup_override "lam_trans" lam_trans
   in
@@ -336,18 +333,18 @@
               fun prover_fast_enough () = can_min_fast_enough run_time
             in
               (case Lazy.force preplay of
-                 (reconstr as Metis _, Played timeout) =>
+                 (meth as Metis_Method _, Played timeout) =>
                  if isar_proofs = SOME true then
                    (* Cheat: Assume the selected ATP is as fast as "metis" for the goal it proved
                       itself. *)
                    (can_min_fast_enough timeout, (isar_supported_prover_of thy name, params))
                  else if can_min_fast_enough timeout then
-                   (true, extract_reconstructor params reconstr
+                   (true, extract_proof_method params meth
                           ||> (fn override_params =>
-                                  adjust_reconstructor_params override_params params))
+                                  adjust_proof_method_params override_params params))
                  else
                    (prover_fast_enough (), (name, params))
-               | (SMT, Played timeout) =>
+               | (SMT_Method, Played timeout) =>
                  (* Cheat: Assume the original prover is as fast as "smt" for the goal it proved
                     itself. *)
                  (can_min_fast_enough timeout, (name, params))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -233,9 +233,8 @@
       (case outcome of
         NONE =>
         (Lazy.lazy (fn () =>
-           play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT
-             (bunch_of_reconstructors false (fn desperate =>
-                if desperate then liftingN else default_metis_lam_trans))),
+           play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
+             SMT_Method (bunch_of_proof_methods false liftingN)),
          fn preplay =>
             let
               val one_line_params =
@@ -248,7 +247,8 @@
             end,
          if verbose then "\nSMT solver real CPU time: " ^ string_of_time run_time ^ "." else "")
       | SOME failure =>
-        (Lazy.value (plain_metis, Play_Failed), fn _ => string_of_atp_failure failure, ""))
+        (Lazy.value (Metis_Method (NONE, NONE), Play_Failed),
+         fn _ => string_of_atp_failure failure, ""))
   in
     {outcome = outcome, used_facts = used_facts, used_from = used_from, run_time = run_time,
      preplay = preplay, message = message, message_tail = message_tail}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -9,9 +9,18 @@
 sig
   type stature = ATP_Problem_Generate.stature
 
-  datatype reconstructor =
-    Metis of string * string |
-    SMT
+  datatype proof_method =
+    Metis_Method of string option * string option |
+    Meson_Method |
+    SMT_Method |
+    Simp_Method |
+    Simp_Size_Method |
+    Auto_Method |
+    Fastforce_Method |
+    Force_Method |
+    Arith_Method |
+    Blast_Method |
+    Algebra_Method
 
   datatype play_outcome =
     Played of Time.time |
@@ -21,16 +30,17 @@
 
   type minimize_command = string list -> string
   type one_line_params =
-    (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
+    (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
 
   val smtN : string
 
-  val string_of_reconstructor : reconstructor -> string
+  val string_of_proof_method : proof_method -> string
+  val tac_of_proof_method : Proof.context -> thm list * thm list -> proof_method -> int -> tactic
   val string_of_play_outcome : play_outcome -> string
   val play_outcome_ord : play_outcome * play_outcome -> order
 
   val one_line_proof_text : int -> one_line_params -> string
-  val silence_reconstructors : bool -> Proof.context -> Proof.context
+  val silence_proof_methods : bool -> Proof.context -> Proof.context
 end;
 
 structure Sledgehammer_Reconstructor : SLEDGEHAMMER_RECONSTRUCTOR =
@@ -40,9 +50,18 @@
 open ATP_Problem_Generate
 open ATP_Proof_Reconstruct
 
-datatype reconstructor =
-  Metis of string * string |
-  SMT
+datatype proof_method =
+  Metis_Method of string option * string option |
+  Meson_Method |
+  SMT_Method |
+  Simp_Method |
+  Simp_Size_Method |
+  Auto_Method |
+  Fastforce_Method |
+  Force_Method |
+  Arith_Method |
+  Blast_Method |
+  Algebra_Method
 
 datatype play_outcome =
   Played of Time.time |
@@ -52,12 +71,46 @@
 
 type minimize_command = string list -> string
 type one_line_params =
-  (reconstructor * play_outcome) * string * (string * stature) list * minimize_command * int * int
+  (proof_method * play_outcome) * string * (string * stature) list * minimize_command * int * int
 
 val smtN = "smt"
 
-fun string_of_reconstructor (Metis (type_enc, lam_trans)) = metis_call type_enc lam_trans
-  | string_of_reconstructor SMT = smtN
+fun string_of_proof_method meth =
+  (case meth of
+    Metis_Method (NONE, NONE) => "metis"
+  | Metis_Method (type_enc_opt, lam_trans_opt) =>
+    "metis (" ^ commas (map_filter I [type_enc_opt, lam_trans_opt]) ^ ")"
+  | Meson_Method => "meson"
+  | SMT_Method => "smt"
+  | Simp_Method => "simp"
+  | Simp_Size_Method => "simp add: size_ne_size_imp_ne"
+  | Auto_Method => "auto"
+  | Fastforce_Method => "fastforce"
+  | Force_Method => "force"
+  | Arith_Method => "arith"
+  | Blast_Method => "blast"
+  | Algebra_Method => "algebra")
+
+fun tac_of_proof_method ctxt (local_facts, global_facts) meth =
+  Method.insert_tac local_facts THEN'
+  (case meth of
+    Metis_Method (type_enc_opt, lam_trans_opt) =>
+    Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
+      (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
+  | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
+  | Meson_Method => Meson.meson_tac ctxt global_facts
+  | _ =>
+    Method.insert_tac global_facts THEN'
+    (case meth of
+      Simp_Method => Simplifier.asm_full_simp_tac ctxt
+    | Simp_Size_Method =>
+      Simplifier.asm_full_simp_tac (Simplifier.add_simp @{thm size_ne_size_imp_ne} ctxt)
+    | Auto_Method => K (Clasimp.auto_tac ctxt)
+    | Fastforce_Method => Clasimp.fast_force_tac ctxt
+    | Force_Method => Clasimp.force_tac ctxt
+    | Arith_Method => Arith_Data.arith_tac ctxt
+    | Blast_Method => blast_tac ctxt
+    | Algebra_Method => Groebner.algebra_tac [] [] ctxt))
 
 fun string_of_play_outcome (Played time) = string_of_ext_time (false, time)
   | string_of_play_outcome (Play_Timed_Out time) = string_of_ext_time (true, time) ^ ", timed out"
@@ -94,9 +147,10 @@
     name |> not (Symbol_Pos.is_identifier name) ? enclose "(" ")"
   | command_call name args = "(" ^ name ^ " " ^ space_implode " " args ^ ")"
 
-fun reconstructor_command reconstr i n used_chaineds num_chained ss =
+(* FIXME *)
+fun proof_method_command meth i n used_chaineds num_chained ss =
   (* unusing_chained_facts used_chaineds num_chained ^ *)
-  apply_on_subgoal i n ^ command_call (string_of_reconstructor reconstr) ss
+  apply_on_subgoal i n ^ command_call (string_of_proof_method meth) ss
 
 fun show_time NONE = ""
   | show_time (SOME ext_time) = " (" ^ string_of_ext_time ext_time ^ ")"
@@ -116,7 +170,7 @@
   |> pairself (sort_distinct (string_ord o pairself fst))
 
 fun one_line_proof_text num_chained
-    ((reconstr, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
+    ((meth, play), banner, used_facts, minimize_command, subgoal, subgoal_count) =
   let
     val (chained, extra) = split_used_facts used_facts
 
@@ -129,7 +183,7 @@
 
     val try_line =
       map fst extra
-      |> reconstructor_command reconstr subgoal subgoal_count (map fst chained) num_chained
+      |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
       |> (if failed then
             enclose "One-line proof reconstruction failed: "
               ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
@@ -139,9 +193,9 @@
     try_line ^ minimize_line minimize_command (map fst (extra @ chained))
   end
 
-(* Makes reconstructor tools as silent as possible. The "set_visible" calls suppresses "Unification
-   bound exceeded" warnings and the like. *)
-fun silence_reconstructors debug =
+(* Makes proof methods as silent as possible. The "set_visible" calls suppresses "Unification bound
+   exceeded" warnings and the like. *)
+fun silence_proof_methods debug =
   Try0.silence_methods debug
   #> Config.put SMT_Config.verbose debug
 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Feb 03 14:35:19 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Mon Feb 03 15:19:07 2014 +0100
@@ -69,10 +69,10 @@
    | "" => SOME true
    | _ => raise Option.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
+    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
 
 val has_junk =
   exists (fn s => not (Symbol.is_digit s) andalso s <> ".") o raw_explode (* FIXME Symbol.explode (?) *)
@@ -80,8 +80,8 @@
 fun parse_time name s =
   let val secs = if has_junk s then NONE else Real.fromString s in
     if is_none secs orelse Real.< (the secs, 0.0) then
-      error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \
-             \number of seconds (e.g., \"60\", \"0.5\") or \"none\".")
+      error ("Parameter " ^ quote name ^ " must be assigned a nonnegative \number of seconds \
+        \(e.g., \"60\", \"0.5\") or \"none\".")
     else
       seconds (the secs)
   end