header{*Miscellaneous*}
theory Miscellaneous
imports "~~/src/HOL/Multivariate_Analysis/Multivariate_Analysis"
begin
subsection{*Definitions of number of rows and columns of a matrix*}
definition nrows :: "'a^'columns^'rows => nat"
where "nrows A = CARD('rows)"
definition ncols :: "'a^'columns^'rows => nat"
where "ncols A = CARD('columns)"
subsection{*Basic properties about matrices*}
lemma nrows_not_0[simp]:
shows "0 ≠ nrows A" unfolding nrows_def by simp
lemma ncols_not_0[simp]:
shows "0 ≠ ncols A" unfolding ncols_def by simp
lemma nrows_transpose: "nrows (transpose A) = ncols A"
unfolding nrows_def ncols_def ..
lemma ncols_transpose: "ncols (transpose A) = nrows A"
unfolding nrows_def ncols_def ..
lemma finite_rows: "finite (rows A)"
using finite_Atleast_Atmost_nat[of "λi. row i A"] unfolding rows_def .
lemma finite_columns: "finite (columns A)"
using finite_Atleast_Atmost_nat[of "λi. column i A"] unfolding columns_def .
lemma matrix_vector_zero: "A *v 0 = 0"
unfolding matrix_vector_mult_def by (simp add: zero_vec_def)
lemma vector_matrix_zero: "0 v* A = 0"
unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
lemma vector_matrix_zero': "x v* 0 = 0"
unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
lemma transpose_vector: "x v* A = transpose A *v x"
by (unfold matrix_vector_mult_def vector_matrix_mult_def transpose_def, auto)
lemma transpose_zero[simp]: "(transpose A = 0) = (A = 0)"
unfolding transpose_def zero_vec_def vec_eq_iff by auto
subsection{*Theorems obtained from the AFP*}
text{*The following seven theorems have been obtained from the AFP \url{http://afp.sourceforge.net/browser_info/current/HOL/Tarskis_Geometry/Linear_Algebra2.html}.
I have removed some restrictions over the type classes.*}
lemma vector_matrix_left_distrib:
shows "(x + y) v* A = x v* A + y v* A"
unfolding vector_matrix_mult_def
by (simp add: algebra_simps setsum_addf vec_eq_iff)
lemma matrix_vector_right_distrib:
shows "M *v (v + w) = M *v v + M *v w"
proof -
have "M *v (v + w) = (v + w) v* transpose M" by (metis transpose_transpose transpose_vector)
also have "… = v v* transpose M + w v* transpose M"
by (rule vector_matrix_left_distrib [of v w "transpose M"])
finally show "M *v (v + w) = M *v v + M *v w" by (metis transpose_transpose transpose_vector)
qed
lemma scalar_vector_matrix_assoc:
fixes k :: real and x :: "'a::{semiring_1, real_algebra}^('n::finite)" and A :: "'a^('m::finite)^'n"
shows "(k *⇩R x) v* A = k *⇩R (x v* A)"
by (unfold vector_matrix_mult_def vec_eq_iff, auto simp add: scaleR_setsum_right)
lemma vector_scalar_matrix_ac:
fixes k :: real and x :: "'a::{semiring_1, real_algebra}^('n::finite)" and A :: "'a^('m::finite)^'n"
shows "x v* (k *⇩R A) = k *⇩R (x v* A)"
using scalar_vector_matrix_assoc unfolding vector_matrix_mult_def by auto
lemma transpose_scalar: "transpose (k *⇩R A) = k *⇩R transpose A"
unfolding transpose_def
by (simp add: vec_eq_iff)
lemma scalar_matrix_vector_assoc:
fixes A :: "'a::{semiring_1, real_algebra}^('m::finite)^('n::finite)"
shows "k *⇩R (A *v v) = k *⇩R A *v v"
proof -
have "k *⇩R (A *v v) = k *⇩R (v v* transpose A)" by (metis transpose_transpose transpose_vector)
also have "… = v v* k *⇩R transpose A"
by (rule vector_scalar_matrix_ac [symmetric])
also have "… = v v* transpose (k *⇩R A)" unfolding transpose_scalar ..
finally show "k *⇩R (A *v v) = k *⇩R A *v v" by (metis transpose_transpose transpose_vector)
qed
lemma matrix_scalar_vector_ac:
fixes A :: "'a::{semiring_1, real_algebra}^('m::finite)^('n::finite)"
shows "A *v (k *⇩R v) = k *⇩R A *v v"
proof -
have "A *v (k *⇩R v) = k *⇩R (v v* transpose A)" by (metis transpose_transpose scalar_vector_matrix_assoc transpose_vector)
also have "… = v v* k *⇩R transpose A"
by (subst vector_scalar_matrix_ac) simp
also have "… = v v* transpose (k *⇩R A)" by (subst transpose_scalar) simp
also have "… = k *⇩R A *v v" by (metis transpose_transpose transpose_vector)
finally show "A *v (k *⇩R v) = k *⇩R A *v v" .
qed
text{*Here ends the theorems obtained from AFP.*}
text{*The following definitions and lemmas are also obtained from AFP: \url{http://afp.sourceforge.net/browser_info/current/HOL/Tarskis_Geometry/Linear_Algebra2.html}*}
definition
is_basis :: "(real^('n::finite)) set => bool" where
"is_basis S ≡ independent S ∧ span S = UNIV"
lemma card_finite:
assumes "card S = CARD('n::finite)"
shows "finite S"
proof -
from `card S = CARD('n)` have "card S ≠ 0" by simp
with card_eq_0_iff [of S] show "finite S" by simp
qed
lemma independent_is_basis:
fixes B :: "(real^('n::finite)) set"
shows "independent B ∧ card B = CARD('n) <-> is_basis B"
proof
assume "independent B ∧ card B = CARD('n)"
hence "independent B" and "card B = CARD('n)" by simp+
from card_finite [of B, where 'n = 'n] and `card B = CARD('n)`
have "finite B" by simp
from `card B = CARD('n)`
have "card B = dim (UNIV :: ((real^'n) set))"
by (simp add: dim_UNIV)
with card_eq_dim [of B UNIV] and `finite B` and `independent B`
have "span B = UNIV" by auto
with `independent B` show "is_basis B" unfolding is_basis_def ..
next
assume "is_basis B"
hence "independent B" unfolding is_basis_def ..
moreover have "card B = CARD('n)"
proof -
have "B ⊆ UNIV" by simp
moreover
{ from `is_basis B` have "UNIV ⊆ span B" and "independent B"
unfolding is_basis_def
by simp+ }
ultimately have "card B = dim (UNIV::((real^'n) set))"
using basis_card_eq_dim [of B UNIV]
by simp
then show "card B = CARD('n)" by (simp add: dim_UNIV)
qed
ultimately show "independent B ∧ card B = CARD('n)" ..
qed
lemma basis_finite:
fixes B :: "(real^('n::finite)) set"
assumes "is_basis B"
shows "finite B"
proof -
from independent_is_basis [of B] and `is_basis B` have "card B = CARD('n)"
by simp
with card_finite [of B, where 'n = 'n] show "finite B" by simp
qed
text{*Here ends the facts obtained from AFP: \url{http://afp.sourceforge.net/browser_info/current/HOL/Tarskis_Geometry/Linear_Algebra2.html}*}
subsection{*Basic properties involving span, linearity and dimensions*}
text{*This theorem is the reciprocal theorem of @{thm "indep_card_eq_dim_span"}*}
lemma card_eq_dim_span_indep:
fixes A :: "('n::euclidean_space) set"
assumes "dim (span A) = card A" and "finite A"
shows "independent A"
by (metis assms card_le_dim_spanning dim_subset equalityE span_inc)
lemma dim_zero_eq:
fixes A::"'a::euclidean_space set"
assumes dim_A: "dim A = 0"
shows "A = {} ∨ A = {0}"
proof -
obtain B where ind_B: "independent B" and A_in_span_B: "A ⊆ span B" and card_B: "card B = 0" using basis_exists[of A] unfolding dim_A by blast
have finite_B: "finite B" using indep_card_eq_dim_span[OF ind_B] by simp
hence B_eq_empty: "B={}" using card_B unfolding card_eq_0_iff by simp
have "A ⊆ {0}" using A_in_span_B unfolding B_eq_empty span_empty .
thus ?thesis by blast
qed
lemma dim_zero_eq':
fixes A::"'a::euclidean_space set"
assumes A: "A = {} ∨ A = {0}"
shows "dim A = 0"
proof -
have "card ({}::'a set) = dim A"
proof (rule basis_card_eq_dim[THEN conjunct2, of "{}::'a set" A])
show "{} ⊆ A" by simp
show "A ⊆ span {}" using A by fastforce
show "independent {}" by (rule independent_empty)
qed
thus ?thesis by simp
qed
lemma dim_zero_subspace_eq:
fixes A::"'a::euclidean_space set"
assumes subs_A: "subspace A"
shows "(dim A = 0) = (A = {0})" using dim_zero_eq dim_zero_eq' subspace_0[OF subs_A] by auto
lemma span_0_imp_set_empty_or_0:
assumes "span A = {0}"
shows "A = {} ∨ A = {0}" by (metis assms span_inc subset_singletonD)
lemma linear_injective_ker_0:
assumes lf: "linear f"
shows "inj f = ({x. f x = 0} = {0})"
unfolding linear_injective_0[OF lf]
using linear_0[OF lf] by blast
lemma snd_if_conv:
shows "snd (if P then (A,B) else (C,D))=(if P then B else D)" by simp
subsection{*Basic properties about matrix multiplication*}
lemma row_matrix_matrix_mult:
fixes A::"'a::{comm_ring_1}^'n^'m"
shows "(P $ i) v* A = (P ** A) $ i"
unfolding vec_eq_iff
unfolding vector_matrix_mult_def unfolding matrix_matrix_mult_def
by (auto intro!: setsum_cong)
corollary row_matrix_matrix_mult':
fixes A::"'a::{comm_ring_1}^'n^'m"
shows "(row i P) v* A = row i (P ** A)"
using row_matrix_matrix_mult unfolding row_def vec_nth_inverse .
lemma column_matrix_matrix_mult:
shows "column i (P**A) = P *v (column i A)"
unfolding column_def matrix_vector_mult_def matrix_matrix_mult_def by fastforce
lemma matrix_matrix_mult_inner_mult:
shows "(A ** B) $ i $ j = row i A • column j B"
unfolding inner_vec_def matrix_matrix_mult_def row_def column_def by auto
lemma matrix_vmult_column_sum:
fixes A::"real^'n^'m"
shows "∃f. A *v x = setsum (λy. f y *⇩R y) (columns A)"
proof (rule exI[of _ "λy. setsum (λi. x $ i) {i. y = column i A}"])
let ?f="λy. setsum (λi. x $ i) {i. y = column i A}"
let ?g="(λy. {i. y=column i (A)})"
have inj: "inj_on ?g (columns (A))" unfolding inj_on_def unfolding columns_def by auto
have union_univ: "\<Union> (?g`(columns (A))) = UNIV" unfolding columns_def by auto
have "A *v x = (∑i∈UNIV. x $ i *s column i A)" unfolding matrix_mult_vsum ..
also have "... = setsum (λi. x $ i *s column i A) (\<Union>(?g`(columns A)))" unfolding union_univ ..
also have "... = setsum (setsum ((λi. x $ i *s column i A))) (?g`(columns A))" by (rule setsum_Union_disjoint, auto)
also have "... = setsum ((setsum ((λi. x $ i *s column i A))) o ?g) (columns A)" by (rule setsum_reindex, simp add: inj)
also have "... = setsum (λy. ?f y *⇩R y) (columns A)"
proof (rule setsum_cong2, unfold o_def)
fix xa
have "setsum (λi. x $ i *s column i A) {i. xa = column i A} = setsum (λi. x $ i *s xa) {i. xa = column i A}" by simp
also have "... = setsum (λi. x $ i *⇩R xa) {i. xa = column i A}" unfolding scalar_mult_eq_scaleR ..
also have "... = setsum (λi. x $ i) {i. xa = column i A} *⇩R xa" using scaleR_setsum_left[of "(λi. x $ i)" "{i. xa = column i A}" xa] ..
finally show "(∑i | xa = column i A. x $ i *s column i A) = (∑i | xa = column i A. x $ i) *⇩R xa" .
qed
finally show "A *v x = (∑y∈columns A. (∑i | y = column i A. x $ i) *⇩R y)" .
qed
subsection{*Properties about invertibility*}
lemma matrix_inv:
assumes "invertible M"
shows matrix_inv_left: "matrix_inv M ** M = mat 1"
and matrix_inv_right: "M ** matrix_inv M = mat 1"
using `invertible M` and someI_ex [of "λ N. M ** N = mat 1 ∧ N ** M = mat 1"]
unfolding invertible_def and matrix_inv_def
by simp_all
lemma invertible_mult:
assumes inv_A: "invertible A"
and inv_B: "invertible B"
shows "invertible (A**B)"
proof -
obtain A' where AA': "A ** A' = mat 1" and A'A: "A' ** A = mat 1" using inv_A unfolding invertible_def by blast
obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1" using inv_B unfolding invertible_def by blast
show ?thesis
proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI)
have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))" using matrix_mul_assoc[of A B "(B' ** A')", symmetric] .
also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] ..
also have "... = A ** (mat 1 ** A')" unfolding BB' ..
also have "... = A ** A'" unfolding matrix_mul_lid ..
also have "... = mat 1" unfolding AA' ..
finally show "A ** B ** (B' ** A') = mat (1::'a)" .
have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] .
also have "... = B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] ..
also have "... = B' ** (mat 1 ** B)" unfolding A'A ..
also have "... = B' ** B" unfolding matrix_mul_lid ..
also have "... = mat 1" unfolding B'B ..
finally show "B' ** A' ** (A ** B) = mat 1" .
qed
qed
text{*In the library, @{thm "matrix_inv_def"} allows the use of non squary matrices.
The following lemma can be also proved fixing @{term "A::'a::{semiring_1}^'n^'m"}*}
lemma matrix_inv_unique:
fixes A::"'a::{semiring_1}^'n^'n"
assumes AB: "A ** B = mat 1" and BA: "B ** A = mat 1"
shows "matrix_inv A = B"
proof (unfold matrix_inv_def, rule some_equality)
show "A ** B = mat (1::'a) ∧ B ** A = mat (1::'a)" using AB BA by simp
fix C assume "A ** C = mat (1::'a) ∧ C ** A = mat (1::'a)"
hence AC: "A ** C = mat (1::'a)" and CA: "C ** A = mat (1::'a)" by auto
have "B = B ** (mat 1)" unfolding matrix_mul_rid ..
also have "... = B ** (A**C)" unfolding AC ..
also have "... = B ** A ** C" unfolding matrix_mul_assoc ..
also have "... = C" unfolding BA matrix_mul_lid ..
finally show "C = B" ..
qed
lemma matrix_vector_mult_zero_eq:
assumes P: "invertible P"
shows "((P**A)*v x = 0) = (A *v x = 0)"
proof (rule iffI)
assume "P ** A *v x = 0"
hence "matrix_inv P *v (P ** A *v x) = matrix_inv P *v 0" by simp
hence "matrix_inv P *v (P ** A *v x) = 0" by (metis matrix_vector_zero)
hence "(matrix_inv P ** P ** A) *v x = 0" by (metis matrix_vector_mul_assoc)
thus "A *v x = 0" by (metis assms matrix_inv_left matrix_mul_lid)
next
assume "A *v x = 0"
thus "P ** A *v x = 0" by (metis matrix_vector_mul_assoc matrix_vector_zero)
qed
lemma inj_matrix_vector_mult:
fixes P::"real^'n^'m"
assumes P: "invertible P"
shows "inj (op *v P)"
unfolding linear_injective_0[OF matrix_vector_mul_linear]
using matrix_left_invertible_ker[of P] P unfolding invertible_def by blast
lemma independent_image_matrix_vector_mult:
fixes P::"real^'n^'m"
assumes ind_B: "independent B" and inv_P: "invertible P"
shows "independent ((op *v P)` B)"
proof (rule independent_injective_on_span_image)
show "independent B" using ind_B .
show "linear (op *v P)" using matrix_vector_mul_linear by force
show "inj_on (op *v P) (span B)" using inj_matrix_vector_mult[OF inv_P] unfolding inj_on_def by simp
qed
lemma independent_preimage_matrix_vector_mult:
fixes P::"real^'n^'n"
assumes ind_B: "independent ((op *v P)` B)" and inv_P: "invertible P"
shows "independent B"
proof -
have "independent ((op *v (matrix_inv P))` ((op *v P)` B))"
proof (rule independent_image_matrix_vector_mult)
show "independent (op *v P ` B)" using ind_B .
show "invertible (matrix_inv P)" by (metis inv_P invertible_righ_inverse matrix_inv_left)
qed
moreover have "(op *v (matrix_inv P))` ((op *v P)` B) = B"
proof (auto)
fix x assume x: "x ∈ B" show "matrix_inv P *v (P *v x) ∈ B" by (metis (full_types) x inv_P matrix_inv_left matrix_vector_mul_assoc matrix_vector_mul_lid)
thus "x ∈ op *v (matrix_inv P) ` op *v P ` B"
unfolding image_def by (auto, metis inv_P matrix_inv_left matrix_vector_mul_assoc matrix_vector_mul_lid)
qed
ultimately show ?thesis by simp
qed
subsection{*Instantiations*}
text{*Functions between two real vector spaces form a real vector*}
instantiation "fun" :: (real_vector, real_vector) real_vector
begin
definition "plus_fun f g = (λi. f i + g i)"
definition "zero_fun = (λi. 0)"
definition "scaleR_fun a f = (λi. a *⇩R f i )"
instance proof
fix a::"'a => 'b" and b::"'a => 'b" and c::"'a => 'b"
show "a + b + c = a + (b + c)" unfolding fun_eq_iff unfolding plus_fun_def by auto
show "a + b = b + a" unfolding fun_eq_iff unfolding plus_fun_def by auto
show " (0::'a => 'b) + a = a" unfolding fun_eq_iff unfolding plus_fun_def zero_fun_def by auto
show "- a + a = (0::'a => 'b)" unfolding fun_eq_iff unfolding plus_fun_def zero_fun_def by auto
show "a - b = a + - b" unfolding fun_eq_iff unfolding plus_fun_def zero_fun_def by auto
next
fix a::real and x::"('a => 'b)" and y::"'a => 'b"
show "a *⇩R (x + y) = a *⇩R x + a *⇩R y"
unfolding fun_eq_iff plus_fun_def scaleR_fun_def scaleR_right.add by auto
next
fix a::real and b::real and x::"'a => 'b"
show "(a + b) *⇩R x = a *⇩R x + b *⇩R x"
unfolding fun_eq_iff unfolding plus_fun_def scaleR_fun_def unfolding scaleR_left.add by auto
show " a *⇩R b *⇩R x = (a * b) *⇩R x" unfolding fun_eq_iff unfolding scaleR_fun_def by auto
show "(1::real) *⇩R x = x" unfolding fun_eq_iff unfolding scaleR_fun_def by auto
qed
end
instantiation vec :: (type, finite) equal
begin
definition equal_vec :: "('a, 'b::finite) vec => ('a, 'b::finite) vec => bool"
where "equal_vec x y = (∀i. x$i = y$i)"
instance
proof (intro_classes)
fix x y::"('a, 'b::finite) vec"
show "equal_class.equal x y = (x = y)" unfolding equal_vec_def using vec_eq_iff by auto
qed
end
subsection{*Properties about lists*}
text{*The following definitions and theorems are developed in order to compute setprods. More theorems and properties can be demonstrated in a similar way to the ones
about @{term "listsum"}.*}
definition (in monoid_mult) listprod :: "'a list => 'a" where
"listprod xs = foldr times xs 1"
lemma (in monoid_mult) listprod_simps [simp]:
"listprod [] = 1"
"listprod (x # xs) = x * listprod xs"
by (simp_all add: listprod_def)
lemma (in monoid_mult) listprod_append [simp]:
"listprod (xs @ ys) = listprod xs * listprod ys"
by (induct xs) (simp_all add: mult.assoc)
lemma (in comm_monoid_mult) listprod_rev [simp]:
"listprod (rev xs) = listprod xs"
by (simp add: listprod_def foldr_fold fold_rev fun_eq_iff mult_ac)
lemma (in monoid_mult) listprod_distinct_conv_setprod_set:
"distinct xs ==> listprod (map f xs) = setprod f (set xs)"
by (induct xs) simp_all
lemma setprod_code [code]:
"setprod f (set xs) = listprod (map f (remdups xs))"
by (simp add: listprod_distinct_conv_setprod_set)
end