Theory Jordan_Normal_Form.Determinant
section ‹Determinants›
text ‹Most of the following definitions and proofs on determinants have been copied and adapted
from ~~/src/HOL/Multivariate-Analysis/Determinants.thy.
Exceptions are \emph{det-identical-rows}.
We further generalized some lemmas, e.g., that the determinant is 0 iff the kernel of a matrix
is non-empty is available for integral domains, not just for fields.›
theory Determinant
imports
Missing_Misc
Column_Operations
"HOL-Computational_Algebra.Polynomial_Factorial"
Polynomial_Interpolation.Ring_Hom
Polynomial_Interpolation.Missing_Unsorted
begin
definition det:: "'a mat ⇒ 'a :: comm_ring_1" where
"det A = (if dim_row A = dim_col A then (∑ p ∈ {p. p permutes {0 ..< dim_row A}}.
signof p * (∏ i = 0 ..< dim_row A. A $$ (i, p i))) else 0)"
lemma(in ring_hom) hom_signof[simp]: "hom (signof p) = signof p"
by (simp add: hom_uminus sign_def)
lemma(in comm_ring_hom) hom_det[simp]: "det (map_mat hom A) = hom (det A)"
unfolding det_def by (auto simp: hom_distribs)
lemma det_def': "A ∈ carrier_mat n n ⟹
det A = (∑ p ∈ {p. p permutes {0 ..< n}}.
signof p * (∏ i = 0 ..< n. A $$ (i, p i)))" unfolding det_def by auto
lemma det_smult[simp]: "det (a ⋅⇩m A) = a ^ dim_col A * det A"
proof -
have [simp]: "(∏i = 0..<dim_col A. a) = a ^ dim_col A" by(subst prod_constant;simp)
show ?thesis
unfolding det_def
unfolding index_smult_mat
by (auto intro: sum.cong simp: sum_distrib_left prod.distrib)
qed
lemma det_transpose: assumes A: "A ∈ carrier_mat n n"
shows "det (transpose_mat A) = det A"
proof -
let ?di = "λA i j. A $$ (i,j)"
let ?U = "{0 ..< n}"
have fU: "finite ?U" by simp
let ?inv = "Hilbert_Choice.inv"
{
fix p
assume p: "p ∈ {p. p permutes ?U}"
from p have pU: "p permutes ?U"
by blast
have sth: "signof (?inv p) = signof p"
by (rule signof_inv[OF _ pU], simp)
from permutes_inj[OF pU]
have pi: "inj_on p ?U"
by (blast intro: subset_inj_on)
let ?f = "λi. transpose_mat A $$ (i, ?inv p i)"
note pU_U = permutes_image[OF pU]
note [simp] = permutes_less[OF pU]
have "prod ?f ?U = prod ?f (p ` ?U)"
using pU_U by simp
also have "… = prod (?f ∘ p) ?U"
by (rule prod.reindex[OF pi])
also have "… = prod (λi. A $$ (i, p i)) ?U"
by (rule prod.cong, insert A, auto)
finally have "signof (?inv p) * prod ?f ?U =
signof p * prod (λi. A $$ (i, p i)) ?U"
unfolding sth by simp
}
then show ?thesis
unfolding det_def using A
by (simp, subst sum_permutations_inverse, intro sum.cong, auto)
qed
lemma det_col:
assumes A: "A ∈ carrier_mat n n"
shows "det A = (∑ p | p permutes {0 ..< n}. signof p * (∏j<n. A $$ (p j, j)))"
(is "_ = (sum (λp. _ * ?prod p) ?P)")
proof -
let ?i = "Hilbert_Choice.inv"
let ?N = "{0 ..< n}"
let ?f = "λp. signof p * ?prod p"
let ?prod' = "λp. ∏j<n. A $$ (j, ?i p j)"
let ?prod'' = "λp. ∏j<n. A $$ (j, p j)"
let ?f' = "λp. signof (?i p) * ?prod' p"
let ?f'' = "λp. signof p * ?prod'' p"
let ?P' = "{ ?i p | p. p permutes ?N }"
have [simp]: "{0..<n} = {..<n}" by auto
have "sum ?f ?P = sum ?f' ?P"
proof (rule sum.cong[OF refl],unfold mem_Collect_eq)
fix p assume p: "p permutes ?N"
have [simp]: "?prod p = ?prod' p"
using permutes_prod[OF p, of "λx y. A $$ (x,y)"] by auto
have [simp]: "signof p = signof (?i p)"
apply(rule signof_inv[symmetric]) using p by auto
show "?f p = ?f' p" by auto
qed
also have "... = sum ?f' ?P'"
by (rule sum.cong[OF image_inverse_permutations[symmetric]],auto)
also have "... = sum ?f'' ?P"
unfolding sum.reindex[OF inv_inj_on_permutes,unfolded image_Collect]
unfolding o_def
apply (rule sum.cong[OF refl])
using inv_inv_eq[OF permutes_bij] by force
finally show ?thesis unfolding det_def'[OF A] by auto
qed
lemma mat_det_left_def: assumes A: "A ∈ carrier_mat n n"
shows "det A = (∑p∈{p. p permutes {0..<dim_row A}}. signof p * (∏i = 0 ..< dim_row A. A $$ (p i, i)))"
proof -
have cong: "⋀ a b c. b = c ⟹ a * b = a * c" by simp
show ?thesis
unfolding det_transpose[OF A, symmetric]
unfolding det_def index_transpose_mat using A by simp
qed
lemma det_upper_triangular:
assumes ut: "upper_triangular A"
and m: "A ∈ carrier_mat n n"
shows "det A = prod_list (diag_mat A)"
proof -
note det_def = det_def'[OF m]
let ?U = "{0..<n}"
let ?PU = "{p. p permutes ?U}"
let ?pp = "λp. signof p * (∏ i = 0 ..< n. A $$ (i, p i))"
have fU: "finite ?U"
by simp
from finite_permutations[OF fU] have fPU: "finite ?PU" .
have id0: "{id} ⊆ ?PU"
by (auto simp add: permutes_id)
{
fix p
assume p: "p ∈ ?PU - {id}"
from p have pU: "p permutes ?U" and pid: "p ≠ id"
by blast+
from permutes_natset_ge[OF pU] pid obtain i where i: "p i < i" and "i < n"
by fastforce
from upper_triangularD[OF ut i] ‹i < n› m
have ex:"∃i ∈ ?U. A $$ (i,p i) = 0" by auto
have "(∏ i = 0 ..< n. A $$ (i, p i)) = 0"
by (rule prod_zero[OF fU ex])
hence "?pp p = 0" by simp
}
then have p0: "⋀ p. p ∈ ?PU - {id} ⟹ ?pp p = 0"
by blast
from m have dim: "dim_row A = n" by simp
have "det A = (∑ p ∈ ?PU. ?pp p)" unfolding det_def by auto
also have "… = ?pp id + (∑ p ∈ ?PU - {id}. ?pp p)"
by (rule sum.remove, insert id0 fPU m, auto simp: p0)
also have "(∑ p ∈ ?PU - {id}. ?pp p) = 0"
by (rule sum.neutral, insert fPU, auto simp: p0)
finally show ?thesis using m by (auto simp: prod_list_diag_prod)
qed
lemma det_single: assumes "A ∈ carrier_mat 1 1"
shows "det A = A $$ (0,0)"
by (subst det_upper_triangular[of _ 1], insert assms, auto simp: diag_mat_def)
lemma det_one[simp]: "det (1⇩m n) = 1"
proof -
have "det (1⇩m n) = prod_list (diag_mat (1⇩m n))"
by (rule det_upper_triangular[of _ n], auto)
also have "… = 1" by (induct n, auto)
finally show ?thesis .
qed
lemma det_zero[simp]: assumes "n > 0" shows "det (0⇩m n n) = 0"
proof -
have "det (0⇩m n n) = prod_list (diag_mat (0⇩m n n))"
by (rule det_upper_triangular[of _ n], auto)
also have "… = 0" using ‹n > 0› by (cases n, auto)
finally show ?thesis .
qed
lemma det_dim_zero[simp]: "A ∈ carrier_mat 0 0 ⟹ det A = 1"
unfolding det_def carrier_mat_def sign_def by auto
lemma det_lower_triangular:
assumes ld: "⋀i j. i < j ⟹ j < n ⟹ A $$ (i,j) = 0"
and m: "A ∈ carrier_mat n n"
shows "det A = prod_list (diag_mat A)"
proof -
have "det A = det (transpose_mat A)" using det_transpose[OF m] by simp
also have "… = prod_list (diag_mat (transpose_mat A))"
by (rule det_upper_triangular, insert m ld, auto)
finally show ?thesis using m by simp
qed
lemma det_permute_rows: assumes A: "A ∈ carrier_mat n n"
and p: "p permutes {0 ..< (n :: nat)}"
shows "det (mat n n (λ (i,j). A $$ (p i, j))) = signof p * det A"
proof -
let ?U = "{0 ..< (n :: nat)}"
have cong: "⋀ a b c. b = c ⟹ a * b = a * c" by auto
have "det (mat n n (λ (i,j). A $$ (p i, j))) =
(∑ q ∈ {q . q permutes ?U}. signof q * (∏ i ∈ ?U. A $$ (p i, q i)))"
unfolding det_def using A p by auto
also have "… = (∑ q ∈ {q . q permutes ?U}. signof (q ∘ p) * (∏ i ∈ ?U. A $$ (p i, (q ∘ p) i)))"
by (rule sum_permutations_compose_right[OF p])
finally have 1: "det (mat n n (λ (i,j). A $$ (p i, j)))
= (∑ q ∈ {q . q permutes ?U}. signof (q ∘ p) * (∏ i ∈ ?U. A $$ (p i, (q ∘ p) i)))" .
have 2: "signof p * det A =
(∑ q∈{q. q permutes ?U}. signof p * signof q * (∏i∈ ?U. A $$ (i, q i)))"
unfolding det_def'[OF A] sum_distrib_left by (simp add: ac_simps)
show ?thesis unfolding 1 2
proof (rule sum.cong, insert p A, auto)
fix q
assume q: "q permutes ?U"
let ?inv = "Hilbert_Choice.inv"
from permutes_inv[OF p] have ip: "?inv p permutes ?U" .
have "prod (λi. A $$ (p i, (q ∘ p) i)) ?U =
prod (λi. A $$ ((p ∘ ?inv p) i, (q ∘ (p ∘ ?inv p)) i)) ?U" unfolding o_def
by (rule trans[OF prod.permute[OF ip] prod.cong], insert A p q, auto)
also have "… = prod (λi. A$$(i,q i)) ?U"
by (simp only: o_def permutes_inverses[OF p])
finally have thp: "prod (λi. A $$ (p i, (q ∘ p) i)) ?U = prod (λi. A$$(i,q i)) ?U" .
show "signof (q ∘ p) * (∏i∈{0..<n}. A $$ (p i, q (p i))) =
signof p * signof q * (∏i∈{0..<n}. A $$ (i, q i))"
unfolding thp[symmetric] signof_compose[OF q p]
by (simp add: ac_simps)
qed
qed
lemma det_multrow_mat: assumes k: "k < n"
shows "det (multrow_mat n k a) = a"
proof (rule trans[OF det_lower_triangular[of n]], unfold prod_list_diag_prod)
let ?f = "λ i. multrow_mat n k a $$ (i, i)"
have "(∏i∈{0..<n}. ?f i) = ?f k * (∏i∈{0..<n} - {k}. ?f i)"
by (rule prod.remove, insert k, auto)
also have "(∏i∈{0..<n} - {k}. ?f i) = 1"
by (rule prod.neutral, auto)
finally show "(∏i∈{0..<dim_row (multrow_mat n k a)}. ?f i) = a" using k by simp
qed (insert k, auto)
lemma swap_rows_mat_eq_permute:
"k < n ⟹ l < n ⟹ swaprows_mat n k l = mat n n (λ(i, j). 1⇩m n $$ (transpose k l i, j))"
by (rule eq_matI) (auto simp add: transpose_def)
lemma det_swaprows_mat: assumes k: "k < n" and l: "l < n" and kl: "k ≠ l"
shows "det (swaprows_mat n k l) = - 1"
proof -
let ?n = "{0 ..< (n :: nat)}"
let ?p = "transpose k l"
have p: "?p permutes ?n"
by (rule permutes_swap_id, insert k l, auto)
show ?thesis
by (rule trans[OF trans[OF _ det_permute_rows[OF one_carrier_mat[of n] p]]],
subst swap_rows_mat_eq_permute[OF k l], auto simp: sign_swap_id kl)
qed
lemma det_addrow_mat:
assumes l: "k ≠ l"
shows "det (addrow_mat n a k l) = 1"
proof -
have "det (addrow_mat n a k l) = prod_list (diag_mat (addrow_mat n a k l))"
proof (cases "k < l")
case True
show ?thesis
by (rule det_upper_triangular[of _ n], insert True, auto intro!: upper_triangularI)
next
case False
show ?thesis
by (rule det_lower_triangular[of n], insert False, auto)
qed
also have "… = 1" unfolding prod_list_diag_prod
by (rule prod.neutral, insert l, auto)
finally show ?thesis .
qed
text ‹The following proof is new, as it does not use $2 \neq 0$ as in Multivariate-Analysis.›
lemma det_identical_rows:
assumes A: "A ∈ carrier_mat n n"
and ij: "i ≠ j"
and i: "i < n" and j: "j < n"
and r: "row A i = row A j"
shows "det A = 0"
proof-
let ?p = "transpose i j"
let ?n = "{0 ..< n}"
have sp: "signof ?p = - 1" "sign ?p = (- 1 :: int)" using ij
by (auto simp add: sign_swap_id)
let ?f = "λ p. signof p * (∏i∈?n. A $$ (p i, i))"
let ?all = "{p. p permutes ?n}"
let ?one = "{p. p permutes ?n ∧ sign p = (1 :: int)}"
let ?none = "{p. p permutes ?n ∧ sign p ≠ (1 :: int)}"
let ?pone = "(λ p. ?p o p) ` ?one"
have split: "?one ∪ ?none = ?all" by auto
have p: "?p permutes ?n" by (rule permutes_swap_id, insert i j, auto)
from permutes_inj[OF p] have injp: "inj ?p" by auto
{
fix q
assume q: "q permutes ?n"
have "(∏k∈?n. A $$ (?p (q k), k)) = (∏k∈?n. A $$ (q k, k))"
proof (rule prod.cong)
fix k
assume k: "k ∈ ?n"
from r have row: "row A i $ k = row A j $ k" by simp
hence "A $$ (i,k) = A $$ (j,k)" using k i j A by auto
thus "A $$ (?p (q k), k) = A $$ (q k, k)"
by (cases "q k = i", auto, cases "q k = j", auto)
qed (insert A q, auto)
} note * = this
have pp: "⋀ q. q permutes ?n ⟹ permutation q" unfolding
permutation_permutes by auto
have "det A = (∑p∈ ?one ∪ ?none. ?f p)"
using A unfolding mat_det_left_def[OF A] split by simp
also have "… = (∑p∈ ?one. ?f p) + (∑p∈ ?none. ?f p)"
by (rule sum.union_disjoint, insert A, auto simp: finite_permutations)
also have "?none = ?pone"
proof -
{
fix q
assume "q ∈ ?none"
hence q: "q permutes ?n" and sq: "sign q = (- 1 :: int)" unfolding sign_def by auto
from permutes_compose[OF q p] sign_compose[OF pp[OF p] pp[OF q], unfolded sp sq]
have "?p o q ∈ ?one" by auto
hence "?p o (?p o q) ∈ ?pone" by auto
also have "?p o (?p o q) = q"
by (auto simp: swap_id_eq)
finally have "q ∈ ?pone" .
}
moreover
{
fix pq
assume "pq ∈ ?pone"
then obtain q where q: "q ∈ ?one" and pq: "pq = ?p o q" by auto
from q have q: "q permutes ?n" and sq: "sign q = (1 :: int)" by auto
from sign_compose[OF pp[OF p] pp[OF q], unfolded sq sp]
have spq: "sign pq = (- 1 :: int)" unfolding pq by auto
from permutes_compose[OF q p] have pq: "pq permutes ?n" unfolding pq by auto
from pq spq have "pq ∈ ?none" by auto
}
ultimately
show ?thesis by blast
qed
also have "(∑p∈ ?pone. ?f p) = (∑p∈ ?one. ?f (?p o p))"
proof (rule trans[OF sum.reindex])
show "inj_on ((∘) ?p) ?one"
using fun.inj_map[OF injp] unfolding inj_on_def by auto
qed simp
also have "(∑p∈ ?one. ?f p) + (∑p∈ ?one. ?f (?p o p))
= (∑p∈ ?one. ?f p + ?f (?p o p))"
by (rule sum.distrib[symmetric])
also have "… = 0"
by (rule sum.neutral, insert A, auto simp:
sp sign_compose[OF pp[OF p] pp] ij finite_permutations *)
finally show ?thesis .
qed
lemma det_row_0: assumes k: "k < n"
and c: "c ∈ {0 ..< n} → carrier_vec n"
shows "det (mat⇩r n n (λi. if i = k then 0⇩v n else c i)) = 0"
proof -
{
fix p
assume p: "p permutes {0 ..< n}"
have "(∏i∈{0..<n}. mat⇩r n n (λi. if i = k then 0⇩v n else c i) $$ (i, p i)) = 0"
by (rule prod_zero[OF _ bexI[of _ k]],
insert k p c[unfolded carrier_vec_def], auto)
}
thus ?thesis unfolding det_def by simp
qed
lemma det_row_add:
assumes abc: "a k ∈ carrier_vec n" "b k ∈ carrier_vec n" "c ∈ {0..<n} → carrier_vec n"
and k: "k < n"
shows "det(mat⇩r n n (λ i. if i = k then a i + b i else c i)) =
det(mat⇩r n n (λ i. if i = k then a i else c i)) +
det(mat⇩r n n (λ i. if i = k then b i else c i))"
(is "?lhs = ?rhs")
proof -
let ?n = "{0..<n}"
let ?m = "λ a b p i. mat⇩r n n (λi. if i = k then a i else b i) $$ (i, p i)"
let ?c = "λ p i. mat⇩r n n c $$ (i, p i)"
let ?ab = "λ i. a i + b i"
note intros = add_carrier_vec[of _ n]
have "?rhs = (∑p∈{p. p permutes ?n}.
signof p * (∏i∈?n. ?m a c p i)) + (∑p∈{p. p permutes ?n}. signof p * (∏i∈?n. ?m b c p i))"
unfolding det_def by simp
also have "… = (∑p∈{p. p permutes ?n}. signof p * (∏i∈?n. ?m a c p i) + signof p * (∏i∈?n. ?m b c p i))"
by (rule sum.distrib[symmetric])
also have "… = (∑p∈{p. p permutes ?n}. signof p * (∏i∈?n. ?m ?ab c p i))"
proof (rule sum.cong, force)
fix p
assume "p ∈ {p. p permutes ?n}"
hence p: "p permutes ?n" by simp
show "signof p * (∏i∈?n. ?m a c p i) + signof p * (∏i∈?n. ?m b c p i) =
signof p * (∏i∈?n. ?m ?ab c p i)"
unfolding distrib_left[symmetric]
proof (rule arg_cong[of _ _ "λ a. signof p * a"])
from k have f: "finite ?n" and k': "k ∈ ?n" by auto
let ?nk = "?n - {k}"
note split = prod.remove[OF f k']
have id1: "(∏i∈?n. ?m a c p i) = ?m a c p k * (∏i∈?nk. ?m a c p i)"
by (rule split)
have id2: "(∏i∈?n. ?m b c p i) = ?m b c p k * (∏i∈?nk. ?m b c p i)"
by (rule split)
have id3: "(∏i∈?n. ?m ?ab c p i) = ?m ?ab c p k * (∏i∈?nk. ?m ?ab c p i)"
by (rule split)
have id: "⋀ a. (∏i∈?nk. ?m a c p i) = (∏i∈?nk. ?c p i)"
by (rule prod.cong, insert abc k p, auto intro!: intros)
have ab: "?ab k ∈ carrier_vec n" using abc by (auto intro: intros)
{
fix f
assume "f k ∈ (carrier_vec n :: 'a vec set)"
hence "mat⇩r n n (λi. if i = k then f i else c i) $$ (k, p k) = f k $ p k"
by (insert p k abc, auto)
} note first = this
note id' = id1 id2 id3
have dist: "(a k + b k) $ p k = a k $ p k + b k $ p k"
by (rule index_add_vec(1), insert p k abc, force)
show "(∏i∈?n. ?m a c p i) + (∏i∈?n. ?m b c p i) = (∏i∈?n. ?m ?ab c p i)"
unfolding id' id first[of a, OF abc(1)] first[of b, OF abc(2)] first[of ?ab, OF ab] dist
by (rule distrib_right[symmetric])
qed
qed
also have "… = ?lhs" unfolding det_def by simp
finally show ?thesis by simp
qed
lemma det_linear_row_finsum:
assumes fS: "finite S" and c: "c ∈ {0..<n} → carrier_vec n" and k: "k < n"
and a: "a k ∈ S → carrier_vec n"
shows "det (mat⇩r n n (λ i. if i = k then finsum_vec TYPE('a :: comm_ring_1) n (a i) S else c i)) =
sum (λj. det (mat⇩r n n (λ i. if i = k then a i j else c i))) S"
proof -
let ?sum = "finsum_vec TYPE('a) n"
show ?thesis using a
proof (induct rule: finite_induct[OF fS])
case 1
show ?case
by (simp, unfold finsum_vec_empty, rule det_row_0[OF k c])
next
case (2 x F)
from 2(4) have ak: "a k ∈ F → carrier_vec n" and akx: "a k x ∈ carrier_vec n" by auto
{
fix i
note if_cong[OF refl finsum_vec_insert[OF 2(1-2)],
of _ "a i" n "c i" "c i"]
} note * = this
show ?case
proof (subst *)
show "det (mat⇩r n n (λi. if i = k then a i x + ?sum (a i) F else c i)) =
(∑j∈insert x F. det (mat⇩r n n (λi. if i = k then a i j else c i)))"
proof (subst det_row_add)
show "det (mat⇩r n n (λi. if i = k then a i x else c i)) +
det (mat⇩r n n (λi. if i = k then ?sum (a i) F else c i)) =
(∑j∈insert x F. det (mat⇩r n n (λi. if i = k then a i j else c i)))"
unfolding 2(3)[OF ak] sum.insert[OF 2(1-2)] by simp
qed (insert c k ak akx 2(1),
auto intro!: finsum_vec_closed)
qed (insert akx ak, force+)
qed
qed
lemma det_linear_rows_finsum_lemma:
assumes fS: "finite S"
and fT: "finite T" and c: "c ∈ {0..<n} → carrier_vec n"
and T: "T ⊆ {0 ..< n}"
and a: "a ∈ T → S → carrier_vec n"
shows "det (mat⇩r n n (λ i. if i ∈ T then finsum_vec TYPE('a :: comm_ring_1) n (a i) S else c i)) =
sum (λf. det(mat⇩r n n (λ i. if i ∈ T then a i (f i) else c i)))
{f. (∀i ∈ T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)}"
proof -
let ?sum = "finsum_vec TYPE('a) n"
show ?thesis using fT c a T
proof (induct T arbitrary: a c set: finite)
case empty
let ?f = "(λ i. i) :: nat ⇒ nat"
have [simp]: "{f. ∀i. f i = i} = {?f}" by auto
show ?case by simp
next
case (insert z T a c)
hence z: "z < n" and azS: "a z ∈ S → carrier_vec n" by auto
let ?F = "λT. {f. (∀i ∈ T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)}"
let ?h = "λ(y,g) i. if i = z then y else g i"
let ?k = "λh. (h(z),(λi. if i = z then i else h i))"
let ?s = "λ k a c f. det(mat⇩r n n (λ i. if i ∈ T then a i (f i) else c i))"
let ?c = "λj i. if i = z then a i j else c i"
have thif: "⋀a b c d. (if a ∨ b then c else d) = (if a then c else if b then c else d)"
by simp
have thif2: "⋀a b c d e. (if a then b else if c then d else e) =
(if c then (if a then b else d) else (if a then b else e))"
by simp
from ‹z ∉ T› have nz: "⋀i. i ∈ T ⟹ i = z ⟷ False"
by auto
from insert have c: "⋀ i. i < n ⟹ c i ∈ carrier_vec n" by auto
have fin: "finite {f. (∀i∈T. f i ∈ S) ∧ (∀i. i ∉ T ⟶ f i = i)}"
by (rule finite_bounded_functions[OF fS insert(1)])
have "det (mat⇩r n n (λ i. if i ∈ insert z T then ?sum (a i) S else c i)) =
det (mat⇩r n n (λ i. if i = z then ?sum (a i) S else if i ∈ T then ?sum (a i) S else c i))"
unfolding insert_iff thif ..
also have "… = (∑j∈S. det (mat⇩r n n (λ i. if i ∈ T then ?sum (a i) S else if i = z then a i j else c i)))"
apply (subst det_linear_row_finsum[OF fS _ z])
prefer 3
apply (subst thif2)
using nz
apply (simp cong del: if_weak_cong cong add: if_cong)
apply (insert azS c fS insert(5), (force intro!: finsum_vec_closed)+)
done
also have "… = (sum (λ (j, f). det (mat⇩r n n (λ i. if i ∈ T then a i (f i)
else if i = z then a i j
else c i))) (S × ?F T))"
unfolding sum.cartesian_product[symmetric]
by (rule sum.cong[OF refl], subst insert.hyps(3),
insert azS c fin z insert(5-6), auto)
finally have tha:
"det (mat⇩r n n (λ i. if i ∈ insert z T then ?sum (a i) S else c i)) =
(sum (λ (j, f). det (mat⇩r n n (λ i. if i ∈ T then a i (f i)
else if i = z then a i j
else c i))) (S × ?F T))" .
show ?case unfolding tha
by (rule sum.reindex_bij_witness[where i="?k" and j="?h"], insert ‹z ∉ T›
azS c fS insert(5-6) z fin,
auto intro!: arg_cong[of _ _ det])
qed
qed
lemma det_linear_rows_sum:
assumes fS: "finite S"
and a: "a ∈ {0..<n} → S → carrier_vec n"
shows "det (mat⇩r n n (λ i. finsum_vec TYPE('a :: comm_ring_1) n (a i) S)) =
sum (λf. det (mat⇩r n n (λ i. a i (f i))))
{f. (∀i∈{0..<n}. f i ∈ S) ∧ (∀i. i ∉ {0..<n} ⟶ f i = i)}"
proof -
let ?T = "{0..<n}"
have fT: "finite ?T" by auto
have th0: "⋀x y. mat⇩r n n (λ i. if i ∈ ?T then x i else y i) = mat⇩r n n (λ i. x i)"
by (rule eq_rowI, auto)
have c: "(λ _. 0⇩v n) ∈ ?T → carrier_vec n" by auto
show ?thesis
by (rule det_linear_rows_finsum_lemma[OF fS fT c subset_refl a, unfolded th0])
qed
lemma det_rows_mul:
assumes a: "a ∈ {0..<n} → carrier_vec n"
shows "det(mat⇩r n n (λ i. c i ⋅⇩v a i)) =
prod c {0..<n} * det(mat⇩r n n (λ i. a i))"
proof -
have A: "mat⇩r n n (λ i. c i ⋅⇩v a i) ∈ carrier_mat n n"
and A': "mat⇩r n n (λ i. a i) ∈ carrier_mat n n" using a unfolding carrier_mat_def by auto
show ?thesis unfolding det_def'[OF A] det_def'[OF A']
proof (rule trans[OF sum.cong sum_distrib_left[symmetric]])
fix p
assume p: "p ∈ {p. p permutes {0..<n}}"
have id: "(∏ia∈{0..<n}. mat⇩r n n (λi. c i ⋅⇩v a i) $$ (ia, p ia))
= prod c {0..<n} * (∏ia∈{0..<n}. mat⇩r n n a $$ (ia, p ia))"
unfolding prod.distrib[symmetric]
by (rule prod.cong, insert p a, force+)
show "signof p * (∏ia∈{0..<n}. mat⇩r n n (λi. c i ⋅⇩v a i) $$ (ia, p ia)) =
prod c {0..<n} * (signof p * (∏ia∈{0..<n}. mat⇩r n n a $$ (ia, p ia)))"
unfolding id by auto
qed simp
qed
lemma mat_mul_finsum_alt:
assumes A: "A ∈ carrier_mat nr n" and B: "B ∈ carrier_mat n nc"
shows "A * B = mat⇩r nr nc (λ i. finsum_vec TYPE('a :: semiring_0) nc (λk. A $$ (i,k) ⋅⇩v row B k) {0 ..< n})"
by (rule eq_matI, insert A B, auto, subst index_finsum_vec, auto simp: scalar_prod_def intro: sum.cong)
lemma det_mult:
assumes A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n"
shows "det (A * B) = det A * det (B :: 'a :: comm_ring_1 mat)"
proof -
let ?U = "{0 ..< n}"
let ?F = "{f. (∀i∈ ?U. f i ∈ ?U) ∧ (∀i. i ∉ ?U ⟶ f i = i)}"
let ?PU = "{p. p permutes ?U}"
have fU: "finite ?U"
by blast
have fF: "finite ?F"
by (rule finite_bounded_functions, auto)
{
fix p
assume p: "p permutes ?U"
have "p ∈ ?F" unfolding mem_Collect_eq permutes_in_image[OF p]
using p[unfolded permutes_def] by simp
}
then have PUF: "?PU ⊆ ?F" by blast
{
fix f
assume fPU: "f ∈ ?F - ?PU"
have fUU: "f ` ?U ⊆ ?U"
using fPU by auto
from fPU have f: "∀i ∈ ?U. f i ∈ ?U" "∀i. i ∉ ?U ⟶ f i = i" "¬(∀y. ∃!x. f x = y)"
unfolding permutes_def by auto
let ?A = "mat⇩r n n (λ i. A $$ (i, f i) ⋅⇩v row B (f i))"
let ?B = "mat⇩r n n (λ i. row B (f i))"
have B': "?B ∈ carrier_mat n n"
by (intro mat_row_carrierI)
{
assume fi: "inj_on f ?U"
from inj_on_nat_permutes[OF fi] f
have "f permutes ?U" by auto
with fPU have False by simp
}
hence fni: "¬ inj_on f ?U" by auto
then obtain i j where ij: "f i = f j" "i ≠ j" "i < n" "j < n"
unfolding inj_on_def by auto
from ij
have rth: "row ?B i = row ?B j" by auto
have "det ?A = 0"
by (subst det_rows_mul, unfold det_identical_rows[OF B' ij(2-4) rth], insert f A B, auto)
}
then have zth: "⋀ f. f ∈ ?F - ?PU ⟹ det (mat⇩r n n (λ i. A $$ (i, f i) ⋅⇩v row B (f i))) = 0"
by simp
{
fix p
assume pU: "p ∈ ?PU"
from pU have p: "p permutes ?U"
by blast
let ?s = "λp. (signof p) :: 'a"
let ?f = "λq. ?s p * (∏ i∈ ?U. A $$ (i,p i)) * (?s q * (∏i∈ ?U. B $$ (i, q i)))"
have "(sum (λq. ?s q *
(∏i∈ ?U. mat⇩r n n (λ i. A $$ (i, p i) ⋅⇩v row B (p i)) $$ (i, q i))) ?PU) =
(sum (λq. ?s p * (∏ i∈ ?U. A $$ (i,p i)) * (?s q * (∏ i∈ ?U. B $$ (i, q i)))) ?PU)"
unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f]
proof (rule sum.cong[OF refl])
fix q
assume "q ∈ {q. q permutes ?U}"
hence q: "q permutes ?U" by simp
from p q have pp: "permutation p" and pq: "permutation q"
unfolding permutation_permutes by auto
note sign = signof_compose[OF q permutes_inv[OF p], unfolded signof_inv[OF fU p]]
let ?inv = "Hilbert_Choice.inv"
have th001: "prod (λi. B$$ (i, q (?inv p i))) ?U = prod ((λi. B$$ (i, q (?inv p i))) ∘ p) ?U"
by (rule prod.permute[OF p])
have thp: "prod (λi. mat⇩r n n (λ i. A$$(i,p i) ⋅⇩v row B (p i)) $$ (i, q i)) ?U =
prod (λi. A$$(i,p i)) ?U * prod (λi. B$$ (i, q (?inv p i))) ?U"
unfolding th001 o_def permutes_inverses[OF p]
by (subst prod.distrib[symmetric], insert A p q B, auto intro: prod.cong)
define AA where "AA = (∏i∈?U. A $$ (i, p i))"
define BB where "BB = (∏ia∈{0..<n}. B $$ (ia, q (?inv p ia)))"
have "?s q * (∏ia∈{0..<n}. mat⇩r n n (λi. A $$ (i, p i) ⋅⇩v row B (p i)) $$ (ia, q ia)) =
?s p * (∏i∈{0..<n}. A $$ (i, p i)) * (?s (q ∘ ?inv p) * (∏ia∈{0..<n}. B $$ (ia, q (?inv p ia))))"
unfolding sign thp
unfolding AA_def[symmetric] BB_def[symmetric]
by (simp add: ac_simps flip: of_int_mult)
thus "?s q * (∏i = 0..<n. mat⇩r n n (λi. A $$ (i, p i) ⋅⇩v row B (p i)) $$ (i, q i)) =
?s p * (∏i = 0..<n. A $$ (i, p i)) *
(?s (q ∘ ?inv p) * (∏i = 0..<n. B $$ (i, (q ∘ ?inv p) i)))" by simp
qed
} note * = this
have th2: "sum (λf. det (mat⇩r n n (λ i. A$$(i,f i) ⋅⇩v row B (f i)))) ?PU = det A * det B"
unfolding det_def'[OF A] det_def'[OF B] det_def'[OF mat_row_carrierI]
unfolding sum_product dim_row_mat
by (rule sum.cong, insert A, force, subst *, insert A B, auto)
let ?f = "λ f. det (mat⇩r n n (λ i. A $$ (i, f i) ⋅⇩v row B (f i)))"
have "det (A * B) = sum ?f ?F"
unfolding mat_mul_finsum_alt[OF A B]
by (rule det_linear_rows_sum[OF fU], insert A B, auto)
also have "… = sum ?f ((?F - ?PU) ∪ (?F ∩ ?PU))"
by (rule arg_cong[where f = "sum ?f"], auto)
also have "… = sum ?f (?F - ?PU) + sum ?f (?F ∩ ?PU)"
by (rule sum.union_disjoint, insert A B finite_bounded_functions[OF fU fU], auto)
also have "sum ?f (?F - ?PU) = 0"
by (rule sum.neutral, insert zth, auto)
also have "?F ∩ ?PU = ?PU" unfolding permutes_def by fastforce
also have "sum ?f ?PU = det A * det B"
unfolding th2 ..
finally show ?thesis by simp
qed
lemma unit_imp_det_non_zero: assumes "A ∈ Units (ring_mat TYPE('a :: comm_ring_1) n b)"
shows "det A ≠ 0"
proof -
from assms[unfolded Units_def ring_mat_def]
obtain B where A: "A ∈ carrier_mat n n" and B: "B ∈ carrier_mat n n" and BA: "B * A = 1⇩m n" by auto
from arg_cong[OF BA, of det, unfolded det_mult[OF B A] det_one]
show ?thesis by auto
qed
text ‹The following proof is based on the Gauss-Jordan algorithm.›
lemma det_non_zero_imp_unit: assumes A: "A ∈ carrier_mat n n"
and dA: "det A ≠ (0 :: 'a :: field)"
shows "A ∈ Units (ring_mat TYPE('a) n b)"
proof (rule ccontr)
let ?g = "gauss_jordan A (0⇩m n 0)"
let ?B = "fst ?g"
obtain B C where B: "?g = (B,C)" by (cases ?g)
assume "¬ ?thesis"
from this[unfolded gauss_jordan_check_invertable[OF A zero_carrier_mat[of n 0]] B]
have "B ≠ 1⇩m n" by auto
with row_echelon_form_imp_1_or_0_row[OF gauss_jordan_carrier(1)[OF A _ B] gauss_jordan_row_echelon[OF A B], of 0]
have n: "0 < n" and row: "row B (n - 1) = 0⇩v n" by auto
let ?n = "n - 1"
from n have n1: "?n < n" by auto
from gauss_jordan_transform[OF A _ B, of 0 b] obtain P
where P: "P∈Units (ring_mat TYPE('a) n b)" and PA: "B = P * A" by auto
from unit_imp_det_non_zero[OF P] have dP: "det P ≠ 0" by auto
from P have P: "P ∈ carrier_mat n n" unfolding Units_def ring_mat_def by auto
from det_mult[OF P A] dP dA have "det B ≠ 0" unfolding PA by simp
also have "det B = 0"
proof -
from gauss_jordan_carrier[OF A _ B, of 0] have B: "B ∈ carrier_mat n n" by auto
{
fix j
assume j: "j < n"
from index_row(1)[symmetric, of ?n B j, unfolded row] B
have "B $$ (?n, j) = 0" using B n j by auto
}
hence "B = mat⇩r n n (λi. if i = ?n then 0⇩v n else row B i)"
by (intro eq_matI, insert B, auto)
also have "det … = 0"
by (rule det_row_0[OF n1], insert B, auto)
finally show "det B = 0" .
qed
finally show False by simp
qed
lemma mat_mult_left_right_inverse: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
and B: "B ∈ carrier_mat n n" and AB: "A * B = 1⇩m n"
shows "B * A = 1⇩m n"
proof -
let ?R = "ring_mat TYPE('a) n undefined"
from det_mult[OF A B, unfolded AB] have "det A ≠ 0" "det B ≠ 0" by auto
from det_non_zero_imp_unit[OF A this(1)] det_non_zero_imp_unit[OF B this(2)]
have U: "A ∈ Units ?R" "B ∈ Units ?R" .
interpret ring ?R by (rule ring_mat)
from Units_inv_comm[unfolded ring_mat_simps, OF AB U] show ?thesis .
qed
lemma det_zero_imp_zero_row: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
and det: "det A = 0"
shows "∃ P. P ∈ Units (ring_mat TYPE('a) n b) ∧ row (P * A) (n - 1) = 0⇩v n ∧ 0 < n
∧ row_echelon_form (P * A)"
proof -
let ?R = "ring_mat TYPE('a) n b"
let ?U = "Units ?R"
interpret m: ring ?R by (rule ring_mat)
let ?g = "gauss_jordan A A"
obtain A' B' where g: "?g = (A', B')" by (cases ?g)
from det unit_imp_det_non_zero[of A n b] have AU: "A ∉ ?U" by auto
with gauss_jordan_inverse_one_direction(1)[OF A A, of _ b]
have A'1: "A' ≠ 1⇩m n" using g by auto
from gauss_jordan_carrier(1)[OF A A g] have A': "A' ∈ carrier_mat n n" by auto
from gauss_jordan_row_echelon[OF A g] have re: "row_echelon_form A'" .
from row_echelon_form_imp_1_or_0_row[OF A' this] A'1
have n: "0 < n" and row: "row A' (n - 1) = 0⇩v n" by auto
from gauss_jordan_transform[OF A A g, of b] obtain P
where P: "P ∈ ?U" and A': "A' = P * A" by auto
thus ?thesis using n row re by auto
qed
lemma det_0_iff_vec_prod_zero_field: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
shows "det A = 0 ⟷ (∃ v. v ∈ carrier_vec n ∧ v ≠ 0⇩v n ∧ A *⇩v v = 0⇩v n)" (is "?l = (∃ v. ?P v)")
proof -
let ?R = "ring_mat TYPE('a) n ()"
let ?U = "Units ?R"
interpret m: ring ?R by (rule ring_mat)
show ?thesis
proof (cases "det A = 0")
case False
from det_non_zero_imp_unit[OF A this, of "()"]
have "A ∈ ?U" .
then obtain B where unit: "B * A = 1⇩m n" and B: "B ∈ carrier_mat n n"
unfolding Units_def ring_mat_def by auto
{
fix v
assume "?P v"
hence v: "v ∈ carrier_vec n" "v ≠ 0⇩v n" "A *⇩v v = 0⇩v n" by auto
have "v = (B * A) *⇩v v" using v B unfolding unit by auto
also have "… = B *⇩v (A *⇩v v)" using B A v by simp
also have "… = B *⇩v 0⇩v n" unfolding v ..
also have "… = 0⇩v n" using B by auto
finally have False using v by simp
}
with False show ?thesis by blast
next
case True
let ?n = "n - 1"
from det_zero_imp_zero_row[OF A True, of "()"]
obtain P where PU: "P ∈ ?U" and row: "row (P * A) ?n = 0⇩v n" and n: "0 < n" "?n < n"
and re: "row_echelon_form (P * A)" by auto
define PA where "PA = P * A"
note row = row[folded PA_def]
note re = re[folded PA_def]
from PU obtain Q where P: "P ∈ carrier_mat n n" and Q: "Q ∈ carrier_mat n n"
and unit: "Q * P = 1⇩m n" "P * Q = 1⇩m n" unfolding Units_def ring_mat_def by auto
from P A have PA: "PA ∈ carrier_mat n n" and dimPA: "dim_row PA = n" unfolding PA_def by auto
from re[unfolded row_echelon_form_def] obtain p where p: "pivot_fun PA p n" using PA by auto
note piv = pivot_positions[OF PA p]
note pivot = pivot_funD[OF dimPA p n(2)]
{
assume "p ?n < n"
with pivot(4)[OF this] n arg_cong[OF row, of "λ v. v $ p ?n"] have False using PA by auto
}
with pivot(1) have pn: "p ?n = n" by fastforce
with piv(1) have "set (pivot_positions PA) ⊆ {(i, p i) |i. i < n ∧ p i ≠ n} - {(?n,p ?n)}" by auto
also have "… ⊆ {(i, p i) | i. i < ?n}" using n by force
finally have "card (set (pivot_positions PA)) ≤ card {(i, p i) | i. i < ?n}"
by (intro card_mono, auto)
also have "{(i, p i) | i. i < ?n} = (λ i. (i, p i)) ` {0 ..< ?n}" by auto
also have "card … = card {0 ..< ?n}" by (rule card_image, auto simp: inj_on_def)
also have "… < n" using n by simp
finally have "card (set (pivot_positions PA)) < n" .
hence "card (snd ` (set (pivot_positions PA))) < n"
using card_image_le[OF finite_set, of snd "pivot_positions PA"] by auto
hence neq: "snd ` (set (pivot_positions PA)) ≠ {0 ..< n}" by auto
from find_base_vector[OF re PA neq] obtain v where v: "v ∈ carrier_vec n"
and v0: "v ≠ 0⇩v n" and pav: "PA *⇩v v = 0⇩v n" by auto
have "A *⇩v v = Q * P *⇩v (A *⇩v v)" unfolding unit using A v by auto
also have "… = Q *⇩v (PA *⇩v v)" unfolding PA_def using Q P A v by auto
also have "PA *⇩v v = 0⇩v n" unfolding pav ..
also have "Q *⇩v 0⇩v n = 0⇩v n" using Q by auto
finally have Av: "A *⇩v v = 0⇩v n" by auto
show ?thesis unfolding True using Av v0 v by auto
qed
qed
text ‹In order to get the result for integral domains, we embed the domain in its
fraction field, and then apply the result for fields.›
lemma det_0_iff_vec_prod_zero: assumes A: "(A :: 'a :: idom mat) ∈ carrier_mat n n"
shows "det A = 0 ⟷ (∃ v. v ∈ carrier_vec n ∧ v ≠ 0⇩v n ∧ A *⇩v v = 0⇩v n)"
proof -
let ?h = "to_fract :: 'a ⇒ 'a fract"
let ?A = "map_mat ?h A"
have A': "?A ∈ carrier_mat n n" using A by auto
interpret inj_comm_ring_hom ?h by (unfold_locales, auto)
have "(det A = 0) = (?h (det A) = ?h 0)" by auto
also have "… = (det ?A = 0)" unfolding hom_zero hom_det ..
also have "… = ((∃ v. v ∈ carrier_vec n ∧ v ≠ 0⇩v n ∧ ?A *⇩v v = 0⇩v n))"
unfolding det_0_iff_vec_prod_zero_field[OF A'] ..
also have "… = ((∃ v. v ∈ carrier_vec n ∧ v ≠ 0⇩v n ∧ A *⇩v v = 0⇩v n))" (is "?l = ?r")
proof
assume ?r
then obtain v where v: "v ∈ carrier_vec n" "v ≠ 0⇩v n" "A *⇩v v = 0⇩v n" by auto
show ?l
by (rule exI[of _ "map_vec ?h v"], insert v, auto simp: mult_mat_vec_hom[symmetric, OF A v(1)])
next
assume ?l
then obtain v where v: "v ∈ carrier_vec n" and v0: "v ≠ 0⇩v n" and Av: "?A *⇩v v = 0⇩v n" by auto
have "∀ i. ∃ a b. v $ i = Fraction_Field.Fract a b ∧ b ≠ 0" using Fract_cases[of "v $ i" for i] by metis
from choice[OF this] obtain a where "∀ i. ∃ b. v $ i = Fraction_Field.Fract (a i) b ∧ b ≠ 0" by metis
from choice[OF this] obtain b where vi: "⋀ i. v $ i = Fraction_Field.Fract (a i) (b i)" and bi: "⋀ i. b i ≠ 0" by auto
define m where "m = prod_list (map b [0..<n])"
let ?m = "?h m"
have m0: "m ≠ 0" unfolding m_def hom_0_iff prod_list_zero_iff using bi by auto
from v0[unfolded vec_eq_iff] v obtain i where i: "i < n" "v $ i ≠ 0" by auto
{
fix i
assume "i < n"
hence "b i ∈ set (map b [0 ..< n])" by auto
from split_list[OF this]
obtain ys zs where "map b [0..<n] = ys @ b i # zs" by auto
hence "b i dvd m" unfolding m_def by auto
then obtain c where "m = b i * c" ..
hence "?m * v $ i = ?h (a i * c)" unfolding vi using bi[of i]
by (simp add: eq_fract to_fract_def)
hence "∃ c. ?m * v $ i = ?h c" ..
}
hence "∀ i. ∃ c. i < n ⟶ ?m * v $ i = ?h c" by auto
from choice[OF this] obtain c where c: "⋀ i. i < n ⟹ ?m * v $ i = ?h (c i)" by auto
define w where "w = vec n c"
have w: "w ∈ carrier_vec n" unfolding w_def by simp
have mvw: "?m ⋅⇩v v = map_vec ?h w" unfolding w_def using c v
by (intro eq_vecI, auto)
with m0 i c[OF i(1)] have "w $ i ≠ 0" unfolding w_def by auto
with i w have w0: "w ≠ 0⇩v n" by auto
from arg_cong[OF Av, of "λ v. ?m ⋅⇩v v"]
have "?m ⋅⇩v (?A *⇩v v) = map_vec ?h (0⇩v n)" by auto
also have "?m ⋅⇩v (?A *⇩v v) = ?A *⇩v (?m ⋅⇩v v)" using A v by auto
also have "… = ?A *⇩v (map_vec ?h w)" unfolding mvw ..
also have "… = map_vec ?h (A *⇩v w)" unfolding mult_mat_vec_hom[OF A w] ..
finally have "A *⇩v w = 0⇩v n" by (rule vec_hom_inj)
with w w0 show ?r by blast
qed
finally show ?thesis .
qed
lemma det_0_negate: assumes A: "(A :: 'a :: field mat) ∈ carrier_mat n n"
shows "(det (- A) = 0) = (det A = 0)"
proof -
from A have mA: "- A ∈ carrier_mat n n" by auto
{
fix v :: "'a vec"
assume v: "v ∈ carrier_vec n"
hence Av: "A *⇩v v ∈ carrier_vec n" using A by auto
have id: "- A *⇩v v = - (A *⇩v v)" using v A by simp
have "(- A *⇩v v = 0⇩v n) = (A *⇩v v = 0⇩v n)" unfolding id
unfolding uminus_zero_vec_eq[OF Av] ..
}
thus ?thesis unfolding det_0_iff_vec_prod_zero[OF A] det_0_iff_vec_prod_zero[OF mA] by auto
qed
lemma det_multrow:
assumes k: "k < n" and A: "A ∈ carrier_mat n n"
shows "det (multrow k a A) = a * det A"
proof -
have "multrow k a A = multrow_mat n k a * A"
by (rule multrow_mat[OF A])
also have "det (multrow_mat n k a * A) = det (multrow_mat n k a) * det A"
by (rule det_mult[OF _ A], auto)
also have "det (multrow_mat n k a) = a"
by (rule det_multrow_mat[OF k])
finally show ?thesis .
qed
lemma det_multrow_div:
assumes k: "k < n" and A: "A ∈ carrier_mat n n" and a0: "a ≠ 0"
shows "det (multrow k a A :: 'a :: idom_divide mat) div a = det A"
proof -
have "det (multrow k a A) div a = a * det A div a" using k A
by (simp add: det_multrow)
also have "... = det A" using a0 by auto
finally show ?thesis.
qed
lemma det_addrow:
assumes l: "l < n" and k: "k ≠ l" and A: "A ∈ carrier_mat n n"
shows "det (addrow a k l A) = det A"
proof -
have "addrow a k l A = addrow_mat n a k l * A"
by (rule addrow_mat[OF A l])
also have "det (addrow_mat n a k l * A) = det (addrow_mat n a k l) * det A"
by (rule det_mult[OF _ A], auto)
also have "det (addrow_mat n a k l) = 1"
by (rule det_addrow_mat[OF k])
finally show ?thesis using A by simp
qed
lemma det_swaprows:
assumes *: "k < n" "l < n" and k: "k ≠ l" and A: "A ∈ carrier_mat n n"
shows "det (swaprows k l A) = - det A"
proof -
have "swaprows k l A = swaprows_mat n k l * A"
by (rule swaprows_mat[OF A *])
also have "det (swaprows_mat n k l * A) = det (swaprows_mat n k l) * det A"
by (rule det_mult[OF _ A], insert A, auto)
also have "det (swaprows_mat n k l) = - 1"
by (rule det_swaprows_mat[OF * k])
finally show ?thesis using A by simp
qed
lemma det_similar: assumes "similar_mat A B"
shows "det A = det B"
proof -
from similar_matD[OF assms] obtain n P Q where
carr: "{A, B, P, Q} ⊆ carrier_mat n n" (is "_ ⊆ ?C")
and PQ: "P * Q = 1⇩m n"
and AB: "A = P * B * Q" by blast
hence A: "A ∈ ?C" and B: "B ∈ ?C" and P: "P ∈ ?C" and Q: "Q ∈ ?C" by auto
from det_mult[OF P Q, unfolded PQ] have PQ: "det P * det Q = 1" by auto
from det_mult[OF _ Q, of "P * B", unfolded det_mult[OF P B] AB[symmetric]] P B
have "det A = det P * det B * det Q" by auto
also have "… = (det P * det Q) * det B" by (simp add: ac_simps)
also have "… = det B" unfolding PQ by simp
finally show ?thesis .
qed
lemma det_four_block_mat_upper_right_zero_col: assumes A1: "A1 ∈ carrier_mat n n"
and A20: "A2 = (0⇩m n 1)" and A3: "A3 ∈ carrier_mat 1 n"
and A4: "A4 ∈ carrier_mat 1 1"
shows "det (four_block_mat A1 A2 A3 A4) = det A1 * det A4" (is "det ?A = _")
proof -
let ?A = "four_block_mat A1 A2 A3 A4"
from A20 have A2: "A2 ∈ carrier_mat n 1" by auto
define A where "A = ?A"
from four_block_carrier_mat[OF A1 A4] A1
have A: "A ∈ carrier_mat (Suc n) (Suc n)" and dim: "dim_row A1 = n" unfolding A_def by auto
let ?Pn = "λ p. p permutes {0 ..< n}"
let ?Psn = "λ p. p permutes {0 ..< Suc n}"
let ?perm = "{p. ?Psn p}"
let ?permn = "{p. ?Pn p}"
let ?prod = "λ p. signof p * (∏i = 0..<Suc n. A $$ (p i, i))"
let ?prod' = "λ p. A $$ (p n, n) * signof p * (∏i = 0..<n. A $$ (p i, i))"
let ?prod'' = "λ p. signof p * (∏i = 0..< n. A $$ (p i, i))"
let ?prod''' = "λ p. signof p * (∏i = 0..< n. A1 $$ (p i, i))"
let ?p0 = "{p. p 0 = 0}"
have [simp]: "{0..<Suc n} - {n} = {0..< n}" by auto
{
fix p
assume "?Psn p"
have "?prod p = signof p * (A $$ (p n, n) * (∏ i ∈ {0..< n}. A $$ (p i, i)))"
by (subst prod.remove[of _ n], auto)
also have "… = A $$ (p n, n) * signof p * (∏ i ∈ {0..< n}. A $$ (p i, i))" by simp
finally have "?prod p = ?prod' p" .
} note prod_id = this
define prod' where "prod' = ?prod'"
{
fix i q
assume i: "i ∈ {0..< n}" "q permutes {0 ..< n}"
hence "Fun.swap n i id (q n) < n"
unfolding permutes_def by auto
hence "A $$ (Fun.swap n i id (q n), n) = 0"
unfolding A_def using A1 A20 A3 A4 by auto
hence "prod' (Fun.swap n i id ∘ q) = 0"
unfolding prod'_def by simp
} note zero = this
have cong: "⋀ a b c. b = c ⟹ a * b = a * c" by auto
have "det ?A = sum ?prod ?perm"
unfolding A_def[symmetric] using mat_det_left_def[OF A] A by simp
also have "… = sum prod' ?perm" unfolding prod'_def
by (rule sum.cong[OF refl], insert prod_id, auto)
also have "{0 ..< Suc n} = insert n {0 ..< n}" by auto
also have "sum prod' {p. p permutes …} =
(∑i∈insert n {0..<n}. ∑q∈?permn. prod' (Fun.swap n i id ∘ q))"
by (subst sum_over_permutations_insert, auto)
also have "… = (∑q∈?permn. prod' q) +
(∑i∈{0..<n}. ∑q∈?permn. prod' (Fun.swap n i id ∘ q))"
by (subst sum.insert, auto)
also have "(∑i∈{0..<n}. ∑q∈?permn. prod' (Fun.swap n i id ∘ q)) = 0"
by (rule sum.neutral, intro ballI, rule sum.neutral, intro ballI, rule zero, auto)
also have "(∑q∈ ?permn. prod' q) = A $$ (n,n) * (∑q∈ ?permn. ?prod'' q)"
unfolding prod'_def
by (subst sum_distrib_left, rule sum.cong[OF refl], auto simp: permutes_def ac_simps)
also have "A $$ (n,n) = A4 $$ (0,0)" unfolding A_def using A1 A2 A3 A4 by auto
also have "(∑q∈ ?permn. ?prod'' q) = (∑q∈ ?permn. ?prod''' q)"
by (rule sum.cong[OF refl], rule cong, rule prod.cong,
insert A1 A2 A3 A4, auto simp: permutes_def A_def)
also have "… = det A1"
unfolding mat_det_left_def[OF A1] dim by auto
also have "A4 $$ (0,0) = det A4"
using A4 unfolding det_def[of A4] by (auto simp: sign_def)
finally show ?thesis by simp
qed
lemma det_swap_initial_rows: assumes A: "A ∈ carrier_mat m m"
and lt: "k + n ≤ m"
shows "det A = (- 1) ^ (k * n) *
det (mat m m (λ(i, j). A $$ (if i < n then i + k else if i < k + n then i - n else i, j)))"
proof -
define sw where "sw = (λ (A :: 'a mat) xs. fold (λ (i,j). swaprows i j) xs A)"
have dim_sw[simp]: "dim_row (sw A xs) = dim_row A" "dim_col (sw A xs) = dim_col A" for xs A
unfolding sw_def by (induct xs arbitrary: A, auto)
{
fix xs and A :: "'a mat"
assume "dim_row A = dim_col A" "⋀ i j. (i,j) ∈ set xs ⟹ i < dim_col A ∧ j < dim_col A ∧ i ≠ j"
hence "det (sw A xs) = (-1)^(length xs) * det A"
unfolding sw_def
proof (induct xs arbitrary: A)
case (Cons xy xs A)
obtain x y where xy: "xy = (x,y)" by force
from Cons(3)[unfolded xy, of x y] Cons(2)
have [simp]: "det (swaprows x y A) = - det A"
by (intro det_swaprows, auto)
show ?case unfolding xy by (simp, insert Cons(2-), (subst Cons(1), auto)+)
qed simp
} note sw = this
define swb where "swb = (λ A i n. sw A (map (λ j. (j,Suc j)) [i ..< i + n]))"
{
fix k n and A :: "'a mat"
assume k_n: "