# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1493218415 -3600
# Node ID 8d53b3bebab4a5061c2db33fb2b154522c280e0b
# Parent  66351f79c295db0335a26311c696e212119cd0cd
Further new material. The simprule status of some exp and ln identities was reverted.

diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -1046,6 +1046,9 @@
   apply auto
   done
 
+lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln x = 0 \<longleftrightarrow> x = 1"
+  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
+
 subsection\<open>Relation to Real Logarithm\<close>
 
 lemma Ln_of_real:
@@ -1679,23 +1682,19 @@
   fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
   by (simp add: exp_of_nat_mult powr_def)
 
-lemma powr_add_complex:
-  fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
-  by (simp add: powr_def algebra_simps exp_add)
-
-lemma powr_minus_complex:
-  fixes w::complex shows  "w powr (-z) = inverse(w powr z)"
-  by (simp add: powr_def exp_minus)
-
-lemma powr_diff_complex:
-  fixes w::complex shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
-  by (simp add: powr_def algebra_simps exp_diff)
-
 lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
   apply (simp add: powr_def)
   using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
   by auto
 
+lemma powr_complexpow [simp]:
+  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
+  by (induct n) (auto simp: ac_simps powr_add)
+
+lemma powr_complexnumeral [simp]:
+  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (numeral n) = x ^ (numeral n)"
+  by (metis of_nat_numeral powr_complexpow)
+
 lemma cnj_powr:
   assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
   shows   "cnj (a powr b) = cnj a powr cnj b"
@@ -1759,16 +1758,15 @@
   apply (intro derivative_eq_intros | simp)+
   done
 
-lemma field_differentiable_powr_right:
+lemma field_differentiable_powr_right [derivative_intros]:
   fixes w::complex
-  shows
-    "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
+  shows "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
 using field_differentiable_def has_field_derivative_powr_right by blast
 
-lemma holomorphic_on_powr_right:
+lemma holomorphic_on_powr_right [holomorphic_intros]:
     "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
-    unfolding holomorphic_on_def field_differentiable_def
-by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
+  unfolding holomorphic_on_def field_differentiable_def
+  by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
 
 lemma norm_powr_real_powr:
   "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
@@ -2562,6 +2560,9 @@
   using arctan_bounds[of "1/5"   4]
         arctan_bounds[of "1/239" 4]
   by (simp_all add: eval_nat_numeral)
+    
+corollary pi_gt3: "pi > 3"
+  using pi_approx by simp
 
 
 subsection\<open>Inverse Sine\<close>
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -258,6 +258,14 @@
     unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
 qed
 
+lemma convex_halfspace_abs_le: "convex {x. \<bar>inner a x\<bar> \<le> b}"
+proof -
+  have *: "{x. \<bar>inner a x\<bar> \<le> b} = {x. inner a x \<le> b} \<inter> {x. -b \<le> inner a x}"
+    by auto
+  show ?thesis
+    unfolding * by (simp add: convex_Int convex_halfspace_ge convex_halfspace_le)
+qed
+
 lemma convex_hyperplane: "convex {x. inner a x = b}"
 proof -
   have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}"
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Analysis/Generalised_Binomial_Theorem.thy
--- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -129,12 +129,12 @@
       by (auto intro!: derivative_eq_intros)
     also from z have "a * f z = (1 + z) * f' z" by (rule deriv)
     finally show "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative 0) (at z within ball 0 K)"
