diff -r 46be26e02456 -r 899c9c4e4a4c src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Dec 14 14:46:01 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Fri Dec 14 15:46:01 2012 +0100
@@ -23,24 +23,24 @@
   assumes euclidean_all_zero_iff:
     "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> (x = 0)"
 
-  -- "FIXME: make this a separate definition"
-  fixes dimension :: "'a itself \<Rightarrow> nat"
-  assumes dimension_def: "dimension TYPE('a) = card Basis"
-
-  -- "FIXME: eventually basis function can be removed"
-  fixes basis :: "nat \<Rightarrow> 'a"
-  assumes image_basis: "basis ` {..<dimension TYPE('a)} = Basis"
-  assumes basis_finite: "basis ` {dimension TYPE('a)..} = {0}"
+abbreviation dimension :: "('a::euclidean_space) itself \<Rightarrow> nat" where
+  "dimension TYPE('a) \<equiv> card (Basis :: 'a set)"
 
 syntax "_type_dimension" :: "type => nat" ("(1DIM/(1'(_')))")
 
 translations "DIM('t)" == "CONST dimension (TYPE('t))"
 
-lemma (in euclidean_space) norm_Basis: "u \<in> Basis \<Longrightarrow> norm u = 1"
+lemma (in euclidean_space) norm_Basis[simp]: "u \<in> Basis \<Longrightarrow> norm u = 1"
   unfolding norm_eq_sqrt_inner by (simp add: inner_Basis)
 
+lemma (in euclidean_space) inner_same_Basis[simp]: "u \<in> Basis \<Longrightarrow> inner u u = 1"
+  by (simp add: inner_Basis)
+
+lemma (in euclidean_space) inner_not_same_Basis: "u \<in> Basis \<Longrightarrow> v \<in> Basis \<Longrightarrow> u \<noteq> v \<Longrightarrow> inner u v = 0"
+  by (simp add: inner_Basis)
+
 lemma (in euclidean_space) sgn_Basis: "u \<in> Basis \<Longrightarrow> sgn u = u"
-  unfolding sgn_div_norm by (simp add: norm_Basis scaleR_one)
+  unfolding sgn_div_norm by (simp add: scaleR_one)
 
 lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
 proof
@@ -51,184 +51,45 @@
 lemma (in euclidean_space) nonzero_Basis: "u \<in> Basis \<Longrightarrow> u \<noteq> 0"
   by clarsimp
 
-text {* Lemmas related to @{text basis} function. *}
-
-lemma (in euclidean_space) euclidean_all_zero:
-  "(\<forall>i<DIM('a). inner (basis i) x = 0) \<longleftrightarrow> (x = 0)"
-  using euclidean_all_zero_iff [of x, folded image_basis]
-  unfolding ball_simps by (simp add: Ball_def inner_commute)
-
-lemma (in euclidean_space) basis_zero [simp]:
-  "DIM('a) \<le> i \<Longrightarrow> basis i = 0"
-  using basis_finite by auto
+lemma (in euclidean_space) SOME_Basis: "(SOME i. i \<in> Basis) \<in> Basis"
+  by (metis ex_in_conv nonempty_Basis someI_ex)
 
-lemma (in euclidean_space) DIM_positive [intro]: "0 < DIM('a)"
-  unfolding dimension_def by (simp add: card_gt_0_iff)
-
-lemma (in euclidean_space) basis_inj [simp, intro]: "inj_on basis {..<DIM('a)}"
-  by (simp add: inj_on_iff_eq_card image_basis dimension_def [symmetric])
-
-lemma (in euclidean_space) basis_in_Basis [simp]:
-  "basis i \<in> Basis \<longleftrightarrow> i < DIM('a)"
-  by (cases "i < DIM('a)", simp add: image_basis [symmetric], simp)
-
-lemma (in euclidean_space) Basis_elim:
-  assumes "u \<in> Basis" obtains i where "i < DIM('a)" and "u = basis i"
-  using assms unfolding image_basis [symmetric] by fast
+lemma (in euclidean_space) inner_setsum_left_Basis[simp]:
+    "b \<in> Basis \<Longrightarrow> inner (\<Sum>i\<in>Basis. f i *\<^sub>R i) b = f b"
+  by (simp add: inner_setsum_left inner_Basis if_distrib setsum_cases)
 
-lemma (in euclidean_space) basis_orthonormal:
-    "\<forall>i<DIM('a). \<forall>j<DIM('a).
-      inner (basis i) (basis j) = (if i = j then 1 else 0)"
-  apply clarify
-  apply (simp add: inner_Basis)
-  apply (simp add: basis_inj [unfolded inj_on_def])
-  done
-
-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 euclidean_space) basis_eq_0_iff [simp]:
-  "basis i = 0 \<longleftrightarrow> DIM('a) \<le> i"
+lemma (in euclidean_space) euclidean_eqI:
+  assumes b: "\<And>b. b \<in> Basis \<Longrightarrow> inner x b = inner y b" shows "x = y"
 proof -
