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`
     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   val setup: theory -> theory
    12 end;
    13 
    14 structure Meson_Tactic : MESON_TACTIC =
    15 struct
    16 
    17 open Meson_Clausify
    18 
    19 fun meson_general_tac ctxt ths =
    20   let val ctxt = Classical.put_claset HOL_cs ctxt in
    21     Meson.meson_tac ctxt (maps (snd o cnf_axiom ctxt false 0) ths)
    22   end
    23 
    24 val setup =
    25   Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
    26      SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
    27      "MESON resolution proof procedure"
    28 
    29 end;