# HG changeset patch
# User huffman
# Date 1314289022 25200
# Node ID ea85d78a994eaf36abc0631309ea9b35e59e0869
# Parent  219a6fe4cfae6c16ef5919bbaf7af3ab2fea0f78
simplify definition of 'interior';
add lemmas interiorI and interiorE;
change lemmas interior_unique and closure_unique to rule_format;
tidy some proofs;

diff -r 219a6fe4cfae -r ea85d78a994e src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Wed Aug 24 16:08:21 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Convex_Euclidean_Space.thy	Thu Aug 25 09:17:02 2011 -0700
@@ -3453,22 +3453,27 @@
         ultimately show ?thesis using injpi by auto qed qed
   qed auto qed
 
-lemma homeomorphic_convex_compact_lemma: fixes s::"('a::euclidean_space) set"
-  assumes "convex s" "compact s" "cball 0 1 \<subseteq> s"
+lemma homeomorphic_convex_compact_lemma:
+  fixes s :: "('a::euclidean_space) set"
+  assumes "convex s" and "compact s" and "cball 0 1 \<subseteq> s"
   shows "s homeomorphic (cball (0::'a) 1)"
-  apply(rule starlike_compact_projective[OF assms(2-3)]) proof(rule,rule,rule,erule conjE)
-  fix x u assume as:"x \<in> s" "0 \<le> u" "u < (1::real)"
-  hence "u *\<^sub>R x \<in> interior s" unfolding interior_def mem_Collect_eq
-    apply(rule_tac x="ball (u *\<^sub>R x) (1 - u)" in exI) apply(rule, rule open_ball)
-    unfolding centre_in_ball apply rule defer apply(rule) unfolding mem_ball proof-
-    fix y assume "dist (u *\<^sub>R x) y < 1 - u"
-    hence "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s"
-      using assms(3) apply(erule_tac subsetD) unfolding mem_cball dist_commute dist_norm
-      unfolding group_add_class.diff_0 group_add_class.diff_0_right norm_minus_cancel norm_scaleR
-      apply (rule mult_left_le_imp_le[of "1 - u"])
-      unfolding mult_assoc[symmetric] using `u<1` by auto
-    thus "y \<in> s" using assms(1)[unfolded convex_def, rule_format, of "inverse(1 - u) *\<^sub>R (y - u *\<^sub>R x)" x "1 - u" u]
-      using as unfolding scaleR_scaleR by auto qed auto
+proof (rule starlike_compact_projective[OF assms(2-3)], clarify)
+  fix x u assume "x \<in> s" and "0 \<le> u" and "u < (1::real)"
+  have "open (ball (u *\<^sub>R x) (1 - u))" by (rule open_ball)
+  moreover have "u *\<^sub>R x \<in> ball (u *\<^sub>R x) (1 - u)"
+    unfolding centre_in_ball using `u < 1` by simp
+  moreover have "ball (u *\<^sub>R x) (1 - u) \<subseteq> s"
+  proof
+    fix y assume "y \<in> ball (u *\<^sub>R x) (1 - u)"
+    hence "dist (u *\<^sub>R x) y < 1 - u" unfolding mem_ball .
+    with `u < 1` have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> cball 0 1"
+      by (simp add: dist_norm inverse_eq_divide norm_minus_commute)
+    with assms(3) have "inverse (1 - u) *\<^sub>R (y - u *\<^sub>R x) \<in> s" ..
+    with assms(1) have "(1 - u) *\<^sub>R ((y - u *\<^sub>R x) /\<^sub>R (1 - u)) + u *\<^sub>R x \<in> s"
+      using `x \<in> s` `0 \<le> u` `u < 1` [THEN less_imp_le] by (rule mem_convex)
+    thus "y \<in> s" using `u < 1` by simp
+  qed
+  ultimately have "u *\<^sub>R x \<in> interior s" ..
   thus "u *\<^sub>R x \<in> s - frontier s" using frontier_def and interior_subset by auto qed
 
 lemma homeomorphic_convex_compact_cball: fixes e::real and s::"('a::euclidean_space) set"
diff -r 219a6fe4cfae -r ea85d78a994e src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 24 16:08:21 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 25 09:17:02 2011 -0700
@@ -555,37 +555,58 @@
 
 subsection {* Interior of a Set *}
 
