author  immler 
Wed, 02 May 2018 13:49:38 +0200  
changeset 68072  493b818e8e10 
parent 67990  c0ebecf6e3eb 
child 68073  fad29d2a17a5 
permissions  rwrr 
63627  1 
(* Title: HOL/Analysis/Determinants.thy 
41959  2 
Author: Amine Chaieb, University of Cambridge 
33175  3 
*) 
4 

60420  5 
section \<open>Traces, Determinant of square matrices and some properties\<close> 
33175  6 

7 
theory Determinants 

44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

8 
imports 
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

9 
Cartesian_Euclidean_Space 
66453
cc19f7ca2ed6
sessionqualified theory imports: isabelle imports U i d '~~/src/Benchmarks' a;
wenzelm
parents:
64272
diff
changeset

10 
"HOLLibrary.Permutations" 
33175  11 
begin 
12 

60420  13 
subsection \<open>Trace\<close> 
33175  14 

53253  15 
definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" 
64267  16 
where "trace A = sum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)" 
33175  17 

53854  18 
lemma trace_0: "trace (mat 0) = 0" 
33175  19 
by (simp add: trace_def mat_def) 
20 

53854  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 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
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 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
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 

53854  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 

60420  36 
text \<open>Definition of determinant.\<close> 
33175  37 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

38 
definition 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 

60420  43 
text \<open>A few general lemmas we need below.\<close> 
33175  44 

64272  45 
lemma prod_permute: 
33175  46 
assumes p: "p permutes S" 
64272  47 
shows "prod f S = prod (f \<circ> p) S" 
48 
using assms by (fact prod.permute) 

33175  49 

64272  50 
lemma product_permute_nat_interval: 
53854  51 
fixes m n :: nat 
64272  52 
shows "p permutes {m..n} \<Longrightarrow> prod f {m..n} = prod (f \<circ> p) {m..n}" 
53 
by (blast intro!: prod_permute) 

33175  54 

60420  55 
text \<open>Basic determinant properties.\<close> 
33175  56 

67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

57 
lemma det_transpose [simp]: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" 
53253  58 
proof  
33175  59 
let ?di = "\<lambda>A i j. A$i$j" 
60 
let ?U = "(UNIV :: 'n set)" 

61 
have fU: "finite ?U" by simp 

53253  62 
{ 
63 
fix p 

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

53854  65 
from p have pU: "p permutes ?U" 
66 
by blast 

33175  67 
have sth: "sign (inv p) = sign p" 
44260
7784fa3232ce
Determinants.thy: avoid using mem_def/Collect_def
huffman
parents:
44228
diff
changeset

68 
by (metis sign_inverse fU p mem_Collect_eq permutation_permutes) 
33175  69 
from permutes_inj[OF pU] 
53854  70 
have pi: "inj_on p ?U" 
71 
by (blast intro: subset_inj_on) 

33175  72 
from permutes_image[OF pU] 
64272  73 
have "prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U = 
74 
prod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)" 

53854  75 
by simp 
64272  76 
also have "\<dots> = prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U" 
77 
unfolding prod.reindex[OF pi] .. 

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

53253  79 
proof  
80 
{ 

81 
fix i 

82 
assume i: "i \<in> ?U" 

33175  83 
from i permutes_inv_o[OF pU] permutes_in_image[OF pU] 
53854  84 
have "((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) i = ?di A i (p i)" 
53253  85 
unfolding transpose_def by (simp add: fun_eq_iff) 
86 
} 

64272  87 
then show "prod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U = 
88 
prod (\<lambda>i. ?di A i (p i)) ?U" 

89 
by (auto intro: prod.cong) 

33175  90 
qed 
64272  91 
finally have "of_int (sign (inv p)) * (prod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = 
92 
of_int (sign p) * (prod (\<lambda>i. ?di A i (p i)) ?U)" 

53854  93 
using sth by simp 
53253  94 
} 
95 
then show ?thesis 

96 
unfolding det_def 

64267  97 
apply (subst sum_permutations_inverse) 
98 
apply (rule sum.cong) 

57418  99 
apply (rule refl) 
53253  100 
apply blast 
101 
done 

33175  102 
qed 
103 

104 
lemma det_lowerdiagonal: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

105 
fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})" 
33175  106 
assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0" 
64272  107 
shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)" 
53253  108 
proof  
33175  109 
let ?U = "UNIV:: 'n set" 
110 
let ?PU = "{p. p permutes ?U}" 

64272  111 
let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" 
53854  112 
have fU: "finite ?U" 
113 
by simp 

33175  114 
from finite_permutations[OF fU] have fPU: "finite ?PU" . 
53854  115 
have id0: "{id} \<subseteq> ?PU" 
116 
by (auto simp add: permutes_id) 

53253  117 
{ 
118 
fix p 

53854  119 
assume p: "p \<in> ?PU  {id}" 
53253  120 
from p have pU: "p permutes ?U" and pid: "p \<noteq> id" 
121 
by blast+ 

122 
from permutes_natset_le[OF pU] pid obtain i where i: "p i > i" 

123 
by (metis not_le) 

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

125 
by blast 

64272  126 
from prod_zero[OF fU ex] have "?pp p = 0" 
53253  127 
by simp 
128 
} 

53854  129 
then have p0: "\<forall>p \<in> ?PU  {id}. ?pp p = 0" 
53253  130 
by blast 
64267  131 
from sum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis 
33175  132 
unfolding det_def by (simp add: sign_id) 
133 
qed 

134 

135 
lemma det_upperdiagonal: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

136 
fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}" 
33175  137 
assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0" 
64272  138 
shows "det A = prod (\<lambda>i. A$i$i) (UNIV:: 'n set)" 
53253  139 
proof  
33175  140 
let ?U = "UNIV:: 'n set" 
141 
let ?PU = "{p. p permutes ?U}" 

64272  142 
let ?pp = "(\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))" 
53854  143 
have fU: "finite ?U" 
144 
by simp 

33175  145 
from finite_permutations[OF fU] have fPU: "finite ?PU" . 
53854  146 
have id0: "{id} \<subseteq> ?PU" 
147 
by (auto simp add: permutes_id) 

53253  148 
{ 
149 
fix p 

53854  150 
assume p: "p \<in> ?PU  {id}" 
53253  151 
from p have pU: "p permutes ?U" and pid: "p \<noteq> id" 
152 
by blast+ 

153 
from permutes_natset_ge[OF pU] pid obtain i where i: "p i < i" 

154 
by (metis not_le) 

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

64272  157 
from prod_zero[OF fU ex] have "?pp p = 0" 
53854  158 
by simp 
53253  159 
} 
160 
then have p0: "\<forall>p \<in> ?PU {id}. ?pp p = 0" 

