--- a/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 16 13:42:21 2005 +0200
+++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Aug 16 13:42:23 2005 +0200
@@ -1,7 +1,20 @@
%
\begin{isabellebody}%
\def\isabellecontext{Induction}%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+\isamarkuptrue%
%
\begin{isamarkuptext}%
Assuming we have defined our function such that Isabelle could prove
@@ -19,8 +32,14 @@
for all recursive calls on the right-hand side. Here is a simple example
involving the predefined \isa{map} functional on lists:%
\end{isamarkuptext}%
+\isamarkupfalse%
+\isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
\isamarkuptrue%
-\isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
%
\begin{isamarkuptxt}%
\noindent
@@ -28,8 +47,8 @@
is the result of applying \isa{f} to all elements of \isa{xs}. We prove
this lemma by recursion induction over \isa{sep}:%
\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}\isamarkupfalse%
+\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}\isamarkuptrue%
%
\begin{isamarkuptxt}%
\noindent
@@ -44,10 +63,17 @@
\end{isabelle}
The rest is pure simplification:%
\end{isamarkuptxt}%
-\isamarkuptrue%
+\isamarkupfalse%
\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
\isamarkupfalse%
-\isacommand{done}\isamarkupfalse%
+\isacommand{done}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+\isamarkuptrue%
%
\begin{isamarkuptext}%
Try proving the above lemma by structural induction, and you find that you
@@ -75,8 +101,19 @@
The final case has an induction hypothesis: you may assume that \isa{P}
holds for the tail of that list.%
\end{isamarkuptext}%
-\isamarkuptrue%
-\isamarkupfalse%
+%
+\isadelimtheory
+%
+\endisadelimtheory
+%
+\isatagtheory
+%
+\endisatagtheory
+{\isafoldtheory}%
+%
+\isadelimtheory
+%
+\endisadelimtheory
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex