# Theory Symmetric_Polynomials.Symmetric_Polynomials

```(*
File:     Symmetric_Polynomials.thy
Author:   Manuel Eberl (TU München)

The definition of symmetric polynomials and the elementary symmetric polynomials.
Proof of the fundamental theorem of symmetric polynomials and its corollaries.
*)
section ‹Symmetric Polynomials›
theory Symmetric_Polynomials
imports
Vieta
"Polynomials.More_MPoly_Type"
"HOL-Combinatorics.Permutations"
begin

subsection ‹Auxiliary facts›

(*
TODO: Many of these facts and definitions should be moved elsewhere, especially
the ones on polynomials (leading monomial, mapping, insertion etc.)
*)

text ‹
An infinite set has infinitely many infinite subsets.
›
lemma infinite_infinite_subsets:
assumes "infinite A"
shows   "infinite {X. X ⊆ A ∧ infinite X}"
proof -
have "∀k. ∃X. X ⊆ A ∧ infinite X ∧ card (A - X) = k" for k :: nat
proof
fix k :: nat obtain Y where "finite Y" "card Y = k" "Y ⊆ A"
using infinite_arbitrarily_large[of A k] assms by auto
moreover from this have "A - (A - Y) = Y" by auto
ultimately show "∃X. X ⊆ A ∧ infinite X ∧ card (A - X) = k"
using assms by (intro exI[of _ "A - Y"]) auto
qed
from choice[OF this] obtain f
where f: "⋀k. f k ⊆ A ∧ infinite (f k) ∧ card (A - f k) = k" by blast
have "k = l" if "f k = f l" for k l
proof (rule ccontr)
assume "k ≠ l"
hence "card (A - f k) ≠ card (A - f l)"
using f[of k] f[of l] by auto
with ‹f k = f l› show False by simp
qed
hence "inj f" by (auto intro: injI)
moreover have "range f ⊆ {X. X ⊆ A ∧ infinite X}"
using f by auto
ultimately show ?thesis
by (subst infinite_iff_countable_subset) auto
qed

text ‹
An infinite set contains infinitely many finite subsets of any fixed nonzero cardinality.
›
lemma infinite_card_subsets:
assumes "infinite A" "k > 0"
shows   "infinite {X. X ⊆ A ∧ finite X ∧ card X = k}"
proof -
obtain B where B: "B ⊆ A" "finite B" "card B = k - 1"
using infinite_arbitrarily_large[OF assms(1), of "k - 1"] by blast
define f where "f = (λx. insert x B)"
have "f ` (A - B) ⊆ {X. X ⊆ A ∧ finite X ∧ card X = k}"
using assms B by (auto simp: f_def)
moreover have "inj_on f (A - B)"
by (auto intro!: inj_onI simp: f_def)
hence "infinite (f ` (A - B))"
using assms B by (subst finite_image_iff) auto
ultimately show ?thesis
by (rule infinite_super)
qed

lemma comp_bij_eq_iff:
assumes "bij f"
shows   "g ∘ f = h ∘ f ⟷ g = h"
proof
assume *: "g ∘ f = h ∘ f"
show "g = h"
proof
fix x
obtain y where [simp]: "x = f y" using bij_is_surj[OF assms] by auto
have "(g ∘ f) y = (h ∘ f) y" by (simp only: *)
thus "g x = h x" by simp
qed
qed auto

lemma sum_list_replicate [simp]:
"sum_list (replicate n x) = of_nat n * (x :: 'a :: semiring_1)"
by (induction n) (auto simp: algebra_simps)

lemma ex_subset_of_card:
assumes "finite A" "card A ≥ k"
shows   "∃B. B ⊆ A ∧ card B = k"
using assms
proof (induction arbitrary: k rule: finite_induct)
case empty
thus ?case by auto
next
case (insert x A k)
show ?case
proof (cases "k = 0")
case True
thus ?thesis by (intro exI[of _ "{}"]) auto
next
case False
from insert have "∃B⊆A. card B = k - 1" by (intro insert.IH) auto
then obtain B where B: "B ⊆ A" "card B = k - 1" by auto
with insert have [simp]: "x ∉ B" by auto
have "insert x B ⊆ insert x A"
using B insert by auto
moreover have "card (insert x B) = k"
using insert B finite_subset[of B A] False by (subst card.insert_remove) auto
ultimately show ?thesis by blast
qed
qed

lemma length_sorted_list_of_set [simp]: "length (sorted_list_of_set A) = card A"
using distinct_card[of "sorted_list_of_set A"] by (cases "finite A") simp_all

lemma upt_add_eq_append': "i ≤ j ⟹ j ≤ k ⟹ [i..<k] = [i..<j] @ [j..<k]"
using upt_add_eq_append[of i j "k - j"] by simp

subsection ‹Subrings and ring homomorphisms›

locale ring_closed =
fixes A :: "'a :: comm_ring_1 set"
assumes zero_closed [simp]: "0 ∈ A"
assumes one_closed [simp]: "1 ∈ A"
assumes add_closed [simp]: "x ∈ A ⟹ y ∈ A ⟹ (x + y) ∈ A"
assumes mult_closed [simp]: "x ∈ A ⟹ y ∈ A ⟹ (x * y) ∈ A"
assumes uminus_closed [simp]: "x ∈ A ⟹ -x ∈ A"
begin

lemma minus_closed [simp]: "x ∈ A ⟹ y ∈ A ⟹ x - y ∈ A"
using add_closed[of x "-y"] uminus_closed[of y] by auto

lemma sum_closed [intro]: "(⋀x. x ∈ X ⟹ f x ∈ A) ⟹ sum f X ∈ A"
by (induction X rule: infinite_finite_induct) auto

lemma power_closed [intro]: "x ∈ A ⟹ x ^ n ∈ A"
by (induction n) auto

lemma Sum_any_closed [intro]: "(⋀x. f x ∈ A) ⟹ Sum_any f ∈ A"
unfolding Sum_any.expand_set by (rule sum_closed)

lemma prod_closed [intro]: "(⋀x. x ∈ X ⟹ f x ∈ A) ⟹ prod f X ∈ A"
by (induction X rule: infinite_finite_induct) auto

lemma Prod_any_closed [intro]: "(⋀x. f x ∈ A) ⟹ Prod_any f ∈ A"
unfolding Prod_any.expand_set by (rule prod_closed)

lemma prod_fun_closed [intro]: "(⋀x. f x ∈ A) ⟹ (⋀x. g x ∈ A) ⟹ prod_fun f g x ∈ A"
by (auto simp: prod_fun_def when_def intro!: Sum_any_closed mult_closed)

lemma of_nat_closed [simp, intro]: "of_nat n ∈ A"
by (induction n) auto

lemma of_int_closed [simp, intro]: "of_int n ∈ A"
by (induction n) auto

end

locale ring_homomorphism =
fixes f :: "'a :: comm_ring_1 ⇒ 'b :: comm_ring_1"
assumes add[simp]: "f (x + y) = f x + f y"
assumes uminus[simp]: "f (-x) = -f x"
assumes mult[simp]: "f (x * y) = f x * f y"
assumes zero[simp]: "f 0 = 0"
assumes one [simp]: "f 1 = 1"
begin

lemma diff [simp]: "f (x - y) = f x - f y"

lemma power [simp]: "f (x ^ n) = f x ^ n"
by (induction n) auto

lemma sum [simp]: "f (sum g A) = (∑x∈A. f (g x))"
by (induction A rule: infinite_finite_induct) auto

lemma prod [simp]: "f (prod g A) = (∏x∈A. f (g x))"
by (induction A rule: infinite_finite_induct) auto

