# HG changeset patch
# User desharna
# Date 1625750730 -7200
# Node ID 9231ea46e041434b1cbb32dd4aff8978320e628c
# Parent  d593d18a7a9250843b4d1988f22c1814795d5359
promoted "sledgehammer_instantiate_inducts" to proper option "induction_rules"

diff -r d593d18a7a92 -r 9231ea46e041 src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 08 15:25:58 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 08 15:25:30 2021 +0200
@@ -245,8 +245,8 @@
     cat_lines (map (fn (filter, facts) =>
       (if filter = "" then "" else quote filter ^ ": ") ^ string_of_facts facts) factss)
 
-fun run_sledgehammer (params as {verbose, spy, provers, max_facts, ...}) mode writeln_result i
-    (fact_override as {only, ...}) state =
+fun run_sledgehammer (params as {verbose, spy, provers, induction_rules, max_facts, ...}) mode
+    writeln_result i (fact_override as {only, ...}) state =
   if null provers then
     error "No prover is set"
   else
@@ -272,9 +272,11 @@
         val {facts = chained, goal, ...} = Proof.goal state
         val (_, hyp_ts, concl_t) = strip_subgoal goal i ctxt
         val ho_atp = exists (is_ho_atp ctxt) provers
+        val induction_rules = the_default (if ho_atp then Instantiate else Exclude) induction_rules
         val css = clasimpset_rule_table_of ctxt
         val all_facts =
-          nearly_all_facts ctxt ho_atp fact_override keywords css chained hyp_ts concl_t
+          nearly_all_facts ctxt induction_rules fact_override keywords css chained hyp_ts
+            concl_t
         val _ =
           (case find_first (not o is_prover_supported ctxt) provers of
             SOME name => error ("No such prover: " ^ name)
diff -r d593d18a7a92 -r 9231ea46e041 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jul 08 15:25:58 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jul 08 15:25:30 2021 +0200
@@ -260,6 +260,7 @@
     val fact_filter =
       lookup_option lookup_string "fact_filter"
       |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf)
+    val induction_rules = lookup_option (the o induction_rules_of_string) "induction_rules"
     val max_facts = lookup_option lookup_int "max_facts"
     val fact_thresholds = lookup_real_pair "fact_thresholds"
     val max_mono_iters = lookup_option lookup_int "max_mono_iters"
@@ -278,10 +279,11 @@
     {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
      type_enc = type_enc, strict = strict, lam_trans = lam_trans,
      uncurried_aliases = uncurried_aliases, learn = learn, fact_filter = fact_filter,
-     max_facts = max_facts, fact_thresholds = fact_thresholds, max_mono_iters = max_mono_iters,
-     max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
-     compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = slice, minimize = minimize,
-     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     induction_rules = induction_rules, max_facts = max_facts, fact_thresholds = fact_thresholds,
+     max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
+     isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
+     slice = slice, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
+     expect = expect}
   end
 
 fun get_params mode = extract_params mode o default_raw_params mode
diff -r d593d18a7a92 -r 9231ea46e041 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 08 15:25:58 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 08 15:25:30 2021 +0200
@@ -18,27 +18,30 @@
      del : (Facts.ref * Token.src list) list,
      only : bool}
 
-  val instantiate_inducts : bool Config.T
+  datatype induction_rules = Include | Exclude | Instantiate
+  val induction_rules_of_string : string -> induction_rules option
+
   val no_fact_override : fact_override
 
   val fact_of_ref : Proof.context -> Keyword.keywords -> thm list -> status Termtab.table ->
     Facts.ref * Token.src list -> ((string * stature) * thm) list
   val cartouche_thm : Proof.context -> thm -> string
