Theory Reduction

(* Author: Fabian Immler, Alexander Maletzky *)

section ‹Polynomial Reduction›

theory Reduction
imports "Polynomials.MPoly_Type_Class_Ordered" Confluence
begin

text ‹This theory formalizes the concept of @{emph ‹reduction›} of polynomials by polynomials.›

context ordered_term
begin

definition red_single :: "('t 0 'b::field)  ('t 0 'b)  ('t 0 'b)  'a  bool"
  where "red_single p q f t  (f  0  lookup p (t  lt f)  0 
                                q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f)"

definition red :: "('t 0 'b::field) set  ('t 0 'b)  ('t 0 'b)  bool"
  where "red F p q  (fF. t. red_single p q f t)"

definition is_red :: "('t 0 'b::field) set  ('t 0 'b)  bool"
  where "is_red F a  ¬ relation.is_final (red F) a"

subsection ‹Basic Properties of Reduction›

lemma red_setI:
  assumes "f  F" and a: "red_single p q f t"
  shows "red F p q"
  unfolding red_def
proof
  from f  F show "f  F" .
next
  from a show "t. red_single p q f t" ..
qed

lemma red_setE:
  assumes "red F p q"
  obtains f and t where "f  F" and "red_single p q f t"
proof -
  from assms obtain f where "f  F" and t: "t. red_single p q f t" unfolding red_def by auto
  from t obtain t where "red_single p q f t" ..
  from f  F this show "?thesis" ..
qed

lemma red_empty: "¬ red {} p q"
  by (rule, elim red_setE, simp)

lemma red_singleton_zero: "¬ red {0} p q"
  by (rule, elim red_setE, simp add: red_single_def)

lemma red_union: "red (F  G) p q = (red F p q  red G p q)"
proof
  assume "red (F  G) p q"
  from red_setE[OF this] obtain f t where "f  F  G" and r: "red_single p q f t" .
  from f  F  G have "f  F  f  G" by simp
  thus "red F p q  red G p q"
  proof
    assume "f  F" 
    show ?thesis by (intro disjI1, rule red_setI[OF f  F r])
  next
    assume "f  G" 
    show ?thesis by (intro disjI2, rule red_setI[OF f  G r])
  qed
next
  assume "red F p q  red G p q"
  thus "red (F  G) p q"
  proof
    assume "red F p q"
    from red_setE[OF this] obtain f t where "f  F" and "red_single p q f t" .
    show ?thesis by (intro red_setI[of f _ _ _ t], rule UnI1, rule f  F, fact)
  next
    assume "red G p q"
    from red_setE[OF this] obtain f t where "f  G" and "red_single p q f t" .
    show ?thesis by (intro red_setI[of f _ _ _ t], rule UnI2, rule f  G, fact)
  qed
qed

lemma red_unionI1:
  assumes "red F p q"
  shows "red (F  G) p q"
  unfolding red_union by (rule disjI1, fact)

lemma red_unionI2:
  assumes "red G p q"
  shows "red (F  G) p q"
  unfolding red_union by (rule disjI2, fact)

lemma red_subset:
  assumes "red G p q" and "G  F"
  shows "red F p q"
proof -
  from G  F obtain H where "F = G  H" by auto
  show ?thesis unfolding F = G  H by (rule red_unionI1, fact)
qed

lemma red_union_singleton_zero: "red (F  {0}) = red F"
  by (intro ext, simp only: red_union red_singleton_zero, simp)

lemma red_minus_singleton_zero: "red (F - {0}) = red F"
  by (metis Un_Diff_cancel2 red_union_singleton_zero)

lemma red_rtrancl_subset:
  assumes major: "(red G)** p q" and "G  F"
  shows "(red F)** p q"
  using major
proof (induct rule: rtranclp_induct)
  show "(red F)** p p" ..
next
  fix r q
  assume "red G r q" and "(red F)** p r"
  show "(red F)** p q"
  proof
    show "(red F)** p r" by fact
  next
    from red_subset[OF red G r q G  F] show "red F r q" .
  qed
qed

lemma red_singleton: "red {f} p q  (t. red_single p q f t)"
  unfolding red_def
proof
  assume "f{f}. t. red_single p q f t"
  from this obtain f0 where "f0  {f}" and a: "t. red_single p q f0 t" ..
  from f0  {f} have "f0 = f" by simp
  from this a show "t. red_single p q f t" by simp
next
  assume a: "t. red_single p q f t"
  show "f{f}. t. red_single p q f t"
  proof (rule, simp)
    from a show "t. red_single p q f t" .
  qed
qed

lemma red_single_lookup:
  assumes "red_single p q f t"
  shows "lookup q (t  lt f) = 0"
  using assms unfolding red_single_def
proof
  assume "f  0" and "lookup p (t  lt f)  0  q = p - monom_mult (lookup p (t  lt f) / lc f) t f"
  hence "lookup p (t  lt f)  0" and q_def: "q = p - monom_mult (lookup p (t  lt f) / lc f) t f"
    by auto
  from lookup_minus[of p "monom_mult (lookup p (t  lt f) / lc f) t f" "t  lt f"]
       lookup_monom_mult_plus[of "lookup p (t  lt f) / lc f" t f "lt f"]
       lc_not_0[OF f  0]
    show ?thesis unfolding q_def lc_def by simp
qed

lemma red_single_higher:
  assumes "red_single p q f t"
  shows "higher q (t  lt f) = higher p (t  lt f)"
  using assms unfolding higher_eq_iff red_single_def
proof (intro allI, intro impI)
  fix u
  assume a: "t  lt f t u"
    and "f  0  lookup p (t  lt f)  0  q = p - monom_mult (lookup p (t  lt f) / lc f) t f"
  hence "f  0"
    and "lookup p (t  lt f)  0"
    and q_def: "q = p - monom_mult (lookup p (t  lt f) / lc f) t f"
    by simp_all
  from lookup p (t  lt f)  0 lc_not_0[OF f  0] have c_not_0: "lookup p (t  lt f) / lc f  0"
    by (simp add: field_simps)
  from q_def lookup_minus[of p "monom_mult (lookup p (t  lt f) / lc f) t f"]
    have q_lookup: "s. lookup q s = lookup p s - lookup (monom_mult (lookup p (t  lt f) / lc f) t f) s"
    by simp
  from a lt_monom_mult[OF c_not_0 f  0, of t]
    have "¬ u t lt (monom_mult (lookup p (t  lt f) / lc f) t f)" by simp
  with lt_max[of "monom_mult (lookup p (t  lt f) / lc f) t f" u]
  have "lookup (monom_mult (lookup p (t  lt f) / lc f) t f) u = 0" by auto
  thus "lookup q u = lookup p u" using q_lookup[of u] by simp
qed

lemma red_single_ord:
  assumes "red_single p q f t"
  shows "q p p"
  unfolding ord_strict_higher
proof (intro exI, intro conjI)
  from red_single_lookup[OF assms] show "lookup q (t  lt f) = 0" .
next
  from assms show "lookup p (t  lt f)  0" unfolding red_single_def by simp
next
  from red_single_higher[OF assms] show "higher q (t  lt f) = higher p (t  lt f)" .
qed

lemma red_single_nonzero1:
  assumes "red_single p q f t"
  shows "p  0"
proof
  assume "p = 0"
  from this red_single_ord[OF assms] ord_p_zero_min[of q] show False by simp
qed

lemma red_single_nonzero2:
  assumes "red_single p q f t"
  shows "f  0"
proof
  assume "f = 0"
  from assms monom_mult_zero_right have "f  0" by (simp add: red_single_def)
  from this f = 0 show False by simp
qed

lemma red_single_self:
  assumes "p  0"
  shows "red_single p 0 p 0"
proof -
  from lc_not_0[OF assms] have lc: "lc p  0" .
  show ?thesis unfolding red_single_def
  proof (intro conjI)
    show "p  0" by fact
  next
    from lc show "lookup p (0  lt p)  0" unfolding lc_def by (simp add: term_simps)
  next
    from lc have "(lookup p (0  lt p)) / lc p = 1" unfolding lc_def by (simp add: term_simps)
    from this monom_mult_one_left[of p] show "0 = p - monom_mult (lookup p (0  lt p) / lc p) 0 p"
      by simp
  qed
qed

lemma red_single_trans:
  assumes "red_single p p0 f t" and "lt g addst lt f" and "g  0"
  obtains p1 where "red_single p p1 g (t + (lp f - lp g))"
proof -
  let ?s = "t + (lp f - lp g)"
  let ?p = "p - monom_mult (lookup p (?s  lt g) / lc g) ?s g"
  have "red_single p ?p g ?s" unfolding red_single_def
  proof (intro conjI)
    from assms(2) have eq: "?s  lt g = t  lt f" using adds_term_alt splus_assoc
      by (auto simp: term_simps)
    from red_single p p0 f t have "lookup p (t  lt f)  0" unfolding red_single_def by simp
    thus "lookup p (?s  lt g)  0" by (simp add: eq)
  qed (fact, fact refl)
  thus ?thesis ..
qed

lemma red_nonzero:
  assumes "red F p q"
  shows "p  0"
proof -
  from red_setE[OF assms] obtain f t where "red_single p q f t" .
  show ?thesis by (rule red_single_nonzero1, fact)
qed

lemma red_self:
  assumes "p  0"
  shows "red {p} p 0"
unfolding red_singleton
proof
  from red_single_self[OF assms] show "red_single p 0 p 0" .
qed

lemma red_ord:
  assumes "red F p q"
  shows "q p p"
proof -
  from red_setE[OF assms] obtain f and t where "red_single p q f t" .
  from red_single_ord[OF this] show "q p p" .
qed

lemma red_indI1:
  assumes "f  F" and "f  0" and "p  0" and adds: "lt f addst lt p"
  shows "red F p (p - monom_mult (lc p / lc f) (lp p - lp f) f)"
proof (intro red_setI[OF f  F])
  let ?s = "lp p - lp f"
  have c: "lookup p (?s  lt f) = lc p" unfolding lc_def
    by (metis add_diff_cancel_right' adds adds_termE pp_of_term_splus)
  show "red_single p (p - monom_mult (lc p / lc f) ?s f) f ?s" unfolding red_single_def
  proof (intro conjI, fact)
    from c lc_not_0[OF p  0] show "lookup p (?s  lt f)  0" by simp
  next
    from c show "p - monom_mult (lc p / lc f) ?s f = p - monom_mult (lookup p (?s  lt f) / lc f) ?s f"
      by simp
  qed
qed

lemma red_indI2:
  assumes "p  0" and r: "red F (tail p) q"
  shows "red F p (q + monomial (lc p) (lt p))"
proof -
  from red_setE[OF r] obtain f t where "f  F" and rs: "red_single (tail p) q f t" by auto
  from rs have "f  0" and ct: "lookup (tail p) (t  lt f)  0"
    and q: "q = tail p - monom_mult (lookup (tail p) (t  lt f) / lc f) t f"
    unfolding red_single_def by simp_all
  from ct lookup_tail[of p "t  lt f"] have "t  lt f t lt p" by (auto split: if_splits)
  hence c: "lookup (tail p) (t  lt f) = lookup p (t  lt f)" using lookup_tail[of p] by simp
  show ?thesis
  proof (intro red_setI[OF f  F])
    show "red_single p (q + Poly_Mapping.single (lt p) (lc p)) f t" unfolding red_single_def
    proof (intro conjI, fact)
      from ct c show "lookup p (t  lt f)  0" by simp
    next
      from q have "q + monomial (lc p) (lt p) =
                  (monomial (lc p) (lt p) + tail p) - monom_mult (lookup (tail p) (t  lt f) / lc f) t f"
        by simp
      also have " = p - monom_mult (lookup (tail p) (t  lt f) / lc f) t f"
        using leading_monomial_tail[of p] by auto
      finally show "q + monomial (lc p) (lt p) = p - monom_mult (lookup p (t  lt f) / lc f) t f"
        by (simp only: c)
    qed
  qed
qed

lemma red_indE:
  assumes "red F p q"
  shows "(fF. f  0  lt f addst lt p 
            (q = p - monom_mult (lc p / lc f) (lp p - lp f) f)) 
            red F (tail p) (q - monomial (lc p) (lt p))"
proof -
  from red_nonzero[OF assms] have "p  0" .
  from red_setE[OF assms] obtain f t where "f  F" and rs: "red_single p q f t" by auto
  from rs have "f  0"
    and cn0: "lookup p (t  lt f)  0"
    and q: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    unfolding red_single_def by simp_all
  show ?thesis
  proof (cases "lt p = t  lt f")
    case True
    hence "lt f addst lt p" by (simp add: term_simps)
    from True have eq1: "lp p - lp f = t" by (simp add: term_simps)
    from True have eq2: "lc p = lookup p (t  lt f)" unfolding lc_def by simp
    show ?thesis
    proof (intro disjI1, rule bexI[of _ f], intro conjI, fact+)
      from q eq1 eq2 show "q = p - monom_mult (lc p / lc f) (lp p - lp f) f"
        by simp
    qed (fact)
  next
    case False
    from this lookup_tail_2[of p "t  lt f"]
      have ct: "lookup (tail p) (t  lt f) = lookup p (t  lt f)" by simp
    show ?thesis
    proof (intro disjI2, intro red_setI[of f], fact)
      show "red_single (tail p) (q - monomial (lc p) (lt p)) f t" unfolding red_single_def
      proof (intro conjI, fact)
        from cn0 ct show "lookup (tail p) (t  lt f)  0" by simp
      next
        from leading_monomial_tail[of p]
          have "p - monomial (lc p) (lt p) = (monomial (lc p) (lt p) + tail p) - monomial (lc p) (lt p)"
          by simp
        also have " = tail p" by simp
        finally have eq: "p - monomial (lc p) (lt p) = tail p" .
        from q have "q - monomial (lc p) (lt p) =
                    (p - monomial (lc p) (lt p)) - monom_mult ((lookup p (t  lt f)) / lc f) t f" by simp
        also from eq have " = tail p - monom_mult ((lookup p (t  lt f)) / lc f) t f" by simp
        finally show "q - monomial (lc p) (lt p) = tail p - monom_mult (lookup (tail p) (t  lt f) / lc f) t f"
          using ct by simp
      qed
    qed
  qed
