33175

1 
(* Title: Determinants


2 
Author: Amine Chaieb, University of Cambridge


3 
*)


4 


5 
header {* Traces, Determinant of square matrices and some properties *}


6 


7 
theory Determinants


8 
imports Euclidean_Space Permutations


9 
begin


10 


11 
subsection{* First some facts about products*}


12 
lemma setprod_insert_eq: "finite A \<Longrightarrow> setprod f (insert a A) = (if a \<in> A then setprod f A else f a * setprod f A)"


13 
apply clarsimp


14 
by(subgoal_tac "insert a A = A", auto)


15 


16 
lemma setprod_add_split:


17 
assumes mn: "(m::nat) <= n + 1"


18 
shows "setprod f {m.. n+p} = setprod f {m .. n} * setprod f {n+1..n+p}"


19 
proof


20 
let ?A = "{m .. n+p}"


21 
let ?B = "{m .. n}"


22 
let ?C = "{n+1..n+p}"


23 
from mn have un: "?B \<union> ?C = ?A" by auto


24 
from mn have dj: "?B \<inter> ?C = {}" by auto


25 
have f: "finite ?B" "finite ?C" by simp_all


26 
from setprod_Un_disjoint[OF f dj, of f, unfolded un] show ?thesis .


27 
qed


28 


29 


30 
lemma setprod_offset: "setprod f {(m::nat) + p .. n + p} = setprod (\<lambda>i. f (i + p)) {m..n}"


31 
apply (rule setprod_reindex_cong[where f="op + p"])


32 
apply (auto simp add: image_iff Bex_def inj_on_def)


33 
apply arith


34 
apply (rule ext)


35 
apply (simp add: add_commute)


36 
done


37 


38 
lemma setprod_singleton: "setprod f {x} = f x" by simp


39 


40 
lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" by simp


41 


42 
lemma setprod_numseg: "setprod f {m..0} = (if m=0 then f 0 else 1)"


43 
"setprod f {m .. Suc n} = (if m \<le> Suc n then f (Suc n) * setprod f {m..n}


44 
else setprod f {m..n})"


45 
by (auto simp add: atLeastAtMostSuc_conv)


46 


47 
lemma setprod_le: assumes fS: "finite S" and fg: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (g x :: 'a::ordered_idom)"


48 
shows "setprod f S \<le> setprod g S"


49 
using fS fg


50 
apply(induct S)


51 
apply simp


52 
apply auto


53 
apply (rule mult_mono)


54 
apply (auto intro: setprod_nonneg)


55 
done


56 


57 
(* FIXME: In Finite_Set there is a useless further assumption *)


58 
lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_by_zero, field})"


59 
apply (erule finite_induct)


60 
apply (simp)


61 
apply simp


62 
done


63 


64 
lemma setprod_le_1: assumes fS: "finite S" and f: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (1::'a::ordered_idom)"


65 
shows "setprod f S \<le> 1"


66 
using setprod_le[OF fS f] unfolding setprod_1 .


67 


68 
subsection{* Trace *}


69 


70 
definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" where


71 
"trace A = setsum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"


72 


73 
lemma trace_0: "trace(mat 0) = 0"


74 
by (simp add: trace_def mat_def)


75 


76 
lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"


77 
by (simp add: trace_def mat_def)


78 


79 
lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"


80 
by (simp add: trace_def setsum_addf)


81 


82 
lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n)  B) = trace A  trace B"


83 
by (simp add: trace_def setsum_subtractf)


84 


85 
lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)"


86 
apply (simp add: trace_def matrix_matrix_mult_def)


87 
apply (subst setsum_commute)


88 
by (simp add: mult_commute)


89 


90 
(*  *)


91 
(* Definition of determinant. *)


92 
(*  *)


93 


94 
definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where


95 
"det A = setsum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)) {p. p permutes (UNIV :: 'n set)}"


96 


97 
(*  *)


98 
(* A few general lemmas we need below. *)


99 
(*  *)


100 


101 
lemma setprod_permute:


102 
assumes p: "p permutes S"


103 
shows "setprod f S = setprod (f o p) S"


104 
proof


105 
{assume "\<not> finite S" hence ?thesis by simp}


106 
moreover


107 
{assume fS: "finite S"


108 
then have ?thesis


109 
apply (simp add: setprod_def cong del:strong_setprod_cong)


110 
apply (rule ab_semigroup_mult.fold_image_permute)


111 
apply (auto simp add: p)


112 
apply unfold_locales


113 
done}


114 
ultimately show ?thesis by blast


115 
qed


116 


117 
lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"


118 
by (blast intro!: setprod_permute)


119 


120 
(*  *)


121 
(* Basic determinant properties. *)


122 
(*  *)


123 


124 
lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n::finite)"


125 
proof


126 
let ?di = "\<lambda>A i j. A$i$j"


127 
let ?U = "(UNIV :: 'n set)"


128 
have fU: "finite ?U" by simp


129 
{fix p assume p: "p \<in> {p. p permutes ?U}"


130 
from p have pU: "p permutes ?U" by blast


131 
have sth: "sign (inv p) = sign p"


132 
by (metis sign_inverse fU p mem_def Collect_def permutation_permutes)


133 
from permutes_inj[OF pU]


134 
have pi: "inj_on p ?U" by (blast intro: subset_inj_on)


135 
from permutes_image[OF pU]


136 
have "setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transp A) i (inv p i)) (p ` ?U)" by simp


137 
also have "\<dots> = setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U"


138 
unfolding setprod_reindex[OF pi] ..


139 
also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U"


140 
proof


141 
{fix i assume i: "i \<in> ?U"


142 
from i permutes_inv_o[OF pU] permutes_in_image[OF pU]


143 
have "((\<lambda>i. ?di (transp A) i (inv p i)) o p) i = ?di A i (p i)"


144 
unfolding transp_def by (simp add: expand_fun_eq)}


145 
then show "setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)


146 
qed


147 
finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth


148 
by simp}


149 
then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse)


150 
apply (rule setsum_cong2) by blast


151 
qed


152 


153 
lemma det_lowerdiagonal:


154 
fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}"


