author paulson Tue Jan 03 16:48:49 2017 +0000 (2017-01-03) changeset 64758 3b33d2fc5fc0 parent 64757 7e3924224769 child 64768 34ef44748370
A few new lemmas and needed adaptations
 src/HOL/Analysis/Cauchy_Integral_Theorem.thy file | annotate | diff | revisions src/HOL/Analysis/Ordered_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Analysis/Topology_Euclidean_Space.thy file | annotate | diff | revisions src/HOL/Int.thy file | annotate | diff | revisions src/HOL/Orderings.thy file | annotate | diff | revisions src/HOL/Rat.thy file | annotate | diff | revisions src/HOL/Topological_Spaces.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Mon Jan 02 18:08:04 2017 +0100
1.2 +++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Jan 03 16:48:49 2017 +0000
1.3 @@ -4601,11 +4601,11 @@
1.4      by metis
1.5    note ee_rule = ee [THEN conjunct2, rule_format]
1.6    define C where "C = (\<lambda>t. ball t (ee t / 3)) ` {0..1}"
1.7 -  have "\<forall>t \<in> C. open t" by (simp add: C_def)
1.8 -  moreover have "{0..1} \<subseteq> \<Union>C"
1.9 -    using ee [THEN conjunct1] by (auto simp: C_def dist_norm)
1.10 -  ultimately obtain C' where C': "C' \<subseteq> C" "finite C'" and C'01: "{0..1} \<subseteq> \<Union>C'"
1.11 -    by (rule compactE [OF compact_interval])
1.12 +  obtain C' where C': "C' \<subseteq> C" "finite C'" and C'01: "{0..1} \<subseteq> \<Union>C'"
1.13 +  proof (rule compactE [OF compact_interval])
1.14 +    show "{0..1} \<subseteq> \<Union>C"
1.15 +      using ee [THEN conjunct1] by (auto simp: C_def dist_norm)
1.16 +  qed (use C_def in auto)
1.17    define kk where "kk = {t \<in> {0..1}. ball t (ee t / 3) \<in> C'}"
1.18    have kk01: "kk \<subseteq> {0..1}" by (auto simp: kk_def)
1.19    define e where "e = Min (ee ` kk)"
```
```     2.1 --- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Mon Jan 02 18:08:04 2017 +0100
2.2 +++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue Jan 03 16:48:49 2017 +0000
2.3 @@ -197,13 +197,13 @@
2.4    shows "closed {a..}"
2.6
2.7 -lemma bounded_closed_interval:
2.8 +lemma bounded_closed_interval [simp]:
2.9    fixes a :: "'a::ordered_euclidean_space"
2.10    shows "bounded {a .. b}"
2.11    using bounded_cbox[of a b]
2.12    by (metis interval_cbox)
2.13
2.14 -lemma convex_closed_interval:
2.15 +lemma convex_closed_interval [simp]:
2.16    fixes a :: "'a::ordered_euclidean_space"
2.17    shows "convex {a .. b}"
2.18    using convex_box[of a b]
2.19 @@ -214,11 +214,11 @@
2.20    using image_smult_cbox[of m a b]
2.22
2.23 -lemma is_interval_closed_interval:
2.24 +lemma is_interval_closed_interval [simp]:
2.25    "is_interval {a .. (b::'a::ordered_euclidean_space)}"
2.26    by (metis cbox_interval is_interval_cbox)
2.27
2.28 -lemma compact_interval:
2.29 +lemma compact_interval [simp]:
2.30    fixes a b::"'a::ordered_euclidean_space"
2.31    shows "compact {a .. b}"
2.32    by (metis compact_cbox interval_cbox)
```
```     3.1 --- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Jan 02 18:08:04 2017 +0100
3.2 +++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Jan 03 16:48:49 2017 +0000
3.3 @@ -794,28 +794,28 @@
3.5
3.6  lemma openin_subtopology_empty:
3.7 -   "openin (subtopology U {}) s \<longleftrightarrow> s = {}"
3.8 +   "openin (subtopology U {}) S \<longleftrightarrow> S = {}"
3.9  by (metis Int_empty_right openin_empty openin_subtopology)
3.10
3.11  lemma closedin_subtopology_empty:
3.12 -   "closedin (subtopology U {}) s \<longleftrightarrow> s = {}"
3.13 +   "closedin (subtopology U {}) S \<longleftrightarrow> S = {}"
3.14  by (metis Int_empty_right closedin_empty closedin_subtopology)
3.15
3.16 -lemma closedin_subtopology_refl:
3.17 -   "closedin (subtopology U u) u \<longleftrightarrow> u \<subseteq> topspace U"
3.18 +lemma closedin_subtopology_refl [simp]:
3.19 +   "closedin (subtopology U X) X \<longleftrightarrow> X \<subseteq> topspace U"
3.20  by (metis closedin_def closedin_topspace inf.absorb_iff2 le_inf_iff topspace_subtopology)
3.21
3.22  lemma openin_imp_subset:
3.23 -   "openin (subtopology U s) t \<Longrightarrow> t \<subseteq> s"
3.24 +   "openin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
3.25  by (metis Int_iff openin_subtopology subsetI)
3.26
3.27  lemma closedin_imp_subset:
3.28 -   "closedin (subtopology U s) t \<Longrightarrow> t \<subseteq> s"
3.29 +   "closedin (subtopology U S) T \<Longrightarrow> T \<subseteq> S"
3.30  by (simp add: closedin_def topspace_subtopology)
3.31
3.32  lemma openin_subtopology_Un:
3.33 -    "openin (subtopology U t) s \<and> openin (subtopology U u) s
3.34 -     \<Longrightarrow> openin (subtopology U (t \<union> u)) s"
3.35 +    "openin (subtopology U T) S \<and> openin (subtopology U u) S
3.36 +     \<Longrightarrow> openin (subtopology U (T \<union> u)) S"
3.37  by (simp add: openin_subtopology) blast
3.38
3.39
3.40 @@ -1061,6 +1061,9 @@
3.41  lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
3.42    by force
3.43
3.44 +lemma cball_diff_sphere: "cball a r - sphere a r = ball a r"
3.45 +  by auto
3.46 +
3.47  lemma subset_ball[intro]: "d \<le> e \<Longrightarrow> ball x d \<subseteq> ball x e"
3.49
3.50 @@ -1073,6 +1076,12 @@
3.51  lemma ball_min_Int: "ball a (min r s) = ball a r \<inter> ball a s"
3.53
3.54 +lemma cball_max_Un: "cball a (max r s) = cball a r \<union> cball a s"
3.55 +  by (simp add: set_eq_iff) arith
3.56 +
3.57 +lemma cball_min_Int: "cball a (min r s) = cball a r \<inter> cball a s"
3.58 +  by (simp add: set_eq_iff)
3.59 +
3.60  lemma cball_diff_eq_sphere: "cball a r - ball a r =  {x. dist x a = r}"
3.61    by (auto simp: cball_def ball_def dist_commute)
3.62
3.63 @@ -2463,6 +2472,54 @@
3.64    apply (simp add: connected_component_maximal connected_component_mono subset_antisym)
3.65    using connected_component_eq_empty by blast
3.66
3.67 +proposition connected_Times:
3.68 +  assumes S: "connected S" and T: "connected T"
3.69 +  shows "connected (S \<times> T)"
3.70 +proof (clarsimp simp add: connected_iff_connected_component)
3.71 +  fix x y x' y'
3.72 +  assume xy: "x \<in> S" "y \<in> T" "x' \<in> S" "y' \<in> T"
3.73 +  with xy obtain U V where U: "connected U" "U \<subseteq> S" "x \<in> U" "x' \<in> U"
3.74 +                       and V: "connected V" "V \<subseteq> T" "y \<in> V" "y' \<in> V"
3.75 +    using S T \<open>x \<in> S\<close> \<open>x' \<in> S\<close> by blast+
3.76 +  show "connected_component (S \<times> T) (x, y) (x', y')"
3.77 +    unfolding connected_component_def
3.78 +  proof (intro exI conjI)
3.79 +    show "connected ((\<lambda>x. (x, y)) ` U \<union> Pair x' ` V)"
3.80 +    proof (rule connected_Un)
3.81 +      have "continuous_on U (\<lambda>x. (x, y))"
3.82 +        by (intro continuous_intros)
3.83 +      then show "connected ((\<lambda>x. (x, y)) ` U)"
3.84 +        by (rule connected_continuous_image) (rule \<open>connected U\<close>)
3.85 +      have "continuous_on V (Pair x')"
3.86 +        by (intro continuous_intros)
3.87 +      then show "connected (Pair x' ` V)"
3.88 +        by (rule connected_continuous_image) (rule \<open>connected V\<close>)
3.89 +    qed (use U V in auto)
3.90 +  qed (use U V in auto)
3.91 +qed
3.92 +
3.93 +corollary connected_Times_eq [simp]:
3.94 +   "connected (S \<times> T) \<longleftrightarrow> S = {} \<or> T = {} \<or> connected S \<and> connected T"  (is "?lhs = ?rhs")
3.95 +proof
3.96 +  assume L: ?lhs
3.97 +  show ?rhs
3.98 +  proof (cases "S = {} \<or> T = {}")
3.99 +    case True
3.100 +    then show ?thesis by auto
3.101 +  next
3.102 +    case False
3.103 +    have "connected (fst ` (S \<times> T))" "connected (snd ` (S \<times> T))"
3.104 +      using continuous_on_fst continuous_on_snd continuous_on_id
3.105 +      by (blast intro: connected_continuous_image [OF _ L])+
3.106 +    with False show ?thesis
3.107 +      by auto
3.108 +  qed
3.109 +next
3.110 +  assume ?rhs
3.111 +  then show ?lhs
3.112 +    by (auto simp: connected_Times)
3.113 +qed
3.114 +
3.115
3.116  subsection \<open>The set of connected components of a set\<close>
3.117
3.118 @@ -7240,7 +7297,7 @@
3.119    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}"
3.120      unfolding openin_open by force+
3.121    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"
3.122 -    by (rule compactE)
3.123 +    by (meson compactE)
3.124    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)"
3.125      by auto
3.126    then show "\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D" ..
3.127 @@ -10189,7 +10246,7 @@
3.128      by metis
3.129    from * have "\<forall>t\<in>Y ` K. open t" "K \<subseteq> \<Union>(Y ` K)" by auto
3.130    with \<open>compact K\<close> obtain CC where CC: "CC \<subseteq> Y ` K" "finite CC" "K \<subseteq> \<Union>CC"
3.131 -    by (rule compactE)
3.132 +    by (meson compactE)
3.133    then obtain c where c: "\<And>C. C \<in> CC \<Longrightarrow> c C \<in> K \<and> C = Y (c C)"
3.134      by (force intro!: choice)
3.135    with * CC show ?thesis
```
```     4.1 --- a/src/HOL/Int.thy	Mon Jan 02 18:08:04 2017 +0100
4.2 +++ b/src/HOL/Int.thy	Tue Jan 03 16:48:49 2017 +0000
4.3 @@ -832,6 +832,10 @@
4.4
4.5  end
4.6
4.7 +lemma (in linordered_idom) Ints_abs [simp]:
4.8 +  shows "a \<in> \<int> \<Longrightarrow> abs a \<in> \<int>"
4.9 +  by (auto simp: abs_if)
4.10 +
4.11  lemma (in linordered_idom) Nats_altdef2: "\<nat> = {n \<in> \<int>. n \<ge> 0}"
4.12  proof (intro subsetI equalityI)
4.13    fix x :: 'a
4.14 @@ -968,6 +972,24 @@
4.15    for z :: int
4.16    by arith
4.17
4.18 +lemma Ints_nonzero_abs_ge1:
4.19 +  fixes x:: "'a :: linordered_idom"
4.20 +    assumes "x \<in> Ints" "x \<noteq> 0"
4.21 +    shows "1 \<le> abs x"
4.22 +proof (rule Ints_cases [OF \<open>x \<in> Ints\<close>])
4.23 +  fix z::int
4.24 +  assume "x = of_int z"
4.25 +    with \<open>x \<noteq> 0\<close>
4.26 +  show "1 \<le> \<bar>x\<bar>"
4.27 +    apply (auto simp add: abs_if)
4.28 +    by (metis diff_0 of_int_1 of_int_le_iff of_int_minus zle_diff1_eq)
4.29 +qed
4.30 +
4.31 +lemma Ints_nonzero_abs_less1:
4.32 +  fixes x:: "'a :: linordered_idom"
4.33 +  shows "\<lbrakk>x \<in> Ints; abs x < 1\<rbrakk> \<Longrightarrow> x = 0"
4.34 +    using Ints_nonzero_abs_ge1 [of x] by auto
4.35 +
4.36
4.37  subsection \<open>The functions @{term nat} and @{term int}\<close>
4.38
```
```     5.1 --- a/src/HOL/Orderings.thy	Mon Jan 02 18:08:04 2017 +0100
5.2 +++ b/src/HOL/Orderings.thy	Tue Jan 03 16:48:49 2017 +0000
5.3 @@ -405,6 +405,10 @@
5.4  lemma not_le_imp_less: "\<not> y \<le> x \<Longrightarrow> x < y"
5.5  unfolding not_le .
5.6
5.7 +lemma linorder_less_wlog[case_names less refl sym]:
5.8 +     "\<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"
5.9 +  using antisym_conv3 by blast
5.10 +
5.11  text \<open>Dual order\<close>
5.12
5.13  lemma dual_linorder:
```
```     6.1 --- a/src/HOL/Rat.thy	Mon Jan 02 18:08:04 2017 +0100
6.2 +++ b/src/HOL/Rat.thy	Tue Jan 03 16:48:49 2017 +0000
6.3 @@ -824,9 +824,15 @@
6.4  lemma Rats_of_int [simp]: "of_int z \<in> \<rat>"
6.5    by (subst of_rat_of_int_eq [symmetric]) (rule Rats_of_rat)
6.6
6.7 +lemma Ints_subset_Rats: "\<int> \<subseteq> \<rat>"
6.8 +  using Ints_cases Rats_of_int by blast
6.9 +
6.10  lemma Rats_of_nat [simp]: "of_nat n \<in> \<rat>"
6.11    by (subst of_rat_of_nat_eq [symmetric]) (rule Rats_of_rat)
6.12
6.13 +lemma Nats_subset_Rats: "\<nat> \<subseteq> \<rat>"
6.14 +  using Ints_subset_Rats Nats_subset_Ints by blast
6.15 +
6.16  lemma Rats_number_of [simp]: "numeral w \<in> \<rat>"
6.17    by (subst of_rat_numeral_eq [symmetric]) (rule Rats_of_rat)
6.18
```
```     7.1 --- a/src/HOL/Topological_Spaces.thy	Mon Jan 02 18:08:04 2017 +0100
7.2 +++ b/src/HOL/Topological_Spaces.thy	Tue Jan 03 16:48:49 2017 +0000
7.3 @@ -1547,6 +1547,18 @@
7.4  lemma tendsto_compose_filtermap: "((g \<circ> f) \<longlongrightarrow> T) F \<longleftrightarrow> (g \<longlongrightarrow> T) (filtermap f F)"
7.5    by (simp add: filterlim_def filtermap_filtermap comp_def)
7.6
7.7 +lemma tendsto_compose_at:
7.8 +  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"
7.9 +  shows "((g \<circ> f) \<longlongrightarrow> z) F"
7.10 +proof -
7.11 +  have "(\<forall>\<^sub>F a in F. f a \<noteq> y) \<or> g y = z"
7.12 +    using fg by force
7.13 +  moreover have "(g \<longlongrightarrow> z) (filtermap f F) \<or> \<not> (\<forall>\<^sub>F a in F. f a \<noteq> y)"
7.14 +    by (metis (no_types) filterlim_atI filterlim_def tendsto_mono f g)
7.15 +  ultimately show ?thesis
7.16 +    by (metis (no_types) f filterlim_compose filterlim_filtermap g tendsto_at_iff_tendsto_nhds tendsto_compose_filtermap)
7.17 +qed
7.18 +
7.19
7.20  subsubsection \<open>Relation of \<open>LIM\<close> and \<open>LIMSEQ\<close>\<close>
7.21
7.22 @@ -2087,12 +2099,10 @@
7.23  lemma compact_empty[simp]: "compact {}"
7.24    by (auto intro!: compactI)
7.25
7.26 -lemma compactE:
7.27 -  assumes "compact s"
7.28 -    and "\<forall>t\<in>C. open t"
7.29 -    and "s \<subseteq> \<Union>C"
7.30 -  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> \<Union>C'"
7.31 -  using assms unfolding compact_eq_heine_borel by metis
7.32 +lemma compactE: (*related to COMPACT_IMP_HEINE_BOREL in HOL Light*)
7.33 +  assumes "compact S" "S \<subseteq> \<Union>\<T>" "\<And>B. B \<in> \<T> \<Longrightarrow> open B"
7.34 +  obtains \<T>' where "\<T>' \<subseteq> \<T>" "finite \<T>'" "S \<subseteq> \<Union>\<T>'"
7.35 +  by (meson assms compact_eq_heine_borel)
7.36
7.37  lemma compactE_image:
7.38    assumes "compact s"
7.39 @@ -2197,9 +2207,7 @@
7.40    fix y
7.41    assume "y \<in> - s"
7.42    let ?C = "\<Union>x\<in>s. {u. open u \<and> x \<in> u \<and> eventually (\<lambda>y. y \<notin> u) (nhds y)}"
7.43 -  note \<open>compact s\<close>
7.44 -  moreover have "\<forall>u\<in>?C. open u" by simp
7.45 -  moreover have "s \<subseteq> \<Union>?C"
7.46 +  have "s \<subseteq> \<Union>?C"
7.47    proof
7.48      fix x
7.49      assume "x \<in> s"
7.50 @@ -2209,8 +2217,8 @@
7.51      with \<open>x \<in> s\<close> show "x \<in> \<Union>?C"
7.52        unfolding eventually_nhds by auto
7.53    qed
7.54 -  ultimately obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
7.55 -    by (rule compactE)
7.56 +  then obtain D where "D \<subseteq> ?C" and "finite D" and "s \<subseteq> \<Union>D"
7.57 +    by (rule compactE [OF \<open>compact s\<close>]) auto
7.58    from \<open>D \<subseteq> ?C\<close> have "\<forall>x\<in>D. eventually (\<lambda>y. y \<notin> x) (nhds y)"
7.59      by auto
7.60    with \<open>finite D\<close> have "eventually (\<lambda>y. y \<notin> \<Union>D) (nhds y)"
```
```     8.1 --- a/src/HOL/Transcendental.thy	Mon Jan 02 18:08:04 2017 +0100
8.2 +++ b/src/HOL/Transcendental.thy	Tue Jan 03 16:48:49 2017 +0000
8.3 @@ -2370,6 +2370,53 @@
8.4    qed (rule exp_at_top)
8.5  qed
8.6
8.7 +subsubsection\<open> A couple of simple bounds\<close>
8.8 +
8.9 +lemma exp_plus_inverse_exp:
8.10 +  fixes x::real
8.11 +  shows "2 \<le> exp x + inverse (exp x)"
8.12 +proof -
8.13 +  have "2 \<le> exp x + exp (-x)"
8.15 +    by linarith
8.16 +  then show ?thesis
8.17 +    by (simp add: exp_minus)
8.18 +qed
8.19 +
8.20 +lemma real_le_x_sinh:
8.21 +  fixes x::real
8.22 +  assumes "0 \<le> x"
8.23 +  shows "x \<le> (exp x - inverse(exp x)) / 2"
8.24 +proof -
8.25 +  have *: "exp a - inverse(exp a) - 2*a \<le> exp b - inverse(exp b) - 2*b" if "a \<le> b" for a b::real
8.26 +    apply (rule DERIV_nonneg_imp_nondecreasing [OF that])
8.27 +    using exp_plus_inverse_exp
8.28 +    apply (intro exI allI impI conjI derivative_eq_intros | force)+
8.29 +    done
8.30 +  show ?thesis
8.31 +    using*[OF assms] by simp
8.32 +qed
8.33 +
8.34 +lemma real_le_abs_sinh:
8.35 +  fixes x::real
8.36 +  shows "abs x \<le> abs((exp x - inverse(exp x)) / 2)"
8.37 +proof (cases "0 \<le> x")
8.38 +  case True
8.39 +  show ?thesis
8.40 +    using real_le_x_sinh [OF True] True by (simp add: abs_if)
8.41 +next
8.42 +  case False
8.43 +  have "-x \<le> (exp(-x) - inverse(exp(-x))) / 2"
8.44 +    by (meson False linear neg_le_0_iff_le real_le_x_sinh)
8.45 +  also have "... \<le> \<bar>(exp x - inverse (exp x)) / 2\<bar>"
8.46 +    by (metis (no_types, hide_lams) abs_divide abs_le_iff abs_minus_cancel
8.47 +       add.inverse_inverse exp_minus minus_diff_eq order_refl)
8.48 +  finally show ?thesis
8.49 +    using False by linarith
8.50 +qed
8.51 +
8.52 +subsection\<open>The general logarithm\<close>
8.53 +
8.54  definition log :: "real \<Rightarrow> real \<Rightarrow> real"
8.55    \<comment> \<open>logarithm of @{term x} to base @{term a}\<close>
8.56    where "log a x = ln x / ln a"
```