src/HOL/Library/Determinants.thy
author nipkow
Wed Apr 01 22:29:10 2009 +0200 (2009-04-01)
changeset 30843 3419ca741dbf
parent 30837 3d4832d9f7e4
child 31280 8ef7ba78bf26
permissions -rw-r--r--
cleaned up setprod_zero-related lemmas
chaieb@29846
     1
(* Title:      Determinants
chaieb@29846
     2
   Author:     Amine Chaieb, University of Cambridge
chaieb@29846
     3
*)
chaieb@29846
     4
chaieb@29846
     5
header {* Traces, Determinant of square matrices and some properties *}
chaieb@29846
     6
chaieb@29846
     7
theory Determinants
haftmann@30661
     8
imports Euclidean_Space Permutations
chaieb@29846
     9
begin
chaieb@29846
    10
chaieb@29846
    11
subsection{* First some facts about products*}
chaieb@29846
    12
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)"
chaieb@29846
    13
apply clarsimp
chaieb@29846
    14
by(subgoal_tac "insert a A = A", auto)
chaieb@29846
    15
chaieb@29846
    16
lemma setprod_add_split:
chaieb@29846
    17
  assumes mn: "(m::nat) <= n + 1"
chaieb@29846
    18
  shows "setprod f {m.. n+p} = setprod f {m .. n} * setprod f {n+1..n+p}"
chaieb@29846
    19
proof-
chaieb@29846
    20
  let ?A = "{m .. n+p}"
chaieb@29846
    21
  let ?B = "{m .. n}"
chaieb@29846
    22
  let ?C = "{n+1..n+p}"
chaieb@29846
    23
  from mn have un: "?B \<union> ?C = ?A" by auto
chaieb@29846
    24
  from mn have dj: "?B \<inter> ?C = {}" by auto
chaieb@29846
    25
  have f: "finite ?B" "finite ?C" by simp_all
chaieb@29846
    26
  from setprod_Un_disjoint[OF f dj, of f, unfolded un] show ?thesis .
chaieb@29846
    27
qed
chaieb@29846
    28
chaieb@29846
    29
chaieb@29846
    30
lemma setprod_offset: "setprod f {(m::nat) + p .. n + p} = setprod (\<lambda>i. f (i + p)) {m..n}"
chaieb@29846
    31
apply (rule setprod_reindex_cong[where f="op + p"])
chaieb@29846
    32
apply (auto simp add: image_iff Bex_def inj_on_def)
chaieb@29846
    33
apply arith
chaieb@29846
    34
apply (rule ext)
chaieb@29846
    35
apply (simp add: add_commute)
chaieb@29846
    36
done
chaieb@29846
    37
chaieb@29846
    38
lemma setprod_singleton: "setprod f {x} = f x" by simp
chaieb@29846
    39
chaieb@29846
    40
lemma setprod_singleton_nat_seg: "setprod f {n..n} = f (n::'a::order)" by simp
chaieb@29846
    41
chaieb@29846
    42
lemma setprod_numseg: "setprod f {m..0} = (if m=0 then f 0 else 1)"
huffman@30489
    43
  "setprod f {m .. Suc n} = (if m \<le> Suc n then f (Suc n) * setprod f {m..n}
chaieb@29846
    44
                             else setprod f {m..n})"
chaieb@29846
    45
  by (auto simp add: atLeastAtMostSuc_conv)
chaieb@29846
    46
chaieb@29846
    47
lemma setprod_le: assumes fS: "finite S" and fg: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (g x :: 'a::ordered_idom)"
chaieb@29846
    48
  shows "setprod f S \<le> setprod g S"
chaieb@29846
    49
using fS fg
chaieb@29846
    50
apply(induct S)
chaieb@29846
    51
apply simp
chaieb@29846
    52
apply auto
chaieb@29846
    53
apply (rule mult_mono)
chaieb@29846
    54
apply (auto intro: setprod_nonneg)
chaieb@29846
    55
done
chaieb@29846
    56
chaieb@29846
    57
  (* FIXME: In Finite_Set there is a useless further assumption *)
chaieb@29846
    58
lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_by_zero, field})"
chaieb@29846
    59
  apply (erule finite_induct)
chaieb@29846
    60
  apply (simp)
chaieb@29846
    61
  apply simp
chaieb@29846
    62
  done
chaieb@29846
    63
chaieb@29846
    64
lemma setprod_le_1: assumes fS: "finite S" and f: "\<forall>x\<in>S. f x \<ge> 0 \<and> f x \<le> (1::'a::ordered_idom)"
chaieb@29846
    65
  shows "setprod f S \<le> 1"
chaieb@29846
    66
using setprod_le[OF fS f] unfolding setprod_1 .
chaieb@29846
    67
chaieb@29846
    68
subsection{* Trace *}
chaieb@29846
    69
chaieb@29846
    70
definition trace :: "'a::semiring_1^'n^'n \<Rightarrow> 'a" where
huffman@30582
    71
  "trace A = setsum (\<lambda>i. ((A$i)$i)) (UNIV::'n set)"
chaieb@29846
    72
chaieb@29846
    73
lemma trace_0: "trace(mat 0) = 0"
huffman@30582
    74
  by (simp add: trace_def mat_def)
chaieb@29846
    75
huffman@30582
    76
lemma trace_I: "trace(mat 1 :: 'a::semiring_1^'n^'n) = of_nat(CARD('n))"
huffman@30582
    77
  by (simp add: trace_def mat_def)
chaieb@29846
    78
chaieb@29846
    79
lemma trace_add: "trace ((A::'a::comm_semiring_1^'n^'n) + B) = trace A + trace B"
huffman@30582
    80
  by (simp add: trace_def setsum_addf)
chaieb@29846
    81
chaieb@29846
    82
lemma trace_sub: "trace ((A::'a::comm_ring_1^'n^'n) - B) = trace A - trace B"
huffman@30582
    83
  by (simp add: trace_def setsum_subtractf)
chaieb@29846
    84
chaieb@29846
    85
lemma trace_mul_sym:"trace ((A::'a::comm_semiring_1^'n^'n) ** B) = trace (B**A)"
huffman@30582
    86
  apply (simp add: trace_def matrix_matrix_mult_def)
chaieb@29846
    87
  apply (subst setsum_commute)
chaieb@29846
    88
  by (simp add: mult_commute)
chaieb@29846
    89
chaieb@29846
    90
(* ------------------------------------------------------------------------- *)
chaieb@29846
    91
(* Definition of determinant.                                                *)
chaieb@29846
    92
(* ------------------------------------------------------------------------- *)
chaieb@29846
    93
chaieb@29846
    94
definition det:: "'a::comm_ring_1^'n^'n \<Rightarrow> 'a" where
huffman@30582
    95
  "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)}"
chaieb@29846
    96
chaieb@29846
    97
(* ------------------------------------------------------------------------- *)
chaieb@29846
    98
(* A few general lemmas we need below.                                       *)
chaieb@29846
    99
(* ------------------------------------------------------------------------- *)
chaieb@29846
   100
chaieb@29846
   101
lemma setprod_permute:
huffman@30489
   102
  assumes p: "p permutes S"
chaieb@29846
   103
  shows "setprod f S = setprod (f o p) S"
chaieb@29846
   104
proof-
chaieb@29846
   105
  {assume "\<not> finite S" hence ?thesis by simp}
chaieb@29846
   106
  moreover
chaieb@29846
   107
  {assume fS: "finite S"
huffman@30489
   108
    then have ?thesis
nipkow@30837
   109
      apply (simp add: setprod_def cong del:strong_setprod_cong)
chaieb@29846
   110
      apply (rule ab_semigroup_mult.fold_image_permute)
chaieb@29846
   111
      apply (auto simp add: p)
chaieb@29846
   112
      apply unfold_locales
chaieb@29846
   113
      done}
chaieb@29846
   114
  ultimately show ?thesis by blast
chaieb@29846
   115
qed
chaieb@29846
   116
chaieb@29846
   117
lemma setproduct_permute_nat_interval: "p permutes {m::nat .. n} ==> setprod f {m..n} = setprod (f o p) {m..n}"
nipkow@30837
   118
  by (blast intro!: setprod_permute)
chaieb@29846
   119
chaieb@29846
   120
(* ------------------------------------------------------------------------- *)
chaieb@29846
   121
(* Basic determinant properties.                                             *)
chaieb@29846
   122
(* ------------------------------------------------------------------------- *)
chaieb@29846
   123
huffman@30582
   124
lemma det_transp: "det (transp A) = det (A::'a::comm_ring_1 ^'n^'n::finite)"
chaieb@29846
   125
proof-
chaieb@29846
   126
  let ?di = "\<lambda>A i j. A$i$j"
huffman@30582
   127
  let ?U = "(UNIV :: 'n set)"
huffman@30582
   128
  have fU: "finite ?U" by simp
chaieb@29846
   129
  {fix p assume p: "p \<in> {p. p permutes ?U}"
chaieb@29846
   130
    from p have pU: "p permutes ?U" by blast
huffman@30489
   131
    have sth: "sign (inv p) = sign p"
chaieb@29846
   132
      by (metis sign_inverse fU p mem_def Collect_def permutation_permutes)
huffman@30489
   133
    from permutes_inj[OF pU]
chaieb@29846
   134
    have pi: "inj_on p ?U" by (blast intro: subset_inj_on)
chaieb@29846
   135
    from permutes_image[OF pU]
chaieb@29846
   136
    have "setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U = setprod (\<lambda>i. ?di (transp A) i (inv p i)) (p ` ?U)" by simp
chaieb@29846
   137
    also have "\<dots> = setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U"
chaieb@29846
   138
      unfolding setprod_reindex[OF pi] ..
chaieb@29846
   139
    also have "\<dots> = setprod (\<lambda>i. ?di A i (p i)) ?U"
chaieb@29846
   140
    proof-
chaieb@29846
   141
      {fix i assume i: "i \<in> ?U"
chaieb@29846
   142
	from i permutes_inv_o[OF pU] permutes_in_image[OF pU]
chaieb@29846
   143
	have "((\<lambda>i. ?di (transp A) i (inv p i)) o p) i = ?di A i (p i)"
huffman@30582
   144
	  unfolding transp_def by (simp add: expand_fun_eq)}
huffman@30489
   145
      then show "setprod ((\<lambda>i. ?di (transp A) i (inv p i)) o p) ?U = setprod (\<lambda>i. ?di A i (p i)) ?U" by (auto intro: setprod_cong)
chaieb@29846
   146
    qed
chaieb@29846
   147
    finally have "of_int (sign (inv p)) * (setprod (\<lambda>i. ?di (transp A) i (inv p i)) ?U) = of_int (sign p) * (setprod (\<lambda>i. ?di A i (p i)) ?U)" using sth
chaieb@29846
   148
      by simp}