-definition "interior S = {x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> S}"
+definition "interior S = \<Union>{T. open T \<and> T \<subseteq> S}"
+
+lemma interiorI [intro?]:
+  assumes "open T" and "x \<in> T" and "T \<subseteq> S"
+  shows "x \<in> interior S"
+  using assms unfolding interior_def by fast
+
+lemma interiorE [elim?]:
+  assumes "x \<in> interior S"
+  obtains T where "open T" and "x \<in> T" and "T \<subseteq> S"
+  using assms unfolding interior_def by fast
+
+lemma open_interior [simp, intro]: "open (interior S)"
+  by (simp add: interior_def open_Union)
+
+lemma interior_subset: "interior S \<subseteq> S"
+  by (auto simp add: interior_def)
+
+lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T \<Longrightarrow> T \<subseteq> interior S"
+  by (auto simp add: interior_def)
+
+lemma interior_open: "open S \<Longrightarrow> interior S = S"
+  by (intro equalityI interior_subset interior_maximal subset_refl)
 
 lemma interior_eq: "interior S = S \<longleftrightarrow> open S"
-  apply (simp add: set_eq_iff interior_def)
-  apply (subst (2) open_subopen) by (safe, blast+)
-
-lemma interior_open: "open S ==> (interior S = S)" by (metis interior_eq)
-
-lemma interior_empty[simp]: "interior {} = {}" by (simp add: interior_def)
-
-lemma open_interior[simp, intro]: "open(interior S)"
-  apply (simp add: interior_def)
-  apply (subst open_subopen) by blast
-
-lemma interior_interior[simp]: "interior(interior S) = interior S" by (metis interior_eq open_interior)
-lemma interior_subset: "interior S \<subseteq> S" by (auto simp add: interior_def)
-lemma subset_interior: "S \<subseteq> T ==> (interior S) \<subseteq> (interior T)" by (auto simp add: interior_def)
-lemma interior_maximal: "T \<subseteq> S \<Longrightarrow> open T ==> T \<subseteq> (interior S)" by (auto simp add: interior_def)
-lemma interior_unique: "T \<subseteq> S \<Longrightarrow> open T  \<Longrightarrow> (\<forall>T'. T' \<subseteq> S \<and> open T' \<longrightarrow> T' \<subseteq> T) \<Longrightarrow> interior S = T"
-  by (metis equalityI interior_maximal interior_subset open_interior)
-lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e. 0 < e \<and> ball x e \<subseteq> S)"
-  apply (simp add: interior_def)
-  by (metis open_contains_ball centre_in_ball open_ball subset_trans)
-
-lemma open_subset_interior: "open S ==> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
+  by (metis open_interior interior_open)
+
+lemma open_subset_interior: "open S \<Longrightarrow> S \<subseteq> interior T \<longleftrightarrow> S \<subseteq> T"
   by (metis interior_maximal interior_subset subset_trans)
 
-lemma interior_inter[simp]: "interior(S \<inter> T) = interior S \<inter> interior T"
-  apply (rule equalityI, simp)
-  apply (metis Int_lower1 Int_lower2 subset_interior)
-  by (metis Int_mono interior_subset open_Int open_interior open_subset_interior)
+lemma interior_empty [simp]: "interior {} = {}"
+  using open_empty by (rule interior_open)
+
+lemma interior_interior [simp]: "interior (interior S) = interior S"
+  using open_interior by (rule interior_open)
+
+lemma subset_interior: "S \<subseteq> T \<Longrightarrow> interior S \<subseteq> interior T"
+  by (auto simp add: interior_def) (* TODO: rename to interior_mono *)
+
+lemma interior_unique:
+  assumes "T \<subseteq> S" and "open T"
+  assumes "\<And>T'. T' \<subseteq> S \<Longrightarrow> open T' \<Longrightarrow> T' \<subseteq> T"
+  shows "interior S = T"
+  by (intro equalityI assms interior_subset open_interior interior_maximal)
+
+lemma interior_inter [simp]: "interior (S \<inter> T) = interior S \<inter> interior T"
+  by (intro equalityI Int_mono Int_greatest subset_interior Int_lower1
+    Int_lower2 interior_maximal interior_subset open_Int open_interior)
+
+lemma mem_interior: "x \<in> interior S \<longleftrightarrow> (\<exists>e>0. ball x e \<subseteq> S)"
+  using open_contains_ball_eq [where S="interior S"]
+  by (simp add: open_subset_interior)
 
 lemma interior_limit_point [intro]:
   fixes x :: "'a::perfect_space"
