summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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