155 
assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"


156 
shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"


157 
proof


158 
let ?U = "UNIV:: 'n set"


159 
let ?PU = "{p. p permutes ?U}"


160 
let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"


161 
have fU: "finite ?U" by simp


162 
from finite_permutations[OF fU] have fPU: "finite ?PU" .


163 
have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)


164 
{fix p assume p: "p \<in> ?PU {id}"


165 
from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+


166 
from permutes_natset_le[OF pU] pid obtain i where


167 
i: "p i > i" by (metis not_le)


168 
from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast


169 
from setprod_zero[OF fU ex] have "?pp p = 0" by simp}


170 
then have p0: "\<forall>p \<in> ?PU {id}. ?pp p = 0" by blast


171 
from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis


172 
unfolding det_def by (simp add: sign_id)


173 
qed


174 


175 
lemma det_upperdiagonal:


176 
fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}"


177 
assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0"


178 
shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"


179 
proof


180 
let ?U = "UNIV:: 'n set"


181 
let ?PU = "{p. p permutes ?U}"


182 
let ?pp = "(\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"


183 
have fU: "finite ?U" by simp


184 
from finite_permutations[OF fU] have fPU: "finite ?PU" .


185 
have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)


186 
{fix p assume p: "p \<in> ?PU {id}"


187 
from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+


188 
from permutes_natset_ge[OF pU] pid obtain i where


189 
i: "p i < i" by (metis not_le)


190 
from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast


191 
from setprod_zero[OF fU ex] have "?pp p = 0" by simp}


192 
then have p0: "\<forall>p \<in> ?PU {id}. ?pp p = 0" by blast


193 
from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis


194 
unfolding det_def by (simp add: sign_id)


195 
qed


196 


197 
lemma det_diagonal:


198 
fixes A :: "'a::comm_ring_1^'n^'n::finite"


199 
assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0"


200 
shows "det A = setprod (\<lambda>i. A$i$i) (UNIV::'n set)"


201 
proof


202 
let ?U = "UNIV:: 'n set"


203 
let ?PU = "{p. p permutes ?U}"


204 
let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"


205 
have fU: "finite ?U" by simp


206 
from finite_permutations[OF fU] have fPU: "finite ?PU" .


207 
have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)


208 
{fix p assume p: "p \<in> ?PU  {id}"


209 
then have "p \<noteq> id" by simp


210 
then obtain i where i: "p i \<noteq> i" unfolding expand_fun_eq by auto


211 
from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast


212 
from setprod_zero [OF fU ex] have "?pp p = 0" by simp}


213 
then have p0: "\<forall>p \<in> ?PU  {id}. ?pp p = 0" by blast


214 
from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis


215 
unfolding det_def by (simp add: sign_id)


216 
qed


217 


218 
lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n::finite) = 1"


219 
proof


220 
let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n"


221 
let ?U = "UNIV :: 'n set"


222 
let ?f = "\<lambda>i j. ?A$i$j"


223 
{fix i assume i: "i \<in> ?U"


224 
have "?f i i = 1" using i by (vector mat_def)}


225 
hence th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U"


226 
by (auto intro: setprod_cong)


227 
{fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"


228 
have "?f i j = 0" using i j ij by (vector mat_def) }


229 
then have "det ?A = setprod (\<lambda>i. ?f i i) ?U" using det_diagonal


230 
by blast


231 
also have "\<dots> = 1" unfolding th setprod_1 ..


232 
finally show ?thesis .


233 
qed


234 


235 
lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n::finite) = 0"


236 
by (simp add: det_def setprod_zero)


237 


238 
lemma det_permute_rows:


239 
fixes A :: "'a::comm_ring_1^'n^'n::finite"


240 
assumes p: "p permutes (UNIV :: 'n::finite set)"


241 
shows "det(\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A"


242 
apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric])


243 
apply (subst sum_permutations_compose_right[OF p])


244 
proof(rule setsum_cong2)


245 
let ?U = "UNIV :: 'n set"


246 
let ?PU = "{p. p permutes ?U}"


247 
fix q assume qPU: "q \<in> ?PU"


248 
have fU: "finite ?U" by simp


249 
from qPU have q: "q permutes ?U" by blast


250 
from p q have pp: "permutation p" and qp: "permutation q"


251 
by (metis fU permutation_permutes)+


252 
from permutes_inv[OF p] have ip: "inv p permutes ?U" .


253 
have "setprod (\<lambda>i. A$p i$ (q o p) i) ?U = setprod ((\<lambda>i. A$p i$(q o p) i) o inv p) ?U"


254 
by (simp only: setprod_permute[OF ip, symmetric])


255 
also have "\<dots> = setprod (\<lambda>i. A $ (p o inv p) i $ (q o (p o inv p)) i) ?U"


256 
by (simp only: o_def)


257 
also have "\<dots> = setprod (\<lambda>i. A$i$q i) ?U" by (simp only: o_def permutes_inverses[OF p])


258 
finally have thp: "setprod (\<lambda>i. A$p i$ (q o p) i) ?U = setprod (\<lambda>i. A$i$q i) ?U"


259 
by blast


260 
show "of_int (sign (q o p)) * setprod (\<lambda>i. A$ p i$ (q o p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\<lambda>i. A$i$q i) ?U"


261 
by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult)


262 
qed


263 


264 
lemma det_permute_columns:


265 
fixes A :: "'a::comm_ring_1^'n^'n::finite"


266 
assumes p: "p permutes (UNIV :: 'n set)"


267 
shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A"


268 
proof


269 
let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n"


270 
let ?At = "transp A"


271 
have "of_int (sign p) * det A = det (transp (\<chi> i. transp A $ p i))"


272 
unfolding det_permute_rows[OF p, of ?At] det_transp ..


273 
moreover


274 
have "?Ap = transp (\<chi> i. transp A $ p i)"


275 
by (simp add: transp_def Cart_eq)


276 
ultimately show ?thesis by simp


277 
qed


278 


279 
lemma det_identical_rows:


280 
fixes A :: "'a::ordered_idom^'n^'n::finite"


281 
assumes ij: "i \<noteq> j"