161 
by blast 

64267  162 
from sum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis 
33175  163 
unfolding det_def by (simp add: sign_id) 
164 
qed 

165 

166 
lemma det_diagonal: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

167 
fixes A :: "'a::comm_ring_1^'n^'n" 
33175  168 
assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0" 
64272  169 
shows "det A = prod (\<lambda>i. A$i$i) (UNIV::'n set)" 
53253  170 
proof  
33175  171 
let ?U = "UNIV:: 'n set" 
172 
let ?PU = "{p. p permutes ?U}" 

64272  173 
let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" 
33175  174 
have fU: "finite ?U" by simp 
175 
from finite_permutations[OF fU] have fPU: "finite ?PU" . 

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

53253  178 
{ 
179 
fix p 

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

53854  181 
then have "p \<noteq> id" 
182 
by simp 

183 
then obtain i where i: "p i \<noteq> i" 

184 
unfolding fun_eq_iff by auto 

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

186 
by blast 

64272  187 
from prod_zero [OF fU ex] have "?pp p = 0" 
53854  188 
by simp 
189 
} 

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

191 
by blast 

64267  192 
from sum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis 
33175  193 
unfolding det_def by (simp add: sign_id) 
194 
qed 

195 

67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

196 
lemma det_I [simp]: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

197 
by (simp add: det_diagonal mat_def) 
33175  198 

67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

199 
lemma det_0 [simp]: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" 
67970  200 
by (simp add: det_def prod_zero power_0_left) 
33175  201 

202 
lemma det_permute_rows: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

203 
fixes A :: "'a::comm_ring_1^'n^'n" 
33175  204 
assumes p: "p permutes (UNIV :: 'n::finite set)" 
53854  205 
shows "det (\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" 
64267  206 
apply (simp add: det_def sum_distrib_left mult.assoc[symmetric]) 
33175  207 
apply (subst sum_permutations_compose_right[OF p]) 
64267  208 
proof (rule sum.cong) 
33175  209 
let ?U = "UNIV :: 'n set" 
210 
let ?PU = "{p. p permutes ?U}" 

53253  211 
fix q 
212 
assume qPU: "q \<in> ?PU" 

53854  213 
have fU: "finite ?U" 
214 
by simp 

53253  215 
from qPU have q: "q permutes ?U" 
216 
by blast 

33175  217 
from p q have pp: "permutation p" and qp: "permutation q" 
218 
by (metis fU permutation_permutes)+ 

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

64272  220 
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" 
221 
by (simp only: prod_permute[OF ip, symmetric]) 

222 
also have "\<dots> = prod (\<lambda>i. A $ (p \<circ> inv p) i $ (q \<circ> (p \<circ> inv p)) i) ?U" 

53253  223 
by (simp only: o_def) 
64272  224 
also have "\<dots> = prod (\<lambda>i. A$i$q i) ?U" 
53253  225 
by (simp only: o_def permutes_inverses[OF p]) 
64272  226 
finally have thp: "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod (\<lambda>i. A$i$q i) ?U" 
53253  227 
by blast 
64272  228 
show "of_int (sign (q \<circ> p)) * prod (\<lambda>i. A$ p i$ (q \<circ> p) i) ?U = 
229 
of_int (sign p) * of_int (sign q) * prod (\<lambda>i. A$i$q i) ?U" 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

230 
by (simp only: thp sign_compose[OF qp pp] mult.commute of_int_mult) 
57418  231 
qed rule 
33175  232 

233 
lemma det_permute_columns: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

234 
fixes A :: "'a::comm_ring_1^'n^'n" 
33175  235 
assumes p: "p permutes (UNIV :: 'n set)" 
236 
shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A" 

53253  237 
proof  
33175  238 
let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n" 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

239 
let ?At = "transpose A" 
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

240 
have "of_int (sign p) * det A = det (transpose (\<chi> i. transpose A $ p i))" 
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

241 
unfolding det_permute_rows[OF p, of ?At] det_transpose .. 
33175  242 
moreover 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

243 
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

244 
by (simp add: transpose_def vec_eq_iff) 
53854  245 
ultimately show ?thesis 
246 
by simp 

33175  247 
qed 
248 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

249 
lemma det_identical_columns: 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

250 
fixes A :: "'a::comm_ring_1^'n^'n" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

251 
assumes jk: "j \<noteq> k" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

252 
and r: "column j A = column k A" 
33175  253 
shows "det A = 0" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

254 
proof  
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

255 
let ?U="UNIV::'n set" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

256 
let ?t_jk="Fun.swap j k id" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

257 
let ?PU="{p. p permutes ?U}" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

258 
let ?S1="{p. p\<in>?PU \<and> evenperm p}" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

259 
let ?S2="{(?t_jk \<circ> p) p. p \<in>?S1}" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

260 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

261 
let ?g="\<lambda>p. ?t_jk \<circ> p" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

262 
have g_S1: "?S2 = ?g` ?S1" by auto 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

263 
have inj_g: "inj_on ?g ?S1" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

264 
proof (unfold inj_on_def, auto) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

265 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

266 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

267 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

268 
qed 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

269 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

270 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

271 
using r jk 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

272 
unfolding column_def vec_eq_iff swap_id_eq by fastforce 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

273 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

274 
{fix x 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

275 
assume x: "x\<in> ?S1" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

276 
have "sign (?t_jk \<circ> x) = sign (?t_jk) * sign x" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

277 
by (metis (lifting) finite_class.finite_UNIV mem_Collect_eq 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

278 
permutation_permutes permutation_swap_id sign_compose x) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

279 
also have "... =  sign x" using sign_tjk by simp 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

280 
also have "... \<noteq> sign x" unfolding sign_def by simp 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

281 
finally have "sign (?t_jk \<circ> x) \<noteq> sign x" and "(?t_jk \<circ> x) \<in> ?S2" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

282 
by (auto, metis (lifting, full_types) mem_Collect_eq x) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

283 
} 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

284 
hence disjoint: "?S1 \<inter> ?S2 = {}" by (auto, metis sign_def) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

285 
have PU_decomposition: "?PU = ?S1 \<union> ?S2" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

286 
proof (auto) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

287 
fix x 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

288 
assume x: "x permutes ?U" and "\<forall>p. p permutes ?U \<longrightarrow> x = Fun.swap j k id \<circ> p \<longrightarrow> \<not> evenperm p" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

289 
from this obtain p where p: "p permutes UNIV" and x_eq: "x = Fun.swap j k id \<circ> p" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

290 
and odd_p: "\<not> evenperm p" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

