1.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 09 13:09:35 2011 -0700
1.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 10 00:29:31 2011 -0700
1.3 @@ -355,9 +355,11 @@
1.4 lemma \<pi>_inj_on: "inj_on (\<pi>::nat\<Rightarrow>'n::finite) {..<CARD('n)}"
1.5 using bij_betw_pi[where 'n='n] by (simp add: bij_betw_def)
1.6
1.7 -instantiation cart :: (real_basis,finite) real_basis
1.8 +instantiation cart :: (euclidean_space, finite) euclidean_space
1.9 begin
1.10
1.11 +definition "dimension (t :: ('a ^ 'b) itself) = CARD('b) * DIM('a)"
1.12 +
1.13 definition "(basis i::'a^'b) =
1.14 (if i < (CARD('b) * DIM('a))
1.15 then (\<chi> j::'b. if j = \<pi>(i div DIM('a)) then basis (i mod DIM('a)) else 0)
1.16 @@ -417,133 +419,84 @@
1.17 finally show ?thesis by simp
1.18 qed
1.19
1.20 -instance
1.21 -proof
1.22 - let ?b = "basis :: nat \<Rightarrow> 'a^'b"
1.23 - let ?b' = "basis :: nat \<Rightarrow> 'a"
1.24 +lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
1.25 + by (rule dimension_cart_def)
1.26
1.27 - have setsum_basis:
1.28 - "\<And>f. (\<Sum>x\<in>range basis. f (x::'a)) = f 0 + (\<Sum>i<DIM('a). f (basis i))"
1.29 - unfolding range_basis apply (subst setsum.insert)
1.30 - by (auto simp: basis_eq_0_iff setsum.insert setsum_reindex[OF basis_inj])
1.31 +lemma all_less_DIM_cart:
1.32 + fixes m n :: nat
1.33 + shows "(\<forall>i<DIM('a^'b). P i) \<longleftrightarrow> (\<forall>x::'b. \<forall>i<DIM('a). P (i + \<pi>' x * DIM('a)))"
1.34 +unfolding DIM_cart
1.35 +apply safe
1.36 +apply (drule spec, erule mp, erule linear_less_than_times [OF pi'_range])
1.37 +apply (erule split_CARD_DIM, simp)
1.38 +done
1.39
1.40 - have inj: "inj_on ?b {..<CARD('b)*DIM('a)}"
1.41 - by (auto intro!: inj_onI elim!: split_CARD_DIM split: split_if_asm
1.42 - simp add: Cart_eq basis_eq_pi' all_conj_distrib basis_neq_0
1.43 - inj_on_iff[OF basis_inj])
1.44 - moreover
1.45 - hence indep: "independent (?b ` {..<CARD('b) * DIM('a)})"
1.46 - proof (rule independent_eq_inj_on[THEN iffD2], safe elim!: split_CARD_DIM del: notI)
1.47 - fix j and i :: 'b and u :: "'a^'b \<Rightarrow> real" assume "j < DIM('a)"
1.48 - let ?x = "j + \<pi>' i * DIM('a)"
1.49 - show "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) \<noteq> ?b ?x"
1.50 - unfolding Cart_eq not_all
1.51 - proof
1.52 - have "(\<lambda>j. j + \<pi>' i*DIM('a))`({..<DIM('a)}-{j}) =
1.53 - {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)} - {?x}"(is "?S = ?I - _")
1.54 - proof safe
1.55 - fix y assume "y \<in> ?I"
1.56 - moreover def k \<equiv> "y - \<pi>' i*DIM('a)"
1.57 - ultimately have "k < DIM('a)" and "y = k + \<pi>' i * DIM('a)" by auto
1.58 - moreover assume "y \<notin> ?S"
1.59 - ultimately show "y = j + \<pi>' i * DIM('a)" by auto
1.60 - qed auto
1.61 +lemma eq_pi_iff:
1.62 + fixes x :: "'c::finite"
1.63 + shows "i < CARD('c::finite) \<Longrightarrow> x = \<pi> i \<longleftrightarrow> \<pi>' x = i"
1.64 + by auto
1.65
1.66 - have "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) $ i =
1.67 - (\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k $ i)" by simp
1.68 - also have "\<dots> = (\<Sum>k\<in>?S. u(?b k) *\<^sub>R ?b k $ i)"
1.69 - unfolding `?S = ?I - {?x}`
1.70 - proof (safe intro!: setsum_mono_zero_cong_right)
1.71 - fix y assume "y \<in> {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)}"
1.72 - moreover have "Suc (\<pi>' i) * DIM('a) \<le> CARD('b) * DIM('a)"
1.73 - unfolding mult_le_cancel2 using pi'_range[of i] by simp
1.74 - ultimately show "y < CARD('b) * DIM('a)" by simp
1.75 - next
1.76 - fix y assume "y < CARD('b) * DIM('a)"
1.77 - with split_CARD_DIM guess l k . note y = this
1.78 - moreover assume "u (?b y) *\<^sub>R ?b y $ i \<noteq> 0"
1.79 - ultimately show "y \<in> {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)}"
1.80 - by (auto simp: basis_eq_pi' split: split_if_asm)
1.81 - qed simp
1.82 - also have "\<dots> = (\<Sum>k\<in>{..<DIM('a)} - {j}. u (?b (k + \<pi>' i*DIM('a))) *\<^sub>R (?b' k))"
1.83 - by (subst setsum_reindex) (auto simp: basis_eq_pi' intro!: inj_onI)
1.84 - also have "\<dots> \<noteq> ?b ?x $ i"
1.85 - proof -
1.86 - note independent_eq_inj_on[THEN iffD1, OF basis_inj independent_basis, rule_format]
1.87 - note this[of j "\<lambda>v. u (\<chi> ka::'b. if ka = i then v else (0\<Colon>'a))"]
1.88 - thus ?thesis by (simp add: `j < DIM('a)` basis_eq pi'_range)
1.89 - qed
1.90 - finally show "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) $ i \<noteq> ?b ?x $ i" .
1.91 - qed
1.92 - qed
1.93 - ultimately
1.94 - show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
1.95 - by (auto intro!: exI[of _ "CARD('b) * DIM('a)"] simp: basis_cart_def)
1.96 +lemma all_less_mult:
1.97 + fixes m n :: nat
1.98 + shows "(\<forall>i<(m * n). P i) \<longleftrightarrow> (\<forall>i<m. \<forall>j<n. P (j + i * n))"
1.99 +apply safe
1.100 +apply (drule spec, erule mp, erule (1) linear_less_than_times)
1.101 +apply (erule split_times_into_modulo, simp)
1.102 +done
1.103
1.104 - from indep have exclude_0: "0 \<notin> ?b ` {..<CARD('b) * DIM('a)}"
1.105 - using dependent_0[of "?b ` {..<CARD('b) * DIM('a)}"] by blast
1.106 +lemma inner_if:
1.107 + "inner (if a then x else y) z = (if a then inner x z else inner y z)"
1.108 + "inner x (if a then y else z) = (if a then inner x y else inner x z)"
1.109 + by simp_all
1.110
1.111 - show "span (range ?b) = UNIV"
1.112 - proof -
1.113 - { fix x :: "'a^'b"
1.114 - let "?if i y" = "(\<chi> k::'b. if k = i then ?b' y else (0\<Colon>'a))"
1.115 - have The_if: "\<And>i j. j < DIM('a) \<Longrightarrow> (THE k. (?if i j) $ k \<noteq> 0) = i"
1.116 - by (rule the_equality) (simp_all split: split_if_asm add: basis_neq_0)
1.117 - { fix x :: 'a
1.118 - have "x \<in> span (range basis)"
1.119 - using span_basis by (auto simp: range_basis)
1.120 - hence "\<exists>u. (\<Sum>x<DIM('a). u (?b' x) *\<^sub>R ?b' x) = x"
1.121 - by (subst (asm) span_finite) (auto simp: setsum_basis) }
1.122 - hence "\<forall>i. \<exists>u. (\<Sum>x<DIM('a). u (?b' x) *\<^sub>R ?b' x) = i" by auto
1.123 - then obtain u where u: "\<forall>i. (\<Sum>x<DIM('a). u i (?b' x) *\<^sub>R ?b' x) = i"
1.124 - by (auto dest: choice)
1.125 - have "\<exists>u. \<forall>i. (\<Sum>j<DIM('a). u (?if i j) *\<^sub>R ?b' j) = x $ i"
1.126 - apply (rule exI[of _ "\<lambda>v. let i = (THE i. v$i \<noteq> 0) in u (x$i) (v$i)"])
1.127 - using The_if u by simp }
1.128 - moreover
1.129 - have "\<And>i::'b. {..<CARD('b)} \<inter> {x. i = \<pi> x} = {\<pi>' i}"
1.130 - using pi'_range[where 'n='b] by auto
1.131 - moreover
1.132 - have "range ?b = {0} \<union> ?b ` {..<CARD('b) * DIM('a)}"
1.133 - by (auto simp: image_def basis_cart_def)
1.134 - ultimately
1.135 - show ?thesis
1.136 - by (auto simp add: Cart_eq setsum_reindex[OF inj] range_basis
1.137 - setsum_mult_product basis_eq if_distrib setsum_cases span_finite
1.138 - setsum_reindex[OF basis_inj])
1.139 - qed
1.140 +instance proof
1.141 + show "0 < DIM('a ^ 'b)"
1.142 + unfolding dimension_cart_def
1.143 + by (intro mult_pos_pos zero_less_card_finite DIM_positive)
1.144 +next
1.145 + fix i :: nat
1.146 + assume "DIM('a ^ 'b) \<le> i" thus "basis i = (0::'a^'b)"
1.147 + unfolding dimension_cart_def basis_cart_def
1.148 + by simp
1.149 +next
1.150 + show "\<forall>i<DIM('a ^ 'b). \<forall>j<DIM('a ^ 'b).
1.151 + (basis i :: 'a ^ 'b) \<bullet> basis j = (if i = j then 1 else 0)"
1.152 + apply (simp add: inner_vector_def)
1.153 + apply safe
1.154 + apply (erule split_CARD_DIM, simp add: basis_eq_pi')
1.155 + apply (simp add: inner_if setsum_delta cong: if_cong)
1.156 + apply (simp add: basis_orthonormal)
1.157 + apply (elim split_CARD_DIM, simp add: basis_eq_pi')
1.158 + apply (simp add: inner_if setsum_delta cong: if_cong)
1.159 + apply (clarsimp simp add: basis_orthonormal)
1.160 + done
1.161 +next
1.162 + fix x :: "'a ^ 'b"
1.163 + show "(\<forall>i<DIM('a ^ 'b). inner (basis i) x = 0) \<longleftrightarrow> x = 0"
1.164 + unfolding all_less_DIM_cart
1.165 + unfolding inner_vector_def
1.166 + apply (simp add: basis_eq_pi')
1.167 + apply (simp add: inner_if setsum_delta cong: if_cong)
1.168 + apply (simp add: euclidean_all_zero)
1.169 + apply (simp add: Cart_eq)
1.170 + done
1.171 qed
1.172
1.173 end
1.174
1.175 -lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a::real_basis)"
1.176 -proof (safe intro!: dimension_eq elim!: split_times_into_modulo del: notI)
1.177 - fix i j assume *: "i < CARD('b)" "j < DIM('a)"
1.178 - hence A: "(i * DIM('a) + j) div DIM('a) = i"
1.179 - by (subst div_add1_eq) simp
1.180 - from * have B: "(i * DIM('a) + j) mod DIM('a) = j"
1.181 - unfolding mod_mult_self3 by simp
1.182 - show "basis (j + i * DIM('a)) \<noteq> (0::'a^'b)" unfolding basis_cart_def
1.183 - using * basis_finite[where 'a='a]
1.184 - linear_less_than_times[of i "CARD('b)" j "DIM('a)"]
1.185 - by (auto simp: A B field_simps Cart_eq basis_eq_0_iff)
1.186 -qed (auto simp: basis_cart_def)
1.187 -
1.188 lemma if_distr: "(if P then f else g) $ i = (if P then f $ i else g $ i)" by simp
1.189
1.190 lemma split_dimensions'[consumes 1]:
1.191 - assumes "k < DIM('a::real_basis^'b)"
1.192 - obtains i j where "i < CARD('b::finite)" and "j < DIM('a::real_basis)" and "k = j + i * DIM('a::real_basis)"
1.193 + assumes "k < DIM('a::euclidean_space^'b)"
1.194 + obtains i j where "i < CARD('b::finite)" and "j < DIM('a::euclidean_space)" and "k = j + i * DIM('a::euclidean_space)"
1.195 using split_times_into_modulo[OF assms[simplified]] .
1.196
1.197 lemma cart_euclidean_bound[intro]:
1.198 - assumes j:"j < DIM('a::{real_basis})"
1.199 - shows "j + \<pi>' (i::'b::finite) * DIM('a) < CARD('b) * DIM('a::real_basis)"
1.200 + assumes j:"j < DIM('a::euclidean_space)"
1.201 + shows "j + \<pi>' (i::'b::finite) * DIM('a) < CARD('b) * DIM('a::euclidean_space)"
1.202 using linear_less_than_times[OF pi'_range j, of i] .
1.203
1.204 -instance cart :: (real_basis_with_inner,finite) real_basis_with_inner ..
1.205 -
1.206 -lemma (in real_basis) forall_CARD_DIM:
1.207 +lemma (in euclidean_space) forall_CARD_DIM:
1.208 "(\<forall>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<forall>(i::'b::finite) j. j<DIM('a) \<longrightarrow> P (j + \<pi>' i * DIM('a)))"
1.209 (is "?l \<longleftrightarrow> ?r")
1.210 proof (safe elim!: split_times_into_modulo)
1.211 @@ -557,7 +510,7 @@
1.212 show "P (j + i * DIM('a))" by simp
1.213 qed
1.214
1.215 -lemma (in real_basis) exists_CARD_DIM:
1.216 +lemma (in euclidean_space) exists_CARD_DIM:
1.217 "(\<exists>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<exists>i::'b::finite. \<exists>j<DIM('a). P (j + \<pi>' i * DIM('a)))"
1.218 using forall_CARD_DIM[where 'b='b, of "\<lambda>x. \<not> P x"] by blast
1.219
1.220 @@ -572,7 +525,7 @@
1.221 lemmas cart_simps = forall_CARD_DIM exists_CARD_DIM forall_CARD exists_CARD
1.222
1.223 lemma cart_euclidean_nth[simp]:
1.224 - fixes x :: "('a::real_basis_with_inner, 'b::finite) cart"
1.225 + fixes x :: "('a::euclidean_space, 'b::finite) cart"
1.226 assumes j:"j < DIM('a)"
1.227 shows "x $$ (j + \<pi>' i * DIM('a)) = x $ i $$ j"
1.228 unfolding euclidean_component_def inner_vector_def basis_eq_pi'[OF j] if_distrib cond_application_beta
1.229 @@ -606,22 +559,6 @@
1.230 thus "x = y \<and> i = j" using * by simp
1.231 qed simp
1.232
1.233 -instance cart :: (euclidean_space,finite) euclidean_space
1.234 -proof (default, safe elim!: split_dimensions')
1.235 - let ?b = "basis :: nat \<Rightarrow> 'a^'b"
1.236 - have if_distrib_op: "\<And>f P Q a b c d.
1.237 - f (if P then a else b) (if Q then c else d) =
1.238 - (if P then if Q then f a c else f a d else if Q then f b c else f b d)"
1.239 - by simp
1.240 -
1.241 - fix i j k l
1.242 - assume "i < CARD('b)" "k < CARD('b)" "j < DIM('a)" "l < DIM('a)"
1.243 - thus "?b (j + i * DIM('a)) \<bullet> ?b (l + k * DIM('a)) =
1.244 - (if j + i * DIM('a) = l + k * DIM('a) then 1 else 0)"
1.245 - using inj_on_iff[OF \<pi>_inj_on[where 'n='b], of k i]
1.246 - by (auto simp add: basis_eq inner_vector_def if_distrib_op[of inner] setsum_cases basis_orthonormal mult_split_eq)
1.247 -qed
1.248 -
1.249 instance cart :: (ordered_euclidean_space,finite) ordered_euclidean_space
1.250 proof
1.251 fix x y::"'a^'b"
2.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 09 13:09:35 2011 -0700
2.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 10 00:29:31 2011 -0700
2.3 @@ -1582,119 +1582,50 @@
2.4
2.5 subsection{* Euclidean Spaces as Typeclass*}
2.6
2.7 -class real_basis = real_vector +
2.8 +class euclidean_space = real_inner +
2.9 + fixes dimension :: "'a itself \<Rightarrow> nat"
2.10 fixes basis :: "nat \<Rightarrow> 'a"
2.11 - assumes span_basis: "span (range basis) = UNIV"
2.12 - assumes dimension_exists: "\<exists>d>0.
2.13 - basis ` {d..} = {0} \<and>
2.14 - independent (basis ` {..<d}) \<and>
2.15 - inj_on basis {..<d}"
2.16 -
2.17 -definition (in real_basis) dimension :: "'a itself \<Rightarrow> nat" where
2.18 - "dimension x =
2.19 - (THE d. basis ` {d..} = {0} \<and> independent (basis ` {..<d}) \<and> inj_on basis {..<d})"
2.20 + assumes DIM_positive [intro]:
2.21 + "0 < dimension TYPE('a)"
2.22 + assumes basis_zero [simp]:
2.23 + "dimension TYPE('a) \<le> i \<Longrightarrow> basis i = 0"
2.24 + assumes basis_orthonormal:
2.25 + "\<forall>i<dimension TYPE('a). \<forall>j<dimension TYPE('a).
2.26 + inner (basis i) (basis j) = (if i = j then 1 else 0)"
2.27 + assumes euclidean_all_zero:
2.28 + "(\<forall>i<dimension TYPE('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)"
2.29
2.30 syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
2.31
2.32 translations "DIM('t)" == "CONST dimension (TYPE('t))"
2.33
2.34 -lemma (in real_basis) dimensionI:
2.35 - assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0}; independent (basis ` {..<d});
2.36 - inj_on basis {..<d} \<rbrakk> \<Longrightarrow> P d"
2.37 - shows "P DIM('a)"
2.38 +lemma (in euclidean_space) dot_basis:
2.39 + "inner (basis i) (basis j) = (if i = j \<and> i < DIM('a) then 1 else 0)"
2.40 +proof (cases "(i < DIM('a) \<and> j < DIM('a))")
2.41 + case False
2.42 + hence "inner (basis i) (basis j) = 0" by auto
2.43 + thus ?thesis using False by auto
2.44 +next
2.45 + case True thus ?thesis using basis_orthonormal by auto
2.46 +qed
2.47 +
2.48 +lemma (in euclidean_space) basis_eq_0_iff [simp]:
2.49 + "basis i = 0 \<longleftrightarrow> DIM('a) \<le> i"
2.50 proof -
2.51 - obtain d where "0 < d" and d: "basis ` {d..} = {0} \<and>
2.52 - independent (basis ` {..<d}) \<and> inj_on basis {..<d}" (is "?P d")
2.53 - using dimension_exists by auto
2.54 - show ?thesis unfolding dimension_def
2.55 - proof (rule theI2)
2.56 - fix d' assume "?P d'"
2.57 - with d have "basis d' = 0" "basis d = 0" and
2.58 - "d < d' \<Longrightarrow> basis d \<noteq> 0"
2.59 - "d' < d \<Longrightarrow> basis d' \<noteq> 0"
2.60 - using dependent_0 by auto
2.61 - thus "d' = d" by (cases rule: linorder_cases) auto
2.62 - moreover have "P d" using assms[of d] `0 < d` d by auto
2.63 - ultimately show "P d'" by simp
2.64 - next show "?P d" using `?P d` .
2.65 - qed
2.66 + have "inner (basis i) (basis i) = 0 \<longleftrightarrow> DIM('a) \<le> i"
2.67 + by (simp add: dot_basis)
2.68 + thus ?thesis by simp
2.69 qed
2.70
2.71 -lemma (in real_basis) dimension_eq:
2.72 - assumes "\<And>i. i < d \<Longrightarrow> basis i \<noteq> 0"
2.73 - assumes "\<And>i. d \<le> i \<Longrightarrow> basis i = 0"
2.74 - shows "DIM('a) = d"
2.75 -proof (rule dimensionI)
2.76 - let ?b = "basis :: nat \<Rightarrow> 'a"
2.77 - fix d' assume *: "?b ` {d'..} = {0}" "independent (?b ` {..<d'})"
2.78 - show "d' = d"
2.79 - proof (cases rule: linorder_cases)
2.80 - assume "d' < d" hence "basis d' \<noteq> 0" using assms by auto
2.81 - with * show ?thesis by auto
2.82 - next
2.83 - assume "d < d'" hence "basis d \<noteq> 0" using * dependent_0 by auto
2.84 - with assms(2) `d < d'` show ?thesis by auto
2.85 - qed
2.86 -qed
2.87 -
2.88 -lemma (in real_basis)
2.89 - shows basis_finite: "basis ` {DIM('a)..} = {0}"
2.90 - and independent_basis: "independent (basis ` {..<DIM('a)})"
2.91 - and DIM_positive[intro]: "(DIM('a) :: nat) > 0"
2.92 - and basis_inj[simp, intro]: "inj_on basis {..<DIM('a)}"
2.93 - by (auto intro!: dimensionI)
2.94 -
2.95 -lemma (in real_basis) basis_eq_0_iff: "basis j = 0 \<longleftrightarrow> DIM('a) \<le> j"
2.96 -proof
2.97 - show "DIM('a) \<le> j \<Longrightarrow> basis j = 0" using basis_finite by auto
2.98 -next
2.99 - have "j < DIM('a) \<Longrightarrow> basis j \<noteq> 0"
2.100 - using independent_basis by (auto intro!: dependent_0)
2.101 - thus "basis j = 0 \<Longrightarrow> DIM('a) \<le> j" unfolding not_le[symmetric] by blast
2.102 -qed
2.103 -
2.104 -lemma (in real_basis) range_basis:
2.105 - "range basis = insert 0 (basis ` {..<DIM('a)})"
2.106 -proof -
2.107 - have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto
2.108 - show ?thesis unfolding * image_Un basis_finite by auto
2.109 -qed
2.110 -
2.111 -lemma (in real_basis) range_basis_finite[intro]:
2.112 - "finite (range basis)"
2.113 - unfolding range_basis by auto
2.114 -
2.115 -lemma (in real_basis) basis_neq_0[intro]:
2.116 - assumes "i<DIM('a)" shows "(basis i) \<noteq> 0"
2.117 -proof(rule ccontr) assume "\<not> basis i \<noteq> (0::'a)"
2.118 - hence "(0::'a) \<in> basis ` {..<DIM('a)}" using assms by auto
2.119 - from dependent_0[OF this] show False using independent_basis by auto
2.120 -qed
2.121 -
2.122 -lemma (in real_basis) basis_zero[simp]:
2.123 - assumes"i \<ge> DIM('a)" shows "basis i = 0"
2.124 -proof-
2.125 - have "(basis i::'a) \<in> basis ` {DIM('a)..}" using assms by auto
2.126 - thus ?thesis unfolding basis_finite by fastsimp
2.127 -qed
2.128 -
2.129 -lemma basis_representation:
2.130 - "\<exists>u. x = (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R (v\<Colon>'a\<Colon>real_basis))"
2.131 -proof -
2.132 - have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]]
2.133 - have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x"
2.134 - unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto
2.135 - thus ?thesis by fastsimp
2.136 -qed
2.137 -
2.138 -lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = UNIV"
2.139 - apply(subst span_basis[symmetric]) unfolding range_basis by auto
2.140 -
2.141 -lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = DIM('a)"
2.142 - apply(subst card_image) using basis_inj by auto
2.143 -
2.144 -lemma in_span_basis: "(x::'a::real_basis) \<in> span (basis ` {..<DIM('a)})"
2.145 - unfolding span_basis' ..
2.146 +lemma (in euclidean_space) norm_basis [simp]:
2.147 + "norm (basis i) = (if i < DIM('a) then 1 else 0)"
2.148 + unfolding norm_eq_sqrt_inner dot_basis by simp
2.149 +
2.150 +lemma (in euclidean_space) basis_inj[simp, intro]: "inj_on basis {..<DIM('a)}"
2.151 + by (rule inj_onI, rule ccontr, cut_tac i=x and j=y in dot_basis, simp)
2.152 +
2.153 +lemma (in euclidean_space) basis_finite: "basis ` {DIM('a)..} = {0}"
2.154 + by (auto intro: image_eqI [where x="DIM('a)"])
2.155
2.156 lemma independent_eq_inj_on:
2.157 fixes D :: nat and f :: "nat \<Rightarrow> 'c::real_vector" assumes *: "inj_on f {..<D}"
2.158 @@ -1708,56 +1639,98 @@
2.159 by (auto simp: eq setsum_reindex[OF inj])
2.160 qed
2.161
2.162 -class real_basis_with_inner = real_inner + real_basis
2.163 -begin
2.164 -
2.165 -definition euclidean_component (infixl "$$" 90) where
2.166 - "x $$ i = inner (basis i) x"
2.167 -
2.168 -definition Chi (binder "\<chi>\<chi> " 10) where
2.169 - "(\<chi>\<chi> i. f i) = (\<Sum>i<DIM('a). f i *\<^sub>R basis i)"
2.170 -
2.171 -lemma basis_at_neq_0[intro]:
2.172 +lemma independent_basis:
2.173 + "independent (basis ` {..<DIM('a)} :: 'a::euclidean_space set)"
2.174 + unfolding independent_eq_inj_on [OF basis_inj]
2.175 + apply clarify
2.176 + apply (drule_tac f="inner (basis a)" in arg_cong)
2.177 + apply (simp add: inner_right.setsum dot_basis)
2.178 + done
2.179 +
2.180 +lemma dimensionI:
2.181 + assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0::'a::euclidean_space};
2.182 + independent (basis ` {..<d} :: 'a set);
2.183 + inj_on (basis :: nat \<Rightarrow> 'a) {..<d} \<rbrakk> \<Longrightarrow> P d"
2.184 + shows "P DIM('a::euclidean_space)"
2.185 + using DIM_positive basis_finite independent_basis basis_inj
2.186 + by (rule assms)
2.187 +
2.188 +lemma (in euclidean_space) dimension_eq:
2.189 + assumes "\<And>i. i < d \<Longrightarrow> basis i \<noteq> 0"
2.190 + assumes "\<And>i. d \<le> i \<Longrightarrow> basis i = 0"
2.191 + shows "DIM('a) = d"
2.192 +proof (rule linorder_cases [of "DIM('a)" d])
2.193 + assume "DIM('a) < d"
2.194 + hence "basis DIM('a) \<noteq> 0" by (rule assms)
2.195 + thus ?thesis by simp
2.196 +next
2.197 + assume "d < DIM('a)"
2.198 + hence "basis d \<noteq> 0" by simp
2.199 + thus ?thesis by (simp add: assms)
2.200 +next
2.201 + assume "DIM('a) = d" thus ?thesis .
2.202 +qed
2.203 +
2.204 +lemma (in euclidean_space) range_basis:
2.205 + "range basis = insert 0 (basis ` {..<DIM('a)})"
2.206 +proof -
2.207 + have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto
2.208 + show ?thesis unfolding * image_Un basis_finite by auto
2.209 +qed
2.210 +
2.211 +lemma (in euclidean_space) range_basis_finite[intro]:
2.212 + "finite (range basis)"
2.213 + unfolding range_basis by auto
2.214 +
2.215 +lemma (in euclidean_space) basis_neq_0 [intro]:
2.216 + assumes "i<DIM('a)" shows "(basis i) \<noteq> 0"
2.217 + using assms by simp
2.218 +
2.219 +subsubsection {* Projecting components *}
2.220 +
2.221 +definition (in euclidean_space) euclidean_component (infixl "$$" 90)
2.222 + where "x $$ i = inner (basis i) x"
2.223 +
2.224 +lemma bounded_linear_euclidean_component:
2.225 + "bounded_linear (\<lambda>x. euclidean_component x i)"
2.226 + unfolding euclidean_component_def
2.227 + by (rule inner.bounded_linear_right)
2.228 +
2.229 +interpretation euclidean_component:
2.230 + bounded_linear "\<lambda>x. euclidean_component x i"
2.231 + by (rule bounded_linear_euclidean_component)
2.232 +
2.233 +lemma euclidean_eqI:
2.234 + fixes x y :: "'a::euclidean_space"
2.235 + assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
2.236 +proof -
2.237 + from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
2.238 + by (simp add: euclidean_component.diff)
2.239 + then show "x = y"
2.240 + unfolding euclidean_component_def euclidean_all_zero by simp
2.241 +qed
2.242 +
2.243 +lemma euclidean_eq:
2.244 + fixes x y :: "'a::euclidean_space"
2.245 + shows "x = y \<longleftrightarrow> (\<forall>i<DIM('a). x $$ i = y $$ i)"
2.246 + by (auto intro: euclidean_eqI)
2.247 +
2.248 +lemma (in euclidean_space) basis_component [simp]:
2.249 + "basis i $$ j = (if i = j \<and> i < DIM('a) then 1 else 0)"
2.250 + unfolding euclidean_component_def dot_basis by auto
2.251 +
2.252 +lemma (in euclidean_space) basis_at_neq_0 [intro]:
2.253 "i < DIM('a) \<Longrightarrow> basis i $$ i \<noteq> 0"
2.254 - unfolding euclidean_component_def by (auto intro!: basis_neq_0)
2.255 -
2.256 -lemma euclidean_component_ge[simp]:
2.257 + by simp
2.258 +
2.259 +lemma (in euclidean_space) euclidean_component_ge [simp]:
2.260 assumes "i \<ge> DIM('a)" shows "x $$ i = 0"
2.261 - unfolding euclidean_component_def basis_zero[OF assms] by auto
2.262 + unfolding euclidean_component_def basis_zero[OF assms] by simp
2.263
2.264 lemma euclidean_scaleR:
2.265 shows "(a *\<^sub>R x) $$ i = a * (x$$i)"
2.266 unfolding euclidean_component_def by auto
2.267
2.268 -end
2.269 -
2.270 -interpretation euclidean_component:
2.271 - bounded_linear "\<lambda>x. euclidean_component x i"
2.272 - unfolding euclidean_component_def
2.273 - by (rule inner.bounded_linear_right)
2.274 -
2.275 -subsection{* Euclidean Spaces as Typeclass *}
2.276 -
2.277 -class euclidean_space = real_basis_with_inner +
2.278 - assumes basis_orthonormal: "\<forall>i<DIM('a). \<forall>j<DIM('a).
2.279 - inner (basis i) (basis j) = (if i = j then 1 else 0)"
2.280 -
2.281 -lemma (in euclidean_space) dot_basis:
2.282 - "inner (basis i) (basis j) = (if i = j \<and> i<DIM('a) then 1 else 0)"
2.283 -proof (cases "(i < DIM('a) \<and> j < DIM('a))")
2.284 - case False
2.285 - hence "basis i = 0 \<or> basis j = 0"
2.286 - using basis_finite by fastsimp
2.287 - hence "inner (basis i) (basis j) = 0" by (rule disjE) simp_all
2.288 - thus ?thesis using False by auto
2.289 -next
2.290 - case True thus ?thesis using basis_orthonormal by auto
2.291 -qed
2.292 -
2.293 -lemma (in euclidean_space) basis_component[simp]:
2.294 - "basis i $$ j = (if i = j \<and> i < DIM('a) then 1 else 0)"
2.295 - unfolding euclidean_component_def dot_basis by auto
2.296 -
2.297 lemmas euclidean_simps =
2.298 euclidean_component.add
2.299 euclidean_component.diff
2.300 @@ -1767,34 +1740,22 @@
2.301 basis_component
2.302
2.303 lemma euclidean_representation:
2.304 - "(x\<Colon>'a\<Colon>euclidean_space) = (\<Sum>i\<in>{..<DIM('a)}. (x$$i) *\<^sub>R basis i)"
2.305 -proof-
2.306 - from basis_representation[of x] guess u ..
2.307 - hence *:"x = (\<Sum>i\<in>{..<DIM('a)}. u (basis i) *\<^sub>R (basis i))"
2.308 - by (simp add: setsum_reindex)
2.309 - show ?thesis apply(subst *)
2.310 - proof(safe intro!: setsum_cong2)
2.311 - fix i assume i: "i < DIM('a)"
2.312 - hence "x$$i = (\<Sum>x<DIM('a). (if i = x then u (basis x) else 0))"
2.313 - by (auto simp: euclidean_simps * intro!: setsum_cong)
2.314 - also have "... = u (basis i)" using i by (auto simp: setsum_cases)
2.315 - finally show "u (basis i) *\<^sub>R basis i = x $$ i *\<^sub>R basis i" by simp
2.316 - qed
2.317 -qed
2.318 -
2.319 -lemma euclidean_eq:
2.320 - fixes x y :: "'a\<Colon>euclidean_space"
2.321 - shows "x = y \<longleftrightarrow> (\<forall>i<DIM('a). x$$i = y$$i)" (is "?l = ?r")
2.322 -proof safe
2.323 - assume "\<forall>i<DIM('a). x $$ i = y $$ i"
2.324 - thus "x = y"
2.325 - by (subst (1 2) euclidean_representation) auto
2.326 -qed
2.327 -
2.328 -lemma euclidean_lambda_beta[simp]:
2.329 + fixes x :: "'a::euclidean_space"
2.330 + shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
2.331 + apply (rule euclidean_eqI)
2.332 + apply (simp add: euclidean_component.setsum euclidean_component.scaleR)
2.333 + apply (simp add: if_distrib setsum_delta cong: if_cong)
2.334 + done
2.335 +
2.336 +subsubsection {* Binder notation for vectors *}
2.337 +
2.338 +definition (in euclidean_space) Chi (binder "\<chi>\<chi> " 10) where
2.339 + "(\<chi>\<chi> i. f i) = (\<Sum>i<DIM('a). f i *\<^sub>R basis i)"
2.340 +
2.341 +lemma euclidean_lambda_beta [simp]:
2.342 "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
2.343 - by (auto simp: euclidean_simps Chi_def if_distrib setsum_cases
2.344 - intro!: setsum_cong)
2.345 + by (auto simp: euclidean_component.setsum euclidean_component.scaleR
2.346 + Chi_def if_distrib setsum_cases intro!: setsum_cong)
2.347
2.348 lemma euclidean_lambda_beta':
2.349 "j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j"
2.350 @@ -1805,7 +1766,7 @@
2.351
2.352 lemma euclidean_beta_reduce[simp]:
2.353 "(\<chi>\<chi> i. x $$ i) = (x::'a::euclidean_space)"
2.354 - by (subst euclidean_eq) (simp add: euclidean_lambda_beta)
2.355 + by (simp add: euclidean_eq)
2.356
2.357 lemma euclidean_lambda_beta_0[simp]:
2.358 "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ 0 = f 0"
2.359 @@ -1823,6 +1784,34 @@
2.360 finally show ?thesis .
2.361 qed
2.362
2.363 +lemma span_basis: "span (range basis) = (UNIV :: 'a::euclidean_space set)"
2.364 +proof -
2.365 + { fix x :: 'a
2.366 + have "(\<Sum>i<DIM('a). (x $$ i) *\<^sub>R basis i) \<in> span (range basis :: 'a set)"
2.367 + by (simp add: span_setsum span_mul span_superset)
2.368 + hence "x \<in> span (range basis)"
2.369 + by (simp only: euclidean_representation [symmetric])
2.370 + } thus ?thesis by auto
2.371 +qed
2.372 +
2.373 +lemma basis_representation:
2.374 + "\<exists>u. x = (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R (v\<Colon>'a\<Colon>euclidean_space))"
2.375 +proof -
2.376 + have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]]
2.377 + have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x"
2.378 + unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto
2.379 + thus ?thesis by fastsimp
2.380 +qed
2.381 +
2.382 +lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = UNIV"
2.383 + apply(subst span_basis[symmetric]) unfolding range_basis by auto
2.384 +
2.385 +lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = DIM('a)"
2.386 + apply(subst card_image) using basis_inj by auto
2.387 +
2.388 +lemma in_span_basis: "(x::'a::euclidean_space) \<in> span (basis ` {..<DIM('a)})"
2.389 + unfolding span_basis' ..
2.390 +
2.391 lemma norm_basis[simp]:"norm (basis i::'a::euclidean_space) = (if i<DIM('a) then 1 else 0)"
2.392 unfolding norm_eq_sqrt_inner dot_basis by auto
2.393
2.394 @@ -3301,31 +3290,27 @@
2.395
2.396 subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
2.397
2.398 -instantiation real :: real_basis_with_inner
2.399 +instantiation real :: euclidean_space
2.400 begin
2.401 -definition [simp]: "basis i = (if i = 0 then (1::real) else 0)"
2.402 +
2.403 +definition
2.404 + "dimension (t::real itself) = 1"
2.405 +
2.406 +definition [simp]:
2.407 + "basis i = (if i = 0 then 1 else (0::real))"
2.408 +
2.409 +lemma DIM_real [simp]: "DIM(real) = 1"
2.410 + by (rule dimension_real_def)
2.411 +
2.412 +instance
2.413 + by default simp+
2.414 +
2.415 +end
2.416
2.417 lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto
2.418
2.419 -instance proof
2.420 - let ?b = "basis::nat \<Rightarrow> real"
2.421 -
2.422 - from basis_real_range have "independent (?b ` {..<1})" by auto
2.423 - thus "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
2.424 - by (auto intro!: exI[of _ 1] inj_onI)
2.425 -
2.426 - { fix x::real
2.427 - have "x \<in> span (range ?b)"
2.428 - using span_mul[of 1 "range ?b" x] span_clauses(1)[of 1 "range ?b"]
2.429 - by auto }
2.430 - thus "span (range ?b) = UNIV" by auto
2.431 -qed
2.432 -end
2.433 -
2.434 -lemma DIM_real[simp]: "DIM(real) = 1"
2.435 - by (rule dimension_eq) (auto simp: basis_real_def)
2.436 -
2.437 -instance real::ordered_euclidean_space proof qed(auto simp add:euclidean_component_def)
2.438 +instance real::ordered_euclidean_space
2.439 + by default (auto simp add: euclidean_component_def)
2.440
2.441 lemma Eucl_real_simps[simp]:
2.442 "(x::real) $$ 0 = x"
2.443 @@ -3335,177 +3320,89 @@
2.444 unfolding euclidean_lambda_beta'
2.445 unfolding euclidean_component_def by auto
2.446
2.447 -instantiation complex :: real_basis_with_inner
2.448 +instantiation complex :: euclidean_space
2.449 begin
2.450 -definition "basis i = (if i = 0 then 1 else if i = 1 then ii else 0)"
2.451 -
2.452 -lemma complex_basis[simp]:"basis 0 = (1::complex)" "basis 1 = ii" "basis (Suc 0) = ii"
2.453 +
2.454 +definition
2.455 + "dimension (t::complex itself) = 2"
2.456 +
2.457 +definition
2.458 + "basis i = (if i = 0 then 1 else if i = 1 then ii else 0)"
2.459 +
2.460 +lemma all_less_Suc: "(\<forall>i<Suc n. P i) \<longleftrightarrow> (\<forall>i<n. P i) \<and> P n"
2.461 + by (auto simp add: less_Suc_eq)
2.462 +
2.463 +instance proof
2.464 + show "0 < DIM(complex)"
2.465 + unfolding dimension_complex_def by simp
2.466 +next
2.467 + fix i :: nat
2.468 + assume "DIM(complex) \<le> i" thus "basis i = (0::complex)"
2.469 + unfolding dimension_complex_def basis_complex_def by simp
2.470 +next
2.471 + show "\<forall>i<DIM(complex). \<forall>j<DIM(complex).
2.472 + inner (basis i::complex) (basis j) = (if i = j then 1 else 0)"
2.473 + unfolding dimension_complex_def basis_complex_def inner_complex_def
2.474 + by (simp add: numeral_2_eq_2 all_less_Suc)
2.475 +next
2.476 + fix x :: complex
2.477 + show "(\<forall>i<DIM(complex). inner (basis i) x = 0) \<longleftrightarrow> x = 0"
2.478 + unfolding dimension_complex_def basis_complex_def inner_complex_def
2.479 + by (simp add: numeral_2_eq_2 all_less_Suc complex_eq_iff)
2.480 +qed
2.481 +
2.482 +end
2.483 +
2.484 +lemma complex_basis[simp]:
2.485 + shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii"
2.486 unfolding basis_complex_def by auto
2.487
2.488 -instance
2.489 -proof
2.490 - let ?b = "basis::nat \<Rightarrow> complex"
2.491 - have [simp]: "(range ?b) = {0, basis 0, basis 1}"
2.492 - by (auto simp: basis_complex_def split: split_if_asm)
2.493 - { fix z::complex
2.494 - have "z \<in> span (range ?b)"
2.495 - by (auto simp: span_finite complex_equality
2.496 - intro!: exI[of _ "\<lambda>i. if i = 1 then Re z else if i = ii then Im z else 0"]) }
2.497 - thus "span (range ?b) = UNIV" by auto
2.498 -
2.499 - have "{..<2} = {0, 1::nat}" by auto
2.500 - hence *: "?b ` {..<2} = {1, ii}"
2.501 - by (auto simp add: basis_complex_def)
2.502 - moreover have "1 \<notin> span {\<i>}"
2.503 - by (simp add: span_finite complex_equality complex_scaleR_def)
2.504 - hence "independent (?b ` {..<2})"
2.505 - by (simp add: * basis_complex_def independent_empty independent_insert)
2.506 - ultimately show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
2.507 - by (auto intro!: exI[of _ 2] inj_onI simp: basis_complex_def split: split_if_asm)
2.508 +lemma DIM_complex[simp]: "DIM(complex) = 2"
2.509 + by (rule dimension_complex_def)
2.510 +
2.511 +section {* Products Spaces *}
2.512 +
2.513 +instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
2.514 +begin
2.515 +
2.516 +definition
2.517 + "dimension (t::('a \<times> 'b) itself) = DIM('a) + DIM('b)"
2.518 +
2.519 +definition
2.520 + "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
2.521 +
2.522 +lemma all_less_sum:
2.523 + fixes m n :: nat
2.524 + shows "(\<forall>i<(m + n). P i) \<longleftrightarrow> (\<forall>i<m. P i) \<and> (\<forall>i<n. P (m + i))"
2.525 + by (induct n, simp, simp add: all_less_Suc)
2.526 +
2.527 +instance proof
2.528 + show "0 < DIM('a \<times> 'b)"
2.529 + unfolding dimension_prod_def by (intro add_pos_pos DIM_positive)
2.530 +next
2.531 + fix i :: nat
2.532 + assume "DIM('a \<times> 'b) \<le> i" thus "basis i = (0::'a \<times> 'b)"
2.533 + unfolding dimension_prod_def basis_prod_def zero_prod_def
2.534 + by simp
2.535 +next
2.536 + show "\<forall>i<DIM('a \<times> 'b). \<forall>j<DIM('a \<times> 'b).
2.537 + inner (basis i::'a \<times> 'b) (basis j) = (if i = j then 1 else 0)"
2.538 + unfolding dimension_prod_def basis_prod_def inner_prod_def
2.539 + unfolding all_less_sum prod_eq_iff
2.540 + by (simp add: basis_orthonormal)
2.541 +next
2.542 + fix x :: "'a \<times> 'b"
2.543 + show "(\<forall>i<DIM('a \<times> 'b). inner (basis i) x = 0) \<longleftrightarrow> x = 0"
2.544 + unfolding dimension_prod_def basis_prod_def inner_prod_def
2.545 + unfolding all_less_sum prod_eq_iff
2.546 + by (simp add: euclidean_all_zero)
2.547 qed
2.548 +
2.549 end
2.550
2.551 -lemma DIM_complex[simp]: "DIM(complex) = 2"
2.552 - by (rule dimension_eq) (auto simp: basis_complex_def)
2.553 -
2.554 -instance complex :: euclidean_space
2.555 - proof qed (auto simp add: basis_complex_def inner_complex_def)
2.556 -
2.557 -section {* Products Spaces *}
2.558 -
2.559 -instantiation prod :: (real_basis, real_basis) real_basis
2.560 -begin
2.561 -
2.562 -definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
2.563 -
2.564 -instance
2.565 -proof
2.566 - let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
2.567 - let ?b_a = "basis :: nat \<Rightarrow> 'a"
2.568 - let ?b_b = "basis :: nat \<Rightarrow> 'b"
2.569 -
2.570 - note image_range =
2.571 - image_add_atLeastLessThan[symmetric, of 0 "DIM('a)" "DIM('b)", simplified]
2.572 -
2.573 - have split_range:
2.574 - "{..<DIM('b) + DIM('a)} = {..<DIM('a)} \<union> {DIM('a)..<DIM('b) + DIM('a)}"
2.575 - by auto
2.576 - have *: "?b ` {DIM('a)..<DIM('b) + DIM('a)} = {0} \<times> (?b_b ` {..<DIM('b)})"
2.577 - "?b ` {..<DIM('a)} = (?b_a ` {..<DIM('a)}) \<times> {0}"
2.578 - unfolding image_range image_image basis_prod_def_raw range_basis
2.579 - by (auto simp: zero_prod_def basis_eq_0_iff)
2.580 - hence b_split:
2.581 - "?b ` {..<DIM('b) + DIM('a)} = (?b_a ` {..<DIM('a)}) \<times> {0} \<union> {0} \<times> (?b_b ` {..<DIM('b)})" (is "_ = ?prod")
2.582 - by (subst split_range) (simp add: image_Un)
2.583 -
2.584 - have b_0: "?b ` {DIM('b) + DIM('a)..} = {0}" unfolding basis_prod_def_raw
2.585 - by (auto simp: zero_prod_def image_iff basis_eq_0_iff elim!: ballE[of _ _ "DIM('a) + DIM('b)"])
2.586 -
2.587 - have split_UNIV:
2.588 - "UNIV = {..<DIM('b) + DIM('a)} \<union> {DIM('b)+DIM('a)..}"
2.589 - by auto
2.590 -
2.591 - have range_b: "range ?b = ?prod \<union> {0}"
2.592 - by (subst split_UNIV) (simp add: image_Un b_split b_0)
2.593 -
2.594 - have prod: "\<And>f A B. setsum f (A \<times> B) = (\<Sum>a\<in>A. \<Sum>b\<in>B. f (a, b))"
2.595 - by (simp add: setsum_cartesian_product)
2.596 -
2.597 - show "span (range ?b) = UNIV"
2.598 - unfolding span_explicit range_b
2.599 - proof safe
2.600 - fix a::'a and b::'b
2.601 - from in_span_basis[of a] in_span_basis[of b]
2.602 - obtain Sa ua Sb ub where span:
2.603 - "finite Sa" "Sa \<subseteq> basis ` {..<DIM('a)}" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)"
2.604 - "finite Sb" "Sb \<subseteq> basis ` {..<DIM('b)}" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)"
2.605 - unfolding span_explicit by auto
2.606 -
2.607 - let ?S = "((Sa - {0}) \<times> {0} \<union> {0} \<times> (Sb - {0}))"
2.608 - have *:
2.609 - "?S \<inter> {v. fst v = 0} \<inter> {v. snd v = 0} = {}"
2.610 - "?S \<inter> - {v. fst v = 0} \<inter> {v. snd v = 0} = (Sa - {0}) \<times> {0}"
2.611 - "?S \<inter> {v. fst v = 0} \<inter> - {v. snd v = 0} = {0} \<times> (Sb - {0})"
2.612 - by (auto simp: zero_prod_def)
2.613 - show "\<exists>S u. finite S \<and> S \<subseteq> ?prod \<union> {0} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = (a, b)"
2.614 - apply (rule exI[of _ ?S])
2.615 - apply (rule exI[of _ "\<lambda>(v, w). (if w = 0 then ua v else 0) + (if v = 0 then ub w else 0)"])
2.616 - using span
2.617 - apply (simp add: prod_case_unfold setsum_addf if_distrib cond_application_beta setsum_cases prod *)
2.618 - by (auto simp add: setsum_prod intro!: setsum_mono_zero_cong_left)
2.619 - qed simp
2.620 -
2.621 - show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
2.622 - apply (rule exI[of _ "DIM('b) + DIM('a)"]) unfolding b_0
2.623 - proof (safe intro!: DIM_positive del: notI)
2.624 - show inj_on: "inj_on ?b {..<DIM('b) + DIM('a)}" unfolding split_range
2.625 - using inj_on_iff[OF basis_inj[where 'a='a]] inj_on_iff[OF basis_inj[where 'a='b]]
2.626 - by (auto intro!: inj_onI simp: basis_prod_def basis_eq_0_iff)
2.627 -
2.628 - show "independent (?b ` {..<DIM('b) + DIM('a)})"
2.629 - unfolding independent_eq_inj_on[OF inj_on]
2.630 - proof safe
2.631 - fix i u assume i_upper: "i < DIM('b) + DIM('a)" and
2.632 - "(\<Sum>j\<in>{..<DIM('b) + DIM('a)} - {i}. u (?b j) *\<^sub>R ?b j) = ?b i" (is "?SUM = _")
2.633 - let ?left = "{..<DIM('a)}" and ?right = "{DIM('a)..<DIM('b) + DIM('a)}"
2.634 - show False
2.635 - proof cases
2.636 - assume "i < DIM('a)"
2.637 - hence "(basis i, 0) = ?SUM" unfolding `?SUM = ?b i` unfolding basis_prod_def by auto
2.638 - also have "\<dots> = (\<Sum>j\<in>?left - {i}. u (?b j) *\<^sub>R ?b j) +
2.639 - (\<Sum>j\<in>?right. u (?b j) *\<^sub>R ?b j)"
2.640 - using `i < DIM('a)` by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
2.641 - also have "\<dots> = (\<Sum>j\<in>?left - {i}. u (?b_a j, 0) *\<^sub>R (?b_a j, 0)) +
2.642 - (\<Sum>j\<in>?right. u (0, ?b_b (j-DIM('a))) *\<^sub>R (0, ?b_b (j-DIM('a))))"
2.643 - unfolding basis_prod_def by auto
2.644 - finally have "basis i = (\<Sum>j\<in>?left - {i}. u (?b_a j, 0) *\<^sub>R ?b_a j)"
2.645 - by (simp add: setsum_prod)
2.646 - moreover
2.647 - note independent_basis[where 'a='a, unfolded independent_eq_inj_on[OF basis_inj]]
2.648 - note this[rule_format, of i "\<lambda>v. u (v, 0)"]
2.649 - ultimately show False using `i < DIM('a)` by auto
2.650 - next
2.651 - let ?i = "i - DIM('a)"
2.652 - assume not: "\<not> i < DIM('a)" hence "DIM('a) \<le> i" by auto
2.653 - hence "?i < DIM('b)" using `i < DIM('b) + DIM('a)` by auto
2.654 -
2.655 - have inj_on: "inj_on (\<lambda>j. j - DIM('a)) {DIM('a)..<DIM('b) + DIM('a)}"
2.656 - by (auto intro!: inj_onI)
2.657 - with i_upper not have *: "{..<DIM('b)} - {?i} = (\<lambda>j. j-DIM('a))`(?right - {i})"
2.658 - by (auto simp: inj_on_image_set_diff image_minus_const_atLeastLessThan_nat)
2.659 -
2.660 - have "(0, basis ?i) = ?SUM" unfolding `?SUM = ?b i`
2.661 - unfolding basis_prod_def using not `?i < DIM('b)` by auto
2.662 - also have "\<dots> = (\<Sum>j\<in>?left. u (?b j) *\<^sub>R ?b j) +
2.663 - (\<Sum>j\<in>?right - {i}. u (?b j) *\<^sub>R ?b j)"
2.664 - using not by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
2.665 - also have "\<dots> = (\<Sum>j\<in>?left. u (?b_a j, 0) *\<^sub>R (?b_a j, 0)) +
2.666 - (\<Sum>j\<in>?right - {i}. u (0, ?b_b (j-DIM('a))) *\<^sub>R (0, ?b_b (j-DIM('a))))"
2.667 - unfolding basis_prod_def by auto
2.668 - finally have "basis ?i = (\<Sum>j\<in>{..<DIM('b)} - {?i}. u (0, ?b_b j) *\<^sub>R ?b_b j)"
2.669 - unfolding *
2.670 - by (subst setsum_reindex[OF inj_on[THEN subset_inj_on]])
2.671 - (auto simp: setsum_prod)
2.672 - moreover
2.673 - note independent_basis[where 'a='b, unfolded independent_eq_inj_on[OF basis_inj]]
2.674 - note this[rule_format, of ?i "\<lambda>v. u (0, v)"]
2.675 - ultimately show False using `?i < DIM('b)` by auto
2.676 - qed
2.677 - qed
2.678 - qed
2.679 -qed
2.680 -end
2.681 -
2.682 -lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::real_basis) + DIM('a::real_basis)"
2.683 - by (rule dimension_eq) (auto simp: basis_prod_def zero_prod_def basis_eq_0_iff)
2.684 -
2.685 -instance prod :: (euclidean_space, euclidean_space) euclidean_space
2.686 -proof (default, safe)
2.687 - let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
2.688 - fix i j assume "i < DIM('a \<times> 'b)" "j < DIM('a \<times> 'b)"
2.689 - thus "?b i \<bullet> ?b j = (if i = j then 1 else 0)"
2.690 - unfolding basis_prod_def by (auto simp: dot_basis)
2.691 -qed
2.692 +lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)"
2.693 + (* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *)
2.694 + unfolding dimension_prod_def by (rule add_commute)
2.695
2.696 instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
2.697 begin
3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 09 13:09:35 2011 -0700
3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 10 00:29:31 2011 -0700
3.3 @@ -473,7 +473,7 @@
3.4 using islimpt_UNIV [of x]
3.5 by (simp add: islimpt_approachable)
3.6
3.7 -instance real_basis_with_inner \<subseteq> perfect_space
3.8 +instance euclidean_space \<subseteq> perfect_space
3.9 proof
3.10 fix x :: 'a
3.11 { fix e :: real assume "0 < e"