chaieb@29846
   149
  then show ?thesis unfolding det_def apply (subst setsum_permutations_inverse)
chaieb@29846
   150
  apply (rule setsum_cong2) by blast
chaieb@29846
   151
qed
chaieb@29846
   152
huffman@30489
   153
lemma det_lowerdiagonal:
huffman@30582
   154
  fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}"
huffman@30582
   155
  assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"
huffman@30582
   156
  shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
chaieb@29846
   157
proof-
huffman@30582
   158
  let ?U = "UNIV:: 'n set"
chaieb@29846
   159
  let ?PU = "{p. p permutes ?U}"
huffman@30582
   160
  let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
huffman@30582
   161
  have fU: "finite ?U" by simp
chaieb@29846
   162
  from finite_permutations[OF fU] have fPU: "finite ?PU" .
chaieb@29846
   163
  have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
chaieb@29846
   164
  {fix p assume p: "p \<in> ?PU -{id}"
chaieb@29846
   165
    from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+
chaieb@29846
   166
    from permutes_natset_le[OF pU] pid obtain i where
huffman@30582
   167
      i: "p i > i" by (metis not_le)
huffman@30582
   168
    from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast
chaieb@29846
   169
    from setprod_zero[OF fU ex] have "?pp p = 0" by simp}
chaieb@29846
   170
  then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"  by blast
chaieb@30259
   171
  from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis
chaieb@29846
   172
    unfolding det_def by (simp add: sign_id)
chaieb@29846
   173
qed
chaieb@29846
   174
huffman@30489
   175
lemma det_upperdiagonal:
huffman@30582
   176
  fixes A :: "'a::comm_ring_1^'n^'n::{finite,wellorder}"
huffman@30582
   177
  assumes ld: "\<And>i j. i > j \<Longrightarrow> A$i$j = 0"
huffman@30582
   178
  shows "det A = setprod (\<lambda>i. A$i$i) (UNIV:: 'n set)"
chaieb@29846
   179
proof-
huffman@30582
   180
  let ?U = "UNIV:: 'n set"
chaieb@29846
   181
  let ?PU = "{p. p permutes ?U}"
huffman@30582
   182
  let ?pp = "(\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
huffman@30582
   183
  have fU: "finite ?U" by simp
chaieb@29846
   184
  from finite_permutations[OF fU] have fPU: "finite ?PU" .
chaieb@29846
   185
  have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
chaieb@29846
   186
  {fix p assume p: "p \<in> ?PU -{id}"
chaieb@29846
   187
    from p have pU: "p permutes ?U" and pid: "p \<noteq> id" by blast+
chaieb@29846
   188
    from permutes_natset_ge[OF pU] pid obtain i where
huffman@30582
   189
      i: "p i < i" by (metis not_le)
huffman@30582
   190
    from ld[OF i] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast
chaieb@29846
   191
    from setprod_zero[OF fU ex] have "?pp p = 0" by simp}
chaieb@29846
   192
  then have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"  by blast
chaieb@30259
   193
  from   setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis
chaieb@29846
   194
    unfolding det_def by (simp add: sign_id)
chaieb@29846
   195
qed
chaieb@29846
   196
huffman@30598
   197
lemma det_diagonal:
huffman@30598
   198
  fixes A :: "'a::comm_ring_1^'n^'n::finite"
huffman@30598
   199
  assumes ld: "\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0"
huffman@30598
   200
  shows "det A = setprod (\<lambda>i. A$i$i) (UNIV::'n set)"
huffman@30598
   201
proof-
huffman@30598
   202
  let ?U = "UNIV:: 'n set"
huffman@30598
   203
  let ?PU = "{p. p permutes ?U}"
huffman@30598
   204
  let ?pp = "\<lambda>p. of_int (sign p) * setprod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
huffman@30598
   205
  have fU: "finite ?U" by simp
huffman@30598
   206
  from finite_permutations[OF fU] have fPU: "finite ?PU" .
huffman@30598
   207
  have id0: "{id} \<subseteq> ?PU" by (auto simp add: permutes_id)
huffman@30598
   208
  {fix p assume p: "p \<in> ?PU - {id}"
huffman@30598
   209
    then have "p \<noteq> id" by simp
huffman@30598
   210
    then obtain i where i: "p i \<noteq> i" unfolding expand_fun_eq by auto
huffman@30598
   211
    from ld [OF i [symmetric]] have ex:"\<exists>i \<in> ?U. A$i$p i = 0" by blast
huffman@30598
   212
    from setprod_zero [OF fU ex] have "?pp p = 0" by simp}
huffman@30598
   213
  then have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"  by blast
huffman@30598
   214
  from setsum_mono_zero_cong_left[OF fPU id0 p0] show ?thesis
huffman@30598
   215
    unfolding det_def by (simp add: sign_id)
huffman@30598
   216
qed
huffman@30598
   217
huffman@30598
   218
lemma det_I: "det (mat 1 :: 'a::comm_ring_1^'n^'n::finite) = 1"
chaieb@29846
   219
proof-
chaieb@29846
   220
  let ?A = "mat 1 :: 'a::comm_ring_1^'n^'n"
huffman@30582
   221
  let ?U = "UNIV :: 'n set"
chaieb@29846
   222
  let ?f = "\<lambda>i j. ?A$i$j"
chaieb@29846
   223
  {fix i assume i: "i \<in> ?U"
chaieb@29846
   224
    have "?f i i = 1" using i by (vector mat_def)}
chaieb@29846
   225
  hence th: "setprod (\<lambda>i. ?f i i) ?U = setprod (\<lambda>x. 1) ?U"
chaieb@29846
   226
    by (auto intro: setprod_cong)
huffman@30598
   227
  {fix i j assume i: "i \<in> ?U" and j: "j \<in> ?U" and ij: "i \<noteq> j"
chaieb@29846
   228
    have "?f i j = 0" using i j ij by (vector mat_def) }
huffman@30598
   229
  then have "det ?A = setprod (\<lambda>i. ?f i i) ?U" using det_diagonal
chaieb@29846
   230
    by blast
chaieb@29846
   231
  also have "\<dots> = 1" unfolding th setprod_1 ..
huffman@30489
   232
  finally show ?thesis .
chaieb@29846
   233
qed
chaieb@29846
   234
huffman@30582
   235
lemma det_0: "det (mat 0 :: 'a::comm_ring_1^'n^'n::finite) = 0"
huffman@30582
   236
  by (simp add: det_def setprod_zero)
chaieb@29846
   237
chaieb@29846
   238
lemma det_permute_rows:
huffman@30582
   239
  fixes A :: "'a::comm_ring_1^'n^'n::finite"
huffman@30582
   240
  assumes p: "p permutes (UNIV :: 'n::finite set)"
chaieb@29846
   241
  shows "det(\<chi> i. A$p i :: 'a^'n^'n) = of_int (sign p) * det A"
huffman@30582
   242
  apply (simp add: det_def setsum_right_distrib mult_assoc[symmetric])
huffman@30489
   243
  apply (subst sum_permutations_compose_right[OF p])
chaieb@29846
   244
proof(rule setsum_cong2)
huffman@30582
   245
  let ?U = "UNIV :: 'n set"
chaieb@29846
   246
  let ?PU = "{p. p permutes ?U}"
chaieb@29846
   247
  fix q assume qPU: "q \<in> ?PU"
huffman@30582
   248
  have fU: "finite ?U" by simp
chaieb@29846
   249
  from qPU have q: "q permutes ?U" by blast
chaieb@29846
   250
  from p q have pp: "permutation p" and qp: "permutation q"
chaieb@29846
   251
    by (metis fU permutation_permutes)+
chaieb@29846
   252
  from permutes_inv[OF p] have ip: "inv p permutes ?U" .
huffman@30582
   253
    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"
chaieb@29846
   254
      by (simp only: setprod_permute[OF ip, symmetric])
chaieb@29846
   255
    also have "\<dots> = setprod (\<lambda>i. A $ (p o inv p) i $ (q o (p o inv p)) i) ?U"
chaieb@29846
   256
      by (simp only: o_def)
chaieb@29846
   257
    also have "\<dots> = setprod (\<lambda>i. A$i$q i) ?U" by (simp only: o_def permutes_inverses[OF p])
huffman@30582
   258
    finally   have thp: "setprod (\<lambda>i. A$p i$ (q o p) i) ?U = setprod (\<lambda>i. A$i$q i) ?U"
chaieb@29846
   259
      by blast
huffman@30582
   260
  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"
chaieb@29846
   261
    by (simp only: thp sign_compose[OF qp pp] mult_commute of_int_mult)
chaieb@29846
   262
qed
chaieb@29846
   263
chaieb@29846
   264
lemma det_permute_columns:
huffman@30582
   265
  fixes A :: "'a::comm_ring_1^'n^'n::finite"
huffman@30582
   266
  assumes p: "p permutes (UNIV :: 'n set)"
chaieb@29846
   267
  shows "det(\<chi> i j. A$i$ p j :: 'a^'n^'n) = of_int (sign p) * det A"
chaieb@29846
   268
proof-
chaieb@29846
   269
  let ?Ap = "\<chi> i j. A$i$ p j :: 'a^'n^'n"
chaieb@29846
   270
  let ?At = "transp A"
chaieb@29846
   271
  have "of_int (sign p) * det A = det (transp (\<chi> i. transp A $ p i))"
chaieb@29846
   272
    unfolding det_permute_rows[OF p, of ?At] det_transp ..
chaieb@29846
   273
  moreover
chaieb@29846
   274
  have "?Ap = transp (\<chi> i. transp A $ p i)"
huffman@30582
   275
    by (simp add: transp_def Cart_eq)
huffman@30489
   276
  ultimately show ?thesis by simp
chaieb@29846
   277
qed
chaieb@29846
   278
chaieb@29846
   279