282 
and r: "row i A = row j A"


283 
shows "det A = 0"


284 
proof


285 
have tha: "\<And>(a::'a) b. a = b ==> b =  a ==> a = 0"


286 
by simp


287 
have th1: "of_int (1) =  1" by (metis of_int_1 of_int_minus number_of_Min)


288 
let ?p = "Fun.swap i j id"


289 
let ?A = "\<chi> i. A $ ?p i"


290 
from r have "A = ?A" by (simp add: Cart_eq row_def swap_def)


291 
hence "det A = det ?A" by simp


292 
moreover have "det A =  det ?A"


293 
by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1)


294 
ultimately show "det A = 0" by (metis tha)


295 
qed


296 


297 
lemma det_identical_columns:


298 
fixes A :: "'a::ordered_idom^'n^'n::finite"


299 
assumes ij: "i \<noteq> j"


300 
and r: "column i A = column j A"


301 
shows "det A = 0"


302 
apply (subst det_transp[symmetric])


303 
apply (rule det_identical_rows[OF ij])


304 
by (metis row_transp r)


305 


306 
lemma det_zero_row:


307 
fixes A :: "'a::{idom, ring_char_0}^'n^'n::finite"


308 
assumes r: "row i A = 0"


309 
shows "det A = 0"


310 
using r


311 
apply (simp add: row_def det_def Cart_eq)


312 
apply (rule setsum_0')


313 
apply (auto simp: sign_nz)


314 
done


315 


316 
lemma det_zero_column:


317 
fixes A :: "'a::{idom,ring_char_0}^'n^'n::finite"


318 
assumes r: "column i A = 0"


319 
shows "det A = 0"


320 
apply (subst det_transp[symmetric])


321 
apply (rule det_zero_row [of i])


322 
by (metis row_transp r)


323 


324 
lemma det_row_add:


325 
fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n"


326 
shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) =


327 
det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +


328 
det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)"


329 
unfolding det_def Cart_lambda_beta setsum_addf[symmetric]


330 
proof (rule setsum_cong2)


331 
let ?U = "UNIV :: 'n set"


332 
let ?pU = "{p. p permutes ?U}"


333 
let ?f = "(\<lambda>i. if i = k then a i + b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"


334 
let ?g = "(\<lambda> i. if i = k then a i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"


335 
let ?h = "(\<lambda> i. if i = k then b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"


336 
fix p assume p: "p \<in> ?pU"


337 
let ?Uk = "?U  {k}"


338 
from p have pU: "p permutes ?U" by blast


339 
have kU: "?U = insert k ?Uk" by blast


340 
{fix j assume j: "j \<in> ?Uk"


341 
from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j"


342 
by simp_all}


343 
then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"


344 
and th2: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?h i $ p i) ?Uk"


345 
apply 


346 
apply (rule setprod_cong, simp_all)+


347 
done


348 
have th3: "finite ?Uk" "k \<notin> ?Uk" by auto


349 
have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"


350 
unfolding kU[symmetric] ..


351 
also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"


352 
apply (rule setprod_insert)


353 
apply simp


354 
by blast


355 
also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk)" by (simp add: ring_simps)


356 
also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?h i $ p i) ?Uk)" by (metis th1 th2)


357 
also have "\<dots> = setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i $ p i) (insert k ?Uk)"


358 
unfolding setprod_insert[OF th3] by simp


359 
finally have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?g i $ p i) ?U + setprod (\<lambda>i. ?h i $ p i) ?U" unfolding kU[symmetric] .


360 
then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i $ p i) ?U"


361 
by (simp add: ring_simps)


362 
qed


363 


364 
lemma det_row_mul:


365 
fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n"


366 
shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) =


367 
c* det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)"


368 


369 
unfolding det_def Cart_lambda_beta setsum_right_distrib


370 
proof (rule setsum_cong2)


371 
let ?U = "UNIV :: 'n set"


372 
let ?pU = "{p. p permutes ?U}"


373 
let ?f = "(\<lambda>i. if i = k then c*s a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n"


374 
let ?g = "(\<lambda> i. if i = k then a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n"


375 
fix p assume p: "p \<in> ?pU"


376 
let ?Uk = "?U  {k}"


377 
from p have pU: "p permutes ?U" by blast


378 
have kU: "?U = insert k ?Uk" by blast


379 
{fix j assume j: "j \<in> ?Uk"


380 
from j have "?f j $ p j = ?g j $ p j" by simp}


381 
then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"


382 
apply 


383 
apply (rule setprod_cong, simp_all)


384 
done


385 
have th3: "finite ?Uk" "k \<notin> ?Uk" by auto


386 
have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"


387 
unfolding kU[symmetric] ..


388 
also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"


389 
apply (rule setprod_insert)


390 
apply simp


391 
by blast


392 
also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" by (simp add: ring_simps)


393 
also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)"


394 
unfolding th1 by (simp add: mult_ac)


395 
also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"


396 
unfolding setprod_insert[OF th3] by simp


397 
finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)" unfolding kU[symmetric] .


398 
then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = c * (of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U)"


399 
by (simp add: ring_simps)


400 
qed


401 


402 
lemma det_row_0:


403 
fixes b :: "'n::finite \<Rightarrow> _ ^ 'n"


404 
shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0"


405 
using det_row_mul[of k 0 "\<lambda>i. 1" b]


406 
apply (simp)


407 
unfolding vector_smult_lzero .


408 


409 
lemma det_row_operation:


410 
fixes A :: "'a::ordered_idom^'n^'n::finite"


411 
assumes ij: "i \<noteq> j"


412 
shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A"


413 
proof


414 
let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n"


415 
have th: "row i ?Z = row j ?Z" by (vector row_def)


416 
have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A"


417 
by (vector row_def)


418 
show ?thesis


419 
unfolding det_row_add [of i] det_row_mul[of i] det_identical_rows[OF ij th] th2


420 
by simp


421 
qed


422 


423 
lemma det_row_span:


424 
fixes A :: "'a:: ordered_idom^'n^'n::finite"


425 
assumes x: "x \<in> span {row j A j. j \<noteq> i}"


