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