-      using nz by (simp add: field_simps powr_diff_complex at_within_open[OF z'])
+      using nz by (simp add: field_simps powr_diff at_within_open[OF z'])
   qed simp_all
   then obtain c where c: "\<And>z. z \<in> ball 0 K \<Longrightarrow> f z * (1 + z) powr (-a) = c" by blast
   from c[of 0] and K have "c = 1" by simp
   with c[of z] have "f z = (1 + z) powr a" using K
-    by (simp add: powr_minus_complex field_simps dist_complex_def)
+    by (simp add: powr_minus field_simps dist_complex_def)
   with summable K show ?thesis unfolding f_f'_def by (simp add: sums_iff)
 qed
 
@@ -158,7 +158,7 @@
       by (subst powr_times_real[symmetric]) (simp_all add: field_simps)
     also from xy have "complex_of_real (1 + x / y) * complex_of_real y = of_real (x + y)"
       by (simp add: field_simps)
-    finally have "?P x y" using xy by (simp add: field_simps powr_diff_complex powr_nat)
+    finally have "?P x y" using xy by (simp add: field_simps powr_diff powr_nat)
   } note A = this
 
   show ?thesis
@@ -174,7 +174,7 @@
       fix n :: nat
       from y have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) =
                        (a gchoose n) * (-of_real x / -of_real y) ^ n * (- of_real y) powr a"
-        by (subst power_divide) (simp add: powr_diff_complex powr_nat)
+        by (subst power_divide) (simp add: powr_diff powr_nat)
       also from y have "(- of_real y) powr a = (-1) powr -a * of_real y powr a"
         by (subst powr_neg_real_complex) simp
       also have "-complex_of_real x / -complex_of_real y = complex_of_real x / complex_of_real y"
@@ -182,7 +182,7 @@
       also have "... ^ n = of_real x ^ n / of_real y ^ n" by (simp add: power_divide)
       also have "(a gchoose n) * ... * ((-1) powr -a * of_real y powr a) =
                    (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - n))"
-        by (simp add: algebra_simps powr_diff_complex powr_nat)
+        by (simp add: algebra_simps powr_diff powr_nat)
       finally have "(a gchoose n) * of_real (- x) ^ n * of_real (- y) powr (a - of_nat n) =
                       (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - of_nat n))" .
     }
@@ -229,7 +229,7 @@
   hence "(\<lambda>n. (a gchoose n) * (x / y) ^ n * y powr a) sums ((1 + x / y) powr a * y powr a)"
     by (rule sums_mult2)
   with xy show ?thesis
-    by (simp add: field_simps powr_divide powr_divide2[symmetric] powr_realpow)
+    by (simp add: field_simps powr_divide powr_diff powr_realpow)
 qed
 
 lemma one_plus_neg_powr_powser:
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -407,7 +407,7 @@
     then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
       by (metis exp_less_mono exp_ln that)
     then show ?thesis
-      by (simp add: \<delta>01(1) \<open>0 < k\<close>)
+      by (simp add: \<delta>01(1) \<open>0 < k\<close> exp_of_nat_mult)
   qed
   { fix t and e::real
     assume "e>0"
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Complex.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -95,6 +95,11 @@
   unfolding divide_complex_def times_complex.sel inverse_complex.sel
   by (simp add: divide_simps)
 
+lemma Complex_divide:
+    "(x / y) = Complex ((Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2))
+                       ((Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2))"
+  by (metis Im_divide Re_divide complex_surj)
+
 lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2"
   by (simp add: power2_eq_square)
 
@@ -261,6 +266,20 @@
 lemma divide_numeral_i [simp]: "z / (numeral n * \<i>) = - (\<i> * z) / numeral n"
   by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
 
+lemma imaginary_eq_real_iff [simp]:
+  assumes "y \<in> Reals" "x \<in> Reals"
+  shows "\<i> * y = x \<longleftrightarrow> x=0 \<and> y=0"
+    using assms
+    unfolding Reals_def
+    apply clarify
+      apply (rule iffI)
+    apply (metis Im_complex_of_real Im_i_times Re_complex_of_real mult_eq_0_iff of_real_0)
+    by simp
+
+lemma real_eq_imaginary_iff [simp]:
+  assumes "y \<in> Reals" "x \<in> Reals"
+  shows "x = \<i> * y  \<longleftrightarrow> x=0 \<and> y=0"
+    using assms imaginary_eq_real_iff by fastforce
 
 subsection \<open>Vector Norm\<close>
 
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Computational_Algebra/Primes.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -119,7 +119,8 @@
   proof (intro allI impI)
     fix m assume "m dvd nat n"
     with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
-    with n(2) have "int m = 1 \<or> int m = n" by auto
+    with n(2) have "int m = 1 \<or> int m = n"
+      using of_nat_0_le_iff by blast
     thus "m = 1 \<or> m = nat n" by auto
   qed
   ultimately show "prime n" 
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Library/Float.thy
--- a/src/HOL/Library/Float.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Library/Float.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -82,7 +82,7 @@
     if "e1 \<le> e2" for e1 m1 e2 m2 :: int
   proof -
     from that have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1"
-      by (simp add: powr_realpow[symmetric] powr_divide2[symmetric] field_simps)
+      by (simp add: powr_realpow[symmetric] powr_diff field_simps)
     then show ?thesis
       by blast
   qed
@@ -384,7 +384,7 @@
     have "m1 \<noteq> 0"
       using m1 unfolding dvd_def by auto
     from \<open>e1 \<le> e2\<close> eq have "m1 = m2 * 2 powr nat (e2 - e1)"
-      by (simp add: powr_divide2[symmetric] field_simps)
+      by (simp add: powr_diff field_simps)
     also have "\<dots> = m2 * 2^nat (e2 - e1)"
       by (simp add: powr_realpow)
     finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)"
