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