author | kleing |
Mon, 19 Apr 2004 09:31:00 +0200 | |
changeset 14626 | dfb8d2977263 |
parent 14607 | 099575a938e5 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
10214 | 1 |
(* Title: HOL/NatArith.thy |
2 |
ID: $Id$ |
|
13297 | 3 |
Author: Tobias Nipkow and Markus Wenzel |
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
*) |
|
10214 | 6 |
|
13297 | 7 |
header {* More arithmetic on natural numbers *} |
10214 | 8 |
|
9 |
theory NatArith = Nat |
|
10 |
files "arith_data.ML": |
|
11 |
||
12 |
setup arith_setup |
|
13 |
||
13297 | 14 |
|
11655 | 15 |
lemma pred_nat_trancl_eq_le: "((m, n) : pred_nat^*) = (m <= n)" |
14208 | 16 |
by (simp add: less_eq reflcl_trancl [symmetric] |
17 |
del: reflcl_trancl, arith) |
|
11454
7514e5e21cb8
Hilbert restructuring: Wellfounded_Relations no longer needs Hilbert_Choice
paulson
parents:
11324
diff
changeset
|
18 |
|
10214 | 19 |
lemma nat_diff_split: |
10599 | 20 |
"P(a - b::nat) = ((a<b --> P 0) & (ALL d. a = b + d --> P d))" |
13297 | 21 |
-- {* elimination of @{text -} on @{text nat} *} |
22 |
by (cases "a<b" rule: case_split) |
|
23 |
(auto simp add: diff_is_0_eq [THEN iffD2]) |
|
11324 | 24 |
|
25 |
lemma nat_diff_split_asm: |
|
26 |
"P(a - b::nat) = (~ (a < b & ~ P 0 | (EX d. a = b + d & ~ P d)))" |
|
13297 | 27 |
-- {* elimination of @{text -} on @{text nat} in assumptions *} |
11324 | 28 |
by (simp split: nat_diff_split) |
10214 | 29 |
|
11164 | 30 |
ML {* |
31 |
val nat_diff_split = thm "nat_diff_split"; |
|
11324 | 32 |
val nat_diff_split_asm = thm "nat_diff_split_asm"; |
13499 | 33 |
*} |
34 |
(* Careful: arith_tac produces counter examples! |
|
11181
d04f57b91166
renamed addaltern to addafter, addSaltern to addSafter
oheimb
parents:
11164
diff
changeset
|
35 |
fun add_arith cs = cs addafter ("arith_tac", arith_tac); |
14607 | 36 |
TODO: use arith_tac for force_tac in Provers/clasimp.ML *) |
10214 | 37 |
|
38 |
lemmas [arith_split] = nat_diff_split split_min split_max |
|
39 |
||
11164 | 40 |
|
14607 | 41 |
subsection {* Generic summation indexed over natural numbers *} |
13297 | 42 |
|
43 |
consts |
|
44 |
Summation :: "(nat => 'a::{zero, plus}) => nat => 'a" |
|
45 |
primrec |
|
46 |
"Summation f 0 = 0" |
|
47 |
"Summation f (Suc n) = Summation f n + f n" |
|
48 |
||
49 |
syntax |
|
50 |
"_Summation" :: "idt => nat => 'a => nat" ("\<Sum>_<_. _" [0, 51, 10] 10) |
|
51 |
translations |
|
52 |
"\<Sum>i < n. b" == "Summation (\<lambda>i. b) n" |
|
53 |
||
54 |
theorem Summation_step: |
|
55 |
"0 < n ==> (\<Sum>i < n. f i) = (\<Sum>i < n - 1. f i) + f (n - 1)" |
|
56 |
by (induct n) simp_all |
|
57 |
||
10214 | 58 |
end |