44 fscons_def: "fscons a \<equiv> \<Lambda> s. Def a && s" |
44 fscons_def: "fscons a \<equiv> \<Lambda> s. Def a && s" |
45 fsfilter_def: "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))" |
45 fsfilter_def: "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))" |
46 |
46 |
47 ML {* use_legacy_bindings (the_context ()) *} |
47 ML {* use_legacy_bindings (the_context ()) *} |
48 |
48 |
|
49 lemma Def_maximal: "a = Def d \<Longrightarrow> a\<sqsubseteq>b \<Longrightarrow> b = Def d" |
|
50 apply (rule flat_eq [THEN iffD1, symmetric]) |
|
51 apply (rule Def_not_UU) |
|
52 apply (drule antisym_less_inverse) |
|
53 apply (erule (1) conjunct2 [THEN trans_less]) |
|
54 done |
|
55 |
|
56 |
|
57 section "fscons" |
|
58 |
|
59 lemma fscons_def2: "a~>s = Def a && s" |
|
60 apply (unfold fscons_def) |
|
61 apply (simp) |
|
62 done |
|
63 |
|
64 lemma fstream_exhaust: "x = UU | (? a y. x = a~> y)" |
|
65 apply (simp add: fscons_def2) |
|
66 apply (cut_tac stream.exhaust) |
|
67 apply (fast dest: not_Undef_is_Def [THEN iffD1]) |
|
68 done |
|
69 |
|
70 lemma fstream_cases: "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P" |
|
71 apply (cut_tac fstream_exhaust) |
|
72 apply (erule disjE) |
|
73 apply fast |
|
74 apply fast |
|
75 done |
|
76 (* |
|
77 fun fstream_case_tac s i = res_inst_tac [("x",s)] fstream_cases i |
|
78 THEN hyp_subst_tac i THEN hyp_subst_tac (i+1); |
|
79 *) |
|
80 lemma fstream_exhaust_eq: "(x ~= UU) = (? a y. x = a~> y)" |
|
81 apply (simp add: fscons_def2 stream_exhaust_eq) |
|
82 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
|
83 done |
|
84 |
|
85 |
|
86 lemma fscons_not_empty [simp]: "a~> s ~= <>" |
|
87 by (simp add: fscons_def2) |
|
88 |
|
89 |
|
90 lemma fscons_inject [simp]: "(a~> s = b~> t) = (a = b & s = t)" |
|
91 by (simp add: fscons_def2) |
|
92 |
|
93 lemma fstream_prefix: "a~> s << t ==> ? tt. t = a~> tt & s << tt" |
|
94 apply (rule_tac x="t" in stream.casedist) |
|
95 apply (cut_tac fscons_not_empty) |
|
96 apply (fast dest: eq_UU_iff [THEN iffD2]) |
|
97 apply (simp add: fscons_def2) |
|
98 apply (drule stream_flat_prefix) |
|
99 apply (rule Def_not_UU) |
|
100 apply (fast) |
|
101 done |
|
102 |
|
103 lemma fstream_prefix' [simp]: |
|
104 "x << a~> z = (x = <> | (? y. x = a~> y & y << z))" |
|
105 apply (simp add: fscons_def2 Def_not_UU [THEN stream_prefix']) |
|
106 apply (safe) |
|
107 apply (erule_tac [!] contrapos_np) |
|
108 prefer 2 apply (fast elim: DefE) |
|
109 apply (rule Lift_cases) |
|
110 apply (erule (1) notE) |
|
111 apply (safe) |
|
112 apply (drule Def_inject_less_eq [THEN iffD1]) |
|
113 apply fast |
|
114 done |
|
115 |
|
116 (* ------------------------------------------------------------------------- *) |
|
117 |
|
118 section "ft & rt" |
|
119 |
|
120 lemmas ft_empty = stream.sel_rews (1) |
|
121 lemma ft_fscons [simp]: "ft\<cdot>(m~> s) = Def m" |
|
122 by (simp add: fscons_def) |
|
123 |
|
124 lemmas rt_empty = stream.sel_rews (2) |
|
125 lemma rt_fscons [simp]: "rt\<cdot>(m~> s) = s" |
|
126 by (simp add: fscons_def) |
|
127 |
|
128 lemma ft_eq [simp]: "(ft\<cdot>s = Def a) = (? t. s = a~> t)" |
|
129 apply (unfold fscons_def) |
|
130 apply (simp) |
|
131 apply (safe) |
|
132 apply (erule subst) |
|
133 apply (rule exI) |
|
134 apply (rule surjectiv_scons [symmetric]) |
|
135 apply (simp) |
|
136 done |
|
137 |
|
138 lemma surjective_fscons_lemma: "(d\<leadsto>y = x) = (ft\<cdot>x = Def d & rt\<cdot>x = y)" |
|
139 by auto |
|
140 |
|
141 lemma surjective_fscons: "ft\<cdot>x = Def d \<Longrightarrow> d\<leadsto>rt\<cdot>x = x" |
|
142 by (simp add: surjective_fscons_lemma) |
|
143 |
|
144 |
|
145 (* ------------------------------------------------------------------------- *) |
|
146 |
|
147 section "take" |
|
148 |
|
149 lemma fstream_take_Suc [simp]: |
|
150 "stream_take (Suc n)\<cdot>(a~> s) = a~> stream_take n\<cdot>s" |
|
151 by (simp add: fscons_def) |
|
152 |
|
153 |
|
154 (* ------------------------------------------------------------------------- *) |
|
155 |
|
156 section "slen" |
|
157 |
|
158 (*bind_thm("slen_empty", slen_empty);*) |
|
159 |
|
160 lemma slen_fscons: "#(m~> s) = iSuc (#s)" |
|
161 by (simp add: fscons_def) |
|
162 |
|
163 lemma slen_fscons_eq: |
|
164 "(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" |
|
165 apply (simp add: fscons_def2 slen_scons_eq) |
|
166 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
|
167 done |
|
168 |
|
169 lemma slen_fscons_eq_rev: |
|
170 "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" |
|
171 apply (simp add: fscons_def2 slen_scons_eq_rev) |
|
172 apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") |
|
173 apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") |
|
174 apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") |
|
175 apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") |
|
176 apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") |
|
177 apply (tactic "step_tac (HOL_cs addSEs [DefE]) 1") |
|
178 apply (erule contrapos_np) |
|
179 apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) |
|
180 done |
|
181 |
|
182 lemma slen_fscons_less_eq: |
|
183 "(#(a~> y) < Fin (Suc (Suc n))) = (#y < Fin (Suc n))" |
|
184 apply (subst slen_fscons_eq_rev) |
|
185 apply (fast dest!: fscons_inject [THEN iffD1]) |
|
186 done |
|
187 |
|
188 |
|
189 (* ------------------------------------------------------------------------- *) |
|
190 |
|
191 section "induction" |
|
192 |
|
193 lemma fstream_ind: |
|
194 "[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" |
|
195 apply (erule stream.ind) |
|
196 apply (assumption) |
|
197 apply (unfold fscons_def2) |
|
198 apply (fast dest: not_Undef_is_Def [THEN iffD1]) |
|
199 done |
|
200 |
|
201 lemma fstream_ind2: |
|
202 "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x" |
|
203 apply (erule stream_ind2) |
|
204 apply (assumption) |
|
205 apply (unfold fscons_def2) |
|
206 apply (fast dest: not_Undef_is_Def [THEN iffD1]) |
|
207 apply (fast dest: not_Undef_is_Def [THEN iffD1]) |
|
208 done |
|
209 |
|
210 |
|
211 (* ------------------------------------------------------------------------- *) |
|
212 |
|
213 section "fsfilter" |
|
214 |
|
215 lemma fsfilter_empty: "A(C)UU = UU" |
|
216 apply (unfold fsfilter_def) |
|
217 apply (rule sfilter_empty) |
|
218 done |
|
219 |
|
220 lemma fsfilter_fscons: |
|
221 "A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" |
|
222 apply (unfold fsfilter_def) |
|
223 apply (simp add: fscons_def2 sfilter_scons If_and_if) |
|
224 done |
|
225 |
|
226 lemma fsfilter_emptys: "{}(C)x = UU" |
|
227 apply (rule_tac x="x" in fstream_ind) |
|
228 apply (simp) |
|
229 apply (rule fsfilter_empty) |
|
230 apply (simp add: fsfilter_fscons) |
|
231 done |
|
232 |
|
233 lemma fsfilter_insert: "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" |
|
234 by (simp add: fsfilter_fscons) |
|
235 |
|
236 lemma fsfilter_single_in: "{a}(C)a~> x = a~> ({a}(C)x)" |
|
237 by (rule fsfilter_insert) |
|
238 |
|
239 lemma fsfilter_single_out: "b ~= a ==> {a}(C)b~> x = ({a}(C)x)" |
|
240 by (simp add: fsfilter_fscons) |
|
241 |
|
242 lemma fstream_lub_lemma1: |
|
243 "\<lbrakk>chain Y; lub (range Y) = a\<leadsto>s\<rbrakk> \<Longrightarrow> \<exists>j t. Y j = a\<leadsto>t" |
|
244 apply (case_tac "max_in_chain i Y") |
|
245 apply (drule (1) lub_finch1 [THEN thelubI, THEN sym]) |
|
246 apply (force) |
|
247 apply (unfold max_in_chain_def) |
|
248 apply auto |
|
249 apply (frule (1) chain_mono3) |
|
250 apply (rule_tac x="Y j" in fstream_cases) |
|
251 apply (force) |
|
252 apply (drule_tac x="j" in is_ub_thelub) |
|
253 apply (force) |
|
254 done |
|
255 |
|
256 lemma fstream_lub_lemma: |
|
257 "\<lbrakk>chain Y; lub (range Y) = a\<leadsto>s\<rbrakk> \<Longrightarrow> (\<exists>j t. Y j = a\<leadsto>t) & (\<exists>X. chain X & (!i. ? j. Y j = a\<leadsto>X i) & lub (range X) = s)" |
|
258 apply (frule (1) fstream_lub_lemma1) |
|
259 apply (clarsimp) |
|
260 apply (rule_tac x="%i. rt\<cdot>(Y(i+j))" in exI) |
|
261 apply (rule conjI) |
|
262 apply (erule chain_shift [THEN chain_monofun]) |
|
263 apply safe |
|
264 apply (drule_tac x="j" and y="i+j" in chain_mono3) |
|
265 apply (simp) |
|
266 apply (simp) |
|
267 apply (rule_tac x="i+j" in exI) |
|
268 apply (drule fstream_prefix) |
|
269 apply (clarsimp) |
|
270 apply (subst contlub_cfun [symmetric]) |
|
271 apply (rule chainI) |
|
272 apply (fast) |
|
273 apply (erule chain_shift) |
|
274 apply (subst lub_const [THEN thelubI]) |
|
275 apply (subst lub_range_shift) |
|
276 apply (assumption) |
|
277 apply (simp) |
|
278 done |
|
279 |
49 end |
280 end |