# HG changeset patch
# User paulson
# Date 1039794500 -3600
# Node ID b5cd10cb106b6dfbe89efc76136c1decd59ac031
# Parent  6844c38d74dfd7fba2e87c132106a58a0b4d9537
integer induction rules

diff -r 6844c38d74df -r b5cd10cb106b doc-src/TutorialI/Types/document/Axioms.tex
--- 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:
diff -r 6844c38d74df -r b5cd10cb106b doc-src/TutorialI/Types/document/Overloading.tex
--- 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:
diff -r 6844c38d74df -r b5cd10cb106b doc-src/TutorialI/Types/document/Overloading0.tex
--- 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:
diff -r 6844c38d74df -r b5cd10cb106b doc-src/TutorialI/Types/document/Overloading1.tex
--- 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:
diff -r 6844c38d74df -r b5cd10cb106b doc-src/TutorialI/Types/document/Overloading2.tex
--- 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:
diff -r 6844c38d74df -r b5cd10cb106b doc-src/TutorialI/Types/document/Pairs.tex
--- 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:
diff -r 6844c38d74df -r b5cd10cb106b doc-src/TutorialI/Types/document/Records.tex
--- 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:
diff -r 6844c38d74df -r b5cd10cb106b doc-src/TutorialI/Types/document/Typedefs.tex
--- 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:
diff -r 6844c38d74df -r b5cd10cb106b doc-src/TutorialI/Types/numerics.tex
--- 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}}