426 
shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"


427 
proof


428 
let ?U = "UNIV :: 'n set"


429 
let ?S = "{row j A j. j \<noteq> i}"


430 
let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)"


431 
let ?P = "\<lambda>x. ?d (row i A + x) = det A"


432 
{fix k


433 


434 
have "(if k = i then row i A + 0 else row k A) = row k A" by simp}


435 
then have P0: "?P 0"


436 
apply 


437 
apply (rule cong[of det, OF refl])


438 
by (vector row_def)


439 
moreover


440 
{fix c z y assume zS: "z \<in> ?S" and Py: "?P y"


441 
from zS obtain j where j: "z = row j A" "i \<noteq> j" by blast


442 
let ?w = "row i A + y"


443 
have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector


444 
have thz: "?d z = 0"


445 
apply (rule det_identical_rows[OF j(2)])


446 
using j by (vector row_def)


447 
have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 ..


448 
then have "?P (c*s z + y)" unfolding thz Py det_row_mul[of i] det_row_add[of i]


449 
by simp }


450 


451 
ultimately show ?thesis


452 
apply 


453 
apply (rule span_induct_alt[of ?P ?S, OF P0])


454 
apply blast


455 
apply (rule x)


456 
done


457 
qed


458 


459 
(*  *)


460 
(* May as well do this, though it's a bit unsatisfactory since it ignores *)


461 
(* exact duplicates by considering the rows/columns as a set. *)


462 
(*  *)


463 


464 
lemma det_dependent_rows:


465 
fixes A:: "'a::ordered_idom^'n^'n::finite"


466 
assumes d: "dependent (rows A)"


467 
shows "det A = 0"


468 
proof


469 
let ?U = "UNIV :: 'n set"


470 
from d obtain i where i: "row i A \<in> span (rows A  {row i A})"


471 
unfolding dependent_def rows_def by blast


472 
{fix j k assume jk: "j \<noteq> k"


473 
and c: "row j A = row k A"


474 
from det_identical_rows[OF jk c] have ?thesis .}


475 
moreover


476 
{assume H: "\<And> i j. i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A"


477 
have th0: " row i A \<in> span {row j Aj. j \<noteq> i}"


478 
apply (rule span_neg)


479 
apply (rule set_rev_mp)


480 
apply (rule i)


481 
apply (rule span_mono)


482 
using H i by (auto simp add: rows_def)


483 
from det_row_span[OF th0]


484 
have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)"


485 
unfolding right_minus vector_smult_lzero ..


486 
with det_row_mul[of i "0::'a" "\<lambda>i. 1"]


487 
have "det A = 0" by simp}


488 
ultimately show ?thesis by blast


489 
qed


490 


491 
lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n::finite))" shows "det A = 0"


492 
by (metis d det_dependent_rows rows_transp det_transp)


493 


494 
(*  *)


495 
(* Multilinearity and the multiplication formula. *)


496 
(*  *)


497 


498 
lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)"


499 
apply (rule iffD1[OF Cart_lambda_unique]) by vector


500 


501 
lemma det_linear_row_setsum:


502 
assumes fS: "finite S"


503 
shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n::finite) = setsum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S"


504 
proof(induct rule: finite_induct[OF fS])


505 
case 1 thus ?case apply simp unfolding setsum_empty det_row_0[of k] ..


506 
next


507 
case (2 x F)


508 
then show ?case by (simp add: det_row_add cong del: if_weak_cong)


509 
qed


510 


511 
lemma finite_bounded_functions:


512 
assumes fS: "finite S"


513 
shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"


514 
proof(induct k)


515 
case 0


516 
have th: "{f. \<forall>i. f i = i} = {id}" by (auto intro: ext)


517 
show ?case by (auto simp add: th)


518 
next


519 
case (Suc k)


520 
let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i"


521 
let ?S = "?f ` (S \<times> {f. (\<forall>i\<in>{1..k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1..k} \<longrightarrow> f i = i)})"


522 
have "?S = {f. (\<forall>i\<in>{1.. Suc k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1.. Suc k} \<longrightarrow> f i = i)}"


523 
apply (auto simp add: image_iff)


524 
apply (rule_tac x="x (Suc k)" in bexI)


525 
apply (rule_tac x = "\<lambda>i. if i = Suc k then i else x i" in exI)


526 
apply (auto intro: ext)


527 
done


528 
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]


529 
show ?case by metis


530 
qed


531 


532 


533 
lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by (auto intro: ext)


534 


535 
lemma det_linear_rows_setsum_lemma:


536 
assumes fS: "finite S" and fT: "finite T"


537 
shows "det((\<chi> i. if i \<in> T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n::finite) =


538 
setsum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))


539 
{f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"


540 
using fT


541 
proof(induct T arbitrary: a c set: finite)


542 
case empty


543 
have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)" by vector


544 
from "empty.prems" show ?case unfolding th0 by simp


545 
next


546 
case (insert z T a c)


547 
let ?F = "\<lambda>T. {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"


548 
let ?h = "\<lambda>(y,g) i. if i = z then y else g i"


549 
let ?k = "\<lambda>h. (h(z),(\<lambda>i. if i = z then i else h i))"


550 
let ?s = "\<lambda> k a c f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)"


551 
let ?c = "\<lambda>i. if i = z then a i j else c i"


552 
have thif: "\<And>a b c d. (if a \<or> b then c else d) = (if a then c else if b then c else d)" by simp


553 
have thif2: "\<And>a b c d e. (if a then b else if c then d else e) =


554 
(if c then (if a then b else d) else (if a then b else e))" by simp


555 
from `z \<notin> T` have nz: "\<And>i. i \<in> T \<Longrightarrow> i = z \<longleftrightarrow> False" by auto


556 
have "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) =


557 
det (\<chi> i. if i = z then setsum (a i) S


558 
else if i \<in> T then setsum (a i) S else c i)"


559 
unfolding insert_iff thif ..


560 
also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<in> T then setsum (a i) S


561 
else if i = z then a i j else c i))"


562 
unfolding det_linear_row_setsum[OF fS]


563 
apply (subst thif2)


