# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1483462129 0
# Node ID 3b33d2fc5fc01a66d96f0d914168f0061bb89e8e
# Parent  7e3924224769346df21d06eed2a14884fd0d2a31
A few new lemmas and needed adaptations

diff -r 7e3924224769 -r 3b33d2fc5fc0 src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- 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)"
diff -r 7e3924224769 -r 3b33d2fc5fc0 src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- 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)
diff -r 7e3924224769 -r 3b33d2fc5fc0 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- 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
diff -r 7e3924224769 -r 3b33d2fc5fc0 src/HOL/Int.thy
--- 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>
 
diff -r 7e3924224769 -r 3b33d2fc5fc0 src/HOL/Orderings.thy
--- 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:
diff -r 7e3924224769 -r 3b33d2fc5fc0 src/HOL/Rat.thy
--- 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)
 
diff -r 7e3924224769 -r 3b33d2fc5fc0 src/HOL/Topological_Spaces.thy
--- 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)"
diff -r 7e3924224769 -r 3b33d2fc5fc0 src/HOL/Transcendental.thy
--- 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"