src/HOLCF/stream.ML
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 297 5ef75ff3baeb
permissions -rw-r--r--
made tutorial first;
     1 (*  Title: 	HOLCF/stream.ML
     2     ID:         $Id$
     3     Author: 	Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6 Lemmas for stream.thy
     7 *)
     8 
     9 open Stream;
    10 
    11 (* ------------------------------------------------------------------------*)
    12 (* The isomorphisms stream_rep_iso and stream_abs_iso are strict           *)
    13 (* ------------------------------------------------------------------------*)
    14 
    15 val stream_iso_strict= stream_rep_iso RS (stream_abs_iso RS 
    16 	(allI  RSN (2,allI RS iso_strict)));
    17 
    18 val stream_rews = [stream_iso_strict RS conjunct1,
    19 		stream_iso_strict RS conjunct2];
    20 
    21 (* ------------------------------------------------------------------------*)
    22 (* Properties of stream_copy                                               *)
    23 (* ------------------------------------------------------------------------*)
    24 
    25 fun prover defs thm =  prove_goalw Stream.thy defs thm
    26  (fn prems =>
    27 	[
    28 	(cut_facts_tac prems 1),
    29 	(asm_simp_tac (HOLCF_ss addsimps 
    30 		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
    31 	]);
    32 
    33 val stream_copy = 
    34 	[
    35 	prover [stream_copy_def] "stream_copy[f][UU]=UU",
    36 	prover [stream_copy_def,scons_def] 
    37 	"x~=UU ==> stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
    38 	];
    39 
    40 val stream_rews =  stream_copy @ stream_rews; 
    41 
    42 (* ------------------------------------------------------------------------*)
    43 (* Exhaustion and elimination for streams                                  *)
    44 (* ------------------------------------------------------------------------*)
    45 
    46 val Exh_stream = prove_goalw Stream.thy [scons_def]
    47 	"s = UU | (? x xs. x~=UU & s = scons[x][xs])"
    48  (fn prems =>
    49 	[
    50 	(simp_tac HOLCF_ss  1),
    51 	(rtac (stream_rep_iso RS subst) 1),
    52 	(res_inst_tac [("p","stream_rep[s]")] sprodE 1),
    53 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
    54 	(asm_simp_tac HOLCF_ss  1),
    55 	(res_inst_tac [("p","y")] liftE1 1),
    56 	(contr_tac 1),
    57 	(rtac disjI2 1),
    58 	(rtac exI 1),
    59 	(rtac exI 1),
    60 	(etac conjI 1),
    61 	(asm_simp_tac HOLCF_ss  1)
    62 	]);
    63 
    64 val streamE = prove_goal Stream.thy 
    65 	"[| s=UU ==> Q; !!x xs.[|s=scons[x][xs];x~=UU|]==>Q|]==>Q"
    66  (fn prems =>
    67 	[
    68 	(rtac (Exh_stream RS disjE) 1),
    69 	(eresolve_tac prems 1),
    70 	(etac exE 1),
    71 	(etac exE 1),
    72 	(resolve_tac prems 1),
    73 	(fast_tac HOL_cs 1),
    74 	(fast_tac HOL_cs 1)
    75 	]);
    76 
    77 (* ------------------------------------------------------------------------*)
    78 (* Properties of stream_when                                               *)
    79 (* ------------------------------------------------------------------------*)
    80 
    81 fun prover defs thm =  prove_goalw Stream.thy defs thm
    82  (fn prems =>
    83 	[
    84 	(cut_facts_tac prems 1),
    85 	(asm_simp_tac (HOLCF_ss addsimps 
    86 		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
    87 	]);
    88 
    89 
    90 val stream_when = [
    91 	prover [stream_when_def] "stream_when[f][UU]=UU",
    92 	prover [stream_when_def,scons_def] 
    93 		"x~=UU ==> stream_when[f][scons[x][xs]]= f[x][xs]"
    94 	];
    95 
    96 val stream_rews = stream_when @ stream_rews;
    97 
    98 (* ------------------------------------------------------------------------*)
    99 (* Rewrites for  discriminators and  selectors                             *)
   100 (* ------------------------------------------------------------------------*)
   101 
   102 fun prover defs thm = prove_goalw Stream.thy defs thm
   103  (fn prems =>
   104 	[
   105 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   106 	]);
   107 
   108 val stream_discsel = [
   109 	prover [is_scons_def] "is_scons[UU]=UU",
   110 	prover [shd_def] "shd[UU]=UU",
   111 	prover [stl_def] "stl[UU]=UU"
   112 	];
   113 
   114 fun prover defs thm = prove_goalw Stream.thy defs thm
   115  (fn prems =>
   116 	[
   117 	(cut_facts_tac prems 1),
   118 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   119 	]);
   120 
   121 val stream_discsel = [
   122 prover [is_scons_def,shd_def,stl_def] "x~=UU ==> is_scons[scons[x][xs]]=TT",
   123 prover [is_scons_def,shd_def,stl_def] "x~=UU ==> shd[scons[x][xs]]=x",
   124 prover [is_scons_def,shd_def,stl_def] "x~=UU ==> stl[scons[x][xs]]=xs"
   125 	] @ stream_discsel;
   126 
   127 val stream_rews = stream_discsel @ stream_rews;
   128 
   129 (* ------------------------------------------------------------------------*)
   130 (* Definedness and strictness                                              *)
   131 (* ------------------------------------------------------------------------*)
   132 
   133 fun prover contr thm = prove_goal Stream.thy thm
   134  (fn prems =>
   135 	[
   136 	(res_inst_tac [("P1",contr)] classical3 1),
   137 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   138 	(dtac sym 1),
   139 	(asm_simp_tac HOLCF_ss  1),
   140 	(simp_tac (HOLCF_ss addsimps (prems @ stream_rews)) 1)
   141 	]);
   142 
   143 val stream_constrdef = [
   144 	prover "is_scons[UU] ~= UU" "x~=UU ==> scons[x][xs]~=UU"
   145 	]; 
   146 
   147 fun prover defs thm = prove_goalw Stream.thy defs thm
   148  (fn prems =>
   149 	[
   150 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   151 	]);
   152 
   153 val stream_constrdef = [
   154 	prover [scons_def] "scons[UU][xs]=UU"
   155 	] @ stream_constrdef;
   156 
   157 val stream_rews = stream_constrdef @ stream_rews;
   158 
   159 
   160 (* ------------------------------------------------------------------------*)
   161 (* Distinctness wrt. << and =                                              *)
   162 (* ------------------------------------------------------------------------*)
   163 
   164 
   165 (* ------------------------------------------------------------------------*)
   166 (* Invertibility                                                           *)
   167 (* ------------------------------------------------------------------------*)
   168 
   169 val stream_invert =
   170 	[
   171 prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
   172 \ scons[x1][x2] << scons[y1][y2]|] ==> x1<< y1 & x2 << y2"
   173  (fn prems =>
   174 	[
   175 	(cut_facts_tac prems 1),
   176 	(rtac conjI 1),
   177 	(dres_inst_tac [("fo5","stream_when[LAM x l.x]")] monofun_cfun_arg 1),
   178 	(etac box_less 1),
   179 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   180 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   181 	(dres_inst_tac [("fo5","stream_when[LAM x l.l]")] monofun_cfun_arg 1),
   182 	(etac box_less 1),
   183 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   184 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
   185 	])
   186 	];
   187 
   188 (* ------------------------------------------------------------------------*)
   189 (* Injectivity                                                             *)
   190 (* ------------------------------------------------------------------------*)
   191 
   192 val stream_inject = 
   193 	[
   194 prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
   195 \ scons[x1][x2] = scons[y1][y2]|] ==> x1= y1 & x2 = y2"
   196  (fn prems =>
   197 	[
   198 	(cut_facts_tac prems 1),
   199 	(rtac conjI 1),
   200 	(dres_inst_tac [("f","stream_when[LAM x l.x]")] cfun_arg_cong 1),
   201 	(etac box_equals 1),
   202 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   203 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   204 	(dres_inst_tac [("f","stream_when[LAM x l.l]")] cfun_arg_cong 1),
   205 	(etac box_equals 1),
   206 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   207 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
   208 	])
   209 	];
   210 
   211 (* ------------------------------------------------------------------------*)
   212 (* definedness for  discriminators and  selectors                          *)
   213 (* ------------------------------------------------------------------------*)
   214 
   215 fun prover thm = prove_goal Stream.thy thm
   216  (fn prems =>
   217 	[
   218 	(cut_facts_tac prems 1),
   219 	(rtac streamE 1),
   220 	(contr_tac 1),
   221 	(REPEAT (asm_simp_tac (HOLCF_ss addsimps stream_discsel) 1))
   222 	]);
   223 
   224 val stream_discsel_def = 
   225 	[
   226 	prover "s~=UU ==> is_scons[s]~=UU", 
   227 	prover "s~=UU ==> shd[s]~=UU" 
   228 	];
   229 
   230 val stream_rews = stream_discsel_def @ stream_rews;
   231 
   232 
   233 (* ------------------------------------------------------------------------*)
   234 (* Properties stream_take                                                  *)
   235 (* ------------------------------------------------------------------------*)
   236 
   237 val stream_take =
   238 	[
   239 prove_goalw Stream.thy [stream_take_def] "stream_take(n)[UU]=UU"
   240  (fn prems =>
   241 	[
   242 	(res_inst_tac [("n","n")] natE 1),
   243 	(asm_simp_tac iterate_ss 1),
   244 	(asm_simp_tac iterate_ss 1),
   245 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   246 	]),
   247 prove_goalw Stream.thy [stream_take_def] "stream_take(0)[xs]=UU"
   248  (fn prems =>
   249 	[
   250 	(asm_simp_tac iterate_ss 1)
   251 	])];
   252 
   253 fun prover thm = prove_goalw Stream.thy [stream_take_def] thm
   254  (fn prems =>
   255 	[
   256 	(cut_facts_tac prems 1),
   257 	(simp_tac iterate_ss 1),
   258 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   259 	]);
   260 
   261 val stream_take = [
   262 prover 
   263   "x~=UU ==> stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
   264 	] @ stream_take;
   265 
   266 val stream_rews = stream_take @ stream_rews;
   267 
   268 (* ------------------------------------------------------------------------*)
   269 (* enhance the simplifier                                                  *)
   270 (* ------------------------------------------------------------------------*)
   271 
   272 val stream_copy2 = prove_goal Stream.thy 
   273      "stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
   274  (fn prems =>
   275 	[
   276 	(res_inst_tac [("Q","x=UU")] classical2 1),
   277 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   278 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   279 	]);
   280 
   281 val shd2 = prove_goal Stream.thy "shd[scons[x][xs]]=x"
   282  (fn prems =>
   283 	[
   284 	(res_inst_tac [("Q","x=UU")] classical2 1),
   285 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   286 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   287 	]);
   288 
   289 val stream_take2 = prove_goal Stream.thy 
   290  "stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
   291  (fn prems =>
   292 	[
   293 	(res_inst_tac [("Q","x=UU")] classical2 1),
   294 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   295 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   296 	]);
   297 
   298 val stream_rews = [stream_iso_strict RS conjunct1,
   299 		   stream_iso_strict RS conjunct2,
   300                    hd stream_copy, stream_copy2]
   301                   @ stream_when
   302                   @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))  
   303                   @ stream_constrdef
   304                   @ stream_discsel_def
   305                   @ [ stream_take2] @ (tl stream_take);
   306 
   307 
   308 (* ------------------------------------------------------------------------*)
   309 (* take lemma for streams                                                  *)
   310 (* ------------------------------------------------------------------------*)
   311 
   312 fun prover reach defs thm  = prove_goalw Stream.thy defs thm
   313  (fn prems =>
   314 	[
   315 	(res_inst_tac [("t","s1")] (reach RS subst) 1),
   316 	(res_inst_tac [("t","s2")] (reach RS subst) 1),
   317 	(rtac (fix_def2 RS ssubst) 1),
   318 	(rtac (contlub_cfun_fun RS ssubst) 1),
   319 	(rtac is_chain_iterate 1),
   320 	(rtac (contlub_cfun_fun RS ssubst) 1),
   321 	(rtac is_chain_iterate 1),
   322 	(rtac lub_equal 1),
   323 	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
   324 	(rtac (is_chain_iterate RS ch2ch_fappL) 1),
   325 	(rtac allI 1),
   326 	(resolve_tac prems 1)
   327 	]);
   328 
   329 val stream_take_lemma = prover stream_reach  [stream_take_def]
   330 	"(!!n.stream_take(n)[s1]=stream_take(n)[s2]) ==> s1=s2";
   331 
   332 
   333 (* ------------------------------------------------------------------------*)
   334 (* Co -induction for streams                                               *)
   335 (* ------------------------------------------------------------------------*)
   336 
   337 val stream_coind_lemma = prove_goalw Stream.thy [stream_bisim_def] 
   338 "stream_bisim(R) ==> ! p q.R(p,q) --> stream_take(n)[p]=stream_take(n)[q]"
   339  (fn prems =>
   340 	[
   341 	(cut_facts_tac prems 1),
   342 	(nat_ind_tac "n" 1),
   343 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   344 	(strip_tac 1),
   345 	((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
   346 	(atac 1),
   347 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   348 	(etac exE 1),
   349 	(etac exE 1),
   350 	(etac exE 1),
   351 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   352 	(REPEAT (etac conjE 1)),
   353 	(rtac cfun_arg_cong 1),
   354 	(fast_tac HOL_cs 1)
   355 	]);
   356 
   357 val stream_coind = prove_goal Stream.thy "[|stream_bisim(R);R(p,q)|] ==> p = q"
   358  (fn prems =>
   359 	[
   360 	(rtac stream_take_lemma 1),
   361 	(rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
   362 	(resolve_tac prems 1),
   363 	(resolve_tac prems 1)
   364 	]);
   365 
   366 (* ------------------------------------------------------------------------*)
   367 (* structural induction for admissible predicates                          *)
   368 (* ------------------------------------------------------------------------*)
   369 
   370 val stream_finite_ind = prove_goal Stream.thy
   371 "[|P(UU);\
   372 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   373 \  |] ==> !s.P(stream_take(n)[s])"
   374  (fn prems =>
   375 	[
   376 	(nat_ind_tac "n" 1),
   377 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   378 	(resolve_tac prems 1),
   379 	(rtac allI 1),
   380 	(res_inst_tac [("s","s")] streamE 1),
   381 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   382 	(resolve_tac prems 1),
   383 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   384 	(resolve_tac prems 1),
   385 	(atac 1),
   386 	(etac spec 1)
   387 	]);
   388 
   389 val stream_finite_ind2 = prove_goalw Stream.thy  [stream_finite_def]
   390 "(!!n.P(stream_take(n)[s])) ==>  stream_finite(s) -->P(s)"
   391  (fn prems =>
   392 	[
   393 	(strip_tac 1),
   394 	(etac exE 1),
   395 	(etac subst 1),
   396 	(resolve_tac prems 1)
   397 	]);
   398 
   399 val stream_finite_ind3 = prove_goal Stream.thy 
   400 "[|P(UU);\
   401 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   402 \  |] ==> stream_finite(s) --> P(s)"
   403  (fn prems =>
   404 	[
   405 	(rtac stream_finite_ind2 1),
   406 	(rtac (stream_finite_ind RS spec) 1),
   407 	(REPEAT (resolve_tac prems 1)),
   408 	(REPEAT (atac 1))
   409 	]);
   410 
   411 val stream_ind = prove_goal Stream.thy
   412 "[|adm(P);\
   413 \  P(UU);\
   414 \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   415 \  |] ==> P(s)"
   416  (fn prems =>
   417 	[
   418 	(rtac (stream_reach RS subst) 1),
   419 	(res_inst_tac [("x","s")] spec 1),
   420 	(rtac wfix_ind 1),
   421 	(rtac adm_impl_admw 1),
   422 	(REPEAT (resolve_tac adm_thms 1)),
   423 	(rtac adm_subst 1),
   424 	(contX_tacR 1),
   425 	(resolve_tac prems 1),
   426 	(rtac allI 1),
   427 	(rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
   428 	(REPEAT (resolve_tac prems 1)),
   429 	(REPEAT (atac 1))
   430 	]);
   431 
   432 
   433 (* ------------------------------------------------------------------------*)
   434 (* simplify use of Co-induction                                            *)
   435 (* ------------------------------------------------------------------------*)
   436 
   437 val surjectiv_scons = prove_goal Stream.thy "scons[shd[s]][stl[s]]=s"
   438  (fn prems =>
   439 	[
   440 	(res_inst_tac [("s","s")] streamE 1),
   441 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   442 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   443 	]);
   444 
   445 
   446 val stream_coind_lemma2 = prove_goalw Stream.thy [stream_bisim_def]
   447 "!s1 s2. R(s1, s2)-->shd[s1]=shd[s2] & R(stl[s1],stl[s2]) ==>stream_bisim(R)"
   448  (fn prems =>
   449 	[
   450 	(cut_facts_tac prems 1),
   451 	(strip_tac 1),
   452 	(etac allE 1),
   453 	(etac allE 1),
   454 	(dtac mp 1),
   455 	(atac 1),
   456 	(etac conjE 1),
   457 	(res_inst_tac [("Q","s1 = UU & s2 = UU")] classical2 1),
   458 	(rtac disjI1 1),
   459 	(fast_tac HOL_cs 1),
   460 	(rtac disjI2 1),
   461 	(rtac disjE 1),
   462 	(etac (de_morgan2 RS ssubst) 1),
   463 	(res_inst_tac [("x","shd[s1]")] exI 1),
   464 	(res_inst_tac [("x","stl[s1]")] exI 1),
   465 	(res_inst_tac [("x","stl[s2]")] exI 1),
   466 	(rtac conjI 1),
   467 	(eresolve_tac stream_discsel_def 1),
   468 	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
   469 	(eres_inst_tac [("s","shd[s1]"),("t","shd[s2]")] subst 1),
   470 	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
   471 	(res_inst_tac [("x","shd[s2]")] exI 1),
   472 	(res_inst_tac [("x","stl[s1]")] exI 1),
   473 	(res_inst_tac [("x","stl[s2]")] exI 1),
   474 	(rtac conjI 1),
   475 	(eresolve_tac stream_discsel_def 1),
   476 	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
   477 	(res_inst_tac [("s","shd[s1]"),("t","shd[s2]")] ssubst 1),
   478 	(etac sym 1),
   479 	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1)
   480 	]);
   481 
   482 
   483 (* ------------------------------------------------------------------------*)
   484 (* theorems about finite and infinite streams                              *)
   485 (* ------------------------------------------------------------------------*)
   486 
   487 (* ----------------------------------------------------------------------- *)
   488 (* 2 lemmas about stream_finite                                            *)
   489 (* ----------------------------------------------------------------------- *)
   490 
   491 val stream_finite_UU = prove_goalw Stream.thy [stream_finite_def]
   492 	 "stream_finite(UU)"
   493  (fn prems =>
   494 	[
   495 	(rtac exI 1),
   496 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   497 	]);
   498 
   499 val inf_stream_not_UU = prove_goal Stream.thy  "~stream_finite(s)  ==> s ~= UU"
   500  (fn prems =>
   501 	[
   502 	(cut_facts_tac prems 1),
   503 	(etac swap 1),
   504 	(dtac notnotD 1),
   505 	(hyp_subst_tac  1),
   506 	(rtac stream_finite_UU 1)
   507 	]);
   508 
   509 (* ----------------------------------------------------------------------- *)
   510 (* a lemma about shd                                                       *)
   511 (* ----------------------------------------------------------------------- *)
   512 
   513 val stream_shd_lemma1 = prove_goal Stream.thy "shd[s]=UU --> s=UU"
   514  (fn prems =>
   515 	[
   516 	(res_inst_tac [("s","s")] streamE 1),
   517 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   518 	(hyp_subst_tac 1),
   519 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   520 	]);
   521 
   522 
   523 (* ----------------------------------------------------------------------- *)
   524 (* lemmas about stream_take                                                *)
   525 (* ----------------------------------------------------------------------- *)
   526 
   527 val stream_take_lemma1 = prove_goal Stream.thy 
   528  "!x xs.x~=UU --> \
   529 \  stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
   530  (fn prems =>
   531 	[
   532 	(rtac allI 1),
   533 	(rtac allI 1),
   534 	(rtac impI 1),
   535 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   536 	(strip_tac 1),
   537 	(rtac ((hd stream_inject) RS conjunct2) 1),
   538 	(atac 1),
   539 	(atac 1),
   540 	(atac 1)
   541 	]);
   542 
   543 
   544 val stream_take_lemma2 = prove_goal Stream.thy 
   545  "! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
   546  (fn prems =>
   547 	[
   548 	(nat_ind_tac "n" 1),
   549 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   550 	(strip_tac 1 ),
   551 	(hyp_subst_tac  1),
   552 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   553 	(rtac allI 1),
   554 	(res_inst_tac [("s","s2")] streamE 1),
   555 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   556 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   557 	(strip_tac 1 ),
   558 	(subgoal_tac "stream_take(n1)[xs] = xs" 1),
   559 	(rtac ((hd stream_inject) RS conjunct2) 2),
   560 	(atac 4),
   561 	(atac 2),
   562 	(atac 2),
   563 	(rtac cfun_arg_cong 1),
   564 	(fast_tac HOL_cs 1)
   565 	]);
   566 
   567 val stream_take_lemma3 = prove_goal Stream.thy 
   568  "!x xs.x~=UU --> \
   569 \  stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
   570  (fn prems =>
   571 	[
   572 	(nat_ind_tac "n" 1),
   573 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   574 	(strip_tac 1 ),
   575 	(res_inst_tac [("P","scons[x][xs]=UU")] notE 1),
   576 	(eresolve_tac stream_constrdef 1),
   577 	(etac sym 1),
   578 	(strip_tac 1 ),
   579 	(rtac (stream_take_lemma2 RS spec RS mp) 1),
   580 	(res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
   581 	(atac 1),
   582 	(atac 1),
   583 	(etac (stream_take2 RS subst) 1)
   584 	]);
   585 
   586 val stream_take_lemma4 = prove_goal Stream.thy 
   587  "!x xs.\
   588 \stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
   589  (fn prems =>
   590 	[
   591 	(nat_ind_tac "n" 1),
   592 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   593 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   594 	]);
   595 
   596 (* ---- *)
   597 
   598 val stream_take_lemma5 = prove_goal Stream.thy 
   599 "!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
   600  (fn prems =>
   601 	[
   602 	(nat_ind_tac "n" 1),
   603 	(simp_tac iterate_ss 1),
   604 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   605 	(strip_tac 1),
   606 	(res_inst_tac [("s","s")] streamE 1),
   607 	(hyp_subst_tac 1),
   608 	(rtac (iterate_Suc2 RS ssubst) 1),
   609 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   610 	(rtac (iterate_Suc2 RS ssubst) 1),
   611 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   612 	(etac allE 1),
   613 	(etac mp 1),
   614 	(hyp_subst_tac 1),
   615 	(etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
   616 	(atac 1)
   617 	]);
   618 
   619 val stream_take_lemma6 = prove_goal Stream.thy 
   620 "!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
   621  (fn prems =>
   622 	[
   623 	(nat_ind_tac "n" 1),
   624 	(simp_tac iterate_ss 1),
   625 	(strip_tac 1),
   626 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   627 	(rtac allI 1),
   628 	(res_inst_tac [("s","s")] streamE 1),
   629 	(hyp_subst_tac 1),
   630 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   631 	(hyp_subst_tac 1),
   632 	(rtac (iterate_Suc2 RS ssubst) 1),
   633 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   634 	]);
   635 
   636 val stream_take_lemma7 = prove_goal Stream.thy 
   637 "(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
   638  (fn prems =>
   639 	[
   640 	(rtac iffI 1),
   641 	(etac (stream_take_lemma6 RS spec RS mp) 1),
   642 	(etac (stream_take_lemma5 RS spec RS mp) 1)
   643 	]);
   644 
   645 
   646 (* ----------------------------------------------------------------------- *)
   647 (* lemmas stream_finite                                                    *)
   648 (* ----------------------------------------------------------------------- *)
   649 
   650 val stream_finite_lemma1 = prove_goalw Stream.thy [stream_finite_def]
   651  "stream_finite(xs) ==> stream_finite(scons[x][xs])"
   652  (fn prems =>
   653 	[
   654 	(cut_facts_tac prems 1),
   655 	(etac exE 1),
   656 	(rtac exI 1),
   657 	(etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
   658 	]);
   659 
   660 val stream_finite_lemma2 = prove_goalw Stream.thy [stream_finite_def]
   661  "[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
   662  (fn prems =>
   663 	[
   664 	(cut_facts_tac prems 1),
   665 	(etac exE 1),
   666 	(rtac exI 1),
   667 	(etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
   668 	(atac 1)
   669 	]);
   670 
   671 val stream_finite_lemma3 = prove_goal Stream.thy 
   672  "x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
   673  (fn prems =>
   674 	[
   675 	(cut_facts_tac prems 1),
   676 	(rtac iffI 1),
   677 	(etac stream_finite_lemma2 1),
   678 	(atac 1),
   679 	(etac stream_finite_lemma1 1)
   680 	]);
   681 
   682 
   683 val stream_finite_lemma5 = prove_goalw Stream.thy [stream_finite_def]
   684  "(!n. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
   685 \=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
   686  (fn prems =>
   687 	[
   688 	(rtac iffI 1),
   689 	(fast_tac HOL_cs 1),
   690 	(fast_tac HOL_cs 1)
   691 	]);
   692 
   693 val stream_finite_lemma6 = prove_goal Stream.thy
   694  "!s1 s2. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
   695  (fn prems =>
   696 	[
   697 	(nat_ind_tac "n" 1),
   698 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   699 	(strip_tac 1 ),
   700 	(hyp_subst_tac  1),
   701 	(dtac UU_I 1),
   702 	(hyp_subst_tac  1),
   703 	(rtac stream_finite_UU 1),
   704 	(rtac allI 1),
   705 	(rtac allI 1),
   706 	(res_inst_tac [("s","s1")] streamE 1),
   707 	(hyp_subst_tac  1),
   708 	(strip_tac 1 ),
   709 	(rtac stream_finite_UU 1),
   710 	(hyp_subst_tac  1),
   711 	(res_inst_tac [("s","s2")] streamE 1),
   712 	(hyp_subst_tac  1),
   713 	(strip_tac 1 ),
   714 	(dtac UU_I 1),
   715 	(asm_simp_tac(HOLCF_ss addsimps (stream_rews @ [stream_finite_UU])) 1),
   716 	(hyp_subst_tac  1),
   717 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   718 	(strip_tac 1 ),
   719 	(rtac stream_finite_lemma1 1),
   720 	(subgoal_tac "xs << xsa" 1),
   721 	(subgoal_tac "stream_take(n1)[xsa] = xsa" 1),
   722 	(fast_tac HOL_cs 1),
   723 	(res_inst_tac  [("x1.1","xa"),("y1.1","xa")] 
   724                    ((hd stream_inject) RS conjunct2) 1),
   725 	(atac 1),
   726 	(atac 1),
   727 	(atac 1),
   728 	(res_inst_tac [("x1.1","x"),("y1.1","xa")]
   729 	 ((hd stream_invert) RS conjunct2) 1),
   730 	(atac 1),
   731 	(atac 1),
   732 	(atac 1)
   733 	]);
   734 
   735 val stream_finite_lemma7 = prove_goal Stream.thy 
   736 "s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
   737  (fn prems =>
   738 	[
   739 	(rtac (stream_finite_lemma5 RS iffD1) 1),
   740 	(rtac allI 1),
   741 	(rtac (stream_finite_lemma6 RS spec RS spec) 1)
   742 	]);
   743 
   744 val stream_finite_lemma8 = prove_goalw Stream.thy [stream_finite_def]
   745 "stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
   746  (fn prems =>
   747 	[
   748 	(simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
   749 	]);
   750 
   751 
   752 (* ----------------------------------------------------------------------- *)
   753 (* admissibility of ~stream_finite                                         *)
   754 (* ----------------------------------------------------------------------- *)
   755 
   756 val adm_not_stream_finite = prove_goalw Stream.thy [adm_def]
   757  "adm(%s. ~ stream_finite(s))"
   758  (fn prems =>
   759 	[
   760 	(strip_tac 1 ),
   761 	(res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),
   762 	(atac 2),
   763 	(subgoal_tac "!i.stream_finite(Y(i))" 1),
   764 	(fast_tac HOL_cs 1),
   765 	(rtac allI 1),
   766 	(rtac (stream_finite_lemma7 RS mp RS mp) 1),
   767 	(etac is_ub_thelub 1),
   768 	(atac 1)
   769 	]);
   770 
   771 (* ----------------------------------------------------------------------- *)
   772 (* alternative prove for admissibility of ~stream_finite                   *)
   773 (* show that stream_finite(s) = (? n. iterate(n, stl, s) = UU)             *)
   774 (* and prove adm. of ~(? n. iterate(n, stl, s) = UU)                       *)
   775 (* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
   776 (* ----------------------------------------------------------------------- *)
   777 
   778 
   779 val adm_not_stream_finite2=prove_goal Stream.thy "adm(%s. ~ stream_finite(s))"
   780  (fn prems =>
   781 	[
   782 	(subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
   783 	(etac (adm_cong RS iffD2)1),
   784 	(REPEAT(resolve_tac adm_thms 1)),
   785 	(rtac  contX_iterate2 1),
   786 	(rtac allI 1),
   787 	(rtac (stream_finite_lemma8 RS ssubst) 1),
   788 	(fast_tac HOL_cs 1)
   789 	]);
   790 
   791