# HG changeset patch # User blanchet # Date 1306188093 -7200 # Node ID 96f62b77748f95f8ffc0d1b1d33c1b19df817fee # Parent 40bf0173fbedad4961371a238f4335b154ab79e8 tuning -- the "appropriate" terminology is inspired from TPTP diff -r 40bf0173fbed -r 96f62b77748f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- 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, diff -r 40bf0173fbed -r 96f62b77748f src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- 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 diff -r 40bf0173fbed -r 96f62b77748f src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- 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 diff -r 40bf0173fbed -r 96f62b77748f src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- 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 = diff -r 40bf0173fbed -r 96f62b77748f src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- 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