564 
using nz by (simp cong del: if_weak_cong cong add: if_cong)


565 
finally have tha:


566 
"det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) =


567 
(\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i)


568 
else if i = z then a i j


569 
else c i))"


570 
unfolding insert.hyps unfolding setsum_cartesian_product by blast


571 
show ?case unfolding tha


572 
apply(rule setsum_eq_general_reverses[where h= "?h" and k= "?k"],


573 
blast intro: finite_cartesian_product fS finite,


574 
blast intro: finite_cartesian_product fS finite)


575 
using `z \<notin> T`


576 
apply (auto intro: ext)


577 
apply (rule cong[OF refl[of det]])


578 
by vector


579 
qed


580 


581 
lemma det_linear_rows_setsum:


582 
assumes fS: "finite (S::'n::finite set)"


583 
shows "det (\<chi> i. setsum (a i) S) = setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n::finite)) {f. \<forall>i. f i \<in> S}"


584 
proof


585 
have th0: "\<And>x y. ((\<chi> i. if i \<in> (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\<chi> i. x i)" by vector


586 


587 
from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] show ?thesis by simp


588 
qed


589 


590 
lemma matrix_mul_setsum_alt:


591 
fixes A B :: "'a::comm_ring_1^'n^'n::finite"


592 
shows "A ** B = (\<chi> i. setsum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))"


593 
by (vector matrix_matrix_mult_def setsum_component)


594 


595 
lemma det_rows_mul:


596 
"det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n::finite) =


597 
setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"


598 
proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2)


599 
let ?U = "UNIV :: 'n set"


600 
let ?PU = "{p. p permutes ?U}"


601 
fix p assume pU: "p \<in> ?PU"


602 
let ?s = "of_int (sign p)"


603 
from pU have p: "p permutes ?U" by blast


604 
have "setprod (\<lambda>i. c i * a i $ p i) ?U = setprod c ?U * setprod (\<lambda>i. a i $ p i) ?U"


605 
unfolding setprod_timesf ..


606 
then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) =


607 
setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" by (simp add: ring_simps)


608 
qed


609 


610 
lemma det_mul:


611 
fixes A B :: "'a::ordered_idom^'n^'n::finite"


612 
shows "det (A ** B) = det A * det B"


613 
proof


614 
let ?U = "UNIV :: 'n set"


615 
let ?F = "{f. (\<forall>i\<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}"


616 
let ?PU = "{p. p permutes ?U}"


617 
have fU: "finite ?U" by simp


618 
have fF: "finite ?F" by (rule finite)


619 
{fix p assume p: "p permutes ?U"


620 


621 
have "p \<in> ?F" unfolding mem_Collect_eq permutes_in_image[OF p]


622 
using p[unfolded permutes_def] by simp}


623 
then have PUF: "?PU \<subseteq> ?F" by blast


624 
{fix f assume fPU: "f \<in> ?F  ?PU"


625 
have fUU: "f ` ?U \<subseteq> ?U" using fPU by auto


626 
from fPU have f: "\<forall>i \<in> ?U. f i \<in> ?U"


627 
"\<forall>i. i \<notin> ?U \<longrightarrow> f i = i" "\<not>(\<forall>y. \<exists>!x. f x = y)" unfolding permutes_def


628 
by auto


629 


630 
let ?A = "(\<chi> i. A$i$f i *s B$f i) :: 'a^'n^'n"


631 
let ?B = "(\<chi> i. B$f i) :: 'a^'n^'n"


632 
{assume fni: "\<not> inj_on f ?U"


633 
then obtain i j where ij: "f i = f j" "i \<noteq> j"


634 
unfolding inj_on_def by blast


635 
from ij


636 
have rth: "row i ?B = row j ?B" by (vector row_def)


637 
from det_identical_rows[OF ij(2) rth]


638 
have "det (\<chi> i. A$i$f i *s B$f i) = 0"


639 
unfolding det_rows_mul by simp}


640 
moreover


641 
{assume fi: "inj_on f ?U"


642 
from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j"


643 
unfolding inj_on_def by metis


644 
note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]]


645 


646 
{fix y


647 
from fs f have "\<exists>x. f x = y" by blast


648 
then obtain x where x: "f x = y" by blast


649 
{fix z assume z: "f z = y" from fith x z have "z = x" by metis}


650 
with x have "\<exists>!x. f x = y" by blast}


651 
with f(3) have "det (\<chi> i. A$i$f i *s B$f i) = 0" by blast}


652 
ultimately have "det (\<chi> i. A$i$f i *s B$f i) = 0" by blast}


653 
hence zth: "\<forall> f\<in> ?F  ?PU. det (\<chi> i. A$i$f i *s B$f i) = 0" by simp


654 
{fix p assume pU: "p \<in> ?PU"


655 
from pU have p: "p permutes ?U" by blast


656 
let ?s = "\<lambda>p. of_int (sign p)"


657 
let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) *


658 
(?s q * (\<Prod>i\<in> ?U. B $ i $ q i))"


659 
have "(setsum (\<lambda>q. ?s q *


660 
(\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) =


661 
(setsum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) *


662 
(?s q * (\<Prod>i\<in> ?U. B $ i $ q i))) ?PU)"


663 
unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f]


664 
proof(rule setsum_cong2)


665 
fix q assume qU: "q \<in> ?PU"


666 
hence q: "q permutes ?U" by blast


667 
from p q have pp: "permutation p" and pq: "permutation q"


668 
unfolding permutation_permutes by auto


669 
have th00: "of_int (sign p) * of_int (sign p) = (1::'a)"


670 
"\<And>a. of_int (sign p) * (of_int (sign p) * a) = a"


671 
unfolding mult_assoc[symmetric] unfolding of_int_mult[symmetric]


672 
by (simp_all add: sign_idempotent)


673 
have ths: "?s q = ?s p * ?s (q o inv p)"


674 
using pp pq permutation_inverse[OF pp] sign_inverse[OF pp]


675 
by (simp add: th00 mult_ac sign_idempotent sign_compose)


676 
have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) o p) ?U"


677 
by (rule setprod_permute[OF p])


