309 (* take lemma for streams *) |
309 (* take lemma for streams *) |
310 (* ------------------------------------------------------------------------*) |
310 (* ------------------------------------------------------------------------*) |
311 |
311 |
312 fun prover reach defs thm = prove_goalw Stream.thy defs thm |
312 fun prover reach defs thm = prove_goalw Stream.thy defs thm |
313 (fn prems => |
313 (fn prems => |
314 [ |
314 [ |
315 (res_inst_tac [("t","s1")] (reach RS subst) 1), |
315 (res_inst_tac [("t","s1")] (reach RS subst) 1), |
316 (res_inst_tac [("t","s2")] (reach RS subst) 1), |
316 (res_inst_tac [("t","s2")] (reach RS subst) 1), |
317 (rtac (fix_def2 RS ssubst) 1), |
317 (rtac (fix_def2 RS ssubst) 1), |
318 (rtac (contlub_cfun_fun RS ssubst) 1), |
318 (rtac (contlub_cfun_fun RS ssubst) 1), |
319 (rtac is_chain_iterate 1), |
319 (rtac is_chain_iterate 1), |
320 (rtac (contlub_cfun_fun RS ssubst) 1), |
320 (rtac (contlub_cfun_fun RS ssubst) 1), |
321 (rtac is_chain_iterate 1), |
321 (rtac is_chain_iterate 1), |
322 (rtac lub_equal 1), |
322 (rtac lub_equal 1), |
323 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
323 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
324 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
324 (rtac (is_chain_iterate RS ch2ch_fappL) 1), |
325 (rtac allI 1), |
325 (rtac allI 1), |
326 (resolve_tac prems 1) |
326 (resolve_tac prems 1), |
327 ]); |
327 ]); |
328 |
328 |
329 val stream_take_lemma = prover stream_reach [stream_take_def] |
329 val stream_take_lemma = prover stream_reach [stream_take_def] |
330 "(!!n.stream_take n`s1 = stream_take n`s2) ==> s1=s2"; |
330 "(!!n.stream_take n`s1 = stream_take n`s2) ==> s1=s2"; |
331 |
331 |
332 |
332 |