Theory Polynomials.MPoly_PM
section ‹Multivariate Polynomials with Power-Products Represented by Polynomial Mappings›
theory MPoly_PM
imports Quasi_PM_Power_Products
begin
text ‹Many notions introduced in this theory for type @{typ "('x ⇒⇩0 'a) ⇒⇩0 'b"} closely resemble
those introduced in @{theory Polynomials.MPoly_Type} for type @{typ "'a mpoly"}.›
lemma monomial_single_power:
"(monomial c (Poly_Mapping.single x k)) ^ n = monomial (c ^ n) (Poly_Mapping.single x (k * n))"
proof -
have eq: "(∑i = 0..<n. Poly_Mapping.single x k) = Poly_Mapping.single x (k * n)"
by (induct n, simp_all add: add.commute single_add)
show ?thesis by (simp add: punit.monomial_power eq)
qed
lemma monomial_power_map_scale: "(monomial c t) ^ n = monomial (c ^ n) (n ⋅ t)"
proof -
have "(∑i = 0..<n. t) = (∑i = 0..<n. 1) ⋅ t"
by (simp only: map_scale_sum_distrib_right map_scale_one_left)
thus ?thesis by (simp add: punit.monomial_power)
qed
lemma times_canc_left:
assumes "h * p = h * q" and "h ≠ (0::('x::linorder ⇒⇩0 nat) ⇒⇩0 'a::ring_no_zero_divisors)"
shows "p = q"
proof (rule ccontr)
assume "p ≠ q"
hence "p - q ≠ 0" by simp
with assms(2) have "h * (p - q) ≠ 0" by simp
hence "h * p ≠ h * q" by (simp add: algebra_simps)
thus False using assms(1) ..
qed
lemma times_canc_right:
assumes "p * h = q * h" and "h ≠ (0::('x::linorder ⇒⇩0 nat) ⇒⇩0 'a::ring_no_zero_divisors)"
shows "p = q"
proof (rule ccontr)
assume "p ≠ q"
hence "p - q ≠ 0" by simp
hence "(p - q) * h ≠ 0" using assms(2) by simp
hence "p * h ≠ q * h" by (simp add: algebra_simps)
thus False using assms(1) ..
qed
subsection ‹Degree›
lemma plus_minus_assoc_pm_nat_1: "s + t - u = (s - (u - t)) + (t - (u::_ ⇒⇩0 nat))"
by (rule poly_mapping_eqI, simp add: lookup_add lookup_minus)
lemma plus_minus_assoc_pm_nat_2:
"s + (t - u) = (s + (except (u - t) (- keys s))) + t - (u::_ ⇒⇩0 nat)"
proof (rule poly_mapping_eqI)
fix x
show "lookup (s + (t - u)) x = lookup (s + except (u - t) (- keys s) + t - u) x"
proof (cases "x ∈ keys s")
case True
thus ?thesis
by (simp add: plus_minus_assoc_pm_nat_1 lookup_add lookup_minus lookup_except)
next
case False
hence "lookup s x = 0" by (simp add: in_keys_iff)
with False show ?thesis
by (simp add: lookup_add lookup_minus lookup_except)
qed
qed
lemma deg_pm_sum: "deg_pm (sum t A) = (∑a∈A. deg_pm (t a))"
by (induct A rule: infinite_finite_induct) (auto simp: deg_pm_plus)
lemma deg_pm_mono: "s adds t ⟹ deg_pm s ≤ deg_pm (t::_ ⇒⇩0 _::add_linorder_min)"
by (metis addsE deg_pm_plus le_iff_add)
lemma adds_deg_pm_antisym: "s adds t ⟹ deg_pm t ≤ deg_pm (s::_ ⇒⇩0 _::add_linorder_min) ⟹ s = t"
by (metis (no_types, lifting) add.right_neutral add.right_neutral add_left_cancel addsE
deg_pm_eq_0_iff deg_pm_mono deg_pm_plus dual_order.antisym)
lemma deg_pm_minus:
assumes "s adds (t::_ ⇒⇩0 _::comm_monoid_add)"
shows "deg_pm (t - s) = deg_pm t - deg_pm s"
proof -
from assms have "(t - s) + s = t" by (rule adds_minus)
hence "deg_pm t = deg_pm ((t - s) + s)" by simp
also have "… = deg_pm (t - s) + deg_pm s" by (simp only: deg_pm_plus)
finally show ?thesis by simp
qed
lemma adds_group [simp]: "s adds (t::'a ⇒⇩0 'b::ab_group_add)"
proof (rule addsI)
show "t = s + (t - s)" by simp
qed
lemmas deg_pm_minus_group = deg_pm_minus[OF adds_group]
lemma deg_pm_minus_le: "deg_pm (t - s) ≤ deg_pm (t::_ ⇒⇩0 nat)"
proof -
have "keys (t - s) ⊆ keys t" by (rule, simp add: lookup_minus in_keys_iff)
hence "deg_pm (t - s) = (∑x∈keys t. lookup (t - s) x)" using finite_keys by (rule deg_pm_superset)
also have "… ≤ (∑x∈keys t. lookup t x)" by (rule sum_mono) (simp add: lookup_minus)
also have "… = deg_pm t" by (rule sym, rule deg_pm_superset, fact subset_refl, fact finite_keys)
finally show ?thesis .
qed
lemma minus_id_iff: "t - s = t ⟷ keys t ∩ keys (s::_ ⇒⇩0 nat) = {}"
proof
assume "t - s = t"
{
fix x
assume "x ∈ keys t" and "x ∈ keys s"
hence "0 < lookup t x" and "0 < lookup s x" by (simp_all add: in_keys_iff)
hence "lookup (t - s) x ≠ lookup t x" by (simp add: lookup_minus)
with ‹t - s = t› have False by simp
}
thus "keys t ∩ keys s = {}" by blast
next
assume *: "keys t ∩ keys s = {}"
show "t - s = t"
proof (rule poly_mapping_eqI)
fix x
have "lookup t x - lookup s x = lookup t x"
proof (cases "x ∈ keys t")
case True
with * have "x ∉ keys s" by blast
thus ?thesis by (simp add: in_keys_iff)
next
case False
thus ?thesis by (simp add: in_keys_iff)
qed
thus "lookup (t - s) x = lookup t x" by (simp only: lookup_minus)
qed
qed
lemma deg_pm_minus_id_iff: "deg_pm (t - s) = deg_pm t ⟷ keys t ∩ keys (s::_ ⇒⇩0 nat) = {}"
proof
assume eq: "deg_pm (t - s) = deg_pm t"
{
fix x
assume "x ∈ keys t" and "x ∈ keys s"
hence "0 < lookup t x" and "0 < lookup s x" by (simp_all add: in_keys_iff)
hence *: "lookup (t - s) x < lookup t x" by (simp add: lookup_minus)
have "keys (t - s) ⊆ keys t" by (rule, simp add: lookup_minus in_keys_iff)
hence "deg_pm (t - s) = (∑x∈keys t. lookup (t - s) x)" using finite_keys by (rule deg_pm_superset)
also from finite_keys have "… < (∑x∈keys t. lookup t x)"
proof (rule sum_strict_mono_ex1)
show "∀x∈keys t. lookup (t - s) x ≤ lookup t x" by (simp add: lookup_minus)
next
from ‹x ∈ keys t› * show "∃x∈keys t. lookup (t - s) x < lookup t x" ..
qed
also have "… = deg_pm t" by (rule sym, rule deg_pm_superset, fact subset_refl, fact finite_keys)
finally have False by (simp add: eq)
}
thus "keys t ∩ keys s = {}" by blast
next
assume "keys t ∩ keys s = {}"
hence "t - s = t" by (simp only: minus_id_iff)
thus "deg_pm (t - s) = deg_pm t" by (simp only:)
qed
definition poly_deg :: "(('x ⇒⇩0 'a::add_linorder) ⇒⇩0 'b::zero) ⇒ 'a" where
"poly_deg p = (if keys p = {} then 0 else Max (deg_pm ` keys p))"
definition maxdeg :: "(('x ⇒⇩0 'a::add_linorder) ⇒⇩0 'b::zero) set ⇒ 'a" where
"maxdeg A = Max (poly_deg ` A)"
definition mindeg :: "(('x ⇒⇩0 'a::add_linorder) ⇒⇩0 'b::zero) set ⇒ 'a" where
"mindeg A = Min (poly_deg ` A)"
lemma poly_deg_monomial: "poly_deg (monomial c t) = (if c = 0 then 0 else deg_pm t)"
by (simp add: poly_deg_def)
lemma poly_deg_monomial_zero [simp]: "poly_deg (monomial c 0) = 0"
by (simp add: poly_deg_monomial)
lemma poly_deg_zero [simp]: "poly_deg 0 = 0"
by (simp only: single_zero[of 0, symmetric] poly_deg_monomial_zero)
lemma poly_deg_one [simp]: "poly_deg 1 = 0"
by (simp only: single_one[symmetric] poly_deg_monomial_zero)
lemma poly_degE:
assumes "p ≠ 0"
obtains t where "t ∈ keys p" and "poly_deg p = deg_pm t"
proof -
from assms have "poly_deg p = Max (deg_pm ` keys p)" by (simp add: poly_deg_def)
also have "… ∈ deg_pm ` keys p"
proof (rule Max_in)
from assms show "deg_pm ` keys p ≠ {}" by simp
qed simp
finally obtain t where "t ∈ keys p" and "poly_deg p = deg_pm t" ..
thus ?thesis ..
qed
lemma poly_deg_max_keys: "t ∈ keys p ⟹ deg_pm t ≤ poly_deg p"
using finite_keys by (auto simp: poly_deg_def)
lemma poly_deg_leI: "(⋀t. t ∈ keys p ⟹ deg_pm t ≤ (d::'a::add_linorder_min)) ⟹ poly_deg p ≤ d"
using finite_keys by (auto simp: poly_deg_def)
lemma poly_deg_lessI:
"p ≠ 0 ⟹ (⋀t. t ∈ keys p ⟹ deg_pm t < (d::'a::add_linorder_min)) ⟹ poly_deg p < d"
using finite_keys by (auto simp: poly_deg_def)
lemma poly_deg_zero_imp_monomial:
assumes "poly_deg p = (0::'a::add_linorder_min)"
shows "monomial (lookup p 0) 0 = p"
proof (rule keys_subset_singleton_imp_monomial, rule)
fix t
assume "t ∈ keys p"
have "t = 0"
proof (rule ccontr)
assume "t ≠ 0"
hence "deg_pm t ≠ 0" by simp
hence "0 < deg_pm t" using not_gr_zero by blast
also from ‹t ∈ keys p› have "... ≤ poly_deg p" by (rule poly_deg_max_keys)
finally have "poly_deg p ≠ 0" by simp
from this assms show False ..
qed
thus "t ∈ {0}" by simp
qed
lemma poly_deg_plus_le:
"poly_deg (p + q) ≤ max (poly_deg p) (poly_deg (q::(_ ⇒⇩0 'a::add_linorder_min) ⇒⇩0 _))"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys (p + q)"
also have "... ⊆ keys p ∪ keys q" by (fact Poly_Mapping.keys_add)
finally show "deg_pm t ≤ max (poly_deg p) (poly_deg q)"
proof
assume "t ∈ keys p"
hence "deg_pm t ≤ poly_deg p" by (rule poly_deg_max_keys)
thus ?thesis by (simp add: le_max_iff_disj)
next
assume "t ∈ keys q"
hence "deg_pm t ≤ poly_deg q" by (rule poly_deg_max_keys)
thus ?thesis by (simp add: le_max_iff_disj)
qed
qed
lemma poly_deg_uminus [simp]: "poly_deg (-p) = poly_deg p"
by (simp add: poly_deg_def keys_uminus)
lemma poly_deg_minus_le:
"poly_deg (p - q) ≤ max (poly_deg p) (poly_deg (q::(_ ⇒⇩0 'a::add_linorder_min) ⇒⇩0 _))"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys (p - q)"
also have "... ⊆ keys p ∪ keys q" by (fact keys_minus)
finally show "deg_pm t ≤ max (poly_deg p) (poly_deg q)"
proof
assume "t ∈ keys p"
hence "deg_pm t ≤ poly_deg p" by (rule poly_deg_max_keys)
thus ?thesis by (simp add: le_max_iff_disj)
next
assume "t ∈ keys q"
hence "deg_pm t ≤ poly_deg q" by (rule poly_deg_max_keys)
thus ?thesis by (simp add: le_max_iff_disj)
qed
qed
lemma poly_deg_times_le:
"poly_deg (p * q) ≤ poly_deg p + poly_deg (q::(_ ⇒⇩0 'a::add_linorder_min) ⇒⇩0 _)"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys (p * q)"
then obtain u v where "u ∈ keys p" and "v ∈ keys q" and "t = u + v" by (rule in_keys_timesE)
from ‹u ∈ keys p› have "deg_pm u ≤ poly_deg p" by (rule poly_deg_max_keys)
moreover from ‹v ∈ keys q› have "deg_pm v ≤ poly_deg q" by (rule poly_deg_max_keys)
ultimately show "deg_pm t ≤ poly_deg p + poly_deg q" by (simp add: ‹t = u + v› deg_pm_plus add_mono)
qed
lemma poly_deg_times:
assumes "p ≠ 0" and "q ≠ (0::('x::linorder ⇒⇩0 'a::add_linorder_min) ⇒⇩0 'b::semiring_no_zero_divisors)"
shows "poly_deg (p * q) = poly_deg p + poly_deg q"
using poly_deg_times_le
proof (rule antisym)
let ?A = "λf. {u. deg_pm u < poly_deg f}"
define p1 where "p1 = except p (?A p)"
define p2 where "p2 = except p (- ?A p)"
define q1 where "q1 = except q (?A q)"
define q2 where "q2 = except q (- ?A q)"
have deg_p1: "deg_pm t = poly_deg p" if "t ∈ keys p1" for t
proof -
from that have "t ∈ keys p" and "poly_deg p ≤ deg_pm t"
by (simp_all add: p1_def keys_except not_less)
from this(1) have "deg_pm t ≤ poly_deg p" by (rule poly_deg_max_keys)
thus ?thesis using ‹poly_deg p ≤ deg_pm t› by (rule antisym)
qed
have deg_p2: "t ∈ keys p2 ⟹ deg_pm t < poly_deg p" for t by (simp add: p2_def keys_except)
have deg_q1: "deg_pm t = poly_deg q" if "t ∈ keys q1" for t
proof -
from that have "t ∈ keys q" and "poly_deg q ≤ deg_pm t"
by (simp_all add: q1_def keys_except not_less)
from this(1) have "deg_pm t ≤ poly_deg q" by (rule poly_deg_max_keys)
thus ?thesis using ‹poly_deg q ≤ deg_pm t› by (rule antisym)
qed
have deg_q2: "t ∈ keys q2 ⟹ deg_pm t < poly_deg q" for t by (simp add: q2_def keys_except)
have p: "p = p1 + p2" unfolding p1_def p2_def by (fact except_decomp)
have "p1 ≠ 0"
proof -
from assms(1) obtain t where "t ∈ keys p" and "poly_deg p = deg_pm t" by (rule poly_degE)
hence "t ∈ keys p1" by (simp add: p1_def keys_except)
thus ?thesis by auto
qed
have q: "q = q1 + q2" unfolding q1_def q2_def by (fact except_decomp)
have "q1 ≠ 0"
proof -
from assms(2) obtain t where "t ∈ keys q" and "poly_deg q = deg_pm t" by (rule poly_degE)
hence "t ∈ keys q1" by (simp add: q1_def keys_except)
thus ?thesis by auto
qed
with ‹p1 ≠ 0› have "p1 * q1 ≠ 0" by simp
hence "keys (p1 * q1) ≠ {}" by simp
then obtain u where "u ∈ keys (p1 * q1)" by blast
then obtain s t where "s ∈ keys p1" and "t ∈ keys q1" and u: "u = s + t" by (rule in_keys_timesE)
from ‹s ∈ keys p1› have "deg_pm s = poly_deg p" by (rule deg_p1)
moreover from ‹t ∈ keys q1› have "deg_pm t = poly_deg q" by (rule deg_q1)
ultimately have eq: "poly_deg p + poly_deg q = deg_pm u" by (simp only: u deg_pm_plus)
also have "… ≤ poly_deg (p * q)"
proof (rule poly_deg_max_keys)
have "u ∉ keys (p1 * q2 + p2 * q)"
proof
assume "u ∈ keys (p1 * q2 + p2 * q)"
also have "… ⊆ keys (p1 * q2) ∪ keys (p2 * q)" by (rule Poly_Mapping.keys_add)
finally have "deg_pm u < poly_deg p + poly_deg q"
proof
assume "u ∈ keys (p1 * q2)"
then obtain s' t' where "s' ∈ keys p1" and "t' ∈ keys q2" and u: "u = s' + t'"
by (rule in_keys_timesE)
from ‹s' ∈ keys p1› have "deg_pm s' = poly_deg p" by (rule deg_p1)
moreover from ‹t' ∈ keys q2› have "deg_pm t' < poly_deg q" by (rule deg_q2)
ultimately show ?thesis by (simp add: u deg_pm_plus)
next
assume "u ∈ keys (p2 * q)"
then obtain s' t' where "s' ∈ keys p2" and "t' ∈ keys q" and u: "u = s' + t'"
by (rule in_keys_timesE)
from ‹s' ∈ keys p2› have "deg_pm s' < poly_deg p" by (rule deg_p2)
moreover from ‹t' ∈ keys q› have "deg_pm t' ≤ poly_deg q" by (rule poly_deg_max_keys)
ultimately show ?thesis by (simp add: u deg_pm_plus add_less_le_mono)
qed
thus False by (simp only: eq)
qed
with ‹u ∈ keys (p1 * q1)› have "u ∈ keys (p1 * q1 + (p1 * q2 + p2 * q))" by (rule in_keys_plusI1)
thus "u ∈ keys (p * q)" by (simp only: p q algebra_simps)
qed
finally show "poly_deg p + poly_deg q ≤ poly_deg (p * q)" .
qed
corollary poly_deg_monom_mult_le:
"poly_deg (punit.monom_mult c (t::_ ⇒⇩0 'a::add_linorder_min) p) ≤ deg_pm t + poly_deg p"
proof -
have "poly_deg (punit.monom_mult c t p) ≤ poly_deg (monomial c t) + poly_deg p"
by (simp only: times_monomial_left[symmetric] poly_deg_times_le)
also have "... ≤ deg_pm t + poly_deg p" by (simp add: poly_deg_monomial)
finally show ?thesis .
qed
lemma poly_deg_monom_mult:
assumes "c ≠ 0" and "p ≠ (0::(_ ⇒⇩0 'a::add_linorder_min) ⇒⇩0 'b::semiring_no_zero_divisors)"
shows "poly_deg (punit.monom_mult c t p) = deg_pm t + poly_deg p"
proof (rule order.antisym, fact poly_deg_monom_mult_le)
from assms(2) obtain s where "s ∈ keys p" and "poly_deg p = deg_pm s" by (rule poly_degE)
have "deg_pm t + poly_deg p = deg_pm (t + s)" by (simp add: ‹poly_deg p = deg_pm s› deg_pm_plus)
also have "... ≤ poly_deg (punit.monom_mult c t p)"
proof (rule poly_deg_max_keys)
from ‹s ∈ keys p› show "t + s ∈ keys (punit.monom_mult c t p)"
unfolding punit.keys_monom_mult[OF assms(1)] by fastforce
qed
finally show "deg_pm t + poly_deg p ≤ poly_deg (punit.monom_mult c t p)" .
qed
lemma poly_deg_map_scale:
"poly_deg (c ⋅ p) = (if c = (0::_::semiring_no_zero_divisors) then 0 else poly_deg p)"
by (simp add: poly_deg_def keys_map_scale)
lemma poly_deg_sum_le: "((poly_deg (sum f A))::'a::add_linorder_min) ≤ Max (poly_deg ` f ` A)"
proof (cases "finite A")
case True
thus ?thesis
proof (induct A)
case empty
show ?case by simp
next
case (insert a A)
show ?case
proof (cases "A = {}")
case True
thus ?thesis by simp
next
case False
have "poly_deg (sum f (insert a A)) ≤ max (poly_deg (f a)) (poly_deg (sum f A))"
by (simp only: comm_monoid_add_class.sum.insert[OF insert(1) insert(2)] poly_deg_plus_le)
also have "... ≤ max (poly_deg (f a)) (Max (poly_deg ` f ` A))"
using insert(3) max.mono by blast
also have "... = (Max (poly_deg ` f ` (insert a A)))" using False by (simp add: insert(1))
finally show ?thesis .
qed
qed
next
case False
thus ?thesis by simp
qed
lemma poly_deg_prod_le: "((poly_deg (prod f A))::'a::add_linorder_min) ≤ (∑a∈A. poly_deg (f a))"
proof (cases "finite A")
case True
thus ?thesis
proof (induct A)
case empty
show ?case by simp
next
case (insert a A)
have "poly_deg (prod f (insert a A)) ≤ (poly_deg (f a)) + (poly_deg (prod f A))"
by (simp only: comm_monoid_mult_class.prod.insert[OF insert(1) insert(2)] poly_deg_times_le)
also have "... ≤ (poly_deg (f a)) + (∑a∈A. poly_deg (f a))"
using insert(3) add_le_cancel_left by blast
also have "... = (∑a∈insert a A. poly_deg (f a))" by (simp add: insert(1) insert(2))
finally show ?case .
qed
next
case False
thus ?thesis by simp
qed
lemma maxdeg_max:
assumes "finite A" and "p ∈ A"
shows "poly_deg p ≤ maxdeg A"
unfolding maxdeg_def using assms by auto
lemma mindeg_min:
assumes "finite A" and "p ∈ A"
shows "mindeg A ≤ poly_deg p"
unfolding mindeg_def using assms by auto
subsection ‹Indeterminates›
definition indets :: "(('x ⇒⇩0 nat) ⇒⇩0 'b::zero) ⇒ 'x set"
where "indets p = ⋃ (keys ` keys p)"
definition PPs :: "'x set ⇒ ('x ⇒⇩0 nat) set" (‹.[(_)]›)
where "PPs X = {t. keys t ⊆ X}"
definition Polys :: "'x set ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'b::zero) set" (‹P[(_)]›)
where "Polys X = {p. keys p ⊆ .[X]}"
subsubsection ‹@{const indets}›
lemma in_indetsI:
assumes "x ∈ keys t" and "t ∈ keys p"
shows "x ∈ indets p"
using assms by (auto simp add: indets_def)
lemma in_indetsE:
assumes "x ∈ indets p"
obtains t where "t ∈ keys p" and "x ∈ keys t"
using assms by (auto simp add: indets_def)
lemma keys_subset_indets: "t ∈ keys p ⟹ keys t ⊆ indets p"
by (auto dest: in_indetsI)
lemma indets_empty_imp_monomial:
assumes "indets p = {}"
shows "monomial (lookup p 0) 0 = p"
proof (rule keys_subset_singleton_imp_monomial, rule)
fix t
assume "t ∈ keys p"
have "t = 0"
proof (rule ccontr)
assume "t ≠ 0"
hence "keys t ≠ {}" by simp
then obtain x where "x ∈ keys t" by blast
from this ‹t ∈ keys p› have "x ∈ indets p" by (rule in_indetsI)
with assms show False by simp
qed
thus "t ∈ {0}" by simp
qed
lemma finite_indets: "finite (indets p)"
by (simp only: indets_def, rule finite_UN_I, (rule finite_keys)+)
lemma indets_zero [simp]: "indets 0 = {}"
by (simp add: indets_def)
lemma indets_one [simp]: "indets 1 = {}"
by (simp add: indets_def)
lemma indets_monomial_single_subset: "indets (monomial c (Poly_Mapping.single v k)) ⊆ {v}"
proof
fix x assume "x ∈ indets (monomial c (Poly_Mapping.single v k))"
then have "x = v" unfolding indets_def
by (metis UN_E lookup_eq_zero_in_keys_contradict lookup_single_not_eq)
thus "x ∈ {v}" by simp
qed
lemma indets_monomial_single:
assumes "c ≠ 0" and "k ≠ 0"
shows "indets (monomial c (Poly_Mapping.single v k)) = {v}"
proof (rule, fact indets_monomial_single_subset, simp)
from assms show "v ∈ indets (monomial c (monomial k v))" by (simp add: indets_def)
qed
lemma indets_monomial:
assumes "c ≠ 0"
shows "indets (monomial c t) = keys t"
proof (rule antisym; rule subsetI)
fix x
assume "x ∈ indets (monomial c t)"
then have "lookup t x ≠ 0" unfolding indets_def
by (metis UN_E lookup_eq_zero_in_keys_contradict lookup_single_not_eq)
thus "x ∈ keys t" by (meson lookup_not_eq_zero_eq_in_keys)
next
fix x
assume "x ∈ keys t"
then have "lookup t x ≠ 0" by (meson lookup_not_eq_zero_eq_in_keys)
thus "x ∈ indets (monomial c t)" unfolding indets_def using assms
by (metis UN_iff lookup_not_eq_zero_eq_in_keys lookup_single_eq)
qed
lemma indets_monomial_subset: "indets (monomial c t) ⊆ keys t"
by (cases "c = 0", simp_all add: indets_def)
lemma indets_monomial_zero [simp]: "indets (monomial c 0) = {}"
by (simp add: indets_def)
lemma indets_plus_subset: "indets (p + q) ⊆ indets p ∪ indets q"
proof
fix x
assume "x ∈ indets (p + q)"
then obtain t where "x ∈ keys t" and "t ∈ keys (p + q)" by (metis UN_E indets_def)
hence "t ∈ keys p ∪ keys q" by (metis Poly_Mapping.keys_add subsetCE)
thus "x ∈ indets p ∪ indets q" using indets_def ‹x ∈ keys t› by fastforce
qed
lemma indets_uminus [simp]: "indets (-p) = indets p"
by (simp add: indets_def keys_uminus)
lemma indets_minus_subset: "indets (p - q) ⊆ indets p ∪ indets q"
proof
fix x
assume "x ∈ indets (p - q)"
then obtain t where "x ∈ keys t" and "t ∈ keys (p - q)" by (metis UN_E indets_def)
hence "t ∈ keys p ∪ keys q" by (metis keys_minus subsetCE)
thus "x ∈ indets p ∪ indets q" using indets_def ‹x ∈ keys t› by fastforce
qed
lemma indets_times_subset: "indets (p * q) ⊆ indets p ∪ indets (q::(_ ⇒⇩0 _::cancel_comm_monoid_add) ⇒⇩0 _)"
proof
fix x
assume "x ∈ indets (p * q)"
then obtain t where "t ∈ keys (p * q)" and "x ∈ keys t" unfolding indets_def by blast
from this(1) obtain u v where "u ∈ keys p" "v ∈ keys q" and "t = u + v" by (rule in_keys_timesE)
hence "x ∈ keys u ∪ keys v" by (metis ‹x ∈ keys t› Poly_Mapping.keys_add subsetCE)
thus "x ∈ indets p ∪ indets q" unfolding indets_def using ‹u ∈ keys p› ‹v ∈ keys q› by blast
qed
corollary indets_monom_mult_subset: "indets (punit.monom_mult c t p) ⊆ keys t ∪ indets p"
proof -
have "indets (punit.monom_mult c t p) ⊆ indets (monomial c t) ∪ indets p"
by (simp only: times_monomial_left[symmetric] indets_times_subset)
also have "... ⊆ keys t ∪ indets p" using indets_monomial_subset[of t c] by blast
finally show ?thesis .
qed
lemma indets_monom_mult:
assumes "c ≠ 0" and "p ≠ (0::('x ⇒⇩0 nat) ⇒⇩0 'b::semiring_no_zero_divisors)"
shows "indets (punit.monom_mult c t p) = keys t ∪ indets p"
proof (rule, fact indets_monom_mult_subset, rule)
fix x
assume "x ∈ keys t ∪ indets p"
thus "x ∈ indets (punit.monom_mult c t p)"
proof
assume "x ∈ keys t"
from assms(2) have "keys p ≠ {}" by simp
then obtain s where "s ∈ keys p" by blast
hence "t + s ∈ (+) t ` keys p" by fastforce
also from assms(1) have "... = keys (punit.monom_mult c t p)" by (simp add: punit.keys_monom_mult)
finally have "t + s ∈ keys (punit.monom_mult c t p)" .
show ?thesis
proof (rule in_indetsI)
from ‹x ∈ keys t› show "x ∈ keys (t + s)" by (simp add: keys_plus_ninv_comm_monoid_add)
qed fact
next
assume "x ∈ indets p"
then obtain s where "s ∈ keys p" and "x ∈ keys s" by (rule in_indetsE)
from this(1) have "t + s ∈ (+) t ` keys p" by fastforce
also from assms(1) have "... = keys (punit.monom_mult c t p)" by (simp add: punit.keys_monom_mult)
finally have "t + s ∈ keys (punit.monom_mult c t p)" .
show ?thesis
proof (rule in_indetsI)
from ‹x ∈ keys s› show "x ∈ keys (t + s)" by (simp add: keys_plus_ninv_comm_monoid_add)
qed fact
qed
qed
lemma indets_sum_subset: "indets (sum f A) ⊆ (⋃a∈A. indets (f a))"
proof (cases "finite A")
case True
thus ?thesis
proof (induct A)
case empty
show ?case by simp
next
case (insert a A)
have "indets (sum f (insert a A)) ⊆ indets (f a) ∪ indets (sum f A)"
by (simp only: comm_monoid_add_class.sum.insert[OF insert(1) insert(2)] indets_plus_subset)
also have "... ⊆ indets (f a) ∪ (⋃a∈A. indets (f a))" using insert(3) by blast
also have "... = (⋃a∈insert a A. indets (f a))" by simp
finally show ?case .
qed
next
case False
thus ?thesis by simp
qed
lemma indets_prod_subset:
"indets (prod (f::_ ⇒ ((_ ⇒⇩0 _::cancel_comm_monoid_add) ⇒⇩0 _)) A) ⊆ (⋃a∈A. indets (f a))"
proof (cases "finite A")
case True
thus ?thesis
proof (induct A)
case empty
show ?case by simp
next
case (insert a A)
have "indets (prod f (insert a A)) ⊆ indets (f a) ∪ indets (prod f A)"
by (simp only: comm_monoid_mult_class.prod.insert[OF insert(1) insert(2)] indets_times_subset)
also have "... ⊆ indets (f a) ∪ (⋃a∈A. indets (f a))" using insert(3) by blast
also have "... = (⋃a∈insert a A. indets (f a))" by simp
finally show ?case .
qed
next
case False
thus ?thesis by simp
qed
lemma indets_power_subset: "indets (p ^ n) ⊆ indets (p::('x ⇒⇩0 nat) ⇒⇩0 'b::comm_semiring_1)"
proof -
have "p ^ n = (∏i=0..<n. p)" by simp
also have "indets ... ⊆ (⋃i∈{0..<n}. indets p)" by (fact indets_prod_subset)
also have "... ⊆ indets p" by simp
finally show ?thesis .
qed
lemma indets_empty_iff_poly_deg_zero: "indets p = {} ⟷ poly_deg p = 0"
proof
assume "indets p = {}"
hence "monomial (lookup p 0) 0 = p" by (rule indets_empty_imp_monomial)
moreover have "poly_deg (monomial (lookup p 0) 0) = 0" by simp
ultimately show "poly_deg p = 0" by metis
next
assume "poly_deg p = 0"
hence "monomial (lookup p 0) 0 = p" by (rule poly_deg_zero_imp_monomial)
moreover have "indets (monomial (lookup p 0) 0) = {}" by simp
ultimately show "indets p = {}" by metis
qed
subsubsection ‹@{const PPs}›
lemma PPsI: "keys t ⊆ X ⟹ t ∈ .[X]"
by (simp add: PPs_def)
lemma PPsD: "t ∈ .[X] ⟹ keys t ⊆ X"
by (simp add: PPs_def)
lemma PPs_empty [simp]: ".[{}] = {0}"
by (simp add: PPs_def)
lemma PPs_UNIV [simp]: ".[UNIV] = UNIV"
by (simp add: PPs_def)
lemma PPs_singleton: ".[{x}] = range (Poly_Mapping.single x)"
proof (rule set_eqI)
fix t
show "t ∈ .[{x}] ⟷ t ∈ range (Poly_Mapping.single x)"
proof
assume "t ∈ .[{x}]"
hence "keys t ⊆ {x}" by (rule PPsD)
hence "Poly_Mapping.single x (lookup t x) = t" by (rule keys_subset_singleton_imp_monomial)
from this[symmetric] UNIV_I show "t ∈ range (Poly_Mapping.single x)" ..
next
assume "t ∈ range (Poly_Mapping.single x)"
then obtain e where "t = Poly_Mapping.single x e" ..
thus "t ∈ .[{x}]" by (simp add: PPs_def)
qed
qed
lemma zero_in_PPs: "0 ∈ .[X]"
by (simp add: PPs_def)
lemma PPs_mono: "X ⊆ Y ⟹ .[X] ⊆ .[Y]"
by (auto simp: PPs_def)
lemma PPs_closed_single:
assumes "x ∈ X"
shows "Poly_Mapping.single x e ∈ .[X]"
proof (rule PPsI)
have "keys (Poly_Mapping.single x e) ⊆ {x}" by simp
also from assms have "... ⊆ X" by simp
finally show "keys (Poly_Mapping.single x e) ⊆ X" .
qed
lemma PPs_closed_plus:
assumes "s ∈ .[X]" and "t ∈ .[X]"
shows "s + t ∈ .[X]"
proof -
have "keys (s + t) ⊆ keys s ∪ keys t" by (fact Poly_Mapping.keys_add)
also from assms have "... ⊆ X" by (simp add: PPs_def)
finally show ?thesis by (rule PPsI)
qed
lemma PPs_closed_minus:
assumes "s ∈ .[X]"
shows "s - t ∈ .[X]"
proof -
have "keys (s - t) ⊆ keys s" by (metis lookup_minus lookup_not_eq_zero_eq_in_keys subsetI zero_diff)
also from assms have "... ⊆ X" by (rule PPsD)
finally show ?thesis by (rule PPsI)
qed
lemma PPs_closed_adds:
assumes "s ∈ .[X]" and "t adds s"
shows "t ∈ .[X]"
proof -
from assms(2) have "s - (s - t) = t" by (metis add_minus_2 adds_minus)
moreover from assms(1) have "s - (s - t) ∈ .[X]" by (rule PPs_closed_minus)
ultimately show ?thesis by simp
qed
lemma PPs_closed_gcs:
assumes "s ∈ .[X]"
shows "gcs s t ∈ .[X]"
using assms gcs_adds by (rule PPs_closed_adds)
lemma PPs_closed_lcs:
assumes "s ∈ .[X]" and "t ∈ .[X]"
shows "lcs s t ∈ .[X]"
proof -
from assms have "s + t ∈ .[X]" by (rule PPs_closed_plus)
hence "(s + t) - gcs s t ∈ .[X]" by (rule PPs_closed_minus)
thus ?thesis by (simp add: gcs_plus_lcs[of s t, symmetric])
qed
lemma PPs_closed_except': "t ∈ .[X] ⟹ except t Y ∈ .[X - Y]"
by (auto simp: keys_except PPs_def)
lemma PPs_closed_except: "t ∈ .[X] ⟹ except t Y ∈ .[X]"
by (auto simp: keys_except PPs_def)
lemma PPs_UnI:
assumes "tx ∈ .[X]" and "ty ∈ .[Y]" and "t = tx + ty"
shows "t ∈ .[X ∪ Y]"
proof -
from assms(1) have "tx ∈ .[X ∪ Y]" by rule (simp add: PPs_mono)
moreover from assms(2) have "ty ∈ .[X ∪ Y]" by rule (simp add: PPs_mono)
ultimately show ?thesis unfolding assms(3) by (rule PPs_closed_plus)
qed
lemma PPs_UnE:
assumes "t ∈ .[X ∪ Y]"
obtains tx ty where "tx ∈ .[X]" and "ty ∈ .[Y]" and "t = tx + ty"
proof -
from assms have "keys t ⊆ X ∪ Y" by (rule PPsD)
define tx where "tx = except t (- X)"
have "keys tx ⊆ X" by (simp add: tx_def keys_except)
hence "tx ∈ .[X]" by (simp add: PPs_def)
have "tx adds t" by (simp add: tx_def adds_poly_mappingI le_fun_def lookup_except)
from adds_minus[OF this] have "t = tx + (t - tx)" by (simp only: ac_simps)
have "t - tx ∈ .[Y]"
proof (rule PPsI, rule)
fix x
assume "x ∈ keys (t - tx)"
also have "... ⊆ keys t ∪ keys tx" by (rule keys_minus)
also from ‹keys t ⊆ X ∪ Y› ‹keys tx ⊆ X› have "... ⊆ X ∪ Y" by blast
finally show "x ∈ Y"
proof
assume "x ∈ X"
hence "x ∉ keys (t - tx)" by (simp add: tx_def lookup_except lookup_minus in_keys_iff)
thus ?thesis using ‹x ∈ keys (t - tx)› ..
qed
qed
with ‹tx ∈ .[X]› show ?thesis using ‹t = tx + (t - tx)› ..
qed
lemma PPs_Un: ".[X ∪ Y] = (⋃t∈.[X]. (+) t ` .[Y])" (is "?A = ?B")
proof (rule set_eqI)
fix t
show "t ∈ ?A ⟷ t ∈ ?B"
proof
assume "t ∈ ?A"
then obtain tx ty where "tx ∈ .[X]" and "ty ∈ .[Y]" and "t = tx + ty" by (rule PPs_UnE)
from this(2) have "t ∈ (+) tx ` .[Y]" unfolding ‹t = tx + ty› by (rule imageI)
with ‹tx ∈ .[X]› show "t ∈ ?B" ..
next
assume "t ∈ ?B"
then obtain tx where "tx ∈ .[X]" and "t ∈ (+) tx ` .[Y]" ..
from this(2) obtain ty where "ty ∈ .[Y]" and "t = tx + ty" ..
with ‹tx ∈ .[X]› show "t ∈ ?A" by (rule PPs_UnI)
qed
qed
corollary PPs_insert: ".[insert x X] = (⋃e. (+) (Poly_Mapping.single x e) ` .[X])"
proof -
have ".[insert x X] = .[{x} ∪ X]" by simp
also have "... = (⋃t∈.[{x}]. (+) t ` .[X])" by (fact PPs_Un)
also have "... = (⋃e. (+) (Poly_Mapping.single x e) ` .[X])" by (simp add: PPs_singleton)
finally show ?thesis .
qed
corollary PPs_insertI:
assumes "tx ∈ .[X]" and "t = Poly_Mapping.single x e + tx"
shows "t ∈ .[insert x X]"
proof -
from assms(1) have "t ∈ (+) (Poly_Mapping.single x e) ` .[X]" unfolding assms(2) by (rule imageI)
with UNIV_I show ?thesis unfolding PPs_insert by (rule UN_I)
qed
corollary PPs_insertE:
assumes "t ∈ .[insert x X]"
obtains e tx where "tx ∈ .[X]" and "t = Poly_Mapping.single x e + tx"
proof -
from assms obtain e where "t ∈ (+) (Poly_Mapping.single x e) ` .[X]" unfolding PPs_insert ..
then obtain tx where "tx ∈ .[X]" and "t = Poly_Mapping.single x e + tx" ..
thus ?thesis ..
qed
lemma PPs_Int: ".[X ∩ Y] = .[X] ∩ .[Y]"
by (auto simp: PPs_def)
lemma PPs_INT: ".[⋂ X] = ⋂ (PPs ` X)"
by (auto simp: PPs_def)
subsubsection ‹@{const Polys}›
lemma Polys_alt: "P[X] = {p. indets p ⊆ X}"
by (auto simp: Polys_def PPs_def indets_def)
lemma PolysI: "keys p ⊆ .[X] ⟹ p ∈ P[X]"
by (simp add: Polys_def)
lemma PolysI_alt: "indets p ⊆ X ⟹ p ∈ P[X]"
by (simp add: Polys_alt)
lemma PolysD:
assumes "p ∈ P[X]"
shows "keys p ⊆ .[X]" and "indets p ⊆ X"
using assms by (simp add: Polys_def, simp add: Polys_alt)
lemma Polys_empty: "P[{}] = ((range (Poly_Mapping.single 0))::(('x ⇒⇩0 nat) ⇒⇩0 'b::zero) set)"
proof (rule set_eqI)
fix p :: "('x ⇒⇩0 nat) ⇒⇩0 'b::zero"
show "p ∈ P[{}] ⟷ p ∈ range (Poly_Mapping.single 0)"
proof
assume "p ∈ P[{}]"
hence "keys p ⊆ .[{}]" by (rule PolysD)
also have "... = {0}" by simp
finally have "keys p ⊆ {0}" .
hence "Poly_Mapping.single 0 (lookup p 0) = p" by (rule keys_subset_singleton_imp_monomial)
from this[symmetric] UNIV_I show "p ∈ range (Poly_Mapping.single 0)" ..
next
assume "p ∈ range (Poly_Mapping.single 0)"
then obtain c where "p = monomial c 0" ..
thus "p ∈ P[{}]" by (simp add: Polys_def)
qed
qed
lemma Polys_UNIV [simp]: "P[UNIV] = UNIV"
by (simp add: Polys_def)
lemma zero_in_Polys: "0 ∈ P[X]"
by (simp add: Polys_def)
lemma one_in_Polys: "1 ∈ P[X]"
by (simp add: Polys_def zero_in_PPs)
lemma Polys_mono: "X ⊆ Y ⟹ P[X] ⊆ P[Y]"
by (auto simp: Polys_alt)
lemma Polys_closed_monomial: "t ∈ .[X] ⟹ monomial c t ∈ P[X]"
using indets_monomial_subset[where c=c and t=t] by (auto simp: Polys_alt PPs_def)
lemma Polys_closed_plus: "p ∈ P[X] ⟹ q ∈ P[X] ⟹ p + q ∈ P[X]"
using indets_plus_subset[of p q] by (auto simp: Polys_alt PPs_def)
lemma Polys_closed_uminus: "p ∈ P[X] ⟹ -p ∈ P[X]"
by (simp add: Polys_def keys_uminus)
lemma Polys_closed_minus: "p ∈ P[X] ⟹ q ∈ P[X] ⟹ p - q ∈ P[X]"
using indets_minus_subset[of p q] by (auto simp: Polys_alt PPs_def)
lemma Polys_closed_monom_mult: "t ∈ .[X] ⟹ p ∈ P[X] ⟹ punit.monom_mult c t p ∈ P[X]"
using indets_monom_mult_subset[of c t p] by (auto simp: Polys_alt PPs_def)
corollary Polys_closed_map_scale: "p ∈ P[X] ⟹ (c::_::semiring_0) ⋅ p ∈ P[X]"
unfolding punit.map_scale_eq_monom_mult using zero_in_PPs by (rule Polys_closed_monom_mult)
lemma Polys_closed_times: "p ∈ P[X] ⟹ q ∈ P[X] ⟹ p * q ∈ P[X]"
using indets_times_subset[of p q] by (auto simp: Polys_alt PPs_def)
lemma Polys_closed_power: "p ∈ P[X] ⟹ p ^ m ∈ P[X]"
by (induct m) (auto intro: one_in_Polys Polys_closed_times)
lemma Polys_closed_sum: "(⋀a. a ∈ A ⟹ f a ∈ P[X]) ⟹ sum f A ∈ P[X]"
by (induct A rule: infinite_finite_induct) (auto intro: zero_in_Polys Polys_closed_plus)
lemma Polys_closed_prod: "(⋀a. a ∈ A ⟹ f a ∈ P[X]) ⟹ prod f A ∈ P[X]"
by (induct A rule: infinite_finite_induct) (auto intro: one_in_Polys Polys_closed_times)
lemma Polys_closed_sum_list: "(⋀x. x ∈ set xs ⟹ x ∈ P[X]) ⟹ sum_list xs ∈ P[X]"
by (induct xs) (auto intro: zero_in_Polys Polys_closed_plus)
lemma Polys_closed_except: "p ∈ P[X] ⟹ except p T ∈ P[X]"
by (auto intro!: PolysI simp: keys_except dest!: PolysD(1))
lemma times_in_PolysD:
assumes "p * q ∈ P[X]" and "p ∈ P[X]" and "p ≠ (0::('x::linorder ⇒⇩0 nat) ⇒⇩0 'a::semiring_no_zero_divisors)"
shows "q ∈ P[X]"
proof -
define qX where "qX = except q (- .[X])"
define qY where "qY = except q .[X]"
have q: "q = qX + qY" by (simp only: qX_def qY_def add.commute flip: except_decomp)
have "qX ∈ P[X]" by (rule PolysI) (simp add: qX_def keys_except)
with assms(2) have "p * qX ∈ P[X]" by (rule Polys_closed_times)
show ?thesis
proof (cases "qY = 0")
case True
with ‹qX ∈ P[X]› show ?thesis by (simp add: q)
next
case False
with assms(3) have "p * qY ≠ 0" by simp
hence "keys (p * qY) ≠ {}" by simp
then obtain t where "t ∈ keys (p * qY)" by blast
then obtain t1 t2 where "t2 ∈ keys qY" and t: "t = t1 + t2" by (rule in_keys_timesE)
have "t ∉ .[X]" unfolding t
proof
assume "t1 + t2 ∈ .[X]"
hence "t1 + t2 - t1 ∈ .[X]" by (rule PPs_closed_minus)
hence "t2 ∈ .[X]" by simp
with ‹t2 ∈ keys qY› show False by (simp add: qY_def keys_except)
qed
have "t ∉ keys (p * qX)"
proof
assume "t ∈ keys (p * qX)"
also from ‹p * qX ∈ P[X]› have "… ⊆ .[X]" by (rule PolysD)
finally have "t ∈ .[X]" .
with ‹t ∉ .[X]› show False ..
qed
with ‹t ∈ keys (p * qY)› have "t ∈ keys (p * qX + p * qY)" by (rule in_keys_plusI2)
also have "… = keys (p * q)" by (simp only: q algebra_simps)
finally have "p * q ∉ P[X]" using ‹t ∉ .[X]› by (auto simp: Polys_def)
thus ?thesis using assms(1) ..
qed
qed
lemma poly_mapping_plus_induct_Polys [consumes 1, case_names 0 plus]:
assumes "p ∈ P[X]" and "P 0"
and "⋀p c t. t ∈ .[X] ⟹ p ∈ P[X] ⟹ c ≠ 0 ⟹ t ∉ keys p ⟹ P p ⟹ P (monomial c t + p)"
shows "P p"
using assms(1)
proof (induct p rule: poly_mapping_plus_induct)
case 1
show ?case by (fact assms(2))
next
case step: (2 p c t)
from step.hyps(1) have 1: "keys (monomial c t) = {t}" by simp
also from step.hyps(2) have "… ∩ keys p = {}" by simp
finally have "keys (monomial c t + p) = keys (monomial c t) ∪ keys p" by (rule keys_add[symmetric])
hence "keys (monomial c t + p) = insert t (keys p)" by (simp only: 1 flip: insert_is_Un)
moreover from step.prems(1) have "keys (monomial c t + p) ⊆ .[X]" by (rule PolysD)
ultimately have "t ∈ .[X]" and "keys p ⊆ .[X]" by blast+
from this(2) have "p ∈ P[X]" by (rule PolysI)
hence "P p" by (rule step.hyps)
with ‹t ∈ .[X]› ‹p ∈ P[X]› step.hyps(1, 2) show ?case by (rule assms(3))
qed
lemma Polys_Int: "P[X ∩ Y] = P[X] ∩ P[Y]"
by (auto simp: Polys_def PPs_Int)
lemma Polys_INT: "P[⋂ X] = ⋂ (Polys ` X)"
by (auto simp: Polys_def PPs_INT)
subsection ‹Substitution Homomorphism›
text ‹The substitution homomorphism defined here is more general than @{const insertion}, since
it replaces indeterminates by @{emph ‹polynomials›} rather than coefficients, and therefore
constructs new polynomials.›
definition subst_pp :: "('x ⇒ (('y ⇒⇩0 nat) ⇒⇩0 'a)) ⇒ ('x ⇒⇩0 nat) ⇒ (('y ⇒⇩0 nat) ⇒⇩0 'a::comm_semiring_1)"
where "subst_pp f t = (∏x∈keys t. (f x) ^ (lookup t x))"
definition poly_subst :: "('x ⇒ (('y ⇒⇩0 nat) ⇒⇩0 'a)) ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ (('y ⇒⇩0 nat) ⇒⇩0 'a::comm_semiring_1)"
where "poly_subst f p = (∑t∈keys p. punit.monom_mult (lookup p t) 0 (subst_pp f t))"
lemma subst_pp_alt: "subst_pp f t = (∏x. (f x) ^ (lookup t x))"
proof -
from finite_keys have "subst_pp f t = (∏x. if x ∈ keys t then (f x) ^ (lookup t x) else 1)"
unfolding subst_pp_def by (rule Prod_any.conditionalize)
also have "... = (∏x. (f x) ^ (lookup t x))" by (rule Prod_any.cong) (simp add: in_keys_iff)
finally show ?thesis .
qed
lemma subst_pp_zero [simp]: "subst_pp f 0 = 1"
by (simp add: subst_pp_def)
lemma subst_pp_trivial_not_zero:
assumes "t ≠ 0"
shows "subst_pp (λ_. 0) t = (0::(_ ⇒⇩0 'b::comm_semiring_1))"
unfolding subst_pp_def using finite_keys
proof (rule prod_zero)
from assms have "keys t ≠ {}" by simp
then obtain x where "x ∈ keys t" by blast
thus "∃x∈keys t. 0 ^ lookup t x = (0::(_ ⇒⇩0 'b))"
proof
from ‹x ∈ keys t› have "0 < lookup t x" by (simp add: in_keys_iff)
thus "0 ^ lookup t x = (0::(_ ⇒⇩0 'b))" by (rule Power.semiring_1_class.zero_power)
qed
qed
lemma subst_pp_single: "subst_pp f (Poly_Mapping.single x e) = (f x) ^ e"
by (simp add: subst_pp_def)
corollary subst_pp_trivial: "subst_pp (λ_. 0) t = (if t = 0 then 1 else 0)"
by (simp split: if_split add: subst_pp_trivial_not_zero)
lemma power_lookup_not_one_subset_keys: "{x. f x ^ (lookup t x) ≠ 1} ⊆ keys t"
proof (rule, simp)
fix x
assume "f x ^ (lookup t x) ≠ 1"
thus "x ∈ keys t" unfolding in_keys_iff by (metis power_0)
qed
corollary finite_power_lookup_not_one: "finite {x. f x ^ (lookup t x) ≠ 1}"
by (rule finite_subset, fact power_lookup_not_one_subset_keys, fact finite_keys)
lemma subst_pp_plus: "subst_pp f (s + t) = subst_pp f s * subst_pp f t"
by (simp add: subst_pp_alt lookup_add power_add, rule Prod_any.distrib, (fact finite_power_lookup_not_one)+)
lemma subst_pp_id:
assumes "⋀x. x ∈ keys t ⟹ f x = monomial 1 (Poly_Mapping.single x 1)"
shows "subst_pp f t = monomial 1 t"
proof -
have "subst_pp f t = (∏x∈keys t. monomial 1 (Poly_Mapping.single x (lookup t x)))"
proof (simp only: subst_pp_def, rule prod.cong, fact refl)
fix x
assume "x ∈ keys t"
thus "f x ^ lookup t x = monomial 1 (Poly_Mapping.single x (lookup t x))"
by (simp add: assms monomial_single_power)
qed
also have "... = monomial 1 t"
by (simp add: punit.monomial_prod_sum[symmetric] poly_mapping_sum_monomials)
finally show ?thesis .
qed
lemma in_indets_subst_ppE:
assumes "x ∈ indets (subst_pp f t)"
obtains y where "y ∈ keys t" and "x ∈ indets (f y)"
proof -
note assms
also have "indets (subst_pp f t) ⊆ (⋃y∈keys t. indets ((f y) ^ (lookup t y)))" unfolding subst_pp_def
by (rule indets_prod_subset)
finally obtain y where "y ∈ keys t" and "x ∈ indets ((f y) ^ (lookup t y))" ..
note this(2)
also have "indets ((f y) ^ (lookup t y)) ⊆ indets (f y)" by (rule indets_power_subset)
finally have "x ∈ indets (f y)" .
with ‹y ∈ keys t› show ?thesis ..
qed
lemma subst_pp_by_monomials:
assumes "⋀y. y ∈ keys t ⟹ f y = monomial (c y) (s y)"
shows "subst_pp f t = monomial (∏y∈keys t. (c y) ^ lookup t y) (∑y∈keys t. lookup t y ⋅ s y)"
by (simp add: subst_pp_def assms monomial_power_map_scale punit.monomial_prod_sum)
lemma poly_deg_subst_pp_eq_zeroI:
assumes "⋀x. x ∈ keys t ⟹ poly_deg (f x) = 0"
shows "poly_deg (subst_pp f t) = 0"
proof -
have "poly_deg (subst_pp f t) ≤ (∑x∈keys t. poly_deg ((f x) ^ (lookup t x)))"
unfolding subst_pp_def by (fact poly_deg_prod_le)
also have "... = 0"
proof (rule sum.neutral, rule)
fix x
assume "x ∈ keys t"
hence "poly_deg (f x) = 0" by (rule assms)
have "f x ^ lookup t x = (∏i=0..<lookup t x. f x)" by simp
also have "poly_deg ... ≤ (∑i=0..<lookup t x. poly_deg (f x))" by (rule poly_deg_prod_le)
also have "... = 0" by (simp add: ‹poly_deg (f x) = 0›)
finally show "poly_deg (f x ^ lookup t x) = 0" by simp
qed
finally show ?thesis by simp
qed
lemma poly_deg_subst_pp_le:
assumes "⋀x. x ∈ keys t ⟹ poly_deg (f x) ≤ 1"
shows "poly_deg (subst_pp f t) ≤ deg_pm t"
proof -
have "poly_deg (subst_pp f t) ≤ (∑x∈keys t. poly_deg ((f x) ^ (lookup t x)))"
unfolding subst_pp_def by (fact poly_deg_prod_le)
also have "... ≤ (∑x∈keys t. lookup t x)"
proof (rule sum_mono)
fix x
assume "x ∈ keys t"
hence "poly_deg (f x) ≤ 1" by (rule assms)
have "f x ^ lookup t x = (∏i=0..<lookup t x. f x)" by simp
also have "poly_deg ... ≤ (∑i=0..<lookup t x. poly_deg (f x))" by (rule poly_deg_prod_le)
also from ‹poly_deg (f x) ≤ 1› have "... ≤ (∑i=0..<lookup t x. 1)" by (rule sum_mono)
finally show "poly_deg (f x ^ lookup t x) ≤ lookup t x" by simp
qed
also have "... = deg_pm t" by (rule deg_pm_superset[symmetric], fact subset_refl, fact finite_keys)
finally show ?thesis by simp
qed
lemma poly_subst_alt: "poly_subst f p = (∑t. punit.monom_mult (lookup p t) 0 (subst_pp f t))"
proof -
from finite_keys have "poly_subst f p = (∑t. if t ∈ keys p then punit.monom_mult (lookup p t) 0 (subst_pp f t) else 0)"
unfolding poly_subst_def by (rule Sum_any.conditionalize)
also have "… = (∑t. punit.monom_mult (lookup p t) 0 (subst_pp f t))"
by (rule Sum_any.cong) (simp add: in_keys_iff)
finally show ?thesis .
qed
lemma poly_subst_trivial [simp]: "poly_subst (λ_. 0) p = monomial (lookup p 0) 0"
by (simp add: poly_subst_def subst_pp_trivial if_distrib in_keys_iff cong: if_cong)
(metis mult.right_neutral times_monomial_left)
lemma poly_subst_zero [simp]: "poly_subst f 0 = 0"
by (simp add: poly_subst_def)
lemma monom_mult_lookup_not_zero_subset_keys:
"{t. punit.monom_mult (lookup p t) 0 (subst_pp f t) ≠ 0} ⊆ keys p"
proof (rule, simp)
fix t
assume "punit.monom_mult (lookup p t) 0 (subst_pp f t) ≠ 0"
thus "t ∈ keys p" unfolding in_keys_iff by (metis punit.monom_mult_zero_left)
qed
corollary finite_monom_mult_lookup_not_zero:
"finite {t. punit.monom_mult (lookup p t) 0 (subst_pp f t) ≠ 0}"
by (rule finite_subset, fact monom_mult_lookup_not_zero_subset_keys, fact finite_keys)
lemma poly_subst_plus: "poly_subst f (p + q) = poly_subst f p + poly_subst f q"
by (simp add: poly_subst_alt lookup_add punit.monom_mult_dist_left, rule Sum_any.distrib,
(fact finite_monom_mult_lookup_not_zero)+)
lemma poly_subst_uminus: "poly_subst f (-p) = - poly_subst f (p::('x ⇒⇩0 nat) ⇒⇩0 'b::comm_ring_1)"
by (simp add: poly_subst_def keys_uminus punit.monom_mult_uminus_left sum_negf)
lemma poly_subst_minus:
"poly_subst f (p - q) = poly_subst f p - poly_subst f (q::('x ⇒⇩0 nat) ⇒⇩0 'b::comm_ring_1)"
proof -
have "poly_subst f (p + (-q)) = poly_subst f p + poly_subst f (-q)" by (fact poly_subst_plus)
thus ?thesis by (simp add: poly_subst_uminus)
qed
lemma poly_subst_monomial: "poly_subst f (monomial c t) = punit.monom_mult c 0 (subst_pp f t)"
by (simp add: poly_subst_def lookup_single)
corollary poly_subst_one [simp]: "poly_subst f 1 = 1"
by (simp add: single_one[symmetric] poly_subst_monomial punit.monom_mult_monomial del: single_one)
lemma poly_subst_times: "poly_subst f (p * q) = poly_subst f p * poly_subst f q"
proof -
have bij: "bij (λ(l, n, m). (m, l, n))"
by (auto intro!: bijI injI simp add: image_def)
let ?P = "keys p"
let ?Q = "keys q"
let ?PQ = "{s + t | s t. lookup p s ≠ 0 ∧ lookup q t ≠ 0}"
have fin_PQ: "finite ?PQ"
by (rule finite_not_eq_zero_sumI, simp_all)
have fin_1: "finite {l. lookup p l * (∑qa. lookup q qa when t = l + qa) ≠ 0}" for t
proof (rule finite_subset)
show "{l. lookup p l * (∑qa. lookup q qa when t = l + qa) ≠ 0} ⊆ keys p"
by (rule, auto simp: in_keys_iff)
qed (fact finite_keys)
have fin_2: "finite {v. (lookup q v when t = u + v) ≠ 0}" for t u
proof (rule finite_subset)
show "{v. (lookup q v when t = u + v) ≠ 0} ⊆ keys q"
by (rule, auto simp: in_keys_iff)
qed (fact finite_keys)
have fin_3: "finite {v. (lookup p u * lookup q v when t = u + v) ≠ 0}" for t u
proof (rule finite_subset)
show "{v. (lookup p u * lookup q v when t = u + v) ≠ 0} ⊆ keys q"
by (rule, auto simp add: in_keys_iff simp del: lookup_not_eq_zero_eq_in_keys)
qed (fact finite_keys)
have "(∑t. punit.monom_mult (lookup (p * q) t) 0 (subst_pp f t)) =
(∑t. ∑u. punit.monom_mult (lookup p u * (∑v. lookup q v when t = u + v)) 0 (subst_pp f t))"
by (simp add: times_poly_mapping.rep_eq prod_fun_def punit.monom_mult_Sum_any_left[OF fin_1])
also have "… = (∑t. ∑u. ∑v. (punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t)) when t = u + v)"
by (simp add: Sum_any_right_distrib[OF fin_2] punit.monom_mult_Sum_any_left[OF fin_3] mult_when punit.when_monom_mult)
also have "… = (∑t. (∑(u, v). (punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t)) when t = u + v))"
by (subst (2) Sum_any.cartesian_product [of "?P × ?Q"]) (auto simp: in_keys_iff)
also have "… = (∑(t, u, v). punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t) when t = u + v)"
apply (subst Sum_any.cartesian_product [of "?PQ × (?P × ?Q)"])
apply (auto simp: fin_PQ in_keys_iff)
apply (metis monomial_0I mult_not_zero times_monomial_left)
done
also have "… = (∑(u, v, t). punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t) when t = u + v)"
using bij by (rule Sum_any.reindex_cong [of "λ(u, v, t). (t, u, v)"]) (simp add: fun_eq_iff)
also have "… = (∑(u, v). ∑t. punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f t) when t = u + v)"
apply (subst Sum_any.cartesian_product2 [of "(?P × ?Q) × ?PQ"])
apply (auto simp: fin_PQ in_keys_iff)
apply (metis monomial_0I mult_not_zero times_monomial_left)
done
also have "… = (∑(u, v). punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f u * subst_pp f v))"
by (simp add: subst_pp_plus)
also have "… = (∑u. ∑v. punit.monom_mult (lookup p u * lookup q v) 0 (subst_pp f u * subst_pp f v))"
by (subst Sum_any.cartesian_product [of "?P × ?Q"]) (auto simp: in_keys_iff)
also have "… = (∑u. ∑v. (punit.monom_mult (lookup p u) 0 (subst_pp f u)) * (punit.monom_mult (lookup q v) 0 (subst_pp f v)))"
by (simp add: times_monomial_left[symmetric] ac_simps mult_single)
also have "… = (∑t. punit.monom_mult (lookup p t) 0 (subst_pp f t)) *
(∑t. punit.monom_mult (lookup q t) 0 (subst_pp f t))"
by (rule Sum_any_product [symmetric], (fact finite_monom_mult_lookup_not_zero)+)
finally show ?thesis by (simp add: poly_subst_alt)
qed
corollary poly_subst_monom_mult:
"poly_subst f (punit.monom_mult c t p) = punit.monom_mult c 0 (subst_pp f t * poly_subst f p)"
by (simp only: times_monomial_left[symmetric] poly_subst_times poly_subst_monomial mult.assoc)
corollary poly_subst_monom_mult':
"poly_subst f (punit.monom_mult c t p) = (punit.monom_mult c 0 (subst_pp f t)) * poly_subst f p"
by (simp only: times_monomial_left[symmetric] poly_subst_times poly_subst_monomial)
lemma poly_subst_sum: "poly_subst f (sum p A) = (∑a∈A. poly_subst f (p a))"
by (rule fun_sum_commute, simp_all add: poly_subst_plus)
lemma poly_subst_prod: "poly_subst f (prod p A) = (∏a∈A. poly_subst f (p a))"
by (rule fun_prod_commute, simp_all add: poly_subst_times)
lemma poly_subst_power: "poly_subst f (p ^ n) = (poly_subst f p) ^ n"
by (induct n, simp_all add: poly_subst_times)
lemma poly_subst_subst_pp: "poly_subst f (subst_pp g t) = subst_pp (λx. poly_subst f (g x)) t"
by (simp only: subst_pp_def poly_subst_prod poly_subst_power)
lemma poly_subst_poly_subst: "poly_subst f (poly_subst g p) = poly_subst (λx. poly_subst f (g x)) p"
proof -
have "poly_subst f (poly_subst g p) =
poly_subst f (∑t∈keys p. punit.monom_mult (lookup p t) 0 (subst_pp g t))"
by (simp only: poly_subst_def)
also have "… = (∑t∈keys p. punit.monom_mult (lookup p t) 0 (subst_pp (λx. poly_subst f (g x)) t))"
by (simp add: poly_subst_sum poly_subst_monom_mult poly_subst_subst_pp)
also have "… = poly_subst (λx. poly_subst f (g x)) p" by (simp only: poly_subst_def)
finally show ?thesis .
qed
lemma poly_subst_id:
assumes "⋀x. x ∈ indets p ⟹ f x = monomial 1 (Poly_Mapping.single x 1)"
shows "poly_subst f p = p"
proof -
have "poly_subst f p = (∑t∈keys p. monomial (lookup p t) t)"
proof (simp only: poly_subst_def, rule sum.cong, fact refl)
fix t
assume "t ∈ keys p"
have eq: "subst_pp f t = monomial 1 t"
by (rule subst_pp_id, rule assms, erule in_indetsI, fact ‹t ∈ keys p›)
show "punit.monom_mult (lookup p t) 0 (subst_pp f t) = monomial (lookup p t) t"
by (simp add: eq punit.monom_mult_monomial)
qed
also have "... = p" by (simp only: poly_mapping_sum_monomials)
finally show ?thesis .
qed
lemma in_keys_poly_substE:
assumes "t ∈ keys (poly_subst f p)"
obtains s where "s ∈ keys p" and "t ∈ keys (subst_pp f s)"
proof -
note assms
also have "keys (poly_subst f p) ⊆ (⋃t∈keys p. keys (punit.monom_mult (lookup p t) 0 (subst_pp f t)))"
unfolding poly_subst_def by (rule keys_sum_subset)
finally obtain s where "s ∈ keys p" and "t ∈ keys (punit.monom_mult (lookup p s) 0 (subst_pp f s))" ..
note this(2)
also have "… ⊆ (+) 0 ` keys (subst_pp f s)" by (rule punit.keys_monom_mult_subset[simplified])
also have "… = keys (subst_pp f s)" by simp
finally have "t ∈ keys (subst_pp f s)" .
with ‹s ∈ keys p› show ?thesis ..
qed
lemma in_indets_poly_substE:
assumes "x ∈ indets (poly_subst f p)"
obtains y where "y ∈ indets p" and "x ∈ indets (f y)"
proof -
note assms
also have "indets (poly_subst f p) ⊆ (⋃t∈keys p. indets (punit.monom_mult (lookup p t) 0 (subst_pp f t)))"
unfolding poly_subst_def by (rule indets_sum_subset)
finally obtain t where "t ∈ keys p" and "x ∈ indets (punit.monom_mult (lookup p t) 0 (subst_pp f t))" ..
note this(2)
also have "indets (punit.monom_mult (lookup p t) 0 (subst_pp f t)) ⊆ keys (0::('a ⇒⇩0 nat)) ∪ indets (subst_pp f t)"
by (rule indets_monom_mult_subset)
also have "... = indets (subst_pp f t)" by simp
finally obtain y where "y ∈ keys t" and "x ∈ indets (f y)" by (rule in_indets_subst_ppE)
from this(1) ‹t ∈ keys p› have "y ∈ indets p" by (rule in_indetsI)
from this ‹x ∈ indets (f y)› show ?thesis ..
qed
lemma poly_deg_poly_subst_eq_zeroI:
assumes "⋀x. x ∈ indets p ⟹ poly_deg (f x) = 0"
shows "poly_deg (poly_subst (f::_ ⇒ (('y ⇒⇩0 _) ⇒⇩0 _)) (p::('x ⇒⇩0 _) ⇒⇩0 'b::comm_semiring_1)) = 0"
proof (cases "p = 0")
case True
thus ?thesis by simp
next
case False
have "poly_deg (poly_subst f p) ≤ Max (poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p)"
unfolding poly_subst_def by (fact poly_deg_sum_le)
also have "... ≤ 0"
proof (rule Max.boundedI)
show "finite (poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p)"
by (simp add: finite_image_iff)
next
from False show "poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p ≠ {}" by simp
next
fix d
assume "d ∈ poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p"
then obtain t where "t ∈ keys p" and d: "d = poly_deg (punit.monom_mult (lookup p t) 0 (subst_pp f t))"
by fastforce
have "d ≤ deg_pm (0::'y ⇒⇩0 nat) + poly_deg (subst_pp f t)"
unfolding d by (fact poly_deg_monom_mult_le)
also have "... = poly_deg (subst_pp f t)" by simp
also have "... = 0" by (rule poly_deg_subst_pp_eq_zeroI, rule assms, erule in_indetsI, fact)
finally show "d ≤ 0" .
qed
finally show ?thesis by simp
qed
lemma poly_deg_poly_subst_le:
assumes "⋀x. x ∈ indets p ⟹ poly_deg (f x) ≤ 1"
shows "poly_deg (poly_subst (f::_ ⇒ (('y ⇒⇩0 _) ⇒⇩0 _)) (p::('x ⇒⇩0 nat) ⇒⇩0 'b::comm_semiring_1)) ≤ poly_deg p"
proof (cases "p = 0")
case True
thus ?thesis by simp
next
case False
have "poly_deg (poly_subst f p) ≤ Max (poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p)"
unfolding poly_subst_def by (fact poly_deg_sum_le)
also have "... ≤ poly_deg p"
proof (rule Max.boundedI)
show "finite (poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p)"
by (simp add: finite_image_iff)
next
from False show "poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p ≠ {}" by simp
next
fix d
assume "d ∈ poly_deg ` (λt. punit.monom_mult (lookup p t) 0 (subst_pp f t)) ` keys p"
then obtain t where "t ∈ keys p" and d: "d = poly_deg (punit.monom_mult (lookup p t) 0 (subst_pp f t))"
by fastforce
have "d ≤ deg_pm (0::'y ⇒⇩0 nat) + poly_deg (subst_pp f t)"
unfolding d by (fact poly_deg_monom_mult_le)
also have "... = poly_deg (subst_pp f t)" by simp
also have "... ≤ deg_pm t" by (rule poly_deg_subst_pp_le, rule assms, erule in_indetsI, fact)
also from ‹t ∈ keys p› have "... ≤ poly_deg p" by (rule poly_deg_max_keys)
finally show "d ≤ poly_deg p" .
qed
finally show ?thesis by simp
qed
lemma subst_pp_cong: "s = t ⟹ (⋀x. x ∈ keys t ⟹ f x = g x) ⟹ subst_pp f s = subst_pp g t"
by (simp add: subst_pp_def)
lemma poly_subst_cong:
assumes "p = q" and "⋀x. x ∈ indets q ⟹ f x = g x"
shows "poly_subst f p = poly_subst g q"
proof (simp add: poly_subst_def assms(1), rule sum.cong)
fix t
assume "t ∈ keys q"
{
fix x
assume "x ∈ keys t"
with ‹t ∈ keys q› have "x ∈ indets q" by (auto simp: indets_def)
hence "f x = g x" by (rule assms(2))
}
thus "punit.monom_mult (lookup q t) 0 (subst_pp f t) = punit.monom_mult (lookup q t) 0 (subst_pp g t)"
by (simp cong: subst_pp_cong)
qed (fact refl)
lemma Polys_homomorphismE:
obtains h where "⋀p q. h (p + q) = h p + h q" and "⋀p q. h (p * q) = h p * h q"
and "⋀p::('x ⇒⇩0 nat) ⇒⇩0 'a::comm_ring_1. h (h p) = h p" and "range h = P[X]"
proof -
let ?f = "λx. if x ∈ X then monomial (1::'a) (Poly_Mapping.single x 1) else 1"
have 1: "poly_subst ?f p = p" if "p ∈ P[X]" for p
proof (rule poly_subst_id)
fix x
assume "x ∈ indets p"
also from that have "… ⊆ X" by (rule PolysD)
finally show "?f x = monomial 1 (Poly_Mapping.single x 1)" by simp
qed
have 2: "poly_subst ?f p ∈ P[X]" for p
proof (intro PolysI_alt subsetI)
fix x
assume "x ∈ indets (poly_subst ?f p)"
then obtain y where "x ∈ indets (?f y)" by (rule in_indets_poly_substE)
thus "x ∈ X" by (simp add: indets_monomial split: if_split_asm)
qed
from poly_subst_plus poly_subst_times show ?thesis
proof
fix p
from 2 show "poly_subst ?f (poly_subst ?f p) = poly_subst ?f p" by (rule 1)
next
show "range (poly_subst ?f) = P[X]"
proof (intro set_eqI iffI)
fix p :: "_ ⇒⇩0 'a"
assume "p ∈ P[X]"
hence "p = poly_subst ?f p" by (simp only: 1)
thus "p ∈ range (poly_subst ?f)" by (rule image_eqI) simp
qed (auto intro: 2)
qed
qed
lemma in_idealE_Polys_finite:
assumes "finite B" and "B ⊆ P[X]" and "p ∈ P[X]" and "(p::('x ⇒⇩0 nat) ⇒⇩0 'a::comm_ring_1) ∈ ideal B"
obtains q where "⋀b. q b ∈ P[X]" and "p = (∑b∈B. q b * b)"
proof -
obtain h where "⋀p q. h (p + q) = h p + h q" and "⋀p q. h (p * q) = h p * h q"
and "⋀p::('x ⇒⇩0 nat) ⇒⇩0 'a. h (h p) = h p" and rng[symmetric]: "range h = P[X]"
by (rule Polys_homomorphismE) blast
from this(1-3) assms obtain q where "⋀b. q b ∈ P[X]" and "p = (∑b∈B. q b * b)"
unfolding rng by (rule in_idealE_homomorphism_finite) blast
thus ?thesis ..
qed
corollary in_idealE_Polys:
assumes "B ⊆ P[X]" and "p ∈ P[X]" and "p ∈ ideal B"
obtains A q where "finite A" and "A ⊆ B" and "⋀b. q b ∈ P[X]" and "p = (∑b∈A. q b * b)"
proof -
from assms(3) obtain A where "finite A" and "A ⊆ B" and "p ∈ ideal A"
by (rule ideal.span_finite_subset)
from this(2) assms(1) have "A ⊆ P[X]" by (rule subset_trans)
with ‹finite A› obtain q where "⋀b. q b ∈ P[X]" and "p = (∑b∈A. q b * b)"
using assms(2) ‹p ∈ ideal A› by (rule in_idealE_Polys_finite) blast
with ‹finite A› ‹A ⊆ B› show ?thesis ..
qed
lemma ideal_induct_Polys [consumes 3, case_names 0 plus]:
assumes "F ⊆ P[X]" and "p ∈ P[X]" and "p ∈ ideal F"
assumes "P 0" and "⋀c q h. c ∈ P[X] ⟹ q ∈ F ⟹ P h ⟹ h ∈ P[X] ⟹ P (c * q + h)"
shows "P (p::('x ⇒⇩0 nat) ⇒⇩0 'a::comm_ring_1)"
proof -
obtain h where "⋀p q. h (p + q) = h p + h q" and "⋀p q. h (p * q) = h p * h q"
and "⋀p::('x ⇒⇩0 nat) ⇒⇩0 'a. h (h p) = h p" and rng[symmetric]: "range h = P[X]"
by (rule Polys_homomorphismE) blast
from this(1-3) assms show ?thesis
unfolding rng by (rule ideal_induct_homomorphism) blast
qed
lemma image_poly_subst_ideal_subset: "poly_subst g ` ideal F ⊆ ideal (poly_subst g ` F)"
proof (intro subsetI, elim imageE)
fix h f
assume h: "h = poly_subst g f"
assume "f ∈ ideal F"
thus "h ∈ ideal (poly_subst g ` F)" unfolding h
proof (induct f rule: ideal.span_induct_alt)
case base
show ?case by (simp add: ideal.span_zero)
next
case (step c f h)
from step.hyps(1) have "poly_subst g f ∈ ideal (poly_subst g ` F)"
by (intro ideal.span_base imageI)
hence "poly_subst g c * poly_subst g f ∈ ideal (poly_subst g ` F)" by (rule ideal.span_scale)
hence "poly_subst g c * poly_subst g f + poly_subst g h ∈ ideal (poly_subst g ` F)"
using step.hyps(2) by (rule ideal.span_add)
thus ?case by (simp only: poly_subst_plus poly_subst_times)
qed
qed
subsection ‹Evaluating Polynomials›
lemma lookup_times_zero:
"lookup (p * q) 0 = lookup p 0 * lookup q (0::'a::{comm_powerprod,ninv_comm_monoid_add})"
proof -
have eq: "(∑v∈keys q. lookup q v when t + v = 0) = (lookup q 0 when t = 0)" for t
proof -
have "(∑v∈keys q. lookup q v when t + v = 0) = (∑v∈keys q ∩ {0}. lookup q v when t + v = 0)"
proof (intro sum.mono_neutral_right ballI)
fix v
assume "v ∈ keys q - keys q ∩ {0}"
hence "v ≠ 0" by blast
hence "t + v ≠ 0" using plus_eq_zero_2 by blast
thus "(lookup q v when t + v = 0) = 0" by simp
qed simp_all
also have "… = (lookup q 0 when t = 0)" by (cases "0 ∈ keys q") (simp_all add: in_keys_iff)
finally show ?thesis .
qed
have "(∑t∈keys p. lookup p t * lookup q 0 when t = 0) =
(∑t∈keys p ∩ {0}. lookup p t * lookup q 0 when t = 0)"
proof (intro sum.mono_neutral_right ballI)
fix t
assume "t ∈ keys p - keys p ∩ {0}"
hence "t ≠ 0" by blast
thus "(lookup p t * lookup q 0 when t = 0) = 0" by simp
qed simp_all
also have "… = lookup p 0 * lookup q 0" by (cases "0 ∈ keys p") (simp_all add: in_keys_iff)
finally show ?thesis by (simp add: lookup_times eq when_distrib)
qed
corollary lookup_prod_zero:
"lookup (prod f I) 0 = (∏i∈I. lookup (f i) (0::_::{comm_powerprod,ninv_comm_monoid_add}))"
by (induct I rule: infinite_finite_induct) (simp_all add: lookup_times_zero)
corollary lookup_power_zero:
"lookup (p ^ k) 0 = lookup p (0::_::{comm_powerprod,ninv_comm_monoid_add}) ^ k"
by (induct k) (simp_all add: lookup_times_zero)
definition poly_eval :: "('x ⇒ 'a) ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ 'a::comm_semiring_1"
where "poly_eval a p = lookup (poly_subst (λy. monomial (a y) (0::'x ⇒⇩0 nat)) p) 0"
lemma poly_eval_alt: "poly_eval a p = (∑t∈keys p. lookup p t * (∏x∈keys t. a x ^ lookup t x))"
by (simp add: poly_eval_def poly_subst_def lookup_sum lookup_times_zero subst_pp_def
lookup_prod_zero lookup_power_zero flip: times_monomial_left)
lemma poly_eval_monomial: "poly_eval a (monomial c t) = c * (∏x∈keys t. a x ^ lookup t x)"
by (simp add: poly_eval_def poly_subst_monomial subst_pp_def punit.lookup_monom_mult
lookup_prod_zero lookup_power_zero)
lemma poly_eval_zero [simp]: "poly_eval a 0 = 0"
by (simp only: poly_eval_def poly_subst_zero lookup_zero)
lemma poly_eval_zero_left [simp]: "poly_eval 0 p = lookup p 0"
by (simp add: poly_eval_def)
lemma poly_eval_plus: "poly_eval a (p + q) = poly_eval a p + poly_eval a q"
by (simp only: poly_eval_def poly_subst_plus lookup_add)
lemma poly_eval_uminus [simp]: "poly_eval a (- p) = - poly_eval (a::_::comm_ring_1) p"
by (simp only: poly_eval_def poly_subst_uminus lookup_uminus)
lemma poly_eval_minus: "poly_eval a (p - q) = poly_eval a p - poly_eval (a::_::comm_ring_1) q"
by (simp only: poly_eval_def poly_subst_minus lookup_minus)
lemma poly_eval_one [simp]: "poly_eval a 1 = 1"
by (simp add: poly_eval_def lookup_one)
lemma poly_eval_times: "poly_eval a (p * q) = poly_eval a p * poly_eval a q"
by (simp only: poly_eval_def poly_subst_times lookup_times_zero)
lemma poly_eval_power: "poly_eval a (p ^ m) = poly_eval a p ^ m"
by (induct m) (simp_all add: poly_eval_times)
lemma poly_eval_sum: "poly_eval a (sum f I) = (∑i∈I. poly_eval a (f i))"
by (induct I rule: infinite_finite_induct) (simp_all add: poly_eval_plus)
lemma poly_eval_prod: "poly_eval a (prod f I) = (∏i∈I. poly_eval a (f i))"
by (induct I rule: infinite_finite_induct) (simp_all add: poly_eval_times)
lemma poly_eval_cong: "p = q ⟹ (⋀x. x ∈ indets q ⟹ a x = b x) ⟹ poly_eval a p = poly_eval b q"
by (simp add: poly_eval_def cong: poly_subst_cong)
lemma indets_poly_eval_subset:
"indets (poly_eval a p) ⊆ ⋃ (indets ` a ` indets p) ∪ ⋃ (indets ` lookup p ` keys p)"
proof (induct p rule: poly_mapping_plus_induct)
case 1
show ?case by simp
next
case (2 p c t)
have "keys (monomial c t + p) = keys (monomial c t) ∪ keys p"
by (rule keys_plus_eqI) (simp add: 2(2))
with 2(1) have eq1: "keys (monomial c t + p) = insert t (keys p)" by simp
hence eq2: "indets (monomial c t + p) = keys t ∪ indets p" by (simp add: indets_def)
from 2(2) have eq3: "lookup (monomial c t + p) t = c" by (simp add: lookup_add in_keys_iff)
have eq4: "lookup (monomial c t + p) s = lookup p s" if "s ∈ keys p" for s
using that 2(2) by (auto simp: lookup_add lookup_single when_def)
have "indets (poly_eval a (monomial c t + p)) =
indets (c * (∏x∈keys t. a x ^ lookup t x) + poly_eval a p)"
by (simp only: poly_eval_plus poly_eval_monomial)
also have "… ⊆ indets (c * (∏x∈keys t. a x ^ lookup t x)) ∪ indets (poly_eval a p)"
by (fact indets_plus_subset)
also have "… ⊆ indets c ∪ (⋃ (indets ` a ` keys t)) ∪
(⋃ (indets ` a ` indets p) ∪ ⋃ (indets ` lookup p ` keys p))"
proof (intro Un_mono 2(3))
have "indets (c * (∏x∈keys t. a x ^ lookup t x)) ⊆ indets c ∪ indets (∏x∈keys t. a x ^ lookup t x)"
by (fact indets_times_subset)
also have "indets (∏x∈keys t. a x ^ lookup t x) ⊆ (⋃x∈keys t. indets (a x ^ lookup t x))"
by (fact indets_prod_subset)
also have "… ⊆ (⋃x∈keys t. indets (a x))" by (intro UN_mono subset_refl indets_power_subset)
also have "… = ⋃ (indets ` a ` keys t)" by simp
finally show "indets (c * (∏x∈keys t. a x ^ lookup t x)) ⊆ indets c ∪ ⋃ (indets ` a ` keys t)"
by blast
qed
also have "… = ⋃ (indets ` a ` indets (monomial c t + p)) ∪
⋃ (indets ` lookup (monomial c t + p) ` keys (monomial c t + p))"
by (simp add: eq1 eq2 eq3 eq4 Un_commute Un_assoc Un_left_commute)
finally show ?case .
qed
lemma image_poly_eval_ideal: "poly_eval a ` ideal F = ideal (poly_eval a ` F)"
proof (intro image_ideal_eq_surj poly_eval_plus poly_eval_times surjI)
fix x
show "poly_eval a (monomial x 0) = x" by (simp add: poly_eval_monomial)
qed
subsection ‹Replacing Indeterminates›
definition map_indets where "map_indets f = poly_subst (λx. monomial 1 (Poly_Mapping.single (f x) 1))"
lemma
shows map_indets_zero [simp]: "map_indets f 0 = 0"
and map_indets_one [simp]: "map_indets f 1 = 1"
and map_indets_uminus [simp]: "map_indets f (- r) = - map_indets f (r::_ ⇒⇩0 _::comm_ring_1)"
and map_indets_plus: "map_indets f (p + q) = map_indets f p + map_indets f q"
and map_indets_minus: "map_indets f (r - s) = map_indets f r - map_indets f s"
and map_indets_times: "map_indets f (p * q) = map_indets f p * map_indets f q"
and map_indets_power [simp]: "map_indets f (p ^ m) = map_indets f p ^ m"
and map_indets_sum: "map_indets f (sum g A) = (∑a∈A. map_indets f (g a))"
and map_indets_prod: "map_indets f (prod g A) = (∏a∈A. map_indets f (g a))"
by (simp_all add: map_indets_def poly_subst_uminus poly_subst_plus poly_subst_minus poly_subst_times
poly_subst_power poly_subst_sum poly_subst_prod)
lemma map_indets_monomial:
"map_indets f (monomial c t) = monomial c (∑x∈keys t. Poly_Mapping.single (f x) (lookup t x))"
by (simp add: map_indets_def poly_subst_monomial subst_pp_def monomial_power_map_scale
punit.monom_mult_monomial flip: punit.monomial_prod_sum)
lemma map_indets_id: "(⋀x. x ∈ indets p ⟹ f x = x) ⟹ map_indets f p = p"
by (simp add: map_indets_def poly_subst_id)
lemma map_indets_map_indets: "map_indets f (map_indets g p) = map_indets (f ∘ g) p"
by (simp add: map_indets_def poly_subst_poly_subst poly_subst_monomial subst_pp_single)
lemma map_indets_cong: "p = q ⟹ (⋀x. x ∈ indets q ⟹ f x = g x) ⟹ map_indets f p = map_indets g q"
unfolding map_indets_def by (simp cong: poly_subst_cong)
lemma poly_subst_map_indets: "poly_subst f (map_indets g p) = poly_subst (f ∘ g) p"
by (simp add: map_indets_def poly_subst_poly_subst poly_subst_monomial subst_pp_single comp_def)
lemma poly_eval_map_indets: "poly_eval a (map_indets g p) = poly_eval (a ∘ g) p"
by (simp add: poly_eval_def poly_subst_map_indets comp_def)
(simp add: poly_subst_def lookup_sum lookup_times_zero subst_pp_def lookup_prod_zero
lookup_power_zero flip: times_monomial_left)
lemma map_indets_inverseE_Polys:
assumes "inj_on f X" and "p ∈ P[X]"
shows "map_indets (the_inv_into X f) (map_indets f p) = p"
unfolding map_indets_map_indets
proof (rule map_indets_id)
fix x
assume "x ∈ indets p"
also from assms(2) have "… ⊆ X" by (rule PolysD)
finally show "(the_inv_into X f ∘ f) x = x" using assms(1) by (auto intro: the_inv_into_f_f)
qed
lemma map_indets_inverseE:
assumes "inj f"
obtains g where "g = the_inv f" and "g ∘ f = id" and "map_indets g ∘ map_indets f = id"
proof -
define g where "g = the_inv f"
moreover from assms have eq: "g ∘ f = id" by (auto intro!: ext the_inv_f_f simp: g_def)
moreover have "map_indets g ∘ map_indets f = id"
by (rule ext) (simp add: map_indets_map_indets eq map_indets_id)
ultimately show ?thesis ..
qed
lemma indets_map_indets_subset: "indets (map_indets f (p::_ ⇒⇩0 'a::comm_semiring_1)) ⊆ f ` indets p"
proof
fix x
assume "x ∈ indets (map_indets f p)"
then obtain y where "y ∈ indets p" and "x ∈ indets (monomial (1::'a) (Poly_Mapping.single (f y) 1))"
unfolding map_indets_def by (rule in_indets_poly_substE)
from this(2) have x: "x = f y" by (simp add: indets_monomial)
from ‹y ∈ indets p› show "x ∈ f ` indets p" unfolding x by (rule imageI)
qed
corollary map_indets_in_Polys: "map_indets f p ∈ P[f ` indets p]"
using indets_map_indets_subset by (rule PolysI_alt)
lemma indets_map_indets:
assumes "inj_on f (indets p)"
shows "indets (map_indets f p) = f ` indets p"
using indets_map_indets_subset
proof (rule subset_antisym)
let ?g = "the_inv_into (indets p) f"
have "p = map_indets ?g (map_indets f p)" unfolding map_indets_map_indets
by (rule sym, rule map_indets_id) (simp add: assms the_inv_into_f_f)
also have "indets … ⊆ ?g ` indets (map_indets f p)" by (fact indets_map_indets_subset)
finally have "f ` indets p ⊆ f ` ?g ` indets (map_indets f p)" by (rule image_mono)
also have "… = (λx. x) ` indets (map_indets f p)" unfolding image_image using refl
proof (rule image_cong)
fix x
assume "x ∈ indets (map_indets f p)"
with indets_map_indets_subset have "x ∈ f ` indets p" ..
with assms show "f (?g x) = x" by (rule f_the_inv_into_f)
qed
finally show "f ` indets p ⊆ indets (map_indets f p)" by simp
qed
lemma image_map_indets_Polys: "map_indets f ` P[X] = (P[f ` X]::(_ ⇒⇩0 'a::comm_semiring_1) set)"
proof (intro set_eqI iffI)
fix p :: "_ ⇒⇩0 'a"
assume "p ∈ map_indets f ` P[X]"
then obtain q where "q ∈ P[X]" and "p = map_indets f q" ..
note this(2)
also have "map_indets f q ∈ P[f ` indets q]" by (fact map_indets_in_Polys)
also from ‹q ∈ _› have "… ⊆ P[f ` X]" by (auto intro!: Polys_mono imageI dest: PolysD)
finally show "p ∈ P[f ` X]" .
next
fix p :: "_ ⇒⇩0 'a"
assume "p ∈ P[f ` X]"
define g where "g = (λy. SOME x. x ∈ X ∧ f x = y)"
have "g y ∈ X ∧ f (g y) = y" if "y ∈ indets p" for y
proof -
note that
also from ‹p ∈ _› have "indets p ⊆ f ` X" by (rule PolysD)
finally obtain x where "x ∈ X" and "y = f x" ..
hence "x ∈ X ∧ f x = y" by simp
thus ?thesis unfolding g_def by (rule someI)
qed
hence 1: "g y ∈ X" and 2: "f (g y) = y" if "y ∈ indets p" for y using that by simp_all
show "p ∈ map_indets f ` P[X]"
proof
show "p = map_indets f (map_indets g p)"
by (rule sym) (simp add: map_indets_map_indets map_indets_id 2)
next
have "map_indets g p ∈ P[g ` indets p]" by (fact map_indets_in_Polys)
also have "… ⊆ P[X]" by (auto intro!: Polys_mono 1)
finally show "map_indets g p ∈ P[X]" .
qed
qed
corollary range_map_indets: "range (map_indets f) = P[range f]"
proof -
have "range (map_indets f) = map_indets f ` P[UNIV]" by simp
also have "… = P[range f]" by (simp only: image_map_indets_Polys)
finally show ?thesis .
qed
lemma in_keys_map_indetsE:
assumes "t ∈ keys (map_indets f (p::_ ⇒⇩0 'a::comm_semiring_1))"
obtains s where "s ∈ keys p" and "t = (∑x∈keys s. Poly_Mapping.single (f x) (lookup s x))"
proof -
let ?f = "(λx. monomial (1::'a) (Poly_Mapping.single (f x) 1))"
from assms obtain s where "s ∈ keys p" and "t ∈ keys (subst_pp ?f s)" unfolding map_indets_def
by (rule in_keys_poly_substE)
note this(2)
also have "… ⊆ {∑x∈keys s. Poly_Mapping.single (f x) (lookup s x)}"
by (simp add: subst_pp_def monomial_power_map_scale flip: punit.monomial_prod_sum)
finally have "t = (∑x∈keys s. Poly_Mapping.single (f x) (lookup s x))" by simp
with ‹s ∈ keys p› show ?thesis ..
qed
lemma keys_map_indets_subset:
"keys (map_indets f p) ⊆ (λt. ∑x∈keys t. Poly_Mapping.single (f x) (lookup t x)) ` keys p"
by (auto elim: in_keys_map_indetsE)
lemma keys_map_indets:
assumes "inj_on f (indets p)"
shows "keys (map_indets f p) = (λt. ∑x∈keys t. Poly_Mapping.single (f x) (lookup t x)) ` keys p"
using keys_map_indets_subset
proof (rule subset_antisym)
let ?g = "the_inv_into (indets p) f"
have "p = map_indets ?g (map_indets f p)" unfolding map_indets_map_indets
by (rule sym, rule map_indets_id) (simp add: assms the_inv_into_f_f)
also have "keys … ⊆ (λt. ∑x∈keys t. monomial (lookup t x) (?g x)) ` keys (map_indets f p)"
by (rule keys_map_indets_subset)
finally have "(λt. ∑x∈keys t. Poly_Mapping.single (f x) (lookup t x)) ` keys p ⊆
(λt. ∑x∈keys t. Poly_Mapping.single (f x) (lookup t x)) `
(λt. ∑x∈keys t. Poly_Mapping.single (?g x) (lookup t x)) ` keys (map_indets f p)"
by (rule image_mono)
also from refl have "… = (λt. ∑x. Poly_Mapping.single (f x) (lookup t x)) `
(λt. ∑x∈keys t. Poly_Mapping.single (?g x) (lookup t x)) ` keys (map_indets f p)"
by (rule image_cong)
(smt (verit) Sum_any.conditionalize Sum_any.cong finite_keys not_in_keys_iff_lookup_eq_zero single_zero)
also have "… = (λt. t) ` keys (map_indets f p)" unfolding image_image using refl
proof (rule image_cong)
fix t
assume "t ∈ keys (map_indets f p)"
have "(∑x. monomial (lookup (∑y∈keys t. Poly_Mapping.single (?g y) (lookup t y)) x) (f x)) =
(∑x. ∑y∈keys t. monomial (lookup t y when ?g y = x) (f x))"
by (simp add: lookup_sum lookup_single monomial_sum)
also have "… = (∑x∈indets p. ∑y∈keys t. Poly_Mapping.single (f x) (lookup t y when ?g y = x))"
proof (intro Sum_any.expand_superset finite_indets subsetI)
fix x
assume "x ∈ {a. (∑y∈keys t. Poly_Mapping.single (f a) (lookup t y when ?g y = a)) ≠ 0}"
hence "(∑y∈keys t. Poly_Mapping.single (f x) (lookup t y when ?g y = x)) ≠ 0" by simp
then obtain y where "y ∈ keys t" and *: "Poly_Mapping.single (f x) (lookup t y when ?g y = x) ≠ 0"
by (rule sum.not_neutral_contains_not_neutral)
from this(1) have "y ∈ indets (map_indets f p)" using ‹t ∈ _› by (rule in_indetsI)
with indets_map_indets_subset have "y ∈ f ` indets p" ..
from * have "x = ?g y" by (simp add: when_def split: if_split_asm)
also from assms ‹y ∈ f ` indets p› subset_refl have "… ∈ indets p" by (rule the_inv_into_into)
finally show "x ∈ indets p" .
qed
also have "… = (∑y∈keys t. ∑x∈indets p. Poly_Mapping.single (f x) (lookup t y when ?g y = x))"
by (fact sum.swap)
also from refl have "… = (∑y∈keys t. Poly_Mapping.single y (lookup t y))"
proof (rule sum.cong)
fix x
assume "x ∈ keys t"
hence "x ∈ indets (map_indets f p)" using ‹t ∈ _› by (rule in_indetsI)
with indets_map_indets_subset have "x ∈ f ` indets p" ..
with assms have "?g x ∈ indets p" using subset_refl by (rule the_inv_into_into)
hence "{?g x} ⊆ indets p" by simp
with finite_indets have "(∑y∈indets p. Poly_Mapping.single (f y) (lookup t x when ?g x = y)) =
(∑y∈{?g x}. Poly_Mapping.single (f y) (lookup t x when ?g x = y))"
by (rule sum.mono_neutral_right) (simp add: monomial_0_iff when_def)
also from assms ‹x ∈ f ` indets p› have "… = Poly_Mapping.single x (lookup t x)"
by (simp add: f_the_inv_into_f)
finally show "(∑y∈indets p. Poly_Mapping.single (f y) (lookup t x when ?g x = y)) =
Poly_Mapping.single x (lookup t x)" .
qed
also have "… = t" by (fact poly_mapping_sum_monomials)
finally show "(∑x. monomial (lookup (∑y∈keys t. Poly_Mapping.single (?g y) (lookup t y)) x) (f x)) = t" .
qed
also have "… = keys (map_indets f p)" by simp
finally show "(λt. ∑x∈keys t. Poly_Mapping.single (f x) (lookup t x)) ` keys p ⊆ keys (map_indets f p)" .
qed
lemma poly_deg_map_indets_le: "poly_deg (map_indets f p) ≤ poly_deg p"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys (map_indets f p)"
then obtain s where "s ∈ keys p" and t: "t = (∑x∈keys s. Poly_Mapping.single (f x) (lookup s x))"
by (rule in_keys_map_indetsE)
from this(1) have "deg_pm s ≤ poly_deg p" by (rule poly_deg_max_keys)
thus "deg_pm t ≤ poly_deg p"
by (simp add: t deg_pm_sum deg_pm_single deg_pm_superset[OF subset_refl])
qed
lemma poly_deg_map_indets:
assumes "inj_on f (indets p)"
shows "poly_deg (map_indets f p) = poly_deg p"
proof -
from assms have "deg_pm ` keys (map_indets f p) = deg_pm ` keys p"
by (simp add: keys_map_indets image_image deg_pm_sum deg_pm_single
flip: deg_pm_superset[OF subset_refl])
thus ?thesis by (auto simp: poly_deg_def)
qed
lemma map_indets_inj_on_PolysI:
assumes "inj_on (f::'x ⇒ 'y) X"
shows "inj_on ((map_indets f)::_ ⇒ _ ⇒⇩0 'a::comm_semiring_1) P[X]"
proof (rule inj_onI)
fix p q :: "_ ⇒⇩0 'a"
assume "p ∈ P[X]"
with assms have 1: "map_indets (the_inv_into X f) (map_indets f p) = p" (is "map_indets ?g _ = _")
by (rule map_indets_inverseE_Polys)
assume "q ∈ P[X]"
with assms have "map_indets ?g (map_indets f q) = q" by (rule map_indets_inverseE_Polys)
moreover assume "map_indets f p = map_indets f q"
ultimately show "p = q" using 1 by (simp add: map_indets_map_indets)
qed
lemma map_indets_injI:
assumes "inj f"
shows "inj (map_indets f)"
proof -
from assms have "inj_on (map_indets f) P[UNIV]" by (rule map_indets_inj_on_PolysI)
thus ?thesis by simp
qed
lemma image_map_indets_ideal:
assumes "inj f"
shows "map_indets f ` ideal F = ideal (map_indets f ` (F::(_ ⇒⇩0 'a::comm_ring_1) set)) ∩ P[range f]"
proof
from map_indets_plus map_indets_times have "map_indets f ` ideal F ⊆ ideal (map_indets f ` F)"
by (rule image_ideal_subset)
moreover from subset_UNIV have "map_indets f ` ideal F ⊆ range (map_indets f)" by (rule image_mono)
ultimately show "map_indets f ` ideal F ⊆ ideal (map_indets f ` F) ∩ P[range f]"
unfolding range_map_indets by blast
next
show "ideal (map_indets f ` F) ∩ P[range f] ⊆ map_indets f ` ideal F"
proof
fix p
assume "p ∈ ideal (map_indets f ` F) ∩ P[range f]"
hence "p ∈ ideal (map_indets f ` F)" and "p ∈ range (map_indets f)"
by (simp_all add: range_map_indets)
from this(1) obtain F0 q where "F0 ⊆ map_indets f ` F" and p: "p = (∑f'∈F0. q f' * f')"
by (rule ideal.spanE)
from this(1) obtain F' where "F' ⊆ F" and F0: "F0 = map_indets f ` F'" by (rule subset_imageE)
from assms obtain g where "map_indets g ∘ map_indets f = (id::_ ⇒ _ ⇒⇩0 'a)"
by (rule map_indets_inverseE)
hence eq: "map_indets g (map_indets f p') = p'" for p'::"_ ⇒⇩0 'a"
by (simp add: pointfree_idE)
from assms have "inj (map_indets f)" by (rule map_indets_injI)
from this subset_UNIV have "inj_on (map_indets f) F'" by (rule inj_on_subset)
from ‹p ∈ range _› obtain p' where "p = map_indets f p'" ..
hence "p = map_indets f (map_indets g p)" by (simp add: eq)
also from ‹inj_on _ F'› have "… = map_indets f (∑f'∈F'. map_indets g (q (map_indets f f')) * f')"
by (simp add: p F0 sum.reindex map_indets_sum map_indets_times eq)
finally have "p = map_indets f (∑f'∈F'. map_indets g (q (map_indets f f')) * f')" .
moreover have "(∑f'∈F'. map_indets g (q (map_indets f f')) * f') ∈ ideal F"
proof
show "(∑f'∈F'. map_indets g (q (map_indets f f')) * f') ∈ ideal F'" by (rule ideal.sum_in_spanI)
next
from ‹F' ⊆ F› show "ideal F' ⊆ ideal F" by (rule ideal.span_mono)
qed
ultimately show "p ∈ map_indets f ` ideal F" by (rule image_eqI)
qed
qed
subsection ‹Homogeneity›
definition homogeneous :: "(('x ⇒⇩0 nat) ⇒⇩0 'a::zero) ⇒ bool"
where "homogeneous p ⟷ (∀s∈keys p. ∀t∈keys p. deg_pm s = deg_pm t)"
definition hom_component :: "(('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ nat ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a::zero)"
where "hom_component p n = except p {t. deg_pm t ≠ n}"
definition hom_components :: "(('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a::zero) set"
where "hom_components p = hom_component p ` deg_pm ` keys p"
definition homogeneous_set :: "(('x ⇒⇩0 nat) ⇒⇩0 'a::zero) set ⇒ bool"
where "homogeneous_set A ⟷ (∀a∈A. ∀n. hom_component a n ∈ A)"
lemma homogeneousI: "(⋀s t. s ∈ keys p ⟹ t ∈ keys p ⟹ deg_pm s = deg_pm t) ⟹ homogeneous p"
unfolding homogeneous_def by blast
lemma homogeneousD: "homogeneous p ⟹ s ∈ keys p ⟹ t ∈ keys p ⟹ deg_pm s = deg_pm t"
unfolding homogeneous_def by blast
lemma homogeneousD_poly_deg:
assumes "homogeneous p" and "t ∈ keys p"
shows "deg_pm t = poly_deg p"
proof (rule antisym)
from assms(2) show "deg_pm t ≤ poly_deg p" by (rule poly_deg_max_keys)
next
show "poly_deg p ≤ deg_pm t"
proof (rule poly_deg_leI)
fix s
assume "s ∈ keys p"
with assms(1) have "deg_pm s = deg_pm t" using assms(2) by (rule homogeneousD)
thus "deg_pm s ≤ deg_pm t" by simp
qed
qed
lemma homogeneous_monomial [simp]: "homogeneous (monomial c t)"
by (auto split: if_split_asm intro: homogeneousI)
corollary homogeneous_zero [simp]: "homogeneous 0" and homogeneous_one [simp]: "homogeneous 1"
by (simp_all only: homogeneous_monomial flip: single_zero[of 0] single_one)
lemma homogeneous_uminus_iff [simp]: "homogeneous (- p) ⟷ homogeneous p"
by (auto intro!: homogeneousI dest: homogeneousD simp: keys_uminus)
lemma homogeneous_monom_mult: "homogeneous p ⟹ homogeneous (punit.monom_mult c t p)"
by (auto intro!: homogeneousI elim!: punit.keys_monom_multE simp: deg_pm_plus dest: homogeneousD)
lemma homogeneous_monom_mult_rev:
assumes "c ≠ (0::'a::semiring_no_zero_divisors)" and "homogeneous (punit.monom_mult c t p)"
shows "homogeneous p"
proof (rule homogeneousI)
fix s s'
assume "s ∈ keys p"
hence 1: "t + s ∈ keys (punit.monom_mult c t p)"
using assms(1) by (rule punit.keys_monom_multI[simplified])
assume "s' ∈ keys p"
hence "t + s' ∈ keys (punit.monom_mult c t p)"
using assms(1) by (rule punit.keys_monom_multI[simplified])
with assms(2) 1 have "deg_pm (t + s) = deg_pm (t + s')" by (rule homogeneousD)
thus "deg_pm s = deg_pm s'" by (simp add: deg_pm_plus)
qed
lemma homogeneous_times:
assumes "homogeneous p" and "homogeneous q"
shows "homogeneous (p * q)"
proof (rule homogeneousI)
fix s t
assume "s ∈ keys (p * q)"
then obtain sp sq where sp: "sp ∈ keys p" and sq: "sq ∈ keys q" and s: "s = sp + sq"
by (rule in_keys_timesE)
assume "t ∈ keys (p * q)"
then obtain tp tq where tp: "tp ∈ keys p" and tq: "tq ∈ keys q" and t: "t = tp + tq"
by (rule in_keys_timesE)
from assms(1) sp tp have "deg_pm sp = deg_pm tp" by (rule homogeneousD)
moreover from assms(2) sq tq have "deg_pm sq = deg_pm tq" by (rule homogeneousD)
ultimately show "deg_pm s = deg_pm t" by (simp only: s t deg_pm_plus)
qed
lemma lookup_hom_component: "lookup (hom_component p n) = (λt. lookup p t when deg_pm t = n)"
by (rule ext) (simp add: hom_component_def lookup_except)
lemma keys_hom_component: "keys (hom_component p n) = {t. t ∈ keys p ∧ deg_pm t = n}"
by (auto simp: hom_component_def keys_except)
lemma keys_hom_componentD:
assumes "t ∈ keys (hom_component p n)"
shows "t ∈ keys p" and "deg_pm t = n"
using assms by (simp_all add: keys_hom_component)
lemma homogeneous_hom_component: "homogeneous (hom_component p n)"
by (auto dest: keys_hom_componentD intro: homogeneousI)
lemma hom_component_zero [simp]: "hom_component 0 = 0"
by (rule ext) (simp add: hom_component_def)
lemma hom_component_zero_iff: "hom_component p n = 0 ⟷ (∀t∈keys p. deg_pm t ≠ n)"
by (metis (mono_tags, lifting) empty_iff keys_eq_empty_iff keys_hom_component mem_Collect_eq subsetI subset_antisym)
lemma hom_component_uminus [simp]: "hom_component (- p) = - hom_component p"
by (intro ext poly_mapping_eqI) (simp add: hom_component_def lookup_except)
lemma hom_component_plus: "hom_component (p + q) n = hom_component p n + hom_component q n"
by (rule poly_mapping_eqI) (simp add: hom_component_def lookup_except lookup_add)
lemma hom_component_minus: "hom_component (p - q) n = hom_component p n - hom_component q n"
by (rule poly_mapping_eqI) (simp add: hom_component_def lookup_except lookup_minus)
lemma hom_component_monom_mult:
"punit.monom_mult c t (hom_component p n) = hom_component (punit.monom_mult c t p) (deg_pm t + n)"
by (auto simp: hom_component_def lookup_except punit.lookup_monom_mult deg_pm_minus deg_pm_mono intro!: poly_mapping_eqI)
lemma hom_component_inject:
assumes "t ∈ keys p" and "hom_component p (deg_pm t) = hom_component p n"
shows "deg_pm t = n"
proof -
from assms(1) have "t ∈ keys (hom_component p (deg_pm t))" by (simp add: keys_hom_component)
hence "0 ≠ lookup (hom_component p (deg_pm t)) t" by (simp add: in_keys_iff)
also have "lookup (hom_component p (deg_pm t)) t = lookup (hom_component p n) t"
by (simp only: assms(2))
also have "… = (lookup p t when deg_pm t = n)" by (simp only: lookup_hom_component)
finally show ?thesis by simp
qed
lemma hom_component_of_homogeneous:
assumes "homogeneous p"
shows "hom_component p n = (p when n = poly_deg p)"
proof (cases "n = poly_deg p")
case True
have "hom_component p n = p"
proof (rule poly_mapping_eqI)
fix t
show "lookup (hom_component p n) t = lookup p t"
proof (cases "t ∈ keys p")
case True
with assms have "deg_pm t = n" unfolding ‹n = poly_deg p› by (rule homogeneousD_poly_deg)
thus ?thesis by (simp add: lookup_hom_component)
next
case False
moreover from this have "t ∉ keys (hom_component p n)" by (simp add: keys_hom_component)
ultimately show ?thesis by (simp add: in_keys_iff)
qed
qed
with True show ?thesis by simp
next
case False
have "hom_component p n = 0" unfolding hom_component_zero_iff
proof (intro ballI notI)
fix t
assume "t ∈ keys p"
with assms have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
moreover assume "deg_pm t = n"
ultimately show False using False by simp
qed
with False show ?thesis by simp
qed
lemma hom_components_zero [simp]: "hom_components 0 = {}"
by (simp add: hom_components_def)
lemma hom_components_zero_iff [simp]: "hom_components p = {} ⟷ p = 0"
by (simp add: hom_components_def)
lemma hom_components_uminus: "hom_components (- p) = uminus ` hom_components p"
by (simp add: hom_components_def keys_uminus image_image)
lemma hom_components_monom_mult:
"hom_components (punit.monom_mult c t p) = (if c = 0 then {} else punit.monom_mult c t ` hom_components p)"
for c::"'a::semiring_no_zero_divisors"
by (simp add: hom_components_def punit.keys_monom_mult image_image deg_pm_plus hom_component_monom_mult)
lemma hom_componentsI: "q = hom_component p (deg_pm t) ⟹ t ∈ keys p ⟹ q ∈ hom_components p"
unfolding hom_components_def by blast
lemma hom_componentsE:
assumes "q ∈ hom_components p"
obtains t where "t ∈ keys p" and "q = hom_component p (deg_pm t)"
using assms unfolding hom_components_def by blast
lemma hom_components_of_homogeneous:
assumes "homogeneous p"
shows "hom_components p = (if p = 0 then {} else {p})"
proof (split if_split, intro conjI impI)
assume "p ≠ 0"
have "deg_pm ` keys p = {poly_deg p}"
proof (rule set_eqI)
fix n
have "n ∈ deg_pm ` keys p ⟷ n = poly_deg p"
proof
assume "n ∈ deg_pm ` keys p"
then obtain t where "t ∈ keys p" and "n = deg_pm t" ..
from assms this(1) have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
thus "n = poly_deg p" by (simp only: ‹n = deg_pm t›)
next
assume "n = poly_deg p"
from ‹p ≠ 0› have "keys p ≠ {}" by simp
then obtain t where "t ∈ keys p" by blast
with assms have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
hence "n = deg_pm t" by (simp only: ‹n = poly_deg p›)
with ‹t ∈ keys p› show "n ∈ deg_pm ` keys p" by (rule rev_image_eqI)
qed
thus "n ∈ deg_pm ` keys p ⟷ n ∈ {poly_deg p}" by simp
qed
with assms show "hom_components p = {p}"
by (simp add: hom_components_def hom_component_of_homogeneous)
qed simp
lemma finite_hom_components: "finite (hom_components p)"
unfolding hom_components_def using finite_keys by (intro finite_imageI)
lemma hom_components_homogeneous: "q ∈ hom_components p ⟹ homogeneous q"
by (elim hom_componentsE) (simp only: homogeneous_hom_component)
lemma hom_components_nonzero: "q ∈ hom_components p ⟹ q ≠ 0"
by (auto elim!: hom_componentsE simp: hom_component_zero_iff)
lemma deg_pm_hom_components:
assumes "q1 ∈ hom_components p" and "q2 ∈ hom_components p" and "t1 ∈ keys q1" and "t2 ∈ keys q2"
shows "deg_pm t1 = deg_pm t2 ⟷ q1 = q2"
proof -
from assms(1) obtain s1 where "s1 ∈ keys p" and q1: "q1 = hom_component p (deg_pm s1)"
by (rule hom_componentsE)
from assms(3) have t1: "deg_pm t1 = deg_pm s1" unfolding q1 by (rule keys_hom_componentD)
from assms(2) obtain s2 where "s2 ∈ keys p" and q2: "q2 = hom_component p (deg_pm s2)"
by (rule hom_componentsE)
from assms(4) have t2: "deg_pm t2 = deg_pm s2" unfolding q2 by (rule keys_hom_componentD)
from ‹s1 ∈ keys p› show ?thesis by (auto simp: q1 q2 t1 t2 dest: hom_component_inject)
qed
lemma poly_deg_hom_components:
assumes "q1 ∈ hom_components p" and "q2 ∈ hom_components p"
shows "poly_deg q1 = poly_deg q2 ⟷ q1 = q2"
proof -
from assms(1) have "homogeneous q1" and "q1 ≠ 0"
by (rule hom_components_homogeneous, rule hom_components_nonzero)
from this(2) have "keys q1 ≠ {}" by simp
then obtain t1 where "t1 ∈ keys q1" by blast
with ‹homogeneous q1› have t1: "deg_pm t1 = poly_deg q1" by (rule homogeneousD_poly_deg)
from assms(2) have "homogeneous q2" and "q2 ≠ 0"
by (rule hom_components_homogeneous, rule hom_components_nonzero)
from this(2) have "keys q2 ≠ {}" by simp
then obtain t2 where "t2 ∈ keys q2" by blast
with ‹homogeneous q2› have t2: "deg_pm t2 = poly_deg q2" by (rule homogeneousD_poly_deg)
from assms ‹t1 ∈ keys q1› ‹t2 ∈ keys q2› have "deg_pm t1 = deg_pm t2 ⟷ q1 = q2"
by (rule deg_pm_hom_components)
thus ?thesis by (simp only: t1 t2)
qed
lemma hom_components_keys_disjoint:
assumes "q1 ∈ hom_components p" and "q2 ∈ hom_components p" and "q1 ≠ q2"
shows "keys q1 ∩ keys q2 = {}"
proof (rule ccontr)
assume "keys q1 ∩ keys q2 ≠ {}"
then obtain t where "t ∈ keys q1" and "t ∈ keys q2" by blast
with assms(1, 2) have "deg_pm t = deg_pm t ⟷ q1 = q2" by (rule deg_pm_hom_components)
with assms(3) show False by simp
qed
lemma Keys_hom_components: "Keys (hom_components p) = keys p"
by (auto simp: Keys_def hom_components_def keys_hom_component)
lemma lookup_hom_components: "q ∈ hom_components p ⟹ t ∈ keys q ⟹ lookup q t = lookup p t"
by (auto elim!: hom_componentsE simp: keys_hom_component lookup_hom_component)
lemma poly_deg_hom_components_le:
assumes "q ∈ hom_components p"
shows "poly_deg q ≤ poly_deg p"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys q"
also from assms have "… ⊆ Keys (hom_components p)" by (rule keys_subset_Keys)
also have "… = keys p" by (fact Keys_hom_components)
finally show "deg_pm t ≤ poly_deg p" by (rule poly_deg_max_keys)
qed
lemma sum_hom_components: "∑(hom_components p) = p"
proof (rule poly_mapping_eqI)
fix t
show "lookup (∑(hom_components p)) t = lookup p t" unfolding lookup_sum
proof (cases "t ∈ keys p")
case True
also have "keys p = Keys (hom_components p)" by (simp only: Keys_hom_components)
finally obtain q where q: "q ∈ hom_components p" and t: "t ∈ keys q" by (rule in_KeysE)
from this(1) have "(∑q0∈hom_components p. lookup q0 t) =
(∑q0∈insert q (hom_components p). lookup q0 t)"
by (simp only: insert_absorb)
also from finite_hom_components have "… = lookup q t + (∑q0∈hom_components p - {q}. lookup q0 t)"
by (rule sum.insert_remove)
also from q t have "… = lookup p t + (∑q0∈hom_components p - {q}. lookup q0 t)"
by (simp only: lookup_hom_components)
also have "(∑q0∈hom_components p - {q}. lookup q0 t) = 0"
proof (intro sum.neutral ballI)
fix q0
assume "q0 ∈ hom_components p - {q}"
hence "q0 ∈ hom_components p" and "q ≠ q0" by blast+
with q have "keys q ∩ keys q0 = {}" by (rule hom_components_keys_disjoint)
with t have "t ∉ keys q0" by blast
thus "lookup q0 t = 0" by (simp add: in_keys_iff)
qed
finally show "(∑q∈hom_components p. lookup q t) = lookup p t" by simp
next
case False
hence "t ∉ Keys (hom_components p)" by (simp add: Keys_hom_components)
hence "∀q∈hom_components p. lookup q t = 0" by (simp add: Keys_def in_keys_iff)
hence "(∑q∈hom_components p. lookup q t) = 0" by (rule sum.neutral)
also from False have "… = lookup p t" by (simp add: in_keys_iff)
finally show "(∑q∈hom_components p. lookup q t) = lookup p t" .
qed
qed
lemma homogeneous_setI: "(⋀a n. a ∈ A ⟹ hom_component a n ∈ A) ⟹ homogeneous_set A"
by (simp add: homogeneous_set_def)
lemma homogeneous_setD: "homogeneous_set A ⟹ a ∈ A ⟹ hom_component a n ∈ A"
by (simp add: homogeneous_set_def)
lemma homogeneous_set_Polys: "homogeneous_set (P[X]::(_ ⇒⇩0 'a::zero) set)"
proof (intro homogeneous_setI PolysI subsetI)
fix p::"_ ⇒⇩0 'a" and n t
assume "p ∈ P[X]"
assume "t ∈ keys (hom_component p n)"
hence "t ∈ keys p" by (rule keys_hom_componentD)
also from ‹p ∈ P[X]› have "… ⊆ .[X]" by (rule PolysD)
finally show "t ∈ .[X]" .
qed
lemma homogeneous_set_IntI: "homogeneous_set A ⟹ homogeneous_set B ⟹ homogeneous_set (A ∩ B)"
by (simp add: homogeneous_set_def)
lemma homogeneous_setD_hom_components:
assumes "homogeneous_set A" and "a ∈ A" and "b ∈ hom_components a"
shows "b ∈ A"
proof -
from assms(3) obtain t::"'a ⇒⇩0 nat" where "b = hom_component a (deg_pm t)"
by (rule hom_componentsE)
also from assms(1, 2) have "… ∈ A" by (rule homogeneous_setD)
finally show ?thesis .
qed
lemma zero_in_homogeneous_set:
assumes "homogeneous_set A" and "A ≠ {}"
shows "0 ∈ A"
proof -
from assms(2) obtain a where "a ∈ A" by blast
have "lookup a t = 0" if "deg_pm t = Suc (poly_deg a)" for t
proof (rule ccontr)
assume "lookup a t ≠ 0"
hence "t ∈ keys a" by (simp add: in_keys_iff)
hence "deg_pm t ≤ poly_deg a" by (rule poly_deg_max_keys)
thus False by (simp add: that)
qed
hence "0 = hom_component a (Suc (poly_deg a))"
by (intro poly_mapping_eqI) (simp add: lookup_hom_component when_def)
also from assms(1) ‹a ∈ A› have "… ∈ A" by (rule homogeneous_setD)
finally show ?thesis .
qed
lemma homogeneous_ideal:
assumes "⋀f. f ∈ F ⟹ homogeneous f" and "p ∈ ideal F"
shows "hom_component p n ∈ ideal F"
proof -
from assms(2) have "p ∈ punit.pmdl F" by simp
thus ?thesis
proof (induct p rule: punit.pmdl_induct)
case module_0
show ?case by (simp add: ideal.span_zero)
next
case (module_plus a f c t)
let ?f = "punit.monom_mult c t f"
from module_plus.hyps(3) have "f ∈ punit.pmdl F" by (simp add: ideal.span_base)
hence *: "?f ∈ punit.pmdl F" by (rule punit.pmdl_closed_monom_mult)
from module_plus.hyps(3) have "homogeneous f" by (rule assms(1))
hence "homogeneous ?f" by (rule homogeneous_monom_mult)
hence "hom_component ?f n = (?f when n = poly_deg ?f)" by (rule hom_component_of_homogeneous)
also from * have "… ∈ ideal F" by (simp add: when_def ideal.span_zero)
finally have "hom_component ?f n ∈ ideal F" .
with module_plus.hyps(2) show ?case unfolding hom_component_plus by (rule ideal.span_add)
qed
qed
corollary homogeneous_set_homogeneous_ideal:
"(⋀f. f ∈ F ⟹ homogeneous f) ⟹ homogeneous_set (ideal F)"
by (auto intro: homogeneous_setI homogeneous_ideal)
corollary homogeneous_ideal':
assumes "⋀f. f ∈ F ⟹ homogeneous f" and "p ∈ ideal F" and "q ∈ hom_components p"
shows "q ∈ ideal F"
using _ assms(2, 3)
proof (rule homogeneous_setD_hom_components)
from assms(1) show "homogeneous_set (ideal F)" by (rule homogeneous_set_homogeneous_ideal)
qed
lemma homogeneous_idealE_homogeneous:
assumes "⋀f. f ∈ F ⟹ homogeneous f" and "p ∈ ideal F" and "homogeneous p"
obtains F' q where "finite F'" and "F' ⊆ F" and "p = (∑f∈F'. q f * f)" and "⋀f. homogeneous (q f)"
and "⋀f. f ∈ F' ⟹ poly_deg (q f * f) = poly_deg p" and "⋀f. f ∉ F' ⟹ q f = 0"
proof -
from assms(2) obtain F'' q' where "finite F''" and "F'' ⊆ F" and p: "p = (∑f∈F''. q' f * f)"
by (rule ideal.spanE)
let ?A = "λf. {h ∈ hom_components (q' f). poly_deg h + poly_deg f = poly_deg p}"
let ?B = "λf. {h ∈ hom_components (q' f). poly_deg h + poly_deg f ≠ poly_deg p}"
define F' where "F' = {f ∈ F''. (∑(?A f)) * f ≠ 0}"
define q where "q = (λf. (∑(?A f)) when f ∈ F')"
have "F' ⊆ F''" by (simp add: F'_def)
hence "F' ⊆ F" using ‹F'' ⊆ F› by (rule subset_trans)
have 1: "deg_pm t + poly_deg f = poly_deg p" if "f ∈ F'" and "t ∈ keys (q f)" for f t
proof -
from that have "t ∈ keys (∑(?A f))" by (simp add: q_def)
also have "… ⊆ (⋃h∈?A f. keys h)" by (fact keys_sum_subset)
finally obtain h where "h ∈ ?A f" and "t ∈ keys h" ..
from this(1) have "h ∈ hom_components (q' f)" and eq: "poly_deg h + poly_deg f = poly_deg p"
by simp_all
from this(1) have "homogeneous h" by (rule hom_components_homogeneous)
hence "deg_pm t = poly_deg h" using ‹t ∈ keys h› by (rule homogeneousD_poly_deg)
thus ?thesis by (simp only: eq)
qed
have 2: "deg_pm t = poly_deg p" if "f ∈ F'" and "t ∈ keys (q f * f)" for f t
proof -
from that(1) ‹F' ⊆ F› have "f ∈ F" ..
hence "homogeneous f" by (rule assms(1))
from that(2) obtain s1 s2 where "s1 ∈ keys (q f)" and "s2 ∈ keys f" and t: "t = s1 + s2"
by (rule in_keys_timesE)
from that(1) this(1) have "deg_pm s1 + poly_deg f = poly_deg p" by (rule 1)
moreover from ‹homogeneous f› ‹s2 ∈ keys f› have "deg_pm s2 = poly_deg f"
by (rule homogeneousD_poly_deg)
ultimately show ?thesis by (simp add: t deg_pm_plus)
qed
from ‹F' ⊆ F''› ‹finite F''› have "finite F'" by (rule finite_subset)
thus ?thesis using ‹F' ⊆ F›
proof
note p
also from refl have "(∑f∈F''. q' f * f) = (∑f∈F''. (∑(?A f) * f) + (∑(?B f) * f))"
proof (rule sum.cong)
fix f
assume "f ∈ F''"
from sum_hom_components have "q' f = (∑(hom_components (q' f)))" by (rule sym)
also have "… = (∑(?A f ∪ ?B f))" by (rule arg_cong[where f="sum (λx. x)"]) blast
also have "… = ∑(?A f) + ∑(?B f)"
proof (rule sum.union_disjoint)
have "?A f ⊆ hom_components (q' f)" by blast
thus "finite (?A f)" using finite_hom_components by (rule finite_subset)
next
have "?B f ⊆ hom_components (q' f)" by blast
thus "finite (?B f)" using finite_hom_components by (rule finite_subset)
qed blast
finally show "q' f * f = (∑(?A f) * f) + (∑(?B f) * f)"
by (metis (no_types, lifting) distrib_right)
qed
also have "… = (∑f∈F''. ∑(?A f) * f) + (∑f∈F''. ∑(?B f) * f)" by (rule sum.distrib)
also from ‹finite F''› ‹F' ⊆ F''› have "(∑f∈F''. ∑(?A f) * f) = (∑f∈F'. q f * f)"
proof (intro sum.mono_neutral_cong_right ballI)
fix f
assume "f ∈ F'' - F'"
thus "∑(?A f) * f = 0" by (simp add: F'_def)
next
fix f
assume "f ∈ F'"
thus "∑(?A f) * f = q f * f" by (simp add: q_def)
qed
finally have p[symmetric]: "p = (∑f∈F'. q f * f) + (∑f∈F''. ∑(?B f) * f)" .
moreover have "keys (∑f∈F''. ∑(?B f) * f) = {}"
proof (rule, rule)
fix t
assume t_in: "t ∈ keys (∑f∈F''. ∑(?B f) * f)"
also have "… ⊆ (⋃f∈F''. keys (∑(?B f) * f))" by (fact keys_sum_subset)
finally obtain f where "f ∈ F''" and "t ∈ keys (∑(?B f) * f)" ..
from this(2) obtain s1 s2 where "s1 ∈ keys (∑(?B f))" and "s2 ∈ keys f" and t: "t = s1 + s2"
by (rule in_keys_timesE)
from ‹f ∈ F''› ‹F'' ⊆ F› have "f ∈ F" ..
hence "homogeneous f" by (rule assms(1))
note ‹s1 ∈ keys (∑(?B f))›
also have "keys (∑(?B f)) ⊆ (⋃h∈?B f. keys h)" by (fact keys_sum_subset)
finally obtain h where "h ∈ ?B f" and "s1 ∈ keys h" ..
from this(1) have "h ∈ hom_components (q' f)" and neq: "poly_deg h + poly_deg f ≠ poly_deg p"
by simp_all
from this(1) have "homogeneous h" by (rule hom_components_homogeneous)
hence "deg_pm s1 = poly_deg h" using ‹s1 ∈ keys h› by (rule homogeneousD_poly_deg)
moreover from ‹homogeneous f› ‹s2 ∈ keys f› have "deg_pm s2 = poly_deg f"
by (rule homogeneousD_poly_deg)
ultimately have "deg_pm t ≠ poly_deg p" using neq by (simp add: t deg_pm_plus)
have "t ∉ keys (∑f∈F'. q f * f)"
proof
assume "t ∈ keys (∑f∈F'. q f * f)"
also have "… ⊆ (⋃f∈F'. keys (q f * f))" by (fact keys_sum_subset)
finally obtain f where "f ∈ F'" and "t ∈ keys (q f * f)" ..
hence "deg_pm t = poly_deg p" by (rule 2)
with ‹deg_pm t ≠ poly_deg p› show False ..
qed
with t_in have "t ∈ keys ((∑f∈F'. q f * f) + (∑f∈F''. ∑(?B f) * f))"
by (rule in_keys_plusI2)
hence "t ∈ keys p" by (simp only: p)
with assms(3) have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
with ‹deg_pm t ≠ poly_deg p› show "t ∈ {}" ..
qed (fact empty_subsetI)
ultimately show "p = (∑f∈F'. q f * f)" by simp
next
fix f
show "homogeneous (q f)"
proof (cases "f ∈ F'")
case True
show ?thesis
proof (rule homogeneousI)
fix s t
assume "s ∈ keys (q f)"
with True have *: "deg_pm s + poly_deg f = poly_deg p" by (rule 1)
assume "t ∈ keys (q f)"
with True have "deg_pm t + poly_deg f = poly_deg p" by (rule 1)
with * show "deg_pm s = deg_pm t" by simp
qed
next
case False
thus ?thesis by (simp add: q_def)
qed
assume "f ∈ F'"
show "poly_deg (q f * f) = poly_deg p"
proof (intro antisym)
show "poly_deg (q f * f) ≤ poly_deg p"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys (q f * f)"
with ‹f ∈ F'› have "deg_pm t = poly_deg p" by (rule 2)
thus "deg_pm t ≤ poly_deg p" by simp
qed
next
from ‹f ∈ F'› have "q f * f ≠ 0" by (simp add: q_def F'_def)
hence "keys (q f * f) ≠ {}" by simp
then obtain t where "t ∈ keys (q f * f)" by blast
with ‹f ∈ F'› have "deg_pm t = poly_deg p" by (rule 2)
moreover from ‹t ∈ keys (q f * f)› have "deg_pm t ≤ poly_deg (q f * f)" by (rule poly_deg_max_keys)
ultimately show "poly_deg p ≤ poly_deg (q f * f)" by simp
qed
qed (simp add: q_def)
qed
corollary homogeneous_idealE:
assumes "⋀f. f ∈ F ⟹ homogeneous f" and "p ∈ ideal F"
obtains F' q where "finite F'" and "F' ⊆ F" and "p = (∑f∈F'. q f * f)"
and "⋀f. poly_deg (q f * f) ≤ poly_deg p" and "⋀f. f ∉ F' ⟹ q f = 0"
proof (cases "p = 0")
case True
show ?thesis
proof
show "p = (∑f∈{}. (λ_. 0) f * f)" by (simp add: True)
qed simp_all
next
case False
define P where "P = (λh qf. finite (fst qf) ∧ fst qf ⊆ F ∧ h = (∑f∈fst qf. snd qf f * f) ∧
(∀f∈fst qf. poly_deg (snd qf f * f) = poly_deg h) ∧ (∀f. f ∉ fst qf ⟶ snd qf f = 0))"
define q0 where "q0 = (λh. SOME qf. P h qf)"
have 1: "P h (q0 h)" if "h ∈ hom_components p" for h
proof -
note assms(1)
moreover from assms that have "h ∈ ideal F" by (rule homogeneous_ideal')
moreover from that have "homogeneous h" by (rule hom_components_homogeneous)
ultimately obtain F' q where "finite F'" and "F' ⊆ F" and "h = (∑f∈F'. q f * f)"
and "⋀f. f ∈ F' ⟹ poly_deg (q f * f) = poly_deg h" and "⋀f. f ∉ F' ⟹ q f = 0"
by (rule homogeneous_idealE_homogeneous) blast+
hence "P h (F', q)" by (simp add: P_def)
thus ?thesis unfolding q0_def by (rule someI)
qed
define F' where "F' = (⋃h∈hom_components p. fst (q0 h))"
define q where "q = (λf. ∑h∈hom_components p. snd (q0 h) f)"
show ?thesis
proof
have "finite F' ∧ F' ⊆ F" unfolding F'_def UN_subset_iff finite_UN[OF finite_hom_components]
proof (intro conjI ballI)
fix h
assume "h ∈ hom_components p"
hence "P h (q0 h)" by (rule 1)
thus "finite (fst (q0 h))" and "fst (q0 h) ⊆ F" by (simp_all only: P_def)
qed
thus "finite F'" and "F' ⊆ F" by simp_all
from sum_hom_components have "p = (∑(hom_components p))" by (rule sym)
also from refl have "… = (∑h∈hom_components p. ∑f∈F'. snd (q0 h) f * f)"
proof (rule sum.cong)
fix h
assume "h ∈ hom_components p"
hence "P h (q0 h)" by (rule 1)
hence "h = (∑f∈fst (q0 h). snd (q0 h) f * f)" and 2: "⋀f. f ∉ fst (q0 h) ⟹ snd (q0 h) f = 0"
by (simp_all add: P_def)
note this(1)
also from ‹finite F'› have "(∑f∈fst (q0 h). (snd (q0 h)) f * f) = (∑f∈F'. snd (q0 h) f * f)"
proof (intro sum.mono_neutral_left ballI)
show "fst (q0 h) ⊆ F'" unfolding F'_def using ‹h ∈ hom_components p› by blast
next
fix f
assume "f ∈ F' - fst (q0 h)"
hence "f ∉ fst (q0 h)" by simp
hence "snd (q0 h) f = 0" by (rule 2)
thus "snd (q0 h) f * f = 0" by simp
qed
finally show "h = (∑f∈F'. snd (q0 h) f * f)" .
qed
also have "… = (∑f∈F'. ∑h∈hom_components p. snd (q0 h) f * f)" by (rule sum.swap)
also have "… = (∑f∈F'. q f * f)" by (simp only: q_def sum_distrib_right)
finally show "p = (∑f∈F'. q f * f)" .
fix f
have "poly_deg (q f * f) = poly_deg (∑h∈hom_components p. snd (q0 h) f * f)"
by (simp only: q_def sum_distrib_right)
also have "… ≤ Max (poly_deg ` (λh. snd (q0 h) f * f) ` hom_components p)"
by (rule poly_deg_sum_le)
also have "… = Max ((λh. poly_deg (snd (q0 h) f * f)) ` hom_components p)"
(is "_ = Max (?f ` _)") by (simp only: image_image)
also have "… ≤ poly_deg p"
proof (rule Max.boundedI)
from finite_hom_components show "finite (?f ` hom_components p)" by (rule finite_imageI)
next
from False show "?f ` hom_components p ≠ {}" by simp
next
fix d
assume "d ∈ ?f ` hom_components p"
then obtain h where "h ∈ hom_components p" and d: "d = ?f h" ..
from this(1) have "P h (q0 h)" by (rule 1)
hence 2: "⋀f. f ∈ fst (q0 h) ⟹ poly_deg (snd (q0 h) f * f) = poly_deg h"
and 3: "⋀f. f ∉ fst (q0 h) ⟹ snd (q0 h) f = 0" by (simp_all add: P_def)
show "d ≤ poly_deg p"
proof (cases "f ∈ fst (q0 h)")
case True
hence "poly_deg (snd (q0 h) f * f) = poly_deg h" by (rule 2)
hence "d = poly_deg h" by (simp only: d)
also from ‹h ∈ hom_components p› have "… ≤ poly_deg p" by (rule poly_deg_hom_components_le)
finally show ?thesis .
next
case False
hence "snd (q0 h) f = 0" by (rule 3)
thus ?thesis by (simp add: d)
qed
qed
finally show "poly_deg (q f * f) ≤ poly_deg p" .
assume "f ∉ F'"
show "q f = 0" unfolding q_def
proof (intro sum.neutral ballI)
fix h
assume "h ∈ hom_components p"
hence "P h (q0 h)" by (rule 1)
hence 2: "⋀f. f ∉ fst (q0 h) ⟹ snd (q0 h) f = 0" by (simp add: P_def)
show "snd (q0 h) f = 0"
proof (intro 2 notI)
assume "f ∈ fst (q0 h)"
hence "f ∈ F'" unfolding F'_def using ‹h ∈ hom_components p› by blast
with ‹f ∉ F'› show False ..
qed
qed
qed
qed
corollary homogeneous_idealE_finite:
assumes "finite F" and "⋀f. f ∈ F ⟹ homogeneous f" and "p ∈ ideal F"
obtains q where "p = (∑f∈F. q f * f)" and "⋀f. poly_deg (q f * f) ≤ poly_deg p"
and "⋀f. f ∉ F ⟹ q f = 0"
proof -
from assms(2, 3) obtain F' q where "F' ⊆ F" and p: "p = (∑f∈F'. q f * f)"
and "⋀f. poly_deg (q f * f) ≤ poly_deg p" and 1: "⋀f. f ∉ F' ⟹ q f = 0"
by (rule homogeneous_idealE) blast+
show ?thesis
proof
from assms(1) ‹F' ⊆ F› have "(∑f∈F'. q f * f) = (∑f∈F. q f * f)"
proof (intro sum.mono_neutral_left ballI)
fix f
assume "f ∈ F - F'"
hence "f ∉ F'" by simp
hence "q f = 0" by (rule 1)
thus "q f * f = 0" by simp
qed
thus "p = (∑f∈F. q f * f)" by (simp only: p)
next
fix f
show "poly_deg (q f * f) ≤ poly_deg p" by fact
assume "f ∉ F"
with ‹F' ⊆ F› have "f ∉ F'" by blast
thus "q f = 0" by (rule 1)
qed
qed
subsubsection ‹Homogenization and Dehomogenization›
definition homogenize :: "'x ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a::semiring_1)"
where "homogenize x p = (∑t∈keys p. monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"
definition dehomo_subst :: "'x ⇒ 'x ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a::zero_neq_one)"
where "dehomo_subst x = (λy. if y = x then 1 else monomial 1 (Poly_Mapping.single y 1))"
definition dehomogenize :: "'x ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a::comm_semiring_1)"
where "dehomogenize x = poly_subst (dehomo_subst x)"
lemma homogenize_zero [simp]: "homogenize x 0 = 0"
by (simp add: homogenize_def)
lemma homogenize_uminus [simp]: "homogenize x (- p) = - homogenize x (p::_ ⇒⇩0 'a::ring_1)"
by (simp add: homogenize_def keys_uminus sum.reindex inj_on_def single_uminus sum_negf)
lemma homogenize_monom_mult [simp]:
"homogenize x (punit.monom_mult c t p) = punit.monom_mult c t (homogenize x p)"
for c::"'a::{semiring_1,semiring_no_zero_divisors_cancel}"
proof (cases "p = 0")
case True
thus ?thesis by simp
next
case False
show ?thesis
proof (cases "c = 0")
case True
thus ?thesis by simp
next
case False
show ?thesis
by (simp add: homogenize_def punit.keys_monom_mult ‹p ≠ 0› False sum.reindex
punit.lookup_monom_mult punit.monom_mult_sum_right poly_deg_monom_mult
punit.monom_mult_monomial ac_simps deg_pm_plus)
qed
qed
lemma homogenize_alt:
"homogenize x p = (∑q∈hom_components p. punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q)"
proof -
have "homogenize x p = (∑t∈Keys (hom_components p). monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"
by (simp only: homogenize_def Keys_hom_components)
also have "… = (∑t∈(⋃ (keys ` hom_components p)). monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"
by (simp only: Keys_def)
also have "… = (∑q∈hom_components p. (∑t∈keys q. monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)))"
by (auto intro!: sum.UNION_disjoint finite_hom_components finite_keys dest: hom_components_keys_disjoint)
also have "… = (∑q∈hom_components p. punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q)"
using refl
proof (rule sum.cong)
fix q
assume q: "q ∈ hom_components p"
hence "homogeneous q" by (rule hom_components_homogeneous)
have "(∑t∈keys q. monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)) =
(∑t∈keys q. punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) (monomial (lookup q t) t))"
using refl
proof (rule sum.cong)
fix t
assume "t ∈ keys q"
with ‹homogeneous q› have "deg_pm t = poly_deg q" by (rule homogeneousD_poly_deg)
moreover from q ‹t ∈ keys q› have "lookup q t = lookup p t" by (rule lookup_hom_components)
ultimately show "monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t) =
punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) (monomial (lookup q t) t)"
by (simp add: punit.monom_mult_monomial)
qed
also have "… = punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q"
by (simp only: poly_mapping_sum_monomials flip: punit.monom_mult_sum_right)
finally show "(∑t∈keys q. monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)) =
punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q" .
qed
finally show ?thesis .
qed
lemma keys_homogenizeE:
assumes "t ∈ keys (homogenize x p)"
obtains t' where "t' ∈ keys p" and "t = Poly_Mapping.single x (poly_deg p - deg_pm t') + t'"
proof -
note assms
also have "keys (homogenize x p) ⊆
(⋃t∈keys p. keys (monomial (lookup p t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)))"
unfolding homogenize_def by (rule keys_sum_subset)
finally obtain t' where "t' ∈ keys p"
and "t ∈ keys (monomial (lookup p t') (Poly_Mapping.single x (poly_deg p - deg_pm t') + t'))" ..
from this(2) have "t = Poly_Mapping.single x (poly_deg p - deg_pm t') + t'"
by (simp split: if_split_asm)
with ‹t' ∈ keys p› show ?thesis ..
qed
lemma keys_homogenizeE_alt:
assumes "t ∈ keys (homogenize x p)"
obtains q t' where "q ∈ hom_components p" and "t' ∈ keys q"
and "t = Poly_Mapping.single x (poly_deg p - poly_deg q) + t'"
proof -
note assms
also have "keys (homogenize x p) ⊆
(⋃q∈hom_components p. keys (punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q))"
unfolding homogenize_alt by (rule keys_sum_subset)
finally obtain q where q: "q ∈ hom_components p"
and "t ∈ keys (punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q)" ..
note this(2)
also have "… ⊆ (+) (Poly_Mapping.single x (poly_deg p - poly_deg q)) ` keys q"
by (rule punit.keys_monom_mult_subset[simplified])
finally obtain t' where "t' ∈ keys q" and "t = Poly_Mapping.single x (poly_deg p - poly_deg q) + t'" ..
with q show ?thesis ..
qed
lemma deg_pm_homogenize:
assumes "t ∈ keys (homogenize x p)"
shows "deg_pm t = poly_deg p"
proof -
from assms obtain q t' where q: "q ∈ hom_components p" and "t' ∈ keys q"
and t: "t = Poly_Mapping.single x (poly_deg p - poly_deg q) + t'" by (rule keys_homogenizeE_alt)
from q have "homogeneous q" by (rule hom_components_homogeneous)
hence "deg_pm t' = poly_deg q" using ‹t' ∈ keys q› by (rule homogeneousD_poly_deg)
moreover from q have "poly_deg q ≤ poly_deg p" by (rule poly_deg_hom_components_le)
ultimately show ?thesis by (simp add: t deg_pm_plus deg_pm_single)
qed
corollary homogeneous_homogenize: "homogeneous (homogenize x p)"
proof (rule homogeneousI)
fix s t
assume "s ∈ keys (homogenize x p)"
hence *: "deg_pm s = poly_deg p" by (rule deg_pm_homogenize)
assume "t ∈ keys (homogenize x p)"
hence "deg_pm t = poly_deg p" by (rule deg_pm_homogenize)
with * show "deg_pm s = deg_pm t" by simp
qed
corollary poly_deg_homogenize_le: "poly_deg (homogenize x p) ≤ poly_deg p"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys (homogenize x p)"
hence "deg_pm t = poly_deg p" by (rule deg_pm_homogenize)
thus "deg_pm t ≤ poly_deg p" by simp
qed
lemma homogenize_id_iff [simp]: "homogenize x p = p ⟷ homogeneous p"
proof
assume "homogenize x p = p"
moreover have "homogeneous (homogenize x p)" by (fact homogeneous_homogenize)
ultimately show "homogeneous p" by simp
next
assume "homogeneous p"
hence "hom_components p = (if p = 0 then {} else {p})" by (rule hom_components_of_homogeneous)
thus "homogenize x p = p" by (simp add: homogenize_alt split: if_split_asm)
qed
lemma homogenize_homogenize [simp]: "homogenize x (homogenize x p) = homogenize x p"
by (simp add: homogeneous_homogenize)
lemma homogenize_monomial: "homogenize x (monomial c t) = monomial c t"
by (simp only: homogenize_id_iff homogeneous_monomial)
lemma indets_homogenize_subset: "indets (homogenize x p) ⊆ insert x (indets p)"
proof
fix y
assume "y ∈ indets (homogenize x p)"
then obtain t where "t ∈ keys (homogenize x p)" and "y ∈ keys t" by (rule in_indetsE)
from this(1) obtain t' where "t' ∈ keys p"
and t: "t = Poly_Mapping.single x (poly_deg p - deg_pm t') + t'" by (rule keys_homogenizeE)
note ‹y ∈ keys t›
also have "keys t ⊆ keys (Poly_Mapping.single x (poly_deg p - deg_pm t')) ∪ keys t'"
unfolding t by (rule Poly_Mapping.keys_add)
finally show "y ∈ insert x (indets p)"
proof
assume "y ∈ keys (Poly_Mapping.single x (poly_deg p - deg_pm t'))"
thus ?thesis by (simp split: if_split_asm)
next
assume "y ∈ keys t'"
hence "y ∈ indets p" using ‹t' ∈ keys p› by (rule in_indetsI)
thus ?thesis by simp
qed
qed
lemma homogenize_in_Polys: "p ∈ P[X] ⟹ homogenize x p ∈ P[insert x X]"
using indets_homogenize_subset[of x p] by (auto simp: Polys_alt)
lemma lookup_homogenize:
assumes "x ∉ indets p" and "x ∉ keys t"
shows "lookup (homogenize x p) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t) = lookup p t"
proof -
let ?p = "homogenize x p"
let ?t = "Poly_Mapping.single x (poly_deg p - deg_pm t) + t"
have eq: "(∑s∈keys p - {t}. lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t) = 0"
proof (intro sum.neutral ballI)
fix s
assume "s ∈ keys p - {t}"
hence "s ∈ keys p" and "s ≠ t" by simp_all
from this(1) have "keys s ⊆ indets p" by (simp add: in_indetsI subsetI)
with assms(1) have "x ∉ keys s" by blast
have "?t ≠ Poly_Mapping.single x (poly_deg p - deg_pm s) + s"
proof
assume a: "?t = Poly_Mapping.single x (poly_deg p - deg_pm s) + s"
hence "lookup ?t x = lookup (Poly_Mapping.single x (poly_deg p - deg_pm s) + s) x"
by simp
moreover from assms(2) have "lookup t x = 0" by (simp add: in_keys_iff)
moreover from ‹x ∉ keys s› have "lookup s x = 0" by (simp add: in_keys_iff)
ultimately have "poly_deg p - deg_pm t = poly_deg p - deg_pm s" by (simp add: lookup_add)
with a have "s = t" by simp
with ‹s ≠ t› show False ..
qed
thus "lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t = 0"
by (simp add: lookup_single)
qed
show ?thesis
proof (cases "t ∈ keys p")
case True
have "lookup ?p ?t = (∑s∈keys p. lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t)"
by (simp add: homogenize_def lookup_sum)
also have "… = lookup (monomial (lookup p t) ?t) ?t +
(∑s∈keys p - {t}. lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t)"
using finite_keys True by (rule sum.remove)
also have "… = lookup p t" by (simp add: eq)
finally show ?thesis .
next
case False
hence 1: "keys p - {t} = keys p" by simp
have "lookup ?p ?t = (∑s∈keys p - {t}. lookup (monomial (lookup p s) (Poly_Mapping.single x (poly_deg p - deg_pm s) + s)) ?t)"
by (simp add: homogenize_def lookup_sum 1)
also have "… = 0" by (simp only: eq)
also from False have "… = lookup p t" by (simp add: in_keys_iff)
finally show ?thesis .
qed
qed
lemma keys_homogenizeI:
assumes "x ∉ indets p" and "t ∈ keys p"
shows "Poly_Mapping.single x (poly_deg p - deg_pm t) + t ∈ keys (homogenize x p)" (is "?t ∈ keys ?p")
proof -
from assms(2) have "keys t ⊆ indets p" by (simp add: in_indetsI subsetI)
with assms(1) have "x ∉ keys t" by blast
with assms(1) have "lookup ?p ?t = lookup p t" by (rule lookup_homogenize)
also from assms(2) have "… ≠ 0" by (simp add: in_keys_iff)
finally show ?thesis by (simp add: in_keys_iff)
qed
lemma keys_homogenize:
"x ∉ indets p ⟹ keys (homogenize x p) = (λt. Poly_Mapping.single x (poly_deg p - deg_pm t) + t) ` keys p"
by (auto intro: keys_homogenizeI elim: keys_homogenizeE)
lemma card_keys_homogenize:
assumes "x ∉ indets p"
shows "card (keys (homogenize x p)) = card (keys p)"
unfolding keys_homogenize[OF assms]
proof (intro card_image inj_onI)
fix s t
assume "s ∈ keys p" and "t ∈ keys p"
with assms have "x ∉ keys s" and "x ∉ keys t" by (auto dest: in_indetsI simp only:)
let ?s = "Poly_Mapping.single x (poly_deg p - deg_pm s)"
let ?t = "Poly_Mapping.single x (poly_deg p - deg_pm t)"
assume "?s + s = ?t + t"
hence "lookup (?s + s) x = lookup (?t + t) x" by simp
with ‹x ∉ keys s› ‹x ∉ keys t› have "?s = ?t" by (simp add: lookup_add in_keys_iff)
with ‹?s + s = ?t + t› show "s = t" by simp
qed
lemma poly_deg_homogenize:
assumes "x ∉ indets p"
shows "poly_deg (homogenize x p) = poly_deg p"
proof (cases "p = 0")
case True
thus ?thesis by simp
next
case False
then obtain t where "t ∈ keys p" and 1: "poly_deg p = deg_pm t" by (rule poly_degE)
from assms this(1) have "Poly_Mapping.single x (poly_deg p - deg_pm t) + t ∈ keys (homogenize x p)"
by (rule keys_homogenizeI)
hence "t ∈ keys (homogenize x p)" by (simp add: 1)
hence "poly_deg p ≤ poly_deg (homogenize x p)" unfolding 1 by (rule poly_deg_max_keys)
with poly_deg_homogenize_le show ?thesis by (rule antisym)
qed
lemma maxdeg_homogenize:
assumes "x ∉ ⋃ (indets ` F)"
shows "maxdeg (homogenize x ` F) = maxdeg F"
unfolding maxdeg_def image_image
proof (rule arg_cong[where f=Max], rule set_eqI)
fix d
show "d ∈ (λf. poly_deg (homogenize x f)) ` F ⟷ d ∈ poly_deg ` F"
proof
assume "d ∈ (λf. poly_deg (homogenize x f)) ` F"
then obtain f where "f ∈ F" and d: "d = poly_deg (homogenize x f)" ..
from assms this(1) have "x ∉ indets f" by blast
hence "d = poly_deg f" by (simp add: d poly_deg_homogenize)
with ‹f ∈ F› show "d ∈ poly_deg ` F" by (rule rev_image_eqI)
next
assume "d ∈ poly_deg ` F"
then obtain f where "f ∈ F" and d: "d = poly_deg f" ..
from assms this(1) have "x ∉ indets f" by blast
hence "d = poly_deg (homogenize x f)" by (simp add: d poly_deg_homogenize)
with ‹f ∈ F› show "d ∈ (λf. poly_deg (homogenize x f)) ` F" by (rule rev_image_eqI)
qed
qed
lemma homogeneous_ideal_homogenize:
assumes "⋀f. f ∈ F ⟹ homogeneous f" and "p ∈ ideal F"
shows "homogenize x p ∈ ideal F"
proof -
have "homogenize x p = (∑q∈hom_components p. punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q)"
by (fact homogenize_alt)
also have "… ∈ ideal F"
proof (rule ideal.span_sum)
fix q
assume "q ∈ hom_components p"
with assms have "q ∈ ideal F" by (rule homogeneous_ideal')
thus "punit.monom_mult 1 (Poly_Mapping.single x (poly_deg p - poly_deg q)) q ∈ ideal F"
by (rule punit.pmdl_closed_monom_mult[simplified])
qed
finally show ?thesis .
qed
lemma subst_pp_dehomo_subst [simp]:
"subst_pp (dehomo_subst x) t = monomial (1::'b::comm_semiring_1) (except t {x})"
proof -
have "subst_pp (dehomo_subst x) t = ((∏y∈keys t. dehomo_subst x y ^ lookup t y)::_ ⇒⇩0 'b)"
by (fact subst_pp_def)
also have "… = (∏y∈keys t - {y0. dehomo_subst x y0 ^ lookup t y0 = (1::_ ⇒⇩0 'b)}. dehomo_subst x y ^ lookup t y)"
by (rule sym, rule prod.setdiff_irrelevant, fact finite_keys)
also have "… = (∏y∈keys t - {x}. monomial 1 (Poly_Mapping.single y 1) ^ lookup t y)"
proof (rule prod.cong)
have "dehomo_subst x x ^ lookup t x = 1" by (simp add: dehomo_subst_def)
moreover {
fix y
assume "y ≠ x"
hence "dehomo_subst x y ^ lookup t y = monomial 1 (Poly_Mapping.single y (lookup t y))"
by (simp add: dehomo_subst_def monomial_single_power)
moreover assume "dehomo_subst x y ^ lookup t y = 1"
ultimately have "Poly_Mapping.single y (lookup t y) = 0"
by (smt (verit) single_one monomial_inj zero_neq_one)
hence "lookup t y = 0" by (rule monomial_0D)
moreover assume "y ∈ keys t"
ultimately have False by (simp add: in_keys_iff)
}
ultimately show "keys t - {y0. dehomo_subst x y0 ^ lookup t y0 = 1} = keys t - {x}" by auto
qed (simp add: dehomo_subst_def)
also have "… = (∏y∈keys t - {x}. monomial 1 (Poly_Mapping.single y (lookup t y)))"
by (simp add: monomial_single_power)
also have "… = monomial 1 (∑y∈keys t - {x}. Poly_Mapping.single y (lookup t y))"
by (simp flip: punit.monomial_prod_sum)
also have "(∑y∈keys t - {x}. Poly_Mapping.single y (lookup t y)) = except t {x}"
proof (rule poly_mapping_eqI, simp add: lookup_sum lookup_except lookup_single, rule)
fix y
assume "y ≠ x"
show "(∑z∈keys t - {x}. lookup t z when z = y) = lookup t y"
proof (cases "y ∈ keys t")
case True
have "finite (keys t - {x})" by simp
moreover from True ‹y ≠ x› have "y ∈ keys t - {x}" by simp
ultimately have "(∑z∈keys t - {x}. lookup t z when z = y) =
(lookup t y when y = y) + (∑z∈keys t - {x} - {y}. lookup t z when z = y)"
by (rule sum.remove)
also have "(∑z∈keys t - {x} - {y}. lookup t z when z = y) = 0" by auto
finally show ?thesis by simp
next
case False
hence "(∑z∈keys t - {x}. lookup t z when z = y) = 0" by (auto simp: when_def)
also from False have "… = lookup t y" by (simp add: in_keys_iff)
finally show ?thesis .
qed
qed
finally show ?thesis .
qed
lemma
shows dehomogenize_zero [simp]: "dehomogenize x 0 = 0"
and dehomogenize_one [simp]: "dehomogenize x 1 = 1"
and dehomogenize_monomial: "dehomogenize x (monomial c t) = monomial c (except t {x})"
and dehomogenize_plus: "dehomogenize x (p + q) = dehomogenize x p + dehomogenize x q"
and dehomogenize_uminus: "dehomogenize x (- r) = - dehomogenize x (r::_ ⇒⇩0 _::comm_ring_1)"
and dehomogenize_minus: "dehomogenize x (r - r') = dehomogenize x r - dehomogenize x r'"
and dehomogenize_times: "dehomogenize x (p * q) = dehomogenize x p * dehomogenize x q"
and dehomogenize_power: "dehomogenize x (p ^ n) = dehomogenize x p ^ n"
and dehomogenize_sum: "dehomogenize x (sum f A) = (∑a∈A. dehomogenize x (f a))"
and dehomogenize_prod: "dehomogenize x (prod f A) = (∏a∈A. dehomogenize x (f a))"
by (simp_all add: dehomogenize_def poly_subst_monomial poly_subst_plus poly_subst_uminus
poly_subst_minus poly_subst_times poly_subst_power poly_subst_sum poly_subst_prod punit.monom_mult_monomial)
corollary dehomogenize_monom_mult:
"dehomogenize x (punit.monom_mult c t p) = punit.monom_mult c (except t {x}) (dehomogenize x p)"
by (simp only: times_monomial_left[symmetric] dehomogenize_times dehomogenize_monomial)
lemma poly_deg_dehomogenize_le: "poly_deg (dehomogenize x p) ≤ poly_deg p"
unfolding dehomogenize_def dehomo_subst_def
by (rule poly_deg_poly_subst_le) (simp add: poly_deg_monomial deg_pm_single)
lemma indets_dehomogenize: "indets (dehomogenize x p) ⊆ indets p - {x}"
for p::"('x ⇒⇩0 nat) ⇒⇩0 'a::comm_semiring_1"
proof
fix y::'x
assume "y ∈ indets (dehomogenize x p)"
then obtain y' where "y' ∈ indets p" and "y ∈ indets ((dehomo_subst x y')::_ ⇒⇩0 'a)"
unfolding dehomogenize_def by (rule in_indets_poly_substE)
from this(2) have "y = y'" and "y' ≠ x"
by (simp_all add: dehomo_subst_def indets_monomial split: if_split_asm)
with ‹y' ∈ indets p› show "y ∈ indets p - {x}" by simp
qed
lemma dehomogenize_id_iff [simp]: "dehomogenize x p = p ⟷ x ∉ indets p"
proof
assume eq: "dehomogenize x p = p"
from indets_dehomogenize[of x p] show "x ∉ indets p" by (auto simp: eq)
next
assume a: "x ∉ indets p"
show "dehomogenize x p = p" unfolding dehomogenize_def
proof (rule poly_subst_id)
fix y
assume "y ∈ indets p"
with a have "y ≠ x" by blast
thus "dehomo_subst x y = monomial 1 (Poly_Mapping.single y 1)" by (simp add: dehomo_subst_def)
qed
qed
lemma dehomogenize_dehomogenize [simp]: "dehomogenize x (dehomogenize x p) = dehomogenize x p"
proof -
from indets_dehomogenize[of x p] have "x ∉ indets (dehomogenize x p)" by blast
thus ?thesis by simp
qed
lemma dehomogenize_homogenize [simp]: "dehomogenize x (homogenize x p) = dehomogenize x p"
proof -
have "dehomogenize x (homogenize x p) = sum (dehomogenize x) (hom_components p)"
by (simp add: homogenize_alt dehomogenize_sum dehomogenize_monom_mult except_single)
also have "… = dehomogenize x p" by (simp only: sum_hom_components flip: dehomogenize_sum)
finally show ?thesis .
qed
corollary dehomogenize_homogenize_id: "x ∉ indets p ⟹ dehomogenize x (homogenize x p) = p"
by simp
lemma range_dehomogenize: "range (dehomogenize x) = (P[- {x}] :: (_ ⇒⇩0 'a::comm_semiring_1) set)"
proof (intro subset_antisym subsetI PolysI_alt range_eqI)
fix p::"_ ⇒⇩0 'a" and y
assume "p ∈ range (dehomogenize x)"
then obtain q where p: "p = dehomogenize x q" ..
assume "y ∈ indets p"
hence "y ∈ indets (dehomogenize x q)" by (simp only: p)
with indets_dehomogenize have "y ∈ indets q - {x}" ..
thus "y ∈ - {x}" by simp
next
fix p::"_ ⇒⇩0 'a"
assume "p ∈ P[- {x}]"
hence "x ∉ indets p" by (auto dest: PolysD)
thus "p = dehomogenize x (homogenize x p)" by (rule dehomogenize_homogenize_id[symmetric])
qed
lemma dehomogenize_alt: "dehomogenize x p = (∑t∈keys p. monomial (lookup p t) (except t {x}))"
proof -
have "dehomogenize x p = dehomogenize x (∑t∈keys p. monomial (lookup p t) t)"
by (simp only: poly_mapping_sum_monomials)
also have "… = (∑t∈keys p. monomial (lookup p t) (except t {x}))"
by (simp only: dehomogenize_sum dehomogenize_monomial)
finally show ?thesis .
qed
lemma keys_dehomogenizeE:
assumes "t ∈ keys (dehomogenize x p)"
obtains s where "s ∈ keys p" and "t = except s {x}"
proof -
note assms
also have "keys (dehomogenize x p) ⊆ (⋃s∈keys p. keys (monomial (lookup p s) (except s {x})))"
unfolding dehomogenize_alt by (rule keys_sum_subset)
finally obtain s where "s ∈ keys p" and "t ∈ keys (monomial (lookup p s) (except s {x}))" ..
from this(2) have "t = except s {x}" by (simp split: if_split_asm)
with ‹s ∈ keys p› show ?thesis ..
qed
lemma except_inj_on_keys_homogeneous:
assumes "homogeneous p"
shows "inj_on (λt. except t {x}) (keys p)"
proof
fix s t
assume "s ∈ keys p" and "t ∈ keys p"
from assms this(1) have "deg_pm s = poly_deg p" by (rule homogeneousD_poly_deg)
moreover from assms ‹t ∈ keys p› have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
ultimately have "deg_pm (Poly_Mapping.single x (lookup s x) + except s {x}) =
deg_pm (Poly_Mapping.single x (lookup t x) + except t {x})"
by (simp only: flip: plus_except)
moreover assume 1: "except s {x} = except t {x}"
ultimately have 2: "lookup s x = lookup t x"
by (simp only: deg_pm_plus deg_pm_single)
show "s = t"
proof (rule poly_mapping_eqI)
fix y
show "lookup s y = lookup t y"
proof (cases "y = x")
case True
with 2 show ?thesis by simp
next
case False
hence "lookup s y = lookup (except s {x}) y" and "lookup t y = lookup (except t {x}) y"
by (simp_all add: lookup_except)
with 1 show ?thesis by simp
qed
qed
qed
lemma lookup_dehomogenize:
assumes "homogeneous p" and "t ∈ keys p"
shows "lookup (dehomogenize x p) (except t {x}) = lookup p t"
proof -
let ?t = "except t {x}"
have eq: "(∑s∈keys p - {t}. lookup (monomial (lookup p s) (except s {x})) ?t) = 0"
proof (intro sum.neutral ballI)
fix s
assume "s ∈ keys p - {t}"
hence "s ∈ keys p" and "s ≠ t" by simp_all
have "?t ≠ except s {x}"
proof
from assms(1) have "inj_on (λt. except t {x}) (keys p)" by (rule except_inj_on_keys_homogeneous)
moreover assume "?t = except s {x}"
ultimately have "t = s" using assms(2) ‹s ∈ keys p› by (rule inj_onD)
with ‹s ≠ t› show False by simp
qed
thus "lookup (monomial (lookup p s) (except s {x})) ?t = 0" by (simp add: lookup_single)
qed
have "lookup (dehomogenize x p) ?t = (∑s∈keys p. lookup (monomial (lookup p s) (except s {x})) ?t)"
by (simp only: dehomogenize_alt lookup_sum)
also have "… = lookup (monomial (lookup p t) ?t) ?t +
(∑s∈keys p - {t}. lookup (monomial (lookup p s) (except s {x})) ?t)"
using finite_keys assms(2) by (rule sum.remove)
also have "… = lookup p t" by (simp add: eq)
finally show ?thesis .
qed
lemma keys_dehomogenizeI:
assumes "homogeneous p" and "t ∈ keys p"
shows "except t {x} ∈ keys (dehomogenize x p)"
proof -
from assms have "lookup (dehomogenize x p) (except t {x}) = lookup p t" by (rule lookup_dehomogenize)
also from assms(2) have "… ≠ 0" by (simp add: in_keys_iff)
finally show ?thesis by (simp add: in_keys_iff)
qed
lemma homogeneous_homogenize_dehomogenize:
assumes "homogeneous p"
obtains d where "d = poly_deg p - poly_deg (homogenize x (dehomogenize x p))"
and "punit.monom_mult 1 (Poly_Mapping.single x d) (homogenize x (dehomogenize x p)) = p"
proof (cases "p = 0")
case True
hence "0 = poly_deg p - poly_deg (homogenize x (dehomogenize x p))"
and "punit.monom_mult 1 (Poly_Mapping.single x 0) (homogenize x (dehomogenize x p)) = p"
by simp_all
thus ?thesis ..
next
case False
let ?q = "dehomogenize x p"
let ?p = "homogenize x ?q"
define d where "d = poly_deg p - poly_deg ?p"
show ?thesis
proof
have "punit.monom_mult 1 (Poly_Mapping.single x d) ?p =
(∑t∈keys ?q. monomial (lookup ?q t) (Poly_Mapping.single x (d + (poly_deg ?q - deg_pm t)) + t))"
by (simp add: homogenize_def punit.monom_mult_sum_right punit.monom_mult_monomial flip: add.assoc single_add)
also have "… = (∑t∈keys ?q. monomial (lookup ?q t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"
using refl
proof (rule sum.cong)
fix t
assume "t ∈ keys ?q"
have "poly_deg ?p = poly_deg ?q"
proof (rule poly_deg_homogenize)
from indets_dehomogenize show "x ∉ indets ?q" by fastforce
qed
hence d: "d = poly_deg p - poly_deg ?q" by (simp only: d_def)
thm poly_deg_dehomogenize_le
from ‹t ∈ keys ?q› have "d + (poly_deg ?q - deg_pm t) = (d + poly_deg ?q) - deg_pm t"
by (intro add_diff_assoc poly_deg_max_keys)
also have "d + poly_deg ?q = poly_deg p" by (simp add: d poly_deg_dehomogenize_le)
finally show "monomial (lookup ?q t) (Poly_Mapping.single x (d + (poly_deg ?q - deg_pm t)) + t) =
monomial (lookup ?q t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t)"
by (simp only:)
qed
also have "… = (∑t∈(λs. except s {x}) ` keys p.
monomial (lookup ?q t) (Poly_Mapping.single x (poly_deg p - deg_pm t) + t))"
proof (rule sum.mono_neutral_left)
show "keys (dehomogenize x p) ⊆ (λs. except s {x}) ` keys p"
proof
fix t
assume "t ∈ keys (dehomogenize x p)"
then obtain s where "s ∈ keys p" and "t = except s {x}" by (rule keys_dehomogenizeE)
thus "t ∈ (λs. except s {x}) ` keys p" by (rule rev_image_eqI)
qed
qed (simp_all add: in_keys_iff)
also from assms have "… = (∑t∈keys p. monomial (lookup ?q (except t {x}))
(Poly_Mapping.single x (poly_deg p - deg_pm (except t {x})) + except t {x}))"
by (intro sum.reindex[unfolded comp_def] except_inj_on_keys_homogeneous)
also from refl have "… = (∑t∈keys p. monomial (lookup p t) t)"
proof (rule sum.cong)
fix t
assume "t ∈ keys p"
with assms have "lookup ?q (except t {x}) = lookup p t" by (rule lookup_dehomogenize)
moreover have "Poly_Mapping.single x (poly_deg p - deg_pm (except t {x})) + except t {x} = t"
(is "?l = _")
proof (rule poly_mapping_eqI)
fix y
show "lookup ?l y = lookup t y"
proof (cases "y = x")
case True
from assms ‹t ∈ keys p› have "deg_pm t = poly_deg p" by (rule homogeneousD_poly_deg)
also have "deg_pm t = deg_pm (Poly_Mapping.single x (lookup t x) + except t {x})"
by (simp flip: plus_except)
also have "… = lookup t x + deg_pm (except t {x})" by (simp only: deg_pm_plus deg_pm_single)
finally have "poly_deg p - deg_pm (except t {x}) = lookup t x" by simp
thus ?thesis by (simp add: True lookup_add lookup_except lookup_single)
next
case False
thus ?thesis by (simp add: lookup_add lookup_except lookup_single)
qed
qed
ultimately show "monomial (lookup ?q (except t {x}))
(Poly_Mapping.single x (poly_deg p - deg_pm (except t {x})) + except t {x}) =
monomial (lookup p t) t" by (simp only:)
qed
also have "… = p" by (fact poly_mapping_sum_monomials)
finally show "punit.monom_mult 1 (Poly_Mapping.single x d) ?p = p" .
qed (simp only: d_def)
qed
lemma dehomogenize_zeroD:
assumes "dehomogenize x p = 0" and "homogeneous p"
shows "p = 0"
proof -
from assms(2) obtain d
where "punit.monom_mult 1 (Poly_Mapping.single x d) (homogenize x (dehomogenize x p)) = p"
by (rule homogeneous_homogenize_dehomogenize)
thus ?thesis by (simp add: assms(1))
qed
lemma dehomogenize_ideal: "dehomogenize x ` ideal F = ideal (dehomogenize x ` F) ∩ P[- {x}]"
unfolding range_dehomogenize[symmetric]
using dehomogenize_plus dehomogenize_times dehomogenize_dehomogenize by (rule image_ideal_eq_Int)
corollary dehomogenize_ideal_subset: "dehomogenize x ` ideal F ⊆ ideal (dehomogenize x ` F)"
by (simp add: dehomogenize_ideal)
lemma ideal_dehomogenize:
assumes "ideal G = ideal (homogenize x ` F)" and "F ⊆ P[UNIV - {x}]"
shows "ideal (dehomogenize x ` G) = ideal F"
proof -
have eq: "dehomogenize x (homogenize x f) = f" if "f ∈ F" for f
proof (rule dehomogenize_homogenize_id)
from that assms(2) have "f ∈ P[UNIV - {x}]" ..
thus "x ∉ indets f" by (auto simp: Polys_alt)
qed
show ?thesis
proof (intro Set.equalityI ideal.span_subset_spanI)
show "dehomogenize x ` G ⊆ ideal F"
proof
fix q
assume "q ∈ dehomogenize x ` G"
then obtain g where "g ∈ G" and q: "q = dehomogenize x g" ..
from this(1) have "g ∈ ideal G" by (rule ideal.span_base)
also have "… = ideal (homogenize x ` F)" by fact
finally have "q ∈ dehomogenize x ` ideal (homogenize x ` F)" using q by (rule rev_image_eqI)
also have "… ⊆ ideal (dehomogenize x ` homogenize x ` F)" by (rule dehomogenize_ideal_subset)
also have "dehomogenize x ` homogenize x ` F = F"
by (auto simp: eq image_image simp del: dehomogenize_homogenize intro!: image_eqI)
finally show "q ∈ ideal F" .
qed
next
show "F ⊆ ideal (dehomogenize x ` G)"
proof
fix f
assume "f ∈ F"
hence "homogenize x f ∈ homogenize x ` F" by (rule imageI)
also have "… ⊆ ideal (homogenize x ` F)" by (rule ideal.span_superset)
also from assms(1) have "… = ideal G" by (rule sym)
finally have "dehomogenize x (homogenize x f) ∈ dehomogenize x ` ideal G" by (rule imageI)
with ‹f ∈ F› have "f ∈ dehomogenize x ` ideal G" by (simp only: eq)
also have "… ⊆ ideal (dehomogenize x ` G)" by (rule dehomogenize_ideal_subset)
finally show "f ∈ ideal (dehomogenize x ` G)" .
qed
qed
qed
subsection ‹Embedding Polynomial Rings in Larger Polynomial Rings (With One Additional Indeterminate)›
text ‹We define a homomorphism for embedding a polynomial ring in a larger polynomial ring, and its
inverse. This is mainly needed for homogenizing wrt. a fresh indeterminate.›
definition extend_indets_subst :: "'x ⇒ ('x option ⇒⇩0 nat) ⇒⇩0 'a::comm_semiring_1"
where "extend_indets_subst x = monomial 1 (Poly_Mapping.single (Some x) 1)"
definition extend_indets :: "(('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ ('x option ⇒⇩0 nat) ⇒⇩0 'a::comm_semiring_1"
where "extend_indets = poly_subst extend_indets_subst"
definition restrict_indets_subst :: "'x option ⇒ 'x ⇒⇩0 nat"
where "restrict_indets_subst x = (case x of Some y ⇒ Poly_Mapping.single y 1 | _ ⇒ 0)"
definition restrict_indets :: "(('x option ⇒⇩0 nat) ⇒⇩0 'a) ⇒ ('x ⇒⇩0 nat) ⇒⇩0 'a::comm_semiring_1"
where "restrict_indets = poly_subst (λx. monomial 1 (restrict_indets_subst x))"
definition restrict_indets_pp :: "('x option ⇒⇩0 nat) ⇒ ('x ⇒⇩0 nat)"
where "restrict_indets_pp t = (∑x∈keys t. lookup t x ⋅ restrict_indets_subst x)"
lemma lookup_extend_indets_subst_aux:
"lookup (∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y)) = (λx. case x of Some y ⇒ lookup t y | _ ⇒ 0)"
proof -
have "(∑x∈keys t. lookup t x when x = y) = lookup t y" for y
proof (cases "y ∈ keys t")
case True
hence "(∑x∈keys t. lookup t x when x = y) = (∑x∈insert y (keys t). lookup t x when x = y)"
by (simp only: insert_absorb)
also have "… = lookup t y + (∑x∈keys t - {y}. lookup t x when x = y)"
by (simp add: sum.insert_remove)
also have "(∑x∈keys t - {y}. lookup t x when x = y) = 0"
by (auto simp: when_def intro: sum.neutral)
finally show ?thesis by simp
next
case False
hence "(∑x∈keys t. lookup t x when x = y) = 0" by (auto simp: when_def intro: sum.neutral)
with False show ?thesis by (simp add: in_keys_iff)
qed
thus ?thesis by (auto simp: lookup_sum lookup_single split: option.split)
qed
lemma keys_extend_indets_subst_aux:
"keys (∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y)) = Some ` keys t"
by (auto simp: lookup_extend_indets_subst_aux simp flip: lookup_not_eq_zero_eq_in_keys split: option.splits)
lemma subst_pp_extend_indets_subst:
"subst_pp extend_indets_subst t = monomial 1 (∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y))"
proof -
have "subst_pp extend_indets_subst t =
monomial (∏y∈keys t. 1 ^ lookup t y) (∑y∈keys t. lookup t y ⋅ Poly_Mapping.single (Some y) 1)"
by (rule subst_pp_by_monomials) (simp only: extend_indets_subst_def)
also have "… = monomial 1 (∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y))"
by simp
finally show ?thesis .
qed
lemma keys_extend_indets:
"keys (extend_indets p) = (λt. ∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y)) ` keys p"
proof -
have "keys (extend_indets p) = (⋃t∈keys p. keys (punit.monom_mult (lookup p t) 0 (subst_pp extend_indets_subst t)))"
unfolding extend_indets_def poly_subst_def using finite_keys
proof (rule keys_sum)
fix s t :: "'a ⇒⇩0 nat"
assume "s ≠ t"
then obtain x where "lookup s x ≠ lookup t x" by (meson poly_mapping_eqI)
have "(∑y∈keys t. monomial (lookup t y) (Some y)) ≠ (∑y∈keys s. monomial (lookup s y) (Some y))"
(is "?l ≠ ?r")
proof
assume "?l = ?r"
hence "lookup ?l (Some x) = lookup ?r (Some x)" by (simp only:)
hence "lookup s x = lookup t x" by (simp add: lookup_extend_indets_subst_aux)
with ‹lookup s x ≠ lookup t x› show False ..
qed
thus "keys (punit.monom_mult (lookup p s) 0 (subst_pp extend_indets_subst s)) ∩
keys (punit.monom_mult (lookup p t) 0 (subst_pp extend_indets_subst t)) =
{}"
by (simp add: subst_pp_extend_indets_subst punit.monom_mult_monomial)
qed
also have "… = (λt. ∑y∈keys t. monomial (lookup t y) (Some y)) ` keys p"
by (auto simp: subst_pp_extend_indets_subst punit.monom_mult_monomial split: if_split_asm)
finally show ?thesis .
qed
lemma indets_extend_indets: "indets (extend_indets p) = Some ` indets (p::_ ⇒⇩0 'a::comm_semiring_1)"
proof (rule set_eqI)
fix x
show "x ∈ indets (extend_indets p) ⟷ x ∈ Some ` indets p"
proof
assume "x ∈ indets (extend_indets p)"
then obtain y where "y ∈ indets p" and "x ∈ indets (monomial (1::'a) (Poly_Mapping.single (Some y) 1))"
unfolding extend_indets_def extend_indets_subst_def by (rule in_indets_poly_substE)
from this(2) indets_monomial_single_subset have "x ∈ {Some y}" ..
hence "x = Some y" by simp
with ‹y ∈ indets p› show "x ∈ Some ` indets p" by (rule rev_image_eqI)
next
assume "x ∈ Some ` indets p"
then obtain y where "y ∈ indets p" and x: "x = Some y" ..
from this(1) obtain t where "t ∈ keys p" and "y ∈ keys t" by (rule in_indetsE)
from this(2) have "Some y ∈ keys (∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y))"
unfolding keys_extend_indets_subst_aux by (rule imageI)
moreover have "(∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y)) ∈ keys (extend_indets p)"
unfolding keys_extend_indets using ‹t ∈ keys p› by (rule imageI)
ultimately show "x ∈ indets (extend_indets p)" unfolding x by (rule in_indetsI)
qed
qed
lemma poly_deg_extend_indets [simp]: "poly_deg (extend_indets p) = poly_deg p"
proof -
have eq: "deg_pm ((∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y))) = deg_pm t"
for t::"'a ⇒⇩0 nat"
proof -
have "deg_pm ((∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y))) = (∑y∈keys t. lookup t y)"
by (simp add: deg_pm_sum deg_pm_single)
also from subset_refl finite_keys have "… = deg_pm t" by (rule deg_pm_superset[symmetric])
finally show ?thesis .
qed
show ?thesis
proof (rule antisym)
show "poly_deg (extend_indets p) ≤ poly_deg p"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys (extend_indets p)"
then obtain s where "s ∈ keys p" and "t = (∑y∈keys s. Poly_Mapping.single (Some y) (lookup s y))"
unfolding keys_extend_indets ..
from this(2) have "deg_pm t = deg_pm s" by (simp only: eq)
also from ‹s ∈ keys p› have "… ≤ poly_deg p" by (rule poly_deg_max_keys)
finally show "deg_pm t ≤ poly_deg p" .
qed
next
show "poly_deg p ≤ poly_deg (extend_indets p)"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys p"
hence *: "(∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y)) ∈ keys (extend_indets p)"
unfolding keys_extend_indets by (rule imageI)
have "deg_pm t = deg_pm (∑y∈keys t. Poly_Mapping.single (Some y) (lookup t y))"
by (simp only: eq)
also from * have "… ≤ poly_deg (extend_indets p)" by (rule poly_deg_max_keys)
finally show "deg_pm t ≤ poly_deg (extend_indets p)" .
qed
qed
qed
lemma
shows extend_indets_zero [simp]: "extend_indets 0 = 0"
and extend_indets_one [simp]: "extend_indets 1 = 1"
and extend_indets_monomial: "extend_indets (monomial c t) = punit.monom_mult c 0 (subst_pp extend_indets_subst t)"
and extend_indets_plus: "extend_indets (p + q) = extend_indets p + extend_indets q"
and extend_indets_uminus: "extend_indets (- r) = - extend_indets (r::_ ⇒⇩0 _::comm_ring_1)"
and extend_indets_minus: "extend_indets (r - r') = extend_indets r - extend_indets r'"
and extend_indets_times: "extend_indets (p * q) = extend_indets p * extend_indets q"
and extend_indets_power: "extend_indets (p ^ n) = extend_indets p ^ n"
and extend_indets_sum: "extend_indets (sum f A) = (∑a∈A. extend_indets (f a))"
and extend_indets_prod: "extend_indets (prod f A) = (∏a∈A. extend_indets (f a))"
by (simp_all add: extend_indets_def poly_subst_monomial poly_subst_plus poly_subst_uminus
poly_subst_minus poly_subst_times poly_subst_power poly_subst_sum poly_subst_prod)
lemma extend_indets_zero_iff [simp]: "extend_indets p = 0 ⟷ p = 0"
by (metis (no_types, lifting) imageE imageI keys_extend_indets lookup_zero
not_in_keys_iff_lookup_eq_zero poly_deg_extend_indets poly_deg_zero poly_deg_zero_imp_monomial)
lemma extend_indets_inject:
assumes "extend_indets p = extend_indets (q::_ ⇒⇩0 _::comm_ring_1)"
shows "p = q"
proof -
from assms have "extend_indets (p - q) = 0" by (simp add: extend_indets_minus)
thus ?thesis by simp
qed
corollary inj_extend_indets: "inj (extend_indets::_ ⇒ _ ⇒⇩0 _::comm_ring_1)"
using extend_indets_inject by (intro injI)
lemma poly_subst_extend_indets: "poly_subst f (extend_indets p) = poly_subst (f ∘ Some) p"
by (simp add: extend_indets_def poly_subst_poly_subst extend_indets_subst_def poly_subst_monomial
subst_pp_single o_def)
lemma poly_eval_extend_indets: "poly_eval a (extend_indets p) = poly_eval (a ∘ Some) p"
proof -
have eq: "poly_eval a (extend_indets (monomial c t)) = poly_eval (λx. a (Some x)) (monomial c t)"
for c t
by (simp add: extend_indets_monomial poly_eval_times poly_eval_monomial poly_eval_prod poly_eval_power
subst_pp_def extend_indets_subst_def flip: times_monomial_left)
show ?thesis
by (induct p rule: poly_mapping_plus_induct) (simp_all add: extend_indets_plus poly_eval_plus eq)
qed
lemma lookup_restrict_indets_pp: "lookup (restrict_indets_pp t) = (λx. lookup t (Some x))"
proof -
let ?f = "λz x. lookup t x * lookup (case x of None ⇒ 0 | Some y ⇒ Poly_Mapping.single y 1) z"
have "sum (?f z) (keys t) = lookup t (Some z)" for z
proof (cases "Some z ∈ keys t")
case True
hence "sum (?f z) (keys t) = sum (?f z) (insert (Some z) (keys t))"
by (simp only: insert_absorb)
also have "… = lookup t (Some z) + sum (?f z) (keys t - {Some z})"
by (simp add: sum.insert_remove)
also have "sum (?f z) (keys t - {Some z}) = 0"
by (auto simp: when_def lookup_single intro: sum.neutral split: option.splits)
finally show ?thesis by simp
next
case False
hence "sum (?f z) (keys t) = 0"
by (auto simp: when_def lookup_single intro: sum.neutral split: option.splits)
with False show ?thesis by (simp add: in_keys_iff)
qed
thus ?thesis by (auto simp: restrict_indets_pp_def restrict_indets_subst_def lookup_sum)
qed
lemma keys_restrict_indets_pp: "keys (restrict_indets_pp t) = the ` (keys t - {None})"
proof (rule set_eqI)
fix x
show "x ∈ keys (restrict_indets_pp t) ⟷ x ∈ the ` (keys t - {None})"
proof
assume "x ∈ keys (restrict_indets_pp t)"
hence "Some x ∈ keys t" by (simp add: lookup_restrict_indets_pp flip: lookup_not_eq_zero_eq_in_keys)
hence "Some x ∈ keys t - {None}" by blast
moreover have "x = the (Some x)" by simp
ultimately show "x ∈ the ` (keys t - {None})" by (rule rev_image_eqI)
next
assume "x ∈ the ` (keys t - {None})"
then obtain y where "y ∈ keys t - {None}" and "x = the y" ..
hence "Some x ∈ keys t" by auto
thus "x ∈ keys (restrict_indets_pp t)"
by (simp add: lookup_restrict_indets_pp flip: lookup_not_eq_zero_eq_in_keys)
qed
qed
lemma subst_pp_restrict_indets_subst:
"subst_pp (λx. monomial 1 (restrict_indets_subst x)) t = monomial 1 (restrict_indets_pp t)"
by (simp add: subst_pp_def monomial_power_map_scale restrict_indets_pp_def flip: punit.monomial_prod_sum)
lemma restrict_indets_pp_zero [simp]: "restrict_indets_pp 0 = 0"
by (simp add: restrict_indets_pp_def)
lemma restrict_indets_pp_plus: "restrict_indets_pp (s + t) = restrict_indets_pp s + restrict_indets_pp t"
by (rule poly_mapping_eqI) (simp add: lookup_add lookup_restrict_indets_pp)
lemma restrict_indets_pp_except_None [simp]:
"restrict_indets_pp (except t {None}) = restrict_indets_pp t"
by (rule poly_mapping_eqI) (simp add: lookup_add lookup_restrict_indets_pp lookup_except)
lemma deg_pm_restrict_indets_pp: "deg_pm (restrict_indets_pp t) + lookup t None = deg_pm t"
proof -
have "deg_pm t = sum (lookup t) (insert None (keys t))" by (rule deg_pm_superset) auto
also from finite_keys have "… = lookup t None + sum (lookup t) (keys t - {None})"
by (rule sum.insert_remove)
also have "sum (lookup t) (keys t - {None}) = (∑x∈keys t. lookup t x * deg_pm (restrict_indets_subst x))"
by (intro sum.mono_neutral_cong_left) (auto simp: restrict_indets_subst_def deg_pm_single)
also have "… = deg_pm (restrict_indets_pp t)"
by (simp only: restrict_indets_pp_def deg_pm_sum deg_pm_map_scale)
finally show ?thesis by simp
qed
lemma keys_restrict_indets_subset: "keys (restrict_indets p) ⊆ restrict_indets_pp ` keys p"
proof
fix t
assume "t ∈ keys (restrict_indets p)"
also have "… = keys (∑t∈keys p. monomial (lookup p t) (restrict_indets_pp t))"
by (simp add: restrict_indets_def poly_subst_def subst_pp_restrict_indets_subst punit.monom_mult_monomial)
also have "… ⊆ (⋃t∈keys p. keys (monomial (lookup p t) (restrict_indets_pp t)))"
by (rule keys_sum_subset)
also have "… = restrict_indets_pp ` keys p" by (auto split: if_split_asm)
finally show "t ∈ restrict_indets_pp ` keys p" .
qed
lemma keys_restrict_indets:
assumes "None ∉ indets p"
shows "keys (restrict_indets p) = restrict_indets_pp ` keys p"
proof -
have "keys (restrict_indets p) = keys (∑t∈keys p. monomial (lookup p t) (restrict_indets_pp t))"
by (simp add: restrict_indets_def poly_subst_def subst_pp_restrict_indets_subst punit.monom_mult_monomial)
also from finite_keys have "… = (⋃t∈keys p. keys (monomial (lookup p t) (restrict_indets_pp t)))"
proof (rule keys_sum)
fix s t
assume "s ∈ keys p"
hence "keys s ⊆ indets p" by (rule keys_subset_indets)
with assms have "None ∉ keys s" by blast
assume "t ∈ keys p"
hence "keys t ⊆ indets p" by (rule keys_subset_indets)
with assms have "None ∉ keys t" by blast
assume "s ≠ t"
then obtain x where neq: "lookup s x ≠ lookup t x" by (meson poly_mapping_eqI)
have "x ≠ None"
proof
assume "x = None"
with ‹None ∉ keys s› and ‹None ∉ keys t› have "x ∉ keys s" and "x ∉ keys t" by blast+
with neq show False by (simp add: in_keys_iff)
qed
then obtain y where x: "x = Some y" by blast
have "restrict_indets_pp t ≠ restrict_indets_pp s"
proof
assume "restrict_indets_pp t = restrict_indets_pp s"
hence "lookup (restrict_indets_pp t) y = lookup (restrict_indets_pp s) y" by (simp only:)
hence "lookup s x = lookup t x" by (simp add: x lookup_restrict_indets_pp)
with neq show False ..
qed
thus "keys (monomial (lookup p s) (restrict_indets_pp s)) ∩
keys (monomial (lookup p t) (restrict_indets_pp t)) = {}"
by (simp add: subst_pp_extend_indets_subst)
qed
also have "… = restrict_indets_pp ` keys p" by (auto split: if_split_asm)
finally show ?thesis .
qed
lemma indets_restrict_indets_subset: "indets (restrict_indets p) ⊆ the ` (indets p - {None})"
proof
fix x
assume "x ∈ indets (restrict_indets p)"
then obtain t where "t ∈ keys (restrict_indets p)" and "x ∈ keys t" by (rule in_indetsE)
from this(1) keys_restrict_indets_subset have "t ∈ restrict_indets_pp ` keys p" ..
then obtain s where "s ∈ keys p" and "t = restrict_indets_pp s" ..
from ‹x ∈ keys t› this(2) have "x ∈ the ` (keys s - {None})" by (simp only: keys_restrict_indets_pp)
also from ‹s ∈ keys p› have "… ⊆ the ` (indets p - {None})"
by (intro image_mono Diff_mono keys_subset_indets subset_refl)
finally show "x ∈ the ` (indets p - {None})" .
qed
lemma poly_deg_restrict_indets_le: "poly_deg (restrict_indets p) ≤ poly_deg p"
proof (rule poly_deg_leI)
fix t
assume "t ∈ keys (restrict_indets p)"
hence "t ∈ restrict_indets_pp ` keys p" using keys_restrict_indets_subset ..
then obtain s where "s ∈ keys p" and "t = restrict_indets_pp s" ..
from this(2) have "deg_pm t + lookup s None = deg_pm s"
by (simp only: deg_pm_restrict_indets_pp)
also from ‹s ∈ keys p› have "… ≤ poly_deg p" by (rule poly_deg_max_keys)
finally show "deg_pm t ≤ poly_deg p" by simp
qed
lemma
shows restrict_indets_zero [simp]: "restrict_indets 0 = 0"
and restrict_indets_one [simp]: "restrict_indets 1 = 1"
and restrict_indets_monomial: "restrict_indets (monomial c t) = monomial c (restrict_indets_pp t)"
and restrict_indets_plus: "restrict_indets (p + q) = restrict_indets p + restrict_indets q"
and restrict_indets_uminus: "restrict_indets (- r) = - restrict_indets (r::_ ⇒⇩0 _::comm_ring_1)"
and restrict_indets_minus: "restrict_indets (r - r') = restrict_indets r - restrict_indets r'"
and restrict_indets_times: "restrict_indets (p * q) = restrict_indets p * restrict_indets q"
and restrict_indets_power: "restrict_indets (p ^ n) = restrict_indets p ^ n"
and restrict_indets_sum: "restrict_indets (sum f A) = (∑a∈A. restrict_indets (f a))"
and restrict_indets_prod: "restrict_indets (prod f A) = (∏a∈A. restrict_indets (f a))"
by (simp_all add: restrict_indets_def poly_subst_monomial poly_subst_plus poly_subst_uminus
poly_subst_minus poly_subst_times poly_subst_power poly_subst_sum poly_subst_prod
subst_pp_restrict_indets_subst punit.monom_mult_monomial)
lemma restrict_extend_indets [simp]: "restrict_indets (extend_indets p) = p"
unfolding extend_indets_def restrict_indets_def poly_subst_poly_subst
by (rule poly_subst_id)
(simp add: extend_indets_subst_def restrict_indets_subst_def poly_subst_monomial subst_pp_single)
lemma extend_restrict_indets:
assumes "None ∉ indets p"
shows "extend_indets (restrict_indets p) = p"
unfolding extend_indets_def restrict_indets_def poly_subst_poly_subst
proof (rule poly_subst_id)
fix x
assume "x ∈ indets p"
with assms have "x ≠ None" by meson
then obtain y where x: "x = Some y" by blast
thus "poly_subst extend_indets_subst (monomial 1 (restrict_indets_subst x)) =
monomial 1 (Poly_Mapping.single x 1)"
by (simp add: extend_indets_subst_def restrict_indets_subst_def poly_subst_monomial subst_pp_single)
qed
lemma restrict_indets_dehomogenize [simp]: "restrict_indets (dehomogenize None p) = restrict_indets p"
proof -
have eq: "poly_subst (λx. (monomial 1 (restrict_indets_subst x))) (dehomo_subst None y) =
monomial 1 (restrict_indets_subst y)" for y::"'x option"
by (auto simp: restrict_indets_subst_def dehomo_subst_def poly_subst_monomial subst_pp_single)
show ?thesis by (simp only: dehomogenize_def restrict_indets_def poly_subst_poly_subst eq)
qed
corollary restrict_indets_comp_dehomogenize: "restrict_indets ∘ dehomogenize None = restrict_indets"
by (rule ext) (simp only: o_def restrict_indets_dehomogenize)
corollary extend_restrict_indets_eq_dehomogenize:
"extend_indets (restrict_indets p) = dehomogenize None p"
proof -
have "extend_indets (restrict_indets p) = extend_indets (restrict_indets (dehomogenize None p))"
by simp
also have "… = dehomogenize None p"
proof (intro extend_restrict_indets notI)
assume "None ∈ indets (dehomogenize None p)"
hence "None ∈ indets p - {None}" using indets_dehomogenize ..
thus False by simp
qed
finally show ?thesis .
qed
corollary extend_indets_comp_restrict_indets: "extend_indets ∘ restrict_indets = dehomogenize None"
by (rule ext) (simp only: o_def extend_restrict_indets_eq_dehomogenize)
lemma restrict_homogenize_extend_indets [simp]:
"restrict_indets (homogenize None (extend_indets p)) = p"
proof -
have "restrict_indets (homogenize None (extend_indets p)) =
restrict_indets (dehomogenize None (homogenize None (extend_indets p)))"
by (simp only: restrict_indets_dehomogenize)
also have "… = restrict_indets (dehomogenize None (extend_indets p))"
by (simp only: dehomogenize_homogenize)
also have "… = p" by simp
finally show ?thesis .
qed
lemma dehomogenize_extend_indets [simp]: "dehomogenize None (extend_indets p) = extend_indets p"
by (simp add: indets_extend_indets)
lemma restrict_indets_ideal: "restrict_indets ` ideal F = ideal (restrict_indets ` F)"
using restrict_indets_plus restrict_indets_times
proof (rule image_ideal_eq_surj)
from restrict_extend_indets show "surj restrict_indets" by (rule surjI)
qed
lemma ideal_restrict_indets:
"ideal G = ideal (homogenize None ` extend_indets ` F) ⟹ ideal (restrict_indets ` G) = ideal F"
by (simp flip: restrict_indets_ideal) (simp add: restrict_indets_ideal image_image)
lemma extend_indets_ideal: "extend_indets ` ideal F = ideal (extend_indets ` F) ∩ P[- {None}]"
proof -
have "extend_indets ` ideal F = extend_indets ` restrict_indets ` ideal (extend_indets ` F)"
by (simp add: restrict_indets_ideal image_image)
also have "… = ideal (extend_indets ` F) ∩ P[- {None}]"
by (simp add: extend_restrict_indets_eq_dehomogenize dehomogenize_ideal image_image)
finally show ?thesis .
qed
corollary extend_indets_ideal_subset: "extend_indets ` ideal F ⊆ ideal (extend_indets ` F)"
by (simp add: extend_indets_ideal)
subsection ‹Canonical Isomorphisms between ‹P[X,Y]› and ‹P[X][Y]›: ‹focus› and ‹flatten››
definition focus :: "'x set ⇒ (('x ⇒⇩0 nat) ⇒⇩0 'a) ⇒ (('x ⇒⇩0 nat) ⇒⇩0 ('x ⇒⇩0 nat) ⇒⇩0 'a::comm_monoid_add)"
where "focus X p = (∑t∈keys p. monomial (monomial (lookup p t) (except t X)) (except t (- X)))"
definition flatten :: "('a ⇒⇩0 'a ⇒⇩0 'b) ⇒ ('a::comm_powerprod ⇒⇩0 'b::semiring_1)"
where "flatten p = (∑t∈keys p. punit.monom_mult 1 t (lookup p t))"
lemma focus_superset:
assumes "finite A" and "keys p ⊆ A"
shows "focus X p = (∑t∈A. monomial (monomial (lookup p t) (except t X)) (except t (- X)))"
unfolding focus_def using assms by (rule sum.mono_neutral_left) (simp add: in_keys_iff)
lemma keys_focus: "keys (focus X p) = (λt. except t (- X)) ` keys p"
proof
have "keys (focus X p) ⊆ (⋃t∈keys p. keys (monomial (monomial (lookup p t) (except t X)) (except t (- X))))"
unfolding focus_def by (rule keys_sum_subset)
also have "… ⊆ (⋃t∈keys p. {except t (- X)})" by (intro UN_mono subset_refl) simp
also have "… = (λt. except t (- X)) ` keys p" by (rule UNION_singleton_eq_range)
finally show "keys (focus X p) ⊆ (λt. except t (- X)) ` keys p" .
next
{
fix s
assume "s ∈ keys p"
have "lookup (focus X p) (except s (- X)) =
(∑t∈keys p. monomial (lookup p t) (except t X) when except t (- X) = except s (- X))"
(is "_ = ?p")
by (simp only: focus_def lookup_sum lookup_single)
also have "… ≠ 0"
proof
have "lookup ?p (except s X) =
(∑t∈keys p. lookup p t when except t X = except s X ∧ except t (- X) = except s (- X))"
by (simp add: lookup_sum lookup_single when_def if_distrib if_distribR)
(metis (no_types, opaque_lifting) lookup_single_eq lookup_single_not_eq lookup_zero)
also have "… = (∑t∈{s}. lookup p t)"
proof (intro sum.mono_neutral_cong_right ballI)
fix t
assume "t ∈ keys p - {s}"
hence "t ≠ s" by simp
hence "except t X + except t (- X) ≠ except s X + except s (- X)"
by (simp flip: except_decomp)
thus "(lookup p t when except t X = except s X ∧ except t (- X) = except s (- X)) = 0"
by (auto simp: when_def)
next
from ‹s ∈ keys p› show "{s} ⊆ keys p" by simp
qed simp_all
also from ‹s ∈ keys p› have "… ≠ 0" by (simp add: in_keys_iff)
finally have "except s X ∈ keys ?p" by (simp add: in_keys_iff)
moreover assume "?p = 0"
ultimately show False by simp
qed
finally have "except s (- X) ∈ keys (focus X p)" by (simp add: in_keys_iff)
}
thus "(λt. except t (- X)) ` keys p ⊆ keys (focus X p)" by blast
qed
lemma keys_coeffs_focus_subset:
assumes "c ∈ range (lookup (focus X p))"
shows "keys c ⊆ (λt. except t X) ` keys p"
proof -
from assms obtain s where "c = lookup (focus X p) s" ..
hence "keys c = keys (lookup (focus X p) s)" by (simp only:)
also have "… ⊆ (⋃t∈keys p. keys (lookup (monomial (monomial (lookup p t) (except t X)) (except t (- X))) s))"
unfolding focus_def lookup_sum by (rule keys_sum_subset)
also from subset_refl have "… ⊆ (⋃t∈keys p. {except t X})"
by (rule UN_mono) (simp add: lookup_single when_def)
also have "… = (λt. except t X) ` keys p" by (rule UNION_singleton_eq_range)
finally show ?thesis .
qed
lemma focus_in_Polys':
assumes "p ∈ P[Y]"
shows "focus X p ∈ P[Y ∩ X]"
proof (intro PolysI subsetI)
fix t
assume "t ∈ keys (focus X p)"
then obtain s where "s ∈ keys p" and t: "t = except s (- X)" unfolding keys_focus ..
note this(1)
also from assms have "keys p ⊆ .[Y]" by (rule PolysD)
finally have "keys s ⊆ Y" by (rule PPsD)
hence "keys t ⊆ Y ∩ X" by (simp add: t keys_except le_infI1)
thus "t ∈ .[Y ∩ X]" by (rule PPsI)
qed
corollary focus_in_Polys: "focus X p ∈ P[X]"
proof -
have "p ∈ P[UNIV]" by simp
hence "focus X p ∈ P[UNIV ∩ X]" by (rule focus_in_Polys')
thus ?thesis by simp
qed
lemma focus_coeffs_subset_Polys':
assumes "p ∈ P[Y]"
shows "range (lookup (focus X p)) ⊆ P[Y - X]"
proof (intro subsetI PolysI)
fix c t
assume "c ∈ range (lookup (focus X p))"
hence "keys c ⊆ (λt. except t X) ` keys p" by (rule keys_coeffs_focus_subset)
moreover assume "t ∈ keys c"
ultimately have "t ∈ (λt. except t X) ` keys p" ..
then obtain s where "s ∈ keys p" and t: "t = except s X" ..
note this(1)
also from assms have "keys p ⊆ .[Y]" by (rule PolysD)
finally have "keys s ⊆ Y" by (rule PPsD)
hence "keys t ⊆ Y - X" by (simp add: t keys_except Diff_mono)
thus "t ∈ .[Y - X]" by (rule PPsI)
qed
corollary focus_coeffs_subset_Polys: "range (lookup (focus X p)) ⊆ P[- X]"
proof -
have "p ∈ P[UNIV]" by simp
hence "range (lookup (focus X p)) ⊆ P[UNIV - X]" by (rule focus_coeffs_subset_Polys')
thus ?thesis by (simp only: Compl_eq_Diff_UNIV)
qed
corollary lookup_focus_in_Polys: "lookup (focus X p) t ∈ P[- X]"
using focus_coeffs_subset_Polys by blast
lemma focus_zero [simp]: "focus X 0 = 0"
by (simp add: focus_def)
lemma focus_eq_zero_iff [iff]: "focus X p = 0 ⟷ p = 0"
by (simp only: keys_focus flip: keys_eq_empty_iff) simp
lemma focus_one [simp]: "focus X 1 = 1"
by (simp add: focus_def)
lemma focus_monomial: "focus X (monomial c t) = monomial (monomial c (except t X)) (except t (- X))"
by (simp add: focus_def)
lemma focus_uminus [simp]: "focus X (- p) = - focus X p"
by (simp add: focus_def keys_uminus single_uminus sum_negf)
lemma focus_plus: "focus X (p + q) = focus X p + focus X q"
proof -
have "finite (keys p ∪ keys q)" by simp
moreover have "keys (p + q) ⊆ keys p ∪ keys q" by (rule Poly_Mapping.keys_add)
ultimately show ?thesis
by (simp add: focus_superset[where A="keys p ∪ keys q"] lookup_add single_add sum.distrib)
qed
lemma focus_minus: "focus X (p - q) = focus X p - focus X (q::_ ⇒⇩0 _::ab_group_add)"
by (simp only: diff_conv_add_uminus focus_plus focus_uminus)
lemma focus_times: "focus X (p * q) = focus X p * focus X q"
proof -
have eq: "focus X (monomial c s * q) = focus X (monomial c s) * focus X q" for c s
proof -
have "focus X (monomial c s * q) = focus X (punit.monom_mult c s q)"
by (simp only: times_monomial_left)
also have "… = (∑t∈(+) s ` keys q. monomial (monomial (lookup (punit.monom_mult c s q) t)
(except t X)) (except t (- X)))"
by (rule focus_superset) (simp_all add: punit.keys_monom_mult_subset[simplified])
also have "… = (∑t∈keys q. ((λt. monomial (monomial (lookup (punit.monom_mult c s q) t)
(except t X)) (except t (- X))) ∘ ((+) s)) t)"
by (rule sum.reindex) simp
also have "… = monomial (monomial c (except s X)) (except s (- X)) *
(∑t∈keys q. monomial (monomial (lookup q t) (except t X)) (except t (- X)))"
by (simp add: o_def punit.lookup_monom_mult except_plus times_monomial_monomial sum_distrib_left)
also have "… = focus X (monomial c s) * focus X q"
by (simp only: focus_monomial focus_def[where p=q])
finally show ?thesis .
qed
show ?thesis by (induct p rule: poly_mapping_plus_induct) (simp_all add: ring_distribs focus_plus eq)
qed
lemma focus_sum: "focus X (sum f I) = (∑i∈I. focus X (f i))"
by (induct I rule: infinite_finite_induct) (simp_all add: focus_plus)
lemma focus_prod: "focus X (prod f I) = (∏i∈I. focus X (f i))"
by (induct I rule: infinite_finite_induct) (simp_all add: focus_times)
lemma focus_power [simp]: "focus X (f ^ m) = focus X f ^ m"
by (induct m) (simp_all add: focus_times)
lemma focus_Polys:
assumes "p ∈ P[X]"
shows "focus X p = (∑t∈keys p. monomial (monomial (lookup p t) 0) t)"
unfolding focus_def
proof (rule sum.cong)
fix t
assume "t ∈ keys p"
also from assms have "… ⊆ .[X]" by (rule PolysD)
finally have "keys t ⊆ X" by (rule PPsD)
hence "except t X = 0" and "except t (- X) = t" by (rule except_eq_zeroI, auto simp: except_id_iff)
thus "monomial (monomial (lookup p t) (except t X)) (except t (- X)) =
monomial (monomial (lookup p t) 0) t" by simp
qed (fact refl)
corollary lookup_focus_Polys: "p ∈ P[X] ⟹ lookup (focus X p) t = monomial (lookup p t) 0"
by (simp add: focus_Polys lookup_sum lookup_single when_def in_keys_iff)
lemma focus_Polys_Compl:
assumes "p ∈ P[- X]"
shows "focus X p = monomial p 0"
proof -
have "focus X p = (∑t∈keys p. monomial (monomial (lookup p t) t) 0)" unfolding focus_def
proof (rule sum.cong)
fix t
assume "t ∈ keys p"
also from assms have "… ⊆ .[- X]" by (rule PolysD)
finally have "keys t ⊆ - X" by (rule PPsD)
hence "except t (- X) = 0" and "except t X = t" by (rule except_eq_zeroI, auto simp: except_id_iff)
thus "monomial (monomial (lookup p t) (except t X)) (except t (- X)) =
monomial (monomial (lookup p t) t) 0" by simp
qed (fact refl)
also have "… = monomial (∑t∈keys p. monomial (lookup p t) t) 0" by (simp only: monomial_sum)
also have "… = monomial p 0" by (simp only: poly_mapping_sum_monomials)
finally show ?thesis .
qed
corollary focus_empty [simp]: "focus {} p = monomial p 0"
by (rule focus_Polys_Compl) simp
lemma focus_Int:
assumes "p ∈ P[Y]"
shows "focus (X ∩ Y) p = focus X p"
unfolding focus_def using refl
proof (rule sum.cong)
fix t
assume "t ∈ keys p"
also from assms have "… ⊆ .[Y]" by (rule PolysD)
finally have "keys t ⊆ Y" by (rule PPsD)
hence "keys t ⊆ X ∪ Y" by blast
hence "except t (X ∩ Y) = except t X + except t Y" by (rule except_Int)
also from ‹keys t ⊆ Y› have "except t Y = 0" by (rule except_eq_zeroI)
finally have eq: "except t (X ∩ Y) = except t X" by simp
have "except t (- (X ∩ Y)) = except (except t (- Y)) (- X)" by (simp add: except_except Un_commute)
also from ‹keys t ⊆ Y› have "except t (- Y) = t" by (auto simp: except_id_iff)
finally show "monomial (monomial (lookup p t) (except t (X ∩ Y))) (except t (- (X ∩ Y))) =
monomial (monomial (lookup p t) (except t X)) (except t (- X))" by (simp only: eq)
qed
lemma range_focusD:
assumes "p ∈ range (focus X)"
shows "p ∈ P[X]" and "range (lookup p) ⊆ P[- X]" and "lookup p t ∈ P[- X]"
using assms by (auto intro: focus_in_Polys lookup_focus_in_Polys)
lemma range_focusI:
assumes "p ∈ P[X]" and "lookup p ` keys (p::_ ⇒⇩0 _ ⇒⇩0 _::semiring_1) ⊆ P[- X]"
shows "p ∈ range (focus X)"
using assms
proof (induct p rule: poly_mapping_plus_induct_Polys)
case 0
show ?case by simp
next
case (plus p c t)
from plus.hyps(3) have 1: "keys (monomial c t) = {t}" by simp
also from plus.hyps(4) have "… ∩ keys p = {}" by simp
finally have "keys (monomial c t + p) = keys (monomial c t) ∪ keys p" by (rule keys_add[symmetric])
hence 2: "keys (monomial c t + p) = insert t (keys p)" by (simp only: 1 flip: insert_is_Un)
from ‹t ∈ .[X]› have "keys t ⊆ X" by (rule PPsD)
hence eq1: "except t X = 0" and eq2: "except t (- X) = t"
by (rule except_eq_zeroI, auto simp: except_id_iff)
from plus.hyps(3, 4) plus.prems have "c ∈ P[- X]" and "lookup p ` keys p ⊆ P[- X]"
by (simp_all add: 2 lookup_add lookup_single in_keys_iff)
(smt (verit) add.commute add.right_neutral image_cong plus.hyps(4) when_simps(2))
from this(2) have "p ∈ range (focus X)" by (rule plus.hyps)
then obtain q where p: "p = focus X q" ..
moreover from ‹c ∈ P[- X]› have "monomial c t = focus X (monomial 1 t * c)"
by (simp add: focus_times focus_monomial eq1 eq2 focus_Polys_Compl times_monomial_monomial)
ultimately have "monomial c t + p = focus X (monomial 1 t * c + q)" by (simp only: focus_plus)
thus ?case by (rule range_eqI)
qed
lemma inj_focus: "inj ((focus X) :: (('x ⇒⇩0 nat) ⇒⇩0 'a::ab_group_add) ⇒ _)"
proof (rule injI)
fix p q :: "('x ⇒⇩0 nat) ⇒⇩0 'a"
assume "focus X p = focus X q"
hence "focus X (p - q) = 0" by (simp add: focus_minus)
thus "p = q" by simp
qed
lemma flatten_superset:
assumes "finite A" and "keys p ⊆ A"
shows "flatten p = (∑t∈A. punit.monom_mult 1 t (lookup p t))"
unfolding flatten_def using assms by (rule sum.mono_neutral_left) (simp add: in_keys_iff)
lemma keys_flatten_subset: "keys (flatten p) ⊆ (⋃t∈keys p. (+) t ` keys (lookup p t))"
proof -
have "keys (flatten p) ⊆ (⋃t∈keys p. keys (punit.monom_mult 1 t (lookup p t)))"
unfolding flatten_def by (rule keys_sum_subset)
also from subset_refl have "… ⊆ (⋃t∈keys p. (+) t ` keys (lookup p t))"
by (rule UN_mono) (rule punit.keys_monom_mult_subset[simplified])
finally show ?thesis .
qed
lemma flatten_in_Polys:
assumes "p ∈ P[X]" and "lookup p ` keys p ⊆ P[Y]"
shows "flatten p ∈ P[X ∪ Y]"
proof (intro PolysI subsetI)
fix t
assume "t ∈ keys (flatten p)"
also have "… ⊆ (⋃t∈keys p. (+) t ` keys (lookup p t))" by (rule keys_flatten_subset)
finally obtain s where "s ∈ keys p" and "t ∈ (+) s ` keys (lookup p s)" ..
from this(2) obtain s' where "s' ∈ keys (lookup p s)" and t: "t = s + s'" ..
from assms(1) have "keys p ⊆ .[X]" by (rule PolysD)
with ‹s ∈ keys p› have "s ∈ .[X]" ..
also have "… ⊆ .[X ∪ Y]" by (rule PPs_mono) simp
finally have 1: "s ∈ .[X ∪ Y]" .
from ‹s ∈ keys p› have "lookup p s ∈ lookup p ` keys p" by (rule imageI)
also have "… ⊆ P[Y]" by fact
finally have "keys (lookup p s) ⊆ .[Y]" by (rule PolysD)
with ‹s' ∈ _› have "s' ∈ .[Y]" ..
also have "… ⊆ .[X ∪ Y]" by (rule PPs_mono) simp
finally have "s' ∈ .[X ∪ Y]" .
with 1 show "t ∈ .[X ∪ Y]" unfolding t by (rule PPs_closed_plus)
qed
lemma flatten_zero [simp]: "flatten 0 = 0"
by (simp add: flatten_def)
lemma flatten_one [simp]: "flatten 1 = 1"
by (simp add: flatten_def)
lemma flatten_monomial: "flatten (monomial c t) = punit.monom_mult 1 t c"
by (simp add: flatten_def)
lemma flatten_uminus [simp]: "flatten (- p) = - flatten (p::_ ⇒⇩0 _ ⇒⇩0 _::ring)"
by (simp add: flatten_def keys_uminus punit.monom_mult_uminus_right sum_negf)
lemma flatten_plus: "flatten (p + q) = flatten p + flatten q"
proof -
have "finite (keys p ∪ keys q)" by simp
moreover have "keys (p + q) ⊆ keys p ∪ keys q" by (rule Poly_Mapping.keys_add)
ultimately show ?thesis
by (simp add: flatten_superset[where A="keys p ∪ keys q"] punit.monom_mult_dist_right lookup_add
sum.distrib)
qed
lemma flatten_minus: "flatten (p - q) = flatten p - flatten (q::_ ⇒⇩0 _ ⇒⇩0 _::ring)"
by (simp only: diff_conv_add_uminus flatten_plus flatten_uminus)
lemma flatten_times: "flatten (p * q) = flatten p * flatten (q::_ ⇒⇩0 _ ⇒⇩0 'b::comm_semiring_1)"
proof -
have eq: "flatten (monomial c s * q) = flatten (monomial c s) * flatten q" for c s
proof -
have eq: "monomial 1 (t + s) = monomial 1 s * monomial (1::'b) t" for t
by (simp add: times_monomial_monomial add.commute)
have "flatten (monomial c s * q) = flatten (punit.monom_mult c s q)"
by (simp only: times_monomial_left)
also have "… = (∑t∈(+) s ` keys q. punit.monom_mult 1 t (lookup (punit.monom_mult c s q) t))"
by (rule flatten_superset) (simp_all add: punit.keys_monom_mult_subset[simplified])
also have "… = (∑t∈keys q. ((λt. punit.monom_mult 1 t (lookup (punit.monom_mult c s q) t)) ∘ (+) s) t)"
by (rule sum.reindex) simp
thm times_monomial_left
also have "… = punit.monom_mult 1 s c *
(∑t∈keys q. punit.monom_mult 1 t (lookup q t))"
by (simp add: o_def punit.lookup_monom_mult sum_distrib_left)
(simp add: algebra_simps eq flip: times_monomial_left)
also have "… = flatten (monomial c s) * flatten q"
by (simp only: flatten_monomial flatten_def[where p=q])
finally show ?thesis .
qed
show ?thesis by (induct p rule: poly_mapping_plus_induct) (simp_all add: ring_distribs flatten_plus eq)
qed
lemma flatten_monom_mult:
"flatten (punit.monom_mult c t p) = punit.monom_mult 1 t (c * flatten (p::_ ⇒⇩0 _ ⇒⇩0 'b::comm_semiring_1))"
by (simp only: flatten_times flatten_monomial mult.assoc flip: times_monomial_left)
lemma flatten_sum: "flatten (sum f I) = (∑i∈I. flatten (f i))"
by (induct I rule: infinite_finite_induct) (simp_all add: flatten_plus)
lemma flatten_prod: "flatten (prod f I) = (∏i∈I. flatten (f i :: _ ⇒⇩0 _::comm_semiring_1))"
by (induct I rule: infinite_finite_induct) (simp_all add: flatten_times)
lemma flatten_power [simp]: "flatten (f ^ m) = flatten (f:: _ ⇒⇩0 _::comm_semiring_1) ^ m"
by (induct m) (simp_all add: flatten_times)
lemma surj_flatten: "surj flatten"
proof (rule surjI)
fix p
show "flatten (monomial p 0) = p" by (simp add: flatten_monomial)
qed
lemma flatten_focus [simp]: "flatten (focus X p) = p"
by (induct p rule: poly_mapping_plus_induct)
(simp_all add: focus_plus flatten_plus focus_monomial flatten_monomial
punit.monom_mult_monomial add.commute flip: except_decomp)
lemma focus_flatten:
assumes "p ∈ P[X]" and "lookup p ` keys p ⊆ P[- X]"
shows "focus X (flatten p) = p"
proof -
from assms have "p ∈ range (focus X)" by (rule range_focusI)
then obtain q where "p = focus X q" ..
thus ?thesis by simp
qed
lemma image_focus_ideal: "focus X ` ideal F = ideal (focus X ` F) ∩ range (focus X)"
proof
from focus_plus focus_times have "focus X ` ideal F ⊆ ideal (focus X ` F)"
by (rule image_ideal_subset)
moreover from subset_UNIV have "focus X ` ideal F ⊆ range (focus X)" by (rule image_mono)
ultimately show "focus X ` ideal F ⊆ ideal (focus X ` F) ∩ range (focus X)" by blast
next
show "ideal (focus X ` F) ∩ range (focus X) ⊆ focus X ` ideal F"
proof
fix p
assume "p ∈ ideal (focus X ` F) ∩ range (focus X)"
hence "p ∈ ideal (focus X ` F)" and "p ∈ range (focus X)" by simp_all
from this(1) obtain F0 q where "F0 ⊆ focus X ` F" and p: "p = (∑f'∈F0. q f' * f')"
by (rule ideal.spanE)
from this(1) obtain F' where "F' ⊆ F" and F0: "F0 = focus X ` F'" by (rule subset_imageE)
from inj_focus subset_UNIV have "inj_on (focus X) F'" by (rule inj_on_subset)
from ‹p ∈ range _› obtain p' where "p = focus X p'" ..
hence "p = focus X (flatten p)" by simp
also from ‹inj_on _ F'› have "… = focus X (∑f'∈F'. flatten (q (focus X f')) * f')"
by (simp add: p F0 sum.reindex flatten_sum flatten_times)
finally have "p = focus X (∑f'∈F'. flatten (q (focus X f')) * f')" .
moreover have "(∑f'∈F'. flatten (q (focus X f')) * f') ∈ ideal F"
proof
show "(∑f'∈F'. flatten (q (focus X f')) * f') ∈ ideal F'" by (rule ideal.sum_in_spanI)
next
from ‹F' ⊆ F› show "ideal F' ⊆ ideal F" by (rule ideal.span_mono)
qed
ultimately show "p ∈ focus X ` ideal F" by (rule image_eqI)
qed
qed
lemma image_flatten_ideal: "flatten ` ideal F = ideal (flatten ` F)"
using flatten_plus flatten_times surj_flatten by (rule image_ideal_eq_surj)
lemma poly_eval_focus:
"poly_eval a (focus X p) = poly_subst (λx. if x ∈ X then a x else monomial 1 (Poly_Mapping.single x 1)) p"
proof -
let ?b = "λx. if x ∈ X then a x else monomial 1 (Poly_Mapping.single x 1)"
have *: "lookup (punit.monom_mult (monomial (lookup p t) (except t X)) 0
(subst_pp (λx. monomial (a x) 0) (except t (- X)))) 0 =
punit.monom_mult (lookup p t) 0 (subst_pp ?b t)" for t
proof -
have 1: "subst_pp ?b (except t X) = monomial 1 (except t X)"
by (rule subst_pp_id) (simp add: keys_except)
from refl have 2: "subst_pp ?b (except t (- X)) = subst_pp a (except t (-X))"
by (rule subst_pp_cong) (simp add: keys_except)
have "lookup (punit.monom_mult (monomial (lookup p t) (except t X)) 0
(subst_pp (λx. monomial (a x) 0) (except t (- X)))) 0 =
punit.monom_mult (lookup p t) (except t X) (subst_pp a (except t (- X)))"
by (simp add: lookup_times_zero subst_pp_def lookup_prod_zero lookup_power_zero
flip: times_monomial_left)
also have "… = punit.monom_mult (lookup p t) 0 (monomial 1 (except t X) * subst_pp a (except t (- X)))"
by (simp add: times_monomial_monomial flip: times_monomial_left mult.assoc)
also have "… = punit.monom_mult (lookup p t) 0 (subst_pp ?b (except t X + except t (- X)))"
by (simp only: subst_pp_plus 1 2)
also have "… = punit.monom_mult (lookup p t) 0 (subst_pp ?b t)" by (simp flip: except_decomp)
finally show ?thesis .
qed
show ?thesis by (simp add: poly_eval_def focus_def poly_subst_sum lookup_sum poly_subst_monomial *
flip: poly_subst_def)
qed
corollary poly_eval_poly_eval_focus:
"poly_eval a (poly_eval b (focus X p)) = poly_eval (λx::'x. if x ∈ X then poly_eval a (b x) else a x) p"
proof -
have eq: "monomial (lookup (poly_subst (λy. monomial (a y) (0::'x ⇒⇩0 nat)) q) 0) 0 =
poly_subst (λy. monomial (a y) (0::'x ⇒⇩0 nat)) q" for q
by (intro poly_deg_zero_imp_monomial poly_deg_poly_subst_eq_zeroI) simp
show ?thesis unfolding poly_eval_focus
by (simp add: poly_eval_def poly_subst_poly_subst if_distrib poly_subst_monomial subst_pp_single eq
cong: if_cong)
qed
lemma indets_poly_eval_focus_subset:
"indets (poly_eval a (focus X p)) ⊆ ⋃ (indets ` a ` X) ∪ (indets p - X)"
proof
fix x
assume "x ∈ indets (poly_eval a (focus X p))"
also have "… = indets (poly_subst (λx. if x ∈ X then a x else monomial 1 (Poly_Mapping.single x 1)) p)"
(is "_ = indets (poly_subst ?f _)") by (simp only: poly_eval_focus)
finally obtain y where "y ∈ indets p" and "x ∈ indets (?f y)" by (rule in_indets_poly_substE)
from this(2) have "(x ∉ X ∧ x = y) ∨ (y ∈ X ∧ x ∈ indets (a y))"
by (simp add: indets_monomial split: if_split_asm)
thus "x ∈ ⋃ (indets ` a ` X) ∪ (indets p - X)"
proof (elim disjE conjE)
assume "x ∉ X" and "x = y"
with ‹y ∈ indets p› have "x ∈ indets p - X" by simp
thus ?thesis ..
next
assume "y ∈ X" and "x ∈ indets (a y)"
hence "x ∈ ⋃ (indets ` a ` X)" by blast
thus ?thesis ..
qed
qed
lemma lookup_poly_eval_focus:
"lookup (poly_eval (λx. monomial (a x) 0) (focus X p)) t = poly_eval a (lookup (focus (- X) p) t)"
proof -
let ?f = "λx. if x ∈ X then monomial (a x) 0 else monomial 1 (Poly_Mapping.single x 1)"
have eq: "subst_pp ?f s = monomial (∏x∈keys s ∩ X. a x ^ lookup s x) (except s X)" for s
proof -
have "subst_pp ?f s = (∏x∈(keys s ∩ X) ∪ (keys s - X). ?f x ^ lookup s x)"
unfolding subst_pp_def by (rule prod.cong) blast+
also have "… = (∏x∈keys s ∩ X. ?f x ^ lookup s x) * (∏x∈keys s - X. ?f x ^ lookup s x)"
by (rule prod.union_disjoint) auto
also have "… = monomial (∏x∈keys s ∩ X. a x ^ lookup s x)
(∑x∈keys s - X. Poly_Mapping.single x (lookup s x))"
by (simp add: monomial_power_map_scale times_monomial_monomial flip: punit.monomial_prod_sum)
also have "(∑x∈keys s - X. Poly_Mapping.single x (lookup s x)) = except s X"
by (metis (mono_tags, lifting) DiffD2 keys_except lookup_except_eq_idI
poly_mapping_sum_monomials sum.cong)
finally show ?thesis .
qed
show ?thesis
by (simp add: poly_eval_focus poly_subst_def lookup_sum eq flip: punit.map_scale_eq_monom_mult)
(simp add: focus_def lookup_sum poly_eval_sum lookup_single when_distrib poly_eval_monomial
keys_except lookup_except_when)
qed
lemma keys_poly_eval_focus_subset:
"keys (poly_eval (λx. monomial (a x) 0) (focus X p)) ⊆ (λt. except t X) ` keys p"
proof
fix t
assume "t ∈ keys (poly_eval (λx. monomial (a x) 0) (focus X p))"
hence "lookup (poly_eval (λx. monomial (a x) 0) (focus X p)) t ≠ 0" by (simp add: in_keys_iff)
hence "poly_eval a (lookup (focus (- X) p) t) ≠ 0" by (simp add: lookup_poly_eval_focus)
hence "t ∈ keys (focus (- X) p)" by (auto simp flip: lookup_not_eq_zero_eq_in_keys)
thus "t ∈ (λt. except t X) ` keys p" by (simp add: keys_focus)
qed
lemma poly_eval_focus_in_Polys:
assumes "p ∈ P[X]"
shows "poly_eval (λx. monomial (a x) 0) (focus Y p) ∈ P[X - Y]"
proof (rule PolysI_alt)
have "indets (poly_eval (λx. monomial (a x) 0) (focus Y p)) ⊆
⋃ (indets ` (λx. monomial (a x) 0) ` Y) ∪ (indets p - Y)"
by (fact indets_poly_eval_focus_subset)
also have "… = indets p - Y" by simp
also from assms have "… ⊆ X - Y" by (auto dest: PolysD)
finally show "indets (poly_eval (λx. monomial (a x) 0) (focus Y p)) ⊆ X - Y" .
qed
lemma image_poly_eval_focus_ideal:
"poly_eval (λx. monomial (a x) 0) ` focus X ` ideal F =
ideal (poly_eval (λx. monomial (a x) 0) ` focus X ` F) ∩
(P[- X]::(('x ⇒⇩0 nat) ⇒⇩0 'a::comm_ring_1) set)"
proof -
let ?h = "λf. poly_eval (λx. monomial (a x) 0) (focus X f)"
have h_id: "?h p = p" if "p ∈ P[- X]" for p
proof -
from that have "focus X p ∈ P[- X ∩ X]" by (rule focus_in_Polys')
also have "… = P[{}]" by simp
finally obtain c where eq: "focus X p = monomial c 0" unfolding Polys_empty ..
hence "flatten (focus X p) = flatten (monomial c 0)" by (rule arg_cong)
hence "c = p" by (simp add: flatten_monomial)
thus "?h p = p" by (simp add: eq poly_eval_monomial)
qed
have rng: "range ?h = P[- X]"
proof (intro subset_antisym subsetI, elim rangeE)
fix b f
assume b: "b = ?h f"
have "?h f ∈ P[UNIV - X]" by (rule poly_eval_focus_in_Polys) simp
thus "b ∈ P[- X]" by (simp add: b Compl_eq_Diff_UNIV)
next
fix p :: "('x ⇒⇩0 nat) ⇒⇩0 'a"
assume "p ∈ P[- X]"
hence "?h p = p" by (rule h_id)
hence "p = ?h p" by (rule sym)
thus "p ∈ range ?h" by (rule range_eqI)
qed
have "poly_eval (λx. monomial (a x) 0) ` focus X ` ideal F = ?h ` ideal F" by (fact image_image)
also have "… = ideal (?h ` F) ∩ range ?h"
proof (rule image_ideal_eq_Int)
fix p
have "?h p ∈ range ?h" by (fact rangeI)
also have "… = P[- X]" by fact
finally show "?h (?h p) = ?h p" by (rule h_id)
qed (simp_all only: focus_plus poly_eval_plus focus_times poly_eval_times)
also have "… = ideal (poly_eval (λx. monomial (a x) 0) ` focus X ` F) ∩ P[- X]"
by (simp only: image_image rng)
finally show ?thesis .
qed
subsection ‹Locale @{term pm_powerprod}›
lemma varnum_eq_zero_iff: "varnum X t = 0 ⟷ t ∈ .[X]"
by (auto simp: varnum_def PPs_def)
lemma dgrad_set_varnum: "dgrad_set (varnum X) 0 = .[X]"
by (simp add: dgrad_set_def PPs_def varnum_eq_zero_iff)
context ordered_powerprod
begin
abbreviation "lcf ≡ punit.lc"
abbreviation "tcf ≡ punit.tc"
abbreviation "lpp ≡ punit.lt"
abbreviation "tpp ≡ punit.tt"
end
locale pm_powerprod =
ordered_powerprod ord ord_strict
for ord::"('x::{countable,linorder} ⇒⇩0 nat) ⇒ ('x ⇒⇩0 nat) ⇒ bool" (infixl ‹≼› 50)
and ord_strict (infixl ‹≺› 50)
begin
sublocale gd_powerprod ..
lemma PPs_closed_lpp:
assumes "p ∈ P[X]"
shows "lpp p ∈ .[X]"
proof (cases "p = 0")
case True
thus ?thesis by (simp add: zero_in_PPs)
next
case False
hence "lpp p ∈ keys p" by (rule punit.lt_in_keys)
also from assms have "… ⊆ .[X]" by (rule PolysD)
finally show ?thesis .
qed
lemma PPs_closed_tpp:
assumes "p ∈ P[X]"
shows "tpp p ∈ .[X]"
proof (cases "p = 0")
case True
thus ?thesis by (simp add: zero_in_PPs)
next
case False
hence "tpp p ∈ keys p" by (rule punit.tt_in_keys)
also from assms have "… ⊆ .[X]" by (rule PolysD)
finally show ?thesis .
qed
corollary PPs_closed_image_lpp: "F ⊆ P[X] ⟹ lpp ` F ⊆ .[X]"
by (auto intro: PPs_closed_lpp)
corollary PPs_closed_image_tpp: "F ⊆ P[X] ⟹ tpp ` F ⊆ .[X]"
by (auto intro: PPs_closed_tpp)
lemma hom_component_lpp:
assumes "p ≠ 0"
shows "hom_component p (deg_pm (lpp p)) ≠ 0" (is "?p ≠ 0")
and "lpp (hom_component p (deg_pm (lpp p))) = lpp p"
proof -
from assms have "lpp p ∈ keys p" by (rule punit.lt_in_keys)
hence *: "lpp p ∈ keys ?p" by (simp add: keys_hom_component)
thus "?p ≠ 0" by auto
from * show "lpp ?p = lpp p"
proof (rule punit.lt_eqI_keys)
fix t
assume "t ∈ keys ?p"
hence "t ∈ keys p" by (simp add: keys_hom_component)
thus "t ≼ lpp p" by (rule punit.lt_max_keys)
qed
qed
definition is_hom_ord :: "'x ⇒ bool"
where "is_hom_ord x ⟷ (∀s t. deg_pm s = deg_pm t ⟶ (s ≼ t ⟷ except s {x} ≼ except t {x}))"
lemma is_hom_ordD: "is_hom_ord x ⟹ deg_pm s = deg_pm t ⟹ s ≼ t ⟷ except s {x} ≼ except t {x}"
by (simp add: is_hom_ord_def)
lemma dgrad_p_set_varnum: "punit.dgrad_p_set (varnum X) 0 = P[X]"
by (simp add: punit.dgrad_p_set_def dgrad_set_varnum Polys_def)
end
text ‹We must create a copy of @{locale pm_powerprod} to avoid infinite chains of interpretations.›
instantiation option :: (linorder) linorder
begin
fun less_eq_option :: "'a option ⇒ 'a option ⇒ bool" where
"less_eq_option None _ = True" |
"less_eq_option (Some x) None = False" |
"less_eq_option (Some x) (Some y) = (x ≤ y)"
definition less_option :: "'a option ⇒ 'a option ⇒ bool"
where "less_option x y ⟷ x ≤ y ∧ ¬ y ≤ x"
instance proof
fix x :: "'a option"
show "x ≤ x" using less_eq_option.elims(3) by fastforce
qed (auto simp: less_option_def elim!: less_eq_option.elims)
end
locale extended_ord_pm_powerprod = pm_powerprod
begin
definition extended_ord :: "('a option ⇒⇩0 nat) ⇒ ('a option ⇒⇩0 nat) ⇒ bool"
where "extended_ord s t ⟷ (restrict_indets_pp s ≺ restrict_indets_pp t ∨
(restrict_indets_pp s = restrict_indets_pp t ∧ lookup s None ≤ lookup t None))"
definition extended_ord_strict :: "('a option ⇒⇩0 nat) ⇒ ('a option ⇒⇩0 nat) ⇒ bool"
where "extended_ord_strict s t ⟷ (restrict_indets_pp s ≺ restrict_indets_pp t ∨
(restrict_indets_pp s = restrict_indets_pp t ∧ lookup s None < lookup t None))"
sublocale extended_ord: pm_powerprod extended_ord extended_ord_strict
proof -
have 1: "s = t" if "lookup s None = lookup t None" and "restrict_indets_pp s = restrict_indets_pp t"
for s t :: "'a option ⇒⇩0 nat"
proof (rule poly_mapping_eqI)
fix y
show "lookup s y = lookup t y"
proof (cases y)
case None
with that(1) show ?thesis by simp
next
case y: (Some z)
have "lookup s y = lookup (restrict_indets_pp s) z" by (simp only: lookup_restrict_indets_pp y)
also have "… = lookup (restrict_indets_pp t) z" by (simp only: that(2))
also have "… = lookup t y" by (simp only: lookup_restrict_indets_pp y)
finally show ?thesis .
qed
qed
have 2: "0 ≺ t" if "t ≠ 0" for t::"'a ⇒⇩0 nat"
using that zero_min by (rule ordered_powerprod_lin.dual_order.not_eq_order_implies_strict)
show "pm_powerprod extended_ord extended_ord_strict"
by standard (auto simp: extended_ord_def extended_ord_strict_def restrict_indets_pp_plus lookup_add 1
dest: plus_monotone_strict 2)
qed
lemma extended_ord_is_hom_ord: "extended_ord.is_hom_ord None"
by (auto simp add: extended_ord_def lookup_restrict_indets_pp lookup_except extended_ord.is_hom_ord_def
simp flip: deg_pm_restrict_indets_pp)
end
end