14 |
14 |
15 codata 'a stream = Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65) |
15 codata 'a stream = Stream (shd: 'a) (stl: "'a stream") (infixr "##" 65) |
16 |
16 |
17 (* TODO: Provide by the package*) |
17 (* TODO: Provide by the package*) |
18 theorem stream_set_induct: |
18 theorem stream_set_induct: |
19 "\<lbrakk>\<And>s. P (shd s) s; \<And>s y. \<lbrakk>y \<in> stream_set (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s\<rbrakk> \<Longrightarrow> |
19 "\<lbrakk>\<And>s. P (shd s) s; \<And>s y. \<lbrakk>y \<in> stream_set (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s\<rbrakk> \<Longrightarrow> |
20 \<forall>y \<in> stream_set s. P y s" |
20 \<forall>y \<in> stream_set s. P y s" |
21 by (rule stream.dtor_set_induct) |
21 by (rule stream.dtor_set_induct) |
22 (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
22 (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
|
23 |
|
24 lemma stream_map_simps[simp]: |
|
25 "shd (stream_map f s) = f (shd s)" "stl (stream_map f s) = stream_map f (stl s)" |
|
26 unfolding shd_def stl_def stream_case_def stream_map_def stream.dtor_unfold |
|
27 by (case_tac [!] s) (auto simp: Stream_def stream.dtor_ctor) |
|
28 |
|
29 lemma stream_map_Stream[simp]: "stream_map f (x ## s) = f x ## stream_map f s" |
|
30 by (metis stream.exhaust stream.sels stream_map_simps) |
23 |
31 |
24 theorem shd_stream_set: "shd s \<in> stream_set s" |
32 theorem shd_stream_set: "shd s \<in> stream_set s" |
25 by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
33 by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
26 (metis UnCI fsts_def insertI1 stream.dtor_set) |
34 (metis UnCI fsts_def insertI1 stream.dtor_set) |
27 |
35 |
28 theorem stl_stream_set: "y \<in> stream_set (stl s) \<Longrightarrow> y \<in> stream_set s" |
36 theorem stl_stream_set: "y \<in> stream_set (stl s) \<Longrightarrow> y \<in> stream_set s" |
29 by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
37 by (auto simp add: shd_def stl_def stream_case_def fsts_def snds_def split_beta) |
30 (metis insertI1 set_mp snds_def stream.dtor_set_set_incl) |
38 (metis insertI1 set_mp snds_def stream.dtor_set_set_incl) |
31 |
39 |
32 (* only for the non-mutual case: *) |
40 (* only for the non-mutual case: *) |
33 theorem stream_set_induct1[consumes 1, case_names shd stl, induct set: "stream_set"]: |
41 theorem stream_set_induct1[consumes 1, case_names shd stl, induct set: "stream_set"]: |
34 assumes "y \<in> stream_set s" and "\<And>s. P (shd s) s" |
42 assumes "y \<in> stream_set s" and "\<And>s. P (shd s) s" |
35 and "\<And>s y. \<lbrakk>y \<in> stream_set (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s" |
43 and "\<And>s y. \<lbrakk>y \<in> stream_set (stl s); P y (stl s)\<rbrakk> \<Longrightarrow> P y s" |
36 shows "P y s" |
44 shows "P y s" |
37 using assms stream_set_induct by blast |
45 using assms stream_set_induct by blast |
38 (* end TODO *) |
46 (* end TODO *) |
39 |
47 |
40 |
48 |
41 subsection {* prepend list to stream *} |
49 subsection {* prepend list to stream *} |
42 |
50 |
43 primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where |
51 primrec shift :: "'a list \<Rightarrow> 'a stream \<Rightarrow> 'a stream" (infixr "@-" 65) where |
44 "shift [] s = s" |
52 "shift [] s = s" |
45 | "shift (x # xs) s = x ## shift xs s" |
53 | "shift (x # xs) s = x ## shift xs s" |
46 |
54 |
47 lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s" |
55 lemma shift_append[simp]: "(xs @ ys) @- s = xs @- ys @- s" |
48 by (induct xs) auto |
56 by (induct xs) auto |
49 |
57 |
50 lemma shift_simps[simp]: |
58 lemma shift_simps[simp]: |
51 "shd (xs @- s) = (if xs = [] then shd s else hd xs)" |
59 "shd (xs @- s) = (if xs = [] then shd s else hd xs)" |
52 "stl (xs @- s) = (if xs = [] then stl s else tl xs @- s)" |
60 "stl (xs @- s) = (if xs = [] then stl s else tl xs @- s)" |
53 by (induct xs) auto |
61 by (induct xs) auto |
54 |
62 |
55 |
63 lemma stream_set_shift[simp]: "stream_set (xs @- s) = set xs \<union> stream_set s" |
56 subsection {* recurring stream out of a list *} |
64 by (induct xs) auto |
57 |
65 |
58 definition cycle :: "'a list \<Rightarrow> 'a stream" where |
66 |
59 "cycle = stream_unfold hd (\<lambda>xs. tl xs @ [hd xs])" |
67 subsection {* set of streams with elements in some fixes set *} |
60 |
|
61 lemma cycle_simps[simp]: |
|
62 "shd (cycle u) = hd u" |
|
63 "stl (cycle u) = cycle (tl u @ [hd u])" |
|
64 by (auto simp: cycle_def) |
|
65 |
|
66 |
|
67 lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u" |
|
68 proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>u. s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []"]) |
|
69 case (2 s1 s2) |
|
70 then obtain u where "s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []" by blast |
|
71 thus ?case using stream.unfold[of hd "\<lambda>xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def) |
|
72 qed auto |
|
73 |
|
74 lemma cycle_Cons: "cycle (x # xs) = x ## cycle (xs @ [x])" |
|
75 proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])"]) |
|
76 case (2 s1 s2) |
|
77 then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])" by blast |
|
78 thus ?case |
|
79 by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold) |
|
80 qed auto |
|
81 |
68 |
82 coinductive_set |
69 coinductive_set |
83 streams :: "'a set => 'a stream set" |
70 streams :: "'a set => 'a stream set" |
84 for A :: "'a set" |
71 for A :: "'a set" |
85 where |
72 where |
86 Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A" |
73 Stream[intro!, simp, no_atp]: "\<lbrakk>a \<in> A; s \<in> streams A\<rbrakk> \<Longrightarrow> a ## s \<in> streams A" |
87 |
74 |
88 lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A" |
75 lemma shift_streams: "\<lbrakk>w \<in> lists A; s \<in> streams A\<rbrakk> \<Longrightarrow> w @- s \<in> streams A" |
89 by (induct w) auto |
76 by (induct w) auto |
90 |
77 |
91 lemma stream_set_streams: |
78 lemma stream_set_streams: |
92 assumes "stream_set s \<subseteq> A" |
79 assumes "stream_set s \<subseteq> A" |
93 shows "s \<in> streams A" |
80 shows "s \<in> streams A" |
94 proof (coinduct rule: streams.coinduct[of "\<lambda>s'. \<exists>a s. s' = a ## s \<and> a \<in> A \<and> stream_set s \<subseteq> A"]) |
81 proof (coinduct rule: streams.coinduct[of "\<lambda>s'. \<exists>a s. s' = a ## s \<and> a \<in> A \<and> stream_set s \<subseteq> A"]) |
108 "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else tl (shd s) ## stl s)" |
95 "flat \<equiv> stream_unfold (hd o shd) (\<lambda>s. if tl (shd s) = [] then stl s else tl (shd s) ## stl s)" |
109 |
96 |
110 lemma flat_simps[simp]: |
97 lemma flat_simps[simp]: |
111 "shd (flat ws) = hd (shd ws)" |
98 "shd (flat ws) = hd (shd ws)" |
112 "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)" |
99 "stl (flat ws) = flat (if tl (shd ws) = [] then stl ws else tl (shd ws) ## stl ws)" |
113 unfolding flat_def by auto |
100 unfolding flat_def by auto |
114 |
101 |
115 lemma flat_Cons[simp]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)" |
102 lemma flat_Cons[simp]: "flat ((x # xs) ## ws) = x ## flat (if xs = [] then ws else xs ## ws)" |
116 unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto |
103 unfolding flat_def using stream.unfold[of "hd o shd" _ "(x # xs) ## ws"] by auto |
117 |
104 |
118 lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws" |
105 lemma flat_Stream[simp]: "xs \<noteq> [] \<Longrightarrow> flat (xs ## ws) = xs @- flat ws" |
119 by (induct xs) auto |
106 by (induct xs) auto |
120 |
107 |
121 lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)" |
108 lemma flat_unfold: "shd ws \<noteq> [] \<Longrightarrow> flat ws = shd ws @- flat (stl ws)" |
122 by (cases ws) auto |
109 by (cases ws) auto |
123 |
110 |
124 |
111 |
125 subsection {* take, drop, nth for streams *} |
112 subsection {* nth, take, drop for streams *} |
|
113 |
|
114 primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where |
|
115 "s !! 0 = shd s" |
|
116 | "s !! Suc n = stl s !! n" |
|
117 |
|
118 lemma snth_stream_map[simp]: "stream_map f s !! n = f (s !! n)" |
|
119 by (induct n arbitrary: s) auto |
|
120 |
|
121 lemma shift_snth_less[simp]: "p < length xs \<Longrightarrow> (xs @- s) !! p = xs ! p" |
|
122 by (induct p arbitrary: xs) (auto simp: hd_conv_nth nth_tl) |
|
123 |
|
124 lemma shift_snth_ge[simp]: "p \<ge> length xs \<Longrightarrow> (xs @- s) !! p = s !! (p - length xs)" |
|
125 by (induct p arbitrary: xs) (auto simp: Suc_diff_eq_diff_pred) |
|
126 |
|
127 lemma snth_stream_set[simp]: "s !! n \<in> stream_set s" |
|
128 by (induct n arbitrary: s) (auto intro: shd_stream_set stl_stream_set) |
|
129 |
|
130 lemma stream_set_range: "stream_set s = range (snth s)" |
|
131 proof (intro equalityI subsetI) |
|
132 fix x assume "x \<in> stream_set s" |
|
133 thus "x \<in> range (snth s)" |
|
134 proof (induct s) |
|
135 case (stl s x) |
|
136 then obtain n where "x = stl s !! n" by auto |
|
137 thus ?case by (auto intro: range_eqI[of _ _ "Suc n"]) |
|
138 qed (auto intro: range_eqI[of _ _ 0]) |
|
139 qed auto |
126 |
140 |
127 primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where |
141 primrec stake :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a list" where |
128 "stake 0 s = []" |
142 "stake 0 s = []" |
129 | "stake (Suc n) s = shd s # stake n (stl s)" |
143 | "stake (Suc n) s = shd s # stake n (stl s)" |
130 |
144 |
|
145 lemma length_stake[simp]: "length (stake n s) = n" |
|
146 by (induct n arbitrary: s) auto |
|
147 |
|
148 lemma stake_stream_map[simp]: "stake n (stream_map f s) = map f (stake n s)" |
|
149 by (induct n arbitrary: s) auto |
|
150 |
131 primrec sdrop :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where |
151 primrec sdrop :: "nat \<Rightarrow> 'a stream \<Rightarrow> 'a stream" where |
132 "sdrop 0 s = s" |
152 "sdrop 0 s = s" |
133 | "sdrop (Suc n) s = sdrop n (stl s)" |
153 | "sdrop (Suc n) s = sdrop n (stl s)" |
134 |
154 |
135 primrec snth :: "'a stream \<Rightarrow> nat \<Rightarrow> 'a" (infixl "!!" 100) where |
155 lemma sdrop_simps[simp]: |
136 "s !! 0 = shd s" |
156 "shd (sdrop n s) = s !! n" "stl (sdrop n s) = sdrop (Suc n) s" |
137 | "s !! Suc n = stl s !! n" |
157 by (induct n arbitrary: s) auto |
|
158 |
|
159 lemma sdrop_stream_map[simp]: "sdrop n (stream_map f s) = stream_map f (sdrop n s)" |
|
160 by (induct n arbitrary: s) auto |
138 |
161 |
139 lemma stake_sdrop: "stake n s @- sdrop n s = s" |
162 lemma stake_sdrop: "stake n s @- sdrop n s = s" |
140 by (induct n arbitrary: s) auto |
163 by (induct n arbitrary: s) auto |
141 |
164 |
142 lemma stake_empty: "stake n s = [] \<longleftrightarrow> n = 0" |
165 lemma id_stake_snth_sdrop: |
143 by (cases n) auto |
166 "s = stake i s @- s !! i ## sdrop (Suc i) s" |
|
167 by (subst stake_sdrop[symmetric, of _ i]) (metis sdrop_simps stream.collapse) |
|
168 |
|
169 lemma stream_map_alt: "stream_map f s = s' \<longleftrightarrow> (\<forall>n. f (s !! n) = s' !! n)" (is "?L = ?R") |
|
170 proof |
|
171 assume ?R |
|
172 thus ?L |
|
173 by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>n. s1 = stream_map f (sdrop n s) \<and> s2 = sdrop n s'"]) |
|
174 (auto intro: exI[of _ 0] simp del: sdrop.simps(2)) |
|
175 qed auto |
|
176 |
|
177 lemma stake_invert_Nil[iff]: "stake n s = [] \<longleftrightarrow> n = 0" |
|
178 by (induct n) auto |
144 |
179 |
145 lemma sdrop_shift: "\<lbrakk>s = w @- s'; length w = n\<rbrakk> \<Longrightarrow> sdrop n s = s'" |
180 lemma sdrop_shift: "\<lbrakk>s = w @- s'; length w = n\<rbrakk> \<Longrightarrow> sdrop n s = s'" |
146 by (induct n arbitrary: w s) auto |
181 by (induct n arbitrary: w s) auto |
147 |
182 |
148 lemma stake_shift: "\<lbrakk>s = w @- s'; length w = n\<rbrakk> \<Longrightarrow> stake n s = w" |
183 lemma stake_shift: "\<lbrakk>s = w @- s'; length w = n\<rbrakk> \<Longrightarrow> stake n s = w" |
149 by (induct n arbitrary: w s) auto |
184 by (induct n arbitrary: w s) auto |
150 |
185 |
151 lemma stake_add[simp]: "stake m s @ stake n (sdrop m s) = stake (m + n) s" |
186 lemma stake_add[simp]: "stake m s @ stake n (sdrop m s) = stake (m + n) s" |
152 by (induct m arbitrary: s) auto |
187 by (induct m arbitrary: s) auto |
153 |
188 |
154 lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s" |
189 lemma sdrop_add[simp]: "sdrop n (sdrop m s) = sdrop (m + n) s" |
155 by (induct m arbitrary: s) auto |
190 by (induct m arbitrary: s) auto |
|
191 |
|
192 |
|
193 subsection {* unary predicates lifted to streams *} |
|
194 |
|
195 definition "stream_all P s = (\<forall>p. P (s !! p))" |
|
196 |
|
197 lemma stream_all_iff[iff]: "stream_all P s \<longleftrightarrow> Ball (stream_set s) P" |
|
198 unfolding stream_all_def stream_set_range by auto |
|
199 |
|
200 lemma stream_all_shift[simp]: "stream_all P (xs @- s) = (list_all P xs \<and> stream_all P s)" |
|
201 unfolding stream_all_iff list_all_iff by auto |
|
202 |
|
203 |
|
204 subsection {* recurring stream out of a list *} |
|
205 |
|
206 definition cycle :: "'a list \<Rightarrow> 'a stream" where |
|
207 "cycle = stream_unfold hd (\<lambda>xs. tl xs @ [hd xs])" |
|
208 |
|
209 lemma cycle_simps[simp]: |
|
210 "shd (cycle u) = hd u" |
|
211 "stl (cycle u) = cycle (tl u @ [hd u])" |
|
212 by (auto simp: cycle_def) |
|
213 |
|
214 lemma cycle_decomp: "u \<noteq> [] \<Longrightarrow> cycle u = u @- cycle u" |
|
215 proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>u. s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []"]) |
|
216 case (2 s1 s2) |
|
217 then obtain u where "s1 = cycle u \<and> s2 = u @- cycle u \<and> u \<noteq> []" by blast |
|
218 thus ?case using stream.unfold[of hd "\<lambda>xs. tl xs @ [hd xs]" u] by (auto simp: cycle_def) |
|
219 qed auto |
|
220 |
|
221 lemma cycle_Cons: "cycle (x # xs) = x ## cycle (xs @ [x])" |
|
222 proof (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. \<exists>x xs. s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])"]) |
|
223 case (2 s1 s2) |
|
224 then obtain x xs where "s1 = cycle (x # xs) \<and> s2 = x ## cycle (xs @ [x])" by blast |
|
225 thus ?case |
|
226 by (auto simp: cycle_def intro!: exI[of _ "hd (xs @ [x])"] exI[of _ "tl (xs @ [x])"] stream.unfold) |
|
227 qed auto |
156 |
228 |
157 lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @- s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @- s" |
229 lemma cycle_rotated: "\<lbrakk>v \<noteq> []; cycle u = v @- s\<rbrakk> \<Longrightarrow> cycle (tl u @ [hd u]) = tl v @- s" |
158 by (auto dest: arg_cong[of _ _ stl]) |
230 by (auto dest: arg_cong[of _ _ stl]) |
159 |
231 |
160 lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s" |
232 lemma stake_append: "stake n (u @- s) = take (min (length u) n) u @ stake (n - length u) s" |
161 proof (induct n arbitrary: u) |
233 proof (induct n arbitrary: u) |
162 case (Suc n) thus ?case by (cases u) auto |
234 case (Suc n) thus ?case by (cases u) auto |
163 qed auto |
235 qed auto |
164 |
236 |
165 lemma stake_cycle_le[simp]: |
237 lemma stake_cycle_le[simp]: |
166 assumes "u \<noteq> []" "n < length u" |
238 assumes "u \<noteq> []" "n < length u" |
167 shows "stake n (cycle u) = take n u" |
239 shows "stake n (cycle u) = take n u" |
168 using min_absorb2[OF less_imp_le_nat[OF assms(2)]] |
240 using min_absorb2[OF less_imp_le_nat[OF assms(2)]] |
169 by (subst cycle_decomp[OF assms(1)], subst stake_append) auto |
241 by (subst cycle_decomp[OF assms(1)], subst stake_append) auto |
170 |
242 |
171 lemma stake_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> stake (length u) (cycle u) = u" |
243 lemma stake_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> stake (length u) (cycle u) = u" |
172 by (metis cycle_decomp stake_shift) |
244 by (metis cycle_decomp stake_shift) |
173 |
245 |
174 lemma sdrop_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> sdrop (length u) (cycle u) = cycle u" |
246 lemma sdrop_cycle_eq[simp]: "u \<noteq> [] \<Longrightarrow> sdrop (length u) (cycle u) = cycle u" |
175 by (metis cycle_decomp sdrop_shift) |
247 by (metis cycle_decomp sdrop_shift) |
176 |
248 |
177 lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow> |
249 lemma stake_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow> |
178 stake n (cycle u) = concat (replicate (n div length u) u)" |
250 stake n (cycle u) = concat (replicate (n div length u) u)" |
179 by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric]) |
251 by (induct "n div length u" arbitrary: n u) (auto simp: stake_add[symmetric]) |
180 |
252 |
181 lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow> |
253 lemma sdrop_cycle_eq_mod_0[simp]: "\<lbrakk>u \<noteq> []; n mod length u = 0\<rbrakk> \<Longrightarrow> |
182 sdrop n (cycle u) = cycle u" |
254 sdrop n (cycle u) = cycle u" |
183 by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric]) |
255 by (induct "n div length u" arbitrary: n u) (auto simp: sdrop_add[symmetric]) |
184 |
256 |
185 lemma stake_cycle: "u \<noteq> [] \<Longrightarrow> |
257 lemma stake_cycle: "u \<noteq> [] \<Longrightarrow> |
186 stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u" |
258 stake n (cycle u) = concat (replicate (n div length u) u) @ take (n mod length u) u" |
187 by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto |
259 by (subst mod_div_equality[of n "length u", symmetric], unfold stake_add[symmetric]) auto |
188 |
260 |
189 lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)" |
261 lemma sdrop_cycle: "u \<noteq> [] \<Longrightarrow> sdrop n (cycle u) = cycle (rotate (n mod length u) u)" |
190 by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric]) |
262 by (induct n arbitrary: u) (auto simp: rotate1_rotate_swap rotate1_hd_tl rotate_conv_mod[symmetric]) |
|
263 |
|
264 |
|
265 subsection {* stream repeating a single element *} |
|
266 |
|
267 definition "same x = stream_unfold (\<lambda>_. x) id ()" |
|
268 |
|
269 lemma same_simps[simp]: "shd (same x) = x" "stl (same x) = same x" |
|
270 unfolding same_def by auto |
|
271 |
|
272 lemma same_unfold: "same x = Stream x (same x)" |
|
273 by (metis same_simps stream.collapse) |
|
274 |
|
275 lemma snth_same[simp]: "same x !! n = x" |
|
276 unfolding same_def by (induct n) auto |
|
277 |
|
278 lemma stake_same[simp]: "stake n (same x) = replicate n x" |
|
279 unfolding same_def by (induct n) (auto simp: upt_rec) |
|
280 |
|
281 lemma sdrop_same[simp]: "sdrop n (same x) = same x" |
|
282 unfolding same_def by (induct n) auto |
|
283 |
|
284 lemma shift_replicate_same[simp]: "replicate n x @- same x = same x" |
|
285 by (metis sdrop_same stake_same stake_sdrop) |
|
286 |
|
287 lemma stream_all_same[simp]: "stream_all P (same x) \<longleftrightarrow> P x" |
|
288 unfolding stream_all_def by auto |
|
289 |
|
290 lemma same_cycle: "same x = cycle [x]" |
|
291 by (coinduct rule: stream.coinduct[of "\<lambda>s1 s2. s1 = same x \<and> s2 = cycle [x]"]) auto |
|
292 |
|
293 |
|
294 subsection {* stream of natural numbers *} |
|
295 |
|
296 definition "fromN n = stream_unfold id Suc n" |
|
297 |
|
298 lemma fromN_simps[simp]: "shd (fromN n) = n" "stl (fromN n) = fromN (Suc n)" |
|
299 unfolding fromN_def by auto |
|
300 |
|
301 lemma snth_fromN[simp]: "fromN n !! m = n + m" |
|
302 unfolding fromN_def by (induct m arbitrary: n) auto |
|
303 |
|
304 lemma stake_fromN[simp]: "stake m (fromN n) = [n ..< m + n]" |
|
305 unfolding fromN_def by (induct m arbitrary: n) (auto simp: upt_rec) |
|
306 |
|
307 lemma sdrop_fromN[simp]: "sdrop m (fromN n) = fromN (n + m)" |
|
308 unfolding fromN_def by (induct m arbitrary: n) auto |
|
309 |
|
310 abbreviation "nats \<equiv> fromN 0" |
|
311 |
|
312 |
|
313 subsection {* zip *} |
|
314 |
|
315 definition "szip s1 s2 = |
|
316 stream_unfold (map_pair shd shd) (map_pair stl stl) (s1, s2)" |
|
317 |
|
318 lemma szip_simps[simp]: |
|
319 "shd (szip s1 s2) = (shd s1, shd s2)" "stl (szip s1 s2) = szip (stl s1) (stl s2)" |
|
320 unfolding szip_def by auto |
|
321 |
|
322 lemma snth_szip[simp]: "szip s1 s2 !! n = (s1 !! n, s2 !! n)" |
|
323 by (induct n arbitrary: s1 s2) auto |
|
324 |
|
325 |
|
326 subsection {* zip via function *} |
|
327 |
|
328 definition "stream_map2 f s1 s2 = |
|
329 stream_unfold (\<lambda>(s1,s2). f (shd s1) (shd s2)) (map_pair stl stl) (s1, s2)" |
|
330 |
|
331 lemma stream_map2_simps[simp]: |
|
332 "shd (stream_map2 f s1 s2) = f (shd s1) (shd s2)" |
|
333 "stl (stream_map2 f s1 s2) = stream_map2 f (stl s1) (stl s2)" |
|
334 unfolding stream_map2_def by auto |
|
335 |
|
336 lemma stream_map2_szip: |
|
337 "stream_map2 f s1 s2 = stream_map (split f) (szip s1 s2)" |
|
338 by (coinduct rule: stream.coinduct[of |
|
339 "\<lambda>s1 s2. \<exists>s1' s2'. s1 = stream_map2 f s1' s2' \<and> s2 = stream_map (split f) (szip s1' s2')"]) |
|
340 fastforce+ |
191 |
341 |
192 end |
342 end |