Theory Total_Degree_Env

theory Total_Degree_Env
  imports "Total_Degree" "Substitutions"
begin

section ‹Bottom-up total\_degree under a substitution-degree environment›

lift_definition total_degree_env
  :: "(nat ⇒ nat) ⇒ 'a::zero_neq_one mpoly ⇒ nat"
is "λenv p. Max (insert 0
     ((λm. sum (λi. env i * lookup m i) (keys m)) `
            (keys p)))" .

text ‹
  @{term‹total_degree_env env p›} walks over the monomial representation of p,
  and whenever it sees @{term‹Var i^m›}, it contributes @{term‹m * env i›} instead of m.
›

lemma total_degree_env_id:
  "total_degree_env (λ_. 1) p = total_degree p"
  by transfer simp

lemma total_degree_env_zero[simp]: "total_degree_env f 0 = 0"
  by (simp add: total_degree_env.rep_eq zero_mpoly.rep_eq)

lemma total_degree_env_one[simp]: "total_degree_env f 1 = 0"
  by (simp add: total_degree_env.rep_eq one_mpoly.rep_eq)

lemma total_degree_env_Const[simp]: "total_degree_env f (Const c) = 0"
  by (simp add: total_degree_env.rep_eq Const.rep_eq Const0_def)

lemma total_degree_env_Const_le: "total_degree_env f (Const c) ≤ 0"
  by simp

lemma total_degree_env_Var[simp]:
  "total_degree_env f (Var i) = f i"
  by (simp add: total_degree_env.rep_eq Var.rep_eq Var0_def)

lemma total_degree_env_Var_le: "total_degree_env f (Var i) ≤ f i"
  by simp

lemma total_degree_env_neg: "total_degree_env f (-P) = total_degree_env f P"
  by (simp add: total_degree_env.rep_eq uminus_mpoly.rep_eq)

lemma total_degree_env_mult: "total_degree_env f (P * Q) ≤ total_degree_env f P + total_degree_env f Q"
proof -
  have "m ∈ keys (mapping_of (P * Q)) ⟹
        sum (λi. f i * lookup m i) (keys m) ≤ total_degree_env f P + total_degree_env f Q" for m
  proof -
    assume "m ∈ keys (mapping_of (P * Q))"
    hence "m ∈ {a + b | a b. a ∈ keys (mapping_of P) ∧ b ∈ keys (mapping_of Q)}"
      unfolding times_mpoly.rep_eq using keys_mult by blast
    then obtain a b where m_def: "m = a + b"
                      and a_key: "a ∈ keys (mapping_of P)"
                      and b_key: "b ∈ keys (mapping_of Q)"
      by blast
    have a_bound: "sum (λi. f i * lookup a i) (keys a) ≤ total_degree_env f P"
      unfolding total_degree_env.rep_eq
      by (rule Max_ge, simp_all add: a_key)
    have b_bound: "sum (λi. f i * lookup b i) (keys b) ≤ total_degree_env f Q"
      unfolding total_degree_env.rep_eq
      by (rule Max_ge, simp_all add: b_key)
    show "sum (λi. f i * lookup m i) (keys m) ≤ total_degree_env f P + total_degree_env f Q"
      unfolding m_def
      apply (subst setsum_keys_plus_distrib, simp_all add: algebra_simps)
      using a_bound b_bound by linarith
  qed
  thus ?thesis
    unfolding total_degree_env.rep_eq by simp
qed

lemma total_degree_env_pow: "total_degree_env f (P ^ n) ≤ n * total_degree_env f P"
  by (induction n, simp_all add: le_trans[OF total_degree_env_mult])

lemma total_degree_env_add: "total_degree_env f (P + Q) ≤ max (total_degree_env f P) (total_degree_env f Q)"
proof -
  have "m ∈ keys (mapping_of (P + Q)) ⟹
        sum (λi. f i * lookup m i) (keys m) ≤ max (total_degree_env f P) (total_degree_env f Q)" for m
  proof -
    assume "m ∈ keys (mapping_of (P + Q))"
    hence in_union: "m ∈ keys (mapping_of P) ∪ keys (mapping_of Q)"
      unfolding plus_mpoly.rep_eq using Poly_Mapping.keys_add by fastforce
    show "sum (λi. f i * lookup m i) (keys m) ≤ max (total_degree_env f P) (total_degree_env f Q)"
      unfolding total_degree_env.rep_eq
      by (metis (mono_tags, lifting) Max_ge UnE finite_imageI finite_insert finite_keys imageI
           in_union insertCI le_max_iff_disj)
  qed
  thus ?thesis unfolding total_degree_env.rep_eq by simp
qed

lemma total_degree_env_diff:
  fixes P :: "'a::{ab_group_add,zero_neq_one} mpoly"
  shows "total_degree_env f (P - Q) ≤ max (total_degree_env f P) (total_degree_env f Q)"
  unfolding diff_conv_add_uminus total_degree_env_neg[of f Q, symmetric]
  by (rule total_degree_env_add)

lemma total_degree_env_sum:
  fixes P :: "'a ⇒ 'b::{ab_group_add,zero_neq_one} mpoly"
  assumes S_fin: "finite S"
  shows "total_degree_env ctxt (sum P S) ≤ Max (insert 0 ((λi. total_degree_env ctxt (P i)) ` S))"
  apply (induct rule: finite_induct[OF S_fin], simp_all)
  apply (rule le_trans[OF total_degree_env_add], simp)
  using order.trans by fastforce

