--- a/src/Doc/ProgProve/Logic.thy Thu Oct 24 19:43:21 2013 +0200
+++ b/src/Doc/ProgProve/Logic.thy Fri Oct 25 16:20:54 2013 +0200
@@ -769,6 +769,17 @@
\subsection{Exercises}
\begin{exercise}
+In \autoref{sec:AExp} we defined a recursive evaluation function
+@{text "aval :: aexp \<Rightarrow> state \<Rightarrow> val"}.
+Define an inductive evaluation predicate
+@{text "aval_rel :: aexp \<Rightarrow> state \<Rightarrow> val \<Rightarrow> bool"}
+and prove that it agrees with the recursive function:
+@{prop "aval_rel a s v \<Longrightarrow> aval a s = v"},
+@{prop "aval a s = v \<Longrightarrow> aval_rel a s v"} and thus
+\noquotes{@{prop [source] "aval_rel a s v \<longleftrightarrow> aval a s = v"}}.
+\end{exercise}
+
+\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}