src/HOL/Tools/Meson/meson_tactic.ML
author haftmann
Sat Dec 24 16:14:58 2011 +0100 (2011-12-24)
changeset 45981 4c629115e3ab
parent 45508 b216dc1b3630
child 58817 4cd778c91fdc
permissions -rw-r--r--
dropped references to obsolete facts `mem_def_raw` and `Collect_def_raw`
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 =
wenzelm@42793
    20
  let val ctxt' = put_claset HOL_cs ctxt
blanchet@45508
    21
  in Meson.meson_tac ctxt' (maps (snd o cnf_axiom ctxt' false true 0) ths) end
blanchet@39948
    22
blanchet@39948
    23
val setup =
blanchet@39948
    24
  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
blanchet@39948
    25
     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
blanchet@39948
    26
     "MESON resolution proof procedure"
blanchet@39948
    27
blanchet@39948
    28
end;