src/HOL/Isar_Examples/Summation.thy
author hoelzl
Tue Mar 26 12:20:58 2013 +0100 (2013-03-26)
changeset 51526 155263089e7b
parent 50086 ecffea78d381
child 55640 abc140f21caa
permissions -rw-r--r--
move SEQ.thy and Lim.thy to Limits.thy
     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 {* Subsequently, we prove some summation laws of natural numbers
    12   (including odds, squares, and cubes).  These examples demonstrate
    13   how plain natural deduction (including induction) may be combined
    14   with calculational proof. *}
    15 
    16 
    17 subsection {* Summation laws *}
    18 
    19 text {* The sum of natural numbers $0 + \cdots + n$ equals $n \times
    20   (n + 1)/2$.  Avoiding formal reasoning about division we prove this
    21   equation multiplied by $2$. *}
    22 
    23 theorem sum_of_naturals:
    24   "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
    25   (is "?P n" is "?S n = _")
    26 proof (induct n)
    27   show "?P 0" by simp
    28 next
    29   fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
    30   also assume "?S n = n * (n + 1)"
    31   also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
    32   finally show "?P (Suc n)" by simp
    33 qed
    34 
    35 text {* The above proof is a typical instance of mathematical
    36   induction.  The main statement is viewed as some $\var{P} \ap n$
    37   that is split by the induction method into base case $\var{P} \ap
    38   0$, and step case $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap
    39   n)$ for arbitrary $n$.
    40 
    41   The step case is established by a short calculation in forward
    42   manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
    43   the thesis, the final result is achieved by transformations
    44   involving basic arithmetic reasoning (using the Simplifier).  The
    45   main point is where the induction hypothesis $\var{S} \ap n = n
    46   \times (n + 1)$ is introduced in order to replace a certain subterm.
    47   So the ``transitivity'' rule involved here is actual
    48   \emph{substitution}.  Also note how the occurrence of ``\dots'' in
    49   the subsequent step documents the position where the right-hand side
    50   of the hypothesis got filled in.
    51 
    52   \medskip A further notable point here is integration of calculations
    53   with plain natural deduction.  This works so well in Isar for two
    54   reasons.
    55   \begin{enumerate}
    56 
    57   \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
    58   calculational chains may be just anything.  There is nothing special
    59   about \isakeyword{have}, so the natural deduction element
    60   \isakeyword{assume} works just as well.
    61 
    62   \item There are two \emph{separate} primitives for building natural
    63   deduction contexts: \isakeyword{fix}~$x$ and
    64   \isakeyword{assume}~$A$.  Thus it is possible to start reasoning
    65   with some new ``arbitrary, but fixed'' elements before bringing in
    66   the actual assumption.  In contrast, natural deduction is
    67   occasionally formalized with basic context elements of the form
    68   $x:A$ instead.
    69 
    70   \end{enumerate}
    71 *}
    72 
    73 text {* \medskip We derive further summation laws for odds, squares,
    74   and cubes as follows.  The basic technique of induction plus
    75   calculation is the same as before. *}
    76 
    77 theorem sum_of_odds:
    78   "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
    79   (is "?P n" is "?S n = _")
    80 proof (induct n)
    81   show "?P 0" by simp
    82 next
    83   fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
    84   also assume "?S n = n^Suc (Suc 0)"
    85   also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
    86   finally show "?P (Suc n)" by simp
    87 qed
    88 
    89 text {* Subsequently we require some additional tweaking of Isabelle
    90   built-in arithmetic simplifications, such as bringing in
    91   distributivity by hand. *}
    92 
    93 lemmas distrib = add_mult_distrib add_mult_distrib2
    94 
    95 theorem sum_of_squares:
    96   "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
    97   (is "?P n" is "?S n = _")
    98 proof (induct n)
    99   show "?P 0" by simp
   100 next
   101   fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"
   102     by (simp add: distrib)
   103   also assume "?S n = n * (n + 1) * (2 * n + 1)"
   104   also have "... + 6 * (n + 1)^Suc (Suc 0) =
   105       (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
   106   finally show "?P (Suc n)" by simp
   107 qed
   108 
   109 theorem sum_of_cubes:
   110   "4 * (\<Sum>i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)"
   111   (is "?P n" is "?S n = _")
   112 proof (induct n)
   113   show "?P 0" by (simp add: power_eq_if)
   114 next
   115   fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"
   116     by (simp add: power_eq_if distrib)
   117   also assume "?S n = (n * (n + 1))^Suc (Suc 0)"
   118   also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"
   119     by (simp add: power_eq_if distrib)
   120   finally show "?P (Suc n)" by simp
   121 qed
   122 
   123 text {* Note that in contrast to older traditions of tactical proof
   124   scripts, the structured proof applies induction on the original,
   125   unsimplified statement.  This allows to state the induction cases
   126   robustly and conveniently.  Simplification (or other automated)
   127   methods are then applied in terminal position to solve certain
   128   sub-problems completely.
   129 
   130   As a general rule of good proof style, automatic methods such as
   131   $\idt{simp}$ or $\idt{auto}$ should normally be never used as
   132   initial proof methods with a nested sub-proof to address the
   133   automatically produced situation, but only as terminal ones to solve
   134   sub-problems.  *}
   135 
   136 end