merged
authorhuffman
Fri, 12 Aug 2011 07:13:12 -0700
changeset 44168 9c120cde98f9
parent 44167 e81d676d598e (diff)
parent 44157 a21d3e1e64fd (current diff)
child 44169 bdcc11b2fdc8
merged
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Fri Aug 12 07:13:12 2011 -0700
@@ -467,7 +467,7 @@
 text {* some lemmas to map between Eucl and Cart *}
 lemma basis_real_n[simp]:"(basis (\<pi>' i)::real^'a) = cart_basis i"
   unfolding basis_vec_def using pi'_range[where 'n='a]
-  by (auto simp: vec_eq_iff)
+  by (auto simp: vec_eq_iff axis_def)
 
 subsection {* Orthogonality on cartesian products *}
 
@@ -866,7 +866,7 @@
     obtain g where g: "linear g" "g o op *v A = id" by blast
     have "matrix g ** A = mat 1"
       unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
-      using g(2) by (simp add: o_def id_def stupid_ext)
+      using g(2) by (simp add: fun_eq_iff)
     then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast}
   ultimately show ?thesis by blast
 qed
@@ -894,7 +894,7 @@
     have "A ** (matrix g) = mat 1"
       unfolding matrix_eq  matrix_vector_mul_lid
         matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
-      using g(2) unfolding o_def stupid_ext[symmetric] id_def
+      using g(2) unfolding o_def fun_eq_iff id_def
       .
     hence "\<exists>B. A ** (B::real^'m^'n) = mat 1" by blast
   }
@@ -1635,11 +1635,8 @@
 abbreviation dest_vec1:: "'a ^1 \<Rightarrow> 'a"
   where "dest_vec1 x \<equiv> (x$1)"
 
-lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y"
-  by (simp_all add:  vec_eq_iff)
-
-lemma vec1_component[simp]: "(vec1 x)$1 = x"
-  by (simp_all add:  vec_eq_iff)
+lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x"
+  by (simp add: vec_eq_iff)
 
 lemma forall_vec1: "(\<forall>x. P x) \<longleftrightarrow> (\<forall>x. P (vec1 x))"
   by (metis vec1_dest_vec1(1))
@@ -1647,9 +1644,6 @@
 lemma exists_vec1: "(\<exists>x. P x) \<longleftrightarrow> (\<exists>x. P(vec1 x))"
   by (metis vec1_dest_vec1(1))
 
-lemma vec1_eq[simp]:  "vec1 x = vec1 y \<longleftrightarrow> x = y"
-  by (metis vec1_dest_vec1(2))
-
 lemma dest_vec1_eq[simp]: "dest_vec1 x = dest_vec1 y \<longleftrightarrow> x = y"
   by (metis vec1_dest_vec1(1))
 
@@ -1741,12 +1735,12 @@
   by (simp add: vec_def norm_real)
 
 lemma dist_vec1: "dist(vec1 x) (vec1 y) = abs(x - y)"
-  by (simp only: dist_real vec1_component)
+  by (simp only: dist_real vec_component)
 lemma abs_dest_vec1: "norm x = \<bar>dest_vec1 x\<bar>"
   by (metis vec1_dest_vec1(1) norm_vec1)
 
 lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component
