52 "constr_sconc s1 s2 = (case #s1 of |
52 "constr_sconc s1 s2 = (case #s1 of |
53 Fin n \<Rightarrow> constr_sconc' n s1 s2 |
53 Fin n \<Rightarrow> constr_sconc' n s1 s2 |
54 | \<infinity> \<Rightarrow> s1)" |
54 | \<infinity> \<Rightarrow> s1)" |
55 |
55 |
56 |
56 |
57 declare stream.rews [simp add] |
|
58 |
|
59 (* ----------------------------------------------------------------------- *) |
57 (* ----------------------------------------------------------------------- *) |
60 (* theorems about scons *) |
58 (* theorems about scons *) |
61 (* ----------------------------------------------------------------------- *) |
59 (* ----------------------------------------------------------------------- *) |
62 |
60 |
63 |
61 |
147 |
145 |
148 lemma stream_reach2: "(LUB i. stream_take i$s) = s" |
146 lemma stream_reach2: "(LUB i. stream_take i$s) = s" |
149 apply (insert stream.reach [of s], erule subst) back |
147 apply (insert stream.reach [of s], erule subst) back |
150 apply (simp add: fix_def2 stream.take_def) |
148 apply (simp add: fix_def2 stream.take_def) |
151 apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym]) |
149 apply (insert contlub_cfun_fun [of "%i. iterate i$stream_copy$UU" s,THEN sym]) |
152 by (simp add: chain_iterate) |
150 by simp |
153 |
151 |
154 lemma chain_stream_take: "chain (%i. stream_take i$s)" |
152 lemma chain_stream_take: "chain (%i. stream_take i$s)" |
155 apply (rule chainI) |
153 apply (rule chainI) |
156 apply (rule monofun_cfun_fun) |
154 apply (rule monofun_cfun_fun) |
157 apply (simp add: stream.take_def del: iterate_Suc) |
155 apply (simp add: stream.take_def del: iterate_Suc) |
158 by (rule chainE, simp add: chain_iterate) |
156 by (rule chainE, simp) |
159 |
157 |
160 lemma stream_take_prefix [simp]: "stream_take n$s << s" |
158 lemma stream_take_prefix [simp]: "stream_take n$s << s" |
161 apply (insert stream_reach2 [of s]) |
159 apply (insert stream_reach2 [of s]) |
162 apply (erule subst) back |
160 apply (erule subst) back |
163 apply (rule is_ub_thelub) |
161 apply (rule is_ub_thelub) |