src/HOL/Tools/Sledgehammer/meson_tactic.ML
author blanchet
Tue Jun 29 10:25:53 2010 +0200 (2010-06-29)
changeset 37626 1146291fe718
parent 37619 bcb19259f92a
child 37628 78334f400ae6
permissions -rw-r--r--
move blacklisting completely out of the clausifier;
the only reason it was in the clausifier as well was the Skolem cache
blanchet@35865
     1
(*  Title:      HOL/Tools/Sledgehammer/meson_tactic.ML
blanchet@35865
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory
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@37619
    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;