# HG changeset patch # User paulson # Date 1525369214 -3600 # Node ID 315043faa871eff105e9dd7b79808fe374b29d49 # Parent 262b42b5915130e6bb8553769abcabfd9a63db7a tidied up Infinite_Products diff -r 262b42b59151 -r 315043faa871 src/HOL/Analysis/Infinite_Products.thy --- 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 \ 0" using maxge Suc_n_not_le_n le_trans by force - have eq1: "(\i\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 = "\i. i + Suc (Max ?Z)"]) - apply (auto simp: ) - apply (simp add: inj_on_def) - 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: "(\i\n + Max N. f (Suc (i + Max ?Z))) = ?q" for n + proof - + have "(\i\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 = "\i. i + Suc (Max ?Z)", THEN sym]) + show "{Suc (Max ?Z)..n + Max N + Suc (Max ?Z)} = (\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 \finite N\] f in \force+\) + 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)"]) - apply (simp add: eq1 eq atLeast0LessThan del: add_Suc_right) - done + proof (simp add: gen_has_prod_def) + show "(\n. \i\n. f (Suc (i + Max ?Z))) \ ?q" + by (rule LIMSEQ_offset[of _ "(Max N)"]) (simp add: eq) + qed show ?thesis unfolding has_prod_def proof (intro disjI2 exI conjI)