Quelle  F4.thy

(* Author: Alexander Maletzky *)

section ‹Faug\`ere's F4 Algorithm›

theory F4
  imports Macaulay_Matrix Algorithm_Schema
begin

text ‹This theory implements Faug\`ere's F4 algorithm based on @{const gd_term.gb_schema_direct}.›

subsection ‹Symbolic Preprocessing›

context gd_term
begin

definition sym_preproc_aux_term1 :: "('a ==> nat) ==> ((('t ==>₀ 'b) list × 't list × 't list × ('t ==>₀ 'b) list) ×
                                                (('t ==>₀ 'b) list × 't list × 't list × ('t ==>₀ 'b) list)) set"
  where "sym_preproc_aux_term1 d =
            {((gs1, ks1, ts1, fs1), (gs2::('t ==>₀ 'b) list, ks2, ts2, fs2)). ∃t2∈set ts2. ∀t1∈set ts1. t1 ≺_t t2}"

definition sym_preproc_aux_term2 :: "('a ==> nat) ==> ((('t ==>₀ 'b::zero) list × 't list × 't list × ('t ==>₀ 'b) list) ×
                                                (('t ==>₀ 'b) list × 't list × 't list × ('t ==>₀ 'b) list)) set"
  where "sym_preproc_aux_term2 d =
            {((gs1, ks1, ts1, fs1), (gs2::('t ==>₀ 'b) list, ks2, ts2, fs2)). gs1 = gs2 ∧
                                              dgrad_set_le d (pp_of_term ` set ts1) (pp_of_term ` (Keys (set gs2) ∪ set ts2))}"

definition sym_preproc_aux_term
  where "sym_preproc_aux_term d = sym_preproc_aux_term1 d ∩ sym_preproc_aux_term2 d"

lemma wfp_on_ord_term_strict:
  assumes "dickson_grading d"
  shows "wfp_on (≺_t) (pp_of_term -` dgrad_set d m)"
proof (rule wfp_onI_min)
  fix x Q
  assume "x ∈ Q" and "Q ⊆ pp_of_term -` dgrad_set d m"
  from wf_dickson_less_v[OF assms, of m] ‹x ∈ Q› obtain z
    where "z ∈ Q" and *: "∧y. dickson_less_v d m y z ==> y ∉ Q" by (rule wfE_min[to_pred], blast)
  from this(1) ‹Q ⊆ pp_of_term -` dgrad_set d m› have "z ∈ pp_of_term -` dgrad_set d m" ..
  show "∃z∈Q. ∀y ∈ pp_of_term -` dgrad_set d m. y ≺<sub>t</sub> z ⟶ y ∉ Q"
  proof (intro bexI ballI impI, rule *)
    fix y
    assume "y ∈ pp_of_term -` dgrad_set d m" and "y ≺_t z"
    from this(1) ‹z ∈ pp_of_term -` dgrad_set d m› have "d (pp_of_term y) ≤ m" and "d (pp_of_term z) ≤ m"
      by (simp_all add: dgrad_set_def)
    thus "dickson_less_v d m y z" using ‹y ≺_t z› by (rule dickson_less_vI)
  qed fact
qed

lemma sym_preproc_aux_term1_wf_on:
  assumes "dickson_grading d"
  shows "wfp_on (λx y. (x, y) ∈ sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) ⊆ pp_of_term -` dgrad_set d m}"
proof (rule wfp_onI_min)
  let ?B = "pp_of_term -` dgrad_set d m"
  let ?A = "{x::(('t ==>₀ 'b) list × 't list × 't list × ('t ==>₀ 'b) list). set (fst (snd (snd x))) ⊆ ?B}"
  have A_sub_Pow: "set ` fst ` snd ` snd ` ?A ⊆ Pow ?B" by auto
  fix x Q
  assume "x ∈ Q" and "Q ⊆ ?A"
  let ?Q = "{ord_term_lin.Max (set (fst (snd (snd q)))) | q. q ∈ Q ∧ fst (snd (snd q)) ≠ []}"
  show "∃z∈Q. ∀y∈{x. set (fst (snd (snd x))) ⊆ ?B}. (y, z) ∈ sym_preproc_aux_term1 d ⟶ y ∉ Q"
  proof (cases "∃z∈Q. fst (snd (snd z)) = []")
    case True
    then obtain z where "z ∈ Q" and "fst (snd (snd z)) = []" ..
    show ?thesis
    proof (intro bexI ballI impI)
      fix y
      assume "(y, z) ∈ sym_preproc_aux_term1 d"
      then obtain t where "t ∈ set (fst (snd (snd z)))" unfolding sym_preproc_aux_term1_def by auto
      with ‹fst (snd (snd z)) = []› show "y ∉ Q" by simp
    qed fact
  next
    case False
    hence *: "q ∈ Q ==> fst (snd (snd q)) ≠ []" for q by blast
    with ‹x ∈ Q› have "fst (snd (snd x)) ≠ []" by simp
    from assms have "wfp_on (≺_t) ?B" by (rule wfp_on_ord_term_strict)
    moreover from ‹x ∈ Q› ‹fst (snd (snd x)) ≠ []›
    have "ord_term_lin.Max (set (fst (snd (snd x)))) ∈ ?Q" by blast
    moreover have "?Q ⊆ ?B"
    proof (rule, simp, elim exE conjE, simp)
      fix a b c d0
      assume "(a, b, c, d0) ∈ Q" and "c ≠ []"
      from this(1) ‹Q ⊆ ?A› have "(a, b, c, d0) ∈ ?A" ..
      hence "pp_of_term ` set c ⊆ dgrad_set d m" by auto
      moreover have "pp_of_term (ord_term_lin.Max (set c)) ∈ pp_of_term ` set c"
      proof
        from ‹c ≠ []› show "ord_term_lin.Max (set c) ∈ set c" by simp
      qed (fact refl)
      ultimately show "pp_of_term (ord_term_lin.Max (set c)) ∈ dgrad_set d m" ..
    qed
    ultimately obtain t where "t ∈ ?Q" and min: "∧s. s ≺_t t ==> s ∉ ?Q" by (rule wfp_onE_min) blast
    from this(1) obtain z where "z ∈ Q" and "fst (snd (snd z)) ≠ []"
      and t: "t = ord_term_lin.Max (set (fst (snd (snd z))))" by blast
    show ?thesis
    proof (intro bexI ballI impI, rule)
      fix y
      assume "y ∈ ?A" and "(y, z) ∈ sym_preproc_aux_term1 d" and "y ∈ Q"
      from this(2) obtain t' where "t' ∈ set (fst (snd (snd z)))"
        and **: "∧s. s ∈ set (fst (snd (snd y))) ==> s ≺_t t'"
        unfolding sym_preproc_aux_term1_def by auto
      from ‹y ∈ Q› have "fst (snd (snd y)) ≠ []" by (rule *)
      with ‹y ∈ Q› have "ord_term_lin.Max (set (fst (snd (snd y)))) ∈ ?Q" (is "?s ∈ _")
        by blast
      from ‹fst (snd (snd y)) ≠ []› have "?s ∈ set (fst (snd (snd y)))" by simp
      hence "?s ≺_t t'" by (rule **)
      also from ‹t' ∈ set (fst (snd (snd z)))› have "t' ⪯_t t" unfolding t
        using ‹fst (snd (snd z)) ≠ []› by simp
      finally have "?s ∉ ?Q" by (rule min)
      from this ‹?s ∈ ?Q› show False ..
    qed fact
  qed
qed

lemma sym_preproc_aux_term_wf:
  assumes "dickson_grading d"
  shows "wf (sym_preproc_aux_term d)"
proof (rule wfI_min)
  fix x::"(('t ==>₀ 'b) list × 't list × 't list × ('t ==>₀ 'b) list)" and Q
  assume "x ∈ Q"
  let ?A = "Keys (set (fst x)) ∪ set (fst (snd (snd x)))"
  have "finite ?A" by (simp add: finite_Keys)
  hence "finite (pp_of_term ` ?A)" by (rule finite_imageI)
  then obtain m where "pp_of_term ` ?A ⊆ dgrad_set d m" by (rule dgrad_set_exhaust)
  hence A: "?A ⊆ pp_of_term -` dgrad_set d m" by blast
  let ?B = "pp_of_term -` dgrad_set d m"
  let ?Q = "{q ∈ Q. Keys (set (fst q)) ∪ set (fst (snd (snd q))) ⊆ ?B}"
  from assms have "wfp_on (λx y. (x, y) ∈ sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) ⊆ ?B}"
    by (rule sym_preproc_aux_term1_wf_on)
  moreover from ‹x ∈ Q› A have "x ∈ ?Q" by simp
  moreover have "?Q ⊆ {x. set (fst (snd (snd x))) ⊆ ?B}" by auto
  ultimately obtain z where "z ∈ ?Q"
    and *: "∧y. (y, z) ∈ sym_preproc_aux_term1 d ==> y ∉ ?Q" by (rule wfp_onE_min) blast
  from this(1) have "z ∈ Q" and "Keys (set (fst z)) ∪ set (fst (snd (snd z))) ⊆ ?B" by simp_all
  from this(2) have a: "pp_of_term ` (Keys (set (fst z)) ∪ set (fst (snd (snd z)))) ⊆ dgrad_set d m"
    by blast
  show "∃z∈Q. ∀y. (y, z) ∈ sym_preproc_aux_term d ⟶ y ∉ Q"
  proof (intro bexI allI impI)
    fix y
    assume "(y, z) ∈ sym_preproc_aux_term d"
    hence "(y, z) ∈ sym_preproc_aux_term1 d" and "(y, z) ∈ sym_preproc_aux_term2 d"
      by (simp_all add: sym_preproc_aux_term_def)
    from this(2) have "fst y = fst z"
      and "dgrad_set_le d (pp_of_term ` set (fst (snd (snd y)))) (pp_of_term ` (Keys (set (fst z)) ∪ set (fst (snd (snd z)))))"
      by (auto simp add: sym_preproc_aux_term2_def)
    from this(2) a have "pp_of_term ` (set (fst (snd (snd y)))) ⊆ dgrad_set d m"
      by (rule dgrad_set_le_dgrad_set)
    hence "Keys (set (fst y)) ∪ set (fst (snd (snd y))) ⊆ ?B"
      using a by (auto simp add: ‹fst y = fst z›)
    moreover from ‹(y, z) ∈ sym_preproc_aux_term1 d› have "y ∉ ?Q" by (rule *)
    ultimately show "y ∉ Q" by simp
  qed fact
qed

