--- a/CONTRIBUTORS Fri Jun 29 20:32:24 2018 +0200
+++ b/CONTRIBUTORS Fri Jun 29 22:14:33 2018 +0200
@@ -12,6 +12,9 @@
* June 2018: Martin Baillon and Paulo EmÃlio de Vilhena
A variety of contributions to HOL-Algebra.
+* June 2018: Wenda Li
+ New/strengthened results involving analysis, topology, etc.
+
* May/June 2018: Makarius Wenzel
System infrastructure to export blobs as theory presentation, and to dump
PIDE database content in batch mode.
@@ -38,6 +41,9 @@
* March 2018: Viorel Preoteasa
Generalisation of complete_distrib_lattice
+* February 2018: Wenda Li
+ A unified definition for the order of zeros and poles. Improved reasoning around non-essential singularities.
+
* January 2018: Sebastien Gouezel
Various small additions to HOL-Analysis
--- a/NEWS Fri Jun 29 20:32:24 2018 +0200
+++ b/NEWS Fri Jun 29 22:14:33 2018 +0200
@@ -399,6 +399,10 @@
as Ln, namely (-pi,pi]; the old Arg function has been renamed Arg2pi.
INCOMPATIBILITY.
+* Session HOL-Analysis: the functions zorder, zer_poly, porder and pol_poly have been redefined.
+All related lemmas have been reworked.
+INCOMPATIBILITY.
+
* Session HOL-Analysis: infinite products, Moebius functions, the
Riemann mapping theorem, the Vitali covering theorem,
change-of-variables results for integration and measures.
--- a/src/HOL/Analysis/Arcwise_Connected.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Arcwise_Connected.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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}"
@@ -774,7 +774,27 @@
ultimately show ?thesis unfolding valid_path_def piecewise_C1_differentiable_on_def path_def
using \<open>finite S\<close> by auto
qed
-
+
+lemma valid_path_uminus_comp[simp]:
+ fixes g::"real \<Rightarrow> 'a ::real_normed_field"
+ shows "valid_path (uminus \<circ> g) \<longleftrightarrow> valid_path g"
+proof
+ show "valid_path g \<Longrightarrow> valid_path (uminus \<circ> g)" for g::"real \<Rightarrow> 'a"
+ by (auto intro!: valid_path_compose derivative_intros simp add: deriv_linear[of "-1",simplified])
+ then show "valid_path g" when "valid_path (uminus \<circ> g)"
+ by (metis fun.map_comp group_add_class.minus_comp_minus id_comp that)
+qed
+
+lemma valid_path_offset[simp]:
+ shows "valid_path (\<lambda>t. g t - z) \<longleftrightarrow> valid_path g"
+proof
+ show *: "valid_path (g::real\<Rightarrow>'a) \<Longrightarrow> valid_path (\<lambda>t. g t - z)" for g z
+ unfolding valid_path_def
+ by (fastforce intro:derivative_intros C1_differentiable_imp_piecewise piecewise_C1_differentiable_diff)
+ show "valid_path (\<lambda>t. g t - z) \<Longrightarrow> valid_path g"
+ using *[of "\<lambda>t. g t - z" "-z",simplified] .
+qed
+
subsection\<open>Contour Integrals along a path\<close>
@@ -3554,6 +3574,19 @@
"(\<And>t. \<lbrakk>0 \<le> t; t \<le> 1\<rbrakk> \<Longrightarrow> p t = q t) \<Longrightarrow> winding_number p z = winding_number q z"
by (simp add: winding_number_def winding_number_prop_def pathstart_def pathfinish_def)
+lemma winding_number_constI:
+ assumes "c\<noteq>z" "\<And>t. \<lbrakk>0\<le>t; t\<le>1\<rbrakk> \<Longrightarrow> g t = c"
+ shows "winding_number g z = 0"
+proof -
+ have "winding_number g z = winding_number (linepath c c) z"
+ apply (rule winding_number_cong)
+ using assms unfolding linepath_def by auto
+ moreover have "winding_number (linepath c c) z =0"
+ apply (rule winding_number_trivial)
+ using assms by auto
+ ultimately show ?thesis by auto
+qed
+
lemma winding_number_offset: "winding_number p z = winding_number (\<lambda>w. p w - z) 0"
unfolding winding_number_def
proof (intro ext arg_cong [where f = Eps] arg_cong [where f = All] imp_cong refl, safe)
@@ -4812,8 +4845,7 @@
winding_number (subpath u w g) z"
apply (rule trans [OF winding_number_join [THEN sym]
winding_number_homotopic_paths [OF homotopic_join_subpaths]])
-apply (auto dest: path_image_subpath_subset)
-done
+ using path_image_subpath_subset by auto
subsection\<open>Partial circle path\<close>
@@ -4829,6 +4861,11 @@
"pathfinish(part_circlepath z r s t) = z + r*exp(\<i>*t)"
by (metis part_circlepath_def pathfinish_def pathfinish_linepath)
+lemma reversepath_part_circlepath[simp]:
+ "reversepath (part_circlepath z r s t) = part_circlepath z r t s"
+ unfolding part_circlepath_def reversepath_def linepath_def
+ by (auto simp:algebra_simps)
+
proposition has_vector_derivative_part_circlepath [derivative_intros]:
"((part_circlepath z r s t) has_vector_derivative
(\<i> * r * (of_real t - of_real s) * exp(\<i> * linepath s t x)))
@@ -6161,7 +6198,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/Change_Of_Vars.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Change_Of_Vars.thy Fri Jun 29 22:14:33 2018 +0200
@@ -2937,7 +2937,7 @@
moreover have "integral (g ` S) (h n) \<le> integral S (\<lambda>x. ?D x * f (g x))" for n
using hint by (blast intro: le order_trans)
ultimately show ?thesis
- by (auto intro: Lim_bounded_ereal)
+ by (auto intro: Lim_bounded)
qed
--- a/src/HOL/Analysis/Complex_Transcendental.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy Fri Jun 29 22:14:33 2018 +0200
@@ -1177,21 +1177,6 @@
obtains w where "w \<noteq> 0" "z = w ^ n"
by (metis exists_complex_root [of n z] assms power_0_left)
-subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
-
-text\<open>Note that in this special case the unwinding number is -1, 0 or 1.\<close>
-
-definition unwinding :: "complex \<Rightarrow> complex" where
- "unwinding(z) = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
-
-lemma unwinding_2pi: "(2*pi) * \<i> * unwinding(z) = z - Ln(exp z)"
- by (simp add: unwinding_def)
-
-lemma Ln_times_unwinding:
- "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \<i> * unwinding(Ln w + Ln z)"
- using unwinding_2pi by (simp add: exp_add)
-
-
subsection\<open>Derivative of Ln away from the branch cut\<close>
lemma
@@ -1465,6 +1450,10 @@
using mpi_less_Im_Ln Im_Ln_le_pi
by (force simp: Ln_times)
+corollary Ln_times_Reals:
+ "\<lbrakk>r \<in> Reals; Re r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(r * z) = ln (Re r) + Ln(z)"
+ using Ln_Reals_eq Ln_times_of_real by fastforce
+
corollary Ln_divide_of_real:
"\<lbrakk>r > 0; z \<noteq> 0\<rbrakk> \<Longrightarrow> Ln(z / of_real r) = Ln(z) - ln r"
using Ln_times_of_real [of "inverse r" z]
@@ -1571,9 +1560,61 @@
subsection\<open>The Argument of a Complex Number\<close>
+text\<open>Finally: it's is defined for the same interval as the complex logarithm: $(-\pi,\pi]$.\<close>
+
definition Arg :: "complex \<Rightarrow> real" where "Arg z \<equiv> (if z = 0 then 0 else Im (Ln z))"
-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 is_Arg_Arg: "z \<noteq> 0 \<Longrightarrow> is_Arg z (Arg z)"
+ by (simp add: Arg_eq is_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"
@@ -1603,14 +1644,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 +1651,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 +1703,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 +1724,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)"])
@@ -1747,6 +1776,47 @@
using continuous_at_Arg continuous_at_imp_continuous_within by blast
+subsection\<open>The Unwinding Number and the Ln-product Formula\<close>
+
+text\<open>Note that in this special case the unwinding number is -1, 0 or 1. But it's always an integer.\<close>
+
+lemma is_Arg_exp_Im: "is_Arg (exp z) (Im z)"
+ using exp_eq_polar is_Arg_def norm_exp_eq_Re by auto
+
+lemma is_Arg_exp_diff_2pi:
+ assumes "is_Arg (exp z) \<theta>"
+ shows "\<exists>k. Im z - of_int k * (2 * pi) = \<theta>"
+proof (intro exI is_Arg_eqI)
+ let ?k = "\<lfloor>(Im z - \<theta>) / (2 * pi)\<rfloor>"
+ show "is_Arg (exp z) (Im z - real_of_int ?k * (2 * pi))"
+ by (metis diff_add_cancel is_Arg_2pi_iff is_Arg_exp_Im)
+ show "\<bar>Im z - real_of_int ?k * (2 * pi) - \<theta>\<bar> < 2 * pi"
+ using floor_divide_upper [of "2*pi" "Im z - \<theta>"] floor_divide_lower [of "2*pi" "Im z - \<theta>"]
+ by (auto simp: algebra_simps abs_if)
+qed (auto simp: is_Arg_exp_Im assms)
+
+lemma Arg_exp_diff_2pi: "\<exists>k. Im z - of_int k * (2 * pi) = Arg (exp z)"
+ using is_Arg_exp_diff_2pi [OF is_Arg_Arg] by auto
+
+lemma unwinding_in_Ints: "(z - Ln(exp z)) / (of_real(2*pi) * \<i>) \<in> \<int>"
+ using Arg_exp_diff_2pi [of z]
+ by (force simp: Ints_def image_def field_simps Arg_def intro!: complex_eqI)
+
+definition unwinding :: "complex \<Rightarrow> int" where
+ "unwinding z \<equiv> THE k. of_int k = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
+
+lemma unwinding: "of_int (unwinding z) = (z - Ln(exp z)) / (of_real(2*pi) * \<i>)"
+ using unwinding_in_Ints [of z]
+ unfolding unwinding_def Ints_def by force
+
+lemma unwinding_2pi: "(2*pi) * \<i> * unwinding(z) = z - Ln(exp z)"
+ by (simp add: unwinding)
+
+lemma Ln_times_unwinding:
+ "w \<noteq> 0 \<Longrightarrow> z \<noteq> 0 \<Longrightarrow> Ln(w * z) = Ln(w) + Ln(z) - (2*pi) * \<i> * unwinding(Ln w + Ln z)"
+ using unwinding_2pi by (simp add: exp_add)
+
+
subsection\<open>Relation between Ln and Arg2pi, and hence continuity of Arg2pi\<close>
lemma Arg2pi_Ln:
--- a/src/HOL/Analysis/Connected.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Connected.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Derivative.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Great_Picard.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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/Interval_Integral.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy Fri Jun 29 22:14:33 2018 +0200
@@ -875,7 +875,7 @@
using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
- by (intro decseq_le, auto simp: decseq_def)
+ by (intro decseq_ge, auto simp: decseq_def)
have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
@@ -972,7 +972,7 @@
using A apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (l i)" in spec, auto)
hence A3: "\<And>i. g (l i) \<ge> A"
- by (intro decseq_le, auto simp: decseq_def)
+ by (intro decseq_ge, auto simp: decseq_def)
have B2: "(\<lambda>i. g (u i)) \<longlonglongrightarrow> B"
using B apply (auto simp: einterval_def tendsto_at_iff_sequentially comp_def)
by (drule_tac x = "\<lambda>i. ereal (u i)" in spec, auto)
--- a/src/HOL/Analysis/Measure_Space.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy Fri Jun 29 22:14:33 2018 +0200
@@ -389,7 +389,7 @@
show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
using A by auto
qed
- from INF_Lim_ereal[OF decseq_f this]
+ from INF_Lim[OF decseq_f this]
have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
by auto
@@ -2020,7 +2020,7 @@
finally show ?thesis by simp
qed
ultimately have "emeasure M (\<Union>N. B N) \<le> ennreal (\<Sum>n. measure M (A n))"
- by (simp add: Lim_bounded_ereal)
+ by (simp add: Lim_bounded)
then show "emeasure M (\<Union>n. A n) \<le> (\<Sum>n. measure M (A n))"
unfolding B_def by (metis UN_UN_flatten UN_lessThan_UNIV)
then show "emeasure M (\<Union>n. A n) < \<infinity>"
--- a/src/HOL/Analysis/Path_Connected.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Path_Connected.thy Fri Jun 29 22:14:33 2018 +0200
@@ -929,10 +929,10 @@
done
lemma path_image_subpath_subset:
- "\<lbrakk>path g; u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
+ "\<lbrakk>u \<in> {0..1}; v \<in> {0..1}\<rbrakk> \<Longrightarrow> path_image(subpath u v g) \<subseteq> path_image g"
apply (simp add: closed_segment_real_eq image_affinity_atLeastAtMost path_image_subpath)
apply (auto simp: path_image_def)
- done
+ done
lemma join_subpaths_middle: "subpath (0) ((1 / 2)) p +++ subpath ((1 / 2)) 1 p = p"
by (rule ext) (simp add: joinpaths_def subpath_def divide_simps)
@@ -1751,14 +1751,14 @@
by (simp add: path_connected_def)
qed
-lemma path_component: "path_component s x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> s \<and> x \<in> t \<and> y \<in> t)"
+lemma path_component: "path_component S x y \<longleftrightarrow> (\<exists>t. path_connected t \<and> t \<subseteq> S \<and> x \<in> t \<and> y \<in> t)"
apply (intro iffI)
apply (metis path_connected_path_image path_defs(5) pathfinish_in_path_image pathstart_in_path_image)
using path_component_of_subset path_connected_component by blast
lemma path_component_path_component [simp]:
- "path_component_set (path_component_set s x) x = path_component_set s x"
-proof (cases "x \<in> s")
+ "path_component_set (path_component_set S x) x = path_component_set S x"
+proof (cases "x \<in> S")
case True show ?thesis
apply (rule subset_antisym)
apply (simp add: path_component_subset)
@@ -1769,11 +1769,11 @@
qed
lemma path_component_subset_connected_component:
- "(path_component_set s x) \<subseteq> (connected_component_set s x)"
-proof (cases "x \<in> s")
+ "(path_component_set S x) \<subseteq> (connected_component_set S x)"
+proof (cases "x \<in> S")
case True show ?thesis
apply (rule connected_component_maximal)
- apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected path_connected_path_component)
+ apply (auto simp: True path_component_subset path_component_refl path_connected_imp_connected)
done
next
case False then show ?thesis
@@ -1784,11 +1784,11 @@
lemma path_connected_linear_image:
fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
- assumes "path_connected s" "bounded_linear f"
- shows "path_connected(f ` s)"
+ assumes "path_connected S" "bounded_linear f"
+ shows "path_connected(f ` S)"
by (auto simp: linear_continuous_on assms path_connected_continuous_image)
-lemma is_interval_path_connected: "is_interval s \<Longrightarrow> path_connected s"
+lemma is_interval_path_connected: "is_interval S \<Longrightarrow> path_connected S"
by (simp add: convex_imp_path_connected is_interval_convex)
lemma linear_homeomorphism_image:
--- a/src/HOL/Analysis/Starlike.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Starlike.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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/Analysis/Summation_Tests.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Summation_Tests.thy Fri Jun 29 22:14:33 2018 +0200
@@ -752,7 +752,7 @@
assumes lim: "(\<lambda>n. ereal (norm (f n) / norm (f (Suc n)))) \<longlonglongrightarrow> c"
shows "conv_radius f = c"
proof (rule conv_radius_eqI')
- show "c \<ge> 0" by (intro Lim_bounded2_ereal[OF lim]) simp_all
+ show "c \<ge> 0" by (intro Lim_bounded2[OF lim]) simp_all
next
fix r assume r: "0 < r" "ereal r < c"
let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))"
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Fri Jun 29 22:14:33 2018 +0200
@@ -2068,32 +2068,45 @@
lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
by (auto simp: islimpt_def)
+lemma finite_ball_include:
+ fixes a :: "'a::metric_space"
+ assumes "finite S"
+ shows "\<exists>e>0. S \<subseteq> ball a e"
+ using assms
+proof induction
+ case (insert x S)
+ then obtain e0 where "e0>0" and e0:"S \<subseteq> ball a e0" by auto
+ define e where "e = max e0 (2 * dist a x)"
+ have "e>0" unfolding e_def using \<open>e0>0\<close> by auto
+ moreover have "insert x S \<subseteq> ball a e"
+ using e0 \<open>e>0\<close> unfolding e_def by auto
+ ultimately show ?case by auto
+qed (auto intro: zero_less_one)
+
lemma finite_set_avoid:
fixes a :: "'a::metric_space"
- assumes fS: "finite S"
+ assumes "finite S"
shows "\<exists>d>0. \<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
-proof (induct rule: finite_induct[OF fS])
- case 1
- then show ?case by (auto intro: zero_less_one)
-next
- case (2 x F)
- from 2 obtain d where d: "d > 0" "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> d \<le> dist a x"
+ using assms
+proof induction
+ case (insert x S)
+ then obtain d where "d > 0" and d: "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> d \<le> dist a x"
by blast
show ?case
proof (cases "x = a")
case True
- with d show ?thesis by auto
+ with \<open>d > 0 \<close>d show ?thesis by auto
next
case False
let ?d = "min d (dist a x)"
- from False d(1) have dp: "?d > 0"
+ from False \<open>d > 0\<close> have dp: "?d > 0"
by auto
- from d have d': "\<forall>x\<in>F. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
+ from d have d': "\<forall>x\<in>S. x \<noteq> a \<longrightarrow> ?d \<le> dist a x"
by auto
with dp False show ?thesis
- by (auto intro!: exI[where x="?d"])
+ by (metis insert_iff le_less min_less_iff_conj not_less)
qed
-qed
+qed (auto intro: zero_less_one)
lemma islimpt_Un: "x islimpt (S \<union> T) \<longleftrightarrow> x islimpt S \<or> x islimpt T"
by (simp add: islimpt_iff_eventually eventually_conj_iff)
--- a/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Computational_Algebra/Fundamental_Theorem_Algebra.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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/Computational_Algebra/Polynomial.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Computational_Algebra/Polynomial.thy Fri Jun 29 22:14:33 2018 +0200
@@ -9,7 +9,7 @@
theory Polynomial
imports
- HOL.Deriv
+ Complex_Main
"HOL-Library.More_List"
"HOL-Library.Infinite_Set"
Factorial_Ring
@@ -1832,10 +1832,13 @@
by simp
qed
-(* Next two lemmas contributed by Wenda Li *)
+(* Next three lemmas contributed by Wenda Li *)
lemma order_1_eq_0 [simp]:"order x 1 = 0"
by (metis order_root poly_1 zero_neq_one)
+lemma order_uminus[simp]: "order x (-p) = order x p"
+ by (metis neg_equal_0_iff_equal order_smult smult_1_left smult_minus_left)
+
lemma order_power_n_n: "order a ([:-a,1:]^n)=n"
proof (induct n) (*might be proved more concisely using nat_less_induct*)
case 0
@@ -2575,17 +2578,28 @@
lemma poly_DERIV [simp]: "DERIV (\<lambda>x. poly p x) x :> poly (pderiv p) x"
by (induct p) (auto intro!: derivative_eq_intros simp add: pderiv_pCons)
+lemma poly_isCont[simp]:
+ fixes x::"'a::real_normed_field"
+ shows "isCont (\<lambda>x. poly p x) x"
+by (rule poly_DERIV [THEN DERIV_isCont])
+
+lemma tendsto_poly [tendsto_intros]: "(f \<longlongrightarrow> a) F \<Longrightarrow> ((\<lambda>x. poly p (f x)) \<longlongrightarrow> poly p a) F"
+ for f :: "_ \<Rightarrow> 'a::real_normed_field"
+ by (rule isCont_tendsto_compose [OF poly_isCont])
+
+lemma continuous_within_poly: "continuous (at z within s) (poly p)"
+ for z :: "'a::{real_normed_field}"
+ by (simp add: continuous_within tendsto_poly)
+
+lemma continuous_poly [continuous_intros]: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. poly p (f x))"
+ for f :: "_ \<Rightarrow> 'a::real_normed_field"
+ unfolding continuous_def by (rule tendsto_poly)
+
lemma continuous_on_poly [continuous_intros]:
fixes p :: "'a :: {real_normed_field} poly"
assumes "continuous_on A f"
shows "continuous_on A (\<lambda>x. poly p (f x))"
-proof -
- have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))"
- by (intro continuous_intros assms)
- also have "\<dots> = (\<lambda>x. poly p (f x))"
- by (rule ext) (simp add: poly_altdef mult_ac)
- finally show ?thesis .
-qed
+ by (metis DERIV_continuous_on assms continuous_on_compose2 poly_DERIV subset_UNIV)
text \<open>Consequences of the derivative theorem above.\<close>
@@ -2593,10 +2607,6 @@
for x :: real
by (simp add: real_differentiable_def) (blast intro: poly_DERIV)
-lemma poly_isCont[simp]: "isCont (\<lambda>x. poly p x) x"
- for x :: real
- by (rule poly_DERIV [THEN DERIV_isCont])
-
lemma poly_IVT_pos: "a < b \<Longrightarrow> poly p a < 0 \<Longrightarrow> 0 < poly p b \<Longrightarrow> \<exists>x. a < x \<and> x < b \<and> poly p x = 0"
for a b :: real
using IVT_objl [of "poly p" a 0 b] by (auto simp add: order_le_less)
--- a/src/HOL/Deriv.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Deriv.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Fields.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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/Library/Extended_Real.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Library/Extended_Real.thy Fri Jun 29 22:14:33 2018 +0200
@@ -2921,17 +2921,6 @@
lemma Lim_bounded_PInfty2: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>N. f n \<le> ereal B \<Longrightarrow> l \<noteq> \<infinity>"
using LIMSEQ_le_const2[of f l "ereal B"] by fastforce
-lemma Lim_bounded_ereal: "f \<longlonglongrightarrow> (l :: 'a::linorder_topology) \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
- by (intro LIMSEQ_le_const2) auto
-
-lemma Lim_bounded2_ereal:
- assumes lim:"f \<longlonglongrightarrow> (l :: 'a::linorder_topology)"
- and ge: "\<forall>n\<ge>N. f n \<ge> C"
- shows "l \<ge> C"
- using ge
- by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
- (auto simp: eventually_sequentially)
-
lemma real_of_ereal_mult[simp]:
fixes a b :: ereal
shows "real_of_ereal (a * b) = real_of_ereal a * real_of_ereal b"
@@ -3341,7 +3330,7 @@
assumes "\<forall>N. (\<Sum>n<N. f n) \<le> x"
and pos: "\<And>n. 0 \<le> f n"
shows "suminf f \<le> x"
-proof (rule Lim_bounded_ereal)
+proof (rule Lim_bounded)
have "summable f" using pos[THEN summable_ereal_pos] .
then show "(\<lambda>N. \<Sum>n<N. f n) \<longlonglongrightarrow> suminf f"
by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
@@ -3879,66 +3868,6 @@
shows "X \<longlonglongrightarrow> -\<infinity> \<longleftrightarrow> limsup X = -\<infinity>"
by (metis Limsup_MInfty trivial_limit_sequentially)
-lemma ereal_lim_mono:
- fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
- assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
- and "X \<longlonglongrightarrow> x"
- and "Y \<longlonglongrightarrow> y"
- shows "x \<le> y"
- using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
-
-lemma incseq_le_ereal:
- fixes X :: "nat \<Rightarrow> 'a::linorder_topology"
- assumes inc: "incseq X"
- and lim: "X \<longlonglongrightarrow> L"
- shows "X N \<le> L"
- using inc
- by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)
-
-lemma decseq_ge_ereal:
- assumes dec: "decseq X"
- and lim: "X \<longlonglongrightarrow> (L::'a::linorder_topology)"
- shows "X N \<ge> L"
- using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)
-
-lemma bounded_abs:
- fixes a :: real
- assumes "a \<le> x"
- and "x \<le> b"
- shows "\<bar>x\<bar> \<le> max \<bar>a\<bar> \<bar>b\<bar>"
- by (metis abs_less_iff assms leI le_max_iff_disj
- less_eq_real_def less_le_not_le less_minus_iff minus_minus)
-
-lemma ereal_Sup_lim:
- fixes a :: "'a::{complete_linorder,linorder_topology}"
- assumes "\<And>n. b n \<in> s"
- and "b \<longlonglongrightarrow> a"
- shows "a \<le> Sup s"
- by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)
-
-lemma ereal_Inf_lim:
- fixes a :: "'a::{complete_linorder,linorder_topology}"
- assumes "\<And>n. b n \<in> s"
- and "b \<longlonglongrightarrow> a"
- shows "Inf s \<le> a"
- by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)
-
-lemma SUP_Lim_ereal:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- assumes inc: "incseq X"
- and l: "X \<longlonglongrightarrow> l"
- shows "(SUP n. X n) = l"
- using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
- by simp
-
-lemma INF_Lim_ereal:
- fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
- assumes dec: "decseq X"
- and l: "X \<longlonglongrightarrow> l"
- shows "(INF n. X n) = l"
- using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
- by simp
-
lemma SUP_eq_LIMSEQ:
assumes "mono f"
shows "(SUP n. ereal (f n)) = ereal x \<longleftrightarrow> f \<longlonglongrightarrow> x"
@@ -3949,7 +3878,7 @@
assume "f \<longlonglongrightarrow> x"
then have "(\<lambda>i. ereal (f i)) \<longlonglongrightarrow> ereal x"
by auto
- from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
+ from SUP_Lim[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
next
assume "(SUP n. ereal (f n)) = ereal x"
with LIMSEQ_SUP[OF inc] show "f \<longlonglongrightarrow> x" by auto
--- a/src/HOL/Limits.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Limits.thy Fri Jun 29 22:14:33 2018 +0200
@@ -1347,12 +1347,17 @@
unfolding filterlim_at_bot eventually_at_top_dense
by (metis leI less_minus_iff order_less_asym)
-lemma at_top_mirror: "at_top = filtermap uminus (at_bot :: real filter)"
- by (rule filtermap_fun_inverse[symmetric, of uminus])
- (auto intro: filterlim_uminus_at_bot_at_top filterlim_uminus_at_top_at_bot)
-
-lemma at_bot_mirror: "at_bot = filtermap uminus (at_top :: real filter)"
- unfolding at_top_mirror filtermap_filtermap by (simp add: filtermap_ident)
+lemma at_bot_mirror :
+ shows "(at_bot::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_top"
+ apply (rule filtermap_fun_inverse[of uminus, symmetric])
+ subgoal unfolding filterlim_at_top eventually_at_bot_linorder using le_minus_iff by auto
+ subgoal unfolding filterlim_at_bot eventually_at_top_linorder using minus_le_iff by auto
+ by auto
+
+lemma at_top_mirror :
+ shows "(at_top::('a::{ordered_ab_group_add,linorder} filter)) = filtermap uminus at_bot"
+ apply (subst at_bot_mirror)
+ by (auto simp add: filtermap_filtermap)
lemma filterlim_at_top_mirror: "(LIM x at_top. f x :> F) \<longleftrightarrow> (LIM x at_bot. f (-x::real) :> F)"
unfolding filterlim_def at_top_mirror filtermap_filtermap ..
@@ -2294,7 +2299,7 @@
obtain L where "X \<longlonglongrightarrow> L"
by (auto simp: convergent_def monoseq_def decseq_def)
with \<open>decseq X\<close> show "\<exists>L. X \<longlonglongrightarrow> L \<and> (\<forall>i. L \<le> X i)"
- by (auto intro!: exI[of _ L] decseq_le)
+ by (auto intro!: exI[of _ L] decseq_ge)
qed
--- a/src/HOL/List.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/List.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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 Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Nonstandard_Analysis/NSA.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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/Probability/Distribution_Functions.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Probability/Distribution_Functions.thy Fri Jun 29 22:14:33 2018 +0200
@@ -107,7 +107,7 @@
using \<open>decseq f\<close> unfolding cdf_def
by (intro finite_Lim_measure_decseq) (auto simp: decseq_def)
also have "(\<Inter>i. {.. f i}) = {.. a}"
- using decseq_le[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
+ using decseq_ge[OF f] by (auto intro: order_trans LIMSEQ_le_const[OF f(2)])
finally show "(\<lambda>n. cdf M (f n)) \<longlonglongrightarrow> cdf M a"
by (simp add: cdf_def)
qed simp
--- a/src/HOL/Rat.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Rat.thy Fri Jun 29 22:14:33 2018 +0200
@@ -825,6 +825,16 @@
end
+lemma Rats_cases [cases set: Rats]:
+ assumes "q \<in> \<rat>"
+ obtains (of_rat) r where "q = of_rat r"
+proof -
+ from \<open>q \<in> \<rat>\<close> have "q \<in> range of_rat"
+ by (simp only: Rats_def)
+ then obtain r where "q = of_rat r" ..
+ then show thesis ..
+qed
+
lemma Rats_of_rat [simp]: "of_rat r \<in> \<rat>"
by (simp add: Rats_def)
@@ -855,11 +865,8 @@
apply (rule of_rat_add [symmetric])
done
-lemma Rats_minus [simp]: "a \<in> \<rat> \<Longrightarrow> - a \<in> \<rat>"
- apply (auto simp add: Rats_def)
- apply (rule range_eqI)
- apply (rule of_rat_minus [symmetric])
- done
+lemma Rats_minus_iff [simp]: "- a \<in> \<rat> \<longleftrightarrow> a \<in> \<rat>"
+by (metis Rats_cases Rats_of_rat add.inverse_inverse of_rat_minus)
lemma Rats_diff [simp]: "a \<in> \<rat> \<Longrightarrow> b \<in> \<rat> \<Longrightarrow> a - b \<in> \<rat>"
apply (auto simp add: Rats_def)
@@ -894,16 +901,6 @@
apply (rule of_rat_power [symmetric])
done
-lemma Rats_cases [cases set: Rats]:
- assumes "q \<in> \<rat>"
- obtains (of_rat) r where "q = of_rat r"
-proof -
- from \<open>q \<in> \<rat>\<close> have "q \<in> range of_rat"
- by (simp only: Rats_def)
- then obtain r where "q = of_rat r" ..
- then show thesis ..
-qed
-
lemma Rats_induct [case_names of_rat, induct set: Rats]: "q \<in> \<rat> \<Longrightarrow> (\<And>r. P (of_rat r)) \<Longrightarrow> P q"
by (rule Rats_cases) auto
--- a/src/HOL/Real.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Real.thy Fri Jun 29 22:14:33 2018 +0200
@@ -1192,6 +1192,10 @@
subsection \<open>Rationals\<close>
+lemma Rats_abs_iff[simp]:
+ "\<bar>(x::real)\<bar> \<in> \<rat> \<longleftrightarrow> x \<in> \<rat>"
+by(simp add: abs_real_def split: if_splits)
+
lemma Rats_eq_int_div_int: "\<rat> = {real_of_int i / real_of_int j | i j. j \<noteq> 0}" (is "_ = ?S")
proof
show "\<rat> \<subseteq> ?S"
@@ -1383,21 +1387,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/Real_Vector_Spaces.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Real_Vector_Spaces.thy Fri Jun 29 22:14:33 2018 +0200
@@ -1092,7 +1092,7 @@
then show ?thesis
by simp
qed
-
+
subclass uniform_space
proof
fix E x
--- a/src/HOL/Series.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Series.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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/Topological_Spaces.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Topological_Spaces.thy Fri Jun 29 22:14:33 2018 +0200
@@ -1109,7 +1109,7 @@
unfolding Lim_def ..
-subsubsection \<open>Monotone sequences and subsequences\<close>
+subsection \<open>Monotone sequences and subsequences\<close>
text \<open>
Definition of monotonicity.
@@ -1132,7 +1132,7 @@
lemma decseq_def: "decseq X \<longleftrightarrow> (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
unfolding antimono_def ..
-text \<open>Definition of subsequence.\<close>
+subsubsection \<open>Definition of subsequence.\<close>
(* For compatibility with the old "subseq" *)
lemma strict_mono_leD: "strict_mono r \<Longrightarrow> m \<le> n \<Longrightarrow> r m \<le> r n"
@@ -1205,7 +1205,7 @@
qed
-text \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
+subsubsection \<open>Subsequence (alternative definition, (e.g. Hoskins)\<close>
lemma strict_mono_Suc_iff: "strict_mono f \<longleftrightarrow> (\<forall>n. f n < f (Suc n))"
proof (intro iffI strict_monoI)
@@ -1351,7 +1351,7 @@
by (rule LIMSEQ_offset [where k="Suc 0"]) simp
lemma LIMSEQ_Suc_iff: "(\<lambda>n. f (Suc n)) \<longlonglongrightarrow> l = f \<longlonglongrightarrow> l"
- by (blast intro: LIMSEQ_imp_Suc LIMSEQ_Suc)
+ by (rule filterlim_sequentially_Suc)
lemma LIMSEQ_lessThan_iff_atMost:
shows "(\<lambda>n. f {..<n}) \<longlonglongrightarrow> x \<longleftrightarrow> (\<lambda>n. f {..n}) \<longlonglongrightarrow> x"
@@ -1375,6 +1375,56 @@
for a x :: "'a::linorder_topology"
by (rule LIMSEQ_le[of X x "\<lambda>n. a"]) auto
+lemma Lim_bounded: "f \<longlonglongrightarrow> l \<Longrightarrow> \<forall>n\<ge>M. f n \<le> C \<Longrightarrow> l \<le> C"
+ for l :: "'a::linorder_topology"
+ by (intro LIMSEQ_le_const2) auto
+
+lemma Lim_bounded2:
+ fixes f :: "nat \<Rightarrow> 'a::linorder_topology"
+ assumes lim:"f \<longlonglongrightarrow> l" and ge: "\<forall>n\<ge>N. f n \<ge> C"
+ shows "l \<ge> C"
+ using ge
+ by (intro tendsto_le[OF trivial_limit_sequentially lim tendsto_const])
+ (auto simp: eventually_sequentially)
+
+lemma lim_mono:
+ fixes X Y :: "nat \<Rightarrow> 'a::linorder_topology"
+ assumes "\<And>n. N \<le> n \<Longrightarrow> X n \<le> Y n"
+ and "X \<longlonglongrightarrow> x"
+ and "Y \<longlonglongrightarrow> y"
+ shows "x \<le> y"
+ using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto
+
+lemma Sup_lim:
+ fixes a :: "'a::{complete_linorder,linorder_topology}"
+ assumes "\<And>n. b n \<in> s"
+ and "b \<longlonglongrightarrow> a"
+ shows "a \<le> Sup s"
+ by (metis Lim_bounded assms complete_lattice_class.Sup_upper)
+
+lemma Inf_lim:
+ fixes a :: "'a::{complete_linorder,linorder_topology}"
+ assumes "\<And>n. b n \<in> s"
+ and "b \<longlonglongrightarrow> a"
+ shows "Inf s \<le> a"
+ by (metis Lim_bounded2 assms complete_lattice_class.Inf_lower)
+
+lemma SUP_Lim:
+ fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+ assumes inc: "incseq X"
+ and l: "X \<longlonglongrightarrow> l"
+ shows "(SUP n. X n) = l"
+ using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
+ by simp
+
+lemma INF_Lim:
+ fixes X :: "nat \<Rightarrow> 'a::{complete_linorder,linorder_topology}"
+ assumes dec: "decseq X"
+ and l: "X \<longlonglongrightarrow> l"
+ shows "(INF n. X n) = l"
+ using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
+ by simp
+
lemma convergentD: "convergent X \<Longrightarrow> \<exists>L. X \<longlonglongrightarrow> L"
by (simp add: convergent_def)
@@ -1417,7 +1467,7 @@
for L :: "'a::linorder_topology"
by (metis incseq_def LIMSEQ_le_const)
-lemma decseq_le: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
+lemma decseq_ge: "decseq X \<Longrightarrow> X \<longlonglongrightarrow> L \<Longrightarrow> L \<le> X n"
for L :: "'a::linorder_topology"
by (metis decseq_def LIMSEQ_le_const2)
--- a/src/HOL/Transcendental.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Transcendental.thy Fri Jun 29 22:14:33 2018 +0200
@@ -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))
--- a/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Fri Jun 29 20:32:24 2018 +0200
+++ b/src/HOL/Types_To_Sets/Examples/Linear_Algebra_On.thy Fri Jun 29 22:14:33 2018 +0200
@@ -100,21 +100,10 @@
module_hom_on_axioms_def
by (auto intro!: ext)
-locale vector_space_on = \<comment>\<open>here we do the same trick as in \<open>module\<close> vs \<open>vector_space\<close>.\<close>
- fixes S and scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
- assumes scale_right_distrib [algebra_simps]: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> a *s (x + y) = a *s x + a *s y"
- and scale_left_distrib [algebra_simps]: "x \<in> S \<Longrightarrow> (a + b) *s x = a *s x + b *s x"
- and scale_scale [simp]: "x \<in> S \<Longrightarrow> a *s (b *s x) = (a * b) *s x"
- and scale_one [simp]: "x \<in> S \<Longrightarrow> 1 *s x = x"
- and mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
- and mem_zero: "0 \<in> S"
- and mem_scale: "x \<in> S \<Longrightarrow> a *s x \<in> S"
+locale vector_space_on = module_on S scale
+ for S and scale :: "'a::field \<Rightarrow> 'b::ab_group_add \<Rightarrow> 'b" (infixr "*s" 75)
begin
-sublocale module_on S "( *s)"
- using vector_space_on_axioms[unfolded vector_space_on_def]
- by unfold_locales auto
-
definition dim :: "'b set \<Rightarrow> nat"
where "dim V = (if \<exists>b\<subseteq>S. \<not> dependent b \<and> span b = span V
then card (SOME b. b \<subseteq> S \<and> \<not> dependent b \<and> span b = span V)
@@ -230,13 +219,13 @@
end
locale local_typedef_ab_group_add = local_typedef S s for S ::"'b::ab_group_add set" and s::"'s itself" +
- assumes mem_zero: "0 \<in> S"
- assumes mem_add: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
- assumes mem_uminus: "x \<in> S \<Longrightarrow> -x \<in> S"
+ assumes mem_zero_lt: "0 \<in> S"
+ assumes mem_add_lt: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x + y \<in> S"
+ assumes mem_uminus_lt: "x \<in> S \<Longrightarrow> -x \<in> S"
begin
-lemma mem_minus: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
- using mem_add[OF _ mem_uminus] by auto
+lemma mem_minus_lt: "x \<in> S \<Longrightarrow> y \<in> S \<Longrightarrow> x - y \<in> S"
+ using mem_add_lt[OF _ mem_uminus_lt] by auto
context includes lifting_syntax begin
@@ -247,19 +236,19 @@
lemma plus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) plus plus_S"
unfolding plus_S_def
- by (auto simp: cr_S_def mem_add intro!: rel_funI)
+ by (auto simp: cr_S_def mem_add_lt intro!: rel_funI)
lemma minus_S_transfer[transfer_rule]: "(cr_S ===> cr_S ===> cr_S) minus minus_S"
unfolding minus_S_def
- by (auto simp: cr_S_def mem_minus intro!: rel_funI)
+ by (auto simp: cr_S_def mem_minus_lt intro!: rel_funI)
lemma uminus_S_transfer[transfer_rule]: "(cr_S ===> cr_S) uminus uminus_S"
unfolding uminus_S_def
- by (auto simp: cr_S_def mem_uminus intro!: rel_funI)
+ by (auto simp: cr_S_def mem_uminus_lt intro!: rel_funI)
lemma zero_S_transfer[transfer_rule]: "cr_S 0 zero_S"
unfolding zero_S_def
- by (auto simp: cr_S_def mem_zero intro!: rel_funI)
+ by (auto simp: cr_S_def mem_zero_lt intro!: rel_funI)
end
@@ -538,11 +527,7 @@
OF type.ab_group_add_axioms type_module_on_with,
untransferred,
var_simplified implicit_ab_group_add]:
- lt_scale_right_distrib = module.scale_right_distrib
- and lt_scale_left_distrib = module.scale_left_distrib
- and lt_scale_scale = module.scale_scale
- and lt_scale_one = module.scale_one
- and lt_scale_left_commute = module.scale_left_commute
+ lt_scale_left_commute = module.scale_left_commute
and lt_scale_zero_left = module.scale_zero_left
and lt_scale_minus_left = module.scale_minus_left
and lt_scale_left_diff_distrib = module.scale_left_diff_distrib
@@ -611,11 +596,11 @@
and lt_module_hom_id = module.module_hom_id
and lt_module_hom_ident = module.module_hom_ident
and lt_module_hom_uminus = module.module_hom_uminus
- and subspace_UNIV = module.subspace_UNIV
- and span_alt = module.span_alt
+ and lt_subspace_UNIV = module.subspace_UNIV
(* should work but don't:
and span_def = module.span_def
and span_UNIV = module.span_UNIV
+ and lt_span_alt = module.span_alt
and dependent_alt = module.dependent_alt
and independent_alt = module.independent_alt
and unique_representation = module.unique_representation
@@ -647,11 +632,7 @@
folded subset_iff',
simplified pred_fun_def,
simplified\<comment>\<open>too much?\<close>]:
- scale_right_distrib = lt_scale_right_distrib
- and scale_left_distrib = lt_scale_left_distrib
- and scale_scale = lt_scale_scale
- and scale_one = lt_scale_one
- and scale_left_commute = lt_scale_left_commute
+ scale_left_commute = lt_scale_left_commute
and scale_zero_left = lt_scale_zero_left
and scale_minus_left = lt_scale_minus_left
and scale_left_diff_distrib = lt_scale_left_diff_distrib
@@ -720,7 +701,7 @@
and module_hom_id = lt_module_hom_id
and module_hom_ident = lt_module_hom_ident
and module_hom_uminus = lt_module_hom_uminus
-
+ and subspace_UNIV = lt_subspace_UNIV
end
subsubsection \<open>Vector Spaces\<close>
@@ -734,10 +715,10 @@
lemmas_with [var_simplified explicit_ab_group_add,
unoverload_type 'd,
OF type.ab_group_add_axioms type_vector_space_on_with,
+ folded dim_S_def,
untransferred,
var_simplified implicit_ab_group_add]:
- lt_vector_space_assms = vector_space.vector_space_assms
-and lt_linear_id = vector_space.linear_id
+ lt_linear_id = vector_space.linear_id
and lt_linear_ident = vector_space.linear_ident
and lt_linear_scale_self = vector_space.linear_scale_self
and lt_linear_scale_left = vector_space.linear_scale_left
@@ -768,13 +749,10 @@
and lt_independent_explicit_finite_subsets = vector_space.independent_explicit_finite_subsets
and lt_independent_if_scalars_zero = vector_space.independent_if_scalars_zero
and lt_subspace_sums = vector_space.subspace_sums
-(* should work but don't:
-and lt_injective_scale = vector_space.lt_injective_scale
-and lt_bij_if_span_eq_span_bases = vector_space.bij_if_span_eq_span_bases
-and lt_dim_def = vector_space.dim_def
+and lt_dim_unique = vector_space.dim_unique
and lt_dim_eq_card = vector_space.dim_eq_card
and lt_basis_card_eq_dim = vector_space.basis_card_eq_dim
-and lt_basis_exists["consumes" - 1, "case_names" "1"] = vector_space.basis_exists
+and lt_basis_exists = vector_space.basis_exists
and lt_dim_eq_card_independent = vector_space.dim_eq_card_independent
and lt_dim_span = vector_space.dim_span
and lt_dim_span_eq_card_independent = vector_space.dim_span_eq_card_independent
@@ -782,10 +760,12 @@
and lt_span_eq_dim = vector_space.span_eq_dim
and lt_dim_le_card' = vector_space.dim_le_card'
and lt_span_card_ge_dim = vector_space.span_card_ge_dim
-and lt_dim_unique = vector_space.dim_unique
-and lt_dim_with = vector_space.dim_with
+and lt_dim_with = vector_space.dim_with
+(* should work but don't:
+and lt_bij_if_span_eq_span_bases = vector_space.bij_if_span_eq_span_bases
*)
(* not expected to work:
+and lt_dim_def = vector_space.dim_def
and lt_extend_basis_superset = vector_space.extend_basis_superset
and lt_independent_extend_basis = vector_space.independent_extend_basis
and lt_span_extend_basis = vector_space.span_extend_basis
@@ -798,8 +778,7 @@
folded subset_iff',
simplified pred_fun_def,
simplified\<comment>\<open>too much?\<close>]:
- vector_space_assms = lt_vector_space_assms
-and linear_id = lt_linear_id
+ linear_id = lt_linear_id
and linear_ident = lt_linear_ident
and linear_scale_self = lt_linear_scale_self
and linear_scale_left = lt_linear_scale_left
@@ -829,6 +808,18 @@
and independent_explicit_finite_subsets = lt_independent_explicit_finite_subsets
and independent_if_scalars_zero = lt_independent_if_scalars_zero
and subspace_sums = lt_subspace_sums
+and dim_unique = lt_dim_unique
+and dim_eq_card = lt_dim_eq_card
+and basis_card_eq_dim = lt_basis_card_eq_dim
+and basis_exists["consumes" - 1, "case_names" "1"] = lt_basis_exists
+and dim_eq_card_independent = lt_dim_eq_card_independent
+and dim_span = lt_dim_span
+and dim_span_eq_card_independent = lt_dim_span_eq_card_independent
+and dim_le_card = lt_dim_le_card
+and span_eq_dim = lt_span_eq_dim
+and dim_le_card' = lt_dim_le_card'
+and span_card_ge_dim = lt_span_card_ge_dim
+and dim_with = lt_dim_with
end
@@ -888,37 +879,34 @@
folded subset_iff',
simplified pred_fun_def,
simplified\<comment>\<open>too much?\<close>]:
- vector_space_assms = lt_vector_space_assms
-and linear_id = lt_linear_id
-and linear_ident = lt_linear_ident
-and linear_scale_self = lt_linear_scale_self
-and linear_scale_left = lt_linear_scale_left
-and linear_uminus = lt_linear_uminus
-and linear_imp_scale["consumes" - 1, "case_names" "1"] = lt_linear_imp_scale
-and scale_eq_0_iff = lt_scale_eq_0_iff
-and scale_left_imp_eq = lt_scale_left_imp_eq
-and scale_right_imp_eq = lt_scale_right_imp_eq
-and scale_cancel_left = lt_scale_cancel_left
-and scale_cancel_right = lt_scale_cancel_right
-and dependent_def = lt_dependent_def
-and dependent_single = lt_dependent_single
-and in_span_insert = lt_in_span_insert
-and dependent_insertD = lt_dependent_insertD
-and independent_insertI = lt_independent_insertI
-and independent_insert = lt_independent_insert
-and maximal_independent_subset_extend["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset_extend
-and maximal_independent_subset["consumes" - 1, "case_names" "1"] = lt_maximal_independent_subset
-and in_span_delete = lt_in_span_delete
-and span_redundant = lt_span_redundant
-and span_trans = lt_span_trans
-and span_insert_0 = lt_span_insert_0
-and span_delete_0 = lt_span_delete_0
-and span_image_scale = lt_span_image_scale
-and exchange_lemma = lt_exchange_lemma
-and independent_span_bound = lt_independent_span_bound
-and independent_explicit_finite_subsets = lt_independent_explicit_finite_subsets
-and independent_if_scalars_zero = lt_independent_if_scalars_zero
-and subspace_sums = lt_subspace_sums
+ finiteI_independent = lt_finiteI_independent
+and dim_empty = lt_dim_empty
+and dim_insert = lt_dim_insert
+and dim_singleton = lt_dim_singleton
+and choose_subspace_of_subspace["consumes" - 1, "case_names" "1"] = lt_choose_subspace_of_subspace
+and basis_subspace_exists["consumes" - 1, "case_names" "1"] = lt_basis_subspace_exists
+and dim_mono = lt_dim_mono
+and dim_subset = lt_dim_subset
+and dim_eq_0 = lt_dim_eq_0
+and dim_UNIV = lt_dim_UNIV
+and independent_card_le_dim = lt_independent_card_le_dim
+and card_ge_dim_independent = lt_card_ge_dim_independent
+and card_le_dim_spanning = lt_card_le_dim_spanning
+and card_eq_dim = lt_card_eq_dim
+and subspace_dim_equal = lt_subspace_dim_equal
+and dim_eq_span = lt_dim_eq_span
+and dim_psubset = lt_dim_psubset
+and indep_card_eq_dim_span = lt_indep_card_eq_dim_span
+and independent_bound_general = lt_independent_bound_general
+and independent_explicit = lt_independent_explicit
+and dim_sums_Int = lt_dim_sums_Int
+and dependent_biggerset_general = lt_dependent_biggerset_general
+and subset_le_dim = lt_subset_le_dim
+and linear_inj_imp_surj = lt_linear_inj_imp_surj
+and linear_surj_imp_inj = lt_linear_surj_imp_inj
+and linear_inverse_left = lt_linear_inverse_left
+and left_inverse_linear = lt_left_inverse_linear
+and right_inverse_linear = lt_right_inverse_linear
end
--- a/src/Pure/Admin/isabelle_cronjob.scala Fri Jun 29 20:32:24 2018 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Fri Jun 29 22:14:33 2018 +0200
@@ -299,7 +299,7 @@
" -e ISABELLE_GHC=/usr/local/ghc-8.0.2/bin/ghc" +
" -e ISABELLE_SMLNJ=/usr/local/smlnj-110.81/bin/sml",
args = "-a",
- detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows"))),
+ detect = Build_Log.Settings.ML_PLATFORM + " = " + SQL.string("x86_64-windows")))
) :::
{
for { (n, hosts) <- List(1 -> List("lxbroy6"), 2 -> List("lxbroy8", "lxbroy5")) }
--- a/src/Pure/Tools/server.scala Fri Jun 29 20:32:24 2018 +0200
+++ b/src/Pure/Tools/server.scala Fri Jun 29 22:14:33 2018 +0200
@@ -102,7 +102,7 @@
val session = context.server.the_session(args.session_id)
Server_Commands.Use_Theories.command(
args, session, id = task.id, progress = task.progress)._1
- }),
+ })
},
"purge_theories" ->
{ case (context, Server_Commands.Purge_Theories(args)) =>