# HG changeset patch # User hoelzl # Date 1266329793 -3600 # Node ID 082fa4bd403d133425b472d402bf318a44853fa0 # Parent ad213c602ec113c91a7ee2918893734b1d49f86b Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma) diff -r ad213c602ec1 -r 082fa4bd403d src/HOL/Multivariate_Analysis/Determinants.thy --- a/src/HOL/Multivariate_Analysis/Determinants.thy Mon Feb 15 23:58:24 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Determinants.thy Tue Feb 16 15:16:33 2010 +0100 @@ -121,7 +121,7 @@ (* Basic determinant properties. *) (* ------------------------------------------------------------------------- *) -lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n)" +lemma det_transpose: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" proof- let ?di = "\A i j. A$i$j" let ?U = "(UNIV :: 'n set)" @@ -133,18 +133,18 @@ from permutes_inj[OF pU] have pi: "inj_on p ?U" by (blast intro: subset_inj_on) from permutes_image[OF pU] - have "setprod (\i. ?di (transp A) i (inv p i)) ?U = setprod (\i. ?di (transp A) i (inv p i)) (p ` ?U)" by simp - also have "\ = setprod ((\i. ?di (transp A) i (inv p i)) o p) ?U" + have "setprod (\i. ?di (transpose A) i (inv p i)) ?U = setprod (\i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp + also have "\ = setprod ((\i. ?di (transpose A) i (inv p i)) o p) ?U" unfolding setprod_reindex[OF pi] .. also have "\ = setprod (\i. ?di A i (p i)) ?U" proof- {fix i assume i: "i \ ?U" from i permutes_inv_o[OF pU] permutes_in_image[OF pU] - have "((\i. ?di (transp A) i (inv p i)) o p) i = ?di A i (p i)" - unfolding transp_def by (simp add: expand_fun_eq)} - then show "setprod ((\i. ?di (transp A) i (inv p i)) o p) ?U = setprod (\i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) + have "((\i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)" + unfolding transpose_def by (simp add: expand_fun_eq)} + then show "setprod ((\i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) qed - finally have "of_int (sign (inv p)) * (setprod (\i. ?di (transp A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" using sth + finally have "of_int (sign (inv p)) * (setprod (\i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" using sth by simp} then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse) apply (rule setsum_cong2) by blast @@ -267,12 +267,12 @@ shows "det(\ i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" proof- let ?Ap = "\ i j. A$i$ p j :: 'a^'n^'n" - let ?At = "transp A" - have "of_int (sign p) * det A = det (transp (\ i. transp A $ p i))" - unfolding det_permute_rows[OF p, of ?At] det_transp .. + let ?At = "transpose A" + have "of_int (sign p) * det A = det (transpose (\ i. transpose A $ p i))" + unfolding det_permute_rows[OF p, of ?At] det_transpose .. moreover - have "?Ap = transp (\ i. transp A $ p i)" - by (simp add: transp_def Cart_eq) + have "?Ap = transpose (\ i. transpose A $ p i)" + by (simp add: transpose_def Cart_eq) ultimately show ?thesis by simp qed @@ -299,9 +299,9 @@ assumes ij: "i \ j" and r: "column i A = column j A" shows "det A = 0" -apply (subst det_transp[symmetric]) +apply (subst det_transpose[symmetric]) apply (rule det_identical_rows[OF ij]) -by (metis row_transp r) +by (metis row_transpose r) lemma det_zero_row: fixes A :: "'a::{idom, ring_char_0}^'n^'n" @@ -317,9 +317,9 @@ fixes A :: "'a::{idom,ring_char_0}^'n^'n" assumes r: "column i A = 0" shows "det A = 0" - apply (subst det_transp[symmetric]) + apply (subst det_transpose[symmetric]) apply (rule det_zero_row [of i]) - by (metis row_transp r) + by (metis row_transpose r) lemma det_row_add: fixes a b c :: "'n::finite \ _ ^ 'n" @@ -489,7 +489,7 @@ qed lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::linordered_idom^'n^'n))" shows "det A = 0" -by (metis d det_dependent_rows rows_transp det_transp) +by (metis d det_dependent_rows rows_transpose det_transpose) (* ------------------------------------------------------------------------- *) (* Multilinearity and the multiplication formula. *) @@ -760,7 +760,7 @@ (* Cramer's rule. *) (* ------------------------------------------------------------------------- *) -lemma cramer_lemma_transp: +lemma cramer_lemma_transpose: fixes A:: "'a::linordered_idom^'n^'n" and x :: "'a ^'n" shows "det ((\ i. if i = k then setsum (\i. x$i *s row i A) (UNIV::'n set) else row i A)::'a^'n^'n) = x$k * det A" @@ -801,13 +801,13 @@ shows "det((\ i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A" proof- let ?U = "UNIV :: 'n set" - have stupid: "\c. setsum (\i. c i *s row i (transp A)) ?U = setsum (\i. c i *s column i A) ?U" - by (auto simp add: row_transp intro: setsum_cong2) + have stupid: "\c. setsum (\i. c i *s row i (transpose A)) ?U = setsum (\i. c i *s column i A) ?U" + by (auto simp add: row_transpose intro: setsum_cong2) show ?thesis unfolding matrix_mult_vsum - unfolding cramer_lemma_transp[of k x "transp A", unfolded det_transp, symmetric] + unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] unfolding stupid[of "\i. x$i"] - apply (subst det_transp[symmetric]) - apply (rule cong[OF refl[of det]]) by (vector transp_def column_def row_def) + apply (subst det_transpose[symmetric]) + apply (rule cong[OF refl[of det]]) by (vector transpose_def column_def row_def) qed lemma cramer: @@ -840,13 +840,13 @@ apply (simp add: real_vector_norm_def) by (simp add: dot_norm linear_add[symmetric]) -definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \ transp Q ** Q = mat 1 \ Q ** transp Q = mat 1" +definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \ transpose Q ** Q = mat 1 \ Q ** transpose Q = mat 1" -lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transp Q ** Q = mat 1" +lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transpose Q ** Q = mat 1" by (metis matrix_left_right_inverse orthogonal_matrix_def) lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)" - by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid) + by (simp add: orthogonal_matrix_def transpose_mat matrix_mul_lid) lemma orthogonal_matrix_mul: fixes A :: "real ^'n^'n" @@ -854,7 +854,7 @@ and oB: "orthogonal_matrix B" shows "orthogonal_matrix(A ** B)" using oA oB - unfolding orthogonal_matrix matrix_transp_mul + unfolding orthogonal_matrix matrix_transpose_mul apply (subst matrix_mul_assoc) apply (subst matrix_mul_assoc[symmetric]) by (simp add: matrix_mul_rid) @@ -873,7 +873,7 @@ from ot have lf: "linear f" and fd: "\v w. f v \ f w = v \ w" unfolding orthogonal_transformation_def orthogonal_matrix by blast+ {fix i j - let ?A = "transp ?mf ** ?mf" + let ?A = "transpose ?mf ** ?mf" have th0: "\b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" "\b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" by simp_all @@ -908,9 +908,9 @@ also have "\ \ x = 1 \ x = - 1" unfolding th0 th1 by simp finally show "?ths x" .. qed - from oQ have "Q ** transp Q = mat 1" by (metis orthogonal_matrix_def) - hence "det (Q ** transp Q) = det (mat 1:: 'a^'n^'n)" by simp - hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transp) + from oQ have "Q ** transpose Q = mat 1" by (metis orthogonal_matrix_def) + hence "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" by simp + hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transpose) then show ?thesis unfolding th . qed diff -r ad213c602ec1 -r 082fa4bd403d src/HOL/Multivariate_Analysis/Euclidean_Space.thy --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Mon Feb 15 23:58:24 2010 +0100 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy Tue Feb 16 15:16:33 2010 +0100 @@ -2029,7 +2029,8 @@ where "v v* m == (\ j. setsum (\i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n" definition "(mat::'a::zero => 'a ^'n^'n) k = (\ i j. if i = j then k else 0)" -definition "(transp::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A$j)$i))" +definition transpose where + "(transpose::'a^'n^'m \ 'a^'m^'n) A = (\ i j. ((A$j)$i))" definition "(row::'m => 'a ^'n^'m \ 'a ^'n) i A = (\ j. ((A$i)$j))" definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\ i. ((A$i)$j))" definition "rows(A::'a^'n^'m) = { row i A | i. i \ (UNIV :: 'm set)}" @@ -2071,8 +2072,8 @@ by (simp add: cond_value_iff cond_application_beta setsum_delta' cong del: if_weak_cong) -lemma matrix_transp_mul: "transp(A ** B) = transp B ** transp (A::'a::comm_semiring_1^_^_)" - by (simp add: matrix_matrix_mult_def transp_def Cart_eq mult_commute) +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) lemma matrix_eq: fixes A B :: "'a::semiring_1 ^ 'n ^ 'm" @@ -2094,26 +2095,26 @@ apply (subst setsum_commute) by simp -lemma transp_mat: "transp (mat n) = mat n" - by (vector transp_def mat_def) - -lemma transp_transp: "transp(transp A) = A" - by (vector transp_def) - -lemma row_transp: +lemma transpose_mat: "transpose (mat n) = mat n" + by (vector transpose_def mat_def) + +lemma transpose_transpose: "transpose(transpose A) = A" + by (vector transpose_def) + +lemma row_transpose: fixes A:: "'a::semiring_1^_^_" - shows "row i (transp A) = column i A" - by (simp add: row_def column_def transp_def Cart_eq) - -lemma column_transp: + shows "row i (transpose A) = column i A" + by (simp add: row_def column_def transpose_def Cart_eq) + +lemma column_transpose: fixes A:: "'a::semiring_1^_^_" - shows "column i (transp A) = row i A" - by (simp add: row_def column_def transp_def Cart_eq) - -lemma rows_transp: "rows(transp (A::'a::semiring_1^_^_)) = columns A" -by (auto simp add: rows_def columns_def row_transp intro: set_ext) - -lemma columns_transp: "columns(transp (A::'a::semiring_1^_^_)) = rows A" by (metis transp_transp rows_transp) + shows "column i (transpose A) = row i A" + by (simp add: row_def column_def transpose_def Cart_eq) + +lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A" +by (auto simp add: rows_def columns_def row_transpose intro: set_ext) + +lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" by (metis transpose_transpose rows_transpose) text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *} @@ -2176,19 +2177,19 @@ using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] 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 ((transp A)$i)) (UNIV:: 'n set)" - by (simp add: matrix_vector_mult_def transp_def Cart_eq mult_commute) - -lemma adjoint_matrix: "adjoint(\x. (A::'a::comm_ring_1^'n^'m) *v x) = (\x. transp A *v x)" +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) + +lemma adjoint_matrix: "adjoint(\x. (A::'a::comm_ring_1^'n^'m) *v x) = (\x. transpose A *v x)" apply (rule adjoint_unique[symmetric]) apply (rule matrix_vector_mul_linear) - apply (simp add: transp_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) + apply (simp add: transpose_def dot_def matrix_vector_mult_def setsum_left_distrib setsum_right_distrib) apply (subst setsum_commute) apply (auto simp add: mult_ac) done lemma matrix_adjoint: assumes lf: "linear (f :: 'a::comm_ring_1^'n \ 'a ^'m)" - shows "matrix(adjoint f) = transp(matrix f)" + shows "matrix(adjoint f) = transpose(matrix f)" apply (subst matrix_vector_mul[OF lf]) unfolding adjoint_matrix matrix_of_matrix_vector_mul .. @@ -4317,13 +4318,13 @@ (* Detailed theorems about left and right invertibility in general case. *) -lemma left_invertible_transp: - "(\(B). B ** transp (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" - by (metis matrix_transp_mul transp_mat transp_transp) - -lemma right_invertible_transp: - "(\(B). transp (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(B). B ** A = mat 1)" - by (metis matrix_transp_mul transp_mat transp_transp) +lemma left_invertible_transpose: + "(\(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" + by (metis matrix_transpose_mul transpose_mat transpose_transpose) + +lemma right_invertible_transpose: + "(\(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(B). B ** A = mat 1)" + by (metis matrix_transpose_mul transpose_mat transpose_transpose) lemma linear_injective_left_inverse: assumes lf: "linear (f::real ^'n \ real ^'m)" and fi: "inj f" @@ -4438,9 +4439,9 @@ lemma matrix_right_invertible_independent_rows: fixes A :: "real^'n^'m" shows "(\(B::real^'m^'n). A ** B = mat 1) \ (\c. setsum (\i. c i *s row i A) (UNIV :: 'm set) = 0 \ (\i. c i = 0))" - unfolding left_invertible_transp[symmetric] + unfolding left_invertible_transpose[symmetric] matrix_left_invertible_independent_columns - by (simp add: column_transp) + by (simp add: column_transpose) lemma matrix_right_invertible_span_columns: "(\(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \ span (columns A) = UNIV" (is "?lhs = ?rhs") @@ -4506,8 +4507,8 @@ lemma matrix_left_invertible_span_rows: "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" - unfolding right_invertible_transp[symmetric] - unfolding columns_transp[symmetric] + unfolding right_invertible_transpose[symmetric] + unfolding columns_transpose[symmetric] unfolding matrix_right_invertible_span_columns .. @@ -4728,12 +4729,12 @@ definition "columnvector v = (\ i j. (v$i))" -lemma transp_columnvector: - "transp(columnvector v) = rowvector v" - by (simp add: transp_def rowvector_def columnvector_def Cart_eq) - -lemma transp_rowvector: "transp(rowvector v) = columnvector v" - by (simp add: transp_def columnvector_def rowvector_def Cart_eq) +lemma transpose_columnvector: + "transpose(columnvector v) = rowvector v" + by (simp add: transpose_def rowvector_def columnvector_def Cart_eq) + +lemma transpose_rowvector: "transpose(rowvector v) = columnvector v" + by (simp add: transpose_def columnvector_def rowvector_def Cart_eq) lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" @@ -4745,9 +4746,9 @@ lemma dot_matrix_vector_mul: fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" shows "(A *v x) \ (B *v y) = - (((rowvector x :: real^'n^1) ** ((transp A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" -unfolding dot_matrix_product transp_columnvector[symmetric] - dot_rowvector_columnvector matrix_transp_mul matrix_mul_assoc .. + (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" +unfolding dot_matrix_product transpose_columnvector[symmetric] + dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc .. (* Infinity norm. *)