# Theory Polynomials.MPoly_Type_Class

(* Author: Fabian Immler, Alexander Maletzky *)

section Type-Class-Multivariate Polynomials

theory MPoly_Type_Class
imports
Utils
Power_Products
More_Modules
begin

text This theory views @{typ "'a 0 'b"} as multivariate polynomials, where type class constraints
on @{typ 'a} ensure that @{typ 'a} represents something like monomials.

lemma when_distrib: "f (a when b) = (f a when b)" if "¬ b  f 0 = 0"
using that by (auto simp: when_def)

definition mapp_2 :: "('a  'b  'c  'd)  ('a 0 'b::zero)  ('a 0 'c::zero)  ('a 0 'd::zero)"
where "mapp_2 f p q = Abs_poly_mapping (λk. f k (lookup p k) (lookup q k) when k  keys p  keys q)"

lemma lookup_mapp_2:
"lookup (mapp_2 f p q) k = (f k (lookup p k) (lookup q k) when k  keys p  keys q)"
proof -
have "lookup (Abs_poly_mapping (λk. f k (lookup p k) (lookup q k) when k  keys p  keys q)) =
(λk. f k (lookup p k) (lookup q k) when k  keys p  keys q)"
by (rule Abs_poly_mapping_inverse, simp)
thus ?thesis by (simp add: mapp_2_def)
qed

lemma lookup_mapp_2_homogenous:
assumes "f k 0 0 = 0"
shows "lookup (mapp_2 f p q) k = f k (lookup p k) (lookup q k)"
by (simp add: lookup_mapp_2 when_def in_keys_iff assms)

lemma mapp_2_cong [fundef_cong]:
assumes "p = p'" and "q = q'"
assumes "k. k  keys p'  keys q'  f k (lookup p' k) (lookup q' k) = f' k (lookup p' k) (lookup q' k)"
shows "mapp_2 f p q = mapp_2 f' p' q'"
by (rule poly_mapping_eqI, simp add: assms(1, 2) lookup_mapp_2, rule when_cong, fact refl, rule assms(3), blast)

lemma keys_mapp_subset: "keys (mapp_2 f p q)  keys p  keys q"
proof
fix t
assume "t  keys (mapp_2 f p q)"
hence "lookup (mapp_2 f p q) t  0" by (simp add: in_keys_iff)
thus "t  keys p  keys q" by (simp add: lookup_mapp_2 when_def split: if_split_asm)
qed

lemma mapp_2_mapp: "mapp_2 (λt a. f t) 0 p = Poly_Mapping.mapp f p"
by (rule poly_mapping_eqI, simp add: lookup_mapp lookup_mapp_2)

subsection @{const keys}

lemma in_keys_plusI1:
assumes "t  keys p" and "t  keys q"
shows "t  keys (p + q)"
using assms unfolding in_keys_iff lookup_add by simp

lemma in_keys_plusI2:
assumes "t  keys q" and "t  keys p"
shows "t  keys (p + q)"
using assms unfolding in_keys_iff lookup_add by simp

lemma keys_plus_eqI:
assumes "keys p  keys q = {}"
shows "keys (p + q) = (keys p  keys q)"
proof
show "keys (p + q)  keys p  keys q"
show "keys p  keys q  keys (p + q)"
qed

lemma keys_uminus: "keys (- p) = keys p"
by (transfer, auto)

lemma keys_minus: "keys (p - q)  (keys p  keys q)"
by (transfer, auto)

subsection Monomials

abbreviation "monomial  (λc t. Poly_Mapping.single t c)"

lemma keys_of_monomial:
assumes "c  0"
shows "keys (monomial c t) = {t}"
using assms by simp

lemma monomial_uminus:
shows "- monomial c s = monomial (- c) s"
by (transfer, rule ext, simp add: Poly_Mapping.when_def)

lemma monomial_inj:
assumes "monomial c s = monomial (d::'b::zero_neq_one) t"
shows "(c = 0  d = 0)  (c = d  s = t)"
using assms unfolding poly_mapping_eq_iff
by (metis (mono_tags, opaque_lifting) lookup_single_eq lookup_single_not_eq)

definition is_monomial :: "('a 0 'b::zero)  bool"
where "is_monomial p  card (keys p) = 1"

lemma monomial_is_monomial:
assumes "c  0"
shows "is_monomial (monomial c t)"
using keys_single[of t c] assms by (simp add: is_monomial_def)

lemma is_monomial_monomial:
assumes "is_monomial p"
obtains c t where "c  0" and "p = monomial c t"
proof -
from assms have "card (keys p) = 1" unfolding is_monomial_def .
then obtain t where sp: "keys p = {t}" by (rule card_1_singletonE)
let ?c = "lookup p t"
from sp have "?c  0" by fastforce
show ?thesis
proof
show "p = monomial ?c t"
proof (intro poly_mapping_keys_eqI)
from sp show "keys p = keys (monomial ?c t)" using ?c  0 by simp
next
fix s
assume "s  keys p"
with sp have "s = t" by simp
show "lookup p s = lookup (monomial ?c t) s" by (simp add: s = t)
qed
qed fact
qed

lemma is_monomial_uminus: "is_monomial (-p)  is_monomial p"
unfolding is_monomial_def keys_uminus ..

lemma monomial_not_0:
assumes "is_monomial p"
shows "p  0"
using assms unfolding is_monomial_def by auto

lemma keys_subset_singleton_imp_monomial:
assumes "keys p  {t}"
shows "monomial (lookup p t) t = p"
proof (rule poly_mapping_eqI, simp add: lookup_single when_def, rule)
fix s
assume "t  s"
hence "s  keys p" using assms by blast
thus "lookup p s = 0" by (simp add: in_keys_iff)
qed

lemma monomial_0I:
assumes "c = 0"
shows "monomial c t = 0"
using assms by transfer (auto)

lemma monomial_0D:
assumes "monomial c t = 0"
shows "c = 0"
using assms by transfer (auto simp: fun_eq_iff when_def; meson)

corollary monomial_0_iff: "monomial c t = 0  c = 0"
by (rule, erule monomial_0D, erule monomial_0I)

