--- 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)
--- 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
--- 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 =
--- 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
--- 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,
--- 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}
--- 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