@@ -599,21 +620,20 @@
 
 lemma interior_closed_Un_empty_interior:
   assumes cS: "closed S" and iT: "interior T = {}"
-  shows "interior(S \<union> T) = interior S"
+  shows "interior (S \<union> T) = interior S"
 proof
-  show "interior S \<subseteq> interior (S\<union>T)"
-    by (rule subset_interior, blast)
+  show "interior S \<subseteq> interior (S \<union> T)"
+    by (rule subset_interior, rule Un_upper1)
 next
   show "interior (S \<union> T) \<subseteq> interior S"
   proof
     fix x assume "x \<in> interior (S \<union> T)"
-    then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T"
-      unfolding interior_def by fast
+    then obtain R where "open R" "x \<in> R" "R \<subseteq> S \<union> T" ..
     show "x \<in> interior S"
     proof (rule ccontr)
       assume "x \<notin> interior S"
       with `x \<in> R` `open R` obtain y where "y \<in> R - S"
-        unfolding interior_def set_eq_iff by fast
+        unfolding interior_def by fast
       from `open R` `closed S` have "open (R - S)" by (rule open_Diff)
       from `R \<subseteq> S \<union> T` have "R - S \<subseteq> T" by fast
       from `y \<in> R - S` `open (R - S)` `R - S \<subseteq> T` `interior T = {}`
@@ -628,15 +648,16 @@
     by (intro Sigma_mono interior_subset)
   show "open (interior A \<times> interior B)"
     by (intro open_Times open_interior)
-  show "\<forall>T. T \<subseteq> A \<times> B \<and> open T \<longrightarrow> T \<subseteq> interior A \<times> interior B"
-    apply (simp add: open_prod_def, clarify)
-    apply (drule (1) bspec, clarify, rename_tac C D)
-    apply (simp add: interior_def, rule conjI)
-    apply (rule_tac x=C in exI, clarsimp)
-    apply (rule SigmaD1, erule subsetD, erule subsetD, erule (1) SigmaI)
-    apply (rule_tac x=D in exI, clarsimp)
-    apply (rule SigmaD2, erule subsetD, erule subsetD, erule (1) SigmaI)
-    done
+  fix T assume "T \<subseteq> A \<times> B" and "open T" thus "T \<subseteq> interior A \<times> interior B"
+  proof (safe)
+    fix x y assume "(x, y) \<in> T"
+    then obtain C D where "open C" "open D" "C \<times> D \<subseteq> T" "x \<in> C" "y \<in> D"
+      using `open T` unfolding open_prod_def by fast
+    hence "open C" "open D" "C \<subseteq> A" "D \<subseteq> B" "x \<in> C" "y \<in> D"
+      using `T \<subseteq> A \<times> B` by auto
+    thus "x \<in> interior A" and "y \<in> interior B"
+      by (auto intro: interiorI)
+  qed
 qed
 
 
@@ -657,57 +678,33 @@
   unfolding closure_def by simp
 
 lemma closure_hull: "closure S = closed hull S"
-proof-
-  have "S \<subseteq> closure S"
-    by (rule closure_subset)
-  moreover
-  have "closed (closure S)"
-    by (rule closed_closure)
-  moreover
-  { fix t
-    assume *:"S \<subseteq> t" "closed t"
-    { fix x
-      assume "x islimpt S"
-      hence "x islimpt t" using *(1)
-        using islimpt_subset[of x, of S, of t]
-        by blast
-    }
-    with * have "closure S \<subseteq> t"
-      unfolding closure_def
-      using closed_limpt[of t]
-      by auto
-  }
-  ultimately show ?thesis
-    by (rule hull_unique [symmetric])
-qed
+  unfolding hull_def closure_interior interior_def by auto
 
 lemma closure_eq: "closure S = S \<longleftrightarrow> closed S"
