author | nipkow |
Tue, 05 Nov 2019 21:07:03 +0100 | |
changeset 71044 | cb504351d058 |
parent 70136 | f03a01a18c6e |
child 73477 | 1d8a79aa2a99 |
permissions | -rw-r--r-- |
63627 | 1 |
(* Title: HOL/Analysis/Determinants.thy |
68143 | 2 |
Author: Amine Chaieb, University of Cambridge; proofs reworked by LCP |
33175 | 3 |
*) |
4 |
||
71044 | 5 |
section \<open>Traces and Determinants of Square Matrices\<close> |
33175 | 6 |
|
7 |
theory Determinants |
|
44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset
|
8 |
imports |
69680 | 9 |
Cartesian_Space |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
64272
diff
changeset
|
10 |
"HOL-Library.Permutations" |
33175 | 11 |
begin |
12 |
||
69683 | 13 |
subsection \<open>Trace\<close> |
33175 | 14 |
|
70136 | 15 |
definition\<^marker>\<open>tag important\<close> trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" |
64267 | 16 |
where "trace A = sum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)" |
33175 | 17 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
18 |
lemma trace_0: "trace (mat 0) = 0" |
33175 | 19 |
by (simp add: trace_def mat_def) |
20 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
21 |
lemma trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))" |
33175 | 22 |
by (simp add: trace_def mat_def) |
23 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
24 |
lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" |
64267 | 25 |
by (simp add: trace_def sum.distrib) |
33175 | 26 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
27 |
lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B" |
64267 | 28 |
by (simp add: trace_def sum_subtractf) |
33175 | 29 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
30 |
lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)" |
33175 | 31 |
apply (simp add: trace_def matrix_matrix_mult_def) |
66804
3f9bb52082c4
avoid name clashes on interpretation of abstract locales
haftmann
parents:
66453
diff
changeset
|
32 |
apply (subst sum.swap) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
33 |
apply (simp add: mult.commute) |
53253 | 34 |
done |
33175 | 35 |
|
70136 | 36 |
subsubsection\<^marker>\<open>tag important\<close> \<open>Definition of determinant\<close> |
33175 | 37 |
|
70136 | 38 |
definition\<^marker>\<open>tag important\<close> det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where |
53253 | 39 |
"det A = |
64272 | 40 |
sum (\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)) |
53253 | 41 |
{p. p permutes (UNIV :: 'n set)}" |
33175 | 42 |
|
68134 | 43 |
text \<open>Basic determinant properties\<close> |
33175 | 44 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
45 |
lemma det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" |
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
46 |
proof - |
33175 | 47 |
let ?di = "\<lambda>A i j. A$i$j" |
48 |
let ?U = "(UNIV :: 'n set)" |
|
49 |
have fU: "finite ?U" by simp |
|
53253 | 50 |
{ |
51 |
fix p |
|
52 |
assume p: "p \<in> {p. p permutes ?U}" |
|
53854 | 53 |
from p have pU: "p permutes ?U" |
54 |
by blast |
|
33175 | 55 |
have sth: "sign (inv p) = sign p" |
44260
7784fa3232ce
Determinants.thy: avoid using mem_def/Collect_def
huffman
parents:
44228
diff
changeset
|
56 |
by (metis sign_inverse fU p mem_Collect_eq permutation_permutes) |
33175 | 57 |
from permutes_inj[OF pU] |
53854 | 58 |
have pi: "inj_on p ?U" |
59 |
by (blast intro: subset_inj_on) |
|
33175 | 60 |
from permutes_image[OF pU] |
64272 | 61 |
have "prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U = |
62 |
prod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)" |
|
53854 | 63 |
by simp |
64272 | 64 |
also have "\<dots> = prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U" |
65 |
unfolding prod.reindex[OF pi] .. |
|
66 |
also have "\<dots> = prod (\<lambda>i. ?di A i (p i)) ?U" |
|
53253 | 67 |
proof - |
68134 | 68 |
have "((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) i = ?di A i (p i)" if "i \<in> ?U" for i |
69 |
using that permutes_inv_o[OF pU] permutes_in_image[OF pU] |
|
70 |
unfolding transpose_def by (simp add: fun_eq_iff) |
|
71 |
then show "prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U = prod (\<lambda>i. ?di A i (p i)) ?U" |
|
64272 | 72 |
by (auto intro: prod.cong) |
33175 | 73 |
qed |
64272 | 74 |
finally have "of_int (sign (inv p)) * (prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = |
75 |
of_int (sign p) * (prod (\<lambda>i. ?di A i (p i)) ?U)" |
|
53854 | 76 |
using sth by simp |
53253 | 77 |
} |
78 |
then show ?thesis |
|
79 |
unfolding det_def |
|
68138 | 80 |
by (subst sum_permutations_inverse) (blast intro: sum.cong) |
33175 | 81 |
qed |
82 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
83 |
lemma det_lowerdiagonal: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
84 |
fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})" |
33175 | 85 |
assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0" |
64272 | 86 |
shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)" |
53253 | 87 |
proof - |
33175 | 88 |
let ?U = "UNIV:: 'n set" |
89 |
let ?PU = "{p. p permutes ?U}" |
|
64272 | 90 |
let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" |
53854 | 91 |
have fU: "finite ?U" |
92 |
by simp |
|
93 |
have id0: "{id} \<subseteq> ?PU" |
|
68138 | 94 |
by (auto simp: permutes_id) |
68134 | 95 |
have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0" |
96 |
proof |
|
53253 | 97 |
fix p |
68134 | 98 |
assume "p \<in> ?PU - {id}" |
99 |
then obtain i where i: "p i > i" |
|
100 |
by clarify (meson leI permutes_natset_le) |
|
101 |
from ld[OF i] have "\<exists>i \<in> ?U. A$i$p i = 0" |
|
53253 | 102 |
by blast |
68134 | 103 |
with prod_zero[OF fU] show "?pp p = 0" |
104 |
by force |
|
105 |
qed |
|
106 |
from sum.mono_neutral_cong_left[OF finite_permutations[OF fU] id0 p0] show ?thesis |
|
33175 | 107 |
unfolding det_def by (simp add: sign_id) |
108 |
qed |
|
109 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
110 |
lemma det_upperdiagonal: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
111 |
fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}" |
33175 | 112 |
assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0" |
64272 | 113 |
shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)" |
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
114 |
proof - |
33175 | 115 |
let ?U = "UNIV:: 'n set" |
116 |
let ?PU = "{p. p permutes ?U}" |
|
64272 | 117 |
let ?pp = "(\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))" |
53854 | 118 |
have fU: "finite ?U" |
119 |
by simp |
|
120 |
have id0: "{id} \<subseteq> ?PU" |
|
68138 | 121 |
by (auto simp: permutes_id) |
68134 | 122 |
have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0" |
123 |
proof |
|
53253 | 124 |
fix p |
53854 | 125 |
assume p: "p \<in> ?PU - {id}" |
68134 | 126 |
then obtain i where i: "p i < i" |
127 |
by clarify (meson leI permutes_natset_ge) |
|
128 |
from ld[OF i] have "\<exists>i \<in> ?U. A$i$p i = 0" |
|
53854 | 129 |
by blast |
68134 | 130 |
with prod_zero[OF fU] show "?pp p = 0" |
131 |
by force |
|
132 |
qed |
|
133 |
from sum.mono_neutral_cong_left[OF finite_permutations[OF fU] id0 p0] show ?thesis |
|
33175 | 134 |
unfolding det_def by (simp add: sign_id) |
135 |
qed |
|
136 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
137 |
proposition det_diagonal: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
138 |
fixes A :: "'a::comm_ring_1^'n^'n" |
33175 | 139 |
assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0" |
64272 | 140 |
shows "det A = prod (\<lambda>i. A$i$i) (UNIV::'n set)" |
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
141 |
proof - |
33175 | 142 |
let ?U = "UNIV:: 'n set" |
143 |
let ?PU = "{p. p permutes ?U}" |
|
64272 | 144 |
let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" |
33175 | 145 |
have fU: "finite ?U" by simp |
146 |
from finite_permutations[OF fU] have fPU: "finite ?PU" . |
|
53854 | 147 |
have id0: "{id} \<subseteq> ?PU" |
68138 | 148 |
by (auto simp: permutes_id) |
68134 | 149 |
have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0" |
150 |
proof |
|
53253 | 151 |
fix p |
152 |
assume p: "p \<in> ?PU - {id}" |
|
53854 | 153 |
then obtain i where i: "p i \<noteq> i" |
68134 | 154 |
by fastforce |
155 |
with ld have "\<exists>i \<in> ?U. A$i$p i = 0" |
|
156 |
by (metis UNIV_I) |
|
157 |
with prod_zero [OF fU] show "?pp p = 0" |
|
158 |
by force |
|
159 |
qed |
|
64267 | 160 |
from sum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis |
33175 | 161 |
unfolding det_def by (simp add: sign_id) |
162 |
qed |
|
163 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
164 |
lemma det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
165 |
by (simp add: det_diagonal mat_def) |
33175 | 166 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
167 |
lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" |
67970 | 168 |
by (simp add: det_def prod_zero power_0_left) |
33175 | 169 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
170 |
lemma det_permute_rows: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
171 |
fixes A :: "'a::comm_ring_1^'n^'n" |
33175 | 172 |
assumes p: "p permutes (UNIV :: 'n::finite set)" |
53854 | 173 |
shows "det (\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" |
68134 | 174 |
proof - |
33175 | 175 |
let ?U = "UNIV :: 'n set" |
176 |
let ?PU = "{p. p permutes ?U}" |
|
68134 | 177 |
have *: "(\<Sum>q\<in>?PU. of_int (sign (q \<circ> p)) * (\<Prod>i\<in>?U. A $ p i $ (q \<circ> p) i)) = |
178 |
(\<Sum>n\<in>?PU. of_int (sign p) * of_int (sign n) * (\<Prod>i\<in>?U. A $ i $ n i))" |
|
179 |
proof (rule sum.cong) |
|
180 |
fix q |
|
181 |
assume qPU: "q \<in> ?PU" |
|
182 |
have fU: "finite ?U" |
|
183 |
by simp |
|
184 |
from qPU have q: "q permutes ?U" |
|
185 |
by blast |
|
186 |
have "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod ((\<lambda>i. A$p i$(q \<circ> p) i) \<circ> inv p) ?U" |
|
187 |
by (simp only: prod.permute[OF permutes_inv[OF p], symmetric]) |
|
188 |
also have "\<dots> = prod (\<lambda>i. A $ (p \<circ> inv p) i $ (q \<circ> (p \<circ> inv p)) i) ?U" |
|
189 |
by (simp only: o_def) |
|
190 |
also have "\<dots> = prod (\<lambda>i. A$i$q i) ?U" |
|
191 |
by (simp only: o_def permutes_inverses[OF p]) |
|
192 |
finally have thp: "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod (\<lambda>i. A$i$q i) ?U" |
|
193 |
by blast |
|
194 |
from p q have pp: "permutation p" and qp: "permutation q" |
|
195 |
by (metis fU permutation_permutes)+ |
|
196 |
show "of_int (sign (q \<circ> p)) * prod (\<lambda>i. A$ p i$ (q \<circ> p) i) ?U = |
|
197 |
of_int (sign p) * of_int (sign q) * prod (\<lambda>i. A$i$q i) ?U" |
|
198 |
by (simp only: thp sign_compose[OF qp pp] mult.commute of_int_mult) |
|
199 |
qed auto |
|
200 |
show ?thesis |
|
201 |
apply (simp add: det_def sum_distrib_left mult.assoc[symmetric]) |
|
202 |
apply (subst sum_permutations_compose_right[OF p]) |
|
203 |
apply (rule *) |
|
204 |
done |
|
68143 | 205 |
qed |
33175 | 206 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
207 |
lemma det_permute_columns: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
208 |
fixes A :: "'a::comm_ring_1^'n^'n" |
33175 | 209 |
assumes p: "p permutes (UNIV :: 'n set)" |
210 |
shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
211 |
proof - |
33175 | 212 |
let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n" |
35150
082fa4bd403d
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset
|
213 |
let ?At = "transpose A" |
082fa4bd403d
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset
|
214 |
have "of_int (sign p) * det A = det (transpose (\<chi> i. transpose A $ p i))" |
082fa4bd403d
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset
|
215 |
unfolding det_permute_rows[OF p, of ?At] det_transpose .. |
33175 | 216 |
moreover |
35150
082fa4bd403d
Rename transp to transpose in HOL-Multivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset
|
217 |
have "?Ap = transpose (\<chi> i. transpose A $ p i)" |
44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset
|
218 |
by (simp add: transpose_def vec_eq_iff) |
53854 | 219 |
ultimately show ?thesis |
220 |
by simp |
|
33175 | 221 |
qed |
222 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
223 |
lemma det_identical_columns: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
224 |
fixes A :: "'a::comm_ring_1^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
225 |
assumes jk: "j \<noteq> k" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
226 |
and r: "column j A = column k A" |
33175 | 227 |
shows "det A = 0" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
228 |
proof - |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
229 |
let ?U="UNIV::'n set" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
230 |
let ?t_jk="Fun.swap j k id" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
231 |
let ?PU="{p. p permutes ?U}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
232 |
let ?S1="{p. p\<in>?PU \<and> evenperm p}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
233 |
let ?S2="{(?t_jk \<circ> p) |p. p \<in>?S1}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
234 |
let ?f="\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
235 |
let ?g="\<lambda>p. ?t_jk \<circ> p" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
236 |
have g_S1: "?S2 = ?g` ?S1" by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
237 |
have inj_g: "inj_on ?g ?S1" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
238 |
proof (unfold inj_on_def, auto) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
239 |
fix x y assume x: "x permutes ?U" and even_x: "evenperm x" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
240 |
and y: "y permutes ?U" and even_y: "evenperm y" and eq: "?t_jk \<circ> x = ?t_jk \<circ> y" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
241 |
show "x = y" by (metis (hide_lams, no_types) comp_assoc eq id_comp swap_id_idempotent) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
242 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
243 |
have tjk_permutes: "?t_jk permutes ?U" unfolding permutes_def swap_id_eq by (auto,metis) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
244 |
have tjk_eq: "\<forall>i l. A $ i $ ?t_jk l = A $ i $ l" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
245 |
using r jk |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
246 |
unfolding column_def vec_eq_iff swap_id_eq by fastforce |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
247 |
have sign_tjk: "sign ?t_jk = -1" using sign_swap_id[of j k] jk by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
248 |
{fix x |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
249 |
assume x: "x\<in> ?S1" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
250 |
have "sign (?t_jk \<circ> x) = sign (?t_jk) * sign x" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
251 |
by (metis (lifting) finite_class.finite_UNIV mem_Collect_eq |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
252 |
permutation_permutes permutation_swap_id sign_compose x) |
68138 | 253 |
also have "\<dots> = - sign x" using sign_tjk by simp |
254 |
also have "\<dots> \<noteq> sign x" unfolding sign_def by simp |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
255 |
finally have "sign (?t_jk \<circ> x) \<noteq> sign x" and "(?t_jk \<circ> x) \<in> ?S2" |
68134 | 256 |
using x by force+ |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
257 |
} |
68134 | 258 |
hence disjoint: "?S1 \<inter> ?S2 = {}" |
259 |
by (force simp: sign_def) |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
260 |
have PU_decomposition: "?PU = ?S1 \<union> ?S2" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
261 |
proof (auto) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
262 |
fix x |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
263 |
assume x: "x permutes ?U" and "\<forall>p. p permutes ?U \<longrightarrow> x = Fun.swap j k id \<circ> p \<longrightarrow> \<not> evenperm p" |
68134 | 264 |
then obtain p where p: "p permutes UNIV" and x_eq: "x = Fun.swap j k id \<circ> p" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
265 |
and odd_p: "\<not> evenperm p" |
68134 | 266 |
by (metis (mono_tags) id_o o_assoc permutes_compose swap_id_idempotent tjk_permutes) |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
267 |
thus "evenperm x" |
68134 | 268 |
by (meson evenperm_comp evenperm_swap finite_class.finite_UNIV |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
269 |
jk permutation_permutes permutation_swap_id) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
270 |
next |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
271 |
fix p assume p: "p permutes ?U" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
272 |
show "Fun.swap j k id \<circ> p permutes UNIV" by (metis p permutes_compose tjk_permutes) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
273 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
274 |
have "sum ?f ?S2 = sum ((\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i)) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
275 |
\<circ> (\<circ>) (Fun.swap j k id)) {p \<in> {p. p permutes UNIV}. evenperm p}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
276 |
unfolding g_S1 by (rule sum.reindex[OF inj_g]) |
68138 | 277 |
also have "\<dots> = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1" |
278 |
unfolding o_def by (rule sum.cong, auto simp: tjk_eq) |
|
279 |
also have "\<dots> = sum (\<lambda>p. - ?f p) ?S1" |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
280 |
proof (rule sum.cong, auto) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
281 |
fix x assume x: "x permutes ?U" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
282 |
and even_x: "evenperm x" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
283 |
hence perm_x: "permutation x" and perm_tjk: "permutation ?t_jk" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
284 |
using permutation_permutes[of x] permutation_permutes[of ?t_jk] permutation_swap_id |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
285 |
by (metis finite_code)+ |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
286 |
have "(sign (?t_jk \<circ> x)) = - (sign x)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
287 |
unfolding sign_compose[OF perm_tjk perm_x] sign_tjk by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
288 |
thus "of_int (sign (?t_jk \<circ> x)) * (\<Prod>i\<in>UNIV. A $ i $ x i) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
289 |
= - (of_int (sign x) * (\<Prod>i\<in>UNIV. A $ i $ x i))" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
290 |
by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
291 |
qed |
68138 | 292 |
also have "\<dots>= - sum ?f ?S1" unfolding sum_negf .. |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
293 |
finally have *: "sum ?f ?S2 = - sum ?f ?S1" . |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
294 |
have "det A = (\<Sum>p | p permutes UNIV. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
295 |
unfolding det_def .. |
68138 | 296 |
also have "\<dots>= sum ?f ?S1 + sum ?f ?S2" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
297 |
by (subst PU_decomposition, rule sum.union_disjoint[OF _ _ disjoint], auto) |
68138 | 298 |
also have "\<dots>= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto |
299 |
also have "\<dots>= 0" by simp |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
300 |
finally show "det A = 0" by simp |
33175 | 301 |
qed |
302 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
303 |
lemma det_identical_rows: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
304 |
fixes A :: "'a::comm_ring_1^'n^'n" |
68134 | 305 |
assumes ij: "i \<noteq> j" and r: "row i A = row j A" |
33175 | 306 |
shows "det A = 0" |
68134 | 307 |
by (metis column_transpose det_identical_columns det_transpose ij r) |
33175 | 308 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
309 |
lemma det_zero_row: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
310 |
fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
311 |
shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0" |
68138 | 312 |
by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+ |
33175 | 313 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
314 |
lemma det_zero_column: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
315 |
fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
316 |
shows "column i A = 0 \<Longrightarrow> det A = 0" and "column j F = 0 \<Longrightarrow> det F = 0" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
317 |
unfolding atomize_conj atomize_imp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
318 |
by (metis det_transpose det_zero_row row_transpose) |
33175 | 319 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
320 |
lemma det_row_add: |
33175 | 321 |
fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n" |
322 |
shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) = |
|
53253 | 323 |
det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) + |
324 |
det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)" |
|
64267 | 325 |
unfolding det_def vec_lambda_beta sum.distrib[symmetric] |
326 |
proof (rule sum.cong) |
|
33175 | 327 |
let ?U = "UNIV :: 'n set" |
328 |
let ?pU = "{p. p permutes ?U}" |
|
329 |
let ?f = "(\<lambda>i. if i = k then a i + b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
330 |
let ?g = "(\<lambda> i. if i = k then a i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
331 |
let ?h = "(\<lambda> i. if i = k then b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
53253 | 332 |
fix p |
333 |
assume p: "p \<in> ?pU" |
|
33175 | 334 |
let ?Uk = "?U - {k}" |
53854 | 335 |
from p have pU: "p permutes ?U" |
336 |
by blast |
|
337 |
have kU: "?U = insert k ?Uk" |
|
338 |
by blast |
|
68134 | 339 |
have eq: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk" |
340 |
"prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?h i $ p i) ?Uk" |
|
341 |
by auto |
|
342 |
have Uk: "finite ?Uk" "k \<notin> ?Uk" |
|
53854 | 343 |
by auto |
64272 | 344 |
have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" |
33175 | 345 |
unfolding kU[symmetric] .. |
64272 | 346 |
also have "\<dots> = ?f k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk" |
68134 | 347 |
by (rule prod.insert) auto |
64272 | 348 |
also have "\<dots> = (a k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * prod (\<lambda>i. ?f i $ p i) ?Uk)" |
53253 | 349 |
by (simp add: field_simps) |
64272 | 350 |
also have "\<dots> = (a k $ p k * prod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * prod (\<lambda>i. ?h i $ p i) ?Uk)" |
68134 | 351 |
by (metis eq) |
64272 | 352 |
also have "\<dots> = prod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + prod (\<lambda>i. ?h i $ p i) (insert k ?Uk)" |
68134 | 353 |
unfolding prod.insert[OF Uk] by simp |
64272 | 354 |
finally have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?g i $ p i) ?U + prod (\<lambda>i. ?h i $ p i) ?U" |
53854 | 355 |
unfolding kU[symmetric] . |
64272 | 356 |
then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U = |
357 |
of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * prod (\<lambda>i. ?h i $ p i) ?U" |
|
36350 | 358 |
by (simp add: field_simps) |
68134 | 359 |
qed auto |
33175 | 360 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
361 |
lemma det_row_mul: |
33175 | 362 |
fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n" |
363 |
shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) = |
|
53253 | 364 |
c * det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" |
64267 | 365 |
unfolding det_def vec_lambda_beta sum_distrib_left |
366 |
proof (rule sum.cong) |
|
33175 | 367 |
let ?U = "UNIV :: 'n set" |
368 |
let ?pU = "{p. p permutes ?U}" |
|
369 |
let ?f = "(\<lambda>i. if i = k then c*s a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
370 |
let ?g = "(\<lambda> i. if i = k then a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n" |
|
53253 | 371 |
fix p |
372 |
assume p: "p \<in> ?pU" |
|
33175 | 373 |
let ?Uk = "?U - {k}" |
53854 | 374 |
from p have pU: "p permutes ?U" |
375 |
by blast |
|
376 |
have kU: "?U = insert k ?Uk" |
|
377 |
by blast |
|
68134 | 378 |
have eq: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk" |
68138 | 379 |
by auto |
68134 | 380 |
have Uk: "finite ?Uk" "k \<notin> ?Uk" |
53854 | 381 |
by auto |
64272 | 382 |
have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" |
33175 | 383 |
unfolding kU[symmetric] .. |
64272 | 384 |
also have "\<dots> = ?f k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk" |
68134 | 385 |
by (rule prod.insert) auto |
64272 | 386 |
also have "\<dots> = (c*s a k) $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk" |
53253 | 387 |
by (simp add: field_simps) |
64272 | 388 |
also have "\<dots> = c* (a k $ p k * prod (\<lambda>i. ?g i $ p i) ?Uk)" |
68134 | 389 |
unfolding eq by (simp add: ac_simps) |
64272 | 390 |
also have "\<dots> = c* (prod (\<lambda>i. ?g i $ p i) (insert k ?Uk))" |
68134 | 391 |
unfolding prod.insert[OF Uk] by simp |
64272 | 392 |
finally have "prod (\<lambda>i. ?f i $ p i) ?U = c* (prod (\<lambda>i. ?g i $ p i) ?U)" |
53253 | 393 |
unfolding kU[symmetric] . |
68134 | 394 |
then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U = c * (of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U)" |
36350 | 395 |
by (simp add: field_simps) |
68134 | 396 |
qed auto |
33175 | 397 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
398 |
lemma det_row_0: |
33175 | 399 |
fixes b :: "'n::finite \<Rightarrow> _ ^ 'n" |
400 |
shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0" |
|
53253 | 401 |
using det_row_mul[of k 0 "\<lambda>i. 1" b] |
402 |
apply simp |
|
403 |
apply (simp only: vector_smult_lzero) |
|
404 |
done |
|
33175 | 405 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
406 |
lemma det_row_operation: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
407 |
fixes A :: "'a::{comm_ring_1}^'n^'n" |
33175 | 408 |
assumes ij: "i \<noteq> j" |
409 |
shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A" |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
410 |
proof - |
33175 | 411 |
let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n" |
412 |
have th: "row i ?Z = row j ?Z" by (vector row_def) |
|
413 |
have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A" |
|
414 |
by (vector row_def) |
|
415 |
show ?thesis |
|
416 |
unfolding det_row_add [of i] det_row_mul[of i] det_identical_rows[OF ij th] th2 |
|
417 |
by simp |
|
418 |
qed |
|
419 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
420 |
lemma det_row_span: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
421 |
fixes A :: "'a::{field}^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
422 |
assumes x: "x \<in> vec.span {row j A |j. j \<noteq> i}" |
33175 | 423 |
shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A" |
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
424 |
using x |
68074 | 425 |
proof (induction rule: vec.span_induct_alt) |
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
426 |
case base |
68134 | 427 |
have "(if k = i then row i A + 0 else row k A) = row k A" for k |
428 |
by simp |
|
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
429 |
then show ?case |
68134 | 430 |
by (simp add: row_def) |
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
431 |
next |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
432 |
case (step c z y) |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
433 |
then obtain j where j: "z = row j A" "i \<noteq> j" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
434 |
by blast |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
435 |
let ?w = "row i A + y" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
436 |
have th0: "row i A + (c*s z + y) = ?w + c*s z" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
437 |
by vector |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
438 |
let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
439 |
have thz: "?d z = 0" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
440 |
apply (rule det_identical_rows[OF j(2)]) |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
441 |
using j |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
442 |
apply (vector row_def) |
33175 | 443 |
done |
68069
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
444 |
have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
445 |
unfolding th0 .. |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
446 |
then have "?d (row i A + (c*s z + y)) = det A" |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
447 |
unfolding thz step.IH det_row_mul[of i] det_row_add[of i] by simp |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
448 |
then show ?case |
36209dfb981e
tidying up and using real induction methods
paulson <lp15@cam.ac.uk>
parents:
68050
diff
changeset
|
449 |
unfolding scalar_mult_eq_scaleR . |
68143 | 450 |
qed |
33175 | 451 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
452 |
lemma matrix_id [simp]: "det (matrix id) = 1" |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
453 |
by (simp add: matrix_id_mat_1) |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
454 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
455 |
proposition det_matrix_scaleR [simp]: "det (matrix (((*\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)" |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
456 |
apply (subst det_diagonal) |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
457 |
apply (auto simp: matrix_def mat_def) |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
458 |
apply (simp add: cart_eq_inner_axis inner_axis_axis) |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
459 |
done |
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
460 |
|
60420 | 461 |
text \<open> |
53854 | 462 |
May as well do this, though it's a bit unsatisfactory since it ignores |
463 |
exact duplicates by considering the rows/columns as a set. |
|
60420 | 464 |
\<close> |
33175 | 465 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
466 |
lemma det_dependent_rows: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
467 |
fixes A:: "'a::{field}^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
468 |
assumes d: "vec.dependent (rows A)" |
33175 | 469 |
shows "det A = 0" |
53253 | 470 |
proof - |
33175 | 471 |
let ?U = "UNIV :: 'n set" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
472 |
from d obtain i where i: "row i A \<in> vec.span (rows A - {row i A})" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
473 |
unfolding vec.dependent_def rows_def by blast |
68134 | 474 |
show ?thesis |
475 |
proof (cases "\<forall>i j. i \<noteq> j \<longrightarrow> row i A \<noteq> row j A") |
|
476 |
case True |
|
477 |
with i have "vec.span (rows A - {row i A}) \<subseteq> vec.span {row j A |j. j \<noteq> i}" |
|
68138 | 478 |
by (auto simp: rows_def intro!: vec.span_mono) |
68134 | 479 |
then have "- row i A \<in> vec.span {row j A|j. j \<noteq> i}" |
480 |
by (meson i subsetCE vec.span_neg) |
|
481 |
from det_row_span[OF this] |
|
33175 | 482 |
have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)" |
483 |
unfolding right_minus vector_smult_lzero .. |
|
68134 | 484 |
with det_row_mul[of i 0 "\<lambda>i. 1"] |
485 |
show ?thesis by simp |
|
486 |
next |
|
487 |
case False |
|
488 |
then obtain j k where jk: "j \<noteq> k" "row j A = row k A" |
|
489 |
by auto |
|
490 |
from det_identical_rows[OF jk] show ?thesis . |
|
491 |
qed |
|
33175 | 492 |
qed |
493 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
494 |
lemma det_dependent_columns: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
495 |
assumes d: "vec.dependent (columns (A::real^'n^'n))" |
53253 | 496 |
shows "det A = 0" |
497 |
by (metis d det_dependent_rows rows_transpose det_transpose) |
|
33175 | 498 |
|
68134 | 499 |
text \<open>Multilinearity and the multiplication formula\<close> |
33175 | 500 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
501 |
lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" |
68134 | 502 |
by auto |
33175 | 503 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
504 |
lemma det_linear_row_sum: |
33175 | 505 |
assumes fS: "finite S" |
64267 | 506 |
shows "det ((\<chi> i. if i = k then sum (a i) S else c i)::'a::comm_ring_1^'n^'n) = |
507 |
sum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S" |
|
68134 | 508 |
using fS by (induct rule: finite_induct; simp add: det_row_0 det_row_add cong: if_cong) |
33175 | 509 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
510 |
lemma finite_bounded_functions: |
33175 | 511 |
assumes fS: "finite S" |
512 |
shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}" |
|
53253 | 513 |
proof (induct k) |
33175 | 514 |
case 0 |
68134 | 515 |
have *: "{f. \<forall>i. f i = i} = {id}" |
53854 | 516 |
by auto |
517 |
show ?case |
|
68138 | 518 |
by (auto simp: *) |
33175 | 519 |
next |
520 |
case (Suc k) |
|
521 |
let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i" |
|
522 |
let ?S = "?f ` (S \<times> {f. (\<forall>i\<in>{1..k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1..k} \<longrightarrow> f i = i)})" |
|
523 |
have "?S = {f. (\<forall>i\<in>{1.. Suc k}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1.. Suc k} \<longrightarrow> f i = i)}" |
|
68138 | 524 |
apply (auto simp: image_iff) |
68134 | 525 |
apply (rename_tac f) |
526 |
apply (rule_tac x="f (Suc k)" in bexI) |
|
68138 | 527 |
apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI, auto) |
33175 | 528 |
done |
529 |
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] |
|
53854 | 530 |
show ?case |
531 |
by metis |
|
33175 | 532 |
qed |
533 |
||
534 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
535 |
lemma det_linear_rows_sum_lemma: |
53854 | 536 |
assumes fS: "finite S" |
537 |
and fT: "finite T" |
|
64267 | 538 |
shows "det ((\<chi> i. if i \<in> T then sum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = |
539 |
sum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)) |
|
53253 | 540 |
{f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}" |
541 |
using fT |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
542 |
proof (induct T arbitrary: a c set: finite) |
33175 | 543 |
case empty |
53253 | 544 |
have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)" |
545 |
by vector |
|
53854 | 546 |
from empty.prems show ?case |
62408
86f27b264d3d
Conformal_mappings: a big development in complex analysis (+ some lemmas)
paulson <lp15@cam.ac.uk>
parents:
61286
diff
changeset
|
547 |
unfolding th0 by (simp add: eq_id_iff) |
33175 | 548 |
next |
549 |
case (insert z T a c) |
|
550 |
let ?F = "\<lambda>T. {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}" |
|
551 |
let ?h = "\<lambda>(y,g) i. if i = z then y else g i" |
|
552 |
let ?k = "\<lambda>h. (h(z),(\<lambda>i. if i = z then i else h i))" |
|
553 |
let ?s = "\<lambda> k a c f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)" |
|
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56545
diff
changeset
|
554 |
let ?c = "\<lambda>j i. if i = z then a i j else c i" |
53253 | 555 |
have thif: "\<And>a b c d. (if a \<or> b then c else d) = (if a then c else if b then c else d)" |
556 |
by simp |
|
33175 | 557 |
have thif2: "\<And>a b c d e. (if a then b else if c then d else e) = |
53253 | 558 |
(if c then (if a then b else d) else (if a then b else e))" |
559 |
by simp |
|
68134 | 560 |
from \<open>z \<notin> T\<close> have nz: "\<And>i. i \<in> T \<Longrightarrow> i \<noteq> z" |
53253 | 561 |
by auto |
64267 | 562 |
have "det (\<chi> i. if i \<in> insert z T then sum (a i) S else c i) = |
563 |
det (\<chi> i. if i = z then sum (a i) S else if i \<in> T then sum (a i) S else c i)" |
|
33175 | 564 |
unfolding insert_iff thif .. |
64267 | 565 |
also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<in> T then sum (a i) S else if i = z then a i j else c i))" |
566 |
unfolding det_linear_row_sum[OF fS] |
|
68134 | 567 |
by (subst thif2) (simp add: nz cong: if_cong) |
33175 | 568 |
finally have tha: |
64267 | 569 |
"det (\<chi> i. if i \<in> insert z T then sum (a i) S else c i) = |
33175 | 570 |
(\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i) |
571 |
else if i = z then a i j |
|
572 |
else c i))" |
|
64267 | 573 |
unfolding insert.hyps unfolding sum.cartesian_product by blast |
33175 | 574 |
show ?case unfolding tha |
60420 | 575 |
using \<open>z \<notin> T\<close> |
64267 | 576 |
by (intro sum.reindex_bij_witness[where i="?k" and j="?h"]) |
57129
7edb7550663e
introduce more powerful reindexing rules for big operators
hoelzl
parents:
56545
diff
changeset
|
577 |
(auto intro!: cong[OF refl[of det]] simp: vec_eq_iff) |
33175 | 578 |
qed |
579 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
580 |
lemma det_linear_rows_sum: |
53854 | 581 |
fixes S :: "'n::finite set" |
582 |
assumes fS: "finite S" |
|
64267 | 583 |
shows "det (\<chi> i. sum (a i) S) = |
584 |
sum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}" |
|
53253 | 585 |
proof - |
586 |
have th0: "\<And>x y. ((\<chi> i. if i \<in> (UNIV:: 'n set) then x i else y i) :: 'a^'n^'n) = (\<chi> i. x i)" |
|
587 |
by vector |
|
64267 | 588 |
from det_linear_rows_sum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] |
53253 | 589 |
show ?thesis by simp |
33175 | 590 |
qed |
591 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
592 |
lemma matrix_mul_sum_alt: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
593 |
fixes A B :: "'a::comm_ring_1^'n^'n" |
64267 | 594 |
shows "A ** B = (\<chi> i. sum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))" |
595 |
by (vector matrix_matrix_mult_def sum_component) |
|
33175 | 596 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
597 |
lemma det_rows_mul: |
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset
|
598 |
"det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) = |
64272 | 599 |
prod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)" |
600 |
proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong) |
|
33175 | 601 |
let ?U = "UNIV :: 'n set" |
602 |
let ?PU = "{p. p permutes ?U}" |
|
53253 | 603 |
fix p |
604 |
assume pU: "p \<in> ?PU" |
|
33175 | 605 |
let ?s = "of_int (sign p)" |
53253 | 606 |
from pU have p: "p permutes ?U" |
607 |
by blast |
|
64272 | 608 |
have "prod (\<lambda>i. c i * a i $ p i) ?U = prod c ?U * prod (\<lambda>i. a i $ p i) ?U" |
609 |
unfolding prod.distrib .. |
|
33175 | 610 |
then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) = |
64272 | 611 |
prod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" |
53854 | 612 |
by (simp add: field_simps) |
57418 | 613 |
qed rule |
33175 | 614 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
615 |
proposition det_mul: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
616 |
fixes A B :: "'a::comm_ring_1^'n^'n" |
33175 | 617 |
shows "det (A ** B) = det A * det B" |
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
618 |
proof - |
33175 | 619 |
let ?U = "UNIV :: 'n set" |
68134 | 620 |
let ?F = "{f. (\<forall>i \<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}" |
33175 | 621 |
let ?PU = "{p. p permutes ?U}" |
68134 | 622 |
have "p \<in> ?F" if "p permutes ?U" for p |
53854 | 623 |
by simp |
624 |
then have PUF: "?PU \<subseteq> ?F" by blast |
|
53253 | 625 |
{ |
626 |
fix f |
|
627 |
assume fPU: "f \<in> ?F - ?PU" |
|
53854 | 628 |
have fUU: "f ` ?U \<subseteq> ?U" |
629 |
using fPU by auto |
|
53253 | 630 |
from fPU have f: "\<forall>i \<in> ?U. f i \<in> ?U" "\<forall>i. i \<notin> ?U \<longrightarrow> f i = i" "\<not>(\<forall>y. \<exists>!x. f x = y)" |
631 |
unfolding permutes_def by auto |
|
33175 | 632 |
|
633 |
let ?A = "(\<chi> i. A$i$f i *s B$f i) :: 'a^'n^'n" |
|
634 |
let ?B = "(\<chi> i. B$f i) :: 'a^'n^'n" |
|
53253 | 635 |
{ |
636 |
assume fni: "\<not> inj_on f ?U" |
|
33175 | 637 |
then obtain i j where ij: "f i = f j" "i \<noteq> j" |
638 |
unfolding inj_on_def by blast |
|
68134 | 639 |
then have "row i ?B = row j ?B" |
53854 | 640 |
by (vector row_def) |
68134 | 641 |
with det_identical_rows[OF ij(2)] |
33175 | 642 |
have "det (\<chi> i. A$i$f i *s B$f i) = 0" |
68134 | 643 |
unfolding det_rows_mul by force |
53253 | 644 |
} |
33175 | 645 |
moreover |
53253 | 646 |
{ |
647 |
assume fi: "inj_on f ?U" |
|
33175 | 648 |
from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j" |
649 |
unfolding inj_on_def by metis |
|
68134 | 650 |
note fs = fi[unfolded surjective_iff_injective_gen[OF finite finite refl fUU, symmetric]] |
651 |
have "\<exists>!x. f x = y" for y |
|
652 |
using fith fs by blast |
|
53854 | 653 |
with f(3) have "det (\<chi> i. A$i$f i *s B$f i) = 0" |
654 |
by blast |
|
53253 | 655 |
} |
53854 | 656 |
ultimately have "det (\<chi> i. A$i$f i *s B$f i) = 0" |
657 |
by blast |
|
53253 | 658 |
} |
53854 | 659 |
then have zth: "\<forall> f\<in> ?F - ?PU. det (\<chi> i. A$i$f i *s B$f i) = 0" |
53253 | 660 |
by simp |
661 |
{ |
|
662 |
fix p |
|
663 |
assume pU: "p \<in> ?PU" |
|
53854 | 664 |
from pU have p: "p permutes ?U" |
665 |
by blast |
|
33175 | 666 |
let ?s = "\<lambda>p. of_int (sign p)" |
53253 | 667 |
let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))" |
64267 | 668 |
have "(sum (\<lambda>q. ?s q * |
53253 | 669 |
(\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = |
64267 | 670 |
(sum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))) ?PU)" |
33175 | 671 |
unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] |
64267 | 672 |
proof (rule sum.cong) |
53253 | 673 |
fix q |
674 |
assume qU: "q \<in> ?PU" |
|
53854 | 675 |
then have q: "q permutes ?U" |
676 |
by blast |
|
33175 | 677 |
from p q have pp: "permutation p" and pq: "permutation q" |
678 |
unfolding permutation_permutes by auto |
|
679 |
have th00: "of_int (sign p) * of_int (sign p) = (1::'a)" |
|
680 |
"\<And>a. of_int (sign p) * (of_int (sign p) * a) = a" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
681 |
unfolding mult.assoc[symmetric] |
53854 | 682 |
unfolding of_int_mult[symmetric] |
33175 | 683 |
by (simp_all add: sign_idempotent) |
53854 | 684 |
have ths: "?s q = ?s p * ?s (q \<circ> inv p)" |
33175 | 685 |
using pp pq permutation_inverse[OF pp] sign_inverse[OF pp] |
68134 | 686 |
by (simp add: th00 ac_simps sign_idempotent sign_compose) |
64272 | 687 |
have th001: "prod (\<lambda>i. B$i$ q (inv p i)) ?U = prod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U" |
68134 | 688 |
by (rule prod.permute[OF p]) |
64272 | 689 |
have thp: "prod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U = |
690 |
prod (\<lambda>i. A$i$p i) ?U * prod (\<lambda>i. B$i$ q (inv p i)) ?U" |
|
691 |
unfolding th001 prod.distrib[symmetric] o_def permutes_inverses[OF p] |
|
692 |
apply (rule prod.cong[OF refl]) |
|
53253 | 693 |
using permutes_in_image[OF q] |
694 |
apply vector |
|
695 |
done |
|
64272 | 696 |
show "?s q * prod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = |
697 |
?s p * (prod (\<lambda>i. A$i$p i) ?U) * (?s (q \<circ> inv p) * prod (\<lambda>i. B$i$(q \<circ> inv p) i) ?U)" |
|
33175 | 698 |
using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] |
36350 | 699 |
by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose) |
57418 | 700 |
qed rule |
33175 | 701 |
} |
64267 | 702 |
then have th2: "sum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B" |
703 |
unfolding det_def sum_product |
|
704 |
by (rule sum.cong [OF refl]) |
|
705 |
have "det (A**B) = sum (\<lambda>f. det (\<chi> i. A $ i $ f i *s B $ f i)) ?F" |
|
68134 | 706 |
unfolding matrix_mul_sum_alt det_linear_rows_sum[OF finite] |
53854 | 707 |
by simp |
64267 | 708 |
also have "\<dots> = sum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU" |
68134 | 709 |
using sum.mono_neutral_cong_left[OF finite PUF zth, symmetric] |
33175 | 710 |
unfolding det_rows_mul by auto |
711 |
finally show ?thesis unfolding th2 . |
|
712 |
qed |
|
713 |
||
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
714 |
|
69683 | 715 |
subsection \<open>Relation to invertibility\<close> |
33175 | 716 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
717 |
proposition invertible_det_nz: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
718 |
fixes A::"'a::{field}^'n^'n" |
33175 | 719 |
shows "invertible A \<longleftrightarrow> det A \<noteq> 0" |
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
720 |
proof (cases "invertible A") |
68134 | 721 |
case True |
722 |
then obtain B :: "'a^'n^'n" where B: "A ** B = mat 1" |
|
723 |
unfolding invertible_right_inverse by blast |
|
724 |
then have "det (A ** B) = det (mat 1 :: 'a^'n^'n)" |
|
725 |
by simp |
|
726 |
then show ?thesis |
|
727 |
by (metis True det_I det_mul mult_zero_left one_neq_zero) |
|
728 |
next |
|
729 |
case False |
|
730 |
let ?U = "UNIV :: 'n set" |
|
731 |
have fU: "finite ?U" |
|
732 |
by simp |
|
733 |
from False obtain c i where c: "sum (\<lambda>i. c i *s row i A) ?U = 0" and iU: "i \<in> ?U" and ci: "c i \<noteq> 0" |
|
734 |
unfolding invertible_right_inverse matrix_right_invertible_independent_rows |
|
53854 | 735 |
by blast |
68134 | 736 |
have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})" |
68143 | 737 |
unfolding sum_cmul using c ci |
68138 | 738 |
by (auto simp: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff) |
68134 | 739 |
have thr: "- row i A \<in> vec.span {row j A| j. j \<noteq> i}" |
740 |
unfolding thr0 by (auto intro: vec.span_base vec.span_scale vec.span_sum) |
|
741 |
let ?B = "(\<chi> k. if k = i then 0 else row k A) :: 'a^'n^'n" |
|
742 |
have thrb: "row i ?B = 0" using iU by (vector row_def) |
|
743 |
have "det A = 0" |
|
744 |
unfolding det_row_span[OF thr, symmetric] right_minus |
|
745 |
unfolding det_zero_row(2)[OF thrb] .. |
|
746 |
then show ?thesis |
|
747 |
by (simp add: False) |
|
33175 | 748 |
qed |
749 |
||
68134 | 750 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
751 |
lemma det_nz_iff_inj_gen: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
752 |
fixes f :: "'a::field^'n \<Rightarrow> 'a::field^'n" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
753 |
assumes "Vector_Spaces.linear (*s) (*s) f" |
67990 | 754 |
shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f" |
755 |
proof |
|
756 |
assume "det (matrix f) \<noteq> 0" |
|
757 |
then show "inj f" |
|
758 |
using assms invertible_det_nz inj_matrix_vector_mult by force |
|
759 |
next |
|
760 |
assume "inj f" |
|
761 |
show "det (matrix f) \<noteq> 0" |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
762 |
using vec.linear_injective_left_inverse [OF assms \<open>inj f\<close>] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
763 |
by (metis assms invertible_det_nz invertible_left_inverse matrix_compose_gen matrix_id_mat_1) |
67990 | 764 |
qed |
765 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
766 |
lemma det_nz_iff_inj: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
767 |
fixes f :: "real^'n \<Rightarrow> real^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
768 |
assumes "linear f" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
769 |
shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
770 |
using det_nz_iff_inj_gen[of f] assms |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
771 |
unfolding linear_matrix_vector_mul_eq . |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
772 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
773 |
lemma det_eq_0_rank: |
67990 | 774 |
fixes A :: "real^'n^'n" |
775 |
shows "det A = 0 \<longleftrightarrow> rank A < CARD('n)" |
|
776 |
using invertible_det_nz [of A] |
|
777 |
by (auto simp: matrix_left_invertible_injective invertible_left_inverse less_rank_noninjective) |
|
778 |
||
70136 | 779 |
subsubsection\<^marker>\<open>tag important\<close> \<open>Invertibility of matrices and corresponding linear functions\<close> |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
780 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
781 |
lemma matrix_left_invertible_gen: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
782 |
fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
783 |
assumes "Vector_Spaces.linear (*s) (*s) f" |
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
784 |
shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id))" |
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
785 |
proof safe |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
786 |
fix B |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
787 |
assume 1: "B ** matrix f = mat 1" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
788 |
show "\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> g \<circ> f = id" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
789 |
proof (intro exI conjI) |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
790 |
show "Vector_Spaces.linear (*s) (*s) (\<lambda>y. B *v y)" |
68138 | 791 |
by simp |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
792 |
show "((*v) B) \<circ> f = id" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
793 |
unfolding o_def |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
794 |
by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
795 |
qed |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
796 |
next |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
797 |
fix g |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
798 |
assume "Vector_Spaces.linear (*s) (*s) g" "g \<circ> f = id" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
799 |
then have "matrix g ** matrix f = mat 1" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
800 |
by (metis assms matrix_compose_gen matrix_id_mat_1) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
801 |
then show "\<exists>B. B ** matrix f = mat 1" .. |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
802 |
qed |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
803 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
804 |
lemma matrix_left_invertible: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
805 |
"linear f \<Longrightarrow> ((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> g \<circ> f = id))" for f::"real^'m \<Rightarrow> real^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
806 |
using matrix_left_invertible_gen[of f] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
807 |
by (auto simp: linear_matrix_vector_mul_eq) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
808 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
809 |
lemma matrix_right_invertible_gen: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
810 |
fixes f :: "'a::field^'m \<Rightarrow> 'a^'n" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
811 |
assumes "Vector_Spaces.linear (*s) (*s) f" |
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
812 |
shows "((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id))" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
813 |
proof safe |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
814 |
fix B |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
815 |
assume 1: "matrix f ** B = mat 1" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
816 |
show "\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
817 |
proof (intro exI conjI) |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
818 |
show "Vector_Spaces.linear (*s) (*s) ((*v) B)" |
68138 | 819 |
by simp |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
820 |
show "f \<circ> (*v) B = id" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
821 |
using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
822 |
by (metis (no_types, hide_lams)) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
823 |
qed |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
824 |
next |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
825 |
fix g |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
826 |
assume "Vector_Spaces.linear (*s) (*s) g" and "f \<circ> g = id" |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
827 |
then have "matrix f ** matrix g = mat 1" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
828 |
by (metis assms matrix_compose_gen matrix_id_mat_1) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
829 |
then show "\<exists>B. matrix f ** B = mat 1" .. |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
830 |
qed |
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
831 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
832 |
lemma matrix_right_invertible: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
833 |
"linear f \<Longrightarrow> ((\<exists>B. matrix f ** B = mat 1) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id))" for f::"real^'m \<Rightarrow> real^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
834 |
using matrix_right_invertible_gen[of f] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
835 |
by (auto simp: linear_matrix_vector_mul_eq) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
836 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
837 |
lemma matrix_invertible_gen: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
838 |
fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
839 |
assumes "Vector_Spaces.linear (*s) (*s) f" |
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
840 |
shows "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear (*s) (*s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
841 |
(is "?lhs = ?rhs") |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
842 |
proof |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
843 |
assume ?lhs then show ?rhs |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
844 |
by (metis assms invertible_def left_right_inverse_eq matrix_left_invertible_gen matrix_right_invertible_gen) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
845 |
next |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
846 |
assume ?rhs then show ?lhs |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
847 |
by (metis assms invertible_def matrix_compose_gen matrix_id_mat_1) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
848 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
849 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
850 |
lemma matrix_invertible: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
851 |
"linear f \<Longrightarrow> invertible (matrix f) \<longleftrightarrow> (\<exists>g. linear g \<and> f \<circ> g = id \<and> g \<circ> f = id)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
852 |
for f::"real^'m \<Rightarrow> real^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
853 |
using matrix_invertible_gen[of f] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
854 |
by (auto simp: linear_matrix_vector_mul_eq) |
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
855 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
856 |
lemma invertible_eq_bij: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
857 |
fixes m :: "'a::field^'m^'n" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
858 |
shows "invertible m \<longleftrightarrow> bij ((*v) m)" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
859 |
using matrix_invertible_gen[OF matrix_vector_mul_linear_gen, of m, simplified matrix_of_matrix_vector_mul] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
860 |
by (metis bij_betw_def left_right_inverse_eq matrix_vector_mul_linear_gen o_bij |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
861 |
vec.linear_injective_left_inverse vec.linear_surjective_right_inverse) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
862 |
|
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset
|
863 |
|
69683 | 864 |
subsection \<open>Cramer's rule\<close> |
33175 | 865 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
866 |
lemma cramer_lemma_transpose: |
68263 | 867 |
fixes A:: "'a::{field}^'n^'n" |
868 |
and x :: "'a::{field}^'n" |
|
64267 | 869 |
shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x$i *s row i A) (UNIV::'n set) |
68263 | 870 |
else row i A)::'a::{field}^'n^'n) = x$k * det A" |
33175 | 871 |
(is "?lhs = ?rhs") |
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
872 |
proof - |
33175 | 873 |
let ?U = "UNIV :: 'n set" |
874 |
let ?Uk = "?U - {k}" |
|
53854 | 875 |
have U: "?U = insert k ?Uk" |
876 |
by blast |
|
877 |
have kUk: "k \<notin> ?Uk" |
|
878 |
by simp |
|
33175 | 879 |
have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s" |
36350 | 880 |
by (vector field_simps) |
53854 | 881 |
have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" |
882 |
by auto |
|
33175 | 883 |
have "(\<chi> i. row i A) = A" by (vector row_def) |
53253 | 884 |
then have thd1: "det (\<chi> i. row i A) = det A" |
885 |
by simp |
|
33175 | 886 |
have thd0: "det (\<chi> i. if i = k then row k A + (\<Sum>i \<in> ?Uk. x $ i *s row i A) else row i A) = det A" |
68134 | 887 |
by (force intro: det_row_span vec.span_sum vec.span_scale vec.span_base) |
33175 | 888 |
show "?lhs = x$k * det A" |
889 |
apply (subst U) |
|
68134 | 890 |
unfolding sum.insert[OF finite kUk] |
33175 | 891 |
apply (subst th00) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset
|
892 |
unfolding add.assoc |
33175 | 893 |
apply (subst det_row_add) |
894 |
unfolding thd0 |
|
895 |
unfolding det_row_mul |
|
896 |
unfolding th001[of k "\<lambda>i. row i A"] |
|
53253 | 897 |
unfolding thd1 |
898 |
apply (simp add: field_simps) |
|
899 |
done |
|
33175 | 900 |
qed |
901 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
902 |
proposition cramer_lemma: |
68263 | 903 |
fixes A :: "'a::{field}^'n^'n" |
904 |
shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a::{field}^'n^'n) = x$k * det A" |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
905 |
proof - |
33175 | 906 |
let ?U = "UNIV :: 'n set" |
64267 | 907 |
have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
908 |
by (auto intro: sum.cong) |
53854 | 909 |
show ?thesis |
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset
|
910 |
unfolding matrix_mult_sum |
53253 | 911 |
unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] |
912 |
unfolding *[of "\<lambda>i. x$i"] |
|
913 |
apply (subst det_transpose[symmetric]) |
|
914 |
apply (rule cong[OF refl[of det]]) |
|
915 |
apply (vector transpose_def column_def row_def) |
|
916 |
done |
|
33175 | 917 |
qed |
918 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
919 |
proposition cramer: |
68263 | 920 |
fixes A ::"'a::{field}^'n^'n" |
33175 | 921 |
assumes d0: "det A \<noteq> 0" |
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset
|
922 |
shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)" |
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
923 |
proof - |
33175 | 924 |
from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" |
53854 | 925 |
unfolding invertible_det_nz[symmetric] invertible_def |
926 |
by blast |
|
927 |
have "(A ** B) *v b = b" |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
928 |
by (simp add: B) |
53854 | 929 |
then have "A *v (B *v b) = b" |
930 |
by (simp add: matrix_vector_mul_assoc) |
|
931 |
then have xe: "\<exists>x. A *v x = b" |
|
932 |
by blast |
|
53253 | 933 |
{ |
934 |
fix x |
|
935 |
assume x: "A *v x = b" |
|
936 |
have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)" |
|
937 |
unfolding x[symmetric] |
|
938 |
using d0 by (simp add: vec_eq_iff cramer_lemma field_simps) |
|
939 |
} |
|
53854 | 940 |
with xe show ?thesis |
941 |
by auto |
|
33175 | 942 |
qed |
943 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
944 |
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
945 |
by (simp add: det_def sign_id) |
33175 | 946 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
947 |
lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1" |
53253 | 948 |
proof - |
33175 | 949 |
have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto |
950 |
show ?thesis |
|
53253 | 951 |
unfolding det_def UNIV_2 |
64267 | 952 |
unfolding sum_over_permutations_insert[OF f12] |
53253 | 953 |
unfolding permutes_sing |
954 |
by (simp add: sign_swap_id sign_id swap_id_eq) |
|
33175 | 955 |
qed |
956 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
957 |
lemma det_3: |
53253 | 958 |
"det (A::'a::comm_ring_1^3^3) = |
959 |
A$1$1 * A$2$2 * A$3$3 + |
|
960 |
A$1$2 * A$2$3 * A$3$1 + |
|
961 |
A$1$3 * A$2$1 * A$3$2 - |
|
962 |
A$1$1 * A$2$3 * A$3$2 - |
|
963 |
A$1$2 * A$2$1 * A$3$3 - |
|
964 |
A$1$3 * A$2$2 * A$3$1" |
|
965 |
proof - |
|
53854 | 966 |
have f123: "finite {2::3, 3}" "1 \<notin> {2::3, 3}" |
967 |
by auto |
|
968 |
have f23: "finite {3::3}" "2 \<notin> {3::3}" |
|
969 |
by auto |
|
33175 | 970 |
|
971 |
show ?thesis |
|
53253 | 972 |
unfolding det_def UNIV_3 |
64267 | 973 |
unfolding sum_over_permutations_insert[OF f123] |
974 |
unfolding sum_over_permutations_insert[OF f23] |
|
53253 | 975 |
unfolding permutes_sing |
976 |
by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) |
|
33175 | 977 |
qed |
978 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
979 |
proposition det_orthogonal_matrix: |
69680 | 980 |
fixes Q:: "'a::linordered_idom^'n^'n" |
981 |
assumes oQ: "orthogonal_matrix Q" |
|
982 |
shows "det Q = 1 \<or> det Q = - 1" |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
983 |
proof - |
69680 | 984 |
have "Q ** transpose Q = mat 1" |
985 |
by (metis oQ orthogonal_matrix_def) |
|
986 |
then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" |
|
987 |
by simp |
|
988 |
then have "det Q * det Q = 1" |
|
989 |
by (simp add: det_mul) |
|
990 |
then show ?thesis |
|
991 |
by (simp add: square_eq_1_iff) |
|
992 |
qed |
|
993 |
||
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
994 |
proposition orthogonal_transformation_det [simp]: |
69680 | 995 |
fixes f :: "real^'n \<Rightarrow> real^'n" |
996 |
shows "orthogonal_transformation f \<Longrightarrow> \<bar>det (matrix f)\<bar> = 1" |
|
70136 | 997 |
using det_orthogonal_matrix orthogonal_transformation_matrix by fastforce |
69680 | 998 |
|
69683 | 999 |
subsection \<open>Rotation, reflection, rotoinversion\<close> |
69680 | 1000 |
|
70136 | 1001 |
definition\<^marker>\<open>tag important\<close> "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1" |
1002 |
definition\<^marker>\<open>tag important\<close> "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1" |
|
69680 | 1003 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1004 |
lemma orthogonal_rotation_or_rotoinversion: |
69680 | 1005 |
fixes Q :: "'a::linordered_idom^'n^'n" |
1006 |
shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q" |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1007 |
by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) |
69680 | 1008 |
|
68134 | 1009 |
text\<open> Slightly stronger results giving rotation, but only in two or more dimensions\<close> |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1010 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1011 |
lemma rotation_matrix_exists_basis: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1012 |
fixes a :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1013 |
assumes 2: "2 \<le> CARD('n)" and "norm a = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1014 |
obtains A where "rotation_matrix A" "A *v (axis k 1) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1015 |
proof - |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1016 |
obtain A where "orthogonal_matrix A" and A: "A *v (axis k 1) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1017 |
using orthogonal_matrix_exists_basis assms by metis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1018 |
with orthogonal_rotation_or_rotoinversion |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1019 |
consider "rotation_matrix A" | "rotoinversion_matrix A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1020 |
by metis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1021 |
then show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1022 |
proof cases |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1023 |
assume "rotation_matrix A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1024 |
then show ?thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1025 |
using \<open>A *v axis k 1 = a\<close> that by auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1026 |
next |
69680 | 1027 |
from ex_card[OF 2] obtain h i::'n where "h \<noteq> i" |
1028 |
by (auto simp add: eval_nat_numeral card_Suc_eq) |
|
1029 |
then obtain j where "j \<noteq> k" |
|
1030 |
by (metis (full_types)) |
|
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1031 |
let ?TA = "transpose A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1032 |
let ?A = "\<chi> i. if i = j then - 1 *\<^sub>R (?TA $ i) else ?TA $i" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1033 |
assume "rotoinversion_matrix A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1034 |
then have [simp]: "det A = -1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1035 |
by (simp add: rotoinversion_matrix_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1036 |
show ?thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1037 |
proof |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1038 |
have [simp]: "row i (\<chi> i. if i = j then - 1 *\<^sub>R ?TA $ i else ?TA $ i) = (if i = j then - row i ?TA else row i ?TA)" for i |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1039 |
by (auto simp: row_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1040 |
have "orthogonal_matrix ?A" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1041 |
unfolding orthogonal_matrix_orthonormal_rows |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1042 |
using \<open>orthogonal_matrix A\<close> by (auto simp: orthogonal_matrix_orthonormal_columns orthogonal_clauses) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1043 |
then show "rotation_matrix (transpose ?A)" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1044 |
unfolding rotation_matrix_def |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1045 |
by (simp add: det_row_mul[of j _ "\<lambda>i. ?TA $ i", unfolded scalar_mult_eq_scaleR]) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1046 |
show "transpose ?A *v axis k 1 = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1047 |
using \<open>j \<noteq> k\<close> A by (simp add: matrix_vector_column axis_def scalar_mult_eq_scaleR if_distrib [of "\<lambda>z. z *\<^sub>R c" for c] cong: if_cong) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1048 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1049 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1050 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1051 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1052 |
lemma rotation_exists_1: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1053 |
fixes a :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1054 |
assumes "2 \<le> CARD('n)" "norm a = 1" "norm b = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1055 |
obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1056 |
proof - |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1057 |
obtain k::'n where True |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1058 |
by simp |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1059 |
obtain A B where AB: "rotation_matrix A" "rotation_matrix B" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1060 |
and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1061 |
using rotation_matrix_exists_basis assms by metis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1062 |
let ?f = "\<lambda>x. (B ** transpose A) *v x" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1063 |
show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1064 |
proof |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1065 |
show "orthogonal_transformation ?f" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1066 |
using AB orthogonal_matrix_mul orthogonal_transformation_matrix rotation_matrix_def matrix_vector_mul_linear by force |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1067 |
show "det (matrix ?f) = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1068 |
using AB by (auto simp: det_mul rotation_matrix_def) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1069 |
show "?f a = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1070 |
using AB unfolding orthogonal_matrix_def rotation_matrix_def |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1071 |
by (metis eq matrix_mul_rid matrix_vector_mul_assoc) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1072 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1073 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1074 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1075 |
lemma rotation_exists: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1076 |
fixes a :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1077 |
assumes 2: "2 \<le> CARD('n)" and eq: "norm a = norm b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1078 |
obtains f where "orthogonal_transformation f" "det(matrix f) = 1" "f a = b" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1079 |
proof (cases "a = 0 \<or> b = 0") |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1080 |
case True |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1081 |
with assms have "a = 0" "b = 0" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1082 |
by auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1083 |
then show ?thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1084 |
by (metis eq_id_iff matrix_id orthogonal_transformation_id that) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1085 |
next |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1086 |
case False |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1087 |
then obtain f where f: "orthogonal_transformation f" "det (matrix f) = 1" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1088 |
and f': "f (a /\<^sub>R norm a) = b /\<^sub>R norm b" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1089 |
using rotation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b", OF 2] by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1090 |
then interpret linear f by (simp add: orthogonal_transformation) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1091 |
have "f a = b" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1092 |
using f' False |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1093 |
by (simp add: eq scale) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
67990
diff
changeset
|
1094 |
with f show thesis .. |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1095 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1096 |
|
69720
be6634e99e09
redid tagging for 3 theories i.e. Determinants, Change_of_Vars, Finite_Cartesian_Product
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
69683
diff
changeset
|
1097 |
lemma rotation_rightward_line: |
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1098 |
fixes a :: "real^'n" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1099 |
obtains f where "orthogonal_transformation f" "2 \<le> CARD('n) \<Longrightarrow> det(matrix f) = 1" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1100 |
"f(norm a *\<^sub>R axis k 1) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1101 |
proof (cases "CARD('n) = 1") |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1102 |
case True |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1103 |
obtain f where "orthogonal_transformation f" "f (norm a *\<^sub>R axis k (1::real)) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1104 |
proof (rule orthogonal_transformation_exists) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1105 |
show "norm (norm a *\<^sub>R axis k (1::real)) = norm a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1106 |
by simp |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1107 |
qed auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1108 |
then show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1109 |
using True that by auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1110 |
next |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1111 |
case False |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1112 |
obtain f where "orthogonal_transformation f" "det(matrix f) = 1" "f (norm a *\<^sub>R axis k 1) = a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1113 |
proof (rule rotation_exists) |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1114 |
show "2 \<le> CARD('n)" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1115 |
using False one_le_card_finite [where 'a='n] by linarith |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1116 |
show "norm (norm a *\<^sub>R axis k (1::real)) = norm a" |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1117 |
by simp |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1118 |
qed auto |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1119 |
then show thesis |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1120 |
using that by blast |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1121 |
qed |
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset
|
1122 |
|
33175 | 1123 |
end |