# HG changeset patch # User wenzelm # Date 936047953 -7200 # Node ID c68ecbf05eb6e6592e798089991fc85318cd52fc # Parent 9228085a25df184dfef5acc70416b2728bf4e044 proper calculation / induction; diff -r 9228085a25df -r c68ecbf05eb6 src/HOL/Isar_examples/NatSum.thy --- a/src/HOL/Isar_examples/NatSum.thy Mon Aug 30 20:30:39 1999 +0200 +++ b/src/HOL/Isar_examples/NatSum.thy Mon Aug 30 23:19:13 1999 +0200 @@ -1,79 +1,101 @@ (* Title: HOL/Isar_examples/NatSum.thy ID: $Id$ - Author: Tobias Nipkow and Markus Wenzel + Author: Markus Wenzel + +Summing natural numbers, squares and cubes (see HOL/ex/NatSum for the +original scripts). + +Demonstrates mathematical induction together with calculational proof. *) + theory NatSum = Main:; + section {* Summing natural numbers *}; text {* A summation operator: sum f (n+1) is the sum of all f(i), i=0...n. *}; consts - sum :: "[nat => nat, nat] => nat"; + sum :: "[nat => nat, nat] => nat"; -primrec +primrec "sum f 0 = 0" "sum f (Suc n) = f n + sum f n"; - -(*theorems [simp] = add_assoc add_commute add_left_commute add_mult_distrib add_mult_distrib2;*) +syntax + "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10); +translations + "SUM i < k. b" == "sum (%i. b) k"; -subsection {* The sum of the first n positive integers equals n(n+1)/2 *}; +subsection {* Summation laws *}; + +(* FIXME fails with binary numeral (why!?) *) -text {* Emulate Isabelle proof script: *}; +syntax + "3" :: nat ("3") + "4" :: nat ("4") + "6" :: nat ("6"); -(* - Goal "2*sum (%i. i) (Suc n) = n*Suc(n)"; - by (Simp_tac 1); - by (induct_tac "n" 1); - by (Simp_tac 1); - by (Asm_simp_tac 1); - qed "sum_of_naturals"; -*) +translations + "3" == "Suc 2" + "4" == "Suc 3" + "6" == "Suc (Suc 4)"; -theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n"; -proof -; - apply simp_tac; - apply (induct n); - apply simp_tac; - apply asm_simp_tac; -qed; + +(* FIXME bind_thms in Arith.ML *) +theorems mult_distrib [simp] = add_mult_distrib add_mult_distrib2; +theorems mult_ac [simp] = mult_assoc mult_commute mult_left_commute; -text {* Proper Isabelle/Isar proof expressing the same reasoning (which - is apparently not the most natural one): *}; +theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)" + (is "??P n" is "??L n = _"); +proof (induct n); + show "??P 0"; by simp; -theorem sum_of_naturals: "2 * sum (%i. i) (Suc n) = n * Suc n"; -proof simp; - show "n + (sum (%i. i) n + sum (%i. i) n) = n * n" (is "??P n"); - proof (induct ??P n); - show "??P 0"; by simp; - fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp); - qed; + fix n; + have "??L (n + 1) = ??L n + 2 * (n + 1)"; by simp; + also; assume "??L n = n * (n + 1)"; + also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp; + finally; show "??P (Suc n)"; by simp; +qed; + +theorem sum_of_odds: "(SUM i < n. 2 * i + 1) = n^2" + (is "??P n" is "??L n = _"); +proof (induct n); + show "??P 0"; by simp; + + fix n; + have "??L (n + 1) = ??L n + 2 * n + 1"; by simp; + also; assume "??L n = n^2"; + also; have "... + 2 * n + 1 = (n + 1)^2"; by simp; + finally; show "??P (Suc n)"; by simp; qed; - -subsection {* The sum of the first n odd numbers equals n squared *}; - -text {* First version: `proof-by-induction' *}; - -theorem sum_of_odds: "sum (%i. Suc (i + i)) n = n * n" (is "??P n"); +theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)" + (is "??P n" is "??L n = _"); proof (induct n); show "??P 0"; by simp; - fix m; assume hyp: "??P m"; show "??P (Suc m)"; by (simp, rule hyp); + + fix n; + have "??L (n + 1) = ??L n + 6 * (n + 1)^2"; by simp; + also; assume "??L n = n * (n + 1) * (2 * n + 1)"; + also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp; + (* FIXME #6: arith and simp fail!! *) + finally; show "??P (Suc n)"; by simp; qed; -text {* The second version tells more about what is going on during the -induction. *}; - -theorem sum_of_odds': "sum (%i. Suc (i + i)) n = n * n" (is "??P n"); +theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2" + (is "??P n" is "??L n = _"); proof (induct n); - show "??P 0" (is "sum (%i. Suc (i + i)) 0 = 0 * 0"); by simp; - fix m; assume hyp: "??P m"; - show "??P (Suc m)" (is "sum (%i. Suc (i + i)) (Suc m) = Suc m * Suc m"); - by (simp, rule hyp); + show "??P 0"; by simp; + + fix n; + have "??L (n + 1) = ??L n + 4 * (n + 1)^3"; by simp; + also; assume "??L n = (n * (n + 1))^2"; + also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2"; by simp; + finally; show "??P (Suc n)"; by simp; qed;