doc-src/TutorialI/CTL/CTL.thy
 changeset 13552 83d674e8cd2a parent 12815 1f073030b97a child 15102 04b0e943fcc9
equal inserted replaced
13551:b7f64ee8da84 13552:83d674e8cd2a
`   279 @{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}`
`   279 @{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"}`
`   280 is extensionally equal to @{term"path s Q"},`
`   280 is extensionally equal to @{term"path s Q"},`
`   281 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}.`
`   281 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}.`
`   282 *};`
`   282 *};`
`   283 (*<*)`
`   283 (*<*)`
`   284 lemma infinity_lemma:`
`   284 lemma`
`   285 "\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow>`
`   285 "\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow>`
`   286  \<exists> p\<in>Paths s. \<forall> i. Q(p i)";`
`   286  \<exists> p\<in>Paths s. \<forall> i. Q(p i)";`
`   287 apply(subgoal_tac`
`   287 apply(subgoal_tac`
`   288  "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");`
`   288  "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))");`
`   289  apply(simp add: Paths_def);`
`   289  apply(simp add: Paths_def);`