# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1525964379 -3600
# Node ID c738f40e88d493959787a2cd863f0ba5b453b578
# Parent  afcdc4c0ef0df57565663084cedcc644957a5dcc
auto-tidying

diff -r afcdc4c0ef0d -r c738f40e88d4 src/HOL/Analysis/Determinants.thy
--- a/src/HOL/Analysis/Determinants.thy	Thu May 10 15:41:45 2018 +0100
+++ b/src/HOL/Analysis/Determinants.thy	Thu May 10 15:59:39 2018 +0100
@@ -77,7 +77,7 @@
   }
   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:
@@ -91,7 +91,7 @@
   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
@@ -118,7 +118,7 @@
   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
@@ -145,7 +145,7 @@
   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
@@ -250,8 +250,8 @@
     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+
   }
@@ -274,9 +274,9 @@
   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"
@@ -289,14 +289,14 @@
       = - (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
 
@@ -309,7 +309,7 @@
 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"
@@ -376,7 +376,7 @@
   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)"
@@ -475,7 +475,7 @@
   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]
@@ -515,17 +515,16 @@
   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
@@ -736,7 +735,7 @@
     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"
@@ -789,7 +788,7 @@
   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)
@@ -817,7 +816,7 @@
   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))
@@ -967,7 +966,7 @@
 
 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"
@@ -1018,8 +1017,7 @@
   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:
@@ -1081,8 +1079,7 @@
     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
@@ -1199,7 +1196,7 @@
 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"
@@ -1349,7 +1346,7 @@
         "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)
     }
diff -r afcdc4c0ef0d -r c738f40e88d4 src/HOL/Analysis/Infinite_Products.thy
--- a/src/HOL/Analysis/Infinite_Products.thy	Thu May 10 15:41:45 2018 +0100
+++ b/src/HOL/Analysis/Infinite_Products.thy	Thu May 10 15:59:39 2018 +0100
@@ -201,14 +201,14 @@
 next
   assume ?rhs then show ?lhs
     unfolding prod_defs
-    by (rule_tac x="0" in exI) (auto simp: )
+    by (rule_tac x=0 in exI) auto
 qed
 
 lemma convergent_prod_iff_convergent: 
   fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
   assumes "\<And>i. f i \<noteq> 0"
   shows "convergent_prod f \<longleftrightarrow> convergent (\<lambda>n. \<Prod>i\<le>n. f i) \<and> lim (\<lambda>n. \<Prod>i\<le>n. f i) \<noteq> 0"
-  by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI)
+  by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)
 
 
 lemma abs_convergent_prod_altdef:
@@ -566,7 +566,7 @@
       by auto
     then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}"
       by simp (subst prod.union_disjoint; force)
-    also have "... = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
+    also have "\<dots> = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
       by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)
     finally show ?thesis by metis
   qed
@@ -616,7 +616,7 @@
     case (elim n)
     then have "{..n} = {..<N} \<union> {N..n}"
       by auto
-    also have "prod f ... = prod f {..<N} * prod f {N..n}"
+    also have "prod f \<dots> = prod f {..<N} * prod f {N..n}"
       by (intro prod.union_disjoint) auto
     also from N have "prod f {N..n} = prod g {N..n}"
       by (intro prod.cong) simp_all
@@ -656,7 +656,7 @@
   have eq: "prod f {..n + Suc (Max N)} = prod f N" for n
   proof (rule prod.mono_neutral_right)
     show "N \<subseteq> {..n + Suc (Max N)}"
-      by (auto simp add: le_Suc_eq trans_le_add2)
+      by (auto simp: le_Suc_eq trans_le_add2)
     show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1"
       using f by blast
   qed auto
@@ -687,7 +687,7 @@
         show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z)) ` {..n + Max N}"
           using le_Suc_ex by fastforce
       qed (auto simp: inj_on_def)
-      also have "... = ?q"
+      also have "\<dots> = ?q"
         by (rule prod.mono_neutral_right)
            (use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
       finally show ?thesis .