src/HOL/Isar_examples/Summation.thy
author wenzelm
Sat Oct 30 20:20:48 1999 +0200 (1999-10-30)
changeset 7982 d534b897ce39
parent 7968 964b65b4e433
child 8584 016314c2fa0a
permissions -rw-r--r--
improved presentation;
     1 (*  Title:      HOL/Isar_examples/Summation.thy
     2     ID:         $Id$
     3     Author:     Markus Wenzel
     4 *)
     5 
     6 header {* Summing natural numbers *};
     7 
     8 theory Summation = Main:;
     9 
    10 text_raw {*
    11  \footnote{This example is somewhat reminiscent of the
    12  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
    13  discussed in \cite{isabelle-ref} in the context of permutative
    14  rewrite rules and ordered rewriting.}
    15 *};
    16 
    17 text {*
    18  Subsequently, we prove some summation laws of natural numbers
    19  (including odds, squares, and cubes).  These examples demonstrate how
    20  plain natural deduction (including induction) may be combined with
    21  calculational proof.
    22 *};
    23 
    24 
    25 subsection {* A summation operator *};
    26 
    27 text {*
    28   The binder operator $\idt{sum} :: (\idt{nat} \To \idt{nat}) \To
    29  \idt{nat} \To \idt{nat}$ formalizes summation of natural numbers
    30  indexed from $0$ up to $k$ (excluding the bound):
    31  \[
    32  \sum\limits_{i < k} f(i) = \idt{sum} \ap (\lam i f \ap i) \ap k
    33  \]
    34 *};
    35 
    36 consts
    37   sum :: "[nat => nat, nat] => nat";
    38 
    39 primrec
    40   "sum f 0 = 0"
    41   "sum f (Suc n) = f n + sum f n";
    42 
    43 syntax
    44   "_SUM" :: "[idt, nat, nat] => nat"
    45     ("SUM _ < _. _" [0, 0, 10] 10);
    46 translations
    47   "SUM i < k. b" == "sum (\<lambda>i. b) k";
    48 
    49 
    50 subsection {* Summation laws *};
    51 
    52 text_raw {* \begin{comment} *};
    53 
    54 (* FIXME binary arithmetic does not yet work here *)
    55 
    56 syntax
    57   "3" :: nat  ("3")
    58   "4" :: nat  ("4")
    59   "6" :: nat  ("6");
    60 
    61 translations
    62   "3" == "Suc 2"
    63   "4" == "Suc 3"
    64   "6" == "Suc (Suc 4)";
    65 
    66 theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
    67 
    68 text_raw {* \end{comment} *};
    69 
    70 text {*
    71  The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
    72  1)/2$.  Avoiding formal reasoning about division we prove this
    73  equation multiplied by $2$.
    74 *};
    75 
    76 theorem sum_of_naturals:
    77   "2 * (SUM i < n + 1. i) = n * (n + 1)"
    78   (is "?P n" is "?S n = _");
    79 proof (induct n);
    80   show "?P 0"; by simp;
    81 
    82   fix n;
    83   have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp;
    84   also; assume "?S n = n * (n + 1)";
    85   also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
    86   finally; show "?P (Suc n)"; by simp;
    87 qed;
    88 
    89 text {*
    90  The above proof is a typical instance of mathematical induction.  The
    91  main statement is viewed as some $\var{P} \ap n$ that is split by the
    92  induction method into base case $\var{P} \ap 0$, and step case
    93  $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
    94 
    95  The step case is established by a short calculation in forward
    96  manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
    97  the thesis, the final result is achieved by transformations involving
    98  basic arithmetic reasoning (using the Simplifier).  The main point is
    99  where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
   100  introduced in order to replace a certain subterm.  So the
   101  ``transitivity'' rule involved here is actual \emph{substitution}.
   102  Also note how the occurrence of ``\dots'' in the subsequent step
   103  documents the position where the right-hand side of the hypothesis
   104  got filled in.
   105 
   106  \medskip A further notable point here is integration of calculations
   107  with plain natural deduction.  This works so well in Isar for two
   108  reasons.
   109  \begin{enumerate}
   110 
   111  \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
   112  calculational chains may be just anything.  There is nothing special
   113  about \isakeyword{have}, so the natural deduction element
   114  \isakeyword{assume} works just as well.
   115 
   116  \item There are two \emph{separate} primitives for building natural
   117  deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
   118  Thus it is possible to start reasoning with some new ``arbitrary, but
   119  fixed'' elements before bringing in the actual assumption.  In
   120  contrast, natural deduction is occasionally formalized with basic
   121  context elements of the form $x:A$ instead.
   122 
   123  \end{enumerate}
   124 *};
   125 
   126 text {*
   127  \medskip We derive further summation laws for odds, squares, and
   128  cubes as follows.  The basic technique of induction plus calculation
   129  is the same as before.
   130 *};
   131 
   132 theorem sum_of_odds:
   133   "(SUM i < n. 2 * i + 1) = n^2"
   134   (is "?P n" is "?S n = _");
   135 proof (induct n);
   136   show "?P 0"; by simp;
   137 
   138   fix n;
   139   have "?S (n + 1) = ?S n + 2 * n + 1"; by simp;
   140   also; assume "?S n = n^2";
   141   also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
   142   finally; show "?P (Suc n)"; by simp;
   143 qed;
   144 
   145 theorem sum_of_squares:
   146   "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
   147   (is "?P n" is "?S n = _");
   148 proof (induct n);
   149   show "?P 0"; by simp;
   150 
   151   fix n;
   152   have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
   153   also; assume "?S n = n * (n + 1) * (2 * n + 1)";
   154   also; have "... + 6 * (n + 1)^2 =
   155     (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
   156   finally; show "?P (Suc n)"; by simp;
   157 qed;
   158 
   159 theorem sum_of_cubes:
   160   "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
   161   (is "?P n" is "?S n = _");
   162 proof (induct n);
   163   show "?P 0"; by simp;
   164 
   165   fix n;
   166   have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
   167   also; assume "?S n = (n * (n + 1))^2";
   168   also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2";
   169     by simp;
   170   finally; show "?P (Suc n)"; by simp;
   171 qed;
   172 
   173 text {*
   174  Comparing these examples with the tactic script version
   175  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
   176  an important difference of how induction vs.\ simplification is
   177  applied.  While \cite[\S10]{isabelle-ref} advises for these examples
   178  that ``induction should not be applied until the goal is in the
   179  simplest form'' this would be a very bad idea in our setting.
   180 
   181  Simplification normalizes all arithmetic expressions involved,
   182  producing huge intermediate goals.  With applying induction
   183  afterwards, the Isar proof text would have to reflect the emerging
   184  configuration by appropriate sub-proofs.  This would result in badly
   185  structured, low-level technical reasoning, without any good idea of
   186  the actual point.
   187 
   188  \medskip As a general rule of good proof style, automatic methods
   189  such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as
   190  initial proof methods, but only as terminal ones, solving certain
   191  goals completely.
   192 *};
   193 
   194 end;