changeset 54496 | 178922b63b58 |
parent 54404 | 9f0f1152c875 |
child 54498 | f7fef6b00bfe |
--- a/src/HOL/List.thy Mon Nov 18 17:10:57 2013 +0100 +++ b/src/HOL/List.thy Mon Nov 18 17:14:01 2013 +0100 @@ -2988,6 +2988,9 @@ lemma map_Suc_upt: "map Suc [m..<n] = [Suc m..<Suc n]" by (induct n) auto +lemma map_add_upt: "map (\<lambda>i. i + n) [0..<m] = [n..<m + n]" + by (induct m) simp_all + lemma nth_map_upt: "i < n-m ==> (map f [m..<n]) ! i = f(m+i)" apply (induct n m arbitrary: i rule: diff_induct) prefer 3 apply (subst map_Suc_upt[symmetric])