src/HOL/Nat.thy
changeset 54496 178922b63b58
parent 54411 f72e58a5a75f
child 54742 7a86358a3c0b
     1.1 --- a/src/HOL/Nat.thy	Mon Nov 18 17:10:57 2013 +0100
     1.2 +++ b/src/HOL/Nat.thy	Mon Nov 18 17:14:01 2013 +0100
     1.3 @@ -1315,6 +1315,11 @@
     1.4    shows "comp f ^^ n = comp (f ^^ n)"
     1.5    by (induct n) simp_all
     1.6  
     1.7 +lemma Suc_funpow[simp]: "Suc ^^ n = (op + n)"
     1.8 +  by (induct n) simp_all
     1.9 +
    1.10 +lemma id_funpow[simp]: "id ^^ n = id"
    1.11 +  by (induct n) simp_all
    1.12  
    1.13  subsection {* Kleene iteration *}
    1.14