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