summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Thu, 02 Sep 1999 15:25:19 +0200 | |

changeset 7443 | e5356e73f57a |

parent 7442 | 2d2849258e3f |

child 7444 | ee17ad649c26 |

renamed NatSum to Summation;

src/HOL/IsaMakefile | file | annotate | diff | comparison | revisions | |

src/HOL/Isar_examples/NatSum.thy | file | annotate | diff | comparison | revisions | |

src/HOL/Isar_examples/ROOT.ML | file | annotate | diff | comparison | revisions | |

src/HOL/Isar_examples/Summation.thy | file | annotate | diff | comparison | revisions |

--- a/src/HOL/IsaMakefile Thu Sep 02 15:24:56 1999 +0200 +++ b/src/HOL/IsaMakefile Thu Sep 02 15:25:19 1999 +0200 @@ -342,8 +342,8 @@ Isar_examples/Cantor.ML Isar_examples/Cantor.thy \ Isar_examples/ExprCompiler.thy Isar_examples/Group.thy \ Isar_examples/KnasterTarski.thy Isar_examples/MultisetOrder.thy \ - Isar_examples/MutilatedCheckerboard.thy Isar_examples/NatSum.thy \ - Isar_examples/Peirce.thy Isar_examples/ROOT.ML + Isar_examples/MutilatedCheckerboard.thy Isar_examples/Peirce.thy \ + Isar_examples/Summation.thy Isar_examples/ROOT.ML @$(ISATOOL) usedir $(OUT)/HOL Isar_examples

--- a/src/HOL/Isar_examples/NatSum.thy Thu Sep 02 15:24:56 1999 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,102 +0,0 @@ -(* Title: HOL/Isar_examples/NatSum.thy - ID: $Id$ - 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"; - -primrec - "sum f 0 = 0" - "sum f (Suc n) = f n + sum f n"; - -syntax - "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10); -translations - "SUM i < k. b" == "sum (%i. b) k"; - - -subsection {* Summation laws *}; - -(* FIXME fails with binary numeral (why!?) *) - -syntax - "3" :: nat ("3") - "4" :: nat ("4") - "6" :: nat ("6"); - -translations - "3" == "Suc 2" - "4" == "Suc 3" - "6" == "Suc (Suc 4)"; - - -(* 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; - - -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; - - 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; - -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 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; - -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"; 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; - - -end;

--- a/src/HOL/Isar_examples/ROOT.ML Thu Sep 02 15:24:56 1999 +0200 +++ b/src/HOL/Isar_examples/ROOT.ML Thu Sep 02 15:25:19 1999 +0200 @@ -10,9 +10,7 @@ time_use_thy "Cantor"; time_use_thy "ExprCompiler"; time_use_thy "Group"; -time_use_thy "NatSum"; +time_use_thy "Summation"; time_use_thy "KnasterTarski"; time_use_thy "MutilatedCheckerboard"; - -add_path "../Induct"; -time_use_thy "MultisetOrder"; +with_path "../Induct" time_use_thy "MultisetOrder";

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Isar_examples/Summation.thy Thu Sep 02 15:25:19 1999 +0200 @@ -0,0 +1,97 @@ +(* Title: HOL/Isar_examples/Summation.thy + ID: $Id$ + 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 Summation = 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"; + +primrec + "sum f 0 = 0" + "sum f (Suc n) = f n + sum f n"; + +syntax + "_SUM" :: "idt => nat => nat => nat" ("SUM _ < _. _" [0, 0, 10] 10); +translations + "SUM i < k. b" == "sum (%i. b) k"; + + +subsection {* Summation laws *}; + +(* FIXME binary arithmetic does not yet work here *) + +syntax + "3" :: nat ("3") + "4" :: nat ("4") + "6" :: nat ("6"); + +translations + "3" == "Suc 2" + "4" == "Suc 3" + "6" == "Suc (Suc 4)"; + +theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac; + + +theorem sum_of_naturals: "2 * (SUM i < n + 1. i) = n * (n + 1)" + (is "??P n" is "??S n = _"); +proof (induct n); + show "??P 0"; by simp; + + fix n; + have "??S (n + 1) = ??S n + 2 * (n + 1)"; by simp; + also; assume "??S 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 "??S n = _"); +proof (induct n); + show "??P 0"; by simp; + + fix n; + have "??S (n + 1) = ??S n + 2 * n + 1"; by simp; + also; assume "??S n = n^2"; + also; have "... + 2 * n + 1 = (n + 1)^2"; by simp; + finally; show "??P (Suc n)"; by simp; +qed; + +theorem sum_of_squares: "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)" + (is "??P n" is "??S n = _"); +proof (induct n); + show "??P 0"; by simp; + + fix n; + have "??S (n + 1) = ??S n + 6 * (n + 1)^2"; by simp; + also; assume "??S n = n * (n + 1) * (2 * n + 1)"; + also; have "... + 6 * (n + 1)^2 = (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp; + finally; show "??P (Suc n)"; by simp; +qed; + +theorem sum_of_cubes: "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2" + (is "??P n" is "??S n = _"); +proof (induct n); + show "??P 0"; by simp; + + fix n; + have "??S (n + 1) = ??S n + 4 * (n + 1)^3"; by simp; + also; assume "??S 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; + + +end;