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.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.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]