src/HOL/Tools/nat_arith.ML
author huffman
Fri Jul 27 17:57:31 2012 +0200 (2012-07-27)
changeset 48559 686cc7c47589
parent 48372 868dc809c8a2
child 48560 e0875d956a6b
permissions -rw-r--r--
give Nat_Arith simprocs proper name bindings by using simproc_setup
     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   val nateq_cancel_sums: simpset -> cterm -> thm option
    12   val natless_cancel_sums: simpset -> cterm -> thm option
    13   val natle_cancel_sums: simpset -> cterm -> thm option
    14   val natdiff_cancel_sums: simpset -> cterm -> thm option
    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 Groups.plus};
    23 val dest_plus = HOLogic.dest_bin @{const_name Groups.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 mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    53   val norm_tac1 = Arith_Data.simp_all_tac [@{thm add_Suc}, @{thm add_Suc_right},
    54     @{thm Nat.add_0}, @{thm Nat.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 end;
    58 
    59 structure EqCancelSums = CancelSumsFun
    60 (struct
    61   open CommonCancelSums;
    62   val mk_bal = HOLogic.mk_eq;
    63   val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT;
    64   val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel};
    65 end);
    66 
    67 structure LessCancelSums = CancelSumsFun
    68 (struct
    69   open CommonCancelSums;
    70   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less};
    71   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less} HOLogic.natT;
    72   val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_less};
    73 end);
    74 
    75 structure LeCancelSums = CancelSumsFun
    76 (struct
    77   open CommonCancelSums;
    78   val mk_bal = HOLogic.mk_binrel @{const_name Orderings.less_eq};
    79   val dest_bal = HOLogic.dest_bin @{const_name Orderings.less_eq} HOLogic.natT;
    80   val cancel_rule = mk_meta_eq @{thm nat_add_left_cancel_le};
    81 end);
    82 
    83 structure DiffCancelSums = CancelSumsFun
    84 (struct
    85   open CommonCancelSums;
    86   val mk_bal = HOLogic.mk_binop @{const_name Groups.minus};
    87   val dest_bal = HOLogic.dest_bin @{const_name Groups.minus} HOLogic.natT;
    88   val cancel_rule = mk_meta_eq @{thm diff_cancel};
    89 end);
    90 
    91 fun nateq_cancel_sums ss = EqCancelSums.proc ss o Thm.term_of
    92 fun natless_cancel_sums ss = LessCancelSums.proc ss o Thm.term_of
    93 fun natle_cancel_sums ss = LeCancelSums.proc ss o Thm.term_of
    94 fun natdiff_cancel_sums ss = DiffCancelSums.proc ss o Thm.term_of
    95 
    96 end;