src/HOL/Tools/nat_arith.ML
author wenzelm
Sat Dec 14 17:28:05 2013 +0100 (2013-12-14)
changeset 54742 7a86358a3c0b
parent 48571 d68b74435605
child 57514 bdc2c6b40bf2
permissions -rw-r--r--
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
clarified tool context in some boundary cases;
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
wenzelm@54742
     9
  val cancel_diff_conv: Proof.context -> conv
wenzelm@54742
    10
  val cancel_eq_conv: Proof.context -> conv
wenzelm@54742
    11
  val cancel_le_conv: Proof.context -> conv
wenzelm@54742
    12
  val cancel_less_conv: Proof.context -> conv
haftmann@26101
    13
end;
wenzelm@9436
    14
haftmann@30496
    15
structure Nat_Arith: NAT_ARITH =
wenzelm@9436
    16
struct
wenzelm@9436
    17
huffman@48560
    18
val add1 = @{lemma "(A::'a::comm_monoid_add) == k + a ==> A + b == k + (a + b)"
huffman@48560
    19
      by (simp only: add_ac)}
huffman@48560
    20
val add2 = @{lemma "(B::'a::comm_monoid_add) == k + b ==> a + B == k + (a + b)"
huffman@48560
    21
      by (simp only: add_ac)}
huffman@48560
    22
val suc1 = @{lemma "A == k + a ==> Suc A == k + Suc a"
huffman@48560
    23
      by (simp only: add_Suc_right)}
huffman@48560
    24
val rule0 = @{lemma "(a::'a::comm_monoid_add) == a + 0"
huffman@48560
    25
      by (simp only: add_0_right)}
webertj@20217
    26
huffman@48560
    27
val norm_rules = map mk_meta_eq @{thms add_0_left add_0_right}
wenzelm@9436
    28
wenzelm@54742
    29
fun move_to_front ctxt path = Conv.every_conv
huffman@48560
    30
    [Conv.rewr_conv (Library.foldl (op RS) (rule0, path)),
wenzelm@54742
    31
     Conv.arg_conv (Raw_Simplifier.rewrite ctxt false norm_rules)]
wenzelm@9436
    32
huffman@48560
    33
fun add_atoms path (Const (@{const_name Groups.plus}, _) $ x $ y) =
huffman@48560
    34
      add_atoms (add1::path) x #> add_atoms (add2::path) y
huffman@48560
    35
  | add_atoms path (Const (@{const_name Nat.Suc}, _) $ x) =
huffman@48560
    36
      add_atoms (suc1::path) x
huffman@48560
    37
  | add_atoms _ (Const (@{const_name Groups.zero}, _)) = I
huffman@48560
    38
  | add_atoms path x = cons (x, path)
huffman@48560
    39
huffman@48560
    40
fun atoms t = add_atoms [] t []
huffman@48560
    41
huffman@48560
    42
exception Cancel
wenzelm@9436
    43
huffman@48560
    44
fun find_common ord xs ys =
huffman@48560
    45
  let
huffman@48560
    46
    fun find (xs as (x, px)::xs') (ys as (y, py)::ys') =
huffman@48560
    47
        (case ord (x, y) of
huffman@48560
    48
          EQUAL => (px, py)
huffman@48560
    49
        | LESS => find xs' ys
huffman@48560
    50
        | GREATER => find xs ys')
huffman@48560
    51
      | find _ _ = raise Cancel
huffman@48560
    52
    fun ord' ((x, _), (y, _)) = ord (x, y)
huffman@48560
    53
  in
huffman@48560
    54
    find (sort ord' xs) (sort ord' ys)
huffman@48560
    55
  end
wenzelm@9436
    56
wenzelm@54742
    57
fun cancel_conv rule ctxt ct =
huffman@48560
    58
  let
huffman@48560
    59
    val ((_, lhs), rhs) = (apfst dest_comb o dest_comb) (Thm.term_of ct)
huffman@48560
    60
    val (lpath, rpath) = find_common Term_Ord.term_ord (atoms lhs) (atoms rhs)
wenzelm@54742
    61
    val lconv = move_to_front ctxt lpath
wenzelm@54742
    62
    val rconv = move_to_front ctxt rpath
huffman@48560
    63
    val conv1 = Conv.combination_conv (Conv.arg_conv lconv) rconv
huffman@48560
    64
    val conv = conv1 then_conv Conv.rewr_conv rule
huffman@48571
    65
  in conv ct end
huffman@48571
    66
    handle Cancel => raise CTERM ("no_conversion", [])
wenzelm@9436
    67
huffman@48560
    68
val cancel_diff_conv = cancel_conv (mk_meta_eq @{thm diff_cancel})
huffman@48560
    69
val cancel_eq_conv = cancel_conv (mk_meta_eq @{thm add_left_cancel})
huffman@48560
    70
val cancel_le_conv = cancel_conv (mk_meta_eq @{thm add_le_cancel_left})
huffman@48560
    71
val cancel_less_conv = cancel_conv (mk_meta_eq @{thm add_less_cancel_left})
wenzelm@24076
    72
wenzelm@24095
    73
end;