Theory Linear_Recurrences.Linear_Recurrences_Misc

(*
  File:    Linear_Recurrences_Misc.thy
  Author:  Manuel Eberl, TU München
*)
section ‹Miscellaneous material required for linear recurrences›
theory Linear_Recurrences_Misc
imports 
  Complex_Main
  "HOL-Computational_Algebra.Computational_Algebra"
  "HOL-Computational_Algebra.Polynomial_Factorial"
begin

fun zip_with where
  "zip_with f (x#xs) (y#ys) = f x y # zip_with f xs ys"
| "zip_with f _ _ = []"

lemma length_zip_with [simp]: "length (zip_with f xs ys) = min (length xs) (length ys)"
  by (induction f xs ys rule: zip_with.induct) simp_all

lemma zip_with_altdef: "zip_with f xs ys = map (λ(x,y). f x y) (zip xs ys)"
  by (induction f xs ys rule: zip_with.induct) simp_all
  
lemma zip_with_nth [simp]:
  "n < length xs  n < length ys  zip_with f xs ys ! n = f (xs!n) (ys!n)"
  by (simp add: zip_with_altdef)

lemma take_zip_with: "take n (zip_with f xs ys) = zip_with f (take n xs) (take n ys)"
proof (induction f xs ys arbitrary: n rule: zip_with.induct)
  case (1 f x xs y ys n)
  thus ?case by (cases n) simp_all
qed simp_all

lemma drop_zip_with: "drop n (zip_with f xs ys) = zip_with f (drop n xs) (drop n ys)"
proof (induction f xs ys arbitrary: n rule: zip_with.induct)
  case (1 f x xs y ys n)
  thus ?case by (cases n) simp_all
qed simp_all

lemma map_zip_with: "map f (zip_with g xs ys) = zip_with (λx y. f (g x y)) xs ys"
  by (induction g xs ys rule: zip_with.induct) simp_all

lemma zip_with_map: "zip_with f (map g xs) (map h ys) = zip_with (λx y. f (g x) (h y)) xs ys"
  by (induction "λx y. f (g x) (h y)" xs ys rule: zip_with.induct) simp_all

lemma zip_with_map_left: "zip_with f (map g xs) ys = zip_with (λx y. f (g x) y) xs ys"
  using zip_with_map[of f g xs "λx. x" ys] by simp

lemma zip_with_map_right: "zip_with f xs (map g ys) = zip_with (λx y. f x (g y)) xs ys"
  using zip_with_map[of f "λx. x" xs g ys] by simp

lemma zip_with_swap: "zip_with (λx y. f y x) xs ys = zip_with f ys xs"
  by (induction f ys xs rule: zip_with.induct) simp_all

lemma set_zip_with: "set (zip_with f xs ys) = (λ(x,y). f x y) ` set (zip xs ys)"
  by (induction f xs ys rule: zip_with.induct) simp_all

lemma zip_with_Pair: "zip_with Pair (xs :: 'a list) (ys :: 'b list) = zip xs ys"
  by (induction "Pair :: 'a  'b  _" xs ys rule: zip_with.induct) simp_all

lemma zip_with_altdef': 
    "zip_with f xs ys = [f (xs!i) (ys!i). i  [0..<min (length xs) (length ys)]]"
  by (induction f xs ys rule: zip_with.induct) (simp_all add: map_upt_Suc del: upt_Suc)

lemma zip_altdef: "zip xs ys = [(xs!i, ys!i). i  [0..<min (length xs) (length ys)]]"
  by (simp add: zip_with_Pair [symmetric] zip_with_altdef')



lemma card_poly_roots_bound:
  fixes p :: "'a::{comm_ring_1,ring_no_zero_divisors} poly"
  assumes "p  0"
  shows   "card {x. poly p x = 0}  degree p"
using assms
proof (induction "degree p" arbitrary: p rule: less_induct)
  case (less p)
  show ?case
  proof (cases "x. poly p x = 0")
    case False
    hence "{x. poly p x = 0} = {}" by blast
    thus ?thesis by simp
  next
    case True
    then obtain x where x: "poly p x = 0" by blast
    hence "[:-x, 1:] dvd p" by (subst (asm) poly_eq_0_iff_dvd)
    then obtain q where q: "p = [:-x, 1:] * q" by (auto simp: dvd_def)
    with p  0 have [simp]: "q  0" by auto
    have deg: "degree p = Suc (degree q)"
      by (subst q, subst degree_mult_eq) auto
    have "card {x. poly p x = 0}  card (insert x {x. poly q x = 0})"
      by (intro card_mono) (auto intro: poly_roots_finite simp: q)
    also have "  Suc (card {x. poly q x = 0})"
      by (rule card_insert_le_m1) auto
    also from deg have  "card {x. poly q x = 0}  degree q"
      using p  0 and q by (intro less) auto
    also have "Suc  = degree p" by (simp add: deg)
    finally show ?thesis by - simp_all
  qed
qed

lemma poly_eqI_degree:
  fixes p q :: "'a :: {comm_ring_1, ring_no_zero_divisors} poly"
  assumes "x. x  A  poly p x = poly q x"
  assumes "card A > degree p" "card A > degree q"
  shows   "p = q"
proof (rule ccontr)
  assume neq: "p  q"
  have "degree (p - q)  max (degree p) (degree q)"
    by (rule degree_diff_le_max)
  also from assms have " < card A" by linarith
  also have "  card {x. poly (p - q) x = 0}"
    using neq and assms by (intro card_mono poly_roots_finite) auto
  finally have "degree (p - q) < card {x. poly (p - q) x = 0}" .
  moreover have "degree (p - q)  card {x. poly (p - q) x = 0}"
    using neq by (intro card_poly_roots_bound) auto
  ultimately show False by linarith
qed  

lemma poly_root_order_induct [case_names 0 no_roots root]:
  fixes p :: "'a :: idom poly"
  assumes "P 0" "p. (x. poly p x  0)  P p" 
          "p x n. n > 0  poly p x  0  P p  P ([:-x, 1:] ^ n * p)"
  shows   "P p"
proof (induction "degree p" arbitrary: p rule: less_induct)
  case (less p)
  consider "p = 0" | "p  0" "x. poly p x = 0" | "x. poly p x  0" by blast
  thus ?case
  proof cases
    case 3
    with assms(2)[of p] show ?thesis by simp
  next
    case 2
    then obtain x where x: "poly p x = 0" by auto
    have "[:-x, 1:] ^ order x p dvd p" by (intro order_1)
    then obtain q where q: "p = [:-x, 1:] ^ order x p * q" by (auto simp: dvd_def)
    with 2 have [simp]: "q  0" by auto
    have order_pos: "order x p > 0"
      using p  0 and x by (auto simp: order_root)
    have "order x p = order x p + order x q"
      by (subst q, subst order_mult) (auto simp: order_power_n_n)
    hence [simp]: "order x q = 0" by simp
    have deg: "degree p = order x p + degree q"
      by (subst q, subst degree_mult_eq) (auto simp: degree_power_eq)
    with order_pos have "degree q < degree p" by simp
    hence "P q" by (rule less)
    with order_pos have "P ([:-x, 1:] ^ order x p * q)"
      by (intro assms(3)) (auto simp: order_root)
    with q show ?thesis by simp
  qed (simp_all add: assms(1))
qed

lemma complex_poly_decompose:
  "smult (lead_coeff p) (z|poly p z = 0. [:-z, 1:] ^ order z p) = (p :: complex poly)"
proof (induction p rule: poly_root_order_induct)
  case (no_roots p)
  show ?case
  proof (cases "degree p = 0")
    case False
    hence "¬constant (poly p)" by (subst constant_degree)
    with fundamental_theorem_of_algebra and no_roots show ?thesis by blast
  qed (auto elim!: degree_eq_zeroE)
next
  case (root p x n)
  from root have *: "{z. poly ([:- x, 1:] ^ n * p) z = 0} = insert x {z. poly p z = 0}"
    by auto
  have "smult (lead_coeff ([:-x, 1:] ^ n * p)) 
           (z|poly ([:-x,1:] ^ n * p) z = 0. [:-z, 1:] ^ order z ([:- x, 1:] ^ n * p)) = 
        [:- x, 1:] ^ order x ([:- x, 1:] ^ n * p) * 
          smult (lead_coeff p) (z{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p))"
    by (subst *, subst prod.insert) 
       (insert root, auto intro: poly_roots_finite simp: mult_ac lead_coeff_mult lead_coeff_power)
  also have "order x ([:- x, 1:] ^ n * p) = n"
    using root by (subst order_mult) (auto simp: order_power_n_n order_0I)
  also have "(z{z. poly p z = 0}. [:- z, 1:] ^ order z ([:- x, 1:] ^ n * p)) =
               (z{z. poly p z = 0}. [:- z, 1:] ^ order z p)"
  proof (intro prod.cong refl, goal_cases)
    case (1 y)
    with root have "order y ([:-x,1:] ^ n) = 0" by (intro order_0I) auto 
    thus ?case using root by (subst order_mult) auto
  qed
  also note root.IH
  finally show ?case .
qed simp_all


lemma normalize_field: 
  "normalize (x :: 'a :: {normalization_semidom,field}) = (if x = 0 then 0 else 1)"
  by (auto simp: normalize_1_iff dvd_field_iff)

lemma unit_factor_field [simp]:
  "unit_factor (x :: 'a :: {normalization_semidom,field}) = x"
  using unit_factor_mult_normalize[of x] normalize_field[of x]
  by (simp split: if_splits)

lemma coprime_linear_poly: 
  fixes c :: "'a :: field_gcd"
  assumes "c  c'"
  shows   "coprime [:c,1:] [:c',1:]"
proof -
  have "gcd [:c,1:] [:c',1:] = gcd ([:c,1:] - [:c',1:]) [:c',1:]"
    by (rule gcd_diff1 [symmetric])
  also have "[:c,1:] - [:c',1:] = [:c-c':]" by simp
  also from assms have "gcd  [:c',1:] = normalize [:c-c':]"
    by (intro gcd_proj1_if_dvd) (auto simp: const_poly_dvd_iff dvd_field_iff)
  also from assms have " = 1" by (simp add: normalize_poly_def)
  finally show "coprime [:c,1:] [:c',1:]"
    by (simp add: gcd_eq_1_imp_coprime)
qed

lemma coprime_linear_poly': 
  fixes c :: "'a :: field_gcd"
  assumes "c  c'" "c  0" "c'  0"
  shows   "coprime [:1,c:] [:1,c':]"
proof -
  have "gcd [:1,c:] [:1,c':] = gcd ([:1,c:] mod [:1,c':]) [:1,c':]"
    by simp
  also have [:1,c:] mod [:1,c':] = [:1 - c / c':]
    using c'  0 by (simp add: mod_pCons)
  also from assms have "gcd  [:1,c':] = normalize ([:1 - c / c':])"
    by (intro gcd_proj1_if_dvd) (auto simp: const_poly_dvd_iff dvd_field_iff)
  also from assms have " = 1" by (auto simp: normalize_poly_def)
  finally show ?thesis
    by (rule gcd_eq_1_imp_coprime)
qed

end