src/HOL/Isar_Examples/Summation.thy
 author wenzelm Tue Oct 20 19:37:09 2009 +0200 (2009-10-20) changeset 33026 8f35633c4922 parent 31758 src/HOL/Isar_examples/Summation.thy@3edd5f813f01 child 37671 fa53d267dab3 permissions -rw-r--r--
modernized session Isar_Examples;
     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_raw {*

    12  \footnote{This example is somewhat reminiscent of the

    13  \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is

    14  discussed in \cite{isabelle-ref} in the context of permutative

    15  rewrite rules and ordered rewriting.}

    16 *}

    17

    18 text {*

    19  Subsequently, we prove some summation laws of natural numbers

    20  (including odds, squares, and cubes).  These examples demonstrate how

    21  plain natural deduction (including induction) may be combined with

    22  calculational proof.

    23 *}

    24

    25

    26 subsection {* Summation laws *}

    27

    28 text {*

    29  The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +   30 1)/2$.  Avoiding formal reasoning about division we prove this

    31  equation multiplied by $2$.

    32 *}

    33

    34 theorem sum_of_naturals:

    35   "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"

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

    37 proof (induct n)

    38   show "?P 0" by simp

    39 next

    40   fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp

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

    42   also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp

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

    44 qed

    45

    46 text {*

    47  The above proof is a typical instance of mathematical induction.  The

    48  main statement is viewed as some $\var{P} \ap n$ that is split by the

    49  induction method into base case $\var{P} \ap 0$, and step case

    50  $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.

    51

    52  The step case is established by a short calculation in forward

    53  manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of

    54  the thesis, the final result is achieved by transformations involving

    55  basic arithmetic reasoning (using the Simplifier).  The main point is

    56  where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is

    57  introduced in order to replace a certain subterm.  So the

    58  transitivity'' rule involved here is actual \emph{substitution}.

    59  Also note how the occurrence of \dots'' in the subsequent step

    60  documents the position where the right-hand side of the hypothesis

    61  got filled in.

    62

    63  \medskip A further notable point here is integration of calculations

    64  with plain natural deduction.  This works so well in Isar for two

    65  reasons.

    66  \begin{enumerate}

    67

    68  \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}

    69  calculational chains may be just anything.  There is nothing special

    70  about \isakeyword{have}, so the natural deduction element

    71  \isakeyword{assume} works just as well.

    72

    73  \item There are two \emph{separate} primitives for building natural

    74  deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.

    75  Thus it is possible to start reasoning with some new arbitrary, but

    76  fixed'' elements before bringing in the actual assumption.  In

    77  contrast, natural deduction is occasionally formalized with basic

    78  context elements of the form $x:A$ instead.

    79

    80  \end{enumerate}

    81 *}

    82

    83 text {*

    84  \medskip We derive further summation laws for odds, squares, and

    85  cubes as follows.  The basic technique of induction plus calculation

    86  is the same as before.

    87 *}

    88

    89 theorem sum_of_odds:

    90   "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"

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

    92 proof (induct n)

    93   show "?P 0" by simp

    94 next

    95   fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp

    96   also assume "?S n = n^Suc (Suc 0)"

    97   also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp

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

    99 qed

   100

   101 text {*

   102  Subsequently we require some additional tweaking of Isabelle built-in

   103  arithmetic simplifications, such as bringing in distributivity by

   104  hand.

   105 *}

   106

   107 lemmas distrib = add_mult_distrib add_mult_distrib2

   108

   109 theorem sum_of_squares:

   110   "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"

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

   112 proof (induct n)

   113   show "?P 0" by simp

   114 next

   115   fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)"

   116     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