src/HOL/Tools/nat_arith.ML
author huffman
Fri Jul 27 19:27:21 2012 +0200 (2012-07-27)
changeset 48561 12aa0cb2b447
parent 48560 e0875d956a6b
child 48571 d68b74435605
permissions -rw-r--r--
move ML functions from nat_arith.ML to Divides.thy, which is the only place they are used
     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 end;
    14 
    15 structure Nat_Arith: NAT_ARITH =
    16 struct
    17 
    18 val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
    19       by (simp only: add_ac)}
    20 val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
    21       by (simp only: add_ac)}
    22 val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
    23       by (simp only: add_Suc_right)}
    24 val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
    25       by (simp only: add_0_right)}
    26 
    27 val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
    28 
    29 fun move_to_front path = Conv.every_conv
    30     [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
    31      Conv.arg_conv (Raw_Simplifier.rewrite false norm_rules)]
    32 
    33 fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
    34       add_atoms (add1::path) x #> add_atoms (add2::path) y
    35   | add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) =
    36       add_atoms (suc1::path) x
    37   | add_atoms _ (Const (@{const_name Groups.zero}, _)) = I
    38   | add_atoms path x = cons (x, path)
    39 
    40 fun atoms t = add_atoms [] t []
    41 
    42 exception Cancel
    43 
    44 fun find_common ord xs ys =
    45   let
    46     fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
    47         (case ord (x, y) of
    48           EQUAL => (px, py)
    49         | LESS => find xs' ys
    50         | GREATER => find xs ys')
    51       | find _ _ = raise Cancel
    52     fun ord' ((x, _), (y, _)) = ord (x, y)
    53   in
    54     find (sort ord' xs) (sort ord' ys)
    55   end
    56 
    57 fun cancel_conv rule ct =
    58   let
    59     val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
    60     val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
    61     val lconv = move_to_front lpath
    62     val rconv = move_to_front rpath
    63     val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
    64     val conv = conv1 then_conv Conv.rewr_conv rule
    65   in conv ct handle Cancel => raise CTERM ("no_conversion", []) end
    66 
    67 val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel})
    68 val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
    69 val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left})
    70 val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left})
    71 
    72 end;