# HG changeset patch
# User blanchet
# Date 1391452322 -3600
# Node ID 1dfcd49f5dcb7738a99df2f79d1fa7dc63ac27ce
# Parent  1d3dadda13a150a9d84350c8104483b7aa141db2
renamed 'smt' option 'smt_proofs' to avoid clash with 'smt' prover

diff -r 1d3dadda13a1 -r 1dfcd49f5dcb NEWS
--- a/NEWS	Mon Feb 03 19:32:02 2014 +0100
+++ b/NEWS	Mon Feb 03 19:32:02 2014 +0100
@@ -116,7 +116,7 @@
 
 * Sledgehammer:
   - New option:
-      smt
+      smt_proofs
   - Renamed options:
       isar_compress ~> compress_isar
       isar_try0 ~> try0_isar
diff -r 1d3dadda13a1 -r 1dfcd49f5dcb src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Feb 03 19:32:02 2014 +0100
@@ -117,7 +117,7 @@
 
 The result of a successful proof search is some source text that usually (but
 not always) reconstructs the proof within Isabelle. For ATPs, the reconstructed
-proof relies on the general-purpose \textit{metis} proof method, which
+proof typically relies on the general-purpose \textit{metis} proof method, which
 integrates the Metis ATP in Isabelle/HOL with explicit inferences going through
 the kernel. Thus its results are correct by construction.
 
@@ -296,7 +296,7 @@
 Waldmeister is run only for unit equational problems, where the goal's
 conclusion is a (universally quantified) equation.
 
-For each successful prover, Sledgehammer gives a one-liner \textit{metis} or
+For each successful prover, Sledgehammer gives a one-line \textit{metis} or
 \textit{smt} method call. Rough timings are shown in parentheses, indicating how
 fast the call is. You can click the proof to insert it into the theory text.
 
@@ -308,7 +308,7 @@
 \postw
 
 When Isar proof construction is successful, it can yield proofs that are more
-readable and also faster than the \textit{metis} or \textit{smt} one-liners.
+readable and also faster than the \textit{metis} or \textit{smt} one-line proofs.
 This feature is experimental and is only available for ATPs.
 
 \section{Hints}
@@ -359,7 +359,7 @@
 if that helps.
 
 \item[\labelitemi] \textbf{\textit{isar\_proofs}} (\S\ref{output-format}) specifies
-that Isar proofs should be generated, in addition to one-liner \textit{metis} or
+that Isar proofs should be generated, in addition to one-line \textit{metis} or
 \textit{smt} proofs. The length of the Isar proofs can be controlled by setting
 \textit{compress\_isar} (\S\ref{output-format}).
 
@@ -463,9 +463,8 @@
 
 \begin{enum}
 \item[\labelitemi] Try the \textit{isar\_proofs} option (\S\ref{output-format}) to
-obtain a step-by-step Isar proof where each step is justified by \textit{metis}.
-Since the steps are fairly small, \textit{metis} is more likely to be able to
-replay them.
+obtain a step-by-step Isar proof. Since the steps are fairly small, \textit{metis}
+and the other Isabelle proof methods are more likely to be able to replay them.
 
 \item[\labelitemi] Try the \textit{smt} proof method instead of \textit{metis}.
 It is usually stronger, but you need to either have Z3 available to replay the
@@ -525,8 +524,8 @@
 versions of Metis. It is somewhat slower than \textit{metis}, but the proof
 search is fully typed, and it also includes more powerful rules such as the
 axiom ``$x = \const{True} \mathrel{\lor} x = \const{False}$'' for reasoning in
