Theory Linear_Polynomial

section ‹Linear Polynomials›

subsection ‹An Abstract Type for Multivariate Linear Polynomials›

theory Linear_Polynomial
  imports 
    Main
begin

typedef (overloaded) ('a :: zero,'v) lpoly = "{ c :: 'v option ⇒ 'a. finite {v. c v ≠ 0}}" 
  by (intro exI[of _ "λ _. 0"], auto)

setup_lifting type_definition_lpoly 

instantiation lpoly :: (ab_group_add,type)ab_group_add
begin

lift_definition uminus_lpoly :: "('a, 'b) lpoly ⇒ ('a, 'b) lpoly" is "λ c x.  - c x" by auto

lift_definition minus_lpoly :: "('a, 'b) lpoly ⇒ ('a, 'b) lpoly ⇒ ('a, 'b) lpoly" is "λ c1 c2 x.  c1 x - c2 x"
proof goal_cases
  case (1 c1 c2)
  have "{v. c1 v - c2 v ≠ 0} ⊆ {v. c1 v ≠ 0} ∪ {v. c2 v ≠ 0}" by auto
  from finite_subset[OF this] 1 show ?case by auto
qed

lift_definition plus_lpoly :: "('a, 'b) lpoly ⇒ ('a, 'b) lpoly ⇒ ('a, 'b) lpoly" is "λ c1 c2 x.  c1 x + c2 x"
proof goal_cases
  case (1 c1 c2)
  have "{v. c1 v + c2 v ≠ 0} ⊆ {v. c1 v ≠ 0} ∪ {v. c2 v ≠ 0}" by auto
  from finite_subset[OF this] 1 show ?case by auto
qed 

lift_definition zero_lpoly :: "('a, 'b) lpoly" is "λ c. 0" by auto

instance by (intro_classes; transfer, auto simp: ac_simps)
end
 
lift_definition var_l :: "'v ⇒ ('a :: {comm_monoid_mult,zero_neq_one}, 'v) lpoly" is "λ x. (λ c. 0)(Some x := 1)" by auto
lift_definition constant_l :: "('a :: zero, 'v) lpoly ⇒ 'a" is "λ c. c None" .
lift_definition coeff_l :: "('a :: zero, 'v) lpoly ⇒ 'v ⇒ 'a" is "λ c x. c (Some x)" . 
lift_definition vars_l :: "('a :: zero, 'v) lpoly ⇒ 'v set" is "λ c. { x. c (Some x) ≠ 0}" .

lemma finite_vars_l[simp,intro]: "finite (vars_l p)" 
proof (transfer, goal_cases)
  case (1 p)
  show ?case by (rule finite_subset[OF _ finite_imageI[OF 1, of the]], force)
qed

type_synonym ('a,'v) assign = "'v ⇒ 'a" 

lemma vars_l_var[simp]: "vars_l (var_l x) = {x}" by transfer auto

lemma vars_l_plus: "vars_l (p1 + p2) ⊆ vars_l p1 ∪ vars_l p2" 
  by (transfer, auto)

lemma vars_l_minus: "vars_l (p1 - p2) ⊆ vars_l p1 ∪ vars_l p2" 
  by (transfer, auto)

lemma vars_l_uminus[simp]: "vars_l (- p) = vars_l p" 
  by (transfer, auto)

lemma vars_l_zero[simp]: "vars_l 0 = {}" 
  by (transfer, auto)

definition eval_l :: "('a :: comm_ring, 'v) assign ⇒ ('a,'v) lpoly ⇒ 'a" where
  "eval_l α p = constant_l p + sum (λ x. coeff_l p x * α x) (vars_l p)" 

lemma eval_l_mono: assumes "finite V" "vars_l p ⊆ V" 
  shows "eval_l α p = constant_l p + sum (λ x. coeff_l p x * α x) V" 
