# HG changeset patch
# User huffman
# Date 1313713922 25200
# Node ID 8766839efb1b90500817338139ae80229d03d1ad
# Parent  584a590ce6d3eb456bf771dfc78ab6d8a3e19191
declare euclidean_component_zero[simp] at the point it is proved

diff -r 584a590ce6d3 -r 8766839efb1b src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 23:43:22 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 17:32:02 2011 -0700
@@ -126,7 +126,7 @@
 lemmas isCont_euclidean_component [simp] =
   bounded_linear.isCont [OF bounded_linear_euclidean_component]
 
-lemma euclidean_component_zero: "0 $$ i = 0"
+lemma euclidean_component_zero [simp]: "0 $$ i = 0"
   unfolding euclidean_component_def by (rule inner_zero_right)
 
 lemma euclidean_component_add: "(x + y) $$ i = x $$ i + y $$ i"
diff -r 584a590ce6d3 -r 8766839efb1b src/HOL/Multivariate_Analysis/Linear_Algebra.thy
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 23:43:22 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 17:32:02 2011 -0700
@@ -1756,7 +1756,7 @@
   have Kp: "?K > 0" by arith
     { assume C: "B < 0"
       have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
-        by(auto intro!:exI[where x=0] simp add:euclidean_component_zero)
+        by(auto intro!:exI[where x=0])
       hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
       with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
         by (simp add: mult_less_0_iff)
diff -r 584a590ce6d3 -r 8766839efb1b src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 23:43:22 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 17:32:02 2011 -0700
@@ -5570,9 +5570,6 @@
 
 subsection {* Some properties of a canonical subspace *}
 
-(** move **)
-declare euclidean_component_zero[simp]
-
 lemma subspace_substandard:
   "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x$$i = 0)}"
   unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)