--- 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 ())
--- 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
--- 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
--- 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 *)
--- 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) ^ ": " ^