proof -
  define W where "W = V - vars_l p"
  have [simp]: "(∑x∈W. coeff_l p x * α x) = 0" 
    by (rule sum.neutral, unfold W_def, transfer, auto)
  have V: "V = W ∪ vars_l p" "W ∩ vars_l p = {}" using assms unfolding W_def by auto
  show ?thesis unfolding eval_l_def using assms unfolding V 
    by (subst sum.union_disjoint[OF _ _ V(2)], auto)
qed

lemma eval_l_cong: assumes "⋀ x. x ∈ vars_l p ⟹ α x = β x" 
  shows "eval_l α p = eval_l β p" 
  unfolding eval_l_mono[OF finite_vars_l subset_refl]
  by (intro arg_cong[of _ _ "λ x. _ + x"] sum.cong refl, insert assms, auto)
 
lemma eval_l_0[simp]: "eval_l α 0 = 0" unfolding eval_l_def
  by (transfer, auto)

lemma eval_l_plus[simp]: "eval_l α (p1 + p2) = eval_l α p1 + eval_l α p2" 
proof -
  have fin: "finite (vars_l p1 ∪ vars_l p2)" by auto
  show ?thesis
    apply (subst (1 2 3) eval_l_mono[OF fin])
    subgoal by auto
    subgoal by auto
    subgoal by (rule vars_l_plus)  
    subgoal by (transfer, auto simp: sum.distrib algebra_simps)
    done
qed

lemma eval_l_minus[simp]: "eval_l α (p1 - p2) = eval_l α p1 - eval_l α p2" 
proof -
  have fin: "finite (vars_l p1 ∪ vars_l p2)" by auto
  show ?thesis
    apply (subst (1 2 3) eval_l_mono[OF fin])
    subgoal by auto
    subgoal by auto
    subgoal by (rule vars_l_minus)  
    subgoal by (transfer, auto simp: sum_subtractf algebra_simps)
    done
qed

lemma eval_l_uminus[simp]: "eval_l α (- p) = - eval_l α p" 
  unfolding eval_l_def
  by (transfer, auto simp: sum_negf)

lemma eval_l_var[simp]: "eval_l α (var_l x) = α x" 
  apply (subst eval_l_mono[of "{x}"])
    apply force
   apply force
  by (transfer, auto)

(* substitute x by p within q *)
lift_definition substitute_l :: "'v ⇒ ('a :: comm_ring, 'v) lpoly ⇒ ('a,'v) lpoly ⇒ ('a,'v) lpoly" is
  "λ x p q y. (q(Some x := 0)) y + q (Some x) * p y"
proof goal_cases
  case (1 x p1 p2)
  show ?case
    apply (rule finite_subset[of _ "{v. p1 v ≠ 0} ∪ {v. p2 v ≠ 0}"])
    using 1 by auto
qed

lemma vars_substitute_l: "vars_l (substitute_l x p q) ⊆ vars_l p ∪ (vars_l q - {x})" 
  by (transfer, auto)

lemma substitute_l_id: "x ∉ vars_l q ⟹ substitute_l x p q = q" 
  by transfer auto


lemma eval_substitute_l: "eval_l α (substitute_l x p q) = eval_l (α( x := eval_l α p)) q" 
proof -
  have fin: "finite (insert x (vars_l p ∪ vars_l q))" 
      and fin2: "finite (vars_l p ∪ vars_l q)" by auto
  define V where "V = vars_l p ∪ vars_l q - {x}" 
  have V: "finite V" "x ∉ V" unfolding V_def by auto
  show ?thesis
    apply (subst (1 2 3) eval_l_mono[OF fin])
    subgoal by auto
    subgoal by auto
    subgoal using vars_substitute_l[of x p q] by auto
    apply (unfold sum.insert_remove[OF fin2])
    apply (unfold V_def[symmetric])
    using V
    apply (transfer)
    apply (simp add: algebra_simps sum.distrib sum_distrib_left)
    apply (intro sum.cong)
     apply (auto simp: ac_simps)
    done
