# Theory Polynomials.Power_Products

(* Author: Fabian Immler, Alexander Maletzky *)

section ‹Abstract Power-Products›

theory Power_Products
imports Complex_Main
"HOL-Library.Function_Algebras"
"HOL-Library.Countable"
"More_MPoly_Type"
"Utils"
Well_Quasi_Orders.Well_Quasi_Orders
begin

text ‹This theory formalizes the concept of "power-products". A power-product can be thought of as
the product of some indeterminates, such as $x$, $x^2\,y$, $x\,y^3\,z^7$, etc., without any
scalar coefficient.

The approach in this theory is to capture the notion of "power-product" (also called "monomial") as
type class. A canonical instance for power-product is the type @{typ "'var ⇒⇩0 nat"}, which is
interpreted as mapping from variables in the power-product to exponents.

A slightly unintuitive (but fitting better with the standard type class instantiations of
@{typ "'a ⇒⇩0 'b"}) approach is to write addition to denote "multiplication" of power products.
For example, $x^2y$ would be represented as a function ‹p = (X ↦ 2, Y ↦ 1)›, $xz$ as a
function ‹q = (X ↦ 1, Z ↦ 1)›. With the (pointwise) instantiation of addition of @{typ "'a ⇒⇩0 'b"},
we will write ‹p + q = (X ↦ 3, Y ↦ 1, Z ↦ 1)› for the product $x^2y \cdot xz = x^3yz$
›

subsection ‹Constant @{term Keys}›

text ‹Legacy:›
lemmas keys_eq_empty_iff = keys_eq_empty

definition Keys :: "('a ⇒⇩0 'b::zero) set ⇒ 'a set"
where "Keys F = ⋃(keys  F)"

lemma in_Keys: "s ∈ Keys F ⟷ (∃f∈F. s ∈ keys f)"
unfolding Keys_def by simp

lemma in_KeysI:
assumes "s ∈ keys f" and "f ∈ F"
shows "s ∈ Keys F"
unfolding in_Keys using assms ..

lemma in_KeysE:
assumes "s ∈ Keys F"
obtains f where "s ∈ keys f" and "f ∈ F"
using assms unfolding in_Keys ..

lemma Keys_mono:
assumes "A ⊆ B"
shows "Keys A ⊆ Keys B"
using assms by (auto simp add: Keys_def)

lemma Keys_insert: "Keys (insert a A) = keys a ∪ Keys A"

lemma Keys_Un: "Keys (A ∪ B) = Keys A ∪ Keys B"

lemma finite_Keys:
assumes "finite A"
shows "finite (Keys A)"
unfolding Keys_def by (rule, fact assms, rule finite_keys)

lemma Keys_not_empty:
assumes "a ∈ A" and "a ≠ 0"
shows "Keys A ≠ {}"
proof
assume "Keys A = {}"
from ‹a ≠ 0› have "keys a ≠ {}" using aux by fastforce
then obtain s where "s ∈ keys a" by blast
from this assms(1) have "s ∈ Keys A" by (rule in_KeysI)
with ‹Keys A = {}› show False by simp
qed

lemma Keys_empty [simp]: "Keys {} = {}"

lemma Keys_zero [simp]: "Keys {0} = {}"

lemma keys_subset_Keys:
assumes "f ∈ F"
shows "keys f ⊆ Keys F"
using in_KeysI[OF _ assms] by auto

lemma Keys_minus: "Keys (A - B) ⊆ Keys A"

lemma Keys_minus_zero: "Keys (A - {0}) = Keys A"
proof (cases "0 ∈ A")
case True
hence "(A - {0}) ∪ {0} = A" by auto
hence "Keys A = Keys ((A - {0}) ∪ {0})" by simp
also have "... = Keys (A - {0}) ∪ Keys {0::('a ⇒⇩0 'b)}" by (fact Keys_Un)
also have "... = Keys (A - {0})" by simp
finally show ?thesis by simp
next
case False
hence "A - {0} = A" by simp
thus ?thesis by simp
qed

subsection ‹Constant @{term except}›

definition except_fun :: "('a ⇒ 'b) ⇒ 'a set ⇒ ('a ⇒ 'b::zero)"
where "except_fun f S = (λx. (f x when x ∉ S))"

lift_definition except :: "('a ⇒⇩0 'b) ⇒ 'a set ⇒ ('a ⇒⇩0 'b::zero)" is except_fun
proof -
fix p::"'a ⇒ 'b" and S::"'a set"
assume "finite {t. p t ≠ 0}"
show "finite {t. except_fun p S t ≠ 0}"
proof (rule finite_subset[of _ "{t. p t ≠ 0}"], rule)
fix u
assume "u ∈ {t. except_fun p S t ≠ 0}"
hence "p u ≠ 0" by (simp add: except_fun_def)
thus "u ∈ {t. p t ≠ 0}" by simp
qed fact
qed

lemma lookup_except_when: "lookup (except p S) = (λt. lookup p t when t ∉ S)"
by (auto simp: except.rep_eq except_fun_def)

lemma lookup_except: "lookup (except p S) = (λt. if t ∈ S then 0 else lookup p t)"
by (rule ext) (simp add: lookup_except_when)

lemma lookup_except_singleton: "lookup (except p {t}) t = 0"

lemma except_zero [simp]: "except 0 S = 0"
by (rule poly_mapping_eqI) (simp add: lookup_except)

lemma lookup_except_eq_idI:
assumes "t ∉ S"
shows "lookup (except p S) t = lookup p t"
using assms by (simp add: lookup_except)

lemma lookup_except_eq_zeroI:
assumes "t ∈ S"
shows "lookup (except p S) t = 0"
using assms by (simp add: lookup_except)

lemma except_empty [simp]: "except p {} = p"
by (rule poly_mapping_eqI) (simp add: lookup_except)

lemma except_eq_zeroI:
assumes "keys p ⊆ S"
shows "except p S = 0"
proof (rule poly_mapping_eqI, simp)
fix t
show "lookup (except p S) t = 0"
proof (cases "t ∈ S")
case True
thus ?thesis by (rule lookup_except_eq_zeroI)
next
case False then show ?thesis
by (metis assms in_keys_iff lookup_except_eq_idI subset_eq)
qed
qed

lemma except_eq_zeroE:
assumes "except p S = 0"
shows "keys p ⊆ S"
by (metis assms aux in_keys_iff lookup_except_eq_idI subset_iff)

lemma except_eq_zero_iff: "except p S = 0 ⟷ keys p ⊆ S"
by (rule, elim except_eq_zeroE, elim except_eq_zeroI)

lemma except_keys [simp]: "except p (keys p) = 0"
by (rule except_eq_zeroI, rule subset_refl)

lemma plus_except: "p = Poly_Mapping.single t (lookup p t) + except p {t}"

lemma keys_except: "keys (except p S) = keys p - S"
by (transfer, auto simp: except_fun_def)

lemma except_single: "except (Poly_Mapping.single u c) S = (Poly_Mapping.single u c when u ∉ S)"
by (rule poly_mapping_eqI) (simp add: lookup_except lookup_single when_def)

lemma except_plus: "except (p + q) S = except p S + except q S"

lemma except_minus: "except (p - q) S = except p S - except q S"
by (rule poly_mapping_eqI) (simp add: lookup_except lookup_minus)

lemma except_uminus: "except (- p) S = - except p S"
by (rule poly_mapping_eqI) (simp add: lookup_except)

lemma except_except: "except (except p S) T = except p (S ∪ T)"
by (rule poly_mapping_eqI) (simp add: lookup_except)

lemma poly_mapping_keys_eqI:
assumes a1: "keys p = keys q" and a2: "⋀t. t ∈ keys p ⟹ lookup p t = lookup q t"
shows "p = q"
proof (rule poly_mapping_eqI)
fix t
show "lookup p t = lookup q t"
proof (cases "t ∈ keys p")
case True
thus ?thesis by (rule a2)
next
case False
moreover from this have "t ∉ keys q" unfolding a1 .
ultimately have "lookup p t = 0" and "lookup q t = 0" unfolding in_keys_iff by simp_all
thus ?thesis by simp
qed
qed

lemma except_id_iff: "except p S = p ⟷ keys p ∩ S = {}"
by (metis Diff_Diff_Int Diff_eq_empty_iff Diff_triv inf_le2 keys_except lookup_except_eq_idI
lookup_except_eq_zeroI not_in_keys_iff_lookup_eq_zero poly_mapping_keys_eqI)

lemma keys_subset_wf:
"wfP (λp q::('a, 'b::zero) poly_mapping. keys p ⊂ keys q)"
unfolding wfP_def
proof (intro wfI_min)
fix x::"('a, 'b) poly_mapping" and Q
assume x_in: "x ∈ Q"
let ?Q0 = "card  keys  Q"
from x_in have "card (keys x) ∈ ?Q0" by simp
from wfE_min[OF wf this] obtain z0
where z0_in: "z0 ∈ ?Q0" and z0_min: "⋀y. (y, z0) ∈ {(x, y). x < y} ⟹ y ∉ ?Q0" by auto
from z0_in obtain z where z0_def: "z0 = card (keys z)" and "z ∈ Q" by auto
show "∃z∈Q. ∀y. (y, z) ∈ {(p, q). keys p ⊂ keys q} ⟶ y ∉ Q"
proof (intro bexI[of _ z], rule, rule)
fix y::"('a, 'b) poly_mapping"
let ?y0 = "card (keys y)"
assume "(y, z) ∈ {(p, q). keys p ⊂ keys q}"
hence "keys y ⊂ keys z" by simp
hence "?y0 < z0" unfolding z0_def by (simp add: psubset_card_mono)
hence "(?y0, z0) ∈ {(x, y). x < y}" by simp
from z0_min[OF this] show "y ∉ Q" by auto
qed (fact)
qed

lemma poly_mapping_except_induct:
assumes base: "P 0" and ind: "⋀p t. p ≠ 0 ⟹ t ∈ keys p ⟹ P (except p {t}) ⟹ P p"
shows "P p"
proof (induct rule: wfP_induct[OF keys_subset_wf])
fix p::"('a, 'b) poly_mapping"
assume "∀q. keys q ⊂ keys p ⟶ P q"
hence IH: "⋀q. keys q ⊂ keys p ⟹ P q" by simp
show "P p"
proof (cases "p = 0")
case True
thus ?thesis using base by simp
next
case False
hence "keys p ≠ {}" by simp
then obtain t where "t ∈ keys p" by blast
show ?thesis
proof (rule ind, fact, fact, rule IH, simp only: keys_except, rule, rule Diff_subset, rule)
assume "keys p - {t} = keys p"
hence "t ∉ keys p" by blast
from this ‹t ∈ keys p› show False ..
qed
qed
qed

lemma poly_mapping_except_induct':
assumes "⋀p. (⋀t. t ∈ keys p ⟹ P (except p {t})) ⟹ P p"
shows "P p"
proof (induct "card (keys p)" arbitrary: p)
case 0
with finite_keys[of p] have "keys p = {}" by simp
show ?case by (rule assms, simp add: ‹keys p = {}›)
next
case step: (Suc n)
show ?case
proof (rule assms)
fix t
assume "t ∈ keys p"
show "P (except p {t})"
proof (rule step(1), simp add: keys_except)
from step(2) ‹t ∈ keys p› finite_keys[of p] show "n = card (keys p - {t})" by simp
qed
qed
qed

lemma poly_mapping_plus_induct:
assumes "P 0" and "⋀p c t. c ≠ 0 ⟹ t ∉ keys p ⟹ P p ⟹ P (Poly_Mapping.single t c + p)"
shows "P p"
proof (induct "card (keys p)" arbitrary: p)
case 0
with finite_keys[of p] have "keys p = {}" by simp
hence "p = 0" by simp
with assms(1) show ?case by simp
next
case step: (Suc n)
from step(2) obtain t where t: "t ∈ keys p" by (metis card_eq_SucD insert_iff)
define c where "c = lookup p t"
define q where "q = except p {t}"
have *: "p = Poly_Mapping.single t c + q"
show ?case
proof (simp only: *, rule assms(2))
from t show "c ≠ 0"
using c_def by auto
next
show "t ∉ keys q" by (simp add: q_def keys_except)
next
show "P q"
proof (rule step(1))
from step(2) ‹t ∈ keys p› show "n = card (keys q)" unfolding q_def keys_except
by (metis Suc_inject card.remove finite_keys)
qed
qed
qed

lemma except_Diff_singleton: "except p (keys p - {t}) = Poly_Mapping.single t (lookup p t)"
by (rule poly_mapping_eqI) (simp add: lookup_single in_keys_iff lookup_except when_def)

lemma except_Un_plus_Int: "except p (U ∪ V) + except p (U ∩ V) = except p U + except p V"