-  have "inner (basis i) (basis i) = 0 \<longleftrightarrow> DIM('a) \<le> i"
-    by (simp add: dot_basis)
-  thus ?thesis by simp
+  from b have "\<forall>b\<in>Basis. inner (x - y) b = 0"
+    by (simp add: inner_diff_left)
+  then show "x = y"
+    by (simp add: euclidean_all_zero_iff)
 qed
 
-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_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 bounded_linear_inner_right)
-
-lemmas tendsto_euclidean_component [tendsto_intros] =
-  bounded_linear.tendsto [OF bounded_linear_euclidean_component]
-
-lemmas isCont_euclidean_component [simp] =
-  bounded_linear.isCont [OF bounded_linear_euclidean_component]
-
-lemma euclidean_component_zero [simp]: "0 $$ i = 0"
-  unfolding euclidean_component_def by (rule inner_zero_right)
-
-lemma euclidean_component_add [simp]: "(x + y) $$ i = x $$ i + y $$ i"
-  unfolding euclidean_component_def by (rule inner_add_right)
-
-lemma euclidean_component_diff [simp]: "(x - y) $$ i = x $$ i - y $$ i"
-  unfolding euclidean_component_def by (rule inner_diff_right)
-
-lemma euclidean_component_minus [simp]: "(- x) $$ i = - (x $$ i)"
-  unfolding euclidean_component_def by (rule inner_minus_right)
-
-lemma euclidean_component_scaleR [simp]: "(scaleR a x) $$ i = a * (x $$ i)"
-  unfolding euclidean_component_def by (rule inner_scaleR_right)
-
-lemma euclidean_component_setsum [simp]: "(\<Sum>x\<in>A. f x) $$ i = (\<Sum>x\<in>A. f x $$ i)"
-  unfolding euclidean_component_def by (rule inner_setsum_right)
-
-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
-  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)"
+lemma (in euclidean_space) euclidean_eq_iff:
+  "x = y \<longleftrightarrow> (\<forall>b\<in>Basis. inner x b = inner y b)"
   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"
-  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 simp
+lemma (in euclidean_space) euclidean_representation_setsum:
+  "(\<Sum>i\<in>Basis. f i *\<^sub>R i) = b \<longleftrightarrow> (\<forall>i\<in>Basis. f i = inner b i)"
+  by (subst euclidean_eq_iff) simp
 
