# HG changeset patch
# User nipkow
# Date 1383943207 -3600
# Node ID ce4a17b2e3739aa9a0a5e387f431e302f83028ec
# Parent  709a2bbd7638ab5fdc6a80be85247114923d01d1
more exercises

diff -r 709a2bbd7638 -r ce4a17b2e373 src/Doc/ProgProve/Isar.thy
--- 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}
diff -r 709a2bbd7638 -r ce4a17b2e373 src/Doc/ProgProve/Logic.thy
--- 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