Quelle Polynomial.thy Sprache: Isabelle

(*  Title:      HOL/Computational_Algebra/Polynomial.thy
    Author:     Brian Huffman
    Author:     Clemens Ballarin
    Author:     Amine Chaieb
    Author:     Florian Haftmann
*)

section \<open>Polynomials as type over a ring structure\<close>

theory Polynomial
imports
  Complex_Main
  "HOL-Library.More_List"
  "HOL-Library.Infinite_Set"
  Primes
begin

context semidom_modulo
begin

lemma not_dvd_imp_mod_neq_0:
  \<open>a mod b \<noteq> 0\<close> if \<open>\<not> b dvd a\<close>
  using that mod_0_imp_dvd [of a b] by blast

end

subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>

definition cCons :: "'a::zero \ 'a list \ 'a list" (infixr \##\ 65)
  where "x ## xs = (if xs = [] \ x = 0 then [] else x # xs)"

lemma cCons_0_Nil_eq [simp]: "0 ## [] = []"
  by (simp add: cCons_def)

lemma cCons_Cons_eq [simp]: "x ## y # ys = x # y # ys"
  by (simp add: cCons_def)

lemma cCons_append_Cons_eq [simp]: "x ## xs @ y # ys = x # xs @ y # ys"
  by (simp add: cCons_def)

lemma cCons_not_0_eq [simp]: "x \ 0 \ x ## xs = x # xs"
  by (simp add: cCons_def)

lemma strip_while_not_0_Cons_eq [simp]:
  "strip_while (\x. x = 0) (x # xs) = x ## strip_while (\x. x = 0) xs"
proof (cases "x = 0")
  case False
  then show ?thesis by simp
next
  case True
  show ?thesis
  proof (induct xs rule: rev_induct)
    case Nil
    with True show ?case by simp
  next
    case (snoc y ys)
    then show ?case
      by (cases "y = 0") (simp_all add: append_Cons [symmetric] del: append_Cons)
  qed
qed

lemma tl_cCons [simp]: "tl (x ## xs) = xs"
  by (simp add: cCons_def)

subsection \<open>Definition of type \<open>poly\<close>\<close>

typedef (overloaded) 'a poly = "{f :: nat \ 'a::zero. \\<^sub>\ n. f n = 0}"
  morphisms coeff Abs_poly
  by (auto intro!: ALL_MOST)

setup_lifting type_definition_poly

lemma poly_eq_iff: "p = q \ (\n. coeff p n = coeff q n)"
  by (simp add: coeff_inject [symmetric] fun_eq_iff)

lemma poly_eqI: "(\n. coeff p n = coeff q n) \ p = q"
  by (simp add: poly_eq_iff)

lemma MOST_coeff_eq_0: "\\<^sub>\ n. coeff p n = 0"
  using coeff [of p] by simp

lemma coeff_Abs_poly:
  assumes "\i. i > n \ f i = 0"
  shows   "coeff (Abs_poly f) = f"
proof (rule Abs_poly_inverse, clarify)
  have "eventually (\i. i > n) cofinite"
    by (auto simp: MOST_nat)
  thus "eventually (\i. f i = 0) cofinite"
    by eventually_elim (use assms in auto)
qed

subsection \<open>Degree of a polynomial\<close>

definition degree :: "'a::zero poly \ nat"
  where "degree p = (LEAST n. \i>n. coeff p i = 0)"

lemma degree_cong:
  assumes "\i. coeff p i = 0 \ coeff q i = 0"
  shows   "degree p = degree q"
proof -
  have "(\n. \i>n. poly.coeff p i = 0) = (\n. \i>n. poly.coeff q i = 0)"
    using assms by (auto simp: fun_eq_iff)
  thus ?thesis
    by (simp only: degree_def)
qed

lemma coeff_Abs_poly_If_le:
  "coeff (Abs_poly (\i. if i \ n then f i else 0)) = (\i. if i \ n then f i else 0)"
proof (rule Abs_poly_inverse, clarify)
  have "eventually (\i. i > n) cofinite"
    by (auto simp: MOST_nat)
  thus "eventually (\i. (if i \ n then f i else 0) = 0) cofinite"
    by eventually_elim auto
qed

lemma coeff_eq_0:
  assumes "degree p < n"
  shows "coeff p n = 0"
proof -
  have "\n. \i>n. coeff p i = 0"
    using MOST_coeff_eq_0 by (simp add: MOST_nat)
  then have "\i>degree p. coeff p i = 0"
    unfolding degree_def by (rule LeastI_ex)
  with assms show ?thesis by simp
qed

lemma le_degree: "coeff p n \ 0 \ n \ degree p"
  using coeff_eq_0 linorder_le_less_linear by blast

lemma degree_le: "\i>n. coeff p i = 0 \ degree p \ n"
  unfolding degree_def by (erule Least_le)

lemma less_degree_imp: "n < degree p \ \i>n. coeff p i \ 0"
  unfolding degree_def by (drule not_less_Least, simp)

lemma poly_eqI2:
  assumes "degree p = degree q" and "\i. i \ degree p \ coeff p i = coeff q i"
  shows "p = q"
  by (metis assms le_degree poly_eqI)

subsection \<open>The zero polynomial\<close>

instantiation poly :: (zero) zero
begin

lift_definition zero_poly :: "'a poly"
  is "\_. 0"
  by (rule MOST_I) simp

instance ..

end

lemma coeff_0 [simp]: "coeff 0 n = 0"
  by transfer rule

lemma degree_0 [simp]: "degree 0 = 0"
  by (rule order_antisym [OF degree_le le0]) simp

lemma leading_coeff_neq_0:
  assumes "p \ 0"
  shows "coeff p (degree p) \ 0"
proof (cases "degree p")
  case 0
  from \<open>p \<noteq> 0\<close> obtain n where "coeff p n \<noteq> 0"
    by (auto simp add: poly_eq_iff)
  then have "n \ degree p"
    by (rule le_degree)
  with \<open>coeff p n \<noteq> 0\<close> and \<open>degree p = 0\<close> show "coeff p (degree p) \<noteq> 0"
    by simp
next
  case (Suc n)
  from \<open>degree p = Suc n\<close> have "n < degree p"
    by simp
  then have "\i>n. coeff p i \ 0"
    by (rule less_degree_imp)
  then obtain i where "n < i" and "coeff p i \ 0"
    by blast
  from \<open>degree p = Suc n\<close> and \<open>n < i\<close> have "degree p \<le> i"
    by simp
  also from \<open>coeff p i \<noteq> 0\<close> have "i \<le> degree p"
    by (rule le_degree)
  finally have "degree p = i" .
  with \<open>coeff p i \<noteq> 0\<close> show "coeff p (degree p) \<noteq> 0" by simp
qed

lemma leading_coeff_0_iff [simp]: "coeff p (degree p) = 0 \ p = 0"
  by (cases "p = 0") (simp_all add: leading_coeff_neq_0)

lemma degree_lessI:
  assumes "p \ 0 \ n > 0" "\k\n. coeff p k = 0"
  shows   "degree p < n"
proof (cases "p = 0")
  case False
  show ?thesis
  proof (rule ccontr)
    assume *: "\(degree p < n)"
    define d where "d = degree p"
    from \<open>p \<noteq> 0\<close> have "coeff p d \<noteq> 0"
      by (auto simp: d_def)
    moreover have "coeff p d = 0"
      using assms(2) * by (auto simp: not_less)
    ultimately show False by contradiction
  qed
qed (use assms in auto)

lemma eq_zero_or_degree_less:
  assumes "degree p \ n" and "coeff p n = 0"
  shows "p = 0 \ degree p < n"
proof (cases n)
  case 0
  with \<open>degree p \<le> n\<close> and \<open>coeff p n = 0\<close> have "coeff p (degree p) = 0"
    by simp
  then have "p = 0" by simp
  then show ?thesis ..
next
  case (Suc m)
  from \<open>degree p \<le> n\<close> have "\<forall>i>n. coeff p i = 0"
    by (simp add: coeff_eq_0)
  with \<open>coeff p n = 0\<close> have "\<forall>i\<ge>n. coeff p i = 0"
    by (simp add: le_less)
  with \<open>n = Suc m\<close> have "\<forall>i>m. coeff p i = 0"
    by (simp add: less_eq_Suc_le)
  then have "degree p \ m"
    by (rule degree_le)
  with \<open>n = Suc m\<close> have "degree p < n"
    by (simp add: less_Suc_eq_le)
  then show ?thesis ..
qed

lemma coeff_0_degree_minus_1: "coeff rrr dr = 0 \ degree rrr \ dr \ degree rrr \ dr - 1"
  using eq_zero_or_degree_less by fastforce

subsection \<open>List-style constructor for polynomials\<close>

lift_definition pCons :: "'a::zero \ 'a poly \ 'a poly"
  is "\a p. case_nat a (coeff p)"
  by (rule MOST_SucD) (simp add: MOST_coeff_eq_0)

lemmas coeff_pCons = pCons.rep_eq

lemma coeff_pCons': "poly.coeff (pCons c p) n = (if n = 0 then c else poly.coeff p (n - 1))"
  by transfer'(auto split: nat.splits)

lemma coeff_pCons_0 [simp]: "coeff (pCons a p) 0 = a"
  by transfer simp

lemma coeff_pCons_Suc [simp]: "coeff (pCons a p) (Suc n) = coeff p n"
  by (simp add: coeff_pCons)

lemma degree_pCons_le: "degree (pCons a p) \ Suc (degree p)"
  by (rule degree_le) (simp add: coeff_eq_0 coeff_pCons split: nat.split)

lemma degree_pCons_eq: "p \ 0 \ degree (pCons a p) = Suc (degree p)"
  by (simp add: degree_pCons_le le_antisym le_degree)

