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