# HG changeset patch
# User huffman
# Date 1379980577 25200
# Node ID 0a62ad289c4d7ea8b58095090c32b9639db4f202
# Parent  369537953d05250c5d1b1906baed0cab0d220501
tuned proofs

diff -r 369537953d05 -r 0a62ad289c4d src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 00:21:40 2013 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 23 16:56:17 2013 -0700
@@ -5776,59 +5776,16 @@
   fixes s :: "'a::real_normed_vector set"
   assumes "closed s"
   shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
-proof (cases "s = {}")
-  case True
-  then show ?thesis by auto
+proof (cases "c = 0")
+  case True then show ?thesis
+    by (auto simp add: image_constant_conv)
 next
   case False
-  show ?thesis
-  proof (cases "c = 0")
-    have *: "(\<lambda>x. 0) ` s = {0}" using `s\<noteq>{}` by auto
-    case True
-    then show ?thesis
-      apply auto
-      unfolding *
-      apply auto
-      done
-  next
-    case False
-    {
-      fix x l
-      assume as: "\<forall>n::nat. x n \<in> scaleR c ` s"  "(x ---> l) sequentially"
-      {
-        fix n :: nat
-        have "scaleR (1 / c) (x n) \<in> s"
-          using as(1)[THEN spec[where x=n]]
-          using `c\<noteq>0`
-          by auto
-      }
-      moreover
-      {
-        fix e :: real
-        assume "e > 0"
-        then have "0 < e *\<bar>c\<bar>"
-          using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto
-        then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>"
-          using as(2)[unfolded LIMSEQ_def, THEN spec[where x="e * abs c"]] by auto
-        then have "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e"
-          unfolding dist_norm
-          unfolding scaleR_right_diff_distrib[symmetric]
-          using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto
-      }
-      then have "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially"
-        unfolding LIMSEQ_def by auto
-      ultimately have "l \<in> scaleR c ` s"
-        using assms[unfolded closed_sequential_limits,
-          THEN spec[where x="\<lambda>n. scaleR (1/c) (x n)"],
-          THEN spec[where x="scaleR (1/c) l"]]
-        unfolding image_iff using `c\<noteq>0`
-          apply (rule_tac x="scaleR (1 / c) l" in bexI)
-          apply auto
-          done
-    }
-    then show ?thesis
-      unfolding closed_sequential_limits by fast
-  qed
+  from assms have "closed ((\<lambda>x. inverse c *\<^sub>R x) -` s)"
+    by (simp add: continuous_closed_vimage)
+  also have "(\<lambda>x. inverse c *\<^sub>R x) -` s = (\<lambda>x. c *\<^sub>R x) ` s"
+    using `c \<noteq> 0` by (auto elim: image_eqI [rotated])
+  finally show ?thesis .
 qed
 
 lemma closed_negations:
@@ -6576,58 +6533,6 @@
   unfolding closure_open_interval[OF assms, symmetric]
   unfolding open_inter_closure_eq_empty[OF open_interval] ..
 
-
-(* Some stuff for half-infinite intervals too; FIXME: notation?  *)
-
-lemma closed_interval_left:
-  fixes b :: "'a::euclidean_space"
-  shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
-proof -
-  {
-    fix i :: 'a
-    assume i: "i \<in> Basis"
-    fix x :: "'a"
-    assume x: "\<forall>e>0. \<exists>x'\<in>{x. \<forall>i\<in>Basis. x \<bullet> i \<le> b \<bullet> i}. x' \<noteq> x \<and> dist x' x < e"
-    {
-      assume "x\<bullet>i > b\<bullet>i"
-      then obtain y where "y \<bullet> i \<le> b \<bullet> i"  "y \<noteq> x"  "dist y x < x\<bullet>i - b\<bullet>i"
-        using x[THEN spec[where x="x\<bullet>i - b\<bullet>i"]] using i by auto
-      then have False
-        using Basis_le_norm[OF i, of "y - x"]
-        unfolding dist_norm inner_simps
-        using i
-        by auto
-    }
-    then have "x\<bullet>i \<le> b\<bullet>i" by (rule ccontr)auto
-  }
-  then show ?thesis
-    unfolding closed_limpt unfolding islimpt_approachable by blast
-qed
-
-lemma closed_interval_right:
-  fixes a :: "'a::euclidean_space"
-  shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
-proof -
-  {
-    fix i :: 'a
-    assume i: "i \<in> Basis"
-    fix x :: "'a"
-    assume x: "\<forall>e>0. \<exists>x'\<in>{x. \<forall>i\<in>Basis. a \<bullet> i \<le> x \<bullet> i}. x' \<noteq> x \<and> dist x' x < e"
-    {
-      assume "a\<bullet>i > x\<bullet>i"
-      then obtain y where "a \<bullet> i \<le> y \<bullet> i"  "y \<noteq> x"  "dist y x < a\<bullet>i - x\<bullet>i"
-        using x[THEN spec[where x="a\<bullet>i - x\<bullet>i"]] i by auto
-      then have False
-        using Basis_le_norm[OF i, of "y - x"]
-        unfolding dist_norm inner_simps
-        by auto
-    }
-    then have "a\<bullet>i \<le> x\<bullet>i" by (rule ccontr) auto
-  }
-  then show ?thesis
-    unfolding closed_limpt unfolding islimpt_approachable by blast
-qed
-
 lemma open_box: "open (box a b)"
 proof -
   have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
