100 |
100 |
101 lemma stream_flat_prefix: |
101 lemma stream_flat_prefix: |
102 "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys" |
102 "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys" |
103 apply (case_tac "y=UU",auto) |
103 apply (case_tac "y=UU",auto) |
104 apply (auto simp add: stream.inverts) |
104 apply (auto simp add: stream.inverts) |
105 by (drule ax_flat [rule_format],simp) |
105 by (drule ax_flat,simp) |
106 |
106 |
107 |
107 |
108 |
108 |
109 |
109 |
110 (* ----------------------------------------------------------------------- *) |
110 (* ----------------------------------------------------------------------- *) |
488 apply (simp add: Suc_ile_eq) |
488 apply (simp add: Suc_ile_eq) |
489 apply (case_tac "y=UU", clarsimp) |
489 apply (case_tac "y=UU", clarsimp) |
490 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+ |
490 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+ |
491 apply (erule_tac x="ya" in allE, simp) |
491 apply (erule_tac x="ya" in allE, simp) |
492 apply (auto simp add: stream.inverts) |
492 apply (auto simp add: stream.inverts) |
493 by (drule ax_flat [rule_format], simp) |
493 by (drule ax_flat, simp) |
494 |
494 |
495 lemma slen_strict_mono_lemma: |
495 lemma slen_strict_mono_lemma: |
496 "stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t" |
496 "stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t" |
497 apply (erule stream_finite_ind, auto) |
497 apply (erule stream_finite_ind, auto) |
498 apply (case_tac "sa=UU", auto) |
498 apply (case_tac "sa=UU", auto) |
499 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
499 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
500 apply (simp add: stream.inverts, clarsimp) |
500 apply (simp add: stream.inverts, clarsimp) |
501 by (drule ax_flat [rule_format], simp) |
501 by (drule ax_flat, simp) |
502 |
502 |
503 lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t" |
503 lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t" |
504 apply (intro ilessI1, auto) |
504 apply (intro ilessI1, auto) |
505 apply (simp add: slen_mono) |
505 apply (simp add: slen_mono) |
506 by (drule slen_strict_mono_lemma, auto) |
506 by (drule slen_strict_mono_lemma, auto) |