equal
deleted
inserted
replaced
3 Copyright : 2001 University of Edinburgh |
3 Copyright : 2001 University of Edinburgh |
4 Description : MacLaurin series |
4 Description : MacLaurin series |
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
5 Conversion to Isar and new proofs by Lawrence C Paulson, 2004 |
6 *) |
6 *) |
7 |
7 |
8 theory MacLaurin = Log: |
8 theory MacLaurin |
|
9 import Log |
|
10 begin |
9 |
11 |
10 lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" |
12 lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" |
11 by (induct_tac "n", auto) |
13 by (induct_tac "n", auto) |
12 |
14 |
13 lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" |
15 lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f" |