-higher-order places (e.g., in set comprehensions). The method kicks in
-automatically as a fallback when \textit{metis} fails, and it is sometimes
+higher-order places (e.g., in set comprehensions). The method is automatically
+tried as a fallback when \textit{metis} fails, and it is sometimes
 generated by Sledgehammer instead of \textit{metis} if the proof obviously
 requires type information or if \textit{metis} failed when Sledgehammer
 preplayed the proof. (By default, Sledgehammer tries to run \textit{metis} with
@@ -1069,9 +1068,9 @@
 
 \opdefault{max\_facts}{smart\_int}{smart}
 Specifies the maximum number of facts that may be returned by the relevance
-filter. If the option is set to \textit{smart}, it effectively takes a value
-that was empirically found to be appropriate for the prover. Typical values
-range between 50 and 1000.
+filter. If the option is set to \textit{smart} (the default), it effectively
+takes a value that was empirically found to be appropriate for the prover.
+Typical values range between 50 and 1000.
 
 For the MaSh-related commands \textit{learn\_isar}, \textit{learn\_prover},
 \textit{relearn\_isar}, and \textit{relearn\_prover}, this option specifies the
@@ -1095,9 +1094,9 @@
 Specifies the maximum number of monomorphic instances to generate beyond
 \textit{max\_facts}. The higher this limit is, the more monomorphic instances
 are potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it takes a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 100.
+type encoding used. If the option is set to \textit{smart} (the default), it
+takes a value that was empirically found to be appropriate for the prover. For
+most provers, this value is 100.
 
 \nopagebreak
 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
@@ -1106,9 +1105,9 @@
 Specifies the maximum number of iterations for the monomorphization fixpoint
 construction. The higher this limit is, the more monomorphic instances are
 potentially generated. Whether monomorphization takes place depends on the
-type encoding used. If the option is set to \textit{smart}, it takes a value
-that was empirically found to be appropriate for the prover. For most provers,
-this value is 3.
+type encoding used. If the option is set to \textit{smart} (the default), it
+takes a value that was empirically found to be appropriate for the prover.
+For most provers, this value is 3.
 
 \nopagebreak
 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
@@ -1298,12 +1297,11 @@
 \textit{overlord} (\S\ref{mode-of-operation}).}
 
 \opsmart{isar\_proofs}{no\_isar\_proofs}
-Specifies whether Isar proofs should be output in addition to one-liner
-\textit{metis} proofs. The construction of Isar proof is still experimental and
-may sometimes fail; however, when they succeed they are usually faster and more
-intelligible than \textit{metis} proofs. If the option is set to \textit{smart}
-(the default), Isar proofs are only generated when no working one-liner
-\textit{metis} proof is available.
+Specifies whether Isar proofs should be output in addition to one-line proofs.
+The construction of Isar proof is still experimental and may sometimes fail;
+however, when they succeed they are usually faster and more intelligible than
+one-line proofs. If the option is set to \textit{smart} (the default), Isar
+proofs are only generated when no working one-line proof is available.
 
 \opdefault{compress\_isar}{int}{\upshape 10}
 Specifies the granularity of the generated Isar proofs if \textit{isar\_proofs}
@@ -1318,10 +1316,11 @@
 \textit{blast} should be tried as alternatives to \textit{metis} in Isar proofs.
 The collection of methods is roughly the same as for the \textbf{try0} command.
 
-\opsmart{smt}{no\_smt}
+\opsmart{smt\_proofs}{no\_smt\_proofs}
 Specifies whether the \textit{smt} proof method should be tried as an
-alternative to \textit{metis}.  If the option is set to \textit{smart}, the
-\textit{smt} method is used for one-line proofs but not in Isar proofs.
+alternative to \textit{metis}.  If the option is set to \textit{smart} (the
+default), the \textit{smt} method is used for one-line proofs but not in Isar
+proofs.
 \end{enum}
 
 \subsection{Authentication}
@@ -1357,10 +1356,10 @@
 searching for a proof. This excludes problem preparation and is a soft limit.
 
 \opdefault{preplay\_timeout}{float}{\upshape 2}
-Specifies the maximum number of seconds that \textit{metis} or \textit{smt}
-should spend trying to ``preplay'' the found proof. If this option is set to 0,
-no preplaying takes place, and no timing information is displayed next to the
-suggested \textit{metis} calls.
+Specifies the maximum number of seconds that \textit{metis} or other proof
+methods should spend trying to ``preplay'' the found proof. If this option
+is set to 0, no preplaying takes place, and no timing information is displayed
+next to the suggested proof method calls.
 
 \nopagebreak
 {\small See also \textit{minimize} (\S\ref{mode-of-operation}).}
