Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/ex/Stream.ML
changeset 11348 e08a0855af67
parent 10835 f4745d77e620
child 11355 778c369559d9
equal deleted inserted replaced
11347:4e41f71179ed 11348:e08a0855af67 
     1 (*  Title: 	HOLCF/ex//Stream.ML
 
     1 (*  Title: 	HOLCF/ex//Stream.ML
 
     2     ID:         $Id$
 
     2     ID:         $Id$
 
     3     Author: 	Franz Regensburger, David von Oheimb
 
     3     Author: 	Franz Regensburger, David von Oheimb
 
     4     Copyright   1993, 1995 Technische Universitaet Muenchen
 
     4     Copyright   1993, 1995 Technische Universitaet Muenchen
 
       
     5     Author: 	David von Oheimb (major extensions)
 
       
     6     License:    GPL (GNU GENERAL PUBLIC LICENSE)
 
     5 
     7 
     6 general Stream domain
 
     8 general Stream domain
 
     7 *)
 
     9 *)
 
     8 
    10 
     9 fun stream_case_tac s i = res_inst_tac [("x",s)] stream.casedist i
 
    11 fun stream_case_tac s i = res_inst_tac [("x",s)] stream.casedist i
 
    10 			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
 
    12 			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
 
    11 
    13 
    12 
    14 
    13 val [stream_con_rew1,stream_con_rew2] = stream.con_rews;
 
    15 val [stream_con_rew1,stream_con_rew2] = stream.con_rews;
 
    14 
    16 
    15 Addsimps stream.take_rews;
 
    17 Addsimps stream.rews;
 
    16 Addsimps stream.when_rews;
 
    18 Addsimps[eq_UU_iff RS sym];
 
    17 Addsimps stream.sel_rews;
 
       
    18 
    19 
    19 (* ----------------------------------------------------------------------- *)
 
    20 (* ----------------------------------------------------------------------- *)
 
    20 (* theorems about scons                                                    *)
 
    21 (* theorems about scons                                                    *)
 
    21 (* ----------------------------------------------------------------------- *)
 
    22 (* ----------------------------------------------------------------------- *)
 
    22 
    23 
    57 Goal "b ~= UU ==> x << b && z = \
 
    58 Goal "b ~= UU ==> x << b && z = \
 
    58 \           (x = UU |  (EX a y. x = a && y &  a ~= UU &  a << b &  y << z))";
 
    59 \           (x = UU |  (EX a y. x = a && y &  a ~= UU &  a << b &  y << z))";
 
    59 by Safe_tac;
 
    60 by Safe_tac;
 
    60 by (stream_case_tac "x" 1);
 
    61 by (stream_case_tac "x" 1);
 
    61 by (safe_tac (claset() addSDs stream.inverts 
    62 by (safe_tac (claset() addSDs stream.inverts 
    62                 addSIs [minimal, monofun_cfun, monofun_cfun_arg]));
 
    63                 addSIs [monofun_cfun, monofun_cfun_arg]));
 
    63 by (Fast_tac 1);
 
    64 by (Fast_tac 1);
 
    64 qed "stream_prefix'";
 
    65 qed "stream_prefix'";
 
    65 
    66 
    66 Goal "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b &  s = t)";
 
    67 Goal "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b &  s = t)";
 
    67 by (best_tac (claset() addSEs stream.injects) 1);
 
    68 by (best_tac (claset() addSEs stream.injects) 1);
 
    68 qed "stream_inject_eq";	
    69 qed "stream_inject_eq";	
       
    70 Addsimps [stream_inject_eq];
 
    69 
    71 
    70 
    72 
    71 (* ----------------------------------------------------------------------- *)
 
    73 (* ----------------------------------------------------------------------- *)
 
    72 (* theorems about stream_when                                              *)
 
    74 (* theorems about stream_when                                              *)
 
    73 (* ----------------------------------------------------------------------- *)
 
    75 (* ----------------------------------------------------------------------- *)
 
    74 
    76 
    75 section "stream_when";
 
    77 section "stream_when";
 
    76 
    78 
    77 Goal "stream_when$UU$s=UU";
 
    79 Goal "stream_when$UU$s=UU";
 
    78 by (stream_case_tac "s" 1);
 
    80 by (stream_case_tac "s" 1);
 
    79 by (ALLGOALS(asm_simp_tac (simpset() addsimps [strict_Rep_CFun1])));
 
    81 by (ALLGOALS Asm_simp_tac);
 
    80 qed "stream_when_strictf";
 
    82 qed "stream_when_strictf";
 
    81 	
    83 	
    82 
    84 
    83 (* ----------------------------------------------------------------------- *)
 
    85 (* ----------------------------------------------------------------------- *)
 
    84 (* theorems about ft and rt                                                *)
 
    86 (* theorems about ft and rt                                                *)
 
    93 qed "stream_ft_lemma1";
 
    95 qed "stream_ft_lemma1";
 
    94 *)
 
    96 *)
 
    95 
    97 
    96 Goal "s~=UU ==> ft$s~=UU";
 
    98 Goal "s~=UU ==> ft$s~=UU";
 
    97 by (stream_case_tac "s" 1);
 
    99 by (stream_case_tac "s" 1);
 
    98 by (Blast_tac 1);
 
   100 by  (Blast_tac 1);
 
    99 by (asm_simp_tac (simpset() addsimps stream.rews) 1);
 
   101 by (Asm_simp_tac 1);
 
   100 qed "ft_defin";
 
   102 qed "ft_defin";
 
   101 
   103 
   102 Goal "rt$s~=UU ==> s~=UU";
 
   104 Goal "rt$s~=UU ==> s~=UU";
 
   103 by Auto_tac;
 
   105 by Auto_tac;
 
   104 qed "rt_strict_rev";
 
   106 qed "rt_strict_rev";
 
   105 
   107 
   106 Goal "(ft$s)&&(rt$s)=s";
 
   108 Goal "(ft$s)&&(rt$s)=s";
 
   107 by (stream_case_tac "s" 1);
 
   109 by (stream_case_tac "s" 1);
 
   108 by (ALLGOALS (asm_simp_tac (simpset() addsimps stream.rews)));
 
   110 by (ALLGOALS Asm_simp_tac);
 
   109 qed "surjectiv_scons";
 
   111 qed "surjectiv_scons";
 
   110 
   112 
   111 Goal "ALL x s. x << s --> iterate i rt x << iterate i rt s";
 
   113 Goal "ALL x s. x << s --> iterate i rt x << iterate i rt s";
 
   112 by (induct_tac "i" 1);
 
   114 by (induct_tac "i" 1);
 
   113 by (Simp_tac 1);
 
   115 by (Simp_tac 1);
 
   134 by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
 
   136 by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
 
   135 qed "stream_reach2";
 
   137 qed "stream_reach2";
 
   136 
   138 
   137 Goal "chain (%i. stream_take i$s)";
 
   139 Goal "chain (%i. stream_take i$s)";
 
   138 by (rtac chainI 1);
 
   140 by (rtac chainI 1);
 
   139 by (subgoal_tac "ALL i s. stream_take i$s << stream_take (Suc i)$s" 1);
 
   141 by (subgoal_tac "ALL i s::'a stream. stream_take i$s << stream_take (Suc i)$s" 1);
 
   140 by (Fast_tac 1);
 
   142 by (Fast_tac 1);
 
   141 by (rtac allI 1);
 
   143 by (rtac allI 1);
 
   142 by (induct_tac "ia" 1);
 
   144 by (induct_tac "ia" 1);
 
   143 by (Simp_tac 1);
 
   145 by (Simp_tac 1);
 
   144 by (rtac allI 1);
 
   146 by (rtac allI 1);
 
   156 by (rtac monofun_cfun_fun 1);
 
   158 by (rtac monofun_cfun_fun 1);
 
   157 by (stac fix_def2 1);
 
   159 by (stac fix_def2 1);
 
   158 by (rtac is_ub_thelub 1);
 
   160 by (rtac is_ub_thelub 1);
 
   159 by (rtac chain_iterate 1);
 
   161 by (rtac chain_iterate 1);
 
   160 by (etac subst 1 THEN rtac monofun_cfun_fun 1);
 
   162 by (etac subst 1 THEN rtac monofun_cfun_fun 1);
 
   161 by (rtac (rewrite_rule [chain] chain_iterate RS spec) 1);
 
   163 by (rtac (rewrite_rule [chain_def] chain_iterate RS spec) 1);
 
   162 qed "stream_take_more";
 
   164 qed "stream_take_more";
 
   163 
   165 
   164 (*
 
   166 (*
 
   165 Goal 
   167 Goal 
   166  "ALL  s2. stream_take n$s2 = s2 --> stream_take (Suc n)$s2=s2";
 
   168  "ALL  s2. stream_take n$s2 = s2 --> stream_take (Suc n)$s2=s2";
 
   183 by (Blast_tac 1);
 
   185 by (Blast_tac 1);
 
   184 qed "stream_take_lemma2";
 
   186 qed "stream_take_lemma2";
 
   185 *)
 
   187 *)
 
   186 
   188 
   187 Goal 
   189 Goal 
   188  "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs";
 
   190 "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs";
 
   189 by (induct_tac "n" 1);
 
   191 by (induct_tac "n" 1);
 
   190 by (Asm_simp_tac 1);
 
   192 by (Asm_simp_tac 1);
 
   191 by (strip_tac 1);
 
   193 by (strip_tac 1);
 
   192 by (res_inst_tac [("P","x && xs=UU")] notE 1);
 
   194 by (res_inst_tac [("P","x && xs=UU")] notE 1);
 
   193 by (eresolve_tac stream.con_rews 1);
 
   195 by (eresolve_tac stream.con_rews 1);
 
   291 by (res_inst_tac [("x","ft$x")] exI 1);
 
   293 by (res_inst_tac [("x","ft$x")] exI 1);
 
   292 by (res_inst_tac [("x","rt$x")] exI 1);
 
   294 by (res_inst_tac [("x","rt$x")] exI 1);
 
   293 by (res_inst_tac [("x","rt$x'")] exI 1);
 
   295 by (res_inst_tac [("x","rt$x'")] exI 1);
 
   294 by (rtac conjI 1);
 
   296 by (rtac conjI 1);
 
   295 by (etac ft_defin 1);
 
   297 by (etac ft_defin 1);
 
   296 by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
 
   298 by (asm_simp_tac (simpset() addsimps [surjectiv_scons]) 1);
 
   297 by (eres_inst_tac [("s","ft$x"),("t","ft$x'")] subst 1);
 
   299 by (eres_inst_tac [("s","ft$x"),("t","ft$x'")] subst 1);
 
   298 by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
 
   300 by (simp_tac (simpset() addsimps [surjectiv_scons]) 1);
 
   299 by (res_inst_tac [("x","ft$x'")] exI 1);
 
   301 by (res_inst_tac [("x","ft$x'")] exI 1);
 
   300 by (res_inst_tac [("x","rt$x")] exI 1);
 
   302 by (res_inst_tac [("x","rt$x")] exI 1);
 
   301 by (res_inst_tac [("x","rt$x'")] exI 1);
 
   303 by (res_inst_tac [("x","rt$x'")] exI 1);
 
   302 by (rtac conjI 1);
 
   304 by (rtac conjI 1);
 
   303 by (etac ft_defin 1);
 
   305 by (etac ft_defin 1);
 
   304 by (asm_simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
 
   306 by (asm_simp_tac (simpset() addsimps [surjectiv_scons]) 1);
 
   305 by (res_inst_tac [("s","ft$x"),("t","ft$x'")] ssubst 1);
 
   307 by (res_inst_tac [("s","ft$x"),("t","ft$x'")] ssubst 1);
 
   306 by (etac sym 1);
 
   308 by (etac sym 1);
 
   307 by (simp_tac (simpset() addsimps stream.rews addsimps [surjectiv_scons]) 1);
 
   309 by (simp_tac (simpset() addsimps [surjectiv_scons]) 1);
 
   308 qed "stream_coind_lemma2";
 
   310 qed "stream_coind_lemma2";
 
   309 
   311 
   310 (* ----------------------------------------------------------------------- *)
 
   312 (* ----------------------------------------------------------------------- *)
 
   311 (* theorems about stream_finite                                            *)
 
   313 (* theorems about stream_finite                                            *)
 
   312 (* ----------------------------------------------------------------------- *)
 
   314 (* ----------------------------------------------------------------------- *)
 
   314 section "stream_finite";
 
   316 section "stream_finite";
 
   315 
   317 
   316 
   318 
   317 Goalw [stream.finite_def] "stream_finite UU";
 
   319 Goalw [stream.finite_def] "stream_finite UU";
 
   318 by (rtac exI 1);
 
   320 by (rtac exI 1);
 
   319 by (simp_tac (simpset() addsimps stream.rews) 1);
 
   321 by (Simp_tac 1);
 
   320 qed "stream_finite_UU";
 
   322 qed "stream_finite_UU";
 
   321 
   323 
   322 Goal  "~  stream_finite s ==> s ~= UU";
 
   324 Goal  "~  stream_finite s ==> s ~= UU";
 
   323 by (blast_tac (claset() addIs [stream_finite_UU]) 1);
 
   325 by (blast_tac (claset() addIs [stream_finite_UU]) 1);
 
   324 qed "stream_finite_UU_rev";
 
   326 qed "stream_finite_UU_rev";
 
   352 
   354 
   353 Goal "adm (%x. ~  stream_finite x)";
 
   355 Goal "adm (%x. ~  stream_finite x)";
 
   354 by (rtac admI2 1);
 
   356 by (rtac admI2 1);
 
   355 by (best_tac (claset() addIs [stream_finite_less, is_ub_thelub]) 1);
 
   357 by (best_tac (claset() addIs [stream_finite_less, is_ub_thelub]) 1);
 
   356 qed "adm_not_stream_finite";
 
   358 qed "adm_not_stream_finite";
 
       
   359 
       
   360 section "smap";
 
       
   361 
       
   362 bind_thm ("smap_unfold", fix_prover2 thy smap_def 
       
   363 	"smap = (\\<Lambda>f s. case s of x && l => f\\<cdot>x && smap\\<cdot>f\\<cdot>l)");
 
       
   364 
       
   365 Goal "smap\\<cdot>f\\<cdot>\\<bottom> = \\<bottom>";
 
       
   366 by (stac smap_unfold 1);
 
       
   367 by (Simp_tac 1);
 
       
   368 qed "smap_empty";
 
       
   369 
       
   370 Goal "x~=\\<bottom> ==> smap\\<cdot>f\\<cdot>(x&&xs) = (f\\<cdot>x)&&(smap\\<cdot>f\\<cdot>xs)";
 
       
   371 by (rtac trans 1);
 
       
   372 by  (stac smap_unfold 1);
 
       
   373 by  (Asm_simp_tac 1);
 
       
   374 by (rtac refl 1);
 
       
   375 qed "smap_scons";
 
       
   376 
       
   377 Addsimps [smap_empty, smap_scons];
 
       
   378 
       
   379 (* ------------------------------------------------------------------------- *)
 
       
   380 
       
   381 section "slen";
 
       
   382 
       
   383 Goalw [slen_def, stream.finite_def] "#\\<bottom> = 0";
 
       
   384 by (Simp_tac 1);
 
       
   385 by (stac Least_equality 1);
 
       
   386 by    Auto_tac;
 
       
   387 by (simp_tac(simpset() addsimps [Fin_0]) 1);
 
       
   388 qed "slen_empty";
 
       
   389 
       
   390 Goalw [slen_def] "x ~= \\<bottom> ==> #(x&&xs) = iSuc (#xs)";
 
       
   391 by (res_inst_tac [("Q1","stream_finite (x && xs)")] (split_if RS iffD2) 1);
 
       
   392 by Safe_tac;
 
       
   393 by (rtac (split_if RS iffD2) 2);
 
       
   394 by  Safe_tac;
 
       
   395 by   (fast_tac (claset() addIs [stream_finite_lemma1]) 2);
 
       
   396 by  (rtac (iSuc_Infty RS sym) 2);
 
       
   397 by (rtac (split_if RS iffD2) 1);
 
       
   398 by (Simp_tac 1);
 
       
   399 by Safe_tac;
 
       
   400 by  (eatac stream_finite_lemma2 1 2);
 
       
   401 by (rewtac stream.finite_def);
 
       
   402 by (Clarify_tac 1);
 
       
   403 by (eatac Least_Suc2 1 1);
 
       
   404 by  (rtac not_sym 1);
 
       
   405 by  Auto_tac;
 
       
   406 qed "slen_scons"; 
       
   407 
       
   408 Addsimps [slen_empty, slen_scons];
 
       
   409 
       
   410 Goal "#x < Fin 1 = (x = UU)";
 
       
   411 by (stream_case_tac "x" 1);
 
       
   412 by (auto_tac (claset(), simpset() delsimps [iSuc_Fin] addsimps
 
       
   413  [Fin_0, iSuc_Fin RS sym,i0_iless_iSuc, iSuc_mono]));
 
       
   414 qed "slen_less_1_eq";
 
       
   415 
       
   416 Goal "(#x = 0) = (x = \\<bottom>)";
 
       
   417 by Auto_tac;
 
       
   418 by (stream_case_tac "x" 1);
 
       
   419 by (rotate_tac ~1 2);
 
       
   420 by Auto_tac;
 
       
   421 qed "slen_empty_eq";
 
       
   422 
       
   423 Goal "Fin (Suc n) < #x = (? a y. x = a && y &  a ~= \\<bottom> &  Fin n < #y)";
 
       
   424 by (stream_case_tac "x" 1);
 
       
   425 by (auto_tac (claset(), simpset() delsimps [iSuc_Fin] addsimps
 
       
   426                 [iSuc_Fin RS sym, iSuc_mono]));
 
       
   427 by  (dtac sym 1);
 
       
   428 by  (rotate_tac 2 2);
 
       
   429 by  Auto_tac;
 
       
   430 qed "slen_scons_eq";
 
       
   431 
       
   432 
       
   433 Goal "#x = iSuc n --> (? a y. x = a&&y &  a ~= \\<bottom> &  #y = n)";
 
       
   434 by (stream_case_tac "x" 1);
 
       
   435 by Auto_tac;
 
       
   436 qed_spec_mp "slen_iSuc";
 
       
   437 
       
   438 
       
   439 Goal 
       
   440 "#x < Fin (Suc (Suc n)) = (!a y. x ~= a && y |  a = \\<bottom> |  #y < Fin (Suc n))";
 
       
   441 by (stac (iSuc_Fin RS sym) 1);
 
       
   442 by (stac (iSuc_Fin RS sym) 1);
 
       
   443 by (safe_tac HOL_cs);
 
       
   444 by  (rotate_tac ~1 1);
 
       
   445 by  (asm_full_simp_tac (HOL_ss addsimps [slen_scons, iSuc_mono]) 1);
 
       
   446 by  (Asm_full_simp_tac 1);
 
       
   447 by (stream_case_tac "x" 1);
 
       
   448 by ( simp_tac (HOL_ss addsimps [slen_empty, i0_iless_iSuc]) 1);
 
       
   449 by (asm_simp_tac (HOL_ss addsimps [slen_scons, iSuc_mono]) 1);
 
       
   450 by (etac allE 1);
 
       
   451 by (etac allE 1);
 
       
   452 by (safe_tac HOL_cs);
 
       
   453 by (  contr_tac 2);
 
       
   454 by ( fast_tac HOL_cs 1);
 
       
   455 by (Asm_full_simp_tac 1);
 
       
   456 qed "slen_scons_eq_rev";
 
       
   457 
       
   458 Goal "!x. Fin n < #x = (stream_take n\\<cdot>x ~= x)";
 
       
   459 by (nat_ind_tac "n" 1);
 
       
   460 by  (simp_tac(simpset() addsimps [slen_empty_eq, Fin_0]) 1);
 
       
   461 by  (Fast_tac 1);
 
       
   462 by (rtac allI 1);
 
       
   463 by (asm_simp_tac (simpset() addsimps [slen_scons_eq]) 1);
 
       
   464 by (etac thin_rl 1);
 
       
   465 by (safe_tac HOL_cs);
 
       
   466 by  (Asm_full_simp_tac 1);
 
       
   467 by (stream_case_tac "x" 1);
 
       
   468 by (rotate_tac ~1 2);
 
       
   469 by Auto_tac;
 
       
   470 qed_spec_mp "slen_take_eq";
 
       
   471 
       
   472 Goalw [ile_def] "#x <= Fin n = (stream_take n\\<cdot>x = x)";
 
       
   473 by (simp_tac (simpset() addsimps [slen_take_eq]) 1);
 
       
   474 qed "slen_take_eq_rev";
 
       
   475 
       
   476 Goal "#x = Fin n ==> stream_take n\\<cdot>x = x";
 
       
   477 by (asm_simp_tac (simpset() addsimps [slen_take_eq_rev RS sym]) 1);
 
       
   478 qed "slen_take_lemma1";
 
       
   479 
       
   480 Goal "!x. ~stream_finite x --> #(stream_take i\\<cdot>x) = Fin i";
 
       
   481 by (nat_ind_tac "i" 1);
 
       
   482 by  (simp_tac(simpset() addsimps [Fin_0]) 1);
 
       
   483 by (rtac allI 1);
 
       
   484 by (stream_case_tac "x" 1);
 
       
   485 by  (auto_tac (claset()addSIs [stream_finite_lemma1], simpset() delsimps [iSuc_Fin] addsimps [iSuc_Fin RS sym]));
 
       
   486 by (force_tac (claset(), simpset() addsimps [stream.finite_def]) 1);
 
       
   487 qed_spec_mp "slen_take_lemma2";
 
       
   488 
       
   489 Goal "stream_finite x = (#x ~= Infty)";
 
       
   490 by (rtac iffI 1);
 
       
   491 by  (etac stream_finite_ind 1);
 
       
   492 by   (Simp_tac 1);
 
       
   493 by  (etac (slen_scons RS ssubst) 1);
 
       
   494 by  (stac (iSuc_Infty RS sym) 1);
 
       
   495 by  (etac contrapos_nn 1);
 
       
   496 by  (etac (iSuc_inject RS iffD1) 1);
 
       
   497 by (case_tac "#x" 1);
 
       
   498 by (auto_tac (claset()addSDs [slen_take_lemma1],
 
       
   499         simpset() addsimps [stream.finite_def]));
 
       
   500 qed "slen_infinite";
 
       
   501 
       
   502 Goal "s << t ==> #s <= #t";
 
       
   503 by (case_tac "stream_finite t" 1);
 
       
   504 by  (EVERY'[dtac (slen_infinite RS subst), dtac notnotD] 2);
 
       
   505 by  (Asm_simp_tac 2);
 
       
   506 by (etac rev_mp 1);
 
       
   507 by (res_inst_tac [("x","s")] allE 1);
 
       
   508 by  (atac 2);
 
       
   509 by (etac (stream_finite_ind) 1);
 
       
   510 by  (Simp_tac 1);
 
       
   511 by (rtac allI 1);
 
       
   512 by (stream_case_tac "x" 1);
 
       
   513 by  (asm_simp_tac (HOL_ss addsimps [slen_empty, i0_lb]) 1);
 
       
   514 by (asm_simp_tac (HOL_ss addsimps [slen_scons]) 1);
 
       
   515 by (fast_tac(claset() addSIs [iSuc_ile_mono RS iffD2] addSDs stream.inverts) 1);
 
       
   516 qed "slen_mono";
 
       
   517 
       
   518 Goal "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> \
 
       
   519 \ stream_take n\\<cdot>x = stream_take n\\<cdot>y";
 
       
   520 by (nat_ind_tac "n" 1);
 
       
   521 by ( simp_tac(simpset() addsimps [slen_empty_eq]) 1);
 
       
   522 by (strip_tac 1);
 
       
   523 by (stream_case_tac "x" 1);
 
       
   524 by  (asm_full_simp_tac (HOL_ss addsimps [slen_empty, 
       
   525               iSuc_Fin RS sym, not_iSuc_ilei0]) 1);
 
       
   526 by (fatac stream_prefix 1 1);
 
       
   527 by (safe_tac (claset() addSDs [stream_flat_prefix]));
 
       
   528 by (Simp_tac 1);
 
       
   529 by (rtac cfun_arg_cong 1);
 
       
   530 by (rotate_tac 3 1);
 
       
   531 by (asm_full_simp_tac (simpset() delsimps [iSuc_Fin] addsimps 
       
   532         [iSuc_Fin RS sym, iSuc_ile_mono]) 1);
 
       
   533 qed_spec_mp "slen_take_lemma3";
 
       
   534 
       
   535 Goal "stream_finite t ==> \
 
       
   536 \!s. #(s::'a::flat stream) = #t &  s << t --> s = t";
 
       
   537 by (etac stream_finite_ind 1);
 
       
   538 by  (fast_tac (claset() addDs [eq_UU_iff RS iffD2]) 1);
 
       
   539 by (Safe_tac);
 
       
   540 by (stream_case_tac "sa" 1);
 
       
   541 by  (dtac sym 1);
 
       
   542 by  (Asm_full_simp_tac 1);
 
       
   543 by (safe_tac (claset() addSDs [stream_flat_prefix]));
 
       
   544 by (rtac cfun_arg_cong 1);
 
       
   545 by (etac allE 1);
 
       
   546 by (etac mp 1);
 
       
   547 by (Asm_full_simp_tac 1);
 
       
   548 qed "slen_strict_mono_lemma";
 
       
   549 
       
   550 Goal "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t";
 
       
   551 by (rtac ilessI1 1);
 
       
   552 by  (etac slen_mono 1);
 
       
   553 by (dtac slen_strict_mono_lemma 1);
 
       
   554 by (Fast_tac 1);
 
       
   555 qed "slen_strict_mono";
 
       
   556 
       
   557 Goal "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i rt x)";
 
       
   558 by (nat_ind_tac "i" 1);
 
       
   559 by  (Simp_tac 1);
 
       
   560 by (strip_tac 1);
 
       
   561 by (stream_case_tac "x" 1);
 
       
   562 by  (asm_full_simp_tac (simpset() delsimps [iSuc_Fin] 
       
   563              addsimps [iSuc_Fin RS sym]) 1);
 
       
   564 by (stac iterate_Suc2 1);
 
       
   565 by (rotate_tac 2 1);
 
       
   566 by (asm_full_simp_tac  (simpset() delsimps [iSuc_Fin] 
       
   567     addsimps [iSuc_Fin RS sym, iSuc_ile_mono]) 1);
 
       
   568 qed_spec_mp "slen_rt_mult";
 
       
   569 
       
   570 
       
   571 (* ------------------------------------------------------------------------- *)
 
       
   572 
       
   573 section "sfilter";
 
       
   574 
       
   575 bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def 
       
   576 	"sfilter = (\\<Lambda>p s. case s of x && xs => \
 
       
   577 \  If p\\<cdot>x then x && sfilter\\<cdot>p\\<cdot>xs else sfilter\\<cdot>p\\<cdot>xs fi)");
 
       
   578 
       
   579 Goal "sfilter\\<cdot>\\<bottom> = \\<bottom>";
 
       
   580 by (rtac ext_cfun 1);
 
       
   581 by (stac sfilter_unfold 1);
 
       
   582 by (stream_case_tac "x" 1);
 
       
   583 by  Auto_tac;
 
       
   584 qed "strict_sfilter";
 
       
   585 
       
   586 Goal "sfilter\\<cdot>f\\<cdot>\\<bottom> = \\<bottom>";
 
       
   587 by (stac sfilter_unfold 1);
 
       
   588 by (Simp_tac 1);
 
       
   589 qed "sfilter_empty";
 
       
   590 
       
   591 Goal "x ~= \\<bottom> ==> sfilter\\<cdot>f\\<cdot>(x && xs) = \
 
       
   592 \ If f\\<cdot>x then x && sfilter\\<cdot>f\\<cdot>xs else sfilter\\<cdot>f\\<cdot>xs fi";
 
       
   593 by (rtac trans 1);
 
       
   594 by (stac sfilter_unfold 1);
 
       
   595 by (Asm_simp_tac 1);
 
       
   596 by (rtac refl 1);
 
       
   597 qed "sfilter_scons";
 
       
   598
isabelle