|
1 (* Title: HOLCF/FOCUS/Fstreams.thy |
|
2 ID: $Id$ |
|
3 Author: Borislav Gajanovic |
|
4 |
|
5 FOCUS flat streams (with lifted elements) |
|
6 ###TODO: integrate this with Fstream.* |
|
7 *) |
|
8 |
|
9 theory Fstreams = Stream: |
|
10 |
|
11 defaultsort type |
|
12 |
|
13 types 'a fstream = "('a lift) stream" |
|
14 |
|
15 consts |
|
16 |
|
17 fsingleton :: "'a => 'a fstream" ("<_>" [1000] 999) |
|
18 fsfilter :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" |
|
19 fsmap :: "('a => 'b) => 'a fstream -> 'b fstream" |
|
20 |
|
21 jth :: "nat => 'a fstream => 'a" |
|
22 |
|
23 first :: "'a fstream => 'a" |
|
24 last :: "'a fstream => 'a" |
|
25 |
|
26 |
|
27 syntax |
|
28 |
|
29 "@emptystream":: "'a fstream" ("<>") |
|
30 "@fsfilter" :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_'(C')_)" [64,63] 63) |
|
31 |
|
32 syntax (xsymbols) |
|
33 |
|
34 "@fsfilter" :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)" |
|
35 [64,63] 63) |
|
36 translations |
|
37 |
|
38 "<>" => "\<bottom>" |
|
39 "A(C)s" == "fsfilter A\<cdot>s" |
|
40 |
|
41 defs |
|
42 |
|
43 fsingleton_def2: "fsingleton == %a. Def a && UU" |
|
44 |
|
45 jth_def: "jth == %n s. if Fin n < #s then THE a. i_th n s = Def a else arbitrary" |
|
46 |
|
47 first_def: "first == %s. jth 0 s" |
|
48 last_def: "last == %s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else arbitrary) |
|
49 | Infty => arbitrary" |
|
50 |
|
51 fsfilter_def: "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))" |
|
52 fsmap_def: "fsmap f == smap$(flift2 f)" |
|
53 |
|
54 |
|
55 lemma ft_fsingleton[simp]: "ft$(<a>) = Def a" |
|
56 by (simp add: fsingleton_def2) |
|
57 |
|
58 lemma slen_fsingleton[simp]: "#(<a>) = Fin 1" |
|
59 by (simp add: fsingleton_def2 inat_defs) |
|
60 |
|
61 lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)" |
|
62 by (simp add: fsingleton_def2) |
|
63 |
|
64 lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)" |
|
65 apply (case_tac "#s", auto) |
|
66 apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto) |
|
67 by (simp add: sconc_def) |
|
68 |
|
69 lemma j_th_0_fsingleton[simp]:"jth 0 (<a>) = a" |
|
70 apply (simp add: fsingleton_def2 jth_def) |
|
71 by (simp add: i_th_def Fin_0) |
|
72 |
|
73 lemma jth_0[simp]: "jth 0 (<a> ooo s) = a" |
|
74 apply (simp add: fsingleton_def2 jth_def) |
|
75 by (simp add: i_th_def Fin_0) |
|
76 |
|
77 lemma first_sconc[simp]: "first (<a> ooo s) = a" |
|
78 by (simp add: first_def) |
|
79 |
|
80 lemma first_fsingleton[simp]: "first (<a>) = a" |
|
81 by (simp add: first_def) |
|
82 |
|
83 lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a" |
|
84 apply (simp add: jth_def, auto) |
|
85 apply (simp add: i_th_def rt_sconc1) |
|
86 by (simp add: inat_defs split: inat_splits) |
|
87 |
|
88 lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a" |
|
89 apply (simp add: last_def) |
|
90 apply (simp add: inat_defs split:inat_splits) |
|
91 by (drule sym, auto) |
|
92 |
|
93 lemma last_fsingleton[simp]: "last (<a>) = a" |
|
94 by (simp add: last_def) |
|
95 |
|
96 lemma first_UU[simp]: "first UU = arbitrary" |
|
97 by (simp add: first_def jth_def) |
|
98 |
|
99 lemma last_UU[simp]:"last UU = arbitrary" |
|
100 by (simp add: last_def jth_def inat_defs) |
|
101 |
|
102 lemma last_infinite[simp]:"#s = Infty ==> last s = arbitrary" |
|
103 by (simp add: last_def) |
|
104 |
|
105 lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = arbitrary" |
|
106 by (simp add: jth_def inat_defs split:inat_splits, auto) |
|
107 |
|
108 lemma jth_UU[simp]:"jth n UU = arbitrary" |
|
109 by (simp add: jth_def) |
|
110 |
|
111 lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s" |
|
112 apply (simp add: last_def) |
|
113 apply (case_tac "#s", auto) |
|
114 apply (simp add: fsingleton_def2) |
|
115 apply (subgoal_tac "Def (jth n s) = i_th n s") |
|
116 apply (auto simp add: i_th_last) |
|
117 apply (drule slen_take_lemma1, auto) |
|
118 apply (simp add: jth_def) |
|
119 apply (case_tac "i_th n s = UU") |
|
120 apply auto |
|
121 apply (simp add: i_th_def) |
|
122 apply (case_tac "i_rt n s = UU", auto) |
|
123 apply (drule i_rt_slen [THEN iffD1]) |
|
124 apply (drule slen_take_eq_rev [rule_format, THEN iffD2],auto) |
|
125 by (drule not_Undef_is_Def [THEN iffD1], auto) |
|
126 |
|
127 |
|
128 lemma fsingleton_lemma1[simp]: "(<a> = <b>) = (a=b)" |
|
129 by (simp add: fsingleton_def2) |
|
130 |
|
131 lemma fsingleton_lemma2[simp]: "<a> ~= <>" |
|
132 by (simp add: fsingleton_def2) |
|
133 |
|
134 lemma fsingleton_sconc:"<a> ooo s = Def a && s" |
|
135 by (simp add: fsingleton_def2) |
|
136 |
|
137 lemma fstreams_ind: |
|
138 "[| adm P; P <>; !!a s. P s ==> P (<a> ooo s) |] ==> P x" |
|
139 apply (simp add: fsingleton_def2) |
|
140 apply (rule stream.ind, auto) |
|
141 by (drule not_Undef_is_Def [THEN iffD1], auto) |
|
142 |
|
143 lemma fstreams_ind2: |
|
144 "[| adm P; P <>; !!a. P (<a>); !!a b s. P s ==> P (<a> ooo <b> ooo s) |] ==> P x" |
|
145 apply (simp add: fsingleton_def2) |
|
146 apply (rule stream_ind2, auto) |
|
147 by (drule not_Undef_is_Def [THEN iffD1], auto)+ |
|
148 |
|
149 lemma fstreams_take_Suc[simp]: "stream_take (Suc n)$(<a> ooo s) = <a> ooo stream_take n$s" |
|
150 by (simp add: fsingleton_def2) |
|
151 |
|
152 lemma fstreams_not_empty[simp]: "<a> ooo s ~= <>" |
|
153 by (simp add: fsingleton_def2) |
|
154 |
|
155 lemma fstreams_not_empty2[simp]: "s ooo <a> ~= <>" |
|
156 by (case_tac "s=UU", auto) |
|
157 |
|
158 lemma fstreams_exhaust: "x = UU | (EX a s. x = <a> ooo s)" |
|
159 apply (simp add: fsingleton_def2, auto) |
|
160 apply (erule contrapos_pp, auto) |
|
161 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
|
162 by (drule not_Undef_is_Def [THEN iffD1], auto) |
|
163 |
|
164 lemma fstreams_cases: "[| x = UU ==> P; !!a y. x = <a> ooo y ==> P |] ==> P" |
|
165 by (insert fstreams_exhaust [of x], auto) |
|
166 |
|
167 lemma fstreams_exhaust_eq: "(x ~= UU) = (? a y. x = <a> ooo y)" |
|
168 apply (simp add: fsingleton_def2, auto) |
|
169 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
|
170 by (drule not_Undef_is_Def [THEN iffD1], auto) |
|
171 |
|
172 lemma fstreams_inject: "(<a> ooo s = <b> ooo t) = (a=b & s=t)" |
|
173 by (simp add: fsingleton_def2) |
|
174 |
|
175 lemma fstreams_prefix: "<a> ooo s << t ==> EX tt. t = <a> ooo tt & s << tt" |
|
176 apply (simp add: fsingleton_def2) |
|
177 apply (insert stream_prefix [of "Def a" s t], auto) |
|
178 by (drule stream.inverts, auto) |
|
179 |
|
180 lemma fstreams_prefix': "x << <a> ooo z = (x = <> | (EX y. x = <a> ooo y & y << z))" |
|
181 apply (auto, case_tac "x=UU", auto) |
|
182 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
|
183 apply (simp add: fsingleton_def2, auto) |
|
184 apply (drule stream.inverts, auto) |
|
185 apply (drule ax_flat [rule_format], simp) |
|
186 apply (drule stream.inverts, auto) |
|
187 by (erule sconc_mono) |
|
188 |
|
189 lemma ft_fstreams[simp]: "ft$(<a> ooo s) = Def a" |
|
190 by (simp add: fsingleton_def2) |
|
191 |
|
192 lemma rt_fstreams[simp]: "rt$(<a> ooo s) = s" |
|
193 by (simp add: fsingleton_def2) |
|
194 |
|
195 lemma ft_eq[simp]: "(ft$s = Def a) = (EX t. s = <a> ooo t)" |
|
196 apply (rule stream.casedist [of s],auto) |
|
197 by (drule sym, auto simp add: fsingleton_def2) |
|
198 |
|
199 lemma surjective_fstreams: "(<d> ooo y = x) = (ft$x = Def d & rt$x = y)" |
|
200 by auto |
|
201 |
|
202 lemma fstreams_mono: "<a> ooo b << <a> ooo c ==> b << c" |
|
203 apply (simp add: fsingleton_def2) |
|
204 by (drule stream.inverts, auto) |
|
205 |
|
206 lemma fsmap_UU[simp]: "fsmap f$UU = UU" |
|
207 by (simp add: fsmap_def) |
|
208 |
|
209 lemma fsmap_fsingleton_sconc: "fsmap f$(<x> ooo xs) = <(f x)> ooo (fsmap f$xs)" |
|
210 by (simp add: fsmap_def fsingleton_def2 flift2_def) |
|
211 |
|
212 lemma fsmap_fsingleton[simp]: "fsmap f$(<x>) = <(f x)>" |
|
213 by (simp add: fsmap_def fsingleton_def2 flift2_def) |
|
214 |
|
215 |
|
216 declare range_composition[simp del] |
|
217 |
|
218 |
|
219 lemma fstreams_chain_lemma[rule_format]: |
|
220 "ALL s x y. stream_take n$(s::'a fstream) << x & x << y & y << s & x ~= y --> stream_take (Suc n)$s << y" |
|
221 apply (induct_tac n, auto) |
|
222 apply (case_tac "s=UU", auto) |
|
223 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
|
224 apply (case_tac "y=UU", auto) |
|
225 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
|
226 apply (drule stream.inverts, auto) |
|
227 apply (simp add: less_lift_def, auto) |
|
228 apply (rule monofun_cfun, auto) |
|
229 apply (case_tac "s=UU", auto) |
|
230 apply (drule stream_exhaust_eq [THEN iffD1], auto) |
|
231 apply (erule_tac x="ya" in allE) |
|
232 apply (drule stream_prefix, auto) |
|
233 apply (case_tac "y=UU",auto) |
|
234 apply (drule stream_exhaust_eq [THEN iffD1], clarsimp) |
|
235 apply (drule stream.inverts, auto) |
|
236 apply (simp add: less_lift_def) |
|
237 apply (drule stream.inverts, auto)+ |
|
238 apply (erule_tac x="tt" in allE) |
|
239 apply (erule_tac x="yb" in allE, auto) |
|
240 apply (simp add: less_lift_def) |
|
241 by (rule monofun_cfun, auto) |
|
242 |
|
243 lemma fstreams_lub_lemma1: "[| chain Y; lub (range Y) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t" |
|
244 apply (subgoal_tac "lub(range Y) ~= UU") |
|
245 apply (drule chain_UU_I_inverse2, auto) |
|
246 apply (drule_tac x="i" in is_ub_thelub, auto) |
|
247 by (drule fstreams_prefix' [THEN iffD1], auto) |
|
248 |
|
249 lemma fstreams_lub1: |
|
250 "[| chain Y; lub (range Y) = <a> ooo s |] |
|
251 ==> (EX j t. Y j = <a> ooo t) & (EX X. chain X & (ALL i. EX j. <a> ooo X i << Y j) & lub (range X) = s)" |
|
252 apply (auto simp add: fstreams_lub_lemma1) |
|
253 apply (rule_tac x="%n. stream_take n$s" in exI, auto) |
|
254 apply (simp add: chain_stream_take) |
|
255 apply (induct_tac i, auto) |
|
256 apply (drule fstreams_lub_lemma1, auto) |
|
257 apply (rule_tac x="j" in exI, auto) |
|
258 apply (case_tac "max_in_chain j Y") |
|
259 apply (frule lub_finch1 [THEN thelubI], auto) |
|
260 apply (rule_tac x="j" in exI) |
|
261 apply (erule subst) back back |
|
262 apply (simp add: less_cprod_def sconc_mono) |
|
263 apply (simp add: max_in_chain_def, auto) |
|
264 apply (rule_tac x="ja" in exI) |
|
265 apply (subgoal_tac "Y j << Y ja") |
|
266 apply (drule fstreams_prefix, auto)+ |
|
267 apply (rule sconc_mono) |
|
268 apply (rule fstreams_chain_lemma, auto) |
|
269 apply (subgoal_tac "Y ja << (LUB i. (Y i))", clarsimp) |
|
270 apply (drule fstreams_mono, simp) |
|
271 apply (rule is_ub_thelub, simp) |
|
272 apply (blast intro: chain_mono3) |
|
273 by (rule stream_reach2) |
|
274 |
|
275 |
|
276 lemma lub_Pair_not_UU_lemma: |
|
277 "[| chain Y; lub (range Y) = ((a::'a::flat), b); a ~= UU; b ~= UU |] |
|
278 ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU" |
|
279 apply (frule thelub_cprod, clarsimp) |
|
280 apply (drule chain_UU_I_inverse2, clarsimp) |
|
281 apply (case_tac "Y i", clarsimp) |
|
282 apply (case_tac "max_in_chain i Y") |
|
283 apply (drule maxinch_is_thelub, auto) |
|
284 apply (rule_tac x="i" in exI, auto) |
|
285 apply (simp add: max_in_chain_def, auto) |
|
286 apply (subgoal_tac "Y i << Y j",auto) |
|
287 apply (simp add: less_cprod_def, clarsimp) |
|
288 apply (drule ax_flat [rule_format], auto) |
|
289 apply (case_tac "snd (Y j) = UU",auto) |
|
290 apply (case_tac "Y j", auto) |
|
291 apply (rule_tac x="j" in exI) |
|
292 apply (case_tac "Y j",auto) |
|
293 by (drule chain_mono3, auto) |
|
294 |
|
295 lemma fstreams_lub_lemma2: |
|
296 "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)" |
|
297 apply (frule lub_Pair_not_UU_lemma, auto) |
|
298 apply (drule_tac x="j" in is_ub_thelub, auto) |
|
299 apply (simp add: less_cprod_def, clarsimp) |
|
300 apply (drule ax_flat [rule_format], clarsimp) |
|
301 by (drule fstreams_prefix' [THEN iffD1], auto) |
|
302 |
|
303 lemma fstreams_lub2: |
|
304 "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] |
|
305 ==> (EX j t. Y j = (a, <m> ooo t)) & (EX X. chain X & (ALL i. EX j. (a, <m> ooo X i) << Y j) & lub (range X) = ms)" |
|
306 apply (auto simp add: fstreams_lub_lemma2) |
|
307 apply (rule_tac x="%n. stream_take n$ms" in exI, auto) |
|
308 apply (simp add: chain_stream_take) |
|
309 apply (induct_tac i, auto) |
|
310 apply (drule fstreams_lub_lemma2, auto) |
|
311 apply (rule_tac x="j" in exI, auto) |
|
312 apply (simp add: less_cprod_def) |
|
313 apply (case_tac "max_in_chain j Y") |
|
314 apply (frule lub_finch1 [THEN thelubI], auto) |
|
315 apply (rule_tac x="j" in exI) |
|
316 apply (erule subst) back back |
|
317 apply (simp add: less_cprod_def sconc_mono) |
|
318 apply (simp add: max_in_chain_def, auto) |
|
319 apply (rule_tac x="ja" in exI) |
|
320 apply (subgoal_tac "Y j << Y ja") |
|
321 apply (simp add: less_cprod_def, auto) |
|
322 apply (drule trans_less) |
|
323 apply (simp add: ax_flat, auto) |
|
324 apply (drule fstreams_prefix, auto)+ |
|
325 apply (rule sconc_mono) |
|
326 apply (subgoal_tac "tt ~= tta" "tta << ms") |
|
327 apply (blast intro: fstreams_chain_lemma) |
|
328 apply (frule lub_cprod [THEN thelubI], auto) |
|
329 apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp) |
|
330 apply (drule fstreams_mono, simp) |
|
331 apply (rule is_ub_thelub chainI) |
|
332 apply (simp add: chain_def less_cprod_def) |
|
333 apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp) |
|
334 apply (drule ax_flat[rule_format], simp)+ |
|
335 apply (drule prod_eqI, auto) |
|
336 apply (simp add: chain_mono3) |
|
337 by (rule stream_reach2) |
|
338 |
|
339 |
|
340 lemma cpo_cont_lemma: |
|
341 "[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f" |
|
342 apply (rule monocontlub2cont, auto) |
|
343 apply (simp add: contlub, auto) |
|
344 apply (erule_tac x="Y" in allE, auto) |
|
345 apply (simp add: po_eq_conv) |
|
346 apply (frule cpo,auto) |
|
347 apply (frule is_lubD1) |
|
348 apply (frule ub2ub_monofun, auto) |
|
349 apply (drule thelubI, auto) |
|
350 apply (rule is_lub_thelub, auto) |
|
351 by (erule ch2ch_monofun, simp) |
|
352 |
|
353 end |
|
354 |
|
355 |
|
356 |
|
357 |