lemma degree_pCons_0: "degree (pCons a 0) = 0"
proof -
  have "degree (pCons a 0) \ Suc 0"
    by (metis (no_types) degree_0 degree_pCons_le)
  then show ?thesis
    by (metis coeff_0 coeff_pCons_Suc degree_0 eq_zero_or_degree_less less_Suc0)
qed

lemma degree_pCons_eq_if [simp]: "degree (pCons a p) = (if p = 0 then 0 else Suc (degree p))"
  by (simp add: degree_pCons_0 degree_pCons_eq)

lemma pCons_0_0 [simp]: "pCons 0 0 = 0"
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)

lemma pCons_eq_iff [simp]: "pCons a p = pCons b q \ a = b \ p = q"
proof safe
  assume "pCons a p = pCons b q"
  then have "coeff (pCons a p) 0 = coeff (pCons b q) 0"
    by simp
  then show "a = b"
    by simp
next
  assume "pCons a p = pCons b q"
  then have "coeff (pCons a p) (Suc n) = coeff (pCons b q) (Suc n)" for n
    by simp
  then show "p = q"
    by (simp add: poly_eq_iff)
qed

lemma pCons_eq_0_iff [simp]: "pCons a p = 0 \ a = 0 \ p = 0"
  using pCons_eq_iff [of a p 0 0] by simp

lemma pCons_cases [cases type: poly]:
  obtains (pCons) a q where "p = pCons a q"
proof
  show "p = pCons (coeff p 0) (Abs_poly (\n. coeff p (Suc n)))"
    by transfer
      (simp_all add: MOST_inj[where f=Suc and P="\n. p n = 0" for p] fun_eq_iff Abs_poly_inverse
        split: nat.split)
qed

lemma pCons_induct [case_names 0 pCons, induct type: poly]:
  assumes zero: "P 0"
  assumes pCons: "\a p. a \ 0 \ p \ 0 \ P p \ P (pCons a p)"
  shows "P p"
proof (induct p rule: measure_induct_rule [where f=degree])
  case (less p)
  obtain a q where "p = pCons a q" by (rule pCons_cases)
  have "P q"
  proof (cases "q = 0")
    case True
    then show "P q" by (simp add: zero)
  next
    case False
    then have "degree (pCons a q) = Suc (degree q)"
      by (rule degree_pCons_eq)
    with \<open>p = pCons a q\<close> have "degree q < degree p"
      by simp
    then show "P q"
      by (rule less.hyps)
  qed
  have "P (pCons a q)"
  proof (cases "a \ 0 \ q \ 0")
    case True
    with \<open>P q\<close> show ?thesis by (auto intro: pCons)
  next
    case False
    with zero show ?thesis by simp
  qed
  with \<open>p = pCons a q\<close> show ?case
    by simp
qed

lemma degree_eq_zeroE:
  fixes p :: "'a::zero poly"
  assumes "degree p = 0"
  obtains a where "p = pCons a 0"
proof -
  obtain a q where p: "p = pCons a q"
    by (cases p)
  with assms have "q = 0"
    by (cases "q = 0") simp_all
  with p have "p = pCons a 0"
    by simp
  then show thesis ..
qed

subsection \<open>Quickcheck generator for polynomials\<close>

quickcheck_generator poly constructors: "0 :: _ poly", pCons

subsection \<open>List-style syntax for polynomials\<close>

syntax
  "_poly" :: "args \ 'a poly" (\(\indent=2 notation=\mixfix polynomial enumeration\\[:_:])\)
syntax_consts
  "_poly" \<rightleftharpoons> pCons
translations
  "[:x, xs:]" \<rightleftharpoons> "CONST pCons x [:xs:]"
  "[:x:]" \<rightleftharpoons> "CONST pCons x 0"

lemma degree_0_id:
  assumes "degree p = 0"
  shows "[: coeff p 0 :] = p"
  by (metis assms coeff_pCons_0 degree_eq_zeroE)

lemma degree0_coeffs: "degree p = 0 \ \ a. p = [: a :]"
  by (meson degree_eq_zeroE)

lemma degree1_coeffs:
  fixes p :: "'a::zero poly"
  assumes "degree p = 1"
  obtains a b where "p = [: b, a :]" "a \ 0"
proof -
  obtain b a q where "p = pCons b q" "q = pCons a 0"
    by (metis assms degree0_coeffs degree_0 degree_pCons_eq_if lessI less_one pCons_cases)
  then show thesis
    using assms that by force
qed

lemma degree2_coeffs:
  fixes p :: "'a::zero poly"
  assumes "degree p = 2"
  obtains a b c where "p = [: c, b, a :]" "a \ 0"
proof -
  obtain c q where "p = pCons c q" "degree q = 1"
    by (metis One_nat_def assms degree_0 degree_pCons_eq_if fact_0 fact_2 nat.inject numeral_2_eq_2 pCons_cases)
  then show thesis
    by (metis degree1_coeffs that)
qed

subsection \<open>Representation of polynomials by lists of coefficients\<close>

primrec Poly :: "'a::zero list \ 'a poly"
  where
    [code_post]: "Poly [] = 0"
  | [code_post]: "Poly (a # as) = pCons a (Poly as)"

lemma Poly_replicate_0 [simp]: "Poly (replicate n 0) = 0"
  by (induct n) simp_all

lemma Poly_eq_0: "Poly as = 0 \ (\n. as = replicate n 0)"
  by (induct as) (auto simp add: Cons_replicate_eq)

lemma Poly_append_replicate_zero [simp]: "Poly (as @ replicate n 0) = Poly as"
  by (induct as) simp_all

lemma Poly_snoc_zero [simp]: "Poly (as @ [0]) = Poly as"
  using Poly_append_replicate_zero [of as 1] by simp

lemma Poly_cCons_eq_pCons_Poly [simp]: "Poly (a ## p) = pCons a (Poly p)"
  by (simp add: cCons_def)

lemma Poly_on_rev_starting_with_0 [simp]: "hd as = 0 \ Poly (rev (tl as)) = Poly (rev as)"
  by (cases as) simp_all

lemma degree_Poly: "degree (Poly xs) \ length xs"
  by (induct xs) simp_all

lemma coeff_Poly_eq [simp]: "coeff (Poly xs) = nth_default 0 xs"
  by (induct xs) (simp_all add: fun_eq_iff coeff_pCons split: nat.splits)

definition coeffs :: "'a poly \ 'a::zero list"
  where "coeffs p = (if p = 0 then [] else map (\i. coeff p i) [0 ..< Suc (degree p)])"

lemma coeffs_eq_Nil [simp]: "coeffs p = [] \ p = 0"
  by (simp add: coeffs_def)

lemma not_0_coeffs_not_Nil: "p \ 0 \ coeffs p \ []"
  by simp

lemma coeffs_0_eq_Nil [simp]: "coeffs 0 = []"
  by simp

