# 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>\sledgehammer_atp_full_names\ (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