--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Wed Aug 31 15:47:41 2005 +0200
+++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Wed Aug 31 17:53:35 2005 +0200
@@ -75,23 +75,23 @@
definition is obvious:
*}
-consts comp :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list";
+consts compile :: "('a,'v)expr \<Rightarrow> ('a,'v)instr list"
primrec
-"comp (Cex v) = [Const v]"
-"comp (Vex a) = [Load a]"
-"comp (Bex f e1 e2) = (comp e2) @ (comp e1) @ [Apply f]";
+"compile (Cex v) = [Const v]"
+"compile (Vex a) = [Load a]"
+"compile (Bex f e1 e2) = (compile e2) @ (compile e1) @ [Apply f]"
text{*
Now we have to prove the correctness of the compiler, i.e.\ that the
execution of a compiled expression results in the value of the expression:
*}
-theorem "exec (comp e) s [] = [value e s]";
+theorem "exec (compile e) s [] = [value e s]";
(*<*)oops;(*>*)
text{*\noindent
This theorem needs to be generalized:
*}
-theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
+theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs";
txt{*\noindent
It will be proved by induction on @{term"e"} followed by simplification.
@@ -124,14 +124,14 @@
text{*\noindent
Although this is more compact, it is less clear for the reader of the proof.
-We could now go back and prove \isa{exec (comp e) s [] = [value e s]}
+We could now go back and prove @{prop"exec (compile e) s [] = [value e s]"}
merely by simplification with the generalized version we just proved.
However, this is unnecessary because the generalized version fully subsumes
its instance.%
\index{compiling expressions example|)}
*}
(*<*)
-theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
+theorem "\<forall>vs. exec (compile e) s vs = (value e s) # vs";
by(induct_tac e, auto);
end
(*>*)
--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Aug 31 15:47:41 2005 +0200
+++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Wed Aug 31 17:53:35 2005 +0200
@@ -97,19 +97,19 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{consts}\isamarkupfalse%
-\ comp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequoteclose}\isanewline
+\ compile\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequoteclose}\isanewline
\isacommand{primrec}\isamarkupfalse%
\isanewline
-{\isachardoublequoteopen}comp\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}comp\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequoteclose}\isanewline
-{\isachardoublequoteopen}comp\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}comp\ e{\isadigit{2}}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}comp\ e{\isadigit{1}}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequoteclose}%
+{\isachardoublequoteopen}compile\ {\isacharparenleft}Cex\ v{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Const\ v{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+{\isachardoublequoteopen}compile\ {\isacharparenleft}Vex\ a{\isacharparenright}\ \ \ \ \ \ \ {\isacharequal}\ {\isacharbrackleft}Load\ a{\isacharbrackright}{\isachardoublequoteclose}\isanewline
+{\isachardoublequoteopen}compile\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}compile\ e{\isadigit{2}}{\isacharparenright}\ {\isacharat}\ {\isacharparenleft}compile\ e{\isadigit{1}}{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}Apply\ f{\isacharbrackright}{\isachardoublequoteclose}%
\begin{isamarkuptext}%
Now we have to prove the correctness of the compiler, i.e.\ that the
execution of a compiled expression results in the value of the expression:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
-\ {\isachardoublequoteopen}exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}exec\ {\isacharparenleft}compile\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
@@ -129,7 +129,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}comp\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequoteclose}%
+\ {\isachardoublequoteopen}{\isasymforall}vs{\isachardot}\ exec\ {\isacharparenleft}compile\ e{\isacharparenright}\ s\ vs\ {\isacharequal}\ {\isacharparenleft}value\ e\ s{\isacharparenright}\ {\isacharhash}\ vs{\isachardoublequoteclose}%
\isadelimproof
%
\endisadelimproof
@@ -202,7 +202,7 @@
\noindent
Although this is more compact, it is less clear for the reader of the proof.
-We could now go back and prove \isa{exec (comp e) s [] = [value e s]}
+We could now go back and prove \isa{exec\ {\isacharparenleft}compile\ e{\isacharparenright}\ s\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}value\ e\ s{\isacharbrackright}}
merely by simplification with the generalized version we just proved.
However, this is unnecessary because the generalized version fully subsumes
its instance.%