A few new lemmas and needed adaptations
authorpaulson <lp15@cam.ac.uk>
Tue Jan 03 16:48:49 2017 +0000 (2017-01-03)
changeset 647583b33d2fc5fc0
parent 64757 7e3924224769
child 64768 34ef44748370
A few new lemmas and needed adaptations
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
src/HOL/Analysis/Ordered_Euclidean_Space.thy
src/HOL/Analysis/Topology_Euclidean_Space.thy
src/HOL/Int.thy
src/HOL/Orderings.thy
src/HOL/Rat.thy
src/HOL/Topological_Spaces.thy
src/HOL/Transcendental.thy
     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.5    by (simp add: eucl_le_atLeast[symmetric])
     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.21    by (simp add: cbox_interval)
    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.4    by (simp add: subtopology_superset)
     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.48    by (simp add: subset_eq)
    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.52    by (simp add: set_eq_iff)
    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.14 +    using exp_ge_add_one_self [of x] exp_ge_add_one_self [of "-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"