src/HOL/Tools/Meson/meson_tactic.ML
author wenzelm
Fri Mar 06 15:58:56 2015 +0100 (2015-03-06)
changeset 59621 291934bac95e
parent 58817 4cd778c91fdc
child 67149 e61557884799
permissions -rw-r--r--
Thm.cterm_of and Thm.ctyp_of operate on local context;
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
end;
blanchet@39948
    12
blanchet@39948
    13
structure Meson_Tactic : MESON_TACTIC =
blanchet@39948
    14
struct
blanchet@39948
    15
blanchet@39948
    16
fun meson_general_tac ctxt ths =
wenzelm@42793
    17
  let val ctxt' = put_claset HOL_cs ctxt
wenzelm@58817
    18
  in Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom ctxt' false true 0) ths) end
blanchet@39948
    19
wenzelm@58817
    20
val _ =
wenzelm@58817
    21
  Theory.setup
wenzelm@58817
    22
    (Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
wenzelm@58817
    23
      SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
wenzelm@58817
    24
      "MESON resolution proof procedure")
blanchet@39948
    25
blanchet@39948
    26
end;