# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1530191637 -3600
# Node ID 2f4e2aab190aa40f15858a837e5abf312347160d
# Parent  f5ca4c2157a5e8f8eef967929feac4e0f148a492
Generalising and renaming some basic results

diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Arcwise_Connected.thy
--- a/src/HOL/Analysis/Arcwise_Connected.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -1243,7 +1243,7 @@
         by (metis atLeastAtMost_iff a_ge_0 b_le_1 order.trans)+
       moreover have "y < \<delta> + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < \<delta> + y"
         using y apply simp_all
-        using alec [of m n] cleb [of m n] n real_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
+        using alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
         by linarith+
       moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close>
       ultimately show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -283,7 +283,7 @@
       have x2: "(x + 1) / 2 \<notin> S"
         using that
         apply (clarsimp simp: image_iff)
-        by (metis add.commute add_diff_cancel_left' mult_2 real_sum_of_halves)
+        by (metis add.commute add_diff_cancel_left' mult_2 field_sum_of_halves)
       have "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
         by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+
       then show "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
@@ -6161,7 +6161,7 @@
   obtain r where "r > 0" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
   proof
     have "cball z ((r + dist w z) / 2) \<subseteq> ball z r"
-      using w by (simp add: dist_commute real_sum_of_halves subset_eq)
+      using w by (simp add: dist_commute field_sum_of_halves subset_eq)
     then show "f holomorphic_on cball z ((r + dist w z) / 2)"
       by (rule holomorphic_on_subset [OF holf])
     have "r > 0"
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -1575,6 +1575,55 @@
 
 text\<open>Finally the Argument is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\<close>
 
+lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
+  by (simp add: Im_Ln_eq_pi Arg_def)
+
+lemma mpi_less_Arg: "-pi < Arg z"
+    and Arg_le_pi: "Arg z \<le> pi"
+  by (auto simp: Arg_def mpi_less_Im_Ln Im_Ln_le_pi)
+
+lemma
+  assumes "z \<noteq> 0"
+  shows Arg_eq: "z = of_real(norm z) * exp(\<i> * Arg z)"
+  using assms exp_Ln exp_eq_polar
+  by (auto simp:  Arg_def)
+
+lemma Argument_exists:
+  assumes "z \<noteq> 0" and R: "R = {r-pi<..r+pi}"
+  obtains s where "is_Arg z s" "s\<in>R"
+proof -
+  let ?rp = "r - Arg z + pi"
+  define k where "k \<equiv> \<lfloor>?rp / (2 * pi)\<rfloor>"
+  have "(Arg z + of_int k * (2 * pi)) \<in> R"
+    using floor_divide_lower [of "2*pi" ?rp] floor_divide_upper [of "2*pi" ?rp]
+    by (auto simp: k_def algebra_simps R)
+  then show ?thesis
+    using Arg_eq \<open>z \<noteq> 0\<close> is_Arg_2pi_iff is_Arg_def that by blast
+qed
+
+lemma Argument_exists_unique:
+  assumes "z \<noteq> 0" and R: "R = {r-pi<..r+pi}"
+  obtains s where "is_Arg z s" "s\<in>R" "\<And>t. \<lbrakk>is_Arg z t; t\<in>R\<rbrakk> \<Longrightarrow> s=t"
+proof -
+  obtain s where s: "is_Arg z s" "s\<in>R"
+    using Argument_exists [OF assms] .
+  moreover have "\<And>t. \<lbrakk>is_Arg z t; t\<in>R\<rbrakk> \<Longrightarrow> s=t"
+    using assms s  by (auto simp: is_Arg_eqI)
+  ultimately show thesis
+    using that by blast
+qed
+
+lemma Argument_Ex1:
+  assumes "z \<noteq> 0" and R: "R = {r-pi<..r+pi}"
+  shows "\<exists>!s. is_Arg z s \<and> s \<in> R"
+  using Argument_exists_unique [OF assms]  by metis
+
+lemma Arg_divide:
+  assumes "w \<noteq> 0" "z \<noteq> 0"
+  shows "is_Arg (z / w) (Arg z - Arg w)"
+  using Arg_eq [of z] Arg_eq [of w] Arg_eq [of "norm(z / w)"] assms
+  by (auto simp: is_Arg_def norm_divide field_simps exp_diff Arg_of_real)
+
 lemma Arg_unique_lemma:
   assumes z:  "is_Arg z t"
       and z': "is_Arg z t'"
@@ -1603,14 +1652,6 @@
     by simp
 qed
 
-lemma
-  assumes "z \<noteq> 0"
-  shows mpi_less_Arg: "-pi < Arg z"
-    and Arg_le_pi: "Arg z \<le> pi"
-    and Arg_eq: "z = of_real(norm z) * exp(\<i> * Arg z)"
-  using assms exp_Ln exp_eq_polar
-  by (auto simp: mpi_less_Im_Ln Im_Ln_le_pi Arg_def)
-
 lemma complex_norm_eq_1_exp_eq: "norm z = 1 \<longleftrightarrow> exp(\<i> * (Arg z)) = z"
   by (metis Arg_eq exp_not_eq_zero exp_zero mult.left_neutral norm_zero of_real_1 norm_exp_i_times)
 
@@ -1618,7 +1659,6 @@
   by (rule Arg_unique_lemma [unfolded is_Arg_def, OF _ Arg_eq])
      (use mpi_less_Arg Arg_le_pi in \<open>auto simp: norm_mult\<close>)
 
-
 lemma Arg_minus:
   assumes "z \<noteq> 0"
   shows "Arg (-z) = (if Arg z \<le> 0 then Arg z + pi else Arg z - pi)"
@@ -1671,9 +1711,6 @@
 corollary Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
   using assms by (auto simp: nonneg_Reals_def Arg_eq_0)
 
-lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
-  by (simp add: Im_Ln_eq_pi Arg_def)
-
 lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
 proof (cases "z=0")
   case False
@@ -1695,7 +1732,7 @@
 next
   case False
   then have "Arg z < pi" "z \<noteq> 0"
-    using Arg_def Arg_eq_0_pi Arg_le_pi by fastforce+
+    using Arg_eq_0_pi Arg_le_pi by (auto simp: less_eq_real_def)
   then show ?thesis
     apply (simp add: False)
     apply (rule Arg_unique [of "inverse (norm z)"])
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Connected.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -2871,7 +2871,7 @@
     then obtain C where C: "x \<in> C" "C \<in> \<C>"
       using \<open>S \<subseteq> \<Union>\<C>\<close> by blast
     then obtain r where r: "r>0" "ball x (2*r) \<subseteq> C"
-      by (metis mult.commute mult_2_right not_le ope openE real_sum_of_halves zero_le_numeral zero_less_mult_iff)
+      by (metis mult.commute mult_2_right not_le ope openE field_sum_of_halves zero_le_numeral zero_less_mult_iff)
     then have "\<exists>r C. r > 0 \<and> ball x (2*r) \<subseteq> C \<and> C \<in> \<C>"
       using C by blast
   }
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -2234,7 +2234,7 @@
   then obtain y where "y\<in>s" and y: "f x > f y" by auto
   then have xy: "0 < dist x y"  by auto
   then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
-    using real_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
+    using field_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
   then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
     using \<open>x\<in>s\<close> \<open>y\<in>s\<close>
     using assms(2)[unfolded convex_on_def,
@@ -5052,7 +5052,7 @@
       next
         assume "u \<noteq> 0" "v \<noteq> 0"
         then obtain w where w: "w>0" "w<u" "w<v"
-          using real_lbound_gt_zero[of u v] and obt(1,2) by auto
+          using field_lbound_gt_zero[of u v] and obt(1,2) by auto
         have "x \<noteq> b"
         proof
           assume "x = b"
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -1132,7 +1132,7 @@
     obtain d2 where "0 < d2" and d2: "\<And>u. dist u y < d2 \<Longrightarrow> u \<in> T"
       using \<open>open T\<close> \<open>y \<in> T\<close> unfolding open_dist by blast
     obtain d where d: "0 < d" "d < d1" "d < d2"
-      using real_lbound_gt_zero[OF \<open>0 < d1\<close> \<open>0 < d2\<close>] by blast
+      using field_lbound_gt_zero[OF \<open>0 < d1\<close> \<open>0 < d2\<close>] by blast
     show "\<exists>d>0. \<forall>z. norm (z - y) < d \<longrightarrow> norm (g z - g y - g' (z - y)) \<le> e * norm (g z - g y)"
     proof (intro exI allI impI conjI)
       fix z
@@ -1188,7 +1188,7 @@
         "\<And>z. norm (z - y) < d' \<Longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
       using lem1 * by blast
     obtain k where k: "0 < k" "k < d" "k < d'"
-      using real_lbound_gt_zero[OF \<open>0 < d\<close> \<open>0 < d'\<close>] by blast
+      using field_lbound_gt_zero[OF \<open>0 < d\<close> \<open>0 < d'\<close>] by blast
     show "\<exists>d>0. \<forall>ya. norm (ya - y) < d \<longrightarrow> norm (g ya - g y - g' (ya - y)) \<le> e * norm (ya - y)"
     proof (intro exI allI impI conjI)
       fix z
@@ -1331,7 +1331,7 @@
     using mem_interior_cball x by blast
   have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
   obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
-    using real_lbound_gt_zero[OF *] by blast
+    using field_lbound_gt_zero[OF *] by blast
   have lem: "\<exists>y\<in>cball (f x) e. f (x + g' (y - f x)) = z" if "z\<in>cball (f x) (e / 2)" for z
   proof (rule brouwer_surjective_cball)
     have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
@@ -1544,7 +1544,7 @@
   obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> S"
     using \<open>0 < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by blast
   obtain d where d: "0 < d" "d < d1" "d < d2"
-    using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
+    using field_lbound_gt_zero[OF d1(1) d2(1)] by blast
   show ?thesis
   proof
     show "0 < d" by (fact d)
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -1371,7 +1371,7 @@
     by (metis dual_order.strict_implies_order negligible_imp_measurable negligible_imp_measure0 order_refl)
 next
   assume ?rhs then show "negligible S"
-    by (metis le_less_trans negligible_outer real_lbound_gt_zero)
+    by (metis le_less_trans negligible_outer field_lbound_gt_zero)
 qed
 
 lemma negligible_UNIV: "negligible S \<longleftrightarrow> (indicat_real S has_integral 0) UNIV" (is "_=?rhs")
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Great_Picard.thy
--- a/src/HOL/Analysis/Great_Picard.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -1209,7 +1209,7 @@
         have "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e/2 + e/2"
           using eventually_conj [OF K z1]
           apply (rule eventually_mono)
-          by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half real_sum_of_halves)
+          by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half field_sum_of_halves)
         then
         show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e"
           by simp
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -7086,7 +7086,7 @@
                 \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
         by (simp only: integral_diff [symmetric] int_integrable integrable_const)
       have norm_xx: "\<lbrakk>x' = y'; norm(x - x') \<le> e/2; norm(y - y') \<le> e/2\<rbrakk> \<Longrightarrow> norm(x - y) \<le> e" for x::'c and y x' y' e
-        using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] real_sum_of_halves
+        using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] field_sum_of_halves
         by (simp add: norm_minus_commute)
       have "norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
             \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX"
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -226,6 +226,23 @@
   shows "convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. f i) \<and> lim (\<lambda>n. \<Prod>i\<le>n. f i) \<noteq> 0"
   by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)
 