corollary except_Int:
assumes "keys p ⊆ U ∪ V"
shows "except p (U ∩ V) = except p U + except p V"
proof -
from assms have "except p (U ∪ V) = 0" by (rule except_eq_zeroI)
hence "except p (U ∩ V) = except p (U ∪ V) + except p (U ∩ V)" by simp
also have "… = except p U + except p V" by (fact except_Un_plus_Int)
finally show ?thesis .
qed

lemma except_keys_Int [simp]: "except p (keys p ∩ U) = except p U"
by (rule poly_mapping_eqI) (simp add: in_keys_iff lookup_except)

lemma except_Int_keys [simp]: "except p (U ∩ keys p) = except p U"
by (simp only: Int_commute[of U] except_keys_Int)

lemma except_keys_Diff: "except p (keys p - U) = except p (- U)"
proof -
have "except p (keys p - U) = except p (keys p ∩ (- U))" by (simp only: Diff_eq)
also have "… = except p (- U)" by simp
finally show ?thesis .
qed

lemma except_decomp: "p = except p U + except p (- U)"

corollary except_Compl: "except p (- U) = p - except p U"

context plus begin

where "b adds a ⟷ (∃k. a = b + k)"

lemma addsI [intro?]: "a = b + k ⟹ b adds a"

lemma addsE [elim?]: "b adds a ⟹ (⋀k. a = b + k ⟹ P) ⟹ P"

end

begin

proof
show "a = a + 0" by simp
qed

proof -
from assms obtain v where "b = a + v"
moreover from assms obtain w where "c = b + w"
ultimately have "c = a + (v + w)"
then show ?thesis ..
qed

shows "a + c adds b + d"
proof -
from ‹a adds b› obtain b' where "b = a + b'" ..
moreover from ‹c adds d› obtain d' where "d = c + d'" ..
ultimately have "b + d = (a + c) + (b' + d')"
then show ?thesis ..
qed

end

assumes plus_eq_zero: "s + t = 0 ⟹ s = 0"
begin

lemma plus_eq_zero_2: "t = 0" if "s + t = 0"
using that
by (simp only: add_commute[of s t] plus_eq_zero)

proof
from this obtain k where "0 = s + k" unfolding adds_def ..
from this plus_eq_zero[of s k] show "s = 0"
by blast
next
assume "s = 0"
thus "s adds 0" by simp
qed

end

begin
end

begin

lemma adds_canc: "s + u adds t + u ⟷ s adds t" for s t u::'a
apply auto

lemma add_minus_2: "(s + t) - s = t"
by simp

shows "(t - s) + s = t"
proof -
from assms adds_def[of s t] obtain u where u: "t = u + s" by (auto simp: ac_simps)
then have "t - s = u"
by simp
thus ?thesis using u by simp
qed

assumes "(s + t) adds u"
shows "s adds (u - t)"
proof -
from assms have "(s + t) adds ((u - t) + t)" using adds_minus local.plus_adds_right by presburger
thus ?thesis using adds_canc[of s t "u - t"] by simp
qed

shows "(s + t) adds u"

proof
assume a1: "(s + t) adds u"
proof
next
qed
next
hence "t adds u" and "s adds (u - t)" by auto
qed

lemma minus_plus:
shows "(t - s) + u = (t + u) - s"
proof -
from assms obtain k where k: "t = s + k" unfolding adds_def ..
hence "t - s = k" by simp
also from k have "(t + u) - s = k + u"
finally show ?thesis by simp
qed

lemma minus_plus_minus:
shows "(t - s) + (v - u) = (t + v) - (s + u)"

lemma minus_plus_minus_cancel:
shows "(t - u) + (u - s) = t - s"

end

text ‹Instances of class ‹lcs_powerprod› are types of commutative power-products admitting
(not necessarily unique) least common sums (inspired from least common multiplies).
Note that if the components of indeterminates are arbitrary integers (as for instance in Laurent
polynomials), then no unique lcss exist.›
class lcs_powerprod = comm_powerprod +
fixes lcs::"'a ⇒ 'a ⇒ 'a"
assumes lcs_comm: "lcs s t = lcs t s"
begin

by (simp only: lcs_comm[of s t], rule adds_lcs)

text ‹"gcs" stands for "greatest common summand".›
definition gcs :: "'a ⇒ 'a ⇒ 'a" where "gcs s t = (s + t) - (lcs s t)"

lemma gcs_plus_lcs: "(gcs s t) + (lcs s t) = s + t"

proof -
have "t adds (lcs s t)" (is "t adds ?l") unfolding lcs_comm[of s t] by (fact adds_lcs)
then obtain u where eq1: "?l = t + u" unfolding adds_def ..
from lcs_adds_plus[of s t] obtain v where eq2: "s + t = ?l + v" unfolding adds_def ..
hence "t + s = t + (u + v)" unfolding eq1 by (simp add: ac_simps)
hence s: "s = u + v" unfolding add_left_cancel .
show ?thesis unfolding eq2 gcs_def unfolding s by simp
qed

lemma gcs_comm: "gcs s t = gcs t s" unfolding gcs_def by (simp add: lcs_comm ac_simps)

by (simp only: gcs_comm[of s t], rule gcs_adds)

end

class ulcs_powerprod = lcs_powerprod + ninv_comm_monoid_add
begin

shows "s = t"
proof -
from ‹s adds t› obtain u where u_def: "t = s + u" unfolding adds_def ..
from ‹t adds s› obtain v where v_def: "s = t + v" unfolding adds_def ..
from u_def v_def have "s = (s + u) + v" by (simp add: ac_simps)
hence "s + 0 = s + (u + v)" by (simp add: ac_simps)
hence "u + v = 0" by simp
hence "u = 0" using plus_eq_zero[of u v] by simp
thus ?thesis using u_def by simp
qed

lemma lcs_unique:
shows "l = lcs s t"

lemma lcs_zero: "lcs 0 t = t"

lemma lcs_plus_left: "lcs (u + s) (u + t) = u + lcs s t"
fix v
hence "s adds v - u" ..
assume "t adds v - u"
with ‹s adds v - u› show "lcs s t adds v - u" by (rule lcs_adds)
qed

lemma lcs_plus_right: "lcs (s + u) (t + u) = (lcs s t) + u"
using lcs_plus_left[of u s t] by (simp add: ac_simps)

shows "u adds (gcs s t)"
proof -
from assms have "s + u adds s + t" and "t + u adds t + s"
hence "lcs (s + u) (t + u) adds s + t"
hence "u + (lcs s t) adds s + t" unfolding lcs_plus_right by (simp add: ac_simps)
hence "u adds (s + t) - (lcs s t)" unfolding plus_adds ..
thus ?thesis unfolding gcs_def .
qed

