# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1568814097 -3600
# Node ID 4e39d87c9737f0dc9e094f7f4d52a5abc7f80a68
# Parent  ae2528273eeb8f2b5eedf24a19f917773d701d1d
imported new material mostly due to Sébastien Gouëzel

diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Analysis/Elementary_Metric_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Analysis/Elementary_Metric_Spaces.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -2179,6 +2179,11 @@
   shows "continuous F (\<lambda>x. infdist (f x) A)"
   using assms unfolding continuous_def by (rule tendsto_infdist)
 
+lemma continuous_on_infdist [continuous_intros]:
+  assumes "continuous_on S f"
+  shows "continuous_on S (\<lambda>x. infdist (f x) A)"
+using assms unfolding continuous_on by (auto intro: tendsto_infdist)
+
 lemma compact_infdist_le:
   fixes A::"'a::heine_borel set"
   assumes "A \<noteq> {}"
@@ -3231,9 +3236,6 @@
     by (auto simp: setdist_def infdist_def)
 qed
 
-lemma continuous_on_infdist [continuous_intros]: "continuous_on B (\<lambda>y. infdist y A)"
-  by (simp add: continuous_on_setdist infdist_eq_setdist)
-
 proposition setdist_attains_inf:
   assumes "compact B" "B \<noteq> {}"
   obtains y where "y \<in> B" "setdist A B = infdist y A"
@@ -3244,7 +3246,7 @@
 next
   case False
   obtain y where "y \<in> B" and min: "\<And>y'. y' \<in> B \<Longrightarrow> infdist y A \<le> infdist y' A"
-    using continuous_attains_inf [OF assms continuous_on_infdist] by blast
+    by (metis continuous_attains_inf [OF assms continuous_on_infdist] continuous_on_id)
   show thesis
   proof
     have "setdist A B = (INF y\<in>B. infdist y A)"
@@ -3266,4 +3268,4 @@
   qed (fact \<open>y \<in> B\<close>)
 qed
 
-end
\ No newline at end of file
+end
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -1219,8 +1219,10 @@
   finally show ?thesis .
 qed
 
-lemma lborel_distr_plus: "distr lborel borel ((+) c) = (lborel :: real measure)"
-  by (subst lborel_real_affine[of 1 c]) (auto simp: density_1 one_ennreal_def[symmetric])
+lemma lborel_distr_plus:
+  fixes c :: "'a::euclidean_space"
+  shows "distr lborel borel ((+) c) = lborel"
+by (subst lborel_affine[of 1 c], auto simp: density_1)
 
 interpretation lborel: sigma_finite_measure lborel
   by (rule sigma_finite_lborel)
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -472,10 +472,23 @@
   "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> emeasure M a + emeasure M b = emeasure M (a \<union> b)"
   using additiveD[OF emeasure_additive] ..
 
-lemma emeasure_Union:
+lemma emeasure_Un:
   "A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> emeasure M (A \<union> B) = emeasure M A + emeasure M (B - A)"
   using plus_emeasure[of A M "B - A"] by auto
 
+lemma emeasure_Un_Int:
+  assumes "A \<in> sets M" "B \<in> sets M"
+  shows "emeasure M A + emeasure M B = emeasure M (A \<union> B) + emeasure M (A \<inter> B)"
+proof -
+  have "A = (A-B) \<union> (A \<inter> B)" by auto
+  then have "emeasure M A = emeasure M (A-B) + emeasure M (A \<inter> B)"
+    by (metis Diff_Diff_Int Diff_disjoint assms plus_emeasure sets.Diff)
+  moreover have "A \<union> B = (A-B) \<union> B" by auto
+  then have "emeasure M (A \<union> B) = emeasure M (A-B) + emeasure M B"
+    by (metis Diff_disjoint Int_commute assms plus_emeasure sets.Diff)
+  ultimately show ?thesis by (metis add.assoc add.commute)
+qed
+
 lemma sum_emeasure:
   "F`I \<subseteq> sets M \<Longrightarrow> disjoint_family_on F I \<Longrightarrow> finite I \<Longrightarrow>
     (\<Sum>i\<in>I. emeasure M (F i)) = emeasure M (\<Union>i\<in>I. F i)"
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -1493,12 +1493,11 @@
   using card_Un_Int [of A B] by simp
 
 lemma card_Un_le: "card (A \<union> B) \<le> card A + card B"