291 
by (metis (no_types) comp_assoc id_comp inv_swap_id permutes_compose 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

292 
permutes_inv_o(1) tjk_permutes) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

293 
thus "evenperm x" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

294 
by (metis evenperm_comp evenperm_swap finite_class.finite_UNIV 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

295 
jk permutation_permutes permutation_swap_id) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

296 
next 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

297 
fix p assume p: "p permutes ?U" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

298 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

299 
qed 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

300 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

301 
\<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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

302 
unfolding g_S1 by (rule sum.reindex[OF inj_g]) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

303 
also have "... = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

304 
unfolding o_def by (rule sum.cong, auto simp add: tjk_eq) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

305 
also have "... = sum (\<lambda>p.  ?f p) ?S1" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

306 
proof (rule sum.cong, auto) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

307 
fix x assume x: "x permutes ?U" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

308 
and even_x: "evenperm x" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

309 
hence perm_x: "permutation x" and perm_tjk: "permutation ?t_jk" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

310 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

311 
by (metis finite_code)+ 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

312 
have "(sign (?t_jk \<circ> x)) =  (sign x)" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

313 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

314 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

315 
=  (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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

316 
by auto 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

317 
qed 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

318 
also have "...=  sum ?f ?S1" unfolding sum_negf .. 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

319 
finally have *: "sum ?f ?S2 =  sum ?f ?S1" . 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

320 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

321 
unfolding det_def .. 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

322 
also have "...= sum ?f ?S1 + sum ?f ?S2" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

323 
by (subst PU_decomposition, rule sum.union_disjoint[OF _ _ disjoint], auto) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

324 
also have "...= sum ?f ?S1  sum ?f ?S1 " unfolding * by auto 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

325 
also have "...= 0" by simp 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

326 
finally show "det A = 0" by simp 
33175  327 
qed 
328 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

329 
lemma det_identical_rows: 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

330 
fixes A :: "'a::comm_ring_1^'n^'n" 
33175  331 
assumes ij: "i \<noteq> j" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

332 
and r: "row i A = row j A" 
33175  333 
shows "det A = 0" 
53253  334 
apply (subst det_transpose[symmetric]) 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

335 
apply (rule det_identical_columns[OF ij]) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

336 
apply (metis column_transpose r) 
53253  337 
done 
33175  338 

339 
lemma det_zero_row: 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

340 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

341 
shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

342 
by (force simp add: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+ 
33175  343 

344 
lemma det_zero_column: 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

345 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

346 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

347 
unfolding atomize_conj atomize_imp 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

348 
by (metis det_transpose det_zero_row row_transpose) 
33175  349 

350 
lemma det_row_add: 

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

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

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

64267  355 
unfolding det_def vec_lambda_beta sum.distrib[symmetric] 
356 
proof (rule sum.cong) 

33175  357 
let ?U = "UNIV :: 'n set" 
358 
let ?pU = "{p. p permutes ?U}" 

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

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

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

53253  362 
fix p 
363 
assume p: "p \<in> ?pU" 

33175  364 
let ?Uk = "?U  {k}" 
53854  365 
from p have pU: "p permutes ?U" 
366 
by blast 

367 
have kU: "?U = insert k ?Uk" 

368 
by blast 

53253  369 
{ 
370 
fix j 

371 
assume j: "j \<in> ?Uk" 

33175  372 
from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j" 
53253  373 
by simp_all 
374 
} 

64272  375 
then have th1: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk" 
376 
and th2: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?h i $ p i) ?Uk" 

33175  377 
apply  
64272  378 
apply (rule prod.cong, simp_all)+ 
33175  379 
done 
53854  380 
have th3: "finite ?Uk" "k \<notin> ?Uk" 
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" 
385 
apply (rule prod.insert) 

33175  386 
apply simp 
53253  387 
apply blast 
388 
done 

64272  389 
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  390 
by (simp add: field_simps) 
64272  391 
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)" 
53253  392 
by (metis th1 th2) 
64272  393 
also have "\<dots> = prod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + prod (\<lambda>i. ?h i $ p i) (insert k ?Uk)" 
394 
unfolding prod.insert[OF th3] by simp 

395 
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  396 
unfolding kU[symmetric] . 
64272  397 
then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U = 
398 
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  399 
by (simp add: field_simps) 
57418  400 
qed rule 
33175  401 

402 
lemma det_row_mul: 

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

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

53253  405 
c * det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)" 
64267  406 
unfolding det_def vec_lambda_beta sum_distrib_left 
407 
proof (rule sum.cong) 

33175  408 
let ?U = "UNIV :: 'n set" 
409 
let ?pU = "{p. p permutes ?U}" 

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

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

53253  412 
fix p 
413 
assume p: "p \<in> ?pU" 

33175  414 
let ?Uk = "?U  {k}" 
53854  415 
from p have pU: "p permutes ?U" 
416 
by blast 

417 
have kU: "?U = insert k ?Uk" 

418 
by blast 

53253  419 
{ 
420 
fix j 

421 
assume j: "j \<in> ?Uk" 

53854  422 
from j have "?f j $ p j = ?g j $ p j" 
423 
by simp 

53253  424 
} 
64272  425 
then have th1: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk" 
33175  426 
apply  
64272  427 
apply (rule prod.cong) 
53253  428 
apply simp_all 
33175  429 
done 
53854  430 
have th3: "finite ?Uk" "k \<notin> ?Uk" 
431 
by auto 

64272  432 
have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" 
33175  433 
unfolding kU[symmetric] .. 
64272  434 
also have "\<dots> = ?f k $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk" 
435 
apply (rule prod.insert) 

33175  436 
apply simp 
53253  437 
apply blast 
438 
done 

64272  439 
also have "\<dots> = (c*s a k) $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk" 
53253  440 
by (simp add: field_simps) 
64272  441 
also have "\<dots> = c* (a k $ p k * prod (\<lambda>i. ?g i $ p i) ?Uk)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

442 
unfolding th1 by (simp add: ac_simps) 
64272  443 
also have "\<dots> = c* (prod (\<lambda>i. ?g i $ p i) (insert k ?Uk))" 
444 
unfolding prod.insert[OF th3] by simp 

445 
finally have "prod (\<lambda>i. ?f i $ p i) ?U = c* (prod (\<lambda>i. ?g i $ p i) ?U)" 

53253  446 
unfolding kU[symmetric] . 
64272  447 
then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U = 
448 
c * (of_int (sign p) * prod (\<lambda>i. ?g i $ p i) ?U)" 

36350  449 
by (simp add: field_simps) 
57418  450 
qed rule 
33175  451 

452 
lemma det_row_0: 

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

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

