src/HOL/Analysis/Infinite_Products.thy
changeset 68138 c738f40e88d4
parent 68136 f022083489d0
child 68361 20375f232f3b
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Thu May 10 15:41:45 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Thu May 10 15:59:39 2018 +0100
     1.3 @@ -201,14 +201,14 @@
     1.4  next
     1.5    assume ?rhs then show ?lhs
     1.6      unfolding prod_defs
     1.7 -    by (rule_tac x="0" in exI) (auto simp: )
     1.8 +    by (rule_tac x=0 in exI) auto
     1.9  qed
    1.10  
    1.11  lemma convergent_prod_iff_convergent: 
    1.12    fixes f :: "nat \<Rightarrow> 'a :: {topological_semigroup_mult,t2_space,idom}"
    1.13    assumes "\<And>i. f i \<noteq> 0"
    1.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"
    1.15 -  by (force simp add: convergent_prod_iff_nz_lim assms convergent_def limI)
    1.16 +  by (force simp: convergent_prod_iff_nz_lim assms convergent_def limI)
    1.17  
    1.18  
    1.19  lemma abs_convergent_prod_altdef:
    1.20 @@ -566,7 +566,7 @@
    1.21        by auto
    1.22      then have "prod f {..n+M} = prod f {..<M} * prod f {M..n+M}"
    1.23        by simp (subst prod.union_disjoint; force)
    1.24 -    also have "... = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
    1.25 +    also have "\<dots> = prod f {..<M} * (\<Prod>i\<le>n. f (i + M))"
    1.26        by (metis (mono_tags, lifting) add.left_neutral atMost_atLeast0 prod_shift_bounds_cl_nat_ivl)
    1.27      finally show ?thesis by metis
    1.28    qed
    1.29 @@ -616,7 +616,7 @@
    1.30      case (elim n)
    1.31      then have "{..n} = {..<N} \<union> {N..n}"
    1.32        by auto
    1.33 -    also have "prod f ... = prod f {..<N} * prod f {N..n}"
    1.34 +    also have "prod f \<dots> = prod f {..<N} * prod f {N..n}"
    1.35        by (intro prod.union_disjoint) auto
    1.36      also from N have "prod f {N..n} = prod g {N..n}"
    1.37        by (intro prod.cong) simp_all
    1.38 @@ -656,7 +656,7 @@
    1.39    have eq: "prod f {..n + Suc (Max N)} = prod f N" for n
    1.40    proof (rule prod.mono_neutral_right)
    1.41      show "N \<subseteq> {..n + Suc (Max N)}"
    1.42 -      by (auto simp add: le_Suc_eq trans_le_add2)
    1.43 +      by (auto simp: le_Suc_eq trans_le_add2)
    1.44      show "\<forall>i\<in>{..n + Suc (Max N)} - N. f i = 1"
    1.45        using f by blast
    1.46    qed auto
    1.47 @@ -687,7 +687,7 @@
    1.48          show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z)) ` {..n + Max N}"
    1.49            using le_Suc_ex by fastforce
    1.50        qed (auto simp: inj_on_def)
    1.51 -      also have "... = ?q"
    1.52 +      also have "\<dots> = ?q"
    1.53          by (rule prod.mono_neutral_right)
    1.54             (use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
    1.55        finally show ?thesis .