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;
     1 (*  Title:      HOL/Tools/Meson/meson_tactic.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
     3     Author:     Jasmin Blanchette, TU Muenchen
     4 
     5 The "meson" proof method for HOL.
     6 *)
     7 
     8 signature MESON_TACTIC =
     9 sig
    10   val meson_general_tac : Proof.context -> thm list -> int -> tactic
    11 end;
    12 
    13 structure Meson_Tactic : MESON_TACTIC =
    14 struct
    15 
    16 fun meson_general_tac ctxt ths =
    17   let val ctxt' = put_claset HOL_cs ctxt
    18   in Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom ctxt' false true 0) ths) end
    19 
    20 val _ =
    21   Theory.setup
    22     (Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
    23       SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
    24       "MESON resolution proof procedure")
    25 
    26 end;