# HG changeset patch
# User hoelzl
# Date 1384791241 -3600
# Node ID 178922b63b58c41bc9a75e731e6b3931c3270571
# Parent  7468e8ce494ccc32898715d9bccf7282e2ee5dfc
add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt

diff -r 7468e8ce494c -r 178922b63b58 src/HOL/List.thy
--- 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])
diff -r 7468e8ce494c -r 178922b63b58 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Nov 18 17:10:57 2013 +0100
+++ b/src/HOL/Nat.thy	Mon Nov 18 17:14:01 2013 +0100
@@ -1315,6 +1315,11 @@
   shows "comp f ^^ n = comp (f ^^ n)"
   by (induct n) simp_all
 
+lemma Suc_funpow[simp]: "Suc ^^ n = (op + n)"
+  by (induct n) simp_all
+
+lemma id_funpow[simp]: "id ^^ n = id"
+  by (induct n) simp_all
 
 subsection {* Kleene iteration *}