--- a/src/Doc/Sledgehammer/document/root.tex Fri Jul 09 08:48:34 2021 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex Fri Jul 09 17:59:25 2021 +0200
@@ -961,6 +961,25 @@
\nopagebreak
{\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}
+
+\opdefault{induction\_rules}{string}{smart}
+Specifies whether induction rules should be considered as relevant facts.
+The following behaviors are available:
+\begin{enum}
+\item[\labelitemi] \textbf{\textit{include}:}
+Induction rules are considered by the relevance filter.
+
+\item[\labelitemi] \textbf{\textit{exclude}:}
+Induction rules are ignored by the relevance filter.
+
+\item[\labelitemi] \textbf{\textit{instantiated}:}
+Induction rules are instantiated based on the conjecture and then
+considered by the relevance filter.
+
+\item[\labelitemi] \textbf{\textit{smart}:}
+Same as \textit{include} if the prover supports higher-order logic;
+same as \textit{exclude} otherwise.
+\end{enum}
\end{enum}
@@ -980,9 +999,9 @@
defined using an equation $\const{c}~x_1~\ldots~x_n = t$ ($\lambda$-lifting).
\item[\labelitemi] \textbf{\textit{opaque\_lifting}:} Same as
-\textbf{\textit{lifting}}, except that the supercombinators are kept opaque,
-i.e. they are unspecified fresh constants. This effectively disables all
-reasoning under $\lambda$-abstractions.
+\textit{lifting}, except that the supercombinators are kept opaque,
+i.e. they are unspecified fresh constants. This effectively disables
+all reasoning under $\lambda$-abstractions.
\item[\labelitemi] \textbf{\textit{combs}:} Rewrite lambdas to the Curry
combinators (\comb{I}, \comb{K}, \comb{S}, \comb{B}, \comb{C}). Combinators
@@ -992,8 +1011,8 @@
resolution.
\item[\labelitemi] \textbf{\textit{opaque\_combs}:} Same as
-\textbf{\textit{combs}}, except that the combinators are kept opaque,
-i.e. without equational definitions.
+\textit{combs}, except that the combinators are kept opaque, i.e. without
+equational definitions.
\item[\labelitemi] \textbf{\textit{combs\_and\_lifting}:} Introduce a new
supercombinator \const{c} for each cluster of $\lambda$-abstractions and characterize it both using a
--- a/src/HOL/TPTP/MaSh_Export_Base.thy Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/TPTP/MaSh_Export_Base.thy Fri Jul 09 17:59:25 2021 +0200
@@ -15,7 +15,6 @@
lam_trans = lifting, timeout = 2, dont_preplay, minimize]
declare [[sledgehammer_fact_duplicates = true]]
-declare [[sledgehammer_instantiate_inducts = false]]
hide_fact (open) HOL.ext
--- a/src/HOL/TPTP/atp_theory_export.ML Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/TPTP/atp_theory_export.ML Fri Jul 09 17:59:25 2021 +0200
@@ -160,8 +160,8 @@
val mono = not (is_type_enc_polymorphic type_enc)
val facts =
- Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true false
- Keyword.empty_keywords [] [] css_table
+ Sledgehammer_Fact.all_facts (Proof_Context.init_global thy) true Keyword.empty_keywords [] []
+ css_table
|> sort (Sledgehammer_MaSh.crude_thm_ord ctxt o apply2 snd)
val problem =
facts
--- a/src/HOL/TPTP/mash_eval.ML Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/TPTP/mash_eval.ML Fri Jul 09 17:59:25 2021 +0200
@@ -36,9 +36,11 @@
fun print s = File.append report_path (s ^ "\n")
- val {provers, max_facts, slice, type_enc, lam_trans, timeout, ...} = default_params thy []
+ val {provers, max_facts, slice, type_enc, lam_trans, timeout, induction_rules, ...} =
+ default_params thy []
val prover = hd provers
val max_suggs = generous_max_suggestions (the max_facts)
+ val inst_inducts = induction_rules = SOME Instantiate
val method_of_file_name =
perhaps (try (unsuffix "_suggestions")) o List.last o space_explode "/"
@@ -53,7 +55,7 @@
val liness' = Ctr_Sugar_Util.transpose (map pad liness0)
val css = clasimpset_rule_table_of ctxt
- val facts = all_facts ctxt true false Keyword.empty_keywords [] [] css
+ val facts = all_facts ctxt true Keyword.empty_keywords [] [] css
val name_tabs = build_name_tables nickname_of_thm facts
fun with_index facts s = (find_index (curry (op =) s) facts + 1, s)
@@ -122,7 +124,7 @@
suggs
|> find_suggested_facts ctxt facts
|> map (fact_of_raw_fact #> nickify)
- |> maybe_instantiate_inducts ctxt hyp_ts concl_t
+ |> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t
|> take (the max_facts)
|> map fact_of_raw_fact
val ctxt = ctxt |> set_file_name method prob_dir_name
@@ -141,7 +143,6 @@
else
zeros
- val inst_inducts = Config.get ctxt instantiate_inducts
val options =
["prover = " ^ prover,
"max_facts = " ^ string_of_int (the max_facts),
--- a/src/HOL/TPTP/mash_export.ML Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/TPTP/mash_export.ML Fri Jul 09 17:59:25 2021 +0200
@@ -64,7 +64,7 @@
fun all_facts ctxt =
let val css = Sledgehammer_Fact.clasimpset_rule_table_of ctxt in
- Sledgehammer_Fact.all_facts ctxt true false Keyword.empty_keywords [] [] css
+ Sledgehammer_Fact.all_facts ctxt true Keyword.empty_keywords [] [] css
|> sort (crude_thm_ord ctxt o apply2 snd)
end
@@ -172,7 +172,7 @@
j mod step <> 0 orelse
Thm.legacy_get_kind th = "" orelse
null (the_list isar_deps) orelse
- is_blacklisted_or_something ctxt ho_atp (Thm.get_name_hint th)
+ is_blacklisted_or_something (Thm.get_name_hint th)
fun generate_isar_or_prover_commands ctxt prover params_opt (range, step) thys max_suggs file_name =
let
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Fri Jul 09 17:59:25 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}
@@ -245,8 +247,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
@@ -271,10 +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 inst_inducts = induction_rules = SOME Instantiate
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 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)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Fri Jul 09 17:59:25 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,6 +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 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"
@@ -278,10 +281,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 Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML Fri Jul 09 17:59:25 2021 +0200
@@ -18,27 +18,27 @@
del : (Facts.ref * Token.src list) list,
only : bool}
- val instantiate_inducts : bool Config.T
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 : 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 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 -> bool -> Keyword.keywords -> thm list -> thm 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;
structure Sledgehammer_Fact : SLEDGEHAMMER_FACT =
@@ -63,10 +63,6 @@
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)
-
val no_fact_override = {add = [], del = [], only = false}
fun needs_quoting keywords s =
@@ -188,11 +184,10 @@
end
(* FIXME: put other record thms here, or declare as "no_atp" *)
-fun multi_base_blacklist ctxt ho_atp =
+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"]
- |> not (ho_atp orelse Config.get ctxt instantiate_inducts) ? 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 +266,8 @@
is_that_fact th
end
-fun is_blacklisted_or_something ctxt ho_atp =
- let val blist = multi_base_blacklist ctxt ho_atp 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
@@ -426,18 +421,15 @@
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
- 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)
@@ -456,7 +448,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 keywords add_ths chained css =
let
val thy = Proof_Context.theory_of ctxt
val transfer = Global_Theory.transfer_theories thy
@@ -474,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 ctxt ho_atp
fun add_facts global foldx facts =
foldx (fn (name0, ths) => fn accum =>
@@ -535,7 +526,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 inst_inducts {add, del, only} keywords css chained hyp_ts
+ concl_t =
if only andalso null add then
[]
else
@@ -549,14 +541,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 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
+ |> inst_inducts ? instantiate_inducts ctxt hyp_ts concl_t
end
fun drop_duplicate_facts facts =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Fri Jul 09 17:59:25 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 facts =
- nearly_all_facts ctxt false 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML Fri Jul 09 17:59:25 2021 +0200
@@ -17,6 +17,9 @@
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,
@@ -29,6 +32,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,
@@ -101,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 =
@@ -115,6 +126,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 Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML Fri Jul 09 17:59:25 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 Fri Jul 09 08:48:34 2021 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML Fri Jul 09 17:59:25 2021 +0200
@@ -30,16 +30,16 @@
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
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 inst_inducts = induction_rules = SOME Instantiate
val facts =
- nearly_all_facts ctxt ho_atp 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