--- a/src/HOL/Analysis/Arcwise_Connected.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Thu Jun 28 14:14:05 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"
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Thu Jun 28 14:14:05 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"
--- a/src/HOL/Analysis/Complex_Transcendental.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Thu Jun 28 14:14:05 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)"])
--- a/src/HOL/Analysis/Connected.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Connected.thy Thu Jun 28 14:14:05 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
}
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Thu Jun 28 14:14:05 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"
--- a/src/HOL/Analysis/Derivative.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy Thu Jun 28 14:14:05 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)
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Thu Jun 28 14:14:05 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")
--- a/src/HOL/Analysis/Great_Picard.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy Thu Jun 28 14:14:05 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
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Thu Jun 28 14:14:05 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"
--- a/src/HOL/Analysis/Infinite_Products.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Thu Jun 28 14:14:05 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}"
--- a/src/HOL/Analysis/Starlike.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Analysis/Starlike.thy Thu Jun 28 14:14:05 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"
--- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Thu Jun 28 14:14:05 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"
--- a/src/HOL/Deriv.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Deriv.thy Thu Jun 28 14:14:05 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
--- a/src/HOL/Fields.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Fields.thy Thu Jun 28 14:14:05 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
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Thu Jun 28 14:14:05 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>
--- a/src/HOL/List.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/List.thy Thu Jun 28 14:14:05 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>
--- a/src/HOL/Nonstandard_Analysis/NSA.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy Thu Jun 28 14:14:05 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
--- a/src/HOL/Real.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Real.thy Thu Jun 28 14:14:05 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
--- a/src/HOL/Series.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Series.thy Thu Jun 28 14:14:05 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"
--- a/src/HOL/Transcendental.thy Thu Jun 28 13:49:02 2018 +0200
+++ b/src/HOL/Transcendental.thy Thu Jun 28 14:14:05 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))