move compact to the HOL image; prove compactness of real closed intervals; show that continuous functions attain supremum and infimum on compact sets

--- a/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Deriv.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -566,30 +566,65 @@
 done
 
 
+lemma compact_Icc[simp, intro]: "compact {a .. b::real}"
+proof (cases "a \<le> b", rule compactI)
+  fix C assume C: "a \<le> b" "\<forall>t\<in>C. open t" "{a..b} \<subseteq> \<Union>C"
+  def T == "{a .. b}"
+  from C(1,3) show "\<exists>C'\<subseteq>C. finite C' \<and> {a..b} \<subseteq> \<Union>C'"
+  proof (induct rule: Bolzano)
+    case (trans a b c)
+    then have *: "{a .. c} = {a .. b} \<union> {b .. c}" by auto
+    from trans obtain C1 C2 where "C1\<subseteq>C \<and> finite C1 \<and> {a..b} \<subseteq> \<Union>C1" "C2\<subseteq>C \<and> finite C2 \<and> {b..c} \<subseteq> \<Union>C2"
+      by (auto simp: *)
+    with trans show ?case
+      unfolding * by (intro exI[of _ "C1 \<union> C2"]) auto
+  next
+    case (local x)
+    then have "x \<in> \<Union>C" using C by auto
+    with C(2) obtain c where "x \<in> c" "open c" "c \<in> C" by auto
+    then obtain e where "0 < e" "{x - e <..< x + e} \<subseteq> c"
+      by (auto simp: open_real_def dist_real_def subset_eq Ball_def abs_less_iff)
+    with `c \<in> C` show ?case
+      by (safe intro!: exI[of _ "e/2"] exI[of _ "{c}"]) auto
+  qed
+qed simp
+
 subsection {* Boundedness of continuous functions *}
 
 text{*By bisection, function continuous on closed interval is bounded above*}
 
+lemma isCont_eq_Ub:
+  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
+  shows "a \<le> b \<Longrightarrow> \<forall>x::real. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
+    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
+  using continuous_attains_sup[of "{a .. b}" f]
+  apply (simp add: continuous_at_imp_continuous_on Ball_def)
+  apply safe
+  apply (rule_tac x="f x" in exI)
+  apply auto
+  done
+
+lemma isCont_eq_Lb:
+  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
+  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
+    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> M \<le> f x) \<and> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
+  using continuous_attains_inf[of "{a .. b}" f]
+  apply (simp add: continuous_at_imp_continuous_on Ball_def)
+  apply safe
+  apply (rule_tac x="f x" in exI)
+  apply auto
+  done
+
 lemma isCont_bounded:
-     "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
-      ==> \<exists>M::real. \<forall>x::real. a \<le> x & x \<le> b --> f(x) \<le> M"
-apply (cut_tac P = "% (u,v) . a \<le> u & u \<le> v & v \<le> b --> (\<exists>M. \<forall>x. u \<le> x & x \<le> v --> f x \<le> M)" in lemma_BOLZANO2)
-apply safe
-apply simp_all
-apply (rename_tac x xa ya M Ma)
-apply (metis linorder_not_less order_le_less order_trans)
-apply (case_tac "a \<le> x & x \<le> b")
- prefer 2
- apply (rule_tac x = 1 in exI, force)
-apply (simp add: LIM_eq isCont_iff)
-apply (drule_tac x = x in spec, auto)
-apply (erule_tac V = "\<forall>M. \<exists>x. a \<le> x & x \<le> b & ~ f x \<le> M" in thin_rl)
-apply (drule_tac x = 1 in spec, auto)
-apply (rule_tac x = s in exI, clarify)
-apply (rule_tac x = "\<bar>f x\<bar> + 1" in exI, clarify)
-apply (drule_tac x = "xa-x" in spec)
-apply (auto simp add: abs_ge_self)
-done
+  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
+  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow> \<exists>M. \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M"
+  using isCont_eq_Ub[of a b f] by auto
+
+lemma isCont_has_Ub:
+  fixes f :: "real \<Rightarrow> 'a::linorder_topology"
+  shows "a \<le> b \<Longrightarrow> \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> isCont f x \<Longrightarrow>
+    \<exists>M. (\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M) \<and> (\<forall>N. N < M \<longrightarrow> (\<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x))"
+  using isCont_eq_Ub[of a b f] by auto
 
 text{*Refine the above to existence of least upper bound*}
 
@@ -597,72 +632,6 @@
       (\<exists>t. isLub UNIV S t)"
 by (blast intro: reals_complete)
 