53253  455 
using det_row_mul[of k 0 "\<lambda>i. 1" b] 
456 
apply simp 

457 
apply (simp only: vector_smult_lzero) 

458 
done 

33175  459 

460 
lemma det_row_operation: 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

461 
fixes A :: "'a::{comm_ring_1}^'n^'n" 
33175  462 
assumes ij: "i \<noteq> j" 
463 
shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A" 

53253  464 
proof  
33175  465 
let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n" 
466 
have th: "row i ?Z = row j ?Z" by (vector row_def) 

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

468 
by (vector row_def) 

469 
show ?thesis 

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

471 
by simp 

472 
qed 

473 

474 
lemma det_row_span: 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

475 
fixes A :: "'a::{field}^'n^'n" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

476 
assumes x: "x \<in> vec.span {row j A j. j \<noteq> i}" 
33175  477 
shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

478 
using x 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

479 
proof (induction rule: vec.span_induct_alt) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

480 
case 1 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

481 
then show ?case 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

482 
by (rule cong[of det, OF refl]) (vector row_def) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

483 
next 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

484 
case (2 c z y) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

485 
note zS = 2(1) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

486 
and Py = 2(2) 
33175  487 
let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)" 
488 
let ?P = "\<lambda>x. ?d (row i A + x) = det A" 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

489 
from zS obtain j where j: "z = row j A" "i \<noteq> j" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

490 
by blast 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

491 
let ?w = "row i A + y" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

492 
have th0: "row i A + (c*s z + y) = ?w + c*s z" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

493 
by vector 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

494 
have thz: "?d z = 0" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

495 
apply (rule det_identical_rows[OF j(2)]) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

496 
using j 
53253  497 
apply (vector row_def) 
498 
done 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

499 
have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

500 
unfolding th0 .. 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

501 
then show ?case 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

502 
unfolding thz Py det_row_mul[of i] det_row_add[of i] 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

503 
by simp 
33175  504 
qed 
505 

67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

506 
lemma matrix_id [simp]: "det (matrix id) = 1" 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

507 
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

508 

c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

509 
lemma det_matrix_scaleR [simp]: "det (matrix ((( *\<^sub>R) r)) :: real^'n^'n) = r ^ CARD('n::finite)" 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

510 
apply (subst det_diagonal) 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

511 
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

512 
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

513 
done 
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

514 

60420  515 
text \<open> 
53854  516 
May as well do this, though it's a bit unsatisfactory since it ignores 
517 
exact duplicates by considering the rows/columns as a set. 

60420  518 
\<close> 
33175  519 

520 
lemma det_dependent_rows: 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

521 
fixes A:: "'a::{field}^'n^'n" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

522 
assumes d: "vec.dependent (rows A)" 
33175  523 
shows "det A = 0" 
53253  524 
proof  
33175  525 
let ?U = "UNIV :: 'n set" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

526 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

527 
unfolding vec.dependent_def rows_def by blast 
53253  528 
{ 
529 
fix j k 

530 
assume jk: "j \<noteq> k" and c: "row j A = row k A" 

531 
from det_identical_rows[OF jk c] have ?thesis . 

532 
} 

33175  533 
moreover 
53253  534 
{ 
535 
assume H: "\<And> i j. i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A" 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

536 
have th0: " row i A \<in> vec.span {row j Aj. j \<noteq> i}" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

537 
apply (rule vec.span_neg) 
33175  538 
apply (rule set_rev_mp) 
539 
apply (rule i) 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

540 
apply (rule vec.span_mono) 
53253  541 
using H i 
542 
apply (auto simp add: rows_def) 

543 
done 

33175  544 
from det_row_span[OF th0] 
545 
have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)" 

546 
unfolding right_minus vector_smult_lzero .. 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

547 
with det_row_mul[of i "0::'a" "\<lambda>i. 1"] 
53253  548 
have "det A = 0" by simp 
549 
} 

33175  550 
ultimately show ?thesis by blast 
551 
qed 

552 

53253  553 
lemma det_dependent_columns: 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

554 
assumes d: "vec.dependent (columns (A::real^'n^'n))" 
53253  555 
shows "det A = 0" 
556 
by (metis d det_dependent_rows rows_transpose det_transpose) 

33175  557 

60420  558 
text \<open>Multilinearity and the multiplication formula.\<close> 
33175  559 

44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

560 
lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" 
53253  561 
by (rule iffD1[OF vec_lambda_unique]) vector 
33175  562 

64267  563 
lemma det_linear_row_sum: 
33175  564 
assumes fS: "finite S" 
64267  565 
shows "det ((\<chi> i. if i = k then sum (a i) S else c i)::'a::comm_ring_1^'n^'n) = 
566 
sum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S" 

53253  567 
proof (induct rule: finite_induct[OF fS]) 
568 
case 1 

569 
then show ?case 

570 
apply simp 

64267  571 
unfolding sum.empty det_row_0[of k] 
53253  572 
apply rule 
573 
done 

33175  574 
next 
575 
case (2 x F) 

53253  576 
then show ?case 
577 
by (simp add: det_row_add cong del: if_weak_cong) 

33175  578 
qed 
579 

580 
lemma finite_bounded_functions: 

581 
assumes fS: "finite S" 

582 
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  583 
proof (induct k) 
33175  584 
case 0 
53854  585 
have th: "{f. \<forall>i. f i = i} = {id}" 
586 
by auto 

587 
show ?case 

588 
by (auto simp add: th) 

33175  589 
next 
590 
case (Suc k) 

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

592 
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)})" 

593 
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)}" 

594 
apply (auto simp add: image_iff) 

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

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

44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44260
diff
changeset

597 
apply auto 
33175  598 
done 
599 
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] 

53854  600 
show ?case 
601 
by metis 

33175  602 
qed 
603 

604 

64267  605 
lemma det_linear_rows_sum_lemma: 
53854  606 
assumes fS: "finite S" 
607 
and fT: "finite T" 

64267  608 
shows "det ((\<chi> i. if i \<in> T then sum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = 
609 
sum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)) 

53253  610 
{f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}" 
611 
using fT 

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

33175  613 
case empty 
53253  614 
have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)" 
615 
by vector 

53854  616 
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

617 
unfolding th0 by (simp add: eq_id_iff) 
33175  618 
next 
619 
case (insert z T a c) 

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

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

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

623 
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

624 
let ?c = "\<lambda>j i. if i = z then a i j else c i" 
53253  625 
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)" 
626 
by simp 

33175  627 
have thif2: "\<And>a b c d e. (if a then b else if c then d else e) = 
53253  628 
(if c then (if a then b else d) else (if a then b else e))" 
629 
by simp 

