section ‹Polynomials›
theory Polynomials
imports
"Abstract-Rewriting.SN_Orders"
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]: "eval_monom_list α (m @ n) = eval_monom_list α m * eval_monom_list α n"
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$.
›
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: "monom_list_vars (monom_mult_list m1 m2) = monom_list_vars m1 ∪ monom_list_vars m2"
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"
by (simp add: id)
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'"
by (auto simp add: id)
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: "sum_var_list (monom_mult_list m n) x = sum_var_list m x + sum_var_list n x"
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]: "eval_monom_list α (monom_mult_list m n) = eval_monom_list α m * eval_monom_list α n"
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 _ Nil], 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]: "eval_monom α 1 = 1"
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 [] q = q"
| "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"
lemma poly_add_monoms: "poly_monoms (poly_add p1 p2) ⊆ poly_monoms p1 ∪ poly_monoms p2"
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
lemma poly_add_inv: "poly_inv p ⟹ poly_inv q ⟹ poly_inv (poly_add p q)"
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
declare poly_add.simps[simp del]
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
by (simp add: nd Cons True, simp add: field_simps l)
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
by (simp add: mc, rule poly_add_inv[OF monom_mult_poly_inv[OF q] Cons(1)[OF p]])
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: "poly_inv zero_poly" 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: "poly_inv one_poly" unfolding one_poly_def poly_inv_def monom_inv_def by auto
lemma poly_one[simp]: "eval_poly α one_poly = 1"
unfolding one_poly_def by simp
lemma poly_zero_add: "poly_add zero_poly p = p" unfolding zero_poly_def using poly_add.simps by auto
lemma poly_zero_mult: "poly_mult zero_poly p = zero_poly" 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: "poly_mult one_poly p =p p"
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_add_comm: "poly_add p q =p poly_add q p" unfolding eq_poly_def by (auto simp: field_simps)
lemma poly_add_assoc: "poly_add p1 (poly_add p2 p3) =p poly_add (poly_add p1 p2) p3" unfolding eq_poly_def by (auto simp: field_simps)
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,
simp add: poly_inv_def monom_inv_def,
simp add: poly_inv_def monom_inv_def,
simp add: zero_poly_inv,
simp add: poly_add_inv,
simp add: one_poly_inv,
simp add: poly_mult_inv)
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)"
by (induct n, simp add: one_poly_inv, simp add: poly_mult_inv[OF p])
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
by (simp add: mc Cons id, simp add: field_simps)
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 "monom_list_subst f m = monom_list_subst g m"
proof (induct m)
case (Cons wn m)
hence rec: "monom_list_subst f m = monom_list_subst g m" 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]: "monom_vars_list 1 = []"
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)
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]: "set (poly_vars_list p) = poly_vars p"
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 "eval_monom_list α m ≥ 0"
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
by (simp add: Pair)
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
lemma poly_add_ge_mono: assumes "p1 ≥p p2" shows "poly_add p1 q ≥p poly_add p2 q"
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: "SN poly_GT"
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 "eval_monom_list f m ≥ eval_monom_list g m" "eval_monom_list g m ≥ 0"
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: " eval_monom_list f m ≥ eval_monom_list g m" and IH2: "eval_monom_list g m ≥ 0" 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: "poly_weak_mono_all 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: "poly_weak_anti_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 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 "poly_weak_mono_all p"
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 "poly_vars_list p", 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: "poly_weak_mono_all 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: "poly_weak_mono_all p"
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
lemma poly_add_gt_mono: assumes "p1 >p p2" shows "poly_add p1 q >p poly_add p2 q"
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]: "monom_list 1 = []"
by (transfer, simp)
lemma monom_degree: "eval_monom (λ _. x) m = x ^ monom_degree m"
by (transfer, rule monom_list_degree)
lemma poly_coeff_sum: "poly_coeff_sum p ≥ 0"
unfolding poly_coeff_sum_def
proof (induct p)
case Nil show ?case by (simp add: ge_refl)
next
case (Cons mc p)
have "(∑mc←mc # p. max 0 (snd mc)) = max 0 (snd mc) + (∑mc←p. 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
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)
from Cons(2) Some mc res have rec: "check_poly_eq p (q1 @ q2)" and c: "c = d" by auto
from Cons(1)[OF rec] have p: "eval_poly α p = eval_poly α (q1 @ q2)" .
show ?thesis unfolding mc eval_poly.simps c p q by (simp add: ac_simps)
qed
qed
qed
declare check_poly_eq.simps[simp del]
fun check_poly_ge :: "('v,'a :: ordered_semiring_0)poly ⇒ ('v,'a)poly ⇒ bool" where
"check_poly_ge [] q = list_all (λ (_,d). 0 ≥ d) q"
| "check_poly_ge ((m,c) # p) q = (case List.extract (λ nd. fst nd = m) q of
None ⇒ c ≥ 0 ∧ check_poly_ge p q
| Some (q1,(_,d),q2) ⇒ c ≥ d ∧ check_poly_ge p (q1 @ q2))"
lemma check_poly_ge: fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
shows "check_poly_ge p q ⟹ p ≥p q"
proof (induct p arbitrary: q)
case Nil
hence "∀ (n,d) ∈ set q. 0 ≥ d" using list_all_iff[of _ q] by auto
hence "[] ≥p q"
proof (induct q)
case Nil thus ?case by (simp)
next
case (Cons nd q)
hence rec: "[] ≥p q" by simp
show ?case
proof (cases nd)
case (Pair n d)
with Cons have ge: "0 ≥ d" by auto
show ?thesis
proof (simp only: Pair, unfold poly_ge_def, intro allI impI)
fix α :: "('v,'a)assign"
assume pos: "pos_assign α"
have ge: "0 ≥ eval_monom α n * d"
using times_right_mono[OF pos_assign_monom[OF pos, of n] ge] by simp
from rec[unfolded poly_ge_def] pos have ge2: "0 ≥ eval_poly α q" by auto
show "eval_poly α [] ≥ eval_poly α ((n,d) # q)" using ge_trans[OF plus_left_mono[OF ge] plus_right_mono[OF ge2]]
by simp
qed
qed
qed
thus ?case by simp
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) have rec: "check_poly_ge p q" and c: "c ≥ 0" using mc by auto
from Cons(1)[OF rec] have rec: "p ≥p q" .
show ?thesis
proof (simp only: mc, unfold poly_ge_def, intro allI impI)
fix α :: "('v,'a)assign"
assume pos: "pos_assign α"
have ge: "eval_monom α m * c ≥ 0"
using times_right_mono[OF pos_assign_monom[OF pos, of m] c] by simp
from rec have pq: "eval_poly α p ≥ eval_poly α q" unfolding poly_ge_def using pos by auto
show "eval_poly α ((m,c) # p) ≥ eval_poly α q"
using ge_trans[OF plus_left_mono[OF ge] plus_right_mono[OF pq]] by simp
qed
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)
from Cons(2) Some mc res have rec: "check_poly_ge p (q1 @ q2)" and c: "c ≥ d" by auto
from Cons(1)[OF rec] have p: "p ≥p q1 @ q2" .
show ?thesis
proof (simp only: mc, unfold poly_ge_def, intro allI impI)
fix α :: "('v,'a)assign"
assume pos: "pos_assign α"
have ge: "eval_monom α m * c ≥ eval_monom α m * d"
using times_right_mono[OF pos_assign_monom[OF pos, of m] c]
by simp
from p have ge2: "eval_poly α p ≥ eval_poly α (q1 @ q2)" unfolding poly_ge_def using pos by auto
show "eval_poly α ((m,c) # p) ≥ eval_poly α q" using ge_trans[OF plus_left_mono[OF ge] plus_right_mono[OF ge2]]
by (simp add: q field_simps)
qed
qed
qed
declare check_poly_ge.simps[simp del]
definition check_poly_weak_mono_all :: "('v,'a :: ordered_semiring_0)poly ⇒ bool"
where "check_poly_weak_mono_all p ≡ list_all (λ (m,c). c ≥ 0) p"
lemma check_poly_weak_mono_all: fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
assumes "check_poly_weak_mono_all p" shows "poly_weak_mono_all p"
unfolding poly_weak_mono_all_def
proof (intro allI impI)
fix f g :: "('v,'a)assign"
assume fg: "∀ x. f x ≥ g x"
and pos: "pos_assign g"
hence fg: "⋀ x. f x ≥ g x" by auto
from pos[unfolded pos_assign_def] have g: "⋀ x. g x ≥ 0" ..
from assms have "⋀ m c. (m,c) ∈ set p ⟹ c ≥ 0" unfolding check_poly_weak_mono_all_def by (auto simp: list_all_iff)
thus "eval_poly f p ≥ eval_poly g p"
proof (induct p)
case Nil thus ?case by (simp add: ge_refl)
next
case (Cons mc p)
hence IH: "eval_poly f p ≥ eval_poly g p" by auto
show ?case
proof (cases mc)
case (Pair m c)
with Cons have c: "c ≥ 0" by auto
show ?thesis unfolding Pair eval_poly.simps fst_conv snd_conv
proof (rule ge_trans[OF plus_left_mono[OF times_left_mono[OF c]] plus_right_mono[OF IH]])
show "eval_monom f m ≥ eval_monom g m"
by (rule eval_monom_mono(1)[OF fg g])
qed
qed
qed
qed
lemma check_poly_weak_mono_all_pos:
assumes "check_poly_weak_mono_all p" shows "p ≥p zero_poly"
unfolding zero_poly_def
proof (rule check_poly_ge)
from assms have "⋀ m c. (m,c) ∈ set p ⟹ c ≥ 0" unfolding check_poly_weak_mono_all_def by (auto simp: list_all_iff)
thus "check_poly_ge p []"
by (induct p, simp add: check_poly_ge.simps, clarify, auto simp: check_poly_ge.simps extract_Nil_code)
qed
text ‹better check for weak monotonicity for discrete carriers:
$p$ is monotone in $v$ if $p(\ldots v+1 \ldots) \geq p(\ldots v \ldots)$›
definition check_poly_weak_mono_discrete :: "('v :: linorder,'a :: poly_carrier)poly ⇒ 'v ⇒ bool"
where "check_poly_weak_mono_discrete p v ≡ check_poly_ge (poly_subst (λ w. poly_of (if w = v then PSum [PNum 1, PVar v] else PVar w)) p) p"
definition check_poly_weak_mono_and_pos :: "bool ⇒ ('v :: linorder,'a :: poly_carrier)poly ⇒ bool"
where "check_poly_weak_mono_and_pos discrete p ≡
if discrete then list_all (λ v. check_poly_weak_mono_discrete p v) (poly_vars_list p) ∧ eval_poly (λ w. 0) p ≥ 0
else check_poly_weak_mono_all p"
definition check_poly_weak_anti_mono_discrete :: "('v :: linorder,'a :: poly_carrier)poly ⇒ 'v ⇒ bool"
where "check_poly_weak_anti_mono_discrete p v ≡ check_poly_ge p (poly_subst (λ w. poly_of (if w = v then PSum [PNum 1, PVar v] else PVar w)) p)"
context poly_order_carrier
begin
lemma check_poly_weak_mono_discrete:
fixes v :: "'v :: linorder" and p :: "('v,'a)poly"
assumes discrete and check: "check_poly_weak_mono_discrete p v"
shows "poly_weak_mono p v"
unfolding poly_weak_mono_def
proof (intro allI impI)
fix f g :: "('v,'a)assign"
assume fgw: "∀ w. (v ≠ w ⟶ f w = g w)"
and gass: "pos_assign g"
and v: "f v ≥ g v"
from fgw have w: "⋀ w. v ≠ w ⟹ f w = g w" by auto
from assms check_poly_ge have ge: "poly_ge (poly_subst (λ w. poly_of (if w = v then PSum [PNum 1, PVar v] else PVar w)) p) p" (is "poly_ge ?p1 p") unfolding check_poly_weak_mono_discrete_def by blast
from discrete[OF ‹discrete› v] obtain k' where id: "f v = (((+) 1)^^k') (g v)" by auto
show "eval_poly f p ≥ eval_poly g p"
proof (cases k')
case 0
{
fix x
have "f x = g x" using id 0 w by (cases "x = v", auto)
}
hence "f = g" ..
thus ?thesis using ge_refl by simp
next
case (Suc k)
with id have "f v = (((+) 1)^^(Suc k)) (g v)" by simp
with w gass show "eval_poly f p ≥ eval_poly g p"
proof (induct k arbitrary: f g rule: less_induct)
case (less k)
show ?case
proof (cases k)
case 0
with less have id0: "f v = 1 + g v" by simp
have id1: "eval_poly f p = eval_poly g ?p1"
proof (rule eval_poly_subst)
fix w
show "f w = eval_poly g (poly_of (if w = v then PSum [PNum 1, PVar v] else PVar w))"
proof (cases "w = v")
case True
show ?thesis by (simp add: True id0 zero_poly_def)
next
case False
with less have "f w = g w" by simp
thus ?thesis by (simp add: False)
qed
qed
have "eval_poly g ?p1 ≥ eval_poly g p" using ge less unfolding poly_ge_def by simp
with id1 show ?thesis by simp
next
case (Suc kk)
obtain g' where g': "g' = (λ w. if (w = v) then 1 + g w else g w)" by auto
have "(1 :: 'a) + g v ≥ 1 + 0"
by (rule plus_right_mono, simp add: less(3)[unfolded pos_assign_def])
also have "1 + (0 :: 'a) = 1" by simp
also have "… ≥ 0" by (rule one_ge_zero)
finally have g'pos: "pos_assign g'" using less(3) unfolding pos_assign_def
by (simp add: g')
{
fix w
assume "v ≠ w"
hence "f w = g' w"
unfolding g' by (simp add: less)
} note w = this
have eq: "f v = ((+) (1 :: 'a) ^^ Suc kk) ((g' v))"
by (simp add: less(4) g' Suc, rule arg_cong[where f = "(+) 1"], induct kk, auto)
from Suc have kk: "kk < k" by simp
from less(1)[OF kk w g'pos] eq
have rec1: "eval_poly f p ≥ eval_poly g' p" by simp
{
fix w
assume "v ≠ w"
hence "g' w = g w"
unfolding g' by simp
} note w = this
from Suc have z: "0 < k" by simp
from less(1)[OF z w less(3)] g'
have rec2: "eval_poly g' p ≥ eval_poly g p" by simp
show ?thesis by (rule ge_trans[OF rec1 rec2])
qed
qed
qed
qed
lemma check_poly_weak_anti_mono_discrete:
fixes v :: "'v :: linorder" and p :: "('v,'a)poly"
assumes discrete and check: "check_poly_weak_anti_mono_discrete p v"
shows "poly_weak_anti_mono p v"
unfolding poly_weak_anti_mono_def
proof (intro allI impI)
fix f g :: "('v,'a)assign"
assume fgw: "∀ w. (v ≠ w ⟶ f w = g w)"
and gass: "pos_assign g"
and v: "f v ≥ g v"
from fgw have w: "⋀ w. v ≠ w ⟹ f w = g w" by auto
from assms check_poly_ge have ge: "poly_ge p (poly_subst (λ w. poly_of (if w = v then PSum [PNum 1, PVar v] else PVar w)) p)" (is "poly_ge p ?p1") unfolding check_poly_weak_anti_mono_discrete_def by blast
from discrete[OF ‹discrete› v] obtain k' where id: "f v = (((+) 1)^^k') (g v)" by auto
show "eval_poly g p ≥ eval_poly f p"
proof (cases k')
case 0
{
fix x
have "f x = g x" using id 0 w by (cases "x = v", auto)
}
hence "f = g" ..
thus ?thesis using ge_refl by simp
next
case (Suc k)
with id have "f v = (((+) 1)^^(Suc k)) (g v)" by simp
with w gass show "eval_poly g p ≥ eval_poly f p"
proof (induct k arbitrary: f g rule: less_induct)
case (less k)
show ?case
proof (cases k)
case 0
with less have id0: "f v = 1 + g v" by simp
have id1: "eval_poly f p = eval_poly g ?p1"
proof (rule eval_poly_subst)
fix w
show "f w = eval_poly g (poly_of (if w = v then PSum [PNum 1, PVar v] else PVar w))"
proof (cases "w = v")
case True
show ?thesis by (simp add: True id0 zero_poly_def)
next
case False
with less have "f w = g w" by simp
thus ?thesis by (simp add: False)
qed
qed
have "eval_poly g p ≥ eval_poly g ?p1" using ge less unfolding poly_ge_def by simp
with id1 show ?thesis by simp
next
case (Suc kk)
obtain g' where g': "g' = (λ w. if (w = v) then 1 + g w else g w)" by auto
have "(1 :: 'a) + g v ≥ 1 + 0"
by (rule plus_right_mono, simp add: less(3)[unfolded pos_assign_def])
also have "(1 :: 'a) + 0 = 1" by simp
also have "… ≥ 0" by (rule one_ge_zero)
finally have g'pos: "pos_assign g'" using less(3) unfolding pos_assign_def
by (simp add: g')
{
fix w
assume "v ≠ w"
hence "f w = g' w"
unfolding g' by (simp add: less)
} note w = this
have eq: "f v = ((+) (1 :: 'a) ^^ Suc kk) ((g' v))"
by (simp add: less(4) g' Suc, rule arg_cong[where f = "(+) 1"], induct kk, auto)
from Suc have kk: "kk < k" by simp
from less(1)[OF kk w g'pos] eq
have rec1: "eval_poly g' p ≥ eval_poly f p" by simp
{
fix w
assume "v ≠ w"
hence "g' w = g w"
unfolding g' by simp
} note w = this
from Suc have z: "0 < k" by simp
from less(1)[OF z w less(3)] g'
have rec2: "eval_poly g p ≥ eval_poly g' p" by simp
show ?thesis by (rule ge_trans[OF rec2 rec1])
qed
qed
qed
qed
lemma check_poly_weak_mono_and_pos:
fixes p :: "('v :: linorder,'a)poly"
assumes "check_poly_weak_mono_and_pos discrete p"
shows "poly_weak_mono_all p ∧ (p ≥p zero_poly)"
proof (cases discrete)
case False
with assms have c: "check_poly_weak_mono_all p" unfolding check_poly_weak_mono_and_pos_def
by auto
from check_poly_weak_mono_all[OF c] check_poly_weak_mono_all_pos[OF c] show ?thesis by auto
next
case True
with assms have c: "list_all (λ v. check_poly_weak_mono_discrete p v) (poly_vars_list p)" and g: "eval_poly (λ w. 0) p ≥ 0"
unfolding check_poly_weak_mono_and_pos_def by auto
have m: "poly_weak_mono_all p"
proof (rule poly_weak_mono)
fix v :: 'v
assume v: "v ∈ poly_vars p"
show "poly_weak_mono p v"
by (rule check_poly_weak_mono_discrete[OF True], insert c[unfolded list_all_iff] v, auto)
qed
have m': "poly_weak_mono_all p"
proof (rule poly_weak_mono)
fix v :: 'v
assume v: "v ∈ poly_vars p"
show "poly_weak_mono p v"
by (rule check_poly_weak_mono_discrete[OF True], insert c[unfolded list_all_iff] v, auto)
qed
from poly_weak_mono_all_pos[OF g m'] m show ?thesis by auto
qed
end
definition check_poly_weak_mono :: "('v :: linorder,'a :: ordered_semiring_0)poly ⇒ 'v ⇒ bool"
where "check_poly_weak_mono p v ≡ list_all (λ (m,c). c ≥ 0 ∨ v ∉ monom_vars m) p"
lemma check_poly_weak_mono: fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
assumes "check_poly_weak_mono p v" shows "poly_weak_mono p v"
unfolding poly_weak_mono_def
proof (intro allI impI)
fix f g :: "('v,'a)assign"
assume "∀ x. v ≠ x ⟶ f x = g x"
and pos: "pos_assign g"
and ge: "f v ≥ g v"
hence fg: "⋀ x. v ≠ x ⟹ f x = g x" by auto
from pos[unfolded pos_assign_def] have g: "⋀ x. g x ≥ 0" ..
from assms have "⋀ m c. (m,c) ∈ set p ⟹ c ≥ 0 ∨ v ∉ monom_vars m" unfolding check_poly_weak_mono_def by (auto simp: list_all_iff)
thus "eval_poly f p ≥ eval_poly g p"
proof (induct p)
case (Cons mc p)
hence IH: "eval_poly f p ≥ eval_poly g p" by auto
obtain m c where mc: "mc = (m,c)" by force
with Cons have c: "c ≥ 0 ∨ v ∉ monom_vars m" by auto
show ?case unfolding mc eval_poly.simps fst_conv snd_conv
proof (rule ge_trans[OF plus_left_mono plus_right_mono[OF IH]])
from c show "eval_monom f m * c ≥ eval_monom g m * c"
proof
assume c: "c ≥ 0"
show ?thesis
proof (rule times_left_mono[OF c], rule eval_monom_mono(1)[OF _ g])
fix x
show "f x ≥ g x" using ge fg[of x] by (cases "x = v", auto simp: ge_refl)
qed
next
assume v: "v ∉ monom_vars m"
have "eval_monom f m = eval_monom g m"
by (rule monom_vars_eval_monom, insert fg v, fast)
thus ?thesis by (simp add: ge_refl)
qed
qed
qed (simp add: ge_refl)
qed
definition check_poly_weak_mono_smart :: "bool ⇒ ('v :: linorder,'a :: poly_carrier)poly ⇒ 'v ⇒ bool"
where "check_poly_weak_mono_smart discrete ≡ if discrete then check_poly_weak_mono_discrete else check_poly_weak_mono"
lemma (in poly_order_carrier) check_poly_weak_mono_smart: fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
shows "check_poly_weak_mono_smart discrete p v ⟹ poly_weak_mono p v"
unfolding check_poly_weak_mono_smart_def
using check_poly_weak_mono check_poly_weak_mono_discrete by (cases discrete, auto)
definition check_poly_weak_anti_mono :: "('v :: linorder,'a :: ordered_semiring_0)poly ⇒ 'v ⇒ bool"
where "check_poly_weak_anti_mono p v ≡ list_all (λ (m,c). 0 ≥ c ∨ v ∉ monom_vars m) p"
lemma check_poly_weak_anti_mono: fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
assumes "check_poly_weak_anti_mono p v" shows "poly_weak_anti_mono p v"
unfolding poly_weak_anti_mono_def
proof (intro allI impI)
fix f g :: "('v,'a)assign"
assume "∀ x. v ≠ x ⟶ f x = g x"
and pos: "pos_assign g"
and ge: "f v ≥ g v"
hence fg: "⋀ x. v ≠ x ⟹ f x = g x" by auto
from pos[unfolded pos_assign_def] have g: "⋀ x. g x ≥ 0" ..
from assms have "⋀ m c. (m,c) ∈ set p ⟹ 0 ≥ c ∨ v ∉ monom_vars m" unfolding check_poly_weak_anti_mono_def by (auto simp: list_all_iff)
thus "eval_poly g p ≥ eval_poly f p"
proof (induct p)
case Nil thus ?case by (simp add: ge_refl)
next
case (Cons mc p)
hence IH: "eval_poly g p ≥ eval_poly f p" by auto
obtain m c where mc: "mc = (m,c)" by force
with Cons have c: "0 ≥ c ∨ v ∉ monom_vars m" by auto
show ?case unfolding mc eval_poly.simps fst_conv snd_conv
proof (rule ge_trans[OF plus_left_mono plus_right_mono[OF IH]])
from c show "eval_monom g m * c ≥ eval_monom f m * c"
proof
assume c: "0 ≥ c"
show ?thesis
proof (rule times_left_anti_mono[OF eval_monom_mono(1)[OF _ g] c])
fix x
show "f x ≥ g x" using ge fg[of x] by (cases "x = v", auto simp: ge_refl)
qed
next
assume v: "v ∉ monom_vars m"
have "eval_monom f m = eval_monom g m"
by (rule monom_vars_eval_monom, insert fg v, fast)
thus ?thesis by (simp add: ge_refl)
qed
qed
qed
qed
definition check_poly_weak_anti_mono_smart :: "bool ⇒ ('v :: linorder,'a :: poly_carrier)poly ⇒ 'v ⇒ bool"
where "check_poly_weak_anti_mono_smart discrete ≡ if discrete then check_poly_weak_anti_mono_discrete else check_poly_weak_anti_mono"
lemma (in poly_order_carrier) check_poly_weak_anti_mono_smart: fixes p :: "('v :: linorder,'a :: poly_carrier)poly"
shows "check_poly_weak_anti_mono_smart discrete p v ⟹ poly_weak_anti_mono p v"
unfolding check_poly_weak_anti_mono_smart_def
using check_poly_weak_anti_mono[of p v] check_poly_weak_anti_mono_discrete[of p v]
by (cases discrete, auto)
definition check_poly_gt :: "('a ⇒ 'a ⇒ bool) ⇒ ('v :: linorder,'a :: ordered_semiring_0)poly ⇒ ('v,'a)poly ⇒ bool"
where "check_poly_gt gt p q ≡ let (a1,p1) = poly_split 1 p; (b1,q1) = poly_split 1 q in gt a1 b1 ∧ check_poly_ge p1 q1"
fun univariate_power_list :: "'v ⇒ 'v monom_list ⇒ nat option" where
"univariate_power_list x [(y,n)] = (if x = y then Some n else None)"
| "univariate_power_list _ _ = None"
lemma univariate_power_list: assumes "monom_inv m" "univariate_power_list x m = Some n"
shows "sum_var_list m = (λ y. if x = y then n else 0)"
"eval_monom_list α m = ((α x)^n)"
"n ≥ 1"
proof -
have m: "m = [(x,n)]" using assms
by (induct x m rule: univariate_power_list.induct, auto split: if_splits)
show "eval_monom_list α m = ((α x)^n)" "sum_var_list m = (λ y. if x = y then n else 0)"
"n ≥ 1" using assms(1)
unfolding m monom_inv_def by (auto simp: sum_var_list_def)
qed
lift_definition univariate_power :: "'v :: linorder ⇒ 'v monom ⇒ nat option"
is univariate_power_list .
lemma univariate_power: assumes "univariate_power x m = Some n"
shows "sum_var m = (λ y. if x = y then n else 0)"
"eval_monom α m = ((α x)^n)"
"n ≥ 1"
by (atomize(full), insert assms, transfer, auto dest: univariate_power_list)
lemma univariate_power_var_monom: "univariate_power y (var_monom x) = (if x = y then Some 1 else None)"
by (transfer, auto)
definition check_monom_strict_mono :: "bool ⇒ 'v :: linorder monom ⇒ 'v ⇒ bool" where
"check_monom_strict_mono pm m v ≡ case univariate_power v m of
Some p ⇒ pm ∨ p = 1
| None ⇒ False"
definition check_poly_strict_mono :: "bool ⇒ ('v :: linorder, 'a :: poly_carrier)poly ⇒ 'v ⇒ bool"
where "check_poly_strict_mono pm p v ≡ list_ex (λ (m,c). (c ≥ 1) ∧ check_monom_strict_mono pm m v) p"
definition check_poly_strict_mono_discrete :: "('a :: poly_carrier ⇒ 'a ⇒ bool) ⇒ ('v :: linorder,'a)poly ⇒ 'v ⇒ bool"
where "check_poly_strict_mono_discrete gt p v ≡ check_poly_gt gt (poly_subst (λ w. poly_of (if w = v then PSum [PNum 1, PVar v] else PVar w)) p) p "
definition check_poly_strict_mono_smart :: "bool ⇒ bool ⇒ ('a :: poly_carrier ⇒ 'a ⇒ bool) ⇒ ('v :: linorder,'a)poly ⇒ 'v ⇒ bool"
where "check_poly_strict_mono_smart discrete pm gt p v ≡
if discrete then check_poly_strict_mono_discrete gt p v else check_poly_strict_mono pm p v"
context poly_order_carrier
begin
lemma check_monom_strict_mono: fixes α β :: "('v :: linorder,'a)assign" and v :: 'v and m :: "'v monom"
assumes check: "check_monom_strict_mono power_mono m v"
and gt: "α v ≻ β v"
and ge: "β v ≥ 0"
shows "eval_monom α m ≻ eval_monom β m"
proof -
from check[unfolded check_monom_strict_mono_def] obtain n where
uni: "univariate_power v m = Some n" and 1: "¬ power_mono ⟹ n = 1"
by (auto split: option.splits)
from univariate_power[OF uni]
have n1: "n ≥ 1" and eval: "eval_monom a m = a v ^ n" for a :: "('v,'a)assign"
by auto
show ?thesis
proof (cases power_mono)
case False
with gt 1[OF this] show ?thesis unfolding eval by auto
next
case True
from power_mono[OF True gt ge n1] show ?thesis unfolding eval .
qed
qed
lemma check_poly_strict_mono:
assumes check1: "check_poly_strict_mono power_mono p v"
and check2: "check_poly_weak_mono_all p"
shows "poly_strict_mono p v"
unfolding poly_strict_mono_def
proof (intro allI impI)
fix f g :: "('b,'a)assign"
assume fgw: "∀ w. (v ≠ w ⟶ f w = g w)"
and pos: "pos_assign g"
and fgv: "f v ≻ g v"
from pos[unfolded pos_assign_def] have g: "⋀ x. g x ≥ 0" ..
{
fix w
have "f w ≥ g w"
proof (cases "v = w")
case False
with fgw ge_refl show ?thesis by auto
next
case True
from fgv[unfolded True] show ?thesis by (rule gt_imp_ge)
qed
} note fgw2 = this
let ?e = "eval_poly"
show "?e f p ≻ ?e g p"
using check1[unfolded check_poly_strict_mono_def, simplified list_ex_iff]
check2[unfolded check_poly_weak_mono_all_def, simplified list_all_iff, THEN bspec]
proof (induct p)
case Nil thus ?case by simp
next
case (Cons mc p)
obtain m c where mc: "mc = (m,c)" by (cases mc, auto)
show ?case
proof (cases "c ≥ 1 ∧ check_monom_strict_mono power_mono m v")
case True
hence c: "c ≥ 1" and m: "check_monom_strict_mono power_mono m v" by blast+
from times_gt_mono[OF check_monom_strict_mono[OF m, of f g, OF fgv g] c]
have gt: "eval_monom f m * c ≻ eval_monom g m * c" .
from Cons(3) have "check_poly_weak_mono_all p" unfolding check_poly_weak_mono_all_def list_all_iff by auto
from check_poly_weak_mono_all[OF this, unfolded poly_weak_mono_all_def, rule_format, OF fgw2 pos]
have ge: "?e f p ≥ ?e g p" .
from compat2[OF plus_gt_left_mono[OF gt] plus_right_mono[OF ge]]
show ?thesis unfolding mc by simp
next
case False
with Cons(2) mc have "∃ mc ∈ set p. (λ (m,c). c ≥ 1 ∧ check_monom_strict_mono power_mono m v) mc" by auto
from Cons(1)[OF this] Cons(3) have rec: "?e f p ≻ ?e g p" by simp
from Cons(3) mc have c: "c ≥ 0" by auto
from times_left_mono[OF c eval_monom_mono(1)[OF fgw2 g]]
have ge: "eval_monom f m * c ≥ eval_monom g m * c" .
from compat2[OF plus_gt_left_mono[OF rec] plus_right_mono[OF ge]]
show ?thesis by (simp add: mc field_simps)
qed
qed
qed
lemma check_poly_gt:
fixes p :: "('v :: linorder,'a)poly"
assumes "check_poly_gt gt p q" shows "p >p q"
proof -
obtain a1 p1 where p: "poly_split 1 p = (a1,p1)" by force
obtain b1 q1 where q: "poly_split 1 q = (b1,q1)" by force
from p q assms have gt: "a1 ≻ b1" and ge: "p1 ≥p q1" unfolding check_poly_gt_def using check_poly_ge[of p1 q1] by auto
show ?thesis
proof (unfold poly_gt_def, intro impI allI)
fix α :: "('v,'a)assign"
assume "pos_assign α"
with ge have ge: "eval_poly α p1 ≥ eval_poly α q1" unfolding poly_ge_def by simp
from plus_gt_left_mono[OF gt] compat[OF plus_left_mono[OF ge]] have gt: "a1 + eval_poly α p1 ≻ b1 + eval_poly α q1" by (force simp: field_simps)
show "eval_poly α p ≻ eval_poly α q"
by (simp add: poly_split[OF p, unfolded eq_poly_def] poly_split[OF q, unfolded eq_poly_def] gt)
qed
qed
lemma check_poly_strict_mono_discrete:
fixes v :: "'v :: linorder" and p :: "('v,'a)poly"
assumes discrete and check: "check_poly_strict_mono_discrete gt p v"
shows "poly_strict_mono p v"
unfolding poly_strict_mono_def
proof (intro allI impI)
fix f g :: "('v,'a)assign"
assume fgw: "∀ w. (v ≠ w ⟶ f w = g w)"
and gass: "pos_assign g"
and v: "f v ≻ g v"
from gass have g: "⋀ x. g x ≥ 0" unfolding pos_assign_def ..
from fgw have w: "⋀ w. v ≠ w ⟹ f w = g w" by auto
from assms check_poly_gt have gt: "poly_gt (poly_subst (λ w. poly_of (if w = v then PSum [PNum 1, PVar v] else PVar w)) p) p" (is "poly_gt ?p1 p") unfolding check_poly_strict_mono_discrete_def by blast
from discrete[OF ‹discrete› gt_imp_ge[OF v]] obtain k' where id: "f v = (((+) 1)^^k') (g v)" by auto
{
assume "k' = 0"
from v[unfolded id this] have "g v ≻ g v" by simp
hence False using SN g[of v] unfolding SN_defs by auto
}
with id obtain k where id: "f v = (((+) 1)^^(Suc k)) (g v)" by (cases k', auto)
with w gass
show "eval_poly f p ≻ eval_poly g p"
proof (induct k arbitrary: f g rule: less_induct)
case (less k)
show ?case
proof (cases k)
case 0
with less(4) have id0: "f v = 1 + g v" by simp
have id1: "eval_poly f p = eval_poly g ?p1"
proof (rule eval_poly_subst)
fix w
show "f w = eval_poly g (poly_of (if w = v then PSum [PNum 1, PVar v] else PVar w))"
proof (cases "w = v")
case True
show ?thesis by (simp add: True id0 zero_poly_def)
next
case False
with less have "f w = g w" by simp
thus ?thesis by (simp add: False)
qed
qed
have "eval_poly g ?p1 ≻ eval_poly g p" using gt less unfolding poly_gt_def by simp
with id1 show ?thesis by simp
next
case (Suc kk)
obtain g' where g': "g' = (λ w. if (w = v) then 1 + g w else g w)" by auto
have "(1 :: 'a) + g v ≥ 1 + 0"
by (rule plus_right_mono, simp add: less(3)[unfolded pos_assign_def])
also have "(1 :: 'a) + 0 = 1" by simp
also have "… ≥ 0" by (rule one_ge_zero)
finally have g'pos: "pos_assign g'" using less(3) unfolding pos_assign_def
by (simp add: g')
{
fix w
assume "v ≠ w"
hence "f w = g' w"
unfolding g' by (simp add: less)
} note w = this
have eq: "f v = ((+) (1 :: 'a) ^^ Suc kk) ((g' v))"
by (simp add: less(4) g' Suc, rule arg_cong[where f = "(+) 1"], induct kk, auto)
from Suc have kk: "kk < k" by simp
from less(1)[OF kk w g'pos] eq
have rec1: "eval_poly f p ≻ eval_poly g' p" by simp
{
fix w
assume "v ≠ w"
hence "g' w = g w"
unfolding g' by simp
} note w = this
from Suc have z: "0 < k" by simp
from less(1)[OF z w less(3)] g'
have rec2: "eval_poly g' p ≻ eval_poly g p" by simp
show ?thesis by (rule gt_trans[OF rec1 rec2])
qed
qed
qed
lemma check_poly_strict_mono_smart:
assumes check1: "check_poly_strict_mono_smart discrete power_mono gt p v"
and check2: "check_poly_weak_mono_and_pos discrete p"
shows "poly_strict_mono p v"
proof (cases discrete)
case True
with check1[unfolded check_poly_strict_mono_smart_def]
check_poly_strict_mono_discrete[OF True]
show ?thesis by auto
next
case False
from check_poly_strict_mono[OF check1[unfolded check_poly_strict_mono_smart_def, simplified False, simplified]]
check2[unfolded check_poly_weak_mono_and_pos_def, simplified False, simplified]
show ?thesis by auto
qed
end
end