diff -r c095d3143047 -r dca11678c495 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Mon May 04 17:35:29 2020 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed May 13 12:55:33 2020 +0200
@@ -302,6 +302,10 @@
   "of_real (x ^ n) = (of_real x :: 'a::{real_algebra_1}) ^ n"
   by (induct n) simp_all
 
+lemma of_real_power_int [simp]:
+  "of_real (power_int x n) = power_int (of_real x :: 'a :: {real_div_algebra,division_ring}) n"
+  by (auto simp: power_int_def)
+
 lemma of_real_eq_iff [simp]: "of_real x = of_real y \<longleftrightarrow> x = y"
   by (simp add: of_real_def)
 
@@ -333,6 +337,27 @@
 lemma of_real_neg_numeral [simp]: "of_real (- numeral w) = - numeral w"
   using of_real_of_int_eq [of "- numeral w"] by simp
 
+lemma numeral_power_int_eq_of_real_cancel_iff [simp]:
+  "power_int (numeral x) n = (of_real y :: 'a :: {real_div_algebra, division_ring}) \<longleftrightarrow>
+     power_int (numeral x) n = y"
+proof -
+  have "power_int (numeral x) n = (of_real (power_int (numeral x) n) :: 'a)"
+    by simp
+  also have "\<dots> = of_real y \<longleftrightarrow> power_int (numeral x) n = y"
+    by (subst of_real_eq_iff) auto
+  finally show ?thesis .
+qed
+
+lemma of_real_eq_numeral_power_int_cancel_iff [simp]:
+  "(of_real y :: 'a :: {real_div_algebra, division_ring}) = power_int (numeral x) n \<longleftrightarrow>
+     y = power_int (numeral x) n"
+  by (subst (1 2) eq_commute) simp
+
+lemma of_real_eq_of_real_power_int_cancel_iff [simp]:
+  "power_int (of_real b :: 'a :: {real_div_algebra, division_ring}) w = of_real x \<longleftrightarrow>
+     power_int b w = x"
+  by (metis of_real_power_int of_real_eq_iff)
+
 text \<open>Every real algebra has characteristic zero.\<close>
 instance real_algebra_1 < ring_char_0
 proof
@@ -958,6 +983,10 @@
   for x :: "'a::real_normed_div_algebra"
   by (induct n) (simp_all add: norm_mult)
 
+lemma norm_power_int: "norm (power_int x n) = power_int (norm x) n"
+  for x :: "'a::real_normed_div_algebra"
+  by (cases n rule: int_cases4) (auto simp: norm_power power_int_minus norm_inverse)
+
 lemma power_eq_imp_eq_norm:
   fixes w :: "'a::real_normed_div_algebra"
   assumes eq: "w ^ n = z ^ n" and "n > 0"