src/HOL/Tools/Sledgehammer/meson_tactic.ML
author haftmann
Thu, 08 Jul 2010 16:19:24 +0200
changeset 37744 3daaf23b9ab4
parent 37628 78334f400ae6
child 38016 135f7d489492
permissions -rw-r--r--
tuned titles

(*  Title:      HOL/Tools/Sledgehammer/meson_tactic.ML
    Author:     Jia Meng, Cambridge University Computer Laboratory
    Author:     Jasmin Blanchette, TU Muenchen

MESON general tactic and proof method.
*)

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

fun meson_general_tac ctxt ths =
  let
    val thy = ProofContext.theory_of ctxt
    val ctxt0 = Classical.put_claset HOL_cs ctxt
  in Meson.meson_tac ctxt0 (maps (Clausifier.cnf_axiom thy false) 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;