src/HOL/Isar_examples/Summation.thy
author wenzelm
Sat Oct 30 20:20:48 1999 +0200 (1999-10-30)
changeset 7982 d534b897ce39
parent 7968 964b65b4e433
child 8584 016314c2fa0a
permissions -rw-r--r--
improved presentation;
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@7748
     6
header {* Summing natural numbers *};
wenzelm@7443
     7
wenzelm@7443
     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@7968
    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@7968
    22
*};
wenzelm@7968
    23
wenzelm@7761
    24
wenzelm@7748
    25
subsection {* A summation operator *};
wenzelm@7443
    26
wenzelm@7968
    27
text {*
wenzelm@7968
    28
  The binder operator $\idt{sum} :: (\idt{nat} \To \idt{nat}) \To
wenzelm@7982
    29
 \idt{nat} \To \idt{nat}$ formalizes summation of natural numbers
wenzelm@7982
    30
 indexed from $0$ up to $k$ (excluding the bound):
wenzelm@7968
    31
 \[
wenzelm@7968
    32
 \sum\limits_{i < k} f(i) = \idt{sum} \ap (\lam i f \ap i) \ap k
wenzelm@7968
    33
 \]
wenzelm@7968
    34
*};
wenzelm@7968
    35
wenzelm@7443
    36
consts
wenzelm@7982
    37
  sum :: "[nat => nat, nat] => nat";
wenzelm@7443
    38
wenzelm@7443
    39
primrec
wenzelm@7443
    40
  "sum f 0 = 0"
wenzelm@7443
    41
  "sum f (Suc n) = f n + sum f n";
wenzelm@7443
    42
wenzelm@7443
    43
syntax
wenzelm@7982
    44
  "_SUM" :: "[idt, nat, nat] => nat"
wenzelm@7800
    45
    ("SUM _ < _. _" [0, 0, 10] 10);
wenzelm@7443
    46
translations
wenzelm@7982
    47
  "SUM i < k. b" == "sum (\<lambda>i. b) k";
wenzelm@7443
    48
wenzelm@7443
    49
wenzelm@7443
    50
subsection {* Summation laws *};
wenzelm@7443
    51
wenzelm@7869
    52
text_raw {* \begin{comment} *};
wenzelm@7800
    53
wenzelm@7761
    54
(* FIXME binary arithmetic does not yet work here *)
wenzelm@7761
    55
wenzelm@7761
    56
syntax
wenzelm@7443
    57
  "3" :: nat  ("3")
wenzelm@7443
    58
  "4" :: nat  ("4")
wenzelm@7443
    59
  "6" :: nat  ("6");
wenzelm@7443
    60
wenzelm@7443
    61
translations
wenzelm@7443
    62
  "3" == "Suc 2"
wenzelm@7443
    63
  "4" == "Suc 3"
wenzelm@7443
    64
  "6" == "Suc (Suc 4)";
wenzelm@7443
    65
wenzelm@7443
    66
theorems [simp] = add_mult_distrib add_mult_distrib2 mult_ac;
wenzelm@7443
    67
wenzelm@7869
    68
text_raw {* \end{comment} *};
wenzelm@7443
    69
wenzelm@7968
    70
text {*
wenzelm@7968
    71
 The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
wenzelm@7982
    72
 1)/2$.  Avoiding formal reasoning about division we prove this
wenzelm@7982
    73
 equation multiplied by $2$.
wenzelm@7968
    74
*};
wenzelm@7800
    75
wenzelm@7800
    76
theorem sum_of_naturals:
wenzelm@7800
    77
  "2 * (SUM i < n + 1. i) = n * (n + 1)"
wenzelm@7480
    78
  (is "?P n" is "?S n = _");
wenzelm@7443
    79
proof (induct n);
wenzelm@7480
    80
  show "?P 0"; by simp;
wenzelm@7443
    81
wenzelm@7443
    82
  fix n;
wenzelm@7480
    83
  have "?S (n + 1) = ?S n + 2 * (n + 1)"; by simp;
wenzelm@7480
    84
  also; assume "?S n = n * (n + 1)";
wenzelm@7443
    85
  also; have "... + 2 * (n + 1) = (n + 1) * (n + 2)"; by simp;
wenzelm@7480
    86
  finally; show "?P (Suc n)"; by simp;
wenzelm@7443
    87
qed;
wenzelm@7443
    88
wenzelm@7968
    89
text {*
wenzelm@7968
    90
 The above proof is a typical instance of mathematical induction.  The
wenzelm@7968
    91
 main statement is viewed as some $\var{P} \ap n$ that is split by the
wenzelm@7968
    92
 induction method into base case $\var{P} \ap 0$, and step case
wenzelm@7982
    93
 $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
wenzelm@7968
    94
wenzelm@7968
    95
 The step case is established by a short calculation in forward
wenzelm@7968
    96
 manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
wenzelm@7982
    97
 the thesis, the final result is achieved by transformations involving
wenzelm@7982
    98
 basic arithmetic reasoning (using the Simplifier).  The main point is
wenzelm@7982
    99
 where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
wenzelm@7982
   100
 introduced in order to replace a certain subterm.  So the
wenzelm@7968
   101
 ``transitivity'' rule involved here is actual \emph{substitution}.
wenzelm@7968
   102
 Also note how the occurrence of ``\dots'' in the subsequent step
wenzelm@7982
   103
 documents the position where the right-hand side of the hypothesis
wenzelm@7968
   104
 got filled in.
wenzelm@7968
   105
wenzelm@7968
   106
 \medskip A further notable point here is integration of calculations
wenzelm@7982
   107
 with plain natural deduction.  This works so well in Isar for two
wenzelm@7982
   108
 reasons.
wenzelm@7968
   109
 \begin{enumerate}
wenzelm@7968
   110
wenzelm@7968
   111
 \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
wenzelm@7968
   112
 calculational chains may be just anything.  There is nothing special
wenzelm@7968
   113
 about \isakeyword{have}, so the natural deduction element
wenzelm@7968
   114
 \isakeyword{assume} works just as well.
wenzelm@7968
   115
wenzelm@7968
   116
 \item There are two \emph{separate} primitives for building natural
wenzelm@7968
   117
 deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
wenzelm@7982
   118
 Thus it is possible to start reasoning with some new ``arbitrary, but
wenzelm@7982
   119
 fixed'' elements before bringing in the actual assumption.  In
wenzelm@7982
   120
 contrast, natural deduction is occasionally formalized with basic
wenzelm@7982
   121
 context elements of the form $x:A$ instead.
wenzelm@7968
   122
wenzelm@7968
   123
 \end{enumerate}
wenzelm@7968
   124
*};
wenzelm@7968
   125
