author  traytel 
Thu, 05 Jun 2014 11:41:38 +0200  
changeset 57175  ca3475504557 
parent 55873  aa50d903e0a7 
child 57206  d9be905d6283 
permissions  rwrr 
55075  1 
(* Title: HOL/BNF_Examples/Stream.thy 
50518  2 
Author: Dmitriy Traytel, TU Muenchen 
3 
Author: Andrei Popescu, TU Muenchen 

51778  4 
Copyright 2012, 2013 
50518  5 

6 
Infinite streams. 

7 
*) 

8 

9 
header {* Infinite Streams *} 

10 

11 
theory Stream 

55076  12 
imports "~~/src/HOL/Library/Nat_Bijection" 
50518  13 
begin 
14 

51804
be6e703908f4
renamed BNF "(co)data" commands to names that are closer to their final names
blanchet
parents:
51788
diff
changeset

15 
codatatype (sset: 'a) stream (map: smap rel: stream_all2) = 
54720
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

16 
SCons (shd: 'a) (stl: "'a stream") (infixr "##" 65) 
51409  17 

51462  18 
(*for code generation only*) 
19 
definition smember :: "'a \<Rightarrow> 'a stream \<Rightarrow> bool" where 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

20 
[code_abbrev]: "smember x s \<longleftrightarrow> x \<in> sset s" 
51462  21 

54720
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

22 
lemma smember_code[code, simp]: "smember x (y ## s) = (if x = y then True else smember x s)" 
51462  23 
unfolding smember_def by auto 
24 

25 
hide_const (open) smember 

26 

50518  27 
(* TODO: Provide by the package*) 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

28 
theorem sset_induct: 
55804  29 
assumes Base: "\<And>s. P (shd s) s" and Step: "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s" 
30 
shows "\<forall>y \<in> sset s. P y s" 

31 
proof (rule stream.dtor_set_induct) 

32 
fix a :: 'a and s :: "'a stream" 

33 
assume "a \<in> set1_pre_stream (dtor_stream s)" 

34 
then have "a = shd s" 

35 
by (cases "dtor_stream s") 

55873  36 
(auto simp: BNF_Comp.id_bnf_comp_def shd_def fsts_def set1_pre_stream_def stream.dtor_ctor SCons_def 
37 
split: stream.splits) 

55804  38 
with Base show "P a s" by simp 
39 
next 

40 
fix a :: 'a and s' :: "'a stream" and s :: "'a stream" 

41 
assume "s' \<in> set2_pre_stream (dtor_stream s)" and prems: "a \<in> sset s'" "P a s'" 

42 
then have "s' = stl s" 

43 
by (cases "dtor_stream s") 

55873  44 
(auto simp: BNF_Comp.id_bnf_comp_def stl_def snds_def set2_pre_stream_def stream.dtor_ctor SCons_def 
45 
split: stream.splits) 

55804  46 
with Step prems show "P a s" by simp 
47 
qed 

51141  48 

57175  49 
lemmas smap_simps[simp] = stream.sel_map 
50 
lemmas shd_sset = stream.sel_set(1) 

51 
lemmas stl_sset = stream.sel_set(2) 

50518  52 

53 
(* only for the nonmutual case: *) 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

54 
theorem sset_induct1[consumes 1, case_names shd stl, induct set: "sset"]: 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

55 
assumes "y \<in> sset s" and "\<And>s. P (shd s) s" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

56 
and "\<And>s y. \<lbrakk>y \<in> sset (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s" 
50518  57 
shows "P y s" 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

58 
using assms sset_induct by blast 
50518  59 
(* end TODO *) 
60 

61 

62 
subsection {* prepend list to stream *} 

63 

64 
primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@" 65) where 

65 
"shift [] s = s" 

51023
550f265864e3
infix syntax for streams (reflecting the one for lists)
traytel
parents:
50518
diff
changeset

66 
 "shift (x # xs) s = x ## shift xs s" 
50518  67 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

68 
lemma smap_shift[simp]: "smap f (xs @ s) = map f xs @ smap f s" 
51353  69 
by (induct xs) auto 
70 

50518  71 
lemma shift_append[simp]: "(xs @ ys) @ s = xs @ ys @ s" 
51141  72 
by (induct xs) auto 
50518  73 

74 
lemma shift_simps[simp]: 

75 
"shd (xs @ s) = (if xs = [] then shd s else hd xs)" 

76 
"stl (xs @ s) = (if xs = [] then stl s else tl xs @ s)" 

51141  77 
by (induct xs) auto 
50518  78 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

79 
lemma sset_shift[simp]: "sset (xs @ s) = set xs \<union> sset s" 
51141  80 
by (induct xs) auto 
50518  81 

51352  82 
lemma shift_left_inj[simp]: "xs @ s1 = xs @ s2 \<longleftrightarrow> s1 = s2" 
83 
by (induct xs) auto 

84 

50518  85 

54469  86 
subsection {* set of streams with elements in some fixed set *} 
50518  87 

88 
coinductive_set 

54469  89 
streams :: "'a set \<Rightarrow> 'a stream set" 
50518  90 
for A :: "'a set" 
91 
where 

51023
550f265864e3
infix syntax for streams (reflecting the one for lists)
traytel
parents:
50518
diff
changeset

92 
Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A" 
50518  93 

94 
lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @ s \<in> streams A" 

51141  95 
by (induct w) auto 
50518  96 

54469  97 
lemma streams_Stream: "x ## s \<in> streams A \<longleftrightarrow> x \<in> A \<and> s \<in> streams A" 
98 
by (auto elim: streams.cases) 

99 

100 
lemma streams_stl: "s \<in> streams A \<Longrightarrow> stl s \<in> streams A" 

101 
by (cases s) (auto simp: streams_Stream) 

102 

103 
lemma streams_shd: "s \<in> streams A \<Longrightarrow> shd s \<in> A" 

104 
by (cases s) (auto simp: streams_Stream) 

105 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

106 
lemma sset_streams: 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

107 
assumes "sset s \<subseteq> A" 
50518  108 
shows "s \<in> streams A" 
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

109 
using assms proof (coinduction arbitrary: s) 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

110 
case streams then show ?case by (cases s) simp 
50518  111 
qed 
112 

54469  113 
lemma streams_sset: 
114 
assumes "s \<in> streams A" 

115 
shows "sset s \<subseteq> A" 

116 
proof 

117 
fix x assume "x \<in> sset s" from this `s \<in> streams A` show "x \<in> A" 

118 
by (induct s) (auto intro: streams_shd streams_stl) 

119 
qed 

120 

121 
lemma streams_iff_sset: "s \<in> streams A \<longleftrightarrow> sset s \<subseteq> A" 

122 
by (metis sset_streams streams_sset) 

123 

124 
lemma streams_mono: "s \<in> streams A \<Longrightarrow> A \<subseteq> B \<Longrightarrow> s \<in> streams B" 

125 
unfolding streams_iff_sset by auto 

126 

127 
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" 

128 
unfolding streams_iff_sset stream.set_map by auto 

129 

130 
lemma streams_empty: "streams {} = {}" 

131 
by (auto elim: streams.cases) 

132 

133 
lemma streams_UNIV[simp]: "streams UNIV = UNIV" 

134 
by (auto simp: streams_iff_sset) 

50518  135 

51141  136 
subsection {* nth, take, drop for streams *} 
137 

138 
primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where 

139 
"s !! 0 = shd s" 

140 
 "s !! Suc n = stl s !! n" 

141 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

142 
lemma snth_smap[simp]: "smap f s !! n = f (s !! n)" 
51141  143 
by (induct n arbitrary: s) auto 
144 

145 
lemma shift_snth_less[simp]: "p < length xs \<Longrightarrow> (xs @ s) !! p = xs ! p" 

146 
by (induct p arbitrary: xs) (auto simp: hd_conv_nth nth_tl) 

147 

148 
lemma shift_snth_ge[simp]: "p \<ge> length xs \<Longrightarrow> (xs @ s) !! p = s !! (p  length xs)" 

149 
by (induct p arbitrary: xs) (auto simp: Suc_diff_eq_diff_pred) 

150 

57175  151 
lemma shift_snth: "(xs @ s) !! n = (if n < length xs then xs ! n else s !! (n  length xs))" 
152 
by auto 

153 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

154 
lemma snth_sset[simp]: "s !! n \<in> sset s" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

155 
by (induct n arbitrary: s) (auto intro: shd_sset stl_sset) 
51141  156 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

157 
lemma sset_range: "sset s = range (snth s)" 
51141  158 
proof (intro equalityI subsetI) 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

159 
fix x assume "x \<in> sset s" 
51141  160 
thus "x \<in> range (snth s)" 
161 
proof (induct s) 

162 
case (stl s x) 

163 
then obtain n where "x = stl s !! n" by auto 

164 
thus ?case by (auto intro: range_eqI[of _ _ "Suc n"]) 

165 
qed (auto intro: range_eqI[of _ _ 0]) 

166 
qed auto 

50518  167 

168 
primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where 

169 
"stake 0 s = []" 

170 
 "stake (Suc n) s = shd s # stake n (stl s)" 

171 

51141  172 
lemma length_stake[simp]: "length (stake n s) = n" 
173 
by (induct n arbitrary: s) auto 

174 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

175 
lemma stake_smap[simp]: "stake n (smap f s) = map f (stake n s)" 
51141  176 
by (induct n arbitrary: s) auto 
177 

57175  178 
lemma take_stake: "take n (stake m s) = stake (min n m) s" 
179 
proof (induct m arbitrary: s n) 

180 
case (Suc m) thus ?case by (cases n) auto 

181 
qed simp 

182 

50518  183 
primrec sdrop :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 
184 
"sdrop 0 s = s" 

185 
 "sdrop (Suc n) s = sdrop n (stl s)" 

186 

51141  187 
lemma sdrop_simps[simp]: 
188 
"shd (sdrop n s) = s !! n" "stl (sdrop n s) = sdrop (Suc n) s" 

189 
by (induct n arbitrary: s) auto 

190 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

191 
lemma sdrop_smap[simp]: "sdrop n (smap f s) = smap f (sdrop n s)" 
51141  192 
by (induct n arbitrary: s) auto 
50518  193 

51352  194 
lemma sdrop_stl: "sdrop n (stl s) = stl (sdrop n s)" 
195 
by (induct n) auto 

196 

57175  197 
lemma drop_stake: "drop n (stake m s) = stake (m  n) (sdrop n s)" 
198 
proof (induct m arbitrary: s n) 

199 
case (Suc m) thus ?case by (cases n) auto 

200 
qed simp 

201 

50518  202 
lemma stake_sdrop: "stake n s @ sdrop n s = s" 
51141  203 
by (induct n arbitrary: s) auto 
204 

205 
lemma id_stake_snth_sdrop: 

206 
"s = stake i s @ s !! i ## sdrop (Suc i) s" 

207 
by (subst stake_sdrop[symmetric, of _ i]) (metis sdrop_simps stream.collapse) 

50518  208 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

209 
lemma smap_alt: "smap f s = s' \<longleftrightarrow> (\<forall>n. f (s !! n) = s' !! n)" (is "?L = ?R") 
51141  210 
proof 
211 
assume ?R 

54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

212 
then have "\<And>n. smap f (sdrop n s) = sdrop n s'" 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

213 
by coinduction (auto intro: exI[of _ 0] simp del: sdrop.simps(2)) 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

214 
then show ?L using sdrop.simps(1) by metis 
51141  215 
qed auto 
216 

217 
lemma stake_invert_Nil[iff]: "stake n s = [] \<longleftrightarrow> n = 0" 

218 
by (induct n) auto 

50518  219 

57175  220 
lemma sdrop_shift: "sdrop i (w @ s) = drop i w @ sdrop (i  length w) s" 
221 
by (induct i arbitrary: w s) (auto simp: drop_tl drop_Suc neq_Nil_conv) 

50518  222 

57175  223 
lemma stake_shift: "stake i (w @ s) = take i w @ stake (i  length w) s" 
224 
by (induct i arbitrary: w s) (auto simp: neq_Nil_conv) 

50518  225 

226 
lemma stake_add[simp]: "stake m s @ stake n (sdrop m s) = stake (m + n) s" 

51141  227 
by (induct m arbitrary: s) auto 
50518  228 

229 
lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s" 

51141  230 
by (induct m arbitrary: s) auto 
231 

57175  232 
lemma sdrop_snth: "sdrop n s !! m = s !! (n + m)" 
233 
by (induct n arbitrary: m s) auto 

234 

51430  235 
partial_function (tailrec) sdrop_while :: "('a \<Rightarrow> bool) \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where 
236 
"sdrop_while P s = (if P (shd s) then sdrop_while P (stl s) else s)" 

237 

54720
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

238 
lemma sdrop_while_SCons[code]: 
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

239 
"sdrop_while P (a ## s) = (if P a then sdrop_while P s else a ## s)" 
51430  240 
by (subst sdrop_while.simps) simp 
241 

242 
lemma sdrop_while_sdrop_LEAST: 

243 
assumes "\<exists>n. P (s !! n)" 

244 
shows "sdrop_while (Not o P) s = sdrop (LEAST n. P (s !! n)) s" 

245 
proof  

246 
from assms obtain m where "P (s !! m)" "\<And>n. P (s !! n) \<Longrightarrow> m \<le> n" 

247 
and *: "(LEAST n. P (s !! n)) = m" by atomize_elim (auto intro: LeastI Least_le) 

248 
thus ?thesis unfolding * 

249 
proof (induct m arbitrary: s) 

250 
case (Suc m) 

251 
hence "sdrop_while (Not \<circ> P) (stl s) = sdrop m (stl s)" 

252 
by (metis (full_types) not_less_eq_eq snth.simps(2)) 

253 
moreover from Suc(3) have "\<not> (P (s !! 0))" by blast 

254 
ultimately show ?case by (subst sdrop_while.simps) simp 

255 
qed (metis comp_apply sdrop.simps(1) sdrop_while.simps snth.simps(1)) 

256 
qed 

257 

54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

258 
primcorec sfilter where 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

259 
"shd (sfilter P s) = shd (sdrop_while (Not o P) s)" 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

260 
 "stl (sfilter P s) = sfilter P (stl (sdrop_while (Not o P) s))" 
52905  261 

262 
lemma sfilter_Stream: "sfilter P (x ## s) = (if P x then x ## sfilter P s else sfilter P s)" 

263 
proof (cases "P x") 

54720
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

264 
case True thus ?thesis by (subst sfilter.ctr) (simp add: sdrop_while_SCons) 
52905  265 
next 
54720
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

266 
case False thus ?thesis by (subst (1 2) sfilter.ctr) (simp add: sdrop_while_SCons) 
52905  267 
qed 
268 

51141  269 

270 
subsection {* unary predicates lifted to streams *} 

271 

272 
definition "stream_all P s = (\<forall>p. P (s !! p))" 

273 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

274 
lemma stream_all_iff[iff]: "stream_all P s \<longleftrightarrow> Ball (sset s) P" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

275 
unfolding stream_all_def sset_range by auto 
51141  276 

277 
lemma stream_all_shift[simp]: "stream_all P (xs @ s) = (list_all P xs \<and> stream_all P s)" 

278 
unfolding stream_all_iff list_all_iff by auto 

279 

54469  280 
lemma stream_all_Stream: "stream_all P (x ## X) \<longleftrightarrow> P x \<and> stream_all P X" 
281 
by simp 

282 

51141  283 

284 
subsection {* recurring stream out of a list *} 

285 

54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

286 
primcorec cycle :: "'a list \<Rightarrow> 'a stream" where 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

287 
"shd (cycle xs) = hd xs" 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

288 
 "stl (cycle xs) = cycle (tl xs @ [hd xs])" 
54720
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

289 

51141  290 
lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @ cycle u" 
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

291 
proof (coinduction arbitrary: u) 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

292 
case Eq_stream then show ?case using stream.collapse[of "cycle u"] 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

293 
by (auto intro!: exI[of _ "tl u @ [hd u]"]) 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

294 
qed 
51141  295 

51409  296 
lemma cycle_Cons[code]: "cycle (x # xs) = x ## cycle (xs @ [x])" 
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

297 
by (subst cycle.ctr) simp 
50518  298 

299 
lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @ s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @ s" 

51141  300 
by (auto dest: arg_cong[of _ _ stl]) 
50518  301 

302 
lemma stake_append: "stake n (u @ s) = take (min (length u) n) u @ stake (n  length u) s" 

303 
proof (induct n arbitrary: u) 

304 
case (Suc n) thus ?case by (cases u) auto 

305 
qed auto 

306 

307 
lemma stake_cycle_le[simp]: 

308 
assumes "u \<noteq> []" "n < length u" 

309 
shows "stake n (cycle u) = take n u" 

310 
using min_absorb2[OF less_imp_le_nat[OF assms(2)]] 

51141  311 
by (subst cycle_decomp[OF assms(1)], subst stake_append) auto 
50518  312 

313 
lemma stake_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> stake (length u) (cycle u) = u" 

57175  314 
by (subst cycle_decomp) (auto simp: stake_shift) 
50518  315 

316 
lemma sdrop_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> sdrop (length u) (cycle u) = cycle u" 

57175  317 
by (subst cycle_decomp) (auto simp: sdrop_shift) 
50518  318 

319 
lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow> 

320 
stake n (cycle u) = concat (replicate (n div length u) u)" 

51141  321 
by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric]) 
50518  322 

