# HG changeset patch
# User nipkow
# Date 1125503615 -7200
# Node ID 6859484b5b2bd79bd2fbec7d92c0cb74fc73dc22
# Parent  ebd268806589ffac85238e756bd7cc3aabf569bc
comp -> compile

diff -r ebd268806589 -r 6859484b5b2b doc-src/TutorialI/CodeGen/CodeGen.thy
--- 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
 (*>*)
diff -r ebd268806589 -r 6859484b5b2b doc-src/TutorialI/CodeGen/document/CodeGen.tex
--- 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.%