src/HOL/Isar_Examples/Summation.thy
 author wenzelm Thu Feb 20 23:46:40 2014 +0100 (2014-02-20) changeset 55640 abc140f21caa parent 50086 ecffea78d381 child 58614 7338eb25226c permissions -rw-r--r--
tuned proofs;
more symbols;
     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