Franz fragen
authornipkow
Thu Mar 24 13:36:34 1994 +0100 (1994-03-24)
changeset 2975ef75ff3baeb
parent 296 e1f6cd9f682e
child 298 3a0485439396
Franz fragen
src/HOLCF/Cfun2.ML
src/HOLCF/Dnat.ML
src/HOLCF/Fix.ML
src/HOLCF/Porder.ML
src/HOLCF/Porder.thy
src/HOLCF/ROOT.ML
src/HOLCF/Stream.ML
src/HOLCF/Stream2.thy
src/HOLCF/cfun2.ML
src/HOLCF/dnat.ML
src/HOLCF/ex/Coind.ML
src/HOLCF/ex/ROOT.ML
src/HOLCF/ex/coind.ML
src/HOLCF/fix.ML
src/HOLCF/porder.ML
src/HOLCF/porder.thy
src/HOLCF/stream.ML
src/HOLCF/stream2.thy
     1.1 --- a/src/HOLCF/Cfun2.ML	Thu Mar 24 13:25:12 1994 +0100
     1.2 +++ b/src/HOLCF/Cfun2.ML	Thu Mar 24 13:36:34 1994 +0100
     1.3 @@ -216,7 +216,7 @@
     1.4  is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
     1.5  *)
     1.6  
     1.7 -val cpo_fun = prove_goal Cfun2.thy 
     1.8 +val cpo_cfun = prove_goal Cfun2.thy 
     1.9    "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
    1.10  (fn prems =>
    1.11  	[
     2.1 --- a/src/HOLCF/Dnat.ML	Thu Mar 24 13:25:12 1994 +0100
     2.2 +++ b/src/HOLCF/Dnat.ML	Thu Mar 24 13:36:34 1994 +0100
     2.3 @@ -171,41 +171,49 @@
     2.4  (* Distinctness wrt. << and =                                              *)
     2.5  (* ------------------------------------------------------------------------*)
     2.6  
     2.7 -fun prover contrfun thm = prove_goal Dnat.thy thm
     2.8 +val temp = prove_goal Dnat.thy  "~dzero << dsucc[n]"
     2.9 + (fn prems =>
    2.10 +	[
    2.11 +	(res_inst_tac [("P1","TT << FF")] classical3 1),
    2.12 +	(resolve_tac dist_less_tr 1),
    2.13 +	(dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
    2.14 +	(etac box_less 1),
    2.15 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    2.16 +	(res_inst_tac [("Q","n=UU")] classical2 1),
    2.17 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    2.18 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
    2.19 +	]);
    2.20 +
    2.21 +val dnat_dist_less = [temp];
    2.22 +
    2.23 +val temp = prove_goal Dnat.thy  "n~=UU ==> ~dsucc[n] << dzero"
    2.24   (fn prems =>
    2.25  	[
    2.26  	(cut_facts_tac prems 1),
    2.27  	(res_inst_tac [("P1","TT << FF")] classical3 1),
    2.28  	(resolve_tac dist_less_tr 1),
    2.29 -	(dres_inst_tac [("fo5",contrfun)] monofun_cfun_arg 1),
    2.30 +	(dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
    2.31  	(etac box_less 1),
    2.32  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    2.33  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
    2.34  	]);
    2.35  
    2.36 -val dnat_dist_less = 
    2.37 -	[
    2.38 -prover "is_dzero" "n~=UU ==> ~dzero << dsucc[n]",
    2.39 -prover "is_dsucc" "n~=UU ==> ~dsucc[n] << dzero"
    2.40 -	];
    2.41 +val dnat_dist_less = temp::dnat_dist_less;
    2.42  
    2.43 -fun prover contrfun thm = prove_goal Dnat.thy thm
    2.44 +val temp = prove_goal Dnat.thy   "dzero ~= dsucc[n]"
    2.45   (fn prems =>
    2.46  	[
    2.47 -	(cut_facts_tac prems 1),
    2.48 +	(res_inst_tac [("Q","n=UU")] classical2 1),
    2.49 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    2.50  	(res_inst_tac [("P1","TT = FF")] classical3 1),
    2.51  	(resolve_tac dist_eq_tr 1),
    2.52 -	(dres_inst_tac [("f",contrfun)] cfun_arg_cong 1),
    2.53 +	(dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
    2.54  	(etac box_equals 1),
    2.55  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
    2.56  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
    2.57  	]);
    2.58  
    2.59 -val dnat_dist_eq = 
    2.60 -	[
    2.61 -prover "is_dzero" "n~=UU ==> dzero ~= dsucc[n]",
    2.62 -prover "is_dsucc" "n~=UU ==> dsucc[n] ~= dzero"
    2.63 -	];
    2.64 +val dnat_dist_eq = [temp, temp RS not_sym];
    2.65  
    2.66  val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
    2.67  
    2.68 @@ -271,39 +279,57 @@
    2.69  (* ------------------------------------------------------------------------*)
    2.70  (* Properties dnat_take                                                    *)
    2.71  (* ------------------------------------------------------------------------*)
    2.72 -
    2.73 -val dnat_take =
    2.74 -	[
    2.75 -prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU"
    2.76 +val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU"
    2.77   (fn prems =>
    2.78  	[
    2.79  	(res_inst_tac [("n","n")] natE 1),
    2.80  	(asm_simp_tac iterate_ss 1),
    2.81  	(asm_simp_tac iterate_ss 1),
    2.82  	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
    2.83 -	]),
    2.84 -prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
    2.85 +	]);
    2.86 +
    2.87 +val dnat_take = [temp];
    2.88 +
    2.89 +val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
    2.90   (fn prems =>
    2.91  	[
    2.92  	(asm_simp_tac iterate_ss 1)
    2.93 -	])];
    2.94 +	]);
    2.95  
    2.96 -fun prover thm = prove_goalw Dnat.thy [dnat_take_def] thm
    2.97 +val dnat_take = temp::dnat_take;
    2.98 +
    2.99 +val temp = prove_goalw Dnat.thy [dnat_take_def]
   2.100 +	"dnat_take(Suc(n))[dzero]=dzero"
   2.101   (fn prems =>
   2.102  	[
   2.103 -	(cut_facts_tac prems 1),
   2.104 -	(simp_tac iterate_ss 1),
   2.105 +	(asm_simp_tac iterate_ss 1),
   2.106 +	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   2.107 +	]);
   2.108 +
   2.109 +val dnat_take = temp::dnat_take;
   2.110 +
   2.111 +val temp = prove_goalw Dnat.thy [dnat_take_def]
   2.112 +  "dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
   2.113 + (fn prems =>
   2.114 +	[
   2.115 +	(res_inst_tac [("Q","xs=UU")] classical2 1),
   2.116 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.117 +	(asm_simp_tac iterate_ss 1),
   2.118 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.119 +	(res_inst_tac [("n","n")] natE 1),
   2.120 +	(asm_simp_tac iterate_ss 1),
   2.121 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.122 +	(asm_simp_tac iterate_ss 1),
   2.123 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.124 +	(asm_simp_tac iterate_ss 1),
   2.125  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   2.126  	]);
   2.127  
   2.128 -val dnat_take = [
   2.129 -prover "dnat_take(Suc(n))[dzero]=dzero",
   2.130 -prover "xs~=UU ==> dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
   2.131 -	] @ dnat_take;
   2.132 -
   2.133 +val dnat_take = temp::dnat_take;
   2.134  
   2.135  val dnat_rews = dnat_take @ dnat_rews;
   2.136  
   2.137 +
   2.138  (* ------------------------------------------------------------------------*)
   2.139  (* take lemma for dnats                                                  *)
   2.140  (* ------------------------------------------------------------------------*)
   2.141 @@ -368,6 +394,7 @@
   2.142  (* structural induction for admissible predicates                          *)
   2.143  (* ------------------------------------------------------------------------*)
   2.144  
   2.145 +(* not needed any longer
   2.146  val dnat_ind = prove_goal Dnat.thy
   2.147  "[| adm(P);\
   2.148  \   P(UU);\
   2.149 @@ -397,6 +424,79 @@
   2.150  	(eresolve_tac prems 1),
   2.151  	(etac spec 1)
   2.152  	]);
   2.153 +*)
   2.154 +
   2.155 +val dnat_finite_ind = prove_goal Dnat.thy
   2.156 +"[|P(UU);P(dzero);\
   2.157 +\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
   2.158 +\  |] ==> !s.P(dnat_take(n)[s])"
   2.159 + (fn prems =>
   2.160 +	[
   2.161 +	(nat_ind_tac "n" 1),
   2.162 +	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.163 +	(resolve_tac prems 1),
   2.164 +	(rtac allI 1),
   2.165 +	(res_inst_tac [("n","s")] dnatE 1),
   2.166 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.167 +	(resolve_tac prems 1),
   2.168 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.169 +	(resolve_tac prems 1),
   2.170 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.171 +	(res_inst_tac [("Q","dnat_take(n1)[x]=UU")] classical2 1),
   2.172 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.173 +	(resolve_tac prems 1),
   2.174 +	(resolve_tac prems 1),
   2.175 +	(atac 1),
   2.176 +	(etac spec 1)
   2.177 +	]);
   2.178 +
   2.179 +val dnat_all_finite_lemma1 = prove_goal Dnat.thy
   2.180 +"!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s"
   2.181 + (fn prems =>
   2.182 +	[
   2.183 +	(nat_ind_tac "n" 1),
   2.184 +	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.185 +	(rtac allI 1),
   2.186 +	(res_inst_tac [("n","s")] dnatE 1),
   2.187 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.188 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.189 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.190 +	(eres_inst_tac [("x","x")] allE 1),
   2.191 +	(etac disjE 1),
   2.192 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.193 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   2.194 +	]);
   2.195 +
   2.196 +val dnat_all_finite_lemma2 = prove_goal Dnat.thy "? n.dnat_take(n)[s]=s"
   2.197 + (fn prems =>
   2.198 +	[
   2.199 +	(res_inst_tac [("Q","s=UU")] classical2 1),
   2.200 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.201 +	(subgoal_tac "(!n.dnat_take(n)[s]=UU) |(? n.dnat_take(n)[s]=s)" 1),
   2.202 +	(etac disjE 1),
   2.203 +	(eres_inst_tac [("P","s=UU")] notE 1),
   2.204 +	(rtac dnat_take_lemma 1),
   2.205 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.206 +	(atac 1),
   2.207 +	(subgoal_tac "!n.!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s" 1),
   2.208 +	(fast_tac HOL_cs 1),
   2.209 +	(rtac allI 1),
   2.210 +	(rtac dnat_all_finite_lemma1 1)
   2.211 +	]);
   2.212 +
   2.213 +
   2.214 +val dnat_ind = prove_goal Dnat.thy
   2.215 +"[|P(UU);P(dzero);\
   2.216 +\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
   2.217 +\  |] ==> P(s)"
   2.218 + (fn prems =>
   2.219 +	[
   2.220 +	(rtac (dnat_all_finite_lemma2 RS exE) 1),
   2.221 +	(etac subst 1),
   2.222 +	(rtac (dnat_finite_ind RS spec) 1),
   2.223 +	(REPEAT (resolve_tac prems 1)),
   2.224 +	(REPEAT (atac 1))
   2.225 +	]);
   2.226  
   2.227  
   2.228  val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(dzero)"
   2.229 @@ -404,12 +504,6 @@
   2.230  	[
   2.231  	(rtac allI 1),
   2.232  	(res_inst_tac [("s","x")] dnat_ind 1),
   2.233 -	(REPEAT (resolve_tac adm_thms 1)),
   2.234 -	(contX_tacR 1),
   2.235 -	(REPEAT (resolve_tac adm_thms 1)),
   2.236 -	(contX_tacR 1),
   2.237 -	(REPEAT (resolve_tac adm_thms 1)),
   2.238 -	(contX_tacR 1),
   2.239  	(fast_tac HOL_cs 1),
   2.240  	(rtac allI 1),
   2.241  	(res_inst_tac [("n","y")] dnatE 1),
   2.242 @@ -419,53 +513,20 @@
   2.243  	(rtac allI 1),
   2.244  	(res_inst_tac [("n","y")] dnatE 1),
   2.245  	(fast_tac (HOL_cs addSIs [UU_I]) 1),
   2.246 +	(asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
   2.247  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.248 -	(hyp_subst_tac 1),
   2.249  	(strip_tac 1),
   2.250 -	(rtac disjI2 1),
   2.251 -	(forward_tac dnat_invert 1),
   2.252 -	(atac 2),
   2.253 -	(atac 1),
   2.254 +	(subgoal_tac "s1<<xa" 1),
   2.255  	(etac allE 1),
   2.256  	(dtac mp 1),
   2.257  	(atac 1),
   2.258  	(etac disjE 1),
   2.259  	(contr_tac 1),
   2.260 -	(asm_simp_tac HOLCF_ss 1)
   2.261 +	(asm_simp_tac HOLCF_ss 1),
   2.262 +	(resolve_tac  dnat_invert 1),
   2.263 +	(REPEAT (atac 1))
   2.264  	]);
   2.265  
   2.266 -val dnat_ind = prove_goal Dnat.thy
   2.267 -"[| adm(P);\
   2.268 -\   P(UU);\
   2.269 -\   P(dzero);\
   2.270 -\   !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)"
   2.271 - (fn prems =>
   2.272 -	[
   2.273 -	(rtac (dnat_reach RS subst) 1),
   2.274 -	(res_inst_tac [("x","s")] spec 1),
   2.275 -	(rtac fix_ind 1),
   2.276 -	(rtac adm_all2 1),
   2.277 -	(rtac adm_subst 1),
   2.278 -	(contX_tacR 1),
   2.279 -	(resolve_tac prems 1),
   2.280 -	(simp_tac HOLCF_ss 1),
   2.281 -	(resolve_tac prems 1),
   2.282 -	(strip_tac 1),
   2.283 -	(res_inst_tac [("n","xa")] dnatE 1),
   2.284 -	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
   2.285 -	(resolve_tac prems 1),
   2.286 -	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
   2.287 -	(resolve_tac prems 1),
   2.288 -	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
   2.289 -	(res_inst_tac [("Q","x[xb]=UU")] classical2 1),
   2.290 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   2.291 -	(resolve_tac prems 1),
   2.292 -	(eresolve_tac prems 1),
   2.293 -	(etac spec 1)
   2.294 -	]);
   2.295 +
   2.296  
   2.297 -val dnat_ind2 = dnat_flat RS adm_flat RS dnat_ind;
   2.298 -(*  "[| ?P(UU); ?P(dzero);
   2.299 -    !!s1. [| s1 ~= UU; ?P(s1) |] ==> ?P(dsucc[s1]) |] ==> ?P(?s)" : thm
   2.300 -*)
   2.301  
     3.1 --- a/src/HOLCF/Fix.ML	Thu Mar 24 13:25:12 1994 +0100
     3.2 +++ b/src/HOLCF/Fix.ML	Thu Mar 24 13:36:34 1994 +0100
     3.3 @@ -387,6 +387,19 @@
     3.4          (rtac refl 1)
     3.5          ]);
     3.6  
     3.7 +(* ------------------------------------------------------------------------ 
     3.8 +
     3.9 +given the definition
    3.10 +
    3.11 +smap_def
    3.12 +  "smap = fix[LAM h f s. stream_when[LAM x l.scons[f[x]][h[f][l]]][s]]"
    3.13 +
    3.14 +use fix_prover for 
    3.15 +
    3.16 +val smap_def2 = fix_prover Stream2.thy smap_def 
    3.17 +        "smap = (LAM f s. stream_when[LAM x l.scons[f[x]][smap[f][l]]][s])";
    3.18 +
    3.19 +   ------------------------------------------------------------------------ *)
    3.20  
    3.21  (* ------------------------------------------------------------------------ *)
    3.22  (* better access to definitions                                             *)
    3.23 @@ -881,7 +894,7 @@
    3.24  	(rtac iffI 1),
    3.25  	(etac FalseE 2),
    3.26  	(rtac notE 1),
    3.27 -	(etac less_not_sym 1),	
    3.28 +	(etac (less_not_sym RS mp) 1),	
    3.29  	(atac 1),
    3.30  	(asm_simp_tac Cfun_ss  1),
    3.31  	(etac (is_chainE RS spec) 1),
    3.32 @@ -921,7 +934,7 @@
    3.33  	(rtac iffI 1),
    3.34  	(etac FalseE 2),
    3.35  	(rtac notE 1),
    3.36 -	(etac less_not_sym 1),	
    3.37 +	(etac (less_not_sym RS mp) 1),	
    3.38  	(atac 1),
    3.39  	(asm_simp_tac nat_ss 1),
    3.40  	(dtac spec 1),
     4.1 --- a/src/HOLCF/Porder.ML	Thu Mar 24 13:25:12 1994 +0100
     4.2 +++ b/src/HOLCF/Porder.ML	Thu Mar 24 13:36:34 1994 +0100
     4.3 @@ -6,9 +6,9 @@
     4.4  Lemmas for theory porder.thy 
     4.5  *)
     4.6  
     4.7 +open Porder0;
     4.8  open Porder;
     4.9  
    4.10 -
    4.11  val box_less = prove_goal Porder.thy 
    4.12  "[| a << b; c << a; b << d|] ==> c << d"
    4.13   (fn prems =>
     5.1 --- a/src/HOLCF/Porder.thy	Thu Mar 24 13:25:12 1994 +0100
     5.2 +++ b/src/HOLCF/Porder.thy	Thu Mar 24 13:36:34 1994 +0100
     5.3 @@ -3,25 +3,13 @@
     5.4      Author: 	Franz Regensburger
     5.5      Copyright   1993 Technische Universitaet Muenchen
     5.6  
     5.7 -Definition of class porder (partial order)
     5.8 -
     5.9 -The prototype theory for this class is void.thy 
    5.10 +Conservative extension of theory Porder0 by constant definitions 
    5.11  
    5.12  *)
    5.13  
    5.14 -Porder = Void +
    5.15 -
    5.16 -(* Introduction of new class. The witness is type void. *)
    5.17 -
    5.18 -classes po < term
    5.19 +Porder = Porder0 +
    5.20  
    5.21 -(* default type is still term ! *)
    5.22 -(* void is the prototype in po *)
    5.23 -
    5.24 -arities void :: po
    5.25 -
    5.26 -consts	"<<"	::	"['a,'a::po] => bool"	(infixl 55)
    5.27 -
    5.28 +consts	
    5.29  	"<|"	::	"['a set,'a::po] => bool"	(infixl 55)
    5.30  	"<<|"	::	"['a set,'a::po] => bool"	(infixl 55)
    5.31  	lub	::	"'a set => 'a::po"
    5.32 @@ -32,21 +20,6 @@
    5.33  
    5.34  rules
    5.35  
    5.36 -(* class axioms: justification is theory Void *)
    5.37 -
    5.38 -refl_less	"x << x"	
    5.39 -				(* witness refl_less_void    *)
    5.40 -
    5.41 -antisym_less	"[|x<<y ; y<<x |] ==> x = y"	
    5.42 -				(* witness antisym_less_void *)
    5.43 -
    5.44 -trans_less	"[|x<<y ; y<<z |] ==> x<<z"
    5.45 -				(* witness trans_less_void   *)
    5.46 -
    5.47 -(* instance of << for the prototype void *)
    5.48 -
    5.49 -inst_void_po	"(op <<)::[void,void]=>bool = less_void"
    5.50 -
    5.51  (* class definitions *)
    5.52  
    5.53  is_ub		"S  <| x == ! y.y:S --> y<<x"
    5.54 @@ -57,11 +30,9 @@
    5.55  (* Arbitrary chains are total orders    *)                  
    5.56  is_tord		"is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
    5.57  
    5.58 -
    5.59  (* Here we use countable chains and I prefer to code them as functions! *)
    5.60  is_chain	"is_chain(F) == (! i.F(i) << F(Suc(i)))"
    5.61  
    5.62 -
    5.63  (* finite chains, needed for monotony of continouous functions *)
    5.64  
    5.65  max_in_chain_def "max_in_chain(i,C) == ! j. i <= j --> C(i) = C(j)" 
     6.1 --- a/src/HOLCF/ROOT.ML	Thu Mar 24 13:25:12 1994 +0100
     6.2 +++ b/src/HOLCF/ROOT.ML	Thu Mar 24 13:36:34 1994 +0100
     6.3 @@ -17,7 +17,10 @@
     6.4  
     6.5  use_thy "Holcfb";
     6.6  use_thy "Void";
     6.7 +
     6.8 +use_thy "Porder0";
     6.9  use_thy "Porder";
    6.10 +
    6.11  use_thy "Pcpo";
    6.12  
    6.13  use_thy "Fun1";
    6.14 @@ -61,6 +64,8 @@
    6.15  use_thy "Dnat2";
    6.16  use_thy "Stream";
    6.17  use_thy "Stream2";
    6.18 +use_thy "Dlist";
    6.19 +
    6.20  
    6.21  use "../Pure/install_pp.ML";
    6.22  print_depth 8;  
     7.1 --- a/src/HOLCF/Stream.ML	Thu Mar 24 13:25:12 1994 +0100
     7.2 +++ b/src/HOLCF/Stream.ML	Thu Mar 24 13:36:34 1994 +0100
     7.3 @@ -229,6 +229,7 @@
     7.4  
     7.5  val stream_rews = stream_discsel_def @ stream_rews;
     7.6  
     7.7 +
     7.8  (* ------------------------------------------------------------------------*)
     7.9  (* Properties stream_take                                                  *)
    7.10  (* ------------------------------------------------------------------------*)
    7.11 @@ -265,6 +266,46 @@
    7.12  val stream_rews = stream_take @ stream_rews;
    7.13  
    7.14  (* ------------------------------------------------------------------------*)
    7.15 +(* enhance the simplifier                                                  *)
    7.16 +(* ------------------------------------------------------------------------*)
    7.17 +
    7.18 +val stream_copy2 = prove_goal Stream.thy 
    7.19 +     "stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
    7.20 + (fn prems =>
    7.21 +	[
    7.22 +	(res_inst_tac [("Q","x=UU")] classical2 1),
    7.23 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
    7.24 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
    7.25 +	]);
    7.26 +
    7.27 +val shd2 = prove_goal Stream.thy "shd[scons[x][xs]]=x"
    7.28 + (fn prems =>
    7.29 +	[
    7.30 +	(res_inst_tac [("Q","x=UU")] classical2 1),
    7.31 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
    7.32 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
    7.33 +	]);
    7.34 +
    7.35 +val stream_take2 = prove_goal Stream.thy 
    7.36 + "stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
    7.37 + (fn prems =>
    7.38 +	[
    7.39 +	(res_inst_tac [("Q","x=UU")] classical2 1),
    7.40 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
    7.41 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
    7.42 +	]);
    7.43 +
    7.44 +val stream_rews = [stream_iso_strict RS conjunct1,
    7.45 +		   stream_iso_strict RS conjunct2,
    7.46 +                   hd stream_copy, stream_copy2]
    7.47 +                  @ stream_when
    7.48 +                  @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))  
    7.49 +                  @ stream_constrdef
    7.50 +                  @ stream_discsel_def
    7.51 +                  @ [ stream_take2] @ (tl stream_take);
    7.52 +
    7.53 +
    7.54 +(* ------------------------------------------------------------------------*)
    7.55  (* take lemma for streams                                                  *)
    7.56  (* ------------------------------------------------------------------------*)
    7.57  
    7.58 @@ -326,8 +367,49 @@
    7.59  (* structural induction for admissible predicates                          *)
    7.60  (* ------------------------------------------------------------------------*)
    7.61  
    7.62 +val stream_finite_ind = prove_goal Stream.thy
    7.63 +"[|P(UU);\
    7.64 +\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
    7.65 +\  |] ==> !s.P(stream_take(n)[s])"
    7.66 + (fn prems =>
    7.67 +	[
    7.68 +	(nat_ind_tac "n" 1),
    7.69 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
    7.70 +	(resolve_tac prems 1),
    7.71 +	(rtac allI 1),
    7.72 +	(res_inst_tac [("s","s")] streamE 1),
    7.73 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
    7.74 +	(resolve_tac prems 1),
    7.75 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
    7.76 +	(resolve_tac prems 1),
    7.77 +	(atac 1),
    7.78 +	(etac spec 1)
    7.79 +	]);
    7.80 +
    7.81 +val stream_finite_ind2 = prove_goalw Stream.thy  [stream_finite_def]
    7.82 +"(!!n.P(stream_take(n)[s])) ==>  stream_finite(s) -->P(s)"
    7.83 + (fn prems =>
    7.84 +	[
    7.85 +	(strip_tac 1),
    7.86 +	(etac exE 1),
    7.87 +	(etac subst 1),
    7.88 +	(resolve_tac prems 1)
    7.89 +	]);
    7.90 +
    7.91 +val stream_finite_ind3 = prove_goal Stream.thy 
    7.92 +"[|P(UU);\
    7.93 +\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
    7.94 +\  |] ==> stream_finite(s) --> P(s)"
    7.95 + (fn prems =>
    7.96 +	[
    7.97 +	(rtac stream_finite_ind2 1),
    7.98 +	(rtac (stream_finite_ind RS spec) 1),
    7.99 +	(REPEAT (resolve_tac prems 1)),
   7.100 +	(REPEAT (atac 1))
   7.101 +	]);
   7.102 +
   7.103  val stream_ind = prove_goal Stream.thy
   7.104 -"[| adm(P);\
   7.105 +"[|adm(P);\
   7.106  \  P(UU);\
   7.107  \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   7.108  \  |] ==> P(s)"
   7.109 @@ -335,21 +417,16 @@
   7.110  	[
   7.111  	(rtac (stream_reach RS subst) 1),
   7.112  	(res_inst_tac [("x","s")] spec 1),
   7.113 -	(rtac fix_ind 1),
   7.114 -	(rtac (allI RS adm_all) 1),
   7.115 +	(rtac wfix_ind 1),
   7.116 +	(rtac adm_impl_admw 1),
   7.117 +	(REPEAT (resolve_tac adm_thms 1)),
   7.118  	(rtac adm_subst 1),
   7.119  	(contX_tacR 1),
   7.120  	(resolve_tac prems 1),
   7.121 -	(simp_tac HOLCF_ss 1),
   7.122 -	(resolve_tac prems 1),
   7.123 -	(strip_tac 1),
   7.124 -	(res_inst_tac [("s","xa")] streamE 1),
   7.125 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.126 -	(resolve_tac prems 1),
   7.127 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.128 -	(resolve_tac prems 1),
   7.129 -	(atac 1),
   7.130 -	(etac spec 1)
   7.131 +	(rtac allI 1),
   7.132 +	(rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
   7.133 +	(REPEAT (resolve_tac prems 1)),
   7.134 +	(REPEAT (atac 1))
   7.135  	]);
   7.136  
   7.137  
   7.138 @@ -403,3 +480,312 @@
   7.139  	]);
   7.140  
   7.141  
   7.142 +(* ------------------------------------------------------------------------*)
   7.143 +(* theorems about finite and infinite streams                              *)
   7.144 +(* ------------------------------------------------------------------------*)
   7.145 +
   7.146 +(* ----------------------------------------------------------------------- *)
   7.147 +(* 2 lemmas about stream_finite                                            *)
   7.148 +(* ----------------------------------------------------------------------- *)
   7.149 +
   7.150 +val stream_finite_UU = prove_goalw Stream.thy [stream_finite_def]
   7.151 +	 "stream_finite(UU)"
   7.152 + (fn prems =>
   7.153 +	[
   7.154 +	(rtac exI 1),
   7.155 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   7.156 +	]);
   7.157 +
   7.158 +val inf_stream_not_UU = prove_goal Stream.thy  "~stream_finite(s)  ==> s ~= UU"
   7.159 + (fn prems =>
   7.160 +	[
   7.161 +	(cut_facts_tac prems 1),
   7.162 +	(etac swap 1),
   7.163 +	(dtac notnotD 1),
   7.164 +	(hyp_subst_tac  1),
   7.165 +	(rtac stream_finite_UU 1)
   7.166 +	]);
   7.167 +
   7.168 +(* ----------------------------------------------------------------------- *)
   7.169 +(* a lemma about shd                                                       *)
   7.170 +(* ----------------------------------------------------------------------- *)
   7.171 +
   7.172 +val stream_shd_lemma1 = prove_goal Stream.thy "shd[s]=UU --> s=UU"
   7.173 + (fn prems =>
   7.174 +	[
   7.175 +	(res_inst_tac [("s","s")] streamE 1),
   7.176 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.177 +	(hyp_subst_tac 1),
   7.178 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   7.179 +	]);
   7.180 +
   7.181 +
   7.182 +(* ----------------------------------------------------------------------- *)
   7.183 +(* lemmas about stream_take                                                *)
   7.184 +(* ----------------------------------------------------------------------- *)
   7.185 +
   7.186 +val stream_take_lemma1 = prove_goal Stream.thy 
   7.187 + "!x xs.x~=UU --> \
   7.188 +\  stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
   7.189 + (fn prems =>
   7.190 +	[
   7.191 +	(rtac allI 1),
   7.192 +	(rtac allI 1),
   7.193 +	(rtac impI 1),
   7.194 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.195 +	(strip_tac 1),
   7.196 +	(rtac ((hd stream_inject) RS conjunct2) 1),
   7.197 +	(atac 1),
   7.198 +	(atac 1),
   7.199 +	(atac 1)
   7.200 +	]);
   7.201 +
   7.202 +
   7.203 +val stream_take_lemma2 = prove_goal Stream.thy 
   7.204 + "! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
   7.205 + (fn prems =>
   7.206 +	[
   7.207 +	(nat_ind_tac "n" 1),
   7.208 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.209 +	(strip_tac 1 ),
   7.210 +	(hyp_subst_tac  1),
   7.211 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.212 +	(rtac allI 1),
   7.213 +	(res_inst_tac [("s","s2")] streamE 1),
   7.214 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.215 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.216 +	(strip_tac 1 ),
   7.217 +	(subgoal_tac "stream_take(n1)[xs] = xs" 1),
   7.218 +	(rtac ((hd stream_inject) RS conjunct2) 2),
   7.219 +	(atac 4),
   7.220 +	(atac 2),
   7.221 +	(atac 2),
   7.222 +	(rtac cfun_arg_cong 1),
   7.223 +	(fast_tac HOL_cs 1)
   7.224 +	]);
   7.225 +
   7.226 +val stream_take_lemma3 = prove_goal Stream.thy 
   7.227 + "!x xs.x~=UU --> \
   7.228 +\  stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
   7.229 + (fn prems =>
   7.230 +	[
   7.231 +	(nat_ind_tac "n" 1),
   7.232 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.233 +	(strip_tac 1 ),
   7.234 +	(res_inst_tac [("P","scons[x][xs]=UU")] notE 1),
   7.235 +	(eresolve_tac stream_constrdef 1),
   7.236 +	(etac sym 1),
   7.237 +	(strip_tac 1 ),
   7.238 +	(rtac (stream_take_lemma2 RS spec RS mp) 1),
   7.239 +	(res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
   7.240 +	(atac 1),
   7.241 +	(atac 1),
   7.242 +	(etac (stream_take2 RS subst) 1)
   7.243 +	]);
   7.244 +
   7.245 +val stream_take_lemma4 = prove_goal Stream.thy 
   7.246 + "!x xs.\
   7.247 +\stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
   7.248 + (fn prems =>
   7.249 +	[
   7.250 +	(nat_ind_tac "n" 1),
   7.251 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.252 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
   7.253 +	]);
   7.254 +
   7.255 +(* ---- *)
   7.256 +
   7.257 +val stream_take_lemma5 = prove_goal Stream.thy 
   7.258 +"!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
   7.259 + (fn prems =>
   7.260 +	[
   7.261 +	(nat_ind_tac "n" 1),
   7.262 +	(simp_tac iterate_ss 1),
   7.263 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.264 +	(strip_tac 1),
   7.265 +	(res_inst_tac [("s","s")] streamE 1),
   7.266 +	(hyp_subst_tac 1),
   7.267 +	(rtac (iterate_Suc2 RS ssubst) 1),
   7.268 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.269 +	(rtac (iterate_Suc2 RS ssubst) 1),
   7.270 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.271 +	(etac allE 1),
   7.272 +	(etac mp 1),
   7.273 +	(hyp_subst_tac 1),
   7.274 +	(etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
   7.275 +	(atac 1)
   7.276 +	]);
   7.277 +
   7.278 +val stream_take_lemma6 = prove_goal Stream.thy 
   7.279 +"!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
   7.280 + (fn prems =>
   7.281 +	[
   7.282 +	(nat_ind_tac "n" 1),
   7.283 +	(simp_tac iterate_ss 1),
   7.284 +	(strip_tac 1),
   7.285 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.286 +	(rtac allI 1),
   7.287 +	(res_inst_tac [("s","s")] streamE 1),
   7.288 +	(hyp_subst_tac 1),
   7.289 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.290 +	(hyp_subst_tac 1),
   7.291 +	(rtac (iterate_Suc2 RS ssubst) 1),
   7.292 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   7.293 +	]);
   7.294 +
   7.295 +val stream_take_lemma7 = prove_goal Stream.thy 
   7.296 +"(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
   7.297 + (fn prems =>
   7.298 +	[
   7.299 +	(rtac iffI 1),
   7.300 +	(etac (stream_take_lemma6 RS spec RS mp) 1),
   7.301 +	(etac (stream_take_lemma5 RS spec RS mp) 1)
   7.302 +	]);
   7.303 +
   7.304 +
   7.305 +(* ----------------------------------------------------------------------- *)
   7.306 +(* lemmas stream_finite                                                    *)
   7.307 +(* ----------------------------------------------------------------------- *)
   7.308 +
   7.309 +val stream_finite_lemma1 = prove_goalw Stream.thy [stream_finite_def]
   7.310 + "stream_finite(xs) ==> stream_finite(scons[x][xs])"
   7.311 + (fn prems =>
   7.312 +	[
   7.313 +	(cut_facts_tac prems 1),
   7.314 +	(etac exE 1),
   7.315 +	(rtac exI 1),
   7.316 +	(etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
   7.317 +	]);
   7.318 +
   7.319 +val stream_finite_lemma2 = prove_goalw Stream.thy [stream_finite_def]
   7.320 + "[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
   7.321 + (fn prems =>
   7.322 +	[
   7.323 +	(cut_facts_tac prems 1),
   7.324 +	(etac exE 1),
   7.325 +	(rtac exI 1),
   7.326 +	(etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
   7.327 +	(atac 1)
   7.328 +	]);
   7.329 +
   7.330 +val stream_finite_lemma3 = prove_goal Stream.thy 
   7.331 + "x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
   7.332 + (fn prems =>
   7.333 +	[
   7.334 +	(cut_facts_tac prems 1),
   7.335 +	(rtac iffI 1),
   7.336 +	(etac stream_finite_lemma2 1),
   7.337 +	(atac 1),
   7.338 +	(etac stream_finite_lemma1 1)
   7.339 +	]);
   7.340 +
   7.341 +
   7.342 +val stream_finite_lemma5 = prove_goalw Stream.thy [stream_finite_def]
   7.343 + "(!n. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
   7.344 +\=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
   7.345 + (fn prems =>
   7.346 +	[
   7.347 +	(rtac iffI 1),
   7.348 +	(fast_tac HOL_cs 1),
   7.349 +	(fast_tac HOL_cs 1)
   7.350 +	]);
   7.351 +
   7.352 +val stream_finite_lemma6 = prove_goal Stream.thy
   7.353 + "!s1 s2. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
   7.354 + (fn prems =>
   7.355 +	[
   7.356 +	(nat_ind_tac "n" 1),
   7.357 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.358 +	(strip_tac 1 ),
   7.359 +	(hyp_subst_tac  1),
   7.360 +	(dtac UU_I 1),
   7.361 +	(hyp_subst_tac  1),
   7.362 +	(rtac stream_finite_UU 1),
   7.363 +	(rtac allI 1),
   7.364 +	(rtac allI 1),
   7.365 +	(res_inst_tac [("s","s1")] streamE 1),
   7.366 +	(hyp_subst_tac  1),
   7.367 +	(strip_tac 1 ),
   7.368 +	(rtac stream_finite_UU 1),
   7.369 +	(hyp_subst_tac  1),
   7.370 +	(res_inst_tac [("s","s2")] streamE 1),
   7.371 +	(hyp_subst_tac  1),
   7.372 +	(strip_tac 1 ),
   7.373 +	(dtac UU_I 1),
   7.374 +	(asm_simp_tac(HOLCF_ss addsimps (stream_rews @ [stream_finite_UU])) 1),
   7.375 +	(hyp_subst_tac  1),
   7.376 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   7.377 +	(strip_tac 1 ),
   7.378 +	(rtac stream_finite_lemma1 1),
   7.379 +	(subgoal_tac "xs << xsa" 1),
   7.380 +	(subgoal_tac "stream_take(n1)[xsa] = xsa" 1),
   7.381 +	(fast_tac HOL_cs 1),
   7.382 +	(res_inst_tac  [("x1.1","xa"),("y1.1","xa")] 
   7.383 +                   ((hd stream_inject) RS conjunct2) 1),
   7.384 +	(atac 1),
   7.385 +	(atac 1),
   7.386 +	(atac 1),
   7.387 +	(res_inst_tac [("x1.1","x"),("y1.1","xa")]
   7.388 +	 ((hd stream_invert) RS conjunct2) 1),
   7.389 +	(atac 1),
   7.390 +	(atac 1),
   7.391 +	(atac 1)
   7.392 +	]);
   7.393 +
   7.394 +val stream_finite_lemma7 = prove_goal Stream.thy 
   7.395 +"s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
   7.396 + (fn prems =>
   7.397 +	[
   7.398 +	(rtac (stream_finite_lemma5 RS iffD1) 1),
   7.399 +	(rtac allI 1),
   7.400 +	(rtac (stream_finite_lemma6 RS spec RS spec) 1)
   7.401 +	]);
   7.402 +
   7.403 +val stream_finite_lemma8 = prove_goalw Stream.thy [stream_finite_def]
   7.404 +"stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
   7.405 + (fn prems =>
   7.406 +	[
   7.407 +	(simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
   7.408 +	]);
   7.409 +
   7.410 +
   7.411 +(* ----------------------------------------------------------------------- *)
   7.412 +(* admissibility of ~stream_finite                                         *)
   7.413 +(* ----------------------------------------------------------------------- *)
   7.414 +
   7.415 +val adm_not_stream_finite = prove_goalw Stream.thy [adm_def]
   7.416 + "adm(%s. ~ stream_finite(s))"
   7.417 + (fn prems =>
   7.418 +	[
   7.419 +	(strip_tac 1 ),
   7.420 +	(res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),
   7.421 +	(atac 2),
   7.422 +	(subgoal_tac "!i.stream_finite(Y(i))" 1),
   7.423 +	(fast_tac HOL_cs 1),
   7.424 +	(rtac allI 1),
   7.425 +	(rtac (stream_finite_lemma7 RS mp RS mp) 1),
   7.426 +	(etac is_ub_thelub 1),
   7.427 +	(atac 1)
   7.428 +	]);
   7.429 +
   7.430 +(* ----------------------------------------------------------------------- *)
   7.431 +(* alternative prove for admissibility of ~stream_finite                   *)
   7.432 +(* show that stream_finite(s) = (? n. iterate(n, stl, s) = UU)             *)
   7.433 +(* and prove adm. of ~(? n. iterate(n, stl, s) = UU)                       *)
   7.434 +(* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
   7.435 +(* ----------------------------------------------------------------------- *)
   7.436 +
   7.437 +
   7.438 +val adm_not_stream_finite2=prove_goal Stream.thy "adm(%s. ~ stream_finite(s))"
   7.439 + (fn prems =>
   7.440 +	[
   7.441 +	(subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
   7.442 +	(etac (adm_cong RS iffD2)1),
   7.443 +	(REPEAT(resolve_tac adm_thms 1)),
   7.444 +	(rtac  contX_iterate2 1),
   7.445 +	(rtac allI 1),
   7.446 +	(rtac (stream_finite_lemma8 RS ssubst) 1),
   7.447 +	(fast_tac HOL_cs 1)
   7.448 +	]);
   7.449 +
   7.450 +
     8.1 --- a/src/HOLCF/Stream2.thy	Thu Mar 24 13:25:12 1994 +0100
     8.2 +++ b/src/HOLCF/Stream2.thy	Thu Mar 24 13:36:34 1994 +0100
     8.3 @@ -19,7 +19,7 @@
     8.4  
     8.5  
     8.6  end
     8.7 -
     8.8 +      
     8.9  
    8.10  (*
    8.11  		smap[f][UU] = UU
     9.1 --- a/src/HOLCF/cfun2.ML	Thu Mar 24 13:25:12 1994 +0100
     9.2 +++ b/src/HOLCF/cfun2.ML	Thu Mar 24 13:36:34 1994 +0100
     9.3 @@ -216,7 +216,7 @@
     9.4  is_chain(?CCF1) ==> lub(range(?CCF1)) = fabs(%x. lub(range(%i. ?CCF1(i)[x])))
     9.5  *)
     9.6  
     9.7 -val cpo_fun = prove_goal Cfun2.thy 
     9.8 +val cpo_cfun = prove_goal Cfun2.thy 
     9.9    "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
    9.10  (fn prems =>
    9.11  	[
    10.1 --- a/src/HOLCF/dnat.ML	Thu Mar 24 13:25:12 1994 +0100
    10.2 +++ b/src/HOLCF/dnat.ML	Thu Mar 24 13:36:34 1994 +0100
    10.3 @@ -171,41 +171,49 @@
    10.4  (* Distinctness wrt. << and =                                              *)
    10.5  (* ------------------------------------------------------------------------*)
    10.6  
    10.7 -fun prover contrfun thm = prove_goal Dnat.thy thm
    10.8 +val temp = prove_goal Dnat.thy  "~dzero << dsucc[n]"
    10.9 + (fn prems =>
   10.10 +	[
   10.11 +	(res_inst_tac [("P1","TT << FF")] classical3 1),
   10.12 +	(resolve_tac dist_less_tr 1),
   10.13 +	(dres_inst_tac [("fo5","is_dzero")] monofun_cfun_arg 1),
   10.14 +	(etac box_less 1),
   10.15 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   10.16 +	(res_inst_tac [("Q","n=UU")] classical2 1),
   10.17 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   10.18 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   10.19 +	]);
   10.20 +
   10.21 +val dnat_dist_less = [temp];
   10.22 +
   10.23 +val temp = prove_goal Dnat.thy  "n~=UU ==> ~dsucc[n] << dzero"
   10.24   (fn prems =>
   10.25  	[
   10.26  	(cut_facts_tac prems 1),
   10.27  	(res_inst_tac [("P1","TT << FF")] classical3 1),
   10.28  	(resolve_tac dist_less_tr 1),
   10.29 -	(dres_inst_tac [("fo5",contrfun)] monofun_cfun_arg 1),
   10.30 +	(dres_inst_tac [("fo5","is_dsucc")] monofun_cfun_arg 1),
   10.31  	(etac box_less 1),
   10.32  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   10.33  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   10.34  	]);
   10.35  
   10.36 -val dnat_dist_less = 
   10.37 -	[
   10.38 -prover "is_dzero" "n~=UU ==> ~dzero << dsucc[n]",
   10.39 -prover "is_dsucc" "n~=UU ==> ~dsucc[n] << dzero"
   10.40 -	];
   10.41 +val dnat_dist_less = temp::dnat_dist_less;
   10.42  
   10.43 -fun prover contrfun thm = prove_goal Dnat.thy thm
   10.44 +val temp = prove_goal Dnat.thy   "dzero ~= dsucc[n]"
   10.45   (fn prems =>
   10.46  	[
   10.47 -	(cut_facts_tac prems 1),
   10.48 +	(res_inst_tac [("Q","n=UU")] classical2 1),
   10.49 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   10.50  	(res_inst_tac [("P1","TT = FF")] classical3 1),
   10.51  	(resolve_tac dist_eq_tr 1),
   10.52 -	(dres_inst_tac [("f",contrfun)] cfun_arg_cong 1),
   10.53 +	(dres_inst_tac [("f","is_dzero")] cfun_arg_cong 1),
   10.54  	(etac box_equals 1),
   10.55  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
   10.56  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   10.57  	]);
   10.58  
   10.59 -val dnat_dist_eq = 
   10.60 -	[
   10.61 -prover "is_dzero" "n~=UU ==> dzero ~= dsucc[n]",
   10.62 -prover "is_dsucc" "n~=UU ==> dsucc[n] ~= dzero"
   10.63 -	];
   10.64 +val dnat_dist_eq = [temp, temp RS not_sym];
   10.65  
   10.66  val dnat_rews = dnat_dist_less @ dnat_dist_eq @ dnat_rews;
   10.67  
   10.68 @@ -271,39 +279,57 @@
   10.69  (* ------------------------------------------------------------------------*)
   10.70  (* Properties dnat_take                                                    *)
   10.71  (* ------------------------------------------------------------------------*)
   10.72 -
   10.73 -val dnat_take =
   10.74 -	[
   10.75 -prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU"
   10.76 +val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(n)[UU]=UU"
   10.77   (fn prems =>
   10.78  	[
   10.79  	(res_inst_tac [("n","n")] natE 1),
   10.80  	(asm_simp_tac iterate_ss 1),
   10.81  	(asm_simp_tac iterate_ss 1),
   10.82  	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
   10.83 -	]),
   10.84 -prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
   10.85 +	]);
   10.86 +
   10.87 +val dnat_take = [temp];
   10.88 +
   10.89 +val temp = prove_goalw Dnat.thy [dnat_take_def] "dnat_take(0)[xs]=UU"
   10.90   (fn prems =>
   10.91  	[
   10.92  	(asm_simp_tac iterate_ss 1)
   10.93 -	])];
   10.94 +	]);
   10.95  
   10.96 -fun prover thm = prove_goalw Dnat.thy [dnat_take_def] thm
   10.97 +val dnat_take = temp::dnat_take;
   10.98 +
   10.99 +val temp = prove_goalw Dnat.thy [dnat_take_def]
  10.100 +	"dnat_take(Suc(n))[dzero]=dzero"
  10.101   (fn prems =>
  10.102  	[
  10.103 -	(cut_facts_tac prems 1),
  10.104 -	(simp_tac iterate_ss 1),
  10.105 +	(asm_simp_tac iterate_ss 1),
  10.106 +	(simp_tac (HOLCF_ss addsimps dnat_rews) 1)
  10.107 +	]);
  10.108 +
  10.109 +val dnat_take = temp::dnat_take;
  10.110 +
  10.111 +val temp = prove_goalw Dnat.thy [dnat_take_def]
  10.112 +  "dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
  10.113 + (fn prems =>
  10.114 +	[
  10.115 +	(res_inst_tac [("Q","xs=UU")] classical2 1),
  10.116 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.117 +	(asm_simp_tac iterate_ss 1),
  10.118 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.119 +	(res_inst_tac [("n","n")] natE 1),
  10.120 +	(asm_simp_tac iterate_ss 1),
  10.121 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.122 +	(asm_simp_tac iterate_ss 1),
  10.123 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.124 +	(asm_simp_tac iterate_ss 1),
  10.125  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
  10.126  	]);
  10.127  
  10.128 -val dnat_take = [
  10.129 -prover "dnat_take(Suc(n))[dzero]=dzero",
  10.130 -prover "xs~=UU ==> dnat_take(Suc(n))[dsucc[xs]]=dsucc[dnat_take(n)[xs]]"
  10.131 -	] @ dnat_take;
  10.132 -
  10.133 +val dnat_take = temp::dnat_take;
  10.134  
  10.135  val dnat_rews = dnat_take @ dnat_rews;
  10.136  
  10.137 +
  10.138  (* ------------------------------------------------------------------------*)
  10.139  (* take lemma for dnats                                                  *)
  10.140  (* ------------------------------------------------------------------------*)
  10.141 @@ -368,6 +394,7 @@
  10.142  (* structural induction for admissible predicates                          *)
  10.143  (* ------------------------------------------------------------------------*)
  10.144  
  10.145 +(* not needed any longer
  10.146  val dnat_ind = prove_goal Dnat.thy
  10.147  "[| adm(P);\
  10.148  \   P(UU);\
  10.149 @@ -397,6 +424,79 @@
  10.150  	(eresolve_tac prems 1),
  10.151  	(etac spec 1)
  10.152  	]);
  10.153 +*)
  10.154 +
  10.155 +val dnat_finite_ind = prove_goal Dnat.thy
  10.156 +"[|P(UU);P(dzero);\
  10.157 +\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
  10.158 +\  |] ==> !s.P(dnat_take(n)[s])"
  10.159 + (fn prems =>
  10.160 +	[
  10.161 +	(nat_ind_tac "n" 1),
  10.162 +	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.163 +	(resolve_tac prems 1),
  10.164 +	(rtac allI 1),
  10.165 +	(res_inst_tac [("n","s")] dnatE 1),
  10.166 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.167 +	(resolve_tac prems 1),
  10.168 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.169 +	(resolve_tac prems 1),
  10.170 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.171 +	(res_inst_tac [("Q","dnat_take(n1)[x]=UU")] classical2 1),
  10.172 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.173 +	(resolve_tac prems 1),
  10.174 +	(resolve_tac prems 1),
  10.175 +	(atac 1),
  10.176 +	(etac spec 1)
  10.177 +	]);
  10.178 +
  10.179 +val dnat_all_finite_lemma1 = prove_goal Dnat.thy
  10.180 +"!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s"
  10.181 + (fn prems =>
  10.182 +	[
  10.183 +	(nat_ind_tac "n" 1),
  10.184 +	(simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.185 +	(rtac allI 1),
  10.186 +	(res_inst_tac [("n","s")] dnatE 1),
  10.187 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.188 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.189 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.190 +	(eres_inst_tac [("x","x")] allE 1),
  10.191 +	(etac disjE 1),
  10.192 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.193 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1)
  10.194 +	]);
  10.195 +
  10.196 +val dnat_all_finite_lemma2 = prove_goal Dnat.thy "? n.dnat_take(n)[s]=s"
  10.197 + (fn prems =>
  10.198 +	[
  10.199 +	(res_inst_tac [("Q","s=UU")] classical2 1),
  10.200 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.201 +	(subgoal_tac "(!n.dnat_take(n)[s]=UU) |(? n.dnat_take(n)[s]=s)" 1),
  10.202 +	(etac disjE 1),
  10.203 +	(eres_inst_tac [("P","s=UU")] notE 1),
  10.204 +	(rtac dnat_take_lemma 1),
  10.205 +	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.206 +	(atac 1),
  10.207 +	(subgoal_tac "!n.!s.dnat_take(n)[s]=UU |dnat_take(n)[s]=s" 1),
  10.208 +	(fast_tac HOL_cs 1),
  10.209 +	(rtac allI 1),
  10.210 +	(rtac dnat_all_finite_lemma1 1)
  10.211 +	]);
  10.212 +
  10.213 +
  10.214 +val dnat_ind = prove_goal Dnat.thy
  10.215 +"[|P(UU);P(dzero);\
  10.216 +\  !! s1.[|s1~=UU;P(s1)|] ==> P(dsucc[s1])\
  10.217 +\  |] ==> P(s)"
  10.218 + (fn prems =>
  10.219 +	[
  10.220 +	(rtac (dnat_all_finite_lemma2 RS exE) 1),
  10.221 +	(etac subst 1),
  10.222 +	(rtac (dnat_finite_ind RS spec) 1),
  10.223 +	(REPEAT (resolve_tac prems 1)),
  10.224 +	(REPEAT (atac 1))
  10.225 +	]);
  10.226  
  10.227  
  10.228  val dnat_flat = prove_goalw Dnat.thy [flat_def] "flat(dzero)"
  10.229 @@ -404,12 +504,6 @@
  10.230  	[
  10.231  	(rtac allI 1),
  10.232  	(res_inst_tac [("s","x")] dnat_ind 1),
  10.233 -	(REPEAT (resolve_tac adm_thms 1)),
  10.234 -	(contX_tacR 1),
  10.235 -	(REPEAT (resolve_tac adm_thms 1)),
  10.236 -	(contX_tacR 1),
  10.237 -	(REPEAT (resolve_tac adm_thms 1)),
  10.238 -	(contX_tacR 1),
  10.239  	(fast_tac HOL_cs 1),
  10.240  	(rtac allI 1),
  10.241  	(res_inst_tac [("n","y")] dnatE 1),
  10.242 @@ -419,53 +513,20 @@
  10.243  	(rtac allI 1),
  10.244  	(res_inst_tac [("n","y")] dnatE 1),
  10.245  	(fast_tac (HOL_cs addSIs [UU_I]) 1),
  10.246 +	(asm_simp_tac (HOLCF_ss addsimps dnat_dist_less) 1),
  10.247  	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.248 -	(hyp_subst_tac 1),
  10.249  	(strip_tac 1),
  10.250 -	(rtac disjI2 1),
  10.251 -	(forward_tac dnat_invert 1),
  10.252 -	(atac 2),
  10.253 -	(atac 1),
  10.254 +	(subgoal_tac "s1<<xa" 1),
  10.255  	(etac allE 1),
  10.256  	(dtac mp 1),
  10.257  	(atac 1),
  10.258  	(etac disjE 1),
  10.259  	(contr_tac 1),
  10.260 -	(asm_simp_tac HOLCF_ss 1)
  10.261 +	(asm_simp_tac HOLCF_ss 1),
  10.262 +	(resolve_tac  dnat_invert 1),
  10.263 +	(REPEAT (atac 1))
  10.264  	]);
  10.265  
  10.266 -val dnat_ind = prove_goal Dnat.thy
  10.267 -"[| adm(P);\
  10.268 -\   P(UU);\
  10.269 -\   P(dzero);\
  10.270 -\   !! s1.[|s1~=UU ; P(s1)|] ==> P(dsucc[s1])|] ==> P(s)"
  10.271 - (fn prems =>
  10.272 -	[
  10.273 -	(rtac (dnat_reach RS subst) 1),
  10.274 -	(res_inst_tac [("x","s")] spec 1),
  10.275 -	(rtac fix_ind 1),
  10.276 -	(rtac adm_all2 1),
  10.277 -	(rtac adm_subst 1),
  10.278 -	(contX_tacR 1),
  10.279 -	(resolve_tac prems 1),
  10.280 -	(simp_tac HOLCF_ss 1),
  10.281 -	(resolve_tac prems 1),
  10.282 -	(strip_tac 1),
  10.283 -	(res_inst_tac [("n","xa")] dnatE 1),
  10.284 -	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
  10.285 -	(resolve_tac prems 1),
  10.286 -	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
  10.287 -	(resolve_tac prems 1),
  10.288 -	(asm_simp_tac (HOLCF_ss addsimps dnat_copy) 1),
  10.289 -	(res_inst_tac [("Q","x[xb]=UU")] classical2 1),
  10.290 -	(asm_simp_tac (HOLCF_ss addsimps dnat_rews) 1),
  10.291 -	(resolve_tac prems 1),
  10.292 -	(eresolve_tac prems 1),
  10.293 -	(etac spec 1)
  10.294 -	]);
  10.295 +
  10.296  
  10.297 -val dnat_ind2 = dnat_flat RS adm_flat RS dnat_ind;
  10.298 -(*  "[| ?P(UU); ?P(dzero);
  10.299 -    !!s1. [| s1 ~= UU; ?P(s1) |] ==> ?P(dsucc[s1]) |] ==> ?P(?s)" : thm
  10.300 -*)
  10.301  
    11.1 --- a/src/HOLCF/ex/Coind.ML	Thu Mar 24 13:25:12 1994 +0100
    11.2 +++ b/src/HOLCF/ex/Coind.ML	Thu Mar 24 13:36:34 1994 +0100
    11.3 @@ -57,7 +57,7 @@
    11.4  \		 scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
    11.5   (fn prems =>
    11.6  	[
    11.7 -	(res_inst_tac [("s","n")] dnat_ind2 1),
    11.8 +	(res_inst_tac [("s","n")] dnat_ind 1),
    11.9  	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
   11.10  	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
   11.11  	(rtac trans 1),
    12.1 --- a/src/HOLCF/ex/ROOT.ML	Thu Mar 24 13:25:12 1994 +0100
    12.2 +++ b/src/HOLCF/ex/ROOT.ML	Thu Mar 24 13:36:34 1994 +0100
    12.3 @@ -13,4 +13,6 @@
    12.4  time_use_thy "ex/Coind";
    12.5  time_use_thy "ex/Hoare";
    12.6  time_use_thy "ex/Loop";
    12.7 +time_use_thy "ex/Dagstuhl";
    12.8 +
    12.9  maketest     "END: Root file for HOLCF examples";
    13.1 --- a/src/HOLCF/ex/coind.ML	Thu Mar 24 13:25:12 1994 +0100
    13.2 +++ b/src/HOLCF/ex/coind.ML	Thu Mar 24 13:36:34 1994 +0100
    13.3 @@ -57,7 +57,7 @@
    13.4  \		 scons[n][iterator[dsucc[n]][smap[dsucc]][nats]]"
    13.5   (fn prems =>
    13.6  	[
    13.7 -	(res_inst_tac [("s","n")] dnat_ind2 1),
    13.8 +	(res_inst_tac [("s","n")] dnat_ind 1),
    13.9  	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
   13.10  	(simp_tac (HOLCF_ss addsimps (coind_rews @ stream_rews)) 1),
   13.11  	(rtac trans 1),
    14.1 --- a/src/HOLCF/fix.ML	Thu Mar 24 13:25:12 1994 +0100
    14.2 +++ b/src/HOLCF/fix.ML	Thu Mar 24 13:36:34 1994 +0100
    14.3 @@ -387,6 +387,19 @@
    14.4          (rtac refl 1)
    14.5          ]);
    14.6  
    14.7 +(* ------------------------------------------------------------------------ 
    14.8 +
    14.9 +given the definition
   14.10 +
   14.11 +smap_def
   14.12 +  "smap = fix[LAM h f s. stream_when[LAM x l.scons[f[x]][h[f][l]]][s]]"
   14.13 +
   14.14 +use fix_prover for 
   14.15 +
   14.16 +val smap_def2 = fix_prover Stream2.thy smap_def 
   14.17 +        "smap = (LAM f s. stream_when[LAM x l.scons[f[x]][smap[f][l]]][s])";
   14.18 +
   14.19 +   ------------------------------------------------------------------------ *)
   14.20  
   14.21  (* ------------------------------------------------------------------------ *)
   14.22  (* better access to definitions                                             *)
   14.23 @@ -881,7 +894,7 @@
   14.24  	(rtac iffI 1),
   14.25  	(etac FalseE 2),
   14.26  	(rtac notE 1),
   14.27 -	(etac less_not_sym 1),	
   14.28 +	(etac (less_not_sym RS mp) 1),	
   14.29  	(atac 1),
   14.30  	(asm_simp_tac Cfun_ss  1),
   14.31  	(etac (is_chainE RS spec) 1),
   14.32 @@ -921,7 +934,7 @@
   14.33  	(rtac iffI 1),
   14.34  	(etac FalseE 2),
   14.35  	(rtac notE 1),
   14.36 -	(etac less_not_sym 1),	
   14.37 +	(etac (less_not_sym RS mp) 1),	
   14.38  	(atac 1),
   14.39  	(asm_simp_tac nat_ss 1),
   14.40  	(dtac spec 1),
    15.1 --- a/src/HOLCF/porder.ML	Thu Mar 24 13:25:12 1994 +0100
    15.2 +++ b/src/HOLCF/porder.ML	Thu Mar 24 13:36:34 1994 +0100
    15.3 @@ -6,9 +6,9 @@
    15.4  Lemmas for theory porder.thy 
    15.5  *)
    15.6  
    15.7 +open Porder0;
    15.8  open Porder;
    15.9  
   15.10 -
   15.11  val box_less = prove_goal Porder.thy 
   15.12  "[| a << b; c << a; b << d|] ==> c << d"
   15.13   (fn prems =>
    16.1 --- a/src/HOLCF/porder.thy	Thu Mar 24 13:25:12 1994 +0100
    16.2 +++ b/src/HOLCF/porder.thy	Thu Mar 24 13:36:34 1994 +0100
    16.3 @@ -3,25 +3,13 @@
    16.4      Author: 	Franz Regensburger
    16.5      Copyright   1993 Technische Universitaet Muenchen
    16.6  
    16.7 -Definition of class porder (partial order)
    16.8 -
    16.9 -The prototype theory for this class is void.thy 
   16.10 +Conservative extension of theory Porder0 by constant definitions 
   16.11  
   16.12  *)
   16.13  
   16.14 -Porder = Void +
   16.15 -
   16.16 -(* Introduction of new class. The witness is type void. *)
   16.17 -
   16.18 -classes po < term
   16.19 +Porder = Porder0 +
   16.20  
   16.21 -(* default type is still term ! *)
   16.22 -(* void is the prototype in po *)
   16.23 -
   16.24 -arities void :: po
   16.25 -
   16.26 -consts	"<<"	::	"['a,'a::po] => bool"	(infixl 55)
   16.27 -
   16.28 +consts	
   16.29  	"<|"	::	"['a set,'a::po] => bool"	(infixl 55)
   16.30  	"<<|"	::	"['a set,'a::po] => bool"	(infixl 55)
   16.31  	lub	::	"'a set => 'a::po"
   16.32 @@ -32,21 +20,6 @@
   16.33  
   16.34  rules
   16.35  
   16.36 -(* class axioms: justification is theory Void *)
   16.37 -
   16.38 -refl_less	"x << x"	
   16.39 -				(* witness refl_less_void    *)
   16.40 -
   16.41 -antisym_less	"[|x<<y ; y<<x |] ==> x = y"	
   16.42 -				(* witness antisym_less_void *)
   16.43 -
   16.44 -trans_less	"[|x<<y ; y<<z |] ==> x<<z"
   16.45 -				(* witness trans_less_void   *)
   16.46 -
   16.47 -(* instance of << for the prototype void *)
   16.48 -
   16.49 -inst_void_po	"(op <<)::[void,void]=>bool = less_void"
   16.50 -
   16.51  (* class definitions *)
   16.52  
   16.53  is_ub		"S  <| x == ! y.y:S --> y<<x"
   16.54 @@ -57,11 +30,9 @@
   16.55  (* Arbitrary chains are total orders    *)                  
   16.56  is_tord		"is_tord(S) == ! x y. x:S & y:S --> (x<<y | y<<x)"
   16.57  
   16.58 -
   16.59  (* Here we use countable chains and I prefer to code them as functions! *)
   16.60  is_chain	"is_chain(F) == (! i.F(i) << F(Suc(i)))"
   16.61  
   16.62 -
   16.63  (* finite chains, needed for monotony of continouous functions *)
   16.64  
   16.65  max_in_chain_def "max_in_chain(i,C) == ! j. i <= j --> C(i) = C(j)" 
    17.1 --- a/src/HOLCF/stream.ML	Thu Mar 24 13:25:12 1994 +0100
    17.2 +++ b/src/HOLCF/stream.ML	Thu Mar 24 13:36:34 1994 +0100
    17.3 @@ -229,6 +229,7 @@
    17.4  
    17.5  val stream_rews = stream_discsel_def @ stream_rews;
    17.6  
    17.7 +
    17.8  (* ------------------------------------------------------------------------*)
    17.9  (* Properties stream_take                                                  *)
   17.10  (* ------------------------------------------------------------------------*)
   17.11 @@ -265,6 +266,46 @@
   17.12  val stream_rews = stream_take @ stream_rews;
   17.13  
   17.14  (* ------------------------------------------------------------------------*)
   17.15 +(* enhance the simplifier                                                  *)
   17.16 +(* ------------------------------------------------------------------------*)
   17.17 +
   17.18 +val stream_copy2 = prove_goal Stream.thy 
   17.19 +     "stream_copy[f][scons[x][xs]]= scons[x][f[xs]]"
   17.20 + (fn prems =>
   17.21 +	[
   17.22 +	(res_inst_tac [("Q","x=UU")] classical2 1),
   17.23 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   17.24 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   17.25 +	]);
   17.26 +
   17.27 +val shd2 = prove_goal Stream.thy "shd[scons[x][xs]]=x"
   17.28 + (fn prems =>
   17.29 +	[
   17.30 +	(res_inst_tac [("Q","x=UU")] classical2 1),
   17.31 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   17.32 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   17.33 +	]);
   17.34 +
   17.35 +val stream_take2 = prove_goal Stream.thy 
   17.36 + "stream_take(Suc(n))[scons[x][xs]]=scons[x][stream_take(n)[xs]]"
   17.37 + (fn prems =>
   17.38 +	[
   17.39 +	(res_inst_tac [("Q","x=UU")] classical2 1),
   17.40 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   17.41 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
   17.42 +	]);
   17.43 +
   17.44 +val stream_rews = [stream_iso_strict RS conjunct1,
   17.45 +		   stream_iso_strict RS conjunct2,
   17.46 +                   hd stream_copy, stream_copy2]
   17.47 +                  @ stream_when
   17.48 +                  @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))  
   17.49 +                  @ stream_constrdef
   17.50 +                  @ stream_discsel_def
   17.51 +                  @ [ stream_take2] @ (tl stream_take);
   17.52 +
   17.53 +
   17.54 +(* ------------------------------------------------------------------------*)
   17.55  (* take lemma for streams                                                  *)
   17.56  (* ------------------------------------------------------------------------*)
   17.57  
   17.58 @@ -326,8 +367,49 @@
   17.59  (* structural induction for admissible predicates                          *)
   17.60  (* ------------------------------------------------------------------------*)
   17.61  
   17.62 +val stream_finite_ind = prove_goal Stream.thy
   17.63 +"[|P(UU);\
   17.64 +\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   17.65 +\  |] ==> !s.P(stream_take(n)[s])"
   17.66 + (fn prems =>
   17.67 +	[
   17.68 +	(nat_ind_tac "n" 1),
   17.69 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
   17.70 +	(resolve_tac prems 1),
   17.71 +	(rtac allI 1),
   17.72 +	(res_inst_tac [("s","s")] streamE 1),
   17.73 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   17.74 +	(resolve_tac prems 1),
   17.75 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
   17.76 +	(resolve_tac prems 1),
   17.77 +	(atac 1),
   17.78 +	(etac spec 1)
   17.79 +	]);
   17.80 +
   17.81 +val stream_finite_ind2 = prove_goalw Stream.thy  [stream_finite_def]
   17.82 +"(!!n.P(stream_take(n)[s])) ==>  stream_finite(s) -->P(s)"
   17.83 + (fn prems =>
   17.84 +	[
   17.85 +	(strip_tac 1),
   17.86 +	(etac exE 1),
   17.87 +	(etac subst 1),
   17.88 +	(resolve_tac prems 1)
   17.89 +	]);
   17.90 +
   17.91 +val stream_finite_ind3 = prove_goal Stream.thy 
   17.92 +"[|P(UU);\
   17.93 +\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
   17.94 +\  |] ==> stream_finite(s) --> P(s)"
   17.95 + (fn prems =>
   17.96 +	[
   17.97 +	(rtac stream_finite_ind2 1),
   17.98 +	(rtac (stream_finite_ind RS spec) 1),
   17.99 +	(REPEAT (resolve_tac prems 1)),
  17.100 +	(REPEAT (atac 1))
  17.101 +	]);
  17.102 +
  17.103  val stream_ind = prove_goal Stream.thy
  17.104 -"[| adm(P);\
  17.105 +"[|adm(P);\
  17.106  \  P(UU);\
  17.107  \  !! x s1.[|x~=UU;P(s1)|] ==> P(scons[x][s1])\
  17.108  \  |] ==> P(s)"
  17.109 @@ -335,21 +417,16 @@
  17.110  	[
  17.111  	(rtac (stream_reach RS subst) 1),
  17.112  	(res_inst_tac [("x","s")] spec 1),
  17.113 -	(rtac fix_ind 1),
  17.114 -	(rtac (allI RS adm_all) 1),
  17.115 +	(rtac wfix_ind 1),
  17.116 +	(rtac adm_impl_admw 1),
  17.117 +	(REPEAT (resolve_tac adm_thms 1)),
  17.118  	(rtac adm_subst 1),
  17.119  	(contX_tacR 1),
  17.120  	(resolve_tac prems 1),
  17.121 -	(simp_tac HOLCF_ss 1),
  17.122 -	(resolve_tac prems 1),
  17.123 -	(strip_tac 1),
  17.124 -	(res_inst_tac [("s","xa")] streamE 1),
  17.125 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.126 -	(resolve_tac prems 1),
  17.127 -	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.128 -	(resolve_tac prems 1),
  17.129 -	(atac 1),
  17.130 -	(etac spec 1)
  17.131 +	(rtac allI 1),
  17.132 +	(rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
  17.133 +	(REPEAT (resolve_tac prems 1)),
  17.134 +	(REPEAT (atac 1))
  17.135  	]);
  17.136  
  17.137  
  17.138 @@ -403,3 +480,312 @@
  17.139  	]);
  17.140  
  17.141  
  17.142 +(* ------------------------------------------------------------------------*)
  17.143 +(* theorems about finite and infinite streams                              *)
  17.144 +(* ------------------------------------------------------------------------*)
  17.145 +
  17.146 +(* ----------------------------------------------------------------------- *)
  17.147 +(* 2 lemmas about stream_finite                                            *)
  17.148 +(* ----------------------------------------------------------------------- *)
  17.149 +
  17.150 +val stream_finite_UU = prove_goalw Stream.thy [stream_finite_def]
  17.151 +	 "stream_finite(UU)"
  17.152 + (fn prems =>
  17.153 +	[
  17.154 +	(rtac exI 1),
  17.155 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
  17.156 +	]);
  17.157 +
  17.158 +val inf_stream_not_UU = prove_goal Stream.thy  "~stream_finite(s)  ==> s ~= UU"
  17.159 + (fn prems =>
  17.160 +	[
  17.161 +	(cut_facts_tac prems 1),
  17.162 +	(etac swap 1),
  17.163 +	(dtac notnotD 1),
  17.164 +	(hyp_subst_tac  1),
  17.165 +	(rtac stream_finite_UU 1)
  17.166 +	]);
  17.167 +
  17.168 +(* ----------------------------------------------------------------------- *)
  17.169 +(* a lemma about shd                                                       *)
  17.170 +(* ----------------------------------------------------------------------- *)
  17.171 +
  17.172 +val stream_shd_lemma1 = prove_goal Stream.thy "shd[s]=UU --> s=UU"
  17.173 + (fn prems =>
  17.174 +	[
  17.175 +	(res_inst_tac [("s","s")] streamE 1),
  17.176 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.177 +	(hyp_subst_tac 1),
  17.178 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
  17.179 +	]);
  17.180 +
  17.181 +
  17.182 +(* ----------------------------------------------------------------------- *)
  17.183 +(* lemmas about stream_take                                                *)
  17.184 +(* ----------------------------------------------------------------------- *)
  17.185 +
  17.186 +val stream_take_lemma1 = prove_goal Stream.thy 
  17.187 + "!x xs.x~=UU --> \
  17.188 +\  stream_take(Suc(n))[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
  17.189 + (fn prems =>
  17.190 +	[
  17.191 +	(rtac allI 1),
  17.192 +	(rtac allI 1),
  17.193 +	(rtac impI 1),
  17.194 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.195 +	(strip_tac 1),
  17.196 +	(rtac ((hd stream_inject) RS conjunct2) 1),
  17.197 +	(atac 1),
  17.198 +	(atac 1),
  17.199 +	(atac 1)
  17.200 +	]);
  17.201 +
  17.202 +
  17.203 +val stream_take_lemma2 = prove_goal Stream.thy 
  17.204 + "! s2. stream_take(n)[s2] = s2 --> stream_take(Suc(n))[s2]=s2"
  17.205 + (fn prems =>
  17.206 +	[
  17.207 +	(nat_ind_tac "n" 1),
  17.208 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.209 +	(strip_tac 1 ),
  17.210 +	(hyp_subst_tac  1),
  17.211 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.212 +	(rtac allI 1),
  17.213 +	(res_inst_tac [("s","s2")] streamE 1),
  17.214 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.215 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.216 +	(strip_tac 1 ),
  17.217 +	(subgoal_tac "stream_take(n1)[xs] = xs" 1),
  17.218 +	(rtac ((hd stream_inject) RS conjunct2) 2),
  17.219 +	(atac 4),
  17.220 +	(atac 2),
  17.221 +	(atac 2),
  17.222 +	(rtac cfun_arg_cong 1),
  17.223 +	(fast_tac HOL_cs 1)
  17.224 +	]);
  17.225 +
  17.226 +val stream_take_lemma3 = prove_goal Stream.thy 
  17.227 + "!x xs.x~=UU --> \
  17.228 +\  stream_take(n)[scons[x][xs]] = scons[x][xs] --> stream_take(n)[xs]=xs"
  17.229 + (fn prems =>
  17.230 +	[
  17.231 +	(nat_ind_tac "n" 1),
  17.232 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.233 +	(strip_tac 1 ),
  17.234 +	(res_inst_tac [("P","scons[x][xs]=UU")] notE 1),
  17.235 +	(eresolve_tac stream_constrdef 1),
  17.236 +	(etac sym 1),
  17.237 +	(strip_tac 1 ),
  17.238 +	(rtac (stream_take_lemma2 RS spec RS mp) 1),
  17.239 +	(res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
  17.240 +	(atac 1),
  17.241 +	(atac 1),
  17.242 +	(etac (stream_take2 RS subst) 1)
  17.243 +	]);
  17.244 +
  17.245 +val stream_take_lemma4 = prove_goal Stream.thy 
  17.246 + "!x xs.\
  17.247 +\stream_take(n)[xs]=xs --> stream_take(Suc(n))[scons[x][xs]] = scons[x][xs]"
  17.248 + (fn prems =>
  17.249 +	[
  17.250 +	(nat_ind_tac "n" 1),
  17.251 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.252 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1)
  17.253 +	]);
  17.254 +
  17.255 +(* ---- *)
  17.256 +
  17.257 +val stream_take_lemma5 = prove_goal Stream.thy 
  17.258 +"!s. stream_take(n)[s]=s --> iterate(n,stl,s)=UU"
  17.259 + (fn prems =>
  17.260 +	[
  17.261 +	(nat_ind_tac "n" 1),
  17.262 +	(simp_tac iterate_ss 1),
  17.263 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.264 +	(strip_tac 1),
  17.265 +	(res_inst_tac [("s","s")] streamE 1),
  17.266 +	(hyp_subst_tac 1),
  17.267 +	(rtac (iterate_Suc2 RS ssubst) 1),
  17.268 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.269 +	(rtac (iterate_Suc2 RS ssubst) 1),
  17.270 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.271 +	(etac allE 1),
  17.272 +	(etac mp 1),
  17.273 +	(hyp_subst_tac 1),
  17.274 +	(etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
  17.275 +	(atac 1)
  17.276 +	]);
  17.277 +
  17.278 +val stream_take_lemma6 = prove_goal Stream.thy 
  17.279 +"!s.iterate(n,stl,s)=UU --> stream_take(n)[s]=s"
  17.280 + (fn prems =>
  17.281 +	[
  17.282 +	(nat_ind_tac "n" 1),
  17.283 +	(simp_tac iterate_ss 1),
  17.284 +	(strip_tac 1),
  17.285 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.286 +	(rtac allI 1),
  17.287 +	(res_inst_tac [("s","s")] streamE 1),
  17.288 +	(hyp_subst_tac 1),
  17.289 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.290 +	(hyp_subst_tac 1),
  17.291 +	(rtac (iterate_Suc2 RS ssubst) 1),
  17.292 +	(asm_simp_tac (HOLCF_ss addsimps stream_rews) 1)
  17.293 +	]);
  17.294 +
  17.295 +val stream_take_lemma7 = prove_goal Stream.thy 
  17.296 +"(iterate(n,stl,s)=UU) = (stream_take(n)[s]=s)"
  17.297 + (fn prems =>
  17.298 +	[
  17.299 +	(rtac iffI 1),
  17.300 +	(etac (stream_take_lemma6 RS spec RS mp) 1),
  17.301 +	(etac (stream_take_lemma5 RS spec RS mp) 1)
  17.302 +	]);
  17.303 +
  17.304 +
  17.305 +(* ----------------------------------------------------------------------- *)
  17.306 +(* lemmas stream_finite                                                    *)
  17.307 +(* ----------------------------------------------------------------------- *)
  17.308 +
  17.309 +val stream_finite_lemma1 = prove_goalw Stream.thy [stream_finite_def]
  17.310 + "stream_finite(xs) ==> stream_finite(scons[x][xs])"
  17.311 + (fn prems =>
  17.312 +	[
  17.313 +	(cut_facts_tac prems 1),
  17.314 +	(etac exE 1),
  17.315 +	(rtac exI 1),
  17.316 +	(etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
  17.317 +	]);
  17.318 +
  17.319 +val stream_finite_lemma2 = prove_goalw Stream.thy [stream_finite_def]
  17.320 + "[|x~=UU; stream_finite(scons[x][xs])|] ==> stream_finite(xs)"
  17.321 + (fn prems =>
  17.322 +	[
  17.323 +	(cut_facts_tac prems 1),
  17.324 +	(etac exE 1),
  17.325 +	(rtac exI 1),
  17.326 +	(etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
  17.327 +	(atac 1)
  17.328 +	]);
  17.329 +
  17.330 +val stream_finite_lemma3 = prove_goal Stream.thy 
  17.331 + "x~=UU ==> stream_finite(scons[x][xs]) = stream_finite(xs)"
  17.332 + (fn prems =>
  17.333 +	[
  17.334 +	(cut_facts_tac prems 1),
  17.335 +	(rtac iffI 1),
  17.336 +	(etac stream_finite_lemma2 1),
  17.337 +	(atac 1),
  17.338 +	(etac stream_finite_lemma1 1)
  17.339 +	]);
  17.340 +
  17.341 +
  17.342 +val stream_finite_lemma5 = prove_goalw Stream.thy [stream_finite_def]
  17.343 + "(!n. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1))\
  17.344 +\=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
  17.345 + (fn prems =>
  17.346 +	[
  17.347 +	(rtac iffI 1),
  17.348 +	(fast_tac HOL_cs 1),
  17.349 +	(fast_tac HOL_cs 1)
  17.350 +	]);
  17.351 +
  17.352 +val stream_finite_lemma6 = prove_goal Stream.thy
  17.353 + "!s1 s2. s1 << s2  --> stream_take(n)[s2] = s2 --> stream_finite(s1)"
  17.354 + (fn prems =>
  17.355 +	[
  17.356 +	(nat_ind_tac "n" 1),
  17.357 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.358 +	(strip_tac 1 ),
  17.359 +	(hyp_subst_tac  1),
  17.360 +	(dtac UU_I 1),
  17.361 +	(hyp_subst_tac  1),
  17.362 +	(rtac stream_finite_UU 1),
  17.363 +	(rtac allI 1),
  17.364 +	(rtac allI 1),
  17.365 +	(res_inst_tac [("s","s1")] streamE 1),
  17.366 +	(hyp_subst_tac  1),
  17.367 +	(strip_tac 1 ),
  17.368 +	(rtac stream_finite_UU 1),
  17.369 +	(hyp_subst_tac  1),
  17.370 +	(res_inst_tac [("s","s2")] streamE 1),
  17.371 +	(hyp_subst_tac  1),
  17.372 +	(strip_tac 1 ),
  17.373 +	(dtac UU_I 1),
  17.374 +	(asm_simp_tac(HOLCF_ss addsimps (stream_rews @ [stream_finite_UU])) 1),
  17.375 +	(hyp_subst_tac  1),
  17.376 +	(simp_tac (HOLCF_ss addsimps stream_rews) 1),
  17.377 +	(strip_tac 1 ),
  17.378 +	(rtac stream_finite_lemma1 1),
  17.379 +	(subgoal_tac "xs << xsa" 1),
  17.380 +	(subgoal_tac "stream_take(n1)[xsa] = xsa" 1),
  17.381 +	(fast_tac HOL_cs 1),
  17.382 +	(res_inst_tac  [("x1.1","xa"),("y1.1","xa")] 
  17.383 +                   ((hd stream_inject) RS conjunct2) 1),
  17.384 +	(atac 1),
  17.385 +	(atac 1),
  17.386 +	(atac 1),
  17.387 +	(res_inst_tac [("x1.1","x"),("y1.1","xa")]
  17.388 +	 ((hd stream_invert) RS conjunct2) 1),
  17.389 +	(atac 1),
  17.390 +	(atac 1),
  17.391 +	(atac 1)
  17.392 +	]);
  17.393 +
  17.394 +val stream_finite_lemma7 = prove_goal Stream.thy 
  17.395 +"s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
  17.396 + (fn prems =>
  17.397 +	[
  17.398 +	(rtac (stream_finite_lemma5 RS iffD1) 1),
  17.399 +	(rtac allI 1),
  17.400 +	(rtac (stream_finite_lemma6 RS spec RS spec) 1)
  17.401 +	]);
  17.402 +
  17.403 +val stream_finite_lemma8 = prove_goalw Stream.thy [stream_finite_def]
  17.404 +"stream_finite(s) = (? n. iterate(n,stl,s)=UU)"
  17.405 + (fn prems =>
  17.406 +	[
  17.407 +	(simp_tac (HOL_ss addsimps [stream_take_lemma7]) 1)
  17.408 +	]);
  17.409 +
  17.410 +
  17.411 +(* ----------------------------------------------------------------------- *)
  17.412 +(* admissibility of ~stream_finite                                         *)
  17.413 +(* ----------------------------------------------------------------------- *)
  17.414 +
  17.415 +val adm_not_stream_finite = prove_goalw Stream.thy [adm_def]
  17.416 + "adm(%s. ~ stream_finite(s))"
  17.417 + (fn prems =>
  17.418 +	[
  17.419 +	(strip_tac 1 ),
  17.420 +	(res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical3 1),
  17.421 +	(atac 2),
  17.422 +	(subgoal_tac "!i.stream_finite(Y(i))" 1),
  17.423 +	(fast_tac HOL_cs 1),
  17.424 +	(rtac allI 1),
  17.425 +	(rtac (stream_finite_lemma7 RS mp RS mp) 1),
  17.426 +	(etac is_ub_thelub 1),
  17.427 +	(atac 1)
  17.428 +	]);
  17.429 +
  17.430 +(* ----------------------------------------------------------------------- *)
  17.431 +(* alternative prove for admissibility of ~stream_finite                   *)
  17.432 +(* show that stream_finite(s) = (? n. iterate(n, stl, s) = UU)             *)
  17.433 +(* and prove adm. of ~(? n. iterate(n, stl, s) = UU)                       *)
  17.434 +(* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
  17.435 +(* ----------------------------------------------------------------------- *)
  17.436 +
  17.437 +
  17.438 +val adm_not_stream_finite2=prove_goal Stream.thy "adm(%s. ~ stream_finite(s))"
  17.439 + (fn prems =>
  17.440 +	[
  17.441 +	(subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate(n,stl,s)~=UU))" 1),
  17.442 +	(etac (adm_cong RS iffD2)1),
  17.443 +	(REPEAT(resolve_tac adm_thms 1)),
  17.444 +	(rtac  contX_iterate2 1),
  17.445 +	(rtac allI 1),
  17.446 +	(rtac (stream_finite_lemma8 RS ssubst) 1),
  17.447 +	(fast_tac HOL_cs 1)
  17.448 +	]);
  17.449 +
  17.450 +
    18.1 --- a/src/HOLCF/stream2.thy	Thu Mar 24 13:25:12 1994 +0100
    18.2 +++ b/src/HOLCF/stream2.thy	Thu Mar 24 13:36:34 1994 +0100
    18.3 @@ -19,7 +19,7 @@
    18.4  
    18.5  
    18.6  end
    18.7 -
    18.8 +      
    18.9  
   18.10  (*
   18.11  		smap[f][UU] = UU