author huffman Thu Aug 11 13:05:56 2011 -0700 (2011-08-11) changeset 44166 d12d89a66742 parent 44165 d26a45f3c835 child 44167 e81d676d598e
modify euclidean_space class to include basis set
```     1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 09:11:15 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Thu Aug 11 13:05:56 2011 -0700
1.3 @@ -467,7 +467,7 @@
1.4  text {* some lemmas to map between Eucl and Cart *}
1.5  lemma basis_real_n[simp]:"(basis (\<pi>' i)::real^'a) = cart_basis i"
1.6    unfolding basis_vec_def using pi'_range[where 'n='a]
1.7 -  by (auto simp: vec_eq_iff)
1.8 +  by (auto simp: vec_eq_iff axis_def)
1.9
1.10  subsection {* Orthogonality on cartesian products *}
1.11
```
```     2.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 11 09:11:15 2011 -0700
2.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Thu Aug 11 13:05:56 2011 -0700
2.3 @@ -15,22 +15,75 @@
2.4  subsection {* Type class of Euclidean spaces *}
2.5
2.6  class euclidean_space = real_inner +
2.7 +  fixes Basis :: "'a set"
2.8 +  assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
2.9 +  assumes finite_Basis [simp]: "finite Basis"
2.10 +  assumes inner_Basis:
2.11 +    "\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)"
2.12 +  assumes euclidean_all_zero_iff:
2.13 +    "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
2.14 +
2.15 +  -- "FIXME: make this a separate definition"
2.16    fixes dimension :: "'a itself \<Rightarrow> nat"
2.17 +  assumes dimension_def: "dimension TYPE('a) = card Basis"
2.18 +
2.19 +  -- "FIXME: eventually basis function can be removed"
2.20    fixes basis :: "nat \<Rightarrow> 'a"
2.21 -  assumes DIM_positive [intro]:
2.22 -    "0 < dimension TYPE('a)"
2.23 -  assumes basis_zero [simp]:
2.24 -    "dimension TYPE('a) \<le> i \<Longrightarrow> basis i = 0"
2.25 -  assumes basis_orthonormal:
2.26 -    "\<forall>i<dimension TYPE('a). \<forall>j<dimension TYPE('a).
2.27 -      inner (basis i) (basis j) = (if i = j then 1 else 0)"
2.28 -  assumes euclidean_all_zero:
2.29 -    "(\<forall>i<dimension TYPE('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)"
2.30 +  assumes image_basis: "basis ` {..<dimension TYPE('a)} = Basis"
2.31 +  assumes basis_finite: "basis ` {dimension TYPE('a)..} = {0}"
2.32
2.33  syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
2.34
2.35  translations "DIM('t)" == "CONST dimension (TYPE('t))"
2.36
2.37 +lemma (in euclidean_space) norm_Basis: "u \<in> Basis \<Longrightarrow> norm u = 1"
2.38 +  unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)
2.39 +
2.40 +lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
2.41 +  unfolding sgn_div_norm by (simp add: norm_Basis scaleR_one)
2.42 +
2.43 +lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
2.44 +proof
2.45 +  assume "0 \<in> Basis" thus "False"
2.46 +    using inner_Basis [of 0 0] by simp
2.47 +qed
2.48 +
2.49 +lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0"
2.50 +  by clarsimp
2.51 +
2.52 +text {* Lemmas related to @{text basis} function. *}
2.53 +
2.54 +lemma (in euclidean_space) euclidean_all_zero:
2.55 +  "(\<forall>i<DIM('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)"
2.56 +  using euclidean_all_zero_iff [of x, folded image_basis]
2.57 +  unfolding ball_simps by (simp add: Ball_def inner_commute)
2.58 +
2.59 +lemma (in euclidean_space) basis_zero [simp]:
2.60 +  "DIM('a) \<le> i \<Longrightarrow> basis i = 0"
2.61 +  using basis_finite by auto
2.62 +
2.63 +lemma (in euclidean_space) DIM_positive [intro]: "0 < DIM('a)"
2.64 +  unfolding dimension_def by (simp add: card_gt_0_iff)
2.65 +
2.66 +lemma (in euclidean_space) basis_inj [simp, intro]: "inj_on basis {..<DIM('a)}"
2.67 +  by (simp add: inj_on_iff_eq_card image_basis dimension_def [symmetric])
2.68 +
2.69 +lemma (in euclidean_space) basis_in_Basis [simp]:
2.70 +  "basis i \<in> Basis \<longleftrightarrow> i < DIM('a)"
2.71 +  by (cases "i < DIM('a)", simp add: image_basis [symmetric], simp)
2.72 +
2.73 +lemma (in euclidean_space) Basis_elim:
2.74 +  assumes "u \<in> Basis" obtains i where "i < DIM('a)" and "u = basis i"
2.75 +  using assms unfolding image_basis [symmetric] by fast
2.76 +
2.77 +lemma (in euclidean_space) basis_orthonormal:
2.78 +    "\<forall>i<DIM('a). \<forall>j<DIM('a).
2.79 +      inner (basis i) (basis j) = (if i = j then 1 else 0)"
2.80 +  apply clarify
2.81 +  apply (simp add: inner_Basis)
2.82 +  apply (simp add: basis_inj [unfolded inj_on_def])
2.83 +  done
2.84 +
2.85  lemma (in euclidean_space) dot_basis:
2.86    "inner (basis i) (basis j) = (if i = j \<and> i < DIM('a) then 1 else 0)"
2.87  proof (cases "(i < DIM('a) \<and> j < DIM('a))")
2.88 @@ -161,6 +214,9 @@
2.89  begin
2.90
2.91  definition
2.92 +  "Basis = {1::real}"
2.93 +
2.94 +definition
2.95    "dimension (t::real itself) = 1"
2.96
2.97  definition [simp]:
2.98 @@ -170,42 +226,44 @@
2.99    by (rule dimension_real_def)
2.100
2.101  instance
2.102 -  by default simp+
2.103 +  by default (auto simp add: Basis_real_def)
2.104
2.105  end
2.106
2.107  subsubsection {* Type @{typ complex} *}
2.108
2.109 + (* TODO: move these to Complex.thy/Inner_Product.thy *)
2.110 +
2.111 +lemma norm_ii [simp]: "norm ii = 1"
2.112 +  unfolding i_def by simp
2.113 +
2.114 +lemma complex_inner_1 [simp]: "inner 1 x = Re x"
2.115 +  unfolding inner_complex_def by simp
2.116 +
2.117 +lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
2.118 +  unfolding inner_complex_def by simp
2.119 +
2.120 +lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
2.121 +  unfolding inner_complex_def by simp
2.122 +
2.123 +lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
2.124 +  unfolding inner_complex_def by simp
2.125 +
2.126  instantiation complex :: euclidean_space
2.127  begin
2.128
2.129 +definition Basis_complex_def:
2.130 +  "Basis = {1, ii}"
2.131 +
2.132  definition
2.133    "dimension (t::complex itself) = 2"
2.134
2.135  definition
2.136    "basis i = (if i = 0 then 1 else if i = 1 then ii else 0)"
2.137
2.138 -lemma all_less_Suc: "(\<forall>i<Suc n. P i) \<longleftrightarrow> (\<forall>i<n. P i) \<and> P n"
2.139 -  by (auto simp add: less_Suc_eq)
2.140 -
2.141 -instance proof
2.142 -  show "0 < DIM(complex)"
2.143 -    unfolding dimension_complex_def by simp
2.144 -next
2.145 -  fix i :: nat
2.146 -  assume "DIM(complex) \<le> i" thus "basis i = (0::complex)"
2.147 -    unfolding dimension_complex_def basis_complex_def by simp
2.148 -next
2.149 -  show "\<forall>i<DIM(complex). \<forall>j<DIM(complex).
2.150 -    inner (basis i::complex) (basis j) = (if i = j then 1 else 0)"
2.151 -    unfolding dimension_complex_def basis_complex_def inner_complex_def
2.152 -    by (simp add: numeral_2_eq_2 all_less_Suc)
2.153 -next
2.154 -  fix x :: complex
2.155 -  show "(\<forall>i<DIM(complex). inner (basis i) x = 0) \<longleftrightarrow> x = 0"
2.156 -    unfolding dimension_complex_def basis_complex_def inner_complex_def
2.157 -    by (simp add: numeral_2_eq_2 all_less_Suc complex_eq_iff)
2.158 -qed
2.159 +instance
2.160 +  by default (auto simp add: Basis_complex_def dimension_complex_def
2.161 +    basis_complex_def intro: complex_eqI split: split_if_asm)
2.162
2.163  end
2.164
2.165 @@ -214,40 +272,50 @@
2.166
2.167  subsubsection {* Type @{typ "'a \<times> 'b"} *}
2.168
2.169 +lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
2.170 +  by auto (* TODO: move elsewhere *)
2.171 +
2.172  instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
2.173  begin
2.174
2.175  definition
2.176 +  "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"
2.177 +
2.178 +definition
2.179    "dimension (t::('a \<times> 'b) itself) = DIM('a) + DIM('b)"
2.180
2.181  definition
2.182    "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
2.183
2.184 -lemma all_less_sum:
2.185 -  fixes m n :: nat
2.186 -  shows "(\<forall>i<(m + n). P i) \<longleftrightarrow> (\<forall>i<m. P i) \<and> (\<forall>i<n. P (m + i))"
2.187 -  by (induct n, simp, simp add: all_less_Suc)
2.188 -
2.189  instance proof
2.190 -  show "0 < DIM('a \<times> 'b)"
2.191 -    unfolding dimension_prod_def by (intro add_pos_pos DIM_positive)
2.192 +  show "(Basis :: ('a \<times> 'b) set) \<noteq> {}"
2.193 +    unfolding Basis_prod_def by simp
2.194  next
2.195 -  fix i :: nat
2.196 -  assume "DIM('a \<times> 'b) \<le> i" thus "basis i = (0::'a \<times> 'b)"
2.197 -    unfolding dimension_prod_def basis_prod_def zero_prod_def
2.198 -    by simp
2.199 +  show "finite (Basis :: ('a \<times> 'b) set)"
2.200 +    unfolding Basis_prod_def by simp
2.201  next
2.202 -  show "\<forall>i<DIM('a \<times> 'b). \<forall>j<DIM('a \<times> 'b).
2.203 -    inner (basis i::'a \<times> 'b) (basis j) = (if i = j then 1 else 0)"
2.204 -    unfolding dimension_prod_def basis_prod_def inner_prod_def
2.205 -    unfolding all_less_sum prod_eq_iff
2.206 -    by (simp add: basis_orthonormal)
2.207 +  fix u v :: "'a \<times> 'b"
2.208 +  assume "u \<in> Basis" and "v \<in> Basis"
2.209 +  thus "inner u v = (if u = v then 1 else 0)"
2.210 +    unfolding Basis_prod_def inner_prod_def
2.211 +    by (auto simp add: inner_Basis split: split_if_asm)
2.212  next
2.213    fix x :: "'a \<times> 'b"
2.214 -  show "(\<forall>i<DIM('a \<times> 'b). inner (basis i) x = 0) \<longleftrightarrow> x = 0"
2.215 -    unfolding dimension_prod_def basis_prod_def inner_prod_def
2.216 -    unfolding all_less_sum prod_eq_iff
2.217 -    by (simp add: euclidean_all_zero)
2.218 +  show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
2.219 +    unfolding Basis_prod_def ball_Un ball_simps
2.220 +    by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
2.221 +next
2.222 +  show "DIM('a \<times> 'b) = card (Basis :: ('a \<times> 'b) set)"
2.223 +    unfolding dimension_prod_def Basis_prod_def
2.224 +    by (simp add: card_Un_disjoint disjoint_iff
2.225 +      card_image inj_on_def dimension_def)
2.226 +next
2.227 +  show "basis ` {..<DIM('a \<times> 'b)} = (Basis :: ('a \<times> 'b) set)"
2.228 +    by (auto simp add: Basis_prod_def dimension_prod_def basis_prod_def
2.229 +      image_def elim!: Basis_elim)
2.230 +next
2.231 +  show "basis ` {DIM('a \<times> 'b)..} = {0::('a \<times> 'b)}"
2.232 +    by (auto simp add: dimension_prod_def basis_prod_def prod_eq_iff image_def)
2.233  qed
2.234
2.235  end
```
```     3.1 --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 11 09:11:15 2011 -0700
3.2 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Thu Aug 11 13:05:56 2011 -0700
3.3 @@ -442,8 +442,44 @@
3.4
3.5  end
3.6
3.7 +
3.8  subsection {* Euclidean space *}
3.9
3.10 +text {* Vectors pointing along a single axis. *}
3.11 +
3.12 +definition "axis k x = (\<chi> i. if i = k then x else 0)"
3.13 +
3.14 +lemma axis_nth [simp]: "axis i x \$ i = x"
3.15 +  unfolding axis_def by simp
3.16 +
3.17 +lemma axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0"
3.18 +  unfolding axis_def vec_eq_iff by auto
3.19 +
3.20 +lemma inner_axis_axis:
3.21 +  "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)"
3.22 +  unfolding inner_vec_def
3.23 +  apply (cases "i = j")
3.24 +  apply clarsimp
3.25 +  apply (subst setsum_diff1' [where a=j], simp_all)
3.26 +  apply (rule setsum_0', simp add: axis_def)
3.27 +  apply (rule setsum_0', simp add: axis_def)
3.28 +  done
3.29 +
3.30 +lemma setsum_single:
3.31 +  assumes "finite A" and "k \<in> A" and "f k = y"
3.32 +  assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0"
3.33 +  shows "(\<Sum>i\<in>A. f i) = y"
3.34 +  apply (subst setsum_diff1' [OF assms(1,2)])
3.35 +  apply (simp add: setsum_0' assms(3,4))
3.36 +  done
3.37 +
3.38 +lemma inner_axis: "inner x (axis i y) = inner (x \$ i) y"
3.39 +  unfolding inner_vec_def
3.40 +  apply (rule_tac k=i in setsum_single)
3.41 +  apply simp_all
3.42 +  apply (simp add: axis_def)
3.43 +  done
3.44 +
3.45  text {* A bijection between @{text "'n::finite"} and @{text "{..<CARD('n)}"} *}
3.46
3.47  definition vec_bij_nat :: "nat \<Rightarrow> ('n::finite)" where
3.48 @@ -482,16 +518,18 @@
3.49  instantiation vec :: (euclidean_space, finite) euclidean_space
3.50  begin
3.51
3.52 +definition "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"
3.53 +
3.54  definition "dimension (t :: ('a ^ 'b) itself) = CARD('b) * DIM('a)"
3.55
3.56 -definition "(basis i::'a^'b) =
3.57 +definition "basis i =
3.58    (if i < (CARD('b) * DIM('a))
3.59 -  then (\<chi> j::'b. if j = \<pi>(i div DIM('a)) then basis (i mod DIM('a)) else 0)
3.60 +  then axis (\<pi>(i div DIM('a))) (basis (i mod DIM('a)))
3.61    else 0)"
3.62
3.63  lemma basis_eq:
3.64    assumes "i < CARD('b)" and "j < DIM('a)"
3.65 -  shows "basis (j + i * DIM('a)) = (\<chi> k. if k = \<pi> i then basis j else 0)"
3.66 +  shows "basis (j + i * DIM('a)) = axis (\<pi> i) (basis j)"
3.67  proof -
3.68    have "j + i * DIM('a) <  DIM('a) * (i + 1)" using assms by (auto simp: field_simps)
3.69    also have "\<dots> \<le> DIM('a) * CARD('b)" using assms unfolding mult_le_cancel1 by auto
3.70 @@ -503,7 +541,7 @@
3.71    assumes "j < DIM('a)"
3.72    shows "basis (j + \<pi>' i * DIM('a)) \$ k = (if k = i then basis j else 0)"
3.73    apply (subst basis_eq)
3.74 -  using pi'_range assms by simp_all
3.75 +  using pi'_range assms by (simp_all add: axis_def)
3.76
3.77  lemma split_times_into_modulo[consumes 1]:
3.78    fixes k :: nat
3.79 @@ -520,20 +558,6 @@
3.80    finally show "k div B < A" by auto
3.81  qed simp
3.82
3.83 -lemma split_CARD_DIM[consumes 1]:
3.84 -  fixes k :: nat
3.85 -  assumes k: "k < CARD('b) * DIM('a)"
3.86 -  obtains i and j::'b where "i < DIM('a)" "k = i + \<pi>' j * DIM('a)"
3.87 -proof -
3.88 -  from split_times_into_modulo[OF k] guess i j . note ij = this
3.89 -  show thesis
3.90 -  proof
3.91 -    show "j < DIM('a)" using ij by simp
3.92 -    show "k = j + \<pi>' (\<pi> i :: 'b) * DIM('a)"
3.93 -      using ij by simp
3.94 -  qed
3.95 -qed
3.96 -
3.97  lemma linear_less_than_times:
3.98    fixes i j A B :: nat assumes "i < B" "j < A"
3.99    shows "j + i * A < B * A"
3.100 @@ -546,64 +570,43 @@
3.101  lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
3.102    by (rule dimension_vec_def)
3.103
3.104 -lemma all_less_DIM_cart:
3.105 -  fixes m n :: nat
3.106 -  shows "(\<forall>i<DIM('a^'b). P i) \<longleftrightarrow> (\<forall>x::'b. \<forall>i<DIM('a). P (i + \<pi>' x * DIM('a)))"
3.107 -unfolding DIM_cart
3.108 -apply safe
3.109 -apply (drule spec, erule mp, erule linear_less_than_times [OF pi'_range])
3.110 -apply (erule split_CARD_DIM, simp)
3.111 -done
3.112 -
3.113 -lemma eq_pi_iff:
3.114 -  fixes x :: "'c::finite"
3.115 -  shows "i < CARD('c::finite) \<Longrightarrow> x = \<pi> i \<longleftrightarrow> \<pi>' x = i"
3.116 -  by auto
3.117 -
3.118 -lemma all_less_mult:
3.119 -  fixes m n :: nat
3.120 -  shows "(\<forall>i<(m * n). P i) \<longleftrightarrow> (\<forall>i<m. \<forall>j<n. P (j + i * n))"
3.121 -apply safe
3.122 -apply (drule spec, erule mp, erule (1) linear_less_than_times)
3.123 -apply (erule split_times_into_modulo, simp)
3.124 -done
3.125 -
3.126 -lemma inner_if:
3.127 -  "inner (if a then x else y) z = (if a then inner x z else inner y z)"
3.128 -  "inner x (if a then y else z) = (if a then inner x y else inner x z)"
3.129 -  by simp_all
3.130 -
3.131  instance proof
3.132 -  show "0 < DIM('a ^ 'b)"
3.133 -    unfolding dimension_vec_def
3.134 -    by (intro mult_pos_pos zero_less_card_finite DIM_positive)
3.135 +  show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
3.136 +    unfolding Basis_vec_def by simp
3.137 +next
3.138 +  show "finite (Basis :: ('a ^ 'b) set)"
3.139 +    unfolding Basis_vec_def by simp
3.140  next
3.141 -  fix i :: nat
3.142 -  assume "DIM('a ^ 'b) \<le> i" thus "basis i = (0::'a^'b)"
3.143 -    unfolding dimension_vec_def basis_vec_def
3.144 -    by simp
3.145 +  fix u v :: "'a ^ 'b"
3.146 +  assume "u \<in> Basis" and "v \<in> Basis"
3.147 +  thus "inner u v = (if u = v then 1 else 0)"
3.148 +    unfolding Basis_vec_def
3.149 +    by (auto simp add: inner_axis_axis axis_eq_axis inner_Basis)
3.150  next
3.151 -  show "\<forall>i<DIM('a ^ 'b). \<forall>j<DIM('a ^ 'b).
3.152 -    inner (basis i :: 'a ^ 'b) (basis j) = (if i = j then 1 else 0)"
3.153 -    apply (simp add: inner_vec_def)
3.154 -    apply safe
3.155 -    apply (erule split_CARD_DIM, simp add: basis_eq_pi')
3.156 -    apply (simp add: inner_if setsum_delta cong: if_cong)
3.157 -    apply (simp add: basis_orthonormal)
3.158 -    apply (elim split_CARD_DIM, simp add: basis_eq_pi')
3.159 -    apply (simp add: inner_if setsum_delta cong: if_cong)
3.160 -    apply (clarsimp simp add: basis_orthonormal)
3.161 +  fix x :: "'a ^ 'b"
3.162 +  show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
3.163 +    unfolding Basis_vec_def
3.164 +    by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
3.165 +next
3.166 +  show "DIM('a ^ 'b) = card (Basis :: ('a ^ 'b) set)"
3.167 +    unfolding Basis_vec_def dimension_vec_def dimension_def
3.168 +    by (simp add: card_UN_disjoint [unfolded disjoint_iff]
3.169 +      axis_eq_axis nonzero_Basis)
3.170 +next
3.171 +  show "basis ` {..<DIM('a ^ 'b)} = (Basis :: ('a ^ 'b) set)"
3.172 +    unfolding Basis_vec_def
3.173 +    apply auto
3.174 +    apply (erule split_times_into_modulo)
3.175 +    apply (simp add: basis_eq axis_eq_axis)
3.176 +    apply (erule Basis_elim)
3.177 +    apply (simp add: image_def basis_vec_def axis_eq_axis)
3.178 +    apply (rule rev_bexI, simp)
3.179 +    apply (erule linear_less_than_times [OF pi'_range])
3.180 +    apply simp
3.181      done
3.182  next
3.183 -  fix x :: "'a ^ 'b"
3.184 -  show "(\<forall>i<DIM('a ^ 'b). inner (basis i) x = 0) \<longleftrightarrow> x = 0"
3.185 -    unfolding all_less_DIM_cart
3.186 -    unfolding inner_vec_def
3.187 -    apply (simp add: basis_eq_pi')
3.188 -    apply (simp add: inner_if setsum_delta cong: if_cong)
3.189 -    apply (simp add: euclidean_all_zero)
3.190 -    apply (simp add: vec_eq_iff)
3.191 -    done
3.192 +  show "basis ` {DIM('a ^ 'b)..} = {0::'a ^ 'b}"
3.193 +    by (auto simp add: image_def basis_vec_def)
3.194  qed
3.195
3.196  end
```
```     4.1 --- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 11 09:11:15 2011 -0700
4.2 +++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy	Thu Aug 11 13:05:56 2011 -0700
4.3 @@ -1581,12 +1581,6 @@
4.4
4.5  subsection{* Euclidean Spaces as Typeclass*}
4.6
4.7 -lemma (in euclidean_space) basis_inj[simp, intro]: "inj_on basis {..<DIM('a)}"
4.8 -  by (rule inj_onI, rule ccontr, cut_tac i=x and j=y in dot_basis, simp)
4.9 -
4.10 -lemma (in euclidean_space) basis_finite: "basis ` {DIM('a)..} = {0}"
4.11 -  by (auto intro: image_eqI [where x="DIM('a)"])
4.12 -
4.13  lemma independent_eq_inj_on:
4.14    fixes D :: nat and f :: "nat \<Rightarrow> 'c::real_vector" assumes *: "inj_on f {..<D}"
4.15    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)"
```