lemma total_degree_env_prod:
  assumes S_fin: "finite S"
  shows "total_degree_env ctxt (prod P S) ≤ sum (λi. total_degree_env ctxt (P i)) S"
  by (induct rule: finite_induct[OF S_fin], simp_all add: le_trans[OF total_degree_env_mult])

lemma total_degree_env_poly_subst_monom:
  defines "degree_monom ≡ (λm t. (lookup m) t)" (* Intentionally written this way for clarity *)
  shows "total_degree_env ctxt (poly_subst_monom f m)
         ≤ (∑t∈keys m. degree_monom m t * total_degree_env ctxt (f t))"
  unfolding poly_subst_monom_alt degree_monom_def
  by (simp add: le_trans[OF total_degree_env_prod[OF finite_keys]]
                le_trans[OF sum_mono[OF total_degree_env_pow]])

lemma total_degree_env_poly_subst_list:
  fixes p :: "'a::comm_ring_1 mpoly"
  shows "total_degree_env ctxt (poly_subst_list fs p)
   ≤ total_degree_env (λm. total_degree_env ctxt (fs !0 m)) p"
proof -
  have "total_degree_env ctxt (poly_subst_list fs p)
        = total_degree_env ctxt (∑m. Const (coeff p m) * poly_subst_monom ((!0) fs) m)"
    by (simp add: poly_subst_list_def poly_subst_def)
  also have "… ≤ Max (insert 0 
                    ((λm. total_degree_env ctxt (Const (coeff p m)
                                   * poly_subst_monom ((!0) fs) m))
                   ` (keys (mapping_of p))))"
    using 
      total_degree_env_sum
    by (metis (no_types) finite_keys poly_subst_alt poly_subst_def total_degree_env_sum)
  also have "… ≤ Max (insert 0 
                    ((λm. total_degree_env ctxt (Const (coeff p m))
                            + total_degree_env ctxt (poly_subst_monom ((!0) fs) m))
                   ` (keys (mapping_of p))))"
    using
      total_degree_env_mult
    by (smt (verit, best) Max.insert Max_function_mono Max_mono empty_not_insert finite_imageI finite_insert finite_keys image_is_empty max_nat.left_neutral subsetI)
  also have "… ≤ Max (insert 0 
                    ((λm. total_degree_env ctxt (poly_subst_monom ((!0) fs) m))
                   ` (keys (mapping_of p))))"
    by simp
  also have "… ≤ Max (insert 0 
                    ((λm. (∑i∈keys m. lookup m i * total_degree_env ctxt (fs !0 i)))
                   ` (keys (mapping_of p))))"
    using 
      total_degree_env_poly_subst_monom[of _ "λm. fs !0 m"]
    by (metis (no_types, lifting) Max.insert Max_function_mono Orderings.order_eq_iff finite_imageI finite_keys image_is_empty max_nat.left_neutral)
  finally show ?thesis by (simp add: total_degree_env_def mult.commute)
qed

lemma total_degree_poly_subst_list_env:
  fixes p :: "'a::comm_ring_1 mpoly"
  shows "total_degree (poly_subst_list fs p)
   ≤ total_degree_env (λm. total_degree (fs !0 m)) p"
  using total_degree_env_poly_subst_list total_degree_env_id
  by (metis (lifting) ext)

(* Lemmas for list of Var constructors *)

lemma total_degree_env_Var_list_bound: "total_degree_env (λ_. 1) ((map Var ls) !0 i) ≤ 1"
  by (cases "i < length ls", auto simp: nth0_def)

lemma total_degree_env_Var_list: 
  "total_degree_env (λ_. 1) ((map Var ls) !0 i) = (if i < length ls then 1 else 0)"
  by (simp add: nth0_def)

lemma total_degree_map_Var: 
  "total_degree ((map Var ls) !0 j :: 'a::comm_semiring_1 mpoly) ≤ 1"
  by (cases "j < length ls"; auto simp add: nth0_def)

