# HG changeset patch # User nik # Date 1314706375 -7200 # Node ID eeba1eedf32d21ded409f161f23456aec7bd5c0d # Parent cfe7f4a68e5145e88dbfd3b875767be75c5c4f58 improved handling of induction rules in Sledgehammer diff -r cfe7f4a68e51 -r eeba1eedf32d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 30 14:12:55 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Tue Aug 30 14:12:55 2011 +0200 @@ -416,11 +416,12 @@ let val _ = if is_appropriate_prop concl_t then () else raise Fail "inappropriate" + val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover_name val facts = - Sledgehammer_Filter.nearly_all_facts ctxt relevance_override - chained_ths hyp_ts concl_t + Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp + relevance_override chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds + |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t diff -r cfe7f4a68e51 -r eeba1eedf32d src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML --- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 30 14:12:55 2011 +0200 +++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Tue Aug 30 14:12:55 2011 +0200 @@ -129,11 +129,12 @@ val relevance_override = {add = [], del = [], only = false} val subgoal = 1 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal subgoal + val is_ho_atp = Sledgehammer_Provers.is_ho_atp ctxt prover val facts = - Sledgehammer_Filter.nearly_all_facts ctxt relevance_override + Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override chained_ths hyp_ts concl_t |> filter (is_appropriate_prop o prop_of o snd) - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds + |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t diff -r cfe7f4a68e51 -r eeba1eedf32d src/HOL/TPTP/atp_export.ML --- a/src/HOL/TPTP/atp_export.ML Tue Aug 30 14:12:55 2011 +0200 +++ b/src/HOL/TPTP/atp_export.ML Tue Aug 30 14:12:55 2011 +0200 @@ -27,8 +27,9 @@ val fact_name_of = prefix fact_prefix o ascii_of fun facts_of thy = - Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) Symtab.empty - true [] [] + Sledgehammer_Filter.all_facts (Proof_Context.init_global thy) + false(*FIXME works only for first-order*) + Symtab.empty true [] [] |> filter (curry (op =) @{typ bool} o fastype_of o Object_Logic.atomize_term thy o prop_of o snd) diff -r cfe7f4a68e51 -r eeba1eedf32d src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 14:12:55 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 14:12:55 2011 +0200 @@ -55,7 +55,6 @@ val get_atp : theory -> string -> atp_config val supported_atps : theory -> string list val is_atp_installed : theory -> string -> bool - val is_ho_atp: string -> bool val refresh_systems_on_tptp : unit -> unit val setup : theory -> theory end; @@ -500,15 +499,6 @@ forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) end -fun is_ho_atp name = - let - val local_ho_atps = [leo2N, satallaxN] - val ho_atps = map (fn n => remote_prefix ^ n) local_ho_atps - in List.filter (fn n => n = name) ho_atps - |> List.null - |> not - end - fun refresh_systems_on_tptp () = Synchronized.change systems (fn _ => get_systems ()) diff -r cfe7f4a68e51 -r eeba1eedf32d src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 14:12:55 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 14:12:55 2011 +0200 @@ -892,9 +892,6 @@ else IConst (proxy_base |>> prefix const_prefix, T, T_args) | NONE => if s = tptp_choice then - (*this could be made neater by adding c_Eps as a proxy, - but we'd need to be able to "see" Hilbert_Choice.Eps - at this level in order to define fEps*) tweak_ho_quant tptp_choice T args else IConst (name, T, T_args)) | intro _ _ (IAbs (bound, tm)) = IAbs (bound, intro false [] tm) diff -r cfe7f4a68e51 -r eeba1eedf32d src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 30 14:12:55 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 30 14:12:55 2011 +0200 @@ -837,8 +837,8 @@ val is_chained = member Thm.eq_thm_prop chained_ths val clasimpset_table = clasimpset_rule_table_of ctxt fun locality_of_theorem global (name: string) th = - if (String.isSubstring ".induct" name) orelse(*FIXME: use structured name*) - (String.isSubstring ".inducts" name) then + if String.isSubstring ".induct" name orelse(*FIXME: use structured name*) + String.isSubstring ".inducts" name then Induction else if is_chained th then Chained diff -r cfe7f4a68e51 -r eeba1eedf32d src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 30 14:12:55 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 30 14:12:55 2011 +0200 @@ -83,6 +83,7 @@ val is_metis_prover : string -> bool val is_atp : theory -> string -> bool val is_smt_prover : Proof.context -> string -> bool + val is_ho_atp: Proof.context -> string -> bool val is_unit_equational_atp : Proof.context -> string -> bool val is_prover_supported : Proof.context -> string -> bool val is_prover_installed : Proof.context -> string -> bool @@ -91,7 +92,6 @@ 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 is_induction_fact: prover_fact -> bool val atp_relevance_fudge : relevance_fudge val smt_relevance_fudge : relevance_fudge val relevance_fudge_for_prover : Proof.context -> string -> relevance_fudge @@ -152,6 +152,19 @@ fun is_smt_prover ctxt name = member (op =) (SMT_Solver.available_solvers_of ctxt) name +fun is_ho_atp ctxt name = + let + val thy = Proof_Context.theory_of ctxt + in case try (get_atp thy) name of + SOME {best_slices, ...} => + exists (fn cfg => case cfg of + (_, (_, (_, THF _, _, _))) => true + | _ => false + ) + (best_slices ctxt) + | NONE => false + end + fun is_unit_equational_atp ctxt name = let val thy = Proof_Context.theory_of ctxt in case try (get_atp thy) name of @@ -330,11 +343,6 @@ type prover = params -> (string -> minimize_command) -> prover_problem -> prover_result -(* checking facts' locality *) - -fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true - | is_induction_fact _ = false - (* configuration attributes *) (* Empty string means create files in Isabelle's temporary files directory. *) diff -r cfe7f4a68e51 -r eeba1eedf32d src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 14:12:55 2011 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 14:12:55 2011 +0200 @@ -144,6 +144,9 @@ get_prover ctxt mode name params minimize_command problem |> minimize ctxt mode name params problem +fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true + | is_induction_fact _ = false + fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing, timeout, expect, ...}) mode minimize_command only @@ -161,12 +164,11 @@ prover_description ctxt params name num_facts subgoal subgoal_count goal val problem = let - val filter_induction = - List.filter (fn fact => - not (Sledgehammer_Provers.is_induction_fact fact)) + val filter_induction = filter_out is_induction_fact in {state = state, goal = goal, subgoal = subgoal, subgoal_count = subgoal_count, facts = - ((ATP_Systems.is_ho_atp name |> not) ? filter_induction) facts + ((Sledgehammer_Provers.is_ho_atp ctxt name |> not) ? filter_induction) + facts |> take num_facts, smt_filter = smt_filter} end @@ -267,12 +269,10 @@ val {facts = chained_ths, goal, ...} = Proof.goal state val chained_ths = chained_ths |> normalize_chained_theorems val (_, hyp_ts, concl_t) = strip_subgoal ctxt goal i - val targetting_ho_provers = - List.foldr (fn (name, so_far) => (ATP_Systems.is_ho_atp name) orelse - so_far) - false provers - val facts = nearly_all_facts ctxt targetting_ho_provers relevance_override - chained_ths hyp_ts concl_t val _ = () |> not blocking ? kill_provers + val is_ho_atp = exists (Sledgehammer_Provers.is_ho_atp ctxt) provers + val facts = nearly_all_facts ctxt is_ho_atp relevance_override + chained_ths hyp_ts concl_t + val _ = () |> not blocking ? kill_provers val _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") | NONE => () @@ -323,7 +323,7 @@ |> (case is_appropriate_prop of SOME is_app => filter (is_app o prop_of o snd) | NONE => I) - |> relevant_facts ctxt targetting_ho_provers relevance_thresholds + |> relevant_facts ctxt is_ho_atp relevance_thresholds max_max_relevant is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t |> tap (fn facts => diff -r cfe7f4a68e51 -r eeba1eedf32d src/HOL/ex/sledgehammer_tactics.ML --- a/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 30 14:12:55 2011 +0200 +++ b/src/HOL/ex/sledgehammer_tactics.ML Tue Aug 30 14:12:55 2011 +0200 @@ -37,10 +37,13 @@ val relevance_fudge = Sledgehammer_Provers.relevance_fudge_for_prover ctxt name val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal i + val is_ho_atp = + exists (Sledgehammer_Provers.is_ho_atp ctxt) + provers(*FIXME: duplicated from sledgehammer_run.ML*) val facts = - Sledgehammer_Filter.nearly_all_facts ctxt relevance_override chained_ths - hyp_ts concl_t - |> Sledgehammer_Filter.relevant_facts ctxt relevance_thresholds + Sledgehammer_Filter.nearly_all_facts ctxt is_ho_atp relevance_override + chained_ths hyp_ts concl_t + |> Sledgehammer_Filter.relevant_facts ctxt is_ho_atp relevance_thresholds (the_default default_max_relevant max_relevant) is_built_in_const relevance_fudge relevance_override chained_ths hyp_ts concl_t val problem =