+lemma bounded_imp_convergent_prod:
+  fixes a :: "nat \<Rightarrow> real"
+  assumes 1: "\<And>n. a n \<ge> 1" and bounded: "\<And>n. (\<Prod>i\<le>n. a i) \<le> B"
+  shows "convergent_prod a"
+proof -
+  have "bdd_above (range(\<lambda>n. \<Prod>i\<le>n. a i))"
+    by (meson bdd_aboveI2 bounded)
+  moreover have "incseq (\<lambda>n. \<Prod>i\<le>n. a i)"
+    unfolding mono_def by (metis 1 prod_mono2 atMost_subset_iff dual_order.trans finite_atMost zero_le_one)
+  ultimately obtain p where p: "(\<lambda>n. \<Prod>i\<le>n. a i) \<longlonglongrightarrow> p"
+    using LIMSEQ_incseq_SUP by blast
+  then have "p \<noteq> 0"
+    by (metis "1" not_one_le_zero prod_ge_1 LIMSEQ_le_const)
+  with 1 p show ?thesis
+    by (metis convergent_prod_iff_nz_lim not_one_le_zero)
+qed
+
 
 lemma abs_convergent_prod_altdef:
   fixes f :: "nat \<Rightarrow> 'a :: {one,real_normed_vector}"
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Analysis/Starlike.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -454,7 +454,7 @@
   apply (clarsimp simp: midpoint_def in_segment)
   apply (rule_tac x="(1 + u) / 2" in exI)
   apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
