author  nipkow 
Mon, 17 Oct 2016 17:33:07 +0200  
changeset 64272  f76b6dda2e56 
parent 64267  b9a1486e79be 
child 66453  cc19f7ca2ed6 
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 
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

10 
"~~/src/HOL/Library/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) 
64267  32 
apply (subst sum.commute) 
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 

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

57 
lemma det_transpose: "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 

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

196 
lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" 
53253  197 
proof  
33175  198 
let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n" 
199 
let ?U = "UNIV :: 'n set" 

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

53253  201 
{ 
202 
fix i 

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

53854  204 
have "?f i i = 1" 
205 
using i by (vector mat_def) 

53253  206 
} 
64272  207 
then have th: "prod (\<lambda>i. ?f i i) ?U = prod (\<lambda>x. 1) ?U" 
208 
by (auto intro: prod.cong) 

53253  209 
{ 
210 
fix i j 

211 
assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j" 

53854  212 
have "?f i j = 0" using i j ij 
213 
by (vector mat_def) 

53253  214 
} 
64272  215 
then have "det ?A = prod (\<lambda>i. ?f i i) ?U" 
53854  216 
using det_diagonal by blast 
217 
also have "\<dots> = 1" 

64272  218 
unfolding th prod.neutral_const .. 
33175  219 
finally show ?thesis . 
220 
qed 

221 

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

222 
lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" 
64272  223 
by (simp add: det_def prod_zero) 
33175  224 

225 
lemma det_permute_rows: 

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

226 
fixes A :: "'a::comm_ring_1^'n^'n" 
33175  227 
assumes p: "p permutes (UNIV :: 'n::finite set)" 
53854  228 
shows "det (\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" 
64267  229 
apply (simp add: det_def sum_distrib_left mult.assoc[symmetric]) 
33175  230 
apply (subst sum_permutations_compose_right[OF p]) 
64267  231 
proof (rule sum.cong) 
33175  232 
let ?U = "UNIV :: 'n set" 
233 
let ?PU = "{p. p permutes ?U}" 

53253  234 
fix q 
235 
assume qPU: "q \<in> ?PU" 

53854  236 
have fU: "finite ?U" 
237 
by simp 

53253  238 
from qPU have q: "q permutes ?U" 
239 
by blast 

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

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

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

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

53253  246 
by (simp only: o_def) 
64272  247 
also have "\<dots> = prod (\<lambda>i. A$i$q i) ?U" 
53253  248 
by (simp only: o_def permutes_inverses[OF p]) 
64272  249 
finally have thp: "prod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = prod (\<lambda>i. A$i$q i) ?U" 
53253  250 
by blast 
64272  251 
show "of_int (sign (q \<circ> p)) * prod (\<lambda>i. A$ p i$ (q \<circ> p) i) ?U = 
252 
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

253 
by (simp only: thp sign_compose[OF qp pp] mult.commute of_int_mult) 
57418  254 
qed rule 
33175  255 

256 
lemma det_permute_columns: 

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

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

53253  260 
proof  
33175  261 
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

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

263 
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

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

266 
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

267 
by (simp add: transpose_def vec_eq_iff) 
53854  268 
ultimately show ?thesis 
269 
by simp 

33175  270 
qed 
271 

272 
lemma det_identical_rows: 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34291
diff
changeset

273 
fixes A :: "'a::linordered_idom^'n^'n" 
33175  274 
assumes ij: "i \<noteq> j" 
53253  275 
and r: "row i A = row j A" 
33175  276 
shows "det A = 0" 
277 
proof 

53253  278 
have tha: "\<And>(a::'a) b. a = b \<Longrightarrow> b =  a \<Longrightarrow> a = 0" 
33175  279 
by simp 
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
44457
diff
changeset

280 
have th1: "of_int (1) =  1" by simp 
33175  281 
let ?p = "Fun.swap i j id" 
282 
let ?A = "\<chi> i. A $ ?p i" 

56545  283 
from r have "A = ?A" by (simp add: vec_eq_iff row_def Fun.swap_def) 
53253  284 
then have "det A = det ?A" by simp 
33175  285 
moreover have "det A =  det ?A" 
286 
by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1) 

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

288 
qed 

289 

290 
lemma det_identical_columns: 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34291
diff
changeset

291 
fixes A :: "'a::linordered_idom^'n^'n" 
33175  292 
assumes ij: "i \<noteq> j" 
53253  293 
and r: "column i A = column j A" 
33175  294 
shows "det A = 0" 
53253  295 
apply (subst det_transpose[symmetric]) 
296 
apply (rule det_identical_rows[OF ij]) 

