src/HOL/Tools/nat_arith.ML
author haftmann
Fri Feb 19 14:47:01 2010 +0100 (2010-02-19)
changeset 35267 8dfd816713c6
parent 35092 cfe605c54e50
child 38715 6513ea67d95d
permissions -rw-r--r--
moved remaning class operations from Algebras.thy to Groups.thy
haftmann@30496
     1
(* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
wenzelm@9436
     2
haftmann@30496
     3
Basic arithmetic for natural numbers.
wenzelm@9436
     4
*)
wenzelm@9436
     5
haftmann@30496
     6
signature NAT_ARITH =
haftmann@26101
     7
sig
haftmann@26101
     8
  val mk_sum: term list -> term
haftmann@26101
     9
  val mk_norm_sum: term list -> term
haftmann@26101
    10
  val dest_sum: term -> term list
haftmann@26101
    11
haftmann@26101
    12
  val nat_cancel_sums_add: simproc list
haftmann@26101
    13
  val nat_cancel_sums: simproc list
haftmann@26101
    14
  val setup: Context.generic -> Context.generic
haftmann@26101
    15
end;
wenzelm@9436
    16
haftmann@30496
    17
structure Nat_Arith: NAT_ARITH =
wenzelm@9436
    18
struct
wenzelm@9436
    19
wenzelm@9436
    20
(** abstract syntax of structure nat: 0, Suc, + **)
wenzelm@9436
    21
haftmann@35267
    22
val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
haftmann@35267
    23
val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
haftmann@26101
    24
wenzelm@9436
    25
fun mk_sum [] = HOLogic.zero
wenzelm@9436
    26
  | mk_sum [t] = t
wenzelm@9436
    27
  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
wenzelm@9436
    28
wenzelm@9436
    29
(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
wenzelm@9436
    30
fun mk_norm_sum ts =
haftmann@21621
    31
  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
wenzelm@9436
    32
    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
wenzelm@9436
    33
  end;
wenzelm@9436
    34
wenzelm@9436
    35
fun dest_sum tm =
wenzelm@9436
    36
  if HOLogic.is_zero tm then []
wenzelm@9436
    37
  else
wenzelm@9436
    38
    (case try HOLogic.dest_Suc tm of
haftmann@21621
    39
      SOME t => HOLogic.Suc_zero :: dest_sum t
skalberg@15531
    40
    | NONE =>
wenzelm@9436
    41
        (case try dest_plus tm of
skalberg@15531
    42
          SOME (t, u) => dest_sum t @ dest_sum u
skalberg@15531
    43
        | NONE => [tm]));
wenzelm@9436
    44
webertj@20217
    45
wenzelm@9436
    46
(** cancel common summands **)
wenzelm@9436
    47
haftmann@30496
    48
structure CommonCancelSums =
wenzelm@9436
    49
struct
wenzelm@9436
    50
  val mk_sum = mk_norm_sum;
wenzelm@9436
    51
  val dest_sum = dest_sum;
haftmann@30496
    52
  val prove_conv = Arith_Data.prove_conv2;
haftmann@35047
    53
  val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
haftmann@35064
    54
    @{thm Nat.add_0}, @{thm Nat.add_0_right}];
haftmann@30496
    55
  val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
wenzelm@18328
    56
  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
haftmann@30496
    57
  fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
haftmann@30496
    58
    in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
wenzelm@9436
    59
end;
wenzelm@9436
    60
wenzelm@9436
    61
structure EqCancelSums = CancelSumsFun
wenzelm@9436
    62
(struct
haftmann@30496
    63
  open CommonCancelSums;
wenzelm@9436
    64
  val mk_bal = HOLogic.mk_eq;
wenzelm@9436
    65
  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
haftmann@22838
    66
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
wenzelm@9436
    67
end);
wenzelm@9436
    68
wenzelm@9436
    69
structure LessCancelSums = CancelSumsFun
wenzelm@9436
    70
(struct
haftmann@30496
    71
  open CommonCancelSums;
haftmann@35092
    72
  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
haftmann@35092
    73
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
haftmann@22838
    74
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
wenzelm@9436
    75
end);
wenzelm@9436
    76
wenzelm@9436
    77
structure LeCancelSums = CancelSumsFun
wenzelm@9436
    78
(struct
haftmann@30496
    79
  open CommonCancelSums;
haftmann@35092
    80
  val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
haftmann@35092
    81
  val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
haftmann@22838
    82
  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
wenzelm@9436
    83
end);
wenzelm@9436
    84
wenzelm@9436
    85
structure DiffCancelSums = CancelSumsFun
wenzelm@9436
    86
(struct
haftmann@30496
    87
  open CommonCancelSums;
haftmann@35267
    88
  val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
haftmann@35267
    89
  val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
haftmann@22838
    90
  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
wenzelm@9436
    91
end);
wenzelm@9436
    92
haftmann@26101
    93
val nat_cancel_sums_add =
wenzelm@32010
    94
  [Simplifier.simproc @{theory} "nateq_cancel_sums"
haftmann@26101
    95
     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
haftmann@26101
    96
     (K EqCancelSums.proc),
wenzelm@32010
    97
   Simplifier.simproc @{theory} "natless_cancel_sums"
haftmann@26101
    98
     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
haftmann@26101
    99
     (K LessCancelSums.proc),
wenzelm@32010
   100
   Simplifier.simproc @{theory} "natle_cancel_sums"
haftmann@26101
   101
     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
haftmann@26101
   102
     (K LeCancelSums.proc)];
wenzelm@9436
   103
wenzelm@9436
   104
val nat_cancel_sums = nat_cancel_sums_add @
wenzelm@32010
   105
  [Simplifier.simproc @{theory} "natdiff_cancel_sums"
haftmann@26101
   106
    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
haftmann@26101
   107
    (K DiffCancelSums.proc)];
wenzelm@9436
   108
haftmann@26101
   109
val setup =
wenzelm@24095
   110
  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
wenzelm@24076
   111
wenzelm@24095
   112
end;