lemma coeffs_pCons_eq_cCons [simp]: "coeffs (pCons a p) = a ## coeffs p"
proof -
  have *: "\m\set ms. m > 0 \ map (case_nat x f) ms = map f (map (\n. n - 1) ms)"
    for ms :: "nat list" and f :: "nat \ 'a" and x :: "'a"
    by (induct ms) (auto split: nat.split)
  show ?thesis
    by (simp add: * coeffs_def upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
qed

lemma length_coeffs: "p \ 0 \ length (coeffs p) = degree p + 1"
  by (simp add: coeffs_def)

lemma coeffs_nth: "p \ 0 \ n \ degree p \ coeffs p ! n = coeff p n"
  by (auto simp: coeffs_def simp del: upt_Suc)

lemma coeff_in_coeffs: "p \ 0 \ n \ degree p \ coeff p n \ set (coeffs p)"
  using coeffs_nth [of p n, symmetric] by (simp add: length_coeffs)

lemma not_0_cCons_eq [simp]: "p \ 0 \ a ## coeffs p = a # coeffs p"
  by (simp add: cCons_def)

lemma Poly_coeffs [simp, code abstype]: "Poly (coeffs p) = p"
  by (induct p) auto

lemma coeffs_Poly [simp]: "coeffs (Poly as) = strip_while (HOL.eq 0) as"
proof (induct as)
  case Nil
  then show ?case by simp
next
  case (Cons a as)
  from replicate_length_same [of as 0] have "(\n. as \ replicate n 0) \ (\a\set as. a \ 0)"
    by (auto dest: sym [of _ as])
  with Cons show ?case by auto
qed

lemma no_trailing_coeffs [simp]:
  "no_trailing (HOL.eq 0) (coeffs p)"
  by (induct p)  auto

lemma strip_while_coeffs [simp]:
  "strip_while (HOL.eq 0) (coeffs p) = coeffs p"
  by simp

lemma coeffs_eq_iff: "p = q \ coeffs p = coeffs q"
  (is "?P \ ?Q")
proof
  assume ?P
  then show ?Q by simp
next
  assume ?Q
  then have "Poly (coeffs p) = Poly (coeffs q)" by simp
  then show ?P by simp
qed

lemma nth_default_coeffs_eq: "nth_default 0 (coeffs p) = coeff p"
  by (metis Poly_coeffs coeff_Poly_eq)

lemma range_coeff: "range (coeff p) = insert 0 (set (coeffs p))"
  by (metis nth_default_coeffs_eq range_nth_default)

lemma [code]: "coeff p = nth_default 0 (coeffs p)"
  by (simp add: nth_default_coeffs_eq)

lemma coeffs_eqI:
  assumes coeff: "\n. coeff p n = nth_default 0 xs n"
  assumes zero: "no_trailing (HOL.eq 0) xs"
  shows "coeffs p = xs"
proof -
  from coeff have "p = Poly xs"
    by (simp add: poly_eq_iff)
  with zero show ?thesis by simp
qed

lemma degree_eq_length_coeffs [code]: "degree p = length (coeffs p) - 1"
  by (simp add: coeffs_def)

lemma length_coeffs_degree: "p \ 0 \ length (coeffs p) = Suc (degree p)"
  by (induct p) (auto simp: cCons_def)

lemma [code abstract]: "coeffs 0 = []"
  by (fact coeffs_0_eq_Nil)

lemma [code abstract]: "coeffs (pCons a p) = a ## coeffs p"
  by (fact coeffs_pCons_eq_cCons)

lemma set_coeffs_subset_singleton_0_iff [simp]:
  "set (coeffs p) \ {0} \ p = 0"
  by (auto simp add: coeffs_def intro: classical)

lemma set_coeffs_not_only_0 [simp]:
  "set (coeffs p) \ {0}"
  by (auto simp add: set_eq_subset)

lemma forall_coeffs_conv:
  "(\n. P (coeff p n)) \ (\c \ set (coeffs p). P c)" if "P 0"
  using that by (auto simp add: coeffs_def)
    (metis atLeastLessThan_iff coeff_eq_0 not_less_iff_gr_or_eq zero_le)

instantiation poly :: ("{zero, equal}") equal
begin

definition [code]: "HOL.equal (p::'a poly) q \ HOL.equal (coeffs p) (coeffs q)"

instance
  by standard (simp add: equal equal_poly_def coeffs_eq_iff)

end

lemma [code nbe]: "HOL.equal (p :: _ poly) p \ True"
  by (fact equal_refl)

definition is_zero :: "'a::zero poly \ bool"
  where [code]: "is_zero p \ List.null (coeffs p)"

lemma is_zero_null [code_abbrev]: "is_zero p \ p = 0"
  by (simp add: is_zero_def)

text \<open>Reconstructing the polynomial from the list\<close>
  \<comment> \<open>contributed by Sebastiaan J.C. Joosten and René Thiemann\<close>

definition poly_of_list :: "'a::comm_monoid_add list \ 'a poly"
  where [simp]: "poly_of_list = Poly"

lemma poly_of_list_impl [code abstract]: "coeffs (poly_of_list as) = strip_while (HOL.eq 0) as"
  by simp

subsection \<open>Fold combinator for polynomials\<close>

definition fold_coeffs :: "('a::zero \ 'b \ 'b) \ 'a poly \ 'b \ 'b"
  where "fold_coeffs f p = foldr f (coeffs p)"

lemma fold_coeffs_0_eq [simp]: "fold_coeffs f 0 = id"
  by (simp add: fold_coeffs_def)

lemma fold_coeffs_pCons_eq [simp]: "f 0 = id \ fold_coeffs f (pCons a p) = f a \ fold_coeffs f p"
  by (simp add: fold_coeffs_def cCons_def fun_eq_iff)

lemma fold_coeffs_pCons_0_0_eq [simp]: "fold_coeffs f (pCons 0 0) = id"
  by (simp add: fold_coeffs_def)

lemma fold_coeffs_pCons_coeff_not_0_eq [simp]:
  "a \ 0 \ fold_coeffs f (pCons a p) = f a \ fold_coeffs f p"
  by (simp add: fold_coeffs_def)

lemma fold_coeffs_pCons_not_0_0_eq [simp]:
  "p \ 0 \ fold_coeffs f (pCons a p) = f a \ fold_coeffs f p"
  by (simp add: fold_coeffs_def)

subsection \<open>Canonical morphism on polynomials -- evaluation\<close>

definition poly :: \<open>'a::comm_semiring_0 poly \<Rightarrow> 'a \<Rightarrow> 'a\<close>
  where \<open>poly p a = horner_sum id a (coeffs p)\<close>

lemma poly_eq_fold_coeffs:
  \<open>poly p = fold_coeffs (\<lambda>a f x. a + x * f x) p (\<lambda>x. 0)\<close>
  by (induction p) (auto simp add: fun_eq_iff poly_def)

lemma poly_0 [simp]: "poly 0 x = 0"
  by (simp add: poly_def)

lemma poly_pCons [simp]: "poly (pCons a p) x = a + x * poly p x"
  by (cases "p = 0 \ a = 0") (auto simp add: poly_def)

lemma poly_altdef: "poly p x = (\i\degree p. coeff p i * x ^ i)"
  for x :: "'a::{comm_semiring_0,semiring_1}"
proof (induction p rule: pCons_induct)
  case 0
  then show ?case
    by simp
next
  case (pCons a p)
  show ?case
  proof (cases "p = 0")
    case True
    then show ?thesis by simp
  next
    case False
    let ?p' = "pCons a p"
    note poly_pCons[of a p x]
    also note pCons.IH
    also have "a + x * (\i\degree p. coeff p i * x ^ i) =
        coeff ?p' 0 * x^0 + (\i\degree p. coeff ?p' (Suc i) * x^Suc i)"
      by (simp add: field_simps sum_distrib_left coeff_pCons)
    also note sum.atMost_Suc_shift[symmetric]
    also note degree_pCons_eq[OF \<open>p \<noteq> 0\<close>, of a, symmetric]
    finally show ?thesis .
  qed
qed

lemma poly_0_coeff_0: "poly p 0 = coeff p 0"
  by (cases p) (auto simp: poly_altdef)

lemma poly_zero:
  fixes p :: "'a :: comm_ring_1 poly"
  assumes x: "poly p x = 0" shows "p = 0 \ degree p = 0"
proof
  assume degp: "degree p = 0"
  hence "poly p x = coeff p (degree p)" by(subst degree_0_id[OF degp,symmetric], simp)
  hence "coeff p (degree p) = 0" using x by auto
  thus "p = 0" by auto
qed auto

subsection \<open>Monomials\<close>

lift_definition monom :: "'a \ nat \ 'a::zero poly"
  is "\a m n. if m = n then a else 0"
  by (simp add: MOST_iff_cofinite)

lemma coeff_monom [simp]: "coeff (monom a m) n = (if m = n then a else 0)"
  by transfer rule

lemma monom_0: "monom a 0 = [:a:]"
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)

lemma monom_Suc: "monom a (Suc n) = pCons 0 (monom a n)"
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)

lemma monom_eq_0 [simp]: "monom 0 n = 0"
  by (rule poly_eqI) simp

lemma monom_eq_0_iff [simp]: "monom a n = 0 \ a = 0"
  by (simp add: poly_eq_iff)

lemma monom_eq_iff [simp]: "monom a n = monom b n \ a = b"
  by (simp add: poly_eq_iff)

lemma degree_monom_le: "degree (monom a n) \ n"
  by (rule degree_le, simp)

lemma degree_monom_eq: "a \ 0 \ degree (monom a n) = n"
  by (metis coeff_monom leading_coeff_0_iff)

lemma coeffs_monom [code abstract]:
  "coeffs (monom a n) = (if a = 0 then [] else replicate n 0 @ [a])"
  by (induct n) (simp_all add: monom_0 monom_Suc)

lemma fold_coeffs_monom [simp]: "a \ 0 \ fold_coeffs f (monom a n) = f 0 ^^ n \ f a"
  by (simp add: fold_coeffs_def coeffs_monom fun_eq_iff)

lemma poly_monom: "poly (monom a n) x = a * x ^ n"
  for a x :: "'a::comm_semiring_1"
  by (cases "a = 0", simp_all) (induct n, simp_all add: mult.left_commute poly_eq_fold_coeffs)

lemma monom_eq_iff': "monom c n = monom d m \ c = d \ (c = 0 \ n = m)"
  by (auto simp: poly_eq_iff)

lemma monom_eq_const_iff: "monom c n = [:d:] \ c = d \ (c = 0 \ n = 0)"
  using monom_eq_iff'[of c n d 0] by (simp add: monom_0)

subsection \<open>Leading coefficient\<close>

abbreviation lead_coeff:: "'a::zero poly \ 'a"
  where "lead_coeff p \ coeff p (degree p)"

lemma lead_coeff_pCons[simp]:
  "p \ 0 \ lead_coeff (pCons a p) = lead_coeff p"
  "p = 0 \ lead_coeff (pCons a p) = a"
  by auto

lemma lead_coeff_monom [simp]: "lead_coeff (monom c n) = c"
  by (cases "c = 0") (simp_all add: degree_monom_eq)

lemma last_coeffs_eq_coeff_degree:
  "last (coeffs p) = lead_coeff p" if "p \ 0"
  using that by (simp add: coeffs_def)

lemma lead_coeff_list_def:
  "lead_coeff p = (if coeffs p=[] then 0 else last (coeffs p))"
  by (simp add: last_coeffs_eq_coeff_degree)

subsection \<open>Addition and subtraction\<close>

instantiation poly :: (comm_monoid_add) comm_monoid_add
begin

lift_definition plus_poly :: "'a poly \ 'a poly \ 'a poly"
  is "\p q n. coeff p n + coeff q n"
proof -
  fix q p :: "'a poly"
  show "\\<^sub>\n. coeff p n + coeff q n = 0"
    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
qed

lemma coeff_add [simp]: "coeff (p + q) n = coeff p n + coeff q n"
  by (simp add: plus_poly.rep_eq)

instance
proof
  fix p q r :: "'a poly"
  show "(p + q) + r = p + (q + r)"
    by (simp add: poly_eq_iff add.assoc)
  show "p + q = q + p"
    by (simp add: poly_eq_iff add.commute)
  show "0 + p = p"
    by (simp add: poly_eq_iff)
qed

end

instantiation poly :: (cancel_comm_monoid_add) cancel_comm_monoid_add
begin

lift_definition minus_poly :: "'a poly \ 'a poly \ 'a poly"
  is "\p q n. coeff p n - coeff q n"
