src/HOL/NatArith.thy
author nipkow
Mon Aug 16 14:22:27 2004 +0200 (2004-08-16)
changeset 15131 c69542757a4d
parent 15048 11b4dce71d73
child 15140 322485b816ac
permissions -rw-r--r--
New theory header syntax.
nipkow@10214
     1
(*  Title:      HOL/NatArith.thy
nipkow@10214
     2
    ID:         $Id$
wenzelm@13297
     3
    Author:     Tobias Nipkow and Markus Wenzel
wenzelm@13297
     4
*)
nipkow@10214
     5
wenzelm@13297
     6
header {* More arithmetic on natural numbers *}
nipkow@10214
     7
nipkow@15131
     8
theory NatArith
nipkow@15131
     9
import Nat
nipkow@15131
    10
files "arith_data.ML"
nipkow@15131
    11
begin
nipkow@10214
    12
nipkow@10214
    13
setup arith_setup
nipkow@10214
    14
wenzelm@13297
    15
wenzelm@11655
    16
lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)"
paulson@14208
    17
by (simp add: less_eq reflcl_trancl [symmetric]
paulson@14208
    18
            del: reflcl_trancl, arith)
paulson@11454
    19
nipkow@10214
    20
lemma nat_diff_split:
paulson@10599
    21
    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
wenzelm@13297
    22
    -- {* elimination of @{text -} on @{text nat} *}
wenzelm@13297
    23
  by (cases "a<b" rule: case_split)
wenzelm@13297
    24
    (auto simp add: diff_is_0_eq [THEN iffD2])
paulson@11324
    25
paulson@11324
    26
lemma nat_diff_split_asm:
paulson@11324
    27
    "P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))"
wenzelm@13297
    28
    -- {* elimination of @{text -} on @{text nat} in assumptions *}
paulson@11324
    29
  by (simp split: nat_diff_split)
nipkow@10214
    30
oheimb@11164
    31
ML {*
oheimb@11164
    32
 val nat_diff_split = thm "nat_diff_split";
paulson@11324
    33
 val nat_diff_split_asm = thm "nat_diff_split_asm";
nipkow@13499
    34
*}
nipkow@13499
    35
(* Careful: arith_tac produces counter examples!
oheimb@11181
    36
fun add_arith cs = cs addafter ("arith_tac", arith_tac);
wenzelm@14607
    37
TODO: use arith_tac for force_tac in Provers/clasimp.ML *)
nipkow@10214
    38
nipkow@10214
    39
lemmas [arith_split] = nat_diff_split split_min split_max
nipkow@10214
    40
nipkow@10214
    41
end