-lemma isCont_has_Ub: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
-         ==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b --> f(x) \<le> M) &
-                   (\<forall>N. N < M --> (\<exists>x. a \<le> x & x \<le> b & N < f(x)))"
-apply (cut_tac S = "Collect (%y. \<exists>x. a \<le> x & x \<le> b & y = f x)"
-        in lemma_reals_complete)
-apply auto
-apply (drule isCont_bounded, assumption)
-apply (auto simp add: isUb_def leastP_def isLub_def setge_def setle_def)
-apply (rule exI, auto)
-apply (auto dest!: spec simp add: linorder_not_less)
-done
-
-text{*Now show that it attains its upper bound*}
-
-lemma isCont_eq_Ub:
-  assumes le: "a \<le> b"
-      and con: "\<forall>x::real. a \<le> x & x \<le> b --> isCont f x"
-  shows "\<exists>M::real. (\<forall>x. a \<le> x & x \<le> b --> f(x) \<le> M) &
-             (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
-proof -
-  from isCont_has_Ub [OF le con]
-  obtain M where M1: "\<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M"
-             and M2: "!!N. N<M ==> \<exists>x. a \<le> x \<and> x \<le> b \<and> N < f x"  by blast
-  show ?thesis
-  proof (intro exI, intro conjI)
-    show " \<forall>x. a \<le> x \<and> x \<le> b \<longrightarrow> f x \<le> M" by (rule M1)
-    show "\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M"
-    proof (rule ccontr)
-      assume "\<not> (\<exists>x. a \<le> x \<and> x \<le> b \<and> f x = M)"
-      with M1 have M3: "\<forall>x. a \<le> x & x \<le> b --> f x < M"
-        by (fastforce simp add: linorder_not_le [symmetric])
-      hence "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. inverse (M - f x)) x"
-        by (auto simp add: con)
-      from isCont_bounded [OF le this]
-      obtain k where k: "!!x. a \<le> x & x \<le> b --> inverse (M - f x) \<le> k" by auto
-      have Minv: "!!x. a \<le> x & x \<le> b --> 0 < inverse (M - f (x))"
-        by (simp add: M3 algebra_simps)
-      have "!!x. a \<le> x & x \<le> b --> inverse (M - f x) < k+1" using k
-        by (auto intro: order_le_less_trans [of _ k])
-      with Minv
-      have "!!x. a \<le> x & x \<le> b --> inverse(k+1) < inverse(inverse(M - f x))"
-        by (intro strip less_imp_inverse_less, simp_all)
-      hence invlt: "!!x. a \<le> x & x \<le> b --> inverse(k+1) < M - f x"
-        by simp
-      have "M - inverse (k+1) < M" using k [of a] Minv [of a] le
-        by (simp, arith)
-      from M2 [OF this]
-      obtain x where ax: "a \<le> x & x \<le> b & M - inverse(k+1) < f x" ..
-      thus False using invlt [of x] by force
-    qed
-  qed
-qed
-
-
-text{*Same theorem for lower bound*}
-
-lemma isCont_eq_Lb: "[| a \<le> b; \<forall>x. a \<le> x & x \<le> b --> isCont f x |]
-         ==> \<exists>M::real. (\<forall>x::real. a \<le> x & x \<le> b --> M \<le> f(x)) &
-                   (\<exists>x. a \<le> x & x \<le> b & f(x) = M)"
-apply (subgoal_tac "\<forall>x. a \<le> x & x \<le> b --> isCont (%x. - (f x)) x")
-prefer 2 apply (blast intro: isCont_minus)
-apply (drule_tac f = "(%x. - (f x))" in isCont_eq_Ub)
-apply safe
-apply auto
-done
-
 
 text{*Another version.*}
 

--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -2362,28 +2362,6 @@
 
 subsection {* Compactness *}
 
-subsubsection{* Open-cover compactness *}
-
-definition compact :: "'a::topological_space set \<Rightarrow> bool" where
-  compact_eq_heine_borel: -- "This name is used for backwards compatibility"
-    "compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
-
-lemma compactI:
-  assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union> C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union> C'"
-  shows "compact s"
-  unfolding compact_eq_heine_borel using assms by metis
-
-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_image:
-  assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
-  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
-  using assms unfolding ball_simps[symmetric] SUP_def
-  by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
-
 subsubsection {* Bolzano-Weierstrass property *}
 
 lemma heine_borel_imp_bolzano_weierstrass:
@@ -2621,11 +2599,6 @@
 
 text{* In particular, some common special cases. *}
 
-lemma compact_empty[simp]:
- "compact {}"
-  unfolding compact_eq_heine_borel
-  by auto
-
 lemma compact_union [intro]:
   assumes "compact s" "compact t" shows " compact (s \<union> t)"
 proof (rule compactI)
@@ -4523,40 +4496,6 @@
   qed
 qed
 
-lemma compact_continuous_image:
-  assumes "continuous_on s f" and "compact s"
-  shows "compact (f ` s)"
-using assms (* FIXME: long unstructured proof *)
-unfolding continuous_on_open
-unfolding compact_eq_openin_cover
-apply clarify
-apply (drule_tac x="image (\<lambda>t. {x \<in> s. f x \<in> t}) C" in spec)
-apply (drule mp)
-apply (rule conjI)
-apply simp
-apply clarsimp
-apply (drule subsetD)
-apply (erule imageI)
-apply fast
-apply (erule thin_rl)
-apply clarify
-apply (rule_tac x="image (inv_into C (\<lambda>t. {x \<in> s. f x \<in> t})) D" in exI)
-apply (intro conjI)
-apply clarify
-apply (rule inv_into_into)
-apply (erule (1) subsetD)
-apply (erule finite_imageI)
-apply (clarsimp, rename_tac x)
-apply (drule (1) subsetD, clarify)
-apply (drule (1) subsetD, clarify)
-apply (rule rev_bexI)
-apply assumption
-apply (subgoal_tac "{x \<in> s. f x \<in> t} \<in> (\<lambda>t. {x \<in> s. f x \<in> t}) ` C")
-apply (drule f_inv_into_f)
-apply fast
-apply (erule imageI)
-done
-
 lemma connected_continuous_image:
   assumes "continuous_on s f"  "connected s"
   shows "connected(f ` s)"
@@ -4710,56 +4649,6 @@
   shows "continuous_on s f \<longleftrightarrow> (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d --> abs(f x' - f x) < e))"
   unfolding continuous_on_iff dist_norm by simp
 
-lemma compact_attains_sup:
-  fixes S :: "'a::linorder_topology set"
-  assumes "compact S" "S \<noteq> {}"
-  shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
-proof (rule classical)
-  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)"
-  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s"
-    by (metis not_le)
-  then have "\<forall>s\<in>S. open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
-    by auto
-  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})"
-    by (erule compactE_image)
-  with `S \<noteq> {}` have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)"
-    by (auto intro!: Max_in)
-  with C have "S \<subseteq> {..< Max (t`C)}"
-    by (auto intro: less_le_trans simp: subset_eq)
-  with t Max `C \<subseteq> S` show ?thesis
-    by fastforce
-qed
-
-lemma compact_attains_inf:
-  fixes S :: "'a::linorder_topology set"
-  assumes "compact S" "S \<noteq> {}"
-  shows "\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t"
-proof (rule classical)
-  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t)"
-  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. t s < s"
-    by (metis not_le)
-  then have "\<forall>s\<in>S. open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
-    by auto
-  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {t s <..})"
-    by (erule compactE_image)
-  with `S \<noteq> {}` have Min: "Min (t`C) \<in> t`C" and "\<forall>s\<in>t`C. Min (t`C) \<le> s"
-    by (auto intro!: Min_in)
-  with C have "S \<subseteq> {Min (t`C) <..}"
-    by (auto intro: le_less_trans simp: subset_eq)
-  with t Min `C \<subseteq> S` show ?thesis
-    by fastforce
-qed
-
-lemma continuous_attains_sup:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
-  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s.  f y \<le> f x)"
-  using compact_attains_sup[of "f ` s"] compact_continuous_image[of s f] by auto
-
-lemma continuous_attains_inf:
-  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
-  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f x \<le> f y)"
-  using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
-
 text {* Hence some handy theorems on distance, diameter etc. of/from a set. *}
 
 lemma distance_attains_sup:

