src/HOL/Power.thy
changeset 58656 7f14d5d9b933
parent 58437 8d124c73c37a
child 58787 af9eb5e566dd
     1.1 --- a/src/HOL/Power.thy	Mon Oct 13 16:07:11 2014 +0200
     1.2 +++ b/src/HOL/Power.thy	Mon Oct 13 18:55:05 2014 +0200
     1.3 @@ -103,6 +103,19 @@
     1.4    ultimately show ?case by (simp add: power_add funpow_add fun_eq_iff mult.assoc)
     1.5  qed
     1.6  
     1.7 +lemma power_commuting_commutes:
     1.8 +  assumes "x * y = y * x"
     1.9 +  shows "x ^ n * y = y * x ^n"
    1.10 +proof (induct n)
    1.11 +  case (Suc n)
    1.12 +  have "x ^ Suc n * y = x ^ n * y * x"
    1.13 +    by (subst power_Suc2) (simp add: assms ac_simps)
    1.14 +  also have "\<dots> = y * x ^ Suc n"
    1.15 +    unfolding Suc power_Suc2
    1.16 +    by (simp add: ac_simps)
    1.17 +  finally show ?case .
    1.18 +qed simp
    1.19 +
    1.20  end
    1.21  
    1.22  context comm_monoid_mult