| changeset 54496 | 178922b63b58 |
| parent 54411 | f72e58a5a75f |
| child 54742 | 7a86358a3c0b |
--- 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 *}