lemma lookup_times_monomial_left: "lookup (monomial c t * p) s = (c * lookup p (s - t) when t adds s)"
for c::"'b::semiring_0" and t::"'a::comm_powerprod"
proof (induct p rule: poly_mapping_except_induct, simp)
fix p::"'a 0 'b" and w
assume "p  0" and "w  keys p"
and IH: "lookup (monomial c t * except p {w}) s =
(c * lookup (except p {w}) (s - t) when t adds s)" (is "_ = ?x")
have "monomial c t * p = monomial c t * (monomial (lookup p w) w + except p {w})"
by (simp only: plus_except[symmetric])
also have "... = monomial c t * monomial (lookup p w) w + monomial c t * except p {w}"
also have "... = monomial (c * lookup p w) (t + w) + monomial c t * except p {w}"
by (simp only: mult_single)
finally have "lookup (monomial c t * p) s = lookup (monomial (c * lookup p w) (t + w)) s + ?x"
also have "... = (lookup (monomial (c * lookup p w) (t + w)) s +
c * lookup (except p {w}) (s - t) when t adds s)"
by (rule when_distrib, auto simp add: lookup_single when_def)
also from refl have "... = (c * lookup p (s - t) when t adds s)"
proof (rule when_cong)
then obtain u where u: "s = t + u" ..
show "lookup (monomial (c * lookup p w) (t + w)) s + c * lookup (except p {w}) (s - t) =
c * lookup p (s - t)"
qed
finally show "lookup (monomial c t * p) s = (c * lookup p (s - t) when t adds s)" .
qed

lemma lookup_times_monomial_right: "lookup (p * monomial c t) s = (lookup p (s - t) * c when t adds s)"
for c::"'b::semiring_0" and t::"'a::comm_powerprod"
proof (induct p rule: poly_mapping_except_induct, simp)
fix p::"'a 0 'b" and w
assume "p  0" and "w  keys p"
and IH: "lookup (except p {w} * monomial c t) s =
((lookup (except p {w}) (s - t)) * c when t adds s)"
(is "_ = ?x")
have "p * monomial c t = (monomial (lookup p w) w + except p {w}) * monomial c t"
by (simp only: plus_except[symmetric])
also have "... = monomial (lookup p w) w * monomial c t + except p {w} * monomial c t"
also have "... = monomial (lookup p w * c) (w + t) + except p {w} * monomial c t"
by (simp only: mult_single)
finally have "lookup (p * monomial c t) s = lookup (monomial (lookup p w * c) (w + t)) s + ?x"
also have "... = (lookup (monomial (lookup p w * c) (w + t)) s +
lookup (except p {w}) (s - t) * c when t adds s)"
by (rule when_distrib, auto simp add: lookup_single when_def)
also from refl have "... = (lookup p (s - t) * c when t adds s)"
proof (rule when_cong)
then obtain u where u: "s = t + u" ..
show "lookup (monomial (lookup p w * c) (w + t)) s + lookup (except p {w}) (s - t) * c =
lookup p (s - t) * c"
qed
finally show "lookup (p * monomial c t) s = (lookup p (s - t) * c when t adds s)" .
qed

subsection Vector-Polynomials

text From now on we consider multivariate vector-polynomials, i.\,e. vectors of scalar polynomials.
We do this by adding a @{emph component} to each power-product, yielding
@{emph terms}. Vector-polynomials are then again just linear combinations of terms.
Note that a term is @{emph not} the same as a vector of power-products!

text We use define terms in a locale, such that later on we can interpret the
locale also by ordinary power-products (without components), exploiting the canonical isomorphism
between @{typ 'a} and @{typ 'a × unit}.

named_theorems term_simps "simplification rules for terms"

locale term_powerprod =
fixes pair_of_term::"'t  ('a::comm_powerprod × 'k::linorder)"
fixes term_of_pair::"('a × 'k)  't"
assumes term_pair [term_simps]: "term_of_pair (pair_of_term v) = v"
assumes pair_term [term_simps]: "pair_of_term (term_of_pair p) = p"
begin

lemma pair_of_term_injective:
assumes "pair_of_term u = pair_of_term v"
shows "u = v"
proof -
from assms have "term_of_pair (pair_of_term u) = term_of_pair (pair_of_term v)" by (simp only:)
thus ?thesis by (simp add: term_simps)
qed

corollary pair_of_term_inj: "inj pair_of_term"
using pair_of_term_injective by (rule injI)

lemma term_of_pair_injective:
assumes "term_of_pair p = term_of_pair q"
shows "p = q"
proof -
from assms have "pair_of_term (term_of_pair p) = pair_of_term (term_of_pair q)" by (simp only:)
thus ?thesis by (simp add: term_simps)
qed

corollary term_of_pair_inj: "inj term_of_pair"
using term_of_pair_injective by (rule injI)

definition pp_of_term :: "'t  'a"
where "pp_of_term v = fst (pair_of_term v)"

definition component_of_term :: "'t  'k"
where "component_of_term v = snd (pair_of_term v)"

lemma term_of_pair_pair [term_simps]: "term_of_pair (pp_of_term v, component_of_term v) = v"
by (simp add: pp_of_term_def component_of_term_def term_pair)

lemma pp_of_term_of_pair [term_simps]: "pp_of_term (term_of_pair (t, k)) = t"

lemma component_of_term_of_pair [term_simps]: "component_of_term (term_of_pair (t, k)) = k"

definition splus :: "'a  't  't" (infixl "" 75)
where "splus t v = term_of_pair (t + pp_of_term v, component_of_term v)"

definition sminus :: "'t  'a  't" (infixl "" 75)
where "sminus v t = term_of_pair (pp_of_term v - t, component_of_term v)"

text Note that the argument order in @{const sminus} is reversed compared to the order in @{const splus}.

where "adds_term u v  component_of_term u = component_of_term v  pp_of_term u adds pp_of_term v"

lemma pp_of_term_splus [term_simps]: "pp_of_term (t  v) = t + pp_of_term v"

lemma component_of_term_splus [term_simps]:

lemma pp_of_term_sminus [term_simps]: "pp_of_term (v  t) = pp_of_term v - t"

lemma component_of_term_sminus [term_simps]:

lemma splus_sminus [term_simps]: "(t  v)  t = v"

lemma splus_zero [term_simps]: "0  v = v"

lemma sminus_zero [term_simps]: "v  0 = v"

lemma splus_assoc [ac_simps]: "(s + t)  v = s  (t  v)"
by (simp add: splus_def ac_simps term_simps)

lemma splus_left_commute [ac_simps]: "s  (t  v) = t  (s  v)"
by (simp add: splus_def ac_simps term_simps)

lemma splus_right_canc [term_simps]: "t  v = s  v  t = s"

lemma splus_left_canc [term_simps]: "t  v = t  u  v = u"
by (metis splus_sminus)

assumes "v = t  u"

obtains u where "v = t  u"
proof -
from assms obtain s where *: "pp_of_term v = t + s" unfolding adds_pp_def ..
have "v = t  (term_of_pair (s, component_of_term v))"
thus ?thesis ..
qed

proof -
note assms(1)
also from assms(2) have "t adds pp_of_term v" by (simp only: adds_pp_def)
finally show ?thesis by (simp only: adds_pp_def)
qed

shows "s + u addsp t  v"

assumes "s + t addsp v"

assumes "s + t addsp v"

shows "t  (v  t) = v"
proof -
from assms adds_pp_alt[of t v] obtain u where u: "v = t  u" by (auto simp: ac_simps)
hence "v  t = u" by (simp add: term_simps)
thus ?thesis using u by simp
qed

assumes "(s + t) addsp v"

shows "(s + t) addsp v"

shows "(t + s) addsp v"

lemma minus_splus:
shows "(t - s)  v = (t  v)  s"
by (simp add: assms minus_plus sminus_def splus_def term_simps)

lemma minus_splus_sminus:
shows "(t - s)  (v  u) = (t  v)  (s + u)"
using assms minus_plus_minus term_powerprod.adds_pp_def term_powerprod_axioms sminus_def
splus_def term_simps by fastforce

lemma minus_splus_sminus_cancel:
shows "(t - s)  (v  t) = v  s"

lemma sminus_plus:
shows "v  (s + t) = (v  s)  t"

assumes "v = t  u"

obtains t where "v = t  u"
proof -
from assms have eq:  and
from this(2) obtain s where *:  unfolding adds_term_def
have "v = s  u" by (simp add: splus_def eq * term_simps)
thus ?thesis ..
qed

shows "s  u addst t  v"

shows "(t - pp_of_term u)  u = term_of_pair (t, component_of_term u)"

subsubsection Projections and Conversions

lift_definition proj_poly :: "'k  ('t 0 'b)  ('a 0 'b::zero)"
is "λk p t. p (term_of_pair (t, k))"
proof -
fix k::'k and p::"'t  'b"
assume fin: "finite {v. p v  0}"
have "{t. p (term_of_pair (t, k))  0}  pp_of_term ` {v. p v  0}"
proof (rule, simp)
fix t
assume "p (term_of_pair (t, k))  0"
hence *: "term_of_pair (t, k)  {v. p v  0}" by simp
have "t = pp_of_term (term_of_pair (t, k))" by (simp add: pp_of_term_def pair_term)
from this * show "t  pp_of_term ` {v. p v  0}" ..
qed
moreover from fin have "finite (pp_of_term ` {v. p v  0})" by (rule finite_imageI)
ultimately show "finite {t. p (term_of_pair (t, k))  0}" by (rule finite_subset)
qed

definition vectorize_poly :: "('t 0 'b)  ('k 0 ('a 0 'b::zero))"
where "vectorize_poly p = Abs_poly_mapping (λk. proj_poly k p)"

definition atomize_poly :: "('k 0 ('a 0 'b))  ('t 0 'b::zero)"
where "atomize_poly p = Abs_poly_mapping (λv. lookup (lookup p (component_of_term v)) (pp_of_term v))"

lemma lookup_proj_poly: "lookup (proj_poly k p) t = lookup p (term_of_pair (t, k))"
by (transfer, simp)

lemma lookup_vectorize_poly: "lookup (vectorize_poly p) k = proj_poly k p"
proof -
have "lookup (Abs_poly_mapping (λk. proj_poly k p)) = (λk. proj_poly k p)"
proof (rule Abs_poly_mapping_inverse, simp)
have "{k. proj_poly k p  0}  component_of_term ` keys p"
proof (rule, simp)
fix k
assume "proj_poly k p  0"
hence "keys (proj_poly k p)  {}" using poly_mapping_eq_zeroI by blast
then obtain t where "lookup (proj_poly k p) t  0" by blast
hence "term_of_pair (t, k)  keys p" by (simp add: lookup_proj_poly in_keys_iff)
hence "component_of_term (term_of_pair (t, k))  component_of_term ` keys p" by fastforce
qed
moreover from finite_keys have  by (rule finite_imageI)
ultimately show "finite {k. proj_poly k p  0}" by (rule finite_subset)
qed
thus ?thesis by (simp add: vectorize_poly_def)
qed

