src/HOL/Multivariate_Analysis/Determinants.thy
author wenzelm
Sun Nov 02 17:09:04 2014 +0100 (2014-11-02)
changeset 58877 262572d90bc6
parent 57514 bdc2c6b40bf2
child 59867 58043346ca64
permissions -rw-r--r--
modernized header;
wenzelm@41959
     1
(*  Title:      HOL/Multivariate_Analysis/Determinants.thy
wenzelm@41959
     2
    Author:     Amine Chaieb, University of Cambridge
himmelma@33175
     3
*)
himmelma@33175
     4
wenzelm@58877
     5
section {* Traces, Determinant of square matrices and some properties *}
himmelma@33175
     6
himmelma@33175
     7
theory Determinants
huffman@44228
     8
imports
huffman@44228
     9
  Cartesian_Euclidean_Space
huffman@44228
    10
  "~~/src/HOL/Library/Permutations"
himmelma@33175
    11
begin
himmelma@33175
    12
himmelma@33175
    13
subsection{* First some facts about products*}
wenzelm@53253
    14
himmelma@33175
    15
lemma setprod_add_split:
wenzelm@53854
    16
  fixes m n :: nat
wenzelm@53854
    17
  assumes mn: "m \<le> n + 1"
wenzelm@53854
    18
  shows "setprod f {m..n+p} = setprod f {m .. n} * setprod f {n+1..n+p}"
wenzelm@53253
    19
proof -
wenzelm@53854
    20
  let ?A = "{m..n+p}"
wenzelm@53854
    21
  let ?B = "{m..n}"
himmelma@33175
    22
  let ?C = "{n+1..n+p}"
wenzelm@53854
    23
  from mn have un: "?B \<union> ?C = ?A"
wenzelm@53854
    24
    by auto
wenzelm@53854
    25
  from mn have dj: "?B \<inter> ?C = {}"
wenzelm@53854
    26
    by auto
wenzelm@53854
    27
  have f: "finite ?B" "finite ?C"
wenzelm@53854
    28
    by simp_all
haftmann@57418
    29
  from setprod.union_disjoint[OF f dj, of f, unfolded un] show ?thesis .
himmelma@33175
    30
qed
himmelma@33175
    31
himmelma@33175
    32
wenzelm@53854
    33
lemma setprod_offset:
wenzelm@53854
    34
  fixes m n :: nat
wenzelm@53854
    35
  shows "setprod f {m + p .. n + p} = setprod (\<lambda>i. f (i + p)) {m..n}"
hoelzl@57129
    36
  by (rule setprod.reindex_bij_witness[where i="op + p" and j="\<lambda>i. i - p"]) auto
himmelma@33175
    37
wenzelm@53253
    38
lemma setprod_singleton: "setprod f {x} = f x"
wenzelm@53253
    39
  by simp
himmelma@33175
    40
wenzelm@53854
    41
lemma setprod_singleton_nat_seg:
wenzelm@53854
    42
  fixes n :: "'a::order"
wenzelm@53854
    43
  shows "setprod f {n..n} = f n"
wenzelm@53253
    44
  by simp
wenzelm@53253
    45
wenzelm@53253
    46
lemma setprod_numseg:
wenzelm@53253
    47
  "setprod f {m..0} = (if m = 0 then f 0 else 1)"
wenzelm@53253
    48
  "setprod f {m .. Suc n} =
wenzelm@53253
    49
    (if m \<le> Suc n then f (Suc n) * setprod f {m..n} else setprod f {m..n})"
himmelma@33175
    50
  by (auto simp add: atLeastAtMostSuc_conv)
himmelma@33175
    51
wenzelm@53253
    52
lemma setprod_le:
wenzelm@53854
    53
  fixes f g :: "'b \<Rightarrow> 'a::linordered_idom"
wenzelm@53253
    54
  assumes fS: "finite S"
wenzelm@53854
    55
    and fg: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> g x"
himmelma@33175
    56
  shows "setprod f S \<le> setprod g S"
wenzelm@53253
    57
  using fS fg
wenzelm@53253
    58
  apply (induct S)
wenzelm@53253
    59
  apply simp
wenzelm@53253
    60
  apply auto
wenzelm@53253
    61
  apply (rule mult_mono)
wenzelm@53253
    62
  apply (auto intro: setprod_nonneg)
wenzelm@53253
    63
  done
himmelma@33175
    64
wenzelm@53854
    65
(* FIXME: In Finite_Set there is a useless further assumption *)
wenzelm@53253
    66
lemma setprod_inversef:
wenzelm@53253
    67
  "finite A \<Longrightarrow> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)"
himmelma@33175
    68
  apply (erule finite_induct)
himmelma@33175
    69
  apply (simp)
himmelma@33175
    70
  apply simp
himmelma@33175
    71
  done
himmelma@33175
    72
wenzelm@53253
    73
lemma setprod_le_1:
wenzelm@53854
    74
  fixes f :: "'b \<Rightarrow> 'a::linordered_idom"
wenzelm@53253
    75
  assumes fS: "finite S"
wenzelm@53854
    76
    and f: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> 1"
himmelma@33175
    77
  shows "setprod f S \<le> 1"
haftmann@57418
    78
  using setprod_le[OF fS f] unfolding setprod.neutral_const .
himmelma@33175
    79
wenzelm@53253
    80
wenzelm@53253
    81
subsection {* Trace *}
himmelma@33175
    82
wenzelm@53253
    83
definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a"
wenzelm@53253
    84
  where "trace A = setsum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
himmelma@33175
    85
wenzelm@53854
    86
lemma trace_0: "trace (mat 0) = 0"
himmelma@33175
    87
  by (simp add: trace_def mat_def)
himmelma@33175
    88
wenzelm@53854
    89
lemma trace_I: "trace (mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
himmelma@33175
    90
  by (simp add: trace_def mat_def)
himmelma@33175
    91
hoelzl@34291
    92
lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
haftmann@57418
    93
  by (simp add: trace_def setsum.distrib)
himmelma@33175
    94
hoelzl@34291
    95
lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
himmelma@33175
    96
  by (simp add: trace_def setsum_subtractf)
himmelma@33175
    97
wenzelm@53854
    98
lemma trace_mul_sym: "trace ((A::'a::comm_semiring_1^'n^'m) ** B) = trace (B**A)"
himmelma@33175
    99
  apply (simp add: trace_def matrix_matrix_mult_def)
haftmann@57418
   100
  apply (subst setsum.commute)
haftmann@57512
   101
  apply (simp add: mult.commute)
wenzelm@53253
   102
  done
himmelma@33175
   103
wenzelm@53854
   104
text {* Definition of determinant. *}
himmelma@33175
   105
hoelzl@34291
   106
definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
wenzelm@53253
   107
  "det A =
wenzelm@53253
   108
    setsum (\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))
