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 ?;
 wenzelm@7443 ` 1` ```(* Title: HOL/Isar_examples/Summation.thy ``` wenzelm@7443 ` 2` ``` ID: \$Id\$ ``` wenzelm@7443 ` 3` ``` Author: Markus Wenzel ``` wenzelm@7443 ` 4` wenzelm@7443 ` 5` ```Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the ``` wenzelm@7443 ` 6` ```original scripts). Demonstrates mathematical induction together with ``` wenzelm@7443 ` 7` ```calculational proof. ``` wenzelm@7443 ` 8` ```*) ``` wenzelm@7443 ` 9` wenzelm@7443 ` 10` wenzelm@7443 ` 11` ```theory Summation = Main:; ``` wenzelm@7443 ` 12` wenzelm@7443 ` 13` wenzelm@7443 ` 14` ```section {* Summing natural numbers *}; ``` wenzelm@7443 ` 15` wenzelm@7443 ` 16` ```text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *}; ``` wenzelm@7443 ` 17` wenzelm@7443 ` 18` ```consts ``` wenzelm@7443 ` 19` ``` sum :: "[nat => nat, nat] => nat"; ``` wenzelm@7443 ` 20` wenzelm@7443 ` 21` ```primrec ``` wenzelm@7443 ` 22` ``` "sum f 0 = 0" ``` wenzelm@7443 ` 23` ``` "sum f (Suc n) = f n + sum f n"; ``` wenzelm@7443 ` 24` wenzelm@7443 ` 25` ```syntax ``` wenzelm@7443 ` 26` ``` "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10); ``` wenzelm@7443 ` 27` ```translations ``` wenzelm@7443 ` 28` ``` "SUM i < k. b" == "sum (%i. b) k"; ``` wenzelm@7443 ` 29` wenzelm@7443 ` 30` wenzelm@7443 ` 31` ```subsection {* Summation laws *}; ``` wenzelm@7443 ` 32` wenzelm@7443 ` 33` ```(* FIXME binary arithmetic does not yet work here *) ``` wenzelm@7443 ` 34` wenzelm@7443 ` 35` ```syntax ``` wenzelm@7443 ` 36` ``` "3" :: nat ("3") ``` wenzelm@7443 ` 37` ``` "4" :: nat ("4") ``` wenzelm@7443 ` 38` ``` "6" :: nat ("6"); ``` wenzelm@7443 ` 39` wenzelm@7443 ` 40` ```translations ``` wenzelm@7443 ` 41` ``` "3" == "Suc 2" ``` wenzelm@7443 ` 42` ``` "4" == "Suc 3" ``` wenzelm@7443 ` 43` ``` "6" == "Suc (Suc 4)"; ``` wenzelm@7443 ` 44` wenzelm@7443 ` 45` ```theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac; ``` wenzelm@7443 ` 46` wenzelm@7443 ` 47` wenzelm@7443 ` 48` ```theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)" ``` wenzelm@7480 ` 49` ``` (is "?P n" is "?S n = _"); ``` wenzelm@7443 ` 50` ```proof (induct n); ``` wenzelm@7480 ` 51` ``` show "?P 0"; by simp; ``` wenzelm@7443 ` 52` wenzelm@7443 ` 53` ``` fix n; ``` wenzelm@7480 ` 54` ``` have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp; ``` wenzelm@7480 ` 55` ``` also; assume "?S n = n * (n + 1)"; ``` wenzelm@7443 ` 56` ``` also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp; ``` wenzelm@7480 ` 57` ``` finally; show "?P (Suc n)"; by simp; ``` wenzelm@7443 ` 58` ```qed; ``` wenzelm@7443 ` 59` wenzelm@7443 ` 60` ```theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2" ``` wenzelm@7480 ` 61` ``` (is "?P n" is "?S n = _"); ``` wenzelm@7443 ` 62` ```proof (induct n); ``` wenzelm@7480 ` 63` ``` show "?P 0"; by simp; ``` wenzelm@7443 ` 64` wenzelm@7443 ` 65` ``` fix n; ``` wenzelm@7480 ` 66` ``` have "?S (n + 1) = ?S n + 2 * n + 1"; by simp; ``` wenzelm@7480 ` 67` ``` also; assume "?S n = n^2"; ``` wenzelm@7443 ` 68` ``` also; have "... + 2 * n + 1 = (n + 1)^2"; by simp; ``` wenzelm@7480 ` 69` ``` finally; show "?P (Suc n)"; by simp; ``` wenzelm@7443 ` 70` ```qed; ``` wenzelm@7443 ` 71` wenzelm@7443 ` 72` ```theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)" ``` wenzelm@7480 ` 73` ``` (is "?P n" is "?S n = _"); ``` wenzelm@7443 ` 74` ```proof (induct n); ``` wenzelm@7480 ` 75` ``` show "?P 0"; by simp; ``` wenzelm@7443 ` 76` wenzelm@7443 ` 77` ``` fix n; ``` wenzelm@7480 ` 78` ``` have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp; ``` wenzelm@7480 ` 79` ``` also; assume "?S n = n * (n + 1) * (2 * n + 1)"; ``` wenzelm@7443 ` 80` ``` also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp; ``` wenzelm@7480 ` 81` ``` finally; show "?P (Suc n)"; by simp; ``` wenzelm@7443 ` 82` ```qed; ``` wenzelm@7443 ` 83` wenzelm@7443 ` 84` ```theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2" ``` wenzelm@7480 ` 85` ``` (is "?P n" is "?S n = _"); ``` wenzelm@7443 ` 86` ```proof (induct n); ``` wenzelm@7480 ` 87` ``` show "?P 0"; by simp; ``` wenzelm@7443 ` 88` wenzelm@7443 ` 89` ``` fix n; ``` wenzelm@7480 ` 90` ``` have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp; ``` wenzelm@7480 ` 91` ``` also; assume "?S n = (n * (n + 1))^2"; ``` wenzelm@7443 ` 92` ``` also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp; ``` wenzelm@7480 ` 93` ``` finally; show "?P (Suc n)"; by simp; ``` wenzelm@7443 ` 94` ```qed; ``` wenzelm@7443 ` 95` wenzelm@7443 ` 96` wenzelm@7443 ` 97` ```end; ```