27 |
27 |
28 |
28 |
29 (* concatenation *) |
29 (* concatenation *) |
30 |
30 |
31 definition |
31 definition |
32 i_rt :: "nat => 'a stream => 'a stream" where (* chops the first i elements *) |
32 i_rt :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where (* chops the first i elements *) |
33 "i_rt = (%i s. iterate i$rt$s)" |
33 "i_rt = (\<lambda>i s. iterate i\<cdot>rt\<cdot>s)" |
34 |
34 |
35 definition |
35 definition |
36 i_th :: "nat => 'a stream => 'a" where (* the i-th element *) |
36 i_th :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a" where (* the i-th element *) |
37 "i_th = (%i s. ft$(i_rt i s))" |
37 "i_th = (\<lambda>i s. ft\<cdot>(i_rt i s))" |
38 |
38 |
39 definition |
39 definition |
40 sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) where |
40 sconc :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "ooo" 65) where |
41 "s1 ooo s2 = (case #s1 of |
41 "s1 ooo s2 = (case #s1 of |
42 enat n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) |
42 enat n \<Rightarrow> (SOME s. (stream_take n\<cdot>s = s1) \<and> (i_rt n s = s2)) |
43 | \<infinity> \<Rightarrow> s1)" |
43 | \<infinity> \<Rightarrow> s1)" |
44 |
44 |
45 primrec constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" |
45 primrec constr_sconc' :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" |
46 where |
46 where |
47 constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2" |
47 constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2" |
48 | constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 && |
48 | constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft\<cdot>s1 && constr_sconc' n (rt\<cdot>s1) s2" |
49 constr_sconc' n (rt$s1) s2" |
|
50 |
49 |
51 definition |
50 definition |
52 constr_sconc :: "'a stream => 'a stream => 'a stream" where (* constructive *) |
51 constr_sconc :: "'a stream \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where (* constructive *) |
53 "constr_sconc s1 s2 = (case #s1 of |
52 "constr_sconc s1 s2 = (case #s1 of |
54 enat n \<Rightarrow> constr_sconc' n s1 s2 |
53 enat n \<Rightarrow> constr_sconc' n s1 s2 |
55 | \<infinity> \<Rightarrow> s1)" |
54 | \<infinity> \<Rightarrow> s1)" |
56 |
55 |
57 |
56 |
63 section "scons" |
62 section "scons" |
64 |
63 |
65 lemma scons_eq_UU: "(a && s = UU) = (a = UU)" |
64 lemma scons_eq_UU: "(a && s = UU) = (a = UU)" |
66 by simp |
65 by simp |
67 |
66 |
68 lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R" |
67 lemma scons_not_empty: "\<lbrakk>a && x = UU; a \<noteq> UU\<rbrakk> \<Longrightarrow> R" |
69 by simp |
68 by simp |
70 |
69 |
71 lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU & x = a && y)" |
70 lemma stream_exhaust_eq: "x \<noteq> UU \<longleftrightarrow> (\<exists>a y. a \<noteq> UU \<and> x = a && y)" |
72 by (cases x, auto) |
71 by (cases x, auto) |
73 |
72 |
74 lemma stream_neq_UU: "x~=UU ==> EX a a_s. x=a&&a_s & a~=UU" |
73 lemma stream_neq_UU: "x \<noteq> UU \<Longrightarrow> \<exists>a a_s. x = a && a_s \<and> a \<noteq> UU" |
75 by (simp add: stream_exhaust_eq,auto) |
74 by (simp add: stream_exhaust_eq,auto) |
76 |
75 |
77 lemma stream_prefix: |
76 lemma stream_prefix: |
78 "[| a && s << t; a ~= UU |] ==> EX b tt. t = b && tt & b ~= UU & s << tt" |
77 "\<lbrakk>a && s \<sqsubseteq> t; a \<noteq> UU\<rbrakk> \<Longrightarrow> \<exists>b tt. t = b && tt \<and> b \<noteq> UU \<and> s \<sqsubseteq> tt" |
79 by (cases t, auto) |
78 by (cases t, auto) |
80 |
79 |
81 lemma stream_prefix': |
80 lemma stream_prefix': |
82 "b ~= UU ==> x << b && z = |
81 "b \<noteq> UU \<Longrightarrow> x \<sqsubseteq> b && z = |
83 (x = UU | (EX a y. x = a && y & a ~= UU & a << b & y << z))" |
82 (x = UU \<or> (\<exists>a y. x = a && y \<and> a \<noteq> UU \<and> a \<sqsubseteq> b \<and> y \<sqsubseteq> z))" |
84 by (cases x, auto) |
83 by (cases x, auto) |
85 |
84 |
86 |
85 |
87 (* |
86 (* |
88 lemma stream_prefix1: "[| x<<y; xs<<ys |] ==> x&&xs << y&&ys" |
87 lemma stream_prefix1: "\<lbrakk>x \<sqsubseteq> y; xs \<sqsubseteq> ys\<rbrakk> \<Longrightarrow> x && xs \<sqsubseteq> y && ys" |
89 by (insert stream_prefix' [of y "x&&xs" ys],force) |
88 by (insert stream_prefix' [of y "x && xs" ys],force) |
90 *) |
89 *) |
91 |
90 |
92 lemma stream_flat_prefix: |
91 lemma stream_flat_prefix: |
93 "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys" |
92 "\<lbrakk>x && xs \<sqsubseteq> y && ys; (x::'a::flat) \<noteq> UU\<rbrakk> \<Longrightarrow> x = y \<and> xs \<sqsubseteq> ys" |
94 apply (case_tac "y=UU",auto) |
93 apply (case_tac "y = UU",auto) |
95 apply (drule ax_flat,simp) |
94 apply (drule ax_flat,simp) |
96 done |
95 done |
97 |
96 |
98 |
97 |
99 |
98 |
138 |
137 |
139 |
138 |
140 section "stream_take" |
139 section "stream_take" |
141 |
140 |
142 |
141 |
143 lemma stream_reach2: "(LUB i. stream_take i$s) = s" |
142 lemma stream_reach2: "(LUB i. stream_take i\<cdot>s) = s" |
144 by (rule stream.reach) |
143 by (rule stream.reach) |
145 |
144 |
146 lemma chain_stream_take: "chain (%i. stream_take i$s)" |
145 lemma chain_stream_take: "chain (\<lambda>i. stream_take i\<cdot>s)" |
147 by simp |
146 by simp |
148 |
147 |
149 lemma stream_take_prefix [simp]: "stream_take n$s << s" |
148 lemma stream_take_prefix [simp]: "stream_take n\<cdot>s \<sqsubseteq> s" |
150 apply (insert stream_reach2 [of s]) |
149 apply (insert stream_reach2 [of s]) |
151 apply (erule subst) back |
150 apply (erule subst) back |
152 apply (rule is_ub_thelub) |
151 apply (rule is_ub_thelub) |
153 apply (simp only: chain_stream_take) |
152 apply (simp only: chain_stream_take) |
154 done |
153 done |
155 |
154 |
156 lemma stream_take_more [rule_format]: |
155 lemma stream_take_more [rule_format]: |
157 "ALL x. stream_take n$x = x --> stream_take (Suc n)$x = x" |
156 "\<forall>x. stream_take n\<cdot>x = x \<longrightarrow> stream_take (Suc n)\<cdot>x = x" |
158 apply (induct_tac n,auto) |
157 apply (induct_tac n,auto) |
159 apply (case_tac "x=UU",auto) |
158 apply (case_tac "x=UU",auto) |
160 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
159 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
161 done |
160 done |
162 |
161 |
163 lemma stream_take_lemma3 [rule_format]: |
162 lemma stream_take_lemma3 [rule_format]: |
164 "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs" |
163 "\<forall>x xs. x \<noteq> UU \<longrightarrow> stream_take n\<cdot>(x && xs) = x && xs \<longrightarrow> stream_take n\<cdot>xs = xs" |
165 apply (induct_tac n,clarsimp) |
164 apply (induct_tac n,clarsimp) |
166 (*apply (drule sym, erule scons_not_empty, simp)*) |
165 (*apply (drule sym, erule scons_not_empty, simp)*) |
167 apply (clarify, rule stream_take_more) |
166 apply (clarify, rule stream_take_more) |
168 apply (erule_tac x="x" in allE) |
167 apply (erule_tac x="x" in allE) |
169 apply (erule_tac x="xs" in allE,simp) |
168 apply (erule_tac x="xs" in allE,simp) |
170 done |
169 done |
171 |
170 |
172 lemma stream_take_lemma4: |
171 lemma stream_take_lemma4: |
173 "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs" |
172 "\<forall>x xs. stream_take n\<cdot>xs = xs \<longrightarrow> stream_take (Suc n)\<cdot>(x && xs) = x && xs" |
174 by auto |
173 by auto |
175 |
174 |
176 lemma stream_take_idempotent [rule_format, simp]: |
175 lemma stream_take_idempotent [rule_format, simp]: |
177 "ALL s. stream_take n$(stream_take n$s) = stream_take n$s" |
176 "\<forall>s. stream_take n\<cdot>(stream_take n\<cdot>s) = stream_take n\<cdot>s" |
178 apply (induct_tac n, auto) |
177 apply (induct_tac n, auto) |
179 apply (case_tac "s=UU", auto) |
178 apply (case_tac "s=UU", auto) |
180 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
179 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
181 done |
180 done |
182 |
181 |
183 lemma stream_take_take_Suc [rule_format, simp]: |
182 lemma stream_take_take_Suc [rule_format, simp]: |
184 "ALL s. stream_take n$(stream_take (Suc n)$s) = |
183 "\<forall>s. stream_take n\<cdot>(stream_take (Suc n)\<cdot>s) = stream_take n\<cdot>s" |
185 stream_take n$s" |
|
186 apply (induct_tac n, auto) |
184 apply (induct_tac n, auto) |
187 apply (case_tac "s=UU", auto) |
185 apply (case_tac "s=UU", auto) |
188 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
186 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
189 done |
187 done |
190 |
188 |
191 lemma mono_stream_take_pred: |
189 lemma mono_stream_take_pred: |
192 "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> |
190 "stream_take (Suc n)\<cdot>s1 \<sqsubseteq> stream_take (Suc n)\<cdot>s2 \<Longrightarrow> |
193 stream_take n$s1 << stream_take n$s2" |
191 stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2" |
194 by (insert monofun_cfun_arg [of "stream_take (Suc n)$s1" |
192 by (insert monofun_cfun_arg [of "stream_take (Suc n)\<cdot>s1" |
195 "stream_take (Suc n)$s2" "stream_take n"], auto) |
193 "stream_take (Suc n)\<cdot>s2" "stream_take n"], auto) |
196 (* |
194 (* |
197 lemma mono_stream_take_pred: |
195 lemma mono_stream_take_pred: |
198 "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> |
196 "stream_take (Suc n)\<cdot>s1 \<sqsubseteq> stream_take (Suc n)\<cdot>s2 \<Longrightarrow> |
199 stream_take n$s1 << stream_take n$s2" |
197 stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2" |
200 by (drule mono_stream_take [of _ _ n],simp) |
198 by (drule mono_stream_take [of _ _ n],simp) |
201 *) |
199 *) |
202 |
200 |
203 lemma stream_take_lemma10 [rule_format]: |
201 lemma stream_take_lemma10 [rule_format]: |
204 "ALL k<=n. stream_take n$s1 << stream_take n$s2 |
202 "\<forall>k\<le>n. stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2 \<longrightarrow> stream_take k\<cdot>s1 \<sqsubseteq> stream_take k\<cdot>s2" |
205 --> stream_take k$s1 << stream_take k$s2" |
|
206 apply (induct_tac n,simp,clarsimp) |
203 apply (induct_tac n,simp,clarsimp) |
207 apply (case_tac "k=Suc n",blast) |
204 apply (case_tac "k=Suc n",blast) |
208 apply (erule_tac x="k" in allE) |
205 apply (erule_tac x="k" in allE) |
209 apply (drule mono_stream_take_pred,simp) |
206 apply (drule mono_stream_take_pred,simp) |
210 done |
207 done |
211 |
208 |
212 lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1" |
209 lemma stream_take_le_mono : "k \<le> n \<Longrightarrow> stream_take k\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s1" |
213 apply (insert chain_stream_take [of s1]) |
210 apply (insert chain_stream_take [of s1]) |
214 apply (drule chain_mono,auto) |
211 apply (drule chain_mono,auto) |
215 done |
212 done |
216 |
213 |
217 lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2" |
214 lemma mono_stream_take: "s1 \<sqsubseteq> s2 \<Longrightarrow> stream_take n\<cdot>s1 \<sqsubseteq> stream_take n\<cdot>s2" |
218 by (simp add: monofun_cfun_arg) |
215 by (simp add: monofun_cfun_arg) |
219 |
216 |
220 (* |
217 (* |
221 lemma stream_take_prefix [simp]: "stream_take n$s << s" |
218 lemma stream_take_prefix [simp]: "stream_take n\<cdot>s \<sqsubseteq> s" |
222 apply (subgoal_tac "s=(LUB n. stream_take n$s)") |
219 apply (subgoal_tac "s=(LUB n. stream_take n\<cdot>s)") |
223 apply (erule ssubst, rule is_ub_thelub) |
220 apply (erule ssubst, rule is_ub_thelub) |
224 apply (simp only: chain_stream_take) |
221 apply (simp only: chain_stream_take) |
225 by (simp only: stream_reach2) |
222 by (simp only: stream_reach2) |
226 *) |
223 *) |
227 |
224 |
228 lemma stream_take_take_less:"stream_take k$(stream_take n$s) << stream_take k$s" |
225 lemma stream_take_take_less:"stream_take k\<cdot>(stream_take n\<cdot>s) \<sqsubseteq> stream_take k\<cdot>s" |
229 by (rule monofun_cfun_arg,auto) |
226 by (rule monofun_cfun_arg,auto) |
230 |
227 |
231 |
228 |
232 (* ------------------------------------------------------------------------- *) |
229 (* ------------------------------------------------------------------------- *) |
233 (* special induction rules *) |
230 (* special induction rules *) |
235 |
232 |
236 |
233 |
237 section "induction" |
234 section "induction" |
238 |
235 |
239 lemma stream_finite_ind: |
236 lemma stream_finite_ind: |
240 "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x" |
237 "\<lbrakk>stream_finite x; P UU; \<And>a s. \<lbrakk>a \<noteq> UU; P s\<rbrakk> \<Longrightarrow> P (a && s)\<rbrakk> \<Longrightarrow> P x" |
241 apply (simp add: stream.finite_def,auto) |
238 apply (simp add: stream.finite_def,auto) |
242 apply (erule subst) |
239 apply (erule subst) |
243 apply (drule stream.finite_induct [of P _ x], auto) |
240 apply (drule stream.finite_induct [of P _ x], auto) |
244 done |
241 done |
245 |
242 |
246 lemma stream_finite_ind2: |
243 lemma stream_finite_ind2: |
247 "[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==> |
244 "\<lbrakk>P UU; \<And>x. x \<noteq> UU \<Longrightarrow> P (x && UU); \<And>y z s. \<lbrakk>y \<noteq> UU; z \<noteq> UU; P s\<rbrakk> \<Longrightarrow> P (y && z && s)\<rbrakk> \<Longrightarrow> |
248 !s. P (stream_take n$s)" |
245 \<forall>s. P (stream_take n\<cdot>s)" |
249 apply (rule nat_less_induct [of _ n],auto) |
246 apply (rule nat_less_induct [of _ n],auto) |
250 apply (case_tac n, auto) |
247 apply (case_tac n, auto) |
251 apply (case_tac nat, auto) |
248 apply (case_tac nat, auto) |
252 apply (case_tac "s=UU",clarsimp) |
249 apply (case_tac "s=UU",clarsimp) |
253 apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) |
250 apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) |
291 section "stream_finite" |
288 section "stream_finite" |
292 |
289 |
293 lemma stream_finite_UU [simp]: "stream_finite UU" |
290 lemma stream_finite_UU [simp]: "stream_finite UU" |
294 by (simp add: stream.finite_def) |
291 by (simp add: stream.finite_def) |
295 |
292 |
296 lemma stream_finite_UU_rev: "~ stream_finite s ==> s ~= UU" |
293 lemma stream_finite_UU_rev: "\<not> stream_finite s \<Longrightarrow> s \<noteq> UU" |
297 by (auto simp add: stream.finite_def) |
294 by (auto simp add: stream.finite_def) |
298 |
295 |
299 lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)" |
296 lemma stream_finite_lemma1: "stream_finite xs \<Longrightarrow> stream_finite (x && xs)" |
300 apply (simp add: stream.finite_def,auto) |
297 apply (simp add: stream.finite_def,auto) |
301 apply (rule_tac x="Suc n" in exI) |
298 apply (rule_tac x="Suc n" in exI) |
302 apply (simp add: stream_take_lemma4) |
299 apply (simp add: stream_take_lemma4) |
303 done |
300 done |
304 |
301 |
305 lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" |
302 lemma stream_finite_lemma2: "\<lbrakk>x \<noteq> UU; stream_finite (x && xs)\<rbrakk> \<Longrightarrow> stream_finite xs" |
306 apply (simp add: stream.finite_def, auto) |
303 apply (simp add: stream.finite_def, auto) |
307 apply (rule_tac x="n" in exI) |
304 apply (rule_tac x="n" in exI) |
308 apply (erule stream_take_lemma3,simp) |
305 apply (erule stream_take_lemma3,simp) |
309 done |
306 done |
310 |
307 |
311 lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s" |
308 lemma stream_finite_rt_eq: "stream_finite (rt\<cdot>s) = stream_finite s" |
312 apply (cases s, auto) |
309 apply (cases s, auto) |
313 apply (rule stream_finite_lemma1, simp) |
310 apply (rule stream_finite_lemma1, simp) |
314 apply (rule stream_finite_lemma2,simp) |
311 apply (rule stream_finite_lemma2,simp) |
315 apply assumption |
312 apply assumption |
316 done |
313 done |
317 |
314 |
318 lemma stream_finite_less: "stream_finite s ==> !t. t<<s --> stream_finite t" |
315 lemma stream_finite_less: "stream_finite s \<Longrightarrow> \<forall>t. t \<sqsubseteq> s \<longrightarrow> stream_finite t" |
319 apply (erule stream_finite_ind [of s], auto) |
316 apply (erule stream_finite_ind [of s], auto) |
320 apply (case_tac "t=UU", auto) |
317 apply (case_tac "t=UU", auto) |
321 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
318 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
322 apply (erule_tac x="y" in allE, simp) |
319 apply (erule_tac x="y" in allE, simp) |
323 apply (rule stream_finite_lemma1, simp) |
320 apply (rule stream_finite_lemma1, simp) |
324 done |
321 done |
325 |
322 |
326 lemma stream_take_finite [simp]: "stream_finite (stream_take n$s)" |
323 lemma stream_take_finite [simp]: "stream_finite (stream_take n\<cdot>s)" |
327 apply (simp add: stream.finite_def) |
324 apply (simp add: stream.finite_def) |
328 apply (rule_tac x="n" in exI,simp) |
325 apply (rule_tac x="n" in exI,simp) |
329 done |
326 done |
330 |
327 |
331 lemma adm_not_stream_finite: "adm (%x. ~ stream_finite x)" |
328 lemma adm_not_stream_finite: "adm (\<lambda>x. \<not> stream_finite x)" |
332 apply (rule adm_upward) |
329 apply (rule adm_upward) |
333 apply (erule contrapos_nn) |
330 apply (erule contrapos_nn) |
334 apply (erule (1) stream_finite_less [rule_format]) |
331 apply (erule (1) stream_finite_less [rule_format]) |
335 done |
332 done |
336 |
333 |
362 by (cases x) (auto simp add: enat_0 eSuc_enat[THEN sym]) |
359 by (cases x) (auto simp add: enat_0 eSuc_enat[THEN sym]) |
363 |
360 |
364 lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)" |
361 lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)" |
365 by (cases x) auto |
362 by (cases x) auto |
366 |
363 |
367 lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y & a ~= \<bottom> & enat n < #y)" |
364 lemma slen_scons_eq: "(enat (Suc n) < #x) = (? a y. x = a && y \<and> a \<noteq> \<bottom> \<and> enat n < #y)" |
368 apply (auto, case_tac "x=UU",auto) |
365 apply (auto, case_tac "x=UU",auto) |
369 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
366 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
370 apply (case_tac "#y") apply simp_all |
367 apply (case_tac "#y") apply simp_all |
371 apply (case_tac "#y") apply simp_all |
368 apply (case_tac "#y") apply simp_all |
372 done |
369 done |
373 |
370 |
374 lemma slen_eSuc: "#x = eSuc n --> (? a y. x = a&&y & a ~= \<bottom> & #y = n)" |
371 lemma slen_eSuc: "#x = eSuc n \<longrightarrow> (\<exists>a y. x = a && y \<and> a \<noteq> \<bottom> \<and> #y = n)" |
375 by (cases x) auto |
372 by (cases x) auto |
376 |
373 |
377 lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>" |
374 lemma slen_stream_take_finite [simp]: "#(stream_take n\<cdot>s) \<noteq> \<infinity>" |
378 by (simp add: slen_def) |
375 by (simp add: slen_def) |
379 |
376 |
380 lemma slen_scons_eq_rev: "(#x < enat (Suc (Suc n))) = (!a y. x ~= a && y | a = \<bottom> | #y < enat (Suc n))" |
377 lemma slen_scons_eq_rev: "#x < enat (Suc (Suc n)) \<longleftrightarrow> (\<forall>a y. x \<noteq> a && y \<or> a = \<bottom> \<or> #y < enat (Suc n))" |
381 apply (cases x, auto) |
378 apply (cases x, auto) |
382 apply (simp add: zero_enat_def) |
379 apply (simp add: zero_enat_def) |
383 apply (case_tac "#stream") apply (simp_all add: eSuc_enat) |
380 apply (case_tac "#stream") apply (simp_all add: eSuc_enat) |
384 apply (case_tac "#stream") apply (simp_all add: eSuc_enat) |
381 apply (case_tac "#stream") apply (simp_all add: eSuc_enat) |
385 done |
382 done |
386 |
383 |
387 lemma slen_take_lemma4 [rule_format]: |
384 lemma slen_take_lemma4 [rule_format]: |
388 "!s. stream_take n$s ~= s --> #(stream_take n$s) = enat n" |
385 "\<forall>s. stream_take n\<cdot>s \<noteq> s \<longrightarrow> #(stream_take n\<cdot>s) = enat n" |
389 apply (induct n, auto simp add: enat_0) |
386 apply (induct n, auto simp add: enat_0) |
390 apply (case_tac "s=UU", simp) |
387 apply (case_tac "s=UU", simp) |
391 apply (drule stream_exhaust_eq [THEN iffD1], auto simp add: eSuc_enat) |
388 apply (drule stream_exhaust_eq [THEN iffD1], auto simp add: eSuc_enat) |
392 done |
389 done |
393 |
390 |
394 (* |
391 (* |
395 lemma stream_take_idempotent [simp]: |
392 lemma stream_take_idempotent [simp]: |
396 "stream_take n$(stream_take n$s) = stream_take n$s" |
393 "stream_take n\<cdot>(stream_take n\<cdot>s) = stream_take n\<cdot>s" |
397 apply (case_tac "stream_take n$s = s") |
394 apply (case_tac "stream_take n\<cdot>s = s") |
398 apply (auto,insert slen_take_lemma4 [of n s]); |
395 apply (auto,insert slen_take_lemma4 [of n s]); |
399 by (auto,insert slen_take_lemma1 [of "stream_take n$s" n],simp) |
396 by (auto,insert slen_take_lemma1 [of "stream_take n\<cdot>s" n],simp) |
400 |
397 |
401 lemma stream_take_take_Suc [simp]: "stream_take n$(stream_take (Suc n)$s) = |
398 lemma stream_take_take_Suc [simp]: "stream_take n\<cdot>(stream_take (Suc n)\<cdot>s) = |
402 stream_take n$s" |
399 stream_take n\<cdot>s" |
403 apply (simp add: po_eq_conv,auto) |
400 apply (simp add: po_eq_conv,auto) |
404 apply (simp add: stream_take_take_less) |
401 apply (simp add: stream_take_take_less) |
405 apply (subgoal_tac "stream_take n$s = stream_take n$(stream_take n$s)") |
402 apply (subgoal_tac "stream_take n\<cdot>s = stream_take n\<cdot>(stream_take n\<cdot>s)") |
406 apply (erule ssubst) |
403 apply (erule ssubst) |
407 apply (rule_tac monofun_cfun_arg) |
404 apply (rule_tac monofun_cfun_arg) |
408 apply (insert chain_stream_take [of s]) |
405 apply (insert chain_stream_take [of s]) |
409 by (simp add: chain_def,simp) |
406 by (simp add: chain_def,simp) |
410 *) |
407 *) |
411 |
408 |
412 lemma slen_take_eq: "ALL x. (enat n < #x) = (stream_take n\<cdot>x ~= x)" |
409 lemma slen_take_eq: "\<forall>x. enat n < #x \<longleftrightarrow> stream_take n\<cdot>x \<noteq> x" |
413 apply (induct_tac n, auto) |
410 apply (induct_tac n, auto) |
414 apply (simp add: enat_0, clarsimp) |
411 apply (simp add: enat_0, clarsimp) |
415 apply (drule not_sym) |
412 apply (drule not_sym) |
416 apply (drule slen_empty_eq [THEN iffD1], simp) |
413 apply (drule slen_empty_eq [THEN iffD1], simp) |
417 apply (case_tac "x=UU", simp) |
414 apply (case_tac "x=UU", simp) |
424 apply (erule_tac x="y" in allE, simp) |
421 apply (erule_tac x="y" in allE, simp) |
425 apply (case_tac "#y") |
422 apply (case_tac "#y") |
426 apply simp_all |
423 apply simp_all |
427 done |
424 done |
428 |
425 |
429 lemma slen_take_eq_rev: "(#x <= enat n) = (stream_take n\<cdot>x = x)" |
426 lemma slen_take_eq_rev: "#x \<le> enat n \<longleftrightarrow> stream_take n\<cdot>x = x" |
430 by (simp add: linorder_not_less [symmetric] slen_take_eq) |
427 by (simp add: linorder_not_less [symmetric] slen_take_eq) |
431 |
428 |
432 lemma slen_take_lemma1: "#x = enat n ==> stream_take n\<cdot>x = x" |
429 lemma slen_take_lemma1: "#x = enat n \<Longrightarrow> stream_take n\<cdot>x = x" |
433 by (rule slen_take_eq_rev [THEN iffD1], auto) |
430 by (rule slen_take_eq_rev [THEN iffD1], auto) |
434 |
431 |
435 lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)" |
432 lemma slen_rt_mono: "#s2 \<le> #s1 \<Longrightarrow> #(rt\<cdot>s2) \<le> #(rt\<cdot>s1)" |
436 apply (cases s1) |
433 apply (cases s1) |
437 apply (cases s2, simp+)+ |
434 apply (cases s2, simp+)+ |
438 done |
435 done |
439 |
436 |
440 lemma slen_take_lemma5: "#(stream_take n$s) <= enat n" |
437 lemma slen_take_lemma5: "#(stream_take n\<cdot>s) \<le> enat n" |
441 apply (case_tac "stream_take n$s = s") |
438 apply (case_tac "stream_take n\<cdot>s = s") |
442 apply (simp add: slen_take_eq_rev) |
439 apply (simp add: slen_take_eq_rev) |
443 apply (simp add: slen_take_lemma4) |
440 apply (simp add: slen_take_lemma4) |
444 done |
441 done |
445 |
442 |
446 lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\<cdot>x) = enat i" |
443 lemma slen_take_lemma2: "\<forall>x. \<not> stream_finite x \<longrightarrow> #(stream_take i\<cdot>x) = enat i" |
447 apply (simp add: stream.finite_def, auto) |
444 apply (simp add: stream.finite_def, auto) |
448 apply (simp add: slen_take_lemma4) |
445 apply (simp add: slen_take_lemma4) |
449 done |
446 done |
450 |
447 |
451 lemma slen_infinite: "stream_finite x = (#x ~= \<infinity>)" |
448 lemma slen_infinite: "stream_finite x \<longleftrightarrow> #x \<noteq> \<infinity>" |
452 by (simp add: slen_def) |
449 by (simp add: slen_def) |
453 |
450 |
454 lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t" |
451 lemma slen_mono_lemma: "stream_finite s \<Longrightarrow> \<forall>t. s \<sqsubseteq> t \<longrightarrow> #s \<le> #t" |
455 apply (erule stream_finite_ind [of s], auto) |
452 apply (erule stream_finite_ind [of s], auto) |
456 apply (case_tac "t=UU", auto) |
453 apply (case_tac "t = UU", auto) |
457 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
454 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
458 done |
455 done |
459 |
456 |
460 lemma slen_mono: "s << t ==> #s <= #t" |
457 lemma slen_mono: "s \<sqsubseteq> t \<Longrightarrow> #s \<le> #t" |
461 apply (case_tac "stream_finite t") |
458 apply (case_tac "stream_finite t") |
462 apply (frule stream_finite_less) |
459 apply (frule stream_finite_less) |
463 apply (erule_tac x="s" in allE, simp) |
460 apply (erule_tac x="s" in allE, simp) |
464 apply (drule slen_mono_lemma, auto) |
461 apply (drule slen_mono_lemma, auto) |
465 apply (simp add: slen_def) |
462 apply (simp add: slen_def) |
466 done |
463 done |
467 |
464 |
468 lemma iterate_lemma: "F$(iterate n$F$x) = iterate n$F$(F$x)" |
465 lemma iterate_lemma: "F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate n\<cdot>F\<cdot>(F\<cdot>x)" |
469 by (insert iterate_Suc2 [of n F x], auto) |
466 by (insert iterate_Suc2 [of n F x], auto) |
470 |
467 |
471 lemma slen_rt_mult [rule_format]: "!x. enat (i + j) <= #x --> enat j <= #(iterate i$rt$x)" |
468 lemma slen_rt_mult [rule_format]: "\<forall>x. enat (i + j) \<le> #x \<longrightarrow> enat j \<le> #(iterate i\<cdot>rt\<cdot>x)" |
472 apply (induct i, auto) |
469 apply (induct i, auto) |
473 apply (case_tac "x=UU", auto simp add: zero_enat_def) |
470 apply (case_tac "x = UU", auto simp add: zero_enat_def) |
474 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
471 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
475 apply (erule_tac x="y" in allE, auto) |
472 apply (erule_tac x = "y" in allE, auto) |
476 apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: eSuc_enat) |
473 apply (simp add: not_le) apply (case_tac "#y") apply (simp_all add: eSuc_enat) |
477 apply (simp add: iterate_lemma) |
474 apply (simp add: iterate_lemma) |
478 done |
475 done |
479 |
476 |
480 lemma slen_take_lemma3 [rule_format]: |
477 lemma slen_take_lemma3 [rule_format]: |
481 "!(x::'a::flat stream) y. enat n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y" |
478 "\<forall>(x::'a::flat stream) y. enat n \<le> #x \<longrightarrow> x \<sqsubseteq> y \<longrightarrow> stream_take n\<cdot>x = stream_take n\<cdot>y" |
482 apply (induct_tac n, auto) |
479 apply (induct_tac n, auto) |
483 apply (case_tac "x=UU", auto) |
480 apply (case_tac "x=UU", auto) |
484 apply (simp add: zero_enat_def) |
481 apply (simp add: zero_enat_def) |
485 apply (simp add: Suc_ile_eq) |
482 apply (simp add: Suc_ile_eq) |
486 apply (case_tac "y=UU", clarsimp) |
483 apply (case_tac "y=UU", clarsimp) |
487 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+ |
484 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+ |
488 apply (erule_tac x="ya" in allE, simp) |
485 apply (erule_tac x="ya" in allE, simp) |
489 by (drule ax_flat, simp) |
486 by (drule ax_flat, simp) |
490 |
487 |
491 lemma slen_strict_mono_lemma: |
488 lemma slen_strict_mono_lemma: |
492 "stream_finite t ==> !s. #(s::'a::flat stream) = #t & s << t --> s = t" |
489 "stream_finite t \<Longrightarrow> \<forall>s. #(s::'a::flat stream) = #t \<and> s \<sqsubseteq> t \<longrightarrow> s = t" |
493 apply (erule stream_finite_ind, auto) |
490 apply (erule stream_finite_ind, auto) |
494 apply (case_tac "sa=UU", auto) |
491 apply (case_tac "sa = UU", auto) |
495 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
492 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
496 apply (drule ax_flat, simp) |
493 apply (drule ax_flat, simp) |
497 done |
494 done |
498 |
495 |
499 lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t" |
496 lemma slen_strict_mono: "\<lbrakk>stream_finite t; s \<noteq> t; s \<sqsubseteq> (t::'a::flat stream)\<rbrakk> \<Longrightarrow> #s < #t" |
500 by (auto simp add: slen_mono less_le dest: slen_strict_mono_lemma) |
497 by (auto simp add: slen_mono less_le dest: slen_strict_mono_lemma) |
501 |
498 |
502 lemma stream_take_Suc_neq: "stream_take (Suc n)$s ~=s ==> |
499 lemma stream_take_Suc_neq: "stream_take (Suc n)\<cdot>s \<noteq> s \<Longrightarrow> |
503 stream_take n$s ~= stream_take (Suc n)$s" |
500 stream_take n\<cdot>s \<noteq> stream_take (Suc n)\<cdot>s" |
504 apply auto |
501 apply auto |
505 apply (subgoal_tac "stream_take n$s ~=s") |
502 apply (subgoal_tac "stream_take n\<cdot>s \<noteq> s") |
506 apply (insert slen_take_lemma4 [of n s],auto) |
503 apply (insert slen_take_lemma4 [of n s],auto) |
507 apply (cases s, simp) |
504 apply (cases s, simp) |
508 apply (simp add: slen_take_lemma4 eSuc_enat) |
505 apply (simp add: slen_take_lemma4 eSuc_enat) |
509 done |
506 done |
510 |
507 |
561 by (induct n) (simp_all add: i_rt_def) |
558 by (induct n) (simp_all add: i_rt_def) |
562 |
559 |
563 lemma i_rt_0 [simp]: "i_rt 0 s = s" |
560 lemma i_rt_0 [simp]: "i_rt 0 s = s" |
564 by (simp add: i_rt_def) |
561 by (simp add: i_rt_def) |
565 |
562 |
566 lemma i_rt_Suc [simp]: "a ~= UU ==> i_rt (Suc n) (a&&s) = i_rt n s" |
563 lemma i_rt_Suc [simp]: "a \<noteq> UU \<Longrightarrow> i_rt (Suc n) (a&&s) = i_rt n s" |
567 by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc) |
564 by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc) |
568 |
565 |
569 lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt$s)" |
566 lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt\<cdot>s)" |
570 by (simp only: i_rt_def iterate_Suc2) |
567 by (simp only: i_rt_def iterate_Suc2) |
571 |
568 |
572 lemma i_rt_Suc_back:"i_rt (Suc n) s = rt$(i_rt n s)" |
569 lemma i_rt_Suc_back: "i_rt (Suc n) s = rt\<cdot>(i_rt n s)" |
573 by (simp only: i_rt_def,auto) |
570 by (simp only: i_rt_def,auto) |
574 |
571 |
575 lemma i_rt_mono: "x << s ==> i_rt n x << i_rt n s" |
572 lemma i_rt_mono: "x << s \<Longrightarrow> i_rt n x << i_rt n s" |
576 by (simp add: i_rt_def monofun_rt_mult) |
573 by (simp add: i_rt_def monofun_rt_mult) |
577 |
574 |
578 lemma i_rt_ij_lemma: "enat (i + j) <= #x ==> enat j <= #(i_rt i x)" |
575 lemma i_rt_ij_lemma: "enat (i + j) \<le> #x \<Longrightarrow> enat j \<le> #(i_rt i x)" |
579 by (simp add: i_rt_def slen_rt_mult) |
576 by (simp add: i_rt_def slen_rt_mult) |
580 |
577 |
581 lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)" |
578 lemma slen_i_rt_mono: "#s2 \<le> #s1 \<Longrightarrow> #(i_rt n s2) \<le> #(i_rt n s1)" |
582 apply (induct_tac n,auto) |
579 apply (induct_tac n,auto) |
583 apply (simp add: i_rt_Suc_back) |
580 apply (simp add: i_rt_Suc_back) |
584 apply (drule slen_rt_mono,simp) |
581 apply (drule slen_rt_mono,simp) |
585 done |
582 done |
586 |
583 |
587 lemma i_rt_take_lemma1 [rule_format]: "ALL s. i_rt n (stream_take n$s) = UU" |
584 lemma i_rt_take_lemma1 [rule_format]: "\<forall>s. i_rt n (stream_take n\<cdot>s) = UU" |
588 apply (induct_tac n) |
585 apply (induct_tac n) |
589 apply (simp add: i_rt_Suc_back,auto) |
586 apply (simp add: i_rt_Suc_back,auto) |
590 apply (case_tac "s=UU",auto) |
587 apply (case_tac "s=UU",auto) |
591 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
588 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
592 done |
589 done |
593 |
590 |
594 lemma i_rt_slen: "(i_rt n s = UU) = (stream_take n$s = s)" |
591 lemma i_rt_slen: "i_rt n s = UU \<longleftrightarrow> stream_take n\<cdot>s = s" |
595 apply auto |
592 apply auto |
596 apply (insert i_rt_ij_lemma [of n "Suc 0" s]) |
593 apply (insert i_rt_ij_lemma [of n "Suc 0" s]) |
597 apply (subgoal_tac "#(i_rt n s)=0") |
594 apply (subgoal_tac "#(i_rt n s)=0") |
598 apply (case_tac "stream_take n$s = s",simp+) |
595 apply (case_tac "stream_take n\<cdot>s = s",simp+) |
599 apply (insert slen_take_eq [rule_format,of n s],simp) |
596 apply (insert slen_take_eq [rule_format,of n s],simp) |
600 apply (cases "#s") apply (simp_all add: zero_enat_def) |
597 apply (cases "#s") apply (simp_all add: zero_enat_def) |
601 apply (simp add: slen_take_eq) |
598 apply (simp add: slen_take_eq) |
602 apply (cases "#s") |
599 apply (cases "#s") |
603 using i_rt_take_lemma1 [of n s] |
600 using i_rt_take_lemma1 [of n s] |
604 apply (simp_all add: zero_enat_def) |
601 apply (simp_all add: zero_enat_def) |
605 done |
602 done |
606 |
603 |
607 lemma i_rt_lemma_slen: "#s=enat n ==> i_rt n s = UU" |
604 lemma i_rt_lemma_slen: "#s=enat n \<Longrightarrow> i_rt n s = UU" |
608 by (simp add: i_rt_slen slen_take_lemma1) |
605 by (simp add: i_rt_slen slen_take_lemma1) |
609 |
606 |
610 lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s" |
607 lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s" |
611 apply (induct_tac n, auto) |
608 apply (induct_tac n, auto) |
612 apply (cases s, auto simp del: i_rt_Suc) |
609 apply (cases s, auto simp del: i_rt_Suc) |
613 apply (simp add: i_rt_Suc_back stream_finite_rt_eq)+ |
610 apply (simp add: i_rt_Suc_back stream_finite_rt_eq)+ |
614 done |
611 done |
615 |
612 |
616 lemma take_i_rt_len_lemma: "ALL sl x j t. enat sl = #x & n <= sl & |
613 lemma take_i_rt_len_lemma: "\<forall>sl x j t. enat sl = #x \<and> n \<le> sl \<and> |
617 #(stream_take n$x) = enat t & #(i_rt n x)= enat j |
614 #(stream_take n\<cdot>x) = enat t \<and> #(i_rt n x) = enat j |
618 --> enat (j + t) = #x" |
615 \<longrightarrow> enat (j + t) = #x" |
619 apply (induct n, auto) |
616 apply (induct n, auto) |
620 apply (simp add: zero_enat_def) |
617 apply (simp add: zero_enat_def) |
621 apply (case_tac "x=UU",auto) |
618 apply (case_tac "x=UU",auto) |
622 apply (simp add: zero_enat_def) |
619 apply (simp add: zero_enat_def) |
623 apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) |
620 apply (drule stream_exhaust_eq [THEN iffD1],clarsimp) |
624 apply (subgoal_tac "EX k. enat k = #y",clarify) |
621 apply (subgoal_tac "\<exists>k. enat k = #y",clarify) |
625 apply (erule_tac x="k" in allE) |
622 apply (erule_tac x="k" in allE) |
626 apply (erule_tac x="y" in allE,auto) |
623 apply (erule_tac x="y" in allE,auto) |
627 apply (erule_tac x="THE p. Suc p = t" in allE,auto) |
624 apply (erule_tac x="THE p. Suc p = t" in allE,auto) |
628 apply (simp add: eSuc_def split: enat.splits) |
625 apply (simp add: eSuc_def split: enat.splits) |
629 apply (simp add: eSuc_def split: enat.splits) |
626 apply (simp add: eSuc_def split: enat.splits) |
650 apply (cases "i_rt n s1", simp) |
647 apply (cases "i_rt n s1", simp) |
651 apply (cases "i_rt n s2", auto) |
648 apply (cases "i_rt n s2", auto) |
652 done |
649 done |
653 |
650 |
654 lemma i_th_stream_take_Suc [rule_format]: |
651 lemma i_th_stream_take_Suc [rule_format]: |
655 "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s" |
652 "\<forall>s. i_th n (stream_take (Suc n)\<cdot>s) = i_th n s" |
656 apply (induct_tac n,auto) |
653 apply (induct_tac n,auto) |
657 apply (simp add: i_th_def) |
654 apply (simp add: i_th_def) |
658 apply (case_tac "s=UU",auto) |
655 apply (case_tac "s=UU",auto) |
659 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
656 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
660 apply (case_tac "s=UU",simp add: i_th_def) |
657 apply (case_tac "s=UU",simp add: i_th_def) |
661 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
658 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
662 apply (simp add: i_th_def i_rt_Suc_forw) |
659 apply (simp add: i_th_def i_rt_Suc_forw) |
663 done |
660 done |
664 |
661 |
665 lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)$s)" |
662 lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)\<cdot>s)" |
666 apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)$s)"]) |
663 apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)\<cdot>s)"]) |
667 apply (rule i_th_stream_take_Suc [THEN subst]) |
664 apply (rule i_th_stream_take_Suc [THEN subst]) |
668 apply (simp add: i_th_def i_rt_Suc_back [symmetric]) |
665 apply (simp add: i_th_def i_rt_Suc_back [symmetric]) |
669 by (simp add: i_rt_take_lemma1) |
666 by (simp add: i_rt_take_lemma1) |
670 |
667 |
671 lemma i_th_last_eq: |
668 lemma i_th_last_eq: |
672 "i_th n s1 = i_th n s2 ==> i_rt n (stream_take (Suc n)$s1) = i_rt n (stream_take (Suc n)$s2)" |
669 "i_th n s1 = i_th n s2 \<Longrightarrow> i_rt n (stream_take (Suc n)\<cdot>s1) = i_rt n (stream_take (Suc n)\<cdot>s2)" |
673 apply (insert i_th_last [of n s1]) |
670 apply (insert i_th_last [of n s1]) |
674 apply (insert i_th_last [of n s2]) |
671 apply (insert i_th_last [of n s2]) |
675 apply auto |
672 apply auto |
676 done |
673 done |
677 |
674 |
678 lemma i_th_prefix_lemma: |
675 lemma i_th_prefix_lemma: |
679 "[| k <= n; stream_take (Suc n)$s1 << stream_take (Suc n)$s2 |] ==> |
676 "\<lbrakk>k \<le> n; stream_take (Suc n)\<cdot>s1 << stream_take (Suc n)\<cdot>s2\<rbrakk> \<Longrightarrow> |
680 i_th k s1 << i_th k s2" |
677 i_th k s1 << i_th k s2" |
681 apply (insert i_th_stream_take_Suc [of k s1, THEN sym]) |
678 apply (insert i_th_stream_take_Suc [of k s1, THEN sym]) |
682 apply (insert i_th_stream_take_Suc [of k s2, THEN sym],auto) |
679 apply (insert i_th_stream_take_Suc [of k s2, THEN sym],auto) |
683 apply (simp add: i_th_def) |
680 apply (simp add: i_th_def) |
684 apply (rule monofun_cfun, auto) |
681 apply (rule monofun_cfun, auto) |
685 apply (rule i_rt_mono) |
682 apply (rule i_rt_mono) |
686 apply (blast intro: stream_take_lemma10) |
683 apply (blast intro: stream_take_lemma10) |
687 done |
684 done |
688 |
685 |
689 lemma take_i_rt_prefix_lemma1: |
686 lemma take_i_rt_prefix_lemma1: |
690 "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> |
687 "stream_take (Suc n)\<cdot>s1 << stream_take (Suc n)\<cdot>s2 \<Longrightarrow> |
691 i_rt (Suc n) s1 << i_rt (Suc n) s2 ==> |
688 i_rt (Suc n) s1 << i_rt (Suc n) s2 \<Longrightarrow> |
692 i_rt n s1 << i_rt n s2 & stream_take n$s1 << stream_take n$s2" |
689 i_rt n s1 << i_rt n s2 \<and> stream_take n\<cdot>s1 << stream_take n\<cdot>s2" |
693 apply auto |
690 apply auto |
694 apply (insert i_th_prefix_lemma [of n n s1 s2]) |
691 apply (insert i_th_prefix_lemma [of n n s1 s2]) |
695 apply (rule i_th_i_rt_step,auto) |
692 apply (rule i_th_i_rt_step,auto) |
696 apply (drule mono_stream_take_pred,simp) |
693 apply (drule mono_stream_take_pred,simp) |
697 done |
694 done |
698 |
695 |
699 lemma take_i_rt_prefix_lemma: |
696 lemma take_i_rt_prefix_lemma: |
700 "[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2" |
697 "\<lbrakk>stream_take n\<cdot>s1 << stream_take n\<cdot>s2; i_rt n s1 << i_rt n s2\<rbrakk> \<Longrightarrow> s1 << s2" |
701 apply (case_tac "n=0",simp) |
698 apply (case_tac "n=0",simp) |
702 apply (auto) |
699 apply (auto) |
703 apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 & |
700 apply (subgoal_tac "stream_take 0\<cdot>s1 << stream_take 0\<cdot>s2 \<and> i_rt 0 s1 << i_rt 0 s2") |
704 i_rt 0 s1 << i_rt 0 s2") |
|
705 defer 1 |
701 defer 1 |
706 apply (rule zero_induct,blast) |
702 apply (rule zero_induct,blast) |
707 apply (blast dest: take_i_rt_prefix_lemma1) |
703 apply (blast dest: take_i_rt_prefix_lemma1) |
708 apply simp |
704 apply simp |
709 done |
705 done |
710 |
706 |
711 lemma streams_prefix_lemma: "(s1 << s2) = |
707 lemma streams_prefix_lemma: "s1 << s2 \<longleftrightarrow> |
712 (stream_take n$s1 << stream_take n$s2 & i_rt n s1 << i_rt n s2)" |
708 (stream_take n\<cdot>s1 << stream_take n\<cdot>s2 \<and> i_rt n s1 << i_rt n s2)" |
713 apply auto |
709 apply auto |
714 apply (simp add: monofun_cfun_arg) |
710 apply (simp add: monofun_cfun_arg) |
715 apply (simp add: i_rt_mono) |
711 apply (simp add: i_rt_mono) |
716 apply (erule take_i_rt_prefix_lemma,simp) |
712 apply (erule take_i_rt_prefix_lemma,simp) |
717 done |
713 done |
718 |
714 |
719 lemma streams_prefix_lemma1: |
715 lemma streams_prefix_lemma1: |
720 "[| stream_take n$s1 = stream_take n$s2; i_rt n s1 = i_rt n s2 |] ==> s1 = s2" |
716 "\<lbrakk>stream_take n\<cdot>s1 = stream_take n\<cdot>s2; i_rt n s1 = i_rt n s2\<rbrakk> \<Longrightarrow> s1 = s2" |
721 apply (simp add: po_eq_conv,auto) |
717 apply (simp add: po_eq_conv,auto) |
722 apply (insert streams_prefix_lemma) |
718 apply (insert streams_prefix_lemma) |
723 apply blast+ |
719 apply blast+ |
724 done |
720 done |
725 |
721 |
729 (* ----------------------------------------------------------------------- *) |
725 (* ----------------------------------------------------------------------- *) |
730 |
726 |
731 lemma UU_sconc [simp]: " UU ooo s = s " |
727 lemma UU_sconc [simp]: " UU ooo s = s " |
732 by (simp add: sconc_def zero_enat_def) |
728 by (simp add: sconc_def zero_enat_def) |
733 |
729 |
734 lemma scons_neq_UU: "a~=UU ==> a && s ~=UU" |
730 lemma scons_neq_UU: "a \<noteq> UU \<Longrightarrow> a && s \<noteq> UU" |
735 by auto |
731 by auto |
736 |
732 |
737 lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y" |
733 lemma singleton_sconc [rule_format, simp]: "x \<noteq> UU \<longrightarrow> (x && UU) ooo y = x && y" |
738 apply (simp add: sconc_def zero_enat_def eSuc_def split: enat.splits, auto) |
734 apply (simp add: sconc_def zero_enat_def eSuc_def split: enat.splits, auto) |
739 apply (rule someI2_ex,auto) |
735 apply (rule someI2_ex,auto) |
740 apply (rule_tac x="x && y" in exI,auto) |
736 apply (rule_tac x="x && y" in exI,auto) |
741 apply (simp add: i_rt_Suc_forw) |
737 apply (simp add: i_rt_Suc_forw) |
742 apply (case_tac "xa=UU",simp) |
738 apply (case_tac "xa=UU",simp) |
743 by (drule stream_exhaust_eq [THEN iffD1],auto) |
739 by (drule stream_exhaust_eq [THEN iffD1],auto) |
744 |
740 |
745 lemma ex_sconc [rule_format]: |
741 lemma ex_sconc [rule_format]: |
746 "ALL k y. #x = enat k --> (EX w. stream_take k$w = x & i_rt k w = y)" |
742 "\<forall>k y. #x = enat k \<longrightarrow> (\<exists>w. stream_take k\<cdot>w = x \<and> i_rt k w = y)" |
747 apply (case_tac "#x") |
743 apply (case_tac "#x") |
748 apply (rule stream_finite_ind [of x],auto) |
744 apply (rule stream_finite_ind [of x],auto) |
749 apply (simp add: stream.finite_def) |
745 apply (simp add: stream.finite_def) |
750 apply (drule slen_take_lemma1,blast) |
746 apply (drule slen_take_lemma1,blast) |
751 apply (simp_all add: zero_enat_def eSuc_def split: enat.splits) |
747 apply (simp_all add: zero_enat_def eSuc_def split: enat.splits) |
752 apply (erule_tac x="y" in allE,auto) |
748 apply (erule_tac x="y" in allE,auto) |
753 apply (rule_tac x="a && w" in exI,auto) |
749 apply (rule_tac x="a && w" in exI,auto) |
754 done |
750 done |
755 |
751 |
756 lemma rt_sconc1: "enat n = #x ==> i_rt n (x ooo y) = y" |
752 lemma rt_sconc1: "enat n = #x \<Longrightarrow> i_rt n (x ooo y) = y" |
757 apply (simp add: sconc_def split: enat.splits, arith?,auto) |
753 apply (simp add: sconc_def split: enat.splits, arith?,auto) |
758 apply (rule someI2_ex,auto) |
754 apply (rule someI2_ex,auto) |
759 apply (drule ex_sconc,simp) |
755 apply (drule ex_sconc,simp) |
760 done |
756 done |
761 |
757 |
775 apply (drule slen_take_lemma1,auto) |
771 apply (drule slen_take_lemma1,auto) |
776 apply (simp add: i_rt_slen) |
772 apply (simp add: i_rt_slen) |
777 apply (simp add: sconc_def) |
773 apply (simp add: sconc_def) |
778 done |
774 done |
779 |
775 |
780 lemma stream_take_sconc [simp]: "enat n = #x ==> stream_take n$(x ooo y) = x" |
776 lemma stream_take_sconc [simp]: "enat n = #x \<Longrightarrow> stream_take n\<cdot>(x ooo y) = x" |
781 apply (simp add: sconc_def) |
777 apply (simp add: sconc_def) |
782 apply (cases "#x") |
778 apply (cases "#x") |
783 apply auto |
779 apply auto |
784 apply (rule someI2_ex, auto) |
780 apply (rule someI2_ex, auto) |
785 apply (drule ex_sconc,simp) |
781 apply (drule ex_sconc,simp) |
786 done |
782 done |
787 |
783 |
788 lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y" |
784 lemma scons_sconc [rule_format,simp]: "a \<noteq> UU \<longrightarrow> (a && x) ooo y = a && x ooo y" |
789 apply (cases "#x",auto) |
785 apply (cases "#x",auto) |
790 apply (simp add: sconc_def eSuc_enat) |
786 apply (simp add: sconc_def eSuc_enat) |
791 apply (rule someI2_ex) |
787 apply (rule someI2_ex) |
792 apply (drule ex_sconc, simp) |
788 apply (drule ex_sconc, simp) |
793 apply (rule someI2_ex, auto) |
789 apply (rule someI2_ex, auto) |
823 apply (cases "stream_finite x") |
819 apply (cases "stream_finite x") |
824 apply (erule cont_sconc_lemma1) |
820 apply (erule cont_sconc_lemma1) |
825 apply (erule cont_sconc_lemma2) |
821 apply (erule cont_sconc_lemma2) |
826 done |
822 done |
827 |
823 |
828 lemma sconc_mono: "y << y' ==> x ooo y << x ooo y'" |
824 lemma sconc_mono: "y << y' \<Longrightarrow> x ooo y << x ooo y'" |
829 by (rule cont_sconc [THEN cont2mono, THEN monofunE]) |
825 by (rule cont_sconc [THEN cont2mono, THEN monofunE]) |
830 |
826 |
831 lemma sconc_mono1 [simp]: "x << x ooo y" |
827 lemma sconc_mono1 [simp]: "x << x ooo y" |
832 by (rule sconc_mono [of UU, simplified]) |
828 by (rule sconc_mono [of UU, simplified]) |
833 |
829 |
834 (* ----------------------------------------------------------------------- *) |
830 (* ----------------------------------------------------------------------- *) |
835 |
831 |
836 lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)" |
832 lemma empty_sconc [simp]: "x ooo y = UU \<longleftrightarrow> x = UU \<and> y = UU" |
837 apply (case_tac "#x",auto) |
833 apply (case_tac "#x",auto) |
838 apply (insert sconc_mono1 [of x y]) |
834 apply (insert sconc_mono1 [of x y]) |
839 apply auto |
835 apply auto |
840 done |
836 done |
841 |
837 |
842 (* ----------------------------------------------------------------------- *) |
838 (* ----------------------------------------------------------------------- *) |
843 |
839 |
844 lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x" |
840 lemma rt_sconc [rule_format, simp]: "s \<noteq> UU \<longrightarrow> rt\<cdot>(s ooo x) = rt\<cdot>s ooo x" |
845 by (cases s, auto) |
841 by (cases s, auto) |
846 |
842 |
847 lemma i_th_sconc_lemma [rule_format]: |
843 lemma i_th_sconc_lemma [rule_format]: |
848 "ALL x y. enat n < #x --> i_th n (x ooo y) = i_th n x" |
844 "\<forall>x y. enat n < #x \<longrightarrow> i_th n (x ooo y) = i_th n x" |
849 apply (induct_tac n, auto) |
845 apply (induct_tac n, auto) |
850 apply (simp add: enat_0 i_th_def) |
846 apply (simp add: enat_0 i_th_def) |
851 apply (simp add: slen_empty_eq ft_sconc) |
847 apply (simp add: slen_empty_eq ft_sconc) |
852 apply (simp add: i_th_def) |
848 apply (simp add: i_th_def) |
853 apply (case_tac "x=UU",auto) |
849 apply (case_tac "x=UU",auto) |
859 |
855 |
860 |
856 |
861 |
857 |
862 (* ----------------------------------------------------------------------- *) |
858 (* ----------------------------------------------------------------------- *) |
863 |
859 |
864 lemma sconc_lemma [rule_format, simp]: "ALL s. stream_take n$s ooo i_rt n s = s" |
860 lemma sconc_lemma [rule_format, simp]: "\<forall>s. stream_take n\<cdot>s ooo i_rt n s = s" |
865 apply (induct_tac n,auto) |
861 apply (induct_tac n,auto) |
866 apply (case_tac "s=UU",auto) |
862 apply (case_tac "s=UU",auto) |
867 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
863 apply (drule stream_exhaust_eq [THEN iffD1],auto) |
868 done |
864 done |
869 |
865 |
870 (* ----------------------------------------------------------------------- *) |
866 (* ----------------------------------------------------------------------- *) |
871 subsection "pointwise equality" |
867 subsection "pointwise equality" |
872 (* ----------------------------------------------------------------------- *) |
868 (* ----------------------------------------------------------------------- *) |
873 |
869 |
874 lemma ex_last_stream_take_scons: "stream_take (Suc n)$s = |
870 lemma ex_last_stream_take_scons: "stream_take (Suc n)\<cdot>s = |
875 stream_take n$s ooo i_rt n (stream_take (Suc n)$s)" |
871 stream_take n\<cdot>s ooo i_rt n (stream_take (Suc n)\<cdot>s)" |
876 by (insert sconc_lemma [of n "stream_take (Suc n)$s"],simp) |
872 by (insert sconc_lemma [of n "stream_take (Suc n)\<cdot>s"],simp) |
877 |
873 |
878 lemma i_th_stream_take_eq: |
874 lemma i_th_stream_take_eq: |
879 "!!n. ALL n. i_th n s1 = i_th n s2 ==> stream_take n$s1 = stream_take n$s2" |
875 "\<And>n. \<forall>n. i_th n s1 = i_th n s2 \<Longrightarrow> stream_take n\<cdot>s1 = stream_take n\<cdot>s2" |
880 apply (induct_tac n,auto) |
876 apply (induct_tac n,auto) |
881 apply (subgoal_tac "stream_take (Suc na)$s1 = |
877 apply (subgoal_tac "stream_take (Suc na)\<cdot>s1 = |
882 stream_take na$s1 ooo i_rt na (stream_take (Suc na)$s1)") |
878 stream_take na\<cdot>s1 ooo i_rt na (stream_take (Suc na)\<cdot>s1)") |
883 apply (subgoal_tac "i_rt na (stream_take (Suc na)$s1) = |
879 apply (subgoal_tac "i_rt na (stream_take (Suc na)\<cdot>s1) = |
884 i_rt na (stream_take (Suc na)$s2)") |
880 i_rt na (stream_take (Suc na)\<cdot>s2)") |
885 apply (subgoal_tac "stream_take (Suc na)$s2 = |
881 apply (subgoal_tac "stream_take (Suc na)\<cdot>s2 = |
886 stream_take na$s2 ooo i_rt na (stream_take (Suc na)$s2)") |
882 stream_take na\<cdot>s2 ooo i_rt na (stream_take (Suc na)\<cdot>s2)") |
887 apply (insert ex_last_stream_take_scons,simp) |
883 apply (insert ex_last_stream_take_scons,simp) |
888 apply blast |
884 apply blast |
889 apply (erule_tac x="na" in allE) |
885 apply (erule_tac x="na" in allE) |
890 apply (insert i_th_last_eq [of _ s1 s2]) |
886 apply (insert i_th_last_eq [of _ s1 s2]) |
891 by blast+ |
887 by blast+ |
892 |
888 |
893 lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2" |
889 lemma pointwise_eq_lemma[rule_format]: "\<forall>n. i_th n s1 = i_th n s2 \<Longrightarrow> s1 = s2" |
894 by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast) |
890 by (insert i_th_stream_take_eq [THEN stream.take_lemma],blast) |
895 |
891 |
896 (* ----------------------------------------------------------------------- *) |
892 (* ----------------------------------------------------------------------- *) |
897 subsection "finiteness" |
893 subsection "finiteness" |
898 (* ----------------------------------------------------------------------- *) |
894 (* ----------------------------------------------------------------------- *) |
899 |
895 |
900 lemma slen_sconc_finite1: |
896 lemma slen_sconc_finite1: |
901 "[| #(x ooo y) = \<infinity>; enat n = #x |] ==> #y = \<infinity>" |
897 "\<lbrakk>#(x ooo y) = \<infinity>; enat n = #x\<rbrakk> \<Longrightarrow> #y = \<infinity>" |
902 apply (case_tac "#y ~= \<infinity>",auto) |
898 apply (case_tac "#y \<noteq> \<infinity>",auto) |
903 apply (drule_tac y=y in rt_sconc1) |
899 apply (drule_tac y=y in rt_sconc1) |
904 apply (insert stream_finite_i_rt [of n "x ooo y"]) |
900 apply (insert stream_finite_i_rt [of n "x ooo y"]) |
905 apply (simp add: slen_infinite) |
901 apply (simp add: slen_infinite) |
906 done |
902 done |
907 |
903 |
908 lemma slen_sconc_infinite1: "#x=\<infinity> ==> #(x ooo y) = \<infinity>" |
904 lemma slen_sconc_infinite1: "#x=\<infinity> \<Longrightarrow> #(x ooo y) = \<infinity>" |
909 by (simp add: sconc_def) |
905 by (simp add: sconc_def) |
910 |
906 |
911 lemma slen_sconc_infinite2: "#y=\<infinity> ==> #(x ooo y) = \<infinity>" |
907 lemma slen_sconc_infinite2: "#y=\<infinity> \<Longrightarrow> #(x ooo y) = \<infinity>" |
912 apply (case_tac "#x") |
908 apply (case_tac "#x") |
913 apply (simp add: sconc_def) |
909 apply (simp add: sconc_def) |
914 apply (rule someI2_ex) |
910 apply (rule someI2_ex) |
915 apply (drule ex_sconc,auto) |
911 apply (drule ex_sconc,auto) |
916 apply (erule contrapos_pp) |
912 apply (erule contrapos_pp) |
917 apply (insert stream_finite_i_rt) |
913 apply (insert stream_finite_i_rt) |
918 apply (fastforce simp add: slen_infinite,auto) |
914 apply (fastforce simp add: slen_infinite,auto) |
919 by (simp add: sconc_def) |
915 by (simp add: sconc_def) |
920 |
916 |
921 lemma sconc_finite: "(#x~=\<infinity> & #y~=\<infinity>) = (#(x ooo y)~=\<infinity>)" |
917 lemma sconc_finite: "#x \<noteq> \<infinity> \<and> #y \<noteq> \<infinity> \<longleftrightarrow> #(x ooo y) \<noteq> \<infinity>" |
922 apply auto |
918 apply auto |
923 apply (metis not_infinity_eq slen_sconc_finite1) |
919 apply (metis not_infinity_eq slen_sconc_finite1) |
924 apply (metis not_infinity_eq slen_sconc_infinite1) |
920 apply (metis not_infinity_eq slen_sconc_infinite1) |
925 apply (metis not_infinity_eq slen_sconc_infinite2) |
921 apply (metis not_infinity_eq slen_sconc_infinite2) |
926 done |
922 done |
927 |
923 |
928 (* ----------------------------------------------------------------------- *) |
924 (* ----------------------------------------------------------------------- *) |
929 |
925 |
930 lemma slen_sconc_mono3: "[| enat n = #x; enat k = #(x ooo y) |] ==> n <= k" |
926 lemma slen_sconc_mono3: "\<lbrakk>enat n = #x; enat k = #(x ooo y)\<rbrakk> \<Longrightarrow> n \<le> k" |
931 apply (insert slen_mono [of "x" "x ooo y"]) |
927 apply (insert slen_mono [of "x" "x ooo y"]) |
932 apply (cases "#x") apply simp_all |
928 apply (cases "#x") apply simp_all |
933 apply (cases "#(x ooo y)") apply simp_all |
929 apply (cases "#(x ooo y)") apply simp_all |
934 done |
930 done |
935 |
931 |
936 (* ----------------------------------------------------------------------- *) |
932 (* ----------------------------------------------------------------------- *) |
937 subsection "finite slen" |
933 subsection "finite slen" |
938 (* ----------------------------------------------------------------------- *) |
934 (* ----------------------------------------------------------------------- *) |
939 |
935 |
940 lemma slen_sconc: "[| enat n = #x; enat m = #y |] ==> #(x ooo y) = enat (n + m)" |
936 lemma slen_sconc: "\<lbrakk>enat n = #x; enat m = #y\<rbrakk> \<Longrightarrow> #(x ooo y) = enat (n + m)" |
941 apply (case_tac "#(x ooo y)") |
937 apply (case_tac "#(x ooo y)") |
942 apply (frule_tac y=y in rt_sconc1) |
938 apply (frule_tac y=y in rt_sconc1) |
943 apply (insert take_i_rt_len [of "THE j. enat j = #(x ooo y)" "x ooo y" n n m],simp) |
939 apply (insert take_i_rt_len [of "THE j. enat j = #(x ooo y)" "x ooo y" n n m],simp) |
944 apply (insert slen_sconc_mono3 [of n x _ y],simp) |
940 apply (insert slen_sconc_mono3 [of n x _ y],simp) |
945 apply (insert sconc_finite [of x y],auto) |
941 apply (insert sconc_finite [of x y],auto) |
965 |
961 |
966 (* ----------------------------------------------------------------------- *) |
962 (* ----------------------------------------------------------------------- *) |
967 subsection "continuity" |
963 subsection "continuity" |
968 (* ----------------------------------------------------------------------- *) |
964 (* ----------------------------------------------------------------------- *) |
969 |
965 |
970 lemma chain_sconc: "chain S ==> chain (%i. (x ooo S i))" |
966 lemma chain_sconc: "chain S \<Longrightarrow> chain (\<lambda>i. (x ooo S i))" |
971 by (simp add: chain_def,auto simp add: sconc_mono) |
967 by (simp add: chain_def,auto simp add: sconc_mono) |
972 |
968 |
973 lemma chain_scons: "chain S ==> chain (%i. a && S i)" |
969 lemma chain_scons: "chain S \<Longrightarrow> chain (\<lambda>i. a && S i)" |
974 apply (simp add: chain_def,auto) |
970 apply (simp add: chain_def,auto) |
975 apply (rule monofun_cfun_arg,simp) |
971 apply (rule monofun_cfun_arg,simp) |
976 done |
972 done |
977 |
973 |
978 lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)" |
974 lemma contlub_scons_lemma: "chain S \<Longrightarrow> (LUB i. a && S i) = a && (LUB i. S i)" |
979 by (rule cont2contlubE [OF cont_Rep_cfun2, symmetric]) |
975 by (rule cont2contlubE [OF cont_Rep_cfun2, symmetric]) |
980 |
976 |
981 lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==> |
977 lemma finite_lub_sconc: "chain Y \<Longrightarrow> stream_finite x \<Longrightarrow> |
982 (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" |
978 (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" |
983 apply (rule stream_finite_ind [of x]) |
979 apply (rule stream_finite_ind [of x]) |
984 apply (auto) |
980 apply (auto) |
985 apply (subgoal_tac "(LUB i. a && (s ooo Y i)) = a && (LUB i. s ooo Y i)") |
981 apply (subgoal_tac "(LUB i. a && (s ooo Y i)) = a && (LUB i. s ooo Y i)") |
986 apply (force,blast dest: contlub_scons_lemma chain_sconc) |
982 apply (force,blast dest: contlub_scons_lemma chain_sconc) |
987 done |
983 done |
988 |
984 |
989 lemma contlub_sconc_lemma: |
985 lemma contlub_sconc_lemma: |
990 "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" |
986 "chain Y \<Longrightarrow> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" |
991 apply (case_tac "#x=\<infinity>") |
987 apply (case_tac "#x=\<infinity>") |
992 apply (simp add: sconc_def) |
988 apply (simp add: sconc_def) |
993 apply (drule finite_lub_sconc,auto simp add: slen_infinite) |
989 apply (drule finite_lub_sconc,auto simp add: slen_infinite) |
994 done |
990 done |
995 |
991 |
996 lemma monofun_sconc: "monofun (%y. x ooo y)" |
992 lemma monofun_sconc: "monofun (\<lambda>y. x ooo y)" |
997 by (simp add: monofun_def sconc_mono) |
993 by (simp add: monofun_def sconc_mono) |
998 |
994 |
999 |
995 |
1000 (* ----------------------------------------------------------------------- *) |
996 (* ----------------------------------------------------------------------- *) |
1001 section "constr_sconc" |
997 section "constr_sconc" |