-   vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def real_norm_def
+   vec_inj[where 'b=1] vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def real_norm_def
 
 lemma bounded_linear_vec1:"bounded_linear (vec1::real\<Rightarrow>real^1)"
   unfolding bounded_linear_def additive_def bounded_linear_axioms_def 
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Aug 12 07:13:12 2011 -0700
@@ -15,22 +15,75 @@
 subsection {* Type class of Euclidean spaces *}
 
 class euclidean_space = real_inner +
+  fixes Basis :: "'a set"
+  assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
+  assumes finite_Basis [simp]: "finite Basis"
+  assumes inner_Basis:
+    "\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)"
+  assumes euclidean_all_zero_iff:
+    "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
+
+  -- "FIXME: make this a separate definition"
   fixes dimension :: "'a itself \<Rightarrow> nat"
+  assumes dimension_def: "dimension TYPE('a) = card Basis"
+
+  -- "FIXME: eventually basis function can be removed"
   fixes basis :: "nat \<Rightarrow> 'a"
-  assumes DIM_positive [intro]:
-    "0 < dimension TYPE('a)"
-  assumes basis_zero [simp]:
-    "dimension TYPE('a) \<le> i \<Longrightarrow> basis i = 0"
-  assumes basis_orthonormal:
-    "\<forall>i<dimension TYPE('a). \<forall>j<dimension TYPE('a).
-      inner (basis i) (basis j) = (if i = j then 1 else 0)"
-  assumes euclidean_all_zero:
-    "(\<forall>i<dimension TYPE('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)"
+  assumes image_basis: "basis ` {..<dimension TYPE('a)} = Basis"
+  assumes basis_finite: "basis ` {dimension TYPE('a)..} = {0}"
 
 syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
 
 translations "DIM('t)" == "CONST dimension (TYPE('t))"
 
+lemma (in euclidean_space) norm_Basis: "u \<in> Basis \<Longrightarrow> norm u = 1"
+  unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)
+
+lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
+  unfolding sgn_div_norm by (simp add: norm_Basis scaleR_one)
+
+lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
+proof
+  assume "0 \<in> Basis" thus "False"
+    using inner_Basis [of 0 0] by simp
+qed
+
+lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0"
+  by clarsimp
+
+text {* Lemmas related to @{text basis} function. *}
+
+lemma (in euclidean_space) euclidean_all_zero:
+  "(\<forall>i<DIM('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)"
+  using euclidean_all_zero_iff [of x, folded image_basis]
+  unfolding ball_simps by (simp add: Ball_def inner_commute)
+
+lemma (in euclidean_space) basis_zero [simp]:
+  "DIM('a) \<le> i \<Longrightarrow> basis i = 0"
+  using basis_finite by auto
+
+lemma (in euclidean_space) DIM_positive [intro]: "0 < DIM('a)"
+  unfolding dimension_def by (simp add: card_gt_0_iff)
+
+lemma (in euclidean_space) basis_inj [simp, intro]: "inj_on basis {..<DIM('a)}"
+  by (simp add: inj_on_iff_eq_card image_basis dimension_def [symmetric])
+
+lemma (in euclidean_space) basis_in_Basis [simp]:
+  "basis i \<in> Basis \<longleftrightarrow> i < DIM('a)"
+  by (cases "i < DIM('a)", simp add: image_basis [symmetric], simp)
+
+lemma (in euclidean_space) Basis_elim:
+  assumes "u \<in> Basis" obtains i where "i < DIM('a)" and "u = basis i"
+  using assms unfolding image_basis [symmetric] by fast
+
+lemma (in euclidean_space) basis_orthonormal:
+    "\<forall>i<DIM('a). \<forall>j<DIM('a).
+      inner (basis i) (basis j) = (if i = j then 1 else 0)"
+  apply clarify
+  apply (simp add: inner_Basis)
+  apply (simp add: basis_inj [unfolded inj_on_def])
+  done
+
 lemma (in euclidean_space) dot_basis:
   "inner (basis i) (basis j) = (if i = j \<and> i < DIM('a) then 1 else 0)"
 proof (cases "(i < DIM('a) \<and> j < DIM('a))")
@@ -161,6 +214,9 @@
 begin
 
 definition
+  "Basis = {1::real}"
+
+definition
   "dimension (t::real itself) = 1"
 
 definition [simp]:
@@ -170,42 +226,44 @@
   by (rule dimension_real_def)
 
 instance
-  by default simp+
+  by default (auto simp add: Basis_real_def)
 
 end
 
 subsubsection {* Type @{typ complex} *}
 
+ (* TODO: move these to Complex.thy/Inner_Product.thy *)
+
+lemma norm_ii [simp]: "norm ii = 1"
+  unfolding i_def by simp
+
+lemma complex_inner_1 [simp]: "inner 1 x = Re x"
+  unfolding inner_complex_def by simp
+
+lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
+  unfolding inner_complex_def by simp
+
+lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
+  unfolding inner_complex_def by simp
+
+lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
+  unfolding inner_complex_def by simp
+
 instantiation complex :: euclidean_space
 begin
 