lemma total_degree_map_Var_int: 
  "total_degree ((map Var ls) !0 j :: int mpoly) ≤ Suc 0"
  using total_degree_map_Var by auto

lemma total_degree_env_mono3_map_Var: 
  "(⋀i. env i ≤ 1) ⟹ total_degree_env env ((map Var ls) !0 j) ≤ 1"
  by (cases "j < length ls", simp_all add: nth0_def)

(* Substitution of a shorter list *)

lemma total_degree_env_reduce: "i < length ls
  ⟹ total_degree_env env ((ls @ xs) !0 i) = total_degree_env env (ls !0 i)"
  unfolding nth0_def by (simp add: nth_append_left)

(* Lemmas of general monotonicity properties *)

lemma total_degree_env_mono: 
  fixes P :: "int mpoly" 
  assumes "∀i≤max_vars P. env1 i ≤ env2 i"
  shows "total_degree_env env1 P ≤ total_degree_env env2 P"
  unfolding total_degree_env.rep_eq apply simp
  apply (rule)
  subgoal premises h for m
    apply (rule le_trans[of _ "(∑i∈keys m. env2 i * lookup m i)"])
    subgoal 
      apply (rule sum_mono)
      using h assms after_max_vars
      by (metis Suc_eq_plus1 in_keys_iff mult_le_mono1 not_less_eq_eq)
    subgoal 
      by (meson Max_ge finite_imageI finite_insert finite_keys h image_eqI insert_iff)
    done
  done
         
lemma total_degree_env_mono2:
  fixes P :: "int mpoly"
  shows "total_degree P ≤ rhs1 ⟹ (⋀i. i ≤ max_vars P ⟹ env i ≤ 1) ⟹ rhs1 = rhs2
  ⟹ total_degree_env env P ≤ rhs2"
  unfolding total_degree_env_id[symmetric]
  by (meson dual_order.trans total_degree_env_mono)

lemma total_degree_env_mono3_bounded: 
  fixes ls :: "int mpoly list"
  shows "j ≤ bound ⟹ (⋀i. i ≤ bound ⟹ env i ≤ 1) ⟹ max_vars (ls !0 j) ≤ bound
    ⟹ total_degree (ls !0 j) ≤ Suc 0 ⟹ total_degree_env env (ls !0 j) ≤ Suc 0"
proof -
  assume a: "j ≤ bound" and b: "⋀i. i ≤ bound ⟹ env i ≤ 1"
    and c: "max_vars (ls !0 j) ≤ bound" and d: "total_degree (ls !0 j) ≤ Suc 0"

  {
    fix a
    assume "a ∈ keys (mapping_of (ls !0 j))"
    with c have "∀i∈keys a. i ≤ bound"
      unfolding max_vars_def vars_def by simp
      (* unfolding max_vars_def vars_def
      by (meson Max_ge UN_I finite_UN finite_keys le_trans) *)
    with b have "(∑i∈keys a. env i * lookup a i) ≤ sum (lookup a) (keys a)"
      by (subst sum_mono, simp_all)
  } note e = this
  
  from d e show ?thesis
    apply (cases "j < length ls", simp_all add: nth0_def)
    unfolding total_degree_env_id[symmetric] total_degree_env.rep_eq
    using dual_order.trans by (auto, blast)
qed

lemma total_degree_env_mono3: 
  "(⋀i. env i ≤ 1) ⟹ total_degree (ls !0 j) ≤ 1
    ⟹ total_degree_env env (ls !0 j) ≤ 1"
proof -
  assume a: "(⋀i. env i ≤ 1)" and b: "total_degree (ls !0 j) ≤ 1"

  {
    fix a
    assume "a ∈ keys (mapping_of (ls ! j))"
    have "(∑i∈keys a. env i * lookup a i) ≤ sum (lookup a) (keys a)"
      apply (rule sum_mono)
      using a by simp
  } note c = this
  
  from a b show ?thesis
    apply (cases "j < length ls", simp_all add: nth0_def )
    unfolding total_degree_env_id[symmetric] total_degree_env.rep_eq
    using c dual_order.trans by (auto, blast)
qed

lemma total_degree_env_mono3': 
  "(⋀i. env i ≤ Suc 0) ⟹ total_degree (ls !0 j) ≤ Suc 0
    ⟹ total_degree_env env (ls !0 j) ≤ Suc 0"
  using total_degree_env_mono3 by auto

lemma total_degree_env_mono4: 
  "(⋀i. env i ≤ 1) ⟹ total_degree_env (λ_. 1) (ls !0 j) ≤ 1
    ⟹ total_degree_env env (ls !0 j) ≤ 1"
  unfolding total_degree_env_id by (rule total_degree_env_mono3, simp_all)

end