@@ -6777,6 +6682,16 @@
 lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\<bullet>i \<ge> a}"
   by (simp add: closed_Collect_le)
 
+lemma closed_interval_left:
+  fixes b :: "'a::euclidean_space"
+  shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
+  by (simp add: Collect_ball_eq closed_INT closed_Collect_le)
+
+lemma closed_interval_right:
+  fixes a :: "'a::euclidean_space"
+  shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
+  by (simp add: Collect_ball_eq closed_INT closed_Collect_le)
+
 text {* Openness of halfspaces. *}
 
 lemma open_halfspace_lt: "open {x. inner a x < b}"
@@ -7314,58 +7229,24 @@
 lemma dim_substandard:
   assumes d: "d \<subseteq> Basis"
   shows "dim {x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0} = card d" (is "dim ?A = _")
-proof -
-  let ?D = "Basis :: 'a set"
-  have "d \<subseteq> ?A" using d by (auto simp: inner_Basis)
-  moreover
-  {
-    fix x::"'a" assume "x \<in> ?A"
-    then have "finite d" "x \<in> ?A"
-      using assms by (auto intro: finite_subset[OF _ finite_Basis])
-    from this d have "x \<in> span d"
-    proof (induct d arbitrary: x)
-      case empty
-      then have "x = 0"
-        apply (rule_tac euclidean_eqI)
-        apply auto
-        done
-      then show ?case
-        using subspace_0[OF subspace_span[of "{}"]] by auto
-    next
-      case (insert k F)
-      then have *: "\<forall>i\<in>Basis. i \<notin> insert k F \<longrightarrow> x \<bullet> i = 0" by auto
-      have **: "F \<subseteq> insert k F" by auto
-      def y \<equiv> "x - (x\<bullet>k) *\<^sub>R k"
-      have y: "x = y + (x\<bullet>k) *\<^sub>R k" unfolding y_def by auto
-      { fix i assume i': "i \<notin> F" "i \<in> Basis"
-        then have "y \<bullet> i = 0" unfolding y_def
-          using *[THEN bspec[where x=i]] insert by (auto simp: inner_simps inner_Basis) }
-      then have "y \<in> span F" using insert by auto
-      then have "y \<in> span (insert k F)"
-        using span_mono[of F "insert k F"] using assms by auto
-      moreover
-      have "k \<in> span (insert k F)" by(rule span_superset, auto)
-      then have "(x\<bullet>k) *\<^sub>R k \<in> span (insert k F)"
-        using span_mul by auto
-      ultimately
-      have "y + (x\<bullet>k) *\<^sub>R k \<in> span (insert k F)"
-        using span_add by auto
-      then show ?case using y by auto
-    qed
-  }
-  then have "?A \<subseteq> span d" by auto
-  moreover
-  {
-    fix x
-    assume "x \<in> d"
-    then have "x \<in> ?D" using assms by auto
-  }
-  then have "independent d"
-    using independent_mono[OF independent_Basis, of d] and assms by auto
-  moreover
-  have "d \<subseteq> ?D" unfolding subset_eq using assms by auto
-  ultimately show ?thesis using dim_unique[of d ?A] by auto
-qed
+proof (rule dim_unique)
+  show "d \<subseteq> ?A"
+    using d by (auto simp: inner_Basis)
+  show "independent d"
+    using independent_mono [OF independent_Basis d] .
+  show "?A \<subseteq> span d"
+  proof (clarify)
+    fix x assume x: "\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0"
+    have "finite d"
+      using finite_subset [OF d finite_Basis] .
+    then have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) \<in> span d"
+      by (simp add: span_setsum span_clauses)
+    also have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i)"
+      by (rule setsum_mono_zero_cong_left [OF finite_Basis d]) (auto simp add: x)
+    finally show "x \<in> span d"
+      unfolding euclidean_representation .
+  qed
+qed simp
 
 text{* Hence closure and completeness of all subspaces. *}