lemma det_identical_rows:
huffman@30582
   280
  fixes A :: "'a::ordered_idom^'n^'n::finite"
huffman@30582
   281
  assumes ij: "i \<noteq> j"
chaieb@29846
   282
  and r: "row i A = row j A"
chaieb@29846
   283
  shows	"det A = 0"
chaieb@29846
   284
proof-
huffman@30489
   285
  have tha: "\<And>(a::'a) b. a = b ==> b = - a ==> a = 0"
chaieb@29846
   286
    by simp
chaieb@29846
   287
  have th1: "of_int (-1) = - 1" by (metis of_int_1 of_int_minus number_of_Min)
chaieb@29846
   288
  let ?p = "Fun.swap i j id"
chaieb@29846
   289
  let ?A = "\<chi> i. A $ ?p i"
huffman@30582
   290
  from r have "A = ?A" by (simp add: Cart_eq row_def swap_def)
chaieb@29846
   291
  hence "det A = det ?A" by simp
chaieb@29846
   292
  moreover have "det A = - det ?A"
huffman@30582
   293
    by (simp add: det_permute_rows[OF permutes_swap_id] sign_swap_id ij th1)
huffman@30489
   294
  ultimately show "det A = 0" by (metis tha)
chaieb@29846
   295
qed
chaieb@29846
   296
chaieb@29846
   297
lemma det_identical_columns:
huffman@30582
   298
  fixes A :: "'a::ordered_idom^'n^'n::finite"
huffman@30582
   299
  assumes ij: "i \<noteq> j"
chaieb@29846
   300
  and r: "column i A = column j A"
chaieb@29846
   301
  shows	"det A = 0"
chaieb@29846
   302
apply (subst det_transp[symmetric])
huffman@30582
   303
apply (rule det_identical_rows[OF ij])
huffman@30582
   304
by (metis row_transp r)
chaieb@29846
   305
huffman@30489
   306
lemma det_zero_row:
huffman@30582
   307
  fixes A :: "'a::{idom, ring_char_0}^'n^'n::finite"
huffman@30582
   308
  assumes r: "row i A = 0"
chaieb@29846
   309
  shows "det A = 0"
huffman@30582
   310
using r
huffman@30582
   311
apply (simp add: row_def det_def Cart_eq)
chaieb@29846
   312
apply (rule setsum_0')
nipkow@30843
   313
apply (auto simp: sign_nz)
chaieb@29846
   314
done
chaieb@29846
   315
chaieb@29846
   316
lemma det_zero_column:
huffman@30582
   317
  fixes A :: "'a::{idom,ring_char_0}^'n^'n::finite"
huffman@30582
   318
  assumes r: "column i A = 0"
chaieb@29846
   319
  shows "det A = 0"
chaieb@29846
   320
  apply (subst det_transp[symmetric])
huffman@30582
   321
  apply (rule det_zero_row [of i])
huffman@30582
   322
  by (metis row_transp r)
chaieb@29846
   323
chaieb@29846
   324
lemma det_row_add:
huffman@30582
   325
  fixes a b c :: "'n::finite \<Rightarrow> _ ^ 'n"
chaieb@29846
   326
  shows "det((\<chi> i. if i = k then a i + b i else c i)::'a::comm_ring_1^'n^'n) =
chaieb@29846
   327
             det((\<chi> i. if i = k then a i else c i)::'a::comm_ring_1^'n^'n) +
chaieb@29846
   328
             det((\<chi> i. if i = k then b i else c i)::'a::comm_ring_1^'n^'n)"
huffman@30582
   329
unfolding det_def Cart_lambda_beta setsum_addf[symmetric]
chaieb@29846
   330
proof (rule setsum_cong2)
huffman@30582
   331
  let ?U = "UNIV :: 'n set"
chaieb@29846
   332
  let ?pU = "{p. p permutes ?U}"
huffman@30582
   333
  let ?f = "(\<lambda>i. if i = k then a i + b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
huffman@30582
   334
  let ?g = "(\<lambda> i. if i = k then a i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
huffman@30582
   335
  let ?h = "(\<lambda> i. if i = k then b i else c i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
chaieb@29846
   336
  fix p assume p: "p \<in> ?pU"
chaieb@29846
   337
  let ?Uk = "?U - {k}"
chaieb@29846
   338
  from p have pU: "p permutes ?U" by blast
huffman@30582
   339
  have kU: "?U = insert k ?Uk" by blast
chaieb@29846
   340
  {fix j assume j: "j \<in> ?Uk"
huffman@30489
   341
    from j have "?f j $ p j = ?g j $ p j" and "?f j $ p j= ?h j $ p j"
chaieb@29846
   342
      by simp_all}
chaieb@29846
   343
  then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"
chaieb@29846
   344
    and th2: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?h i $ p i) ?Uk"
chaieb@29846
   345
    apply -
chaieb@29846
   346
    apply (rule setprod_cong, simp_all)+
chaieb@29846
   347
    done
huffman@30582
   348
  have th3: "finite ?Uk" "k \<notin> ?Uk" by auto
chaieb@29846
   349
  have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
chaieb@29846
   350
    unfolding kU[symmetric] ..
chaieb@29846
   351
  also have "\<dots> = ?f k $ p k  * setprod (\<lambda>i. ?f i $ p i) ?Uk"
chaieb@29846
   352
    apply (rule setprod_insert)
chaieb@29846
   353
    apply simp
huffman@30582
   354
    by blast
huffman@30582
   355
  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: ring_simps)
chaieb@29846
   356
  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)
chaieb@29846
   357
  also have "\<dots> = setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk) + setprod (\<lambda>i. ?h i $ p i) (insert k ?Uk)"
chaieb@29846
   358
    unfolding  setprod_insert[OF th3] by simp
chaieb@29846
   359
  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] .
chaieb@29846
   360
  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"
chaieb@29846
   361
    by (simp add: ring_simps)
chaieb@29846
   362
qed
chaieb@29846
   363
chaieb@29846
   364
lemma det_row_mul:
huffman@30582
   365
  fixes a b :: "'n::finite \<Rightarrow> _ ^ 'n"
chaieb@29846
   366
  shows "det((\<chi> i. if i = k then c *s a i else b i)::'a::comm_ring_1^'n^'n) =
chaieb@29846
   367
             c* det((\<chi> i. if i = k then a i else b i)::'a::comm_ring_1^'n^'n)"
chaieb@29846
   368
huffman@30582
   369
unfolding det_def Cart_lambda_beta setsum_right_distrib
chaieb@29846
   370
proof (rule setsum_cong2)
huffman@30582
   371
  let ?U = "UNIV :: 'n set"
chaieb@29846
   372
  let ?pU = "{p. p permutes ?U}"
huffman@30582
   373
  let ?f = "(\<lambda>i. if i = k then c*s a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
huffman@30582
   374
  let ?g = "(\<lambda> i. if i = k then a i else b i)::'n \<Rightarrow> 'a::comm_ring_1^'n"
chaieb@29846
   375
  fix p assume p: "p \<in> ?pU"
chaieb@29846
   376
  let ?Uk = "?U - {k}"
chaieb@29846
   377
  from p have pU: "p permutes ?U" by blast
huffman@30582
   378
  have kU: "?U = insert k ?Uk" by blast
chaieb@29846
   379
  {fix j assume j: "j \<in> ?Uk"
chaieb@29846
   380
    from j have "?f j $ p j = ?g j $ p j" by simp}
chaieb@29846
   381
  then have th1: "setprod (\<lambda>i. ?f i $ p i) ?Uk = setprod (\<lambda>i. ?g i $ p i) ?Uk"
chaieb@29846
   382
    apply -
chaieb@29846
   383
    apply (rule setprod_cong, simp_all)
chaieb@29846
   384
    done
huffman@30582
   385
  have th3: "finite ?Uk" "k \<notin> ?Uk" by auto
chaieb@29846
   386
  have "setprod (\<lambda>i. ?f i $ p i) ?U = setprod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
chaieb@29846
   387
    unfolding kU[symmetric] ..
chaieb@29846
   388
  also have "\<dots> = ?f k $ p k  * setprod (\<lambda>i. ?f i $ p i) ?Uk"
chaieb@29846
   389
    apply (rule setprod_insert)
chaieb@29846
   390
    apply simp
huffman@30582
   391
    by blast
huffman@30582
   392
  also have "\<dots> = (c*s a k) $ p k * setprod (\<lambda>i. ?f i $ p i) ?Uk" by (simp add: ring_simps)
chaieb@29846
   393
  also have "\<dots> = c* (a k $ p k * setprod (\<lambda>i. ?g i $ p i) ?Uk)"
huffman@30582
   394
    unfolding th1 by (simp add: mult_ac)
chaieb@29846
   395
  also have "\<dots> = c* (setprod (\<lambda>i. ?g i $ p i) (insert k ?Uk))"
chaieb@29846
   396
    unfolding  setprod_insert[OF th3] by simp
chaieb@29846
   397
  finally have "setprod (\<lambda>i. ?f i $ p i) ?U = c* (setprod (\<lambda>i. ?g i $ p i) ?U)" unfolding kU[symmetric] .
chaieb@29846
   398
  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)"
chaieb@29846
   399
    by (simp add: ring_simps)
chaieb@29846
   400
qed
chaieb@29846
   401
chaieb@29846
   402
lemma det_row_0:
huffman@30582
   403
  fixes b :: "'n::finite \<Rightarrow> _ ^ 'n"
chaieb@29846
   404
  shows "det((\<chi> i. if i = k then 0 else b i)::'a::comm_ring_1^'n^'n) = 0"
huffman@30582
   405
using det_row_mul[of k 0 "\<lambda>i. 1" b]
chaieb@29846
   406
apply (simp)
chaieb@29846
   407
  unfolding vector_smult_lzero .
chaieb@29846
   408
chaieb@29846
   409
lemma det_row_operation:
huffman@30582
   410
  fixes A :: "'a::ordered_idom^'n^'n::finite"
huffman@30582
   411
  assumes ij: "i \<noteq> j"
chaieb@29846
   412
  shows "det (\<chi> k. if k = i then row i A + c *s row j A else row k A) = det A"
chaieb@29846
   413
proof-
chaieb@29846
   414
  let ?Z = "(\<chi> k. if k = i then row j A else row k A) :: 'a ^'n^'n"
huffman@30582
   415
  have th: "row i ?Z = row j ?Z" by (vector row_def)