60420  630 
from \<open>z \<notin> T\<close> have nz: "\<And>i. i \<in> T \<Longrightarrow> i = z \<longleftrightarrow> False" 
53253  631 
by auto 
64267  632 
have "det (\<chi> i. if i \<in> insert z T then sum (a i) S else c i) = 
633 
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  634 
unfolding insert_iff thif .. 
64267  635 
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))" 
636 
unfolding det_linear_row_sum[OF fS] 

33175  637 
apply (subst thif2) 
53253  638 
using nz 
639 
apply (simp cong del: if_weak_cong cong add: if_cong) 

640 
done 

33175  641 
finally have tha: 
64267  642 
"det (\<chi> i. if i \<in> insert z T then sum (a i) S else c i) = 
33175  643 
(\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i) 
644 
else if i = z then a i j 

645 
else c i))" 

64267  646 
unfolding insert.hyps unfolding sum.cartesian_product by blast 
33175  647 
show ?case unfolding tha 
60420  648 
using \<open>z \<notin> T\<close> 
64267  649 
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

650 
(auto intro!: cong[OF refl[of det]] simp: vec_eq_iff) 
33175  651 
qed 
652 

64267  653 
lemma det_linear_rows_sum: 
53854  654 
fixes S :: "'n::finite set" 
655 
assumes fS: "finite S" 

64267  656 
shows "det (\<chi> i. sum (a i) S) = 
657 
sum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}" 

53253  658 
proof  
659 
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)" 

660 
by vector 

64267  661 
from det_linear_rows_sum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] 
53253  662 
show ?thesis by simp 
33175  663 
qed 
664 

64267  665 
lemma matrix_mul_sum_alt: 
34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

666 
fixes A B :: "'a::comm_ring_1^'n^'n" 
64267  667 
shows "A ** B = (\<chi> i. sum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))" 
668 
by (vector matrix_matrix_mult_def sum_component) 

33175  669 

670 
lemma det_rows_mul: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

671 
"det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) = 
64272  672 
prod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)" 
673 
proof (simp add: det_def sum_distrib_left cong add: prod.cong, rule sum.cong) 

33175  674 
let ?U = "UNIV :: 'n set" 
675 
let ?PU = "{p. p permutes ?U}" 

53253  676 
fix p 
677 
assume pU: "p \<in> ?PU" 

33175  678 
let ?s = "of_int (sign p)" 
53253  679 
from pU have p: "p permutes ?U" 
680 
by blast 

64272  681 
have "prod (\<lambda>i. c i * a i $ p i) ?U = prod c ?U * prod (\<lambda>i. a i $ p i) ?U" 
682 
unfolding prod.distrib .. 

33175  683 
then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) = 
64272  684 
prod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" 
53854  685 
by (simp add: field_simps) 
57418  686 
qed rule 
33175  687 

688 
lemma det_mul: 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

689 
fixes A B :: "'a::comm_ring_1^'n^'n" 
33175  690 
shows "det (A ** B) = det A * det B" 
53253  691 
proof  
33175  692 
let ?U = "UNIV :: 'n set" 
693 
let ?F = "{f. (\<forall>i\<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}" 

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

53854  695 
have fU: "finite ?U" 
696 
by simp 

697 
have fF: "finite ?F" 

698 
by (rule finite) 

53253  699 
{ 
700 
fix p 

701 
assume p: "p permutes ?U" 

33175  702 
have "p \<in> ?F" unfolding mem_Collect_eq permutes_in_image[OF p] 
53253  703 
using p[unfolded permutes_def] by simp 
704 
} 

53854  705 
then have PUF: "?PU \<subseteq> ?F" by blast 
53253  706 
{ 
707 
fix f 

708 
assume fPU: "f \<in> ?F  ?PU" 

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

53253  711 
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)" 
712 
unfolding permutes_def by auto 

33175  713 

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

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

53253  716 
{ 
717 
assume fni: "\<not> inj_on f ?U" 

33175  718 
then obtain i j where ij: "f i = f j" "i \<noteq> j" 
719 
unfolding inj_on_def by blast 

720 
from ij 

53854  721 
have rth: "row i ?B = row j ?B" 
722 
by (vector row_def) 

33175  723 
from det_identical_rows[OF ij(2) rth] 
724 
have "det (\<chi> i. A$i$f i *s B$f i) = 0" 

53253  725 
unfolding det_rows_mul by simp 
726 
} 

33175  727 
moreover 
53253  728 
{ 
729 
assume fi: "inj_on f ?U" 

33175  730 
from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j" 
731 
unfolding inj_on_def by metis 

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

53253  733 
{ 
734 
fix y 

53854  735 
from fs f have "\<exists>x. f x = y" 
736 
by blast 

737 
then obtain x where x: "f x = y" 

738 
by blast 

53253  739 
{ 
740 
fix z 

741 
assume z: "f z = y" 

53854  742 
from fith x z have "z = x" 
743 
by metis 

53253  744 
} 
53854  745 
with x have "\<exists>!x. f x = y" 
746 
by blast 

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

53253  750 
} 
53854  751 
ultimately have "det (\<chi> i. A$i$f i *s B$f i) = 0" 
752 
by blast 

53253  753 
} 
53854  754 
then have zth: "\<forall> f\<in> ?F  ?PU. det (\<chi> i. A$i$f i *s B$f i) = 0" 
53253  755 
by simp 
756 
{ 

757 
fix p 

758 
assume pU: "p \<in> ?PU" 

53854  759 
from pU have p: "p permutes ?U" 
760 
by blast 

33175  761 
let ?s = "\<lambda>p. of_int (sign p)" 
53253  762 
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  763 
have "(sum (\<lambda>q. ?s q * 
53253  764 
(\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = 
64267  765 
(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  766 
unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] 
64267  767 
proof (rule sum.cong) 
53253  768 
fix q 
769 
assume qU: "q \<in> ?PU" 

53854  770 
then have q: "q permutes ?U" 
771 
by blast 

33175  772 
from p q have pp: "permutation p" and pq: "permutation q" 
773 
unfolding permutation_permutes by auto 

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

775 
"\<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

776 
unfolding mult.assoc[symmetric] 
53854  777 
unfolding of_int_mult[symmetric] 
33175  778 
by (simp_all add: sign_idempotent) 
53854  779 
have ths: "?s q = ?s p * ?s (q \<circ> inv p)" 
33175  780 
using pp pq permutation_inverse[OF pp] sign_inverse[OF pp] 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

781 
by (simp add: th00 ac_simps sign_idempotent sign_compose) 
64272  782 
have th001: "prod (\<lambda>i. B$i$ q (inv p i)) ?U = prod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U" 
783 
by (rule prod_permute[OF p]) 

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

785 
prod (\<lambda>i. A$i$p i) ?U * prod (\<lambda>i. B$i$ q (inv p i)) ?U" 

786 
unfolding th001 prod.distrib[symmetric] o_def permutes_inverses[OF p] 

787 
apply (rule prod.cong[OF refl]) 

53253  788 
using permutes_in_image[OF q] 
789 
apply vector 

790 
done 

64272  791 
show "?s q * prod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = 
792 
?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  793 
using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] 
36350  794 
by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose) 
57418  795 
qed rule 
33175  796 
} 
64267  797 
then have th2: "sum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B" 
798 
unfolding det_def sum_product 

