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