proof -
  fix q p :: "'a poly"
  show "\\<^sub>\n. coeff p n - coeff q n = 0"
    using MOST_coeff_eq_0[of p] MOST_coeff_eq_0[of q] by eventually_elim simp
qed

lemma coeff_diff [simp]: "coeff (p - q) n = coeff p n - coeff q n"
  by (simp add: minus_poly.rep_eq)

instance
proof
  fix p q r :: "'a poly"
  show "p + q - p = q"
    by (simp add: poly_eq_iff)
  show "p - q - r = p - (q + r)"
    by (simp add: poly_eq_iff diff_diff_eq)
qed

end

instantiation poly :: (ab_group_add) ab_group_add
begin

lift_definition uminus_poly :: "'a poly \ 'a poly"
  is "\p n. - coeff p n"
proof -
  fix p :: "'a poly"
  show "\\<^sub>\n. - coeff p n = 0"
    using MOST_coeff_eq_0 by simp
qed

lemma coeff_minus [simp]: "coeff (- p) n = - coeff p n"
  by (simp add: uminus_poly.rep_eq)

instance
proof
  fix p q :: "'a poly"
  show "- p + p = 0"
    by (simp add: poly_eq_iff)
  show "p - q = p + - q"
    by (simp add: poly_eq_iff)
qed

end

lemma add_pCons [simp]: "pCons a p + pCons b q = pCons (a + b) (p + q)"
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)

lemma minus_pCons [simp]: "- pCons a p = pCons (- a) (- p)"
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)

lemma diff_pCons [simp]: "pCons a p - pCons b q = pCons (a - b) (p - q)"
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)

lemma degree_add_le_max: "degree (p + q) \ max (degree p) (degree q)"
  by (rule degree_le) (auto simp add: coeff_eq_0)

lemma degree_add_le: "degree p \ n \ degree q \ n \ degree (p + q) \ n"
  by (auto intro: order_trans degree_add_le_max)

lemma degree_add_less: "degree p < n \ degree q < n \ degree (p + q) < n"
  by (auto intro: le_less_trans degree_add_le_max)

lemma degree_add_eq_right: assumes "degree p < degree q" shows "degree (p + q) = degree q"
proof (cases "q = 0")
  case False
  show ?thesis
  proof (rule order_antisym)
    show "degree (p + q) \ degree q"
      by (simp add: assms degree_add_le order.strict_implies_order)
    show "degree q \ degree (p + q)"
      by (simp add: False assms coeff_eq_0 le_degree)
  qed
qed (use assms in auto)

lemma degree_add_eq_left: "degree q < degree p \ degree (p + q) = degree p"
  using degree_add_eq_right [of q p] by (simp add: add.commute)

lemma degree_minus [simp]: "degree (- p) = degree p"
  by (simp add: degree_def)

lemma lead_coeff_add_le: "degree p < degree q \ lead_coeff (p + q) = lead_coeff q"
  by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right)

lemma lead_coeff_minus: "lead_coeff (- p) = - lead_coeff p"
  by (metis coeff_minus degree_minus)

lemma degree_diff_le_max: "degree (p - q) \ max (degree p) (degree q)"
  for p q :: "'a::ab_group_add poly"
  using degree_add_le [where p=p and q="-q"] by simp

lemma degree_diff_le: "degree p \ n \ degree q \ n \ degree (p - q) \ n"
  for p q :: "'a::ab_group_add poly"
  using degree_add_le [of p n "- q"] by simp

lemma degree_diff_less: "degree p < n \ degree q < n \ degree (p - q) < n"
  for p q :: "'a::ab_group_add poly"
  using degree_add_less [of p n "- q"] by simp

lemma add_monom: "monom a n + monom b n = monom (a + b) n"
  by (rule poly_eqI) simp

lemma diff_monom: "monom a n - monom b n = monom (a - b) n"
  by (rule poly_eqI) simp

lemma minus_monom: "- monom a n = monom (- a) n"
  by (rule poly_eqI) simp

lemma coeff_sum: "coeff (\x\A. p x) i = (\x\A. coeff (p x) i)"
  by (induct A rule: infinite_finite_induct) simp_all

lemma monom_sum: "monom (\x\A. a x) n = (\x\A. monom (a x) n)"
  by (rule poly_eqI) (simp add: coeff_sum)

fun plus_coeffs :: "'a::comm_monoid_add list \ 'a list \ 'a list"
  where
    "plus_coeffs xs [] = xs"
  | "plus_coeffs [] ys = ys"
  | "plus_coeffs (x # xs) (y # ys) = (x + y) ## plus_coeffs xs ys"

lemma coeffs_plus_eq_plus_coeffs [code abstract]:
  "coeffs (p + q) = plus_coeffs (coeffs p) (coeffs q)"
proof -
  have *: "nth_default 0 (plus_coeffs xs ys) n = nth_default 0 xs n + nth_default 0 ys n"
    for xs ys :: "'a list" and n
  proof (induct xs ys arbitrary: n rule: plus_coeffs.induct)
    case (3 x xs y ys n)
    then show ?case
      by (cases n) (auto simp add: cCons_def)
  qed simp_all
  have **: "no_trailing (HOL.eq 0) (plus_coeffs xs ys)"
    if "no_trailing (HOL.eq 0) xs" and "no_trailing (HOL.eq 0) ys"
    for xs ys :: "'a list"
    using that by (induct xs ys rule: plus_coeffs.induct) (simp_all add: cCons_def)
  show ?thesis
    by (rule coeffs_eqI) (auto simp add: * nth_default_coeffs_eq intro: **)
qed

lemma coeffs_uminus [code abstract]:
  "coeffs (- p) = map uminus (coeffs p)"
proof -
  have eq_0: "HOL.eq 0 \ uminus = HOL.eq (0::'a)"
    by (simp add: fun_eq_iff)
  show ?thesis
    by (rule coeffs_eqI) (simp_all add: nth_default_map_eq nth_default_coeffs_eq no_trailing_map eq_0)
qed

lemma [code]: "p - q = p + - q"
  for p q :: "'a::ab_group_add poly"
  by (fact diff_conv_add_uminus)

lemma poly_add [simp]: "poly (p + q) x = poly p x + poly q x"
proof (induction p arbitrary: q)
  case (pCons a p)
  then show ?case
    by (cases q) (simp add: algebra_simps)
qed auto

lemma poly_minus [simp]: "poly (- p) x = - poly p x"
  for x :: "'a::comm_ring"
  by (induct p) simp_all

lemma poly_diff [simp]: "poly (p - q) x = poly p x - poly q x"
  for x :: "'a::comm_ring"
  using poly_add [of p "- q" x] by simp

lemma poly_sum: "poly (\k\A. p k) x = (\k\A. poly (p k) x)"
  by (induct A rule: infinite_finite_induct) simp_all

lemma poly_sum_list: "poly (\p\ps. p) y = (\p\ps. poly p y)"
  by (induction ps) auto

lemma poly_sum_mset: "poly (\x\#A. p x) y = (\x\#A. poly (p x) y)"
  by (induction A) auto

lemma degree_sum_le: "finite S \ (\p. p \ S \ degree (f p) \ n) \ degree (sum f S) \ n"
proof (induct S rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert p S)
  then have "degree (sum f S) \ n" "degree (f p) \ n"
    by auto
  then show ?case
    unfolding sum.insert[OF insert(1-2)] by (metis degree_add_le)
qed

lemma degree_sum_less:
  assumes "\x. x \ A \ degree (f x) < n" "n > 0"
  shows   "degree (sum f A) < n"
  using assms by (induction rule: infinite_finite_induct) (auto intro!: degree_add_less)

lemma poly_as_sum_of_monoms':
  assumes "degree p \ n"
  shows "(\i\n. monom (coeff p i) i) = p"
proof -
  have eq: "\i. {..n} \ {i} = (if i \ n then {i} else {})"
    by auto
  from assms show ?thesis
    by (simp add: poly_eq_iff coeff_sum coeff_eq_0 sum.If_cases eq
        if_distrib[where f="\x. x * a" for a])
qed

lemma poly_as_sum_of_monoms: "(\i\degree p. monom (coeff p i) i) = p"
  by (intro poly_as_sum_of_monoms' order_refl)

lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
  by (induct xs) (simp_all add: monom_0 monom_Suc)

subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>

lift_definition smult :: "'a::comm_semiring_0 \ 'a poly \ 'a poly"
  is "\a p n. a * coeff p n"
proof -
  fix a :: 'a and p :: "'a poly"
  show "\\<^sub>\ i. a * coeff p i = 0"
    using MOST_coeff_eq_0[of p] by eventually_elim simp
qed

lemma coeff_smult [simp]: "coeff (smult a p) n = a * coeff p n"
  by (simp add: smult.rep_eq)

lemma degree_smult_le: "degree (smult a p) \ degree p"
  by (rule degree_le) (simp add: coeff_eq_0)

lemma smult_smult [simp]: "smult a (smult b p) = smult (a * b) p"
  by (rule poly_eqI) (simp add: mult.assoc)

lemma smult_0_right [simp]: "smult a 0 = 0"
  by (rule poly_eqI) simp

lemma smult_0_left [simp]: "smult 0 p = 0"
  by (rule poly_eqI) simp

lemma smult_1_left [simp]: "smult (1::'a::comm_semiring_1) p = p"
  by (rule poly_eqI) simp

lemma smult_add_right: "smult a (p + q) = smult a p + smult a q"
  by (rule poly_eqI) (simp add: algebra_simps)

lemma smult_add_left: "smult (a + b) p = smult a p + smult b p"
  by (rule poly_eqI) (simp add: algebra_simps)

lemma smult_minus_right [simp]: "smult a (- p) = - smult a p"
  for a :: "'a::comm_ring"
  by (rule poly_eqI) simp

lemma smult_minus_left [simp]: "smult (- a) p = - smult a p"
  for a :: "'a::comm_ring"
  by (rule poly_eqI) simp

lemma smult_diff_right: "smult a (p - q) = smult a p - smult a q"
  for a :: "'a::comm_ring"
  by (rule poly_eqI) (simp add: algebra_simps)

lemma smult_diff_left: "smult (a - b) p = smult a p - smult b p"
  for a b :: "'a::comm_ring"
  by (rule poly_eqI) (simp add: algebra_simps)

lemmas smult_distribs =
  smult_add_left smult_add_right
  smult_diff_left smult_diff_right

lemma smult_pCons [simp]: "smult a (pCons b p) = pCons (a * b) (smult a p)"
  by (rule poly_eqI) (simp add: coeff_pCons split: nat.split)

lemma smult_monom: "smult a (monom b n) = monom (a * b) n"
  by (induct n) (simp_all add: monom_0 monom_Suc)

lemma smult_Poly: "smult c (Poly xs) = Poly (map ((*) c) xs)"
  by (auto simp: poly_eq_iff nth_default_def)

lemma degree_smult_eq [simp]: "degree (smult a p) = (if a = 0 then 0 else degree p)"
  for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
  by (cases "a = 0") (simp_all add: degree_def)

lemma smult_eq_0_iff [simp]: "smult a p = 0 \ a = 0 \ p = 0"
  for a :: "'a::{comm_semiring_0,semiring_no_zero_divisors}"
  by (simp add: poly_eq_iff)

lemma coeffs_smult [code abstract]:
  "coeffs (smult a p) = (if a = 0 then [] else map (Groups.times a) (coeffs p))"
  for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
proof -
  have eq_0: "HOL.eq 0 \ times a = HOL.eq (0::'a)" if "a \ 0"
    using that by (simp add: fun_eq_iff)
  show ?thesis
    by (rule coeffs_eqI) (auto simp add: no_trailing_map nth_default_map_eq nth_default_coeffs_eq eq_0)
qed

lemma smult_eq_iff:
  fixes b :: "'a :: field"
  assumes "b \ 0"
  shows "smult a p = smult b q \ smult (a / b) p = q"
    (is "?lhs \ ?rhs")
proof
  assume ?lhs
  also from assms have "smult (inverse b) \ = q"
    by simp
  finally show ?rhs
    by (simp add: field_simps)
next
  assume ?rhs
  with assms show ?lhs by auto
qed

lemma smult_cancel:
  fixes p::"'a::idom poly"
  assumes "c\0" and smult: "smult c p = smult c q"
  shows "p=q"
proof -
  have "smult c (p-q) = 0" using smult by (metis diff_self smult_diff_right)
  thus ?thesis using \<open>c\<noteq>0\<close> by auto
qed

instantiation poly :: (comm_semiring_0) comm_semiring_0
begin

definition "p * q = fold_coeffs (\a p. smult a q + pCons 0 p) p 0"

lemma mult_poly_0_left: "(0::'a poly) * q = 0"
  by (simp add: times_poly_def)

lemma mult_pCons_left [simp]: "pCons a p * q = smult a q + pCons 0 (p * q)"
  by (cases "p = 0 \ a = 0") (auto simp add: times_poly_def)

lemma mult_poly_0_right: "p * (0::'a poly) = 0"
  by (induct p) (simp_all add: mult_poly_0_left)

lemma mult_pCons_right [simp]: "p * pCons a q = smult a p + pCons 0 (p * q)"
  by (induct p) (simp_all add: mult_poly_0_left algebra_simps)

lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right

lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)"
  by (induct p) (simp_all add: mult_poly_0 smult_add_right)

lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)"
  by (induct q) (simp_all add: mult_poly_0 smult_add_right)

lemma mult_poly_add_left: "(p + q) * r = p * r + q * r"
  for p q r :: "'a poly"
  by (induct r) (simp_all add: mult_poly_0 smult_distribs algebra_simps)

instance
proof
  fix p q r :: "'a poly"
  show 0: "0 * p = 0"
    by (rule mult_poly_0_left)
  show "p * 0 = 0"
    by (rule mult_poly_0_right)
  show "(p + q) * r = p * r + q * r"
    by (rule mult_poly_add_left)
  show "(p * q) * r = p * (q * r)"
    by (induct p) (simp_all add: mult_poly_0 mult_poly_add_left)
  show "p * q = q * p"
    by (induct p) (simp_all add: mult_poly_0)
qed

end

lemma coeff_mult_degree_sum:
  "coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)"
  by (induct p) (simp_all add: coeff_eq_0)

instance poly :: ("{comm_semiring_0,semiring_no_zero_divisors}") semiring_no_zero_divisors
proof
  fix p q :: "'a poly"
  assume "p \ 0" and "q \ 0"
  have "coeff (p * q) (degree p + degree q) = coeff p (degree p) * coeff q (degree q)"
    by (rule coeff_mult_degree_sum)
  also from \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close> have "coeff p (degree p) * coeff q (degree q) \<noteq> 0"
    by simp
  finally have "\n. coeff (p * q) n \ 0" ..
  then show "p * q \ 0"
    by (simp add: poly_eq_iff)
qed

instance poly :: (comm_semiring_0_cancel) comm_semiring_0_cancel ..

lemma coeff_mult: "coeff (p * q) n = (\i\n. coeff p i * coeff q (n-i))"
proof (induct p arbitrary: n)
  case 0
  show ?case by simp
next
  case (pCons a p n)
  then show ?case
    by (cases n) (simp_all add: sum.atMost_Suc_shift del: sum.atMost_Suc)
qed

lemma coeff_mult_0: "coeff (p * q) 0 = coeff p 0 * coeff q 0"
  by (simp add: coeff_mult)

lemma degree_mult_le: "degree (p * q) \ degree p + degree q"
proof (rule degree_le)
  show "\i>degree p + degree q. coeff (p * q) i = 0"
    by (induct p) (simp_all add: coeff_eq_0 coeff_pCons split: nat.split)
qed

lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)"
  by (induct m) (simp add: monom_0 smult_monom, simp add: monom_Suc)

instantiation poly :: (comm_semiring_1) comm_semiring_1
begin

lift_definition one_poly :: "'a poly"
  is "\n. of_bool (n = 0)"
  by (rule MOST_SucD) simp

lemma coeff_1 [simp]:
  "coeff 1 n = of_bool (n = 0)"
  by (simp add: one_poly.rep_eq)

lemma one_pCons:
  "1 = [:1:]"
  by (simp add: poly_eq_iff coeff_pCons split: nat.splits)

lemma pCons_one:
  "[:1:] = 1"
  by (simp add: one_pCons)

instance
  by standard (simp_all add: one_pCons)

end

lemma poly_1 [simp]:
  "poly 1 x = 1"
  by (simp add: one_pCons)

lemma one_poly_eq_simps [simp]:
  "1 = [:1:] \ True"
  "[:1:] = 1 \ True"
  by (simp_all add: one_pCons)

lemma degree_1 [simp]:
  "degree 1 = 0"
  by (simp add: one_pCons)

lemma coeffs_1_eq [simp, code abstract]:
  "coeffs 1 = [1]"
  by (simp add: one_pCons)

lemma smult_one [simp]:
  "smult c 1 = [:c:]"
  by (simp add: one_pCons)

lemma smult_sum: "smult (\i \ S. f i) p = (\i \ S. smult (f i) p)"
  by (induct S rule: infinite_finite_induct, auto simp: smult_add_left)

lemma smult_power: "(smult a p) ^ n = smult (a ^ n) (p ^ n)"
  by (induct n, auto simp: field_simps)

lemma monom_eq_1 [simp]:
  "monom 1 0 = 1"
  by (simp add: monom_0 one_pCons)

lemma monom_eq_1_iff:
  "monom c n = 1 \ c = 1 \ n = 0"
  using monom_eq_const_iff [of c n 1] by auto

lemma monom_altdef:
  "monom c n = smult c ([:0, 1:] ^ n)"
  by (induct n) (simp_all add: monom_0 monom_Suc)

lemma degree_sum_list_le: "(\ p . p \ set ps \ degree p \ n)
  \<Longrightarrow> degree (sum_list ps) \<le> n"
proof (induct ps)
  case (Cons p ps)
  hence "degree (sum_list ps) \ n" "degree p \ n" by auto
  thus ?case unfolding sum_list.Cons by (metis degree_add_le)
qed simp

lemma degree_prod_list_le: "degree (prod_list ps) \ sum_list (map degree ps)"
proof (induct ps)
  case (Cons p ps)
  show ?case unfolding prod_list.Cons
    by (rule order.trans[OF degree_mult_le], insert Cons, auto)
qed simp

instance poly :: ("{comm_semiring_1,semiring_1_no_zero_divisors}") semiring_1_no_zero_divisors ..
instance poly :: (comm_ring) comm_ring ..
instance poly :: (comm_ring_1) comm_ring_1 ..
instance poly :: (comm_ring_1) comm_semiring_1_cancel ..

lemma prod_smult: "(\x\A. smult (c x) (p x)) = smult (prod c A) (prod p A)"
  by (induction A rule: infinite_finite_induct) (auto simp: mult_ac)

lemma degree_power_le: "degree (p ^ n) \ degree p * n"
  by (induct n) (auto intro: order_trans degree_mult_le)

lemma coeff_0_power: "coeff (p ^ n) 0 = coeff p 0 ^ n"
  by (induct n) (simp_all add: coeff_mult)

lemma poly_smult [simp]: "poly (smult a p) x = a * poly p x"
  by (induct p) (simp_all add: algebra_simps)

lemma poly_mult [simp]: "poly (p * q) x = poly p x * poly q x"
  by (induct p) (simp_all add: algebra_simps)

