# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1662032916 -3600
# Node ID f3f1cf4711d7088063bcde1f48ffa4c1aa98b705
# Parent  04ce6cf2bd3b77d704eed036a515ca1ebd622a5a
Three new theorems about real polynomial functions

diff -r 04ce6cf2bd3b -r f3f1cf4711d7 src/HOL/Analysis/Weierstrass_Theorems.thy
--- a/src/HOL/Analysis/Weierstrass_Theorems.thy	Mon Aug 29 23:59:47 2022 +0200
+++ b/src/HOL/Analysis/Weierstrass_Theorems.thy	Thu Sep 01 12:48:36 2022 +0100
@@ -853,11 +853,31 @@
   using polynomial_function_diff [of f]
   by (simp add: real_polynomial_function_eq)
 
+lemma real_polynomial_function_divide [intro]:
+  assumes "real_polynomial_function p" shows "real_polynomial_function (\<lambda>x. p x / c)"
+proof -
+  have "real_polynomial_function (\<lambda>x. p x * Fields.inverse c)"
+    using assms by auto
+  then show ?thesis
+    by (simp add: divide_inverse)
+qed
+
 lemma real_polynomial_function_sum [intro]:
     "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> real_polynomial_function (\<lambda>x. f x i)\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. sum (f x) I)"
   using polynomial_function_sum [of I f]
   by (simp add: real_polynomial_function_eq)
 
+lemma real_polynomial_function_prod [intro]:
+  "\<lbrakk>finite I; \<And>i. i \<in> I \<Longrightarrow> real_polynomial_function (\<lambda>x. f x i)\<rbrakk> \<Longrightarrow> real_polynomial_function (\<lambda>x. prod (f x) I)"
+  by (induct I rule: finite_induct) auto
+
+lemma real_polynomial_function_gchoose:
+  obtains p where "real_polynomial_function p" "\<And>x. x gchoose r = p x"
+proof
+  show "real_polynomial_function (\<lambda>x. (\<Prod>i = 0..<r. x - real i) / fact r)"
+    by force
+qed (simp add: gbinomial_prod_rev)
+
 lemma real_polynomial_function_power [intro]:
     "real_polynomial_function f \<Longrightarrow> real_polynomial_function (\<lambda>x. f x^n)"
   by (induct n) (simp_all add: const mult)