678 
have thp: "setprod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U = setprod (\<lambda>i. A$i$p i) ?U * setprod (\<lambda>i. B$i$ q (inv p i)) ?U"


679 
unfolding th001 setprod_timesf[symmetric] o_def permutes_inverses[OF p]


680 
apply (rule setprod_cong[OF refl])


681 
using permutes_in_image[OF q] by vector


682 
show "?s q * setprod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = ?s p * (setprod (\<lambda>i. A$i$p i) ?U) * (?s (q o inv p) * setprod (\<lambda>i. B$i$(q o inv p) i) ?U)"


683 
using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp]


684 
by (simp add: sign_nz th00 ring_simps sign_idempotent sign_compose)


685 
qed


686 
}


687 
then have th2: "setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B"


688 
unfolding det_def setsum_product


689 
by (rule setsum_cong2)


690 
have "det (A**B) = setsum (\<lambda>f. det (\<chi> i. A $ i $ f i *s B $ f i)) ?F"


691 
unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] by simp


692 
also have "\<dots> = setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU"


693 
using setsum_mono_zero_cong_left[OF fF PUF zth, symmetric]


694 
unfolding det_rows_mul by auto


695 
finally show ?thesis unfolding th2 .


696 
qed


697 


698 
(*  *)


699 
(* Relation to invertibility. *)


700 
(*  *)


701 


702 
lemma invertible_left_inverse:


703 
fixes A :: "real^'n^'n::finite"


704 
shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). B** A = mat 1)"


705 
by (metis invertible_def matrix_left_right_inverse)


706 


707 
lemma invertible_righ_inverse:


708 
fixes A :: "real^'n^'n::finite"


709 
shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). A** B = mat 1)"


710 
by (metis invertible_def matrix_left_right_inverse)


711 


712 
lemma invertible_det_nz:


713 
fixes A::"real ^'n^'n::finite"


714 
shows "invertible A \<longleftrightarrow> det A \<noteq> 0"


715 
proof


716 
{assume "invertible A"


717 
then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1"


718 
unfolding invertible_righ_inverse by blast


719 
hence "det (A ** B) = det (mat 1 :: real ^'n^'n)" by simp


720 
hence "det A \<noteq> 0"


721 
apply (simp add: det_mul det_I) by algebra }


722 
moreover


723 
{assume H: "\<not> invertible A"


724 
let ?U = "UNIV :: 'n set"


725 
have fU: "finite ?U" by simp


726 
from H obtain c i where c: "setsum (\<lambda>i. c i *s row i A) ?U = 0"


727 
and iU: "i \<in> ?U" and ci: "c i \<noteq> 0"


728 
unfolding invertible_righ_inverse


729 
unfolding matrix_right_invertible_independent_rows by blast


730 
have stupid: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> a = b"


731 
apply (drule_tac f="op + ( a)" in cong[OF refl])


732 
apply (simp only: ab_left_minus add_assoc[symmetric])


733 
apply simp


734 
done


735 
from c ci


736 
have thr0: " row i A = setsum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U  {i})"


737 
unfolding setsum_diff1'[OF fU iU] setsum_cmul


738 
apply 


739 
apply (rule vector_mul_lcancel_imp[OF ci])


740 
apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps)


741 
unfolding stupid ..


742 
have thr: " row i A \<in> span {row j A j. j \<noteq> i}"


743 
unfolding thr0


744 
apply (rule span_setsum)


745 
apply simp


746 
apply (rule ballI)


747 
apply (rule span_mul)+


748 
apply (rule span_superset)


749 
apply auto


750 
done


751 
let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n"


752 
have thrb: "row i ?B = 0" using iU by (vector row_def)


753 
have "det A = 0"


754 
unfolding det_row_span[OF thr, symmetric] right_minus


755 
unfolding det_zero_row[OF thrb] ..}


756 
ultimately show ?thesis by blast


757 
qed


758 


759 
(*  *)


760 
(* Cramer's rule. *)


761 
(*  *)


762 


763 
lemma cramer_lemma_transp:


764 
fixes A:: "'a::ordered_idom^'n^'n::finite" and x :: "'a ^'n::finite"


765 
shows "det ((\<chi> i. if i = k then setsum (\<lambda>i. x$i *s row i A) (UNIV::'n set)


766 
else row i A)::'a^'n^'n) = x$k * det A"


767 
(is "?lhs = ?rhs")


768 
proof


769 
let ?U = "UNIV :: 'n set"


770 
let ?Uk = "?U  {k}"


771 
have U: "?U = insert k ?Uk" by blast


772 
have fUk: "finite ?Uk" by simp


773 
have kUk: "k \<notin> ?Uk" by simp


774 
have th00: "\<And>k s. x$k *s row k A + s = (x$k  1) *s row k A + row k A + s"


775 
by (vector ring_simps)


776 
have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by (auto intro: ext)


777 
have "(\<chi> i. row i A) = A" by (vector row_def)


778 
then have thd1: "det (\<chi> i. row i A) = det A" by simp


779 
have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A"


780 
apply (rule det_row_span)


781 
apply (rule span_setsum[OF fUk])


782 
apply (rule ballI)


783 
apply (rule span_mul)


784 
apply (rule span_superset)


785 
apply auto


786 
done


787 
show "?lhs = x$k * det A"


788 
apply (subst U)


789 
unfolding setsum_insert[OF fUk kUk]


790 
apply (subst th00)


791 
unfolding add_assoc


792 
apply (subst det_row_add)


793 
unfolding thd0


794 
unfolding det_row_mul


795 
unfolding th001[of k "\<lambda>i. row i A"]


796 
unfolding thd1 by (simp add: ring_simps)


797 
qed


798 


799 
lemma cramer_lemma:


800 
fixes A :: "'a::ordered_idom ^'n^'n::finite"


801 
shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A"


802 
proof


803 
let ?U = "UNIV :: 'n set"


804 
have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transp A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U"


805 
by (auto simp add: row_transp intro: setsum_cong2)


806 
show ?thesis unfolding matrix_mult_vsum


807 
unfolding cramer_lemma_transp[of k x "transp A", unfolded det_transp, symmetric]