qed

lemma is_redI:
  assumes "red F a b"
  shows "is_red F a"
  unfolding is_red_def relation.is_final_def by (simp, intro exI[of _ b], fact)

lemma is_redE:
  assumes "is_red F a"
  obtains b where "red F a b"
  using assms unfolding is_red_def relation.is_final_def
proof simp
  assume r: "b. red F a b  thesis" and b: "x. red F a x"
  from b obtain b where "red F a b" ..
  show thesis by (rule r[of b], fact)
qed

lemma is_red_alt:
  shows "is_red F a  (b. red F a b)"
proof
  assume "is_red F a"
  from is_redE[OF this] obtain b where "red F a b" .
  show "b. red F a b" by (intro exI[of _ b], fact)
next
  assume "b. red F a b"
  from this obtain b where "red F a b" ..
  show "is_red F a" by (rule is_redI, fact)
qed

lemma is_red_singletonI:
  assumes "is_red F q"
  obtains p where "p  F" and "is_red {p} q"
proof -
  from assms obtain q0 where "red F q q0" unfolding is_red_alt ..
  from this red_def[of F q q0] obtain p where "p  F" and t: "t. red_single q q0 p t" by auto
  have "is_red {p} q" unfolding is_red_alt
  proof
    from red_singleton[of p q q0] t show "red {p} q q0" by simp
  qed
  from p  F this show ?thesis ..
qed

lemma is_red_singletonD:
  assumes "is_red {p} q" and "p  F"
  shows "is_red F q"
proof -
  from assms(1) obtain q0 where "red {p} q q0" unfolding is_red_alt ..
  from red_singleton[of p q q0] this have "t. red_single q q0 p t" ..
  from this obtain t where "red_single q q0 p t" ..
  show ?thesis unfolding is_red_alt
    by (intro exI[of _ q0], intro red_setI[OF assms(2), of q q0 t], fact)
qed

lemma is_red_singleton_trans:
  assumes "is_red {f} p" and "lt g addst lt f" and "g  0"
  shows "is_red {g} p"
proof -
  from is_red {f} p obtain q where "red {f} p q" unfolding is_red_alt ..
  from this red_singleton[of f p q] obtain t where "red_single p q f t" by auto
  from red_single_trans[OF this assms(2, 3)] obtain q0 where
    "red_single p q0 g (t + (lp f - lp g))" .
  show ?thesis
  proof (rule is_redI[of "{g}" p q0])
    show "red {g} p q0" unfolding red_def
      by (intro bexI[of _ g], intro exI[of _ "t + (lp f - lp g)"], fact, simp)
  qed
qed

lemma is_red_singleton_not_0:
  assumes "is_red {f} p"
  shows "f  0"
using assms unfolding is_red_alt
proof
  fix q
  assume "red {f} p q"
  from this red_singleton[of f p q] obtain t where "red_single p q f t" by auto
  thus ?thesis unfolding red_single_def ..
qed

lemma irred_0:
  shows "¬ is_red F 0"
proof (rule, rule is_redE)
  fix b
  assume "red F 0 b"
  from ord_p_zero_min[of b] red_ord[OF this] show False by simp
qed

lemma is_red_indI1:
  assumes "f  F" and "f  0" and "p  0" and "lt f addst lt p"
  shows "is_red F p"
by (intro is_redI, rule red_indI1[OF assms])

lemma is_red_indI2:
  assumes "p  0" and "is_red F (tail p)"
  shows "is_red F p"
proof -
  from is_redE[OF is_red F (tail p)] obtain q where "red F (tail p) q" .
  show ?thesis by (intro is_redI, rule red_indI2[OF p  0], fact)
qed

lemma is_red_indE:
  assumes "is_red F p"
  shows "(fF. f  0  lt f addst lt p)  is_red F (tail p)"
proof -
  from is_redE[OF assms] obtain q where "red F p q" .
  from red_indE[OF this] show ?thesis
  proof
    assume "fF. f  0  lt f addst lt p  q = p - monom_mult (lc p / lc f) (lp p - lp f) f"
    from this obtain f where "f  F" and "f  0" and "lt f addst lt p" by auto
    show ?thesis by (intro disjI1, rule bexI[of _ f], intro conjI, fact+)
  next
    assume "red F (tail p) (q - monomial (lc p) (lt p))"
    show ?thesis by (intro disjI2, intro is_redI, fact)
  qed
qed

lemma rtrancl_0:
  assumes "(red F)** 0 x"
  shows "x = 0"
proof -
  from irred_0[of F] have "relation.is_final (red F) 0" unfolding is_red_def by simp
  from relation.rtrancl_is_final[OF (red F)** 0 x this] show ?thesis by simp
qed

lemma red_rtrancl_ord:
  assumes "(red F)** p q"
  shows "q p p"
  using assms
proof induct
  case base
  show ?case ..
next
  case (step y z)
  from step(2) have "z p y" by (rule red_ord)
  hence "z p y" by simp
  also note step(3)
  finally show ?case .
qed

lemma components_red_subset:
  assumes "red F p q"
  shows "component_of_term ` keys q  component_of_term ` keys p  component_of_term ` Keys F"
proof -
  from assms obtain f t where "f  F" and "red_single p q f t" by (rule red_setE)
  from this(2) have q: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    by (simp add: red_single_def)
  have "component_of_term ` keys q 
        component_of_term ` (keys p  keys (monom_mult ((lookup p (t  lt f)) / lc f) t f))"
    by (rule image_mono, simp add: q keys_minus)
  also have "...  component_of_term ` keys p  component_of_term ` Keys F"
  proof (simp add: image_Un, rule)
    fix k
    assume "k  component_of_term ` keys (monom_mult (lookup p (t  lt f) / lc f) t f)"
    then obtain v where "v  keys (monom_mult (lookup p (t  lt f) / lc f) t f)"
      and "k = component_of_term v" ..
    from this(1) keys_monom_mult_subset have "v  (⊕) t ` keys f" ..
    then obtain u where "u  keys f" and "v = t  u" ..
    have "k = component_of_term u" by (simp add: k = component_of_term v v = t  u term_simps)
    with u  keys f have "k  component_of_term ` keys f" by fastforce
    also have "...  component_of_term ` Keys F" by (rule image_mono, rule keys_subset_Keys, fact)
    finally show "k  component_of_term ` keys p  component_of_term ` Keys F" by simp
  qed
  finally show ?thesis .
qed

corollary components_red_rtrancl_subset:
  assumes "(red F)** p q"
  shows "component_of_term ` keys q  component_of_term ` keys p  component_of_term ` Keys F"
  using assms
proof (induct)
  case base
  show ?case by simp
next
  case (step q r)
  from step(2) have "component_of_term ` keys r  component_of_term ` keys q  component_of_term ` Keys F"
    by (rule components_red_subset)
  also from step(3) have "...  component_of_term ` keys p  component_of_term ` Keys F" by blast
  finally show ?case .
qed

subsection ‹Reducibility and Addition \& Multiplication›

lemma red_single_monom_mult:
  assumes "red_single p q f t" and "c  0"
  shows "red_single (monom_mult c s p) (monom_mult c s q) f (s + t)"
proof -
  from assms(1) have "f  0"
    and "lookup p (t  lt f)  0"
    and q_def: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    unfolding red_single_def by auto
  have assoc: "(s + t)  lt f = s  (t  lt f)" by (simp add: ac_simps)
  have g2: "lookup (monom_mult c s p) ((s + t)  lt f)  0"
  proof
    assume "lookup (monom_mult c s p) ((s + t)  lt f) = 0"
    hence "c * lookup p (t  lt f) = 0" using assoc by (simp add: lookup_monom_mult_plus)
    thus False using c  0 lookup p (t  lt f)  0 by simp
  qed
  have g3: "monom_mult c s q =
    (monom_mult c s p) - monom_mult ((lookup (monom_mult c s p) ((s + t)  lt f)) / lc f) (s + t) f"
  proof -
    from q_def monom_mult_dist_right_minus[of c s p]
      have "monom_mult c s q =
            monom_mult c s p - monom_mult c s (monom_mult (lookup p (t  lt f) / lc f) t f)" by simp
    also from monom_mult_assoc[of c s "lookup p (t  lt f) / lc f" t f] assoc
      have "monom_mult c s (monom_mult (lookup p (t  lt f) / lc f) t f) =
            monom_mult ((lookup (monom_mult c s p) ((s + t)  lt f)) / lc f) (s + t) f"
        by (simp add: lookup_monom_mult_plus)
    finally show ?thesis .
  qed
  from f  0 g2 g3 show ?thesis unfolding red_single_def by auto
qed

lemma red_single_plus_1:
  assumes "red_single p q f t" and "t  lt f  keys (p + r)"
  shows "red_single (q + r) (p + r) f t"
proof -
  from assms have "f  0" and "lookup p (t  lt f)  0"
    and q: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    by (simp_all add: red_single_def)
  from assms(1) have cq_0: "lookup q (t  lt f) = 0" by (rule red_single_lookup)
  from assms(2) have "lookup (p + r) (t  lt f) = 0"
    by (simp add: in_keys_iff)
  with neg_eq_iff_add_eq_0[of "lookup p (t  lt f)" "lookup r (t  lt f)"]
    have cr: "lookup r (t  lt f) = - (lookup p (t  lt f))" by (simp add: lookup_add)
  hence cr_not_0: "lookup r (t  lt f)  0" using lookup p (t  lt f)  0 by simp
  from f  0 show ?thesis unfolding red_single_def
  proof (intro conjI)
    from cr_not_0 show "lookup (q + r) (t  lt f)  0" by (simp add: lookup_add cq_0)
  next
    from lc_not_0[OF f  0]
      have "monom_mult ((lookup (q + r) (t  lt f)) / lc f) t f =
                  monom_mult ((lookup r (t  lt f)) / lc f) t f"
        by (simp add: field_simps lookup_add cq_0)
    thus "p + r = q + r - monom_mult (lookup (q + r) (t  lt f) / lc f) t f"
      by (simp add: cr q monom_mult_uminus_left)
  qed
qed

lemma red_single_plus_2:
  assumes "red_single p q f t" and "t  lt f  keys (q + r)"
  shows "red_single (p + r) (q + r) f t"
proof -
  from assms have "f  0" and cp: "lookup p (t  lt f)  0"
    and q: "q = p - monom_mult ((lookup p (t  lt f)) / lc f) t f"
    by (simp_all add: red_single_def)
  from assms(1) have cq_0: "lookup q (t  lt f) = 0" by (rule red_single_lookup)
  with assms(2) have cr_0: "lookup r (t  lt f) = 0"
    by (simp add: lookup_add in_keys_iff)
  from f  0 show ?thesis unfolding red_single_def
  proof (intro conjI)
    from cp show "lookup (p + r) (t  lt f)  0" by (simp add: lookup_add cr_0)
  next
    show "q + r = p + r - monom_mult (lookup (p + r) (t  lt f) / lc f) t f"
      by (simp add: cr_0 q lookup_add)
  qed
qed

lemma red_single_plus_3:
  assumes "red_single p q f t" and "t  lt f  keys (p + r)" and "t  lt f  keys (q + r)"
  shows "s. red_single (p + r) s f t  red_single (q + r) s f t"
proof -
  let ?t = "t  lt f"
  from assms have "f  0" and "lookup p ?t  0"
    and q: "q = p - monom_mult ((lookup p ?t) / lc f) t f"
    by (simp_all add: red_single_def)
  from assms(2) have cpr: "lookup (p + r) ?t  0" by (simp add: in_keys_iff)
  from assms(3) have cqr: "lookup (q + r) ?t  0" by (simp add: in_keys_iff)
  from assms(1) have cq_0: "lookup q ?t = 0" by (rule red_single_lookup)
  let ?s = "(p + r) - monom_mult ((lookup (p + r) ?t) / lc f) t f"
  from f  0 cpr have "red_single (p + r) ?s f t" by (simp add: red_single_def)
  moreover from f  0 have "red_single (q + r) ?s f t" unfolding red_single_def
  proof (intro conjI)
    from cqr show "lookup (q + r) ?t  0" .
  next
    from lc_not_0[OF f  0]
      monom_mult_dist_left[of "(lookup p ?t) / lc f" "(lookup r ?t) / lc f" t f]
      have "monom_mult ((lookup (p + r) ?t) / lc f) t f =
                (monom_mult ((lookup p ?t) / lc f) t f) +
                  (monom_mult ((lookup r ?t) / lc f) t f)"
        by (simp add: field_simps lookup_add)
    moreover from lc_not_0[OF f  0]
      monom_mult_dist_left[of "(lookup q ?t) / lc f" "(lookup r ?t) / lc f" t f]
      have "monom_mult ((lookup (q + r) ?t) / lc f) t f =
                monom_mult ((lookup r ?t) / lc f) t f"
        by (simp add: field_simps lookup_add cq_0)
    ultimately show "p + r - monom_mult (lookup (p + r) ?t / lc f) t f =
                     q + r - monom_mult (lookup (q + r) ?t / lc f) t f" by (simp add: q)
  qed
  ultimately show ?thesis by auto
