# Theory Polynomials.Polynomials

(*  Title:       Executable multivariate polynomials
Author:      Christian Sternagel <christian.sternagel@uibk.ac.at>
René Thiemann       <rene.thiemann@uibk.ac.at>
Maintainer:  Christian Sternagel and René Thiemann
*)

(*
Copyright 2010 Christian Sternagel, René Thiemann

This file is part of IsaFoR/CeTA.

IsaFoR/CeTA is free software: you can redistribute it and/or modify it under the
Foundation, either version 3 of the License, or (at your option) any later
version.

IsaFoR/CeTA is distributed in the hope that it will be useful, but WITHOUT ANY
WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.

You should have received a copy of the GNU Lesser General Public License along
with IsaFoR/CeTA. If not, see <http://www.gnu.org/licenses/>.
*)

section ‹Polynomials›

(* TODO: attempt to turn polynomials into type *)

theory Polynomials
imports

Matrix.Utility
begin

subsection ‹
Polynomials represented as trees
›
datatype (vars_tpoly: 'v, nums_tpoly: 'a)tpoly = PVar 'v | PNum 'a | PSum "('v,'a)tpoly list" | PMult "('v,'a)tpoly list"

type_synonym ('v,'a)assign = "'v  'a"

primrec eval_tpoly :: "('v,'a::{monoid_add,monoid_mult})assign  ('v,'a)tpoly  'a"
where "eval_tpoly α (PVar x) = α x"
|  "eval_tpoly α (PNum a) = a"
|  "eval_tpoly α (PSum ps) = sum_list (map (eval_tpoly α) ps)"
|  "eval_tpoly α (PMult ps) = prod_list (map (eval_tpoly α) ps)"

subsection ‹Polynomials represented in normal form as lists of monomials›
text ‹
The internal representation of polynomials is a sum of products of monomials with coefficients
where all coefficients are non-zero, and all monomials are different
›

text ‹Definition of type monom›

type_synonym 'v monom_list = "('v × nat)list"
text ‹
\begin{itemize}
\item $[(x,n),(y,m)]$ represent $x^n \cdot y^m$
\item invariants: all powers are $\geq 1$ and each variable occurs at most once \\
hence: $[(x,1),(y,2),(x,2)]$ will not occur, but $[(x,3),(y,2)]$;
$[(x,1),(y,0)]$ will not occur, but $[(x,1)]$
\end{itemize}
›

context linorder
begin
definition monom_inv :: "'a monom_list  bool" where
"monom_inv m  ( (x,n)  set m. 1  n)  distinct (map fst m)  sorted (map fst m)"

fun eval_monom_list :: "('a,'b :: comm_semiring_1)assign  ('a monom_list)  'b" where
"eval_monom_list α [] = 1"
| "eval_monom_list α ((x,p) # m) = eval_monom_list α m * (α x)^p"

lemma eval_monom_list[simp]:
by (induct m, auto simp: field_simps)

definition sum_var_list :: "'a monom_list  'a  nat" where
"sum_var_list m x  sum_list (map (λ (y,c). if x = y then c else 0) m)"

lemma sum_var_list_not: "x  fst  set m  sum_var_list m x = 0"
unfolding sum_var_list_def by (induct m, auto)

text ‹
show that equality of monomials is equivalent to statement that
all variables occur with the same (accumulated) power;
afterwards properties like transitivity, etc. are easy to prove›

lemma monom_inv_Cons: assumes "monom_inv ((x,p) # m)"
and "y  x" shows "y  fst  set m"
proof -
define M where "M = map fst m"
from assms[unfolded monom_inv_def]
have "distinct (x # map fst m)" "sorted (x # map fst m)"  by auto
with assms(2) have "y  set (map fst m)" unfolding M_def[symmetric]
by (induct M, auto)
thus ?thesis by auto
qed

