Theory Auto_Reduction

(* Author: Alexander Maletzky *)

section ‹Auto-reducing Lists of Polynomials›

theory Auto_Reduction
  imports Reduction More_MPoly_Type_Class
begin

subsection ‹Reduction and Monic Sets›

context ordered_term
begin

lemma is_red_monic: "is_red B (monic p)  is_red B p"
  unfolding is_red_adds_iff keys_monic ..

lemma red_image_monic [simp]: "red (monic ` B) = red B"
proof (rule, rule)
  fix p q
  show "red (monic ` B) p q  red B p q"
  proof
    assume "red (monic ` B) p q"
    then obtain f t where "f  monic ` B" and *: "red_single p q f t" by (rule red_setE)
    from this(1) obtain g where "g  B" and "f = monic g" ..
    from * have "f  0" by (simp add: red_single_def)
    hence "g  0" by (simp add: monic_0_iff f = monic g)
    hence "lc g  0" by (rule lc_not_0)
    have eq: "monom_mult (lc g) 0 f = g" by (simp add: f = monic g mult_lc_monic[OF g  0])
    from g  B show "red B p q"
    proof (rule red_setI)
      from * lc g  0 have "red_single p q (monom_mult (lc g) 0 f) t" by (rule red_single_mult_const)
      thus "red_single p q g t" by (simp only: eq)
    qed
  next
    assume "red B p q"
    then obtain f t where "f  B" and *: "red_single p q f t" by (rule red_setE)
    from * have "f  0" by (simp add: red_single_def)
    hence "lc f  0" by (rule lc_not_0)
    hence "1 / lc f  0" by simp
    from f  B have "monic f  monic ` B" by (rule imageI)
    thus "red (monic ` B) p q"
    proof (rule red_setI)
      from * 1 / lc f  0 show "red_single p q (monic f) t" unfolding monic_def
        by (rule red_single_mult_const)
    qed
  qed
qed

lemma is_red_image_monic [simp]: "is_red (monic ` B) p  is_red B p"
  by (simp add: is_red_def)

subsection ‹Minimal Bases and Auto-reduced Bases›

definition is_auto_reduced :: "('t 0 'b::field) set  bool" where
  "is_auto_reduced B  (bB. ¬ is_red (B - {b}) b)"

definition is_minimal_basis :: "('t 0 'b::zero) set  bool" where
  "is_minimal_basis B  (0  B  (p q. p  B  q  B  p  q  ¬ lt p addst lt q))"

lemma is_auto_reducedD:
  assumes "is_auto_reduced B" and "b  B"
  shows "¬ is_red (B - {b}) b"
  using assms unfolding is_auto_reduced_def by auto

text ‹The converse of the following lemma is only true if @{term B} is minimal!›
lemma image_monic_is_auto_reduced:
  assumes "is_auto_reduced B"
  shows "is_auto_reduced (monic ` B)"
  unfolding is_auto_reduced_def
proof
  fix b
  assume "b  monic ` B"
  then obtain b' where b_def: "b = monic b'" and "b'  B" ..
  from assms b'  B have nred: "¬ is_red (B - {b'}) b'" by (rule is_auto_reducedD)
  show "¬ is_red ((monic ` B) - {b}) b"
  proof
    assume red: "is_red ((monic ` B) - {b}) b"
    have "(monic ` B) - {b}  monic ` (B - {b'})" unfolding b_def by auto
    with red have "is_red (monic ` (B - {b'})) b" by (rule is_red_subset)
    hence "is_red (B - {b'}) b'" unfolding b_def is_red_monic is_red_image_monic .
    with nred show False ..
  qed
qed
  
lemma is_minimal_basisI:
  assumes "p. p  B  p  0" and "p q. p  B  q  B  p  q  ¬ lt p addst lt q"
  shows "is_minimal_basis B"
  unfolding is_minimal_basis_def using assms by auto
    
lemma is_minimal_basisD1:
  assumes "is_minimal_basis B" and "p  B"
  shows "p  0"
  using assms unfolding is_minimal_basis_def by auto
    
lemma is_minimal_basisD2:
  assumes "is_minimal_basis B" and "p  B" and "q  B" and "p  q"
  shows "¬ lt p addst lt q"
  using assms unfolding is_minimal_basis_def by auto
  
lemma is_minimal_basisD3:
  assumes "is_minimal_basis B" and "p  B" and "q  B" and "p  q"
  shows "¬ lt q addst lt p"
  using assms unfolding is_minimal_basis_def by auto
    
lemma is_minimal_basis_subset:
  assumes "is_minimal_basis B" and "A  B"
  shows "is_minimal_basis A"
proof (intro is_minimal_basisI)
  fix p
  assume "p  A"
  with A  B have "p  B" ..
  with is_minimal_basis B show "p  0" by (rule is_minimal_basisD1)
