src/HOL/Tools/Sledgehammer/meson_tactic.ML
author blanchet
Tue Aug 17 16:47:40 2010 +0200 (2010-08-17)
changeset 38490 57de0f12516f
parent 38027 505657ddb047
permissions -rw-r--r--
tuning
blanchet@35865
     1
(*  Title:      HOL/Tools/Sledgehammer/meson_tactic.ML
blanchet@38027
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
blanchet@37619
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@35865
     4
blanchet@35865
     5
MESON general tactic and proof method.
blanchet@35865
     6
*)
blanchet@35865
     7
blanchet@35865
     8
signature MESON_TACTIC =
blanchet@35865
     9
sig
blanchet@35865
    10
  val meson_general_tac : Proof.context -> thm list -> int -> tactic
blanchet@35865
    11
  val setup: theory -> theory
blanchet@35865
    12
end;
blanchet@35865
    13
blanchet@35865
    14
structure Meson_Tactic : MESON_TACTIC =
blanchet@35865
    15
struct
blanchet@35865
    16
blanchet@37619
    17
fun meson_general_tac ctxt ths =
blanchet@35865
    18
  let
blanchet@35865
    19
    val thy = ProofContext.theory_of ctxt
blanchet@35865
    20
    val ctxt0 = Classical.put_claset HOL_cs ctxt
blanchet@38016
    21
  in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
blanchet@35865
    22
blanchet@35865
    23
val setup =
blanchet@35865
    24
  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
blanchet@35865
    25
    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
blanchet@35865
    26
    "MESON resolution proof procedure";
blanchet@35865
    27
blanchet@35865
    28
end;