doc-src/TutorialI/CodeGen/CodeGen.thy

 (*>*)
 
 section{*Case Study: Compiling Expressions*}
 
 text{*\label{sec:ExprCompiler}
+\index{compiling expressions example|(}%
 The task is to develop a compiler from a generic type of expressions (built
 from variables, constants and binary operations) to a stack machine.  This
 generic type of expressions is a generalization of the boolean expressions in
 \S\ref{sec:boolex}.  This time we do not commit ourselves to a particular
 type of variables or values but make them type parameters.  Neither is there

   | Apply f  \<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))";
 
 text{*\noindent
 Recall that @{term"hd"} and @{term"tl"}
 return the first element and the remainder of a list.
-Because all functions are total, @{term"hd"} is defined even for the empty
+Because all functions are total, \cdx{hd} is defined even for the empty
 list, although we do not know what the result is. Thus our model of the
 machine always terminates properly, although the definition above does not
 tell us much about the result in situations where @{term"Apply"} was executed
 with fewer than two elements on the stack.
 

 execution of a compiled expression results in the value of the expression:
 *}
 theorem "exec (comp e) s [] = [value e s]";
 (*<*)oops;(*>*)
 text{*\noindent
-This theorem needs to be generalized to
+This theorem needs to be generalized:
 *}
 
 theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
 
 txt{*\noindent
-which is proved by induction on @{term"e"} followed by simplification, once
-we have the following lemma about executing the concatenation of two
+It will be proved by induction on @{term"e"} followed by simplification.  
+First, we must prove a lemma about executing the concatenation of two
 instruction sequences:
 *}
 (*<*)oops;(*>*)
 lemma exec_app[simp]:
   "\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
 
 txt{*\noindent
 This requires induction on @{term"xs"} and ordinary simplification for the
 base cases. In the induction step, simplification leaves us with a formula
 that contains two @{text"case"}-expressions over instructions. Thus we add
-automatic case splitting as well, which finishes the proof:
+automatic case splitting, which finishes the proof:
 *}
 apply(induct_tac xs, simp, simp split: instr.split);
 (*<*)done(*>*)
 text{*\noindent
 Note that because both \methdx{simp_all} and \methdx{auto} perform simplification, they can

 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]}
 merely by simplification with the generalized version we just proved.
 However, this is unnecessary because the generalized version fully subsumes
-its instance.
+its instance.%
+\index{compiling expressions example|)}
 *}
 (*<*)
 theorem "\<forall>vs. exec (comp e) s vs = (value e s) # vs";
 by(induct_tac e, auto);
 end