# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1589367333 -7200
# Node ID dca11678c49527f3bfdd294e73d505aa30cec469
# Parent  c095d31430478ab058509b99e08f720e50085eef
new constant power_int in HOL

diff -r c095d3143047 -r dca11678c495 NEWS
--- a/NEWS	Mon May 04 17:35:29 2020 +0200
+++ b/NEWS	Wed May 13 12:55:33 2020 +0200
@@ -35,6 +35,9 @@
 
 *** HOL ***
 
+* New constant "power_int" for exponentiation with integer exponent,
+written as "x powi n".
+
 * Added the "at most 1" quantifier, Uniq.
 
 * For the natural numbers, Sup{} = 0.
diff -r c095d3143047 -r dca11678c495 src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Mon May 04 17:35:29 2020 +0200
+++ b/src/HOL/Deriv.thy	Wed May 13 12:55:33 2020 +0200
@@ -542,6 +542,30 @@
   using has_derivative_mult[OF f has_derivative_inverse[OF x g]]
   by (simp add: field_simps)
 
+lemma has_derivative_power_int':
+  fixes x :: "'a::real_normed_field"
+  assumes x: "x \<noteq> 0"
+  shows "((\<lambda>x. power_int x n) has_derivative (\<lambda>y. y * (of_int n * power_int x (n - 1)))) (at x within S)"
+proof (cases n rule: int_cases4)
+  case (nonneg n)
+  thus ?thesis using x
+    by (cases "n = 0") (auto intro!: derivative_eq_intros simp: field_simps power_int_diff fun_eq_iff
+                             simp flip: power_Suc)
+next
+  case (neg n)
+  thus ?thesis using x
+    by (auto intro!: derivative_eq_intros simp: field_simps power_int_diff power_int_minus
+             simp flip: power_Suc power_Suc2 power_add)
+qed
+
+lemma has_derivative_power_int[simp, derivative_intros]:
+  fixes f :: "_ \<Rightarrow> 'a::real_normed_field"
+  assumes x:  "f x \<noteq> 0"
+    and f: "(f has_derivative f') (at x within S)"
+  shows "((\<lambda>x. power_int (f x) n) has_derivative (\<lambda>h. f' h * (of_int n * power_int (f x) (n - 1))))
+           (at x within S)"
+  using has_derivative_compose[OF f has_derivative_power_int', OF x] .
+
 
 text \<open>Conventional form requires mult-AC laws. Types real and complex only.\<close>
 
@@ -695,6 +719,12 @@
   shows "f differentiable (at x within s) \<Longrightarrow> (\<lambda>x. f x ^ n) differentiable (at x within s)"
   unfolding differentiable_def by (blast intro: has_derivative_power)
 
+lemma differentiable_power_int [simp, derivative_intros]:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_field"
+  shows "f differentiable (at x within s) \<Longrightarrow> f x \<noteq> 0 \<Longrightarrow>
+           (\<lambda>x. power_int (f x) n) differentiable (at x within s)"
+  unfolding differentiable_def by (blast intro: has_derivative_power_int)
+
 lemma differentiable_scaleR [simp, derivative_intros]:
   "f differentiable (at x within s) \<Longrightarrow> g differentiable (at x within s) \<Longrightarrow>
     (\<lambda>x. f x *\<^sub>R g x) differentiable (at x within s)"
@@ -1040,6 +1070,23 @@
 lemma DERIV_pow: "((\<lambda>x. x ^ n) has_field_derivative real n * (x ^ (n - Suc 0))) (at x within s)"
   using DERIV_power [OF DERIV_ident] by simp
 
+lemma DERIV_power_int [derivative_intros]:
+  assumes [derivative_intros]: "(f has_field_derivative d) (at x within s)" and [simp]: "f x \<noteq> 0"
+  shows   "((\<lambda>x. power_int (f x) n) has_field_derivative
+             (of_int n * power_int (f x) (n - 1) * d)) (at x within s)"
+proof (cases n rule: int_cases4)
+  case (nonneg n)
+  thus ?thesis 
+    by (cases "n = 0")
+       (auto intro!: derivative_eq_intros simp: field_simps power_int_diff
+             simp flip: power_Suc power_Suc2 power_add)
+next
+  case (neg n)
+  thus ?thesis
+    by (auto intro!: derivative_eq_intros simp: field_simps power_int_diff power_int_minus
+             simp flip: power_Suc power_Suc2 power_add)
+qed
+
 lemma DERIV_chain': "(f has_field_derivative D) (at x within s) \<Longrightarrow> DERIV g (f x) :> E \<Longrightarrow>
   ((\<lambda>x. g (f x)) has_field_derivative E * D) (at x within s)"
   using has_derivative_compose[of f "(*) D" x s g "(*) E"]
