src/HOLCF/Stream.ML
changeset 892 d0dc8d057929
parent 625 119391dd1d59
child 948 3647161d15d3
equal deleted inserted replaced
891:a5ad535a241a 892:d0dc8d057929
    41 
    41 
    42 (* ------------------------------------------------------------------------*)
    42 (* ------------------------------------------------------------------------*)
    43 (* Exhaustion and elimination for streams                                  *)
    43 (* Exhaustion and elimination for streams                                  *)
    44 (* ------------------------------------------------------------------------*)
    44 (* ------------------------------------------------------------------------*)
    45 
    45 
    46 val Exh_stream = prove_goalw Stream.thy [scons_def]
    46 qed_goalw "Exh_stream" Stream.thy [scons_def]
    47 	"s = UU | (? x xs. x~=UU & s = scons[x][xs])"
    47 	"s = UU | (? x xs. x~=UU & s = scons[x][xs])"
    48  (fn prems =>
    48  (fn prems =>
    49 	[
    49 	[
    50 	(simp_tac HOLCF_ss  1),
    50 	(simp_tac HOLCF_ss  1),
    51 	(rtac (stream_rep_iso RS subst) 1),
    51 	(rtac (stream_rep_iso RS subst) 1),
    59 	(rtac exI 1),
    59 	(rtac exI 1),
    60 	(etac conjI 1),
    60 	(etac conjI 1),
    61 	(asm_simp_tac HOLCF_ss  1)
    61 	(asm_simp_tac HOLCF_ss  1)
    62 	]);
    62 	]);
    63 
    63 
    64 val streamE = prove_goal Stream.thy 
    64 qed_goal "streamE" Stream.thy 
    65 	"[| s=UU ==> Q; !!x xs.[|s=scons[x][xs];x~=UU|]==>Q|]==>Q"
    65 	"[| s=UU ==> Q; !!x xs.[|s=scons[x][xs];x~=UU|]==>Q|]==>Q"
    66  (fn prems =>
    66  (fn prems =>
    67 	[
    67 	[
    68 	(rtac (Exh_stream RS disjE) 1),
    68 	(rtac (Exh_stream RS disjE) 1),
    69 	(eresolve_tac prems 1),
    69 	(eresolve_tac prems 1),
   267 
   267 
   268 (* ------------------------------------------------------------------------*)
   268 (* ------------------------------------------------------------------------*)
   269 (* enhance the simplifier                                                  *)
   269 (* enhance the simplifier                                                  *)
   270 (* ------------------------------------------------------------------------*)
   270 (* ------------------------------------------------------------------------*)
   271 
   271 
   272 val stream_copy2 = prove_goal Stream.thy 
   272 qed_goal "stream_copy2" Stream.thy 
   273      "stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
   273      "stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
   274  (fn prems =>
   274  (fn prems =>
   275 	[
   275 	[
   276 	(res_inst_tac [("Q","x=UU")] classical2 1),
   276 	(res_inst_tac [("Q","x=UU")] classical2 1),
   277 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   277 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   278 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   278 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   279 	]);
   279 	]);
   280 
   280 
   281 val shd2 = prove_goal Stream.thy "shd[scons[x][xs]]=x"
   281 qed_goal "shd2" Stream.thy "shd[scons[x][xs]]=x"
   282  (fn prems =>
   282  (fn prems =>
   283 	[
   283 	[
   284 	(res_inst_tac [("Q","x=UU")] classical2 1),
   284 	(res_inst_tac [("Q","x=UU")] classical2 1),
   285 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   285 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   286 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   286 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   287 	]);
   287 	]);
   288 
   288 
   289 val stream_take2 = prove_goal Stream.thy 
   289 qed_goal "stream_take2" Stream.thy 
   290  "stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
   290  "stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
   291  (fn prems =>
   291  (fn prems =>
   292 	[
   292 	[
   293 	(res_inst_tac [("Q","x=UU")] classical2 1),
   293 	(res_inst_tac [("Q","x=UU")] classical2 1),
   294 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   294 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   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 
   333 val stream_reach2 = prove_goal Stream.thy  "lub(range(%i.stream_take(i)[s]))=s"
   333 qed_goal "stream_reach2" Stream.thy  "lub(range(%i.stream_take(i)[s]))=s"
   334  (fn prems =>
   334  (fn prems =>
   335 	[
   335 	[
   336 	(res_inst_tac [("t","s")] (stream_reach RS subst) 1),
   336 	(res_inst_tac [("t","s")] (stream_reach RS subst) 1),
   337 	(rtac (fix_def2 RS ssubst) 1),
   337 	(rtac (fix_def2 RS ssubst) 1),
   338 	(rewrite_goals_tac [stream_take_def]),
   338 	(rewrite_goals_tac [stream_take_def]),
   343 
   343 
   344 (* ------------------------------------------------------------------------*)
   344 (* ------------------------------------------------------------------------*)
   345 (* Co -induction for streams                                               *)
   345 (* Co -induction for streams                                               *)
   346 (* ------------------------------------------------------------------------*)
   346 (* ------------------------------------------------------------------------*)
   347 
   347 
   348 val stream_coind_lemma = prove_goalw Stream.thy [stream_bisim_def] 
   348 qed_goalw "stream_coind_lemma" Stream.thy [stream_bisim_def] 
   349 "stream_bisim(R) ==> ! p q.R(p,q) --> stream_take(n)[p]=stream_take(n)[q]"
   349 "stream_bisim(R) ==> ! p q.R(p,q) --> stream_take(n)[p]=stream_take(n)[q]"
   350  (fn prems =>
   350  (fn prems =>
   351 	[
   351 	[
   352 	(cut_facts_tac prems 1),
   352 	(cut_facts_tac prems 1),
   353 	(nat_ind_tac "n" 1),
   353 	(nat_ind_tac "n" 1),
   363 	(REPEAT (etac conjE 1)),
   363 	(REPEAT (etac conjE 1)),
   364 	(rtac cfun_arg_cong 1),
   364 	(rtac cfun_arg_cong 1),
   365 	(fast_tac HOL_cs 1)
   365 	(fast_tac HOL_cs 1)
   366 	]);
   366 	]);
   367 
   367 
   368 val stream_coind = prove_goal Stream.thy "[|stream_bisim(R);R(p,q)|] ==> p = q"
   368 qed_goal "stream_coind" Stream.thy "[|stream_bisim(R);R(p,q)|] ==> p = q"
   369  (fn prems =>
   369  (fn prems =>
   370 	[
   370 	[
   371 	(rtac stream_take_lemma 1),
   371 	(rtac stream_take_lemma 1),
   372 	(rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
   372 	(rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
   373 	(resolve_tac prems 1),
   373 	(resolve_tac prems 1),
   376 
   376 
   377 (* ------------------------------------------------------------------------*)
   377 (* ------------------------------------------------------------------------*)
   378 (* structural induction for admissible predicates                          *)
   378 (* structural induction for admissible predicates                          *)
   379 (* ------------------------------------------------------------------------*)
   379 (* ------------------------------------------------------------------------*)
   380 
   380 
   381 val stream_finite_ind = prove_goal Stream.thy
   381 qed_goal "stream_finite_ind" Stream.thy
   382 "[|P(UU);\
   382 "[|P(UU);\
   383 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   383 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   384 \  |] ==> !s.P(stream_take(n)[s])"
   384 \  |] ==> !s.P(stream_take(n)[s])"
   385  (fn prems =>
   385  (fn prems =>
   386 	[
   386 	[
   395 	(resolve_tac prems 1),
   395 	(resolve_tac prems 1),
   396 	(atac 1),
   396 	(atac 1),
   397 	(etac spec 1)
   397 	(etac spec 1)
   398 	]);
   398 	]);
   399 
   399 
   400 val stream_finite_ind2 = prove_goalw Stream.thy  [stream_finite_def]
   400 qed_goalw "stream_finite_ind2" Stream.thy  [stream_finite_def]
   401 "(!!n.P(stream_take(n)[s])) ==>  stream_finite(s) -->P(s)"
   401 "(!!n.P(stream_take(n)[s])) ==>  stream_finite(s) -->P(s)"
   402  (fn prems =>
   402  (fn prems =>
   403 	[
   403 	[
   404 	(strip_tac 1),
   404 	(strip_tac 1),
   405 	(etac exE 1),
   405 	(etac exE 1),
   406 	(etac subst 1),
   406 	(etac subst 1),
   407 	(resolve_tac prems 1)
   407 	(resolve_tac prems 1)
   408 	]);
   408 	]);
   409 
   409 
   410 val stream_finite_ind3 = prove_goal Stream.thy 
   410 qed_goal "stream_finite_ind3" Stream.thy 
   411 "[|P(UU);\
   411 "[|P(UU);\
   412 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   412 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   413 \  |] ==> stream_finite(s) --> P(s)"
   413 \  |] ==> stream_finite(s) --> P(s)"
   414  (fn prems =>
   414  (fn prems =>
   415 	[
   415 	[
   421 
   421 
   422 (* prove induction using definition of admissibility 
   422 (* prove induction using definition of admissibility 
   423    stream_reach rsp. stream_reach2 
   423    stream_reach rsp. stream_reach2 
   424    and finite induction stream_finite_ind *)
   424    and finite induction stream_finite_ind *)
   425 
   425 
   426 val stream_ind = prove_goal Stream.thy
   426 qed_goal "stream_ind" Stream.thy
   427 "[|adm(P);\
   427 "[|adm(P);\
   428 \  P(UU);\
   428 \  P(UU);\
   429 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   429 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   430 \  |] ==> P(s)"
   430 \  |] ==> P(s)"
   431  (fn prems =>
   431  (fn prems =>
   441 	(REPEAT (resolve_tac prems 1)),
   441 	(REPEAT (resolve_tac prems 1)),
   442 	(REPEAT (atac 1))
   442 	(REPEAT (atac 1))
   443 	]);
   443 	]);
   444 
   444 
   445 (* prove induction with usual LCF-Method using fixed point induction *)
   445 (* prove induction with usual LCF-Method using fixed point induction *)
   446 val stream_ind = prove_goal Stream.thy
   446 qed_goal "stream_ind" Stream.thy
   447 "[|adm(P);\
   447 "[|adm(P);\
   448 \  P(UU);\
   448 \  P(UU);\
   449 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   449 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   450 \  |] ==> P(s)"
   450 \  |] ==> P(s)"
   451  (fn prems =>
   451  (fn prems =>
   467 
   467 
   468 (* ------------------------------------------------------------------------*)
   468 (* ------------------------------------------------------------------------*)
   469 (* simplify use of Co-induction                                            *)
   469 (* simplify use of Co-induction                                            *)
   470 (* ------------------------------------------------------------------------*)
   470 (* ------------------------------------------------------------------------*)
   471 
   471 
   472 val surjectiv_scons = prove_goal Stream.thy "scons[shd[s]][stl[s]]=s"
   472 qed_goal "surjectiv_scons" Stream.thy "scons[shd[s]][stl[s]]=s"
   473  (fn prems =>
   473  (fn prems =>
   474 	[
   474 	[
   475 	(res_inst_tac [("s","s")] streamE 1),
   475 	(res_inst_tac [("s","s")] streamE 1),
   476 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   476 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   477 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   477 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   478 	]);
   478 	]);
   479 
   479 
   480 
   480 
   481 val stream_coind_lemma2 = prove_goalw Stream.thy [stream_bisim_def]
   481 qed_goalw "stream_coind_lemma2" Stream.thy [stream_bisim_def]
   482 "!s1 s2. R(s1, s2)-->shd[s1]=shd[s2] & R(stl[s1],stl[s2]) ==>stream_bisim(R)"
   482 "!s1 s2. R(s1, s2)-->shd[s1]=shd[s2] & R(stl[s1],stl[s2]) ==>stream_bisim(R)"
   483  (fn prems =>
   483  (fn prems =>
   484 	[
   484 	[
   485 	(cut_facts_tac prems 1),
   485 	(cut_facts_tac prems 1),
   486 	(strip_tac 1),
   486 	(strip_tac 1),
   521 
   521 
   522 (* ----------------------------------------------------------------------- *)
   522 (* ----------------------------------------------------------------------- *)
   523 (* 2 lemmas about stream_finite                                            *)
   523 (* 2 lemmas about stream_finite                                            *)
   524 (* ----------------------------------------------------------------------- *)
   524 (* ----------------------------------------------------------------------- *)
   525 
   525 
   526 val stream_finite_UU = prove_goalw Stream.thy [stream_finite_def]
   526 qed_goalw "stream_finite_UU" Stream.thy [stream_finite_def]
   527 	 "stream_finite(UU)"
   527 	 "stream_finite(UU)"
   528  (fn prems =>
   528  (fn prems =>
   529 	[
   529 	[
   530 	(rtac exI 1),
   530 	(rtac exI 1),
   531 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   531 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   532 	]);
   532 	]);
   533 
   533 
   534 val inf_stream_not_UU = prove_goal Stream.thy  "~stream_finite(s)  ==> s ~= UU"
   534 qed_goal "inf_stream_not_UU" Stream.thy  "~stream_finite(s)  ==> s ~= UU"
   535  (fn prems =>
   535  (fn prems =>
   536 	[
   536 	[
   537 	(cut_facts_tac prems 1),
   537 	(cut_facts_tac prems 1),
   538 	(etac swap 1),
   538 	(etac swap 1),
   539 	(dtac notnotD 1),
   539 	(dtac notnotD 1),
   543 
   543 
   544 (* ----------------------------------------------------------------------- *)
   544 (* ----------------------------------------------------------------------- *)
   545 (* a lemma about shd                                                       *)
   545 (* a lemma about shd                                                       *)
   546 (* ----------------------------------------------------------------------- *)
   546 (* ----------------------------------------------------------------------- *)
   547 
   547 
   548 val stream_shd_lemma1 = prove_goal Stream.thy "shd[s]=UU --> s=UU"
   548 qed_goal "stream_shd_lemma1" Stream.thy "shd[s]=UU --> s=UU"
   549  (fn prems =>
   549  (fn prems =>
   550 	[
   550 	[
   551 	(res_inst_tac [("s","s")] streamE 1),
   551 	(res_inst_tac [("s","s")] streamE 1),
   552 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   552 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   553 	(hyp_subst_tac 1),
   553 	(hyp_subst_tac 1),
   557 
   557 
   558 (* ----------------------------------------------------------------------- *)
   558 (* ----------------------------------------------------------------------- *)
   559 (* lemmas about stream_take                                                *)
   559 (* lemmas about stream_take                                                *)
   560 (* ----------------------------------------------------------------------- *)
   560 (* ----------------------------------------------------------------------- *)
   561 
   561 
   562 val stream_take_lemma1 = prove_goal Stream.thy 
   562 qed_goal "stream_take_lemma1" Stream.thy 
   563  "!x xs.x~=UU --> \
   563  "!x xs.x~=UU --> \
   564 \  stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
   564 \  stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
   565  (fn prems =>
   565  (fn prems =>
   566 	[
   566 	[
   567 	(rtac allI 1),
   567 	(rtac allI 1),
   574 	(atac 1),
   574 	(atac 1),
   575 	(atac 1)
   575 	(atac 1)
   576 	]);
   576 	]);
   577 
   577 
   578 
   578 
   579 val stream_take_lemma2 = prove_goal Stream.thy 
   579 qed_goal "stream_take_lemma2" Stream.thy 
   580  "! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
   580  "! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
   581  (fn prems =>
   581  (fn prems =>
   582 	[
   582 	[
   583 	(nat_ind_tac "n" 1),
   583 	(nat_ind_tac "n" 1),
   584 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   584 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   597 	(atac 2),
   597 	(atac 2),
   598 	(rtac cfun_arg_cong 1),
   598 	(rtac cfun_arg_cong 1),
   599 	(fast_tac HOL_cs 1)
   599 	(fast_tac HOL_cs 1)
   600 	]);
   600 	]);
   601 
   601 
   602 val stream_take_lemma3 = prove_goal Stream.thy 
   602 qed_goal "stream_take_lemma3" Stream.thy 
   603  "!x xs.x~=UU --> \
   603  "!x xs.x~=UU --> \
   604 \  stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
   604 \  stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
   605  (fn prems =>
   605  (fn prems =>
   606 	[
   606 	[
   607 	(nat_ind_tac "n" 1),
   607 	(nat_ind_tac "n" 1),
   616 	(atac 1),
   616 	(atac 1),
   617 	(atac 1),
   617 	(atac 1),
   618 	(etac (stream_take2 RS subst) 1)
   618 	(etac (stream_take2 RS subst) 1)
   619 	]);
   619 	]);
   620 
   620 
   621 val stream_take_lemma4 = prove_goal Stream.thy 
   621 qed_goal "stream_take_lemma4" Stream.thy 
   622  "!x xs.\
   622  "!x xs.\
   623 \stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
   623 \stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
   624  (fn prems =>
   624  (fn prems =>
   625 	[
   625 	[
   626 	(nat_ind_tac "n" 1),
   626 	(nat_ind_tac "n" 1),
   628 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   628 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   629 	]);
   629 	]);
   630 
   630 
   631 (* ---- *)
   631 (* ---- *)
   632 
   632 
   633 val stream_take_lemma5 = prove_goal Stream.thy 
   633 qed_goal "stream_take_lemma5" Stream.thy 
   634 "!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
   634 "!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
   635  (fn prems =>
   635  (fn prems =>
   636 	[
   636 	[
   637 	(nat_ind_tac "n" 1),
   637 	(nat_ind_tac "n" 1),
   638 	(simp_tac iterate_ss 1),
   638 	(simp_tac iterate_ss 1),
   649 	(hyp_subst_tac 1),
   649 	(hyp_subst_tac 1),
   650 	(etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
   650 	(etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
   651 	(atac 1)
   651 	(atac 1)
   652 	]);
   652 	]);
   653 
   653 
   654 val stream_take_lemma6 = prove_goal Stream.thy 
   654 qed_goal "stream_take_lemma6" Stream.thy 
   655 "!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
   655 "!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
   656  (fn prems =>
   656  (fn prems =>
   657 	[
   657 	[
   658 	(nat_ind_tac "n" 1),
   658 	(nat_ind_tac "n" 1),
   659 	(simp_tac iterate_ss 1),
   659 	(simp_tac iterate_ss 1),
   666 	(hyp_subst_tac 1),
   666 	(hyp_subst_tac 1),
   667 	(rtac (iterate_Suc2 RS ssubst) 1),
   667 	(rtac (iterate_Suc2 RS ssubst) 1),
   668 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   668 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   669 	]);
   669 	]);
   670 
   670 
   671 val stream_take_lemma7 = prove_goal Stream.thy 
   671 qed_goal "stream_take_lemma7" Stream.thy 
   672 "(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
   672 "(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
   673  (fn prems =>
   673  (fn prems =>
   674 	[
   674 	[
   675 	(rtac iffI 1),
   675 	(rtac iffI 1),
   676 	(etac (stream_take_lemma6 RS spec RS mp) 1),
   676 	(etac (stream_take_lemma6 RS spec RS mp) 1),
   677 	(etac (stream_take_lemma5 RS spec RS mp) 1)
   677 	(etac (stream_take_lemma5 RS spec RS mp) 1)
   678 	]);
   678 	]);
   679 
   679 
   680 
   680 
   681 val stream_take_lemma8 = prove_goal Stream.thy
   681 qed_goal "stream_take_lemma8" Stream.thy
   682 "[|adm(P); !n. ? m. n < m & P(stream_take(m)[s])|] ==> P(s)"
   682 "[|adm(P); !n. ? m. n < m & P(stream_take(m)[s])|] ==> P(s)"
   683  (fn prems =>
   683  (fn prems =>
   684 	[
   684 	[
   685 	(cut_facts_tac prems 1),
   685 	(cut_facts_tac prems 1),
   686 	(rtac (stream_reach2 RS subst) 1),
   686 	(rtac (stream_reach2 RS subst) 1),
   694 
   694 
   695 (* ----------------------------------------------------------------------- *)
   695 (* ----------------------------------------------------------------------- *)
   696 (* lemmas stream_finite                                                    *)
   696 (* lemmas stream_finite                                                    *)
   697 (* ----------------------------------------------------------------------- *)
   697 (* ----------------------------------------------------------------------- *)
   698 
   698 
   699 val stream_finite_lemma1 = prove_goalw Stream.thy [stream_finite_def]
   699 qed_goalw "stream_finite_lemma1" Stream.thy [stream_finite_def]
   700  "stream_finite(xs) ==> stream_finite(scons[x][xs])"
   700  "stream_finite(xs) ==> stream_finite(scons[x][xs])"
   701  (fn prems =>
   701  (fn prems =>
   702 	[
   702 	[
   703 	(cut_facts_tac prems 1),
   703 	(cut_facts_tac prems 1),
   704 	(etac exE 1),
   704 	(etac exE 1),
   705 	(rtac exI 1),
   705 	(rtac exI 1),
   706 	(etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
   706 	(etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
   707 	]);
   707 	]);
   708 
   708 
   709 val stream_finite_lemma2 = prove_goalw Stream.thy [stream_finite_def]
   709 qed_goalw "stream_finite_lemma2" Stream.thy [stream_finite_def]
   710  "[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
   710  "[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
   711  (fn prems =>
   711  (fn prems =>
   712 	[
   712 	[
   713 	(cut_facts_tac prems 1),
   713 	(cut_facts_tac prems 1),
   714 	(etac exE 1),
   714 	(etac exE 1),
   715 	(rtac exI 1),
   715 	(rtac exI 1),
   716 	(etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
   716 	(etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
   717 	(atac 1)
   717 	(atac 1)
   718 	]);
   718 	]);
   719 
   719 
   720 val stream_finite_lemma3 = prove_goal Stream.thy 
   720 qed_goal "stream_finite_lemma3" Stream.thy 
   721  "x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
   721  "x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
   722  (fn prems =>
   722  (fn prems =>
   723 	[
   723 	[
   724 	(cut_facts_tac prems 1),
   724 	(cut_facts_tac prems 1),
   725 	(rtac iffI 1),
   725 	(rtac iffI 1),
   727 	(atac 1),
   727 	(atac 1),
   728 	(etac stream_finite_lemma1 1)
   728 	(etac stream_finite_lemma1 1)
   729 	]);
   729 	]);
   730 
   730 
   731 
   731 
   732 val stream_finite_lemma5 = prove_goalw Stream.thy [stream_finite_def]
   732 qed_goalw "stream_finite_lemma5" Stream.thy [stream_finite_def]
   733  "(!n. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
   733  "(!n. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
   734 \=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
   734 \=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
   735  (fn prems =>
   735  (fn prems =>
   736 	[
   736 	[
   737 	(rtac iffI 1),
   737 	(rtac iffI 1),
   738 	(fast_tac HOL_cs 1),
   738 	(fast_tac HOL_cs 1),
   739 	(fast_tac HOL_cs 1)
   739 	(fast_tac HOL_cs 1)
   740 	]);
   740 	]);
   741 
   741 
   742 val stream_finite_lemma6 = prove_goal Stream.thy
   742 qed_goal "stream_finite_lemma6" Stream.thy
   743  "!s1 s2. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
   743  "!s1 s2. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
   744  (fn prems =>
   744  (fn prems =>
   745 	[
   745 	[
   746 	(nat_ind_tac "n" 1),
   746 	(nat_ind_tac "n" 1),
   747 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   747 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   779 	(atac 1),
   779 	(atac 1),
   780 	(atac 1),
   780 	(atac 1),
   781 	(atac 1)
   781 	(atac 1)
   782 	]);
   782 	]);
   783 
   783 
   784 val stream_finite_lemma7 = prove_goal Stream.thy 
   784 qed_goal "stream_finite_lemma7" Stream.thy 
   785 "s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
   785 "s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
   786  (fn prems =>
   786  (fn prems =>
   787 	[
   787 	[
   788 	(rtac (stream_finite_lemma5 RS iffD1) 1),
   788 	(rtac (stream_finite_lemma5 RS iffD1) 1),
   789 	(rtac allI 1),
   789 	(rtac allI 1),
   790 	(rtac (stream_finite_lemma6 RS spec RS spec) 1)
   790 	(rtac (stream_finite_lemma6 RS spec RS spec) 1)
   791 	]);
   791 	]);
   792 
   792 
   793 val stream_finite_lemma8 = prove_goalw Stream.thy [stream_finite_def]
   793 qed_goalw "stream_finite_lemma8" Stream.thy [stream_finite_def]
   794 "stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
   794 "stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
   795  (fn prems =>
   795  (fn prems =>
   796 	[
   796 	[
   797 	(simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
   797 	(simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
   798 	]);
   798 	]);
   800 
   800 
   801 (* ----------------------------------------------------------------------- *)
   801 (* ----------------------------------------------------------------------- *)
   802 (* admissibility of ~stream_finite                                         *)
   802 (* admissibility of ~stream_finite                                         *)
   803 (* ----------------------------------------------------------------------- *)
   803 (* ----------------------------------------------------------------------- *)
   804 
   804 
   805 val adm_not_stream_finite = prove_goalw Stream.thy [adm_def]
   805 qed_goalw "adm_not_stream_finite" Stream.thy [adm_def]
   806  "adm(%s. ~ stream_finite(s))"
   806  "adm(%s. ~ stream_finite(s))"
   807  (fn prems =>
   807  (fn prems =>
   808 	[
   808 	[
   809 	(strip_tac 1 ),
   809 	(strip_tac 1 ),
   810 	(res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),
   810 	(res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),
   823 (* and prove adm. of ~(? n. iterate(n, stl, s) = UU)                       *)
   823 (* and prove adm. of ~(? n. iterate(n, stl, s) = UU)                       *)
   824 (* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
   824 (* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
   825 (* ----------------------------------------------------------------------- *)
   825 (* ----------------------------------------------------------------------- *)
   826 
   826 
   827 
   827 
   828 val adm_not_stream_finite2=prove_goal Stream.thy "adm(%s. ~ stream_finite(s))"
   828 qed_goal "adm_not_stream_finite" Stream.thy "adm(%s. ~ stream_finite(s))"
   829  (fn prems =>
   829  (fn prems =>
   830 	[
   830 	[
   831 	(subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
   831 	(subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
   832 	(etac (adm_cong RS iffD2)1),
   832 	(etac (adm_cong RS iffD2)1),
   833 	(REPEAT(resolve_tac adm_thms 1)),
   833 	(REPEAT(resolve_tac adm_thms 1)),