-lemmas euclidean_simps =
-  euclidean_component_add
-  euclidean_component_diff
-  euclidean_component_scaleR
-  euclidean_component_minus
-  euclidean_component_setsum
-  basis_component
-
-lemma euclidean_representation:
-  fixes x :: "'a::euclidean_space"
-  shows "x = (\<Sum>i<DIM('a). (x$$i) *\<^sub>R basis i)"
-  apply (rule euclidean_eqI)
-  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 (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
+  unfolding euclidean_representation_setsum by simp
 
-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: 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"
-  by simp
-
-lemma euclidean_lambda_beta'':"(\<forall>j < DIM('a::euclidean_space). P j (((\<chi>\<chi> i. f i)::'a) $$ j)) \<longleftrightarrow>
-  (\<forall>j < DIM('a::euclidean_space). P j (f j))" by auto
-
-lemma euclidean_beta_reduce[simp]:
-  "(\<chi>\<chi> i. x $$ i) = (x::'a::euclidean_space)"
-  by (simp add: euclidean_eq)
-
-lemma euclidean_lambda_beta_0[simp]:
-    "((\<chi>\<chi> i. f i)::'a::euclidean_space) $$ 0 = f 0"
-  by (simp add: DIM_positive)
+lemma (in euclidean_space) choice_Basis_iff:
+  fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
+  shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
+  unfolding bchoice_iff
+proof safe
+  fix f assume "\<forall>i\<in>Basis. P i (f i)"
+  then show "\<exists>x. \<forall>i\<in>Basis. P i (inner x i)"
+    by (auto intro!: exI[of _ "\<Sum>i\<in>Basis. f i *\<^sub>R i"])
+qed auto
 
-lemma euclidean_inner:
-  "inner x (y::'a) = (\<Sum>i<DIM('a::euclidean_space). (x $$ i) * (y $$ i))"
-  by (subst (1 2) euclidean_representation,
-    simp add: inner_setsum_left inner_setsum_right
-    dot_basis if_distrib setsum_cases mult_commute)
-
-lemma euclidean_dist_l2:
-  fixes x y :: "'a::euclidean_space"
-  shows "dist x y = setL2 (\<lambda>i. dist (x $$ i) (y $$ i)) {..<DIM('a)}"
-  unfolding dist_norm norm_eq_sqrt_inner setL2_def
-  by (simp add: euclidean_inner power2_eq_square)
-
-lemma component_le_norm: "\<bar>x$$i\<bar> \<le> norm (x::'a::euclidean_space)"
-  unfolding euclidean_component_def
-  by (rule order_trans [OF Cauchy_Schwarz_ineq2]) simp
-
-lemma dist_nth_le: "dist (x $$ i) (y $$ i) \<le> dist x (y::'a::euclidean_space)"
-  unfolding euclidean_dist_l2 [where 'a='a]
-  by (cases "i < DIM('a)", rule member_le_setL2, auto)
+lemma DIM_positive: "0 < DIM('a::euclidean_space)"
+  by (simp add: card_gt_0_iff)
 
 subsection {* Subclass relationships *}
 
@@ -239,11 +100,13 @@
     assume "open {x}"
     then obtain e where "0 < e" and e: "\<forall>y. dist y x < e \<longrightarrow> y = x"
       unfolding open_dist by fast
-    def y \<equiv> "x + scaleR (e/2) (sgn (basis 0))"
+    def y \<equiv> "x + scaleR (e/2) (SOME b. b \<in> Basis)"
+    have [simp]: "(SOME b. b \<in> Basis) \<in> Basis"
+      by (rule someI_ex) (auto simp: ex_in_conv)
     from `0 < e` have "y \<noteq> x"
-      unfolding y_def by (simp add: sgn_zero_iff DIM_positive)
+      unfolding y_def by (auto intro!: nonzero_Basis)
     from `0 < e` have "dist y x < e"
-      unfolding y_def by (simp add: dist_norm norm_sgn)
+      unfolding y_def by (simp add: dist_norm norm_Basis)
     from `y \<noteq> x` and `dist y x < e` show "False"
       using e by simp
   qed
@@ -256,23 +119,17 @@
 instantiation real :: euclidean_space
 begin
 
-definition
-  "Basis = {1::real}"
-
-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)
+definition 
+  [simp]: "Basis = {1::real}"
 
 instance
   by default (auto simp add: Basis_real_def)
 
 end
 
+lemma DIM_real[simp]: "DIM(real) = 1"
+  by simp
+
 subsubsection {* Type @{typ complex} *}
 
 instantiation complex :: euclidean_space
@@ -281,20 +138,13 @@
 definition Basis_complex_def:
   "Basis = {1, ii}"
 
-definition
-  "dimension (t::complex itself) = 2"
-
-definition
-  "basis i = (if i = 0 then 1 else if i = 1 then ii else 0)"
-
 instance
-  by default (auto simp add: Basis_complex_def dimension_complex_def
-    basis_complex_def intro: complex_eqI split: split_if_asm)
+  by default (auto simp add: Basis_complex_def intro: complex_eqI split: split_if_asm)
 
 end
 
 lemma DIM_complex[simp]: "DIM(complex) = 2"
-  by (rule dimension_complex_def)
+  unfolding Basis_complex_def by simp
 
 subsubsection {* Type @{typ "'a \<times> 'b"} *}
 
@@ -304,12 +154,6 @@
 definition
   "Basis = (\<lambda>u. (u, 0)) ` Basis \<union> (\<lambda>v. (0, v)) ` Basis"
 
-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))))"
-
 instance proof
   show "(Basis :: ('a \<times> 'b) set) \<noteq> {}"
     unfolding Basis_prod_def by simp
@@ -327,20 +171,12 @@
   show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
     unfolding Basis_prod_def ball_Un ball_simps
     by (simp add: inner_prod_def prod_eq_iff euclidean_all_zero_iff)
-next
-  show "DIM('a \<times> 'b) = card (Basis :: ('a \<times> 'b) set)"
-    unfolding dimension_prod_def Basis_prod_def
-    by (simp add: card_Un_disjoint disjoint_iff_not_equal
-      card_image inj_on_def dimension_def)
-next
-  show "basis ` {..<DIM('a \<times> 'b)} = (Basis :: ('a \<times> 'b) set)"
-    by (auto simp add: Basis_prod_def dimension_prod_def basis_prod_def
-      image_def elim!: Basis_elim)
-next
-  show "basis ` {DIM('a \<times> 'b)..} = {0::('a \<times> 'b)}"
-    by (auto simp add: dimension_prod_def basis_prod_def prod_eq_iff image_def)
 qed
 
+lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('a) + DIM('b)"
+  unfolding Basis_prod_def
+  by (subst card_Un_disjoint) (auto intro!: card_image arg_cong2[where f="op +"] inj_onI)
+
 end
 
 end