src/HOL/Isar_examples/Summation.thy
author oheimb
Wed Jan 31 10:15:55 2001 +0100 (2001-01-31)
changeset 11008 f7333f055ef6
parent 10672 3b1c2d74a01b
child 11701 3d51fbf81c17
permissions -rw-r--r--
improved theory reference in comment
wenzelm@7443
     1
(*  Title:      HOL/Isar_examples/Summation.thy
wenzelm@7443
     2
    ID:         $Id$
wenzelm@7443
     3
    Author:     Markus Wenzel
wenzelm@7443
     4
*)
wenzelm@7443
     5
wenzelm@10007
     6
header {* Summing natural numbers *}
wenzelm@7443
     7
wenzelm@10007
     8
theory Summation = Main:
wenzelm@7443
     9
wenzelm@7968
    10
text_raw {*
wenzelm@7968
    11
 \footnote{This example is somewhat reminiscent of the
wenzelm@7968
    12
 \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
wenzelm@7968
    13
 discussed in \cite{isabelle-ref} in the context of permutative
wenzelm@7968
    14
 rewrite rules and ordered rewriting.}
wenzelm@10007
    15
*}
wenzelm@7968
    16
wenzelm@7968
    17
text {*
wenzelm@7968
    18
 Subsequently, we prove some summation laws of natural numbers
wenzelm@7982
    19
 (including odds, squares, and cubes).  These examples demonstrate how
wenzelm@7968
    20
 plain natural deduction (including induction) may be combined with
wenzelm@7968
    21
 calculational proof.
wenzelm@10007
    22
*}
wenzelm@7968
    23
wenzelm@7761
    24
wenzelm@10007
    25
subsection {* Summation laws *}
wenzelm@7443
    26
wenzelm@7968
    27
text {*
wenzelm@7968
    28
 The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
wenzelm@7982
    29
 1)/2$.  Avoiding formal reasoning about division we prove this
wenzelm@7982
    30
 equation multiplied by $2$.
wenzelm@10007
    31
*}
wenzelm@7800
    32
wenzelm@7800
    33
theorem sum_of_naturals:
wenzelm@10672
    34
  "2 * (\<Sum>i < n + 1. i) = n * (n + 1)"
wenzelm@10007
    35
  (is "?P n" is "?S n = _")
wenzelm@10007
    36
proof (induct n)
wenzelm@10007
    37
  show "?P 0" by simp
wenzelm@10146
    38
next
wenzelm@10146
    39
  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
wenzelm@10007
    40
  also assume "?S n = n * (n + 1)"
wenzelm@10007
    41
  also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
wenzelm@10007
    42
  finally show "?P (Suc n)" by simp
wenzelm@10007
    43
qed
wenzelm@7443
    44
wenzelm@7968
    45
text {*
wenzelm@7968
    46
 The above proof is a typical instance of mathematical induction.  The
wenzelm@7968
    47
 main statement is viewed as some $\var{P} \ap n$ that is split by the
wenzelm@7968
    48
 induction method into base case $\var{P} \ap 0$, and step case
wenzelm@7982
    49
 $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
wenzelm@7968
    50
wenzelm@7968
    51
 The step case is established by a short calculation in forward
wenzelm@7968
    52
 manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
wenzelm@7982
    53
 the thesis, the final result is achieved by transformations involving
wenzelm@7982
    54
 basic arithmetic reasoning (using the Simplifier).  The main point is
wenzelm@7982
    55
 where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
wenzelm@7982
    56
 introduced in order to replace a certain subterm.  So the
wenzelm@7968
    57
 ``transitivity'' rule involved here is actual \emph{substitution}.
wenzelm@7968
    58
 Also note how the occurrence of ``\dots'' in the subsequent step
wenzelm@7982
    59
 documents the position where the right-hand side of the hypothesis
wenzelm@7968
    60
 got filled in.
wenzelm@7968
    61
wenzelm@7968
    62
 \medskip A further notable point here is integration of calculations
wenzelm@7982
    63
 with plain natural deduction.  This works so well in Isar for two
wenzelm@7982
    64
 reasons.
wenzelm@7968
    65
 \begin{enumerate}
wenzelm@7968
    66
wenzelm@7968
    67
 \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
wenzelm@7968
    68
 calculational chains may be just anything.  There is nothing special
wenzelm@7968
    69
 about \isakeyword{have}, so the natural deduction element
wenzelm@7968
    70
 \isakeyword{assume} works just as well.
wenzelm@7968
    71
wenzelm@7968
    72
 \item There are two \emph{separate} primitives for building natural
wenzelm@7968
    73
 deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
wenzelm@7982
    74
 Thus it is possible to start reasoning with some new ``arbitrary, but
wenzelm@7982
    75
 fixed'' elements before bringing in the actual assumption.  In
wenzelm@7982
    76
 contrast, natural deduction is occasionally formalized with basic
wenzelm@7982
    77
 context elements of the form $x:A$ instead.
wenzelm@7968
    78
wenzelm@7968
    79
 \end{enumerate}
wenzelm@10007
    80
*}
wenzelm@7968
    81