-  unfolding closure_hull
-  using hull_eq[of closed, OF  closed_Inter, of S]
-  by metis
-
-lemma closure_closed[simp]: "closed S \<Longrightarrow> closure S = S"
-  using closure_eq[of S]
-  by simp
-
-lemma closure_closure[simp]: "closure (closure S) = closure S"
+  unfolding closure_hull using closed_Inter by (rule hull_eq)
+
+lemma closure_closed [simp]: "closed S \<Longrightarrow> closure S = S"
+  unfolding closure_eq .
+
+lemma closure_closure [simp]: "closure (closure S) = closure S"
   unfolding closure_hull by (rule hull_hull)
 
 lemma subset_closure: "S \<subseteq> T \<Longrightarrow> closure S \<subseteq> closure T"
   unfolding closure_hull by (rule hull_mono)
 
-lemma closure_minimal: "S \<subseteq> T \<Longrightarrow>  closed T \<Longrightarrow> closure S \<subseteq> T"
+lemma closure_minimal: "S \<subseteq> T \<Longrightarrow> closed T \<Longrightarrow> closure S \<subseteq> T"
   unfolding closure_hull by (rule hull_minimal)
 
-lemma closure_unique: "S \<subseteq> T \<and> closed T \<and> (\<forall> T'. S \<subseteq> T' \<and> closed T' \<longrightarrow> T \<subseteq> T') \<Longrightarrow> closure S = T"
-  using hull_unique[of S T closed]
-  unfolding closure_hull
-  by simp
-
-lemma closure_empty[simp]: "closure {} = {}"
+lemma closure_unique:
+  assumes "S \<subseteq> T" and "closed T"
+  assumes "\<And>T'. S \<subseteq> T' \<Longrightarrow> closed T' \<Longrightarrow> T \<subseteq> T'"
+  shows "closure S = T"
+  using assms unfolding closure_hull by (rule hull_unique)
+
+lemma closure_empty [simp]: "closure {} = {}"
   using closed_empty by (rule closure_closed)
 
-lemma closure_univ[simp]: "closure UNIV = UNIV"
+lemma closure_univ [simp]: "closure UNIV = UNIV"
   using closed_UNIV by (rule closure_closed)
 
 lemma closure_union [simp]: "closure (S \<union> T) = closure S \<union> closure T"
@@ -752,19 +749,19 @@
     by blast
 qed
 
-lemma closure_complement: "closure(- S) = - interior(S)"
+lemma closure_complement: "closure (- S) = - interior S"
   unfolding closure_interior by simp
 
-lemma interior_complement: "interior(- S) = - closure(S)"
+lemma interior_complement: "interior (- S) = - closure S"
   unfolding closure_interior by simp
 
 lemma closure_Times: "closure (A \<times> B) = closure A \<times> closure B"
-proof (intro closure_unique conjI)
+proof (rule closure_unique)
   show "A \<times> B \<subseteq> closure A \<times> closure B"
     by (intro Sigma_mono closure_subset)
   show "closed (closure A \<times> closure B)"
     by (intro closed_Times closed_closure)
-  show "\<forall>T. A \<times> B \<subseteq> T \<and> closed T \<longrightarrow> closure A \<times> closure B \<subseteq> T"
+  fix T assume "A \<times> B \<subseteq> T" and "closed T" thus "closure A \<times> closure B \<subseteq> T"
     apply (simp add: closed_def open_prod_def, clarify)
     apply (rule ccontr)
     apply (drule_tac x="(a, b)" in bspec, simp, clarify, rename_tac C D)
@@ -1038,8 +1035,7 @@
   assumes "x \<in> interior S"
   shows "eventually P (at x within S) \<longleftrightarrow> eventually P (at x)" (is "?lhs = ?rhs")
 proof-
