--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 10 09:23:42 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 10 10:13:16 2011 -0700
@@ -213,8 +213,6 @@
instance cart :: (comm_ring_1,finite) comm_ring_1 ..
instance cart :: (ring_char_0,finite) ring_char_0 ..
-instance cart :: (real_vector,finite) real_vector ..
-
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x"
by (vector mult_assoc)
lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x"
@@ -320,170 +318,6 @@
finally show ?thesis .
qed
-subsection {* A bijection between 'n::finite and {..<CARD('n)} *}
-
-definition cart_bij_nat :: "nat \<Rightarrow> ('n::finite)" where
- "cart_bij_nat = (SOME p. bij_betw p {..<CARD('n)} (UNIV::'n set) )"
-
-abbreviation "\<pi> \<equiv> cart_bij_nat"
-definition "\<pi>' = inv_into {..<CARD('n)} (\<pi>::nat \<Rightarrow> ('n::finite))"
-
-lemma bij_betw_pi:
- "bij_betw \<pi> {..<CARD('n::finite)} (UNIV::('n::finite) set)"
- using ex_bij_betw_nat_finite[of "UNIV::'n set"]
- by (auto simp: cart_bij_nat_def atLeast0LessThan
- intro!: someI_ex[of "\<lambda>x. bij_betw x {..<CARD('n)} (UNIV::'n set)"])
-
-lemma bij_betw_pi'[intro]: "bij_betw \<pi>' (UNIV::'n set) {..<CARD('n::finite)}"
- using bij_betw_inv_into[OF bij_betw_pi] unfolding \<pi>'_def by auto
-
-lemma pi'_inj[intro]: "inj \<pi>'"
- using bij_betw_pi' unfolding bij_betw_def by auto
-
-lemma pi'_range[intro]: "\<And>i::'n. \<pi>' i < CARD('n::finite)"
- using bij_betw_pi' unfolding bij_betw_def by auto
-
-lemma \<pi>\<pi>'[simp]: "\<And>i::'n::finite. \<pi> (\<pi>' i) = i"
- using bij_betw_pi by (auto intro!: f_inv_into_f simp: \<pi>'_def bij_betw_def)
-
-lemma \<pi>'\<pi>[simp]: "\<And>i. i\<in>{..<CARD('n::finite)} \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
- using bij_betw_pi by (auto intro!: inv_into_f_eq simp: \<pi>'_def bij_betw_def)
-
-lemma \<pi>\<pi>'_alt[simp]: "\<And>i. i<CARD('n::finite) \<Longrightarrow> \<pi>' (\<pi> i::'n) = i"
- by auto
-
-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 :: (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)
- 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)"
-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
- finally show ?thesis
- unfolding basis_cart_def using assms by (auto simp: Cart_eq not_less field_simps)
-qed
-
-lemma basis_eq_pi':
- 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
-
-lemma split_times_into_modulo[consumes 1]:
- fixes k :: nat
- assumes "k < A * B"
- obtains i j where "i < A" and "j < B" and "k = j + i * B"
-proof
- have "A * B \<noteq> 0"
- proof assume "A * B = 0" with assms show False by simp qed
- hence "0 < B" by auto
- thus "k mod B < B" using `0 < B` by auto
-next
- have "k div B * B \<le> k div B * B + k mod B" by (rule le_add1)
- also have "... < A * B" using assms by simp
- 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"
-proof -
- have "i * A + j < (Suc i)*A" using `j < A` by simp
- also have "\<dots> \<le> B * A" using `i < B` unfolding mult_le_cancel2 by simp
- finally show ?thesis by simp
-qed
-
-lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
- by (rule dimension_cart_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_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 if_distr: "(if P then f else g) $ i = (if P then f $ i else g $ i)" by simp
lemma split_dimensions'[consumes 1]: