Further new material. The simprule status of some exp and ln identities was reverted.
authorpaulson <lp15@cam.ac.uk>
Wed Apr 26 15:53:35 2017 +0100 (2017-04-26)
changeset 655838d53b3bebab4
parent 65580 66351f79c295
child 65584 1d9a96750a40
Further new material. The simprule status of some exp and ln identities was reverted.
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Generalised_Binomial_Theorem.thy
src/HOL/Analysis/Weierstrass_Theorems.thy
src/HOL/Complex.thy
src/HOL/Computational_Algebra/Primes.thy
src/HOL/Library/Float.thy
src/HOL/Matrix_LP/ComputeFloat.thy
src/HOL/Nat.thy
src/HOL/Real_Vector_Spaces.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Tue Apr 25 21:31:28 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Wed Apr 26 15:53:35 2017 +0100
     1.3 @@ -1046,6 +1046,9 @@
     1.4    apply auto
     1.5    done
     1.6  
     1.7 +lemma Ln_eq_zero_iff [simp]: "x \<notin> \<real>\<^sub>\<le>\<^sub>0 \<Longrightarrow> Ln x = 0 \<longleftrightarrow> x = 1"
     1.8 +  by auto (metis exp_Ln exp_zero nonpos_Reals_zero_I)
     1.9 +
    1.10  subsection\<open>Relation to Real Logarithm\<close>
    1.11  
    1.12  lemma Ln_of_real:
    1.13 @@ -1679,23 +1682,19 @@
    1.14    fixes n::nat and z::complex shows "z powr n = (if z = 0 then 0 else z^n)"
    1.15    by (simp add: exp_of_nat_mult powr_def)
    1.16  
    1.17 -lemma powr_add_complex:
    1.18 -  fixes w::complex shows "w powr (z1 + z2) = w powr z1 * w powr z2"
    1.19 -  by (simp add: powr_def algebra_simps exp_add)
    1.20 -
    1.21 -lemma powr_minus_complex:
    1.22 -  fixes w::complex shows  "w powr (-z) = inverse(w powr z)"
    1.23 -  by (simp add: powr_def exp_minus)
    1.24 -
    1.25 -lemma powr_diff_complex:
    1.26 -  fixes w::complex shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
    1.27 -  by (simp add: powr_def algebra_simps exp_diff)
    1.28 -
    1.29  lemma norm_powr_real: "w \<in> \<real> \<Longrightarrow> 0 < Re w \<Longrightarrow> norm(w powr z) = exp(Re z * ln(Re w))"
    1.30    apply (simp add: powr_def)
    1.31    using Im_Ln_eq_0 complex_is_Real_iff norm_complex_def
    1.32    by auto
    1.33  
    1.34 +lemma powr_complexpow [simp]:
    1.35 +  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (of_nat n) = x^n"
    1.36 +  by (induct n) (auto simp: ac_simps powr_add)
    1.37 +
    1.38 +lemma powr_complexnumeral [simp]:
    1.39 +  fixes x::complex shows "x \<noteq> 0 \<Longrightarrow> x powr (numeral n) = x ^ (numeral n)"
    1.40 +  by (metis of_nat_numeral powr_complexpow)
    1.41 +
    1.42  lemma cnj_powr:
    1.43    assumes "Im a = 0 \<Longrightarrow> Re a \<ge> 0"
    1.44    shows   "cnj (a powr b) = cnj a powr cnj b"
    1.45 @@ -1759,16 +1758,15 @@
    1.46    apply (intro derivative_eq_intros | simp)+
    1.47    done
    1.48  
    1.49 -lemma field_differentiable_powr_right:
    1.50 +lemma field_differentiable_powr_right [derivative_intros]:
    1.51    fixes w::complex
    1.52 -  shows
    1.53 -    "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
    1.54 +  shows "w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr z) field_differentiable (at z)"
    1.55  using field_differentiable_def has_field_derivative_powr_right by blast
    1.56  
    1.57 -lemma holomorphic_on_powr_right:
    1.58 +lemma holomorphic_on_powr_right [holomorphic_intros]:
    1.59      "f holomorphic_on s \<Longrightarrow> w \<noteq> 0 \<Longrightarrow> (\<lambda>z. w powr (f z)) holomorphic_on s"
    1.60 -    unfolding holomorphic_on_def field_differentiable_def
    1.61 -by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
    1.62 +  unfolding holomorphic_on_def field_differentiable_def
    1.63 +  by (metis (full_types) DERIV_chain' has_field_derivative_powr_right)
    1.64  
    1.65  lemma norm_powr_real_powr:
    1.66    "w \<in> \<real> \<Longrightarrow> 0 \<le> Re w \<Longrightarrow> cmod (w powr z) = Re w powr Re z"
    1.67 @@ -2562,6 +2560,9 @@
    1.68    using arctan_bounds[of "1/5"   4]
    1.69          arctan_bounds[of "1/239" 4]
    1.70    by (simp_all add: eval_nat_numeral)
    1.71 +    
    1.72 +corollary pi_gt3: "pi > 3"
    1.73 +  using pi_approx by simp
    1.74  
    1.75  
    1.76  subsection\<open>Inverse Sine\<close>
     2.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Apr 25 21:31:28 2017 +0200
     2.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Wed Apr 26 15:53:35 2017 +0100
     2.3 @@ -258,6 +258,14 @@
     2.4      unfolding * using convex_halfspace_le[of "-a" "-b"] by auto
     2.5  qed
     2.6  
     2.7 +lemma convex_halfspace_abs_le: "convex {x. \<bar>inner a x\<bar> \<le> b}"
     2.8 +proof -
     2.9 +  have *: "{x. \<bar>inner a x\<bar> \<le> b} = {x. inner a x \<le> b} \<inter> {x. -b \<le> inner a x}"
    2.10 +    by auto
    2.11 +  show ?thesis
    2.12 +    unfolding * by (simp add: convex_Int convex_halfspace_ge convex_halfspace_le)
    2.13 +qed
    2.14 +
    2.15  lemma convex_hyperplane: "convex {x. inner a x = b}"
    2.16  proof -
    2.17    have *: "{x. inner a x = b} = {x. inner a x \<le> b} \<inter> {x. inner a x \<ge> b}"
     3.1 --- a/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Tue Apr 25 21:31:28 2017 +0200
     3.2 +++ b/src/HOL/Analysis/Generalised_Binomial_Theorem.thy	Wed Apr 26 15:53:35 2017 +0100
     3.3 @@ -129,12 +129,12 @@
     3.4        by (auto intro!: derivative_eq_intros)
     3.5      also from z have "a * f z = (1 + z) * f' z" by (rule deriv)
     3.6      finally show "((\<lambda>z. f z * (1 + z) powr (-a)) has_field_derivative 0) (at z within ball 0 K)"
     3.7 -      using nz by (simp add: field_simps powr_diff_complex at_within_open[OF z'])
     3.8 +      using nz by (simp add: field_simps powr_diff at_within_open[OF z'])
     3.9    qed simp_all
    3.10    then obtain c where c: "\<And>z. z \<in> ball 0 K \<Longrightarrow> f z * (1 + z) powr (-a) = c" by blast
    3.11    from c[of 0] and K have "c = 1" by simp
    3.12    with c[of z] have "f z = (1 + z) powr a" using K
    3.13 -    by (simp add: powr_minus_complex field_simps dist_complex_def)
    3.14 +    by (simp add: powr_minus field_simps dist_complex_def)
    3.15    with summable K show ?thesis unfolding f_f'_def by (simp add: sums_iff)
    3.16  qed
    3.17  
    3.18 @@ -158,7 +158,7 @@
    3.19        by (subst powr_times_real[symmetric]) (simp_all add: field_simps)
    3.20      also from xy have "complex_of_real (1 + x / y) * complex_of_real y = of_real (x + y)"
    3.21        by (simp add: field_simps)
    3.22 -    finally have "?P x y" using xy by (simp add: field_simps powr_diff_complex powr_nat)
    3.23 +    finally have "?P x y" using xy by (simp add: field_simps powr_diff powr_nat)
    3.24    } note A = this
    3.25  
    3.26    show ?thesis
    3.27 @@ -174,7 +174,7 @@
    3.28        fix n :: nat
    3.29        from y have "(a gchoose n) * of_real (-x) ^ n * of_real (-y) powr (a - of_nat n) =
    3.30                         (a gchoose n) * (-of_real x / -of_real y) ^ n * (- of_real y) powr a"
    3.31 -        by (subst power_divide) (simp add: powr_diff_complex powr_nat)
    3.32 +        by (subst power_divide) (simp add: powr_diff powr_nat)
    3.33        also from y have "(- of_real y) powr a = (-1) powr -a * of_real y powr a"
    3.34          by (subst powr_neg_real_complex) simp
    3.35        also have "-complex_of_real x / -complex_of_real y = complex_of_real x / complex_of_real y"
    3.36 @@ -182,7 +182,7 @@
    3.37        also have "... ^ n = of_real x ^ n / of_real y ^ n" by (simp add: power_divide)
    3.38        also have "(a gchoose n) * ... * ((-1) powr -a * of_real y powr a) =
    3.39                     (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - n))"
    3.40 -        by (simp add: algebra_simps powr_diff_complex powr_nat)
    3.41 +        by (simp add: algebra_simps powr_diff powr_nat)
    3.42        finally have "(a gchoose n) * of_real (- x) ^ n * of_real (- y) powr (a - of_nat n) =
    3.43                        (-1) powr -a * ((a gchoose n) * of_real x ^ n * of_real y powr (a - of_nat n))" .
    3.44      }
    3.45 @@ -229,7 +229,7 @@
    3.46    hence "(\<lambda>n. (a gchoose n) * (x / y) ^ n * y powr a) sums ((1 + x / y) powr a * y powr a)"
    3.47      by (rule sums_mult2)
    3.48    with xy show ?thesis
    3.49 -    by (simp add: field_simps powr_divide powr_divide2[symmetric] powr_realpow)
    3.50 +    by (simp add: field_simps powr_divide powr_diff powr_realpow)
    3.51  qed
    3.52  
    3.53  lemma one_plus_neg_powr_powser:
     4.1 --- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Tue Apr 25 21:31:28 2017 +0200
     4.2 +++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Wed Apr 26 15:53:35 2017 +0100
     4.3 @@ -407,7 +407,7 @@
     4.4      then have "exp (real (NN e) * ln (1 / (real k * \<delta>))) < e"
     4.5        by (metis exp_less_mono exp_ln that)
     4.6      then show ?thesis
     4.7 -      by (simp add: \<delta>01(1) \<open>0 < k\<close>)
     4.8 +      by (simp add: \<delta>01(1) \<open>0 < k\<close> exp_of_nat_mult)
     4.9    qed
    4.10    { fix t and e::real
    4.11      assume "e>0"
     5.1 --- a/src/HOL/Complex.thy	Tue Apr 25 21:31:28 2017 +0200
     5.2 +++ b/src/HOL/Complex.thy	Wed Apr 26 15:53:35 2017 +0100
     5.3 @@ -95,6 +95,11 @@
     5.4    unfolding divide_complex_def times_complex.sel inverse_complex.sel
     5.5    by (simp add: divide_simps)
     5.6  
     5.7 +lemma Complex_divide:
     5.8 +    "(x / y) = Complex ((Re x * Re y + Im x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2))
     5.9 +                       ((Im x * Re y - Re x * Im y) / ((Re y)\<^sup>2 + (Im y)\<^sup>2))"
    5.10 +  by (metis Im_divide Re_divide complex_surj)
    5.11 +
    5.12  lemma Re_power2: "Re (x ^ 2) = (Re x)^2 - (Im x)^2"
    5.13    by (simp add: power2_eq_square)
    5.14  
    5.15 @@ -261,6 +266,20 @@
    5.16  lemma divide_numeral_i [simp]: "z / (numeral n * \<i>) = - (\<i> * z) / numeral n"
    5.17    by (metis divide_divide_eq_left divide_i mult.commute mult_minus_right)
    5.18  
    5.19 +lemma imaginary_eq_real_iff [simp]:
    5.20 +  assumes "y \<in> Reals" "x \<in> Reals"
    5.21 +  shows "\<i> * y = x \<longleftrightarrow> x=0 \<and> y=0"
    5.22 +    using assms
    5.23 +    unfolding Reals_def
    5.24 +    apply clarify
    5.25 +      apply (rule iffI)
    5.26 +    apply (metis Im_complex_of_real Im_i_times Re_complex_of_real mult_eq_0_iff of_real_0)
    5.27 +    by simp
    5.28 +
    5.29 +lemma real_eq_imaginary_iff [simp]:
    5.30 +  assumes "y \<in> Reals" "x \<in> Reals"
    5.31 +  shows "x = \<i> * y  \<longleftrightarrow> x=0 \<and> y=0"
    5.32 +    using assms imaginary_eq_real_iff by fastforce
    5.33  
    5.34  subsection \<open>Vector Norm\<close>
    5.35  
     6.1 --- a/src/HOL/Computational_Algebra/Primes.thy	Tue Apr 25 21:31:28 2017 +0200
     6.2 +++ b/src/HOL/Computational_Algebra/Primes.thy	Wed Apr 26 15:53:35 2017 +0100
     6.3 @@ -119,7 +119,8 @@
     6.4    proof (intro allI impI)
     6.5      fix m assume "m dvd nat n"
     6.6      with \<open>n > 1\<close> have "int m dvd n" by (auto simp: int_dvd_iff)
     6.7 -    with n(2) have "int m = 1 \<or> int m = n" by auto
     6.8 +    with n(2) have "int m = 1 \<or> int m = n"
     6.9 +      using of_nat_0_le_iff by blast
    6.10      thus "m = 1 \<or> m = nat n" by auto
    6.11    qed
    6.12    ultimately show "prime n" 
     7.1 --- a/src/HOL/Library/Float.thy	Tue Apr 25 21:31:28 2017 +0200
     7.2 +++ b/src/HOL/Library/Float.thy	Wed Apr 26 15:53:35 2017 +0100
     7.3 @@ -82,7 +82,7 @@
     7.4      if "e1 \<le> e2" for e1 m1 e2 m2 :: int
     7.5    proof -
     7.6      from that have "m1 * 2 powr e1 + m2 * 2 powr e2 = (m1 + m2 * 2 ^ nat (e2 - e1)) * 2 powr e1"
     7.7 -      by (simp add: powr_realpow[symmetric] powr_divide2[symmetric] field_simps)
     7.8 +      by (simp add: powr_realpow[symmetric] powr_diff field_simps)
     7.9      then show ?thesis
    7.10        by blast
    7.11    qed
    7.12 @@ -384,7 +384,7 @@
    7.13      have "m1 \<noteq> 0"
    7.14        using m1 unfolding dvd_def by auto
    7.15      from \<open>e1 \<le> e2\<close> eq have "m1 = m2 * 2 powr nat (e2 - e1)"
    7.16 -      by (simp add: powr_divide2[symmetric] field_simps)
    7.17 +      by (simp add: powr_diff field_simps)
    7.18      also have "\<dots> = m2 * 2^nat (e2 - e1)"
    7.19        by (simp add: powr_realpow)
    7.20      finally have m1_eq: "m1 = m2 * 2^nat (e2 - e1)"
    7.21 @@ -517,7 +517,7 @@
    7.22    have "m * 2 powr e = mantissa f * 2 powr exponent f"
    7.23      by simp
    7.24    then have eq: "m = mantissa f * 2 powr (exponent f - e)"
    7.25 -    by (simp add: powr_divide2[symmetric] field_simps)
    7.26 +    by (simp add: powr_diff field_simps)
    7.27    moreover
    7.28    have "e \<le> exponent f"
    7.29    proof (rule ccontr)
    7.30 @@ -526,7 +526,7 @@
    7.31      then have "2 powr (exponent f - e) = 2 powr - real_of_int (e - exponent f)"
    7.32        by simp
    7.33      also have "\<dots> = 1 / 2^nat (e - exponent f)"
    7.34 -      using pos by (simp add: powr_realpow[symmetric] powr_divide2[symmetric])
    7.35 +      using pos by (simp add: powr_realpow[symmetric] powr_diff)
    7.36      finally have "m * 2^nat (e - exponent f) = real_of_int (mantissa f)"
    7.37        using eq by simp
    7.38      then have "mantissa f = m * 2^nat (e - exponent f)"
    7.39 @@ -583,7 +583,7 @@
    7.40       else if m2 = 0 then Float m1 e1
    7.41       else if e1 \<le> e2 then Float (m1 + m2 * 2^nat (e2 - e1)) e1
    7.42       else Float (m2 + m1 * 2^nat (e1 - e2)) e2)"
    7.43 -  by transfer (simp add: field_simps powr_realpow[symmetric] powr_divide2[symmetric])
    7.44 +  by transfer (simp add: field_simps powr_realpow[symmetric] powr_diff)
    7.45  
    7.46  qualified lemma compute_float_minus[code]: "f - g = f + (-g)" for f g :: float
    7.47    by simp
    7.48 @@ -669,12 +669,12 @@
    7.49  
    7.50  lemma round_down_shift: "round_down p (x * 2 powr k) = 2 powr k * round_down (p + k) x"
    7.51    unfolding round_down_def
    7.52 -  by (simp add: powr_add powr_mult field_simps powr_divide2[symmetric])
    7.53 +  by (simp add: powr_add powr_mult field_simps powr_diff)
    7.54      (simp add: powr_add[symmetric])
    7.55  
    7.56  lemma round_up_shift: "round_up p (x * 2 powr k) = 2 powr k * round_up (p + k) x"
    7.57    unfolding round_up_def
    7.58 -  by (simp add: powr_add powr_mult field_simps powr_divide2[symmetric])
    7.59 +  by (simp add: powr_add powr_mult field_simps powr_diff)
    7.60      (simp add: powr_add[symmetric])
    7.61  
    7.62  lemma round_up_uminus_eq: "round_up p (-x) = - round_down p x"
    7.63 @@ -702,7 +702,7 @@
    7.64    have "x * 2 powr p < 1 / 2 * 2 powr p"
    7.65      using assms by simp
    7.66    also have "\<dots> \<le> 2 powr p - 1" using \<open>p > 0\<close>
    7.67 -    by (auto simp: powr_divide2[symmetric] powr_int field_simps self_le_power)
    7.68 +    by (auto simp: powr_diff powr_int field_simps self_le_power)
    7.69    finally show ?thesis using \<open>p > 0\<close>
    7.70      by (simp add: round_up_def field_simps powr_minus powr_int ceiling_less_iff)
    7.71  qed
    7.72 @@ -1126,7 +1126,7 @@
    7.73        auto
    7.74          intro!: floor_eq2
    7.75          intro: powr_strict powr
    7.76 -        simp: powr_divide2[symmetric] powr_add divide_simps algebra_simps)+
    7.77 +        simp: powr_diff powr_add divide_simps algebra_simps)+
    7.78    finally
    7.79    show ?thesis by simp
    7.80  qed
    7.81 @@ -1296,7 +1296,7 @@
    7.82    "float_divl prec (Float m1 s1) (Float m2 s2) = lapprox_rat prec m1 m2 * Float 1 (s1 - s2)"
    7.83    apply transfer
    7.84    unfolding real_divl_def of_int_1 mult_1 truncate_down_shift_int[symmetric]
    7.85 -  apply (simp add: powr_divide2[symmetric] powr_minus)
    7.86 +  apply (simp add: powr_diff powr_minus)
    7.87    done
    7.88  
    7.89  lift_definition float_divr :: "nat \<Rightarrow> float \<Rightarrow> float \<Rightarrow> float" is real_divr
    7.90 @@ -1510,9 +1510,9 @@
    7.91          \<lfloor>real_of_int ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
    7.92      proof -
    7.93        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>"
    7.94 -        by (subst powr_divide2[symmetric]) (simp add: field_simps)
    7.95 +        by (subst powr_diff) (simp add: field_simps)
    7.96        also have "\<dots> = \<lfloor>(ai + sgn b / 2) / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
    7.97 -        using leqp by (simp add: powr_realpow[symmetric] powr_divide2[symmetric])
    7.98 +        using leqp by (simp add: powr_realpow[symmetric] powr_diff)
    7.99        also have "\<dots> = \<lfloor>ai / real_of_int ((2::int) ^ nat (p - q))\<rfloor>"
   7.100          by (simp del: of_int_power add: floor_divide_real_eq_div floor_eq)
   7.101        finally show ?thesis .
   7.102 @@ -1646,7 +1646,7 @@
   7.103        powr_realpow[symmetric] powr_mult_base)
   7.104  
   7.105    have "\<bar>?m2\<bar> * 2 < 2 powr (bitlen \<bar>m2\<bar> + ?shift + 1)"
   7.106 -    by (auto simp: field_simps powr_add powr_mult_base powr_divide2[symmetric] abs_mult)
   7.107 +    by (auto simp: field_simps powr_add powr_mult_base powr_diff abs_mult)
   7.108    also have "\<dots> \<le> 2 powr 0"
   7.109      using H by (intro powr_mono) auto
   7.110    finally have abs_m2_less_half: "\<bar>?m2\<bar> < 1 / 2"
   7.111 @@ -1657,7 +1657,7 @@
   7.112    also have "\<dots> \<le> 2 powr real_of_int (e1 - e2 - 2)"
   7.113      by simp
   7.114    finally have b_less_quarter: "\<bar>?b\<bar> < 1/4 * 2 powr real_of_int e1"
   7.115 -    by (simp add: powr_add field_simps powr_divide2[symmetric] abs_mult)
   7.116 +    by (simp add: powr_add field_simps powr_diff abs_mult)
   7.117    also have "1/4 < \<bar>real_of_int m1\<bar> / 2" using \<open>m1 \<noteq> 0\<close> by simp
   7.118    finally have b_less_half_a: "\<bar>?b\<bar> < 1/2 * \<bar>?a\<bar>"
   7.119      by (simp add: algebra_simps powr_mult_base abs_mult)
   7.120 @@ -1691,7 +1691,7 @@
   7.121      by (auto simp: sgn_if zero_less_mult_iff less_not_sym)
   7.122    also
   7.123    have "\<bar>?m1 + ?m2'\<bar> * 2 powr ?e = \<bar>?m1 * 2 + sgn m2\<bar> * 2 powr (?e - 1)"
   7.124 -    by (auto simp: field_simps powr_minus[symmetric] powr_divide2[symmetric] powr_mult_base)
   7.125 +    by (auto simp: field_simps powr_minus[symmetric] powr_diff powr_mult_base)
   7.126    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>"
   7.127      using \<open>?m1 + ?m2' \<noteq> 0\<close>
   7.128      unfolding floor_add_int
   7.129 @@ -1707,7 +1707,7 @@
   7.130      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>"
   7.131      proof (rule floor_sum_times_2_powr_sgn_eq)
   7.132        show "?a * 2 powr real_of_int (-?e) = real_of_int ?ai"
   7.133 -        by (simp add: powr_add powr_realpow[symmetric] powr_divide2[symmetric])
   7.134 +        by (simp add: powr_add powr_realpow[symmetric] powr_diff)
   7.135        show "\<bar>?b * 2 powr real_of_int (-?e + 1)\<bar> \<le> 1"
   7.136          using abs_m2_less_half
   7.137          by (simp add: abs_mult powr_add[symmetric] algebra_simps powr_mult_base)
   7.138 @@ -1796,7 +1796,7 @@
   7.139    using two_powr_int_float[of 2] two_powr_int_float[of "-1"] two_powr_int_float[of "-2"]
   7.140      two_powr_int_float[of "-3"]
   7.141    using powr_realpow[of 2 2] powr_realpow[of 2 3]
   7.142 -  using powr_minus[of 2 1] powr_minus[of 2 2] powr_minus[of 2 3]
   7.143 +  using powr_minus[of "2::real" 1] powr_minus[of "2::real" 2] powr_minus[of "2::real" 3]
   7.144    by auto
   7.145  
   7.146  lemma real_of_Float_int[simp]: "real_of_float (Float n 0) = real n"
   7.147 @@ -1975,7 +1975,7 @@
   7.148        have "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le>
   7.149          x * (2 powr real (Suc prec) / (2 powr log 2 x))"
   7.150          using real_of_int_floor_add_one_ge[of "log 2 x"] assms
   7.151 -        by (auto simp add: algebra_simps powr_divide2 intro!: mult_left_mono)
   7.152 +        by (auto simp add: algebra_simps powr_diff [symmetric]  intro!: mult_left_mono)
   7.153        then show "x * 2 powr real_of_int (int prec - \<lfloor>log 2 x\<rfloor>) \<le> real_of_int ((2::int) ^ (Suc prec))"
   7.154          using \<open>0 < x\<close> by (simp add: powr_realpow powr_add)
   7.155      qed
   7.156 @@ -2059,12 +2059,12 @@
   7.157      also have "\<dots> \<le> y * 2 powr real (Suc prec) / (2 powr (real_of_int \<lfloor>log 2 y\<rfloor> + 1))"
   7.158        using \<open>0 \<le> y\<close> \<open>0 \<le> x\<close> assms(2)
   7.159        by (auto intro!: powr_mono divide_left_mono
   7.160 -          simp: of_nat_diff powr_add powr_divide2[symmetric])
   7.161 +          simp: of_nat_diff powr_add powr_diff)
   7.162      also have "\<dots> = y * 2 powr real (Suc prec) / (2 powr real_of_int \<lfloor>log 2 y\<rfloor> * 2)"
   7.163        by (auto simp: powr_add)
   7.164      finally have "(2 ^ prec) \<le> \<lfloor>y * 2 powr real_of_int (int (Suc prec) - \<lfloor>log 2 \<bar>y\<bar>\<rfloor> - 1)\<rfloor>"
   7.165        using \<open>0 \<le> y\<close>
   7.166 -      by (auto simp: powr_divide2[symmetric] le_floor_iff powr_realpow powr_add)
   7.167 +      by (auto simp: powr_diff le_floor_iff powr_realpow powr_add)
   7.168      then have "(2 ^ (prec)) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>) \<le> truncate_down prec y"
   7.169        by (auto simp: truncate_down_def round_down_def)
   7.170      moreover have "x \<le> (2 ^ prec) * 2 powr - real_of_int (int prec - \<lfloor>log 2 \<bar>y\<bar>\<rfloor>)"
   7.171 @@ -2079,7 +2079,7 @@
   7.172          using logless flogless \<open>x > 0\<close> \<open>y > 0\<close>
   7.173          by (auto intro!: floor_mono)
   7.174        finally show ?thesis
   7.175 -        by (auto simp: powr_realpow[symmetric] powr_divide2[symmetric] assms of_nat_diff)
   7.176 +        by (auto simp: powr_realpow[symmetric] powr_diff assms of_nat_diff)
   7.177      qed
   7.178      ultimately show ?thesis
   7.179        by (metis dual_order.trans truncate_down)
     8.1 --- a/src/HOL/Matrix_LP/ComputeFloat.thy	Tue Apr 25 21:31:28 2017 +0200
     8.2 +++ b/src/HOL/Matrix_LP/ComputeFloat.thy	Wed Apr 26 15:53:35 2017 +0100
     8.3 @@ -170,7 +170,7 @@
     8.4  lemma float_add:
     8.5    "float (a1, e1) + float (a2, e2) =
     8.6    (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1) else float (a1*2^(nat (e1-e2))+a2, e2))"
     8.7 -  by (simp add: float_def algebra_simps powr_realpow[symmetric] powr_divide2[symmetric])
     8.8 +  by (simp add: float_def algebra_simps powr_realpow[symmetric] powr_diff)
     8.9  
    8.10  lemma float_mult_l0: "float (0, e) * x = float (0, 0)"
    8.11    by (simp add: float_def)
     9.1 --- a/src/HOL/Nat.thy	Tue Apr 25 21:31:28 2017 +0200
     9.2 +++ b/src/HOL/Nat.thy	Wed Apr 26 15:53:35 2017 +0100
     9.3 @@ -1700,6 +1700,12 @@
     9.4  lemma of_nat_eq_0_iff [simp]: "of_nat m = 0 \<longleftrightarrow> m = 0"
     9.5    by (fact of_nat_eq_iff [of m 0, unfolded of_nat_0])
     9.6  
     9.7 +lemma of_nat_1_eq_iff [simp]: "1 = of_nat n \<longleftrightarrow> n=1"
     9.8 +  using of_nat_eq_iff by fastforce
     9.9 +
    9.10 +lemma of_nat_eq_1_iff [simp]: "of_nat n = 1 \<longleftrightarrow> n=1"
    9.11 +  using of_nat_eq_iff by fastforce
    9.12 +
    9.13  lemma of_nat_neq_0 [simp]: "of_nat (Suc n) \<noteq> 0"
    9.14    unfolding of_nat_eq_0_iff by simp
    9.15  
    10.1 --- a/src/HOL/Real_Vector_Spaces.thy	Tue Apr 25 21:31:28 2017 +0200
    10.2 +++ b/src/HOL/Real_Vector_Spaces.thy	Wed Apr 26 15:53:35 2017 +0100
    10.3 @@ -1407,6 +1407,10 @@
    10.4    assumes "linear f" obtains c where "f = op* c"
    10.5    by (rule linear_imp_scaleR [OF assms]) (force simp: scaleR_conv_of_real)
    10.6  
    10.7 +lemma linear_times_of_real: "linear (\<lambda>x. a * of_real x)"
    10.8 +  apply (simp add: linear_def Real_Vector_Spaces.additive_def linear_axioms_def)
    10.9 +  by (metis distrib_left mult_scaleR_right scaleR_conv_of_real)
   10.10 +
   10.11  lemma linearI:
   10.12    assumes "\<And>x y. f (x + y) = f x + f y"
   10.13      and "\<And>c x. f (c *\<^sub>R x) = c *\<^sub>R f x"
    11.1 --- a/src/HOL/Topological_Spaces.thy	Tue Apr 25 21:31:28 2017 +0200
    11.2 +++ b/src/HOL/Topological_Spaces.thy	Wed Apr 26 15:53:35 2017 +0100
    11.3 @@ -2150,11 +2150,12 @@
    11.4  
    11.5  lemma compactE_image:
    11.6    assumes "compact S"
    11.7 -    and "\<forall>T\<in>C. open (f T)"
    11.8 -    and "S \<subseteq> (\<Union>c\<in>C. f c)"
    11.9 +    and op: "\<And>T. T \<in> C \<Longrightarrow> open (f T)"
   11.10 +    and S: "S \<subseteq> (\<Union>c\<in>C. f c)"
   11.11    obtains C' where "C' \<subseteq> C" and "finite C'" and "S \<subseteq> (\<Union>c\<in>C'. f c)"
   11.12 -  using assms unfolding ball_simps [symmetric]
   11.13 -  by (metis (lifting) finite_subset_image compact_eq_heine_borel[of S])
   11.14 +    apply (rule compactE[OF \<open>compact S\<close> S])
   11.15 +    using op apply force
   11.16 +    by (metis finite_subset_image)
   11.17  
   11.18  lemma compact_Int_closed [intro]:
   11.19    assumes "compact S"
   11.20 @@ -2287,7 +2288,7 @@
   11.21      unfolding continuous_on_open_invariant by blast
   11.22    then obtain A where A: "\<forall>c\<in>C. open (A c) \<and> A c \<inter> s = f -` c \<inter> s"
   11.23      unfolding bchoice_iff ..
   11.24 -  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
   11.25 +  with cover have "\<And>c. c \<in> C \<Longrightarrow> open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
   11.26      by (fastforce simp add: subset_eq set_eq_iff)+
   11.27    from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
   11.28    with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
   11.29 @@ -2340,10 +2341,10 @@
   11.30    assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)"
   11.31    then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s"
   11.32      by (metis not_le)
   11.33 -  then have "\<forall>s\<in>S. open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
   11.34 +  then have "\<And>s. s\<in>S \<Longrightarrow> open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
   11.35      by auto
   11.36    with \<open>compact S\<close> obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})"
   11.37 -    by (erule compactE_image)
   11.38 +    by (metis compactE_image)
   11.39    with \<open>S \<noteq> {}\<close> have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)"
   11.40      by (auto intro!: Max_in)
   11.41    with C have "S \<subseteq> {..< Max (t`C)}"
   11.42 @@ -2359,10 +2360,10 @@
   11.43    assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t)"
   11.44    then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. t s < s"
   11.45      by (metis not_le)
   11.46 -  then have "\<forall>s\<in>S. open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
   11.47 +  then have "\<And>s. s\<in>S \<Longrightarrow> open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
   11.48      by auto
   11.49    with \<open>compact S\<close> obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {t s <..})"
   11.50 -    by (erule compactE_image)
   11.51 +    by (metis compactE_image)
   11.52    with \<open>S \<noteq> {}\<close> have Min: "Min (t`C) \<in> t`C" and "\<forall>s\<in>t`C. Min (t`C) \<le> s"
   11.53      by (auto intro!: Min_in)
   11.54    with C have "S \<subseteq> {Min (t`C) <..}"
    12.1 --- a/src/HOL/Transcendental.thy	Tue Apr 25 21:31:28 2017 +0200
    12.2 +++ b/src/HOL/Transcendental.thy	Wed Apr 26 15:53:35 2017 +0100
    12.3 @@ -1506,7 +1506,7 @@
    12.4    finally show False by simp
    12.5  qed
    12.6  
    12.7 -lemma exp_minus_inverse [simp]: "exp x * exp (- x) = 1"
    12.8 +lemma exp_minus_inverse: "exp x * exp (- x) = 1"
    12.9    by (simp add: exp_add_commuting[symmetric])
   12.10  
   12.11  lemma exp_minus: "exp (- x) = inverse (exp x)"
   12.12 @@ -1517,18 +1517,18 @@
   12.13    for x :: "'a::{real_normed_field,banach}"
   12.14    using exp_add [of x "- y"] by (simp add: exp_minus divide_inverse)
   12.15  
   12.16 -lemma exp_of_nat_mult [simp]: "exp (of_nat n * x) = exp x ^ n"
   12.17 +lemma exp_of_nat_mult: "exp (of_nat n * x) = exp x ^ n"
   12.18    for x :: "'a::{real_normed_field,banach}"
   12.19    by (induct n) (auto simp add: distrib_left exp_add mult.commute)
   12.20  
   12.21 -corollary exp_of_nat2_mult [simp]: "exp (x * of_nat n) = exp x ^ n"
   12.22 +corollary exp_of_nat2_mult: "exp (x * of_nat n) = exp x ^ n"
   12.23    for x :: "'a::{real_normed_field,banach}"
   12.24    by (metis exp_of_nat_mult mult_of_nat_commute)
   12.25  
   12.26  lemma exp_sum: "finite I \<Longrightarrow> exp (sum f I) = prod (\<lambda>x. exp (f x)) I"
   12.27    by (induct I rule: finite_induct) (auto simp: exp_add_commuting mult.commute)
   12.28  
   12.29 -lemma exp_divide_power_eq [simp]:
   12.30 +lemma exp_divide_power_eq:
   12.31    fixes x :: "'a::{real_normed_field,banach}"
   12.32    assumes "n > 0"
   12.33    shows "exp (x / of_nat n) ^ n = exp x"
   12.34 @@ -1743,7 +1743,7 @@
   12.35    for x :: real
   12.36    by (erule subst) (rule ln_exp)
   12.37  
   12.38 -lemma ln_mult [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   12.39 +lemma ln_mult: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln (x * y) = ln x + ln y"
   12.40    for x :: real
   12.41    by (rule ln_unique) (simp add: exp_add)
   12.42  
   12.43 @@ -1751,7 +1751,7 @@
   12.44    for f :: "'a \<Rightarrow> real"
   12.45    by (induct I rule: finite_induct) (auto simp: ln_mult prod_pos)
   12.46  
   12.47 -lemma ln_inverse [simp]: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   12.48 +lemma ln_inverse: "0 < x \<Longrightarrow> ln (inverse x) = - ln x"
   12.49    for x :: real
   12.50    by (rule ln_unique) (simp add: exp_minus)
   12.51  
   12.52 @@ -1759,8 +1759,8 @@
   12.53    for x :: real
   12.54    by (rule ln_unique) (simp add: exp_diff)
   12.55  
   12.56 -lemma ln_realpow [simp]: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
   12.57 -  by (rule ln_unique) simp
   12.58 +lemma ln_realpow: "0 < x \<Longrightarrow> ln (x^n) = real n * ln x"
   12.59 +  by (rule ln_unique) (simp add: exp_of_nat_mult)
   12.60  
   12.61  lemma ln_less_cancel_iff [simp]: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> ln x < ln y \<longleftrightarrow> x < y"
   12.62    for x :: real
   12.63 @@ -2480,6 +2480,10 @@
   12.64    by (auto simp: powr_def)
   12.65  declare powr_one_gt_zero_iff [THEN iffD2, simp]
   12.66  
   12.67 +lemma powr_diff:
   12.68 +  fixes w:: "'a::{ln,real_normed_field}" shows  "w powr (z1 - z2) = w powr z1 / w powr z2"
   12.69 +  by (simp add: powr_def algebra_simps exp_diff)
   12.70 +
   12.71  lemma powr_mult: "0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x * y) powr a = (x powr a) * (y powr a)"
   12.72    for a x y :: real
   12.73    by (simp add: powr_def exp_add [symmetric] ln_mult distrib_left)
   12.74 @@ -2494,15 +2498,8 @@
   12.75    apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
   12.76    done
   12.77  
   12.78 -lemma powr_divide2: "x powr a / x powr b = x powr (a - b)"
   12.79 -  for a b x :: real
   12.80 -  apply (simp add: powr_def)
   12.81 -  apply (subst exp_diff [THEN sym])
   12.82 -  apply (simp add: left_diff_distrib)
   12.83 -  done
   12.84 -
   12.85  lemma powr_add: "x powr (a + b) = (x powr a) * (x powr b)"
   12.86 -  for a b x :: real
   12.87 +  for a b x :: "'a::{ln,real_normed_field}"
   12.88    by (simp add: powr_def exp_add [symmetric] distrib_right)
   12.89  
   12.90  lemma powr_mult_base: "0 < x \<Longrightarrow>x * x powr y = x powr (1 + y)"
   12.91 @@ -2518,7 +2515,7 @@
   12.92    by (simp add: powr_powr mult.commute)
   12.93  
   12.94  lemma powr_minus: "x powr (- a) = inverse (x powr a)"
   12.95 -  for x a :: real
   12.96 +      for a x :: "'a::{ln,real_normed_field}"
   12.97    by (simp add: powr_def exp_minus [symmetric])
   12.98  
   12.99  lemma powr_minus_divide: "x powr (- a) = 1/(x powr a)"
  12.100 @@ -2705,27 +2702,13 @@
  12.101  lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
  12.102    by (induct n) (simp_all add: ac_simps powr_add)
  12.103  
  12.104 -lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
  12.105 -  by (metis of_nat_numeral powr_realpow)
  12.106 -
  12.107 -lemma numeral_powr_numeral[simp]:
  12.108 -  "(numeral m :: real) powr (numeral n :: real) = numeral m ^ (numeral n)"
  12.109 -by(simp add: powr_numeral)
  12.110 -
  12.111  lemma powr_real_of_int:
  12.112    "x > 0 \<Longrightarrow> x powr real_of_int n = (if n \<ge> 0 then x ^ nat n else inverse (x ^ nat (- n)))"
  12.113    using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
  12.114    by (auto simp: field_simps powr_minus)
  12.115  
  12.116 -lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
  12.117 -  by (simp add: powr_numeral)
  12.118 -
  12.119 -lemma powr_realpow2: "0 \<le> x \<Longrightarrow> 0 < n \<Longrightarrow> x^n = (if (x = 0) then 0 else x powr (real n))"
  12.120 -  apply (cases "x = 0")
  12.121 -   apply simp_all
  12.122 -  apply (rule powr_realpow [THEN sym])
  12.123 -  apply simp
  12.124 -  done
  12.125 +lemma powr_numeral [simp]: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
  12.126 +  by (metis of_nat_numeral powr_realpow)
  12.127  
  12.128  lemma powr_int:
  12.129    assumes "x > 0"
  12.130 @@ -3027,7 +3010,7 @@
  12.131      and pos: "g x > 0"
  12.132    shows "DERIV (\<lambda>x. (g x) powr r) x :> r * (g x) powr (r - of_nat 1) * m"
  12.133    using DERIV_powr[OF g pos DERIV_const, of r] pos
  12.134 -  by (simp add: powr_divide2[symmetric] field_simps)
  12.135 +  by (simp add: powr_diff field_simps)
  12.136  
  12.137  lemma has_real_derivative_powr:
  12.138    assumes "z > 0"