move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
authorblanchet
Sun Apr 25 14:40:36 2010 +0200 (2010-04-25)
changeset 363941a48d18449d8
parent 36393 be73a2b2443b
child 36395 e73923451f6f
move "neg_clausify" method and "clausify" attribute to "sledgehammer_isar.ML"
src/HOL/Sledgehammer.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/Sledgehammer.thy	Sun Apr 25 11:38:46 2010 +0200
     1.2 +++ b/src/HOL/Sledgehammer.thy	Sun Apr 25 14:40:36 2010 +0200
     1.3 @@ -105,6 +105,7 @@
     1.4  setup ATP_Systems.setup
     1.5  use "Tools/Sledgehammer/sledgehammer_fact_minimizer.ML"
     1.6  use "Tools/Sledgehammer/sledgehammer_isar.ML"
     1.7 +setup Sledgehammer_Isar.setup
     1.8  
     1.9  
    1.10  subsection {* The MESON prover *}
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 25 11:38:46 2010 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML	Sun Apr 25 14:40:36 2010 +0200
     2.3 @@ -20,6 +20,7 @@
     2.4    val neg_conjecture_clauses: Proof.context -> thm -> int -> thm list * (string * typ) list
     2.5    val suppress_endtheory: bool Unsynchronized.ref
     2.6      (*for emergency use where endtheory causes problems*)
     2.7 +  val neg_clausify_tac: Proof.context -> int -> tactic
     2.8    val setup: theory -> theory
     2.9  end;
    2.10  
    2.11 @@ -484,26 +485,10 @@
    2.12          REPEAT_DETERM_N (length ts) o etac thin_rl] i
    2.13       end);
    2.14  
    2.15 -val neg_clausify_setup =
    2.16 -  Method.setup @{binding neg_clausify} (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
    2.17 -  "conversion of goal to conjecture clauses";
    2.18 -
    2.19 -
    2.20 -(** Attribute for converting a theorem into clauses **)
    2.21 -
    2.22 -val clausify_setup =
    2.23 -  Attrib.setup @{binding clausify}
    2.24 -    (Scan.lift OuterParse.nat >>
    2.25 -      (fn i => Thm.rule_attribute (fn context => fn th =>
    2.26 -          Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))))
    2.27 -  "conversion of theorem to clauses";
    2.28 -
    2.29  
    2.30  (** setup **)
    2.31  
    2.32  val setup =
    2.33 -  neg_clausify_setup #>
    2.34 -  clausify_setup #>
    2.35    perhaps saturate_skolem_cache #>
    2.36    Theory.at_end clause_cache_endtheory;
    2.37  
     3.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Apr 25 11:38:46 2010 +0200
     3.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Apr 25 14:40:36 2010 +0200
     3.3 @@ -12,18 +12,42 @@
     3.4    val timeout: int Unsynchronized.ref
     3.5    val full_types: bool Unsynchronized.ref
     3.6    val default_params : theory -> (string * string) list -> params
     3.7 +  val setup: theory -> theory
     3.8  end;
     3.9  
    3.10  structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    3.11  struct
    3.12  
    3.13  open Sledgehammer_Util
    3.14 +open Sledgehammer_Fact_Preprocessor
    3.15  open ATP_Manager
    3.16  open ATP_Systems
    3.17  open Sledgehammer_Fact_Minimizer
    3.18  
    3.19  structure K = OuterKeyword and P = OuterParse
    3.20  
    3.21 +(** Proof method used in Isar proofs **)
    3.22 +
    3.23 +val neg_clausify_setup =
    3.24 +  Method.setup @{binding neg_clausify}
    3.25 +               (Scan.succeed (SIMPLE_METHOD' o neg_clausify_tac))
    3.26 +               "conversion of goal to negated conjecture clauses"
    3.27 +
    3.28 +val parse_clausify_attribute =
    3.29 +  Scan.lift OuterParse.nat
    3.30 +  >> (fn i => Thm.rule_attribute (fn context => fn th =>
    3.31 +                  let val thy = Context.theory_of context in
    3.32 +                    Meson.make_meta_clause (nth (cnf_axiom thy th) i)
    3.33 +                  end))
    3.34 +
    3.35 +(** Attribute for converting a theorem into clauses **)
    3.36 +
    3.37 +val clausify_setup =
    3.38 +  Attrib.setup @{binding clausify} parse_clausify_attribute
    3.39 +               "conversion of theorem to clauses"
    3.40 +
    3.41 +(** Sledgehammer commands **)
    3.42 +
    3.43  fun add_to_relevance_override ns : relevance_override =
    3.44    {add = ns, del = [], only = false}
    3.45  fun del_from_relevance_override ns : relevance_override =
    3.46 @@ -323,11 +347,15 @@
    3.47  
    3.48  val _ =
    3.49    OuterSyntax.improper_command sledgehammerN
    3.50 -    "search for first-order proof using automatic theorem provers" K.diag
    3.51 -    parse_sledgehammer_command
    3.52 +      "search for first-order proof using automatic theorem provers" K.diag
    3.53 +      parse_sledgehammer_command
    3.54  val _ =
    3.55    OuterSyntax.command sledgehammer_paramsN
    3.56 -    "set and display the default parameters for Sledgehammer" K.thy_decl
    3.57 -    parse_sledgehammer_params_command
    3.58 +      "set and display the default parameters for Sledgehammer" K.thy_decl
    3.59 +      parse_sledgehammer_params_command
    3.60 +
    3.61 +val setup =
    3.62 +  neg_clausify_setup
    3.63 +  #> clausify_setup
    3.64  
    3.65  end;