lemma lookup_atomize_poly:
"lookup (atomize_poly p) v = lookup (lookup p (component_of_term v)) (pp_of_term v)"
proof -
have "lookup (Abs_poly_mapping (λv. lookup (lookup p (component_of_term v)) (pp_of_term v))) =
(λv. lookup (lookup p (component_of_term v)) (pp_of_term v))"
proof (rule Abs_poly_mapping_inverse, simp)
have "{v. pp_of_term v  keys (lookup p (component_of_term v))}
(kkeys p. (λt. term_of_pair (t, k)) ` keys (lookup p k))" (is "_  ?A")
proof (rule, simp)
fix v
assume *:
hence "keys (lookup p (component_of_term v))  {}" by blast
hence  by auto
hence  (is "?k  _")
thus "kkeys p. v  (λt. term_of_pair (t, k)) ` keys (lookup p k)"
proof
have "v = term_of_pair (pp_of_term v, component_of_term v)" by (simp add: term_simps)
from this * show "v  (λt. term_of_pair (t, ?k)) ` keys (lookup p ?k)" ..
qed
qed
moreover have "finite ?A" by (rule, fact finite_keys, rule finite_imageI, rule finite_keys)
ultimately show "finite {x. lookup (lookup p (component_of_term x)) (pp_of_term x)  0}"
qed
thus ?thesis by (simp add: atomize_poly_def)
qed

lemma keys_proj_poly: "keys (proj_poly k p) = pp_of_term ` {xkeys p. component_of_term x = k}"
proof
show "keys (proj_poly k p)  pp_of_term ` {xkeys p. component_of_term x = k}"
proof
fix t
assume "t  keys (proj_poly k p)"
hence "lookup (proj_poly k p) t  0" by (simp add: in_keys_iff)
hence "term_of_pair (t, k)  keys p" by (simp add: in_keys_iff lookup_proj_poly)
hence "term_of_pair (t, k)  {xkeys p. component_of_term x = k}" by (simp add: term_simps)
hence "pp_of_term (term_of_pair (t, k))  pp_of_term ` {xkeys p. component_of_term x = k}" by (rule imageI)
thus "t  pp_of_term ` {xkeys p. component_of_term x = k}" by (simp only: pp_of_term_of_pair)
qed
next
show "pp_of_term ` {xkeys p. component_of_term x = k}  keys (proj_poly k p)"
proof
fix t
assume "t  pp_of_term ` {xkeys p. component_of_term x = k}"
then obtain x where "x  {xkeys p. component_of_term x = k}" and "t = pp_of_term x" ..
from this(1) have "x  keys p" and  by simp_all
from this(2) have "x = term_of_pair (t, k)" by (simp add: term_of_pair_pair t = pp_of_term x)
with x  keys p have "lookup p (term_of_pair (t, k))  0" by (simp add: in_keys_iff)
hence "lookup (proj_poly k p) t  0" by (simp add: lookup_proj_poly)
thus "t  keys (proj_poly k p)" by (simp add: in_keys_iff)
qed
qed

lemma keys_vectorize_poly:
proof
show
proof
fix k
assume "k  keys (vectorize_poly p)"
hence "lookup (vectorize_poly p) k  0" by (simp add: in_keys_iff)
hence "proj_poly k p  0" by (simp add: lookup_vectorize_poly)
then obtain t where "lookup (proj_poly k p) t  0" using aux by blast
hence "term_of_pair (t, k)  keys p" by (simp add: lookup_proj_poly in_keys_iff)
hence "component_of_term (term_of_pair (t, k))  component_of_term ` keys p" by (rule imageI)
thus  by (simp only: component_of_term_of_pair)
qed
next
show
proof
fix k
assume
then obtain x where "x  keys p" and  ..
from this(2) have "term_of_pair (pp_of_term x, k) = x" by (simp add: term_of_pair_pair)
with x  keys p have "lookup p (term_of_pair (pp_of_term x, k))  0" by (simp add: in_keys_iff)
hence "lookup (proj_poly k p) (pp_of_term x)  0" by (simp add: lookup_proj_poly)
hence "proj_poly k p  0" by auto
hence "lookup (vectorize_poly p) k  0" by (simp add: lookup_vectorize_poly)
thus "k  keys (vectorize_poly p)" by (simp add: in_keys_iff)
qed
qed

lemma keys_atomize_poly:
"keys (atomize_poly p) = (kkeys p. (λt. term_of_pair (t, k)) ` keys (lookup p k))" (is "?l = ?r")
proof
show "?l  ?r"
proof
fix v
assume "v  ?l"
hence "lookup (atomize_poly p) v  0" by (simp add: in_keys_iff)
hence *:  by (simp add: in_keys_iff lookup_atomize_poly)
hence  by fastforce
thus "v  ?r"
proof
from * have "term_of_pair (pp_of_term v, component_of_term v)
(λt. term_of_pair (t, component_of_term v)) ` keys (lookup p (component_of_term v))"
by (rule imageI)
thus "v  (λt. term_of_pair (t, component_of_term v)) ` keys (lookup p (component_of_term v))"
by (simp only: term_of_pair_pair)
qed
qed
next
show "?r  ?l"
proof
fix v
assume "v  ?r"
then obtain k where "k  keys p" and "v  (λt. term_of_pair (t, k)) ` keys (lookup p k)" ..
from this(2) obtain t where "t  keys (lookup p k)" and v: "v = term_of_pair (t, k)" ..
from this(1) have "lookup (atomize_poly p) v  0" by (simp add: v lookup_atomize_poly in_keys_iff term_simps)
thus "v  ?l" by (simp add: in_keys_iff)
qed
qed

lemma proj_atomize_poly [term_simps]: "proj_poly k (atomize_poly p) = lookup p k"
by (rule poly_mapping_eqI, simp add: lookup_proj_poly lookup_atomize_poly term_simps)

lemma vectorize_atomize_poly [term_simps]:
by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly term_simps)

lemma atomize_vectorize_poly [term_simps]:
by (rule poly_mapping_eqI, simp add: lookup_atomize_poly lookup_vectorize_poly lookup_proj_poly term_simps)

lemma proj_zero [term_simps]: "proj_poly k 0 = 0"
by (rule poly_mapping_eqI, simp add: lookup_proj_poly)

lemma proj_plus: "proj_poly k (p + q) = proj_poly k p + proj_poly k q"

lemma proj_uminus [term_simps]: "proj_poly k (- p) = - proj_poly k p"
by (rule poly_mapping_eqI, simp add: lookup_proj_poly)

lemma proj_minus: "proj_poly k (p - q) = proj_poly k p - proj_poly k q"
by (rule poly_mapping_eqI, simp add: lookup_proj_poly lookup_minus)

lemma vectorize_zero [term_simps]:
by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly term_simps)

lemma vectorize_plus:

lemma vectorize_uminus [term_simps]:
by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly term_simps)

lemma vectorize_minus:
by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly lookup_minus proj_minus)

lemma atomize_zero [term_simps]:
by (rule poly_mapping_eqI, simp add: lookup_atomize_poly)

lemma atomize_plus:

lemma atomize_uminus [term_simps]:
by (rule poly_mapping_eqI, simp add: lookup_atomize_poly)

lemma atomize_minus:
by (rule poly_mapping_eqI, simp add: lookup_atomize_poly lookup_minus)

lemma proj_monomial:
"proj_poly k (monomial c v) = (monomial c (pp_of_term v) when component_of_term v = k)"
proof (rule poly_mapping_eqI, simp add: lookup_proj_poly lookup_single when_def term_simps, intro impI)
fix t
assume 1: "pp_of_term v = t" and 2:
assume "v  term_of_pair (t, k)"
moreover have "v = term_of_pair (t, k)" by (simp add: 1[symmetric] 2[symmetric] term_simps)
ultimately show "c = 0" ..
qed

lemma vectorize_monomial:

by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly proj_monomial lookup_single)

lemma atomize_monomial_monomial:
"atomize_poly (monomial (monomial c t) k) = monomial c (term_of_pair (t, k))"
proof -
define v where "v = term_of_pair (t, k)"
have t: "t = pp_of_term v" and k:  by (simp_all add: v_def term_simps)
show ?thesis by (simp add: t k vectorize_monomial[symmetric] term_simps)
qed

lemma poly_mapping_eqI_proj:
assumes "k. proj_poly k p = proj_poly k q"
shows "p = q"
proof (rule poly_mapping_eqI)
fix v::'t
have  by (rule assms)
hence  by simp
thus "lookup p v = lookup q v" by (simp add: lookup_proj_poly term_simps)
qed

subsection Scalar Multiplication by Monomials

definition monom_mult :: "'b::semiring_0  'a::comm_powerprod  ('t 0 'b)  ('t 0 'b)"
where "monom_mult c t p = Abs_poly_mapping (λv. if t addsp v then c * (lookup p (v  t)) else 0)"