end

lemma ring_homomorphism_id [intro]: "ring_homomorphism id"
by standard auto

lemma ring_homomorphism_id' [intro]: "ring_homomorphism (λx. x)"
by standard auto

lemma ring_homomorphism_of_int [intro]: "ring_homomorphism of_int"
by standard auto

subsection ‹Various facts about multivariate polynomials›

lemma poly_mapping_nat_ge_0 [simp]: "(m :: nat ⇒⇩0 nat) ≥ 0"
proof (cases "m = 0")
case False
hence "Poly_Mapping.lookup m ≠ Poly_Mapping.lookup 0" by transfer auto
hence "∃k. Poly_Mapping.lookup m k ≠ 0" by (auto simp: fun_eq_iff)
from LeastI_ex[OF this] Least_le[of "λk. Poly_Mapping.lookup m k ≠ 0"] show ?thesis
by (force simp: less_eq_poly_mapping_def less_fun_def)
qed auto

lemma poly_mapping_nat_le_0 [simp]: "(m :: nat ⇒⇩0 nat) ≤ 0 ⟷ m = 0"
unfolding less_eq_poly_mapping_def poly_mapping_eq_iff less_fun_def by auto

lemma of_nat_diff_poly_mapping_nat:
assumes "m ≥ n"
shows   "of_nat (m - n) = (of_nat m - of_nat n :: 'a :: monoid_add ⇒⇩0 nat)"
by (auto intro!: poly_mapping_eqI simp: lookup_of_nat lookup_minus when_def)

lemma mpoly_coeff_transfer [transfer_rule]:
"rel_fun cr_mpoly (=) poly_mapping.lookup MPoly_Type.coeff"
unfolding MPoly_Type.coeff_def by transfer_prover

lemma mapping_of_sum: "(∑x∈A. mapping_of (f x)) = mapping_of (sum f A)"
by (induction A rule: infinite_finite_induct) (auto simp: plus_mpoly.rep_eq zero_mpoly.rep_eq)

lemma mapping_of_eq_0_iff [simp]: "mapping_of p = 0 ⟷ p = 0"
by transfer auto

lemma Sum_any_mapping_of: "Sum_any (λx. mapping_of (f x)) = mapping_of (Sum_any f)"

lemma Sum_any_parametric_cr_mpoly [transfer_rule]:
"(rel_fun (rel_fun (=) cr_mpoly) cr_mpoly) Sum_any Sum_any"
by (auto simp: rel_fun_def cr_mpoly_def Sum_any_mapping_of)

lemma lookup_mult_of_nat [simp]: "lookup (of_nat n * m) k = n * lookup m k"
proof -
have "of_nat n * m = (∑i<n. m)" by simp
also have "lookup … k = (∑i<n. lookup m k)"
by (simp only: lookup_sum)
also have "… = n * lookup m k"
by simp
finally show ?thesis .
qed

lemma mpoly_eqI:
assumes "⋀mon. MPoly_Type.coeff p mon = MPoly_Type.coeff q mon"
shows   "p = q"
using assms by (transfer, transfer) (auto simp: fun_eq_iff)

lemma coeff_mpoly_times:
"MPoly_Type.coeff (p * q) mon = prod_fun (MPoly_Type.coeff p) (MPoly_Type.coeff q) mon"
by (transfer', transfer') auto

lemma (in ring_closed) coeff_mult_closed [intro]:
"(⋀x. coeff p x ∈ A) ⟹ (⋀x. coeff q x ∈ A) ⟹ coeff (p * q) x ∈ A"
by (auto simp: coeff_mpoly_times prod_fun_closed)

lemma coeff_notin_vars:
assumes "¬(keys m ⊆ vars p)"
shows   "coeff p m = 0"
using assms unfolding vars_def by transfer' (auto simp: in_keys_iff)

lemma finite_coeff_support [intro]: "finite {m. coeff p m ≠ 0}"
by transfer simp

lemma insertion_altdef:
"insertion f p = Sum_any (λm. coeff p m * Prod_any (λi. f i ^ lookup m i))"
by (transfer', transfer') (simp add: insertion_fun_def)

lemma mpoly_coeff_uminus [simp]: "coeff (-p) m = -coeff p m"
by transfer auto

lemma Sum_any_uminus: "Sum_any (λx. -f x :: 'a :: ab_group_add) = -Sum_any f"

lemma insertion_uminus [simp]: "insertion f (-p :: 'a :: comm_ring_1 mpoly) = -insertion f p"

lemma Sum_any_lookup: "finite {x. g x ≠ 0} ⟹ Sum_any (λx. lookup (g x) y) = lookup (Sum_any g) y"
by (auto simp: Sum_any.expand_set lookup_sum intro!: sum.mono_neutral_left)

lemma Sum_any_diff:
assumes "finite {x. f x ≠ 0}"
assumes "finite {x. g x ≠ 0}"
shows   "Sum_any (λx. f x - g x :: 'a :: ab_group_add) = Sum_any f - Sum_any g"
proof -
have "{x. f x - g x ≠ 0} ⊆ {x. f x ≠ 0} ∪ {x. g x ≠ 0}" by auto
moreover have "finite ({x. f x ≠ 0} ∪ {x. g x ≠ 0})"
by (subst finite_Un) (insert assms, auto)
ultimately have "finite {x. f x - g x ≠ 0}"
by (rule finite_subset)
with assms show ?thesis
by (simp add: algebra_simps Sum_any.distrib [symmetric])
qed

lemma insertion_diff:
"insertion f (p - q :: 'a :: comm_ring_1 mpoly) = insertion f p - insertion f q"
proof (transfer, transfer)
fix f :: "nat ⇒ 'a" and p q :: "(nat ⇒⇩0 nat) ⇒ 'a"
assume fin: "finite {x. p x ≠ 0}" "finite {x. q x ≠ 0}"
have "insertion_fun f (λx. p x - q x) =
(∑m. p m * (∏v. f v ^ lookup m v) - q m * (∏v. f v ^ lookup m v))"
by (simp add: insertion_fun_def algebra_simps Sum_any_diff)
also have "… = (∑m. p m * (∏v. f v ^ lookup m v)) - (∑m. q m * (∏v. f v ^ lookup m v))"
by (subst Sum_any_diff) (auto intro: finite_subset[OF _ fin(1)] finite_subset[OF _ fin(2)])
also have "… = insertion_fun f p - insertion_fun f q"
finally show "insertion_fun f (λx. p x - q x) = …" .
qed

lemma insertion_power: "insertion f (p ^ n) = insertion f p ^ n"
by (induction n) (simp_all add: insertion_mult)

lemma insertion_sum: "insertion f (sum g A) = (∑x∈A. insertion f (g x))"
by (induction A rule: infinite_finite_induct) (auto simp: insertion_add)

lemma insertion_prod: "insertion f (prod g A) = (∏x∈A. insertion f (g x))"
by (induction A rule: infinite_finite_induct) (auto simp: insertion_mult)

lemma coeff_Var: "coeff (Var i) m = (1 when m = Poly_Mapping.single i 1)"
by transfer' (auto simp: Var⇩0_def lookup_single when_def)

lemma vars_Var: "vars (Var i :: 'a :: {one,zero} mpoly) = (if (0::'a) = 1 then {} else {i})"
unfolding vars_def by (auto simp: Var.rep_eq Var⇩0_def)

