equal
deleted
inserted
replaced
3037 by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split) |
3037 by (induct j) (auto simp add: less_Suc_eq nth_append split: nat_diff_split) |
3038 |
3038 |
3039 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i" |
3039 lemma hd_upt[simp]: "i < j \<Longrightarrow> hd[i..<j] = i" |
3040 by(simp add:upt_conv_Cons) |
3040 by(simp add:upt_conv_Cons) |
3041 |
3041 |
|
3042 lemma tl_upt: "tl [m..<n] = [Suc m..<n]" |
|
3043 by (simp add: upt_rec) |
|
3044 |
3042 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1" |
3045 lemma last_upt[simp]: "i < j \<Longrightarrow> last[i..<j] = j - 1" |
3043 by(cases j)(auto simp: upt_Suc_append) |
3046 by(cases j)(auto simp: upt_Suc_append) |
3044 |
3047 |
3045 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]" |
3048 lemma take_upt [simp]: "i+m <= n ==> take m [i..<n] = [i..<i+m]" |
3046 apply (induct m arbitrary: i, simp) |
3049 apply (induct m arbitrary: i, simp) |