src/HOL/Isar_examples/Summation.thy
 author obua Mon Apr 10 16:00:34 2006 +0200 (2006-04-10) changeset 19404 9bf2cdc9e8e8 parent 18193 54419506df9e child 31758 3edd5f813f01 permissions -rw-r--r--
Moved stuff from Ring_and_Field to Matrix
     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)"

   117     by (simp add: distrib)

   118   also assume "?S n = n * (n + 1) * (2 * n + 1)"

   119   also have "... + 6 * (n + 1)^Suc (Suc 0) =

   120     (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)

   121   finally show "?P (Suc n)" by simp

   122 qed

   123

   124 theorem sum_of_cubes:

   125   "4 * (\<Sum>i::nat=0..n. i^3) = (n * (n + 1))^Suc (Suc 0)"

   126   (is "?P n" is "?S n = _")

   127 proof (induct n)

   128   show "?P 0" by (simp add: power_eq_if)

   129 next

   130   fix n have "?S (n + 1) = ?S n + 4 * (n + 1)^3"

   131     by (simp add: power_eq_if distrib)

   132   also assume "?S n = (n * (n + 1))^Suc (Suc 0)"

   133   also have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^Suc (Suc 0)"

   134     by (simp add: power_eq_if distrib)

   135   finally show "?P (Suc n)" by simp

   136 qed

   137

   138 text {*

   139  Comparing these examples with the tactic script version

   140  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note

   141  an important difference of how induction vs.\ simplification is

   142  applied.  While \cite[\S10]{isabelle-ref} advises for these examples

   143  that induction should not be applied until the goal is in the

   144  simplest form'' this would be a very bad idea in our setting.

   145

   146  Simplification normalizes all arithmetic expressions involved,

   147  producing huge intermediate goals.  With applying induction

   148  afterwards, the Isar proof text would have to reflect the emerging

   149  configuration by appropriate sub-proofs.  This would result in badly

   150  structured, low-level technical reasoning, without any good idea of

   151  the actual point.

   152

   153  \medskip As a general rule of good proof style, automatic methods

   154  such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as

   155  initial proof methods, but only as terminal ones, solving certain

   156  goals completely.

   157 *}

   158

   159 end