src/HOL/Tools/Meson/meson_tactic.ML
author haftmann
Wed Dec 08 13:34:50 2010 +0100 (2010-12-08)
changeset 41075 4bed56dc95fb
parent 39948 317010af8972
child 42793 88bee9f6eec7
permissions -rw-r--r--
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
blanchet@39948
     1
(*  Title:      HOL/Tools/Meson/meson_tactic.ML
blanchet@39948
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
blanchet@39948
     3
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@39948
     4
blanchet@39948
     5
The "meson" proof method for HOL.
blanchet@39948
     6
*)
blanchet@39948
     7
blanchet@39948
     8
signature MESON_TACTIC =
blanchet@39948
     9
sig
blanchet@39948
    10
  val meson_general_tac : Proof.context -> thm list -> int -> tactic
blanchet@39948
    11
  val setup: theory -> theory
blanchet@39948
    12
end;
blanchet@39948
    13
blanchet@39948
    14
structure Meson_Tactic : MESON_TACTIC =
blanchet@39948
    15
struct
blanchet@39948
    16
blanchet@39948
    17
open Meson_Clausify
blanchet@39948
    18
blanchet@39948
    19
fun meson_general_tac ctxt ths =
blanchet@39948
    20
  let val ctxt = Classical.put_claset HOL_cs ctxt in
blanchet@39948
    21
    Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
blanchet@39948
    22
  end
blanchet@39948
    23
blanchet@39948
    24
val setup =
blanchet@39948
    25
  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
blanchet@39948
    26
     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
blanchet@39948
    27
     "MESON resolution proof procedure"
blanchet@39948
    28
blanchet@39948
    29
end;