297 
apply (metis row_transpose r) 

298 
done 

33175  299 

300 
lemma det_zero_row: 

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

301 
fixes A :: "'a::{idom, ring_char_0}^'n^'n" 
33175  302 
assumes r: "row i A = 0" 
303 
shows "det A = 0" 

53253  304 
using r 
305 
apply (simp add: row_def det_def vec_eq_iff) 

64267  306 
apply (rule sum.neutral) 
53253  307 
apply (auto simp: sign_nz) 
308 
done 

33175  309 

310 
lemma det_zero_column: 

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

311 
fixes A :: "'a::{idom,ring_char_0}^'n^'n" 
33175  312 
assumes r: "column i A = 0" 
313 
shows "det A = 0" 

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

314 
apply (subst det_transpose[symmetric]) 
33175  315 
apply (rule det_zero_row [of i]) 
53253  316 
apply (metis row_transpose r) 
317 
done 

33175  318 

319 
lemma det_row_add: 

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

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

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

64267  324 
unfolding det_def vec_lambda_beta sum.distrib[symmetric] 
325 
proof (rule sum.cong) 

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

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

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

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

53253  331 
fix p 
332 
assume p: "p \<in> ?pU" 

33175  333 
let ?Uk = "?U  {k}" 
53854  334 
from p have pU: "p permutes ?U" 
335 
by blast 

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

337 
by blast 

53253  338 
{ 
339 
fix j 

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

33175  341 
from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j" 
53253  342 
by simp_all 
343 
} 

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

33175  346 
apply  
64272  347 
apply (rule prod.cong, simp_all)+ 
33175  348 
done 
53854  349 
have th3: "finite ?Uk" "k \<notin> ?Uk" 
350 
by auto 

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

33175  355 
apply simp 
53253  356 
apply blast 
357 
done 

64272  358 
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  359 
by (simp add: field_simps) 
64272  360 
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  361 
by (metis th1 th2) 
64272  362 
also have "\<dots> = prod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + prod (\<lambda>i. ?h i $ p i) (insert k ?Uk)" 
363 
unfolding prod.insert[OF th3] by simp 

364 
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  365 
unfolding kU[symmetric] . 
64272  366 
then show "of_int (sign p) * prod (\<lambda>i. ?f i $ p i) ?U = 
367 
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  368 
by (simp add: field_simps) 
57418  369 
qed rule 
33175  370 

371 
lemma det_row_mul: 

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

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

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

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

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

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

53253  381 
fix p 
382 
assume p: "p \<in> ?pU" 

33175  383 
let ?Uk = "?U  {k}" 
53854  384 
from p have pU: "p permutes ?U" 
385 
by blast 

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

387 
by blast 

53253  388 
{ 
389 
fix j 

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

53854  391 
from j have "?f j $ p j = ?g j $ p j" 
392 
by simp 

53253  393 
} 
64272  394 
then have th1: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk" 
33175  395 
apply  
64272  396 
apply (rule prod.cong) 
53253  397 
apply simp_all 
33175  398 
done 
53854  399 
have th3: "finite ?Uk" "k \<notin> ?Uk" 
400 
by auto 

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

33175  405 
apply simp 
53253  406 
apply blast 
407 
done 

64272  408 
also have "\<dots> = (c*s a k) $ p k * prod (\<lambda>i. ?f i $ p i) ?Uk" 
53253  409 
by (simp add: field_simps) 
64272  410 
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

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

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

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

36350  418 
by (simp add: field_simps) 
57418  419 
qed rule 
33175  420 

421 
lemma det_row_0: 

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

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

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

426 
apply (simp only: vector_smult_lzero) 

427 
done 

33175  428 

429 
lemma det_row_operation: 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34291
diff
changeset

430 
fixes A :: "'a::linordered_idom^'n^'n" 
33175  431 
assumes ij: "i \<noteq> j" 
432 
shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A" 

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

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

437 
by (vector row_def) 

438 
show ?thesis 

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

440 
by simp 

441 
qed 

442 

443 
lemma det_row_span: 

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

444 
fixes A :: "real^'n^'n" 
33175  445 
assumes x: "x \<in> span {row j A j. j \<noteq> i}" 
446 
shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A" 

53253  447 
proof  
33175  448 
let ?U = "UNIV :: 'n set" 
449 
let ?S = "{row j A j. j \<noteq> i}" 

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

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