lemma keys_monom_mult_aux:
"{v. (if t addsp v then c * lookup p (v  t) else 0)  0}  (⊕) t ` keys p" (is "?l  ?r")
for c::"'b::semiring_0"
proof
fix v::'t
assume "v  ?l"
hence "(if t addsp v then c * lookup p (v  t) else 0)  0" by simp
hence "t addsp v" and cp_not_zero: "c * lookup p (v  t)  0" by (simp_all split: if_split_asm)
show "v  ?r"
proof
from adds_pp_sminus[OF t addsp v] show "v = t  (v  t)" by simp
next
from mult_not_zero[OF cp_not_zero] show "v  t  keys p"
qed
qed

lemma lookup_monom_mult:
"lookup (monom_mult c t p) v = (if t addsp v then c * lookup p (v  t) else 0)"
proof -
have "lookup (monom_mult c t p) = (λv. if t addsp v then c * lookup p (v  t) else 0)"
unfolding monom_mult_def
proof (rule Abs_poly_mapping_inverse)
from finite_keys have "finite ((⊕) t ` keys p)" ..
with keys_monom_mult_aux have "finite {v. (if t addsp v then c * lookup p (v  t) else 0)  0}"
by (rule finite_subset)
thus "(λv. if t addsp v then c * lookup p (v  t) else 0)  {f. finite {x. f x  0}}" by simp
qed
thus ?thesis by simp
qed

lemma lookup_monom_mult_plus:
"lookup (monom_mult c t p) (t  v) = (c::'b::semiring_0) * lookup p v"

lemma monom_mult_assoc: "monom_mult c s (monom_mult d t p) = monom_mult (c * d) (s + t) p"
proof (rule poly_mapping_eqI, simp add: lookup_monom_mult sminus_plus ac_simps, intro conjI impI)
fix v
moreover assume "¬ s + t addsp v"
ultimately show "c * (d * lookup p (v  s  t)) = 0" by simp
next
fix v
assume "s + t addsp v"
moreover assume "¬ s addsp v"
ultimately show "c * (d * lookup p (v  (s + t))) = 0" by simp
next
fix v
assume "s + t addsp v"
moreover assume "¬ t addsp v  s"
ultimately show "c * (d * lookup p (v  (s + t))) = 0" by simp
qed

lemma monom_mult_uminus_left: "monom_mult (- c) t p = - monom_mult (c::'b::ring) t p"
by (rule poly_mapping_eqI, simp add: lookup_monom_mult)

lemma monom_mult_uminus_right: "monom_mult c t (- p) = - monom_mult (c::'b::ring) t p"
by (rule poly_mapping_eqI, simp add: lookup_monom_mult)

lemma uminus_monom_mult: "- p = monom_mult (-1::'b::comm_ring_1) 0 p"
by (rule poly_mapping_eqI, simp add: lookup_monom_mult term_simps)

lemma monom_mult_dist_left: "monom_mult (c + d) t p = (monom_mult c t p) + (monom_mult d t p)"

lemma monom_mult_dist_left_minus:
"monom_mult (c - d) t p = (monom_mult c t p) - (monom_mult (d::'b::ring) t p)"
using monom_mult_dist_left[of c "-d" t p] monom_mult_uminus_left[of d t p] by simp

lemma monom_mult_dist_right:
"monom_mult c t (p + q) = (monom_mult c t p) + (monom_mult c t q)"

lemma monom_mult_dist_right_minus:
"monom_mult c t (p - q) = (monom_mult c t p) - (monom_mult (c::'b::ring) t q)"
using monom_mult_dist_right[of c t p "-q"] monom_mult_uminus_right[of c t q] by simp

lemma monom_mult_zero_left [simp]: "monom_mult 0 t p = 0"
by (rule poly_mapping_eqI, simp add: lookup_monom_mult)

lemma monom_mult_zero_right [simp]: "monom_mult c t 0 = 0"
by (rule poly_mapping_eqI, simp add: lookup_monom_mult)

lemma monom_mult_one_left [simp]: "(monom_mult (1::'b::semiring_1) 0 p) = p"
by (rule poly_mapping_eqI, simp add: lookup_monom_mult term_simps)

lemma monom_mult_monomial:
"monom_mult c s (monomial d v) = monomial (c * (d::'b::semiring_0)) (s  v)"
by (rule poly_mapping_eqI, auto simp add: lookup_monom_mult lookup_single adds_pp_alt when_def term_simps, metis)

lemma monom_mult_eq_zero_iff: "(monom_mult c t p = 0)  ((c::'b::semiring_no_zero_divisors) = 0  p = 0)"
proof
assume eq: "monom_mult c t p = 0"
show "c = 0  p = 0"
proof (rule ccontr, simp)
assume "c  0  p  0"
hence "c  0" and "p  0" by simp_all
from lookup_zero poly_mapping_eq_iff[of p 0] p  0 obtain v where "lookup p v  0" by fastforce
from eq lookup_zero have "lookup (monom_mult c t p) (t  v) = 0" by simp
hence "c * lookup p v = 0" by (simp only: lookup_monom_mult_plus)
with c  0 lookup p v  0 show False by auto
qed
next
assume "c = 0  p = 0"
with monom_mult_zero_left[of t p] monom_mult_zero_right[of c t] show "monom_mult c t p = 0" by auto
qed

lemma lookup_monom_mult_zero: "lookup (monom_mult c 0 p) t = c * lookup p t"
proof -
have "lookup (monom_mult c 0 p) t = lookup (monom_mult c 0 p) (0  t)" by (simp add: term_simps)
also have "... = c * lookup p t" by (rule lookup_monom_mult_plus)
finally show ?thesis .
qed

lemma monom_mult_inj_1:
assumes "monom_mult c1 t p = monom_mult c2 t p"
and "(p::(_ 0 'b::semiring_no_zero_divisors_cancel))  0"
shows "c1 = c2"
proof -
from assms(2) have "keys p  {}" using poly_mapping_eq_zeroI by blast
then obtain v where "v  keys p" by blast
hence *: "lookup p v  0" by (simp add: in_keys_iff)
from assms(1) have "lookup (monom_mult c1 t p) (t  v) = lookup (monom_mult c2 t p) (t  v)"
by simp
hence "c1 * lookup p v = c2 * lookup p v" by (simp only: lookup_monom_mult_plus)
with * show ?thesis by auto
qed

text Multiplication by a monomial is injective in the second argument (the power-product) only in
context @{locale ordered_powerprod}; see lemma monom_mult_inj_2› below.

