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