-  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S"
-    unfolding interior_def by fast
+  from assms obtain T where T: "open T" "x \<in> T" "T \<subseteq> S" ..
   { assume "?lhs"
     then obtain A where "open A" "x \<in> A" "\<forall>y\<in>A. y \<noteq> x \<longrightarrow> y \<in> S \<longrightarrow> P y"
       unfolding Limits.eventually_within Limits.eventually_at_topological
@@ -2731,8 +2727,8 @@
   fixes x :: "'a::t1_space"
   shows "closure (insert x s) = insert x (closure s)"
 apply (rule closure_unique)
-apply (rule conjI [OF insert_mono [OF closure_subset]])
-apply (rule conjI [OF closed_insert [OF closed_closure]])
+apply (rule insert_mono [OF closure_subset])
+apply (rule closed_insert [OF closed_closure])
 apply (simp add: closure_minimal)
 done
 
@@ -3299,10 +3295,9 @@
   unfolding continuous_on by (metis subset_eq Lim_within_subset)
 
 lemma continuous_on_interior:
-  shows "continuous_on s f \<Longrightarrow> x \<in> interior s ==> continuous (at x) f"
-unfolding interior_def
-apply simp
-by (meson continuous_on_eq_continuous_at continuous_on_subset)
+  shows "continuous_on s f \<Longrightarrow> x \<in> interior s \<Longrightarrow> continuous (at x) f"
+  by (erule interiorE, drule (1) continuous_on_subset,
+    simp add: continuous_on_eq_continuous_at)
 
 lemma continuous_on_eq:
   "(\<forall>x \<in> s. f x = g x) \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on s g"
@@ -3744,13 +3739,20 @@
 lemma interior_image_subset:
   assumes "\<forall>x. continuous (at x) f" "inj f"
   shows "interior (f ` s) \<subseteq> f ` (interior s)"
-  apply rule unfolding interior_def mem_Collect_eq image_iff apply safe
-proof- fix x T assume as:"open T" "x \<in> T" "T \<subseteq> f ` s" 
-  hence "x \<in> f ` s" by auto then guess y unfolding image_iff .. note y=this
-  thus "\<exists>xa\<in>{x. \<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> s}. x = f xa" apply(rule_tac x=y in bexI) using assms as
-    apply safe apply(rule_tac x="{x. f x \<in> T}" in exI) apply(safe,rule continuous_open_preimage_univ)
-  proof- fix x assume "f x \<in> T" hence "f x \<in> f ` s" using as by auto
-    thus "x \<in> s" unfolding inj_image_mem_iff[OF assms(2)] . qed auto qed
+proof
+  fix x assume "x \<in> interior (f ` s)"
+  then obtain T where as: "open T" "x \<in> T" "T \<subseteq> f ` s" ..
+  hence "x \<in> f ` s" by auto
+  then obtain y where y: "y \<in> s" "x = f y" by auto
+  have "open (vimage f T)"
+    using assms(1) `open T` by (rule continuous_open_vimage)
+  moreover have "y \<in> vimage f T"
+    using `x = f y` `x \<in> T` by simp
+  moreover have "vimage f T \<subseteq> s"
+    using `T \<subseteq> image f s` `inj f` unfolding inj_on_def subset_eq by auto
+  ultimately have "y \<in> interior s" ..
+  with `x = f y` show "x \<in> f ` interior s" ..
+qed
 
 text {* Equality of continuous functions on closure and related results. *}
 
@@ -4818,13 +4820,15 @@
   finally show "closed {a .. b}" .
 qed
 
-lemma interior_closed_interval[intro]: fixes a :: "'a::ordered_euclidean_space" shows
- "interior {a .. b} = {a<..<b}" (is "?L = ?R")
+lemma interior_closed_interval [intro]:
+  fixes a b :: "'a::ordered_euclidean_space"
+  shows "interior {a..b} = {a<..<b}" (is "?L = ?R")
 proof(rule subset_antisym)
-  show "?R \<subseteq> ?L" using interior_maximal[OF interval_open_subset_closed open_interval] by auto
+  show "?R \<subseteq> ?L" using interval_open_subset_closed open_interval
+    by (rule interior_maximal)
 next
-  { fix x assume "\<exists>T. open T \<and> x \<in> T \<and> T \<subseteq> {a..b}"
-    then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" by auto
+  { fix x assume "x \<in> interior {a..b}"
+    then obtain s where s:"open s" "x \<in> s" "s \<subseteq> {a..b}" ..
     then obtain e where "e>0" and e:"\<forall>x'. dist x' x < e \<longrightarrow> x' \<in> {a..b}" unfolding open_dist and subset_eq by auto
     { fix i assume i:"i<DIM('a)"
       have "dist (x - (e / 2) *\<^sub>R basis i) x < e"
@@ -4839,7 +4843,7 @@
       hence "a $$ i < x $$ i" and "x $$ i < b $$ i" unfolding euclidean_simps
         unfolding basis_component using `e>0` i by auto  }
     hence "x \<in> {a<..<b}" unfolding mem_interval by auto  }
-  thus "?L \<subseteq> ?R" unfolding interior_def and subset_eq by auto
+  thus "?L \<subseteq> ?R" ..
 qed
 
 lemma bounded_closed_interval: fixes a :: "'a::ordered_euclidean_space" shows "bounded {a .. b}"