tuned proofs
authorhuffman
Mon Sep 23 16:56:17 2013 -0700 (2013-09-23)
changeset 538130a62ad289c4d
parent 53812 369537953d05
child 53814 255a2929c137
child 53820 9c7e97d67b45
tuned proofs
src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Sep 24 00:21:40 2013 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 23 16:56:17 2013 -0700
     1.3 @@ -5776,59 +5776,16 @@
     1.4    fixes s :: "'a::real_normed_vector set"
     1.5    assumes "closed s"
     1.6    shows "closed ((\<lambda>x. c *\<^sub>R x) ` s)"
     1.7 -proof (cases "s = {}")
     1.8 -  case True
     1.9 -  then show ?thesis by auto
    1.10 +proof (cases "c = 0")
    1.11 +  case True then show ?thesis
    1.12 +    by (auto simp add: image_constant_conv)
    1.13  next
    1.14    case False
    1.15 -  show ?thesis
    1.16 -  proof (cases "c = 0")
    1.17 -    have *: "(\<lambda>x. 0) ` s = {0}" using `s\<noteq>{}` by auto
    1.18 -    case True
    1.19 -    then show ?thesis
    1.20 -      apply auto
    1.21 -      unfolding *
    1.22 -      apply auto
    1.23 -      done
    1.24 -  next
    1.25 -    case False
    1.26 -    {
    1.27 -      fix x l
    1.28 -      assume as: "\<forall>n::nat. x n \<in> scaleR c ` s"  "(x ---> l) sequentially"
    1.29 -      {
    1.30 -        fix n :: nat
    1.31 -        have "scaleR (1 / c) (x n) \<in> s"
    1.32 -          using as(1)[THEN spec[where x=n]]
    1.33 -          using `c\<noteq>0`
    1.34 -          by auto
    1.35 -      }
    1.36 -      moreover
    1.37 -      {
    1.38 -        fix e :: real
    1.39 -        assume "e > 0"
    1.40 -        then have "0 < e *\<bar>c\<bar>"
    1.41 -          using `c\<noteq>0` mult_pos_pos[of e "abs c"] by auto
    1.42 -        then obtain N where "\<forall>n\<ge>N. dist (x n) l < e * \<bar>c\<bar>"
    1.43 -          using as(2)[unfolded LIMSEQ_def, THEN spec[where x="e * abs c"]] by auto
    1.44 -        then have "\<exists>N. \<forall>n\<ge>N. dist (scaleR (1 / c) (x n)) (scaleR (1 / c) l) < e"
    1.45 -          unfolding dist_norm
    1.46 -          unfolding scaleR_right_diff_distrib[symmetric]
    1.47 -          using mult_imp_div_pos_less[of "abs c" _ e] `c\<noteq>0` by auto
    1.48 -      }
    1.49 -      then have "((\<lambda>n. scaleR (1 / c) (x n)) ---> scaleR (1 / c) l) sequentially"
    1.50 -        unfolding LIMSEQ_def by auto
    1.51 -      ultimately have "l \<in> scaleR c ` s"
    1.52 -        using assms[unfolded closed_sequential_limits,
    1.53 -          THEN spec[where x="\<lambda>n. scaleR (1/c) (x n)"],
    1.54 -          THEN spec[where x="scaleR (1/c) l"]]
    1.55 -        unfolding image_iff using `c\<noteq>0`
    1.56 -          apply (rule_tac x="scaleR (1 / c) l" in bexI)
    1.57 -          apply auto
    1.58 -          done
    1.59 -    }
    1.60 -    then show ?thesis
    1.61 -      unfolding closed_sequential_limits by fast
    1.62 -  qed
    1.63 +  from assms have "closed ((\<lambda>x. inverse c *\<^sub>R x) -` s)"
    1.64 +    by (simp add: continuous_closed_vimage)
    1.65 +  also have "(\<lambda>x. inverse c *\<^sub>R x) -` s = (\<lambda>x. c *\<^sub>R x) ` s"
    1.66 +    using `c \<noteq> 0` by (auto elim: image_eqI [rotated])
    1.67 +  finally show ?thesis .
    1.68  qed
    1.69  
    1.70  lemma closed_negations:
    1.71 @@ -6576,58 +6533,6 @@
    1.72    unfolding closure_open_interval[OF assms, symmetric]
    1.73    unfolding open_inter_closure_eq_empty[OF open_interval] ..
    1.74  
    1.75 -
    1.76 -(* Some stuff for half-infinite intervals too; FIXME: notation?  *)
    1.77 -
    1.78 -lemma closed_interval_left:
    1.79 -  fixes b :: "'a::euclidean_space"
    1.80 -  shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
    1.81 -proof -
    1.82 -  {
    1.83 -    fix i :: 'a
    1.84 -    assume i: "i \<in> Basis"
    1.85 -    fix x :: "'a"
    1.86 -    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"
    1.87 -    {
    1.88 -      assume "x\<bullet>i > b\<bullet>i"
    1.89 -      then obtain y where "y \<bullet> i \<le> b \<bullet> i"  "y \<noteq> x"  "dist y x < x\<bullet>i - b\<bullet>i"
    1.90 -        using x[THEN spec[where x="x\<bullet>i - b\<bullet>i"]] using i by auto
    1.91 -      then have False
    1.92 -        using Basis_le_norm[OF i, of "y - x"]
    1.93 -        unfolding dist_norm inner_simps
    1.94 -        using i
    1.95 -        by auto
    1.96 -    }
    1.97 -    then have "x\<bullet>i \<le> b\<bullet>i" by (rule ccontr)auto
    1.98 -  }
    1.99 -  then show ?thesis
   1.100 -    unfolding closed_limpt unfolding islimpt_approachable by blast
   1.101 -qed
   1.102 -
   1.103 -lemma closed_interval_right:
   1.104 -  fixes a :: "'a::euclidean_space"
   1.105 -  shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
   1.106 -proof -
   1.107 -  {
   1.108 -    fix i :: 'a
   1.109 -    assume i: "i \<in> Basis"
   1.110 -    fix x :: "'a"
   1.111 -    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"
   1.112 -    {
   1.113 -      assume "a\<bullet>i > x\<bullet>i"
   1.114 -      then obtain y where "a \<bullet> i \<le> y \<bullet> i"  "y \<noteq> x"  "dist y x < a\<bullet>i - x\<bullet>i"
   1.115 -        using x[THEN spec[where x="a\<bullet>i - x\<bullet>i"]] i by auto
   1.116 -      then have False
   1.117 -        using Basis_le_norm[OF i, of "y - x"]
   1.118 -        unfolding dist_norm inner_simps
   1.119 -        by auto
   1.120 -    }
   1.121 -    then have "a\<bullet>i \<le> x\<bullet>i" by (rule ccontr) auto
   1.122 -  }
   1.123 -  then show ?thesis
   1.124 -    unfolding closed_limpt unfolding islimpt_approachable by blast
   1.125 -qed
   1.126 -
   1.127  lemma open_box: "open (box a b)"
   1.128  proof -
   1.129    have "open (\<Inter>i\<in>Basis. (op \<bullet> i) -` {a \<bullet> i <..< b \<bullet> i})"
   1.130 @@ -6777,6 +6682,16 @@
   1.131  lemma closed_halfspace_component_ge: "closed {x::'a::euclidean_space. x\<bullet>i \<ge> a}"
   1.132    by (simp add: closed_Collect_le)
   1.133  
   1.134 +lemma closed_interval_left:
   1.135 +  fixes b :: "'a::euclidean_space"
   1.136 +  shows "closed {x::'a. \<forall>i\<in>Basis. x\<bullet>i \<le> b\<bullet>i}"
   1.137 +  by (simp add: Collect_ball_eq closed_INT closed_Collect_le)
   1.138 +
   1.139 +lemma closed_interval_right:
   1.140 +  fixes a :: "'a::euclidean_space"
   1.141 +  shows "closed {x::'a. \<forall>i\<in>Basis. a\<bullet>i \<le> x\<bullet>i}"
   1.142 +  by (simp add: Collect_ball_eq closed_INT closed_Collect_le)
   1.143 +
   1.144  text {* Openness of halfspaces. *}
   1.145  
   1.146  lemma open_halfspace_lt: "open {x. inner a x < b}"
   1.147 @@ -7314,58 +7229,24 @@
   1.148  lemma dim_substandard:
   1.149    assumes d: "d \<subseteq> Basis"
   1.150    shows "dim {x::'a::euclidean_space. \<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x\<bullet>i = 0} = card d" (is "dim ?A = _")
   1.151 -proof -
   1.152 -  let ?D = "Basis :: 'a set"
   1.153 -  have "d \<subseteq> ?A" using d by (auto simp: inner_Basis)
   1.154 -  moreover
   1.155 -  {
   1.156 -    fix x::"'a" assume "x \<in> ?A"
   1.157 -    then have "finite d" "x \<in> ?A"
   1.158 -      using assms by (auto intro: finite_subset[OF _ finite_Basis])
   1.159 -    from this d have "x \<in> span d"
   1.160 -    proof (induct d arbitrary: x)
   1.161 -      case empty
   1.162 -      then have "x = 0"
   1.163 -        apply (rule_tac euclidean_eqI)
   1.164 -        apply auto
   1.165 -        done
   1.166 -      then show ?case
   1.167 -        using subspace_0[OF subspace_span[of "{}"]] by auto
   1.168 -    next
   1.169 -      case (insert k F)
   1.170 -      then have *: "\<forall>i\<in>Basis. i \<notin> insert k F \<longrightarrow> x \<bullet> i = 0" by auto
   1.171 -      have **: "F \<subseteq> insert k F" by auto
   1.172 -      def y \<equiv> "x - (x\<bullet>k) *\<^sub>R k"
   1.173 -      have y: "x = y + (x\<bullet>k) *\<^sub>R k" unfolding y_def by auto
   1.174 -      { fix i assume i': "i \<notin> F" "i \<in> Basis"
   1.175 -        then have "y \<bullet> i = 0" unfolding y_def
   1.176 -          using *[THEN bspec[where x=i]] insert by (auto simp: inner_simps inner_Basis) }
   1.177 -      then have "y \<in> span F" using insert by auto
   1.178 -      then have "y \<in> span (insert k F)"
   1.179 -        using span_mono[of F "insert k F"] using assms by auto
   1.180 -      moreover
   1.181 -      have "k \<in> span (insert k F)" by(rule span_superset, auto)
   1.182 -      then have "(x\<bullet>k) *\<^sub>R k \<in> span (insert k F)"
   1.183 -        using span_mul by auto
   1.184 -      ultimately
   1.185 -      have "y + (x\<bullet>k) *\<^sub>R k \<in> span (insert k F)"
   1.186 -        using span_add by auto
   1.187 -      then show ?case using y by auto
   1.188 -    qed
   1.189 -  }
   1.190 -  then have "?A \<subseteq> span d" by auto
   1.191 -  moreover
   1.192 -  {
   1.193 -    fix x
   1.194 -    assume "x \<in> d"
   1.195 -    then have "x \<in> ?D" using assms by auto
   1.196 -  }
   1.197 -  then have "independent d"
   1.198 -    using independent_mono[OF independent_Basis, of d] and assms by auto
   1.199 -  moreover
   1.200 -  have "d \<subseteq> ?D" unfolding subset_eq using assms by auto
   1.201 -  ultimately show ?thesis using dim_unique[of d ?A] by auto
   1.202 -qed
   1.203 +proof (rule dim_unique)
   1.204 +  show "d \<subseteq> ?A"
   1.205 +    using d by (auto simp: inner_Basis)
   1.206 +  show "independent d"
   1.207 +    using independent_mono [OF independent_Basis d] .
   1.208 +  show "?A \<subseteq> span d"
   1.209 +  proof (clarify)
   1.210 +    fix x assume x: "\<forall>i\<in>Basis. i \<notin> d \<longrightarrow> x \<bullet> i = 0"
   1.211 +    have "finite d"
   1.212 +      using finite_subset [OF d finite_Basis] .
   1.213 +    then have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) \<in> span d"
   1.214 +      by (simp add: span_setsum span_clauses)
   1.215 +    also have "(\<Sum>i\<in>d. (x \<bullet> i) *\<^sub>R i) = (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i)"
   1.216 +      by (rule setsum_mono_zero_cong_left [OF finite_Basis d]) (auto simp add: x)
   1.217 +    finally show "x \<in> span d"
   1.218 +      unfolding euclidean_representation .
   1.219 +  qed
   1.220 +qed simp
   1.221  
   1.222  text{* Hence closure and completeness of all subspaces. *}
   1.223