diff -r 1d3dadda13a1 -r 1dfcd49f5dcb src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -96,7 +96,7 @@
    ("isar_proofs", "smart"),
    ("compress_isar", "10"),
    ("try0_isar", "true"),
-   ("smt", "smart"),
+   ("smt_proofs", "smart"),
    ("slice", "true"),
    ("minimize", "smart"),
    ("preplay_timeout", "2")]
@@ -119,7 +119,7 @@
    ("dont_slice", "slice"),
    ("dont_minimize", "minimize"),
    ("dont_try0_isar", "try0_isar"),
-   ("no_smt", "smt")]
+   ("no_smt_proofs", "smt_proofs")]
 
 val params_not_for_minimize =
   ["blocking", "fact_filter", "max_facts", "fact_thresholds", "slice", "minimize"];
@@ -288,7 +288,7 @@
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
     val compress_isar = Real.max (1.0, lookup_real "compress_isar")
     val try0_isar = lookup_bool "try0_isar"
-    val smt = lookup_option lookup_bool "smt"
+    val smt_proofs = lookup_option lookup_bool "smt_proofs"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
     val timeout = lookup_time "timeout"
@@ -300,7 +300,7 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
+     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
      minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
diff -r 1d3dadda13a1 -r 1dfcd49f5dcb src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -126,7 +126,7 @@
 val skolem_methods =
   [Metis_Method (NONE, NONE), Blast_Method, Meson_Method]
 
-fun isar_proof_text ctxt debug isar_proofs smt isar_params
+fun isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
     (one_line_params as (_, _, _, _, subgoal, subgoal_count)) =
   let
     fun isar_proof_of () =
@@ -137,7 +137,9 @@
         val metislike_methods = insert (op =) (Metis_Method alt_metis_args) metislike_methods0
 
         fun massage_meths (meths as meth :: _) =
-          if not try0_isar then [meth] else if smt = SOME true then SMT_Method :: meths else meths
+          if not try0_isar then [meth]
+          else if smt_proofs = SOME true then SMT_Method :: meths
+          else meths
 
         val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
         val fixes = map (fn (s, T) => (Binding.name s, SOME T, NoSyn)) params
@@ -355,18 +357,18 @@
           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 smt (meth, play) =
+fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
   (case play of
-    Played _ => meth = SMT_Method andalso smt <> SOME true
+    Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
   | Play_Timed_Out _ => true
   | Play_Failed => true
   | Not_Played => false)
 
-fun proof_text ctxt debug isar_proofs smt isar_params num_chained
+fun proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
     (one_line_params as (preplay, _, _, _, _, _)) =
   (if isar_proofs = SOME true orelse
-      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt preplay) then
-     isar_proof_text ctxt debug isar_proofs smt isar_params
+      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea smt_proofs preplay) then
+     isar_proof_text ctxt debug isar_proofs smt_proofs isar_params
    else
      one_line_proof_text num_chained) one_line_params
 
diff -r 1d3dadda13a1 -r 1dfcd49f5dcb src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -38,7 +38,7 @@
      isar_proofs : bool option,
      compress_isar : real,
      try0_isar : bool,
-     smt : bool option,
+     smt_proofs : bool option,
      slice : bool,
      minimize : bool option,
      timeout : Time.time,
@@ -147,7 +147,7 @@
    isar_proofs : bool option,
    compress_isar : real,
    try0_isar : bool,
-   smt : bool option,
+   smt_proofs : bool option,
    slice : bool,
    minimize : bool option,
    timeout : Time.time,
@@ -183,7 +183,7 @@
   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   | _ => "Try this")
 
