--- a/doc-src/TutorialI/Types/document/Axioms.tex Fri Dec 13 14:20:47 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Axioms.tex Fri Dec 13 16:48:20 2002 +0100
@@ -290,6 +290,7 @@
worry us.%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Overloading.tex Fri Dec 13 14:20:47 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading.tex Fri Dec 13 16:48:20 2002 +0100
@@ -1,6 +1,7 @@
%
\begin{isabellebody}%
\def\isabellecontext{Overloading}%
+\isanewline
\isamarkupfalse%
\isacommand{instance}\ list\ {\isacharcolon}{\isacharcolon}\ {\isacharparenleft}type{\isacharparenright}ordrel\isanewline
\isamarkupfalse%
@@ -21,6 +22,7 @@
\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}{\isacharequal}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ {\isasymequiv}\ \ {\isasymexists}zs{\isachardot}\ ys\ {\isacharequal}\ xs{\isacharat}zs{\isachardoublequote}\isanewline
strict{\isacharunderscore}prefix{\isacharunderscore}def{\isacharcolon}\isanewline
\ \ {\isachardoublequote}xs\ {\isacharless}{\isacharless}\ {\isacharparenleft}ys{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isacharcolon}{\isacharcolon}ordrel\ list{\isacharparenright}\ \ \ {\isasymequiv}\ \ xs\ {\isacharless}{\isacharless}{\isacharequal}\ ys\ {\isasymand}\ xs\ {\isasymnoteq}\ ys{\isachardoublequote}\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Overloading0.tex Fri Dec 13 14:20:47 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading0.tex Fri Dec 13 16:48:20 2002 +0100
@@ -49,6 +49,7 @@
To prevent such terms from even being formed requires the use of type classes.%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Overloading1.tex Fri Dec 13 14:20:47 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading1.tex Fri Dec 13 16:48:20 2002 +0100
@@ -81,6 +81,7 @@
we need to make lists a type of class \isa{ordrel}:%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Overloading2.tex Fri Dec 13 14:20:47 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Overloading2.tex Fri Dec 13 16:48:20 2002 +0100
@@ -53,6 +53,7 @@
For technical reasons, it is not translated back upon output.%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Pairs.tex Fri Dec 13 14:20:47 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Fri Dec 13 16:48:20 2002 +0100
@@ -101,6 +101,7 @@
\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
+\isanewline
\isamarkupfalse%
\isacommand{by}{\isacharparenleft}simp\ split{\isacharcolon}\ split{\isacharunderscore}split{\isacharparenright}\isamarkupfalse%
%
@@ -120,6 +121,7 @@
can be split as above. The same is true for paired set comprehension:%
\end{isamarkuptxt}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymlongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isanewline
\isamarkupfalse%
@@ -135,6 +137,7 @@
The same proof procedure works for%
\end{isamarkuptxt}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}p\ {\isasymin}\ {\isacharbraceleft}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}{\isachardot}\ x{\isacharequal}y{\isacharbraceright}\ {\isasymLongrightarrow}\ fst\ p\ {\isacharequal}\ snd\ p{\isachardoublequote}\isamarkupfalse%
%
@@ -147,6 +150,7 @@
may be present in the goal. Consider the following function:%
\end{isamarkuptxt}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\isacommand{consts}\ swap\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}b\ {\isasymRightarrow}\ {\isacharprime}b\ {\isasymtimes}\ {\isacharprime}a{\isachardoublequote}\isanewline
\isamarkupfalse%
@@ -188,6 +192,7 @@
with the rewrite rule \isa{split{\isacharunderscore}paired{\isacharunderscore}all}:%
\end{isamarkuptxt}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\isacommand{lemma}\ {\isachardoublequote}{\isasymAnd}p\ q{\isachardot}\ swap{\isacharparenleft}swap\ p{\isacharparenright}\ {\isacharequal}\ q\ {\isasymlongrightarrow}\ p\ {\isacharequal}\ q{\isachardoublequote}\isanewline
\isamarkupfalse%
@@ -217,6 +222,7 @@
where two separate \isa{simp} applications succeed.%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ split{\isacharunderscore}paired{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
@@ -245,6 +251,7 @@
\end{center}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Records.tex Fri Dec 13 14:20:47 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Records.tex Fri Dec 13 16:48:20 2002 +0100
@@ -452,6 +452,7 @@
\index{records|)}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/document/Typedefs.tex Fri Dec 13 14:20:47 2002 +0100
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex Fri Dec 13 16:48:20 2002 +0100
@@ -271,6 +271,7 @@
\index{types!defining|)}%
\end{isamarkuptext}%
\isamarkuptrue%
+\isanewline
\isamarkupfalse%
\end{isabellebody}%
%%% Local Variables:
--- a/doc-src/TutorialI/Types/numerics.tex Fri Dec 13 14:20:47 2002 +0100
+++ b/doc-src/TutorialI/Types/numerics.tex Fri Dec 13 16:48:20 2002 +0100
@@ -363,6 +363,18 @@
\isa{zdiv_zmult2_eq} is $-2$ while the right-hand side is~$-1$.%
\index{integers|)}\index{*int (type)|)}
+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 $<$):
+\begin{isabelle}
+\isasymlbrakk k\ \isasymle \ i;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk k\ \isasymle \ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
+\rulename{int_ge_induct}\isanewline
+\isasymlbrakk k\ <\ i;\ P(k+1);\ \isasymAnd i.\ \isasymlbrakk k\ <\ i;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i+1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
+\rulename{int_gr_induct}\isanewline
+\isasymlbrakk i\ \isasymle \ k;\ P\ k;\ \isasymAnd i.\ \isasymlbrakk i\ \isasymle \ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
+\rulename{int_le_induct}\isanewline
+\isasymlbrakk i\ <\ k;\ P(k-1);\ \isasymAnd i.\ \isasymlbrakk i\ <\ k;\ P\ i\isasymrbrakk \ \isasymLongrightarrow \ P(i-1)\isasymrbrakk \ \isasymLongrightarrow \ P\ i%
+\rulename{int_less_induct}
+\end{isabelle}
+
\subsection{The Type of Real Numbers, {\tt\slshape real}}