src/HOL/Library/Topology_Euclidean_Space.thy

 *)
 
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-  imports SEQ Euclidean_Space
+imports SEQ Euclidean_Space
 begin
-
 
 declare fstcart_pastecart[simp] sndcart_pastecart[simp]
 
 subsection{* General notion of a topology *}
 

   let ?U = "ball x (dist x y / 2)"
   let ?V = "ball y (dist x y / 2)"
   have th0: "\<And>d x y z. (d x z :: real) <= d x y + d y z \<Longrightarrow> d y z = d z y
                ==> ~(d x y * 2 < d x z \<and> d z y * 2 < d x z)" by arith
   have "?P ?U ?V" using dist_pos_lt[OF xy] th0[of dist,OF dist_triangle dist_sym]
-    by (auto simp add: dist_refl expand_set_eq Arith_Tools.less_divide_eq_number_of1)
+    by (auto simp add: dist_refl expand_set_eq less_divide_eq_number_of1)
   then show ?thesis by blast
 qed
 
 lemma separation_t2: "x \<noteq> y \<longleftrightarrow> (\<exists>U V. open U \<and> open V \<and> x \<in> U \<and> y \<in> V \<and> U \<inter> V = {})"
   using hausdorff[of x y] by blast

 	let ?k = "min d (e - dist x y)"
 	have kp: "?k > 0" using d e(1) y[unfolded mem_ball] by norm
 	have "?k/2 \<ge> 0" using kp by simp
 	then obtain w where w: "dist y w = ?k/ 2" by (metis vector_choose_dist)
 	from iT[unfolded expand_set_eq mem_interior]
-	have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+	have "\<not> ball w (?k/4) \<subseteq> T" using kp by (auto simp add: less_divide_eq_number_of1)
 	then obtain z where z: "dist w z < ?k/4" "z \<notin> T" by (auto simp add: subset_eq)
 	have "z \<notin> T \<and> z\<noteq> y \<and> dist z y < d \<and> dist x z < e" using z apply simp
 	  using w e(1) d apply (auto simp only: dist_sym)
 	  apply (auto simp add: min_def cong del: if_weak_cong)
 	  apply (cases "d \<le> e - dist x y", auto simp add: ring_simps cong del: if_weak_cong)

   assume as:"(f ---> l) net" "(g ---> m) net"
   { fix e::real
     assume "e>0"
     hence *:"eventually (\<lambda>x. dist (f x) l < e/2) net"
             "eventually (\<lambda>x. dist (g x) m < e/2) net" using as
-      by (auto intro: tendstoD simp del: Arith_Tools.less_divide_eq_number_of1)
+      by (auto intro: tendstoD simp del: less_divide_eq_number_of1)
     hence "eventually (\<lambda>x. dist (f x + g x) (l + m) < e) net"
     proof(cases "trivial_limit net")
       case True
       thus ?thesis unfolding eventually_def by auto
     next

     { fix x assume "netord net x y"
       hence *:"\<bar>f x - l\<bar> < min (\<bar>l\<bar> / 2) (l\<twosuperior> * e / 2)" using y[THEN spec[where x=x]] unfolding o_def dist_vec1 by auto
       hence fx0:"f x \<noteq> 0" using `l \<noteq> 0` by auto
       hence fxl0: "(f x) * l \<noteq> 0" using `l \<noteq> 0` by auto
       from * have **:"\<bar>f x - l\<bar> < l\<twosuperior> * e / 2" by auto
-      have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: Arith_Tools.less_divide_eq_number_of1)
+      have "\<bar>f x\<bar> * 2 \<ge> \<bar>l\<bar>" using * by (auto simp del: less_divide_eq_number_of1)
       hence "\<bar>f x\<bar> * 2 * \<bar>l\<bar>  \<ge> \<bar>l\<bar> * \<bar>l\<bar>" unfolding mult_le_cancel_right by auto
       hence "\<bar>f x * l\<bar> * 2  \<ge> \<bar>l\<bar>^2" unfolding real_mult_commute and power2_eq_square by auto
       hence ***:"inverse \<bar>f x * l\<bar> \<le> inverse (l\<twosuperior> / 2)" using fxl0
 	using le_imp_inverse_le[of "l^2 / 2" "\<bar>f x * l\<bar>"]  by auto
 

     let ?x = "(1/2) *s (a + b)"
     { fix i
       have "a$i < b$i" using as[THEN spec[where x=i]] by auto
       hence "a$i < ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i < b$i"
 	unfolding vector_smult_component and vector_add_component
-	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)  }
+	by (auto simp add: less_divide_eq_number_of1)  }
     hence "{a <..< b} \<noteq> {}" using mem_interval(1)[of "?x" a b] by auto  }
   ultimately show ?th1 by blast
 
   { fix i x assume as:"b$i < a$i" and x:"x\<in>{a .. b}"
     hence "a $ i \<le> x $ i \<and> x $ i \<le> b $ i" unfolding mem_interval by auto

     let ?x = "(1/2) *s (a + b)"
     { fix i
       have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto
       hence "a$i \<le> ((1/2) *s (a+b)) $ i" "((1/2) *s (a+b)) $ i \<le> b$i"
 	unfolding vector_smult_component and vector_add_component
-	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)  }
+	by (auto simp add: less_divide_eq_number_of1)  }
     hence "{a .. b} \<noteq> {}" using mem_interval(2)[of "?x" a b] by auto  }
   ultimately show ?th2 by blast
 qed
 
 lemma interval_ne_empty: fixes a :: "real^'n::finite" shows

     { let ?x = "(\<chi> j. (if j=i then ((min (a$j) (d$j))+c$j)/2 else (c$j+d$j)/2))::real^'n"
       assume as2: "a$i > c$i"
       { fix j
 	have "c $ j < ?x $ j \<and> ?x $ j < d $ j" unfolding Cart_lambda_beta
 	  apply(cases "j=i") using as(2)[THEN spec[where x=j]]
-	  by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2)  }
+	  by (auto simp add: less_divide_eq_number_of1 as2)  }
       hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
       moreover
       have "?x\<notin>{a .. b}"
 	unfolding mem_interval apply auto apply(rule_tac x=i in exI)
 	using as(2)[THEN spec[where x=i]] and as2