qed

lift_definition fun_of_lpoly :: "('a :: zero,'v) lpoly ⇒ 'v option ⇒ 'a" is "λ x. x" .

lift_definition smult_l :: "'a :: comm_ring ⇒ ('a,'v)lpoly ⇒ ('a,'v)lpoly" is
  "λ y c z. y * c z" 
proof (goal_cases)
  case 1
  show ?case by (rule finite_subset[OF _ 1], auto)
qed

lemma coeff_smult_l[simp]: "coeff_l (smult_l c p) x = c * coeff_l p x" 
  by transfer auto

lemma constant_smult_l[simp]: "constant_l (smult_l c p) = c * constant_l p" 
  by transfer auto

lemma eval_smult_l[simp]: "eval_l α (smult_l c p) = c * eval_l α p" 
  apply (subst (1 2) eval_l_mono[of "vars_l p"])
  subgoal by simp
  subgoal by simp
  subgoal by transfer auto
  unfolding eval_l_def coeff_smult_l
  by (auto simp: algebra_simps sum_distrib_left)

lift_definition const_l :: "'a :: zero ⇒ ('a,'v) lpoly" is "λ c. (λ z. 0)(None := c)" 
  by auto

lemma eval_l_const_l_constant: "eval_l α (const_l (constant_l p)) = constant_l p" 
  unfolding eval_l_def
  by transfer auto

definition substitute_all_l :: "('v ⇒ ('a,'w) lpoly) ⇒ ('a :: comm_ring, 'v) lpoly ⇒ ('a, 'w) lpoly" where
  "substitute_all_l σ p = (const_l (constant_l p) + sum (λ x. smult_l (coeff_l p x) (σ x)) (vars_l p))" 

lemma eval_substitute_all_l: "eval_l α (substitute_all_l σ p) = eval_l (λ x. eval_l α (σ x)) p" 
proof -
  define xs where "xs = vars_l p" 
  have fin: "finite xs" unfolding xs_def by auto
  show ?thesis
    unfolding substitute_all_l_def
    unfolding eval_l_mono[OF finite_vars_l subset_refl, of _ p]
    unfolding eval_l_plus eval_l_const_l_constant
    unfolding xs_def[symmetric] using fin
  proof (intro arg_cong[of _ _ "λ x. _ + x"], induct xs rule: finite_induct)
    case *: (insert x xs)
    note IH = *(3)[OF *(1)]
    note sum = sum.insert[OF *(1-2)]
    show ?case unfolding sum eval_l_plus IH eval_smult_l by simp
  qed simp
qed

lift_definition sdiv_l :: "(int, 'v) lpoly ⇒ int ⇒ (int, 'v) lpoly" is "λ c q x. c x div q" 
proof (goal_cases)
  case 1
  show ?case by (rule finite_subset[OF _ 1], auto)
qed

definition "vars_l_list p = sorted_list_of_set (vars_l p)" 

lemma vars_l_list[simp]: "set (vars_l_list p) = vars_l p" 
  unfolding vars_l_list_def by simp

definition min_var :: "('a :: {linorder, ordered_ab_group_add_abs}, 'v :: linorder) lpoly ⇒ 'v" where
  "min_var p = (let 
     xcs = map (λ x. (x,coeff_l p x)) (vars_l_list p);
     axcs = map (map_prod id abs) xcs;
     m = min_list (map snd axcs)
   in (case filter (λ xa. snd xa = m) axcs of
     (x,a) # _ ⇒ x))" 

lemma min_var: "vars_l p ≠ {} ⟹ coeff_l p (min_var p) ≠ 0" 
    "x ∈ vars_l p ⟹ abs (coeff_l p (min_var p)) ≤ abs (coeff_l p x)"
proof -
  let ?m = "min_var p" 
  define xcs where "xcs = map (λ x. (x,coeff_l p x)) (vars_l_list p)" 
  define axcs where "axcs = map (map_prod id abs) xcs" 
  define m where "m = min_list (map snd axcs)" 
  define fxs where "fxs = filter (λ xa. snd xa = m) axcs" 
  {
    fix x
    assume x: "x ∈ vars_l p" 
    let ?c = "coeff_l p x" 
    from x have cx: "?c ≠ 0" by transfer auto
    from x have "(x, ?c) ∈ set xcs" unfolding xcs_def by force
    hence ax: "(x, abs ?c) ∈ set axcs" unfolding axcs_def by force
    hence "map snd axcs ≠ []" "abs ?c ∈ set (map snd axcs)" by force+
    with min_list_Min[OF this(1), folded m_def] 
    have m: "m = Min (set (map snd axcs))" "m ∈ set (map snd axcs)" "m ≤ abs ?c" by auto
    from m(2) have "m ∈ snd ` set fxs" unfolding fxs_def by force
    then obtain y m' xs where fxs: "fxs = ((y,m') # xs)" 
      by (cases fxs, auto simp: fxs_def)
    hence "(y,m') ∈ set fxs" by auto
    from this[unfolded fxs_def] have m': "m' = m" by auto
    with fxs have fxs: "fxs = ((y,m) # xs)" by auto
    have m': "?m = y" 
      unfolding min_var_def Let_def xcs_def[symmetric]
      unfolding axcs_def[symmetric]
      unfolding m_def[symmetric]
      unfolding fxs_def[symmetric]
      unfolding fxs by simp
    from fxs have "(y,m) ∈ set axcs" unfolding fxs_def 
      by (metis Cons_eq_filter_iff in_set_conv_decomp)
    then obtain c where "(y,c) ∈ set xcs" and mc: "m = abs c" unfolding axcs_def by auto
    hence c: "c = coeff_l p y" and y: "y ∈ vars_l p" unfolding xcs_def by auto
    hence c0: "c ≠ 0" by transfer auto
    show "abs (coeff_l p ?m) ≤ abs (coeff_l p x)" 
      unfolding m' using m(3) unfolding c mc .
    have "abs (coeff_l p ?m) ≠ 0" using c0 unfolding c m' by auto
  }
  thus "vars_l p ≠ {} ⟹ coeff_l p (min_var p) ≠ 0" by auto
qed

definition gcd_coeffs_l :: "('a :: Gcd, 'v)lpoly ⇒ 'a" where
  "gcd_coeffs_l p = Gcd (coeff_l p ` vars_l p)"

lift_definition change_const :: "'a :: zero ⇒ ('a,'v)lpoly ⇒ ('a,'v)lpoly" is "λ x c. c(None := x)" 
proof goal_cases
  case (1 x c)
  hence f: "finite ((insert None) {v. c v ≠ 0})" by auto
  show ?case
    by (rule finite_subset[OF _ f], auto)
qed

lemma lpoly_fun_of_eqI: assumes "⋀ x. fun_of_lpoly p x = fun_of_lpoly q x" 
  shows "p = q" 
  using assms by transfer auto

lift_definition reorder_nontriv_var :: "'v ⇒ (int,'v) lpoly ⇒ 'v ⇒ (int,'v) lpoly" is
  "λ x c y. (λ z. c z div c (Some x))(Some x := 1, Some y := -1)"
proof (goal_cases)
  case (1 x c y)
  from 1 have fin: "finite (insert (Some y) (insert (Some x) ({v. c v ≠ 0})))" by auto
  show ?case by (rule finite_subset[OF _ fin], auto)
qed

lemma coeff_l_reorder_nontriv_var: "coeff_l (reorder_nontriv_var x p y)
  = (λ z. coeff_l p z div coeff_l p x)(x := 1, y := -1)" 
  by (transfer, auto simp: Let_def)

lemma vars_reorder_non_triv: "vars_l (reorder_nontriv_var x p y) ⊆ insert x (insert y (vars_l p))"
  by (transfer, auto simp: Let_def)


end