src/HOL/Isar_examples/Summation.thy
changeset 7982 d534b897ce39
parent 7968 964b65b4e433
child 8584 016314c2fa0a
     1.1 --- a/src/HOL/Isar_examples/Summation.thy	Sat Oct 30 20:13:16 1999 +0200
     1.2 +++ b/src/HOL/Isar_examples/Summation.thy	Sat Oct 30 20:20:48 1999 +0200
     1.3 @@ -16,7 +16,7 @@
     1.4  
     1.5  text {*
     1.6   Subsequently, we prove some summation laws of natural numbers
     1.7 - (including odds, squares and cubes).  These examples demonstrate how
     1.8 + (including odds, squares, and cubes).  These examples demonstrate how
     1.9   plain natural deduction (including induction) may be combined with
    1.10   calculational proof.
    1.11  *};
    1.12 @@ -26,25 +26,25 @@
    1.13  
    1.14  text {*
    1.15    The binder operator $\idt{sum} :: (\idt{nat} \To \idt{nat}) \To
    1.16 - \idt{nat} \To \idt{nat}$ formalizes summation from $0$ up to $k$
    1.17 - (excluding the bound).
    1.18 + \idt{nat} \To \idt{nat}$ formalizes summation of natural numbers
    1.19 + indexed from $0$ up to $k$ (excluding the bound):
    1.20   \[
    1.21   \sum\limits_{i < k} f(i) = \idt{sum} \ap (\lam i f \ap i) \ap k
    1.22   \]
    1.23  *};
    1.24  
    1.25  consts
    1.26 -  sum   :: "[nat => nat, nat] => nat";
    1.27 +  sum :: "[nat => nat, nat] => nat";
    1.28  
    1.29  primrec
    1.30    "sum f 0 = 0"
    1.31    "sum f (Suc n) = f n + sum f n";
    1.32  
    1.33  syntax
    1.34 -  "_SUM" :: "idt => nat => nat => nat"
    1.35 +  "_SUM" :: "[idt, nat, nat] => nat"
    1.36      ("SUM _ < _. _" [0, 0, 10] 10);
    1.37  translations
    1.38 -  "SUM i < k. b" == "sum (%i. b) k";
    1.39 +  "SUM i < k. b" == "sum (\<lambda>i. b) k";
    1.40  
    1.41  
    1.42  subsection {* Summation laws *};
    1.43 @@ -69,8 +69,8 @@
    1.44  
    1.45  text {*
    1.46   The sum of natural numbers $0 + \cdots + n$ equals $n \times (n +
    1.47 - 1)/2$.  In order to avoid formal reasoning about division, we just
    1.48 - show $2 \times \Sigma_{i < n} i = n \times (n + 1)$.
    1.49 + 1)/2$.  Avoiding formal reasoning about division we prove this
    1.50 + equation multiplied by $2$.
    1.51  *};
    1.52  
    1.53  theorem sum_of_naturals:
    1.54 @@ -90,23 +90,22 @@
    1.55   The above proof is a typical instance of mathematical induction.  The
    1.56   main statement is viewed as some $\var{P} \ap n$ that is split by the
    1.57   induction method into base case $\var{P} \ap 0$, and step case
    1.58 - $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for any $n$.
    1.59 + $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap n)$ for arbitrary $n$.
    1.60  
    1.61   The step case is established by a short calculation in forward
    1.62   manner.  Starting from the left-hand side $\var{S} \ap (n + 1)$ of
    1.63 - the thesis, the final result is achieved by basic transformations
    1.64 - involving arithmetic reasoning (using the Simplifier).  The main
    1.65 - point is where the induction hypothesis $\var{S} \ap n = n \times (n
    1.66 - + 1)$ is introduced in order to replace a certain subterm.  So the
    1.67 + the thesis, the final result is achieved by transformations involving
    1.68 + basic arithmetic reasoning (using the Simplifier).  The main point is
    1.69 + where the induction hypothesis $\var{S} \ap n = n \times (n + 1)$ is
    1.70 + introduced in order to replace a certain subterm.  So the
    1.71   ``transitivity'' rule involved here is actual \emph{substitution}.
    1.72   Also note how the occurrence of ``\dots'' in the subsequent step
    1.73 - documents the position where the right-hand side of the hypotheses
    1.74 + documents the position where the right-hand side of the hypothesis
    1.75   got filled in.
    1.76  
    1.77   \medskip A further notable point here is integration of calculations
    1.78 - with plain natural deduction.  This works works quite well in Isar
    1.79 - for two reasons.
    1.80 -
    1.81 + with plain natural deduction.  This works so well in Isar for two
    1.82 + reasons.
    1.83   \begin{enumerate}
    1.84  
    1.85   \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
    1.86 @@ -116,19 +115,18 @@
    1.87  
    1.88   \item There are two \emph{separate} primitives for building natural
    1.89   deduction contexts: \isakeyword{fix}~$x$ and \isakeyword{assume}~$A$.
    1.90 - Thus it is possible to start reasoning with new ``arbitrary, but
    1.91 - fixed'' elements before bringing in the actual assumptions.
    1.92 - Occasionally, natural deduction is formalized with basic context
    1.93 - elements of the form $x:A$; this would rule out mixing with
    1.94 - calculations as done here.
    1.95 + Thus it is possible to start reasoning with some new ``arbitrary, but
    1.96 + fixed'' elements before bringing in the actual assumption.  In
    1.97 + contrast, natural deduction is occasionally formalized with basic
    1.98 + context elements of the form $x:A$ instead.
    1.99  
   1.100   \end{enumerate}
   1.101  *};
   1.102  
   1.103  text {*
   1.104 - \medskip We derive further summation laws for odds, squares, cubes as
   1.105 - follows.  The basic technique of induction plus calculation is the
   1.106 - same.
   1.107 + \medskip We derive further summation laws for odds, squares, and
   1.108 + cubes as follows.  The basic technique of induction plus calculation
   1.109 + is the same as before.
   1.110  *};
   1.111  
   1.112  theorem sum_of_odds:
   1.113 @@ -175,20 +173,20 @@
   1.114  text {*
   1.115   Comparing these examples with the tactic script version
   1.116   \url{http://isabelle.in.tum.de/library/HOL/ex/NatSum.html}, we note
   1.117 - an important difference how of induction vs.\ simplification is
   1.118 + an important difference of how induction vs.\ simplification is
   1.119   applied.  While \cite[\S10]{isabelle-ref} advises for these examples
   1.120   that ``induction should not be applied until the goal is in the
   1.121   simplest form'' this would be a very bad idea in our setting.
   1.122  
   1.123   Simplification normalizes all arithmetic expressions involved,
   1.124 - producing huge intermediate goals.  Applying induction afterwards,
   1.125 - the Isar document would then have to reflect the emerging
   1.126 - configuration by appropriate the sub-proofs.  This would result in
   1.127 - badly structured, low-level technical reasoning, without any good
   1.128 - idea of the actual point.
   1.129 + producing huge intermediate goals.  With applying induction
   1.130 + afterwards, the Isar proof text would have to reflect the emerging
   1.131 + configuration by appropriate sub-proofs.  This would result in badly
   1.132 + structured, low-level technical reasoning, without any good idea of
   1.133 + the actual point.
   1.134  
   1.135   \medskip As a general rule of good proof style, automatic methods
   1.136 - such as $\idt{simp}$ or $\idt{auto}$ should normally never used as
   1.137 + such as $\idt{simp}$ or $\idt{auto}$ should normally be never used as
   1.138   initial proof methods, but only as terminal ones, solving certain
   1.139   goals completely.
   1.140  *};