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