primrec sym_preproc_addnew :: "('t ==>₀ 'b::semiring_1) list ==> 't list ==> ('t ==>₀ 'b) list ==> 't ==>
                              ('t list × ('t ==>₀ 'b) list)" where
  "sym_preproc_addnew [] vs fs _ = (vs, fs)"|
  "sym_preproc_addnew (g # gs) vs fs v =
    (if lt g adds_t v then
      (let f = monom_mult 1 (pp_of_term v - lp g) g in
        sym_preproc_addnew gs (merge_wrt (≻_t) vs (keys_to_list (tail f))) (insert_list f fs) v
      )
    else
      sym_preproc_addnew gs vs fs v
    )"

lemma fst_sym_preproc_addnew_less:
  assumes "∧u. u ∈ set vs ==> u ≺_t v"
    and "u ∈ set (fst (sym_preproc_addnew gs vs fs v))"
  shows "u ≺_t v"
  using assms
proof (induct gs arbitrary: fs vs)
  case Nil
  from Nil(2) have "u ∈ set vs" by simp
  thus ?case by (rule Nil(1))
next
  case (Cons g gs)
  from Cons(3) show ?case
  proof (simp add: Let_def split: if_splits)
    let ?t = "pp_of_term v - lp g"
    assume "lt g adds_t v"
    assume "u ∈ set (fst (sym_preproc_addnew gs
                                (merge_wrt (≻_t) vs (keys_to_list (tail (monom_mult 1 ?t g))))
                                (insert_list (monom_mult 1 ?t g) fs) v))"
    with _ show ?thesis
    proof (rule Cons(1))
      fix u
      assume "u ∈ set (merge_wrt (≻_t) vs (keys_to_list (tail (monom_mult 1 ?t g))))"
      hence "u ∈ set vs ∨ u ∈ keys (tail (monom_mult 1 ?t g))"
        by (simp add: set_merge_wrt keys_to_list_def set_pps_to_list)
      thus "u ≺_t v"
      proof
        assume "u ∈ set vs"
        thus ?thesis by (rule Cons(2))
      next
        assume "u ∈ keys (tail (monom_mult 1 ?t g))"
        hence "u ≺_t lt (monom_mult 1 ?t g)" by (rule keys_tail_less_lt)
        also have "... ⪯_t ?t ⊕ lt g" by (rule lt_monom_mult_le)
        also from ‹lt g adds_t v› have "... = v"
          by (metis add_diff_cancel_right' adds_termE pp_of_term_splus)
        finally show ?thesis .
      qed
    qed
  next
    assume "u ∈ set (fst (sym_preproc_addnew gs vs fs v))"
    with Cons(2) show ?thesis by (rule Cons(1))
  qed
qed

lemma fst_sym_preproc_addnew_dgrad_set_le:
  assumes "dickson_grading d"
  shows "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (pp_of_term ` (Keys (set gs) ∪ insert v (set vs)))"
proof (induct gs arbitrary: fs vs)
  case Nil
  show ?case by (auto intro: dgrad_set_le_subset)
next
  case (Cons g gs)
  show ?case
  proof (simp add: Let_def, intro conjI impI)
    assume "lt g adds_t v"
    let ?t = "pp_of_term v - lp g"
    let ?vs = "merge_wrt (≻_t) vs (keys_to_list (tail (monom_mult 1 ?t g)))"
    let ?fs = "insert_list (monom_mult 1 ?t g) fs"
    from Cons have "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)))
                                    (pp_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs)))"
    proof (rule dgrad_set_le_trans)
      show "dgrad_set_le d (pp_of_term ` (Keys (set gs) ∪ insert v (set ?vs)))
                            (pp_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs)))"
        unfolding dgrad_set_le_def set_merge_wrt set_keys_to_list
      proof (intro ballI)
        fix s
        assume "s ∈ pp_of_term ` (Keys (set gs) ∪ insert v (set vs ∪ keys (tail (monom_mult 1 ?t g))))"
        hence "s ∈ pp_of_term ` (Keys (set gs) ∪ insert v (set vs)) ∪ pp_of_term ` keys (tail (monom_mult 1 ?t g))"
          by auto
        thus "∃t ∈ pp_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs)). d s ≤ d t"
        proof
          assume "s ∈ pp_of_term ` (Keys (set gs) ∪ insert v (set vs))"
          thus ?thesis by (auto simp add: Keys_insert)
        next
          assume "s ∈ pp_of_term ` keys (tail (monom_mult 1 ?t g))"
          hence "s ∈ pp_of_term ` keys (monom_mult 1 ?t g)" by (auto simp add: keys_tail)
          from this keys_monom_mult_subset have "s ∈ pp_of_term ` (⊕) ?t ` keys g" by blast
          then obtain u where "u ∈ keys g" and s: "s = pp_of_term (?t ⊕ u)" by blast
          have "d s = d ?t ∨ d s = d (pp_of_term u)" unfolding s pp_of_term_splus
            using dickson_gradingD1[OF assms] by auto
          thus ?thesis
          proof
            from ‹lt g adds<sub>t</sub> v› have "lp g adds pp_of_term v" by (simp add: adds_term_def)
            assume "d s = d ?t"
            also from assms ‹lp g adds pp_of_term v› have "... ≤ d (pp_of_term v)"
              by (rule dickson_grading_minus)
            finally show ?thesis by blast
          next
            assume "d s = d (pp_of_term u)"
            moreover from ‹u ∈ keys g› have "u ∈ Keys (insert g (set gs))" by (simp add: Keys_insert)
            ultimately show ?thesis by auto
          qed
        qed
      qed
    qed
    thus "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)))
                        (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) ∪ set vs)))"
      by simp
  next
    from Cons show "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v)))
                           (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) ∪ set vs)))"
    proof (rule dgrad_set_le_trans)
      show "dgrad_set_le d (pp_of_term ` (Keys (set gs) ∪ insert v (set vs)))
                          (insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) ∪ set vs)))"
        by (rule dgrad_set_le_subset, auto simp add: Keys_def)
    qed
  qed
qed

lemma components_fst_sym_preproc_addnew_subset:
  "component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) ⊆ component_of_term ` (Keys (set gs) ∪ insert v (set vs))"
proof (induct gs arbitrary: fs vs)
  case Nil
  show ?case by (auto intro: dgrad_set_le_subset)
next
  case (Cons g gs)
  show ?case
  proof (simp add: Let_def, intro conjI impI)
    assume "lt g adds_t v"
    let ?t = "pp_of_term v - lp g"
    let ?vs = "merge_wrt (≻_t) vs (keys_to_list (tail (monom_mult 1 ?t g)))"
    let ?fs = "insert_list (monom_mult 1 ?t g) fs"
    from Cons have "component_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)) ⊆
                     component_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs))"
    proof (rule subset_trans)
      show "component_of_term ` (Keys (set gs) ∪ insert v (set ?vs)) ⊆
             component_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs))"
        unfolding set_merge_wrt set_keys_to_list
      proof
        fix k
        assume "k ∈ component_of_term ` (Keys (set gs) ∪ insert v (set vs ∪ keys (tail (monom_mult 1 ?t g))))"
        hence "k ∈ component_of_term ` (Keys (set gs) ∪ insert v (set vs)) ∪ component_of_term ` keys (tail (monom_mult 1 ?t g))"
          by auto
        thus "k ∈ component_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs))"
        proof
          assume "k ∈ component_of_term ` (Keys (set gs) ∪ insert v (set vs))"
          thus ?thesis by (auto simp add: Keys_insert)
        next
          assume "k ∈ component_of_term ` keys (tail (monom_mult 1 ?t g))"
          hence "k ∈ component_of_term ` keys (monom_mult 1 ?t g)" by (auto simp add: keys_tail)
          from this keys_monom_mult_subset have "k ∈ component_of_term ` (⊕) ?t ` keys g" by blast
          also have "... ⊆ component_of_term ` keys g" using component_of_term_splus by fastforce
          finally show ?thesis by (simp add: image_Un Keys_insert)
        qed
      qed
    qed
    thus "component_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)) ⊆
           insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) ∪ set vs))"
      by simp
  next
    from Cons show "component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) ⊆
                insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) ∪ set vs))"
    proof (rule subset_trans)
      show "component_of_term ` (Keys (set gs) ∪ insert v (set vs)) ⊆
             insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) ∪ set vs))"
        by (auto simp add: Keys_def)
    qed
  qed
qed

lemma fst_sym_preproc_addnew_superset: "set vs ⊆ set (fst (sym_preproc_addnew gs vs fs v))"
proof (induct gs arbitrary: vs fs)
  case Nil
  show ?case by simp
next
  case (Cons g gs)
  show ?case
  proof (simp add: Let_def, intro conjI impI)
    let ?t = "pp_of_term v - lp g"
    define f where "f = monom_mult 1 ?t g"
    have "set vs ⊆ set (merge_wrt (≻_t) vs (keys_to_list (tail f)))" by (auto simp add: set_merge_wrt)
    thus "set vs ⊆ set (fst (sym_preproc_addnew gs
                              (merge_wrt (≻_t) vs (keys_to_list (tail f))) (insert_list f fs) v))"
      using Cons by (rule subset_trans)
  next
    show "set vs ⊆ set (fst (sym_preproc_addnew gs vs fs v))" by (fact Cons)
  qed
qed

lemma snd_sym_preproc_addnew_superset: "set fs ⊆ set (snd (sym_preproc_addnew gs vs fs v))"
proof (induct gs arbitrary: vs fs)
  case Nil
  show ?case by simp
next
  case (Cons g gs)
  show ?case
  proof (simp add: Let_def, intro conjI impI)
    let ?t = "pp_of_term v - lp g"
    define f where "f = monom_mult 1 ?t g"
    have "set fs ⊆ set (insert_list f fs)" by (auto simp add: set_insert_list)
    thus "set fs ⊆ set (snd (sym_preproc_addnew gs
                              (merge_wrt (≻_t) vs (keys_to_list (tail f))) (insert_list f fs) v))"
      using Cons by (rule subset_trans)
  next
    show "set fs ⊆ set (snd (sym_preproc_addnew gs vs fs v))" by (fact Cons)
  qed
qed

lemma in_snd_sym_preproc_addnewE:
  assumes "p ∈ set (snd (sym_preproc_addnew gs vs fs v))"
  assumes 1: "p ∈ set fs ==> thesis"
  assumes 2: "∧g s. g ∈ set gs ==> p = monom_mult 1 s g ==> thesis"
  shows thesis
  using assms
proof (induct gs arbitrary: vs fs thesis)
  case Nil
  from Nil(1) have "p ∈ set fs" by simp
  thus ?case by (rule Nil(2))
next
  case (Cons g gs)
  from Cons(2) show ?case
  proof (simp add: Let_def split: if_splits)
    define f where "f = monom_mult 1 (pp_of_term v - lp g) g"
    define ts' where "ts' = merge_wrt (≻_t) vs (keys_to_list (tail f))"
    define fs' where "fs' = insert_list f fs"
    assume "p ∈ set (snd (sym_preproc_addnew gs ts' fs' v))"
    thus ?thesis
    proof (rule Cons(1))
      assume "p ∈ set fs'"
      hence "p = f ∨ p ∈ set fs" by (simp add: fs'_def set_insert_list)
      thus ?thesis
      proof
        assume "p = f"
        have "g ∈ set (g # gs)" by simp
        from this ‹p = f› show ?thesis unfolding f_def by (rule Cons(4))
      next
        assume "p ∈ set fs"
        thus ?thesis by (rule Cons(3))
      qed
    next
      fix h s
      assume "h ∈ set gs"
      hence "h ∈ set (g # gs)" by simp
      moreover assume "p = monom_mult 1 s h"
      ultimately show thesis by (rule Cons(4))
    qed
  next
    assume "p ∈ set (snd (sym_preproc_addnew gs vs fs v))"
    moreover note Cons(3)
    moreover have "h ∈ set gs ==> p = monom_mult 1 s h ==> thesis" for h s
    proof -
      assume "h ∈ set gs"
      hence "h ∈ set (g # gs)" by simp
      moreover assume "p = monom_mult 1 s h"
      ultimately show thesis by (rule Cons(4))
    qed
    ultimately show ?thesis by (rule Cons(1))
  qed
qed

lemma sym_preproc_addnew_pmdl:
  "pmdl (set gs ∪ set (snd (sym_preproc_addnew gs vs fs v))) = pmdl (set gs ∪ set fs)"
    (is "pmdl (set gs ∪ ?l) = ?r")
proof
  have "set gs ⊆ set gs ∪ set fs" by simp
  also have "... ⊆ ?r" by (fact pmdl.span_superset)
  finally have "set gs ⊆ ?r" .
  moreover have "?l ⊆ ?r"
  proof
    fix p
    assume "p ∈ ?l"
    thus "p ∈ ?r"
    proof (rule in_snd_sym_preproc_addnewE)
      assume "p ∈ set fs"
      hence "p ∈ set gs ∪ set fs" by simp
      thus ?thesis by (rule pmdl.span_base)
    next
      fix g s
      assume "g ∈ set gs" and p: "p = monom_mult 1 s g"
      from this(1) ‹set gs ⊆ ?r› have "g ∈ ?r" ..
      thus ?thesis unfolding p by (rule pmdl_closed_monom_mult)
    qed
  qed
  ultimately have "set gs ∪ ?l ⊆ ?r" by blast
  thus "pmdl (set gs ∪ ?l) ⊆ ?r" by (rule pmdl.span_subset_spanI)
next
  from snd_sym_preproc_addnew_superset have "set gs ∪ set fs ⊆ set gs ∪ ?l" by blast
  thus "?r ⊆ pmdl (set gs ∪ ?l)" by (rule pmdl.span_mono)
qed

lemma Keys_snd_sym_preproc_addnew:
  "Keys (set (snd (sym_preproc_addnew gs vs fs v))) ∪ insert v (set vs) =
   Keys (set fs) ∪ insert v (set (fst (sym_preproc_addnew gs vs (fs::('t ==>₀ 'b::semiring_1_no_zero_divisors) list) v)))"
proof (induct gs arbitrary: vs fs)
  case Nil
  show ?case by simp
next
  case (Cons g gs)
  from Cons have eq: "insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) ∪ set ts') =
                      insert v (Keys (set fs') ∪ set (fst (sym_preproc_addnew gs ts' fs' v)))"
    for ts' fs' by simp
  show ?case
  proof (simp add: Let_def eq, rule)
    assume "lt g adds_t v"
    let ?t = "pp_of_term v - lp g"
    define f where "f = monom_mult 1 ?t g"
    define ts' where "ts' = merge_wrt (≻_t) vs (keys_to_list (tail f))"
    define fs' where "fs' = insert_list f fs"
    have "keys (tail f) = keys f - {v}"
    proof (cases "g = 0")
      case True
      hence "f = 0" by (simp add: f_def)
      thus ?thesis by simp
    next
      case False
      hence "lt f = ?t ⊕ lt g" by (simp add: f_def lt_monom_mult)
      also from ‹lt g adds_t v› have "... = v"
        by (metis add_diff_cancel_right' adds_termE pp_of_term_splus)
      finally show ?thesis by (simp add: keys_tail)
    qed
    hence ts': "set ts' = set vs ∪ (keys f - {v})"
      by (simp add: ts'_def set_merge_wrt set_keys_to_list)
    have fs': "set fs' = insert f (set fs)" by (simp add: fs'_def set_insert_list)
    hence "f ∈ set fs'" by simp
    from this snd_sym_preproc_addnew_superset have "f ∈ set (snd (sym_preproc_addnew gs ts' fs' v))" ..
    hence "keys f ⊆ Keys (set (snd (sym_preproc_addnew gs ts' fs' v)))" by (rule keys_subset_Keys)
    hence "insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) ∪ set vs) =
          insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) ∪ set ts')"
      by (auto simp add: ts')
    also have "... = insert v (Keys (set fs') ∪ set (fst (sym_preproc_addnew gs ts' fs' v)))"
      by (fact eq)
    also have "... = insert v (Keys (set fs) ∪ set (fst (sym_preproc_addnew gs ts' fs' v)))"
    proof -
      {
        fix u
        assume "u ≠ v" and "u ∈ keys f"
        hence "u ∈ set ts'" by (simp add: ts')
        from this fst_sym_preproc_addnew_superset have "u ∈ set (fst (sym_preproc_addnew gs ts' fs' v))" ..
      }
      thus ?thesis by (auto simp add: fs' Keys_insert)
    qed
    finally show "insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) ∪ set vs) =
                  insert v (Keys (set fs) ∪ set (fst (sym_preproc_addnew gs ts' fs' v)))" .
  qed
qed

lemma sym_preproc_addnew_complete:
  assumes "g ∈ set gs" and "lt g adds_t v"
  shows "monom_mult 1 (pp_of_term v - lp g) g ∈ set (snd (sym_preproc_addnew gs vs fs v))"
  using assms(1)
proof (induct gs arbitrary: vs fs)
  case Nil
  thus ?case by simp
next
  case (Cons h gs)
  let ?t = "pp_of_term v - lp g"
  show ?case
  proof (cases "h = g")
    case True
    show ?thesis
    proof (simp add: True assms(2) Let_def)
      define f where "f = monom_mult 1 ?t g"
      define ts' where "ts' = merge_wrt (≻_t) vs (keys_to_list (tail (monom_mult 1 ?t g)))"
      have "f ∈ set (insert_list f fs)" by (simp add: set_insert_list)
      with snd_sym_preproc_addnew_superset show "f ∈ set (snd (sym_preproc_addnew gs ts' (insert_list f fs) v))" ..
    qed
  next
    case False
    with Cons(2) have "g ∈ set gs" by simp
    hence *: "monom_mult 1 ?t g ∈ set (snd (sym_preproc_addnew gs ts' fs' v))" for ts' fs'
      by (rule Cons(1))
    show ?thesis by (simp add: Let_def *)
  qed
qed

function sym_preproc_aux :: "('t ==>₀ 'b::semiring_1) list ==> 't list ==> ('t list × ('t ==>₀ 'b) list) ==>
                              ('t list × ('t ==>₀ 'b) list)" where
  "sym_preproc_aux gs ks (vs, fs) =
    (if vs = [] then
      (ks, fs)
    else
      let v = ord_term_lin.max_list vs; vs' = removeAll v vs in
        sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)
    )"
  by pat_completeness auto
termination proof -
  from ex_dgrad obtain d::"'a ==> nat" where dg: "dickson_grading d" ..
  let ?R = "(sym_preproc_aux_term d)::((('t ==>₀ 'b) list × 't list × 't list × ('t ==>₀ 'b) list) ×
                                        ('t ==>₀ 'b) list × 't list × 't list × ('t ==>₀ 'b) list) set"
  show ?thesis
  proof
    from dg show "wf ?R" by (rule sym_preproc_aux_term_wf)
  next
    fix gs::"('t ==>₀ 'b) list" and ks vs fs v vs'
    assume "vs ≠ []" and "v = ord_term_lin.max_list vs" and vs': "vs' = removeAll v vs"
    from this(1, 2) have v: "v = ord_term_lin.Max (set vs)"
      by (simp add: ord_term_lin.max_list_Max)
    obtain vs0 fs0 where eq: "sym_preproc_addnew gs vs' fs v = (vs0, fs0)" by fastforce
    show "((gs, ks @ [v], sym_preproc_addnew gs vs' fs v), (gs, ks, vs, fs)) ∈ ?R"
    proof (simp add: eq sym_preproc_aux_term_def sym_preproc_aux_term1_def sym_preproc_aux_term2_def,
           intro conjI bexI ballI)
      fix w
      assume "w ∈ set vs0"
      show "w ≺_t v"
      proof (rule fst_sym_preproc_addnew_less)
        fix u
        assume "u ∈ set vs'"
        thus "u ≺_t v" unfolding vs' v set_removeAll using ord_term_lin.antisym_conv1 by fastforce
      next
        from ‹w ∈ set vs0› show "w ∈ set (fst (sym_preproc_addnew gs vs' fs v))" by (simp add: eq)
      qed
    next
      from ‹vs ≠ []› show "v ∈ set vs" by (simp add: v)
    next
      from dg have "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs' fs v)))
                                    (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
        by (rule fst_sym_preproc_addnew_dgrad_set_le)
      moreover have "insert v (set vs') = set vs" by (auto simp add: vs' v ‹vs ≠ []›)
      ultimately show "dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) ∪ set vs))"
        by (simp add: eq)
    qed
  qed
qed

lemma sym_preproc_aux_Nil: "sym_preproc_aux gs ks ([], fs) = (ks, fs)"
  by simp

lemma sym_preproc_aux_sorted:
  assumes "sorted_wrt (≻_t) (v # vs)"
  shows "sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)"
proof -
  from assms have *: "u ∈ set vs ==> u ≺_t v" for u by simp
  have "ord_term_lin.max_list (v # vs) = ord_term_lin.Max (set (v # vs))"
    by (simp add: ord_term_lin.max_list_Max del: ord_term_lin.max_list.simps)
  also have "... = v"
  proof (rule ord_term_lin.Max_eqI)
    fix s
    assume "s ∈ set (v # vs)"
    hence "s = v ∨ s ∈ set vs" by simp
    thus "s ⪯_t v"
    proof
      assume "s = v"
      thus ?thesis by simp
    next
      assume "s ∈ set vs"
      hence "s ≺_t v" by (rule *)
      thus ?thesis by simp
    qed
  next
    show "v ∈ set (v # vs)" by simp
  qed rule
  finally have eq1: "ord_term_lin.max_list (v # vs) = v" .
  have eq2: "removeAll v (v # vs) = vs"
  proof (simp, rule removeAll_id, rule)
    assume "v ∈ set vs"
    hence "v ≺_t v" by (rule *)
    thus False ..
  qed
  show ?thesis by (simp only: sym_preproc_aux.simps eq1 eq2 Let_def, simp)
qed

lemma sym_preproc_aux_induct [consumes 0, case_names base rec]:
  assumes base: "∧ks fs. P ks [] fs (ks, fs)"
    and rec: "∧ks vs fs v vs'. vs ≠ [] ==> v = ord_term_lin.Max (set vs) ==> vs' = removeAll v vs ==>
                P (ks @ [v]) (fst (sym_preproc_addnew gs vs' fs v)) (snd (sym_preproc_addnew gs vs' fs v))
                    (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)) ==>
                P ks vs fs (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))"
  shows "P ks vs fs (sym_preproc_aux gs ks (vs, fs))"
proof -
  from ex_dgrad obtain d::"'a ==> nat" where dg: "dickson_grading d" ..
  let ?R = "(sym_preproc_aux_term d)::((('t ==>₀ 'b) list × 't list × 't list × ('t ==>₀ 'b) list) ×
                                        ('t ==>₀ 'b) list × 't list × 't list × ('t ==>₀ 'b) list) set"
  define args where "args = (gs, ks, vs, fs)"
  from dg have "wf ?R" by (rule sym_preproc_aux_term_wf)
  hence "fst args = gs ==> P (fst (snd args)) (fst (snd (snd args))) (snd (snd (snd args)))
                              (sym_preproc_aux gs (fst (snd args)) (snd (snd args)))"
  proof induct
    fix x
    assume IH': "∧y. (y, x) ∈ sym_preproc_aux_term d ==> fst y = gs ==>
                    P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y)))
                      (sym_preproc_aux gs (fst (snd y)) (snd (snd y)))"
    assume "fst x = gs"
    then obtain x0 where x: "x = (gs, x0)" by (meson eq_fst_iff)
    obtain ks x1 where x0: "x0 = (ks, x1)" by (meson case_prodE case_prodI2)
    obtain vs fs where x1: "x1 = (vs, fs)" by (meson case_prodE case_prodI2)
    from IH' have IH: "∧ks' n. ((gs, ks', n), (gs, ks, vs, fs)) ∈ sym_preproc_aux_term d ==>
                            P ks' (fst n) (snd n) (sym_preproc_aux gs ks' n)"
      unfolding x x0 x1 by fastforce
    show "P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x)))
            (sym_preproc_aux gs (fst (snd x)) (snd (snd x)))"
    proof (simp add: x x0 x1 Let_def, intro conjI impI)
      show "P ks [] fs (ks, fs)" by (fact base)
    next
      assume "vs ≠ []"
      define v where "v = ord_term_lin.max_list vs"
      from ‹vs ≠ []› have v_alt: "v = ord_term_lin.Max (set vs)" unfolding v_def
        by (rule ord_term_lin.max_list_Max)
      define vs' where "vs' = removeAll v vs"
      show "P ks vs fs (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))"
      proof (rule rec, fact ‹vs ≠ []›, fact v_alt, fact vs'_def)
        let ?n = "sym_preproc_addnew gs vs' fs v"
        obtain vs0 fs0 where eq: "?n = (vs0, fs0)" by fastforce
        show "P (ks @ [v]) (fst ?n) (snd ?n) (sym_preproc_aux gs (ks @ [v]) ?n)"
        proof (rule IH,
              simp add: eq sym_preproc_aux_term_def sym_preproc_aux_term1_def sym_preproc_aux_term2_def,
              intro conjI bexI ballI)
          fix s
          assume "s ∈ set vs0"
          show "s ≺_t v"
          proof (rule fst_sym_preproc_addnew_less)
            fix u
            assume "u ∈ set vs'"
            thus "u ≺_t v" unfolding vs'_def v_alt set_removeAll using ord_term_lin.antisym_conv1
              by fastforce
          next
            from ‹s ∈ set vs0› show "s ∈ set (fst (sym_preproc_addnew gs vs' fs v))" by (simp add: eq)
          qed
        next
          from ‹vs ≠ []› show "v ∈ set vs" by (simp add: v_alt)
        next
          from dg have "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs' fs v)))
                                        (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
            by (rule fst_sym_preproc_addnew_dgrad_set_le)
          moreover have "insert v (set vs') = set vs" by (auto simp add: vs'_def v_alt ‹vs ≠ []›)
          ultimately show "dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) ∪ set vs))"
            by (simp add: eq)
        qed
      qed
    qed
  qed
  thus ?thesis by (simp add: args_def)
qed

lemma fst_sym_preproc_aux_sorted_wrt:
  assumes "sorted_wrt (≻_t) ks" and "∧k v. k ∈ set ks ==> v ∈ set vs ==> v ≺_t k"
  shows "sorted_wrt (≻_t) (fst (sym_preproc_aux gs ks (vs, fs)))"
  using assms
proof (induct gs ks vs fs rule: sym_preproc_aux_induct)
  case (base ks fs)
  from base(1) show ?case by simp
next
  case (rec ks vs fs v vs')
  from rec(1) have "v ∈ set vs" by (simp add: rec(2))
  from rec(1) have *: "∧u. u ∈ set vs' ==> u ≺_t v" unfolding rec(2, 3) set_removeAll
    using ord_term_lin.antisym_conv3 by force
  show ?case
  proof (rule rec(4))
    show "sorted_wrt (≻_t) (ks @ [v])"
    proof (simp add: sorted_wrt_append rec(5), rule)
      fix k
      assume "k ∈ set ks"
      from this ‹v ∈ set vs› show "v ≺_t k" by (rule rec(6))
    qed
  next
    fix k u
    assume "k ∈ set (ks @ [v])" and "u ∈ set (fst (sym_preproc_addnew gs vs' fs v))"
    from * this(2) have "u ≺_t v" by (rule fst_sym_preproc_addnew_less)
    from ‹k ∈ set (ks @ [v])› have "k ∈ set ks ∨ k = v" by auto
    thus "u ≺_t k"
    proof
      assume "k ∈ set ks"
      from this ‹v ∈ set vs› have "v ≺_t k" by (rule rec(6))
      with ‹u ≺_t v› show ?thesis by simp
    next
      assume "k = v"
      with ‹u ≺_t v› show ?thesis by simp
    qed
  qed
qed

lemma fst_sym_preproc_aux_complete:
  assumes "Keys (set (fs::('t ==>₀ 'b::semiring_1_no_zero_divisors) list)) = set ks ∪ set vs"
  shows "set (fst (sym_preproc_aux gs ks (vs, fs))) = Keys (set (snd (sym_preproc_aux gs ks (vs, fs))))"
  using assms
proof (induct gs ks vs fs rule: sym_preproc_aux_induct)
  case (base ks fs)
  thus ?case by simp
next
  case (rec ks vs fs v vs')
  from rec(1) have "v ∈ set vs" by (simp add: rec(2))
  hence eq: "insert v (set vs') = set vs" by (auto simp add: rec(3))
  also from rec(5) have "... ⊆ Keys (set fs)" by simp
  also from snd_sym_preproc_addnew_superset have "... ⊆ Keys (set (snd (sym_preproc_addnew gs vs' fs v)))"
    by (rule Keys_mono)
  finally have "... = ... ∪ (insert v (set vs'))" by blast
  also have "... = Keys (set fs) ∪ insert v (set (fst (sym_preproc_addnew gs vs' fs v)))"
    by (fact Keys_snd_sym_preproc_addnew)
  also have "... = (set ks ∪ (insert v (set vs'))) ∪ (insert v (set (fst (sym_preproc_addnew gs vs' fs v))))"
    by (simp only: rec(5) eq)
  also have "... = set (ks @ [v]) ∪ (set vs' ∪ set (fst (sym_preproc_addnew gs vs' fs v)))" by auto
  also from fst_sym_preproc_addnew_superset have "... = set (ks @ [v]) ∪ set (fst (sym_preproc_addnew gs vs' fs v))"
    by blast
  finally show ?case by (rule rec(4))
qed

lemma snd_sym_preproc_aux_superset: "set fs ⊆ set (snd (sym_preproc_aux gs ks (vs, fs)))"
proof (induct fs rule: sym_preproc_aux_induct)
  case (base ks fs)
  show ?case by simp
next
  case (rec ks vs fs v vs')
  from snd_sym_preproc_addnew_superset rec(4) show ?case by (rule subset_trans)
qed

lemma in_snd_sym_preproc_auxE:
  assumes "p ∈ set (snd (sym_preproc_aux gs ks (vs, fs)))"
  assumes 1: "p ∈ set fs ==> thesis"
  assumes 2: "∧g t. g ∈ set gs ==> p = monom_mult 1 t g ==> thesis"
  shows thesis
  using assms
proof (induct gs ks vs fs arbitrary: thesis rule: sym_preproc_aux_induct)
  case (base ks fs)
  from base(1) have "p ∈ set fs" by simp
  thus ?case by (rule base(2))
next
  case (rec ks vs fs v vs')
  from rec(5) show ?case
  proof (rule rec(4))
    assume "p ∈ set (snd (sym_preproc_addnew gs vs' fs v))"
    thus ?thesis
    proof (rule in_snd_sym_preproc_addnewE)
      assume "p ∈ set fs"
      thus ?thesis by (rule rec(6))
    next
      fix g s
      assume "g ∈ set gs" and "p = monom_mult 1 s g"
      thus ?thesis by (rule rec(7))
    qed
  next
    fix g t
    assume "g ∈ set gs" and "p = monom_mult 1 t g"
    thus ?thesis by (rule rec(7))
  qed
qed

lemma snd_sym_preproc_aux_pmdl:
  "pmdl (set gs ∪ set (snd (sym_preproc_aux gs ks (ts, fs)))) = pmdl (set gs ∪ set fs)"
proof (induct fs rule: sym_preproc_aux_induct)
  case (base ks fs)
  show ?case by simp
next
  case (rec ks vs fs v vs')
  from rec(4) sym_preproc_addnew_pmdl show ?case by (rule trans)
qed

lemma snd_sym_preproc_aux_dgrad_set_le:
  assumes "dickson_grading d" and "set vs ⊆ Keys (set (fs::('t ==>₀ 'b::semiring_1_no_zero_divisors) list))"
  shows "dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_aux gs ks (vs, fs))))) (pp_of_term ` Keys (set gs ∪ set fs))"
  using assms(2)
proof (induct fs rule: sym_preproc_aux_induct)
  case (base ks fs)
  show ?case by (rule dgrad_set_le_subset, simp add: Keys_Un image_Un)
next
  case (rec ks vs fs v vs')
  let ?n = "sym_preproc_addnew gs vs' fs v"
  from rec(1) have "v ∈ set vs" by (simp add: rec(2))
  hence set_vs: "insert v (set vs') = set vs" by (auto simp add: rec(3))
  from rec(5) have eq: "Keys (set fs) ∪ (Keys (set gs) ∪ set vs) = Keys (set gs) ∪ Keys (set fs)"
    by blast
  have "dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) ?n))))
                        (pp_of_term ` Keys (set gs ∪ set (snd ?n)))"
  proof (rule rec(4))
    have "set (fst ?n) ⊆ Keys (set (snd ?n)) ∪ insert v (set vs')"
      by (simp only: Keys_snd_sym_preproc_addnew, blast)
    also have "... = Keys (set (snd ?n)) ∪ (set vs)" by (simp only: set_vs)
    also have "... ⊆ Keys (set (snd ?n))"
    proof -
      {
        fix u
        assume "u ∈ set vs"
        with rec(5) have "u ∈ Keys (set fs)" ..
        then obtain f where "f ∈ set fs" and "u ∈ keys f" by (rule in_KeysE)
        from this(1) snd_sym_preproc_addnew_superset have "f ∈ set (snd ?n)" ..
        with ‹u ∈ keys f› have "u ∈ Keys (set (snd ?n))" by (rule in_KeysI)
      }
      thus ?thesis by auto
    qed
    finally show "set (fst ?n) ⊆ Keys (set (snd ?n))" .
  qed
  also have "dgrad_set_le d ... (pp_of_term ` Keys (set gs ∪ set fs))"
  proof (simp only: image_Un Keys_Un dgrad_set_le_Un, rule)
    show "dgrad_set_le d (pp_of_term ` Keys (set gs)) (pp_of_term ` Keys (set gs) ∪ pp_of_term ` Keys (set fs))"
      by (rule dgrad_set_le_subset, simp)
  next
    have "dgrad_set_le d (pp_of_term ` Keys (set (snd ?n))) (pp_of_term ` (Keys (set fs) ∪ insert v (set (fst ?n))))"
      by (rule dgrad_set_le_subset, auto simp only: Keys_snd_sym_preproc_addnew[symmetric])
    also have "dgrad_set_le d ... (pp_of_term ` Keys (set fs) ∪ pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
    proof (simp only: dgrad_set_le_Un image_Un, rule)
      show "dgrad_set_le d (pp_of_term ` Keys (set fs))
            (pp_of_term ` Keys (set fs) ∪ (pp_of_term ` Keys (set gs) ∪ pp_of_term ` insert v (set vs')))"
        by (rule dgrad_set_le_subset, blast)
    next
      have "dgrad_set_le d (pp_of_term ` {v}) (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
        by (rule dgrad_set_le_subset, simp)
      moreover from assms(1) have "dgrad_set_le d (pp_of_term ` set (fst ?n)) (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
        by (rule fst_sym_preproc_addnew_dgrad_set_le)
      ultimately have "dgrad_set_le d (pp_of_term ` ({v} ∪ set (fst ?n))) (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
        by (simp only: dgrad_set_le_Un image_Un)
      also have "dgrad_set_le d (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))
                                (pp_of_term ` (Keys (set fs) ∪ (Keys (set gs) ∪ insert v (set vs'))))"
        by (rule dgrad_set_le_subset, blast)
      finally show "dgrad_set_le d (pp_of_term ` insert v (set (fst ?n)))
                                   (pp_of_term ` Keys (set fs) ∪ (pp_of_term ` Keys (set gs) ∪ pp_of_term ` insert v (set vs')))"
        by (simp add: image_Un)
    qed
    finally show "dgrad_set_le d (pp_of_term ` Keys (set (snd ?n))) (pp_of_term ` Keys (set gs) ∪ pp_of_term ` Keys (set fs))"
      by (simp only: set_vs eq, metis eq image_Un)
  qed
  finally show ?case .
qed

lemma components_snd_sym_preproc_aux_subset:
  assumes "set vs ⊆ Keys (set (fs::('t ==>₀ 'b::semiring_1_no_zero_divisors) list))"
  shows "component_of_term ` Keys (set (snd (sym_preproc_aux gs ks (vs, fs)))) ⊆
          component_of_term ` Keys (set gs ∪ set fs)"
  using assms
proof (induct fs rule: sym_preproc_aux_induct)
  case (base ks fs)
  show ?case by (simp add: Keys_Un image_Un)
next
  case (rec ks vs fs v vs')
  let ?n = "sym_preproc_addnew gs vs' fs v"
  from rec(1) have "v ∈ set vs" by (simp add: rec(2))
  hence set_vs: "insert v (set vs') = set vs" by (auto simp add: rec(3))
  from rec(5) have eq: "Keys (set fs) ∪ (Keys (set gs) ∪ set vs) = Keys (set gs) ∪ Keys (set fs)"
    by blast
  have "component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) ?n))) ⊆
                        component_of_term ` Keys (set gs ∪ set (snd ?n))"
  proof (rule rec(4))
    have "set (fst ?n) ⊆ Keys (set (snd ?n)) ∪ insert v (set vs')"
      by (simp only: Keys_snd_sym_preproc_addnew, blast)
    also have "... = Keys (set (snd ?n)) ∪ (set vs)" by (simp only: set_vs)
    also have "... ⊆ Keys (set (snd ?n))"
    proof -
      {
        fix u
        assume "u ∈ set vs"
        with rec(5) have "u ∈ Keys (set fs)" ..
        then obtain f where "f ∈ set fs" and "u ∈ keys f" by (rule in_KeysE)
        from this(1) snd_sym_preproc_addnew_superset have "f ∈ set (snd ?n)" ..
        with ‹u ∈ keys f› have "u ∈ Keys (set (snd ?n))" by (rule in_KeysI)
      }
      thus ?thesis by auto
    qed
    finally show "set (fst ?n) ⊆ Keys (set (snd ?n))" .
  qed
  also have "... ⊆ component_of_term ` Keys (set gs ∪ set fs)"
  proof (simp only: image_Un Keys_Un Un_subset_iff, rule, fact Un_upper1)
    have "component_of_term ` Keys (set (snd ?n)) ⊆ component_of_term ` (Keys (set fs) ∪ insert v (set (fst ?n)))"
      by (auto simp only: Keys_snd_sym_preproc_addnew[symmetric])
    also have "... ⊆ component_of_term ` Keys (set fs) ∪ component_of_term ` (Keys (set gs) ∪ insert v (set vs'))"
    proof (simp only: Un_subset_iff image_Un, rule, fact Un_upper1)
      have "component_of_term ` {v} ⊆ component_of_term ` (Keys (set gs) ∪ insert v (set vs'))"
        by simp
      moreover have "component_of_term ` set (fst ?n) ⊆ component_of_term ` (Keys (set gs) ∪ insert v (set vs'))"
        by (rule components_fst_sym_preproc_addnew_subset)
      ultimately have "component_of_term ` ({v} ∪ set (fst ?n)) ⊆ component_of_term ` (Keys (set gs) ∪ insert v (set vs'))"
        by (simp only: Un_subset_iff image_Un)
      also have "component_of_term ` (Keys (set gs) ∪ insert v (set vs')) ⊆
                          component_of_term ` (Keys (set fs) ∪ (Keys (set gs) ∪ insert v (set vs')))"
        by blast
      finally show "component_of_term ` insert v (set (fst ?n)) ⊆
                        component_of_term ` Keys (set fs) ∪
                        (component_of_term ` Keys (set gs) ∪ component_of_term ` insert v (set vs'))"
        by (simp add: image_Un)
    qed
    finally show "component_of_term ` Keys (set (snd ?n)) ⊆
                    component_of_term ` Keys (set gs) ∪ component_of_term ` Keys (set fs)"
      by (simp only: set_vs eq, metis eq image_Un)
  qed
  finally show ?case .
qed

lemma snd_sym_preproc_aux_complete:
  assumes "∧u' g'. u' ∈ Keys (set fs) ==> u' ∉ set vs ==> g' ∈ set gs ==> lt g' adds_t u' ==>
            monom_mult 1 (pp_of_term u' - lp g') g' ∈ set fs"
  assumes "u ∈ Keys (set (snd (sym_preproc_aux gs ks (vs, fs))))" and "g ∈ set gs" and "lt g adds_t u"
  shows "monom_mult (1::'b::semiring_1_no_zero_divisors) (pp_of_term u - lp g) g ∈
          set (snd (sym_preproc_aux gs ks (vs, fs)))"
  using assms
proof (induct fs rule: sym_preproc_aux_induct)
  case (base ks fs)
  from base(2) have "u ∈ Keys (set fs)" by simp
  from this _ base(3, 4) have "monom_mult 1 (pp_of_term u - lp g) g ∈ set fs"
  proof (rule base(1))
    show "u ∉ set []" by simp
  qed
  thus ?case by simp
next
  case (rec ks vs fs v vs')
  from rec(1) have "v ∈ set vs" by (simp add: rec(2))
  hence set_ts: "set vs = insert v (set vs')" by (auto simp add: rec(3))

  let ?n = "sym_preproc_addnew gs vs' fs v"
  from _ rec(6, 7, 8) show ?case
  proof (rule rec(4))
    fix v' g'
    assume "v' ∈ Keys (set (snd ?n))" and "v' ∉ set (fst ?n)" and "g' ∈ set gs" and "lt g' adds_t v'"
    from this(1) Keys_snd_sym_preproc_addnew have "v' ∈ Keys (set fs) ∪ insert v (set (fst ?n))"
      by blast
    with ‹v' ∉ set (fst ?n)› have disj: "v' ∈ Keys (set fs) ∨ v' = v" by blast
    show "monom_mult 1 (pp_of_term v' - lp g') g' ∈ set (snd ?n)"
    proof (cases "v' = v")
      case True
      from ‹g' ∈ set gs› ‹lt g' adds_t v'› show ?thesis
        unfolding True by (rule sym_preproc_addnew_complete)
    next
      case False
      with disj have "v' ∈ Keys (set fs)" by simp
      moreover have "v' ∉ set vs"
      proof
        assume "v' ∈ set vs"
        hence "v' ∈ set vs'" using False by (simp add: rec(3))
        with fst_sym_preproc_addnew_superset have "v' ∈ set (fst ?n)" ..
        with ‹v' ∉ set (fst ?n)› show False ..
      qed
      ultimately have "monom_mult 1 (pp_of_term v' - lp g') g' ∈ set fs"
        using ‹g' ∈ set gs› ‹lt g' adds_t v'› by (rule rec(5))
      with snd_sym_preproc_addnew_superset show ?thesis ..
    qed
  qed
qed

definition sym_preproc :: "('t ==>₀ 'b::semiring_1) list ==> ('t ==>₀ 'b) list ==> ('t list × ('t ==>₀ 'b) list)"
  where "sym_preproc gs fs = sym_preproc_aux gs [] (Keys_to_list fs, fs)"

lemma sym_preproc_Nil [simp]: "sym_preproc gs [] = ([], [])"
  by (simp add: sym_preproc_def)

lemma fst_sym_preproc:
  "fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs (fs::('t ==>₀ 'b::semiring_1_no_zero_divisors) list)))"
proof -
  let ?a = "fst (sym_preproc gs fs)"
  let ?b = "Keys_to_list (snd (sym_preproc gs fs))"
  have "antisymp (≻_t)" unfolding antisymp_def by fastforce
  have "irreflp (≻_t)" by (simp add: irreflp_def)
  moreover have "transp (≻_t)" unfolding transp_def by fastforce
  moreover have s1: "sorted_wrt (≻_t) ?a" unfolding sym_preproc_def
    by (rule fst_sym_preproc_aux_sorted_wrt, simp_all)
  ultimately have d1: "distinct ?a" by (rule distinct_sorted_wrt_irrefl)
  have s2: "sorted_wrt (≻_t) ?b" by (fact Keys_to_list_sorted_wrt)
  with ‹irreflp (≻_t)› ‹transp (≻_t)› have d2: "distinct ?b" by (rule distinct_sorted_wrt_irrefl)
  from ‹antisymp (≻_t)› s1 d1 s2 d2 show ?thesis
  proof (rule sorted_wrt_distinct_set_unique)
    show "set ?a = set ?b" unfolding set_Keys_to_list sym_preproc_def
      by (rule fst_sym_preproc_aux_complete, simp add: set_Keys_to_list)
  qed
qed

lemma snd_sym_preproc_superset: "set fs ⊆ set (snd (sym_preproc gs fs))"
  by (simp only: sym_preproc_def snd_conv, fact snd_sym_preproc_aux_superset)

lemma in_snd_sym_preprocE:
  assumes "p ∈ set (snd (sym_preproc gs fs))"
  assumes 1: "p ∈ set fs ==> thesis"
  assumes 2: "∧g t. g ∈ set gs ==> p = monom_mult 1 t g ==> thesis"
  shows thesis
  using assms unfolding sym_preproc_def snd_conv by (rule in_snd_sym_preproc_auxE)

lemma snd_sym_preproc_pmdl: "pmdl (set gs ∪ set (snd (sym_preproc gs fs))) = pmdl (set gs ∪ set fs)"
  unfolding sym_preproc_def snd_conv by (fact snd_sym_preproc_aux_pmdl)

lemma snd_sym_preproc_dgrad_set_le:
  assumes "dickson_grading d"
  shows "dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc gs fs))))
                        (pp_of_term ` Keys (set gs ∪ set (fs::('t ==>₀ 'b::semiring_1_no_zero_divisors) list)))"
  unfolding sym_preproc_def snd_conv using assms
proof (rule snd_sym_preproc_aux_dgrad_set_le)
  show "set (Keys_to_list fs) ⊆ Keys (set fs)" by (simp add: set_Keys_to_list)
qed

corollary snd_sym_preproc_dgrad_p_set_le:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d (set (snd (sym_preproc gs fs))) (set gs ∪ set (fs::('t ==>₀ 'b::semiring_1_no_zero_divisors) list))"
  unfolding dgrad_p_set_le_def
proof -
  from assms show "dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc gs fs)))) (pp_of_term ` Keys (set gs ∪ set fs))"
    by (rule snd_sym_preproc_dgrad_set_le)
qed

lemma components_snd_sym_preproc_subset:
  "component_of_term ` Keys (set (snd (sym_preproc gs fs))) ⊆
          component_of_term ` Keys (set gs ∪ set (fs::('t ==>₀ 'b::semiring_1_no_zero_divisors) list))"
  unfolding sym_preproc_def snd_conv
  by (rule components_snd_sym_preproc_aux_subset, simp add: set_Keys_to_list)

lemma snd_sym_preproc_complete:
  assumes "v ∈ Keys (set (snd (sym_preproc gs fs)))" and "g ∈ set gs" and "lt g adds_t v"
  shows "monom_mult (1::'b::semiring_1_no_zero_divisors) (pp_of_term v - lp g) g ∈ set (snd (sym_preproc gs fs))"
  using _ assms unfolding sym_preproc_def snd_conv
proof (rule snd_sym_preproc_aux_complete)
  fix u' and g'::"'t ==>₀ 'b"
  assume "u' ∈ Keys (set fs)" and "u' ∉ set (Keys_to_list fs)"
  thus "monom_mult 1 (pp_of_term u' - lp g') g' ∈ set fs" by (simp add: set_Keys_to_list)
qed

end (* gd_term *)

subsection ‹‹lin_red››

context ordered_term
begin

definition lin_red :: "('t ==>₀ 'b::field) set ==> ('t ==>₀ 'b) ==> ('t ==>₀ 'b) ==> bool"
  where "lin_red F p q ≡ (∃f∈F. red_single p q f 0)"

text ‹@{const lin_red} is a restriction of @{const red}, where the reductor (‹f›) may only be
 multiplied by a constant factor, i.\,e. where the power-product is ‹0›.›

lemma lin_redI:
  assumes "f ∈ F" and "red_single p q f 0"
  shows "lin_red F p q"
  unfolding lin_red_def using assms ..

lemma lin_redE:
  assumes "lin_red F p q"
  obtains f::"'t ==>₀ 'b::field" where "f ∈ F" and "red_single p q f 0"
proof -
  from assms obtain f where "f ∈ F" and t: "red_single p q f 0" unfolding lin_red_def by blast
  thus "?thesis" ..
qed

lemma lin_red_imp_red:
  assumes "lin_red F p q"
  shows "red F p q"
proof -
  from assms obtain f where "f ∈ F" and "red_single p q f 0" by (rule lin_redE)
  thus ?thesis by (rule red_setI)
qed

lemma lin_red_Un: "lin_red (F ∪ G) p q = (lin_red F p q ∨ lin_red G p q)"
proof
  assume "lin_red (F ∪ G) p q"
  then obtain f where "f ∈ F ∪ G" and r: "red_single p q f 0" by (rule lin_redE)
  from this(1) show "lin_red F p q ∨ lin_red G p q"
  proof
    assume "f ∈ F"
    from this r have "lin_red F p q" by (rule lin_redI)
    thus ?thesis ..
  next
    assume "f ∈ G" 
    from this r have "lin_red G p q" by (rule lin_redI)
    thus ?thesis ..
  qed
next
  assume "lin_red F p q ∨ lin_red G p q"
  thus "lin_red (F ∪ G) p q"
  proof
    assume "lin_red F p q"
    then obtain f where "f ∈ F" and r: "red_single p q f 0" by (rule lin_redE)
    from this(1) have "f ∈ F ∪ G" by simp
    from this r show ?thesis by (rule lin_redI)
  next
    assume "lin_red G p q"
    then obtain g where "g ∈ G" and r: "red_single p q g 0" by (rule lin_redE)
    from this(1) have "g ∈ F ∪ G" by simp
    from this r show ?thesis by (rule lin_redI)
  qed
qed

lemma lin_red_imp_red_rtrancl:
  assumes "(lin_red F)^** p q"
  shows "(red F)^** p q"
  using assms
proof induct
  case base
  show ?case ..
next
  case (step y z)
  from step(2) have "red F y z" by (rule lin_red_imp_red)
  with step(3) show ?case ..
qed

lemma phull_closed_lin_red:
  assumes "phull B ⊆ phull A" and "p ∈ phull A" and "lin_red B p q"
  shows "q ∈ phull A"
proof -
  from assms(3) obtain f where "f ∈ B" and "red_single p q f 0" by (rule lin_redE)
  hence q: "q = p - (lookup p (lt f) / lc f) ⋅ f"
    by (simp add: red_single_def term_simps map_scale_eq_monom_mult)
  have "q - p ∈ phull B"
    by (simp add: q, rule phull.span_neg, rule phull.span_scale, rule phull.span_base, fact ‹f ∈ B›)
  with assms(1) have "q - p ∈ phull A" ..
  from this assms(2) have "(q - p) + p ∈ phull A" by (rule phull.span_add)
  thus ?thesis by simp
qed

subsection ‹Reduction›

definition Macaulay_red :: "'t list ==> ('t ==>₀ 'b) list ==> ('t ==>₀ 'b::field) list"
  where "Macaulay_red vs fs =
     (let lts = map lt (filter (λp. p ≠ 0) fs) in
       filter (λp. p ≠ 0 ∧ lt p ∉ set lts) (mat_to_polys vs (row_echelon (polys_to_mat vs fs)))
     )"

text ‹‹Macaulay_red vs fs› auto-reduces (w.\,r.\,t. @{const lin_red}) the given list ‹fs› and returns
 those non-zero polynomials whose leading terms are not in ‹lt_set (set fs)›.
 Argument ‹vs› is expected to be ‹Keys_to_list fs›; this list is passed as an argument
 to @{const Macaulay_red}, because it can be efficiently computed by symbolic preprocessing.›

lemma Macaulay_red_alt:
  "Macaulay_red (Keys_to_list fs) fs = filter (λp. lt p ∉ lt_set (set fs)) (Macaulay_list fs)"
proof -
  have "{x ∈ set fs. x ≠ 0} = set fs - {0}" by blast
  thus ?thesis by (simp add: Macaulay_red_def Macaulay_list_def Macaulay_mat_def lt_set_def Let_def)
qed

lemma set_Macaulay_red:
  "set (Macaulay_red (Keys_to_list fs) fs) = set (Macaulay_list fs) - {p. lt p ∈ lt_set (set fs)}"
  by (auto simp add: Macaulay_red_alt)

lemma Keys_Macaulay_red: "Keys (set (Macaulay_red (Keys_to_list fs) fs)) ⊆ Keys (set fs)"
proof -
  have "Keys (set (Macaulay_red (Keys_to_list fs) fs)) ⊆ Keys (set (Macaulay_list fs))"
    unfolding set_Macaulay_red by (fact Keys_minus)
  also have "... ⊆ Keys (set fs)" by (fact Keys_Macaulay_list)
  finally show ?thesis .
qed

end (* ordered_term *)

context gd_term
begin

lemma Macaulay_red_reducible:
  assumes "f ∈ phull (set fs)" and "F ⊆ set fs" and "lt_set F = lt_set (set fs)"
  shows "(lin_red (F ∪ set (Macaulay_red (Keys_to_list fs) fs)))^** f 0"
proof -
  define A where "A = F ∪ set (Macaulay_red (Keys_to_list fs) fs)"

  have phull_A: "phull A ⊆ phull (set fs)"
  proof (rule phull.span_subset_spanI, simp add: A_def, rule)
    have "F ⊆ phull F" by (rule phull.span_superset)
    also from assms(2) have "... ⊆ phull (set fs)" by (rule phull.span_mono)
    finally show "F ⊆ phull (set fs)" .
  next
    have "set (Macaulay_red (Keys_to_list fs) fs) ⊆ set (Macaulay_list fs)"
      by (auto simp add: set_Macaulay_red)
    also have "... ⊆ phull (set (Macaulay_list fs))" by (rule phull.span_superset)
    also have "... = phull (set fs)" by (rule phull_Macaulay_list)
    finally show "set (Macaulay_red (Keys_to_list fs) fs) ⊆ phull (set fs)" .
  qed

  have lt_A: "p ∈ phull (set fs) ==> p ≠ 0 ==> (∧g. g ∈ A ==> g ≠ 0 ==> lt g = lt p ==> thesis) ==> thesis"
    for p thesis
  proof -
    assume "p ∈ phull (set fs)" and "p ≠ 0"
    then obtain g where g_in: "g ∈ set (Macaulay_list fs)" and "g ≠ 0" and "lt p = lt g"
      by (rule Macaulay_list_lt)
    assume *: "∧g. g ∈ A ==> g ≠ 0 ==> lt g = lt p ==> thesis"
    show ?thesis
    proof (cases "g ∈ set (Macaulay_red (Keys_to_list fs) fs)")
      case True
      hence "g ∈ A" by (simp add: A_def)
      from this ‹g ≠ 0› ‹lt p = lt g›[symmetric] show ?thesis by (rule *)
    next
      case False
      with g_in have "lt g ∈ lt_set (set fs)" by (simp add: set_Macaulay_red)
      also have "... = lt_set F" by (simp only: assms(3))
      finally obtain g' where "g' ∈ F" and "g' ≠ 0" and "lt g' = lt g" by (rule lt_setE)
      from this(1) have "g' ∈ A" by (simp add: A_def)
      moreover note ‹g' ≠ 0›
      moreover have "lt g' = lt p" by (simp only: ‹lt p = lt g› ‹lt g' = lt g›)
      ultimately show ?thesis by (rule *)
    qed
  qed

  from assms(2) finite_set have "finite F" by (rule finite_subset)
  from this finite_set have fin_A: "finite A" unfolding A_def by (rule finite_UnI)

  from ex_dgrad obtain d::"'a ==> nat" where dg: "dickson_grading d" ..
  from fin_A have "finite (insert f A)" ..
  then obtain m where "insert f A ⊆ dgrad_p_set d m" by (rule dgrad_p_set_exhaust)
  hence A_sub: "A ⊆ dgrad_p_set d m" and "f ∈ dgrad_p_set d m" by simp_all
  from dg have "wfP (dickson_less_p d m)" by (rule wf_dickson_less_p)
  from this assms(1) ‹f ∈ dgrad_p_set d m› show "(lin_red A)^** f 0"
  proof (induct f)
    fix p
    assume IH: "∧q. dickson_less_p d m q p ==> q ∈ phull (set fs) ==> q ∈ dgrad_p_set d m ==>
                    (lin_red A)^** q 0"
      and "p ∈ phull (set fs)" and "p ∈ dgrad_p_set d m"
    show "(lin_red A)^** p 0"
    proof (cases "p = 0")
      case True
      thus ?thesis by simp
    next
      case False
      with ‹p ∈ phull (set fs)› obtain g where "g ∈ A" and "g ≠ 0" and "lt g = lt p" by (rule lt_A)
      define q where "q = p - monom_mult (lc p / lc g) 0 g"
      from ‹g ∈ A› have lr: "lin_red A p q"
      proof (rule lin_redI)
        show "red_single p q g 0"
          by (simp add: red_single_def ‹lt g = lt p› lc_def[symmetric] q_def ‹g ≠ 0› lc_not_0[OF False] term_simps)
      qed
      moreover have "(lin_red A)^** q 0"
      proof -
        from lr have red: "red A p q" by (rule lin_red_imp_red)
        with dg A_sub ‹p ∈ dgrad_p_set d m› have "q ∈ dgrad_p_set d m" by (rule dgrad_p_set_closed_red)
        moreover from red have "q ≺_p p" by (rule red_ord)
        ultimately have "dickson_less_p d m q p" using ‹p ∈ dgrad_p_set d m›
          by (simp add: dickson_less_p_def)
        moreover from phull_A ‹p ∈ phull (set fs)› lr have "q ∈ phull (set fs)"
          by (rule phull_closed_lin_red)
        ultimately show ?thesis using ‹q ∈ dgrad_p_set d m› by (rule IH)
      qed
      ultimately show ?thesis by fastforce
    qed
  qed
qed

primrec pdata_pairs_to_list :: "('t, 'b::field, 'c) pdata_pair list ==> ('t ==>₀ 'b) list" where
  "pdata_pairs_to_list [] = []"|
  "pdata_pairs_to_list (p # ps) =
    (let f = fst (fst p); g = fst (snd p); lf = lp f; lg = lp g; l = lcs lf lg in
      (monom_mult (1 / lc f) (l - lf) f) # (monom_mult (1 / lc g) (l - lg) g) #
      (pdata_pairs_to_list ps)
    )"

lemma in_pdata_pairs_to_listI1:
  assumes "(f, g) ∈ set ps"
  shows "monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f)))
              (fst f) ∈ set (pdata_pairs_to_list ps)" (is "?m ∈ _")
  using assms
proof (induct ps)
  case Nil
  thus ?case by simp
next
  case (Cons p ps)
  from Cons(2) have "p = (f, g) ∨ (f, g) ∈ set ps" by auto
  thus ?case
  proof
    assume "p = (f, g)"
    show ?thesis by (simp add: ‹p = (f, g)› Let_def)
  next
    assume "(f, g) ∈ set ps"
    hence "?m ∈ set (pdata_pairs_to_list ps)" by (rule Cons(1))
    thus ?thesis by (simp add: Let_def)
  qed
qed

lemma in_pdata_pairs_to_listI2:
  assumes "(f, g) ∈ set ps"
  shows "monom_mult (1 / lc (fst g)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst g)))
              (fst g) ∈ set (pdata_pairs_to_list ps)" (is "?m ∈ _")
  using assms
proof (induct ps)
  case Nil
  thus ?case by simp
next
  case (Cons p ps)
  from Cons(2) have "p = (f, g) ∨ (f, g) ∈ set ps" by auto
  thus ?case
  proof
    assume "p = (f, g)"
    show ?thesis by (simp add: ‹p = (f, g)› Let_def)
  next
    assume "(f, g) ∈ set ps"
    hence "?m ∈ set (pdata_pairs_to_list ps)" by (rule Cons(1))
    thus ?thesis by (simp add: Let_def)
  qed
qed

lemma in_pdata_pairs_to_listE:
  assumes "h ∈ set (pdata_pairs_to_list ps)"
  obtains f g where "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
    and "h = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
  using assms
proof (induct ps arbitrary: thesis)
  case Nil
  from Nil(2) show ?case by simp
next
  case (Cons p ps)
  let ?f = "fst (fst p)"
  let ?g = "fst (snd p)"
  let ?lf = "lp ?f"
  let ?lg = "lp ?g"
  let ?l = "lcs ?lf ?lg"
  from Cons(3) have "h = monom_mult (1 / lc ?f) (?l - ?lf) ?f ∨ h = monom_mult (1 / lc ?g) (?l - ?lg) ?g ∨
                     h ∈ set (pdata_pairs_to_list ps)"
    by (simp add: Let_def)
  thus ?case
  proof (elim disjE)
    assume h: "h = monom_mult (1 / lc ?f) (?l - ?lf) ?f"
    have "(fst p, snd p) ∈ set (p # ps)" by simp
    hence "(fst p, snd p) ∈ set (p # ps) ∨ (snd p, fst p) ∈ set (p # ps)" ..
    from this h show ?thesis by (rule Cons(2))
  next
    assume h: "h = monom_mult (1 / lc ?g) (?l - ?lg) ?g"
    have "(fst p, snd p) ∈ set (p # ps)" by simp
    hence "(snd p, fst p) ∈ set (p # ps) ∨ (fst p, snd p) ∈ set (p # ps)" ..
    moreover from h have "h = monom_mult (1 / lc ?g) ((lcs ?lg ?lf) - ?lg) ?g"
      by (simp only: lcs_comm)
    ultimately show ?thesis by (rule Cons(2))
  next
    assume h_in: "h ∈ set (pdata_pairs_to_list ps)"
    obtain f g where "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
      and h: "h = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
      by (rule Cons(1), assumption, intro h_in)
    from this(1) have "(f, g) ∈ set (p # ps) ∨ (g, f) ∈ set (p # ps)" by auto
    from this h show ?thesis by (rule Cons(2))
  qed
qed

definition f4_red_aux :: "('t, 'b::field, 'c) pdata list ==> ('t, 'b, 'c) pdata_pair list ==>
                          ('t ==>₀ 'b) list"
  where "f4_red_aux bs ps =
            (let aux = sym_preproc (map fst bs) (pdata_pairs_to_list ps) in Macaulay_red (fst aux) (snd aux))"

text ‹@{const f4_red_aux} only takes two arguments, since it does not distinguish between those
 elements of the current basis that are known to be a Gr\"obner basis (called ‹gs› in
 @{theory Groebner_Bases.Algorithm_Schema}) and the remaining ones.›

lemma f4_red_aux_not_zero: "0 ∉ set (f4_red_aux bs ps)"
  by (simp add: f4_red_aux_def Let_def fst_sym_preproc set_Macaulay_red set_Macaulay_list)

lemma f4_red_aux_irredudible:
  assumes "h ∈ set (f4_red_aux bs ps)" and "b ∈ set bs" and "fst b ≠ 0"
  shows "¬ lt (fst b) adds_t lt h"
proof
  from assms(1) f4_red_aux_not_zero have "h ≠ 0" by metis
  hence "lt h ∈ keys h" by (rule lt_in_keys)
  also from assms(1) have "... ⊆ Keys (set (f4_red_aux bs ps))" by (rule keys_subset_Keys)
  also have "... ⊆ Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
    (is "_ ⊆ Keys (set ?s)") by (simp only: f4_red_aux_def Let_def fst_sym_preproc Keys_Macaulay_red)
  finally have "lt h ∈ Keys (set ?s)" .
  moreover from assms(2) have "fst b ∈ set (map fst bs)" by auto
  moreover assume a: "lt (fst b) adds_t lt h"
  ultimately have "monom_mult 1 (lp h - lp (fst b)) (fst b) ∈ set ?s" (is "?m ∈ _")
    by (rule snd_sym_preproc_complete)
  from assms(3) have "?m ≠ 0" by (simp add: monom_mult_eq_zero_iff)
  with ‹?m ∈ set ?s› have "lt ?m ∈ lt_set (set ?s)" by (rule lt_setI)
  moreover from assms(3) a have "lt ?m = lt h"
    by (simp add: lt_monom_mult, metis add_diff_cancel_right' adds_termE pp_of_term_splus)
  ultimately have "lt h ∈ lt_set (set ?s)" by simp
  moreover from assms(1) have "lt h ∉ lt_set (set ?s)"
    by (simp add: f4_red_aux_def Let_def fst_sym_preproc set_Macaulay_red)
  ultimately show False by simp
qed

lemma f4_red_aux_dgrad_p_set_le:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d (set (f4_red_aux bs ps)) (args_to_set ([], bs, ps))"
  unfolding dgrad_p_set_le_def dgrad_set_le_def
proof
  fix s
  assume "s ∈ pp_of_term ` Keys (set (f4_red_aux bs ps))"
  also have "... ⊆ pp_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
    (is "_ ⊆ pp_of_term ` Keys (set ?s)")
    by (rule image_mono, simp only: f4_red_aux_def Let_def fst_sym_preproc Keys_Macaulay_red)
  finally have "s ∈ pp_of_term ` Keys (set ?s)" .
  with snd_sym_preproc_dgrad_set_le[OF assms] obtain t
    where "t ∈ pp_of_term ` Keys (set (map fst bs) ∪ set (pdata_pairs_to_list ps))" and "d s ≤ d t"
    by (rule dgrad_set_leE)
  from this(1) have "t ∈ pp_of_term ` Keys (fst ` set bs) ∨ t ∈ pp_of_term ` Keys (set (pdata_pairs_to_list ps))"
    by (simp add: Keys_Un image_Un)
  thus "∃t ∈ pp_of_term ` Keys (args_to_set ([], bs, ps)). d s ≤ d t"
  proof
    assume "t ∈ pp_of_term ` Keys (fst ` set bs)"
    also have "... ⊆ pp_of_term ` Keys (args_to_set ([], bs, ps))"
      by (rule image_mono, rule Keys_mono, auto simp add: args_to_set_alt)
    finally have "t ∈ pp_of_term ` Keys (args_to_set ([], bs, ps))" .
    with ‹d s ≤ d t› show ?thesis ..
  next
    assume "t ∈ pp_of_term ` Keys (set (pdata_pairs_to_list ps))"
    then obtain p where "p ∈ set (pdata_pairs_to_list ps)" and "t ∈ pp_of_term ` keys p"
      by (auto elim: in_KeysE)
    from this(1) obtain f g where disj: "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
      and p: "p = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
      by (rule in_pdata_pairs_to_listE)
    from disj have "fst f ∈ args_to_set ([], bs, ps) ∧ fst g ∈ args_to_set ([], bs, ps)"
    proof
      assume "(f, g) ∈ set ps"
      hence "f ∈ fst ` set ps" and "g ∈ snd ` set ps" by force+
      hence "fst f ∈ fst ` fst ` set ps" and "fst g ∈ fst ` snd ` set ps" by simp_all
      thus ?thesis by (simp add: args_to_set_def image_Un)
    next
      assume "(g, f) ∈ set ps"
      hence "f ∈ snd ` set ps" and "g ∈ fst ` set ps" by force+
      hence "fst f ∈ fst ` snd ` set ps" and "fst g ∈ fst ` fst ` set ps" by simp_all
      thus ?thesis by (simp add: args_to_set_def image_Un)
    qed
    hence "fst f ∈ args_to_set ([], bs, ps)" and "fst g ∈ args_to_set ([], bs, ps)" by simp_all
    hence keys_f: "keys (fst f) ⊆ Keys (args_to_set ([], bs, ps))"
      and keys_g: "keys (fst g) ⊆ Keys (args_to_set ([], bs, ps))"
      by (auto intro!: keys_subset_Keys)
    let ?lf = "lp (fst f)"
    let ?lg = "lp (fst g)"
    define l where "l = lcs ?lf ?lg"
    have "pp_of_term ` keys p ⊆ pp_of_term ` ((⊕) (lcs ?lf ?lg - ?lf) ` keys (fst f))" unfolding p
      using keys_monom_mult_subset by (rule image_mono)
    with ‹t ∈ pp_of_term ` keys p› have "t ∈ pp_of_term ` ((⊕) (l - ?lf) ` keys (fst f))" unfolding l_def ..
    then obtain t' where "t' ∈ pp_of_term ` keys (fst f)" and t: "t = (l - ?lf) + t'"
      using pp_of_term_splus by fastforce
    from this(1) have "fst f ≠ 0" by auto
    show ?thesis
    proof (cases "fst g = 0")
      case True
      hence "?lg = 0" by (simp add: lt_def min_term_def term_simps)
      hence "l = ?lf" by (simp add: l_def lcs_zero lcs_comm)
      hence "t = t'" by (simp add: t)
      with ‹d s ≤ d t› have "d s ≤ d t'" by simp
      moreover from ‹t' ∈ pp_of_term ` keys (fst f)› keys_f have "t' ∈ pp_of_term ` Keys (args_to_set ([], bs, ps))"
        by blast
      ultimately show ?thesis ..
    next
      case False
      have "d t = d (l - ?lf) ∨ d t = d t'"
        by (auto simp add: t dickson_gradingD1[OF assms])
      thus ?thesis
      proof
        assume "d t = d (l - ?lf)"
        also from assms have "... ≤ ord_class.max (d ?lf) (d ?lg)"
          unfolding l_def by (rule dickson_grading_lcs_minus)
        finally have "d s ≤ d ?lf ∨ d s ≤ d ?lg" using ‹d s ≤ d t› by auto
        thus ?thesis
        proof
          assume "d s ≤ d ?lf"
          moreover have "lt (fst f) ∈ Keys (args_to_set ([], bs, ps))"
            by (rule, rule lt_in_keys, fact+)
          ultimately show ?thesis by blast
        next
          assume "d s ≤ d ?lg"
          moreover have "lt (fst g) ∈ Keys (args_to_set ([], bs, ps))"
            by (rule, rule lt_in_keys, fact+)
          ultimately show ?thesis by blast
        qed
      next
        assume "d t = d t'"
        with ‹d s ≤ d t› have "d s ≤ d t'" by simp
        moreover from ‹t' ∈ pp_of_term ` keys (fst f)› keys_f have "t' ∈ pp_of_term ` Keys (args_to_set ([], bs, ps))"
          by blast
        ultimately show ?thesis ..
      qed
    qed
  qed
qed

lemma components_f4_red_aux_subset:
  "component_of_term ` Keys (set (f4_red_aux bs ps)) ⊆ component_of_term ` Keys (args_to_set ([], bs, ps))"
proof
  fix k
  assume "k ∈ component_of_term ` Keys (set (f4_red_aux bs ps))"
  also have "... ⊆ component_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
    by (rule image_mono, simp only: f4_red_aux_def Let_def fst_sym_preproc Keys_Macaulay_red)
  also have "... ⊆ component_of_term ` Keys (set (map fst bs) ∪ set (pdata_pairs_to_list ps))"
    by (fact components_snd_sym_preproc_subset)
  finally have "k ∈ component_of_term ` Keys (fst ` set bs) ∪ component_of_term ` Keys (set (pdata_pairs_to_list ps))"
    by (simp add: image_Un Keys_Un)
  thus "k ∈ component_of_term ` Keys (args_to_set ([], bs, ps))"
  proof
    assume "k ∈ component_of_term ` Keys (fst ` set bs)"
    also have "... ⊆ component_of_term ` Keys (args_to_set ([], bs, ps))"
      by (rule image_mono, rule Keys_mono, auto simp add: args_to_set_alt)
    finally show "k ∈ component_of_term ` Keys (args_to_set ([], bs, ps))" .
  next
    assume "k ∈ component_of_term ` Keys (set (pdata_pairs_to_list ps))"
    then obtain p where "p ∈ set (pdata_pairs_to_list ps)" and "k ∈ component_of_term ` keys p"
      by (auto elim: in_KeysE)
    from this(1) obtain f g where disj: "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
      and p: "p = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
      by (rule in_pdata_pairs_to_listE)
    from disj have "fst f ∈ args_to_set ([], bs, ps)"
      by (simp add: args_to_set_alt, metis fst_conv image_eqI snd_conv)
    hence "fst f ∈ args_to_set ([], bs, ps)" by simp
    hence keys_f: "keys (fst f) ⊆ Keys (args_to_set ([], bs, ps))"
      by (auto intro!: keys_subset_Keys)
    let ?lf = "lp (fst f)"
    let ?lg = "lp (fst g)"
    define l where "l = lcs ?lf ?lg"
    have "component_of_term ` keys p ⊆ component_of_term ` ((⊕) (lcs ?lf ?lg - ?lf) ` keys (fst f))"
      unfolding p using keys_monom_mult_subset by (rule image_mono)
    with ‹k ∈ component_of_term ` keys p› have "k ∈ component_of_term ` ((⊕) (l - ?lf) ` keys (fst f))"
      unfolding l_def ..
    hence "k ∈ component_of_term ` keys (fst f)" using component_of_term_splus by fastforce
    with keys_f show "k ∈ component_of_term ` Keys (args_to_set ([], bs, ps))" by blast
  qed
qed

lemma pmdl_f4_red_aux: "set (f4_red_aux bs ps) ⊆ pmdl (args_to_set ([], bs, ps))"
proof -
  have "set (f4_red_aux bs ps) ⊆
          set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
    by (auto simp add: f4_red_aux_def Let_def fst_sym_preproc set_Macaulay_red)
  also have "... ⊆ pmdl (set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))))"
    by (fact pmdl.span_superset)
  also have "... = pmdl (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
    by (fact pmdl_Macaulay_list)
  also have "... ⊆ pmdl (set (map fst bs) ∪
                        set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
    by (rule pmdl.span_mono, blast)
  also have "... = pmdl (set (map fst bs) ∪ set (pdata_pairs_to_list ps))"
    by (fact snd_sym_preproc_pmdl)
  also have "... ⊆ pmdl (args_to_set ([], bs, ps))"
  proof (rule pmdl.span_subset_spanI, simp only: Un_subset_iff, rule conjI)
    have "set (map fst bs) ⊆ args_to_set ([], bs, ps)" by (auto simp add: args_to_set_def)
    also have "... ⊆ pmdl (args_to_set ([], bs, ps))" by (rule pmdl.span_superset)
    finally show "set (map fst bs) ⊆ pmdl (args_to_set ([], bs, ps))" .
  next
    show "set (pdata_pairs_to_list ps) ⊆ pmdl (args_to_set ([], bs, ps))"
    proof
      fix p
      assume "p ∈ set (pdata_pairs_to_list ps)"
      then obtain f g where "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
        and p: "p = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
        by (rule in_pdata_pairs_to_listE)
      from this(1) have "f ∈ fst ` set ps ∪ snd ` set ps" by force
      hence "fst f ∈ args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
      hence "fst f ∈ pmdl (args_to_set ([], bs, ps))" by (rule pmdl.span_base)
      thus "p ∈ pmdl (args_to_set ([], bs, ps))" unfolding p by (rule pmdl_closed_monom_mult)
    qed
  qed
  finally show ?thesis .
qed

lemma f4_red_aux_phull_reducible:
  assumes "set ps ⊆ set bs × set bs"
    and "f ∈ phull (set (pdata_pairs_to_list ps))"
  shows "(red (fst ` set bs ∪ set (f4_red_aux bs ps)))^** f 0"
proof -
  define fs where "fs = snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))"
  have "set (pdata_pairs_to_list ps) ⊆ set fs" unfolding fs_def by (fact snd_sym_preproc_superset)
  hence "phull (set (pdata_pairs_to_list ps)) ⊆ phull (set fs)" by (rule phull.span_mono)
  with assms(2) have f_in: "f ∈ phull (set fs)" ..
  have eq: "(set fs) ∪ set (f4_red_aux bs ps) = (set fs) ∪ set (Macaulay_red (Keys_to_list fs) fs)"
    by (simp add: f4_red_aux_def fs_def Let_def fst_sym_preproc)

  have "(lin_red ((set fs) ∪ set (f4_red_aux bs ps)))^** f 0"
    by (simp only: eq, rule Macaulay_red_reducible, fact f_in, fact subset_refl, fact refl)
  thus ?thesis
  proof induct
    case base
    show ?case ..
  next
    case (step y z)
    from step(2) have "red (fst ` set bs ∪ set (f4_red_aux bs ps)) y z" unfolding lin_red_Un
    proof
      assume "lin_red (set fs) y z"
      then obtain a where "a ∈ set fs" and r: "red_single y z a 0" by (rule lin_redE)
      from this(1) obtain b c t where "b ∈ fst ` set bs" and a: "a = monom_mult c t b" unfolding fs_def
      proof (rule in_snd_sym_preprocE)
        assume *: "∧b c t. b ∈ fst ` set bs ==> a = monom_mult c t b ==> thesis"
        assume "a ∈ set (pdata_pairs_to_list ps)"
        then obtain f g where "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
          and a: "a = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
          by (rule in_pdata_pairs_to_listE)
        from this(1) have "f ∈ fst ` set ps ∪ snd ` set ps" by force
        with assms(1) have "f ∈ set bs" by fastforce
        hence "fst f ∈ fst ` set bs" by simp
        from this a show ?thesis by (rule *)
      next
        fix g s
        assume *: "∧b c t. b ∈ fst ` set bs ==> a = monom_mult c t b ==> thesis"
        assume "g ∈ set (map fst bs)"
        hence "g ∈ fst ` set bs" by simp
        moreover assume "a = monom_mult 1 s g"
        ultimately show ?thesis by (rule *)
      qed
      from r have "c ≠ 0" and "b ≠ 0" by (simp_all add: a red_single_def monom_mult_eq_zero_iff)
      from r have "red_single y z b t"
        by (simp add: a red_single_def monom_mult_eq_zero_iff lt_monom_mult[OF ‹c ≠ 0› ‹b ≠ 0›]
                      monom_mult_assoc term_simps)
      with ‹b ∈ fst ` set bs› have "red (fst ` set bs) y z" by (rule red_setI)
      thus ?thesis by (rule red_unionI1)
    next
      assume "lin_red (set (f4_red_aux bs ps)) y z"
      hence "red (set (f4_red_aux bs ps)) y z" by (rule lin_red_imp_red)
      thus ?thesis by (rule red_unionI2)
    qed
    with step(3) show ?case ..
  qed
qed

corollary f4_red_aux_spoly_reducible:
  assumes "set ps ⊆ set bs × set bs" and "(p, q) ∈ set ps"
  shows "(red (fst ` set bs ∪ set (f4_red_aux bs ps)))^** (spoly (fst p) (fst q)) 0"
  using assms(1)
proof (rule f4_red_aux_phull_reducible)
  let ?lt = "lp (fst p)"
  let ?lq = "lp (fst q)"
  let ?l = "lcs ?lt ?lq"
  let ?p = "monom_mult (1 / lc (fst p)) (?l - ?lt) (fst p)"
  let ?q = "monom_mult (1 / lc (fst q)) (?l - ?lq) (fst q)"
  from assms(2) have "?p ∈ set (pdata_pairs_to_list ps)" and "?q ∈ set (pdata_pairs_to_list ps)"
    by (rule in_pdata_pairs_to_listI1, rule in_pdata_pairs_to_listI2)
  hence "?p ∈ phull (set (pdata_pairs_to_list ps))" and "?q ∈ phull (set (pdata_pairs_to_list ps))"
    by (auto intro: phull.span_base)
  hence "?p - ?q ∈ phull (set (pdata_pairs_to_list ps))" by (rule phull.span_diff)
  thus "spoly (fst p) (fst q) ∈ phull (set (pdata_pairs_to_list ps))"
    by (simp add: spoly_def Let_def phull.span_zero lc_def split: if_split)
qed

definition f4_red :: "('t, 'b::field, 'c::default, 'd) complT"
  where "f4_red gs bs ps sps data = (map (λh. (h, default)) (f4_red_aux (gs @ bs) sps), snd data)"

lemma fst_set_fst_f4_red: "fst ` set (fst (f4_red gs bs ps sps data)) = set (f4_red_aux (gs @ bs) sps)"
  by (simp add: f4_red_def, force)

lemma rcp_spec_f4_red: "rcp_spec f4_red"
proof (rule rcp_specI)
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat × 'd"
  show "0 ∉ fst ` set (fst (f4_red gs bs ps sps data))"
    by (simp add: fst_set_fst_f4_red f4_red_aux_not_zero)
next
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps h b and data::"nat × 'd"
  assume "h ∈ set (fst (f4_red gs bs ps sps data))" and "b ∈ set gs ∪ set bs"
  from this(1) have "fst h ∈ fst ` set (fst (f4_red gs bs ps sps data))" by simp
  hence "fst h ∈ set (f4_red_aux (gs @ bs) sps)" by (simp only: fst_set_fst_f4_red)
  moreover from ‹b ∈ set gs ∪ set bs› have "b ∈ set (gs @ bs)" by simp
  moreover assume "fst b ≠ 0"
  ultimately show "¬ lt (fst b) adds_t lt (fst h)" by (rule f4_red_aux_irredudible)
next
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and d::"'a ==> nat" and data::"nat × 'd"
  assume "dickson_grading d"
  hence "dgrad_p_set_le d (set (f4_red_aux (gs @ bs) sps)) (args_to_set ([], gs @ bs, sps))"
    by (fact f4_red_aux_dgrad_p_set_le)
  also have "... = args_to_set (gs, bs, sps)" by (simp add: args_to_set_alt image_Un)
  finally show "dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))"
    by (simp only: fst_set_fst_f4_red)
next
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat × 'd"
  have "component_of_term ` Keys (set (f4_red_aux (gs @ bs) sps)) ⊆
        component_of_term ` Keys (args_to_set ([], gs @ bs, sps))"
    by (fact components_f4_red_aux_subset)
  also have "... = component_of_term ` Keys (args_to_set (gs, bs, sps))"
    by (simp add: args_to_set_alt image_Un)
  finally show "component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) ⊆
        component_of_term ` Keys (args_to_set (gs, bs, sps))"
    by (simp only: fst_set_fst_f4_red)
next
  fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat × 'd"
  have "set (f4_red_aux (gs @ bs) sps) ⊆ pmdl (args_to_set ([], gs @ bs, sps))"
    by (fact pmdl_f4_red_aux)
  also have "... = pmdl (args_to_set (gs, bs, sps))" by (simp add: args_to_set_alt image_Un)
  finally have "fst ` set (fst (f4_red gs bs ps sps data)) ⊆ pmdl (args_to_set (gs, bs, sps))"
    by (simp only: fst_set_fst_f4_red)
  moreover {
    fix p q :: "('t, 'b, 'c) pdata"
    assume "set sps ⊆ set bs × (set gs ∪ set bs)"
    hence "set sps ⊆ set (gs @ bs) × set (gs @ bs)" by fastforce
    moreover assume "(p, q) ∈ set sps"
    ultimately have "(red (fst ` set (gs @ bs) ∪ set (f4_red_aux (gs @ bs) sps)))<sup>**</sup> (spoly (fst p) (fst q)) 0"
      by (rule f4_red_aux_spoly_reducible)
  }
  ultimately show
    "fst ` set (fst (f4_red gs bs ps sps data)) ⊆ pmdl (args_to_set (gs, bs, sps)) ∧
     (∀(p, q)∈set sps.
         set sps ⊆ set bs × (set gs ∪ set bs) ⟶
         (red (fst ` (set gs ∪ set bs) ∪ fst ` set (fst (f4_red gs bs ps sps data))))^** (spoly (fst p) (fst q)) 0)"
    by (auto simp add: image_Un fst_set_fst_f4_red)
qed

lemmas compl_struct_f4_red = compl_struct_rcp[OF rcp_spec_f4_red]
lemmas compl_pmdl_f4_red = compl_pmdl_rcp[OF rcp_spec_f4_red]
lemmas compl_conn_f4_red = compl_conn_rcp[OF rcp_spec_f4_red]

subsection ‹Pair Selection›

primrec f4_sel_aux :: "'a ==> ('t, 'b::zero, 'c) pdata_pair list ==> ('t, 'b, 'c) pdata_pair list" where
  "f4_sel_aux _ [] = []"|
  "f4_sel_aux t (p # ps) =
    (if (lcs (lp (fst (fst p))) (lp (fst (snd p)))) = t then
      p # (f4_sel_aux t ps)
    else
      []
    )"

lemma f4_sel_aux_subset: "set (f4_sel_aux t ps) ⊆ set ps"
  by (induct ps, auto)

primrec f4_sel :: "('t, 'b::zero, 'c, 'd) selT" where
  "f4_sel gs bs [] data = []"|
  "f4_sel gs bs (p # ps) data = p # (f4_sel_aux (lcs (lp (fst (fst p))) (lp (fst (snd p)))) ps)"

lemma sel_spec_f4_sel: "sel_spec f4_sel"
proof (rule sel_specI)
  fix gs bs :: "('t, 'b, 'c) pdata list" and ps::"('t, 'b, 'c) pdata_pair list" and data::"nat × 'd"
  assume "ps ≠ []"
  then obtain p ps' where ps: "ps = p # ps'" by (meson list.exhaust)
  show "f4_sel gs bs ps data ≠ [] ∧ set (f4_sel gs bs ps data) ⊆ set ps"
  proof
    show "f4_sel gs bs ps data ≠ []" by (simp add: ps)
  next
    from f4_sel_aux_subset show "set (f4_sel gs bs ps data) ⊆ set ps" by (auto simp add: ps)
  qed
qed

subsection ‹The F4 Algorithm›

text ‹The F4 algorithm is just @{const gb_schema_direct} with parameters instantiated by suitable
 functions.›

lemma struct_spec_f4: "struct_spec f4_sel add_pairs_canon add_basis_canon f4_red"
  using sel_spec_f4_sel ap_spec_add_pairs_canon ab_spec_add_basis_sorted compl_struct_f4_red
  by (rule struct_specI)

definition f4_aux :: "('t, 'b, 'c) pdata list ==> nat × nat × 'd ==> ('t, 'b, 'c) pdata list ==>
                   ('t, 'b, 'c) pdata_pair list ==> ('t, 'b::field, 'c::default) pdata list"
  where "f4_aux = gb_schema_aux f4_sel add_pairs_canon add_basis_canon f4_red"

lemmas f4_aux_simps [code] = gb_schema_aux_simps[OF struct_spec_f4, folded f4_aux_def]

definition f4 :: "('t, 'b, 'c) pdata' list ==> 'd ==> ('t, 'b::field, 'c::default) pdata' list"
  where "f4 = gb_schema_direct f4_sel add_pairs_canon add_basis_canon f4_red"

lemmas f4_simps [code] = gb_schema_direct_def[of f4_sel add_pairs_canon add_basis_canon f4_red, folded f4_def f4_aux_def]

lemmas f4_isGB = gb_schema_direct_isGB[OF struct_spec_f4 compl_conn_f4_red, folded f4_def]

lemmas f4_pmdl = gb_schema_direct_pmdl[OF struct_spec_f4 compl_pmdl_f4_red, folded f4_def]

subsubsection ‹Special Case: ‹punit››

lemma (in gd_term) struct_spec_f4_punit: "punit.struct_spec punit.f4_sel add_pairs_punit_canon punit.add_basis_canon punit.f4_red"
  using punit.sel_spec_f4_sel ap_spec_add_pairs_punit_canon ab_spec_add_basis_sorted punit.compl_struct_f4_red
  by (rule punit.struct_specI)

definition f4_aux_punit :: "('a, 'b, 'c) pdata list ==> nat × nat × 'd ==> ('a, 'b, 'c) pdata list ==>
                   ('a, 'b, 'c) pdata_pair list ==> ('a, 'b::field, 'c::default) pdata list"
  where "f4_aux_punit = punit.gb_schema_aux punit.f4_sel add_pairs_punit_canon punit.add_basis_canon punit.f4_red"

lemmas f4_aux_punit_simps [code] = punit.gb_schema_aux_simps[OF struct_spec_f4_punit, folded f4_aux_punit_def]

definition f4_punit :: "('a, 'b, 'c) pdata' list ==> 'd ==> ('a, 'b::field, 'c::default) pdata' list"
  where "f4_punit = punit.gb_schema_direct punit.f4_sel add_pairs_punit_canon punit.add_basis_canon punit.f4_red"

lemmas f4_punit_simps [code] = punit.gb_schema_direct_def[of "punit.f4_sel" add_pairs_punit_canon
                                "punit.add_basis_canon" "punit.f4_red", folded f4_punit_def f4_aux_punit_def]

lemmas f4_punit_isGB = punit.gb_schema_direct_isGB[OF struct_spec_f4_punit punit.compl_conn_f4_red, folded f4_punit_def]

lemmas f4_punit_pmdl = punit.gb_schema_direct_pmdl[OF struct_spec_f4_punit punit.compl_pmdl_f4_red, folded f4_punit_def]

end (* gd_term *)

end (* theory *)