# HG changeset patch
# User huffman
# Date 1312961371 25200
# Node ID 286bd57858b9f40c45ee0feaa66a6c021b28ed48
# Parent  e6c6ca74d81beb38d2259323d2d51ea78a259210
simplified definition of class euclidean_space;
removed classes real_basis and real_basis_with_inner

diff -r e6c6ca74d81b -r 286bd57858b9 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- 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"
diff -r e6c6ca74d81b -r 286bd57858b9 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- 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
diff -r e6c6ca74d81b -r 286bd57858b9 src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy
--- 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"