lemma monom_mult_inj_3:
assumes "monom_mult c t p1 = monom_mult c t (p2::(_ 0 'b::semiring_no_zero_divisors_cancel))"
and "c  0"
shows "p1 = p2"
proof (rule poly_mapping_eqI)
fix v
from assms(1) have "lookup (monom_mult c t p1) (t  v) = lookup (monom_mult c t p2) (t  v)"
by simp
hence "c * lookup p1 v = c * lookup p2 v" by (simp only: lookup_monom_mult_plus)
with assms(2) show "lookup p1 v = lookup p2 v" by simp
qed

lemma keys_monom_multI:
assumes "v  keys p" and "c  (0::'b::semiring_no_zero_divisors)"
shows "t  v  keys (monom_mult c t p)"
using assms unfolding in_keys_iff lookup_monom_mult_plus by simp

lemma keys_monom_mult_subset: "keys (monom_mult c t p)  ((⊕) t) ` (keys p)"
proof -
have "keys (monom_mult c t p)  {v. (if t addsp v then c * lookup p (v  t) else 0)  0}" (is "_  ?A")
proof
fix v
assume "v  keys (monom_mult c t p)"
hence "lookup (monom_mult c t p) v  0" by (simp add: in_keys_iff)
thus "v  ?A" unfolding lookup_monom_mult by simp
qed
also note keys_monom_mult_aux
finally show ?thesis .
qed

lemma keys_monom_multE:
assumes "v  keys (monom_mult c t p)"
obtains u where "u  keys p" and "v = t  u"
proof -
note assms
also have "keys (monom_mult c t p)  ((⊕) t) ` (keys p)" by (fact keys_monom_mult_subset)
finally have "v  ((⊕) t) ` (keys p)" .
then obtain u where "u  keys p" and "v = t  u" ..
thus ?thesis ..
qed

lemma keys_monom_mult:
assumes "c  (0::'b::semiring_no_zero_divisors)"
shows "keys (monom_mult c t p) = ((⊕) t) ` (keys p)"
proof (rule, fact keys_monom_mult_subset, rule)
fix v
assume "v  (⊕) t ` keys p"
then obtain u where "u  keys p" and v: "v = t  u" ..
from u  keys p assms show "v  keys (monom_mult c t p)" unfolding v by (rule keys_monom_multI)
qed

lemma monom_mult_when: "monom_mult c t (p when P) = ((monom_mult c t p) when P)"
by (cases P, simp_all)

lemma when_monom_mult: "monom_mult (c when P) t p = ((monom_mult c t p) when P)"
by (cases P, simp_all)

lemma monomial_power: "(monomial c t) ^ n = monomial (c ^ n) (i=0..<n. t)"

subsection Component-wise Lifting

text Component-wise lifting of functions on @{typ "'a 0 'b"} to functions on @{typ "'t 0 'b"}.

definition lift_poly_fun_2 :: "(('a 0 'b)  ('a 0 'b)  ('a 0 'b))  ('t 0 'b)  ('t 0 'b)  ('t 0 'b::zero)"
where "lift_poly_fun_2 f p q = atomize_poly (mapp_2 (λ_. f) (vectorize_poly p) (vectorize_poly q))"

definition lift_poly_fun :: "(('a 0 'b)  ('a 0 'b))  ('t 0 'b)  ('t 0 'b::zero)"
where "lift_poly_fun f p = lift_poly_fun_2 (λ_. f) 0 p"

lemma lookup_lift_poly_fun_2:

by (simp add: lift_poly_fun_2_def lookup_atomize_poly lookup_mapp_2 lookup_vectorize_poly
when_distrib[of _ "λq. lookup q (pp_of_term v)", OF lookup_zero])

lemma lookup_lift_poly_fun:

by (simp add: lift_poly_fun_def lookup_lift_poly_fun_2 term_simps)

lemma lookup_lift_poly_fun_2_homogenous:
assumes "f 0 0 = 0"
shows "lookup (lift_poly_fun_2 f p q) v =
lookup (f (proj_poly (component_of_term v) p) (proj_poly (component_of_term v) q)) (pp_of_term v)"
by (simp add: lookup_lift_poly_fun_2 when_def in_keys_iff lookup_vectorize_poly assms)

lemma proj_lift_poly_fun_2_homogenous:
assumes "f 0 0 = 0"
shows "proj_poly k (lift_poly_fun_2 f p q) = f (proj_poly k p) (proj_poly k q)"
by (rule poly_mapping_eqI,
simp add: lookup_proj_poly lookup_lift_poly_fun_2_homogenous[of f, OF assms] term_simps)

lemma lookup_lift_poly_fun_homogenous:
assumes "f 0 = 0"
shows "lookup (lift_poly_fun f p) v = lookup (f (proj_poly (component_of_term v) p)) (pp_of_term v)"
by (simp add: lookup_lift_poly_fun when_def in_keys_iff lookup_vectorize_poly assms)

lemma proj_lift_poly_fun_homogenous:
assumes "f 0 = 0"
shows "proj_poly k (lift_poly_fun f p) = f (proj_poly k p)"
by (rule poly_mapping_eqI,
simp add: lookup_proj_poly lookup_lift_poly_fun_homogenous[of f, OF assms] term_simps)

subsection Component-wise Multiplication

definition mult_vec :: "('t 0 'b)  ('t 0 'b)  ('t 0 'b::semiring_0)" (infixl "**" 75)
where "mult_vec = lift_poly_fun_2 (*)"

lemma lookup_mult_vec:
"lookup (p ** q) v = lookup ((proj_poly (component_of_term v) p) * (proj_poly (component_of_term v) q)) (pp_of_term v)"
unfolding mult_vec_def by (rule lookup_lift_poly_fun_2_homogenous, simp)

lemma proj_mult_vec [term_simps]: "proj_poly k (p ** q) = (proj_poly k p) * (proj_poly k q)"
unfolding mult_vec_def by (rule proj_lift_poly_fun_2_homogenous, simp)

lemma mult_vec_zero_left: "0 ** p = 0"
by (rule poly_mapping_eqI_proj, simp add: term_simps)

lemma mult_vec_zero_right: "p ** 0 = 0"
by (rule poly_mapping_eqI_proj, simp add: term_simps)

lemma mult_vec_assoc: "(p ** q) ** r = p ** (q ** r)"
by (rule poly_mapping_eqI_proj, simp add: ac_simps term_simps)

lemma mult_vec_distrib_right: "(p + q) ** r = p ** r + q ** r"
by (rule poly_mapping_eqI_proj, simp add: algebra_simps proj_plus term_simps)

lemma mult_vec_distrib_left: "r ** (p + q) = r ** p + r ** q"
by (rule poly_mapping_eqI_proj, simp add: algebra_simps proj_plus term_simps)

lemma mult_vec_minus_mult_left: "(- p) ** q = - (p ** q)"
by (rule sym, rule minus_unique, simp add: mult_vec_distrib_right[symmetric] mult_vec_zero_left)

