3 begin |
3 begin |
4 |
4 |
5 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
5 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
6 where "moment n s = rev (take n (rev s))" |
6 where "moment n s = rev (take n (rev s))" |
7 |
7 |
8 value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
|
9 |
|
10 definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
8 definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
11 where "restm n s = rev (drop n (rev s))" |
9 where "restm n s = rev (drop n (rev s))" |
12 |
10 |
|
11 value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
|
12 value "moment 2 [5, 4, 3, 2, 1, 0::int]" |
|
13 |
13 value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
14 value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
14 |
|
15 definition from_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
16 where "from_to i j s = take (j - i) (drop i s)" |
|
17 |
|
18 definition down_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
19 where "down_to j i s = rev (from_to i j (rev s))" |
|
20 |
|
21 value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]" |
|
22 value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]" |
|
23 |
|
24 value "from_to 0 2 [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]" |
|
26 |
|
27 |
15 |
28 lemma moment_restm_s: "(restm n s) @ (moment n s) = s" |
16 lemma moment_restm_s: "(restm n s) @ (moment n s) = s" |
29 unfolding restm_def moment_def |
17 unfolding restm_def moment_def |
30 by (metis append_take_drop_id rev_append rev_rev_ident) |
18 by (metis append_take_drop_id rev_append rev_rev_ident) |
31 |
|
32 declare drop.simps [simp del] |
|
33 |
|
34 lemma length_take_le: |
|
35 "n \<le> length s \<Longrightarrow> length (take n s) = n" |
|
36 by (metis length_take min.absorb2) |
|
37 |
19 |
38 lemma length_moment_le: |
20 lemma length_moment_le: |
39 assumes le_k: "k \<le> length s" |
21 assumes le_k: "k \<le> length s" |
40 shows "length (moment k s) = k" |
22 shows "length (moment k s) = k" |
41 using le_k unfolding moment_def by auto |
23 using le_k unfolding moment_def by auto |
43 lemma length_moment_ge: |
25 lemma length_moment_ge: |
44 assumes le_k: "length s \<le> k" |
26 assumes le_k: "length s \<le> k" |
45 shows "length (moment k s) = (length s)" |
27 shows "length (moment k s) = (length s)" |
46 using assms unfolding moment_def by simp |
28 using assms unfolding moment_def by simp |
47 |
29 |
48 lemma length_take: |
|
49 "(length (take n s) = length s) \<or> (length (take n s) = n)" |
|
50 by (metis length_take min_def) |
|
51 |
|
52 lemma take_conc: |
|
53 assumes le_mn: "m \<le> n" |
|
54 shows "take m s = take m (take n s)" |
|
55 using assms by (metis min.absorb1 take_take) |
|
56 |
|
57 (* |
|
58 value "down_to 2 0 [5, 4, 3, 2, 1, 0]" |
|
59 value "moment 2 [5, 4, 3, 2, 1, 0]" |
|
60 *) |
|
61 |
|
62 lemma from_to_take: "from_to 0 k s = take k s" |
|
63 by (simp add:from_to_def drop.simps) |
|
64 |
|
65 lemma moment_app [simp]: |
30 lemma moment_app [simp]: |
66 assumes ile: "i \<le> length s" |
31 assumes ile: "i \<le> length s" |
67 shows "moment i (s'@s) = moment i s" |
32 shows "moment i (s' @ s) = moment i s" |
68 using assms unfolding moment_def by simp |
33 using assms unfolding moment_def by simp |
69 |
34 |
70 lemma moment_eq [simp]: "moment (length s) (s'@s) = s" |
35 lemma moment_eq [simp]: "moment (length s) (s' @ s) = s" |
71 unfolding moment_def by simp |
36 unfolding moment_def by simp |
72 |
37 |
73 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s" |
38 lemma moment_ge [simp]: "length s \<le> n \<Longrightarrow> moment n s = s" |
74 by (unfold moment_def, simp) |
39 by (unfold moment_def, simp) |
75 |
40 |
170 } ultimately show ?thesis by auto |
135 } ultimately show ?thesis by auto |
171 qed |
136 qed |
172 qed |
137 qed |
173 |
138 |
174 lemma p_split: |
139 lemma p_split: |
175 "\<And> s Q. \<lbrakk>Q s; \<not> Q []\<rbrakk> \<Longrightarrow> |
140 "\<lbrakk>Q s; \<not> Q []\<rbrakk> \<Longrightarrow> |
176 (\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
141 (\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
177 proof - |
142 proof - |
178 fix s Q |
143 fix s Q |
179 assume qs: "Q s" and nq: "\<not> Q []" |
144 assume qs: "Q s" and nq: "\<not> Q []" |
180 from nq have "\<not> Q (moment 0 s)" by simp |
145 from nq have "\<not> Q (moment 0 s)" by simp |
181 from p_split_gen [of Q s 0, OF qs this] |
146 from p_split_gen [of Q s 0, OF qs this] |
182 show "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
147 show "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
183 by auto |
148 by auto |
184 qed |
149 qed |
185 |
|
186 (* |
|
187 value "from_to 2 5 [0, 1, 2, 3, 4]" |
|
188 value "drop 2 [0, 1, 2, 3, 4]" |
|
189 *) |
|
190 |
|
191 (* |
|
192 lemma down_to_moment: "down_to k 0 s = moment k s" |
|
193 proof - |
|
194 have "rev (from_to 0 k (rev s)) = rev (take k (rev s))" |
|
195 using from_to_take by metis |
|
196 thus ?thesis by (simp add:down_to_def moment_def) |
|
197 qed |
|
198 *) |
|
199 |
150 |
200 lemma moment_plus_split: |
151 lemma moment_plus_split: |
201 shows "moment (m + i) s = moment m (restm i s) @ moment i s" |
152 shows "moment (m + i) s = moment m (restm i s) @ moment i s" |
202 unfolding moment_def restm_def |
153 unfolding moment_def restm_def |
203 by (metis add.commute rev_append rev_rev_ident take_add) |
154 by (metis add.commute rev_append rev_rev_ident take_add) |
209 have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)" |
160 have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)" |
210 by auto |
161 by auto |
211 have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" |
162 have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" |
212 by (simp add: moment_def) |
163 by (simp add: moment_def) |
213 with moment_app show ?thesis by auto |
164 with moment_app show ?thesis by auto |
214 qed |
|
215 |
|
216 lemma length_down_to_in: |
|
217 assumes le_ij: "i \<le> j" |
|
218 and le_js: "j \<le> length s" |
|
219 shows "length (down_to j i s) = j - i" |
|
220 using assms |
|
221 unfolding down_to_def from_to_def |
|
222 by (simp) |
|
223 |
|
224 lemma moment_head: |
|
225 assumes le_it: "Suc i \<le> length t" |
|
226 obtains e where "moment (Suc i) t = e#moment i t" |
|
227 proof - |
|
228 have "i \<le> Suc i" by simp |
|
229 from length_down_to_in [OF this le_it] |
|
230 have a: "length (down_to (Suc i) i t) = 1" by auto |
|
231 then obtain e where "down_to (Suc i) i t = [e]" |
|
232 apply (cases "(down_to (Suc i) i t)") by auto |
|
233 moreover have "down_to (Suc i) 0 t = down_to (Suc i) i t @ down_to i 0 t" |
|
234 unfolding down_to_def from_to_def rev_append[symmetric] |
|
235 apply(simp del: rev_append) |
|
236 by (metis One_nat_def Suc_eq_plus1_left add.commute take_add) |
|
237 ultimately have eq_me: "moment (Suc i) t = e # (moment i t)" |
|
238 by(simp add: moment_def down_to_def from_to_def) |
|
239 from that [OF this] show ?thesis . |
|
240 qed |
165 qed |
241 |
166 |
242 lemma moment_plus: |
167 lemma moment_plus: |
243 "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)" |
168 "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)" |
244 proof(induct s, simp+) |
169 proof(induct s, simp+) |