-  apply (cases "finite A")
-   apply (cases "finite B")
-    apply (use le_iff_add card_Un_Int in blast)
-   apply simp
-  apply simp
-  done
+proof (cases "finite A \<and> finite B")
+  case True
+  then show ?thesis
+    using le_iff_add card_Un_Int [of A B] by auto
+qed auto
 
 lemma card_Diff_subset:
   assumes "finite B"
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Groups_Big.thy
--- a/src/HOL/Groups_Big.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Groups_Big.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -1187,6 +1187,16 @@
     using assms card_eq_0_iff finite_UnionD by fastforce
 qed
 
+lemma card_UN_le:
+  assumes "finite I"
+  shows "card(\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. card(A i))"
+  using assms
+proof induction
+  case (insert i I)
+  then show ?case
+    using card_Un_le nat_add_left_cancel_le by (force intro: order_trans) 
+qed auto
+
 lemma sum_multicount_gen:
   assumes "finite s" "finite t" "\<forall>j\<in>t. (card {i\<in>s. R i j} = k j)"
   shows "sum (\<lambda>i. (card {j\<in>t. R i j})) s = sum k t"
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Limits.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -2392,7 +2392,7 @@
     by (rule LIMSEQ_imp_Suc) (simp add: True)
 qed
 
-lemma LIMSEQ_power_zero: "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
+lemma LIMSEQ_power_zero [tendsto_intros]: "norm x < 1 \<Longrightarrow> (\<lambda>n. x ^ n) \<longlonglongrightarrow> 0"
   for x :: "'a::real_normed_algebra_1"
   apply (drule LIMSEQ_realpow_zero [OF norm_ge_zero])
   by (simp add: Zfun_le norm_power_ineq tendsto_Zfun_iff)
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/CLim.thy
--- a/src/HOL/Nonstandard_Analysis/CLim.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/CLim.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -11,7 +11,7 @@
 begin
 
 (*not in simpset?*)
-declare hypreal_epsilon_not_zero [simp]
+declare epsilon_not_zero [simp]
 
 (*??generalize*)
 lemma lemma_complex_mult_inverse_squared [simp]: "x \<noteq> 0 \<Longrightarrow> x * (inverse x)\<^sup>2 = inverse x"
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/HDeriv.thy
--- a/src/HOL/Nonstandard_Analysis/HDeriv.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HDeriv.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -46,7 +46,7 @@
   shows "NSDERIV f x :> D \<Longrightarrow> NSDERIV f x :> E \<Longrightarrow> D = E"
 proof -
   have "\<exists>s. (s::'a star) \<in> Infinitesimal - {0}"
-    by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal hypreal_epsilon_not_zero singletonD)
+    by (metis Diff_iff HDeriv.of_hypreal_eq_0_iff Infinitesimal_epsilon Infinitesimal_of_hypreal epsilon_not_zero singletonD)
   with assms show ?thesis
     by (meson approx_trans3 nsderiv_def star_of_approx_iff)
 qed
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/HLim.thy
--- a/src/HOL/Nonstandard_Analysis/HLim.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLim.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -93,7 +93,7 @@
     have "star_of a + of_hypreal \<epsilon> \<approx> star_of a"
       by (simp add: approx_def)
     then show ?thesis
-      using hypreal_epsilon_not_zero that by (force simp add: NSLIM_def)
+      using epsilon_not_zero that by (force simp add: NSLIM_def)
   qed
   with assms show ?thesis by metis
 qed
@@ -151,7 +151,7 @@
     hnorm (starfun f x - star_of L) < star_of r"
   proof (rule exI, safe)
     show "0 < \<epsilon>"