323 
lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow> 

324 
sdrop n (cycle u) = cycle u" 

51141  325 
by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric]) 
50518  326 

327 
lemma stake_cycle: "u \<noteq> [] \<Longrightarrow> 

328 
stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u" 

51141  329 
by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto 
50518  330 

331 
lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)" 

51141  332 
by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric]) 
333 

334 

54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

335 
subsection {* iterated application of a function *} 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

336 

c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

337 
primcorec siterate where 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

338 
"shd (siterate f x) = x" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

339 
 "stl (siterate f x) = siterate f (f x)" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

340 

c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

341 
lemma stake_Suc: "stake (Suc n) s = stake n s @ [s !! n]" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

342 
by (induct n arbitrary: s) auto 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

343 

c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

344 
lemma snth_siterate[simp]: "siterate f x !! n = (f^^n) x" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

345 
by (induct n arbitrary: x) (auto simp: funpow_swap1) 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

346 

c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

347 
lemma sdrop_siterate[simp]: "sdrop n (siterate f x) = siterate f ((f^^n) x)" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

348 
by (induct n arbitrary: x) (auto simp: funpow_swap1) 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

349 

c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

350 
lemma stake_siterate[simp]: "stake n (siterate f x) = map (\<lambda>n. (f^^n) x) [0 ..< n]" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

