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]" |
8 value "moment 3 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9::int]" |
9 value "moment 2 [5, 4, 3, 2, 1, 0::int]" |
9 value "moment 2 [5, 4, 3, 2, 1, 0::int]" |
10 |
|
11 (* |
|
12 lemma length_moment_le: |
|
13 assumes le_k: "k \<le> length s" |
|
14 shows "length (moment k s) = k" |
|
15 using le_k unfolding moment_def by auto |
|
16 *) |
|
17 |
|
18 (* |
|
19 lemma length_moment_ge: |
|
20 assumes le_k: "length s \<le> k" |
|
21 shows "length (moment k s) = (length s)" |
|
22 using assms unfolding moment_def by simp |
|
23 *) |
|
24 |
10 |
25 lemma moment_app [simp]: |
11 lemma moment_app [simp]: |
26 assumes ile: "i \<le> length s" |
12 assumes ile: "i \<le> length s" |
27 shows "moment i (s' @ s) = moment i s" |
13 shows "moment i (s' @ s) = moment i s" |
28 using assms unfolding moment_def by simp |
14 using assms unfolding moment_def by simp |