tuned
authornipkow
Wed Jun 22 07:54:13 2005 +0200 (2005-06-22)
changeset 16522f718767efd49
parent 16521 ad77345f1db8
child 16523 f8a734dc0fbc
tuned
doc-src/IsarOverview/Isar/Induction.thy
doc-src/IsarOverview/Isar/document/Induction.tex
     1.1 --- a/doc-src/IsarOverview/Isar/Induction.thy	Wed Jun 22 07:54:01 2005 +0200
     1.2 +++ b/doc-src/IsarOverview/Isar/Induction.thy	Wed Jun 22 07:54:13 2005 +0200
     1.3 @@ -77,7 +77,7 @@
     1.4  subsection{*Structural induction*}
     1.5  
     1.6  text{* We start with an inductive proof where both cases are proved automatically: *}
     1.7 -lemma "2 * (\<Sum>i::nat < n+1. i) = n*(n+1)"
     1.8 +lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)"
     1.9  by (induct n, simp_all)
    1.10  
    1.11  text{*\noindent The constraint @{text"::nat"} is needed because all of
    1.12 @@ -86,7 +86,7 @@
    1.13  If we want to expose more of the structure of the
    1.14  proof, we can use pattern matching to avoid having to repeat the goal
    1.15  statement: *}
    1.16 -lemma "2 * (\<Sum>i::nat = 0..<n+1. i) = n*(n+1)" (is "?P n")
    1.17 +lemma "2 * (\<Sum>i::nat\<le>n. i) = n*(n+1)" (is "?P n")
    1.18  proof (induct n)
    1.19    show "?P 0" by simp
    1.20  next
    1.21 @@ -97,7 +97,7 @@
    1.22  text{* \noindent We could refine this further to show more of the equational
    1.23  proof. Instead we explore the same avenue as for case distinctions:
    1.24  introducing context via the \isakeyword{case} command: *}
    1.25 -lemma "2 * (\<Sum>i::nat < n+1. i) = n*(n+1)"
    1.26 +lemma "2 * (\<Sum>i::nat \<le> n. i) = n*(n+1)"
    1.27  proof (induct n)
    1.28    case 0 show ?case by simp
    1.29  next
     2.1 --- a/doc-src/IsarOverview/Isar/document/Induction.tex	Wed Jun 22 07:54:01 2005 +0200
     2.2 +++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Wed Jun 22 07:54:13 2005 +0200
     2.3 @@ -127,7 +127,7 @@
     2.4  We start with an inductive proof where both cases are proved automatically:%
     2.5  \end{isamarkuptext}%
     2.6  \isamarkuptrue%
     2.7 -\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
     2.8 +\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
     2.9  \isamarkupfalse%
    2.10  \isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
    2.11  %
    2.12 @@ -140,7 +140,7 @@
    2.13  statement:%
    2.14  \end{isamarkuptext}%
    2.15  \isamarkuptrue%
    2.16 -\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
    2.17 +\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat{\isasymle}n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
    2.18  \isamarkupfalse%
    2.19  \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
    2.20  \ \ \isamarkupfalse%
    2.21 @@ -163,7 +163,7 @@
    2.22  introducing context via the \isakeyword{case} command:%
    2.23  \end{isamarkuptext}%
    2.24  \isamarkuptrue%
    2.25 -\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
    2.26 +\isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isasymle}\ n{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
    2.27  \isamarkupfalse%
    2.28  \isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
    2.29  \ \ \isamarkupfalse%