351 
by (induct n arbitrary: x) (auto simp del: stake.simps(2) simp: stake_Suc) 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

352 

c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

353 
lemma sset_siterate: "sset (siterate f x) = {(f^^n) x  n. True}" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

354 
by (auto simp: sset_range) 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

355 

c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

356 
lemma smap_siterate: "smap f (siterate f x) = siterate f (f x)" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

357 
by (coinduction arbitrary: x) auto 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

358 

c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

359 

51141  360 
subsection {* stream repeating a single element *} 
361 

54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

362 
abbreviation "sconst \<equiv> siterate id" 
51141  363 

54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

364 
lemma shift_replicate_sconst[simp]: "replicate n x @ sconst x = sconst x" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

365 
by (subst (3) stake_sdrop[symmetric]) (simp add: map_replicate_trivial) 
51141  366 

57175  367 
lemma sset_sconst[simp]: "sset (sconst x) = {x}" 
54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

368 
by (simp add: sset_siterate) 
51141  369 

57175  370 
lemma sconst_alt: "s = sconst x \<longleftrightarrow> sset s = {x}" 
371 
proof 

372 
assume "sset s = {x}" 

373 
then show "s = sconst x" 

374 
proof (coinduction arbitrary: s) 

375 
case Eq_stream 

376 
then have "shd s = x" "sset (stl s) \<subseteq> {x}" by (case_tac [!] s) auto 

