Theory F4

(* 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 0 'b) list × 't list × 't list × ('t 0 'b) list) ×
                                                (('t 0 'b) list × 't list × 't list × ('t 0 'b) list)) set"
  where "sym_preproc_aux_term1 d =
            {((gs1, ks1, ts1, fs1), (gs2::('t 0 'b) list, ks2, ts2, fs2)). t2set ts2. t1set ts1. t1 t t2}"

definition sym_preproc_aux_term2 :: "('a  nat)  ((('t 0 'b::zero) list × 't list × 't list × ('t 0 'b) list) ×
                                                (('t 0 'b) list × 't list × 't list × ('t 0 'b) list)) set"
  where "sym_preproc_aux_term2 d =
            {((gs1, ks1, ts1, fs1), (gs2::('t 0 '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 "zQ. y  pp_of_term -` dgrad_set d m. y t 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 0 'b) list × 't list × 't list × ('t 0 '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 "zQ. y{x. set (fst (snd (snd x)))  ?B}. (y, z)  sym_preproc_aux_term1 d  y  Q"
  proof (cases "zQ. 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 0 'b) list × 't list × 't list × ('t 0 '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 "zQ. 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 0 'b::semiring_1) list  't list  ('t 0 'b) list  't 
                              ('t list × ('t 0 'b) list)" where
  "sym_preproc_addnew [] vs fs _ = (vs, fs)"|
  "sym_preproc_addnew (g # gs) vs fs v =
    (if lt g addst 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 addst 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 addst 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 addst 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 addst 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 addst 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 0 '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 addst 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 addst 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 addst 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 0 'b::semiring_1) list  't list  ('t list × ('t 0 'b) list) 
                              ('t list × ('t 0 '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 0 'b) list × 't list × 't list × ('t 0 'b) list) ×
                                        ('t 0 'b) list × 't list × 't list × ('t 0 'b) list) set"
  show ?thesis
  proof
    from dg show "wf ?R" by (rule sym_preproc_aux_term_wf)
  next
    fix gs::"('t 0 '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 0 'b) list × 't list × 't list × ('t 0 'b) list) ×
                                        ('t 0 'b) list × 't list × 't list × ('t 0 '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 0 '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 0 '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 0 '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' addst 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 addst 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' addst 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' addst 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' addst v' by (rule rec(5))
      with snd_sym_preproc_addnew_superset show ?thesis ..
    qed
  qed
qed

definition sym_preproc :: "('t 0 'b::semiring_1) list  ('t 0 'b) list  ('t list × ('t 0 '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 0 '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 0 '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 0 '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 0 '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 addst 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 0 '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 0 'b::field) set  ('t 0 'b)  ('t 0 'b)  bool"
  where "lin_red F p q  (fF. 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 0 '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 0 'b) list  ('t 0 '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 0 '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 0 '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) addst 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) addst 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) addst 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)))** (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 *)