auto-tidying
authorpaulson <lp15@cam.ac.uk>
Thu May 10 15:59:39 2018 +0100 (14 months ago)
changeset 68138c738f40e88d4
parent 68137 afcdc4c0ef0d
child 68142 53b4e204755e
auto-tidying
src/HOL/Analysis/Determinants.thy
src/HOL/Analysis/Infinite_Products.thy
     1.1 --- a/src/HOL/Analysis/Determinants.thy	Thu May 10 15:41:45 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Determinants.thy	Thu May 10 15:59:39 2018 +0100
     1.3 @@ -77,7 +77,7 @@
     1.4    }
     1.5    then show ?thesis
     1.6      unfolding det_def
     1.7 -    by (subst sum_permutations_inverse) (blast intro: sum.cong elim: )
     1.8 +    by (subst sum_permutations_inverse) (blast intro: sum.cong)
     1.9  qed
    1.10  
    1.11  lemma det_lowerdiagonal:
    1.12 @@ -91,7 +91,7 @@
    1.13    have fU: "finite ?U"
    1.14      by simp
    1.15    have id0: "{id} \<subseteq> ?PU"
    1.16 -    by (auto simp add: permutes_id)
    1.17 +    by (auto simp: permutes_id)
    1.18    have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
    1.19    proof
    1.20      fix p
    1.21 @@ -118,7 +118,7 @@
    1.22    have fU: "finite ?U"
    1.23      by simp
    1.24    have id0: "{id} \<subseteq> ?PU"
    1.25 -    by (auto simp add: permutes_id)
    1.26 +    by (auto simp: permutes_id)
    1.27    have p0: "\<forall>p \<in> ?PU -{id}. ?pp p = 0"
    1.28    proof
    1.29      fix p
    1.30 @@ -145,7 +145,7 @@
    1.31    have fU: "finite ?U" by simp
    1.32    from finite_permutations[OF fU] have fPU: "finite ?PU" .
    1.33    have id0: "{id} \<subseteq> ?PU"
    1.34 -    by (auto simp add: permutes_id)
    1.35 +    by (auto simp: permutes_id)
    1.36    have p0: "\<forall>p \<in> ?PU - {id}. ?pp p = 0"
    1.37    proof
    1.38      fix p
    1.39 @@ -250,8 +250,8 @@
    1.40      have "sign (?t_jk \<circ> x) = sign (?t_jk) * sign x"
    1.41        by (metis (lifting) finite_class.finite_UNIV mem_Collect_eq
    1.42            permutation_permutes permutation_swap_id sign_compose x)
    1.43 -    also have "... = - sign x" using sign_tjk by simp
    1.44 -    also have "... \<noteq> sign x" unfolding sign_def by simp
    1.45 +    also have "\<dots> = - sign x" using sign_tjk by simp
    1.46 +    also have "\<dots> \<noteq> sign x" unfolding sign_def by simp
    1.47      finally have "sign (?t_jk \<circ> x) \<noteq> sign x" and "(?t_jk \<circ> x) \<in> ?S2"
    1.48        using x by force+
    1.49    }
    1.50 @@ -274,9 +274,9 @@
    1.51    have "sum ?f ?S2 = sum ((\<lambda>p. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))
    1.52    \<circ> (\<circ>) (Fun.swap j k id)) {p \<in> {p. p permutes UNIV}. evenperm p}"
    1.53      unfolding g_S1 by (rule sum.reindex[OF inj_g])
    1.54 -  also have "... = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1"
    1.55 -    unfolding o_def by (rule sum.cong, auto simp add: tjk_eq)
    1.56 -  also have "... = sum (\<lambda>p. - ?f p) ?S1"
    1.57 +  also have "\<dots> = sum (\<lambda>p. of_int (sign (?t_jk \<circ> p)) * (\<Prod>i\<in>UNIV. A $ i $ p i)) ?S1"
    1.58 +    unfolding o_def by (rule sum.cong, auto simp: tjk_eq)
    1.59 +  also have "\<dots> = sum (\<lambda>p. - ?f p) ?S1"
    1.60    proof (rule sum.cong, auto)
    1.61      fix x assume x: "x permutes ?U"
    1.62        and even_x: "evenperm x"
    1.63 @@ -289,14 +289,14 @@
    1.64        = - (of_int (sign x) * (\<Prod>i\<in>UNIV. A $ i $ x i))"
    1.65        by auto
    1.66    qed
    1.67 -  also have "...= - sum ?f ?S1" unfolding sum_negf ..
    1.68 +  also have "\<dots>= - sum ?f ?S1" unfolding sum_negf ..
    1.69    finally have *: "sum ?f ?S2 = - sum ?f ?S1" .
    1.70    have "det A = (\<Sum>p | p permutes UNIV. of_int (sign p) * (\<Prod>i\<in>UNIV. A $ i $ p i))"
    1.71      unfolding det_def ..
    1.72 -  also have "...= sum ?f ?S1 + sum ?f ?S2"
    1.73 +  also have "\<dots>= sum ?f ?S1 + sum ?f ?S2"
    1.74      by (subst PU_decomposition, rule sum.union_disjoint[OF _ _ disjoint], auto)
    1.75 -  also have "...= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto
    1.76 -  also have "...= 0" by simp
    1.77 +  also have "\<dots>= sum ?f ?S1 - sum ?f ?S1 " unfolding * by auto
    1.78 +  also have "\<dots>= 0" by simp
    1.79    finally show "det A = 0" by simp
    1.80  qed
    1.81  
    1.82 @@ -309,7 +309,7 @@
    1.83  lemma det_zero_row:
    1.84    fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
    1.85    shows "row i A = 0 \<Longrightarrow> det A = 0" and "row j F = 0 \<Longrightarrow> det F = 0"
    1.86 -  by (force simp add: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
    1.87 +  by (force simp: row_def det_def vec_eq_iff sign_nz intro!: sum.neutral)+
    1.88  
    1.89  lemma det_zero_column:
    1.90    fixes A :: "'a::{idom, ring_char_0}^'n^'n" and F :: "'b::{field}^'m^'m"
    1.91 @@ -376,7 +376,7 @@
    1.92    have kU: "?U = insert k ?Uk"
    1.93      by blast
    1.94    have eq: "prod (\<lambda>i. ?f i $ p i) ?Uk = prod (\<lambda>i. ?g i $ p i) ?Uk"
    1.95 -    by (auto simp: )
    1.96 +    by auto
    1.97    have Uk: "finite ?Uk" "k \<notin> ?Uk"
    1.98      by auto
    1.99    have "prod (\<lambda>i. ?f i $ p i) ?U = prod (\<lambda>i. ?f i $ p i) (insert k ?Uk)"
   1.100 @@ -475,7 +475,7 @@
   1.101    proof (cases "\<forall>i j. i \<noteq> j \<longrightarrow> row i A \<noteq> row j A")
   1.102      case True
   1.103      with i have "vec.span (rows A - {row i A}) \<subseteq> vec.span {row j A |j. j \<noteq> i}"
   1.104 -      by (auto simp add: rows_def intro!: vec.span_mono)
   1.105 +      by (auto simp: rows_def intro!: vec.span_mono)
   1.106      then have "- row i A \<in> vec.span {row j A|j. j \<noteq> i}"
   1.107        by (meson i subsetCE vec.span_neg)
   1.108      from det_row_span[OF this]
   1.109 @@ -515,17 +515,16 @@
   1.110    have *: "{f. \<forall>i. f i = i} = {id}"
   1.111      by auto
   1.112    show ?case
   1.113 -    by (auto simp add: *)
   1.114 +    by (auto simp: *)
   1.115  next
   1.116    case (Suc k)
   1.117    let ?f = "\<lambda>(y::nat,g) i. if i = Suc k then y else g i"
   1.118    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)})"
   1.119    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)}"
   1.120 -    apply (auto simp add: image_iff)
   1.121 +    apply (auto simp: image_iff)
   1.122      apply (rename_tac f)
   1.123      apply (rule_tac x="f (Suc k)" in bexI)
   1.124 -    apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI)
   1.125 -    apply auto
   1.126 +    apply (rule_tac x = "\<lambda>i. if i = Suc k then i else f i" in exI, auto)
   1.127      done
   1.128    with finite_imageI[OF finite_cartesian_product[OF fS Suc.hyps(1)], of ?f]
   1.129    show ?case
   1.130 @@ -736,7 +735,7 @@
   1.131      by blast
   1.132    have thr0: "- row i A = sum (\<lambda>j. (1/ c i) *s (c j *s row j A)) (?U - {i})"
   1.133      unfolding sum_cmul  using c ci   
   1.134 -    by (auto simp add: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
   1.135 +    by (auto simp: sum.remove[OF fU iU] eq_vector_fraction_iff add_eq_0_iff)
   1.136    have thr: "- row i A \<in> vec.span {row j A| j. j \<noteq> i}"
   1.137      unfolding thr0 by (auto intro: vec.span_base vec.span_scale vec.span_sum)
   1.138    let ?B = "(\<chi> k. if k = i then 0 else row k A) :: 'a^'n^'n"
   1.139 @@ -789,7 +788,7 @@
   1.140    show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> g \<circ> f = id"
   1.141    proof (intro exI conjI)
   1.142      show "Vector_Spaces.linear ( *s) ( *s) (\<lambda>y. B *v y)"
   1.143 -      by (simp add:)
   1.144 +      by simp
   1.145      show "(( *v) B) \<circ> f = id"
   1.146        unfolding o_def
   1.147        by (metis assms 1 eq_id_iff matrix_vector_mul(1) matrix_vector_mul_assoc matrix_vector_mul_lid)
   1.148 @@ -817,7 +816,7 @@
   1.149    show "\<exists>g. Vector_Spaces.linear ( *s) ( *s) g \<and> f \<circ> g = id"
   1.150    proof (intro exI conjI)
   1.151      show "Vector_Spaces.linear ( *s) ( *s) (( *v) B)"
   1.152 -      by (simp add: )
   1.153 +      by simp
   1.154      show "f \<circ> ( *v) B = id"
   1.155        using 1 assms comp_apply eq_id_iff vec.linear_id matrix_id_mat_1 matrix_vector_mul_assoc matrix_works
   1.156        by (metis (no_types, hide_lams))
   1.157 @@ -967,7 +966,7 @@
   1.158  
   1.159  lemma orthogonal_transformation_compose:
   1.160     "\<lbrakk>orthogonal_transformation f; orthogonal_transformation g\<rbrakk> \<Longrightarrow> orthogonal_transformation(f \<circ> g)"
   1.161 -  by (auto simp add: orthogonal_transformation_def linear_compose)
   1.162 +  by (auto simp: orthogonal_transformation_def linear_compose)
   1.163  
   1.164  lemma orthogonal_transformation_neg:
   1.165    "orthogonal_transformation(\<lambda>x. -(f x)) \<longleftrightarrow> orthogonal_transformation f"
   1.166 @@ -1018,8 +1017,7 @@
   1.167    using oA oB
   1.168    unfolding orthogonal_matrix matrix_transpose_mul
   1.169    apply (subst matrix_mul_assoc)
   1.170 -  apply (subst matrix_mul_assoc[symmetric])
   1.171 -  apply (simp add: )
   1.172 +  apply (subst matrix_mul_assoc[symmetric], simp)
   1.173    done
   1.174  
   1.175  lemma orthogonal_transformation_matrix:
   1.176 @@ -1081,8 +1079,7 @@
   1.177      have th0: "x * x - 1 = (x - 1) * (x + 1)"
   1.178        by (simp add: field_simps)
   1.179      have th1: "\<And>(x::'a) y. x = - y \<longleftrightarrow> x + y = 0"
   1.180 -      apply (subst eq_iff_diff_eq_0)
   1.181 -      apply simp
   1.182 +      apply (subst eq_iff_diff_eq_0, simp)
   1.183        done
   1.184      have "x * x = 1 \<longleftrightarrow> x * x - 1 = 0"
   1.185        by simp
   1.186 @@ -1199,7 +1196,7 @@
   1.187  proof -
   1.188    obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
   1.189     and "independent S" "card S = CARD('n)" "span S = UNIV"
   1.190 -    using vector_in_orthonormal_basis assms by (force simp: )
   1.191 +    using vector_in_orthonormal_basis assms by force
   1.192    then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
   1.193      by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
   1.194    then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
   1.195 @@ -1349,7 +1346,7 @@
   1.196          "norm (f (inverse (norm x) *\<^sub>R x) - f (inverse (norm y) *\<^sub>R y)) =
   1.197            norm (inverse (norm x) *\<^sub>R x - inverse (norm y) *\<^sub>R y)"
   1.198          using z
   1.199 -        by (auto simp add: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
   1.200 +        by (auto simp: field_simps intro: f1[rule_format] fd1[rule_format, unfolded dist_norm])
   1.201        from z th0[OF th00] have "dist (?g x) (?g y) = dist x y"
   1.202          by (simp add: dist_norm)
   1.203      }
     2.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Thu May 10 15:41:45 2018 +0100
     2.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Thu May 10 15:59:39 2018 +0100
     2.3 @@ -201,14 +201,14 @@
     2.4  next
     2.5    assume ?rhs then show ?lhs
     2.6      unfolding prod_defs
     2.7 -    by (rule_tac x="0" in exI) (auto simp: )
     2.8 +    by (rule_tac x=0 in exI) auto
     2.9  qed
    2.10  
    2.11  lemma convergent_prod_iff_convergent: 
    2.12    fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
    2.13    assumes "\<And>i. f i \<noteq> 0"
    2.14    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"
    2.15 -  by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI)
    2.16 +  by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)
    2.17  
    2.18  
    2.19  lemma abs_convergent_prod_altdef:
    2.20 @@ -566,7 +566,7 @@
    2.21        by auto
    2.22      then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}"
    2.23        by simp (subst prod.union_disjoint; force)
    2.24 -    also have "... = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
    2.25 +    also have "\<dots> = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
    2.26        by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)
    2.27      finally show ?thesis by metis
    2.28    qed
    2.29 @@ -616,7 +616,7 @@
    2.30      case (elim n)
    2.31      then have "{..n} = {..<N} \<union> {N..n}"
    2.32        by auto
    2.33 -    also have "prod f ... = prod f {..<N} * prod f {N..n}"
    2.34 +    also have "prod f \<dots> = prod f {..<N} * prod f {N..n}"
    2.35        by (intro prod.union_disjoint) auto
    2.36      also from N have "prod f {N..n} = prod g {N..n}"
    2.37        by (intro prod.cong) simp_all
    2.38 @@ -656,7 +656,7 @@
    2.39    have eq: "prod f {..n + Suc (Max N)} = prod f N" for n
    2.40    proof (rule prod.mono_neutral_right)
    2.41      show "N \<subseteq> {..n + Suc (Max N)}"
    2.42 -      by (auto simp add: le_Suc_eq trans_le_add2)
    2.43 +      by (auto simp: le_Suc_eq trans_le_add2)
    2.44      show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1"
    2.45        using f by blast
    2.46    qed auto
    2.47 @@ -687,7 +687,7 @@
    2.48          show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z)) ` {..n + Max N}"
    2.49            using le_Suc_ex by fastforce
    2.50        qed (auto simp: inj_on_def)
    2.51 -      also have "... = ?q"
    2.52 +      also have "\<dots> = ?q"
    2.53          by (rule prod.mono_neutral_right)
    2.54             (use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
    2.55        finally show ?thesis .