chaieb@29846
   416
  have th2: "((\<chi> k. if k = i then row i A else row k A) :: 'a^'n^'n) = A"
huffman@30582
   417
    by (vector row_def)
chaieb@29846
   418
  show ?thesis
huffman@30582
   419
    unfolding det_row_add [of i] det_row_mul[of i] det_identical_rows[OF ij th] th2
chaieb@29846
   420
    by simp
chaieb@29846
   421
qed
chaieb@29846
   422
chaieb@29846
   423
lemma det_row_span:
huffman@30582
   424
  fixes A :: "'a:: ordered_idom^'n^'n::finite"
huffman@30582
   425
  assumes x: "x \<in> span {row j A |j. j \<noteq> i}"
chaieb@29846
   426
  shows "det (\<chi> k. if k = i then row i A + x else row k A) = det A"
chaieb@29846
   427
proof-
huffman@30582
   428
  let ?U = "UNIV :: 'n set"
huffman@30582
   429
  let ?S = "{row j A |j. j \<noteq> i}"
chaieb@29846
   430
  let ?d = "\<lambda>x. det (\<chi> k. if k = i then x else row k A)"
chaieb@29846
   431
  let ?P = "\<lambda>x. ?d (row i A + x) = det A"
huffman@30489
   432
  {fix k
huffman@30489
   433
chaieb@29846
   434
    have "(if k = i then row i A + 0 else row k A) = row k A" by simp}
chaieb@29846
   435
  then have P0: "?P 0"
chaieb@29846
   436
    apply -
chaieb@29846
   437
    apply (rule cong[of det, OF refl])
huffman@30582
   438
    by (vector row_def)
chaieb@29846
   439
  moreover
chaieb@29846
   440
  {fix c z y assume zS: "z \<in> ?S" and Py: "?P y"
huffman@30582
   441
    from zS obtain j where j: "z = row j A" "i \<noteq> j" by blast
chaieb@29846
   442
    let ?w = "row i A + y"
chaieb@29846
   443
    have th0: "row i A + (c*s z + y) = ?w + c*s z" by vector
chaieb@29846
   444
    have thz: "?d z = 0"
huffman@30582
   445
      apply (rule det_identical_rows[OF j(2)])
huffman@30582
   446
      using j by (vector row_def)
chaieb@29846
   447
    have "?d (row i A + (c*s z + y)) = ?d (?w + c*s z)" unfolding th0 ..
huffman@30582
   448
    then have "?P (c*s z + y)" unfolding thz Py det_row_mul[of i] det_row_add[of i]
chaieb@29846
   449
      by simp }
chaieb@29846
   450
huffman@30489
   451
  ultimately show ?thesis
chaieb@29846
   452
    apply -
chaieb@29846
   453
    apply (rule span_induct_alt[of ?P ?S, OF P0])
chaieb@29846
   454
    apply blast
chaieb@29846
   455
    apply (rule x)
chaieb@29846
   456
    done
chaieb@29846
   457
qed
chaieb@29846
   458
chaieb@29846
   459
(* ------------------------------------------------------------------------- *)
chaieb@29846
   460
(* May as well do this, though it's a bit unsatisfactory since it ignores    *)
chaieb@29846
   461
(* exact duplicates by considering the rows/columns as a set.                *)
chaieb@29846
   462
(* ------------------------------------------------------------------------- *)
chaieb@29846
   463
chaieb@29846
   464
lemma det_dependent_rows:
huffman@30582
   465
  fixes A:: "'a::ordered_idom^'n^'n::finite"
chaieb@29846
   466
  assumes d: "dependent (rows A)"
chaieb@29846
   467
  shows "det A = 0"
chaieb@29846
   468
proof-
huffman@30582
   469
  let ?U = "UNIV :: 'n set"
huffman@30582
   470
  from d obtain i where i: "row i A \<in> span (rows A - {row i A})"
chaieb@29846
   471
    unfolding dependent_def rows_def by blast
huffman@30582
   472
  {fix j k assume jk: "j \<noteq> k"
huffman@30489
   473
    and c: "row j A = row k A"
huffman@30582
   474
    from det_identical_rows[OF jk c] have ?thesis .}
chaieb@29846
   475
  moreover
huffman@30582
   476
  {assume H: "\<And> i j. i \<noteq> j \<Longrightarrow> row i A \<noteq> row j A"
huffman@30582
   477
    have th0: "- row i A \<in> span {row j A|j. j \<noteq> i}"
chaieb@29846
   478
      apply (rule span_neg)
chaieb@29846
   479
      apply (rule set_rev_mp)
huffman@30582
   480
      apply (rule i)
chaieb@29846
   481
      apply (rule span_mono)
chaieb@29846
   482
      using H i by (auto simp add: rows_def)
huffman@30582
   483
    from det_row_span[OF th0]
chaieb@29846
   484
    have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)"
chaieb@29846
   485
      unfolding right_minus vector_smult_lzero ..
huffman@30582
   486
    with det_row_mul[of i "0::'a" "\<lambda>i. 1"]
chaieb@29846
   487
    have "det A = 0" by simp}
chaieb@29846
   488
  ultimately show ?thesis by blast
chaieb@29846
   489
qed
chaieb@29846
   490
huffman@30582
   491
lemma det_dependent_columns: assumes d: "dependent(columns (A::'a::ordered_idom^'n^'n::finite))" shows "det A = 0"
chaieb@29846
   492
by (metis d det_dependent_rows rows_transp det_transp)
chaieb@29846
   493
chaieb@29846
   494
(* ------------------------------------------------------------------------- *)
chaieb@29846
   495
(* Multilinearity and the multiplication formula.                            *)
chaieb@29846
   496
(* ------------------------------------------------------------------------- *)
chaieb@29846
   497
huffman@30582
   498
lemma Cart_lambda_cong: "(\<And>x. f x = g x) \<Longrightarrow> (Cart_lambda f::'a^'n) = (Cart_lambda g :: 'a^'n)"
chaieb@29846
   499
  apply (rule iffD1[OF Cart_lambda_unique]) by vector
chaieb@29846
   500
huffman@30489
   501
lemma det_linear_row_setsum:
huffman@30582
   502
  assumes fS: "finite S"
huffman@30582
   503
  shows "det ((\<chi> i. if i = k then setsum (a i) S else c i)::'a::comm_ring_1^'n^'n::finite) = setsum (\<lambda>j. det ((\<chi> i. if i = k then a  i j else c i)::'a^'n^'n)) S"
chaieb@29846
   504
proof(induct rule: finite_induct[OF fS])
huffman@30582
   505
  case 1 thus ?case apply simp  unfolding setsum_empty det_row_0[of k] ..
chaieb@29846
   506
next
chaieb@29846
   507
  case (2 x F)
chaieb@29846
   508
  then  show ?case by (simp add: det_row_add cong del: if_weak_cong)
chaieb@29846
   509
qed
chaieb@29846
   510
chaieb@29846
   511
lemma finite_bounded_functions:
chaieb@29846
   512
  assumes fS: "finite S"
chaieb@29846
   513
  shows "finite {f. (\<forall>i \<in> {1.. (k::nat)}. f i \<in> S) \<and> (\<forall>i. i \<notin> {1 .. k} \<longrightarrow> f i = i)}"
chaieb@29846
   514
proof(induct k)
huffman@30489
   515
  case 0
chaieb@29846
   516
  have th: "{f. \<forall>i. f i = i} = {id}" by (auto intro: ext)
chaieb@29846
   517
  show ?case by (auto simp add: th)
chaieb@29846
   518
next
chaieb@29846
   519
  case (Suc k)
chaieb@29846
   520
  let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i"
chaieb@29846
   521
  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)})"
chaieb@29846
   522
  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)}"
chaieb@29846
   523
    apply (auto simp add: image_iff)
chaieb@29846
   524
    apply (rule_tac x="x (Suc k)" in bexI)
chaieb@29846
   525
    apply (rule_tac x = "\<lambda>i. if i = Suc k then i else x i" in exI)
chaieb@29846
   526
    apply (auto intro: ext)
chaieb@29846
   527
    done
chaieb@29846
   528
  with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]
huffman@30489
   529
  show ?case by metis
chaieb@29846
   530
qed
chaieb@29846
   531
chaieb@29846
   532
chaieb@29846
   533
lemma eq_id_iff[simp]: "(\<forall>x. f x = x) = (f = id)" by (auto intro: ext)
chaieb@29846
   534
chaieb@29846
   535
lemma det_linear_rows_setsum_lemma:
huffman@30582
   536
  assumes fS: "finite S" and fT: "finite T"
huffman@30582
   537
  shows "det((\<chi> i. if i \<in> T then setsum (a i) S else c i):: 'a::comm_ring_1^'n^'n::finite) =
huffman@30582
   538
             setsum (\<lambda>f. det((\<chi> i. if i \<in> T then a i (f i) else c i)::'a^'n^'n))
huffman@30582
   539
                 {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
huffman@30582
   540
using fT
huffman@30582
   541
proof(induct T arbitrary: a c set: finite)
huffman@30582
   542
  case empty
huffman@30582
   543
  have th0: "\<And>x y. (\<chi> i. if i \<in> {} then x i else y i) = (\<chi> i. y i)" by vector
huffman@30582
   544
  from "empty.prems"  show ?case unfolding th0 by simp
chaieb@29846
   545
next
huffman@30582
   546
  case (insert z T a c)
huffman@30582
   547
  let ?F = "\<lambda>T. {f. (\<forall>i \<in> T. f i \<in> S) \<and> (\<forall>i. i \<notin> T \<longrightarrow> f i = i)}"
huffman@30582
   548
  let ?h = "\<lambda>(y,g) i. if i = z then y else g i"
huffman@30582
   549
  let ?k = "\<lambda>h. (h(z),(\<lambda>i. if i = z then i else h i))"
huffman@30582
   550
  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)"
huffman@30582
   551
  let ?c = "\<lambda>i. if i = z then a i j else c i"
huffman@30582
   552
  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
chaieb@29846
   553
  have thif2: "\<And>a b c d e. (if a then b else if c then d else e) =
huffman@30489
   554
     (if c then (if a then b else d) else (if a then b else e))" by simp
huffman@30582
   555
  from `z \<notin> T` have nz: "\<And>i. i \<in> T \<Longrightarrow> i = z \<longleftrightarrow> False" by auto
huffman@30582
   556
  have "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) =
huffman@30582
   557
        det (\<chi> i. if i = z then setsum (a i) S
huffman@30582
   558
                 else if i \<in> T then setsum (a i) S else c i)"
huffman@30582
   559
    unfolding insert_iff thif ..
huffman@30582
   560
  also have "\<dots> = (\<Sum>j\<in>S. det (\<chi> i. if i \<in> T then setsum (a i) S
huffman@30582
   561
                    else if i = z then a i j else c i))"
