Theory MPoly_Type_Class
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"
by (simp add: Poly_Mapping.keys_add)
show "keys p ∪ keys q ⊆ keys (p + q)"
by (simp add: More_MPoly_Type.keys_add assms)
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}"
by (simp add: algebra_simps)
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"
by (simp only: lookup_add IH)
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)
assume "t adds s"
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)"
by (simp add: u, cases "u = w", simp_all add: lookup_except lookup_single add.commute)
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"
by (simp add: algebra_simps)
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"
by (simp only: lookup_add IH)
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)
assume "t adds s"
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"
by (simp add: u, cases "u = w", simp_all add: lookup_except lookup_single add.commute)
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"
by (simp add: pp_of_term_def pair_term)
lemma component_of_term_of_pair [term_simps]: "component_of_term (term_of_pair (t, k)) = k"
by (simp add: component_of_term_def pair_term)
subsubsection ‹Additive Structure of Terms›
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}.›
definition adds_pp :: "'a ⇒ 't ⇒ bool" (infix "adds⇩p" 50)
where "adds_pp t v ⟷ t adds pp_of_term v"
definition adds_term :: "'t ⇒ 't ⇒ bool" (infix "adds⇩t" 50)
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"
by (simp add: splus_def term_simps)
lemma component_of_term_splus [term_simps]: "component_of_term (t ⊕ v) = component_of_term v"
by (simp add: splus_def term_simps)
lemma pp_of_term_sminus [term_simps]: "pp_of_term (v ⊖ t) = pp_of_term v - t"
by (simp add: sminus_def term_simps)
lemma component_of_term_sminus [term_simps]: "component_of_term (v ⊖ t) = component_of_term v"
by (simp add: sminus_def term_simps)
lemma splus_sminus [term_simps]: "(t ⊕ v) ⊖ t = v"
by (simp add: sminus_def term_simps)
lemma splus_zero [term_simps]: "0 ⊕ v = v"
by (simp add: splus_def term_simps)
lemma sminus_zero [term_simps]: "v ⊖ 0 = v"
by (simp add: sminus_def term_simps)
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"
by (metis add_right_cancel pp_of_term_splus)
lemma splus_left_canc [term_simps]: "t ⊕ v = t ⊕ u ⟷ v = u"
by (metis splus_sminus)
lemma adds_ppI [intro?]:
assumes "v = t ⊕ u"
shows "t adds⇩p v"
by (simp add: adds_pp_def assms splus_def term_simps)
lemma adds_ppE [elim?]:
assumes "t adds⇩p v"
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))"
by (simp add: splus_def term_simps, metis * add.commute term_of_pair_pair)
thus ?thesis ..
qed
lemma adds_pp_alt: "t adds⇩p v ⟷ (∃u. v = t ⊕ u)"
by (meson adds_ppE adds_ppI)
lemma adds_pp_refl [term_simps]: "(pp_of_term v) adds⇩p v"
by (simp add: adds_pp_def)
lemma adds_pp_trans [trans]:
assumes "s adds t" and "t adds⇩p v"
shows "s adds⇩p v"
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
lemma zero_adds_pp [term_simps]: "0 adds⇩p v"
by (simp add: adds_pp_def)
lemma adds_pp_splus:
assumes "t adds⇩p v"
shows "t adds⇩p s ⊕ v"
using assms by (simp add: adds_pp_def term_simps)
lemma adds_pp_triv [term_simps]: "t adds⇩p t ⊕ v"
by (simp add: adds_pp_def term_simps)
lemma plus_adds_pp_mono:
assumes "s adds t"
and "u adds⇩p v"
shows "s + u adds⇩p t ⊕ v"
using assms by (simp add: adds_pp_def term_simps) (rule plus_adds_mono)
lemma plus_adds_pp_left:
assumes "s + t adds⇩p v"
shows "s adds⇩p v"
using assms by (simp add: adds_pp_def plus_adds_left)
lemma plus_adds_pp_right:
assumes "s + t adds⇩p v"
shows "t adds⇩p v"
using assms by (simp add: adds_pp_def plus_adds_right)
lemma adds_pp_sminus:
assumes "t adds⇩p 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
lemma adds_pp_canc: "t + s adds⇩p (t ⊕ v) ⟷ s adds⇩p v"
by (simp add: adds_pp_def adds_canc_2 term_simps)
lemma adds_pp_canc_2: "s + t adds⇩p (t ⊕ v) ⟷ s adds⇩p v"
by (simp add: adds_pp_canc add.commute[of s t])
lemma plus_adds_pp_0:
assumes "(s + t) adds⇩p v"
shows "s adds⇩p (v ⊖ t)"
using assms by (simp add: adds_pp_def term_simps) (rule plus_adds_0)
lemma plus_adds_ppI_1:
assumes "t adds⇩p v" and "s adds⇩p (v ⊖ t)"
shows "(s + t) adds⇩p v"
using assms by (simp add: adds_pp_def term_simps) (rule plus_adds_2)
lemma plus_adds_ppI_2:
assumes "t adds⇩p v" and "s adds⇩p (v ⊖ t)"
shows "(t + s) adds⇩p v"
unfolding add.commute[of t s] using assms by (rule plus_adds_ppI_1)
lemma plus_adds_pp: "(s + t) adds⇩p v ⟷ (t adds⇩p v ∧ s adds⇩p (v ⊖ t))"
by (simp add: adds_pp_def plus_adds term_simps)
lemma minus_splus:
assumes "s adds t"
shows "(t - s) ⊕ v = (t ⊕ v) ⊖ s"
by (simp add: assms minus_plus sminus_def splus_def term_simps)
lemma minus_splus_sminus:
assumes "s adds t" and "u adds⇩p v"
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:
assumes "s adds t" and "t adds⇩p v"
shows "(t - s) ⊕ (v ⊖ t) = v ⊖ s"
by (simp add: adds_pp_sminus assms minus_splus)
lemma sminus_plus:
assumes "s adds⇩p v" and "t adds⇩p (v ⊖ s)"
shows "v ⊖ (s + t) = (v ⊖ s) ⊖ t"
by (simp add: diff_diff_add sminus_def term_simps)
lemma adds_termI [intro?]:
assumes "v = t ⊕ u"
shows "u adds⇩t v"
by (simp add: adds_term_def assms splus_def term_simps)
lemma adds_termE [elim?]:
assumes "u adds⇩t v"
obtains t where "v = t ⊕ u"
proof -
from assms have eq: "component_of_term u = component_of_term v" and "pp_of_term u adds pp_of_term v"
by (simp_all add: adds_term_def)
from this(2) obtain s where *: "s + pp_of_term u = pp_of_term v" unfolding adds_term_def
using adds_minus by blast
have "v = s ⊕ u" by (simp add: splus_def eq * term_simps)
thus ?thesis ..
qed
lemma adds_term_alt: "u adds⇩t v ⟷ (∃t. v = t ⊕ u)"
by (meson adds_termE adds_termI)
lemma adds_term_refl [term_simps]: "v adds⇩t v"
by (simp add: adds_term_def)
lemma adds_term_trans [trans]:
assumes "u adds⇩t v" and "v adds⇩t w"
shows "u adds⇩t w"
using assms unfolding adds_term_def using adds_trans by auto
lemma adds_term_splus:
assumes "u adds⇩t v"
shows "u adds⇩t s ⊕ v"
using assms by (simp add: adds_term_def term_simps)
lemma adds_term_triv [term_simps]: "v adds⇩t t ⊕ v"
by (simp add: adds_term_def term_simps)
lemma splus_adds_term_mono:
assumes "s adds t"
and "u adds⇩t v"
shows "s ⊕ u adds⇩t t ⊕ v"
using assms by (auto simp: adds_term_def term_simps intro: plus_adds_mono)
lemma splus_adds_term:
assumes "t ⊕ u adds⇩t v"
shows "u adds⇩t v"
using assms by (auto simp add: adds_term_def term_simps elim: plus_adds_right)
lemma adds_term_adds_pp:
"u adds⇩t v ⟷ (component_of_term u = component_of_term v ∧ pp_of_term u adds⇩p v)"
by (simp add: adds_term_def adds_pp_def)
lemma adds_term_canc: "t ⊕ u adds⇩t t ⊕ v ⟷ u adds⇩t v"
by (simp add: adds_term_def adds_canc_2 term_simps)
lemma adds_term_canc_2: "s ⊕ v adds⇩t t ⊕ v ⟷ s adds t"
by (simp add: adds_term_def adds_canc term_simps)
lemma splus_adds_term_0:
assumes "t ⊕ u adds⇩t v"
shows "u adds⇩t (v ⊖ t)"
using assms by (simp add: adds_term_def add.commute[of t] term_simps) (auto intro: plus_adds_0)
lemma splus_adds_termI_1:
assumes "t adds⇩p v" and "u adds⇩t (v ⊖ t)"
shows "t ⊕ u adds⇩t v"
using assms apply (simp add: adds_term_def term_simps) by (metis add.commute adds_pp_def plus_adds_2)
lemma splus_adds_term_iff: "t ⊕ u adds⇩t v ⟷ (t adds⇩p v ∧ u adds⇩t (v ⊖ t))"
by (metis adds_ppI adds_pp_splus adds_termE splus_adds_termI_1 splus_adds_term_0)
lemma adds_minus_splus:
assumes "pp_of_term u adds t"
shows "(t - pp_of_term u) ⊕ u = term_of_pair (t, component_of_term u)"
by (simp add: splus_def adds_minus[OF assms])
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
thus "k ∈ component_of_term ` keys p" by (simp add: term_simps)
qed
moreover from finite_keys have "finite (component_of_term ` keys p)" 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))} ⊆
(⋃k∈keys p. (λt. term_of_pair (t, k)) ` keys (lookup p k))" (is "_ ⊆ ?A")
proof (rule, simp)
fix v
assume *: "pp_of_term v ∈ keys (lookup p (component_of_term v))"
hence "keys (lookup p (component_of_term v)) ≠ {}" by blast
hence "lookup p (component_of_term v) ≠ 0" by auto
hence "component_of_term v ∈ keys p" (is "?k ∈ _")
by (simp add: in_keys_iff)
thus "∃k∈keys 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}"
by (simp add: finite_subset in_keys_iff)
qed
thus ?thesis by (simp add: atomize_poly_def)
qed
lemma keys_proj_poly: "keys (proj_poly k p) = pp_of_term ` {x∈keys p. component_of_term x = k}"
proof
show "keys (proj_poly k p) ⊆ pp_of_term ` {x∈keys 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) ∈ {x∈keys p. component_of_term x = k}" by (simp add: term_simps)
hence "pp_of_term (term_of_pair (t, k)) ∈ pp_of_term ` {x∈keys p. component_of_term x = k}" by (rule imageI)
thus "t ∈ pp_of_term ` {x∈keys p. component_of_term x = k}" by (simp only: pp_of_term_of_pair)
qed
next
show "pp_of_term ` {x∈keys p. component_of_term x = k} ⊆ keys (proj_poly k p)"
proof
fix t
assume "t ∈ pp_of_term ` {x∈keys p. component_of_term x = k}"
then obtain x where "x ∈ {x∈keys p. component_of_term x = k}" and "t = pp_of_term x" ..
from this(1) have "x ∈ keys p" and "k = component_of_term x" 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: "keys (vectorize_poly p) = component_of_term ` keys p"
proof
show "keys (vectorize_poly p) ⊆ component_of_term ` keys p"
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 "k ∈ component_of_term ` keys p" by (simp only: component_of_term_of_pair)
qed
next
show "component_of_term ` keys p ⊆ keys (vectorize_poly p)"
proof
fix k
assume "k ∈ component_of_term ` keys p"
then obtain x where "x ∈ keys p" and "k = component_of_term x" ..
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) = (⋃k∈keys 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 *: "pp_of_term v ∈ keys (lookup p (component_of_term v))" by (simp add: in_keys_iff lookup_atomize_poly)
hence "lookup p (component_of_term v) ≠ 0" by fastforce
hence "component_of_term v ∈ keys p" by (simp add: in_keys_iff)
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]: "vectorize_poly (atomize_poly p) = p"
by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly term_simps)
lemma atomize_vectorize_poly [term_simps]: "atomize_poly (vectorize_poly p) = p"
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"
by (rule poly_mapping_eqI, simp add: lookup_proj_poly lookup_add)
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]: "vectorize_poly 0 = 0"
by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly term_simps)
lemma vectorize_plus: "vectorize_poly (p + q) = vectorize_poly p + vectorize_poly q"
by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly lookup_add proj_plus)
lemma vectorize_uminus [term_simps]: "vectorize_poly (- p) = - vectorize_poly p"
by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly term_simps)
lemma vectorize_minus: "vectorize_poly (p - q) = vectorize_poly p - vectorize_poly q"
by (rule poly_mapping_eqI, simp add: lookup_vectorize_poly lookup_minus proj_minus)
lemma atomize_zero [term_simps]: "atomize_poly 0 = 0"
by (rule poly_mapping_eqI, simp add: lookup_atomize_poly)
lemma atomize_plus: "atomize_poly (p + q) = atomize_poly p + atomize_poly q"
by (rule poly_mapping_eqI, simp add: lookup_atomize_poly lookup_add)
lemma atomize_uminus [term_simps]: "atomize_poly (- p) = - atomize_poly p"
by (rule poly_mapping_eqI, simp add: lookup_atomize_poly)
lemma atomize_minus: "atomize_poly (p - q) = atomize_poly p - atomize_poly q"
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: "component_of_term v = k"
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:
"vectorize_poly (monomial c v) = monomial (monomial c (pp_of_term v)) (component_of_term v)"
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: "k = component_of_term v" 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 "proj_poly (component_of_term v) p = proj_poly (component_of_term v) q" by (rule assms)
hence "lookup (proj_poly (component_of_term v) p) (pp_of_term v) =
lookup (proj_poly (component_of_term v) q) (pp_of_term v)" 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 adds⇩p v then c * (lookup p (v ⊖ t)) else 0)"
lemma keys_monom_mult_aux:
"{v. (if t adds⇩p 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 adds⇩p v then c * lookup p (v ⊖ t) else 0) ≠ 0" by simp
hence "t adds⇩p 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 adds⇩p v›] show "v = t ⊕ (v ⊖ t)" by simp
next
from mult_not_zero[OF cp_not_zero] show "v ⊖ t ∈ keys p"
by (simp add: in_keys_iff)
qed
qed
lemma lookup_monom_mult:
"lookup (monom_mult c t p) v = (if t adds⇩p v then c * lookup p (v ⊖ t) else 0)"
proof -
have "lookup (monom_mult c t p) = (λv. if t adds⇩p 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 adds⇩p v then c * lookup p (v ⊖ t) else 0) ≠ 0}"
by (rule finite_subset)
thus "(λv. if t adds⇩p 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"
by (simp add: lookup_monom_mult term_simps)
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
assume "s adds⇩p v" and "t adds⇩p v ⊖ s"
hence "s + t adds⇩p v" by (rule plus_adds_ppI_2)
moreover assume "¬ s + t adds⇩p v"
ultimately show "c * (d * lookup p (v ⊖ s ⊖ t)) = 0" by simp
next
fix v
assume "s + t adds⇩p v"
hence "s adds⇩p v" by (rule plus_adds_pp_left)
moreover assume "¬ s adds⇩p v"
ultimately show "c * (d * lookup p (v ⊖ (s + t))) = 0" by simp
next
fix v
assume "s + t adds⇩p v"
hence "t adds⇩p v ⊖ s" by (simp add: add.commute plus_adds_pp_0)
moreover assume "¬ t adds⇩p 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)"
by (rule poly_mapping_eqI, simp add: lookup_monom_mult lookup_add algebra_simps)
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)"
by (rule poly_mapping_eqI, simp add: lookup_monom_mult lookup_add algebra_simps)
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 adds⇩p 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)"
by (induct n, simp_all add: mult_single monom_mult_monomial add.commute)
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:
"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)
when component_of_term v ∈ keys (vectorize_poly p) ∪ keys (vectorize_poly q))"
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:
"lookup (lift_poly_fun f p) v =
(lookup (f (proj_poly (component_of_term v) p)) (pp_of_term v) when component_of_term v ∈ keys (vectorize_poly p))"
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"
by (simp add: mult_vec_minus_mult_left mult_vec_minus_mult_right)
lemma minus_mult_vec_commute: "(- p) ** q = p ** (- q)"
by (simp add: mult_vec_minus_mult_left mult_vec_minus_mult_right)
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 "component_of_term u = component_of_term v"
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))"
by (simp add: in_keys_iff)
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 "component_of_term ?u = component_of_term ?v" by (simp add: term_simps)
moreover have "w = term_of_pair (pp_of_term ?u + pp_of_term ?v, component_of_term ?u)"
by (simp add: eq[symmetric] term_simps)
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 adds⇩t u)"
proof -
have eq1: "lookup ((monomial c (pp_of_term v) when component_of_term v = component_of_term u) * proj_poly (component_of_term u) p)
(pp_of_term u) =
(lookup ((monomial c (pp_of_term v)) * proj_poly (component_of_term u) p) (pp_of_term u) when
component_of_term v = component_of_term u)"
by (rule when_distrib, simp)
show ?thesis
by (simp add: lookup_mult_vec proj_monomial eq1 lookup_times_monomial_left when_when
adds_term_def lookup_proj_poly conj_commute)
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 adds⇩t u)"
proof -
have eq1: "lookup (proj_poly (component_of_term u) p * (monomial c (pp_of_term v) when component_of_term v = component_of_term u))
(pp_of_term u) =
(lookup (proj_poly (component_of_term u) p * (monomial c (pp_of_term v))) (pp_of_term u) when
component_of_term v = component_of_term u)"
by (rule when_distrib, simp)
show ?thesis
by (simp add: lookup_mult_vec proj_monomial eq1 lookup_times_monomial_right when_when
adds_term_def lookup_proj_poly conj_commute)
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 = (∑t∈keys p. lookup p t * (∑v∈keys 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 "… = (∑t∈keys 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 "… = (∑t∈keys p. lookup p t * (∑v∈keys 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) = (∑s∈keys (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 "component_of_term v1 = component_of_term v2" 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 "… = (∑v∈keys 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]: "component_of_term v = component_of_term u" by simp
have "u = t ⊕ v ⟷ pp_of_term u = t + pp_of_term v"
proof
assume "pp_of_term u = t + pp_of_term v"
hence "pp_of_term u = pp_of_term (t ⊕ v)" by (simp only: pp_of_term_splus)
moreover have "component_of_term u = component_of_term (t ⊕ v)"
by (simp only: eq component_of_term_splus)
ultimately show "u = t ⊕ v" by (metis term_of_pair_pair)
qed (simp add: pp_of_term_splus)
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 * (∑v∈keys 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) = (∑a∈A. 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 = (∑a∈A. 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
adds_pp_def sminus_def term_simps)
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 "pp_of_term v ∈ keys (p * proj_poly (component_of_term v) q)" 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 adds⇩t u)"
proof -
have eq1: "lookup (p * (monomial c (pp_of_term v) when component_of_term v = component_of_term u)) (pp_of_term u) =
(lookup (p * (monomial c (pp_of_term v))) (pp_of_term u) when component_of_term v = component_of_term u)"
by (rule when_distrib, simp)
show ?thesis
by (simp add: lookup_mult_scalar eq1 proj_monomial lookup_times_monomial_right when_when
adds_term_def lookup_proj_poly conj_commute)
qed
lemma lookup_mult_scalar_monomial_right_plus: "lookup (p ⊙ monomial c v) (t ⊕ v) = lookup p t * c"
by (simp add: lookup_mult_scalar_monomial_right term_simps)
lemma keys_mult_scalar_monomial_right_subset: "keys (p ⊙ monomial c v) ⊆ (λt. t ⊕ v) ` keys p"
proof
fix u
assume "u ∈ keys (p ⊙ monomial c v)"
then obtain t w where "t ∈ keys p" and "w ∈ keys (monomial c v)" and "u = t ⊕ w"
by (rule in_keys_mult_scalarE)
from this(2) have "w = v" by (metis empty_iff insert_iff keys_single)
from ‹t ∈ keys p› show "u ∈ (λt. t ⊕ v) ` keys p" unfolding ‹u = t ⊕ w› ‹w = v› by fastforce
qed
lemma keys_mult_scalar_monomial_right:
assumes "c ≠ (0::'b::semiring_no_zero_divisors)"
shows "keys (p ⊙ monomial c v) = (λt. t ⊕ v) ` keys p"
proof
show "(λt. t ⊕ v) ` keys p ⊆ keys (p ⊙ monomial c v)"
proof
fix u
assume "u ∈ (λt. t ⊕ v) ` keys p"
then obtain t where "t ∈ keys p" and "u = t ⊕ v" ..
have "lookup (p ⊙ monomial c v) (t ⊕ v) = lookup p t * c"
by (fact lookup_mult_scalar_monomial_right_plus)
also from ‹t ∈ keys p› assms have "... ≠ 0" by (simp add: in_keys_iff)
finally show "u ∈ keys (p ⊙ monomial c v)" by (simp add: in_keys_iff ‹u = t ⊕ v›)
qed
qed (fact keys_mult_scalar_monomial_right_subset)
end
subsection ‹Sums and Products›
lemma sum_poly_mapping_eq_zeroI:
assumes "p ` A ⊆ {0}"
shows "sum p A = (0::(_ ⇒⇩0 'b::comm_monoid_add))"
proof (rule ccontr)
assume "sum p A ≠ 0"
then obtain a where "a ∈ A" and "p a ≠ 0"
by (rule comm_monoid_add_class.sum.not_neutral_contains_not_neutral)
with assms show False by auto
qed
lemma lookup_sum_list: "lookup (sum_list ps) a = sum_list (map (λp. lookup p a) ps)"
proof (induct ps)
case Nil
show ?case by simp
next
case (Cons p ps)
thus ?case by (simp add: lookup_add)
qed
text ‹Legacy:›
lemmas keys_sum_subset = Poly_Mapping.keys_sum
lemma keys_sum_list_subset: "keys (sum_list ps) ⊆ Keys (set ps)"
proof (induct ps)
case Nil
show ?case by simp
next
case (Cons p ps)
have "keys (sum_list (p # ps)) = keys (p + sum_list ps)" by simp
also have "… ⊆ keys p ∪ keys (sum_list ps)" by (fact Poly_Mapping.keys_add)
also from Cons have "… ⊆ keys p ∪ Keys (set ps)" by blast
also have "… = Keys (set (p # ps))" by (simp add: Keys_insert)
finally show ?case .
qed
lemma keys_sum:
assumes "finite A" and "⋀a1 a2. a1 ∈ A ⟹ a2 ∈ A ⟹ a1 ≠ a2 ⟹ keys (f a1) ∩ keys (f a2) = {}"
shows "keys (sum f A) = (⋃a∈A. keys (f a))"
using assms
proof (induct A)
case empty
show ?case by simp
next
case (insert a A)
have IH: "keys (sum f A) = (⋃i∈A. keys (f i))" by (rule insert(3), rule insert.prems, simp_all)
have "keys (sum f (insert a A)) = keys (f a) ∪ keys (sum f A)"
proof (simp only: comm_monoid_add_class.sum.insert[OF insert(1) insert(2)], rule keys_add[symmetric])
have "keys (f a) ∩ keys (sum f A) = (⋃i∈A. keys (f a) ∩ keys (f i))"
by (simp only: IH Int_UN_distrib)
also have "... = {}"
proof -
have "i ∈ A ⟹ keys (f a) ∩ keys (f i) = {}" for i
proof (rule insert.prems)
assume "i ∈ A"
with insert(2) show "a ≠ i" by blast
qed simp_all
thus ?thesis by simp
qed
finally show "keys (f a) ∩ keys (sum f A) = {}" .
qed
also have "... = (⋃a∈insert a A. keys (f a))" by (simp add: IH)
finally show ?case .
qed
lemma poly_mapping_sum_monomials: "(∑a∈keys p. monomial (lookup p a) a) = p"
proof (induct p rule: poly_mapping_plus_induct)
case 1
show ?case by simp
next
case step: (2 p c t)
from step(2) have "lookup p t = 0" by (simp add: in_keys_iff)
have *: "keys (monomial c t + p) = insert t (keys p)"
proof -
from step(1) have a: "keys (monomial c t) = {t}" by simp
with step(2) have "keys (monomial c t) ∩ keys p = {}" by simp
hence "keys (monomial c t + p) = {t} ∪ keys p" by (simp only: a keys_plus_eqI)
thus ?thesis by simp
qed
have **: "(∑ta∈keys p. monomial ((c when t = ta) + lookup p ta) ta) = (∑ta∈keys p. monomial (lookup p ta) ta)"
proof (rule comm_monoid_add_class.sum.cong, rule refl)
fix s
assume "s ∈ keys p"
with step(2) have "t ≠ s" by auto
thus "monomial ((c when t = s) + lookup p s) s = monomial (lookup p s) s" by simp
qed
show ?case by (simp only: * comm_monoid_add_class.sum.insert[OF finite_keys step(2)],
simp add: lookup_add lookup_single ‹lookup p t = 0› ** step(3))
qed
lemma monomial_sum: "monomial (sum f C) a = (∑c∈C. monomial (f c) a)"
by (rule fun_sum_commute, simp_all add: single_add)
lemma monomial_Sum_any:
assumes "finite {c. f c ≠ 0}"
shows "monomial (Sum_any f) a = (∑c. monomial (f c) a)"
proof -
have "{c. monomial (f c) a ≠ 0} ⊆ {c. f c ≠ 0}" by (rule, auto)
with assms show ?thesis
by (simp add: Groups_Big_Fun.comm_monoid_add_class.Sum_any.expand_superset monomial_sum)
qed
context term_powerprod
begin
lemma proj_sum: "proj_poly k (sum f A) = (∑a∈A. proj_poly k (f a))"
using proj_zero proj_plus by (rule fun_sum_commute)
lemma proj_sum_list: "proj_poly k (sum_list xs) = sum_list (map (proj_poly k) xs)"
using proj_zero proj_plus by (rule fun_sum_list_commute)
lemma mult_scalar_sum_monomials: "q ⊙ p = (∑t∈keys q. monom_mult (lookup q t) t p)"
by (rule poly_mapping_eqI_proj, simp add: proj_sum mult_scalar_monomial[symmetric]
sum_distrib_right[symmetric] poly_mapping_sum_monomials term_simps)
lemma fun_mult_scalar_commute:
assumes "f 0 = 0" and "⋀x y. f (x + y) = f x + f y"
and "⋀c t. f (monom_mult c t p) = monom_mult c t (f p)"
shows "f (q ⊙ p) = q ⊙ (f p)"
by (simp add: mult_scalar_sum_monomials assms(3)[symmetric], rule fun_sum_commute, fact+)
lemma fun_mult_scalar_commute_canc:
assumes "⋀x y. f (x + y) = f x + f y" and "⋀c t. f (monom_mult c t p) = monom_mult c t (f p)"
shows "f (q ⊙ p) = q ⊙ (f (p::'t ⇒⇩0 'b::{semiring_0,cancel_comm_monoid_add}))"
by (simp add: mult_scalar_sum_monomials assms(2)[symmetric], rule fun_sum_commute_canc, fact)
lemma monom_mult_sum_left: "monom_mult (sum f C) t p = (∑c∈C. monom_mult (f c) t p)"
by (rule fun_sum_commute, simp_all add: monom_mult_dist_left)
lemma monom_mult_sum_right: "monom_mult c t (sum f P) = (∑p∈P. monom_mult c t (f p))"
by (rule fun_sum_commute, simp_all add: monom_mult_dist_right)
lemma monom_mult_Sum_any_left:
assumes "finite {c. f c ≠ 0}"
shows "monom_mult (Sum_any f) t p = (∑c. monom_mult (f c) t p)"
proof -
have "{c. monom_mult (f c) t p ≠ 0} ⊆ {c. f c ≠ 0}" by (rule, auto)
with assms show ?thesis
by (simp add: Groups_Big_Fun.comm_monoid_add_class.Sum_any.expand_superset monom_mult_sum_left)
qed
lemma monom_mult_Sum_any_right:
assumes "finite {p. f p ≠ 0}"
shows "monom_mult c t (Sum_any f) = (∑p. monom_mult c t (f p))"
proof -
have "{p. monom_mult c t (f p) ≠ 0} ⊆ {p. f p ≠ 0}" by (rule, auto)
with assms show ?thesis
by (simp add: Groups_Big_Fun.comm_monoid_add_class.Sum_any.expand_superset monom_mult_sum_right)
qed
lemma monomial_prod_sum: "monomial (prod c I) (sum a I) = (∏i∈I. monomial (c i) (a i))"
proof (cases "finite I")
case True
thus ?thesis
proof (induct I)
case empty
show ?case by simp
next
case (insert i I)
show ?case
by (simp only: comm_monoid_add_class.sum.insert[OF insert(1) insert(2)]
comm_monoid_mult_class.prod.insert[OF insert(1) insert(2)] insert(3) mult_single[symmetric])
qed
next
case False
thus ?thesis by simp
qed
subsection ‹Submodules›
sublocale pmdl: module mult_scalar
apply standard
subgoal by (rule poly_mapping_eqI_proj, simp add: algebra_simps proj_plus)
subgoal by (rule poly_mapping_eqI_proj, simp add: algebra_simps proj_plus)
subgoal by (rule poly_mapping_eqI_proj, simp add: ac_simps)
subgoal by (rule poly_mapping_eqI_proj, simp)
done
lemmas [simp del] = pmdl.scale_one pmdl.scale_zero_left pmdl.scale_zero_right pmdl.scale_scale
pmdl.scale_minus_left pmdl.scale_minus_right pmdl.span_eq_iff
lemmas [algebra_simps del] = pmdl.scale_left_distrib pmdl.scale_right_distrib
pmdl.scale_left_diff_distrib pmdl.scale_right_diff_distrib
abbreviation "pmdl ≡ pmdl.span"
lemma pmdl_closed_monom_mult:
assumes "p ∈ pmdl B"
shows "monom_mult c t p ∈ pmdl B"
unfolding mult_scalar_monomial[symmetric] using assms by (rule pmdl.span_scale)
lemma monom_mult_in_pmdl: "b ∈ B ⟹ monom_mult c t b ∈ pmdl B"
by (intro pmdl_closed_monom_mult pmdl.span_base)
lemma pmdl_induct [consumes 1, case_names module_0 module_plus]:
assumes "p ∈ pmdl B" and "P 0"
and "⋀a p c t. a ∈ pmdl B ⟹ P a ⟹ p ∈ B ⟹ c ≠ 0 ⟹ P (a + monom_mult c t p)"
shows "P p"
using assms(1)
proof (induct p rule: pmdl.span_induct')
case base
from assms(2) show ?case .
next
case (step a q b)
from this(1) this(2) show ?case
proof (induct q arbitrary: a rule: poly_mapping_except_induct)
case 1
thus ?case by simp
next
case step: (2 q0 t)
from this(4) step(5) ‹b ∈ B› have "P (a + monomial (lookup q0 t) t ⊙ b)"
unfolding mult_scalar_monomial
proof (rule assms(3))
from step(2) show "lookup q0 t ≠ 0" by (simp add: in_keys_iff)
qed
with _ have "P ((a + monomial (lookup q0 t) t ⊙ b) + except q0 {t} ⊙ b)"
proof (rule step(3))
from ‹b ∈ B› have "b ∈ pmdl B" by (rule pmdl.span_base)
hence "monomial (lookup q0 t) t ⊙ b ∈ pmdl B" by (rule pmdl.span_scale)
with step(4) show "a + monomial (lookup q0 t) t ⊙ b ∈ pmdl B" by (rule pmdl.span_add)
qed
hence "P (a + (monomial (lookup q0 t) t + except q0 {t}) ⊙ b)" by (simp add: algebra_simps)
thus ?case by (simp only: plus_except[of q0 t, symmetric])
qed
qed
lemma components_pmdl: "component_of_term ` Keys (pmdl B) = component_of_term ` Keys B"
proof
show "component_of_term ` Keys (pmdl B) ⊆ component_of_term ` Keys B"
proof
fix k
assume "k ∈ component_of_term ` Keys (pmdl B)"
then obtain v where "v ∈ Keys (pmdl B)" and "k = component_of_term v" ..
from this(1) obtain b where "b ∈ pmdl B" and "v ∈ keys b" by (rule in_KeysE)
thus "k ∈ component_of_term ` Keys B"
proof (induct b rule: pmdl_induct)
case module_0
thus ?case by simp
next
case ind: (module_plus a p c t)
from ind.prems Poly_Mapping.keys_add have "v ∈ keys a ∪ keys (monom_mult c t p)" ..
thus ?case
proof
assume "v ∈ keys a"
thus ?thesis by (rule ind.hyps(2))
next
assume "v ∈ keys (monom_mult c t p)"
from this keys_monom_mult_subset have "v ∈ (⊕) t ` keys p" ..
then obtain u where "u ∈ keys p" and "v = t ⊕ u" ..
have "k = component_of_term u" by (simp add: ‹k = component_of_term v› ‹v = t ⊕ u› term_simps)
moreover from ‹u ∈ keys p› ind.hyps(3) have "u ∈ Keys B" by (rule in_KeysI)
ultimately show ?thesis ..
qed
qed
qed
next
show "component_of_term ` Keys B ⊆ component_of_term ` Keys (pmdl B)"
by (rule image_mono, rule Keys_mono, fact pmdl.span_superset)
qed
lemma pmdl_idI:
assumes "0 ∈ B" and "⋀b1 b2. b1 ∈ B ⟹ b2 ∈ B ⟹ b1 + b2 ∈ B"
and "⋀c t b. b ∈ B ⟹ monom_mult c t b ∈ B"
shows "pmdl B = B"
proof
show "pmdl B ⊆ B"
proof
fix p
assume "p ∈ pmdl B"
thus "p ∈ B"
proof (induct p rule: pmdl_induct)
case module_0
show ?case by (fact assms(1))
next
case step: (module_plus a b c t)
from step(2) show ?case
proof (rule assms(2))
from step(3) show "monom_mult c t b ∈ B" by (rule assms(3))
qed
qed
qed
qed (fact pmdl.span_superset)
definition full_pmdl :: "'k set ⇒ ('t ⇒⇩0 'b::zero) set"
where "full_pmdl K = {p. component_of_term ` keys p ⊆ K}"
definition is_full_pmdl :: "('t ⇒⇩0 'b::comm_ring_1) set ⇒ bool"
where "is_full_pmdl B ⟷ (∀p. component_of_term ` keys p ⊆ component_of_term ` Keys B ⟶ p ∈ pmdl B)"
lemma full_pmdl_iff: "p ∈ full_pmdl K ⟷ component_of_term ` keys p ⊆ K"
by (simp add: full_pmdl_def)
lemma full_pmdlI:
assumes "⋀v. v ∈ keys p ⟹ component_of_term v ∈ K"
shows "p ∈ full_pmdl K"
using assms by (auto simp add: full_pmdl_iff)
lemma full_pmdlD:
assumes "p ∈ full_pmdl K" and "v ∈ keys p"
shows "component_of_term v ∈ K"
using assms by (auto simp add: full_pmdl_iff)
lemma full_pmdl_empty: "full_pmdl {} = {0}"
by (simp add: full_pmdl_def)
lemma full_pmdl_UNIV: "full_pmdl UNIV = UNIV"
by (simp add: full_pmdl_def)
lemma zero_in_full_pmdl: "0 ∈ full_pmdl K"
by (simp add: full_pmdl_iff)
lemma full_pmdl_closed_plus:
assumes "p ∈ full_pmdl K" and "q ∈ full_pmdl K"
shows "p + q ∈ full_pmdl K"
proof (rule full_pmdlI)
fix v
assume "v ∈ keys (p + q)"
also have "... ⊆ keys p ∪ keys q" by (fact Poly_Mapping.keys_add)
finally show "component_of_term v ∈ K"
proof
assume "v ∈ keys p"
with assms(1) show ?thesis by (rule full_pmdlD)
next
assume "v ∈ keys q"
with assms(2) show ?thesis by (rule full_pmdlD)
qed
qed
lemma full_pmdl_closed_monom_mult:
assumes "p ∈ full_pmdl K"
shows "monom_mult c t p ∈ full_pmdl K"
proof (rule full_pmdlI)
fix v
assume "v ∈ keys (monom_mult c t p)"
also have "... ⊆ (⊕) t ` keys p" by (fact keys_monom_mult_subset)
finally obtain u where "u ∈ keys p" and v: "v = t ⊕ u" ..
have "component_of_term v = component_of_term u" by (simp add: v term_simps)
also from assms ‹u ∈ keys p› have "... ∈ K" by (rule full_pmdlD)
finally show "component_of_term v ∈ K" .
qed
lemma pmdl_full_pmdl: "pmdl (full_pmdl K) = full_pmdl K"
using zero_in_full_pmdl full_pmdl_closed_plus full_pmdl_closed_monom_mult by (rule pmdl_idI)
lemma components_full_pmdl_subset:
"component_of_term ` Keys ((full_pmdl K)::('t ⇒⇩0 'b::zero) set) ⊆ K" (is "?l ⊆ _")
proof
let ?M = "(full_pmdl K)::('t ⇒⇩0 'b) set"
fix k
assume "k ∈ ?l"
then obtain v where "v ∈ Keys ?M" and k: "k = component_of_term v" ..
from this(1) obtain p where "p ∈ ?M" and "v ∈ keys p" by (rule in_KeysE)
thus "k ∈ K" unfolding k by (rule full_pmdlD)
qed
lemma components_full_pmdl:
"component_of_term ` Keys ((full_pmdl K)::('t ⇒⇩0 'b::zero_neq_one) set) = K" (is "?l = _")
proof
let ?M = "(full_pmdl K)::('t ⇒⇩0 'b) set"
show "K ⊆ ?l"
proof
fix k
assume "k ∈ K"
hence "monomial 1 (term_of_pair (0, k)) ∈ ?M" by (simp add: full_pmdl_iff term_simps)
hence "keys (monomial (1::'b) (term_of_pair (0, k))) ⊆ Keys ?M" by (rule keys_subset_Keys)
hence "term_of_pair (0, k) ∈ Keys ?M" by simp
hence "component_of_term (term_of_pair (0, k)) ∈ component_of_term ` Keys ?M" by (rule imageI)
thus "k ∈ ?l" by (simp only: component_of_term_of_pair)
qed
qed (fact components_full_pmdl_subset)
lemma is_full_pmdlI:
assumes "⋀p. component_of_term ` keys p ⊆ component_of_term ` Keys B ⟹ p ∈ pmdl B"
shows "is_full_pmdl B"
unfolding is_full_pmdl_def using assms by blast
lemma is_full_pmdlD:
assumes "is_full_pmdl B" and "component_of_term ` keys p ⊆ component_of_term ` Keys B"
shows "p ∈ pmdl B"
using assms unfolding is_full_pmdl_def by blast
lemma is_full_pmdl_alt: "is_full_pmdl B ⟷ pmdl B = full_pmdl (component_of_term ` Keys B)"
proof -
have "b ∈ pmdl B ⟹ v ∈ keys b ⟹ component_of_term v ∈ component_of_term ` Keys B" for b v
by (metis components_pmdl image_eqI in_KeysI)
thus ?thesis by (auto simp add: is_full_pmdl_def full_pmdl_def)
qed
lemma is_full_pmdl_pmdl: "is_full_pmdl (pmdl B) ⟷ is_full_pmdl B"
by (simp only: is_full_pmdl_def pmdl.span_span components_pmdl)
lemma is_full_pmdl_subset:
assumes "is_full_pmdl B1" and "is_full_pmdl B2"
and "component_of_term ` Keys B1 ⊆ component_of_term ` Keys B2"
shows "pmdl B1 ⊆ pmdl B2"
proof
fix p
assume "p ∈ pmdl B1"
from assms(2) show "p ∈ pmdl B2"
proof (rule is_full_pmdlD)
have "component_of_term ` keys p ⊆ component_of_term ` Keys (pmdl B1)"
by (rule image_mono, rule keys_subset_Keys, fact)
also have "... = component_of_term ` Keys B1" by (fact components_pmdl)
finally show "component_of_term ` keys p ⊆ component_of_term ` Keys B2" using assms(3)
by (rule subset_trans)
qed
qed
lemma is_full_pmdl_eq:
assumes "is_full_pmdl B1" and "is_full_pmdl B2"
and "component_of_term ` Keys B1 = component_of_term ` Keys B2"
shows "pmdl B1 = pmdl B2"
proof
have "component_of_term ` Keys B1 ⊆ component_of_term ` Keys B2" by (simp add: assms(3))
with assms(1, 2) show "pmdl B1 ⊆ pmdl B2" by (rule is_full_pmdl_subset)
next
have "component_of_term ` Keys B2 ⊆ component_of_term ` Keys B1" by (simp add: assms(3))
with assms(2, 1) show "pmdl B2 ⊆ pmdl B1" by (rule is_full_pmdl_subset)
qed
end
definition map_scale :: "'b ⇒ ('a ⇒⇩0 'b) ⇒ ('a ⇒⇩0 'b::mult_zero)" (infixr "⋅" 71)
where "map_scale c = Poly_Mapping.map ((*) c)"
text ‹If the polynomial mapping ‹p› is interpreted as a power-product, then @{term "c ⋅ p"}
corresponds to exponentiation; if it is interpreted as a (vector-) polynomial, then @{term "c ⋅ p"}
corresponds to multiplication by scalar from the coefficient type.›
lemma lookup_map_scale [simp]: "lookup (c ⋅ p) = (λx. c * lookup p x)"
by (auto simp: map_scale_def map.rep_eq when_def)
lemma map_scale_single [simp]: "k ⋅ Poly_Mapping.single x l = Poly_Mapping.single x (k * l)"
by (simp add: map_scale_def)
lemma map_scale_zero_left [simp]: "0 ⋅ t = 0"
by (rule poly_mapping_eqI) simp
lemma map_scale_zero_right [simp]: "k ⋅ 0 = 0"
by (rule poly_mapping_eqI) simp
lemma map_scale_eq_0_iff: "c ⋅ t = 0 ⟷ ((c::_::semiring_no_zero_divisors) = 0 ∨ t = 0)"
by (metis aux lookup_map_scale mult_eq_0_iff)
lemma keys_map_scale_subset: "keys (k ⋅ t) ⊆ keys t"
by (metis in_keys_iff lookup_map_scale mult_zero_right subsetI)
lemma keys_map_scale: "keys ((k::'b::semiring_no_zero_divisors) ⋅ t) = (if k = 0 then {} else keys t)"
proof (split if_split, intro conjI impI)
assume "k = 0"
thus "keys (k ⋅ t) = {}" by simp
next
assume "k ≠ 0"
show "keys (k ⋅ t) = keys t"
proof
show "keys t ⊆ keys (k ⋅ t)" by rule (simp add: ‹k ≠ 0› flip: lookup_not_eq_zero_eq_in_keys)
qed (fact keys_map_scale_subset)
qed
lemma map_scale_one_left [simp]: "(1::'b::{mult_zero,monoid_mult}) ⋅ t = t"
by (rule poly_mapping_eqI) simp
lemma map_scale_assoc [ac_simps]: "c ⋅ d ⋅ t = (c * d) ⋅ (t::_ ⇒⇩0 _::{semigroup_mult,zero})"
by (rule poly_mapping_eqI) (simp add: ac_simps)
lemma map_scale_distrib_left [algebra_simps]: "(k::'b::semiring_0) ⋅ (s + t) = k ⋅ s + k ⋅ t"
by (rule poly_mapping_eqI) (simp add: lookup_add distrib_left)
lemma map_scale_distrib_right [algebra_simps]: "(k + (l::'b::semiring_0)) ⋅ t = k ⋅ t + l ⋅ t"
by (rule poly_mapping_eqI) (simp add: lookup_add distrib_right)
lemma map_scale_Suc: "(Suc k) ⋅ t = k ⋅ t + t"
by (rule poly_mapping_eqI) (simp add: lookup_add distrib_right)
lemma map_scale_uminus_left: "(- k::'b::ring) ⋅ p = - (k ⋅ p)"
by (rule poly_mapping_eqI) auto
lemma map_scale_uminus_right: "(k::'b::ring) ⋅ (- p) = - (k ⋅ p)"
by (rule poly_mapping_eqI) auto
lemma map_scale_uminus_uminus [simp]: "(- k::'b::ring) ⋅ (- p) = k ⋅ p"
by (simp add: map_scale_uminus_left map_scale_uminus_right)
lemma map_scale_minus_distrib_left [algebra_simps]:
"(k::'b::comm_semiring_1_cancel) ⋅ (p - q) = k ⋅ p - k ⋅ q"
by (rule poly_mapping_eqI) (auto simp add: lookup_minus right_diff_distrib')
lemma map_scale_minus_distrib_right [algebra_simps]:
"(k - (l::'b::comm_semiring_1_cancel)) ⋅ f = k ⋅ f - l ⋅ f"
by (rule poly_mapping_eqI) (auto simp add: lookup_minus left_diff_distrib')
lemma map_scale_sum_distrib_left: "(k::'b::semiring_0) ⋅ (sum f A) = (∑a∈A. k ⋅ f a)"
by (induct A rule: infinite_finite_induct) (simp_all add: map_scale_distrib_left)
lemma map_scale_sum_distrib_right: "(sum (f::_ ⇒ 'b::semiring_0) A) ⋅ p = (∑a∈A. f a ⋅ p)"
by (induct A rule: infinite_finite_induct) (simp_all add: map_scale_distrib_right)
lemma deg_pm_map_scale: "deg_pm (k ⋅ t) = (k::'b::semiring_0) * deg_pm t"
proof -
from keys_map_scale_subset finite_keys have "deg_pm (k ⋅ t) = sum (lookup (k ⋅ t)) (keys t)"
by (rule deg_pm_superset)
also have "… = k * sum (lookup t) (keys t)" by (simp add: sum_distrib_left)
also from subset_refl finite_keys have "sum (lookup t) (keys t) = deg_pm t"
by (rule deg_pm_superset[symmetric])
finally show ?thesis .
qed