--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Dec 17 09:57:22 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sat Dec 18 13:27:42 2021 +0100
@@ -342,7 +342,9 @@
time_isa) = time_limit (Mirabelle.cpu_time (fn () =>
let
val ctxt = Proof.context_of state
- val inst_inducts = induction_rules = SOME Sledgehammer_Prover.Instantiate
+ val induction_rules =
+ Sledgehammer.induction_rules_for_prover ctxt prover_name induction_rules
+ val inst_inducts = induction_rules = Sledgehammer_Prover.Instantiate
val fact_override = Sledgehammer_Fact.no_fact_override
val {facts = chained_thms, goal, ...} = Proof.goal state
val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
@@ -350,11 +352,12 @@
chained_thms hyp_ts concl_t
val default_max_facts =
Sledgehammer_Prover_Minimize.default_max_facts_of_prover ctxt prover_name
+ val max_facts = the_default default_max_facts max_facts
val factss =
facts
- |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name
- (the_default default_max_facts max_facts)
- Sledgehammer_Fact.no_fact_override hyp_ts concl_t
+ |> Sledgehammer_MaSh.relevant_facts ctxt params prover_name max_facts fact_override
+ hyp_ts concl_t
+ |> map (apsnd (Sledgehammer_Prover.maybe_filter_out_induction_rules induction_rules))
val prover = get_prover ctxt prover_name params goal
val problem =
{comment = "", state = state', goal = goal, subgoal = i,
@@ -560,4 +563,4 @@
val () = Mirabelle.register_action "sledgehammer" make_action
-end
\ No newline at end of file
+end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Dec 17 09:57:22 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Sat Dec 18 13:27:42 2021 +0100
@@ -15,12 +15,15 @@
type play_outcome = Sledgehammer_Proof_Methods.play_outcome
type mode = Sledgehammer_Prover.mode
type params = Sledgehammer_Prover.params
+ type induction_rules = Sledgehammer_Prover.induction_rules
val someN : string
val noneN : string
val timeoutN : string
val unknownN : 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
@@ -50,6 +53,9 @@
val timeoutN = "timeout"
val unknownN = "unknown"
+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
+
val ordered_outcome_codes = [someN, unknownN, timeoutN, noneN]
fun max_outcome_code codes =
@@ -125,16 +131,14 @@
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 facts |> not only ? Integer.min max_facts
- val induction_rules =
- the_default (if is_ho_atp ctxt name then Include else Exclude) induction_rules
+ val induction_rules = induction_rules_for_prover ctxt name induction_rules
val problem =
{comment = comment, state = state, goal = goal, subgoal = subgoal,
subgoal_count = subgoal_count,
factss = factss
- |> map (apsnd ((induction_rules = Exclude
- ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false))
- #> take num_facts)),
+ (* We take num_facts because factss contain facts for the maximum of all called provers. *)
+ |> map (apsnd (take num_facts o maybe_filter_out_induction_rules induction_rules)),
found_proof = found_proof}
fun print_used_facts used_facts used_from =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Dec 17 09:57:22 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Sat Dec 18 13:27:42 2021 +0100
@@ -19,6 +19,7 @@
datatype induction_rules = Include | Exclude | Instantiate
val induction_rules_of_string : string -> induction_rules option
+ val maybe_filter_out_induction_rules : induction_rules -> fact list -> fact list
type params =
{debug : bool,
@@ -147,6 +148,10 @@
fun string_of_params (params : params) =
YXML.content_of (ML_Pretty.string_of_polyml (ML_system_pretty (params, 100)))
+fun maybe_filter_out_induction_rules induction_rules : fact list -> fact list =
+ induction_rules = Exclude ?
+ filter_out (fn ((_, (_, ATP_Problem_Generate.Induction)), _) => true | _ => false)
+
fun set_params_provers params provers =
{debug = #debug params,
verbose = #verbose params,