huffman@30582
   562
    unfolding det_linear_row_setsum[OF fS]
chaieb@29846
   563
    apply (subst thif2)
huffman@30582
   564
    using nz by (simp cong del: if_weak_cong cong add: if_cong)
huffman@30489
   565
  finally have tha:
huffman@30582
   566
    "det (\<chi> i. if i \<in> insert z T then setsum (a i) S else c i) =
huffman@30582
   567
     (\<Sum>(j, f)\<in>S \<times> ?F T. det (\<chi> i. if i \<in> T then a i (f i)
huffman@30582
   568
                                else if i = z then a i j
huffman@30489
   569
                                else c i))"
huffman@30582
   570
    unfolding  insert.hyps unfolding setsum_cartesian_product by blast
chaieb@29846
   571
  show ?case unfolding tha
huffman@30489
   572
    apply(rule setsum_eq_general_reverses[where h= "?h" and k= "?k"],
huffman@30582
   573
      blast intro: finite_cartesian_product fS finite,
huffman@30582
   574
      blast intro: finite_cartesian_product fS finite)
huffman@30582
   575
    using `z \<notin> T`
huffman@30582
   576
    apply (auto intro: ext)
chaieb@29846
   577
    apply (rule cong[OF refl[of det]])
chaieb@29846
   578
    by vector
chaieb@29846
   579
qed
chaieb@29846
   580
chaieb@29846
   581
lemma det_linear_rows_setsum:
huffman@30582
   582
  assumes fS: "finite (S::'n::finite set)"
huffman@30582
   583
  shows "det (\<chi> i. setsum (a i) S) = setsum (\<lambda>f. det (\<chi> i. a i (f i) :: 'a::comm_ring_1 ^ 'n^'n::finite)) {f. \<forall>i. f i \<in> S}"
chaieb@29846
   584
proof-
huffman@30582
   585
  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
huffman@30489
   586
huffman@30582
   587
  from det_linear_rows_setsum_lemma[OF fS, of "UNIV :: 'n set" a, unfolded th0, OF finite] show ?thesis by simp
chaieb@29846
   588
qed
chaieb@29846
   589
chaieb@29846
   590
lemma matrix_mul_setsum_alt:
huffman@30582
   591
  fixes A B :: "'a::comm_ring_1^'n^'n::finite"
huffman@30582
   592
  shows "A ** B = (\<chi> i. setsum (\<lambda>k. A$i$k *s B $ k) (UNIV :: 'n set))"
chaieb@29846
   593
  by (vector matrix_matrix_mult_def setsum_component)
chaieb@29846
   594
chaieb@29846
   595
lemma det_rows_mul:
huffman@30582
   596
  "det((\<chi> i. c i *s a i)::'a::comm_ring_1^'n^'n::finite) =
huffman@30582
   597
  setprod (\<lambda>i. c i) (UNIV:: 'n set) * det((\<chi> i. a i)::'a^'n^'n)"
huffman@30582
   598
proof (simp add: det_def setsum_right_distrib cong add: setprod_cong, rule setsum_cong2)
huffman@30582
   599
  let ?U = "UNIV :: 'n set"
chaieb@29846
   600
  let ?PU = "{p. p permutes ?U}"
chaieb@29846
   601
  fix p assume pU: "p \<in> ?PU"
chaieb@29846
   602
  let ?s = "of_int (sign p)"
chaieb@29846
   603
  from pU have p: "p permutes ?U" by blast
huffman@30582
   604
  have "setprod (\<lambda>i. c i * a i $ p i) ?U = setprod c ?U * setprod (\<lambda>i. a i $ p i) ?U"
chaieb@29846
   605
    unfolding setprod_timesf ..
huffman@30582
   606
  then show "?s * (\<Prod>xa\<in>?U. c xa * a xa $ p xa) =
chaieb@29846
   607
        setprod c ?U * (?s* (\<Prod>xa\<in>?U. a xa $ p xa))" by (simp add: ring_simps)
chaieb@29846
   608
qed
chaieb@29846
   609
chaieb@29846
   610
lemma det_mul:
huffman@30582
   611
  fixes A B :: "'a::ordered_idom^'n^'n::finite"
chaieb@29846
   612
  shows "det (A ** B) = det A * det B"
chaieb@29846
   613
proof-
huffman@30582
   614
  let ?U = "UNIV :: 'n set"
chaieb@29846
   615
  let ?F = "{f. (\<forall>i\<in> ?U. f i \<in> ?U) \<and> (\<forall>i. i \<notin> ?U \<longrightarrow> f i = i)}"
chaieb@29846
   616
  let ?PU = "{p. p permutes ?U}"
chaieb@29846
   617
  have fU: "finite ?U" by simp
huffman@30582
   618
  have fF: "finite ?F" by (rule finite)
chaieb@29846
   619
  {fix p assume p: "p permutes ?U"
huffman@30489
   620
chaieb@29846
   621
    have "p \<in> ?F" unfolding mem_Collect_eq permutes_in_image[OF p]
chaieb@29846
   622
      using p[unfolded permutes_def] by simp}
huffman@30489
   623
  then have PUF: "?PU \<subseteq> ?F"  by blast
chaieb@29846
   624
  {fix f assume fPU: "f \<in> ?F - ?PU"
chaieb@29846
   625
    have fUU: "f ` ?U \<subseteq> ?U" using fPU by auto
chaieb@29846
   626
    from fPU have f: "\<forall>i \<in> ?U. f i \<in> ?U"
huffman@30489
   627
      "\<forall>i. i \<notin> ?U \<longrightarrow> f i = i" "\<not>(\<forall>y. \<exists>!x. f x = y)" unfolding permutes_def
chaieb@29846
   628
      by auto
huffman@30489
   629
chaieb@29846
   630
    let ?A = "(\<chi> i. A$i$f i *s B$f i) :: 'a^'n^'n"
chaieb@29846
   631
    let ?B = "(\<chi> i. B$f i) :: 'a^'n^'n"
chaieb@29846
   632
    {assume fni: "\<not> inj_on f ?U"
huffman@30582
   633
      then obtain i j where ij: "f i = f j" "i \<noteq> j"
chaieb@29846
   634
	unfolding inj_on_def by blast
huffman@30489
   635
      from ij
chaieb@29846
   636
      have rth: "row i ?B = row j ?B" by (vector row_def)
huffman@30582
   637
      from det_identical_rows[OF ij(2) rth]
huffman@30489
   638
      have "det (\<chi> i. A$i$f i *s B$f i) = 0"
chaieb@29846
   639
	unfolding det_rows_mul by simp}
chaieb@29846
   640
    moreover
chaieb@29846
   641
    {assume fi: "inj_on f ?U"
chaieb@29846
   642
      from f fi have fith: "\<And>i j. f i = f j \<Longrightarrow> i = j"
huffman@30582
   643
	unfolding inj_on_def by metis
chaieb@29846
   644
      note fs = fi[unfolded surjective_iff_injective_gen[OF fU fU refl fUU, symmetric]]
huffman@30489
   645
chaieb@29846
   646
      {fix y
huffman@30582
   647
	from fs f have "\<exists>x. f x = y" by blast
chaieb@29846
   648
	then obtain x where x: "f x = y" by blast
chaieb@29846
   649
	{fix z assume z: "f z = y" from fith x z have "z = x" by metis}
chaieb@29846
   650
	with x have "\<exists>!x. f x = y" by blast}
chaieb@29846
   651
      with f(3) have "det (\<chi> i. A$i$f i *s B$f i) = 0" by blast}
chaieb@29846
   652
    ultimately have "det (\<chi> i. A$i$f i *s B$f i) = 0" by blast}
chaieb@29846
   653
  hence zth: "\<forall> f\<in> ?F - ?PU. det (\<chi> i. A$i$f i *s B$f i) = 0" by simp
chaieb@29846
   654
  {fix p assume pU: "p \<in> ?PU"
chaieb@29846
   655
    from pU have p: "p permutes ?U" by blast
chaieb@29846
   656
    let ?s = "\<lambda>p. of_int (sign p)"
chaieb@29846
   657
    let ?f = "\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) *
chaieb@29846
   658
               (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))"
chaieb@29846
   659
    have "(setsum (\<lambda>q. ?s q *
chaieb@29846
   660
            (\<Prod>i\<in> ?U. (\<chi> i. A $ i $ p i *s B $ p i :: 'a^'n^'n) $ i $ q i)) ?PU) =
chaieb@29846
   661
        (setsum (\<lambda>q. ?s p * (\<Prod>i\<in> ?U. A $ i $ p i) *
chaieb@29846
   662
               (?s q * (\<Prod>i\<in> ?U. B $ i $ q i))) ?PU)"
chaieb@29846
   663
      unfolding sum_permutations_compose_right[OF permutes_inv[OF p], of ?f]
chaieb@29846
   664
    proof(rule setsum_cong2)
chaieb@29846
   665
      fix q assume qU: "q \<in> ?PU"
chaieb@29846
   666
      hence q: "q permutes ?U" by blast
chaieb@29846
   667
      from p q have pp: "permutation p" and pq: "permutation q"
huffman@30489
   668
	unfolding permutation_permutes by auto
huffman@30489
   669
      have th00: "of_int (sign p) * of_int (sign p) = (1::'a)"
huffman@30489
   670
	"\<And>a. of_int (sign p) * (of_int (sign p) * a) = a"
huffman@30489
   671
	unfolding mult_assoc[symmetric]	unfolding of_int_mult[symmetric]
chaieb@29846
   672
	by (simp_all add: sign_idempotent)
chaieb@29846
   673
      have ths: "?s q = ?s p * ?s (q o inv p)"
chaieb@29846
   674
	using pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
chaieb@29846
   675
	by (simp add:  th00 mult_ac sign_idempotent sign_compose)
chaieb@29846
   676
      have th001: "setprod (\<lambda>i. B$i$ q (inv p i)) ?U = setprod ((\<lambda>i. B$i$ q (inv p i)) o p) ?U"
chaieb@29846
   677
	by (rule setprod_permute[OF p])
huffman@30489
   678
      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"
chaieb@29846
   679
	unfolding th001 setprod_timesf[symmetric] o_def permutes_inverses[OF p]
chaieb@29846
   680
	apply (rule setprod_cong[OF refl])
chaieb@29846
   681
	using permutes_in_image[OF q] by vector
chaieb@29846
   682
      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)"
chaieb@29846
   683
	using ths thp pp pq permutation_inverse[OF pp] sign_inverse[OF pp]
chaieb@29846
   684
	by (simp add: sign_nz th00 ring_simps sign_idempotent sign_compose)
chaieb@29846
   685
    qed
chaieb@29846
   686
  }
