doc-src/TutorialI/Types/numerics.tex
 changeset 13750 b5cd10cb106b parent 12333 ef43a3d6e962 child 13979 4c3a638828b9
     1.1 --- a/doc-src/TutorialI/Types/numerics.tex	Fri Dec 13 14:20:47 2002 +0100
1.2 +++ b/doc-src/TutorialI/Types/numerics.tex	Fri Dec 13 16:48:20 2002 +0100
1.3 @@ -363,6 +363,18 @@
1.4  \isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
1.5  \index{integers|)}\index{*int (type)|)}
1.6
1.7 +Induction is less important for integers than it is for the natural numbers, but it can be valuable if the range of integers has a lower or upper bound.  There are four rules for integer induction, corresponding to the possible relations of the bound ($\ge$, $>$, $\le$ and $<$):
1.8 +\begin{isabelle}
1.9 +\isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
1.10 +\rulename{int_ge_induct}\isanewline
1.11 +\isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
1.12 +\rulename{int_gr_induct}\isanewline
1.13 +\isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
1.14 +\rulename{int_le_induct}\isanewline
1.15 +\isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
1.16 +\rulename{int_less_induct}
1.17 +\end{isabelle}
1.18 +
1.19
1.20  \subsection{The Type of Real Numbers, {\tt\slshape real}}
1.21