@@ -517,7 +517,7 @@
   have "m * 2 powr e = mantissa f * 2 powr exponent f"
     by simp
   then have eq: "m = mantissa f * 2 powr (exponent f - e)"
-    by (simp add: powr_divide2[symmetric] field_simps)
+    by (simp add: powr_diff field_simps)
   moreover
   have "e \<le> exponent f"
   proof (rule ccontr)
@@ -526,7 +526,7 @@
     then have "2 powr (exponent f - e) = 2 powr - real_of_int (e - exponent f)"
       by simp
     also have "\<dots> = 1 / 2^nat (e - exponent f)"
-      using pos by (simp add: powr_realpow[symmetric] powr_divide2[symmetric])
+      using pos by (simp add: powr_realpow[symmetric] powr_diff)
     finally have "m * 2^nat (e - exponent f) = real_of_int (mantissa f)"
       using eq by simp
     then have "mantissa f = m * 2^nat (e - exponent f)"
@@ -583,7 +583,7 @@
      else if m2 = 0 then Float m1 e1
      else if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1
      else Float (m2 + m1 * 2^nat (e1 - e2)) e2)"
-  by transfer (simp add: field_simps powr_realpow[symmetric] powr_divide2[symmetric])
+  by transfer (simp add: field_simps powr_realpow[symmetric] powr_diff)
 
 qualified lemma compute_float_minus[code]: "f - g = f + (-g)" for f g :: float
   by simp
@@ -669,12 +669,12 @@
 
 lemma round_down_shift: "round_down p (x * 2 powr k) = 2 powr k * round_down (p + k) x"
   unfolding round_down_def
-  by (simp add: powr_add powr_mult field_simps powr_divide2[symmetric])
+  by (simp add: powr_add powr_mult field_simps powr_diff)
     (simp add: powr_add[symmetric])
 
 lemma round_up_shift: "round_up p (x * 2 powr k) = 2 powr k * round_up (p + k) x"
   unfolding round_up_def
-  by (simp add: powr_add powr_mult field_simps powr_divide2[symmetric])
+  by (simp add: powr_add powr_mult field_simps powr_diff)
     (simp add: powr_add[symmetric])
 
 lemma round_up_uminus_eq: "round_up p (-x) = - round_down p x"
@@ -702,7 +702,7 @@
   have "x * 2 powr p < 1 / 2 * 2 powr p"
     using assms by simp
   also have "\<dots> \<le> 2 powr p - 1" using \<open>p > 0\<close>
-    by (auto simp: powr_divide2[symmetric] powr_int field_simps self_le_power)
+    by (auto simp: powr_diff powr_int field_simps self_le_power)
   finally show ?thesis using \<open>p > 0\<close>
     by (simp add: round_up_def field_simps powr_minus powr_int ceiling_less_iff)
 qed
@@ -1126,7 +1126,7 @@
       auto
         intro!: floor_eq2
         intro: powr_strict powr
-        simp: powr_divide2[symmetric] powr_add divide_simps algebra_simps)+
+        simp: powr_diff powr_add divide_simps algebra_simps)+
   finally
   show ?thesis by simp
 qed
@@ -1296,7 +1296,7 @@
   "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
   apply transfer
   unfolding real_divl_def of_int_1 mult_1 truncate_down_shift_int[symmetric]
-  apply (simp add: powr_divide2[symmetric] powr_minus)
+  apply (simp add: powr_diff powr_minus)
   done
 
 lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divr
@@ -1510,9 +1510,9 @@
         \<lfloor>real_of_int ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
     proof -
       have "\<lfloor>(2 * ai + sgn b) * 2 powr (real_of_int (q - p) - 1)\<rfloor> = \<lfloor>(ai + sgn b / 2) * 2 powr (q - p)\<rfloor>"
-        by (subst powr_divide2[symmetric]) (simp add: field_simps)
+        by (subst powr_diff) (simp add: field_simps)
       also have "\<dots> = \<lfloor>(ai + sgn b / 2) / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
-        using leqp by (simp add: powr_realpow[symmetric] powr_divide2[symmetric])
+        using leqp by (simp add: powr_realpow[symmetric] powr_diff)
       also have "\<dots> = \<lfloor>ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
         by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
       finally show ?thesis .
@@ -1646,7 +1646,7 @@
       powr_realpow[symmetric] powr_mult_base)
 
   have "\<bar>?m2\<bar> * 2 < 2 powr (bitlen \<bar>m2\<bar> + ?shift + 1)"
-    by (auto simp: field_simps powr_add powr_mult_base powr_divide2[symmetric] abs_mult)
+    by (auto simp: field_simps powr_add powr_mult_base powr_diff abs_mult)
   also have "\<dots> \<le> 2 powr 0"
     using H by (intro powr_mono) auto
   finally have abs_m2_less_half: "\<bar>?m2\<bar> < 1 / 2"
@@ -1657,7 +1657,7 @@
   also have "\<dots> \<le> 2 powr real_of_int (e1 - e2 - 2)"
     by simp
   finally have b_less_quarter: "\<bar>?b\<bar> < 1/4 * 2 powr real_of_int e1"
-    by (simp add: powr_add field_simps powr_divide2[symmetric] abs_mult)
+    by (simp add: powr_add field_simps powr_diff abs_mult)
   also have "1/4 < \<bar>real_of_int m1\<bar> / 2" using \<open>m1 \<noteq> 0\<close> by simp
   finally have b_less_half_a: "\<bar>?b\<bar> < 1/2 * \<bar>?a\<bar>"
     by (simp add: algebra_simps powr_mult_base abs_mult)
@@ -1691,7 +1691,7 @@
     by (auto simp: sgn_if zero_less_mult_iff less_not_sym)
   also
   have "\<bar>?m1 + ?m2'\<bar> * 2 powr ?e = \<bar>?m1 * 2 + sgn m2\<bar> * 2 powr (?e - 1)"
-    by (auto simp: field_simps powr_minus[symmetric] powr_divide2[symmetric] powr_mult_base)
+    by (auto simp: field_simps powr_minus[symmetric] powr_diff powr_mult_base)
   then have "\<lfloor>log 2 \<bar>?m1 + ?m2'\<bar>\<rfloor> + ?e = \<lfloor>log 2 \<bar>real_of_float (Float (?m1 * 2 + sgn m2) (?e - 1))\<bar>\<rfloor>"
     using \<open>?m1 + ?m2' \<noteq> 0\<close>
     unfolding floor_add_int
@@ -1707,7 +1707,7 @@
     have "\<lfloor>(?a + ?b) * 2 powr real_of_int ?f\<rfloor> = \<lfloor>(real_of_int (2 * ?ai) + sgn ?b) * 2 powr real_of_int (?f - - ?e - 1)\<rfloor>"
     proof (rule floor_sum_times_2_powr_sgn_eq)
       show "?a * 2 powr real_of_int (-?e) = real_of_int ?ai"
