tidied up Infinite_Products
authorpaulson <lp15@cam.ac.uk>
Thu May 03 18:40:14 2018 +0100 (14 months ago)
changeset 68076315043faa871
parent 68075 262b42b59151
child 68077 ee8c13ae81e9
tidied up Infinite_Products
src/HOL/Analysis/Infinite_Products.thy
     1.1 --- a/src/HOL/Analysis/Infinite_Products.thy	Thu May 03 18:49:10 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Infinite_Products.thy	Thu May 03 18:40:14 2018 +0100
     1.3 @@ -643,22 +643,23 @@
     1.4      let ?q = "prod f {Suc (Max ?Z)..Max N}"
     1.5      have [simp]: "?q \<noteq> 0"
     1.6        using maxge Suc_n_not_le_n le_trans by force
     1.7 -    have eq1: "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + (Max N) + Suc (Max ?Z)}" for n
     1.8 -      apply (rule sym)
     1.9 -      apply (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)"])
    1.10 -        apply (auto simp: )
    1.11 -       apply (simp add: inj_on_def)
    1.12 -      apply (auto simp: image_iff)
    1.13 -      using le_Suc_ex by fastforce
    1.14 -    have eq: "prod f {Suc (Max ?Z)..n + (Max N) + Suc (Max ?Z)} = ?q" for n
    1.15 -      apply (rule prod.mono_neutral_right)
    1.16 -        apply (auto simp: )
    1.17 -      using Max.coboundedI assms(1) f by blast
    1.18 +    have eq: "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = ?q" for n
    1.19 +    proof -
    1.20 +      have "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}" 
    1.21 +      proof (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)", THEN sym])
    1.22 +        show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\<lambda>i. i + Suc (Max ?Z)) ` {..n + Max N}"
    1.23 +          using le_Suc_ex by fastforce
    1.24 +      qed (auto simp: inj_on_def)
    1.25 +      also have "... = ?q"
    1.26 +        by (rule prod.mono_neutral_right)
    1.27 +           (use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
    1.28 +      finally show ?thesis .
    1.29 +    qed
    1.30      have q: "gen_has_prod f (Suc (Max ?Z)) ?q"
    1.31 -      apply (auto simp: gen_has_prod_def)
    1.32 -      apply (rule LIMSEQ_offset[of _ "(Max N)"])
    1.33 -      apply (simp add: eq1 eq atLeast0LessThan del: add_Suc_right)
    1.34 -      done
    1.35 +    proof (simp add: gen_has_prod_def)
    1.36 +      show "(\<lambda>n. \<Prod>i\<le>n. f (Suc (i + Max ?Z))) \<longlonglongrightarrow> ?q"
    1.37 +        by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq)
    1.38 +    qed
    1.39      show ?thesis
    1.40        unfolding has_prod_def
    1.41      proof (intro disjI2 exI conjI)