# HG changeset patch
# User blanchet
# Date 1643641763 -3600
# Node ID 30a619de7973e89ee805f081320d9e46b9f07cf1
# Parent  fcfd96a59625ca3db9c5b3526022a6d886adae23
use same default for FO and HO provers w.r.t. induction principles, based on evaluation -- this also simplifies the code

diff -r fcfd96a59625 -r 30a619de7973 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/Doc/Sledgehammer/document/root.tex	Mon Jan 31 16:09:23 2022 +0100
@@ -341,9 +341,9 @@
 The traditional relevance filter, \emph{MePo}
 (\underline{Me}ng--\underline{Pau}lson), assigns a score to every available
 fact (lemma, theorem, definition, or axiom) based upon how many constants that
-fact shares with the conjecture. This process iterates to include facts
+fact shares with the goal. This process iterates to include facts
 relevant to those just accepted. The constants are weighted to give unusual
-ones greater significance. MePo copes best when the conjecture contains some
+ones greater significance. MePo copes best when the goal contains some
 unusual constants; if all the constants are common, it is unable to
 discriminate among the hundreds of facts that are picked up. The filter is also
 memoryless: It has no information about how many times a particular fact has
@@ -922,23 +922,19 @@
 \nopagebreak
 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
 
-\opdefault{induction\_rules}{string}{smart}
+\opdefault{induction\_rules}{string}{exclude}
 Specifies whether induction rules should be considered as relevant facts.
 The following behaviors are available:
 \begin{enum}
-\item[\labelitemi] \textbf{\textit{include}:}
-Induction rules are considered by the relevance filter.
-
 \item[\labelitemi] \textbf{\textit{exclude}:}
 Induction rules are ignored by the relevance filter.
 
 \item[\labelitemi] \textbf{\textit{instantiate}:}
-Induction rules are instantiated based on the conjecture and then
+Induction rules are instantiated based on the goal and then
 considered by the relevance filter.
 
-\item[\labelitemi] \textbf{\textit{smart}:}
-Same as \textit{include} if the prover supports higher-order logic;
-same as \textit{exclude} otherwise.
+\item[\labelitemi] \textbf{\textit{include}:}
+Induction rules are considered by the relevance filter.
 \end{enum}
 \end{enum}
 
diff -r fcfd96a59625 -r 30a619de7973 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -23,8 +23,6 @@
 
   val short_string_of_sledgehammer_outcome : sledgehammer_outcome -> string
 
-  val induction_rules_for_prover : Proof.context -> string -> induction_rules option ->
-    induction_rules
   val play_one_line_proof : bool -> Time.time -> (string * stature) list -> Proof.state -> int ->
     proof_method * proof_method list list -> (string * stature) list * (proof_method * play_outcome)
   val string_of_factss : (string * fact list) list -> string
@@ -78,8 +76,6 @@
     |> the_default (SH_Unknown, "")
   end
 
-fun induction_rules_for_prover ctxt prover_name induction_rules =
-  the_default (if is_ho_atp ctxt prover_name then Include else Exclude) induction_rules
 
 fun is_metis_method (Metis_Method _) = true
   | is_metis_method _ = false
@@ -144,7 +140,7 @@
     val _ = spying spy (fn () => (state, subgoal, name, "Launched"))
     val max_facts = max_facts |> the_default (default_max_facts_of_prover ctxt name)
     val num_facts = length (snd facts) |> not only ? Integer.min max_facts
-    val induction_rules = induction_rules_for_prover ctxt name induction_rules
+    val induction_rules = the_default Exclude induction_rules
 
     val problem =
       {comment = comment, state = state, goal = goal, subgoal = subgoal,
diff -r fcfd96a59625 -r 30a619de7973 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jan 31 16:09:23 2022 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Jan 31 16:09:23 2022 +0100
@@ -17,8 +17,6 @@
   val atp_completish : int Config.T
   val atp_full_names : bool Config.T
 
-  val is_ho_atp : Proof.context -> string -> bool
-
   val run_atp : mode -> string -> prover
 end;
 
@@ -49,16 +47,6 @@
    names are enabled by default. *)
 val atp_full_names = Attrib.setup_config_bool \<^binding>\<open>sledgehammer_atp_full_names\<close> (K false)
 
-fun is_atp_of_format is_format ctxt name =
-  let val thy = Proof_Context.theory_of ctxt in
-    (case try (get_atp thy) name of
-      SOME config =>
-      exists (fn (_, ((_, format, _, _, _), _)) => is_format format) (#best_slices (config ()) ctxt)
-    | NONE => false)
-  end
-
-val is_ho_atp = is_atp_of_format is_format_higher_order
-
 fun choose_type_enc strictness best_type_enc format =
   the_default best_type_enc
   #> type_enc_of_string strictness