lemma eq_monom_sum_var_list: assumes "monom_inv m" and "monom_inv n"
shows "(m = n) = ( x. sum_var_list m x = sum_var_list n x)" (is "?l = ?r")
using assms
proof (induct m arbitrary: n)
case Nil
show ?case
proof (cases n)
case (Cons yp nn)
obtain y p where yp: "yp = (y,p)" by (cases yp, auto)
with Cons Nil(2)[unfolded monom_inv_def] have p: "0 < p" by auto
show ?thesis by (simp add: Cons, rule exI[of _ y], simp add: sum_var_list_def yp p)
qed simp
next
case (Cons xp m)
obtain x p where xp: "xp = (x,p)" by (cases xp, auto)
with Cons(2) have p: "0 < p" and x: "x  fst  set m" and m: "monom_inv m" unfolding monom_inv_def
by (auto)
show ?case
proof (cases n)
case Nil
thus ?thesis by (auto simp: xp sum_var_list_def p intro!: exI[of _ x])
next
case n: (Cons yq n')
from Cons(3)[unfolded n] have n': "monom_inv n'" by (auto simp: monom_inv_def)
show ?thesis
proof (cases "yq = xp")
case True
show ?thesis unfolding n True using Cons(1)[OF m n'] by (auto simp: xp sum_var_list_def)
next
case False
obtain y q where yq: "yq = (y,q)" by force
from Cons(3)[unfolded n yq monom_inv_def] have q: "q > 0" by auto
define z where "z = min x y"
have zm: "z  fst  set m" using Cons(2) unfolding xp z_def
by (rule monom_inv_Cons, simp)
have zn': "z  fst  set n'" using Cons(3) unfolding n yq z_def
by (rule monom_inv_Cons, simp)
have smz: "sum_var_list (xp # m) z = sum_var_list [(x,p)] z"
using sum_var_list_not[OF zm] by (simp add: sum_var_list_def xp)
also have "  sum_var_list [(y,q)] z" using False unfolding xp yq
by (auto simp: sum_var_list_def z_def p q min_def)
also have "sum_var_list [(y,q)] z = sum_var_list n z"
using sum_var_list_not[OF zn'] by (simp add: sum_var_list_def n yq)
finally show ?thesis using False unfolding n by auto
qed
qed
qed

text ‹
equality of monomials is also a complete for several carriers, e.g. the naturals, integers, where $x^p = x^q$ implies $p = q$.
note that it is not complete for carriers like the Booleans where e.g. $x^{Suc(m)} = x^{Suc(n)}$ for all $n,m$.
›
(*
lemma eq_monom_inv:
fixes m :: "'v :: linorder monom_list"
assumes exp_inject: "⋀ p q :: nat. ∃ base :: 'a :: poly_carrier. base^p = base^q ⟹ p = q"
and m: "monom_inv m" and n: "monom_inv n"
shows "(m = n) = (∀ α :: ('v,'a :: poly_carrier)assign. eval_monom_list α m = eval_monom_list α n)"
proof(intro iffI allI, rule eq_monom_list)
assume "∀ α :: ('v,'a :: poly_carrier)assign. eval_monom_list α m = eval_monom_list α n"
with m n show "m = n"
proof (induct m arbitrary: n)
case Nil
show ?case
proof (cases n)
case (Cons yq nn)
with Nil obtain y q where yq: "yq = (y,q)" and "1 ≤ q" by (cases yq, auto simp: monom_inv_def)
then obtain qq where q: "q = Suc (qq)" by (cases q, auto)
from Nil(3) have "1 = eval_monom_list (λ x. 0 :: 'a) n" (is "?one = _") by simp
also have "… = 0" by (simp add: Cons yq q)
finally show ?thesis by simp
qed simp
next
case (Cons xp m) note mCons = this
show ?case
proof (cases xp)
case (Pair x p)
let ?ass = "(λ v y. if x = y then v else 1 :: 'a)"
{
fix v :: 'a and m :: "'v monom_list"
assume "x ∉ fst  (set m)"
hence "eval_monom_list (?ass v) m = 1"
proof (induct m)
case (Cons yp m)
thus ?case
by (cases yp, cases "fst yp = x", auto)
qed simp
} note ass = this
from Cons(2)[unfolded Pair] obtain pp where p: "p = Suc pp" and xm: "x ∉ fst  (set m)" unfolding monom_inv_def by (cases p, auto)
from ass[OF xm] have "⋀ v. eval_monom_list (?ass v) (xp # m) = v * v^pp" by (simp add: Pair p)
with Cons(4) have eval: "⋀ v. eval_monom_list (?ass v) n = v * v^pp" by auto
show ?thesis
proof (cases "List.extract (λ yq. fst yq = x) n")
case None
with ass[of n] have "⋀ v. eval_monom_list (?ass v) n = 1" by (auto simp: extract_None_iff)
from this[of 0] eval[of 0] show ?thesis by simp
next
case (Some res)
obtain n1 yq n2 where "res = (n1,yq,n2)" by (cases res, auto)
then obtain y q where "res = (n1,(y,q),n2)" by (cases yq, auto)
from extract_SomeE[OF Some[simplified this]] mCons(2)  Some Pair this have n: "n = n1 @ (x,q) # n2" and res: "res = (n1,(x,q),n2)" by auto
from mCons(3)[unfolded n] have xn: "x ∉ fst  (set (n1 @ n2))" unfolding monom_inv_def by auto
have "⋀ v. eval_monom_list (?ass v) n = v^q * eval_monom_list  (?ass v) (n1 @ n2)" unfolding n by (auto simp: field_simps)
from eval[unfolded this ass[OF xn]] have id: "⋀ v :: 'a. v^p = v^q" using p by auto
from exp_inject[of p q] id have pq: "p = q" by auto
have rec: "((xp # m) =m n) = (m =m (n1 @ n2))" by (simp add: Pair Some res pq)
have ass: "∀α :: ('v,'a)assign. eval_monom_list  α m = eval_monom_list α (n1 @ n2)"
proof
fix α :: "('v,'a)assign"
show "eval_monom_list α m = eval_monom_list α (n1 @ n2)"
proof (rule ccontr)
assume neq: "¬ ?thesis"
let ?ass =  "λ y :: 'v. if x = y then 1 :: 'a else α y"
{
fix m :: "'v monom_list"
assume "x ∉ fst  set m"
hence "eval_monom_list α m = eval_monom_list ?ass m"
by (induct m, auto)
} note ass = this
have "eval_monom_list α (n1 @ n2) = eval_monom_list ?ass (n1 @ n2)" using ass[OF xn] .
also have "… = eval_monom_list ?ass n" unfolding n by auto
also have "… = eval_monom_list ?ass ((xp # m))" using mCons(4) by auto
also have "… = eval_monom_list ?ass m" unfolding Pair by simp
also have "… = eval_monom_list α m" using ass[OF xm] by simp
also have "… ≠ eval_monom_list α (n1 @ n2)" by (rule neq)
finally show False by simp
qed
qed
from mCons(2) mCons(3) have "monom_inv m" and "monom_inv (n1 @ n2)" unfolding monom_inv_def n by auto
from mCons(1)[OF this ass] rec show ?thesis by simp
qed
qed
qed
qed simp  *)

abbreviation (input) monom_list_vars :: "'a monom_list  'a set"
where "monom_list_vars m  fst  set m"

fun monom_mult_list :: "'a monom_list  'a monom_list  'a monom_list" where
"monom_mult_list [] n = n"
| "monom_mult_list ((x,p) # m) n = (case n of
Nil  (x,p) # m
| (y,q) # n'  if x = y then (x,p + q) # monom_mult_list m n' else
if x < y then (x,p) # monom_mult_list m n else (y,q) # monom_mult_list ((x,p) # m) n')"

lemma monom_list_mult_list_vars:
by (induct m1 m2 rule: monom_mult_list.induct, auto split: list.splits)

lemma monom_mult_list_inv: "monom_inv m1  monom_inv m2  monom_inv (monom_mult_list m1 m2)"
proof (induct m1 m2 rule: monom_mult_list.induct)
case (2 x p m n')
note IH = 2(1-3)
note xpm = 2(4)
note n' = 2(5)
show ?case
proof (cases n')
case Nil
with xpm show ?thesis by auto
next
case (Cons yq n)
then obtain y q where id: "n' = ((y,q) # n)" by (cases yq, auto)
from xpm have m: "monom_inv m" and p: "p > 0" and x: "x  fst  set m"
and xm: " z. z  fst  set m  x  z"
unfolding monom_inv_def by (auto)
from n'[unfolded id] have n: "monom_inv n" and q: "q > 0" and y: "y  fst  set n"
and yn: " z. z  fst  set n  y  z"
unfolding monom_inv_def by (auto)
show ?thesis
proof (cases "x = y")
case True
hence res: "monom_mult_list ((x, p) # m) n' = (x, p + q) # monom_mult_list m n"
from IH(1)[OF id refl True m n] have inv: "monom_inv (monom_mult_list m n)" by simp
show ?thesis unfolding res using inv p x y True xm yn
by (fastforce simp add: monom_inv_def monom_list_mult_list_vars)
next
case False
show ?thesis
proof (cases "x < y")
case True
hence res: "monom_mult_list ((x, p) # m) n' = (x,p) # monom_mult_list m n'"
from IH(2)[OF id refl False True m n'] have inv: "monom_inv (monom_mult_list m n')" .
show ?thesis unfolding res using inv p x y True xm yn unfolding id
by (fastforce simp add: monom_inv_def monom_list_mult_list_vars)
next
case gt: False
with False have lt: "y < x" by auto
hence res: "monom_mult_list ((x, p) # m) n' = (y,q) # monom_mult_list ((x, p) # m) n"
using False by (auto simp add: id)
from lt have zm: "z  x  (z,b)  set m" for z b using xm[of z] x by force
from zm[of y] lt have ym: "(y,b)  set m" for b by auto
from yn have yn': "(a, b)  set n  y  a" for a b by force
from IH(3)[OF id refl False gt xpm n] have inv: "monom_inv (monom_mult_list ((x, p) # m) n)" .
define xpm where "xpm = ((x,p) # m)"
have xpm': "fst  set xpm = insert x (fst  set m)" unfolding xpm_def by auto
show ?thesis unfolding res using inv p q x y False gt ym lt xm yn' zm xpm' unfolding id xpm_def[symmetric]
by (auto simp add: monom_inv_def monom_list_mult_list_vars)
qed
qed
qed
qed auto

lemma monom_inv_ConsD: "monom_inv (x # xs)  monom_inv xs"
by (auto simp: monom_inv_def)

lemma sum_var_list_monom_mult_list:
proof (induct m n rule: monom_mult_list.induct)
case (2 x p m n)
thus ?case by (cases n; cases "hd n", auto split: if_splits simp: sum_var_list_def)
qed (auto simp: sum_var_list_def)

lemma monom_mult_list_inj: assumes m: "monom_inv m" and m1: "monom_inv m1" and m2: "monom_inv m2"
and eq: "monom_mult_list m m1 = monom_mult_list m m2"
shows "m1 = m2"
proof -
from eq sum_var_list_monom_mult_list[of m] show ?thesis
by (auto simp: eq_monom_sum_var_list[OF m1 m2] eq_monom_sum_var_list[OF monom_mult_list_inv[OF m m1] monom_mult_list_inv[OF m m2]])
qed

lemma monom_mult_list[simp]:
by (induct m n rule: monom_mult_list.induct, auto split: list.splits prod.splits simp: field_simps power_add)
end

declare monom_mult_list.simps[simp del]

typedef (overloaded) 'v monom = "Collect (monom_inv :: 'v :: linorder monom_list  bool)"
by (rule exI[of _ ], auto simp: monom_inv_def)

setup_lifting type_definition_monom

lift_definition eval_monom :: "('v :: linorder,'a :: comm_semiring_1)assign  'v monom  'a"
is eval_monom_list .

lift_definition sum_var :: "'v :: linorder monom  'v  nat" is sum_var_list .

instantiation monom :: (linorder) comm_monoid_mult
begin

lift_definition times_monom :: "'a monom  'a monom  'a monom" is monom_mult_list
using monom_mult_list_inv by auto

lift_definition one_monom :: "'a monom" is Nil
by (auto simp: monom_inv_def)

instance
proof
fix a b c :: "'a monom"
show "a * b * c = a * (b * c)"
by (transfer, auto simp: eq_monom_sum_var_list monom_mult_list_inv sum_var_list_monom_mult_list)
show "a * b = b * a"
by (transfer, auto simp: eq_monom_sum_var_list monom_mult_list_inv sum_var_list_monom_mult_list)
show "1 * a = a"
by (transfer, auto simp: eq_monom_sum_var_list monom_mult_list_inv sum_var_list_monom_mult_list monom_mult_list.simps)
qed
end

lemma eq_monom_sum_var: "m = n  ( x. sum_var m x = sum_var n x)"
by (transfer, auto simp: eq_monom_sum_var_list)

lemma eval_monom_mult[simp]: "eval_monom α (m * n) = eval_monom α m * eval_monom α n"
by (transfer, rule monom_mult_list)

lemma sum_var_monom_mult:  "sum_var (m * n) x = sum_var m x + sum_var n x"
by (transfer, rule sum_var_list_monom_mult_list)

lemma monom_mult_inj: fixes m1 :: "_ monom"
shows "m * m1 = m * m2  m1 = m2"
by (transfer, rule monom_mult_list_inj, auto)

lemma one_monom_inv_sum_var_inv[simp]: "sum_var 1 x = 0"
by (transfer, auto simp: sum_var_list_def)

lemma eval_monom_1[simp]:
by (transfer, auto)

lift_definition var_monom :: "'v :: linorder  'v monom" is "λ x. [(x,1)]"
by (auto simp: monom_inv_def)

lemma var_monom_1[simp]: "var_monom x  1"
by (transfer, auto)

lemma eval_var_monom[simp]: "eval_monom α (var_monom x) = α x"
by (transfer, auto)

lemma sum_var_monom_var: "sum_var (var_monom x) y = (if x = y then 1 else 0)"
by (transfer, auto simp: sum_var_list_def)

instantiation monom :: ("{equal,linorder}")equal
begin

lift_definition equal_monom :: "'a monom  'a monom  bool" is "(=)" .

instance by (standard, transfer, auto)
end

text ‹
Polynomials are represented with as sum of monomials multiplied by some coefficient
›
type_synonym ('v,'a)poly = "('v monom × 'a)list"

text ‹
The polynomials we construct satisfy the following invariants:
\begin{itemize}
\item all coefficients are non-zero
\item the monomial list is distinct
\end{itemize}
›

definition poly_inv :: "('v,'a :: zero)poly  bool"
where "poly_inv p  ( c  snd  set p. c  0)  distinct (map fst p)"

abbreviation eval_monomc where "eval_monomc α mc  eval_monom α (fst mc) * (snd mc)"

primrec eval_poly :: "('v :: linorder, 'a :: comm_semiring_1)assign  ('v,'a)poly  'a" where
"eval_poly α [] = 0"
| "eval_poly α (mc # p) = eval_monomc α mc + eval_poly α p"

definition poly_const :: "'a :: zero  ('v :: linorder,'a)poly" where
"poly_const a = (if a = 0 then [] else [(1,a)])"

lemma poly_const[simp]: "eval_poly α (poly_const a) = a"
unfolding poly_const_def by auto

lemma poly_const_inv: "poly_inv (poly_const a)"
unfolding poly_const_def poly_inv_def by auto

fun poly_add :: "('v,'a)poly  ('v,'a :: semiring_0)poly  ('v,'a)poly" where
| "poly_add ((m,c) # p) q = (case List.extract (λ mc. fst mc = m) q of
None  (m,c) # poly_add p q
| Some (q1,(_,d),q2)  if (c+d = 0) then poly_add p (q1 @ q2) else (m,c+d) # poly_add p (q1 @ q2))"

lemma eval_poly_append[simp]: "eval_poly α (mc1 @ mc2) = eval_poly α mc1 + eval_poly α mc2"
by (induct mc1, auto simp: field_simps)

abbreviation poly_monoms :: "('v,'a)poly  'v monom set"
where "poly_monoms p  fst  set p"

proof (induct p1 arbitrary: p2)
case (Cons mc p)
obtain m c where mc: "mc = (m,c)" by (cases mc, auto)
hence m: "m  poly_monoms (mc # p1)" by auto
show ?case
proof (cases "List.extract (λ nd. fst nd = m) p2")
case None
with Cons m show ?thesis by (auto simp: mc)
next
case (Some res)
obtain q1 md q2 where res: "res = (q1,md,q2)" by (cases res, auto)
from extract_SomeE[OF Some[simplified res]] res obtain d where q: "p2 = q1 @ (m,d) # q2" and res: "res = (q1,(m,d),q2)" by (cases md, auto)
show ?thesis
by (simp add: mc Some res, rule subset_trans[OF Cons[of "q1  q2"]], auto simp: q)
qed
qed simp

proof (induct p arbitrary: q)
case (Cons mc p)
obtain m c where mc: "mc = (m,c)" by (cases mc, auto)
with Cons(2) have p: "poly_inv p" and c: "c  0" and mp: " mm  fst  set p. (¬ mm = m)" unfolding poly_inv_def by auto
show ?case
proof (cases "List.extract (λ mc. fst mc = m) q")
case None
hence mq: " mm  fst  set q. ¬ mm = m" by (auto simp: extract_None_iff)
{
fix mm
assume "mm  fst  set (poly_add p q)"
then obtain dd where "(mm,dd)  set (poly_add p q)" by auto
with poly_add_monoms have "mm  poly_monoms p  mm  poly_monoms q" by force
hence "¬ mm = m" using mp mq by auto
} note main = this
show ?thesis using Cons(1)[OF p Cons(3)] unfolding poly_inv_def using main by (auto simp add: None mc c)
next
case (Some res)
obtain q1 md q2 where res: "res = (q1,md,q2)" by (cases res, auto)
from extract_SomeE[OF Some[simplified res]] res obtain d where q: "q = q1 @ (m,d) # q2" and res: "res = (q1,(m,d),q2)" by (cases md, auto)
from q Cons(3) have q1q2: "poly_inv (q1 @ q2)" unfolding poly_inv_def by auto
from Cons(1)[OF p q1q2]  have main1: "poly_inv (poly_add p (q1 @ q2))" .
{
fix mm
assume "mm  fst  set (poly_add p (q1 @ q2))"
then obtain dd where "(mm,dd)  set (poly_add p (q1 @ q2))" by auto
with poly_add_monoms have "mm  poly_monoms p  mm  poly_monoms (q1 @ q2)" by force
hence "mm  m"
proof
assume "mm  poly_monoms p"
thus ?thesis using mp  by auto
next
assume member: "mm  poly_monoms (q1 @ q2)"
from member have "mm  poly_monoms q1  mm  poly_monoms q2" by auto
thus "mm  m"
proof
assume "mm  poly_monoms q2"
with Cons(3)[simplified q]
show ?thesis unfolding poly_inv_def by auto
next
assume "mm  poly_monoms q1"
with Cons(3)[simplified q]
show ?thesis unfolding poly_inv_def by auto
qed
qed
} note main2 = this
show ?thesis using  main1[unfolded poly_inv_def] main2
by (auto simp: poly_inv_def mc Some res)
qed
qed simp

lemma poly_add[simp]: "eval_poly α (poly_add p q) = eval_poly α p + eval_poly α q"
proof (induct p arbitrary: q)
case (Cons mc p)
obtain m c where mc: "mc = (m,c)" by (cases mc, auto)
show ?case
proof (cases "List.extract (λ mc. fst mc = m) q")
case None
show ?thesis by (simp add: Cons[of q] mc None field_simps)
next
case (Some res)
obtain q1 md q2 where res: "res = (q1,md,q2)" by (cases res, auto)
from extract_SomeE[OF Some[simplified res]] res obtain d where q: "q = q1 @ (m,d) # q2" and res: "res = (q1,(m,d),q2)" by (cases md, auto)
{
fix x
assume c: "c + d = 0"
have "c * x + d * x = (c + d) * x" by (auto simp: field_simps)
also have " = 0 * x" by (simp only: c)
finally have "c * x + d * x = 0" by simp
} note id = this
show ?thesis
by (simp add: Cons[of "q1 @ q2"] mc Some res, simp only: q, simp add: field_simps, auto simp: field_simps id)
qed
qed simp

fun monom_mult_poly :: "('v :: linorder monom × 'a)  ('v,'a :: semiring_0)poly  ('v,'a)poly" where
"monom_mult_poly _ [] = []"
| "monom_mult_poly (m,c) ((m',d) # p) = (if c * d = 0 then monom_mult_poly (m,c) p else (m * m', c * d) # monom_mult_poly (m,c) p)"

lemma monom_mult_poly_inv: "poly_inv p  poly_inv (monom_mult_poly (m,c) p)"
proof (induct p)
case Nil thus ?case by (simp add: poly_inv_def)
next
case (Cons md p)
obtain m' d where md: "md = (m',d)" by (cases md, auto)
with Cons(2) have p: "poly_inv p" unfolding poly_inv_def by auto
from Cons(1)[OF p] have prod: "poly_inv (monom_mult_poly (m,c) p)" .
{
fix mm
assume "mm  fst  set (monom_mult_poly (m,c) p)"
and two: "mm = m * m'"
then obtain dd where one: "(mm,dd)  set (monom_mult_poly (m,c) p)" by auto
have "poly_monoms (monom_mult_poly (m,c) p)  (*) m  poly_monoms p"
proof (induct p, simp)
case (Cons md p)
thus ?case
by (cases md, auto)
qed
with one have "mm  (*) m ` poly_monoms p" by force
then obtain mmm where mmm: "mmm  poly_monoms p" and mm: "mm = m * mmm" by blast
from Cons(2)[simplified md] mmm have not1: "¬ mmm = m'" unfolding poly_inv_def by auto
from mm two have "m * mmm = m * m'" by simp
from monom_mult_inj[OF this] not1
have False by simp
}
thus ?case
by (simp add: md prod, intro impI, auto simp: poly_inv_def prod[simplified poly_inv_def])
qed

lemma monom_mult_poly[simp]: "eval_poly α (monom_mult_poly mc p) = eval_monomc α mc * eval_poly α p"
proof (cases mc)
case (Pair m c)
show ?thesis
proof (simp add: Pair, induct p)
case (Cons nd q)
obtain n d where nd: "nd = (n,d)" by (cases nd, auto)
show ?case
proof (cases "c * d = 0")
case False
thus ?thesis by (simp add: nd Cons field_simps)
next
case True
let ?l = "c * (d * (eval_monom α m * eval_monom α n))"
have "?l = (c * d) * (eval_monom α m * eval_monom α n)"
by (simp only: field_simps)
also have " = 0" by (simp only: True, simp add: field_simps)
finally have l: "?l = 0" .
show ?thesis
qed
qed simp
qed

declare monom_mult_poly.simps[simp del]

definition poly_minus :: "('v :: linorder,'a :: ring_1)poly  ('v,'a)poly  ('v,'a)poly" where
"poly_minus f g = poly_add f (monom_mult_poly (1,-1) g)"

lemma poly_minus[simp]: "eval_poly α (poly_minus f g) = eval_poly α f - eval_poly α g"
unfolding poly_minus_def by simp

lemma poly_minus_inv: "poly_inv f  poly_inv g  poly_inv (poly_minus f g)"
unfolding poly_minus_def by (intro poly_add_inv monom_mult_poly_inv)

fun poly_mult :: "('v :: linorder, 'a :: semiring_0)poly  ('v,'a)poly  ('v,'a)poly" where
"poly_mult [] q = []"
| "poly_mult (mc # p) q = poly_add (monom_mult_poly mc q) (poly_mult p q)"

lemma poly_mult_inv: assumes p: "poly_inv p" and q: "poly_inv q"
shows "poly_inv (poly_mult p q)"
using p
proof (induct p)
case Nil thus ?case by (simp add: poly_inv_def)
next
case (Cons mc p)
obtain m c where mc: "mc = (m,c)" by (cases mc, auto)
with Cons(2) have p: "poly_inv p" unfolding poly_inv_def by auto
show ?case
qed

lemma poly_mult[simp]: "eval_poly α (poly_mult p q) = eval_poly α p * eval_poly α q"
by (induct p, auto simp: field_simps)

declare poly_mult.simps[simp del]

definition zero_poly :: "('v,'a)poly"
where "zero_poly  []"

lemma zero_poly_inv:  unfolding zero_poly_def poly_inv_def by auto

definition one_poly :: "('v :: linorder,'a :: semiring_1)poly" where
"one_poly  [(1,1)]"

lemma one_poly_inv:  unfolding one_poly_def poly_inv_def monom_inv_def by auto

lemma poly_one[simp]:
unfolding one_poly_def by simp

lemma poly_zero_mult:  unfolding zero_poly_def using poly_mult.simps by auto

text ‹equality of polynomials›
definition eq_poly :: "('v :: linorder, 'a :: comm_semiring_1)poly  ('v,'a)poly  bool" (infix "=p" 51)
where "p =p q   α. eval_poly α p = eval_poly α q"

lemma poly_one_mult:
unfolding eq_poly_def one_poly_def by simp

lemma eq_poly_refl[simp]: "p =p p" unfolding eq_poly_def by auto

lemma eq_poly_trans[trans]: "p1 =p p2; p2 =p p3  p1 =p p3"
unfolding eq_poly_def by auto

lemma poly_mult_comm: "poly_mult p q =p poly_mult q p" unfolding eq_poly_def by (auto simp: field_simps)

lemma poly_mult_assoc: "poly_mult p1 (poly_mult p2 p3) =p poly_mult (poly_mult p1 p2) p3" unfolding eq_poly_def by (auto simp: field_simps)

lemma poly_distrib: "poly_mult p (poly_add q1 q2) =p poly_add (poly_mult p q1) (poly_mult p q2)" unfolding eq_poly_def by (auto simp: field_simps)

subsection ‹Computing normal forms of polynomials›
fun
poly_of :: "('v :: linorder,'a :: comm_semiring_1)tpoly  ('v,'a)poly"
where "poly_of (PNum i) = (if i = 0 then [] else [(1,i)])"
| "poly_of (PVar x) = [(var_monom x,1)]"
| "poly_of (PSum []) = zero_poly"
| "poly_of (PSum (p # ps)) = (poly_add (poly_of p) (poly_of (PSum ps)))"
| "poly_of (PMult []) = one_poly"
| "poly_of (PMult (p # ps)) = (poly_mult (poly_of p) (poly_of (PMult ps)))"

text ‹
evaluation is preserved by poly\_of
›
lemma poly_of: "eval_poly α (poly_of p) = eval_tpoly α p"
by (induct p rule: poly_of.induct, (simp add: zero_poly_def one_poly_def)+)

text ‹
poly\_of only generates polynomials that satisfy the invariant
›
lemma poly_of_inv: "poly_inv (poly_of p)"
by (induct p rule: poly_of.induct,

subsection ‹Powers and substitutions of polynomials›
fun poly_power :: "('v :: linorder, 'a :: comm_semiring_1)poly  nat  ('v,'a)poly" where
"poly_power _ 0 = one_poly"
| "poly_power p (Suc n) = poly_mult p (poly_power p n)"

lemma poly_power[simp]: "eval_poly α (poly_power p n) = (eval_poly α p) ^ n"
by (induct n, auto simp: one_poly_def)

lemma poly_power_inv: assumes p: "poly_inv p"
shows "poly_inv (poly_power p n)"

declare poly_power.simps[simp del]

fun monom_list_subst :: "('v  ('w :: linorder,'a :: comm_semiring_1)poly)  'v monom_list  ('w,'a)poly" where
"monom_list_subst σ [] = one_poly"
| "monom_list_subst σ ((x,p) # m) = poly_mult (poly_power (σ x) p) (monom_list_subst σ m)"

lift_definition monom_list :: "'v :: linorder monom  'v monom_list" is "λ x. x" .

definition monom_subst :: "('v :: linorder  ('w :: linorder,'a :: comm_semiring_1)poly)  'v monom  ('w,'a)poly" where
"monom_subst σ m = monom_list_subst σ (monom_list m)"

lemma monom_list_subst_inv: assumes sub: " x. poly_inv (σ x)"
shows "poly_inv (monom_list_subst σ m)"
proof (induct m)
case Nil thus ?case by (simp add: one_poly_inv)
next
case (Cons xp m)
obtain x p where xp: "xp = (x,p)" by (cases xp, auto)
show ?case by (simp add: xp, rule poly_mult_inv[OF poly_power_inv[OF sub] Cons])
qed

lemma monom_subst_inv: assumes sub: " x. poly_inv (σ x)"
shows "poly_inv (monom_subst σ m)"
unfolding monom_subst_def by (rule monom_list_subst_inv[OF sub])

lemma monom_subst[simp]: "eval_poly α (monom_subst σ m) = eval_monom (λ v. eval_poly α (σ v)) m"
unfolding monom_subst_def
proof (transfer fixing: α σ, clarsimp)
fix m
show "monom_inv m  eval_poly α (monom_list_subst σ m) = eval_monom_list (λv. eval_poly α (σ v)) m"
by (induct m, simp add: one_poly_def, auto simp: field_simps monom_inv_ConsD)
qed

fun poly_subst :: "('v :: linorder  ('w :: linorder,'a :: comm_semiring_1)poly)  ('v,'a)poly  ('w,'a)poly" where
"poly_subst σ [] = zero_poly"
| "poly_subst σ ((m,c) # p) = poly_add (poly_mult [(1,c)] (monom_subst σ m)) (poly_subst σ p)"

lemma poly_subst_inv: assumes sub: " x. poly_inv (σ x)" and p: "poly_inv p"
shows "poly_inv (poly_subst σ p)"
using p
proof (induct p)
case Nil thus ?case by (simp add: zero_poly_inv)
next
case (Cons mc p)
obtain m c where mc: "mc = (m,c)" by (cases mc, auto)
with Cons(2) have c: "c  0" and p: "poly_inv p" unfolding poly_inv_def by auto
from c have c: "poly_inv [(1,c)]" unfolding poly_inv_def monom_inv_def by auto
show ?case
by (simp add: mc, rule poly_add_inv[OF poly_mult_inv[OF c monom_subst_inv[OF sub]] Cons(1)[OF p]])
qed

lemma poly_subst: "eval_poly α (poly_subst σ p) = eval_poly (λ v. eval_poly α (σ v)) p"
by (induct p, simp add: zero_poly_def, auto simp: field_simps)

lemma eval_poly_subst:
assumes eq: " w. f w = eval_poly g (q w)"
shows "eval_poly f p = eval_poly g (poly_subst q p)"
proof (induct p)
case Nil thus ?case by (simp add: zero_poly_def)
next
case (Cons mc p)
obtain m c where mc: "mc = (m,c)" by (cases mc, auto)
have id: "eval_monom f m =  eval_monom (λv. eval_poly g (q v)) m"
proof (transfer fixing: f g q, clarsimp)
fix m
show "eval_monom_list f m = eval_monom_list (λv. eval_poly g (q v)) m"
proof (induct m)
case (Cons wp m)
obtain w p where wp: "wp = (w,p)" by (cases wp, auto)
show ?case
by (simp add: wp Cons eq)
qed simp
qed
show ?case
qed

lift_definition monom_vars_list :: "'v :: linorder monom  'v list" is "map fst" .

lemma monom_vars_list_subst: assumes " w. w  set (monom_vars_list m)  f w = g w"
shows "monom_subst f m = monom_subst g m"
unfolding monom_subst_def using assms
proof (transfer fixing: f g)
fix m :: "'a monom_list"
assume eq: "w. w  set (map fst m)  f w = g w"
thus
proof (induct m)
case (Cons wn m)
hence rec:  and eq: "f (fst wn) = g (fst wn)" by auto
show ?case
proof (cases wn)
case (Pair w n)
with eq rec show ?thesis by auto
qed
qed simp
qed

lemma eval_monom_vars_list: assumes " x. x  set (monom_vars_list xs)  α x = β x"
shows "eval_monom α xs = eval_monom β xs" using assms
proof (transfer fixing: α β)
fix xs :: "'a monom_list"
assume eq: "w. w  set (map fst xs)  α w = β w"
thus "eval_monom_list α xs = eval_monom_list β xs"
proof (induct xs)
case (Cons xi xs)
hence IH: "eval_monom_list α xs = eval_monom_list β xs" by auto
obtain x i where xi: "xi = (x,i)" by force
from Cons(2) xi have "α x = β x" by auto
with IH show ?case unfolding xi by auto
qed simp
qed

definition monom_vars where "monom_vars m = set (monom_vars_list m)"

lemma monom_vars_list_1[simp]:
by transfer auto

lemma monom_vars_list_var_monom[simp]: "monom_vars_list (var_monom x) = [x]"
by transfer auto

lemma monom_vars_eval_monom:
"( x. x  monom_vars m  f x = g x)  eval_monom f m = eval_monom g m"
by (rule eval_monom_vars_list, auto simp: monom_vars_def)

(* the list of variables occurring in p *)
definition poly_vars_list :: "('v :: linorder,'a)poly  'v list" where
"poly_vars_list p = remdups (concat (map (monom_vars_list o fst) p))"

definition poly_vars :: "('v :: linorder,'a)poly  'v set" where
"poly_vars p = set (concat (map (monom_vars_list o fst) p))"

lemma poly_vars_list[simp]:
unfolding poly_vars_list_def poly_vars_def by auto

lemma poly_vars: assumes eq: " w. w  poly_vars p  f w = g w"
shows "poly_subst f p = poly_subst g p"
using eq
proof (induct p)
case (Cons mc p)
hence rec: "poly_subst f p = poly_subst g p" unfolding poly_vars_def by auto
show ?case
proof (cases mc)
case (Pair m c)
with Cons(2) have " w. w  set (monom_vars_list m)  f w = g w" unfolding poly_vars_def by auto
hence "monom_subst f m = monom_subst g m"
by (rule monom_vars_list_subst)
with rec Pair show ?thesis by auto
qed
qed simp

lemma poly_var: assumes pv: "v  poly_vars p" and diff: " w. v  w  f w = g w"
shows "poly_subst f p = poly_subst g p"
proof (rule poly_vars)
fix w
assume "w  poly_vars p"
thus "f w = g w" using pv diff by (cases "v = w", auto)
qed

lemma eval_poly_vars: assumes " x. x  poly_vars p  α x = β x"
shows "eval_poly α p = eval_poly β p"
using assms
proof (induct p)
case Nil thus ?case by simp
next
case (Cons m p)
from Cons(2) have " x. x  poly_vars p  α x = β x" unfolding poly_vars_def by auto
from Cons(1)[OF this] have IH: "eval_poly α p = eval_poly β p" .
obtain xs c where m: "m = (xs,c)" by force
from Cons(2) have " x. x  set (monom_vars_list xs)  α x = β x" unfolding poly_vars_def m by auto
hence "eval_monom α xs = eval_monom β xs"
by (rule eval_monom_vars_list)
thus ?case unfolding eval_poly.simps IH m by auto
qed

declare poly_subst.simps[simp del]

subsection ‹
Polynomial orders
›

definition pos_assign :: "('v,'a :: ordered_semiring_0)assign  bool"
where "pos_assign α = ( x. α x  0)"

definition poly_ge :: "('v :: linorder,'a :: poly_carrier)poly  ('v,'a)poly  bool" (infix "≥p" 51)
where "p ≥p q = ( α. pos_assign α  eval_poly α p  eval_poly α q)"

lemma poly_ge_refl[simp]: "p ≥p p"
unfolding poly_ge_def using ge_refl by auto

lemma poly_ge_trans[trans]: "p1 ≥p p2; p2 ≥p p3  p1 ≥p p3"
unfolding poly_ge_def using ge_trans by blast

lemma pos_assign_monom_list: fixes α :: "('v :: linorder, 'a :: poly_carrier)assign"
assumes pos: "pos_assign α"
shows
proof (induct m)
case Nil thus ?case by (simp add: one_ge_zero)
next
case (Cons xp m)
show ?case
proof (cases xp)
case (Pair x p)
from pos[unfolded pos_assign_def] have ge: "α x  0" by simp
have ge: "α x ^ p  0"
proof (induct p)
case 0 thus ?case by (simp add: one_ge_zero)
next
case (Suc p)
from ge_trans[OF times_left_mono[OF ge Suc] times_right_mono[OF ge_refl ge]]
show ?case by (simp add: field_simps)
qed
from ge_trans[OF times_right_mono[OF Cons ge] times_left_mono[OF ge_refl Cons]]
show ?thesis
qed
qed

lemma pos_assign_monom: fixes α :: "('v :: linorder, 'a :: poly_carrier)assign"
assumes pos: "pos_assign α"
shows "eval_monom α m  0"
by (transfer fixing: α, rule pos_assign_monom_list[OF pos])

lemma pos_assign_poly:   assumes pos: "pos_assign α"
and p: "p ≥p zero_poly"
shows "eval_poly α p  0"
proof -
from p[unfolded poly_ge_def zero_poly_def] pos
show ?thesis by auto
qed

using assms unfolding poly_ge_def by (auto simp: field_simps plus_left_mono)

lemma poly_mult_ge_mono: assumes "p1 ≥p p2" and "q ≥p zero_poly"
shows "poly_mult p1 q ≥p poly_mult p2 q"
using assms unfolding poly_ge_def zero_poly_def by (auto simp: times_left_mono)

context poly_order_carrier
begin

definition poly_gt :: "('v :: linorder,'a)poly  ('v,'a)poly  bool" (infix ">p" 51)
where "p >p q = ( α. pos_assign α  eval_poly α p  eval_poly α q)"

lemma poly_gt_imp_poly_ge: "p >p q  p ≥p q" unfolding poly_ge_def poly_gt_def using gt_imp_ge by blast

abbreviation poly_GT :: "('v :: linorder,'a)poly rel"
where "poly_GT  {(p,q) | p q. p >p q  q ≥p zero_poly}"

lemma poly_compat: "p1 ≥p p2; p2 >p p3  p1 >p p3"
unfolding poly_ge_def poly_gt_def using compat by blast

lemma poly_compat2: "p1 >p p2; p2 ≥p p3  p1 >p p3"
unfolding poly_ge_def poly_gt_def using compat2 by blast

lemma poly_gt_trans[trans]: "p1 >p p2; p2 >p p3  p1 >p p3"
unfolding poly_gt_def using gt_trans by blast

lemma poly_GT_SN:
proof
fix f :: "nat  ('c :: linorder,'a)poly"
assume f: " i. (f i, f (Suc i))  poly_GT"
have pos: "pos_assign ((λ x. 0) :: ('v,'a)assign)" (is "pos_assign ?ass") unfolding pos_assign_def using ge_refl by auto
obtain g where g: " i. g i = eval_poly ?ass (f i)" by auto
from f pos have " i. g (Suc i)  0  g i  g (Suc i)" unfolding poly_gt_def g using pos_assign_poly by auto
with SN show False unfolding SN_defs by blast
qed
end

text ‹monotonicity of polynomials›

lemma eval_monom_list_mono: assumes fg: " x. (f :: ('v :: linorder,'a :: poly_carrier)assign) x  g x"
and g: " x. g x  0"
shows
proof (atomize(full), induct m)
case Nil show ?case using one_ge_zero by (auto simp: ge_refl)
next
case (Cons xd m)
hence IH1:  and IH2:  by auto
obtain x d where xd: "xd = (x,d)" by force
from pow_mono[OF fg g, of x d] have fgd: "f x ^ d  g x ^ d" and gd: "g x ^ d  0" by auto
show ?case unfolding xd eval_monom_list.simps
proof (rule conjI, rule ge_trans[OF times_left_mono[OF pow_ge_zero IH1] times_right_mono[OF IH2 fgd]])
show "f x  0" by (rule ge_trans[OF fg g])
show "eval_monom_list g m * g x ^ d  0"
by (rule mult_ge_zero[OF IH2 gd])
qed
qed

lemma eval_monom_mono: assumes fg: " x. (f :: ('v :: linorder,'a :: poly_carrier)assign) x  g x"
and g: " x. g x  0"
shows "eval_monom f m  eval_monom g m" "eval_monom g m  0"
by (atomize(full), transfer fixing: f g, insert eval_monom_list_mono[of g f, OF fg g], auto)

definition poly_weak_mono_all :: "('v :: linorder,'a :: poly_carrier)poly  bool" where
"poly_weak_mono_all p   (α :: ('v,'a)assign) β. ( x. α x  β x)
pos_assign β  eval_poly α p  eval_poly β p"

lemma poly_weak_mono_all_E: assumes p:  and
ge: " x. f x ≥p g x  g x ≥p zero_poly"
shows "poly_subst f p ≥p poly_subst g p"
unfolding poly_ge_def poly_subst
proof (intro allI impI, rule p[unfolded poly_weak_mono_all_def, rule_format])
fix α :: "('c,'b)assign" and x
show "pos_assign α  eval_poly α (f x)  eval_poly α (g x)" using ge[of x] unfolding poly_ge_def by auto
next
fix α :: "('c,'b)assign"
assume alpha: "pos_assign α"
show "pos_assign (λv. eval_poly α (g v))"
unfolding pos_assign_def
proof
fix x
show "eval_poly α (g x)  0"
using ge[of x] unfolding poly_ge_def zero_poly_def using alpha by auto
qed
qed

definition poly_weak_mono :: "('v :: linorder,'a :: poly_carrier)poly  'v  bool" where
"poly_weak_mono p v   (α :: ('v,'a)assign) β. ( x. v  x  α x = β x)  pos_assign β  α v  β v  eval_poly α p  eval_poly β p"

lemma poly_weak_mono_E: assumes p: "poly_weak_mono p v"
and fgw: " w. v  w  f w = g w"
and g: " w. g w ≥p zero_poly"
and fgv: "f v ≥p g v"
shows "poly_subst f p ≥p poly_subst g p"
unfolding poly_ge_def poly_subst
proof (intro allI impI, rule p[unfolded poly_weak_mono_def, rule_format])
fix α :: "('c,'b)assign"
show "pos_assign α  eval_poly α (f v)  eval_poly α (g v)" using fgv unfolding poly_ge_def by auto
next
fix α :: "('c,'b)assign"
assume alpha: "pos_assign α"
show "pos_assign (λv. eval_poly α (g v))"
unfolding pos_assign_def
proof
fix x
show "eval_poly α (g x)  0"
using g[of x] unfolding poly_ge_def zero_poly_def using alpha by auto
qed
next
fix α :: "('c,'b)assign" and x
assume v: "v  x"
show "pos_assign α  eval_poly α (f x) = eval_poly α (g x)" using fgw[OF v] unfolding poly_ge_def by auto
qed

definition poly_weak_anti_mono :: "('v :: linorder,'a :: poly_carrier)poly  'v  bool" where
"poly_weak_anti_mono p v   (α :: ('v,'a)assign) β. ( x. v  x  α x = β x)  pos_assign β  α v  β v  eval_poly β p  eval_poly α p"

lemma poly_weak_anti_mono_E: assumes p:
and fgw: " w. v  w  f w = g w"
and g: " w. g w ≥p zero_poly"
and fgv: "f v ≥p g v"
shows "poly_subst g p ≥p poly_subst f p"
unfolding poly_ge_def poly_subst
proof (intro allI impI, rule p[unfolded poly_weak_anti_mono_def, rule_format])
fix α :: "('c,'b)assign"
show "pos_assign α  eval_poly α (f v)  eval_poly α (g v)" using fgv unfolding poly_ge_def by auto
next
fix α :: "('c,'b)assign"
assume alpha: "pos_assign α"
show "pos_assign (λv. eval_poly α (g v))"
unfolding pos_assign_def
proof
fix x
show "eval_poly α (g x)  0"
using g[of x] unfolding poly_ge_def zero_poly_def using alpha by auto
qed
next
fix α :: "('c,'b)assign" and x
assume v: "v  x"
show "pos_assign α  eval_poly α (f x) = eval_poly α (g x)" using fgw[OF v] unfolding poly_ge_def by auto
qed

lemma poly_weak_mono: fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
assumes mono: " v. v  poly_vars p  poly_weak_mono p v"
shows
unfolding poly_weak_mono_all_def
proof (intro allI impI)
fix α β :: "('v,'a)assign"
assume all: " x. α x  β x"
assume pos: "pos_assign β"
let ?ab = "λ vs v. if (v  set vs) then α v else β v"
{
fix vs :: "'v list"
assume "set vs  poly_vars p"
hence "eval_poly (?ab vs) p  eval_poly β p"
proof (induct vs)
case Nil show ?case by (simp add: ge_refl)
next
case (Cons v vs)
hence subset: "set vs  poly_vars p"  and v: "v  poly_vars p" by auto
show ?case
proof (rule ge_trans[OF mono[OF v, unfolded poly_weak_mono_def, rule_format] Cons(1)[OF subset]])
show "pos_assign (?ab vs)" unfolding pos_assign_def
proof
fix x
from pos[unfolded pos_assign_def] have beta: "β x  0" by simp
from ge_trans[OF all[rule_format] this] have alpha: "α x  0" .
from alpha beta show "?ab vs x  0" by auto
qed
show "(?ab (v # vs) v)  (?ab vs v)" using all ge_refl by auto
next
fix x
assume "v  x"
thus "(?ab (v # vs) x) = (?ab vs x)" by simp
qed
qed
}
from this[of , unfolded poly_vars_list]
have "eval_poly (λv. if v  poly_vars p then α v else β v) p  eval_poly β p" by auto
also have "eval_poly (λv. if v  poly_vars p then α v else β v) p = eval_poly α p"
by (rule eval_poly_vars, auto)
finally
show "eval_poly α p  eval_poly β p" .
qed

lemma poly_weak_mono_all: fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
assumes p:
shows "poly_weak_mono p v"
unfolding poly_weak_mono_def
proof (intro allI impI)
fix α β :: "('v,'a)assign"
assume all: "x. v  x  α x = β x"
assume pos: "pos_assign β"
assume v: "α v  β v"
show "eval_poly α p  eval_poly β p"
proof (rule p[unfolded poly_weak_mono_all_def, rule_format, OF _ pos])
fix x
show "α x  β x"
using v all ge_refl[of "β x"] by auto
qed
qed

lemma poly_weak_mono_all_pos:
fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
assumes pos_at_zero: "eval_poly (λ w. 0) p  0"
and mono:
shows "p ≥p zero_poly"
unfolding poly_ge_def zero_poly_def
proof (intro allI impI, simp)
fix  α :: "('v,'a)assign"
assume pos: "pos_assign α"
show "eval_poly α p  0"
proof -
let ?id = "λ w. poly_of (PVar w)"
let ?z = "λ w. zero_poly"
have "poly_subst ?id p ≥p poly_subst ?z p"
by (rule poly_weak_mono_all_E[OF mono],
simp, simp add: poly_ge_def zero_poly_def pos_assign_def)
hence "eval_poly α (poly_subst ?id p)  eval_poly α (poly_subst ?z p)" (is "_  ?res")
unfolding poly_ge_def using pos by simp
also have "?res = eval_poly (λ w. 0) p" by (simp add: poly_subst zero_poly_def)
also have "  0" by (rule pos_at_zero)
finally show ?thesis by  (simp add: poly_subst)
qed
qed

context poly_order_carrier
begin

definition poly_strict_mono :: "('v :: linorder,'a)poly  'v  bool" where
"poly_strict_mono p v   (α :: ('v,'a)assign) β. ( x. (v  x  α x = β x))  pos_assign β  α v  β v  eval_poly α p  eval_poly β p"

lemma poly_strict_mono_E: assumes p: "poly_strict_mono p v"
and fgw: " w. v  w  f w = g w"
and g: " w. g w ≥p zero_poly"
and fgv: "f v >p g v"
shows "poly_subst f p >p poly_subst g p"
unfolding poly_gt_def poly_subst
proof (intro allI impI, rule p[unfolded poly_strict_mono_def, rule_format])
fix α :: "('c,'a)assign"
show "pos_assign α  eval_poly α (f v)  eval_poly α (g v)" using fgv unfolding poly_gt_def by auto
next
fix α :: "('c,'a)assign"
assume alpha: "pos_assign α"
show "pos_assign (λv. eval_poly α (g v))"
unfolding pos_assign_def
proof
fix x
show "eval_poly α (g x)  0"
using g[of x] unfolding poly_ge_def zero_poly_def using alpha by auto
qed
next
fix α :: "('c,'a)assign" and x
assume v: "v  x"
show "pos_assign α  eval_poly α (f x) = eval_poly α (g x)" using fgw[OF v] unfolding poly_ge_def by auto
qed

using assms unfolding poly_gt_def by (auto simp: field_simps plus_gt_left_mono)

lemma poly_mult_gt_mono:
fixes q :: "('v :: linorder,'a)poly"
assumes gt: "p1 >p p2" and mono: "q ≥p one_poly"
shows "poly_mult p1 q >p poly_mult p2 q"
proof (unfold poly_gt_def, intro impI allI)
fix α :: "('v,'a)assign"
assume p: "pos_assign α"
with gt have gt: "eval_poly α p1  eval_poly α p2" unfolding poly_gt_def by simp
from mono p have one: "eval_poly α q  1" unfolding poly_ge_def one_poly_def by auto
show "eval_poly α (poly_mult p1 q)  eval_poly α (poly_mult p2 q)"
using times_gt_mono[OF gt one] by simp
qed
end

subsection ‹Degree of polynomials›

definition monom_list_degree :: "'v monom_list  nat" where
"monom_list_degree xps  sum_list (map snd xps)"

lift_definition monom_degree :: "'v :: linorder monom  nat" is monom_list_degree .

definition poly_degree :: "(_,'a) poly  nat" where
"poly_degree p  max_list (map (λ (m,c). monom_degree m) p)"

definition poly_coeff_sum :: "('v,'a :: ordered_ab_semigroup) poly  'a" where
"poly_coeff_sum p  sum_list (map (λ mc. max 0 (snd mc)) p)"

lemma monom_list_degree: "eval_monom_list (λ _. x) m = x ^ monom_list_degree m"
unfolding monom_list_degree_def
proof (induct m)
case Nil show ?case by simp
next
case (Cons mc m)
thus ?case by (cases mc, auto simp: power_add field_simps)
qed

lemma monom_list_var_monom[simp]: "monom_list (var_monom x) = [(x,1)]"
by (transfer, simp)

lemma monom_list_1[simp]:
by (transfer, simp)

lemma monom_degree: "eval_monom (λ _. x) m = x ^ monom_degree m"
by (transfer, rule monom_list_degree)

lemma poly_coeff_sum:
unfolding poly_coeff_sum_def
proof (induct p)
case Nil show ?case by (simp add: ge_refl)
next
case (Cons mc p)
have "(mcmc # p. max 0 (snd mc)) = max 0 (snd mc) + (mcp. max 0 (snd mc))" by auto
also have "  0 + 0"
by (rule ge_trans[OF plus_left_mono plus_right_mono[OF Cons]], auto)
finally show ?case by simp
qed

lemma poly_degree: assumes x: "x  (1 :: 'a :: poly_carrier)"
shows "poly_coeff_sum p * (x ^ poly_degree p)  eval_poly (λ _. x) p"
proof (induct p)
case Nil show ?case by (simp add: ge_refl poly_degree_def poly_coeff_sum_def)
next
case (Cons mc p)
obtain m c where mc: "mc = (m,c)" by force
from ge_trans[OF x one_ge_zero] have x0: "x  0" .
have id1: "eval_poly (λ_. x) (mc # p) = x ^ monom_degree m  * c + eval_poly (λ_. x) p" unfolding mc by (simp add: monom_degree)
have id2: "poly_coeff_sum (mc # p) * x ^ poly_degree (mc # p) =
x ^ max (monom_degree m) (poly_degree p) * (max 0 c) + poly_coeff_sum p * x ^ max (monom_degree m) (poly_degree p)"
unfolding poly_coeff_sum_def poly_degree_def by (simp add: mc field_simps)
show "poly_coeff_sum (mc # p) * x ^ poly_degree (mc # p)  eval_poly (λ_. x) (mc # p)"
unfolding id1 id2
proof (rule ge_trans[OF plus_left_mono plus_right_mono])
show "x ^ max (monom_degree m) (poly_degree p) * max 0 c  x ^ monom_degree m * c"
by (rule ge_trans[OF times_left_mono[OF _ pow_mono_exp] times_right_mono[OF pow_ge_zero]], insert x x0, auto)
show "poly_coeff_sum p * x ^ max (monom_degree m) (poly_degree p)  eval_poly (λ_. x) p"
by (rule ge_trans[OF times_right_mono[OF poly_coeff_sum pow_mono_exp[OF x]] Cons], auto)
qed
qed

lemma poly_degree_bound: assumes x: "x  (1 :: 'a :: poly_carrier)"
and c: "c  poly_coeff_sum p"
and d: "d  poly_degree p"
shows "c * (x ^ d)  eval_poly (λ _. x) p"
by (rule ge_trans[OF ge_trans[OF
times_left_mono[OF pow_ge_zero[OF ge_trans[OF x one_ge_zero]] c]
times_right_mono[OF poly_coeff_sum pow_mono_exp[OF x d]]] poly_degree[OF x]])

subsection ‹Executable and sufficient criteria to compare polynomials and ensure monotonicity›

text ‹poly\_split extracts the coefficient for a given monomial and returns additionally the remaining polynomial›
definition poly_split :: "('v monom)  ('v,'a :: zero)poly  'a × ('v,'a)poly"
where "poly_split m p  case List.extract (λ (n,_). m = n) p of None  (0,p) | Some (p1,(_,c),p2)  (c, p1 @ p2)"

lemma poly_split: assumes "poly_split m p = (c,q)"
shows "p =p (m,c) # q"
proof (cases "List.extract (λ (n,_). m = n) p")
case None
with assms have "(c,q) = (0,p)" unfolding poly_split_def by auto
thus ?thesis unfolding eq_poly_def by auto
next
case (Some res)
obtain p1 mc p2 where "res = (p1,mc,p2)" by (cases res, auto)
with extract_SomeE[OF Some[simplified this]] obtain a where p: "p = p1 @ (m,a) # p2" and res: "res = (p1,(m,a),p2)" by (cases mc, auto)
from Some res assms have c: "c = a" and q: "q = p1 @ p2" unfolding poly_split_def by auto
show ?thesis unfolding eq_poly_def by (simp add: p c q field_simps)
qed

lemma poly_split_eval: assumes "poly_split m p = (c,q)"
shows "eval_poly α p = (eval_monom α m * c) + eval_poly α q"
using poly_split[OF assms] unfolding eq_poly_def by auto

(* we assume that the polynomial invariant is present, otherwise this check might fail, e.g., on 0 =p 0 + 0 *)
fun check_poly_eq :: "('v,'a :: semiring_0)poly  ('v,'a)poly  bool" where
"check_poly_eq [] q = (q = [])"
| "check_poly_eq ((m,c) # p) q = (case List.extract (λ nd. fst nd = m) q of
None  False
| Some (q1,(_,d),q2)  c = d  check_poly_eq p (q1 @ q2))"

lemma check_poly_eq: fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
assumes chk: "check_poly_eq p q"
shows "p =p q" unfolding eq_poly_def
proof
fix α
from chk show "eval_poly α p = eval_poly α q"
proof (induct p arbitrary: q)
case Nil
thus ?case by auto
next
case (Cons mc p)
obtain m c where mc: "mc = (m,c)" by (cases mc, auto)
show ?case
proof (cases "List.extract (λ mc. fst mc = m) q")
case None
with Cons(2) show ?thesis unfolding mc by simp
next
case (Some res)
obtain q1 md q2 where "res = (q1,md,q2)" by (cases res, auto)
with extract_SomeE[OF Some[simplified this]] obtain d where q: "q = q1 @ (m,d) # q2" and res: "res = (q1,(m,d),q2)"
by (cases md, auto)