-	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+	by (auto simp add: less_divide_eq_number_of1)
       ultimately have False using as by auto  }
     hence "a$i \<le> c$i" by(rule ccontr)auto
     moreover
     { let ?x = "(\<chi> j. (if j=i then ((max (b$j) (c$j))+d$j)/2 else (c$j+d$j)/2))::real^'n"
       assume as2: "b$i < d$i"
       { fix j
 	have "d $ j > ?x $ j \<and> ?x $ j > c $ j" unfolding Cart_lambda_beta
 	  apply(cases "j=i") using as(2)[THEN spec[where x=j]]
-	  by (auto simp add: Arith_Tools.less_divide_eq_number_of1 as2)  }
+	  by (auto simp add: less_divide_eq_number_of1 as2)  }
       hence "?x\<in>{c<..<d}" unfolding mem_interval by auto
       moreover
       have "?x\<notin>{a .. b}"
 	unfolding mem_interval apply auto apply(rule_tac x=i in exI)
 	using as(2)[THEN spec[where x=i]] and as2
-	by (auto simp add: Arith_Tools.less_divide_eq_number_of1)
+	by (auto simp add: less_divide_eq_number_of1)
       ultimately have False using as by auto  }
     hence "b$i \<ge> d$i" by(rule ccontr)auto
     ultimately
     have "a$i \<le> c$i \<and> d$i \<le> b$i" by auto
   } note part1 = this

 qed
 
 lemma inter_interval: fixes a :: "'a::linorder^'n::finite" shows
  "{a .. b} \<inter> {c .. d} =  {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}"
   unfolding expand_set_eq and Int_iff and mem_interval
-  by (auto simp add: Arith_Tools.less_divide_eq_number_of1 intro!: bexI)
+  by (auto simp add: less_divide_eq_number_of1 intro!: bexI)
 
 (* Moved interval_open_subset_closed a bit upwards *)
 
 lemma open_interval_lemma: fixes x :: "real" shows
  "a < x \<Longrightarrow> x < b ==> (\<exists>d>0. \<forall>x'. abs(x' - x) < d --> a < x' \<and> x' < b)"

 proof-
   { fix i
     have "a $ i < ((1 / 2) *s (a + b)) $ i \<and> ((1 / 2) *s (a + b)) $ i < b $ i"
       using assms[unfolded interval_ne_empty, THEN spec[where x=i]]
       unfolding vector_smult_component and vector_add_component
-      by(auto simp add: Arith_Tools.less_divide_eq_number_of1)  }
+      by(auto simp add: less_divide_eq_number_of1)  }
   thus ?thesis unfolding mem_interval by auto
 qed
 
 lemma open_closed_interval_convex: fixes x :: "real^'n::finite"
   assumes x:"x \<in> {a<..<b}" and y:"y \<in> {a .. b}" and e:"0 < e" "e \<le> 1"

 	using norm_minus_cancel[of "x - y"] by (auto simp add: uminus_add_conv_diff) } note ** = this
 
     { assume as:"dist a b > dist (f n x) (f n y)"
       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"
 	and "\<forall>m\<ge>Nb. dist (f (r m) y) b < (dist a b - dist (f n x) (f n y)) / 2"
-	using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: Arith_Tools.less_divide_eq_number_of1)
+	using lima limb unfolding h_def Lim_sequentially by (fastsimp simp del: less_divide_eq_number_of1)
       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)"
 	apply(erule_tac x="Na+Nb+n" in allE)
 	apply(erule_tac x="Na+Nb+n" in allE) apply simp
 	using dist_triangle_add_half[of a "f (r (Na + Nb + n)) x" "dist a b - dist (f n x) (f n y)"
           "-b"  "- f (r (Na + Nb + n)) y"]