--- a/src/Doc/ProgProve/Logic.thy Mon Oct 21 10:49:02 2013 +0200
+++ b/src/Doc/ProgProve/Logic.thy Mon Oct 21 21:06:19 2013 +0200
@@ -764,6 +764,26 @@
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