src/HOL/Tools/arith_data.ML
author Philipp Meyer
Wed Sep 30 11:33:59 2009 +0200 (2009-09-30)
changeset 32866 1238cbb7c08f
parent 32155 e2bf2f73b0c8
child 32957 675c0c7e6a37
permissions -rw-r--r--
atp_minimal using chain_ths again
     1 (*  Title:      HOL/Tools/arith_data.ML
     2     Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
     3 
     4 Common arithmetic proof auxiliary.
     5 *)
     6 
     7 signature ARITH_DATA =
     8 sig
     9   val arith_tac: Proof.context -> int -> tactic
    10   val verbose_arith_tac: Proof.context -> int -> tactic
    11   val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
    12   val get_arith_facts: Proof.context -> thm list
    13 
    14   val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
    15   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
    16   val prove_conv2: tactic -> (simpset -> tactic) -> simpset -> term * term -> thm
    17   val simp_all_tac: thm list -> simpset -> tactic
    18   val simplify_meta_eq: thm list -> simpset -> thm -> thm
    19   val trans_tac: thm option -> tactic
    20   val prep_simproc: theory -> string * string list * (theory -> simpset -> term -> thm option)
    21     -> simproc
    22 
    23   val setup: theory -> theory
    24 end;
    25 
    26 structure Arith_Data: ARITH_DATA =
    27 struct
    28 
    29 (* slots for plugging in arithmetic facts and tactics *)
    30 
    31 structure Arith_Facts = Named_Thms
    32 (
    33   val name = "arith"
    34   val description = "arith facts - only ground formulas"
    35 );
    36 
    37 val get_arith_facts = Arith_Facts.get;
    38 
    39 structure Arith_Tactics = TheoryDataFun
    40 (
    41   type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
    42   val empty = [];
    43   val copy = I;
    44   val extend = I;
    45   fun merge _ = AList.merge (op =) (K true);
    46 );
    47 
    48 fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
    49 
    50 fun gen_arith_tac verbose ctxt =
    51   let
    52     val tactics = (Arith_Tactics.get o ProofContext.theory_of) ctxt
    53     fun invoke (_, (name, tac)) k st = (if verbose
    54       then warning ("Trying " ^ name ^ "...") else ();
    55       tac verbose ctxt k st);
    56   in FIRST' (map invoke (rev tactics)) end;
    57 
    58 val arith_tac = gen_arith_tac false;
    59 val verbose_arith_tac = gen_arith_tac true;
    60 
    61 val setup =
    62   Arith_Facts.setup #>
    63   Method.setup @{binding arith}
    64     (Args.bang_facts >> (fn prems => fn ctxt =>
    65       METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ get_arith_facts ctxt @ facts)
    66         THEN' verbose_arith_tac ctxt))))
    67     "various arithmetic decision procedures";
    68 
    69 
    70 (* various auxiliary and legacy *)
    71 
    72 fun prove_conv_nohyps tacs ctxt (t, u) =
    73   if t aconv u then NONE
    74   else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
    75   in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
    76 
    77 fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
    78 
    79 fun prove_conv2 expand_tac norm_tac ss tu = (*FIXME avoid standard*)
    80   mk_meta_eq (standard (Goal.prove (Simplifier.the_context ss) [] []
    81       (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
    82     (K (EVERY [expand_tac, norm_tac ss]))));
    83 
    84 fun simp_all_tac rules =
    85   let val ss0 = HOL_ss addsimps rules
    86   in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
    87 
    88 fun simplify_meta_eq rules =
    89   let val ss0 = HOL_basic_ss addeqcongs [eq_cong2] addsimps rules
    90   in fn ss => simplify (Simplifier.inherit_context ss ss0) o mk_meta_eq end
    91 
    92 fun trans_tac NONE  = all_tac
    93   | trans_tac (SOME th) = ALLGOALS (rtac (th RS trans));
    94 
    95 fun prep_simproc thy (name, pats, proc) =
    96   Simplifier.simproc thy name pats proc;
    97 
    98 end;