Theory Degree

theory Degree
  imports Notation
begin

subsection ‹Degree of a given variable›

lemma degree_Const [simp]: "degree (Const x) v = 0"
  unfolding degree_def Const_def Const⇩0_def
  by (simp add: MPoly_inverse)

lemma degree_Var [simp]:
  "degree ((Var v):: 'a::comm_semiring_1 mpoly) v' = (if v = v' then 1 else 0)"
  unfolding degree_def Var_def Var⇩0_def
  by (simp add: MPoly_inverse lookup_single)

lemma degree_neg:
  fixes P :: "'a::ab_group_add mpoly"
  shows "degree (- P) = degree P"
  unfolding degree.rep_eq uminus_mpoly.rep_eq keys.rep_eq
  by auto

lemma degree_add:
  fixes P Q :: "'a::ab_group_add mpoly"
  shows "degree (P + Q) v ≤ max (degree P v) (degree Q v)"
proof - 
  { fix m assume "m ∈ keys (mapping_of (P + Q))" 
    hence "m ∈ keys (mapping_of P) ∨ m ∈ keys (mapping_of Q)"
      by (metis add.right_neutral coeff_add coeff_keys)
    moreover have "m ∈ keys (mapping_of P) ⟹ lookup m v ≤ degree P v"
      by (simp add: degree_def)
    moreover have "m ∈ keys (mapping_of Q) ⟹ lookup m v ≤ degree Q v"
      by (simp add: degree_def)
    ultimately have "lookup m v ≤ max (degree P v) (degree Q v)"
      by auto }
  thus ?thesis by (simp add: degree_def)
qed

lemma degree_add':
  fixes P Q :: "'a::ab_group_add mpoly"
  shows "degree (P + Q) v ≤ degree P v + degree Q v"
  using degree_add
  by (metis max_def trans_le_add1 trans_le_add2)

lemma degree_add_different_degree:
  fixes P :: "'a::ab_group_add mpoly"
  assumes "degree P v ≠ degree Q v"
  shows "degree (P + Q) v = max (degree P v) (degree Q v)"
proof -
  have 0: "Max (insert 0 ((λm. lookup m v) ` keys (mapping_of P))) ≠
           Max (insert 0 ((λm. lookup m v) ` keys (mapping_of Q)))"
    using assms unfolding degree.rep_eq .
  have "Max (insert 0 ((λm. lookup m v) ` keys (mapping_of P + mapping_of Q))) =
        max (Max (insert 0 ((λm. lookup m v) ` keys (mapping_of P))))
            (Max (insert 0 ((λm. lookup m v) ` keys (mapping_of Q))))"
  proof cases
    assume 1: "(λm. lookup m v) ` keys (mapping_of P) = {}"
    show ?thesis
    proof cases
      assume 2: "(λm. lookup m v) ` keys (mapping_of Q) = {}"
      show ?thesis using 0 1 assms unfolding degree.rep_eq by simp
    next
      assume 3: "(λm. lookup m v) ` keys (mapping_of Q) ≠ {}"
      have "(λm. lookup m v) ` keys (mapping_of P + mapping_of Q) =
            (λm. lookup m v) ` keys (mapping_of Q)"
        using 1 3 by auto
      thus ?thesis using 1 by auto
    qed
  next
    assume 4: "(λm. lookup m v) ` keys (mapping_of P) ≠ {}"
    show ?thesis
    proof cases
      assume 5: "(λm. lookup m v) ` keys (mapping_of Q) = {}"
      have "(λm. lookup m v) ` keys (mapping_of P + mapping_of Q) =
            (λm. lookup m v) ` keys (mapping_of P)"
        using 4 5 by auto
      thus ?thesis using 5 by auto
    next
      assume 6: "(λm. lookup m v) ` keys (mapping_of Q) ≠ {}"
      have 7: "(λm. lookup m v) ` keys (mapping_of P + mapping_of Q) ≠ {}"
        using 0 eq_neg_iff_add_eq_0 by force
      obtain a where 8: "lookup a v = (MAX m∈keys (mapping_of P). lookup m v)"
                        "lookup (mapping_of P) a ≠ 0"
                        "⋀m. lookup (mapping_of P) m ≠ 0 ⟹ lookup m v ≤ lookup a v"
        using 4
        by (smt (verit, best) Max_ge Max_in finite_imageI finite_keys image_iff in_keys_iff)
      obtain b where 9: "lookup b v = (MAX m∈keys (mapping_of Q). lookup m v)"
                        "lookup (mapping_of Q) b ≠ 0"
                        "⋀m. lookup (mapping_of Q) m ≠ 0 ⟹ lookup m v ≤ lookup b v"
        using 6
        by (smt (verit, best) Max_ge Max_in finite_imageI finite_keys image_iff in_keys_iff)
      obtain c where 10: "lookup c v = (MAX m∈keys (mapping_of P + mapping_of Q). lookup m v)"
                         "lookup (mapping_of P) c + lookup (mapping_of Q) c ≠ 0"
                         "⋀m. lookup (mapping_of P) m + lookup (mapping_of Q) m ≠ 0 
                          ⟹ lookup m v ≤ lookup c v"
        using 7
        by (smt (verit, del_insts) Max_ge Max_in finite_imageI finite_keys image_iff 
            lookup_not_eq_zero_eq_in_keys plus_poly_mapping.rep_eq)
      have 11: "lookup a v ≠ lookup b v" unfolding 8(1) 9(1) using 0 4 6 by simp
      have "lookup c v = max (lookup a v) (lookup b v)"
        using 8 9 10 11
        by (smt (verit, del_insts) add_cancel_right_right max.bounded_iff order_class.order_eq_iff)
      hence "(MAX m∈keys (mapping_of P + mapping_of Q). lookup m v) =
             max (MAX m∈keys (mapping_of P). lookup m v)
                 (MAX m∈keys (mapping_of Q). lookup m v)"
        unfolding 8(1) 9(1) 10(1) .
      thus ?thesis using 4 6 7 by auto
    qed
  qed
  thus ?thesis unfolding degree.rep_eq plus_mpoly.rep_eq plus_poly_mapping.rep_eq .
qed

lemma degree_diff:
  fixes P Q :: "'a::ab_group_add mpoly"
  shows "degree (P - Q) v ≤ max (degree P v) (degree Q v)"
  unfolding diff_conv_add_uminus[of P] degree_neg[of Q, symmetric]
  by (rule degree_add)

lemma degree_diff':
  fixes P Q :: "'a::ab_group_add mpoly"
  shows "degree (P - Q) v ≤ degree P v + degree Q v"
  unfolding diff_conv_add_uminus[of P] degree_neg[of Q, symmetric]
  by (rule degree_add')

lemma degree_diff_different_degree:
  fixes P :: "'a::ab_group_add mpoly"
  assumes "degree P v ≠ degree Q v"
  shows "degree (P - Q) v = max (degree P v) (degree Q v)"
  unfolding diff_conv_add_uminus[of P] degree_neg[of Q, symmetric]
  apply (rule degree_add_different_degree)
  unfolding degree_neg apply (rule assms)
  done

lemma degree_sum:
  fixes P :: "'a ⇒ 'b::ab_group_add mpoly"
  assumes S_fin: "finite S"
  shows "degree (sum P S) v ≤ Max (insert 0 ((λi. degree (P i) v) ` S))"
proof (induct rule:finite_induct[OF S_fin])
  case 1 show ?case by simp
next 
  case (2 x S)
  have "degree (sum P (insert x S)) v = degree (sum P S + P x) v"
    by (simp add: "2.hyps" add.commute)
  also have "... ≤ max (degree (sum P S) v) (degree (P x) v)"
    using degree_add by auto
  also have "... ≤ max (Max (insert 0 ((λi. degree (P i) v) ` S))) (degree (P x) v)"
    using "2.hyps" by auto
  also have "... = Max (insert (degree (P x) v) (insert 0 ((λi. degree (P i) v) ` S)))"
    by (simp add: "2.hyps")
  also have "... = Max (insert 0 ((λi. degree (P i) v) ` (insert x S)))"
    by (simp add: insert_commute)
  finally show ?case .
qed

lemma degree_mult: "degree (P * Q) v ≤ degree P v + degree Q v"
proof -
  have "m ∈ keys (mapping_of (P * Q)) ⟹
        lookup m v ≤ degree P v + degree Q v" for m
  proof -
    assume "m ∈ keys (mapping_of (P * Q))"
    hence "m ∈ keys (mapping_of P * mapping_of Q)"
      by (simp add: times_mpoly.rep_eq)
    hence "m ∈ {a + b | a b. a ∈ keys (mapping_of P) ∧ b ∈ keys (mapping_of Q)}"
      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
    from a_key have a_bound: "lookup a v ≤ degree P v"
      unfolding degree.rep_eq by simp
    from b_key have b_bound: "lookup b v ≤ degree Q v"
      unfolding degree.rep_eq by simp
    have "lookup m v = lookup a v + lookup b v"
      unfolding m_def lookup_add by simp
    thus "lookup m v ≤ degree P v + degree Q v"
      using a_bound b_bound by simp
  qed
  thus ?thesis unfolding degree.rep_eq by simp
qed

lemma degree_mult_non_zero:
  fixes P Q :: "'a::idom mpoly"
  assumes "P ≠ 0" "Q ≠ 0"
  shows "degree (P * Q) v = degree P v + degree Q v"
proof (rule antisym)
  show "degree (P * Q) v ≤ degree P v + degree Q v" by (rule degree_mult)
next
  define a where "a = Max ((λm. lookup m v) ` keys (mapping_of P))"
  define b where "b = Max ((λm. lookup m v) ` keys (mapping_of Q))"
  define c where "c = Max ((λm. lookup m v) ` keys (mapping_of (P * Q)))"
  define p where "p = Max {m ∈ keys (mapping_of P). lookup m v = a}"
  define q where "q = Max {m ∈ keys (mapping_of Q). lookup m v = b}"
  define r where "r = Max {m ∈ keys (mapping_of (P * Q)). lookup m v = c}"
  have 0: "P * Q ≠ 0" using assms by auto
  have 1: "keys (mapping_of P) ≠ {}"
          "keys (mapping_of Q) ≠ {}"
          "keys (mapping_of (P * Q)) ≠ {}"
    using assms 0 mapping_of_inject zero_mpoly.rep_eq
    by (metis keys_eq_empty)+
  have 2: "a ∈ (λm. lookup m v) ` keys (mapping_of P)"
          "b ∈ (λm. lookup m v) ` keys (mapping_of Q)"
          "c ∈ (λm. lookup m v) ` keys (mapping_of (P * Q))"
    unfolding a_def b_def c_def
    using 1 Max_in
    by simp+
  have 3: "p ∈ {m ∈ keys (mapping_of P). lookup m v = a}"
          "q ∈ {m ∈ keys (mapping_of Q). lookup m v = b}"
          "r ∈ {m ∈ keys (mapping_of (P * Q)). lookup m v = c}"
    unfolding p_def q_def r_def
    using 2 Max_in[of "{m ∈ keys (mapping_of _). lookup m v = _}"]
    by auto
  have 4: "⋀m. m ∈ keys (mapping_of P) ⟹ lookup m v ≤ a"
          "⋀m. m ∈ keys (mapping_of Q) ⟹ lookup m v ≤ b"
          "⋀m. m ∈ keys (mapping_of (P * Q)) ⟹ lookup m v ≤ c"
    unfolding a_def b_def c_def
    by auto
  have 5: "⋀m. m ∈ keys (mapping_of P) ⟹ lookup m v = a ⟹ m ≤ p"
          "⋀m. m ∈ keys (mapping_of Q) ⟹ lookup m v = b ⟹ m ≤ q"
          "⋀m. m ∈ keys (mapping_of (P * Q)) ⟹ lookup m v = c ⟹ m ≤ r"
    unfolding p_def q_def r_def
    by auto
  have "p' + q' = p + q ⟹
        lookup (mapping_of P) p' ≠ 0 ⟹
        lookup (mapping_of Q) q' ≠ 0 ⟹
        p' = p ∧ q' = q" for p' q'
  proof -
    assume 6: "p' + q' = p + q"
    assume 7: "lookup (mapping_of P) p' ≠ 0" "lookup (mapping_of Q) q' ≠ 0"
    have 8: "lookup p' v ≤ lookup p v" "lookup q' v ≤ lookup q v"
      using 3 4 7 unfolding in_keys_iff by auto
    have "lookup p' v + lookup q' v = lookup p v + lookup q v"
      using 6
      by (metis lookup_add)
    hence "lookup p' v = lookup p v ∧ lookup q' v = lookup q v"
      using 8
      by linarith
    hence "p' ≤ p" "q' ≤ q"
      using 3 5 7 unfolding in_keys_iff by blast+
    thus "p' = p ∧ q' = q"
      using 6
      by (metis add.commute add_le_cancel_left antisym)
  qed
  hence 9: "(p + q = p' + q' ∧
             lookup (mapping_of P) p' ≠ 0 ∧
             lookup (mapping_of Q) q' ≠ 0) ⟷
            (p', q') = (p, q)" for p' q'
    using 3 by auto
  have "lookup (mapping_of (P * Q)) (p + q) =
        (∑(p', q'). lookup (mapping_of P) p' * lookup (mapping_of Q) q' when p + q = p' + q')"
    unfolding times_mpoly.rep_eq times_poly_mapping.rep_eq
    by (rule prod_fun_unfold_prod; simp)
  also have "... = (∑(p', q'). lookup (mapping_of P) p' * lookup (mapping_of Q) q' 
              when p + q = p' + q' ∧ lookup (mapping_of P) p' ≠ 0 ∧ lookup (mapping_of Q) q' ≠ 0)"
    apply (rule Sum_any.cong)
    unfolding when_def apply auto
    done
  also have "... = Sum_any (λa. (case a of (p', q') 
                    ⇒ lookup (mapping_of P) p' * lookup (mapping_of Q) q') when a = (p, q))"
    unfolding 9
    by (rule Sum_any.cong; auto)
  also have "... = lookup (mapping_of P) p * lookup (mapping_of Q) q"
    unfolding Sum_any_when_equal
    by auto
  also have "... ≠ 0"
    using 3 by auto
  finally have 10: "lookup (mapping_of (P * Q)) (p + q) ≠ 0" .
  have "a + b = lookup (p + q) v"
    using 3
    unfolding plus_poly_mapping.rep_eq by simp
  also have "... ≤ c"
    by (rule 4(3)[unfolded in_keys_iff]; rule 10)
  finally show "degree P v + degree Q v ≤ degree (P * Q) v"
    unfolding a_def b_def c_def degree.rep_eq
    using 1
    by simp
