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  *};