# HG changeset patch
# User desharna
# Date 1625757781 -7200
# Node ID f58108b7a60cf3bede8ebd235936391fea1121b0
# Parent  9231ea46e041434b1cbb32dd4aff8978320e628c
refactored Sledgehammer option "induction_rules"

diff -r 9231ea46e041 -r f58108b7a60c src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 08 15:25:30 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Jul 08 17:23:01 2021 +0200
@@ -118,7 +118,7 @@
          (meth, play)))
 
 fun launch_prover (params as {debug, verbose, spy, max_facts, minimize, timeout, preplay_timeout,
-      expect, ...}) mode writeln_result only learn
+      expect, induction_rules, ...}) mode writeln_result only learn
     {comment, state, goal, subgoal, subgoal_count, factss as (_, facts) :: _, found_proof} name =
   let
     val ctxt = Proof.context_of state
@@ -127,12 +127,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 problem =
       {comment = comment, state = state, goal = goal, subgoal = subgoal,
        subgoal_count = subgoal_count,
        factss = factss
-       |> map (apsnd ((not (is_ho_atp ctxt name)
+       |> map (apsnd ((induction_rules = Exclude
            ? filter_out (fn ((_, (_, Induction)), _) => true | _ => false))
          #> take num_facts)),
        found_proof = found_proof}
@@ -271,12 +273,10 @@
         val keywords = Thy_Header.get_keywords' ctxt
         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 inst_inducts = induction_rules = SOME Instantiate
         val css = clasimpset_rule_table_of ctxt
         val all_facts =
-          nearly_all_facts ctxt induction_rules fact_override keywords css chained hyp_ts
-            concl_t
+          nearly_all_facts ctxt inst_inducts 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 9231ea46e041 -r f58108b7a60c src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jul 08 15:25:30 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Thu Jul 08 17:23:01 2021 +0200
@@ -62,6 +62,7 @@
    ("uncurried_aliases", "smart"),
    ("learn", "true"),
    ("fact_filter", "smart"),
+   ("induction_rules", "smart"),
    ("max_facts", "smart"),
    ("fact_thresholds", "0.45 0.85"),
    ("max_mono_iters", "smart"),
@@ -260,7 +261,8 @@
     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 induction_rules =
+      lookup_option (the o induction_rules_of_string o lookup_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"
diff -r 9231ea46e041 -r f58108b7a60c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 08 15:25:30 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Jul 08 17:23:01 2021 +0200
@@ -18,28 +18,25 @@
      del : (Facts.ref * Token.src list) list,
      only : bool}
 
-  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 : induction_rules -> string -> bool
+  val is_blacklisted_or_something : 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 -> induction_rules -> term list -> term ->
+  val instantiate_inducts : Proof.context -> 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 -> 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 all_facts : Proof.context -> 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 drop_duplicate_facts : raw_fact list -> raw_fact list
 
 end;
@@ -66,13 +63,6 @@
 val max_facts_for_complex_check = 25000
 val max_simps_for_clasimpset = 10000
 
-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}
 
 fun needs_quoting keywords s =
@@ -194,11 +184,10 @@
   end
 
 (* FIXME: put other record thms here, or declare as "no_atp" *)
-fun multi_base_blacklist induction_rules =
+val multi_base_blacklist =
   ["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"]
-  |> 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. *)
@@ -277,8 +266,8 @@
     is_that_fact th
   end
 
-fun is_blacklisted_or_something induction_rules =
-  let val blist = multi_base_blacklist induction_rules in
+val is_blacklisted_or_something =
+  let val blist = multi_base_blacklist in
     fn name => is_package_def name orelse exists (fn s => String.isSuffix s name) blist
   end
 
@@ -432,18 +421,15 @@
 fun external_frees t =
   [] |> Term.add_frees t |> filter_out (Name.is_internal o fst)
 
-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)
-        |> Logic.list_implies |> Object_Logic.atomize_term ctxt
-      val ind_stmt_xs = external_frees ind_stmt
-    in
-      maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
-    end
-  else
-    I
+fun instantiate_inducts ctxt hyp_ts concl_t =
+  let
+    val ind_stmt =
+      (hyp_ts |> filter_out (null o external_frees), concl_t)
+      |> Logic.list_implies |> Object_Logic.atomize_term ctxt
+    val ind_stmt_xs = external_frees ind_stmt
+  in
+    maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
+  end
 
 fun fact_of_raw_fact ((name, stature), th) = ((name (), stature), th)
 
@@ -462,7 +448,7 @@
       not (member (op aconv) named_locals (normalize_eq (Thm.prop_of th)))
   end
 
-fun all_facts ctxt generous induction_rules keywords add_ths chained css =
+fun all_facts ctxt generous keywords add_ths chained css =
   let
     val thy = Proof_Context.theory_of ctxt
     val transfer = Global_Theory.transfer_theories thy
@@ -480,7 +466,6 @@
       |> 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 induction_rules
 
     fun add_facts global foldx facts =
       foldx (fn (name0, ths) => fn accum =>
@@ -541,7 +526,7 @@
     |> op @
   end
 
-fun nearly_all_facts ctxt induction_rules {add, del, only} keywords css chained hyp_ts
+fun nearly_all_facts ctxt inst_inducts {add, del, only} keywords css chained hyp_ts
     concl_t =
   if only andalso null add then
     []
@@ -556,14 +541,14 @@
          let
            val (add, del) = apply2 (Attrib.eval_thms ctxt) (add, del)
            val facts =
-             all_facts ctxt false induction_rules keywords add chained css
+             all_facts ctxt false 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 induction_rules hyp_ts concl_t
+      |> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t
     end
 
 fun drop_duplicate_facts facts =
diff -r 9231ea46e041 -r f58108b7a60c src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 08 15:25:30 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Thu Jul 08 17:23:01 2021 +0200
@@ -1481,13 +1481,13 @@
       end)
   end
 
-fun mash_learn ctxt (params as {provers, timeout, induction_rules, ...}) 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 induction_rules = the_default Exclude induction_rules
     val facts =
-      nearly_all_facts ctxt induction_rules fact_override Keyword.empty_keywords css chained []
-        \<^prop>\<open>True\<close>
+      nearly_all_facts ctxt (induction_rules = SOME Instantiate) 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 9231ea46e041 -r f58108b7a60c src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jul 08 15:25:30 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML	Thu Jul 08 17:23:01 2021 +0200
@@ -12,12 +12,14 @@
   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
 
   datatype mode = Auto_Try | Try | Normal | Minimize | MaSh
 
+  datatype induction_rules = Include | Exclude | Instantiate
+  val induction_rules_of_string : string -> induction_rules option
+
   type params =
     {debug : bool,
      verbose : bool,
@@ -103,6 +105,13 @@
   | str_of_mode Minimize = "Minimize"
   | str_of_mode MaSh = "MaSh"
 
+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 is_atp = member (op =) o supported_atps
 
 type params =
diff -r 9231ea46e041 -r f58108b7a60c src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Thu Jul 08 15:25:30 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML	Thu Jul 08 17:23:01 2021 +0200
@@ -35,12 +35,11 @@
     val prover = get_prover ctxt mode name
     val default_max_facts = default_max_facts_of_prover ctxt name
     val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal goal i ctxt
-    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 inst_inducts = induction_rules = SOME Instantiate
     val facts =
-      nearly_all_facts ctxt induction_rules fact_override keywords css_table chained hyp_ts concl_t
+      nearly_all_facts ctxt inst_inducts 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