--- a/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
+++ b/src/HOL/Topological_Spaces.thy	Fri Mar 22 10:41:43 2013 +0100
@@ -1780,5 +1780,98 @@
   "isCont g (f x) \<Longrightarrow> continuous (at x within s) f \<Longrightarrow> continuous (at x within s) (\<lambda>x. g (f x))"
   using continuous_within_compose2[of x s f g] by (simp add: continuous_at_within)
 
+subsubsection{* Open-cover compactness *}
+
+context topological_space
+begin
+
+definition compact :: "'a set \<Rightarrow> bool" where
+  compact_eq_heine_borel: -- "This name is used for backwards compatibility"
+    "compact S \<longleftrightarrow> (\<forall>C. (\<forall>c\<in>C. open c) \<and> S \<subseteq> \<Union>C \<longrightarrow> (\<exists>D\<subseteq>C. finite D \<and> S \<subseteq> \<Union>D))"
+
+lemma compactI:
+  assumes "\<And>C. \<forall>t\<in>C. open t \<Longrightarrow> s \<subseteq> \<Union> C \<Longrightarrow> \<exists>C'. C' \<subseteq> C \<and> finite C' \<and> s \<subseteq> \<Union> C'"
+  shows "compact s"
+  unfolding compact_eq_heine_borel using assms by metis
+
+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_image:
+  assumes "compact s" and "\<forall>t\<in>C. open (f t)" and "s \<subseteq> (\<Union>c\<in>C. f c)"
+  obtains C' where "C' \<subseteq> C" and "finite C'" and "s \<subseteq> (\<Union>c\<in>C'. f c)"
+  using assms unfolding ball_simps[symmetric] SUP_def
+  by (metis (lifting) finite_subset_image compact_eq_heine_borel[of s])
+
 end
 