qed

lemma degree_pow: "degree (P ^ n) v ≤ n * degree P v"
proof (induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  have "degree (P ^ Suc n) v ≤ degree P v + degree (P ^ n) v"
    using degree_mult by auto
  also have "... ≤ degree P v + n * degree P v"
    using Suc by auto
  also have "... = Suc n * degree P v"
    by auto
  finally show ?case .
qed

lemma degree_pow_positive:
  fixes P :: "'a::idom mpoly"
  assumes "n > 0"
  shows "degree (P ^ n) v = n * degree P v"
proof (induction rule: nat_induct_non_zero[OF assms])
  show "degree (P ^ 1) v = 1 * degree P v" by simp
next
  fix m :: nat
  assume 0: "m > 0"
  assume 1: "degree (P ^ m) v = m * degree P v"
  show "degree (P ^ Suc m) v = Suc m * degree P v"
  proof cases
    assume 2: "P = 0"
    show ?thesis unfolding 2 by simp
  next
    assume 3: "P ≠ 0"
    show ?thesis
      unfolding power_Suc2
      apply (subst degree_mult_non_zero)
      subgoal using 0 3 pow_positive by blast
      subgoal using 3 .
      subgoal using 1 by simp
      done
  qed
qed

lemma degree_prod:
  assumes S_fin: "finite S"
  shows "degree (prod P S) v ≤ sum (λi. degree (P i) v) S"
proof (induct rule:finite_induct[OF S_fin])
  case 1 show ?case by simp
next
  case (2 x S)
  have "degree (prod P (insert x S)) v = degree (prod P S * P x) v"
    by (simp add: "2.hyps" mult.commute)
  also have "... ≤ (degree (prod P S) v) + (degree (P x) v)"
    using degree_mult by auto
  also have "... ≤ (sum (λi. degree (P i) v) S) + (degree (P x) v)"
    using "2.hyps" by auto
  also have "... = sum (λi. degree (P i) v) (insert x S)"
    by (simp add: "2.hyps")
  finally show ?case .
qed


end