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 "p1"} and p2 is
defined by @{term "λ v. p1 v + p2 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
  "pv " == "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 ( lpv )"
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: "((xA. f x)  v ) = (xA. ((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. yx  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 "mv = (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 (xxs. 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  = (xvars 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