-  val is_blacklisted_or_something : Proof.context -> bool -> string -> bool
+  val is_blacklisted_or_something : induction_rules -> string -> bool
   val clasimpset_rule_table_of : Proof.context -> status Termtab.table
   val build_name_tables : (thm -> string) -> ('a * thm) list ->
     string Symtab.table * string Symtab.table
   val fact_distinct : (term * term -> bool) -> ('a * thm) list -> ('a * thm) list
-  val maybe_instantiate_inducts : Proof.context -> term list -> term ->
+  val maybe_instantiate_inducts : Proof.context -> induction_rules -> term list -> term ->
     (((unit -> string) * 'a) * thm) list -> (((unit -> string) * 'a) * thm) list
   val fact_of_raw_fact : raw_fact -> fact
   val is_useful_unnamed_local_fact : Proof.context -> thm -> bool
 
-  val all_facts : Proof.context -> bool -> bool -> Keyword.keywords -> thm list -> thm list ->
-    status Termtab.table -> raw_fact list
-  val nearly_all_facts : Proof.context -> bool -> fact_override -> Keyword.keywords ->
-    status Termtab.table -> thm list -> term list -> term -> raw_fact list
+  val all_facts : Proof.context -> bool -> induction_rules -> Keyword.keywords ->
+    thm list -> thm list -> status Termtab.table -> raw_fact list
+  val nearly_all_facts : Proof.context -> induction_rules -> fact_override ->
+    Keyword.keywords -> status Termtab.table -> thm list -> term list -> term -> raw_fact list
   val drop_duplicate_facts : raw_fact list -> raw_fact list
+
 end;
 
 structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
@@ -63,9 +66,12 @@
 val max_facts_for_complex_check = 25000
 val max_simps_for_clasimpset = 10000
 
-(* experimental feature *)
-val instantiate_inducts =
-  Attrib.setup_config_bool \<^binding>\<open>sledgehammer_instantiate_inducts\<close> (K false)
+datatype induction_rules = Include | Exclude | Instantiate
+
+fun induction_rules_of_string "include" = SOME Include
+  | induction_rules_of_string "exclude" = SOME Exclude
+  | induction_rules_of_string "instantiate" = SOME Instantiate
+  | induction_rules_of_string _ = NONE
 
 val no_fact_override = {add = [], del = [], only = false}
 
@@ -188,11 +194,11 @@
   end
 
 (* FIXME: put other record thms here, or declare as "no_atp" *)
-fun multi_base_blacklist ctxt ho_atp =
+fun multi_base_blacklist induction_rules =
   ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "ext_cases", "eq.simps",
    "eq.refl", "nchotomy", "case_cong", "case_cong_weak", "nat_of_char_simps", "nibble.simps",
    "nibble.distinct"]
-  |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"]
+  |> induction_rules = Exclude ? append ["induct", "inducts"]
   |> map (prefix Long_Name.separator)
 
 (* The maximum apply depth of any "metis" call in "Metis_Examples" (back in 2007) was 11. *)
@@ -271,8 +277,8 @@
     is_that_fact th
   end
 
-fun is_blacklisted_or_something ctxt ho_atp =
-  let val blist = multi_base_blacklist ctxt ho_atp in
+fun is_blacklisted_or_something induction_rules =
+  let val blist = multi_base_blacklist induction_rules in
     fn name => is_package_def name orelse exists (fn s => String.isSuffix s name) blist
   end
 
@@ -426,8 +432,8 @@
 fun external_frees t =
   [] |> Term.add_frees t |> filter_out (Name.is_internal o fst)
 
-fun maybe_instantiate_inducts ctxt hyp_ts concl_t =
-  if Config.get ctxt instantiate_inducts then
+fun maybe_instantiate_inducts ctxt induction_rules hyp_ts concl_t =
+  if induction_rules = Instantiate then
     let
       val ind_stmt =
         (hyp_ts |> filter_out (null o external_frees), concl_t)
@@ -456,7 +462,7 @@
       not (member (op aconv) named_locals (normalize_eq (Thm.prop_of th)))
   end
 
-fun all_facts ctxt generous ho_atp keywords add_ths chained css =
+fun all_facts ctxt generous induction_rules keywords add_ths chained css =
   let
     val thy = Proof_Context.theory_of ctxt
     val transfer = Global_Theory.transfer_theories thy
@@ -474,7 +480,7 @@
       |> map (pair "" o single)
 
     val full_space = Name_Space.merge (Facts.space_of global_facts, Facts.space_of local_facts)
-    val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
+    val is_blacklisted_or_something = is_blacklisted_or_something induction_rules
 
     fun add_facts global foldx facts =
       foldx (fn (name0, ths) => fn accum =>
@@ -535,7 +541,8 @@
     |> op @
   end
 
-fun nearly_all_facts ctxt ho_atp {add, del, only} keywords css chained hyp_ts concl_t =
+fun nearly_all_facts ctxt induction_rules {add, del, only} keywords css chained hyp_ts
+    concl_t =
   if only andalso null add then
     []
   else
@@ -549,14 +556,14 @@
          let
            val (add, del) = apply2 (Attrib.eval_thms ctxt) (add, del)
            val facts =
-             all_facts ctxt false ho_atp keywords add chained css
+             all_facts ctxt false induction_rules keywords add chained css
              |> filter_out ((member Thm.eq_thm_prop del orf
                (Named_Theorems.member ctxt \<^named_theorems>\<open>no_atp\<close> andf
                  not o member Thm.eq_thm_prop add)) o snd)
          in
            facts
          end)
-      |> maybe_instantiate_inducts ctxt hyp_ts concl_t
+      |> maybe_instantiate_inducts ctxt induction_rules hyp_ts concl_t
     end
 
 fun drop_duplicate_facts facts =
diff -r d593d18a7a92 -r 9231ea46e041 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 08 15:25:58 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 08 15:25:30 2021 +0200
@@ -1481,12 +1481,13 @@
       end)
   end
 
