section ‹Polynomial coefficients with integer index› text ‹We provide a function to access the coefficients of a polynomial via an integer index. Then index-shifting becomes more convenient, e.g., compare in the lemmas for accessing the coeffiencent of a product with a monomial there is no special case for integer coefficients, whereas for natural number coefficients there is a case-distinction.› theory Coeff_Int imports "HOL-Combinatorics.Permutations" Polynomial_Interpolation.Missing_Polynomial begin definition coeff_int :: "'a :: zero poly ⇒ int ⇒ 'a" where "coeff_int p i = (if i < 0 then 0 else coeff p (nat i))" lemma coeff_int_eq_0: "i < 0 ∨ i > int (degree p) ⟹ coeff_int p i = 0" unfolding coeff_int_def by (cases "i < 0", auto intro: coeff_eq_0) lemma coeff_int_smult[simp]: "coeff_int (smult c p) i = c * coeff_int p i" unfolding coeff_int_def by simp lemma coeff_int_signof_mult: "coeff_int (of_int (sign x) * f) i = of_int (sign x) * coeff_int f i" by (auto simp: coeff_int_def sign_def) lemma coeff_int_sum: "coeff_int (sum p A) i = (∑x∈A. coeff_int (p x) i)" using coeff_sum[of p A "nat i"] unfolding coeff_int_def by (cases "i < 0", auto) lemma coeff_int_0[simp]: "coeff_int f 0 = coeff f 0" unfolding coeff_int_def by simp lemma coeff_int_monom_mult: "coeff_int (monom a d * f) i = (a * coeff_int f (i - d))" proof (cases "i < 0") case True thus ?thesis unfolding coeff_int_def by simp next case False hence "i ≥ 0" by auto then obtain j where i: "i = int j" by (rule nonneg_eq_int) show ?thesis proof (cases "i ≥ d") case True with i have "nat (int j - int d) = j - d" by auto with coeff_monom_mult[of a] show ?thesis unfolding coeff_int_def i by simp next case False thus ?thesis unfolding i by (simp add: coeff_int_def coeff_monom_mult) qed qed lemma coeff_prod_const: assumes "finite xs" and "y ∉ xs" and "⋀ x. x ∈ xs ⟹ degree (f x) = 0" shows "coeff (prod f (insert y xs)) i = prod (λ x. coeff (f x) 0) xs * coeff (f y) i" using assms proof (induct xs rule: finite_induct) case (insert x xs) from insert(2,4) have id: "insert y (insert x xs) - {x} = insert y xs" by auto have "prod f (insert y (insert x xs)) = f x * prod f (insert y xs)" by (subst prod.remove[of _ x], insert insert(1,2) id, auto) hence "coeff (prod f (insert y (insert x xs))) i = coeff (f x * prod f (insert y xs)) i" by simp also have "… = coeff (f x) 0 * (coeff (prod f (insert y xs)) i)" proof - from insert(5)[of x] degree0_coeffs[of "f x"] obtain c where fx: "f x = [: c :]" by auto show ?thesis unfolding fx by auto qed also have "(coeff (prod f (insert y xs)) i) = (∏x∈xs. coeff (f x) 0) * coeff (f y) i" using insert by auto also have "coeff (f x) 0 * … = prod (λ x. coeff (f x) 0) (insert x xs) * coeff (f y) i" by (subst prod.insert_remove, insert insert(1,2,4), auto simp: ac_simps) finally show ?case . qed simp lemma coeff_int_prod_const: assumes "finite xs" and "y ∉ xs" and "⋀ x. x ∈ xs ⟹ degree (f x) = 0" shows "coeff_int (prod f (insert y xs)) i = prod (λ x. coeff_int (f x) 0) xs * coeff_int (f y) i" using coeff_prod_const[OF assms] unfolding coeff_int_def by (cases "i < 0", auto) lemma coeff_int[simp]: "coeff_int p n = coeff p n" unfolding coeff_int_def by auto lemma coeff_int_minus[simp]: "coeff_int (a - b) i = coeff_int a i - coeff_int b i" by (auto simp: coeff_int_def) lemma coeff_int_pCons_0[simp]: "coeff_int (pCons 0 b) i = coeff_int b (i - 1)" by (auto simp: Nitpick.case_nat_unfold coeff_int_def coeff_pCons nat_diff_distrib') end