lemma insertion_Var [simp]: "insertion f (Var i) = f i"
proof -
have "insertion f (Var i) = (∑m. (1 when m = Poly_Mapping.single i 1) *
(∏i. f i ^ lookup m i))"
also have "… = (∏j. f j ^ lookup (Poly_Mapping.single i 1) j)"
by (subst Sum_any.expand_superset[of "{Poly_Mapping.single i 1}"]) (auto simp: when_def)
also have "… = f i"
by (subst Prod_any.expand_superset[of "{i}"]) (auto simp: when_def lookup_single)
finally show ?thesis .
qed

lemma insertion_Sum_any:
assumes "finite {x. g x ≠ 0}"
shows   "insertion f (Sum_any g) = Sum_any (λx. insertion f (g x))"
unfolding Sum_any.expand_set insertion_sum
by (intro sum.mono_neutral_right) (auto intro!: finite_subset[OF _ assms])

lemma keys_diff_subset:
"keys (f - g) ⊆ keys f ∪ keys g"
by transfer auto

lemma keys_empty_iff [simp]: "keys p = {} ⟷ p = 0"
by transfer auto

lemma mpoly_coeff_0 [simp]: "MPoly_Type.coeff 0 m = 0"
by transfer auto

lemma lookup_1: "lookup 1 m = (if m = 0 then 1 else 0)"

lemma mpoly_coeff_1: "MPoly_Type.coeff 1 m = (if m = 0 then 1 else 0)"
by (simp add: MPoly_Type.coeff_def one_mpoly.rep_eq lookup_1)

lemma lookup_Const⇩0: "lookup (Const⇩0 c) m = (if m = 0 then c else 0)"
unfolding Const⇩0_def by (simp add: lookup_single when_def)

lemma mpoly_coeff_Const: "MPoly_Type.coeff (Const c) m = (if m = 0 then c else 0)"
by (simp add: MPoly_Type.coeff_def Const.rep_eq lookup_Const⇩0)

lemma coeff_smult [simp]: "coeff (smult c p) m = (c :: 'a :: mult_zero) * coeff p m"
by transfer (auto simp: map_lookup)

lemma in_keys_mapI: "x ∈ keys m ⟹ f (lookup m x) ≠ 0 ⟹ x ∈ keys (Poly_Mapping.map f m)"
by transfer auto

lemma keys_uminus [simp]: "keys (-m) = keys m"
by transfer auto

lemma vars_uminus [simp]: "vars (-p) = vars p"
unfolding vars_def by transfer' auto

lemma vars_smult: "vars (smult c p) ⊆ vars p"
unfolding vars_def by (transfer', transfer') auto

lemma vars_0 [simp]: "vars 0 = {}"
unfolding vars_def by transfer' simp

lemma vars_1 [simp]: "vars 1 = {}"
unfolding vars_def by transfer' simp

lemma vars_sum: "vars (sum f A) ⊆ (⋃x∈A. vars (f x))"
using vars_add by (induction A rule: infinite_finite_induct) auto

lemma vars_prod: "vars (prod f A) ⊆ (⋃x∈A. vars (f x))"
using vars_mult by (induction A rule: infinite_finite_induct) auto

lemma vars_Sum_any: "vars (Sum_any h) ⊆ (⋃i. vars (h i))"
unfolding Sum_any.expand_set by (intro order.trans[OF vars_sum]) auto

lemma vars_Prod_any: "vars (Prod_any h) ⊆ (⋃i. vars (h i))"
unfolding Prod_any.expand_set by (intro order.trans[OF vars_prod]) auto

lemma vars_power: "vars (p ^ n) ⊆ vars p"
using vars_mult by (induction n) auto

lemma vars_diff: "vars (p1 - p2) ⊆ vars p1 ∪ vars p2"
unfolding vars_def
proof transfer'
fix p1 p2 :: "(nat ⇒⇩0 nat) ⇒⇩0 'a"
show "⋃ (keys ` keys (p1 - p2)) ⊆ ⋃(keys ` (keys p1)) ∪ ⋃(keys ` (keys p2))"
using keys_diff_subset[of p1 p2] by (auto simp flip: not_in_keys_iff_lookup_eq_zero)
qed

lemma insertion_smult [simp]: "insertion f (smult c p) = c * insertion f p"
unfolding insertion_altdef
by (subst Sum_any_right_distrib)
(auto intro: finite_subset[OF _ finite_coeff_support[of p]] simp: mult.assoc)

lemma coeff_add [simp]: "coeff (p + q) m = coeff p m + coeff q m"

lemma coeff_diff [simp]: "coeff (p - q) m = coeff p m - coeff q m"

