--- a/src/Doc/ProgProve/Isar.thy Fri Nov 08 19:03:14 2013 +0100
+++ b/src/Doc/ProgProve/Isar.thy Fri Nov 08 21:40:07 2013 +0100
@@ -1081,8 +1081,7 @@
\exercise
-Give a structured proof of @{prop "ev(Suc(Suc n)) \<Longrightarrow> ev n"}
-by rule inversion:
+Give a structured proof by rule inversion:
*}
lemma assumes a: "ev(Suc(Suc n))" shows "ev n"
@@ -1098,6 +1097,13 @@
\end{exercise}
\begin{exercise}
+Recall predicate @{text star} from \autoref{sec:star} and @{text iter}
+from Exercise~\ref{exe:iter}. Prove @{prop "iter r n x y \<Longrightarrow> star r x y"}
+in a structured style, do not just sledgehammer each case of the
+required induction.
+\end{exercise}
+
+\begin{exercise}
Define a recursive function @{text "elems ::"} @{typ"'a list \<Rightarrow> 'a set"}
and prove @{prop "x : elems xs \<Longrightarrow> \<exists>ys zs. xs = ys @ x # zs \<and> x \<notin> elems ys"}.
\end{exercise}
--- a/src/Doc/ProgProve/Logic.thy Fri Nov 08 19:03:14 2013 +0100
+++ b/src/Doc/ProgProve/Logic.thy Fri Nov 08 21:40:07 2013 +0100
@@ -816,7 +816,7 @@
if the assumption about the inductive predicate is not the first assumption.
\endexercise
-\begin{exercise}
+\begin{exercise}\label{exe:iter}
Analogous to @{const star}, give an inductive definition of the @{text n}-fold iteration
of a relation @{text r}: @{term "iter r n x y"} should hold if there are @{text x\<^sub>0}, \dots, @{text x\<^sub>n}
such that @{prop"x = x\<^sub>0"}, @{prop"x\<^sub>n = y"} and @{text"r x\<^bsub>i\<^esub> x\<^bsub>i+1\<^esub>"} for