move Stream theory from Datatype_Examples to Library
authorhoelzl
Tue Oct 07 10:48:29 2014 +0200 (2014-10-07)
changeset 586071f90ea1b4010
parent 58606 9c66f7c541fb
child 58608 5b7f0b5da884
move Stream theory from Datatype_Examples to Library
src/HOL/Datatype_Examples/Koenig.thy
src/HOL/Datatype_Examples/Process.thy
src/HOL/Datatype_Examples/Stream.thy
src/HOL/Datatype_Examples/Stream_Processor.thy
src/HOL/Library/Library.thy
src/HOL/Library/Stream.thy
src/HOL/Probability/Stream_Space.thy
     1.1 --- a/src/HOL/Datatype_Examples/Koenig.thy	Tue Oct 07 10:34:24 2014 +0200
     1.2 +++ b/src/HOL/Datatype_Examples/Koenig.thy	Tue Oct 07 10:48:29 2014 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  header {* Koenig's Lemma *}
     1.5  
     1.6  theory Koenig
     1.7 -imports TreeFI Stream
     1.8 +imports TreeFI "~~/src/HOL/Library/Stream"
     1.9  begin
    1.10  
    1.11  (* infinite trees: *)
     2.1 --- a/src/HOL/Datatype_Examples/Process.thy	Tue Oct 07 10:34:24 2014 +0200
     2.2 +++ b/src/HOL/Datatype_Examples/Process.thy	Tue Oct 07 10:48:29 2014 +0200
     2.3 @@ -8,7 +8,7 @@
     2.4  header {* Processes *}
     2.5  
     2.6  theory Process
     2.7 -imports Stream 
     2.8 +imports "~~/src/HOL/Library/Stream"
     2.9  begin
    2.10  
    2.11  codatatype 'a process =
     3.1 --- a/src/HOL/Datatype_Examples/Stream.thy	Tue Oct 07 10:34:24 2014 +0200
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,582 +0,0 @@
     3.4 -(*  Title:      HOL/Datatype_Examples/Stream.thy
     3.5 -    Author:     Dmitriy Traytel, TU Muenchen
     3.6 -    Author:     Andrei Popescu, TU Muenchen
     3.7 -    Copyright   2012, 2013
     3.8 -
     3.9 -Infinite streams.
    3.10 -*)
    3.11 -
    3.12 -header {* Infinite Streams *}
    3.13 -
    3.14 -theory Stream
    3.15 -imports "~~/src/HOL/Library/Nat_Bijection"
    3.16 -begin
    3.17 -
    3.18 -codatatype (sset: 'a) stream =
    3.19 -  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
    3.20 -for
    3.21 -  map: smap
    3.22 -  rel: stream_all2
    3.23 -
    3.24 -(*for code generation only*)
    3.25 -definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where
    3.26 -  [code_abbrev]: "smember x s \<longleftrightarrow> x \<in> sset s"
    3.27 -
    3.28 -lemma smember_code[code, simp]: "smember x (y ## s) = (if x = y then True else smember x s)"
    3.29 -  unfolding smember_def by auto
    3.30 -
    3.31 -hide_const (open) smember
    3.32 -
    3.33 -lemmas smap_simps[simp] = stream.map_sel
    3.34 -lemmas shd_sset = stream.set_sel(1)
    3.35 -lemmas stl_sset = stream.set_sel(2)
    3.36 -
    3.37 -theorem sset_induct[consumes 1, case_names shd stl, induct set: sset]:
    3.38 -  assumes "y \<in> sset s" and "\<And>s. P (shd s) s" and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
    3.39 -  shows "P y s"
    3.40 -using assms by induct (metis stream.sel(1), auto)
    3.41 -
    3.42 -
    3.43 -subsection {* prepend list to stream *}
    3.44 -
    3.45 -primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where
    3.46 -  "shift [] s = s"
    3.47 -| "shift (x # xs) s = x ## shift xs s"
    3.48 -
    3.49 -lemma smap_shift[simp]: "smap f (xs @- s) = map f xs @- smap f s"
    3.50 -  by (induct xs) auto
    3.51 -
    3.52 -lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s"
    3.53 -  by (induct xs) auto
    3.54 -
    3.55 -lemma shift_simps[simp]:
    3.56 -   "shd (xs @- s) = (if xs = [] then shd s else hd xs)"
    3.57 -   "stl (xs @- s) = (if xs = [] then stl s else tl xs @- s)"
    3.58 -  by (induct xs) auto
    3.59 -
    3.60 -lemma sset_shift[simp]: "sset (xs @- s) = set xs \<union> sset s"
    3.61 -  by (induct xs) auto
    3.62 -
    3.63 -lemma shift_left_inj[simp]: "xs @- s1 = xs @- s2 \<longleftrightarrow> s1 = s2"
    3.64 -  by (induct xs) auto
    3.65 -
    3.66 -
    3.67 -subsection {* set of streams with elements in some fixed set *}
    3.68 -
    3.69 -coinductive_set
    3.70 -  streams :: "'a set \<Rightarrow> 'a stream set"
    3.71 -  for A :: "'a set"
    3.72 -where
    3.73 -  Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
    3.74 -
    3.75 -lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A"
    3.76 -  by (induct w) auto
    3.77 -
    3.78 -lemma streams_Stream: "x ## s \<in> streams A \<longleftrightarrow> x \<in> A \<and> s \<in> streams A"
    3.79 -  by (auto elim: streams.cases)
    3.80 -
    3.81 -lemma streams_stl: "s \<in> streams A \<Longrightarrow> stl s \<in> streams A"
    3.82 -  by (cases s) (auto simp: streams_Stream)
    3.83 -
    3.84 -lemma streams_shd: "s \<in> streams A \<Longrightarrow> shd s \<in> A"
    3.85 -  by (cases s) (auto simp: streams_Stream)
    3.86 -
    3.87 -lemma sset_streams:
    3.88 -  assumes "sset s \<subseteq> A"
    3.89 -  shows "s \<in> streams A"
    3.90 -using assms proof (coinduction arbitrary: s)
    3.91 -  case streams then show ?case by (cases s) simp
    3.92 -qed
    3.93 -
    3.94 -lemma streams_sset:
    3.95 -  assumes "s \<in> streams A"
    3.96 -  shows "sset s \<subseteq> A"
    3.97 -proof
    3.98 -  fix x assume "x \<in> sset s" from this `s \<in> streams A` show "x \<in> A"
    3.99 -    by (induct s) (auto intro: streams_shd streams_stl)
   3.100 -qed
   3.101 -
   3.102 -lemma streams_iff_sset: "s \<in> streams A \<longleftrightarrow> sset s \<subseteq> A"
   3.103 -  by (metis sset_streams streams_sset)
   3.104 -
   3.105 -lemma streams_mono:  "s \<in> streams A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> s \<in> streams B"
   3.106 -  unfolding streams_iff_sset by auto
   3.107 -
   3.108 -lemma smap_streams: "s \<in> streams A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> smap f s \<in> streams B"
   3.109 -  unfolding streams_iff_sset stream.set_map by auto
   3.110 -
   3.111 -lemma streams_empty: "streams {} = {}"
   3.112 -  by (auto elim: streams.cases)
   3.113 -
   3.114 -lemma streams_UNIV[simp]: "streams UNIV = UNIV"
   3.115 -  by (auto simp: streams_iff_sset)
   3.116 -
   3.117 -subsection {* nth, take, drop for streams *}
   3.118 -
   3.119 -primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
   3.120 -  "s !! 0 = shd s"
   3.121 -| "s !! Suc n = stl s !! n"
   3.122 -
   3.123 -lemma snth_smap[simp]: "smap f s !! n = f (s !! n)"
   3.124 -  by (induct n arbitrary: s) auto
   3.125 -
   3.126 -lemma shift_snth_less[simp]: "p < length xs \<Longrightarrow> (xs @- s) !! p = xs ! p"
   3.127 -  by (induct p arbitrary: xs) (auto simp: hd_conv_nth nth_tl)
   3.128 -
   3.129 -lemma shift_snth_ge[simp]: "p \<ge> length xs \<Longrightarrow> (xs @- s) !! p = s !! (p - length xs)"
   3.130 -  by (induct p arbitrary: xs) (auto simp: Suc_diff_eq_diff_pred)
   3.131 -
   3.132 -lemma shift_snth: "(xs @- s) !! n = (if n < length xs then xs ! n else s !! (n - length xs))"
   3.133 -  by auto
   3.134 -
   3.135 -lemma snth_sset[simp]: "s !! n \<in> sset s"
   3.136 -  by (induct n arbitrary: s) (auto intro: shd_sset stl_sset)
   3.137 -
   3.138 -lemma sset_range: "sset s = range (snth s)"
   3.139 -proof (intro equalityI subsetI)
   3.140 -  fix x assume "x \<in> sset s"
   3.141 -  thus "x \<in> range (snth s)"
   3.142 -  proof (induct s)
   3.143 -    case (stl s x)
   3.144 -    then obtain n where "x = stl s !! n" by auto
   3.145 -    thus ?case by (auto intro: range_eqI[of _ _ "Suc n"])
   3.146 -  qed (auto intro: range_eqI[of _ _ 0])
   3.147 -qed auto
   3.148 -
   3.149 -primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
   3.150 -  "stake 0 s = []"
   3.151 -| "stake (Suc n) s = shd s # stake n (stl s)"
   3.152 -
   3.153 -lemma length_stake[simp]: "length (stake n s) = n"
   3.154 -  by (induct n arbitrary: s) auto
   3.155 -
   3.156 -lemma stake_smap[simp]: "stake n (smap f s) = map f (stake n s)"
   3.157 -  by (induct n arbitrary: s) auto
   3.158 -
   3.159 -lemma take_stake: "take n (stake m s) = stake (min n m) s"
   3.160 -proof (induct m arbitrary: s n)
   3.161 -  case (Suc m) thus ?case by (cases n) auto
   3.162 -qed simp
   3.163 -
   3.164 -primrec sdrop :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
   3.165 -  "sdrop 0 s = s"
   3.166 -| "sdrop (Suc n) s = sdrop n (stl s)"
   3.167 -
   3.168 -lemma sdrop_simps[simp]:
   3.169 -  "shd (sdrop n s) = s !! n" "stl (sdrop n s) = sdrop (Suc n) s"
   3.170 -  by (induct n arbitrary: s)  auto
   3.171 -
   3.172 -lemma sdrop_smap[simp]: "sdrop n (smap f s) = smap f (sdrop n s)"
   3.173 -  by (induct n arbitrary: s) auto
   3.174 -
   3.175 -lemma sdrop_stl: "sdrop n (stl s) = stl (sdrop n s)"
   3.176 -  by (induct n) auto
   3.177 -
   3.178 -lemma drop_stake: "drop n (stake m s) = stake (m - n) (sdrop n s)"
   3.179 -proof (induct m arbitrary: s n)
   3.180 -  case (Suc m) thus ?case by (cases n) auto
   3.181 -qed simp
   3.182 -
   3.183 -lemma stake_sdrop: "stake n s @- sdrop n s = s"
   3.184 -  by (induct n arbitrary: s) auto
   3.185 -
   3.186 -lemma id_stake_snth_sdrop:
   3.187 -  "s = stake i s @- s !! i ## sdrop (Suc i) s"
   3.188 -  by (subst stake_sdrop[symmetric, of _ i]) (metis sdrop_simps stream.collapse)
   3.189 -
   3.190 -lemma smap_alt: "smap f s = s' \<longleftrightarrow> (\<forall>n. f (s !! n) = s' !! n)" (is "?L = ?R")
   3.191 -proof
   3.192 -  assume ?R
   3.193 -  then have "\<And>n. smap f (sdrop n s) = sdrop n s'"
   3.194 -    by coinduction (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
   3.195 -  then show ?L using sdrop.simps(1) by metis
   3.196 -qed auto
   3.197 -
   3.198 -lemma stake_invert_Nil[iff]: "stake n s = [] \<longleftrightarrow> n = 0"
   3.199 -  by (induct n) auto
   3.200 -
   3.201 -lemma sdrop_shift: "sdrop i (w @- s) = drop i w @- sdrop (i - length w) s"
   3.202 -  by (induct i arbitrary: w s) (auto simp: drop_tl drop_Suc neq_Nil_conv)
   3.203 -
   3.204 -lemma stake_shift: "stake i (w @- s) = take i w @ stake (i - length w) s"
   3.205 -  by (induct i arbitrary: w s) (auto simp: neq_Nil_conv)
   3.206 -
   3.207 -lemma stake_add[simp]: "stake m s @ stake n (sdrop m s) = stake (m + n) s"
   3.208 -  by (induct m arbitrary: s) auto
   3.209 -
   3.210 -lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s"
   3.211 -  by (induct m arbitrary: s) auto
   3.212 -
   3.213 -lemma sdrop_snth: "sdrop n s !! m = s !! (n + m)"
   3.214 -  by (induct n arbitrary: m s) auto
   3.215 -
   3.216 -partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 
   3.217 -  "sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
   3.218 -
   3.219 -lemma sdrop_while_SCons[code]:
   3.220 -  "sdrop_while P (a ## s) = (if P a then sdrop_while P s else a ## s)"
   3.221 -  by (subst sdrop_while.simps) simp
   3.222 -
   3.223 -lemma sdrop_while_sdrop_LEAST:
   3.224 -  assumes "\<exists>n. P (s !! n)"
   3.225 -  shows "sdrop_while (Not o P) s = sdrop (LEAST n. P (s !! n)) s"
   3.226 -proof -
   3.227 -  from assms obtain m where "P (s !! m)" "\<And>n. P (s !! n) \<Longrightarrow> m \<le> n"
   3.228 -    and *: "(LEAST n. P (s !! n)) = m" by atomize_elim (auto intro: LeastI Least_le)
   3.229 -  thus ?thesis unfolding *
   3.230 -  proof (induct m arbitrary: s)
   3.231 -    case (Suc m)
   3.232 -    hence "sdrop_while (Not \<circ> P) (stl s) = sdrop m (stl s)"
   3.233 -      by (metis (full_types) not_less_eq_eq snth.simps(2))
   3.234 -    moreover from Suc(3) have "\<not> (P (s !! 0))" by blast
   3.235 -    ultimately show ?case by (subst sdrop_while.simps) simp
   3.236 -  qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
   3.237 -qed
   3.238 -
   3.239 -primcorec sfilter where
   3.240 -  "shd (sfilter P s) = shd (sdrop_while (Not o P) s)"
   3.241 -| "stl (sfilter P s) = sfilter P (stl (sdrop_while (Not o P) s))"
   3.242 -
   3.243 -lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
   3.244 -proof (cases "P x")
   3.245 -  case True thus ?thesis by (subst sfilter.ctr) (simp add: sdrop_while_SCons)
   3.246 -next
   3.247 -  case False thus ?thesis by (subst (1 2) sfilter.ctr) (simp add: sdrop_while_SCons)
   3.248 -qed
   3.249 -
   3.250 -
   3.251 -subsection {* unary predicates lifted to streams *}
   3.252 -
   3.253 -definition "stream_all P s = (\<forall>p. P (s !! p))"
   3.254 -
   3.255 -lemma stream_all_iff[iff]: "stream_all P s \<longleftrightarrow> Ball (sset s) P"
   3.256 -  unfolding stream_all_def sset_range by auto
   3.257 -
   3.258 -lemma stream_all_shift[simp]: "stream_all P (xs @- s) = (list_all P xs \<and> stream_all P s)"
   3.259 -  unfolding stream_all_iff list_all_iff by auto
   3.260 -
   3.261 -lemma stream_all_Stream: "stream_all P (x ## X) \<longleftrightarrow> P x \<and> stream_all P X"
   3.262 -  by simp
   3.263 -
   3.264 -
   3.265 -subsection {* recurring stream out of a list *}
   3.266 -
   3.267 -primcorec cycle :: "'a list \<Rightarrow> 'a stream" where
   3.268 -  "shd (cycle xs) = hd xs"
   3.269 -| "stl (cycle xs) = cycle (tl xs @ [hd xs])"
   3.270 -
   3.271 -lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u"
   3.272 -proof (coinduction arbitrary: u)
   3.273 -  case Eq_stream then show ?case using stream.collapse[of "cycle u"]
   3.274 -    by (auto intro!: exI[of _ "tl u @ [hd u]"])
   3.275 -qed
   3.276 -
   3.277 -lemma cycle_Cons[code]: "cycle (x # xs) = x ## cycle (xs @ [x])"
   3.278 -  by (subst cycle.ctr) simp
   3.279 -
   3.280 -lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @- s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @- s"
   3.281 -  by (auto dest: arg_cong[of _ _ stl])
   3.282 -
   3.283 -lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s"
   3.284 -proof (induct n arbitrary: u)
   3.285 -  case (Suc n) thus ?case by (cases u) auto
   3.286 -qed auto
   3.287 -
   3.288 -lemma stake_cycle_le[simp]:
   3.289 -  assumes "u \<noteq> []" "n < length u"
   3.290 -  shows "stake n (cycle u) = take n u"
   3.291 -using min_absorb2[OF less_imp_le_nat[OF assms(2)]]
   3.292 -  by (subst cycle_decomp[OF assms(1)], subst stake_append) auto
   3.293 -
   3.294 -lemma stake_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> stake (length u) (cycle u) = u"
   3.295 -  by (subst cycle_decomp) (auto simp: stake_shift)
   3.296 -
   3.297 -lemma sdrop_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> sdrop (length u) (cycle u) = cycle u"
   3.298 -  by (subst cycle_decomp) (auto simp: sdrop_shift)
   3.299 -
   3.300 -lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
   3.301 -   stake n (cycle u) = concat (replicate (n div length u) u)"
   3.302 -  by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric])
   3.303 -
   3.304 -lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
   3.305 -   sdrop n (cycle u) = cycle u"
   3.306 -  by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric])
   3.307 -
   3.308 -lemma stake_cycle: "u \<noteq> [] \<Longrightarrow>
   3.309 -   stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
   3.310 -  by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto
   3.311 -
   3.312 -lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
   3.313 -  by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
   3.314 -
   3.315 -
   3.316 -subsection {* iterated application of a function *}
   3.317 -
   3.318 -primcorec siterate where
   3.319 -  "shd (siterate f x) = x"
   3.320 -| "stl (siterate f x) = siterate f (f x)"
   3.321 -
   3.322 -lemma stake_Suc: "stake (Suc n) s = stake n s @ [s !! n]"
   3.323 -  by (induct n arbitrary: s) auto
   3.324 -
   3.325 -lemma snth_siterate[simp]: "siterate f x !! n = (f^^n) x"
   3.326 -  by (induct n arbitrary: x) (auto simp: funpow_swap1)
   3.327 -
   3.328 -lemma sdrop_siterate[simp]: "sdrop n (siterate f x) = siterate f ((f^^n) x)"
   3.329 -  by (induct n arbitrary: x) (auto simp: funpow_swap1)
   3.330 -
   3.331 -lemma stake_siterate[simp]: "stake n (siterate f x) = map (\<lambda>n. (f^^n) x) [0 ..< n]"
   3.332 -  by (induct n arbitrary: x) (auto simp del: stake.simps(2) simp: stake_Suc)
   3.333 -
   3.334 -lemma sset_siterate: "sset (siterate f x) = {(f^^n) x | n. True}"
   3.335 -  by (auto simp: sset_range)
   3.336 -
   3.337 -lemma smap_siterate: "smap f (siterate f x) = siterate f (f x)"
   3.338 -  by (coinduction arbitrary: x) auto
   3.339 -
   3.340 -
   3.341 -subsection {* stream repeating a single element *}
   3.342 -
   3.343 -abbreviation "sconst \<equiv> siterate id"
   3.344 -
   3.345 -lemma shift_replicate_sconst[simp]: "replicate n x @- sconst x = sconst x"
   3.346 -  by (subst (3) stake_sdrop[symmetric]) (simp add: map_replicate_trivial)
   3.347 -
   3.348 -lemma sset_sconst[simp]: "sset (sconst x) = {x}"
   3.349 -  by (simp add: sset_siterate)
   3.350 -
   3.351 -lemma sconst_alt: "s = sconst x \<longleftrightarrow> sset s = {x}"
   3.352 -proof
   3.353 -  assume "sset s = {x}"
   3.354 -  then show "s = sconst x"
   3.355 -  proof (coinduction arbitrary: s)
   3.356 -    case Eq_stream
   3.357 -    then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (case_tac [!] s) auto
   3.358 -    then have "sset (stl s) = {x}" by (cases "stl s") auto
   3.359 -    with `shd s = x` show ?case by auto
   3.360 -  qed
   3.361 -qed simp
   3.362 -
   3.363 -lemma same_cycle: "sconst x = cycle [x]"
   3.364 -  by coinduction auto
   3.365 -
   3.366 -lemma smap_sconst: "smap f (sconst x) = sconst (f x)"
   3.367 -  by coinduction auto
   3.368 -
   3.369 -lemma sconst_streams: "x \<in> A \<Longrightarrow> sconst x \<in> streams A"
   3.370 -  by (simp add: streams_iff_sset)
   3.371 -
   3.372 -
   3.373 -subsection {* stream of natural numbers *}
   3.374 -
   3.375 -abbreviation "fromN \<equiv> siterate Suc"
   3.376 -
   3.377 -abbreviation "nats \<equiv> fromN 0"
   3.378 -
   3.379 -lemma sset_fromN[simp]: "sset (fromN n) = {n ..}"
   3.380 -  by (auto simp add: sset_siterate le_iff_add)
   3.381 -
   3.382 -lemma stream_smap_fromN: "s = smap (\<lambda>j. let i = j - n in s !! i) (fromN n)"
   3.383 -  by (coinduction arbitrary: s n)
   3.384 -    (force simp: neq_Nil_conv Let_def snth.simps(2)[symmetric] Suc_diff_Suc
   3.385 -      intro: stream.map_cong split: if_splits simp del: snth.simps(2))
   3.386 -
   3.387 -lemma stream_smap_nats: "s = smap (snth s) nats"
   3.388 -  using stream_smap_fromN[where n = 0] by simp
   3.389 -
   3.390 -
   3.391 -subsection {* flatten a stream of lists *}
   3.392 -
   3.393 -primcorec flat where
   3.394 -  "shd (flat ws) = hd (shd ws)"
   3.395 -| "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
   3.396 -
   3.397 -lemma flat_Cons[simp, code]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
   3.398 -  by (subst flat.ctr) simp
   3.399 -
   3.400 -lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
   3.401 -  by (induct xs) auto
   3.402 -
   3.403 -lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
   3.404 -  by (cases ws) auto
   3.405 -
   3.406 -lemma flat_snth: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then 
   3.407 -  shd s ! n else flat (stl s) !! (n - length (shd s)))"
   3.408 -  by (metis flat_unfold not_less shd_sset shift_snth_ge shift_snth_less)
   3.409 -
   3.410 -lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> 
   3.411 -  sset (flat s) = (\<Union>xs \<in> sset s. set xs)" (is "?P \<Longrightarrow> ?L = ?R")
   3.412 -proof safe
   3.413 -  fix x assume ?P "x : ?L"
   3.414 -  then obtain m where "x = flat s !! m" by (metis image_iff sset_range)
   3.415 -  with `?P` obtain n m' where "x = s !! n ! m'" "m' < length (s !! n)"
   3.416 -  proof (atomize_elim, induct m arbitrary: s rule: less_induct)
   3.417 -    case (less y)
   3.418 -    thus ?case
   3.419 -    proof (cases "y < length (shd s)")
   3.420 -      case True thus ?thesis by (metis flat_snth less(2,3) snth.simps(1))
   3.421 -    next
   3.422 -      case False
   3.423 -      hence "x = flat (stl s) !! (y - length (shd s))" by (metis less(2,3) flat_snth)
   3.424 -      moreover
   3.425 -      { from less(2) have *: "length (shd s) > 0" by (cases s) simp_all
   3.426 -        with False have "y > 0" by (cases y) simp_all
   3.427 -        with * have "y - length (shd s) < y" by simp
   3.428 -      }
   3.429 -      moreover have "\<forall>xs \<in> sset (stl s). xs \<noteq> []" using less(2) by (cases s) auto
   3.430 -      ultimately have "\<exists>n m'. x = stl s !! n ! m' \<and> m' < length (stl s !! n)" by (intro less(1)) auto
   3.431 -      thus ?thesis by (metis snth.simps(2))
   3.432 -    qed
   3.433 -  qed
   3.434 -  thus "x \<in> ?R" by (auto simp: sset_range dest!: nth_mem)
   3.435 -next
   3.436 -  fix x xs assume "xs \<in> sset s" ?P "x \<in> set xs" thus "x \<in> ?L"
   3.437 -    by (induct rule: sset_induct)
   3.438 -      (metis UnI1 flat_unfold shift.simps(1) sset_shift,
   3.439 -       metis UnI2 flat_unfold shd_sset stl_sset sset_shift)
   3.440 -qed
   3.441 -
   3.442 -
   3.443 -subsection {* merge a stream of streams *}
   3.444 -
   3.445 -definition smerge :: "'a stream stream \<Rightarrow> 'a stream" where
   3.446 -  "smerge ss = flat (smap (\<lambda>n. map (\<lambda>s. s !! n) (stake (Suc n) ss) @ stake n (ss !! n)) nats)"
   3.447 -
   3.448 -lemma stake_nth[simp]: "m < n \<Longrightarrow> stake n s ! m = s !! m"
   3.449 -  by (induct n arbitrary: s m) (auto simp: nth_Cons', metis Suc_pred snth.simps(2))
   3.450 -
   3.451 -lemma snth_sset_smerge: "ss !! n !! m \<in> sset (smerge ss)"
   3.452 -proof (cases "n \<le> m")
   3.453 -  case False thus ?thesis unfolding smerge_def
   3.454 -    by (subst sset_flat)
   3.455 -      (auto simp: stream.set_map in_set_conv_nth simp del: stake.simps
   3.456 -        intro!: exI[of _ n, OF disjI2] exI[of _ m, OF mp])
   3.457 -next
   3.458 -  case True thus ?thesis unfolding smerge_def
   3.459 -    by (subst sset_flat)
   3.460 -      (auto simp: stream.set_map in_set_conv_nth image_iff simp del: stake.simps snth.simps
   3.461 -        intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp])
   3.462 -qed
   3.463 -
   3.464 -lemma sset_smerge: "sset (smerge ss) = UNION (sset ss) sset"
   3.465 -proof safe
   3.466 -  fix x assume "x \<in> sset (smerge ss)"
   3.467 -  thus "x \<in> UNION (sset ss) sset"
   3.468 -    unfolding smerge_def by (subst (asm) sset_flat)
   3.469 -      (auto simp: stream.set_map in_set_conv_nth sset_range simp del: stake.simps, fast+)
   3.470 -next
   3.471 -  fix s x assume "s \<in> sset ss" "x \<in> sset s"
   3.472 -  thus "x \<in> sset (smerge ss)" using snth_sset_smerge by (auto simp: sset_range)
   3.473 -qed
   3.474 -
   3.475 -
   3.476 -subsection {* product of two streams *}
   3.477 -
   3.478 -definition sproduct :: "'a stream \<Rightarrow> 'b stream \<Rightarrow> ('a \<times> 'b) stream" where
   3.479 -  "sproduct s1 s2 = smerge (smap (\<lambda>x. smap (Pair x) s2) s1)"
   3.480 -
   3.481 -lemma sset_sproduct: "sset (sproduct s1 s2) = sset s1 \<times> sset s2"
   3.482 -  unfolding sproduct_def sset_smerge by (auto simp: stream.set_map)
   3.483 -
   3.484 -
   3.485 -subsection {* interleave two streams *}
   3.486 -
   3.487 -primcorec sinterleave where
   3.488 -  "shd (sinterleave s1 s2) = shd s1"
   3.489 -| "stl (sinterleave s1 s2) = sinterleave s2 (stl s1)"
   3.490 -
   3.491 -lemma sinterleave_code[code]:
   3.492 -  "sinterleave (x ## s1) s2 = x ## sinterleave s2 s1"
   3.493 -  by (subst sinterleave.ctr) simp
   3.494 -
   3.495 -lemma sinterleave_snth[simp]:
   3.496 -  "even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
   3.497 -   "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
   3.498 -  by (induct n arbitrary: s1 s2)
   3.499 -    (auto dest: even_nat_Suc_div_2 odd_nat_plus_one_div_two[folded nat_2])
   3.500 -
   3.501 -lemma sset_sinterleave: "sset (sinterleave s1 s2) = sset s1 \<union> sset s2"
   3.502 -proof (intro equalityI subsetI)
   3.503 -  fix x assume "x \<in> sset (sinterleave s1 s2)"
   3.504 -  then obtain n where "x = sinterleave s1 s2 !! n" unfolding sset_range by blast
   3.505 -  thus "x \<in> sset s1 \<union> sset s2" by (cases "even n") auto
   3.506 -next
   3.507 -  fix x assume "x \<in> sset s1 \<union> sset s2"
   3.508 -  thus "x \<in> sset (sinterleave s1 s2)"
   3.509 -  proof
   3.510 -    assume "x \<in> sset s1"
   3.511 -    then obtain n where "x = s1 !! n" unfolding sset_range by blast
   3.512 -    hence "sinterleave s1 s2 !! (2 * n) = x" by simp
   3.513 -    thus ?thesis unfolding sset_range by blast
   3.514 -  next
   3.515 -    assume "x \<in> sset s2"
   3.516 -    then obtain n where "x = s2 !! n" unfolding sset_range by blast
   3.517 -    hence "sinterleave s1 s2 !! (2 * n + 1) = x" by simp
   3.518 -    thus ?thesis unfolding sset_range by blast
   3.519 -  qed
   3.520 -qed
   3.521 -
   3.522 -
   3.523 -subsection {* zip *}
   3.524 -
   3.525 -primcorec szip where
   3.526 -  "shd (szip s1 s2) = (shd s1, shd s2)"
   3.527 -| "stl (szip s1 s2) = szip (stl s1) (stl s2)"
   3.528 -
   3.529 -lemma szip_unfold[code]: "szip (a ## s1) (b ## s2) = (a, b) ## (szip s1 s2)"
   3.530 -  by (subst szip.ctr) simp
   3.531 -
   3.532 -lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)"
   3.533 -  by (induct n arbitrary: s1 s2) auto
   3.534 -
   3.535 -lemma stake_szip[simp]:
   3.536 -  "stake n (szip s1 s2) = zip (stake n s1) (stake n s2)"
   3.537 -  by (induct n arbitrary: s1 s2) auto
   3.538 -
   3.539 -lemma sdrop_szip[simp]: "sdrop n (szip s1 s2) = szip (sdrop n s1) (sdrop n s2)"
   3.540 -  by (induct n arbitrary: s1 s2) auto
   3.541 -
   3.542 -lemma smap_szip_fst:
   3.543 -  "smap (\<lambda>x. f (fst x)) (szip s1 s2) = smap f s1"
   3.544 -  by (coinduction arbitrary: s1 s2) auto
   3.545 -
   3.546 -lemma smap_szip_snd:
   3.547 -  "smap (\<lambda>x. g (snd x)) (szip s1 s2) = smap g s2"
   3.548 -  by (coinduction arbitrary: s1 s2) auto
   3.549 -
   3.550 -
   3.551 -subsection {* zip via function *}
   3.552 -
   3.553 -primcorec smap2 where
   3.554 -  "shd (smap2 f s1 s2) = f (shd s1) (shd s2)"
   3.555 -| "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)"
   3.556 -
   3.557 -lemma smap2_unfold[code]:
   3.558 -  "smap2 f (a ## s1) (b ## s2) = f a b ## (smap2 f s1 s2)"
   3.559 -  by (subst smap2.ctr) simp
   3.560 -
   3.561 -lemma smap2_szip:
   3.562 -  "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
   3.563 -  by (coinduction arbitrary: s1 s2) auto
   3.564 -
   3.565 -lemma smap_smap2[simp]:
   3.566 -  "smap f (smap2 g s1 s2) = smap2 (\<lambda>x y. f (g x y)) s1 s2"
   3.567 -  unfolding smap2_szip stream.map_comp o_def split_def ..
   3.568 -
   3.569 -lemma smap2_alt:
   3.570 -  "(smap2 f s1 s2 = s) = (\<forall>n. f (s1 !! n) (s2 !! n) = s !! n)"
   3.571 -  unfolding smap2_szip smap_alt by auto
   3.572 -
   3.573 -lemma snth_smap2[simp]:
   3.574 -  "smap2 f s1 s2 !! n = f (s1 !! n) (s2 !! n)"
   3.575 -  by (induct n arbitrary: s1 s2) auto
   3.576 -
   3.577 -lemma stake_smap2[simp]:
   3.578 -  "stake n (smap2 f s1 s2) = map (split f) (zip (stake n s1) (stake n s2))"
   3.579 -  by (induct n arbitrary: s1 s2) auto
   3.580 -
   3.581 -lemma sdrop_smap2[simp]:
   3.582 -  "sdrop n (smap2 f s1 s2) = smap2 f (sdrop n s1) (sdrop n s2)"
   3.583 -  by (induct n arbitrary: s1 s2) auto
   3.584 -
   3.585 -end
     4.1 --- a/src/HOL/Datatype_Examples/Stream_Processor.thy	Tue Oct 07 10:34:24 2014 +0200
     4.2 +++ b/src/HOL/Datatype_Examples/Stream_Processor.thy	Tue Oct 07 10:48:29 2014 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  header {* Stream Processors---A Syntactic Representation of Continuous Functions on Streams *}
     4.5  
     4.6  theory Stream_Processor
     4.7 -imports Stream "~~/src/HOL/Library/BNF_Axiomatization"
     4.8 +imports "~~/src/HOL/Library/Stream" "~~/src/HOL/Library/BNF_Axiomatization"
     4.9  begin
    4.10  
    4.11  section {* Continuous Functions on Streams *}
     5.1 --- a/src/HOL/Library/Library.thy	Tue Oct 07 10:34:24 2014 +0200
     5.2 +++ b/src/HOL/Library/Library.thy	Tue Oct 07 10:48:29 2014 +0200
     5.3 @@ -65,6 +65,7 @@
     5.4    Saturated
     5.5    Set_Algebras
     5.6    State_Monad
     5.7 +  Stream
     5.8    Sublist
     5.9    Sum_of_Squares
    5.10    Transitive_Closure_Table
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/HOL/Library/Stream.thy	Tue Oct 07 10:48:29 2014 +0200
     6.3 @@ -0,0 +1,582 @@
     6.4 +(*  Title:      HOL/Library/Stream.thy
     6.5 +    Author:     Dmitriy Traytel, TU Muenchen
     6.6 +    Author:     Andrei Popescu, TU Muenchen
     6.7 +    Copyright   2012, 2013
     6.8 +
     6.9 +Infinite streams.
    6.10 +*)
    6.11 +
    6.12 +header {* Infinite Streams *}
    6.13 +
    6.14 +theory Stream
    6.15 +imports "~~/src/HOL/Library/Nat_Bijection"
    6.16 +begin
    6.17 +
    6.18 +codatatype (sset: 'a) stream =
    6.19 +  SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65)
    6.20 +for
    6.21 +  map: smap
    6.22 +  rel: stream_all2
    6.23 +
    6.24 +(*for code generation only*)
    6.25 +definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where
    6.26 +  [code_abbrev]: "smember x s \<longleftrightarrow> x \<in> sset s"
    6.27 +
    6.28 +lemma smember_code[code, simp]: "smember x (y ## s) = (if x = y then True else smember x s)"
    6.29 +  unfolding smember_def by auto
    6.30 +
    6.31 +hide_const (open) smember
    6.32 +
    6.33 +lemmas smap_simps[simp] = stream.map_sel
    6.34 +lemmas shd_sset = stream.set_sel(1)
    6.35 +lemmas stl_sset = stream.set_sel(2)
    6.36 +
    6.37 +theorem sset_induct[consumes 1, case_names shd stl, induct set: sset]:
    6.38 +  assumes "y \<in> sset s" and "\<And>s. P (shd s) s" and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s"
    6.39 +  shows "P y s"
    6.40 +using assms by induct (metis stream.sel(1), auto)
    6.41 +
    6.42 +
    6.43 +subsection {* prepend list to stream *}
    6.44 +
    6.45 +primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where
    6.46 +  "shift [] s = s"
    6.47 +| "shift (x # xs) s = x ## shift xs s"
    6.48 +
    6.49 +lemma smap_shift[simp]: "smap f (xs @- s) = map f xs @- smap f s"
    6.50 +  by (induct xs) auto
    6.51 +
    6.52 +lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s"
    6.53 +  by (induct xs) auto
    6.54 +
    6.55 +lemma shift_simps[simp]:
    6.56 +   "shd (xs @- s) = (if xs = [] then shd s else hd xs)"
    6.57 +   "stl (xs @- s) = (if xs = [] then stl s else tl xs @- s)"
    6.58 +  by (induct xs) auto
    6.59 +
    6.60 +lemma sset_shift[simp]: "sset (xs @- s) = set xs \<union> sset s"
    6.61 +  by (induct xs) auto
    6.62 +
    6.63 +lemma shift_left_inj[simp]: "xs @- s1 = xs @- s2 \<longleftrightarrow> s1 = s2"
    6.64 +  by (induct xs) auto
    6.65 +
    6.66 +
    6.67 +subsection {* set of streams with elements in some fixed set *}
    6.68 +
    6.69 +coinductive_set
    6.70 +  streams :: "'a set \<Rightarrow> 'a stream set"
    6.71 +  for A :: "'a set"
    6.72 +where
    6.73 +  Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A"
    6.74 +
    6.75 +lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A"
    6.76 +  by (induct w) auto
    6.77 +
    6.78 +lemma streams_Stream: "x ## s \<in> streams A \<longleftrightarrow> x \<in> A \<and> s \<in> streams A"
    6.79 +  by (auto elim: streams.cases)
    6.80 +
    6.81 +lemma streams_stl: "s \<in> streams A \<Longrightarrow> stl s \<in> streams A"
    6.82 +  by (cases s) (auto simp: streams_Stream)
    6.83 +
    6.84 +lemma streams_shd: "s \<in> streams A \<Longrightarrow> shd s \<in> A"
    6.85 +  by (cases s) (auto simp: streams_Stream)
    6.86 +
    6.87 +lemma sset_streams:
    6.88 +  assumes "sset s \<subseteq> A"
    6.89 +  shows "s \<in> streams A"
    6.90 +using assms proof (coinduction arbitrary: s)
    6.91 +  case streams then show ?case by (cases s) simp
    6.92 +qed
    6.93 +
    6.94 +lemma streams_sset:
    6.95 +  assumes "s \<in> streams A"
    6.96 +  shows "sset s \<subseteq> A"
    6.97 +proof
    6.98 +  fix x assume "x \<in> sset s" from this `s \<in> streams A` show "x \<in> A"
    6.99 +    by (induct s) (auto intro: streams_shd streams_stl)
   6.100 +qed
   6.101 +
   6.102 +lemma streams_iff_sset: "s \<in> streams A \<longleftrightarrow> sset s \<subseteq> A"
   6.103 +  by (metis sset_streams streams_sset)
   6.104 +
   6.105 +lemma streams_mono:  "s \<in> streams A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> s \<in> streams B"
   6.106 +  unfolding streams_iff_sset by auto
   6.107 +
   6.108 +lemma smap_streams: "s \<in> streams A \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<in> B) \<Longrightarrow> smap f s \<in> streams B"
   6.109 +  unfolding streams_iff_sset stream.set_map by auto
   6.110 +
   6.111 +lemma streams_empty: "streams {} = {}"
   6.112 +  by (auto elim: streams.cases)
   6.113 +
   6.114 +lemma streams_UNIV[simp]: "streams UNIV = UNIV"
   6.115 +  by (auto simp: streams_iff_sset)
   6.116 +
   6.117 +subsection {* nth, take, drop for streams *}
   6.118 +
   6.119 +primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where
   6.120 +  "s !! 0 = shd s"
   6.121 +| "s !! Suc n = stl s !! n"
   6.122 +
   6.123 +lemma snth_smap[simp]: "smap f s !! n = f (s !! n)"
   6.124 +  by (induct n arbitrary: s) auto
   6.125 +
   6.126 +lemma shift_snth_less[simp]: "p < length xs \<Longrightarrow> (xs @- s) !! p = xs ! p"
   6.127 +  by (induct p arbitrary: xs) (auto simp: hd_conv_nth nth_tl)
   6.128 +
   6.129 +lemma shift_snth_ge[simp]: "p \<ge> length xs \<Longrightarrow> (xs @- s) !! p = s !! (p - length xs)"
   6.130 +  by (induct p arbitrary: xs) (auto simp: Suc_diff_eq_diff_pred)
   6.131 +
   6.132 +lemma shift_snth: "(xs @- s) !! n = (if n < length xs then xs ! n else s !! (n - length xs))"
   6.133 +  by auto
   6.134 +
   6.135 +lemma snth_sset[simp]: "s !! n \<in> sset s"
   6.136 +  by (induct n arbitrary: s) (auto intro: shd_sset stl_sset)
   6.137 +
   6.138 +lemma sset_range: "sset s = range (snth s)"
   6.139 +proof (intro equalityI subsetI)
   6.140 +  fix x assume "x \<in> sset s"
   6.141 +  thus "x \<in> range (snth s)"
   6.142 +  proof (induct s)
   6.143 +    case (stl s x)
   6.144 +    then obtain n where "x = stl s !! n" by auto
   6.145 +    thus ?case by (auto intro: range_eqI[of _ _ "Suc n"])
   6.146 +  qed (auto intro: range_eqI[of _ _ 0])
   6.147 +qed auto
   6.148 +
   6.149 +primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where
   6.150 +  "stake 0 s = []"
   6.151 +| "stake (Suc n) s = shd s # stake n (stl s)"
   6.152 +
   6.153 +lemma length_stake[simp]: "length (stake n s) = n"
   6.154 +  by (induct n arbitrary: s) auto
   6.155 +
   6.156 +lemma stake_smap[simp]: "stake n (smap f s) = map f (stake n s)"
   6.157 +  by (induct n arbitrary: s) auto
   6.158 +
   6.159 +lemma take_stake: "take n (stake m s) = stake (min n m) s"
   6.160 +proof (induct m arbitrary: s n)
   6.161 +  case (Suc m) thus ?case by (cases n) auto
   6.162 +qed simp
   6.163 +
   6.164 +primrec sdrop :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where
   6.165 +  "sdrop 0 s = s"
   6.166 +| "sdrop (Suc n) s = sdrop n (stl s)"
   6.167 +
   6.168 +lemma sdrop_simps[simp]:
   6.169 +  "shd (sdrop n s) = s !! n" "stl (sdrop n s) = sdrop (Suc n) s"
   6.170 +  by (induct n arbitrary: s)  auto
   6.171 +
   6.172 +lemma sdrop_smap[simp]: "sdrop n (smap f s) = smap f (sdrop n s)"
   6.173 +  by (induct n arbitrary: s) auto
   6.174 +
   6.175 +lemma sdrop_stl: "sdrop n (stl s) = stl (sdrop n s)"
   6.176 +  by (induct n) auto
   6.177 +
   6.178 +lemma drop_stake: "drop n (stake m s) = stake (m - n) (sdrop n s)"
   6.179 +proof (induct m arbitrary: s n)
   6.180 +  case (Suc m) thus ?case by (cases n) auto
   6.181 +qed simp
   6.182 +
   6.183 +lemma stake_sdrop: "stake n s @- sdrop n s = s"
   6.184 +  by (induct n arbitrary: s) auto
   6.185 +
   6.186 +lemma id_stake_snth_sdrop:
   6.187 +  "s = stake i s @- s !! i ## sdrop (Suc i) s"
   6.188 +  by (subst stake_sdrop[symmetric, of _ i]) (metis sdrop_simps stream.collapse)
   6.189 +
   6.190 +lemma smap_alt: "smap f s = s' \<longleftrightarrow> (\<forall>n. f (s !! n) = s' !! n)" (is "?L = ?R")
   6.191 +proof
   6.192 +  assume ?R
   6.193 +  then have "\<And>n. smap f (sdrop n s) = sdrop n s'"
   6.194 +    by coinduction (auto intro: exI[of _ 0] simp del: sdrop.simps(2))
   6.195 +  then show ?L using sdrop.simps(1) by metis
   6.196 +qed auto
   6.197 +
   6.198 +lemma stake_invert_Nil[iff]: "stake n s = [] \<longleftrightarrow> n = 0"
   6.199 +  by (induct n) auto
   6.200 +
   6.201 +lemma sdrop_shift: "sdrop i (w @- s) = drop i w @- sdrop (i - length w) s"
   6.202 +  by (induct i arbitrary: w s) (auto simp: drop_tl drop_Suc neq_Nil_conv)
   6.203 +
   6.204 +lemma stake_shift: "stake i (w @- s) = take i w @ stake (i - length w) s"
   6.205 +  by (induct i arbitrary: w s) (auto simp: neq_Nil_conv)
   6.206 +
   6.207 +lemma stake_add[simp]: "stake m s @ stake n (sdrop m s) = stake (m + n) s"
   6.208 +  by (induct m arbitrary: s) auto
   6.209 +
   6.210 +lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s"
   6.211 +  by (induct m arbitrary: s) auto
   6.212 +
   6.213 +lemma sdrop_snth: "sdrop n s !! m = s !! (n + m)"
   6.214 +  by (induct n arbitrary: m s) auto
   6.215 +
   6.216 +partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 
   6.217 +  "sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)"
   6.218 +
   6.219 +lemma sdrop_while_SCons[code]:
   6.220 +  "sdrop_while P (a ## s) = (if P a then sdrop_while P s else a ## s)"
   6.221 +  by (subst sdrop_while.simps) simp
   6.222 +
   6.223 +lemma sdrop_while_sdrop_LEAST:
   6.224 +  assumes "\<exists>n. P (s !! n)"
   6.225 +  shows "sdrop_while (Not o P) s = sdrop (LEAST n. P (s !! n)) s"
   6.226 +proof -
   6.227 +  from assms obtain m where "P (s !! m)" "\<And>n. P (s !! n) \<Longrightarrow> m \<le> n"
   6.228 +    and *: "(LEAST n. P (s !! n)) = m" by atomize_elim (auto intro: LeastI Least_le)
   6.229 +  thus ?thesis unfolding *
   6.230 +  proof (induct m arbitrary: s)
   6.231 +    case (Suc m)
   6.232 +    hence "sdrop_while (Not \<circ> P) (stl s) = sdrop m (stl s)"
   6.233 +      by (metis (full_types) not_less_eq_eq snth.simps(2))
   6.234 +    moreover from Suc(3) have "\<not> (P (s !! 0))" by blast
   6.235 +    ultimately show ?case by (subst sdrop_while.simps) simp
   6.236 +  qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1))
   6.237 +qed
   6.238 +
   6.239 +primcorec sfilter where
   6.240 +  "shd (sfilter P s) = shd (sdrop_while (Not o P) s)"
   6.241 +| "stl (sfilter P s) = sfilter P (stl (sdrop_while (Not o P) s))"
   6.242 +
   6.243 +lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)"
   6.244 +proof (cases "P x")
   6.245 +  case True thus ?thesis by (subst sfilter.ctr) (simp add: sdrop_while_SCons)
   6.246 +next
   6.247 +  case False thus ?thesis by (subst (1 2) sfilter.ctr) (simp add: sdrop_while_SCons)
   6.248 +qed
   6.249 +
   6.250 +
   6.251 +subsection {* unary predicates lifted to streams *}
   6.252 +
   6.253 +definition "stream_all P s = (\<forall>p. P (s !! p))"
   6.254 +
   6.255 +lemma stream_all_iff[iff]: "stream_all P s \<longleftrightarrow> Ball (sset s) P"
   6.256 +  unfolding stream_all_def sset_range by auto
   6.257 +
   6.258 +lemma stream_all_shift[simp]: "stream_all P (xs @- s) = (list_all P xs \<and> stream_all P s)"
   6.259 +  unfolding stream_all_iff list_all_iff by auto
   6.260 +
   6.261 +lemma stream_all_Stream: "stream_all P (x ## X) \<longleftrightarrow> P x \<and> stream_all P X"
   6.262 +  by simp
   6.263 +
   6.264 +
   6.265 +subsection {* recurring stream out of a list *}
   6.266 +
   6.267 +primcorec cycle :: "'a list \<Rightarrow> 'a stream" where
   6.268 +  "shd (cycle xs) = hd xs"
   6.269 +| "stl (cycle xs) = cycle (tl xs @ [hd xs])"
   6.270 +
   6.271 +lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u"
   6.272 +proof (coinduction arbitrary: u)
   6.273 +  case Eq_stream then show ?case using stream.collapse[of "cycle u"]
   6.274 +    by (auto intro!: exI[of _ "tl u @ [hd u]"])
   6.275 +qed
   6.276 +
   6.277 +lemma cycle_Cons[code]: "cycle (x # xs) = x ## cycle (xs @ [x])"
   6.278 +  by (subst cycle.ctr) simp
   6.279 +
   6.280 +lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @- s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @- s"
   6.281 +  by (auto dest: arg_cong[of _ _ stl])
   6.282 +
   6.283 +lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s"
   6.284 +proof (induct n arbitrary: u)
   6.285 +  case (Suc n) thus ?case by (cases u) auto
   6.286 +qed auto
   6.287 +
   6.288 +lemma stake_cycle_le[simp]:
   6.289 +  assumes "u \<noteq> []" "n < length u"
   6.290 +  shows "stake n (cycle u) = take n u"
   6.291 +using min_absorb2[OF less_imp_le_nat[OF assms(2)]]
   6.292 +  by (subst cycle_decomp[OF assms(1)], subst stake_append) auto
   6.293 +
   6.294 +lemma stake_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> stake (length u) (cycle u) = u"
   6.295 +  by (subst cycle_decomp) (auto simp: stake_shift)
   6.296 +
   6.297 +lemma sdrop_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> sdrop (length u) (cycle u) = cycle u"
   6.298 +  by (subst cycle_decomp) (auto simp: sdrop_shift)
   6.299 +
   6.300 +lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
   6.301 +   stake n (cycle u) = concat (replicate (n div length u) u)"
   6.302 +  by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric])
   6.303 +
   6.304 +lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow>
   6.305 +   sdrop n (cycle u) = cycle u"
   6.306 +  by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric])
   6.307 +
   6.308 +lemma stake_cycle: "u \<noteq> [] \<Longrightarrow>
   6.309 +   stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u"
   6.310 +  by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto
   6.311 +
   6.312 +lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)"
   6.313 +  by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric])
   6.314 +
   6.315 +
   6.316 +subsection {* iterated application of a function *}
   6.317 +
   6.318 +primcorec siterate where
   6.319 +  "shd (siterate f x) = x"
   6.320 +| "stl (siterate f x) = siterate f (f x)"
   6.321 +
   6.322 +lemma stake_Suc: "stake (Suc n) s = stake n s @ [s !! n]"
   6.323 +  by (induct n arbitrary: s) auto
   6.324 +
   6.325 +lemma snth_siterate[simp]: "siterate f x !! n = (f^^n) x"
   6.326 +  by (induct n arbitrary: x) (auto simp: funpow_swap1)
   6.327 +
   6.328 +lemma sdrop_siterate[simp]: "sdrop n (siterate f x) = siterate f ((f^^n) x)"
   6.329 +  by (induct n arbitrary: x) (auto simp: funpow_swap1)
   6.330 +
   6.331 +lemma stake_siterate[simp]: "stake n (siterate f x) = map (\<lambda>n. (f^^n) x) [0 ..< n]"
   6.332 +  by (induct n arbitrary: x) (auto simp del: stake.simps(2) simp: stake_Suc)
   6.333 +
   6.334 +lemma sset_siterate: "sset (siterate f x) = {(f^^n) x | n. True}"
   6.335 +  by (auto simp: sset_range)
   6.336 +
   6.337 +lemma smap_siterate: "smap f (siterate f x) = siterate f (f x)"
   6.338 +  by (coinduction arbitrary: x) auto
   6.339 +
   6.340 +
   6.341 +subsection {* stream repeating a single element *}
   6.342 +
   6.343 +abbreviation "sconst \<equiv> siterate id"
   6.344 +
   6.345 +lemma shift_replicate_sconst[simp]: "replicate n x @- sconst x = sconst x"
   6.346 +  by (subst (3) stake_sdrop[symmetric]) (simp add: map_replicate_trivial)
   6.347 +
   6.348 +lemma sset_sconst[simp]: "sset (sconst x) = {x}"
   6.349 +  by (simp add: sset_siterate)
   6.350 +
   6.351 +lemma sconst_alt: "s = sconst x \<longleftrightarrow> sset s = {x}"
   6.352 +proof
   6.353 +  assume "sset s = {x}"
   6.354 +  then show "s = sconst x"
   6.355 +  proof (coinduction arbitrary: s)
   6.356 +    case Eq_stream
   6.357 +    then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (case_tac [!] s) auto
   6.358 +    then have "sset (stl s) = {x}" by (cases "stl s") auto
   6.359 +    with `shd s = x` show ?case by auto
   6.360 +  qed
   6.361 +qed simp
   6.362 +
   6.363 +lemma same_cycle: "sconst x = cycle [x]"
   6.364 +  by coinduction auto
   6.365 +
   6.366 +lemma smap_sconst: "smap f (sconst x) = sconst (f x)"
   6.367 +  by coinduction auto
   6.368 +
   6.369 +lemma sconst_streams: "x \<in> A \<Longrightarrow> sconst x \<in> streams A"
   6.370 +  by (simp add: streams_iff_sset)
   6.371 +
   6.372 +
   6.373 +subsection {* stream of natural numbers *}
   6.374 +
   6.375 +abbreviation "fromN \<equiv> siterate Suc"
   6.376 +
   6.377 +abbreviation "nats \<equiv> fromN 0"
   6.378 +
   6.379 +lemma sset_fromN[simp]: "sset (fromN n) = {n ..}"
   6.380 +  by (auto simp add: sset_siterate le_iff_add)
   6.381 +
   6.382 +lemma stream_smap_fromN: "s = smap (\<lambda>j. let i = j - n in s !! i) (fromN n)"
   6.383 +  by (coinduction arbitrary: s n)
   6.384 +    (force simp: neq_Nil_conv Let_def snth.simps(2)[symmetric] Suc_diff_Suc
   6.385 +      intro: stream.map_cong split: if_splits simp del: snth.simps(2))
   6.386 +
   6.387 +lemma stream_smap_nats: "s = smap (snth s) nats"
   6.388 +  using stream_smap_fromN[where n = 0] by simp
   6.389 +
   6.390 +
   6.391 +subsection {* flatten a stream of lists *}
   6.392 +
   6.393 +primcorec flat where
   6.394 +  "shd (flat ws) = hd (shd ws)"
   6.395 +| "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)"
   6.396 +
   6.397 +lemma flat_Cons[simp, code]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)"
   6.398 +  by (subst flat.ctr) simp
   6.399 +
   6.400 +lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws"
   6.401 +  by (induct xs) auto
   6.402 +
   6.403 +lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)"
   6.404 +  by (cases ws) auto
   6.405 +
   6.406 +lemma flat_snth: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then 
   6.407 +  shd s ! n else flat (stl s) !! (n - length (shd s)))"
   6.408 +  by (metis flat_unfold not_less shd_sset shift_snth_ge shift_snth_less)
   6.409 +
   6.410 +lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> 
   6.411 +  sset (flat s) = (\<Union>xs \<in> sset s. set xs)" (is "?P \<Longrightarrow> ?L = ?R")
   6.412 +proof safe
   6.413 +  fix x assume ?P "x : ?L"
   6.414 +  then obtain m where "x = flat s !! m" by (metis image_iff sset_range)
   6.415 +  with `?P` obtain n m' where "x = s !! n ! m'" "m' < length (s !! n)"
   6.416 +  proof (atomize_elim, induct m arbitrary: s rule: less_induct)
   6.417 +    case (less y)
   6.418 +    thus ?case
   6.419 +    proof (cases "y < length (shd s)")
   6.420 +      case True thus ?thesis by (metis flat_snth less(2,3) snth.simps(1))
   6.421 +    next
   6.422 +      case False
   6.423 +      hence "x = flat (stl s) !! (y - length (shd s))" by (metis less(2,3) flat_snth)
   6.424 +      moreover
   6.425 +      { from less(2) have *: "length (shd s) > 0" by (cases s) simp_all
   6.426 +        with False have "y > 0" by (cases y) simp_all
   6.427 +        with * have "y - length (shd s) < y" by simp
   6.428 +      }
   6.429 +      moreover have "\<forall>xs \<in> sset (stl s). xs \<noteq> []" using less(2) by (cases s) auto
   6.430 +      ultimately have "\<exists>n m'. x = stl s !! n ! m' \<and> m' < length (stl s !! n)" by (intro less(1)) auto
   6.431 +      thus ?thesis by (metis snth.simps(2))
   6.432 +    qed
   6.433 +  qed
   6.434 +  thus "x \<in> ?R" by (auto simp: sset_range dest!: nth_mem)
   6.435 +next
   6.436 +  fix x xs assume "xs \<in> sset s" ?P "x \<in> set xs" thus "x \<in> ?L"
   6.437 +    by (induct rule: sset_induct)
   6.438 +      (metis UnI1 flat_unfold shift.simps(1) sset_shift,
   6.439 +       metis UnI2 flat_unfold shd_sset stl_sset sset_shift)
   6.440 +qed
   6.441 +
   6.442 +
   6.443 +subsection {* merge a stream of streams *}
   6.444 +
   6.445 +definition smerge :: "'a stream stream \<Rightarrow> 'a stream" where
   6.446 +  "smerge ss = flat (smap (\<lambda>n. map (\<lambda>s. s !! n) (stake (Suc n) ss) @ stake n (ss !! n)) nats)"
   6.447 +
   6.448 +lemma stake_nth[simp]: "m < n \<Longrightarrow> stake n s ! m = s !! m"
   6.449 +  by (induct n arbitrary: s m) (auto simp: nth_Cons', metis Suc_pred snth.simps(2))
   6.450 +
   6.451 +lemma snth_sset_smerge: "ss !! n !! m \<in> sset (smerge ss)"
   6.452 +proof (cases "n \<le> m")
   6.453 +  case False thus ?thesis unfolding smerge_def
   6.454 +    by (subst sset_flat)
   6.455 +      (auto simp: stream.set_map in_set_conv_nth simp del: stake.simps
   6.456 +        intro!: exI[of _ n, OF disjI2] exI[of _ m, OF mp])
   6.457 +next
   6.458 +  case True thus ?thesis unfolding smerge_def
   6.459 +    by (subst sset_flat)
   6.460 +      (auto simp: stream.set_map in_set_conv_nth image_iff simp del: stake.simps snth.simps
   6.461 +        intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp])
   6.462 +qed
   6.463 +
   6.464 +lemma sset_smerge: "sset (smerge ss) = UNION (sset ss) sset"
   6.465 +proof safe
   6.466 +  fix x assume "x \<in> sset (smerge ss)"
   6.467 +  thus "x \<in> UNION (sset ss) sset"
   6.468 +    unfolding smerge_def by (subst (asm) sset_flat)
   6.469 +      (auto simp: stream.set_map in_set_conv_nth sset_range simp del: stake.simps, fast+)
   6.470 +next
   6.471 +  fix s x assume "s \<in> sset ss" "x \<in> sset s"
   6.472 +  thus "x \<in> sset (smerge ss)" using snth_sset_smerge by (auto simp: sset_range)
   6.473 +qed
   6.474 +
   6.475 +
   6.476 +subsection {* product of two streams *}
   6.477 +
   6.478 +definition sproduct :: "'a stream \<Rightarrow> 'b stream \<Rightarrow> ('a \<times> 'b) stream" where
   6.479 +  "sproduct s1 s2 = smerge (smap (\<lambda>x. smap (Pair x) s2) s1)"
   6.480 +
   6.481 +lemma sset_sproduct: "sset (sproduct s1 s2) = sset s1 \<times> sset s2"
   6.482 +  unfolding sproduct_def sset_smerge by (auto simp: stream.set_map)
   6.483 +
   6.484 +
   6.485 +subsection {* interleave two streams *}
   6.486 +
   6.487 +primcorec sinterleave where
   6.488 +  "shd (sinterleave s1 s2) = shd s1"
   6.489 +| "stl (sinterleave s1 s2) = sinterleave s2 (stl s1)"
   6.490 +
   6.491 +lemma sinterleave_code[code]:
   6.492 +  "sinterleave (x ## s1) s2 = x ## sinterleave s2 s1"
   6.493 +  by (subst sinterleave.ctr) simp
   6.494 +
   6.495 +lemma sinterleave_snth[simp]:
   6.496 +  "even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)"
   6.497 +   "odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)"
   6.498 +  by (induct n arbitrary: s1 s2)
   6.499 +    (auto dest: even_nat_Suc_div_2 odd_nat_plus_one_div_two[folded nat_2])
   6.500 +
   6.501 +lemma sset_sinterleave: "sset (sinterleave s1 s2) = sset s1 \<union> sset s2"
   6.502 +proof (intro equalityI subsetI)
   6.503 +  fix x assume "x \<in> sset (sinterleave s1 s2)"
   6.504 +  then obtain n where "x = sinterleave s1 s2 !! n" unfolding sset_range by blast
   6.505 +  thus "x \<in> sset s1 \<union> sset s2" by (cases "even n") auto
   6.506 +next
   6.507 +  fix x assume "x \<in> sset s1 \<union> sset s2"
   6.508 +  thus "x \<in> sset (sinterleave s1 s2)"
   6.509 +  proof
   6.510 +    assume "x \<in> sset s1"
   6.511 +    then obtain n where "x = s1 !! n" unfolding sset_range by blast
   6.512 +    hence "sinterleave s1 s2 !! (2 * n) = x" by simp
   6.513 +    thus ?thesis unfolding sset_range by blast
   6.514 +  next
   6.515 +    assume "x \<in> sset s2"
   6.516 +    then obtain n where "x = s2 !! n" unfolding sset_range by blast
   6.517 +    hence "sinterleave s1 s2 !! (2 * n + 1) = x" by simp
   6.518 +    thus ?thesis unfolding sset_range by blast
   6.519 +  qed
   6.520 +qed
   6.521 +
   6.522 +
   6.523 +subsection {* zip *}
   6.524 +
   6.525 +primcorec szip where
   6.526 +  "shd (szip s1 s2) = (shd s1, shd s2)"
   6.527 +| "stl (szip s1 s2) = szip (stl s1) (stl s2)"
   6.528 +
   6.529 +lemma szip_unfold[code]: "szip (a ## s1) (b ## s2) = (a, b) ## (szip s1 s2)"
   6.530 +  by (subst szip.ctr) simp
   6.531 +
   6.532 +lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)"
   6.533 +  by (induct n arbitrary: s1 s2) auto
   6.534 +
   6.535 +lemma stake_szip[simp]:
   6.536 +  "stake n (szip s1 s2) = zip (stake n s1) (stake n s2)"
   6.537 +  by (induct n arbitrary: s1 s2) auto
   6.538 +
   6.539 +lemma sdrop_szip[simp]: "sdrop n (szip s1 s2) = szip (sdrop n s1) (sdrop n s2)"
   6.540 +  by (induct n arbitrary: s1 s2) auto
   6.541 +
   6.542 +lemma smap_szip_fst:
   6.543 +  "smap (\<lambda>x. f (fst x)) (szip s1 s2) = smap f s1"
   6.544 +  by (coinduction arbitrary: s1 s2) auto
   6.545 +
   6.546 +lemma smap_szip_snd:
   6.547 +  "smap (\<lambda>x. g (snd x)) (szip s1 s2) = smap g s2"
   6.548 +  by (coinduction arbitrary: s1 s2) auto
   6.549 +
   6.550 +
   6.551 +subsection {* zip via function *}
   6.552 +
   6.553 +primcorec smap2 where
   6.554 +  "shd (smap2 f s1 s2) = f (shd s1) (shd s2)"
   6.555 +| "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)"
   6.556 +
   6.557 +lemma smap2_unfold[code]:
   6.558 +  "smap2 f (a ## s1) (b ## s2) = f a b ## (smap2 f s1 s2)"
   6.559 +  by (subst smap2.ctr) simp
   6.560 +
   6.561 +lemma smap2_szip:
   6.562 +  "smap2 f s1 s2 = smap (split f) (szip s1 s2)"
   6.563 +  by (coinduction arbitrary: s1 s2) auto
   6.564 +
   6.565 +lemma smap_smap2[simp]:
   6.566 +  "smap f (smap2 g s1 s2) = smap2 (\<lambda>x y. f (g x y)) s1 s2"
   6.567 +  unfolding smap2_szip stream.map_comp o_def split_def ..
   6.568 +
   6.569 +lemma smap2_alt:
   6.570 +  "(smap2 f s1 s2 = s) = (\<forall>n. f (s1 !! n) (s2 !! n) = s !! n)"
   6.571 +  unfolding smap2_szip smap_alt by auto
   6.572 +
   6.573 +lemma snth_smap2[simp]:
   6.574 +  "smap2 f s1 s2 !! n = f (s1 !! n) (s2 !! n)"
   6.575 +  by (induct n arbitrary: s1 s2) auto
   6.576 +
   6.577 +lemma stake_smap2[simp]:
   6.578 +  "stake n (smap2 f s1 s2) = map (split f) (zip (stake n s1) (stake n s2))"
   6.579 +  by (induct n arbitrary: s1 s2) auto
   6.580 +
   6.581 +lemma sdrop_smap2[simp]:
   6.582 +  "sdrop n (smap2 f s1 s2) = smap2 f (sdrop n s1) (sdrop n s2)"
   6.583 +  by (induct n arbitrary: s1 s2) auto
   6.584 +
   6.585 +end
     7.1 --- a/src/HOL/Probability/Stream_Space.thy	Tue Oct 07 10:34:24 2014 +0200
     7.2 +++ b/src/HOL/Probability/Stream_Space.thy	Tue Oct 07 10:48:29 2014 +0200
     7.3 @@ -4,7 +4,7 @@
     7.4  theory Stream_Space
     7.5  imports
     7.6    Infinite_Product_Measure
     7.7 -  "~~/src/HOL/Datatype_Examples/Stream"
     7.8 +  "~~/src/HOL/Library/Stream"
     7.9  begin
    7.10  
    7.11  lemma stream_eq_Stream_iff: "s = x ## t \<longleftrightarrow> (shd s = x \<and> stl s = t)"