diff -r c095d3143047 -r dca11678c495 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon May 04 17:35:29 2020 +0200
+++ b/src/HOL/Int.thy	Wed May 13 12:55:33 2020 +0200
@@ -1694,6 +1694,344 @@
 qed
 
 
+subsection \<open>Powers with integer exponents\<close>
+
+text \<open>
+  The following allows writing powers with an integer exponent. While the type signature
+  is very generic, most theorems will assume that the underlying type is a division ring or
+  a field.
+
+  The notation `powi' is inspired by the `powr' notation for real/complex exponentiation.
+\<close>
+definition power_int :: "'a :: {inverse, power} \<Rightarrow> int \<Rightarrow> 'a" (infixr "powi" 80) where
+  "power_int x n = (if n \<ge> 0 then x ^ nat n else inverse x ^ (nat (-n)))"
+
+lemma power_int_0_right [simp]: "power_int x 0 = 1"
+  and power_int_1_right [simp]:
+        "power_int (y :: 'a :: {power, inverse, monoid_mult}) 1 = y"
+  and power_int_minus1_right [simp]:
+        "power_int (y :: 'a :: {power, inverse, monoid_mult}) (-1) = inverse y"
+  by (simp_all add: power_int_def)
+
+lemma power_int_of_nat [simp]: "power_int x (int n) = x ^ n"
+  by (simp add: power_int_def)
+
+lemma power_int_numeral [simp]: "power_int x (numeral n) = x ^ numeral n"
+  by (simp add: power_int_def)
+
+lemma int_cases4 [case_names nonneg neg]:
+  fixes m :: int
+  obtains n where "m = int n" | n where "n > 0" "m = -int n"
+proof (cases "m \<ge> 0")
+  case True
+  thus ?thesis using that(1)[of "nat m"] by auto
+next
+  case False
+  thus ?thesis using that(2)[of "nat (-m)"] by auto
+qed
+
+
+context
+  assumes "SORT_CONSTRAINT('a::division_ring)"
+begin
+
+lemma power_int_minus: "power_int (x::'a) (-n) = inverse (power_int x n)"
+  by (auto simp: power_int_def power_inverse)
+
+lemma power_int_eq_0_iff [simp]: "power_int (x::'a) n = 0 \<longleftrightarrow> x = 0 \<and> n \<noteq> 0"
+  by (auto simp: power_int_def)
+
+lemma power_int_0_left_If: "power_int (0 :: 'a) m = (if m = 0 then 1 else 0)"
+  by (auto simp: power_int_def)
+
+lemma power_int_0_left [simp]: "m \<noteq> 0 \<Longrightarrow> power_int (0 :: 'a) m = 0"
+  by (simp add: power_int_0_left_If)
+
+lemma power_int_1_left [simp]: "power_int 1 n = (1 :: 'a :: division_ring)"
+  by (auto simp: power_int_def) 
+
+lemma power_diff_conv_inverse: "x \<noteq> 0 \<Longrightarrow> m \<le> n \<Longrightarrow> (x :: 'a) ^ (n - m) = x ^ n * inverse x ^ m"
+  by (simp add: field_simps flip: power_add)
+
+lemma power_mult_inverse_distrib: "x ^ m * inverse (x :: 'a) = inverse x * x ^ m"
+proof (cases "x = 0")
+  case [simp]: False
+  show ?thesis
+  proof (cases m)
+    case (Suc m')
+    have "x ^ Suc m' * inverse x = x ^ m'"
+      by (subst power_Suc2) (auto simp: mult.assoc)
+    also have "\<dots> = inverse x * x ^ Suc m'"
+      by (subst power_Suc) (auto simp: mult.assoc [symmetric])
+    finally show ?thesis using Suc by simp
+  qed auto
+qed auto
+
+lemma power_mult_power_inverse_commute:
+  "x ^ m * inverse (x :: 'a) ^ n = inverse x ^ n * x ^ m"
+proof (induction n)
+  case (Suc n)
+  have "x ^ m * inverse x ^ Suc n = (x ^ m * inverse x ^ n) * inverse x"
+    by (simp only: power_Suc2 mult.assoc)
+  also have "x ^ m * inverse x ^ n = inverse x ^ n * x ^ m"
+    by (rule Suc)
+  also have "\<dots> * inverse x = (inverse x ^ n * inverse x) * x ^ m"
+    by (simp add: mult.assoc power_mult_inverse_distrib)
+  also have "\<dots> = inverse x ^ (Suc n) * x ^ m"
+    by (simp only: power_Suc2)
+  finally show ?case .
+qed auto
+
+lemma power_int_add:
+  assumes "x \<noteq> 0 \<or> m + n \<noteq> 0"
+  shows   "power_int (x::'a) (m + n) = power_int x m * power_int x n"
+proof (cases "x = 0")
+  case True
+  thus ?thesis using assms by (auto simp: power_int_0_left_If)
+next
+  case [simp]: False
+  show ?thesis
+  proof (cases m n rule: int_cases4[case_product int_cases4])
+    case (nonneg_nonneg a b)
+    thus ?thesis
+      by (auto simp: power_int_def nat_add_distrib power_add)
+  next
+    case (nonneg_neg a b)
+    thus ?thesis
+      by (auto simp: power_int_def nat_diff_distrib not_le power_diff_conv_inverse
+                     power_mult_power_inverse_commute)
+  next
+    case (neg_nonneg a b)
+    thus ?thesis
+      by (auto simp: power_int_def nat_diff_distrib not_le power_diff_conv_inverse
+                     power_mult_power_inverse_commute)    
+  next
+    case (neg_neg a b)
+    thus ?thesis
+      by (auto simp: power_int_def nat_add_distrib add.commute simp flip: power_add)
+  qed
+qed
+
+lemma power_int_add_1:
+  assumes "x \<noteq> 0 \<or> m \<noteq> -1"
+  shows   "power_int (x::'a) (m + 1) = power_int x m * x"
+  using assms by (subst power_int_add) auto
+
+lemma power_int_add_1':
+  assumes "x \<noteq> 0 \<or> m \<noteq> -1"
+  shows   "power_int (x::'a) (m + 1) = x * power_int x m"
+  using assms by (subst add.commute, subst power_int_add) auto
+
+lemma power_int_commutes: "power_int (x :: 'a) n * x = x * power_int x n"
+  by (cases "x = 0") (auto simp flip: power_int_add_1 power_int_add_1')
+
+lemma power_int_inverse [field_simps, field_split_simps, divide_simps]:
+  "power_int (inverse (x :: 'a)) n = inverse (power_int x n)"
+  by (auto simp: power_int_def power_inverse)
+
+lemma power_int_mult: "power_int (x :: 'a) (m * n) = power_int (power_int x m) n"
+  by (auto simp: power_int_def zero_le_mult_iff simp flip: power_mult power_inverse nat_mult_distrib)
+
+end
+
+context
+  assumes "SORT_CONSTRAINT('a::field)"
+begin
+
+lemma power_int_diff:
+  assumes "x \<noteq> 0 \<or> m \<noteq> n"
+  shows   "power_int (x::'a) (m - n) = power_int x m / power_int x n"
+  using power_int_add[of x m "-n"] assms by (auto simp: field_simps power_int_minus)
+
+lemma power_int_minus_mult: "x \<noteq> 0 \<or> n \<noteq> 0 \<Longrightarrow> power_int (x :: 'a) (n - 1) * x = power_int x n"
+  by (auto simp flip: power_int_add_1)  
+
+lemma power_int_mult_distrib: "power_int (x * y :: 'a) m = power_int x m * power_int y m"
+  by (auto simp: power_int_def power_mult_distrib)
+
+lemmas power_int_mult_distrib_numeral1 = power_int_mult_distrib [where x = "numeral w" for w, simp]
+lemmas power_int_mult_distrib_numeral2 = power_int_mult_distrib [where y = "numeral w" for w, simp]
+
+lemma power_int_divide_distrib: "power_int (x / y :: 'a) m = power_int x m / power_int y m"
+  using power_int_mult_distrib[of x "inverse y" m] unfolding power_int_inverse
+  by (simp add: field_simps)
+
+end
+
+
+lemma power_int_add_numeral [simp]:
+  "power_int x (numeral m) * power_int x (numeral n) = power_int x (numeral (m + n))"
+  for x :: "'a :: division_ring"
+  by (simp add: power_int_add [symmetric])
+
+lemma power_int_add_numeral2 [simp]:
+  "power_int x (numeral m) * (power_int x (numeral n) * b) = power_int x (numeral (m + n)) * b"
+  for x :: "'a :: division_ring"
+  by (simp add: mult.assoc [symmetric])
+
+lemma power_int_mult_numeral [simp]:
+  "power_int (power_int x (numeral m)) (numeral n) = power_int x (numeral (m * n))"
+  for x :: "'a :: division_ring"
+  by (simp only: numeral_mult power_int_mult)
+  
+lemma power_int_not_zero: "(x :: 'a :: division_ring) \<noteq> 0 \<or> n = 0 \<Longrightarrow> power_int x n \<noteq> 0"
+  by (subst power_int_eq_0_iff) auto
+
+lemma power_int_one_over [field_simps, field_split_simps, divide_simps]:
+  "power_int (1 / x :: 'a :: division_ring) n = 1 / power_int x n"
+  using power_int_inverse[of x] by (simp add: divide_inverse)
+
+
+context
+  assumes "SORT_CONSTRAINT('a :: linordered_field)"
+begin
+
+lemma power_int_numeral_neg_numeral [simp]:
+  "power_int (numeral m) (-numeral n) = (inverse (numeral (Num.pow m n)) :: 'a)"
+  by (simp add: power_int_minus)
+
+lemma zero_less_power_int [simp]: "0 < (x :: 'a) \<Longrightarrow> 0 < power_int x n"
+  by (auto simp: power_int_def)
+
+lemma zero_le_power_int [simp]: "0 \<le> (x :: 'a) \<Longrightarrow> 0 \<le> power_int x n"
+  by (auto simp: power_int_def)
+
+lemma power_int_mono: "(x :: 'a) \<le> y \<Longrightarrow> n \<ge> 0 \<Longrightarrow> 0 \<le> x \<Longrightarrow> power_int x n \<le> power_int y n"
+  by (cases n rule: int_cases4) (auto intro: power_mono)
+
+lemma one_le_power_int [simp]: "1 \<le> (x :: 'a) \<Longrightarrow> n \<ge> 0 \<Longrightarrow> 1 \<le> power_int x n"
+  using power_int_mono [of 1 x n] by simp
+
+lemma power_int_le_one: "0 \<le> (x :: 'a) \<Longrightarrow> n \<ge> 0 \<Longrightarrow> x \<le> 1 \<Longrightarrow> power_int x n \<le> 1"
+  using power_int_mono [of x 1 n] by simp
+
+lemma power_int_le_imp_le_exp:
+  assumes gt1: "1 < (x :: 'a :: linordered_field)"
+  assumes "power_int x m \<le> power_int x n" "n \<ge> 0"
+  shows   "m \<le> n"
+proof (cases "m < 0")
+  case True
+  with \<open>n \<ge> 0\<close> show ?thesis by simp
+next
+  case False
+  with assms have "x ^ nat m \<le> x ^ nat n"
+    by (simp add: power_int_def)
+  from gt1 and this show ?thesis
+    using False \<open>n \<ge> 0\<close> by auto
+qed
+
+lemma power_int_le_imp_less_exp:
+  assumes gt1: "1 < (x :: 'a :: linordered_field)"
+  assumes "power_int x m < power_int x n" "n \<ge> 0"
+  shows   "m < n"
+proof (cases "m < 0")
+  case True
+  with \<open>n \<ge> 0\<close> show ?thesis by simp
+next
+  case False
+  with assms have "x ^ nat m < x ^ nat n"
+    by (simp add: power_int_def)
+  from gt1 and this show ?thesis
+    using False \<open>n \<ge> 0\<close> by auto
+qed
+
+lemma power_int_strict_mono:
+  "(a :: 'a :: linordered_field) < b \<Longrightarrow> 0 \<le> a \<Longrightarrow> 0 < n \<Longrightarrow> power_int a n < power_int b n"
+  by (auto simp: power_int_def intro!: power_strict_mono)
+
+lemma power_int_mono_iff [simp]:
+  fixes a b :: "'a :: linordered_field"
+  shows "\<lbrakk>a \<ge> 0; b \<ge> 0; n > 0\<rbrakk> \<Longrightarrow> power_int a n \<le> power_int b n \<longleftrightarrow> a \<le> b"
+  by (auto simp: power_int_def intro!: power_strict_mono)
+
+lemma power_int_strict_increasing:
+  fixes a :: "'a :: linordered_field"
+  assumes "n < N" "1 < a"
+  shows   "power_int a N > power_int a n"
+proof -
+  have *: "a ^ nat (N - n) > a ^ 0"
+    using assms by (intro power_strict_increasing) auto
+  have "power_int a N = power_int a n * power_int a (N - n)"
+    using assms by (simp flip: power_int_add)
+  also have "\<dots> > power_int a n * 1"
+    using assms *
+    by (intro mult_strict_left_mono zero_less_power_int) (auto simp: power_int_def)
+  finally show ?thesis by simp
+qed
+
+lemma power_int_increasing:
+  fixes a :: "'a :: linordered_field"
+  assumes "n \<le> N" "a \<ge> 1"
+  shows   "power_int a N \<ge> power_int a n"
+proof -
+  have *: "a ^ nat (N - n) \<ge> a ^ 0"
+    using assms by (intro power_increasing) auto
+  have "power_int a N = power_int a n * power_int a (N - n)"
+    using assms by (simp flip: power_int_add)
+  also have "\<dots> \<ge> power_int a n * 1"
+    using assms * by (intro mult_left_mono) (auto simp: power_int_def)
+  finally show ?thesis by simp
+qed
+
+lemma power_int_strict_decreasing:
+  fixes a :: "'a :: linordered_field"
+  assumes "n < N" "0 < a" "a < 1"
+  shows   "power_int a N < power_int a n"
+proof -
+  have *: "a ^ nat (N - n) < a ^ 0"
+    using assms by (intro power_strict_decreasing) auto
+  have "power_int a N = power_int a n * power_int a (N - n)"
+    using assms by (simp flip: power_int_add)
+  also have "\<dots> < power_int a n * 1"
+    using assms *
+    by (intro mult_strict_left_mono zero_less_power_int) (auto simp: power_int_def)
+  finally show ?thesis by simp
+qed
+
+lemma power_int_decreasing:
+  fixes a :: "'a :: linordered_field"
+  assumes "n \<le> N" "0 \<le> a" "a \<le> 1" "a \<noteq> 0 \<or> N \<noteq> 0 \<or> n = 0"
+  shows   "power_int a N \<le> power_int a n"
+proof (cases "a = 0")
+  case False
+  have *: "a ^ nat (N - n) \<le> a ^ 0"
+    using assms by (intro power_decreasing) auto
+  have "power_int a N = power_int a n * power_int a (N - n)"
+    using assms False by (simp flip: power_int_add)
+  also have "\<dots> \<le> power_int a n * 1"
+    using assms * by (intro mult_left_mono) (auto simp: power_int_def)
+  finally show ?thesis by simp
+qed (use assms in \<open>auto simp: power_int_0_left_If\<close>)
+
+lemma one_less_power_int: "1 < (a :: 'a) \<Longrightarrow> 0 < n \<Longrightarrow> 1 < power_int a n"
+  using power_int_strict_increasing[of 0 n a] by simp
+
+lemma power_int_abs: "\<bar>power_int a n :: 'a\<bar> = power_int \<bar>a\<bar> n"
+  by (auto simp: power_int_def power_abs)
+
+lemma power_int_sgn [simp]: "sgn (power_int a n :: 'a) = power_int (sgn a) n"
+  by (auto simp: power_int_def)
+
+lemma abs_power_int_minus [simp]: "\<bar>power_int (- a) n :: 'a\<bar> = \<bar>power_int a n\<bar>"
+  by (simp add: power_int_abs)
+
+lemma power_int_strict_antimono:
+  assumes "(a :: 'a :: linordered_field) < b" "0 < a" "n < 0"
+  shows   "power_int a n > power_int b n"
+proof -
+  have "inverse (power_int a (-n)) > inverse (power_int b (-n))"
+    using assms by (intro less_imp_inverse_less power_int_strict_mono zero_less_power_int) auto
+  thus ?thesis by (simp add: power_int_minus)
+qed
+
+lemma power_int_antimono:
+  assumes "(a :: 'a :: linordered_field) \<le> b" "0 < a" "n < 0"
+  shows   "power_int a n \<ge> power_int b n"
+  using power_int_strict_antimono[of a b n] assms by (cases "a = b") auto
+
+end
+
+
 subsection \<open>Finiteness of intervals\<close>
 
 lemma finite_interval_int1 [iff]: "finite {i :: int. a \<le> i \<and> i \<le> b}"
diff -r c095d3143047 -r dca11678c495 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Mon May 04 17:35:29 2020 +0200
+++ b/src/HOL/Limits.thy	Wed May 13 12:55:33 2020 +0200
@@ -1227,6 +1227,33 @@
   shows "continuous_on s (\<lambda>x. (f x) / (g x))"
   using assms unfolding continuous_on_def by (blast intro: tendsto_divide)
 
+lemma tendsto_power_int [tendsto_intros]:
+  fixes a :: "'a::real_normed_div_algebra"
+  assumes f: "(f \<longlongrightarrow> a) F"
+    and a: "a \<noteq> 0"
+  shows "((\<lambda>x. power_int (f x) n) \<longlongrightarrow> power_int a n) F"
+  using assms by (cases n rule: int_cases4) (auto intro!: tendsto_intros simp: power_int_minus)
+
+lemma continuous_power_int:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
+  assumes "continuous F f"
+    and "f (Lim F (\<lambda>x. x)) \<noteq> 0"
+  shows "continuous F (\<lambda>x. power_int (f x) n)"
+  using assms unfolding continuous_def by (rule tendsto_power_int)
+
+lemma continuous_at_within_power_int[continuous_intros]:
+  fixes f :: "'a::t2_space \<Rightarrow> 'b::real_normed_div_algebra"
+  assumes "continuous (at a within s) f"
+    and "f a \<noteq> 0"
+  shows "continuous (at a within s) (\<lambda>x. power_int (f x) n)"
+  using assms unfolding continuous_within by (rule tendsto_power_int)
+
+lemma continuous_on_power_int [continuous_intros]:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::real_normed_div_algebra"
+  assumes "continuous_on s f" and "\<forall>x\<in>s. f x \<noteq> 0"
+  shows "continuous_on s (\<lambda>x. power_int (f x) n)"
+  using assms unfolding continuous_on_def by (blast intro: tendsto_power_int)
+
 lemma tendsto_sgn [tendsto_intros]: "(f \<longlongrightarrow> l) F \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> ((\<lambda>x. sgn (f x)) \<longlongrightarrow> sgn l) F"
   for l :: "'a::real_normed_vector"
   unfolding sgn_div_norm by (simp add: tendsto_intros)
diff -r c095d3143047 -r dca11678c495 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Mon May 04 17:35:29 2020 +0200
+++ b/src/HOL/Parity.thy	Wed May 13 12:55:33 2020 +0200
@@ -674,6 +674,40 @@
     using mod_mult2_eq' [of \<open>- a\<close> \<open>nat (- b)\<close> \<open>nat c\<close>] by simp
 qed
 
+context
+  assumes "SORT_CONSTRAINT('a::division_ring)"
+begin
+
+lemma power_int_minus_left:
+  "power_int (-a :: 'a) n = (if even n then power_int a n else -power_int a n)"
+  by (auto simp: power_int_def minus_one_power_iff even_nat_iff)
+
+lemma power_int_minus_left_even [simp]: "even n \<Longrightarrow> power_int (-a :: 'a) n = power_int a n"
+  by (simp add: power_int_minus_left)
+
+lemma power_int_minus_left_odd [simp]: "odd n \<Longrightarrow> power_int (-a :: 'a) n = -power_int a n"
+  by (simp add: power_int_minus_left)
+
+lemma power_int_minus_left_distrib:
+  "NO_MATCH (-1) x \<Longrightarrow> power_int (-a :: 'a) n = power_int (-1) n * power_int a n"
+  by (simp add: power_int_minus_left)
+
+lemma power_int_minus_one_minus: "power_int (-1 :: 'a) (-n) = power_int (-1) n"
+  by (simp add: power_int_minus_left)
+
+lemma power_int_minus_one_diff_commute: "power_int (-1 :: 'a) (a - b) = power_int (-1) (b - a)"
+  by (subst power_int_minus_one_minus [symmetric]) auto
+
+lemma power_int_minus_one_mult_self [simp]:
+  "power_int (-1 :: 'a) m * power_int (-1) m = 1"
+  by (simp add: power_int_minus_left)
+
+lemma power_int_minus_one_mult_self' [simp]:
+  "power_int (-1 :: 'a) m * (power_int (-1) m * b) = b"
+  by (simp add: power_int_minus_left)
+
+end
+
 
 subsection \<open>Abstract bit structures\<close>
 
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"
diff -r c095d3143047 -r dca11678c495 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon May 04 17:35:29 2020 +0200
+++ b/src/HOL/Transcendental.thy	Wed May 13 12:55:33 2020 +0200
@@ -2499,7 +2499,25 @@
   by (simp add: linorder_not_less [symmetric])
 
 lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
-by (induction n) (simp_all add: ac_simps powr_add)
+  by (induction n) (simp_all add: ac_simps powr_add)
+
+lemma powr_real_of_int':
+  assumes "x \<ge> 0" "x \<noteq> 0 \<or> n > 0"
+  shows   "x powr real_of_int n = power_int x n"
+proof (cases "x = 0")
+  case False
+  with assms have "x > 0" by simp
+  show ?thesis
+  proof (cases n rule: int_cases4)
+    case (nonneg n)
+    thus ?thesis using \<open>x > 0\<close>
+      by (auto simp add: powr_realpow)
+  next
+    case (neg n)
+    thus ?thesis using \<open>x > 0\<close>
+      by (auto simp add: powr_realpow powr_minus power_int_minus)
+  qed
+qed (use assms in auto)
 
 lemma log_ln: "ln x = log (exp(1)) x"
   by (simp add: log_def)