alternative simplification of ^^ to the righthand side;
lifting of comp_fun_commute to ^^

--- a/src/HOL/Finite_Set.thy	Fri Oct 05 18:01:48 2012 +0200
+++ b/src/HOL/Finite_Set.thy	Sat Oct 06 11:08:52 2012 +0200
@@ -739,7 +739,7 @@
 end
 
 
-subsubsection {* Expressing set operations via @{const fold} *}
+subsubsection {* Liftings to @{text comp_fun_commute} etc. *}
 
 lemma (in comp_fun_commute) comp_comp_fun_commute:
   "comp_fun_commute (f \<circ> g)"
@@ -751,6 +751,47 @@
   by (rule comp_fun_idem.intro, rule comp_comp_fun_commute, unfold_locales)
     (simp_all add: comp_fun_idem)
 
+lemma (in comp_fun_commute) comp_fun_commute_funpow:
+  "comp_fun_commute (\<lambda>x. f x ^^ g x)"
+proof
+  fix y x
+  show "f y ^^ g y \<circ> f x ^^ g x = f x ^^ g x \<circ> f y ^^ g y"
+  proof (cases "x = y")
+    case True then show ?thesis by simp
+  next
+    case False show ?thesis
+    proof (induct "g x" arbitrary: g)
+      case 0 then show ?case by simp
+    next
+      case (Suc n g)
+      have hyp1: "f y ^^ g y \<circ> f x = f x \<circ> f y ^^ g y"
+      proof (induct "g y" arbitrary: g)
+        case 0 then show ?case by simp
+      next
+        case (Suc n g)
+        def h \<equiv> "\<lambda>z. g z - 1"
+        with Suc have "n = h y" by simp
+        with Suc have hyp: "f y ^^ h y \<circ> f x = f x \<circ> f y ^^ h y"
+          by auto
+        from Suc h_def have "g y = Suc (h y)" by simp
+        then show ?case by (simp add: o_assoc [symmetric] hyp)
+          (simp add: o_assoc comp_fun_commute)
+      qed
+      def h \<equiv> "\<lambda>z. if z = x then g x - 1 else g z"
+      with Suc have "n = h x" by simp
+      with Suc have "f y ^^ h y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ h y"
+        by auto
+      with False h_def have hyp2: "f y ^^ g y \<circ> f x ^^ h x = f x ^^ h x \<circ> f y ^^ g y" by simp
+      from Suc h_def have "g x = Suc (h x)" by simp
+      then show ?case by (simp del: funpow.simps add: funpow_Suc_right o_assoc hyp2)
+        (simp add: o_assoc [symmetric] hyp1)
+    qed
+  qed
+qed
+
+
+subsubsection {* Expressing set operations via @{const fold} *}
+
 lemma comp_fun_idem_insert:
   "comp_fun_idem insert"
 proof
@@ -2400,3 +2441,4 @@
 hide_const (open) Finite_Set.fold Finite_Set.filter
 
 end
+

--- a/src/HOL/Nat.thy	Fri Oct 05 18:01:48 2012 +0200
+++ b/src/HOL/Nat.thy	Sat Oct 06 11:08:52 2012 +0200
@@ -1249,6 +1249,19 @@
 
 end
 
+lemma funpow_Suc_right:
+  "f ^^ Suc n = f ^^ n \<circ> f"
+proof (induct n)
+  case 0 then show ?case by simp
+next
+  fix n
+  assume "f ^^ Suc n = f ^^ n \<circ> f"
+  then show "f ^^ Suc (Suc n) = f ^^ Suc n \<circ> f"
+    by (simp add: o_assoc)
+qed
+
+lemmas funpow_simps_right = funpow.simps(1) funpow_Suc_right
+
 text {* for code generation *}
 
 definition funpow :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" where