+definition Basis_complex_def:
+  "Basis = {1, ii}"
+
 definition
   "dimension (t::complex itself) = 2"
 
 definition
   "basis i = (if i = 0 then 1 else if i = 1 then ii else 0)"
 
-lemma all_less_Suc: "(\<forall>i<Suc n. P i) \<longleftrightarrow> (\<forall>i<n. P i) \<and> P n"
-  by (auto simp add: less_Suc_eq)
-
-instance proof
-  show "0 < DIM(complex)"
-    unfolding dimension_complex_def by simp
-next
-  fix i :: nat
-  assume "DIM(complex) \<le> i" thus "basis i = (0::complex)"
-    unfolding dimension_complex_def basis_complex_def by simp
-next
-  show "\<forall>i<DIM(complex). \<forall>j<DIM(complex).
-    inner (basis i::complex) (basis j) = (if i = j then 1 else 0)"
-    unfolding dimension_complex_def basis_complex_def inner_complex_def
-    by (simp add: numeral_2_eq_2 all_less_Suc)
-next
-  fix x :: complex
-  show "(\<forall>i<DIM(complex). inner (basis i) x = 0) \<longleftrightarrow> x = 0"
-    unfolding dimension_complex_def basis_complex_def inner_complex_def
-    by (simp add: numeral_2_eq_2 all_less_Suc complex_eq_iff)
-qed
+instance
+  by default (auto simp add: Basis_complex_def dimension_complex_def
+    basis_complex_def intro: complex_eqI split: split_if_asm)
 
 end
 
@@ -214,40 +272,50 @@
 
 subsubsection {* Type @{typ "'a \<times> 'b"} *}
 
+lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
+  by auto (* TODO: move elsewhere *)
+
 instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
 begin
 
 definition
+  "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"
+
+definition
   "dimension (t::('a \<times> 'b) itself) = DIM('a) + DIM('b)"
 
 definition
   "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
 
-lemma all_less_sum:
-  fixes m n :: nat
-  shows "(\<forall>i<(m + n). P i) \<longleftrightarrow> (\<forall>i<m. P i) \<and> (\<forall>i<n. P (m + i))"
-  by (induct n, simp, simp add: all_less_Suc)
-
 instance proof
-  show "0 < DIM('a \<times> 'b)"
-    unfolding dimension_prod_def by (intro add_pos_pos DIM_positive)
+  show "(Basis :: ('a \<times> 'b) set) \<noteq> {}"
+    unfolding Basis_prod_def by simp
 next
-  fix i :: nat
-  assume "DIM('a \<times> 'b) \<le> i" thus "basis i = (0::'a \<times> 'b)"
-    unfolding dimension_prod_def basis_prod_def zero_prod_def
-    by simp
+  show "finite (Basis :: ('a \<times> 'b) set)"
+    unfolding Basis_prod_def by simp
 next
-  show "\<forall>i<DIM('a \<times> 'b). \<forall>j<DIM('a \<times> 'b).
-    inner (basis i::'a \<times> 'b) (basis j) = (if i = j then 1 else 0)"
-    unfolding dimension_prod_def basis_prod_def inner_prod_def
-    unfolding all_less_sum prod_eq_iff
-    by (simp add: basis_orthonormal)
+  fix u v :: "'a \<times> 'b"
+  assume "u \<in> Basis" and "v \<in> Basis"
+  thus "inner u v = (if u = v then 1 else 0)"
+    unfolding Basis_prod_def inner_prod_def
+    by (auto simp add: inner_Basis split: split_if_asm)
 next
   fix x :: "'a \<times> 'b"
-  show "(\<forall>i<DIM('a \<times> 'b). inner (basis i) x = 0) \<longleftrightarrow> x = 0"
-    unfolding dimension_prod_def basis_prod_def inner_prod_def
-    unfolding all_less_sum prod_eq_iff
-    by (simp add: euclidean_all_zero)
+  show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
+    unfolding Basis_prod_def ball_Un ball_simps
+    by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
+next
+  show "DIM('a \<times> 'b) = card (Basis :: ('a \<times> 'b) set)"
+    unfolding dimension_prod_def Basis_prod_def
+    by (simp add: card_Un_disjoint disjoint_iff
+      card_image inj_on_def dimension_def)
+next
+  show "basis ` {..<DIM('a \<times> 'b)} = (Basis :: ('a \<times> 'b) set)"
+    by (auto simp add: Basis_prod_def dimension_prod_def basis_prod_def
+      image_def elim!: Basis_elim)
+next
+  show "basis ` {DIM('a \<times> 'b)..} = {0::('a \<times> 'b)}"
+    by (auto simp add: dimension_prod_def basis_prod_def prod_eq_iff image_def)
 qed
 
 end
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Fri Aug 12 07:13:12 2011 -0700
@@ -1146,9 +1146,6 @@
   shows "suminf f = (\<Sum>N<n. f N)"
   using sums_finite[OF assms, THEN sums_unique] by simp
 
