# HG changeset patch
# User huffman
# Date 1259019032 28800
# Node ID 87cbdecaa87958281c6f2a0b79a9c03449b509a7
# Parent  22758f95e624e44117b85b4de0f27bb0fa2bd017
replace 'UNIV - S' with '- S'

diff -r 22758f95e624 -r 87cbdecaa879 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Nov 24 10:14:59 2009 -0800
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Nov 23 15:30:32 2009 -0800
@@ -383,14 +383,15 @@
                  ~(e2 = {}))"
 unfolding connected_def openin_open by (safe, blast+)
 
-lemma exists_diff: "(\<exists>S. P(UNIV - S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
+lemma exists_diff:
+  fixes P :: "'a set \<Rightarrow> bool"
+  shows "(\<exists>S. P(- S)) \<longleftrightarrow> (\<exists>S. P S)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
-
   {assume "?lhs" hence ?rhs by blast }
   moreover
   {fix S assume H: "P S"
-    have "S = UNIV - (UNIV - S)" by auto
-    with H have "P (UNIV - (UNIV - S))" by metis }
+    have "S = - (- S)" by auto
+    with H have "P (- (- S))" by metis }
   ultimately show ?thesis by metis
 qed
 
@@ -398,11 +399,11 @@
         (\<forall>T. openin (subtopology euclidean S) T \<and>
             closedin (subtopology euclidean S) T \<longrightarrow> T = {} \<or> T = S)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof-
-  have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (UNIV - e2) \<and> S \<subseteq> e1 \<union> (UNIV - e2) \<and> e1 \<inter> (UNIV - e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV - e2) \<inter> S \<noteq> {})"
+  have " \<not> connected S \<longleftrightarrow> (\<exists>e1 e2. open e1 \<and> open (- e2) \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
     unfolding connected_def openin_open closedin_closed
     apply (subst exists_diff) by blast
-  hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (UNIV - e2) \<and> e1 \<inter> (UNIV - e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (UNIV - e2) \<inter> S \<noteq> {})"
-    (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def Compl_eq_Diff_UNIV) by metis
+  hence th0: "connected S \<longleftrightarrow> \<not> (\<exists>e2 e1. closed e2 \<and> open e1 \<and> S \<subseteq> e1 \<union> (- e2) \<and> e1 \<inter> (- e2) \<inter> S = {} \<and> e1 \<inter> S \<noteq> {} \<and> (- e2) \<inter> S \<noteq> {})"
+    (is " _ \<longleftrightarrow> \<not> (\<exists>e2 e1. ?P e2 e1)") apply (simp add: closed_def) by metis
 
   have th1: "?rhs \<longleftrightarrow> \<not> (\<exists>t' t. closed t'\<and>t = S\<inter>t' \<and> t\<noteq>{} \<and> t\<noteq>S \<and> (\<exists>t'. open t' \<and> t = S \<inter> t'))"
     (is "_ \<longleftrightarrow> \<not> (\<exists>t' t. ?Q t' t)")
@@ -558,8 +559,8 @@
 lemma closed_limpt: "closed S \<longleftrightarrow> (\<forall>x. x islimpt S \<longrightarrow> x \<in> S)"
   unfolding closed_def
   apply (subst open_subopen)
-  apply (simp add: islimpt_def subset_eq Compl_eq_Diff_UNIV)
-  by (metis DiffE DiffI UNIV_I insertCI insert_absorb mem_def)
+  apply (simp add: islimpt_def subset_eq)
+  by (metis ComplE ComplI insertCI insert_absorb mem_def)
 
 lemma islimpt_EMPTY[simp]: "\<not> x islimpt {}"
   unfolding islimpt_def by auto
@@ -719,12 +720,12 @@
 
 definition "closure S = S \<union> {x | x. x islimpt S}"
 
-lemma closure_interior: "closure S = UNIV - interior (UNIV - S)"
+lemma closure_interior: "closure S = - interior (- S)"
 proof-
   { fix x
-    have "x\<in>UNIV - interior (UNIV - S) \<longleftrightarrow> x \<in> closure S"  (is "?lhs = ?rhs")
+    have "x\<in>- interior (- S) \<longleftrightarrow> x \<in> closure S"  (is "?lhs = ?rhs")
     proof
-      let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> UNIV - S)"
+      let ?exT = "\<lambda> y. (\<exists>T. open T \<and> y \<in> T \<and> T \<subseteq> - S)"
       assume "?lhs"
       hence *:"\<not> ?exT x"
         unfolding interior_def
