# HG changeset patch
# User huffman
# Date 1314803507 25200
# Node ID bd17b7543af1bcf476fb89ba050d003d18b8b9bf
# Parent  134c06282ae6022bc588fb3140846f8ed158a92a
move lemmas from Topology_Euclidean_Space to Euclidean_Space

diff -r 134c06282ae6 -r bd17b7543af1 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Aug 31 07:51:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Wed Aug 31 08:11:47 2011 -0700
@@ -7,7 +7,7 @@
 
 theory Euclidean_Space
 imports
-  Complex_Main
+  L2_Norm
   "~~/src/HOL/Library/Inner_Product"
   "~~/src/HOL/Library/Product_Vector"
 begin
@@ -216,10 +216,20 @@
     simp add: inner_setsum_left inner_setsum_right
     dot_basis if_distrib setsum_cases mult_commute)
 
+lemma euclidean_dist_l2:
+  fixes x y :: "'a::euclidean_space"
+  shows "dist x y = setL2 (\<lambda>i. dist (x $$ i) (y $$ i)) {..<DIM('a)}"
+  unfolding dist_norm norm_eq_sqrt_inner setL2_def
+  by (simp add: euclidean_inner power2_eq_square)
+
 lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
   unfolding euclidean_component_def
   by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
 
+lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
+  unfolding euclidean_dist_l2 [where 'a='a]
+  by (cases "i < DIM('a)", rule member_le_setL2, auto)
+
 subsection {* Subclass relationships *}
 
 instance euclidean_space \<subseteq> perfect_space
diff -r 134c06282ae6 -r bd17b7543af1 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 31 07:51:55 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Wed Aug 31 08:11:47 2011 -0700
@@ -7,19 +7,9 @@
 header {* Elementary topology in Euclidean space. *}
 
 theory Topology_Euclidean_Space
-imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith L2_Norm
+imports SEQ Linear_Algebra "~~/src/HOL/Library/Glbs" Norm_Arith
 begin
 
-(* to be moved elsewhere *)
-
-lemma euclidean_dist_l2:"dist x (y::'a::euclidean_space) = setL2 (\<lambda>i. dist(x$$i) (y$$i)) {..<DIM('a)}"
-  unfolding dist_norm norm_eq_sqrt_inner setL2_def apply(subst euclidean_inner)
-  by(auto simp add:power2_eq_square)
-
-lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
-  apply(subst(2) euclidean_dist_l2) apply(cases "i<DIM('a)")
-  apply(rule member_le_setL2) by auto
-
 subsection {* General notion of a topology as a value *}
 
 definition "istopology L \<longleftrightarrow> L {} \<and> (\<forall>S T. L S \<longrightarrow> L T \<longrightarrow> L (S \<inter> T)) \<and> (\<forall>K. Ball K L \<longrightarrow> L (\<Union> K))"