src/HOLCF/Stream.ML
changeset 1168 74be52691d62
parent 948 3647161d15d3
child 1267 bca91b4e1710
equal deleted inserted replaced
1167:cbd32a0f2f41 1168:74be52691d62
    30 		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
    30 		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
    31 	]);
    31 	]);
    32 
    32 
    33 val stream_copy = 
    33 val stream_copy = 
    34 	[
    34 	[
    35 	prover [stream_copy_def] "stream_copy[f][UU]=UU",
    35 	prover [stream_copy_def] "stream_copy`f`UU=UU",
    36 	prover [stream_copy_def,scons_def] 
    36 	prover [stream_copy_def,scons_def] 
    37 	"x~=UU ==> stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
    37 	"x~=UU ==> stream_copy`f`(scons`x`xs)= scons`x`(f`xs)"
    38 	];
    38 	];
    39 
    39 
    40 val stream_rews =  stream_copy @ stream_rews; 
    40 val stream_rews =  stream_copy @ stream_rews; 
    41 
    41 
    42 (* ------------------------------------------------------------------------*)
    42 (* ------------------------------------------------------------------------*)
    43 (* Exhaustion and elimination for streams                                  *)
    43 (* Exhaustion and elimination for streams                                  *)
    44 (* ------------------------------------------------------------------------*)
    44 (* ------------------------------------------------------------------------*)
    45 
    45 
    46 qed_goalw "Exh_stream" 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),
    52 	(res_inst_tac [("p","stream_rep[s]")] sprodE 1),
    52 	(res_inst_tac [("p","stream_rep`s")] sprodE 1),
    53 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
    53 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
    54 	(asm_simp_tac HOLCF_ss  1),
    54 	(asm_simp_tac HOLCF_ss  1),
    55 	(res_inst_tac [("p","y")] liftE1 1),
    55 	(res_inst_tac [("p","y")] liftE1 1),
    56 	(contr_tac 1),
    56 	(contr_tac 1),
    57 	(rtac disjI2 1),
    57 	(rtac disjI2 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 qed_goal "streamE" 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),
    70 	(etac exE 1),
    70 	(etac exE 1),
    86 		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
    86 		(stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
    87 	]);
    87 	]);
    88 
    88 
    89 
    89 
    90 val stream_when = [
    90 val stream_when = [
    91 	prover [stream_when_def] "stream_when[f][UU]=UU",
    91 	prover [stream_when_def] "stream_when`f`UU=UU",
    92 	prover [stream_when_def,scons_def] 
    92 	prover [stream_when_def,scons_def] 
    93 		"x~=UU ==> stream_when[f][scons[x][xs]]= f[x][xs]"
    93 		"x~=UU ==> stream_when`f`(scons`x`xs)= f`x`xs"
    94 	];
    94 	];
    95 
    95 
    96 val stream_rews = stream_when @ stream_rews;
    96 val stream_rews = stream_when @ stream_rews;
    97 
    97 
    98 (* ------------------------------------------------------------------------*)
    98 (* ------------------------------------------------------------------------*)
   104 	[
   104 	[
   105 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   105 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   106 	]);
   106 	]);
   107 
   107 
   108 val stream_discsel = [
   108 val stream_discsel = [
   109 	prover [is_scons_def] "is_scons[UU]=UU",
   109 	prover [is_scons_def] "is_scons`UU=UU",
   110 	prover [shd_def] "shd[UU]=UU",
   110 	prover [shd_def] "shd`UU=UU",
   111 	prover [stl_def] "stl[UU]=UU"
   111 	prover [stl_def] "stl`UU=UU"
   112 	];
   112 	];
   113 
   113 
   114 fun prover defs thm = prove_goalw Stream.thy defs thm
   114 fun prover defs thm = prove_goalw Stream.thy defs thm
   115  (fn prems =>
   115  (fn prems =>
   116 	[
   116 	[
   117 	(cut_facts_tac prems 1),
   117 	(cut_facts_tac prems 1),
   118 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   118 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   119 	]);
   119 	]);
   120 
   120 
   121 val stream_discsel = [
   121 val stream_discsel = [
   122 prover [is_scons_def,shd_def,stl_def] "x~=UU ==> is_scons[scons[x][xs]]=TT",
   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",
   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"
   124 prover [is_scons_def,shd_def,stl_def] "x~=UU ==> stl`(scons`x`xs)=xs"
   125 	] @ stream_discsel;
   125 	] @ stream_discsel;
   126 
   126 
   127 val stream_rews = stream_discsel @ stream_rews;
   127 val stream_rews = stream_discsel @ stream_rews;
   128 
   128 
   129 (* ------------------------------------------------------------------------*)
   129 (* ------------------------------------------------------------------------*)
   139 	(asm_simp_tac HOLCF_ss  1),
   139 	(asm_simp_tac HOLCF_ss  1),
   140 	(simp_tac (HOLCF_ss addsimps (prems @ stream_rews)) 1)
   140 	(simp_tac (HOLCF_ss addsimps (prems @ stream_rews)) 1)
   141 	]);
   141 	]);
   142 
   142 
   143 val stream_constrdef = [
   143 val stream_constrdef = [
   144 	prover "is_scons[UU::'a stream] ~= UU" "x~=UU ==> scons[x::'a][xs]~=UU"
   144 	prover "is_scons`(UU::'a stream)~=UU" "x~=UU ==> scons`(x::'a)`xs~=UU"
   145 	]; 
   145 	]; 
   146 
   146 
   147 fun prover defs thm = prove_goalw Stream.thy defs thm
   147 fun prover defs thm = prove_goalw Stream.thy defs thm
   148  (fn prems =>
   148  (fn prems =>
   149 	[
   149 	[
   150 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   150 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   151 	]);
   151 	]);
   152 
   152 
   153 val stream_constrdef = [
   153 val stream_constrdef = [
   154 	prover [scons_def] "scons[UU][xs]=UU"
   154 	prover [scons_def] "scons`UU`xs=UU"
   155 	] @ stream_constrdef;
   155 	] @ stream_constrdef;
   156 
   156 
   157 val stream_rews = stream_constrdef @ stream_rews;
   157 val stream_rews = stream_constrdef @ stream_rews;
   158 
   158 
   159 
   159 
   167 (* ------------------------------------------------------------------------*)
   167 (* ------------------------------------------------------------------------*)
   168 
   168 
   169 val stream_invert =
   169 val stream_invert =
   170 	[
   170 	[
   171 prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
   171 prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
   172 \ scons[x1][x2] << scons[y1][y2]|] ==> x1<< y1 & x2 << y2"
   172 \ scons`x1`x2 << scons`y1`y2|] ==> x1<< y1 & x2 << y2"
   173  (fn prems =>
   173  (fn prems =>
   174 	[
   174 	[
   175 	(cut_facts_tac prems 1),
   175 	(cut_facts_tac prems 1),
   176 	(rtac conjI 1),
   176 	(rtac conjI 1),
   177 	(dres_inst_tac [("fo5","stream_when[LAM x l.x]")] monofun_cfun_arg 1),
   177 	(dres_inst_tac [("fo5","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
   178 	(etac box_less 1),
   178 	(etac box_less 1),
   179 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   179 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   180 	(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),
   181 	(dres_inst_tac [("fo5","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
   182 	(etac box_less 1),
   182 	(etac box_less 1),
   183 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   183 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   184 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
   184 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
   185 	])
   185 	])
   186 	];
   186 	];
   190 (* ------------------------------------------------------------------------*)
   190 (* ------------------------------------------------------------------------*)
   191 
   191 
   192 val stream_inject = 
   192 val stream_inject = 
   193 	[
   193 	[
   194 prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
   194 prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
   195 \ scons[x1][x2] = scons[y1][y2]|] ==> x1= y1 & x2 = y2"
   195 \ scons`x1`x2 = scons`y1`y2 |] ==> x1= y1 & x2 = y2"
   196  (fn prems =>
   196  (fn prems =>
   197 	[
   197 	[
   198 	(cut_facts_tac prems 1),
   198 	(cut_facts_tac prems 1),
   199 	(rtac conjI 1),
   199 	(rtac conjI 1),
   200 	(dres_inst_tac [("f","stream_when[LAM x l.x]")] cfun_arg_cong 1),
   200 	(dres_inst_tac [("f","stream_when`(LAM x l.x)")] cfun_arg_cong 1),
   201 	(etac box_equals 1),
   201 	(etac box_equals 1),
   202 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   202 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   203 	(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),
   204 	(dres_inst_tac [("f","stream_when`(LAM x l.l)")] cfun_arg_cong 1),
   205 	(etac box_equals 1),
   205 	(etac box_equals 1),
   206 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   206 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1),
   207 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
   207 	(asm_simp_tac (HOLCF_ss addsimps stream_when) 1)
   208 	])
   208 	])
   209 	];
   209 	];
   221 	(REPEAT (asm_simp_tac (HOLCF_ss addsimps stream_discsel) 1))
   221 	(REPEAT (asm_simp_tac (HOLCF_ss addsimps stream_discsel) 1))
   222 	]);
   222 	]);
   223 
   223 
   224 val stream_discsel_def = 
   224 val stream_discsel_def = 
   225 	[
   225 	[
   226 	prover "s~=UU ==> is_scons[s]~=UU", 
   226 	prover "s~=UU ==> is_scons`s ~= UU", 
   227 	prover "s~=UU ==> shd[s]~=UU" 
   227 	prover "s~=UU ==> shd`s ~=UU" 
   228 	];
   228 	];
   229 
   229 
   230 val stream_rews = stream_discsel_def @ stream_rews;
   230 val stream_rews = stream_discsel_def @ stream_rews;
   231 
   231 
   232 
   232 
   234 (* Properties stream_take                                                  *)
   234 (* Properties stream_take                                                  *)
   235 (* ------------------------------------------------------------------------*)
   235 (* ------------------------------------------------------------------------*)
   236 
   236 
   237 val stream_take =
   237 val stream_take =
   238 	[
   238 	[
   239 prove_goalw Stream.thy [stream_take_def] "stream_take(n)[UU]=UU"
   239 prove_goalw Stream.thy [stream_take_def] "stream_take n`UU = UU"
   240  (fn prems =>
   240  (fn prems =>
   241 	[
   241 	[
   242 	(res_inst_tac [("n","n")] natE 1),
   242 	(res_inst_tac [("n","n")] natE 1),
   243 	(asm_simp_tac iterate_ss 1),
   243 	(asm_simp_tac iterate_ss 1),
   244 	(asm_simp_tac iterate_ss 1),
   244 	(asm_simp_tac iterate_ss 1),
   245 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   245 	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   246 	]),
   246 	]),
   247 prove_goalw Stream.thy [stream_take_def] "stream_take(0)[xs]=UU"
   247 prove_goalw Stream.thy [stream_take_def] "stream_take 0`xs=UU"
   248  (fn prems =>
   248  (fn prems =>
   249 	[
   249 	[
   250 	(asm_simp_tac iterate_ss 1)
   250 	(asm_simp_tac iterate_ss 1)
   251 	])];
   251 	])];
   252 
   252 
   258 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   258 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   259 	]);
   259 	]);
   260 
   260 
   261 val stream_take = [
   261 val stream_take = [
   262 prover 
   262 prover 
   263   "x~=UU ==> stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
   263   "x~=UU ==> stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
   264 	] @ stream_take;
   264 	] @ stream_take;
   265 
   265 
   266 val stream_rews = stream_take @ stream_rews;
   266 val stream_rews = stream_take @ stream_rews;
   267 
   267 
   268 (* ------------------------------------------------------------------------*)
   268 (* ------------------------------------------------------------------------*)
   269 (* enhance the simplifier                                                  *)
   269 (* enhance the simplifier                                                  *)
   270 (* ------------------------------------------------------------------------*)
   270 (* ------------------------------------------------------------------------*)
   271 
   271 
   272 qed_goal "stream_copy2" 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 qed_goal "shd2" 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 qed_goal "stream_take2" 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),
   295 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   295 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 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 
   333 qed_goal "stream_reach2" 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]),
   344 (* ------------------------------------------------------------------------*)
   344 (* ------------------------------------------------------------------------*)
   345 (* Co -induction for streams                                               *)
   345 (* Co -induction for streams                                               *)
   346 (* ------------------------------------------------------------------------*)
   346 (* ------------------------------------------------------------------------*)
   347 
   347 
   348 qed_goalw "stream_coind_lemma" 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),
   354 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   354 	(simp_tac (HOLCF_ss addsimps stream_rews) 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 qed_goal "stream_coind" 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),
   378 (* structural induction for admissible predicates                          *)
   378 (* structural induction for admissible predicates                          *)
   379 (* ------------------------------------------------------------------------*)
   379 (* ------------------------------------------------------------------------*)
   380 
   380 
   381 qed_goal "stream_finite_ind" 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 	[
   387 	(nat_ind_tac "n" 1),
   387 	(nat_ind_tac "n" 1),
   388 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   388 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   389 	(resolve_tac prems 1),
   389 	(resolve_tac prems 1),
   396 	(atac 1),
   396 	(atac 1),
   397 	(etac spec 1)
   397 	(etac spec 1)
   398 	]);
   398 	]);
   399 
   399 
   400 qed_goalw "stream_finite_ind2" 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 qed_goal "stream_finite_ind3" 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 	[
   416 	(rtac stream_finite_ind2 1),
   416 	(rtac stream_finite_ind2 1),
   417 	(rtac (stream_finite_ind RS spec) 1),
   417 	(rtac (stream_finite_ind RS spec) 1),
   424    and finite induction stream_finite_ind *)
   424    and finite induction stream_finite_ind *)
   425 
   425 
   426 qed_goal "stream_ind" 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 =>
   432 	[
   432 	[
   433 	(rtac (stream_reach2 RS subst) 1),
   433 	(rtac (stream_reach2 RS subst) 1),
   434 	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   434 	(rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   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 qed_goal "stream_ind" 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 =>
   452 	[
   452 	[
   453 	(rtac (stream_reach RS subst) 1),
   453 	(rtac (stream_reach RS subst) 1),
   454 	(res_inst_tac [("x","s")] spec 1),
   454 	(res_inst_tac [("x","s")] spec 1),
   455 	(rtac wfix_ind 1),
   455 	(rtac wfix_ind 1),
   456 	(rtac adm_impl_admw 1),
   456 	(rtac adm_impl_admw 1),
   457 	(REPEAT (resolve_tac adm_thms 1)),
   457 	(REPEAT (resolve_tac adm_thms 1)),
   458 	(rtac adm_subst 1),
   458 	(rtac adm_subst 1),
   459 	(contX_tacR 1),
   459 	(cont_tacR 1),
   460 	(resolve_tac prems 1),
   460 	(resolve_tac prems 1),
   461 	(rtac allI 1),
   461 	(rtac allI 1),
   462 	(rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
   462 	(rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
   463 	(REPEAT (resolve_tac prems 1)),
   463 	(REPEAT (resolve_tac prems 1)),
   464 	(REPEAT (atac 1))
   464 	(REPEAT (atac 1))
   467 
   467 
   468 (* ------------------------------------------------------------------------*)
   468 (* ------------------------------------------------------------------------*)
   469 (* simplify use of Co-induction                                            *)
   469 (* simplify use of Co-induction                                            *)
   470 (* ------------------------------------------------------------------------*)
   470 (* ------------------------------------------------------------------------*)
   471 
   471 
   472 qed_goal "surjectiv_scons" 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 qed_goalw "stream_coind_lemma2" 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),
   487 	(etac allE 1),
   487 	(etac allE 1),
   493 	(rtac disjI1 1),
   493 	(rtac disjI1 1),
   494 	(fast_tac HOL_cs 1),
   494 	(fast_tac HOL_cs 1),
   495 	(rtac disjI2 1),
   495 	(rtac disjI2 1),
   496 	(rtac disjE 1),
   496 	(rtac disjE 1),
   497 	(etac (de_morgan2 RS ssubst) 1),
   497 	(etac (de_morgan2 RS ssubst) 1),
   498 	(res_inst_tac [("x","shd[s1]")] exI 1),
   498 	(res_inst_tac [("x","shd`s1")] exI 1),
   499 	(res_inst_tac [("x","stl[s1]")] exI 1),
   499 	(res_inst_tac [("x","stl`s1")] exI 1),
   500 	(res_inst_tac [("x","stl[s2]")] exI 1),
   500 	(res_inst_tac [("x","stl`s2")] exI 1),
   501 	(rtac conjI 1),
   501 	(rtac conjI 1),
   502 	(eresolve_tac stream_discsel_def 1),
   502 	(eresolve_tac stream_discsel_def 1),
   503 	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
   503 	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
   504 	(eres_inst_tac [("s","shd[s1]"),("t","shd[s2]")] subst 1),
   504 	(eres_inst_tac [("s","shd`s1"),("t","shd`s2")] subst 1),
   505 	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
   505 	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
   506 	(res_inst_tac [("x","shd[s2]")] exI 1),
   506 	(res_inst_tac [("x","shd`s2")] exI 1),
   507 	(res_inst_tac [("x","stl[s1]")] exI 1),
   507 	(res_inst_tac [("x","stl`s1")] exI 1),
   508 	(res_inst_tac [("x","stl[s2]")] exI 1),
   508 	(res_inst_tac [("x","stl`s2")] exI 1),
   509 	(rtac conjI 1),
   509 	(rtac conjI 1),
   510 	(eresolve_tac stream_discsel_def 1),
   510 	(eresolve_tac stream_discsel_def 1),
   511 	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
   511 	(asm_simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1),
   512 	(res_inst_tac [("s","shd[s1]"),("t","shd[s2]")] ssubst 1),
   512 	(res_inst_tac [("s","shd`s1"),("t","shd`s2")] ssubst 1),
   513 	(etac sym 1),
   513 	(etac sym 1),
   514 	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1)
   514 	(simp_tac (HOLCF_ss addsimps stream_rews addsimps [surjectiv_scons]) 1)
   515 	]);
   515 	]);
   516 
   516 
   517 
   517 
   543 
   543 
   544 (* ----------------------------------------------------------------------- *)
   544 (* ----------------------------------------------------------------------- *)
   545 (* a lemma about shd                                                       *)
   545 (* a lemma about shd                                                       *)
   546 (* ----------------------------------------------------------------------- *)
   546 (* ----------------------------------------------------------------------- *)
   547 
   547 
   548 qed_goal "stream_shd_lemma1" 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),
   559 (* lemmas about stream_take                                                *)
   559 (* lemmas about stream_take                                                *)
   560 (* ----------------------------------------------------------------------- *)
   560 (* ----------------------------------------------------------------------- *)
   561 
   561 
   562 qed_goal "stream_take_lemma1" 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),
   568 	(rtac allI 1),
   568 	(rtac allI 1),
   569 	(rtac impI 1),
   569 	(rtac impI 1),
   575 	(atac 1)
   575 	(atac 1)
   576 	]);
   576 	]);
   577 
   577 
   578 
   578 
   579 qed_goal "stream_take_lemma2" 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),
   585 	(strip_tac 1 ),
   585 	(strip_tac 1 ),
   588 	(rtac allI 1),
   588 	(rtac allI 1),
   589 	(res_inst_tac [("s","s2")] streamE 1),
   589 	(res_inst_tac [("s","s2")] streamE 1),
   590 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   590 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   591 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   591 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   592 	(strip_tac 1 ),
   592 	(strip_tac 1 ),
   593 	(subgoal_tac "stream_take(n1)[xs] = xs" 1),
   593 	(subgoal_tac "stream_take n1`xs = xs" 1),
   594 	(rtac ((hd stream_inject) RS conjunct2) 2),
   594 	(rtac ((hd stream_inject) RS conjunct2) 2),
   595 	(atac 4),
   595 	(atac 4),
   596 	(atac 2),
   596 	(atac 2),
   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 qed_goal "stream_take_lemma3" 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),
   608 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   608 	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   609 	(strip_tac 1 ),
   609 	(strip_tac 1 ),
   610 	(res_inst_tac [("P","scons[x][xs]=UU")] notE 1),
   610 	(res_inst_tac [("P","scons`x`xs=UU")] notE 1),
   611 	(eresolve_tac stream_constrdef 1),
   611 	(eresolve_tac stream_constrdef 1),
   612 	(etac sym 1),
   612 	(etac sym 1),
   613 	(strip_tac 1 ),
   613 	(strip_tac 1 ),
   614 	(rtac (stream_take_lemma2 RS spec RS mp) 1),
   614 	(rtac (stream_take_lemma2 RS spec RS mp) 1),
   615 	(res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
   615 	(res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
   618 	(etac (stream_take2 RS subst) 1)
   618 	(etac (stream_take2 RS subst) 1)
   619 	]);
   619 	]);
   620 
   620 
   621 qed_goal "stream_take_lemma4" 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),
   627 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   627 	(simp_tac (HOLCF_ss addsimps stream_rews) 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 qed_goal "stream_take_lemma5" 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),
   639 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   639 	(simp_tac (HOLCF_ss addsimps stream_rews) 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 qed_goal "stream_take_lemma6" 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),
   660 	(strip_tac 1),
   660 	(strip_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 qed_goal "stream_take_lemma7" 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 qed_goal "stream_take_lemma8" 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),
   687 	(rtac adm_disj_lemma11 1),
   687 	(rtac adm_disj_lemma11 1),
   695 (* ----------------------------------------------------------------------- *)
   695 (* ----------------------------------------------------------------------- *)
   696 (* lemmas stream_finite                                                    *)
   696 (* lemmas stream_finite                                                    *)
   697 (* ----------------------------------------------------------------------- *)
   697 (* ----------------------------------------------------------------------- *)
   698 
   698 
   699 qed_goalw "stream_finite_lemma1" 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 qed_goalw "stream_finite_lemma2" 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 qed_goal "stream_finite_lemma3" 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),
   726 	(etac stream_finite_lemma2 1),
   726 	(etac stream_finite_lemma2 1),
   728 	(etac stream_finite_lemma1 1)
   728 	(etac stream_finite_lemma1 1)
   729 	]);
   729 	]);
   730 
   730 
   731 
   731 
   732 qed_goalw "stream_finite_lemma5" 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 qed_goal "stream_finite_lemma6" 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),
   748 	(strip_tac 1 ),
   748 	(strip_tac 1 ),
   765 	(hyp_subst_tac  1),
   765 	(hyp_subst_tac  1),
   766 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   766 	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   767 	(strip_tac 1 ),
   767 	(strip_tac 1 ),
   768 	(rtac stream_finite_lemma1 1),
   768 	(rtac stream_finite_lemma1 1),
   769 	(subgoal_tac "xs << xsa" 1),
   769 	(subgoal_tac "xs << xsa" 1),
   770 	(subgoal_tac "stream_take(n1)[xsa] = xsa" 1),
   770 	(subgoal_tac "stream_take n1`xsa = xsa" 1),
   771 	(fast_tac HOL_cs 1),
   771 	(fast_tac HOL_cs 1),
   772 	(res_inst_tac  [("x1.1","xa"),("y1.1","xa")] 
   772 	(res_inst_tac  [("x1.1","xa"),("y1.1","xa")] 
   773                    ((hd stream_inject) RS conjunct2) 1),
   773                    ((hd stream_inject) RS conjunct2) 1),
   774 	(atac 1),
   774 	(atac 1),
   775 	(atac 1),
   775 	(atac 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 qed_goalw "stream_finite_lemma8" 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 	]);
   799 
   799 
   817 	(atac 1)
   817 	(atac 1)
   818 	]);
   818 	]);
   819 
   819 
   820 (* ----------------------------------------------------------------------- *)
   820 (* ----------------------------------------------------------------------- *)
   821 (* alternative prove for admissibility of ~stream_finite                   *)
   821 (* alternative prove for admissibility of ~stream_finite                   *)
   822 (* show that stream_finite(s) = (? n. iterate(n, stl, s) = UU)             *)
   822 (* show that stream_finite(s) = (? n. iterate n stl s = UU)                *)
   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 qed_goal "adm_not_stream_finite" 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)),
   834 	(rtac  contX_iterate2 1),
   834 	(rtac  cont_iterate2 1),
   835 	(rtac allI 1),
   835 	(rtac allI 1),
   836 	(rtac (stream_finite_lemma8 RS ssubst) 1),
   836 	(rtac (stream_finite_lemma8 RS ssubst) 1),
   837 	(fast_tac HOL_cs 1)
   837 	(fast_tac HOL_cs 1)
   838 	]);
   838 	]);
   839 
   839