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