1 theory Moment |
1 theory Moment |
2 imports Main |
2 imports Main |
3 begin |
3 begin |
4 |
4 |
5 fun firstn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
6 where |
|
7 "firstn 0 s = []" | |
|
8 "firstn (Suc n) [] = []" | |
|
9 "firstn (Suc n) (e#s) = e#(firstn n s)" |
|
10 |
|
11 lemma upto_map_plus: "map (op + k) [i..j] = [i+k..j+k]" |
|
12 proof(induct "[i..j]" arbitrary:i j rule:length_induct) |
|
13 case (1 i j) |
|
14 thus ?case |
|
15 proof(cases "i \<le> j") |
|
16 case True |
|
17 hence le_k: "i + k \<le> j + k" by simp |
|
18 show ?thesis (is "?L = ?R") |
|
19 proof - |
|
20 have "?L = (k + i) # map (op + k) [i + 1..j]" |
|
21 by (simp add: upto_rec1[OF True]) |
|
22 moreover have "?R = (i + k) # [i + k + 1..j + k]" |
|
23 by (simp add: upto_rec1[OF le_k]) |
|
24 moreover have "map (op + k) [i + 1..j] = [i + k + 1..j + k]" |
|
25 proof - |
|
26 have h: "i + k + 1 = (i + 1) + k" by simp |
|
27 show ?thesis |
|
28 proof(unfold h, rule 1[rule_format]) |
|
29 show "length [i + 1..j] < length [i..j]" |
|
30 using upto_rec1[OF True] by simp |
|
31 qed simp |
|
32 qed |
|
33 ultimately show ?thesis by simp |
|
34 qed |
|
35 qed auto |
|
36 qed |
|
37 |
|
38 lemma firstn_alt_def: |
|
39 "firstn n s = map (\<lambda> i. s!(nat i)) [0..(int (min (length s) n)) - 1]" |
|
40 proof(induct n arbitrary:s) |
|
41 case (0 s) |
|
42 thus ?case by auto |
|
43 next |
|
44 case (Suc n s) |
|
45 thus ?case (is "?L = ?R") |
|
46 proof(cases s) |
|
47 case Nil |
|
48 thus ?thesis by simp |
|
49 next |
|
50 case (Cons e es) |
|
51 with Suc |
|
52 have "?L = e # map (\<lambda>i. es ! nat i) [0..int (min (length es) n) - 1]" |
|
53 by simp |
|
54 also have "... = map (\<lambda>i. (e # es) ! nat i) [0..int (min (length es) n)]" |
|
55 (is "?L1 = ?R1") |
|
56 proof - |
|
57 have "?R1 = e # map (\<lambda>i. (e # es) ! nat i) |
|
58 [1..int (min (length es) n)]" |
|
59 proof - |
|
60 have "[0..int (min (length es) n)] = 0#[1..int (min (length es) n)]" |
|
61 by (simp add: upto.simps) |
|
62 thus ?thesis by simp |
|
63 qed |
|
64 also have "... = ?L1" (is "_#?L2 = _#?R2") |
|
65 proof - |
|
66 have "?L2 = ?R2" |
|
67 proof - |
|
68 have "map (\<lambda>i. (e # es) ! nat i) [1..int (min (length es) n)] = |
|
69 map ((\<lambda>i. (e # es) ! nat i) \<circ> op + 1) [0..int (min (length es) n) - 1]" |
|
70 proof - |
|
71 have "[1..int (min (length es) n)] = |
|
72 map (op + 1) [0..int (min (length es) n) - 1]" |
|
73 by (unfold upto_map_plus, simp) |
|
74 thus ?thesis by simp |
|
75 qed |
|
76 also have "... = map (\<lambda>i. es ! nat i) [0..int (min (length es) n) - 1]" |
|
77 proof(rule map_cong) |
|
78 fix x |
|
79 assume "x \<in> set [0..int (min (length es) n) - 1]" |
|
80 thus "((\<lambda>i. (e # es) ! nat i) \<circ> op + 1) x = es ! nat x" |
|
81 by (metis atLeastLessThan_iff atLeastLessThan_upto |
|
82 comp_apply local.Cons nat_0_le nat_int nth_Cons_Suc of_nat_Suc) |
|
83 qed auto |
|
84 finally show ?thesis . |
|
85 qed |
|
86 thus ?thesis by simp |
|
87 qed |
|
88 finally show ?thesis by simp |
|
89 qed |
|
90 also have "... = ?R" |
|
91 by (unfold Cons, simp) |
|
92 finally show ?thesis . |
|
93 qed |
|
94 qed |
|
95 |
|
96 fun restn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
97 where "restn n s = rev (firstn (length s - n) (rev s))" |
|
98 |
|
99 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
5 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
100 where "moment n s = rev (firstn n (rev s))" |
6 where "moment n s = rev (take n (rev s))" |
|
7 |
|
8 value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
101 |
9 |
102 definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
10 definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
103 where "restm n s = rev (restn n (rev s))" |
11 where "restm n s = rev (drop n (rev s))" |
|
12 |
|
13 value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
104 |
14 |
105 definition from_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
15 definition from_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
106 where "from_to i j s = firstn (j - i) (restn i s)" |
16 where "from_to i j s = take (j - i) (drop i s)" |
107 |
17 |
108 definition down_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
18 definition down_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
109 where "down_to j i s = rev (from_to i j (rev s))" |
19 where "down_to j i s = rev (from_to i j (rev s))" |
110 |
20 |
111 value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]" |
21 value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]" |
112 value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]" |
22 value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]" |
113 |
23 |
114 lemma length_eq_elim_l: "\<lbrakk>length xs = length ys; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs" |
|
115 by auto |
|
116 |
|
117 lemma length_eq_elim_r: "\<lbrakk>length us = length vs; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs" |
|
118 by simp |
|
119 |
|
120 lemma firstn_nil [simp]: "firstn n [] = []" |
|
121 by (cases n, simp+) |
|
122 |
|
123 |
|
124 value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ |
24 value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ |
125 from_to 2 5 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]" |
25 from_to 2 5 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9]" |
126 |
26 |
127 lemma firstn_le: "\<And> n s'. n \<le> length s \<Longrightarrow> firstn n (s@s') = firstn n s" |
27 |
128 proof (induct s, simp) |
28 lemma moment_restm_s: "(restm n s) @ (moment n s) = s" |
129 fix a s n s' |
29 unfolding restm_def moment_def |
130 assume ih: "\<And>n s'. n \<le> length s \<Longrightarrow> firstn n (s @ s') = firstn n s" |
30 by (metis append_take_drop_id rev_append rev_rev_ident) |
131 and le_n: " n \<le> length (a # s)" |
31 |
132 show "firstn n ((a # s) @ s') = firstn n (a # s)" |
32 declare drop.simps [simp del] |
133 proof(cases n, simp) |
33 |
134 fix k |
34 lemma length_take_le: |
135 assume eq_n: "n = Suc k" |
35 "n \<le> length s \<Longrightarrow> length (take n s) = n" |
136 with le_n have "k \<le> length s" by auto |
36 by (metis length_take min.absorb2) |
137 from ih [OF this] and eq_n |
|
138 show "firstn n ((a # s) @ s') = firstn n (a # s)" by auto |
|
139 qed |
|
140 qed |
|
141 |
|
142 lemma firstn_ge [simp]: "\<And>n. length s \<le> n \<Longrightarrow> firstn n s = s" |
|
143 proof(induct s, simp) |
|
144 fix a s n |
|
145 assume ih: "\<And>n. length s \<le> n \<Longrightarrow> firstn n s = s" |
|
146 and le: "length (a # s) \<le> n" |
|
147 show "firstn n (a # s) = a # s" |
|
148 proof(cases n) |
|
149 assume eq_n: "n = 0" with le show ?thesis by simp |
|
150 next |
|
151 fix k |
|
152 assume eq_n: "n = Suc k" |
|
153 with le have le_k: "length s \<le> k" by simp |
|
154 from ih [OF this] have "firstn k s = s" . |
|
155 from eq_n and this |
|
156 show ?thesis by simp |
|
157 qed |
|
158 qed |
|
159 |
|
160 lemma firstn_eq [simp]: "firstn (length s) s = s" |
|
161 by simp |
|
162 |
|
163 lemma firstn_restn_s: "(firstn n (s::'a list)) @ (restn n s) = s" |
|
164 proof(induct n arbitrary:s, simp) |
|
165 fix n s |
|
166 assume ih: "\<And>t. firstn n (t::'a list) @ restn n t = t" |
|
167 show "firstn (Suc n) (s::'a list) @ restn (Suc n) s = s" |
|
168 proof(cases s, simp) |
|
169 fix x xs |
|
170 assume eq_s: "s = x#xs" |
|
171 show "firstn (Suc n) s @ restn (Suc n) s = s" |
|
172 proof - |
|
173 have "firstn (Suc n) s @ restn (Suc n) s = x # (firstn n xs @ restn n xs)" |
|
174 proof - |
|
175 from eq_s have "firstn (Suc n) s = x # firstn n xs" by simp |
|
176 moreover have "restn (Suc n) s = restn n xs" |
|
177 proof - |
|
178 from eq_s have "restn (Suc n) s = rev (firstn (length xs - n) (rev xs @ [x]))" by simp |
|
179 also have "\<dots> = restn n xs" |
|
180 proof - |
|
181 have "(firstn (length xs - n) (rev xs @ [x])) = (firstn (length xs - n) (rev xs))" |
|
182 by(rule firstn_le, simp) |
|
183 hence "rev (firstn (length xs - n) (rev xs @ [x])) = |
|
184 rev (firstn (length xs - n) (rev xs))" by simp |
|
185 also have "\<dots> = rev (firstn (length (rev xs) - n) (rev xs))" by simp |
|
186 finally show ?thesis by simp |
|
187 qed |
|
188 finally show ?thesis by simp |
|
189 qed |
|
190 ultimately show ?thesis by simp |
|
191 qed with ih eq_s show ?thesis by simp |
|
192 qed |
|
193 qed |
|
194 qed |
|
195 |
|
196 lemma moment_restm_s: "(restm n s)@(moment n s) = s" |
|
197 proof - |
|
198 have " rev ((firstn n (rev s)) @ (restn n (rev s))) = s" (is "rev ?x = s") |
|
199 proof - |
|
200 have "?x = rev s" by (simp only:firstn_restn_s) |
|
201 thus ?thesis by auto |
|
202 qed |
|
203 thus ?thesis |
|
204 by (auto simp:restm_def moment_def) |
|
205 qed |
|
206 |
|
207 declare restn.simps [simp del] firstn.simps[simp del] |
|
208 |
|
209 lemma length_firstn_ge: "length s \<le> n \<Longrightarrow> length (firstn n s) = length s" |
|
210 proof(induct n arbitrary:s, simp add:firstn.simps) |
|
211 case (Suc k) |
|
212 assume ih: "\<And> s. length (s::'a list) \<le> k \<Longrightarrow> length (firstn k s) = length s" |
|
213 and le: "length s \<le> Suc k" |
|
214 show ?case |
|
215 proof(cases s) |
|
216 case Nil |
|
217 from Nil show ?thesis by simp |
|
218 next |
|
219 case (Cons x xs) |
|
220 from le and Cons have "length xs \<le> k" by simp |
|
221 from ih [OF this] have "length (firstn k xs) = length xs" . |
|
222 moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))" |
|
223 by (simp add:firstn.simps) |
|
224 moreover note Cons |
|
225 ultimately show ?thesis by simp |
|
226 qed |
|
227 qed |
|
228 |
|
229 lemma length_firstn_le: "n \<le> length s \<Longrightarrow> length (firstn n s) = n" |
|
230 proof(induct n arbitrary:s, simp add:firstn.simps) |
|
231 case (Suc k) |
|
232 assume ih: "\<And>s. k \<le> length (s::'a list) \<Longrightarrow> length (firstn k s) = k" |
|
233 and le: "Suc k \<le> length s" |
|
234 show ?case |
|
235 proof(cases s) |
|
236 case Nil |
|
237 from Nil and le show ?thesis by auto |
|
238 next |
|
239 case (Cons x xs) |
|
240 from le and Cons have "k \<le> length xs" by simp |
|
241 from ih [OF this] have "length (firstn k xs) = k" . |
|
242 moreover from Cons have "length (firstn (Suc k) s) = Suc (length (firstn k xs))" |
|
243 by (simp add:firstn.simps) |
|
244 ultimately show ?thesis by simp |
|
245 qed |
|
246 qed |
|
247 |
|
248 lemma app_firstn_restn: |
|
249 fixes s1 s2 |
|
250 shows "s1 = firstn (length s1) (s1 @ s2) \<and> s2 = restn (length s1) (s1 @ s2)" |
|
251 proof(rule length_eq_elim_l) |
|
252 have "length s1 \<le> length (s1 @ s2)" by simp |
|
253 from length_firstn_le [OF this] |
|
254 show "length s1 = length (firstn (length s1) (s1 @ s2))" by simp |
|
255 next |
|
256 from firstn_restn_s |
|
257 show "s1 @ s2 = firstn (length s1) (s1 @ s2) @ restn (length s1) (s1 @ s2)" |
|
258 by metis |
|
259 qed |
|
260 |
|
261 |
37 |
262 lemma length_moment_le: |
38 lemma length_moment_le: |
263 fixes k s |
|
264 assumes le_k: "k \<le> length s" |
39 assumes le_k: "k \<le> length s" |
265 shows "length (moment k s) = k" |
40 shows "length (moment k s) = k" |
266 proof - |
41 using le_k unfolding moment_def by auto |
267 have "length (rev (firstn k (rev s))) = k" |
|
268 proof - |
|
269 have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp |
|
270 also have "\<dots> = k" |
|
271 proof(rule length_firstn_le) |
|
272 from le_k show "k \<le> length (rev s)" by simp |
|
273 qed |
|
274 finally show ?thesis . |
|
275 qed |
|
276 thus ?thesis by (simp add:moment_def) |
|
277 qed |
|
278 |
|
279 lemma app_moment_restm: |
|
280 fixes s1 s2 |
|
281 shows "s1 = restm (length s2) (s1 @ s2) \<and> s2 = moment (length s2) (s1 @ s2)" |
|
282 proof(rule length_eq_elim_r) |
|
283 have "length s2 \<le> length (s1 @ s2)" by simp |
|
284 from length_moment_le [OF this] |
|
285 show "length s2 = length (moment (length s2) (s1 @ s2))" by simp |
|
286 next |
|
287 from moment_restm_s |
|
288 show "s1 @ s2 = restm (length s2) (s1 @ s2) @ moment (length s2) (s1 @ s2)" |
|
289 by metis |
|
290 qed |
|
291 |
42 |
292 lemma length_moment_ge: |
43 lemma length_moment_ge: |
293 fixes k s |
|
294 assumes le_k: "length s \<le> k" |
44 assumes le_k: "length s \<le> k" |
295 shows "length (moment k s) = (length s)" |
45 shows "length (moment k s) = (length s)" |
296 proof - |
46 using assms unfolding moment_def by simp |
297 have "length (rev (firstn k (rev s))) = length s" |
47 |
298 proof - |
48 lemma length_take: |
299 have "length (rev (firstn k (rev s))) = length (firstn k (rev s))" by simp |
49 "(length (take n s) = length s) \<or> (length (take n s) = n)" |
300 also have "\<dots> = length s" |
50 by (metis length_take min_def) |
301 proof - |
51 |
302 have "\<dots> = length (rev s)" |
52 lemma take_conc: |
303 proof(rule length_firstn_ge) |
|
304 from le_k show "length (rev s) \<le> k" by simp |
|
305 qed |
|
306 also have "\<dots> = length s" by simp |
|
307 finally show ?thesis . |
|
308 qed |
|
309 finally show ?thesis . |
|
310 qed |
|
311 thus ?thesis by (simp add:moment_def) |
|
312 qed |
|
313 |
|
314 lemma length_firstn: "(length (firstn n s) = length s) \<or> (length (firstn n s) = n)" |
|
315 proof(cases "n \<le> length s") |
|
316 case True |
|
317 from length_firstn_le [OF True] show ?thesis by auto |
|
318 next |
|
319 case False |
|
320 from False have "length s \<le> n" by simp |
|
321 from firstn_ge [OF this] show ?thesis by auto |
|
322 qed |
|
323 |
|
324 lemma firstn_conc: |
|
325 fixes m n |
|
326 assumes le_mn: "m \<le> n" |
53 assumes le_mn: "m \<le> n" |
327 shows "firstn m s = firstn m (firstn n s)" |
54 shows "take m s = take m (take n s)" |
328 proof(cases "m \<le> length s") |
55 using assms by (metis min.absorb1 take_take) |
329 case True |
|
330 have "s = (firstn n s) @ (restn n s)" by (simp add:firstn_restn_s) |
|
331 hence "firstn m s = firstn m \<dots>" by simp |
|
332 also have "\<dots> = firstn m (firstn n s)" |
|
333 proof - |
|
334 from length_firstn [of n s] |
|
335 have "m \<le> length (firstn n s)" |
|
336 proof |
|
337 assume "length (firstn n s) = length s" with True show ?thesis by simp |
|
338 next |
|
339 assume "length (firstn n s) = n " with le_mn show ?thesis by simp |
|
340 qed |
|
341 from firstn_le [OF this, of "restn n s"] |
|
342 show ?thesis . |
|
343 qed |
|
344 finally show ?thesis by simp |
|
345 next |
|
346 case False |
|
347 from False and le_mn have "length s \<le> n" by simp |
|
348 from firstn_ge [OF this] show ?thesis by simp |
|
349 qed |
|
350 |
|
351 lemma restn_conc: |
|
352 fixes i j k s |
|
353 assumes eq_k: "j + i = k" |
|
354 shows "restn k s = restn j (restn i s)" |
|
355 proof - |
|
356 have "(firstn (length s - k) (rev s)) = |
|
357 (firstn (length (rev (firstn (length s - i) (rev s))) - j) |
|
358 (rev (rev (firstn (length s - i) (rev s)))))" |
|
359 proof - |
|
360 have "(firstn (length s - k) (rev s)) = |
|
361 (firstn (length (rev (firstn (length s - i) (rev s))) - j) |
|
362 (firstn (length s - i) (rev s)))" |
|
363 proof - |
|
364 have " (length (rev (firstn (length s - i) (rev s))) - j) = length s - k" |
|
365 proof - |
|
366 have "(length (rev (firstn (length s - i) (rev s))) - j) = (length s - i) - j" |
|
367 proof - |
|
368 have "(length (rev (firstn (length s - i) (rev s))) - j) = |
|
369 length ((firstn (length s - i) (rev s))) - j" |
|
370 by simp |
|
371 also have "\<dots> = length ((firstn (length (rev s) - i) (rev s))) - j" by simp |
|
372 also have "\<dots> = (length (rev s) - i) - j" |
|
373 proof - |
|
374 have "length ((firstn (length (rev s) - i) (rev s))) = (length (rev s) - i)" |
|
375 by (rule length_firstn_le, simp) |
|
376 thus ?thesis by simp |
|
377 qed |
|
378 also have "\<dots> = (length s - i) - j" by simp |
|
379 finally show ?thesis . |
|
380 qed |
|
381 with eq_k show ?thesis by auto |
|
382 qed |
|
383 moreover have "(firstn (length s - k) (rev s)) = |
|
384 (firstn (length s - k) (firstn (length s - i) (rev s)))" |
|
385 proof(rule firstn_conc) |
|
386 from eq_k show "length s - k \<le> length s - i" by simp |
|
387 qed |
|
388 ultimately show ?thesis by simp |
|
389 qed |
|
390 thus ?thesis by simp |
|
391 qed |
|
392 thus ?thesis by (simp only:restn.simps) |
|
393 qed |
|
394 |
56 |
395 (* |
57 (* |
396 value "down_to 2 0 [5, 4, 3, 2, 1, 0]" |
58 value "down_to 2 0 [5, 4, 3, 2, 1, 0]" |
397 value "moment 2 [5, 4, 3, 2, 1, 0]" |
59 value "moment 2 [5, 4, 3, 2, 1, 0]" |
398 *) |
60 *) |
399 |
61 |
400 lemma from_to_firstn: "from_to 0 k s = firstn k s" |
62 lemma from_to_take: "from_to 0 k s = take k s" |
401 by (simp add:from_to_def restn.simps) |
63 by (simp add:from_to_def drop.simps) |
402 |
64 |
403 lemma moment_app [simp]: |
65 lemma moment_app [simp]: |
404 assumes |
66 assumes ile: "i \<le> length s" |
405 ile: "i \<le> length s" |
|
406 shows "moment i (s'@s) = moment i s" |
67 shows "moment i (s'@s) = moment i s" |
407 proof - |
68 using assms unfolding moment_def by simp |
408 have "moment i (s'@s) = rev (firstn i (rev (s'@s)))" by (simp add:moment_def) |
|
409 moreover have "firstn i (rev (s'@s)) = firstn i (rev s @ rev s')" by simp |
|
410 moreover have "\<dots> = firstn i (rev s)" |
|
411 proof(rule firstn_le) |
|
412 have "length (rev s) = length s" by simp |
|
413 with ile show "i \<le> length (rev s)" by simp |
|
414 qed |
|
415 ultimately show ?thesis by (simp add:moment_def) |
|
416 qed |
|
417 |
69 |
418 lemma moment_eq [simp]: "moment (length s) (s'@s) = s" |
70 lemma moment_eq [simp]: "moment (length s) (s'@s) = s" |
419 proof - |
71 unfolding moment_def by simp |
420 have "length s \<le> length s" by simp |
|
421 from moment_app [OF this, of s'] |
|
422 have " moment (length s) (s' @ s) = moment (length s) s" . |
|
423 moreover have "\<dots> = s" by (simp add:moment_def) |
|
424 ultimately show ?thesis by simp |
|
425 qed |
|
426 |
72 |
427 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s" |
73 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s" |
428 by (unfold moment_def, simp) |
74 by (unfold moment_def, simp) |
429 |
75 |
430 lemma moment_zero [simp]: "moment 0 s = []" |
76 lemma moment_zero [simp]: "moment 0 s = []" |
431 by (simp add:moment_def firstn.simps) |
77 by (simp add:moment_def) |
432 |
78 |
433 lemma p_split_gen: |
79 lemma p_split_gen: |
434 "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> \<Longrightarrow> |
80 "\<lbrakk>Q s; \<not> Q (moment k s)\<rbrakk> \<Longrightarrow> |
435 (\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
81 (\<exists> i. i < length s \<and> k \<le> i \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
436 proof (induct s, simp) |
82 proof (induct s, simp) |
571 ultimately show ?thesis by auto |
273 ultimately show ?thesis by auto |
572 qed |
274 qed |
573 qed |
275 qed |
574 qed |
276 qed |
575 |
277 |
576 lemma from_to_conc: |
|
577 fixes i j k s |
|
578 assumes le_ij: "i \<le> j" |
|
579 and le_jk: "j \<le> k" |
|
580 shows "from_to i j s @ from_to j k s = from_to i k s" |
|
581 proof - |
|
582 let ?ris = "restn i s" |
|
583 have "firstn (j - i) (restn i s) @ firstn (k - j) (restn j s) = |
|
584 firstn (k - i) (restn i s)" (is "?x @ ?y = ?z") |
|
585 proof - |
|
586 let "firstn (k-j) ?u" = "?y" |
|
587 let ?rst = " restn (k - j) (restn (j - i) ?ris)" |
|
588 let ?rst' = "restn (k - i) ?ris" |
|
589 have "?u = restn (j-i) ?ris" |
|
590 proof(rule restn_conc) |
|
591 from le_ij show "j - i + i = j" by simp |
|
592 qed |
|
593 hence "?x @ ?y = ?x @ firstn (k-j) (restn (j-i) ?ris)" by simp |
|
594 moreover have "firstn (k - j) (restn (j - i) (restn i s)) @ ?rst = |
|
595 restn (j-i) ?ris" by (simp add:firstn_restn_s) |
|
596 ultimately have "?x @ ?y @ ?rst = ?x @ (restn (j-i) ?ris)" by simp |
|
597 also have "\<dots> = ?ris" by (simp add:firstn_restn_s) |
|
598 finally have "?x @ ?y @ ?rst = ?ris" . |
|
599 moreover have "?z @ ?rst = ?ris" |
|
600 proof - |
|
601 have "?z @ ?rst' = ?ris" by (simp add:firstn_restn_s) |
|
602 moreover have "?rst' = ?rst" |
|
603 proof(rule restn_conc) |
|
604 from le_ij le_jk show "k - j + (j - i) = k - i" by auto |
|
605 qed |
|
606 ultimately show ?thesis by simp |
|
607 qed |
|
608 ultimately have "?x @ ?y @ ?rst = ?z @ ?rst" by simp |
|
609 thus ?thesis by auto |
|
610 qed |
|
611 thus ?thesis by (simp only:from_to_def) |
|
612 qed |
|
613 |
|
614 lemma down_to_conc: |
|
615 fixes i j k s |
|
616 assumes le_ij: "i \<le> j" |
|
617 and le_jk: "j \<le> k" |
|
618 shows "down_to k j s @ down_to j i s = down_to k i s" |
|
619 proof - |
|
620 have "rev (from_to j k (rev s)) @ rev (from_to i j (rev s)) = rev (from_to i k (rev s))" |
|
621 (is "?L = ?R") |
|
622 proof - |
|
623 have "?L = rev (from_to i j (rev s) @ from_to j k (rev s))" by simp |
|
624 also have "\<dots> = ?R" (is "rev ?x = rev ?y") |
|
625 proof - |
|
626 have "?x = ?y" by (rule from_to_conc[OF le_ij le_jk]) |
|
627 thus ?thesis by simp |
|
628 qed |
|
629 finally show ?thesis . |
|
630 qed |
|
631 thus ?thesis by (simp add:down_to_def) |
|
632 qed |
|
633 |
|
634 lemma restn_ge: |
|
635 fixes s k |
|
636 assumes le_k: "length s \<le> k" |
|
637 shows "restn k s = []" |
|
638 proof - |
|
639 from firstn_restn_s [of k s, symmetric] have "s = (firstn k s) @ (restn k s)" . |
|
640 hence "length s = length \<dots>" by simp |
|
641 also have "\<dots> = length (firstn k s) + length (restn k s)" by simp |
|
642 finally have "length s = ..." by simp |
|
643 moreover from length_firstn_ge and le_k |
|
644 have "length (firstn k s) = length s" by simp |
|
645 ultimately have "length (restn k s) = 0" by auto |
|
646 thus ?thesis by auto |
|
647 qed |
|
648 |
|
649 lemma from_to_ge: "length s \<le> k \<Longrightarrow> from_to k j s = []" |
|
650 proof(simp only:from_to_def) |
|
651 assume "length s \<le> k" |
|
652 from restn_ge [OF this] |
|
653 show "firstn (j - k) (restn k s) = []" by simp |
|
654 qed |
|
655 |
|
656 (* |
|
657 value "from_to 2 5 [0, 1, 2, 3, 4]" |
|
658 value "restn 2 [0, 1, 2, 3, 4]" |
|
659 *) |
|
660 |
|
661 lemma from_to_restn: |
|
662 fixes k j s |
|
663 assumes le_j: "length s \<le> j" |
|
664 shows "from_to k j s = restn k s" |
|
665 proof - |
|
666 have "from_to 0 k s @ from_to k j s = from_to 0 j s" |
|
667 proof(cases "k \<le> j") |
|
668 case True |
|
669 from from_to_conc True show ?thesis by auto |
|
670 next |
|
671 case False |
|
672 from False le_j have lek: "length s \<le> k" by auto |
|
673 from from_to_ge [OF this] have "from_to k j s = []" . |
|
674 hence "from_to 0 k s @ from_to k j s = from_to 0 k s" by simp |
|
675 also have "\<dots> = s" |
|
676 proof - |
|
677 from from_to_firstn [of k s] |
|
678 have "\<dots> = firstn k s" . |
|
679 also have "\<dots> = s" by (rule firstn_ge [OF lek]) |
|
680 finally show ?thesis . |
|
681 qed |
|
682 finally have "from_to 0 k s @ from_to k j s = s" . |
|
683 moreover have "from_to 0 j s = s" |
|
684 proof - |
|
685 have "from_to 0 j s = firstn j s" by (simp add:from_to_firstn) |
|
686 also have "\<dots> = s" |
|
687 proof(rule firstn_ge) |
|
688 from le_j show "length s \<le> j " by simp |
|
689 qed |
|
690 finally show ?thesis . |
|
691 qed |
|
692 ultimately show ?thesis by auto |
|
693 qed |
|
694 also have "\<dots> = s" |
|
695 proof - |
|
696 from from_to_firstn have "\<dots> = firstn j s" . |
|
697 also have "\<dots> = s" |
|
698 proof(rule firstn_ge) |
|
699 from le_j show "length s \<le> j" by simp |
|
700 qed |
|
701 finally show ?thesis . |
|
702 qed |
|
703 finally have "from_to 0 k s @ from_to k j s = s" . |
|
704 moreover have "from_to 0 k s @ restn k s = s" |
|
705 proof - |
|
706 from from_to_firstn [of k s] |
|
707 have "from_to 0 k s = firstn k s" . |
|
708 thus ?thesis by (simp add:firstn_restn_s) |
|
709 qed |
|
710 ultimately have "from_to 0 k s @ from_to k j s = |
|
711 from_to 0 k s @ restn k s" by simp |
|
712 thus ?thesis by auto |
|
713 qed |
|
714 |
|
715 lemma down_to_moment: "down_to k 0 s = moment k s" |
|
716 proof - |
|
717 have "rev (from_to 0 k (rev s)) = rev (firstn k (rev s))" |
|
718 using from_to_firstn by metis |
|
719 thus ?thesis by (simp add:down_to_def moment_def) |
|
720 qed |
|
721 |
|
722 lemma down_to_restm: |
|
723 assumes le_s: "length s \<le> j" |
|
724 shows "down_to j k s = restm k s" |
|
725 proof - |
|
726 have "rev (from_to k j (rev s)) = rev (restn k (rev s))" (is "?L = ?R") |
|
727 proof - |
|
728 from le_s have "length (rev s) \<le> j" by simp |
|
729 from from_to_restn [OF this, of k] show ?thesis by simp |
|
730 qed |
|
731 thus ?thesis by (simp add:down_to_def restm_def) |
|
732 qed |
|
733 |
|
734 lemma moment_split: "moment (m+i) s = down_to (m+i) i s @down_to i 0 s" |
|
735 proof - |
|
736 have "moment (m + i) s = down_to (m+i) 0 s" using down_to_moment by metis |
|
737 also have "\<dots> = (down_to (m+i) i s) @ (down_to i 0 s)" |
|
738 by(rule down_to_conc[symmetric], auto) |
|
739 finally show ?thesis . |
|
740 qed |
|
741 |
|
742 lemma length_restn: "length (restn i s) = length s - i" |
|
743 proof(cases "i \<le> length s") |
|
744 case True |
|
745 from length_firstn_le [OF this] have "length (firstn i s) = i" . |
|
746 moreover have "length s = length (firstn i s) + length (restn i s)" |
|
747 proof - |
|
748 have "s = firstn i s @ restn i s" using firstn_restn_s by metis |
|
749 hence "length s = length \<dots>" by simp |
|
750 thus ?thesis by simp |
|
751 qed |
|
752 ultimately show ?thesis by simp |
|
753 next |
|
754 case False |
|
755 hence "length s \<le> i" by simp |
|
756 from restn_ge [OF this] have "restn i s = []" . |
|
757 with False show ?thesis by simp |
|
758 qed |
|
759 |
|
760 lemma length_from_to_in: |
|
761 fixes i j s |
|
762 assumes le_ij: "i \<le> j" |
|
763 and le_j: "j \<le> length s" |
|
764 shows "length (from_to i j s) = j - i" |
|
765 proof - |
|
766 have "from_to 0 j s = from_to 0 i s @ from_to i j s" |
|
767 by (rule from_to_conc[symmetric, OF _ le_ij], simp) |
|
768 moreover have "length (from_to 0 j s) = j" |
|
769 proof - |
|
770 have "from_to 0 j s = firstn j s" using from_to_firstn by metis |
|
771 moreover have "length \<dots> = j" by (rule length_firstn_le [OF le_j]) |
|
772 ultimately show ?thesis by simp |
|
773 qed |
|
774 moreover have "length (from_to 0 i s) = i" |
|
775 proof - |
|
776 have "from_to 0 i s = firstn i s" using from_to_firstn by metis |
|
777 moreover have "length \<dots> = i" |
|
778 proof (rule length_firstn_le) |
|
779 from le_ij le_j show "i \<le> length s" by simp |
|
780 qed |
|
781 ultimately show ?thesis by simp |
|
782 qed |
|
783 ultimately show ?thesis by auto |
|
784 qed |
|
785 |
|
786 lemma firstn_restn_from_to: "from_to i (m + i) s = firstn m (restn i s)" |
|
787 proof(cases "m+i \<le> length s") |
|
788 case True |
|
789 have "restn i s = from_to i (m+i) s @ from_to (m+i) (length s) s" |
|
790 proof - |
|
791 have "restn i s = from_to i (length s) s" |
|
792 by(rule from_to_restn[symmetric], simp) |
|
793 also have "\<dots> = from_to i (m+i) s @ from_to (m+i) (length s) s" |
|
794 by(rule from_to_conc[symmetric, OF _ True], simp) |
|
795 finally show ?thesis . |
|
796 qed |
|
797 hence "firstn m (restn i s) = firstn m \<dots>" by simp |
|
798 moreover have "\<dots> = firstn (length (from_to i (m+i) s)) |
|
799 (from_to i (m+i) s @ from_to (m+i) (length s) s)" |
|
800 proof - |
|
801 have "length (from_to i (m+i) s) = m" |
|
802 proof - |
|
803 have "length (from_to i (m+i) s) = (m+i) - i" |
|
804 by(rule length_from_to_in [OF _ True], simp) |
|
805 thus ?thesis by simp |
|
806 qed |
|
807 thus ?thesis by simp |
|
808 qed |
|
809 ultimately show ?thesis using app_firstn_restn by metis |
|
810 next |
|
811 case False |
|
812 hence "length s \<le> m + i" by simp |
|
813 from from_to_restn [OF this] |
|
814 have "from_to i (m + i) s = restn i s" . |
|
815 moreover have "firstn m (restn i s) = restn i s" |
|
816 proof(rule firstn_ge) |
|
817 show "length (restn i s) \<le> m" |
|
818 proof - |
|
819 have "length (restn i s) = length s - i" using length_restn by metis |
|
820 with False show ?thesis by simp |
|
821 qed |
|
822 qed |
|
823 ultimately show ?thesis by simp |
|
824 qed |
|
825 |
|
826 lemma down_to_moment_restm: |
|
827 fixes m i s |
|
828 shows "down_to (m + i) i s = moment m (restm i s)" |
|
829 by (simp add:firstn_restn_from_to down_to_def moment_def restm_def) |
|
830 |
|
831 lemma moment_plus_split: |
|
832 fixes m i s |
|
833 shows "moment (m + i) s = moment m (restm i s) @ moment i s" |
|
834 proof - |
|
835 from moment_split [of m i s] |
|
836 have "moment (m + i) s = down_to (m + i) i s @ down_to i 0 s" . |
|
837 also have "\<dots> = down_to (m+i) i s @ moment i s" using down_to_moment by simp |
|
838 also from down_to_moment_restm have "\<dots> = moment m (restm i s) @ moment i s" |
|
839 by simp |
|
840 finally show ?thesis . |
|
841 qed |
|
842 |
|
843 lemma length_restm: "length (restm i s) = length s - i" |
|
844 proof - |
|
845 have "length (rev (restn i (rev s))) = length s - i" (is "?L = ?R") |
|
846 proof - |
|
847 have "?L = length (restn i (rev s))" by simp |
|
848 also have "\<dots> = length (rev s) - i" using length_restn by metis |
|
849 also have "\<dots> = ?R" by simp |
|
850 finally show ?thesis . |
|
851 qed |
|
852 thus ?thesis by (simp add:restm_def) |
|
853 qed |
|
854 |
|
855 lemma moment_prefix: "(moment i t @ s) = moment (i + length s) (t @ s)" |
|
856 proof - |
|
857 from moment_plus_split [of i "length s" "t@s"] |
|
858 have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)" |
|
859 by auto |
|
860 with app_moment_restm[of t s] |
|
861 have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" by simp |
|
862 with moment_app show ?thesis by auto |
|
863 qed |
|
864 |
|
865 end |
278 end |