integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
authoroheimb
Tue Sep 07 16:02:42 2004 +0200 (2004-09-07)
changeset 151889d57263faf9e
parent 15187 8b74a39dba89
child 15189 9cfbc392918c
integrated Streams with ex/Stream.*; added FOCUS/Fstreams.thy
src/HOLCF/FOCUS/Buffer.ML
src/HOLCF/FOCUS/Buffer_adm.ML
src/HOLCF/FOCUS/FOCUS.ML
src/HOLCF/FOCUS/Fstream.ML
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/FOCUS/Fstreams.thy
src/HOLCF/FOCUS/ROOT.ML
src/HOLCF/FOCUS/Stream_adm.ML
src/HOLCF/IsaMakefile
src/HOLCF/ROOT.ML
src/HOLCF/Streams.thy
src/HOLCF/ex/Dagstuhl.ML
src/HOLCF/ex/Stream.ML
src/HOLCF/ex/Stream.thy
     1.1 --- a/src/HOLCF/FOCUS/Buffer.ML	Tue Sep 07 15:59:16 2004 +0200
     1.2 +++ b/src/HOLCF/FOCUS/Buffer.ML	Tue Sep 07 16:02:42 2004 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4  by (Fast_tac 1);
     1.5  qed_spec_mp "BufAC_Asm_cong_lemma";
     1.6  Goal "\\<lbrakk>f \\<in> BufEq; ff \\<in> BufEq; s \\<in> BufAC_Asm\\<rbrakk> \\<Longrightarrow> f\\<cdot>s = ff\\<cdot>s";
     1.7 -by (resolve_tac stream.take_lemmas 1);
     1.8 +by (resolve_tac (thms "stream.take_lemmas") 1);
     1.9  by (eatac BufAC_Asm_cong_lemma 2 1);
    1.10  qed "BufAC_Asm_cong";
    1.11  
     2.1 --- a/src/HOLCF/FOCUS/Buffer_adm.ML	Tue Sep 07 15:59:16 2004 +0200
     2.2 +++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Tue Sep 07 16:02:42 2004 +0200
     2.3 @@ -30,7 +30,7 @@
     2.4  	subgoal_tac "!d x. (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> (? y. t = d\\<leadsto>y & (x,y):C)) = \
     2.5  		   \ (s = Md d\\<leadsto>\\<bullet>\\<leadsto>x --> ft\\<cdot>t = Def d & (x,rt\\<cdot>t):C)"  1,
     2.6  	Asm_simp_tac 1,
     2.7 -	auto_tac (claset() addIs [surjectiv_scons RS sym], simpset())]);
     2.8 +	auto_tac (claset() addIs [thm "surjectiv_scons" RS sym], simpset())]);
     2.9  
    2.10  val cont_BufAC_Cmt_F = prove_goal thy "down_cont BufAC_Cmt_F" (K [
    2.11  	auto_tac (claset(),simpset() addsimps [down_cont_def,BufAC_Cmt_F_def3])]);
    2.12 @@ -56,7 +56,7 @@
    2.13  b y res_inst_tac [("x","Suc (Suc 0)")] exI 1;
    2.14  b y rtac conjI 1;
    2.15  b y  strip_tac 2;
    2.16 -b y  dtac slen_mono 2;
    2.17 +b y  dtac (thm "slen_mono") 2;
    2.18  b y  datac (thm "ile_trans") 1 2;
    2.19  b y ALLGOALS Force_tac;
    2.20  qed "BufAC_Asm_F_stream_antiP";
     3.1 --- a/src/HOLCF/FOCUS/FOCUS.ML	Tue Sep 07 15:59:16 2004 +0200
     3.2 +++ b/src/HOLCF/FOCUS/FOCUS.ML	Tue Sep 07 16:02:42 2004 +0200
     3.3 @@ -10,10 +10,10 @@
     3.4  AddSIs [ex_eqI, ex2_eqI];
     3.5  Addsimps[eq_UU_symf];
     3.6  Goal "(#x ~= 0) = (? a y. x = a~> y)";
     3.7 -by (simp_tac (simpset() addsimps [slen_empty_eq, fstream_exhaust_eq]) 1);
     3.8 +by (simp_tac (simpset() addsimps [thm "slen_empty_eq", fstream_exhaust_eq]) 1);
     3.9  qed "fstream_exhaust_slen_eq";
    3.10  
    3.11 -Addsimps[slen_less_1_eq, fstream_exhaust_slen_eq,
    3.12 -		   slen_fscons_eq, slen_fscons_less_eq];
    3.13 +Addsimps[thm "slen_less_1_eq", fstream_exhaust_slen_eq,
    3.14 +		   thm "slen_fscons_eq", thm "slen_fscons_less_eq"];
    3.15  Addsimps[thm "Suc_ile_eq"];
    3.16  AddEs  [strictI];
     4.1 --- a/src/HOLCF/FOCUS/Fstream.ML	Tue Sep 07 15:59:16 2004 +0200
     4.2 +++ b/src/HOLCF/FOCUS/Fstream.ML	Tue Sep 07 16:02:42 2004 +0200
     4.3 @@ -3,6 +3,8 @@
     4.4      Author: 	David von Oheimb, TU Muenchen
     4.5  *)
     4.6  
     4.7 +Addsimps[eq_UU_iff RS sym];
     4.8 +
     4.9  Goal "a = Def d \\<Longrightarrow> a\\<sqsubseteq>b \\<Longrightarrow> b = Def d";
    4.10  by (rtac (flat_eq RS iffD1 RS sym) 1);
    4.11  by (rtac Def_not_UU 1);
    4.12 @@ -19,7 +21,7 @@
    4.13  
    4.14  qed_goal "fstream_exhaust" thy "x = UU |  (? a y. x = a~> y)" (fn _ => [
    4.15  	simp_tac (simpset() addsimps [fscons_def2]) 1,
    4.16 -	cut_facts_tac [stream.exhaust] 1,
    4.17 +	cut_facts_tac [thm "stream.exhaust"] 1,
    4.18  	fast_tac (claset() addDs [not_Undef_is_Def RS iffD1]) 1]);
    4.19  
    4.20  qed_goal "fstream_cases" thy "[| x = UU ==> P; !!a y. x = a~> y ==> P |] ==> P" 
    4.21 @@ -34,7 +36,7 @@
    4.22  			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
    4.23  
    4.24  qed_goal "fstream_exhaust_eq" thy "(x ~= UU) = (? a y. x = a~> y)" (fn _ => [
    4.25 -	simp_tac(simpset() addsimps [fscons_def2,stream_exhaust_eq]) 1,
    4.26 +	simp_tac(simpset() addsimps [fscons_def2,thm "stream_exhaust_eq"]) 1,
    4.27  	fast_tac (claset() addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
    4.28  
    4.29  
    4.30 @@ -52,17 +54,17 @@
    4.31  
    4.32  qed_goal "fstream_prefix" thy "a~> s << t ==> ? tt. t = a~> tt &  s << tt" (fn prems =>[
    4.33  	cut_facts_tac prems 1,
    4.34 -	stream_case_tac "t" 1,
    4.35 +	res_inst_tac [("x","t")] (thm "stream.casedist") 1,
    4.36  	 cut_facts_tac [fscons_not_empty] 1,
    4.37  	 fast_tac (HOL_cs addDs [eq_UU_iff RS iffD2]) 1,
    4.38  	asm_full_simp_tac (HOL_ss addsimps [fscons_def2]) 1,
    4.39 -	dtac stream_flat_prefix 1,
    4.40 +	dtac (thm "stream_flat_prefix") 1,
    4.41  	rtac Def_not_UU 1,
    4.42  	fast_tac HOL_cs 1]);
    4.43  
    4.44  qed_goal "fstream_prefix'" thy
    4.45  	"x << a~> z = (x = <> |  (? y. x = a~> y &  y << z))" (fn _ => [
    4.46 -	simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS stream_prefix'])1,
    4.47 +	simp_tac(HOL_ss addsimps [fscons_def2, Def_not_UU RS thm "stream_prefix'"])1,
    4.48  	Step_tac 1,
    4.49  	 ALLGOALS(etac swap),
    4.50  	 fast_tac (HOL_cs addIs [refl_less] addEs [DefE]) 2,
    4.51 @@ -77,12 +79,12 @@
    4.52  
    4.53  section "ft & rt";
    4.54  
    4.55 -bind_thm("ft_empty",hd stream.sel_rews);
    4.56 +bind_thm("ft_empty",hd (thms "stream.sel_rews"));
    4.57  qed_goalw "ft_fscons" thy [fscons_def] "ft\\<cdot>(m~> s) = Def m" (fn _ => [
    4.58  	(Simp_tac 1)]);
    4.59  Addsimps[ft_fscons];
    4.60  
    4.61 -bind_thm("rt_empty",hd (tl stream.sel_rews));
    4.62 +bind_thm("rt_empty",hd (tl (thms "stream.sel_rews")));
    4.63  qed_goalw "rt_fscons" thy [fscons_def] "rt\\<cdot>(m~> s) = s" (fn _ => [
    4.64  	(Simp_tac 1)]);
    4.65  Addsimps[rt_fscons];
    4.66 @@ -92,7 +94,7 @@
    4.67  	Safe_tac,
    4.68  	 etac subst 1,
    4.69  	 rtac exI 1,
    4.70 -	 rtac (surjectiv_scons RS sym) 1,
    4.71 +	 rtac (thm "surjectiv_scons" RS sym) 1,
    4.72  	Simp_tac 1]);
    4.73  Addsimps[ft_eq];
    4.74  
    4.75 @@ -125,12 +127,12 @@
    4.76  
    4.77  qed_goal "slen_fscons_eq" thy 
    4.78  	"(Fin (Suc n) < #x) = (? a y. x = a~> y & Fin n < #y)" (fn _ => [
    4.79 -	simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq]) 1,
    4.80 +	simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq"]) 1,
    4.81  	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] addEs [DefE]) 1]);
    4.82  
    4.83  qed_goal "slen_fscons_eq_rev" thy 
    4.84  	"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" (K [
    4.85 -	simp_tac (HOL_ss addsimps [fscons_def2, slen_scons_eq_rev]) 1,
    4.86 +	simp_tac (HOL_ss addsimps [fscons_def2, thm "slen_scons_eq_rev"]) 1,
    4.87  	step_tac (HOL_cs addSEs [DefE]) 1,
    4.88  	step_tac (HOL_cs addSEs [DefE]) 1,
    4.89  	step_tac (HOL_cs addSEs [DefE]) 1,
    4.90 @@ -153,7 +155,7 @@
    4.91  qed_goal "fstream_ind" thy 
    4.92  	"[| adm P; P <>; !!a s. P s ==> P (a~> s) |] ==> P x" (fn prems => [
    4.93  	cut_facts_tac prems 1,
    4.94 -	etac stream.ind 1,
    4.95 +	etac (thm "stream.ind") 1,
    4.96  	 atac 1,
    4.97  	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] 
    4.98  			 addEs (tl (tl prems) RL [fscons_def2 RS subst])) 1]);
    4.99 @@ -161,7 +163,7 @@
   4.100  qed_goal "fstream_ind2" thy 
   4.101    "[| adm P; P UU; !!a. P (a~> UU); !!a b s. P s ==> P (a~> b~> s) |] ==> P x" (fn prems => [
   4.102  	cut_facts_tac prems 1,
   4.103 -	etac stream_ind2 1,
   4.104 +	etac (thm "stream_ind2") 1,
   4.105  	  atac 1,
   4.106  	fast_tac (HOL_cs addDs [not_Undef_is_Def RS iffD1] 
   4.107  			 addIs ([hd(tl(tl prems))]RL[fscons_def2 RS subst]))1,
   4.108 @@ -175,11 +177,11 @@
   4.109  section "fsfilter";
   4.110  
   4.111  qed_goalw "fsfilter_empty" thy [fsfilter_def] "A(C)UU = UU" (fn _ => [
   4.112 -	rtac sfilter_empty 1]);
   4.113 +	rtac (thm "sfilter_empty") 1]);
   4.114  
   4.115  qed_goalw "fsfilter_fscons" thy [fsfilter_def] 
   4.116  	"A(C)x~> xs = (if x:A then x~> (A(C)xs) else A(C)xs)" (fn _ => [
   4.117 -	simp_tac (simpset() addsimps [fscons_def2,sfilter_scons,If_and_if]) 1]);
   4.118 +	simp_tac (simpset() addsimps [fscons_def2,thm "sfilter_scons",If_and_if]) 1]);
   4.119  
   4.120  qed_goal "fsfilter_emptys" thy "{}(C)x = UU" (fn _ => [
   4.121  	res_inst_tac [("x","x")] fstream_ind 1,
   4.122 @@ -189,7 +191,7 @@
   4.123  	asm_simp_tac (simpset()addsimps [fsfilter_fscons]) 1]);
   4.124  
   4.125  qed_goal "fsfilter_insert" thy "(insert a A)(C)a~> x = a~> ((insert a A)(C)x)" (fn _=> [
   4.126 -	simp_tac (simpset() addsimps [fsfilter_fscons]) 1]);
   4.127 +	simp_tac (simpset() addsimps [thm "fsfilter_fscons"]) 1]);
   4.128  
   4.129  qed_goal "fsfilter_single_in" thy "{a}(C)a~> x = a~> ({a}(C)x)" (fn _=> [
   4.130  	rtac fsfilter_insert 1]);
     5.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Tue Sep 07 15:59:16 2004 +0200
     5.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Tue Sep 07 16:02:42 2004 +0200
     5.3 @@ -3,11 +3,12 @@
     5.4      Author: 	David von Oheimb, TU Muenchen
     5.5  
     5.6  FOCUS streams (with lifted elements)
     5.7 +###TODO: integrate Fstreams.thy
     5.8  *)
     5.9  
    5.10  (* FOCUS flat streams *)
    5.11  
    5.12 -Fstream = Streams + 
    5.13 +Fstream = Stream + 
    5.14  
    5.15  default type
    5.16  
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOLCF/FOCUS/Fstreams.thy	Tue Sep 07 16:02:42 2004 +0200
     6.3 @@ -0,0 +1,357 @@
     6.4 +(*  Title: 	HOLCF/FOCUS/Fstreams.thy
     6.5 +    ID:         $Id$
     6.6 +    Author: 	Borislav Gajanovic
     6.7 +
     6.8 +FOCUS flat streams (with lifted elements)
     6.9 +###TODO: integrate this with Fstream.*
    6.10 +*)
    6.11 +
    6.12 +theory Fstreams = Stream:
    6.13 +
    6.14 +defaultsort type
    6.15 +
    6.16 +types 'a fstream = "('a lift) stream"
    6.17 +
    6.18 +consts
    6.19 +
    6.20 +  fsingleton    :: "'a => 'a fstream"  ("<_>" [1000] 999)
    6.21 +  fsfilter      :: "'a set \<Rightarrow> 'a fstream \<rightarrow> 'a fstream"
    6.22 +  fsmap		:: "('a => 'b) => 'a fstream -> 'b fstream"
    6.23 +
    6.24 +  jth           :: "nat => 'a fstream => 'a"
    6.25 +
    6.26 +  first         :: "'a fstream => 'a"
    6.27 +  last          :: "'a fstream => 'a"
    6.28 +
    6.29 +
    6.30 +syntax
    6.31 +
    6.32 +  "@emptystream":: "'a fstream" 			("<>")
    6.33 +  "@fsfilter"	:: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream"	("(_'(C')_)" [64,63] 63)
    6.34 +
    6.35 +syntax (xsymbols)
    6.36 +
    6.37 +  "@fsfilter"	:: "'a set \<Rightarrow> 'a fstream \<Rightarrow> 'a fstream" ("(_\<copyright>_)"
    6.38 +								     [64,63] 63)
    6.39 +translations
    6.40 +
    6.41 +  "<>"    => "\<bottom>"
    6.42 +  "A(C)s" == "fsfilter A\<cdot>s"
    6.43 +
    6.44 +defs
    6.45 +
    6.46 +  fsingleton_def2:    "fsingleton  == %a. Def a && UU"
    6.47 +
    6.48 +  jth_def:            "jth == %n s. if Fin n < #s then THE a. i_th n s = Def a else arbitrary" 
    6.49 +
    6.50 +  first_def:          "first == %s. jth 0 s"
    6.51 +  last_def:           "last == %s. case #s of Fin n => (if n~=0 then jth (THE k. Suc k = n) s else arbitrary)
    6.52 +                              | Infty => arbitrary"
    6.53 +
    6.54 +  fsfilter_def:       "fsfilter A \<equiv> sfilter\<cdot>(flift2 (\<lambda>x. x\<in>A))"
    6.55 +  fsmap_def:   	      "fsmap f  == smap$(flift2 f)"
    6.56 +
    6.57 +
    6.58 +lemma ft_fsingleton[simp]: "ft$(<a>) = Def a"
    6.59 +by (simp add: fsingleton_def2)
    6.60 +
    6.61 +lemma slen_fsingleton[simp]: "#(<a>) = Fin 1"
    6.62 +by (simp add: fsingleton_def2 inat_defs)
    6.63 +
    6.64 +lemma slen_fstreams[simp]: "#(<a> ooo s) = iSuc (#s)"
    6.65 +by (simp add: fsingleton_def2)
    6.66 +
    6.67 +lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)"
    6.68 +apply (case_tac "#s", auto)
    6.69 +apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto)
    6.70 +by (simp add: sconc_def)
    6.71 +
    6.72 +lemma j_th_0_fsingleton[simp]:"jth 0 (<a>) = a"
    6.73 +apply (simp add: fsingleton_def2 jth_def)
    6.74 +by (simp add: i_th_def Fin_0)
    6.75 +
    6.76 +lemma jth_0[simp]: "jth 0 (<a> ooo s) = a"  
    6.77 +apply (simp add: fsingleton_def2 jth_def)
    6.78 +by (simp add: i_th_def Fin_0)
    6.79 +
    6.80 +lemma first_sconc[simp]: "first (<a> ooo s) = a"
    6.81 +by (simp add: first_def)
    6.82 +
    6.83 +lemma first_fsingleton[simp]: "first (<a>) = a"
    6.84 +by (simp add: first_def)
    6.85 +
    6.86 +lemma jth_n[simp]: "Fin n = #s ==> jth n (s ooo <a>) = a"
    6.87 +apply (simp add: jth_def, auto)
    6.88 +apply (simp add: i_th_def rt_sconc1)
    6.89 +by (simp add: inat_defs split: inat_splits)
    6.90 +
    6.91 +lemma last_sconc[simp]: "Fin n = #s ==> last (s ooo <a>) = a"
    6.92 +apply (simp add: last_def)
    6.93 +apply (simp add: inat_defs split:inat_splits)
    6.94 +by (drule sym, auto)
    6.95 +
    6.96 +lemma last_fsingleton[simp]: "last (<a>) = a"
    6.97 +by (simp add: last_def)
    6.98 +
    6.99 +lemma first_UU[simp]: "first UU = arbitrary"
   6.100 +by (simp add: first_def jth_def)
   6.101 +
   6.102 +lemma last_UU[simp]:"last UU = arbitrary"
   6.103 +by (simp add: last_def jth_def inat_defs)
   6.104 +
   6.105 +lemma last_infinite[simp]:"#s = Infty ==> last s = arbitrary"
   6.106 +by (simp add: last_def)
   6.107 +
   6.108 +lemma jth_slen_lemma1:"n <= k & Fin n = #s ==> jth k s = arbitrary"
   6.109 +by (simp add: jth_def inat_defs split:inat_splits, auto)
   6.110 +
   6.111 +lemma jth_UU[simp]:"jth n UU = arbitrary" 
   6.112 +by (simp add: jth_def)
   6.113 +
   6.114 +lemma ext_last:"[|s ~= UU; Fin (Suc n) = #s|] ==> (stream_take n$s) ooo <(last s)> = s" 
   6.115 +apply (simp add: last_def)
   6.116 +apply (case_tac "#s", auto)
   6.117 +apply (simp add: fsingleton_def2)
   6.118 +apply (subgoal_tac "Def (jth n s) = i_th n s")
   6.119 +apply (auto simp add: i_th_last)
   6.120 +apply (drule slen_take_lemma1, auto)
   6.121 +apply (simp add: jth_def)
   6.122 +apply (case_tac "i_th n s = UU")
   6.123 +apply auto
   6.124 +apply (simp add: i_th_def)
   6.125 +apply (case_tac "i_rt n s = UU", auto)
   6.126 +apply (drule i_rt_slen [THEN iffD1])
   6.127 +apply (drule slen_take_eq_rev [rule_format, THEN iffD2],auto)
   6.128 +by (drule not_Undef_is_Def [THEN iffD1], auto)
   6.129 +
   6.130 +
   6.131 +lemma fsingleton_lemma1[simp]: "(<a> = <b>) = (a=b)"
   6.132 +by (simp add: fsingleton_def2)
   6.133 +
   6.134 +lemma fsingleton_lemma2[simp]: "<a> ~= <>"
   6.135 +by (simp add: fsingleton_def2)
   6.136 +
   6.137 +lemma fsingleton_sconc:"<a> ooo s = Def a && s"
   6.138 +by (simp add: fsingleton_def2)
   6.139 +
   6.140 +lemma fstreams_ind: 
   6.141 +  "[| adm P; P <>; !!a s. P s ==> P (<a> ooo s) |] ==> P x"
   6.142 +apply (simp add: fsingleton_def2)
   6.143 +apply (rule stream.ind, auto)
   6.144 +by (drule not_Undef_is_Def [THEN iffD1], auto)
   6.145 +
   6.146 +lemma fstreams_ind2:
   6.147 +  "[| adm P; P <>; !!a. P (<a>); !!a b s. P s ==> P (<a> ooo <b> ooo s) |] ==> P x"
   6.148 +apply (simp add: fsingleton_def2)
   6.149 +apply (rule stream_ind2, auto)
   6.150 +by (drule not_Undef_is_Def [THEN iffD1], auto)+
   6.151 +
   6.152 +lemma fstreams_take_Suc[simp]: "stream_take (Suc n)$(<a> ooo s) = <a> ooo stream_take n$s"
   6.153 +by (simp add: fsingleton_def2)
   6.154 +
   6.155 +lemma fstreams_not_empty[simp]: "<a> ooo s ~= <>"
   6.156 +by (simp add: fsingleton_def2)
   6.157 +
   6.158 +lemma fstreams_not_empty2[simp]: "s ooo <a> ~= <>"
   6.159 +by (case_tac "s=UU", auto)
   6.160 +
   6.161 +lemma fstreams_exhaust: "x = UU | (EX a s. x = <a> ooo s)"
   6.162 +apply (simp add: fsingleton_def2, auto)
   6.163 +apply (erule contrapos_pp, auto)
   6.164 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
   6.165 +by (drule not_Undef_is_Def [THEN iffD1], auto)
   6.166 +
   6.167 +lemma fstreams_cases: "[| x = UU ==> P; !!a y. x = <a> ooo y ==> P |] ==> P"
   6.168 +by (insert fstreams_exhaust [of x], auto)
   6.169 +
   6.170 +lemma fstreams_exhaust_eq: "(x ~= UU) = (? a y. x = <a> ooo y)"
   6.171 +apply (simp add: fsingleton_def2, auto)
   6.172 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
   6.173 +by (drule not_Undef_is_Def [THEN iffD1], auto)
   6.174 +
   6.175 +lemma fstreams_inject: "(<a> ooo s = <b> ooo t) = (a=b & s=t)"
   6.176 +by (simp add: fsingleton_def2)
   6.177 +
   6.178 +lemma fstreams_prefix: "<a> ooo s << t ==> EX tt. t = <a> ooo tt &  s << tt"
   6.179 +apply (simp add: fsingleton_def2)
   6.180 +apply (insert stream_prefix [of "Def a" s t], auto)
   6.181 +by (drule stream.inverts, auto)
   6.182 +
   6.183 +lemma fstreams_prefix': "x << <a> ooo z = (x = <> |  (EX y. x = <a> ooo y &  y << z))"
   6.184 +apply (auto, case_tac "x=UU", auto)
   6.185 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
   6.186 +apply (simp add: fsingleton_def2, auto)
   6.187 +apply (drule stream.inverts, auto)
   6.188 +apply (drule ax_flat [rule_format], simp)
   6.189 +apply (drule stream.inverts, auto)
   6.190 +by (erule sconc_mono)
   6.191 +
   6.192 +lemma ft_fstreams[simp]: "ft$(<a> ooo s) = Def a"
   6.193 +by (simp add: fsingleton_def2)
   6.194 +
   6.195 +lemma rt_fstreams[simp]: "rt$(<a> ooo s) = s"
   6.196 +by (simp add: fsingleton_def2)
   6.197 +
   6.198 +lemma ft_eq[simp]: "(ft$s = Def a) = (EX t. s = <a> ooo t)"
   6.199 +apply (rule stream.casedist [of s],auto)
   6.200 +by (drule sym, auto simp add: fsingleton_def2)
   6.201 +
   6.202 +lemma surjective_fstreams: "(<d> ooo y = x) = (ft$x = Def d & rt$x = y)"
   6.203 +by auto
   6.204 +
   6.205 +lemma fstreams_mono: "<a> ooo b << <a> ooo c ==> b << c"
   6.206 +apply (simp add: fsingleton_def2)
   6.207 +by (drule stream.inverts, auto)
   6.208 +
   6.209 +lemma fsmap_UU[simp]: "fsmap f$UU = UU"
   6.210 +by (simp add: fsmap_def)
   6.211 +
   6.212 +lemma fsmap_fsingleton_sconc: "fsmap f$(<x> ooo xs) = <(f x)> ooo (fsmap f$xs)"
   6.213 +by (simp add: fsmap_def fsingleton_def2 flift2_def)
   6.214 +
   6.215 +lemma fsmap_fsingleton[simp]: "fsmap f$(<x>) = <(f x)>"
   6.216 +by (simp add: fsmap_def fsingleton_def2 flift2_def)
   6.217 +
   6.218 +
   6.219 +declare range_composition[simp del]
   6.220 +
   6.221 +
   6.222 +lemma fstreams_chain_lemma[rule_format]:
   6.223 +  "ALL s x y. stream_take n$(s::'a fstream) << x & x << y & y << s & x ~= y --> stream_take (Suc n)$s << y"
   6.224 +apply (induct_tac n, auto)
   6.225 +apply (case_tac "s=UU", auto)
   6.226 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
   6.227 +apply (case_tac "y=UU", auto)
   6.228 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
   6.229 +apply (drule stream.inverts, auto)
   6.230 +apply (simp add: less_lift_def, auto)
   6.231 +apply (rule monofun_cfun, auto)
   6.232 +apply (case_tac "s=UU", auto)
   6.233 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
   6.234 +apply (erule_tac x="ya" in allE)
   6.235 +apply (drule stream_prefix, auto)
   6.236 +apply (case_tac "y=UU",auto)
   6.237 +apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
   6.238 +apply (drule stream.inverts, auto)
   6.239 +apply (simp add: less_lift_def)
   6.240 +apply (drule stream.inverts, auto)+
   6.241 +apply (erule_tac x="tt" in allE)
   6.242 +apply (erule_tac x="yb" in allE, auto)
   6.243 +apply (simp add: less_lift_def)
   6.244 +by (rule monofun_cfun, auto)
   6.245 +
   6.246 +lemma fstreams_lub_lemma1: "[| chain Y; lub (range Y) = <a> ooo s |] ==> EX j t. Y j = <a> ooo t"
   6.247 +apply (subgoal_tac "lub(range Y) ~= UU")
   6.248 +apply (drule chain_UU_I_inverse2, auto)
   6.249 +apply (drule_tac x="i" in is_ub_thelub, auto)
   6.250 +by (drule fstreams_prefix' [THEN iffD1], auto)
   6.251 +
   6.252 +lemma fstreams_lub1: 
   6.253 + "[| chain Y; lub (range Y) = <a> ooo s |]
   6.254 +     ==> (EX j t. Y j = <a> ooo t) & (EX X. chain X & (ALL i. EX j. <a> ooo X i << Y j) & lub (range X) = s)"
   6.255 +apply (auto simp add: fstreams_lub_lemma1)
   6.256 +apply (rule_tac x="%n. stream_take n$s" in exI, auto)
   6.257 +apply (simp add: chain_stream_take)
   6.258 +apply (induct_tac i, auto)
   6.259 +apply (drule fstreams_lub_lemma1, auto)
   6.260 +apply (rule_tac x="j" in exI, auto)
   6.261 +apply (case_tac "max_in_chain j Y")
   6.262 +apply (frule lub_finch1 [THEN thelubI], auto)
   6.263 +apply (rule_tac x="j" in exI)
   6.264 +apply (erule subst) back back
   6.265 +apply (simp add: less_cprod_def sconc_mono)
   6.266 +apply (simp add: max_in_chain_def, auto)
   6.267 +apply (rule_tac x="ja" in exI)
   6.268 +apply (subgoal_tac "Y j << Y ja")
   6.269 +apply (drule fstreams_prefix, auto)+
   6.270 +apply (rule sconc_mono)
   6.271 +apply (rule fstreams_chain_lemma, auto)
   6.272 +apply (subgoal_tac "Y ja << (LUB i. (Y i))", clarsimp)
   6.273 +apply (drule fstreams_mono, simp)
   6.274 +apply (rule is_ub_thelub, simp)
   6.275 +apply (blast intro: chain_mono3)
   6.276 +by (rule stream_reach2)
   6.277 +
   6.278 +
   6.279 +lemma lub_Pair_not_UU_lemma: 
   6.280 +  "[| chain Y; lub (range Y) = ((a::'a::flat), b); a ~= UU; b ~= UU |] 
   6.281 +      ==> EX j c d. Y j = (c, d) & c ~= UU & d ~= UU"
   6.282 +apply (frule thelub_cprod, clarsimp)
   6.283 +apply (drule chain_UU_I_inverse2, clarsimp)
   6.284 +apply (case_tac "Y i", clarsimp)
   6.285 +apply (case_tac "max_in_chain i Y")
   6.286 +apply (drule maxinch_is_thelub, auto)
   6.287 +apply (rule_tac x="i" in exI, auto)
   6.288 +apply (simp add: max_in_chain_def, auto)
   6.289 +apply (subgoal_tac "Y i << Y j",auto)
   6.290 +apply (simp add: less_cprod_def, clarsimp)
   6.291 +apply (drule ax_flat [rule_format], auto)
   6.292 +apply (case_tac "snd (Y j) = UU",auto)
   6.293 +apply (case_tac "Y j", auto)
   6.294 +apply (rule_tac x="j" in exI)
   6.295 +apply (case_tac "Y j",auto)
   6.296 +by (drule chain_mono3, auto)
   6.297 +
   6.298 +lemma fstreams_lub_lemma2: 
   6.299 +  "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] ==> EX j t. Y j = (a, <m> ooo t)"
   6.300 +apply (frule lub_Pair_not_UU_lemma, auto)
   6.301 +apply (drule_tac x="j" in is_ub_thelub, auto)
   6.302 +apply (simp add: less_cprod_def, clarsimp)
   6.303 +apply (drule ax_flat [rule_format], clarsimp)
   6.304 +by (drule fstreams_prefix' [THEN iffD1], auto)
   6.305 +
   6.306 +lemma fstreams_lub2:
   6.307 +  "[| chain Y; lub (range Y) = (a, <m> ooo ms); (a::'a::flat) ~= UU |] 
   6.308 +      ==> (EX j t. Y j = (a, <m> ooo t)) & (EX X. chain X & (ALL i. EX j. (a, <m> ooo X i) << Y j) & lub (range X) = ms)"
   6.309 +apply (auto simp add: fstreams_lub_lemma2)
   6.310 +apply (rule_tac x="%n. stream_take n$ms" in exI, auto)
   6.311 +apply (simp add: chain_stream_take)
   6.312 +apply (induct_tac i, auto)
   6.313 +apply (drule fstreams_lub_lemma2, auto)
   6.314 +apply (rule_tac x="j" in exI, auto)
   6.315 +apply (simp add: less_cprod_def)
   6.316 +apply (case_tac "max_in_chain j Y")
   6.317 +apply (frule lub_finch1 [THEN thelubI], auto)
   6.318 +apply (rule_tac x="j" in exI)
   6.319 +apply (erule subst) back back
   6.320 +apply (simp add: less_cprod_def sconc_mono)
   6.321 +apply (simp add: max_in_chain_def, auto)
   6.322 +apply (rule_tac x="ja" in exI)
   6.323 +apply (subgoal_tac "Y j << Y ja")
   6.324 +apply (simp add: less_cprod_def, auto)
   6.325 +apply (drule trans_less)
   6.326 +apply (simp add: ax_flat, auto)
   6.327 +apply (drule fstreams_prefix, auto)+
   6.328 +apply (rule sconc_mono)
   6.329 +apply (subgoal_tac "tt ~= tta" "tta << ms")
   6.330 +apply (blast intro: fstreams_chain_lemma)
   6.331 +apply (frule lub_cprod [THEN thelubI], auto)
   6.332 +apply (subgoal_tac "snd (Y ja) << (LUB i. snd (Y i))", clarsimp)
   6.333 +apply (drule fstreams_mono, simp)
   6.334 +apply (rule is_ub_thelub chainI)
   6.335 +apply (simp add: chain_def less_cprod_def)
   6.336 +apply (subgoal_tac "fst (Y j) ~= fst (Y ja) | snd (Y j) ~= snd (Y ja)", simp)
   6.337 +apply (drule ax_flat[rule_format], simp)+
   6.338 +apply (drule prod_eqI, auto)
   6.339 +apply (simp add: chain_mono3)
   6.340 +by (rule stream_reach2)
   6.341 +
   6.342 +
   6.343 +lemma cpo_cont_lemma:
   6.344 +  "[| monofun (f::'a::cpo => 'b::cpo); (!Y. chain Y --> f (lub(range Y)) << (LUB i. f (Y i))) |] ==> cont f"
   6.345 +apply (rule monocontlub2cont, auto)
   6.346 +apply (simp add: contlub, auto)
   6.347 +apply (erule_tac x="Y" in allE, auto)
   6.348 +apply (simp add: po_eq_conv)
   6.349 +apply (frule cpo,auto)
   6.350 +apply (frule is_lubD1)
   6.351 +apply (frule ub2ub_monofun, auto)
   6.352 +apply (drule thelubI, auto)
   6.353 +apply (rule is_lub_thelub, auto)
   6.354 +by (erule ch2ch_monofun, simp)
   6.355 +
   6.356 +end
   6.357 +
   6.358 +
   6.359 +
   6.360 +
     7.1 --- a/src/HOLCF/FOCUS/ROOT.ML	Tue Sep 07 15:59:16 2004 +0200
     7.2 +++ b/src/HOLCF/FOCUS/ROOT.ML	Tue Sep 07 16:02:42 2004 +0200
     7.3 @@ -9,5 +9,6 @@
     7.4  val banner = "HOLCF/FOCUS";
     7.5  writeln banner;
     7.6  
     7.7 +use_thy "Fstreams";
     7.8  use_thy "FOCUS";
     7.9  use_thy "Buffer_adm";
     8.1 --- a/src/HOLCF/FOCUS/Stream_adm.ML	Tue Sep 07 15:59:16 2004 +0200
     8.2 +++ b/src/HOLCF/FOCUS/Stream_adm.ML	Tue Sep 07 16:02:42 2004 +0200
     8.3 @@ -24,12 +24,12 @@
     8.4  by ( dtac spec 1);
     8.5  by ( Safe_tac);
     8.6  by ( rtac exI 1);
     8.7 -by ( rtac slen_strict_mono 1);
     8.8 +by ( rtac (thm "slen_strict_mono") 1);
     8.9  by (   etac spec 1);
    8.10  by (  atac 1);
    8.11  by ( atac 1);
    8.12  by (dtac (not_ex RS iffD1) 1);
    8.13 -by (stac slen_infinite 1);
    8.14 +by (stac (thm "slen_infinite") 1);
    8.15  by (etac thin_rl 1);
    8.16  by (dtac spec 1);
    8.17  by (fold_goals_tac [thm "ile_def"]);
    8.18 @@ -67,16 +67,16 @@
    8.19  by (dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1);
    8.20  by (etac allE 1 THEN dtac mp 1 THEN rtac ile_lemma 1);
    8.21  by ( etac (thm "ile_trans") 1);
    8.22 -by ( etac slen_mono 1);
    8.23 +by ( etac (thm "slen_mono") 1);
    8.24  by (etac ssubst 1);
    8.25  by (safe_tac HOL_cs);
    8.26 -by ( eatac (ile_lemma RS slen_take_lemma3 RS subst) 2 1);
    8.27 +by ( eatac (ile_lemma RS thm "slen_take_lemma3" RS subst) 2 1);
    8.28  by (etac allE 1);
    8.29  by (etac allE 1);
    8.30  by (dtac mp 1);
    8.31 -by ( etac slen_rt_mult 1);
    8.32 +by ( etac (thm "slen_rt_mult") 1);
    8.33  by (dtac mp 1);
    8.34 -by (etac monofun_rt_mult 1);
    8.35 +by (etac (thm "monofun_rt_mult") 1);
    8.36  by (mp_tac 1); 
    8.37  by (atac 1);
    8.38  qed "stream_monoP2I";
    8.39 @@ -123,9 +123,9 @@
    8.40          etac allE 1 THEN mp_tac 1,
    8.41  	dres_inst_tac [("P","%x. x")] subst 1 THEN atac 1,
    8.42  	etac conjE 1 THEN rtac conjI 1,
    8.43 -	 etac (slen_take_lemma3 RS ssubst) 1 THEN atac 1,
    8.44 +	 etac (thm "slen_take_lemma3" RS ssubst) 1 THEN atac 1,
    8.45  	 atac 1,
    8.46 -	etac allE 1 THEN etac allE 1 THEN dtac mp 1 THEN etac monofun_rt_mult 1,
    8.47 +	etac allE 1 THEN etac allE 1 THEN dtac mp 1 THEN etac (thm "monofun_rt_mult") 1,
    8.48  	mp_tac 1,
    8.49  	atac 1]);
    8.50  
     9.1 --- a/src/HOLCF/IsaMakefile	Tue Sep 07 15:59:16 2004 +0200
     9.2 +++ b/src/HOLCF/IsaMakefile	Tue Sep 07 16:02:42 2004 +0200
     9.3 @@ -39,7 +39,7 @@
     9.4    Up1.thy Up2.ML Up2.thy Up3.ML Up3.thy adm.ML cont_consts.ML \
     9.5    domain/axioms.ML domain/extender.ML domain/interface.ML \
     9.6    domain/library.ML domain/syntax.ML domain/theorems.ML holcf_logic.ML \
     9.7 -  ex/Stream.thy ex/Stream.ML Streams.thy
     9.8 +  ex/Stream.thy
     9.9  	@$(ISATOOL) usedir -b -r $(OUT)/HOL HOLCF
    9.10  
    9.11  
    9.12 @@ -68,7 +68,8 @@
    9.13  
    9.14  HOLCF-FOCUS: HOLCF $(LOG)/HOLCF-FOCUS.gz
    9.15  
    9.16 -$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstream.thy FOCUS/Fstream.ML \
    9.17 +$(LOG)/HOLCF-FOCUS.gz: $(OUT)/HOLCF FOCUS/Fstreams.thy \
    9.18 +  FOCUS/Fstream.thy FOCUS/Fstream.ML \
    9.19    FOCUS/FOCUS.thy FOCUS/FOCUS.ML \
    9.20    FOCUS/Stream_adm.thy FOCUS/Stream_adm.ML  ../HOL/Library/Continuity.thy \
    9.21    FOCUS/Buffer.thy FOCUS/Buffer.ML FOCUS/Buffer_adm.thy FOCUS/Buffer_adm.ML
    10.1 --- a/src/HOLCF/ROOT.ML	Tue Sep 07 15:59:16 2004 +0200
    10.2 +++ b/src/HOLCF/ROOT.ML	Tue Sep 07 16:02:42 2004 +0200
    10.3 @@ -24,6 +24,5 @@
    10.4  use "domain/interface.ML";
    10.5  
    10.6  path_add "~~/src/HOLCF/ex";
    10.7 -use_thy "Streams";
    10.8  
    10.9  print_depth 10;  
    11.1 --- a/src/HOLCF/Streams.thy	Tue Sep 07 15:59:16 2004 +0200
    11.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.3 @@ -1,564 +0,0 @@
    11.4 -(*  Title: 	HOLCF/Streams.thy
    11.5 -    ID:         $Id$
    11.6 -    Author: 	Borislav Gajanovic and David von Oheimb
    11.7 -
    11.8 -Stream domains with concatenation.
    11.9 -TODO: HOLCF/ex/Stream.* should be integrated into this file.
   11.10 -*)
   11.11 -
   11.12 -theory Streams = Stream :
   11.13 -
   11.14 -(* ----------------------------------------------------------------------- *)
   11.15 -
   11.16 -lemma stream_neq_UU: "x~=UU ==> EX a as. x=a&&as & a~=UU"
   11.17 -by (simp add: stream_exhaust_eq,auto)
   11.18 -
   11.19 -lemma stream_prefix1: "[| x<<y; xs<<ys |] ==> x&&xs << y&&ys"
   11.20 -by (insert stream_prefix' [of y "x&&xs" ys],force)
   11.21 -
   11.22 -lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1"
   11.23 -apply (insert chain_stream_take [of s1])
   11.24 -by (drule chain_mono3,auto)
   11.25 -
   11.26 -lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2"
   11.27 -by (simp add: monofun_cfun_arg)
   11.28 -
   11.29 -lemma stream_take_prefix [simp]: "stream_take n$s << s"
   11.30 -apply (subgoal_tac "s=(LUB n. stream_take n$s)")
   11.31 - apply (erule ssubst, rule is_ub_thelub)
   11.32 - apply (simp only: chain_stream_take)
   11.33 -by (simp only: stream_reach2)
   11.34 -
   11.35 -lemma stream_take_take_less:"stream_take k$(stream_take n$s) << stream_take k$s"
   11.36 -by (rule monofun_cfun_arg,auto)
   11.37 -
   11.38 -(* ----------------------------------------------------------------------- *)
   11.39 -
   11.40 -lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)"
   11.41 -apply (rule stream.casedist [of s1])
   11.42 - apply (rule stream.casedist [of s2],simp+)
   11.43 -by (rule stream.casedist [of s2],auto)
   11.44 -
   11.45 -lemma slen_take_lemma4 [rule_format]: 
   11.46 -  "!s. stream_take n$s ~= s --> #(stream_take n$s) = Fin n"
   11.47 -apply (induct_tac n,auto simp add: Fin_0)
   11.48 -apply (case_tac "s=UU",simp)
   11.49 -by (drule stream_neq_UU,auto)
   11.50 -
   11.51 -lemma slen_take_lemma5: "#(stream_take n$s) <= Fin n"; 
   11.52 -apply (case_tac "stream_take n$s = s")
   11.53 - apply (simp add: slen_take_eq_rev)
   11.54 -by (simp add: slen_take_lemma4)
   11.55 -
   11.56 -lemma stream_take_idempotent [simp]: 
   11.57 - "stream_take n$(stream_take n$s) = stream_take n$s"
   11.58 -apply (case_tac "stream_take n$s = s")
   11.59 -apply (auto,insert slen_take_lemma4 [of n s]);
   11.60 -by (auto,insert slen_take_lemma1 [of "stream_take n$s" n],simp)
   11.61 -
   11.62 -lemma stream_take_take_Suc [simp]: "stream_take n$(stream_take (Suc n)$s) = 
   11.63 -                                    stream_take n$s"
   11.64 -apply (simp add: po_eq_conv,auto)
   11.65 - apply (simp add: stream_take_take_less)
   11.66 -apply (subgoal_tac "stream_take n$s = stream_take n$(stream_take n$s)")
   11.67 - apply (erule ssubst)
   11.68 - apply (rule_tac monofun_cfun_arg)
   11.69 - apply (insert chain_stream_take [of s])
   11.70 -by (simp add: chain_def,simp)
   11.71 -
   11.72 -lemma mono_stream_take_pred: 
   11.73 -  "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
   11.74 -                       stream_take n$s1 << stream_take n$s2"
   11.75 -by (drule mono_stream_take [of _ _ n],simp)
   11.76 -
   11.77 -lemma stream_take_lemma10 [rule_format]:
   11.78 -  "ALL k<=n. stream_take n$s1 << stream_take n$s2 
   11.79 -                             --> stream_take k$s1 << stream_take k$s2"
   11.80 -apply (induct_tac n,simp,clarsimp)
   11.81 -apply (case_tac "k=Suc n",blast)
   11.82 -apply (erule_tac x="k" in allE)
   11.83 -by (drule mono_stream_take_pred,simp)
   11.84 -
   11.85 -lemma stream_take_finite [simp]: "stream_finite (stream_take n$s)"
   11.86 -apply (simp add: stream.finite_def)
   11.87 -by (rule_tac x="n" in exI,simp)
   11.88 -
   11.89 -lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
   11.90 -by (simp add: slen_def)
   11.91 -
   11.92 -lemma stream_take_Suc_neq: "stream_take (Suc n)$s ~=s ==> 
   11.93 -                     stream_take n$s ~= stream_take (Suc n)$s"
   11.94 -apply auto
   11.95 -apply (subgoal_tac "stream_take n$s ~=s")
   11.96 - apply (insert slen_take_lemma4 [of n s],auto)
   11.97 -apply (rule stream.casedist [of s],simp)
   11.98 -apply (simp add: inat_defs split:inat_splits)
   11.99 -by (simp add: slen_take_lemma4)
  11.100 -
  11.101 -
  11.102 -(* ----------------------------------------------------------------------- *)
  11.103 -
  11.104 -consts
  11.105 - 
  11.106 -  i_rt :: "nat => 'a stream => 'a stream" (* chops the first i elements *)
  11.107 -  i_th :: "nat => 'a stream => 'a"        (* the i-th element *)
  11.108 -
  11.109 -  sconc         :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) 
  11.110 -  constr_sconc  :: "'a stream => 'a stream => 'a stream" (* constructive *)
  11.111 -  constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" 
  11.112 -
  11.113 -defs
  11.114 -  i_rt_def: "i_rt == %i s. iterate i rt s"  
  11.115 -  i_th_def: "i_th == %i s. ft$(i_rt i s)" 
  11.116 -
  11.117 -  sconc_def: "s1 ooo s2 == case #s1 of 
  11.118 -                       Fin n => (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
  11.119 -                     | \<infinity>     => s1" 
  11.120 -
  11.121 -  constr_sconc_def: "constr_sconc s1 s2 == case #s1 of 
  11.122 -                                             Fin n => constr_sconc' n s1 s2 
  11.123 -                                           | \<infinity>    => s1"
  11.124 -primrec 
  11.125 -  constr_sconc'_0:   "constr_sconc' 0 s1 s2 = s2"
  11.126 -  constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 && 
  11.127 -                                                    constr_sconc' n (rt$s1) s2"
  11.128 -
  11.129 -
  11.130 -(* ----------------------------------------------------------------------- *)
  11.131 -   section "i_rt"
  11.132 -(* ----------------------------------------------------------------------- *)
  11.133 -
  11.134 -lemma i_rt_UU [simp]: "i_rt n UU = UU"
  11.135 -apply (simp add: i_rt_def)
  11.136 -by (rule iterate.induct,auto)
  11.137 -
  11.138 -lemma i_rt_0 [simp]: "i_rt 0 s = s"
  11.139 -by (simp add: i_rt_def)
  11.140 -
  11.141 -lemma i_rt_Suc [simp]: "a ~= UU ==> i_rt (Suc n) (a&&s) = i_rt n s"
  11.142 -by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc)
  11.143 -
  11.144 -lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt$s)"
  11.145 -by (simp only: i_rt_def iterate_Suc2)
  11.146 -
  11.147 -lemma i_rt_Suc_back:"i_rt (Suc n) s = rt$(i_rt n s)"
  11.148 -by (simp only: i_rt_def,auto)
  11.149 -
  11.150 -lemma i_rt_mono: "x << s ==> i_rt n x  << i_rt n s"
  11.151 -by (simp add: i_rt_def monofun_rt_mult)
  11.152 -
  11.153 -lemma i_rt_ij_lemma: "Fin (i + j) <= #x ==> Fin j <= #(i_rt i x)"
  11.154 -by (simp add: i_rt_def slen_rt_mult)
  11.155 -
  11.156 -lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)"
  11.157 -apply (induct_tac n,auto)
  11.158 -apply (simp add: i_rt_Suc_back)
  11.159 -by (drule slen_rt_mono,simp)
  11.160 -
  11.161 -lemma i_rt_take_lemma1 [rule_format]: "ALL s. i_rt n (stream_take n$s) = UU"
  11.162 -apply (induct_tac n); 
  11.163 - apply (simp add: i_rt_Suc_back,auto)
  11.164 -apply (case_tac "s=UU",auto)
  11.165 -by (drule stream_neq_UU,simp add: i_rt_Suc_forw,auto)
  11.166 -
  11.167 -lemma i_rt_slen: "(i_rt n s = UU) = (stream_take n$s = s)"
  11.168 -apply auto
  11.169 - apply (insert i_rt_ij_lemma [of n "Suc 0" s]);
  11.170 - apply (subgoal_tac "#(i_rt n s)=0")
  11.171 -  apply (case_tac "stream_take n$s = s",simp+)
  11.172 -  apply (insert slen_take_eq [of n s],simp)
  11.173 -  apply (simp add: inat_defs split:inat_splits)
  11.174 - apply (simp add: slen_take_eq )
  11.175 -by (simp, insert i_rt_take_lemma1 [of n s],simp)
  11.176 -
  11.177 -lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU"
  11.178 -by (simp add: i_rt_slen slen_take_lemma1)
  11.179 -
  11.180 -lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s"
  11.181 -apply (induct_tac n, auto)
  11.182 - apply (rule stream.casedist [of "s"], auto simp del: i_rt_Suc)
  11.183 -by (simp add: i_rt_Suc_back stream_finite_rt_eq)+
  11.184 -
  11.185 -lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl &
  11.186 -                            #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j 
  11.187 -                                              --> Fin (j + t) = #x"
  11.188 -apply (induct_tac n,auto)
  11.189 - apply (simp add: inat_defs)
  11.190 -apply (case_tac "x=UU",auto)
  11.191 - apply (simp add: inat_defs)
  11.192 -apply (drule stream_neq_UU,auto)
  11.193 -apply (subgoal_tac "EX k. Fin k = #as",clarify)
  11.194 - apply (erule_tac x="k" in allE)
  11.195 - apply (erule_tac x="as" in allE,auto)
  11.196 - apply (erule_tac x="THE p. Suc p = t" in allE,auto)
  11.197 -   apply (simp add: inat_defs split:inat_splits)
  11.198 -  apply (simp add: inat_defs split:inat_splits)
  11.199 -  apply (simp only: the_equality)
  11.200 - apply (simp add: inat_defs split:inat_splits)
  11.201 - apply force
  11.202 -by (simp add: inat_defs split:inat_splits)
  11.203 -
  11.204 -lemma take_i_rt_len: 
  11.205 -"[| Fin sl = #x; n <= sl; #(stream_take n$x) = Fin t; #(i_rt n x) = Fin j |] ==>
  11.206 -    Fin (j + t) = #x"
  11.207 -by (blast intro: take_i_rt_len_lemma [rule_format])
  11.208 -
  11.209 -
  11.210 -(* ----------------------------------------------------------------------- *)
  11.211 -   section "i_th"
  11.212 -(* ----------------------------------------------------------------------- *)
  11.213 -
  11.214 -lemma i_th_i_rt_step:
  11.215 -"[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==> 
  11.216 -   i_rt n s1 << i_rt n s2"
  11.217 -apply (simp add: i_th_def i_rt_Suc_back)
  11.218 -apply (rule stream.casedist [of "i_rt n s1"],simp)
  11.219 -apply (rule stream.casedist [of "i_rt n s2"],auto)
  11.220 -by (drule stream_prefix1,auto)
  11.221 -
  11.222 -lemma i_th_stream_take_Suc [rule_format]: 
  11.223 - "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s"
  11.224 -apply (induct_tac n,auto)
  11.225 - apply (simp add: i_th_def)
  11.226 - apply (case_tac "s=UU",auto)
  11.227 - apply (drule stream_neq_UU,auto)
  11.228 -apply (case_tac "s=UU",simp add: i_th_def)
  11.229 -apply (drule stream_neq_UU,auto)
  11.230 -by (simp add: i_th_def i_rt_Suc_forw)
  11.231 -
  11.232 -lemma last_lemma10: "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==> 
  11.233 -                     i_th n s1 << i_th n s2"
  11.234 -apply (rule i_th_stream_take_Suc [THEN subst])
  11.235 -apply (rule i_th_stream_take_Suc [THEN subst]) back
  11.236 -apply (simp add: i_th_def)
  11.237 -apply (rule monofun_cfun_arg)
  11.238 -by (erule i_rt_mono)
  11.239 -
  11.240 -lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)$s)"
  11.241 -apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)$s)"])
  11.242 -apply (rule i_th_stream_take_Suc [THEN subst])
  11.243 -apply (simp add: i_th_def  i_rt_Suc_back [symmetric])
  11.244 -by (simp add: i_rt_take_lemma1)
  11.245 -
  11.246 -lemma i_th_last_eq: 
  11.247 -"i_th n s1 = i_th n s2 ==> i_rt n (stream_take (Suc n)$s1) = i_rt n (stream_take (Suc n)$s2)"
  11.248 -apply (insert i_th_last [of n s1])
  11.249 -apply (insert i_th_last [of n s2])
  11.250 -by auto
  11.251 -
  11.252 -lemma i_th_prefix_lemma:
  11.253 -"[| k <= n; stream_take (Suc n)$s1 << stream_take (Suc n)$s2 |] ==> 
  11.254 -    i_th k s1 << i_th k s2"
  11.255 -apply (subgoal_tac "stream_take (Suc k)$s1 << stream_take (Suc k)$s2")
  11.256 - apply (simp add: last_lemma10)
  11.257 -by (blast intro: stream_take_lemma10)
  11.258 -
  11.259 -lemma take_i_rt_prefix_lemma1: 
  11.260 -  "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
  11.261 -   i_rt (Suc n) s1 << i_rt (Suc n) s2 ==> 
  11.262 -   i_rt n s1 << i_rt n s2 & stream_take n$s1 << stream_take n$s2"
  11.263 -apply auto
  11.264 - apply (insert i_th_prefix_lemma [of n n s1 s2])
  11.265 - apply (rule i_th_i_rt_step,auto)
  11.266 -by (drule mono_stream_take_pred,simp)
  11.267 -
  11.268 -lemma take_i_rt_prefix_lemma: 
  11.269 -"[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2"
  11.270 -apply (case_tac "n=0",simp)
  11.271 -apply (insert neq0_conv [of n])
  11.272 -apply (insert not0_implies_Suc [of n],auto)
  11.273 -apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 & 
  11.274 -                    i_rt 0 s1 << i_rt 0 s2")
  11.275 - defer 1
  11.276 - apply (rule zero_induct,blast)
  11.277 - apply (blast dest: take_i_rt_prefix_lemma1)
  11.278 -by simp
  11.279 -
  11.280 -lemma streams_prefix_lemma: "(s1 << s2) = 
  11.281 -  (stream_take n$s1 << stream_take n$s2 & i_rt n s1 << i_rt n s2)"; 
  11.282 -apply auto
  11.283 -  apply (simp add: monofun_cfun_arg)
  11.284 - apply (simp add: i_rt_mono)
  11.285 -by (erule take_i_rt_prefix_lemma,simp)
  11.286 -
  11.287 -lemma streams_prefix_lemma1:
  11.288 - "[| stream_take n$s1 = stream_take n$s2; i_rt n s1 = i_rt n s2 |] ==> s1 = s2"
  11.289 -apply (simp add: po_eq_conv,auto)
  11.290 - apply (insert streams_prefix_lemma)
  11.291 - by blast+
  11.292 -
  11.293 -
  11.294 -(* ----------------------------------------------------------------------- *)
  11.295 -   section "sconc"
  11.296 -(* ----------------------------------------------------------------------- *)
  11.297 -
  11.298 -lemma UU_sconc [simp]: " UU ooo s = s "
  11.299 -by (simp add: sconc_def inat_defs)
  11.300 -
  11.301 -lemma scons_neq_UU: "a~=UU ==> a && s ~=UU"
  11.302 -by auto
  11.303 -
  11.304 -lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y"
  11.305 -apply (simp add: sconc_def inat_defs split:inat_splits,auto)
  11.306 -apply (rule someI2_ex,auto)
  11.307 - apply (rule_tac x="x && y" in exI,auto)
  11.308 -apply (simp add: i_rt_Suc_forw)
  11.309 -apply (case_tac "xa=UU",simp)
  11.310 -by (drule stream_neq_UU,auto)
  11.311 -
  11.312 -lemma ex_sconc [rule_format]: 
  11.313 -  "ALL k y. #x = Fin k --> (EX w. stream_take k$w = x & i_rt k w = y)"
  11.314 -apply (case_tac "#x")
  11.315 - apply (rule stream_finite_ind [of x],auto)
  11.316 -  apply (simp add: stream.finite_def)
  11.317 -  apply (drule slen_take_lemma1,blast)
  11.318 - apply (simp add: inat_defs split:inat_splits)+
  11.319 -apply (erule_tac x="y" in allE,auto)
  11.320 -by (rule_tac x="a && w" in exI,auto)
  11.321 -
  11.322 -lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y"; 
  11.323 -apply (simp add: sconc_def inat_defs split:inat_splits , arith?,auto)
  11.324 -apply (rule someI2_ex,auto)
  11.325 -by (drule ex_sconc,simp)
  11.326 -
  11.327 -lemma sconc_inj2: "\<lbrakk>Fin n = #x; x ooo y = x ooo z\<rbrakk> \<Longrightarrow> y = z"
  11.328 -apply (frule_tac y=y in rt_sconc1)
  11.329 -by (auto elim: rt_sconc1)
  11.330 -
  11.331 -lemma sconc_UU [simp]:"s ooo UU = s"
  11.332 -apply (case_tac "#s")
  11.333 - apply (simp add: sconc_def inat_defs)
  11.334 - apply (rule someI2_ex)
  11.335 -  apply (rule_tac x="s" in exI)
  11.336 -  apply auto
  11.337 -   apply (drule slen_take_lemma1,auto)
  11.338 -  apply (simp add: i_rt_lemma_slen)
  11.339 - apply (drule slen_take_lemma1,auto)
  11.340 - apply (simp add: i_rt_slen)
  11.341 -by (simp add: sconc_def inat_defs)
  11.342 -
  11.343 -lemma stream_take_sconc [simp]: "Fin n = #x ==> stream_take n$(x ooo y) = x"
  11.344 -apply (simp add: sconc_def)
  11.345 -apply (simp add: inat_defs split:inat_splits,auto)
  11.346 -apply (rule someI2_ex,auto)
  11.347 -by (drule ex_sconc,simp)
  11.348 -
  11.349 -lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y"
  11.350 -apply (case_tac "#x",auto)
  11.351 - apply (simp add: sconc_def) 
  11.352 - apply (rule someI2_ex)
  11.353 -  apply (drule ex_sconc,simp)
  11.354 - apply (rule someI2_ex,auto)
  11.355 -  apply (simp add: i_rt_Suc_forw)
  11.356 -  apply (rule_tac x="a && x" in exI,auto)
  11.357 - apply (case_tac "xa=UU",auto)
  11.358 -  apply (drule_tac s="stream_take nat$x" in scons_neq_UU)
  11.359 -  apply (simp add: i_rt_Suc_forw)
  11.360 - apply (drule stream_neq_UU,clarsimp)
  11.361 - apply (drule streams_prefix_lemma1,simp+)
  11.362 -by (simp add: sconc_def)
  11.363 -
  11.364 -lemma ft_sconc: "x ~= UU ==> ft$(x ooo y) = ft$x"
  11.365 -by (rule stream.casedist [of x],auto)
  11.366 -
  11.367 -lemma sconc_assoc: "(x ooo y) ooo z = x ooo y ooo z"
  11.368 -apply (case_tac "#x")
  11.369 - apply (rule stream_finite_ind [of x],auto simp del: scons_sconc)
  11.370 -  apply (simp add: stream.finite_def del: scons_sconc)
  11.371 -  apply (drule slen_take_lemma1,auto simp del: scons_sconc)
  11.372 - apply (case_tac "a = UU", auto)
  11.373 -by (simp add: sconc_def)
  11.374 -
  11.375 -
  11.376 -(* ----------------------------------------------------------------------- *)
  11.377 -
  11.378 -lemma sconc_mono: "y << y' ==> x ooo y << x ooo y'"
  11.379 -apply (case_tac "#x")
  11.380 - apply (rule stream_finite_ind [of "x"])
  11.381 -   apply (auto simp add: stream.finite_def)
  11.382 -  apply (drule slen_take_lemma1,blast)
  11.383 - by (simp add: stream_prefix',auto simp add: sconc_def)
  11.384 -
  11.385 -lemma sconc_mono1 [simp]: "x << x ooo y"
  11.386 -by (rule sconc_mono [of UU, simplified])
  11.387 -
  11.388 -(* ----------------------------------------------------------------------- *)
  11.389 -
  11.390 -lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)"
  11.391 -apply (case_tac "#x",auto)
  11.392 -   by (insert sconc_mono1 [of x y],auto);
  11.393 -
  11.394 -(* ----------------------------------------------------------------------- *)
  11.395 -
  11.396 -lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x"
  11.397 -by (rule stream.casedist,auto)
  11.398 -
  11.399 -(* ----------------------------------------------------------------------- *)
  11.400 -
  11.401 -lemma sconc_lemma [rule_format, simp]: "ALL s. stream_take n$s ooo i_rt n s = s"
  11.402 -apply (induct_tac n,auto)
  11.403 -apply (case_tac "s=UU",auto)
  11.404 -by (drule stream_neq_UU,auto)
  11.405 -
  11.406 -(* ----------------------------------------------------------------------- *)
  11.407 -   subsection "pointwise equality"
  11.408 -(* ----------------------------------------------------------------------- *)
  11.409 -
  11.410 -lemma ex_last_stream_take_scons: "stream_take (Suc n)$s = 
  11.411 -                     stream_take n$s ooo i_rt n (stream_take (Suc n)$s)"
  11.412 -by (insert sconc_lemma [of n "stream_take (Suc n)$s"],simp)
  11.413 -
  11.414 -lemma i_th_stream_take_eq: 
  11.415 -"!!n. ALL n. i_th n s1 = i_th n s2 ==> stream_take n$s1 = stream_take n$s2"
  11.416 -apply (induct_tac n,auto)
  11.417 -apply (subgoal_tac "stream_take (Suc na)$s1 =
  11.418 -                    stream_take na$s1 ooo i_rt na (stream_take (Suc na)$s1)")
  11.419 - apply (subgoal_tac "i_rt na (stream_take (Suc na)$s1) = 
  11.420 -                    i_rt na (stream_take (Suc na)$s2)")
  11.421 -  apply (subgoal_tac "stream_take (Suc na)$s2 = 
  11.422 -                    stream_take na$s2 ooo i_rt na (stream_take (Suc na)$s2)")
  11.423 -   apply (insert ex_last_stream_take_scons,simp)
  11.424 -  apply blast
  11.425 - apply (erule_tac x="na" in allE)
  11.426 - apply (insert i_th_last_eq [of _ s1 s2])
  11.427 -by blast+
  11.428 -
  11.429 -lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2"
  11.430 -by (insert i_th_stream_take_eq [THEN stream.take_lemmas],blast)
  11.431 -
  11.432 -(* ----------------------------------------------------------------------- *)
  11.433 -   subsection "finiteness"
  11.434 -(* ----------------------------------------------------------------------- *)
  11.435 -
  11.436 -lemma slen_sconc_finite1:
  11.437 -  "[| #(x ooo y) = Infty; Fin n = #x |] ==> #y = Infty"
  11.438 -apply (case_tac "#y ~= Infty",auto)
  11.439 -apply (simp only: slen_infinite [symmetric])
  11.440 -apply (drule_tac y=y in rt_sconc1)
  11.441 -apply (insert stream_finite_i_rt [of n "x ooo y"])
  11.442 -by (simp add: slen_infinite)
  11.443 -
  11.444 -lemma slen_sconc_infinite1: "#x=Infty ==> #(x ooo y) = Infty"
  11.445 -by (simp add: sconc_def)
  11.446 -
  11.447 -lemma slen_sconc_infinite2: "#y=Infty ==> #(x ooo y) = Infty"
  11.448 -apply (case_tac "#x")
  11.449 - apply (simp add: sconc_def)
  11.450 - apply (rule someI2_ex)
  11.451 -  apply (drule ex_sconc,auto)
  11.452 - apply (erule contrapos_pp)
  11.453 - apply (insert stream_finite_i_rt)
  11.454 - apply (simp add: slen_infinite ,auto)
  11.455 -by (simp add: sconc_def)
  11.456 -
  11.457 -lemma sconc_finite: "(#x~=Infty & #y~=Infty) = (#(x ooo y)~=Infty)"
  11.458 -apply auto
  11.459 -  apply (case_tac "#x",auto)
  11.460 -  apply (erule contrapos_pp,simp)
  11.461 -  apply (erule slen_sconc_finite1,simp)
  11.462 - apply (drule slen_sconc_infinite1 [of _ y],simp)
  11.463 -by (drule slen_sconc_infinite2 [of _ x],simp)
  11.464 -
  11.465 -(* ----------------------------------------------------------------------- *)
  11.466 -
  11.467 -lemma slen_sconc_mono3: "[| Fin n = #x; Fin k = #(x ooo y) |] ==> n <= k"
  11.468 -apply (insert slen_mono [of "x" "x ooo y"])
  11.469 -by (simp add: inat_defs split: inat_splits)
  11.470 -
  11.471 -(* ----------------------------------------------------------------------- *)
  11.472 -   subsection "finite slen"
  11.473 -(* ----------------------------------------------------------------------- *)
  11.474 -
  11.475 -lemma slen_sconc: "[| Fin n = #x; Fin m = #y |] ==> #(x ooo y) = Fin (n + m)"
  11.476 -apply (case_tac "#(x ooo y)")
  11.477 - apply (frule_tac y=y in rt_sconc1)
  11.478 - apply (insert take_i_rt_len [of "THE j. Fin j = #(x ooo y)" "x ooo y" n n m],simp)
  11.479 - apply (insert slen_sconc_mono3 [of n x _ y],simp)
  11.480 -by (insert sconc_finite [of x y],auto)
  11.481 -
  11.482 -(* ----------------------------------------------------------------------- *)
  11.483 -   subsection "flat prefix"
  11.484 -(* ----------------------------------------------------------------------- *)
  11.485 -
  11.486 -lemma sconc_prefix: "(s1::'a::flat stream) << s2 ==> EX t. s1 ooo t = s2"
  11.487 -apply (case_tac "#s1")
  11.488 - apply (subgoal_tac "stream_take nat$s1 = stream_take nat$s2");
  11.489 -  apply (rule_tac x="i_rt nat s2" in exI)
  11.490 -  apply (simp add: sconc_def)
  11.491 -  apply (rule someI2_ex)
  11.492 -   apply (drule ex_sconc)
  11.493 -   apply (simp,clarsimp,drule streams_prefix_lemma1)
  11.494 -   apply (simp+,rule slen_take_lemma3 [rule_format, of _ s1 s2]);
  11.495 -  apply (simp+,rule_tac x="UU" in exI)
  11.496 -apply (insert slen_take_lemma3 [rule_format, of _ s1 s2]);
  11.497 -by (rule stream.take_lemmas,simp)
  11.498 -
  11.499 -(* ----------------------------------------------------------------------- *)
  11.500 -   subsection "continuity"
  11.501 -(* ----------------------------------------------------------------------- *)
  11.502 -
  11.503 -lemma chain_sconc: "chain S ==> chain (%i. (x ooo S i))"
  11.504 -by (simp add: chain_def,auto simp add: sconc_mono)
  11.505 -
  11.506 -lemma chain_scons: "chain S ==> chain (%i. a && S i)"
  11.507 -apply (simp add: chain_def,auto)
  11.508 -by (rule monofun_cfun_arg,simp)
  11.509 -
  11.510 -lemma contlub_scons: "contlub (%x. a && x)"
  11.511 -by (simp add: contlub_Rep_CFun2)
  11.512 -
  11.513 -lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
  11.514 -apply (insert contlub_scons [of a])
  11.515 -by (simp only: contlub)
  11.516 -
  11.517 -lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==> 
  11.518 -                        (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
  11.519 -apply (rule stream_finite_ind [of x])
  11.520 - apply (auto)
  11.521 -apply (subgoal_tac "(LUB i. a && (s ooo Y i)) = a && (LUB i. s ooo Y i)")
  11.522 - by (force,blast dest: contlub_scons_lemma chain_sconc)
  11.523 -
  11.524 -lemma contlub_sconc_lemma: 
  11.525 -  "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
  11.526 -apply (case_tac "#x=Infty")
  11.527 - apply (simp add: sconc_def)
  11.528 - prefer 2
  11.529 - apply (drule finite_lub_sconc,auto simp add: slen_infinite)
  11.530 -apply (simp add: slen_def)
  11.531 -apply (insert lub_const [of x] unique_lub [of _ x _])
  11.532 -by (auto simp add: lub)
  11.533 -
  11.534 -lemma contlub_sconc: "contlub (%y. x ooo y)"; 
  11.535 -by (rule contlubI, insert contlub_sconc_lemma [of _ x], simp);
  11.536 -
  11.537 -lemma monofun_sconc: "monofun (%y. x ooo y)"
  11.538 -by (simp add: monofun sconc_mono)
  11.539 -
  11.540 -lemma cont_sconc: "cont (%y. x ooo y)"
  11.541 -apply (rule  monocontlub2cont)
  11.542 - apply (rule monofunI, simp add: sconc_mono)
  11.543 -by (rule contlub_sconc);
  11.544 -
  11.545 -
  11.546 -(* ----------------------------------------------------------------------- *)
  11.547 -   section "constr_sconc"
  11.548 -(* ----------------------------------------------------------------------- *)
  11.549 -
  11.550 -lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s"
  11.551 -by (simp add: constr_sconc_def inat_defs)
  11.552 -
  11.553 -lemma "x ooo y = constr_sconc x y"
  11.554 -apply (case_tac "#x")
  11.555 - apply (rule stream_finite_ind [of x],auto simp del: scons_sconc)
  11.556 -  defer 1
  11.557 -  apply (simp add: constr_sconc_def del: scons_sconc)
  11.558 -  apply (case_tac "#s")
  11.559 -   apply (simp add: inat_defs)
  11.560 -   apply (case_tac "a=UU",auto simp del: scons_sconc)
  11.561 -   apply (simp)
  11.562 -  apply (simp add: sconc_def)
  11.563 - apply (simp add: constr_sconc_def)
  11.564 -apply (simp add: stream.finite_def)
  11.565 -by (drule slen_take_lemma1,auto)
  11.566 -
  11.567 -end
    12.1 --- a/src/HOLCF/ex/Dagstuhl.ML	Tue Sep 07 15:59:16 2004 +0200
    12.2 +++ b/src/HOLCF/ex/Dagstuhl.ML	Tue Sep 07 16:02:42 2004 +0200
    12.3 @@ -30,12 +30,12 @@
    12.4  val lemma5=result();
    12.5  
    12.6  val prems = goal Dagstuhl.thy "YS = YYS";
    12.7 -by (resolve_tac stream.take_lemmas 1);
    12.8 +by (resolve_tac (thms "stream.take_lemmas") 1);
    12.9  by (induct_tac "n" 1);
   12.10 -by (simp_tac (simpset() addsimps stream.rews) 1);
   12.11 +by (simp_tac (simpset() addsimps (thms "stream.rews")) 1);
   12.12  by (stac YS_def2 1);
   12.13  by (stac YYS_def2 1);
   12.14 -by (asm_simp_tac (simpset() addsimps stream.rews) 1);
   12.15 +by (asm_simp_tac (simpset() addsimps (thms "stream.rews")) 1);
   12.16  by (rtac (lemma5 RS sym RS subst) 1);
   12.17  by (rtac refl 1);
   12.18  val wir_moel=result();
    13.1 --- a/src/HOLCF/ex/Stream.ML	Tue Sep 07 15:59:16 2004 +0200
    13.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.3 @@ -1,594 +0,0 @@
    13.4 -(*  Title: 	HOLCF/ex//Stream.ML
    13.5 -    ID:         $Id$
    13.6 -    Author: 	Franz Regensburger and David von Oheimb, TU Muenchen
    13.7 -
    13.8 -General Stream domain.
    13.9 -*)
   13.10 -
   13.11 -fun stream_case_tac s i = res_inst_tac [("x",s)] stream.casedist i
   13.12 -			  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1);
   13.13 -
   13.14 -
   13.15 -val [stream_con_rew1,stream_con_rew2] = stream.con_rews;
   13.16 -
   13.17 -Addsimps stream.rews;
   13.18 -Addsimps[eq_UU_iff RS sym];
   13.19 -
   13.20 -(* ----------------------------------------------------------------------- *)
   13.21 -(* theorems about scons                                                    *)
   13.22 -(* ----------------------------------------------------------------------- *)
   13.23 -
   13.24 -section "scons";
   13.25 -
   13.26 -Goal "(a && s = UU) = (a = UU)";
   13.27 -by Safe_tac;
   13.28 -by (etac contrapos_pp 1);
   13.29 -by (safe_tac (claset() addSIs stream.con_rews));
   13.30 -qed "scons_eq_UU";
   13.31 -
   13.32 -Goal "[| a && x = UU; a ~= UU |] ==> R";
   13.33 -by (dtac stream_con_rew2 1);
   13.34 -by (contr_tac 1);
   13.35 -qed "scons_not_empty";
   13.36 -
   13.37 -Goal "(x ~= UU) = (EX a y. a ~= UU &  x = a && y)";
   13.38 -by (cut_facts_tac [stream.exhaust] 1);
   13.39 -by (best_tac (claset() addDs [stream_con_rew2]) 1);
   13.40 -qed "stream_exhaust_eq";
   13.41 -
   13.42 -Goal 
   13.43 -"[| a && s << t; a ~= UU  |] ==> EX b tt. t = b && tt &  b ~= UU &  s << tt";
   13.44 -by (stream_case_tac "t" 1);
   13.45 -by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1);
   13.46 -by (fast_tac (claset() addDs stream.inverts) 1);
   13.47 -qed "stream_prefix";
   13.48 -
   13.49 -Goal "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys";
   13.50 -by (cut_inst_tac [("x1","x::'a::flat"), ("x","y::'a::flat")] 
   13.51 -                 (ax_flat RS spec RS spec) 1);
   13.52 -by (forward_tac stream.inverts 1);
   13.53 -by Safe_tac;
   13.54 -by (dtac (hd stream.con_rews RS subst) 1);
   13.55 -by (fast_tac (claset() addDs [eq_UU_iff RS iffD2, stream_con_rew2]) 1);
   13.56 -qed "stream_flat_prefix";
   13.57 -
   13.58 -Goal "b ~= UU ==> x << b && z = \
   13.59 -\           (x = UU |  (EX a y. x = a && y &  a ~= UU &  a << b &  y << z))";
   13.60 -by Safe_tac;
   13.61 -by (stream_case_tac "x" 1);
   13.62 -by (safe_tac (claset() addSDs stream.inverts 
   13.63 -                addSIs [monofun_cfun, monofun_cfun_arg]));
   13.64 -by (Fast_tac 1);
   13.65 -qed "stream_prefix'";
   13.66 -
   13.67 -Goal "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b &  s = t)";
   13.68 -by (best_tac (claset() addSEs stream.injects) 1);
   13.69 -qed "stream_inject_eq";	
   13.70 -Addsimps [stream_inject_eq];
   13.71 -
   13.72 -
   13.73 -(* ----------------------------------------------------------------------- *)
   13.74 -(* theorems about stream_when                                              *)
   13.75 -(* ----------------------------------------------------------------------- *)
   13.76 -
   13.77 -section "stream_when";
   13.78 -
   13.79 -Goal "stream_when$UU$s=UU";
   13.80 -by (stream_case_tac "s" 1);
   13.81 -by (ALLGOALS Asm_simp_tac);
   13.82 -qed "stream_when_strictf";
   13.83 -	
   13.84 -
   13.85 -(* ----------------------------------------------------------------------- *)
   13.86 -(* theorems about ft and rt                                                *)
   13.87 -(* ----------------------------------------------------------------------- *)
   13.88 -
   13.89 -section "ft & rt";
   13.90 -
   13.91 -(*
   13.92 -Goal "ft$s=UU --> s=UU";
   13.93 -by (stream_case_tac "s" 1);
   13.94 -by (REPEAT (asm_simp_tac (simpset() addsimps stream.rews) 1));
   13.95 -qed "stream_ft_lemma1";
   13.96 -*)
   13.97 -
   13.98 -Goal "s~=UU ==> ft$s~=UU";
   13.99 -by (stream_case_tac "s" 1);
  13.100 -by  (Blast_tac 1);
  13.101 -by (Asm_simp_tac 1);
  13.102 -qed "ft_defin";
  13.103 -
  13.104 -Goal "rt$s~=UU ==> s~=UU";
  13.105 -by Auto_tac;
  13.106 -qed "rt_strict_rev";
  13.107 -
  13.108 -Goal "(ft$s)&&(rt$s)=s";
  13.109 -by (stream_case_tac "s" 1);
  13.110 -by (ALLGOALS Asm_simp_tac);
  13.111 -qed "surjectiv_scons";
  13.112 -
  13.113 -Goal "ALL x s. x << s --> iterate i rt x << iterate i rt s";
  13.114 -by (induct_tac "i" 1);
  13.115 -by (Simp_tac 1);
  13.116 -by (strip_tac 1);
  13.117 -by (stream_case_tac "x" 1);
  13.118 -by (rtac (minimal RS (monofun_iterate2 RS monofunE RS spec RS spec RS mp))1);
  13.119 -by (dtac stream_prefix 1);
  13.120 -by Safe_tac;
  13.121 -by (asm_simp_tac (HOL_ss addsimps iterate_Suc2::stream.rews) 1);
  13.122 -qed_spec_mp "monofun_rt_mult";
  13.123 -
  13.124 -			
  13.125 -
  13.126 -(* ----------------------------------------------------------------------- *)
  13.127 -(* theorems about stream_take                                              *)
  13.128 -(* ----------------------------------------------------------------------- *)
  13.129 -
  13.130 -section "stream_take";
  13.131 -
  13.132 -Goal  "(LUB i. stream_take i$s) = s";
  13.133 -by (subgoal_tac "(LUB i. stream_take i$s) = fix$stream_copy$s" 1);
  13.134 -by (simp_tac (simpset() addsimps [fix_def2, stream.take_def,
  13.135 -                                  contlub_cfun_fun, chain_iterate]) 2);
  13.136 -by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
  13.137 -qed "stream_reach2";
  13.138 -
  13.139 -Goal "chain (%i. stream_take i$s)";
  13.140 -by (rtac chainI 1);
  13.141 -by (subgoal_tac "ALL i s::'a stream. stream_take i$s << stream_take (Suc i)$s" 1);
  13.142 -by (Fast_tac 1);
  13.143 -by (rtac allI 1);
  13.144 -by (induct_tac "ia" 1);
  13.145 -by (Simp_tac 1);
  13.146 -by (rtac allI 1);
  13.147 -by (stream_case_tac "s" 1);
  13.148 -by (Simp_tac 1);
  13.149 -by (asm_simp_tac (simpset() addsimps [monofun_cfun_arg]) 1);
  13.150 -qed "chain_stream_take";
  13.151 -
  13.152 -
  13.153 -Goalw [stream.take_def]
  13.154 -	"stream_take n$x = x ==> stream_take (Suc n)$x = x";
  13.155 -by (rtac antisym_less 1);
  13.156 -by (subgoal_tac "iterate (Suc n) stream_copy UU$x << fix$stream_copy$x" 1);
  13.157 -by (asm_full_simp_tac (simpset() addsimps [stream.reach]) 1);
  13.158 -by (rtac monofun_cfun_fun 1);
  13.159 -by (stac fix_def2 1);
  13.160 -by (rtac is_ub_thelub 1);
  13.161 -by (rtac chain_iterate 1);
  13.162 -by (etac subst 1 THEN rtac monofun_cfun_fun 1);
  13.163 -by (rtac (rewrite_rule [chain_def] chain_iterate RS spec) 1);
  13.164 -qed "stream_take_more";
  13.165 -
  13.166 -(*
  13.167 -Goal 
  13.168 - "ALL  s2. stream_take n$s2 = s2 --> stream_take (Suc n)$s2=s2";
  13.169 -by (induct_tac "n" 1);
  13.170 -by (simp_tac (simpset() addsimps stream_rews) 1);
  13.171 -by (strip_tac 1);
  13.172 -by (hyp_subst_tac  1);
  13.173 -by (simp_tac (simpset() addsimps stream_rews) 1);
  13.174 -by (rtac allI 1);
  13.175 -by (res_inst_tac [("s","s2")] streamE 1);
  13.176 -by (asm_simp_tac (simpset() addsimps stream_rews) 1);
  13.177 -by (asm_simp_tac (simpset() addsimps stream_rews) 1);
  13.178 -by (strip_tac 1 );
  13.179 -by (subgoal_tac "stream_take n1$xs = xs" 1);
  13.180 -by (rtac ((hd stream_inject) RS conjunct2) 2);
  13.181 -by (atac 4);
  13.182 -by (atac 2);
  13.183 -by (atac 2);
  13.184 -by (rtac cfun_arg_cong 1);
  13.185 -by (Blast_tac 1);
  13.186 -qed "stream_take_lemma2";
  13.187 -*)
  13.188 -
  13.189 -Goal 
  13.190 -"ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs";
  13.191 -by (induct_tac "n" 1);
  13.192 -by (Asm_simp_tac 1);
  13.193 -by (strip_tac 1);
  13.194 -by (res_inst_tac [("P","x && xs=UU")] notE 1);
  13.195 -by (eresolve_tac stream.con_rews 1);
  13.196 -by (etac sym 1);
  13.197 -by (strip_tac 1);
  13.198 -by (rtac stream_take_more 1);
  13.199 -by (res_inst_tac [("a1","x")] ((hd stream.injects) RS conjunct2) 1);
  13.200 -by (assume_tac 3);
  13.201 -by (etac (hd(tl(tl(stream.take_rews))) RS subst) 1);
  13.202 -by (atac 1);
  13.203 -qed_spec_mp "stream_take_lemma3";
  13.204 -
  13.205 -Goal 
  13.206 - "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs";
  13.207 -by (induct_tac "n" 1);
  13.208 -by Auto_tac;  
  13.209 -qed_spec_mp "stream_take_lemma4";
  13.210 -
  13.211 -
  13.212 -(* ------------------------------------------------------------------------- *)
  13.213 -(* special induction rules                                                   *)
  13.214 -(* ------------------------------------------------------------------------- *)
  13.215 -
  13.216 -section "induction";
  13.217 -
  13.218 -
  13.219 -val prems = Goalw [stream.finite_def]
  13.220 - "[| stream_finite x;  \
  13.221 -\    P UU; \
  13.222 -\    !!a s. [| a ~= UU; P s |] \
  13.223 -\ ==> P (a && s) |] ==> P x";
  13.224 -by (cut_facts_tac prems 1);
  13.225 -by (etac exE 1);
  13.226 -by (etac subst 1);
  13.227 -by (rtac stream.finite_ind 1);
  13.228 -by (atac 1);
  13.229 -by (eresolve_tac prems 1);
  13.230 -by (atac 1);
  13.231 -qed "stream_finite_ind";
  13.232 -
  13.233 -val major::prems = Goal
  13.234 -"[| P UU;\
  13.235 -\   !! x    .    x ~= UU                  ==> P (x      && UU); \
  13.236 -\   !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )  \
  13.237 -\   |] ==> !s. P (stream_take n$s)";
  13.238 -by (res_inst_tac [("n","n")] nat_induct2 1);
  13.239 -by (asm_simp_tac (simpset() addsimps [major]) 1);
  13.240 -by (rtac allI 1);
  13.241 -by (stream_case_tac "s" 1);
  13.242 -by (asm_simp_tac (simpset() addsimps [major]) 1);
  13.243 -by (asm_simp_tac (simpset() addsimps prems) 1);
  13.244 -by (rtac allI 1);
  13.245 -by (stream_case_tac "s" 1);
  13.246 -by (asm_simp_tac (simpset() addsimps [major]) 1);
  13.247 -by (res_inst_tac [("x","sa")] stream.casedist 1);
  13.248 -by (asm_simp_tac (simpset() addsimps prems) 1);
  13.249 -by (asm_simp_tac (simpset() addsimps prems) 1);
  13.250 -qed "stream_finite_ind2";
  13.251 -
  13.252 -
  13.253 -val prems = Goal
  13.254 -"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); \
  13.255 -\   !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s)\
  13.256 -\ |] ==> P x";
  13.257 -by (rtac (stream.reach RS subst) 1);
  13.258 -by (rtac (adm_impl_admw RS wfix_ind) 1);
  13.259 -by (rtac adm_subst 1);
  13.260 -by (cont_tacR 1);
  13.261 -by (resolve_tac prems 1);
  13.262 -by (rtac allI 1);
  13.263 -by (rtac (rewrite_rule [stream.take_def] stream_finite_ind2 RS spec) 1);
  13.264 -by (resolve_tac prems 1);
  13.265 -by (eresolve_tac prems 1);
  13.266 -by (eresolve_tac prems 1);
  13.267 -by (atac 1);
  13.268 -by (atac 1);
  13.269 -qed "stream_ind2";
  13.270 -
  13.271 -
  13.272 -(* ----------------------------------------------------------------------- *)
  13.273 -(* simplify use of coinduction                                             *)
  13.274 -(* ----------------------------------------------------------------------- *)
  13.275 -
  13.276 -section "coinduction";
  13.277 -
  13.278 -
  13.279 -Goalw [stream.bisim_def]
  13.280 -"!s1 s2. R s1 s2 --> ft$s1 = ft$s2 &  R (rt$s1) (rt$s2) ==> stream_bisim R";
  13.281 -by (strip_tac 1);
  13.282 -by (etac allE 1);
  13.283 -by (etac allE 1);
  13.284 -by (dtac mp 1);
  13.285 -by (atac 1);
  13.286 -by (etac conjE 1);
  13.287 -by (case_tac "x = UU & x' = UU" 1);
  13.288 -by (rtac disjI1 1);
  13.289 -by (Blast_tac 1);
  13.290 -by (rtac disjI2 1);
  13.291 -by (rtac disjE 1);
  13.292 -by (etac (de_Morgan_conj RS subst) 1);
  13.293 -by (res_inst_tac [("x","ft$x")] exI 1);
  13.294 -by (res_inst_tac [("x","rt$x")] exI 1);
  13.295 -by (res_inst_tac [("x","rt$x'")] exI 1);
  13.296 -by (rtac conjI 1);
  13.297 -by (etac ft_defin 1);
  13.298 -by (asm_simp_tac (simpset() addsimps [surjectiv_scons]) 1);
  13.299 -by (eres_inst_tac [("s","ft$x"),("t","ft$x'")] subst 1);
  13.300 -by (simp_tac (simpset() addsimps [surjectiv_scons]) 1);
  13.301 -by (res_inst_tac [("x","ft$x'")] exI 1);
  13.302 -by (res_inst_tac [("x","rt$x")] exI 1);
  13.303 -by (res_inst_tac [("x","rt$x'")] exI 1);
  13.304 -by (rtac conjI 1);
  13.305 -by (etac ft_defin 1);
  13.306 -by (asm_simp_tac (simpset() addsimps [surjectiv_scons]) 1);
  13.307 -by (res_inst_tac [("s","ft$x"),("t","ft$x'")] ssubst 1);
  13.308 -by (etac sym 1);
  13.309 -by (simp_tac (simpset() addsimps [surjectiv_scons]) 1);
  13.310 -qed "stream_coind_lemma2";
  13.311 -
  13.312 -(* ----------------------------------------------------------------------- *)
  13.313 -(* theorems about stream_finite                                            *)
  13.314 -(* ----------------------------------------------------------------------- *)
  13.315 -
  13.316 -section "stream_finite";
  13.317 -
  13.318 -
  13.319 -Goalw [stream.finite_def] "stream_finite UU";
  13.320 -by (rtac exI 1);
  13.321 -by (Simp_tac 1);
  13.322 -qed "stream_finite_UU";
  13.323 -
  13.324 -Goal  "~  stream_finite s ==> s ~= UU";
  13.325 -by (blast_tac (claset() addIs [stream_finite_UU]) 1);
  13.326 -qed "stream_finite_UU_rev";
  13.327 -
  13.328 -Goalw [stream.finite_def] "stream_finite xs ==> stream_finite (x && xs)";
  13.329 -by (blast_tac (claset() addIs [stream_take_lemma4]) 1);
  13.330 -qed "stream_finite_lemma1";
  13.331 -
  13.332 -Goalw [stream.finite_def]
  13.333 - "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs";
  13.334 -by (blast_tac (claset() addIs [stream_take_lemma3]) 1);
  13.335 -qed "stream_finite_lemma2";
  13.336 -
  13.337 -Goal "stream_finite (rt$s) = stream_finite s";
  13.338 -by (stream_case_tac "s" 1);
  13.339 -by (simp_tac (simpset() addsimps [stream_finite_UU]) 1);
  13.340 -by (Asm_simp_tac 1);
  13.341 -by (fast_tac (claset() addIs [stream_finite_lemma1] 
  13.342 -                       addDs [stream_finite_lemma2]) 1);
  13.343 -qed "stream_finite_rt_eq";
  13.344 -
  13.345 -Goal "stream_finite s ==> !t. t<<s --> stream_finite t";
  13.346 -by (eres_inst_tac [("x","s")] stream_finite_ind 1);
  13.347 -by (strip_tac 1); 
  13.348 -by (dtac UU_I 1);
  13.349 -by (asm_simp_tac (simpset() addsimps [stream_finite_UU]) 1);
  13.350 -by (strip_tac 1);
  13.351 -by (asm_full_simp_tac (simpset() addsimps [stream_prefix']) 1);
  13.352 -by (fast_tac (claset() addSIs [stream_finite_UU, stream_finite_lemma1]) 1);
  13.353 -qed_spec_mp "stream_finite_less";
  13.354 -
  13.355 -Goal "adm (%x. ~  stream_finite x)";
  13.356 -by (rtac admI2 1);
  13.357 -by (best_tac (claset() addIs [stream_finite_less, is_ub_thelub]) 1);
  13.358 -qed "adm_not_stream_finite";
  13.359 -
  13.360 -section "smap";
  13.361 -
  13.362 -bind_thm ("smap_unfold", fix_prover2 thy smap_def 
  13.363 -	"smap = (\\<Lambda> f s. case s of x && l => f\\<cdot>x && smap\\<cdot>f\\<cdot>l)");
  13.364 -
  13.365 -Goal "smap\\<cdot>f\\<cdot>\\<bottom> = \\<bottom>";
  13.366 -by (stac smap_unfold 1);
  13.367 -by (Simp_tac 1);
  13.368 -qed "smap_empty";
  13.369 -
  13.370 -Goal "x~=\\<bottom> ==> smap\\<cdot>f\\<cdot>(x&&xs) = (f\\<cdot>x)&&(smap\\<cdot>f\\<cdot>xs)";
  13.371 -by (rtac trans 1);
  13.372 -by  (stac smap_unfold 1);
  13.373 -by  (Asm_simp_tac 1);
  13.374 -by (rtac refl 1);
  13.375 -qed "smap_scons";
  13.376 -
  13.377 -Addsimps [smap_empty, smap_scons];
  13.378 -
  13.379 -(* ------------------------------------------------------------------------- *)
  13.380 -
  13.381 -section "slen";
  13.382 -
  13.383 -Goalw [slen_def, stream.finite_def] "#\\<bottom> = 0";
  13.384 -by (Simp_tac 1);
  13.385 -by (stac Least_equality 1);
  13.386 -by    Auto_tac;
  13.387 -by (simp_tac(simpset() addsimps [thm "Fin_0"]) 1);
  13.388 -qed "slen_empty";
  13.389 -
  13.390 -Goalw [slen_def] "x ~= \\<bottom> ==> #(x&&xs) = iSuc (#xs)";
  13.391 -by (res_inst_tac [("Q1","stream_finite (x && xs)")] (split_if RS iffD2) 1);
  13.392 -by Safe_tac;
  13.393 -by (rtac (split_if RS iffD2) 2);
  13.394 -by  Safe_tac;
  13.395 -by   (fast_tac (claset() addIs [stream_finite_lemma1]) 2);
  13.396 -by  (rtac (thm "iSuc_Infty" RS sym) 2);
  13.397 -by (rtac (split_if RS iffD2) 1);
  13.398 -by (Simp_tac 1);
  13.399 -by Safe_tac;
  13.400 -by  (eatac stream_finite_lemma2 1 2);
  13.401 -by (rewtac stream.finite_def);
  13.402 -by (Clarify_tac 1);
  13.403 -by (eatac Least_Suc2 1 1);
  13.404 -by  (rtac not_sym 1);
  13.405 -by  Auto_tac;
  13.406 -qed "slen_scons"; 
  13.407 -
  13.408 -Addsimps [slen_empty, slen_scons];
  13.409 -
  13.410 -Goal "(#x < Fin (Suc 0)) = (x = UU)";
  13.411 -by (stream_case_tac "x" 1);
  13.412 -by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
  13.413 - [thm "Fin_0", thm "iSuc_Fin" RS sym, thm "i0_iless_iSuc", thm "iSuc_mono"]));
  13.414 -qed "slen_less_1_eq";
  13.415 -
  13.416 -Goal "(#x = 0) = (x = \\<bottom>)";
  13.417 -by Auto_tac;
  13.418 -by (stream_case_tac "x" 1);
  13.419 -by (rotate_tac ~1 2);
  13.420 -by Auto_tac;
  13.421 -qed "slen_empty_eq";
  13.422 -
  13.423 -Goal "(Fin (Suc n) < #x) = (? a y. x = a && y &  a ~= \\<bottom> &  Fin n < #y)";
  13.424 -by (stream_case_tac "x" 1);
  13.425 -by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps
  13.426 -                [thm "iSuc_Fin" RS sym, thm "iSuc_mono"]));
  13.427 -by  (dtac sym 1);
  13.428 -by  Auto_tac;
  13.429 -qed "slen_scons_eq";
  13.430 -
  13.431 -
  13.432 -Goal "#x = iSuc n --> (? a y. x = a&&y &  a ~= \\<bottom> &  #y = n)";
  13.433 -by (stream_case_tac "x" 1);
  13.434 -by Auto_tac;
  13.435 -qed_spec_mp "slen_iSuc";
  13.436 -
  13.437 -
  13.438 -Goal 
  13.439 -"(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \\<bottom> |  #y < Fin (Suc n))";
  13.440 -by (stac (thm "iSuc_Fin" RS sym) 1);
  13.441 -by (stac (thm "iSuc_Fin" RS sym) 1);
  13.442 -by (safe_tac HOL_cs);
  13.443 -by  (rotate_tac ~1 1);
  13.444 -by  (asm_full_simp_tac (HOL_ss addsimps [slen_scons, thm "iSuc_mono"]) 1);
  13.445 -by  (Asm_full_simp_tac 1);
  13.446 -by (stream_case_tac "x" 1);
  13.447 -by ( simp_tac (HOL_ss addsimps [slen_empty, thm "i0_iless_iSuc"]) 1);
  13.448 -by (asm_simp_tac (HOL_ss addsimps [slen_scons, thm "iSuc_mono"]) 1);
  13.449 -by (etac allE 1);
  13.450 -by (etac allE 1);
  13.451 -by (safe_tac HOL_cs);
  13.452 -by (  contr_tac 2);
  13.453 -by ( fast_tac HOL_cs 1);
  13.454 -by (Asm_full_simp_tac 1);
  13.455 -qed "slen_scons_eq_rev";
  13.456 -
  13.457 -Goal "!x. (Fin n < #x) = (stream_take n\\<cdot>x ~= x)";
  13.458 -by (induct_tac "n" 1);
  13.459 -by  (simp_tac(simpset() addsimps [slen_empty_eq, thm "Fin_0"]) 1);
  13.460 -by  (Fast_tac 1);
  13.461 -by (rtac allI 1);
  13.462 -by (asm_simp_tac (simpset() addsimps [slen_scons_eq]) 1);
  13.463 -by (etac thin_rl 1);
  13.464 -by (safe_tac HOL_cs);
  13.465 -by  (Asm_full_simp_tac 1);
  13.466 -by (stream_case_tac "x" 1);
  13.467 -by (rotate_tac ~1 2);
  13.468 -by Auto_tac;
  13.469 -qed_spec_mp "slen_take_eq";
  13.470 -
  13.471 -Goalw [thm "ile_def"] "(#x <= Fin n) = (stream_take n\\<cdot>x = x)";
  13.472 -by (simp_tac (simpset() addsimps [slen_take_eq]) 1);
  13.473 -qed "slen_take_eq_rev";
  13.474 -
  13.475 -Goal "#x = Fin n ==> stream_take n\\<cdot>x = x";
  13.476 -by (asm_simp_tac (simpset() addsimps [slen_take_eq_rev RS sym]) 1);
  13.477 -qed "slen_take_lemma1";
  13.478 -
  13.479 -Goal "!x. ~stream_finite x --> #(stream_take i\\<cdot>x) = Fin i";
  13.480 -by (induct_tac "i" 1);
  13.481 -by  (simp_tac(simpset() addsimps [thm "Fin_0"]) 1);
  13.482 -by (rtac allI 1);
  13.483 -by (stream_case_tac "x" 1);
  13.484 -by  (auto_tac (claset()addSIs [stream_finite_lemma1], simpset() delsimps [thm "iSuc_Fin"] addsimps [thm "iSuc_Fin" RS sym]));
  13.485 -by (force_tac (claset(), simpset() addsimps [stream.finite_def]) 1);
  13.486 -qed_spec_mp "slen_take_lemma2";
  13.487 -
  13.488 -Goal "stream_finite x = (#x ~= Infty)";
  13.489 -by (rtac iffI 1);
  13.490 -by  (etac stream_finite_ind 1);
  13.491 -by   (Simp_tac 1);
  13.492 -by  (etac (slen_scons RS ssubst) 1);
  13.493 -by  (stac (thm "iSuc_Infty" RS sym) 1);
  13.494 -by  (etac contrapos_nn 1);
  13.495 -by  (etac (thm "iSuc_inject" RS iffD1) 1);
  13.496 -by (case_tac "#x" 1);
  13.497 -by (auto_tac (claset()addSDs [slen_take_lemma1],
  13.498 -        simpset() addsimps [stream.finite_def]));
  13.499 -qed "slen_infinite";
  13.500 -
  13.501 -Goal "s << t ==> #s <= #t";
  13.502 -by (case_tac "stream_finite t" 1);
  13.503 -by  (EVERY'[dtac (slen_infinite RS subst), dtac notnotD] 2);
  13.504 -by  (Asm_simp_tac 2);
  13.505 -by (etac rev_mp 1);
  13.506 -by (res_inst_tac [("x","s")] allE 1);
  13.507 -by  (atac 2);
  13.508 -by (etac (stream_finite_ind) 1);
  13.509 -by  (Simp_tac 1);
  13.510 -by (rtac allI 1);
  13.511 -by (stream_case_tac "x" 1);
  13.512 -by  (asm_simp_tac (HOL_ss addsimps [slen_empty, thm "i0_lb"]) 1);
  13.513 -by (asm_simp_tac (HOL_ss addsimps [slen_scons]) 1);
  13.514 -by (fast_tac(claset() addSIs [thm "iSuc_ile_mono" RS iffD2] addSDs stream.inverts) 1);
  13.515 -qed "slen_mono";
  13.516 -
  13.517 -Goal "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> \
  13.518 -\ stream_take n\\<cdot>x = stream_take n\\<cdot>y";
  13.519 -by (induct_tac "n" 1);
  13.520 -by ( simp_tac(simpset() addsimps [slen_empty_eq]) 1);
  13.521 -by (strip_tac 1);
  13.522 -by (stream_case_tac "x" 1);
  13.523 -by  (asm_full_simp_tac (HOL_ss addsimps [slen_empty, 
  13.524 -              thm "iSuc_Fin" RS sym, thm "not_iSuc_ilei0"]) 1);
  13.525 -by (fatac stream_prefix 1 1);
  13.526 -by (safe_tac (claset() addSDs [stream_flat_prefix]));
  13.527 -by (Simp_tac 1);
  13.528 -by (rtac cfun_arg_cong 1);
  13.529 -by (rotate_tac 3 1);
  13.530 -by (asm_full_simp_tac (simpset() delsimps [thm "iSuc_Fin"] addsimps 
  13.531 -        [thm "iSuc_Fin" RS sym, thm "iSuc_ile_mono"]) 1);
  13.532 -qed_spec_mp "slen_take_lemma3";
  13.533 -
  13.534 -Goal "stream_finite t ==> \
  13.535 -\!s. #(s::'a::flat stream) = #t &  s << t --> s = t";
  13.536 -by (etac stream_finite_ind 1);
  13.537 -by  (fast_tac (claset() addDs [eq_UU_iff RS iffD2]) 1);
  13.538 -by Safe_tac;
  13.539 -by (stream_case_tac "sa" 1);
  13.540 -by  (dtac sym 1);
  13.541 -by  (Asm_full_simp_tac 1);
  13.542 -by (safe_tac (claset() addSDs [stream_flat_prefix]));
  13.543 -by (rtac cfun_arg_cong 1);
  13.544 -by (etac allE 1);
  13.545 -by (etac mp 1);
  13.546 -by (Asm_full_simp_tac 1);
  13.547 -qed "slen_strict_mono_lemma";
  13.548 -
  13.549 -Goal "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t";
  13.550 -by (rtac (thm "ilessI1") 1);
  13.551 -by  (etac slen_mono 1);
  13.552 -by (dtac slen_strict_mono_lemma 1);
  13.553 -by (Fast_tac 1);
  13.554 -qed "slen_strict_mono";
  13.555 -
  13.556 -Goal "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i rt x)";
  13.557 -by (induct_tac "i" 1);
  13.558 -by  (Simp_tac 1);
  13.559 -by (strip_tac 1);
  13.560 -by (stream_case_tac "x" 1);
  13.561 -by  (asm_full_simp_tac (simpset() delsimps [thm "iSuc_Fin"] 
  13.562 -             addsimps [thm "iSuc_Fin" RS sym]) 1);
  13.563 -by (stac iterate_Suc2 1);
  13.564 -by (rotate_tac 2 1);
  13.565 -by (asm_full_simp_tac  (simpset() delsimps [thm "iSuc_Fin"] 
  13.566 -    addsimps [thm "iSuc_Fin" RS sym, thm "iSuc_ile_mono"]) 1);
  13.567 -qed_spec_mp "slen_rt_mult";
  13.568 -
  13.569 -
  13.570 -(* ------------------------------------------------------------------------- *)
  13.571 -
  13.572 -section "sfilter";
  13.573 -
  13.574 -bind_thm ("sfilter_unfold", fix_prover2 thy sfilter_def 
  13.575 -	"sfilter = (\\<Lambda> p s. case s of x && xs => \
  13.576 -\  If p\\<cdot>x then x && sfilter\\<cdot>p\\<cdot>xs else sfilter\\<cdot>p\\<cdot>xs fi)");
  13.577 -
  13.578 -Goal "sfilter\\<cdot>\\<bottom> = \\<bottom>";
  13.579 -by (rtac ext_cfun 1);
  13.580 -by (stac sfilter_unfold 1);
  13.581 -by (stream_case_tac "x" 1);
  13.582 -by  Auto_tac;
  13.583 -qed "strict_sfilter";
  13.584 -
  13.585 -Goal "sfilter\\<cdot>f\\<cdot>\\<bottom> = \\<bottom>";
  13.586 -by (stac sfilter_unfold 1);
  13.587 -by (Simp_tac 1);
  13.588 -qed "sfilter_empty";
  13.589 -
  13.590 -Goal "x ~= \\<bottom> ==> sfilter\\<cdot>f\\<cdot>(x && xs) = \
  13.591 -\ If f\\<cdot>x then x && sfilter\\<cdot>f\\<cdot>xs else sfilter\\<cdot>f\\<cdot>xs fi";
  13.592 -by (rtac trans 1);
  13.593 -by (stac sfilter_unfold 1);
  13.594 -by (Asm_simp_tac 1);
  13.595 -by (rtac refl 1);
  13.596 -qed "sfilter_scons";
  13.597 -
    14.1 --- a/src/HOLCF/ex/Stream.thy	Tue Sep 07 15:59:16 2004 +0200
    14.2 +++ b/src/HOLCF/ex/Stream.thy	Tue Sep 07 16:02:42 2004 +0200
    14.3 @@ -1,29 +1,1012 @@
    14.4  (*  Title: 	HOLCF/ex/Stream.thy
    14.5      ID:         $Id$
    14.6 -    Author: 	Franz Regensburger, David von Oheimb
    14.7 +    Author: 	Franz Regensburger, David von Oheimb, Borislav Gajanovic
    14.8  
    14.9  General Stream domain.
   14.10 -TODO: should be integrated with HOLCF/Streams
   14.11  *)
   14.12  
   14.13 -Stream = HOLCF + Nat_Infinity +
   14.14 +theory Stream = HOLCF + Nat_Infinity:
   14.15  
   14.16 -domain 'a stream = "&&" (ft::'a) (lazy rt::'a stream) (infixr 65)
   14.17 +domain 'a stream = "&&" (ft::'a) (lazy rt::"'a stream") (infixr 65)
   14.18  
   14.19  consts
   14.20  
   14.21 -  smap		:: "('a -> 'b) -> 'a stream -> 'b stream"
   14.22 -  sfilter	:: "('a -> tr) -> 'a stream -> 'a stream"
   14.23 -  slen		:: "'a stream => inat"			("#_" [1000] 1000)
   14.24 +  smap		:: "('a \<rightarrow> 'b) \<rightarrow> 'a stream \<rightarrow> 'b stream"
   14.25 +  sfilter	:: "('a \<rightarrow> tr) \<rightarrow> 'a stream \<rightarrow> 'a stream"
   14.26 +  slen		:: "'a stream \<Rightarrow> inat"			("#_" [1000] 1000)
   14.27  
   14.28  defs
   14.29  
   14.30 -  smap_def	"smap	 == fix\\<cdot>(\\<Lambda> h f s. case s of x && xs => f\\<cdot>x && h\\<cdot>f\\<cdot>xs)"
   14.31 -  sfilter_def	"sfilter == fix\\<cdot>(\\<Lambda> h p s. case s of x && xs => 
   14.32 -				     If p\\<cdot>x then x && h\\<cdot>p\\<cdot>xs else h\\<cdot>p\\<cdot>xs fi)"
   14.33 -  slen_def	"#s == if stream_finite s 
   14.34 -		      then Fin (LEAST n. stream_take n\\<cdot>s = s) else \\<infinity>"
   14.35 +  smap_def:	"smap	 \<equiv> fix\<cdot>(\<Lambda> h f s. case s of x && xs \<Rightarrow> f\<cdot>x && h\<cdot>f\<cdot>xs)"
   14.36 +  sfilter_def:	"sfilter \<equiv> fix\<cdot>(\<Lambda> h p s. case s of x && xs \<Rightarrow> 
   14.37 +				     If p\<cdot>x then x && h\<cdot>p\<cdot>xs else h\<cdot>p\<cdot>xs fi)"
   14.38 +  slen_def:	"#s \<equiv> if stream_finite s 
   14.39 +		      then Fin (LEAST n. stream_take n\<cdot>s = s) else \<infinity>"
   14.40 +
   14.41 +(* concatenation *)
   14.42 +
   14.43 +consts
   14.44 + 
   14.45 +  i_rt :: "nat => 'a stream => 'a stream" (* chops the first i elements *)
   14.46 +  i_th :: "nat => 'a stream => 'a"        (* the i-th element *)
   14.47 +
   14.48 +  sconc         :: "'a stream => 'a stream => 'a stream" (infixr "ooo" 65) 
   14.49 +  constr_sconc  :: "'a stream => 'a stream => 'a stream" (* constructive *)
   14.50 +  constr_sconc' :: "nat => 'a stream => 'a stream => 'a stream" 
   14.51 +
   14.52 +defs
   14.53 +  i_rt_def: "i_rt == %i s. iterate i rt s"  
   14.54 +  i_th_def: "i_th == %i s. ft$(i_rt i s)" 
   14.55 +
   14.56 +  sconc_def: "s1 ooo s2 == case #s1 of 
   14.57 +                       Fin n \<Rightarrow> (SOME s. (stream_take n$s=s1) & (i_rt n s = s2))
   14.58 +                     | \<infinity>     \<Rightarrow> s1" 
   14.59 +
   14.60 +  constr_sconc_def: "constr_sconc s1 s2 == case #s1 of 
   14.61 +                                             Fin n \<Rightarrow> constr_sconc' n s1 s2 
   14.62 +                                           | \<infinity>    \<Rightarrow> s1"
   14.63 +primrec 
   14.64 +  constr_sconc'_0:   "constr_sconc' 0 s1 s2 = s2"
   14.65 +  constr_sconc'_Suc: "constr_sconc' (Suc n) s1 s2 = ft$s1 && 
   14.66 +                                                    constr_sconc' n (rt$s1) s2"
   14.67 +
   14.68 +
   14.69 +declare stream.rews [simp add]
   14.70 +
   14.71 +(* ----------------------------------------------------------------------- *)
   14.72 +(* theorems about scons                                                    *)
   14.73 +(* ----------------------------------------------------------------------- *)
   14.74 +
   14.75 +
   14.76 +section "scons"
   14.77 +
   14.78 +lemma scons_eq_UU: "(a && s = UU) = (a = UU)"
   14.79 +by (auto, erule contrapos_pp, simp)
   14.80 +
   14.81 +lemma scons_not_empty: "[| a && x = UU; a ~= UU |] ==> R"
   14.82 +by auto
   14.83 +
   14.84 +lemma stream_exhaust_eq: "(x ~= UU) = (EX a y. a ~= UU &  x = a && y)"
   14.85 +by (auto,insert stream.exhaust [of x],auto)
   14.86 +
   14.87 +lemma stream_neq_UU: "x~=UU ==> EX a as. x=a&&as & a~=UU"
   14.88 +by (simp add: stream_exhaust_eq,auto)
   14.89 +
   14.90 +lemma stream_inject_eq [simp]:
   14.91 +  "[| a ~= UU; b ~= UU |] ==> (a && s = b && t) = (a = b &  s = t)"
   14.92 +by (insert stream.injects [of a s b t], auto)
   14.93 +
   14.94 +lemma stream_prefix: 
   14.95 +  "[| a && s << t; a ~= UU  |] ==> EX b tt. t = b && tt &  b ~= UU &  s << tt"
   14.96 +apply (insert stream.exhaust [of t], auto)
   14.97 +apply (drule eq_UU_iff [THEN iffD2], simp)
   14.98 +by (drule stream.inverts, auto)
   14.99 +
  14.100 +lemma stream_prefix': 
  14.101 +  "b ~= UU ==> x << b && z = 
  14.102 +   (x = UU |  (EX a y. x = a && y &  a ~= UU &  a << b &  y << z))"
  14.103 +apply (case_tac "x=UU",auto)
  14.104 +apply (drule stream_exhaust_eq [THEN iffD1],auto)
  14.105 +apply (drule stream.inverts,auto)
  14.106 +by (intro monofun_cfun,auto)
  14.107 +
  14.108 +(*
  14.109 +lemma stream_prefix1: "[| x<<y; xs<<ys |] ==> x&&xs << y&&ys"
  14.110 +by (insert stream_prefix' [of y "x&&xs" ys],force)
  14.111 +*)
  14.112 +
  14.113 +lemma stream_flat_prefix: 
  14.114 +  "[| x && xs << y && ys; (x::'a::flat) ~= UU|] ==> x = y & xs << ys"
  14.115 +apply (case_tac "y=UU",auto)
  14.116 +apply (drule eq_UU_iff [THEN iffD2],auto)
  14.117 +apply (drule stream.inverts,auto)
  14.118 +apply (drule ax_flat [rule_format],simp)
  14.119 +by (drule stream.inverts,auto)
  14.120 +
  14.121 +
  14.122 +
  14.123 +(* ----------------------------------------------------------------------- *)
  14.124 +(* theorems about stream_when                                              *)
  14.125 +(* ----------------------------------------------------------------------- *)
  14.126 +
  14.127 +section "stream_when"
  14.128 +
  14.129 +
  14.130 +lemma stream_when_strictf: "stream_when$UU$s=UU"
  14.131 +by (rule stream.casedist [of s], auto)
  14.132 +
  14.133 +
  14.134 +
  14.135 +(* ----------------------------------------------------------------------- *)
  14.136 +(* theorems about ft and rt                                                *)
  14.137 +(* ----------------------------------------------------------------------- *)
  14.138 +
  14.139 +
  14.140 +section "ft & rt"
  14.141 +
  14.142 +
  14.143 +lemma ft_defin: "s~=UU ==> ft$s~=UU"
  14.144 +by (drule stream_exhaust_eq [THEN iffD1],auto)
  14.145 +
  14.146 +lemma rt_strict_rev: "rt$s~=UU ==> s~=UU"
  14.147 +by auto
  14.148 +
  14.149 +lemma surjectiv_scons: "(ft$s)&&(rt$s)=s"
  14.150 +by (rule stream.casedist [of s], auto)
  14.151 +
  14.152 +lemma monofun_rt_mult: "x << s ==> iterate i rt x << iterate i rt s"
  14.153 +by (insert monofun_iterate2 [of i "rt"], simp add: monofun, auto)
  14.154 +
  14.155 +
  14.156 +
  14.157 +(* ----------------------------------------------------------------------- *)
  14.158 +(* theorems about stream_take                                              *)
  14.159 +(* ----------------------------------------------------------------------- *)
  14.160 +
  14.161 +
  14.162 +section "stream_take";
  14.163 +
  14.164 +
  14.165 +lemma stream_reach2: "(LUB i. stream_take i$s) = s"
  14.166 +apply (insert stream.reach [of s], erule subst) back
  14.167 +apply (simp add: fix_def2 stream.take_def)
  14.168 +apply (insert contlub_cfun_fun [of "%i. iterate i stream_copy UU" s,THEN sym])
  14.169 +by (simp add: chain_iterate)
  14.170 +
  14.171 +lemma chain_stream_take: "chain (%i. stream_take i$s)"
  14.172 +apply (rule chainI) 
  14.173 +apply (rule monofun_cfun_fun)
  14.174 +apply (simp add: stream.take_def del: iterate_Suc)
  14.175 +by (rule chainE, simp add: chain_iterate)
  14.176 +
  14.177 +lemma stream_take_prefix [simp]: "stream_take n$s << s"
  14.178 +apply (insert stream_reach2 [of s])
  14.179 +apply (erule subst) back
  14.180 +apply (rule is_ub_thelub)
  14.181 +by (simp only: chain_stream_take)
  14.182 +
  14.183 +lemma stream_take_more [rule_format]: 
  14.184 +  "ALL x. stream_take n$x = x --> stream_take (Suc n)$x = x"
  14.185 +apply (induct_tac n,auto)
  14.186 +apply (case_tac "x=UU",auto)
  14.187 +by (drule stream_exhaust_eq [THEN iffD1],auto)
  14.188 +
  14.189 +lemma stream_take_lemma3 [rule_format]: 
  14.190 +  "ALL x xs. x~=UU --> stream_take n$(x && xs) = x && xs --> stream_take n$xs=xs"
  14.191 +apply (induct_tac n,clarsimp)
  14.192 +apply (drule sym, erule scons_not_empty, simp)
  14.193 +apply (clarify, rule stream_take_more)
  14.194 +apply (erule_tac x="x" in allE)
  14.195 +by (erule_tac x="xs" in allE,simp)
  14.196 +
  14.197 +lemma stream_take_lemma4: 
  14.198 +  "ALL x xs. stream_take n$xs=xs --> stream_take (Suc n)$(x && xs) = x && xs"
  14.199 +by auto
  14.200 +
  14.201 +lemma stream_take_idempotent [rule_format, simp]: 
  14.202 + "ALL s. stream_take n$(stream_take n$s) = stream_take n$s"
  14.203 +apply (induct_tac n, auto)
  14.204 +apply (case_tac "s=UU", auto)
  14.205 +by (drule stream_exhaust_eq [THEN iffD1], auto)
  14.206 +
  14.207 +lemma stream_take_take_Suc [rule_format, simp]: 
  14.208 +  "ALL s. stream_take n$(stream_take (Suc n)$s) = 
  14.209 +                                    stream_take n$s"
  14.210 +apply (induct_tac n, auto)
  14.211 +apply (case_tac "s=UU", auto)
  14.212 +by (drule stream_exhaust_eq [THEN iffD1], auto)
  14.213 +
  14.214 +lemma mono_stream_take_pred: 
  14.215 +  "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
  14.216 +                       stream_take n$s1 << stream_take n$s2"
  14.217 +by (insert monofun_cfun_arg [of "stream_take (Suc n)$s1" 
  14.218 +  "stream_take (Suc n)$s2" "stream_take n"], auto)
  14.219 +(*
  14.220 +lemma mono_stream_take_pred: 
  14.221 +  "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
  14.222 +                       stream_take n$s1 << stream_take n$s2"
  14.223 +by (drule mono_stream_take [of _ _ n],simp)
  14.224 +*)
  14.225 +
  14.226 +lemma stream_take_lemma10 [rule_format]:
  14.227 +  "ALL k<=n. stream_take n$s1 << stream_take n$s2 
  14.228 +                             --> stream_take k$s1 << stream_take k$s2"
  14.229 +apply (induct_tac n,simp,clarsimp)
  14.230 +apply (case_tac "k=Suc n",blast)
  14.231 +apply (erule_tac x="k" in allE)
  14.232 +by (drule mono_stream_take_pred,simp)
  14.233 +
  14.234 +lemma stream_take_le_mono : "k<=n ==> stream_take k$s1 << stream_take n$s1"
  14.235 +apply (insert chain_stream_take [of s1])
  14.236 +by (drule chain_mono3,auto)
  14.237 +
  14.238 +lemma mono_stream_take: "s1 << s2 ==> stream_take n$s1 << stream_take n$s2"
  14.239 +by (simp add: monofun_cfun_arg)
  14.240 +
  14.241 +(*
  14.242 +lemma stream_take_prefix [simp]: "stream_take n$s << s"
  14.243 +apply (subgoal_tac "s=(LUB n. stream_take n$s)")
  14.244 + apply (erule ssubst, rule is_ub_thelub)
  14.245 + apply (simp only: chain_stream_take)
  14.246 +by (simp only: stream_reach2)
  14.247 +*)
  14.248 +
  14.249 +lemma stream_take_take_less:"stream_take k$(stream_take n$s) << stream_take k$s"
  14.250 +by (rule monofun_cfun_arg,auto)
  14.251 +
  14.252 +
  14.253 +(* ------------------------------------------------------------------------- *)
  14.254 +(* special induction rules                                                   *)
  14.255 +(* ------------------------------------------------------------------------- *)
  14.256 +
  14.257 +
  14.258 +section "induction"
  14.259 +
  14.260 +lemma stream_finite_ind: 
  14.261 + "[| stream_finite x; P UU; !!a s. [| a ~= UU; P s |] ==> P (a && s) |] ==> P x"
  14.262 +apply (simp add: stream.finite_def,auto)
  14.263 +apply (erule subst)
  14.264 +by (drule stream.finite_ind [of P _ x], auto)
  14.265 +
  14.266 +lemma stream_finite_ind2: 
  14.267 +"[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==> 
  14.268 +                                 !s. P (stream_take n$s)"
  14.269 +apply (rule nat_induct2 [of _ n],auto)
  14.270 +apply (case_tac "s=UU",clarsimp)
  14.271 +apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
  14.272 +apply (case_tac "s=UU",clarsimp)
  14.273 +apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
  14.274 +apply (case_tac "y=UU",clarsimp)
  14.275 +by (drule stream_exhaust_eq [THEN iffD1],clarsimp)
  14.276 +
  14.277 +lemma stream_ind2: 
  14.278 +"[| adm P; P UU; !!a. a ~= UU ==> P (a && UU); !!a b s. [| a ~= UU; b ~= UU; P s |] ==> P (a && b && s) |] ==> P x"
  14.279 +apply (insert stream.reach [of x],erule subst)
  14.280 +apply (frule adm_impl_admw, rule wfix_ind, auto)
  14.281 +apply (rule adm_subst [THEN adm_impl_admw],auto)
  14.282 +apply (insert stream_finite_ind2 [of P])
  14.283 +by (simp add: stream.take_def)
  14.284 +
  14.285 +
  14.286 +
  14.287 +(* ----------------------------------------------------------------------- *)
  14.288 +(* simplify use of coinduction                                             *)
  14.289 +(* ----------------------------------------------------------------------- *)
  14.290 +
  14.291 +
  14.292 +section "coinduction"
  14.293 +
  14.294 +lemma stream_coind_lemma2: "!s1 s2. R s1 s2 --> ft$s1 = ft$s2 &  R (rt$s1) (rt$s2) ==> stream_bisim R"
  14.295 +apply (simp add: stream.bisim_def,clarsimp)
  14.296 +apply (case_tac "x=UU",clarsimp)
  14.297 +apply (erule_tac x="UU" in allE,simp)
  14.298 +apply (case_tac "x'=UU",simp)
  14.299 +apply (drule stream_exhaust_eq [THEN iffD1],auto)+
  14.300 +apply (case_tac "x'=UU",auto)
  14.301 +apply (erule_tac x="a && y" in allE)
  14.302 +apply (erule_tac x="UU" in allE)+
  14.303 +apply (auto,drule stream_exhaust_eq [THEN iffD1],clarsimp)
  14.304 +apply (erule_tac x="a && y" in allE)
  14.305 +apply (erule_tac x="aa && ya" in allE)
  14.306 +by auto
  14.307 +
  14.308 +
  14.309 +
  14.310 +(* ----------------------------------------------------------------------- *)
  14.311 +(* theorems about stream_finite                                            *)
  14.312 +(* ----------------------------------------------------------------------- *)
  14.313 +
  14.314 +
  14.315 +section "stream_finite"
  14.316 +
  14.317 +lemma stream_finite_UU [simp]: "stream_finite UU"
  14.318 +by (simp add: stream.finite_def)
  14.319 +
  14.320 +lemma stream_finite_UU_rev: "~  stream_finite s ==> s ~= UU"
  14.321 +by (auto simp add: stream.finite_def)
  14.322 +
  14.323 +lemma stream_finite_lemma1: "stream_finite xs ==> stream_finite (x && xs)"
  14.324 +apply (simp add: stream.finite_def,auto)
  14.325 +apply (rule_tac x="Suc n" in exI)
  14.326 +by (simp add: stream_take_lemma4)
  14.327 +
  14.328 +lemma stream_finite_lemma2: "[| x ~= UU; stream_finite (x && xs) |] ==> stream_finite xs"
  14.329 +apply (simp add: stream.finite_def, auto)
  14.330 +apply (rule_tac x="n" in exI)
  14.331 +by (erule stream_take_lemma3,simp)
  14.332 +
  14.333 +lemma stream_finite_rt_eq: "stream_finite (rt$s) = stream_finite s"
  14.334 +apply (rule stream.casedist [of s], auto)
  14.335 +apply (rule stream_finite_lemma1, simp)
  14.336 +by (rule stream_finite_lemma2,simp)
  14.337 +
  14.338 +lemma stream_finite_less: "stream_finite s ==> !t. t<<s --> stream_finite t"
  14.339 +apply (erule stream_finite_ind [of s])
  14.340 +apply (clarsimp, drule eq_UU_iff [THEN iffD2], auto)
  14.341 +apply (case_tac "t=UU", auto)
  14.342 +apply (drule stream_exhaust_eq [THEN iffD1],auto)
  14.343 +apply (drule stream.inverts, auto)
  14.344 +apply (erule_tac x="y" in allE, simp)
  14.345 +by (rule stream_finite_lemma1, simp)
  14.346 +
  14.347 +lemma stream_take_finite [simp]: "stream_finite (stream_take n$s)"
  14.348 +apply (simp add: stream.finite_def)
  14.349 +by (rule_tac x="n" in exI,simp)
  14.350 +
  14.351 +lemma adm_not_stream_finite: "adm (%x. ~ stream_finite x)"
  14.352 +apply (rule admI2, auto)
  14.353 +apply (drule stream_finite_less,drule is_ub_thelub)
  14.354 +by auto
  14.355 +
  14.356 +
  14.357 +
  14.358 +(* ----------------------------------------------------------------------- *)
  14.359 +(* theorems about stream length                                            *)
  14.360 +(* ----------------------------------------------------------------------- *)
  14.361 +
  14.362 +
  14.363 +section "slen"
  14.364 +
  14.365 +lemma slen_empty [simp]: "#\<bottom> = 0"
  14.366 +apply (simp add: slen_def stream.finite_def)
  14.367 +by (simp add: inat_defs Least_equality)
  14.368 +
  14.369 +lemma slen_scons [simp]: "x ~= \<bottom> ==> #(x&&xs) = iSuc (#xs)"
  14.370 +apply (case_tac "stream_finite (x && xs)")
  14.371 +apply (simp add: slen_def, auto)
  14.372 +apply (simp add: stream.finite_def, auto)
  14.373 +apply (rule Least_Suc2,auto)
  14.374 +apply (drule sym)
  14.375 +apply (drule sym scons_eq_UU [THEN iffD1],simp)
  14.376 +apply (erule stream_finite_lemma2, simp)
  14.377 +apply (simp add: slen_def, auto)
  14.378 +by (drule stream_finite_lemma1,auto)
  14.379 +
  14.380 +lemma slen_less_1_eq: "(#x < Fin (Suc 0)) = (x = \<bottom>)"
  14.381 +by (rule stream.casedist [of x], auto simp del: iSuc_Fin 
  14.382 +    simp add: Fin_0 iSuc_Fin[THEN sym] i0_iless_iSuc iSuc_mono)
  14.383 +
  14.384 +lemma slen_empty_eq: "(#x = 0) = (x = \<bottom>)"
  14.385 +by (rule stream.casedist [of x], auto)
  14.386 +
  14.387 +lemma slen_scons_eq: "(Fin (Suc n) < #x) = (? a y. x = a && y &  a ~= \<bottom> &  Fin n < #y)"
  14.388 +apply (auto, case_tac "x=UU",auto)
  14.389 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
  14.390 +apply (rule_tac x="a" in exI)
  14.391 +apply (rule_tac x="y" in exI, simp)
  14.392 +by (simp add: inat_defs split:inat_splits)+
  14.393 +
  14.394 +lemma slen_iSuc: "#x = iSuc n --> (? a y. x = a&&y &  a ~= \<bottom> &  #y = n)"
  14.395 +by (rule stream.casedist [of x], auto)
  14.396 +
  14.397 +lemma slen_stream_take_finite [simp]: "#(stream_take n$s) ~= \<infinity>"
  14.398 +by (simp add: slen_def)
  14.399 +
  14.400 +lemma slen_scons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a && y |  a = \<bottom> |  #y < Fin (Suc n))"
  14.401 +apply (rule stream.casedist [of x], auto)
  14.402 +apply (drule sym, drule scons_eq_UU [THEN iffD1],auto)
  14.403 +apply (simp add: inat_defs split:inat_splits)
  14.404 +apply (subgoal_tac "s=y & aa=a",simp);
  14.405 +apply (simp add: inat_defs split:inat_splits)
  14.406 +apply (case_tac "aa=UU",auto)
  14.407 +apply (erule_tac x="a" in allE, simp)
  14.408 +by (simp add: inat_defs split:inat_splits)
  14.409 +
  14.410 +lemma slen_take_lemma4 [rule_format]: 
  14.411 +  "!s. stream_take n$s ~= s --> #(stream_take n$s) = Fin n"
  14.412 +apply (induct_tac n,auto simp add: Fin_0)
  14.413 +apply (case_tac "s=UU",simp)
  14.414 +by (drule stream_exhaust_eq [THEN iffD1], auto)
  14.415 +
  14.416 +(*
  14.417 +lemma stream_take_idempotent [simp]: 
  14.418 + "stream_take n$(stream_take n$s) = stream_take n$s"
  14.419 +apply (case_tac "stream_take n$s = s")
  14.420 +apply (auto,insert slen_take_lemma4 [of n s]);
  14.421 +by (auto,insert slen_take_lemma1 [of "stream_take n$s" n],simp)
  14.422 +
  14.423 +lemma stream_take_take_Suc [simp]: "stream_take n$(stream_take (Suc n)$s) = 
  14.424 +                                    stream_take n$s"
  14.425 +apply (simp add: po_eq_conv,auto)
  14.426 + apply (simp add: stream_take_take_less)
  14.427 +apply (subgoal_tac "stream_take n$s = stream_take n$(stream_take n$s)")
  14.428 + apply (erule ssubst)
  14.429 + apply (rule_tac monofun_cfun_arg)
  14.430 + apply (insert chain_stream_take [of s])
  14.431 +by (simp add: chain_def,simp)
  14.432 +*)
  14.433 +
  14.434 +lemma slen_take_eq: "ALL x. (Fin n < #x) = (stream_take n\<cdot>x ~= x)"
  14.435 +apply (induct_tac n, auto)
  14.436 +apply (simp add: Fin_0, clarsimp)
  14.437 +apply (drule not_sym)
  14.438 +apply (drule slen_empty_eq [THEN iffD1], simp)
  14.439 +apply (case_tac "x=UU", simp)
  14.440 +apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
  14.441 +apply (erule_tac x="y" in allE, auto)
  14.442 +apply (simp add: inat_defs split:inat_splits)
  14.443 +apply (case_tac "x=UU", simp)
  14.444 +apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
  14.445 +apply (erule_tac x="y" in allE, simp)
  14.446 +by (simp add: inat_defs split:inat_splits)
  14.447 +
  14.448 +lemma slen_take_eq_rev: "(#x <= Fin n) = (stream_take n\<cdot>x = x)"
  14.449 +by (simp add: ile_def slen_take_eq)
  14.450 +
  14.451 +lemma slen_take_lemma1: "#x = Fin n ==> stream_take n\<cdot>x = x"
  14.452 +by (rule slen_take_eq_rev [THEN iffD1], auto)
  14.453 +
  14.454 +lemma slen_rt_mono: "#s2 <= #s1 ==> #(rt$s2) <= #(rt$s1)"
  14.455 +apply (rule stream.casedist [of s1])
  14.456 + by (rule stream.casedist [of s2],simp+)+
  14.457 +
  14.458 +lemma slen_take_lemma5: "#(stream_take n$s) <= Fin n"; 
  14.459 +apply (case_tac "stream_take n$s = s")
  14.460 + apply (simp add: slen_take_eq_rev)
  14.461 +by (simp add: slen_take_lemma4)
  14.462 +
  14.463 +lemma slen_take_lemma2: "!x. ~stream_finite x --> #(stream_take i\<cdot>x) = Fin i"
  14.464 +apply (simp add: stream.finite_def, auto)
  14.465 +by (simp add: slen_take_lemma4)
  14.466 +
  14.467 +lemma slen_infinite: "stream_finite x = (#x ~= Infty)"
  14.468 +by (simp add: slen_def)
  14.469 +
  14.470 +lemma slen_mono_lemma: "stream_finite s ==> ALL t. s << t --> #s <= #t"
  14.471 +apply (erule stream_finite_ind [of s], auto)
  14.472 +apply (case_tac "t=UU", auto)
  14.473 +apply (drule eq_UU_iff [THEN iffD2])
  14.474 +apply (drule scons_eq_UU [THEN iffD2], simp)
  14.475 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
  14.476 +apply (erule_tac x="y" in allE, auto)
  14.477 +by (drule stream.inverts, auto)
  14.478 +
  14.479 +lemma slen_mono: "s << t ==> #s <= #t"
  14.480 +apply (case_tac "stream_finite t")
  14.481 +apply (frule stream_finite_less) 
  14.482 +apply (erule_tac x="s" in allE, simp)
  14.483 +apply (drule slen_mono_lemma, auto)
  14.484 +by (simp add: slen_def)
  14.485 +
  14.486 +lemma iterate_lemma: "F$(iterate n F x) = iterate n F (F$x)" 
  14.487 +by (insert iterate_Suc2 [of n F x], auto)
  14.488 +
  14.489 +lemma slen_rt_mult [rule_format]: "!x. Fin (i + j) <= #x --> Fin j <= #(iterate i rt x)"
  14.490 +apply (induct_tac i, auto)
  14.491 +apply (case_tac "x=UU", auto)
  14.492 +apply (simp add: inat_defs)
  14.493 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
  14.494 +apply (erule_tac x="y" in allE, auto)
  14.495 +apply (simp add: inat_defs split:inat_splits)
  14.496 +by (simp add: iterate_lemma)
  14.497 +
  14.498 +lemma slen_take_lemma3 [rule_format]: 
  14.499 +  "!(x::'a::flat stream) y. Fin n <= #x --> x << y --> stream_take n\<cdot>x = stream_take n\<cdot>y"
  14.500 +apply (induct_tac n, auto)
  14.501 +apply (case_tac "x=UU", auto)
  14.502 +apply (simp add: inat_defs)
  14.503 +apply (simp add: Suc_ile_eq)
  14.504 +apply (case_tac "y=UU", clarsimp)
  14.505 +apply (drule eq_UU_iff [THEN iffD2],simp)
  14.506 +apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)+
  14.507 +apply (erule_tac x="ya" in allE, simp)
  14.508 +apply (drule stream.inverts,auto)
  14.509 +by (drule ax_flat [rule_format], simp)
  14.510 +
  14.511 +lemma slen_strict_mono_lemma: 
  14.512 +  "stream_finite t ==> !s. #(s::'a::flat stream) = #t &  s << t --> s = t"
  14.513 +apply (erule stream_finite_ind, auto)
  14.514 +apply (drule eq_UU_iff [THEN iffD2], simp)
  14.515 +apply (case_tac "sa=UU", auto)
  14.516 +apply (drule stream_exhaust_eq [THEN iffD1], clarsimp)
  14.517 +apply (drule stream.inverts, simp, simp, clarsimp)
  14.518 +by (drule ax_flat [rule_format], simp)
  14.519 +
  14.520 +lemma slen_strict_mono: "[|stream_finite t; s ~= t; s << (t::'a::flat stream) |] ==> #s < #t"
  14.521 +apply (intro ilessI1, auto)
  14.522 +apply (simp add: slen_mono)
  14.523 +by (drule slen_strict_mono_lemma, auto)
  14.524 +
  14.525 +lemma stream_take_Suc_neq: "stream_take (Suc n)$s ~=s ==> 
  14.526 +                     stream_take n$s ~= stream_take (Suc n)$s"
  14.527 +apply auto
  14.528 +apply (subgoal_tac "stream_take n$s ~=s")
  14.529 + apply (insert slen_take_lemma4 [of n s],auto)
  14.530 +apply (rule stream.casedist [of s],simp)
  14.531 +apply (simp add: inat_defs split:inat_splits)
  14.532 +by (simp add: slen_take_lemma4)
  14.533 +
  14.534 +(* ----------------------------------------------------------------------- *)
  14.535 +(* theorems about smap                                                     *)
  14.536 +(* ----------------------------------------------------------------------- *)
  14.537 +
  14.538 +
  14.539 +section "smap"
  14.540 +
  14.541 +lemma smap_unfold: "smap = (\<Lambda> f t. case t of x&&xs \<Rightarrow> f$x && smap$f$xs)"
  14.542 +by (insert smap_def [THEN fix_eq2], auto)
  14.543 +
  14.544 +lemma smap_empty [simp]: "smap\<cdot>f\<cdot>\<bottom> = \<bottom>"
  14.545 +by (subst smap_unfold, simp)
  14.546 +
  14.547 +lemma smap_scons [simp]: "x~=\<bottom> ==> smap\<cdot>f\<cdot>(x&&xs) = (f\<cdot>x)&&(smap\<cdot>f\<cdot>xs)"
  14.548 +by (subst smap_unfold, force)
  14.549 +
  14.550 +
  14.551 +
  14.552 +(* ----------------------------------------------------------------------- *)
  14.553 +(* theorems about sfilter                                                  *)
  14.554 +(* ----------------------------------------------------------------------- *)
  14.555 +
  14.556 +section "sfilter"
  14.557 +
  14.558 +lemma sfilter_unfold: 
  14.559 + "sfilter = (\<Lambda> p s. case s of x && xs \<Rightarrow>
  14.560 +  If p\<cdot>x then x && sfilter\<cdot>p\<cdot>xs else sfilter\<cdot>p\<cdot>xs fi)"
  14.561 +by (insert sfilter_def [THEN fix_eq2], auto)
  14.562 +
  14.563 +lemma strict_sfilter: "sfilter\<cdot>\<bottom> = \<bottom>"
  14.564 +apply (rule ext_cfun)
  14.565 +apply (subst sfilter_unfold, auto)
  14.566 +apply (case_tac "x=UU", auto)
  14.567 +by (drule stream_exhaust_eq [THEN iffD1], auto)
  14.568 +
  14.569 +lemma sfilter_empty [simp]: "sfilter\<cdot>f\<cdot>\<bottom> = \<bottom>"
  14.570 +by (subst sfilter_unfold, force)
  14.571 +
  14.572 +lemma sfilter_scons [simp]: 
  14.573 +  "x ~= \<bottom> ==> sfilter\<cdot>f\<cdot>(x && xs) = 
  14.574 +                           If f\<cdot>x then x && sfilter\<cdot>f\<cdot>xs else sfilter\<cdot>f\<cdot>xs fi" 
  14.575 +by (subst sfilter_unfold, force)
  14.576 +
  14.577 +
  14.578 +(* ----------------------------------------------------------------------- *)
  14.579 +   section "i_rt"
  14.580 +(* ----------------------------------------------------------------------- *)
  14.581 +
  14.582 +lemma i_rt_UU [simp]: "i_rt n UU = UU"
  14.583 +apply (simp add: i_rt_def)
  14.584 +by (rule iterate.induct,auto)
  14.585 +
  14.586 +lemma i_rt_0 [simp]: "i_rt 0 s = s"
  14.587 +by (simp add: i_rt_def)
  14.588 +
  14.589 +lemma i_rt_Suc [simp]: "a ~= UU ==> i_rt (Suc n) (a&&s) = i_rt n s"
  14.590 +by (simp add: i_rt_def iterate_Suc2 del: iterate_Suc)
  14.591 +
  14.592 +lemma i_rt_Suc_forw: "i_rt (Suc n) s = i_rt n (rt$s)"
  14.593 +by (simp only: i_rt_def iterate_Suc2)
  14.594 +
  14.595 +lemma i_rt_Suc_back:"i_rt (Suc n) s = rt$(i_rt n s)"
  14.596 +by (simp only: i_rt_def,auto)
  14.597 +
  14.598 +lemma i_rt_mono: "x << s ==> i_rt n x  << i_rt n s"
  14.599 +by (simp add: i_rt_def monofun_rt_mult)
  14.600 +
  14.601 +lemma i_rt_ij_lemma: "Fin (i + j) <= #x ==> Fin j <= #(i_rt i x)"
  14.602 +by (simp add: i_rt_def slen_rt_mult)
  14.603 +
  14.604 +lemma slen_i_rt_mono: "#s2 <= #s1 ==> #(i_rt n s2) <= #(i_rt n s1)"
  14.605 +apply (induct_tac n,auto)
  14.606 +apply (simp add: i_rt_Suc_back)
  14.607 +by (drule slen_rt_mono,simp)
  14.608 +
  14.609 +lemma i_rt_take_lemma1 [rule_format]: "ALL s. i_rt n (stream_take n$s) = UU"
  14.610 +apply (induct_tac n); 
  14.611 + apply (simp add: i_rt_Suc_back,auto)
  14.612 +apply (case_tac "s=UU",auto)
  14.613 +by (drule stream_exhaust_eq [THEN iffD1],auto)
  14.614 +
  14.615 +lemma i_rt_slen: "(i_rt n s = UU) = (stream_take n$s = s)"
  14.616 +apply auto
  14.617 + apply (insert i_rt_ij_lemma [of n "Suc 0" s]);
  14.618 + apply (subgoal_tac "#(i_rt n s)=0")
  14.619 +  apply (case_tac "stream_take n$s = s",simp+)
  14.620 +  apply (insert slen_take_eq [rule_format,of n s],simp)
  14.621 +  apply (simp add: inat_defs split:inat_splits)
  14.622 + apply (simp add: slen_take_eq )
  14.623 +by (simp, insert i_rt_take_lemma1 [of n s],simp)
  14.624 +
  14.625 +lemma i_rt_lemma_slen: "#s=Fin n ==> i_rt n s = UU"
  14.626 +by (simp add: i_rt_slen slen_take_lemma1)
  14.627 +
  14.628 +lemma stream_finite_i_rt [simp]: "stream_finite (i_rt n s) = stream_finite s"
  14.629 +apply (induct_tac n, auto)
  14.630 + apply (rule stream.casedist [of "s"], auto simp del: i_rt_Suc)
  14.631 +by (simp add: i_rt_Suc_back stream_finite_rt_eq)+
  14.632 +
  14.633 +lemma take_i_rt_len_lemma: "ALL sl x j t. Fin sl = #x & n <= sl &
  14.634 +                            #(stream_take n$x) = Fin t & #(i_rt n x)= Fin j 
  14.635 +                                              --> Fin (j + t) = #x"
  14.636 +apply (induct_tac n,auto)
  14.637 + apply (simp add: inat_defs)
  14.638 +apply (case_tac "x=UU",auto)
  14.639 + apply (simp add: inat_defs)
  14.640 +apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
  14.641 +apply (subgoal_tac "EX k. Fin k = #y",clarify)
  14.642 + apply (erule_tac x="k" in allE)
  14.643 + apply (erule_tac x="y" in allE,auto)
  14.644 + apply (erule_tac x="THE p. Suc p = t" in allE,auto)
  14.645 +   apply (simp add: inat_defs split:inat_splits)
  14.646 +  apply (simp add: inat_defs split:inat_splits)
  14.647 +  apply (simp only: the_equality)
  14.648 + apply (simp add: inat_defs split:inat_splits)
  14.649 + apply force
  14.650 +by (simp add: inat_defs split:inat_splits)
  14.651 +
  14.652 +lemma take_i_rt_len: 
  14.653 +"[| Fin sl = #x; n <= sl; #(stream_take n$x) = Fin t; #(i_rt n x) = Fin j |] ==>
  14.654 +    Fin (j + t) = #x"
  14.655 +by (blast intro: take_i_rt_len_lemma [rule_format])
  14.656 +
  14.657 +
  14.658 +(* ----------------------------------------------------------------------- *)
  14.659 +   section "i_th"
  14.660 +(* ----------------------------------------------------------------------- *)
  14.661 +
  14.662 +lemma i_th_i_rt_step:
  14.663 +"[| i_th n s1 << i_th n s2; i_rt (Suc n) s1 << i_rt (Suc n) s2 |] ==> 
  14.664 +   i_rt n s1 << i_rt n s2"
  14.665 +apply (simp add: i_th_def i_rt_Suc_back)
  14.666 +apply (rule stream.casedist [of "i_rt n s1"],simp)
  14.667 +apply (rule stream.casedist [of "i_rt n s2"],auto)
  14.668 +apply (drule eq_UU_iff [THEN iffD2], simp add: scons_eq_UU)
  14.669 +by (intro monofun_cfun, auto)
  14.670 +
  14.671 +lemma i_th_stream_take_Suc [rule_format]: 
  14.672 + "ALL s. i_th n (stream_take (Suc n)$s) = i_th n s"
  14.673 +apply (induct_tac n,auto)
  14.674 + apply (simp add: i_th_def)
  14.675 + apply (case_tac "s=UU",auto)
  14.676 + apply (drule stream_exhaust_eq [THEN iffD1],auto)
  14.677 +apply (case_tac "s=UU",simp add: i_th_def)
  14.678 +apply (drule stream_exhaust_eq [THEN iffD1],auto)
  14.679 +by (simp add: i_th_def i_rt_Suc_forw)
  14.680 +
  14.681 +lemma i_th_last: "i_th n s && UU = i_rt n (stream_take (Suc n)$s)"
  14.682 +apply (insert surjectiv_scons [of "i_rt n (stream_take (Suc n)$s)"])
  14.683 +apply (rule i_th_stream_take_Suc [THEN subst])
  14.684 +apply (simp add: i_th_def  i_rt_Suc_back [symmetric])
  14.685 +by (simp add: i_rt_take_lemma1)
  14.686 +
  14.687 +lemma i_th_last_eq: 
  14.688 +"i_th n s1 = i_th n s2 ==> i_rt n (stream_take (Suc n)$s1) = i_rt n (stream_take (Suc n)$s2)"
  14.689 +apply (insert i_th_last [of n s1])
  14.690 +apply (insert i_th_last [of n s2])
  14.691 +by auto
  14.692 +
  14.693 +lemma i_th_prefix_lemma:
  14.694 +"[| k <= n; stream_take (Suc n)$s1 << stream_take (Suc n)$s2 |] ==> 
  14.695 +    i_th k s1 << i_th k s2"
  14.696 +apply (insert i_th_stream_take_Suc [of k s1, THEN sym])
  14.697 +apply (insert i_th_stream_take_Suc [of k s2, THEN sym],auto)
  14.698 +apply (simp add: i_th_def)
  14.699 +apply (rule monofun_cfun, auto)
  14.700 +apply (rule i_rt_mono)
  14.701 +by (blast intro: stream_take_lemma10)
  14.702 +
  14.703 +lemma take_i_rt_prefix_lemma1: 
  14.704 +  "stream_take (Suc n)$s1 << stream_take (Suc n)$s2 ==>
  14.705 +   i_rt (Suc n) s1 << i_rt (Suc n) s2 ==> 
  14.706 +   i_rt n s1 << i_rt n s2 & stream_take n$s1 << stream_take n$s2"
  14.707 +apply auto
  14.708 + apply (insert i_th_prefix_lemma [of n n s1 s2])
  14.709 + apply (rule i_th_i_rt_step,auto)
  14.710 +by (drule mono_stream_take_pred,simp)
  14.711 +
  14.712 +lemma take_i_rt_prefix_lemma: 
  14.713 +"[| stream_take n$s1 << stream_take n$s2; i_rt n s1 << i_rt n s2 |] ==> s1 << s2"
  14.714 +apply (case_tac "n=0",simp)
  14.715 +apply (insert neq0_conv [of n])
  14.716 +apply (insert not0_implies_Suc [of n],auto)
  14.717 +apply (subgoal_tac "stream_take 0$s1 << stream_take 0$s2 & 
  14.718 +                    i_rt 0 s1 << i_rt 0 s2")
  14.719 + defer 1
  14.720 + apply (rule zero_induct,blast)
  14.721 + apply (blast dest: take_i_rt_prefix_lemma1)
  14.722 +by simp
  14.723 +
  14.724 +lemma streams_prefix_lemma: "(s1 << s2) = 
  14.725 +  (stream_take n$s1 << stream_take n$s2 & i_rt n s1 << i_rt n s2)"; 
  14.726 +apply auto
  14.727 +  apply (simp add: monofun_cfun_arg)
  14.728 + apply (simp add: i_rt_mono)
  14.729 +by (erule take_i_rt_prefix_lemma,simp)
  14.730 +
  14.731 +lemma streams_prefix_lemma1:
  14.732 + "[| stream_take n$s1 = stream_take n$s2; i_rt n s1 = i_rt n s2 |] ==> s1 = s2"
  14.733 +apply (simp add: po_eq_conv,auto)
  14.734 + apply (insert streams_prefix_lemma)
  14.735 + by blast+
  14.736 +
  14.737 +
  14.738 +(* ----------------------------------------------------------------------- *)
  14.739 +   section "sconc"
  14.740 +(* ----------------------------------------------------------------------- *)
  14.741 +
  14.742 +lemma UU_sconc [simp]: " UU ooo s = s "
  14.743 +by (simp add: sconc_def inat_defs)
  14.744 +
  14.745 +lemma scons_neq_UU: "a~=UU ==> a && s ~=UU"
  14.746 +by auto
  14.747 +
  14.748 +lemma singleton_sconc [rule_format, simp]: "x~=UU --> (x && UU) ooo y = x && y"
  14.749 +apply (simp add: sconc_def inat_defs split:inat_splits,auto)
  14.750 +apply (rule someI2_ex,auto)
  14.751 + apply (rule_tac x="x && y" in exI,auto)
  14.752 +apply (simp add: i_rt_Suc_forw)
  14.753 +apply (case_tac "xa=UU",simp)
  14.754 +by (drule stream_exhaust_eq [THEN iffD1],auto)
  14.755 +
  14.756 +lemma ex_sconc [rule_format]: 
  14.757 +  "ALL k y. #x = Fin k --> (EX w. stream_take k$w = x & i_rt k w = y)"
  14.758 +apply (case_tac "#x")
  14.759 + apply (rule stream_finite_ind [of x],auto)
  14.760 +  apply (simp add: stream.finite_def)
  14.761 +  apply (drule slen_take_lemma1,blast)
  14.762 + apply (simp add: inat_defs split:inat_splits)+
  14.763 +apply (erule_tac x="y" in allE,auto)
  14.764 +by (rule_tac x="a && w" in exI,auto)
  14.765 +
  14.766 +lemma rt_sconc1: "Fin n = #x ==> i_rt n (x ooo y) = y"; 
  14.767 +apply (simp add: sconc_def inat_defs split:inat_splits, arith?,auto)
  14.768 +apply (rule someI2_ex,auto)
  14.769 +by (drule ex_sconc,simp)
  14.770 +
  14.771 +lemma sconc_inj2: "\<lbrakk>Fin n = #x; x ooo y = x ooo z\<rbrakk> \<Longrightarrow> y = z"
  14.772 +apply (frule_tac y=y in rt_sconc1)
  14.773 +by (auto elim: rt_sconc1)
  14.774 +
  14.775 +lemma sconc_UU [simp]:"s ooo UU = s"
  14.776 +apply (case_tac "#s")
  14.777 + apply (simp add: sconc_def inat_defs)
  14.778 + apply (rule someI2_ex)
  14.779 +  apply (rule_tac x="s" in exI)
  14.780 +  apply auto
  14.781 +   apply (drule slen_take_lemma1,auto)
  14.782 +  apply (simp add: i_rt_lemma_slen)
  14.783 + apply (drule slen_take_lemma1,auto)
  14.784 + apply (simp add: i_rt_slen)
  14.785 +by (simp add: sconc_def inat_defs)
  14.786 +
  14.787 +lemma stream_take_sconc [simp]: "Fin n = #x ==> stream_take n$(x ooo y) = x"
  14.788 +apply (simp add: sconc_def)
  14.789 +apply (simp add: inat_defs split:inat_splits,auto)
  14.790 +apply (rule someI2_ex,auto)
  14.791 +by (drule ex_sconc,simp)
  14.792 +
  14.793 +lemma scons_sconc [rule_format,simp]: "a~=UU --> (a && x) ooo y = a && x ooo y"
  14.794 +apply (case_tac "#x",auto)
  14.795 + apply (simp add: sconc_def) 
  14.796 + apply (rule someI2_ex)
  14.797 +  apply (drule ex_sconc,simp)
  14.798 + apply (rule someI2_ex,auto)
  14.799 +  apply (simp add: i_rt_Suc_forw)
  14.800 +  apply (rule_tac x="a && x" in exI,auto)
  14.801 + apply (case_tac "xa=UU",auto)
  14.802 +  apply (drule_tac s="stream_take nat$x" in scons_neq_UU)
  14.803 +  apply (simp add: i_rt_Suc_forw)
  14.804 + apply (drule stream_exhaust_eq [THEN iffD1],auto)
  14.805 + apply (drule streams_prefix_lemma1,simp+)
  14.806 +by (simp add: sconc_def)
  14.807 +
  14.808 +lemma ft_sconc: "x ~= UU ==> ft$(x ooo y) = ft$x"
  14.809 +by (rule stream.casedist [of x],auto)
  14.810 +
  14.811 +lemma sconc_assoc: "(x ooo y) ooo z = x ooo y ooo z"
  14.812 +apply (case_tac "#x")
  14.813 + apply (rule stream_finite_ind [of x],auto simp del: scons_sconc)
  14.814 +  apply (simp add: stream.finite_def del: scons_sconc)
  14.815 +  apply (drule slen_take_lemma1,auto simp del: scons_sconc)
  14.816 + apply (case_tac "a = UU", auto)
  14.817 +by (simp add: sconc_def)
  14.818 +
  14.819 +
  14.820 +(* ----------------------------------------------------------------------- *)
  14.821 +
  14.822 +lemma sconc_mono: "y << y' ==> x ooo y << x ooo y'"
  14.823 +apply (case_tac "#x")
  14.824 + apply (rule stream_finite_ind [of "x"])
  14.825 +   apply (auto simp add: stream.finite_def)
  14.826 +  apply (drule slen_take_lemma1,blast)
  14.827 + by (simp add: stream_prefix',auto simp add: sconc_def)
  14.828 +
  14.829 +lemma sconc_mono1 [simp]: "x << x ooo y"
  14.830 +by (rule sconc_mono [of UU, simplified])
  14.831 +
  14.832 +(* ----------------------------------------------------------------------- *)
  14.833 +
  14.834 +lemma empty_sconc [simp]: "(x ooo y = UU) = (x = UU & y = UU)"
  14.835 +apply (case_tac "#x",auto)
  14.836 +   apply (insert sconc_mono1 [of x y]);
  14.837 +   by (insert eq_UU_iff [THEN iffD2, of x],auto)
  14.838 +
  14.839 +(* ----------------------------------------------------------------------- *)
  14.840 +
  14.841 +lemma rt_sconc [rule_format, simp]: "s~=UU --> rt$(s ooo x) = rt$s ooo x"
  14.842 +by (rule stream.casedist,auto)
  14.843 +
  14.844 +lemma i_th_sconc_lemma [rule_format]: 
  14.845 +  "ALL x y. Fin n < #x --> i_th n (x ooo y) = i_th n x"
  14.846 +apply (induct_tac n, auto)
  14.847 +apply (simp add: Fin_0 i_th_def)
  14.848 +apply (simp add: slen_empty_eq ft_sconc)
  14.849 +apply (simp add: i_th_def)
  14.850 +apply (case_tac "x=UU",auto)
  14.851 +apply (drule stream_exhaust_eq [THEN iffD1], auto)
  14.852 +apply (erule_tac x="ya" in allE)
  14.853 +by (simp add: inat_defs split:inat_splits)
  14.854 +
  14.855 +
  14.856 +
  14.857 +(* ----------------------------------------------------------------------- *)
  14.858 +
  14.859 +lemma sconc_lemma [rule_format, simp]: "ALL s. stream_take n$s ooo i_rt n s = s"
  14.860 +apply (induct_tac n,auto)
  14.861 +apply (case_tac "s=UU",auto)
  14.862 +by (drule stream_exhaust_eq [THEN iffD1],auto)
  14.863 +
  14.864 +(* ----------------------------------------------------------------------- *)
  14.865 +   subsection "pointwise equality"
  14.866 +(* ----------------------------------------------------------------------- *)
  14.867 +
  14.868 +lemma ex_last_stream_take_scons: "stream_take (Suc n)$s = 
  14.869 +                     stream_take n$s ooo i_rt n (stream_take (Suc n)$s)"
  14.870 +by (insert sconc_lemma [of n "stream_take (Suc n)$s"],simp)
  14.871 +
  14.872 +lemma i_th_stream_take_eq: 
  14.873 +"!!n. ALL n. i_th n s1 = i_th n s2 ==> stream_take n$s1 = stream_take n$s2"
  14.874 +apply (induct_tac n,auto)
  14.875 +apply (subgoal_tac "stream_take (Suc na)$s1 =
  14.876 +                    stream_take na$s1 ooo i_rt na (stream_take (Suc na)$s1)")
  14.877 + apply (subgoal_tac "i_rt na (stream_take (Suc na)$s1) = 
  14.878 +                    i_rt na (stream_take (Suc na)$s2)")
  14.879 +  apply (subgoal_tac "stream_take (Suc na)$s2 = 
  14.880 +                    stream_take na$s2 ooo i_rt na (stream_take (Suc na)$s2)")
  14.881 +   apply (insert ex_last_stream_take_scons,simp)
  14.882 +  apply blast
  14.883 + apply (erule_tac x="na" in allE)
  14.884 + apply (insert i_th_last_eq [of _ s1 s2])
  14.885 +by blast+
  14.886 +
  14.887 +lemma pointwise_eq_lemma[rule_format]: "ALL n. i_th n s1 = i_th n s2 ==> s1 = s2"
  14.888 +by (insert i_th_stream_take_eq [THEN stream.take_lemmas],blast)
  14.889 +
  14.890 +(* ----------------------------------------------------------------------- *)
  14.891 +   subsection "finiteness"
  14.892 +(* ----------------------------------------------------------------------- *)
  14.893 +
  14.894 +lemma slen_sconc_finite1:
  14.895 +  "[| #(x ooo y) = Infty; Fin n = #x |] ==> #y = Infty"
  14.896 +apply (case_tac "#y ~= Infty",auto)
  14.897 +apply (simp only: slen_infinite [symmetric])
  14.898 +apply (drule_tac y=y in rt_sconc1)
  14.899 +apply (insert stream_finite_i_rt [of n "x ooo y"])
  14.900 +by (simp add: slen_infinite)
  14.901 +
  14.902 +lemma slen_sconc_infinite1: "#x=Infty ==> #(x ooo y) = Infty"
  14.903 +by (simp add: sconc_def)
  14.904 +
  14.905 +lemma slen_sconc_infinite2: "#y=Infty ==> #(x ooo y) = Infty"
  14.906 +apply (case_tac "#x")
  14.907 + apply (simp add: sconc_def)
  14.908 + apply (rule someI2_ex)
  14.909 +  apply (drule ex_sconc,auto)
  14.910 + apply (erule contrapos_pp)
  14.911 + apply (insert stream_finite_i_rt)
  14.912 + apply (simp add: slen_infinite,auto)
  14.913 +by (simp add: sconc_def)
  14.914 +
  14.915 +lemma sconc_finite: "(#x~=Infty & #y~=Infty) = (#(x ooo y)~=Infty)"
  14.916 +apply auto
  14.917 +  apply (case_tac "#x",auto)
  14.918 +  apply (erule contrapos_pp,simp)
  14.919 +  apply (erule slen_sconc_finite1,simp)
  14.920 + apply (drule slen_sconc_infinite1 [of _ y],simp)
  14.921 +by (drule slen_sconc_infinite2 [of _ x],simp)
  14.922 +
  14.923 +(* ----------------------------------------------------------------------- *)
  14.924 +
  14.925 +lemma slen_sconc_mono3: "[| Fin n = #x; Fin k = #(x ooo y) |] ==> n <= k"
  14.926 +apply (insert slen_mono [of "x" "x ooo y"])
  14.927 +by (simp add: inat_defs split: inat_splits)
  14.928 +
  14.929 +(* ----------------------------------------------------------------------- *)
  14.930 +   subsection "finite slen"
  14.931 +(* ----------------------------------------------------------------------- *)
  14.932 +
  14.933 +lemma slen_sconc: "[| Fin n = #x; Fin m = #y |] ==> #(x ooo y) = Fin (n + m)"
  14.934 +apply (case_tac "#(x ooo y)")
  14.935 + apply (frule_tac y=y in rt_sconc1)
  14.936 + apply (insert take_i_rt_len [of "THE j. Fin j = #(x ooo y)" "x ooo y" n n m],simp)
  14.937 + apply (insert slen_sconc_mono3 [of n x _ y],simp)
  14.938 +by (insert sconc_finite [of x y],auto)
  14.939 +
  14.940 +(* ----------------------------------------------------------------------- *)
  14.941 +   subsection "flat prefix"
  14.942 +(* ----------------------------------------------------------------------- *)
  14.943 +
  14.944 +lemma sconc_prefix: "(s1::'a::flat stream) << s2 ==> EX t. s1 ooo t = s2"
  14.945 +apply (case_tac "#s1")
  14.946 + apply (subgoal_tac "stream_take nat$s1 = stream_take nat$s2");
  14.947 +  apply (rule_tac x="i_rt nat s2" in exI)
  14.948 +  apply (simp add: sconc_def)
  14.949 +  apply (rule someI2_ex)
  14.950 +   apply (drule ex_sconc)
  14.951 +   apply (simp,clarsimp,drule streams_prefix_lemma1)
  14.952 +   apply (simp+,rule slen_take_lemma3 [of _ s1 s2]);
  14.953 +  apply (simp+,rule_tac x="UU" in exI)
  14.954 +apply (insert slen_take_lemma3 [of _ s1 s2]);
  14.955 +by (rule stream.take_lemmas,simp)
  14.956 +
  14.957 +(* ----------------------------------------------------------------------- *)
  14.958 +   subsection "continuity"
  14.959 +(* ----------------------------------------------------------------------- *)
  14.960 +
  14.961 +lemma chain_sconc: "chain S ==> chain (%i. (x ooo S i))"
  14.962 +by (simp add: chain_def,auto simp add: sconc_mono)
  14.963 +
  14.964 +lemma chain_scons: "chain S ==> chain (%i. a && S i)"
  14.965 +apply (simp add: chain_def,auto)
  14.966 +by (rule monofun_cfun_arg,simp)
  14.967 +
  14.968 +lemma contlub_scons: "contlub (%x. a && x)"
  14.969 +by (simp add: contlub_Rep_CFun2)
  14.970 +
  14.971 +lemma contlub_scons_lemma: "chain S ==> (LUB i. a && S i) = a && (LUB i. S i)"
  14.972 +apply (insert contlub_scons [of a])
  14.973 +by (simp only: contlub)
  14.974 +
  14.975 +lemma finite_lub_sconc: "chain Y ==> (stream_finite x) ==> 
  14.976 +                        (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
  14.977 +apply (rule stream_finite_ind [of x])
  14.978 + apply (auto)
  14.979 +apply (subgoal_tac "(LUB i. a && (s ooo Y i)) = a && (LUB i. s ooo Y i)")
  14.980 + by (force,blast dest: contlub_scons_lemma chain_sconc)
  14.981 +
  14.982 +lemma contlub_sconc_lemma: 
  14.983 +  "chain Y ==> (LUB i. x ooo Y i) = (x ooo (LUB i. Y i))"
  14.984 +apply (case_tac "#x=Infty")
  14.985 + apply (simp add: sconc_def)
  14.986 + prefer 2
  14.987 + apply (drule finite_lub_sconc,auto simp add: slen_infinite)
  14.988 +apply (simp add: slen_def)
  14.989 +apply (insert lub_const [of x] unique_lub [of _ x _])
  14.990 +by (auto simp add: lub)
  14.991 +
  14.992 +lemma contlub_sconc: "contlub (%y. x ooo y)"; 
  14.993 +by (rule contlubI, insert contlub_sconc_lemma [of _ x], simp);
  14.994 +
  14.995 +lemma monofun_sconc: "monofun (%y. x ooo y)"
  14.996 +by (simp add: monofun sconc_mono)
  14.997 +
  14.998 +lemma cont_sconc: "cont (%y. x ooo y)"
  14.999 +apply (rule  monocontlub2cont)
 14.1000 + apply (rule monofunI, simp add: sconc_mono)
 14.1001 +by (rule contlub_sconc);
 14.1002 +
 14.1003 +
 14.1004 +(* ----------------------------------------------------------------------- *)
 14.1005 +   section "constr_sconc"
 14.1006 +(* ----------------------------------------------------------------------- *)
 14.1007 +
 14.1008 +lemma constr_sconc_UUs [simp]: "constr_sconc UU s = s"
 14.1009 +by (simp add: constr_sconc_def inat_defs)
 14.1010 +
 14.1011 +lemma "x ooo y = constr_sconc x y"
 14.1012 +apply (case_tac "#x")
 14.1013 + apply (rule stream_finite_ind [of x],auto simp del: scons_sconc)
 14.1014 +  defer 1
 14.1015 +  apply (simp add: constr_sconc_def del: scons_sconc)
 14.1016 +  apply (case_tac "#s")
 14.1017 +   apply (simp add: inat_defs)
 14.1018 +   apply (case_tac "a=UU",auto simp del: scons_sconc)
 14.1019 +   apply (simp)
 14.1020 +  apply (simp add: sconc_def)
 14.1021 + apply (simp add: constr_sconc_def)
 14.1022 +apply (simp add: stream.finite_def)
 14.1023 +by (drule slen_take_lemma1,auto)
 14.1024 +
 14.1025 +declare eq_UU_iff [THEN sym, simp add]
 14.1026  
 14.1027  end
 14.1028 -
 14.1029 -