53253  452 
{ 
453 
fix k 

53854  454 
have "(if k = i then row i A + 0 else row k A) = row k A" 
455 
by simp 

53253  456 
} 
33175  457 
then have P0: "?P 0" 
458 
apply  

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

53253  460 
apply (vector row_def) 
461 
done 

33175  462 
moreover 
53253  463 
{ 
464 
fix c z y 

465 
assume zS: "z \<in> ?S" and Py: "?P y" 

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

33175  468 
let ?w = "row i A + y" 
53854  469 
have th0: "row i A + (c*s z + y) = ?w + c*s z" 
470 
by vector 

33175  471 
have thz: "?d z = 0" 
472 
apply (rule det_identical_rows[OF j(2)]) 

53253  473 
using j 
474 
apply (vector row_def) 

475 
done 

476 
have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" 

477 
unfolding th0 .. 

478 
then have "?P (c*s z + y)" 

479 
unfolding thz Py det_row_mul[of i] det_row_add[of i] 

480 
by simp 

481 
} 

33175  482 
ultimately show ?thesis 
483 
apply  

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

484 
apply (rule span_induct_alt[of ?P ?S, OF P0, folded scalar_mult_eq_scaleR]) 
33175  485 
apply blast 
486 
apply (rule x) 

487 
done 

488 
qed 

489 

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

60420  493 
\<close> 
33175  494 

495 
lemma det_dependent_rows: 

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

496 
fixes A:: "real^'n^'n" 
33175  497 
assumes d: "dependent (rows A)" 
498 
shows "det A = 0" 

53253  499 
proof  
33175  500 
let ?U = "UNIV :: 'n set" 
501 
from d obtain i where i: "row i A \<in> span (rows A  {row i A})" 

502 
unfolding dependent_def rows_def by blast 

53253  503 
{ 
504 
fix j k 

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

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

507 
} 

33175  508 
moreover 
53253  509 
{ 
510 
assume H: "\<And> i j. i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A" 

33175  511 
have th0: " row i A \<in> span {row j Aj. j \<noteq> i}" 
512 
apply (rule span_neg) 

513 
apply (rule set_rev_mp) 

514 
apply (rule i) 

515 
apply (rule span_mono) 

53253  516 
using H i 
517 
apply (auto simp add: rows_def) 

518 
done 

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

521 
unfolding right_minus vector_smult_lzero .. 

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

522 
with det_row_mul[of i "0::real" "\<lambda>i. 1"] 
53253  523 
have "det A = 0" by simp 
524 
} 

33175  525 
ultimately show ?thesis by blast 
526 
qed 

527 

53253  528 
lemma det_dependent_columns: 
529 
assumes d: "dependent (columns (A::real^'n^'n))" 

530 
shows "det A = 0" 

531 
by (metis d det_dependent_rows rows_transpose det_transpose) 

33175  532 

60420  533 
text \<open>Multilinearity and the multiplication formula.\<close> 
33175  534 

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

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

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

53253  542 
proof (induct rule: finite_induct[OF fS]) 
543 
case 1 

544 
then show ?case 

545 
apply simp 

64267  546 
unfolding sum.empty det_row_0[of k] 
53253  547 
apply rule 
548 
done 

33175  549 
next 
550 
case (2 x F) 

53253  551 
then show ?case 
552 
by (simp add: det_row_add cong del: if_weak_cong) 

33175  553 
qed 
554 

555 
lemma finite_bounded_functions: 

556 
assumes fS: "finite S" 

557 
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  558 
proof (induct k) 
33175  559 
case 0 
53854  560 
have th: "{f. \<forall>i. f i = i} = {id}" 
561 
by auto 

562 
show ?case 

563 
by (auto simp add: th) 

33175  564 
next 
565 
case (Suc k) 

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

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

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

569 
apply (auto simp add: image_iff) 

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

571 
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

572 
apply auto 
33175  573 
done 
574 
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] 

53854  575 
show ?case 
576 
by metis 

33175  577 
qed 
578 

579 

64267  580 
lemma det_linear_rows_sum_lemma: 
53854  581 
assumes fS: "finite S" 
582 
and fT: "finite T" 

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

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

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

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

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

592 
unfolding th0 by (simp add: eq_id_iff) 
33175  593 
next 
594 
case (insert z T a c) 

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

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

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

598 
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

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

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

60420  605 
from \<open>z \<notin> T\<close> have nz: "\<And>i. i \<in> T \<Longrightarrow> i = z \<longleftrightarrow> False" 
53253  606 
by auto 
64267  607 
have "det (\<chi> i. if i \<in> insert z T then sum (a i) S else c i) = 
608 
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  609 
unfolding insert_iff thif .. 
64267  610 
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))" 
611 
unfolding det_linear_row_sum[OF fS] 

33175  612 
apply (subst thif2) 
53253  613 
using nz 
614 
apply (simp cong del: if_weak_cong cong add: if_cong) 

615 
done 

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

620 
else c i))" 

64267  621 
unfolding insert.hyps unfolding sum.cartesian_product by blast 
33175  622 
show ?case unfolding tha 
60420  623 
using \<open>z \<notin> T\<close> 
64267  624 
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

625 
(auto intro!: cong[OF refl[of det]] simp: vec_eq_iff) 
33175  626 
qed 
627 

64267  628 
lemma det_linear_rows_sum: 
53854  629 
fixes S :: "'n::finite set" 
630 
assumes fS: "finite S" 

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

53253  633 
proof  
634 
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)" 

635 
by vector 

64267  636 
from det_linear_rows_sum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] 
53253  637 
show ?thesis by simp 
33175  638 
qed 
639 

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

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

33175  644 

645 
lemma det_rows_mul: 

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

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

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

53253  651 
fix p 
652 
assume pU: "p \<in> ?PU" 

33175  653 
let ?s = "of_int (sign p)" 
53253  654 
from pU have p: "p permutes ?U" 
655 
by blast 

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

33175  658 
then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) = 
64272  659 
prod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" 
53854  660 
by (simp add: field_simps) 
57418  661 
qed rule 
33175  662 

663 
lemma det_mul: 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34291
diff
changeset

664 
fixes A B :: "'a::linordered_idom^'n^'n" 
33175  665 
shows "det (A ** B) = det A * det B" 
53253  666 
proof  
33175  667 
let ?U = "UNIV :: 'n set" 
668 
let ?F = "{f. (\<forall>i\<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}" 

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

53854  670 
have fU: "finite ?U" 
671 
by simp 

672 
have fF: "finite ?F" 

673 
by (rule finite) 

53253  674 
{ 
675 
fix p 

676 
assume p: "p permutes ?U" 

33175  677 
have "p \<in> ?F" unfolding mem_Collect_eq permutes_in_image[OF p] 
53253  678 
using p[unfolded permutes_def] by simp 
679 
} 

53854  680 
then have PUF: "?PU \<subseteq> ?F" by blast 
53253  681 
{ 
682 
fix f 

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

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

53253  686 
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)" 
687 
unfolding permutes_def by auto 

33175  688 

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

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

53253  691 
{ 
692 
assume fni: "\<not> inj_on f ?U" 

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

695 
from ij 

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

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

53253  700 
unfolding det_rows_mul by simp 
701 
} 

33175  702 
moreover 
53253  703 
{ 
704 
assume fi: "inj_on f ?U" 

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

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

53253  708 
{ 
709 
fix y 

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

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

713 
by blast 

53253  714 
{ 
715 
fix z 

716 
assume z: "f z = y" 

53854  717 
from fith x z have "z = x" 
718 
by metis 

53253  719 
} 
53854  720 
with x have "\<exists>!x. f x = y" 
721 
by blast 

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

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

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

732 
fix p 

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

53854  734 
from pU have p: "p permutes ?U" 
735 
by blast 

33175  736 
let ?s = "\<lambda>p. of_int (sign p)" 
53253  737 
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  738 
have "(sum (\<lambda>q. ?s q * 
53253  739 
(\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = 
64267  740 
(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  741 
unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] 
64267  742 
proof (rule sum.cong) 
53253  743 
fix q 
744 
assume qU: "q \<in> ?PU" 

53854  745 
then have q: "q permutes ?U" 
746 
by blast 

33175  747 
from p q have pp: "permutation p" and pq: "permutation q" 
748 
unfolding permutation_permutes by auto 

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

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

751 
unfolding mult.assoc[symmetric] 
53854  752 
unfolding of_int_mult[symmetric] 
33175  753 
by (simp_all add: sign_idempotent) 
53854  754 
have ths: "?s q = ?s p * ?s (q \<circ> inv p)" 
33175  755 
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

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

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

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

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

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

53253  763 
using permutes_in_image[OF q] 
764 
apply vector 

765 
done 

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

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

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

776 
unfolding matrix_mul_sum_alt det_linear_rows_sum[OF fU] 

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

33175  780 
unfolding det_rows_mul by auto 
781 
finally show ?thesis unfolding th2 . 

782 
qed 

783 

60420  784 
text \<open>Relation to invertibility.\<close> 
33175  785 

786 
lemma invertible_left_inverse: 

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

787 
fixes A :: "real^'n^'n" 
33175  788 
shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). B** A = mat 1)" 
789 
by (metis invertible_def matrix_left_right_inverse) 

790 

791 
lemma invertible_righ_inverse: 

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

792 
fixes A :: "real^'n^'n" 
33175  793 
shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). A** B = mat 1)" 
794 
by (metis invertible_def matrix_left_right_inverse) 

