equal
deleted
inserted
replaced
843 apply (erule_tac x="na" in allE) |
843 apply (erule_tac x="na" in allE) |
844 apply (insert i_th_last_eq [of _ s1 s2]) |
844 apply (insert i_th_last_eq [of _ s1 s2]) |
845 by blast+ |
845 by blast+ |
846 |
846 |
847 lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2" |
847 lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2" |
848 by (insert i_th_stream_take_eq [THEN stream.take_lemmas],blast) |
848 by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast) |
849 |
849 |
850 (* ----------------------------------------------------------------------- *) |
850 (* ----------------------------------------------------------------------- *) |
851 subsection "finiteness" |
851 subsection "finiteness" |
852 (* ----------------------------------------------------------------------- *) |
852 (* ----------------------------------------------------------------------- *) |
853 |
853 |
910 apply (drule ex_sconc) |
910 apply (drule ex_sconc) |
911 apply (simp,clarsimp,drule streams_prefix_lemma1) |
911 apply (simp,clarsimp,drule streams_prefix_lemma1) |
912 apply (simp+,rule slen_take_lemma3 [of _ s1 s2]) |
912 apply (simp+,rule slen_take_lemma3 [of _ s1 s2]) |
913 apply (simp+,rule_tac x="UU" in exI) |
913 apply (simp+,rule_tac x="UU" in exI) |
914 apply (insert slen_take_lemma3 [of _ s1 s2]) |
914 apply (insert slen_take_lemma3 [of _ s1 s2]) |
915 by (rule stream.take_lemmas,simp) |
915 by (rule stream.take_lemma,simp) |
916 |
916 |
917 (* ----------------------------------------------------------------------- *) |
917 (* ----------------------------------------------------------------------- *) |
918 subsection "continuity" |
918 subsection "continuity" |
919 (* ----------------------------------------------------------------------- *) |
919 (* ----------------------------------------------------------------------- *) |
920 |
920 |