author  huffman 
Wed, 17 Aug 2011 15:02:17 0700  
changeset 44260  7784fa3232ce 
parent 44228  5f974bead436 
child 44457  d366fa5551ef 
permissions  rwrr 
41959  1 
(* Title: HOL/Multivariate_Analysis/Determinants.thy 
2 
Author: Amine Chaieb, University of Cambridge 

33175  3 
*) 
4 

5 
header {* Traces, Determinant of square matrices and some properties *} 

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 

13 
subsection{* First some facts about products*} 

14 
lemma setprod_insert_eq: "finite A \<Longrightarrow> setprod f (insert a A) = (if a \<in> A then setprod f A else f a * setprod f A)" 

15 
apply clarsimp 

16 
by(subgoal_tac "insert a A = A", auto) 

17 

18 
lemma setprod_add_split: 

19 
assumes mn: "(m::nat) <= n + 1" 

20 
shows "setprod f {m.. n+p} = setprod f {m .. n} * setprod f {n+1..n+p}" 

21 
proof 

22 
let ?A = "{m .. n+p}" 

23 
let ?B = "{m .. n}" 

24 
let ?C = "{n+1..n+p}" 

25 
from mn have un: "?B \<union> ?C = ?A" by auto 

26 
from mn have dj: "?B \<inter> ?C = {}" by auto 

27 
have f: "finite ?B" "finite ?C" by simp_all 

28 
from setprod_Un_disjoint[OF f dj, of f, unfolded un] show ?thesis . 

29 
qed 

30 

31 

32 
lemma setprod_offset: "setprod f {(m::nat) + p .. n + p} = setprod (\<lambda>i. f (i + p)) {m..n}" 

33 
apply (rule setprod_reindex_cong[where f="op + p"]) 

34 
apply (auto simp add: image_iff Bex_def inj_on_def) 

35 
apply arith 

36 
apply (rule ext) 

37 
apply (simp add: add_commute) 

38 
done 

39 

40 
lemma setprod_singleton: "setprod f {x} = f x" by simp 

41 

42 
lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" by simp 

43 

44 
lemma setprod_numseg: "setprod f {m..0} = (if m=0 then f 0 else 1)" 

45 
"setprod f {m .. Suc n} = (if m \<le> Suc n then f (Suc n) * setprod f {m..n} 

46 
else setprod f {m..n})" 

47 
by (auto simp add: atLeastAtMostSuc_conv) 

48 

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

49 
lemma setprod_le: assumes fS: "finite S" and fg: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (g x :: 'a::linordered_idom)" 
33175  50 
shows "setprod f S \<le> setprod g S" 
51 
using fS fg 

52 
apply(induct S) 

53 
apply simp 

54 
apply auto 

55 
apply (rule mult_mono) 

56 
apply (auto intro: setprod_nonneg) 

57 
done 

58 

59 
(* FIXME: In Finite_Set there is a useless further assumption *) 

36409  60 
lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)" 
33175  61 
apply (erule finite_induct) 
62 
apply (simp) 

63 
apply simp 

64 
done 

65 

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

66 
lemma setprod_le_1: assumes fS: "finite S" and f: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (1::'a::linordered_idom)" 
33175  67 
shows "setprod f S \<le> 1" 
68 
using setprod_le[OF fS f] unfolding setprod_1 . 

69 

70 
subsection{* Trace *} 

71 

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

72 
definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" where 
33175  73 
"trace A = setsum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)" 
74 

75 
lemma trace_0: "trace(mat 0) = 0" 

76 
by (simp add: trace_def mat_def) 

77 

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

78 
lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))" 
33175  79 
by (simp add: trace_def mat_def) 
80 

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

81 
lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B" 
33175  82 
by (simp add: trace_def setsum_addf) 
83 

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

84 
lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n)  B) = trace A  trace B" 
33175  85 
by (simp add: trace_def setsum_subtractf) 
86 

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

87 
lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)" 
33175  88 
apply (simp add: trace_def matrix_matrix_mult_def) 
89 
apply (subst setsum_commute) 

90 
by (simp add: mult_commute) 

91 

92 
(*  *) 

93 
(* Definition of determinant. *) 

94 
(*  *) 

95 

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

96 
definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where 
33175  97 
"det A = setsum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)) {p. p permutes (UNIV :: 'n set)}" 
98 

99 
(*  *) 

100 
(* A few general lemmas we need below. *) 

101 
(*  *) 

102 

103 
lemma setprod_permute: 

104 
assumes p: "p permutes S" 

105 
shows "setprod f S = setprod (f o p) S" 

106 
proof 

107 
{assume "\<not> finite S" hence ?thesis by simp} 

108 
moreover 

109 
{assume fS: "finite S" 

110 
then have ?thesis 

111 
apply (simp add: setprod_def cong del:strong_setprod_cong) 

112 
apply (rule ab_semigroup_mult.fold_image_permute) 

113 
apply (auto simp add: p) 

114 
apply unfold_locales 

115 
done} 

116 
ultimately show ?thesis by blast 

117 
qed 

118 

119 
lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}" 

120 
by (blast intro!: setprod_permute) 

121 

122 
(*  *) 

123 
(* Basic determinant properties. *) 

124 
(*  *) 

125 

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

126 
lemma det_transpose: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)" 
33175  127 
proof 
128 
let ?di = "\<lambda>A i j. A$i$j" 

129 
let ?U = "(UNIV :: 'n set)" 

130 
have fU: "finite ?U" by simp 

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

132 
from p have pU: "p permutes ?U" by blast 

133 
have sth: "sign (inv p) = sign p" 

44260
7784fa3232ce
Determinants.thy: avoid using mem_def/Collect_def
huffman
parents:
44228
diff
changeset

