src/HOL/NatArith.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 10214 77349ed89f45
child 10599 2df753cf86e9
permissions -rw-r--r--
hide many names from Datatype_Universe.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
10214
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/NatArith.thy
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     2
    ID:         $Id$
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     3
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     4
Setup arithmetic proof procedures.
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     5
*)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     6
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     7
theory NatArith = Nat
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     8
files "arith_data.ML":
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
     9
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    10
setup arith_setup
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    11
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    12
(*elimination of `-' on nat*)
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    13
lemma nat_diff_split:
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    14
    "P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    15
  by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    16
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    17
ML {* val nat_diff_split = thm "nat_diff_split" *}
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    18
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    19
lemmas [arith_split] = nat_diff_split split_min split_max
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    20
77349ed89f45 *** empty log message ***
nipkow
parents:
diff changeset
    21
end