# HG changeset patch
# User nipkow
# Date 1383897594 -3600
# Node ID fee1276d47f701d787821ad30d2277c94e6b92b7
# Parent  5a1be63f32cf5706ffb0d3d4d3b0f3e3cf7f8977
added exercise

diff -r 5a1be63f32cf -r fee1276d47f7 src/Doc/ProgProve/Logic.thy
--- a/src/Doc/ProgProve/Logic.thy	Thu Nov 07 16:08:19 2013 +1100
+++ b/src/Doc/ProgProve/Logic.thy	Fri Nov 08 08:59:54 2013 +0100
@@ -817,6 +817,14 @@
 \endexercise
 
 \begin{exercise}
+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
+all @{prop"i < n"}. Correct and prove the following claim:
+@{prop"star r x y \<Longrightarrow> iter r n x y"}.
+\end{exercise}
+
+\begin{exercise}
 A context-free grammar can be seen as an inductive definition where each
 nonterminal $A$ is an inductively defined predicate on lists of terminal
 symbols: $A(w)$ mans that $w$ is in the language generated by $A$.