Generalising and renaming some basic results
authorpaulson <lp15@cam.ac.uk>
Thu Jun 28 14:13:57 2018 +0100 (12 months ago)
changeset 685272f4e2aab190a
parent 68524 f5ca4c2157a5
child 68528 d31e986fbebc
Generalising and renaming some basic results
src/HOL/Analysis/Arcwise_Connected.thy
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Connected.thy
src/HOL/Analysis/Convex_Euclidean_Space.thy
src/HOL/Analysis/Derivative.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Great_Picard.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Analysis/Infinite_Products.thy
src/HOL/Analysis/Starlike.thy
src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy
src/HOL/Deriv.thy
src/HOL/Fields.thy
src/HOL/Library/Extended_Nonnegative_Real.thy
src/HOL/List.thy
src/HOL/Nonstandard_Analysis/NSA.thy
src/HOL/Real.thy
src/HOL/Series.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Arcwise_Connected.thy	Thu Jun 28 10:13:54 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Arcwise_Connected.thy	Thu Jun 28 14:13:57 2018 +0100
     1.3 @@ -1243,7 +1243,7 @@
     1.4          by (metis atLeastAtMost_iff a_ge_0 b_le_1 order.trans)+
     1.5        moreover have "y < \<delta> + c (real m / 2 ^ n)" "c (real m / 2 ^ n) < \<delta> + y"
     1.6          using y apply simp_all
     1.7 -        using alec [of m n] cleb [of m n] n real_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
     1.8 +        using alec [of m n] cleb [of m n] n field_sum_of_halves close_ab [OF \<open>odd m\<close>, of n]
     1.9          by linarith+
    1.10        moreover note \<open>0 < m\<close> mless \<open>0 \<le> x\<close> \<open>x \<le> 1\<close>
    1.11        ultimately show "\<exists>k. \<exists>m\<in>{0<..<2 ^ k}. dist (h (real m / 2 ^ k)) (f x) < e"
     2.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Jun 28 10:13:54 2018 +0200
     2.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Jun 28 14:13:57 2018 +0100
     2.3 @@ -283,7 +283,7 @@
     2.4        have x2: "(x + 1) / 2 \<notin> S"
     2.5          using that
     2.6          apply (clarsimp simp: image_iff)
     2.7 -        by (metis add.commute add_diff_cancel_left' mult_2 real_sum_of_halves)
     2.8 +        by (metis add.commute add_diff_cancel_left' mult_2 field_sum_of_halves)
     2.9        have "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
    2.10          by (rule differentiable_chain_within differentiable_subset [OF S [of "(x+1)/2"]] | use x2 that in force)+
    2.11        then show "g1 +++ g2 \<circ> (\<lambda>x. (x+1) / 2) differentiable at x within {0..1}"
    2.12 @@ -6161,7 +6161,7 @@
    2.13    obtain r where "r > 0" and holfc: "f holomorphic_on cball z r" and w: "w \<in> ball z r"
    2.14    proof
    2.15      have "cball z ((r + dist w z) / 2) \<subseteq> ball z r"
    2.16 -      using w by (simp add: dist_commute real_sum_of_halves subset_eq)
    2.17 +      using w by (simp add: dist_commute field_sum_of_halves subset_eq)
    2.18      then show "f holomorphic_on cball z ((r + dist w z) / 2)"
    2.19        by (rule holomorphic_on_subset [OF holf])
    2.20      have "r > 0"
     3.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Jun 28 10:13:54 2018 +0200
     3.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Jun 28 14:13:57 2018 +0100
     3.3 @@ -1575,6 +1575,55 @@
     3.4  
     3.5  text\<open>Finally the Argument is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\<close>
     3.6  
     3.7 +lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
     3.8 +  by (simp add: Im_Ln_eq_pi Arg_def)
     3.9 +
    3.10 +lemma mpi_less_Arg: "-pi < Arg z"
    3.11 +    and Arg_le_pi: "Arg z \<le> pi"
    3.12 +  by (auto simp: Arg_def mpi_less_Im_Ln Im_Ln_le_pi)
    3.13 +
    3.14 +lemma
    3.15 +  assumes "z \<noteq> 0"
    3.16 +  shows Arg_eq: "z = of_real(norm z) * exp(\<i> * Arg z)"
    3.17 +  using assms exp_Ln exp_eq_polar
    3.18 +  by (auto simp:  Arg_def)
    3.19 +
    3.20 +lemma Argument_exists:
    3.21 +  assumes "z \<noteq> 0" and R: "R = {r-pi<..r+pi}"
    3.22 +  obtains s where "is_Arg z s" "s\<in>R"
    3.23 +proof -
    3.24 +  let ?rp = "r - Arg z + pi"
    3.25 +  define k where "k \<equiv> \<lfloor>?rp / (2 * pi)\<rfloor>"
    3.26 +  have "(Arg z + of_int k * (2 * pi)) \<in> R"
    3.27 +    using floor_divide_lower [of "2*pi" ?rp] floor_divide_upper [of "2*pi" ?rp]
    3.28 +    by (auto simp: k_def algebra_simps R)
    3.29 +  then show ?thesis
    3.30 +    using Arg_eq \<open>z \<noteq> 0\<close> is_Arg_2pi_iff is_Arg_def that by blast
    3.31 +qed
    3.32 +
    3.33 +lemma Argument_exists_unique:
    3.34 +  assumes "z \<noteq> 0" and R: "R = {r-pi<..r+pi}"
    3.35 +  obtains s where "is_Arg z s" "s\<in>R" "\<And>t. \<lbrakk>is_Arg z t; t\<in>R\<rbrakk> \<Longrightarrow> s=t"
    3.36 +proof -
    3.37 +  obtain s where s: "is_Arg z s" "s\<in>R"
    3.38 +    using Argument_exists [OF assms] .
    3.39 +  moreover have "\<And>t. \<lbrakk>is_Arg z t; t\<in>R\<rbrakk> \<Longrightarrow> s=t"
    3.40 +    using assms s  by (auto simp: is_Arg_eqI)
    3.41 +  ultimately show thesis
    3.42 +    using that by blast
    3.43 +qed
    3.44 +
    3.45 +lemma Argument_Ex1:
    3.46 +  assumes "z \<noteq> 0" and R: "R = {r-pi<..r+pi}"
    3.47 +  shows "\<exists>!s. is_Arg z s \<and> s \<in> R"
    3.48 +  using Argument_exists_unique [OF assms]  by metis
    3.49 +
    3.50 +lemma Arg_divide:
    3.51 +  assumes "w \<noteq> 0" "z \<noteq> 0"
    3.52 +  shows "is_Arg (z / w) (Arg z - Arg w)"
    3.53 +  using Arg_eq [of z] Arg_eq [of w] Arg_eq [of "norm(z / w)"] assms
    3.54 +  by (auto simp: is_Arg_def norm_divide field_simps exp_diff Arg_of_real)
    3.55 +
    3.56  lemma Arg_unique_lemma:
    3.57    assumes z:  "is_Arg z t"
    3.58        and z': "is_Arg z t'"
    3.59 @@ -1603,14 +1652,6 @@
    3.60      by simp
    3.61  qed
    3.62  
    3.63 -lemma
    3.64 -  assumes "z \<noteq> 0"
    3.65 -  shows mpi_less_Arg: "-pi < Arg z"
    3.66 -    and Arg_le_pi: "Arg z \<le> pi"
    3.67 -    and Arg_eq: "z = of_real(norm z) * exp(\<i> * Arg z)"
    3.68 -  using assms exp_Ln exp_eq_polar
    3.69 -  by (auto simp: mpi_less_Im_Ln Im_Ln_le_pi Arg_def)
    3.70 -
    3.71  lemma complex_norm_eq_1_exp_eq: "norm z = 1 \<longleftrightarrow> exp(\<i> * (Arg z)) = z"
    3.72    by (metis Arg_eq exp_not_eq_zero exp_zero mult.left_neutral norm_zero of_real_1 norm_exp_i_times)
    3.73  
    3.74 @@ -1618,7 +1659,6 @@
    3.75    by (rule Arg_unique_lemma [unfolded is_Arg_def, OF _ Arg_eq])
    3.76       (use mpi_less_Arg Arg_le_pi in \<open>auto simp: norm_mult\<close>)
    3.77  
    3.78 -
    3.79  lemma Arg_minus:
    3.80    assumes "z \<noteq> 0"
    3.81    shows "Arg (-z) = (if Arg z \<le> 0 then Arg z + pi else Arg z - pi)"
    3.82 @@ -1671,9 +1711,6 @@
    3.83  corollary Arg_ne_0: assumes "z \<notin> \<real>\<^sub>\<ge>\<^sub>0" shows "Arg z \<noteq> 0"
    3.84    using assms by (auto simp: nonneg_Reals_def Arg_eq_0)
    3.85  
    3.86 -lemma Arg_of_real: "Arg (of_real r) = (if r<0 then pi else 0)"
    3.87 -  by (simp add: Im_Ln_eq_pi Arg_def)
    3.88 -
    3.89  lemma Arg_eq_pi_iff: "Arg z = pi \<longleftrightarrow> z \<in> \<real> \<and> Re z < 0"
    3.90  proof (cases "z=0")
    3.91    case False
    3.92 @@ -1695,7 +1732,7 @@
    3.93  next
    3.94    case False
    3.95    then have "Arg z < pi" "z \<noteq> 0"
    3.96 -    using Arg_def Arg_eq_0_pi Arg_le_pi by fastforce+
    3.97 +    using Arg_eq_0_pi Arg_le_pi by (auto simp: less_eq_real_def)
    3.98    then show ?thesis
    3.99      apply (simp add: False)
   3.100      apply (rule Arg_unique [of "inverse (norm z)"])
     4.1 --- a/src/HOL/Analysis/Connected.thy	Thu Jun 28 10:13:54 2018 +0200
     4.2 +++ b/src/HOL/Analysis/Connected.thy	Thu Jun 28 14:13:57 2018 +0100
     4.3 @@ -2871,7 +2871,7 @@
     4.4      then obtain C where C: "x \<in> C" "C \<in> \<C>"
     4.5        using \<open>S \<subseteq> \<Union>\<C>\<close> by blast
     4.6      then obtain r where r: "r>0" "ball x (2*r) \<subseteq> C"
     4.7 -      by (metis mult.commute mult_2_right not_le ope openE real_sum_of_halves zero_le_numeral zero_less_mult_iff)
     4.8 +      by (metis mult.commute mult_2_right not_le ope openE field_sum_of_halves zero_le_numeral zero_less_mult_iff)
     4.9      then have "\<exists>r C. r > 0 \<and> ball x (2*r) \<subseteq> C \<and> C \<in> \<C>"
    4.10        using C by blast
    4.11    }
     5.1 --- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Jun 28 10:13:54 2018 +0200
     5.2 +++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Jun 28 14:13:57 2018 +0100
     5.3 @@ -2234,7 +2234,7 @@
     5.4    then obtain y where "y\<in>s" and y: "f x > f y" by auto
     5.5    then have xy: "0 < dist x y"  by auto
     5.6    then obtain u where "0 < u" "u \<le> 1" and u: "u < e / dist x y"
     5.7 -    using real_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
     5.8 +    using field_lbound_gt_zero[of 1 "e / dist x y"] xy \<open>e>0\<close> by auto
     5.9    then have "f ((1-u) *\<^sub>R x + u *\<^sub>R y) \<le> (1-u) * f x + u * f y"
    5.10      using \<open>x\<in>s\<close> \<open>y\<in>s\<close>
    5.11      using assms(2)[unfolded convex_on_def,
    5.12 @@ -5052,7 +5052,7 @@
    5.13        next
    5.14          assume "u \<noteq> 0" "v \<noteq> 0"
    5.15          then obtain w where w: "w>0" "w<u" "w<v"
    5.16 -          using real_lbound_gt_zero[of u v] and obt(1,2) by auto
    5.17 +          using field_lbound_gt_zero[of u v] and obt(1,2) by auto
    5.18          have "x \<noteq> b"
    5.19          proof
    5.20            assume "x = b"
     6.1 --- a/src/HOL/Analysis/Derivative.thy	Thu Jun 28 10:13:54 2018 +0200
     6.2 +++ b/src/HOL/Analysis/Derivative.thy	Thu Jun 28 14:13:57 2018 +0100
     6.3 @@ -1132,7 +1132,7 @@
     6.4      obtain d2 where "0 < d2" and d2: "\<And>u. dist u y < d2 \<Longrightarrow> u \<in> T"
     6.5        using \<open>open T\<close> \<open>y \<in> T\<close> unfolding open_dist by blast
     6.6      obtain d where d: "0 < d" "d < d1" "d < d2"
     6.7 -      using real_lbound_gt_zero[OF \<open>0 < d1\<close> \<open>0 < d2\<close>] by blast
     6.8 +      using field_lbound_gt_zero[OF \<open>0 < d1\<close> \<open>0 < d2\<close>] by blast
     6.9      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)"
    6.10      proof (intro exI allI impI conjI)
    6.11        fix z
    6.12 @@ -1188,7 +1188,7 @@
    6.13          "\<And>z. norm (z - y) < d' \<Longrightarrow> norm (g z - g y - g' (z - y)) \<le> e / B * norm (g z - g y)"
    6.14        using lem1 * by blast
    6.15      obtain k where k: "0 < k" "k < d" "k < d'"
    6.16 -      using real_lbound_gt_zero[OF \<open>0 < d\<close> \<open>0 < d'\<close>] by blast
    6.17 +      using field_lbound_gt_zero[OF \<open>0 < d\<close> \<open>0 < d'\<close>] by blast
    6.18      show "\<exists>d>0. \<forall>ya. norm (ya - y) < d \<longrightarrow> norm (g ya - g y - g' (ya - y)) \<le> e * norm (ya - y)"
    6.19      proof (intro exI allI impI conjI)
    6.20        fix z
    6.21 @@ -1331,7 +1331,7 @@
    6.22      using mem_interior_cball x by blast
    6.23    have *: "0 < e0 / B" "0 < e1 / B" using e0 e1 B by auto
    6.24    obtain e where e: "0 < e" "e < e0 / B" "e < e1 / B"
    6.25 -    using real_lbound_gt_zero[OF *] by blast
    6.26 +    using field_lbound_gt_zero[OF *] by blast
    6.27    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
    6.28    proof (rule brouwer_surjective_cball)
    6.29      have z: "z \<in> S" if as: "y \<in>cball (f x) e" "z = x + (g' y - g' (f x))" for y z
    6.30 @@ -1544,7 +1544,7 @@
    6.31    obtain d2 where d2: "0 < d2" "ball a d2 \<subseteq> S"
    6.32      using \<open>0 < d2\<close> \<open>ball a d2 \<subseteq> S\<close> by blast
    6.33    obtain d where d: "0 < d" "d < d1" "d < d2"
    6.34 -    using real_lbound_gt_zero[OF d1(1) d2(1)] by blast
    6.35 +    using field_lbound_gt_zero[OF d1(1) d2(1)] by blast
    6.36    show ?thesis
    6.37    proof
    6.38      show "0 < d" by (fact d)
     7.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Jun 28 10:13:54 2018 +0200
     7.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Jun 28 14:13:57 2018 +0100
     7.3 @@ -1371,7 +1371,7 @@
     7.4      by (metis dual_order.strict_implies_order negligible_imp_measurable negligible_imp_measure0 order_refl)
     7.5  next
     7.6    assume ?rhs then show "negligible S"
     7.7 -    by (metis le_less_trans negligible_outer real_lbound_gt_zero)
     7.8 +    by (metis le_less_trans negligible_outer field_lbound_gt_zero)
     7.9  qed
    7.10  
    7.11  lemma negligible_UNIV: "negligible S \<longleftrightarrow> (indicat_real S has_integral 0) UNIV" (is "_=?rhs")
     8.1 --- a/src/HOL/Analysis/Great_Picard.thy	Thu Jun 28 10:13:54 2018 +0200
     8.2 +++ b/src/HOL/Analysis/Great_Picard.thy	Thu Jun 28 14:13:57 2018 +0100
     8.3 @@ -1209,7 +1209,7 @@
     8.4          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"
     8.5            using eventually_conj [OF K z1]
     8.6            apply (rule eventually_mono)
     8.7 -          by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half real_sum_of_halves)
     8.8 +          by (metis (no_types, hide_lams) diff_add_eq diff_diff_eq2 dist_commute dist_norm dist_triangle_add_half field_sum_of_halves)
     8.9          then
    8.10          show "\<forall>\<^sub>F n in sequentially. \<forall>x\<in>K. dist (\<F> n x - \<F> n z1) (g x - g z1) < e"
    8.11            by simp
     9.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Jun 28 10:13:54 2018 +0200
     9.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Jun 28 14:13:57 2018 +0100
     9.3 @@ -7086,7 +7086,7 @@
     9.4                  \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX/2"
     9.5          by (simp only: integral_diff [symmetric] int_integrable integrable_const)
     9.6        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
     9.7 -        using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] real_sum_of_halves
     9.8 +        using norm_triangle_mono [of "x-y'" "e/2" "y'-y" "e/2"] field_sum_of_halves
     9.9          by (simp add: norm_minus_commute)
    9.10        have "norm (integral (cbox (u,w) (v,z)) f - integral (cbox u v) (\<lambda>x. integral (cbox w z) (\<lambda>y. f (x,y))))
    9.11              \<le> e * content (cbox (u,w) (v,z)) / content ?CBOX"
    10.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Thu Jun 28 10:13:54 2018 +0200
    10.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Thu Jun 28 14:13:57 2018 +0100
    10.3 @@ -226,6 +226,23 @@
    10.4    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"
    10.5    by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)
    10.6  
    10.7 +lemma bounded_imp_convergent_prod:
    10.8 +  fixes a :: "nat \<Rightarrow> real"
    10.9 +  assumes 1: "\<And>n. a n \<ge> 1" and bounded: "\<And>n. (\<Prod>i\<le>n. a i) \<le> B"
   10.10 +  shows "convergent_prod a"
   10.11 +proof -
   10.12 +  have "bdd_above (range(\<lambda>n. \<Prod>i\<le>n. a i))"
   10.13 +    by (meson bdd_aboveI2 bounded)
   10.14 +  moreover have "incseq (\<lambda>n. \<Prod>i\<le>n. a i)"
   10.15 +    unfolding mono_def by (metis 1 prod_mono2 atMost_subset_iff dual_order.trans finite_atMost zero_le_one)
   10.16 +  ultimately obtain p where p: "(\<lambda>n. \<Prod>i\<le>n. a i) \<longlonglongrightarrow> p"
   10.17 +    using LIMSEQ_incseq_SUP by blast
   10.18 +  then have "p \<noteq> 0"
   10.19 +    by (metis "1" not_one_le_zero prod_ge_1 LIMSEQ_le_const)
   10.20 +  with 1 p show ?thesis
   10.21 +    by (metis convergent_prod_iff_nz_lim not_one_le_zero)
   10.22 +qed
   10.23 +
   10.24  
   10.25  lemma abs_convergent_prod_altdef:
   10.26    fixes f :: "nat \<Rightarrow> 'a :: {one,real_normed_vector}"
    11.1 --- a/src/HOL/Analysis/Starlike.thy	Thu Jun 28 10:13:54 2018 +0200
    11.2 +++ b/src/HOL/Analysis/Starlike.thy	Thu Jun 28 14:13:57 2018 +0100
    11.3 @@ -454,7 +454,7 @@
    11.4    apply (clarsimp simp: midpoint_def in_segment)
    11.5    apply (rule_tac x="(1 + u) / 2" in exI)
    11.6    apply (auto simp: algebra_simps add_divide_distrib diff_divide_distrib)
    11.7 -  by (metis real_sum_of_halves scaleR_left.add)
    11.8 +  by (metis field_sum_of_halves scaleR_left.add)
    11.9  
   11.10  lemma notin_segment_midpoint:
   11.11    fixes a :: "'a :: euclidean_space"
    12.1 --- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Thu Jun 28 10:13:54 2018 +0200
    12.2 +++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy	Thu Jun 28 14:13:57 2018 +0100
    12.3 @@ -337,13 +337,13 @@
    12.4        by (simp add: field_simps)
    12.5      have one0: "1 > (0::real)"
    12.6        by arith
    12.7 -    from real_lbound_gt_zero[OF one0 em0]
    12.8 +    from field_lbound_gt_zero[OF one0 em0]
    12.9      obtain d where d: "d > 0" "d < 1" "d < e / m"
   12.10        by blast
   12.11      from d(1,3) m(1) have dm: "d * m > 0" "d * m < e"
   12.12        by (simp_all add: field_simps)
   12.13      show ?case
   12.14 -    proof (rule ex_forward[OF real_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
   12.15 +    proof (rule ex_forward[OF field_lbound_gt_zero[OF one0 em0]], clarsimp simp add: norm_mult)
   12.16        fix d w
   12.17        assume H: "d > 0" "d < 1" "d < e/m" "w \<noteq> z" "norm (w - z) < d"
   12.18        then have d1: "norm (w-z) \<le> 1" "d \<ge> 0"
   12.19 @@ -754,7 +754,7 @@
   12.20        have inv0: "0 < inverse (cmod w ^ (k + 1) * m)"
   12.21          using norm_ge_zero[of w] w0 m(1)
   12.22          by (simp add: inverse_eq_divide zero_less_mult_iff)
   12.23 -      with real_lbound_gt_zero[OF zero_less_one] obtain t where
   12.24 +      with field_lbound_gt_zero[OF zero_less_one] obtain t where
   12.25          t: "t > 0" "t < 1" "t < inverse (cmod w ^ (k + 1) * m)" by blast
   12.26        let ?ct = "complex_of_real t"
   12.27        let ?w = "?ct * w"
   12.28 @@ -844,7 +844,7 @@
   12.29              m: "m > 0" "\<forall>z. \<forall>z. cmod z \<le> 1 \<longrightarrow> cmod (poly ds z) \<le> m" by blast
   12.30            have dm: "cmod d / m > 0"
   12.31              using False m(1) by (simp add: field_simps)
   12.32 -          from real_lbound_gt_zero[OF dm zero_less_one]
   12.33 +          from field_lbound_gt_zero[OF dm zero_less_one]
   12.34            obtain x where x: "x > 0" "x < cmod d / m" "x < 1"
   12.35              by blast
   12.36            let ?x = "complex_of_real x"
    13.1 --- a/src/HOL/Deriv.thy	Thu Jun 28 10:13:54 2018 +0200
    13.2 +++ b/src/HOL/Deriv.thy	Thu Jun 28 14:13:57 2018 +0100
    13.3 @@ -1234,7 +1234,7 @@
    13.4    obtain d' where d': "0 < d'" and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x - h)"
    13.5      by blast
    13.6    obtain e where "0 < e \<and> e < d \<and> e < d'"
    13.7 -    using real_lbound_gt_zero [OF d d']  ..
    13.8 +    using field_lbound_gt_zero [OF d d']  ..
    13.9    with lt le [THEN spec [where x="x - e"]] show ?thesis
   13.10      by (auto simp add: abs_if)
   13.11  next
   13.12 @@ -1243,7 +1243,7 @@
   13.13    obtain d' where d': "0 < d'" and lt: "\<forall>h > 0. h < d' \<longrightarrow> f x < f (x + h)"
   13.14      by blast
   13.15    obtain e where "0 < e \<and> e < d \<and> e < d'"
   13.16 -    using real_lbound_gt_zero [OF d d'] ..
   13.17 +    using field_lbound_gt_zero [OF d d'] ..
   13.18    with lt le [THEN spec [where x="x + e"]] show ?thesis
   13.19      by (auto simp add: abs_if)
   13.20  qed
    14.1 --- a/src/HOL/Fields.thy	Thu Jun 28 10:13:54 2018 +0200
    14.2 +++ b/src/HOL/Fields.thy	Thu Jun 28 14:13:57 2018 +0100
    14.3 @@ -425,17 +425,9 @@
    14.4  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>
    14.5  because the latter are covered by a simproc.\<close>
    14.6  
    14.7 -lemma mult_divide_mult_cancel_left:
    14.8 -  "c \<noteq> 0 \<Longrightarrow> (c * a) / (c * b) = a / b"
    14.9 -apply (cases "b = 0")
   14.10 -apply simp_all
   14.11 -done
   14.12 +lemmas mult_divide_mult_cancel_left = nonzero_mult_divide_mult_cancel_left
   14.13  
   14.14 -lemma mult_divide_mult_cancel_right:
   14.15 -  "c \<noteq> 0 \<Longrightarrow> (a * c) / (b * c) = a / b"
   14.16 -apply (cases "b = 0")
   14.17 -apply simp_all
   14.18 -done
   14.19 +lemmas mult_divide_mult_cancel_right = nonzero_mult_divide_mult_cancel_right
   14.20  
   14.21  lemma divide_divide_eq_right [simp]:
   14.22    "a / (b / c) = (a * c) / b"
   14.23 @@ -468,9 +460,7 @@
   14.24  
   14.25  lemma minus_divide_divide:
   14.26    "(- a) / (- b) = a / b"
   14.27 -apply (cases "b=0", simp)
   14.28 -apply (simp add: nonzero_minus_divide_divide)
   14.29 -done
   14.30 +  by (cases "b=0") (simp_all add: nonzero_minus_divide_divide)
   14.31  
   14.32  lemma inverse_eq_1_iff [simp]:
   14.33    "inverse x = 1 \<longleftrightarrow> x = 1"
   14.34 @@ -482,21 +472,15 @@
   14.35  
   14.36  lemma divide_cancel_right [simp]:
   14.37    "a / c = b / c \<longleftrightarrow> c = 0 \<or> a = b"
   14.38 -  apply (cases "c=0", simp)
   14.39 -  apply (simp add: divide_inverse)
   14.40 -  done
   14.41 +  by (cases "c=0") (simp_all add: divide_inverse)
   14.42  
   14.43  lemma divide_cancel_left [simp]:
   14.44    "c / a = c / b \<longleftrightarrow> c = 0 \<or> a = b"
   14.45 -  apply (cases "c=0", simp)
   14.46 -  apply (simp add: divide_inverse)
   14.47 -  done
   14.48 +  by (cases "c=0") (simp_all add: divide_inverse)
   14.49  
   14.50  lemma divide_eq_1_iff [simp]:
   14.51    "a / b = 1 \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   14.52 -  apply (cases "b=0", simp)
   14.53 -  apply (simp add: right_inverse_eq)
   14.54 -  done
   14.55 +  by (cases "b=0") (simp_all add: right_inverse_eq)
   14.56  
   14.57  lemma one_eq_divide_iff [simp]:
   14.58    "1 = a / b \<longleftrightarrow> b \<noteq> 0 \<and> a = b"
   14.59 @@ -521,17 +505,13 @@
   14.60  lemma dvd_field_iff:
   14.61    "a dvd b \<longleftrightarrow> (a = 0 \<longrightarrow> b = 0)"
   14.62  proof (cases "a = 0")
   14.63 -  case True
   14.64 -  then show ?thesis
   14.65 -    by simp
   14.66 -next
   14.67    case False
   14.68    then have "b = a * (b / a)"
   14.69      by (simp add: field_simps)
   14.70    then have "a dvd b" ..
   14.71    with False show ?thesis
   14.72      by simp
   14.73 -qed
   14.74 +qed simp
   14.75  
   14.76  end
   14.77  
    15.1 --- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jun 28 10:13:54 2018 +0200
    15.2 +++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Thu Jun 28 14:13:57 2018 +0100
    15.3 @@ -190,16 +190,6 @@
    15.4      done
    15.5    done
    15.6  
    15.7 -lemma sum_le_suminf:
    15.8 -  fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
    15.9 -  shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> sum f I \<le> suminf f"
   15.10 -  by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
   15.11 -
   15.12 -lemma suminf_eq_SUP_real:
   15.13 -  assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)"
   15.14 -  by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP)
   15.15 -     (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono2)
   15.16 -
   15.17  subsection \<open>Defining the extended non-negative reals\<close>
   15.18  
   15.19  text \<open>Basic definitions and type class setup\<close>
    16.1 --- a/src/HOL/List.thy	Thu Jun 28 10:13:54 2018 +0200
    16.2 +++ b/src/HOL/List.thy	Thu Jun 28 14:13:57 2018 +0100
    16.3 @@ -4381,13 +4381,11 @@
    16.4  
    16.5  lemma rotate_rev:
    16.6    "rotate n (rev xs) = rev(rotate (length xs - (n mod length xs)) xs)"
    16.7 -apply(simp add:rotate_drop_take rev_drop rev_take)
    16.8 -apply(cases "length xs = 0")
    16.9 - apply simp
   16.10 -apply(cases "n mod length xs = 0")
   16.11 - apply simp
   16.12 -apply(simp add:rotate_drop_take rev_drop rev_take)
   16.13 -done
   16.14 +proof (cases "length xs = 0 \<or> n mod length xs = 0")
   16.15 +  case False
   16.16 +  then show ?thesis
   16.17 +    by(simp add:rotate_drop_take rev_drop rev_take)
   16.18 +qed force
   16.19  
   16.20  lemma hd_rotate_conv_nth: "xs \<noteq> [] \<Longrightarrow> hd(rotate n xs) = xs!(n mod length xs)"
   16.21  apply(simp add:rotate_drop_take hd_append hd_drop_conv_nth hd_conv_nth)
   16.22 @@ -4395,6 +4393,9 @@
   16.23   prefer 2 apply simp
   16.24  using mod_less_divisor[of "length xs" n] by arith
   16.25  
   16.26 +lemma rotate_append: "rotate (length l) (l @ q) = q @ l"
   16.27 +  by (induct l arbitrary: q) (auto simp add: rotate1_rotate_swap)
   16.28 +
   16.29  
   16.30  subsubsection \<open>@{const nths} --- a generalization of @{const nth} to sets\<close>
   16.31  
    17.1 --- a/src/HOL/Nonstandard_Analysis/NSA.thy	Thu Jun 28 10:13:54 2018 +0200
    17.2 +++ b/src/HOL/Nonstandard_Analysis/NSA.thy	Thu Jun 28 14:13:57 2018 +0100
    17.3 @@ -273,13 +273,9 @@
    17.4  lemma Infinitesimal_zero [iff]: "0 \<in> Infinitesimal"
    17.5    by (simp add: Infinitesimal_def)
    17.6  
    17.7 -lemma hypreal_sum_of_halves: "x / 2 + x / 2 = x"
    17.8 -  for x :: hypreal
    17.9 -  by auto
   17.10 -
   17.11  lemma Infinitesimal_add: "x \<in> Infinitesimal \<Longrightarrow> y \<in> Infinitesimal \<Longrightarrow> x + y \<in> Infinitesimal"
   17.12    apply (rule InfinitesimalI)
   17.13 -  apply (rule hypreal_sum_of_halves [THEN subst])
   17.14 +  apply (rule field_sum_of_halves [THEN subst])
   17.15    apply (drule half_gt_zero)
   17.16    apply (blast intro: hnorm_add_less SReal_divide_numeral dest: InfinitesimalD)
   17.17    done
    18.1 --- a/src/HOL/Real.thy	Thu Jun 28 10:13:54 2018 +0200
    18.2 +++ b/src/HOL/Real.thy	Thu Jun 28 14:13:57 2018 +0100
    18.3 @@ -1383,21 +1383,16 @@
    18.4  
    18.5  subsection \<open>Density of the Reals\<close>
    18.6  
    18.7 -lemma real_lbound_gt_zero: "0 < d1 \<Longrightarrow> 0 < d2 \<Longrightarrow> \<exists>e. 0 < e \<and> e < d1 \<and> e < d2"
    18.8 -  for d1 d2 :: real
    18.9 +lemma field_lbound_gt_zero: "0 < d1 \<Longrightarrow> 0 < d2 \<Longrightarrow> \<exists>e. 0 < e \<and> e < d1 \<and> e < d2"
   18.10 +  for d1 d2 :: "'a::linordered_field"
   18.11    by (rule exI [where x = "min d1 d2 / 2"]) (simp add: min_def)
   18.12  
   18.13 -text \<open>Similar results are proved in @{theory HOL.Fields}\<close>
   18.14 -lemma real_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2"
   18.15 -  for x y :: real
   18.16 +lemma field_less_half_sum: "x < y \<Longrightarrow> x < (x + y) / 2"
   18.17 +  for x y :: "'a::linordered_field"
   18.18    by auto
   18.19  
   18.20 -lemma real_gt_half_sum: "x < y \<Longrightarrow> (x + y) / 2 < y"
   18.21 -  for x y :: real
   18.22 -  by auto
   18.23 -
   18.24 -lemma real_sum_of_halves: "x / 2 + x / 2 = x"
   18.25 -  for x :: real
   18.26 +lemma field_sum_of_halves: "x / 2 + x / 2 = x"
   18.27 +  for x :: "'a::linordered_field"
   18.28    by simp
   18.29  
   18.30  
    19.1 --- a/src/HOL/Series.thy	Thu Jun 28 10:13:54 2018 +0200
    19.2 +++ b/src/HOL/Series.thy	Thu Jun 28 14:13:57 2018 +0100
    19.3 @@ -213,11 +213,12 @@
    19.4  lemma suminf_le: "\<forall>n. f n \<le> g n \<Longrightarrow> summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f \<le> suminf g"
    19.5    by (auto dest: sums_summable intro: sums_le)
    19.6  
    19.7 -lemma sum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> sum f {..<n} \<le> suminf f"
    19.8 +lemma sum_le_suminf:
    19.9 +  shows "summable f \<Longrightarrow> finite I \<Longrightarrow> \<forall>m\<in>- I. 0 \<le> f m \<Longrightarrow> sum f I \<le> suminf f"
   19.10    by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
   19.11  
   19.12  lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
   19.13 -  using sum_le_suminf[of 0] by simp
   19.14 +  using sum_le_suminf by force
   19.15  
   19.16  lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. sum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
   19.17    by (metis LIMSEQ_le_const2 summable_LIMSEQ)
   19.18 @@ -237,7 +238,7 @@
   19.19  qed (metis suminf_zero fun_eq_iff)
   19.20  
   19.21  lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
   19.22 -  using sum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
   19.23 +  using sum_le_suminf[of "{}"] suminf_eq_zero_iff by (simp add: less_le)
   19.24  
   19.25  lemma suminf_pos2:
   19.26    assumes "summable f" "\<forall>n. 0 \<le> f n" "0 < f i"
   19.27 @@ -261,7 +262,7 @@
   19.28  
   19.29  lemma sum_less_suminf2:
   19.30    "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"
   19.31 -  using sum_le_suminf[of f "Suc i"]
   19.32 +  using sum_le_suminf[of f "{..< Suc i}"]
   19.33      and add_strict_increasing[of "f i" "sum f {..<n}" "sum f {..<i}"]
   19.34      and sum_mono2[of "{..<i}" "{..<n}" f]
   19.35    by (auto simp: less_imp_le ac_simps)
   19.36 @@ -288,6 +289,11 @@
   19.37    for f :: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add,linorder_topology,complete_linorder}"
   19.38    by (intro summableI_nonneg_bounded[where x=top] zero_le top_greatest)
   19.39  
   19.40 +lemma suminf_eq_SUP_real:
   19.41 +  assumes X: "summable X" "\<And>i. 0 \<le> X i" shows "suminf X = (SUP i. \<Sum>n<i. X n::real)"
   19.42 +  by (intro LIMSEQ_unique[OF summable_LIMSEQ] X LIMSEQ_incseq_SUP)
   19.43 +     (auto intro!: bdd_aboveI2[where M="\<Sum>i. X i"] sum_le_suminf X monoI sum_mono2)
   19.44 +
   19.45  
   19.46  subsection \<open>Infinite summability on topological monoids\<close>
   19.47  
   19.48 @@ -1116,7 +1122,8 @@
   19.49      also have "\<dots> \<le> (\<Sum>i<m. f i)"
   19.50        by (rule sum_mono2) (auto simp add: pos n[rule_format])
   19.51      also have "\<dots> \<le> suminf f"
   19.52 -      using \<open>summable f\<close> by (rule sum_le_suminf) (simp add: pos)
   19.53 +      using \<open>summable f\<close>
   19.54 +      by (rule sum_le_suminf) (simp_all add: pos)
   19.55      finally show "(\<Sum>i<n. (f \<circ>  g) i) \<le> suminf f"
   19.56        by simp
   19.57    qed
   19.58 @@ -1151,7 +1158,7 @@
   19.59      also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)"
   19.60        by (rule sum_mono2)(auto simp add: pos n)
   19.61      also have "\<dots> \<le> suminf (f \<circ> g)"
   19.62 -      using \<open>summable (f \<circ> g)\<close> by (rule sum_le_suminf) (simp add: pos)
   19.63 +      using \<open>summable (f \<circ> g)\<close> by (rule sum_le_suminf) (simp_all add: pos)
   19.64      finally show "sum f {..<n} \<le> suminf (f \<circ> g)" .
   19.65    qed
   19.66    with le show "suminf (f \<circ> g) = suminf f"
    20.1 --- a/src/HOL/Transcendental.thy	Thu Jun 28 10:13:54 2018 +0200
    20.2 +++ b/src/HOL/Transcendental.thy	Thu Jun 28 14:13:57 2018 +0100
    20.3 @@ -4643,7 +4643,7 @@
    20.4    apply (drule_tac x = "inverse y" in spec)
    20.5    apply safe
    20.6     apply force
    20.7 -  apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] real_lbound_gt_zero])
    20.8 +  apply (drule_tac ?d1.0 = s in pi_half_gt_zero [THEN [2] field_lbound_gt_zero])
    20.9    apply safe
   20.10    apply (rule_tac x = "(pi/2) - e" in exI)
   20.11    apply (simp (no_asm_simp))