wenzelm@53253
   109
      {p. p permutes (UNIV :: 'n set)}"
himmelma@33175
   110
wenzelm@53854
   111
text {* A few general lemmas we need below. *}
himmelma@33175
   112
himmelma@33175
   113
lemma setprod_permute:
himmelma@33175
   114
  assumes p: "p permutes S"
wenzelm@53854
   115
  shows "setprod f S = setprod (f \<circ> p) S"
haftmann@51489
   116
  using assms by (fact setprod.permute)
himmelma@33175
   117
wenzelm@53253
   118
lemma setproduct_permute_nat_interval:
wenzelm@53854
   119
  fixes m n :: nat
wenzelm@53854
   120
  shows "p permutes {m..n} \<Longrightarrow> setprod f {m..n} = setprod (f \<circ> p) {m..n}"
himmelma@33175
   121
  by (blast intro!: setprod_permute)
himmelma@33175
   122
wenzelm@53854
   123
text {* Basic determinant properties. *}
himmelma@33175
   124
hoelzl@35150
   125
lemma det_transpose: "det (transpose A) = det (A::'a::comm_ring_1 ^'n^'n)"
wenzelm@53253
   126
proof -
himmelma@33175
   127
  let ?di = "\<lambda>A i j. A$i$j"
himmelma@33175
   128
  let ?U = "(UNIV :: 'n set)"
himmelma@33175
   129
  have fU: "finite ?U" by simp
wenzelm@53253
   130
  {
wenzelm@53253
   131
    fix p
wenzelm@53253
   132
    assume p: "p \<in> {p. p permutes ?U}"
wenzelm@53854
   133
    from p have pU: "p permutes ?U"
wenzelm@53854
   134
      by blast
himmelma@33175
   135
    have sth: "sign (inv p) = sign p"
huffman@44260
   136
      by (metis sign_inverse fU p mem_Collect_eq permutation_permutes)
himmelma@33175
   137
    from permutes_inj[OF pU]
wenzelm@53854
   138
    have pi: "inj_on p ?U"
wenzelm@53854
   139
      by (blast intro: subset_inj_on)
himmelma@33175
   140
    from permutes_image[OF pU]
wenzelm@53253
   141
    have "setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U =
wenzelm@53854
   142
      setprod (\<lambda>i. ?di (transpose A) i (inv p i)) (p ` ?U)"
wenzelm@53854
   143
      by simp
wenzelm@53854
   144
    also have "\<dots> = setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U"
haftmann@57418
   145
      unfolding setprod.reindex[OF pi] ..
himmelma@33175
   146
    also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U"
wenzelm@53253
   147
    proof -
wenzelm@53253
   148
      {
wenzelm@53253
   149
        fix i
wenzelm@53253
   150
        assume i: "i \<in> ?U"
himmelma@33175
   151
        from i permutes_inv_o[OF pU] permutes_in_image[OF pU]
wenzelm@53854
   152
        have "((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) i = ?di A i (p i)"
wenzelm@53253
   153
          unfolding transpose_def by (simp add: fun_eq_iff)
wenzelm@53253
   154
      }
wenzelm@53854
   155
      then show "setprod ((\<lambda>i. ?di (transpose A) i (inv p i)) \<circ> p) ?U =
wenzelm@53854
   156
        setprod (\<lambda>i. ?di A i (p i)) ?U"
haftmann@57418
   157
        by (auto intro: setprod.cong)
himmelma@33175
   158
    qed
wenzelm@53253
   159
    finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transpose A) i (inv p i)) ?U) =
wenzelm@53854
   160
      of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)"
wenzelm@53854
   161
      using sth by simp
wenzelm@53253
   162
  }
wenzelm@53253
   163
  then show ?thesis
wenzelm@53253
   164
    unfolding det_def
wenzelm@53253
   165
    apply (subst setsum_permutations_inverse)
haftmann@57418
   166
    apply (rule setsum.cong)
haftmann@57418
   167
    apply (rule refl)
wenzelm@53253
   168
    apply blast
wenzelm@53253
   169
    done
himmelma@33175
   170
qed
himmelma@33175
   171
himmelma@33175
   172
lemma det_lowerdiagonal:
hoelzl@34291
   173
  fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})"
himmelma@33175
   174
  assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"
himmelma@33175
   175
  shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
wenzelm@53253
   176
proof -
himmelma@33175
   177
  let ?U = "UNIV:: 'n set"
himmelma@33175
   178
  let ?PU = "{p. p permutes ?U}"
himmelma@33175
   179
  let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
wenzelm@53854
   180
  have fU: "finite ?U"
wenzelm@53854
   181
    by simp
himmelma@33175
   182
  from finite_permutations[OF fU] have fPU: "finite ?PU" .
wenzelm@53854
   183
  have id0: "{id} \<subseteq> ?PU"
wenzelm@53854
   184
    by (auto simp add: permutes_id)
wenzelm@53253
   185
  {
wenzelm@53253
   186
    fix p
wenzelm@53854
   187
    assume p: "p \<in> ?PU - {id}"
wenzelm@53253
   188
    from p have pU: "p permutes ?U" and pid: "p \<noteq> id"
wenzelm@53253
   189
      by blast+
wenzelm@53253
   190
    from permutes_natset_le[OF pU] pid obtain i where i: "p i > i"
wenzelm@53253
   191
      by (metis not_le)
wenzelm@53253
   192
    from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0"
wenzelm@53253
   193
      by blast
wenzelm@53253
   194
    from setprod_zero[OF fU ex] have "?pp p = 0"
wenzelm@53253
   195
      by simp
wenzelm@53253
   196
  }
wenzelm@53854
   197
  then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
wenzelm@53253
   198
    by blast
haftmann@57418
   199
  from setsum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis
himmelma@33175
   200
    unfolding det_def by (simp add: sign_id)
himmelma@33175
   201
qed
himmelma@33175
   202
himmelma@33175
   203
lemma det_upperdiagonal:
hoelzl@34291
   204
  fixes A :: "'a::comm_ring_1^'n::{finite,wellorder}^'n::{finite,wellorder}"
himmelma@33175
   205
  assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0"
himmelma@33175
   206
  shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
wenzelm@53253
   207
proof -
himmelma@33175
   208
  let ?U = "UNIV:: 'n set"
himmelma@33175
   209
  let ?PU = "{p. p permutes ?U}"
himmelma@33175
   210
  let ?pp = "(\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
wenzelm@53854
   211
  have fU: "finite ?U"
wenzelm@53854
   212
    by simp
himmelma@33175
   213
  from finite_permutations[OF fU] have fPU: "finite ?PU" .
wenzelm@53854
   214
  have id0: "{id} \<subseteq> ?PU"
wenzelm@53854
   215
    by (auto simp add: permutes_id)
wenzelm@53253
   216
  {
wenzelm@53253
   217
    fix p
wenzelm@53854
   218
    assume p: "p \<in> ?PU - {id}"
wenzelm@53253
   219
    from p have pU: "p permutes ?U" and pid: "p \<noteq> id"
wenzelm@53253
   220
      by blast+
wenzelm@53253
   221
    from permutes_natset_ge[OF pU] pid obtain i where i: "p i < i"
wenzelm@53253
   222
      by (metis not_le)
wenzelm@53854
   223
    from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0"
wenzelm@53854
   224
      by blast
wenzelm@53854
   225
    from setprod_zero[OF fU ex] have "?pp p = 0"
wenzelm@53854
   226
      by simp
wenzelm@53253
   227
  }
wenzelm@53253
   228
  then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"
wenzelm@53253
   229
    by blast
haftmann@57418
   230
  from setsum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis
himmelma@33175
   231
    unfolding det_def by (simp add: sign_id)
himmelma@33175
   232
qed
himmelma@33175
   233
himmelma@33175
   234
lemma det_diagonal:
hoelzl@34291
   235
  fixes A :: "'a::comm_ring_1^'n^'n"
himmelma@33175
   236
  assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0"
himmelma@33175
   237
  shows "det A = setprod (\<lambda>i. A$i$i) (UNIV::'n set)"
wenzelm@53253
   238
proof -
himmelma@33175
   239
  let ?U = "UNIV:: 'n set"
himmelma@33175
   240
  let ?PU = "{p. p permutes ?U}"
himmelma@33175
   241
  let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
himmelma@33175
   242
  have fU: "finite ?U" by simp
himmelma@33175
   243
  from finite_permutations[OF fU] have fPU: "finite ?PU" .
wenzelm@53854
   244
  have id0: "{id} \<subseteq> ?PU"
wenzelm@53854
   245
    by (auto simp add: permutes_id)
wenzelm@53253
   246
  {
wenzelm@53253
   247
    fix p
wenzelm@53253
   248
    assume p: "p \<in> ?PU - {id}"
wenzelm@53854
   249
    then have "p \<noteq> id"
wenzelm@53854
   250
      by simp
wenzelm@53854
   251
    then obtain i where i: "p i \<noteq> i"
wenzelm@53854
   252
      unfolding fun_eq_iff by auto
wenzelm@53854
   253
    from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0"
wenzelm@53854
   254
      by blast
wenzelm@53854
   255
    from setprod_zero [OF fU ex] have "?pp p = 0"
wenzelm@53854
   256
      by simp
wenzelm@53854
   257
  }
wenzelm@53854
   258
  then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
wenzelm@53854
   259
    by blast
haftmann@57418
   260
  from setsum.mono_neutral_cong_left[OF fPU id0 p0] show ?thesis
himmelma@33175
   261
    unfolding det_def by (simp add: sign_id)
himmelma@33175
   262
qed
himmelma@33175
   263
hoelzl@34291
   264
lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n) = 1"
wenzelm@53253
   265
proof -
himmelma@33175
   266
  let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n"
himmelma@33175
   267
  let ?U = "UNIV :: 'n set"
himmelma@33175
   268
  let ?f = "\<lambda>i j. ?A$i$j"
wenzelm@53253
   269
  {
wenzelm@53253
   270
    fix i
wenzelm@53253
   271
    assume i: "i \<in> ?U"
wenzelm@53854
   272
    have "?f i i = 1"
wenzelm@53854
   273
      using i by (vector mat_def)
wenzelm@53253
   274
  }
wenzelm@53253
   275
  then have th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U"
haftmann@57418
   276
    by (auto intro: setprod.cong)
wenzelm@53253
   277
  {
wenzelm@53253
   278
    fix i j
wenzelm@53253
   279
    assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"
wenzelm@53854
   280
    have "?f i j = 0" using i j ij
wenzelm@53854
   281
      by (vector mat_def)
wenzelm@53253
   282
  }
wenzelm@53854
   283
  then have "det ?A = setprod (\<lambda>i. ?f i i) ?U"
wenzelm@53854
   284
    using det_diagonal by blast
wenzelm@53854
   285
  also have "\<dots> = 1"
haftmann@57418
   286
    unfolding th setprod.neutral_const ..
himmelma@33175
   287
  finally show ?thesis .
himmelma@33175
   288
qed
himmelma@33175
   289
hoelzl@34291
   290
lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n) = 0"
himmelma@33175
   291
  by (simp add: det_def setprod_zero)
himmelma@33175
   292
himmelma@33175
   293
lemma det_permute_rows:
hoelzl@34291
   294
  fixes A :: "'a::comm_ring_1^'n^'n"
himmelma@33175
   295
  assumes p: "p permutes (UNIV :: 'n::finite set)"
wenzelm@53854
   296
  shows "det (\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A"
haftmann@57512
   297
  apply (simp add: det_def setsum_right_distrib mult.assoc[symmetric])
himmelma@33175
   298
  apply (subst sum_permutations_compose_right[OF p])
haftmann@57418
   299
proof (rule setsum.cong)
himmelma@33175
   300
  let ?U = "UNIV :: 'n set"
himmelma@33175
   301
  let ?PU = "{p. p permutes ?U}"
wenzelm@53253
   302
  fix q
wenzelm@53253
   303
  assume qPU: "q \<in> ?PU"
wenzelm@53854
   304
  have fU: "finite ?U"
wenzelm@53854
   305
    by simp
wenzelm@53253
   306
  from qPU have q: "q permutes ?U"
wenzelm@53253
   307
    by blast
himmelma@33175
   308
  from p q have pp: "permutation p" and qp: "permutation q"
himmelma@33175
   309
    by (metis fU permutation_permutes)+
himmelma@33175
   310
  from permutes_inv[OF p] have ip: "inv p permutes ?U" .
wenzelm@53854
   311
  have "setprod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = setprod ((\<lambda>i. A$p i$(q \<circ> p) i) \<circ> inv p) ?U"
wenzelm@53253
   312
    by (simp only: setprod_permute[OF ip, symmetric])
wenzelm@53854
   313
  also have "\<dots> = setprod (\<lambda>i. A $ (p \<circ> inv p) i $ (q \<circ> (p \<circ> inv p)) i) ?U"
wenzelm@53253
   314
    by (simp only: o_def)
wenzelm@53253
   315
  also have "\<dots> = setprod (\<lambda>i. A$i$q i) ?U"
wenzelm@53253
   316
    by (simp only: o_def permutes_inverses[OF p])
wenzelm@53854
   317
  finally have thp: "setprod (\<lambda>i. A$p i$ (q \<circ> p) i) ?U = setprod (\<lambda>i. A$i$q i) ?U"
wenzelm@53253
   318
    by blast
wenzelm@53854
   319
  show "of_int (sign (q \<circ> p)) * setprod (\<lambda>i. A$ p i$ (q \<circ> p) i) ?U =
wenzelm@53253
   320
    of_int (sign p) * of_int (sign q) * setprod (\<lambda>i. A$i$q i) ?U"
haftmann@57512
   321
    by (simp only: thp sign_compose[OF qp pp] mult.commute of_int_mult)
haftmann@57418
   322
qed rule
himmelma@33175
   323
himmelma@33175
   324
lemma det_permute_columns:
hoelzl@34291
   325
  fixes A :: "'a::comm_ring_1^'n^'n"
himmelma@33175
   326
  assumes p: "p permutes (UNIV :: 'n set)"
himmelma@33175
   327
  shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A"
wenzelm@53253
   328
proof -
himmelma@33175
   329
  let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n"
hoelzl@35150
   330
  let ?At = "transpose A"
hoelzl@35150
   331
  have "of_int (sign p) * det A = det (transpose (\<chi> i. transpose A $ p i))"
hoelzl@35150
   332
    unfolding det_permute_rows[OF p, of ?At] det_transpose ..
himmelma@33175
   333
  moreover
hoelzl@35150
   334
  have "?Ap = transpose (\<chi> i. transpose A $ p i)"
huffman@44228
   335
    by (simp add: transpose_def vec_eq_iff)
wenzelm@53854
   336
  ultimately show ?thesis
wenzelm@53854
   337
    by simp
himmelma@33175
   338
qed
himmelma@33175
   339
himmelma@33175
   340
lemma det_identical_rows:
haftmann@35028
   341
  fixes A :: "'a::linordered_idom^'n^'n"
himmelma@33175
   342
  assumes ij: "i \<noteq> j"
wenzelm@53253
   343
    and r: "row i A = row j A"
himmelma@33175
   344
  shows "det A = 0"
himmelma@33175
   345
proof-
wenzelm@53253
   346
  have tha: "\<And>(a::'a) b. a = b \<Longrightarrow> b = - a \<Longrightarrow> a = 0"
himmelma@33175
   347
    by simp
huffman@47108
   348
  have th1: "of_int (-1) = - 1" by simp
himmelma@33175
   349
  let ?p = "Fun.swap i j id"
himmelma@33175
   350
  let ?A = "\<chi> i. A $ ?p i"
haftmann@56545
   351
  from r have "A = ?A" by (simp add: vec_eq_iff row_def Fun.swap_def)
wenzelm@53253
   352
  then have "det A = det ?A" by simp
himmelma@33175
   353
  moreover have "det A = - det ?A"
himmelma@33175
   354
    by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1)
himmelma@33175
   355
  ultimately show "det A = 0" by (metis tha)
himmelma@33175
   356
qed
himmelma@33175
   357
himmelma@33175
   358
lemma det_identical_columns:
haftmann@35028
   359
  fixes A :: "'a::linordered_idom^'n^'n"
himmelma@33175
   360
  assumes ij: "i \<noteq> j"
wenzelm@53253
   361
    and r: "column i A = column j A"
himmelma@33175
   362
  shows "det A = 0"
wenzelm@53253
   363
  apply (subst det_transpose[symmetric])
wenzelm@53253
   364
  apply (rule det_identical_rows[OF ij])
wenzelm@53253
   365
  apply (metis row_transpose r)
wenzelm@53253
   366
  done
himmelma@33175
   367
himmelma@33175
   368
lemma det_zero_row:
hoelzl@34291
   369
  fixes A :: "'a::{idom, ring_char_0}^'n^'n"
himmelma@33175
   370
  assumes r: "row i A = 0"
himmelma@33175
   371
  shows "det A = 0"
wenzelm@53253
   372
  using r
wenzelm@53253
   373
  apply (simp add: row_def det_def vec_eq_iff)
haftmann@57418
   374
  apply (rule setsum.neutral)
wenzelm@53253
   375
  apply (auto simp: sign_nz)
wenzelm@53253
   376
  done
himmelma@33175
   377
himmelma@33175
   378
lemma det_zero_column:
hoelzl@34291
   379
  fixes A :: "'a::{idom,ring_char_0}^'n^'n"
himmelma@33175
   380
  assumes r: "column i A = 0"
himmelma@33175
   381
  shows "det A = 0"
hoelzl@35150
   382
  apply (subst det_transpose[symmetric])
himmelma@33175
   383
  apply (rule det_zero_row [of i])
wenzelm@53253
   384
  apply (metis row_transpose r)
wenzelm@53253
   385
  done
himmelma@33175
   386
himmelma@33175
   387
lemma det_row_add:
himmelma@33175
   388
  fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n"
himmelma@33175
   389
  shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) =
wenzelm@53253
   390
    det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +
wenzelm@53253
   391
    det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)"
haftmann@57418
   392
  unfolding det_def vec_lambda_beta setsum.distrib[symmetric]
haftmann@57418
   393
proof (rule setsum.cong)
himmelma@33175
   394
  let ?U = "UNIV :: 'n set"
himmelma@33175
   395
  let ?pU = "{p. p permutes ?U}"
himmelma@33175
   396
  let ?f = "(\<lambda>i. if i = k then a i + b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
himmelma@33175
   397
  let ?g = "(\<lambda> i. if i = k then a i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
himmelma@33175
   398
  let ?h = "(\<lambda> i. if i = k then b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
wenzelm@53253
   399
  fix p
wenzelm@53253
   400
  assume p: "p \<in> ?pU"
himmelma@33175
   401
  let ?Uk = "?U - {k}"
wenzelm@53854
   402
  from p have pU: "p permutes ?U"
wenzelm@53854
   403
    by blast
wenzelm@53854
   404
  have kU: "?U = insert k ?Uk"
wenzelm@53854
   405
    by blast
wenzelm@53253
   406
  {
wenzelm@53253
   407
    fix j
wenzelm@53253
   408
    assume j: "j \<in> ?Uk"
himmelma@33175
   409
    from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j"
wenzelm@53253
   410
      by simp_all
wenzelm@53253
   411
  }
himmelma@33175
   412
  then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"
himmelma@33175
   413
    and th2: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?h i $ p i) ?Uk"
himmelma@33175
   414
    apply -
haftmann@57418
   415
    apply (rule setprod.cong, simp_all)+
himmelma@33175
   416
    done
wenzelm@53854
   417
  have th3: "finite ?Uk" "k \<notin> ?Uk"
wenzelm@53854
   418
    by auto
himmelma@33175
   419
  have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
himmelma@33175
   420
    unfolding kU[symmetric] ..
wenzelm@53854
   421
  also have "\<dots> = ?f k $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
haftmann@57418
   422
    apply (rule setprod.insert)
himmelma@33175
   423
    apply simp
wenzelm@53253
   424
    apply blast
wenzelm@53253
   425
    done
wenzelm@53253
   426
  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)"
wenzelm@53253
   427
    by (simp add: field_simps)
wenzelm@53253
   428
  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)"
wenzelm@53253
   429
    by (metis th1 th2)
himmelma@33175
   430
  also have "\<dots> = setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i $ p i) (insert k ?Uk)"
haftmann@57418
   431
    unfolding  setprod.insert[OF th3] by simp
wenzelm@53854
   432
  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"
wenzelm@53854
   433
    unfolding kU[symmetric] .
wenzelm@53253
   434
  then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U =
wenzelm@53253
   435
    of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U + of_int (sign p) * setprod (\<lambda>i. ?h i $ p i) ?U"
haftmann@36350
   436
    by (simp add: field_simps)
haftmann@57418
   437
qed rule
himmelma@33175
   438
himmelma@33175
   439
lemma det_row_mul:
himmelma@33175
   440
  fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n"
himmelma@33175
   441
  shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) =
wenzelm@53253
   442
    c * det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)"
wenzelm@53253
   443
  unfolding det_def vec_lambda_beta setsum_right_distrib
haftmann@57418
   444
proof (rule setsum.cong)
himmelma@33175
   445
  let ?U = "UNIV :: 'n set"
himmelma@33175
   446
  let ?pU = "{p. p permutes ?U}"
himmelma@33175
   447
  let ?f = "(\<lambda>i. if i = k then c*s a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
himmelma@33175
   448
  let ?g = "(\<lambda> i. if i = k then a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
wenzelm@53253
   449
  fix p
wenzelm@53253
   450
  assume p: "p \<in> ?pU"
himmelma@33175
   451
  let ?Uk = "?U - {k}"
wenzelm@53854
   452
  from p have pU: "p permutes ?U"
wenzelm@53854
   453
    by blast
wenzelm@53854
   454
  have kU: "?U = insert k ?Uk"
wenzelm@53854
   455
    by blast
wenzelm@53253
   456
  {
wenzelm@53253
   457
    fix j
wenzelm@53253
   458
    assume j: "j \<in> ?Uk"
wenzelm@53854
   459
    from j have "?f j $ p j = ?g j $ p j"
wenzelm@53854
   460
      by simp
wenzelm@53253
   461
  }
himmelma@33175
   462
  then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"
himmelma@33175
   463
    apply -
haftmann@57418
   464
    apply (rule setprod.cong)
wenzelm@53253
   465
    apply simp_all
himmelma@33175
   466
    done
wenzelm@53854
   467
  have th3: "finite ?Uk" "k \<notin> ?Uk"
wenzelm@53854
   468
    by auto
himmelma@33175
   469
  have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
himmelma@33175
   470
    unfolding kU[symmetric] ..
himmelma@33175
   471
  also have "\<dots> = ?f k $ p k  * setprod (\<lambda>i. ?f i $ p i) ?Uk"
haftmann@57418
   472
    apply (rule setprod.insert)
himmelma@33175
   473
    apply simp
wenzelm@53253
   474
    apply blast
wenzelm@53253
   475
    done
wenzelm@53253
   476
  also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk"
wenzelm@53253
   477
    by (simp add: field_simps)
himmelma@33175
   478
  also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)"
haftmann@57514
   479
    unfolding th1 by (simp add: ac_simps)
himmelma@33175
   480
  also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
haftmann@57418
   481
    unfolding setprod.insert[OF th3] by simp
wenzelm@53253
   482
  finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)"
wenzelm@53253
   483
    unfolding kU[symmetric] .
wenzelm@53253
   484
  then show "of_int (sign p) * setprod (\<lambda>i. ?f i $ p i) ?U =
wenzelm@53253
   485
    c * (of_int (sign p) * setprod (\<lambda>i. ?g i $ p i) ?U)"
haftmann@36350
   486
    by (simp add: field_simps)
haftmann@57418
   487
qed rule
himmelma@33175
   488
himmelma@33175
   489
lemma det_row_0:
himmelma@33175
   490
  fixes b :: "'n::finite \<Rightarrow> _ ^ 'n"
himmelma@33175
   491
  shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0"
wenzelm@53253
   492
  using det_row_mul[of k 0 "\<lambda>i. 1" b]
wenzelm@53253
   493
  apply simp
wenzelm@53253
   494
  apply (simp only: vector_smult_lzero)
wenzelm@53253
   495
  done
himmelma@33175
   496
himmelma@33175
   497
lemma det_row_operation:
haftmann@35028
   498
  fixes A :: "'a::linordered_idom^'n^'n"
himmelma@33175
   499
  assumes ij: "i \<noteq> j"
himmelma@33175
   500
  shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A"
wenzelm@53253
   501
proof -
himmelma@33175
   502
  let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n"
himmelma@33175
   503
  have th: "row i ?Z = row j ?Z" by (vector row_def)
himmelma@33175
   504
  have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A"
himmelma@33175
   505
    by (vector row_def)
himmelma@33175
   506
  show ?thesis
himmelma@33175
   507
    unfolding det_row_add [of i] det_row_mul[of i] det_identical_rows[OF ij th] th2
himmelma@33175
   508
    by simp
himmelma@33175
   509
qed
himmelma@33175
   510
himmelma@33175
   511
lemma det_row_span:
huffman@36593
   512
  fixes A :: "real^'n^'n"
himmelma@33175
   513
  assumes x: "x \<in> span {row j A |j. j \<noteq> i}"
himmelma@33175
   514
  shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
wenzelm@53253
   515
proof -
himmelma@33175
   516
  let ?U = "UNIV :: 'n set"
himmelma@33175
   517
  let ?S = "{row j A |j. j \<noteq> i}"
himmelma@33175
   518
  let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)"
himmelma@33175
   519
  let ?P = "\<lambda>x. ?d (row i A + x) = det A"
wenzelm@53253
   520
  {
wenzelm@53253
   521
    fix k
wenzelm@53854
   522
    have "(if k = i then row i A + 0 else row k A) = row k A"
wenzelm@53854
   523
      by simp
wenzelm@53253
   524
  }
himmelma@33175
   525
  then have P0: "?P 0"
himmelma@33175
   526
    apply -
himmelma@33175
   527
    apply (rule cong[of det, OF refl])
wenzelm@53253
   528
    apply (vector row_def)
wenzelm@53253
   529
    done
himmelma@33175
   530
  moreover
wenzelm@53253
   531
  {
wenzelm@53253
   532
    fix c z y
wenzelm@53253
   533
    assume zS: "z \<in> ?S" and Py: "?P y"
wenzelm@53854
   534
    from zS obtain j where j: "z = row j A" "i \<noteq> j"
wenzelm@53854
   535
      by blast
himmelma@33175
   536
    let ?w = "row i A + y"
wenzelm@53854
   537
    have th0: "row i A + (c*s z + y) = ?w + c*s z"
wenzelm@53854
   538
      by vector
himmelma@33175
   539
    have thz: "?d z = 0"
himmelma@33175
   540
      apply (rule det_identical_rows[OF j(2)])
wenzelm@53253
   541
      using j
wenzelm@53253
   542
      apply (vector row_def)
wenzelm@53253
   543
      done
wenzelm@53253
   544
    have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)"
wenzelm@53253
   545
      unfolding th0 ..
wenzelm@53253
   546
    then have "?P (c*s z + y)"
wenzelm@53253
   547
      unfolding thz Py det_row_mul[of i] det_row_add[of i]
wenzelm@53253
   548
      by simp
wenzelm@53253
   549
  }
himmelma@33175
   550
  ultimately show ?thesis
himmelma@33175
   551
    apply -
hoelzl@50526
   552
    apply (rule span_induct_alt[of ?P ?S, OF P0, folded scalar_mult_eq_scaleR])
himmelma@33175
   553
    apply blast
himmelma@33175
   554
    apply (rule x)
himmelma@33175
   555
    done
himmelma@33175
   556
qed
himmelma@33175
   557
wenzelm@53854
   558
text {*
wenzelm@53854
   559
  May as well do this, though it's a bit unsatisfactory since it ignores
wenzelm@53854
   560
  exact duplicates by considering the rows/columns as a set.
wenzelm@53854
   561
*}
himmelma@33175
   562
himmelma@33175
   563
lemma det_dependent_rows:
huffman@36593
   564
  fixes A:: "real^'n^'n"
himmelma@33175
   565
  assumes d: "dependent (rows A)"
himmelma@33175
   566
  shows "det A = 0"
wenzelm@53253
   567
proof -
himmelma@33175
   568
  let ?U = "UNIV :: 'n set"
himmelma@33175
   569
  from d obtain i where i: "row i A \<in> span (rows A - {row i A})"
himmelma@33175
   570
    unfolding dependent_def rows_def by blast
wenzelm@53253
   571
  {
wenzelm@53253
   572
    fix j k
wenzelm@53253
   573
    assume jk: "j \<noteq> k" and c: "row j A = row k A"
wenzelm@53253
   574
    from det_identical_rows[OF jk c] have ?thesis .
wenzelm@53253
   575
  }
himmelma@33175
   576
  moreover
wenzelm@53253
   577
  {
wenzelm@53253
   578
    assume H: "\<And> i j. i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A"
himmelma@33175
   579
    have th0: "- row i A \<in> span {row j A|j. j \<noteq> i}"
himmelma@33175
   580
      apply (rule span_neg)
himmelma@33175
   581
      apply (rule set_rev_mp)
himmelma@33175
   582
      apply (rule i)
himmelma@33175
   583
      apply (rule span_mono)
wenzelm@53253
   584
      using H i
wenzelm@53253
   585
      apply (auto simp add: rows_def)
wenzelm@53253
   586
      done
himmelma@33175
   587
    from det_row_span[OF th0]
himmelma@33175
   588
    have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)"
himmelma@33175
   589
      unfolding right_minus vector_smult_lzero ..
huffman@36593
   590
    with det_row_mul[of i "0::real" "\<lambda>i. 1"]
wenzelm@53253
   591
    have "det A = 0" by simp
wenzelm@53253
   592
  }
himmelma@33175
   593
  ultimately show ?thesis by blast
himmelma@33175
   594
qed
himmelma@33175
   595
wenzelm@53253
   596
lemma det_dependent_columns:
wenzelm@53253
   597
  assumes d: "dependent (columns (A::real^'n^'n))"
wenzelm@53253
   598
  shows "det A = 0"
wenzelm@53253
   599
  by (metis d det_dependent_rows rows_transpose det_transpose)
himmelma@33175
   600
wenzelm@53854
   601
text {* Multilinearity and the multiplication formula. *}
himmelma@33175
   602
huffman@44228
   603
lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (vec_lambda f::'a^'n) = (vec_lambda g :: 'a^'n)"
wenzelm@53253
   604
  by (rule iffD1[OF vec_lambda_unique]) vector
himmelma@33175
   605
himmelma@33175
   606
lemma det_linear_row_setsum:
himmelma@33175
   607
  assumes fS: "finite S"
wenzelm@53253
   608
  shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n) =
wenzelm@53253
   609
    setsum (\<lambda>j. det ((\<chi> i. if i = k then a  i j else c i)::'a^'n^'n)) S"
wenzelm@53253
   610
proof (induct rule: finite_induct[OF fS])
wenzelm@53253
   611
  case 1
wenzelm@53253
   612
  then show ?case
wenzelm@53253
   613
    apply simp
haftmann@57418
   614
    unfolding setsum.empty det_row_0[of k]
wenzelm@53253
   615
    apply rule
wenzelm@53253
   616
    done
himmelma@33175
   617
next
himmelma@33175
   618
  case (2 x F)
wenzelm@53253
   619
  then show ?case
wenzelm@53253
   620
    by (simp add: det_row_add cong del: if_weak_cong)
himmelma@33175
   621
qed
himmelma@33175
   622
himmelma@33175
   623
lemma finite_bounded_functions:
himmelma@33175
   624
  assumes fS: "finite S"
himmelma@33175
   625
  shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"
wenzelm@53253
   626
proof (induct k)
himmelma@33175
   627
  case 0
wenzelm@53854
   628
  have th: "{f. \<forall>i. f i = i} = {id}"
wenzelm@53854
   629
    by auto
wenzelm@53854
   630
  show ?case
wenzelm@53854
   631
    by (auto simp add: th)
himmelma@33175
   632
next
himmelma@33175
   633
  case (Suc k)
himmelma@33175
   634
  let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i"
himmelma@33175
   635
  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)})"
himmelma@33175
   636
  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)}"
himmelma@33175
   637
    apply (auto simp add: image_iff)
himmelma@33175
   638
    apply (rule_tac x="x (Suc k)" in bexI)
himmelma@33175
   639
    apply (rule_tac x = "\<lambda>i. if i = Suc k then i else x i" in exI)
huffman@44457
   640
    apply auto
himmelma@33175
   641
    done
himmelma@33175
   642
  with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]
wenzelm@53854
   643
  show ?case
wenzelm@53854
   644
    by metis
himmelma@33175
   645
qed
himmelma@33175
   646
himmelma@33175
   647
wenzelm@53854
   648
lemma eq_id_iff[simp]: "(\<forall>x. f x = x) \<longleftrightarrow> f = id"
wenzelm@53854
   649
  by auto
himmelma@33175
   650
himmelma@33175
   651
lemma det_linear_rows_setsum_lemma:
wenzelm@53854
   652
  assumes fS: "finite S"
wenzelm@53854
   653
    and fT: "finite T"
wenzelm@53854
   654
  shows "det ((\<chi> i. if i \<in> T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n) =
wenzelm@53253
   655
    setsum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))
wenzelm@53253
   656
      {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
wenzelm@53253
   657
  using fT
wenzelm@53253
   658
proof (induct T arbitrary: a c set: finite)
himmelma@33175
   659
  case empty
wenzelm@53253
   660
  have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)"
wenzelm@53253
   661
    by vector
wenzelm@53854
   662
  from empty.prems show ?case
wenzelm@53854
   663
    unfolding th0 by simp
himmelma@33175
   664
next
himmelma@33175
   665
  case (insert z T a c)
himmelma@33175
   666
  let ?F = "\<lambda>T. {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
himmelma@33175
   667
  let ?h = "\<lambda>(y,g) i. if i = z then y else g i"
himmelma@33175
   668
  let ?k = "\<lambda>h. (h(z),(\<lambda>i. if i = z then i else h i))"
himmelma@33175
   669
  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)"
hoelzl@57129
   670
  let ?c = "\<lambda>j i. if i = z then a i j else c i"
wenzelm@53253
   671
  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)"
wenzelm@53253
   672
    by simp
himmelma@33175
   673
  have thif2: "\<And>a b c d e. (if a then b else if c then d else e) =
wenzelm@53253
   674
     (if c then (if a then b else d) else (if a then b else e))"
wenzelm@53253
   675
    by simp
wenzelm@53253
   676
  from `z \<notin> T` have nz: "\<And>i. i \<in> T \<Longrightarrow> i = z \<longleftrightarrow> False"
wenzelm@53253
   677
    by auto
himmelma@33175
   678
  have "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) =
wenzelm@53253
   679
    det (\<chi> i. if i = z then setsum (a i) S else if i \<in> T then setsum (a i) S else c i)"
himmelma@33175
   680
    unfolding insert_iff thif ..
wenzelm@53253
   681
  also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<in> T then setsum (a i) S else if i = z then a i j else c i))"
himmelma@33175
   682
    unfolding det_linear_row_setsum[OF fS]
himmelma@33175
   683
    apply (subst thif2)
wenzelm@53253
   684
    using nz
wenzelm@53253
   685
    apply (simp cong del: if_weak_cong cong add: if_cong)
wenzelm@53253
   686
    done
himmelma@33175
   687
  finally have tha:
himmelma@33175
   688
    "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) =
himmelma@33175
   689
     (\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i)
himmelma@33175
   690
                                else if i = z then a i j
himmelma@33175
   691
                                else c i))"
haftmann@57418
   692
    unfolding insert.hyps unfolding setsum.cartesian_product by blast
himmelma@33175
   693
  show ?case unfolding tha
himmelma@33175
   694
    using `z \<notin> T`
hoelzl@57129
   695
    by (intro setsum.reindex_bij_witness[where i="?k" and j="?h"])
hoelzl@57129
   696
       (auto intro!: cong[OF refl[of det]] simp: vec_eq_iff)
himmelma@33175
   697
qed
himmelma@33175
   698
himmelma@33175
   699
lemma det_linear_rows_setsum:
wenzelm@53854
   700
  fixes S :: "'n::finite set"
wenzelm@53854
   701
  assumes fS: "finite S"
wenzelm@53253
   702
  shows "det (\<chi> i. setsum (a i) S) =
wenzelm@53253
   703
    setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n)) {f. \<forall>i. f i \<in> S}"
wenzelm@53253
   704
proof -
wenzelm@53253
   705
  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)"
wenzelm@53253
   706
    by vector
wenzelm@53253
   707
  from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite]
wenzelm@53253
   708
  show ?thesis by simp
himmelma@33175
   709
qed
himmelma@33175
   710
himmelma@33175
   711
lemma matrix_mul_setsum_alt:
hoelzl@34291
   712
  fixes A B :: "'a::comm_ring_1^'n^'n"
himmelma@33175
   713
  shows "A ** B = (\<chi> i. setsum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))"
himmelma@33175
   714
  by (vector matrix_matrix_mult_def setsum_component)
himmelma@33175
   715
himmelma@33175
   716
lemma det_rows_mul:
hoelzl@34291
   717
  "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n) =
wenzelm@53253
   718
    setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
haftmann@57418
   719
proof (simp add: det_def setsum_right_distrib cong add: setprod.cong, rule setsum.cong)
himmelma@33175
   720
  let ?U = "UNIV :: 'n set"
himmelma@33175
   721
  let ?PU = "{p. p permutes ?U}"
wenzelm@53253
   722
  fix p
wenzelm@53253
   723
  assume pU: "p \<in> ?PU"
himmelma@33175
   724
  let ?s = "of_int (sign p)"
wenzelm@53253
   725
  from pU have p: "p permutes ?U"
wenzelm@53253
   726
    by blast
himmelma@33175
   727
  have "setprod (\<lambda>i. c i * a i $ p i) ?U = setprod c ?U * setprod (\<lambda>i. a i $ p i) ?U"
haftmann@57418
   728
    unfolding setprod.distrib ..
himmelma@33175
   729
  then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) =
wenzelm@53854
   730
    setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))"
wenzelm@53854
   731
    by (simp add: field_simps)
haftmann@57418
   732
qed rule
himmelma@33175
   733
himmelma@33175
   734
lemma det_mul:
haftmann@35028
   735
  fixes A B :: "'a::linordered_idom^'n^'n"
himmelma@33175
   736
  shows "det (A ** B) = det A * det B"
wenzelm@53253
   737
proof -
himmelma@33175
   738
  let ?U = "UNIV :: 'n set"
himmelma@33175
   739
  let ?F = "{f. (\<forall>i\<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}"
himmelma@33175
   740
  let ?PU = "{p. p permutes ?U}"
wenzelm@53854
   741
  have fU: "finite ?U"
wenzelm@53854
   742
    by simp
wenzelm@53854
   743
  have fF: "finite ?F"
wenzelm@53854
   744
    by (rule finite)
wenzelm@53253
   745
  {
wenzelm@53253
   746
    fix p
wenzelm@53253
   747
    assume p: "p permutes ?U"
himmelma@33175
   748
    have "p \<in> ?F" unfolding mem_Collect_eq permutes_in_image[OF p]
wenzelm@53253
   749
      using p[unfolded permutes_def] by simp
wenzelm@53253
   750
  }
wenzelm@53854
   751
  then have PUF: "?PU \<subseteq> ?F" by blast
wenzelm@53253
   752
  {
wenzelm@53253
   753
    fix f
wenzelm@53253
   754
    assume fPU: "f \<in> ?F - ?PU"
wenzelm@53854
   755
    have fUU: "f ` ?U \<subseteq> ?U"
wenzelm@53854
   756
      using fPU by auto
wenzelm@53253
   757
    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)"
wenzelm@53253
   758
      unfolding permutes_def by auto
himmelma@33175
   759
himmelma@33175
   760
    let ?A = "(\<chi> i. A$i$f i *s B$f i) :: 'a^'n^'n"
himmelma@33175
   761
    let ?B = "(\<chi> i. B$f i) :: 'a^'n^'n"
wenzelm@53253
   762
    {
wenzelm@53253
   763
      assume fni: "\<not> inj_on f ?U"
himmelma@33175
   764
      then obtain i j where ij: "f i = f j" "i \<noteq> j"
himmelma@33175
   765
        unfolding inj_on_def by blast
himmelma@33175
   766
      from ij
wenzelm@53854
   767
      have rth: "row i ?B = row j ?B"
wenzelm@53854
   768
        by (vector row_def)
himmelma@33175
   769
      from det_identical_rows[OF ij(2) rth]
himmelma@33175
   770
      have "det (\<chi> i. A$i$f i *s B$f i) = 0"
wenzelm@53253
   771
        unfolding det_rows_mul by simp
wenzelm@53253
   772
    }
himmelma@33175
   773
    moreover
wenzelm@53253
   774
    {
wenzelm@53253
   775
      assume fi: "inj_on f ?U"
himmelma@33175
   776
      from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j"
himmelma@33175
   777
        unfolding inj_on_def by metis
himmelma@33175
   778
      note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]]
wenzelm@53253
   779
      {
wenzelm@53253
   780
        fix y
wenzelm@53854
   781
        from fs f have "\<exists>x. f x = y"
wenzelm@53854
   782
          by blast
wenzelm@53854
   783
        then obtain x where x: "f x = y"
wenzelm@53854
   784
          by blast
wenzelm@53253
   785
        {
wenzelm@53253
   786
          fix z
wenzelm@53253
   787
          assume z: "f z = y"
wenzelm@53854
   788
          from fith x z have "z = x"
wenzelm@53854
   789
            by metis
wenzelm@53253
   790
        }
wenzelm@53854
   791
        with x have "\<exists>!x. f x = y"
wenzelm@53854
   792
          by blast
wenzelm@53253
   793
      }
wenzelm@53854
   794
      with f(3) have "det (\<chi> i. A$i$f i *s B$f i) = 0"
wenzelm@53854
   795
        by blast
wenzelm@53253
   796
    }
wenzelm@53854
   797
    ultimately have "det (\<chi> i. A$i$f i *s B$f i) = 0"
wenzelm@53854
   798
      by blast
wenzelm@53253
   799
  }
wenzelm@53854
   800
  then have zth: "\<forall> f\<in> ?F - ?PU. det (\<chi> i. A$i$f i *s B$f i) = 0"
wenzelm@53253
   801
    by simp
wenzelm@53253
   802
  {
wenzelm@53253
   803
    fix p
wenzelm@53253
   804
    assume pU: "p \<in> ?PU"
wenzelm@53854
   805
    from pU have p: "p permutes ?U"
wenzelm@53854
   806
      by blast
himmelma@33175
   807
    let ?s = "\<lambda>p. of_int (sign p)"
wenzelm@53253
   808
    let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))"
himmelma@33175
   809
    have "(setsum (\<lambda>q. ?s q *
wenzelm@53253
   810
        (\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) =
wenzelm@53253
   811
      (setsum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) * (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))) ?PU)"
himmelma@33175
   812
      unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f]
haftmann@57418
   813
    proof (rule setsum.cong)
wenzelm@53253
   814
      fix q
wenzelm@53253
   815
      assume qU: "q \<in> ?PU"
wenzelm@53854
   816
      then have q: "q permutes ?U"
wenzelm@53854
   817
        by blast
himmelma@33175
   818
      from p q have pp: "permutation p" and pq: "permutation q"
himmelma@33175
   819
        unfolding permutation_permutes by auto
himmelma@33175
   820
      have th00: "of_int (sign p) * of_int (sign p) = (1::'a)"
himmelma@33175
   821
        "\<And>a. of_int (sign p) * (of_int (sign p) * a) = a"
haftmann@57512
   822
        unfolding mult.assoc[symmetric]
wenzelm@53854
   823
        unfolding of_int_mult[symmetric]
himmelma@33175
   824
        by (simp_all add: sign_idempotent)
wenzelm@53854
   825
      have ths: "?s q = ?s p * ?s (q \<circ> inv p)"
himmelma@33175
   826
        using pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
haftmann@57514
   827
        by (simp add:  th00 ac_simps sign_idempotent sign_compose)
wenzelm@53854
   828
      have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) \<circ> p) ?U"
himmelma@33175
   829
        by (rule setprod_permute[OF p])
wenzelm@53253
   830
      have thp: "setprod (\<lambda>i. (\<chi> i. A$i$p i *s B$p i :: 'a^'n^'n) $i $ q i) ?U =
wenzelm@53253
   831
        setprod (\<lambda>i. A$i$p i) ?U * setprod (\<lambda>i. B$i$ q (inv p i)) ?U"
haftmann@57418
   832
        unfolding th001 setprod.distrib[symmetric] o_def permutes_inverses[OF p]
haftmann@57418
   833
        apply (rule setprod.cong[OF refl])
wenzelm@53253
   834
        using permutes_in_image[OF q]
wenzelm@53253
   835
        apply vector
wenzelm@53253
   836
        done
wenzelm@53253
   837
      show "?s q * setprod (\<lambda>i. (((\<chi> i. A$i$p i *s B$p i) :: 'a^'n^'n)$i$q i)) ?U =
wenzelm@53854
   838
        ?s p * (setprod (\<lambda>i. A$i$p i) ?U) * (?s (q \<circ> inv p) * setprod (\<lambda>i. B$i$(q \<circ> inv p) i) ?U)"
himmelma@33175
   839
        using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
haftmann@36350
   840
        by (simp add: sign_nz th00 field_simps sign_idempotent sign_compose)
haftmann@57418
   841
    qed rule
himmelma@33175
   842
  }
himmelma@33175
   843
  then have th2: "setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B"
himmelma@33175
   844
    unfolding det_def setsum_product
haftmann@57418
   845
    by (rule setsum.cong [OF refl])
himmelma@33175
   846
  have "det (A**B) = setsum (\<lambda>f.  det (\<chi> i. A $ i $ f i *s B $ f i)) ?F"
wenzelm@53854
   847
    unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU]
wenzelm@53854
   848
    by simp
