changeset 27270 | 6a353260735e |
parent 27185 | 0407630909ef |
child 27316 | 9e74019041d4 |
--- a/src/HOLCF/Fix.thy Wed Jun 18 23:15:41 2008 +0200 +++ b/src/HOLCF/Fix.thy Thu Jun 19 00:02:08 2008 +0200 @@ -33,7 +33,11 @@ declare iterate.simps [simp del] lemma iterate_Suc2: "iterate (Suc n)\<cdot>F\<cdot>x = iterate n\<cdot>F\<cdot>(F\<cdot>x)" -by (induct_tac n, auto) +by (induct n) simp_all + +lemma iterate_iterate: + "iterate m\<cdot>F\<cdot>(iterate n\<cdot>F\<cdot>x) = iterate (m + n)\<cdot>F\<cdot>x" +by (induct m) simp_all text {* The sequence of function iterations is a chain.