-  by (metis real_sum_of_halves scaleR_left.add)
+  by (metis field_sum_of_halves scaleR_left.add)
 
 lemma notin_segment_midpoint:
   fixes a :: "'a :: euclidean_space"
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
--- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -337,13 +337,13 @@
       by (simp add: field_simps)
     have one0: "1 > (0::real)"
       by arith
-    from real_lbound_gt_zero[OF one0 em0]
+    from field_lbound_gt_zero[OF one0 em0]
     obtain d where d: "d > 0" "d < 1" "d < e / m"
       by blast
     from d(1,3) m(1) have dm: "d * m > 0" "d * m < e"
       by (simp_all add: field_simps)
     show ?case
-    proof (rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
+    proof (rule ex_forward[OF field_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
       fix d w
       assume H: "d > 0" "d < 1" "d < e/m" "w \<noteq> z" "norm (w - z) < d"
       then have d1: "norm (w-z) \<le> 1" "d \<ge> 0"
@@ -754,7 +754,7 @@
       have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
         using norm_ge_zero[of w] w0 m(1)
         by (simp add: inverse_eq_divide zero_less_mult_iff)
-      with real_lbound_gt_zero[OF zero_less_one] obtain t where
+      with field_lbound_gt_zero[OF zero_less_one] obtain t where
         t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
       let ?ct = "complex_of_real t"
       let ?w = "?ct * w"
@@ -844,7 +844,7 @@
             m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
           have dm: "cmod d / m > 0"
             using False m(1) by (simp add: field_simps)
-          from real_lbound_gt_zero[OF dm zero_less_one]
+          from field_lbound_gt_zero[OF dm zero_less_one]
           obtain x where x: "x > 0" "x < cmod d / m" "x < 1"
             by blast
           let ?x = "complex_of_real x"
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Deriv.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -1234,7 +1234,7 @@
   obtain d' where d': "0 < d'" and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x - h)"
     by blast
   obtain e where "0 < e \<and> e < d \<and> e < d'"
-    using real_lbound_gt_zero [OF d d']  ..
+    using field_lbound_gt_zero [OF d d']  ..
   with lt le [THEN spec [where x="x - e"]] show ?thesis
     by (auto simp add: abs_if)
 next
@@ -1243,7 +1243,7 @@
   obtain d' where d': "0 < d'" and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)"
     by blast
   obtain e where "0 < e \<and> e < d \<and> e < d'"
-    using real_lbound_gt_zero [OF d d'] ..
+    using field_lbound_gt_zero [OF d d'] ..
   with lt le [THEN spec [where x="x + e"]] show ?thesis
     by (auto simp add: abs_if)
 qed
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Fields.thy
--- a/src/HOL/Fields.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Fields.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -425,17 +425,9 @@
 text\<open>There is a whole bunch of simp-rules just for class \<open>field\<close> but none for class \<open>field\<close> and \<open>nonzero_divides\<close>
 because the latter are covered by a simproc.\<close>
 
-lemma mult_divide_mult_cancel_left:
-  "c \<noteq> 0 \<Longrightarrow> (c * a) / (c * b) = a / b"
-apply (cases "b = 0")
-apply simp_all
-done
+lemmas mult_divide_mult_cancel_left = nonzero_mult_divide_mult_cancel_left
 
-lemma mult_divide_mult_cancel_right:
-  "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
-apply (cases "b = 0")
-apply simp_all
-done
+lemmas mult_divide_mult_cancel_right = nonzero_mult_divide_mult_cancel_right
 
 lemma divide_divide_eq_right [simp]:
   "a / (b / c) = (a * c) / b"
@@ -468,9 +460,7 @@
 
 lemma minus_divide_divide:
   "(- a) / (- b) = a / b"
-apply (cases "b=0", simp)
-apply (simp add: nonzero_minus_divide_divide)
-done
+  by (cases "b=0") (simp_all add: nonzero_minus_divide_divide)
 
 lemma inverse_eq_1_iff [simp]:
   "inverse x = 1 \<longleftrightarrow> x = 1"
@@ -482,21 +472,15 @@
 
 lemma divide_cancel_right [simp]:
   "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
-  apply (cases "c=0", simp)
-  apply (simp add: divide_inverse)
-  done
+  by (cases "c=0") (simp_all add: divide_inverse)
 
 lemma divide_cancel_left [simp]:
   "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b"
-  apply (cases "c=0", simp)
-  apply (simp add: divide_inverse)
-  done
+  by (cases "c=0") (simp_all add: divide_inverse)
 
 lemma divide_eq_1_iff [simp]:
   "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
-  apply (cases "b=0", simp)
-  apply (simp add: right_inverse_eq)
-  done
+  by (cases "b=0") (simp_all add: right_inverse_eq)
 
 lemma one_eq_divide_iff [simp]:
   "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
@@ -521,17 +505,13 @@
 lemma dvd_field_iff:
   "a dvd b \<longleftrightarrow> (a = 0 \<longrightarrow> b = 0)"
 proof (cases "a = 0")
-  case True
-  then show ?thesis
-    by simp
-next
   case False
   then have "b = a * (b / a)"
     by (simp add: field_simps)
   then have "a dvd b" ..
   with False show ?thesis
     by simp
-qed
+qed simp
 
 end
 
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -190,16 +190,6 @@
     done
   done
 
-lemma sum_le_suminf:
-  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
-  shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> sum f I \<le> suminf f"
-  by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
-
-lemma suminf_eq_SUP_real:
-  assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)"
-  by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP)
-     (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono2)
-
 subsection \<open>Defining the extended non-negative reals\<close>
 
 text \<open>Basic definitions and type class setup\<close>
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/List.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -4381,13 +4381,11 @@
 
 lemma rotate_rev:
   "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
-apply(simp add:rotate_drop_take rev_drop rev_take)
-apply(cases "length xs = 0")
- apply simp
-apply(cases "n mod length xs = 0")
- apply simp
-apply(simp add:rotate_drop_take rev_drop rev_take)
-done
+proof (cases "length xs = 0 \<or> n mod length xs = 0")
+  case False
+  then show ?thesis
+    by(simp add:rotate_drop_take rev_drop rev_take)
+qed force
 
 lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
 apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
@@ -4395,6 +4393,9 @@
  prefer 2 apply simp
 using mod_less_divisor[of "length xs" n] by arith
 
+lemma rotate_append: "rotate (length l) (l @ q) = q @ l"
+  by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap)
+
 
 subsubsection \<open>@{const nths} --- a generalization of @{const nth} to sets\<close>
 
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Nonstandard_Analysis/NSA.thy
--- a/src/HOL/Nonstandard_Analysis/NSA.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -273,13 +273,9 @@
 lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal"
   by (simp add: Infinitesimal_def)
 
-lemma hypreal_sum_of_halves: "x / 2 + x / 2 = x"
-  for x :: hypreal
-  by auto
-
 lemma Infinitesimal_add: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x + y \<in> Infinitesimal"
   apply (rule InfinitesimalI)
-  apply (rule hypreal_sum_of_halves [THEN subst])
+  apply (rule field_sum_of_halves [THEN subst])
   apply (drule half_gt_zero)
   apply (blast intro: hnorm_add_less SReal_divide_numeral dest: InfinitesimalD)
   done
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Real.thy
--- a/src/HOL/Real.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Real.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -1383,21 +1383,16 @@
 
 subsection \<open>Density of the Reals\<close>
 
-lemma real_lbound_gt_zero: "0 < d1 \<Longrightarrow> 0 < d2 \<Longrightarrow> \<exists>e. 0 < e \<and> e < d1 \<and> e < d2"
-  for d1 d2 :: real
+lemma field_lbound_gt_zero: "0 < d1 \<Longrightarrow> 0 < d2 \<Longrightarrow> \<exists>e. 0 < e \<and> e < d1 \<and> e < d2"
+  for d1 d2 :: "'a::linordered_field"
   by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def)
 
-text \<open>Similar results are proved in @{theory HOL.Fields}\<close>
-lemma real_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2"
-  for x y :: real
+lemma field_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2"
+  for x y :: "'a::linordered_field"
   by auto
 
-lemma real_gt_half_sum: "x < y \<Longrightarrow> (x + y) / 2 < y"
-  for x y :: real
-  by auto
-
-lemma real_sum_of_halves: "x / 2 + x / 2 = x"
-  for x :: real
+lemma field_sum_of_halves: "x / 2 + x / 2 = x"
+  for x :: "'a::linordered_field"
   by simp
 
 
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Series.thy
--- a/src/HOL/Series.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Series.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -213,11 +213,12 @@
 lemma suminf_le: "\<forall>n. f n \<le> g n \<Longrightarrow> summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f \<le> suminf g"
   by (auto dest: sums_summable intro: sums_le)
 
-lemma sum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> sum f {..<n} \<le> suminf f"
+lemma sum_le_suminf:
+  shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> sum f I \<le> suminf f"
   by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
 
 lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
-  using sum_le_suminf[of 0] by simp
+  using sum_le_suminf by force
 
 lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. sum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   by (metis LIMSEQ_le_const2 summable_LIMSEQ)
@@ -237,7 +238,7 @@
 qed (metis suminf_zero fun_eq_iff)
 
 lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
-  using sum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
+  using sum_le_suminf[of "{}"] suminf_eq_zero_iff by (simp add: less_le)
 
 lemma suminf_pos2:
   assumes "summable f" "\<forall>n. 0 \<le> f n" "0 < f i"
@@ -261,7 +262,7 @@
 
 lemma sum_less_suminf2:
   "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> sum f {..<n} < suminf f"
-  using sum_le_suminf[of f "Suc i"]
+  using sum_le_suminf[of f "{..< Suc i}"]
     and add_strict_increasing[of "f i" "sum f {..<n}" "sum f {..<i}"]
     and sum_mono2[of "{..<i}" "{..<n}" f]
   by (auto simp: less_imp_le ac_simps)
@@ -288,6 +289,11 @@
   for f :: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add,linorder_topology,complete_linorder}"
   by (intro summableI_nonneg_bounded[where x=top] zero_le top_greatest)
 
