src/HOL/Tools/nat_arith.ML
changeset 30496 7cdcc9dd95cb
parent 29302 eb782d1dc07c
child 32010 cb1a1c94b4cd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Thu Mar 12 18:01:26 2009 +0100
     1.3 @@ -0,0 +1,112 @@
     1.4 +(* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
     1.5 +
     1.6 +Basic arithmetic for natural numbers.
     1.7 +*)
     1.8 +
     1.9 +signature NAT_ARITH =
    1.10 +sig
    1.11 +  val mk_sum: term list -> term
    1.12 +  val mk_norm_sum: term list -> term
    1.13 +  val dest_sum: term -> term list
    1.14 +
    1.15 +  val nat_cancel_sums_add: simproc list
    1.16 +  val nat_cancel_sums: simproc list
    1.17 +  val setup: Context.generic -> Context.generic
    1.18 +end;
    1.19 +
    1.20 +structure Nat_Arith: NAT_ARITH =
    1.21 +struct
    1.22 +
    1.23 +(** abstract syntax of structure nat: 0, Suc, + **)
    1.24 +
    1.25 +val mk_plus = HOLogic.mk_binop @{const_name HOL.plus};
    1.26 +val dest_plus = HOLogic.dest_bin @{const_name HOL.plus} HOLogic.natT;
    1.27 +
    1.28 +fun mk_sum [] = HOLogic.zero
    1.29 +  | mk_sum [t] = t
    1.30 +  | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    1.31 +
    1.32 +(*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    1.33 +fun mk_norm_sum ts =
    1.34 +  let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
    1.35 +    funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    1.36 +  end;
    1.37 +
    1.38 +fun dest_sum tm =
    1.39 +  if HOLogic.is_zero tm then []
    1.40 +  else
    1.41 +    (case try HOLogic.dest_Suc tm of
    1.42 +      SOME t => HOLogic.Suc_zero :: dest_sum t
    1.43 +    | NONE =>
    1.44 +        (case try dest_plus tm of
    1.45 +          SOME (t, u) => dest_sum t @ dest_sum u
    1.46 +        | NONE => [tm]));
    1.47 +
    1.48 +
    1.49 +(** cancel common summands **)
    1.50 +
    1.51 +structure CommonCancelSums =
    1.52 +struct
    1.53 +  val mk_sum = mk_norm_sum;
    1.54 +  val dest_sum = dest_sum;
    1.55 +  val prove_conv = Arith_Data.prove_conv2;
    1.56 +  val norm_tac1 = Arith_Data.simp_all_tac [@{thm "add_Suc"}, @{thm "add_Suc_right"},
    1.57 +    @{thm "add_0"}, @{thm "add_0_right"}];
    1.58 +  val norm_tac2 = Arith_Data.simp_all_tac @{thms add_ac};
    1.59 +  fun norm_tac ss = norm_tac1 ss THEN norm_tac2 ss;
    1.60 +  fun gen_uncancel_tac rule = let val rule' = rule RS @{thm subst_equals}
    1.61 +    in fn ct => rtac (instantiate' [] [NONE, SOME ct] rule') 1 end;
    1.62 +end;
    1.63 +
    1.64 +structure EqCancelSums = CancelSumsFun
    1.65 +(struct
    1.66 +  open CommonCancelSums;
    1.67 +  val mk_bal = HOLogic.mk_eq;
    1.68 +  val dest_bal = HOLogic.dest_bin "op =" HOLogic.natT;
    1.69 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
    1.70 +end);
    1.71 +
    1.72 +structure LessCancelSums = CancelSumsFun
    1.73 +(struct
    1.74 +  open CommonCancelSums;
    1.75 +  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less};
    1.76 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less} HOLogic.natT;
    1.77 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_less"};
    1.78 +end);
    1.79 +
    1.80 +structure LeCancelSums = CancelSumsFun
    1.81 +(struct
    1.82 +  open CommonCancelSums;
    1.83 +  val mk_bal = HOLogic.mk_binrel @{const_name HOL.less_eq};
    1.84 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.less_eq} HOLogic.natT;
    1.85 +  val uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel_le"};
    1.86 +end);
    1.87 +
    1.88 +structure DiffCancelSums = CancelSumsFun
    1.89 +(struct
    1.90 +  open CommonCancelSums;
    1.91 +  val mk_bal = HOLogic.mk_binop @{const_name HOL.minus};
    1.92 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.minus} HOLogic.natT;
    1.93 +  val uncancel_tac = gen_uncancel_tac @{thm "diff_cancel"};
    1.94 +end);
    1.95 +
    1.96 +val nat_cancel_sums_add =
    1.97 +  [Simplifier.simproc (the_context ()) "nateq_cancel_sums"
    1.98 +     ["(l::nat) + m = n", "(l::nat) = m + n", "Suc m = n", "m = Suc n"]
    1.99 +     (K EqCancelSums.proc),
   1.100 +   Simplifier.simproc (the_context ()) "natless_cancel_sums"
   1.101 +     ["(l::nat) + m < n", "(l::nat) < m + n", "Suc m < n", "m < Suc n"]
   1.102 +     (K LessCancelSums.proc),
   1.103 +   Simplifier.simproc (the_context ()) "natle_cancel_sums"
   1.104 +     ["(l::nat) + m <= n", "(l::nat) <= m + n", "Suc m <= n", "m <= Suc n"]
   1.105 +     (K LeCancelSums.proc)];
   1.106 +
   1.107 +val nat_cancel_sums = nat_cancel_sums_add @
   1.108 +  [Simplifier.simproc (the_context ()) "natdiff_cancel_sums"
   1.109 +    ["((l::nat) + m) - n", "(l::nat) - (m + n)", "Suc m - n", "m - Suc n"]
   1.110 +    (K DiffCancelSums.proc)];
   1.111 +
   1.112 +val setup =
   1.113 +  Simplifier.map_ss (fn ss => ss addsimprocs nat_cancel_sums);
   1.114 +
   1.115 +end;