src/HOL/Tools/nat_arith.ML
author huffman
Fri Jul 27 17:59:18 2012 +0200 (2012-07-27)
changeset 48560 e0875d956a6b
parent 48559 686cc7c47589
child 48561 12aa0cb2b447
permissions -rw-r--r--
replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
     1 (* Author: Markus Wenzel, Stefan Berghofer, and Tobias Nipkow
     2    Author: Brian Huffman
     3 
     4 Basic arithmetic for natural numbers.
     5 *)
     6 
     7 signature NAT_ARITH =
     8 sig
     9   val cancel_diff_conv: conv
    10   val cancel_eq_conv: conv
    11   val cancel_le_conv: conv
    12   val cancel_less_conv: conv
    13   (* legacy functions: *)
    14   val mk_sum: term list -> term
    15   val mk_norm_sum: term list -> term
    16   val dest_sum: term -> term list
    17 end;
    18 
    19 structure Nat_Arith: NAT_ARITH =
    20 struct
    21 
    22 (** abstract syntax of structure nat: 0, Suc, + **)
    23 
    24 val mk_plus = HOLogic.mk_binop @{const_name Groups.plus};
    25 val dest_plus = HOLogic.dest_bin @{const_name Groups.plus} HOLogic.natT;
    26 
    27 fun mk_sum [] = HOLogic.zero
    28   | mk_sum [t] = t
    29   | mk_sum (t :: ts) = mk_plus (t, mk_sum ts);
    30 
    31 (*normal form of sums: Suc (... (Suc (a + (b + ...))))*)
    32 fun mk_norm_sum ts =
    33   let val (ones, sums) = List.partition (equal HOLogic.Suc_zero) ts in
    34     funpow (length ones) HOLogic.mk_Suc (mk_sum sums)
    35   end;
    36 
    37 fun dest_sum tm =
    38   if HOLogic.is_zero tm then []
    39   else
    40     (case try HOLogic.dest_Suc tm of
    41       SOME t => HOLogic.Suc_zero :: dest_sum t
    42     | NONE =>
    43         (case try dest_plus tm of
    44           SOME (t, u) => dest_sum t @ dest_sum u
    45         | NONE => [tm]));
    46 
    47 val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
    48       by (simp only: add_ac)}
    49 val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
    50       by (simp only: add_ac)}
    51 val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
    52       by (simp only: add_Suc_right)}
    53 val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
    54       by (simp only: add_0_right)}
    55 
    56 val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
    57 
    58 fun move_to_front path = Conv.every_conv
    59     [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
    60      Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
    61 
    62 fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
    63       add_atoms (add1::path) x #> add_atoms (add2::path) y
    64   | add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) =
    65       add_atoms (suc1::path) x
    66   | add_atoms _ (Const (@{const_name Groups.zero}, _)) = I
    67   | add_atoms path x = cons (x, path)
    68 
    69 fun atoms t = add_atoms [] t []
    70 
    71 exception Cancel
    72 
    73 fun find_common ord xs ys =
    74   let
    75     fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
    76         (case ord (x, y) of
    77           EQUAL => (px, py)
    78         | LESS => find xs' ys
    79         | GREATER => find xs ys')
    80       | find _ _ = raise Cancel
    81     fun ord' ((x, _), (y, _)) = ord (x, y)
    82   in
    83     find (sort ord' xs) (sort ord' ys)
    84   end
    85 
    86 fun cancel_conv rule ct =
    87   let
    88     val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
    89     val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
    90     val lconv = move_to_front lpath
    91     val rconv = move_to_front rpath
    92     val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
    93     val conv = conv1 then_conv Conv.rewr_conv rule
    94   in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
    95 
    96 val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel})
    97 val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
    98 val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left})
    99 val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left})
   100 
   101 end;