808 
unfolding stupid[of "\<lambda>i. x$i"]


809 
apply (subst det_transp[symmetric])


810 
apply (rule cong[OF refl[of det]]) by (vector transp_def column_def row_def)


811 
qed


812 


813 
lemma cramer:


814 
fixes A ::"real^'n^'n::finite"


815 
assumes d0: "det A \<noteq> 0"


816 
shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)"


817 
proof


818 
from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"


819 
unfolding invertible_det_nz[symmetric] invertible_def by blast


820 
have "(A ** B) *v b = b" by (simp add: B matrix_vector_mul_lid)


821 
hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc)


822 
then have xe: "\<exists>x. A*v x = b" by blast


823 
{fix x assume x: "A *v x = b"


824 
have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)"


825 
unfolding x[symmetric]


826 
using d0 by (simp add: Cart_eq cramer_lemma field_simps)}


827 
with xe show ?thesis by auto


828 
qed


829 


830 
(*  *)


831 
(* Orthogonality of a transformation and matrix. *)


832 
(*  *)


833 


834 
definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"


835 


836 
lemma orthogonal_transformation: "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>(v::real ^_). norm (f v) = norm v)"


837 
unfolding orthogonal_transformation_def


838 
apply auto


839 
apply (erule_tac x=v in allE)+


840 
apply (simp add: real_vector_norm_def)


841 
by (simp add: dot_norm linear_add[symmetric])


842 


843 
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1"


844 


845 
lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n::finite) \<longleftrightarrow> transp Q ** Q = mat 1"


846 
by (metis matrix_left_right_inverse orthogonal_matrix_def)


847 


848 
lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n::finite)"


849 
by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid)


850 


851 
lemma orthogonal_matrix_mul:


852 
fixes A :: "real ^'n^'n::finite"


853 
assumes oA : "orthogonal_matrix A"


854 
and oB: "orthogonal_matrix B"


855 
shows "orthogonal_matrix(A ** B)"


856 
using oA oB


857 
unfolding orthogonal_matrix matrix_transp_mul


858 
apply (subst matrix_mul_assoc)


859 
apply (subst matrix_mul_assoc[symmetric])


860 
by (simp add: matrix_mul_rid)


861 


862 
lemma orthogonal_transformation_matrix:


863 
fixes f:: "real^'n \<Rightarrow> real^'n::finite"


864 
shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"


865 
(is "?lhs \<longleftrightarrow> ?rhs")


866 
proof


867 
let ?mf = "matrix f"


868 
let ?ot = "orthogonal_transformation f"


869 
let ?U = "UNIV :: 'n set"


870 
have fU: "finite ?U" by simp


871 
let ?m1 = "mat 1 :: real ^'n^'n"


872 
{assume ot: ?ot


873 
from ot have lf: "linear f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w"


874 
unfolding orthogonal_transformation_def orthogonal_matrix by blast+


875 
{fix i j


876 
let ?A = "transp ?mf ** ?mf"


877 
have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"


878 
"\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"


879 
by simp_all


880 
from fd[rule_format, of "basis i" "basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul]


881 
have "?A$i$j = ?m1 $ i $ j"


882 
by (simp add: dot_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def)}


883 
hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector


884 
with lf have ?rhs by blast}


885 
moreover


886 
{assume lf: "linear f" and om: "orthogonal_matrix ?mf"


887 
from lf om have ?lhs


888 
unfolding orthogonal_matrix_def norm_eq orthogonal_transformation


889 
unfolding matrix_works[OF lf, symmetric]


890 
apply (subst dot_matrix_vector_mul)


891 
by (simp add: dot_matrix_product matrix_mul_lid)}


892 
ultimately show ?thesis by blast


893 
qed


894 


895 
lemma det_orthogonal_matrix:


896 
fixes Q:: "'a::ordered_idom^'n^'n::finite"


897 
assumes oQ: "orthogonal_matrix Q"


898 
shows "det Q = 1 \<or> det Q =  1"


899 
proof


900 


901 
have th: "\<And>x::'a. x = 1 \<or> x =  1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x")


902 
proof


903 
fix x:: 'a


904 
have th0: "x*x  1 = (x  1)*(x + 1)" by (simp add: ring_simps)


905 
have th1: "\<And>(x::'a) y. x =  y \<longleftrightarrow> x + y = 0"


906 
apply (subst eq_iff_diff_eq_0) by simp


907 
have "x*x = 1 \<longleftrightarrow> x*x  1 = 0" by simp


908 
also have "\<dots> \<longleftrightarrow> x = 1 \<or> x =  1" unfolding th0 th1 by simp


909 
finally show "?ths x" ..


910 
qed


911 
from oQ have "Q ** transp Q = mat 1" by (metis orthogonal_matrix_def)


912 
hence "det (Q ** transp Q) = det (mat 1:: 'a^'n^'n)" by simp


913 
hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transp)


914 
then show ?thesis unfolding th .


915 
qed


916 


917 
(*  *)


918 
(* Linearity of scaling, and hence isometry, that preserves origin. *)


919 
(*  *)


920 
lemma scaling_linear:


921 
fixes f :: "real ^'n \<Rightarrow> real ^'n::finite"


922 
assumes f0: "f 0 = 0" and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"


923 
shows "linear f"


924 
proof


925 
{fix v w


926 
{fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] }


927 
note th0 = this


928 
have "f v \<bullet> f w = c^2 * (v \<bullet> w)"


929 
unfolding dot_norm_neg dist_norm[symmetric]


930 
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}


931 
note fc = this


932 
show ?thesis unfolding linear_def vector_eq


933 
by (simp add: dot_lmult dot_ladd dot_rmult dot_radd fc ring_simps)


934 
qed


935 


936 
lemma isometry_linear:


937 
"f (0:: real^'n) = (0:: real^'n::finite) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y


938 
\<Longrightarrow> linear f"


939 
by (rule scaling_linear[where c=1]) simp_all


940 


941 
(*  *)


942 
(* Hence another formulation of orthogonal transformation. *)


943 
(*  *)


944 


945 
lemma orthogonal_transformation_isometry:


946 
"orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n::finite) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"


