# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1694523288 -3600
# Node ID 3032bc7d613d875b3acacdb842c500b3dfb3c82a
# Parent  123bbc715ec9bf160582ec7686d3e59c383ce2be
A little reorganisation

diff -r 123bbc715ec9 -r 3032bc7d613d src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Mon Sep 11 23:13:23 2023 +0200
+++ b/src/HOL/Set_Interval.thy	Tue Sep 12 13:54:48 2023 +0100
@@ -2228,6 +2228,28 @@
   shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
 using assms by (induct n) (auto simp: le_Suc_eq)
 
+lemma sum_diff_split:
+  fixes f:: "nat \<Rightarrow> 'a::ab_group_add"
+  assumes "m \<le> n"
+  shows "(\<Sum>i\<le>n - m. f(n - i)) = (\<Sum>i\<le>n. f i) - (\<Sum>i<m. f i)"
+proof -
+  have inj: "inj_on ((-) n) {m..n}"
+    by (auto simp: inj_on_def)
+  have "(\<Sum>i\<le>n - m. f(n - i)) = (\<Sum>i\<in>(-) n ` {m..n}. f(n - i))"
+  proof (rule sum.cong)
+    have "\<And>x. x \<le> n - m \<Longrightarrow> \<exists>k\<ge>m. k \<le> n \<and> x = n - k"
+      by (metis assms diff_diff_cancel diff_le_mono2 diff_le_self le_trans)
+    then show "{..n - m} = (-) n ` {m..n}"
+      by (auto simp: image_iff Bex_def)
+  qed auto
+  also have "\<dots> = (\<Sum>i=m..n. f i)"
+    by (simp add: sum.reindex_cong [OF inj])
+  also have "\<dots> = (\<Sum>i\<le>n. f i) - (\<Sum>i<m. f i)"
+    using sum_diff_nat_ivl[of 0 "m" "Suc n" f] assms 
+    by (simp only: atLeast0AtMost atLeast0LessThan atLeastLessThanSuc_atLeastAtMost)
+  finally show ?thesis .
+qed
+
 
 subsubsection \<open>Telescoping\<close>
 
@@ -2626,4 +2648,45 @@
 
 (* TODO: Add support for folding over more kinds of intervals here *)
 
