1(*  Title:      HOL/HOLCF/FOCUS/Fstream.thy
2    Author:     David von Oheimb, TU Muenchen
3
4FOCUS streams (with lifted elements).
5
6TODO: integrate Fstreams.thy
7*)
8
9section \<open>FOCUS flat streams\<close>
10
11theory Fstream
12imports "HOLCF-Library.Stream"
13begin
14
15default_sort type
16
17type_synonym 'a fstream = "'a lift stream"
18
19definition
20  fscons        :: "'a     \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
21  "fscons a = (\<Lambda> s. Def a && s)"
22
23definition
24  fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream" where
25  "fsfilter A = (sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A)))"
26
27abbreviation
28  emptystream   :: "'a fstream"                          ("<>") where
29  "<> == \<bottom>"
30
31abbreviation
32  fscons'       :: "'a \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"       ("(_\<leadsto>_)" [66,65] 65) where
33  "a\<leadsto>s == fscons a\<cdot>s"
34
35abbreviation
36  fsfilter'     :: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"   ("(_\<copyright>_)" [64,63] 63) where
37  "A\<copyright>s == fsfilter A\<cdot>s"
38
39notation (ASCII)
40  fscons'  ("(_~>_)" [66,65] 65) and
41  fsfilter'  ("(_'(C')_)" [64,63] 63)
42
43
44lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d"
45by simp
46
47
48section "fscons"
49
50lemma fscons_def2: "a~>s = Def a && s"
51apply (unfold fscons_def)
52apply (simp)
53done
54
55lemma fstream_exhaust: "x = UU \<or> (\<exists>a y. x = a~> y)"
56apply (simp add: fscons_def2)
57apply (cut_tac stream.nchotomy)
58apply (fast dest: not_Undef_is_Def [THEN iffD1])
59done
60
61lemma fstream_cases: "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P"
62apply (cut_tac fstream_exhaust)
63apply (erule disjE)
64apply fast
65apply fast
66done
67
68lemma fstream_exhaust_eq: "(x \<noteq> UU) = (\<exists>a y. x = a~> y)"
69apply (simp add: fscons_def2 stream_exhaust_eq)
70apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
71done
72
73
74lemma fscons_not_empty [simp]: "a~> s \<noteq> <>"
75by (simp add: fscons_def2)
76
77
78lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b \<and> s = t)"
79by (simp add: fscons_def2)
80
81lemma fstream_prefix: "a~> s << t ==> \<exists>tt. t = a~> tt \<and> s << tt"
82apply (cases t)
83apply (cut_tac fscons_not_empty)
84apply (fast dest: bottomI)
85apply (simp add: fscons_def2)
86done
87
88lemma fstream_prefix' [simp]:
89        "x << a~> z = (x = <> \<or> (\<exists>y. x = a~> y \<and> y << z))"
90apply (simp add: fscons_def2 lift.distinct(2) [THEN stream_prefix'])
91apply (safe)
92apply (erule_tac [!] contrapos_np)
93prefer 2 apply (fast elim: DefE)
94apply (rule lift.exhaust)
95apply (erule (1) notE)
96apply (safe)
97apply (drule Def_below_Def [THEN iffD1])
98apply fast
99done
100
101(* ------------------------------------------------------------------------- *)
102
103section "ft & rt"
104
105lemmas ft_empty = stream.sel_rews (1)
106lemma ft_fscons [simp]: "ft\<cdot>(m~> s) = Def m"
107by (simp add: fscons_def)
108
109lemmas rt_empty = stream.sel_rews (2)
110lemma rt_fscons [simp]: "rt\<cdot>(m~> s) = s"
111by (simp add: fscons_def)
112
113lemma ft_eq [simp]: "(ft\<cdot>s = Def a) = (\<exists>t. s = a~> t)"
114apply (unfold fscons_def)
115apply (simp)
116apply (safe)
117apply (erule subst)
118apply (rule exI)
119apply (rule surjectiv_scons [symmetric])
120apply (simp)
121done
122
123lemma surjective_fscons_lemma: "(d\<leadsto>y = x) = (ft\<cdot>x = Def d & rt\<cdot>x = y)"
124by auto
125
126lemma surjective_fscons: "ft\<cdot>x = Def d \<Longrightarrow> d\<leadsto>rt\<cdot>x = x"
127by (simp add: surjective_fscons_lemma)
128
129
130(* ------------------------------------------------------------------------- *)
131
132section "take"
133
134lemma fstream_take_Suc [simp]:
135        "stream_take (Suc n)\<cdot>(a~> s) = a~> stream_take n\<cdot>s"
136by (simp add: fscons_def)
137
138
139(* ------------------------------------------------------------------------- *)
140
141section "slen"
142
143lemma slen_fscons: "#(m~> s) = eSuc (#s)"
144by (simp add: fscons_def)
145
146lemma slen_fscons_eq:
147        "(enat (Suc n) < #x) = (\<exists>a y. x = a~> y \<and> enat n < #y)"
148apply (simp add: fscons_def2 slen_scons_eq)
149apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
150done
151
152lemma slen_fscons_eq_rev:
153        "(#x < enat (Suc (Suc n))) = (\<forall>a y. x \<noteq> a~> y \<or> #y < enat (Suc n))"
154apply (simp add: fscons_def2 slen_scons_eq_rev)
155apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>)
156apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>)
157apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>)
158apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>)
159apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>)
160apply (tactic \<open>step_tac (put_claset HOL_cs \<^context> addSEs @{thms DefE}) 1\<close>)
161apply (erule contrapos_np)
162apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
163done
164
165lemma slen_fscons_less_eq:
166        "(#(a~> y) < enat (Suc (Suc n))) = (#y < enat (Suc n))"
167apply (subst slen_fscons_eq_rev)
168apply (fast dest!: fscons_inject [THEN iffD1])
169done
170
171
172(* ------------------------------------------------------------------------- *)
173
174section "induction"
175
176lemma fstream_ind:
177        "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x"
178apply (erule stream.induct)
179apply (assumption)
180apply (unfold fscons_def2)
181apply (fast dest: not_Undef_is_Def [THEN iffD1])
182done
183
184lemma fstream_ind2:
185  "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x"
186apply (erule stream_ind2)
187apply (assumption)
188apply (unfold fscons_def2)
189apply (fast dest: not_Undef_is_Def [THEN iffD1])
190apply (fast dest: not_Undef_is_Def [THEN iffD1])
191done
192
193
194(* ------------------------------------------------------------------------- *)
195
196section "fsfilter"
197
198lemma fsfilter_empty: "A(C)UU = UU"
199apply (unfold fsfilter_def)
200apply (rule sfilter_empty)
201done
202
203lemma fsfilter_fscons:
204        "A(C)x~> xs = (if x\<in>A then x~> (A(C)xs) else A(C)xs)"
205apply (unfold fsfilter_def)
206apply (simp add: fscons_def2 If_and_if)
207done
208
209lemma fsfilter_emptys: "{}(C)x = UU"
210apply (rule_tac x="x" in fstream_ind)
211apply (simp)
212apply (rule fsfilter_empty)
213apply (simp add: fsfilter_fscons)
214done
215
216lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)"
217by (simp add: fsfilter_fscons)
218
219lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)"
220by (rule fsfilter_insert)
221
222lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)"
223by (simp add: fsfilter_fscons)
224
225lemma fstream_lub_lemma1:
226    "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t"
227apply (case_tac "max_in_chain i Y")
228apply  (drule (1) lub_finch1 [THEN lub_eqI, THEN sym])
229apply  (force)
230apply (unfold max_in_chain_def)
231apply auto
232apply (frule (1) chain_mono)
233apply (rule_tac x="Y j" in fstream_cases)
234apply  (force)
235apply (drule_tac x="j" in is_ub_thelub)
236apply (force)
237done
238
239lemma fstream_lub_lemma:
240      "\<lbrakk>chain Y; (\<Squnion>i. Y i) = a\<leadsto>s\<rbrakk> \<Longrightarrow> (\<exists>j t. Y j = a\<leadsto>t) \<and> (\<exists>X. chain X \<and> (\<forall>i. \<exists>j. Y j = a\<leadsto>X i) \<and> (\<Squnion>i. X i) = s)"
241apply (frule (1) fstream_lub_lemma1)
242apply (clarsimp)
243apply (rule_tac x="\<lambda>i. rt\<cdot>(Y(i+j))" in exI)
244apply (rule conjI)
245apply  (erule chain_shift [THEN chain_monofun])
246apply safe
247apply  (drule_tac i="j" and j="i+j" in chain_mono)
248apply   (simp)
249apply  (simp)
250apply  (rule_tac x="i+j" in exI)
251apply  (drule fstream_prefix)
252apply  (clarsimp)
253apply  (subst lub_APP)
254apply   (rule chainI)
255apply   (fast)
256apply  (erule chain_shift)
257apply (subst lub_const)
258apply (subst lub_range_shift)
259apply  (assumption)
260apply (simp)
261done
262
263end
264