# HG changeset patch
# User huffman
# Date 1213826528 -7200
# Node ID 6a353260735eec5efe7938dc816abd755e7e9d36
# Parent  1e9c05cddc64b6f14909352bc80d30a07e9c3d2f
add lemma iterate_iterate

diff -r 1e9c05cddc64 -r 6a353260735e src/HOLCF/Fix.thy
--- 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.