equal
deleted
inserted
replaced
356 apply (erule stream_finite_lemma2, simp) |
356 apply (erule stream_finite_lemma2, simp) |
357 apply (simp add: slen_def, auto) |
357 apply (simp add: slen_def, auto) |
358 by (drule stream_finite_lemma1,auto) |
358 by (drule stream_finite_lemma1,auto) |
359 |
359 |
360 lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \<bottom>)" |
360 lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \<bottom>)" |
361 by (rule stream.casedist [of x], auto simp del: iSuc_Fin |
361 by (rule stream.casedist [of x], auto simp add: Fin_0 iSuc_Fin[THEN sym]) |
362 simp add: Fin_0 iSuc_Fin[THEN sym] i0_iless_iSuc iSuc_mono) |
|
363 |
362 |
364 lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)" |
363 lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)" |
365 by (rule stream.casedist [of x], auto) |
364 by (rule stream.casedist [of x], auto) |
366 |
365 |
367 lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y & a ~= \<bottom> & Fin n < #y)" |
366 lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y & a ~= \<bottom> & Fin n < #y)" |