equal
deleted
inserted
replaced
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); |