src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
changeset 44890 22f665a2e91c
parent 44668 31d41a0f6b5d
child 44905 3e8cc9046731
     1.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -4224,8 +4224,8 @@
     1.4      unfolding compact_eq_bounded_closed
     1.5      using bounded_Int and closed_Int and assms(1) by auto
     1.6    ultimately obtain x where "x\<in>cball a (dist b a) \<inter> s" "\<forall>y\<in>cball a (dist b a) \<inter> s. dist a x \<le> dist a y"
     1.7 -    using continuous_attains_inf[of ?B "dist a"] by fastsimp
     1.8 -  thus ?thesis by fastsimp
     1.9 +    using continuous_attains_inf[of ?B "dist a"] by fastforce
    1.10 +  thus ?thesis by fastforce
    1.11  qed
    1.12  
    1.13  
    1.14 @@ -4603,7 +4603,7 @@
    1.15  lemma interval_ne_empty: fixes a :: "'a::ordered_euclidean_space" shows
    1.16    "{a  ..  b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i \<le> b$$i)" and
    1.17    "{a <..< b} \<noteq> {} \<longleftrightarrow> (\<forall>i<DIM('a). a$$i < b$$i)"
    1.18 -  unfolding interval_eq_empty[of a b] by fastsimp+
    1.19 +  unfolding interval_eq_empty[of a b] by fastforce+
    1.20  
    1.21  lemma interval_sing:
    1.22    fixes a :: "'a::ordered_euclidean_space"
    1.23 @@ -4672,7 +4672,7 @@
    1.24    } note part1 = this
    1.25    show ?th3 unfolding subset_eq and Ball_def and mem_interval 
    1.26      apply(rule,rule,rule,rule) apply(rule part1) unfolding subset_eq and Ball_def and mem_interval
    1.27 -    prefer 4 apply auto by(erule_tac x=i in allE,erule_tac x=i in allE,fastsimp)+ 
    1.28 +    prefer 4 apply auto by(erule_tac x=i in allE,erule_tac x=i in allE,fastforce)+ 
    1.29    { assume as:"{c<..<d} \<subseteq> {a<..<b}" "\<forall>i<DIM('a). c$$i < d$$i"
    1.30      fix i assume i:"i<DIM('a)"
    1.31      from as(1) have "{c<..<d} \<subseteq> {a..b}" using interval_open_subset_closed[of a b] by auto
    1.32 @@ -5834,7 +5834,7 @@
    1.33      { assume as:"dist a b > dist (f n x) (f n y)"
    1.34        then obtain Na Nb where "\<forall>m\<ge>Na. dist (f (r m) x) a < (dist a b - dist (f n x) (f n y)) / 2"
    1.35          and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
    1.36 -        using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: less_divide_eq_number_of1)
    1.37 +        using lima limb unfolding h_def Lim_sequentially by (fastforce simp del: less_divide_eq_number_of1)
    1.38        hence "dist (f (r (Na + Nb + n)) x - f (r (Na + Nb + n)) y) (a - b) < dist a b - dist (f n x) (f n y)"
    1.39          apply(erule_tac x="Na+Nb+n" in allE)
    1.40          apply(erule_tac x="Na+Nb+n" in allE) apply simp
    1.41 @@ -5853,10 +5853,10 @@
    1.42  
    1.43    have [simp]:"a = b" proof(rule ccontr)
    1.44      def e \<equiv> "dist a b - dist (g a) (g b)"
    1.45 -    assume "a\<noteq>b" hence "e > 0" unfolding e_def using dist by fastsimp
    1.46 +    assume "a\<noteq>b" hence "e > 0" unfolding e_def using dist by fastforce
    1.47      hence "\<exists>n. dist (f n x) a < e/2 \<and> dist (f n y) b < e/2"
    1.48        using lima limb unfolding Lim_sequentially
    1.49 -      apply (auto elim!: allE[where x="e/2"]) apply(rule_tac x="r (max N Na)" in exI) unfolding h_def by fastsimp
    1.50 +      apply (auto elim!: allE[where x="e/2"]) apply(rule_tac x="r (max N Na)" in exI) unfolding h_def by fastforce
    1.51      then obtain n where n:"dist (f n x) a < e/2 \<and> dist (f n y) b < e/2" by auto
    1.52      have "dist (f (Suc n) x) (g a) \<le> dist (f n x) a"
    1.53        using dist[THEN bspec[where x="f n x"], THEN bspec[where x="a"]] and fs by auto
    1.54 @@ -5869,7 +5869,7 @@
    1.55    have [simp]:"\<And>n. f (Suc n) x = f n y" unfolding f_def y_def by(induct_tac n)auto
    1.56    { fix x y assume "x\<in>s" "y\<in>s" moreover
    1.57      fix e::real assume "e>0" ultimately
    1.58 -    have "dist y x < e \<longrightarrow> dist (g y) (g x) < e" using dist by fastsimp }
    1.59 +    have "dist y x < e \<longrightarrow> dist (g y) (g x) < e" using dist by fastforce }
    1.60    hence "continuous_on s g" unfolding continuous_on_iff by auto
    1.61  
    1.62    hence "((snd \<circ> h \<circ> r) ---> g a) sequentially" unfolding continuous_on_sequentially