@@ -746,10 +747,10 @@
     by blast
 qed
 
-lemma interior_closure: "interior S = UNIV - (closure (UNIV - S))"
+lemma interior_closure: "interior S = - (closure (- S))"
 proof-
   { fix x
-    have "x \<in> interior S \<longleftrightarrow> x \<in> UNIV - (closure (UNIV - S))"
+    have "x \<in> interior S \<longleftrightarrow> x \<in> - (closure (- S))"
       unfolding interior_def closure_def islimpt_def
       by auto
   }
@@ -759,7 +760,7 @@
 
 lemma closed_closure[simp, intro]: "closed (closure S)"
 proof-
-  have "closed (UNIV - interior (UNIV -S))" by blast
+  have "closed (- interior (-S))" by blast
   thus ?thesis using closure_interior[of S] by simp
 qed
 
@@ -844,8 +845,8 @@
 
 lemma open_inter_closure_eq_empty:
   "open S \<Longrightarrow> (S \<inter> closure T) = {} \<longleftrightarrow> S \<inter> T = {}"
-  using open_subset_interior[of S "UNIV - T"]
-  using interior_subset[of "UNIV - T"]
+  using open_subset_interior[of S "- T"]
+  using interior_subset[of "- T"]
   unfolding closure_interior
   by auto
 
@@ -873,16 +874,16 @@
     by blast
 qed
 
-lemma closure_complement: "closure(UNIV - S) = UNIV - interior(S)"
+lemma closure_complement: "closure(- S) = - interior(S)"
 proof-
-  have "S = UNIV - (UNIV - S)"
+  have "S = - (- S)"
     by auto
   thus ?thesis
     unfolding closure_interior
     by auto
 qed
 
-lemma interior_complement: "interior(UNIV - S) = UNIV - closure(S)"
+lemma interior_complement: "interior(- S) = - closure(S)"
   unfolding closure_interior
   by blast
 
@@ -893,7 +894,7 @@
 lemma frontier_closed: "closed(frontier S)"
   by (simp add: frontier_def closed_Diff)
 
-lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(UNIV - S))"
+lemma frontier_closures: "frontier S = (closure S) \<inter> (closure(- S))"
   by (auto simp add: frontier_def interior_closure)
 
 lemma frontier_straddle:
@@ -937,10 +938,10 @@
   { fix T assume "a \<in> T"  "open T" "a\<in>S"
     then obtain e where "e>0" and balle: "ball a e \<subseteq> T" unfolding open_contains_ball using `?rhs` by auto
     obtain x where "x \<notin> S" "dist a x < e" using `?rhs` using `e>0` by auto
-    hence "\<exists>y\<in>UNIV - S. y \<in> T \<and> y \<noteq> a" using balle `a\<in>S` unfolding ball_def by (rule_tac x=x in bexI)auto
+    hence "\<exists>y\<in>- S. y \<in> T \<and> y \<noteq> a" using balle `a\<in>S` unfolding ball_def by (rule_tac x=x in bexI)auto
   }
-  hence "a islimpt (UNIV - S) \<or> a\<notin>S" unfolding islimpt_def by auto
-  ultimately show ?lhs unfolding frontier_closures using closure_def[of "UNIV - S"] by auto
+  hence "a islimpt (- S) \<or> a\<notin>S" unfolding islimpt_def by auto
+  ultimately show ?lhs unfolding frontier_closures using closure_def[of "- S"] by auto
 qed
 
 lemma frontier_subset_closed: "closed S \<Longrightarrow> frontier S \<subseteq> S"
@@ -958,12 +959,12 @@
   thus ?thesis using frontier_subset_closed[of S] by auto
 qed
 
-lemma frontier_complement: "frontier(UNIV - S) = frontier S"
+lemma frontier_complement: "frontier(- S) = frontier S"
   by (auto simp add: frontier_def closure_complement interior_complement)
 
 lemma frontier_disjoint_eq: "frontier S \<inter> S = {} \<longleftrightarrow> open S"
-  using frontier_complement frontier_subset_eq[of "UNIV - S"]
-  unfolding open_closed Compl_eq_Diff_UNIV by auto
+  using frontier_complement frontier_subset_eq[of "- S"]
+  unfolding open_closed by auto
 
 subsection{* Common nets and The "within" modifier for nets. *}
 