himmelma@33175
   849
  also have "\<dots> = setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU"
haftmann@57418
   850
    using setsum.mono_neutral_cong_left[OF fF PUF zth, symmetric]
himmelma@33175
   851
    unfolding det_rows_mul by auto
himmelma@33175
   852
  finally show ?thesis unfolding th2 .
himmelma@33175
   853
qed
himmelma@33175
   854
wenzelm@53854
   855
text {* Relation to invertibility. *}
himmelma@33175
   856
himmelma@33175
   857
lemma invertible_left_inverse:
hoelzl@34291
   858
  fixes A :: "real^'n^'n"
himmelma@33175
   859
  shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). B** A = mat 1)"
himmelma@33175
   860
  by (metis invertible_def matrix_left_right_inverse)
himmelma@33175
   861
himmelma@33175
   862
lemma invertible_righ_inverse:
hoelzl@34291
   863
  fixes A :: "real^'n^'n"
himmelma@33175
   864
  shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). A** B = mat 1)"
himmelma@33175
   865
  by (metis invertible_def matrix_left_right_inverse)
himmelma@33175
   866
himmelma@33175
   867
lemma invertible_det_nz:
hoelzl@34291
   868
  fixes A::"real ^'n^'n"
himmelma@33175
   869
  shows "invertible A \<longleftrightarrow> det A \<noteq> 0"
wenzelm@53253
   870
proof -
wenzelm@53253
   871
  {
wenzelm@53253
   872
    assume "invertible A"
himmelma@33175
   873
    then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1"
himmelma@33175
   874
      unfolding invertible_righ_inverse by blast
wenzelm@53854
   875
    then have "det (A ** B) = det (mat 1 :: real ^'n^'n)"
wenzelm@53854
   876
      by simp
wenzelm@53854
   877
    then have "det A \<noteq> 0"
wenzelm@53854
   878
      by (simp add: det_mul det_I) algebra
wenzelm@53253
   879
  }
himmelma@33175
   880
  moreover
wenzelm@53253
   881
  {
wenzelm@53253
   882
    assume H: "\<not> invertible A"
himmelma@33175
   883
    let ?U = "UNIV :: 'n set"
wenzelm@53854
   884
    have fU: "finite ?U"
wenzelm@53854
   885
      by simp
himmelma@33175
   886
    from H obtain c i where c: "setsum (\<lambda>i. c i *s row i A) ?U = 0"
wenzelm@53854
   887
      and iU: "i \<in> ?U"
wenzelm@53854
   888
      and ci: "c i \<noteq> 0"
himmelma@33175
   889
      unfolding invertible_righ_inverse
wenzelm@53854
   890
      unfolding matrix_right_invertible_independent_rows
wenzelm@53854
   891
      by blast
wenzelm@53253
   892
    have *: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b"
himmelma@33175
   893
      apply (drule_tac f="op + (- a)" in cong[OF refl])
haftmann@57512
   894
      apply (simp only: ab_left_minus add.assoc[symmetric])
himmelma@33175
   895
      apply simp
himmelma@33175
   896
      done
himmelma@33175
   897
    from c ci
himmelma@33175
   898
    have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
haftmann@57418
   899
      unfolding setsum.remove[OF fU iU] setsum_cmul
himmelma@33175
   900
      apply -
himmelma@33175
   901
      apply (rule vector_mul_lcancel_imp[OF ci])
huffman@44457
   902
      apply (auto simp add: field_simps)
wenzelm@53854
   903
      unfolding *
wenzelm@53854
   904
      apply rule
wenzelm@53854
   905
      done
himmelma@33175
   906
    have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
himmelma@33175
   907
      unfolding thr0
himmelma@33175
   908
      apply (rule span_setsum)
himmelma@33175
   909
      apply simp
himmelma@33175
   910
      apply (rule ballI)
hoelzl@50526
   911
      apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
himmelma@33175
   912
      apply (rule span_superset)
himmelma@33175
   913
      apply auto
himmelma@33175
   914
      done
himmelma@33175
   915
    let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n"
himmelma@33175
   916
    have thrb: "row i ?B = 0" using iU by (vector row_def)
himmelma@33175
   917
    have "det A = 0"
himmelma@33175
   918
      unfolding det_row_span[OF thr, symmetric] right_minus
wenzelm@53253
   919
      unfolding det_zero_row[OF thrb] ..
wenzelm@53253
   920
  }
wenzelm@53854
   921
  ultimately show ?thesis
wenzelm@53854
   922
    by blast
himmelma@33175
   923
qed
himmelma@33175
   924
wenzelm@53854
   925
text {* Cramer's rule. *}
himmelma@33175
   926
hoelzl@35150
   927
lemma cramer_lemma_transpose:
wenzelm@53854
   928
  fixes A:: "real^'n^'n"
wenzelm@53854
   929
    and x :: "real^'n"
himmelma@33175
   930
  shows "det ((\<chi> i. if i = k then setsum (\<lambda>i. x$i *s row i A) (UNIV::'n set)
wenzelm@53854
   931
                             else row i A)::real^'n^'n) = x$k * det A"
himmelma@33175
   932
  (is "?lhs = ?rhs")
wenzelm@53253
   933
proof -
himmelma@33175
   934
  let ?U = "UNIV :: 'n set"
himmelma@33175
   935
  let ?Uk = "?U - {k}"
wenzelm@53854
   936
  have U: "?U = insert k ?Uk"
wenzelm@53854
   937
    by blast
wenzelm@53854
   938
  have fUk: "finite ?Uk"
wenzelm@53854
   939
    by simp
wenzelm@53854
   940
  have kUk: "k \<notin> ?Uk"
wenzelm@53854
   941
    by simp
himmelma@33175
   942
  have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s"
haftmann@36350
   943
    by (vector field_simps)
wenzelm@53854
   944
  have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f"
wenzelm@53854
   945
    by auto
himmelma@33175
   946
  have "(\<chi> i. row i A) = A" by (vector row_def)
wenzelm@53253
   947
  then have thd1: "det (\<chi> i. row i A) = det A"
wenzelm@53253
   948
    by simp
himmelma@33175
   949
  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"
himmelma@33175
   950
    apply (rule det_row_span)
huffman@56196
   951
    apply (rule span_setsum)
himmelma@33175
   952
    apply (rule ballI)
hoelzl@50526
   953
    apply (rule span_mul [where 'a="real^'n", folded scalar_mult_eq_scaleR])+
himmelma@33175
   954
    apply (rule span_superset)
himmelma@33175
   955
    apply auto
himmelma@33175
   956
    done
himmelma@33175
   957
  show "?lhs = x$k * det A"
himmelma@33175
   958
    apply (subst U)
haftmann@57418
   959
    unfolding setsum.insert[OF fUk kUk]
himmelma@33175
   960
    apply (subst th00)
haftmann@57512
   961
    unfolding add.assoc
himmelma@33175
   962
    apply (subst det_row_add)
himmelma@33175
   963
    unfolding thd0
himmelma@33175
   964
    unfolding det_row_mul
himmelma@33175
   965
    unfolding th001[of k "\<lambda>i. row i A"]
wenzelm@53253
   966
    unfolding thd1
wenzelm@53253
   967
    apply (simp add: field_simps)
wenzelm@53253
   968
    done
himmelma@33175
   969
qed
himmelma@33175
   970
himmelma@33175
   971
lemma cramer_lemma:
huffman@36593
   972
  fixes A :: "real^'n^'n"
huffman@36593
   973
  shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: real^'n^'n) = x$k * det A"
wenzelm@53253
   974
proof -
himmelma@33175
   975
  let ?U = "UNIV :: 'n set"
wenzelm@53253
   976
  have *: "\<And>c. setsum (\<lambda>i. c i *s row i (transpose A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U"
haftmann@57418
   977
    by (auto simp add: row_transpose intro: setsum.cong)
wenzelm@53854
   978
  show ?thesis
wenzelm@53854
   979
    unfolding matrix_mult_vsum
wenzelm@53253
   980
    unfolding cramer_lemma_transpose[of k x "transpose A", unfolded det_transpose, symmetric]
wenzelm@53253
   981
    unfolding *[of "\<lambda>i. x$i"]
wenzelm@53253
   982
    apply (subst det_transpose[symmetric])
wenzelm@53253
   983
    apply (rule cong[OF refl[of det]])
wenzelm@53253
   984
    apply (vector transpose_def column_def row_def)
wenzelm@53253
   985
    done
himmelma@33175
   986
qed
himmelma@33175
   987
himmelma@33175
   988
lemma cramer:
hoelzl@34291
   989
  fixes A ::"real^'n^'n"
himmelma@33175
   990
  assumes d0: "det A \<noteq> 0"
huffman@36362
   991
  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)"
wenzelm@53253
   992
proof -
himmelma@33175
   993
  from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"
wenzelm@53854
   994
    unfolding invertible_det_nz[symmetric] invertible_def
wenzelm@53854
   995
    by blast
wenzelm@53854
   996
  have "(A ** B) *v b = b"
wenzelm@53854
   997
    by (simp add: B matrix_vector_mul_lid)
wenzelm@53854
   998
  then have "A *v (B *v b) = b"
wenzelm@53854
   999
    by (simp add: matrix_vector_mul_assoc)
wenzelm@53854
  1000
  then have xe: "\<exists>x. A *v x = b"
wenzelm@53854
  1001
    by blast
wenzelm@53253
  1002
  {
wenzelm@53253
  1003
    fix x
wenzelm@53253
  1004
    assume x: "A *v x = b"
wenzelm@53253
  1005
    have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j) / det A)"
wenzelm@53253
  1006
      unfolding x[symmetric]
wenzelm@53253
  1007
      using d0 by (simp add: vec_eq_iff cramer_lemma field_simps)
wenzelm@53253
  1008
  }
wenzelm@53854
  1009
  with xe show ?thesis
wenzelm@53854
  1010
    by auto
himmelma@33175
  1011
qed
himmelma@33175
  1012
wenzelm@53854
  1013
text {* Orthogonality of a transformation and matrix. *}
himmelma@33175
  1014
himmelma@33175
  1015
definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
himmelma@33175
  1016
wenzelm@53253
  1017
lemma orthogonal_transformation:
wenzelm@53253
  1018
  "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>(v::real ^_). norm (f v) = norm v)"
himmelma@33175
  1019
  unfolding orthogonal_transformation_def
himmelma@33175
  1020
  apply auto
himmelma@33175
  1021
  apply (erule_tac x=v in allE)+
himmelma@35542
  1022
  apply (simp add: norm_eq_sqrt_inner)
wenzelm@53253
  1023
  apply (simp add: dot_norm  linear_add[symmetric])
wenzelm@53253
  1024
  done
himmelma@33175
  1025
wenzelm@53253
  1026
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
wenzelm@53253
  1027
  transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
himmelma@33175
  1028
wenzelm@53253
  1029
lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
himmelma@33175
  1030
  by (metis matrix_left_right_inverse orthogonal_matrix_def)
himmelma@33175
  1031
hoelzl@34291
  1032
lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
hoelzl@35150
  1033
  by (simp add: orthogonal_matrix_def transpose_mat matrix_mul_lid)
himmelma@33175
  1034
himmelma@33175
  1035
lemma orthogonal_matrix_mul:
hoelzl@34291
  1036
  fixes A :: "real ^'n^'n"
himmelma@33175
  1037
  assumes oA : "orthogonal_matrix A"
wenzelm@53253
  1038
    and oB: "orthogonal_matrix B"
himmelma@33175
  1039
  shows "orthogonal_matrix(A ** B)"
himmelma@33175
  1040
  using oA oB
hoelzl@35150
  1041
  unfolding orthogonal_matrix matrix_transpose_mul
himmelma@33175
  1042
  apply (subst matrix_mul_assoc)
himmelma@33175
  1043
  apply (subst matrix_mul_assoc[symmetric])
wenzelm@53253
  1044
  apply (simp add: matrix_mul_rid)
wenzelm@53253
  1045
  done
himmelma@33175
  1046
himmelma@33175
  1047
lemma orthogonal_transformation_matrix:
hoelzl@34291
  1048
  fixes f:: "real^'n \<Rightarrow> real^'n"
himmelma@33175
  1049
  shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
himmelma@33175
  1050
  (is "?lhs \<longleftrightarrow> ?rhs")
wenzelm@53253
  1051
proof -
himmelma@33175
  1052
  let ?mf = "matrix f"
himmelma@33175
  1053
  let ?ot = "orthogonal_transformation f"
himmelma@33175
  1054
  let ?U = "UNIV :: 'n set"
himmelma@33175
  1055
  have fU: "finite ?U" by simp
himmelma@33175
  1056
  let ?m1 = "mat 1 :: real ^'n^'n"
wenzelm@53253
  1057
  {
wenzelm@53253
  1058
    assume ot: ?ot
himmelma@33175
  1059
    from ot have lf: "linear f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w"
himmelma@33175
  1060
      unfolding  orthogonal_transformation_def orthogonal_matrix by blast+
wenzelm@53253
  1061
    {
wenzelm@53253
  1062
      fix i j
hoelzl@35150
  1063
      let ?A = "transpose ?mf ** ?mf"
himmelma@33175
  1064
      have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
himmelma@33175
  1065
        "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"
himmelma@33175
  1066
        by simp_all
hoelzl@50526
  1067
      from fd[rule_format, of "axis i 1" "axis j 1", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
himmelma@33175
  1068
      have "?A$i$j = ?m1 $ i $ j"
hoelzl@50526
  1069
        by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def
haftmann@57418
  1070
            th0 setsum.delta[OF fU] mat_def axis_def)
wenzelm@53253
  1071
    }
wenzelm@53854
  1072
    then have "orthogonal_matrix ?mf"
wenzelm@53854
  1073
      unfolding orthogonal_matrix
wenzelm@53253
  1074
      by vector
wenzelm@53854
  1075
    with lf have ?rhs
wenzelm@53854
  1076
      by blast
wenzelm@53253
  1077
  }
himmelma@33175
  1078
  moreover
wenzelm@53253
  1079
  {
wenzelm@53253
  1080
    assume lf: "linear f" and om: "orthogonal_matrix ?mf"
himmelma@33175
  1081
    from lf om have ?lhs
himmelma@33175
  1082
      unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
himmelma@33175
  1083
      unfolding matrix_works[OF lf, symmetric]
himmelma@33175
  1084
      apply (subst dot_matrix_vector_mul)
wenzelm@53253
  1085
      apply (simp add: dot_matrix_product matrix_mul_lid)
wenzelm@53253
  1086
      done
wenzelm@53253
  1087
  }
wenzelm@53854
  1088
  ultimately show ?thesis
wenzelm@53854
  1089
    by blast
himmelma@33175
  1090
qed
himmelma@33175
  1091
himmelma@33175
  1092
lemma det_orthogonal_matrix:
haftmann@35028
  1093
  fixes Q:: "'a::linordered_idom^'n^'n"
himmelma@33175
  1094
  assumes oQ: "orthogonal_matrix Q"
himmelma@33175
  1095
  shows "det Q = 1 \<or> det Q = - 1"
wenzelm@53253
  1096
proof -
himmelma@33175
  1097
  have th: "\<And>x::'a. x = 1 \<or> x = - 1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x")
wenzelm@53253
  1098
  proof -
himmelma@33175
  1099
    fix x:: 'a
wenzelm@53854
  1100
    have th0: "x * x - 1 = (x - 1) * (x + 1)"
wenzelm@53253
  1101
      by (simp add: field_simps)
himmelma@33175
  1102
    have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0"
wenzelm@53253
  1103
      apply (subst eq_iff_diff_eq_0)
wenzelm@53253
  1104
      apply simp
wenzelm@53253
  1105
      done
wenzelm@53854
  1106
    have "x * x = 1 \<longleftrightarrow> x * x - 1 = 0"
wenzelm@53854
  1107
      by simp
wenzelm@53854
  1108
    also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1"
wenzelm@53854
  1109
      unfolding th0 th1 by simp
himmelma@33175
  1110
    finally show "?ths x" ..
himmelma@33175
  1111
  qed
wenzelm@53253
  1112
  from oQ have "Q ** transpose Q = mat 1"
wenzelm@53253
  1113
    by (metis orthogonal_matrix_def)
wenzelm@53253
  1114
  then have "det (Q ** transpose Q) = det (mat 1:: 'a^'n^'n)"
wenzelm@53253
  1115
    by simp
wenzelm@53253
  1116
  then have "det Q * det Q = 1"
wenzelm@53253
  1117
    by (simp add: det_mul det_I det_transpose)
himmelma@33175
  1118
  then show ?thesis unfolding th .
himmelma@33175
  1119
qed
himmelma@33175
  1120
wenzelm@53854
  1121
text {* Linearity of scaling, and hence isometry, that preserves origin. *}
wenzelm@53854
  1122
himmelma@33175
  1123
lemma scaling_linear:
hoelzl@34291
  1124
  fixes f :: "real ^'n \<Rightarrow> real ^'n"
wenzelm@53253
  1125
  assumes f0: "f 0 = 0"
wenzelm@53253
  1126
    and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
himmelma@33175
  1127
  shows "linear f"
wenzelm@53253
  1128
