|
1 (* Title: HOLCF/Streams.thy |
|
2 ID: $Id$ |
|
3 Author: Borislav Gajanovic and David von Oheimb |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
5 |
|
6 Stream domains with concatenation. |
|
7 TODO: HOLCF/ex/Stream.* should be integrated into this file. |
|
8 *) |
|
9 |
|
10 theory Streams = Stream : |
|
11 |
|
12 (* ----------------------------------------------------------------------- *) |
|
13 |
|
14 lemma stream_neq_UU: "x~=UU ==> EX a as. x=a&&as & a~=UU" |
|
15 by (simp add: stream_exhaust_eq,auto) |
|
16 |
|
17 lemma stream_prefix1: "[| x<<y; xs<<ys |] ==> x&&xs << y&&ys" |
|
18 by (insert stream_prefix' [of y "x&&xs" ys],force) |
|
19 |
|
20 lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1" |
|
21 apply (insert chain_stream_take [of s1]) |
|
22 by (drule chain_mono3,auto) |
|
23 |
|
24 lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2" |
|
25 by (simp add: monofun_cfun_arg) |
|
26 |
|
27 lemma stream_take_prefix [simp]: "stream_take n$s << s" |
|
28 apply (subgoal_tac "s=(LUB n. stream_take n$s)") |
|
29 apply (erule ssubst, rule is_ub_thelub) |
|
30 apply (simp only: chain_stream_take) |
|
31 by (simp only: stream_reach2) |
|
32 |
|
33 lemma stream_take_take_less:"stream_take k$(stream_take n$s) << stream_take k$s" |
|
34 by (rule monofun_cfun_arg,auto) |
|
35 |
|
36 (* ----------------------------------------------------------------------- *) |
|
37 |
|
38 lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)" |
|
39 apply (rule stream.casedist [of s1]) |
|
40 apply (rule stream.casedist [of s2],simp+) |
|
41 by (rule stream.casedist [of s2],auto) |
|
42 |
|
43 lemma slen_take_lemma4 [rule_format]: |
|
44 "!s. stream_take n$s ~= s --> #(stream_take n$s) = Fin n" |
|
45 apply (induct_tac n,auto simp add: Fin_0) |
|
46 apply (case_tac "s=UU",simp) |
|
47 by (drule stream_neq_UU,auto) |
|
48 |
|
49 lemma slen_take_lemma5: "#(stream_take n$s) <= Fin n"; |
|
50 apply (case_tac "stream_take n$s = s") |
|
51 apply (simp add: slen_take_eq_rev) |
|
52 by (simp add: slen_take_lemma4) |
|
53 |
|
54 lemma stream_take_idempotent [simp]: |
|
55 "stream_take n$(stream_take n$s) = stream_take n$s" |
|
56 apply (case_tac "stream_take n$s = s") |
|
57 apply (auto,insert slen_take_lemma4 [of n s]); |
|
58 by (auto,insert slen_take_lemma1 [of "stream_take n$s" n],simp) |
|
59 |
|
60 lemma stream_take_take_Suc [simp]: "stream_take n$(stream_take (Suc n)$s) = |
|
61 stream_take n$s" |
|
62 apply (simp add: po_eq_conv,auto) |
|
63 apply (simp add: stream_take_take_less) |
|
64 apply (subgoal_tac "stream_take n$s = stream_take n$(stream_take n$s)") |
|
65 apply (erule ssubst) |
|
66 apply (rule_tac monofun_cfun_arg) |
|
67 apply (insert chain_stream_take [of s]) |
|
68 by (simp add: chain_def,simp) |
|
69 |
|
70 lemma mono_stream_take_pred: |
|
71 "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> |
|
72 stream_take n$s1 << stream_take n$s2" |
|
73 by (drule mono_stream_take [of _ _ n],simp) |
|
74 |
|
75 lemma stream_take_lemma10 [rule_format]: |
|
76 "ALL k<=n. stream_take n$s1 << stream_take n$s2 |
|
77 --> stream_take k$s1 << stream_take k$s2" |
|
78 apply (induct_tac n,simp,clarsimp) |
|
79 apply (case_tac "k=Suc n",blast) |
|
80 apply (erule_tac x="k" in allE) |
|
81 by (drule mono_stream_take_pred,simp) |
|
82 |
|
83 lemma stream_take_finite [simp]: "stream_finite (stream_take n$s)" |
|
84 apply (simp add: stream.finite_def) |
|
85 by (rule_tac x="n" in exI,simp) |
|
86 |
|
87 lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>" |
|
88 by (simp add: slen_def) |
|
89 |
|
90 lemma stream_take_Suc_neq: "stream_take (Suc n)$s ~=s ==> |
|
91 stream_take n$s ~= stream_take (Suc n)$s" |
|
92 apply auto |
|
93 apply (subgoal_tac "stream_take n$s ~=s") |
|
94 apply (insert slen_take_lemma4 [of n s],auto) |
|
95 apply (rule stream.casedist [of s],simp) |
|
96 apply (simp add: inat_defs split:inat_splits) |
|
97 by (simp add: slen_take_lemma4) |
|
98 |
|
99 |
|
100 (* ----------------------------------------------------------------------- *) |
|
101 |
|
102 consts |
|
103 |
|
104 i_rt :: "nat => 'a stream => 'a stream" (* chops the first i elements *) |
|
105 i_th :: "nat => 'a stream => 'a" (* the i-th element *) |
|
106 |
|
107 sconc :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) |
|
108 constr_sconc :: "'a stream => 'a stream => 'a stream" (* constructive *) |
|
109 constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" |
|
110 |
|
111 defs |
|
112 i_rt_def: "i_rt == %i s. iterate i rt s" |
|
113 i_th_def: "i_th == %i s. ft$(i_rt i s)" |
|
114 |
|
115 sconc_def: "s1 ooo s2 == case #s1 of |
|
116 Fin n => (SOME s. (stream_take n$s=s1) & (i_rt n s = s2)) |
|
117 | \<infinity> => s1" |
|
118 |
|
119 constr_sconc_def: "constr_sconc s1 s2 == case #s1 of |
|
120 Fin n => constr_sconc' n s1 s2 |
|
121 | \<infinity> => s1" |
|
122 primrec |
|
123 constr_sconc'_0: "constr_sconc' 0 s1 s2 = s2" |
|
124 constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 && |
|
125 constr_sconc' n (rt$s1) s2" |
|
126 |
|
127 |
|
128 (* ----------------------------------------------------------------------- *) |
|
129 section "i_rt" |
|
130 (* ----------------------------------------------------------------------- *) |
|
131 |
|
132 lemma i_rt_UU [simp]: "i_rt n UU = UU" |
|
133 apply (simp add: i_rt_def) |
|
134 by (rule iterate.induct,auto) |
|
135 |
|
136 lemma i_rt_0 [simp]: "i_rt 0 s = s" |
|
137 by (simp add: i_rt_def) |
|
138 |
|
139 lemma i_rt_Suc [simp]: "a ~= UU ==> i_rt (Suc n) (a&&s) = i_rt n s" |
|
140 by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc) |
|
141 |
|
142 lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt$s)" |
|
143 by (simp only: i_rt_def iterate_Suc2) |
|
144 |
|
145 lemma i_rt_Suc_back:"i_rt (Suc n) s = rt$(i_rt n s)" |
|
146 by (simp only: i_rt_def,auto) |
|
147 |
|
148 lemma i_rt_mono: "x << s ==> i_rt n x << i_rt n s" |
|
149 by (simp add: i_rt_def monofun_rt_mult) |
|
150 |
|
151 lemma i_rt_ij_lemma: "Fin (i + j) <= #x ==> Fin j <= #(i_rt i x)" |
|
152 by (simp add: i_rt_def slen_rt_mult) |
|
153 |
|
154 lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)" |
|
155 apply (induct_tac n,auto) |
|
156 apply (simp add: i_rt_Suc_back) |
|
157 by (drule slen_rt_mono,simp) |
|
158 |
|
159 lemma i_rt_take_lemma1 [rule_format]: "ALL s. i_rt n (stream_take n$s) = UU" |
|
160 apply (induct_tac n); |
|
161 apply (simp add: i_rt_Suc_back,auto) |
|
162 apply (case_tac "s=UU",auto) |
|
163 by (drule stream_neq_UU,simp add: i_rt_Suc_forw,auto) |
|
164 |
|
165 lemma i_rt_slen: "(i_rt n s = UU) = (stream_take n$s = s)" |
|
166 apply auto |
|
167 apply (insert i_rt_ij_lemma [of n "Suc 0" s]); |
|
168 apply (subgoal_tac "#(i_rt n s)=0") |
|
169 apply (case_tac "stream_take n$s = s",simp+) |
|
170 apply (insert slen_take_eq [of n s],simp) |
|
171 apply (simp add: inat_defs split:inat_splits) |
|
172 apply (simp add: slen_take_eq ) |
|
173 by (simp, insert i_rt_take_lemma1 [of n s],simp) |
|
174 |
|
175 lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU" |
|
176 by (simp add: i_rt_slen slen_take_lemma1) |
|
177 |
|
178 lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s" |
|
179 apply (induct_tac n, auto) |
|
180 apply (rule stream.casedist [of "s"], auto simp del: i_rt_Suc) |
|
181 by (simp add: i_rt_Suc_back stream_finite_rt_eq)+ |
|
182 |
|
183 lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl & |
|
184 #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j |
|
185 --> Fin (j + t) = #x" |
|
186 apply (induct_tac n,auto) |
|
187 apply (simp add: inat_defs) |
|
188 apply (case_tac "x=UU",auto) |
|
189 apply (simp add: inat_defs) |
|
190 apply (drule stream_neq_UU,auto) |
|
191 apply (subgoal_tac "EX k. Fin k = #as",clarify) |
|
192 apply (erule_tac x="k" in allE) |
|
193 apply (erule_tac x="as" in allE,auto) |
|
194 apply (erule_tac x="THE p. Suc p = t" in allE,auto) |
|
195 apply (simp add: inat_defs split:inat_splits) |
|
196 apply (simp add: inat_defs split:inat_splits) |
|
197 apply (simp only: the_equality) |
|
198 apply (simp add: inat_defs split:inat_splits) |
|
199 apply force |
|
200 by (simp add: inat_defs split:inat_splits) |
|
201 |
|
202 lemma take_i_rt_len: |
|
203 "[| Fin sl = #x; n <= sl; #(stream_take n$x) = Fin t; #(i_rt n x) = Fin j |] ==> |
|
204 Fin (j + t) = #x" |
|
205 by (blast intro: take_i_rt_len_lemma [rule_format]) |
|
206 |
|
207 |
|
208 (* ----------------------------------------------------------------------- *) |
|
209 section "i_th" |
|
210 (* ----------------------------------------------------------------------- *) |
|
211 |
|
212 lemma i_th_i_rt_step: |
|
213 "[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==> |
|
214 i_rt n s1 << i_rt n s2" |
|
215 apply (simp add: i_th_def i_rt_Suc_back) |
|
216 apply (rule stream.casedist [of "i_rt n s1"],simp) |
|
217 apply (rule stream.casedist [of "i_rt n s2"],auto) |
|
218 by (drule stream_prefix1,auto) |
|
219 |
|
220 lemma i_th_stream_take_Suc [rule_format]: |
|
221 "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s" |
|
222 apply (induct_tac n,auto) |
|
223 apply (simp add: i_th_def) |
|
224 apply (case_tac "s=UU",auto) |
|
225 apply (drule stream_neq_UU,auto) |
|
226 apply (case_tac "s=UU",simp add: i_th_def) |
|
227 apply (drule stream_neq_UU,auto) |
|
228 by (simp add: i_th_def i_rt_Suc_forw) |
|
229 |
|
230 lemma last_lemma10: "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> |
|
231 i_th n s1 << i_th n s2" |
|
232 apply (rule i_th_stream_take_Suc [THEN subst]) |
|
233 apply (rule i_th_stream_take_Suc [THEN subst]) back |
|
234 apply (simp add: i_th_def) |
|
235 apply (rule monofun_cfun_arg) |
|
236 by (erule i_rt_mono) |
|
237 |
|
238 lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)$s)" |
|
239 apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)$s)"]) |
|
240 apply (rule i_th_stream_take_Suc [THEN subst]) |
|
241 apply (simp add: i_th_def i_rt_Suc_back [symmetric]) |
|
242 by (simp add: i_rt_take_lemma1) |
|
243 |
|
244 lemma i_th_last_eq: |
|
245 "i_th n s1 = i_th n s2 ==> i_rt n (stream_take (Suc n)$s1) = i_rt n (stream_take (Suc n)$s2)" |
|
246 apply (insert i_th_last [of n s1]) |
|
247 apply (insert i_th_last [of n s2]) |
|
248 by auto |
|
249 |
|
250 lemma i_th_prefix_lemma: |
|
251 "[| k <= n; stream_take (Suc n)$s1 << stream_take (Suc n)$s2 |] ==> |
|
252 i_th k s1 << i_th k s2" |
|
253 apply (subgoal_tac "stream_take (Suc k)$s1 << stream_take (Suc k)$s2") |
|
254 apply (simp add: last_lemma10) |
|
255 by (blast intro: stream_take_lemma10) |
|
256 |
|
257 lemma take_i_rt_prefix_lemma1: |
|
258 "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> |
|
259 i_rt (Suc n) s1 << i_rt (Suc n) s2 ==> |
|
260 i_rt n s1 << i_rt n s2 & stream_take n$s1 << stream_take n$s2" |
|
261 apply auto |
|
262 apply (insert i_th_prefix_lemma [of n n s1 s2]) |
|
263 apply (rule i_th_i_rt_step,auto) |
|
264 by (drule mono_stream_take_pred,simp) |
|
265 |
|
266 lemma take_i_rt_prefix_lemma: |
|
267 "[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2" |
|
268 apply (case_tac "n=0",simp) |
|
269 apply (insert neq0_conv [of n]) |
|
270 apply (insert not0_implies_Suc [of n],auto) |
|
271 apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 & |
|
272 i_rt 0 s1 << i_rt 0 s2") |
|
273 defer 1 |
|
274 apply (rule zero_induct,blast) |
|
275 apply (blast dest: take_i_rt_prefix_lemma1) |
|
276 by simp |
|
277 |
|
278 lemma streams_prefix_lemma: "(s1 << s2) = |
|
279 (stream_take n$s1 << stream_take n$s2 & i_rt n s1 << i_rt n s2)"; |
|
280 apply auto |
|
281 apply (simp add: monofun_cfun_arg) |
|
282 apply (simp add: i_rt_mono) |
|
283 by (erule take_i_rt_prefix_lemma,simp) |
|
284 |
|
285 lemma streams_prefix_lemma1: |
|
286 "[| stream_take n$s1 = stream_take n$s2; i_rt n s1 = i_rt n s2 |] ==> s1 = s2" |
|
287 apply (simp add: po_eq_conv,auto) |
|
288 apply (insert streams_prefix_lemma) |
|
289 by blast+ |
|
290 |
|
291 |
|
292 (* ----------------------------------------------------------------------- *) |
|
293 section "sconc" |
|
294 (* ----------------------------------------------------------------------- *) |
|
295 |
|
296 lemma UU_sconc [simp]: " UU ooo s = s " |
|
297 by (simp add: sconc_def inat_defs) |
|
298 |
|
299 lemma scons_neq_UU: "a~=UU ==> a && s ~=UU" |
|
300 by auto |
|
301 |
|
302 lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y" |
|
303 apply (simp add: sconc_def inat_defs split:inat_splits,auto) |
|
304 apply (rule someI2_ex,auto) |
|
305 apply (rule_tac x="x && y" in exI,auto) |
|
306 apply (simp add: i_rt_Suc_forw) |
|
307 apply (case_tac "xa=UU",simp) |
|
308 by (drule stream_neq_UU,auto) |
|
309 |
|
310 lemma ex_sconc [rule_format]: |
|
311 "ALL k y. #x = Fin k --> (EX w. stream_take k$w = x & i_rt k w = y)" |
|
312 apply (case_tac "#x") |
|
313 apply (rule stream_finite_ind [of x],auto) |
|
314 apply (simp add: stream.finite_def) |
|
315 apply (drule slen_take_lemma1,blast) |
|
316 apply (simp add: inat_defs split:inat_splits)+ |
|
317 apply (erule_tac x="y" in allE,auto) |
|
318 by (rule_tac x="a && w" in exI,auto) |
|
319 |
|
320 lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y"; |
|
321 apply (simp add: sconc_def inat_defs split:inat_splits , arith?,auto) |
|
322 apply (rule someI2_ex,auto) |
|
323 by (drule ex_sconc,simp) |
|
324 |
|
325 lemma sconc_inj2: "\<lbrakk>Fin n = #x; x ooo y = x ooo z\<rbrakk> \<Longrightarrow> y = z" |
|
326 apply (frule_tac y=y in rt_sconc1) |
|
327 by (auto elim: rt_sconc1) |
|
328 |
|
329 lemma sconc_UU [simp]:"s ooo UU = s" |
|
330 apply (case_tac "#s") |
|
331 apply (simp add: sconc_def inat_defs) |
|
332 apply (rule someI2_ex) |
|
333 apply (rule_tac x="s" in exI) |
|
334 apply auto |
|
335 apply (drule slen_take_lemma1,auto) |
|
336 apply (simp add: i_rt_lemma_slen) |
|
337 apply (drule slen_take_lemma1,auto) |
|
338 apply (simp add: i_rt_slen) |
|
339 by (simp add: sconc_def inat_defs) |
|
340 |
|
341 lemma stream_take_sconc [simp]: "Fin n = #x ==> stream_take n$(x ooo y) = x" |
|
342 apply (simp add: sconc_def) |
|
343 apply (simp add: inat_defs split:inat_splits,auto) |
|
344 apply (rule someI2_ex,auto) |
|
345 by (drule ex_sconc,simp) |
|
346 |
|
347 lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y" |
|
348 apply (case_tac "#x",auto) |
|
349 apply (simp add: sconc_def) |
|
350 apply (rule someI2_ex) |
|
351 apply (drule ex_sconc,simp) |
|
352 apply (rule someI2_ex,auto) |
|
353 apply (simp add: i_rt_Suc_forw) |
|
354 apply (rule_tac x="a && x" in exI,auto) |
|
355 apply (case_tac "xa=UU",auto) |
|
356 apply (drule_tac s="stream_take nat$x" in scons_neq_UU) |
|
357 apply (simp add: i_rt_Suc_forw) |
|
358 apply (drule stream_neq_UU,clarsimp) |
|
359 apply (drule streams_prefix_lemma1,simp+) |
|
360 by (simp add: sconc_def) |
|
361 |
|
362 lemma ft_sconc: "x ~= UU ==> ft$(x ooo y) = ft$x" |
|
363 by (rule stream.casedist [of x],auto) |
|
364 |
|
365 lemma sconc_assoc: "(x ooo y) ooo z = x ooo y ooo z" |
|
366 apply (case_tac "#x") |
|
367 apply (rule stream_finite_ind [of x],auto simp del: scons_sconc) |
|
368 apply (simp add: stream.finite_def del: scons_sconc) |
|
369 apply (drule slen_take_lemma1,auto simp del: scons_sconc) |
|
370 apply (case_tac "a = UU", auto) |
|
371 by (simp add: sconc_def) |
|
372 |
|
373 |
|
374 (* ----------------------------------------------------------------------- *) |
|
375 |
|
376 lemma sconc_mono: "y << y' ==> x ooo y << x ooo y'" |
|
377 apply (case_tac "#x") |
|
378 apply (rule stream_finite_ind [of "x"]) |
|
379 apply (auto simp add: stream.finite_def) |
|
380 apply (drule slen_take_lemma1,blast) |
|
381 by (simp add: stream_prefix',auto simp add: sconc_def) |
|
382 |
|
383 lemma sconc_mono1 [simp]: "x << x ooo y" |
|
384 by (rule sconc_mono [of UU, simplified]) |
|
385 |
|
386 (* ----------------------------------------------------------------------- *) |
|
387 |
|
388 lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)" |
|
389 apply (case_tac "#x",auto) |
|
390 by (insert sconc_mono1 [of x y],auto); |
|
391 |
|
392 (* ----------------------------------------------------------------------- *) |
|
393 |
|
394 lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x" |
|
395 by (rule stream.casedist,auto) |
|
396 |
|
397 (* ----------------------------------------------------------------------- *) |
|
398 |
|
399 lemma sconc_lemma [rule_format, simp]: "ALL s. stream_take n$s ooo i_rt n s = s" |
|
400 apply (induct_tac n,auto) |
|
401 apply (case_tac "s=UU",auto) |
|
402 by (drule stream_neq_UU,auto) |
|
403 |
|
404 (* ----------------------------------------------------------------------- *) |
|
405 subsection "pointwise equality" |
|
406 (* ----------------------------------------------------------------------- *) |
|
407 |
|
408 lemma ex_last_stream_take_scons: "stream_take (Suc n)$s = |
|
409 stream_take n$s ooo i_rt n (stream_take (Suc n)$s)" |
|
410 by (insert sconc_lemma [of n "stream_take (Suc n)$s"],simp) |
|
411 |
|
412 lemma i_th_stream_take_eq: |
|
413 "!!n. ALL n. i_th n s1 = i_th n s2 ==> stream_take n$s1 = stream_take n$s2" |
|
414 apply (induct_tac n,auto) |
|
415 apply (subgoal_tac "stream_take (Suc na)$s1 = |
|
416 stream_take na$s1 ooo i_rt na (stream_take (Suc na)$s1)") |
|
417 apply (subgoal_tac "i_rt na (stream_take (Suc na)$s1) = |
|
418 i_rt na (stream_take (Suc na)$s2)") |
|
419 apply (subgoal_tac "stream_take (Suc na)$s2 = |
|
420 stream_take na$s2 ooo i_rt na (stream_take (Suc na)$s2)") |
|
421 apply (insert ex_last_stream_take_scons,simp) |
|
422 apply blast |
|
423 apply (erule_tac x="na" in allE) |
|
424 apply (insert i_th_last_eq [of _ s1 s2]) |
|
425 by blast+ |
|
426 |
|
427 lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2" |
|
428 by (insert i_th_stream_take_eq [THEN stream.take_lemmas],blast) |
|
429 |
|
430 (* ----------------------------------------------------------------------- *) |
|
431 subsection "finiteness" |
|
432 (* ----------------------------------------------------------------------- *) |
|
433 |
|
434 lemma slen_sconc_finite1: |
|
435 "[| #(x ooo y) = Infty; Fin n = #x |] ==> #y = Infty" |
|
436 apply (case_tac "#y ~= Infty",auto) |
|
437 apply (simp only: slen_infinite [symmetric]) |
|
438 apply (drule_tac y=y in rt_sconc1) |
|
439 apply (insert stream_finite_i_rt [of n "x ooo y"]) |
|
440 by (simp add: slen_infinite) |
|
441 |
|
442 lemma slen_sconc_infinite1: "#x=Infty ==> #(x ooo y) = Infty" |
|
443 by (simp add: sconc_def) |
|
444 |
|
445 lemma slen_sconc_infinite2: "#y=Infty ==> #(x ooo y) = Infty" |
|
446 apply (case_tac "#x") |
|
447 apply (simp add: sconc_def) |
|
448 apply (rule someI2_ex) |
|
449 apply (drule ex_sconc,auto) |
|
450 apply (erule contrapos_pp) |
|
451 apply (insert stream_finite_i_rt) |
|
452 apply (simp add: slen_infinite ,auto) |
|
453 by (simp add: sconc_def) |
|
454 |
|
455 lemma sconc_finite: "(#x~=Infty & #y~=Infty) = (#(x ooo y)~=Infty)" |
|
456 apply auto |
|
457 apply (case_tac "#x",auto) |
|
458 apply (erule contrapos_pp,simp) |
|
459 apply (erule slen_sconc_finite1,simp) |
|
460 apply (drule slen_sconc_infinite1 [of _ y],simp) |
|
461 by (drule slen_sconc_infinite2 [of _ x],simp) |
|
462 |
|
463 (* ----------------------------------------------------------------------- *) |
|
464 |
|
465 lemma slen_sconc_mono3: "[| Fin n = #x; Fin k = #(x ooo y) |] ==> n <= k" |
|
466 apply (insert slen_mono [of "x" "x ooo y"]) |
|
467 by (simp add: inat_defs split: inat_splits) |
|
468 |
|
469 (* ----------------------------------------------------------------------- *) |
|
470 subsection "finite slen" |
|
471 (* ----------------------------------------------------------------------- *) |
|
472 |
|
473 lemma slen_sconc: "[| Fin n = #x; Fin m = #y |] ==> #(x ooo y) = Fin (n + m)" |
|
474 apply (case_tac "#(x ooo y)") |
|
475 apply (frule_tac y=y in rt_sconc1) |
|
476 apply (insert take_i_rt_len [of "THE j. Fin j = #(x ooo y)" "x ooo y" n n m],simp) |
|
477 apply (insert slen_sconc_mono3 [of n x _ y],simp) |
|
478 by (insert sconc_finite [of x y],auto) |
|
479 |
|
480 (* ----------------------------------------------------------------------- *) |
|
481 subsection "flat prefix" |
|
482 (* ----------------------------------------------------------------------- *) |
|
483 |
|
484 lemma sconc_prefix: "(s1::'a::flat stream) << s2 ==> EX t. s1 ooo t = s2" |
|
485 apply (case_tac "#s1") |
|
486 apply (subgoal_tac "stream_take nat$s1 = stream_take nat$s2"); |
|
487 apply (rule_tac x="i_rt nat s2" in exI) |
|
488 apply (simp add: sconc_def) |
|
489 apply (rule someI2_ex) |
|
490 apply (drule ex_sconc) |
|
491 apply (simp,clarsimp,drule streams_prefix_lemma1) |
|
492 apply (simp+,rule slen_take_lemma3 [rule_format, of _ s1 s2]); |
|
493 apply (simp+,rule_tac x="UU" in exI) |
|
494 apply (insert slen_take_lemma3 [rule_format, of _ s1 s2]); |
|
495 by (rule stream.take_lemmas,simp) |
|
496 |
|
497 (* ----------------------------------------------------------------------- *) |
|
498 subsection "continuity" |
|
499 (* ----------------------------------------------------------------------- *) |
|
500 |
|
501 lemma chain_sconc: "chain S ==> chain (%i. (x ooo S i))" |
|
502 by (simp add: chain_def,auto simp add: sconc_mono) |
|
503 |
|
504 lemma chain_scons: "chain S ==> chain (%i. a && S i)" |
|
505 apply (simp add: chain_def,auto) |
|
506 by (rule monofun_cfun_arg,simp) |
|
507 |
|
508 lemma contlub_scons: "contlub (%x. a && x)" |
|
509 by (simp add: contlub_Rep_CFun2) |
|
510 |
|
511 lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)" |
|
512 apply (insert contlub_scons [of a]) |
|
513 by (simp only: contlub) |
|
514 |
|
515 lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==> |
|
516 (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" |
|
517 apply (rule stream_finite_ind [of x]) |
|
518 apply (auto) |
|
519 apply (subgoal_tac "(LUB i. a && (s ooo Y i)) = a && (LUB i. s ooo Y i)") |
|
520 by (force,blast dest: contlub_scons_lemma chain_sconc) |
|
521 |
|
522 lemma contlub_sconc_lemma: |
|
523 "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))" |
|
524 apply (case_tac "#x=Infty") |
|
525 apply (simp add: sconc_def) |
|
526 prefer 2 |
|
527 apply (drule finite_lub_sconc,auto simp add: slen_infinite) |
|
528 apply (simp add: slen_def) |
|
529 apply (insert lub_const [of x] unique_lub [of _ x _]) |
|
530 by (auto simp add: lub) |
|
531 |
|
532 lemma contlub_sconc: "contlub (%y. x ooo y)"; |
|
533 by (rule contlubI, insert contlub_sconc_lemma [of _ x], simp); |
|
534 |
|
535 lemma monofun_sconc: "monofun (%y. x ooo y)" |
|
536 by (simp add: monofun sconc_mono) |
|
537 |
|
538 lemma cont_sconc: "cont (%y. x ooo y)" |
|
539 apply (rule monocontlub2cont) |
|
540 apply (rule monofunI, simp add: sconc_mono) |
|
541 by (rule contlub_sconc); |
|
542 |
|
543 |
|
544 (* ----------------------------------------------------------------------- *) |
|
545 section "constr_sconc" |
|
546 (* ----------------------------------------------------------------------- *) |
|
547 |
|
548 lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s" |
|
549 by (simp add: constr_sconc_def inat_defs) |
|
550 |
|
551 lemma "x ooo y = constr_sconc x y" |
|
552 apply (case_tac "#x") |
|
553 apply (rule stream_finite_ind [of x],auto simp del: scons_sconc) |
|
554 defer 1 |
|
555 apply (simp add: constr_sconc_def del: scons_sconc) |
|
556 apply (case_tac "#s") |
|
557 apply (simp add: inat_defs) |
|
558 apply (case_tac "a=UU",auto simp del: scons_sconc) |
|
559 apply (simp) |
|
560 apply (simp add: sconc_def) |
|
561 apply (simp add: constr_sconc_def) |
|
562 apply (simp add: stream.finite_def) |
|
563 by (drule slen_take_lemma1,auto) |
|
564 |
|
565 end |