--- a/src/HOL/Power.thy Wed Sep 18 14:41:37 2019 +0100
+++ b/src/HOL/Power.thy Thu Sep 19 12:36:15 2019 +0100
@@ -54,12 +54,6 @@
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)
@@ -73,6 +67,15 @@
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