947 
unfolding orthogonal_transformation


948 
apply (rule iffI)


949 
apply clarify


950 
apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_norm)


951 
apply (rule conjI)


952 
apply (rule isometry_linear)


953 
apply simp


954 
apply simp


955 
apply clarify


956 
apply (erule_tac x=v in allE)


957 
apply (erule_tac x=0 in allE)


958 
by (simp add: dist_norm)


959 


960 
(*  *)


961 
(* Can extend an isometry from unit sphere. *)


962 
(*  *)


963 


964 
lemma isometry_sphere_extend:


965 
fixes f:: "real ^'n \<Rightarrow> real ^'n::finite"


966 
assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1"


967 
and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y"


968 
shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"


969 
proof


970 
{fix x y x' y' x0 y0 x0' y0' :: "real ^'n"


971 
assume H: "x = norm x *s x0" "y = norm y *s y0"


972 
"x' = norm x *s x0'" "y' = norm y *s y0'"


973 
"norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1"


974 
"norm(x0'  y0') = norm(x0  y0)"


975 


976 
have "norm(x'  y') = norm(x  y)"


977 
apply (subst H(1))


978 
apply (subst H(2))


979 
apply (subst H(3))


980 
apply (subst H(4))


981 
using H(59)


982 
apply (simp add: norm_eq norm_eq_1)


983 
apply (simp add: dot_lsub dot_rsub dot_lmult dot_rmult)


984 
apply (simp add: ring_simps)


985 
by (simp only: right_distrib[symmetric])}


986 
note th0 = this


987 
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)"


988 
{fix x:: "real ^'n" assume nx: "norm x = 1"


989 
have "?g x = f x" using nx by auto}


990 
hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast


991 
have g0: "?g 0 = 0" by simp


992 
{fix x y :: "real ^'n"


993 
{assume "x = 0" "y = 0"


994 
then have "dist (?g x) (?g y) = dist x y" by simp }


995 
moreover


996 
{assume "x = 0" "y \<noteq> 0"


997 
then have "dist (?g x) (?g y) = dist x y"


998 
apply (simp add: dist_norm norm_mul)


999 
apply (rule f1[rule_format])


1000 
by(simp add: norm_mul field_simps)}


1001 
moreover


1002 
{assume "x \<noteq> 0" "y = 0"


1003 
then have "dist (?g x) (?g y) = dist x y"


1004 
apply (simp add: dist_norm norm_mul)


1005 
apply (rule f1[rule_format])


1006 
by(simp add: norm_mul field_simps)}


1007 
moreover


1008 
{assume z: "x \<noteq> 0" "y \<noteq> 0"


1009 
have th00: "x = norm x *s (inverse (norm x) *s x)" "y = norm y *s (inverse (norm y) *s y)" "norm x *s f ((inverse (norm x) *s x)) = norm x *s f (inverse (norm x) *s x)"


1010 
"norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)"


1011 
"norm (inverse (norm x) *s x) = 1"


1012 
"norm (f (inverse (norm x) *s x)) = 1"


1013 
"norm (inverse (norm y) *s y) = 1"


1014 
"norm (f (inverse (norm y) *s y)) = 1"


1015 
"norm (f (inverse (norm x) *s x)  f (inverse (norm y) *s y)) =


1016 
norm (inverse (norm x) *s x  inverse (norm y) *s y)"


1017 
using z


1018 
by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])


1019 
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"


1020 
by (simp add: dist_norm)}


1021 
ultimately have "dist (?g x) (?g y) = dist x y" by blast}


1022 
note thd = this


1023 
show ?thesis


1024 
apply (rule exI[where x= ?g])


1025 
unfolding orthogonal_transformation_isometry


1026 
using g0 thfg thd by metis


1027 
qed


1028 


1029 
(*  *)


1030 
(* Rotation, reflection, rotoinversion. *)


1031 
(*  *)


1032 


1033 
definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"


1034 
definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q =  1"


1035 


1036 
lemma orthogonal_rotation_or_rotoinversion:


1037 
fixes Q :: "'a::ordered_idom^'n^'n::finite"


1038 
shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"


1039 
by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)


1040 
(*  *)


1041 
(* Explicit formulas for low dimensions. *)


1042 
(*  *)


1043 


1044 
lemma setprod_1: "setprod f {(1::nat)..1} = f 1" by simp


1045 


1046 
lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2"


1047 
by (simp add: nat_number setprod_numseg mult_commute)


1048 
lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3"


1049 
by (simp add: nat_number setprod_numseg mult_commute)


1050 


1051 
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"


1052 
by (simp add: det_def permutes_sing sign_id UNIV_1)


1053 


1054 
lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2  A$1$2 * A$2$1"


1055 
proof


1056 
have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto


1057 
show ?thesis


1058 
unfolding det_def UNIV_2


1059 
unfolding setsum_over_permutations_insert[OF f12]


1060 
unfolding permutes_sing


1061 
apply (simp add: sign_swap_id sign_id swap_id_eq)


1062 
by (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31))


1063 
qed


1064 


1065 
lemma det_3: "det (A::'a::comm_ring_1^3^3) =


1066 
A$1$1 * A$2$2 * A$3$3 +


1067 
A$1$2 * A$2$3 * A$3$1 +


1068 
A$1$3 * A$2$1 * A$3$2 


1069 
A$1$1 * A$2$3 * A$3$2 


1070 
A$1$2 * A$2$1 * A$3$3 


1071 
A$1$3 * A$2$2 * A$3$1"


1072 
proof


1073 
have f123: "finite {2::3, 3}" "1 \<notin> {2::3, 3}" by auto


1074 
have f23: "finite {3::3}" "2 \<notin> {3::3}" by auto


1075 


1076 
show ?thesis


1077 
unfolding det_def UNIV_3


1078 
unfolding setsum_over_permutations_insert[OF f123]


1079 
unfolding setsum_over_permutations_insert[OF f23]


1080 


1081 
unfolding permutes_sing


1082 
apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)


1083 
apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31))


1084 
by (simp add: ring_simps)


1085 
qed


1086 


1087 
end
