--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Mon Jan 02 18:08:04 2017 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy Tue Jan 03 16:48:49 2017 +0000
@@ -4601,11 +4601,11 @@
by metis
note ee_rule = ee [THEN conjunct2, rule_format]
define C where "C = (\<lambda>t. ball t (ee t / 3)) ` {0..1}"
- have "\<forall>t \<in> C. open t" by (simp add: C_def)
- moreover have "{0..1} \<subseteq> \<Union>C"
- using ee [THEN conjunct1] by (auto simp: C_def dist_norm)
- ultimately obtain C' where C': "C' \<subseteq> C" "finite C'" and C'01: "{0..1} \<subseteq> \<Union>C'"
- by (rule compactE [OF compact_interval])
+ obtain C' where C': "C' \<subseteq> C" "finite C'" and C'01: "{0..1} \<subseteq> \<Union>C'"
+ proof (rule compactE [OF compact_interval])
+ show "{0..1} \<subseteq> \<Union>C"
+ using ee [THEN conjunct1] by (auto simp: C_def dist_norm)
+ qed (use C_def in auto)
define kk where "kk = {t \<in> {0..1}. ball t (ee t / 3) \<in> C'}"
have kk01: "kk \<subseteq> {0..1}" by (auto simp: kk_def)
define e where "e = Min (ee ` kk)"
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy Mon Jan 02 18:08:04 2017 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy Tue Jan 03 16:48:49 2017 +0000
@@ -197,13 +197,13 @@
shows "closed {a..}"
by (simp add: eucl_le_atLeast[symmetric])
-lemma bounded_closed_interval:
+lemma bounded_closed_interval [simp]:
fixes a :: "'a::ordered_euclidean_space"
shows "bounded {a .. b}"
using bounded_cbox[of a b]
by (metis interval_cbox)
-lemma convex_closed_interval:
+lemma convex_closed_interval [simp]:
fixes a :: "'a::ordered_euclidean_space"
shows "convex {a .. b}"
using convex_box[of a b]
@@ -214,11 +214,11 @@
using image_smult_cbox[of m a b]
by (simp add: cbox_interval)
-lemma is_interval_closed_interval:
+lemma is_interval_closed_interval [simp]:
"is_interval {a .. (b::'a::ordered_euclidean_space)}"
by (metis cbox_interval is_interval_cbox)
-lemma compact_interval:
+lemma compact_interval [simp]:
fixes a b::"'a::ordered_euclidean_space"
shows "compact {a .. b}"
by (metis compact_cbox interval_cbox)
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy Mon Jan 02 18:08:04 2017 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy Tue Jan 03 16:48:49 2017 +0000
@@ -794,28 +794,28 @@
by (simp add: subtopology_superset)
lemma openin_subtopology_empty:
- "openin (subtopology U {}) s \<longleftrightarrow> s = {}"
+ "openin (subtopology U {}) S \<longleftrightarrow> S = {}"
by (metis Int_empty_right openin_empty openin_subtopology)
lemma closedin_subtopology_empty:
- "closedin (subtopology U {}) s \<longleftrightarrow> s = {}"
+ "closedin (subtopology U {}) S \<longleftrightarrow> S = {}"
by (metis Int_empty_right closedin_empty closedin_subtopology)
-lemma closedin_subtopology_refl:
- "closedin (subtopology U u) u \<longleftrightarrow> u \<subseteq> topspace U"
+lemma closedin_subtopology_refl [simp]:
+ "closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
lemma openin_imp_subset:
- "openin (subtopology U s) t \<Longrightarrow> t \<subseteq> s"
+ "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
by (metis Int_iff openin_subtopology subsetI)
lemma closedin_imp_subset:
- "closedin (subtopology U s) t \<Longrightarrow> t \<subseteq> s"
+ "closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
by (simp add: closedin_def topspace_subtopology)
lemma openin_subtopology_Un:
- "openin (subtopology U t) s \<and> openin (subtopology U u) s
- \<Longrightarrow> openin (subtopology U (t \<union> u)) s"
+ "openin (subtopology U T) S \<and> openin (subtopology U u) S
+ \<Longrightarrow> openin (subtopology U (T \<union> u)) S"
by (simp add: openin_subtopology) blast
@@ -1061,6 +1061,9 @@
lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
by force
+lemma cball_diff_sphere: "cball a r - sphere a r = ball a r"
+ by auto
+
lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
by (simp add: subset_eq)
@@ -1073,6 +1076,12 @@
lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
by (simp add: set_eq_iff)
+lemma cball_max_Un: "cball a (max r s) = cball a r \<union> cball a s"
+ by (simp add: set_eq_iff) arith
+
+lemma cball_min_Int: "cball a (min r s) = cball a r \<inter> cball a s"
+ by (simp add: set_eq_iff)
+
lemma cball_diff_eq_sphere: "cball a r - ball a r = {x. dist x a = r}"
by (auto simp: cball_def ball_def dist_commute)
@@ -2463,6 +2472,54 @@
apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
using connected_component_eq_empty by blast
+proposition connected_Times:
+ assumes S: "connected S" and T: "connected T"
+ shows "connected (S \<times> T)"
+proof (clarsimp simp add: connected_iff_connected_component)
+ fix x y x' y'
+ assume xy: "x \<in> S" "y \<in> T" "x' \<in> S" "y' \<in> T"
+ with xy obtain U V where U: "connected U" "U \<subseteq> S" "x \<in> U" "x' \<in> U"
+ and V: "connected V" "V \<subseteq> T" "y \<in> V" "y' \<in> V"
+ using S T \<open>x \<in> S\<close> \<open>x' \<in> S\<close> by blast+
+ show "connected_component (S \<times> T) (x, y) (x', y')"
+ unfolding connected_component_def
+ proof (intro exI conjI)
+ show "connected ((\<lambda>x. (x, y)) ` U \<union> Pair x' ` V)"
+ proof (rule connected_Un)
+ have "continuous_on U (\<lambda>x. (x, y))"
+ by (intro continuous_intros)
+ then show "connected ((\<lambda>x. (x, y)) ` U)"
+ by (rule connected_continuous_image) (rule \<open>connected U\<close>)
+ have "continuous_on V (Pair x')"
+ by (intro continuous_intros)
+ then show "connected (Pair x' ` V)"
+ by (rule connected_continuous_image) (rule \<open>connected V\<close>)
+ qed (use U V in auto)
+ qed (use U V in auto)
+qed
+
+corollary connected_Times_eq [simp]:
+ "connected (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> connected S \<and> connected T" (is "?lhs = ?rhs")
+proof
+ assume L: ?lhs
+ show ?rhs
+ proof (cases "S = {} \<or> T = {}")
+ case True
+ then show ?thesis by auto
+ next
+ case False
+ have "connected (fst ` (S \<times> T))" "connected (snd ` (S \<times> T))"
+ using continuous_on_fst continuous_on_snd continuous_on_id
+ by (blast intro: connected_continuous_image [OF _ L])+
+ with False show ?thesis
+ by auto
+ qed
+next
+ assume ?rhs
+ then show ?lhs
+ by (auto simp: connected_Times)
+qed
+
subsection \<open>The set of connected components of a set\<close>
@@ -7240,7 +7297,7 @@
then have "\<forall>c\<in>{T. open T \<and> S \<inter> T \<in> C}. open c" and "S \<subseteq> \<Union>{T. open T \<and> S \<inter> T \<in> C}"
unfolding openin_open by force+
with \<open>compact S\<close> obtain D where "D \<subseteq> {T. open T \<and> S \<inter> T \<in> C}" and "finite D" and "S \<subseteq> \<Union>D"
- by (rule compactE)
+ by (meson compactE)
then have "image (\<lambda>T. S \<inter> T) D \<subseteq> C \<and> finite (image (\<lambda>T. S \<inter> T) D) \<and> S \<subseteq> \<Union>(image (\<lambda>T. S \<inter> T) D)"
by auto
then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
@@ -10189,7 +10246,7 @@
by metis
from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
- by (rule compactE)
+ by (meson compactE)
then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
by (force intro!: choice)
with * CC show ?thesis
--- a/src/HOL/Int.thy Mon Jan 02 18:08:04 2017 +0100
+++ b/src/HOL/Int.thy Tue Jan 03 16:48:49 2017 +0000
@@ -832,6 +832,10 @@
end
+lemma (in linordered_idom) Ints_abs [simp]:
+ shows "a \<in> \<int> \<Longrightarrow> abs a \<in> \<int>"
+ by (auto simp: abs_if)
+
lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}"
proof (intro subsetI equalityI)
fix x :: 'a
@@ -968,6 +972,24 @@
for z :: int
by arith
+lemma Ints_nonzero_abs_ge1:
+ fixes x:: "'a :: linordered_idom"
+ assumes "x \<in> Ints" "x \<noteq> 0"
+ shows "1 \<le> abs x"
+proof (rule Ints_cases [OF \<open>x \<in> Ints\<close>])
+ fix z::int
+ assume "x = of_int z"
+ with \<open>x \<noteq> 0\<close>
+ show "1 \<le> \<bar>x\<bar>"
+ apply (auto simp add: abs_if)
+ by (metis diff_0 of_int_1 of_int_le_iff of_int_minus zle_diff1_eq)
+qed
+
+lemma Ints_nonzero_abs_less1:
+ fixes x:: "'a :: linordered_idom"
+ shows "\<lbrakk>x \<in> Ints; abs x < 1\<rbrakk> \<Longrightarrow> x = 0"
+ using Ints_nonzero_abs_ge1 [of x] by auto
+
subsection \<open>The functions @{term nat} and @{term int}\<close>
--- a/src/HOL/Orderings.thy Mon Jan 02 18:08:04 2017 +0100
+++ b/src/HOL/Orderings.thy Tue Jan 03 16:48:49 2017 +0000
@@ -405,6 +405,10 @@
lemma not_le_imp_less: "\<not> y \<le> x \<Longrightarrow> x < y"
unfolding not_le .
+lemma linorder_less_wlog[case_names less refl sym]:
+ "\<lbrakk>\<And>a b. a < b \<Longrightarrow> P a b; \<And>a. P a a; \<And>a b. P b a \<Longrightarrow> P a b\<rbrakk> \<Longrightarrow> P a b"
+ using antisym_conv3 by blast
+
text \<open>Dual order\<close>
lemma dual_linorder:
--- a/src/HOL/Rat.thy Mon Jan 02 18:08:04 2017 +0100
+++ b/src/HOL/Rat.thy Tue Jan 03 16:48:49 2017 +0000
@@ -824,9 +824,15 @@
lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
by (subst of_rat_of_int_eq [symmetric]) (rule Rats_of_rat)
+lemma Ints_subset_Rats: "\<int> \<subseteq> \<rat>"
+ using Ints_cases Rats_of_int by blast
+
lemma Rats_of_nat [simp]: "of_nat n \<in> \<rat>"
by (subst of_rat_of_nat_eq [symmetric]) (rule Rats_of_rat)
+lemma Nats_subset_Rats: "\<nat> \<subseteq> \<rat>"
+ using Ints_subset_Rats Nats_subset_Ints by blast
+
lemma Rats_number_of [simp]: "numeral w \<in> \<rat>"
by (subst of_rat_numeral_eq [symmetric]) (rule Rats_of_rat)
--- a/src/HOL/Topological_Spaces.thy Mon Jan 02 18:08:04 2017 +0100
+++ b/src/HOL/Topological_Spaces.thy Tue Jan 03 16:48:49 2017 +0000
@@ -1547,6 +1547,18 @@
lemma tendsto_compose_filtermap: "((g \<circ> f) \<longlongrightarrow> T) F \<longleftrightarrow> (g \<longlongrightarrow> T) (filtermap f F)"
by (simp add: filterlim_def filtermap_filtermap comp_def)
+lemma tendsto_compose_at:
+ assumes f: "(f \<longlongrightarrow> y) F" and g: "(g \<longlongrightarrow> z) (at y)" and fg: "eventually (\<lambda>w. f w = y \<longrightarrow> g y = z) F"
+ shows "((g \<circ> f) \<longlongrightarrow> z) F"
+proof -
+ have "(\<forall>\<^sub>F a in F. f a \<noteq> y) \<or> g y = z"
+ using fg by force
+ moreover have "(g \<longlongrightarrow> z) (filtermap f F) \<or> \<not> (\<forall>\<^sub>F a in F. f a \<noteq> y)"
+ by (metis (no_types) filterlim_atI filterlim_def tendsto_mono f g)
+ ultimately show ?thesis
+ by (metis (no_types) f filterlim_compose filterlim_filtermap g tendsto_at_iff_tendsto_nhds tendsto_compose_filtermap)
+qed
+
subsubsection \<open>Relation of \<open>LIM\<close> and \<open>LIMSEQ\<close>\<close>
@@ -2087,12 +2099,10 @@
lemma compact_empty[simp]: "compact {}"
by (auto intro!: compactI)
-lemma compactE:
- assumes "compact s"
- and "\<forall>t\<in>C. open t"
- and "s \<subseteq> \<Union>C"
- obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'"
- using assms unfolding compact_eq_heine_borel by metis
+lemma compactE: (*related to COMPACT_IMP_HEINE_BOREL in HOL Light*)
+ assumes "compact S" "S \<subseteq> \<Union>\<T>" "\<And>B. B \<in> \<T> \<Longrightarrow> open B"
+ obtains \<T>' where "\<T>' \<subseteq> \<T>" "finite \<T>'" "S \<subseteq> \<Union>\<T>'"
+ by (meson assms compact_eq_heine_borel)
lemma compactE_image:
assumes "compact s"
@@ -2197,9 +2207,7 @@
fix y
assume "y \<in> - s"
let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
- note \<open>compact s\<close>
- moreover have "\<forall>u\<in>?C. open u" by simp
- moreover have "s \<subseteq> \<Union>?C"
+ have "s \<subseteq> \<Union>?C"
proof
fix x
assume "x \<in> s"
@@ -2209,8 +2217,8 @@
with \<open>x \<in> s\<close> show "x \<in> \<Union>?C"
unfolding eventually_nhds by auto
qed
- ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
- by (rule compactE)
+ then obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
+ by (rule compactE [OF \<open>compact s\<close>]) auto
from \<open>D \<subseteq> ?C\<close> have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)"
by auto
with \<open>finite D\<close> have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
--- a/src/HOL/Transcendental.thy Mon Jan 02 18:08:04 2017 +0100
+++ b/src/HOL/Transcendental.thy Tue Jan 03 16:48:49 2017 +0000
@@ -2370,6 +2370,53 @@
qed (rule exp_at_top)
qed
+subsubsection\<open> A couple of simple bounds\<close>
+
+lemma exp_plus_inverse_exp:
+ fixes x::real
+ shows "2 \<le> exp x + inverse (exp x)"
+proof -
+ have "2 \<le> exp x + exp (-x)"
+ using exp_ge_add_one_self [of x] exp_ge_add_one_self [of "-x"]
+ by linarith
+ then show ?thesis
+ by (simp add: exp_minus)
+qed
+
+lemma real_le_x_sinh:
+ fixes x::real
+ assumes "0 \<le> x"
+ shows "x \<le> (exp x - inverse(exp x)) / 2"
+proof -
+ have *: "exp a - inverse(exp a) - 2*a \<le> exp b - inverse(exp b) - 2*b" if "a \<le> b" for a b::real
+ apply (rule DERIV_nonneg_imp_nondecreasing [OF that])
+ using exp_plus_inverse_exp
+ apply (intro exI allI impI conjI derivative_eq_intros | force)+
+ done
+ show ?thesis
+ using*[OF assms] by simp
+qed
+
+lemma real_le_abs_sinh:
+ fixes x::real
+ shows "abs x \<le> abs((exp x - inverse(exp x)) / 2)"
+proof (cases "0 \<le> x")
+ case True
+ show ?thesis
+ using real_le_x_sinh [OF True] True by (simp add: abs_if)
+next
+ case False
+ have "-x \<le> (exp(-x) - inverse(exp(-x))) / 2"
+ by (meson False linear neg_le_0_iff_le real_le_x_sinh)
+ also have "... \<le> \<bar>(exp x - inverse (exp x)) / 2\<bar>"
+ by (metis (no_types, hide_lams) abs_divide abs_le_iff abs_minus_cancel
+ add.inverse_inverse exp_minus minus_diff_eq order_refl)
+ finally show ?thesis
+ using False by linarith
+qed
+
+subsection\<open>The general logarithm\<close>
+
definition log :: "real \<Rightarrow> real \<Rightarrow> real"
\<comment> \<open>logarithm of @{term x} to base @{term a}\<close>
where "log a x = ln x / ln a"