src/HOL/Analysis/Starlike.thy
 changeset 66793 deabce3ccf1f parent 66765 c1dfa973b269 child 66884 c2128ab11f61
```     1.1 --- a/src/HOL/Analysis/Starlike.thy	Sun Oct 08 16:50:37 2017 +0200
1.2 +++ b/src/HOL/Analysis/Starlike.thy	Mon Oct 09 15:34:23 2017 +0100
1.3 @@ -3776,24 +3776,6 @@
1.4
1.5  subsection\<open>Explicit formulas for interior and relative interior of convex hull\<close>
1.6
1.7 -lemma interior_atLeastAtMost [simp]:
1.8 -  fixes a::real shows "interior {a..b} = {a<..<b}"
1.9 -  using interior_cbox [of a b] by auto
1.10 -
1.11 -lemma interior_atLeastLessThan [simp]:
1.12 -  fixes a::real shows "interior {a..<b} = {a<..<b}"
1.13 -  by (metis atLeastLessThan_def greaterThanLessThan_def interior_atLeastAtMost interior_Int interior_interior interior_real_semiline)
1.14 -
1.15 -lemma interior_lessThanAtMost [simp]:
1.16 -  fixes a::real shows "interior {a<..b} = {a<..<b}"
1.17 -  by (metis atLeastAtMost_def greaterThanAtMost_def interior_atLeastAtMost interior_Int
1.18 -            interior_interior interior_real_semiline)
1.19 -
1.20 -lemma at_within_closed_interval:
1.21 -    fixes x::real
1.22 -    shows "a < x \<Longrightarrow> x < b \<Longrightarrow> (at x within {a..b}) = at x"
1.23 -  by (metis at_within_interior greaterThanLessThan_iff interior_atLeastAtMost)
1.24 -
1.25  lemma at_within_cbox_finite:
1.26    assumes "x \<in> box a b" "x \<notin> S" "finite S"
1.27    shows "(at x within cbox a b - S) = at x"
1.28 @@ -5087,7 +5069,6 @@
1.29  using separation_closures [of S T]
1.30  by (metis assms closure_closed disjnt_def inf_commute)
1.31
1.32 -
1.33  lemma separation_normal_local:
1.34    fixes S :: "'a::euclidean_space set"
1.35    assumes US: "closedin (subtopology euclidean U) S"
1.36 @@ -5147,6 +5128,139 @@
1.37      by auto (meson bounded_ball bounded_subset compl_le_swap2 disjoint_eq_subset_Compl)
1.38  qed
1.39
1.40 +subsection\<open>Connectedness of the intersection of a chain\<close>
1.41 +
1.42 +proposition connected_chain:
1.43 +  fixes \<F> :: "'a :: euclidean_space set set"
1.44 +  assumes cc: "\<And>S. S \<in> \<F> \<Longrightarrow> compact S \<and> connected S"
1.45 +      and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
1.46 +  shows "connected(\<Inter>\<F>)"
1.47 +proof (cases "\<F> = {}")
1.48 +  case True then show ?thesis
1.49 +    by auto
1.50 +next
1.51 +  case False
1.52 +  then have cf: "compact(\<Inter>\<F>)"
1.53 +    by (simp add: cc compact_Inter)
1.54 +  have False if AB: "closed A" "closed B" "A \<inter> B = {}"
1.55 +                and ABeq: "A \<union> B = \<Inter>\<F>" and "A \<noteq> {}" "B \<noteq> {}" for A B
1.56 +  proof -
1.57 +    obtain U V where "open U" "open V" "A \<subseteq> U" "B \<subseteq> V" "U \<inter> V = {}"
1.58 +      using separation_normal [OF AB] by metis
1.59 +    obtain K where "K \<in> \<F>" "compact K"
1.60 +      using cc False by blast
1.61 +    then obtain N where "open N" and "K \<subseteq> N"
1.62 +      by blast
1.63 +    let ?\<C> = "insert (U \<union> V) ((\<lambda>S. N - S) ` \<F>)"
1.64 +    obtain \<D> where "\<D> \<subseteq> ?\<C>" "finite \<D>" "K \<subseteq> \<Union>\<D>"
1.65 +    proof (rule compactE [OF \<open>compact K\<close>])
1.66 +      show "K \<subseteq> \<Union>insert (U \<union> V) (op - N ` \<F>)"
1.67 +        using \<open>K \<subseteq> N\<close> ABeq \<open>A \<subseteq> U\<close> \<open>B \<subseteq> V\<close> by auto
1.68 +      show "\<And>B. B \<in> insert (U \<union> V) (op - N ` \<F>) \<Longrightarrow> open B"
1.69 +        by (auto simp:  \<open>open U\<close> \<open>open V\<close> open_Un \<open>open N\<close> cc compact_imp_closed open_Diff)
1.70 +    qed
1.71 +    then have "finite(\<D> - {U \<union> V})"
1.72 +      by blast
1.73 +    moreover have "\<D> - {U \<union> V} \<subseteq> (\<lambda>S. N - S) ` \<F>"
1.74 +      using \<open>\<D> \<subseteq> ?\<C>\<close> by blast
1.75 +    ultimately obtain \<G> where "\<G> \<subseteq> \<F>" "finite \<G>" and Deq: "\<D> - {U \<union> V} = (\<lambda>S. N-S) ` \<G>"
1.76 +      using finite_subset_image by metis
1.77 +    obtain J where "J \<in> \<F>" and J: "(\<Union>S\<in>\<G>. N - S) \<subseteq> N - J"
1.78 +    proof (cases "\<G> = {}")
1.79 +      case True
1.80 +      with \<open>\<F> \<noteq> {}\<close> that show ?thesis
1.81 +        by auto
1.82 +    next
1.83 +      case False
1.84 +      have "\<And>S T. \<lbrakk>S \<in> \<G>; T \<in> \<G>\<rbrakk> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
1.85 +        by (meson \<open>\<G> \<subseteq> \<F>\<close> in_mono local.linear)
1.86 +      with \<open>finite \<G>\<close> \<open>\<G> \<noteq> {}\<close>
1.87 +      have "\<exists>J \<in> \<G>. (\<Union>S\<in>\<G>. N - S) \<subseteq> N - J"
1.88 +      proof induction
1.89 +        case (insert X \<H>)
1.90 +        show ?case
1.91 +        proof (cases "\<H> = {}")
1.92 +          case True then show ?thesis by auto
1.93 +        next
1.94 +          case False
1.95 +          then have "\<And>S T. \<lbrakk>S \<in> \<H>; T \<in> \<H>\<rbrakk> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
1.96 +            by (simp add: insert.prems)
1.97 +          with insert.IH False obtain J where "J \<in> \<H>" and J: "(\<Union>Y\<in>\<H>. N - Y) \<subseteq> N - J"
1.98 +            by metis
1.99 +          have "N - J \<subseteq> N - X \<or> N - X \<subseteq> N - J"
1.100 +            by (meson Diff_mono \<open>J \<in> \<H>\<close> insert.prems(2) insert_iff order_refl)
1.101 +          then show ?thesis
1.102 +          proof
1.103 +            assume "N - J \<subseteq> N - X" with J show ?thesis
1.104 +              by auto
1.105 +          next
1.106 +            assume "N - X \<subseteq> N - J"
1.107 +            with J have "N - X \<union> UNION \<H> (op - N) \<subseteq> N - J"
1.108 +              by auto
1.109 +            with \<open>J \<in> \<H>\<close> show ?thesis
1.110 +              by blast
1.111 +          qed
1.112 +        qed
1.113 +      qed simp
1.114 +      with \<open>\<G> \<subseteq> \<F>\<close> show ?thesis by (blast intro: that)
1.115 +    qed
1.116 +    have "K \<subseteq> \<Union>(insert (U \<union> V) (\<D> - {U \<union> V}))"
1.117 +      using \<open>K \<subseteq> \<Union>\<D>\<close> by auto
1.118 +    also have "... \<subseteq> (U \<union> V) \<union> (N - J)"
1.119 +      by (metis (no_types, hide_lams) Deq Un_subset_iff Un_upper2 J Union_insert order_trans sup_ge1)
1.120 +    finally have "J \<inter> K \<subseteq> U \<union> V"
1.121 +      by blast
1.122 +    moreover have "connected(J \<inter> K)"
1.123 +      by (metis Int_absorb1 \<open>J \<in> \<F>\<close> \<open>K \<in> \<F>\<close> cc inf.orderE local.linear)
1.124 +    moreover have "U \<inter> (J \<inter> K) \<noteq> {}"
1.125 +      using ABeq \<open>J \<in> \<F>\<close> \<open>K \<in> \<F>\<close> \<open>A \<noteq> {}\<close> \<open>A \<subseteq> U\<close> by blast
1.126 +    moreover have "V \<inter> (J \<inter> K) \<noteq> {}"
1.127 +      using ABeq \<open>J \<in> \<F>\<close> \<open>K \<in> \<F>\<close> \<open>B \<noteq> {}\<close> \<open>B \<subseteq> V\<close> by blast
1.128 +    ultimately show False
1.129 +        using connectedD [of "J \<inter> K" U V] \<open>open U\<close> \<open>open V\<close> \<open>U \<inter> V = {}\<close>  by auto
1.130 +  qed
1.131 +  with cf show ?thesis
1.132 +    by (auto simp: connected_closed_set compact_imp_closed)
1.133 +qed
1.134 +
1.135 +lemma connected_chain_gen:
1.136 +  fixes \<F> :: "'a :: euclidean_space set set"
1.137 +  assumes X: "X \<in> \<F>" "compact X"
1.138 +      and cc: "\<And>T. T \<in> \<F> \<Longrightarrow> closed T \<and> connected T"
1.139 +      and linear: "\<And>S T. S \<in> \<F> \<and> T \<in> \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
1.140 +  shows "connected(\<Inter>\<F>)"
1.141 +proof -
1.142 +  have "\<Inter>\<F> = (\<Inter>T\<in>\<F>. X \<inter> T)"
1.143 +    using X by blast
1.144 +  moreover have "connected (\<Inter>T\<in>\<F>. X \<inter> T)"
1.145 +  proof (rule connected_chain)
1.146 +    show "\<And>T. T \<in> op \<inter> X ` \<F> \<Longrightarrow> compact T \<and> connected T"
1.147 +      using cc X by auto (metis inf.absorb2 inf.orderE local.linear)
1.148 +    show "\<And>S T. S \<in> op \<inter> X ` \<F> \<and> T \<in> op \<inter> X ` \<F> \<Longrightarrow> S \<subseteq> T \<or> T \<subseteq> S"
1.149 +      using local.linear by blast
1.150 +  qed
1.151 +  ultimately show ?thesis
1.152 +    by metis
1.153 +qed
1.154 +
1.155 +lemma connected_nest:
1.156 +  fixes S :: "'a::linorder \<Rightarrow> 'b::euclidean_space set"
1.157 +  assumes S: "\<And>n. compact(S n)" "\<And>n. connected(S n)"
1.158 +    and nest: "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
1.159 +  shows "connected(\<Inter> (range S))"
1.160 +  apply (rule connected_chain)
1.161 +  using S apply blast
1.162 +  by (metis image_iff le_cases nest)
1.163 +
1.164 +lemma connected_nest_gen:
1.165 +  fixes S :: "'a::linorder \<Rightarrow> 'b::euclidean_space set"
1.166 +  assumes S: "\<And>n. closed(S n)" "\<And>n. connected(S n)" "compact(S k)"
1.167 +    and nest: "\<And>m n. m \<le> n \<Longrightarrow> S n \<subseteq> S m"
1.168 +  shows "connected(\<Inter> (range S))"
1.169 +  apply (rule connected_chain_gen [of "S k"])
1.170 +  using S apply auto
1.171 +  by (meson le_cases nest subsetCE)
1.172 +
1.173  subsection\<open>Proper maps, including projections out of compact sets\<close>
1.174
1.175  lemma finite_indexed_bound:
```