134 
by (metis sign_inverse fU p mem_Collect_eq permutation_permutes) 
33175  135 
from permutes_inj[OF pU] 
136 
have pi: "inj_on p ?U" by (blast intro: subset_inj_on) 

137 
from permutes_image[OF pU] 

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

138 
have "setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)" by simp 
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

139 
also have "\<dots> = setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U" 
33175  140 
unfolding setprod_reindex[OF pi] .. 
141 
also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U" 

142 
proof 

143 
{fix i assume i: "i \<in> ?U" 

144 
from i permutes_inv_o[OF pU] permutes_in_image[OF pU] 

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

145 
have "((\<lambda>i. ?di (transpose A) i (inv p i)) o p) i = ?di A i (p i)" 
39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

146 
unfolding transpose_def by (simp add: fun_eq_iff)} 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

147 
then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong) 
33175  148 
qed 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

149 
finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth 
33175  150 
by simp} 
151 
then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse) 

152 
apply (rule setsum_cong2) by blast 

153 
qed 

154 

155 
lemma det_lowerdiagonal: 

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

156 
fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})" 
33175  157 
assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0" 
158 
shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)" 

159 
proof 

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

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

162 
let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" 

163 
have fU: "finite ?U" by simp 

164 
from finite_permutations[OF fU] have fPU: "finite ?PU" . 

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

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

167 
from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+ 

168 
from permutes_natset_le[OF pU] pid obtain i where 

169 
i: "p i > i" by (metis not_le) 

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

171 
from setprod_zero[OF fU ex] have "?pp p = 0" by simp} 

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

173 
from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis 

174 
unfolding det_def by (simp add: sign_id) 

175 
qed 

176 

177 
lemma det_upperdiagonal: 

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

178 
fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}" 
33175  179 
assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0" 
180 
shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)" 

181 
proof 

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

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

184 
let ?pp = "(\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))" 

185 
have fU: "finite ?U" by simp 

186 
from finite_permutations[OF fU] have fPU: "finite ?PU" . 

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

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

189 
from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+ 

190 
from permutes_natset_ge[OF pU] pid obtain i where 

191 
i: "p i < i" by (metis not_le) 

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

193 
from setprod_zero[OF fU ex] have "?pp p = 0" by simp} 

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

195 
from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis 

196 
unfolding det_def by (simp add: sign_id) 

197 
qed 

198 

199 
lemma det_diagonal: 

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

200 
fixes A :: "'a::comm_ring_1^'n^'n" 
33175  201 
assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0" 
202 
shows "det A = setprod (\<lambda>i. A$i$i) (UNIV::'n set)" 

203 
proof 

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

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

206 
let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)" 

207 
have fU: "finite ?U" by simp 

208 
from finite_permutations[OF fU] have fPU: "finite ?PU" . 

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

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

211 
then have "p \<noteq> id" by simp 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39198
diff
changeset

212 
then obtain i where i: "p i \<noteq> i" unfolding fun_eq_iff by auto 
33175  213 
from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast 
214 
from setprod_zero [OF fU ex] have "?pp p = 0" by simp} 

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

216 
from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis 

217 
unfolding det_def by (simp add: sign_id) 

218 
qed 

219 

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

220 
lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1" 
33175  221 
proof 
222 
let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n" 

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

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

225 
{fix i assume i: "i \<in> ?U" 

226 
have "?f i i = 1" using i by (vector mat_def)} 

227 
hence th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U" 

228 
by (auto intro: setprod_cong) 

229 
{fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j" 

230 
have "?f i j = 0" using i j ij by (vector mat_def) } 

231 
then have "det ?A = setprod (\<lambda>i. ?f i i) ?U" using det_diagonal 

232 
by blast 

233 
also have "\<dots> = 1" unfolding th setprod_1 .. 

234 
finally show ?thesis . 

235 
qed 

236 

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

237 
lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0" 
33175  238 
by (simp add: det_def setprod_zero) 
239 

240 
lemma det_permute_rows: 

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

241 
fixes A :: "'a::comm_ring_1^'n^'n" 
33175  242 
assumes p: "p permutes (UNIV :: 'n::finite set)" 
243 
shows "det(\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A" 

244 
apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric]) 

245 
apply (subst sum_permutations_compose_right[OF p]) 

246 
proof(rule setsum_cong2) 

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

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

249 
fix q assume qPU: "q \<in> ?PU" 

250 
have fU: "finite ?U" by simp 

251 
from qPU have q: "q permutes ?U" by blast 

252 
from p q have pp: "permutation p" and qp: "permutation q" 

253 
by (metis fU permutation_permutes)+ 

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

255 
have "setprod (\<lambda>i. A$p i$ (q o p) i) ?U = setprod ((\<lambda>i. A$p i$(q o p) i) o inv p) ?U" 

256 
by (simp only: setprod_permute[OF ip, symmetric]) 

257 
also have "\<dots> = setprod (\<lambda>i. A $ (p o inv p) i $ (q o (p o inv p)) i) ?U" 

258 
by (simp only: o_def) 

259 
also have "\<dots> = setprod (\<lambda>i. A$i$q i) ?U" by (simp only: o_def permutes_inverses[OF p]) 

260 
finally have thp: "setprod (\<lambda>i. A$p i$ (q o p) i) ?U = setprod (\<lambda>i. A$i$q i) ?U" 

261 
by blast 

262 
show "of_int (sign (q o p)) * setprod (\<lambda>i. A$ p i$ (q o p) i) ?U = of_int (sign p) * of_int (sign q) * setprod (\<lambda>i. A$i$q i) ?U" 

263 
by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult) 

264 
qed 

265 

266 
lemma det_permute_columns: 

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

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

270 
proof 

271 
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

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

273 
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

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

276 
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

277 
by (simp add: transpose_def vec_eq_iff) 
33175  278 
ultimately show ?thesis by simp 
279 
qed 

280 

281 
lemma det_identical_rows: 

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

282 
fixes A :: "'a::linordered_idom^'n^'n" 
33175  283 
assumes ij: "i \<noteq> j" 
284 
and r: "row i A = row j A" 

285 
shows "det A = 0" 

286 
proof 

287 
have tha: "\<And>(a::'a) b. a = b ==> b =  a ==> a = 0" 

288 
by simp 

289 
have th1: "of_int (1) =  1" by (metis of_int_1 of_int_minus number_of_Min) 

290 
let ?p = "Fun.swap i j id" 

291 
let ?A = "\<chi> i. A $ ?p i" 

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

292 
from r have "A = ?A" by (simp add: vec_eq_iff row_def swap_def) 
33175  293 
hence "det A = det ?A" by simp 
294 
moreover have "det A =  det ?A" 

295 
by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1) 

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

297 
qed 

298 

299 
lemma det_identical_columns: 

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

300 
fixes A :: "'a::linordered_idom^'n^'n" 
33175  301 
assumes ij: "i \<noteq> j" 
302 
and r: "column i A = column j A" 

303 
shows "det A = 0" 

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

304 
apply (subst det_transpose[symmetric]) 
33175  305 
apply (rule det_identical_rows[OF ij]) 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

306 
by (metis row_transpose r) 
33175  307 

308 
lemma det_zero_row: 

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

309 
fixes A :: "'a::{idom, ring_char_0}^'n^'n" 
33175  310 
assumes r: "row i A = 0" 
311 
shows "det A = 0" 

312 
using r 

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

313 
apply (simp add: row_def det_def vec_eq_iff) 
33175  314 
apply (rule setsum_0') 
315 
apply (auto simp: sign_nz) 

316 
done 

317 

318 
lemma det_zero_column: 

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

319 
fixes A :: "'a::{idom,ring_char_0}^'n^'n" 
33175  320 
assumes r: "column i A = 0" 
321 
shows "det A = 0" 

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

322 
apply (subst det_transpose[symmetric]) 
33175  323 
apply (rule det_zero_row [of i]) 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

324 
by (metis row_transpose r) 
33175  325 

326 
lemma det_row_add: 

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

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

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

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

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

331 
unfolding det_def vec_lambda_beta setsum_addf[symmetric] 
33175  332 
proof (rule setsum_cong2) 
333 
let ?U = "UNIV :: 'n set" 

334 
let ?pU = "{p. p permutes ?U}" 

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

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

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

338 
fix p assume p: "p \<in> ?pU" 

339 
let ?Uk = "?U  {k}" 

340 
from p have pU: "p permutes ?U" by blast 

341 
have kU: "?U = insert k ?Uk" by blast 

342 
{fix j assume j: "j \<in> ?Uk" 

343 
from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j" 

344 
by simp_all} 

345 
then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk" 

346 
and th2: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?h i $ p i) ?Uk" 

347 
apply  

348 
apply (rule setprod_cong, simp_all)+ 

349 
done 

350 
have th3: "finite ?Uk" "k \<notin> ?Uk" by auto 

351 
have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" 

352 
unfolding kU[symmetric] .. 

353 
also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" 

354 
apply (rule setprod_insert) 

355 
apply simp 

356 
by blast 

36350  357 
also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk)" by (simp add: field_simps) 
33175  358 
also have "\<dots> = (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk) + (b k$ p k * setprod (\<lambda>i. ?h i $ p i) ?Uk)" by (metis th1 th2) 
359 
also have "\<dots> = setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i $ p i) (insert k ?Uk)" 

360 
unfolding setprod_insert[OF th3] by simp 

361 
finally have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?g i $ p i) ?U + setprod (\<lambda>i. ?h i $ p i) ?U" unfolding kU[symmetric] . 

362 
then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i $ p i) ?U" 

36350  363 
by (simp add: field_simps) 
33175  364 
qed 
365 

366 
lemma det_row_mul: 

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

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

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

370 

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

371 
unfolding det_def vec_lambda_beta setsum_right_distrib 
33175  372 
proof (rule setsum_cong2) 
373 
let ?U = "UNIV :: 'n set" 

374 
let ?pU = "{p. p permutes ?U}" 

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

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

377 
fix p assume p: "p \<in> ?pU" 

378 
let ?Uk = "?U  {k}" 

379 
from p have pU: "p permutes ?U" by blast 

380 
have kU: "?U = insert k ?Uk" by blast 

381 
{fix j assume j: "j \<in> ?Uk" 

382 
from j have "?f j $ p j = ?g j $ p j" by simp} 

383 
then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk" 

384 
apply  

385 
apply (rule setprod_cong, simp_all) 

386 
done 

387 
have th3: "finite ?Uk" "k \<notin> ?Uk" by auto 

388 
have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)" 

389 
unfolding kU[symmetric] .. 

390 
also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" 

391 
apply (rule setprod_insert) 

392 
apply simp 

393 
by blast 

36350  394 
also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" by (simp add: field_simps) 
33175  395 
also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)" 
396 
unfolding th1 by (simp add: mult_ac) 

397 
also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))" 

398 
unfolding setprod_insert[OF th3] by simp 

399 
finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)" unfolding kU[symmetric] . 

400 
then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U = c * (of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U)" 

36350  401 
by (simp add: field_simps) 
33175  402 
qed 
403 

404 
lemma det_row_0: 

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

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

407 
using det_row_mul[of k 0 "\<lambda>i. 1" b] 

408 
apply (simp) 

409 
unfolding vector_smult_lzero . 

410 

411 
lemma det_row_operation: 

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

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

415 
proof 

416 
let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n" 

417 
have th: "row i ?Z = row j ?Z" by (vector row_def) 

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

419 
by (vector row_def) 

420 
show ?thesis 

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

422 
by simp 

423 
qed 

424 

425 
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

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

429 
proof 

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

431 
let ?S = "{row j A j. j \<noteq> i}" 

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

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

434 
{fix k 

435 

436 
have "(if k = i then row i A + 0 else row k A) = row k A" by simp} 

437 
then have P0: "?P 0" 

438 
apply  

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

440 
by (vector row_def) 

441 
moreover 

442 
{fix c z y assume zS: "z \<in> ?S" and Py: "?P y" 

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

444 
let ?w = "row i A + y" 

445 
have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector 

446 
have thz: "?d z = 0" 

447 
apply (rule det_identical_rows[OF j(2)]) 

448 
using j by (vector row_def) 

449 
have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 .. 

450 
then have "?P (c*s z + y)" unfolding thz Py det_row_mul[of i] det_row_add[of i] 

451 
by simp } 

452 

453 
ultimately show ?thesis 

454 
apply  

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

455 
apply (rule span_induct_alt[of ?P ?S, OF P0, folded smult_conv_scaleR]) 
33175  456 
apply blast 
457 
apply (rule x) 

458 
done 

459 
qed 

460 

461 
(*  *) 

462 
(* May as well do this, though it's a bit unsatisfactory since it ignores *) 

463 
(* exact duplicates by considering the rows/columns as a set. *) 

464 
(*  *) 

465 

466 
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

467 
fixes A:: "real^'n^'n" 
33175  468 
assumes d: "dependent (rows A)" 
469 
shows "det A = 0" 

470 
proof 

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

472 
from d obtain i where i: "row i A \<in> span (rows A  {row i A})" 

473 
unfolding dependent_def rows_def by blast 

474 
{fix j k assume jk: "j \<noteq> k" 

475 
and c: "row j A = row k A" 

476 
from det_identical_rows[OF jk c] have ?thesis .} 

477 
moreover 

478 
{assume H: "\<And> i j. i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A" 

479 
have th0: " row i A \<in> span {row j Aj. j \<noteq> i}" 

480 
apply (rule span_neg) 

481 
apply (rule set_rev_mp) 

482 
apply (rule i) 

483 
apply (rule span_mono) 

484 
using H i by (auto simp add: rows_def) 

485 
from det_row_span[OF th0] 

486 
have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)" 

487 
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

488 
with det_row_mul[of i "0::real" "\<lambda>i. 1"] 
33175  489 
have "det A = 0" by simp} 
490 
ultimately show ?thesis by blast 

491 
qed 

492 

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

493 
lemma det_dependent_columns: assumes d: "dependent(columns (A::real^'n^'n))" shows "det A = 0" 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

494 
by (metis d det_dependent_rows rows_transpose det_transpose) 
33175  495 

496 
(*  *) 

497 
(* Multilinearity and the multiplication formula. *) 

498 
(*  *) 

499 

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

500 
lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)" 
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

501 
apply (rule iffD1[OF vec_lambda_unique]) by vector 
33175  502 

503 
lemma det_linear_row_setsum: 

504 
assumes fS: "finite S" 

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

505 
shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) = setsum (\<lambda>j. det ((\<chi> i. if i = k then a i j else c i)::'a^'n^'n)) S" 
33175  506 
proof(induct rule: finite_induct[OF fS]) 
507 
case 1 thus ?case apply simp unfolding setsum_empty det_row_0[of k] .. 

508 
next 

509 
case (2 x F) 

510 
then show ?case by (simp add: det_row_add cong del: if_weak_cong) 

511 
qed 

512 

513 
lemma finite_bounded_functions: 

514 
assumes fS: "finite S" 

515 
shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}" 

516 
proof(induct k) 

517 
case 0 

518 
have th: "{f. \<forall>i. f i = i} = {id}" by (auto intro: ext) 

519 
show ?case by (auto simp add: th) 

520 
next 

521 
case (Suc k) 

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

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

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

525 
apply (auto simp add: image_iff) 

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

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

528 
apply (auto intro: ext) 

529 
done 

530 
with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f] 

531 
show ?case by metis 

532 
qed 

533 

534 

535 
lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by (auto intro: ext) 

536 

537 
lemma det_linear_rows_setsum_lemma: 

538 
assumes fS: "finite S" and fT: "finite T" 

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

539 
shows "det((\<chi> i. if i \<in> T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) = 
33175  540 
setsum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n)) 
541 
{f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}" 

542 
using fT 

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

544 
case empty 

545 
have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)" by vector 

546 
from "empty.prems" show ?case unfolding th0 by simp 

547 
next 

548 
case (insert z T a c) 

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

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

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

552 
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)" 

553 
let ?c = "\<lambda>i. if i = z then a i j else c i" 

554 
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)" by simp 

555 
have thif2: "\<And>a b c d e. (if a then b else if c then d else e) = 

556 
(if c then (if a then b else d) else (if a then b else e))" by simp 

557 
from `z \<notin> T` have nz: "\<And>i. i \<in> T \<Longrightarrow> i = z \<longleftrightarrow> False" by auto 

558 
have "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) = 

559 
det (\<chi> i. if i = z then setsum (a i) S 

560 
else if i \<in> T then setsum (a i) S else c i)" 

561 
unfolding insert_iff thif .. 

562 
also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<in> T then setsum (a i) S 

563 
else if i = z then a i j else c i))" 

564 
unfolding det_linear_row_setsum[OF fS] 

565 
apply (subst thif2) 

566 
using nz by (simp cong del: if_weak_cong cong add: if_cong) 

567 
finally have tha: 

568 
"det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) = 

569 
(\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i) 

570 
else if i = z then a i j 

571 
else c i))" 

572 
unfolding insert.hyps unfolding setsum_cartesian_product by blast 

573 
show ?case unfolding tha 

574 
apply(rule setsum_eq_general_reverses[where h= "?h" and k= "?k"], 

575 
blast intro: finite_cartesian_product fS finite, 

576 
blast intro: finite_cartesian_product fS finite) 

577 
using `z \<notin> T` 

578 
apply (auto intro: ext) 

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

580 
by vector 

581 
qed 

582 

583 
lemma det_linear_rows_setsum: 

584 
assumes fS: "finite (S::'n::finite set)" 

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

585 
shows "det (\<chi> i. setsum (a i) S) = setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}" 
33175  586 
proof 
587 
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)" by vector 

588 

589 
from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] show ?thesis by simp 

590 
qed 

591 

592 
lemma matrix_mul_setsum_alt: 

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

593 
fixes A B :: "'a::comm_ring_1^'n^'n" 
33175  594 
shows "A ** B = (\<chi> i. setsum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))" 
595 
by (vector matrix_matrix_mult_def setsum_component) 

596 

597 
lemma det_rows_mul: 

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

598 
"det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) = 
33175  599 
setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)" 
600 
proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2) 

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

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

603 
fix p assume pU: "p \<in> ?PU" 

604 
let ?s = "of_int (sign p)" 

605 
from pU have p: "p permutes ?U" by blast 

606 
have "setprod (\<lambda>i. c i * a i $ p i) ?U = setprod c ?U * setprod (\<lambda>i. a i $ p i) ?U" 

607 
unfolding setprod_timesf .. 

608 
then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) = 

36350  609 
setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" by (simp add: field_simps) 
33175  610 
qed 
611 

612 
lemma det_mul: 

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

613 
fixes A B :: "'a::linordered_idom^'n^'n" 
33175  614 
shows "det (A ** B) = det A * det B" 
615 
proof 

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

617 
let ?F = "{f. (\<forall>i\<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}" 

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

619 
have fU: "finite ?U" by simp 

620 
have fF: "finite ?F" by (rule finite) 

621 
{fix p assume p: "p permutes ?U" 

622 

623 
have "p \<in> ?F" unfolding mem_Collect_eq permutes_in_image[OF p] 

624 
using p[unfolded permutes_def] by simp} 

625 
then have PUF: "?PU \<subseteq> ?F" by blast 

626 
{fix f assume fPU: "f \<in> ?F  ?PU" 

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

628 
from fPU have f: "\<forall>i \<in> ?U. f i \<in> ?U" 

629 
"\<forall>i. i \<notin> ?U \<longrightarrow> f i = i" "\<not>(\<forall>y. \<exists>!x. f x = y)" unfolding permutes_def 

630 
by auto 

631 

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

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

634 
{assume fni: "\<not> inj_on f ?U" 

635 
then obtain i j where ij: "f i = f j" "i \<noteq> j" 

636 
unfolding inj_on_def by blast 

637 
from ij 

638 
have rth: "row i ?B = row j ?B" by (vector row_def) 

639 
from det_identical_rows[OF ij(2) rth] 

640 
have "det (\<chi> i. A$i$f i *s B$f i) = 0" 

641 
unfolding det_rows_mul by simp} 

642 
moreover 

643 
{assume fi: "inj_on f ?U" 

644 
from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j" 

645 
unfolding inj_on_def by metis 

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

647 

648 
{fix y 

649 
from fs f have "\<exists>x. f x = y" by blast 

650 
then obtain x where x: "f x = y" by blast 

651 
{fix z assume z: "f z = y" from fith x z have "z = x" by metis} 

652 
with x have "\<exists>!x. f x = y" by blast} 

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

654 
ultimately have "det (\<chi> i. A$i$f i *s B$f i) = 0" by blast} 

655 
hence zth: "\<forall> f\<in> ?F  ?PU. det (\<chi> i. A$i$f i *s B$f i) = 0" by simp 

656 
{fix p assume pU: "p \<in> ?PU" 

657 
from pU have p: "p permutes ?U" by blast 

658 
let ?s = "\<lambda>p. of_int (sign p)" 

659 
let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * 

660 
(?s q * (\<Prod>i\<in> ?U. B $ i $ q i))" 

661 
have "(setsum (\<lambda>q. ?s q * 

662 
(\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) = 

663 
(setsum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * 

664 
(?s q * (\<Prod>i\<in> ?U. B $ i $ q i))) ?PU)" 

665 
unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f] 

666 
proof(rule setsum_cong2) 

667 
fix q assume qU: "q \<in> ?PU" 

668 
hence q: "q permutes ?U" by blast 

669 
from p q have pp: "permutation p" and pq: "permutation q" 

670 
unfolding permutation_permutes by auto 

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

672 
"\<And>a. of_int (sign p) * (of_int (sign p) * a) = a" 

673 
unfolding mult_assoc[symmetric] unfolding of_int_mult[symmetric] 

674 
by (simp_all add: sign_idempotent) 

675 
have ths: "?s q = ?s p * ?s (q o inv p)" 

676 
using pp pq permutation_inverse[OF pp] sign_inverse[OF pp] 

677 
by (simp add: th00 mult_ac sign_idempotent sign_compose) 

678 
have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) o p) ?U" 

679 
by (rule setprod_permute[OF p]) 

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

681 
unfolding th001 setprod_timesf[symmetric] o_def permutes_inverses[OF p] 

682 
apply (rule setprod_cong[OF refl]) 

683 
using permutes_in_image[OF q] by vector 

684 
show "?s q * setprod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U = ?s p * (setprod (\<lambda>i. A$i$p i) ?U) * (?s (q o inv p) * setprod (\<lambda>i. B$i$(q o inv p) i) ?U)" 

685 
using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp] 

36350  686 
by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose) 
33175  687 
qed 
688 
} 

689 
then have th2: "setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B" 

690 
unfolding det_def setsum_product 

691 
by (rule setsum_cong2) 

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

693 
unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] by simp 

694 
also have "\<dots> = setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU" 

695 
using setsum_mono_zero_cong_left[OF fF PUF zth, symmetric] 

696 
unfolding det_rows_mul by auto 

697 
finally show ?thesis unfolding th2 . 

698 
qed 

699 

700 
(*  *) 

701 
(* Relation to invertibility. *) 

702 
(*  *) 

703 

704 
lemma invertible_left_inverse: 

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

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

708 

709 
lemma invertible_righ_inverse: 

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

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

713 

714 
lemma invertible_det_nz: 

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

715 
fixes A::"real ^'n^'n" 
33175  716 
shows "invertible A \<longleftrightarrow> det A \<noteq> 0" 
717 
proof 

718 
{assume "invertible A" 

719 
then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1" 

720 
unfolding invertible_righ_inverse by blast 

721 
hence "det (A ** B) = det (mat 1 :: real ^'n^'n)" by simp 

722 
hence "det A \<noteq> 0" 

723 
apply (simp add: det_mul det_I) by algebra } 

724 
moreover 

725 
{assume H: "\<not> invertible A" 

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

727 
have fU: "finite ?U" by simp 

728 
from H obtain c i where c: "setsum (\<lambda>i. c i *s row i A) ?U = 0" 

729 
and iU: "i \<in> ?U" and ci: "c i \<noteq> 0" 

730 
unfolding invertible_righ_inverse 

731 
unfolding matrix_right_invertible_independent_rows by blast 

732 
have stupid: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> a = b" 

733 
apply (drule_tac f="op + ( a)" in cong[OF refl]) 

734 
apply (simp only: ab_left_minus add_assoc[symmetric]) 

735 
apply simp 

736 
done 

737 
from c ci 

738 
have thr0: " row i A = setsum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U  {i})" 

739 
unfolding setsum_diff1'[OF fU iU] setsum_cmul 

740 
apply  

741 
apply (rule vector_mul_lcancel_imp[OF ci]) 

742 
apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps) 

743 
unfolding stupid .. 

744 
have thr: " row i A \<in> span {row j A j. j \<noteq> i}" 

745 
unfolding thr0 

746 
apply (rule span_setsum) 

747 
apply simp 

748 
apply (rule ballI) 

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

749 
apply (rule span_mul [where 'a="real^'n", folded smult_conv_scaleR])+ 
33175  750 
apply (rule span_superset) 
751 
apply auto 

752 
done 

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

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

755 
have "det A = 0" 

756 
unfolding det_row_span[OF thr, symmetric] right_minus 

757 
unfolding det_zero_row[OF thrb] ..} 

758 
ultimately show ?thesis by blast 

759 
qed 

760 

761 
(*  *) 

762 
(* Cramer's rule. *) 

763 
(*  *) 

764 

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

765 
lemma cramer_lemma_transpose: 
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

766 
fixes A:: "real^'n^'n" and x :: "real^'n" 
33175  767 
shows "det ((\<chi> i. if i = k then setsum (\<lambda>i. x$i *s row i A) (UNIV::'n set) 
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

768 
else row i A)::real^'n^'n) = x$k * det A" 
33175  769 
(is "?lhs = ?rhs") 
770 
proof 

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

772 
let ?Uk = "?U  {k}" 

773 
have U: "?U = insert k ?Uk" by blast 

774 
have fUk: "finite ?Uk" by simp 

775 
have kUk: "k \<notin> ?Uk" by simp 

776 
have th00: "\<And>k s. x$k *s row k A + s = (x$k  1) *s row k A + row k A + s" 

36350  777 
by (vector field_simps) 
33175  778 
have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by (auto intro: ext) 
779 
have "(\<chi> i. row i A) = A" by (vector row_def) 

780 
then have thd1: "det (\<chi> i. row i A) = det A" by simp 

781 
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" 

782 
apply (rule det_row_span) 

783 
apply (rule span_setsum[OF fUk]) 

784 
apply (rule ballI) 

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

785 
apply (rule span_mul [where 'a="real^'n", folded smult_conv_scaleR])+ 
33175  786 
apply (rule span_superset) 
787 
apply auto 

788 
done 

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

790 
apply (subst U) 

791 
unfolding setsum_insert[OF fUk kUk] 

792 
apply (subst th00) 

793 
unfolding add_assoc 

794 
apply (subst det_row_add) 

795 
unfolding thd0 

796 
unfolding det_row_mul 

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

36350  798 
unfolding thd1 by (simp add: field_simps) 
33175  799 
qed 
800 

801 
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

802 
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

803 
shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: real^'n^'n) = x$k * det A" 
33175  804 
proof 
805 
let ?U = "UNIV :: 'n set" 

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

806 
have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transpose A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U" 
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

807 
by (auto simp add: row_transpose intro: setsum_cong2) 
33175  808 
show ?thesis unfolding matrix_mult_vsum 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

809 
unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric] 
33175  810 
unfolding stupid[of "\<lambda>i. x$i"] 
35150
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

811 
apply (subst det_transpose[symmetric]) 
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

812 
apply (rule cong[OF refl[of det]]) by (vector transpose_def column_def row_def) 
33175  813 
qed 
814 

815 
lemma cramer: 

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

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

818 
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)" 
33175  819 
proof 
820 
from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1" 

821 
unfolding invertible_det_nz[symmetric] invertible_def by blast 

822 
have "(A ** B) *v b = b" by (simp add: B matrix_vector_mul_lid) 

823 
hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc) 

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

825 
{fix x assume x: "A *v x = b" 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

826 
have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)" 
33175  827 
unfolding x[symmetric] 
44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

828 
using d0 by (simp add: vec_eq_iff cramer_lemma field_simps)} 
33175  829 
with xe show ?thesis by auto 
830 
qed 

831 

832 
(*  *) 

833 
(* Orthogonality of a transformation and matrix. *) 

834 
(*  *) 

835 

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

837 

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

839 
unfolding orthogonal_transformation_def 

840 
apply auto 

841 
apply (erule_tac x=v in allE)+ 

35542  842 
apply (simp add: norm_eq_sqrt_inner) 
33175  843 
by (simp add: dot_norm linear_add[symmetric]) 
844 

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

845 
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1" 
33175  846 

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

847 
lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1" 
33175  848 
by (metis matrix_left_right_inverse orthogonal_matrix_def) 
849 

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

850 
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

851 
by (simp add: orthogonal_matrix_def transpose_mat matrix_mul_lid) 
33175  852 

853 
lemma orthogonal_matrix_mul: 

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

854 
fixes A :: "real ^'n^'n" 
33175  855 
assumes oA : "orthogonal_matrix A" 
856 
and oB: "orthogonal_matrix B" 

857 
shows "orthogonal_matrix(A ** B)" 

858 
using oA oB 

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

859 
unfolding orthogonal_matrix matrix_transpose_mul 
33175  860 
apply (subst matrix_mul_assoc) 
861 
apply (subst matrix_mul_assoc[symmetric]) 

862 
by (simp add: matrix_mul_rid) 

863 

864 
lemma orthogonal_transformation_matrix: 

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

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

868 
proof 

869 
let ?mf = "matrix f" 

870 
let ?ot = "orthogonal_transformation f" 

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

872 
have fU: "finite ?U" by simp 

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

874 
{assume ot: ?ot 

875 
from ot have lf: "linear f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w" 

876 
unfolding orthogonal_transformation_def orthogonal_matrix by blast+ 

877 
{fix i j 

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

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

881 
by simp_all 

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

882 
from fd[rule_format, of "cart_basis i" "cart_basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul] 
33175  883 
have "?A$i$j = ?m1 $ i $ j" 
44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

884 
by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def cart_basis_def th0 setsum_delta[OF fU] mat_def)} 
33175  885 
hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector 
886 
with lf have ?rhs by blast} 

887 
moreover 

888 
{assume lf: "linear f" and om: "orthogonal_matrix ?mf" 

889 
from lf om have ?lhs 

890 
unfolding orthogonal_matrix_def norm_eq orthogonal_transformation 

891 
unfolding matrix_works[OF lf, symmetric] 

892 
apply (subst dot_matrix_vector_mul) 

893 
by (simp add: dot_matrix_product matrix_mul_lid)} 

894 
ultimately show ?thesis by blast 

895 
qed 

896 

897 
lemma det_orthogonal_matrix: 

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

898 
fixes Q:: "'a::linordered_idom^'n^'n" 
33175  899 
assumes oQ: "orthogonal_matrix Q" 
900 
shows "det Q = 1 \<or> det Q =  1" 

901 
proof 

902 

903 
have th: "\<And>x::'a. x = 1 \<or> x =  1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x") 

904 
proof 

905 
fix x:: 'a 

36350  906 
have th0: "x*x  1 = (x  1)*(x + 1)" by (simp add: field_simps) 
33175  907 
have th1: "\<And>(x::'a) y. x =  y \<longleftrightarrow> x + y = 0" 
908 
apply (subst eq_iff_diff_eq_0) by simp 

909 
have "x*x = 1 \<longleftrightarrow> x*x  1 = 0" by simp 

910 
also have "\<dots> \<longleftrightarrow> x = 1 \<or> x =  1" unfolding th0 th1 by simp 

911 
finally show "?ths x" .. 

912 
qed 

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

913 
from oQ have "Q ** transpose Q = mat 1" by (metis orthogonal_matrix_def) 
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

914 
hence "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)" by simp 
082fa4bd403d
Rename transp to transpose in HOLMultivariate_Analysis. (by himmelma)
hoelzl
parents:
35028
diff
changeset

915 
hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transpose) 
33175  916 
then show ?thesis unfolding th . 
917 
qed 

918 

919 
(*  *) 

920 
(* Linearity of scaling, and hence isometry, that preserves origin. *) 

921 
(*  *) 

922 
lemma scaling_linear: 

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

923 
fixes f :: "real ^'n \<Rightarrow> real ^'n" 
33175  924 
assumes f0: "f 0 = 0" and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y" 
925 
shows "linear f" 

926 
proof 

927 
{fix v w 

928 
{fix x note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right] } 

929 
note th0 = this 

930 
have "f v \<bullet> f w = c^2 * (v \<bullet> w)" 

931 
unfolding dot_norm_neg dist_norm[symmetric] 

932 
unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)} 

933 
note fc = this 

36585  934 
show ?thesis unfolding linear_def vector_eq[where 'a="real^'n"] smult_conv_scaleR by (simp add: inner_simps fc field_simps) 
33175  935 
qed 
936 

937 
lemma isometry_linear: 

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

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

941 

942 
(*  *) 

943 
(* Hence another formulation of orthogonal transformation. *) 

944 
(*  *) 

945 

946 
lemma orthogonal_transformation_isometry: 

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

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

950 
apply clarify 

951 
apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_norm) 

952 
apply (rule conjI) 

953 
apply (rule isometry_linear) 

954 
apply simp 

955 
apply simp 

956 
apply clarify 

957 
apply (erule_tac x=v in allE) 

958 
apply (erule_tac x=0 in allE) 