-fun bunch_of_proof_methods smt needs_full_types desperate_lam_trans =
+fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
   [Metis_Method (SOME full_type_enc, NONE)] @
   (if needs_full_types then
      [Metis_Method (SOME full_type_enc, NONE),
@@ -193,7 +193,7 @@
      [Metis_Method (NONE, NONE),
       Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
   [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
-  (if smt then [SMT_Method] else [])
+  (if smt_proofs then [SMT_Method] else [])
 
 fun extract_proof_method ({type_enc, lam_trans, ...} : params)
       (Metis_Method (type_enc', lam_trans')) =
diff -r 1d3dadda13a1 -r 1dfcd49f5dcb src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -132,7 +132,7 @@
 fun run_atp mode name
     (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
        fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
-       try0_isar, smt, slice, minimize, timeout, preplay_timeout, ...})
+       try0_isar, smt_proofs, slice, minimize, timeout, preplay_timeout, ...})
     minimize_command
     ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
@@ -347,7 +347,7 @@
           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 meths =
-            bunch_of_proof_methods (smt <> SOME false) needs_full_types
+            bunch_of_proof_methods (smt_proofs <> SOME false) needs_full_types
               (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN)
         in
           (used_facts,
@@ -380,7 +380,7 @@
                    subgoal_count)
                 val num_chained = length (#facts (Proof.goal state))
               in
-                proof_text ctxt debug isar_proofs smt isar_params num_chained one_line_params
+                proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
               end,
            (if verbose then "\nATP real CPU time: " ^ string_of_time run_time ^ "." else "") ^
            (if important_message <> "" then
diff -r 1d3dadda13a1 -r 1dfcd49f5dcb src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -129,8 +129,8 @@
 fun print silent f = if silent then () else Output.urgent_message (f ())
 
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
-      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar, smt,
-      preplay_timeout, ...} : params)
+      type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress_isar, try0_isar,
+      smt_proofs, preplay_timeout, ...} : params)
     silent (prover : prover) timeout i n state goal facts =
   let
     val _ =
@@ -144,9 +144,9 @@
        uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
        max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
        max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
-       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar, smt = smt,
-       slice = false, minimize = SOME false, timeout = timeout, preplay_timeout = preplay_timeout,
-       expect = ""}
+       isar_proofs = isar_proofs, compress_isar = compress_isar, try0_isar = try0_isar,
+       smt_proofs = smt_proofs, slice = false, minimize = SOME false, timeout = timeout,
+       preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)]}
@@ -289,8 +289,8 @@
 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, smt, slice, minimize, timeout,
-      preplay_timeout, expect} : params) =
+      max_new_mono_instances, isar_proofs, compress_isar, try0_isar, smt_proofs, slice, minimize,
+      timeout, preplay_timeout, expect} : params) =
   let
     fun lookup_override name default_value =
       (case AList.lookup (op =) override_params name of
@@ -305,7 +305,7 @@
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
      max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress_isar = compress_isar, try0_isar = try0_isar, smt = smt, slice = slice,
+     compress_isar = compress_isar, try0_isar = try0_isar, smt_proofs = smt_proofs, slice = slice,
      minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
   end
 
diff -r 1d3dadda13a1 -r 1dfcd49f5dcb src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 19:32:02 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Mon Feb 03 19:32:02 2014 +0100
@@ -212,7 +212,7 @@
     do_slice timeout 1 NONE Time.zeroTime
   end
 
-fun run_smt_solver mode name (params as {debug, verbose, smt, preplay_timeout, ...})
+fun run_smt_solver mode name (params as {debug, verbose, smt_proofs, preplay_timeout, ...})
     minimize_command ({state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
   let
     val thy = Proof.theory_of state
@@ -234,7 +234,7 @@
         NONE =>
         (Lazy.lazy (fn () =>
            play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal
-             SMT_Method (bunch_of_proof_methods (smt <> SOME false) false liftingN)),
+             SMT_Method (bunch_of_proof_methods (smt_proofs <> SOME false) false liftingN)),
          fn preplay =>
             let
               val one_line_params =