6 where |
6 where |
7 "firstn 0 s = []" | |
7 "firstn 0 s = []" | |
8 "firstn (Suc n) [] = []" | |
8 "firstn (Suc n) [] = []" | |
9 "firstn (Suc n) (e#s) = e#(firstn n s)" |
9 "firstn (Suc n) (e#s) = e#(firstn n s)" |
10 |
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 |
11 fun restn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
96 fun restn :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
12 where "restn n s = rev (firstn (length s - n) (rev s))" |
97 where "restn n s = rev (firstn (length s - n) (rev s))" |
13 |
98 |
14 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
99 definition moment :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
15 where "moment n s = rev (firstn n (rev s))" |
100 where "moment n s = rev (firstn n (rev s))" |
21 where "from_to i j s = firstn (j - i) (restn i s)" |
106 where "from_to i j s = firstn (j - i) (restn i s)" |
22 |
107 |
23 definition down_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
108 definition down_to :: "nat \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> 'a list" |
24 where "down_to j i s = rev (from_to i j (rev s))" |
109 where "down_to j i s = rev (from_to i j (rev s))" |
25 |
110 |
26 (* |
|
27 value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]" |
111 value "down_to 6 2 [10, 9, 8, 7, 6, 5, 4, 3, 2, 1, 0]" |
28 value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]" |
112 value "from_to 2 6 [0, 1, 2, 3, 4, 5, 6, 7]" |
29 *) |
|
30 |
113 |
31 lemma length_eq_elim_l: "\<lbrakk>length xs = length ys; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs" |
114 lemma length_eq_elim_l: "\<lbrakk>length xs = length ys; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs" |
32 by auto |
115 by auto |
33 |
116 |
34 lemma length_eq_elim_r: "\<lbrakk>length us = length vs; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs" |
117 lemma length_eq_elim_r: "\<lbrakk>length us = length vs; xs@us = ys@vs\<rbrakk> \<Longrightarrow> xs = ys \<and> us = vs" |
35 by simp |
118 by simp |
36 |
119 |
37 lemma firstn_nil [simp]: "firstn n [] = []" |
120 lemma firstn_nil [simp]: "firstn n [] = []" |
38 by (cases n, simp+) |
121 by (cases n, simp+) |
39 |
122 |
40 (* |
123 |
41 value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ |
124 value "from_to 0 2 [0, 1, 2, 3, 4, 5, 6, 7, 8, 9] @ |
42 from_to 2 5 [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]" |
43 *) |
|
44 |
126 |
45 lemma firstn_le: "\<And> n s'. n \<le> length s \<Longrightarrow> firstn n (s@s') = firstn n s" |
127 lemma firstn_le: "\<And> n s'. n \<le> length s \<Longrightarrow> firstn n (s@s') = firstn n s" |
46 proof (induct s, simp) |
128 proof (induct s, simp) |
47 fix a s n s' |
129 fix a s n s' |
48 assume ih: "\<And>n s'. n \<le> length s \<Longrightarrow> firstn n (s @ s') = firstn n s" |
130 assume ih: "\<And>n s'. n \<le> length s \<Longrightarrow> firstn n (s @ s') = firstn n s" |