next
  fix p q
  assume "p  A" and "q  A" and "p  q"
  from p  A and q  A have "p  B" and "q  B" using A  B by auto
  from is_minimal_basis B this p  q show " ¬ lt p addst lt q" by (rule is_minimal_basisD2)
qed
  
lemma nadds_red:
  assumes nadds: "q. q  B  ¬ lt q addst lt p" and red: "red B p r"
  shows "r  0  lt r = lt p"
proof -
  from red obtain q t where "q  B" and rs: "red_single p r q t" by (rule red_setE)
  from rs have "q  0" and "lookup p (t  lt q)  0"
    and r_def: "r = p - monom_mult (lookup p (t  lt q) / lc q) t q" unfolding red_single_def by simp_all
  have "t  lt q t lt p" by (rule lt_max, fact)
  moreover have "t  lt q  lt p"
  proof
    assume "t  lt q = lt p"
    hence "lt q addst lt p" by (metis adds_term_triv) 
    with nadds[OF q  B] show False ..
  qed
  ultimately have "t  lt q t lt p" by simp
  let ?m = "monom_mult (lookup p (t  lt q) / lc q) t q"
  from lookup p (t  lt q)  0 lc_not_0[OF q  0] have c0: "lookup p (t  lt q) / lc q  0" by simp
  from q  0 c0 have "?m  0" by (simp add: monom_mult_eq_zero_iff)
  have "lt (-?m) = lt ?m" by (fact lt_uminus)
  also have lt1: "lt ?m = t  lt q" by (rule lt_monom_mult, fact+)
  finally have lt2: "lt (-?m) = t  lt q" .
  
  show ?thesis
  proof
    show "r  0"
    proof
      assume "r = 0"
      hence "p = ?m" unfolding r_def by simp
      with lt1 t  lt q  lt p show False by simp
    qed
  next
    have "lt (-?m + p) = lt p"
    proof (rule lt_plus_eqI)
      show "lt (-?m) t lt p" unfolding lt2 by fact
    qed
    thus "lt r = lt p" unfolding r_def by simp
  qed
qed
    
lemma nadds_red_nonzero:
  assumes nadds: "q. q  B  ¬ lt q addst lt p" and "red B p r"
  shows "r  0"
  using nadds_red[OF assms] by simp
    
lemma nadds_red_lt:
  assumes nadds: "q. q  B  ¬ lt q addst lt p" and "red B p r"
  shows "lt r = lt p"
  using nadds_red[OF assms] by simp
  
lemma nadds_red_rtrancl_lt:
  assumes nadds: "q. q  B  ¬ lt q addst lt p" and rtrancl: "(red B)** p r"
  shows "lt r = lt p"
  using rtrancl
proof (induct rule: rtranclp_induct)
  case base
  show ?case ..
next
  case (step y z)
  have "lt z = lt y"
  proof (rule nadds_red_lt)
    fix q
    assume "q  B"
    thus "¬ lt q addst lt y" unfolding lt y = lt p by (rule nadds)
  qed fact
  with lt y = lt p show ?case by simp
qed
  
lemma nadds_red_rtrancl_nonzero:
  assumes nadds: "q. q  B  ¬ lt q addst lt p" and "p  0" and rtrancl: "(red B)** p r"
  shows "r  0"
  using rtrancl
proof (induct rule: rtranclp_induct)
  case base
  show ?case by fact
next
  case (step y z)
  from nadds (red B)** p y have "lt y = lt p" by (rule nadds_red_rtrancl_lt)
  show "z  0"
  proof (rule nadds_red_nonzero)
    fix q
    assume "q  B"
    thus "¬ lt q addst lt y" unfolding lt y = lt p by (rule nadds)
  qed fact
qed
  
lemma minimal_basis_red_rtrancl_nonzero:
  assumes "is_minimal_basis B" and "p  B" and "(red (B - {p}))** p r"
  shows "r  0"
proof (rule nadds_red_rtrancl_nonzero)
  fix q
  assume "q  (B - {p})"
  hence "q  B" and "q  p" by auto
  show "¬ lt q addst lt p" by (rule is_minimal_basisD2, fact+)
next
  show "p  0" by (rule is_minimal_basisD1, fact+)
qed fact

lemma minimal_basis_red_rtrancl_lt:
  assumes "is_minimal_basis B" and "p  B" and "(red (B - {p}))** p r"
  shows "lt r = lt p"
proof (rule nadds_red_rtrancl_lt)
  fix q
  assume "q  (B - {p})"
  hence "q  B" and "q  p" by auto
  show "¬ lt q addst lt p" by (rule is_minimal_basisD2, fact+)
qed fact
  
lemma is_minimal_basis_replace:
  assumes major: "is_minimal_basis B" and "p  B" and red: "(red (B - {p}))** p r"
  shows "is_minimal_basis (insert r (B - {p}))"