377 
then have "sset (stl s) = {x}" by (cases "stl s") auto 

378 
with `shd s = x` show ?case by auto 

379 
qed 

380 
qed simp 

381 

54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

382 
lemma same_cycle: "sconst x = cycle [x]" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

383 
by coinduction auto 
51141  384 

54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

385 
lemma smap_sconst: "smap f (sconst x) = sconst (f x)" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

386 
by coinduction auto 
51141  387 

54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

388 
lemma sconst_streams: "x \<in> A \<Longrightarrow> sconst x \<in> streams A" 
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

389 
by (simp add: streams_iff_sset) 
51141  390 

391 

392 
subsection {* stream of natural numbers *} 

393 

54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

394 
abbreviation "fromN \<equiv> siterate Suc" 
54469  395 

51141  396 
abbreviation "nats \<equiv> fromN 0" 
397 

54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

398 
lemma sset_fromN[simp]: "sset (fromN n) = {n ..}" 
54720
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

399 
by (auto simp add: sset_siterate le_iff_add) 
54497
c76dec4df4d7
BNF/Examples/Stream: rename same to sconst; define same, fromN in terms of siterate
hoelzl
parents:
54469
diff
changeset

400 

57175  401 
lemma stream_smap_fromN: "s = smap (\<lambda>j. let i = j  n in s !! i) (fromN n)" 
402 
by (coinduction arbitrary: s n) 

403 
(force simp: neq_Nil_conv Let_def snth.simps(2)[symmetric] Suc_diff_Suc 

404 
intro: stream.map_cong split: if_splits simp del: snth.simps(2)) 

405 

406 
lemma stream_smap_nats: "s = smap (snth s) nats" 

407 
using stream_smap_fromN[where n = 0] by simp 

408 

51141  409 

51462  410 
subsection {* flatten a stream of lists *} 
411 

54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

412 
primcorec flat where 
51462  413 
"shd (flat ws) = hd (shd ws)" 
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

414 
 "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)" 
51462  415 

416 
lemma flat_Cons[simp, code]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)" 

54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

417 
by (subst flat.ctr) simp 
51462  418 

419 
lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @ flat ws" 

420 
by (induct xs) auto 

421 

422 
lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @ flat (stl ws)" 

423 
by (cases ws) auto 

424 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

425 
lemma flat_snth: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> flat s !! n = (if n < length (shd s) then 
51462  426 
shd s ! n else flat (stl s) !! (n  length (shd s)))" 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

427 
by (metis flat_unfold not_less shd_sset shift_snth_ge shift_snth_less) 
51462  428 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

429 
lemma sset_flat[simp]: "\<forall>xs \<in> sset s. xs \<noteq> [] \<Longrightarrow> 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

