author huffman Thu Aug 18 17:32:02 2011 -0700 (2011-08-18) changeset 44286 8766839efb1b parent 44284 584a590ce6d3 child 44287 598ed12b9bee
declare euclidean_component_zero[simp] at the point it is proved
```     1.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 23:43:22 2011 +0200
1.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 18 17:32:02 2011 -0700
1.3 @@ -126,7 +126,7 @@
1.4  lemmas isCont_euclidean_component [simp] =
1.5    bounded_linear.isCont [OF bounded_linear_euclidean_component]
1.6
1.7 -lemma euclidean_component_zero: "0 \$\$ i = 0"
1.8 +lemma euclidean_component_zero [simp]: "0 \$\$ i = 0"
1.9    unfolding euclidean_component_def by (rule inner_zero_right)
1.10
1.11  lemma euclidean_component_add: "(x + y) \$\$ i = x \$\$ i + y \$\$ i"
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 23:43:22 2011 +0200
2.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 18 17:32:02 2011 -0700
2.3 @@ -1756,7 +1756,7 @@
2.4    have Kp: "?K > 0" by arith
2.5      { assume C: "B < 0"
2.6        have "((\<chi>\<chi> i. 1)::'a) \<noteq> 0" unfolding euclidean_eq[where 'a='a]
2.7 -        by(auto intro!:exI[where x=0] simp add:euclidean_component_zero)
2.8 +        by(auto intro!:exI[where x=0])
2.9        hence "norm ((\<chi>\<chi> i. 1)::'a) > 0" by auto
2.10        with C have "B * norm ((\<chi>\<chi> i. 1)::'a) < 0"
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 23:43:22 2011 +0200
3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 18 17:32:02 2011 -0700
3.3 @@ -5570,9 +5570,6 @@
3.4
3.5  subsection {* Some properties of a canonical subspace *}
3.6
3.7 -(** move **)
3.8 -declare euclidean_component_zero[simp]
3.9 -
3.10  lemma subspace_substandard:
3.11    "subspace {x::'a::euclidean_space. (\<forall>i<DIM('a). P i \<longrightarrow> x\$\$i = 0)}"
3.12    unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)
```