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: