Theory Coeff_Int

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