added exercise
Fri, 08 Nov 2013 08:59:54 +0100
changeset 54290 fee1276d47f7
parent 54289 5a1be63f32cf
child 54291 709a2bbd7638
added exercise
--- 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 @@
+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"}.
 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$.