# 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 {.. ('n::finite)" where - "cart_bij_nat = (SOME p. bij_betw p {.. \ cart_bij_nat" -definition "\' = inv_into {..::nat \ ('n::finite))" - -lemma bij_betw_pi: - "bij_betw \ {..x. bij_betw x {..' (UNIV::'n set) {..'_def by auto - -lemma pi'_inj[intro]: "inj \'" - using bij_betw_pi' unfolding bij_betw_def by auto - -lemma pi'_range[intro]: "\i::'n. \' i < CARD('n::finite)" - using bij_betw_pi' unfolding bij_betw_def by auto - -lemma \\'[simp]: "\i::'n::finite. \ (\' i) = i" - using bij_betw_pi by (auto intro!: f_inv_into_f simp: \'_def bij_betw_def) - -lemma \'\[simp]: "\i. i\{.. \' (\ i::'n) = i" - using bij_betw_pi by (auto intro!: inv_into_f_eq simp: \'_def bij_betw_def) - -lemma \\'_alt[simp]: "\i. i \' (\ i::'n) = i" - by auto - -lemma \_inj_on: "inj_on (\::nat\'n::finite) {.. j::'b. if j = \(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)) = (\ k. if k = \ 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 "\ \ 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 + \' 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 \ 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 \ 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 + \' 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 + \' (\ 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 "\ \ 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 "(\i (\x::'b. \i' 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) \ x = \ i \ \' x = i" - by auto - -lemma all_less_mult: - fixes m n :: nat - shows "(\i<(m * n). P i) \ (\ij i" thus "basis i = (0::'a^'b)" - unfolding dimension_cart_def basis_cart_def - by simp -next - show "\ij 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 "(\i 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 "{.. ('n::finite)" where + "cart_bij_nat = (SOME p. bij_betw p {.. \ cart_bij_nat" +definition "\' = inv_into {..::nat \ ('n::finite))" + +lemma bij_betw_pi: + "bij_betw \ {..x. bij_betw x {..' (UNIV::'n set) {..'_def by auto + +lemma pi'_inj[intro]: "inj \'" + using bij_betw_pi' unfolding bij_betw_def by auto + +lemma pi'_range[intro]: "\i::'n. \' i < CARD('n::finite)" + using bij_betw_pi' unfolding bij_betw_def by auto + +lemma \\'[simp]: "\i::'n::finite. \ (\' i) = i" + using bij_betw_pi by (auto intro!: f_inv_into_f simp: \'_def bij_betw_def) + +lemma \'\[simp]: "\i. i\{.. \' (\ i::'n) = i" + using bij_betw_pi by (auto intro!: inv_into_f_eq simp: \'_def bij_betw_def) + +lemma \\'_alt[simp]: "\i. i \' (\ i::'n) = i" + by auto + +lemma \_inj_on: "inj_on (\::nat\'n::finite) {.. j::'b. if j = \(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)) = (\ k. if k = \ 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 "\ \ 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 + \' 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 \ 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 \ 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 + \' 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 + \' (\ 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 "\ \ 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 "(\i (\x::'b. \i' 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) \ x = \ i \ \' x = i" + by auto + +lemma all_less_mult: + fixes m n :: nat + shows "(\i<(m * n). P i) \ (\ij i" thus "basis i = (0::'a^'b)" + unfolding dimension_cart_def basis_cart_def + by simp +next + show "\iji 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