--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue May 24 00:01:33 2011 +0200
@@ -383,8 +383,8 @@
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
prover_name
- val is_good_prop =
- Sledgehammer_Provers.is_good_prop_for_prover ctxt prover_name
+ val is_appropriate_prop =
+ Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt prover_name
val is_built_in_const =
Sledgehammer_Provers.is_built_in_const_for_prover ctxt prover_name
val relevance_fudge =
@@ -401,9 +401,9 @@
let
val facts =
Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant) is_good_prop
- is_built_in_const relevance_fudge relevance_override chained_ths
- hyp_ts concl_t
+ (the_default default_max_relevant max_relevant)
+ is_appropriate_prop is_built_in_const relevance_fudge
+ relevance_override chained_ths hyp_ts concl_t
val problem =
{state = st', goal = goal, subgoal = i,
subgoal_count = Sledgehammer_Util.subgoal_count st,
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue May 24 00:01:33 2011 +0200
@@ -118,8 +118,9 @@
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing
prover
- val is_good_prop =
- Sledgehammer_Provers.is_good_prop_for_prover ctxt default_prover
+ val is_appropriate_prop =
+ Sledgehammer_Provers.is_appropriate_prop_for_prover ctxt
+ default_prover
val is_built_in_const =
Sledgehammer_Provers.is_built_in_const_for_prover ctxt default_prover
val relevance_fudge =
@@ -130,9 +131,9 @@
val (_, hyp_ts, concl_t) = Sledgehammer_Util.strip_subgoal goal subgoal
val facts =
Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds
- (the_default default_max_relevant max_relevant) is_good_prop
- is_built_in_const relevance_fudge relevance_override facts hyp_ts
- concl_t
+ (the_default default_max_relevant max_relevant)
+ is_appropriate_prop is_built_in_const relevance_fudge
+ relevance_override facts hyp_ts concl_t
|> map (fst o fst)
val (found_facts, lost_facts) =
flat proofs |> sort_distinct string_ord
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue May 24 00:01:33 2011 +0200
@@ -785,9 +785,9 @@
(**** Predicates to detect unwanted facts (prolific or likely to cause
unsoundness) ****)
-fun is_theorem_bad_for_atps is_good_prop thm =
+fun is_theorem_bad_for_atps is_appropriate_prop thm =
let val t = prop_of thm in
- not (is_good_prop t) orelse is_formula_too_complex t orelse
+ not (is_appropriate_prop t) orelse is_formula_too_complex t orelse
exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse
exists_low_level_class_const t orelse is_metastrange_theorem thm orelse
is_that_fact thm
@@ -815,7 +815,7 @@
mk_fact_table normalize_simp_prop snd simps)
end
-fun all_facts ctxt reserved really_all is_good_prop add_ths chained_ths =
+fun all_facts ctxt reserved really_all is_appropriate_prop add_ths chained_ths =
let
val thy = Proof_Context.theory_of ctxt
val global_facts = Global_Theory.facts_of thy
@@ -869,8 +869,8 @@
pair 1
#> fold (fn th => fn (j, rest) =>
(j + 1,
- if is_theorem_bad_for_atps is_good_prop th andalso
- not (member Thm.eq_thm add_ths th) then
+ if not (member Thm.eq_thm add_ths th) andalso
+ is_theorem_bad_for_atps is_appropriate_prop th then
rest
else
(((fn () =>
@@ -903,9 +903,9 @@
fun external_frees t =
[] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst)
-fun relevant_facts ctxt (threshold0, threshold1) max_relevant is_good_prop
- is_built_in_const fudge (override as {add, only, ...})
- chained_ths hyp_ts concl_t =
+fun relevant_facts ctxt (threshold0, threshold1) max_relevant
+ is_appropriate_prop is_built_in_const fudge
+ (override as {add, only, ...}) chained_ths hyp_ts concl_t =
let
val thy = Proof_Context.theory_of ctxt
val decay = Math.pow ((1.0 - threshold1) / (1.0 - threshold0),
@@ -921,7 +921,7 @@
maps (map (fn ((name, loc), th) => ((K name, loc), (true, th)))
o fact_from_ref ctxt reserved chained_ths) add
else
- all_facts ctxt reserved false is_good_prop add_ths chained_ths)
+ all_facts ctxt reserved false is_appropriate_prop add_ths chained_ths)
|> Config.get ctxt instantiate_inducts
? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs)
|> rearrange_facts ctxt only
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue May 24 00:01:33 2011 +0200
@@ -76,7 +76,7 @@
val is_prover_installed : Proof.context -> string -> bool
val default_max_relevant_for_prover : Proof.context -> bool -> string -> int
val is_unit_equality : term -> bool
- val is_good_prop_for_prover : Proof.context -> string -> term -> bool
+ val is_appropriate_prop_for_prover : Proof.context -> string -> term -> bool
val is_built_in_const_for_prover :
Proof.context -> string -> string * typ -> term list -> bool * term list
val atp_relevance_fudge : relevance_fudge
@@ -168,7 +168,7 @@
T <> @{typ bool}
| is_unit_equality _ = false
-fun is_good_prop_for_prover ctxt name =
+fun is_appropriate_prop_for_prover ctxt name =
if is_unit_equational_atp ctxt name then is_unit_equality else K true
fun is_built_in_const_for_prover ctxt name =
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 24 00:01:33 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue May 24 00:01:33 2011 +0200
@@ -215,7 +215,7 @@
|> (if blocking then smart_par_list_map else map) (launch problem)
|> exists fst |> rpair state
end
- fun get_facts label is_good_prop relevance_fudge provers =
+ fun get_facts label is_appropriate_prop relevance_fudge provers =
let
val max_max_relevant =
case max_relevant of
@@ -228,9 +228,9 @@
val is_built_in_const =
is_built_in_const_for_prover ctxt (hd provers)
in
- relevant_facts ctxt relevance_thresholds max_max_relevant is_good_prop
- is_built_in_const relevance_fudge relevance_override
- chained_ths hyp_ts concl_t
+ relevant_facts ctxt relevance_thresholds max_max_relevant
+ is_appropriate_prop is_built_in_const relevance_fudge
+ relevance_override chained_ths hyp_ts concl_t
|> tap (fn facts =>
if debug then
label ^ plural_s (length provers) ^ ": " ^
@@ -244,10 +244,10 @@
else
())
end
- fun launch_atps label is_good_prop atps accum =
+ fun launch_atps label is_appropriate_prop atps accum =
if null atps then
accum
- else if not (is_good_prop concl_t) then
+ else if not (is_appropriate_prop concl_t) then
(if verbose orelse length atps = length provers then
"Goal outside the scope of " ^
space_implode " " (serial_commas "and" (map quote atps)) ^ "."
@@ -257,7 +257,7 @@
accum)
else
launch_provers state
- (get_facts label is_good_prop atp_relevance_fudge o K atps)
+ (get_facts label is_appropriate_prop atp_relevance_fudge o K atps)
(K (Untranslated_Fact o fst)) (K (K NONE)) atps
fun launch_smts accum =
if null smts then