--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed May 25 09:03:53 2005 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed May 25 09:04:24 2005 +0200
@@ -105,12 +105,27 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+It will be proved by induction on \isa{e} followed by simplification.
+First, we must prove a lemma about executing the concatenation of two
+instruction sequences:%
+\end{isamarkuptxt}%
\isamarkuptrue%
\isamarkupfalse%
\isacommand{lemma}\ exec{\isacharunderscore}app{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
\ \ {\isachardoublequote}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}xs{\isacharat}ys{\isacharparenright}\ s\ vs\ {\isacharequal}\ exec\ ys\ s\ {\isacharparenleft}exec\ xs\ s\ vs{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+\noindent
+This requires induction on \isa{xs} and ordinary simplification for the
+base cases. In the induction step, simplification leaves us with a formula
+that contains two \isa{case}-expressions over instructions. Thus we add
+automatic case splitting, which finishes the proof:%
+\end{isamarkuptxt}%
\isamarkuptrue%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharcomma}\ simp\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -122,7 +137,7 @@
\isamarkuptrue%
\isamarkupfalse%
\isamarkupfalse%
-\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharcomma}\ simp{\isacharunderscore}all\ split{\isacharcolon}\ instr{\isachardot}split{\isacharparenright}\isamarkupfalse%
\isamarkupfalse%
%
\begin{isamarkuptext}%
@@ -137,7 +152,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isamarkupfalse%
-\isanewline
\isamarkupfalse%
\isamarkupfalse%
\end{isabellebody}%