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