795 

796 
lemma invertible_det_nz: 

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

797 
fixes A::"real ^'n^'n" 
33175  798 
shows "invertible A \<longleftrightarrow> det A \<noteq> 0" 
53253  799 
proof  
800 
{ 

801 
assume "invertible A" 

33175  802 
then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1" 
803 
unfolding invertible_righ_inverse by blast 

53854  804 
then have "det (A ** B) = det (mat 1 :: real ^'n^'n)" 
805 
by simp 

806 
then have "det A \<noteq> 0" 

807 
by (simp add: det_mul det_I) algebra 

53253  808 
} 
33175  809 
moreover 
53253  810 
{ 
811 
assume H: "\<not> invertible A" 

33175  812 
let ?U = "UNIV :: 'n set" 
53854  813 
have fU: "finite ?U" 
814 
by simp 

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

33175  818 
unfolding invertible_righ_inverse 
53854  819 
unfolding matrix_right_invertible_independent_rows 
820 
by blast 

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

823 
apply (simp only: ab_left_minus add.assoc[symmetric]) 
33175  824 
apply simp 
825 
done 

826 
from c ci 

64267  827 
have thr0: " row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U  {i})" 
828 
unfolding sum.remove[OF fU iU] sum_cmul 

33175  829 
apply  
830 
apply (rule vector_mul_lcancel_imp[OF ci]) 

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

831 
apply (auto simp add: field_simps) 
53854  832 
unfolding * 
833 
apply rule 

834 
done 

33175  835 
have thr: " row i A \<in> span {row j A j. j \<noteq> i}" 
836 
unfolding thr0 

64267  837 
apply (rule span_sum) 
33175  838 
apply simp 
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

839 
apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+ 
33175  840 
apply (rule span_superset) 
841 
apply auto 

842 
done 

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

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

845 
have "det A = 0" 

846 
unfolding det_row_span[OF thr, symmetric] right_minus 

53253  847 
unfolding det_zero_row[OF thrb] .. 
848 
} 

53854  849 
ultimately show ?thesis 
850 
by blast 

33175  851 
qed 
852 

60420  853 
text \<open>Cramer's rule.\<close> 
33175  854 

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

855 
lemma cramer_lemma_transpose: 
53854  856 
fixes A:: "real^'n^'n" 
857 
and x :: "real^'n" 

64267  858 
shows "det ((\<chi> i. if i = k then sum (\<lambda>i. x$i *s row i A) (UNIV::'n set) 
53854  859 
else row i A)::real^'n^'n) = x$k * det A" 
33175  860 
(is "?lhs = ?rhs") 
53253  861 
proof  
33175  862 
let ?U = "UNIV :: 'n set" 
863 
let ?Uk = "?U  {k}" 

53854  864 
have U: "?U = insert k ?Uk" 
865 
by blast 

866 
have fUk: "finite ?Uk" 

867 
by simp 

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

869 
by simp 

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

33175  874 
have "(\<chi> i. row i A) = A" by (vector row_def) 
53253  875 
then have thd1: "det (\<chi> i. row i A) = det A" 
876 
by simp 

33175  877 
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" 
878 
apply (rule det_row_span) 

64267  879 
apply (rule span_sum) 
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

880 
apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+ 
33175  881 
apply (rule span_superset) 
882 
apply auto 

883 
done 

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

885 
apply (subst U) 

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

888 
unfolding add.assoc 
33175  889 
apply (subst det_row_add) 
890 
unfolding thd0 

891 
unfolding det_row_mul 

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

53253  893 
unfolding thd1 
894 
apply (simp add: field_simps) 

895 
done 

33175  896 
qed 
897 

898 
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

899 
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

