# 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 \ ('a,'v)instr list"; +consts compile :: "('a,'v)expr \ ('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 "\vs. exec (comp e) s vs = (value e s) # vs"; +theorem "\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 "\vs. exec (comp e) s vs = (value e s) # vs"; +theorem "\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.%