src/Doc/ProgProve/Logic.thy

 respects. @{text I} can have any number of arguments and each rule can have
 additional premises not involving @{text I}, so-called \concept{side
 conditions}. In rule inductions, these side-conditions appear as additional
 assumptions. The \isacom{for} clause seen in the definition of the reflexive
 transitive closure merely simplifies the form of the induction rule.
+
+\ifsem
+\subsection{Exercises}
+
+\begin{exercise}
+Consider the stack machine from \autoref{sec:aexp_comp}.
+A \concept{stack underflow} occurs when executing an instruction
+on a stack containing too few values, e.g., executing an @{text ADD}
+instruction on a stack of size less than two. Define an inductive predicate
+@{text "ok :: nat \<Rightarrow> instr list \<Rightarrow> nat \<Rightarrow> bool"}
+such that @{text "ok n is n'"} means that with any initial stack of length
+@{text n} the instructions @{text "is"} can be executed
+without stack underflow and that the final stack has length @{text n'}.
+Prove that @{text ok} correctly computes the final stack size
+@{prop[display] "\<lbrakk>ok n is n'; length stk = n\<rbrakk> \<Longrightarrow> length (exec is s stk) = n'"}
+and that instruction sequences generated by @{text comp}
+cannot cause stack underflow: \ @{text "ok n (comp a) ?"} \ for
+some suitable value of @{text "?"}.
+\end{exercise}
+\fi
 *}
 (*<*)
 end
 (*>*)