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