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