proof (rule is_minimal_basisI)
  fix q
  assume "q  insert r (B - {p})"
  hence "q = r  q  B  q  p" by simp
  thus "q  0"
  proof
    assume "q = r"
    from assms show ?thesis unfolding q = r by (rule minimal_basis_red_rtrancl_nonzero)
  next
    assume "q  B  q  p"
    hence "q  B" ..
    with major show ?thesis by (rule is_minimal_basisD1)
  qed
next
  fix a b
  assume "a  insert r (B - {p})" and "b  insert r (B - {p})" and "a  b"
  from assms have ltr: "lt r = lt p" by (rule minimal_basis_red_rtrancl_lt)
  from b  insert r (B - {p}) have b: "b = r  b  B  b  p" by simp
  from a  insert r (B - {p}) have "a = r  a  B  a  p" by simp
  thus "¬ lt a addst lt b"
  proof
    assume "a = r"
    hence lta: "lt a = lt p" using ltr by simp
    from b show ?thesis
    proof
      assume "b = r"
      with a  b show ?thesis unfolding a = r by simp
    next
      assume "b  B  b  p"
      hence "b  B" and "p  b" by auto
      with major p  B have "¬ lt p addst lt b" by (rule is_minimal_basisD2)
      thus ?thesis unfolding lta .
    qed
  next
    assume "a  B  a  p"
    hence "a  B" and "a  p" by simp_all
    from b show ?thesis
    proof
      assume "b = r"
      from major a  B p  B a  p have "¬ lt a addst lt p" by (rule is_minimal_basisD2)
      thus ?thesis unfolding b = r ltr by simp
    next
      assume "b  B  b  p"
      hence "b  B" ..
      from major a  B b  B a  b show ?thesis by (rule is_minimal_basisD2)
    qed
  qed
qed

subsection ‹Computing Minimal Bases›

definition comp_min_basis :: "('t 0 'b) list  ('t 0 'b::zero) list" where
  "comp_min_basis xs = filter_min (λx y. lt x addst lt y) (filter (λx. x  0) xs)"

lemma comp_min_basis_subset': "set (comp_min_basis xs)  {x  set xs. x  0}"
proof -
  have "set (comp_min_basis xs)  set (filter (λx. x  0) xs)"
    unfolding comp_min_basis_def by (rule filter_min_subset)
  also have " = {x  set xs. x  0}" by simp
  finally show ?thesis .
qed

