src/HOL/Isar_examples/Summation.thy
author paulson
Tue Jun 28 15:27:45 2005 +0200 (2005-06-28)
changeset 16587 b34c8aa657a5
parent 15912 47aa1a8fcdc9
child 18193 54419506df9e
permissions -rw-r--r--
Constant "If" is now local
     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
     9 imports Main
    10 begin
    11 
    12 text_raw {*
    13  \footnote{This example is somewhat reminiscent of the
    14  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
    15  discussed in \cite{isabelle-ref} in the context of permutative
    16  rewrite rules and ordered rewriting.}
    17 *}
    18 
    19 text {*
    20  Subsequently, we prove some summation laws of natural numbers
    21  (including odds, squares, and cubes).  These examples demonstrate how
    22  plain natural deduction (including induction) may be combined with
    23  calculational proof.
    24 *}
    25 
    26 
    27 subsection {* Summation laws *}
    28 
    29 text {*
    30  The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
    31  1)/2$.  Avoiding formal reasoning about division we prove this
    32  equation multiplied by $2$.
    33 *}
    34 
    35 theorem sum_of_naturals:
    36   "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
    37   (is "?P n" is "?S n = _")
    38 proof (induct n)
    39   show "?P 0" by simp
    40 next
    41   fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
    42   also assume "?S n = n * (n + 1)"
    43   also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
    44   finally show "?P (Suc n)" by simp
    45 qed
    46 
    47 text {*
    48  The above proof is a typical instance of mathematical induction.  The
    49  main statement is viewed as some $\var{P} \ap n$ that is split by the
    50  induction method into base case $\var{P} \ap 0$, and step case
    51  $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
    52 
    53  The step case is established by a short calculation in forward
    54  manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
    55  the thesis, the final result is achieved by transformations involving
    56  basic arithmetic reasoning (using the Simplifier).  The main point is
    57  where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
    58  introduced in order to replace a certain subterm.  So the
    59  ``transitivity'' rule involved here is actual \emph{substitution}.
    60  Also note how the occurrence of ``\dots'' in the subsequent step
    61  documents the position where the right-hand side of the hypothesis
    62  got filled in.
    63 
    64  \medskip A further notable point here is integration of calculations
    65  with plain natural deduction.  This works so well in Isar for two
    66  reasons.
    67  \begin{enumerate}
    68 
    69  \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
    70  calculational chains may be just anything.  There is nothing special
    71  about \isakeyword{have}, so the natural deduction element
    72  \isakeyword{assume} works just as well.
    73 
    74  \item There are two \emph{separate} primitives for building natural
    75  deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
    76  Thus it is possible to start reasoning with some new ``arbitrary, but
    77  fixed'' elements before bringing in the actual assumption.  In
    78  contrast, natural deduction is occasionally formalized with basic
    79  context elements of the form $x:A$ instead.
    80 
    81  \end{enumerate}
    82 *}
    83 
    84 text {*
    85  \medskip We derive further summation laws for odds, squares, and
    86  cubes as follows.  The basic technique of induction plus calculation
    87  is the same as before.
    88 *}
    89 
    90 theorem sum_of_odds:
    91   "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
    92   (is "?P n" is "?S n = _")
    93 proof (induct n)
    94   show "?P 0" by simp
    95 next
    96   fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
    97   also assume "?S n = n^Suc (Suc 0)"
    98   also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
    99   finally show "?P (Suc n)" by simp
   100 qed
   101 
   102 text {*
   103  Subsequently we require some additional tweaking of Isabelle built-in
   104  arithmetic simplifications, such as bringing in distributivity by
   105  hand.
   106 *}
   107 
   108 lemmas distrib = add_mult_distrib add_mult_distrib2
   109 
   110 theorem sum_of_squares:
   111   "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
   112   (is "?P n" is "?S n = _")
   113 proof (induct n)
   114   show "?P 0" by simp
   115 next
   116   fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" 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