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.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.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.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.62    hence "((snd \<circ> h \<circ> r) ---> g a) sequentially" unfolding continuous_on_sequentially