src/HOL/Library/Coinductive_List.thy

 
 subsection{* A rather complex proof about iterates -- cf.\ Andy Pitts *}
 
 lemma funpow_lmap:
   fixes f :: "'a \<Rightarrow> 'a"
-  shows "(lmap f ^ n) (LCons b l) = LCons ((f ^ n) b) ((lmap f ^ n) l)"
+  shows "(lmap f o^ n) (LCons b l) = LCons ((f o^ n) b) ((lmap f o^ n) l)"
   by (induct n) simp_all
 
 
 lemma iterates_equality:
   assumes h: "\<And>x. h x = LCons x (lmap f (h x))"
   shows "h = iterates f"
 proof
   fix x
   have "(h x, iterates f x) \<in>
-      {((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u)) | u n. True}"
+      {((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u)) | u n. True}"
   proof -
-    have "(h x, iterates f x) = ((lmap f ^ 0) (h x), (lmap f ^ 0) (iterates f x))"
+    have "(h x, iterates f x) = ((lmap f o^ 0) (h x), (lmap f o^ 0) (iterates f x))"
       by simp
     then show ?thesis by blast
   qed
   then show "h x = iterates f x"
   proof (coinduct rule: llist_equalityI)
     case (Eqllist q)
-    then obtain u n where "q = ((lmap f ^ n) (h u), (lmap f ^ n) (iterates f u))"
+    then obtain u n where "q = ((lmap f o^ n) (h u), (lmap f o^ n) (iterates f u))"
         (is "_ = (?q1, ?q2)")
       by auto
-    also have "?q1 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (h u))"
+    also have "?q1 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (h u))"
     proof -
-      have "?q1 = (lmap f ^ n) (LCons u (lmap f (h u)))"
+      have "?q1 = (lmap f o^ n) (LCons u (lmap f (h u)))"
         by (subst h) rule
-      also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (lmap f (h u)))"
+      also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (lmap f (h u)))"
         by (rule funpow_lmap)
-      also have "(lmap f ^ n) (lmap f (h u)) = (lmap f ^ Suc n) (h u)"
+      also have "(lmap f o^ n) (lmap f (h u)) = (lmap f o^ Suc n) (h u)"
         by (simp add: funpow_swap1)
       finally show ?thesis .
     qed
-    also have "?q2 = LCons ((f ^ n) u) ((lmap f ^ Suc n) (iterates f u))"
+    also have "?q2 = LCons ((f o^ n) u) ((lmap f o^ Suc n) (iterates f u))"
     proof -
-      have "?q2 = (lmap f ^ n) (LCons u (iterates f (f u)))"
+      have "?q2 = (lmap f o^ n) (LCons u (iterates f (f u)))"
         by (subst iterates) rule
-      also have "\<dots> = LCons ((f ^ n) u) ((lmap f ^ n) (iterates f (f u)))"
+      also have "\<dots> = LCons ((f o^ n) u) ((lmap f o^ n) (iterates f (f u)))"
         by (rule funpow_lmap)
-      also have "(lmap f ^ n) (iterates f (f u)) = (lmap f ^ Suc n) (iterates f u)"
+      also have "(lmap f o^ n) (iterates f (f u)) = (lmap f o^ Suc n) (iterates f u)"
         by (simp add: lmap_iterates funpow_swap1)
       finally show ?thesis .
     qed
     finally have ?EqLCons by (auto simp del: funpow.simps)
     then show ?case ..