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
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
nipkow@15561
     8
theory Summation
nipkow@15561
     9
imports Main
nipkow@15561
    10
begin
nipkow@15561
    11
wenzelm@7968
    12
text_raw {*
wenzelm@7968
    13
 \footnote{This example is somewhat reminiscent of the
wenzelm@7968
    14
 \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, which is
wenzelm@7968
    15
 discussed in \cite{isabelle-ref} in the context of permutative
wenzelm@7968
    16
 rewrite rules and ordered rewriting.}
wenzelm@10007
    17
*}
wenzelm@7968
    18
wenzelm@7968
    19
text {*
wenzelm@7968
    20
 Subsequently, we prove some summation laws of natural numbers
wenzelm@7982
    21
 (including odds, squares, and cubes).  These examples demonstrate how
wenzelm@7968
    22
 plain natural deduction (including induction) may be combined with
wenzelm@7968
    23
 calculational proof.
wenzelm@10007
    24
*}
wenzelm@7968
    25
wenzelm@7761
    26
wenzelm@10007
    27
subsection {* Summation laws *}
wenzelm@7443
    28
wenzelm@7968
    29
text {*
wenzelm@7968
    30
 The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
wenzelm@7982
    31
 1)/2$.  Avoiding formal reasoning about division we prove this
wenzelm@7982
    32
 equation multiplied by $2$.
wenzelm@10007
    33
*}
wenzelm@7800
    34
wenzelm@7800
    35
theorem sum_of_naturals:
nipkow@15561
    36
  "2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
wenzelm@10007
    37
  (is "?P n" is "?S n = _")
wenzelm@10007
    38
proof (induct n)
wenzelm@10007
    39
  show "?P 0" by simp
wenzelm@10146
    40
next
wenzelm@11704
    41
  fix n have "?S (n + 1) = ?S n + 2 * (n + 1)" by simp
wenzelm@10007
    42
  also assume "?S n = n * (n + 1)"
wenzelm@11704
    43
  also have "... + 2 * (n + 1) = (n + 1) * (n + 2)" by simp
wenzelm@10007
    44
  finally show "?P (Suc n)" by simp
wenzelm@10007
    45
qed
wenzelm@7443
    46
wenzelm@7968
    47
text {*
wenzelm@7968
    48
 The above proof is a typical instance of mathematical induction.  The
wenzelm@7968
    49
 main statement is viewed as some $\var{P} \ap n$ that is split by the
wenzelm@7968
    50
 induction method into base case $\var{P} \ap 0$, and step case
wenzelm@7982
    51
 $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
wenzelm@7968
    52
wenzelm@7968
    53
 The step case is established by a short calculation in forward
wenzelm@7968
    54
 manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
wenzelm@7982
    55
 the thesis, the final result is achieved by transformations involving
wenzelm@7982
    56
 basic arithmetic reasoning (using the Simplifier).  The main point is
wenzelm@7982
    57
 where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
wenzelm@7982
    58
 introduced in order to replace a certain subterm.  So the
wenzelm@7968
    59
 ``transitivity'' rule involved here is actual \emph{substitution}.
wenzelm@7968
    60
 Also note how the occurrence of ``\dots'' in the subsequent step
wenzelm@7982
    61
 documents the position where the right-hand side of the hypothesis
wenzelm@7968
    62
 got filled in.
wenzelm@7968
    63
wenzelm@7968
    64
 \medskip A further notable point here is integration of calculations
wenzelm@7982
    65
 with plain natural deduction.  This works so well in Isar for two
wenzelm@7982
    66
 reasons.
wenzelm@7968
    67
 \begin{enumerate}
wenzelm@7968
    68
wenzelm@7968
    69
 \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
wenzelm@7968
    70
 calculational chains may be just anything.  There is nothing special
wenzelm@7968
    71
 about \isakeyword{have}, so the natural deduction element
wenzelm@7968
    72
 \isakeyword{assume} works just as well.
wenzelm@7968
    73
wenzelm@7968
    74
 \item There are two \emph{separate} primitives for building natural
wenzelm@7968
    75
 deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
wenzelm@7982
    76
 Thus it is possible to start reasoning with some new ``arbitrary, but
wenzelm@7982
    77
 fixed'' elements before bringing in the actual assumption.  In
wenzelm@7982
    78
 contrast, natural deduction is occasionally formalized with basic
wenzelm@7982
    79
 context elements of the form $x:A$ instead.
wenzelm@7968
    80
wenzelm@7968
    81
 \end{enumerate}
wenzelm@10007
    82
*}
wenzelm@7968
    83
wenzelm@7968
    84
text {*
wenzelm@7982
    85
 \medskip We derive further summation laws for odds, squares, and
wenzelm@7982
    86
 cubes as follows.  The basic technique of induction plus calculation
wenzelm@7982
    87
 is the same as before.
wenzelm@10007
    88
*}
wenzelm@7968
    89
wenzelm@7800
    90
theorem sum_of_odds:
nipkow@15561
    91
  "(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
wenzelm@10007
    92
  (is "?P n" is "?S n = _")
wenzelm@10007
    93
proof (induct n)
wenzelm@10007
    94
  show "?P 0" by simp
wenzelm@10146
    95
next
wenzelm@11704
    96
  fix n have "?S (n + 1) = ?S n + 2 * n + 1" by simp
wenzelm@11701
    97
  also assume "?S n = n^Suc (Suc 0)"
wenzelm@11704
    98
  also have "... + 2 * n + 1 = (n + 1)^Suc (Suc 0)" by simp
wenzelm@10007
    99
  finally show "?P (Suc n)" by simp
wenzelm@10007
   100
qed
wenzelm@7443
   101
wenzelm@8814
   102
text {*
wenzelm@8814
   103
 Subsequently we require some additional tweaking of Isabelle built-in
wenzelm@8814
   104
 arithmetic simplifications, such as bringing in distributivity by
wenzelm@8814
   105
 hand.
wenzelm@10007
   106
*}
wenzelm@8814
   107
wenzelm@10007
   108
lemmas distrib = add_mult_distrib add_mult_distrib2
wenzelm@8814
   109
wenzelm@7761
   110
theorem sum_of_squares:
nipkow@15561
   111
  "6 * (\<Sum>i::nat=0..n. i^Suc (Suc 0)) = n * (n + 1) * (2 * n + 1)"
wenzelm@10007
   112
  (is "?P n" is "?S n = _")
wenzelm@10007
   113
proof (induct n)
wenzelm@10007
   114
  show "?P 0" by simp
wenzelm@10146
   115
next
wenzelm@11704
   116
  fix n have "?S (n + 1) = ?S n + 6 * (n + 1)^Suc (Suc 0)" 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