src/HOL/NatArith.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10599 2df753cf86e9
child 11164 03f5dc539fd9
permissions -rw-r--r--
improved theory reference in comment
nipkow@10214
     1
(*  Title:      HOL/NatArith.thy
nipkow@10214
     2
    ID:         $Id$
nipkow@10214
     3
nipkow@10214
     4
Setup arithmetic proof procedures.
nipkow@10214
     5
*)
nipkow@10214
     6
nipkow@10214
     7
theory NatArith = Nat
nipkow@10214
     8
files "arith_data.ML":
nipkow@10214
     9
nipkow@10214
    10
setup arith_setup
nipkow@10214
    11
nipkow@10214
    12
(*elimination of `-' on nat*)
nipkow@10214
    13
lemma nat_diff_split:
paulson@10599
    14
    "P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))"
nipkow@10214
    15
  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
nipkow@10214
    16
nipkow@10214
    17
ML {* val nat_diff_split = thm "nat_diff_split" *}
nipkow@10214
    18
nipkow@10214
    19
lemmas [arith_split] = nat_diff_split split_min split_max
nipkow@10214
    20
nipkow@10214
    21
end