lemma gcs_unique:
shows "g = gcs s t"

lemma gcs_plus_left: "gcs (u + s) (u + t) = u + gcs s t"
proof -
have "u + s + (u + t) - (u + lcs s t) = u + s + (u + t) - u - lcs s t" by (simp only: diff_diff_add)
also have "... = u + s + t + (u - u) - lcs s t" by (simp add: add.left_commute)
also have "... = u + s + t - lcs s t" by simp
also have "... =  u + (s + t - lcs s t)"
finally show ?thesis unfolding gcs_def lcs_plus_left .
qed

lemma gcs_plus_right: "gcs (s + u) (t + u) = (gcs s t) + u"
using gcs_plus_left[of u s t] by (simp add: ac_simps)

lemma lcs_same [simp]: "lcs s s = s"
proof -
ultimately show ?thesis by (rule adds_antisym)
qed

lemma gcs_same [simp]: "gcs s s = s"
proof -
ultimately show ?thesis by (rule adds_antisym)
qed

end

subsection ‹Dickson Classes›

definition (in plus) dickson_grading :: "('a ⇒ nat) ⇒ bool"
((∀s t. d (s + t) = max (d s) (d t)) ∧ (∀n::nat. almost_full_on (adds) {x. d x ≤ n}))"

definition dgrad_set :: "('a ⇒ nat) ⇒ nat ⇒ 'a set"
where "dgrad_set d m = {t. d t ≤ m}"

definition dgrad_set_le :: "('a ⇒ nat) ⇒ ('a set) ⇒ ('a set) ⇒ bool"
where "dgrad_set_le d S T ⟷ (∀s∈S. ∃t∈T. d s ≤ d t)"

assumes "⋀s t. d (s + t) = max (d s) (d t)"
assumes "⋀n::nat. almost_full_on (adds) {x. d x ≤ n}"
unfolding dickson_grading_def using assms by blast

lemma dickson_gradingD1: "dickson_grading d ⟹ d (s + t) = max (d s) (d t)"

shows "wqo_on (adds) {x. d x ≤ n}"
proof (intro wqo_onI transp_onI)
fix x y z :: 'a
next
from assms show "almost_full_on (adds) {x. d x ≤ n}" by (rule dickson_gradingD2)
qed

assumes "dickson_grading d" and "⋀i::nat. d ((seq::nat ⇒ 'a::plus) i) ≤ n"
obtains i j where "i < j" and "seq i adds seq j"
proof -
from assms(1) have "almost_full_on (adds) {x. d x ≤ n}" by (rule dickson_gradingD2)
moreover from assms(2) have "⋀i. seq i ∈ {x. d x ≤ n}" by simp
ultimately obtain i j where "i < j" and "seq i adds seq j" by (rule almost_full_onD)
thus ?thesis ..
qed

shows "d s ≤ d t"
proof -
from assms(2) obtain u where "t = s + u" ..
hence "d t = max (d s) (d u)" by (simp only: dickson_gradingD1[OF assms(1)])
thus ?thesis by simp
qed

shows "d (t - s) ≤ d t"
proof -
from assms(2) obtain u where "t = s + u" ..
hence "t - s = u" by simp
from assms(1) have "d t = ord_class.max (d s) (d u)" unfolding ‹t = s + u› by (rule dickson_gradingD1)
thus ?thesis by (simp add: ‹t - s = u›)
qed

shows "d (lcs s t) ≤ max (d s) (d t)"
proof -
from assms have "d (lcs s t) ≤ d (s + t)" by (rule dickson_grading_adds_imp_le, intro lcs_adds_plus)
thus ?thesis by (simp only: dickson_gradingD1[OF assms])
qed

shows "d (lcs s t - s) ≤ max (d s) (d t)"
proof -
from assms have "d (lcs s t - s) ≤ d (lcs s t)" by (rule dickson_grading_minus, intro adds_lcs)
also from assms have "... ≤ max (d s) (d t)" by (rule dickson_grading_lcs)
finally show ?thesis .
qed

assumes "⋀s. s ∈ S ⟹ ∃t∈T. d s ≤ d t"
using assms by (auto simp: dgrad_set_le_def)

assumes "dgrad_set_le d S T" and "s ∈ S"
obtains t where "t ∈ T" and "d s ≤ d t"
using assms by (auto simp: dgrad_set_le_def)

assumes "finite F"
shows "F ⊆ dgrad_set d (Max (d  F))"
proof
fix f
assume "f ∈ F"
hence "d f ∈ d  F" by simp
with _ have "d f ≤ Max (d  F)"
proof (rule Max_ge)
from assms show "finite (d  F)" by auto
qed
hence "dgrad_set d (d f) ⊆ dgrad_set d (Max (d  F))" by (auto simp: dgrad_set_def)
ultimately show "f ∈ dgrad_set d (Max (d  F))" ..
qed

assumes "finite F"
obtains m where "F ⊆ dgrad_set d m"
proof
from assms show "F ⊆ dgrad_set d (Max (d  F))" by (rule dgrad_set_exhaust_expl)
qed

proof
fix s
assume "s ∈ S"
with assms(1) obtain t where "t ∈ T" and 1: "d s ≤ d t" by (auto simp add: dgrad_set_le_def)
from assms(2) this(1) obtain u where "u ∈ U" and 2: "d t ≤ d u" by (auto simp add: dgrad_set_le_def)
from this(1) show "∃u∈U. d s ≤ d u"
proof
from 1 2 show "d s ≤ d u" by (rule le_trans)
qed
qed

assumes "S ⊆ T"
unfolding dgrad_set_le_def using assms by blast

shows "F ⊆ dgrad_set d m"
proof
fix f
assume "f ∈ F"
with assms(1) obtain g where "g ∈ G" and *: "d f ≤ d g" by (auto simp add: dgrad_set_le_def)
from assms(2) this(1) have "g ∈ dgrad_set d m" ..
with * have "d f ≤ m" by (rule le_trans)
qed

assumes "d t ≤ m"
shows "t ∈ dgrad_set d m"
using assms by (auto simp: dgrad_set_def)

assumes "t ∈ dgrad_set d m"
shows "d t ≤ m"

by auto

by simp

assumes "m ≤ n"
using assms by (auto simp: dgrad_set_def)

shows "s + t ∈ dgrad_set d m"
proof -
from assms(1) have "d (s + t) = ord_class.max (d s) (d t)" by (rule dickson_gradingD1)
also from assms(2, 3) have "... ≤ m" by (simp add: dgrad_set_def)
qed

shows "s - t ∈ dgrad_set d m"
proof -
from assms(1, 3) have "d (s - t) ≤ d s" by (rule dickson_grading_minus)
qed

shows "lcs s t ∈ dgrad_set d m"
proof -
from assms(1) have "d (lcs s t) ≤ ord_class.max (d s) (d t)" by (rule dickson_grading_lcs)
also from assms(2, 3) have "... ≤ m" by (simp add: dgrad_set_def)
qed

obtains T where "finite T" and "T ⊆ S" and "⋀s. s ∈ S ⟹ (∃t∈T. t adds (s::'a::cancel_comm_monoid_add))"
proof -
moreover from assms(2) have "almost_full_on (adds) S"
proof (rule almost_full_on_subset)
qed
ultimately obtain T where "finite T" and "T ⊆ S" and "⋀s. s ∈ S ⟹ (∃t∈T. t adds s)"
by (rule almost_full_on_finite_subsetE, blast)
thus ?thesis ..
qed

begin

class dickson_powerprod = ulcs_powerprod +
begin

end (* dickson_powerprod *)