+lemma pairs_le_eq_Sigma: "{(i, j). i + j \<le> m} = Sigma (atMost m) (\<lambda>r. atMost (m - r))"
+  for m :: nat
+  by auto
+
+lemma sum_up_index_split: "(\<Sum>k\<le>m + n. f k) = (\<Sum>k\<le>m. f k) + (\<Sum>k = Suc m..m + n. f k)"
+  by (metis atLeast0AtMost Suc_eq_plus1 le0 sum.ub_add_nat)
+
+lemma Sigma_interval_disjoint: "(SIGMA i:A. {..v i}) \<inter> (SIGMA i:A.{v i<..w}) = {}"
+  for w :: "'a::order"
+  by auto
+
+lemma product_atMost_eq_Un: "A \<times> {..m} = (SIGMA i:A.{..m - i}) \<union> (SIGMA i:A.{m - i<..m})"
+  for m :: nat
+  by auto
+
+lemma polynomial_product: (*with thanks to Chaitanya Mangla*)
+  fixes x :: "'a::idom"
+  assumes m: "\<And>i. i > m \<Longrightarrow> a i = 0"
+    and n: "\<And>j. j > n \<Longrightarrow> b j = 0"
+  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) =
+         (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+proof -
+  have "\<And>i j. \<lbrakk>m + n - i < j; a i \<noteq> 0\<rbrakk> \<Longrightarrow> b j = 0"
+    by (meson le_add_diff leI le_less_trans m n)
+  then have \<section>: "(\<Sum>(i,j)\<in>(SIGMA i:{..m+n}. {m+n - i<..m+n}). a i * x ^ i * (b j * x ^ j)) = 0"
+    by (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral)
+  have "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = (\<Sum>i\<le>m. \<Sum>j\<le>n. (a i * x ^ i) * (b j * x ^ j))"
+    by (rule sum_product)
+  also have "\<dots> = (\<Sum>i\<le>m + n. \<Sum>j\<le>n + m. a i * x ^ i * (b j * x ^ j))"
+    using assms by (auto simp: sum_up_index_split)
+  also have "\<dots> = (\<Sum>r\<le>m + n. \<Sum>j\<le>m + n - r. a r * x ^ r * (b j * x ^ j))"
+    by (simp add: add_ac sum.Sigma product_atMost_eq_Un sum_Un Sigma_interval_disjoint \<section>)
+  also have "\<dots> = (\<Sum>(i,j)\<in>{(i,j). i+j \<le> m+n}. (a i * x ^ i) * (b j * x ^ j))"
+    by (auto simp: pairs_le_eq_Sigma sum.Sigma)
+  also have "... = (\<Sum>k\<le>m + n. \<Sum>i\<le>k. a i * x ^ i * (b (k - i) * x ^ (k - i)))"
+    by (rule sum.triangle_reindex_eq)
+  also have "\<dots> = (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
+    by (auto simp: algebra_simps sum_distrib_left simp flip: power_add intro!: sum.cong)
+  finally show ?thesis .
+qed
+
 end
diff -r 123bbc715ec9 -r 3032bc7d613d src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Mon Sep 11 23:13:23 2023 +0200
+++ b/src/HOL/Transcendental.thy	Tue Sep 12 13:54:48 2023 +0100
@@ -6241,51 +6241,10 @@
 
 subsection \<open>Basics about polynomial functions: products, extremal behaviour and root counts\<close>
 
-lemma pairs_le_eq_Sigma: "{(i, j). i + j \<le> m} = Sigma (atMost m) (\<lambda>r. atMost (m - r))"
-  for m :: nat
-  by auto
-
-lemma sum_up_index_split: "(\<Sum>k\<le>m + n. f k) = (\<Sum>k\<le>m. f k) + (\<Sum>k = Suc m..m + n. f k)"
-  by (metis atLeast0AtMost Suc_eq_plus1 le0 sum.ub_add_nat)
-
-lemma Sigma_interval_disjoint: "(SIGMA i:A. {..v i}) \<inter> (SIGMA i:A.{v i<..w}) = {}"
-  for w :: "'a::order"
-  by auto
-
-lemma product_atMost_eq_Un: "A \<times> {..m} = (SIGMA i:A.{..m - i}) \<union> (SIGMA i:A.{m - i<..m})"
-  for m :: nat
-  by auto
-
-lemma polynomial_product: (*with thanks to Chaitanya Mangla*)
-  fixes x :: "'a::idom"
-  assumes m: "\<And>i. i > m \<Longrightarrow> a i = 0"
-    and n: "\<And>j. j > n \<Longrightarrow> b j = 0"
-  shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) =
-         (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
-proof -
-  have "\<And>i j. \<lbrakk>m + n - i < j; a i \<noteq> 0\<rbrakk> \<Longrightarrow> b j = 0"
-    by (meson le_add_diff leI le_less_trans m n)
-  then have \<section>: "(\<Sum>(i,j)\<in>(SIGMA i:{..m+n}. {m+n - i<..m+n}). a i * x ^ i * (b j * x ^ j)) = 0"
-    by (clarsimp simp add: sum_Un Sigma_interval_disjoint intro!: sum.neutral)
-  have "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) = (\<Sum>i\<le>m. \<Sum>j\<le>n. (a i * x ^ i) * (b j * x ^ j))"
-    by (rule sum_product)
-  also have "\<dots> = (\<Sum>i\<le>m + n. \<Sum>j\<le>n + m. a i * x ^ i * (b j * x ^ j))"
-    using assms by (auto simp: sum_up_index_split)
-  also have "\<dots> = (\<Sum>r\<le>m + n. \<Sum>j\<le>m + n - r. a r * x ^ r * (b j * x ^ j))"
-    by (simp add: add_ac sum.Sigma product_atMost_eq_Un sum_Un Sigma_interval_disjoint \<section>)
-  also have "\<dots> = (\<Sum>(i,j)\<in>{(i,j). i+j \<le> m+n}. (a i * x ^ i) * (b j * x ^ j))"
-    by (auto simp: pairs_le_eq_Sigma sum.Sigma)
-  also have "... = (\<Sum>k\<le>m + n. \<Sum>i\<le>k. a i * x ^ i * (b (k - i) * x ^ (k - i)))"
-    by (rule sum.triangle_reindex_eq)
-  also have "\<dots> = (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
-    by (auto simp: algebra_simps sum_distrib_left simp flip: power_add intro!: sum.cong)
-  finally show ?thesis .
-qed
-
 lemma polynomial_product_nat:
   fixes x :: nat
-  assumes m: "\<And>i. i > m \<Longrightarrow> a i = 0"
-    and n: "\<And>j. j > n \<Longrightarrow> b j = 0"
+  assumes m: "\<And>i. i > m \<Longrightarrow> int (a i) = 0"
+    and n: "\<And>j. j > n \<Longrightarrow> int (b j) = 0"
   shows "(\<Sum>i\<le>m. (a i) * x ^ i) * (\<Sum>j\<le>n. (b j) * x ^ j) =
          (\<Sum>r\<le>m + n. (\<Sum>k\<le>r. (a k) * (b (r - k))) * x ^ r)"
   using polynomial_product [of m a n b x] assms