src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44457 d366fa5551ef
parent 44365 5daa55003649
child 44516 d9a496ae5d9d
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 23 07:12:05 2011 -0700
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Tue Aug 23 14:11:02 2011 -0700
     1.3 @@ -14,7 +14,7 @@
     1.4  
     1.5  lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
     1.6    unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
     1.7 -  apply(auto simp add:power2_eq_square) unfolding euclidean_component_diff ..
     1.8 +  by(auto simp add:power2_eq_square)
     1.9  
    1.10  lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
    1.11    apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
    1.12 @@ -5601,26 +5601,17 @@
    1.13  
    1.14  lemma subspace_substandard:
    1.15    "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
    1.16 -  unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)
    1.17 +  unfolding subspace_def by auto
    1.18  
    1.19  lemma closed_substandard:
    1.20   "closed {x::'a::euclidean_space. \<forall>i<DIM('a). P i --> x$$i = 0}" (is "closed ?A")
    1.21  proof-
    1.22    let ?D = "{i. P i} \<inter> {..<DIM('a)}"
    1.23 -  let ?Bs = "{{x::'a. inner (basis i) x = 0}| i. i \<in> ?D}"
    1.24 -  { fix x
    1.25 -    { assume "x\<in>?A"
    1.26 -      hence x:"\<forall>i\<in>?D. x $$ i = 0" by auto
    1.27 -      hence "x\<in> \<Inter> ?Bs" by(auto simp add: x euclidean_component_def) }
    1.28 -    moreover
    1.29 -    { assume x:"x\<in>\<Inter>?Bs"
    1.30 -      { fix i assume i:"i \<in> ?D"
    1.31 -        then obtain B where BB:"B \<in> ?Bs" and B:"B = {x::'a. inner (basis i) x = 0}" by auto
    1.32 -        hence "x $$ i = 0" unfolding B using x unfolding euclidean_component_def by auto  }
    1.33 -      hence "x\<in>?A" by auto }
    1.34 -    ultimately have "x\<in>?A \<longleftrightarrow> x\<in> \<Inter>?Bs" .. }
    1.35 -  hence "?A = \<Inter> ?Bs" by auto
    1.36 -  thus ?thesis by(auto simp add: closed_Inter closed_hyperplane)
    1.37 +  have "closed (\<Inter>i\<in>?D. {x::'a. x$$i = 0})"
    1.38 +    by (simp add: closed_INT closed_Collect_eq)
    1.39 +  also have "(\<Inter>i\<in>?D. {x::'a. x$$i = 0}) = ?A"
    1.40 +    by auto
    1.41 +  finally show "closed ?A" .
    1.42  qed
    1.43  
    1.44  lemma dim_substandard: assumes "d\<subseteq>{..<DIM('a::euclidean_space)}"
    1.45 @@ -5645,7 +5636,7 @@
    1.46        have y:"x = y + (x$$k) *\<^sub>R basis k" unfolding y_def by auto
    1.47        { fix i assume i':"i \<notin> F"
    1.48          hence "y $$ i = 0" unfolding y_def 
    1.49 -          using *[THEN spec[where x=i]] by(auto simp add: euclidean_simps) }
    1.50 +          using *[THEN spec[where x=i]] by auto }
    1.51        hence "y \<in> span (basis ` F)" using insert(3) by auto
    1.52        hence "y \<in> span (basis ` (insert k F))"
    1.53          using span_mono[of "?bas ` F" "?bas ` (insert k F)"]
    1.54 @@ -5763,25 +5754,25 @@
    1.55    case False
    1.56    { fix y assume "a \<le> y" "y \<le> b" "m > 0"
    1.57      hence "m *\<^sub>R a + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R b + c"
    1.58 -      unfolding eucl_le[where 'a='a] by(auto simp add: euclidean_simps)
    1.59 +      unfolding eucl_le[where 'a='a] by auto
    1.60    } moreover
    1.61    { fix y assume "a \<le> y" "y \<le> b" "m < 0"
    1.62      hence "m *\<^sub>R b + c \<le> m *\<^sub>R y + c"  "m *\<^sub>R y + c \<le> m *\<^sub>R a + c"
    1.63 -      unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg euclidean_simps)
    1.64 +      unfolding eucl_le[where 'a='a] by(auto simp add: mult_left_mono_neg)
    1.65    } moreover
    1.66    { fix y assume "m > 0"  "m *\<^sub>R a + c \<le> y"  "y \<le> m *\<^sub>R b + c"
    1.67      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
    1.68        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
    1.69        apply(auto simp add: pth_3[symmetric] 
    1.70          intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"]) 
    1.71 -      by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff euclidean_simps)
    1.72 +      by(auto simp add: pos_le_divide_eq pos_divide_le_eq mult_commute diff_le_iff)
    1.73    } moreover
    1.74    { fix y assume "m *\<^sub>R b + c \<le> y" "y \<le> m *\<^sub>R a + c" "m < 0"
    1.75      hence "y \<in> (\<lambda>x. m *\<^sub>R x + c) ` {a..b}"
    1.76        unfolding image_iff Bex_def mem_interval eucl_le[where 'a='a]
    1.77        apply(auto simp add: pth_3[symmetric]
    1.78          intro!: exI[where x="(1 / m) *\<^sub>R (y - c)"])
    1.79 -      by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff euclidean_simps)
    1.80 +      by(auto simp add: neg_le_divide_eq neg_divide_le_eq mult_commute diff_le_iff)
    1.81    }
    1.82    ultimately show ?thesis using False by auto
    1.83  qed