text ‹Class @{class graded_dickson_powerprod} is a slightly artificial construction. It is needed,
because type @{typ "nat ⇒⇩0 nat"} does not satisfy the usual conditions of a "Dickson domain" (as
formulated in class @{class dickson_powerprod}), but we still want to use that type as the type of
power-products in the computation of Gr\"obner bases. So, we exploit the fact that in a finite
set of polynomials (which is the input of Buchberger's algorithm) there is always some "highest"
indeterminate that occurs with non-zero exponent, and no "higher" indeterminates are generated
during the execution of the algorithm. This allows us to prove that the algorithm terminates, even
though there are in principle infinitely many indeterminates.›

lemma group_eq_aux: "a + (b - a) = (b::'a::ab_group_add)"
proof -
have "a + (b - a) = b - a + a" by simp
also have "... = b" by simp
finally show ?thesis .
qed

assumes le_imp_add: "a ≤ b ⟹ (∃c. b = a + c)"

begin
end

begin

lemma le_imp_inv:
assumes "a ≤ b"
shows "b = a + (b - a)"

lemma max_eq_sum:
obtains y where "max a b = a + y"
unfolding max_def
proof (cases "a ≤ b")
case True
hence "b = a + (b - a)" by (rule le_imp_inv)
then obtain c where eq: "b = a + c" ..
show ?thesis
proof
from True show "max a b = a + c" unfolding max_def eq by simp
qed
next
case False
show ?thesis
proof
from False show "max a b = a + 0" unfolding max_def by simp
qed
qed

lemma min_plus_max:
shows "(min a b) + (max a b) = a + b"
proof (cases "a ≤ b")
case True
thus ?thesis unfolding min_def max_def by simp
next
case False
thus ?thesis unfolding min_def max_def by (simp add: ac_simps)
qed

assumes zero_min: "0 ≤ x"
begin

proof
fix x y
assume *: "x + y = 0"
show "x = 0"
proof -
from zero_min[of x] have "0 = x ∨ x > 0" by auto
thus ?thesis
proof
assume "x > 0"
have "0 ≤ y" by (fact zero_min)
also have "... = 0 + y" by simp
also from ‹x > 0› have "... < x + y" by (rule add_strict_right_mono)
finally have "0 < x + y" .
hence "x + y ≠ 0" by simp
from this * show ?thesis ..
qed simp
qed
qed

shows "x ≤ x + y"
using add_left_mono[OF zero_min[of y], of x] by simp

shows "x ≤ y + x"
using add_right_mono[OF zero_min[of y], of x] by simp

begin

instance by (standard, simp)

begin
instance by (standard, simp)
end

begin
instance ..
end

begin

proof (standard, intro exI)
fix a b
show "b = a + (b - a)" using add_commute local.diff_add_cancel by auto
qed

begin
instance ..
end

begin
instance ..
end

begin
instance ..
end

subsection ‹Ordered Power-Products›

locale ordered_powerprod =
ordered_powerprod_lin: linorder ord ord_strict
for ord::"'a ⇒ 'a::comm_powerprod ⇒ bool" (infixl "≼" 50)
and ord_strict::"'a ⇒ 'a::comm_powerprod ⇒ bool" (infixl "≺" 50) +
assumes zero_min: "0 ≼ t"
assumes plus_monotone: "s ≼ t ⟹ s + u ≼ t + u"
begin

abbreviation ord_conv (infixl "≽" 50) where "ord_conv ≡ (≼)¯¯"
abbreviation ord_strict_conv (infixl "≻" 50) where "ord_strict_conv ≡ (≺)¯¯"

lemma ord_canc:
assumes "s + u ≼ t + u"
shows "s ≼ t"
proof (rule ordered_powerprod_lin.le_cases[of s t], simp)
assume "t ≼ s"
from assms plus_monotone[OF this, of u] have "t + u = s + u"
using ordered_powerprod_lin.order.eq_iff by simp
hence "t = s" by simp
thus "s ≼ t" by simp
qed

shows "s ≼ t"
proof -
from assms have "∃u. t = s + u" unfolding adds_def by simp
then obtain k where "t = s + k" ..
thus ?thesis using plus_monotone[OF zero_min[of k], of s] by (simp add: ac_simps)
qed

lemma ord_canc_left:
assumes "u + s ≼ u + t"
shows "s ≼ t"
using assms unfolding add.commute[of u] by (rule ord_canc)

lemma ord_strict_canc:
assumes "s + u ≺ t + u"
shows "s ≺ t"
using assms ord_canc[of s u t] add_right_cancel[of s u t]
ordered_powerprod_lin.le_imp_less_or_eq ordered_powerprod_lin.order.strict_implies_order by blast

lemma ord_strict_canc_left:
assumes "u + s ≺ u + t"
shows "s ≺ t"
using assms unfolding add.commute[of u] by (rule ord_strict_canc)

lemma plus_monotone_left:
assumes "s ≼ t"
shows "u + s ≼ u + t"
using assms

lemma plus_monotone_strict:
assumes "s ≺ t"
shows "s + u ≺ t + u"
using assms

lemma plus_monotone_strict_left:
assumes "s ≺ t"
shows "u + s ≺ u + t"
using assms

end

locale gd_powerprod =
ordered_powerprod ord ord_strict
for ord::"'a ⇒ 'a::graded_dickson_powerprod ⇒ bool" (infixl "≼" 50)
and ord_strict (infixl "≺" 50)
begin

definition dickson_le :: "('a ⇒ nat) ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool"
where "dickson_le d m s t ⟷ (d s ≤ m ∧ d t ≤ m ∧ s ≼ t)"

definition dickson_less :: "('a ⇒ nat) ⇒ nat ⇒ 'a ⇒ 'a ⇒ bool"
where "dickson_less d m s t ⟷ (d s ≤ m ∧ d t ≤ m ∧ s ≺ t)"

lemma dickson_leI:
assumes "d s ≤ m" and "d t ≤ m" and "s ≼ t"
shows "dickson_le d m s t"
using assms by (simp add: dickson_le_def)

lemma dickson_leD1:
assumes "dickson_le d m s t"
shows "d s ≤ m"
using assms by (simp add: dickson_le_def)

lemma dickson_leD2:
assumes "dickson_le d m s t"
shows "d t ≤ m"
using assms by (simp add: dickson_le_def)

lemma dickson_leD3:
assumes "dickson_le d m s t"
shows "s ≼ t"
using assms by (simp add: dickson_le_def)

lemma dickson_le_trans:
assumes "dickson_le d m s t" and "dickson_le d m t u"
shows "dickson_le d m s u"
using assms by (auto simp add: dickson_le_def)

lemma dickson_lessI:
assumes "d s ≤ m" and "d t ≤ m" and "s ≺ t"
shows "dickson_less d m s t"
using assms by (simp add: dickson_less_def)

lemma dickson_lessD1:
assumes "dickson_less d m s t"
shows "d s ≤ m"
using assms by (simp add: dickson_less_def)

lemma dickson_lessD2:
assumes "dickson_less d m s t"
shows "d t ≤ m"
using assms by (simp add: dickson_less_def)

lemma dickson_lessD3:
assumes "dickson_less d m s t"
shows "s ≺ t"
using assms by (simp add: dickson_less_def)

lemma dickson_less_irrefl: "¬ dickson_less d m t t"

lemma dickson_less_trans:
assumes "dickson_less d m s t" and "dickson_less d m t u"
shows "dickson_less d m s u"
using assms by (auto simp add: dickson_less_def)

lemma transp_dickson_less: "transp (dickson_less d m)"
by (rule transpI, fact dickson_less_trans)

lemma wfp_on_ord_strict:
shows "wfp_on (≺) {x. d x ≤ n}"
proof -
let ?A = "{x. d x ≤ n}"
have "strict (≼) = (≺)" by (intro ext, simp only: ordered_powerprod_lin.less_le_not_le)
have "qo_on (adds) ?A" by (auto simp: qo_on_def reflp_on_def transp_on_def dest: adds_trans)
ultimately have "(∀Q. (∀x∈?A. ∀y∈?A. x adds y ⟶ Q x y) ∧ qo_on Q ?A ⟶ wfp_on (strict Q) ?A)"
by (simp only: wqo_extensions_wf_conv)
hence "(∀x∈?A. ∀y∈?A. x adds y ⟶ x ≼ y) ∧ qo_on (≼) ?A ⟶ wfp_on (strict (≼)) ?A" ..
thus ?thesis unfolding ‹strict (≼) = (≺)›
proof
show "(∀x∈?A. ∀y∈?A. x adds y ⟶ x ≼ y) ∧ qo_on (≼) ?A"
proof (intro conjI ballI impI ord_adds)
show "qo_on (≼) ?A" by (auto simp: qo_on_def reflp_on_def transp_on_def)
qed
qed
qed

lemma wf_dickson_less:
shows "wfP (dickson_less d m)"
proof (rule wfP_chain)
show "¬ (∃seq. ∀i. dickson_less d m (seq (Suc i)) (seq i))"
proof
assume "∃seq. ∀i. dickson_less d m (seq (Suc i)) (seq i)"
then obtain seq::"nat ⇒ 'a" where "∀i. dickson_less d m (seq (Suc i)) (seq i)" ..
hence *: "⋀i. dickson_less d m (seq (Suc i)) (seq i)" ..
with transp_dickson_less have seq_decr: "⋀i j. i < j ⟹ dickson_less d m (seq j) (seq i)"
by (rule transp_sequence)

from assms obtain i j where "i < j" and i_adds_j: "seq i adds seq j"
fix i
from * show "d (seq i) ≤ m" by (rule dickson_lessD2)
qed
from ‹i < j› have "dickson_less d m (seq j) (seq i)" by (rule seq_decr)
hence "seq j ≺ seq i" by (rule dickson_lessD3)
moreover from i_adds_j have "seq i ≼ seq j" by (rule ord_adds)
ultimately show False by simp
qed
qed

end

text ‹‹gd_powerprod› stands for @{emph ‹graded ordered Dickson power-products›}.›

locale od_powerprod =
ordered_powerprod ord ord_strict
for ord::"'a ⇒ 'a::dickson_powerprod ⇒ bool" (infixl "≼" 50)
and ord_strict (infixl "≺" 50)
begin

sublocale gd_powerprod by standard

lemma wf_ord_strict: "wfP (≺)"
proof (rule wfP_chain)
show "¬ (∃seq. ∀i. seq (Suc i) ≺ seq i)"
proof
assume "∃seq. ∀i. seq (Suc i) ≺ seq i"
then obtain seq::"nat ⇒ 'a" where "∀i. seq (Suc i) ≺ seq i" ..
hence "⋀i. seq (Suc i) ≺ seq i" ..
with ordered_powerprod_lin.transp_less have seq_decr: "⋀i j. i < j ⟹ (seq j) ≺ (seq i)"
by (rule transp_sequence)

from dickson obtain i j::nat where "i < j" and i_adds_j: "seq i adds seq j"
by (auto elim!: almost_full_onD)
from seq_decr[OF ‹i < j›] have "seq j ≼ seq i ∧ seq j ≠ seq i" by auto
hence "seq j ≼ seq i" and "seq j ≠ seq i" by simp_all
from ‹seq j ≠ seq i› ‹seq j ≼ seq i› ord_adds[OF i_adds_j]
ordered_powerprod_lin.order.eq_iff[of "seq j" "seq i"]
show False by simp
qed
qed

end

text ‹‹od_powerprod› stands for @{emph ‹ordered Dickson power-products›}.›

subsection ‹Functions as Power-Products›

lemma finite_neq_0:
assumes fin_A: "finite {x. f x ≠ 0}" and fin_B: "finite {x. g x ≠ 0}" and "⋀x. h x 0 0 = 0"
shows "finite {x. h x (f x) (g x) ≠ 0}"
proof -
from fin_A fin_B have  "finite ({x. f x ≠ 0} ∪ {x. g x ≠ 0})" by (intro finite_UnI)
hence finite_union: "finite {x. (f x ≠ 0) ∨ (g x ≠ 0)}" by (simp only: Collect_disj_eq)
have "{x. h x (f x) (g x) ≠ 0} ⊆ {x. (f x ≠ 0) ∨ (g x ≠ 0)}"
proof (intro Collect_mono, rule)
fix x::'a
assume h_not_zero: "h x (f x) (g x) ≠ 0"
have "f x = 0 ⟹ g x ≠ 0"
proof
assume "f x = 0" "g x = 0"
thus False using h_not_zero ‹h x 0 0 = 0›  by simp
qed
thus "f x ≠ 0 ∨ g x ≠ 0" by auto
qed
from finite_subset[OF this] finite_union show "finite {x. h x (f x) (g x) ≠ 0}" .
qed

lemma finite_neq_0':
assumes "finite {x. f x ≠ 0}" and "finite {x. g x ≠ 0}" and "h 0 0 = 0"
shows "finite {x. h (f x) (g x) ≠ 0}"
using assms by (rule finite_neq_0)

lemma finite_neq_0_inv:
assumes fin_A: "finite {x. h x (f x) (g x) ≠ 0}" and fin_B: "finite {x. f x ≠ 0}" and "⋀x y. h x 0 y = y"
shows "finite {x. g x ≠ 0}"
proof -
from fin_A and fin_B have "finite ({x. h x (f x) (g x) ≠ 0} ∪ {x. f x ≠ 0})" by (intro finite_UnI)
hence finite_union: "finite {x. (h x (f x) (g x) ≠ 0) ∨ f x ≠ 0}" by (simp only: Collect_disj_eq)
have "{x. g x ≠ 0} ⊆ {x. (h x (f x) (g x) ≠ 0) ∨ f x ≠ 0}"
by (intro Collect_mono, rule, rule disjCI, simp add: assms(3))
from this finite_union show "finite {x. g x ≠ 0}" by (rule finite_subset)
qed

lemma finite_neq_0_inv':
assumes inf_A: "finite {x. h (f x) (g x) ≠ 0}" and fin_B: "finite {x. f x ≠ 0}" and "⋀x. h 0 x = x"
shows "finite {x. g x ≠ 0}"
using assms by (rule finite_neq_0_inv)

subsubsection ‹@{typ "'a ⇒ 'b"} belongs to class @{class comm_powerprod}›

instance "fun" :: (type, cancel_comm_monoid_add) comm_powerprod
by standard

subsubsection ‹@{typ "'a ⇒ 'b"} belongs to class @{class ninv_comm_monoid_add}›

by (standard, simp only: plus_fun_def zero_fun_def fun_eq_iff, intro allI, rule plus_eq_zero, auto)

subsubsection ‹@{typ "'a ⇒ 'b"} belongs to class @{class lcs_powerprod}›

instantiation "fun" :: (type, add_linorder) lcs_powerprod
begin

definition lcs_fun::"('a ⇒ 'b) ⇒ ('a ⇒ 'b) ⇒ ('a ⇒ 'b)" where "lcs f g = (λx. max (f x) (g x))"

assumes "s ≤ t"
shows "s adds (t::'a ⇒ 'b)"
fix x
from assms have "s x ≤ t x" unfolding le_fun_def ..
hence "t x = s x + (t x - s x)" by (rule le_imp_inv)
thus "t x = (s + (t - s)) x" by simp
qed

lemma adds_fun_iff': "f adds (g::'a ⇒ 'b) ⟷ (∀x. ∃y. g x = f x + y)"

shows "s adds (lcs s (t::'a ⇒ 'b))"
by (rule adds_funI, simp only: le_fun_def lcs_fun_def, auto simp: max_def)

lemma lcs_comm_fun:  "lcs s t = lcs t (s::'a ⇒ 'b)"
unfolding lcs_fun_def
by (auto simp: max_def intro!: ext)

shows "(lcs s t) adds u"
proof -
assume a1: "∀x. ∃y. u x = s x + y" and a2: "∀x. ∃y. u x = t x + y"
show "∀x. ∃y. u x = max (s x) (t x) + y"
proof
fix x
from a1 have b1: "∃y. u x = s x + y" ..
from a2 have b2: "∃y. u x = t x + y" ..
show "∃y. u x = max (s x) (t x) + y" unfolding max_def
by (split if_split, intro conjI impI, rule b2, rule b1)
qed
qed

instance
apply standard
subgoal by (rule lcs_comm_fun)
done

end

lemma leq_lcs_fun_1: "s ≤ (lcs s (t::'a ⇒ 'b::add_linorder))"

lemma leq_lcs_fun_2: "t ≤ (lcs s (t::'a ⇒ 'b::add_linorder))"

lemma lcs_leq_fun:
assumes "s ≤ u" and "t ≤ (u::'a ⇒ 'b::add_linorder)"
shows "(lcs s t) ≤ u"
using assms by (simp add: lcs_fun_def le_fun_def)

proof
from this obtain k where "t = s + k" ..
show "s ≤ t" unfolding ‹t = s + k› le_fun_def plus_fun_def le_iff_add by (simp add: leq_add_right)

lemma gcs_fun: "gcs s (t::'a ⇒ ('b::add_linorder)) = (λx. min (s x) (t x))"
proof -
show ?thesis unfolding gcs_def lcs_fun_def fun_diff_def
proof (simp, rule)
fix x
have eq: "s x + t x = max (s x) (t x) + min (s x) (t x)" by (metis add.commute min_def max_def)
thus "s x + t x - max (s x) (t x) = min (s x) (t x)" by simp
qed
qed

lemma gcs_leq_fun_1: "(gcs s (t::'a ⇒ 'b::add_linorder)) ≤ s"

lemma gcs_leq_fun_2: "(gcs s (t::'a ⇒ 'b::add_linorder)) ≤ t"

lemma leq_gcs_fun:
assumes "u ≤ s" and "u ≤ (t::'a ⇒ 'b::add_linorder)"
shows "u ≤ (gcs s t)"
using assms by (simp add: gcs_fun le_fun_def)

subsubsection ‹@{typ "'a ⇒ 'b"} belongs to class @{class ulcs_powerprod}›

instance "fun" :: (type, add_linorder_min) ulcs_powerprod ..

subsubsection ‹Power-products in a given set of indeterminates›

definition supp_fun::"('a ⇒ 'b::zero) ⇒ 'a set" where "supp_fun f = {x. f x ≠ 0}"

text ‹@{term supp_fun} for general functions is like @{term keys} for @{type poly_mapping},
but does not need to be finite.›

lemma keys_eq_supp: "keys s = supp_fun (lookup s)"
unfolding supp_fun_def by (transfer, rule)

lemma supp_fun_zero [simp]: "supp_fun 0 = {}"
by (auto simp: supp_fun_def)

lemma supp_fun_eq_zero_iff: "supp_fun f = {} ⟷ f = 0"
by (auto simp: supp_fun_def)

lemma sub_supp_empty: "supp_fun s ⊆ {} ⟷ (s = 0)"
by (auto simp: supp_fun_def)

lemma except_fun_idI: "supp_fun f ∩ V = {} ⟹ except_fun f V = f"
by (auto simp: except_fun_def supp_fun_def when_def intro!: ext)

lemma supp_except_fun: "supp_fun (except_fun s V) = supp_fun s - V"
by (auto simp: except_fun_def supp_fun_def)

lemma supp_fun_plus_subset: "supp_fun (s + t) ⊆ supp_fun s ∪ supp_fun (t::'a ⇒ 'b::monoid_add)"
unfolding supp_fun_def by force

lemma fun_eq_zeroI:
assumes "⋀x. x ∈ supp_fun f ⟹ f x = 0"
shows "f = 0"
proof (rule, simp)
fix x
show "f x = 0"
proof (cases "x ∈ supp_fun f")
case True
then show ?thesis by (rule assms)
next
case False
then show ?thesis by (simp add: supp_fun_def)
qed
qed

lemma except_fun_cong1:
"supp_fun s ∩ ((V - U) ∪ (U - V)) ⊆ {} ⟹ except_fun s V = except_fun s U"
by (auto simp: except_fun_def when_def supp_fun_def intro!: ext)

"s adds t = (except_fun s V adds except_fun t V ∧ except_fun s (- V) adds except_fun t (- V))"
for s t :: "'a ⇒ 'b::add_linorder"
by (auto simp: supp_fun_def except_fun_def adds_fun_iff when_def)

for s t :: "'a ⇒ 'b::add_linorder"
by (auto simp: supp_fun_def except_fun_def adds_fun_iff when_def)

subsubsection ‹Dickson's lemma for power-products in finitely many indeterminates›

lemma Dickson_fun:
assumes "finite V"
using assms
proof (induct V)
case empty
have "finite {0}" by simp
ultimately have "almost_full_on (adds) {0::'a ⇒ 'b}" by (rule finite_almost_full_on)
thus ?case by (simp add: supp_fun_eq_zero_iff)
next
case (insert v V)
show ?case
proof (rule almost_full_onI)
fix seq::"nat ⇒ 'a ⇒ 'b"
assume "∀i. seq i ∈ {x. supp_fun x ⊆ insert v V}"
hence a: "supp_fun (seq i) ⊆ insert v V" for i by simp
define seq' where "seq' = (λi. (except_fun (seq i) {v}, except_fun (seq i) V))"
have "almost_full_on (adds) {x::'a ⇒ 'b. supp_fun x ⊆ {v}}"
proof (rule almost_full_onI)
fix f::"nat ⇒ 'a ⇒ 'b"
assume "∀i. f i ∈ {x. supp_fun x ⊆ {v}}"
hence b: "supp_fun (f i) ⊆ {v}" for i by simp
let ?f = "λi. f i v"
have "wfP ((<)::'b ⇒ _)" by (simp add: wf wfP_def)
hence "∀f::nat ⇒ 'b. ∃i. f i ≤ f (Suc i)"
hence "∃i. ?f i ≤ ?f (Suc i)" ..
then obtain i where "?f i ≤ ?f (Suc i)" ..
have "i < Suc i" by simp
proof
fix x
show "f i x adds f (Suc i) x"
proof (cases "x = v")
case True
next
case False
with b have "x ∉ supp_fun (f i)" and "x ∉ supp_fun (f (Suc i))" by blast+
thus ?thesis by (simp add: supp_fun_def)
qed
qed
ultimately show "good (adds) f" by (meson goodI)
qed
with insert(3) have
"almost_full_on (prod_le (adds) (adds)) ({x::'a ⇒ 'b. supp_fun x ⊆ V} × {x::'a ⇒ 'b. supp_fun x ⊆ {v}})"
(is "almost_full_on ?P ?A") by (rule almost_full_on_Sigma)
moreover from a have "seq' i ∈ ?A" for i by (auto simp add: seq'_def supp_except_fun)
ultimately obtain i j where "i < j" and "?P (seq' i) (seq' j)" by (rule almost_full_onD)
have "seq i adds seq j" unfolding adds_except_fun[where s="seq i" and V=V]
proof
from ‹?P (seq' i) (seq' j)› show "except_fun (seq i) V adds except_fun (seq j) V"
next
from ‹?P (seq' i) (seq' j)› have "except_fun (seq i) {v} adds except_fun (seq j) {v}"
moreover have "except_fun (seq i) (- V) = except_fun (seq i) {v}"
by (rule except_fun_cong1; use a[of i] insert.hyps(2) in blast)
moreover have "except_fun (seq j) (- V) = except_fun (seq j) {v}"
by (rule except_fun_cong1; use a[of j] insert.hyps(2) in blast)
ultimately show "except_fun (seq i) (- V) adds except_fun (seq j) (- V)" by simp
qed
with ‹i < j› show "good (adds) seq" by (meson goodI)
qed
qed

instance "fun" :: (finite, add_wellorder) dickson_powerprod
proof
have "finite (UNIV::'a set)" by simp
hence "almost_full_on (adds) {x::'a ⇒ 'b. supp_fun x ⊆ UNIV}" by (rule Dickson_fun)
thus "almost_full_on (adds) (UNIV::('a ⇒ 'b) set)" by simp
qed

subsubsection ‹Lexicographic Term Order›

text ‹Term orders are certain linear orders on power-products, satisfying additional requirements.
Further information on term orders can be found, e.\,g., in @{cite Robbiano1985}.›

context wellorder
begin

lemma neq_fun_alt:
assumes "s ≠ (t::'a ⇒ 'b)"
obtains