metis_tac: proper context (ProofContext.init it *not* sufficient);
authorwenzelm
Sun Jul 29 14:29:57 2007 +0200 (2007-07-29)
changeset 24041d5845b7c1a24
parent 24040 0d5cf52ebf87
child 24042 968f42fe6836
metis_tac: proper context (ProofContext.init it *not* sufficient);
simplified method setup;
src/HOL/Tools/metis_tools.ML
     1.1 --- a/src/HOL/Tools/metis_tools.ML	Sun Jul 29 14:29:56 2007 +0200
     1.2 +++ b/src/HOL/Tools/metis_tools.ML	Sun Jul 29 14:29:57 2007 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  signature METIS_TOOLS =
     1.5  sig
     1.6    val type_lits: bool ref
     1.7 -  val metis_tac : Thm.thm list -> int -> Tactical.tactic
     1.8 +  val metis_tac : Proof.context -> thm list -> int -> tactic
     1.9    val setup : theory -> theory
    1.10  end
    1.11  
    1.12 @@ -556,37 +556,29 @@
    1.13      end;
    1.14  
    1.15    fun metis_general_tac mode ctxt ths i st0 =
    1.16 -    let val _ = Output.debug (fn () => "Metis called with theorems " ^ cat_lines (map string_of_thm ths))
    1.17 +    let val _ = Output.debug (fn () =>
    1.18 +          "Metis called with theorems " ^ cat_lines (map string_of_thm ths))
    1.19          val ths' = ResAxioms.cnf_rules_of_ths ths
    1.20      in
    1.21         (MESON ResAxioms.neg_clausify (fn cls => rtac (FOL_SOLVE mode ctxt cls ths') 1) i
    1.22          THEN ResAxioms.expand_defs_tac st0) st0
    1.23      end;
    1.24  
    1.25 -  fun metis_tac ths gno st =
    1.26 -    metis_general_tac ResAtp.Auto (ProofContext.init (theory_of_thm st)) ths gno st;
    1.27 +  val metis_tac = metis_general_tac ResAtp.Auto;
    1.28 +  val metisF_tac = metis_general_tac ResAtp.Fol;
    1.29 +  val metisH_tac = metis_general_tac ResAtp.Hol;
    1.30  
    1.31 -  fun metisF_tac ths gno st =
    1.32 -    metis_general_tac ResAtp.Fol (ProofContext.init (theory_of_thm st)) ths gno st;
    1.33 -
    1.34 -  fun metisH_tac ths gno st =
    1.35 -    metis_general_tac ResAtp.Hol (ProofContext.init (theory_of_thm st)) ths gno st;
    1.36 -
    1.37 -  fun metis_meth mode ths ctxt =
    1.38 +  fun method mode = Method.thms_ctxt_args (fn ths => fn ctxt =>
    1.39      Method.SIMPLE_METHOD'
    1.40        (setmp ResHolClause.typ_level ResHolClause.T_CONST  (*constant-typed*)
    1.41          (setmp ResHolClause.minimize_applies false        (*avoid this optimization*)
    1.42 -          (CHANGED_PROP o metis_general_tac mode ctxt ths)));
    1.43 -
    1.44 -  fun metis  ths ctxt = metis_meth ResAtp.Auto ths ctxt;
    1.45 -  fun metisF ths ctxt = metis_meth ResAtp.Fol  ths ctxt;
    1.46 -  fun metisH ths ctxt = metis_meth ResAtp.Hol  ths ctxt;
    1.47 +          (CHANGED_PROP o metis_general_tac mode ctxt ths))));
    1.48  
    1.49    val setup =
    1.50      Method.add_methods
    1.51 -      [("metis",  Method.thms_ctxt_args metis,  "METIS for FOL & HOL problems"),
    1.52 -       ("metisF", Method.thms_ctxt_args metisF, "METIS for FOL problems"),
    1.53 -       ("metisH", Method.thms_ctxt_args metisH, "METIS for HOL problems"),
    1.54 +      [("metis", method ResAtp.Auto, "METIS for FOL & HOL problems"),
    1.55 +       ("metisF", method ResAtp.Fol, "METIS for FOL problems"),
    1.56 +       ("metisH", method ResAtp.Hol, "METIS for HOL problems"),
    1.57         ("finish_clausify",
    1.58           Method.no_args (Method.SIMPLE_METHOD' (K (ResAxioms.expand_defs_tac refl))),
    1.59      "cleanup after conversion to clauses")];