-        by (simp add: powr_add powr_realpow[symmetric] powr_divide2[symmetric])
+        by (simp add: powr_add powr_realpow[symmetric] powr_diff)
       show "\<bar>?b * 2 powr real_of_int (-?e + 1)\<bar> \<le> 1"
         using abs_m2_less_half
         by (simp add: abs_mult powr_add[symmetric] algebra_simps powr_mult_base)
@@ -1796,7 +1796,7 @@
   using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"]
     two_powr_int_float[of "-3"]
   using powr_realpow[of 2 2] powr_realpow[of 2 3]
-  using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3]
+  using powr_minus[of "2::real" 1] powr_minus[of "2::real" 2] powr_minus[of "2::real" 3]
   by auto
 
 lemma real_of_Float_int[simp]: "real_of_float (Float n 0) = real n"
@@ -1975,7 +1975,7 @@
       have "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le>
         x * (2 powr real (Suc prec) / (2 powr log 2 x))"
         using real_of_int_floor_add_one_ge[of "log 2 x"] assms
-        by (auto simp add: algebra_simps powr_divide2 intro!: mult_left_mono)
+        by (auto simp add: algebra_simps powr_diff [symmetric]  intro!: mult_left_mono)
       then show "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> real_of_int ((2::int) ^ (Suc prec))"
         using \<open>0 < x\<close> by (simp add: powr_realpow powr_add)
     qed
@@ -2059,12 +2059,12 @@
     also have "\<dots> \<le> y * 2 powr real (Suc prec) / (2 powr (real_of_int \<lfloor>log 2 y\<rfloor> + 1))"
       using \<open>0 \<le> y\<close> \<open>0 \<le> x\<close> assms(2)
       by (auto intro!: powr_mono divide_left_mono
-          simp: of_nat_diff powr_add powr_divide2[symmetric])
+          simp: of_nat_diff powr_add powr_diff)
     also have "\<dots> = y * 2 powr real (Suc prec) / (2 powr real_of_int \<lfloor>log 2 y\<rfloor> * 2)"
       by (auto simp: powr_add)
     finally have "(2 ^ prec) \<le> \<lfloor>y * 2 powr real_of_int (int (Suc prec) - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)\<rfloor>"
       using \<open>0 \<le> y\<close>
-      by (auto simp: powr_divide2[symmetric] le_floor_iff powr_realpow powr_add)
+      by (auto simp: powr_diff le_floor_iff powr_realpow powr_add)
     then have "(2 ^ (prec)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>) \<le> truncate_down prec y"
       by (auto simp: truncate_down_def round_down_def)
     moreover have "x \<le> (2 ^ prec) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>)"
@@ -2079,7 +2079,7 @@
         using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
         by (auto intro!: floor_mono)
       finally show ?thesis
-        by (auto simp: powr_realpow[symmetric] powr_divide2[symmetric] assms of_nat_diff)
+        by (auto simp: powr_realpow[symmetric] powr_diff assms of_nat_diff)
     qed
     ultimately show ?thesis
       by (metis dual_order.trans truncate_down)
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Matrix_LP/ComputeFloat.thy
--- a/src/HOL/Matrix_LP/ComputeFloat.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -170,7 +170,7 @@
 lemma float_add:
   "float (a1, e1) + float (a2, e2) =
   (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1) else float (a1*2^(nat (e1-e2))+a2, e2))"
-  by (simp add: float_def algebra_simps powr_realpow[symmetric] powr_divide2[symmetric])
+  by (simp add: float_def algebra_simps powr_realpow[symmetric] powr_diff)
 
 lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
   by (simp add: float_def)
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Nat.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -1700,6 +1700,12 @@
 lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
   by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
 
+lemma of_nat_1_eq_iff [simp]: "1 = of_nat n \<longleftrightarrow> n=1"
+  using of_nat_eq_iff by fastforce
+
+lemma of_nat_eq_1_iff [simp]: "of_nat n = 1 \<longleftrightarrow> n=1"
+  using of_nat_eq_iff by fastforce
+
 lemma of_nat_neq_0 [simp]: "of_nat (Suc n) \<noteq> 0"
   unfolding of_nat_eq_0_iff by simp
 
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -1407,6 +1407,10 @@
   assumes "linear f" obtains c where "f = op* c"
   by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
 