+lemma suminf_eq_SUP_real:
+  assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)"
+  by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP)
+     (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono2)
+
 
 subsection \<open>Infinite summability on topological monoids\<close>
 
@@ -1116,7 +1122,8 @@
     also have "\<dots> \<le> (\<Sum>i<m. f i)"
       by (rule sum_mono2) (auto simp add: pos n[rule_format])
     also have "\<dots> \<le> suminf f"
-      using \<open>summable f\<close> by (rule sum_le_suminf) (simp add: pos)
+      using \<open>summable f\<close>
+      by (rule sum_le_suminf) (simp_all add: pos)
     finally show "(\<Sum>i<n. (f \<circ>  g) i) \<le> suminf f"
       by simp
   qed
@@ -1151,7 +1158,7 @@
     also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)"
       by (rule sum_mono2)(auto simp add: pos n)
     also have "\<dots> \<le> suminf (f \<circ> g)"
-      using \<open>summable (f \<circ> g)\<close> by (rule sum_le_suminf) (simp add: pos)
+      using \<open>summable (f \<circ> g)\<close> by (rule sum_le_suminf) (simp_all add: pos)
     finally show "sum f {..<n} \<le> suminf (f \<circ> g)" .
   qed
   with le show "suminf (f \<circ> g) = suminf f"
diff -r f5ca4c2157a5 -r 2f4e2aab190a src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Thu Jun 28 10:13:54 2018 +0200
+++ b/src/HOL/Transcendental.thy	Thu Jun 28 14:13:57 2018 +0100
@@ -4643,7 +4643,7 @@
   apply (drule_tac x = "inverse y" in spec)
   apply safe
    apply force
-  apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero])
+  apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] field_lbound_gt_zero])
   apply safe
   apply (rule_tac x = "(pi/2) - e" in exI)
   apply (simp (no_asm_simp))