wenzelm@7968
   126
text {*
wenzelm@7982
   127
 \medskip We derive further summation laws for odds, squares, and
wenzelm@7982
   128
 cubes as follows.  The basic technique of induction plus calculation
wenzelm@7982
   129
 is the same as before.
wenzelm@7968
   130
*};
wenzelm@7968
   131
wenzelm@7800
   132
theorem sum_of_odds:
wenzelm@7800
   133
  "(SUM i < n. 2 * i + 1) = n^2"
wenzelm@7480
   134
  (is "?P n" is "?S n = _");
wenzelm@7443
   135
proof (induct n);
wenzelm@7480
   136
  show "?P 0"; by simp;
wenzelm@7443
   137
wenzelm@7443
   138
  fix n;
wenzelm@7480
   139
  have "?S (n + 1) = ?S n + 2 * n + 1"; by simp;
wenzelm@7480
   140
  also; assume "?S n = n^2";
wenzelm@7443
   141
  also; have "... + 2 * n + 1 = (n + 1)^2"; by simp;
wenzelm@7480
   142
  finally; show "?P (Suc n)"; by simp;
wenzelm@7443
   143
qed;
wenzelm@7443
   144
wenzelm@7761
   145
theorem sum_of_squares:
wenzelm@7761
   146
  "6 * (SUM i < n + 1. i^2) = n * (n + 1) * (2 * n + 1)"
wenzelm@7480
   147
  (is "?P n" is "?S n = _");
wenzelm@7443
   148
proof (induct n);
wenzelm@7480
   149
  show "?P 0"; by simp;
wenzelm@7443
   150
wenzelm@7443
   151
  fix n;
wenzelm@7480
   152
  have "?S (n + 1) = ?S n + 6 * (n + 1)^2"; by simp;
wenzelm@7480
   153
  also; assume "?S n = n * (n + 1) * (2 * n + 1)";
wenzelm@7800
   154
  also; have "... + 6 * (n + 1)^2 =
wenzelm@7800
   155
    (n + 1) * (n + 2) * (2 * (n + 1) + 1)"; by simp;
wenzelm@7480
   156
  finally; show "?P (Suc n)"; by simp;
wenzelm@7443
   157
qed;
wenzelm@7443
   158
wenzelm@7800
   159
theorem sum_of_cubes:
wenzelm@7800
   160
  "4 * (SUM i < n + 1. i^3) = (n * (n + 1))^2"
wenzelm@7480
   161
  (is "?P n" is "?S n = _");
wenzelm@7443
   162
proof (induct n);
wenzelm@7480
   163
  show "?P 0"; by simp;
wenzelm@7443
   164
wenzelm@7443
   165
  fix n;
wenzelm@7480
   166
  have "?S (n + 1) = ?S n + 4 * (n + 1)^3"; by simp;
wenzelm@7480
   167
  also; assume "?S n = (n * (n + 1))^2";
wenzelm@7761
   168
  also; have "... + 4 * (n + 1)^3 = ((n + 1) * ((n + 1) + 1))^2";
wenzelm@7761
   169
    by simp;
wenzelm@7480
   170
  finally; show "?P (Suc n)"; by simp;
wenzelm@7443
   171
qed;
wenzelm@7443
   172
wenzelm@7968
   173
text {*
wenzelm@7968
   174
 Comparing these examples with the tactic script version
wenzelm@7968
   175
 \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
wenzelm@7982
   176
 an important difference of how induction vs.\ simplification is
wenzelm@7968
   177
 applied.  While \cite[\S10]{isabelle-ref} advises for these examples
wenzelm@7968
   178
 that ``induction should not be applied until the goal is in the
wenzelm@7968
   179
 simplest form'' this would be a very bad idea in our setting.
wenzelm@7968
   180
wenzelm@7968
   181
 Simplification normalizes all arithmetic expressions involved,
wenzelm@7982
   182
 producing huge intermediate goals.  With applying induction
wenzelm@7982
   183
 afterwards, the Isar proof text would have to reflect the emerging
wenzelm@7982
   184
 configuration by appropriate sub-proofs.  This would result in badly
wenzelm@7982
   185
 structured, low-level technical reasoning, without any good idea of
wenzelm@7982
   186
 the actual point.
wenzelm@7968
   187
wenzelm@7968
   188
 \medskip As a general rule of good proof style, automatic methods
wenzelm@7982
   189
 such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as
wenzelm@7968
   190
 initial proof methods, but only as terminal ones, solving certain
wenzelm@7968
   191
 goals completely.
wenzelm@7968
   192
*};
wenzelm@7968
   193
wenzelm@7443
   194
end;