Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
--- 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 = "\<lambda>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 (\<lambda>i. ?di (transp A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transp A) i (inv p i)) (p ` ?U)" by simp
- also have "\<dots> = setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U"
+ have "setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp
+ also have "\<dots> = setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U"
unfolding setprod_reindex[OF pi] ..
also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U"
proof-
{fix i assume i: "i \<in> ?U"
from i permutes_inv_o[OF pU] permutes_in_image[OF pU]
- have "((\<lambda>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 ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
+ have "((\<lambda>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 ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
qed
- finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth
+ finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>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(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A"
proof-
let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n"
- let ?At = "transp A"
- have "of_int (sign p) * det A = det (transp (\<chi> 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 (\<chi> i. transpose A $ p i))"
+ unfolding det_permute_rows[OF p, of ?At] det_transpose ..
moreover
- have "?Ap = transp (\<chi> i. transp A $ p i)"
- by (simp add: transp_def Cart_eq)
+ have "?Ap = transpose (\<chi> 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 \<noteq> 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 \<Rightarrow> _ ^ '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 ((\<chi> i. if i = k then setsum (\<lambda>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((\<chi> 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: "\<And>c. setsum (\<lambda>i. c i *s row i (transp A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U"
- by (auto simp add: row_transp intro: setsum_cong2)
+ have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transpose A)) ?U = setsum (\<lambda>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 "\<lambda>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) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1"
+definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
-lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1"
+lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> 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: "\<forall>v w. f v \<bullet> f w = v \<bullet> w"
unfolding orthogonal_transformation_def orthogonal_matrix by blast+
{fix i j
- let ?A = "transp ?mf ** ?mf"
+ let ?A = "transpose ?mf ** ?mf"
have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
"\<And>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 "\<dots> \<longleftrightarrow> x = 1 \<or> 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
--- 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 == (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n"
definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)"
-definition "(transp::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
+definition transpose where
+ "(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))"
definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))"
definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (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 (\<lambda>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(\<lambda>x. (A::'a::comm_ring_1^'n^'m) *v x) = (\<lambda>x. transp A *v x)"
+lemma matrix_vector_column:"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>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(\<lambda>x. (A::'a::comm_ring_1^'n^'m) *v x) = (\<lambda>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 \<Rightarrow> '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:
- "(\<exists>(B). B ** transp (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
- by (metis matrix_transp_mul transp_mat transp_transp)
-
-lemma right_invertible_transp:
- "(\<exists>(B). transp (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
- by (metis matrix_transp_mul transp_mat transp_transp)
+lemma left_invertible_transpose:
+ "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
+ by (metis matrix_transpose_mul transpose_mat transpose_transpose)
+
+lemma right_invertible_transpose:
+ "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(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 \<Rightarrow> real ^'m)" and fi: "inj f"
@@ -4438,9 +4439,9 @@
lemma matrix_right_invertible_independent_rows:
fixes A :: "real^'n^'m"
shows "(\<exists>(B::real^'m^'n). A ** B = mat 1) \<longleftrightarrow> (\<forall>c. setsum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>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:
"(\<exists>(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> span (columns A) = UNIV" (is "?lhs = ?rhs")
@@ -4506,8 +4507,8 @@
lemma matrix_left_invertible_span_rows:
"(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> 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 = (\<chi> 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) \<bullet> (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. *)