lemma poly_power [simp]: "poly (p ^ n) x = poly p x ^ n"
  for p :: "'a::comm_semiring_1 poly"
  by (induct n) simp_all

lemma poly_prod: "poly (\k\A. p k) x = (\k\A. poly (p k) x)"
  by (induct A rule: infinite_finite_induct) simp_all

lemma poly_prod_list: "poly (\p\ps. p) y = (\p\ps. poly p y)"
  by (induction ps) auto

lemma poly_prod_mset: "poly (\x\#A. p x) y = (\x\#A. poly (p x) y)"
  by (induction A) auto

lemma poly_const_pow: "[: c :] ^ n = [: c ^ n :]"
  by (induction n) (auto simp: algebra_simps)

lemma monom_power: "monom c n ^ k = monom (c ^ k) (n * k)"
  by (induction k) (auto simp: mult_monom)

lemma degree_prod_sum_le: "finite S \ degree (prod f S) \ sum (degree \ f) S"
proof (induct S rule: finite_induct)
  case empty
  then show ?case by simp
next
  case (insert a S)
  show ?case
    unfolding prod.insert[OF insert(1-2)] sum.insert[OF insert(1-2)]
    by (rule le_trans[OF degree_mult_le]) (use insert in auto)
qed

lemma coeff_0_prod_list: "coeff (prod_list xs) 0 = prod_list (map (\p. coeff p 0) xs)"
  by (induct xs) (simp_all add: coeff_mult)

lemma coeff_monom_mult: "coeff (monom c n * p) k = (if k < n then 0 else c * coeff p (k - n))"
proof -
  have "coeff (monom c n * p) k = (\i\k. (if n = i then c else 0) * coeff p (k - i))"
    by (simp add: coeff_mult)
  also have "\ = (\i\k. (if n = i then c * coeff p (k - i) else 0))"
    by (intro sum.cong) simp_all
  also have "\ = (if k < n then 0 else c * coeff p (k - n))"
    by simp
  finally show ?thesis .
qed

lemma coeff_monom_Suc: "coeff (monom a (Suc d) * p) (Suc i) = coeff (monom a d * p) i"
  by (simp add: monom_Suc)

lemma monom_1_dvd_iff': "monom 1 n dvd p \ (\k
proof
  assume "monom 1 n dvd p"
  then obtain r where "p = monom 1 n * r"
    by (rule dvdE)
  then show "\k
    by (simp add: coeff_mult)
next
  assume zero: "(\k
  define r where "r = Abs_poly (\k. coeff p (k + n))"
  have "\\<^sub>\k. coeff p (k + n) = 0"
    by (subst cofinite_eq_sequentially, subst eventually_sequentially_seg,
        subst cofinite_eq_sequentially [symmetric]) transfer
  then have coeff_r [simp]: "coeff r k = coeff p (k + n)" for k
    unfolding r_def by (subst poly.Abs_poly_inverse) simp_all
  have "p = monom 1 n * r"
    by (rule poly_eqI, subst coeff_monom_mult) (simp_all add: zero)
  then show "monom 1 n dvd p" by simp
qed

lemma coeff_sum_monom:
  assumes n: "n \ d"
  shows "coeff (\i\d. monom (f i) i) n = f n" (is "?l = _")
proof -
  have "?l = (\i\d. coeff (monom (f i) i) n)" (is "_ = sum ?cmf _")
    using coeff_sum.
  also have "{..d} = insert n ({..d}-{n})" using n by auto
    hence "sum ?cmf {..d} = sum ?cmf ..." by auto
  also have "... = sum ?cmf ({..d}-{n}) + ?cmf n" by (subst sum.insert,auto)
  also have "sum ?cmf ({..d}-{n}) = 0" by (subst sum.neutral, auto)
  finally show ?thesis by simp
qed

subsection \<open>Mapping polynomials\<close>

definition map_poly :: "('a :: zero \ 'b :: zero) \ 'a poly \ 'b poly"
  where "map_poly f p = Poly (map f (coeffs p))"

lemma map_poly_0 [simp]: "map_poly f 0 = 0"
  by (simp add: map_poly_def)

lemma map_poly_1: "map_poly f 1 = [:f 1:]"
  by (simp add: map_poly_def)

lemma map_poly_1' [simp]: "f 1 = 1 \ map_poly f 1 = 1"
  by (simp add: map_poly_def one_pCons)

lemma coeff_map_poly:
  assumes "f 0 = 0"
  shows "coeff (map_poly f p) n = f (coeff p n)"
  by (auto simp: assms map_poly_def nth_default_def coeffs_def not_less Suc_le_eq coeff_eq_0
      simp del: upt_Suc)

lemma lead_coeff_map_poly_nz:
  assumes "f (lead_coeff p) \ 0" "f 0 = 0"
  shows "lead_coeff (map_poly f p) = f (lead_coeff p)"
  by (metis (no_types, lifting) antisym assms coeff_0 coeff_map_poly le_degree leading_coeff_0_iff)

lemma coeffs_map_poly [code abstract]:
  "coeffs (map_poly f p) = strip_while ((=) 0) (map f (coeffs p))"
  by (simp add: map_poly_def)

lemma coeffs_map_poly':
  assumes "\x. x \ 0 \ f x \ 0"
  shows "coeffs (map_poly f p) = map f (coeffs p)"
  using assms
  by (auto simp add: coeffs_map_poly strip_while_idem_iff
    last_coeffs_eq_coeff_degree no_trailing_unfold last_map)