-      by (rule hypreal_epsilon_gt_zero)
+      by (rule epsilon_gt_zero)
   next
     fix x
     assume neq: "x \<noteq> star_of a"
@@ -291,7 +291,7 @@
   have "\<exists>s>0. \<forall>x y. hnorm (x - y) < s \<longrightarrow> hnorm (starfun f x - starfun f y) < star_of r"
   proof (rule exI, safe)
     show "0 < \<epsilon>"
-      by (rule hypreal_epsilon_gt_zero)
+      by (rule epsilon_gt_zero)
   next
     fix x y :: "'a star"
     assume "hnorm (x - y) < \<epsilon>"
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/HLog.thy
--- a/src/HOL/Nonstandard_Analysis/HLog.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HLog.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -9,15 +9,6 @@
   imports HTranscendental
 begin
 
-
-(* should be in NSA.ML *)
-lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
-  by (simp add: epsilon_def star_n_zero_num star_n_le)
-
-lemma hpfinite_witness: "\<epsilon> \<in> {x. 0 \<le> x \<and> x \<in> HFinite}"
-  by auto
-
-
 definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"  (infixr "powhr" 80)
   where [transfer_unfold]: "x powhr a = starfun2 (powr) x a"
 
@@ -39,7 +30,7 @@
 lemma powhr_not_zero [simp]: "\<And>a x. x powhr a \<noteq> 0 \<longleftrightarrow> x \<noteq> 0"
   by transfer simp
 
-lemma powhr_divide: "\<And>a x y. 0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
+lemma powhr_divide: "\<And>a x y. 0 \<le> x \<Longrightarrow> 0 \<le> y \<Longrightarrow> (x / y) powhr a = (x powhr a) / (y powhr a)"
   by transfer (rule powr_divide)
 
 lemma powhr_add: "\<And>a b x. x powhr (a + b) = (x powhr a) * (x powhr b)"
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/HyperDef.thy
--- a/src/HOL/Nonstandard_Analysis/HyperDef.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/HyperDef.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -229,14 +229,17 @@
     by (auto simp: epsilon_def star_of_def star_n_eq_iff)
 qed
 
-lemma hypreal_epsilon_not_zero: "\<epsilon> \<noteq> 0"
+lemma epsilon_ge_zero [simp]: "0 \<le> \<epsilon>"
+  by (simp add: epsilon_def star_n_zero_num star_n_le)
+
+lemma epsilon_not_zero: "\<epsilon> \<noteq> 0"
   using hypreal_of_real_not_eq_epsilon by force
 
-lemma hypreal_epsilon_inverse_omega: "\<epsilon> = inverse \<omega>"
+lemma epsilon_inverse_omega: "\<epsilon> = inverse \<omega>"
   by (simp add: epsilon_def omega_def star_n_inverse)
 
-lemma hypreal_epsilon_gt_zero: "0 < \<epsilon>"
-  by (simp add: hypreal_epsilon_inverse_omega)
+lemma epsilon_gt_zero: "0 < \<epsilon>"
+  by (simp add: epsilon_inverse_omega)
 
 
 subsection \<open>Embedding the Naturals into the Hyperreals\<close>
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/NSA.thy
--- a/src/HOL/Nonstandard_Analysis/NSA.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -1592,7 +1592,7 @@
 
 lemma Infinitesimal_epsilon [simp]: "\<epsilon> \<in> Infinitesimal"
   by (auto intro!: HInfinite_inverse_Infinitesimal HInfinite_omega
-      simp add: hypreal_epsilon_inverse_omega)
+      simp add: epsilon_inverse_omega)
 
 lemma HFinite_epsilon [simp]: "\<epsilon> \<in> HFinite"
   by (auto intro: Infinitesimal_subset_HFinite [THEN subsetD])
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Nonstandard_Analysis/NSComplex.thy
--- a/src/HOL/Nonstandard_Analysis/NSComplex.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Nonstandard_Analysis/NSComplex.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -197,8 +197,8 @@
 lemma hIm_hcomplex_of_hypreal [simp]: "\<And>z. hIm (hcomplex_of_hypreal z) = 0"
   by transfer (rule Im_complex_of_real)
 
