simplified 'smt_proofs' option to be a binary option (instead of ternary), now that SMT proofs are accepted in the AFP (done with Martin Desharnais)

--- a/src/Doc/Sledgehammer/document/root.tex	Tue Jun 09 12:13:15 2020 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Jun 10 15:55:41 2020 +0200
@@ -1234,11 +1234,9 @@
 \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\_proofs}{no\_smt\_proofs}
+\optrue{smt\_proofs}{no\_smt\_proofs}
 Specifies whether the \textit{smt} proof method should be tried in addition to
-Isabelle's other proof methods. 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.
+Isabelle's built-in proof methods.
 \end{enum}
 
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Tue Jun 09 12:13:15 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jun 10 15:55:41 2020 +0200
@@ -68,7 +68,7 @@
    ("isar_proofs", "smart"),
    ("compress", "smart"),
    ("try0", "true"),
-   ("smt_proofs", "smart"),
+   ("smt_proofs", "true"),
    ("slice", "true"),
    ("minimize", "true"),
    ("preplay_timeout", "1")]
@@ -267,7 +267,7 @@
     val isar_proofs = lookup_option lookup_bool "isar_proofs"
     val compress = Option.map (curry Real.max 1.0) (lookup_option lookup_real "compress")
     val try0 = lookup_bool "try0"
-    val smt_proofs = lookup_option lookup_bool "smt_proofs"
+    val smt_proofs = lookup_bool "smt_proofs"
     val slice = mode <> Auto_Try andalso lookup_bool "slice"
     val minimize = lookup_bool "minimize"
     val timeout = lookup_time "timeout"

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Jun 09 12:13:15 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Jun 10 15:55:41 2020 +0200
@@ -19,8 +19,8 @@
     bool * (string option * string option) * Time.time * real option * bool * bool
     * (term, string) atp_step list * thm
 
-  val proof_text : Proof.context -> bool -> bool option -> bool option -> (unit -> isar_params) ->
-    int -> one_line_params -> string
+  val proof_text : Proof.context -> bool -> bool option -> bool -> (unit -> isar_params) -> int ->
+    one_line_params -> string
 end;
 
 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
@@ -164,7 +164,7 @@
 
             fun massage_methods (meths as meth :: _) =
               if not try0 then [meth]
-              else if smt_proofs = SOME true then SMT_Method :: meths
+              else if smt_proofs then SMT_Method :: meths
               else meths
 
             val (params, _, concl_t) = strip_subgoal goal subgoal ctxt
@@ -461,16 +461,16 @@
         (if isar_proofs = SOME true then "\nWarning: Isar proof construction failed" else ""))
   end
 
-fun isar_proof_would_be_a_good_idea smt_proofs (meth, play) =
+fun isar_proof_would_be_a_good_idea (meth, play) =
   (case play of
-    Played _ => meth = SMT_Method andalso smt_proofs <> SOME true
+    Played _ => false
   | Play_Timed_Out time => time > Time.zeroTime
   | Play_Failed => true)
 
 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_proofs preplay) then
+      (isar_proofs = NONE andalso isar_proof_would_be_a_good_idea preplay) then
      isar_proof_text ctxt debug num_chained isar_proofs smt_proofs isar_params
    else
      one_line_proof_text ctxt num_chained) one_line_params

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Tue Jun 09 12:13:15 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Wed Jun 10 15:55:41 2020 +0200
@@ -36,7 +36,7 @@
      isar_proofs : bool option,
      compress : real option,
      try0 : bool,
-     smt_proofs : bool option,
+     smt_proofs : bool,
      slice : bool,
      minimize : bool,
      timeout : Time.time,
@@ -121,7 +121,7 @@
    isar_proofs : bool option,
    compress : real option,
    try0 : bool,
-   smt_proofs : bool option,
+   smt_proofs : bool,
    slice : bool,
    minimize : bool,
    timeout : Time.time,
@@ -155,7 +155,7 @@
   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   | _ => "Try this")
 
-fun bunches_of_proof_methods try0 smt_method needs_full_types desperate_lam_trans =
+fun bunches_of_proof_methods try0 smt_proofs needs_full_types desperate_lam_trans =
   (if try0 then
     [[Simp_Method, Auto_Method, Blast_Method, Linarith_Method],
      [Meson_Method, Fastforce_Method, Force_Method, Presburger_Method]]
@@ -171,7 +171,7 @@
       [Metis_Method (SOME full_typesN, NONE),
        Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
        Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)])] @
-  (if smt_method then [[SMT_Method]] else [])
+  (if smt_proofs then [[SMT_Method]] else [])
 
 fun is_fact_chained ((_, (sc, _)), _) = sc = Chained
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Tue Jun 09 12:13:15 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Jun 10 15:55:41 2020 +0200
@@ -362,8 +362,8 @@
           val needs_full_types = is_typed_helper_used_in_atp_proof atp_proof
           val preferred_methss =
             (Metis_Method (NONE, NONE),
-             bunches_of_proof_methods try0 (smt_proofs <> SOME false) needs_full_types
-               (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN))
+             bunches_of_proof_methods try0 smt_proofs needs_full_types
+              (if atp_proof_prefers_lifting atp_proof then liftingN else hide_lamsN))
         in
           (used_facts, preferred_methss,
            fn preplay =>

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Tue Jun 09 12:13:15 2020 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Wed Jun 10 15:55:41 2020 +0200
@@ -200,10 +200,9 @@
         NONE =>
         let
           val _ = found_proof ();
-          val smt_method = smt_proofs <> SOME false
           val preferred_methss =
-            (if smt_method then SMT_Method else Metis_Method (NONE, NONE),
-             bunches_of_proof_methods try0 smt_method false liftingN)
+            (if smt_proofs then SMT_Method else Metis_Method (NONE, NONE),
+             bunches_of_proof_methods try0 smt_proofs false liftingN)
         in
           (preferred_methss,
            fn preplay =>
@@ -217,8 +216,7 @@
                val one_line_params = (preplay (), proof_banner mode name, subgoal, subgoal_count)
                val num_chained = length (#facts (Proof.goal state))
              in
-               proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained
-                 one_line_params
+               proof_text ctxt debug isar_proofs smt_proofs isar_params num_chained one_line_params
              end)
         end
       | SOME failure => ((Auto_Method (* dummy *), []), fn _ => string_of_atp_failure failure))