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