--- a/src/HOL/Sledgehammer.thy Sun Apr 25 11:38:46 2010 +0200
+++ b/src/HOL/Sledgehammer.thy Sun Apr 25 14:40:36 2010 +0200
@@ -105,6 +105,7 @@
setup ATP_Systems.setup
use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
use "Tools/Sledgehammer/sledgehammer_isar.ML"
+setup Sledgehammer_Isar.setup
subsection {* The MESON prover *}
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 25 11:38:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Sun Apr 25 14:40:36 2010 +0200
@@ -20,6 +20,7 @@
val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
val suppress_endtheory: bool Unsynchronized.ref
(*for emergency use where endtheory causes problems*)
+ val neg_clausify_tac: Proof.context -> int -> tactic
val setup: theory -> theory
end;
@@ -484,26 +485,10 @@
REPEAT_DETERM_N (length ts) o etac thin_rl] i
end);
-val neg_clausify_setup =
- Method.setup @{binding neg_clausify} (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
- "conversion of goal to conjecture clauses";
-
-
-(** Attribute for converting a theorem into clauses **)
-
-val clausify_setup =
- Attrib.setup @{binding clausify}
- (Scan.lift OuterParse.nat >>
- (fn i => Thm.rule_attribute (fn context => fn th =>
- Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))))
- "conversion of theorem to clauses";
-
(** setup **)
val setup =
- neg_clausify_setup #>
- clausify_setup #>
perhaps saturate_skolem_cache #>
Theory.at_end clause_cache_endtheory;
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Apr 25 11:38:46 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Sun Apr 25 14:40:36 2010 +0200
@@ -12,18 +12,42 @@
val timeout: int Unsynchronized.ref
val full_types: bool Unsynchronized.ref
val default_params : theory -> (string * string) list -> params
+ val setup: theory -> theory
end;
structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
struct
open Sledgehammer_Util
+open Sledgehammer_Fact_Preprocessor
open ATP_Manager
open ATP_Systems
open Sledgehammer_Fact_Minimizer
structure K = OuterKeyword and P = OuterParse
+(** Proof method used in Isar proofs **)
+
+val neg_clausify_setup =
+ Method.setup @{binding neg_clausify}
+ (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
+ "conversion of goal to negated conjecture clauses"
+
+val parse_clausify_attribute =
+ Scan.lift OuterParse.nat
+ >> (fn i => Thm.rule_attribute (fn context => fn th =>
+ let val thy = Context.theory_of context in
+ Meson.make_meta_clause (nth (cnf_axiom thy th) i)
+ end))
+
+(** Attribute for converting a theorem into clauses **)
+
+val clausify_setup =
+ Attrib.setup @{binding clausify} parse_clausify_attribute
+ "conversion of theorem to clauses"
+
+(** Sledgehammer commands **)
+
fun add_to_relevance_override ns : relevance_override =
{add = ns, del = [], only = false}
fun del_from_relevance_override ns : relevance_override =
@@ -323,11 +347,15 @@
val _ =
OuterSyntax.improper_command sledgehammerN
- "search for first-order proof using automatic theorem provers" K.diag
- parse_sledgehammer_command
+ "search for first-order proof using automatic theorem provers" K.diag
+ parse_sledgehammer_command
val _ =
OuterSyntax.command sledgehammer_paramsN
- "set and display the default parameters for Sledgehammer" K.thy_decl
- parse_sledgehammer_params_command
+ "set and display the default parameters for Sledgehammer" K.thy_decl
+ parse_sledgehammer_params_command
+
+val setup =
+ neg_clausify_setup
+ #> clausify_setup
end;