simplified definition of class euclidean_space;
removed classes real_basis and real_basis_with_inner
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Tue Aug 09 13:09:35 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 10 00:29:31 2011 -0700
@@ -355,9 +355,11 @@
lemma \<pi>_inj_on: "inj_on (\<pi>::nat\<Rightarrow>'n::finite) {..<CARD('n)}"
using bij_betw_pi[where 'n='n] by (simp add: bij_betw_def)
-instantiation cart :: (real_basis,finite) real_basis
+instantiation cart :: (euclidean_space, finite) euclidean_space
begin
+definition "dimension (t :: ('a ^ 'b) itself) = CARD('b) * DIM('a)"
+
definition "(basis i::'a^'b) =
(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)
@@ -417,133 +419,84 @@
finally show ?thesis by simp
qed
-instance
-proof
- let ?b = "basis :: nat \<Rightarrow> 'a^'b"
- let ?b' = "basis :: nat \<Rightarrow> 'a"
+lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
+ by (rule dimension_cart_def)
- have setsum_basis:
- "\<And>f. (\<Sum>x\<in>range basis. f (x::'a)) = f 0 + (\<Sum>i<DIM('a). f (basis i))"
- unfolding range_basis apply (subst setsum.insert)
- by (auto simp: basis_eq_0_iff setsum.insert setsum_reindex[OF basis_inj])
+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
- have inj: "inj_on ?b {..<CARD('b)*DIM('a)}"
- by (auto intro!: inj_onI elim!: split_CARD_DIM split: split_if_asm
- simp add: Cart_eq basis_eq_pi' all_conj_distrib basis_neq_0
- inj_on_iff[OF basis_inj])
- moreover
- hence indep: "independent (?b ` {..<CARD('b) * DIM('a)})"
- proof (rule independent_eq_inj_on[THEN iffD2], safe elim!: split_CARD_DIM del: notI)
- fix j and i :: 'b and u :: "'a^'b \<Rightarrow> real" assume "j < DIM('a)"
- let ?x = "j + \<pi>' i * DIM('a)"
- show "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) \<noteq> ?b ?x"
- unfolding Cart_eq not_all
- proof
- have "(\<lambda>j. j + \<pi>' i*DIM('a))`({..<DIM('a)}-{j}) =
- {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)} - {?x}"(is "?S = ?I - _")
- proof safe
- fix y assume "y \<in> ?I"
- moreover def k \<equiv> "y - \<pi>' i*DIM('a)"
- ultimately have "k < DIM('a)" and "y = k + \<pi>' i * DIM('a)" by auto
- moreover assume "y \<notin> ?S"
- ultimately show "y = j + \<pi>' i * DIM('a)" by auto
- qed auto
+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
- have "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) $ i =
- (\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k $ i)" by simp
- also have "\<dots> = (\<Sum>k\<in>?S. u(?b k) *\<^sub>R ?b k $ i)"
- unfolding `?S = ?I - {?x}`
- proof (safe intro!: setsum_mono_zero_cong_right)
- fix y assume "y \<in> {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)}"
- moreover have "Suc (\<pi>' i) * DIM('a) \<le> CARD('b) * DIM('a)"
- unfolding mult_le_cancel2 using pi'_range[of i] by simp
- ultimately show "y < CARD('b) * DIM('a)" by simp
- next
- fix y assume "y < CARD('b) * DIM('a)"
- with split_CARD_DIM guess l k . note y = this
- moreover assume "u (?b y) *\<^sub>R ?b y $ i \<noteq> 0"
- ultimately show "y \<in> {\<pi>' i*DIM('a)..<Suc (\<pi>' i) * DIM('a)}"
- by (auto simp: basis_eq_pi' split: split_if_asm)
- qed simp
- also have "\<dots> = (\<Sum>k\<in>{..<DIM('a)} - {j}. u (?b (k + \<pi>' i*DIM('a))) *\<^sub>R (?b' k))"
- by (subst setsum_reindex) (auto simp: basis_eq_pi' intro!: inj_onI)
- also have "\<dots> \<noteq> ?b ?x $ i"
- proof -
- note independent_eq_inj_on[THEN iffD1, OF basis_inj independent_basis, rule_format]
- note this[of j "\<lambda>v. u (\<chi> ka::'b. if ka = i then v else (0\<Colon>'a))"]
- thus ?thesis by (simp add: `j < DIM('a)` basis_eq pi'_range)
- qed
- finally show "(\<Sum>k\<in>{..<CARD('b) * DIM('a)} - {?x}. u(?b k) *\<^sub>R ?b k) $ i \<noteq> ?b ?x $ i" .
- qed
- qed
- ultimately
- show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
- by (auto intro!: exI[of _ "CARD('b) * DIM('a)"] simp: basis_cart_def)
-
- from indep have exclude_0: "0 \<notin> ?b ` {..<CARD('b) * DIM('a)}"
- using dependent_0[of "?b ` {..<CARD('b) * DIM('a)}"] by blast
-
- show "span (range ?b) = UNIV"
- proof -
- { fix x :: "'a^'b"
- let "?if i y" = "(\<chi> k::'b. if k = i then ?b' y else (0\<Colon>'a))"
- have The_if: "\<And>i j. j < DIM('a) \<Longrightarrow> (THE k. (?if i j) $ k \<noteq> 0) = i"
- by (rule the_equality) (simp_all split: split_if_asm add: basis_neq_0)
- { fix x :: 'a
- have "x \<in> span (range basis)"
- using span_basis by (auto simp: range_basis)
- hence "\<exists>u. (\<Sum>x<DIM('a). u (?b' x) *\<^sub>R ?b' x) = x"
- by (subst (asm) span_finite) (auto simp: setsum_basis) }
- hence "\<forall>i. \<exists>u. (\<Sum>x<DIM('a). u (?b' x) *\<^sub>R ?b' x) = i" by auto
- then obtain u where u: "\<forall>i. (\<Sum>x<DIM('a). u i (?b' x) *\<^sub>R ?b' x) = i"
- by (auto dest: choice)
- have "\<exists>u. \<forall>i. (\<Sum>j<DIM('a). u (?if i j) *\<^sub>R ?b' j) = x $ i"
- apply (rule exI[of _ "\<lambda>v. let i = (THE i. v$i \<noteq> 0) in u (x$i) (v$i)"])
- using The_if u by simp }
- moreover
- have "\<And>i::'b. {..<CARD('b)} \<inter> {x. i = \<pi> x} = {\<pi>' i}"
- using pi'_range[where 'n='b] by auto
- moreover
- have "range ?b = {0} \<union> ?b ` {..<CARD('b) * DIM('a)}"
- by (auto simp: image_def basis_cart_def)
- ultimately
- show ?thesis
- by (auto simp add: Cart_eq setsum_reindex[OF inj] range_basis
- setsum_mult_product basis_eq if_distrib setsum_cases span_finite
- setsum_reindex[OF basis_inj])
- qed
+instance proof
+ show "0 < DIM('a ^ 'b)"
+ unfolding dimension_cart_def
+ by (intro mult_pos_pos zero_less_card_finite DIM_positive)
+next
+ fix i :: nat
+ assume "DIM('a ^ 'b) \<le> i" thus "basis i = (0::'a^'b)"
+ unfolding dimension_cart_def basis_cart_def
+ by simp
+next
+ show "\<forall>i<DIM('a ^ 'b). \<forall>j<DIM('a ^ 'b).
+ (basis i :: 'a ^ 'b) \<bullet> basis j = (if i = j then 1 else 0)"
+ apply (simp add: inner_vector_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)
+ 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_vector_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: Cart_eq)
+ done
qed
end
-lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a::real_basis)"
-proof (safe intro!: dimension_eq elim!: split_times_into_modulo del: notI)
- fix i j assume *: "i < CARD('b)" "j < DIM('a)"
- hence A: "(i * DIM('a) + j) div DIM('a) = i"
- by (subst div_add1_eq) simp
- from * have B: "(i * DIM('a) + j) mod DIM('a) = j"
- unfolding mod_mult_self3 by simp
- show "basis (j + i * DIM('a)) \<noteq> (0::'a^'b)" unfolding basis_cart_def
- using * basis_finite[where 'a='a]
- linear_less_than_times[of i "CARD('b)" j "DIM('a)"]
- by (auto simp: A B field_simps Cart_eq basis_eq_0_iff)
-qed (auto simp: basis_cart_def)
-
lemma if_distr: "(if P then f else g) $ i = (if P then f $ i else g $ i)" by simp
lemma split_dimensions'[consumes 1]:
- assumes "k < DIM('a::real_basis^'b)"
- obtains i j where "i < CARD('b::finite)" and "j < DIM('a::real_basis)" and "k = j + i * DIM('a::real_basis)"
+ assumes "k < DIM('a::euclidean_space^'b)"
+ obtains i j where "i < CARD('b::finite)" and "j < DIM('a::euclidean_space)" and "k = j + i * DIM('a::euclidean_space)"
using split_times_into_modulo[OF assms[simplified]] .
lemma cart_euclidean_bound[intro]:
- assumes j:"j < DIM('a::{real_basis})"
- shows "j + \<pi>' (i::'b::finite) * DIM('a) < CARD('b) * DIM('a::real_basis)"
+ assumes j:"j < DIM('a::euclidean_space)"
+ shows "j + \<pi>' (i::'b::finite) * DIM('a) < CARD('b) * DIM('a::euclidean_space)"
using linear_less_than_times[OF pi'_range j, of i] .
-instance cart :: (real_basis_with_inner,finite) real_basis_with_inner ..
-
-lemma (in real_basis) forall_CARD_DIM:
+lemma (in euclidean_space) forall_CARD_DIM:
"(\<forall>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<forall>(i::'b::finite) j. j<DIM('a) \<longrightarrow> P (j + \<pi>' i * DIM('a)))"
(is "?l \<longleftrightarrow> ?r")
proof (safe elim!: split_times_into_modulo)
@@ -557,7 +510,7 @@
show "P (j + i * DIM('a))" by simp
qed
-lemma (in real_basis) exists_CARD_DIM:
+lemma (in euclidean_space) exists_CARD_DIM:
"(\<exists>i<CARD('b) * DIM('a). P i) \<longleftrightarrow> (\<exists>i::'b::finite. \<exists>j<DIM('a). P (j + \<pi>' i * DIM('a)))"
using forall_CARD_DIM[where 'b='b, of "\<lambda>x. \<not> P x"] by blast
@@ -572,7 +525,7 @@
lemmas cart_simps = forall_CARD_DIM exists_CARD_DIM forall_CARD exists_CARD
lemma cart_euclidean_nth[simp]:
- fixes x :: "('a::real_basis_with_inner, 'b::finite) cart"
+ fixes x :: "('a::euclidean_space, 'b::finite) cart"
assumes j:"j < DIM('a)"
shows "x $$ (j + \<pi>' i * DIM('a)) = x $ i $$ j"
unfolding euclidean_component_def inner_vector_def basis_eq_pi'[OF j] if_distrib cond_application_beta
@@ -606,22 +559,6 @@
thus "x = y \<and> i = j" using * by simp
qed simp
-instance cart :: (euclidean_space,finite) euclidean_space
-proof (default, safe elim!: split_dimensions')
- let ?b = "basis :: nat \<Rightarrow> 'a^'b"
- have if_distrib_op: "\<And>f P Q a b c d.
- f (if P then a else b) (if Q then c else d) =
- (if P then if Q then f a c else f a d else if Q then f b c else f b d)"
- by simp
-
- fix i j k l
- assume "i < CARD('b)" "k < CARD('b)" "j < DIM('a)" "l < DIM('a)"
- thus "?b (j + i * DIM('a)) \<bullet> ?b (l + k * DIM('a)) =
- (if j + i * DIM('a) = l + k * DIM('a) then 1 else 0)"
- using inj_on_iff[OF \<pi>_inj_on[where 'n='b], of k i]
- by (auto simp add: basis_eq inner_vector_def if_distrib_op[of inner] setsum_cases basis_orthonormal mult_split_eq)
-qed
-
instance cart :: (ordered_euclidean_space,finite) ordered_euclidean_space
proof
fix x y::"'a^'b"
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Aug 09 13:09:35 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Wed Aug 10 00:29:31 2011 -0700
@@ -1582,119 +1582,50 @@
subsection{* Euclidean Spaces as Typeclass*}
-class real_basis = real_vector +
+class euclidean_space = real_inner +
+ fixes dimension :: "'a itself \<Rightarrow> nat"
fixes basis :: "nat \<Rightarrow> 'a"
- assumes span_basis: "span (range basis) = UNIV"
- assumes dimension_exists: "\<exists>d>0.
- basis ` {d..} = {0} \<and>
- independent (basis ` {..<d}) \<and>
- inj_on basis {..<d}"
-
-definition (in real_basis) dimension :: "'a itself \<Rightarrow> nat" where
- "dimension x =
- (THE d. basis ` {d..} = {0} \<and> independent (basis ` {..<d}) \<and> inj_on basis {..<d})"
+ 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)"
syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
translations "DIM('t)" == "CONST dimension (TYPE('t))"
-lemma (in real_basis) dimensionI:
- assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0}; independent (basis ` {..<d});
- inj_on basis {..<d} \<rbrakk> \<Longrightarrow> P d"
- shows "P DIM('a)"
-proof -
- obtain d where "0 < d" and d: "basis ` {d..} = {0} \<and>
- independent (basis ` {..<d}) \<and> inj_on basis {..<d}" (is "?P d")
- using dimension_exists by auto
- show ?thesis unfolding dimension_def
- proof (rule theI2)
- fix d' assume "?P d'"
- with d have "basis d' = 0" "basis d = 0" and
- "d < d' \<Longrightarrow> basis d \<noteq> 0"
- "d' < d \<Longrightarrow> basis d' \<noteq> 0"
- using dependent_0 by auto
- thus "d' = d" by (cases rule: linorder_cases) auto
- moreover have "P d" using assms[of d] `0 < d` d by auto
- ultimately show "P d'" by simp
- next show "?P d" using `?P d` .
- qed
-qed
-
-lemma (in real_basis) dimension_eq:
- assumes "\<And>i. i < d \<Longrightarrow> basis i \<noteq> 0"
- assumes "\<And>i. d \<le> i \<Longrightarrow> basis i = 0"
- shows "DIM('a) = d"
-proof (rule dimensionI)
- let ?b = "basis :: nat \<Rightarrow> 'a"
- fix d' assume *: "?b ` {d'..} = {0}" "independent (?b ` {..<d'})"
- show "d' = d"
- proof (cases rule: linorder_cases)
- assume "d' < d" hence "basis d' \<noteq> 0" using assms by auto
- with * show ?thesis by auto
- next
- assume "d < d'" hence "basis d \<noteq> 0" using * dependent_0 by auto
- with assms(2) `d < d'` show ?thesis by auto
- qed
+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))")
+ case False
+ hence "inner (basis i) (basis j) = 0" by auto
+ thus ?thesis using False by auto
+next
+ case True thus ?thesis using basis_orthonormal by auto
qed
-lemma (in real_basis)
- shows basis_finite: "basis ` {DIM('a)..} = {0}"
- and independent_basis: "independent (basis ` {..<DIM('a)})"
- and DIM_positive[intro]: "(DIM('a) :: nat) > 0"
- and basis_inj[simp, intro]: "inj_on basis {..<DIM('a)}"
- by (auto intro!: dimensionI)
-
-lemma (in real_basis) basis_eq_0_iff: "basis j = 0 \<longleftrightarrow> DIM('a) \<le> j"
-proof
- show "DIM('a) \<le> j \<Longrightarrow> basis j = 0" using basis_finite by auto
-next
- have "j < DIM('a) \<Longrightarrow> basis j \<noteq> 0"
- using independent_basis by (auto intro!: dependent_0)
- thus "basis j = 0 \<Longrightarrow> DIM('a) \<le> j" unfolding not_le[symmetric] by blast
-qed
-
-lemma (in real_basis) range_basis:
- "range basis = insert 0 (basis ` {..<DIM('a)})"
+lemma (in euclidean_space) basis_eq_0_iff [simp]:
+ "basis i = 0 \<longleftrightarrow> DIM('a) \<le> i"
proof -
- have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto
- show ?thesis unfolding * image_Un basis_finite by auto
+ have "inner (basis i) (basis i) = 0 \<longleftrightarrow> DIM('a) \<le> i"
+ by (simp add: dot_basis)
+ thus ?thesis by simp
qed
-lemma (in real_basis) range_basis_finite[intro]:
- "finite (range basis)"
- unfolding range_basis by auto
-
-lemma (in real_basis) basis_neq_0[intro]:
- assumes "i<DIM('a)" shows "(basis i) \<noteq> 0"
-proof(rule ccontr) assume "\<not> basis i \<noteq> (0::'a)"
- hence "(0::'a) \<in> basis ` {..<DIM('a)}" using assms by auto
- from dependent_0[OF this] show False using independent_basis by auto
-qed
-
-lemma (in real_basis) basis_zero[simp]:
- assumes"i \<ge> DIM('a)" shows "basis i = 0"
-proof-
- have "(basis i::'a) \<in> basis ` {DIM('a)..}" using assms by auto
- thus ?thesis unfolding basis_finite by fastsimp
-qed
-
-lemma basis_representation:
- "\<exists>u. x = (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R (v\<Colon>'a\<Colon>real_basis))"
-proof -
- have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]]
- have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x"
- unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto
- thus ?thesis by fastsimp
-qed
-
-lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = UNIV"
- apply(subst span_basis[symmetric]) unfolding range_basis by auto
-
-lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::real_basis)}) = DIM('a)"
- apply(subst card_image) using basis_inj by auto
-
-lemma in_span_basis: "(x::'a::real_basis) \<in> span (basis ` {..<DIM('a)})"
- unfolding span_basis' ..
+lemma (in euclidean_space) norm_basis [simp]:
+ "norm (basis i) = (if i < DIM('a) then 1 else 0)"
+ unfolding norm_eq_sqrt_inner dot_basis by simp
+
+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}"
@@ -1708,56 +1639,98 @@
by (auto simp: eq setsum_reindex[OF inj])
qed
-class real_basis_with_inner = real_inner + real_basis
-begin
-
-definition euclidean_component (infixl "$$" 90) where
- "x $$ i = inner (basis i) x"
-
-definition Chi (binder "\<chi>\<chi> " 10) where
- "(\<chi>\<chi> i. f i) = (\<Sum>i<DIM('a). f i *\<^sub>R basis i)"
-
-lemma basis_at_neq_0[intro]:
+lemma independent_basis:
+ "independent (basis ` {..<DIM('a)} :: 'a::euclidean_space set)"
+ unfolding independent_eq_inj_on [OF basis_inj]
+ apply clarify
+ apply (drule_tac f="inner (basis a)" in arg_cong)
+ apply (simp add: inner_right.setsum dot_basis)
+ done
+
+lemma dimensionI:
+ assumes "\<And>d. \<lbrakk> 0 < d; basis ` {d..} = {0::'a::euclidean_space};
+ independent (basis ` {..<d} :: 'a set);
+ inj_on (basis :: nat \<Rightarrow> 'a) {..<d} \<rbrakk> \<Longrightarrow> P d"
+ shows "P DIM('a::euclidean_space)"
+ using DIM_positive basis_finite independent_basis basis_inj
+ by (rule assms)
+
+lemma (in euclidean_space) dimension_eq:
+ assumes "\<And>i. i < d \<Longrightarrow> basis i \<noteq> 0"
+ assumes "\<And>i. d \<le> i \<Longrightarrow> basis i = 0"
+ shows "DIM('a) = d"
+proof (rule linorder_cases [of "DIM('a)" d])
+ assume "DIM('a) < d"
+ hence "basis DIM('a) \<noteq> 0" by (rule assms)
+ thus ?thesis by simp
+next
+ assume "d < DIM('a)"
+ hence "basis d \<noteq> 0" by simp
+ thus ?thesis by (simp add: assms)
+next
+ assume "DIM('a) = d" thus ?thesis .
+qed
+
+lemma (in euclidean_space) range_basis:
+ "range basis = insert 0 (basis ` {..<DIM('a)})"
+proof -
+ have *: "UNIV = {..<DIM('a)} \<union> {DIM('a)..}" by auto
+ show ?thesis unfolding * image_Un basis_finite by auto
+qed
+
+lemma (in euclidean_space) range_basis_finite[intro]:
+ "finite (range basis)"
+ unfolding range_basis by auto
+
+lemma (in euclidean_space) basis_neq_0 [intro]:
+ assumes "i<DIM('a)" shows "(basis i) \<noteq> 0"
+ using assms by simp
+
+subsubsection {* Projecting components *}
+
+definition (in euclidean_space) euclidean_component (infixl "$$" 90)
+ where "x $$ i = inner (basis i) x"
+
+lemma bounded_linear_euclidean_component:
+ "bounded_linear (\<lambda>x. euclidean_component x i)"
+ unfolding euclidean_component_def
+ by (rule inner.bounded_linear_right)
+
+interpretation euclidean_component:
+ bounded_linear "\<lambda>x. euclidean_component x i"
+ by (rule bounded_linear_euclidean_component)
+
+lemma euclidean_eqI:
+ fixes x y :: "'a::euclidean_space"
+ assumes "\<And>i. i < DIM('a) \<Longrightarrow> x $$ i = y $$ i" shows "x = y"
+proof -
+ from assms have "\<forall>i<DIM('a). (x - y) $$ i = 0"
+ by (simp add: euclidean_component.diff)
+ then show "x = y"
+ unfolding euclidean_component_def euclidean_all_zero by simp
+qed
+
+lemma euclidean_eq:
+ fixes x y :: "'a::euclidean_space"
+ shows "x = y \<longleftrightarrow> (\<forall>i<DIM('a). x $$ i = y $$ i)"
+ by (auto intro: euclidean_eqI)
+
+lemma (in euclidean_space) basis_component [simp]:
+ "basis i $$ j = (if i = j \<and> i < DIM('a) then 1 else 0)"
+ unfolding euclidean_component_def dot_basis by auto
+
+lemma (in euclidean_space) basis_at_neq_0 [intro]:
"i < DIM('a) \<Longrightarrow> basis i $$ i \<noteq> 0"
- unfolding euclidean_component_def by (auto intro!: basis_neq_0)
-
-lemma euclidean_component_ge[simp]:
+ by simp
+
+lemma (in euclidean_space) euclidean_component_ge [simp]:
assumes "i \<ge> DIM('a)" shows "x $$ i = 0"
- unfolding euclidean_component_def basis_zero[OF assms] by auto
+ unfolding euclidean_component_def basis_zero[OF assms] by simp
lemma euclidean_scaleR:
shows "(a *\<^sub>R x) $$ i = a * (x$$i)"
unfolding euclidean_component_def by auto
-end
-
-interpretation euclidean_component:
- bounded_linear "\<lambda>x. euclidean_component x i"
- unfolding euclidean_component_def
- by (rule inner.bounded_linear_right)
-
-subsection{* Euclidean Spaces as Typeclass *}
-
-class euclidean_space = real_basis_with_inner +
- assumes basis_orthonormal: "\<forall>i<DIM('a). \<forall>j<DIM('a).
- inner (basis i) (basis j) = (if i = j then 1 else 0)"
-
-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))")
- case False
- hence "basis i = 0 \<or> basis j = 0"
- using basis_finite by fastsimp
- hence "inner (basis i) (basis j) = 0" by (rule disjE) simp_all
- thus ?thesis using False by auto
-next
- case True thus ?thesis using basis_orthonormal by auto
-qed
-
-lemma (in euclidean_space) basis_component[simp]:
- "basis i $$ j = (if i = j \<and> i < DIM('a) then 1 else 0)"
- unfolding euclidean_component_def dot_basis by auto
-
lemmas euclidean_simps =
euclidean_component.add
euclidean_component.diff
@@ -1767,34 +1740,22 @@
basis_component
lemma euclidean_representation:
- "(x\<Colon>'a\<Colon>euclidean_space) = (\<Sum>i\<in>{..<DIM('a)}. (x$$i) *\<^sub>R basis i)"
-proof-
- from basis_representation[of x] guess u ..
- hence *:"x = (\<Sum>i\<in>{..<DIM('a)}. u (basis i) *\<^sub>R (basis i))"
- by (simp add: setsum_reindex)
- show ?thesis apply(subst *)
- proof(safe intro!: setsum_cong2)
- fix i assume i: "i < DIM('a)"
- hence "x$$i = (\<Sum>x<DIM('a). (if i = x then u (basis x) else 0))"
- by (auto simp: euclidean_simps * intro!: setsum_cong)
- also have "... = u (basis i)" using i by (auto simp: setsum_cases)
- finally show "u (basis i) *\<^sub>R basis i = x $$ i *\<^sub>R basis i" by simp
- qed
-qed
-
-lemma euclidean_eq:
- fixes x y :: "'a\<Colon>euclidean_space"
- shows "x = y \<longleftrightarrow> (\<forall>i<DIM('a). x$$i = y$$i)" (is "?l = ?r")
-proof safe
- assume "\<forall>i<DIM('a). x $$ i = y $$ i"
- thus "x = y"
- by (subst (1 2) euclidean_representation) auto
-qed
-
-lemma euclidean_lambda_beta[simp]:
+ fixes x :: "'a::euclidean_space"
+ shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
+ apply (rule euclidean_eqI)
+ apply (simp add: euclidean_component.setsum euclidean_component.scaleR)
+ apply (simp add: if_distrib setsum_delta cong: if_cong)
+ done
+
+subsubsection {* Binder notation for vectors *}
+
+definition (in euclidean_space) Chi (binder "\<chi>\<chi> " 10) where
+ "(\<chi>\<chi> i. f i) = (\<Sum>i<DIM('a). f i *\<^sub>R basis i)"
+
+lemma euclidean_lambda_beta [simp]:
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = (if j < DIM('a) then f j else 0)"
- by (auto simp: euclidean_simps Chi_def if_distrib setsum_cases
- intro!: setsum_cong)
+ by (auto simp: euclidean_component.setsum euclidean_component.scaleR
+ Chi_def if_distrib setsum_cases intro!: setsum_cong)
lemma euclidean_lambda_beta':
"j < DIM('a) \<Longrightarrow> ((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ j = f j"
@@ -1805,7 +1766,7 @@
lemma euclidean_beta_reduce[simp]:
"(\<chi>\<chi> i. x $$ i) = (x::'a::euclidean_space)"
- by (subst euclidean_eq) (simp add: euclidean_lambda_beta)
+ by (simp add: euclidean_eq)
lemma euclidean_lambda_beta_0[simp]:
"((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ 0 = f 0"
@@ -1823,6 +1784,34 @@
finally show ?thesis .
qed
+lemma span_basis: "span (range basis) = (UNIV :: 'a::euclidean_space set)"
+proof -
+ { fix x :: 'a
+ have "(\<Sum>i<DIM('a). (x $$ i) *\<^sub>R basis i) \<in> span (range basis :: 'a set)"
+ by (simp add: span_setsum span_mul span_superset)
+ hence "x \<in> span (range basis)"
+ by (simp only: euclidean_representation [symmetric])
+ } thus ?thesis by auto
+qed
+
+lemma basis_representation:
+ "\<exists>u. x = (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R (v\<Colon>'a\<Colon>euclidean_space))"
+proof -
+ have "x\<in>UNIV" by auto from this[unfolded span_basis[THEN sym]]
+ have "\<exists>u. (\<Sum>v\<in>basis ` {..<DIM('a)}. u v *\<^sub>R v) = x"
+ unfolding range_basis span_insert_0 apply(subst (asm) span_finite) by auto
+ thus ?thesis by fastsimp
+qed
+
+lemma span_basis'[simp]:"span ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = UNIV"
+ apply(subst span_basis[symmetric]) unfolding range_basis by auto
+
+lemma card_basis[simp]:"card ((basis::nat=>'a) ` {..<DIM('a::euclidean_space)}) = DIM('a)"
+ apply(subst card_image) using basis_inj by auto
+
+lemma in_span_basis: "(x::'a::euclidean_space) \<in> span (basis ` {..<DIM('a)})"
+ unfolding span_basis' ..
+
lemma norm_basis[simp]:"norm (basis i::'a::euclidean_space) = (if i<DIM('a) then 1 else 0)"
unfolding norm_eq_sqrt_inner dot_basis by auto
@@ -3301,31 +3290,27 @@
subsection "Instantiate @{typ real} and @{typ complex} as typeclass @{text ordered_euclidean_space}."
-instantiation real :: real_basis_with_inner
+instantiation real :: euclidean_space
begin
-definition [simp]: "basis i = (if i = 0 then (1::real) else 0)"
+
+definition
+ "dimension (t::real itself) = 1"
+
+definition [simp]:
+ "basis i = (if i = 0 then 1 else (0::real))"
+
+lemma DIM_real [simp]: "DIM(real) = 1"
+ by (rule dimension_real_def)
+
+instance
+ by default simp+
+
+end
lemma basis_real_range: "basis ` {..<1} = {1::real}" by auto
-instance proof
- let ?b = "basis::nat \<Rightarrow> real"
-
- from basis_real_range have "independent (?b ` {..<1})" by auto
- thus "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
- by (auto intro!: exI[of _ 1] inj_onI)
-
- { fix x::real
- have "x \<in> span (range ?b)"
- using span_mul[of 1 "range ?b" x] span_clauses(1)[of 1 "range ?b"]
- by auto }
- thus "span (range ?b) = UNIV" by auto
-qed
-end
-
-lemma DIM_real[simp]: "DIM(real) = 1"
- by (rule dimension_eq) (auto simp: basis_real_def)
-
-instance real::ordered_euclidean_space proof qed(auto simp add:euclidean_component_def)
+instance real::ordered_euclidean_space
+ by default (auto simp add: euclidean_component_def)
lemma Eucl_real_simps[simp]:
"(x::real) $$ 0 = x"
@@ -3335,177 +3320,89 @@
unfolding euclidean_lambda_beta'
unfolding euclidean_component_def by auto
-instantiation complex :: real_basis_with_inner
+instantiation complex :: euclidean_space
begin
-definition "basis i = (if i = 0 then 1 else if i = 1 then ii else 0)"
-
-lemma complex_basis[simp]:"basis 0 = (1::complex)" "basis 1 = ii" "basis (Suc 0) = 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
+
+end
+
+lemma complex_basis[simp]:
+ shows "basis 0 = (1::complex)" and "basis 1 = ii" and "basis (Suc 0) = ii"
unfolding basis_complex_def by auto
-instance
-proof
- let ?b = "basis::nat \<Rightarrow> complex"
- have [simp]: "(range ?b) = {0, basis 0, basis 1}"
- by (auto simp: basis_complex_def split: split_if_asm)
- { fix z::complex
- have "z \<in> span (range ?b)"
- by (auto simp: span_finite complex_equality
- intro!: exI[of _ "\<lambda>i. if i = 1 then Re z else if i = ii then Im z else 0"]) }
- thus "span (range ?b) = UNIV" by auto
-
- have "{..<2} = {0, 1::nat}" by auto
- hence *: "?b ` {..<2} = {1, ii}"
- by (auto simp add: basis_complex_def)
- moreover have "1 \<notin> span {\<i>}"
- by (simp add: span_finite complex_equality complex_scaleR_def)
- hence "independent (?b ` {..<2})"
- by (simp add: * basis_complex_def independent_empty independent_insert)
- ultimately show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
- by (auto intro!: exI[of _ 2] inj_onI simp: basis_complex_def split: split_if_asm)
-qed
-end
-
lemma DIM_complex[simp]: "DIM(complex) = 2"
- by (rule dimension_eq) (auto simp: basis_complex_def)
-
-instance complex :: euclidean_space
- proof qed (auto simp add: basis_complex_def inner_complex_def)
+ by (rule dimension_complex_def)
section {* Products Spaces *}
-instantiation prod :: (real_basis, real_basis) real_basis
+instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
begin
-definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))"
-
-instance
-proof
- let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
- let ?b_a = "basis :: nat \<Rightarrow> 'a"
- let ?b_b = "basis :: nat \<Rightarrow> 'b"
-
- note image_range =
- image_add_atLeastLessThan[symmetric, of 0 "DIM('a)" "DIM('b)", simplified]
-
- have split_range:
- "{..<DIM('b) + DIM('a)} = {..<DIM('a)} \<union> {DIM('a)..<DIM('b) + DIM('a)}"
- by auto
- have *: "?b ` {DIM('a)..<DIM('b) + DIM('a)} = {0} \<times> (?b_b ` {..<DIM('b)})"
- "?b ` {..<DIM('a)} = (?b_a ` {..<DIM('a)}) \<times> {0}"
- unfolding image_range image_image basis_prod_def_raw range_basis
- by (auto simp: zero_prod_def basis_eq_0_iff)
- hence b_split:
- "?b ` {..<DIM('b) + DIM('a)} = (?b_a ` {..<DIM('a)}) \<times> {0} \<union> {0} \<times> (?b_b ` {..<DIM('b)})" (is "_ = ?prod")
- by (subst split_range) (simp add: image_Un)
-
- have b_0: "?b ` {DIM('b) + DIM('a)..} = {0}" unfolding basis_prod_def_raw
- by (auto simp: zero_prod_def image_iff basis_eq_0_iff elim!: ballE[of _ _ "DIM('a) + DIM('b)"])
-
- have split_UNIV:
- "UNIV = {..<DIM('b) + DIM('a)} \<union> {DIM('b)+DIM('a)..}"
- by auto
-
- have range_b: "range ?b = ?prod \<union> {0}"
- by (subst split_UNIV) (simp add: image_Un b_split b_0)
-
- have prod: "\<And>f A B. setsum f (A \<times> B) = (\<Sum>a\<in>A. \<Sum>b\<in>B. f (a, b))"
- by (simp add: setsum_cartesian_product)
-
- show "span (range ?b) = UNIV"
- unfolding span_explicit range_b
- proof safe
- fix a::'a and b::'b
- from in_span_basis[of a] in_span_basis[of b]
- obtain Sa ua Sb ub where span:
- "finite Sa" "Sa \<subseteq> basis ` {..<DIM('a)}" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)"
- "finite Sb" "Sb \<subseteq> basis ` {..<DIM('b)}" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)"
- unfolding span_explicit by auto
-
- let ?S = "((Sa - {0}) \<times> {0} \<union> {0} \<times> (Sb - {0}))"
- have *:
- "?S \<inter> {v. fst v = 0} \<inter> {v. snd v = 0} = {}"
- "?S \<inter> - {v. fst v = 0} \<inter> {v. snd v = 0} = (Sa - {0}) \<times> {0}"
- "?S \<inter> {v. fst v = 0} \<inter> - {v. snd v = 0} = {0} \<times> (Sb - {0})"
- by (auto simp: zero_prod_def)
- show "\<exists>S u. finite S \<and> S \<subseteq> ?prod \<union> {0} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = (a, b)"
- apply (rule exI[of _ ?S])
- apply (rule exI[of _ "\<lambda>(v, w). (if w = 0 then ua v else 0) + (if v = 0 then ub w else 0)"])
- using span
- apply (simp add: prod_case_unfold setsum_addf if_distrib cond_application_beta setsum_cases prod *)
- by (auto simp add: setsum_prod intro!: setsum_mono_zero_cong_left)
- qed simp
-
- show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}"
- apply (rule exI[of _ "DIM('b) + DIM('a)"]) unfolding b_0
- proof (safe intro!: DIM_positive del: notI)
- show inj_on: "inj_on ?b {..<DIM('b) + DIM('a)}" unfolding split_range
- using inj_on_iff[OF basis_inj[where 'a='a]] inj_on_iff[OF basis_inj[where 'a='b]]
- by (auto intro!: inj_onI simp: basis_prod_def basis_eq_0_iff)
-
- show "independent (?b ` {..<DIM('b) + DIM('a)})"
- unfolding independent_eq_inj_on[OF inj_on]
- proof safe
- fix i u assume i_upper: "i < DIM('b) + DIM('a)" and
- "(\<Sum>j\<in>{..<DIM('b) + DIM('a)} - {i}. u (?b j) *\<^sub>R ?b j) = ?b i" (is "?SUM = _")
- let ?left = "{..<DIM('a)}" and ?right = "{DIM('a)..<DIM('b) + DIM('a)}"
- show False
- proof cases
- assume "i < DIM('a)"
- hence "(basis i, 0) = ?SUM" unfolding `?SUM = ?b i` unfolding basis_prod_def by auto
- also have "\<dots> = (\<Sum>j\<in>?left - {i}. u (?b j) *\<^sub>R ?b j) +
- (\<Sum>j\<in>?right. u (?b j) *\<^sub>R ?b j)"
- using `i < DIM('a)` by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
- also have "\<dots> = (\<Sum>j\<in>?left - {i}. u (?b_a j, 0) *\<^sub>R (?b_a j, 0)) +
- (\<Sum>j\<in>?right. u (0, ?b_b (j-DIM('a))) *\<^sub>R (0, ?b_b (j-DIM('a))))"
- unfolding basis_prod_def by auto
- finally have "basis i = (\<Sum>j\<in>?left - {i}. u (?b_a j, 0) *\<^sub>R ?b_a j)"
- by (simp add: setsum_prod)
- moreover
- note independent_basis[where 'a='a, unfolded independent_eq_inj_on[OF basis_inj]]
- note this[rule_format, of i "\<lambda>v. u (v, 0)"]
- ultimately show False using `i < DIM('a)` by auto
- next
- let ?i = "i - DIM('a)"
- assume not: "\<not> i < DIM('a)" hence "DIM('a) \<le> i" by auto
- hence "?i < DIM('b)" using `i < DIM('b) + DIM('a)` by auto
-
- have inj_on: "inj_on (\<lambda>j. j - DIM('a)) {DIM('a)..<DIM('b) + DIM('a)}"
- by (auto intro!: inj_onI)
- with i_upper not have *: "{..<DIM('b)} - {?i} = (\<lambda>j. j-DIM('a))`(?right - {i})"
- by (auto simp: inj_on_image_set_diff image_minus_const_atLeastLessThan_nat)
-
- have "(0, basis ?i) = ?SUM" unfolding `?SUM = ?b i`
- unfolding basis_prod_def using not `?i < DIM('b)` by auto
- also have "\<dots> = (\<Sum>j\<in>?left. u (?b j) *\<^sub>R ?b j) +
- (\<Sum>j\<in>?right - {i}. u (?b j) *\<^sub>R ?b j)"
- using not by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong)
- also have "\<dots> = (\<Sum>j\<in>?left. u (?b_a j, 0) *\<^sub>R (?b_a j, 0)) +
- (\<Sum>j\<in>?right - {i}. u (0, ?b_b (j-DIM('a))) *\<^sub>R (0, ?b_b (j-DIM('a))))"
- unfolding basis_prod_def by auto
- finally have "basis ?i = (\<Sum>j\<in>{..<DIM('b)} - {?i}. u (0, ?b_b j) *\<^sub>R ?b_b j)"
- unfolding *
- by (subst setsum_reindex[OF inj_on[THEN subset_inj_on]])
- (auto simp: setsum_prod)
- moreover
- note independent_basis[where 'a='b, unfolded independent_eq_inj_on[OF basis_inj]]
- note this[rule_format, of ?i "\<lambda>v. u (0, v)"]
- ultimately show False using `?i < DIM('b)` by auto
- qed
- qed
- qed
+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)
+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
+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)
+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)
qed
+
end
-lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::real_basis) + DIM('a::real_basis)"
- by (rule dimension_eq) (auto simp: basis_prod_def zero_prod_def basis_eq_0_iff)
-
-instance prod :: (euclidean_space, euclidean_space) euclidean_space
-proof (default, safe)
- let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b"
- fix i j assume "i < DIM('a \<times> 'b)" "j < DIM('a \<times> 'b)"
- thus "?b i \<bullet> ?b j = (if i = j then 1 else 0)"
- unfolding basis_prod_def by (auto simp: dot_basis)
-qed
+lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::euclidean_space) + DIM('a::euclidean_space)"
+ (* FIXME: why this orientation? Why not "DIM('a) + DIM('b)" ? *)
+ unfolding dimension_prod_def by (rule add_commute)
instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space
begin
--- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Tue Aug 09 13:09:35 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy Wed Aug 10 00:29:31 2011 -0700
@@ -473,7 +473,7 @@
using islimpt_UNIV [of x]
by (simp add: islimpt_approachable)
-instance real_basis_with_inner \<subseteq> perfect_space
+instance euclidean_space \<subseteq> perfect_space
proof
fix x :: 'a
{ fix e :: real assume "0 < e"