src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
 changeset 44167 e81d676d598e parent 44139 abccf1b7ea4b child 44170 510ac30f44c0
```     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 11 13:05:56 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 11 14:24:05 2011 -0700
1.3 @@ -479,7 +479,7 @@
1.4    { fix e :: real assume "0 < e"
1.5      def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))"
1.6      from `0 < e` have "y \<noteq> x"
1.7 -      unfolding y_def by (simp add: sgn_zero_iff basis_eq_0_iff DIM_positive)
1.8 +      unfolding y_def by (simp add: sgn_zero_iff DIM_positive)
1.9      from `0 < e` have "dist y x < e"
1.10        unfolding y_def by (simp add: dist_norm norm_sgn)
1.11      from `y \<noteq> x` and `dist y x < e`
1.12 @@ -5646,7 +5646,7 @@
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)
1.17 +  unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)
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 @@ -5674,7 +5674,7 @@
1.22    let ?D = "{..<DIM('a)}"
1.23    let ?B = "(basis::nat => 'a) ` d"
1.24    let ?bas = "basis::nat \<Rightarrow> 'a"
1.25 -  have "?B \<subseteq> ?A" by(auto simp add:basis_component)
1.26 +  have "?B \<subseteq> ?A" by auto
1.27    moreover
1.28    { fix x::"'a" assume "x\<in>?A"
1.29      hence "finite d" "x\<in>?A" using assms by(auto intro:finite_subset)
1.30 @@ -5690,7 +5690,7 @@
1.31        have y:"x = y + (x\$\$k) *\<^sub>R basis k" unfolding y_def by auto
1.32        { fix i assume i':"i \<notin> F"
1.33          hence "y \$\$ i = 0" unfolding y_def
1.34 -          using *[THEN spec[where x=i]] by(auto simp add: euclidean_simps basis_component) }
1.35 +          using *[THEN spec[where x=i]] by(auto simp add: euclidean_simps) }
1.36        hence "y \<in> span (basis ` F)" using insert(3) by auto
1.37        hence "y \<in> span (basis ` (insert k F))"
1.38          using span_mono[of "?bas ` F" "?bas ` (insert k F)"]
1.39 @@ -6025,7 +6025,7 @@
1.40    have lima:"((fst \<circ> (h \<circ> r)) ---> a) sequentially"
1.41     and limb:"((snd \<circ> (h \<circ> r)) ---> b) sequentially"
1.42      using lr
1.43 -    unfolding o_def a_def b_def by (simp_all add: tendsto_intros)
1.44 +    unfolding o_def a_def b_def by (rule tendsto_intros)+
1.45
1.46    { fix n::nat
1.47      have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_norm by norm
```