src/HOL/Tools/Sledgehammer/meson_tactic.ML
author blanchet
Fri Apr 16 14:48:34 2010 +0200 (2010-04-16)
changeset 36169 27b1cc58715e
parent 35865 2f8fb5242799
child 37498 b426cbdb5a23
permissions -rw-r--r--
store nonmangled names along with mangled type names in Sledgehammer for debugging purposes
blanchet@35865
     1
(*  Title:      HOL/Tools/Sledgehammer/meson_tactic.ML
blanchet@35865
     2
    Author:     Jia Meng, Cambridge University Computer Laboratory
blanchet@35865
     3
blanchet@35865
     4
MESON general tactic and proof method.
blanchet@35865
     5
*)
blanchet@35865
     6
blanchet@35865
     7
signature MESON_TACTIC =
blanchet@35865
     8
sig
blanchet@35865
     9
  val expand_defs_tac : thm -> tactic
blanchet@35865
    10
  val meson_general_tac : Proof.context -> thm list -> int -> tactic
blanchet@35865
    11
  val setup: theory -> theory
blanchet@35865
    12
end;
blanchet@35865
    13
blanchet@35865
    14
structure Meson_Tactic : MESON_TACTIC =
blanchet@35865
    15
struct
blanchet@35865
    16
blanchet@35865
    17
open Sledgehammer_Fact_Preprocessor
blanchet@35865
    18
blanchet@35865
    19
(*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
blanchet@35865
    20
fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) =
blanchet@35865
    21
    String.isPrefix skolem_prefix a
blanchet@35865
    22
  | is_absko _ = false;
blanchet@35865
    23
blanchet@35865
    24
fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) =   (*Definition of Free, not in certain terms*)
blanchet@35865
    25
      is_Free t andalso not (member (op aconv) xs t)
blanchet@35865
    26
  | is_okdef _ _ = false
blanchet@35865
    27
blanchet@35865
    28
(*This function tries to cope with open locales, which introduce hypotheses of the form
blanchet@35865
    29
  Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
blanchet@35865
    30
  of sko_ functions. *)
blanchet@35865
    31
fun expand_defs_tac st0 st =
blanchet@35865
    32
  let val hyps0 = #hyps (rep_thm st0)
blanchet@35865
    33
      val hyps = #hyps (crep_thm st)
blanchet@35865
    34
      val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
blanchet@35865
    35
      val defs = filter (is_absko o Thm.term_of) newhyps
blanchet@35865
    36
      val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
blanchet@35865
    37
                                      (map Thm.term_of hyps)
blanchet@35865
    38
      val fixed = OldTerm.term_frees (concl_of st) @
blanchet@35865
    39
                  fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
blanchet@35865
    40
  in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
blanchet@35865
    41
blanchet@35865
    42
fun meson_general_tac ctxt ths i st0 =
blanchet@35865
    43
  let
blanchet@35865
    44
    val thy = ProofContext.theory_of ctxt
blanchet@35865
    45
    val ctxt0 = Classical.put_claset HOL_cs ctxt
blanchet@35865
    46
  in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
blanchet@35865
    47
blanchet@35865
    48
val setup =
blanchet@35865
    49
  Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
blanchet@35865
    50
    SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
blanchet@35865
    51
    "MESON resolution proof procedure";
blanchet@35865
    52
blanchet@35865
    53
end;