qed

lemma red_single_plus:
  assumes "red_single p q f t"
  shows "red_single (p + r) (q + r) f t 
          red_single (q + r) (p + r) f t 
          (s. red_single (p + r) s f t  red_single (q + r) s f t)" (is "?A  ?B  ?C")
proof (cases "t  lt f  keys (p + r)")
  case True
  show ?thesis
  proof (cases "t  lt f  keys (q + r)")
    case True
    with assms t  lt f  keys (p + r) have ?C by (rule red_single_plus_3)
    thus ?thesis by simp
  next
    case False
    with assms have ?A by (rule red_single_plus_2)
    thus ?thesis ..
  qed
next
  case False
  with assms have ?B by (rule red_single_plus_1)
  thus ?thesis by simp
qed

lemma red_single_diff:
  assumes "red_single (p - q) r f t"
  shows "red_single p (r + q) f t  red_single q (p - r) f t 
          (p' q'. red_single p p' f t  red_single q q' f t  r = p' - q')" (is "?A  ?B  ?C")
proof -
  let ?s = "t  lt f"
  from assms have "f  0"
    and "lookup (p - q) ?s  0"
    and r: "r = p - q - monom_mult ((lookup (p - q) ?s) / lc f) t f"
    unfolding red_single_def by auto
  from this(2) have diff: "lookup p ?s  lookup q ?s" by (simp add: lookup_minus)
  show ?thesis
  proof (cases "lookup p ?s = 0")
    case True
    with diff have "?s  keys q" by (simp add: in_keys_iff)
    moreover have "lookup (p - q) ?s = - lookup q ?s" by (simp add: lookup_minus True)
    ultimately have ?B using f  0 by (simp add: in_keys_iff red_single_def r monom_mult_uminus_left)
    thus ?thesis by simp
  next
    case False
    hence "?s  keys p" by (simp add: in_keys_iff)
    show ?thesis
    proof (cases "lookup q ?s = 0")
      case True
      hence "lookup (p - q) ?s = lookup p ?s" by (simp add: lookup_minus)
      hence ?A using f  0 ?s  keys p by (simp add: in_keys_iff red_single_def r monom_mult_uminus_left)
      thus ?thesis ..
    next
      case False
      hence "?s  keys q" by (simp add: in_keys_iff)
      let ?p = "p - monom_mult ((lookup p ?s) / lc f) t f"
      let ?q = "q - monom_mult ((lookup q ?s) / lc f) t f"
      have ?C
      proof (intro exI conjI)
        from f  0 ?s  keys p show "red_single p ?p f t" by (simp add: in_keys_iff red_single_def)
      next
        from f  0 ?s  keys q show "red_single q ?q f t" by (simp add: in_keys_iff red_single_def)
      next
        from f  0 have "lc f  0" by (rule lc_not_0)
        hence eq: "(lookup p ?s - lookup q ?s) / lc f =
                   lookup p ?s / lc f - lookup q ?s / lc f" by (simp add: field_simps)
        show "r = ?p - ?q" by (simp add: r lookup_minus eq monom_mult_dist_left_minus)
      qed
      thus ?thesis by simp
    qed
  qed
qed

lemma red_monom_mult:
  assumes a: "red F p q" and "c  0"
  shows "red F (monom_mult c s p) (monom_mult c s q)"
proof -
  from red_setE[OF a] obtain f and t where "f  F" and rs: "red_single p q f t" by auto
  from red_single_monom_mult[OF rs c  0, of s] show ?thesis by (intro red_setI[OF f  F])
qed

lemma red_plus_keys_disjoint:
  assumes "red F p q" and "keys p  keys r = {}"
  shows "red F (p + r) (q + r)"
proof -
  from assms(1) obtain f t where "f  F" and *: "red_single p q f t" by (rule red_setE)
  from this(2) have "red_single (p + r) (q + r) f t"
  proof (rule red_single_plus_2)
    from * have "lookup q (t  lt f) = 0"
      by (simp add: red_single_def lookup_minus lookup_monom_mult lc_def[symmetric] lc_not_0 term_simps)
    hence "t  lt f  keys q" by (simp add: in_keys_iff)
    moreover have "t  lt f  keys r"
    proof
      assume "t  lt f  keys r"
      moreover from * have "t  lt f  keys p" by (simp add: in_keys_iff red_single_def)
      ultimately have "t  lt f  keys p  keys r" by simp
      with assms(2) show False by simp
    qed
    ultimately have "t  lt f  keys q  keys r" by simp
    thus "t  lt f  keys (q + r)"
      by (meson Poly_Mapping.keys_add subsetD)
  qed
  with f  F show ?thesis by (rule red_setI)
qed

lemma red_plus:
  assumes "red F p q"
  obtains s where "(red F)** (p + r) s" and "(red F)** (q + r) s"
proof -
  from red_setE[OF assms] obtain f and t where "f  F" and rs: "red_single p q f t" by auto
  from red_single_plus[OF rs, of r] show ?thesis
  proof
    assume c1: "red_single (p + r) (q + r) f t"
    show ?thesis
    proof
      from c1 show "(red F)** (p + r) (q + r)" by (intro r_into_rtranclp, intro red_setI[OF f  F])
    next
      show "(red F)** (q + r) (q + r)" ..
    qed
  next
    assume "red_single (q + r) (p + r) f t  (s. red_single (p + r) s f t  red_single (q + r) s f t)"
    thus ?thesis
    proof
      assume c2: "red_single (q + r) (p + r) f t"
      show ?thesis
      proof
        show "(red F)** (p + r) (p + r)" ..
      next
        from c2 show "(red F)** (q + r) (p + r)" by (intro r_into_rtranclp, intro red_setI[OF f  F])
      qed
    next
      assume "s. red_single (p + r) s f t  red_single (q + r) s f t"
      then obtain s where s1: "red_single (p + r) s f t" and s2: "red_single (q + r) s f t" by auto
      show ?thesis
      proof
        from s1 show "(red F)** (p + r) s" by (intro r_into_rtranclp, intro red_setI[OF f  F])
      next
        from s2 show "(red F)** (q + r) s" by (intro r_into_rtranclp, intro red_setI[OF f  F])
      qed
    qed
  qed
qed

corollary red_plus_cs:
  assumes "red F p q"
  shows "relation.cs (red F) (p + r) (q + r)"
  unfolding relation.cs_def
proof -
  from assms obtain s where "(red F)** (p + r) s" and "(red F)** (q + r) s" by (rule red_plus)
  show "s. (red F)** (p + r) s  (red F)** (q + r) s" by (intro exI, intro conjI, fact, fact)
qed

lemma red_uminus:
  assumes "red F p q"
  shows "red F (-p) (-q)"
  using red_monom_mult[OF assms, of "-1" 0] by (simp add: uminus_monom_mult)

lemma red_diff:
  assumes "red F (p - q) r"
  obtains p' q' where "(red F)** p p'" and "(red F)** q q'" and "r = p' - q'"
proof -
  from assms obtain f t where "f  F" and "red_single (p - q) r f t" by (rule red_setE)
  from red_single_diff[OF this(2)] show ?thesis
  proof (elim disjE)
    assume "red_single p (r + q) f t"
    with f  F have *: "red F p (r + q)" by (rule red_setI)
    show ?thesis
    proof
      from * show "(red F)** p (r + q)" ..
    next
      show "(red F)** q q" ..
    qed simp
  next
    assume "red_single q (p - r) f t"
    with f  F have *: "red F q (p - r)" by (rule red_setI)
    show ?thesis
    proof
      show "(red F)** p p" ..
    next
      from * show "(red F)** q (p - r)" ..
    qed simp
  next
    assume "p' q'. red_single p p' f t  red_single q q' f t  r = p' - q'"
    then obtain p' q' where 1: "red_single p p' f t" and 2: "red_single q q' f t" and "r = p' - q'"
      by blast
    from f  F 2 have "red F q q'" by (rule red_setI)
    from f  F 1 have "red F p p'" by (rule red_setI)
    hence "(red F)** p p'" ..
    moreover from red F q q' have "(red F)** q q'" ..
    moreover note r = p' - q'
    ultimately show ?thesis ..
  qed
qed

lemma red_diff_rtrancl':
  assumes "(red F)** (p - q) r"
  obtains p' q' where "(red F)** p p'" and "(red F)** q q'" and "r = p' - q'"
  using assms
proof (induct arbitrary: thesis rule: rtranclp_induct)
  case base
  show ?case by (rule base, fact rtrancl_refl[to_pred], fact rtrancl_refl[to_pred], fact refl)
next
  case (step y z)
  obtain p1 q1 where p1: "(red F)** p p1" and q1: "(red F)** q q1" and y: "y = p1 - q1" by (rule step(3))
  from step(2) obtain p' q' where p': "(red F)** p1 p'" and q': "(red F)** q1 q'" and z: "z = p' - q'"
    unfolding y by (rule red_diff)
  show ?case
  proof (rule step(4))
    from p1 p' show "(red F)** p p'" by simp
  next
    from q1 q' show "(red F)** q q'" by simp
  qed fact
qed

lemma red_diff_rtrancl:
  assumes "(red F)** (p - q) 0"
  obtains s where "(red F)** p s" and "(red F)** q s"
