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 definition restm :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
|
9 where "restm n s = rev (drop n (rev s))" |
|
10 |
|
11 value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
8 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]" |
9 value "moment 2 [5, 4, 3, 2, 1, 0::int]" |
13 |
10 |
14 value "restm 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
11 (* |
15 |
|
16 lemma moment_restm_s: "(restm n s) @ (moment n s) = s" |
|
17 unfolding restm_def moment_def |
|
18 by (metis append_take_drop_id rev_append rev_rev_ident) |
|
19 |
|
20 lemma length_moment_le: |
12 lemma length_moment_le: |
21 assumes le_k: "k \<le> length s" |
13 assumes le_k: "k \<le> length s" |
22 shows "length (moment k s) = k" |
14 shows "length (moment k s) = k" |
23 using le_k unfolding moment_def by auto |
15 using le_k unfolding moment_def by auto |
|
16 *) |
24 |
17 |
|
18 (* |
25 lemma length_moment_ge: |
19 lemma length_moment_ge: |
26 assumes le_k: "length s \<le> k" |
20 assumes le_k: "length s \<le> k" |
27 shows "length (moment k s) = (length s)" |
21 shows "length (moment k s) = (length s)" |
28 using assms unfolding moment_def by simp |
22 using assms unfolding moment_def by simp |
|
23 *) |
29 |
24 |
30 lemma moment_app [simp]: |
25 lemma moment_app [simp]: |
31 assumes ile: "i \<le> length s" |
26 assumes ile: "i \<le> length s" |
32 shows "moment i (s' @ s) = moment i s" |
27 shows "moment i (s' @ s) = moment i s" |
33 using assms unfolding moment_def by simp |
28 using assms unfolding moment_def by simp |
146 from p_split_gen [of Q s 0, OF qs this] |
141 from p_split_gen [of Q s 0, OF qs this] |
147 show "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
142 show "(\<exists> i. i < length s \<and> \<not> Q (moment i s) \<and> (\<forall> i' > i. Q (moment i' s)))" |
148 by auto |
143 by auto |
149 qed |
144 qed |
150 |
145 |
151 lemma moment_plus_split: |
146 lemma moment_Suc_tl: |
152 shows "moment (m + i) s = moment m (restm i s) @ moment i s" |
147 assumes "Suc i \<le> length s" |
153 unfolding moment_def restm_def |
148 shows "tl (moment (Suc i) s) = moment i s" |
154 by (metis add.commute rev_append rev_rev_ident take_add) |
149 using assms unfolding moment_def |
|
150 sorry |
155 |
151 |
156 lemma moment_prefix: |
152 |
157 "(moment i t @ s) = moment (i + length s) (t @ s)" |
153 lemma moment_plus: |
|
154 assumes "Suc i \<le> length s" |
|
155 shows "(moment (Suc i) s) = (hd (moment (Suc i) s)) # (moment i s)" |
158 proof - |
156 proof - |
159 from moment_plus_split [of i "length s" "t@s"] |
157 have "(moment (Suc i) s) \<noteq> []" |
160 have " moment (i + length s) (t @ s) = moment i (restm (length s) (t @ s)) @ moment (length s) (t @ s)" |
158 using assms by (auto simp add: moment_def) |
|
159 hence "(moment (Suc i) s) = (hd (moment (Suc i) s)) # tl (moment (Suc i) s)" |
161 by auto |
160 by auto |
162 have "moment (i + length s) (t @ s) = moment i t @ moment (length s) (t @ s)" |
161 with moment_Suc_tl[OF assms] |
163 by (simp add: moment_def) |
162 show ?thesis by metis |
164 with moment_app show ?thesis by auto |
|
165 qed |
|
166 |
|
167 lemma moment_plus: |
|
168 "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = (hd (moment (Suc i) s)) # (moment i s)" |
|
169 proof(induct s, simp+) |
|
170 fix a s |
|
171 assume ih: "Suc i \<le> length s \<Longrightarrow> moment (Suc i) s = hd (moment (Suc i) s) # moment i s" |
|
172 and le_i: "i \<le> length s" |
|
173 show "moment (Suc i) (a # s) = hd (moment (Suc i) (a # s)) # moment i (a # s)" |
|
174 proof(cases "i= length s") |
|
175 case True |
|
176 hence "Suc i = length (a#s)" by simp |
|
177 with moment_eq have "moment (Suc i) (a#s) = a#s" by auto |
|
178 moreover have "moment i (a#s) = s" |
|
179 proof - |
|
180 from moment_app [OF le_i, of "[a]"] |
|
181 and True show ?thesis by simp |
|
182 qed |
|
183 ultimately show ?thesis by auto |
|
184 next |
|
185 case False |
|
186 from False and le_i have lti: "i < length s" by arith |
|
187 hence les_i: "Suc i \<le> length s" by arith |
|
188 show ?thesis |
|
189 proof - |
|
190 from moment_app [OF les_i, of "[a]"] |
|
191 have "moment (Suc i) (a # s) = moment (Suc i) s" by simp |
|
192 moreover have "moment i (a#s) = moment i s" |
|
193 proof - |
|
194 from lti have "i \<le> length s" by simp |
|
195 from moment_app [OF this, of "[a]"] show ?thesis by simp |
|
196 qed |
|
197 moreover note ih [OF les_i] |
|
198 ultimately show ?thesis by auto |
|
199 qed |
|
200 qed |
|
201 qed |
163 qed |
202 |
164 |
203 end |
165 end |
204 |
166 |