lemma insertion_monom [simp]:
"insertion f (monom m c) = c * Prod_any (λx. f x ^ lookup m x)"
proof -
have "insertion f (monom m c) =
(∑m'. (c when m = m') * (∏v. f v ^ lookup m' v))"
by (simp add: insertion_def insertion_aux_def insertion_fun_def lookup_single)
also have "… = c * (∏v. f v ^ lookup m v)"
by (subst Sum_any.expand_superset[of "{m}"]) (auto simp: when_def)
finally show ?thesis .
qed

lemma insertion_aux_Const⇩0 [simp]: "insertion_aux f (Const⇩0 c) = c"
proof -
have "insertion_aux f (Const⇩0 c) = (∑m. (c when m = 0) * (∏v. f v ^ lookup m v))"
by (simp add: Const⇩0_def insertion_aux_def insertion_fun_def lookup_single)
also have "… = (∑m∈{0}. (c when m = 0) * (∏v. f v ^ lookup m v))"
by (intro Sum_any.expand_superset) (auto simp: when_def)
also have "… = c" by simp
finally show ?thesis .
qed

lemma insertion_Const [simp]: "insertion f (Const c) = c"

lemma coeffs_0 [simp]: "coeffs 0 = {}"
by transfer auto

lemma coeffs_1 [simp]: "coeffs 1 = {1}"
by transfer auto

lemma coeffs_Const: "coeffs (Const c) = (if c = 0 then {} else {c})"
unfolding Const_def Const⇩0_def by transfer' auto

lemma coeffs_subset: "coeffs (Const c) ⊆ {c}"
by (auto simp: coeffs_Const)

lemma keys_Const⇩0: "keys (Const⇩0 c) = (if c = 0 then {} else {0})"
unfolding Const⇩0_def by transfer' auto

lemma vars_Const [simp]: "vars (Const c) = {}"
unfolding vars_def by transfer' (auto simp: keys_Const⇩0)

lemma prod_fun_compose_bij:
assumes "bij f" and f: "⋀x y. f (x + y) = f x + f y"
shows   "prod_fun m1 m2 (f x) = prod_fun (m1 ∘ f) (m2 ∘ f) x"
proof -
have [simp]: "f x = f y ⟷ x = y" for x y
using ‹bij f› by (auto dest!: bij_is_inj inj_onD)
have "prod_fun (m1 ∘ f) (m2 ∘ f) x =
Sum_any ((λl. m1 l * Sum_any ((λq. m2 q when f x = l + q) ∘ f)) ∘ f)"
by (simp add: prod_fun_def f(1) [symmetric] o_def)
also have "… = Sum_any ((λl. m1 l * Sum_any ((λq. m2 q when f x = l + q))))"
by (simp only: Sum_any.reindex_cong[OF assms(1) refl, symmetric])
also have "… = prod_fun m1 m2 (f x)"
finally show ?thesis ..
qed

"(a + b :: 'a ⇒⇩0 nat) = 0 ⟷ a = 0 ∧ b = 0"
by transfer (auto simp: fun_eq_iff)

lemma prod_fun_nat_0:
fixes f g :: "('a ⇒⇩0 nat) ⇒ 'b::semiring_0"
shows   "prod_fun f g 0 = f 0 * g 0"
proof -
have "prod_fun f g 0 = (∑l. f l * (∑q. g q when 0 = l + q))"
unfolding prod_fun_def ..
also have "(λl. ∑q. g q when 0 = l + q) = (λl. ∑q∈{0}. g q when 0 = l + q)"
by (intro ext Sum_any.expand_superset) (auto simp: when_def)
also have "(∑l. f l * … l) = (∑l∈{0}. f l * … l)"
by (intro ext Sum_any.expand_superset) (auto simp: when_def)
finally show ?thesis by simp
qed

lemma mpoly_coeff_times_0: "coeff (p * q) 0 = coeff p 0 * coeff q 0"

lemma mpoly_coeff_prod_0: "coeff (∏x∈A. f x) 0 = (∏x∈A. coeff (f x) 0)"
by (induction A rule: infinite_finite_induct) (auto simp: mpoly_coeff_times_0 mpoly_coeff_1)

lemma mpoly_coeff_power_0: "coeff (p ^ n) 0 = coeff p 0 ^ n"
by (induction n) (auto simp: mpoly_coeff_times_0 mpoly_coeff_1)

lemma prod_fun_max:
fixes f g :: "'a::{linorder, ordered_cancel_comm_monoid_add} ⇒ 'b::semiring_0"
assumes zero: "⋀m. m > a ⟹ f m = 0" "⋀m. m > b ⟹ g m = 0"
assumes fin: "finite {m. f m ≠ 0}" "finite {m. g m ≠ 0}"
shows   "prod_fun f g (a + b) = f a * g b"
proof -
note fin' = finite_subset[OF _ fin(1)] finite_subset[OF _ fin(2)]
have "prod_fun f g (a + b) = (∑l. f l * (∑q. g q when a + b = l + q))"
also have "… = (∑l. ∑q. f l * g q when a + b = l + q)"
by (subst Sum_any_right_distrib) (auto intro!: Sum_any.cong fin'(2) simp: when_def)
also {
fix l q assume lq: "a + b = l + q" "(a, b) ≠ (l, q)" and nz: "f l * g q ≠ 0"
from nz and zero have "l ≤ a" "q ≤ b" by (auto intro: leI)
moreover from this and lq(2) have "l < a ∨ q < b" by auto
ultimately have "l + q < a + b"
with lq(1) have False by simp
}
hence "(∑l. ∑q. f l * g q when a + b = l + q) = (∑l. ∑q. f l * g q when (a, b) = (l, q))"
by (intro Sum_any.cong refl) (auto simp: when_def)
also have "… = (∑(l,q). f l * g q when (a, b) = (l, q))"
by (intro Sum_any.cartesian_product[of "{(a, b)}"]) auto
also have "… = (∑(l,q)∈{(a,b)}. f l * g q when (a, b) = (l, q))"
by (intro Sum_any.expand_superset) auto
also have "… = f a * g b" by simp
finally show ?thesis .
qed

lemma prod_fun_gt_max_eq_zero:
fixes f g :: "'a::{linorder, ordered_cancel_comm_monoid_add} ⇒ 'b::semiring_0"
assumes "m > a + b"
assumes zero: "⋀m. m > a ⟹ f m = 0" "⋀m. m > b ⟹ g m = 0"
assumes fin: "finite {m. f m ≠ 0}" "finite {m. g m ≠ 0}"
shows   "prod_fun f g m = 0"
proof -
note fin' = finite_subset[OF _ fin(1)] finite_subset[OF _ fin(2)]
have "prod_fun f g m = (∑l. f l * (∑q. g q when m = l + q))"
also have "… = (∑l. ∑q. f l * g q when m = l + q)"
by (subst Sum_any_right_distrib) (auto intro!: Sum_any.cong fin'(2) simp: when_def)
also {
fix l q assume lq: "m = l + q" and nz: "f l * g q ≠ 0"
from nz and zero have "l ≤ a" "q ≤ b" by (auto intro: leI)
hence "l + q ≤ a + b" by (intro add_mono)
also have "… < m" by fact
finally have "l + q < m" .
}
hence "(∑l. ∑q. f l * g q when m = l + q) = (∑l. ∑q. f l * g q when False)"
by (intro Sum_any.cong refl) (auto simp: when_def)
also have "… = 0" by simp
finally show ?thesis .
qed

subsection ‹Restricting a monomial to a subset of variables›

lift_definition restrictpm :: "'a set ⇒ ('a ⇒⇩0 'b :: zero) ⇒ ('a ⇒⇩0 'b)" is
"λA f x. if x ∈ A then f x else 0"
by (erule finite_subset[rotated]) auto

lemma lookup_restrictpm: "lookup (restrictpm A m) x = (if x ∈ A then lookup m x else 0)"
by transfer auto

lemma lookup_restrictpm_in [simp]: "x ∈ A ⟹ lookup (restrictpm A m) x = lookup m x"
and lookup_restrict_pm_not_in [simp]: "x ∉ A ⟹ lookup (restrictpm A m) x = 0"

lemma keys_restrictpm [simp]: "keys (restrictpm A m) = keys m ∩ A"
by transfer auto

lemma restrictpm_add: "restrictpm X (m1 + m2) = restrictpm X m1 + restrictpm X m2"
by transfer auto

lemma restrictpm_id [simp]: "keys m ⊆ X ⟹ restrictpm X m = m"
by transfer (auto simp: fun_eq_iff)

lemma restrictpm_orthogonal [simp]: "keys m ⊆ -X ⟹ restrictpm X m = 0"
by transfer (auto simp: fun_eq_iff)

"X ∩ Y = {} ⟹ restrictpm X m + restrictpm Y m = restrictpm (X ∪ Y) m"
by transfer (auto simp: fun_eq_iff)

"restrictpm X m + restrictpm (-X) m = m" "restrictpm (-X) m + restrictpm X m = m"

subsection ‹Mapping over a polynomial›

lift_definition map_mpoly :: "('a :: zero ⇒ 'b :: zero) ⇒ 'a mpoly ⇒ 'b mpoly" is
"λ(f :: 'a ⇒ 'b) (p :: (nat ⇒⇩0 nat) ⇒⇩0 'a). Poly_Mapping.map f p" .

lift_definition mapm_mpoly :: "((nat ⇒⇩0 nat) ⇒ 'a :: zero ⇒ 'b :: zero) ⇒ 'a mpoly ⇒ 'b mpoly" is
"λ(f :: (nat ⇒⇩0 nat) ⇒ 'a ⇒ 'b) (p :: (nat ⇒⇩0 nat) ⇒⇩0 'a).
Poly_Mapping.mapp f p" .

lemma poly_mapping_map_conv_mapp: "Poly_Mapping.map f = Poly_Mapping.mapp (λ_. f)"
by (auto simp: Poly_Mapping.mapp_def Poly_Mapping.map_def map_fun_def
o_def fun_eq_iff when_def in_keys_iff cong: if_cong)

lemma map_mpoly_conv_mapm_mpoly: "map_mpoly f = mapm_mpoly (λ_. f)"
by transfer' (auto simp: poly_mapping_map_conv_mapp)

lemma map_mpoly_comp: "f 0 = 0 ⟹ map_mpoly f (map_mpoly g p) = map_mpoly (f ∘ g) p"
by (transfer', transfer') (auto simp: when_def fun_eq_iff)

lemma mapp_mapp:
"(⋀x. f x 0 = 0) ⟹ Poly_Mapping.mapp f (Poly_Mapping.mapp g m) =
Poly_Mapping.mapp (λx y. f x (g x y)) m"
by transfer' (auto simp: fun_eq_iff lookup_mapp in_keys_iff)

lemma mapm_mpoly_comp:
"(⋀x. f x 0 = 0) ⟹ mapm_mpoly f (mapm_mpoly g p) = mapm_mpoly (λm c. f m (g m c)) p"

lemma coeff_map_mpoly:
"coeff (map_mpoly f p) m = (if coeff p m = 0 then 0 else f (coeff p m))"
by (transfer, transfer) auto

lemma coeff_map_mpoly' [simp]: "f 0 = 0 ⟹ coeff (map_mpoly f p) m = f (coeff p m)"
by (subst coeff_map_mpoly) auto

lemma coeff_mapm_mpoly: "coeff (mapm_mpoly f p) m = (if coeff p m = 0 then 0 else f m (coeff p m))"
by (transfer, transfer') (auto simp: in_keys_iff)

lemma coeff_mapm_mpoly' [simp]: "(⋀m. f m 0 = 0) ⟹ coeff (mapm_mpoly f p) m = f m (coeff p m)"
by (subst coeff_mapm_mpoly) auto

lemma vars_map_mpoly_subset: "vars (map_mpoly f p) ⊆ vars p"
unfolding vars_def by (transfer', transfer') (auto simp: map_mpoly.rep_eq)

lemma coeff_sum [simp]: "coeff (sum f A) m = (∑x∈A. coeff (f x) m)"
by (induction A rule: infinite_finite_induct) auto

lemma coeff_Sum_any: "finite {x. f x ≠ 0} ⟹ coeff (Sum_any f) m = Sum_any (λx. coeff (f x) m)"
by (auto simp add: Sum_any.expand_set intro!: sum.mono_neutral_right)

lemma Sum_any_zeroI: "(⋀x. f x = 0) ⟹ Sum_any f = 0"
by (auto simp: Sum_any.expand_set)

lemma insertion_Prod_any:
"finite {x. g x ≠ 1} ⟹ insertion f (Prod_any g) = Prod_any (λx. insertion f (g x))"
by (auto simp: Prod_any.expand_set insertion_prod intro!: prod.mono_neutral_right)

lemma insertion_insertion:
"insertion g (insertion k p) =
insertion (λx. insertion g (k x)) (map_mpoly (insertion g) p)" (is "?lhs = ?rhs")
proof -
have "insertion g (insertion k p) =
(∑x. insertion g (coeff p x) * insertion g (∏i. k i ^ lookup x i))"
unfolding insertion_altdef[of k p]
by (subst insertion_Sum_any)
(auto intro: finite_subset[OF _ finite_coeff_support[of p]] simp: insertion_mult)
also have "… = (∑x. insertion g (coeff p x) * (∏i. insertion g (k i) ^ lookup x i))"
proof (intro Sum_any.cong)
fix x show "insertion g (coeff p x) * insertion g (∏i. k i ^ lookup x i) =
insertion g (coeff p x) * (∏i. insertion g (k i) ^ lookup x i)"
by (subst insertion_Prod_any)
(auto simp: insertion_power intro!: finite_subset[OF _ finite_lookup[of x]] Nat.gr0I)
qed
also have "… = insertion (λx. insertion g (k x)) (map_mpoly (insertion g) p)"
unfolding insertion_altdef[of _ "map_mpoly f p" for f] by auto
finally show ?thesis .
qed

lemma insertion_substitute_linear:
"insertion (λi. c i * f i) p =
insertion f (mapm_mpoly (λm d. Prod_any (λi. c i ^ lookup m i) * d) p)"
unfolding insertion_altdef
proof (intro Sum_any.cong, goal_cases)
case (1 m)
have "coeff (mapm_mpoly (λm. (*) (∏i. c i ^ lookup m i)) p) m * (∏i. f i ^ lookup m i) =
MPoly_Type.coeff p m * ((∏i. c i ^ lookup m i) * (∏i. f i ^ lookup m i))"
also have "(∏i. c i ^ lookup m i) * (∏i. f i ^ lookup m i) =
(∏i. (c i * f i) ^ lookup m i)"
by (subst Prod_any.distrib [symmetric])
(auto simp: power_mult_distrib intro!: finite_subset[OF _ finite_lookup[of m]] Nat.gr0I)
finally show ?case by simp
qed

lemma vars_mapm_mpoly_subset: "vars (mapm_mpoly f p) ⊆ vars p"
unfolding vars_def using keys_mapp_subset[of f] by (auto simp: mapm_mpoly.rep_eq)

lemma map_mpoly_cong:
assumes "⋀m. f (coeff p m) = g (coeff p m)" "p = q"
shows   "map_mpoly f p = map_mpoly g q"
using assms by (intro mpoly_eqI) (auto simp: coeff_map_mpoly)

text ‹
The leading monomial of a multivariate polynomial is the one with the largest monomial
w.\,r.\,t.\ the monomial ordering induced by the standard variable ordering. The

As a convention, the leading monomial of the zero polynomial is defined to be the same as
that of any non-constant zero polynomial, i.\,e.\ the monomial \$X_1^0 \ldots X_n^0\$.
›

lift_definition lead_monom :: "'a :: zero mpoly ⇒ (nat ⇒⇩0 nat)" is
"λf :: (nat ⇒⇩0 nat) ⇒⇩0 'a. Max (insert 0 (keys f))" .

assumes "coeff p m ≠ 0"
using assms by (auto simp: lead_monom_def coeff_def in_keys_iff)

shows   "coeff p m = 0"
using lead_monom_geI[of p m] assms by force

assumes "p ≠ 0"
shows   "lead_monom p = Max (keys (mapping_of p))"
using assms by transfer (simp add: max_def)

lemma keys_mult_const [simp]:
fixes c :: "'a :: {semiring_0, semiring_no_zero_divisors}"
assumes "c ≠ 0"
shows "keys (Poly_Mapping.map ((*) c) p) = keys p"
using assms by transfer auto

unfolding vars_def by transfer' (auto simp: Max_eq_iff)

lemma lead_monom_monom: "lead_monom (monom m c) = (if c = 0 then 0 else m)"

lemma lead_monom_monom' [simp]: "c ≠ 0 ⟹ lead_monom (monom m c) = m"

unfolding monom_numeral[symmetric] by (subst lead_monom_monom) auto

proof transfer
fix p q :: "(nat ⇒⇩0 nat) ⇒⇩0 'a"
show "Max (insert 0 (keys (p + q))) ≤ max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))"
proof (rule Max.boundedI)
fix m assume m: "m ∈ insert 0 (keys (p + q))"
thus "m ≤ max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))"
proof
assume "m ∈ keys (p + q)"
with keys_add[of p q] have "m ∈ keys p ∨ m ∈ keys q"
by (auto simp: in_keys_iff plus_poly_mapping.rep_eq)
thus ?thesis by (auto simp: le_max_iff_disj)
qed auto
qed auto
qed

proof transfer
fix p q :: "(nat ⇒⇩0 nat) ⇒⇩0 'a"
show "Max (insert 0 (keys (p - q))) ≤ max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))"
proof (rule Max.boundedI)
fix m assume m: "m ∈ insert 0 (keys (p - q))"
thus "m ≤ max (Max (insert 0 (keys p))) (Max (insert 0 (keys q)))"
proof
assume "m ∈ keys (p - q)"
with keys_diff_subset[of p q] have "m ∈ keys p ∨ m ∈ keys q" by auto
thus ?thesis by (auto simp: le_max_iff_disj)
qed auto
qed auto
qed

lemma vars_empty_iff: "vars p = {} ⟷ p = Const (lead_coeff p)"
proof
assume "vars p = {}"
hence [simp]: "lead_monom p = 0"
have [simp]: "mon ≠ 0 ⟷ (mon > (0 :: nat ⇒⇩0 nat))" for mon
by (auto simp: order.strict_iff_order)
thus "p = Const (lead_coeff p)"
by (intro mpoly_eqI) (auto simp: mpoly_coeff_Const lead_coeff_def)
next
assume "p = Const (lead_coeff p)"
also have "vars … = {}" by simp
finally show "vars p = {}" .
qed

by (cases "keys (mapping_of p) = {}") (auto simp: coeff_def max_def)

lemma
fixes c :: "'a :: semiring_0"
assumes "c * lead_coeff p ≠ 0"
proof -
from assms have *: "keys (mapping_of p) ≠ {}"
by auto
from assms have "coeff (MPoly_Type.smult c p) (lead_monom p) ≠ 0"
hence smult_nz: "MPoly_Type.smult c p ≠ 0" by (auto simp del: coeff_smult)
with assms have **: "keys (mapping_of (smult c p)) ≠ {}"
by simp

have "Max (keys (mapping_of (smult c p))) = Max (keys (mapping_of p))"
proof (safe intro!: antisym Max.coboundedI)
have "lookup (mapping_of p) (Max (keys (mapping_of p))) = lead_coeff p"
with assms show "Max (keys (mapping_of p)) ∈ keys (mapping_of (smult c p))"
using * by (auto simp: smult.rep_eq intro!: in_keys_mapI)
from smult_nz have "lead_coeff (smult c p) ≠ 0"
hence "coeff p (Max (keys (mapping_of (smult c p)))) ≠ 0"
thus "Max (keys (mapping_of (smult c p))) ∈ keys (mapping_of p)"
by (auto simp: smult.rep_eq coeff_def in_keys_iff)
qed auto
qed

proof (cases "p = 0 ∨ q = 0")
case False
define a b where "a = lead_monom p" and "b = lead_monom q"
have "coeff (p * q) (a + b) = coeff p a * coeff q b"
unfolding coeff_mpoly_times
by (rule prod_fun_max) (insert False, auto simp: a_def b_def)
qed auto

proof (cases "p * q = 0")
case False
show ?thesis
proof (intro leI notI)
hence "lead_coeff (p * q) = 0"
unfolding lead_coeff_def coeff_mpoly_times by (rule prod_fun_gt_max_eq_zero) auto
with False show False by simp
qed
qed auto

proof (cases "p = 0")
case False
hence "lead_coeff p ≠ 0" by simp
thus ?thesis unfolding vars_def by transfer' (auto simp: max_def in_keys_iff)
qed auto

lemma
assumes "(∏i∈A. lead_coeff (f i)) ≠ 0"
proof -
have "?th1 ∧ ?th2" using assms
proof (induction A rule: infinite_finite_induct)
case (insert x A)
from insert have nz: "lead_coeff (f x) ≠ 0" "(∏i∈A. lead_coeff (f i)) ≠ 0" by auto
note IH = insert.IH[OF this(2)]
from insert have nz': "lead_coeff (f x) * lead_coeff (∏i∈A. f i) ≠ 0"
by (subst IH) auto
from insert.prems insert.hyps nz nz' show ?case
qed auto
thus ?th1 ?th2 by blast+
qed

lemma lead_monom_sum_le: "(⋀x. x ∈ X ⟹ lead_monom (h x) ≤ ub) ⟹ lead_monom (sum h X) ≤ ub"

text ‹
The leading monomial of a sum where the leading monomial the summands are distinct is
simply the maximum of the leading monomials.
›
assumes "inj_on (lead_monom ∘ h) X" and "finite X" and "X ≠ {}" and "⋀x. x ∈ X ⟹ h x ≠ 0"
defines "m ≡ Max ((lead_monom ∘ h) ` X)"
shows   "lead_monom (∑x∈X. h x) = m"
proof (rule antisym)
show "lead_monom (sum h X) ≤ m" unfolding m_def using assms
by (intro lead_monom_sum_le Max_ge finite_imageI) auto
next
from assms have "m ∈ (lead_monom ∘ h) ` X"
unfolding m_def by (intro Max_in finite_imageI) auto
then obtain x where x: "x ∈ X" "m = lead_monom (h x)" by auto
have "coeff (∑x∈X. h x) m = (∑x∈X. coeff (h x) m)"
by simp
also have "… = (∑x∈{x}. coeff (h x) m)"
proof (intro sum.mono_neutral_right ballI)
fix y assume y: "y ∈ X - {x}"
hence "(lead_monom ∘ h) y ≤ m"
using assms unfolding m_def by (intro Max_ge finite_imageI) auto
using ‹x ∈ X› y inj_onD[OF assms(1), of x y] by auto
ultimately have "lead_monom (h y) < m"
using x by auto
thus "coeff (h y) m = 0" by simp
qed (insert x assms, auto)
also have "… = coeff (h x) m" by simp
also have "… ≠ 0" using assms x by auto
qed

by (cases "p = 0") auto

lemma
fixes f :: "_ ⇒ 'a :: semidom mpoly"
assumes "⋀i. i ∈ A ⟹ f i ≠ 0"
proof -
from assms have "(∏i∈A. lead_coeff (f i)) ≠ 0"
by (cases "finite A") auto
qed

lemma
fixes p :: "'a :: comm_semiring_1 mpoly"
assumes "lead_coeff p ^ n ≠ 0"
by simp_all

lemma
fixes p :: "'a :: semidom mpoly"
assumes "p ≠ 0"
by simp_all

subsection ‹Turning a set of variables into a monomial›

text ‹
Given a finite set \$\{X_1,\ldots,X_n\}\$ of variables, the following is the monomial
\$X_1\ldots X_n\$:
›
lift_definition monom_of_set :: "nat set ⇒ (nat ⇒⇩0 nat)" is
"λX x. if finite X ∧ x ∈ X then 1 else 0"
by auto

lemma lookup_monom_of_set:
"Poly_Mapping.lookup (monom_of_set X) i = (if finite X ∧ i ∈ X then 1 else 0)"
by transfer auto

lemma lookup_monom_of_set_1 [simp]:
"finite X ⟹ i ∈ X ⟹ Poly_Mapping.lookup (monom_of_set X) i = 1"
and lookup_monom_of_set_0 [simp]:
"i ∉ X ⟹ Poly_Mapping.lookup (monom_of_set X) i = 0"

lemma keys_monom_of_set: "keys (monom_of_set X) = (if finite X then X else {})"
by transfer auto

lemma keys_monom_of_set_finite [simp]: "finite X ⟹ keys (monom_of_set X) = X"

lemma monom_of_set_eq_iff [simp]: "finite X ⟹ finite Y ⟹ monom_of_set X = monom_of_set Y ⟷ X = Y"
by transfer (auto simp: fun_eq_iff)

lemma monom_of_set_empty [simp]: "monom_of_set {} = 0"
by transfer auto

lemma monom_of_set_eq_zero_iff [simp]: "monom_of_set X = 0 ⟷ infinite X ∨ X = {}"
by transfer (auto simp: fun_eq_iff)

lemma zero_eq_monom_of_set_iff [simp]: "0 = monom_of_set X ⟷ infinite X ∨ X = {}"
by transfer (auto simp: fun_eq_iff)

subsection ‹Permuting the variables of a polynomial›

text ‹
Next, we define the operation of permuting the variables of a monomial and polynomial.
›

lift_definition permutep :: "('a ⇒ 'a) ⇒ ('a ⇒⇩0 'b) ⇒ ('a ⇒⇩0 'b :: zero)" is
"λf p. if bij f then p ∘ f else p"
proof -
fix f :: "'a ⇒ 'a" and g :: "'a ⇒ 'b"
assume *: "finite {x. g x ≠ 0}"
show "finite {x. (if bij f then g ∘ f else g) x ≠ 0}"
proof (cases "bij f")
case True
with * have "finite (f -` {x. g x ≠ 0})"
by (intro finite_vimageI) (auto dest: bij_is_inj)
with True show ?thesis by auto
qed (use * in auto)
qed

lift_definition mpoly_map_vars :: "(nat ⇒ nat) ⇒ 'a :: zero mpoly ⇒ 'a mpoly" is
"λf p. permutep (permutep f) p" .

lemma keys_permutep: "bij f ⟹ keys (permutep f m) = f -` keys m"
by transfer auto

lemma permutep_id'' [simp]: "permutep id = id"
by transfer' (auto simp: fun_eq_iff)

lemma permutep_id''' [simp]: "permutep (λx. x) = id"
by transfer' (auto simp: fun_eq_iff)

lemma permutep_0 [simp]: "permutep f 0 = 0"
by transfer auto

lemma permutep_single:
"bij f ⟹ permutep f (Poly_Mapping.single a b) = Poly_Mapping.single (inv_into UNIV f a) b"
by transfer (auto simp: fun_eq_iff when_def inv_f_f surj_f_inv_f bij_is_inj bij_is_surj)

lemma mpoly_map_vars_id [simp]: "mpoly_map_vars id = id"
by transfer auto

lemma mpoly_map_vars_id' [simp]: "mpoly_map_vars (λx. x) = id"
by transfer auto

lemma lookup_permutep:
"Poly_Mapping.lookup (permutep f m) x = (if bij f then Poly_Mapping.lookup m (f x) else Poly_Mapping.lookup m x)"
by transfer auto

lemma inj_permutep [intro]: "inj (permutep (f :: 'a ⇒ 'a) :: _ ⇒ 'a ⇒⇩0 'b :: zero)"
unfolding inj_def
proof (transfer, safe)
fix f :: "'a ⇒ 'a" and x y :: "'a ⇒ 'b"
assume eq: "(if bij f then x ∘ f else x) = (if bij f then y ∘ f else y)"
show "x = y"
proof (cases "bij f")
case True
show ?thesis
proof
fix t :: 'a
from ‹bij f› obtain s where "t = f s"
by (auto dest!: bij_is_surj)
with eq and True show "x t = y t"
by (auto simp: fun_eq_iff)
qed
qed (use eq in auto)
qed

lemma surj_permutep [intro]: "surj (permutep (f :: 'a ⇒ 'a) :: _ ⇒ 'a ⇒⇩0 'b :: zero)"
unfolding surj_def
proof (transfer, safe)
fix f :: "'a ⇒ 'a" and y :: "'a ⇒ 'b"
assume fin: "finite {t. y t ≠ 0}"
show "∃x∈{f. finite {x. f x ≠ 0}}. y = (if bij f then x ∘ f else x)"
proof (cases "bij f")
case True
with fin have "finite (the_inv f -` {t. y t ≠ 0})"
by (intro finite_vimageI) (auto simp: bij_is_inj bij_betw_the_inv_into)
moreover have "y ∘ the_inv f ∘ f = y"
using True by (simp add: fun_eq_iff the_inv_f_f bij_is_inj)
ultimately show ?thesis by (intro bexI[of _ "y ∘ the_inv f"]) (auto simp: True)
qed (use fin in auto)
qed

lemma bij_permutep [intro]: "bij (permutep f)"
using inj_permutep[of f] surj_permutep[of f] by (simp add: bij_def)

lemma mpoly_map_vars_map_mpoly:
"mpoly_map_vars f (map_mpoly g p) = map_mpoly g (mpoly_map_vars f p)"
by (transfer', transfer') (auto simp: fun_eq_iff)

lemma coeff_mpoly_map_vars:
fixes f :: "nat ⇒ nat" and p :: "'a :: zero mpoly"
assumes "bij f"
shows   "MPoly_Type.coeff (mpoly_map_vars f p) mon =
MPoly_Type.coeff p (permutep f mon)"
using assms by transfer' (simp add: lookup_permutep bij_permutep)

lemma permutep_monom_of_set:
assumes "bij f"
shows   "permutep f (monom_of_set A) = monom_of_set (f -` A)"
using assms by transfer (auto simp: fun_eq_iff bij_is_inj finite_vimage_iff)

lemma permutep_comp: "bij f ⟹ bij g ⟹ permutep (f ∘ g) = permutep g ∘ permutep f"
by transfer' (auto simp: fun_eq_iff bij_comp)

lemma permutep_comp': "bij f ⟹ bij g ⟹ permutep (f ∘ g) mon = permutep g (permutep f mon)"
by transfer (auto simp: fun_eq_iff bij_comp)

lemma mpoly_map_vars_comp:
"bij f ⟹ bij g ⟹ mpoly_map_vars f (mpoly_map_vars g p) = mpoly_map_vars (f ∘ g) p"
by transfer (auto simp: bij_permutep permutep_comp)

lemma permutep_id [simp]: "permutep id mon = mon"
by transfer auto

lemma permutep_id' [simp]: "permutep (λx. x) mon = mon"
by transfer auto

lemma inv_permutep [simp]:
fixes f :: "'a ⇒ 'a"
assumes "bij f"
shows   "inv_into UNIV (permutep f) = permutep (inv_into UNIV f)"
proof
fix m :: "'a ⇒⇩0 'b"
show "inv_into UNIV (permutep f) m = permutep (inv_into UNIV f) m"
using permutep_comp'[of "inv_into UNIV f" f m] assms inj_iff[of f]
by (intro inv_f_eq) (auto simp: bij_imp_bij_inv bij_is_inj)
qed

lemma mpoly_map_vars_monom:
"bij f ⟹ mpoly_map_vars f (monom m c) = monom (permutep (inv_into UNIV f) m) c"
by transfer' (simp add: permutep_single bij_permutep)

lemma vars_mpoly_map_vars:
fixes f :: "nat ⇒ nat" and p :: "'a :: zero mpoly"
assumes "bij f"
shows   "vars (mpoly_map_vars f p) = f ` vars p"
using assms unfolding vars_def
proof transfer'
fix f :: "nat ⇒ nat" and p :: "(nat ⇒⇩0 nat) ⇒⇩0 'a"
assume f: "bij f"
have eq: "f (inv_into UNIV f x) = x" for x
using f by (subst surj_f_inv_f[of f]) (auto simp: bij_is_surj)
show "⋃ (keys ` keys (permutep (permutep f) p)) = f ` ⋃ (keys ` keys p)"
proof safe
fix m x assume mx: "m ∈ keys (permutep (permutep f) p)" "x ∈ keys m"
from mx have "permutep f m ∈ keys p"
by (auto simp: keys_permutep bij_permutep f)
with mx have "f (inv_into UNIV f x) ∈ f ` (⋃m∈keys p. keys m)"
by (intro imageI) (auto intro!: bexI[of _ "permutep f m"] simp: keys_permutep f eq)
with eq show "x ∈ f ` (⋃m∈keys p. keys m)" by simp
next
fix m x assume mx: "m ∈ keys p" "x ∈ keys m"
from mx have "permutep id m ∈ keys p" by simp
also have "id = inv_into UNIV f ∘ f" using f by (intro ext) (auto simp: bij_is_inj inv_f_f)
also have "permutep … m = permutep f (permutep (inv_into UNIV f) m)"
by (simp add: permutep_comp f bij_imp_bij_inv)
finally have **: "permutep f (permutep (inv_into UNIV f) m) ∈ keys p" .
moreover from f mx have "f x ∈ keys (permutep (inv_into UNIV f) m)"
by (auto simp: keys_permutep bij_imp_bij_inv inv_f_f bij_is_inj)
ultimately show "f x ∈ ⋃ (keys ` keys (permutep (permutep f) p))" using f
by (auto simp: keys_permutep bij_permutep)
qed
qed

lemma permutep_eq_monom_of_set_iff [simp]:
assumes "bij f"
shows   "permutep f mon = monom_of_set A ⟷ mon = monom_of_set (f ` A)"
proof
assume eq: "permutep f mon = monom_of_set A"
have "permutep (inv_into UNIV f) (permutep f mon) = monom_of_set (inv_into UNIV f -` A)"
using assms by (simp add: eq bij_imp_bij_inv assms permutep_monom_of_set)
also have "inv_into UNIV f -` A = f ` A"
using assms by (force simp: bij_is_surj image_iff inv_f_f bij_is_inj surj_f_inv_f)
also have "permutep (inv_into UNIV f) (permutep f mon) = permutep (f ∘ inv_into UNIV f) mon"
using assms by (simp add: permutep_comp bij_imp_bij_inv)
also have "f ∘ inv_into UNIV f = id"
by (subst surj_iff [symmetric]) (insert assms, auto simp: bij_is_surj)
finally show "mon = monom_of_set (f ` A)" by simp
qed (insert assms, auto simp: permutep_monom_of_set inj_vimage_image_eq bij_is_inj)

lemma permutep_monom_of_set_permutes [simp]:
assumes "π permutes A"
shows   "permutep π (monom_of_set A) = monom_of_set A"
using assms
by transfer (auto simp: if_splits fun_eq_iff permutes_in_image)

lemma mpoly_map_vars_0 [simp]: "mpoly_map_vars f 0 = 0"
by (transfer, transfer') (simp add: o_def)

lemma permutep_eq_0_iff [simp]: "permutep f m = 0 ⟷ m = 0"
proof transfer
fix f :: "'a ⇒ 'a" and m :: "'a ⇒ 'b" assume "finite {x. m x ≠ 0}"
show "((if bij f then m ∘ f else m) = (λk. 0)) = (m = (λk. 0))"
proof (cases "bij f")
case True
hence "(∀x. m (f x) = 0) ⟷ (∀x. m x = 0)"
using bij_iff[of f] by metis
with True show ?thesis by (auto simp: fun_eq_iff)
qed (auto simp: fun_eq_iff)
qed

lemma mpoly_map_vars_1 [simp]: "mpoly_map_vars f 1 = 1"
by (transfer, transfer') (auto simp: o_def fun_eq_iff when_def)

lemma permutep_Const⇩0 [simp]: "(⋀x. f x = 0 ⟷ x = 0) ⟹ permutep f (Const⇩0 c) = Const⇩0 c"
unfolding Const⇩0_def by transfer' (auto simp: when_def fun_eq_iff)

lemma permutep_add [simp]: "permutep f (m1 + m2) = permutep f m1 + permutep f m2"
unfolding Const⇩0_def by transfer' (auto simp: when_def fun_eq_iff)

lemma permutep_diff [simp]: "permutep f (m1 - m2) = permutep f m1 - permutep f m2"
unfolding Const⇩0_def by transfer' (auto simp: when_def fun_eq_iff)

lemma permutep_uminus [simp]: "permutep f (-m) = -permutep f m"
unfolding Const⇩0_def by transfer' (auto simp: when_def fun_eq_iff)

lemma permutep_mult [simp]:
"(⋀x y. f (x + y) = f x + f y) ⟹ permutep f (m1 * m2) = permutep f m1 * permutep f m2"
unfolding Const⇩0_def by transfer' (auto simp: when_def fun_eq_iff prod_fun_compose_bij)

lemma mpoly_map_vars_Const [simp]: "mpoly_map_vars f (Const c) = Const c"
by transfer (auto simp: o_def fun_eq_iff when_def)

lemma mpoly_map_vars_add [simp]: "mpoly_map_vars f (p + q) = mpoly_map_vars f p + mpoly_map_vars f q"
by transfer simp

lemma mpoly_map_vars_diff [simp]: "mpoly_map_vars f (p - q) = mpoly_map_vars f p - mpoly_map_vars f q"
by transfer simp

lemma mpoly_map_vars_uminus [simp]: "mpoly_map_vars f (-p) = -mpoly_map_vars f p"
by transfer simp

lemma permutep_smult:
"permutep (permutep f) (Poly_Mapping.map ((*) c) p) =
Poly_Mapping.map ((*) c) (permutep (permutep f) p)"
by transfer' (auto split: if_splits simp: fun_eq_iff)

lemma mpoly_map_vars_smult [simp]: "mpoly_map_vars f (smult c p) = smult c (mpoly_map_vars f p)"

lemma mpoly_map_vars_mult [simp]: "mpoly_map_vars f (p * q) = mpoly_map_vars f p * mpoly_map_vars f q"
by transfer simp

lemma mpoly_map_vars_sum [simp]: "mpoly_map_vars f (sum g A) = (∑x∈A. mpoly_map_vars f (g x))"
by (induction A rule: infinite_finite_induct) auto

lemma mpoly_map_vars_prod [simp]: "mpoly_map_vars f (prod g A) = (∏x∈A. mpoly_map_vars f (g x))"
by (induction A rule: infinite_finite_induct) auto

lemma mpoly_map_vars_eq_0_iff [simp]: "mpoly_map_vars f p = 0 ⟷ p = 0"
by transfer auto

lemma permutep_eq_iff [simp]: "permutep f p = permutep f q ⟷ p = q"
by transfer (auto simp: comp_bij_eq_iff)

lemma mpoly_map_vars_Sum_any [simp]:
"mpoly_map_vars f (Sum_any g) = Sum_any (λx. mpoly_map_vars f (g x))"

lemma mpoly_map_vars_power [simp]: "mpoly_map_vars f (p ^ n) = mpoly_map_vars f p ^ n"
by (induction n) auto

lemma mpoly_map_vars_monom_single [simp]:
assumes "bij f"
shows   "mpoly_map_vars f (monom (Poly_Mapping.single i n) c) =
monom (Poly_Mapping.single (f i) n) c"
using assms by (simp add: mpoly_map_vars_monom permutep_single bij_imp_bij_inv inv_inv_eq)

lemma insertion_mpoly_map_vars:
assumes "bij f"
shows   "insertion g (mpoly_map_vars f p) = insertion (g ∘ f) p"
proof -
have "insertion g (mpoly_map_vars f p) =
(∑m. coeff p (permutep f m) * (∏i. g i ^ lookup m i))"
using assms by (simp add: insertion_altdef coeff_mpoly_map_vars)
also have "… = Sum_any (λm. coeff p (permutep f m) *
Prod_any (λi. g (f i) ^ lookup m (f i)))"
by (intro Sum_any.cong arg_cong[where ?f = "λy. x * y" for x]
Prod_any.reindex_cong[OF assms]) (auto simp: o_def)
also have "… = Sum_any (λm. coeff p m * (∏i. g (f i) ^ lookup m i))"
by (intro Sum_any.reindex_cong [OF bij_permutep[of f], symmetric])
(auto simp: o_def lookup_permutep assms)
also have "… = insertion (g ∘ f) p"