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
     1 (*  Title:      HOL/Tools/Sledgehammer/meson_tactic.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 MESON general tactic and proof method.
     6 *)
     7 
     8 signature MESON_TACTIC =
     9 sig
    10   val meson_general_tac : Proof.context -> thm list -> int -> tactic
    11   val setup: theory -> theory
    12 end;
    13 
    14 structure Meson_Tactic : MESON_TACTIC =
    15 struct
    16 
    17 fun meson_general_tac ctxt ths =
    18   let
    19     val thy = ProofContext.theory_of ctxt
    20     val ctxt0 = Classical.put_claset HOL_cs ctxt
    21   in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy) ths) end
    22 
    23 val setup =
    24   Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
    25     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
    26     "MESON resolution proof procedure";
    27 
    28 end;