src/HOL/Analysis/Determinants.thy

       of_int (sign p) * (prod (\<lambda>i. ?di A i (p i)) ?U)"
       using sth by simp
   }
   then show ?thesis
     unfolding det_def
-    by (subst sum_permutations_inverse) (blast intro: sum.cong elim: )
+    by (subst sum_permutations_inverse) (blast intro: sum.cong)
 qed
 
 lemma det_lowerdiagonal:
   fixes A :: "'a::comm_ring_1^('n::{finite,wellorder})^('n::{finite,wellorder})"
   assumes ld: "\<And>i j. i < j \<Longrightarrow> A$i$j = 0"

   let ?PU = "{p. p permutes ?U}"
   let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
   have fU: "finite ?U"
     by simp
   have id0: "{id} \<subseteq> ?PU"
-    by (auto simp add: permutes_id)
+    by (auto simp: permutes_id)
   have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
   proof
     fix p
     assume "p \<in> ?PU - {id}"
     then obtain i where i: "p i > i"

   let ?PU = "{p. p permutes ?U}"
   let ?pp = "(\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set))"
   have fU: "finite ?U"
     by simp
   have id0: "{id} \<subseteq> ?PU"
-    by (auto simp add: permutes_id)
+    by (auto simp: permutes_id)
   have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"
   proof
     fix p
     assume p: "p \<in> ?PU - {id}"
     then obtain i where i: "p i < i"

   let ?PU = "{p. p permutes ?U}"
   let ?pp = "\<lambda>p. of_int (sign p) * prod (\<lambda>i. A$i$p i) (UNIV :: 'n set)"
   have fU: "finite ?U" by simp
   from finite_permutations[OF fU] have fPU: "finite ?PU" .
   have id0: "{id} \<subseteq> ?PU"
-    by (auto simp add: permutes_id)
+    by (auto simp: permutes_id)
   have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
   proof
     fix p
     assume p: "p \<in> ?PU - {id}"
     then obtain i where i: "p i \<noteq> i"

   {fix x
     assume x: "x\<in> ?S1"
     have "sign (?t_jk \<circ> x) = sign (?t_jk) * sign x"
       by (metis (lifting) finite_class.finite_UNIV mem_Collect_eq
           permutation_permutes permutation_swap_id sign_compose x)
-    also have "... = - sign x" using sign_tjk by simp
-    also have "... \<noteq> sign x" unfolding sign_def by simp
+    also have "\<dots> = - sign x" using sign_tjk by simp
+    also have "\<dots> \<noteq> sign x" unfolding sign_def by simp
     finally have "sign (?t_jk \<circ> x) \<noteq> sign x" and "(?t_jk \<circ> x) \<in> ?S2"
       using x by force+
   }
   hence disjoint: "?S1 \<inter> ?S2 = {}"
     by (force simp: sign_def)

     show "Fun.swap j k id \<circ> p permutes UNIV" by (metis p permutes_compose tjk_permutes)
   qed
   have "sum ?f ?S2 = sum ((\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))
   \<circ> (\<circ>) (Fun.swap j k id)) {p \<in> {p. p permutes UNIV}. evenperm p}"
     unfolding g_S1 by (rule sum.reindex[OF inj_g])
-  also have "... = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1"
-    unfolding o_def by (rule sum.cong, auto simp add: tjk_eq)
-  also have "... = sum (\<lambda>p. - ?f p) ?S1"
+  also have "\<dots> = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1"
+    unfolding o_def by (rule sum.cong, auto simp: tjk_eq)
+  also have "\<dots> = sum (\<lambda>p. - ?f p) ?S1"
   proof (rule sum.cong, auto)
     fix x assume x: "x permutes ?U"
       and even_x: "evenperm x"
     hence perm_x: "permutation x" and perm_tjk: "permutation ?t_jk"
       using permutation_permutes[of x] permutation_permutes[of ?t_jk] permutation_swap_id

       unfolding sign_compose[OF perm_tjk perm_x] sign_tjk by auto
     thus "of_int (sign (?t_jk \<circ> x)) * (\<Prod>i\<in>UNIV. A $ i $ x i)
       = - (of_int (sign x) * (\<Prod>i\<in>UNIV. A $ i $ x i))"
       by auto
   qed
-  also have "...= - sum ?f ?S1" unfolding sum_negf ..
+  also have "\<dots>= - sum ?f ?S1" unfolding sum_negf ..
   finally have *: "sum ?f ?S2 = - sum ?f ?S1" .
   have "det A = (\<Sum>p | p permutes UNIV. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))"
     unfolding det_def ..
-  also have "...= sum ?f ?S1 + sum ?f ?S2"
+  also have "\<dots>= sum ?f ?S1 + sum ?f ?S2"
     by (subst PU_decomposition, rule sum.union_disjoint[OF _ _ disjoint], auto)
-  also have "...= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto
-  also have "...= 0" by simp
+  also have "\<dots>= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto
+  also have "\<dots>= 0" by simp
   finally show "det A = 0" by simp
 qed
 
 lemma det_identical_rows:
   fixes A :: "'a::comm_ring_1^'n^'n"

   by (metis column_transpose det_identical_columns det_transpose ij r)
 
 lemma det_zero_row:
   fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
   shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0"
