modify euclidean_space class to include basis set
authorhuffman
Thu Aug 11 13:05:56 2011 -0700 (2011-08-11)
changeset 44166d12d89a66742
parent 44165 d26a45f3c835
child 44167 e81d676d598e
modify euclidean_space class to include basis set
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
src/HOL/Multivariate_Analysis/Linear_Algebra.thy
     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)"