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
     1 (*  Title:      HOL/Tools/Sledgehammer/meson_tactic.ML
     2     Author:     Jia Meng, Cambridge University Computer Laboratory
     3 
     4 MESON general tactic and proof method.
     5 *)
     6 
     7 signature MESON_TACTIC =
     8 sig
     9   val expand_defs_tac : thm -> tactic
    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 Sledgehammer_Fact_Preprocessor
    18 
    19 (*Expand all new definitions of abstraction or Skolem functions in a proof state.*)
    20 fun is_absko (Const (@{const_name "=="}, _) $ Free (a, _) $ u) =
    21     String.isPrefix skolem_prefix a
    22   | is_absko _ = false;
    23 
    24 fun is_okdef xs (Const (@{const_name "=="}, _) $ t $ u) =   (*Definition of Free, not in certain terms*)
    25       is_Free t andalso not (member (op aconv) xs t)
    26   | is_okdef _ _ = false
    27 
    28 (*This function tries to cope with open locales, which introduce hypotheses of the form
    29   Free == t, conjecture clauses, which introduce various hypotheses, and also definitions
    30   of sko_ functions. *)
    31 fun expand_defs_tac st0 st =
    32   let val hyps0 = #hyps (rep_thm st0)
    33       val hyps = #hyps (crep_thm st)
    34       val newhyps = filter_out (member (op aconv) hyps0 o Thm.term_of) hyps
    35       val defs = filter (is_absko o Thm.term_of) newhyps
    36       val remaining_hyps = filter_out (member (op aconv) (map Thm.term_of defs))
    37                                       (map Thm.term_of hyps)
    38       val fixed = OldTerm.term_frees (concl_of st) @
    39                   fold (union (op aconv)) (map OldTerm.term_frees remaining_hyps) []
    40   in Seq.of_list [Local_Defs.expand (filter (is_okdef fixed o Thm.term_of) defs) st] end;
    41 
    42 fun meson_general_tac ctxt ths i st0 =
    43   let
    44     val thy = ProofContext.theory_of ctxt
    45     val ctxt0 = Classical.put_claset HOL_cs ctxt
    46   in (Meson.meson_tac ctxt0 (maps (cnf_axiom thy) ths) i THEN expand_defs_tac st0) st0 end;
    47 
    48 val setup =
    49   Method.setup @{binding meson} (Attrib.thms >> (fn ths => fn ctxt =>
    50     SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
    51     "MESON resolution proof procedure";
    52 
    53 end;