equal
deleted
inserted
replaced
1327 "funpow 0 f = id" |
1327 "funpow 0 f = id" |
1328 | "funpow (Suc n) f = f o funpow n f" |
1328 | "funpow (Suc n) f = f o funpow n f" |
1329 |
1329 |
1330 end |
1330 end |
1331 |
1331 |
|
1332 lemma funpow_0 [simp]: "(f ^^ 0) x = x" |
|
1333 by simp |
|
1334 |
1332 lemma funpow_Suc_right: |
1335 lemma funpow_Suc_right: |
1333 "f ^^ Suc n = f ^^ n \<circ> f" |
1336 "f ^^ Suc n = f ^^ n \<circ> f" |
1334 proof (induct n) |
1337 proof (induct n) |
1335 case 0 then show ?case by simp |
1338 case 0 then show ?case by simp |
1336 next |
1339 next |