+lemma (in linorder_topology) compact_attains_sup:
+  assumes "compact S" "S \<noteq> {}"
+  shows "\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s"
+proof (rule classical)
+  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. t \<le> s)"
+  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. s < t s"
+    by (metis not_le)
+  then have "\<forall>s\<in>S. open {..< t s}" "S \<subseteq> (\<Union>s\<in>S. {..< t s})"
+    by auto
+  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {..< t s})"
+    by (erule compactE_image)
+  with `S \<noteq> {}` have Max: "Max (t`C) \<in> t`C" and "\<forall>s\<in>t`C. s \<le> Max (t`C)"
+    by (auto intro!: Max_in)
+  with C have "S \<subseteq> {..< Max (t`C)}"
+    by (auto intro: less_le_trans simp: subset_eq)
+  with t Max `C \<subseteq> S` show ?thesis
+    by fastforce
+qed
+
+lemma (in linorder_topology) compact_attains_inf:
+  assumes "compact S" "S \<noteq> {}"
+  shows "\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t"
+proof (rule classical)
+  assume "\<not> (\<exists>s\<in>S. \<forall>t\<in>S. s \<le> t)"
+  then obtain t where t: "\<forall>s\<in>S. t s \<in> S" and "\<forall>s\<in>S. t s < s"
+    by (metis not_le)
+  then have "\<forall>s\<in>S. open {t s <..}" "S \<subseteq> (\<Union>s\<in>S. {t s <..})"
+    by auto
+  with `compact S` obtain C where "C \<subseteq> S" "finite C" and C: "S \<subseteq> (\<Union>s\<in>C. {t s <..})"
+    by (erule compactE_image)
+  with `S \<noteq> {}` have Min: "Min (t`C) \<in> t`C" and "\<forall>s\<in>t`C. Min (t`C) \<le> s"
+    by (auto intro!: Min_in)
+  with C have "S \<subseteq> {Min (t`C) <..}"
+    by (auto intro: le_less_trans simp: subset_eq)
+  with t Min `C \<subseteq> S` show ?thesis
+    by fastforce
+qed
+
+lemma compact_continuous_image:
+  assumes f: "continuous_on s f" and s: "compact s"
+  shows "compact (f ` s)"
+proof (rule compactI)
+  fix C assume "\<forall>c\<in>C. open c" and cover: "f`s \<subseteq> \<Union>C"
+  with f have "\<forall>c\<in>C. \<exists>A. open A \<and> A \<inter> s = f -` c \<inter> s"
+    unfolding continuous_on_open_invariant by blast
+  then guess A unfolding bchoice_iff .. note A = this
+  with cover have "\<forall>c\<in>C. open (A c)" "s \<subseteq> (\<Union>c\<in>C. A c)"
+    by (fastforce simp add: subset_eq set_eq_iff)+
+  from compactE_image[OF s this] obtain D where "D \<subseteq> C" "finite D" "s \<subseteq> (\<Union>c\<in>D. A c)" .
+  with A show "\<exists>D \<subseteq> C. finite D \<and> f`s \<subseteq> \<Union>D"
+    by (intro exI[of _ D]) (fastforce simp add: subset_eq set_eq_iff)+
+qed
+
+lemma continuous_attains_sup:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
+  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s.  f y \<le> f x)"
+  using compact_attains_sup[of "f ` s"] compact_continuous_image[of s f] by auto
+
+lemma continuous_attains_inf:
+  fixes f :: "'a::topological_space \<Rightarrow> 'b::linorder_topology"
+  shows "compact s \<Longrightarrow> s \<noteq> {} \<Longrightarrow> continuous_on s f \<Longrightarrow> (\<exists>x\<in>s. \<forall>y\<in>s. f x \<le> f y)"
+  using compact_attains_inf[of "f ` s"] compact_continuous_image[of s f] by auto
+
+end
+