|
10214
|
1 |
(* Title: HOL/NatArith.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
|
|
|
4 |
Setup arithmetic proof procedures.
|
|
|
5 |
*)
|
|
|
6 |
|
|
|
7 |
theory NatArith = Nat
|
|
|
8 |
files "arith_data.ML":
|
|
|
9 |
|
|
|
10 |
setup arith_setup
|
|
|
11 |
|
|
|
12 |
(*elimination of `-' on nat*)
|
|
|
13 |
lemma nat_diff_split:
|
|
|
14 |
"P(a - b::nat) = (ALL d. (a<b --> P 0) & (a = b + d --> P d))"
|
|
|
15 |
by (cases "a < b" rule: case_split) (auto simp add: diff_is_0_eq [THEN iffD2])
|
|
|
16 |
|
|
|
17 |
ML {* val nat_diff_split = thm "nat_diff_split" *}
|
|
|
18 |
|
|
|
19 |
lemmas [arith_split] = nat_diff_split split_min split_max
|
|
|
20 |
|
|
|
21 |
end
|