-lemma hcomplex_of_hypreal_epsilon_not_zero [simp]: "hcomplex_of_hypreal \<epsilon> \<noteq> 0"
-  by (simp add: hypreal_epsilon_not_zero)
+lemma hcomplex_of_epsilon_not_zero [simp]: "hcomplex_of_hypreal \<epsilon> \<noteq> 0"
+  by (simp add: epsilon_not_zero)
 
 
 subsection \<open>\<open>HComplex\<close> theorems\<close>
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -1981,14 +1981,12 @@
 lemma Cauchy_iff2: "Cauchy X \<longleftrightarrow> (\<forall>j. (\<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. \<bar>X m - X n\<bar> < inverse (real (Suc j))))"
   by (simp only: metric_Cauchy_iff2 dist_real_def)
 
-lemma lim_1_over_n: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
+lemma lim_1_over_n [tendsto_intros]: "((\<lambda>n. 1 / of_nat n) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
 proof (subst lim_sequentially, intro allI impI exI)
-  fix e :: real
-  assume e: "e > 0"
-  fix n :: nat
-  assume n: "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
+  fix e::real and n
+  assume e: "e > 0" 
   have "inverse e < of_nat (nat \<lceil>inverse e + 1\<rceil>)" by linarith
-  also note n
+  also assume "n \<ge> nat \<lceil>inverse e + 1\<rceil>"
   finally show "dist (1 / of_nat n :: 'a) 0 < e"
     using e by (simp add: divide_simps mult.commute norm_divide)
 qed
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Series.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -585,19 +585,17 @@
 text \<open>Sum of a geometric progression.\<close>
 
 lemma geometric_sums:
-  assumes less_1: "norm c < 1"
+  assumes "norm c < 1"
   shows "(\<lambda>n. c^n) sums (1 / (1 - c))"
 proof -
-  from less_1 have neq_1: "c \<noteq> 1" by auto
-  then have neq_0: "c - 1 \<noteq> 0" by simp
-  from less_1 have lim_0: "(\<lambda>n. c^n) \<longlonglongrightarrow> 0"
-    by (rule LIMSEQ_power_zero)
+  have neq_0: "c - 1 \<noteq> 0"
+    using assms by auto
   then have "(\<lambda>n. c ^ n / (c - 1) - 1 / (c - 1)) \<longlonglongrightarrow> 0 / (c - 1) - 1 / (c - 1)"
-    using neq_0 by (intro tendsto_intros)
+    by (intro tendsto_intros assms)
   then have "(\<lambda>n. (c ^ n - 1) / (c - 1)) \<longlonglongrightarrow> 1 / (1 - c)"
     by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib)
-  then show "(\<lambda>n. c ^ n) sums (1 / (1 - c))"
-    by (simp add: sums_def geometric_sum neq_1)
+  with neq_0 show "(\<lambda>n. c ^ n) sums (1 / (1 - c))"
+    by (simp add: sums_def geometric_sum)
 qed
 
 lemma summable_geometric: "norm c < 1 \<Longrightarrow> summable (\<lambda>n. c^n)"
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Set_Interval.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -1268,6 +1268,18 @@
   qed
 qed
 
+lemma UN_le_add_shift_strict:
+  "(\<Union>i<n::nat. M(i+k)) = (\<Union>i\<in>{k..<n+k}. M i)" (is "?A = ?B")
+proof
+  show "?B \<subseteq> ?A"
+  proof
+    fix x assume "x \<in> ?B"
+    then obtain i where i: "i \<in> {k..<n+k}" "x \<in> M(i)" by auto
+    then have "i - k < n \<and> x \<in> M((i-k) + k)" by auto
+    then show "x \<in> ?A" using UN_le_add_shift by blast
+  qed
+qed (fastforce)
+
 lemma UN_UN_finite_eq: "(\<Union>n::nat. \<Union>i\<in>{0..<n}. A i) = (\<Union>n. A n)"
   by (auto simp add: atLeast0LessThan)
 
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Topological_Spaces.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -1633,6 +1633,39 @@
   "eventually P (nhds a) \<longleftrightarrow> (\<forall>f. f \<longlonglongrightarrow> a \<longrightarrow> eventually (\<lambda>n. P (f n)) sequentially)"
   using eventually_nhds_within_iff_sequentially[of P a UNIV] by simp
 
