# HG changeset patch
# User desharna
# Date 1639830462 -3600
# Node ID 0b6f795d3b786bf84288f341d3a1892f11991ed7
# Parent  b350a1f2115dccc0ca878705b0dbacd43b238bee
proper filtering inf induction rules in Mirabelle

diff -r b350a1f2115d -r 0b6f795d3b78 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- 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
diff -r b350a1f2115d -r 0b6f795d3b78 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- 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 =
diff -r b350a1f2115d -r 0b6f795d3b78 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- 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,