+lemma linear_times_of_real: "linear (\<lambda>x. a * of_real x)"
+  apply (simp add: linear_def Real_Vector_Spaces.additive_def linear_axioms_def)
+  by (metis distrib_left mult_scaleR_right scaleR_conv_of_real)
+
 lemma linearI:
   assumes "\<And>x y. f (x + y) = f x + f y"
     and "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Topological_Spaces.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -2150,11 +2150,12 @@
 
 lemma compactE_image:
   assumes "compact S"
-    and "\<forall>T\<in>C. open (f T)"
-    and "S \<subseteq> (\<Union>c\<in>C. f c)"
+    and op: "\<And>T. T \<in> C \<Longrightarrow> open (f T)"
+    and S: "S \<subseteq> (\<Union>c\<in>C. f c)"
   obtains C' where "C' \<subseteq> C" and "finite C'" and "S \<subseteq> (\<Union>c\<in>C'. f c)"
-  using assms unfolding ball_simps [symmetric]
-  by (metis (lifting) finite_subset_image compact_eq_heine_borel[of S])
+    apply (rule compactE[OF \<open>compact S\<close> S])
+    using op apply force
+    by (metis finite_subset_image)
 
 lemma compact_Int_closed [intro]:
   assumes "compact S"
@@ -2287,7 +2288,7 @@
     unfolding continuous_on_open_invariant by blast
   then obtain A where A: "\<forall>c\<in>C. open (A c) \<and> A c \<inter> s = f -` c \<inter> s"
     unfolding bchoice_iff ..
-  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
+  with cover have "\<And>c. c \<in> C \<Longrightarrow> open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
     by (fastforce simp add: subset_eq set_eq_iff)+
   from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
   with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
@@ -2340,10 +2341,10 @@
   assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)"
   then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s"
     by (metis not_le)
-  then have "\<forall>s\<in>S. open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
+  then have "\<And>s. s\<in>S \<Longrightarrow> open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
     by auto
   with \<open>compact S\<close> obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})"
-    by (erule compactE_image)
+    by (metis compactE_image)
   with \<open>S \<noteq> {}\<close> have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)"
     by (auto intro!: Max_in)
   with C have "S \<subseteq> {..< Max (t`C)}"
@@ -2359,10 +2360,10 @@
   assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t)"
   then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. t s < s"
     by (metis not_le)
-  then have "\<forall>s\<in>S. open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
+  then have "\<And>s. s\<in>S \<Longrightarrow> open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
     by auto
   with \<open>compact S\<close> obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {t s <..})"
-    by (erule compactE_image)
+    by (metis compactE_image)
   with \<open>S \<noteq> {}\<close> have Min: "Min (t`C) \<in> t`C" and "\<forall>s\<in>t`C. Min (t`C) \<le> s"
     by (auto intro!: Min_in)
   with C have "S \<subseteq> {Min (t`C) <..}"
diff -r 66351f79c295 -r 8d53b3bebab4 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Apr 25 21:31:28 2017 +0200
+++ b/src/HOL/Transcendental.thy	Wed Apr 26 15:53:35 2017 +0100
@@ -1506,7 +1506,7 @@
   finally show False by simp
 qed
 
-lemma exp_minus_inverse [simp]: "exp x * exp (- x) = 1"
+lemma exp_minus_inverse: "exp x * exp (- x) = 1"
   by (simp add: exp_add_commuting[symmetric])
 
 lemma exp_minus: "exp (- x) = inverse (exp x)"
@@ -1517,18 +1517,18 @@
   for x :: "'a::{real_normed_field,banach}"
   using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
 
-lemma exp_of_nat_mult [simp]: "exp (of_nat n * x) = exp x ^ n"
+lemma exp_of_nat_mult: "exp (of_nat n * x) = exp x ^ n"
   for x :: "'a::{real_normed_field,banach}"
   by (induct n) (auto simp add: distrib_left exp_add mult.commute)
 
