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