src/HOLCF/explicit_domains/Stream.ML
changeset 2679 3eac428cdd1b
parent 2678 d5fe793293ac
child 2680 20fa49e610ca
     1.1 --- a/src/HOLCF/explicit_domains/Stream.ML	Mon Feb 24 09:46:12 1997 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,838 +0,0 @@
     1.4 -(*  
     1.5 -    ID:         $Id$
     1.6 -    Author:     Franz Regensburger
     1.7 -    Copyright   1993 Technische Universitaet Muenchen
     1.8 -
     1.9 -Lemmas for stream.thy
    1.10 -*)
    1.11 -
    1.12 -open Stream;
    1.13 -
    1.14 -(* ------------------------------------------------------------------------*)
    1.15 -(* The isomorphisms stream_rep_iso and stream_abs_iso are strict           *)
    1.16 -(* ------------------------------------------------------------------------*)
    1.17 -
    1.18 -val stream_iso_strict= stream_rep_iso RS (stream_abs_iso RS 
    1.19 -        (allI  RSN (2,allI RS iso_strict)));
    1.20 -
    1.21 -val stream_rews = [stream_iso_strict RS conjunct1,
    1.22 -                stream_iso_strict RS conjunct2];
    1.23 -
    1.24 -(* ------------------------------------------------------------------------*)
    1.25 -(* Properties of stream_copy                                               *)
    1.26 -(* ------------------------------------------------------------------------*)
    1.27 -
    1.28 -fun prover defs thm =  prove_goalw Stream.thy defs thm
    1.29 - (fn prems =>
    1.30 -        [
    1.31 -        (cut_facts_tac prems 1),
    1.32 -        (asm_simp_tac (!simpset addsimps 
    1.33 -                (stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
    1.34 -        ]);
    1.35 -
    1.36 -val stream_copy = 
    1.37 -        [
    1.38 -        prover [stream_copy_def] "stream_copy`f`UU=UU",
    1.39 -        prover [stream_copy_def,scons_def] 
    1.40 -        "x~=UU ==> stream_copy`f`(scons`x`xs)= scons`x`(f`xs)"
    1.41 -        ];
    1.42 -
    1.43 -val stream_rews =  stream_copy @ stream_rews; 
    1.44 -
    1.45 -(* ------------------------------------------------------------------------*)
    1.46 -(* Exhaustion and elimination for streams                                  *)
    1.47 -(* ------------------------------------------------------------------------*)
    1.48 -
    1.49 -qed_goalw "Exh_stream" Stream.thy [scons_def]
    1.50 -        "s = UU | (? x xs. x~=UU & s = scons`x`xs)"
    1.51 - (fn prems =>
    1.52 -        [
    1.53 -        (Simp_tac 1),
    1.54 -        (rtac (stream_rep_iso RS subst) 1),
    1.55 -        (res_inst_tac [("p","stream_rep`s")] sprodE 1),
    1.56 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
    1.57 -        (Asm_simp_tac  1),
    1.58 -        (res_inst_tac [("p","y")] upE1 1),
    1.59 -         (contr_tac 1),
    1.60 -        (rtac disjI2 1),
    1.61 -        (rtac exI 1),
    1.62 -        (etac conjI 1),
    1.63 -	(rtac exI 1),
    1.64 -        (Asm_simp_tac  1)
    1.65 -        ]);
    1.66 -
    1.67 -qed_goal "streamE" Stream.thy 
    1.68 -        "[| s=UU ==> Q; !!x xs.[|s=scons`x`xs;x~=UU|]==>Q|]==>Q"
    1.69 - (fn prems =>
    1.70 -        [
    1.71 -        (rtac (Exh_stream RS disjE) 1),
    1.72 -        (eresolve_tac prems 1),
    1.73 -        (etac exE 1),
    1.74 -        (etac exE 1),
    1.75 -        (resolve_tac prems 1),
    1.76 -        (fast_tac HOL_cs 1),
    1.77 -        (fast_tac HOL_cs 1)
    1.78 -        ]);
    1.79 -
    1.80 -(* ------------------------------------------------------------------------*)
    1.81 -(* Properties of stream_when                                               *)
    1.82 -(* ------------------------------------------------------------------------*)
    1.83 -
    1.84 -fun prover defs thm =  prove_goalw Stream.thy defs thm
    1.85 - (fn prems =>
    1.86 -        [
    1.87 -        (cut_facts_tac prems 1),
    1.88 -        (asm_simp_tac (!simpset addsimps 
    1.89 -                (stream_rews @ [stream_abs_iso,stream_rep_iso])) 1)
    1.90 -        ]);
    1.91 -
    1.92 -
    1.93 -val stream_when = [
    1.94 -        prover [stream_when_def] "stream_when`f`UU=UU",
    1.95 -        prover [stream_when_def,scons_def] 
    1.96 -                "x~=UU ==> stream_when`f`(scons`x`xs)= f`x`xs"
    1.97 -        ];
    1.98 -
    1.99 -val stream_rews = stream_when @ stream_rews;
   1.100 -
   1.101 -(* ------------------------------------------------------------------------*)
   1.102 -(* Rewrites for  discriminators and  selectors                             *)
   1.103 -(* ------------------------------------------------------------------------*)
   1.104 -
   1.105 -fun prover defs thm = prove_goalw Stream.thy defs thm
   1.106 - (fn prems =>
   1.107 -        [
   1.108 -        (simp_tac (!simpset addsimps stream_rews) 1)
   1.109 -        ]);
   1.110 -
   1.111 -val stream_discsel = [
   1.112 -        prover [is_scons_def] "is_scons`UU=UU",
   1.113 -        prover [shd_def] "shd`UU=UU",
   1.114 -        prover [stl_def] "stl`UU=UU"
   1.115 -        ];
   1.116 -
   1.117 -fun prover defs thm = prove_goalw Stream.thy defs thm
   1.118 - (fn prems =>
   1.119 -        [
   1.120 -        (cut_facts_tac prems 1),
   1.121 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
   1.122 -        ]);
   1.123 -
   1.124 -val stream_discsel = [
   1.125 -prover [is_scons_def,shd_def,stl_def] "x~=UU ==> is_scons`(scons`x`xs)=TT",
   1.126 -prover [is_scons_def,shd_def,stl_def] "x~=UU ==> shd`(scons`x`xs)=x",
   1.127 -prover [is_scons_def,shd_def,stl_def] "x~=UU ==> stl`(scons`x`xs)=xs"
   1.128 -        ] @ stream_discsel;
   1.129 -
   1.130 -val stream_rews = stream_discsel @ stream_rews;
   1.131 -
   1.132 -(* ------------------------------------------------------------------------*)
   1.133 -(* Definedness and strictness                                              *)
   1.134 -(* ------------------------------------------------------------------------*)
   1.135 -
   1.136 -fun prover contr thm = prove_goal Stream.thy thm
   1.137 - (fn prems =>
   1.138 -        [
   1.139 -        (res_inst_tac [("P1",contr)] classical2 1),
   1.140 -        (simp_tac (!simpset addsimps stream_rews) 1),
   1.141 -        (dtac sym 1),
   1.142 -        (Asm_simp_tac 1),
   1.143 -        (simp_tac (!simpset addsimps (prems @ stream_rews)) 1)
   1.144 -        ]);
   1.145 -
   1.146 -val stream_constrdef = [
   1.147 -        prover "is_scons`(UU::'a stream)~=UU" "x~=UU ==> scons`(x::'a)`xs~=UU"
   1.148 -        ]; 
   1.149 -
   1.150 -fun prover defs thm = prove_goalw Stream.thy defs thm
   1.151 - (fn prems =>
   1.152 -        [
   1.153 -        (simp_tac (!simpset addsimps stream_rews) 1)
   1.154 -        ]);
   1.155 -
   1.156 -val stream_constrdef = [
   1.157 -        prover [scons_def] "scons`UU`xs=UU"
   1.158 -        ] @ stream_constrdef;
   1.159 -
   1.160 -val stream_rews = stream_constrdef @ stream_rews;
   1.161 -
   1.162 -
   1.163 -(* ------------------------------------------------------------------------*)
   1.164 -(* Distinctness wrt. << and =                                              *)
   1.165 -(* ------------------------------------------------------------------------*)
   1.166 -
   1.167 -
   1.168 -(* ------------------------------------------------------------------------*)
   1.169 -(* Invertibility                                                           *)
   1.170 -(* ------------------------------------------------------------------------*)
   1.171 -
   1.172 -val stream_invert =
   1.173 -        [
   1.174 -prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
   1.175 -\ scons`x1`x2 << scons`y1`y2|] ==> x1<< y1 & x2 << y2"
   1.176 - (fn prems =>
   1.177 -        [
   1.178 -        (cut_facts_tac prems 1),
   1.179 -        (rtac conjI 1),
   1.180 -        (dres_inst_tac [("fo","stream_when`(LAM x l.x)")] monofun_cfun_arg 1),
   1.181 -        (etac box_less 1),
   1.182 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
   1.183 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
   1.184 -        (dres_inst_tac [("fo","stream_when`(LAM x l.l)")] monofun_cfun_arg 1),
   1.185 -        (etac box_less 1),
   1.186 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
   1.187 -        (asm_simp_tac (!simpset addsimps stream_when) 1)
   1.188 -        ])
   1.189 -        ];
   1.190 -
   1.191 -(* ------------------------------------------------------------------------*)
   1.192 -(* Injectivity                                                             *)
   1.193 -(* ------------------------------------------------------------------------*)
   1.194 -
   1.195 -val stream_inject = 
   1.196 -        [
   1.197 -prove_goal Stream.thy "[|x1~=UU; y1~=UU;\
   1.198 -\ scons`x1`x2 = scons`y1`y2 |] ==> x1= y1 & x2 = y2"
   1.199 - (fn prems =>
   1.200 -        [
   1.201 -        (cut_facts_tac prems 1),
   1.202 -        (rtac conjI 1),
   1.203 -        (dres_inst_tac [("f","stream_when`(LAM x l.x)")] cfun_arg_cong 1),
   1.204 -        (etac box_equals 1),
   1.205 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
   1.206 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
   1.207 -        (dres_inst_tac [("f","stream_when`(LAM x l.l)")] cfun_arg_cong 1),
   1.208 -        (etac box_equals 1),
   1.209 -        (asm_simp_tac (!simpset addsimps stream_when) 1),
   1.210 -        (asm_simp_tac (!simpset addsimps stream_when) 1)
   1.211 -        ])
   1.212 -        ];
   1.213 -
   1.214 -(* ------------------------------------------------------------------------*)
   1.215 -(* definedness for  discriminators and  selectors                          *)
   1.216 -(* ------------------------------------------------------------------------*)
   1.217 -
   1.218 -fun prover thm = prove_goal Stream.thy thm
   1.219 - (fn prems =>
   1.220 -        [
   1.221 -        (cut_facts_tac prems 1),
   1.222 -        (rtac streamE 1),
   1.223 -        (contr_tac 1),
   1.224 -        (REPEAT (asm_simp_tac (!simpset addsimps stream_discsel) 1))
   1.225 -        ]);
   1.226 -
   1.227 -val stream_discsel_def = 
   1.228 -        [
   1.229 -        prover "s~=UU ==> is_scons`s ~= UU", 
   1.230 -        prover "s~=UU ==> shd`s ~=UU" 
   1.231 -        ];
   1.232 -
   1.233 -val stream_rews = stream_discsel_def @ stream_rews;
   1.234 -
   1.235 -
   1.236 -(* ------------------------------------------------------------------------*)
   1.237 -(* Properties stream_take                                                  *)
   1.238 -(* ------------------------------------------------------------------------*)
   1.239 -
   1.240 -val stream_take =
   1.241 -        [
   1.242 -prove_goalw Stream.thy [stream_take_def] "stream_take n`UU = UU"
   1.243 - (fn prems =>
   1.244 -        [
   1.245 -        (res_inst_tac [("n","n")] natE 1),
   1.246 -        (Asm_simp_tac 1),
   1.247 -        (Asm_simp_tac 1),
   1.248 -        (simp_tac (!simpset addsimps stream_rews) 1)
   1.249 -        ]),
   1.250 -prove_goalw Stream.thy [stream_take_def] "stream_take 0`xs=UU"
   1.251 - (fn prems =>
   1.252 -        [
   1.253 -        (Asm_simp_tac 1)
   1.254 -        ])];
   1.255 -
   1.256 -fun prover thm = prove_goalw Stream.thy [stream_take_def] thm
   1.257 - (fn prems =>
   1.258 -        [
   1.259 -        (cut_facts_tac prems 1),
   1.260 -        (Simp_tac 1),
   1.261 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
   1.262 -        ]);
   1.263 -
   1.264 -val stream_take = [
   1.265 -prover 
   1.266 -  "x~=UU ==> stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
   1.267 -        ] @ stream_take;
   1.268 -
   1.269 -val stream_rews = stream_take @ stream_rews;
   1.270 -
   1.271 -(* ------------------------------------------------------------------------*)
   1.272 -(* enhance the simplifier                                                  *)
   1.273 -(* ------------------------------------------------------------------------*)
   1.274 -
   1.275 -qed_goal "stream_copy2" Stream.thy 
   1.276 -     "stream_copy`f`(scons`x`xs) = scons`x`(f`xs)"
   1.277 - (fn prems =>
   1.278 -        [
   1.279 -        (case_tac "x=UU" 1),
   1.280 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.281 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
   1.282 -        ]);
   1.283 -
   1.284 -qed_goal "shd2" Stream.thy "shd`(scons`x`xs) = x"
   1.285 - (fn prems =>
   1.286 -        [
   1.287 -        (case_tac "x=UU" 1),
   1.288 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.289 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
   1.290 -        ]);
   1.291 -
   1.292 -qed_goal "stream_take2" Stream.thy 
   1.293 - "stream_take (Suc n)`(scons`x`xs) = scons`x`(stream_take n`xs)"
   1.294 - (fn prems =>
   1.295 -        [
   1.296 -        (case_tac "x=UU" 1),
   1.297 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.298 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
   1.299 -        ]);
   1.300 -
   1.301 -val stream_rews = [stream_iso_strict RS conjunct1,
   1.302 -                   stream_iso_strict RS conjunct2,
   1.303 -                   hd stream_copy, stream_copy2]
   1.304 -                  @ stream_when
   1.305 -                  @ [hd stream_discsel,shd2] @ (tl (tl stream_discsel))  
   1.306 -                  @ stream_constrdef
   1.307 -                  @ stream_discsel_def
   1.308 -                  @ [ stream_take2] @ (tl stream_take);
   1.309 -
   1.310 -
   1.311 -(* ------------------------------------------------------------------------*)
   1.312 -(* take lemma for streams                                                  *)
   1.313 -(* ------------------------------------------------------------------------*)
   1.314 -
   1.315 -fun prover reach defs thm  = prove_goalw Stream.thy defs thm
   1.316 - (fn prems =>
   1.317 -        [
   1.318 -        (res_inst_tac [("t","s1")] (reach RS subst) 1),
   1.319 -        (res_inst_tac [("t","s2")] (reach RS subst) 1),
   1.320 -        (stac fix_def2 1),
   1.321 -        (stac contlub_cfun_fun 1),
   1.322 -        (rtac is_chain_iterate 1),
   1.323 -        (stac contlub_cfun_fun 1),
   1.324 -        (rtac is_chain_iterate 1),
   1.325 -        (rtac lub_equal 1),
   1.326 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   1.327 -        (rtac (is_chain_iterate RS ch2ch_fappL) 1),
   1.328 -        (rtac allI 1),
   1.329 -        (resolve_tac prems 1)
   1.330 -        ]);
   1.331 -
   1.332 -val stream_take_lemma = prover stream_reach  [stream_take_def]
   1.333 -        "(!!n.stream_take n`s1 = stream_take n`s2) ==> s1=s2";
   1.334 -
   1.335 -
   1.336 -qed_goal "stream_reach2" Stream.thy  "lub(range(%i.stream_take i`s))=s"
   1.337 - (fn prems =>
   1.338 -        [
   1.339 -        (res_inst_tac [("t","s")] (stream_reach RS subst) 1),
   1.340 -        (stac fix_def2 1),
   1.341 -        (rewtac stream_take_def),
   1.342 -        (stac contlub_cfun_fun 1),
   1.343 -        (rtac is_chain_iterate 1),
   1.344 -        (rtac refl 1)
   1.345 -        ]);
   1.346 -
   1.347 -(* ------------------------------------------------------------------------*)
   1.348 -(* Co -induction for streams                                               *)
   1.349 -(* ------------------------------------------------------------------------*)
   1.350 -
   1.351 -qed_goalw "stream_coind_lemma" Stream.thy [stream_bisim_def] 
   1.352 -"stream_bisim R ==> ! p q. R p q --> stream_take n`p = stream_take n`q"
   1.353 - (fn prems =>
   1.354 -        [
   1.355 -        (cut_facts_tac prems 1),
   1.356 -        (nat_ind_tac "n" 1),
   1.357 -        (simp_tac (!simpset addsimps stream_rews) 1),
   1.358 -        (strip_tac 1),
   1.359 -        ((etac allE 1) THEN (etac allE 1) THEN (etac (mp RS disjE) 1)),
   1.360 -        (atac 1),
   1.361 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.362 -        (etac exE 1),
   1.363 -        (etac exE 1),
   1.364 -        (etac exE 1),
   1.365 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.366 -        (REPEAT (etac conjE 1)),
   1.367 -        (rtac cfun_arg_cong 1),
   1.368 -        (fast_tac HOL_cs 1)
   1.369 -        ]);
   1.370 -
   1.371 -qed_goal "stream_coind" Stream.thy "[|stream_bisim R ;R p q|] ==> p = q"
   1.372 - (fn prems =>
   1.373 -        [
   1.374 -        (rtac stream_take_lemma 1),
   1.375 -        (rtac (stream_coind_lemma RS spec RS spec RS mp) 1),
   1.376 -        (resolve_tac prems 1),
   1.377 -        (resolve_tac prems 1)
   1.378 -        ]);
   1.379 -
   1.380 -(* ------------------------------------------------------------------------*)
   1.381 -(* structural induction for admissible predicates                          *)
   1.382 -(* ------------------------------------------------------------------------*)
   1.383 -
   1.384 -qed_goal "stream_finite_ind" Stream.thy
   1.385 -"[|P(UU);\
   1.386 -\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
   1.387 -\  |] ==> !s.P(stream_take n`s)"
   1.388 - (fn prems =>
   1.389 -        [
   1.390 -        (nat_ind_tac "n" 1),
   1.391 -        (simp_tac (!simpset addsimps stream_rews) 1),
   1.392 -        (resolve_tac prems 1),
   1.393 -        (rtac allI 1),
   1.394 -        (res_inst_tac [("s","s")] streamE 1),
   1.395 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.396 -        (resolve_tac prems 1),
   1.397 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.398 -        (resolve_tac prems 1),
   1.399 -        (atac 1),
   1.400 -        (etac spec 1)
   1.401 -        ]);
   1.402 -
   1.403 -qed_goalw "stream_finite_ind2" Stream.thy  [stream_finite_def]
   1.404 -"(!!n.P(stream_take n`s)) ==>  stream_finite(s) -->P(s)"
   1.405 - (fn prems =>
   1.406 -        [
   1.407 -        (strip_tac 1),
   1.408 -        (etac exE 1),
   1.409 -        (etac subst 1),
   1.410 -        (resolve_tac prems 1)
   1.411 -        ]);
   1.412 -
   1.413 -qed_goal "stream_finite_ind3" Stream.thy 
   1.414 -"[|P(UU);\
   1.415 -\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
   1.416 -\  |] ==> stream_finite(s) --> P(s)"
   1.417 - (fn prems =>
   1.418 -        [
   1.419 -        (rtac stream_finite_ind2 1),
   1.420 -        (rtac (stream_finite_ind RS spec) 1),
   1.421 -        (REPEAT (resolve_tac prems 1)),
   1.422 -        (REPEAT (atac 1))
   1.423 -        ]);
   1.424 -
   1.425 -(* prove induction using definition of admissibility 
   1.426 -   stream_reach rsp. stream_reach2 
   1.427 -   and finite induction stream_finite_ind *)
   1.428 -
   1.429 -qed_goal "stream_ind" Stream.thy
   1.430 -"[|adm(P);\
   1.431 -\  P(UU);\
   1.432 -\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
   1.433 -\  |] ==> P(s)"
   1.434 - (fn prems =>
   1.435 -        [
   1.436 -        (rtac (stream_reach2 RS subst) 1),
   1.437 -        (rtac (adm_def2 RS iffD1 RS spec RS mp RS mp) 1),
   1.438 -        (resolve_tac prems 1),
   1.439 -        (SELECT_GOAL (rewtac stream_take_def) 1),
   1.440 -        (rtac ch2ch_fappL 1),
   1.441 -        (rtac is_chain_iterate 1),
   1.442 -        (rtac allI 1),
   1.443 -        (rtac (stream_finite_ind RS spec) 1),
   1.444 -        (REPEAT (resolve_tac prems 1)),
   1.445 -        (REPEAT (atac 1))
   1.446 -        ]);
   1.447 -
   1.448 -(* prove induction with usual LCF-Method using fixed point induction *)
   1.449 -qed_goal "stream_ind" Stream.thy
   1.450 -"[|adm(P);\
   1.451 -\  P(UU);\
   1.452 -\  !! x s1.[|x~=UU;P(s1)|] ==> P(scons`x`s1)\
   1.453 -\  |] ==> P(s)"
   1.454 - (fn prems =>
   1.455 -        [
   1.456 -        (rtac (stream_reach RS subst) 1),
   1.457 -        (res_inst_tac [("x","s")] spec 1),
   1.458 -        (rtac wfix_ind 1),
   1.459 -        (rtac adm_impl_admw 1),
   1.460 -        (REPEAT (resolve_tac adm_thms 1)),
   1.461 -        (rtac adm_subst 1),
   1.462 -        (cont_tacR 1),
   1.463 -        (resolve_tac prems 1),
   1.464 -        (rtac allI 1),
   1.465 -        (rtac (rewrite_rule [stream_take_def] stream_finite_ind) 1),
   1.466 -        (REPEAT (resolve_tac prems 1)),
   1.467 -        (REPEAT (atac 1))
   1.468 -        ]);
   1.469 -
   1.470 -
   1.471 -(* ------------------------------------------------------------------------*)
   1.472 -(* simplify use of Co-induction                                            *)
   1.473 -(* ------------------------------------------------------------------------*)
   1.474 -
   1.475 -qed_goal "surjectiv_scons" Stream.thy "scons`(shd`s)`(stl`s)=s"
   1.476 - (fn prems =>
   1.477 -        [
   1.478 -        (res_inst_tac [("s","s")] streamE 1),
   1.479 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.480 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
   1.481 -        ]);
   1.482 -
   1.483 -
   1.484 -qed_goalw "stream_coind_lemma2" Stream.thy [stream_bisim_def]
   1.485 -"!s1 s2. R s1 s2 --> shd`s1 = shd`s2 & R (stl`s1) (stl`s2) ==> stream_bisim R"
   1.486 - (fn prems =>
   1.487 -        [
   1.488 -        (cut_facts_tac prems 1),
   1.489 -        (strip_tac 1),
   1.490 -        (etac allE 1),
   1.491 -        (etac allE 1),
   1.492 -        (dtac mp 1),
   1.493 -        (atac 1),
   1.494 -        (etac conjE 1),
   1.495 -        (case_tac "s1 = UU & s2 = UU" 1),
   1.496 -        (rtac disjI1 1),
   1.497 -        (fast_tac HOL_cs 1),
   1.498 -        (rtac disjI2 1),
   1.499 -        (rtac disjE 1),
   1.500 -        (etac (de_Morgan_conj RS subst) 1),
   1.501 -        (res_inst_tac [("x","shd`s1")] exI 1),
   1.502 -        (res_inst_tac [("x","stl`s1")] exI 1),
   1.503 -        (res_inst_tac [("x","stl`s2")] exI 1),
   1.504 -        (rtac conjI 1),
   1.505 -        (eresolve_tac stream_discsel_def 1),
   1.506 -        (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
   1.507 -        (eres_inst_tac [("s","shd`s1"),("t","shd`s2")] subst 1),
   1.508 -        (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
   1.509 -        (res_inst_tac [("x","shd`s2")] exI 1),
   1.510 -        (res_inst_tac [("x","stl`s1")] exI 1),
   1.511 -        (res_inst_tac [("x","stl`s2")] exI 1),
   1.512 -        (rtac conjI 1),
   1.513 -        (eresolve_tac stream_discsel_def 1),
   1.514 -        (asm_simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1),
   1.515 -        (res_inst_tac [("s","shd`s1"),("t","shd`s2")] ssubst 1),
   1.516 -        (etac sym 1),
   1.517 -        (simp_tac (!simpset addsimps stream_rews addsimps [surjectiv_scons]) 1)
   1.518 -        ]);
   1.519 -
   1.520 -
   1.521 -(* ------------------------------------------------------------------------*)
   1.522 -(* theorems about finite and infinite streams                              *)
   1.523 -(* ------------------------------------------------------------------------*)
   1.524 -
   1.525 -(* ----------------------------------------------------------------------- *)
   1.526 -(* 2 lemmas about stream_finite                                            *)
   1.527 -(* ----------------------------------------------------------------------- *)
   1.528 -
   1.529 -qed_goalw "stream_finite_UU" Stream.thy [stream_finite_def]
   1.530 -         "stream_finite(UU)"
   1.531 - (fn prems =>
   1.532 -        [
   1.533 -        (rtac exI 1),
   1.534 -        (simp_tac (!simpset addsimps stream_rews) 1)
   1.535 -        ]);
   1.536 -
   1.537 -qed_goal "inf_stream_not_UU" Stream.thy  "~stream_finite(s)  ==> s ~= UU"
   1.538 - (fn prems =>
   1.539 -        [
   1.540 -        (cut_facts_tac prems 1),
   1.541 -        (etac swap 1),
   1.542 -        (dtac notnotD 1),
   1.543 -        (hyp_subst_tac  1),
   1.544 -        (rtac stream_finite_UU 1)
   1.545 -        ]);
   1.546 -
   1.547 -(* ----------------------------------------------------------------------- *)
   1.548 -(* a lemma about shd                                                       *)
   1.549 -(* ----------------------------------------------------------------------- *)
   1.550 -
   1.551 -qed_goal "stream_shd_lemma1" Stream.thy "shd`s=UU --> s=UU"
   1.552 - (fn prems =>
   1.553 -        [
   1.554 -        (res_inst_tac [("s","s")] streamE 1),
   1.555 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.556 -        (hyp_subst_tac 1),
   1.557 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
   1.558 -        ]);
   1.559 -
   1.560 -
   1.561 -(* ----------------------------------------------------------------------- *)
   1.562 -(* lemmas about stream_take                                                *)
   1.563 -(* ----------------------------------------------------------------------- *)
   1.564 -
   1.565 -qed_goal "stream_take_lemma1" Stream.thy 
   1.566 - "!x xs.x~=UU --> \
   1.567 -\  stream_take (Suc n)`(scons`x`xs) = scons`x`xs --> stream_take n`xs=xs"
   1.568 - (fn prems =>
   1.569 -        [
   1.570 -        (rtac allI 1),
   1.571 -        (rtac allI 1),
   1.572 -        (rtac impI 1),
   1.573 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.574 -        (strip_tac 1),
   1.575 -        (rtac ((hd stream_inject) RS conjunct2) 1),
   1.576 -        (atac 1),
   1.577 -        (atac 1),
   1.578 -        (atac 1)
   1.579 -        ]);
   1.580 -
   1.581 -
   1.582 -qed_goal "stream_take_lemma2" Stream.thy 
   1.583 - "! s2. stream_take n`s2 = s2 --> stream_take (Suc n)`s2=s2"
   1.584 - (fn prems =>
   1.585 -        [
   1.586 -        (nat_ind_tac "n" 1),
   1.587 -        (simp_tac (!simpset addsimps stream_rews) 1),
   1.588 -        (strip_tac 1),
   1.589 -        (res_inst_tac [("s","s2")] streamE 1),
   1.590 -         (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.591 -	(hyp_subst_tac 1),
   1.592 -	(rotate_tac ~1 1),
   1.593 -        (asm_full_simp_tac (!simpset addsimps stream_rews) 1),
   1.594 -        (subgoal_tac "stream_take n1`xs = xs" 1),
   1.595 -         (rtac ((hd stream_inject) RS conjunct2) 2),
   1.596 -           (atac 4),
   1.597 -          (atac 2),
   1.598 -         (atac 2),
   1.599 -        (rtac cfun_arg_cong 1),
   1.600 -        (fast_tac HOL_cs 1)
   1.601 -        ]);
   1.602 -
   1.603 -qed_goal "stream_take_lemma3" Stream.thy 
   1.604 - "!x xs.x~=UU --> \
   1.605 -\  stream_take n`(scons`x`xs) = scons`x`xs --> stream_take n`xs=xs"
   1.606 - (fn prems =>
   1.607 -        [
   1.608 -        (nat_ind_tac "n" 1),
   1.609 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.610 -        (strip_tac 1 ),
   1.611 -        (res_inst_tac [("P","scons`x`xs=UU")] notE 1),
   1.612 -        (eresolve_tac stream_constrdef 1),
   1.613 -        (etac sym 1),
   1.614 -        (strip_tac 1 ),
   1.615 -        (rtac (stream_take_lemma2 RS spec RS mp) 1),
   1.616 -        (res_inst_tac [("x1.1","x")] ((hd stream_inject) RS conjunct2) 1),
   1.617 -        (atac 1),
   1.618 -        (atac 1),
   1.619 -        (etac (stream_take2 RS subst) 1)
   1.620 -        ]);
   1.621 -
   1.622 -qed_goal "stream_take_lemma4" Stream.thy 
   1.623 - "!x xs.\
   1.624 -\stream_take n`xs=xs --> stream_take (Suc n)`(scons`x`xs) = scons`x`xs"
   1.625 - (fn prems =>
   1.626 -        [
   1.627 -        (nat_ind_tac "n" 1),
   1.628 -        (simp_tac (!simpset addsimps stream_rews) 1),
   1.629 -        (simp_tac (!simpset addsimps stream_rews) 1)
   1.630 -        ]);
   1.631 -
   1.632 -(* ---- *)
   1.633 -
   1.634 -qed_goal "stream_take_lemma5" Stream.thy 
   1.635 -"!s. stream_take n`s=s --> iterate n stl s=UU"
   1.636 - (fn prems =>
   1.637 -        [
   1.638 -        (nat_ind_tac "n" 1),
   1.639 -        (Simp_tac 1),
   1.640 -        (simp_tac (!simpset addsimps stream_rews) 1),
   1.641 -        (strip_tac 1),
   1.642 -        (res_inst_tac [("s","s")] streamE 1),
   1.643 -        (hyp_subst_tac 1),
   1.644 -        (stac iterate_Suc2 1),
   1.645 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.646 -        (stac iterate_Suc2 1),
   1.647 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.648 -        (etac allE 1),
   1.649 -        (etac mp 1),
   1.650 -        (hyp_subst_tac 1),
   1.651 -        (etac (stream_take_lemma1 RS spec RS spec RS mp RS mp) 1),
   1.652 -        (atac 1)
   1.653 -        ]);
   1.654 -
   1.655 -qed_goal "stream_take_lemma6" Stream.thy 
   1.656 -"!s.iterate n stl s =UU --> stream_take n`s=s"
   1.657 - (fn prems =>
   1.658 -        [
   1.659 -        (nat_ind_tac "n" 1),
   1.660 -        (Simp_tac 1),
   1.661 -        (strip_tac 1),
   1.662 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.663 -        (rtac allI 1),
   1.664 -        (res_inst_tac [("s","s")] streamE 1),
   1.665 -        (hyp_subst_tac 1),
   1.666 -        (asm_simp_tac (!simpset addsimps stream_rews) 1),
   1.667 -        (hyp_subst_tac 1),
   1.668 -        (stac iterate_Suc2 1),
   1.669 -        (asm_simp_tac (!simpset addsimps stream_rews) 1)
   1.670 -        ]);
   1.671 -
   1.672 -qed_goal "stream_take_lemma7" Stream.thy 
   1.673 -"(iterate n stl s=UU) = (stream_take n`s=s)"
   1.674 - (fn prems =>
   1.675 -        [
   1.676 -        (rtac iffI 1),
   1.677 -        (etac (stream_take_lemma6 RS spec RS mp) 1),
   1.678 -        (etac (stream_take_lemma5 RS spec RS mp) 1)
   1.679 -        ]);
   1.680 -
   1.681 -
   1.682 -qed_goal "stream_take_lemma8" Stream.thy
   1.683 -"[|adm(P); !n. ? m. n < m & P (stream_take m`s)|] ==> P(s)"
   1.684 - (fn prems =>
   1.685 -        [
   1.686 -        (cut_facts_tac prems 1),
   1.687 -        (rtac (stream_reach2 RS subst) 1),
   1.688 -        (rtac adm_lemma11 1),
   1.689 -        (atac 1),
   1.690 -        (atac 2),
   1.691 -        (rewtac stream_take_def),
   1.692 -        (rtac ch2ch_fappL 1),
   1.693 -        (rtac is_chain_iterate 1)
   1.694 -        ]);
   1.695 -
   1.696 -(* ----------------------------------------------------------------------- *)
   1.697 -(* lemmas stream_finite                                                    *)
   1.698 -(* ----------------------------------------------------------------------- *)
   1.699 -
   1.700 -qed_goalw "stream_finite_lemma1" Stream.thy [stream_finite_def]
   1.701 - "stream_finite(xs) ==> stream_finite(scons`x`xs)"
   1.702 - (fn prems =>
   1.703 -        [
   1.704 -        (cut_facts_tac prems 1),
   1.705 -        (etac exE 1),
   1.706 -        (rtac exI 1),
   1.707 -        (etac (stream_take_lemma4 RS spec RS spec RS mp) 1)
   1.708 -        ]);
   1.709 -
   1.710 -qed_goalw "stream_finite_lemma2" Stream.thy [stream_finite_def]
   1.711 - "[|x~=UU; stream_finite(scons`x`xs)|] ==> stream_finite(xs)"
   1.712 - (fn prems =>
   1.713 -        [
   1.714 -        (cut_facts_tac prems 1),
   1.715 -        (etac exE 1),
   1.716 -        (rtac exI 1),
   1.717 -        (etac (stream_take_lemma3 RS spec RS spec RS mp RS mp) 1),
   1.718 -        (atac 1)
   1.719 -        ]);
   1.720 -
   1.721 -qed_goal "stream_finite_lemma3" Stream.thy 
   1.722 - "x~=UU ==> stream_finite(scons`x`xs) = stream_finite(xs)"
   1.723 - (fn prems =>
   1.724 -        [
   1.725 -        (cut_facts_tac prems 1),
   1.726 -        (rtac iffI 1),
   1.727 -        (etac stream_finite_lemma2 1),
   1.728 -        (atac 1),
   1.729 -        (etac stream_finite_lemma1 1)
   1.730 -        ]);
   1.731 -
   1.732 -
   1.733 -qed_goalw "stream_finite_lemma5" Stream.thy [stream_finite_def]
   1.734 - "(!n. s1 << s2  --> stream_take n`s2 = s2 --> stream_finite(s1))\
   1.735 -\=(s1 << s2  --> stream_finite(s2) --> stream_finite(s1))"
   1.736 - (fn prems =>
   1.737 -        [
   1.738 -        (rtac iffI 1),
   1.739 -        (fast_tac HOL_cs 1),
   1.740 -        (fast_tac HOL_cs 1)
   1.741 -        ]);
   1.742 -
   1.743 -qed_goal "stream_finite_lemma6" Stream.thy
   1.744 - "!s1 s2. s1 << s2  --> stream_take n`s2 = s2 --> stream_finite(s1)"
   1.745 - (fn prems =>
   1.746 -        [
   1.747 -        (nat_ind_tac "n" 1),
   1.748 -        (simp_tac (!simpset addsimps stream_rews) 1),
   1.749 -        (strip_tac 1 ),
   1.750 -        (hyp_subst_tac  1),
   1.751 -        (dtac UU_I 1),
   1.752 -        (hyp_subst_tac  1),
   1.753 -        (rtac stream_finite_UU 1),
   1.754 -        (rtac allI 1),
   1.755 -        (rtac allI 1),
   1.756 -        (res_inst_tac [("s","s1")] streamE 1),
   1.757 -        (hyp_subst_tac  1),
   1.758 -        (strip_tac 1 ),
   1.759 -        (rtac stream_finite_UU 1),
   1.760 -        (hyp_subst_tac  1),
   1.761 -        (res_inst_tac [("s","s2")] streamE 1),
   1.762 -        (hyp_subst_tac  1),
   1.763 -        (strip_tac 1 ),
   1.764 -        (dtac UU_I 1),
   1.765 -        (asm_simp_tac(!simpset addsimps (stream_rews @ [stream_finite_UU])) 1),
   1.766 -        (hyp_subst_tac  1),
   1.767 -        (simp_tac (!simpset addsimps stream_rews) 1),
   1.768 -        (strip_tac 1 ),
   1.769 -        (rtac stream_finite_lemma1 1),
   1.770 -        (subgoal_tac "xs << xsa" 1),
   1.771 -        (subgoal_tac "stream_take n1`xsa = xsa" 1),
   1.772 -        (fast_tac HOL_cs 1),
   1.773 -        (res_inst_tac  [("x1.1","xa"),("y1.1","xa")] 
   1.774 -                   ((hd stream_inject) RS conjunct2) 1),
   1.775 -        (atac 1),
   1.776 -        (atac 1),
   1.777 -        (atac 1),
   1.778 -        (res_inst_tac [("x1.1","x"),("y1.1","xa")]
   1.779 -         ((hd stream_invert) RS conjunct2) 1),
   1.780 -        (atac 1),
   1.781 -        (atac 1),
   1.782 -        (atac 1)
   1.783 -        ]);
   1.784 -
   1.785 -qed_goal "stream_finite_lemma7" Stream.thy 
   1.786 -"s1 << s2  --> stream_finite(s2) --> stream_finite(s1)"
   1.787 - (fn prems =>
   1.788 -        [
   1.789 -        (rtac (stream_finite_lemma5 RS iffD1) 1),
   1.790 -        (rtac allI 1),
   1.791 -        (rtac (stream_finite_lemma6 RS spec RS spec) 1)
   1.792 -        ]);
   1.793 -
   1.794 -qed_goalw "stream_finite_lemma8" Stream.thy [stream_finite_def]
   1.795 -"stream_finite(s) = (? n. iterate n stl s = UU)"
   1.796 - (fn prems =>
   1.797 -        [
   1.798 -        (simp_tac (!simpset addsimps [stream_take_lemma7]) 1)
   1.799 -        ]);
   1.800 -
   1.801 -
   1.802 -(* ----------------------------------------------------------------------- *)
   1.803 -(* admissibility of ~stream_finite                                         *)
   1.804 -(* ----------------------------------------------------------------------- *)
   1.805 -
   1.806 -qed_goalw "adm_not_stream_finite" Stream.thy [adm_def]
   1.807 - "adm(%s. ~ stream_finite(s))"
   1.808 - (fn prems =>
   1.809 -        [
   1.810 -        (strip_tac 1 ),
   1.811 -        (res_inst_tac [("P1","!i. ~ stream_finite(Y(i))")] classical2 1),
   1.812 -        (atac 2),
   1.813 -        (subgoal_tac "!i.stream_finite(Y(i))" 1),
   1.814 -        (fast_tac HOL_cs 1),
   1.815 -        (rtac allI 1),
   1.816 -        (rtac (stream_finite_lemma7 RS mp RS mp) 1),
   1.817 -        (etac is_ub_thelub 1),
   1.818 -        (atac 1)
   1.819 -        ]);
   1.820 -
   1.821 -(* ----------------------------------------------------------------------- *)
   1.822 -(* alternative prove for admissibility of ~stream_finite                   *)
   1.823 -(* show that stream_finite(s) = (? n. iterate n stl s = UU)                *)
   1.824 -(* and prove adm. of ~(? n. iterate n stl s = UU)                          *)
   1.825 -(* proof uses theorems stream_take_lemma5-7; stream_finite_lemma8          *)
   1.826 -(* ----------------------------------------------------------------------- *)
   1.827 -
   1.828 -
   1.829 -qed_goal "adm_not_stream_finite" Stream.thy "adm(%s. ~ stream_finite(s))"
   1.830 - (fn prems =>
   1.831 -        [
   1.832 -        (subgoal_tac "(!s.(~stream_finite(s))=(!n.iterate n stl s ~=UU))" 1),
   1.833 -        (etac (adm_cong RS iffD2)1),
   1.834 -        (REPEAT(resolve_tac adm_thms 1)),
   1.835 -        (rtac  cont_iterate2 1),
   1.836 -        (rtac allI 1),
   1.837 -        (stac stream_finite_lemma8 1),
   1.838 -        (fast_tac HOL_cs 1)
   1.839 -        ]);
   1.840 -
   1.841 -