huffman@30489
   687
  then have th2: "setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU = det A * det B"
chaieb@29846
   688
    unfolding det_def setsum_product
huffman@30489
   689
    by (rule setsum_cong2)
chaieb@29846
   690
  have "det (A**B) = setsum (\<lambda>f.  det (\<chi> i. A $ i $ f i *s B $ f i)) ?F"
huffman@30582
   691
    unfolding matrix_mul_setsum_alt det_linear_rows_setsum[OF fU] by simp
chaieb@29846
   692
  also have "\<dots> = setsum (\<lambda>f. det (\<chi> i. A$i$f i *s B$f i)) ?PU"
huffman@30489
   693
    using setsum_mono_zero_cong_left[OF fF PUF zth, symmetric]
chaieb@30259
   694
    unfolding det_rows_mul by auto
chaieb@29846
   695
  finally show ?thesis unfolding th2 .
huffman@30489
   696
qed
chaieb@29846
   697
chaieb@29846
   698
(* ------------------------------------------------------------------------- *)
chaieb@29846
   699
(* Relation to invertibility.                                                *)
chaieb@29846
   700
(* ------------------------------------------------------------------------- *)
chaieb@29846
   701
chaieb@29846
   702
lemma invertible_left_inverse:
huffman@30582
   703
  fixes A :: "real^'n^'n::finite"
chaieb@29846
   704
  shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). B** A = mat 1)"
chaieb@29846
   705
  by (metis invertible_def matrix_left_right_inverse)
chaieb@29846
   706
chaieb@29846
   707
lemma invertible_righ_inverse:
huffman@30582
   708
  fixes A :: "real^'n^'n::finite"
chaieb@29846
   709
  shows "invertible A \<longleftrightarrow> (\<exists>(B::real^'n^'n). A** B = mat 1)"
chaieb@29846
   710
  by (metis invertible_def matrix_left_right_inverse)
chaieb@29846
   711
huffman@30489
   712
lemma invertible_det_nz:
huffman@30598
   713
  fixes A::"real ^'n^'n::finite"
chaieb@29846
   714
  shows "invertible A \<longleftrightarrow> det A \<noteq> 0"
chaieb@29846
   715
proof-
chaieb@29846
   716
  {assume "invertible A"
chaieb@29846
   717
    then obtain B :: "real ^'n^'n" where B: "A ** B = mat 1"
chaieb@29846
   718
      unfolding invertible_righ_inverse by blast
chaieb@29846
   719
    hence "det (A ** B) = det (mat 1 :: real ^'n^'n)" by simp
chaieb@29846
   720
    hence "det A \<noteq> 0"
chaieb@29846
   721
      apply (simp add: det_mul det_I) by algebra }
chaieb@29846
   722
  moreover
chaieb@29846
   723
  {assume H: "\<not> invertible A"
huffman@30582
   724
    let ?U = "UNIV :: 'n set"
chaieb@29846
   725
    have fU: "finite ?U" by simp
huffman@30489
   726
    from H obtain c i where c: "setsum (\<lambda>i. c i *s row i A) ?U = 0"
chaieb@29846
   727
      and iU: "i \<in> ?U" and ci: "c i \<noteq> 0"
chaieb@29846
   728
      unfolding invertible_righ_inverse
chaieb@29846
   729
      unfolding matrix_right_invertible_independent_rows by blast
chaieb@29846
   730
    have stupid: "\<And>(a::real^'n) b. a + b = 0 \<Longrightarrow> -a = b"
chaieb@29846
   731
      apply (drule_tac f="op + (- a)" in cong[OF refl])
chaieb@29846
   732
      apply (simp only: ab_left_minus add_assoc[symmetric])
chaieb@29846
   733
      apply simp
chaieb@29846
   734
      done
huffman@30489
   735
    from c ci
chaieb@29846
   736
    have thr0: "- row i A = setsum (\<lambda>j. (1/ c i) *s c j *s row j A) (?U - {i})"
huffman@30489
   737
      unfolding setsum_diff1'[OF fU iU] setsum_cmul
huffman@30582
   738
      apply -
chaieb@29846
   739
      apply (rule vector_mul_lcancel_imp[OF ci])
chaieb@29846
   740
      apply (auto simp add: vector_smult_assoc vector_smult_rneg field_simps)
chaieb@29846
   741
      unfolding stupid ..
huffman@30582
   742
    have thr: "- row i A \<in> span {row j A| j. j \<noteq> i}"
chaieb@29846
   743
      unfolding thr0
chaieb@29846
   744
      apply (rule span_setsum)
chaieb@29846
   745
      apply simp
chaieb@29846
   746
      apply (rule ballI)
chaieb@29846
   747
      apply (rule span_mul)+
chaieb@29846
   748
      apply (rule span_superset)
chaieb@29846
   749
      apply auto
chaieb@29846
   750
      done
chaieb@29846
   751
    let ?B = "(\<chi> k. if k = i then 0 else row k A) :: real ^'n^'n"
huffman@30489
   752
    have thrb: "row i ?B = 0" using iU by (vector row_def)
huffman@30489
   753
    have "det A = 0"
huffman@30582
   754
      unfolding det_row_span[OF thr, symmetric] right_minus
huffman@30582
   755
      unfolding  det_zero_row[OF thrb]  ..}
chaieb@29846
   756
  ultimately show ?thesis by blast
chaieb@29846
   757
qed
chaieb@29846
   758
chaieb@29846
   759
(* ------------------------------------------------------------------------- *)
chaieb@29846
   760
(* Cramer's rule.                                                            *)
chaieb@29846
   761
(* ------------------------------------------------------------------------- *)
chaieb@29846
   762
chaieb@29846
   763
lemma cramer_lemma_transp:
huffman@30582
   764
  fixes A:: "'a::ordered_idom^'n^'n::finite" and x :: "'a ^'n::finite"
huffman@30582
   765
  shows "det ((\<chi> i. if i = k then setsum (\<lambda>i. x$i *s row i A) (UNIV::'n set)
huffman@30489
   766
                           else row i A)::'a^'n^'n) = x$k * det A"
huffman@30489
   767
  (is "?lhs = ?rhs")
chaieb@29846
   768
proof-
huffman@30582
   769
  let ?U = "UNIV :: 'n set"
chaieb@29846
   770
  let ?Uk = "?U - {k}"
huffman@30582
   771
  have U: "?U = insert k ?Uk" by blast
chaieb@29846
   772
  have fUk: "finite ?Uk" by simp
chaieb@29846
   773
  have kUk: "k \<notin> ?Uk" by simp
chaieb@29846
   774
  have th00: "\<And>k s. x$k *s row k A + s = (x$k - 1) *s row k A + row k A + s"
chaieb@29846
   775
    by (vector ring_simps)
chaieb@29846
   776
  have th001: "\<And>f k . (\<lambda>x. if x = k then f k else f x) = f" by (auto intro: ext)
chaieb@29846
   777
  have "(\<chi> i. row i A) = A" by (vector row_def)
huffman@30489
   778
  then have thd1: "det (\<chi> i. row i A) = det A"  by simp
chaieb@29846
   779
  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"
huffman@30582
   780
    apply (rule det_row_span)
chaieb@29846
   781
    apply (rule span_setsum[OF fUk])
chaieb@29846
   782
    apply (rule ballI)
chaieb@29846
   783
    apply (rule span_mul)
chaieb@29846
   784
    apply (rule span_superset)
chaieb@29846
   785
    apply auto
chaieb@29846
   786
    done
chaieb@29846
   787
  show "?lhs = x$k * det A"
chaieb@29846
   788
    apply (subst U)
huffman@30489
   789
    unfolding setsum_insert[OF fUk kUk]
chaieb@29846
   790
    apply (subst th00)
chaieb@29846
   791
    unfolding add_assoc
huffman@30582
   792
    apply (subst det_row_add)
chaieb@29846
   793
    unfolding thd0
huffman@30582
   794
    unfolding det_row_mul
chaieb@29846
   795
    unfolding th001[of k "\<lambda>i. row i A"]
chaieb@29846
   796
    unfolding thd1  by (simp add: ring_simps)
chaieb@29846
   797
qed
chaieb@29846
   798
chaieb@29846
   799
lemma cramer_lemma:
huffman@30582
   800
  fixes A :: "'a::ordered_idom ^'n^'n::finite"
chaieb@29846
   801
  shows "det((\<chi> i j. if j = k then (A *v x)$i else A$i$j):: 'a^'n^'n) = x$k * det A"
chaieb@29846
   802
proof-
huffman@30582
   803
  let ?U = "UNIV :: 'n set"
chaieb@29846
   804
  have stupid: "\<And>c. setsum (\<lambda>i. c i *s row i (transp A)) ?U = setsum (\<lambda>i. c i *s column i A) ?U"
chaieb@29846
   805
    by (auto simp add: row_transp intro: setsum_cong2)
huffman@30598
   806
  show ?thesis  unfolding matrix_mult_vsum
huffman@30582
   807
  unfolding cramer_lemma_transp[of k x "transp A", unfolded det_transp, symmetric]
chaieb@29846
   808
  unfolding stupid[of "\<lambda>i. x$i"]
chaieb@29846
   809
  apply (subst det_transp[symmetric])
chaieb@29846
   810
  apply (rule cong[OF refl[of det]]) by (vector transp_def column_def row_def)
chaieb@29846
   811
qed
chaieb@29846
   812
chaieb@29846
   813
lemma cramer:
huffman@30598
   814
  fixes A ::"real^'n^'n::finite"
huffman@30489
   815
  assumes d0: "det A \<noteq> 0"
chaieb@29846
   816
  shows "A *v x = b \<longleftrightarrow> x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)"
chaieb@29846
   817
proof-
huffman@30489
   818
  from d0 obtain B where B: "A ** B = mat 1" "B ** A = mat 1"
chaieb@29846
   819
    unfolding invertible_det_nz[symmetric] invertible_def by blast
chaieb@29846
   820
  have "(A ** B) *v b = b" by (simp add: B matrix_vector_mul_lid)
chaieb@29846
   821
  hence "A *v (B *v b) = b" by (simp add: matrix_vector_mul_assoc)
chaieb@29846
   822
  then have xe: "\<exists>x. A*v x = b" by blast
chaieb@29846
   823
  {fix x assume x: "A *v x = b"
chaieb@29846
   824
  have "x = (\<chi> k. det(\<chi> i j. if j=k then b$i else A$i$j :: real^'n^'n) / det A)"
chaieb@29846
   825
    unfolding x[symmetric]
huffman@30582
   826
    using d0 by (simp add: Cart_eq cramer_lemma field_simps)}
chaieb@29846
   827
  with xe show ?thesis by auto
chaieb@29846
   828
qed
chaieb@29846
   829
chaieb@29846
   830
(* ------------------------------------------------------------------------- *)
chaieb@29846
   831
(* Orthogonality of a transformation and matrix.                             *)
chaieb@29846
   832
(* ------------------------------------------------------------------------- *)
chaieb@29846
   833
chaieb@29846
   834
definition "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>v w. f v \<bullet> f w = v \<bullet> w)"
chaieb@29846
   835
huffman@30582
   836
lemma orthogonal_transformation: "orthogonal_transformation f \<longleftrightarrow> linear f \<and> (\<forall>(v::real ^_). norm (f v) = norm v)"
chaieb@29846
   837
  unfolding orthogonal_transformation_def
huffman@30489
   838
  apply auto
chaieb@29846
   839
  apply (erule_tac x=v in allE)+
chaieb@29846
   840
  apply (simp add: real_vector_norm_def)
huffman@30489
   841
  by (simp add: dot_norm  linear_add[symmetric])
chaieb@29846
   842
chaieb@29846
   843
definition "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow> transp Q ** Q = mat 1 \<and> Q ** transp Q = mat 1"
chaieb@29846
   844
huffman@30582
   845
lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n::finite)  \<longleftrightarrow> transp Q ** Q = mat 1"
chaieb@29846
   846
  by (metis matrix_left_right_inverse orthogonal_matrix_def)
chaieb@29846
   847
huffman@30582
   848
lemma orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n::finite)"
chaieb@29846
   849
  by (simp add: orthogonal_matrix_def transp_mat matrix_mul_lid)
chaieb@29846
   850
huffman@30489
   851
lemma orthogonal_matrix_mul:
huffman@30582
   852
  fixes A :: "real ^'n^'n::finite"
chaieb@29846
   853
  assumes oA : "orthogonal_matrix A"
huffman@30489
   854
  and oB: "orthogonal_matrix B"
chaieb@29846
   855
  shows "orthogonal_matrix(A ** B)"
huffman@30489
   856
  using oA oB
chaieb@29846
   857
  unfolding orthogonal_matrix matrix_transp_mul
chaieb@29846
   858
  apply (subst matrix_mul_assoc)
chaieb@29846
   859
  apply (subst matrix_mul_assoc[symmetric])
chaieb@29846
   860
  by (simp add: matrix_mul_rid)
chaieb@29846
   861
chaieb@29846
   862
lemma orthogonal_transformation_matrix:
huffman@30582
   863
  fixes f:: "real^'n \<Rightarrow> real^'n::finite"
chaieb@29846
   864
  shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
chaieb@29846
   865
  (is "?lhs \<longleftrightarrow> ?rhs")
chaieb@29846
   866
proof-
chaieb@29846
   867
  let ?mf = "matrix f"
chaieb@29846
   868
  let ?ot = "orthogonal_transformation f"
huffman@30582
   869
  let ?U = "UNIV :: 'n set"
chaieb@29846
   870
  have fU: "finite ?U" by simp
chaieb@29846
   871
  let ?m1 = "mat 1 :: real ^'n^'n"
