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