equal
deleted
inserted
replaced
206 |
206 |
207 lemma fsmap_fsingleton[simp]: "fsmap f$(<x>) = <(f x)>" |
207 lemma fsmap_fsingleton[simp]: "fsmap f$(<x>) = <(f x)>" |
208 by (simp add: fsmap_def fsingleton_def2 flift2_def) |
208 by (simp add: fsmap_def fsingleton_def2 flift2_def) |
209 |
209 |
210 |
210 |
211 declare range_composition[simp del] |
|
212 |
|
213 |
|
214 lemma fstreams_chain_lemma[rule_format]: |
211 lemma fstreams_chain_lemma[rule_format]: |
215 "ALL s x y. stream_take n$(s::'a fstream) << x & x << y & y << s & x ~= y --> stream_take (Suc n)$s << y" |
212 "ALL s x y. stream_take n$(s::'a fstream) << x & x << y & y << s & x ~= y --> stream_take (Suc n)$s << y" |
216 apply (induct_tac n, auto) |
213 apply (induct_tac n, auto) |
217 apply (case_tac "s=UU", auto) |
214 apply (case_tac "s=UU", auto) |
218 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
215 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
223 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
220 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
224 apply (erule_tac x="ya" in allE) |
221 apply (erule_tac x="ya" in allE) |
225 apply (drule stream_prefix, auto) |
222 apply (drule stream_prefix, auto) |
226 apply (case_tac "y=UU",auto) |
223 apply (case_tac "y=UU",auto) |
227 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
224 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
228 apply (auto simp add: stream.inverts) |
225 apply auto |
229 apply (simp add: flat_less_iff) |
226 apply (simp add: flat_less_iff) |
230 apply (erule_tac x="tt" in allE) |
227 apply (erule_tac x="tt" in allE) |
231 apply (erule_tac x="yb" in allE, auto) |
228 apply (erule_tac x="yb" in allE, auto) |
232 apply (simp add: flat_less_iff) |
229 apply (simp add: flat_less_iff) |
233 by (simp add: flat_less_iff) |
230 by (simp add: flat_less_iff) |