src/HOLCF/ex/Stream.thy
changeset 35524 a2a59e92b02e
parent 35497 979706bd5c16
child 35557 5da670d57118
equal deleted inserted replaced
35523:cc57f4a274a3 35524:a2a59e92b02e
   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 n" in exI)
   293 apply (rule_tac x="Suc i" 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="n" in exI)
   298 apply (rule_tac x="i" 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)