--- a/src/HOL/Tools/atp_wrapper.ML Wed Jun 03 16:56:41 2009 +0200
+++ b/src/HOL/Tools/atp_wrapper.ML Wed Jun 03 16:56:41 2009 +0200
@@ -68,13 +68,13 @@
case axiom_clauses of
NONE => relevance_filter goal goal_cls
| SOME axcls => axcls
- val (thm_names, clauses) = preparer goal_cls the_axiom_clauses thy
+ val (thm_names, clauses) = preparer goal_cls chain_ths the_axiom_clauses thy
val the_const_counts = case const_counts of
NONE =>
ResHolClause.count_constants(
case axiom_clauses of
NONE => clauses
- | SOME axcls => #2(preparer goal_cls (relevance_filter goal goal_cls) thy)
+ | SOME axcls => #2(preparer goal_cls chain_ths (relevance_filter goal goal_cls) thy)
)
| SOME ccs => ccs
val _ = writer fname the_const_counts clauses
--- a/src/HOL/Tools/res_atp.ML Wed Jun 03 16:56:41 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Wed Jun 03 16:56:41 2009 +0200
@@ -8,7 +8,7 @@
val type_consts_of_terms : theory -> term list -> string list
val get_relevant : int -> bool -> Proof.context * (thm list * 'a) -> thm list ->
(thm * (string * int)) list
- val prepare_clauses : bool -> thm list ->
+ val prepare_clauses : bool -> thm list -> thm list ->
(thm * (ResHolClause.axiom_name * ResHolClause.clause_id)) list -> theory ->
ResHolClause.axiom_name vector * (ResHolClause.clause list * ResHolClause.clause list *
ResHolClause.clause list * ResClause.classrelClause list * ResClause.arityClause list)
@@ -403,23 +403,20 @@
fun display_thm (name,th) = Output.debug (fn () => name ^ ": " ^ Display.string_of_thm th);
(* get lemmas from claset, simpset, atpset and extra supplied rules *)
-fun get_clasimp_atp_lemmas ctxt user_thms =
+fun get_clasimp_atp_lemmas ctxt =
let val included_thms =
- if include_all
- then (tap (fn ths => Output.debug
- (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
- (name_thm_pairs ctxt))
- else
- let val atpset_thms =
- if include_atpset then ResAxioms.atpset_rules_of ctxt
- else []
- val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms)
- in atpset_thms end
- val user_rules = filter check_named
- (map ResAxioms.pairname
- (if null user_thms then whitelist else user_thms))
+ if include_all
+ then (tap (fn ths => Output.debug
+ (fn () => ("Including all " ^ Int.toString (length ths) ^ " theorems")))
+ (name_thm_pairs ctxt))
+ else
+ let val atpset_thms =
+ if include_atpset then ResAxioms.atpset_rules_of ctxt
+ else []
+ val _ = (Output.debug (fn () => "ATP theorems: "); app display_thm atpset_thms)
+ in atpset_thms end
in
- (filter check_named included_thms, user_rules)
+ filter check_named included_thms
end;
(***************************************************************)
@@ -521,19 +518,20 @@
fun get_relevant max_new theory_const (ctxt, (chain_ths, th)) goal_cls =
let
val thy = ProofContext.theory_of ctxt
- val (included_thms,white_thms) = get_clasimp_atp_lemmas ctxt chain_ths
+ val included_thms = get_clasimp_atp_lemmas ctxt
val included_cls = included_thms |> ResAxioms.cnf_rules_pairs thy |> make_unique
|> restrict_to_logic thy (isFO thy goal_cls)
|> remove_unwanted_clauses
- val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
- (*clauses relevant to goal gl*)
in
- white_cls @ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
+ relevance_filter max_new theory_const thy included_cls (map prop_of goal_cls)
end;
(* prepare and count clauses before writing *)
-fun prepare_clauses dfg goal_cls axcls thy =
+fun prepare_clauses dfg goal_cls chain_ths axcls thy =
let
+ val white_thms = filter check_named (map ResAxioms.pairname (if null chain_ths then whitelist else chain_ths))
+ val white_cls = ResAxioms.cnf_rules_pairs thy white_thms
+ val axcls = white_cls @ axcls
val ccls = subtract_cls goal_cls axcls
val _ = app (fn th => Output.debug (fn _ => Display.string_of_thm th)) ccls
val ccltms = map prop_of ccls
--- a/src/HOL/Tools/res_reconstruct.ML Wed Jun 03 16:56:41 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Wed Jun 03 16:56:41 2009 +0200
@@ -528,6 +528,10 @@
in
get_axiom_names thm_names (get_step_nums proofextract)
end;
+
+ (*Used to label theorems chained into the sledgehammer call*)
+ val chained_hint = "CHAINED";
+ val nochained = filter_out (fn y => y = chained_hint)
(* metis-command *)
fun metis_line [] = "apply metis"
@@ -536,13 +540,11 @@
(* atp_minimize [atp=<prover>] <lemmas> *)
fun minimize_line _ [] = ""
| minimize_line name lemmas = "For minimizing the number of lemmas try this command:\n" ^
- (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^ space_implode " " lemmas)
+ (Markup.markup Markup.sendback) ("atp_minimize [atp=" ^ name ^ "] " ^
+ space_implode " " (nochained lemmas))
- (*Used to label theorems chained into the sledgehammer call*)
- val chained_hint = "CHAINED";
fun sendback_metis_nochained lemmas =
- let val nochained = filter_out (fn y => y = chained_hint)
- in (Markup.markup Markup.sendback o metis_line) (nochained lemmas) end
+ (Markup.markup Markup.sendback o metis_line) (nochained lemmas)
fun lemma_list_tstp name result =
let val lemmas = extract_lemmas get_step_nums_tstp result
in sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas end;