src/HOL/NatArith.thy
author nipkow
Fri, 13 Oct 2000 08:28:21 +0200
changeset 10214 77349ed89f45
child 10599 2df753cf86e9
permissions -rw-r--r--
*** empty log message ***

(*  Title:      HOL/NatArith.thy
    ID:         $Id$

Setup arithmetic proof procedures.
*)

theory NatArith = Nat
files "arith_data.ML":

setup arith_setup

(*elimination of `-' on nat*)
lemma nat_diff_split:
    "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])

ML {* val nat_diff_split = thm "nat_diff_split" *}

lemmas [arith_split] = nat_diff_split split_min split_max

end