959 
by (simp add: dist_norm) 

960 

961 
(*  *) 

962 
(* Can extend an isometry from unit sphere. *) 

963 
(*  *) 

964 

965 
lemma isometry_sphere_extend: 

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

966 
fixes f:: "real ^'n \<Rightarrow> real ^'n" 
33175  967 
assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1" 
968 
and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y" 

969 
shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)" 

970 
proof 

971 
{fix x y x' y' x0 y0 x0' y0' :: "real ^'n" 

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

972 
assume H: "x = norm x *\<^sub>R x0" "y = norm y *\<^sub>R y0" 
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

973 
"x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'" 
33175  974 
"norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1" 
975 
"norm(x0'  y0') = norm(x0  y0)" 

35542  976 
hence *:"x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0'  y0 \<bullet> x0 " by(simp add: norm_eq norm_eq_1 inner_simps) 
33175  977 
have "norm(x'  y') = norm(x  y)" 
978 
apply (subst H(1)) 

979 
apply (subst H(2)) 

980 
apply (subst H(3)) 

981 
apply (subst H(4)) 

982 
using H(59) 

983 
apply (simp add: norm_eq norm_eq_1) 

35542  984 
apply (simp add: inner_simps smult_conv_scaleR) unfolding * 
36350  985 
by (simp add: field_simps) } 
33175  986 
note th0 = this 
44228
5f974bead436
get Multivariate_Analysis/Determinants.thy compiled and working again
huffman
parents:
41959
diff
changeset

987 
let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)" 
33175  988 
{fix x:: "real ^'n" assume nx: "norm x = 1" 
989 
have "?g x = f x" using nx by auto} 

990 
hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast 

991 
have g0: "?g 0 = 0" by simp 

992 
{fix x y :: "real ^'n" 

993 
{assume "x = 0" "y = 0" 

994 
then have "dist (?g x) (?g y) = dist x y" by simp } 

995 
moreover 

996 
{assume "x = 0" "y \<noteq> 0" 

997 
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

998 
apply (simp add: dist_norm) 
33175  999 
apply (rule f1[rule_format]) 
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

1000 
by(simp add: field_simps)} 
33175  1001 
moreover 
1002 
{assume "x \<noteq> 0" "y = 0" 

1003 
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

1004 
apply (simp add: dist_norm) 
33175  1005 
apply (rule f1[rule_format]) 
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

1006 
by(simp add: field_simps)} 
33175  1007 
moreover 
1008 
{assume z: "x \<noteq> 0" "y \<noteq> 0" 

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

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

1010 
"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

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

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

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

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

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

1016 
norm (inverse (norm x) *\<^sub>R x  inverse (norm y) *\<^sub>R y)" 
33175  1017 
using z 
36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

1018 
by (auto simp add: vector_smult_assoc field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm]) 
33175  1019 
from z th0[OF th00] have "dist (?g x) (?g y) = dist x y" 
1020 
by (simp add: dist_norm)} 

1021 
ultimately have "dist (?g x) (?g y) = dist x y" by blast} 

1022 
note thd = this 

1023 
show ?thesis 

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

1025 
unfolding orthogonal_transformation_isometry 

1026 
using g0 thfg thd by metis 

1027 
qed 

1028 

1029 
(*  *) 

1030 
(* Rotation, reflection, rotoinversion. *) 

1031 
(*  *) 

1032 

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

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

1035 

1036 
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

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

1040 
(*  *) 

1041 
(* Explicit formulas for low dimensions. *) 

1042 
(*  *) 

1043 

1044 
lemma setprod_1: "setprod f {(1::nat)..1} = f 1" by simp 

1045 

1046 
lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2" 

40077  1047 
by (simp add: eval_nat_numeral setprod_numseg mult_commute) 
33175  1048 
lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3" 
40077  1049 
by (simp add: eval_nat_numeral setprod_numseg mult_commute) 
33175  1050 

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

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

1052 
by (simp add: det_def sign_id UNIV_1) 
33175  1053 

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

1055 
proof 

1056 
have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto 

1057 
show ?thesis 

1058 
unfolding det_def UNIV_2 

1059 
unfolding setsum_over_permutations_insert[OF f12] 

1060 
unfolding permutes_sing 

1061 
apply (simp add: sign_swap_id sign_id swap_id_eq) 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

1062 
by (simp add: arith_simps(31)[symmetric] del: arith_simps(31)) 
33175  1063 
qed 
1064 

1065 
lemma det_3: "det (A::'a::comm_ring_1^3^3) = 

1066 
A$1$1 * A$2$2 * A$3$3 + 

1067 
A$1$2 * A$2$3 * A$3$1 + 

1068 
A$1$3 * A$2$1 * A$3$2  

1069 
A$1$1 * A$2$3 * A$3$2  

1070 
A$1$2 * A$2$1 * A$3$3  

1071 
A$1$3 * A$2$2 * A$3$1" 

1072 
proof 

1073 
have f123: "finite {2::3, 3}" "1 \<notin> {2::3, 3}" by auto 

1074 
have f23: "finite {3::3}" "2 \<notin> {3::3}" by auto 

1075 

1076 
show ?thesis 

1077 
unfolding det_def UNIV_3 

1078 
unfolding setsum_over_permutations_insert[OF f123] 

1079 
unfolding setsum_over_permutations_insert[OF f23] 

1080 

1081 
unfolding permutes_sing 

1082 
apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq) 

36362
06475a1547cb
fix lots of looping simp calls and other warnings
huffman
parents:
35542
diff
changeset

1083 
apply (simp add: arith_simps(31)[symmetric] del: arith_simps(31)) 
36350  1084 
by (simp add: field_simps) 
33175  1085 
qed 
1086 

1087 
end 