900 
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  901 
proof  
33175  902 
let ?U = "UNIV :: 'n set" 
64267  903 
have *: "\<And>c. sum (\<lambda>i. c i *s row i (transpose A)) ?U = sum (\<lambda>i. c i *s column i A) ?U" 
904 
by (auto simp add: row_transpose intro: sum.cong) 

53854  905 
show ?thesis 
906 
unfolding matrix_mult_vsum 

53253  907 
unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] 
908 
unfolding *[of "\<lambda>i. x$i"] 

909 
apply (subst det_transpose[symmetric]) 

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

911 
apply (vector transpose_def column_def row_def) 

912 
done 

33175  913 
qed 
914 

915 
lemma cramer: 

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

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

918 
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  919 
proof  
33175  920 
from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" 
53854  921 
unfolding invertible_det_nz[symmetric] invertible_def 
922 
by blast 

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

924 
by (simp add: B matrix_vector_mul_lid) 

925 
then have "A *v (B *v b) = b" 

926 
by (simp add: matrix_vector_mul_assoc) 

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

928 
by blast 

53253  929 
{ 
930 
fix x 

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

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

933 
unfolding x[symmetric] 

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

935 
} 

53854  936 
with xe show ?thesis 
937 
by auto 

33175  938 
qed 
939 

60420  940 
text \<open>Orthogonality of a transformation and matrix.\<close> 
33175  941 

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

943 

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

33175  946 
unfolding orthogonal_transformation_def 
947 
apply auto 

948 
apply (erule_tac x=v in allE)+ 

35542  949 
apply (simp add: norm_eq_sqrt_inner) 
53253  950 
apply (simp add: dot_norm linear_add[symmetric]) 
951 
done 

33175  952 

53253  953 
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> 
954 
transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1" 

33175  955 

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

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

959 
lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)" 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

960 
by (simp add: orthogonal_matrix_def transpose_mat matrix_mul_lid) 
33175  961 

962 
lemma orthogonal_matrix_mul: 

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

963 
fixes A :: "real ^'n^'n" 
33175  964 
assumes oA : "orthogonal_matrix A" 
53253  965 
and oB: "orthogonal_matrix B" 
33175  966 
shows "orthogonal_matrix(A ** B)" 
967 
using oA oB 

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

968 
unfolding orthogonal_matrix matrix_transpose_mul 
33175  969 
apply (subst matrix_mul_assoc) 
970 
apply (subst matrix_mul_assoc[symmetric]) 

53253  971 
apply (simp add: matrix_mul_rid) 
972 
done 

33175  973 

974 
lemma orthogonal_transformation_matrix: 

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

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

53253  978 
proof  
33175  979 
let ?mf = "matrix f" 
980 
let ?ot = "orthogonal_transformation f" 

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

982 
have fU: "finite ?U" by simp 

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

53253  984 
{ 
985 
assume ot: ?ot 

33175  986 
from ot have lf: "linear f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w" 
987 
unfolding orthogonal_transformation_def orthogonal_matrix by blast+ 

53253  988 
{ 
989 
fix i j 

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

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

993 
by simp_all 

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

33175  996 
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

997 
by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def 
64267  998 
th0 sum.delta[OF fU] mat_def axis_def) 
53253  999 
} 
53854  1000 
then have "orthogonal_matrix ?mf" 
1001 
unfolding orthogonal_matrix 

53253  1002 
by vector 
53854  1003 
with lf have ?rhs 
1004 
by blast 

53253  1005 
} 
33175  1006 
moreover 
53253  1007 
{ 
1008 
assume lf: "linear f" and om: "orthogonal_matrix ?mf" 

33175  1009 
from lf om have ?lhs 
63170  1010 
apply (simp only: orthogonal_matrix_def norm_eq orthogonal_transformation) 
1011 
apply (simp only: matrix_works[OF lf, symmetric]) 

33175  1012 
apply (subst dot_matrix_vector_mul) 
53253  1013 
apply (simp add: dot_matrix_product matrix_mul_lid) 
1014 
done 

1015 
} 

53854  1016 
ultimately show ?thesis 
1017 
by blast 

33175  1018 
qed 
1019 

1020 
lemma det_orthogonal_matrix: 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34291
diff
changeset

1021 
fixes Q:: "'a::linordered_idom^'n^'n" 
33175  1022 
assumes oQ: "orthogonal_matrix Q" 
1023 
shows "det Q = 1 \<or> det Q =  1" 