lemma set_coeffs_map_poly:
  "(\x. f x = 0 \ x = 0) \ set (coeffs (map_poly f p)) = f ` set (coeffs p)"
  by (simp add: coeffs_map_poly')

lemma degree_map_poly:
  assumes "\x. x \ 0 \ f x \ 0"
  shows "degree (map_poly f p) = degree p"
  by (simp add: degree_eq_length_coeffs coeffs_map_poly' assms)

lemma map_poly_eq_0_iff:
  assumes "f 0 = 0" "\x. x \ set (coeffs p) \ x \ 0 \ f x \ 0"
  shows "map_poly f p = 0 \ p = 0"
proof -
  have "(coeff (map_poly f p) n = 0) = (coeff p n = 0)" for n
  proof -
    have "coeff (map_poly f p) n = f (coeff p n)"
      by (simp add: coeff_map_poly assms)
    also have "\ = 0 \ coeff p n = 0"
    proof (cases "n < length (coeffs p)")
      case True
      then have "coeff p n \ set (coeffs p)"
        by (auto simp: coeffs_def simp del: upt_Suc)
      with assms show "f (coeff p n) = 0 \ coeff p n = 0"
        by auto
    next
      case False
      then show ?thesis
        by (auto simp: assms length_coeffs nth_default_coeffs_eq [symmetric] nth_default_def)
    qed
    finally show ?thesis .
  qed
  then show ?thesis by (auto simp: poly_eq_iff)
qed

lemma map_poly_smult:
  assumes "f 0 = 0""\c x. f (c * x) = f c * f x"
  shows "map_poly f (smult c p) = smult (f c) (map_poly f p)"
  by (intro poly_eqI) (simp_all add: assms coeff_map_poly)

lemma map_poly_pCons:
  assumes "f 0 = 0"
  shows "map_poly f (pCons c p) = pCons (f c) (map_poly f p)"
  by (intro poly_eqI) (simp_all add: assms coeff_map_poly coeff_pCons split: nat.splits)

lemma map_poly_map_poly:
  assumes "f 0 = 0" "g 0 = 0"
  shows "map_poly f (map_poly g p) = map_poly (f \ g) p"
  by (intro poly_eqI) (simp add: coeff_map_poly assms)

lemma map_poly_id [simp]: "map_poly id p = p"
  by (simp add: map_poly_def)

lemma map_poly_id' [simp]: "map_poly (\x. x) p = p"
  by (simp add: map_poly_def)

lemma map_poly_cong:
  assumes "(\x. x \ set (coeffs p) \ f x = g x)"
  shows "map_poly f p = map_poly g p"
proof -
  from assms have "map f (coeffs p) = map g (coeffs p)"
    by (intro map_cong) simp_all
  then show ?thesis
    by (simp only: coeffs_eq_iff coeffs_map_poly)
qed

lemma map_poly_monom: "f 0 = 0 \ map_poly f (monom c n) = monom (f c) n"
  by (intro poly_eqI) (simp_all add: coeff_map_poly)

lemma map_poly_idI:
  assumes "\x. x \ set (coeffs p) \ f x = x"
  shows "map_poly f p = p"
  using map_poly_cong[OF assms, of _ id] by simp

lemma map_poly_idI':
  assumes "\x. x \ set (coeffs p) \ f x = x"
  shows "p = map_poly f p"
  using map_poly_cong[OF assms, of _ id] by simp

lemma smult_conv_map_poly: "smult c p = map_poly (\x. c * x) p"
  by (intro poly_eqI) (simp_all add: coeff_map_poly)

lemma poly_cnj: "cnj (poly p z) = poly (map_poly cnj p) (cnj z)"
  by (simp add: poly_altdef degree_map_poly coeff_map_poly)

lemma poly_cnj_real:
  assumes "\n. poly.coeff p n \ \"
  shows   "cnj (poly p z) = poly p (cnj z)"
proof -
  from assms have "map_poly cnj p = p"
    by (intro poly_eqI) (auto simp: coeff_map_poly Reals_cnj_iff)
  with poly_cnj[of p z] show ?thesis by simp
qed

lemma real_poly_cnj_root_iff:
  assumes "\n. poly.coeff p n \ \"
  shows   "poly p (cnj z) = 0 \ poly p z = 0"
proof -
  have "poly p (cnj z) = cnj (poly p z)"
    by (simp add: poly_cnj_real assms)
  also have "\ = 0 \ poly p z = 0" by simp
  finally show ?thesis .
qed

lemma sum_to_poly: "(\x\A. [:f x:]) = [:\x\A. f x:]"
  by (induction A rule: infinite_finite_induct) auto

lemma diff_to_poly: "[:c:] - [:d:] = [:c - d:]"
  by (simp add: poly_eq_iff mult_ac)

lemma mult_to_poly: "[:c:] * [:d:] = [:c * d:]"
  by (simp add: poly_eq_iff mult_ac)

lemma prod_to_poly: "(\x\A. [:f x:]) = [:\x\A. f x:]"
  by (induction A rule: infinite_finite_induct) (auto simp: mult_to_poly mult_ac)

lemma poly_map_poly_cnj [simp]: "poly (map_poly cnj p) x = cnj (poly p (cnj x))"
  using complex_cnj_cnj poly_cnj by force

lemma map_poly_degree_eq:
  assumes "f (lead_coeff p) \ 0"
  shows "degree (map_poly f p) = degree p"
  using assms
  unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly lead_coeff_list_def
  by (metis (full_types) last_conv_nth_default length_map no_trailing_unfold nth_default_coeffs_eq
      nth_default_map_eq strip_while_idem)

lemma map_poly_degree_less:
  assumes "f (lead_coeff p) =0" "degree p\0"
  shows "degree (map_poly f p) < degree p"
proof -
  have "length (coeffs p) >1"
    using \<open>degree p\<noteq>0\<close> by (simp add: degree_eq_length_coeffs)
  then obtain xs x where xs_def:"coeffs p=xs@[x]" "length xs>0"
    by (metis One_nat_def add_0 append_Nil length_greater_0_conv list.size(4) nat_neq_iff not_less_zero rev_exhaust)
  have "f x=0" using assms(1) by (simp add: lead_coeff_list_def xs_def(1))
  have "degree (map_poly f p) = length (strip_while ((=) 0) (map f (xs@[x]))) - 1"
    unfolding map_poly_def degree_eq_length_coeffs coeffs_Poly
    by (subst xs_def,auto)
  also have "\ = length (strip_while ((=) 0) (map f xs)) - 1"
    using \<open>f x=0\<close> by simp
  also have "\ \ length xs -1"
    using length_strip_while_le by (metis diff_le_mono length_map)
  also have "\ < length (xs@[x]) - 1"
    using xs_def(2) by auto
  also have "\ = degree p"
    unfolding degree_eq_length_coeffs xs_def by simp
  finally show ?thesis .
qed

lemma map_poly_degree_leq:
  shows "degree (map_poly f p) \ degree p"
  unfolding map_poly_def degree_eq_length_coeffs
  by (metis coeffs_Poly diff_le_mono length_map length_strip_while_le)

subsection \<open>Conversions\<close>

lemma of_nat_poly: "of_nat n = [:of_nat n:]"
  by (induct n) (simp_all add: one_pCons)

lemma of_nat_monom: "of_nat n = monom (of_nat n) 0"
  by (simp add: of_nat_poly monom_0)

lemma degree_of_nat [simp]: "degree (of_nat n) = 0"
  by (simp add: of_nat_poly)

lemma lead_coeff_of_nat [simp]: "lead_coeff (of_nat n) = of_nat n"
  by (simp add: of_nat_poly)

lemma of_int_poly: "of_int k = [:of_int k:]"
  by (simp only: of_int_of_nat of_nat_poly) simp

lemma of_int_monom: "of_int k = monom (of_int k) 0"
  by (simp add: of_int_poly monom_0)

lemma degree_of_int [simp]: "degree (of_int k) = 0"
  by (simp add: of_int_poly)

lemma lead_coeff_of_int [simp]: "lead_coeff (of_int k) = of_int k"
  by (simp add: of_int_poly)

lemma poly_of_nat [simp]: "poly (of_nat n) x = of_nat n"
  by (simp add: of_nat_poly)

lemma poly_of_int [simp]: "poly (of_int n) x = of_int n"
  by (simp add: of_int_poly)

lemma poly_numeral [simp]: "poly (numeral n) x = numeral n"
  by (metis of_nat_numeral poly_of_nat)

lemma numeral_poly: "numeral n = [:numeral n:]"
proof -
  have "numeral n = of_nat (numeral n)"
    by simp
  also have "\ = [:of_nat (numeral n):]"
    by (simp add: of_nat_poly)
  finally show ?thesis
    by simp
qed

lemma numeral_monom:
  "numeral n = monom (numeral n) 0"
  by (simp add: numeral_poly monom_0)

lemma degree_numeral [simp]:
  "degree (numeral n) = 0"
  by (simp add: numeral_poly)

lemma lead_coeff_numeral [simp]:
  "lead_coeff (numeral n) = numeral n"
  by (simp add: numeral_poly)

lemma coeff_linear_poly_power:
  fixes c :: "'a :: semiring_1"
  assumes "i \ n"
  shows   "coeff ([:a, b:] ^ n) i = of_nat (n choose i) * b ^ i * a ^ (n - i)"
proof -
  have "[:a, b:] = monom b 1 + [:a:]"
    by (simp add: monom_altdef)
  also have "coeff (\ ^ n) i = (\k\n. a^(n-k) * of_nat (n choose k) * (if k = i then b ^ k else 0))"
    by (subst binomial_ring) (simp add: coeff_sum of_nat_poly monom_power poly_const_pow mult_ac)
  also have "\ = (\k\{i}. a ^ (n - i) * b ^ i * of_nat (n choose k))"
    using assms by (intro sum.mono_neutral_cong_right) (auto simp: mult_ac)
  finally show *: ?thesis by (simp add: mult_ac)
qed

subsection \<open>Lemmas about divisibility\<close>

lemma dvd_smult:
  assumes "p dvd q"
  shows "p dvd smult a q"
proof -
  from assms obtain k where "q = p * k" ..
  then have "smult a q = p * smult a k" by simp
  then show "p dvd smult a q" ..
qed

lemma dvd_smult_cancel: "p dvd smult a q \ a \ 0 \ p dvd q"
  for a :: "'a::field"
  by (drule dvd_smult [where a="inverse a"]) simp

lemma dvd_smult_iff: "a \ 0 \ p dvd smult a q \ p dvd q"
  for a :: "'a::field"
  by (safe elim!: dvd_smult dvd_smult_cancel)

lemma smult_dvd_cancel:
  assumes "smult a p dvd q"
  shows "p dvd q"
proof -
  from assms obtain k where "q = smult a p * k" ..
  then have "q = p * smult a k" by simp
  then show "p dvd q" ..
qed

lemma smult_dvd: "p dvd q \ a \ 0 \ smult a p dvd q"
  for a :: "'a::field"
  by (rule smult_dvd_cancel [where a="inverse a"]) simp

lemma smult_dvd_iff: "smult a p dvd q \ (if a = 0 then q = 0 else p dvd q)"
  for a :: "'a::field"
  by (auto elim: smult_dvd smult_dvd_cancel)

lemma is_unit_smult_iff: "smult c p dvd 1 \ c dvd 1 \ p dvd 1"
proof -
  have "smult c p = [:c:] * p" by simp
  also have "\ dvd 1 \ c dvd 1 \ p dvd 1"
  proof safe
    assume *: "[:c:] * p dvd 1"
    then show "p dvd 1"
      by (rule dvd_mult_right)
    from * obtain q where q: "1 = [:c:] * p * q"
      by (rule dvdE)
    have "c dvd c * (coeff p 0 * coeff q 0)"
      by simp
    also have "\ = coeff ([:c:] * p * q) 0"
      by (simp add: mult.assoc coeff_mult)
    also note q [symmetric]
    finally have "c dvd coeff 1 0" .
    then show "c dvd 1" by simp
  next
    assume "c dvd 1" "p dvd 1"
    from this(1) obtain d where "1 = c * d"
      by (rule dvdE)
    then have "1 = [:c:] * [:d:]"
      by (simp add: one_pCons ac_simps)
    then have "[:c:] dvd 1"
      by (rule dvdI)
    from mult_dvd_mono[OF this \<open>p dvd 1\<close>] show "[:c:] * p dvd 1"
      by simp
  qed
  finally show ?thesis .
qed

subsection \<open>Polynomials form an integral domain\<close>

instance poly :: (idom) idom ..

instance poly :: ("{ring_char_0, comm_ring_1}") ring_char_0
  by standard (auto simp add: of_nat_poly intro: injI)

lemma semiring_char_poly [simp]: "CHAR('a :: comm_semiring_1 poly) = CHAR('a)"
  by (rule CHAR_eqI) (auto simp: of_nat_poly of_nat_eq_0_iff_char_dvd)

instance poly :: ("{semiring_prime_char,comm_semiring_1}") semiring_prime_char
  by (rule semiring_prime_charI) auto
instance poly :: ("{comm_semiring_prime_char,comm_semiring_1}") comm_semiring_prime_char
  by standard
instance poly :: ("{comm_ring_prime_char,comm_semiring_1}") comm_ring_prime_char
  by standard
instance poly :: ("{idom_prime_char,comm_semiring_1}") idom_prime_char
  by standard

lemma degree_mult_eq: "p \ 0 \ q \ 0 \ degree (p * q) = degree p + degree q"
  for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  by (rule order_antisym [OF degree_mult_le le_degree]) (simp add: coeff_mult_degree_sum)

lemma degree_prod_sum_eq:
  "(\x. x \ A \ f x \ 0) \
     degree (prod f A :: 'a :: idom poly) = (\x\A. degree (f x))"
  by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq)

lemma dvd_imp_degree:
  \<open>degree x \<le> degree y\<close> if \<open>x dvd y\<close> \<open>x \<noteq> 0\<close> \<open>y \<noteq> 0\<close>
    for x y :: \<open>'a::{comm_semiring_1,semiring_no_zero_divisors} poly\<close>
proof -
  from \<open>x dvd y\<close> obtain z where \<open>y = x * z\<close> ..
  with \<open>x \<noteq> 0\<close> \<open>y \<noteq> 0\<close> show ?thesis
    by (simp add: degree_mult_eq)
qed

lemma degree_prod_eq_sum_degree:
  fixes A :: "'a set"
  and f :: "'a \ 'b::idom poly"
  assumes f0: "\i\A. f i \ 0"
  shows "degree (\i\A. (f i)) = (\i\A. degree (f i))"
  using assms
  by (induction A rule: infinite_finite_induct) (auto simp: degree_mult_eq)

lemma degree_mult_eq_0:
  "degree (p * q) = 0 \ p = 0 \ q = 0 \ (p \ 0 \ q \ 0 \ degree p = 0 \ degree q = 0)"
  for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  by (auto simp: degree_mult_eq)

lemma degree_power_eq: "p \ 0 \ degree ((p :: 'a :: idom poly) ^ n) = n * degree p"
  by (induction n) (simp_all add: degree_mult_eq)

lemma degree_mult_right_le:
  fixes p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  assumes "q \ 0"
  shows "degree p \ degree (p * q)"
  using assms by (cases "p = 0") (simp_all add: degree_mult_eq)

lemma coeff_degree_mult: "coeff (p * q) (degree (p * q)) = coeff q (degree q) * coeff p (degree p)"
  for p q :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
  by (cases "p = 0 \ q = 0") (auto simp: degree_mult_eq coeff_mult_degree_sum mult_ac)

lemma dvd_imp_degree_le: "p dvd q \ q \ 0 \ degree p \ degree q"
  for p q :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
  by (erule dvdE, hypsubst, subst degree_mult_eq) auto

lemma divides_degree:
  fixes p q :: "'a ::{comm_semiring_1,semiring_no_zero_divisors} poly"
  assumes "p dvd q"
  shows "degree p \ degree q \ q = 0"
  by (metis dvd_imp_degree_le assms)

lemma const_poly_dvd_iff:
  fixes c :: "'a::{comm_semiring_1,semiring_no_zero_divisors}"
  shows "[:c:] dvd p \ (\n. c dvd coeff p n)"
proof (cases "c = 0 \ p = 0")
  case True
  then show ?thesis
    by (auto intro!: poly_eqI)
next
  case False
  show ?thesis
  proof
    assume "[:c:] dvd p"
    then show "\n. c dvd coeff p n"
      by (auto simp: coeffs_def)
  next
    assume *: "\n. c dvd coeff p n"
    define mydiv where "mydiv x y = (SOME z. x = y * z)" for x y :: 'a
    have mydiv: "x = y * mydiv x y" if "y dvd x" for x y
      using that unfolding mydiv_def dvd_def by (rule someI_ex)
    define q where "q = Poly (map (\a. mydiv a c) (coeffs p))"
    from False * have "p = q * [:c:]"
      by (intro poly_eqI)
        (auto simp: q_def nth_default_def not_less length_coeffs_degree coeffs_nth
          intro!: coeff_eq_0 mydiv)
    then show "[:c:] dvd p"
      by (simp only: dvd_triv_right)
  qed
qed

lemma const_poly_dvd_const_poly_iff [simp]: "[:a:] dvd [:b:] \ a dvd b"
  for a b :: "'a::{comm_semiring_1,semiring_no_zero_divisors}"
  by (subst const_poly_dvd_iff) (auto simp: coeff_pCons split: nat.splits)

lemma lead_coeff_mult: "lead_coeff (p * q) = lead_coeff p * lead_coeff q"
  for p q :: "'a::{comm_semiring_0, semiring_no_zero_divisors} poly"
  by (cases "p = 0 \ q = 0") (auto simp: coeff_mult_degree_sum degree_mult_eq)

lemma lead_coeff_prod: "lead_coeff (prod f A) = (\x\A. lead_coeff (f x))"
  for f :: "'a \ 'b::{comm_semiring_1, semiring_no_zero_divisors} poly"
  by (induction A rule: infinite_finite_induct) (auto simp: lead_coeff_mult)

lemma lead_coeff_smult: "lead_coeff (smult c p) = c * lead_coeff p"
  for p :: "'a::{comm_semiring_0,semiring_no_zero_divisors} poly"
proof -
  have "smult c p = [:c:] * p" by simp
  also have "lead_coeff \ = c * lead_coeff p"
    by (subst lead_coeff_mult) simp_all
  finally show ?thesis .
qed

lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1"
  by simp

lemma lead_coeff_power: "lead_coeff (p ^ n) = lead_coeff p ^ n"
  for p :: "'a::{comm_semiring_1,semiring_no_zero_divisors} poly"
  by (induct n) (simp_all add: lead_coeff_mult)

subsection \<open>Polynomials form an ordered integral domain\<close>

definition pos_poly :: "'a::linordered_semidom poly \ bool"
  where "pos_poly p \ 0 < coeff p (degree p)"

lemma pos_poly_pCons: "pos_poly (pCons a p) \ pos_poly p \ (p = 0 \ 0 < a)"
  by (simp add: pos_poly_def)

lemma not_pos_poly_0 [simp]: "\ pos_poly 0"
  by (simp add: pos_poly_def)

lemma pos_poly_add: "pos_poly p \ pos_poly q \ pos_poly (p + q)"
proof (induction p arbitrary: q)
  case (pCons a p)
  then show ?case
    by (cases q; force simp add: pos_poly_pCons add_pos_pos)
qed auto

lemma pos_poly_mult: "pos_poly p \ pos_poly q \ pos_poly (p * q)"
  by (simp add: pos_poly_def coeff_degree_mult)

lemma pos_poly_total: "p = 0 \ pos_poly p \ pos_poly (- p)"
  for p :: "'a::linordered_idom poly"
  by (induct p) (auto simp: pos_poly_pCons)

lemma pos_poly_coeffs [code]: "pos_poly p \ (let as = coeffs p in as \ [] \ last as > 0)"
  (is "?lhs \ ?rhs")
proof
  assume ?rhs
  then show ?lhs
    by (auto simp add: pos_poly_def last_coeffs_eq_coeff_degree)
next
  assume ?lhs
  then have *: "0 < coeff p (degree p)"
    by (simp add: pos_poly_def)
  then have "p \ 0"
    by auto
  with * show ?rhs
    by (simp add: last_coeffs_eq_coeff_degree)
qed

instantiation poly :: (linordered_idom) linordered_idom
begin

definition "x < y \ pos_poly (y - x)"

definition "x \ y \ x = y \ pos_poly (y - x)"

definition "\x::'a poly\ = (if x < 0 then - x else x)"

definition "sgn (x::'a poly) = (if x = 0 then 0 else if 0 < x then 1 else - 1)"

instance
proof
  fix x y z :: "'a poly"
  show "x < y \ x \ y \ \ y \ x"
    unfolding less_eq_poly_def less_poly_def
    using pos_poly_add by force
  then show "x \ y \ y \ x \ x = y"
    using less_eq_poly_def less_poly_def by force
  show "x \ x"
    by (simp add: less_eq_poly_def)
  show "x \ y \ y \ z \ x \ z"
    using less_eq_poly_def pos_poly_add by fastforce
  show "x \ y \ z + x \ z + y"
    by (simp add: less_eq_poly_def)
  show "x \ y \ y \ x"
    unfolding less_eq_poly_def
    using pos_poly_total [of "x - y"]
    by auto
  show "x < y \ 0 < z \ z * x < z * y"
    by (simp add: less_poly_def right_diff_distrib [symmetric] pos_poly_mult)
  show "\x\ = (if x < 0 then - x else x)"
    by (rule abs_poly_def)
  show "sgn x = (if x = 0 then 0 else if 0 < x then 1 else - 1)"
    by (rule sgn_poly_def)
qed

end

text \<open>TODO: Simplification rules for comparisons\<close>

subsection \<open>Synthetic division and polynomial roots\<close>

subsubsection \<open>Synthetic division\<close>

text \<open>Synthetic division is simply division by the linear polynomial \<^term>\<open>x - c\<close>.\<close>

definition synthetic_divmod :: "'a::comm_semiring_0 poly \ 'a \ 'a poly \ 'a"
  where "synthetic_divmod p c = fold_coeffs (\a (q, r). (pCons r q, a + c * r)) p (0, 0)"

definition synthetic_div :: "'a::comm_semiring_0 poly \ 'a \ 'a poly"
  where "synthetic_div p c = fst (synthetic_divmod p c)"

lemma synthetic_divmod_0 [simp]: "synthetic_divmod 0 c = (0, 0)"
  by (simp add: synthetic_divmod_def)

lemma synthetic_divmod_pCons [simp]:
  "synthetic_divmod (pCons a p) c = (\(q, r). (pCons r q, a + c * r)) (synthetic_divmod p c)"
  by (cases "p = 0 \ a = 0") (auto simp add: synthetic_divmod_def)

lemma synthetic_div_0 [simp]: "synthetic_div 0 c = 0"
  by (simp add: synthetic_div_def)

lemma synthetic_div_unique_lemma: "smult c p = pCons a p \ p = 0"
  by (induct p arbitrary: a) simp_all

lemma snd_synthetic_divmod: "snd (synthetic_divmod p c) = poly p c"
  by (induct p) (simp_all add: split_def)

lemma synthetic_div_pCons [simp]:
  "synthetic_div (pCons a p) c = pCons (poly p c) (synthetic_div p c)"
  by (simp add: synthetic_div_def split_def snd_synthetic_divmod)

lemma synthetic_div_eq_0_iff: "synthetic_div p c = 0 \ degree p = 0"
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ Dauer der Verarbeitung: 0.29 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.