799 
by (rule sum.cong [OF refl]) 

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

801 
unfolding matrix_mul_sum_alt det_linear_rows_sum[OF fU] 

53854  802 
by simp 
64267  803 
also have "\<dots> = sum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU" 
804 
using sum.mono_neutral_cong_left[OF fF PUF zth, symmetric] 

33175  805 
unfolding det_rows_mul by auto 
806 
finally show ?thesis unfolding th2 . 

807 
qed 

808 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

809 

67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

810 
subsection \<open>Relation to invertibility.\<close> 
33175  811 

812 
lemma invertible_det_nz: 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

813 
fixes A::"'a::{field}^'n^'n" 
33175  814 
shows "invertible A \<longleftrightarrow> det A \<noteq> 0" 
53253  815 
proof  
816 
{ 

817 
assume "invertible A" 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

818 
then obtain B :: "'a^'n^'n" where B: "A ** B = mat 1" 
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

819 
unfolding invertible_right_inverse by blast 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

820 
then have "det (A ** B) = det (mat 1 :: 'a^'n^'n)" 
53854  821 
by simp 
822 
then have "det A \<noteq> 0" 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

823 
by (simp add: det_mul) algebra 
53253  824 
} 
33175  825 
moreover 
53253  826 
{ 
827 
assume H: "\<not> invertible A" 

33175  828 
let ?U = "UNIV :: 'n set" 
53854  829 
have fU: "finite ?U" 
830 
by simp 

64267  831 
from H obtain c i where c: "sum (\<lambda>i. c i *s row i A) ?U = 0" 
53854  832 
and iU: "i \<in> ?U" 
833 
and ci: "c i \<noteq> 0" 

67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

834 
unfolding invertible_right_inverse 
53854  835 
unfolding matrix_right_invertible_independent_rows 
836 
by blast 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

837 
have *: "\<And>(a::'a^'n) b. a + b = 0 \<Longrightarrow> a = b" 
67399  838 
apply (drule_tac f="(+) ( a)" in cong[OF refl]) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

839 
apply (simp only: ab_left_minus add.assoc[symmetric]) 
33175  840 
apply simp 
841 
done 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

842 
from c ci 
64267  843 
have thr0: " row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U  {i})" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

844 
unfolding sum.remove[OF fU iU] sum_cmul 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

845 
apply  
33175  846 
apply (rule vector_mul_lcancel_imp[OF ci]) 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

847 
apply (auto simp add: field_simps) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

848 
unfolding * 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

849 
apply rule 
53854  850 
done 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

851 
have thr: " row i A \<in> vec.span {row j A j. j \<noteq> i}" 
33175  852 
unfolding thr0 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

853 
apply (rule vec.span_sum) 
33175  854 
apply simp 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

855 
apply (rule vec.span_scale[folded scalar_mult_eq_scaleR])+ 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

856 
apply (rule vec.span_base) 
33175  857 
apply auto 
858 
done 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

859 
let ?B = "(\<chi> k. if k = i then 0 else row k A) :: 'a^'n^'n" 
33175  860 
have thrb: "row i ?B = 0" using iU by (vector row_def) 
861 
have "det A = 0" 

862 
unfolding det_row_span[OF thr, symmetric] right_minus 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

863 
unfolding det_zero_row(2)[OF thrb] .. 
53253  864 
} 
53854  865 
ultimately show ?thesis 
866 
by blast 

33175  867 
qed 
868 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

869 
lemma det_nz_iff_inj_gen: 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

870 
fixes f :: "'a::field^'n \<Rightarrow> 'a::field^'n" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

871 
assumes "Vector_Spaces.linear ( *s) ( *s) f" 
67990  872 
shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f" 
873 
proof 

874 
assume "det (matrix f) \<noteq> 0" 

875 
then show "inj f" 

876 
using assms invertible_det_nz inj_matrix_vector_mult by force 

877 
next 

878 
assume "inj f" 

879 
show "det (matrix f) \<noteq> 0" 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

880 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

881 
by (metis assms invertible_det_nz invertible_left_inverse matrix_compose_gen matrix_id_mat_1) 
67990  882 
qed 
883 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

884 
lemma det_nz_iff_inj: 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

885 
fixes f :: "real^'n \<Rightarrow> real^'n" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

886 
assumes "linear f" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

887 
shows "det (matrix f) \<noteq> 0 \<longleftrightarrow> inj f" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

888 
using det_nz_iff_inj_gen[of f] assms 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

889 
unfolding linear_matrix_vector_mul_eq . 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

890 

67990  891 
lemma det_eq_0_rank: 
892 
fixes A :: "real^'n^'n" 

893 
shows "det A = 0 \<longleftrightarrow> rank A < CARD('n)" 

894 
using invertible_det_nz [of A] 

895 
by (auto simp: matrix_left_invertible_injective invertible_left_inverse less_rank_noninjective) 

896 

67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

897 
subsubsection\<open>Invertibility of matrices and corresponding linear functions\<close> 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

898 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

899 
lemma matrix_left_invertible_gen: 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

900 
fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

901 
assumes "Vector_Spaces.linear ( *s) ( *s) f" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

902 
shows "((\<exists>B. B ** matrix f = mat 1) \<longleftrightarrow> (\<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

903 
proof safe 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

904 
fix B 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

905 
assume 1: "B ** matrix f = mat 1" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

906 
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

907 
proof (intro exI conjI) 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

908 
show "Vector_Spaces.linear ( *s) ( *s) (\<lambda>y. B *v y)" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

909 
by (simp add:) 
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

910 
show "(( *v) B) \<circ> f = id" 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

911 
unfolding o_def 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

912 
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

913 
qed 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

914 
next 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

915 
fix g 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

916 
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

917 
then have "matrix g ** matrix f = mat 1" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

918 
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

919 
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

920 
qed 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

921 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

922 
lemma matrix_left_invertible: 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

923 
"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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

924 
using matrix_left_invertible_gen[of f] 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

925 
by (auto simp: linear_matrix_vector_mul_eq) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

926 

493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

927 
lemma matrix_right_invertible_gen: 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

928 
fixes f :: "'a::field^'m \<Rightarrow> 'a^'n" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

929 
assumes "Vector_Spaces.linear ( *s) ( *s) f" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

930 
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

931 
proof safe 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

932 
fix B 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

933 
assume 1: "matrix f ** B = mat 1" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

934 
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

935 
proof (intro exI conjI) 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

936 
show "Vector_Spaces.linear ( *s) ( *s) (( *v) B)" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

937 
by (simp add: ) 
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

938 
show "f \<circ> ( *v) B = id" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

939 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

940 
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

941 
qed 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

942 
next 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

943 
fix g 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

944 
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

945 
then have "matrix f ** matrix g = mat 1" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

946 
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

947 
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

948 
qed 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

949 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

950 
lemma matrix_right_invertible: 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

951 
"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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

952 
using matrix_right_invertible_gen[of f] 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

953 
by (auto simp: linear_matrix_vector_mul_eq) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

954 

493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

955 
lemma matrix_invertible_gen: 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

956 
fixes f :: "'a::field^'m \<Rightarrow> 'a::field^'n" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

957 
assumes "Vector_Spaces.linear ( *s) ( *s) f" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

958 
shows "invertible (matrix f) \<longleftrightarrow> (\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id \<and> g \<circ> f = id)" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

959 
(is "?lhs = ?rhs") 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

960 
proof 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

961 
assume ?lhs then show ?rhs 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

962 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

963 
next 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

964 
assume ?rhs then show ?lhs 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

965 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

966 
qed 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

967 

67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

968 
lemma matrix_invertible: 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

969 
"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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

970 
for f::"real^'m \<Rightarrow> real^'n" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

971 
using matrix_invertible_gen[of f] 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

972 
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

973 

349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

974 
lemma invertible_eq_bij: 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

975 
fixes m :: "'a::field^'m^'n" 
67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

976 
shows "invertible m \<longleftrightarrow> bij (( *v) m)" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

977 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

978 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

979 
vec.linear_injective_left_inverse vec.linear_surjective_right_inverse) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

980 

67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

981 

349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

982 
subsection \<open>Cramer's rule.\<close> 
33175  983 

35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

984 
lemma cramer_lemma_transpose: 
53854  985 
fixes A:: "real^'n^'n" 
986 
and x :: "real^'n" 

64267  987 
shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x$i *s row i A) (UNIV::'n set) 
53854  988 
else row i A)::real^'n^'n) = x$k * det A" 
33175  989 
(is "?lhs = ?rhs") 
53253  990 
proof  
33175  991 
let ?U = "UNIV :: 'n set" 
992 
let ?Uk = "?U  {k}" 

53854  993 
have U: "?U = insert k ?Uk" 
994 
by blast 

995 
have fUk: "finite ?Uk" 

996 
by simp 

997 
have kUk: "k \<notin> ?Uk" 

998 
by simp 

33175  999 
have th00: "\<And>k s. x$k *s row k A + s = (x$k  1) *s row k A + row k A + s" 
36350  1000 
by (vector field_simps) 
53854  1001 
have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" 
1002 
by auto 

33175  1003 
have "(\<chi> i. row i A) = A" by (vector row_def) 
53253  1004 
then have thd1: "det (\<chi> i. row i A) = det A" 
1005 
by simp 

33175  1006 
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" 
1007 
apply (rule det_row_span) 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1008 
apply (rule vec.span_sum) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1009 
apply (rule vec.span_scale) 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1010 
apply (rule vec.span_base) 
33175  1011 
apply auto 
1012 
done 

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

1014 
apply (subst U) 

64267  1015 
unfolding sum.insert[OF fUk kUk] 
33175  1016 
apply (subst th00) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
57418
diff
changeset

1017 
unfolding add.assoc 
33175  1018 
apply (subst det_row_add) 
1019 
unfolding thd0 

1020 
unfolding det_row_mul 

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

53253  1022 
unfolding thd1 
1023 
apply (simp add: field_simps) 

1024 
done 

33175  1025 
qed 
1026 

1027 
lemma cramer_lemma: 

36593
fb69c8cd27bd
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents:
36585
diff
changeset

1028 
fixes A :: "real^'n^'n" 
fb69c8cd27bd
define linear algebra concepts using scaleR instead of (op *s); generalized many lemmas, though a few theorems that used to work on type int^'n are a bit less general
huffman
parents:
36585
diff
changeset

1029 
shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: real^'n^'n) = x$k * det A" 
53253  1030 
proof  
33175  1031 
let ?U = "UNIV :: 'n set" 
64267  1032 
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 HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1033 
by (auto intro: sum.cong) 
53854  1034 
show ?thesis 
67673
c8caefb20564
lots of new material, ultimately related to measure theory
paulson <lp15@cam.ac.uk>
parents:
67399
diff
changeset

1035 
unfolding matrix_mult_sum 
53253  1036 
unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] 
1037 
unfolding *[of "\<lambda>i. x$i"] 

1038 
apply (subst det_transpose[symmetric]) 

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

1040 
apply (vector transpose_def column_def row_def) 

1041 
done 

33175  1042 
qed 
1043 

1044 
lemma cramer: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

1045 
fixes A ::"real^'n^'n" 
33175  1046 
assumes d0: "det A \<noteq> 0" 
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

1047 
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)" 
53253  1048 
proof  
33175  1049 
from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" 
53854  1050 
unfolding invertible_det_nz[symmetric] invertible_def 
1051 
by blast 

1052 
have "(A ** B) *v b = b" 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1053 
by (simp add: B) 
53854  1054 
then have "A *v (B *v b) = b" 
1055 
by (simp add: matrix_vector_mul_assoc) 

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

1057 
by blast 

53253  1058 
{ 
1059 
fix x 

1060 
assume x: "A *v x = b" 

1061 
have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)" 

1062 
unfolding x[symmetric] 

1063 
using d0 by (simp add: vec_eq_iff cramer_lemma field_simps) 

1064 
} 

53854  1065 
with xe show ?thesis 
1066 
by auto 

33175  1067 
qed 
1068 

67968  1069 
subsection \<open>Orthogonality of a transformation and matrix\<close> 
33175  1070 

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

1072 

67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

1073 
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

1074 
transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1" 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

1075 

53253  1076 
lemma orthogonal_transformation: 
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1077 
"orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v. norm (f v) = norm v)" 
33175  1078 
unfolding orthogonal_transformation_def 
1079 
apply auto 

1080 
apply (erule_tac x=v in allE)+ 

35542  1081 
apply (simp add: norm_eq_sqrt_inner) 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1082 
apply (simp add: dot_norm linear_add[symmetric]) 
53253  1083 
done 
33175  1084 

67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1085 
lemma orthogonal_transformation_id [simp]: "orthogonal_transformation (\<lambda>x. x)" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1086 
by (simp add: linear_iff orthogonal_transformation_def) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1087 

817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1088 
lemma orthogonal_orthogonal_transformation: 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1089 
"orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1090 
by (simp add: orthogonal_def orthogonal_transformation_def) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1091 

817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1092 
lemma orthogonal_transformation_compose: 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1093 
"\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1094 
by (auto simp add: orthogonal_transformation_def linear_compose) 
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1095 

817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1096 
lemma orthogonal_transformation_neg: 
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1097 
"orthogonal_transformation(\<lambda>x. (f x)) \<longleftrightarrow> orthogonal_transformation f" 
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1098 
by (auto simp: orthogonal_transformation_def dest: linear_compose_neg) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1099 

67981
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

1100 
lemma orthogonal_transformation_scaleR: "orthogonal_transformation f \<Longrightarrow> f (c *\<^sub>R v) = c *\<^sub>R f v" 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

1101 
by (simp add: linear_iff orthogonal_transformation_def) 
349c639e593c
more new theorems on real^1, matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67971
diff
changeset

1102 

67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1103 
lemma orthogonal_transformation_linear: 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1104 
"orthogonal_transformation f \<Longrightarrow> linear f" 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1105 
by (simp add: orthogonal_transformation_def) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1106 

817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1107 
lemma orthogonal_transformation_inj: 
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1108 
"orthogonal_transformation f \<Longrightarrow> inj f" 
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1109 
unfolding orthogonal_transformation_def inj_on_def 
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1110 
by (metis vector_eq) 
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1111 

817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1112 
lemma orthogonal_transformation_surj: 
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1113 
"orthogonal_transformation f \<Longrightarrow> surj f" 
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1114 
for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space" 
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1115 
by (simp add: linear_injective_imp_surjective orthogonal_transformation_inj orthogonal_transformation_linear) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1116 

817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1117 
lemma orthogonal_transformation_bij: 
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1118 
"orthogonal_transformation f \<Longrightarrow> bij f" 
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1119 
for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space" 
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1120 
by (simp add: bij_def orthogonal_transformation_inj orthogonal_transformation_surj) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1121 

817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1122 
lemma orthogonal_transformation_inv: 
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1123 
"orthogonal_transformation f \<Longrightarrow> orthogonal_transformation (inv f)" 
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1124 
for f :: "'a::euclidean_space \<Rightarrow> 'a::euclidean_space" 
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1125 
by (metis (no_types, hide_lams) bijection.inv_right bijection_def inj_linear_imp_inv_linear orthogonal_transformation orthogonal_transformation_bij orthogonal_transformation_inj) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1126 

817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1127 
lemma orthogonal_transformation_norm: 
67733
346cb74e79f6
generalized lemmas about orthogonal transformation
immler
parents:
67683
diff
changeset

1128 
"orthogonal_transformation f \<Longrightarrow> norm (f x) = norm x" 
67683
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1129 
by (metis orthogonal_transformation) 
817944aeac3f
Lots of new material about matrices, etc.
paulson <lp15@cam.ac.uk>
parents:
67673
diff
changeset

1130 

53253  1131 
lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1" 
33175  1132 
by (metis matrix_left_right_inverse orthogonal_matrix_def) 
1133 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

1134 
lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)" 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1135 
by (simp add: orthogonal_matrix_def) 
33175  1136 

1137 
lemma orthogonal_matrix_mul: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

1138 
fixes A :: "real ^'n^'n" 
33175  1139 
assumes oA : "orthogonal_matrix A" 
53253  1140 
and oB: "orthogonal_matrix B" 
33175  1141 
shows "orthogonal_matrix(A ** B)" 
1142 
using oA oB 

35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

1143 
unfolding orthogonal_matrix matrix_transpose_mul 
33175  1144 
apply (subst matrix_mul_assoc) 
1145 
apply (subst matrix_mul_assoc[symmetric]) 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1146 
apply (simp add: ) 
53253  1147 
done 
33175  1148 

1149 
lemma orthogonal_transformation_matrix: 

34291
4e896680897e
finite annotation on cartesian product is now implicit.
hoelzl
parents:
34289
diff
changeset

1150 
fixes f:: "real^'n \<Rightarrow> real^'n" 
33175  1151 
shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)" 
1152 
(is "?lhs \<longleftrightarrow> ?rhs") 

53253  1153 
proof  
33175  1154 
let ?mf = "matrix f" 
1155 
let ?ot = "orthogonal_transformation f" 

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

1157 
have fU: "finite ?U" by simp 

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

53253  1159 
{ 
1160 
assume ot: ?ot 

68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1161 
from ot have lf: "Vector_Spaces.linear ( *s) ( *s) f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w" 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1162 
unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR 
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1163 
by blast+ 
53253  1164 
{ 
1165 
fix i j 

35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

1166 
let ?A = "transpose ?mf ** ?mf" 
33175  1167 
have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" 
1168 
"\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" 

1169 
by simp_all 

63170  1170 
from fd[rule_format, of "axis i 1" "axis j 1", 
1171 
simplified matrix_works[OF lf, symmetric] dot_matrix_vector_mul] 

33175  1172 
have "?A$i$j = ?m1 $ i $ j" 
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
47108
diff
changeset

1173 
by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def 
64267  1174 
th0 sum.delta[OF fU] mat_def axis_def) 
53253  1175 
} 
53854  1176 
then have "orthogonal_matrix ?mf" 
1177 
unfolding orthogonal_matrix 

53253  1178 
by vector 
53854  1179 
with lf have ?rhs 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1180 
unfolding linear_def scalar_mult_eq_scaleR 
53854  1181 
by blast 
53253  1182 
} 
33175  1183 
moreover 
53253  1184 
{ 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1185 
assume lf: "Vector_Spaces.linear ( *s) ( *s) f" and om: "orthogonal_matrix ?mf" 
33175  1186 
from lf om have ?lhs 
63170  1187 
apply (simp only: orthogonal_matrix_def norm_eq orthogonal_transformation) 
1188 
apply (simp only: matrix_works[OF lf, symmetric]) 

33175  1189 
apply (subst dot_matrix_vector_mul) 
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOLAnalysis accordingly
immler
parents:
67990
diff
changeset

1190 
apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR) 
53253  1191 
done 
220f306f5c4e
tuned proofs;
wenzelm