53253  1024 
proof  
33175  1025 
have th: "\<And>x::'a. x = 1 \<or> x =  1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x") 
53253  1026 
proof  
33175  1027 
fix x:: 'a 
53854  1028 
have th0: "x * x  1 = (x  1) * (x + 1)" 
53253  1029 
by (simp add: field_simps) 
33175  1030 
have th1: "\<And>(x::'a) y. x =  y \<longleftrightarrow> x + y = 0" 
53253  1031 
apply (subst eq_iff_diff_eq_0) 
1032 
apply simp 

1033 
done 

53854  1034 
have "x * x = 1 \<longleftrightarrow> x * x  1 = 0" 
1035 
by simp 

1036 
also have "\<dots> \<longleftrightarrow> x = 1 \<or> x =  1" 

1037 
unfolding th0 th1 by simp 

33175  1038 
finally show "?ths x" .. 
1039 
qed 

53253  1040 
from oQ have "Q ** transpose Q = mat 1" 
1041 
by (metis orthogonal_matrix_def) 

1042 
then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" 

1043 
by simp 

1044 
then have "det Q * det Q = 1" 

1045 
by (simp add: det_mul det_I det_transpose) 

33175  1046 
then show ?thesis unfolding th . 
1047 
qed 

1048 

60420  1049 
text \<open>Linearity of scaling, and hence isometry, that preserves origin.\<close> 
53854  1050 

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

1052 
fixes f :: "real ^'n \<Rightarrow> real ^'n" 
53253  1053 
assumes f0: "f 0 = 0" 
1054 
and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y" 

33175  1055 
shows "linear f" 
53253  1056 
proof  
1057 
{ 

1058 
fix v w 

1059 
{ 

1060 
fix x 

1061 
note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] 

1062 
} 

33175  1063 
note th0 = this 
53077  1064 
have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)" 
33175  1065 
unfolding dot_norm_neg dist_norm[symmetric] 
1066 
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} 

1067 
note fc = this 

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

1068 
show ?thesis 
53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53253
diff
changeset

1069 
unfolding linear_iff vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR 
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

1070 
by (simp add: inner_add fc field_simps) 
33175  1071 
qed 
1072 

1073 
lemma isometry_linear: 

53253  1074 
"f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f" 
1075 
by (rule scaling_linear[where c=1]) simp_all 

33175  1076 

60420  1077 
text \<open>Hence another formulation of orthogonal transformation.\<close> 
33175  1078 

1079 
lemma orthogonal_transformation_isometry: 

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

1080 
"orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)" 
33175  1081 
unfolding orthogonal_transformation 
1082 
apply (rule iffI) 

1083 
apply clarify 

63469
b6900858dcb9
lots of new theorems about differentiable_on, retracts, ANRs, etc.
paulson <lp15@cam.ac.uk>
parents:
63170
diff
changeset

1084 
apply (clarsimp simp add: linear_0 linear_diff[symmetric] dist_norm) 
33175  1085 
apply (rule conjI) 
1086 
apply (rule isometry_linear) 

1087 
apply simp 

1088 
apply simp 

1089 
apply clarify 

1090 
apply (erule_tac x=v in allE) 

1091 
apply (erule_tac x=0 in allE) 

53253  1092 
apply (simp add: dist_norm) 
1093 
done 

33175  1094 

60420  1095 
text \<open>Can extend an isometry from unit sphere.\<close> 
33175  1096 

1097 
lemma isometry_sphere_extend: 

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

1098 
fixes f:: "real ^'n \<Rightarrow> real ^'n" 
33175  1099 
assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1" 
53253  1100 
and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y" 
33175  1101 
shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)" 
53253  1102 
proof  
1103 
{ 

1104 
fix x y x' y' x0 y0 x0' y0' :: "real ^'n" 

1105 
assume H: 

1106 
"x = norm x *\<^sub>R x0" 

1107 
"y = norm y *\<^sub>R y0" 

1108 
"x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'" 

1109 
"norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1" 

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

53854  1111 
then have *: "x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0'  y0 \<bullet> x0 " 
53253  1112 
by (simp add: norm_eq norm_eq_1 inner_add inner_diff) 
33175  1113 
have "norm(x'  y') = norm(x  y)" 
1114 
apply (subst H(1)) 

1115 
apply (subst H(2)) 

1116 
apply (subst H(3)) 

1117 
apply (subst H(4)) 

1118 
using H(59) 

1119 
apply (simp add: norm_eq norm_eq_1) 

53854  1120 
apply (simp add: inner_diff scalar_mult_eq_scaleR) 
1121 
unfolding * 

53253  1122 
apply (simp add: field_simps) 
1123 
done 

1124 
} 