lemma mult_vec_minus_mult_right: "p ** (- q) = - (p ** q)"
by (rule sym, rule minus_unique, simp add: mult_vec_distrib_left [symmetric] mult_vec_zero_right)

lemma minus_mult_vec_minus: "(- p) ** (- q) = p ** q"

lemma minus_mult_vec_commute: "(- p) ** q = p ** (- q)"

lemma mult_vec_right_diff_distrib: "r ** (p - q) = r ** p - r ** q"
for r::"_ 0 'b::ring"
using mult_vec_distrib_left [of r p "- q"] by (simp add: mult_vec_minus_mult_right)

lemma mult_vec_left_diff_distrib: "(p - q) ** r = p ** r - q ** r"
for p::"_ 0 'b::ring"
using mult_vec_distrib_right [of p "- q" r] by (simp add: mult_vec_minus_mult_left)

lemma mult_vec_commute: "p ** q = q ** p" for p::"_ 0 'b::comm_semiring_0"
by (rule poly_mapping_eqI_proj, simp add: term_simps ac_simps)

lemma mult_vec_left_commute: "p ** (q ** r) = q ** (p ** r)"
for p::"_ 0 'b::comm_semiring_0"
by (rule poly_mapping_eqI_proj, simp add: term_simps ac_simps)

lemma mult_vec_monomial_monomial:
"(monomial c u) ** (monomial d v) =
(monomial (c * d) (term_of_pair (pp_of_term u + pp_of_term v, component_of_term u)) when
component_of_term u = component_of_term v)"
by (rule poly_mapping_eqI_proj, simp add: proj_monomial mult_single when_def term_simps)

lemma mult_vec_rec_left: "p ** q = monomial (lookup p v) v ** q + (except p {v}) ** q"
proof -
from plus_except[of p v] have "p ** q = (monomial (lookup p v) v + except p {v}) ** q" by simp
also have "... = monomial (lookup p v) v ** q + except p {v} ** q"
by (simp only: mult_vec_distrib_right)
finally show ?thesis .
qed

lemma mult_vec_rec_right: "p ** q = p ** monomial (lookup q v) v + p ** except q {v}"
proof -
have "p ** monomial (lookup q v) v + p ** except q {v} = p ** (monomial (lookup q v) v + except q {v})"
by (simp only: mult_vec_distrib_left)
also have "... = p ** q" by (simp only: plus_except[of q v, symmetric])
finally show ?thesis by simp
qed

lemma in_keys_mult_vecE:
assumes "w  keys (p ** q)"
obtains u v where "u  keys p" and "v  keys q" and
and "w = term_of_pair (pp_of_term u + pp_of_term v, component_of_term u)"
proof -
from assms have "0  lookup (p ** q) w" by (simp add: in_keys_iff)
also have "lookup (p ** q) w =
lookup ((proj_poly (component_of_term w) p) * (proj_poly (component_of_term w) q)) (pp_of_term w)"
by (fact lookup_mult_vec)
finally have "pp_of_term w  keys ((proj_poly (component_of_term w) p) * (proj_poly (component_of_term w) q))"
from this keys_mult
have "pp_of_term w  {t + s |t s. t  keys (proj_poly (component_of_term w) p)
s  keys (proj_poly (component_of_term w) q)}" ..
then obtain t s where 1: "t  keys (proj_poly (component_of_term w) p)"
and 2: "s  keys (proj_poly (component_of_term w) q)"
and eq: "pp_of_term w = t + s" by fastforce
let ?u = "term_of_pair (t, component_of_term w)"
let ?v = "term_of_pair (s, component_of_term w)"
from 1 have "?u  keys p" by (simp only: in_keys_iff lookup_proj_poly not_False_eq_True)
moreover from 2 have "?v  keys q" by (simp only: in_keys_iff lookup_proj_poly not_False_eq_True)
moreover have  by (simp add: term_simps)
moreover have "w = term_of_pair (pp_of_term ?u + pp_of_term ?v, component_of_term ?u)"
ultimately show ?thesis ..
qed