430 
sset (flat s) = (\<Union>xs \<in> sset s. set xs)" (is "?P \<Longrightarrow> ?L = ?R") 
51462  431 
proof safe 
432 
fix x assume ?P "x : ?L" 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

433 
then obtain m where "x = flat s !! m" by (metis image_iff sset_range) 
51462  434 
with `?P` obtain n m' where "x = s !! n ! m'" "m' < length (s !! n)" 
435 
proof (atomize_elim, induct m arbitrary: s rule: less_induct) 

436 
case (less y) 

437 
thus ?case 

438 
proof (cases "y < length (shd s)") 

439 
case True thus ?thesis by (metis flat_snth less(2,3) snth.simps(1)) 

440 
next 

441 
case False 

442 
hence "x = flat (stl s) !! (y  length (shd s))" by (metis less(2,3) flat_snth) 

443 
moreover 

53374
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53290
diff
changeset

444 
{ from less(2) have *: "length (shd s) > 0" by (cases s) simp_all 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53290
diff
changeset

445 
with False have "y > 0" by (cases y) simp_all 
a14d2a854c02
tuned proofs  clarified flow of facts wrt. calculation;
wenzelm
parents:
53290
diff
changeset

446 
with * have "y  length (shd s) < y" by simp 
51462  447 
} 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

448 
moreover have "\<forall>xs \<in> sset (stl s). xs \<noteq> []" using less(2) by (cases s) auto 
51462  449 
ultimately have "\<exists>n m'. x = stl s !! n ! m' \<and> m' < length (stl s !! n)" by (intro less(1)) auto 
450 
thus ?thesis by (metis snth.simps(2)) 

451 
qed 

452 
qed 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

453 
thus "x \<in> ?R" by (auto simp: sset_range dest!: nth_mem) 
51462  454 
next 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

455 
fix x xs assume "xs \<in> sset s" ?P "x \<in> set xs" thus "x \<in> ?L" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

456 
by (induct rule: sset_induct1) 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

457 
(metis UnI1 flat_unfold shift.simps(1) sset_shift, 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

458 
metis UnI2 flat_unfold shd_sset stl_sset sset_shift) 
51462  459 
qed 
460 

461 

462 
subsection {* merge a stream of streams *} 

463 

464 
definition smerge :: "'a stream stream \<Rightarrow> 'a stream" where 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

465 
"smerge ss = flat (smap (\<lambda>n. map (\<lambda>s. s !! n) (stake (Suc n) ss) @ stake n (ss !! n)) nats)" 
51462  466 

467 
lemma stake_nth[simp]: "m < n \<Longrightarrow> stake n s ! m = s !! m" 

468 
by (induct n arbitrary: s m) (auto simp: nth_Cons', metis Suc_pred snth.simps(2)) 

469 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

470 
lemma snth_sset_smerge: "ss !! n !! m \<in> sset (smerge ss)" 
51462  471 
proof (cases "n \<le> m") 
472 
case False thus ?thesis unfolding smerge_def 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

473 
by (subst sset_flat) 
53290  474 
(auto simp: stream.set_map in_set_conv_nth simp del: stake.simps 
51462  475 
intro!: exI[of _ n, OF disjI2] exI[of _ m, OF mp]) 
476 
next 

477 
case True thus ?thesis unfolding smerge_def 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

478 
by (subst sset_flat) 
53290  479 
(auto simp: stream.set_map in_set_conv_nth image_iff simp del: stake.simps snth.simps 
51462  480 
intro!: exI[of _ m, OF disjI1] bexI[of _ "ss !! n"] exI[of _ n, OF mp]) 
481 
qed 

482 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

483 
lemma sset_smerge: "sset (smerge ss) = UNION (sset ss) sset" 
51462  484 
proof safe 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

485 
fix x assume "x \<in> sset (smerge ss)" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

486 
thus "x \<in> UNION (sset ss) sset" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

487 
unfolding smerge_def by (subst (asm) sset_flat) 
53290  488 
(auto simp: stream.set_map in_set_conv_nth sset_range simp del: stake.simps, fast+) 
51462  489 
next 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

490 
fix s x assume "s \<in> sset ss" "x \<in> sset s" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

491 
thus "x \<in> sset (smerge ss)" using snth_sset_smerge by (auto simp: sset_range) 
51462  492 
qed 
493 

494 

495 
subsection {* product of two streams *} 

496 

497 
definition sproduct :: "'a stream \<Rightarrow> 'b stream \<Rightarrow> ('a \<times> 'b) stream" where 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

498 
"sproduct s1 s2 = smerge (smap (\<lambda>x. smap (Pair x) s2) s1)" 
51462  499 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

500 
lemma sset_sproduct: "sset (sproduct s1 s2) = sset s1 \<times> sset s2" 
53290  501 
unfolding sproduct_def sset_smerge by (auto simp: stream.set_map) 
51462  502 

503 

504 
subsection {* interleave two streams *} 

505 

54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

506 
primcorec sinterleave where 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

507 
"shd (sinterleave s1 s2) = shd s1" 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

508 
 "stl (sinterleave s1 s2) = sinterleave s2 (stl s1)" 
51462  509 

510 
lemma sinterleave_code[code]: 

511 
"sinterleave (x ## s1) s2 = x ## sinterleave s2 s1" 

54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

512 
by (subst sinterleave.ctr) simp 
51462  513 

514 
lemma sinterleave_snth[simp]: 

515 
"even n \<Longrightarrow> sinterleave s1 s2 !! n = s1 !! (n div 2)" 

516 
"odd n \<Longrightarrow> sinterleave s1 s2 !! n = s2 !! (n div 2)" 

517 
by (induct n arbitrary: s1 s2) 

518 
(auto dest: even_nat_Suc_div_2 odd_nat_plus_one_div_two[folded nat_2]) 

519 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

520 
lemma sset_sinterleave: "sset (sinterleave s1 s2) = sset s1 \<union> sset s2" 
51462  521 
proof (intro equalityI subsetI) 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

522 
fix x assume "x \<in> sset (sinterleave s1 s2)" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

523 
then obtain n where "x = sinterleave s1 s2 !! n" unfolding sset_range by blast 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

524 
thus "x \<in> sset s1 \<union> sset s2" by (cases "even n") auto 
51462  525 
next 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

526 
fix x assume "x \<in> sset s1 \<union> sset s2" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

527 
thus "x \<in> sset (sinterleave s1 s2)" 
51462  528 
proof 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

529 
assume "x \<in> sset s1" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

530 
then obtain n where "x = s1 !! n" unfolding sset_range by blast 
51462  531 
hence "sinterleave s1 s2 !! (2 * n) = x" by simp 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

532 
thus ?thesis unfolding sset_range by blast 
51462  533 
next 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

534 
assume "x \<in> sset s2" 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

535 
then obtain n where "x = s2 !! n" unfolding sset_range by blast 
51462  536 
hence "sinterleave s1 s2 !! (2 * n + 1) = x" by simp 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

537 
thus ?thesis unfolding sset_range by blast 
51462  538 
qed 
539 
qed 

540 

541 

51141  542 
subsection {* zip *} 
543 

54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

544 
primcorec szip where 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

545 
"shd (szip s1 s2) = (shd s1, shd s2)" 
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

546 
 "stl (szip s1 s2) = szip (stl s1) (stl s2)" 
51141  547 

54720
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

548 
lemma szip_unfold[code]: "szip (a ## s1) (b ## s2) = (a, b) ## (szip s1 s2)" 
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

549 
by (subst szip.ctr) simp 
51409  550 

51141  551 
lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)" 
552 
by (induct n arbitrary: s1 s2) auto 

