summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Isar_examples/Summation.thy

author | wenzelm |

Sat Sep 04 21:13:01 1999 +0200 (1999-09-04) | |

changeset 7480 | 0a0e0dbe1269 |

parent 7443 | e5356e73f57a |

child 7748 | 5b9c45b21782 |

permissions | -rw-r--r-- |

replaced ?? by ?;

1 (* Title: HOL/Isar_examples/Summation.thy

2 ID: $Id$

3 Author: Markus Wenzel

5 Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the

6 original scripts). Demonstrates mathematical induction together with

7 calculational proof.

8 *)

11 theory Summation = Main:;

14 section {* Summing natural numbers *};

16 text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *};

18 consts

19 sum :: "[nat => nat, nat] => nat";

21 primrec

22 "sum f 0 = 0"

23 "sum f (Suc n) = f n + sum f n";

25 syntax

26 "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10);

27 translations

28 "SUM i < k. b" == "sum (%i. b) k";

31 subsection {* Summation laws *};

33 (* FIXME binary arithmetic does not yet work here *)

35 syntax

36 "3" :: nat ("3")

37 "4" :: nat ("4")

38 "6" :: nat ("6");

40 translations

41 "3" == "Suc 2"

42 "4" == "Suc 3"

43 "6" == "Suc (Suc 4)";

45 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;

48 theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)"

49 (is "?P n" is "?S n = _");

50 proof (induct n);

51 show "?P 0"; by simp;

53 fix n;

54 have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp;

55 also; assume "?S n = n * (n + 1)";

56 also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;

57 finally; show "?P (Suc n)"; by simp;

58 qed;

60 theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2"

61 (is "?P n" is "?S n = _");

62 proof (induct n);

63 show "?P 0"; by simp;

65 fix n;

66 have "?S (n + 1) = ?S n + 2 * n + 1"; by simp;

67 also; assume "?S n = n^2";

68 also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;

69 finally; show "?P (Suc n)"; by simp;

70 qed;

72 theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"

73 (is "?P n" is "?S n = _");

74 proof (induct n);

75 show "?P 0"; by simp;

77 fix n;

78 have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;

79 also; assume "?S n = n * (n + 1) * (2 * n + 1)";

80 also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;

81 finally; show "?P (Suc n)"; by simp;

82 qed;

84 theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"

85 (is "?P n" is "?S n = _");

86 proof (induct n);

87 show "?P 0"; by simp;

89 fix n;

90 have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;

91 also; assume "?S n = (n * (n + 1))^2";

92 also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp;

93 finally; show "?P (Suc n)"; by simp;

94 qed;

97 end;