wenzelm@7968
    82
text {*
wenzelm@7982
    83
 \medskip We derive further summation laws for odds, squares, and
wenzelm@7982
    84
 cubes as follows.  The basic technique of induction plus calculation
wenzelm@7982
    85
 is the same as before.
wenzelm@10007
    86
*}
wenzelm@7968
    87
wenzelm@7800
    88
theorem sum_of_odds:
wenzelm@10672
    89
  "(\<Sum>i < n. 2 * i + 1) = n^2"
wenzelm@10007
    90
  (is "?P n" is "?S n = _")
wenzelm@10007
    91
proof (induct n)
wenzelm@10007
    92
  show "?P 0" by simp
wenzelm@10146
    93
next
wenzelm@10146
    94
  fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
wenzelm@10007
    95
  also assume "?S n = n^2"
wenzelm@10007
    96
  also have "... + 2 * n + 1 = (n + 1)^2" by simp
wenzelm@10007
    97
  finally show "?P (Suc n)" by simp
wenzelm@10007
    98
qed
wenzelm@7443
    99
wenzelm@8814
   100
text {*
wenzelm@8814
   101
 Subsequently we require some additional tweaking of Isabelle built-in
wenzelm@8814
   102
 arithmetic simplifications, such as bringing in distributivity by
wenzelm@8814
   103
 hand.
wenzelm@10007
   104
*}
wenzelm@8814
   105
wenzelm@10007
   106
lemmas distrib = add_mult_distrib add_mult_distrib2
wenzelm@8814
   107
wenzelm@7761
   108
theorem sum_of_squares:
wenzelm@10672
   109
  "#6 * (\<Sum>i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
wenzelm@10007
   110
  (is "?P n" is "?S n = _")
wenzelm@10007
   111
proof (induct n)
wenzelm@10007
   112
  show "?P 0" by simp
wenzelm@10146
   113
next
wenzelm@10146
   114
  fix n have "?S (n + 1) = ?S n + #6 * (n + 1)^2" by (simp add: distrib)
wenzelm@10007
   115
  also assume "?S n = n * (n + 1) * (2 * n + 1)"
wenzelm@10007
   116
  also have "... + #6 * (n + 1)^2 =
wenzelm@10007
   117
    (n + 1) * (n + 2) * (2 * (n + 1) + 1)" by (simp add: distrib)
wenzelm@10007
   118
  finally show "?P (Suc n)" by simp
wenzelm@10007
   119
qed
wenzelm@7443
   120
wenzelm@7800
   121
theorem sum_of_cubes:
wenzelm@10672
   122
  "#4 * (\<Sum>i < n + 1. i^#3) = (n * (n + 1))^2"
wenzelm@10007
   123
  (is "?P n" is "?S n = _")
wenzelm@10007
   124
proof (induct n)
wenzelm@10007
   125
  show "?P 0" by (simp add: power_eq_if)
wenzelm@10146
   126
next
wenzelm@10146
   127
  fix n have "?S (n + 1) = ?S n + #4 * (n + 1)^#3"
wenzelm@10007
   128
    by (simp add: power_eq_if distrib)
wenzelm@10007
   129
  also assume "?S n = (n * (n + 1))^2"
wenzelm@10007
   130
  also have "... + #4 * (n + 1)^#3 = ((n + 1) * ((n + 1) + 1))^2"
wenzelm@10007
   131
    by (simp add: power_eq_if distrib)
wenzelm@10007
   132
  finally show "?P (Suc n)" by simp
wenzelm@10007
   133
qed
wenzelm@7443
   134
wenzelm@7968
   135
text {*
wenzelm@7968
   136
 Comparing these examples with the tactic script version
wenzelm@7968
   137
 \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
wenzelm@7982
   138
 an important difference of how induction vs.\ simplification is
wenzelm@7968
   139
 applied.  While \cite[\S10]{isabelle-ref} advises for these examples
wenzelm@7968
   140
 that ``induction should not be applied until the goal is in the
wenzelm@7968
   141
 simplest form'' this would be a very bad idea in our setting.
wenzelm@7968
   142
wenzelm@7968
   143
 Simplification normalizes all arithmetic expressions involved,
wenzelm@7982
   144
 producing huge intermediate goals.  With applying induction
wenzelm@7982
   145
 afterwards, the Isar proof text would have to reflect the emerging
wenzelm@7982
   146
 configuration by appropriate sub-proofs.  This would result in badly
wenzelm@7982
   147
 structured, low-level technical reasoning, without any good idea of
wenzelm@7982
   148
 the actual point.
wenzelm@7968
   149
wenzelm@7968
   150
 \medskip As a general rule of good proof style, automatic methods
wenzelm@7982
   151
 such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as
wenzelm@7968
   152
 initial proof methods, but only as terminal ones, solving certain
wenzelm@7968
   153
 goals completely.
wenzelm@10007
   154
*}
wenzelm@7968
   155
wenzelm@10007
   156
end