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