2570
|
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]);
|