+(*Thanks to Sébastien Gouëzel*)
+lemma Inf_as_limit:
+  fixes A::"'a::{linorder_topology, first_countable_topology, complete_linorder} set"
+  assumes "A \<noteq> {}"
+  shows "\<exists>u. (\<forall>n. u n \<in> A) \<and> u \<longlonglongrightarrow> Inf A"
+proof (cases "Inf A \<in> A")
+  case True
+  show ?thesis
+    by (rule exI[of _ "\<lambda>n. Inf A"], auto simp add: True)
+next
+  case False
+  obtain y where "y \<in> A" using assms by auto
+  then have "Inf A < y" using False Inf_lower less_le by auto
+  obtain F :: "nat \<Rightarrow> 'a set" where F: "\<And>i. open (F i)" "\<And>i. Inf A \<in> F i"
+                                       "\<And>u. (\<forall>n. u n \<in> F n) \<Longrightarrow> u \<longlonglongrightarrow> Inf A"
+    by (metis first_countable_topology_class.countable_basis)
+  define u where "u = (\<lambda>n. SOME z. z \<in> F n \<and> z \<in> A)"
+  have "\<exists>z. z \<in> U \<and> z \<in> A" if "Inf A \<in> U" "open U" for U
+  proof -
+    obtain b where "b > Inf A" "{Inf A ..<b} \<subseteq> U"
+      using open_right[OF \<open>open U\<close> \<open>Inf A \<in> U\<close> \<open>Inf A < y\<close>] by auto
+    obtain z where "z < b" "z \<in> A"
+      using \<open>Inf A < b\<close> Inf_less_iff by auto
+    then have "z \<in> {Inf A ..<b}"
+      by (simp add: Inf_lower)
+    then show ?thesis using \<open>z \<in> A\<close> \<open>{Inf A ..<b} \<subseteq> U\<close> by auto
+  qed
+  then have *: "u n \<in> F n \<and> u n \<in> A" for n
+    using \<open>Inf A \<in> F n\<close> \<open>open (F n)\<close> unfolding u_def by (metis (no_types, lifting) someI_ex)
+  then have "u \<longlonglongrightarrow> Inf A" using F(3) by simp
+  then show ?thesis using * by auto
+qed
+
 lemma tendsto_at_iff_sequentially:
   "(f \<longlongrightarrow> a) (at x within s) \<longleftrightarrow> (\<forall>X. (\<forall>i. X i \<in> s - {x}) \<longrightarrow> X \<longlonglongrightarrow> x \<longrightarrow> ((f \<circ> X) \<longlonglongrightarrow> a))"
   for f :: "'a::first_countable_topology \<Rightarrow> _"
diff -r ae2528273eeb -r 4e39d87c9737 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Sep 17 16:21:31 2019 +0100
+++ b/src/HOL/Transcendental.thy	Wed Sep 18 14:41:37 2019 +0100
@@ -2461,7 +2461,7 @@
 lemma powr_non_neg[simp]: "\<not>a powr x < 0" for a x::real
   using powr_ge_pzero[of a x] by arith
 
-lemma powr_divide: "0 < x \<Longrightarrow> 0 < y \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
+lemma powr_divide: "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> (x / y) powr a = (x powr a) / (y powr a)"
   for a b x :: real
   apply (simp add: divide_inverse positive_imp_inverse_positive powr_mult)
   apply (simp add: powr_def exp_minus [symmetric] exp_add [symmetric] ln_inverse)
@@ -2471,7 +2471,7 @@
   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)"
+lemma powr_mult_base: "0 \<le> x \<Longrightarrow>x * x powr y = x powr (1 + y)"
   for x :: real
   by (auto simp: powr_add)