| author | paulson |
| Fri, 27 Sep 2002 10:35:10 +0200 | |
| changeset 13592 | dfe0c7191125 |
| parent 13575 | ecb6ecd9af13 |
| child 13685 | 0b8fbcf65d73 |
| permissions | -rw-r--r-- |
| 12023 | 1 |
|
2 |
header {* Integer arithmetic *}
|
|
3 |
||
|
9436
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9214
diff
changeset
|
4 |
theory IntArith = Bin |
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9214
diff
changeset
|
5 |
files ("int_arith1.ML") ("int_arith2.ML"):
|
|
62bb04ab4b01
rearranged setup of arithmetic procedures, avoiding global reference values;
wenzelm
parents:
9214
diff
changeset
|
6 |
|
| 12023 | 7 |
use "int_arith1.ML" |
8 |
setup int_arith_setup |
|
9 |
use "int_arith2.ML" |
|
10 |
declare zabs_split [arith_split] |
|
11 |
||
| 13575 | 12 |
lemma split_nat[arith_split]: |
13 |
"P(nat(i::int)) = ((ALL n. i = int n \<longrightarrow> P n) & (i < 0 \<longrightarrow> P 0))" |
|
14 |
(is "?P = (?L & ?R)") |
|
15 |
proof (cases "i < 0") |
|
16 |
case True thus ?thesis by simp |
|
17 |
next |
|
18 |
case False |
|
19 |
have "?P = ?L" |
|
20 |
proof |
|
21 |
assume ?P thus ?L using False by clarsimp |
|
22 |
next |
|
23 |
assume ?L thus ?P using False by simp |
|
24 |
qed |
|
25 |
with False show ?thesis by simp |
|
26 |
qed |
|
27 |
||
| 7707 | 28 |
end |