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])

     2.1 --- a/src/HOL/Nat.thy	Mon Nov 18 17:10:57 2013 +0100
     2.2 +++ b/src/HOL/Nat.thy	Mon Nov 18 17:14:01 2013 +0100
     2.3 @@ -1315,6 +1315,11 @@
     2.4    shows "comp f ^^ n = comp (f ^^ n)"
     2.5    by (induct n) simp_all
     2.6  
     2.7 +lemma Suc_funpow[simp]: "Suc ^^ n = (op + n)"
     2.8 +  by (induct n) simp_all
     2.9 +
    2.10 +lemma id_funpow[simp]: "id ^^ n = id"
    2.11 +  by (induct n) simp_all
    2.12  
    2.13  subsection {* Kleene iteration *}
    2.14