--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Aug 11 09:11:15 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Thu Aug 11 13:05:56 2011 -0700
@@ -467,7 +467,7 @@
text {* some lemmas to map between Eucl and Cart *}
lemma basis_real_n[simp]:"(basis (\<pi>' i)::real^'a) = cart_basis i"
unfolding basis_vec_def using pi'_range[where 'n='a]
- by (auto simp: vec_eq_iff)
+ by (auto simp: vec_eq_iff axis_def)
subsection {* Orthogonality on cartesian products *}
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 11 09:11:15 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Thu Aug 11 13:05:56 2011 -0700
@@ -15,22 +15,75 @@
subsection {* Type class of Euclidean spaces *}
class euclidean_space = real_inner +
+ fixes Basis :: "'a set"
+ assumes nonempty_Basis [simp]: "Basis \<noteq> {}"
+ assumes finite_Basis [simp]: "finite Basis"
+ assumes inner_Basis:
+ "\<lbrakk>u \<in> Basis; v \<in> Basis\<rbrakk> \<Longrightarrow> inner u v = (if u = v then 1 else 0)"
+ 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 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)"
+ assumes image_basis: "basis ` {..<dimension TYPE('a)} = Basis"
+ assumes basis_finite: "basis ` {dimension TYPE('a)..} = {0}"
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"
+ unfolding norm_eq_sqrt_inner 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)
+
+lemma (in euclidean_space) Basis_zero [simp]: "0 \<notin> Basis"
+proof
+ assume "0 \<in> Basis" thus "False"
+ using inner_Basis [of 0 0] by simp
+qed
+
+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) 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) 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))")
@@ -161,6 +214,9 @@
begin
definition
+ "Basis = {1::real}"
+
+definition
"dimension (t::real itself) = 1"
definition [simp]:
@@ -170,42 +226,44 @@
by (rule dimension_real_def)
instance
- by default simp+
+ by default (auto simp add: Basis_real_def)
end
subsubsection {* Type @{typ complex} *}
+ (* TODO: move these to Complex.thy/Inner_Product.thy *)
+
+lemma norm_ii [simp]: "norm ii = 1"
+ unfolding i_def by simp
+
+lemma complex_inner_1 [simp]: "inner 1 x = Re x"
+ unfolding inner_complex_def by simp
+
+lemma complex_inner_1_right [simp]: "inner x 1 = Re x"
+ unfolding inner_complex_def by simp
+
+lemma complex_inner_ii_left [simp]: "inner ii x = Im x"
+ unfolding inner_complex_def by simp
+
+lemma complex_inner_ii_right [simp]: "inner x ii = Im x"
+ unfolding inner_complex_def by simp
+
instantiation complex :: euclidean_space
begin
+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)"
-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
+instance
+ by default (auto simp add: Basis_complex_def dimension_complex_def
+ basis_complex_def intro: complex_eqI split: split_if_asm)
end
@@ -214,40 +272,50 @@
subsubsection {* Type @{typ "'a \<times> 'b"} *}
+lemma disjoint_iff: "A \<inter> B = {} \<longleftrightarrow> (\<forall>x\<in>A. \<forall>y\<in>B. x \<noteq> y)"
+ by auto (* TODO: move elsewhere *)
+
instantiation prod :: (euclidean_space, euclidean_space) euclidean_space
begin
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))))"
-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)
+ show "(Basis :: ('a \<times> 'b) set) \<noteq> {}"
+ unfolding Basis_prod_def by simp
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
+ show "finite (Basis :: ('a \<times> 'b) set)"
+ unfolding Basis_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)
+ fix u v :: "'a \<times> 'b"
+ assume "u \<in> Basis" and "v \<in> Basis"
+ thus "inner u v = (if u = v then 1 else 0)"
+ unfolding Basis_prod_def inner_prod_def
+ by (auto simp add: inner_Basis split: split_if_asm)
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)
+ 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
+ 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
end
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 11 09:11:15 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Thu Aug 11 13:05:56 2011 -0700
@@ -442,8 +442,44 @@
end
+
subsection {* Euclidean space *}
+text {* Vectors pointing along a single axis. *}
+
+definition "axis k x = (\<chi> i. if i = k then x else 0)"
+
+lemma axis_nth [simp]: "axis i x $ i = x"
+ unfolding axis_def by simp
+
+lemma axis_eq_axis: "axis i x = axis j y \<longleftrightarrow> x = y \<and> i = j \<or> x = 0 \<and> y = 0"
+ unfolding axis_def vec_eq_iff by auto
+
+lemma inner_axis_axis:
+ "inner (axis i x) (axis j y) = (if i = j then inner x y else 0)"
+ unfolding inner_vec_def
+ apply (cases "i = j")
+ apply clarsimp
+ apply (subst setsum_diff1' [where a=j], simp_all)
+ apply (rule setsum_0', simp add: axis_def)
+ apply (rule setsum_0', simp add: axis_def)
+ done
+
+lemma setsum_single:
+ assumes "finite A" and "k \<in> A" and "f k = y"
+ assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0"
+ shows "(\<Sum>i\<in>A. f i) = y"
+ apply (subst setsum_diff1' [OF assms(1,2)])
+ apply (simp add: setsum_0' assms(3,4))
+ done
+
+lemma inner_axis: "inner x (axis i y) = inner (x $ i) y"
+ unfolding inner_vec_def
+ apply (rule_tac k=i in setsum_single)
+ apply simp_all
+ apply (simp add: axis_def)
+ done
+
text {* A bijection between @{text "'n::finite"} and @{text "{..<CARD('n)}"} *}
definition vec_bij_nat :: "nat \<Rightarrow> ('n::finite)" where
@@ -482,16 +518,18 @@
instantiation vec :: (euclidean_space, finite) euclidean_space
begin
+definition "Basis = (\<Union>i. \<Union>u\<in>Basis. {axis i u})"
+
definition "dimension (t :: ('a ^ 'b) itself) = CARD('b) * DIM('a)"
-definition "(basis i::'a^'b) =
+definition "basis i =
(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)
+ then axis (\<pi>(i div DIM('a))) (basis (i mod DIM('a)))
else 0)"
lemma basis_eq:
assumes "i < CARD('b)" and "j < DIM('a)"
- shows "basis (j + i * DIM('a)) = (\<chi> k. if k = \<pi> i then basis j else 0)"
+ shows "basis (j + i * DIM('a)) = axis (\<pi> i) (basis j)"
proof -
have "j + i * DIM('a) < DIM('a) * (i + 1)" using assms by (auto simp: field_simps)
also have "\<dots> \<le> DIM('a) * CARD('b)" using assms unfolding mult_le_cancel1 by auto
@@ -503,7 +541,7 @@
assumes "j < DIM('a)"
shows "basis (j + \<pi>' i * DIM('a)) $ k = (if k = i then basis j else 0)"
apply (subst basis_eq)
- using pi'_range assms by simp_all
+ using pi'_range assms by (simp_all add: axis_def)
lemma split_times_into_modulo[consumes 1]:
fixes k :: nat
@@ -520,20 +558,6 @@
finally show "k div B < A" by auto
qed simp
-lemma split_CARD_DIM[consumes 1]:
- fixes k :: nat
- assumes k: "k < CARD('b) * DIM('a)"
- obtains i and j::'b where "i < DIM('a)" "k = i + \<pi>' j * DIM('a)"
-proof -
- from split_times_into_modulo[OF k] guess i j . note ij = this
- show thesis
- proof
- show "j < DIM('a)" using ij by simp
- show "k = j + \<pi>' (\<pi> i :: 'b) * DIM('a)"
- using ij by simp
- qed
-qed
-
lemma linear_less_than_times:
fixes i j A B :: nat assumes "i < B" "j < A"
shows "j + i * A < B * A"
@@ -546,64 +570,43 @@
lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
by (rule dimension_vec_def)
-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
-
-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
-
instance proof
- show "0 < DIM('a ^ 'b)"
- unfolding dimension_vec_def
- by (intro mult_pos_pos zero_less_card_finite DIM_positive)
+ show "(Basis :: ('a ^ 'b) set) \<noteq> {}"
+ unfolding Basis_vec_def by simp
+next
+ show "finite (Basis :: ('a ^ 'b) set)"
+ unfolding Basis_vec_def by simp
next
- fix i :: nat
- assume "DIM('a ^ 'b) \<le> i" thus "basis i = (0::'a^'b)"
- unfolding dimension_vec_def basis_vec_def
- by simp
+ fix u v :: "'a ^ 'b"
+ assume "u \<in> Basis" and "v \<in> Basis"
+ thus "inner u v = (if u = v then 1 else 0)"
+ unfolding Basis_vec_def
+ by (auto simp add: inner_axis_axis axis_eq_axis inner_Basis)
next
- show "\<forall>i<DIM('a ^ 'b). \<forall>j<DIM('a ^ 'b).
- inner (basis i :: 'a ^ 'b) (basis j) = (if i = j then 1 else 0)"
- apply (simp add: inner_vec_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)
+ fix x :: "'a ^ 'b"
+ show "(\<forall>u\<in>Basis. inner x u = 0) \<longleftrightarrow> x = 0"
+ unfolding Basis_vec_def
+ by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
+next
+ show "DIM('a ^ 'b) = card (Basis :: ('a ^ 'b) set)"
+ unfolding Basis_vec_def dimension_vec_def dimension_def
+ by (simp add: card_UN_disjoint [unfolded disjoint_iff]
+ axis_eq_axis nonzero_Basis)
+next
+ show "basis ` {..<DIM('a ^ 'b)} = (Basis :: ('a ^ 'b) set)"
+ unfolding Basis_vec_def
+ apply auto
+ apply (erule split_times_into_modulo)
+ apply (simp add: basis_eq axis_eq_axis)
+ apply (erule Basis_elim)
+ apply (simp add: image_def basis_vec_def axis_eq_axis)
+ apply (rule rev_bexI, simp)
+ apply (erule linear_less_than_times [OF pi'_range])
+ apply simp
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_vec_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: vec_eq_iff)
- done
+ show "basis ` {DIM('a ^ 'b)..} = {0::'a ^ 'b}"
+ by (auto simp add: image_def basis_vec_def)
qed
end
--- a/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Aug 11 09:11:15 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Linear_Algebra.thy Thu Aug 11 13:05:56 2011 -0700
@@ -1581,12 +1581,6 @@
subsection{* Euclidean Spaces as Typeclass*}
-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}"
shows "independent (f ` {..<D}) \<longleftrightarrow> (\<forall>a u. a < D \<longrightarrow> (\<Sum>i\<in>{..<D}-{a}. u (f i) *\<^sub>R f i) \<noteq> f a)"