lemma lookup_mult_vec_monomial_left:
"lookup (monomial c v ** p) u =
(c * lookup p (term_of_pair (pp_of_term u - pp_of_term v, component_of_term u)) when v addst u)"
proof -
have eq1:
by (rule when_distrib, simp)
show ?thesis
by (simp add: lookup_mult_vec proj_monomial eq1 lookup_times_monomial_left when_when
qed

lemma lookup_mult_vec_monomial_right:
"lookup (p ** monomial c v) u =
(lookup p (term_of_pair (pp_of_term u - pp_of_term v, component_of_term u)) * c when v addst u)"
proof -
have eq1:
by (rule when_distrib, simp)
show ?thesis
by (simp add: lookup_mult_vec proj_monomial eq1 lookup_times_monomial_right when_when
qed

subsection Scalar Multiplication

definition mult_scalar :: "('a 0 'b)  ('t 0 'b)  ('t 0 'b::semiring_0)" (infixl "" 75)
where "mult_scalar p = lift_poly_fun ((*) p)"

lemma lookup_mult_scalar:
"lookup (p  q) v = lookup (p * (proj_poly (component_of_term v) q)) (pp_of_term v)"
unfolding mult_scalar_def by (rule lookup_lift_poly_fun_homogenous, simp)

lemma lookup_mult_scalar_explicit:
"lookup (p  q) u = (tkeys p. lookup p t * (vkeys q. lookup q v when u = t  v))"
proof -
let ?f = "λt s. lookup (proj_poly (component_of_term u) q) s when pp_of_term u = t + s"
note lookup_mult_scalar
also have "lookup (p * proj_poly (component_of_term u) q) (pp_of_term u) =
(t. lookup p t * (Sum_any (?f t)))"
by (fact lookup_mult)
also from finite_keys have " = (tkeys p. lookup p t * (Sum_any (?f t)))"
by (rule Sum_any.expand_superset) (auto simp: in_keys_iff dest: mult_not_zero)
also from refl have " = (tkeys p. lookup p t * (vkeys q. lookup q v when u = t  v))"
proof (rule sum.cong)
fix t
assume "t  keys p"
from finite_keys have "Sum_any (?f t) = (skeys (proj_poly (component_of_term u) q). ?f t s)"
by (rule Sum_any.expand_superset) (auto simp: in_keys_iff)
also have " = (v{x  keys q. component_of_term x = component_of_term u}. ?f t (pp_of_term v))"
unfolding keys_proj_poly
proof (intro sum.reindex[simplified o_def] inj_onI)
fix v1 v2
assume "v1  {x  keys q. component_of_term x = component_of_term u}"
and "v2  {x  keys q. component_of_term x = component_of_term u}"
hence  by simp
moreover assume "pp_of_term v1 = pp_of_term v2"
ultimately show "v1 = v2" by (metis term_of_pair_pair)
qed
also from finite_keys have " = (vkeys q. lookup q v when u = t  v)"
proof (intro sum.mono_neutral_cong_left ballI)
fix v
assume "v  keys q - {x  keys q. component_of_term x = component_of_term u}"
hence "u  t  v" by (auto simp: component_of_term_splus)
thus "(lookup q v when u = t  v) = 0" by simp
next
fix v
assume "v  {x  keys q. component_of_term x = component_of_term u}"
hence eq[symmetric]:  by simp
have "u = t  v  pp_of_term u = t + pp_of_term v"
proof
assume
hence "pp_of_term u = pp_of_term (t  v)" by (simp only: pp_of_term_splus)
moreover have
by (simp only: eq component_of_term_splus)
ultimately show "u = t  v" by (metis term_of_pair_pair)
thus "?f t (pp_of_term v) = (lookup q v when u = t  v)"
by (simp add: lookup_proj_poly eq term_of_pair_pair)
qed auto
finally show "lookup p t * (Sum_any (?f t)) = lookup p t * (vkeys q. lookup q v when u = t  v)"
by (simp only:)
qed
finally show ?thesis .
qed

lemma proj_mult_scalar [term_simps]: "proj_poly k (p  q) = p * (proj_poly k q)"
unfolding mult_scalar_def by (rule proj_lift_poly_fun_homogenous, simp)

lemma mult_scalar_zero_left [simp]: "0  p = 0"
by (rule poly_mapping_eqI_proj, simp add: term_simps)

lemma mult_scalar_zero_right [simp]: "p  0 = 0"
by (rule poly_mapping_eqI_proj, simp add: term_simps)

lemma mult_scalar_one [simp]: "(1::_ 0 'b::semiring_1)  p = p"
by (rule poly_mapping_eqI_proj, simp add: term_simps)

lemma mult_scalar_assoc [ac_simps]: "(p * q)  r = p  (q  r)"
by (rule poly_mapping_eqI_proj, simp add: ac_simps term_simps)

lemma mult_scalar_distrib_right [algebra_simps]: "(p + q)  r = p  r + q  r"
by (rule poly_mapping_eqI_proj, simp add: algebra_simps proj_plus term_simps)

lemma mult_scalar_distrib_left [algebra_simps]: "r  (p + q) = r  p + r  q"
by (rule poly_mapping_eqI_proj, simp add: algebra_simps proj_plus term_simps)

lemma mult_scalar_minus_mult_left [simp]: "(- p)  q = - (p  q)"
by (rule sym, rule minus_unique, simp add: mult_scalar_distrib_right[symmetric])

lemma mult_scalar_minus_mult_right [simp]: "p  (- q) = - (p  q)"
by (rule sym, rule minus_unique, simp add: mult_scalar_distrib_left [symmetric])

lemma minus_mult_scalar_minus [simp]: "(- p)  (- q) = p  q"
by simp

lemma minus_mult_scalar_commute: "(- p)  q = p  (- q)"
by simp

lemma mult_scalar_right_diff_distrib [algebra_simps]: "r  (p - q) = r  p - r  q"
for r::"_ 0 'b::ring"
using mult_scalar_distrib_left [of r p "- q"] by simp

lemma mult_scalar_left_diff_distrib [algebra_simps]: "(p - q)  r = p  r - q  r"
for p::"_ 0 'b::ring"
using mult_scalar_distrib_right [of p "- q" r] by simp

lemma sum_mult_scalar_distrib_left: "r  (sum f A) = (aA. r  f a)"
by (induct A rule: infinite_finite_induct, simp_all add: algebra_simps)

lemma sum_mult_scalar_distrib_right: "(sum f A)  v = (aA. f a  v)"
by (induct A rule: infinite_finite_induct, simp_all add: algebra_simps)

lemma mult_scalar_monomial_monomial: "(monomial c t)  (monomial d v) = monomial (c * d) (t  v)"
by (rule poly_mapping_eqI_proj, simp add: proj_monomial mult_single when_def term_simps)

lemma mult_scalar_monomial: "(monomial c t)  p = monom_mult c t p"
by (rule poly_mapping_eqI_proj, rule poly_mapping_eqI,
auto simp add: lookup_times_monomial_left lookup_proj_poly lookup_monom_mult when_def

lemma mult_scalar_rec_left: "p  q = monom_mult (lookup p t) t q + (except p {t})  q"
proof -
from plus_except[of p t] have "p  q = (monomial (lookup p t) t + except p {t})  q" by simp
also have "... = monomial (lookup p t) t  q + except p {t}  q" by (simp only: algebra_simps)
finally show ?thesis by (simp only: mult_scalar_monomial)
qed

lemma mult_scalar_rec_right: "p  q = p  monomial (lookup q v) v + p  except q {v}"
proof -
have "p  monomial (lookup q v) v + p  except q {v} = p  (monomial (lookup q v) v + except q {v})"
by (simp only: mult_scalar_distrib_left)
also have "... = p  q" by (simp only: plus_except[of q v, symmetric])
finally show ?thesis by simp
qed

lemma in_keys_mult_scalarE:
assumes "v  keys (p  q)"
obtains t u where "t  keys p" and "u  keys q" and "v = t  u"
proof -
from assms have "0  lookup (p  q) v" by (simp add: in_keys_iff)
also have "lookup (p  q) v = lookup (p * (proj_poly (component_of_term v) q)) (pp_of_term v)"
by (fact lookup_mult_scalar)
finally have  by (simp add: in_keys_iff)
from this keys_mult have "pp_of_term v  {t + s |t s. t  keys p  s  keys (proj_poly (component_of_term v) q)}" ..
then obtain t s where "t  keys p" and *: "s  keys (proj_poly (component_of_term v) q)"
and eq: "pp_of_term v = t + s" by fastforce
note this(1)
moreover from * have "term_of_pair (s, component_of_term v)  keys q"
by (simp only: in_keys_iff lookup_proj_poly not_False_eq_True)
moreover have "v = t  term_of_pair (s, component_of_term v)"
by (simp add: splus_def eq[symmetric] term_simps)
ultimately show ?thesis ..
qed

lemma lookup_mult_scalar_monomial_right:
"lookup (p  monomial c v) u = (lookup p (pp_of_term u - pp_of_term v) * c when v addst u)"
proof -
have eq1: