src/HOL/Isar_examples/Summation.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 15912 47aa1a8fcdc9 child 18193 54419506df9e permissions -rw-r--r--
Constant "If" is now local
     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)" by (simp add: distrib)

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

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

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

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

   121 qed

   122

   123 theorem sum_of_cubes:

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

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

   126 proof (induct n)

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

   128 next

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

   130     by (simp add: power_eq_if distrib)

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

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

   133     by (simp add: power_eq_if distrib)

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

   135 qed

   136

   137 text {*

   138  Comparing these examples with the tactic script version

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

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

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

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

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

   144

   145  Simplification normalizes all arithmetic expressions involved,

   146  producing huge intermediate goals.  With applying induction

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

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

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

   150  the actual point.

   151

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

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

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

   155  goals completely.

   156 *}

   157

   158 end