proof -
wenzelm@53253
  1129
  {
wenzelm@53253
  1130
    fix v w
wenzelm@53253
  1131
    {
wenzelm@53253
  1132
      fix x
wenzelm@53253
  1133
      note fd[rule_format, of x 0, unfolded dist_norm f0 diff_0_right]
wenzelm@53253
  1134
    }
himmelma@33175
  1135
    note th0 = this
wenzelm@53077
  1136
    have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
himmelma@33175
  1137
      unfolding dot_norm_neg dist_norm[symmetric]
himmelma@33175
  1138
      unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
himmelma@33175
  1139
  note fc = this
hoelzl@50526
  1140
  show ?thesis
huffman@53600
  1141
    unfolding linear_iff vector_eq[where 'a="real^'n"] scalar_mult_eq_scaleR
hoelzl@50526
  1142
    by (simp add: inner_add fc field_simps)
himmelma@33175
  1143
qed
himmelma@33175
  1144
himmelma@33175
  1145
lemma isometry_linear:
wenzelm@53253
  1146
  "f (0:: real^'n) = (0:: real^'n) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
wenzelm@53253
  1147
  by (rule scaling_linear[where c=1]) simp_all
himmelma@33175
  1148
wenzelm@53854
  1149
text {* Hence another formulation of orthogonal transformation. *}
himmelma@33175
  1150
himmelma@33175
  1151
lemma orthogonal_transformation_isometry:
hoelzl@34291
  1152
  "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
himmelma@33175
  1153
  unfolding orthogonal_transformation
himmelma@33175
  1154
  apply (rule iffI)
himmelma@33175
  1155
  apply clarify
himmelma@33175
  1156
  apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_norm)
himmelma@33175
  1157
  apply (rule conjI)
himmelma@33175
  1158
  apply (rule isometry_linear)
himmelma@33175
  1159
  apply simp
himmelma@33175
  1160
  apply simp
himmelma@33175
  1161
  apply clarify
himmelma@33175
  1162
  apply (erule_tac x=v in allE)
himmelma@33175
  1163
  apply (erule_tac x=0 in allE)
wenzelm@53253
  1164
  apply (simp add: dist_norm)
wenzelm@53253
  1165
  done
himmelma@33175
  1166
wenzelm@53854
  1167
text {* Can extend an isometry from unit sphere. *}
himmelma@33175
  1168
himmelma@33175
  1169
lemma isometry_sphere_extend:
hoelzl@34291
  1170
  fixes f:: "real ^'n \<Rightarrow> real ^'n"
himmelma@33175
  1171
  assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1"
wenzelm@53253
  1172
    and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y"
himmelma@33175
  1173
  shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
wenzelm@53253
  1174
proof -
wenzelm@53253
  1175
  {
wenzelm@53253
  1176
    fix x y x' y' x0 y0 x0' y0' :: "real ^'n"
wenzelm@53253
  1177
    assume H:
wenzelm@53253
  1178
      "x = norm x *\<^sub>R x0"
wenzelm@53253
  1179
      "y = norm y *\<^sub>R y0"
wenzelm@53253
  1180
      "x' = norm x *\<^sub>R x0'" "y' = norm y *\<^sub>R y0'"
wenzelm@53253
  1181
      "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1"
wenzelm@53253
  1182
      "norm(x0' - y0') = norm(x0 - y0)"
wenzelm@53854
  1183
    then have *: "x0 \<bullet> y0 = x0' \<bullet> y0' + y0' \<bullet> x0' - y0 \<bullet> x0 "
wenzelm@53253
  1184
      by (simp add: norm_eq norm_eq_1 inner_add inner_diff)
himmelma@33175
  1185
    have "norm(x' - y') = norm(x - y)"
himmelma@33175
  1186
      apply (subst H(1))
himmelma@33175
  1187
      apply (subst H(2))
himmelma@33175
  1188
      apply (subst H(3))
himmelma@33175
  1189
      apply (subst H(4))
himmelma@33175
  1190
      using H(5-9)
himmelma@33175
  1191
      apply (simp add: norm_eq norm_eq_1)
wenzelm@53854
  1192
      apply (simp add: inner_diff scalar_mult_eq_scaleR)
wenzelm@53854
  1193
      unfolding *
wenzelm@53253
  1194
      apply (simp add: field_simps)
wenzelm@53253
  1195
      done
wenzelm@53253
  1196
  }
himmelma@33175
  1197
  note th0 = this
huffman@44228
  1198
  let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)"
wenzelm@53253
  1199
  {
wenzelm@53253
  1200
    fix x:: "real ^'n"
wenzelm@53253
  1201
    assume nx: "norm x = 1"
wenzelm@53854
  1202
    have "?g x = f x"
wenzelm@53854
  1203
      using nx by auto
wenzelm@53253
  1204
  }
wenzelm@53253
  1205
  then have thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x"
wenzelm@53253
  1206
    by blast
wenzelm@53854
  1207
  have g0: "?g 0 = 0"
wenzelm@53854
  1208
    by simp
wenzelm@53253
  1209
  {
wenzelm@53253
  1210
    fix x y :: "real ^'n"
wenzelm@53253
  1211
    {
wenzelm@53253
  1212
      assume "x = 0" "y = 0"
wenzelm@53854
  1213
      then have "dist (?g x) (?g y) = dist x y"
wenzelm@53854
  1214
        by simp
wenzelm@53253
  1215
    }
himmelma@33175
  1216
    moreover
wenzelm@53253
  1217
    {
wenzelm@53253
  1218
      assume "x = 0" "y \<noteq> 0"
himmelma@33175
  1219
      then have "dist (?g x) (?g y) = dist x y"
huffman@36362
  1220
        apply (simp add: dist_norm)
himmelma@33175
  1221
        apply (rule f1[rule_format])
wenzelm@53253
  1222
        apply (simp add: field_simps)
wenzelm@53253
  1223
        done
wenzelm@53253
  1224
    }
himmelma@33175
  1225
    moreover
wenzelm@53253
  1226
    {
wenzelm@53253
  1227
      assume "x \<noteq> 0" "y = 0"
himmelma@33175
  1228
      then have "dist (?g x) (?g y) = dist x y"
huffman@36362
  1229
        apply (simp add: dist_norm)
himmelma@33175
  1230
        apply (rule f1[rule_format])
wenzelm@53253
  1231
        apply (simp add: field_simps)
wenzelm@53253
  1232
        done
wenzelm@53253
  1233
    }
himmelma@33175
  1234
    moreover
wenzelm@53253
  1235
    {
wenzelm@53253
  1236
      assume z: "x \<noteq> 0" "y \<noteq> 0"
wenzelm@53253
  1237
      have th00:
wenzelm@53253
  1238
        "x = norm x *\<^sub>R (inverse (norm x) *\<^sub>R x)"
wenzelm@53253
  1239
        "y = norm y *\<^sub>R (inverse (norm y) *\<^sub>R y)"
wenzelm@53253
  1240
        "norm x *\<^sub>R f ((inverse (norm x) *\<^sub>R x)) = norm x *\<^sub>R f (inverse (norm x) *\<^sub>R x)"
huffman@44228
  1241
        "norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y) = norm y *\<^sub>R f (inverse (norm y) *\<^sub>R y)"
huffman@44228
  1242
        "norm (inverse (norm x) *\<^sub>R x) = 1"
huffman@44228
  1243
        "norm (f (inverse (norm x) *\<^sub>R x)) = 1"
huffman@44228
  1244
        "norm (inverse (norm y) *\<^sub>R y) = 1"
huffman@44228
  1245
        "norm (f (inverse (norm y) *\<^sub>R y)) = 1"
huffman@44228
  1246
        "norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) =
wenzelm@53253
  1247
          norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
himmelma@33175
  1248
        using z
huffman@44457
  1249
        by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
himmelma@33175
  1250
      from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
wenzelm@53253
  1251
        by (simp add: dist_norm)
wenzelm@53253
  1252
    }
wenzelm@53854
  1253
    ultimately have "dist (?g x) (?g y) = dist x y"
wenzelm@53854
  1254
      by blast
wenzelm@53253
  1255
  }
himmelma@33175
  1256
  note thd = this
himmelma@33175
  1257
    show ?thesis
himmelma@33175
  1258
    apply (rule exI[where x= ?g])
himmelma@33175
  1259
    unfolding orthogonal_transformation_isometry
wenzelm@53253
  1260
    using g0 thfg thd
wenzelm@53253
  1261
    apply metis
wenzelm@53253
  1262
    done
himmelma@33175
  1263
qed
himmelma@33175
  1264
wenzelm@53854
  1265
text {* Rotation, reflection, rotoinversion. *}
himmelma@33175
  1266
himmelma@33175
  1267
definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
himmelma@33175
  1268
definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
himmelma@33175
  1269
himmelma@33175
  1270
lemma orthogonal_rotation_or_rotoinversion:
haftmann@35028
  1271
  fixes Q :: "'a::linordered_idom^'n^'n"
himmelma@33175
  1272
  shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
himmelma@33175
  1273
  by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
wenzelm@53253
  1274
wenzelm@53854
  1275
text {* Explicit formulas for low dimensions. *}
himmelma@33175
  1276
haftmann@57418
  1277
lemma setprod_neutral_const: "setprod f {(1::nat)..1} = f 1"
haftmann@57418
  1278
  by (fact setprod_singleton_nat_seg)
himmelma@33175
  1279
himmelma@33175
  1280
lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2"
haftmann@57512
  1281
  by (simp add: eval_nat_numeral setprod_numseg mult.commute)
wenzelm@53253
  1282
himmelma@33175
  1283
lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3"
haftmann@57512
  1284
  by (simp add: eval_nat_numeral setprod_numseg mult.commute)
himmelma@33175
  1285
himmelma@33175
  1286
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
huffman@44457
  1287
  by (simp add: det_def sign_id)
himmelma@33175
  1288
himmelma@33175
  1289
lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
wenzelm@53253
  1290
proof -
himmelma@33175
  1291
  have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto
himmelma@33175
  1292
  show ?thesis
wenzelm@53253
  1293
    unfolding det_def UNIV_2
wenzelm@53253
  1294
    unfolding setsum_over_permutations_insert[OF f12]
wenzelm@53253
  1295
    unfolding permutes_sing
wenzelm@53253
  1296
    by (simp add: sign_swap_id sign_id swap_id_eq)
himmelma@33175
  1297
qed
himmelma@33175
  1298
wenzelm@53253
  1299
lemma det_3:
wenzelm@53253
  1300
  "det (A::'a::comm_ring_1^3^3) =
wenzelm@53253
  1301
    A$1$1 * A$2$2 * A$3$3 +
wenzelm@53253
  1302
    A$1$2 * A$2$3 * A$3$1 +
wenzelm@53253
  1303
    A$1$3 * A$2$1 * A$3$2 -
wenzelm@53253
  1304
    A$1$1 * A$2$3 * A$3$2 -
wenzelm@53253
  1305
    A$1$2 * A$2$1 * A$3$3 -
wenzelm@53253
  1306
    A$1$3 * A$2$2 * A$3$1"
wenzelm@53253
  1307
proof -
wenzelm@53854
  1308
  have f123: "finite {2::3, 3}" "1 \<notin> {2::3, 3}"
wenzelm@53854
  1309
    by auto
wenzelm@53854
  1310
  have f23: "finite {3::3}" "2 \<notin> {3::3}"
wenzelm@53854
  1311
    by auto
himmelma@33175
  1312
himmelma@33175
  1313
  show ?thesis
wenzelm@53253
  1314
    unfolding det_def UNIV_3
wenzelm@53253
  1315
    unfolding setsum_over_permutations_insert[OF f123]
wenzelm@53253
  1316
    unfolding setsum_over_permutations_insert[OF f23]
wenzelm@53253
  1317
    unfolding permutes_sing
wenzelm@53253
  1318
    by (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
himmelma@33175
  1319
qed
himmelma@33175
  1320
himmelma@33175
  1321
end