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