src/Doc/ProgProve/Logic.thy

 Note that rule induction fails
 if the assumption about the inductive predicate is not the first assumption.
 \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$.
 For example, the production $S \to a S b$ can be viewed as the implication
 @{prop"S w \<Longrightarrow> S (a # w @ [b])"} where @{text a} and @{text b} are terminal symbols,