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: "k + n < dim_row A"
hence "swb A k n = mat (dim_row A) (dim_col A) (λ (i,j). let r =
(if i < k ∨ i > k + n then i else if i = k + n then k else Suc i)
in A $$ (r,j))"
proof (induct n)
case 0
show ?case unfolding swb_def sw_def by (rule eq_matI, auto)
next
case (Suc n)
hence dim: "k + n < dim_row A" by auto
have id: "swb A k (Suc n) = swaprows (k + n) (Suc k + n) (swb A k n)" unfolding swb_def sw_def by simp
show ?case unfolding id Suc(1)[OF dim]
by (rule eq_matI, insert Suc(2), auto)
qed
} note swb = this
define swbl where "swbl = (λ A k n. fold (λ i A. swb A i n) (rev [0 ..< k]) A)"
{
fix k n and A :: "'a mat"
assume k_n: "k + n ≤ dim_row A"
hence "swbl A k n = mat (dim_row A) (dim_col A) (λ (i,j). let r =
(if i < n then i + k else if i < k + n then i - n else i)
in A $$ (r,j))"
proof (induct k arbitrary: A)
case 0
thus ?case unfolding swbl_def by (intro eq_matI, auto simp: swb)
next
case (Suc k)
hence dim: "k + n < dim_row A" by auto
have id: "swbl A (Suc k) n = swbl (swb A k n) k n" unfolding swbl_def by simp
show ?case unfolding id swb[OF dim]
by (subst Suc(1), insert dim, force, intro eq_matI, auto simp: less_Suc_eq_le)
qed
} note swbl = this
{
fix k n and A :: "'a mat"
assume k_n: "k + n ≤ dim_col A" "dim_row A = dim_col A"
hence "det (swbl A k n) = (-1)^(k*n) * det A"
proof (induct k arbitrary: A)
case 0
thus ?case unfolding swbl_def by auto
next
case (Suc k)
hence dim: "k + n < dim_row A" by auto
have id: "swbl A (Suc k) n = swbl (swb A k n) k n" unfolding swbl_def by simp
have det: "det (swb A k n) = (-1)^n * det A" unfolding swb_def
by (subst sw, insert Suc(2-), auto)
show ?case unfolding id
by (subst Suc(1), insert Suc(2-), auto simp: det, auto simp: swb power_add)
qed
} note det_swbl = this
from assms have dim: "dim_row A = dim_col A" "k + n ≤ dim_col A" "k + n ≤ dim_row A" "dim_col A = m" by auto
from arg_cong[OF det_swbl[OF dim(2,1), unfolded swbl[OF dim(3)], unfolded Let_def dim],
of "λ x. (-1)^(k*n) * x"]
show ?thesis by simp
qed
lemma det_swap_rows: assumes A: "A ∈ carrier_mat (k + n) (k + n)"
shows "det A = (-1)^(k * n) * det (mat (k + n) (k + n) (λ (i,j).
A $$ ((if i < k then i + n else i - k),j)))"
proof -
have le: "n + k ≤ k + n" by simp
show ?thesis unfolding det_swap_initial_rows[OF A le]
by (intro arg_cong2[of _ _ _ _ "λ x y. ((-1)^x * det y)"], force, intro eq_matI, auto)
qed
lemma det_swap_final_rows: assumes A: "A ∈ carrier_mat m m"
and m: "m = l + k + n"
shows "det A = (- 1) ^ (k * n) *
det (mat m m (λ(i, j). A $$ (if i < l then i else if i < l + n then i + k else i - n, j)))"
(is "_ = _ * det ?M")
proof -
have m1: "m = (k + n) + l" using m by simp
have m2: "k + n ≤ m" using m by simp
have m3: "m = l + (n + k)" using m by simp
define M where "M = ?M"
let ?M1 = "mat m m (λ(i, j). A $$ (if i < k + n then i + l else i - (k + n), j))"
let ?M2 = "mat m m
(λ(i, j). A $$ (if i < n then i + k + l else if i < k + n then i - n + l else i - (k + n), j))"
have M2: "?M2 ∈ carrier_mat m m" by auto
have "det A = (- 1) ^ ((k + n) * l) * det ?M1"
unfolding det_swap_rows[OF A[unfolded m1]] m1[symmetric] by simp
also have "det ?M1 = (- 1) ^ (k * n) * det ?M2"
by (subst det_swap_initial_rows[OF _ m2], force, rule arg_cong[of _ _ "λ x. _ * det x"],
rule eq_matI, auto simp: m)
also have "det ?M2 = (- 1) ^ (l * (n + k)) * det M"
unfolding M_def det_swap_rows[OF M2[unfolded m3], folded m3]
by (rule arg_cong[of _ _ "λ x. _ * det x"], rule eq_matI, auto simp: m)
finally have "det A = (-1) ^ ((k + n) * l + (k * n) + l * (n + k)) * det M" (is "_ = ?b ^ _ * _")
by (simp add: power_add)
also have "(k + n) * l + (k * n) + l * (n + k) = 2 * (l * (n + k)) + k * n" by simp
also have "?b ^ … = ?b ^ (k * n)" by (simp add: power_add)
finally show ?thesis unfolding M_def .
qed
lemma det_swap_final_cols: assumes A: "A ∈ carrier_mat m m"
and m: "m = l + k + n"
shows "det A = (- 1) ^ (k * n) *
det (mat m m (λ(i, j). A $$ (i, if j < l then j else if j < l + n then j + k else j - n)))"
proof -
have "det A = det (A⇧T)" unfolding det_transpose[OF A] ..
also have "… = (- 1) ^ (k * n) *
det (mat m m (λ(i, j). A⇧T $$ (if i < l then i else if i < l + n then i + k else i - n, j)))"
(is "_ = _ * det ?M")
by (rule det_swap_final_rows[OF _ m], insert A, auto)
also have "det ?M = det (?M⇧T)" by (subst det_transpose, auto)
also have "?M⇧T = mat m m (λ(i, j). A $$ (i, if j < l then j else if j < l + n then j + k else j - n))"
unfolding transpose_mat_def using A m
by (intro eq_matI, auto)
finally show ?thesis .
qed
lemma det_swap_initial_cols: 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 $$ (i, if j < n then j + k else if j < k + n then j - n else j)))"
proof -
have "det A = det (A⇧T)" unfolding det_transpose[OF A] ..
also have "… = (- 1) ^ (k * n) *
det (mat m m (λ(j, i). A⇧T $$ (if j < n then j + k else if j < k + n then j - n else j,i)))"
(is "_ = _ * det ?M")
by (rule det_swap_initial_rows[OF _ lt], insert A, auto)
also have "det ?M = det (?M⇧T)" by (subst det_transpose, auto)
also have "?M⇧T = mat m m (λ(i, j). A $$ (i, if j < n then j + k else if j < k + n then j - n else j))"
unfolding transpose_mat_def using A lt
by (intro eq_matI, auto)
finally show ?thesis .
qed
lemma det_swap_cols: assumes A: "A ∈ carrier_mat (k + n) (k + n)"
shows "det A = (-1)^(k * n) * det (mat (k + n) (k + n) (λ (i,j).
A $$ (i,(if j < k then j + n else j - k))))" (is "_ = _ * det ?B")
proof -
have le: "n + k ≤ k + n" by simp
show ?thesis unfolding det_swap_initial_cols[OF A le]
by (intro arg_cong2[of _ _ _ _ "λ x y. ((-1)^x * det y)"], force, intro eq_matI, auto)
qed
lemma det_four_block_mat_upper_right_zero: fixes A1 :: "'a :: idom mat"
assumes A1: "A1 ∈ carrier_mat n n"
and A20: "A2 = (0⇩m n m)" and A3: "A3 ∈ carrier_mat m n"
and A4: "A4 ∈ carrier_mat m m"
shows "det (four_block_mat A1 A2 A3 A4) = det A1 * det A4"
using assms(2-)
proof (induct m arbitrary: A2 A3 A4)
case (0 A2 A3 A4)
hence *: "four_block_mat A1 A2 A3 A4 = A1" using A1
by (intro eq_matI, auto)
from 0 have 4: "A4 = 1⇩m 0" by auto
show ?case unfolding * unfolding 4 by simp
next
case (Suc m A2 A3 A4)
let ?m = "Suc m"
from Suc have A2: "A2 ∈ carrier_mat n ?m" by auto
note A20 = Suc(2)
note A34 = Suc(3-4)
let ?A = "four_block_mat A1 A2 A3 A4"
let ?P = "λ B3 B4 v k. v ≠ 0 ∧ v * det ?A = det (four_block_mat A1 A2 B3 B4)
∧ v * det A4 = det B4 ∧ B3 ∈ carrier_mat ?m n ∧ B4 ∈ carrier_mat ?m ?m ∧ (∀ i < k. B4 $$ (i,m) = 0)"
have "k ≤ m ⟹ ∃ B3 B4 v. ?P B3 B4 v k" for k
proof (induct k)
case 0
have "?P A3 A4 1 0" using A34 by auto
thus ?case by blast
next
case (Suc k)
then obtain B3 B4 v where v: "v ≠ 0" and det: "v * det ?A =
det (four_block_mat A1 A2 B3 B4)" "v * det A4 = det B4"
and B3: "B3 ∈ carrier_mat ?m n" and B4: "B4 ∈ carrier_mat ?m ?m" and 0: "∀ i < k. B4 $$ (i,m) = 0" by auto
show ?case
proof (cases "B4 $$ (k,m) = 0")
case True
with 0 have 0: "∀ i < Suc k. B4 $$ (i,m) = 0" using less_Suc_eq by auto
with v det B3 B4 have "?P B3 B4 v (Suc k)" by auto
thus ?thesis by blast
next
case Bk: False
let ?k = "Suc k"
from Suc(2) have k: "k < ?m" "Suc k < ?m" "k ≠ Suc k" by auto
show ?thesis
proof (cases "B4 $$ (?k,m) = 0")
case True
let ?B4 = "swaprows k (Suc k) B4"
let ?B3 = "swaprows k (Suc k) B3"
let ?B = "four_block_mat A1 A2 ?B3 ?B4"
let ?v = "-v"
from det_swaprows[OF k B4] det have det1: "?v * det A4 = det ?B4" by simp
from v have v: "?v ≠ 0" by auto
from B3 have B3': "?B3 ∈ carrier_mat ?m n" by auto
from B4 have B4': "?B4 ∈ carrier_mat ?m ?m" by auto
have "?v * det ?A = - det (four_block_mat A1 A2 B3 B4)" using det by simp
also have "… = det (swaprows (n + k) (n + ?k) (four_block_mat A1 A2 B3 B4))"
by (rule sym, rule det_swaprows[of _ "n + ?m"], insert A1 A2 B3 B4 k, auto)
also have "swaprows (n + k) (n + ?k) (four_block_mat A1 A2 B3 B4) = ?B"
proof (rule eq_matI, unfold index_mat_four_block index_mat_swaprows, goal_cases)
case (1 i j)
show ?case
proof (cases "i < n")
case True
thus ?thesis using 1(2) A1 A2 B3 B4 by simp
next
case False
hence "i = n + (i - n)" by simp
then obtain d where "i = n + d" by blast
thus ?thesis using 1 A1 A2 B3 B4 k(2) by simp
qed
qed auto
finally have det2: "?v * det ?A = det ?B" .
from True 0 B4 k(2) have "∀ i < Suc k. ?B4 $$ (i,m) = 0" unfolding less_Suc_eq by auto
with det1 det2 B3' B4' v have "?P ?B3 ?B4 ?v (Suc k)" by auto
thus ?thesis by blast
next
case False
let ?bk = "B4 $$ (?k,m)"
let ?b = "B4 $$ (k,m)"
let ?v = "v * ?bk"
let ?B3 = "addrow (- ?b) k ?k (multrow k ?bk B3)"
let ?B4 = "addrow (- ?b) k ?k (multrow k ?bk B4)"
have *: "det ?B4 = ?bk * det B4"
by (subst det_addrow[OF k(2-3)], force simp: B4, rule det_multrow[OF k(1) B4])
with det(2)[symmetric] have det2: "?v * det A4 = det ?B4" by (auto simp: ac_simps)
from 0 k(2) B4 have 0: "∀ i < Suc k. ?B4 $$ (i,m) = 0" unfolding less_Suc_eq by auto
from False v have v: "?v ≠ 0" by auto
from B3 have B3': "?B3 ∈ carrier_mat ?m n" by auto
from B4 have B4': "?B4 ∈ carrier_mat ?m ?m" by auto
let ?B' = "multrow (n + k) ?bk (four_block_mat A1 A2 B3 B4)"
have B': "?B' ∈ carrier_mat (n + ?m) (n + ?m)" using A1 A2 B3 B4 k by auto
let ?B = "four_block_mat A1 A2 ?B3 ?B4"
have "?v * det ?A = ?bk * det (four_block_mat A1 A2 B3 B4)" using det by simp
also have "… = det (addrow (- ?b) (n + k) (n + ?k) ?B')"
by (subst det_addrow[OF _ _ B'], insert k(2), force, force, rule sym, rule det_multrow[of _ "n + ?m"],
insert A1 A2 B3 B4 k, auto)
also have "addrow (- ?b) (n + k) (n + ?k) ?B' = ?B"
proof (rule eq_matI, unfold index_mat_four_block index_mat_multrow index_mat_addrow, goal_cases)
case (1 i j)
show ?case
proof (cases "i < n")
case True
thus ?thesis using 1(2) A1 A2 B3 B4 by simp
next
case False
hence "i = n + (i - n)" by simp
then obtain d where "i = n + d" by blast
thus ?thesis using 1 A1 A2 B3 B4 k(2) by simp
qed
qed auto
finally have det1: "?v * det ?A = det ?B" .
from det1 det2 B3' B4' v 0 have "?P ?B3 ?B4 ?v (Suc k)" by auto
thus ?thesis by blast
qed
qed
qed
from this[OF le_refl] obtain B3 B4 v where P: "?P B3 B4 v m" by blast
let ?B = "four_block_mat A1 A2 B3 B4"
from P have v: "v ≠ 0" and det: "v * det ?A = det ?B" "v * det A4 = det B4"
and B3: "B3 ∈ carrier_mat ?m n" and B4: "B4 ∈ carrier_mat ?m ?m" and 0: "⋀ i. i < m ⟹ B4 $$ (i, m) = 0"
by auto
let ?A2 = "0⇩m n m"
let ?A3 = "mat m n (λ ij. B3 $$ ij)"
let ?A4 = "mat m m (λ ij. B4 $$ ij)"
let ?B1 = "four_block_mat A1 ?A2 ?A3 ?A4"
let ?B2 = "0⇩m (n + m) 1"
let ?B3 = "mat 1 (n + m) (λ (i,j). if j < n then B3 $$ (m,j) else B4 $$ (m,j - n))"
let ?B4 = "mat 1 1 (λ _. B4 $$ (m,m))"
have B44: "B4 = four_block_mat ?A4 (0⇩m m 1) (mat 1 m (λ (i,j). B4 $$ (m,j))) ?B4"
proof (rule eq_matI, unfold index_mat_four_block dim_col_mat dim_row_mat, goal_cases)
case (1 i j)
hence [simp]: "¬ i < m ⟹ i = m" "¬ j < m ⟹ j = m" by auto
from 1 show ?case using B4 0 by auto
qed (insert B4, auto)
have "?B = four_block_mat ?B1 ?B2 ?B3 ?B4"
proof (rule eq_matI, unfold index_mat_four_block dim_col_mat dim_row_mat, goal_cases)
case (1 i j)
then consider (UL) "i < n + m" "j < n + m" | (UR) "i < n + m" "j = n + m"
| (LL) "i = n + m" "j < n + m" | (LR) "i = n + m" "j = n + m" using A1 by auto linarith
thus ?case
proof cases
case UL
hence [simp]: "¬ i < n ⟹ i - n < m"
"¬ j < n ⟹ j - n < m" "¬ j < n ⟹ j - n < Suc m" by auto
from UL show ?thesis using A1 A20 B3 B4 by simp
next
case LL
hence [simp]: "¬ j < n ⟹ j - n < m" "¬ j < n ⟹ j - n < Suc m" by auto
from LL show ?thesis using A1 A2 B3 B4 by simp
next
case LR
thus ?thesis using A1 A2 B3 B4 by simp
next
case UR
hence [simp]: "¬ i < n ⟹ i - n < m" by auto
from UR show ?thesis using A1 A20 0 B3 B4 by simp
qed
qed (insert B4, auto)
hence "det ?B = det (four_block_mat ?B1 ?B2 ?B3 ?B4)" by simp
also have "… = det ?B1 * det ?B4"
by (rule det_four_block_mat_upper_right_zero_col[of _ "n + m"], insert A1 A2 B3 B4, auto)
also have "det ?B1 = det A1 * det (mat m m (($$) B4))"
by (rule Suc(1), insert B3 B4, auto)
also have "… * det ?B4 = det A1 * (det (mat m m (($$) B4)) * det ?B4)" by simp
also have "det (mat m m (($$) B4)) * det ?B4 = det B4"
unfolding arg_cong[OF B44, of det]
by (subst det_four_block_mat_upper_right_zero_col[OF _ refl], auto)
finally have id: "det ?B = det A1 * det B4" .
from this[folded det] have "v * det ?A = v * (det A1 * det A4)" by simp
with v show "det ?A = det A1 * det A4" by simp
qed
lemma det_four_block_mat_lower_left_zero: fixes A1 :: "'a :: idom mat"
assumes A1: "A1 ∈ carrier_mat n n"
and A2: "A2 ∈ carrier_mat n m" and A30: "A3 = 0⇩m m n"
and A4: "A4 ∈ carrier_mat m m"
shows "det (four_block_mat A1 A2 A3 A4) = det A1 * det A4"
proof -
have A3: "A3 ∈ carrier_mat m n" using A30 by auto
show ?thesis
apply (subst det_transpose[OF four_block_carrier_mat[OF A1 A4], symmetric])
apply (subst transpose_four_block_mat[OF A1 A2 A3 A4])
apply (subst det_four_block_mat_upper_right_zero[of _ n _ m],
insert A1 A2 A30 A4, auto simp: det_transpose)
done
qed
context
begin
private lemma det_four_block_mat_preliminary: assumes A: "(A :: 'a :: idom mat) ∈ carrier_mat n n"
and B: "B ∈ carrier_mat n n"
and C: "C ∈ carrier_mat n n"
and D: "D ∈ carrier_mat n n"
and commute: "C * D = D * C"
and detD: "det D ≠ 0"
shows "det (four_block_mat A B C D) = det (A * D - B * C)"
proof -
let ?m = "n + n"
let ?M = "four_block_mat A B C D"
let ?N = "four_block_mat D (0⇩m n n) (-C) (1⇩m n)"
have M: "?M ∈ carrier_mat ?m ?m" using A B C D by auto
have N: "?N ∈ carrier_mat ?m ?m" using A B C D by auto
have "det ?M * det ?N = det (?M * ?N)" using det_mult[OF M N] ..
also have "?M * ?N = four_block_mat (A * D - B * C) B (0⇩m n n) D"
by (subst mult_four_block_mat[OF A B C D D], insert A B C D, auto simp: commute)
also have "det … = det (A * D - B * C) * det D"
by (rule det_four_block_mat_lower_left_zero, insert A B C D, auto)
also have "det ?N = det D"
by (subst det_four_block_mat_upper_right_zero[OF D], insert C, auto)
finally have "det ?M * det D = det (A * D - B * C) * det D" .
with detD show ?thesis by simp
qed
lemma det_four_block_mat: assumes A: "(A :: 'a :: idom mat) ∈ carrier_mat n n"
and B: "B ∈ carrier_mat n n"
and C: "C ∈ carrier_mat n n"
and D: "D ∈ carrier_mat n n"
and commute: "C * D = D * C"
shows "det (four_block_mat A B C D) = det (A * D - B * C)"
proof (cases "n = 0")
case True
hence "four_block_mat A B C D = A * D - B * C" using four_block_carrier_mat[OF A D, of B C]
A B C D by auto
thus ?thesis by simp
next
case n: False
define l where "l = map_mat (λ x :: 'a. [: x :])"
have coeff: "coeff [: x :] n = (if n = 0 then x else 0)" for x :: 'a and n
by (simp add: coeff_eq_0)
have l_mult: "l (A * B) = l A * l B" if "A ∈ carrier_mat n n" "B ∈ carrier_mat n n" for A B :: "'a mat"
unfolding l_def using that
apply (intro eq_matI, auto simp: scalar_prod_def coeff_sum intro!: poly_eqI)
subgoal for i j n
by (cases n, auto simp: coeff ac_simps)
done
let ?p0 = "map_mat (λp. poly p (0 :: 'a))"
have poly_det: "poly (det A) 0 = det (?p A)" if "A ∈ carrier_mat n n" for A n
apply (subst (1 2) det_def', use that in force, rule that)
unfolding poly_sum poly_mult poly_prod using that
by (intro sum.cong[OF refl] arg_cong2[of _ _ _ _ "(*)"] prod.cong[OF refl], auto simp: sign_def)
let ?A = "l A"
let ?B = "l B"
let ?C = "l C"
let ?D = "l D"
let ?Dx = "?D + monom 1 1 ⋅⇩m 1⇩m n"
from A B C D
have
lA: "?A ∈ carrier_mat n n" and
lB: "?B ∈ carrier_mat n n" and
lC: "?C ∈ carrier_mat n n" and
lD: "?D ∈ carrier_mat n n" and
lDx: "?Dx ∈ carrier_mat n n"
unfolding l_def by auto
have "?C * ?Dx = ?C * ?D + ?C * (monom 1 1 ⋅⇩m 1⇩m n)"
by (subst mult_add_distrib_mat[OF lC lD], auto)
also have "?C * ?D = l (C * D)" using l_mult[OF C D] by simp
also have "… = l (D * C)" using commute by auto
also have "… = ?D * ?C" using l_mult[OF D C] by simp
also have "?C * (monom 1 1 ⋅⇩m 1⇩m n) = (monom 1 1 ⋅⇩m 1⇩m n) * ?C" using lC by auto
also have "?D * ?C + … = ?Dx * ?C"
by (subst add_mult_distrib_mat[OF lD _ lC], auto)
finally have comm: "?C * ?Dx = ?Dx * ?C" .
have "det (four_block_mat ?A ?B ?C ?Dx) =
det (?A * ?Dx - ?B * ?C)"
proof (rule det_four_block_mat_preliminary[OF lA lB lC lDx comm])
define f where "f = (λ p. of_int (sign p) * (∏i = 0..<n. (l D + monom 1 1 ⋅⇩m 1⇩m n) $$ (i, p i)))"
have deg: "degree ([:D $$ ij:] + monom 1 (Suc 0)) = 1" for ij
by (subst degree_add_eq_right, auto simp: degree_monom_eq)
have deg_id: "degree (f id) = n" unfolding f_def
apply (simp, subst degree_prod_eq_sum_degree, insert D, auto simp: l_def deg)
subgoal for i using deg[of "(i,i)"] by auto
done
have "degree (det ?Dx) = degree (sum f {p. p permutes {0..<n}})"
by (subst det_def', use lD in force, auto simp: f_def)
also have "sum f {p. p permutes {0..<n}} = f id + sum f ({p. p permutes {0..<n}} - {id})"
by (rule sum.remove, auto intro: finite_permutations)
also have "degree … = degree (f id)"
proof (rule degree_add_eq_left, unfold deg_id,
rule le_less_trans[of _ "n - 1"], rule degree_sum_le,
force intro: finite_permutations)
fix p
assume p: "p ∈ {p. p permutes {0..<n}} - {id}"
then obtain i where i: "i ∈ {0 ..< n}" and pi: "p i ≠ i"
by (metis Diff_iff mem_Collect_eq permutes_empty permutes_superset singletonI)
from p i have pin: "p i < n" by auto
define g where "g = (λ i. (l D + monom 1 1 ⋅⇩m 1⇩m n) $$ (i, p i))"
have "degree (f p) ≤ degree (of_int (sign p) :: 'a poly) + degree (∏i = 0..<n. g i)"
unfolding f_def g_def by (rule degree_mult_le)
also have "degree (of_int (sign p) :: 'a poly) = 0" unfolding sign_def by auto
also have "0 + degree (∏i = 0..<n. g i) = degree (∏i = 0..<n. g i)" by simp
also have "(∏i = 0..<n. g i) = g i * (prod g ({0..<n} - {i}))"
by (subst prod.remove[OF _ i], auto)
also have "degree … ≤ degree (g i) + degree (prod g ({0..<n} - {i}))"
by (rule degree_mult_le)
also have "… = degree (prod g ({0..<n} - {i}))" unfolding g_def l_def using i D pi pin by auto
also have "… ≤ sum (degree ∘ g) ({0..<n} - {i})"
by (rule degree_prod_sum_le, auto)
also have "… ≤ sum (λ i. 1) ({0..<n} - {i})"
by (rule sum_mono, insert p D, auto simp: g_def o_def l_def deg)
also have "… = n - 1" using i by simp
finally show "degree (f p) ≤ n - 1" .
qed (insert n, auto)
also have "… = n" by fact
finally show "det ?Dx ≠ 0" using n by auto
qed
hence "poly (det (four_block_mat ?A ?B ?C ?Dx)) 0 = poly (det (?A * ?Dx - ?B * ?C)) 0" by simp
also have "… = det (?p0 (?A * (?D + monom 1 1 ⋅⇩m 1⇩m n) - ?B * ?C))"
by (rule poly_det, use lA lB lC lD in force)
also have "?A * (?D + monom 1 1 ⋅⇩m 1⇩m n) = ?A * ?D + l A * (monom 1 1 ⋅⇩m 1⇩m n)"
by (rule mult_add_distrib_mat[OF lA lD], auto)
also have "?A * (monom 1 1 ⋅⇩m 1⇩m n) = monom 1 1 ⋅⇩m ?A" using lA by auto
also have "?p0 (?A * ?D + … - ?B * ?C) = ?p0 (?A * ?D) - ?p0 (?B * ?C)"
by (intro eq_matI, insert lA lB lC lD, auto simp: poly_monom)
also have "?A * ?D = l (A * D)" using l_mult[OF A D] by auto
also have "?p0 … = A * D" unfolding l_def by fastforce
also have "?B * ?C = l (B * C)" using l_mult[OF B C] by auto
also have "?p0 … = B * C" unfolding l_def by fastforce
also have "poly (det (four_block_mat ?A ?B ?C ?Dx)) 0 = det (?p0 (four_block_mat ?A ?B ?C ?Dx))"
by (rule poly_det[OF four_block_carrier_mat[OF lA]], insert lD, auto)
also have "?p0 (four_block_mat ?A ?B ?C ?Dx) = four_block_mat (?p0 ?A) (?p0 ?B) (?p0 ?C) (?p0 ?Dx)"
by (rule map_four_block_mat[OF lA lB lC], insert lD, auto)
also have "?p0 ?A = A" unfolding l_def by fastforce
also have "?p0 ?B = B" unfolding l_def by fastforce
also have "?p0 ?C = C" unfolding l_def by fastforce
also have "?p0 ?Dx = D" unfolding l_def using D by (intro eq_matI, auto simp: poly_monom)
finally show ?thesis .
qed
end
lemma det_swapcols:
assumes *: "k < n" "l < n" "k ≠ l" and A: "A ∈ carrier_mat n n"
shows "det (swapcols k l A) = - det A"
proof -
let ?B = "transpose_mat A"
let ?C = "swaprows k l ?B"
let ?D = "transpose_mat ?C"
have C: "?C ∈ carrier_mat n n" and B: "?B ∈ carrier_mat n n"
unfolding transpose_carrier_mat swaprows_carrier using A by auto
show ?thesis
unfolding
swapcols_is_transp_swap_rows[OF A *(1-2)]
det_transpose[OF C] det_swaprows[OF * B] det_transpose[OF A] ..
qed
lemma swap_row_to_front_det: "A ∈ carrier_mat n n ⟹ I < n ⟹ det (swap_row_to_front A I)
= (-1)^I * det A"
proof (induct I arbitrary: A)
case (Suc I A)
from Suc(3) have I: "I < n" by auto
let ?I = "Suc I"
let ?A = "swaprows I ?I A"
have AA: "?A ∈ carrier_mat n n" using Suc(2) by simp
have "det (swap_row_to_front A (Suc I)) = det (swap_row_to_front ?A I)" by simp
also have "… = (-1)^I * det ?A" by (rule Suc(1)[OF AA I])
also have "det ?A = -1 * det A" using det_swaprows[OF I Suc(3) _ Suc(2)] by simp
finally show ?case by simp
qed simp
lemma swap_col_to_front_det: "A ∈ carrier_mat n n ⟹ I < n ⟹ det (swap_col_to_front A I)
= (-1)^I * det A"
proof (induct I arbitrary: A)
case (Suc I A)
from Suc(3) have I: "I < n" by auto
let ?I = "Suc I"
let ?A = "swapcols I ?I A"
have AA: "?A ∈ carrier_mat n n" using Suc(2) by simp
have "det (swap_col_to_front A (Suc I)) = det (swap_col_to_front ?A I)" by simp
also have "… = (-1)^I * det ?A" by (rule Suc(1)[OF AA I])
also have "det ?A = -1 * det A" using det_swapcols[OF I Suc(3) _ Suc(2)] by simp
finally show ?case by simp
qed simp
lemma swap_row_to_front_four_block: assumes A1: "A1 ∈ carrier_mat n m1"
and A2: "A2 ∈ carrier_mat n m2"
and A3: "A3 ∈ carrier_mat 1 m1"
and A4: "A4 ∈ carrier_mat 1 m2"
shows "swap_row_to_front (four_block_mat A1 A2 A3 A4) n = four_block_mat A3 A4 A1 A2"
by (subst swap_row_to_front_result[OF four_block_carrier_mat[OF A1 A4]], force,
rule eq_matI, insert A1 A2 A3 A4, auto)
lemma swap_col_to_front_four_block: assumes A1: "A1 ∈ carrier_mat n1 m"
and A2: "A2 ∈ carrier_mat n1 1"
and A3: "A3 ∈ carrier_mat n2 m"
and A4: "A4 ∈ carrier_mat n2 1"
shows "swap_col_to_front (four_block_mat A1 A2 A3 A4) m = four_block_mat A2 A1 A4 A3"
by (subst swap_col_to_front_result[OF four_block_carrier_mat[OF A1 A4]], force,
rule eq_matI, insert A1 A2 A3 A4, auto)
lemma det_four_block_mat_lower_right_zero_col: assumes A1: "A1 ∈ carrier_mat 1 n"
and A2: "A2 ∈ carrier_mat 1 1"
and A3: "A3 ∈ carrier_mat n n"
and A40: "A4 = (0⇩m n 1)"
shows "det (four_block_mat A1 A2 A3 A4) = (-1)^n * det A2 * det A3" (is "det ?A = _")
proof -
let ?B = "four_block_mat A3 A4 A1 A2"
from four_block_carrier_mat[OF A3 A2]
have B: "?B ∈ carrier_mat (Suc n) (Suc n)" by simp
from A40 have A4: "A4 ∈ carrier_mat n 1" by auto
from arg_cong[OF swap_row_to_front_four_block[OF A3 A4 A1 A2], of det]
swap_row_to_front_det[OF B, of n]
have "det ?A = (-1)^n * det ?B" by auto
also have "det ?B = det A3 * det A2"
by (rule det_four_block_mat_upper_right_zero_col[OF A3 A40 A1 A2])
finally show ?thesis by simp
qed
lemma det_four_block_mat_lower_left_zero_col: assumes A1: "A1 ∈ carrier_mat 1 1"
and A2: "A2 ∈ carrier_mat 1 n"
and A30: "A3 = (0⇩m n 1)"
and A4: "A4 ∈ carrier_mat n n"
shows "det (four_block_mat A1 A2 A3 A4) = det A1 * det A4" (is "det ?A = _")
proof -
from A30 have A3: "A3 ∈ carrier_mat n 1" by auto
let ?B = "four_block_mat A2 A1 A4 A3"
from four_block_carrier_mat[OF A2 A3]
have B: "?B ∈ carrier_mat (Suc n) (Suc n)" by simp
from arg_cong[OF swap_col_to_front_four_block[OF A2 A1 A4 A3], of det]
swap_col_to_front_det[OF B, of n]
have "det ?A = (-1)^n * det ?B" by auto
also have "det ?B = (- 1) ^ n * det A1 * det A4"
by (rule det_four_block_mat_lower_right_zero_col[OF A2 A1 A4 A30])
also have "(-1)^n * … = (-1 * -1)^n * det A1 * det A4"
unfolding power_mult_distrib by (simp add: ac_simps)
finally show ?thesis by simp
qed
lemma det_addcol[simp]:
assumes l: "l < n" and k: "k ≠ l" and A: "A ∈ carrier_mat n n"
shows "det (addcol a k l A) = det A"
proof -
have "addcol a k l A = A * addrow_mat n a l k"
using addcol_mat[OF A l].
also have "det (A * addrow_mat n a l k) = det A * det (addrow_mat n a l k)"
by(rule det_mult[OF A], auto)
also have "det (addrow_mat n a l k) = 1"
using det_addrow_mat[OF k[symmetric]].
finally show ?thesis using A by simp
qed
definition "insert_index i ≡ λi'. if i' < i then i' else Suc i'"
definition "delete_index i ≡ λi'. if i' < i then i' else i' - Suc 0"
lemma insert_index[simp]:
"i' < i ⟹ insert_index i i' = i'"
"i' ≥ i ⟹ insert_index i i' = Suc i'"
unfolding insert_index_def by auto
lemma delete_insert_index[simp]:
"delete_index i (insert_index i i') = i'"
unfolding insert_index_def delete_index_def by auto
lemma insert_delete_index:
assumes i'i: "i' ≠ i"
shows "insert_index i (delete_index i i') = i'"
unfolding insert_index_def delete_index_def using i'i by auto
definition "delete_dom p i ≡ λi'. p (insert_index i i')"
definition "delete_ran p j ≡ λi. delete_index j (p i)"
definition "permutation_delete p i = delete_ran (delete_dom p i) (p i)"
definition "insert_ran p j ≡ λi. insert_index j (p i)"
definition "insert_dom p i j ≡
λi'. if i' < i then p i' else if i' = i then j else p (i'-1)"
definition "permutation_insert i j p ≡ insert_dom (insert_ran p j) i j"
lemmas permutation_delete_expand =
permutation_delete_def[unfolded delete_dom_def delete_ran_def insert_index_def delete_index_def]
lemmas permutation_insert_expand =
permutation_insert_def[unfolded insert_dom_def insert_ran_def insert_index_def delete_index_def]
lemma permutation_insert_inserted[simp]:
"permutation_insert (i::nat) j p i = j"
unfolding permutation_insert_expand by auto
lemma permutation_insert_base:
assumes p: "p permutes {0..<n}"
shows "permutation_insert n n p = p"
proof (rule ext)
fix x show "permutation_insert n n p x = p x"
apply (cases rule: linorder_cases[of "x" "n"])
unfolding permutation_insert_expand
using permutes_others[OF p] p by auto
qed
lemma permutation_insert_row_step:
‹permutation_insert (Suc i) j p ∘ transpose i (Suc i) = permutation_insert i j p› (is ‹?l = ?r›)
proof (rule ext)
fix x
consider ‹x < i› | ‹x = i› | ‹x = Suc i› | ‹Suc i < x›
using Suc_lessI by (cases rule: linorder_cases [of x i]) blast+
then show ‹?l x = ?r x›
by cases (simp_all add: permutation_insert_expand)
qed
lemma permutation_insert_column_step:
assumes p: "p permutes {0..<n}" and "j < n"
shows "transpose j (Suc j) ∘ permutation_insert i (Suc j) p = permutation_insert i j p"
(is "?l = ?r")
proof (rule ext)
fix x show "?l x = ?r x"
proof (cases rule: linorder_cases[of "x" "i"])
case less note x = this
show ?thesis
apply (cases rule: linorder_cases[of "p x" "j"])
unfolding permutation_insert_expand using x by simp+
next case equal thus ?thesis by simp
next case greater note x = this
show ?thesis
apply (cases rule: linorder_cases[of "p (x-1)" "j"])
unfolding permutation_insert_expand using x by simp+
qed
qed
lemma delete_dom_image:
assumes i: "i ∈ {0..<Suc n}" (is "_ ∈ ?N")
assumes iff: "∀i' ∈ ?N. f i' = f i ⟶ i' = i"
shows "delete_dom f i ` {0..<n} = f ` ?N - {f i}" (is "?L = ?R")
proof(unfold set_eq_iff, intro allI iffI)
fix j'
{ assume L: "j' ∈ ?L"
then obtain i' where i': "i' ∈ {0..<n}" and dj': "delete_dom f i i' = j'" by auto
show "j' ∈ ?R"
proof(cases "i' < i")
case True
show ?thesis
unfolding image_def
unfolding Diff_iff
unfolding mem_Collect_eq singleton_iff
proof(intro conjI bexI)
show "j' ≠ f i"
proof
assume j': "j' = f i"
hence "f i' = f i"
using dj'[unfolded delete_dom_def insert_index_def] using True by simp
thus "False" using iff i True by auto
qed
show "j' = f i'"
using dj' True unfolding delete_dom_def insert_index_def by simp
qed (insert i',simp)
next case False
show ?thesis
unfolding image_def
unfolding Diff_iff
unfolding mem_Collect_eq singleton_iff
proof(intro conjI bexI)
show Si': "Suc i' ∈ ?N" using i' by auto
show "j' ≠ f i"
proof
assume j': "j' = f i"
hence "f (Suc i') = f i"
using dj'[unfolded delete_dom_def insert_index_def] j' False by simp
thus "False" using iff Si' False by auto
qed
show "j' = f (Suc i')"
using dj' False unfolding delete_dom_def insert_index_def by simp
qed
qed
}
{ assume R: "j' ∈ ?R"
then obtain i'
where i': "i' ∈ ?N" and j'fi: "j' ≠ f i" and j'fi': "j' = f i'" by auto
hence i'i: "i' ≠ i" using iff by auto
hence n: "n > 0" using i i' by auto
show "j' ∈ ?L"
proof (cases "i' < i")
case True show ?thesis
proof
show "j' = delete_dom f i i'"
unfolding delete_dom_def insert_index_def using True j'fi' by simp
qed (insert True i, simp)
next case False show ?thesis
proof
show "i'-1 ∈ {0..<n}" using i' n by auto
show "j' = delete_dom f i (i'-1)"
unfolding delete_dom_def insert_index_def using False j'fi' i'i by auto
qed
qed
}
qed
lemma delete_ran_image:
assumes j: "j ∈ {0..<Suc n}" (is "_ ∈ ?N")
assumes fimg: "f ` {0..<n} = ?N - {j}"
shows "delete_ran f j ` {0..<n} = {0..<n}" (is "?L = ?R")
proof(unfold set_eq_iff, intro allI iffI)
fix j'
{ assume L: "j' ∈ ?L"
then obtain i where i: "i ∈ {0..<n}" and ij': "delete_ran f j i = j'" by auto
have "f i ∈ ?N - {j}" using fimg i by blast
thus "j' ∈ ?R" using ij' j unfolding delete_ran_def delete_index_def by auto
}
{ assume R: "j' ∈ ?R" show "j' ∈ ?L"
proof (cases "j' < j")
case True
hence "j' ∈ ?N - {j}" using R by auto
then obtain i where fij': "f i = j'" and i: "i ∈ {0..<n}"
unfolding fimg[symmetric] by auto
have "delete_ran f j i = j'"
unfolding delete_ran_def delete_index_def unfolding fij' using True by simp
thus ?thesis using i by auto
next case False
hence "Suc j' ∈ ?N - {j}" using R by auto
then obtain i where fij': "f i = Suc j'" and i: "i ∈ {0..<n}"
unfolding fimg[symmetric] by auto
have "delete_ran f j i = j'"
unfolding delete_ran_def delete_index_def unfolding fij' using False by simp
thus ?thesis using i by auto
qed
}
qed
lemma delete_index_inj_on:
assumes iS: "i ∉ S"
shows "inj_on (delete_index i) S"
proof(intro inj_onI)
fix x y
assume eq: "delete_index i x = delete_index i y" and x: "x ∈ S" and y: "y ∈ S"
have "x ≠ i" "y ≠ i" using x y iS by auto
thus "x = y"
using eq unfolding delete_index_def
by(cases "x < i"; cases "y < i";simp)
qed
lemma insert_index_inj_on:
shows "inj_on (insert_index i) S"
proof(intro inj_onI)
fix x y
assume eq: "insert_index i x = insert_index i y" and x: "x ∈ S" and y: "y ∈ S"
show "x = y"
using eq unfolding insert_index_def
by(cases "x < i"; cases "y < i";simp)
qed
lemma delete_dom_inj_on:
assumes i: "i ∈ {0..<Suc n}" (is "_ ∈ ?N")
assumes inj: "inj_on f ?N"
shows "inj_on (delete_dom f i) {0..<n}"
proof (rule eq_card_imp_inj_on)
have "card ?N = card (f ` ?N)" using card_image[OF inj]..
hence "card {0..<n} = card (f ` ?N - {f i})" using i by auto
also have "... = card (delete_dom f i ` {0..<n})"
apply(subst delete_dom_image[symmetric])
using i inj unfolding inj_on_def by auto
finally show "card (delete_dom f i ` {0..<n}) = card {0..<n}"..
qed simp
lemma delete_ran_inj_on:
assumes j: "j ∈ {0..<Suc n}" (is "_ ∈ ?N")
assumes img: "f ` {0..<n} = ?N - {j}"
shows "inj_on (delete_ran f j) {0..<n}"
apply (rule eq_card_imp_inj_on)
unfolding delete_ran_image[OF j img] by simp+
lemma permutation_delete_bij_betw:
assumes i: "i ∈ {0 ..< Suc n}" (is "_ ∈ ?N")
assumes bij: "bij_betw p ?N ?N"
shows "bij_betw (permutation_delete p i) {0..<n} {0..<n}" (is "bij_betw ?p _ _")
proof-
have inj: "inj_on p ?N" using bij_betw_imp_inj_on[OF bij].
have ran: "p ` ?N = ?N" using bij_betw_imp_surj_on[OF bij].
hence j: "p i ∈ ?N" using i by auto
have "∀i'∈?N. p i' = p i ⟶ i' = i" using inj i unfolding inj_on_def by auto
from delete_dom_image[OF i this]
have "delete_dom p i ` {0..<n} = ?N - {p i}" unfolding ran.
from delete_ran_inj_on[OF j this] delete_ran_image[OF j this]
show ?thesis unfolding permutation_delete_def
using bij_betw_imageI by blast
qed
lemma permutation_delete_permutes:
assumes p: "p permutes {0 ..< Suc n}" (is "_ permutes ?N")
and i: "i < Suc n"
shows "permutation_delete p i permutes {0..<n}" (is "?p permutes ?N'")
proof (rule bij_imp_permutes, rule permutation_delete_bij_betw)
have pi: "p i < Suc n" using p i by auto
show "bij_betw p ?N ?N" using permutes_imp_bij[OF p].
fix x assume "x ∉ {0..<n}" hence x: "x ≥ n" by simp
show "?p x = x"
proof(cases "x < i")
case True thus ?thesis
unfolding permutation_delete_def using x i by simp
next case False
hence "p (Suc x) = Suc x" using x permutes_others[OF p] by auto
thus ?thesis
unfolding permutation_delete_expand using False pi x by simp
qed
qed (insert i,auto)
lemma permutation_insert_delete:
assumes p: "p permutes {0..<Suc n}"
and i: "i < Suc n"
shows "permutation_insert i (p i) (permutation_delete p i) = p"
(is "?l = _")
proof
fix i'
show "?l i' = p i'"
proof (cases rule: linorder_cases[of "i'" "i"])
case less note i'i = this
show ?thesis
proof (cases "p i = p i'")
case True
hence "i = i'" using permutes_inj[OF p] injD by metis
hence False using i'i by auto
thus ?thesis by auto
next case False thus ?thesis
unfolding permutation_insert_expand permutation_delete_expand
using i'i by auto
qed
next case equal thus ?thesis unfolding permutation_insert_expand by simp
next case greater hence i'i: "i' > i" by auto
hence cond: "¬ i' - 1 < i" using i'i by simp
show ?thesis
proof (cases rule: linorder_cases[of "p i'" "p i"])
case less
hence pd: "permutation_delete p i (i'-1) = p i'"
unfolding permutation_delete_expand
using i'i cond by auto
show ?thesis
unfolding permutation_insert_expand pd
using i'i less by simp
next case equal
hence "i = i'" using permutes_inj[OF p] injD by metis
hence False using i'i by auto
thus ?thesis by auto
next case greater
hence pd: "permutation_delete p i (i'-1) = p i' - 1"
unfolding permutation_delete_expand
using i'i cond by simp
show ?thesis
unfolding permutation_insert_expand pd
using i'i greater by auto
qed
qed
qed
lemma insert_index_exclude[simp]:
"insert_index i i' ≠ i" unfolding insert_index_def by auto
lemma insert_index_image:
assumes i: "i < Suc n"
shows "insert_index i ` {0..<n} = {0..<Suc n} - {i}" (is "?L = ?R")
proof(unfold set_eq_iff, intro allI iffI)
let ?N = "{0..<Suc n}"
fix i'
{ assume L: "i' ∈ ?L"
then obtain i''
where ins: "i' = insert_index i i''" and i'': "i'' ∈ {0..<n}" by auto
show "i' ∈ ?N - {i}"
proof(rule DiffI)
show "i' ∈ ?N" using ins unfolding insert_index_def using i'' by auto
show "i' ∉ {i}"
unfolding singleton_iff
unfolding ins unfolding insert_index_def by auto
qed
}
{ assume R: "i' ∈ ?R"
show "i' ∈ ?L"
proof(cases rule: linorder_cases[of "i'" "i"])
case less
hence i': "i' ∈ {0..<n}" using i by auto
hence "insert_index i i' = i'" unfolding insert_index_def using less by auto
thus ?thesis using i' by force
next case equal
hence False using R by auto
thus ?thesis by auto
next case greater
hence i'': "i'-1 ∈ {0..<n}" using i R by auto
hence "insert_index i (i'-1) = i'"
unfolding insert_index_def using greater by auto
thus ?thesis using i'' by force
qed
}
qed
lemma insert_ran_image:
assumes j: "j < Suc n"
assumes img: "f ` {0..<n} = {0..<n}"
shows "insert_ran f j ` {0..<n} = {0..<Suc n} - {j}" (is "?L = ?R")
proof -
have "?L = (λi. insert_index j (f i)) ` {0..<n}" unfolding insert_ran_def..
also have "... = (insert_index j ∘ f) ` {0..<n}" by auto
also have "... = insert_index j ` f ` {0..<n}" by auto
also have "... = insert_index j ` {0..<n}" unfolding img by auto
finally show ?thesis using insert_index_image[OF j] by auto
qed
lemma insert_dom_image:
assumes i: "i < Suc n" and j: "j < Suc n"
and img: "f ` {0..<n} = {0..<Suc n} - {j}" (is "_ = ?N - _")
shows "insert_dom f i j ` ?N = ?N" (is "?f ` _ = _")
proof(unfold set_eq_iff,intro allI iffI)
fix j'
{ assume "j' ∈ ?f ` ?N"
then obtain i' where i': "i' ∈ ?N" and j': "j' = ?f i'" by auto
show "j' ∈ ?N"
proof (cases rule:linorder_cases[of "i'" "i"])
case less
hence "i' ∈ {0..<n}" using i by auto
hence "f i' < Suc n" using imageI[of i' "{0..<n}" f] img by auto
thus ?thesis
unfolding j' unfolding insert_dom_def using less by auto
next case equal
thus ?thesis unfolding j' insert_dom_def using j by auto
next case greater
hence "i'-1 ∈ {0..<n}" using i' by auto
hence "f (i'-1) < Suc n" using imageI[of "i'-1" "{0..<n}" f] img by auto
thus ?thesis
unfolding j' insert_dom_def using greater by auto
qed
}
{ assume j': "j' ∈ ?N" show "j' ∈ ?f ` ?N"
proof (cases "j' = j")
case True
hence "?f i = j'" unfolding insert_dom_def by auto
thus ?thesis using i by auto
next case False
hence j': "j' ∈ ?N - {j}" using j j' by auto
then obtain i' where j'fi: "j' = f i'" and i': "i' ∈ {0..<n}"
unfolding img[symmetric] by auto
show ?thesis
proof(cases "i' < i")
case True thus ?thesis unfolding j'fi insert_dom_def using i' by auto
next case False
hence "?f (Suc i') = j'" unfolding j'fi insert_dom_def using i' by auto
thus ?thesis using i' by auto
qed
qed
}
qed
lemma insert_ran_inj_on:
assumes inj: "inj_on f {0..<n}" and j: "j < Suc n"
shows "inj_on (insert_ran f j) {0..<n}" (is "inj_on ?f _")
proof (rule inj_onI)
fix i i'
assume i: "i ∈ {0..<n}" and i': "i' ∈ {0..<n}" and eq: "?f i = ?f i'"
note eq2 = eq[unfolded insert_ran_def insert_index_def]
have "f i = f i'"
proof (cases "f i < j")
case True
moreover have "f i' < j" apply (rule ccontr) using eq2 True by auto
ultimately show ?thesis using eq2 by auto
next case False
moreover have "¬ f i' < j" apply (rule ccontr) using eq2 False by auto
ultimately show ?thesis using eq2 by auto
qed
from inj_onD[OF inj this i i'] show "i = i'".
qed
lemma insert_dom_inj_on:
assumes inj: "inj_on f {0..<n}"
and i: "i < Suc n" and j: "j < Suc n"
and img: "f ` {0..<n} = {0..<Suc n} - {j}" (is "_ = ?N - _")
shows "inj_on (insert_dom f i j) ?N"
apply(rule eq_card_imp_inj_on)
unfolding insert_dom_image[OF i j img] by simp+
lemma permutation_insert_bij_betw:
assumes q: "q permutes {0..<n}" and i: "i < Suc n" and j: "j < Suc n"
shows "bij_betw (permutation_insert i j q) {0..<Suc n} {0..<Suc n}"
(is "bij_betw ?q ?N _")
proof (rule bij_betw_imageI)
have img: "q ` {0..<n} = {0..<n}" using permutes_image[OF q].
show "?q ` ?N = ?N"
unfolding permutation_insert_def
using insert_dom_image[OF i j insert_ran_image[OF j permutes_image[OF q]]].
have inj: "inj_on q {0..<n}"
apply(rule subset_inj_on) using permutes_inj[OF q] by auto
show "inj_on ?q ?N"
unfolding permutation_insert_def
using insert_dom_inj_on[OF _ i j]
using insert_ran_inj_on[OF inj j] insert_ran_image[OF j img] by auto
qed
lemma permutation_insert_permutes:
assumes q: "q permutes {0..<n}"
and i: "i < Suc n" and j: "j < Suc n"
shows "permutation_insert i j q permutes {0..<Suc n}" (is "?p permutes ?N")
using permutation_insert_bij_betw[OF q i j]
proof (rule bij_imp_permutes)
fix i' assume "i' ∉ ?N"
moreover hence "q (i'-1) = i'-1" using permutes_others[OF q] by auto
ultimately show "?p i' = i'"
unfolding permutation_insert_expand using i j by auto
qed
lemma permutation_fix:
assumes i: "i < Suc n" and j: "j < Suc n"
shows "{ p. p permutes {0..<Suc n} ∧ p i = j } =
permutation_insert i j ` { q. q permutes {0..<n} }"
(is "?L = ?R")
unfolding set_eq_iff
proof(intro allI iffI)
let ?N = "{0..<Suc n}"
fix p
{ assume "p ∈ ?L"
hence p: "p permutes ?N" and pij: "p i = j" by auto
show "p ∈ ?R"
unfolding mem_Collect_eq
using permutation_delete_permutes[OF p i]
using permutation_insert_delete[OF p i,symmetric]
unfolding pij by auto
}
{ assume "p ∈ ?R"
then obtain q where pq: "p = permutation_insert i j q" and q: "q permutes {0..<n}" by auto
hence "p i = j" unfolding permutation_insert_expand by simp
thus "p ∈ ?L"
using pq permutation_insert_permutes[OF q i j] by auto
}
qed
lemma permutation_split_ran:
assumes j: "j ∈ S"
shows "{ p. p permutes S } = (⋃i ∈ S. { p. p permutes S ∧ p i = j })"
(is "?L = ?R")
unfolding set_eq_iff
proof(intro allI iffI)
fix p
{ assume "p ∈ ?L"
hence p: "p permutes S" by auto
obtain i where i: "i ∈ S" and pij: "p i = j" using j permutes_image[OF p] by force
thus "p ∈ ?R" using p by auto
}
{ assume "p ∈ ?R"
then obtain i
where p: "p permutes S" and i: "i ∈ S" and pij: "p i = j"
by auto
show "p ∈ ?L"
unfolding mem_Collect_eq using p.
}
qed
lemma permutation_disjoint_dom:
assumes i: "i ∈ S" and i': "i' ∈ S" and j: "j ∈ S" and ii': "i ≠ i'"
shows "{ p. p permutes S ∧ p i = j } ∩ { p. p permutes S ∧ p i' = j } = {}"
(is "?L ∩ ?R = {}")
proof -
{
fix p assume "p ∈ ?L ∩ ?R"
hence p: "p permutes S" and "p i = j" and "p i' = j" by auto
hence "p i = p i'" by auto
note injD[OF permutes_inj[OF p] this]
hence False using ii' by auto
}
thus ?thesis by auto
qed
lemma permutation_disjoint_ran:
assumes i: "i ∈ S" and j: "j ∈ S" and j': "j' ∈ S" and jj': "j ≠ j'"
shows "{ p. p permutes S ∧ p i = j } ∩ { p. p permutes S ∧ p i = j' } = {}"
(is "?L ∩ ?R = {}")
proof -
{
fix p assume "p ∈ ?L ∩ ?R"
hence "p permutes S" and "p i = j" and "p i = j'" by auto
hence False using jj' by auto
}
thus ?thesis by auto
qed
lemma permutation_insert_inj_on:
assumes "i < Suc n"
assumes "j < Suc n"
shows "inj_on (permutation_insert i j) { q. q permutes {0..<n} }"
(is "inj_on ?f ?S")
proof (rule inj_onI)
fix q q'
assume "q ∈ ?S" "q' ∈ ?S"
hence q: "q permutes {0..<n}" and q': "q' permutes {0..<n}" by auto
assume "?f q = ?f q'"
hence eq: "permutation_insert i j q = permutation_insert i j q'" by auto
note eq = cong[OF eq refl, unfolded permutation_insert_expand]
show qq': "q = q'"
proof(rule ext)
fix x
have foo: "Suc x - 1 = x" by auto
show "q x = q' x"
proof(cases "x < i")
case True thus ?thesis apply(cases "q x < j";cases "q' x < j") using eq[of x] by auto
next case False thus ?thesis
apply(cases "q x < j";cases "q' x < j") using eq[of "Suc x"] by auto
qed
qed
qed
lemma signof_permutation_insert:
assumes p: "p permutes {0..<n}" and i: "i < Suc n" and j: "j < Suc n"
shows "signof (permutation_insert i j p) = (-1::'a::ring_1)^(i+j) * signof p"
proof -
{ fix j assume "j ≤ n"
hence "signof (permutation_insert n (n-j) p) = (-1::'a)^(n+(n-j)) * signof p"
proof(induct "j")
case 0 show ?case using permutation_insert_base[OF p] by (simp add: mult_2[symmetric])
next case (Suc j)
hence Sjn: "Suc j ≤ n" and j: "j < n" and Sj: "n - Suc j < n" by auto
hence n0: "n > 0" by auto
have ease: "Suc (n - Suc j) = n - j" using j by auto
let ?swap = "transpose (n - Suc j) (n - j)"
let ?prev = "permutation_insert n (n - j) p"
have "signof (permutation_insert n (n - Suc j) p) = signof (?swap ∘ ?prev)"
unfolding permutation_insert_column_step [OF p Sj, unfolded ease] ..
also have "... = signof ?swap * signof ?prev"
proof(rule signof_compose)
show "?swap permutes {0..<Suc n}" by (rule permutes_swap_id,auto)
show "?prev permutes {0..<Suc n}" by (rule permutation_insert_permutes[OF p],auto)
qed
also have "signof ?swap = -1"
proof-
have "n - Suc j < n - j" using Sjn by simp
thus ?thesis unfolding sign_swap_id by simp
qed
also have "signof ?prev = (-1::'a) ^ (n + (n - j)) * signof p" using Suc(1) j by auto
also have "(-1) * ... = (-1) ^ (1 + n + (n - j)) * signof p" by simp
also have "n - j = 1 + (n - Suc j)" using j by simp
also have "1 + n + ... = 2 + (n + (n - Suc j))" by simp
also have "(-1::'a) ^ ... = (-1) ^ 2 * (-1) ^ (n + (n - Suc j))" by simp
also have "... = (-1) ^ (n + (n - Suc j))" by simp
finally show ?case.
qed
}
note col = this
have nj: "n - j ≤ n" using j by auto
have row_base: "signof (permutation_insert n j p) = (-1::'a)^(n+j) * signof p"
using col[OF nj] using j by simp
{ fix i assume "i ≤ n"
hence "signof (permutation_insert (n-i) j p) = (-1::'a)^((n-i)+j) * signof p"
proof (induct i)
case 0 show ?case using row_base by auto
next case (Suc i)
hence Sin: "Suc i ≤ n" and i: "i ≤ n" and Si: "n - Suc i < n" by auto
have ease: "Suc (n - Suc i) = n - i" using Sin by auto
let ?prev = "permutation_insert (n-i) j p"
let ?swap = "transpose (n - Suc i) (n-i)"
have "signof (permutation_insert (n - Suc i) j p) = signof (?prev ∘ ?swap)"
using permutation_insert_row_step[of "n - Suc i"] unfolding ease by auto
also have "... = signof ?prev * signof ?swap"
proof(rule signof_compose)
show "?swap permutes {0..<Suc n}" by (rule permutes_swap_id,auto)
show "?prev permutes {0..<Suc n}"
apply(rule permutation_insert_permutes[OF p]) using j by auto
qed
also have "signof ?swap = (-1)"
proof-
have "n - Suc i < n - i" using Sin by simp
thus ?thesis unfolding sign_swap_id by simp
qed
also have "signof ?prev = (-1::'a) ^ (n - i + j) * signof p"
using Suc(1)[OF i].
also have "... * (-1) = (-1) ^ Suc (n - i + j) * signof p"
by auto
also have "Suc (n - i + j) = Suc (Suc (n - Suc i + j))"
using Sin by auto
also have "(-1::int) ^ ... = (-1) ^ (n - Suc i + j)" by auto
ultimately show ?case by auto
qed
}
note row = this
have ni: "n - i ≤ n" using i by auto
show ?thesis using row[OF ni] using i by simp
qed
lemma foo:
assumes i: "i < Suc n" and j: "j < Suc n"
assumes q: "q permutes {0..<n}"
shows "{(i', permutation_insert i j q i') | i'. i' ∈ {0..<Suc n} - {i} } =
{ (insert_index i i'', insert_index j (q i'')) | i''. i'' < n }" (is "?L = ?R")
unfolding set_eq_iff
proof(intro allI iffI)
fix ij
{ assume "ij ∈ ?L"
then obtain i'
where ij: "ij = (i', permutation_insert i j q i')" and i': "i' < Suc n" and i'i: "i' ≠ i"
by auto
show "ij ∈ ?R" unfolding mem_Collect_eq
proof(intro exI conjI)
show "ij = (insert_index i (delete_index i i'), insert_index j (q (delete_index i i')))"
using ij unfolding insert_delete_index[OF i'i] using i'i
unfolding permutation_insert_expand insert_index_def delete_index_def by auto
show "delete_index i i' < n" using i' i i'i unfolding delete_index_def by auto
qed
}
{ assume "ij ∈ ?R"
then obtain i''
where ij: "ij = (insert_index i i'', insert_index j (q i''))" and i'': "i'' < n"
by auto
show "ij ∈ ?L" unfolding mem_Collect_eq
proof(intro exI conjI)
show "insert_index i i'' ∈ {0..<Suc n} - {i}"
unfolding insert_index_image[OF i,symmetric] using i'' by auto
have "insert_index j (q i'') = permutation_insert i j q (insert_index i i'')"
unfolding permutation_insert_expand insert_index_def by auto
thus "ij = (insert_index i i'', permutation_insert i j q (insert_index i i''))"
unfolding ij by auto
qed
}
qed
definition "mat_delete A i j ≡
mat (dim_row A - 1) (dim_col A - 1) (λ(i',j').
A $$ (if i' < i then i' else Suc i', if j' < j then j' else Suc j'))"
lemma mat_delete_dim[simp]:
"dim_row (mat_delete A i j) = dim_row A - 1"
"dim_col (mat_delete A i j) = dim_col A - 1"
unfolding mat_delete_def by auto
lemma mat_delete_carrier:
assumes A: "A ∈ carrier_mat m n"
shows "mat_delete A i j ∈ carrier_mat (m-1) (n-1)" unfolding mat_delete_def using A by auto
lemma "mat_delete_index":
assumes A: "A ∈ carrier_mat (Suc n) (Suc n)"
and i: "i < Suc n" and j: "j < Suc n"
and i': "i' < n" and j': "j' < n"
shows "A $$ (insert_index i i', insert_index j j') = mat_delete A i j $$ (i', j')"
unfolding mat_delete_def
unfolding permutation_insert_expand
unfolding insert_index_def
using A i j i' j' by auto
definition "cofactor A i j = (-1)^(i+j) * det (mat_delete A i j)"
lemma laplace_expansion_column:
assumes A: "(A :: 'a :: comm_ring_1 mat) ∈ carrier_mat n n"
and j: "j < n"
shows "det A = (∑i<n. A $$ (i,j) * cofactor A i j)"
proof -
define l where "l = n-1"
have A: "A ∈ carrier_mat (Suc l) (Suc l)"
and jl: "j < Suc l" using A j unfolding l_def by auto
let ?N = "{0 ..< Suc l}"
define f where "f = (λp i. A $$ (i, p i))"
define g where "g = (λp. prod (f p) ?N)"
define h where "h = (λp. signof p * g p)"
define Q where "Q = { q . q permutes {0..<l} }"
have jN: "j ∈ ?N" using jl by auto
have disj: "∀i ∈ ?N. ∀i' ∈ ?N. i ≠ i' ⟶
{p. p permutes ?N ∧ p i = j} ∩ {p. p permutes ?N ∧ p i' = j} = {}"
using permutation_disjoint_dom[OF _ _ jN] by auto
have fin: "∀i∈?N. finite {p. p permutes ?N ∧ p i = j}"
using finite_permutations[of ?N] by auto
have "det A = sum h { p. p permutes ?N }"
using det_def'[OF A] unfolding h_def g_def f_def using atLeast0LessThan by auto
also have "... = sum h (⋃i∈?N. {p. p permutes ?N ∧ p i = j})"
unfolding permutation_split_ran[OF jN]..
also have "... = (∑i∈?N. sum h { p | p. p permutes ?N ∧ p i = j})"
using sum.UNION_disjoint[OF _ fin disj] by auto
also {
fix i assume "i ∈ ?N"
hence i: "i < Suc l" by auto
have "sum h { p | p. p permutes ?N ∧ p i = j} = sum h (permutation_insert i j ` Q)"
using permutation_fix[OF i jl] unfolding Q_def by auto
also have "... = sum (h ∘ permutation_insert i j) Q"
unfolding Q_def using sum.reindex[OF permutation_insert_inj_on[OF i jl]].
also have "... = (∑ q ∈ Q.
signof (permutation_insert i j q) * prod (f (permutation_insert i j q)) ?N)"
unfolding h_def g_def Q_def by simp
also {
fix q assume "q ∈ Q"
hence q: "q permutes {0..<l}" unfolding Q_def by auto
let ?p = "permutation_insert i j q"
have fin: "finite (?N - {i})" by auto
have notin: "i ∉ ?N - {i}" by auto
have close: "insert i (?N - {i}) = ?N" using notin i by auto
have "prod (f ?p) ?N = f ?p i * prod (f ?p) (?N-{i})"
unfolding prod.insert[OF fin notin, unfolded close] by auto
also have "... = A $$ (i, j) * prod (f ?p) (?N-{i})"
unfolding f_def Q_def using permutation_insert_inserted by simp
also have "prod (f ?p) (?N-{i}) = prod (λi'. A $$ (i', permutation_insert i j q i')) (?N-{i})"
unfolding f_def..
also have "... = prod (λij. A $$ ij) ((λi'. (i', permutation_insert i j q i')) ` (?N-{i}))"
(is "_ = prod _ ?part")
unfolding prod.reindex[OF inj_on_convol_ident] o_def..
also have "?part = {(i', permutation_insert i j q i') | i'. i' ∈ ?N-{i} }"
unfolding image_def by metis
also have "... = {(insert_index i i'', insert_index j (q i'')) | i''. i'' < l}"
unfolding foo[OF i jl q]..
also have "... = ((λi''. (insert_index i i'', insert_index j (q i''))) ` {0..<l})"
unfolding image_def by auto
also have "prod (λij. A $$ ij)... = prod ((λij. A $$ ij) ∘ (λi''. (insert_index i i'', insert_index j (q i'')))) {0..<l}"
proof(subst prod.reindex[symmetric])
have 1: "inj (λi''. (i'', insert_index j (q i'')))" using inj_on_convol_ident.
have 2: "inj (λ(i'',j). (insert_index i i'', j))"
apply (intro injI) using injD[OF insert_index_inj_on[of _ UNIV]] by auto
have "inj (λi''. (insert_index i i'', insert_index j (q i'')))"
using inj_compose[OF 2 1] unfolding o_def by auto
thus "inj_on (λi''. (insert_index i i'', insert_index j (q i''))) {0..<l}"
using subset_inj_on by auto
qed auto
also have "... = prod (λi''. A $$ (insert_index i i'', insert_index j (q i''))) {0..<l}"
by auto
also have "... = prod (λi''. mat_delete A i j $$ (i'', q i'')) {0..<l}"
proof (rule prod.cong[OF refl], unfold atLeastLessThan_iff, elim conjE)
fix x assume x: "x < l"
show "A $$ (insert_index i x, insert_index j (q x)) = mat_delete A i j $$ (x, q x)"
apply(rule mat_delete_index[OF A i jl]) using q x by auto
qed
finally have "prod (f ?p) ?N =
A $$ (i, j) * (∏i'' = 0..< l. mat_delete A i j $$ (i'', q i''))"
by auto
hence "signof ?p * prod (f ?p) ?N = (-1::'a)^(i+j) * signof q * ..."
unfolding signof_permutation_insert[OF q i jl] by auto
}
hence "... = (∑ q ∈ Q. (-1)^(i+j) * signof q *
A $$ (i, j) * (∏i'' = 0 ..< l. mat_delete A i j $$ (i'', q i'')))"
by(intro sum.cong[OF refl],auto)
also have "... = ( ∑ q ∈ Q. A $$ (i, j) * (-1)^(i+j) *
( signof q * (∏i'' = 0..< l. mat_delete A i j $$ (i'', q i'')) ) )"
by (intro sum.cong[OF refl],auto)
also have "... = A $$ (i, j) * (-1)^(i+j) *
( ∑ q ∈ Q. signof q * (∏i''= 0 ..< l. mat_delete A i j $$ (i'', q i'')) )"
unfolding sum_distrib_left by auto
also have "... = (A $$ (i, j) * (-1)^(i+j) * det (mat_delete A i j))"
unfolding det_def'[OF mat_delete_carrier[OF A]]
unfolding Q_def by auto
finally have "sum h {p | p. p permutes ?N ∧ p i = j} = A $$ (i, j) * cofactor A i j"
unfolding cofactor_def by auto
}
hence "... = (∑i∈?N. A $$ (i,j) * cofactor A i j)" by auto
finally show ?thesis unfolding atLeast0LessThan using A j unfolding l_def by auto
qed
lemma laplace_expansion_row:
assumes A: "(A :: 'a :: comm_ring_1 mat) ∈ carrier_mat n n"
and i: "i < n"
shows "det A = (∑j<n. A $$ (i,j) * cofactor A i j)"
proof -
have "det A = det (A⇧T)" using det_transpose[OF A] by simp
also have "… = (∑j<n. A⇧T $$ (j, i) * cofactor A⇧T j i)"
by (rule laplace_expansion_column[OF _ i], insert A, auto)
also have "… = (∑j<n. A $$ (i,j) * cofactor A i j)" unfolding cofactor_def
proof (rule sum.cong[OF refl], rule arg_cong2[of _ _ _ _ "λ x y. x * y"], goal_cases)
case (1 j)
thus ?case using A i by auto
next
case (2 j)
have "det (mat_delete A⇧T j i) = det ((mat_delete A⇧T j i)⇧T)"
by (subst det_transpose, insert A, auto simp: mat_delete_def)
also have "(mat_delete A⇧T j i)⇧T = mat_delete A i j"
unfolding mat_delete_def using A by auto
finally show ?case by (simp add: ac_simps)
qed
finally show ?thesis .
qed
lemma degree_det_le: assumes "⋀ i j. i < n ⟹ j < n ⟹ degree (A $$ (i,j)) ≤ k"
and A: "A ∈ carrier_mat n n"
shows "degree (det A) ≤ k * n"
proof -
{
fix p
assume p: "p permutes {0..<n}"
have "(∑x = 0..<n. degree (A $$ (x, p x))) ≤ (∑x = 0..<n. k)"
by (rule sum_mono[OF assms(1)], insert p, auto)
also have "… = k * n" unfolding sum_constant by simp
also note calculation
} note * = this
show ?thesis unfolding det_def'[OF A]
apply (rule degree_sum_le)
apply (simp_all add: finite_permutations)
apply (drule *)
apply (rule order.trans [OF degree_mult_le])
apply simp
apply (rule order.trans [OF degree_prod_sum_le])
apply simp_all
done
qed
lemma upper_triangular_imp_det_eq_0_iff:
fixes A :: "'a :: idom mat"
assumes "A ∈ carrier_mat n n" and "upper_triangular A"
shows "det A = 0 ⟷ 0 ∈ set (diag_mat A)"
using assms by (auto simp: det_upper_triangular)
lemma det_identical_columns:
assumes A: "A ∈ carrier_mat n n"
and ij: "i ≠ j"
and i: "i < n" and j: "j < n"
and r: "col A i = col A j"
shows "det A = 0"
proof-
have "det A = det A⇧T" using det_transpose[OF A] ..
also have "... = 0"
proof (rule det_identical_rows[of _ n i j])
show "row (transpose_mat A) i = row (transpose_mat A) j"
using A i j r by auto
qed (auto simp add: assms)
finally show ?thesis .
qed
definition adj_mat :: "'a :: comm_ring_1 mat ⇒ 'a mat" where
"adj_mat A = mat (dim_row A) (dim_col A) (λ (i,j). cofactor A j i)"
lemma adj_mat: assumes A: "A ∈ carrier_mat n n"
shows "adj_mat A ∈ carrier_mat n n"
"A * adj_mat A = det A ⋅⇩m 1⇩m n"
"adj_mat A * A = det A ⋅⇩m 1⇩m n"
proof -
from A have dims: "dim_row A = n" "dim_col A = n" by auto
show aA: "adj_mat A ∈ carrier_mat n n" unfolding adj_mat_def dims by simp
{
fix i j
assume ij: "i < n" "j < n"
define B where "B = mat n n (λ (i',j'). if i' = j then A $$ (i,j') else A $$ (i',j'))"
have "(A * adj_mat A) $$ (i,j) = (∑ k < n. A $$ (i,k) * cofactor A j k)"
unfolding times_mat_def scalar_prod_def adj_mat_def using ij A by (auto intro: sum.cong)
also have "… = (∑ k < n. A $$ (i,k) * (-1)^(j + k) * det (mat_delete A j k))"
unfolding cofactor_def by (auto intro: sum.cong)
also have "… = (∑ k < n. B $$ (j,k) * (-1)^(j + k) * det (mat_delete B j k))"
by (rule sum.cong[OF refl], intro arg_cong2[of _ _ _ _ "λ x y. y * _ * det x"], insert A ij,
auto simp: B_def mat_delete_def)
also have "… = (∑ k < n. B $$ (j,k) * cofactor B j k)"
unfolding cofactor_def by (simp add: ac_simps)
also have "… = det B"
by (rule laplace_expansion_row[symmetric], insert ij, auto simp: B_def)
also have "… = (if i = j then det A else 0)"
proof (cases "i = j")
case True
hence "B = A" using A by (auto simp add: B_def)
with True show ?thesis by simp
next
case False
have "det B = 0"
by (rule Determinant.det_identical_rows[OF _ False ij], insert A ij, auto simp: B_def)
with False show ?thesis by simp
qed
also have "… = (det A ⋅⇩m 1⇩m n) $$ (i,j)" using ij by auto
finally have "(A * adj_mat A) $$ (i, j) = (det A ⋅⇩m 1⇩m n) $$ (i, j)" .
} note main = this
show "A * adj_mat A = det A ⋅⇩m 1⇩m n"
by (rule eq_matI[OF main], insert A aA, auto)
{
fix i j
assume ij: "i < n" "j < n"
define B where "B = mat n n (λ (i',j'). if j' = i then A $$ (i',j) else A $$ (i',j'))"
have "(adj_mat A * A) $$ (i,j) = (∑ k < n. A $$ (k,j) * cofactor A k i)"
unfolding times_mat_def scalar_prod_def adj_mat_def using ij A by (auto intro: sum.cong)
also have "… = (∑ k < n. A $$ (k,j) * (-1)^(k + i) * det (mat_delete A k i))"
unfolding cofactor_def by (auto intro: sum.cong)
also have "… = (∑ k < n. B $$ (k,i) * (-1)^(k + i) * det (mat_delete B k i))"
by (rule sum.cong[OF refl], intro arg_cong2[of _ _ _ _ "λ x y. y * _ * det x"], insert A ij,
auto simp: B_def mat_delete_def)
also have "… = (∑ k < n. B $$ (k,i) * cofactor B k i)"
unfolding cofactor_def by (simp add: ac_simps)
also have "… = det B"
by (rule laplace_expansion_column[symmetric], insert ij, auto simp: B_def)
also have "… = (if i = j then det A else 0)"
proof (cases "i = j")
case True
hence "B = A" using A by (auto simp add: B_def)
with True show ?thesis by simp
next
case False
have "det B = 0"
by (rule Determinant.det_identical_columns[OF _ False ij], insert A ij, auto simp: B_def)
with False show ?thesis by simp
qed
also have "… = (det A ⋅⇩m 1⇩m n) $$ (i,j)" using ij by auto
finally have "(adj_mat A * A) $$ (i, j) = (det A ⋅⇩m 1⇩m n) $$ (i, j)" .
} note main = this
show "adj_mat A * A = det A ⋅⇩m 1⇩m n"
by (rule eq_matI[OF main], insert A aA, auto)
qed
definition "replace_col A b k = mat (dim_row A) (dim_col A) (λ (i,j). if j = k then b $ i else A $$ (i,j))"
lemma cramer_lemma_mat:
assumes A: "A ∈ carrier_mat n n"
and x: "x ∈ carrier_vec n"
and k: "k < n"
shows "det (replace_col A (A *⇩v x) k) = x $ k * det A"
proof -
define b where "b = A *⇩v x"
have b: "b ∈ carrier_vec n" using A x unfolding b_def by auto
let ?Ab = "replace_col A b k"
have Ab: "?Ab ∈ carrier_mat n n" using A by (auto simp: replace_col_def)
have "x $ k * det A = (det A ⋅⇩v x) $ k" using A k x by auto
also have "det A ⋅⇩v x = det A ⋅⇩v (1⇩m n *⇩v x)" using x by auto
also have "… = (det A ⋅⇩m 1⇩m n) *⇩v x" using A x by auto
also have "… = (adj_mat A * A) *⇩v x" using adj_mat[OF A] by simp
also have "… = adj_mat A *⇩v b" using adj_mat[OF A] A x unfolding b_def
by (metis assoc_mult_mat_vec)
also have "… $ k = row (adj_mat A) k ∙ b" using adj_mat[OF A] b k by auto
also have "… = det (replace_col A b k)" unfolding scalar_prod_def using b k A
by (subst laplace_expansion_column[OF Ab k], auto intro!: sum.cong arg_cong[of _ _ det]
arg_cong[of _ _ "λ x. _ * x"] eq_matI
simp: replace_col_def adj_mat_def Matrix.row_def cofactor_def mat_delete_def ac_simps)
finally show ?thesis unfolding b_def by simp
qed
end