chaieb@29846
   872
  {assume ot: ?ot
chaieb@29846
   873
    from ot have lf: "linear f" and fd: "\<forall>v w. f v \<bullet> f w = v \<bullet> w"
chaieb@29846
   874
      unfolding  orthogonal_transformation_def orthogonal_matrix by blast+
huffman@30582
   875
    {fix i j
chaieb@29846
   876
      let ?A = "transp ?mf ** ?mf"
chaieb@29846
   877
      have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
chaieb@29846
   878
	"\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"
chaieb@29846
   879
	by simp_all
huffman@30582
   880
      from fd[rule_format, of "basis i" "basis j", unfolded matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
huffman@30489
   881
      have "?A$i$j = ?m1 $ i $ j"
huffman@30582
   882
	by (simp add: dot_def matrix_matrix_mult_def columnvector_def rowvector_def basis_def th0 setsum_delta[OF fU] mat_def)}
chaieb@29846
   883
    hence "orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector
chaieb@29846
   884
    with lf have ?rhs by blast}
chaieb@29846
   885
  moreover
chaieb@29846
   886
  {assume lf: "linear f" and om: "orthogonal_matrix ?mf"
chaieb@29846
   887
    from lf om have ?lhs
chaieb@29846
   888
      unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
chaieb@29846
   889
      unfolding matrix_works[OF lf, symmetric]
chaieb@29846
   890
      apply (subst dot_matrix_vector_mul)
huffman@30582
   891
      by (simp add: dot_matrix_product matrix_mul_lid)}
chaieb@29846
   892
  ultimately show ?thesis by blast
chaieb@29846
   893
qed
chaieb@29846
   894
huffman@30489
   895
lemma det_orthogonal_matrix:
huffman@30598
   896
  fixes Q:: "'a::ordered_idom^'n^'n::finite"
chaieb@29846
   897
  assumes oQ: "orthogonal_matrix Q"
chaieb@29846
   898
  shows "det Q = 1 \<or> det Q = - 1"
chaieb@29846
   899
proof-
huffman@30489
   900
huffman@30489
   901
  have th: "\<And>x::'a. x = 1 \<or> x = - 1 \<longleftrightarrow> x*x = 1" (is "\<And>x::'a. ?ths x")
huffman@30489
   902
  proof-
chaieb@29846
   903
    fix x:: 'a
chaieb@29846
   904
    have th0: "x*x - 1 = (x - 1)*(x + 1)" by (simp add: ring_simps)
huffman@30489
   905
    have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0"
chaieb@29846
   906
      apply (subst eq_iff_diff_eq_0) by simp
chaieb@29846
   907
    have "x*x = 1 \<longleftrightarrow> x*x - 1 = 0" by simp
chaieb@29846
   908
    also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1" unfolding th0 th1 by simp
chaieb@29846
   909
    finally show "?ths x" ..
chaieb@29846
   910
  qed
chaieb@29846
   911
  from oQ have "Q ** transp Q = mat 1" by (metis orthogonal_matrix_def)
chaieb@29846
   912
  hence "det (Q ** transp Q) = det (mat 1:: 'a^'n^'n)" by simp
chaieb@29846
   913
  hence "det Q * det Q = 1" by (simp add: det_mul det_I det_transp)
huffman@30489
   914
  then show ?thesis unfolding th .
chaieb@29846
   915
qed
chaieb@29846
   916
chaieb@29846
   917
(* ------------------------------------------------------------------------- *)
chaieb@29846
   918
(* Linearity of scaling, and hence isometry, that preserves origin.          *)
chaieb@29846
   919
(* ------------------------------------------------------------------------- *)
huffman@30489
   920
lemma scaling_linear:
huffman@30582
   921
  fixes f :: "real ^'n \<Rightarrow> real ^'n::finite"
chaieb@29846
   922
  assumes f0: "f 0 = 0" and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
chaieb@29846
   923
  shows "linear f"
chaieb@29846
   924
proof-
huffman@30489
   925
  {fix v w
chaieb@29846
   926
    {fix x note fd[rule_format, of x 0, unfolded dist_def f0 diff_0_right] }
chaieb@29846
   927
    note th0 = this
huffman@30489
   928
    have "f v \<bullet> f w = c^2 * (v \<bullet> w)"
chaieb@29846
   929
      unfolding dot_norm_neg dist_def[symmetric]
chaieb@29846
   930
      unfolding th0 fd[rule_format] by (simp add: power2_eq_square field_simps)}
chaieb@29846
   931
  note fc = this
chaieb@29846
   932
  show ?thesis unfolding linear_def vector_eq
chaieb@29846
   933
    by (simp add: dot_lmult dot_ladd dot_rmult dot_radd fc ring_simps)
huffman@30489
   934
qed
chaieb@29846
   935
chaieb@29846
   936
lemma isometry_linear:
huffman@30582
   937
  "f (0:: real^'n) = (0:: real^'n::finite) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y
chaieb@29846
   938
        \<Longrightarrow> linear f"
chaieb@29846
   939
by (rule scaling_linear[where c=1]) simp_all
chaieb@29846
   940
chaieb@29846
   941
(* ------------------------------------------------------------------------- *)
chaieb@29846
   942
(* Hence another formulation of orthogonal transformation.                   *)
chaieb@29846
   943
(* ------------------------------------------------------------------------- *)
chaieb@29846
   944
chaieb@29846
   945
lemma orthogonal_transformation_isometry:
huffman@30582
   946
  "orthogonal_transformation f \<longleftrightarrow> f(0::real^'n) = (0::real^'n::finite) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
huffman@30489
   947
  unfolding orthogonal_transformation
chaieb@29846
   948
  apply (rule iffI)
chaieb@29846
   949
  apply clarify
chaieb@29846
   950
  apply (clarsimp simp add: linear_0 linear_sub[symmetric] dist_def)
chaieb@29846
   951
  apply (rule conjI)
chaieb@29846
   952
  apply (rule isometry_linear)
chaieb@29846
   953
  apply simp
chaieb@29846
   954
  apply simp
chaieb@29846
   955
  apply clarify
chaieb@29846
   956
  apply (erule_tac x=v in allE)
chaieb@29846
   957
  apply (erule_tac x=0 in allE)
chaieb@29846
   958
  by (simp add: dist_def)
chaieb@29846
   959
chaieb@29846
   960
(* ------------------------------------------------------------------------- *)
chaieb@29846
   961
(* Can extend an isometry from unit sphere.                                  *)
chaieb@29846
   962
(* ------------------------------------------------------------------------- *)
chaieb@29846
   963
chaieb@29846
   964
lemma isometry_sphere_extend:
huffman@30582
   965
  fixes f:: "real ^'n \<Rightarrow> real ^'n::finite"
chaieb@29846
   966
  assumes f1: "\<forall>x. norm x = 1 \<longrightarrow> norm (f x) = 1"
chaieb@29846
   967
  and fd1: "\<forall> x y. norm x = 1 \<longrightarrow> norm y = 1 \<longrightarrow> dist (f x) (f y) = dist x y"
chaieb@29846
   968
  shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
chaieb@29846
   969
proof-
huffman@30489
   970
  {fix x y x' y' x0 y0 x0' y0' :: "real ^'n"
chaieb@29846
   971
    assume H: "x = norm x *s x0" "y = norm y *s y0"
huffman@30489
   972
    "x' = norm x *s x0'" "y' = norm y *s y0'"
chaieb@29846
   973
    "norm x0 = 1" "norm x0' = 1" "norm y0 = 1" "norm y0' = 1"
chaieb@29846
   974
    "norm(x0' - y0') = norm(x0 - y0)"
huffman@30489
   975
chaieb@29846
   976
    have "norm(x' - y') = norm(x - y)"
chaieb@29846
   977
      apply (subst H(1))
chaieb@29846
   978
      apply (subst H(2))
chaieb@29846
   979
      apply (subst H(3))
chaieb@29846
   980
      apply (subst H(4))
chaieb@29846
   981
      using H(5-9)
chaieb@29846
   982
      apply (simp add: norm_eq norm_eq_1)
chaieb@29846
   983
      apply (simp add: dot_lsub dot_rsub dot_lmult dot_rmult)
chaieb@29846
   984
      apply (simp add: ring_simps)
chaieb@29846
   985
      by (simp only: right_distrib[symmetric])}
chaieb@29846
   986
  note th0 = this
chaieb@29846
   987
  let ?g = "\<lambda>x. if x = 0 then 0 else norm x *s f (inverse (norm x) *s x)"
chaieb@29846
   988
  {fix x:: "real ^'n" assume nx: "norm x = 1"
huffman@30041
   989
    have "?g x = f x" using nx by auto}
chaieb@29846
   990
  hence thfg: "\<forall>x. norm x = 1 \<longrightarrow> ?g x = f x" by blast
chaieb@29846
   991
  have g0: "?g 0 = 0" by simp
chaieb@29846
   992
  {fix x y :: "real ^'n"
chaieb@29846
   993
    {assume "x = 0" "y = 0"
chaieb@29846
   994
      then have "dist (?g x) (?g y) = dist x y" by simp }
chaieb@29846
   995
    moreover
chaieb@29846
   996
    {assume "x = 0" "y \<noteq> 0"
huffman@30489
   997
      then have "dist (?g x) (?g y) = dist x y"
huffman@30041
   998
	apply (simp add: dist_def norm_mul)
chaieb@29846
   999
	apply (rule f1[rule_format])
huffman@30041
  1000
	by(simp add: norm_mul field_simps)}
chaieb@29846
  1001
    moreover
chaieb@29846
  1002
    {assume "x \<noteq> 0" "y = 0"
huffman@30489
  1003
      then have "dist (?g x) (?g y) = dist x y"
huffman@30041
  1004
	apply (simp add: dist_def norm_mul)
chaieb@29846
  1005
	apply (rule f1[rule_format])
huffman@30041
  1006
	by(simp add: norm_mul field_simps)}
chaieb@29846
  1007
    moreover
chaieb@29846
  1008
    {assume z: "x \<noteq> 0" "y \<noteq> 0"
chaieb@29846
  1009
      have th00: "x = norm x *s inverse (norm x) *s x" "y = norm y *s inverse (norm y) *s y" "norm x *s f (inverse (norm x) *s x) = norm x *s f (inverse (norm x) *s x)"
chaieb@29846
  1010
	"norm y *s f (inverse (norm y) *s y) = norm y *s f (inverse (norm y) *s y)"
chaieb@29846
  1011
	"norm (inverse (norm x) *s x) = 1"
chaieb@29846
  1012
	"norm (f (inverse (norm x) *s x)) = 1"
chaieb@29846
  1013
	"norm (inverse (norm y) *s y) = 1"
chaieb@29846
  1014
	"norm (f (inverse (norm y) *s y)) = 1"
chaieb@29846
  1015
	"norm (f (inverse (norm x) *s x) - f (inverse (norm y) *s y)) =
chaieb@29846
  1016
	norm (inverse (norm x) *s x - inverse (norm y) *s y)"
chaieb@29846
  1017
	using z
huffman@30041
  1018
	by (auto simp add: vector_smult_assoc field_simps norm_mul intro: f1[rule_format] fd1[rule_format, unfolded dist_def])
huffman@30489
  1019
      from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
chaieb@29846
  1020
	by (simp add: dist_def)}
chaieb@29846
  1021
    ultimately have "dist (?g x) (?g y) = dist x y" by blast}
chaieb@29846
  1022
  note thd = this
huffman@30489
  1023
    show ?thesis
chaieb@29846
  1024
    apply (rule exI[where x= ?g])
chaieb@29846
  1025
    unfolding orthogonal_transformation_isometry
huffman@30489
  1026
      using  g0 thfg thd by metis
chaieb@29846
  1027
qed
chaieb@29846
  1028
chaieb@29846
  1029
(* ------------------------------------------------------------------------- *)
chaieb@29846
  1030
(* Rotation, reflection, rotoinversion.                                      *)
chaieb@29846
  1031
(* ------------------------------------------------------------------------- *)
chaieb@29846
  1032
chaieb@29846
  1033
definition "rotation_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = 1"
chaieb@29846
  1034
definition "rotoinversion_matrix Q \<longleftrightarrow> orthogonal_matrix Q \<and> det Q = - 1"
chaieb@29846
  1035
huffman@30489
  1036
lemma orthogonal_rotation_or_rotoinversion:
huffman@30598
  1037
  fixes Q :: "'a::ordered_idom^'n^'n::finite"
chaieb@29846
  1038
  shows " orthogonal_matrix Q \<longleftrightarrow> rotation_matrix Q \<or> rotoinversion_matrix Q"
chaieb@29846
  1039
  by (metis rotoinversion_matrix_def rotation_matrix_def det_orthogonal_matrix)
chaieb@29846
  1040
(* ------------------------------------------------------------------------- *)
chaieb@29846
  1041
(* Explicit formulas for low dimensions.                                     *)
chaieb@29846
  1042
(* ------------------------------------------------------------------------- *)
chaieb@29846
  1043
chaieb@29846
  1044
lemma setprod_1: "setprod f {(1::nat)..1} = f 1" by simp
chaieb@29846
  1045
huffman@30489
  1046
lemma setprod_2: "setprod f {(1::nat)..2} = f 1 * f 2"
chaieb@29846
  1047
  by (simp add: nat_number setprod_numseg mult_commute)
huffman@30489
  1048
lemma setprod_3: "setprod f {(1::nat)..3} = f 1 * f 2 * f 3"
chaieb@29846
  1049
  by (simp add: nat_number setprod_numseg mult_commute)
chaieb@29846
  1050
chaieb@29846
  1051
lemma det_1: "det (A::'a::comm_ring_1^1^1) = A$1$1"
huffman@30582
  1052
  by (simp add: det_def permutes_sing sign_id UNIV_1)
chaieb@29846
  1053
chaieb@29846
  1054
lemma det_2: "det (A::'a::comm_ring_1^2^2) = A$1$1 * A$2$2 - A$1$2 * A$2$1"
chaieb@29846
  1055
proof-
huffman@30582
  1056
  have f12: "finite {2::2}" "1 \<notin> {2::2}" by auto
huffman@30489
  1057
  show ?thesis
huffman@30582
  1058
  unfolding det_def UNIV_2
chaieb@29846
  1059
  unfolding setsum_over_permutations_insert[OF f12]
chaieb@29846
  1060
  unfolding permutes_sing
huffman@30582
  1061
  apply (simp add: sign_swap_id sign_id swap_id_eq)
chaieb@29846
  1062
  by (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31))
chaieb@29846
  1063
qed
chaieb@29846
  1064
huffman@30489
  1065
lemma det_3: "det (A::'a::comm_ring_1^3^3) =
chaieb@29846
  1066
  A$1$1 * A$2$2 * A$3$3 +
chaieb@29846
  1067
  A$1$2 * A$2$3 * A$3$1 +
chaieb@29846
  1068
  A$1$3 * A$2$1 * A$3$2 -
chaieb@29846
  1069
  A$1$1 * A$2$3 * A$3$2 -
chaieb@29846
  1070
  A$1$2 * A$2$1 * A$3$3 -
chaieb@29846
  1071
  A$1$3 * A$2$2 * A$3$1"
chaieb@29846
  1072
proof-
huffman@30582
  1073
  have f123: "finite {2::3, 3}" "1 \<notin> {2::3, 3}" by auto
huffman@30582
  1074
  have f23: "finite {3::3}" "2 \<notin> {3::3}" by auto
chaieb@29846
  1075
huffman@30489
  1076
  show ?thesis
huffman@30582
  1077
  unfolding det_def UNIV_3
chaieb@29846
  1078
  unfolding setsum_over_permutations_insert[OF f123]
chaieb@29846
  1079
  unfolding setsum_over_permutations_insert[OF f23]
chaieb@29846
  1080
chaieb@29846
  1081
  unfolding permutes_sing
huffman@30582
  1082
  apply (simp add: sign_swap_id permutation_swap_id sign_compose sign_id swap_id_eq)
huffman@30582
  1083
  apply (simp add: arith_simps(31)[symmetric] of_int_minus of_int_1 del: arith_simps(31))
chaieb@29846
  1084
  by (simp add: ring_simps)
chaieb@29846
  1085
qed
chaieb@29846
  1086
huffman@30041
  1087
end