553 

57175  554 
lemma stake_szip[simp]: 
555 
"stake n (szip s1 s2) = zip (stake n s1) (stake n s2)" 

556 
by (induct n arbitrary: s1 s2) auto 

557 

558 
lemma sdrop_szip[simp]: "sdrop n (szip s1 s2) = szip (sdrop n s1) (sdrop n s2)" 

559 
by (induct n arbitrary: s1 s2) auto 

560 

561 
lemma smap_szip_fst: 

562 
"smap (\<lambda>x. f (fst x)) (szip s1 s2) = smap f s1" 

563 
by (coinduction arbitrary: s1 s2) auto 

564 

565 
lemma smap_szip_snd: 

566 
"smap (\<lambda>x. g (snd x)) (szip s1 s2) = smap g s2" 

567 
by (coinduction arbitrary: s1 s2) auto 

568 

51141  569 

570 
subsection {* zip via function *} 

571 

54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

572 
primcorec smap2 where 
51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

573 
"shd (smap2 f s1 s2) = f (shd s1) (shd s2)" 
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

574 
 "stl (smap2 f s1 s2) = smap2 f (stl s1) (stl s2)" 
51141  575 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

576 
lemma smap2_unfold[code]: 
54720
0a9920e46b3a
removed obsolete codegen setup; Stream > SCons; tuned
traytel
parents:
54498
diff
changeset

577 
"smap2 f (a ## s1) (b ## s2) = f a b ## (smap2 f s1 s2)" 
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

578 
by (subst smap2.ctr) simp 
51409  579 

51772
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

580 
lemma smap2_szip: 
d2b265ebc1fa
specify nicer names for map, set and rel in the stream library
traytel
parents:
51766
diff
changeset

581 
"smap2 f s1 s2 = smap (split f) (szip s1 s2)" 
54027
e5853a648b59
use new coinduction method and primcorec in examples
traytel
parents:
53808
diff
changeset

582 
by (coinduction arbitrary: s1 s2) auto 
50518  583 

57175  584 
lemma smap_smap2[simp]: 
585 
"smap f (smap2 g s1 s2) = smap2 (\<lambda>x y. f (g x y)) s1 s2" 

586 
unfolding smap2_szip stream.map_comp o_def split_def .. 

587 

588 
lemma smap2_alt: 

589 
"(smap2 f s1 s2 = s) = (\<forall>n. f (s1 !! n) (s2 !! n) = s !! n)" 

590 
unfolding smap2_szip smap_alt by auto 

591 

592 
lemma snth_smap2[simp]: 

593 
"smap2 f s1 s2 !! n = f (s1 !! n) (s2 !! n)" 

594 
by (induct n arbitrary: s1 s2) auto 

595 

596 
lemma stake_smap2[simp]: 

597 
"stake n (smap2 f s1 s2) = map (split f) (zip (stake n s1) (stake n s2))" 

598 
by (induct n arbitrary: s1 s2) auto 

599 

600 
lemma sdrop_smap2[simp]: 

601 
"sdrop n (smap2 f s1 s2) = smap2 f (sdrop n s1) (sdrop n s2)" 

602 
by (induct n arbitrary: s1 s2) auto 

603 

50518  604 
end 