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