-lemma suminf_ereal_0[simp]: "(\<Sum>i. 0) = (0::'a::{comm_monoid_add,t2_space})"
-  using suminf_finite[of 0 "\<lambda>x. 0"] by simp
-
 lemma suminf_upper:
   fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
   shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Fri Aug 12 07:13:12 2011 -0700
@@ -41,9 +41,6 @@
 end
 *}
 
-lemma stupid_ext: "(\<forall>x. f x = g x) \<longleftrightarrow> (f = g)"
-  by auto
-
 lemma vec_eq_iff: "(x = y) \<longleftrightarrow> (\<forall>i. x$i = y$i)"
   by (simp add: vec_nth_inject [symmetric] fun_eq_iff)
 
@@ -445,8 +442,44 @@
 
 end
 
+
 subsection {* Euclidean space *}
 
+text {* Vectors pointing along a single axis. *}
+
+definition "axis k x = (\<chi> i. if i = k then x else 0)"
+
+lemma axis_nth [simp]: "axis i x $ i = x"
+  unfolding axis_def by simp
+
+lemma axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0"
+  unfolding axis_def vec_eq_iff by auto
+
+lemma inner_axis_axis:
+  "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)"
+  unfolding inner_vec_def
+  apply (cases "i = j")
+  apply clarsimp
+  apply (subst setsum_diff1' [where a=j], simp_all)
+  apply (rule setsum_0', simp add: axis_def)
+  apply (rule setsum_0', simp add: axis_def)
+  done
+
+lemma setsum_single:
+  assumes "finite A" and "k \<in> A" and "f k = y"
+  assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0"
+  shows "(\<Sum>i\<in>A. f i) = y"
+  apply (subst setsum_diff1' [OF assms(1,2)])
+  apply (simp add: setsum_0' assms(3,4))
+  done
+
+lemma inner_axis: "inner x (axis i y) = inner (x $ i) y"
+  unfolding inner_vec_def
+  apply (rule_tac k=i in setsum_single)
+  apply simp_all
+  apply (simp add: axis_def)
+  done
+
 text {* A bijection between @{text "'n::finite"} and @{text "{..<CARD('n)}"} *}
 
 definition vec_bij_nat :: "nat \<Rightarrow> ('n::finite)" where
@@ -485,16 +518,18 @@
 instantiation vec :: (euclidean_space, finite) euclidean_space
 begin
 
+definition "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"
+
 definition "dimension (t :: ('a ^ 'b) itself) = CARD('b) * DIM('a)"
 
-definition "(basis i::'a^'b) =
+definition "basis i =
   (if i < (CARD('b) * DIM('a))
-  then (\<chi> j::'b. if j = \<pi>(i div DIM('a)) then basis (i mod DIM('a)) else 0)
+  then axis (\<pi>(i div DIM('a))) (basis (i mod DIM('a)))
   else 0)"
 
 lemma basis_eq:
   assumes "i < CARD('b)" and "j < DIM('a)"
-  shows "basis (j + i * DIM('a)) = (\<chi> k. if k = \<pi> i then basis j else 0)"
+  shows "basis (j + i * DIM('a)) = axis (\<pi> i) (basis j)"
 proof -
   have "j + i * DIM('a) <  DIM('a) * (i + 1)" using assms by (auto simp: field_simps)
   also have "\<dots> \<le> DIM('a) * CARD('b)" using assms unfolding mult_le_cancel1 by auto
@@ -506,7 +541,7 @@
   assumes "j < DIM('a)"
   shows "basis (j + \<pi>' i * DIM('a)) $ k = (if k = i then basis j else 0)"
   apply (subst basis_eq)
-  using pi'_range assms by simp_all
+  using pi'_range assms by (simp_all add: axis_def)
 
 lemma split_times_into_modulo[consumes 1]:
   fixes k :: nat
@@ -523,20 +558,6 @@
   finally show "k div B < A" by auto
 qed simp
 
-lemma split_CARD_DIM[consumes 1]:
-  fixes k :: nat
-  assumes k: "k < CARD('b) * DIM('a)"
-  obtains i and j::'b where "i < DIM('a)" "k = i + \<pi>' j * DIM('a)"
-proof -
-  from split_times_into_modulo[OF k] guess i j . note ij = this
-  show thesis
-  proof
-    show "j < DIM('a)" using ij by simp
-    show "k = j + \<pi>' (\<pi> i :: 'b) * DIM('a)"
-      using ij by simp
-  qed
-qed
-
 lemma linear_less_than_times:
   fixes i j A B :: nat assumes "i < B" "j < A"
   shows "j + i * A < B * A"
@@ -549,64 +570,43 @@
 lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
   by (rule dimension_vec_def)
 
-lemma all_less_DIM_cart:
-  fixes m n :: nat
-  shows "(\<forall>i<DIM('a^'b). P i) \<longleftrightarrow> (\<forall>x::'b. \<forall>i<DIM('a). P (i + \<pi>' x * DIM('a)))"
-unfolding DIM_cart
-apply safe
-apply (drule spec, erule mp, erule linear_less_than_times [OF pi'_range])
-apply (erule split_CARD_DIM, simp)
-done
-
-lemma eq_pi_iff:
-  fixes x :: "'c::finite"
-  shows "i < CARD('c::finite) \<Longrightarrow> x = \<pi> i \<longleftrightarrow> \<pi>' x = i"
-  by auto
-
-lemma all_less_mult:
-  fixes m n :: nat
-  shows "(\<forall>i<(m * n). P i) \<longleftrightarrow> (\<forall>i<m. \<forall>j<n. P (j + i * n))"
-apply safe
-apply (drule spec, erule mp, erule (1) linear_less_than_times)
-apply (erule split_times_into_modulo, simp)
-done
-
-lemma inner_if:
-  "inner (if a then x else y) z = (if a then inner x z else inner y z)"
-  "inner x (if a then y else z) = (if a then inner x y else inner x z)"
-  by simp_all
-
 instance proof
-  show "0 < DIM('a ^ 'b)"
-    unfolding dimension_vec_def
-    by (intro mult_pos_pos zero_less_card_finite DIM_positive)
+  show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
+    unfolding Basis_vec_def by simp
+next
+  show "finite (Basis :: ('a ^ 'b) set)"
+    unfolding Basis_vec_def by simp
 next
-  fix i :: nat
-  assume "DIM('a ^ 'b) \<le> i" thus "basis i = (0::'a^'b)"
-    unfolding dimension_vec_def basis_vec_def
-    by simp
+  fix u v :: "'a ^ 'b"
+  assume "u \<in> Basis" and "v \<in> Basis"
+  thus "inner u v = (if u = v then 1 else 0)"
+    unfolding Basis_vec_def
+    by (auto simp add: inner_axis_axis axis_eq_axis inner_Basis)
 next
-  show "\<forall>i<DIM('a ^ 'b). \<forall>j<DIM('a ^ 'b).
-    inner (basis i :: 'a ^ 'b) (basis j) = (if i = j then 1 else 0)"
-    apply (simp add: inner_vec_def)
-    apply safe
-    apply (erule split_CARD_DIM, simp add: basis_eq_pi')
-    apply (simp add: inner_if setsum_delta cong: if_cong)
-    apply (simp add: basis_orthonormal)
-    apply (elim split_CARD_DIM, simp add: basis_eq_pi')
-    apply (simp add: inner_if setsum_delta cong: if_cong)
-    apply (clarsimp simp add: basis_orthonormal)
+  fix x :: "'a ^ 'b"
+  show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
+    unfolding Basis_vec_def
+    by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
+next
+  show "DIM('a ^ 'b) = card (Basis :: ('a ^ 'b) set)"
+    unfolding Basis_vec_def dimension_vec_def dimension_def
+    by (simp add: card_UN_disjoint [unfolded disjoint_iff]
+      axis_eq_axis nonzero_Basis)
+next
+  show "basis ` {..<DIM('a ^ 'b)} = (Basis :: ('a ^ 'b) set)"
+    unfolding Basis_vec_def
+    apply auto
+    apply (erule split_times_into_modulo)
+    apply (simp add: basis_eq axis_eq_axis)
+    apply (erule Basis_elim)
+    apply (simp add: image_def basis_vec_def axis_eq_axis)
+    apply (rule rev_bexI, simp)
+    apply (erule linear_less_than_times [OF pi'_range])
+    apply simp
     done
 next
-  fix x :: "'a ^ 'b"
-  show "(\<forall>i<DIM('a ^ 'b). inner (basis i) x = 0) \<longleftrightarrow> x = 0"
-    unfolding all_less_DIM_cart
-    unfolding inner_vec_def
-    apply (simp add: basis_eq_pi')
-    apply (simp add: inner_if setsum_delta cong: if_cong)
-    apply (simp add: euclidean_all_zero)
-    apply (simp add: vec_eq_iff)
-    done
+  show "basis ` {DIM('a ^ 'b)..} = {0::'a ^ 'b}"
+    by (auto simp add: image_def basis_vec_def)
 qed
 
 end
--- a/src/HOL/Multivariate_Analysis/Integration.thy	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Integration.thy	Fri Aug 12 07:13:12 2011 -0700
@@ -23,8 +23,6 @@
   by(subst(asm) real_arch_inv)
 subsection {* Sundries *}
 
-(*declare basis_component[simp]*)
-
 lemma conjunctD2: assumes "a \<and> b" shows a b using assms by auto
 lemma conjunctD3: assumes "a \<and> b \<and> c" shows a b c using assms by auto
 lemma conjunctD4: assumes "a \<and> b \<and> c \<and> d" shows a b c d using assms by auto
@@ -142,7 +140,7 @@
       let ?z = "x - (e/2) *\<^sub>R basis k" assume as:"x$$k = a$$k" have "ball ?z (e / 2) \<inter> i = {}" apply(rule ccontr) unfolding ex_in_conv[THEN sym] proof(erule exE)
         fix y assume "y \<in> ball ?z (e / 2) \<inter> i" hence "dist ?z y < e/2" and yi:"y\<in>i" by auto
         hence "\<bar>(?z - y) $$ k\<bar> < e/2" using component_le_norm[of "?z - y" k] unfolding dist_norm by auto
-        hence "y$$k < a$$k" using e[THEN conjunct1] k by(auto simp add:field_simps basis_component as)
+        hence "y$$k < a$$k" using e[THEN conjunct1] k by(auto simp add:field_simps as)
         hence "y \<notin> i" unfolding ab mem_interval not_all apply(rule_tac x=k in exI) using k by auto thus False using yi by auto qed
       moreover have "ball ?z (e/2) \<subseteq> s \<inter> (\<Union>insert i f)" apply(rule order_trans[OF _ e[THEN conjunct2, unfolded lem1]]) proof
         fix y assume as:"y\<in> ball ?z (e/2)" have "norm (x - y) \<le> \<bar>e\<bar> / 2 + norm (x - y - (e / 2) *\<^sub>R basis k)"
@@ -417,10 +415,6 @@
   fix k assume k:"k \<in> p1 \<union> p2"  show "k \<subseteq> s1 \<union> s2" using k d1(2) d2(2) by auto
   show "k \<noteq> {}" using k d1(3) d2(3) by auto show "\<exists>a b. k = {a..b}" using k d1(4) d2(4) by auto qed
 
-(* move *)
-lemma Eucl_nth_inverse[simp]: fixes x::"'a::euclidean_space" shows "(\<chi>\<chi> i. x $$ i) = x"
-  apply(subst euclidean_eq) by auto
-
 lemma partial_division_extend_1:
   assumes "{c..d} \<subseteq> {a..b::'a::ordered_euclidean_space}" "{c..d} \<noteq> {}"
   obtains p where "p division_of {a..b}" "{c..d} \<in> p"
@@ -737,7 +731,7 @@
   "(s tagged_division_of i) \<equiv>
         (s tagged_partial_division_of i) \<and> (\<Union>{k. \<exists>x. (x,k) \<in> s} = i)"
 
-lemma tagged_division_of_finite[dest]: "s tagged_division_of i \<Longrightarrow> finite s"
+lemma tagged_division_of_finite: "s tagged_division_of i \<Longrightarrow> finite s"
   unfolding tagged_division_of_def tagged_partial_division_of_def by auto
 
 lemma tagged_division_of:
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Fri Aug 12 07:13:12 2011 -0700
@@ -1581,12 +1581,6 @@
 
 subsection{* Euclidean Spaces as Typeclass*}
 
-lemma (in euclidean_space) basis_inj[simp, intro]: "inj_on basis {..<DIM('a)}"
-  by (rule inj_onI, rule ccontr, cut_tac i=x and j=y in dot_basis, simp)
-
-lemma (in euclidean_space) basis_finite: "basis ` {DIM('a)..} = {0}"
-  by (auto intro: image_eqI [where x="DIM('a)"])
-
 lemma independent_eq_inj_on:
   fixes D :: nat and f :: "nat \<Rightarrow> 'c::real_vector" assumes *: "inj_on f {..<D}"
   shows "independent (f ` {..<D}) \<longleftrightarrow> (\<forall>a u. a < D \<longrightarrow> (\<Sum>i\<in>{..<D}-{a}. u (f i) *\<^sub>R f i) \<noteq> f a)"
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Thu Aug 11 20:32:44 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Fri Aug 12 07:13:12 2011 -0700
@@ -479,7 +479,7 @@
   { fix e :: real assume "0 < e"
     def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))"
     from `0 < e` have "y \<noteq> x"
-      unfolding y_def by (simp add: sgn_zero_iff basis_eq_0_iff DIM_positive)
+      unfolding y_def by (simp add: sgn_zero_iff DIM_positive)
     from `0 < e` have "dist y x < e"
       unfolding y_def by (simp add: dist_norm norm_sgn)
     from `y \<noteq> x` and `dist y x < e`
@@ -5646,7 +5646,7 @@
 
 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)
+  unfolding subspace_def by(auto simp add: euclidean_simps) (* FIXME: duplicate rewrite rule *)
 
 lemma closed_substandard:
  "closed {x::'a::euclidean_space. \<forall>i<DIM('a). P i --> x$$i = 0}" (is "closed ?A")
@@ -5674,7 +5674,7 @@
   let ?D = "{..<DIM('a)}"
   let ?B = "(basis::nat => 'a) ` d"
   let ?bas = "basis::nat \<Rightarrow> 'a"
-  have "?B \<subseteq> ?A" by(auto simp add:basis_component)
+  have "?B \<subseteq> ?A" by auto
   moreover
   { fix x::"'a" assume "x\<in>?A"
     hence "finite d" "x\<in>?A" using assms by(auto intro:finite_subset)
@@ -5690,7 +5690,7 @@
       have y:"x = y + (x$$k) *\<^sub>R basis k" unfolding y_def by auto
       { fix i assume i':"i \<notin> F"
         hence "y $$ i = 0" unfolding y_def 
-          using *[THEN spec[where x=i]] by(auto simp add: euclidean_simps basis_component) }
+          using *[THEN spec[where x=i]] by(auto simp add: euclidean_simps) }
       hence "y \<in> span (basis ` F)" using insert(3) by auto
       hence "y \<in> span (basis ` (insert k F))"
         using span_mono[of "?bas ` F" "?bas ` (insert k F)"]
@@ -6025,7 +6025,7 @@
   have lima:"((fst \<circ> (h \<circ> r)) ---> a) sequentially"
    and limb:"((snd \<circ> (h \<circ> r)) ---> b) sequentially"
     using lr
-    unfolding o_def a_def b_def by (simp_all add: tendsto_intros)
+    unfolding o_def a_def b_def by (rule tendsto_intros)+
 
   { fix n::nat
     have *:"\<And>fx fy (x::'a) y. dist fx fy \<le> dist x y \<Longrightarrow> \<not> (dist (fx - fy) (a - b) < dist a b - dist x y)" unfolding dist_norm by norm