# HG changeset patch # User huffman # Date 1313007217 25200 # Node ID e63ad7d5158de06077510f4e0ba40ced853c5962 # Parent 18b4ab6854f1d773dcc4a4fa0354f82d3ccb6cac more uniform naming scheme for finite cartesian product type and related theorems diff -r 18b4ab6854f1 -r e63ad7d5158d NEWS --- a/NEWS Wed Aug 10 10:13:16 2011 -0700 +++ b/NEWS Wed Aug 10 13:13:37 2011 -0700 @@ -183,6 +183,19 @@ * Limits.thy: Type "'a net" has been renamed to "'a filter", in accordance with standard mathematical terminology. INCOMPATIBILITY. +* Session Multivariate_Analysis: Type "('a, 'b) cart" has been renamed +to "('a, 'b) vec" (the syntax "'a ^ 'b" remains unaffected). Constants +"Cart_nth" and "Cart_lambda" have been respectively renamed to +"vec_nth" and "vec_lambda"; theorems mentioning those names have +changed to match. Definition theorems for overloaded constants now use +the standard "foo_vec_def" naming scheme. A few other theorems have +been renamed as follows (INCOMPATIBILITY): + + Cart_eq ~> vec_eq_iff + dist_nth_le_cart ~> dist_vec_nth_le + tendsto_vector ~> vec_tendstoI + Cauchy_vector ~> vec_CauchyI + *** Document preparation *** diff -r 18b4ab6854f1 -r e63ad7d5158d src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 10 10:13:16 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy Wed Aug 10 13:13:37 2011 -0700 @@ -36,24 +36,23 @@ subsection{* Basic componentwise operations on vectors. *} -instantiation cart :: (times,finite) times +instantiation vec :: (times, finite) times begin - definition vector_mult_def : "op * \ (\ x y. (\ i. (x$i) * (y$i)))" + definition "op * \ (\ x y. (\ i. (x$i) * (y$i)))" instance .. end -instantiation cart :: (one,finite) one +instantiation vec :: (one, finite) one begin - definition vector_one_def : "1 \ (\ i. 1)" + definition "1 \ (\ i. 1)" instance .. end -instantiation cart :: (ord,finite) ord +instantiation vec :: (ord, finite) ord begin - definition vector_le_def: - "less_eq (x :: 'a ^'b) y = (ALL i. x$i <= y$i)" - definition vector_less_def: "less (x :: 'a ^'b) y = (ALL i. x$i < y$i)" - instance by (intro_classes) + definition "x \ y \ (\i. x$i \ y$i)" + definition "x < y \ (\i. x$i < y$i)" + instance .. end text{* The ordering on one-dimensional vectors is linear. *} @@ -65,12 +64,12 @@ by (auto intro!: card_ge_0_finite) qed end -instantiation cart :: (linorder,cart_one) linorder begin +instantiation vec :: (linorder,cart_one) linorder begin instance proof guess a B using UNIV_one[where 'a='b] unfolding card_Suc_eq apply- by(erule exE)+ hence *:"UNIV = {a}" by auto have "\P. (\i\UNIV. P i) \ P a" unfolding * by auto hence all:"\P. (\i. P i) \ P a" by auto - fix x y z::"'a^'b::cart_one" note * = vector_le_def vector_less_def all Cart_eq + fix x y z::"'a^'b::cart_one" note * = less_eq_vec_def less_vec_def all vec_eq_iff show "x\x" "(x < y) = (x \ y \ \ y \ x)" "x\y \ y\x" unfolding * by(auto simp only:field_simps) { assume "x\y" "y\z" thus "x\z" unfolding * by(auto simp only:field_simps) } { assume "x\y" "y\x" thus "x=y" unfolding * by(auto simp only:field_simps) } @@ -93,16 +92,16 @@ @{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, @{thm setsum_left_distrib}, @{thm setsum_negf} RS sym] val ss2 = @{simpset} addsimps - [@{thm vector_add_def}, @{thm vector_mult_def}, - @{thm vector_minus_def}, @{thm vector_uminus_def}, - @{thm vector_one_def}, @{thm vector_zero_def}, @{thm vec_def}, - @{thm vector_scaleR_def}, - @{thm Cart_lambda_beta}, @{thm vector_scalar_mult_def}] + [@{thm plus_vec_def}, @{thm times_vec_def}, + @{thm minus_vec_def}, @{thm uminus_vec_def}, + @{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def}, + @{thm scaleR_vec_def}, + @{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}] fun vector_arith_tac ths = simp_tac ss1 THEN' (fn i => rtac @{thm setsum_cong2} i ORELSE rtac @{thm setsum_0'} i - ORELSE simp_tac (HOL_basic_ss addsimps [@{thm "Cart_eq"}]) i) + ORELSE simp_tac (HOL_basic_ss addsimps [@{thm vec_eq_iff}]) i) (* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) THEN' asm_full_simp_tac (ss2 addsimps ths) in @@ -110,8 +109,8 @@ end *} "lift trivial vector statements to real arith statements" -lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def) -lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def) +lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def) +lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def) lemma vec_inj[simp]: "vec x = vec y \ x = y" by vector @@ -149,49 +148,47 @@ subsection {* Some frequently useful arithmetic lemmas over vectors. *} -instance cart :: (semigroup_mult,finite) semigroup_mult - apply (intro_classes) by (vector mult_assoc) +instance vec :: (semigroup_mult, finite) semigroup_mult + by default (vector mult_assoc) -instance cart :: (monoid_mult,finite) monoid_mult - apply (intro_classes) by vector+ +instance vec :: (monoid_mult, finite) monoid_mult + by default vector+ -instance cart :: (ab_semigroup_mult,finite) ab_semigroup_mult - apply (intro_classes) by (vector mult_commute) +instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult + by default (vector mult_commute) -instance cart :: (ab_semigroup_idem_mult,finite) ab_semigroup_idem_mult - apply (intro_classes) by (vector mult_idem) +instance vec :: (ab_semigroup_idem_mult, finite) ab_semigroup_idem_mult + by default (vector mult_idem) -instance cart :: (comm_monoid_mult,finite) comm_monoid_mult - apply (intro_classes) by vector +instance vec :: (comm_monoid_mult, finite) comm_monoid_mult + by default vector -instance cart :: (semiring,finite) semiring - apply (intro_classes) by (vector field_simps)+ +instance vec :: (semiring, finite) semiring + by default (vector field_simps)+ -instance cart :: (semiring_0,finite) semiring_0 - apply (intro_classes) by (vector field_simps)+ -instance cart :: (semiring_1,finite) semiring_1 - apply (intro_classes) by vector -instance cart :: (comm_semiring,finite) comm_semiring - apply (intro_classes) by (vector field_simps)+ +instance vec :: (semiring_0, finite) semiring_0 + by default (vector field_simps)+ +instance vec :: (semiring_1, finite) semiring_1 + by default vector +instance vec :: (comm_semiring, finite) comm_semiring + by default (vector field_simps)+ -instance cart :: (comm_semiring_0,finite) comm_semiring_0 by (intro_classes) -instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. -instance cart :: (semiring_0_cancel,finite) semiring_0_cancel by (intro_classes) -instance cart :: (comm_semiring_0_cancel,finite) comm_semiring_0_cancel by (intro_classes) -instance cart :: (ring,finite) ring by (intro_classes) -instance cart :: (semiring_1_cancel,finite) semiring_1_cancel by (intro_classes) -instance cart :: (comm_semiring_1,finite) comm_semiring_1 by (intro_classes) +instance vec :: (comm_semiring_0, finite) comm_semiring_0 .. +instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. +instance vec :: (semiring_0_cancel, finite) semiring_0_cancel .. +instance vec :: (comm_semiring_0_cancel, finite) comm_semiring_0_cancel .. +instance vec :: (ring, finite) ring .. +instance vec :: (semiring_1_cancel, finite) semiring_1_cancel .. +instance vec :: (comm_semiring_1, finite) comm_semiring_1 .. -instance cart :: (ring_1,finite) ring_1 .. +instance vec :: (ring_1, finite) ring_1 .. -instance cart :: (real_algebra,finite) real_algebra +instance vec :: (real_algebra, finite) real_algebra apply intro_classes - apply (simp_all add: vector_scaleR_def field_simps) - apply vector - apply vector + apply (simp_all add: vec_eq_iff) done -instance cart :: (real_algebra_1,finite) real_algebra_1 .. +instance vec :: (real_algebra_1, finite) real_algebra_1 .. lemma of_nat_index: "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n" @@ -203,15 +200,15 @@ lemma one_index[simp]: "(1 :: 'a::one ^'n)$i = 1" by vector -instance cart :: (semiring_char_0, finite) semiring_char_0 +instance vec :: (semiring_char_0, finite) semiring_char_0 proof fix m n :: nat show "inj (of_nat :: nat \ 'a ^ 'b)" - by (auto intro!: injI simp add: Cart_eq of_nat_index) + by (auto intro!: injI simp add: vec_eq_iff of_nat_index) qed -instance cart :: (comm_ring_1,finite) comm_ring_1 .. -instance cart :: (ring_char_0,finite) ring_char_0 .. +instance vec :: (comm_ring_1, finite) comm_ring_1 .. +instance vec :: (ring_char_0, finite) ring_char_0 .. lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" by (vector mult_assoc) @@ -231,7 +228,7 @@ by (vector field_simps) lemma vec_eq[simp]: "(vec m = vec n) \ (m = n)" - by (simp add: Cart_eq) + by (simp add: vec_eq_iff) lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) lemma vector_mul_eq_0[simp]: "(a *s x = 0) \ a = (0::'a::idom) \ x = 0" @@ -246,7 +243,7 @@ by (metis vector_mul_rcancel) lemma component_le_norm_cart: "\x$i\ <= norm x" - apply (simp add: norm_vector_def) + apply (simp add: norm_vec_def) apply (rule member_le_setL2, simp_all) done @@ -257,10 +254,10 @@ by (metis component_le_norm_cart basic_trans_rules(21)) lemma norm_le_l1_cart: "norm x <= setsum(\i. \x$i\) UNIV" - by (simp add: norm_vector_def setL2_le_setsum) + by (simp add: norm_vec_def setL2_le_setsum) lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x" - unfolding vector_scaleR_def vector_scalar_mult_def by simp + unfolding scaleR_vec_def vector_scalar_mult_def by simp lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \c\ * dist x y" unfolding dist_norm scalar_mult_eq_scaleR @@ -272,12 +269,12 @@ by (cases "finite S", induct S set: finite, simp_all) lemma setsum_eq: "setsum f S = (\ i. setsum (\x. (f x)$i ) S)" - by (simp add: Cart_eq) + by (simp add: vec_eq_iff) lemma setsum_cmul: fixes f:: "'c \ ('a::semiring_1)^'n" shows "setsum (\x. c *s f x) S = c *s setsum f S" - by (simp add: Cart_eq setsum_right_distrib) + by (simp add: vec_eq_iff setsum_right_distrib) (* TODO: use setsum_norm_allsubsets_bound *) lemma setsum_norm_allsubsets_bound_cart: @@ -359,10 +356,10 @@ lemmas cart_simps = forall_CARD_DIM exists_CARD_DIM forall_CARD exists_CARD lemma cart_euclidean_nth[simp]: - fixes x :: "('a::euclidean_space, 'b::finite) cart" + fixes x :: "('a::euclidean_space, 'b::finite) vec" assumes j:"j < DIM('a)" shows "x $$ (j + \' i * DIM('a)) = x $ i $$ j" - unfolding euclidean_component_def inner_vector_def basis_eq_pi'[OF j] if_distrib cond_application_beta + unfolding euclidean_component_def inner_vec_def basis_eq_pi'[OF j] if_distrib cond_application_beta by (simp add: setsum_cases) lemma real_euclidean_nth: @@ -393,13 +390,13 @@ thus "x = y \ i = j" using * by simp qed simp -instance cart :: (ordered_euclidean_space,finite) ordered_euclidean_space +instance vec :: (ordered_euclidean_space, finite) ordered_euclidean_space proof fix x y::"'a^'b" - show "(x \ y) = (\i y $$ i)" - unfolding vector_le_def apply(subst eucl_le) by (simp add: cart_simps) - show"(x < y) = (\i y) = (\i y $$ i)" + unfolding less_eq_vec_def apply(subst eucl_le) by (simp add: cart_simps) + show"(x < y) = (\ik. 1::real"] by auto @@ -431,14 +428,14 @@ qed lemma basis_inj[intro]: "inj (cart_basis :: 'n \ real ^'n)" - by (simp add: inj_on_def Cart_eq) + by (simp add: inj_on_def vec_eq_iff) lemma basis_expansion: "setsum (\i. (x$i) *s cart_basis i) UNIV = (x::('a::ring_1) ^'n)" (is "?lhs = ?rhs" is "setsum ?f ?S = _") - by (auto simp add: Cart_eq if_distrib setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) + by (auto simp add: vec_eq_iff if_distrib setsum_delta[of "?S", where ?'b = "'a", simplified] cong del: if_weak_cong) lemma smult_conv_scaleR: "c *s x = scaleR c x" - unfolding vector_scalar_mult_def vector_scaleR_def by simp + unfolding vector_scalar_mult_def scaleR_vec_def by simp lemma basis_expansion': "setsum (\i. (x$i) *\<^sub>R cart_basis i) UNIV = x" @@ -446,22 +443,22 @@ lemma basis_expansion_unique: "setsum (\i. f i *s cart_basis i) UNIV = (x::('a::comm_ring_1) ^'n) \ (\i. f i = x$i)" - by (simp add: Cart_eq setsum_delta if_distrib cong del: if_weak_cong) + by (simp add: vec_eq_iff setsum_delta if_distrib cong del: if_weak_cong) lemma dot_basis: shows "cart_basis i \ x = x$i" "x \ (cart_basis i) = (x$i)" - by (auto simp add: inner_vector_def cart_basis_def cond_application_beta if_distrib setsum_delta + by (auto simp add: inner_vec_def cart_basis_def cond_application_beta if_distrib setsum_delta cong del: if_weak_cong) lemma inner_basis: fixes x :: "'a::{real_inner, real_algebra_1} ^ 'n" shows "inner (cart_basis i) x = inner 1 (x $ i)" and "inner x (cart_basis i) = inner (x $ i) 1" - unfolding inner_vector_def cart_basis_def + unfolding inner_vec_def cart_basis_def by (auto simp add: cond_application_beta if_distrib setsum_delta cong del: if_weak_cong) lemma basis_eq_0: "cart_basis i = (0::'a::semiring_1^'n) \ False" - by (auto simp add: Cart_eq) + by (auto simp add: vec_eq_iff) lemma basis_nonzero: shows "cart_basis k \ (0:: 'a::semiring_1 ^'n)" @@ -469,14 +466,14 @@ text {* some lemmas to map between Eucl and Cart *} lemma basis_real_n[simp]:"(basis (\' i)::real^'a) = cart_basis i" - unfolding basis_cart_def using pi'_range[where 'n='a] - by (auto simp: Cart_eq Cart_lambda_beta) + unfolding basis_vec_def using pi'_range[where 'n='a] + by (auto simp: vec_eq_iff) subsection {* Orthogonality on cartesian products *} lemma orthogonal_basis: shows "orthogonal (cart_basis i) x \ x$i = (0::real)" - by (auto simp add: orthogonal_def inner_vector_def cart_basis_def if_distrib + by (auto simp add: orthogonal_def inner_vec_def cart_basis_def if_distrib cond_application_beta setsum_delta cong del: if_weak_cong) lemma orthogonal_basis_basis: @@ -518,7 +515,7 @@ by (simp add: linear_cmul[OF lf]) finally have "f x \ y = x \ ?w" apply (simp only: ) - apply (simp add: inner_vector_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] field_simps) + apply (simp add: inner_vec_def setsum_left_distrib setsum_right_distrib setsum_commute[of _ ?M ?N] field_simps) done} } then show ?thesis unfolding adjoint_def @@ -612,25 +609,25 @@ setsum_delta' cong del: if_weak_cong) lemma matrix_transpose_mul: "transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)" - by (simp add: matrix_matrix_mult_def transpose_def Cart_eq mult_commute) + by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult_commute) lemma matrix_eq: fixes A B :: "'a::semiring_1 ^ 'n ^ 'm" shows "A = B \ (\x. A *v x = B *v x)" (is "?lhs \ ?rhs") apply auto - apply (subst Cart_eq) + apply (subst vec_eq_iff) apply clarify - apply (clarsimp simp add: matrix_vector_mult_def cart_basis_def if_distrib cond_application_beta Cart_eq cong del: if_weak_cong) + apply (clarsimp simp add: matrix_vector_mult_def cart_basis_def if_distrib cond_application_beta vec_eq_iff cong del: if_weak_cong) apply (erule_tac x="cart_basis ia" in allE) apply (erule_tac x="i" in allE) by (auto simp add: cart_basis_def if_distrib cond_application_beta setsum_delta[OF finite] cong del: if_weak_cong) lemma matrix_vector_mul_component: shows "((A::real^_^_) *v x)$k = (A$k) \ x" - by (simp add: matrix_vector_mult_def inner_vector_def) + by (simp add: matrix_vector_mult_def inner_vec_def) lemma dot_lmul_matrix: "((x::real ^_) v* A) \ y = x \ (A *v y)" - apply (simp add: inner_vector_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) + apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) apply (subst setsum_commute) by simp @@ -643,12 +640,12 @@ lemma row_transpose: fixes A:: "'a::semiring_1^_^_" shows "row i (transpose A) = column i A" - by (simp add: row_def column_def transpose_def Cart_eq) + by (simp add: row_def column_def transpose_def vec_eq_iff) lemma column_transpose: fixes A:: "'a::semiring_1^_^_" shows "column i (transpose A) = row i A" - by (simp add: row_def column_def transpose_def Cart_eq) + by (simp add: row_def column_def transpose_def vec_eq_iff) lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A" by (auto simp add: rows_def columns_def row_transpose intro: set_eqI) @@ -658,15 +655,15 @@ text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *} lemma matrix_mult_dot: "A *v x = (\ i. A$i \ x)" - by (simp add: matrix_vector_mult_def inner_vector_def) + by (simp add: matrix_vector_mult_def inner_vec_def) lemma matrix_mult_vsum: "(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\i. (x$i) *s column i A) (UNIV:: 'n set)" - by (simp add: matrix_vector_mult_def Cart_eq column_def mult_commute) + by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult_commute) lemma vector_componentwise: "(x::'a::ring_1^'n) = (\ j. setsum (\i. (x$i) * (cart_basis i :: 'a^'n)$j) (UNIV :: 'n set))" apply (subst basis_expansion[symmetric]) - by (vector Cart_eq setsum_component) + by (vector vec_eq_iff setsum_component) lemma linear_componentwise: fixes f:: "real ^'m \ real ^ _" @@ -696,10 +693,10 @@ where "matrix f = (\ i j. (f(cart_basis j))$i)" lemma matrix_vector_mul_linear: "linear(\x. A *v (x::real ^ _))" - by (simp add: linear_def matrix_vector_mult_def Cart_eq field_simps setsum_right_distrib setsum_addf) + by (simp add: linear_def matrix_vector_mult_def vec_eq_iff field_simps setsum_right_distrib setsum_addf) lemma matrix_works: assumes lf: "linear f" shows "matrix f *v x = f (x::real ^ 'n)" -apply (simp add: matrix_def matrix_vector_mult_def Cart_eq mult_commute) +apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult_commute) apply clarify apply (rule linear_componentwise[OF lf, symmetric]) done @@ -717,11 +714,11 @@ by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)" - by (simp add: matrix_vector_mult_def transpose_def Cart_eq mult_commute) + by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult_commute) lemma adjoint_matrix: "adjoint(\x. (A::real^'n^'m) *v x) = (\x. transpose A *v x)" apply (rule adjoint_unique) - apply (simp add: transpose_def inner_vector_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) + apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) apply (subst setsum_commute) apply (auto simp add: mult_ac) done @@ -916,10 +913,10 @@ let ?x = "\ i. c i" have th0:"A *v ?x = 0" using c - unfolding matrix_mult_vsum Cart_eq + unfolding matrix_mult_vsum vec_eq_iff by auto from k[rule_format, OF th0] i - have "c i = 0" by (vector Cart_eq)} + have "c i = 0" by (vector vec_eq_iff)} hence ?rhs by blast} moreover {assume H: ?rhs @@ -1038,17 +1035,17 @@ lemma transpose_columnvector: "transpose(columnvector v) = rowvector v" - by (simp add: transpose_def rowvector_def columnvector_def Cart_eq) + by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) lemma transpose_rowvector: "transpose(rowvector v) = columnvector v" - by (simp add: transpose_def columnvector_def rowvector_def Cart_eq) + by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) lemma dot_matrix_product: "(x::real^'n) \ y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1" - by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vector_def) + by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) lemma dot_matrix_vector_mul: fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" @@ -1078,18 +1075,18 @@ unfolding nth_conv_component using component_le_infnorm[of x] . -instance cart :: (perfect_space, finite) perfect_space +instance vec :: (perfect_space, finite) perfect_space proof fix x :: "'a ^ 'b" show "x islimpt UNIV" apply (rule islimptI) - apply (unfold open_vector_def) + apply (unfold open_vec_def) apply (drule (1) bspec) apply clarsimp apply (subgoal_tac "\i\UNIV. \y. y \ A i \ y \ x $ i") apply (drule finite_choice [OF finite_UNIV], erule exE) - apply (rule_tac x="Cart_lambda f" in exI) - apply (simp add: Cart_eq) + apply (rule_tac x="vec_lambda f" in exI) + apply (simp add: vec_eq_iff) apply (rule ballI, drule_tac x=i in spec, clarify) apply (cut_tac x="x $ i" in islimpt_UNIV) apply (simp add: islimpt_def) @@ -1122,7 +1119,7 @@ apply (clarify) apply (drule spec, drule (1) mp) apply (erule eventually_elim1) - apply (erule le_less_trans [OF dist_nth_le_cart]) + apply (erule le_less_trans [OF dist_vec_nth_le]) done lemma bounded_component_cart: "bounded s \ bounded ((\x. x $ i) ` s)" @@ -1131,7 +1128,7 @@ apply (rule_tac x="x $ i" in exI) apply (rule_tac x="e" in exI) apply clarify -apply (rule order_trans [OF dist_nth_le_cart], simp) +apply (rule order_trans [OF dist_vec_nth_le], simp) done lemma compact_lemma_cart: @@ -1168,7 +1165,7 @@ qed qed -instance cart :: (heine_borel, finite) heine_borel +instance vec :: (heine_borel, finite) heine_borel proof fix s :: "('a ^ 'b) set" and f :: "nat \ 'a ^ 'b" assume s: "bounded s" and f: "\n. f n \ s" @@ -1184,7 +1181,7 @@ moreover { fix n assume n: "\i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))" have "dist (f (r n)) l \ (\i\?d. dist (f (r n) $ i) (l $ i))" - unfolding dist_vector_def using zero_le_dist by (rule setL2_le_setsum) + unfolding dist_vec_def using zero_le_dist by (rule setL2_le_setsum) also have "\ < (\i\?d. e / (real_of_nat (card ?d)))" by (rule setsum_strict_mono) (simp_all add: n) finally have "dist (f (r n)) l < e" by simp @@ -1205,12 +1202,12 @@ lemma interval_cart: fixes a :: "'a::ord^'n" shows "{a <..< b} = {x::'a^'n. \i. a$i < x$i \ x$i < b$i}" and "{a .. b} = {x::'a^'n. \i. a$i \ x$i \ x$i \ b$i}" - by (auto simp add: set_eq_iff vector_less_def vector_le_def) + by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def) lemma mem_interval_cart: fixes a :: "'a::ord^'n" shows "x \ {a<.. (\i. a$i < x$i \ x$i < b$i)" "x \ {a .. b} \ (\i. a$i \ x$i \ x$i \ b$i)" - using interval_cart[of a b] by(auto simp add: set_eq_iff vector_less_def vector_le_def) + using interval_cart[of a b] by(auto simp add: set_eq_iff less_vec_def less_eq_vec_def) lemma interval_eq_empty_cart: fixes a :: "real^'n" shows "({a <..< b} = {} \ (\i. b$i \ a$i))" (is ?th1) and @@ -1263,7 +1260,7 @@ lemma interval_sing: fixes a :: "'a::linorder^'n" shows "{a .. a} = {a} \ {a<.. x $ i" using x order_less_imp_le[of "a$i" "x$i"] - by(simp add: set_eq_iff vector_less_def vector_le_def Cart_eq) + by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) } moreover { fix i have "x $ i \ b $ i" using x order_less_imp_le[of "x$i" "b$i"] - by(simp add: set_eq_iff vector_less_def vector_le_def Cart_eq) + by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) } ultimately show "a \ x \ x \ b" - by(simp add: set_eq_iff vector_less_def vector_le_def Cart_eq) + by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) qed lemma subset_interval_cart: fixes a :: "real^'n" shows @@ -1406,12 +1403,12 @@ lemma dim_substandard_cart: shows "dim {x::real^'n. \i. i \ d \ x$i = 0} = card d" (is "dim ?A = _") -proof- have *:"{x. \i \' ` d \ x $$ i = 0} = +proof- have *:"{x. \i \' ` d \ x $$ i = 0} = {x::real^'n. \i. i \ d \ x$i = 0}"apply safe apply(erule_tac x="\' i" in allE) defer apply(erule_tac x="\ i" in allE) unfolding image_iff real_euclidean_nth[symmetric] by (auto simp: pi'_inj[THEN inj_eq]) - have " \' ` d \ {.. {..'" d] using pi'_inj unfolding inj_on_def by auto qed @@ -1464,7 +1461,7 @@ declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp] declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp] -lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component vector_le_def Cart_lambda_beta basis_component vector_uminus_component +lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component less_eq_vec_def vec_lambda_beta basis_component vector_uminus_component lemma convex_box_cart: assumes "\i. convex {x. P i x}" @@ -1489,7 +1486,7 @@ lemma std_simplex_cart: "(insert (0::real^'n) { cart_basis i | i. i\UNIV}) = - (insert 0 { basis i | i. i (a,b) (u,v) (x::real^'n). (\ i. u$i + (x$i - a$i) / (b$i - a$i) * (v$i - u$i))::real^'n)" unfolding interval_bij_def apply(rule ext)+ apply safe - unfolding Cart_eq Cart_lambda_beta unfolding nth_conv_component + unfolding vec_eq_iff vec_lambda_beta unfolding nth_conv_component apply rule apply(subst euclidean_lambda_beta) using pi'_range by auto lemma interval_bij_affine_cart: "interval_bij (a,b) (u,v) = (\x. (\ i. (v$i - u$i) / (b$i - a$i) * x$i) + (\ i. u$i - (v$i - u$i) / (b$i - a$i) * a$i)::real^'n)" - apply rule unfolding Cart_eq interval_bij_cart vector_component_simps + apply rule unfolding vec_eq_iff interval_bij_cart vector_component_simps by(auto simp add: field_simps add_divide_distrib[THEN sym]) subsection "Derivative" @@ -1552,7 +1549,7 @@ proof(rule ccontr) def D \ "jacobian f (at x)" assume "jacobian f (at x) $ k \ 0" - then obtain j where j:"D$k$j \ 0" unfolding Cart_eq D_def by auto + then obtain j where j:"D$k$j \ 0" unfolding vec_eq_iff D_def by auto hence *:"abs (jacobian f (at x) $ k $ j) / 2 > 0" unfolding D_def by auto note as = assms(3)[unfolded jacobian_works has_derivative_at_alt] guess e' using as[THEN conjunct2,rule_format,OF *] .. note e' = this @@ -1639,10 +1636,10 @@ where "dest_vec1 x \ (x$1)" lemma vec1_dest_vec1[simp]: "vec1(dest_vec1 x) = x" "dest_vec1(vec1 y) = y" - by (simp_all add: Cart_eq) + by (simp_all add: vec_eq_iff) lemma vec1_component[simp]: "(vec1 x)$1 = x" - by (simp_all add: Cart_eq) + by (simp_all add: vec_eq_iff) declare vec1_dest_vec1(1) [simp] @@ -1661,7 +1658,7 @@ subsection{* The collapse of the general concepts to dimension one. *} lemma vector_one: "(x::'a ^1) = (\ i. (x$1))" - by (simp add: Cart_eq) + by (simp add: vec_eq_iff) lemma forall_one: "(\(x::'a ^1). P x) \ (\x. P(\ i. x))" apply auto @@ -1670,7 +1667,7 @@ done lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" - by (simp add: norm_vector_def) + by (simp add: norm_vec_def) lemma norm_real: "norm(x::real ^ 1) = abs(x$1)" by (simp add: norm_vector_1) @@ -1751,7 +1748,7 @@ by (metis vec1_dest_vec1(1) norm_vec1) lemmas vec1_dest_vec1_simps = forall_vec1 vec_add[THEN sym] dist_vec1 vec_sub[THEN sym] vec1_dest_vec1 norm_vec1 vector_smult_component - vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def norm_vec1 real_norm_def + vec1_eq vec_cmul[THEN sym] smult_conv_scaleR[THEN sym] o_def dist_real_def real_norm_def lemma bounded_linear_vec1:"bounded_linear (vec1::real\real^1)" unfolding bounded_linear_def additive_def bounded_linear_axioms_def @@ -1770,14 +1767,14 @@ unfolding smult_conv_scaleR apply (rule ext) apply (subst matrix_works[OF lf, symmetric]) - apply (auto simp add: Cart_eq matrix_vector_mult_def column_def mult_commute) + apply (auto simp add: vec_eq_iff matrix_vector_mult_def column_def mult_commute) done lemma linear_to_scalars: assumes lf: "linear (f::real ^'n \ real^1)" shows "f = (\x. vec1(row 1 (matrix f) \ x))" apply (rule ext) apply (subst matrix_works[OF lf, symmetric]) - apply (simp add: Cart_eq matrix_vector_mult_def row_def inner_vector_def mult_commute) + apply (simp add: vec_eq_iff matrix_vector_mult_def row_def inner_vec_def mult_commute) done lemma dest_vec1_eq_0: "dest_vec1 x = 0 \ x = 0" @@ -1801,14 +1798,14 @@ using assms unfolding continuous_on_iff apply safe apply(erule_tac x="x$1" in ballE,erule_tac x=e in allE) apply safe apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real - apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:vector_le_def) + apply(erule_tac x="dest_vec1 x'" in ballE) by(auto simp add:less_eq_vec_def) lemma continuous_on_o_vec1: fixes f::"real^1 \ 'a::real_normed_vector" assumes "continuous_on {a..b} f" shows "continuous_on {dest_vec1 a..dest_vec1 b} (f o vec1)" using assms unfolding continuous_on_iff apply safe apply(erule_tac x="vec x" in ballE,erule_tac x=e in allE) apply safe apply(rule_tac x=d in exI) apply safe unfolding o_def dist_real_def dist_real - apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:vector_le_def) + apply(erule_tac x="vec1 x'" in ballE) by(auto simp add:less_eq_vec_def) lemma continuous_on_vec1:"continuous_on A (vec1::real\real^1)" by(rule linear_continuous_on[OF bounded_linear_vec1]) @@ -1816,12 +1813,12 @@ lemma mem_interval_1: fixes x :: "real^1" shows "(x \ {a .. b} \ dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b)" "(x \ {a<.. dest_vec1 a < dest_vec1 x \ dest_vec1 x < dest_vec1 b)" -by(simp_all add: Cart_eq vector_less_def vector_le_def) +by(simp_all add: vec_eq_iff less_vec_def less_eq_vec_def) lemma vec1_interval:fixes a::"real" shows "vec1 ` {a .. b} = {vec1 a .. vec1 b}" "vec1 ` {a<.. {a .. b} ==> x \ {a<.. (x = a) \ (x = b)" - unfolding Cart_eq vector_less_def vector_le_def mem_interval_cart by(auto simp del:dest_vec1_eq) + unfolding vec_eq_iff less_vec_def less_eq_vec_def mem_interval_cart by(auto simp del:dest_vec1_eq) lemma in_interval_1: fixes x :: "real^1" shows "(x \ {a .. b} \ dest_vec1 a \ dest_vec1 x \ dest_vec1 x \ dest_vec1 b) \ (x \ {a<.. dest_vec1 a < dest_vec1 x \ dest_vec1 x < dest_vec1 b)" - unfolding Cart_eq vector_less_def vector_le_def mem_interval_cart by(auto simp del:dest_vec1_eq) + unfolding vec_eq_iff less_vec_def less_eq_vec_def mem_interval_cart by(auto simp del:dest_vec1_eq) lemma interval_eq_empty_1: fixes a :: "real^1" shows "{a .. b} = {} \ dest_vec1 b < dest_vec1 a" @@ -1871,10 +1868,10 @@ lemma open_closed_interval_1: fixes a :: "real^1" shows "{a<.. dest_vec1 b ==> {a .. b} = {a<.. {a,b}" - unfolding set_eq_iff apply simp unfolding vector_less_def and vector_le_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq) + unfolding set_eq_iff apply simp unfolding less_vec_def and less_eq_vec_def and forall_1 and dest_vec1_eq[THEN sym] by(auto simp del:dest_vec1_eq) lemma Lim_drop_le: fixes f :: "'a \ real^1" shows "(f ---> l) net \ ~(trivial_limit net) \ eventually (\x. dest_vec1 (f x) \ b) net ==> dest_vec1 l \ b" @@ -1903,7 +1900,7 @@ lemma dest_vec1_simps[simp]: fixes a::"real^1" shows "a$1 = 0 \ a = 0" (*"a \ 1 \ dest_vec1 a \ 1" "0 \ a \ 0 \ dest_vec1 a"*) "a \ b \ dest_vec1 a \ dest_vec1 b" "dest_vec1 (1::real^1) = 1" - by(auto simp add: vector_le_def Cart_eq) + by(auto simp add: less_eq_vec_def vec_eq_iff) lemma dest_vec1_inverval: "dest_vec1 ` {a .. b} = {dest_vec1 a .. dest_vec1 b}" @@ -1915,18 +1912,18 @@ apply(rule_tac [!] allI)apply(rule_tac [!] impI) apply(rule_tac[2] x="vec1 x" in exI)apply(rule_tac[4] x="vec1 x" in exI) apply(rule_tac[6] x="vec1 x" in exI)apply(rule_tac[8] x="vec1 x" in exI) - by (auto simp add: vector_less_def vector_le_def) + by (auto simp add: less_vec_def less_eq_vec_def) lemma dest_vec1_setsum: assumes "finite S" shows " dest_vec1 (setsum f S) = setsum (\x. dest_vec1 (f x)) S" using dest_vec1_sum[OF assms] by auto lemma open_dest_vec1_vimage: "open S \ open (dest_vec1 -` S)" -unfolding open_vector_def forall_1 by auto +unfolding open_vec_def forall_1 by auto lemma tendsto_dest_vec1 [tendsto_intros]: "(f ---> l) net \ ((\x. dest_vec1 (f x)) ---> dest_vec1 l) net" -by(rule tendsto_Cart_nth) +by(rule tendsto_vec_nth) lemma continuous_dest_vec1: "continuous net f \ continuous net (\x. dest_vec1 (f x))" unfolding continuous_def by (rule tendsto_dest_vec1) @@ -1952,9 +1949,9 @@ unfolding vec1_dest_vec1_simps by auto qed lemma vec1_le[simp]:fixes a::real shows "vec1 a \ vec1 b \ a \ b" - unfolding vector_le_def by auto + unfolding less_eq_vec_def by auto lemma vec1_less[simp]:fixes a::real shows "vec1 a < vec1 b \ a < b" - unfolding vector_less_def by auto + unfolding less_vec_def by auto subsection {* Derivatives on real = Derivatives on @{typ "real^1"} *} @@ -1998,7 +1995,7 @@ lemma onorm_vec1: fixes f::"real \ real" shows "onorm (\x. vec1 (f (dest_vec1 x))) = onorm f" proof- - have "\x::real^1. norm x = 1 \ x\{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:Cart_eq) + have "\x::real^1. norm x = 1 \ x\{vec1 -1, vec1 (1::real)}" unfolding forall_vec1 by(auto simp add:vec_eq_iff) hence 1:"{x. norm x = 1} = {vec1 -1, vec1 (1::real)}" by auto have 2:"{norm (vec1 (f (dest_vec1 x))) |x. norm x = 1} = (\x. norm (vec1 (f (dest_vec1 x)))) ` {x. norm x=1}" by auto have "\x::real. norm x = 1 \ x\{-1, 1}" by auto hence 3:"{x. norm x = 1} = {-1, (1::real)}" by auto @@ -2037,11 +2034,11 @@ "{a..b::real^'n} \ {x. x$k \ c} = {a .. (\ i. if i = k then min (b$k) c else b$i)}" "{a..b} \ {x. x$k \ c} = {(\ i. if i = k then max (a$k) c else a$i) .. b}" apply(rule_tac[!] set_eqI) unfolding Int_iff mem_interval_cart mem_Collect_eq - unfolding Cart_lambda_beta by auto + unfolding vec_lambda_beta by auto (*lemma content_split_cart: "content {a..b::real^'n} = content({a..b} \ {x. x$k \ c}) + content({a..b} \ {x. x$k >= c})" -proof- note simps = interval_split_cart content_closed_interval_cases_cart Cart_lambda_beta vector_le_def +proof- note simps = interval_split_cart content_closed_interval_cases_cart vec_lambda_beta less_eq_vec_def { presume "a\b \ ?thesis" thus ?thesis apply(cases "a\b") unfolding simps by auto } have *:"UNIV = insert k (UNIV - {k})" "\x. finite (UNIV-{x::'n})" "\x. x\UNIV-{x}" by auto have *:"\X Y Z. (\i\UNIV. Z i (if i = k then X else Y i)) = Z k X * (\i\UNIV-{k}. Z i (Y i))" @@ -2051,7 +2048,7 @@ \ x* (b$k - a$k) = x*(max (a $ k) c - a $ k) + x*(b $ k - max (a $ k) c)" by (auto simp add:field_simps) moreover have "\ a $ k \ c \ \ c \ b $ k \ False" - unfolding not_le using as[unfolded vector_le_def,rule_format,of k] by auto + unfolding not_le using as[unfolded less_eq_vec_def,rule_format,of k] by auto ultimately show ?thesis unfolding simps unfolding *(1)[of "\i x. b$i - x"] *(1)[of "\i x. x - a$i"] *(2) by(auto) qed*) @@ -2059,7 +2056,7 @@ lemma has_integral_vec1: assumes "(f has_integral k) {a..b}" shows "((\x. vec1 (f x)) has_integral (vec1 k)) {a..b}" proof- have *:"\p. (\(x, k)\p. content k *\<^sub>R vec1 (f x)) - vec1 k = vec1 ((\(x, k)\p. content k *\<^sub>R f x) - k)" - unfolding vec_sub Cart_eq by(auto simp add: split_beta) + unfolding vec_sub vec_eq_iff by(auto simp add: split_beta) show ?thesis using assms unfolding has_integral apply safe apply(erule_tac x=e in allE,safe) apply(rule_tac x=d in exI,safe) apply(erule_tac x=p in allE,safe) unfolding * norm_vector_1 by auto qed diff -r 18b4ab6854f1 -r e63ad7d5158d src/HOL/Multivariate_Analysis/Fashoda.thy --- a/src/HOL/Multivariate_Analysis/Fashoda.thy Wed Aug 10 10:13:16 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Fashoda.thy Wed Aug 10 13:13:37 2011 -0700 @@ -46,7 +46,7 @@ apply(rule assms)+ apply(rule continuous_on_compose,subst sqprojection_def) apply(rule continuous_on_mul ) apply(rule continuous_at_imp_continuous_on,rule) apply(rule continuous_at_inv[unfolded o_def]) apply(rule continuous_at_infnorm) unfolding infnorm_eq_0 defer apply(rule continuous_on_id) apply(rule linear_continuous_on) proof- - show "bounded_linear negatex" apply(rule bounded_linearI') unfolding Cart_eq proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real + show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" apply-apply(case_tac[!] "i\1") prefer 3 apply(drule_tac[1-2] 21) unfolding negatex_def by(auto simp add:vector_2 ) qed qed(insert x0, auto) @@ -66,7 +66,7 @@ apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\0" have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)" - unfolding sqprojection_def vector_component_simps Cart_nth.scaleR real_scaleR_def + unfolding sqprojection_def vector_component_simps vec_nth.scaleR real_scaleR_def unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed note lem3 = this[rule_format] have x1:"x $ 1 \ {- 1..1::real}" "x $ 2 \ {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto @@ -77,7 +77,7 @@ next assume as:"x$1 = 1" hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" - using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]] + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] unfolding as negatex_def vector_2 by auto moreover from x1 have "g (x $ 2) \ {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart @@ -85,7 +85,7 @@ next assume as:"x$1 = -1" hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0" - using x(2)[unfolded o_def Cart_eq,THEN spec[where x=1]] + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] unfolding as negatex_def vector_2 by auto moreover from x1 have "g (x $ 2) \ {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart @@ -93,7 +93,7 @@ next assume as:"x$2 = 1" hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" - using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]] + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] unfolding as negatex_def vector_2 by auto moreover from x1 have "f (x $ 1) \ {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart @@ -101,7 +101,7 @@ next assume as:"x$2 = -1" hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" - using x(2)[unfolded o_def Cart_eq,THEN spec[where x=2]] + using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] unfolding as negatex_def vector_2 by auto moreover from x1 have "f (x $ 1) \ {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart @@ -120,7 +120,7 @@ have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+ show "continuous_on {- 1..1} (f \ iscale)" "continuous_on {- 1..1} (g \ iscale)" apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc]) - by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding Cart_eq by auto + by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding vec_eq_iff by auto show "(f \ iscale) (- 1) $ 1 = - 1" "(f \ iscale) 1 $ 1 = 1" "(g \ iscale) (- 1) $ 2 = -1" "(g \ iscale) 1 $ 2 = 1" unfolding o_def iscale_def using assms by(auto simp add:*) qed then guess s .. from this(2) guess t .. note st=this @@ -132,7 +132,7 @@ (* move *) lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\i. a$i < b$i \ u$i < v$i" shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x" - unfolding interval_bij_cart split_conv Cart_eq Cart_lambda_beta + unfolding interval_bij_cart split_conv vec_eq_iff vec_lambda_beta apply(rule,insert assms,erule_tac x=i in allE) by auto lemma fashoda: fixes b::"real^2" @@ -142,23 +142,23 @@ obtains z where "z \ path_image f" "z \ path_image g" proof- fix P Q S presume "P \ Q \ S" "P \ thesis" "Q \ thesis" "S \ thesis" thus thesis by auto next have "{a..b} \ {}" using assms(3) using path_image_nonempty by auto - hence "a \ b" unfolding interval_eq_empty_cart vector_le_def by(auto simp add: not_less) - thus "a$1 = b$1 \ a$2 = b$2 \ (a$1 < b$1 \ a$2 < b$2)" unfolding vector_le_def forall_2 by auto + hence "a \ b" unfolding interval_eq_empty_cart less_eq_vec_def by(auto simp add: not_less) + thus "a$1 = b$1 \ a$2 = b$2 \ (a$1 < b$1 \ a$2 < b$2)" unfolding less_eq_vec_def forall_2 by auto next assume as:"a$1 = b$1" have "\z\path_image g. z$2 = (pathstart f)$2" apply(rule connected_ivt_component_cart) apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image) unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"] - unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this + unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this have "z \ {a..b}" using z(1) assms(4) unfolding path_image_def by blast - hence "z = f 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def + hence "z = f 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def using assms(3)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "f 0" 1] unfolding mem_interval_cart apply(erule_tac x=1 in allE) using as by auto thus thesis apply-apply(rule that[OF _ z(1)]) unfolding path_image_def by auto next assume as:"a$2 = b$2" have "\z\path_image f. z$1 = (pathstart g)$1" apply(rule connected_ivt_component_cart) apply(rule connected_path_image assms)+apply(rule pathstart_in_path_image,rule pathfinish_in_path_image) unfolding assms using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"] - unfolding pathstart_def by(auto simp add: vector_le_def) then guess z .. note z=this + unfolding pathstart_def by(auto simp add: less_eq_vec_def) then guess z .. note z=this have "z \ {a..b}" using z(1) assms(3) unfolding path_image_def by blast - hence "z = g 0" unfolding Cart_eq forall_2 unfolding z(2) pathstart_def + hence "z = g 0" unfolding vec_eq_iff forall_2 unfolding z(2) pathstart_def using assms(4)[unfolded path_image_def subset_eq mem_interval_cart,rule_format,of "g 0" 2] unfolding mem_interval_cart apply(erule_tac x=2 in allE) using as by auto thus thesis apply-apply(rule that[OF z(1)]) unfolding path_image_def by auto @@ -180,7 +180,7 @@ "(interval_bij (a, b) (- 1, 1) \ f) 1 $ 1 = 1" "(interval_bij (a, b) (- 1, 1) \ g) 0 $ 2 = -1" "(interval_bij (a, b) (- 1, 1) \ g) 1 $ 2 = 1" - unfolding interval_bij_cart Cart_lambda_beta vector_component_simps o_def split_conv + unfolding interval_bij_cart vec_lambda_beta vector_component_simps o_def split_conv unfolding assms[unfolded pathstart_def pathfinish_def] using as by auto qed note z=this from z(1) guess zf unfolding image_iff .. note zf=this from z(2) guess zg unfolding image_iff .. note zg=this @@ -197,7 +197,7 @@ proof- let ?L = "\u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \ x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \ 0 \ u \ u \ 1" { presume "?L \ ?R" "?R \ ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq - unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast } + unfolding vec_eq_iff forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast } { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this { fix b a assume "b + u * a > a + u * b" hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps) @@ -221,7 +221,7 @@ proof- let ?L = "\u. (x $ 1 = (1 - u) * a $ 1 + u * b $ 1 \ x $ 2 = (1 - u) * a $ 2 + u * b $ 2) \ 0 \ u \ u \ 1" { presume "?L \ ?R" "?R \ ?L" thus ?thesis unfolding closed_segment_def mem_Collect_eq - unfolding Cart_eq forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast } + unfolding vec_eq_iff forall_2 smult_conv_scaleR[THEN sym] vector_component_simps by blast } { assume ?L then guess u apply-apply(erule exE)apply(erule conjE)+ . note u=this { fix b a assume "b + u * a > a + u * b" hence "(1 - u) * b > (1 - u) * a" by(auto simp add:field_simps) @@ -274,7 +274,7 @@ path_image(linepath(vector[(pathfinish g)$1,a$2 - 1])(vector[b$1 + 1,a$2 - 1])) \ path_image(linepath(vector[b$1 + 1,a$2 - 1])(vector[b$1 + 1,b$2 + 3]))" using assms(1-2) by(auto simp add: path_image_join path_linepath) - have abab: "{a..b} \ {?a..?b}" by(auto simp add:vector_le_def forall_2 vector_2) + have abab: "{a..b} \ {?a..?b}" by(auto simp add:less_eq_vec_def forall_2 vector_2) guess z apply(rule fashoda[of ?P1 ?P2 ?a ?b]) unfolding pathstart_join pathfinish_join pathstart_linepath pathfinish_linepath vector_2 proof- show "path ?P1" "path ?P2" using assms by auto @@ -318,11 +318,11 @@ qed hence "z \ path_image f \ z \ path_image g" using z unfolding Un_iff by blast hence z':"z\{a..b}" using assms(3-4) by auto have "a $ 2 = z $ 2 \ (z $ 1 = pathstart f $ 1 \ z $ 1 = pathfinish f $ 1) \ (z = pathstart f \ z = pathfinish f)" - unfolding Cart_eq forall_2 assms by auto + unfolding vec_eq_iff forall_2 assms by auto with z' show "z\path_image f" using z(1) unfolding Un_iff mem_interval_cart forall_2 apply- apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto have "a $ 2 = z $ 2 \ (z $ 1 = pathstart g $ 1 \ z $ 1 = pathfinish g $ 1) \ (z = pathstart g \ z = pathfinish g)" - unfolding Cart_eq forall_2 assms by auto + unfolding vec_eq_iff forall_2 assms by auto with z' show "z\path_image g" using z(2) unfolding Un_iff mem_interval_cart forall_2 apply- apply(simp only: segment_vertical segment_horizontal vector_2) unfolding assms by auto qed qed diff -r 18b4ab6854f1 -r e63ad7d5158d src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Aug 10 10:13:16 2011 -0700 +++ b/src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy Wed Aug 10 13:13:37 2011 -0700 @@ -13,148 +13,148 @@ subsection {* Finite Cartesian products, with indexing and lambdas. *} -typedef (open Cart) - ('a, 'b) cart = "UNIV :: (('b::finite) \ 'a) set" - morphisms Cart_nth Cart_lambda .. +typedef (open) + ('a, 'b) vec = "UNIV :: (('b::finite) \ 'a) set" + morphisms vec_nth vec_lambda .. notation - Cart_nth (infixl "$" 90) and - Cart_lambda (binder "\" 10) + vec_nth (infixl "$" 90) and + vec_lambda (binder "\" 10) (* Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than - the finite type class write "cart 'b 'n" + the finite type class write "vec 'b 'n" *) -syntax "_finite_cart" :: "type \ type \ type" ("(_ ^/ _)" [15, 16] 15) +syntax "_finite_vec" :: "type \ type \ type" ("(_ ^/ _)" [15, 16] 15) parse_translation {* let - fun cart t u = Syntax.const @{type_syntax cart} $ t $ u; - fun finite_cart_tr [t, u as Free (x, _)] = + fun vec t u = Syntax.const @{type_syntax vec} $ t $ u; + fun finite_vec_tr [t, u as Free (x, _)] = if Lexicon.is_tid x then - cart t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite}) - else cart t u - | finite_cart_tr [t, u] = cart t u + vec t (Syntax.const @{syntax_const "_ofsort"} $ u $ Syntax.const @{class_syntax finite}) + else vec t u + | finite_vec_tr [t, u] = vec t u in - [(@{syntax_const "_finite_cart"}, finite_cart_tr)] + [(@{syntax_const "_finite_vec"}, finite_vec_tr)] end *} lemma stupid_ext: "(\x. f x = g x) \ (f = g)" by (auto intro: ext) -lemma Cart_eq: "(x = y) \ (\i. x$i = y$i)" - by (simp add: Cart_nth_inject [symmetric] fun_eq_iff) +lemma vec_eq_iff: "(x = y) \ (\i. x$i = y$i)" + by (simp add: vec_nth_inject [symmetric] fun_eq_iff) -lemma Cart_lambda_beta [simp]: "Cart_lambda g $ i = g i" - by (simp add: Cart_lambda_inverse) +lemma vec_lambda_beta [simp]: "vec_lambda g $ i = g i" + by (simp add: vec_lambda_inverse) -lemma Cart_lambda_unique: "(\i. f$i = g i) \ Cart_lambda g = f" - by (auto simp add: Cart_eq) +lemma vec_lambda_unique: "(\i. f$i = g i) \ vec_lambda g = f" + by (auto simp add: vec_eq_iff) -lemma Cart_lambda_eta: "(\ i. (g$i)) = g" - by (simp add: Cart_eq) +lemma vec_lambda_eta: "(\ i. (g$i)) = g" + by (simp add: vec_eq_iff) subsection {* Group operations and class instances *} -instantiation cart :: (zero,finite) zero +instantiation vec :: (zero, finite) zero begin - definition vector_zero_def : "0 \ (\ i. 0)" + definition "0 \ (\ i. 0)" instance .. end -instantiation cart :: (plus,finite) plus +instantiation vec :: (plus, finite) plus begin - definition vector_add_def : "op + \ (\ x y. (\ i. (x$i) + (y$i)))" + definition "op + \ (\ x y. (\ i. x$i + y$i))" instance .. end -instantiation cart :: (minus,finite) minus +instantiation vec :: (minus, finite) minus begin - definition vector_minus_def : "op - \ (\ x y. (\ i. (x$i) - (y$i)))" + definition "op - \ (\ x y. (\ i. x$i - y$i))" instance .. end -instantiation cart :: (uminus,finite) uminus +instantiation vec :: (uminus, finite) uminus begin - definition vector_uminus_def : "uminus \ (\ x. (\ i. - (x$i)))" + definition "uminus \ (\ x. (\ i. - (x$i)))" instance .. end lemma zero_index [simp]: "0 $ i = 0" - unfolding vector_zero_def by simp + unfolding zero_vec_def by simp lemma vector_add_component [simp]: "(x + y)$i = x$i + y$i" - unfolding vector_add_def by simp + unfolding plus_vec_def by simp lemma vector_minus_component [simp]: "(x - y)$i = x$i - y$i" - unfolding vector_minus_def by simp + unfolding minus_vec_def by simp lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" - unfolding vector_uminus_def by simp + unfolding uminus_vec_def by simp -instance cart :: (semigroup_add, finite) semigroup_add - by default (simp add: Cart_eq add_assoc) +instance vec :: (semigroup_add, finite) semigroup_add + by default (simp add: vec_eq_iff add_assoc) -instance cart :: (ab_semigroup_add, finite) ab_semigroup_add - by default (simp add: Cart_eq add_commute) +instance vec :: (ab_semigroup_add, finite) ab_semigroup_add + by default (simp add: vec_eq_iff add_commute) -instance cart :: (monoid_add, finite) monoid_add - by default (simp_all add: Cart_eq) +instance vec :: (monoid_add, finite) monoid_add + by default (simp_all add: vec_eq_iff) -instance cart :: (comm_monoid_add, finite) comm_monoid_add - by default (simp add: Cart_eq) +instance vec :: (comm_monoid_add, finite) comm_monoid_add + by default (simp add: vec_eq_iff) -instance cart :: (cancel_semigroup_add, finite) cancel_semigroup_add - by default (simp_all add: Cart_eq) +instance vec :: (cancel_semigroup_add, finite) cancel_semigroup_add + by default (simp_all add: vec_eq_iff) -instance cart :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add - by default (simp add: Cart_eq) +instance vec :: (cancel_ab_semigroup_add, finite) cancel_ab_semigroup_add + by default (simp add: vec_eq_iff) -instance cart :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. +instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. -instance cart :: (group_add, finite) group_add - by default (simp_all add: Cart_eq diff_minus) +instance vec :: (group_add, finite) group_add + by default (simp_all add: vec_eq_iff diff_minus) -instance cart :: (ab_group_add, finite) ab_group_add - by default (simp_all add: Cart_eq) +instance vec :: (ab_group_add, finite) ab_group_add + by default (simp_all add: vec_eq_iff) subsection {* Real vector space *} -instantiation cart :: (real_vector, finite) real_vector +instantiation vec :: (real_vector, finite) real_vector begin -definition vector_scaleR_def: "scaleR = (\ r x. (\ i. scaleR r (x$i)))" +definition "scaleR \ (\ r x. (\