Theory Abstract_Linear_Poly

(* Authors: F. Maric, M. Spasic, R. Thiemann *)
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›
  (* TODO: change rat to arbitrary ring *)

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"    ("_ ⦃ _ ⦄")
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