Theory Simplex.Abstract_Linear_Poly
section ‹Linear Polynomials and Constraints›
theory Abstract_Linear_Poly
imports
Simplex_Algebra
begin
type_synonym var = nat
text‹(Infinite) linear polynomials as functions from vars to coeffs›
definition fun_zero :: "var ⇒ 'a::zero" where
[simp]: "fun_zero == λ v. 0"
definition fun_plus :: "(var ⇒ 'a) ⇒ (var ⇒ 'a) ⇒ var ⇒ 'a::plus" where
[simp]: "fun_plus f1 f2 == λ v. f1 v + f2 v"
definition fun_scale :: "'a ⇒ (var ⇒ 'a) ⇒ (var ⇒ 'a::ring)" where
[simp]: "fun_scale c f == λ v. c*(f v)"
definition fun_coeff :: "(var ⇒ 'a) ⇒ var ⇒ 'a" where
[simp]: "fun_coeff f var = f var"
definition fun_vars :: "(var ⇒ 'a::zero) ⇒ var set" where
[simp]: "fun_vars f = {v. f v ≠ 0}"
definition fun_vars_list :: "(var ⇒ 'a::zero) ⇒ var list" where
[simp]: "fun_vars_list f = sorted_list_of_set {v. f v ≠ 0}"
definition fun_var :: "var ⇒ (var ⇒ 'a::{zero,one})" where
[simp]: "fun_var x = (λ x'. if x' = x then 1 else 0)"
type_synonym 'a valuation = "var ⇒ 'a"
definition fun_valuate :: "(var ⇒ rat) ⇒ 'a valuation ⇒ ('a::rational_vector)" where
[simp]: "fun_valuate lp val = (∑x∈{v. lp v ≠ 0}. lp x *R val x)"
text‹Invariant -- only finitely many variables›
definition inv where
[simp]: "inv c == finite {v. c v ≠ 0}"
lemma inv_fun_zero [simp]:
"inv fun_zero" by simp
lemma inv_fun_plus [simp]:
"⟦inv (f1 :: nat ⇒ 'a::monoid_add); inv f2⟧ ⟹ inv (fun_plus f1 f2)"
proof-
have *: "{v. f1 v + f2 v ≠ (0 :: 'a)} ⊆ {v. f1 v ≠ (0 :: 'a)} ∪ {v. f2 v ≠ (0 :: 'a)}"
by auto
assume "inv f1" "inv f2"
then show ?thesis
using *
by (auto simp add: finite_subset)
qed
lemma inv_fun_scale [simp]:
"inv (f :: nat ⇒ 'a::ring) ⟹ inv (fun_scale r f)"
proof-
have *: "{v. r * (f v) ≠ 0} ⊆ {v. f v ≠ 0}"
by auto
assume "inv f"
then show ?thesis
using *
by (auto simp add: finite_subset)
qed
text‹linear-poly type -- rat coeffs›
typedef linear_poly = "{c :: var ⇒ rat. inv c}"
by (rule_tac x="λ v. 0" in exI) auto
text‹Linear polynomials are of the form $a_1 \cdot x_1 + ... + a_n
\cdot x_n$. Their formalization follows the data-refinement approach
of Isabelle/HOL \<^cite>‹"florian-refinement"›. Abstract representation of
polynomials are functions mapping variables to their coefficients,
where only finitely many variables have non-zero
coefficients. Operations on polynomials are defined as operations on
functions. For example, the sum of @{term "p⇩1"} and ‹p⇩2› is
defined by @{term "λ v. p⇩1 v + p⇩2 v"} and the value of a polynomial
@{term "p"} for a valuation @{term "v"} (denoted by ‹p⦃v⦄›),
is defined by @{term "∑x∈{x. p x ≠ 0}. p x * v x"}. Executable
representation of polynomials uses RBT mappings instead of functions.
›
setup_lifting type_definition_linear_poly
text‹Vector space operations on polynomials›
instantiation linear_poly :: rational_vector
begin
lift_definition zero_linear_poly :: "linear_poly" is fun_zero by (rule inv_fun_zero)
lift_definition plus_linear_poly :: "linear_poly ⇒ linear_poly ⇒ linear_poly" is fun_plus
by (rule inv_fun_plus)
lift_definition scaleRat_linear_poly :: "rat ⇒ linear_poly ⇒ linear_poly" is fun_scale
by (rule inv_fun_scale)
definition uminus_linear_poly :: "linear_poly ⇒ linear_poly" where
"uminus_linear_poly lp = -1 *R lp"
definition minus_linear_poly :: "linear_poly ⇒ linear_poly ⇒ linear_poly" where
"minus_linear_poly lp1 lp2 = lp1 + (- lp2)"
instance
proof
fix a b c::linear_poly
show "a + b + c = a + (b + c)" by (transfer, auto)
show "a + b = b + a" by (transfer, auto)
show "0 + a = a" by (transfer, auto)
show "-a + a = 0" unfolding uminus_linear_poly_def by (transfer, auto)
show "a - b = a + (- b)" unfolding minus_linear_poly_def ..
next
fix a :: rat and x y :: linear_poly
show "a *R (x + y) = a *R x + a *R y" by (transfer, auto simp: field_simps)
next
fix a b::rat and x::linear_poly
show "(a + b) *R x = a *R x + b *R x" by (transfer, auto simp: field_simps)
show "a *R b *R x = (a * b) *R x" by (transfer, auto simp: field_simps)
next
fix x::linear_poly
show "1 *R x = x" by (transfer, auto)
qed
end
text‹Coefficient›
lift_definition coeff :: "linear_poly ⇒ var ⇒ rat" is fun_coeff .
lemma coeff_plus [simp] : "coeff (lp1 + lp2) var = coeff lp1 var + coeff lp2 var"
by transfer auto
lemma coeff_scaleRat [simp]: "coeff (k *R lp1) var = k * coeff lp1 var"
by transfer auto
lemma coeff_uminus [simp]: "coeff (-lp) var = - coeff lp var"
unfolding uminus_linear_poly_def
by transfer auto
lemma coeff_minus [simp]: "coeff (lp1 - lp2) var = coeff lp1 var - coeff lp2 var"
unfolding minus_linear_poly_def uminus_linear_poly_def
by transfer auto
text‹Set of variables›
lift_definition vars :: "linear_poly ⇒ var set" is fun_vars .
lemma coeff_zero: "coeff p x ≠ 0 ⟷ x ∈ vars p"
by transfer auto
lemma finite_vars: "finite (vars p)"
by transfer auto
text‹List of variables›
lift_definition vars_list :: "linear_poly ⇒ var list" is fun_vars_list .
lemma set_vars_list: "set (vars_list lp) = vars lp"
by transfer auto
text‹Construct single variable polynomial›
lift_definition Var :: "var ⇒ linear_poly" is fun_var by auto
text‹Value of a polynomial in a given valuation›
lift_definition valuate :: "linear_poly ⇒ 'a valuation ⇒ ('a::rational_vector)" is fun_valuate .
syntax
"_valuate" :: "linear_poly ⇒ 'a valuation ⇒ 'a" (‹_ ⦃ _ ⦄›)
syntax_consts
"_valuate" == valuate
translations
"p⦃v⦄ " == "CONST valuate p v"
lemma valuate_zero: "(0 ⦃v⦄) = 0"
by transfer auto
lemma
valuate_diff: "(p ⦃v1⦄) - (p ⦃v2⦄) = (p ⦃ λ x. v1 x - v2 x ⦄)"
by (transfer, simp add: sum_subtractf[THEN sym], auto simp: rational_vector.scale_right_diff_distrib)
lemma valuate_opposite_val:
shows "p ⦃ λ x. - v x ⦄ = - (p ⦃ v ⦄)"
using valuate_diff[of p "λ x. 0" v]
by (auto simp add: valuate_def)
lemma valuate_nonneg:
fixes v :: "'a::linordered_rational_vector valuation"
assumes "∀ x ∈ vars p. (coeff p x > 0 ⟶ v x ≥ 0) ∧ (coeff p x < 0 ⟶ v x ≤ 0)"
shows "p ⦃ v ⦄ ≥ 0"
using assms
proof (transfer, unfold fun_valuate_def, goal_cases)
case (1 p v)
from 1 have fin: "finite {v. p v ≠ 0}" by auto
then show "0 ≤ (∑x∈{v. p v ≠ 0}. p x *R v x)"
proof (induct rule: finite_induct)
case empty show ?case by auto
next
case (insert x F)
show ?case unfolding sum.insert[OF insert(1-2)]
proof (rule order.trans[OF _ add_mono[OF _ insert(3)]])
show "0 ≤ p x *R v x" using scaleRat_leq1[of 0 "v x" "p x"]
using scaleRat_leq2[of "v x" 0 "p x"] 1(2)
by (cases "p x > 0"; cases "p x < 0"; auto)
qed auto
qed
qed
lemma valuate_nonpos:
fixes v :: "'a::linordered_rational_vector valuation"
assumes "∀ x ∈ vars p. (coeff p x > 0 ⟶ v x ≤ 0) ∧ (coeff p x < 0 ⟶ v x ≥ 0)"
shows "p ⦃ v ⦄ ≤ 0"
using assms
using valuate_opposite_val[of p v]
using valuate_nonneg[of p "λ x. - v x"]
using scaleRat_leq2[of "0::'a" _ "-1"]
using scaleRat_leq2[of _ "0::'a" "-1"]
by force
lemma valuate_uminus: "(-p) ⦃v⦄ = - (p ⦃v⦄)"
unfolding uminus_linear_poly_def
by (transfer, auto simp: sum_negf)
lemma valuate_add_lemma:
fixes v :: "'a ⇒ 'b::rational_vector"
assumes "finite {v. f1 v ≠ 0}" "finite {v. f2 v ≠ 0}"
shows
"(∑x∈{v. f1 v + f2 v ≠ 0}. (f1 x + f2 x) *R v x) =
(∑x∈{v. f1 v ≠ 0}. f1 x *R v x) + (∑x∈{v. f2 v ≠ 0}. f2 x *R v x)"
proof-
let ?A = "{v. f1 v + f2 v ≠ 0} ∪ {v. f1 v + f2 v = 0 ∧ (f1 v ≠ 0 ∨ f2 v ≠ 0)}"
have "?A = {v. f1 v ≠ 0 ∨ f2 v ≠ 0}"
by auto
then have
"finite ?A"
using assms
by (subgoal_tac "{v. f1 v ≠ 0 ∨ f2 v ≠ 0} = {v. f1 v ≠ 0} ∪ {v. f2 v ≠ 0}") auto
then have "(∑x∈{v. f1 v + f2 v ≠ 0}. (f1 x + f2 x) *R v x) =
(∑x∈{v. f1 v + f2 v ≠ 0} ∪ {v. f1 v + f2 v = 0 ∧ (f1 v ≠ 0 ∨ f2 v ≠ 0)}. (f1 x + f2 x) *R v x)"
by (rule sum.mono_neutral_left) auto
also have "... = (∑x ∈ {v. f1 v ≠ 0 ∨ f2 v ≠ 0}. (f1 x + f2 x) *R v x)"
by (rule sum.cong) auto
also have "... = (∑x ∈ {v. f1 v ≠ 0 ∨ f2 v ≠ 0}. f1 x *R v x) +
(∑x ∈ {v. f1 v ≠ 0 ∨ f2 v ≠ 0}. f2 x *R v x)"
by (simp add: scaleRat_left_distrib sum.distrib)
also have "... = (∑x∈{v. f1 v ≠ 0}. f1 x *R v x) + (∑x∈{v. f2 v ≠ 0}. f2 x *R v x)"
proof-
{
fix f1 f2::"'a ⇒ rat"
assume "finite {v. f1 v ≠ 0}" "finite {v. f2 v ≠ 0}"
then have "finite {v. f1 v ≠ 0 ∨ f2 v ≠ 0 ∧ f1 v = 0}"
by (subgoal_tac "{v. f1 v ≠ 0 ∨ f2 v ≠ 0} = {v. f1 v ≠ 0} ∪ {v. f2 v ≠ 0}") auto
have "(∑x∈{v. f1 v ≠ 0 ∨ f2 v ≠ 0}. f1 x *R v x) =
(∑x∈{v. f1 v ≠ 0 ∨ (f2 v ≠ 0 ∧ f1 v = 0)}. f1 x *R v x)"
by auto
also have "... = (∑x∈{v. f1 v ≠ 0}. f1 x *R v x)"
using ‹finite {v. f1 v ≠ 0 ∨ f2 v ≠ 0 ∧ f1 v = 0}›
by (rule sum.mono_neutral_left[THEN sym]) auto
ultimately have "(∑x∈{v. f1 v ≠ 0 ∨ f2 v ≠ 0}. f1 x *R v x) =
(∑x∈{v. f1 v ≠ 0}. f1 x *R v x)"
by simp
}
note * = this
show ?thesis
using assms
using *[of f1 f2]
using *[of f2 f1]
by (subgoal_tac "{v. f2 v ≠ 0 ∨ f1 v ≠ 0} = {v. f1 v ≠ 0 ∨ f2 v ≠ 0}") auto
qed
ultimately
show ?thesis by simp
qed
lemma valuate_add: "(p1 + p2) ⦃v⦄ = (p1 ⦃v⦄) + (p2 ⦃v⦄)"
by (transfer, simp add: valuate_add_lemma)
lemma valuate_minus: "(p1 - p2) ⦃v⦄ = (p1 ⦃v⦄) - (p2 ⦃v⦄)"
unfolding minus_linear_poly_def valuate_add
by (simp add: valuate_uminus)
lemma valuate_scaleRat:
"(c *R lp) ⦃ v ⦄ = c *R ( lp⦃v⦄ )"
proof (cases "c=0")
case True
then show ?thesis
by (auto simp add: valuate_def zero_linear_poly_def Abs_linear_poly_inverse)
next
case False
then have "⋀ v. Rep_linear_poly (c *R lp) v = c * (Rep_linear_poly lp v)"
unfolding scaleRat_linear_poly_def
using Abs_linear_poly_inverse[of "λv. c * Rep_linear_poly lp v"]
using Rep_linear_poly
by auto
then show ?thesis
unfolding valuate_def
using ‹c ≠ 0›
by auto (subst rational_vector.scale_sum_right, auto)
qed
lemma valuate_Var: "(Var x) ⦃v⦄ = v x"
by transfer auto
lemma valuate_sum: "((∑x∈A. f x) ⦃ v ⦄) = (∑x∈A. ((f x) ⦃ v ⦄))"
by (induct A rule: infinite_finite_induct, auto simp: valuate_zero valuate_add)
lemma distinct_vars_list:
"distinct (vars_list p)"
by transfer (use distinct_sorted_list_of_set in auto)
lemma zero_coeff_zero: "p = 0 ⟷ (∀ v. coeff p v = 0)"
by transfer auto
lemma all_val:
assumes "∀ (v::var ⇒ 'a::lrv). ∃ v'. (∀ x ∈ vars p. v' x = v x) ∧ (p ⦃v'⦄ = 0)"
shows "p = 0"
proof (subst zero_coeff_zero, rule allI)
fix x
show "coeff p x = 0"
proof (cases "x ∈ vars p")
case False
then show ?thesis
using coeff_zero[of p x]
by simp
next
case True
have "(0::'a::lrv) ≠ (1::'a)"
using zero_neq_one
by auto
let ?v = "λ x'. if x = x' then 1 else 0::'a"
obtain v' where "∀ x ∈ vars p. v' x = ?v x" "p ⦃v'⦄ = 0"
using assms
by (erule_tac x="?v" in allE) auto
then have "∀ x' ∈ vars p. v' x' = (if x = x' then 1 else 0)" "p ⦃v'⦄ = 0"
by auto
let ?fp = "Rep_linear_poly p"
have "{x. ?fp x ≠ 0 ∧ v' x ≠ (0 :: 'a)} = {x}"
using ‹x ∈ vars p› unfolding vars_def
proof (safe, simp_all)
fix x'
assume "v' x' ≠ 0" "Rep_linear_poly p x' ≠ 0"
then show "x' = x"
using ‹∀ x' ∈ vars p. v' x' = (if x = x' then 1 else 0)›
unfolding vars_def
by (erule_tac x="x'" in ballE) (simp_all split: if_splits)
next
assume "v' x = 0" "Rep_linear_poly p x ≠ 0"
then show False
using ‹∀ x' ∈ vars p. v' x' = (if x = x' then 1 else 0)›
using ‹0 ≠ 1›
unfolding vars_def
by simp
qed
have "p ⦃v'⦄ = (∑x∈{v. ?fp v ≠ 0}. ?fp x *R v' x)"
unfolding valuate_def
by auto
also have "... = (∑x∈{v. ?fp v ≠ 0 ∧ v' v ≠ 0}. ?fp x *R v' x)"
apply (rule sum.mono_neutral_left[THEN sym])
using Rep_linear_poly[of p]
by auto
also have "... = ?fp x *R v' x"
using ‹{x. ?fp x ≠ 0 ∧ v' x ≠ (0 :: 'a)} = {x}›
by simp
also have "... = ?fp x *R 1"
using ‹x ∈ vars p›
using ‹∀ x' ∈ vars p. v' x' = (if x = x' then 1 else 0)›
by simp
ultimately
have "p ⦃v'⦄ = ?fp x *R 1"
by simp
then have "coeff p x *R (1::'a)= 0"
using ‹p ⦃v'⦄ = 0›
unfolding coeff_def
by simp
then show ?thesis
using rational_vector.scale_eq_0_iff
using ‹0 ≠ 1›
by simp
qed
qed
lift_definition lp_monom :: "rat ⇒ var ⇒ linear_poly" is
"λ c x y. if x = y then c else 0" by auto
lemma valuate_lp_monom: "((lp_monom c x) ⦃v⦄) = c * (v x)"
proof (transfer, simp, goal_cases)
case (1 c x v)
have id: "{v. x = v ∧ (x = v ⟶ c ≠ 0)} = (if c = 0 then {} else {x})" by auto
show ?case unfolding id
by (cases "c = 0", auto)
qed
lemma valuate_lp_monom_1[simp]: "((lp_monom 1 x) ⦃v⦄) = v x"
by transfer simp
lemma coeff_lp_monom [simp]:
shows "coeff (lp_monom c v) v' = (if v = v' then c else 0)"
by (transfer, auto)
lemma vars_uminus [simp]: "vars (-p) = vars p"
unfolding uminus_linear_poly_def
by transfer auto
lemma vars_plus [simp]: "vars (p1 + p2) ⊆ vars p1 ∪ vars p2"
by transfer auto
lemma vars_minus [simp]: "vars (p1 - p2) ⊆ vars p1 ∪ vars p2"
unfolding minus_linear_poly_def
using vars_plus[of p1 "-p2"] vars_uminus[of p2]
by simp
lemma vars_lp_monom: "vars (lp_monom r x) = (if r = 0 then {} else {x})"
by (transfer, auto)
lemma vars_scaleRat1: "vars (c *R p) ⊆ vars p"
by transfer auto
lemma vars_scaleRat: "c ≠ 0 ⟹ vars(c *R p) = vars p"
by transfer auto
lemma vars_Var [simp]: "vars (Var x) = {x}"
by transfer auto
lemma coeff_Var1 [simp]: "coeff (Var x) x = 1"
by transfer auto
lemma coeff_Var2: "x ≠ y ⟹ coeff (Var x) y = 0"
by transfer auto
lemma valuate_depend:
assumes "∀ x ∈ vars p. v x = v' x"
shows "(p ⦃v⦄) = (p ⦃v'⦄)"
using assms
by transfer auto
lemma valuate_update_x_lemma:
fixes v1 v2 :: "'a::rational_vector valuation"
assumes
"∀y. f y ≠ 0 ⟶ y ≠ x ⟶ v1 y = v2 y"
"finite {v. f v ≠ 0}"
shows
"(∑x∈{v. f v ≠ 0}. f x *R v1 x) + f x *R (v2 x - v1 x) = (∑x∈{v. f v ≠ 0}. f x *R v2 x)"
proof (cases "f x = 0")
case True
then have "∀y. f y ≠ 0 ⟶ v1 y = v2 y"
using assms(1) by auto
then show ?thesis using ‹f x = 0› by auto
next
case False
let ?A = "{v. f v ≠ 0}" and ?Ax = "{v. v ≠ x ∧ f v ≠ 0}"
have "?A = ?Ax ∪ {x}"
using ‹f x ≠ 0› by auto
then have "(∑x∈?A. f x *R v1 x) = f x *R v1 x + (∑x∈?Ax. f x *R v1 x)"
"(∑x∈?A. f x *R v2 x) = f x *R v2 x + (∑x∈?Ax. f x *R v2 x)"
using assms(2) by auto
moreover
have "∀ y ∈ ?Ax. v1 y = v2 y"
using assms by auto
moreover
have "f x *R v1 x + f x *R (v2 x - v1 x) = f x *R v2 x"
by (subst rational_vector.scale_right_diff_distrib) auto
ultimately
show ?thesis by simp
qed
lemma valuate_update_x:
fixes v1 v2 :: "'a::rational_vector valuation"
assumes "∀y ∈ vars lp. y≠x ⟶ v1 y = v2 y"
shows "lp ⦃v1⦄ + coeff lp x *R (v2 x - v1 x) = (lp ⦃v2⦄)"
using assms
unfolding valuate_def vars_def coeff_def
using valuate_update_x_lemma[of "Rep_linear_poly lp" x v1 v2] Rep_linear_poly
by auto
lemma vars_zero: "vars 0 = {}"
using zero_coeff_zero coeff_zero by auto
lemma vars_empty_zero: "vars lp = {} ⟷ lp = 0"
using zero_coeff_zero coeff_zero by auto
definition max_var:: "linear_poly ⇒ var" where
"max_var lp ≡ if lp = 0 then 0 else Max (vars lp)"
lemma max_var_max:
assumes "a ∈ vars lp"
shows "max_var lp ≥ a"
using assms
by (auto simp add: finite_vars max_var_def vars_zero)
lemma max_var_code[code]:
"max_var lp = (let vl = vars_list lp
in if vl = [] then 0 else foldl max (hd vl) (tl vl))"
proof (cases "lp = (0::linear_poly)")
case True
then show ?thesis
using set_vars_list[of lp]
by (auto simp add: max_var_def vars_zero)
next
case False
then show ?thesis
using set_vars_list[of lp, THEN sym]
using vars_empty_zero[of lp]
unfolding max_var_def Let_def
using Max.set_eq_fold[of "hd (vars_list lp)" "tl (vars_list lp)"]
by (cases "vars_list lp", auto simp: foldl_conv_fold intro!: fold_cong)
qed
definition monom_var:: "linear_poly ⇒ var" where
"monom_var l = max_var l"
definition monom_coeff:: "linear_poly ⇒ rat" where
"monom_coeff l = coeff l (monom_var l)"
definition is_monom :: "linear_poly ⇒ bool" where
"is_monom l ⟷ length (vars_list l) = 1"
lemma is_monom_vars_not_empty:
"is_monom l ⟹ vars l ≠ {}"
by (auto simp add: is_monom_def vars_list_def) (auto simp add: vars_def)
lemma monom_var_in_vars:
"is_monom l ⟹ monom_var l ∈ vars l"
using vars_zero
by (auto simp add: monom_var_def max_var_def is_monom_vars_not_empty finite_vars is_monom_def)
lemma zero_is_no_monom[simp]: "¬ is_monom 0"
using is_monom_vars_not_empty vars_zero by blast
lemma is_monom_monom_coeff_not_zero:
"is_monom l ⟹ monom_coeff l ≠ 0"
by (simp add: coeff_zero monom_var_in_vars monom_coeff_def)
lemma list_two_elements:
"⟦y ∈ set l; x ∈ set l; length l = Suc 0; y ≠ x⟧ ⟹ False"
by (induct l) auto
lemma is_monom_vars_monom_var:
assumes "is_monom l"
shows "vars l = {monom_var l}"
proof-
have "⋀x. ⟦is_monom l; x ∈ vars l⟧ ⟹ monom_var l = x"
proof-
fix x
assume "is_monom l" "x ∈ vars l"
then have "x ∈ set (vars_list l)"
using finite_vars
by (auto simp add: vars_list_def vars_def)
show "monom_var l = x"
proof(rule ccontr)
assume "monom_var l ≠ x"
then have "∃y. monom_var l = y ∧ y ≠ x"
by simp
then obtain y where "monom_var l = y" "y ≠ x"
by auto
then have "Rep_linear_poly l y ≠ 0"
using monom_var_in_vars ‹is_monom l›
by (auto simp add: vars_def)
then have "y ∈ set (vars_list l)"
using finite_vars
by (auto simp add: vars_def vars_list_def)
then show False
using ‹x ∈ set (vars_list l)› ‹is_monom l› ‹y ≠ x›
using list_two_elements
by (simp add: is_monom_def)
qed
qed
then show "vars l = {monom_var l}"
using assms
by (auto simp add: monom_var_in_vars)
qed
lemma monom_valuate:
assumes "is_monom m"
shows "m⦃v⦄ = (monom_coeff m) *R v (monom_var m)"
using assms
using is_monom_vars_monom_var
by (simp add: vars_def coeff_def monom_coeff_def valuate_def)
lemma coeff_zero_simp [simp]:
"coeff 0 v = 0"
using zero_coeff_zero by blast
lemma poly_eq_iff: "p = q ⟷ (∀ v. coeff p v = coeff q v)"
by transfer auto
lemma poly_eqI:
assumes "⋀v. coeff p v = coeff q v"
shows "p = q"
using assms poly_eq_iff by simp
lemma coeff_sum_list:
assumes "distinct xs"
shows "coeff (∑x←xs. f x *R lp_monom 1 x) v = (if v ∈ set xs then f v else 0)"
using assms by (induction xs) auto
lemma linear_poly_sum:
"p ⦃ v ⦄ = (∑x∈vars p. coeff p x *R v x)"
by transfer simp
lemma all_valuate_zero: assumes "⋀(v::'a::lrv valuation). p ⦃v⦄ = 0"
shows "p = 0"
using all_val assms by blast
lemma linear_poly_eqI: assumes "⋀(v::'a::lrv valuation). (p ⦃v⦄) = (q ⦃v⦄)"
shows "p = q"
using assms
proof -
have "(p - q) ⦃ v ⦄ = 0" for v::"'a::lrv valuation"
using assms by (subst valuate_minus) auto
then have "p - q = 0"
by (intro all_valuate_zero) auto
then show ?thesis
by simp
qed
lemma monom_poly_assemble:
assumes "is_monom p"
shows "monom_coeff p *R lp_monom 1 (monom_var p) = p"
by (simp add: assms linear_poly_eqI monom_valuate valuate_scaleRat)
lemma coeff_sum: "coeff (sum (f :: _ ⇒ linear_poly) is) x = sum (λ i. coeff (f i) x) is"
by (induct "is" rule: infinite_finite_induct, auto)
end