288 lemma stream_finite_UU_rev: "~ stream_finite s ==> s ~= UU" |
288 lemma stream_finite_UU_rev: "~ stream_finite s ==> s ~= UU" |
289 by (auto simp add: stream.finite_def) |
289 by (auto simp add: stream.finite_def) |
290 |
290 |
291 lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)" |
291 lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)" |
292 apply (simp add: stream.finite_def,auto) |
292 apply (simp add: stream.finite_def,auto) |
293 apply (rule_tac x="Suc i" in exI) |
293 apply (rule_tac x="Suc n" in exI) |
294 by (simp add: stream_take_lemma4) |
294 by (simp add: stream_take_lemma4) |
295 |
295 |
296 lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" |
296 lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" |
297 apply (simp add: stream.finite_def, auto) |
297 apply (simp add: stream.finite_def, auto) |
298 apply (rule_tac x="i" in exI) |
298 apply (rule_tac x="n" in exI) |
299 by (erule stream_take_lemma3,simp) |
299 by (erule stream_take_lemma3,simp) |
300 |
300 |
301 lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s" |
301 lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s" |
302 apply (rule stream.casedist [of s], auto) |
302 apply (rule stream.casedist [of s], auto) |
303 apply (rule stream_finite_lemma1, simp) |
303 apply (rule stream_finite_lemma1, simp) |