|
1 (* Title: FOCUS/Stream.ML |
|
2 ID: $ $ |
|
3 Author: Franz Regensburger, David von Oheimb |
|
4 Copyright 1993, 1995 Technische Universitaet Muenchen |
|
5 |
|
6 Theorems for Stream.thy |
|
7 *) |
|
8 |
|
9 open Stream; |
|
10 |
|
11 fun stream_case_tac s i = res_inst_tac [("x",s)] stream.cases i |
|
12 THEN hyp_subst_tac i THEN hyp_subst_tac (i+1); |
|
13 |
|
14 |
|
15 (* ----------------------------------------------------------------------- *) |
|
16 (* theorems about scons *) |
|
17 (* ----------------------------------------------------------------------- *) |
|
18 |
|
19 section "scons"; |
|
20 |
|
21 qed_goal "scons_eq_UU" thy "a && s = UU = (a = UU)" (fn _ => [ |
|
22 safe_tac HOL_cs, |
|
23 etac contrapos2 1, |
|
24 safe_tac (HOL_cs addSIs stream.con_rews)]); |
|
25 |
|
26 qed_goal "scons_not_empty" thy "[| a && x = UU; a ~= UU |] ==> R" (fn prems => [ |
|
27 cut_facts_tac prems 1, |
|
28 dresolve_tac stream.con_rews 1, |
|
29 contr_tac 1]); |
|
30 |
|
31 qed_goal "stream_exhaust_eq" thy "x ~= UU = (? a y. a ~= UU & x = a && y)" (fn _ =>[ |
|
32 cut_facts_tac [stream.exhaust] 1, |
|
33 safe_tac HOL_cs, |
|
34 contr_tac 1, |
|
35 fast_tac (HOL_cs addDs (tl stream.con_rews)) 1, |
|
36 fast_tac HOL_cs 1, |
|
37 fast_tac (HOL_cs addDs (tl stream.con_rews)) 1]); |
|
38 |
|
39 qed_goal "stream_prefix" thy |
|
40 "[| a && s << t; a ~= UU |] ==> ? b tt. t = b && tt & b ~= UU & s << tt" (fn prems => [ |
|
41 cut_facts_tac prems 1, |
|
42 stream_case_tac "t" 1, |
|
43 fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2,hd (tl stream.con_rews)]) 1, |
|
44 fast_tac (HOL_cs addDs stream.inverts) 1]); |
|
45 |
|
46 qed_goal "stream_flat_prefix" thy |
|
47 "[| x && xs << y && ys; (x::'a) ~= UU; flat (z::'a) |] ==> x = y & xs << ys"(fn prems=>[ |
|
48 cut_facts_tac prems 1, |
|
49 (forward_tac stream.inverts 1), |
|
50 (safe_tac HOL_cs), |
|
51 (dtac (hd stream.con_rews RS subst) 1), |
|
52 (fast_tac (HOL_cs addDs ((eq_UU_iff RS iffD2)::stream.con_rews)) 1), |
|
53 (rewtac flat_def), |
|
54 (fast_tac HOL_cs 1)]); |
|
55 |
|
56 qed_goal "stream_prefix'" thy "b ~= UU ==> x << b && z = \ |
|
57 \(x = UU | (? a y. x = a && y & a ~= UU & a << b & y << z))" (fn prems => [ |
|
58 cut_facts_tac prems 1, |
|
59 safe_tac HOL_cs, |
|
60 stream_case_tac "x" 1, |
|
61 safe_tac (HOL_cs addSDs stream.inverts |
|
62 addSIs [minimal, monofun_cfun, monofun_cfun_arg]), |
|
63 fast_tac HOL_cs 1]); |
|
64 |
|
65 qed_goal "stream_inject_eq" thy |
|
66 "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b & s = t)" (fn prems => [ |
|
67 cut_facts_tac prems 1, |
|
68 safe_tac (HOL_cs addSEs stream.injects)]); |
|
69 |
|
70 |
|
71 (* ----------------------------------------------------------------------- *) |
|
72 (* theorems about stream_when *) |
|
73 (* ----------------------------------------------------------------------- *) |
|
74 |
|
75 section "stream_when"; |
|
76 |
|
77 qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [ |
|
78 stream_case_tac "s" 1, |
|
79 ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_fapp1::stream.when_rews)) |
|
80 ]); |
|
81 |
|
82 |
|
83 (* ----------------------------------------------------------------------- *) |
|
84 (* theorems about ft and rt *) |
|
85 (* ----------------------------------------------------------------------- *) |
|
86 |
|
87 section "ft & rt"; |
|
88 |
|
89 (* |
|
90 qed_goal "stream_ft_lemma1" thy "ft`s=UU --> s=UU" (fn prems => [ |
|
91 stream_case_tac "s" 1, |
|
92 REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1)]); |
|
93 *) |
|
94 |
|
95 qed_goal "ft_defin" thy "s~=UU ==> ft`s~=UU" (fn prems => [ |
|
96 cut_facts_tac prems 1, |
|
97 stream_case_tac "s" 1, |
|
98 fast_tac HOL_cs 1, |
|
99 asm_simp_tac (HOLCF_ss addsimps stream.rews) 1]); |
|
100 |
|
101 qed_goal "rt_strict_rev" thy "rt`s~=UU ==> s~=UU" (fn prems => [ |
|
102 cut_facts_tac prems 1, |
|
103 etac contrapos 1, |
|
104 asm_simp_tac (HOLCF_ss addsimps stream.sel_rews) 1]); |
|
105 |
|
106 qed_goal "surjectiv_scons" thy "(ft`s)&&(rt`s)=s" |
|
107 (fn prems => |
|
108 [ |
|
109 stream_case_tac "s" 1, |
|
110 REPEAT (asm_simp_tac (HOLCF_ss addsimps stream.rews) 1) |
|
111 ]); |
|
112 |
|
113 qed_goal_spec_mp "monofun_rt_mult" thy |
|
114 "!x s. x << s --> iterate i rt x << iterate i rt s" (fn _ => [ |
|
115 nat_ind_tac "i" 1, |
|
116 simp_tac (HOLCF_ss addsimps stream.take_rews) 1, |
|
117 strip_tac 1, |
|
118 stream_case_tac "x" 1, |
|
119 rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1, |
|
120 dtac stream_prefix 1, |
|
121 safe_tac HOL_cs, |
|
122 asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1]); |
|
123 |
|
124 |
|
125 (* ----------------------------------------------------------------------- *) |
|
126 (* theorems about stream_take *) |
|
127 (* ----------------------------------------------------------------------- *) |
|
128 |
|
129 section "stream_take"; |
|
130 |
|
131 qed_goal "stream_reach2" thy "(LUB i. stream_take i`s) = s" |
|
132 (fn prems => |
|
133 [ |
|
134 (res_inst_tac [("t","s")] (stream.reach RS subst) 1), |
|
135 (stac fix_def2 1), |
|
136 (rewrite_goals_tac [stream.take_def]), |
|
137 (stac contlub_cfun_fun 1), |
|
138 (rtac is_chain_iterate 1), |
|
139 (rtac refl 1) |
|
140 ]); |
|
141 |
|
142 qed_goal "chain_stream_take" thy "is_chain (%i.stream_take i`s)" (fn _ => [ |
|
143 rtac is_chainI 1, |
|
144 subgoal_tac "!i s. stream_take i`s << stream_take (Suc i)`s" 1, |
|
145 fast_tac HOL_cs 1, |
|
146 rtac allI 1, |
|
147 nat_ind_tac "i" 1, |
|
148 simp_tac (HOLCF_ss addsimps stream.take_rews) 1, |
|
149 rtac allI 1, |
|
150 stream_case_tac "s" 1, |
|
151 simp_tac (HOLCF_ss addsimps stream.take_rews) 1, |
|
152 asm_simp_tac (HOLCF_ss addsimps monofun_cfun_arg::stream.take_rews) 1]); |
|
153 |
|
154 qed_goalw "stream_take_more" thy [stream.take_def] |
|
155 "stream_take n`x = x ==> stream_take (Suc n)`x = x" (fn prems => [ |
|
156 cut_facts_tac prems 1, |
|
157 rtac antisym_less 1, |
|
158 rtac (stream.reach RS subst) 1, (* 1*back(); *) |
|
159 rtac monofun_cfun_fun 1, |
|
160 stac fix_def2 1, |
|
161 rtac is_ub_thelub 1, |
|
162 rtac is_chain_iterate 1, |
|
163 etac subst 1, (* 2*back(); *) |
|
164 rtac monofun_cfun_fun 1, |
|
165 rtac (rewrite_rule [is_chain] is_chain_iterate RS spec) 1]); |
|
166 |
|
167 (* |
|
168 val stream_take_lemma2 = prove_goal thy |
|
169 "! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2" (fn prems => [ |
|
170 (nat_ind_tac "n" 1), |
|
171 (simp_tac (!simpset addsimps stream_rews) 1), |
|
172 (strip_tac 1), |
|
173 (hyp_subst_tac 1), |
|
174 (simp_tac (!simpset addsimps stream_rews) 1), |
|
175 (rtac allI 1), |
|
176 (res_inst_tac [("s","s2")] streamE 1), |
|
177 (asm_simp_tac (!simpset addsimps stream_rews) 1), |
|
178 (asm_simp_tac (!simpset addsimps stream_rews) 1), |
|
179 (strip_tac 1 ), |
|
180 (subgoal_tac "stream_take n1`xs = xs" 1), |
|
181 (rtac ((hd stream_inject) RS conjunct2) 2), |
|
182 (atac 4), |
|
183 (atac 2), |
|
184 (atac 2), |
|
185 (rtac cfun_arg_cong 1), |
|
186 (fast_tac HOL_cs 1) |
|
187 ]); |
|
188 *) |
|
189 |
|
190 val stream_take_lemma3 = prove_goal thy |
|
191 "!x xs.x~=UU --> stream_take n`(x && xs) = x && xs --> stream_take n`xs=xs" |
|
192 (fn prems => [ |
|
193 (nat_ind_tac "n" 1), |
|
194 (asm_simp_tac (HOL_ss addsimps stream.take_rews) 1), |
|
195 (strip_tac 1), |
|
196 (res_inst_tac [("P","x && xs=UU")] notE 1), |
|
197 (eresolve_tac stream.con_rews 1), |
|
198 (etac sym 1), |
|
199 (strip_tac 1), |
|
200 (rtac stream_take_more 1), |
|
201 (res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1), |
|
202 (etac (hd(tl(tl(stream.take_rews))) RS subst) 1), |
|
203 (atac 1), |
|
204 (atac 1)]) RS spec RS spec RS mp RS mp; |
|
205 |
|
206 val stream_take_lemma4 = prove_goal thy |
|
207 "!x xs. stream_take n`xs=xs --> stream_take (Suc n)`(x && xs) = x && xs" |
|
208 (fn _ => [ |
|
209 (nat_ind_tac "n" 1), |
|
210 (simp_tac (HOL_ss addsimps stream.take_rews) 1), |
|
211 (simp_tac (HOL_ss addsimps stream.take_rews) 1) |
|
212 ]) RS spec RS spec RS mp; |
|
213 |
|
214 |
|
215 (* ------------------------------------------------------------------------- *) |
|
216 (* special induction rules *) |
|
217 (* ------------------------------------------------------------------------- *) |
|
218 |
|
219 section "induction"; |
|
220 |
|
221 qed_goalw "stream_finite_ind" thy [stream.finite_def] |
|
222 "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x" |
|
223 (fn prems => [ |
|
224 (cut_facts_tac prems 1), |
|
225 (etac exE 1), |
|
226 (etac subst 1), |
|
227 (rtac stream.finite_ind 1), |
|
228 (atac 1), |
|
229 (eresolve_tac prems 1), |
|
230 (atac 1)]); |
|
231 |
|
232 qed_goal "stream_finite_ind2" thy |
|
233 "[| P UU;\ |
|
234 \ !! x . x ~= UU ==> P (x && UU); \ |
|
235 \ !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s ) \ |
|
236 \ |] ==> !s. P (stream_take n`s)" (fn prems => [ |
|
237 res_inst_tac [("n","n")] nat_induct2 1, |
|
238 asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1, |
|
239 rtac allI 1, |
|
240 stream_case_tac "s" 1, |
|
241 asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1, |
|
242 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1, |
|
243 rtac allI 1, |
|
244 stream_case_tac "s" 1, |
|
245 asm_simp_tac (HOL_ss addsimps (hd prems)::stream.take_rews) 1, |
|
246 res_inst_tac [("x","sa")] stream.cases 1, |
|
247 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1, |
|
248 asm_simp_tac (HOL_ss addsimps stream.take_rews addsimps prems) 1]); |
|
249 |
|
250 |
|
251 qed_goal "stream_ind2" thy |
|
252 "[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); \ |
|
253 \ !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s)\ |
|
254 \ |] ==> P x" (fn prems => [ |
|
255 rtac (stream.reach RS subst) 1, |
|
256 rtac (adm_impl_admw RS wfix_ind) 1, |
|
257 rtac adm_subst 1, |
|
258 cont_tacR 1, |
|
259 resolve_tac prems 1, |
|
260 rtac allI 1, |
|
261 rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1, |
|
262 resolve_tac prems 1, |
|
263 eresolve_tac prems 1, |
|
264 eresolve_tac prems 1, atac 1, atac 1]); |
|
265 |
|
266 |
|
267 (* ----------------------------------------------------------------------- *) |
|
268 (* simplify use of coinduction *) |
|
269 (* ----------------------------------------------------------------------- *) |
|
270 |
|
271 section "coinduction"; |
|
272 |
|
273 qed_goalw "stream_coind_lemma2" thy [stream.bisim_def] |
|
274 "!s1 s2. R s1 s2 --> ft`s1 = ft`s2 & R (rt`s1) (rt`s2) ==> stream_bisim R" |
|
275 (fn prems => |
|
276 [ |
|
277 (cut_facts_tac prems 1), |
|
278 (strip_tac 1), |
|
279 (etac allE 1), |
|
280 (etac allE 1), |
|
281 (dtac mp 1), |
|
282 (atac 1), |
|
283 (etac conjE 1), |
|
284 (case_tac "x = UU & x' = UU" 1), |
|
285 (rtac disjI1 1), |
|
286 (fast_tac HOL_cs 1), |
|
287 (rtac disjI2 1), |
|
288 (rtac disjE 1), |
|
289 (etac (de_Morgan_conj RS subst) 1), |
|
290 (res_inst_tac [("x","ft`x")] exI 1), |
|
291 (res_inst_tac [("x","rt`x")] exI 1), |
|
292 (res_inst_tac [("x","rt`x'")] exI 1), |
|
293 (rtac conjI 1), |
|
294 (etac ft_defin 1), |
|
295 (asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1), |
|
296 (eres_inst_tac [("s","ft`x"),("t","ft`x'")] subst 1), |
|
297 (simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1), |
|
298 (res_inst_tac [("x","ft`x'")] exI 1), |
|
299 (res_inst_tac [("x","rt`x")] exI 1), |
|
300 (res_inst_tac [("x","rt`x'")] exI 1), |
|
301 (rtac conjI 1), |
|
302 (etac ft_defin 1), |
|
303 (asm_simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1), |
|
304 (res_inst_tac [("s","ft`x"),("t","ft`x'")] ssubst 1), |
|
305 (etac sym 1), |
|
306 (simp_tac (HOLCF_ss addsimps stream.rews addsimps [surjectiv_scons]) 1) |
|
307 ]); |
|
308 |
|
309 (* ----------------------------------------------------------------------- *) |
|
310 (* theorems about stream_finite *) |
|
311 (* ----------------------------------------------------------------------- *) |
|
312 |
|
313 section "stream_finite"; |
|
314 |
|
315 qed_goalw "stream_finite_UU" thy [stream.finite_def] "stream_finite UU" |
|
316 (fn prems => [ |
|
317 (rtac exI 1), |
|
318 (simp_tac (HOLCF_ss addsimps stream.rews) 1)]); |
|
319 |
|
320 qed_goal "stream_finite_UU_rev" thy "~ stream_finite s ==> s ~= UU" (fn prems => |
|
321 [ |
|
322 (cut_facts_tac prems 1), |
|
323 (etac contrapos 1), |
|
324 (hyp_subst_tac 1), |
|
325 (rtac stream_finite_UU 1) |
|
326 ]); |
|
327 |
|
328 qed_goalw "stream_finite_lemma1" thy [stream.finite_def] |
|
329 "stream_finite xs ==> stream_finite (x && xs)" (fn prems => [ |
|
330 (cut_facts_tac prems 1), |
|
331 (etac exE 1), |
|
332 (rtac exI 1), |
|
333 (etac stream_take_lemma4 1) |
|
334 ]); |
|
335 |
|
336 qed_goalw "stream_finite_lemma2" thy [stream.finite_def] |
|
337 "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs" (fn prems => |
|
338 [ |
|
339 (cut_facts_tac prems 1), |
|
340 (etac exE 1), |
|
341 (rtac exI 1), |
|
342 (etac stream_take_lemma3 1), |
|
343 (atac 1) |
|
344 ]); |
|
345 |
|
346 qed_goal "stream_finite_rt_eq" thy "stream_finite (rt`s) = stream_finite s" |
|
347 (fn _ => [ |
|
348 stream_case_tac "s" 1, |
|
349 simp_tac (HOL_ss addsimps stream_finite_UU::stream.sel_rews) 1, |
|
350 asm_simp_tac (HOL_ss addsimps stream.sel_rews) 1, |
|
351 fast_tac (HOL_cs addIs [stream_finite_lemma1] |
|
352 addDs [stream_finite_lemma2]) 1]); |
|
353 |
|
354 qed_goal_spec_mp "stream_finite_less" thy |
|
355 "stream_finite s ==> !t. t<<s --> stream_finite t" (fn prems => [ |
|
356 cut_facts_tac prems 1, |
|
357 eres_inst_tac [("x","s")] stream_finite_ind 1, |
|
358 strip_tac 1, dtac UU_I 1, |
|
359 asm_simp_tac (HOLCF_ss addsimps [stream_finite_UU]) 1, |
|
360 strip_tac 1, |
|
361 asm_full_simp_tac (HOL_ss addsimps [stream_prefix']) 1, |
|
362 fast_tac (HOL_cs addSIs [stream_finite_UU, stream_finite_lemma1]) 1]); |
|
363 |
|
364 qed_goal "adm_not_stream_finite" thy "adm (%x. ~ stream_finite x)" (fn _ => [ |
|
365 rtac admI 1, |
|
366 dtac spec 1, |
|
367 etac contrapos 1, |
|
368 dtac stream_finite_less 1, |
|
369 etac is_ub_thelub 1, |
|
370 atac 1]); |