@@ -2957,11 +2958,11 @@
   shows "s \<inter> (\<Inter> f) \<noteq> {}"
 proof
   assume as:"s \<inter> (\<Inter> f) = {}"
-  hence "s \<subseteq> \<Union>op - UNIV ` f" by auto
-  moreover have "Ball (op - UNIV ` f) open" using open_Diff closed_Diff using assms(2) by auto
-  ultimately obtain f' where f':"f' \<subseteq> op - UNIV ` f"  "finite f'"  "s \<subseteq> \<Union>f'" using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="(\<lambda>t. UNIV - t) ` f"]] by auto
-  hence "finite (op - UNIV ` f') \<and> op - UNIV ` f' \<subseteq> f" by(auto simp add: Diff_Diff_Int)
-  hence "s \<inter> \<Inter>op - UNIV ` f' \<noteq> {}" using assms(3)[THEN spec[where x="op - UNIV ` f'"]] by auto
+  hence "s \<subseteq> \<Union> uminus ` f" by auto
+  moreover have "Ball (uminus ` f) open" using open_Diff closed_Diff using assms(2) by auto
+  ultimately obtain f' where f':"f' \<subseteq> uminus ` f"  "finite f'"  "s \<subseteq> \<Union>f'" using assms(1)[unfolded compact_eq_heine_borel, THEN spec[where x="(\<lambda>t. - t) ` f"]] by auto
+  hence "finite (uminus ` f') \<and> uminus ` f' \<subseteq> f" by(auto simp add: Diff_Diff_Int)
+  hence "s \<inter> \<Inter>uminus ` f' \<noteq> {}" using assms(3)[THEN spec[where x="uminus ` f'"]] by auto
   thus False using f'(3) unfolding subset_eq and Union_iff by blast
 qed
 
@@ -4548,6 +4549,11 @@
   thus ?thesis using compact_closed_sums[OF compact_sing[of a] assms] by auto
 qed
 
+lemma translation_Compl:
+  fixes a :: "'a::ab_group_add"
+  shows "(\<lambda>x. a + x) ` (- t) = - ((\<lambda>x. a + x) ` t)"
+  apply (auto simp add: image_iff) apply(rule_tac x="x - a" in bexI) by auto
+
 lemma translation_UNIV:
   fixes a :: "'a::ab_group_add" shows "range (\<lambda>x. a + x) = UNIV"
   apply (auto simp add: image_iff) apply(rule_tac x="x - a" in exI) by auto
@@ -4561,10 +4567,10 @@
   fixes a :: "'a::real_normed_vector"
   shows "closure ((\<lambda>x. a + x) ` s) = (\<lambda>x. a + x) ` (closure s)"
 proof-
-  have *:"op + a ` (UNIV - s) = UNIV - op + a ` s"
+  have *:"op + a ` (- s) = - op + a ` s"
     apply auto unfolding image_iff apply(rule_tac x="x - a" in bexI) by auto
-  show ?thesis unfolding closure_interior translation_diff translation_UNIV
-    using interior_translation[of a "UNIV - s"] unfolding * by auto
+  show ?thesis unfolding closure_interior translation_Compl
+    using interior_translation[of a "- s"] unfolding * by auto
 qed
 
 lemma frontier_translation:
@@ -5163,14 +5169,14 @@
 
 lemma open_halfspace_lt: "open {x. inner a x < b}"
 proof-
-  have "UNIV - {x. b \<le> inner a x} = {x. inner a x < b}" by auto
-  thus ?thesis using closed_halfspace_ge[unfolded closed_def Compl_eq_Diff_UNIV, of b a] by auto
+  have "- {x. b \<le> inner a x} = {x. inner a x < b}" by auto
+  thus ?thesis using closed_halfspace_ge[unfolded closed_def, of b a] by auto
 qed
 
 lemma open_halfspace_gt: "open {x. inner a x > b}"
 proof-
-  have "UNIV - {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
-  thus ?thesis using closed_halfspace_le[unfolded closed_def Compl_eq_Diff_UNIV, of a b] by auto
+  have "- {x. b \<ge> inner a x} = {x. inner a x > b}" by auto
+  thus ?thesis using closed_halfspace_le[unfolded closed_def, of a b] by auto
 qed
 
 lemma open_halfspace_component_lt: