File ‹Tools/Meson/meson_tactic.ML›

(*  Title:      HOL/Tools/Meson/meson_tactic.ML
    Author:     Jia Meng, Cambridge University Computer Laboratory and NICTA
    Author:     Jasmin Blanchette, TU Muenchen

The "meson" proof method for HOL.
*)

signature MESON_TACTIC =
sig
  val meson_general_tac : Proof.context -> thm list -> int -> tactic
end;

structure Meson_Tactic : MESON_TACTIC =
struct

fun meson_general_tac ctxt ths =
  let val ctxt' = put_claset HOL_cs ctxt
  in
    Meson.meson_tac ctxt' (maps (snd o Meson_Clausify.cnf_axiom Meson.simp_options_all_true ctxt'
      false true 0) ths)
  end

(* This is part of a workaround to avoid freezing schematic variables in \<^text>‹using› facts. See
   🗏‹~~/src/HOL/Tools/Metis/metis_tactic.ML› for details. *)
val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o Thm.prop_of

val _ =
  Theory.setup
    (Method.setup \<^binding>‹meson› (Attrib.thms >> (fn ths => fn ctxt0 =>
      CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
        let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
          st
          |> HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
            CHANGED_PROP o meson_general_tac ctxt0 (schem_facts @ ths))
          |> TACTIC_CONTEXT ctxt
        end)))
      "MESON resolution proof procedure")

end;