author paulson Thu, 03 May 2018 18:40:14 +0100 changeset 68076 315043faa871 parent 68075 262b42b59151 child 68077 ee8c13ae81e9
tidied up Infinite_Products
```--- a/src/HOL/Analysis/Infinite_Products.thy	Thu May 03 18:49:10 2018 +0200
+++ b/src/HOL/Analysis/Infinite_Products.thy	Thu May 03 18:40:14 2018 +0100
@@ -643,22 +643,23 @@
let ?q = "prod f {Suc (Max ?Z)..Max N}"
have [simp]: "?q \<noteq> 0"
using maxge Suc_n_not_le_n le_trans by force
-    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
-      apply (rule sym)
-      apply (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)"])
-        apply (auto simp: )
-      apply (auto simp: image_iff)
-      using le_Suc_ex by fastforce
-    have eq: "prod f {Suc (Max ?Z)..n + (Max N) + Suc (Max ?Z)} = ?q" for n
-      apply (rule prod.mono_neutral_right)
-        apply (auto simp: )
-      using Max.coboundedI assms(1) f by blast
+    have eq: "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = ?q" for n
+    proof -
+      have "(\<Prod>i\<le>n + Max N. f (Suc (i + Max ?Z))) = prod f {Suc (Max ?Z)..n + Max N + Suc (Max ?Z)}"
+      proof (rule prod.reindex_cong [where l = "\<lambda>i. i + Suc (Max ?Z)", THEN sym])
+        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"
+        by (rule prod.mono_neutral_right)
+           (use Max.coboundedI [OF \<open>finite N\<close>] f in \<open>force+\<close>)
+      finally show ?thesis .
+    qed
have q: "gen_has_prod f (Suc (Max ?Z)) ?q"
-      apply (auto simp: gen_has_prod_def)
-      apply (rule LIMSEQ_offset[of _ "(Max N)"])