--- a/src/HOL/Isar_Examples/Summation.thy Mon Nov 02 11:43:02 2015 +0100
+++ b/src/HOL/Isar_Examples/Summation.thy Mon Nov 02 13:58:19 2015 +0100
@@ -9,16 +9,16 @@
begin
text \<open>Subsequently, we prove some summation laws of natural numbers
- (including odds, squares, and cubes). These examples demonstrate
- how plain natural deduction (including induction) may be combined
- with calculational proof.\<close>
+ (including odds, squares, and cubes). These examples demonstrate how plain
+ natural deduction (including induction) may be combined with calculational
+ proof.\<close>
subsection \<open>Summation laws\<close>
-text \<open>The sum of natural numbers $0 + \cdots + n$ equals $n \times
- (n + 1)/2$. Avoiding formal reasoning about division we prove this
- equation multiplied by $2$.\<close>
+text \<open>The sum of natural numbers \<open>0 + \<cdots> + n\<close> equals \<open>n \<times> (n + 1)/2\<close>.
+ Avoiding formal reasoning about division we prove this equation multiplied
+ by \<open>2\<close>.\<close>
theorem sum_of_naturals:
"2 * (\<Sum>i::nat=0..n. i) = n * (n + 1)"
@@ -35,47 +35,39 @@
by simp
qed
-text \<open>The above proof is a typical instance of mathematical
- induction. The main statement is viewed as some $\var{P} \ap n$
- that is split by the induction method into base case $\var{P} \ap
- 0$, and step case $\var{P} \ap n \Impl \var{P} \ap (\idt{Suc} \ap
- n)$ for arbitrary $n$.
+text \<open>The above proof is a typical instance of mathematical induction. The
+ main statement is viewed as some \<open>?P n\<close> that is split by the induction
+ method into base case \<open>?P 0\<close>, and step case \<open>?P n \<Longrightarrow> ?P (Suc n)\<close> for
+ arbitrary \<open>n\<close>.
- The step case is established by a short calculation in forward
- manner. Starting from the left-hand side $\var{S} \ap (n + 1)$ of
- the thesis, the final result is achieved by transformations
- involving basic arithmetic reasoning (using the Simplifier). The
- main point is where the induction hypothesis $\var{S} \ap n = n
- \times (n + 1)$ is introduced in order to replace a certain subterm.
- So the ``transitivity'' rule involved here is actual
- \emph{substitution}. Also note how the occurrence of ``\dots'' in
- the subsequent step documents the position where the right-hand side
- of the hypothesis got filled in.
+ The step case is established by a short calculation in forward manner.
+ Starting from the left-hand side \<open>?S (n + 1)\<close> of the thesis, the final
+ result is achieved by transformations involving basic arithmetic reasoning
+ (using the Simplifier). The main point is where the induction hypothesis
+ \<open>?S n = n \<times> (n + 1)\<close> is introduced in order to replace a certain subterm.
+ So the ``transitivity'' rule involved here is actual \<^emph>\<open>substitution\<close>. Also
+ note how the occurrence of ``\dots'' in the subsequent step documents the
+ position where the right-hand side of the hypothesis got filled in.
- \medskip A further notable point here is integration of calculations
- with plain natural deduction. This works so well in Isar for two
- reasons.
- \begin{enumerate}
-
- \item Facts involved in \isakeyword{also}~/ \isakeyword{finally}
- calculational chains may be just anything. There is nothing special
- about \isakeyword{have}, so the natural deduction element
- \isakeyword{assume} works just as well.
+ \<^medskip>
+ A further notable point here is integration of calculations with plain
+ natural deduction. This works so well in Isar for two reasons.
- \item There are two \emph{separate} primitives for building natural
- deduction contexts: \isakeyword{fix}~$x$ and
- \isakeyword{assume}~$A$. Thus it is possible to start reasoning
- with some new ``arbitrary, but fixed'' elements before bringing in
- the actual assumption. In contrast, natural deduction is
- occasionally formalized with basic context elements of the form
- $x:A$ instead.
+ \<^enum> Facts involved in \isakeyword{also}~/ \isakeyword{finally}
+ calculational chains may be just anything. There is nothing special
+ about \isakeyword{have}, so the natural deduction element
+ \isakeyword{assume} works just as well.
+
+ \<^enum> There are two \<^emph>\<open>separate\<close> primitives for building natural deduction
+ contexts: \isakeyword{fix}~\<open>x\<close> and \isakeyword{assume}~\<open>A\<close>. Thus it is
+ possible to start reasoning with some new ``arbitrary, but fixed''
+ elements before bringing in the actual assumption. In contrast, natural
+ deduction is occasionally formalized with basic context elements of the
+ form \<open>x:A\<close> instead.
- \end{enumerate}
-\<close>
-
-text \<open>\medskip We derive further summation laws for odds, squares,
- and cubes as follows. The basic technique of induction plus
- calculation is the same as before.\<close>
+ \<^medskip>
+ We derive further summation laws for odds, squares, and cubes as follows.
+ The basic technique of induction plus calculation is the same as before.\<close>
theorem sum_of_odds:
"(\<Sum>i::nat=0..<n. 2 * i + 1) = n^Suc (Suc 0)"
@@ -93,9 +85,8 @@
by simp
qed
-text \<open>Subsequently we require some additional tweaking of Isabelle
- built-in arithmetic simplifications, such as bringing in
- distributivity by hand.\<close>
+text \<open>Subsequently we require some additional tweaking of Isabelle built-in
+ arithmetic simplifications, such as bringing in distributivity by hand.\<close>
lemmas distrib = add_mult_distrib add_mult_distrib2
@@ -134,15 +125,13 @@
text \<open>Note that in contrast to older traditions of tactical proof
scripts, the structured proof applies induction on the original,
- unsimplified statement. This allows to state the induction cases
- robustly and conveniently. Simplification (or other automated)
- methods are then applied in terminal position to solve certain
- sub-problems completely.
+ unsimplified statement. This allows to state the induction cases robustly
+ and conveniently. Simplification (or other automated) methods are then
+ applied in terminal position to solve certain sub-problems completely.
- As a general rule of good proof style, automatic methods such as
- $\idt{simp}$ or $\idt{auto}$ should normally be never used as
- initial proof methods with a nested sub-proof to address the
- automatically produced situation, but only as terminal ones to solve
- sub-problems.\<close>
+ As a general rule of good proof style, automatic methods such as \<open>simp\<close> or
+ \<open>auto\<close> should normally be never used as initial proof methods with a
+ nested sub-proof to address the automatically produced situation, but only
+ as terminal ones to solve sub-problems.\<close>
end