-fun mash_learn ctxt (params as {provers, timeout, ...}) fact_override chained run_prover =
+fun mash_learn ctxt (params as {provers, timeout, induction_rules, ...}) fact_override chained run_prover =
   let
     val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt
-    val ctxt = ctxt |> Config.put instantiate_inducts false
+    val induction_rules = the_default Exclude induction_rules
     val facts =
-      nearly_all_facts ctxt false fact_override Keyword.empty_keywords css chained [] \<^prop>\<open>True\<close>
+      nearly_all_facts ctxt induction_rules fact_override Keyword.empty_keywords css chained []
+        \<^prop>\<open>True\<close>
       |> sort (crude_thm_ord ctxt o apply2 snd o swap)
     val num_facts = length facts
     val prover = hd provers
diff -r d593d18a7a92 -r 9231ea46e041 src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jul 08 15:25:58 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jul 08 15:25:30 2021 +0200
@@ -12,6 +12,7 @@
   type stature = ATP_Problem_Generate.stature
   type type_enc = ATP_Problem_Generate.type_enc
   type fact = Sledgehammer_Fact.fact
+  type induction_rules = Sledgehammer_Fact.induction_rules
   type proof_method = Sledgehammer_Proof_Methods.proof_method
   type play_outcome = Sledgehammer_Proof_Methods.play_outcome
 
@@ -29,6 +30,7 @@
      uncurried_aliases : bool option,
      learn : bool,
      fact_filter : string option,
+     induction_rules : induction_rules option,
      max_facts : int option,
      fact_thresholds : real * real,
      max_mono_iters : int option,
@@ -115,6 +117,7 @@
    uncurried_aliases : bool option,
    learn : bool,
    fact_filter : string option,
+   induction_rules : induction_rules option,
    max_facts : int option,
    fact_thresholds : real * real,
    max_mono_iters : int option,
diff -r d593d18a7a92 -r 9231ea46e041 src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jul 08 15:25:58 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML	Thu Jul 08 15:25:30 2021 +0200
@@ -80,7 +80,7 @@
 
 fun test_facts ({debug, verbose, overlord, spy, provers, max_mono_iters, max_new_mono_instances,
       type_enc, strict, lam_trans, uncurried_aliases, isar_proofs, compress, try0, smt_proofs,
-      minimize, preplay_timeout, ...} : params)
+      minimize, preplay_timeout, induction_rules, ...} : params)
     silent (prover : prover) timeout i n state goal facts =
   let
     val _ = print silent (fn () => "Testing " ^ n_facts (map fst facts) ^
@@ -91,11 +91,11 @@
       {debug = debug, verbose = verbose, overlord = overlord, spy = spy, provers = provers,
        type_enc = type_enc, strict = strict, lam_trans = lam_trans,
        uncurried_aliases = uncurried_aliases, learn = false, fact_filter = NONE,
-       max_facts = SOME (length facts), fact_thresholds = (1.01, 1.01),
-       max_mono_iters = max_mono_iters, max_new_mono_instances = max_new_mono_instances,
-       isar_proofs = isar_proofs, compress = compress, try0 = try0, smt_proofs = smt_proofs,
-       slice = false, minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout,
-       expect = ""}
+       induction_rules = induction_rules, max_facts = SOME (length facts),
+       fact_thresholds = (1.01, 1.01), max_mono_iters = max_mono_iters,
+       max_new_mono_instances = max_new_mono_instances, isar_proofs = isar_proofs,
+       compress = compress, try0 = try0, smt_proofs = smt_proofs, slice = false,
+       minimize = minimize, timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
     val problem =
       {comment = "", state = state, goal = goal, subgoal = i, subgoal_count = n,
        factss = [("", facts)], found_proof = I}
diff -r d593d18a7a92 -r 9231ea46e041 src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Thu Jul 08 15:25:58 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Thu Jul 08 15:25:30 2021 +0200
@@ -30,7 +30,7 @@
   let
     val thy = Proof_Context.theory_of ctxt
     val mode = Normal
-    val params as {provers, max_facts, ...} = default_params thy override_params
+    val params as {provers, induction_rules, max_facts, ...} = default_params thy override_params
     val name = hd provers
     val prover = get_prover ctxt mode name
     val default_max_facts = default_max_facts_of_prover ctxt name
@@ -38,8 +38,9 @@
     val ho_atp = exists (is_ho_atp ctxt) provers
     val keywords = Thy_Header.get_keywords' ctxt
     val css_table = clasimpset_rule_table_of ctxt
+    val induction_rules = the_default (if ho_atp then Instantiate else Exclude) induction_rules
     val facts =
-      nearly_all_facts ctxt ho_atp fact_override keywords css_table chained hyp_ts concl_t
+      nearly_all_facts ctxt induction_rules fact_override keywords css_table chained hyp_ts concl_t
       |> relevant_facts ctxt params name (the_default default_max_facts max_facts) fact_override
         hyp_ts concl_t
       |> hd |> snd