src/HOL/Library/Determinants.thy
 author chaieb Mon Feb 09 17:21:46 2009 +0000 (2009-02-09) changeset 29847 af32126ee729 parent 29846 57dccccc37b3 child 30041 9becd197a40e permissions -rw-r--r--
 chaieb@29846 ` 1` ```(* Title: Determinants ``` chaieb@29846 ` 2` ``` ID: \$Id: ``` chaieb@29846 ` 3` ``` Author: Amine Chaieb, University of Cambridge ``` chaieb@29846 ` 4` ```*) ``` chaieb@29846 ` 5` chaieb@29846 ` 6` ```header {* Traces, Determinant of square matrices and some properties *} ``` chaieb@29846 ` 7` chaieb@29846 ` 8` ```theory Determinants ``` chaieb@29846 ` 9` ``` imports Euclidean_Space Permutations ``` chaieb@29846 ` 10` ```begin ``` chaieb@29846 ` 11` chaieb@29846 ` 12` ```subsection{* First some facts about products*} ``` chaieb@29846 ` 13` ```lemma setprod_insert_eq: "finite A \ setprod f (insert a A) = (if a \ A then setprod f A else f a * setprod f A)" ``` chaieb@29846 ` 14` ```apply clarsimp ``` chaieb@29846 ` 15` ```by(subgoal_tac "insert a A = A", auto) ``` chaieb@29846 ` 16` chaieb@29846 ` 17` ```lemma setprod_add_split: ``` chaieb@29846 ` 18` ``` assumes mn: "(m::nat) <= n + 1" ``` chaieb@29846 ` 19` ``` shows "setprod f {m.. n+p} = setprod f {m .. n} * setprod f {n+1..n+p}" ``` chaieb@29846 ` 20` ```proof- ``` chaieb@29846 ` 21` ``` let ?A = "{m .. n+p}" ``` chaieb@29846 ` 22` ``` let ?B = "{m .. n}" ``` chaieb@29846 ` 23` ``` let ?C = "{n+1..n+p}" ``` chaieb@29846 ` 24` ``` from mn have un: "?B \ ?C = ?A" by auto ``` chaieb@29846 ` 25` ``` from mn have dj: "?B \ ?C = {}" by auto ``` chaieb@29846 ` 26` ``` have f: "finite ?B" "finite ?C" by simp_all ``` chaieb@29846 ` 27` ``` from setprod_Un_disjoint[OF f dj, of f, unfolded un] show ?thesis . ``` chaieb@29846 ` 28` ```qed ``` chaieb@29846 ` 29` chaieb@29846 ` 30` chaieb@29846 ` 31` ```lemma setprod_offset: "setprod f {(m::nat) + p .. n + p} = setprod (\i. f (i + p)) {m..n}" ``` chaieb@29846 ` 32` ```apply (rule setprod_reindex_cong[where f="op + p"]) ``` chaieb@29846 ` 33` ```apply (auto simp add: image_iff Bex_def inj_on_def) ``` chaieb@29846 ` 34` ```apply arith ``` chaieb@29846 ` 35` ```apply (rule ext) ``` chaieb@29846 ` 36` ```apply (simp add: add_commute) ``` chaieb@29846 ` 37` ```done ``` chaieb@29846 ` 38` chaieb@29846 ` 39` ```lemma setprod_singleton: "setprod f {x} = f x" by simp ``` chaieb@29846 ` 40` chaieb@29846 ` 41` ```lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" by simp ``` chaieb@29846 ` 42` chaieb@29846 ` 43` ```lemma setprod_numseg: "setprod f {m..0} = (if m=0 then f 0 else 1)" ``` chaieb@29846 ` 44` ``` "setprod f {m .. Suc n} = (if m \ Suc n then f (Suc n) * setprod f {m..n} ``` chaieb@29846 ` 45` ``` else setprod f {m..n})" ``` chaieb@29846 ` 46` ``` by (auto simp add: atLeastAtMostSuc_conv) ``` chaieb@29846 ` 47` chaieb@29846 ` 48` ```lemma setprod_le: assumes fS: "finite S" and fg: "\x\S. f x \ 0 \ f x \ (g x :: 'a::ordered_idom)" ``` chaieb@29846 ` 49` ``` shows "setprod f S \ setprod g S" ``` chaieb@29846 ` 50` ```using fS fg ``` chaieb@29846 ` 51` ```apply(induct S) ``` chaieb@29846 ` 52` ```apply simp ``` chaieb@29846 ` 53` ```apply auto ``` chaieb@29846 ` 54` ```apply (rule mult_mono) ``` chaieb@29846 ` 55` ```apply (auto intro: setprod_nonneg) ``` chaieb@29846 ` 56` ```done ``` chaieb@29846 ` 57` chaieb@29846 ` 58` ``` (* FIXME: In Finite_Set there is a useless further assumption *) ``` chaieb@29846 ` 59` ```lemma setprod_inversef: "finite A ==> setprod (inverse \ f) A = (inverse (setprod f A) :: 'a:: {division_by_zero, field})" ``` chaieb@29846 ` 60` ``` apply (erule finite_induct) ``` chaieb@29846 ` 61` ``` apply (simp) ``` chaieb@29846 ` 62` ``` apply simp ``` chaieb@29846 ` 63` ``` done ``` chaieb@29846 ` 64` chaieb@29846 ` 65` ```lemma setprod_le_1: assumes fS: "finite S" and f: "\x\S. f x \ 0 \ f x \ (1::'a::ordered_idom)" ``` chaieb@29846 ` 66` ``` shows "setprod f S \ 1" ``` chaieb@29846 ` 67` ```using setprod_le[OF fS f] unfolding setprod_1 . ``` chaieb@29846 ` 68` chaieb@29846 ` 69` ```subsection{* Trace *} ``` chaieb@29846 ` 70` chaieb@29846 ` 71` ```definition trace :: "'a::semiring_1^'n^'n \ 'a" where ``` chaieb@29846 ` 72` ``` "trace A = setsum (\i. ((A\$i)\$i)) {1..dimindex(UNIV::'n set)}" ``` chaieb@29846 ` 73` chaieb@29846 ` 74` ```lemma trace_0: "trace(mat 0) = 0" ``` chaieb@29846 ` 75` ``` by (simp add: trace_def mat_def Cart_lambda_beta setsum_0) ``` chaieb@29846 ` 76` chaieb@29846 ` 77` ```lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(dimindex(UNIV::'n set))" ``` chaieb@29846 ` 78` ``` by (simp add: trace_def mat_def Cart_lambda_beta) ``` chaieb@29846 ` 79` chaieb@29846 ` 80` ```lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" ``` chaieb@29846 ` 81` ``` by (simp add: trace_def setsum_addf Cart_lambda_beta vector_component) ``` chaieb@29846 ` 82` chaieb@29846 ` 83` ```lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" ``` chaieb@29846 ` 84` ``` by (simp add: trace_def setsum_subtractf Cart_lambda_beta vector_component) ``` chaieb@29846 ` 85` chaieb@29846 ` 86` ```lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)" ``` chaieb@29846 ` 87` ``` apply (simp add: trace_def matrix_matrix_mult_def Cart_lambda_beta) ``` chaieb@29846 ` 88` ``` apply (subst setsum_commute) ``` chaieb@29846 ` 89` ``` by (simp add: mult_commute) ``` chaieb@29846 ` 90` chaieb@29846 ` 91` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 92` ```(* Definition of determinant. *) ``` chaieb@29846 ` 93` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 94` chaieb@29846 ` 95` ```definition det:: "'a::comm_ring_1^'n^'n \ 'a" where ``` chaieb@29846 ` 96` ``` "det A = setsum (\p. of_int (sign p) * setprod (\i. A\$i\$p i) {1 .. dimindex(UNIV :: 'n set)}) {p. p permutes {1 .. dimindex(UNIV :: 'n set)}}" ``` chaieb@29846 ` 97` chaieb@29846 ` 98` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 99` ```(* A few general lemmas we need below. *) ``` chaieb@29846 ` 100` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 101` chaieb@29846 ` 102` ```lemma Cart_lambda_beta_perm: assumes p: "p permutes {1..dimindex(UNIV::'n set)}" ``` chaieb@29846 ` 103` ``` and i: "i \ {1..dimindex(UNIV::'n set)}" ``` chaieb@29846 ` 104` ``` shows "Cart_nth (Cart_lambda g ::'a^'n) (p i) = g(p i)" ``` chaieb@29846 ` 105` ``` using permutes_in_image[OF p] i ``` chaieb@29846 ` 106` ``` by (simp add: Cart_lambda_beta permutes_in_image[OF p]) ``` chaieb@29846 ` 107` chaieb@29846 ` 108` ```lemma setprod_permute: ``` chaieb@29846 ` 109` ``` assumes p: "p permutes S" ``` chaieb@29846 ` 110` ``` shows "setprod f S = setprod (f o p) S" ``` chaieb@29846 ` 111` ```proof- ``` chaieb@29846 ` 112` ``` {assume "\ finite S" hence ?thesis by simp} ``` chaieb@29846 ` 113` ``` moreover ``` chaieb@29846 ` 114` ``` {assume fS: "finite S" ``` chaieb@29846 ` 115` ``` then have ?thesis ``` chaieb@29846 ` 116` ``` apply (simp add: setprod_def) ``` chaieb@29846 ` 117` ``` apply (rule ab_semigroup_mult.fold_image_permute) ``` chaieb@29846 ` 118` ``` apply (auto simp add: p) ``` chaieb@29846 ` 119` ``` apply unfold_locales ``` chaieb@29846 ` 120` ``` done} ``` chaieb@29846 ` 121` ``` ultimately show ?thesis by blast ``` chaieb@29846 ` 122` ```qed ``` chaieb@29846 ` 123` chaieb@29846 ` 124` ```lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}" ``` chaieb@29846 ` 125` ``` by (auto intro: setprod_permute) ``` chaieb@29846 ` 126` chaieb@29846 ` 127` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 128` ```(* Basic determinant properties. *) ``` chaieb@29846 ` 129` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 130` chaieb@29846 ` 131` ```lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n)" ``` chaieb@29846 ` 132` ```proof- ``` chaieb@29846 ` 133` ``` let ?di = "\A i j. A\$i\$j" ``` chaieb@29846 ` 134` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 135` ``` have fU: "finite ?U" by blast ``` chaieb@29846 ` 136` ``` {fix p assume p: "p \ {p. p permutes ?U}" ``` chaieb@29846 ` 137` ``` from p have pU: "p permutes ?U" by blast ``` chaieb@29846 ` 138` ``` have sth: "sign (inv p) = sign p" ``` chaieb@29846 ` 139` ``` by (metis sign_inverse fU p mem_def Collect_def permutation_permutes) ``` chaieb@29846 ` 140` ``` from permutes_inj[OF pU] ``` chaieb@29846 ` 141` ``` have pi: "inj_on p ?U" by (blast intro: subset_inj_on) ``` chaieb@29846 ` 142` ``` from permutes_image[OF pU] ``` chaieb@29846 ` 143` ``` have "setprod (\i. ?di (transp A) i (inv p i)) ?U = setprod (\i. ?di (transp A) i (inv p i)) (p ` ?U)" by simp ``` chaieb@29846 ` 144` ``` also have "\ = setprod ((\i. ?di (transp A) i (inv p i)) o p) ?U" ``` chaieb@29846 ` 145` ``` unfolding setprod_reindex[OF pi] .. ``` chaieb@29846 ` 146` ``` also have "\ = setprod (\i. ?di A i (p i)) ?U" ``` chaieb@29846 ` 147` ``` proof- ``` chaieb@29846 ` 148` ``` {fix i assume i: "i \ ?U" ``` chaieb@29846 ` 149` ``` from i permutes_inv_o[OF pU] permutes_in_image[OF pU] ``` chaieb@29846 ` 150` ``` have "((\i. ?di (transp A) i (inv p i)) o p) i = ?di A i (p i)" ``` chaieb@29846 ` 151` ``` unfolding transp_def by (simp add: Cart_lambda_beta expand_fun_eq)} ``` chaieb@29846 ` 152` ``` then show "setprod ((\i. ?di (transp A) i (inv p i)) o p) ?U = setprod (\i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) ``` chaieb@29846 ` 153` ``` qed ``` chaieb@29846 ` 154` ``` finally have "of_int (sign (inv p)) * (setprod (\i. ?di (transp A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\i. ?di A i (p i)) ?U)" using sth ``` chaieb@29846 ` 155` ``` by simp} ``` chaieb@29846 ` 156` ``` then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse) ``` chaieb@29846 ` 157` ``` apply (rule setsum_cong2) by blast ``` chaieb@29846 ` 158` ```qed ``` chaieb@29846 ` 159` chaieb@29846 ` 160` ```lemma det_lowerdiagonal: ``` chaieb@29846 ` 161` ``` fixes A :: "'a::comm_ring_1^'n^'n" ``` chaieb@29846 ` 162` ``` assumes ld: "\i j. i \ {1 .. dimindex (UNIV:: 'n set)} \ j \ {1 .. dimindex(UNIV:: 'n set)} \ i < j \ A\$i\$j = 0" ``` chaieb@29846 ` 163` ``` shows "det A = setprod (\i. A\$i\$i) {1..dimindex(UNIV:: 'n set)}" ``` chaieb@29846 ` 164` ```proof- ``` chaieb@29846 ` 165` ``` let ?U = "{1..dimindex(UNIV:: 'n set)}" ``` chaieb@29846 ` 166` ``` let ?PU = "{p. p permutes ?U}" ``` chaieb@29846 ` 167` ``` let ?pp = "\p. of_int (sign p) * setprod (\i. A\$i\$p i) {1 .. dimindex(UNIV :: 'n set)}" ``` chaieb@29846 ` 168` ``` have fU: "finite ?U" by blast ``` chaieb@29846 ` 169` ``` from finite_permutations[OF fU] have fPU: "finite ?PU" . ``` chaieb@29846 ` 170` ``` have id0: "{id} \ ?PU" by (auto simp add: permutes_id) ``` chaieb@29846 ` 171` ``` {fix p assume p: "p \ ?PU -{id}" ``` chaieb@29846 ` 172` ``` from p have pU: "p permutes ?U" and pid: "p \ id" by blast+ ``` chaieb@29846 ` 173` ``` from permutes_natset_le[OF pU] pid obtain i where ``` chaieb@29846 ` 174` ``` i: "i \ ?U" "p i > i" by (metis not_le) ``` chaieb@29846 ` 175` ``` from permutes_in_image[OF pU] i(1) have piU: "p i \ ?U" by blast ``` chaieb@29846 ` 176` ``` from ld[OF i(1) piU i(2)] i(1) have ex:"\i \ ?U. A\$i\$p i = 0" by blast ``` chaieb@29846 ` 177` ``` from setprod_zero[OF fU ex] have "?pp p = 0" by simp} ``` chaieb@29846 ` 178` ``` then have p0: "\p \ ?PU -{id}. ?pp p = 0" by blast ``` chaieb@29846 ` 179` ``` from setsum_superset[OF fPU id0 p0] show ?thesis ``` chaieb@29846 ` 180` ``` unfolding det_def by (simp add: sign_id) ``` chaieb@29846 ` 181` ```qed ``` chaieb@29846 ` 182` chaieb@29846 ` 183` ```lemma det_upperdiagonal: ``` chaieb@29846 ` 184` ``` fixes A :: "'a::comm_ring_1^'n^'n" ``` chaieb@29846 ` 185` ``` assumes ld: "\i j. i \ {1 .. dimindex (UNIV:: 'n set)} \ j \ {1 .. dimindex(UNIV:: 'n set)} \ i > j \ A\$i\$j = 0" ``` chaieb@29846 ` 186` ``` shows "det A = setprod (\i. A\$i\$i) {1..dimindex(UNIV:: 'n set)}" ``` chaieb@29846 ` 187` ```proof- ``` chaieb@29846 ` 188` ``` let ?U = "{1..dimindex(UNIV:: 'n set)}" ``` chaieb@29846 ` 189` ``` let ?PU = "{p. p permutes ?U}" ``` chaieb@29846 ` 190` ``` let ?pp = "(\p. of_int (sign p) * setprod (\i. A\$i\$p i) {1 .. dimindex(UNIV :: 'n set)})" ``` chaieb@29846 ` 191` ``` have fU: "finite ?U" by blast ``` chaieb@29846 ` 192` ``` from finite_permutations[OF fU] have fPU: "finite ?PU" . ``` chaieb@29846 ` 193` ``` have id0: "{id} \ ?PU" by (auto simp add: permutes_id) ``` chaieb@29846 ` 194` ``` {fix p assume p: "p \ ?PU -{id}" ``` chaieb@29846 ` 195` ``` from p have pU: "p permutes ?U" and pid: "p \ id" by blast+ ``` chaieb@29846 ` 196` ``` from permutes_natset_ge[OF pU] pid obtain i where ``` chaieb@29846 ` 197` ``` i: "i \ ?U" "p i < i" by (metis not_le) ``` chaieb@29846 ` 198` ``` from permutes_in_image[OF pU] i(1) have piU: "p i \ ?U" by blast ``` chaieb@29846 ` 199` ``` from ld[OF i(1) piU i(2)] i(1) have ex:"\i \ ?U. A\$i\$p i = 0" by blast ``` chaieb@29846 ` 200` ``` from setprod_zero[OF fU ex] have "?pp p = 0" by simp} ``` chaieb@29846 ` 201` ``` then have p0: "\p \ ?PU -{id}. ?pp p = 0" by blast ``` chaieb@29846 ` 202` ``` from setsum_superset[OF fPU id0 p0] show ?thesis ``` chaieb@29846 ` 203` ``` unfolding det_def by (simp add: sign_id) ``` chaieb@29846 ` 204` ```qed ``` chaieb@29846 ` 205` chaieb@29846 ` 206` ```lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" ``` chaieb@29846 ` 207` ```proof- ``` chaieb@29846 ` 208` ``` let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n" ``` chaieb@29846 ` 209` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 210` ``` let ?f = "\i j. ?A\$i\$j" ``` chaieb@29846 ` 211` ``` {fix i assume i: "i \ ?U" ``` chaieb@29846 ` 212` ``` have "?f i i = 1" using i by (vector mat_def)} ``` chaieb@29846 ` 213` ``` hence th: "setprod (\i. ?f i i) ?U = setprod (\x. 1) ?U" ``` chaieb@29846 ` 214` ``` by (auto intro: setprod_cong) ``` chaieb@29846 ` 215` ``` {fix i j assume i: "i \ ?U" and j: "j \ ?U" and ij: "i < j" ``` chaieb@29846 ` 216` ``` have "?f i j = 0" using i j ij by (vector mat_def) } ``` chaieb@29846 ` 217` ``` then have "det ?A = setprod (\i. ?f i i) ?U" using det_lowerdiagonal ``` chaieb@29846 ` 218` ``` by blast ``` chaieb@29846 ` 219` ``` also have "\ = 1" unfolding th setprod_1 .. ``` chaieb@29846 ` 220` ``` finally show ?thesis . ``` chaieb@29846 ` 221` ```qed ``` chaieb@29846 ` 222` chaieb@29846 ` 223` ```lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" ``` chaieb@29846 ` 224` ```proof- ``` chaieb@29846 ` 225` ``` let ?A = "mat 0 :: 'a::comm_ring_1^'n^'n" ``` chaieb@29846 ` 226` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 227` ``` let ?f = "\i j. ?A\$i\$j" ``` chaieb@29846 ` 228` ``` have th:"setprod (\i. ?f i i) ?U = 0" ``` chaieb@29846 ` 229` ``` apply (rule setprod_zero) ``` chaieb@29846 ` 230` ``` apply simp ``` chaieb@29846 ` 231` ``` apply (rule bexI[where x=1]) ``` chaieb@29846 ` 232` ``` using dimindex_ge_1[of "UNIV :: 'n set"] ``` chaieb@29846 ` 233` ``` by (simp_all add: mat_def Cart_lambda_beta) ``` chaieb@29846 ` 234` ``` {fix i j assume i: "i \ ?U" and j: "j \ ?U" and ij: "i < j" ``` chaieb@29846 ` 235` ``` have "?f i j = 0" using i j ij by (vector mat_def) } ``` chaieb@29846 ` 236` ``` then have "det ?A = setprod (\i. ?f i i) ?U" using det_lowerdiagonal ``` chaieb@29846 ` 237` ``` by blast ``` chaieb@29846 ` 238` ``` also have "\ = 0" unfolding th .. ``` chaieb@29846 ` 239` ``` finally show ?thesis . ``` chaieb@29846 ` 240` ```qed ``` chaieb@29846 ` 241` chaieb@29846 ` 242` ```lemma det_permute_rows: ``` chaieb@29846 ` 243` ``` fixes A :: "'a::comm_ring_1^'n^'n" ``` chaieb@29846 ` 244` ``` assumes p: "p permutes {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 245` ``` shows "det(\ i. A\$p i :: 'a^'n^'n) = of_int (sign p) * det A" ``` chaieb@29846 ` 246` ``` apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric] del: One_nat_def) ``` chaieb@29846 ` 247` ``` apply (subst sum_permutations_compose_right[OF p]) ``` chaieb@29846 ` 248` ```proof(rule setsum_cong2) ``` chaieb@29846 ` 249` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 250` ``` let ?PU = "{p. p permutes ?U}" ``` chaieb@29846 ` 251` ``` let ?Ap = "(\ i. A\$p i :: 'a^'n^'n)" ``` chaieb@29846 ` 252` ``` fix q assume qPU: "q \ ?PU" ``` chaieb@29846 ` 253` ``` have fU: "finite ?U" by blast ``` chaieb@29846 ` 254` ``` from qPU have q: "q permutes ?U" by blast ``` chaieb@29846 ` 255` ``` from p q have pp: "permutation p" and qp: "permutation q" ``` chaieb@29846 ` 256` ``` by (metis fU permutation_permutes)+ ``` chaieb@29846 ` 257` ``` from permutes_inv[OF p] have ip: "inv p permutes ?U" . ``` chaieb@29846 ` 258` ``` {fix i assume i: "i \ ?U" ``` chaieb@29846 ` 259` ``` from Cart_lambda_beta[rule_format, OF i, of "\i. A\$ p i"] ``` chaieb@29846 ` 260` ``` have "?Ap\$i\$ (q o p) i = A \$ p i \$ (q o p) i " by simp} ``` chaieb@29846 ` 261` ``` hence "setprod (\i. ?Ap\$i\$ (q o p) i) ?U = setprod (\i. A\$p i\$(q o p) i) ?U" ``` chaieb@29846 ` 262` ``` by (auto intro: setprod_cong) ``` chaieb@29846 ` 263` ``` also have "\ = setprod ((\i. A\$p i\$(q o p) i) o inv p) ?U" ``` chaieb@29846 ` 264` ``` by (simp only: setprod_permute[OF ip, symmetric]) ``` chaieb@29846 ` 265` ``` also have "\ = setprod (\i. A \$ (p o inv p) i \$ (q o (p o inv p)) i) ?U" ``` chaieb@29846 ` 266` ``` by (simp only: o_def) ``` chaieb@29846 ` 267` ``` also have "\ = setprod (\i. A\$i\$q i) ?U" by (simp only: o_def permutes_inverses[OF p]) ``` chaieb@29846 ` 268` ``` finally have thp: "setprod (\i. ?Ap\$i\$ (q o p) i) ?U = setprod (\i. A\$i\$q i) ?U" ``` chaieb@29846 ` 269` ``` by blast ``` chaieb@29846 ` 270` ``` show "of_int (sign (q o p)) * setprod (\i. ?Ap\$i\$ (q o p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\i. A\$i\$q i) ?U" ``` chaieb@29846 ` 271` ``` by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult) ``` chaieb@29846 ` 272` ```qed ``` chaieb@29846 ` 273` chaieb@29846 ` 274` ```lemma det_permute_columns: ``` chaieb@29846 ` 275` ``` fixes A :: "'a::comm_ring_1^'n^'n" ``` chaieb@29846 ` 276` ``` assumes p: "p permutes {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 277` ``` shows "det(\ i j. A\$i\$ p j :: 'a^'n^'n) = of_int (sign p) * det A" ``` chaieb@29846 ` 278` ```proof- ``` chaieb@29846 ` 279` ``` let ?Ap = "\ i j. A\$i\$ p j :: 'a^'n^'n" ``` chaieb@29846 ` 280` ``` let ?At = "transp A" ``` chaieb@29846 ` 281` ``` have "of_int (sign p) * det A = det (transp (\ i. transp A \$ p i))" ``` chaieb@29846 ` 282` ``` unfolding det_permute_rows[OF p, of ?At] det_transp .. ``` chaieb@29846 ` 283` ``` moreover ``` chaieb@29846 ` 284` ``` have "?Ap = transp (\ i. transp A \$ p i)" ``` chaieb@29846 ` 285` ``` by (simp add: transp_def Cart_eq Cart_lambda_beta Cart_lambda_beta_perm[OF p]) ``` chaieb@29846 ` 286` ``` ultimately show ?thesis by simp ``` chaieb@29846 ` 287` ```qed ``` chaieb@29846 ` 288` chaieb@29846 ` 289` ```lemma det_identical_rows: ``` chaieb@29846 ` 290` ``` fixes A :: "'a::ordered_idom^'n^'n" ``` chaieb@29846 ` 291` ``` assumes i: "i\{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 292` ``` and j: "j\{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 293` ``` and ij: "i \ j" ``` chaieb@29846 ` 294` ``` and r: "row i A = row j A" ``` chaieb@29846 ` 295` ``` shows "det A = 0" ``` chaieb@29846 ` 296` ```proof- ``` chaieb@29846 ` 297` ``` have tha: "\(a::'a) b. a = b ==> b = - a ==> a = 0" ``` chaieb@29846 ` 298` ``` by simp ``` chaieb@29846 ` 299` ``` have th1: "of_int (-1) = - 1" by (metis of_int_1 of_int_minus number_of_Min) ``` chaieb@29846 ` 300` ``` let ?p = "Fun.swap i j id" ``` chaieb@29846 ` 301` ``` let ?A = "\ i. A \$ ?p i" ``` chaieb@29846 ` 302` ``` from r have "A = ?A" by (simp add: Cart_eq Cart_lambda_beta Cart_lambda_beta_perm[OF permutes_swap_id[OF i j]] row_def swap_def) ``` chaieb@29846 ` 303` ``` hence "det A = det ?A" by simp ``` chaieb@29846 ` 304` ``` moreover have "det A = - det ?A" ``` chaieb@29846 ` 305` ``` by (simp add: det_permute_rows[OF permutes_swap_id[OF i j]] sign_swap_id ij th1) ``` chaieb@29846 ` 306` ``` ultimately show "det A = 0" by (metis tha) ``` chaieb@29846 ` 307` ```qed ``` chaieb@29846 ` 308` chaieb@29846 ` 309` ```lemma det_identical_columns: ``` chaieb@29846 ` 310` ``` fixes A :: "'a::ordered_idom^'n^'n" ``` chaieb@29846 ` 311` ``` assumes i: "i\{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 312` ``` and j: "j\{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 313` ``` and ij: "i \ j" ``` chaieb@29846 ` 314` ``` and r: "column i A = column j A" ``` chaieb@29846 ` 315` ``` shows "det A = 0" ``` chaieb@29846 ` 316` ```apply (subst det_transp[symmetric]) ``` chaieb@29846 ` 317` ```apply (rule det_identical_rows[OF i j ij]) ``` chaieb@29846 ` 318` ```by (metis row_transp i j r) ``` chaieb@29846 ` 319` chaieb@29846 ` 320` ```lemma det_zero_row: ``` chaieb@29846 ` 321` ``` fixes A :: "'a::{idom, ring_char_0}^'n^'n" ``` chaieb@29846 ` 322` ``` assumes i: "i\{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 323` ``` and r: "row i A = 0" ``` chaieb@29846 ` 324` ``` shows "det A = 0" ``` chaieb@29846 ` 325` ```using i r ``` chaieb@29846 ` 326` ```apply (simp add: row_def det_def Cart_lambda_beta Cart_eq vector_component del: One_nat_def) ``` chaieb@29846 ` 327` ```apply (rule setsum_0') ``` chaieb@29846 ` 328` ```apply (clarsimp simp add: sign_nz simp del: One_nat_def) ``` chaieb@29846 ` 329` ```apply (rule setprod_zero) ``` chaieb@29846 ` 330` ```apply simp ``` chaieb@29846 ` 331` ```apply (rule bexI[where x=i]) ``` chaieb@29846 ` 332` ```apply (erule_tac x="a i" in ballE) ``` chaieb@29846 ` 333` ```apply (subgoal_tac "(0\'a ^ 'n) \$ a i = 0") ``` chaieb@29846 ` 334` ```apply simp ``` chaieb@29846 ` 335` ```apply (rule zero_index) ``` chaieb@29846 ` 336` ```apply (drule permutes_in_image[of _ _ i]) ``` chaieb@29846 ` 337` ```apply simp ``` chaieb@29846 ` 338` ```apply (drule permutes_in_image[of _ _ i]) ``` chaieb@29846 ` 339` ```apply simp ``` chaieb@29846 ` 340` ```apply simp ``` chaieb@29846 ` 341` ```done ``` chaieb@29846 ` 342` chaieb@29846 ` 343` ```lemma det_zero_column: ``` chaieb@29846 ` 344` ``` fixes A :: "'a::{idom,ring_char_0}^'n^'n" ``` chaieb@29846 ` 345` ``` assumes i: "i\{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 346` ``` and r: "column i A = 0" ``` chaieb@29846 ` 347` ``` shows "det A = 0" ``` chaieb@29846 ` 348` ``` apply (subst det_transp[symmetric]) ``` chaieb@29846 ` 349` ``` apply (rule det_zero_row[OF i]) ``` chaieb@29846 ` 350` ``` by (metis row_transp r i) ``` chaieb@29846 ` 351` chaieb@29846 ` 352` ```lemma setsum_lambda_beta[simp]: "setsum (\i. ((\ i. g i) :: 'a::{comm_monoid_add}^'n) \$ i ) {1 .. dimindex (UNIV :: 'n set)} = setsum g {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 353` ``` by (simp add: Cart_lambda_beta) ``` chaieb@29846 ` 354` chaieb@29846 ` 355` ```lemma setprod_lambda_beta[simp]: "setprod (\i. ((\ i. g i) :: 'a::{comm_monoid_mult}^'n) \$ i ) {1 .. dimindex (UNIV :: 'n set)} = setprod g {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 356` ``` apply (rule setprod_cong) ``` chaieb@29846 ` 357` ``` apply simp ``` chaieb@29846 ` 358` ``` apply (simp add: Cart_lambda_beta') ``` chaieb@29846 ` 359` ``` done ``` chaieb@29846 ` 360` chaieb@29846 ` 361` ```lemma setprod_lambda_beta2[simp]: "setprod (\i. ((\ i. g i) :: 'a::{comm_monoid_mult}^'n^'n) \$ i\$ f i ) {1 .. dimindex (UNIV :: 'n set)} = setprod (\i. g i \$ f i) {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 362` ```proof(rule setprod_cong[OF refl]) ``` chaieb@29846 ` 363` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 364` ``` fix i assume i: "i \ ?U" ``` chaieb@29846 ` 365` ``` from Cart_lambda_beta'[OF i, of g] have ``` chaieb@29846 ` 366` ``` "((\ i. g i) :: 'a^'n^'n) \$ i = g i" . ``` chaieb@29846 ` 367` ``` hence "((\ i. g i) :: 'a^'n^'n) \$ i \$ f i = g i \$ f i" by simp ``` chaieb@29846 ` 368` ``` then ``` chaieb@29846 ` 369` ``` show "((\ i. g i):: 'a^'n^'n) \$ i \$ f i = g i \$ f i" . ``` chaieb@29846 ` 370` ```qed ``` chaieb@29846 ` 371` chaieb@29846 ` 372` ```lemma det_row_add: ``` chaieb@29846 ` 373` ``` assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 374` ``` shows "det((\ i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = ``` chaieb@29846 ` 375` ``` det((\ i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + ``` chaieb@29846 ` 376` ``` det((\ i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" ``` chaieb@29846 ` 377` ```unfolding det_def setprod_lambda_beta2 setsum_addf[symmetric] ``` chaieb@29846 ` 378` ```proof (rule setsum_cong2) ``` chaieb@29846 ` 379` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 380` ``` let ?pU = "{p. p permutes ?U}" ``` chaieb@29846 ` 381` ``` let ?f = "(\i. if i = k then a i + b i else c i)::nat \ 'a::comm_ring_1^'n" ``` chaieb@29846 ` 382` ``` let ?g = "(\ i. if i = k then a i else c i)::nat \ 'a::comm_ring_1^'n" ``` chaieb@29846 ` 383` ``` let ?h = "(\ i. if i = k then b i else c i)::nat \ 'a::comm_ring_1^'n" ``` chaieb@29846 ` 384` ``` fix p assume p: "p \ ?pU" ``` chaieb@29846 ` 385` ``` let ?Uk = "?U - {k}" ``` chaieb@29846 ` 386` ``` from p have pU: "p permutes ?U" by blast ``` chaieb@29846 ` 387` ``` from k have pkU: "p k \ ?U" by (simp only: permutes_in_image[OF pU]) ``` chaieb@29846 ` 388` ``` note pin[simp] = permutes_in_image[OF pU] ``` chaieb@29846 ` 389` ``` have kU: "?U = insert k ?Uk" using k by blast ``` chaieb@29846 ` 390` ``` {fix j assume j: "j \ ?Uk" ``` chaieb@29846 ` 391` ``` from j have "?f j \$ p j = ?g j \$ p j" and "?f j \$ p j= ?h j \$ p j" ``` chaieb@29846 ` 392` ``` by simp_all} ``` chaieb@29846 ` 393` ``` then have th1: "setprod (\i. ?f i \$ p i) ?Uk = setprod (\i. ?g i \$ p i) ?Uk" ``` chaieb@29846 ` 394` ``` and th2: "setprod (\i. ?f i \$ p i) ?Uk = setprod (\i. ?h i \$ p i) ?Uk" ``` chaieb@29846 ` 395` ``` apply - ``` chaieb@29846 ` 396` ``` apply (rule setprod_cong, simp_all)+ ``` chaieb@29846 ` 397` ``` done ``` chaieb@29846 ` 398` ``` have th3: "finite ?Uk" "k \ ?Uk" using k by auto ``` chaieb@29846 ` 399` ``` have "setprod (\i. ?f i \$ p i) ?U = setprod (\i. ?f i \$ p i) (insert k ?Uk)" ``` chaieb@29846 ` 400` ``` unfolding kU[symmetric] .. ``` chaieb@29846 ` 401` ``` also have "\ = ?f k \$ p k * setprod (\i. ?f i \$ p i) ?Uk" ``` chaieb@29846 ` 402` ``` apply (rule setprod_insert) ``` chaieb@29846 ` 403` ``` apply simp ``` chaieb@29846 ` 404` ``` using k by blast ``` chaieb@29846 ` 405` ``` also have "\ = (a k \$ p k * setprod (\i. ?f i \$ p i) ?Uk) + (b k\$ p k * setprod (\i. ?f i \$ p i) ?Uk)" using pkU by (simp add: ring_simps vector_component) ``` chaieb@29846 ` 406` ``` also have "\ = (a k \$ p k * setprod (\i. ?g i \$ p i) ?Uk) + (b k\$ p k * setprod (\i. ?h i \$ p i) ?Uk)" by (metis th1 th2) ``` chaieb@29846 ` 407` ``` also have "\ = setprod (\i. ?g i \$ p i) (insert k ?Uk) + setprod (\i. ?h i \$ p i) (insert k ?Uk)" ``` chaieb@29846 ` 408` ``` unfolding setprod_insert[OF th3] by simp ``` chaieb@29846 ` 409` ``` finally have "setprod (\i. ?f i \$ p i) ?U = setprod (\i. ?g i \$ p i) ?U + setprod (\i. ?h i \$ p i) ?U" unfolding kU[symmetric] . ``` chaieb@29846 ` 410` ``` then show "of_int (sign p) * setprod (\i. ?f i \$ p i) ?U = of_int (sign p) * setprod (\i. ?g i \$ p i) ?U + of_int (sign p) * setprod (\i. ?h i \$ p i) ?U" ``` chaieb@29846 ` 411` ``` by (simp add: ring_simps) ``` chaieb@29846 ` 412` ```qed ``` chaieb@29846 ` 413` chaieb@29846 ` 414` ```lemma det_row_mul: ``` chaieb@29846 ` 415` ``` assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 416` ``` shows "det((\ i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = ``` chaieb@29846 ` 417` ``` c* det((\ i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" ``` chaieb@29846 ` 418` chaieb@29846 ` 419` ```unfolding det_def setprod_lambda_beta2 setsum_right_distrib ``` chaieb@29846 ` 420` ```proof (rule setsum_cong2) ``` chaieb@29846 ` 421` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 422` ``` let ?pU = "{p. p permutes ?U}" ``` chaieb@29846 ` 423` ``` let ?f = "(\i. if i = k then c*s a i else b i)::nat \ 'a::comm_ring_1^'n" ``` chaieb@29846 ` 424` ``` let ?g = "(\ i. if i = k then a i else b i)::nat \ 'a::comm_ring_1^'n" ``` chaieb@29846 ` 425` ``` fix p assume p: "p \ ?pU" ``` chaieb@29846 ` 426` ``` let ?Uk = "?U - {k}" ``` chaieb@29846 ` 427` ``` from p have pU: "p permutes ?U" by blast ``` chaieb@29846 ` 428` ``` from k have pkU: "p k \ ?U" by (simp only: permutes_in_image[OF pU]) ``` chaieb@29846 ` 429` ``` note pin[simp] = permutes_in_image[OF pU] ``` chaieb@29846 ` 430` ``` have kU: "?U = insert k ?Uk" using k by blast ``` chaieb@29846 ` 431` ``` {fix j assume j: "j \ ?Uk" ``` chaieb@29846 ` 432` ``` from j have "?f j \$ p j = ?g j \$ p j" by simp} ``` chaieb@29846 ` 433` ``` then have th1: "setprod (\i. ?f i \$ p i) ?Uk = setprod (\i. ?g i \$ p i) ?Uk" ``` chaieb@29846 ` 434` ``` apply - ``` chaieb@29846 ` 435` ``` apply (rule setprod_cong, simp_all) ``` chaieb@29846 ` 436` ``` done ``` chaieb@29846 ` 437` ``` have th3: "finite ?Uk" "k \ ?Uk" using k by auto ``` chaieb@29846 ` 438` ``` have "setprod (\i. ?f i \$ p i) ?U = setprod (\i. ?f i \$ p i) (insert k ?Uk)" ``` chaieb@29846 ` 439` ``` unfolding kU[symmetric] .. ``` chaieb@29846 ` 440` ``` also have "\ = ?f k \$ p k * setprod (\i. ?f i \$ p i) ?Uk" ``` chaieb@29846 ` 441` ``` apply (rule setprod_insert) ``` chaieb@29846 ` 442` ``` apply simp ``` chaieb@29846 ` 443` ``` using k by blast ``` chaieb@29846 ` 444` ``` also have "\ = (c*s a k) \$ p k * setprod (\i. ?f i \$ p i) ?Uk" using pkU by (simp add: ring_simps vector_component) ``` chaieb@29846 ` 445` ``` also have "\ = c* (a k \$ p k * setprod (\i. ?g i \$ p i) ?Uk)" ``` chaieb@29846 ` 446` ``` unfolding th1 using pkU by (simp add: vector_component mult_ac) ``` chaieb@29846 ` 447` ``` also have "\ = c* (setprod (\i. ?g i \$ p i) (insert k ?Uk))" ``` chaieb@29846 ` 448` ``` unfolding setprod_insert[OF th3] by simp ``` chaieb@29846 ` 449` ``` finally have "setprod (\i. ?f i \$ p i) ?U = c* (setprod (\i. ?g i \$ p i) ?U)" unfolding kU[symmetric] . ``` chaieb@29846 ` 450` ``` then show "of_int (sign p) * setprod (\i. ?f i \$ p i) ?U = c * (of_int (sign p) * setprod (\i. ?g i \$ p i) ?U)" ``` chaieb@29846 ` 451` ``` by (simp add: ring_simps) ``` chaieb@29846 ` 452` ```qed ``` chaieb@29846 ` 453` chaieb@29846 ` 454` ```lemma det_row_0: ``` chaieb@29846 ` 455` ``` assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 456` ``` shows "det((\ i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0" ``` chaieb@29846 ` 457` ```using det_row_mul[OF k, of 0 "\i. 1" b] ``` chaieb@29846 ` 458` ```apply (simp) ``` chaieb@29846 ` 459` ``` unfolding vector_smult_lzero . ``` chaieb@29846 ` 460` chaieb@29846 ` 461` ```lemma det_row_operation: ``` chaieb@29846 ` 462` ``` fixes A :: "'a::ordered_idom^'n^'n" ``` chaieb@29846 ` 463` ``` assumes i: "i \ {1 .. dimindex(UNIV :: 'n set)}" ``` chaieb@29846 ` 464` ``` and j: "j \ {1 .. dimindex(UNIV :: 'n set)}" ``` chaieb@29846 ` 465` ``` and ij: "i \ j" ``` chaieb@29846 ` 466` ``` shows "det (\ k. if k = i then row i A + c *s row j A else row k A) = det A" ``` chaieb@29846 ` 467` ```proof- ``` chaieb@29846 ` 468` ``` let ?Z = "(\ k. if k = i then row j A else row k A) :: 'a ^'n^'n" ``` chaieb@29846 ` 469` ``` have th: "row i ?Z = row j ?Z" using i j by (vector row_def) ``` chaieb@29846 ` 470` ``` have th2: "((\ k. if k = i then row i A else row k A) :: 'a^'n^'n) = A" ``` chaieb@29846 ` 471` ``` using i j by (vector row_def) ``` chaieb@29846 ` 472` ``` show ?thesis ``` chaieb@29846 ` 473` ``` unfolding det_row_add [OF i] det_row_mul[OF i] det_identical_rows[OF i j ij th] th2 ``` chaieb@29846 ` 474` ``` by simp ``` chaieb@29846 ` 475` ```qed ``` chaieb@29846 ` 476` chaieb@29846 ` 477` ```lemma det_row_span: ``` chaieb@29846 ` 478` ``` fixes A :: "'a:: ordered_idom^'n^'n" ``` chaieb@29846 ` 479` ``` assumes i: "i \ {1 .. dimindex(UNIV :: 'n set)}" ``` chaieb@29846 ` 480` ``` and x: "x \ span {row j A |j. j\ {1 .. dimindex(UNIV :: 'n set)} \ j\ i}" ``` chaieb@29846 ` 481` ``` shows "det (\ k. if k = i then row i A + x else row k A) = det A" ``` chaieb@29846 ` 482` ```proof- ``` chaieb@29846 ` 483` ``` let ?U = "{1 .. dimindex(UNIV :: 'n set)}" ``` chaieb@29846 ` 484` ``` let ?S = "{row j A |j. j\ ?U \ j\ i}" ``` chaieb@29846 ` 485` ``` let ?d = "\x. det (\ k. if k = i then x else row k A)" ``` chaieb@29846 ` 486` ``` let ?P = "\x. ?d (row i A + x) = det A" ``` chaieb@29846 ` 487` ``` {fix k ``` chaieb@29846 ` 488` ``` ``` chaieb@29846 ` 489` ``` have "(if k = i then row i A + 0 else row k A) = row k A" by simp} ``` chaieb@29846 ` 490` ``` then have P0: "?P 0" ``` chaieb@29846 ` 491` ``` apply - ``` chaieb@29846 ` 492` ``` apply (rule cong[of det, OF refl]) ``` chaieb@29846 ` 493` ``` using i by (vector row_def) ``` chaieb@29846 ` 494` ``` moreover ``` chaieb@29846 ` 495` ``` {fix c z y assume zS: "z \ ?S" and Py: "?P y" ``` chaieb@29846 ` 496` ``` from zS obtain j where j: "z = row j A" "j \ ?U" "i \ j" by blast ``` chaieb@29846 ` 497` ``` let ?w = "row i A + y" ``` chaieb@29846 ` 498` ``` have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector ``` chaieb@29846 ` 499` ``` have thz: "?d z = 0" ``` chaieb@29846 ` 500` ``` apply (rule det_identical_rows[OF i j(2,3)]) ``` chaieb@29846 ` 501` ``` using i j by (vector row_def) ``` chaieb@29846 ` 502` ``` have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 .. ``` chaieb@29846 ` 503` ``` then have "?P (c*s z + y)" unfolding thz Py det_row_mul[OF i] det_row_add[OF i] ``` chaieb@29846 ` 504` ``` by simp } ``` chaieb@29846 ` 505` chaieb@29846 ` 506` ``` ultimately show ?thesis ``` chaieb@29846 ` 507` ``` apply - ``` chaieb@29846 ` 508` ``` apply (rule span_induct_alt[of ?P ?S, OF P0]) ``` chaieb@29846 ` 509` ``` apply blast ``` chaieb@29846 ` 510` ``` apply (rule x) ``` chaieb@29846 ` 511` ``` done ``` chaieb@29846 ` 512` ```qed ``` chaieb@29846 ` 513` chaieb@29846 ` 514` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 515` ```(* May as well do this, though it's a bit unsatisfactory since it ignores *) ``` chaieb@29846 ` 516` ```(* exact duplicates by considering the rows/columns as a set. *) ``` chaieb@29846 ` 517` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 518` chaieb@29846 ` 519` ```lemma det_dependent_rows: ``` chaieb@29846 ` 520` ``` fixes A:: "'a::ordered_idom^'n^'n" ``` chaieb@29846 ` 521` ``` assumes d: "dependent (rows A)" ``` chaieb@29846 ` 522` ``` shows "det A = 0" ``` chaieb@29846 ` 523` ```proof- ``` chaieb@29846 ` 524` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 525` ``` from d obtain i where i: "i \ ?U" "row i A \ span (rows A - {row i A})" ``` chaieb@29846 ` 526` ``` unfolding dependent_def rows_def by blast ``` chaieb@29846 ` 527` ``` {fix j k assume j: "j \?U" and k: "k \ ?U" and jk: "j \ k" ``` chaieb@29846 ` 528` ``` and c: "row j A = row k A" ``` chaieb@29846 ` 529` ``` from det_identical_rows[OF j k jk c] have ?thesis .} ``` chaieb@29846 ` 530` ``` moreover ``` chaieb@29846 ` 531` ``` {assume H: "\ i j. i\ ?U \ j \ ?U \ i \ j \ row i A \ row j A" ``` chaieb@29846 ` 532` ``` have th0: "- row i A \ span {row j A|j. j \ ?U \ j \ i}" ``` chaieb@29846 ` 533` ``` apply (rule span_neg) ``` chaieb@29846 ` 534` ``` apply (rule set_rev_mp) ``` chaieb@29846 ` 535` ``` apply (rule i(2)) ``` chaieb@29846 ` 536` ``` apply (rule span_mono) ``` chaieb@29846 ` 537` ``` using H i by (auto simp add: rows_def) ``` chaieb@29846 ` 538` ``` from det_row_span[OF i(1) th0] ``` chaieb@29846 ` 539` ``` have "det A = det (\ k. if k = i then 0 *s 1 else row k A)" ``` chaieb@29846 ` 540` ``` unfolding right_minus vector_smult_lzero .. ``` chaieb@29846 ` 541` ``` with det_row_mul[OF i(1), of "0::'a" "\i. 1"] ``` chaieb@29846 ` 542` ``` have "det A = 0" by simp} ``` chaieb@29846 ` 543` ``` ultimately show ?thesis by blast ``` chaieb@29846 ` 544` ```qed ``` chaieb@29846 ` 545` chaieb@29846 ` 546` ```lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n))" shows "det A = 0" ``` chaieb@29846 ` 547` ```by (metis d det_dependent_rows rows_transp det_transp) ``` chaieb@29846 ` 548` chaieb@29846 ` 549` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 550` ```(* Multilinearity and the multiplication formula. *) ``` chaieb@29846 ` 551` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 552` chaieb@29846 ` 553` ```lemma Cart_lambda_cong: "(\x. x \ {1 .. dimindex (UNIV :: 'n set)} \ f x = g x) \ (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)" ``` chaieb@29846 ` 554` ``` apply (rule iffD1[OF Cart_lambda_unique]) by vector ``` chaieb@29846 ` 555` chaieb@29846 ` 556` ```lemma det_linear_row_setsum: ``` chaieb@29846 ` 557` ``` assumes fS: "finite S" and k: "k \ {1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 558` ``` shows "det ((\ i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (\j. det ((\ i. if i = k then a i j else c i)::'a^'n^'n)) S" ``` chaieb@29846 ` 559` ``` using k ``` chaieb@29846 ` 560` ```proof(induct rule: finite_induct[OF fS]) ``` chaieb@29846 ` 561` ``` case 1 thus ?case apply simp unfolding setsum_empty det_row_0[OF k] .. ``` chaieb@29846 ` 562` ```next ``` chaieb@29846 ` 563` ``` case (2 x F) ``` chaieb@29846 ` 564` ``` then show ?case by (simp add: det_row_add cong del: if_weak_cong) ``` chaieb@29846 ` 565` ```qed ``` chaieb@29846 ` 566` chaieb@29846 ` 567` ```lemma finite_bounded_functions: ``` chaieb@29846 ` 568` ``` assumes fS: "finite S" ``` chaieb@29846 ` 569` ``` shows "finite {f. (\i \ {1.. (k::nat)}. f i \ S) \ (\i. i \ {1 .. k} \ f i = i)}" ``` chaieb@29846 ` 570` ```proof(induct k) ``` chaieb@29846 ` 571` ``` case 0 ``` chaieb@29846 ` 572` ``` have th: "{f. \i. f i = i} = {id}" by (auto intro: ext) ``` chaieb@29846 ` 573` ``` show ?case by (auto simp add: th) ``` chaieb@29846 ` 574` ```next ``` chaieb@29846 ` 575` ``` case (Suc k) ``` chaieb@29846 ` 576` ``` let ?f = "\(y::nat,g) i. if i = Suc k then y else g i" ``` chaieb@29846 ` 577` ``` let ?S = "?f ` (S \ {f. (\i\{1..k}. f i \ S) \ (\i. i \ {1..k} \ f i = i)})" ``` chaieb@29846 ` 578` ``` have "?S = {f. (\i\{1.. Suc k}. f i \ S) \ (\i. i \ {1.. Suc k} \ f i = i)}" ``` chaieb@29846 ` 579` ``` apply (auto simp add: image_iff) ``` chaieb@29846 ` 580` ``` apply (rule_tac x="x (Suc k)" in bexI) ``` chaieb@29846 ` 581` ``` apply (rule_tac x = "\i. if i = Suc k then i else x i" in exI) ``` chaieb@29846 ` 582` ``` apply (auto intro: ext) ``` chaieb@29846 ` 583` ``` done ``` chaieb@29846 ` 584` ``` with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] ``` chaieb@29846 ` 585` ``` show ?case by metis ``` chaieb@29846 ` 586` ```qed ``` chaieb@29846 ` 587` chaieb@29846 ` 588` chaieb@29846 ` 589` ```lemma eq_id_iff[simp]: "(\x. f x = x) = (f = id)" by (auto intro: ext) ``` chaieb@29846 ` 590` chaieb@29846 ` 591` ```lemma det_linear_rows_setsum_lemma: ``` chaieb@29846 ` 592` ``` assumes fS: "finite S" and k: "k \ dimindex (UNIV :: 'n set)" ``` chaieb@29846 ` 593` ``` shows "det((\ i. if i <= k then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = ``` chaieb@29846 ` 594` ``` setsum (\f. det((\ i. if i <= k then a i (f i) else c i)::'a^'n^'n)) ``` chaieb@29846 ` 595` ``` {f. (\i \ {1 .. k}. f i \ S) \ (\i. i \ {1..k} \ f i = i)}" ``` chaieb@29846 ` 596` ```using k ``` chaieb@29846 ` 597` ```proof(induct k arbitrary: a c) ``` chaieb@29846 ` 598` ``` case 0 ``` chaieb@29846 ` 599` ``` have th0: "\x y. (\ i. if i <= 0 then x i else y i) = (\ i. y i)" by vector ``` chaieb@29846 ` 600` ``` from "0.prems" show ?case unfolding th0 by simp ``` chaieb@29846 ` 601` ```next ``` chaieb@29846 ` 602` ``` case (Suc k a c) ``` chaieb@29846 ` 603` ``` let ?F = "\k. {f. (\i \ {1 .. k}. f i \ S) \ (\i. i \ {1..k} \ f i = i)}" ``` chaieb@29846 ` 604` ``` let ?h = "\(y::nat,g) i. if i = Suc k then y else g i" ``` chaieb@29846 ` 605` ``` let ?k = "\h. (h(Suc k),(\i. if i = Suc k then i else h i))" ``` chaieb@29846 ` 606` ``` let ?s = "\ k a c f. det((\ i. if i <= k then a i (f i) else c i)::'a^'n^'n)" ``` chaieb@29846 ` 607` ``` let ?c = "\i. if i = Suc k then a i j else c i" ``` chaieb@29846 ` 608` ``` from Suc.prems have Sk: "Suc k \ {1 .. dimindex (UNIV :: 'n set)}" by simp ``` chaieb@29846 ` 609` ``` from Suc.prems have k': "k \ dimindex (UNIV :: 'n set)" by arith ``` chaieb@29846 ` 610` ``` have thif: "\a b c d. (if b \ a then c else d) = (if a then c else if b then c else d)" by simp ``` chaieb@29846 ` 611` ``` have thif2: "\a b c d e. (if a then b else if c then d else e) = ``` chaieb@29846 ` 612` ``` (if c then (if a then b else d) else (if a then b else e))" by simp ``` chaieb@29846 ` 613` ``` have "det (\ i. if i \ Suc k then setsum (a i) S else c i) = ``` chaieb@29846 ` 614` ``` det (\ i. if i = Suc k then setsum (a i) S ``` chaieb@29846 ` 615` ``` else if i \ k then setsum (a i) S else c i)" ``` chaieb@29846 ` 616` ``` unfolding le_Suc_eq thif .. ``` chaieb@29846 ` 617` ``` also have "\ = (\j\S. det (\ i. if i \ k then setsum (a i) S ``` chaieb@29846 ` 618` ``` else if i = Suc k then a i j else c i))" ``` chaieb@29846 ` 619` ``` unfolding det_linear_row_setsum[OF fS Sk] ``` chaieb@29846 ` 620` ``` apply (subst thif2) ``` chaieb@29846 ` 621` ``` by (simp cong del: if_weak_cong cong add: if_cong) ``` chaieb@29846 ` 622` ``` finally have tha: ``` chaieb@29846 ` 623` ``` "det (\ i. if i \ Suc k then setsum (a i) S else c i) = ``` chaieb@29846 ` 624` ``` (\(j, f)\S \ ?F k. det (\ i. if i \ k then a i (f i) ``` chaieb@29846 ` 625` ``` else if i = Suc k then a i j ``` chaieb@29846 ` 626` ``` else c i))" ``` chaieb@29846 ` 627` ``` unfolding Suc.hyps[OF k'] unfolding setsum_cartesian_product by blast ``` chaieb@29846 ` 628` ``` show ?case unfolding tha ``` chaieb@29846 ` 629` ``` apply(rule setsum_eq_general_reverses[where h= "?h" and k= "?k"], ``` chaieb@29846 ` 630` ``` blast intro: finite_cartesian_product fS finite_bounded_functions[OF fS], ``` chaieb@29846 ` 631` ``` blast intro: finite_cartesian_product fS finite_bounded_functions[OF fS], auto intro: ext) ``` chaieb@29846 ` 632` ``` apply (rule cong[OF refl[of det]]) ``` chaieb@29846 ` 633` ``` by vector ``` chaieb@29846 ` 634` ```qed ``` chaieb@29846 ` 635` chaieb@29846 ` 636` ```lemma det_linear_rows_setsum: ``` chaieb@29846 ` 637` ``` assumes fS: "finite S" ``` chaieb@29846 ` 638` ``` shows "det (\ i. setsum (a i) S) = setsum (\f. det (\ i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. (\i \ {1 .. dimindex (UNIV :: 'n set)}. f i \ S) \ (\i. i \ {1.. dimindex (UNIV :: 'n set)} \ f i = i)}" ``` chaieb@29846 ` 639` ```proof- ``` chaieb@29846 ` 640` ``` have th0: "\x y. ((\ i. if i <= dimindex(UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\ i. x i)" by vector ``` chaieb@29846 ` 641` ``` ``` chaieb@29846 ` 642` ``` from det_linear_rows_setsum_lemma[OF fS, of "dimindex (UNIV :: 'n set)" a, unfolded th0, OF order_refl] show ?thesis by blast ``` chaieb@29846 ` 643` ```qed ``` chaieb@29846 ` 644` chaieb@29846 ` 645` ```lemma matrix_mul_setsum_alt: ``` chaieb@29846 ` 646` ``` fixes A B :: "'a::comm_ring_1^'n^'n" ``` chaieb@29846 ` 647` ``` shows "A ** B = (\ i. setsum (\k. A\$i\$k *s B \$ k) {1 .. dimindex (UNIV :: 'n set)})" ``` chaieb@29846 ` 648` ``` by (vector matrix_matrix_mult_def setsum_component) ``` chaieb@29846 ` 649` chaieb@29846 ` 650` ```lemma det_rows_mul: ``` chaieb@29846 ` 651` ``` "det((\ i. c i *s a i)::'a::comm_ring_1^'n^'n) = ``` chaieb@29846 ` 652` ``` setprod (\i. c i) {1..dimindex(UNIV:: 'n set)} * det((\ i. a i)::'a^'n^'n)" ``` chaieb@29846 ` 653` ```proof (simp add: det_def Cart_lambda_beta' setsum_right_distrib vector_component cong add: setprod_cong del: One_nat_def, rule setsum_cong2) ``` chaieb@29846 ` 654` ``` let ?U = "{1 .. dimindex(UNIV :: 'n set)}" ``` chaieb@29846 ` 655` ``` let ?PU = "{p. p permutes ?U}" ``` chaieb@29846 ` 656` ``` fix p assume pU: "p \ ?PU" ``` chaieb@29846 ` 657` ``` let ?s = "of_int (sign p)" ``` chaieb@29846 ` 658` ``` from pU have p: "p permutes ?U" by blast ``` chaieb@29846 ` 659` ``` have "setprod (\i. (c i *s a i) \$ p i) ?U = setprod (\i. c i * a i \$ p i) ?U" ``` chaieb@29846 ` 660` ``` apply (rule setprod_cong, blast) ``` chaieb@29846 ` 661` ``` by (auto simp only: permutes_in_image[OF p] intro: vector_smult_component) ``` chaieb@29846 ` 662` ``` also have "\ = setprod c ?U * setprod (\i. a i \$ p i) ?U" ``` chaieb@29846 ` 663` ``` unfolding setprod_timesf .. ``` chaieb@29846 ` 664` ``` finally show "?s * (\xa\?U. (c xa *s a xa) \$ p xa) = ``` chaieb@29846 ` 665` ``` setprod c ?U * (?s* (\xa\?U. a xa \$ p xa))" by (simp add: ring_simps) ``` chaieb@29846 ` 666` ```qed ``` chaieb@29846 ` 667` chaieb@29846 ` 668` ```lemma det_mul: ``` chaieb@29846 ` 669` ``` fixes A B :: "'a::ordered_idom^'n^'n" ``` chaieb@29846 ` 670` ``` shows "det (A ** B) = det A * det B" ``` chaieb@29846 ` 671` ```proof- ``` chaieb@29846 ` 672` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 673` ``` let ?F = "{f. (\i\ ?U. f i \ ?U) \ (\i. i \ ?U \ f i = i)}" ``` chaieb@29846 ` 674` ``` let ?PU = "{p. p permutes ?U}" ``` chaieb@29846 ` 675` ``` have fU: "finite ?U" by simp ``` chaieb@29846 ` 676` ``` have fF: "finite ?F" using finite_bounded_functions[OF fU] . ``` chaieb@29846 ` 677` ``` {fix p assume p: "p permutes ?U" ``` chaieb@29846 ` 678` ``` ``` chaieb@29846 ` 679` ``` have "p \ ?F" unfolding mem_Collect_eq permutes_in_image[OF p] ``` chaieb@29846 ` 680` ``` using p[unfolded permutes_def] by simp} ``` chaieb@29846 ` 681` ``` then have PUF: "?PU \ ?F" by blast ``` chaieb@29846 ` 682` ``` {fix f assume fPU: "f \ ?F - ?PU" ``` chaieb@29846 ` 683` ``` have fUU: "f ` ?U \ ?U" using fPU by auto ``` chaieb@29846 ` 684` ``` from fPU have f: "\i \ ?U. f i \ ?U" ``` chaieb@29846 ` 685` ``` "\i. i \ ?U \ f i = i" "\(\y. \!x. f x = y)" unfolding permutes_def ``` chaieb@29846 ` 686` ``` by auto ``` chaieb@29846 ` 687` ``` ``` chaieb@29846 ` 688` ``` let ?A = "(\ i. A\$i\$f i *s B\$f i) :: 'a^'n^'n" ``` chaieb@29846 ` 689` ``` let ?B = "(\ i. B\$f i) :: 'a^'n^'n" ``` chaieb@29846 ` 690` ``` {assume fni: "\ inj_on f ?U" ``` chaieb@29846 ` 691` ``` then obtain i j where ij: "i \ ?U" "j \ ?U" "f i = f j" "i \ j" ``` chaieb@29846 ` 692` ``` unfolding inj_on_def by blast ``` chaieb@29846 ` 693` ``` from ij ``` chaieb@29846 ` 694` ``` have rth: "row i ?B = row j ?B" by (vector row_def) ``` chaieb@29846 ` 695` ``` from det_identical_rows[OF ij(1,2,4) rth] ``` chaieb@29846 ` 696` ``` have "det (\ i. A\$i\$f i *s B\$f i) = 0" ``` chaieb@29846 ` 697` ``` unfolding det_rows_mul by simp} ``` chaieb@29846 ` 698` ``` moreover ``` chaieb@29846 ` 699` ``` {assume fi: "inj_on f ?U" ``` chaieb@29846 ` 700` ``` from f fi have fith: "\i j. f i = f j \ i = j" ``` chaieb@29846 ` 701` ``` unfolding inj_on_def ``` chaieb@29846 ` 702` ``` apply (case_tac "i \ ?U") ``` chaieb@29846 ` 703` ``` apply (case_tac "j \ ?U") by metis+ ``` chaieb@29846 ` 704` ``` note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]] ``` chaieb@29846 ` 705` ``` ``` chaieb@29846 ` 706` ``` {fix y ``` chaieb@29846 ` 707` ``` from fs f have "\x. f x = y" by (cases "y \ ?U") blast+ ``` chaieb@29846 ` 708` ``` then obtain x where x: "f x = y" by blast ``` chaieb@29846 ` 709` ``` {fix z assume z: "f z = y" from fith x z have "z = x" by metis} ``` chaieb@29846 ` 710` ``` with x have "\!x. f x = y" by blast} ``` chaieb@29846 ` 711` ``` with f(3) have "det (\ i. A\$i\$f i *s B\$f i) = 0" by blast} ``` chaieb@29846 ` 712` ``` ultimately have "det (\ i. A\$i\$f i *s B\$f i) = 0" by blast} ``` chaieb@29846 ` 713` ``` hence zth: "\ f\ ?F - ?PU. det (\ i. A\$i\$f i *s B\$f i) = 0" by simp ``` chaieb@29846 ` 714` ``` {fix p assume pU: "p \ ?PU" ``` chaieb@29846 ` 715` ``` from pU have p: "p permutes ?U" by blast ``` chaieb@29846 ` 716` ``` let ?s = "\p. of_int (sign p)" ``` chaieb@29846 ` 717` ``` let ?f = "\q. ?s p * (\i\ ?U. A \$ i \$ p i) * ``` chaieb@29846 ` 718` ``` (?s q * (\i\ ?U. B \$ i \$ q i))" ``` chaieb@29846 ` 719` ``` have "(setsum (\q. ?s q * ``` chaieb@29846 ` 720` ``` (\i\ ?U. (\ i. A \$ i \$ p i *s B \$ p i :: 'a^'n^'n) \$ i \$ q i)) ?PU) = ``` chaieb@29846 ` 721` ``` (setsum (\q. ?s p * (\i\ ?U. A \$ i \$ p i) * ``` chaieb@29846 ` 722` ``` (?s q * (\i\ ?U. B \$ i \$ q i))) ?PU)" ``` chaieb@29846 ` 723` ``` unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] ``` chaieb@29846 ` 724` ``` proof(rule setsum_cong2) ``` chaieb@29846 ` 725` ``` fix q assume qU: "q \ ?PU" ``` chaieb@29846 ` 726` ``` hence q: "q permutes ?U" by blast ``` chaieb@29846 ` 727` ``` from p q have pp: "permutation p" and pq: "permutation q" ``` chaieb@29846 ` 728` ``` unfolding permutation_permutes by auto ``` chaieb@29846 ` 729` ``` have th00: "of_int (sign p) * of_int (sign p) = (1::'a)" ``` chaieb@29846 ` 730` ``` "\a. of_int (sign p) * (of_int (sign p) * a) = a" ``` chaieb@29846 ` 731` ``` unfolding mult_assoc[symmetric] unfolding of_int_mult[symmetric] ``` chaieb@29846 ` 732` ``` by (simp_all add: sign_idempotent) ``` chaieb@29846 ` 733` ``` have ths: "?s q = ?s p * ?s (q o inv p)" ``` chaieb@29846 ` 734` ``` using pp pq permutation_inverse[OF pp] sign_inverse[OF pp] ``` chaieb@29846 ` 735` ``` by (simp add: th00 mult_ac sign_idempotent sign_compose) ``` chaieb@29846 ` 736` ``` have th001: "setprod (\i. B\$i\$ q (inv p i)) ?U = setprod ((\i. B\$i\$ q (inv p i)) o p) ?U" ``` chaieb@29846 ` 737` ``` by (rule setprod_permute[OF p]) ``` chaieb@29846 ` 738` ``` have thp: "setprod (\i. (\ i. A\$i\$p i *s B\$p i :: 'a^'n^'n) \$i \$ q i) ?U = setprod (\i. A\$i\$p i) ?U * setprod (\i. B\$i\$ q (inv p i)) ?U" ``` chaieb@29846 ` 739` ``` unfolding th001 setprod_timesf[symmetric] o_def permutes_inverses[OF p] ``` chaieb@29846 ` 740` ``` apply (rule setprod_cong[OF refl]) ``` chaieb@29846 ` 741` ``` using permutes_in_image[OF q] by vector ``` chaieb@29846 ` 742` ``` show "?s q * setprod (\i. (((\ i. A\$i\$p i *s B\$p i) :: 'a^'n^'n)\$i\$q i)) ?U = ?s p * (setprod (\i. A\$i\$p i) ?U) * (?s (q o inv p) * setprod (\i. B\$i\$(q o inv p) i) ?U)" ``` chaieb@29846 ` 743` ``` using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] ``` chaieb@29846 ` 744` ``` by (simp add: sign_nz th00 ring_simps sign_idempotent sign_compose) ``` chaieb@29846 ` 745` ``` qed ``` chaieb@29846 ` 746` ``` } ``` chaieb@29846 ` 747` ``` then have th2: "setsum (\f. det (\ i. A\$i\$f i *s B\$f i)) ?PU = det A * det B" ``` chaieb@29846 ` 748` ``` unfolding det_def setsum_product ``` chaieb@29846 ` 749` ``` by (rule setsum_cong2) ``` chaieb@29846 ` 750` ``` have "det (A**B) = setsum (\f. det (\ i. A \$ i \$ f i *s B \$ f i)) ?F" ``` chaieb@29846 ` 751` ``` unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] .. ``` chaieb@29846 ` 752` ``` also have "\ = setsum (\f. det (\ i. A\$i\$f i *s B\$f i)) ?PU" ``` chaieb@29846 ` 753` ``` unfolding setsum_superset[OF fF PUF zth, symmetric] ``` chaieb@29846 ` 754` ``` unfolding det_rows_mul .. ``` chaieb@29846 ` 755` ``` finally show ?thesis unfolding th2 . ``` chaieb@29846 ` 756` ```qed ``` chaieb@29846 ` 757` chaieb@29846 ` 758` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 759` ```(* Relation to invertibility. *) ``` chaieb@29846 ` 760` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 761` chaieb@29846 ` 762` ```lemma invertible_left_inverse: ``` chaieb@29846 ` 763` ``` fixes A :: "real^'n^'n" ``` chaieb@29846 ` 764` ``` shows "invertible A \ (\(B::real^'n^'n). B** A = mat 1)" ``` chaieb@29846 ` 765` ``` by (metis invertible_def matrix_left_right_inverse) ``` chaieb@29846 ` 766` chaieb@29846 ` 767` ```lemma invertible_righ_inverse: ``` chaieb@29846 ` 768` ``` fixes A :: "real^'n^'n" ``` chaieb@29846 ` 769` ``` shows "invertible A \ (\(B::real^'n^'n). A** B = mat 1)" ``` chaieb@29846 ` 770` ``` by (metis invertible_def matrix_left_right_inverse) ``` chaieb@29846 ` 771` chaieb@29846 ` 772` ```lemma invertible_det_nz: ``` chaieb@29846 ` 773` ``` fixes A::"real ^'n^'n" ``` chaieb@29846 ` 774` ``` shows "invertible A \ det A \ 0" ``` chaieb@29846 ` 775` ```proof- ``` chaieb@29846 ` 776` ``` {assume "invertible A" ``` chaieb@29846 ` 777` ``` then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1" ``` chaieb@29846 ` 778` ``` unfolding invertible_righ_inverse by blast ``` chaieb@29846 ` 779` ``` hence "det (A ** B) = det (mat 1 :: real ^'n^'n)" by simp ``` chaieb@29846 ` 780` ``` hence "det A \ 0" ``` chaieb@29846 ` 781` ``` apply (simp add: det_mul det_I) by algebra } ``` chaieb@29846 ` 782` ``` moreover ``` chaieb@29846 ` 783` ``` {assume H: "\ invertible A" ``` chaieb@29846 ` 784` ``` let ?U = "{1 .. dimindex(UNIV :: 'n set)}" ``` chaieb@29846 ` 785` ``` have fU: "finite ?U" by simp ``` chaieb@29846 ` 786` ``` from H obtain c i where c: "setsum (\i. c i *s row i A) ?U = 0" ``` chaieb@29846 ` 787` ``` and iU: "i \ ?U" and ci: "c i \ 0" ``` chaieb@29846 ` 788` ``` unfolding invertible_righ_inverse ``` chaieb@29846 ` 789` ``` unfolding matrix_right_invertible_independent_rows by blast ``` chaieb@29846 ` 790` ``` have stupid: "\(a::real^'n) b. a + b = 0 \ -a = b" ``` chaieb@29846 ` 791` ``` apply (drule_tac f="op + (- a)" in cong[OF refl]) ``` chaieb@29846 ` 792` ``` apply (simp only: ab_left_minus add_assoc[symmetric]) ``` chaieb@29846 ` 793` ``` apply simp ``` chaieb@29846 ` 794` ``` done ``` chaieb@29846 ` 795` ``` from c ci ``` chaieb@29846 ` 796` ``` have thr0: "- row i A = setsum (\j. (1/ c i) *s c j *s row j A) (?U - {i})" ``` chaieb@29846 ` 797` ``` unfolding setsum_diff1'[OF fU iU] setsum_cmul ``` chaieb@29846 ` 798` ``` apply (simp add: field_simps) ``` chaieb@29846 ` 799` ``` apply (rule vector_mul_lcancel_imp[OF ci]) ``` chaieb@29846 ` 800` ``` apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps) ``` chaieb@29846 ` 801` ``` unfolding stupid .. ``` chaieb@29846 ` 802` ``` have thr: "- row i A \ span {row j A| j. j\ ?U \ j \ i}" ``` chaieb@29846 ` 803` ``` unfolding thr0 ``` chaieb@29846 ` 804` ``` apply (rule span_setsum) ``` chaieb@29846 ` 805` ``` apply simp ``` chaieb@29846 ` 806` ``` apply (rule ballI) ``` chaieb@29846 ` 807` ``` apply (rule span_mul)+ ``` chaieb@29846 ` 808` ``` apply (rule span_superset) ``` chaieb@29846 ` 809` ``` apply auto ``` chaieb@29846 ` 810` ``` done ``` chaieb@29846 ` 811` ``` let ?B = "(\ k. if k = i then 0 else row k A) :: real ^'n^'n" ``` chaieb@29846 ` 812` ``` have thrb: "row i ?B = 0" using iU by (vector row_def) ``` chaieb@29846 ` 813` ``` have "det A = 0" ``` chaieb@29846 ` 814` ``` unfolding det_row_span[OF iU thr, symmetric] right_minus ``` chaieb@29846 ` 815` ``` unfolding det_zero_row[OF iU thrb] ..} ``` chaieb@29846 ` 816` ``` ultimately show ?thesis by blast ``` chaieb@29846 ` 817` ```qed ``` chaieb@29846 ` 818` chaieb@29846 ` 819` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 820` ```(* Cramer's rule. *) ``` chaieb@29846 ` 821` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 822` chaieb@29846 ` 823` ```lemma cramer_lemma_transp: ``` chaieb@29846 ` 824` ``` fixes A:: "'a::ordered_idom^'n^'n" and x :: "'a ^'n" ``` chaieb@29846 ` 825` ``` assumes k: "k \ {1 .. dimindex(UNIV ::'n set)}" ``` chaieb@29846 ` 826` ``` shows "det ((\ i. if i = k then setsum (\i. x\$i *s row i A) {1 .. dimindex(UNIV::'n set)} ``` chaieb@29846 ` 827` ``` else row i A)::'a^'n^'n) = x\$k * det A" ``` chaieb@29846 ` 828` ``` (is "?lhs = ?rhs") ``` chaieb@29846 ` 829` ```proof- ``` chaieb@29846 ` 830` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 831` ``` let ?Uk = "?U - {k}" ``` chaieb@29846 ` 832` ``` have U: "?U = insert k ?Uk" using k by blast ``` chaieb@29846 ` 833` ``` have fUk: "finite ?Uk" by simp ``` chaieb@29846 ` 834` ``` have kUk: "k \ ?Uk" by simp ``` chaieb@29846 ` 835` ``` have th00: "\k s. x\$k *s row k A + s = (x\$k - 1) *s row k A + row k A + s" ``` chaieb@29846 ` 836` ``` by (vector ring_simps) ``` chaieb@29846 ` 837` ``` have th001: "\f k . (\x. if x = k then f k else f x) = f" by (auto intro: ext) ``` chaieb@29846 ` 838` ``` have "(\ i. row i A) = A" by (vector row_def) ``` chaieb@29846 ` 839` ``` then have thd1: "det (\ i. row i A) = det A" by simp ``` chaieb@29846 ` 840` ``` have thd0: "det (\ i. if i = k then row k A + (\i \ ?Uk. x \$ i *s row i A) else row i A) = det A" ``` chaieb@29846 ` 841` ``` apply (rule det_row_span[OF k]) ``` chaieb@29846 ` 842` ``` apply (rule span_setsum[OF fUk]) ``` chaieb@29846 ` 843` ``` apply (rule ballI) ``` chaieb@29846 ` 844` ``` apply (rule span_mul) ``` chaieb@29846 ` 845` ``` apply (rule span_superset) ``` chaieb@29846 ` 846` ``` apply auto ``` chaieb@29846 ` 847` ``` done ``` chaieb@29846 ` 848` ``` show "?lhs = x\$k * det A" ``` chaieb@29846 ` 849` ``` apply (subst U) ``` chaieb@29846 ` 850` ``` unfolding setsum_insert[OF fUk kUk] ``` chaieb@29846 ` 851` ``` apply (subst th00) ``` chaieb@29846 ` 852` ``` unfolding add_assoc ``` chaieb@29846 ` 853` ``` apply (subst det_row_add[OF k]) ``` chaieb@29846 ` 854` ``` unfolding thd0 ``` chaieb@29846 ` 855` ``` unfolding det_row_mul[OF k] ``` chaieb@29846 ` 856` ``` unfolding th001[of k "\i. row i A"] ``` chaieb@29846 ` 857` ``` unfolding thd1 by (simp add: ring_simps) ``` chaieb@29846 ` 858` ```qed ``` chaieb@29846 ` 859` chaieb@29846 ` 860` ```lemma cramer_lemma: ``` chaieb@29846 ` 861` ``` fixes A :: "'a::ordered_idom ^'n^'n" ``` chaieb@29846 ` 862` ``` assumes k: "k \ {1 .. dimindex (UNIV :: 'n set)}" (is " _ \ ?U") ``` chaieb@29846 ` 863` ``` shows "det((\ i j. if j = k then (A *v x)\$i else A\$i\$j):: 'a^'n^'n) = x\$k * det A" ``` chaieb@29846 ` 864` ```proof- ``` chaieb@29846 ` 865` ``` have stupid: "\c. setsum (\i. c i *s row i (transp A)) ?U = setsum (\i. c i *s column i A) ?U" ``` chaieb@29846 ` 866` ``` by (auto simp add: row_transp intro: setsum_cong2) ``` chaieb@29846 ` 867` ``` show ?thesis ``` chaieb@29846 ` 868` ``` unfolding matrix_mult_vsum ``` chaieb@29846 ` 869` ``` unfolding cramer_lemma_transp[OF k, of x "transp A", unfolded det_transp, symmetric] ``` chaieb@29846 ` 870` ``` unfolding stupid[of "\i. x\$i"] ``` chaieb@29846 ` 871` ``` apply (subst det_transp[symmetric]) ``` chaieb@29846 ` 872` ``` apply (rule cong[OF refl[of det]]) by (vector transp_def column_def row_def) ``` chaieb@29846 ` 873` ```qed ``` chaieb@29846 ` 874` chaieb@29846 ` 875` ```lemma cramer: ``` chaieb@29846 ` 876` ``` fixes A ::"real^'n^'n" ``` chaieb@29846 ` 877` ``` assumes d0: "det A \ 0" ``` chaieb@29846 ` 878` ``` shows "A *v x = b \ x = (\ k. det(\ i j. if j=k then b\$i else A\$i\$j :: real^'n^'n) / det A)" ``` chaieb@29846 ` 879` ```proof- ``` chaieb@29846 ` 880` ``` from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" ``` chaieb@29846 ` 881` ``` unfolding invertible_det_nz[symmetric] invertible_def by blast ``` chaieb@29846 ` 882` ``` have "(A ** B) *v b = b" by (simp add: B matrix_vector_mul_lid) ``` chaieb@29846 ` 883` ``` hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc) ``` chaieb@29846 ` 884` ``` then have xe: "\x. A*v x = b" by blast ``` chaieb@29846 ` 885` ``` {fix x assume x: "A *v x = b" ``` chaieb@29846 ` 886` ``` have "x = (\ k. det(\ i j. if j=k then b\$i else A\$i\$j :: real^'n^'n) / det A)" ``` chaieb@29846 ` 887` ``` unfolding x[symmetric] ``` chaieb@29846 ` 888` ``` using d0 by (simp add: Cart_eq Cart_lambda_beta' cramer_lemma field_simps)} ``` chaieb@29846 ` 889` ``` with xe show ?thesis by auto ``` chaieb@29846 ` 890` ```qed ``` chaieb@29846 ` 891` chaieb@29846 ` 892` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 893` ```(* Orthogonality of a transformation and matrix. *) ``` chaieb@29846 ` 894` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 895` chaieb@29846 ` 896` ```definition "orthogonal_transformation f \ linear f \ (\v w. f v \ f w = v \ w)" ``` chaieb@29846 ` 897` chaieb@29846 ` 898` ```lemma orthogonal_transformation: "orthogonal_transformation f \ linear f \ (\(v::real ^'n). norm (f v) = norm v)" ``` chaieb@29846 ` 899` ``` unfolding orthogonal_transformation_def ``` chaieb@29846 ` 900` ``` apply auto ``` chaieb@29846 ` 901` ``` apply (erule_tac x=v in allE)+ ``` chaieb@29846 ` 902` ``` apply (simp add: real_vector_norm_def) ``` chaieb@29846 ` 903` ``` by (simp add: dot_norm linear_add[symmetric]) ``` chaieb@29846 ` 904` chaieb@29846 ` 905` ```definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \ transp Q ** Q = mat 1 \ Q ** transp Q = mat 1" ``` chaieb@29846 ` 906` chaieb@29846 ` 907` ```lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transp Q ** Q = mat 1" ``` chaieb@29846 ` 908` ``` by (metis matrix_left_right_inverse orthogonal_matrix_def) ``` chaieb@29846 ` 909` chaieb@29846 ` 910` ```lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1)" ``` chaieb@29846 ` 911` ``` by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid) ``` chaieb@29846 ` 912` chaieb@29846 ` 913` ```lemma orthogonal_matrix_mul: ``` chaieb@29846 ` 914` ``` fixes A :: "real ^'n^'n" ``` chaieb@29846 ` 915` ``` assumes oA : "orthogonal_matrix A" ``` chaieb@29846 ` 916` ``` and oB: "orthogonal_matrix B" ``` chaieb@29846 ` 917` ``` shows "orthogonal_matrix(A ** B)" ``` chaieb@29846 ` 918` ``` using oA oB ``` chaieb@29846 ` 919` ``` unfolding orthogonal_matrix matrix_transp_mul ``` chaieb@29846 ` 920` ``` apply (subst matrix_mul_assoc) ``` chaieb@29846 ` 921` ``` apply (subst matrix_mul_assoc[symmetric]) ``` chaieb@29846 ` 922` ``` by (simp add: matrix_mul_rid) ``` chaieb@29846 ` 923` chaieb@29846 ` 924` ```lemma orthogonal_transformation_matrix: ``` chaieb@29846 ` 925` ``` fixes f:: "real^'n \ real^'n" ``` chaieb@29846 ` 926` ``` shows "orthogonal_transformation f \ linear f \ orthogonal_matrix(matrix f)" ``` chaieb@29846 ` 927` ``` (is "?lhs \ ?rhs") ``` chaieb@29846 ` 928` ```proof- ``` chaieb@29846 ` 929` ``` let ?mf = "matrix f" ``` chaieb@29846 ` 930` ``` let ?ot = "orthogonal_transformation f" ``` chaieb@29846 ` 931` ``` let ?U = "{1 .. dimindex (UNIV :: 'n set)}" ``` chaieb@29846 ` 932` ``` have fU: "finite ?U" by simp ``` chaieb@29846 ` 933` ``` let ?m1 = "mat 1 :: real ^'n^'n" ``` chaieb@29846 ` 934` ``` {assume ot: ?ot ``` chaieb@29846 ` 935` ``` from ot have lf: "linear f" and fd: "\v w. f v \ f w = v \ w" ``` chaieb@29846 ` 936` ``` unfolding orthogonal_transformation_def orthogonal_matrix by blast+ ``` chaieb@29846 ` 937` ``` {fix i j assume i: "i \ ?U" and j: "j \ ?U" ``` chaieb@29846 ` 938` ``` let ?A = "transp ?mf ** ?mf" ``` chaieb@29846 ` 939` ``` have th0: "\b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" ``` chaieb@29846 ` 940` ``` "\b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" ``` chaieb@29846 ` 941` ``` by simp_all ``` chaieb@29846 ` 942` ``` from fd[rule_format, of "basis i" "basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] i j ``` chaieb@29846 ` 943` ``` have "?A\$i\$j = ?m1 \$ i \$ j" ``` chaieb@29846 ` 944` ``` by (simp add: Cart_lambda_beta' dot_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def del: One_nat_def)} ``` chaieb@29846 ` 945` ``` hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector ``` chaieb@29846 ` 946` ``` with lf have ?rhs by blast} ``` chaieb@29846 ` 947` ``` moreover ``` chaieb@29846 ` 948` ``` {assume lf: "linear f" and om: "orthogonal_matrix ?mf" ``` chaieb@29846 ` 949` ``` from lf om have ?lhs ``` chaieb@29846 ` 950` ``` unfolding orthogonal_matrix_def norm_eq orthogonal_transformation ``` chaieb@29846 ` 951` ``` unfolding matrix_works[OF lf, symmetric] ``` chaieb@29846 ` 952` ``` apply (subst dot_matrix_vector_mul) ``` chaieb@29846 ` 953` ``` by (simp add: dot_matrix_product matrix_mul_lid del: One_nat_def)} ``` chaieb@29846 ` 954` ``` ultimately show ?thesis by blast ``` chaieb@29846 ` 955` ```qed ``` chaieb@29846 ` 956` chaieb@29846 ` 957` ```lemma det_orthogonal_matrix: ``` chaieb@29846 ` 958` ``` fixes Q:: "'a::ordered_idom^'n^'n" ``` chaieb@29846 ` 959` ``` assumes oQ: "orthogonal_matrix Q" ``` chaieb@29846 ` 960` ``` shows "det Q = 1 \ det Q = - 1" ``` chaieb@29846 ` 961` ```proof- ``` chaieb@29846 ` 962` ``` ``` chaieb@29846 ` 963` ``` have th: "\x::'a. x = 1 \ x = - 1 \ x*x = 1" (is "\x::'a. ?ths x") ``` chaieb@29846 ` 964` ``` proof- ``` chaieb@29846 ` 965` ``` fix x:: 'a ``` chaieb@29846 ` 966` ``` have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: ring_simps) ``` chaieb@29846 ` 967` ``` have th1: "\(x::'a) y. x = - y \ x + y = 0" ``` chaieb@29846 ` 968` ``` apply (subst eq_iff_diff_eq_0) by simp ``` chaieb@29846 ` 969` ``` have "x*x = 1 \ x*x - 1 = 0" by simp ``` chaieb@29846 ` 970` ``` also have "\ \ x = 1 \ x = - 1" unfolding th0 th1 by simp ``` chaieb@29846 ` 971` ``` finally show "?ths x" .. ``` chaieb@29846 ` 972` ``` qed ``` chaieb@29846 ` 973` ``` from oQ have "Q ** transp Q = mat 1" by (metis orthogonal_matrix_def) ``` chaieb@29846 ` 974` ``` hence "det (Q ** transp Q) = det (mat 1:: 'a^'n^'n)" by simp ``` chaieb@29846 ` 975` ``` hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transp) ``` chaieb@29846 ` 976` ``` then show ?thesis unfolding th . ``` chaieb@29846 ` 977` ```qed ``` chaieb@29846 ` 978` chaieb@29846 ` 979` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 980` ```(* Linearity of scaling, and hence isometry, that preserves origin. *) ``` chaieb@29846 ` 981` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 982` ```lemma scaling_linear: ``` chaieb@29846 ` 983` ``` fixes f :: "real ^'n \ real ^'n" ``` chaieb@29846 ` 984` ``` assumes f0: "f 0 = 0" and fd: "\x y. dist (f x) (f y) = c * dist x y" ``` chaieb@29846 ` 985` ``` shows "linear f" ``` chaieb@29846 ` 986` ```proof- ``` chaieb@29846 ` 987` ``` {fix v w ``` chaieb@29846 ` 988` ``` {fix x note fd[rule_format, of x 0, unfolded dist_def f0 diff_0_right] } ``` chaieb@29846 ` 989` ``` note th0 = this ``` chaieb@29846 ` 990` ``` have "f v \ f w = c^2 * (v \ w)" ``` chaieb@29846 ` 991` ``` unfolding dot_norm_neg dist_def[symmetric] ``` chaieb@29846 ` 992` ``` unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} ``` chaieb@29846 ` 993` ``` note fc = this ``` chaieb@29846 ` 994` ``` show ?thesis unfolding linear_def vector_eq ``` chaieb@29846 ` 995` ``` by (simp add: dot_lmult dot_ladd dot_rmult dot_radd fc ring_simps) ``` chaieb@29846 ` 996` ```qed ``` chaieb@29846 ` 997` chaieb@29846 ` 998` ```lemma isometry_linear: ``` chaieb@29846 ` 999` ``` "f (0:: real^'n) = (0:: real^'n) \ \x y. dist(f x) (f y) = dist x y ``` chaieb@29846 ` 1000` ``` \ linear f" ``` chaieb@29846 ` 1001` ```by (rule scaling_linear[where c=1]) simp_all ``` chaieb@29846 ` 1002` chaieb@29846 ` 1003` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 1004` ```(* Hence another formulation of orthogonal transformation. *) ``` chaieb@29846 ` 1005` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 1006` chaieb@29846 ` 1007` ```lemma orthogonal_transformation_isometry: ``` chaieb@29846 ` 1008` ``` "orthogonal_transformation f \ f(0::real^'n) = (0::real^'n) \ (\x y. dist(f x) (f y) = dist x y)" ``` chaieb@29846 ` 1009` ``` unfolding orthogonal_transformation ``` chaieb@29846 ` 1010` ``` apply (rule iffI) ``` chaieb@29846 ` 1011` ``` apply clarify ``` chaieb@29846 ` 1012` ``` apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_def) ``` chaieb@29846 ` 1013` ``` apply (rule conjI) ``` chaieb@29846 ` 1014` ``` apply (rule isometry_linear) ``` chaieb@29846 ` 1015` ``` apply simp ``` chaieb@29846 ` 1016` ``` apply simp ``` chaieb@29846 ` 1017` ``` apply clarify ``` chaieb@29846 ` 1018` ``` apply (erule_tac x=v in allE) ``` chaieb@29846 ` 1019` ``` apply (erule_tac x=0 in allE) ``` chaieb@29846 ` 1020` ``` by (simp add: dist_def) ``` chaieb@29846 ` 1021` chaieb@29846 ` 1022` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 1023` ```(* Can extend an isometry from unit sphere. *) ``` chaieb@29846 ` 1024` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 1025` chaieb@29846 ` 1026` ```lemma isometry_sphere_extend: ``` chaieb@29846 ` 1027` ``` fixes f:: "real ^'n \ real ^'n" ``` chaieb@29846 ` 1028` ``` assumes f1: "\x. norm x = 1 \ norm (f x) = 1" ``` chaieb@29846 ` 1029` ``` and fd1: "\ x y. norm x = 1 \ norm y = 1 \ dist (f x) (f y) = dist x y" ``` chaieb@29846 ` 1030` ``` shows "\g. orthogonal_transformation g \ (\x. norm x = 1 \ g x = f x)" ``` chaieb@29846 ` 1031` ```proof- ``` chaieb@29846 ` 1032` ``` {fix x y x' y' x0 y0 x0' y0' :: "real ^'n" ``` chaieb@29846 ` 1033` ``` assume H: "x = norm x *s x0" "y = norm y *s y0" ``` chaieb@29846 ` 1034` ``` "x' = norm x *s x0'" "y' = norm y *s y0'" ``` chaieb@29846 ` 1035` ``` "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1" ``` chaieb@29846 ` 1036` ``` "norm(x0' - y0') = norm(x0 - y0)" ``` chaieb@29846 ` 1037` ``` ``` chaieb@29846 ` 1038` ``` have "norm(x' - y') = norm(x - y)" ``` chaieb@29846 ` 1039` ``` apply (subst H(1)) ``` chaieb@29846 ` 1040` ``` apply (subst H(2)) ``` chaieb@29846 ` 1041` ``` apply (subst H(3)) ``` chaieb@29846 ` 1042` ``` apply (subst H(4)) ``` chaieb@29846 ` 1043` ``` using H(5-9) ``` chaieb@29846 ` 1044` ``` apply (simp add: norm_eq norm_eq_1) ``` chaieb@29846 ` 1045` ``` apply (simp add: dot_lsub dot_rsub dot_lmult dot_rmult) ``` chaieb@29846 ` 1046` ``` apply (simp add: ring_simps) ``` chaieb@29846 ` 1047` ``` by (simp only: right_distrib[symmetric])} ``` chaieb@29846 ` 1048` ``` note th0 = this ``` chaieb@29846 ` 1049` ``` let ?g = "\x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)" ``` chaieb@29846 ` 1050` ``` {fix x:: "real ^'n" assume nx: "norm x = 1" ``` chaieb@29846 ` 1051` ``` have "?g x = f x" using nx by (simp add: norm_eq_0[symmetric])} ``` chaieb@29846 ` 1052` ``` hence thfg: "\x. norm x = 1 \ ?g x = f x" by blast ``` chaieb@29846 ` 1053` ``` have g0: "?g 0 = 0" by simp ``` chaieb@29846 ` 1054` ``` {fix x y :: "real ^'n" ``` chaieb@29846 ` 1055` ``` {assume "x = 0" "y = 0" ``` chaieb@29846 ` 1056` ``` then have "dist (?g x) (?g y) = dist x y" by simp } ``` chaieb@29846 ` 1057` ``` moreover ``` chaieb@29846 ` 1058` ``` {assume "x = 0" "y \ 0" ``` chaieb@29846 ` 1059` ``` then have "dist (?g x) (?g y) = dist x y" ``` chaieb@29846 ` 1060` ``` apply (simp add: dist_def norm_neg norm_mul norm_eq_0) ``` chaieb@29846 ` 1061` ``` apply (rule f1[rule_format]) ``` chaieb@29846 ` 1062` ``` by(simp add: norm_mul norm_eq_0 field_simps)} ``` chaieb@29846 ` 1063` ``` moreover ``` chaieb@29846 ` 1064` ``` {assume "x \ 0" "y = 0" ``` chaieb@29846 ` 1065` ``` then have "dist (?g x) (?g y) = dist x y" ``` chaieb@29846 ` 1066` ``` apply (simp add: dist_def norm_neg norm_mul norm_eq_0) ``` chaieb@29846 ` 1067` ``` apply (rule f1[rule_format]) ``` chaieb@29846 ` 1068` ``` by(simp add: norm_mul norm_eq_0 field_simps)} ``` chaieb@29846 ` 1069` ``` moreover ``` chaieb@29846 ` 1070` ``` {assume z: "x \ 0" "y \ 0" ``` chaieb@29846 ` 1071` ``` 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)" ``` chaieb@29846 ` 1072` ``` "norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)" ``` chaieb@29846 ` 1073` ``` "norm (inverse (norm x) *s x) = 1" ``` chaieb@29846 ` 1074` ``` "norm (f (inverse (norm x) *s x)) = 1" ``` chaieb@29846 ` 1075` ``` "norm (inverse (norm y) *s y) = 1" ``` chaieb@29846 ` 1076` ``` "norm (f (inverse (norm y) *s y)) = 1" ``` chaieb@29846 ` 1077` ``` "norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) = ``` chaieb@29846 ` 1078` ``` norm (inverse (norm x) *s x - inverse (norm y) *s y)" ``` chaieb@29846 ` 1079` ``` using z ``` chaieb@29846 ` 1080` ``` by (auto simp add: norm_eq_0 vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def]) ``` chaieb@29846 ` 1081` ``` from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" ``` chaieb@29846 ` 1082` ``` by (simp add: dist_def)} ``` chaieb@29846 ` 1083` ``` ultimately have "dist (?g x) (?g y) = dist x y" by blast} ``` chaieb@29846 ` 1084` ``` note thd = this ``` chaieb@29846 ` 1085` ``` show ?thesis ``` chaieb@29846 ` 1086` ``` apply (rule exI[where x= ?g]) ``` chaieb@29846 ` 1087` ``` unfolding orthogonal_transformation_isometry ``` chaieb@29846 ` 1088` ``` using g0 thfg thd by metis ``` chaieb@29846 ` 1089` ```qed ``` chaieb@29846 ` 1090` chaieb@29846 ` 1091` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 1092` ```(* Rotation, reflection, rotoinversion. *) ``` chaieb@29846 ` 1093` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 1094` chaieb@29846 ` 1095` ```definition "rotation_matrix Q \ orthogonal_matrix Q \ det Q = 1" ``` chaieb@29846 ` 1096` ```definition "rotoinversion_matrix Q \ orthogonal_matrix Q \ det Q = - 1" ``` chaieb@29846 ` 1097` chaieb@29846 ` 1098` ```lemma orthogonal_rotation_or_rotoinversion: ``` chaieb@29846 ` 1099` ``` fixes Q :: "'a::ordered_idom^'n^'n" ``` chaieb@29846 ` 1100` ``` shows " orthogonal_matrix Q \ rotation_matrix Q \ rotoinversion_matrix Q" ``` chaieb@29846 ` 1101` ``` by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) ``` chaieb@29846 ` 1102` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 1103` ```(* Explicit formulas for low dimensions. *) ``` chaieb@29846 ` 1104` ```(* ------------------------------------------------------------------------- *) ``` chaieb@29846 ` 1105` chaieb@29846 ` 1106` ```lemma setprod_1: "setprod f {(1::nat)..1} = f 1" by simp ``` chaieb@29846 ` 1107` chaieb@29846 ` 1108` ```lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2" ``` chaieb@29846 ` 1109` ``` by (simp add: nat_number setprod_numseg mult_commute) ``` chaieb@29846 ` 1110` ```lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3" ``` chaieb@29846 ` 1111` ``` by (simp add: nat_number setprod_numseg mult_commute) ``` chaieb@29846 ` 1112` chaieb@29846 ` 1113` ```lemma det_1: "det (A::'a::comm_ring_1^1^1) = A\$1\$1" ``` chaieb@29846 ` 1114` ``` by (simp add: det_def dimindex_def permutes_sing sign_id del: One_nat_def) ``` chaieb@29846 ` 1115` chaieb@29846 ` 1116` ```lemma det_2: "det (A::'a::comm_ring_1^2^2) = A\$1\$1 * A\$2\$2 - A\$1\$2 * A\$2\$1" ``` chaieb@29846 ` 1117` ```proof- ``` chaieb@29846 ` 1118` ``` have f12: "finite {2::nat}" "1 \ {2::nat}" by auto ``` chaieb@29846 ` 1119` ``` have th12: "{1 .. 2} = insert (1::nat) {2}" by auto ``` chaieb@29846 ` 1120` ``` show ?thesis ``` chaieb@29846 ` 1121` ``` apply (simp add: det_def dimindex_def th12 del: One_nat_def) ``` chaieb@29846 ` 1122` ``` unfolding setsum_over_permutations_insert[OF f12] ``` chaieb@29846 ` 1123` ``` unfolding permutes_sing ``` chaieb@29846 ` 1124` ``` apply (simp add: sign_swap_id sign_id swap_id_eq del: One_nat_def) ``` chaieb@29846 ` 1125` ``` by (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31)) ``` chaieb@29846 ` 1126` ```qed ``` chaieb@29846 ` 1127` chaieb@29846 ` 1128` ```lemma det_3: "det (A::'a::comm_ring_1^3^3) = ``` chaieb@29846 ` 1129` ``` A\$1\$1 * A\$2\$2 * A\$3\$3 + ``` chaieb@29846 ` 1130` ``` A\$1\$2 * A\$2\$3 * A\$3\$1 + ``` chaieb@29846 ` 1131` ``` A\$1\$3 * A\$2\$1 * A\$3\$2 - ``` chaieb@29846 ` 1132` ``` A\$1\$1 * A\$2\$3 * A\$3\$2 - ``` chaieb@29846 ` 1133` ``` A\$1\$2 * A\$2\$1 * A\$3\$3 - ``` chaieb@29846 ` 1134` ``` A\$1\$3 * A\$2\$2 * A\$3\$1" ``` chaieb@29846 ` 1135` ```proof- ``` chaieb@29846 ` 1136` ``` have f123: "finite {(2::nat), 3}" "1 \ {(2::nat), 3}" by auto ``` chaieb@29846 ` 1137` ``` have f23: "finite {(3::nat)}" "2 \ {(3::nat)}" by auto ``` chaieb@29846 ` 1138` ``` have th12: "{1 .. 3} = insert (1::nat) (insert 2 {3})" by auto ``` chaieb@29846 ` 1139` chaieb@29846 ` 1140` ``` show ?thesis ``` chaieb@29846 ` 1141` ``` apply (simp add: det_def dimindex_def th12 del: One_nat_def) ``` chaieb@29846 ` 1142` ``` unfolding setsum_over_permutations_insert[OF f123] ``` chaieb@29846 ` 1143` ``` unfolding setsum_over_permutations_insert[OF f23] ``` chaieb@29846 ` 1144` chaieb@29846 ` 1145` ``` unfolding permutes_sing ``` chaieb@29846 ` 1146` ``` apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq del: One_nat_def) ``` chaieb@29846 ` 1147` ``` apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31) One_nat_def) ``` chaieb@29846 ` 1148` ``` by (simp add: ring_simps) ``` chaieb@29846 ` 1149` ```qed ``` chaieb@29846 ` 1150` chaieb@29846 ` 1151` `end`