lemma comp_min_basis_subset: "set (comp_min_basis xs)  set xs"
proof -
  have "set (comp_min_basis xs)  {x  set xs. x  0}" by (rule comp_min_basis_subset')
  also have "...  set xs" by simp
  finally show ?thesis .
qed
    
lemma comp_min_basis_nonzero: "p  set (comp_min_basis xs)  p  0"
  using comp_min_basis_subset' by blast

lemma comp_min_basis_adds:
  assumes "p  set xs" and "p  0"
  obtains q where "q  set (comp_min_basis xs)" and "lt q addst lt p"
proof -
  let ?rel = "(λx y. lt x addst lt y)"
  have "transp ?rel" by (auto intro!: transpI dest: adds_term_trans)
  moreover have "reflp ?rel" by (simp add: reflp_def adds_term_refl)
  moreover from assms have "p  set (filter (λx. x  0) xs)" by simp
  ultimately obtain q where "q  set (comp_min_basis xs)" and "lt q addst lt p"
    unfolding comp_min_basis_def by (rule filter_min_relE)
  thus ?thesis ..
qed
  
lemma comp_min_basis_is_red:
  assumes "is_red (set xs) f"
  shows "is_red (set (comp_min_basis xs)) f"
proof -
  from assms obtain x t where "x  set xs" and "t  keys f" and "x  0" and "lt x addst t"
    by (rule is_red_addsE)
  from x  set xs x  0 obtain y where yin: "y  set (comp_min_basis xs)" and "lt y addst lt x"
    by (rule comp_min_basis_adds)
  show ?thesis
  proof (rule is_red_addsI)
    from lt y addst lt x lt x addst t show "lt y addst t" by (rule adds_term_trans)
  next
    from yin show "y  0" by (rule comp_min_basis_nonzero)
  qed fact+
qed

lemma comp_min_basis_nadds:
  assumes "p  set (comp_min_basis xs)" and "q  set (comp_min_basis xs)" and "p  q"
  shows "¬ lt q addst lt p"
proof
  have "transp (λx y. lt x addst lt y)" by (auto intro!: transpI dest: adds_term_trans)
  moreover note assms(2, 1)
  moreover assume "lt q addst lt p"
  ultimately have "q = p" unfolding comp_min_basis_def by (rule filter_min_minimal)
  with assms(3) show False by simp
qed

lemma comp_min_basis_is_minimal_basis: "is_minimal_basis (set (comp_min_basis xs))"
  by (rule is_minimal_basisI, rule comp_min_basis_nonzero, assumption, rule comp_min_basis_nadds,
      assumption+, simp)

lemma comp_min_basis_distinct: "distinct (comp_min_basis xs)"
  unfolding comp_min_basis_def by (rule filter_min_distinct) (simp add: reflp_def adds_term_refl)

end (* ordered_term *)

subsection ‹Auto-Reduction›

context gd_term
begin

lemma is_minimal_basis_trd_is_minimal_basis:
  assumes "is_minimal_basis (set (x # xs))" and "x  set xs"
  shows "is_minimal_basis (set ((trd xs x) # xs))"
proof -
  from assms(1) have "is_minimal_basis (insert (trd xs x) (set (x # xs) - {x}))"
  proof (rule is_minimal_basis_replace, simp)
    from assms(2) have eq: "set (x # xs) - {x} = set xs" by simp
    show "(red (set (x # xs) - {x}))** x (trd xs x)" unfolding eq by (rule trd_red_rtrancl)
  qed
  also from assms(2) have "... = set ((trd xs x) # xs)" by auto
  finally show ?thesis .
qed

lemma is_minimal_basis_trd_distinct:
  assumes min: "is_minimal_basis (set (x # xs))" and dist: "distinct (x # xs)"
  shows "distinct ((trd xs x) # xs)"
proof -
  let ?y = "trd xs x"
  from min have lty: "lt ?y = lt x"
  proof (rule minimal_basis_red_rtrancl_lt, simp)
    from dist have "x  set xs" by simp
    hence eq: "set (x # xs) - {x} = set xs" by simp
    show "(red (set (x # xs) - {x}))** x (trd xs x)" unfolding eq by (rule trd_red_rtrancl)
  qed
  have "?y  set xs"
  proof
    assume "?y  set xs"
    hence "?y  set (x # xs)" by simp
    with min have "¬ lt ?y addst lt x"
    proof (rule is_minimal_basisD2, simp)
      show "?y  x"
      proof
        assume "?y = x"
        from dist have "x  set xs" by simp
        with ?y  set xs show False unfolding ?y = x by simp
      qed
    qed
    thus False unfolding lty by (simp add: adds_term_refl)
  qed
  moreover from dist have "distinct xs" by simp
  ultimately show ?thesis by simp
qed

primrec comp_red_basis_aux :: "('t 0 'b) list  ('t 0 'b) list  ('t 0 'b::field) list" where
  comp_red_basis_aux_base: "comp_red_basis_aux Nil ys = ys"|
  comp_red_basis_aux_rec: "comp_red_basis_aux (x # xs) ys = comp_red_basis_aux xs ((trd (xs @ ys) x) # ys)"
  
lemma subset_comp_red_basis_aux: "set ys  set (comp_red_basis_aux xs ys)"
proof (induct xs arbitrary: ys)
  case Nil
  show ?case unfolding comp_red_basis_aux_base ..
next
  case (Cons a xs)
  have "set ys  set ((trd (xs @ ys) a) # ys)" by auto
  also have "...  set (comp_red_basis_aux xs ((trd (xs @ ys) a) # ys))" by (rule Cons.hyps)
  finally show ?case unfolding comp_red_basis_aux_rec .
qed

lemma comp_red_basis_aux_nonzero:
  assumes "is_minimal_basis (set (xs @ ys))" and "distinct (xs @ ys)" and "p  set (comp_red_basis_aux xs ys)"
  shows "p  0"
  using assms
proof (induct xs arbitrary: ys)
  case Nil
  show ?case
  proof (rule is_minimal_basisD1)
    from Nil(1) show "is_minimal_basis (set ys)" by simp
  next
    from Nil(3) show "p  set ys" unfolding comp_red_basis_aux_base .
  qed
next
  case (Cons a xs)
  have eq: "(a # xs) @ ys = a # (xs @ ys)" by simp
  have "a  set (a # xs @ ys)" by simp
  from Cons(3) have "a  set (xs @ ys)" unfolding eq by simp
  let ?ys = "trd (xs @ ys) a # ys"
  show ?case
  proof (rule Cons.hyps)
    from Cons(3) have "a  set (xs @ ys)" unfolding eq by simp
    with Cons(2) show "is_minimal_basis (set (xs @ ?ys))" unfolding set_reorder eq
      by (rule is_minimal_basis_trd_is_minimal_basis)
  next
    from Cons(2) Cons(3) show "distinct (xs @ ?ys)" unfolding distinct_reorder eq
      by (rule is_minimal_basis_trd_distinct)
  next
    from Cons(4) show "p  set (comp_red_basis_aux xs ?ys)" unfolding comp_red_basis_aux_rec .
  qed
qed
  
lemma comp_red_basis_aux_lt:
  assumes "is_minimal_basis (set (xs @ ys))" and "distinct (xs @ ys)"
  shows "lt ` set (xs @ ys) = lt ` set (comp_red_basis_aux xs ys)"
  using assms
proof (induct xs arbitrary: ys)
  case Nil
  show ?case unfolding comp_red_basis_aux_base by simp
next
  case (Cons a xs)
  have eq: "(a # xs) @ ys = a # (xs @ ys)" by simp
  from Cons(3) have a: "a  set (xs @ ys)" unfolding eq by simp
  let ?b = "trd (xs @ ys) a"
  let ?ys = "?b # ys"
  from Cons(2) have "lt ?b = lt a" unfolding eq
  proof (rule minimal_basis_red_rtrancl_lt, simp)
    from a have eq2: "set (a # xs @ ys) - {a} = set (xs @ ys)" by simp
    show "(red (set (a # xs @ ys) - {a}))** a ?b" unfolding eq2 by (rule trd_red_rtrancl)
  qed
  hence "lt ` set ((a # xs) @ ys) = lt ` set ((?b # xs) @ ys)" by simp
  also have "... = lt ` set (xs @ (?b # ys))" by simp
  finally have eq2: "lt ` set ((a # xs) @ ys) = lt ` set (xs @ (?b # ys))" .
  show ?case unfolding comp_red_basis_aux_rec eq2
  proof (rule Cons.hyps)
    from Cons(3) have "a  set (xs @ ys)" unfolding eq by simp
    with Cons(2) show "is_minimal_basis (set (xs @ ?ys))" unfolding set_reorder eq
      by (rule is_minimal_basis_trd_is_minimal_basis)
  next
    from Cons(2) Cons(3) show "distinct (xs @ ?ys)" unfolding distinct_reorder eq
      by (rule is_minimal_basis_trd_distinct)
  qed
qed
  
lemma comp_red_basis_aux_pmdl:
  assumes "is_minimal_basis (set (xs @ ys))" and "distinct (xs @ ys)"
  shows "pmdl (set (comp_red_basis_aux xs ys))  pmdl (set (xs @ ys))"
  using assms
proof (induct xs arbitrary: ys)
  case Nil
  show ?case unfolding comp_red_basis_aux_base by simp
next
  case (Cons a xs)
  have eq: "(a # xs) @ ys = a # (xs @ ys)" by simp
  from Cons(3) have a: "a  set (xs @ ys)" unfolding eq by simp
  let ?b = "trd (xs @ ys) a"
  let ?ys = "?b # ys"
  have "pmdl (set (comp_red_basis_aux xs ?ys))  pmdl (set (xs @ ?ys))"
  proof (rule Cons.hyps)
    from Cons(3) have "a  set (xs @ ys)" unfolding eq by simp
    with Cons(2) show "is_minimal_basis (set (xs @ ?ys))" unfolding set_reorder eq
      by (rule is_minimal_basis_trd_is_minimal_basis)
  next
    from Cons(2) Cons(3) show "distinct (xs @ ?ys)" unfolding distinct_reorder eq
      by (rule is_minimal_basis_trd_distinct)
  qed
  also have "... = pmdl (set (?b # xs @ ys))" by simp
  also from a have "... = pmdl (insert ?b (set (a # xs @ ys) - {a}))" by auto
  also have "...  pmdl (set (a # xs @ ys))"
  proof (rule pmdl.replace_span)
    have "a - (trd (xs @ ys) a)  pmdl (set (xs @ ys))" by (rule trd_in_pmdl)
    have "a - (trd (xs @ ys) a)  pmdl (set (a # xs @ ys))"
    proof
      show "pmdl (set (xs @ ys))  pmdl (set (a # xs @ ys))" by (rule pmdl.span_mono) auto
    qed fact
    hence "- (a - (trd (xs @ ys) a))  pmdl (set (a # xs @ ys))" by (rule pmdl.span_neg)
    hence "(trd (xs @ ys) a) - a  pmdl (set (a # xs @ ys))" by simp
    hence "((trd (xs @ ys) a) - a) + a  pmdl (set (a # xs @ ys))"
    proof (rule pmdl.span_add)
      show "a  pmdl (set (a # xs @ ys))"
      proof
        show "a  set (a # xs @ ys)" by simp
      qed (rule pmdl.span_superset)
    qed
    thus "trd (xs @ ys) a  pmdl (set (a # xs @ ys))" by simp
  qed
  also have "... = pmdl (set ((a # xs) @ ys))" by simp
  finally show ?case unfolding comp_red_basis_aux_rec .
qed
  
lemma comp_red_basis_aux_irred:
  assumes "is_minimal_basis (set (xs @ ys))" and "distinct (xs @ ys)"
    and "y. y  set ys  ¬ is_red (set (xs @ ys) - {y}) y"
    and "p  set (comp_red_basis_aux xs ys)"
  shows "¬ is_red (set (comp_red_basis_aux xs ys) - {p}) p"
  using assms
proof (induct xs arbitrary: ys)
  case Nil
  have "¬ is_red (set ([] @ ys) - {p}) p"
  proof (rule Nil(3))
    from Nil(4) show "p  set ys" unfolding comp_red_basis_aux_base .
  qed
  thus ?case unfolding comp_red_basis_aux_base by simp
next
  case (Cons a xs)
  have eq: "(a # xs) @ ys = a # (xs @ ys)" by simp
  from Cons(3) have a_notin: "a  set (xs @ ys)" unfolding eq by simp
  from Cons(2) have is_min: "is_minimal_basis (set (a # xs @ ys))" unfolding eq .
  let ?b = "trd (xs @ ys) a"
  let ?ys = "?b # ys"
  have dist: "distinct (?b # (xs @ ys))"
  proof (rule is_minimal_basis_trd_distinct, fact is_min)
    from Cons(3) show "distinct (a # xs @ ys)" unfolding eq .
  qed
  
  show ?case unfolding comp_red_basis_aux_rec
  proof (rule Cons.hyps)
    from Cons(2) a_notin show "is_minimal_basis (set (xs @ ?ys))" unfolding set_reorder eq
      by (rule is_minimal_basis_trd_is_minimal_basis)
  next
    from dist show "distinct (xs @ ?ys)" unfolding distinct_reorder .
  next
    fix y
    assume "y  set ?ys"
    hence "y = ?b  y  set ys" by simp
    thus "¬ is_red (set (xs @ ?ys) - {y}) y"
    proof
      assume "y = ?b"
      from dist have "?b  set (xs @ ys)" by simp
      hence eq3: "set (xs @ ?ys) - {?b} = set (xs @ ys)" unfolding set_reorder by simp
      have "¬ is_red (set (xs @ ys)) ?b" by (rule trd_irred)
      thus ?thesis unfolding y = ?b eq3 .
    next
      assume "y  set ys"
      hence irred: "¬ is_red (set ((a # xs) @ ys) - {y}) y" by (rule Cons(4))
      from y  set ys a_notin have "y  a" by auto
      hence eq3: "set ((a # xs) @ ys) - {y} = {a}  (set (xs @ ys) - {y})" by auto
      from irred have i1: "¬ is_red {a} y" and i2: "¬ is_red (set (xs @ ys) - {y}) y"
        unfolding eq3 is_red_union by simp_all
      show ?thesis unfolding set_reorder
      proof (cases "y = ?b")
        case True
        from i2 show "¬ is_red (set (?b # xs @ ys) - {y}) y" by (simp add: True)
      next
        case False
        hence eq4: "set (?b # xs @ ys) - {y} = {?b}  (set (xs @ ys) - {y})" by auto
        show "¬ is_red (set (?b # xs @ ys) - {y}) y" unfolding eq4
        proof
          assume "is_red ({?b}  (set (xs @ ys) - {y})) y"
          thus False unfolding is_red_union
          proof
            have ltb: "lt ?b = lt a"
            proof (rule minimal_basis_red_rtrancl_lt, fact is_min)
              show "a  set (a # xs @ ys)" by simp
            next
              from a_notin have eq: "set (a # xs @ ys) - {a} = set (xs @ ys)" by simp
              show "(red (set (a # xs @ ys) - {a}))** a ?b" unfolding eq by (rule trd_red_rtrancl)
            qed
            assume "is_red {?b} y"
            then obtain t where "t  keys y" and "lt ?b addst t" unfolding is_red_adds_iff by auto
            with ltb have "lt a addst t" by simp
            have "is_red {a} y"
              by (rule is_red_addsI, rule, rule is_minimal_basisD1, fact is_min, simp, fact+)
            with i1 show False ..
          next
            assume "is_red (set (xs @ ys) - {y}) y"
            with i2 show False ..
          qed
        qed
      qed
    qed
  next
    from Cons(5) show "p  set (comp_red_basis_aux xs ?ys)" unfolding comp_red_basis_aux_rec .
  qed
qed

lemma comp_red_basis_aux_dgrad_p_set_le:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d (set (comp_red_basis_aux xs ys)) (set xs  set ys)"
proof (induct xs arbitrary: ys)
  case Nil
  show ?case by (simp, rule dgrad_p_set_le_subset, fact subset_refl)
next
  case (Cons x xs)
  let ?h = "trd (xs @ ys) x"
  have "dgrad_p_set_le d (set (comp_red_basis_aux xs (?h # ys))) (set xs  set (?h # ys))"
    by (fact Cons)
  also have "... = insert ?h (set xs  set ys)" by simp
  also have "dgrad_p_set_le d ... (insert x (set xs  set ys))"
  proof (rule dgrad_p_set_leI_insert)
    show "dgrad_p_set_le d (set xs  set ys) (insert x (set xs  set ys))"
      by (rule dgrad_p_set_le_subset, blast)
  next
    have "(red (set (xs @ ys)))** x ?h" by (rule trd_red_rtrancl)
    with assms have "dgrad_p_set_le d {?h} (insert x (set (xs @ ys)))"
      by (rule dgrad_p_set_le_red_rtrancl)
    thus "dgrad_p_set_le d {?h} (insert x (set xs  set ys))" by simp
  qed
  finally show ?case by simp
qed

definition comp_red_basis :: "('t 0 'b) list  ('t 0 'b::field) list"
  where "comp_red_basis xs = comp_red_basis_aux (comp_min_basis xs) []"
  
lemma comp_red_basis_nonzero:
  assumes "p  set (comp_red_basis xs)"
  shows "p  0"
proof -
  have "is_minimal_basis (set ((comp_min_basis xs) @ []))" by (simp add: comp_min_basis_is_minimal_basis)
  moreover have "distinct ((comp_min_basis xs) @ [])" by (simp add: comp_min_basis_distinct)
  moreover from assms have "p  set (comp_red_basis_aux (comp_min_basis xs) [])" unfolding comp_red_basis_def .
  ultimately show ?thesis by (rule comp_red_basis_aux_nonzero)
qed

lemma pmdl_comp_red_basis_subset: "pmdl (set (comp_red_basis xs))  pmdl (set xs)"
proof
  fix f
  assume fin: "f  pmdl (set (comp_red_basis xs))"
  have "f  pmdl (set (comp_min_basis xs))"
  proof
    from fin show  "f  pmdl (set (comp_red_basis_aux (comp_min_basis xs) []))"
      unfolding comp_red_basis_def .
  next
    have "pmdl (set (comp_red_basis_aux (comp_min_basis xs) []))  pmdl (set ((comp_min_basis xs) @ []))"
      by (rule comp_red_basis_aux_pmdl, simp_all, rule comp_min_basis_is_minimal_basis, rule comp_min_basis_distinct)
    thus "pmdl (set (comp_red_basis_aux (comp_min_basis xs) []))  pmdl (set (comp_min_basis xs))"
      by simp
  qed
  also from comp_min_basis_subset have "...  pmdl (set xs)" by (rule pmdl.span_mono)
  finally show "f  pmdl (set xs)" .
qed

lemma comp_red_basis_adds:
  assumes "p  set xs" and "p  0"
  obtains q where "q  set (comp_red_basis xs)" and "lt q addst lt p"
proof -
  from assms obtain q1 where "q1  set (comp_min_basis xs)" and "lt q1 addst lt p"
    by (rule comp_min_basis_adds)
  from q1  set (comp_min_basis xs) have "lt q1  lt ` set (comp_min_basis xs)" by simp
  also have "... = lt ` set ((comp_min_basis xs) @ [])" by simp
  also have "... = lt ` set (comp_red_basis_aux (comp_min_basis xs) [])"
    by (rule comp_red_basis_aux_lt, simp_all, rule comp_min_basis_is_minimal_basis, rule comp_min_basis_distinct)
  finally obtain q where "q  set (comp_red_basis_aux (comp_min_basis xs) [])" and "lt q = lt q1"
    by auto
  show ?thesis
  proof
    show "q  set (comp_red_basis xs)" unfolding comp_red_basis_def by fact
  next
    from lt q1 addst lt p show "lt q addst lt p" unfolding lt q = lt q1 .
  qed
qed
  
lemma comp_red_basis_lt:
  assumes "p  set (comp_red_basis xs)"
  obtains q where "q  set xs" and "q  0" and "lt q = lt p"
proof -
  have eq: "lt ` set ((comp_min_basis xs) @ []) = lt ` set (comp_red_basis_aux (comp_min_basis xs) [])"
    by (rule comp_red_basis_aux_lt, simp_all, rule comp_min_basis_is_minimal_basis, rule comp_min_basis_distinct)
  from assms have "lt p  lt ` set (comp_red_basis xs)" by simp
  also have "... = lt ` set (comp_red_basis_aux (comp_min_basis xs) [])" unfolding comp_red_basis_def ..
  also have "... = lt ` set (comp_min_basis xs)" unfolding eq[symmetric] by simp
  finally obtain q where "q  set (comp_min_basis xs)" and "lt q = lt p" by auto
  show ?thesis
  proof
    show "q  set xs" by (rule, fact, rule comp_min_basis_subset)
  next
    show "q  0" by (rule comp_min_basis_nonzero, fact)
  qed fact
qed

lemma comp_red_basis_is_red: "is_red (set (comp_red_basis xs)) f  is_red (set xs) f"
proof
  assume "is_red (set (comp_red_basis xs)) f"
  then obtain x t where "x  set (comp_red_basis xs)" and "t  keys f" and "x  0" and "lt x addst t"
    by (rule is_red_addsE)
  from x  set (comp_red_basis xs) obtain y where yin: "y  set xs" and "y  0" and "lt y = lt x"
    by (rule comp_red_basis_lt)
  show "is_red (set xs) f"
  proof (rule is_red_addsI)
    from lt x addst t show "lt y addst t" unfolding lt y = lt x .
  qed fact+
next
  assume "is_red (set xs) f"
  then obtain x t where "x  set xs" and "t  keys f" and "x  0" and "lt x addst t"
    by (rule is_red_addsE)
  from x  set xs x  0 obtain y where yin: "y  set (comp_red_basis xs)" and "lt y addst lt x"
    by (rule comp_red_basis_adds)
  show "is_red (set (comp_red_basis xs)) f"
  proof (rule is_red_addsI)
    from lt y addst lt x lt x addst t show "lt y addst t" by (rule adds_term_trans)
  next
    from yin show "y  0" by (rule comp_red_basis_nonzero)
  qed fact+
qed
    
lemma comp_red_basis_is_auto_reduced: "is_auto_reduced (set (comp_red_basis xs))"
  unfolding is_auto_reduced_def remove_def
proof (intro ballI)
  fix x
  assume xin: "x  set (comp_red_basis xs)"
  show "¬ is_red (set (comp_red_basis xs) - {x}) x" unfolding comp_red_basis_def
  proof (rule comp_red_basis_aux_irred, simp_all, rule comp_min_basis_is_minimal_basis, rule comp_min_basis_distinct)
    from xin show "x  set (comp_red_basis_aux (comp_min_basis xs) [])" unfolding comp_red_basis_def .
  qed
qed

lemma comp_red_basis_dgrad_p_set_le:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d (set (comp_red_basis xs)) (set xs)"
proof -
  have "dgrad_p_set_le d (set (comp_red_basis xs)) (set (comp_min_basis xs)  set [])"
    unfolding comp_red_basis_def using assms by (rule comp_red_basis_aux_dgrad_p_set_le)
  also have "... = set (comp_min_basis xs)" by simp
  also from comp_min_basis_subset have "dgrad_p_set_le d ... (set xs)"
    by (rule dgrad_p_set_le_subset)
  finally show ?thesis .
qed

subsection ‹Auto-Reduction and Monicity›

definition comp_red_monic_basis :: "('t 0 'b) list  ('t 0 'b::field) list" where
  "comp_red_monic_basis xs = map monic (comp_red_basis xs)"

lemma set_comp_red_monic_basis: "set (comp_red_monic_basis xs) = monic ` (set (comp_red_basis xs))"
  by (simp add: comp_red_monic_basis_def)

lemma comp_red_monic_basis_nonzero:
  assumes "p  set (comp_red_monic_basis xs)"
  shows "p  0"
proof -
  from assms obtain p' where p_def: "p = monic p'" and p': "p'  set (comp_red_basis xs)"
    unfolding set_comp_red_monic_basis ..
  from p' have "p'  0" by (rule comp_red_basis_nonzero)
  thus ?thesis unfolding p_def monic_0_iff .
qed

lemma comp_red_monic_basis_is_monic_set: "is_monic_set (set (comp_red_monic_basis xs))"
  unfolding set_comp_red_monic_basis by (rule image_monic_is_monic_set)

lemma pmdl_comp_red_monic_basis_subset: "pmdl (set (comp_red_monic_basis xs))  pmdl (set xs)"
  unfolding set_comp_red_monic_basis pmdl_image_monic by (fact pmdl_comp_red_basis_subset)

lemma comp_red_monic_basis_is_auto_reduced: "is_auto_reduced (set (comp_red_monic_basis xs))"
  unfolding set_comp_red_monic_basis by (rule image_monic_is_auto_reduced, rule comp_red_basis_is_auto_reduced)

lemma comp_red_monic_basis_dgrad_p_set_le:
  assumes "dickson_grading d"
  shows "dgrad_p_set_le d (set (comp_red_monic_basis xs)) (set xs)"
proof -
  have "dgrad_p_set_le d (monic ` (set (comp_red_basis xs))) (set (comp_red_basis xs))"
    by (simp add: dgrad_p_set_le_def, fact dgrad_set_le_refl)
  also from assms have "dgrad_p_set_le d ... (set xs)" by (rule comp_red_basis_dgrad_p_set_le)
  finally show ?thesis by (simp add: set_comp_red_monic_basis)
qed

end (* gd_term *)

end (* theory *)