equal
deleted
inserted
replaced
2986 done |
2986 done |
2987 |
2987 |
2988 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]" |
2988 lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]" |
2989 by (induct n) auto |
2989 by (induct n) auto |
2990 |
2990 |
|
2991 lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]" |
|
2992 by (induct m) simp_all |
|
2993 |
2991 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)" |
2994 lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)" |
2992 apply (induct n m arbitrary: i rule: diff_induct) |
2995 apply (induct n m arbitrary: i rule: diff_induct) |
2993 prefer 3 apply (subst map_Suc_upt[symmetric]) |
2996 prefer 3 apply (subst map_Suc_upt[symmetric]) |
2994 apply (auto simp add: less_diff_conv) |
2997 apply (auto simp add: less_diff_conv) |
2995 done |
2998 done |