256 Function @{const path} has fulfilled its purpose now and can be forgotten. |
256 Function @{const path} has fulfilled its purpose now and can be forgotten. |
257 It was merely defined to provide the witness in the proof of the |
257 It was merely defined to provide the witness in the proof of the |
258 @{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know |
258 @{thm[source]infinity_lemma}. Aficionados of minimal proofs might like to know |
259 that we could have given the witness without having to define a new function: |
259 that we could have given the witness without having to define a new function: |
260 the term |
260 the term |
261 @{term[display]"nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"} |
261 @{term[display]"rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)"} |
262 is extensionally equal to @{term"path s Q"}, |
262 is extensionally equal to @{term"path s Q"}, |
263 where @{term nat_rec} is the predefined primitive recursor on @{typ nat}. |
263 where @{term rec_nat} is the predefined primitive recursor on @{typ nat}. |
264 *}; |
264 *}; |
265 (*<*) |
265 (*<*) |
266 lemma |
266 lemma |
267 "\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow> |
267 "\<lbrakk> Q s; \<forall> s. Q s \<longrightarrow> (\<exists> t. (s,t)\<in>M \<and> Q t) \<rbrakk> \<Longrightarrow> |
268 \<exists> p\<in>Paths s. \<forall> i. Q(p i)"; |
268 \<exists> p\<in>Paths s. \<forall> i. Q(p i)"; |
269 apply(subgoal_tac |
269 apply(subgoal_tac |
270 "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))"); |
270 "\<exists> p. s = p 0 \<and> (\<forall> i. (p i,p(Suc i))\<in>M \<and> Q(p i))"); |
271 apply(simp add: Paths_def); |
271 apply(simp add: Paths_def); |
272 apply(blast); |
272 apply(blast); |
273 apply(rule_tac x = "nat_rec s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI); |
273 apply(rule_tac x = "rec_nat s (\<lambda>n t. SOME u. (t,u)\<in>M \<and> Q u)" in exI); |
274 apply(simp); |
274 apply(simp); |
275 apply(intro strip); |
275 apply(intro strip); |
276 apply(induct_tac i); |
276 apply(induct_tac i); |
277 apply(simp); |
277 apply(simp); |
278 apply(fast intro: someI2_ex); |
278 apply(fast intro: someI2_ex); |