src/Doc/ProgProve/Logic.thy
 changeset 54290 fee1276d47f7 parent 54231 2975658d49cd child 54292 ce4a17b2e373
equal inserted replaced
54289:5a1be63f32cf 54290:fee1276d47f7
   815 Note that rule induction fails
   815 Note that rule induction fails
   816 if the assumption about the inductive predicate is not the first assumption.
   816 if the assumption about the inductive predicate is not the first assumption.
   817 \endexercise
   817 \endexercise
   818
   818
   819 \begin{exercise}
   819 \begin{exercise}

   820 Analogous to @{const star}, give an inductive definition of the @{text n}-fold iteration

   821 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}

   822 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

   823 all @{prop"i < n"}. Correct and prove the following claim:

   824 @{prop"star r x y \<Longrightarrow> iter r n x y"}.

   825 \end{exercise}

   826

   827 \begin{exercise}
   820 A context-free grammar can be seen as an inductive definition where each
   828 A context-free grammar can be seen as an inductive definition where each
   821 nonterminal $A$ is an inductively defined predicate on lists of terminal
   829 nonterminal $A$ is an inductively defined predicate on lists of terminal
   822 symbols: $A(w)$ mans that $w$ is in the language generated by $A$.
   830 symbols: $A(w)$ mans that $w$ is in the language generated by $A$.
   823 For example, the production $S \to a S b$ can be viewed as the implication
   831 For example, the production $S \to a S b$ can be viewed as the implication
   824 @{prop"S w \<Longrightarrow> S (a # w @ [b])"} where @{text a} and @{text b} are terminal symbols,
   832 @{prop"S w \<Longrightarrow> S (a # w @ [b])"} where @{text a} and @{text b} are terminal symbols,