# HG changeset patch
# User huffman
# Date 1312996396 25200
# Node ID 18b4ab6854f1d773dcc4a4fa0354f82d3ccb6cac
# Parent  691c52e900cab050b18f1958a21f5e6571d756a3
move euclidean_space instance from Cartesian_Euclidean_Space.thy to Finite_Cartesian_Product.thy

diff -r 691c52e900ca -r 18b4ab6854f1 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- 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]:
diff -r 691c52e900ca -r 18b4ab6854f1 src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 09:23:42 2011 -0700
+++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy	Wed Aug 10 10:13:16 2011 -0700
@@ -6,7 +6,7 @@
 
 theory Finite_Cartesian_Product
 imports
-  "~~/src/HOL/Library/Inner_Product"
+  Euclidean_Space
   L2_Norm
   "~~/src/HOL/Library/Numeral_Type"
 begin
@@ -449,4 +449,170 @@
 
 end
 
+subsection {* Euclidean space *}
+
+text {* A bijection between @{text "'n::finite"} and @{text "{..<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).
+    inner (basis i :: 'a ^ 'b) (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
+
+end