src/Doc/ProgProve/Logic.thy
changeset 54290 fee1276d47f7
parent 54231 2975658d49cd
child 54292 ce4a17b2e373
equal deleted 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,