src/HOL/Tools/arith_data.ML
author wenzelm
Sat Aug 16 14:32:26 2014 +0200 (2014-08-16)
changeset 57952 1a9a6dfc255f
parent 51717 9e7d1c139569
child 57955 f28337c2c0a8
permissions -rw-r--r--
updated to named_theorems;
     1 (*  Title:      HOL/Tools/arith_data.ML
     2     Author:     Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
     3 
     4 Common arithmetic proof auxiliary and legacy.
     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 
    13   val mk_number: typ -> int -> term
    14   val mk_sum: typ -> term list -> term
    15   val long_mk_sum: typ -> term list -> term
    16   val dest_sum: term -> term list
    17 
    18   val prove_conv_nohyps: tactic list -> Proof.context -> term * term -> thm option
    19   val prove_conv: tactic list -> Proof.context -> thm list -> term * term -> thm option
    20   val prove_conv2: tactic -> (Proof.context -> tactic) -> Proof.context -> term * term -> thm
    21   val simp_all_tac: thm list -> Proof.context -> tactic
    22   val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
    23 
    24   val setup: theory -> theory
    25 end;
    26 
    27 structure Arith_Data: ARITH_DATA =
    28 struct
    29 
    30 (* slot for plugging in tactics *)
    31 
    32 structure Arith_Tactics = Theory_Data
    33 (
    34   type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
    35   val empty = [];
    36   val extend = I;
    37   fun merge data : T = AList.merge (op =) (K true) data;
    38 );
    39 
    40 fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
    41 
    42 fun gen_arith_tac verbose ctxt =
    43   let
    44     val tactics = Arith_Tactics.get (Proof_Context.theory_of ctxt);
    45     fun invoke (_, (_, tac)) k st = tac verbose ctxt k st;
    46   in FIRST' (map invoke (rev tactics)) end;
    47 
    48 val arith_tac = gen_arith_tac false;
    49 val verbose_arith_tac = gen_arith_tac true;
    50 
    51 val setup =
    52   Method.setup @{binding arith}
    53     (Scan.succeed (fn ctxt =>
    54       METHOD (fn facts =>
    55         HEADGOAL
    56         (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
    57           THEN' verbose_arith_tac ctxt))))
    58     "various arithmetic decision procedures";
    59 
    60 
    61 (* some specialized syntactic operations *)
    62 
    63 fun mk_number T 1 = HOLogic.numeral_const T $ HOLogic.one_const
    64   | mk_number T n = HOLogic.mk_number T n;
    65 
    66 val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    67 
    68 fun mk_minus t =
    69   let val T = Term.fastype_of t
    70   in Const (@{const_name Groups.uminus}, T --> T) $ t end;
    71 
    72 (*Thus mk_sum[t] yields t+0; longer sums don't have a trailing zero*)
    73 fun mk_sum T [] = mk_number T 0
    74   | mk_sum T [t, u] = mk_plus (t, u)
    75   | mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
    76 
    77 (*this version ALWAYS includes a trailing zero*)
    78 fun long_mk_sum T [] = mk_number T 0
    79   | long_mk_sum T (t :: ts) = mk_plus (t, mk_sum T ts);
    80 
    81 (*decompose additions AND subtractions as a sum*)
    82 fun dest_summing (pos, Const (@{const_name Groups.plus}, _) $ t $ u, ts) =
    83       dest_summing (pos, t, dest_summing (pos, u, ts))
    84   | dest_summing (pos, Const (@{const_name Groups.minus}, _) $ t $ u, ts) =
    85       dest_summing (pos, t, dest_summing (not pos, u, ts))
    86   | dest_summing (pos, t, ts) = (if pos then t else mk_minus t) :: ts;
    87 
    88 fun dest_sum t = dest_summing (true, t, []);
    89 
    90 
    91 (* various auxiliary and legacy *)
    92 
    93 fun prove_conv_nohyps tacs ctxt (t, u) =
    94   if t aconv u then NONE
    95   else let val eq = HOLogic.mk_Trueprop (HOLogic.mk_eq (t, u))
    96   in SOME (Goal.prove ctxt [] [] eq (K (EVERY tacs))) end;
    97 
    98 fun prove_conv tacs ctxt (_: thm list) = prove_conv_nohyps tacs ctxt;
    99 
   100 fun prove_conv2 expand_tac norm_tac ctxt tu = (* FIXME avoid Drule.export_without_context *)
   101   mk_meta_eq (Drule.export_without_context (Goal.prove ctxt [] []
   102       (HOLogic.mk_Trueprop (HOLogic.mk_eq tu))
   103     (K (EVERY [expand_tac, norm_tac ctxt]))));
   104 
   105 fun simp_all_tac rules ctxt =
   106   ALLGOALS (safe_simp_tac (put_simpset HOL_ss ctxt addsimps rules));
   107 
   108 fun simplify_meta_eq rules ctxt =
   109   simplify (put_simpset HOL_basic_ss ctxt addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2})
   110     o mk_meta_eq;
   111 
   112 end;