src/HOL/Power.thy

   by (induct m) (simp_all add: algebra_simps)
 
 lemma power_mult: "a ^ (m * n) = (a ^ m) ^ n"
   by (induct n) (simp_all add: power_add)
 
-lemma power2_eq_square: "a\<^sup>2 = a * a"
-  by (simp add: numeral_2_eq_2)
-
-lemma power3_eq_cube: "a ^ 3 = a * a * a"
-  by (simp add: numeral_3_eq_3 mult.assoc)
-
 lemma power_even_eq: "a ^ (2 * n) = (a ^ n)\<^sup>2"
   by (subst mult.commute) (simp add: power_mult)
 
 lemma power_odd_eq: "a ^ Suc (2*n) = a * (a ^ n)\<^sup>2"
   by (simp add: power_even_eq)

   by (simp only: numeral_Bit0 power_add Let_def)
 
 lemma power_numeral_odd: "z ^ numeral (Num.Bit1 w) = (let w = z ^ (numeral w) in z * w * w)"
   by (simp only: numeral_Bit1 One_nat_def add_Suc_right add_0_right
       power_Suc power_add Let_def mult.assoc)
+
+lemma power2_eq_square: "a\<^sup>2 = a * a"
+  by (simp add: numeral_2_eq_2)
+
+lemma power3_eq_cube: "a ^ 3 = a * a * a"
+  by (simp add: numeral_3_eq_3 mult.assoc)
+
+lemma power4_eq_xxxx: "x^4 = x * x * x * x"
+  by (simp add: mult.assoc power_numeral_even)
 
 lemma funpow_times_power: "(times x ^^ f x) = times (x ^ f x)"
 proof (induct "f x" arbitrary: f)
   case 0
   then show ?case by (simp add: fun_eq_iff)