-  by (force simp add: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
+  by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
 
 lemma det_zero_column:
   fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
   shows "column i A = 0 \<Longrightarrow> det A = 0" and "column j F = 0 \<Longrightarrow> det F = 0"
   unfolding atomize_conj atomize_imp

   from p have pU: "p permutes ?U"
     by blast
   have kU: "?U = insert k ?Uk"
     by blast
   have eq: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk"
-    by (auto simp: )
+    by auto
   have Uk: "finite ?Uk" "k \<notin> ?Uk"
     by auto
   have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
     unfolding kU[symmetric] ..
   also have "\<dots> = ?f k $ p k  * prod (\<lambda>i. ?f i $ p i) ?Uk"

     unfolding vec.dependent_def rows_def by blast
   show ?thesis
   proof (cases "\<forall>i j. i \<noteq> j \<longrightarrow> row i A \<noteq> row j A")
     case True
     with i have "vec.span (rows A - {row i A}) \<subseteq> vec.span {row j A |j. j \<noteq> i}"
-      by (auto simp add: rows_def intro!: vec.span_mono)
+      by (auto simp: rows_def intro!: vec.span_mono)
     then have "- row i A \<in> vec.span {row j A|j. j \<noteq> i}"
       by (meson i subsetCE vec.span_neg)
     from det_row_span[OF this]
     have "det A = det (\<chi> k. if k = i then 0 *s 1 else row k A)"
       unfolding right_minus vector_smult_lzero ..

 proof (induct k)
   case 0
   have *: "{f. \<forall>i. f i = i} = {id}"
     by auto
   show ?case
-    by (auto simp add: *)
+    by (auto simp: *)
 next
   case (Suc k)
   let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i"
   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)})"
   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)}"
-    apply (auto simp add: image_iff)
+    apply (auto simp: image_iff)
     apply (rename_tac f)
     apply (rule_tac x="f (Suc k)" in bexI)
-    apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI)
-    apply auto
+    apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI, auto)
     done
   with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]
   show ?case
     by metis
 qed

   from False obtain c i where c: "sum (\<lambda>i. c i *s row i A) ?U = 0" and iU: "i \<in> ?U" and ci: "c i \<noteq> 0"
     unfolding invertible_right_inverse matrix_right_invertible_independent_rows
     by blast
   have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
     unfolding sum_cmul  using c ci   
-    by (auto simp add: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
+    by (auto simp: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
   have thr: "- row i A \<in> vec.span {row j A| j. j \<noteq> i}"
     unfolding thr0 by (auto intro: vec.span_base vec.span_scale vec.span_sum)
   let ?B = "(\<chi> k. if k = i then 0 else row k A) :: 'a^'n^'n"
   have thrb: "row i ?B = 0" using iU by (vector row_def)
   have "det A = 0"

   fix B
   assume 1: "B ** matrix f = mat 1"
   show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id"
   proof (intro exI conjI)
     show "Vector_Spaces.linear ( *s) ( *s) (\<lambda>y. B *v y)"
-      by (simp add:)
+      by simp
     show "(( *v) B) \<circ> f = id"
       unfolding o_def
       by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid)
   qed
 next

   fix B
   assume 1: "matrix f ** B = mat 1"
   show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id"
   proof (intro exI conjI)
     show "Vector_Spaces.linear ( *s) ( *s) (( *v) B)"
-      by (simp add: )
+      by simp
     show "f \<circ> ( *v) B = id"
       using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works
       by (metis (no_types, hide_lams))
   qed
 next

     "orthogonal_transformation f \<Longrightarrow> orthogonal (f x) (f y) \<longleftrightarrow> orthogonal x y"
   by (simp add: orthogonal_def orthogonal_transformation_def)
 
 lemma orthogonal_transformation_compose:
    "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
-  by (auto simp add: orthogonal_transformation_def linear_compose)
+  by (auto simp: orthogonal_transformation_def linear_compose)
 
 lemma orthogonal_transformation_neg:
   "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
   by (auto simp: orthogonal_transformation_def dest: linear_compose_neg)
 

     and oB: "orthogonal_matrix B"
   shows "orthogonal_matrix(A ** B)"
   using oA oB
   unfolding orthogonal_matrix matrix_transpose_mul
   apply (subst matrix_mul_assoc)
-  apply (subst matrix_mul_assoc[symmetric])
-  apply (simp add: )
+  apply (subst matrix_mul_assoc[symmetric], simp)
   done
 
 lemma orthogonal_transformation_matrix:
   fixes f:: "real^'n \<Rightarrow> real^'n"
   shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"

   proof -
     fix x:: 'a
     have th0: "x * x - 1 = (x - 1) * (x + 1)"
       by (simp add: field_simps)
     have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0"
-      apply (subst eq_iff_diff_eq_0)
-      apply simp
+      apply (subst eq_iff_diff_eq_0, simp)
       done
     have "x * x = 1 \<longleftrightarrow> x * x - 1 = 0"
       by simp
     also have "\<dots> \<longleftrightarrow> x = 1 \<or> x = - 1"
       unfolding th0 th1 by simp

   assumes "norm a = 1"
   obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
 proof -
   obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
    and "independent S" "card S = CARD('n)" "span S = UNIV"
-    using vector_in_orthonormal_basis assms by (force simp: )
+    using vector_in_orthonormal_basis assms by force
   then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
     by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
   then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
     using bij_swap_iff [of k "inv f0 a" f0]
     by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply1)

         "norm (inverse (norm y) *\<^sub>R y) = 1"
         "norm (f (inverse (norm y) *\<^sub>R y)) = 1"
         "norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) =
           norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
         using z
-        by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
+        by (auto simp: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
       from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
         by (simp add: dist_norm)
     }
     ultimately have "dist (?g x) (?g y) = dist x y"
       by blast