33175  1125 
note th0 = this 
44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

1126 
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" 
53253  1127 
{ 
1128 
fix x:: "real ^'n" 

1129 
assume nx: "norm x = 1" 

53854  1130 
have "?g x = f x" 
1131 
using nx by auto 

53253  1132 
} 
1133 
then have thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" 

1134 
by blast 

53854  1135 
have g0: "?g 0 = 0" 
1136 
by simp 

53253  1137 
{ 
1138 
fix x y :: "real ^'n" 

1139 
{ 

1140 
assume "x = 0" "y = 0" 

53854  1141 
then have "dist (?g x) (?g y) = dist x y" 
1142 
by simp 

53253  1143 
} 
33175  1144 
moreover 
53253  1145 
{ 
1146 
assume "x = 0" "y \<noteq> 0" 

33175  1147 
then have "dist (?g x) (?g y) = dist x y" 
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

1148 
apply (simp add: dist_norm) 
33175  1149 
apply (rule f1[rule_format]) 
53253  1150 
apply (simp add: field_simps) 
1151 
done 

1152 
} 

33175  1153 
moreover 
53253  1154 
{ 
1155 
assume "x \<noteq> 0" "y = 0" 

33175  1156 
then have "dist (?g x) (?g y) = dist x y" 
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

1157 
apply (simp add: dist_norm) 
33175  1158 
apply (rule f1[rule_format]) 
53253  1159 
apply (simp add: field_simps) 
1160 
done 

1161 
} 

33175  1162 
moreover 
53253  1163 
{ 
1164 
assume z: "x \<noteq> 0" "y \<noteq> 0" 

1165 
have th00: 

1166 
"x = norm x *\<^sub>R (inverse (norm x) *\<^sub>R x)" 

1167 
"y = norm y *\<^sub>R (inverse (norm y) *\<^sub>R y)" 

1168 
"norm x *\<^sub>R f ((inverse (norm x) *\<^sub>R x)) = norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" 

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

1169 
"norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y) = norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y)" 
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

1170 
"norm (inverse (norm x) *\<^sub>R x) = 1" 
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

1171 
"norm (f (inverse (norm x) *\<^sub>R x)) = 1" 
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

1172 
"norm (inverse (norm y) *\<^sub>R y) = 1" 
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

1173 
"norm (f (inverse (norm y) *\<^sub>R y)) = 1" 
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

1174 
"norm (f (inverse (norm x) *\<^sub>R x)  f (inverse (norm y) *\<^sub>R y)) = 
53253  1175 
norm (inverse (norm x) *\<^sub>R x  inverse (norm y) *\<^sub>R y)" 
33175  1176 
using z 
44457
d366fa5551ef
declare euclidean_simps [simp] at the point they are proved;
huffman
parents:
44260
diff
changeset

1177 
by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm]) 
33175  1178 
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" 
53253  1179 
by (simp add: dist_norm) 
1180 
} 

53854  1181 
ultimately have "dist (?g x) (?g y) = dist x y" 
1182 
by blast 

53253  1183 
} 
33175  1184 
note thd = this 
1185 
show ?thesis 

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

1187 
unfolding orthogonal_transformation_isometry 

53253  1188 
using g0 thfg thd 
1189 
apply metis 

1190 
done 

33175  1191 
qed 
1192 

60420  1193 
text \<open>Rotation, reflection, rotoinversion.\<close> 
33175  1194 

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

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

1197 

1198 
lemma orthogonal_rotation_or_rotoinversion: 

35028
108662d50512
more consistent naming of type classes involving orderings (and lattices)  c.f. NEWS
haftmann
parents:
34291
diff
changeset

1199 
fixes Q :: "'a::linordered_idom^'n^'n" 
33175  1200 
shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q" 
1201 
by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix) 

53253  1202 

60420  1203 
text \<open>Explicit formulas for low dimensions.\<close> 
33175  1204 

64272  1205 
lemma prod_neutral_const: "prod f {(1::nat)..1} = f 1" 
61286  1206 
by simp 
33175  1207 

64272  1208 
lemma prod_2: "prod f {(1::nat)..2} = f 1 * f 2" 
61286  1209 
by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute) 
53253  1210 

64272  1211 
lemma prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3" 
61286  1212 
by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute) 
33175  1213 

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

61286  1215 
by (simp add: det_def of_nat_Suc sign_id) 
33175  1216 

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

53253  1218 
proof  
33175 