proof -
  from assms obtain p' q' where p': "(red F)** p p'" and q': "(red F)** q q'" and "0 = p' - q'"
    by (rule red_diff_rtrancl')
  from this(3) have "q' = p'" by simp
  from p' q' show ?thesis unfolding q' = p' ..
qed

corollary red_diff_rtrancl_cs:
  assumes "(red F)** (p - q) 0"
  shows "relation.cs (red F) p q"
  unfolding relation.cs_def
proof -
  from assms obtain s where "(red F)** p s" and "(red F)** q s" by (rule red_diff_rtrancl)
  show "s. (red F)** p s  (red F)** q s" by (intro exI, intro conjI, fact, fact)
qed

subsection ‹Confluence of Reducibility›

lemma confluent_distinct_aux:
  assumes r1: "red_single p q1 f1 t1" and r2: "red_single p q2 f2 t2"
    and "t1  lt f1 t t2  lt f2" and "f1  F" and "f2  F"
  obtains s where "(red F)** q1 s" and "(red F)** q2 s"
proof -
  from r1 have "f1  0" and c1: "lookup p (t1  lt f1)  0"
    and q1_def: "q1 = p - monom_mult (lookup p (t1  lt f1) / lc f1) t1 f1"
    unfolding red_single_def by auto
  from r2 have "f2  0" and c2: "lookup p (t2  lt f2)  0"
    and q2_def: "q2 = p - monom_mult (lookup p (t2  lt f2) / lc f2) t2 f2"
    unfolding red_single_def by auto
  from t1  lt f1 t t2  lt f2
  have "lookup (monom_mult (lookup p (t1  lt f1) / lc f1) t1 f1) (t2  lt f2) = 0"
    by (simp add: lookup_monom_mult_eq_zero)
  from lookup_minus[of p _ "t2  lt f2"] this have c: "lookup q1 (t2  lt f2) = lookup p (t2  lt f2)"
    unfolding q1_def by simp
  define q3 where "q3  q1 - monom_mult ((lookup q1 (t2  lt f2)) / lc f2) t2 f2"
  have "red_single q1 q3 f2 t2" unfolding red_single_def
  proof (rule, fact, rule)
    from c c2 show "lookup q1 (t2  lt f2)  0" by simp
  next
    show "q3 = q1 - monom_mult (lookup q1 (t2  lt f2) / lc f2) t2 f2" unfolding q3_def ..
  qed
  hence "red F q1 q3" by (intro red_setI[OF f2  F])
  hence q1q3: "(red F)** q1 q3" by (intro r_into_rtranclp)
  from r1 have "red F p q1" by (intro red_setI[OF f1  F])
  from red_plus[OF this, of "- monom_mult ((lookup p (t2  lt f2)) / lc f2) t2 f2"] obtain s
    where r3: "(red F)** (p - monom_mult (lookup p (t2  lt f2) / lc f2) t2 f2) s"
    and r4: "(red F)** (q1 - monom_mult (lookup p (t2  lt f2) / lc f2) t2 f2) s" by auto
  from r3 have q2s: "(red F)** q2 s" unfolding q2_def by simp
  from r4 c have q3s: "(red F)** q3 s" unfolding q3_def by simp
  show ?thesis
  proof
    from rtranclp_trans[OF q1q3 q3s] show "(red F)** q1 s" .
  next
    from q2s show "(red F)** q2 s" .
  qed
qed

lemma confluent_distinct:
  assumes r1: "red_single p q1 f1 t1" and r2: "red_single p q2 f2 t2"
    and ne: "t1  lt f1  t2  lt f2" and "f1  F" and "f2  F"
  obtains s where "(red F)** q1 s" and "(red F)** q2 s"
proof -
  from ne have "t1  lt f1 t t2  lt f2  t2  lt f2 t t1  lt f1" by auto
  thus ?thesis
  proof
    assume a1: "t1  lt f1 t t2  lt f2"
    from confluent_distinct_aux[OF r1 r2 a1 f1  F f2  F] obtain s where
      "(red F)** q1 s" and "(red F)** q2 s" .
    thus ?thesis ..
  next
    assume a2: "t2  lt f2 t t1  lt f1"
    from confluent_distinct_aux[OF r2 r1 a2 f2  F f1  F] obtain s where
      "(red F)** q1 s" and "(red F)** q2 s" .
    thus ?thesis ..
  qed
qed

corollary confluent_same:
  assumes r1: "red_single p q1 f t1" and r2: "red_single p q2 f t2" and "f  F"
  obtains s where "(red F)** q1 s" and "(red F)** q2 s"
proof (cases "t1 = t2")
  case True
  with r1 r2 have "q1 = q2" by (simp add: red_single_def)
  show ?thesis
  proof
    show "(red F)** q1 q2" unfolding q1 = q2 ..
  next
    show "(red F)** q2 q2" ..
  qed
next
  case False
  hence "t1  lt f  t2  lt f" by (simp add: term_simps)
  from r1 r2 this f  F f  F obtain s where "(red F)** q1 s" and "(red F)** q2 s"
    by (rule confluent_distinct)
  thus ?thesis ..
qed

subsection ‹Reducibility and Module Membership›

lemma srtc_in_pmdl:
  assumes "relation.srtc (red F) p q"
  shows "p - q  pmdl F"
  using assms unfolding relation.srtc_def
proof (induct rule: rtranclp.induct)
  fix p
  show "p - p  pmdl F" by (simp add: pmdl.span_zero)
next
  fix p r q
  assume pr_in: "p - r  pmdl F" and red: "red F r q  red F q r"
  from red obtain f c t where "f  F" and "q = r - monom_mult c t f"
  proof
    assume "red F r q"
    from red_setE[OF this] obtain f t where "f  F" and "red_single r q f t" .
    hence "q = r - monom_mult (lookup r (t  lt f) / lc f) t f" by (simp add: red_single_def)
    show thesis by (rule, fact, fact)
  next
    assume "red F q r"
    from red_setE[OF this] obtain f t where "f  F" and "red_single q r f t" .
    hence "r = q - monom_mult (lookup q (t  lt f) / lc f) t f" by (simp add: red_single_def)
    hence "q = r + monom_mult (lookup q (t  lt f) / lc f) t f" by simp
    hence "q = r - monom_mult (-(lookup q (t  lt f) / lc f)) t f"
      using monom_mult_uminus_left[of _ t f] by simp
    show thesis by (rule, fact, fact)
  qed
  hence eq: "p - q = (p - r) + monom_mult c t f" by simp
  show "p - q  pmdl F" unfolding eq
    by (rule pmdl.span_add, fact, rule monom_mult_in_pmdl, fact)
qed

lemma in_pmdl_srtc:
  assumes "p  pmdl F"
  shows "relation.srtc (red F) p 0"
  using assms
proof (induct p rule: pmdl_induct)
  show "relation.srtc (red F) 0 0" unfolding relation.srtc_def ..
next
  fix a f c t
  assume a_in: "a  pmdl F" and IH: "relation.srtc (red F) a 0" and "f  F"
  show "relation.srtc (red F) (a + monom_mult c t f) 0"
  proof (cases "c = 0")
    assume "c = 0"
    hence "a + monom_mult c t f = a" by simp
    thus ?thesis using IH by simp
  next
    assume "c  0"
    show ?thesis
    proof (cases "f = 0")
      assume "f = 0"
      hence "a + monom_mult c t f = a" by simp
      thus ?thesis using IH by simp
    next
      assume "f  0"
      from lc_not_0[OF this] have "lc f  0" .
      have "red F (monom_mult c t f) 0"
      proof (intro red_setI[OF f  F])
        from lookup_monom_mult_plus[of c t f "lt f"]
          have eq: "lookup (monom_mult c t f) (t  lt f) = c * lc f" unfolding lc_def .
        show "red_single (monom_mult c t f) 0 f t" unfolding red_single_def eq
        proof (intro conjI, fact)
          from c  0 lc f  0 show "c * lc f  0" by simp
        next
          from lc f  0 show "0 = monom_mult c t f - monom_mult (c * lc f / lc f) t f" by simp
        qed
      qed
      from red_plus[OF this, of a] obtain s where
        s1: "(red F)** (monom_mult c t f + a) s" and s2: "(red F)** (0 + a) s" .
      have "relation.cs (red F) (a + monom_mult c t f) a" unfolding relation.cs_def
      proof (intro exI[of _ s], intro conjI)
        from s1 show "(red F)** (a + monom_mult c t f) s" by (simp only: add.commute)
      next
        from s2 show "(red F)** a s" by simp
      qed
      from relation.srtc_transitive[OF relation.cs_implies_srtc[OF this] IH] show ?thesis .
    qed
  qed
qed

lemma red_rtranclp_diff_in_pmdl:
  assumes "(red F)** p q"
  shows "p - q  pmdl F"
proof -
  from assms have "relation.srtc (red F) p q"
    by (simp add: r_into_rtranclp relation.rtc_implies_srtc)
  thus ?thesis by (rule srtc_in_pmdl)
qed

corollary red_diff_in_pmdl:
  assumes "red F p q"
  shows "p - q  pmdl F"
  by (rule red_rtranclp_diff_in_pmdl, rule r_into_rtranclp, fact)
  
corollary red_rtranclp_0_in_pmdl:
  assumes "(red F)** p 0"
  shows "p  pmdl F"
  using assms red_rtranclp_diff_in_pmdl by fastforce

lemma pmdl_closed_red:
  assumes "pmdl B  pmdl A" and "p  pmdl A" and "red B p q"
  shows "q  pmdl A"
proof -
  have "q - p  pmdl A"
  proof
    have "p - q  pmdl B" by (rule red_diff_in_pmdl, fact)
    hence "- (p - q)  pmdl B" by (rule pmdl.span_neg)
    thus "q - p  pmdl B" by simp
  qed fact
  from pmdl.span_add[OF this p  pmdl A] show ?thesis by simp
qed

subsection ‹More Properties of @{const red}, @{const red_single} and @{const is_red}

lemma red_rtrancl_mult:
  assumes "(red F)** p q"
  shows "(red F)** (monom_mult c t p) (monom_mult c t q)"
proof (cases "c = 0")
  case True
  have "(red F)** 0 0" by simp
  thus ?thesis by (simp only: True monom_mult_zero_left)
next
  case False
  from assms show ?thesis
  proof (induct rule: rtranclp_induct)
    show "(red F)** (monom_mult c t p) (monom_mult c t p)" by simp
  next
    fix q0 q
    assume "(red F)** p q0" and "red F q0 q" and "(red F)** (monom_mult c t p) (monom_mult c t q0)"
    show "(red F)** (monom_mult c t p) (monom_mult c t q)"
    proof (rule rtranclp.intros(2)[OF (red F)** (monom_mult c t p) (monom_mult c t q0)])
      from red_monom_mult[OF red F q0 q False, of t] show "red F (monom_mult c t q0) (monom_mult c t q)" .
    qed
  qed
qed

corollary red_rtrancl_uminus:
  assumes "(red F)** p q"
  shows "(red F)** (-p) (-q)"
  using red_rtrancl_mult[OF assms, of "-1" 0] by (simp add: uminus_monom_mult)

lemma red_rtrancl_diff_induct [consumes 1, case_names base step]:
  assumes a: "(red F)** (p - q) r"
    and cases: "P p p" "!!y z. [| (red F)** (p - q) z; red F z y; P p (q + z)|] ==> P p (q + y)"
  shows "P p (q + r)"
  using a
proof (induct rule: rtranclp_induct)
  from cases(1) show "P p (q + (p - q))" by simp
next
  fix y z
  assume "(red F)** (p - q) z" "red F z y" "P p (q + z)"
  thus "P p (q + y)" using cases(2) by simp
qed

lemma red_rtrancl_diff_0_induct [consumes 1, case_names base step]:
  assumes a: "(red F)** (p - q) 0"
    and base: "P p p" and ind: "y z. [| (red F)** (p - q) y; red F y z; P p (y + q)|] ==> P p (z + q)"
  shows "P p q"
proof -
  from ind red_rtrancl_diff_induct[of F p q 0 P, OF a base] have "P p (0 + q)"
    by (simp add: ac_simps)
  thus ?thesis by simp
qed

lemma is_red_union: "is_red (A  B) p  (is_red A p  is_red B p)"
  unfolding is_red_alt red_union by auto

lemma red_single_0_lt:
  assumes "red_single f 0 h t"
  shows "lt f = t  lt h"
proof -
  from red_single_nonzero1[OF assms] have "f  0" .
  {
    assume "h  0" and neq: "lookup f (t  lt h)  0" and
      eq: "f = monom_mult (lookup f (t  lt h) / lc h) t h"
    from lc_not_0[OF h  0] have "lc h  0" .
    with neq have "(lookup f (t  lt h) / lc h)  0" by simp
    from eq lt_monom_mult[OF this h  0, of t] have "lt f = t  lt h" by simp
    hence "lt f = t  lt h" by (simp add: ac_simps)
  }
  with assms show ?thesis unfolding red_single_def by auto
qed

lemma red_single_lt_distinct_lt:
  assumes rs: "red_single f g h t" and "g  0" and "lt g  lt f"
  shows "lt f = t  lt h"
proof -
  from red_single_nonzero1[OF rs] have "f  0" .
  from red_single_ord[OF rs] have "g p f" by simp
  from ord_p_lt[OF this] lt g  lt f have "lt g t lt f" by simp
  {
    assume "h  0" and neq: "lookup f (t  lt h)  0" and
      eq: "f = g + monom_mult (lookup f (t  lt h) / lc h) t h" (is "f = g + ?R")
    from lc_not_0[OF h  0] have "lc h  0" .
    with neq have "(lookup f (t  lt h) / lc h)  0" (is "?c  0") by simp
    from eq lt_monom_mult[OF this h  0, of t] have ltR: "lt ?R = t  lt h" by simp
    from monom_mult_eq_zero_iff[of ?c t h] ?c  0 h  0 have "?R  0" by auto
    from lt_plus_lessE[of g] eq lt g t lt f have "lt g t lt ?R" by auto
    from lt_plus_eqI[OF this] eq ltR have "lt f = t  lt h" by (simp add: ac_simps)
  }
  with assms show ?thesis unfolding red_single_def by auto
qed

lemma zero_reducibility_implies_lt_divisibility':
  assumes "(red F)** f 0" and "f  0"
  shows "hF. h  0  (lt h addst lt f)"
  using assms
proof (induct rule: converse_rtranclp_induct)
  case base
  then show ?case by simp
next
  case (step f g)
  show ?case
  proof (cases "g = 0")
    case True
    with step.hyps have "red F f 0" by simp
    from red_setE[OF this] obtain h t where "h  F" and rs: "red_single f 0 h t" by auto
    show ?thesis
    proof
      from red_single_0_lt[OF rs] have "lt h addst lt f" by (simp add: term_simps)
      also from rs have "h  0" by (simp add: red_single_def) 
      ultimately show "h  0  lt h addst lt f" by simp
    qed (rule h  F)
  next
    case False
    show ?thesis
    proof (cases "lt g = lt f")
      case True
      with False step.hyps show ?thesis by simp
    next
      case False
      from red_setE[OF red F f g] obtain h t where "h  F" and rs: "red_single f g h t" by auto
      show ?thesis
      proof
        from red_single_lt_distinct_lt[OF rs g  0 False] have "lt h addst lt f"
          by (simp add: term_simps)
        also from rs have "h  0" by (simp add: red_single_def) 
        ultimately show "h  0  lt h addst lt f" by simp
      qed (rule h  F)
    qed
  qed
qed
  
lemma zero_reducibility_implies_lt_divisibility:
  assumes "(red F)** f 0" and "f  0"
  obtains h where "h  F" and "h  0" and "lt h addst lt f"
  using zero_reducibility_implies_lt_divisibility'[OF assms] by auto

lemma is_red_addsI:
  assumes "f  F" and "f  0" and "v  keys p" and "lt f addst v"
  shows "is_red F p"
  using assms
proof (induction p rule: poly_mapping_tail_induct)
  case 0
  from v  keys 0 show ?case by auto
next
  case (tail p)
  from "tail.IH"[OF f  F f  0 _ lt f addst v] have imp: "v  keys (tail p)  is_red F (tail p)" .
  show ?case
  proof (cases "v = lt p")
    case True
    show ?thesis
    proof (rule is_red_indI1[OF f  F f  0 p  0])
      from lt f addst v True show "lt f addst lt p" by simp
    qed
  next
    case False
    with v  keys p p  0 have "v  keys (tail p)"
      by (simp add: lookup_tail_2 in_keys_iff) 
    from is_red_indI2[OF p  0 imp[OF this]] show ?thesis .
  qed
qed

lemma is_red_addsE':
  assumes "is_red F p"
  shows "fF. vkeys p. f  0  lt f addst v"
  using assms
proof (induction p rule: poly_mapping_tail_induct)
  case 0
  with irred_0[of F] show ?case by simp
next
  case (tail p)
  from is_red_indE[OF is_red F p] show ?case
  proof
    assume "fF. f  0  lt f addst lt p"
    then obtain f where "f  F" and "f  0" and "lt f addst lt p" by auto
    show ?case
    proof
      show "vkeys p. f  0  lt f addst v"
      proof (intro bexI, intro conjI)
        from p  0 show "lt p  keys p" by (metis in_keys_iff lc_def lc_not_0)
      qed (rule f  0, rule lt f addst lt p)
    qed (rule f  F)
  next
    assume "is_red F (tail p)"
    from "tail.IH"[OF this] obtain f v
      where "f  F" and "f  0" and v_in_keys_tail: "v  keys (tail p)" and "lt f addst v" by auto
    from "tail.hyps" v_in_keys_tail have v_in_keys: "v  keys p" by (metis lookup_tail in_keys_iff)
    show ?case
    proof
      show "vkeys p. f  0  lt f addst v"
        by (intro bexI, intro conjI, rule f  0, rule lt f addst v, rule v_in_keys)
    qed (rule f  F)
  qed
qed

lemma is_red_addsE:
  assumes "is_red F p"
  obtains f v where "f  F" and "v  keys p" and "f  0" and "lt f addst v"
  using is_red_addsE'[OF assms] by auto

lemma is_red_adds_iff:
  shows "(is_red F p)  (fF. vkeys p. f  0  lt f addst v)"
  using is_red_addsE' is_red_addsI by auto
    
lemma is_red_subset:
  assumes red: "is_red A p" and sub: "A  B"
  shows "is_red B p"
proof -
  from red obtain f v where "f  A" and "v  keys p" and "f  0" and "lt f addst v" by (rule is_red_addsE)
  show ?thesis by (rule is_red_addsI, rule, fact+)
qed

lemma not_is_red_empty: "¬ is_red {} f"
  by (simp add: is_red_adds_iff)

lemma red_single_mult_const:
  assumes "red_single p q f t" and "c  0"
  shows "red_single p q (monom_mult c 0 f) t"
proof -
  let ?s = "t  lt f"
  let ?f = "monom_mult c 0 f"
  from assms(1) have "f  0" and "lookup p ?s  0"
    and "q = p - monom_mult ((lookup p ?s) / lc f) t f" by (simp_all add: red_single_def)
  from this(1) assms(2) have lt: "lt ?f = lt f" and lc: "lc ?f = c * lc f"
    by (simp add: lt_monom_mult term_simps, simp)
  show ?thesis unfolding red_single_def
  proof (intro conjI)
    from f  0 assms(2) show "?f  0" by (simp add: monom_mult_eq_zero_iff)
  next
    from lookup p ?s  0 show "lookup p (t  lt ?f)  0" by (simp add: lt)
  next
    show "q = p - monom_mult (lookup p (t  lt ?f) / lc ?f) t ?f"
      by (simp add: lt monom_mult_assoc lc assms(2), fact)
  qed
qed

lemma red_rtrancl_plus_higher:
  assumes "(red F)** p q" and "u v. u  keys p  v  keys r  u t v"
  shows "(red F)** (p + r) (q + r)"
  using assms(1)
proof induct
  case base
  show ?case ..
next
  case (step y z)
  from step(1) have "y p p" by (rule red_rtrancl_ord)
  hence "lt y t lt p" by (rule ord_p_lt)
  from step(2) have "red F (y + r) (z + r)"
  proof (rule red_plus_keys_disjoint)
    show "keys y  keys r = {}"
    proof (rule ccontr)
      assume "keys y  keys r  {}"
      then obtain v where "v  keys y" and "v  keys r" by auto
      from this(1) have "v t lt y" and "y  0" using lt_max by (auto simp: in_keys_iff)
      with y p p have "p  0" using ord_p_zero_min[of y] by auto
      hence "lt p  keys p" by (rule lt_in_keys)
      from this v  keys r have "lt p t v" by (rule assms(2))
      with lt y t lt p have "lt y t v" by simp
      with v t lt y  show False by simp
    qed
  qed
  with step(3) show ?case ..
qed

lemma red_mult_scalar_leading_monomial: "(red {f})** (p  monomial (lc f) (lt f)) (- p  tail f)"
proof (cases "f = 0")
  case True
  show ?thesis by (simp add: True lc_def)
next
  case False
  show ?thesis
  proof (induct p rule: punit.poly_mapping_tail_induct)
    case 0
    show ?case by simp
  next
    case (tail p)
    from False have "lc f  0" by (rule lc_not_0)
    from tail(1) have "punit.lc p  0" by (rule punit.lc_not_0)
    let ?t = "punit.tail p  monomial (lc f) (lt f)"
    let ?m = "monom_mult (punit.lc p) (punit.lt p) (monomial (lc f) (lt f))"
    from lc f  0 have kt: "keys ?t = (λt. t  lt f) ` keys (punit.tail p)"
      by (rule keys_mult_scalar_monomial_right)
    have km: "keys ?m = {punit.lt p  lt f}"
      by (simp add: keys_monom_mult[OF punit.lc p  0] lc f  0)
    from tail(2) have "(red {f})** (?t + ?m) (- punit.tail p  tail f + ?m)"
    proof (rule red_rtrancl_plus_higher)
      fix u v
      assume "u  keys ?t" and "v  keys ?m"
      from this(1) obtain s where "s  keys (punit.tail p)" and u: "u = s  lt f" unfolding kt ..
      from this(1) have "punit.tail p  0" and "s  punit.lt (punit.tail p)" using punit.lt_max by (auto simp: in_keys_iff)
      moreover from punit.tail p  0 have "punit.lt (punit.tail p)  punit.lt p" by (rule punit.lt_tail)
      ultimately have "s  punit.lt p" by simp
      moreover from v  keys ?m have "v = punit.lt p  lt f" by (simp only: km, simp)
      ultimately show "u t v" by (simp add: u splus_mono_strict_left)
    qed
    hence *: "(red {f})** (p  monomial (lc f) (lt f)) (?m - punit.tail p  tail f)"
      by (simp add: punit.leading_monomial_tail[symmetric, of p] mult_scalar_monomial[symmetric]
            mult_scalar_distrib_right[symmetric] add.commute[of "punit.tail p"])
    have "red {f} ?m (- (monomial (punit.lc p) (punit.lt p))  tail f)" unfolding red_singleton
    proof
      show "red_single ?m (- (monomial (punit.lc p) (punit.lt p))  tail f) f (punit.lt p)"
      proof (simp add: red_single_def f  0 km lookup_monom_mult lc f  0 punit.lc p  0 term_simps,
              simp add: monom_mult_dist_right_minus[symmetric] mult_scalar_monomial)
        have "monom_mult (punit.lc p) (punit.lt p) (monomial (lc f) (lt f) - f) =
              - monom_mult (punit.lc p) (punit.lt p) (f - monomial (lc f) (lt f))"
          by (metis minus_diff_eq monom_mult_uminus_right)
        also have "... = - monom_mult (punit.lc p) (punit.lt p) (tail f)" by (simp only: tail_alt_2)
        finally show "- monom_mult (punit.lc p) (punit.lt p) (tail f) =
                      monom_mult (punit.lc p) (punit.lt p) (monomial (lc f) (lt f) - f)" by simp
      qed
    qed
    hence "red {f} (?m + (- punit.tail p  tail f))
                    (- (monomial (punit.lc p) (punit.lt p))  tail f + (- punit.tail p  tail f))"
    proof (rule red_plus_keys_disjoint)
      show "keys ?m  keys (- punit.tail p  tail f) = {}"
      proof (cases "punit.tail p = 0")
        case True
        show ?thesis by (simp add: True)
      next
        case False
        from tail(2) have "- punit.tail p  tail f p ?t" by (rule red_rtrancl_ord)
        hence "lt (- punit.tail p  tail f) t lt ?t" by (rule ord_p_lt)
        also from lc f  0 False have "... = punit.lt (punit.tail p)  lt f"
          by (rule lt_mult_scalar_monomial_right)
        also from punit.lt_tail[OF False] have "... t punit.lt p  lt f" by (rule splus_mono_strict_left)
        finally have "punit.lt p  lt f  keys (- punit.tail p  tail f)" using lt_gr_keys by blast
        thus ?thesis by (simp add: km)
      qed
    qed
    hence "red {f} (?m - punit.tail p  tail f)
            (- (monomial (punit.lc p) (punit.lt p))  tail f - punit.tail p  tail f)"
      by (simp add: term_simps)
    also have "... = - p  tail f" using punit.leading_monomial_tail[symmetric, of p]
      by (metis (mono_tags, lifting) add_uminus_conv_diff minus_add_distrib mult_scalar_distrib_right
          mult_scalar_minus_mult_left)
    finally have "red {f} (?m - punit.tail p  tail f) (- p  tail f)" .
    with * show ?case ..
  qed
qed

corollary red_mult_scalar_lt:
  assumes "f  0"
  shows "(red {f})** (p  monomial c (lt f)) (monom_mult (- c / lc f) 0 (p  tail f))"
proof -
  from assms have "lc f  0" by (rule lc_not_0)
  hence 1: "p  monomial c (lt f) = punit.monom_mult (c / lc f) 0 p  monomial (lc f) (lt f)"
    by (simp add: punit.mult_scalar_monomial[symmetric] mult.commute
        mult_scalar_assoc mult_scalar_monomial_monomial term_simps)
  have 2: "monom_mult (- c / lc f) 0 (p  tail f) = - punit.monom_mult (c / lc f) 0 p  tail f"
    by (simp add: times_monomial_left[symmetric] mult_scalar_assoc
        monom_mult_uminus_left mult_scalar_monomial)
  show ?thesis unfolding 1 2 by (fact red_mult_scalar_leading_monomial)
qed

lemma is_red_monomial_iff: "is_red F (monomial c v)  (c  0  (fF. f  0  lt f addst v))"
  by (simp add: is_red_adds_iff)

lemma is_red_monomialI:
  assumes "c  0" and "f  F" and "f  0" and "lt f addst v"
  shows "is_red F (monomial c v)"
  unfolding is_red_monomial_iff using assms by blast

lemma is_red_monomialD:
  assumes "is_red F (monomial c v)"
  shows "c  0"
  using assms unfolding is_red_monomial_iff ..

lemma is_red_monomialE:
  assumes "is_red F (monomial c v)"
  obtains f where "f  F" and "f  0" and "lt f addst v"
  using assms unfolding is_red_monomial_iff by blast

lemma replace_lt_adds_stable_is_red:
  assumes red: "is_red F f" and "q  0" and "lt q addst lt p"
  shows "is_red (insert q (F - {p})) f"
proof -
  from red obtain g v where "g  F" and "g  0" and "v  keys f" and "lt g addst v"
    by (rule is_red_addsE)
  show ?thesis
  proof (cases "g = p")
    case True
    show ?thesis
    proof (rule is_red_addsI)
      show "q  insert q (F - {p})" by simp
    next
      have "lt q addst lt p" by fact
      also have "... addst v" using lt g addst v unfolding True .
      finally show "lt q addst v" .
    qed (fact+)
  next
    case False
    with g  F have "g  insert q (F - {p})" by blast
    from this g  0 v  keys f lt g addst v show ?thesis by (rule is_red_addsI)
  qed
qed
  
lemma conversion_property:
  assumes "is_red {p} f" and "red {r} p q"
  shows "is_red {q} f  is_red {r} f"
proof -
  let ?s = "lp p - lp r"
  from is_red {p} f obtain v where "v  keys f" and "lt p addst v" and "p  0"
    by (rule is_red_addsE, simp)
  from red_indE[OF red {r} p q]
    have "(r  0  lt r addst lt p  q = p - monom_mult (lc p / lc r) ?s r) 
          red {r} (tail p) (q - monomial (lc p) (lt p))" by simp
  thus ?thesis
  proof
    assume "r  0  lt r addst lt p  q = p - monom_mult (lc p / lc r) ?s r"
    hence "r  0" and "lt r addst lt p" by simp_all
    show ?thesis by (intro disjI2, rule is_red_singleton_trans, rule is_red {p} f, fact+)
  next
    assume "red {r} (tail p) (q - monomial (lc p) (lt p))" (is "red _ ?p' ?q'")
    with red_ord have "?q' p ?p'" .
    hence "?p'  0"
      and assm: "(?q' = 0  ((lt ?q') t (lt ?p')  (lt ?q') = (lt ?p')))"
      unfolding ord_strict_p_rec[of ?q' ?p'] by (auto simp add: Let_def lc_def)
    have "lt ?p' t lt p" by (rule lt_tail, fact)
    let ?m = "monomial (lc p) (lt p)"
    from monomial_0D[of "lt p" "lc p"] lc_not_0[OF p  0] have "?m  0" by blast
    have "lt ?m = lt p" by (rule lt_monomial, rule lc_not_0, fact)
    have "q  0  lt q = lt p"
    proof (cases "?q' = 0")
      case True
      hence "q = ?m" by simp
      with ?m  0 lt ?m = lt p show ?thesis by simp
    next
      case False
      from assm show ?thesis
      proof
        assume "(lt ?q') t (lt ?p')  (lt ?q') = (lt ?p')"
        hence "lt ?q' t lt ?p'" by auto
        also have "... t lt p" by fact
        finally have "lt ?q' t lt p" .
        hence "lt ?q' t lt ?m" unfolding lt ?m = lt p .
        from lt_plus_eqI[OF this] lt ?m = lt p have "lt q = lt p" by simp
        show ?thesis
        proof (intro conjI, rule ccontr)
          assume "¬ q  0"
          hence "q = 0" by simp
          hence "?q' = -?m" by simp
          hence "lt ?q' = lt (-?m)" by simp
          also have "... = lt ?m" using lt_uminus .
          finally have "lt ?q' = lt ?m" .
          with lt ?q' t lt ?m show False by simp
        qed (fact)
      next
        assume "?q' = 0"
        with False show ?thesis ..
      qed
    qed
    hence "q  0" and "lt q addst lt p" by (simp_all add: term_simps)
    show ?thesis by (intro disjI1, rule is_red_singleton_trans, rule is_red {p} f, fact+)
  qed
qed
  
lemma replace_red_stable_is_red:
  assumes a1: "is_red F f" and a2: "red (F - {p}) p q"
  shows "is_red (insert q (F - {p})) f" (is "is_red ?F' f")
proof -
  from a1 obtain g where "g  F" and "is_red {g} f" by (rule is_red_singletonI)
  show ?thesis
  proof (cases "g = p")
    case True
    from a2 obtain h where "h  F - {p}" and "red {h} p q" unfolding red_def by auto
    from is_red {g} f have "is_red {p} f" unfolding True .
    have "is_red {q} f  is_red {h} f" by (rule conversion_property, fact+)
    thus ?thesis
    proof
      assume "is_red {q} f"
      show ?thesis
      proof (rule is_red_singletonD)
        show "q  ?F'" by auto
      qed fact
    next
      assume "is_red {h} f"
      show ?thesis
      proof (rule is_red_singletonD)
        from h  F - {p} show "h  ?F'" by simp
      qed fact
    qed
  next
    case False
    show ?thesis
    proof (rule is_red_singletonD)
      from g  F False show "g  ?F'" by blast
    qed fact
  qed
qed

lemma is_red_map_scale:
  assumes "is_red F (c  p)"
  shows "is_red F p"
proof -
  from assms obtain f u where "f  F" and "u  keys (c  p)" and "f  0"
    and a: "lt f addst u" by (rule is_red_addsE)
  from this(2) keys_map_scale_subset have "u  keys p" ..
  with f  F f  0 show ?thesis using a by (rule is_red_addsI)
qed

corollary is_irred_map_scale: "¬ is_red F p  ¬ is_red F (c  p)"
  by (auto dest: is_red_map_scale)

lemma is_red_map_scale_iff: "is_red F (c  p)  (c  0  is_red F p)"
proof (intro iffI conjI notI)
  assume "is_red F (c  p)" and "c = 0"
  thus False by (simp add: irred_0)
next
  assume "is_red F (c  p)"
  thus "is_red F p" by (rule is_red_map_scale)
next
  assume "c  0  is_red F p"
  hence "is_red F (inverse c  c  p)" by (simp add: map_scale_assoc)
  thus "is_red F (c  p)" by (rule is_red_map_scale)
qed

lemma is_red_uminus: "is_red F (- p)  is_red F p"
  by (auto elim!: is_red_addsE simp: keys_uminus intro: is_red_addsI)

lemma is_red_plus:
  assumes "is_red F (p + q)"
  shows "is_red F p  is_red F q"
proof -
  from assms obtain f u where "f  F" and "u  keys (p + q)" and "f  0"
    and a: "lt f addst u" by (rule is_red_addsE)
  from this(2) have "u  keys p  keys q"
    by (meson Poly_Mapping.keys_add subsetD)
  thus ?thesis
  proof
    assume "u  keys p"
    with f  F f  0 have "is_red F p" using a by (rule is_red_addsI)
    thus ?thesis ..
  next
    assume "u  keys q"
    with f  F f  0 have "is_red F q" using a by (rule is_red_addsI)
    thus ?thesis ..
  qed
qed

lemma is_irred_plus: "¬ is_red F p  ¬ is_red F q  ¬ is_red F (p + q)"
  by (auto dest: is_red_plus)

lemma is_red_minus:
  assumes "is_red F (p - q)"
  shows "is_red F p  is_red F q"
proof -
  from assms have "is_red F (p + (- q))" by simp
  hence "is_red F p  is_red F (- q)" by (rule is_red_plus)
  thus ?thesis by (simp only: is_red_uminus)
qed

lemma is_irred_minus: "¬ is_red F p  ¬ is_red F q  ¬ is_red F (p - q)"
  by (auto dest: is_red_minus)

end (* ordered_term *)

subsection ‹Well-foundedness and Termination›

context gd_term
begin

lemma dgrad_set_le_red_single:
  assumes "dickson_grading d" and "red_single p q f t"
  shows "dgrad_set_le d {t} (pp_of_term ` keys p)"
proof (rule dgrad_set_leI, simp)
  have "t adds t + lp f" by simp
  with assms(1) have "d t  d (pp_of_term (t  lt f))"
    by (simp add: term_simps, rule dickson_grading_adds_imp_le)
  moreover from assms(2) have "t  lt f  keys p" by (simp add: in_keys_iff red_single_def)
  ultimately show "vkeys p. d t  d (pp_of_term v)" ..
qed

lemma dgrad_p_set_le_red_single:
  assumes "dickson_grading d" and "red_single p q f t"
  shows "dgrad_p_set_le d {q} {f, p}"
proof -
  let ?f = "monom_mult ((lookup p (t  lt f)) / lc f) t f"
  from assms(2) have "t  lt f  keys p" and q: "q = p - ?f" by (simp_all add: red_single_def in_keys_iff)
  have "dgrad_p_set_le d {q} {p, ?f}" unfolding q by (fact dgrad_p_set_le_minus)
  also have "dgrad_p_set_le d ... {f, p}"
  proof (rule dgrad_p_set_leI_insert)
    from assms(1) have "dgrad_set_le d (pp_of_term ` keys ?f) (insert t (pp_of_term ` keys f))"
      by (rule dgrad_set_le_monom_mult)
    also have "dgrad_set_le d ... (pp_of_term ` (keys f  keys p))"
    proof (rule dgrad_set_leI, simp)
      fix s
      assume "s = t  s  pp_of_term ` keys f"
      thus "ukeys f  keys p. d s  d (pp_of_term u)"
      proof
        assume "s = t"
        from assms have "dgrad_set_le d {s} (pp_of_term ` keys p)" unfolding s = t
          by (rule dgrad_set_le_red_single)
        moreover have "s  {s}" ..
        ultimately obtain s0 where "s0  pp_of_term ` keys p" and "d s  d s0" by (rule dgrad_set_leE)
        from this(1) obtain u where "u  keys p" and "s0 = pp_of_term u" ..
        from this(1) have "u  keys f  keys p" by simp
        with d s  d s0 show ?thesis unfolding s0 = pp_of_term u ..
      next
        assume "s  pp_of_term ` keys f"
        hence "s  pp_of_term ` (keys f  keys p)" by blast
        then obtain u where "u  keys f  keys p" and "s = pp_of_term u" ..
        note this(1)
        moreover have "d s  d s" ..
        ultimately show ?thesis unfolding s = pp_of_term u ..
      qed
    qed
    finally show "dgrad_p_set_le d {?f} {f, p}" by (simp add: dgrad_p_set_le_def Keys_insert)
  next
    show "dgrad_p_set_le d {p} {f, p}" by (rule dgrad_p_set_le_subset, simp)
  qed
  finally show ?thesis .
qed

lemma dgrad_p_set_le_red:
  assumes "dickson_grading d" and "red F p q"
  shows "dgrad_p_set_le d {q} (insert p F)"
proof -
  from assms(2) obtain f t where "f  F" and "red_single p q f t" by (rule red_setE)
  from assms(1) this(2) have "dgrad_p_set_le d {q} {f, p}" by (rule dgrad_p_set_le_red_single)
  also have "dgrad_p_set_le d ... (insert p F)" by (rule dgrad_p_set_le_subset, auto intro: f  F)
  finally show ?thesis .
qed

corollary dgrad_p_set_le_red_rtrancl:
  assumes "dickson_grading d" and "(red F)** p q"
  shows "dgrad_p_set_le d {q} (insert p F)"
  using assms(2)
proof (induct)
  case base
  show ?case by (rule dgrad_p_set_le_subset, simp)
next
  case (step y z)
  from assms(1) step(2) have "dgrad_p_set_le d {z} (insert y F)" by (rule dgrad_p_set_le_red)
  also have "dgrad_p_set_le d ... (insert p F)"
  proof (rule dgrad_p_set_leI_insert)
    show "dgrad_p_set_le d F (insert p F)" by (rule dgrad_p_set_le_subset, blast)
  qed fact
  finally show ?case .
qed

lemma dgrad_p_set_red_single_pp:
  assumes "dickson_grading d" and "p  dgrad_p_set d m" and "red_single p q f t"
  shows "d t  m"
proof -
  from assms(1) assms(3) have "dgrad_set_le d {t} (pp_of_term ` keys p)" by (rule dgrad_set_le_red_single)
  moreover have "t  {t}" ..
  ultimately obtain s where "s  pp_of_term ` keys p" and "d t  d s" by (rule dgrad_set_leE)
  from this(1) obtain u where "u  keys p" and "s = pp_of_term u" ..
  from assms(2) this(1) have "d (pp_of_term u)  m" by (rule dgrad_p_setD)
  with d t  d s show ?thesis unfolding s = pp_of_term u by (rule le_trans)
qed

lemma dgrad_p_set_closed_red_single:
  assumes "dickson_grading d" and "p  dgrad_p_set d m" and "f  dgrad_p_set d m"
    and "red_single p q f t"
  shows "q  dgrad_p_set d m"
proof -
  from dgrad_p_set_le_red_single[OF assms(1, 4)] have "{q}  dgrad_p_set d m"
  proof (rule dgrad_p_set_le_dgrad_p_set)
    from assms(2, 3) show "{f, p}  dgrad_p_set d m" by simp
  qed
  thus ?thesis by simp
qed

lemma dgrad_p_set_closed_red:
  assumes "dickson_grading d" and "F  dgrad_p_set d m" and "p  dgrad_p_set d m" and "red F p q"
  shows "q  dgrad_p_set d m"
proof -
  from assms(4) obtain f t where "f  F" and *: "red_single p q f t" by (rule red_setE)
  from assms(2) this(1) have "f  dgrad_p_set d m" ..
  from assms(1) assms(3) this * show ?thesis by (rule dgrad_p_set_closed_red_single)
qed

lemma dgrad_p_set_closed_red_rtrancl:
  assumes "dickson_grading d" and "F  dgrad_p_set d m" and "p  dgrad_p_set d m" and "(red F)** p q"
  shows "q  dgrad_p_set d m"
  using assms(4)
proof (induct)
  case base
  from assms(3) show ?case .
next
  case (step r q)
  from assms(1) assms(2) step(3) step(2) show "q  dgrad_p_set d m" by (rule dgrad_p_set_closed_red)
qed

lemma red_rtrancl_repE:
  assumes "dickson_grading d" and "G  dgrad_p_set d m" and "finite G" and "p  dgrad_p_set d m"
    and "(red G)** p r"
  obtains q where "p = r + (gG. q g  g)" and "g. q g  punit.dgrad_p_set d m"
    and "g. lt (q g  g) t lt p"
  using assms(5)
proof (induct r arbitrary: thesis)
  case base
  show ?case
  proof (rule base)
    show "p = p + (gG. 0  g)" by simp
  qed (simp_all add: punit.zero_in_dgrad_p_set min_term_min)
next
  case (step r' r)
  from step.hyps(2) obtain g t where "g  G" and rs: "red_single r' r g t" by (rule red_setE)
  from this(2) have "r' = r + monomial (lookup r' (t  lt g) / lc g) t  g"
    by (simp add: red_single_def mult_scalar_monomial)
  moreover define q0 where "q0 = monomial (lookup r' (t  lt g) / lc g) t"
  ultimately have r': "r' = r + q0  g" by simp
  obtain q' where p: "p = r' + (gG. q' g  g)" and 1: "g. q' g  punit.dgrad_p_set d m"
    and 2: "g. lt (q' g  g) t lt p" by (rule step.hyps) blast
  define q where "q = q'(g := q0 + q' g)"
  show ?case
  proof (rule step.prems)
    from assms(3) g  G have "p = (r + q0  g) + (q' g  g + (gG - {g}. q' g  g))"
      by (simp add: p r' sum.remove)
    also have " = r + (q g  g + (gG - {g}. q' g  g))"
      by (simp add: q_def mult_scalar_distrib_right)
    also from refl have "(gG - {g}. q' g  g) = (gG - {g}. q g  g)"
      by (rule sum.cong) (simp add: q_def)
    finally show "p = r + (gG. q g  g)" using assms(3) g  G by (simp only: sum.remove)
  next
    fix g0
    have "q g0  punit.dgrad_p_set d m  lt (q g0  g0) t lt p"
    proof (cases "g0 = g")
      case True
      have eq: "q g = q0 + q' g" by (simp add: q_def)
      show ?thesis unfolding True eq
      proof
        from assms(1, 2, 4) step.hyps(1) have "r'  dgrad_p_set d m"
          by (rule dgrad_p_set_closed_red_rtrancl)
        with assms(1) have "d t  m" using rs by (rule dgrad_p_set_red_single_pp)
        hence "q0  punit.dgrad_p_set d m" by (simp add: q0_def punit.dgrad_p_set_def dgrad_set_def)
        thus "q0 + q' g  punit.dgrad_p_set d m" by (intro punit.dgrad_p_set_closed_plus 1)
      next
        have "lt (q0  g + q' g  g) t ord_term_lin.max (lt (q0  g)) (lt (q' g  g))"
          by (fact lt_plus_le_max)
        also have " t lt p"
        proof (intro ord_term_lin.max.boundedI 2)
          have "lt (q0  g) t t  lt g" by (simp add: q0_def mult_scalar_monomial lt_monom_mult_le)
          also from rs have " t lt r'" by (intro lt_max) (simp add: red_single_def)
          also from step.hyps(1) have " t lt p" by (intro ord_p_lt red_rtrancl_ord)
          finally show "lt (q0  g) t lt p" .
        qed
        finally show "lt ((q0 + q' g)  g) t lt p" by (simp only: mult_scalar_distrib_right)
      qed
    next
      case False
      hence "q g0 = q' g0" by (simp add: q_def)
      thus ?thesis by (simp add: 1 2)
    qed
    thus "q g0  punit.dgrad_p_set d m" and "lt (q g0  g0) t lt p" by simp_all
  qed
qed

lemma is_relation_order_red:
  assumes "dickson_grading d"
  shows "Confluence.relation_order (red F) (≺p) (dgrad_p_set d m)"
proof
  show "wfp_on (≺p) (dgrad_p_set d m)"
  proof (rule wfp_onI_min)
    fix x::"'t 0 'c" and Q
    assume "x  Q" and "Q  dgrad_p_set d m"
    with assms obtain q where "q  Q" and *: "y. y p q  y  Q"
      by (rule ord_p_minimum_dgrad_p_set, auto)
    from this(1) show "zQ. ydgrad_p_set d m. y p z  y  Q"
    proof
      from * show "ydgrad_p_set d m. y p q  y  Q" by auto
    qed
  qed
next
  show "red F  (≺p)¯¯" by (simp add: predicate2I red_ord)
qed (fact ord_strict_p_transitive)

lemma red_wf_dgrad_p_set_aux:
  assumes "dickson_grading d" and "F  dgrad_p_set d m"
  shows "wfp_on (red F)¯¯ (dgrad_p_set d m)"
proof (rule wfp_onI_min)
  fix x::"'t 0 'b" and Q
  assume "x  Q" and "Q  dgrad_p_set d m"
  with assms(1) obtain q where "q  Q" and *: "y. y p q  y  Q"
    by (rule ord_p_minimum_dgrad_p_set, auto)
  from this(1) show "zQ. ydgrad_p_set d m. (red F)¯¯ y z  y  Q"
  proof
    show "ydgrad_p_set d m. (red F)¯¯ y q  y  Q"
    proof (intro ballI impI, simp)
      fix y
      assume "red F q y"
      hence "y p q" by (rule red_ord)
      thus "y  Q" by (rule *)
    qed
  qed
qed

lemma red_wf_dgrad_p_set:
  assumes "dickson_grading d" and "F  dgrad_p_set d m"
  shows "wfP (red F)¯¯"
proof (rule wfI_min[to_pred])
  fix x::"'t 0 'b" and Q
  assume "x  Q"
  from assms(2) obtain n where "m  n" and "x  dgrad_p_set d n" and "F  dgrad_p_set d n"
    by (rule dgrad_p_set_insert)
  let ?Q = "Q  dgrad_p_set d n"
  from assms(1) F  dgrad_p_set d n have "wfp_on (red F)¯¯ (dgrad_p_set d n)"
    by (rule red_wf_dgrad_p_set_aux)
  moreover from x  Q x  dgrad_p_set d n have "x  ?Q" ..
  moreover have "?Q  dgrad_p_set d n" by simp
  ultimately obtain z where "z  ?Q" and *: "y. (red F)¯¯ y z  y  ?Q" by (rule wfp_onE_min) blast
  from this(1) have "z  Q" and "z  dgrad_p_set d n" by simp_all
  from this(1) show "zQ. y. (red F)¯¯ y z  y  Q"
  proof
    show "y. (red F)¯¯ y z  y  Q"
    proof (intro allI impI)
      fix y
      assume "(red F)¯¯ y z"
      hence "red F z y" by simp
      with assms(1) F  dgrad_p_set d n z  dgrad_p_set d n have "y  dgrad_p_set d n"
        by (rule dgrad_p_set_closed_red)
      moreover from (red F)¯¯ y z have "y  ?Q" by (rule *)
      ultimately show "y  Q" by blast
    qed
  qed
qed

lemmas red_wf_finite = red_wf_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]

lemma cbelow_on_monom_mult:
  assumes "dickson_grading d" and "F  dgrad_p_set d m" and "d t  m" and "c  0"
    and "cbelow_on (dgrad_p_set d m) (≺p) z (λa b. red F a b  red F b a) p q"
  shows "cbelow_on (dgrad_p_set d m) (≺p) (monom_mult c t z) (λa b. red F a b  red F b a)
          (monom_mult c t p) (monom_mult c t q)"
  using assms(5)
proof (induct rule: cbelow_on_induct)
  case base
  show ?case unfolding cbelow_on_def
  proof (rule disjI1, intro conjI, fact refl)
    from assms(5) have "p  dgrad_p_set d m" by (rule cbelow_on_first_in)
    with assms(1) assms(3) show "monom_mult c t p  dgrad_p_set d m" by (rule dgrad_p_set_closed_monom_mult)
  next
    from assms(5) have "p p z" by (rule cbelow_on_first_below)
    from this assms(4) show "monom_mult c t p p monom_mult c t z" by (rule ord_strict_p_monom_mult)
  qed
next
  case (step q' q)
  let ?R = "λa b. red F a b  red F b a"
  from step(5) show ?case
  proof
    from assms(1) assms(3) step(3) show "monom_mult c t q  dgrad_p_set d m" by (rule dgrad_p_set_closed_monom_mult)
  next
    from step(2) red_monom_mult[OF _ assms(4)] show "?R (monom_mult c t q') (monom_mult c t q)" by auto
  next
    from step(4) assms(4) show "monom_mult c t q p monom_mult c t z" by (rule ord_strict_p_monom_mult)
  qed
qed

lemma cbelow_on_monom_mult_monomial:
  assumes "c  0"
    and "cbelow_on (dgrad_p_set d m) (≺p) (monomial c' v) (λa b. red F a b  red F b a) p q"
  shows "cbelow_on (dgrad_p_set d m) (≺p) (monomial c (t  v)) (λa b. red F a b  red F b a) p q"
proof -
  have *: "f p monomial c' v  f p monomial c (t  v)" for f
  proof (simp add: ord_strict_p_monomial_iff assms(1), elim conjE disjE, erule disjI1, rule disjI2)
    assume "lt f t v"
    also have "... t t  v" using local.zero_min using splus_mono_left splus_zero by fastforce
    finally show "lt f t t  v" .
  qed
  from assms(2) show ?thesis
  proof (induct rule: cbelow_on_induct)
    case base
    show ?case unfolding cbelow_on_def
    proof (rule disjI1, intro conjI, fact refl)
      from assms(2) show "p  dgrad_p_set d m" by (rule cbelow_on_first_in)
    next
      from assms(2) have "p p monomial c' v" by (rule cbelow_on_first_below)
      thus "p p monomial c (t  v)" by (rule *)
    qed
  next
    case (step q' q)
    let ?R = "λa b. red F a b  red F b a"
    from step(5) step(3) step(2) show ?case
    proof
      from step(4) show "q p monomial c (t  v)" by (rule *)
    qed
  qed
qed

lemma cbelow_on_plus:
  assumes "dickson_grading d" and "F  dgrad_p_set d m" and "r  dgrad_p_set d m"
    and "keys r  keys z = {}"
    and "cbelow_on (dgrad_p_set d m) (≺p) z (λa b. red F a b  red F b a) p q"
  shows "cbelow_on (dgrad_p_set d m) (≺p) (z + r) (λa b. red F a b  red F b a) (p + r) (q + r)"
  using assms(5)
proof (induct rule: cbelow_on_induct)
  case base
  show ?case unfolding cbelow_on_def
  proof (rule disjI1, intro conjI, fact refl)
    from assms(5) have "p  dgrad_p_set d m" by (rule cbelow_on_first_in)
    from this assms(3) show "p + r  dgrad_p_set d m" by (rule dgrad_p_set_closed_plus)
  next
    from assms(5) have "p p z" by (rule cbelow_on_first_below)
    from this assms(4) show "p + r p z + r" by (rule ord_strict_p_plus)
  qed
next
  case (step q' q)
  let ?RS = "λa b. red F a b  red F b a"
  let ?A = "dgrad_p_set d m"
  let ?R = "red F"
  let ?ord = "(≺p)"
  from assms(1) have ro: "relation_order ?R ?ord ?A"
    by (rule is_relation_order_red)
  have dw: "relation.dw_closed ?R ?A"
    by (rule relation.dw_closedI, rule dgrad_p_set_closed_red, rule assms(1), rule assms(2))
  from step(2) have "relation.cs (red F) (q' + r) (q + r)"
  proof
    assume "red F q q'"
    hence "relation.cs (red F) (q + r) (q' + r)" by (rule red_plus_cs)
    thus ?thesis by (rule relation.cs_sym)
  next
    assume "red F q' q"
    thus ?thesis by (rule red_plus_cs)
  qed
  with ro dw have "cbelow_on ?A ?ord (z + r) ?RS (q' + r) (q + r)"
  proof (rule relation_order.cs_implies_cbelow_on)
    from step(1) have "q'  ?A" by (rule cbelow_on_second_in)
    from this assms(3) show "q' + r  ?A" by (rule dgrad_p_set_closed_plus)
  next
    from step(3) assms(3) show "q + r  ?A" by (rule dgrad_p_set_closed_plus)
  next
    from step(1) have "q' p z" by (rule cbelow_on_second_below)
    from this assms(4) show "q' + r p z + r" by (rule ord_strict_p_plus)
  next
    from step(4) assms(4) show "q + r p z + r" by (rule ord_strict_p_plus)
  qed
  with step(5) show ?case by (rule cbelow_on_transitive)
qed

lemma is_full_pmdlI_lt_dgrad_p_set:
  assumes "dickson_grading d" and "B  dgrad_p_set d m"
  assumes "k. k  component_of_term ` Keys (B::('t 0 'b::field) set) 
            (bB. b  0  component_of_term (lt b) = k  lp b = 0)"
  shows "is_full_pmdl B"
proof (rule is_full_pmdlI)
  fix p::"'t 0 'b"
  from assms(1, 2) have "wfP (red B)¯¯" by (rule red_wf_dgrad_p_set)
  moreover assume "component_of_term ` keys p  component_of_term ` Keys B"
  ultimately show "p  pmdl B"
  proof (induct p)
    case (less p)
    show ?case
    proof (cases "p = 0")
      case True
      show ?thesis by (simp add: True pmdl.span_zero)
    next
      case False
      hence "lt p  keys p" by (rule lt_in_keys)
      hence "component_of_term (lt p)  component_of_term ` keys p" by simp
      also have "...  component_of_term ` Keys B" by fact
      finally have "bB. b  0  component_of_term (lt b) = component_of_term (lt p)  lp b = 0"
        by (rule assms(3))
      then obtain b where "b  B" and "b  0" and "component_of_term (lt b) = component_of_term (lt p)"
        and "lp b = 0" by blast
      from this(3, 4) have eq: "lp p  lt b = lt p" by (simp add: splus_def term_of_pair_pair)
      define q where "q = p - monom_mult (lookup p ((lp p)  lt b) / lc b) (lp p) b"
      have "red_single p q b (lp p)"
        by (auto simp: red_single_def b  0 q_def eq lt p  keys p)
      with b  B have "red B p q" by (rule red_setI)
      hence "(red B)¯¯ q p" ..
      moreover have "component_of_term ` keys q  component_of_term ` Keys B"
      proof (rule subset_trans)
        from red B p q show "component_of_term ` keys q  component_of_term ` keys p  component_of_term ` Keys B"
          by (rule components_red_subset)
      next
        from less(2) show "component_of_term ` keys p  component_of_term ` Keys B  component_of_term ` Keys B"
          by blast
      qed
      ultimately have "q  pmdl B" by (rule less.hyps)
      have "q + monom_mult (lookup p ((lp p)  lt b) / lc b) (lp p) b  pmdl B"
        by (rule pmdl.span_add, fact, rule pmdl_closed_monom_mult, rule pmdl.span_base, fact)
      thus ?thesis by (simp add: q_def)
    qed
  qed
qed

lemmas is_full_pmdlI_lt_finite = is_full_pmdlI_lt_dgrad_p_set[OF dickson_grading_dgrad_dummy dgrad_p_set_exhaust_expl]

end (* gd_term *)

subsection ‹Algorithms›

subsubsection ‹Function find_adds›

context ordered_term
begin

primrec find_adds :: "('t 0 'b) list  't  ('t 0 'b::zero) option" where
  "find_adds [] _ = None"|
  "find_adds (f # fs) u = (if f  0  lt f addst u then Some f else find_adds fs u)"

lemma find_adds_SomeD1:
  assumes "find_adds fs u = Some f"
  shows "f  set fs"
  using assms by (induct fs, simp, simp split: if_splits)

lemma find_adds_SomeD2:
  assumes "find_adds fs u = Some f"
  shows "f  0"
  using assms by (induct fs, simp, simp split: if_splits)

lemma find_adds_SomeD3:
  assumes "find_adds fs u = Some f"
  shows "lt f addst u"
  using assms by (induct fs, simp, simp split: if_splits)

lemma find_adds_NoneE:
  assumes "find_adds fs u = None" and "f  set fs"
  assumes "f = 0  thesis" and "f  0  ¬ lt f addst u  thesis"
  shows thesis
  using assms
proof (induct fs arbitrary: thesis)
  case Nil
  from Nil(2) show ?case by simp
next
  case (Cons a fs)
  from Cons(2) have 1: "a = 0  ¬ lt a addst u" and 2: "find_adds fs u = None"
    by (simp_all split: if_splits)
  from Cons(3) have "f = a  f  set fs" by simp
  thus ?case
  proof
    assume "f = a"
    show ?thesis
    proof (cases "a = 0")
      case True
      show ?thesis by (rule Cons(4), simp add: f = a True)
    next
      case False
      with 1 have *: "¬ lt a addst u" by simp
      show ?thesis by (rule Cons(5), simp_all add: f = a * False)
    qed
  next
    assume "f  set fs"
    with 2 show ?thesis
    proof (rule Cons(1))
      assume "f = 0"
      thus ?thesis by (rule Cons(4))
    next
      assume "f  0" and "¬ lt f addst u"
      thus ?thesis by (rule Cons(5))
    qed
  qed
qed

lemma find_adds_SomeD_red_single:
  assumes "p  0" and "find_adds fs (lt p) = Some f"
  shows "red_single p (tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f)) f (lp p - lp f)"
proof -
  let ?f = "monom_mult (lc p / lc f) (lp p - lp f) f"
  from assms(2) have "f  0" and "lt f addst lt p" by (rule find_adds_SomeD2, rule find_adds_SomeD3)
  from this(2) have eq: "(lp p - lp f)  lt f = lt p"
    by (simp add: adds_minus_splus adds_term_def term_of_pair_pair)
  from assms(1) have "lc p  0" by (rule lc_not_0)
  moreover from f  0 have "lc f  0" by (rule lc_not_0)
  ultimately have "lc p / lc f  0" by simp
  hence "lt ?f = (lp p - lp f)  lt f" by (simp add: lt_monom_mult f  0)
  hence lt_f: "lt ?f = lt p" by (simp only: eq)
  have "lookup ?f (lt p) = lookup ?f ((lp p - lp f)  lt f)" by (simp only: eq)
  also have "... = (lc p / lc f) * lookup f (lt f)" by (rule lookup_monom_mult_plus)
  also from lc f  0 have "... = lookup p (lt p)" by (simp add: lc_def)
  finally have lc_f: "lookup ?f (lt p) = lookup p (lt p)" .
  have "red_single p (p - ?f) f (lp p - lp f)"
    by (auto simp: red_single_def eq lc_def f  0 lt_in_keys assms(1))
  moreover have "p - ?f = tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f)"
    by (rule poly_mapping_eqI,
        simp add: tail_monom_mult[symmetric] lookup_minus lookup_tail_2 lt_f lc_f split: if_split)
  ultimately show ?thesis by simp
qed

lemma find_adds_SomeD_red:
  assumes "p  0" and "find_adds fs (lt p) = Some f"
  shows "red (set fs) p (tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f))"
proof (rule red_setI)
  from assms(2) show "f  set fs" by (rule find_adds_SomeD1)
next
  from assms show "red_single p (tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f)) f (lp p - lp f)"
    by (rule find_adds_SomeD_red_single)
qed

end (* ordered_term *)

subsubsection ‹Function trd›

context gd_term
begin

definition trd_term :: "('a  nat)  ((('t 0 'b::field) list × ('t 0 'b) × ('t 0 'b)) ×
                                        (('t 0 'b) list × ('t 0 'b) × ('t 0 'b))) set"
  where "trd_term d = {(x, y). dgrad_p_set_le d (set (fst (snd x) # fst x)) (set (fst (snd y) # fst y))  fst (snd x) p fst (snd y)}"

lemma trd_term_wf:
  assumes "dickson_grading d"
  shows "wf (trd_term d)"
proof (rule wfI_min)
  fix x :: "('t 0 'b::field) list × ('t 0 'b) × ('t 0 'b)" and Q
  assume "x  Q"
  let ?A = "set (fst (snd x) # fst x)"
  have "finite ?A" ..
  then obtain m where A: "?A  dgrad_p_set d m" by (rule dgrad_p_set_exhaust)
  let ?B = "dgrad_p_set d m"
  let ?Q = "{q  Q. set (fst (snd q) # fst q)  ?B}"
  note assms
  moreover have "fst (snd x)  fst ` snd ` ?Q"
    by (rule, fact refl, rule, fact refl, simp only: mem_Collect_eq A x  Q)
  moreover have "fst ` snd ` ?Q  ?B" by auto
  ultimately obtain z0 where "z0  fst ` snd ` ?Q"
    and *: "y. y p z0  y  fst ` snd ` ?Q" by (rule ord_p_minimum_dgrad_p_set, blast)
  from this(1) obtain z where "z  {q  Q. set (fst (snd q) # fst q)  ?B}" and z0: "z0 = fst (snd z)"
    by fastforce
  from this(1) have "z  Q" and a: "set (fst (snd z) # fst z)  ?B" by simp_all
  from this(1) show "zQ. y. (y, z)  trd_term d  y  Q"
  proof
    show "y. (y, z)  trd_term d  y  Q"
    proof (intro allI impI)
      fix y
      assume "(y, z)  trd_term d"
      hence b: "dgrad_p_set_le d (set (fst (snd y) # fst y)) (set (fst (snd z) # fst z))" and "fst (snd y) p z0"
        by (simp_all add: trd_term_def z0)
      from this(2) have "fst (snd y)  fst ` snd ` ?Q" by (rule *)
      hence "y  Q  ¬ set (fst (snd y) # fst y)  ?B" by auto
      moreover from b a have "set (fst (snd y) # fst y)  ?B" by (rule dgrad_p_set_le_dgrad_p_set)
      ultimately show "y  Q" by simp
    qed
  qed
qed

function trd_aux :: "('t 0 'b) list  ('t 0 'b)  ('t 0 'b)  ('t 0 'b::field)" where
  "trd_aux fs p r =
    (if p = 0 then
      r
    else
      case find_adds fs (lt p) of
        None    trd_aux fs (tail p) (r + monomial (lc p) (lt p))
      | Some f  trd_aux fs (tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f)) r
    )"
  by auto
termination proof -
  from ex_dgrad obtain d::"'a  nat" where dg: "dickson_grading d" ..
  let ?R = "trd_term d"
  show ?thesis
  proof (rule, rule trd_term_wf, fact)
    fix fs and p r::"'t 0 'b"
    assume "p  0"
    show "((fs, tail p, r + monomial (lc p) (lt p)), fs, p, r)  trd_term d"
    proof (simp add: trd_term_def, rule)
      show "dgrad_p_set_le d (insert (tail p) (set fs)) (insert p (set fs))"
      proof (rule dgrad_p_set_leI_insert_keys, rule dgrad_p_set_le_subset, rule subset_insertI,
            rule dgrad_set_le_subset, simp add: Keys_insert image_Un)
        have "keys (tail p)  keys p" by (auto simp: keys_tail)
        hence "pp_of_term ` keys (tail p)  pp_of_term ` keys p" by (rule image_mono)
        thus "pp_of_term ` keys (tail p)  pp_of_term ` keys p  pp_of_term ` Keys (set fs)" by blast
      qed
    next
      from p  0 show "tail p p p" by (rule tail_ord_p)
    qed
  next
    fix fs::"('t 0 'b) list" and p r f ::"'t 0 'b"
    assume "p  0" and "find_adds fs (lt p) = Some f"
    hence "red (set fs) p (tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f))"
      (is "red _ p ?q") by (rule find_adds_SomeD_red)
    show "((fs, ?q, r), fs, p, r)  trd_term d"
      by (simp add: trd_term_def, rule, rule dgrad_p_set_leI_insert, rule dgrad_p_set_le_subset, rule subset_insertI,
            rule dgrad_p_set_le_red, fact dg, fact red (set fs) p ?q, rule red_ord, fact)
  qed
qed

definition trd :: "('t 0 'b::field) list  ('t 0 'b)  ('t 0 'b)"
  where "trd fs p = trd_aux fs p 0"

lemma trd_aux_red_rtrancl: "(red (set fs))** p (trd_aux fs p r - r)"
proof (induct fs p r rule: trd_aux.induct)
  case (1 fs p r)
  show ?case
  proof (simp, split option.split, intro conjI impI allI)
    assume "p  0" and "find_adds fs (lt p) = None"
    hence "(red (set fs))** (tail p) (trd_aux fs (tail p) (r + monomial (lc p) (lt p)) - (r + monomial (lc p) (lt p)))"
      by (rule 1(1))
    hence "(red (set fs))** (tail p + monomial (lc p) (lt p))
              (trd_aux fs (tail p) (r + monomial (lc p) (lt p)) - (r + monomial (lc p) (lt p)) + monomial (lc p ) (lt p))"
    proof (rule red_rtrancl_plus_higher)
      fix u v
      assume "u  keys (tail p)"
      assume "v  keys (monomial (lc p) (lt p))"
      also have "...  {lt p}" by (simp add: keys_monomial)
      finally have "v = lt p" by simp
      from u  keys (tail p) show "u t v" unfolding v = lt p by (rule keys_tail_less_lt)
    qed
    thus "(red (set fs))** p (trd_aux fs (tail p) (r + monomial (lc p) (lt p)) - r)"
      by (simp only: leading_monomial_tail[symmetric] add.commute[of _ "monomial (lc p) (lt p)"], simp)
  next
    fix f
    assume "p  0" and "find_adds fs (lt p) = Some f"
    hence "(red (set fs))** (tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f))
                    (trd_aux fs (tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f)) r - r)"
      and *: "red (set fs) p (tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f))"
      by (rule 1(2), rule find_adds_SomeD_red)
    let ?q = "tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f)"
    from * have "(red (set fs))** p ?q" ..
    moreover have "(red (set fs))** ?q (trd_aux fs ?q r - r)" by fact
    ultimately show "(red (set fs))** p (trd_aux fs ?q r - r)" by (rule rtranclp_trans)
  qed
qed

corollary trd_red_rtrancl: "(red (set fs))** p (trd fs p)"
proof -
  have "(red (set fs))** p (trd fs p - 0)" unfolding trd_def by (rule trd_aux_red_rtrancl)
  thus ?thesis by simp
qed

lemma trd_aux_irred:
  assumes "¬ is_red (set fs) r"
  shows "¬ is_red (set fs) (trd_aux fs p r)"
  using assms
proof (induct fs p r rule: trd_aux.induct)
  case (1 fs p r)
  show ?case
  proof (simp add: 1(3), split option.split, intro impI conjI allI)
    assume "p  0" and *: "find_adds fs (lt p) = None"
    thus "¬ is_red (set fs) (trd_aux fs (tail p) (r + monomial (lc p) (lt p)))"
    proof (rule 1(1))
      show "¬ is_red (set fs) (r + monomial (lc p) (lt p))"
      proof
        assume "is_red (set fs) (r + monomial (lc p) (lt p))"
        then obtain f u where "f  set fs" and "f  0" and "u  keys (r + monomial (lc p) (lt p))"
          and "lt f addst u" by (rule is_red_addsE)
        note this(3)
        also have "keys (r + monomial (lc p) (lt p))  keys r  keys (monomial (lc p) (lt p))"
          by (rule Poly_Mapping.keys_add)
        also have "...  insert (lt p) (keys r)" by auto
        finally show False
        proof
          assume "u = lt p"
          from * f  set fs show ?thesis
          proof (rule find_adds_NoneE)
            assume "f = 0"
            with f  0 show ?thesis ..
          next
            assume "¬ lt f addst lt p"
            from this lt f addst u show ?thesis unfolding u = lt p ..
          qed
        next
          assume "u  keys r"
          from f  set fs f  0 this lt f addst u have "is_red (set fs) r" by (rule is_red_addsI)
          with 1(3) show ?thesis ..
        qed
      qed
    qed
  next
    fix f
    assume "p  0" and "find_adds fs (lt p) = Some f"
    from this 1(3) show "¬ is_red (set fs) (trd_aux fs (tail p - monom_mult (lc p / lc f) (lp p - lp f) (tail f)) r)" 
      by (rule 1(2))
  qed
qed

corollary trd_irred: "¬ is_red (set fs) (trd fs p)"
  unfolding trd_def using irred_0 by (rule trd_aux_irred)

lemma trd_in_pmdl: "p - (trd fs p)  pmdl (set fs)"
  using trd_red_rtrancl by (rule red_rtranclp_diff_in_pmdl)

lemma pmdl_closed_trd:
  assumes "p  pmdl B" and "set fs  pmdl B"
  shows "(trd fs p)  pmdl B"
proof -
  from assms(2) have "pmdl (set fs)  pmdl B" by (rule pmdl.span_subset_spanI)
  with trd_in_pmdl have "p - trd fs p  pmdl B" ..
  with assms(1) have "p - (p - trd fs p)  pmdl B" by (rule pmdl.span_diff)
  thus ?thesis by simp
qed

end (* gd_term *)

end (* theory *)