(* Title: HOL/Tools/Meson/meson_tactic.ML
Author: Jia Meng, Cambridge University Computer Laboratory and NICTA
Author: Jasmin Blanchette, TU Muenchen
The "meson" proof method for HOL.
*)
signature MESON_TACTIC =
sig
val meson_general_tac : Proof.context -> thm list -> int -> tactic
val setup: theory -> theory
end;
structure Meson_Tactic : MESON_TACTIC =
struct
open Meson_Clausify
fun meson_general_tac ctxt ths =
let val ctxt = Classical.put_claset HOL_cs ctxt in
Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
end
val setup =
Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
"MESON resolution proof procedure"
end;