-corollary exp_of_nat2_mult [simp]: "exp (x * of_nat n) = exp x ^ n"
+corollary exp_of_nat2_mult: "exp (x * of_nat n) = exp x ^ n"
   for x :: "'a::{real_normed_field,banach}"
   by (metis exp_of_nat_mult mult_of_nat_commute)
 
 lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = prod (\<lambda>x. exp (f x)) I"
   by (induct I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
 
-lemma exp_divide_power_eq [simp]:
+lemma exp_divide_power_eq:
   fixes x :: "'a::{real_normed_field,banach}"
   assumes "n > 0"
   shows "exp (x / of_nat n) ^ n = exp x"
@@ -1743,7 +1743,7 @@
   for x :: real
   by (erule subst) (rule ln_exp)
 
-lemma ln_mult [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
+lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   for x :: real
   by (rule ln_unique) (simp add: exp_add)
 
@@ -1751,7 +1751,7 @@
   for f :: "'a \<Rightarrow> real"
   by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos)
 
-lemma ln_inverse [simp]: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
+lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   for x :: real
   by (rule ln_unique) (simp add: exp_minus)
 
@@ -1759,8 +1759,8 @@
   for x :: real
   by (rule ln_unique) (simp add: exp_diff)
 
-lemma ln_realpow [simp]: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
-  by (rule ln_unique) simp
+lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
+  by (rule ln_unique) (simp add: exp_of_nat_mult)
 
 lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
   for x :: real
@@ -2480,6 +2480,10 @@
   by (auto simp: powr_def)
 declare powr_one_gt_zero_iff [THEN iffD2, simp]
 
+lemma powr_diff:
+  fixes w:: "'a::{ln,real_normed_field}" shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
+  by (simp add: powr_def algebra_simps exp_diff)
+
 lemma powr_mult: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
   for a x y :: real
   by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
@@ -2494,15 +2498,8 @@
   apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
   done
 
-lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
-  for a b x :: real
-  apply (simp add: powr_def)
-  apply (subst exp_diff [THEN sym])
-  apply (simp add: left_diff_distrib)
-  done
-
 lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
-  for a b x :: real
+  for a b x :: "'a::{ln,real_normed_field}"
   by (simp add: powr_def exp_add [symmetric] distrib_right)
 
 lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
@@ -2518,7 +2515,7 @@
   by (simp add: powr_powr mult.commute)
 
 lemma powr_minus: "x powr (- a) = inverse (x powr a)"
-  for x a :: real
+      for a x :: "'a::{ln,real_normed_field}"
   by (simp add: powr_def exp_minus [symmetric])
 
 lemma powr_minus_divide: "x powr (- a) = 1/(x powr a)"
@@ -2705,27 +2702,13 @@
 lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
   by (induct n) (simp_all add: ac_simps powr_add)
 
-lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
-  by (metis of_nat_numeral powr_realpow)
-
-lemma numeral_powr_numeral[simp]:
-  "(numeral m :: real) powr (numeral n :: real) = numeral m ^ (numeral n)"
-by(simp add: powr_numeral)
-
 lemma powr_real_of_int:
   "x > 0 \<Longrightarrow> x powr real_of_int n = (if n \<ge> 0 then x ^ nat n else inverse (x ^ nat (- n)))"
   using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
   by (auto simp: field_simps powr_minus)
 
-lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
-  by (simp add: powr_numeral)
-
-lemma powr_realpow2: "0 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x^n = (if (x = 0) then 0 else x powr (real n))"
-  apply (cases "x = 0")
-   apply simp_all
-  apply (rule powr_realpow [THEN sym])
-  apply simp
-  done
+lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
+  by (metis of_nat_numeral powr_realpow)
 
 lemma powr_int:
   assumes "x > 0"
@@ -3027,7 +3010,7 @@
     and pos: "g x > 0"
   shows "DERIV (\<lambda>x. (g x) powr r) x :> r * (g x) powr (r - of_nat 1) * m"
   using DERIV_powr[OF g pos DERIV_const, of r] pos
-  by (simp add: powr_divide2[symmetric] field_simps)
+  by (simp add: powr_diff field_simps)
 
 lemma has_real_derivative_powr:
   assumes "z > 0"