--- a/src/HOL/Isar_Examples/Summation.thy Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Summation.thy Sat Dec 26 15:44:14 2015 +0100
@@ -1,5 +1,5 @@
(* Title: HOL/Isar_Examples/Summation.thy
- Author: Markus Wenzel
+ Author: Makarius
*)
section \<open>Summing natural numbers\<close>
@@ -8,17 +8,19 @@
imports Main
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>
+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>
subsection \<open>Summation laws\<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>
+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,39 +37,38 @@
by simp
qed
-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>.
+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 \<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.
+ (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.
- \<^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> Facts involved in \<^theory_text>\<open>also\<close>~/ \<^theory_text>\<open>finally\<close> calculational chains may be just
+ anything. There is nothing special about \<^theory_text>\<open>have\<close>, so the natural deduction
+ element \<^theory_text>\<open>assume\<close> 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.
+ contexts: \<^theory_text>\<open>fix x\<close> and \<^theory_text>\<open>assume 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.
\<^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>
+ 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)"
@@ -85,8 +86,10 @@
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
@@ -123,15 +126,17 @@
by simp
qed
-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.
+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.
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>
+ \<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