# HG changeset patch # User nik # Date 1314706375 -7200 # Node ID cfe7f4a68e5145e88dbfd3b875767be75c5c4f58 # Parent 08ad27488983fb374be3c7b4934d54a5426d2256 added generation of induction rules diff -r 08ad27488983 -r cfe7f4a68e51 src/HOL/Tools/ATP/atp_systems.ML --- a/src/HOL/Tools/ATP/atp_systems.ML Mon Aug 29 13:50:47 2011 -0700 +++ b/src/HOL/Tools/ATP/atp_systems.ML Tue Aug 30 14:12:55 2011 +0200 @@ -55,6 +55,7 @@ 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; @@ -499,6 +500,15 @@ 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 08ad27488983 -r cfe7f4a68e51 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 29 13:50:47 2011 -0700 +++ b/src/HOL/Tools/ATP/atp_translate.ML Tue Aug 30 14:12:55 2011 +0200 @@ -16,8 +16,8 @@ type 'a problem = 'a ATP_Problem.problem datatype locality = - General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | - Chained + General | Helper | Induction | Extensionality | Intro | Elim | Simp | + Local | Assum | Chained datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic @@ -527,8 +527,8 @@ in (IAbs ((name, T), tm), union (op =) atomic_Ts (atyps_of T)) end datatype locality = - General | Helper | Extensionality | Intro | Elim | Simp | Local | Assum | - Chained + General | Helper | Induction | Extensionality | Intro | Elim | Simp | + Local | Assum | Chained datatype order = First_Order | Higher_Order datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic diff -r 08ad27488983 -r cfe7f4a68e51 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Aug 29 13:50:47 2011 -0700 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Tue Aug 30 14:12:55 2011 +0200 @@ -46,13 +46,13 @@ Proof.context -> unit Symtab.table -> thm list -> Facts.ref * Attrib.src list -> ((string * locality) * thm) list val all_facts : - Proof.context -> 'a Symtab.table -> bool -> thm list -> thm list + Proof.context -> bool -> 'a Symtab.table -> bool -> thm list -> thm list -> (((unit -> string) * locality) * thm) list val nearly_all_facts : - Proof.context -> relevance_override -> thm list -> term list -> term + Proof.context -> bool -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * locality) * thm) list val relevant_facts : - Proof.context -> real * real -> int + Proof.context -> bool -> real * real -> int -> (string * typ -> term list -> bool * term list) -> relevance_fudge -> relevance_override -> thm list -> term list -> term -> (((unit -> string) * locality) * thm) list @@ -586,7 +586,7 @@ facts are included. *) val special_fact_index = 75 -fun relevance_filter ctxt threshold0 decay max_relevant is_built_in_const +fun relevance_filter ctxt ho_atp threshold0 decay max_relevant is_built_in_const (fudge as {threshold_divisor, ridiculous_threshold, ...}) ({add, del, ...} : relevance_override) facts chained_ts hyp_ts concl_t = let @@ -729,14 +729,15 @@ (fold (Termtab.update o `(prop_of o snd)) xs Termtab.empty) [] (* FIXME: put other record thms here, or declare as "no_atp" *) -fun multi_base_blacklist ctxt = +fun multi_base_blacklist ctxt ho_atp = ["defs", "select_defs", "update_defs", "split", "splits", "split_asm", "cases", "ext_cases", "eq.simps", "eq.refl", "nchotomy", "case_cong", "weak_case_cong"] - |> not (Config.get ctxt instantiate_inducts) ? append ["induct", "inducts"] + |> not (ho_atp orelse (Config.get ctxt instantiate_inducts)) ? + append ["induct", "inducts"] |> map (prefix ".") -val max_lambda_nesting = 3 +val max_lambda_nesting = 3 (*only applies if not ho_atp*) fun term_has_too_many_lambdas max (t1 $ t2) = exists (term_has_too_many_lambdas max) [t1, t2] @@ -746,11 +747,12 @@ (* Don't count nested lambdas at the level of formulas, since they are quantifiers. *) -fun formula_has_too_many_lambdas Ts (Abs (_, T, t)) = - formula_has_too_many_lambdas (T :: Ts) t - | formula_has_too_many_lambdas Ts t = +fun formula_has_too_many_lambdas true _ _ = false (*i.e. ho_atp*) + | formula_has_too_many_lambdas _ Ts (Abs (_, T, t)) = + formula_has_too_many_lambdas false (T :: Ts) t + | formula_has_too_many_lambdas _ Ts t = if member (op =) [HOLogic.boolT, propT] (fastype_of1 (Ts, t)) then - exists (formula_has_too_many_lambdas Ts) (#2 (strip_comb t)) + exists (formula_has_too_many_lambdas false Ts) (#2 (strip_comb t)) else term_has_too_many_lambdas max_lambda_nesting t @@ -762,8 +764,8 @@ | apply_depth (Abs (_, _, t)) = apply_depth t | apply_depth _ = 0 -fun is_formula_too_complex t = - apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas [] t +fun is_formula_too_complex ho_atp t = + apply_depth t > max_apply_depth orelse formula_has_too_many_lambdas ho_atp [] t (* FIXME: Extend to "Meson" and "Metis" *) val exists_sledgehammer_const = @@ -791,11 +793,11 @@ (**** Predicates to detect unwanted facts (prolific or likely to cause unsoundness) ****) -fun is_theorem_bad_for_atps exporter thm = +fun is_theorem_bad_for_atps ho_atp exporter thm = is_metastrange_theorem thm orelse (not exporter andalso let val t = prop_of thm in - is_formula_too_complex t orelse exists_type type_has_top_sort t orelse + is_formula_too_complex ho_atp t orelse exists_type type_has_top_sort t orelse exists_sledgehammer_const t orelse exists_low_level_class_const t orelse is_that_fact thm end) @@ -824,7 +826,7 @@ |> add Simp normalize_simp_prop snd simps end -fun all_facts ctxt reserved exporter add_ths chained_ths = +fun all_facts ctxt ho_atp reserved exporter add_ths chained_ths = let val thy = Proof_Context.theory_of ctxt val global_facts = Global_Theory.facts_of thy @@ -834,16 +836,18 @@ fun is_assum th = exists (fn ct => prop_of th aconv term_of ct) assms val is_chained = member Thm.eq_thm_prop chained_ths val clasimpset_table = clasimpset_rule_table_of ctxt - fun locality_of_theorem global th = - if is_chained th then + fun locality_of_theorem global (name: string) th = + if (String.isSubstring ".induct" name) orelse(*FIXME: use structured name*) + (String.isSubstring ".inducts" name) then + Induction + else if is_chained th then Chained else if global then case Termtab.lookup clasimpset_table (prop_of th) of SOME loc => loc | NONE => if Thm.eq_thm_prop (th, @{thm ext}) then Extensionality else General - else - if is_assum th then Assum else Local + else if is_assum th then Assum else Local fun is_good_unnamed_local th = not (Thm.has_name_hint th) andalso forall (fn (_, ths) => not (member Thm.eq_thm_prop ths th)) named_locals @@ -860,7 +864,7 @@ (not (Config.get ctxt ignore_no_atp) andalso is_package_def name0) orelse exists (fn s => String.isSuffix s name0) - (multi_base_blacklist ctxt) orelse + (multi_base_blacklist ctxt ho_atp) orelse String.isSuffix "_def_raw" (* FIXME: crude hack *) name0) then I else @@ -877,7 +881,7 @@ #> fold (fn th => fn (j, (multis, unis)) => (j + 1, if not (member Thm.eq_thm_prop add_ths th) andalso - is_theorem_bad_for_atps exporter th then + is_theorem_bad_for_atps ho_atp exporter th then (multis, unis) else let @@ -893,7 +897,7 @@ |> (fn SOME name => make_name reserved multi j name | NONE => "")), - locality_of_theorem global th), th) + locality_of_theorem global name0 th), th) in if multi then (new :: multis, unis) else (multis, new :: unis) @@ -911,8 +915,8 @@ fun external_frees t = [] |> Term.add_frees t |> filter_out (can Name.dest_internal o fst) -fun nearly_all_facts ctxt ({add, only, ...} : relevance_override) chained_ths - hyp_ts concl_t = +fun nearly_all_facts ctxt ho_atp ({add, only, ...} : relevance_override) + chained_ths hyp_ts concl_t = let val thy = Proof_Context.theory_of ctxt val reserved = reserved_isar_keyword_table () @@ -926,7 +930,7 @@ maps (map (fn ((name, loc), th) => ((K name, loc), th)) o fact_from_ref ctxt reserved chained_ths) add else - all_facts ctxt reserved false add_ths chained_ths) + all_facts ctxt ho_atp reserved false add_ths chained_ths) |> Config.get ctxt instantiate_inducts ? maps (instantiate_if_induct_rule ctxt ind_stmt ind_stmt_xs) |> (not (Config.get ctxt ignore_no_atp) andalso not only) @@ -934,7 +938,7 @@ |> uniquify end -fun relevant_facts ctxt (threshold0, threshold1) max_relevant +fun relevant_facts ctxt ho_atp (threshold0, threshold1) max_relevant is_built_in_const fudge (override as {only, ...}) chained_ths hyp_ts concl_t facts = let @@ -950,9 +954,9 @@ max_relevant = 0 then [] else - relevance_filter ctxt threshold0 decay max_relevant is_built_in_const - fudge override facts (chained_ths |> map prop_of) hyp_ts - (concl_t |> theory_constify fudge (Context.theory_name thy))) + relevance_filter ctxt ho_atp threshold0 decay max_relevant + is_built_in_const fudge override facts (chained_ths |> map prop_of) + hyp_ts (concl_t |> theory_constify fudge (Context.theory_name thy))) |> map (apfst (apfst (fn f => f ()))) end diff -r 08ad27488983 -r cfe7f4a68e51 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon Aug 29 13:50:47 2011 -0700 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 30 14:12:55 2011 +0200 @@ -91,6 +91,7 @@ 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 @@ -329,6 +330,10 @@ 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 *) diff -r 08ad27488983 -r cfe7f4a68e51 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon Aug 29 13:50:47 2011 -0700 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Tue Aug 30 14:12:55 2011 +0200 @@ -160,9 +160,16 @@ fun desc () = prover_description ctxt params name num_facts subgoal subgoal_count goal val problem = - {state = state, goal = goal, subgoal = subgoal, - subgoal_count = subgoal_count, facts = facts |> take num_facts, - smt_filter = smt_filter} + let + val filter_induction = + List.filter (fn fact => + not (Sledgehammer_Provers.is_induction_fact fact)) + in {state = state, goal = goal, subgoal = subgoal, + subgoal_count = subgoal_count, facts = + ((ATP_Systems.is_ho_atp name |> not) ? filter_induction) facts + |> take num_facts, + smt_filter = smt_filter} + end fun really_go () = problem |> get_minimizing_prover ctxt mode name params minimize_command @@ -260,9 +267,12 @@ 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 facts = nearly_all_facts ctxt relevance_override chained_ths hyp_ts - concl_t - val _ = () |> not blocking ? kill_provers + 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 _ = case find_first (not o is_prover_supported ctxt) provers of SOME name => error ("No such prover: " ^ name ^ ".") | NONE => () @@ -313,9 +323,9 @@ |> (case is_appropriate_prop of SOME is_app => filter (is_app o prop_of o snd) | NONE => I) - |> relevant_facts ctxt relevance_thresholds max_max_relevant - is_built_in_const relevance_fudge relevance_override - chained_ths hyp_ts concl_t + |> relevant_facts ctxt targetting_ho_provers relevance_thresholds + max_max_relevant 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) ^ ": " ^