Nullstellensatz.thy

(* Author: Alexander Maletzky *)

section \<open>Hilbert's Nullstellensatz\<close>

theory Nullstellensatz
  imports Algebraically_Closed_Fields
          "HOL-Computational_Algebra.Fraction_Field"
          Lex_Order_PP
          Univariate_PM
          Groebner_Bases.Groebner_PM
begin

text \<open>We prove the geometric version of Hilbert's Nullstellensatz, i.e. the precise correspondence
  between algebraic varieties and radical ideals.
  The field-theoretic version of the Nullstellensatz is proved in theory \<open>Nullstellensatz_Field\<close>.\<close>

subsection \<open>Preliminaries\<close>

lemma finite_linorder_induct [consumes 1, case_names empty insert]:
  assumes "finite (A::'a::linorder set)" and "P {}"
    and "\<And>a A. finite A \<Longrightarrow> A \<subseteq> {..<a} \<Longrightarrow> P A \<Longrightarrow> P (insert a A)"
  shows "P A"
proof -
  define k where "k = card A"
  thus ?thesis using assms(1)
  proof (induct k arbitrary: A)
    case 0
    with assms(2) show ?case by simp
  next
    case (Suc k)
    define a where "a = Max A"
    from Suc.prems(1) have "A \<noteq> {}" by auto
    with Suc.prems(2) have "a \<in> A" unfolding a_def by (rule Max_in)
    with Suc.prems have "k = card (A - {a})" by simp
    moreover from Suc.prems(2) have "finite (A - {a})" by simp
    ultimately have "P (A - {a})" by (rule Suc.hyps)
    with \<open>finite (A - {a})\<close> _ have "P (insert a (A - {a}))"
    proof (rule assms(3))
      show "A - {a} \<subseteq> {..<a}"
      proof
        fix b
        assume "b \<in> A - {a}"
        hence "b \<in> A" and "b \<noteq> a" by simp_all
        moreover from Suc.prems(2) this(1) have "b \<le> a" unfolding a_def by (rule Max_ge)
        ultimately show "b \<in> {..<a}" by simp
      qed
    qed
    with \<open>a \<in> A\<close> show ?case by (simp add: insert_absorb)
  qed
qed

lemma Fract_same: "Fract a a = (1 when a \<noteq> 0)"
  by (simp add: One_fract_def Zero_fract_def eq_fract when_def)

lemma Fract_eq_zero_iff: "Fract a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
  by (metis (no_types, lifting) Zero_fract_def eq_fract(1) eq_fract(2) mult_eq_0_iff one_neq_zero)

lemma poly_plus_rightE:
  obtains c where "poly p (x + y) = poly p x + c * y"
proof (induct p arbitrary: thesis)
  case 0
  have "poly 0 (x + y) = poly 0 x + 0 * y" by simp
  thus ?case by (rule 0)
next
  case (pCons a p)
  obtain c where "poly p (x + y) = poly p x + c * y" by (rule pCons.hyps)
  hence "poly (pCons a p) (x + y) = a + (x + y) * (poly p x + c * y)" by simp
  also have "\<dots> = poly (pCons a p) x + (x * c + (poly p x + c * y)) * y" by (simp add: algebra_simps)
  finally show ?case by (rule pCons.prems)
qed

lemma poly_minus_rightE:
  obtains c where "poly p (x - y) = poly p x - c * (y::_::comm_ring)"
  by (metis (no_types, hide_lams) add_uminus_conv_diff linordered_field_class.sign_simps(5)
      mult_minus_left poly_plus_rightE)

lemma map_poly_plus:
  assumes "f 0 = 0" and "\<And>a b. f (a + b) = f a + f b"
  shows "map_poly f (p + q) = map_poly f p + map_poly f q"
  by (rule Polynomial.poly_eqI) (simp add: coeff_map_poly assms)

lemma map_poly_minus:
  assumes "f 0 = 0" and "\<And>a b. f (a - b) = f a - f b"
  shows "map_poly f (p - q) = map_poly f p - map_poly f q"
  by (rule Polynomial.poly_eqI) (simp add: coeff_map_poly assms)

lemma map_poly_sum:
  assumes "f 0 = 0" and "\<And>a b. f (a + b) = f a + f b"
  shows "map_poly f (sum g A) = (\<Sum>a\<in>A. map_poly f (g a))"
  by (induct A rule: infinite_finite_induct) (simp_all add: map_poly_plus assms)

lemma map_poly_times:
  assumes "f 0 = 0" and "\<And>a b. f (a + b) = f a + f b" and "\<And>a b. f (a * b) = f a * f b"
  shows "map_poly f (p * q) = map_poly f p * map_poly f q"
proof (induct p)
  case 0
  show ?case by simp
next
  case (pCons c p)
  show ?case by (simp add: assms map_poly_plus map_poly_smult map_poly_pCons pCons)
qed

lemma poly_Fract:
  assumes "set (Polynomial.coeffs p) \<subseteq> range (\<lambda>x. Fract x 1)"
  obtains q m where "poly p (Fract a b) = Fract q (b ^ m)"
  using assms
proof (induct p arbitrary: thesis)
  case 0
  have "poly 0 (Fract a b) = Fract 0 (b ^ 1)" by (simp add: fract_collapse)
  thus ?case by (rule 0)
next
  case (pCons c p)
  from pCons.hyps(1) have "insert c (set (Polynomial.coeffs p)) = set (Polynomial.coeffs (pCons c p))"
    by auto
  with pCons.prems(2) have "c \<in> range (\<lambda>x. Fract x 1)" and "set (Polynomial.coeffs p) \<subseteq> range (\<lambda>x. Fract x 1)"
    by blast+
  from this(2) obtain q0 m0 where poly_p: "poly p (Fract a b) = Fract q0 (b ^ m0)"
    using pCons.hyps(2) by blast
  from \<open>c \<in> _\<close> obtain c0 where c: "c = Fract c0 1" ..
  show ?case
  proof (cases "b = 0")
    case True
    hence "poly (pCons c p) (Fract a b) = Fract c0 (b ^ 0)" by (simp add: c fract_collapse)
    thus ?thesis by (rule pCons.prems)
  next
    case False
    hence "poly (pCons c p) (Fract a b) = Fract (c0 * b ^ Suc m0 + a * q0) (b ^ Suc m0)"
      by (simp add: poly_p c)
    thus ?thesis by (rule pCons.prems)
  qed
qed

lemma (in ordered_term) lt_sum_le_Max: "lt (sum f A) \<preceq>\<^sub>t ord_term_lin.Max {lt (f a) | a. a \<in> A}"
proof (induct A rule: infinite_finite_induct)
  case (infinite A)
  thus ?case by (simp add: min_term_min)
next
  case empty
  thus ?case by (simp add: min_term_min)
next
  case (insert a A)
  show ?case
  proof (cases "A = {}")
    case True
    thus ?thesis by simp
  next
    case False
    from insert.hyps(1, 2) have "lt (sum f (insert a A)) = lt (f a + sum f A)" by simp
    also have "\<dots> \<preceq>\<^sub>t ord_term_lin.max (lt (f a)) (lt (sum f A))" by (rule lt_plus_le_max)
    also have "\<dots> \<preceq>\<^sub>t ord_term_lin.max (lt (f a)) (ord_term_lin.Max {lt (f a) |a. a \<in> A})"
      using insert.hyps(3) ord_term_lin.max.mono by blast
    also from insert.hyps(1) False have "\<dots> = ord_term_lin.Max (insert (lt (f a)) {lt (f x) |x. x \<in> A})"
      by simp
    also have "\<dots> = ord_term_lin.Max {lt (f x) |x. x \<in> insert a A}"
      by (rule arg_cong[where f=ord_term_lin.Max]) blast
    finally show ?thesis .
  qed
qed

subsection \<open>Ideals and Varieties\<close>

definition variety_of :: "(('x \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) set \<Rightarrow> ('x \<Rightarrow> 'a::comm_semiring_1) set"
  where "variety_of F = {a. \<forall>f\<in>F. poly_eval a f = 0}"

definition ideal_of :: "('x \<Rightarrow> 'a::comm_semiring_1) set \<Rightarrow> (('x \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) set"
  where "ideal_of A = {f. \<forall>a\<in>A. poly_eval a f = 0}"

abbreviation "\<V> \<equiv> variety_of"
abbreviation "\<I> \<equiv> ideal_of"

lemma variety_ofI: "(\<And>f. f \<in> F \<Longrightarrow> poly_eval a f = 0) \<Longrightarrow> a \<in> \<V> F"
  by (simp add: variety_of_def)

lemma variety_ofI_alt: "poly_eval a ` F \<subseteq> {0} \<Longrightarrow> a \<in> \<V> F"
  by (auto intro: variety_ofI)

lemma variety_ofD: "a \<in> \<V> F \<Longrightarrow> f \<in> F \<Longrightarrow> poly_eval a f = 0"
  by (simp add: variety_of_def)

lemma variety_of_empty [simp]: "\<V> {} = UNIV"
  by (simp add: variety_of_def)

lemma variety_of_UNIV [simp]: "\<V> UNIV = {}"
  by (metis (mono_tags, lifting) Collect_empty_eq UNIV_I one_neq_zero poly_eval_one variety_of_def)

lemma variety_of_antimono: "F \<subseteq> G \<Longrightarrow> \<V> G \<subseteq> \<V> F"
  by (auto simp: variety_of_def)

lemma variety_of_ideal [simp]: "\<V> (ideal F) = \<V> F"
proof
  show "\<V> (ideal F) \<subseteq> \<V> F" by (intro variety_of_antimono ideal.span_superset)
next
  show "\<V> F \<subseteq> \<V> (ideal F)"
  proof (intro subsetI variety_ofI)
    fix a f
    assume "a \<in> \<V> F" and "f \<in> ideal F"
    from this(2) show "poly_eval a f = 0"
    proof (induct f rule: ideal.span_induct_alt)
      case base
      show ?case by simp
    next
      case (step c f g)
      with \<open>a \<in> \<V> F\<close> show ?case by (auto simp: poly_eval_plus poly_eval_times dest: variety_ofD)
    qed
  qed
qed

lemma ideal_ofI: "(\<And>a. a \<in> A \<Longrightarrow> poly_eval a f = 0) \<Longrightarrow> f \<in> \<I> A"
  by (simp add: ideal_of_def)

lemma ideal_ofD: "f \<in> \<I> A \<Longrightarrow> a \<in> A \<Longrightarrow> poly_eval a f = 0"
  by (simp add: ideal_of_def)

lemma ideal_of_empty [simp]: "\<I> {} = UNIV"
  by (simp add: ideal_of_def)

lemma ideal_of_antimono: "A \<subseteq> B \<Longrightarrow> \<I> B \<subseteq> \<I> A"
  by (auto simp: ideal_of_def)

lemma ideal_ideal_of [simp]: "ideal (\<I> A) = \<I> A"
  unfolding ideal.span_eq_iff
proof (rule ideal.subspaceI)
  show "0 \<in> \<I> A" by (rule ideal_ofI) simp
next
  fix f g
  assume "f \<in> \<I> A"
  hence f: "poly_eval a f = 0" if "a \<in> A" for a using that by (rule ideal_ofD)
  assume "g \<in> \<I> A"
  hence g: "poly_eval a g = 0" if "a \<in> A" for a using that by (rule ideal_ofD)
  show "f + g \<in> \<I> A" by (rule ideal_ofI) (simp add: poly_eval_plus f g)
next
  fix c f
  assume "f \<in> \<I> A"
  hence f: "poly_eval a f = 0" if "a \<in> A" for a using that by (rule ideal_ofD)
  show "c * f \<in> \<I> A" by (rule ideal_ofI) (simp add: poly_eval_times f)
qed

lemma ideal_of_UN: "\<I> (\<Union> (A ` J)) = (\<Inter>j\<in>J. \<I> (A j))"
proof (intro set_eqI iffI ideal_ofI INT_I)
  fix p j a
  assume "p \<in> \<I> (\<Union> (A ` J))"
  assume "j \<in> J" and "a \<in> A j"
  hence "a \<in> \<Union> (A ` J)" ..
  with \<open>p \<in> _\<close> show "poly_eval a p = 0" by (rule ideal_ofD)
next
  fix p a
  assume "a \<in> \<Union> (A ` J)"
  then obtain j where "j \<in> J" and "a \<in> A j" ..
  assume "p \<in> (\<Inter>j\<in>J. \<I> (A j))"
  hence "p \<in> \<I> (A j)" using \<open>j \<in> J\<close> ..
  thus "poly_eval a p = 0" using \<open>a \<in> A j\<close> by (rule ideal_ofD)
qed

corollary ideal_of_Un: "\<I> (A \<union> B) = \<I> A \<inter> \<I> B"
  using ideal_of_UN[of id "{A, B}"] by simp

lemma variety_of_ideal_of_variety [simp]: "\<V> (\<I> (\<V> F)) = \<V> F" (is "_ = ?V")
proof
  have "F \<subseteq> \<I> (\<V> F)" by (auto intro!: ideal_ofI dest: variety_ofD)
  thus "\<V> (\<I> ?V) \<subseteq> ?V" by (rule variety_of_antimono)
next
  show "?V \<subseteq> \<V> (\<I> ?V)" by (auto intro!: variety_ofI dest: ideal_ofD)
qed

lemma ideal_of_inj_on: "inj_on \<I> (range (\<V>::(('x \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a::comm_semiring_1) set \<Rightarrow> _))"
proof (rule inj_onI)
  fix A B :: "('x \<Rightarrow> 'a) set"
  assume "A \<in> range \<V>"
  then obtain F where A: "A = \<V> F" ..
  assume "B \<in> range \<V>"
  then obtain G where B: "B = \<V> G" ..
  assume "\<I> A = \<I> B"
  hence "\<V> (\<I> A) = \<V> (\<I> B)" by simp
  thus "A = B" by (simp add: A B)
qed

lemma ideal_of_variety_of_ideal [simp]: "\<I> (\<V> (\<I> A)) = \<I> A" (is "_ = ?I")
proof
  have "A \<subseteq> \<V> (\<I> A)" by (auto intro!: variety_ofI dest: ideal_ofD)
  thus "\<I> (\<V> ?I) \<subseteq> ?I" by (rule ideal_of_antimono)
next
  show "?I \<subseteq> \<I> (\<V> ?I)" by (auto intro!: ideal_ofI dest: variety_ofD)
qed

lemma variety_of_inj_on: "inj_on \<V> (range (\<I>::('x \<Rightarrow> 'a::comm_semiring_1) set \<Rightarrow> _))"
proof (rule inj_onI)
  fix F G :: "(('x \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a) set"
  assume "F \<in> range \<I>"
  then obtain A where F: "F = \<I> A" ..
  assume "G \<in> range \<I>"
  then obtain B where G: "G = \<I> B" ..
  assume "\<V> F = \<V> G"
  hence "\<I> (\<V> F) = \<I> (\<V> G)" by simp
  thus "F = G" by (simp add: F G)
qed

lemma image_map_indets_ideal_of:
  assumes "inj f"
  shows "map_indets f ` \<I> A = \<I> ((\<lambda>a. a \<circ> f) -` (A::('x \<Rightarrow> 'a::comm_semiring_1) set)) \<inter> P[range f]"
proof -
  {
    fix p and a::"'x \<Rightarrow> 'a"
    assume "\<forall>a\<in>(\<lambda>a. a \<circ> f) -` A. poly_eval (a \<circ> f) p = 0"
    hence eq: "poly_eval (a \<circ> f) p = 0" if "a \<circ> f \<in> A" for a using that by simp
    have "the_inv f \<circ> f = id" by (rule ext) (simp add: assms the_inv_f_f)
    hence a: "a = a \<circ> the_inv f \<circ> f" by (simp add: comp_assoc)
    moreover assume "a \<in> A"
    ultimately have "(a \<circ> the_inv f) \<circ> f \<in> A" by simp
    hence "poly_eval ((a \<circ> the_inv f) \<circ> f) p = 0" by (rule eq)
    hence "poly_eval a p = 0" by (simp flip: a)
  }
  thus ?thesis
    by (auto simp: ideal_of_def poly_eval_map_indets simp flip: range_map_indets intro!: imageI)
qed

lemma variety_of_map_indets: "\<V> (map_indets f ` F) = (\<lambda>a. a \<circ> f) -` \<V> F"
  by (auto simp: variety_of_def poly_eval_map_indets)

subsection \<open>Radical Ideals\<close>

definition radical :: "'a::monoid_mult set \<Rightarrow> 'a set" ("\<surd>(_)" [999] 999)
  where "radical F = {f. \<exists>m. f ^ m \<in> F}"

lemma radicalI: "f ^ m \<in> F \<Longrightarrow> f \<in> \<surd>F"
  by (auto simp: radical_def)

lemma radicalE:
  assumes "f \<in> \<surd>F"
  obtains m where "f ^ m \<in> F"
  using assms by (auto simp: radical_def)

lemma radical_empty [simp]: "\<surd>{} = {}"
  by (simp add: radical_def)

lemma radical_UNIV [simp]: "\<surd>UNIV = UNIV"
  by (simp add: radical_def)

lemma radical_ideal_eq_UNIV_iff: "\<surd>ideal F = UNIV \<longleftrightarrow> ideal F = UNIV"
proof
  assume "\<surd>ideal F = UNIV"
  hence "1 \<in> \<surd>ideal F" by simp
  then obtain m where "1 ^ m \<in> ideal F" by (rule radicalE)
  thus "ideal F = UNIV" by (simp add: ideal_eq_UNIV_iff_contains_one)
qed simp

lemma zero_in_radical_ideal [simp]: "0 \<in> \<surd>ideal F"
proof (rule radicalI)
  show "0 ^ 1 \<in> ideal F" by (simp add: ideal.span_zero)
qed

lemma radical_mono: "F \<subseteq> G \<Longrightarrow> \<surd>F \<subseteq> \<surd>G"
  by (auto elim!: radicalE intro: radicalI)

lemma radical_superset: "F \<subseteq> \<surd>F"
proof
  fix f
  assume "f \<in> F"
  hence "f ^ 1 \<in> F" by simp
  thus "f \<in> \<surd>F" by (rule radicalI)
qed

lemma radical_idem [simp]: "\<surd>\<surd>F = \<surd>F"
proof
  show "\<surd>\<surd>F \<subseteq> \<surd>F" by (auto elim!: radicalE intro: radicalI simp flip: power_mult)
qed (fact radical_superset)

lemma radical_Int_subset: "\<surd>(A \<inter> B) \<subseteq> \<surd>A \<inter> \<surd>B"
  by (auto intro: radicalI elim: radicalE)

lemma radical_ideal_Int: "\<surd>(ideal F \<inter> ideal G) = \<surd>ideal F \<inter> \<surd>ideal G"
  using radical_Int_subset
proof (rule subset_antisym)
  show "\<surd>ideal F \<inter> \<surd>ideal G \<subseteq> \<surd>(ideal F \<inter> ideal G)"
  proof
    fix p
    assume "p \<in> \<surd>ideal F \<inter> \<surd>ideal G"
    hence "p \<in> \<surd>ideal F" and "p \<in> \<surd>ideal G" by simp_all
    from this(1) obtain m1 where p1: "p ^ m1 \<in> ideal F" by (rule radicalE)
    from \<open>p \<in> \<surd>ideal G\<close> obtain m2 where "p ^ m2 \<in> ideal G" by (rule radicalE)
    hence "p ^ m1 * p ^ m2 \<in> ideal G" by (rule ideal.span_scale)
    moreover from p1 have "p ^ m2 * p ^ m1 \<in> ideal F" by (rule ideal.span_scale)
    ultimately have "p ^ (m1 + m2) \<in> ideal F \<inter> ideal G" by (simp add: power_add mult.commute)
    thus "p \<in> \<surd>(ideal F \<inter> ideal G)" by (rule radicalI)
  qed
qed

lemma ideal_radical_ideal [simp]: "ideal (\<surd>ideal F) = \<surd>ideal F" (is "_ = ?R")
  unfolding ideal.span_eq_iff
proof (rule ideal.subspaceI)
  have "0 ^ 1 \<in> ideal F" by (simp add: ideal.span_zero)
  thus "0 \<in> ?R" by (rule radicalI)
next
  fix a b
  assume "a \<in> ?R"
  then obtain m where "a ^ m \<in> ideal F" by (rule radicalE)
  have a: "a ^ k \<in> ideal F" if "m \<le> k" for k
  proof -
    from \<open>a ^ m \<in> _\<close> have "a ^ (k - m + m) \<in> ideal F" by (simp only: power_add ideal.span_scale)
    with that show ?thesis by simp
  qed
  assume "b \<in> ?R"
  then obtain n where "b ^ n \<in> ideal F" by (rule radicalE)
  have b: "b ^ k \<in> ideal F" if "n \<le> k" for k
  proof -
    from \<open>b ^ n \<in> _\<close> have "b ^ (k - n + n) \<in> ideal F" by (simp only: power_add ideal.span_scale)
    with that show ?thesis by simp
  qed
  have "(a + b) ^ (m + n) \<in> ideal F" unfolding binomial_ring
  proof (rule ideal.span_sum)
    fix k
    show "of_nat (m + n choose k) * a ^ k * b ^ (m + n - k) \<in> ideal F"
    proof (cases "k \<le> m")
      case True
      hence "n \<le> m + n - k" by simp
      hence "b ^ (m + n - k) \<in> ideal F" by (rule b)
      thus ?thesis by (rule ideal.span_scale)
    next
      case False
      hence "m \<le> k" by simp
      hence "a ^ k \<in> ideal F" by (rule a)
      hence "of_nat (m + n choose k) * b ^ (m + n - k) * a ^ k \<in> ideal F" by (rule ideal.span_scale)
      thus ?thesis by (simp only: ac_simps)
    qed
  qed
  thus "a + b \<in> ?R" by (rule radicalI)
next
  fix c a
  assume "a \<in> ?R"
  then obtain m where "a ^ m \<in> ideal F" by (rule radicalE)
  hence "(c * a) ^ m \<in> ideal F" by (simp only: power_mult_distrib ideal.span_scale)
  thus "c * a \<in> ?R" by (rule radicalI)
qed

lemma radical_ideal_of [simp]: "\<surd>\<I> A = \<I> (A::(_ \<Rightarrow> _::semiring_1_no_zero_divisors) set)"
proof
  show "\<surd>\<I> A \<subseteq> \<I> A" by (auto elim!: radicalE dest!: ideal_ofD intro!: ideal_ofI simp: poly_eval_power)
qed (fact radical_superset)

lemma variety_of_radical_ideal [simp]: "\<V> (\<surd>ideal F) = \<V> (F::(_ \<Rightarrow>\<^sub>0 _::semiring_1_no_zero_divisors) set)"
proof
  have "F \<subseteq> ideal F" by (rule ideal.span_superset)
  also have "\<dots> \<subseteq> \<surd>ideal F" by (rule radical_superset)
  finally show "\<V> (\<surd>ideal F) \<subseteq> \<V> F" by (rule variety_of_antimono)
next
  show "\<V> F \<subseteq> \<V> (\<surd>ideal F)"
  proof (intro subsetI variety_ofI)
    fix a f
    assume "a \<in> \<V> F"
    hence "a \<in> \<V> (ideal F)" by simp
    assume "f \<in> \<surd>ideal F"
    then obtain m where "f ^ m \<in> ideal F" by (rule radicalE)
    with \<open>a \<in> \<V> (ideal F)\<close> have "poly_eval a (f ^ m) = 0" by (rule variety_ofD)
    thus "poly_eval a f = 0" by (simp add: poly_eval_power)
  qed
qed

lemma image_map_indets_radical:
  assumes "inj f"
  shows "map_indets f ` \<surd>F = \<surd>(map_indets f ` (F::(_ \<Rightarrow>\<^sub>0 'a::comm_ring_1) set)) \<inter> P[range f]"
proof
  show "map_indets f ` \<surd>F \<subseteq> \<surd>(map_indets f ` F) \<inter> P[range f]"
    by (auto simp: radical_def simp flip: map_indets_power range_map_indets intro!: imageI)
next
  show "\<surd>(map_indets f ` F) \<inter> P[range f] \<subseteq> map_indets f ` \<surd>F"
  proof
    fix p
    assume "p \<in> \<surd>(map_indets f ` F) \<inter> P[range f]"
    hence "p \<in> \<surd>(map_indets f ` F)" and "p \<in> range (map_indets f)"
      by (simp_all add: range_map_indets)
    from this(1) obtain m where "p ^ m \<in> map_indets f ` F" by (rule radicalE)
    then obtain q where "q \<in> F" and p_m: "p ^ m = map_indets f q" ..
    from assms obtain g where "g \<circ> f = id" and "map_indets g \<circ> map_indets f = (id::_ \<Rightarrow> _ \<Rightarrow>\<^sub>0 'a)"
      by (rule map_indets_inverseE)
    hence eq: "map_indets g (map_indets f p') = p'" for p'::"_ \<Rightarrow>\<^sub>0 'a"
      by (simp add: pointfree_idE)
    from p_m have "map_indets g (p ^ m) = map_indets g (map_indets f q)" by (rule arg_cong)
    hence "(map_indets g p) ^ m = q" by (simp add: eq)
    from \<open>p \<in> range _\<close> obtain p' where "p = map_indets f p'" ..
    hence "p = map_indets f (map_indets g p)" by (simp add: eq)
    moreover have "map_indets g p \<in> \<surd>F"
    proof (rule radicalI)
      from \<open>q \<in> F\<close> show "map_indets g p ^ m \<in> F" by (simp add: p_m eq flip: map_indets_power)
    qed
    ultimately show "p \<in> map_indets f ` \<surd>F" by (rule image_eqI)
  qed
qed

subsection \<open>Geometric Version of the Nullstellensatz\<close>

lemma weak_Nullstellensatz_aux_1:
  assumes "\<And>i. i \<in> I \<Longrightarrow> g i \<in> ideal B"
  obtains c where "c \<in> ideal B" and "(\<Prod>i\<in>I. (f i + g i) ^ m i) = (\<Prod>i\<in>I. f i ^ m i) + c"
  using assms
proof (induct I arbitrary: thesis rule: infinite_finite_induct)
  case (infinite I)
  from ideal.span_zero show ?case by (rule infinite) (simp add: infinite(1))
next
  case empty
  from ideal.span_zero show ?case by (rule empty) simp
next
  case (insert j I)
  have "g i \<in> ideal B" if "i \<in> I" for i by (rule insert.prems) (simp add: that)
  with insert.hyps(3) obtain c where c: "c \<in> ideal B"
    and 1: "(\<Prod>i\<in>I. (f i + g i) ^ m i) = (\<Prod>i\<in>I. f i ^ m i) + c" by blast
  define k where "k = m j"
  obtain d where 2: "(f j + g j) ^ m j = f j ^ m j + d * g j" unfolding k_def[symmetric]
  proof (induct k arbitrary: thesis)
    case 0
    have "(f j + g j) ^ 0 = f j ^ 0 + 0 * g j" by simp
    thus ?case by (rule 0)
  next
    case (Suc k)
    obtain d where "(f j + g j) ^ k = f j ^ k + d * g j" by (rule Suc.hyps)
    hence "(f j + g j) ^ Suc k = (f j ^ k + d * g j) * (f j + g j)" by simp
    also have "\<dots> = f j ^ Suc k + (f j ^ k + d * (f j + g j)) * g j" by (simp add: algebra_simps)
    finally show ?case by (rule Suc.prems)
  qed
  from c have *: "f j ^ m j * c + (((\<Prod>i\<in>I. f i ^ m i) + c) * d) * g j \<in> ideal B" (is "?c \<in> _")
    by (intro ideal.span_add ideal.span_scale insert.prems insertI1)
  from insert.hyps(1, 2) have "(\<Prod>i\<in>insert j I. (f i + g i) ^ m i) =
                                (f j ^ m j + d * g j) * ((\<Prod>i\<in>I. f i ^ m i) + c)"
    by (simp add: 1 2)
  also from insert.hyps(1, 2) have "\<dots> = (\<Prod>i\<in>insert j I. f i ^ m i) + ?c" by (simp add: algebra_simps)
  finally have "(\<Prod>i\<in>insert j I. (f i + g i) ^ m i) = (\<Prod>i\<in>insert j I. f i ^ m i) + ?c" .
  with * show ?case by (rule insert.prems)
qed

lemma weak_Nullstellensatz_aux_2:
  assumes "finite X" and "F \<subseteq> P[insert x X]" and "X \<subseteq> {..<x::'x::{countable,linorder}}"
    and "1 \<notin> ideal F" and "ideal F \<inter> P[{x}] \<subseteq> {0}"
  obtains a::"'a::alg_closed_field" where "1 \<notin> ideal (poly_eval (\<lambda>_. monomial a 0) ` focus {x} ` F)"
proof -
  let ?x = "monomial 1 (Poly_Mapping.single x 1)"
  from assms(3) have "x \<notin> X" by blast
  hence eq1: "insert x X - {x} = X" and eq2: "insert x X - X = {x}" by blast+

  interpret i: pm_powerprod lex_pm "lex_pm_strict::('x \<Rightarrow>\<^sub>0 nat) \<Rightarrow> _"
    unfolding lex_pm_def lex_pm_strict_def
    by standard (simp_all add: lex_pm_zero_min lex_pm_plus_monotone flip: lex_pm_def)
  have lpp_focus: "i.lpp (focus X g) = except (i.lpp g) {x}" if "g \<in> P[insert x X]" for g::"_ \<Rightarrow>\<^sub>0 'a"
  proof (cases "g = 0")
    case True
    thus ?thesis by simp
  next
    case False
    have keys_focus_g: "keys (focus X g) = (\<lambda>t. except t {x}) ` keys g"
      unfolding keys_focus using refl
    proof (rule image_cong)
      fix t
      assume "t \<in> keys g"
      also from that have "\<dots> \<subseteq> .[insert x X]" by (rule PolysD)
      finally have "keys t \<subseteq> insert x X" by (rule PPsD)
      hence "except t (- X) = except t (insert x X \<inter> - X)"
        by (metis (no_types, lifting) Int_commute except_keys_Int inf.orderE inf_left_commute)
      also from \<open>x \<notin> X\<close> have "insert x X \<inter> - X = {x}" by simp
      finally show "except t (- X) = except t {x}" .
    qed
    show ?thesis
    proof (rule i.punit.lt_eqI_keys)
      from False have "i.lpp g \<in> keys g" by (rule i.punit.lt_in_keys)
      thus "except (i.lpp g) {x} \<in> keys (focus X g)" unfolding keys_focus_g by (rule imageI)

      fix t
      assume "t \<in> keys (focus X g)"
      then obtain s where "s \<in> keys g" and t: "t = except s {x}" unfolding keys_focus_g ..
      from this(1) have "lex_pm s (i.lpp g)" by (rule i.punit.lt_max_keys)
      moreover have "keys s \<union> keys (i.lpp g) \<subseteq> {..x}"
      proof (rule Un_least)
        from \<open>g \<in> P[_]\<close> have "keys g \<subseteq> .[insert x X]" by (rule PolysD)
        with \<open>s \<in> keys g\<close> have "s \<in> .[insert x X]" ..
        hence "keys s \<subseteq> insert x X" by (rule PPsD)
        thus "keys s \<subseteq> {..x}" using assms(3) by auto

        from \<open>i.lpp g \<in> keys g\<close> \<open>keys g \<subseteq> _\<close> have "i.lpp g \<in> .[insert x X]" ..
        hence "keys (i.lpp g) \<subseteq> insert x X" by (rule PPsD)
        thus "keys (i.lpp g) \<subseteq> {..x}" using assms(3) by auto
      qed
      ultimately show "lex_pm t (except (i.lpp g) {x})" unfolding t by (rule lex_pm_except_max)
    qed
  qed

  define G where "G = i.punit.reduced_GB F"
  from assms(1) have "finite (insert x X)" by simp
  hence fin_G: "finite G" and G_sub: "G \<subseteq> P[insert x X]" and ideal_G: "ideal G = ideal F"
    and "0 \<notin> G" and G_isGB: "i.punit.is_Groebner_basis G" unfolding G_def using assms(2)
    by (rule i.finite_reduced_GB_Polys, rule i.reduced_GB_Polys, rule i.reduced_GB_ideal_Polys,
        rule i.reduced_GB_nonzero_Polys, rule i.reduced_GB_is_GB_Polys)
  define G' where "G' = focus X ` G"
  from fin_G \<open>0 \<notin> G\<close> have fin_G': "finite G'" and "0 \<notin> G'" by (auto simp: G'_def)
  have G'_sub: "G' \<subseteq> P[X]" by (auto simp: G'_def intro: focus_in_Polys)
  define G'' where "G'' = i.lcf ` G'"
  from \<open>0 \<notin> G'\<close> have "0 \<notin> G''" by (auto simp: G''_def i.punit.lc_eq_zero_iff)
  have lookup_focus_in: "lookup (focus X g) t \<in> P[{x}]" if "g \<in> G" for g t
  proof -
    have "lookup (focus X g) t \<in> range (lookup (focus X g))" by (rule rangeI)
    from that G_sub have "g \<in> P[insert x X]" ..
    hence "range (lookup (focus X g)) \<subseteq> P[insert x X - X]" by (rule focus_coeffs_subset_Polys')
    with \<open>_ \<in> range _\<close> have "lookup (focus X g) t \<in> P[insert x X - X]" ..
    also have "insert x X - X = {x}" by (simp only: eq2)
    finally show ?thesis .
  qed
  hence lcf_in: "i.lcf (focus X g) \<in> P[{x}]" if "g \<in> G" for g
    unfolding i.punit.lc_def using that by blast
  have G''_sub: "G'' \<subseteq> P[{x}]"
  proof
    fix c
    assume "c \<in> G''"
    then obtain g' where "g' \<in> G'" and c: "c = i.lcf g'" unfolding G''_def ..
    from \<open>g' \<in> G'\<close> obtain g where "g \<in> G" and g': "g' = focus X g" unfolding G'_def ..
    from this(1) show "c \<in> P[{x}]" unfolding c g' by (rule lcf_in)
  qed
  define P where "P = poly_of_pm x ` G''"
  from fin_G' have fin_P: "finite P" by (simp add: P_def G''_def)
  have "0 \<notin> P"
  proof
    assume "0 \<in> P"
    then obtain g'' where "g'' \<in> G''" and "0 = poly_of_pm x g''" unfolding P_def ..
    from this(2) have *: "keys g'' \<inter> .[{x}] = {}" by (simp add: poly_of_pm_eq_zero_iff)
    from \<open>g'' \<in> G''\<close> G''_sub have "g'' \<in> P[{x}]" ..
    hence "keys g'' \<subseteq> .[{x}]" by (rule PolysD)
    with * have "keys g'' = {}" by blast
    with \<open>g'' \<in> G''\<close> \<open>0 \<notin> G''\<close> show False by simp
  qed
  define Z where "Z = (\<Union>p\<in>P. {z. poly p z = 0})"
  have "finite Z" unfolding Z_def using fin_P
  proof (rule finite_UN_I)
    fix p
    assume "p \<in> P"
    with \<open>0 \<notin> P\<close> have "p \<noteq> 0" by blast
    thus "finite {z. poly p z = 0}" by (rule poly_roots_finite)
  qed
  with infinite_UNIV[where 'a='a] have "- Z \<noteq> {}" using finite_compl by fastforce
  then obtain a where "a \<notin> Z" by blast

  have a_nz: "poly_eval (\<lambda>_. a) (i.lcf (focus X g)) \<noteq> 0" if "g \<in> G" for g
  proof -
    from that G_sub have "g \<in> P[insert x X]" ..
    have "poly_eval (\<lambda>_. a) (i.lcf (focus X g)) = poly (poly_of_pm x (i.lcf (focus X g))) a"
      by (rule sym, intro poly_eq_poly_eval' lcf_in that)
    moreover have "poly_of_pm x (i.lcf (focus X g)) \<in> P"
      by (auto simp: P_def G''_def G'_def that intro!: imageI)
    ultimately show ?thesis using \<open>a \<notin> Z\<close> by (simp add: Z_def)
  qed

  let ?e = "poly_eval (\<lambda>_. monomial a 0)"
  have lookup_e_focus: "lookup (?e (focus {x} g)) t = poly_eval (\<lambda>_. a) (lookup (focus X g) t)"
    if "g \<in> P[insert x X]" for g t
  proof -
    have "focus (- {x}) g = focus (- {x} \<inter> insert x X) g" by (rule sym) (rule focus_Int, fact)
    also have "\<dots> = focus X g" by (simp add: Int_commute eq1 flip: Diff_eq)
    finally show ?thesis by (simp add: lookup_poly_eval_focus)
  qed
  have lpp_e_focus: "i.lpp (?e (focus {x} g)) = except (i.lpp g) {x}" if "g \<in> G" for g
  proof (rule i.punit.lt_eqI_keys)
    from that G_sub have "g \<in> P[insert x X]" ..
    hence "lookup (?e (focus {x} g)) (except (i.lpp g) {x}) = poly_eval (\<lambda>_. a) (i.lcf (focus X g))"
      by (simp only: lookup_e_focus lpp_focus i.punit.lc_def)
    also from that have "\<dots> \<noteq> 0" by (rule a_nz)
    finally show "except (i.lpp g) {x} \<in> keys (?e (focus {x} g))" by (simp add: in_keys_iff)

    fix t
    assume "t \<in> keys (?e (focus {x} g))"
    hence "0 \<noteq> lookup (?e (focus {x} g)) t" by (simp add: in_keys_iff)
    also from \<open>g \<in> P[_]\<close> have "lookup (?e (focus {x} g)) t = poly_eval (\<lambda>_. a) (lookup (focus X g) t)"
      by (rule lookup_e_focus)
    finally have "t \<in> keys (focus X g)" by (auto simp flip: lookup_not_eq_zero_eq_in_keys)
    hence "lex_pm t (i.lpp (focus X g))" by (rule i.punit.lt_max_keys)
    with \<open>g \<in> P[_]\<close> show "lex_pm t (except (i.lpp g) {x})" by (simp only: lpp_focus)
  qed

  show ?thesis
  proof
    define G3 where "G3 = ?e ` focus {x} ` G"
    have "G3 \<subseteq> P[X]"
    proof
      fix h
      assume "h \<in> G3"
      then obtain h0 where "h0 \<in> G" and h: "h = ?e (focus {x} h0)" by (auto simp: G3_def)
      from this(1) G_sub have "h0 \<in> P[insert x X]" ..
      hence "h \<in> P[insert x X - {x}]" unfolding h by (rule poly_eval_focus_in_Polys)
      thus "h \<in> P[X]" by (simp only: eq1)
    qed
    from fin_G have "finite G3" by (simp add: G3_def)
    
    have "ideal G3 \<inter> P[- {x}] = ?e ` focus {x} ` ideal G"
      by (simp only: G3_def image_poly_eval_focus_ideal)
    also have "\<dots> = ideal (?e ` focus {x} ` F) \<inter> P[- {x}]"
      by (simp only: ideal_G image_poly_eval_focus_ideal)
    finally have eq3: "ideal G3 \<inter> P[- {x}] = ideal (?e ` focus {x} ` F) \<inter> P[- {x}]" .
    from assms(1) \<open>G3 \<subseteq> P[X]\<close> \<open>finite G3\<close> have G3_isGB: "i.punit.is_Groebner_basis G3"
    proof (rule i.punit.isGB_I_spoly_rep[simplified, OF dickson_grading_varnum,
                                          where m=0, simplified i.dgrad_p_set_varnum])
      fix g1 g2
      assume "g1 \<in> G3"
      then obtain g1' where "g1' \<in> G" and g1: "g1 = ?e (focus {x} g1')"
        unfolding G3_def by blast
      from this(1) have lpp1: "i.lpp g1 = except (i.lpp g1') {x}" unfolding g1 by (rule lpp_e_focus)
      from \<open>g1' \<in> G\<close> G_sub have "g1' \<in> P[insert x X]" ..
      assume "g2 \<in> G3"
      then obtain g2' where "g2' \<in> G" and g2: "g2 = ?e (focus {x} g2')"
        unfolding G3_def by blast
      from this(1) have lpp2: "i.lpp g2 = except (i.lpp g2') {x}" unfolding g2 by (rule lpp_e_focus)
      from \<open>g2' \<in> G\<close> G_sub have "g2' \<in> P[insert x X]" ..

      define l where "l = lcs (except (i.lpp g1') {x}) (except (i.lpp g2') {x})"
      define c1 where "c1 = i.lcf (focus X g1')"
      define c2 where "c2 = i.lcf (focus X g2')"
      define c where "c = poly_eval (\<lambda>_. a) c1 * poly_eval (\<lambda>_. a) c2"
      define s where "s = c2 * punit.monom_mult 1 (l - except (i.lpp g1') {x}) g1' -
                          c1 * punit.monom_mult 1 (l - except (i.lpp g2') {x}) g2'"
      have "c1 \<in> P[{x}]" unfolding c1_def using \<open>g1' \<in> G\<close> by (rule lcf_in)
      hence eval_c1: "poly_eval (\<lambda>_. monomial a 0) (focus {x} c1) = monomial (poly_eval (\<lambda>_. a) c1) 0"
        by (simp add: focus_Polys poly_eval_sum poly_eval_monomial monomial_power_map_scale
                  times_monomial_monomial flip: punit.monomial_prod_sum monomial_sum)
           (simp add: poly_eval_alt)
      have "c2 \<in> P[{x}]" unfolding c2_def using \<open>g2' \<in> G\<close> by (rule lcf_in)
      hence eval_c2: "poly_eval (\<lambda>_. monomial a 0) (focus {x} c2) = monomial (poly_eval (\<lambda>_. a) c2) 0"
        by (simp add: focus_Polys poly_eval_sum poly_eval_monomial monomial_power_map_scale
                  times_monomial_monomial flip: punit.monomial_prod_sum monomial_sum)
           (simp add: poly_eval_alt)

      assume spoly_nz: "i.punit.spoly g1 g2 \<noteq> 0"
      assume "g1 \<noteq> 0" and "g2 \<noteq> 0"
      hence "g1' \<noteq> 0" and "g2' \<noteq> 0" by (auto simp: g1 g2)
      have c1_nz: "poly_eval (\<lambda>_. a) c1 \<noteq> 0" unfolding c1_def using \<open>g1' \<in> G\<close> by (rule a_nz)
      moreover have c2_nz: "poly_eval (\<lambda>_. a) c2 \<noteq> 0" unfolding c2_def using \<open>g2' \<in> G\<close> by (rule a_nz)
      ultimately have "c \<noteq> 0" by (simp add: c_def)
      hence "inverse c \<noteq> 0" by simp
      from \<open>g1' \<in> P[_]\<close> have "except (i.lpp g1') {x} \<in> .[insert x X - {x}]"
        by (intro PPs_closed_except' i.PPs_closed_lpp)
      moreover from \<open>g2' \<in> P[_]\<close> have "except (i.lpp g2') {x} \<in> .[insert x X - {x}]"
        by (intro PPs_closed_except' i.PPs_closed_lpp)
      ultimately have "l \<in> .[insert x X - {x}]" unfolding l_def by (rule PPs_closed_lcs)
      hence "l \<in> .[X]" by (simp only: eq1)
      hence "l \<in> .[insert x X]" by rule (rule PPs_mono, blast)
      moreover from \<open>c1 \<in> P[{x}]\<close> have "c1 \<in> P[insert x X]" by rule (intro Polys_mono, simp)
      moreover from \<open>c2 \<in> P[{x}]\<close> have "c2 \<in> P[insert x X]" by rule (intro Polys_mono, simp)
      ultimately have "s \<in> P[insert x X]" using \<open>g1' \<in> P[_]\<close> \<open>g2' \<in> P[_]\<close> unfolding s_def
        by (intro Polys_closed_minus Polys_closed_times Polys_closed_monom_mult PPs_closed_minus)
      have "s \<in> ideal G" unfolding s_def times_monomial_left[symmetric]
        by (intro ideal.span_diff ideal.span_scale ideal.span_base \<open>g1' \<in> G\<close> \<open>g2' \<in> G\<close>)
      with G_isGB have "(i.punit.red G)\<^sup>*\<^sup>* s 0" by (rule i.punit.GB_imp_zero_reducibility[simplified])
      with \<open>finite (insert x X)\<close> G_sub fin_G \<open>s \<in> P[_]\<close>
      obtain q0 where 1: "s = 0 + (\<Sum>g\<in>G. q0 g * g)" and 2: "\<And>g. q0 g \<in> P[insert x X]"
        and 3: "\<And>g. lex_pm (i.lpp (q0 g * g)) (i.lpp s)"
        by (rule i.punit.red_rtrancl_repE[simplified, OF dickson_grading_varnum, where m=0,
                                            simplified i.dgrad_p_set_varnum]) blast

      define q where "q = (\<lambda>g. inverse c \<cdot> (\<Sum>h\<in>{y\<in>G. ?e (focus {x} y) = g}. ?e (focus {x} (q0 h))))"

      have eq4: "?e (focus {x} (monomial 1 (l - t))) = monomial 1 (l - t)" for t
      proof -
        have "focus {x} (monomial (1::'a) (l - t)) = monomial (monomial 1 (l - t)) 0"
        proof (intro focus_Polys_Compl Polys_closed_monomial PPs_closed_minus)
          from \<open>x \<notin> X\<close> have "X \<subseteq> - {x}" by simp
          hence ".[X] \<subseteq> .[- {x}]" by (rule PPs_mono)
          with \<open>l \<in> .[X]\<close> show "l \<in> .[- {x}]" ..
        qed
        thus ?thesis by (simp add: poly_eval_monomial)
      qed
      from c2_nz have eq5: "inverse c * poly_eval (\<lambda>_. a) c2 = 1 / lookup g1 (i.lpp g1)"
        unfolding lpp1 using \<open>g1' \<in> P[_]\<close>
        by (simp add: c_def mult.assoc divide_inverse_commute g1 lookup_e_focus
                flip: lpp_focus i.punit.lc_def c1_def)
      from c1_nz have eq6: "inverse c * poly_eval (\<lambda>_. a) c1 = 1 / lookup g2 (i.lpp g2)"
        unfolding lpp2 using \<open>g2' \<in> P[_]\<close>
        by (simp add: c_def mult.assoc mult.left_commute[of "inverse (poly_eval (\<lambda>_. a) c1)"]
                    divide_inverse_commute g2 lookup_e_focus flip: lpp_focus i.punit.lc_def c2_def)
      have l_alt: "l = lcs (i.lpp g1) (i.lpp g2)" by (simp only: l_def lpp1 lpp2)
      have spoly_eq: "i.punit.spoly g1 g2 = (inverse c) \<cdot> ?e (focus {x} s)"
        by (simp add: s_def focus_minus focus_times poly_eval_minus poly_eval_times eval_c1 eval_c2
                      eq4 eq5 eq6 map_scale_eq_times times_monomial_monomial right_diff_distrib
                      i.punit.spoly_def Let_def
                 flip: mult.assoc times_monomial_left g1 g2 lpp1 lpp2 l_alt)
      also have "\<dots> = (\<Sum>g\<in>G. inverse c \<cdot> (?e (focus {x} (q0 g)) * ?e (focus {x} g)))"
        by (simp add: 1 focus_sum poly_eval_sum focus_times poly_eval_times map_scale_sum_distrib_left)
      also have "\<dots> = (\<Sum>g\<in>G3. \<Sum>h\<in>{y\<in>G. ?e (focus{x} y) = g}.
                                      inverse c \<cdot> (?e (focus {x} (q0 h)) * ?e (focus {x} h)))"
        unfolding G3_def image_image using fin_G by (rule sum.image_gen)
      also have "\<dots> = (\<Sum>g\<in>G3. inverse c \<cdot> (\<Sum>h\<in>{y\<in>G. ?e (focus{x} y) = g}. ?e (focus {x} (q0 h))) * g)"
        by (intro sum.cong refl) (simp add: map_scale_eq_times sum_distrib_left sum_distrib_right mult.assoc)
      also from refl have "\<dots> = (\<Sum>g\<in>G3. q g * g)" by (rule sum.cong) (simp add: q_def sum_distrib_right)
      finally have "i.punit.spoly g1 g2 = (\<Sum>g\<in>G3. q g * g)" .
      thus "i.punit.spoly_rep (varnum X) 0 G3 g1 g2"
      proof (rule i.punit.spoly_repI[simplified, where m=0 and d="varnum X",
                                        simplified i.dgrad_p_set_varnum])
        fix g
        show "q g \<in> P[X]" unfolding q_def
        proof (intro Polys_closed_map_scale Polys_closed_sum)
          fix g0
          from \<open>q0 g0 \<in> P[insert x X]\<close> have "?e (focus {x} (q0 g0)) \<in> P[insert x X - {x}]"
            by (rule poly_eval_focus_in_Polys)
          thus "?e (focus {x} (q0 g0)) \<in> P[X]" by (simp only: eq1)
        qed

        assume "q g \<noteq> 0 \<and> g \<noteq> 0"
        hence "q g \<noteq> 0" ..
        have "i.lpp (q g * g) = i.lpp (\<Sum>h\<in>{y\<in>G. ?e (focus {x} y) = g}. inverse c \<cdot> ?e (focus {x} (q0 h)) * g)"
          by (simp add: q_def map_scale_sum_distrib_left sum_distrib_right)
        also have "lex_pm \<dots> (i.ordered_powerprod_lin.Max
                {i.lpp (inverse c \<cdot> ?e (focus {x} (q0 h)) * g) | h. h \<in> {y\<in>G. ?e (focus {x} y) = g}})"
          (is "lex_pm _ (i.ordered_powerprod_lin.Max ?A)") by (fact i.punit.lt_sum_le_Max)
        also have "lex_pm \<dots> (i.lpp s)"
        proof (rule i.ordered_powerprod_lin.Max.boundedI)
          from fin_G show "finite ?A" by simp
        next
          show "?A \<noteq> {}"
          proof
            assume "?A = {}"
            hence "{h \<in> G. ?e (focus {x} h) = g} = {}" by simp
            hence "q g = 0" by (simp only: q_def sum.empty map_scale_zero_right)
            with \<open>q g \<noteq> 0\<close> show False ..
          qed
        next
          fix t
          assume "t \<in> ?A"
          then obtain h where "h \<in> G" and g[symmetric]: "?e (focus {x} h) = g"
            and "t = i.lpp (inverse c \<cdot> ?e (focus {x} (q0 h)) * g)" by blast
          note this(3)
          also have "i.lpp (inverse c \<cdot> ?e (focus {x} (q0 h)) * g) =
                      i.lpp (inverse c \<cdot> (?e (focus {x} (q0 h * h))))"
            by (simp only: map_scale_eq_times mult.assoc g poly_eval_times focus_times)
          also from \<open>inverse c \<noteq> 0\<close> have "\<dots> = i.lpp (?e (focus {x} (q0 h * h)))"
            by (rule i.punit.lt_map_scale)
          also have "lex_pm \<dots> (i.lpp (q0 h * h))"
          proof (rule i.punit.lt_le, rule ccontr)
            fix u
            assume "lookup (?e (focus {x} (q0 h * h))) u \<noteq> 0"
            hence "u \<in> keys (?e (focus {x} (q0 h * h)))" by (simp add: in_keys_iff)
            with keys_poly_eval_focus_subset have "u \<in> (\<lambda>v. except v {x}) ` keys (q0 h * h)" ..
            then obtain v where "v \<in> keys (q0 h * h)" and u: "u = except v {x}" ..
            have "lex_pm u (Poly_Mapping.single x (lookup v x) + u)"
              by (metis add.commute add.right_neutral i.plus_monotone_left lex_pm_zero_min)
            also have "\<dots> = v" by (simp only: u flip: plus_except)
            also from \<open>v \<in> _\<close> have "lex_pm v (i.lpp (q0 h * h))" by (rule i.punit.lt_max_keys)
            finally have "lex_pm u (i.lpp (q0 h * h))" .
            moreover assume "lex_pm_strict (i.lpp (q0 h * h)) u"
            ultimately show False by simp
          qed
          also have "lex_pm \<dots> (i.lpp s)" by fact
          finally show "lex_pm t (i.lpp s)" .
        qed
        also have "lex_pm_strict \<dots> l"
        proof (rule i.punit.lt_less)
          from spoly_nz show "s \<noteq> 0" by (auto simp: spoly_eq)
        next
          fix t
          assume "lex_pm l t"

          have "g1' = flatten (focus X g1')" by simp
          also have "\<dots> = flatten (monomial c1 (i.lpp (focus X g1')) + i.punit.tail (focus X g1'))"
            by (simp only: c1_def flip: i.punit.leading_monomial_tail)
          also from \<open>g1' \<in> P[_]\<close> have "\<dots> = punit.monom_mult 1 (except (i.lpp g1') {x}) c1 +
                                              flatten (i.punit.tail (focus X g1'))"
            by (simp only: flatten_plus flatten_monomial lpp_focus)
          finally have "punit.monom_mult 1 (except (i.lpp g1') {x}) c1 +
                              flatten (i.punit.tail (focus X g1')) = g1'" (is "?l = _") by (rule sym)
          moreover have "c2 * punit.monom_mult 1 (l - except (i.lpp g1') {x}) ?l =
                          punit.monom_mult 1 l (c1 * c2) +
                          c2 * punit.monom_mult 1 (l - i.lpp (focus X g1'))
                                                  (flatten (i.punit.tail (focus X g1')))"
            (is "_ = punit.monom_mult 1 l (c1 * c2) + ?a")
            by (simp add: punit.monom_mult_dist_right punit.monom_mult_assoc l_def minus_plus adds_lcs)
               (simp add: distrib_left lpp_focus \<open>g1' \<in> P[_]\<close> flip: times_monomial_left)
          ultimately have a: "c2 * punit.monom_mult 1 (l - except (i.lpp g1') {x}) g1' =
                                punit.monom_mult 1 l (c1 * c2) + ?a" by simp

          have "g2' = flatten (focus X g2')" by simp
          also have "\<dots> = flatten (monomial c2 (i.lpp (focus X g2')) + i.punit.tail (focus X g2'))"
            by (simp only: c2_def flip: i.punit.leading_monomial_tail)
          also from \<open>g2' \<in> P[_]\<close> have "\<dots> = punit.monom_mult 1 (except (i.lpp g2') {x}) c2 +
                                              flatten (i.punit.tail (focus X g2'))"
            by (simp only: flatten_plus flatten_monomial lpp_focus)
          finally have "punit.monom_mult 1 (except (i.lpp g2') {x}) c2 +
                              flatten (i.punit.tail (focus X g2')) = g2'" (is "?l = _") by (rule sym)
          moreover have "c1 * punit.monom_mult 1 (l - except (i.lpp g2') {x}) ?l =
                          punit.monom_mult 1 l (c1 * c2) +
                          c1 * punit.monom_mult 1 (l - i.lpp (focus X g2'))
                                                  (flatten (i.punit.tail (focus X g2')))"
            (is "_ = punit.monom_mult 1 l (c1 * c2) + ?b")
            by (simp add: punit.monom_mult_dist_right punit.monom_mult_assoc l_def minus_plus adds_lcs_2)
               (simp add: distrib_left lpp_focus \<open>g2' \<in> P[_]\<close> flip: times_monomial_left)
          ultimately have b: "c1 * punit.monom_mult 1 (l - except (i.lpp g2') {x}) g2' =
                                punit.monom_mult 1 l (c1 * c2) + ?b" by simp

          have lex_pm_strict_t: "lex_pm_strict t (l - i.lpp (focus X h) + i.lpp (focus X h))"
            if "t \<in> keys (d * punit.monom_mult 1 (l - i.lpp (focus X h))
                                            (flatten (i.punit.tail (focus X h))))"
            and "h \<in> G" and "d \<in> P[{x}]" for d h
          proof -
            have 0: "lex_pm_strict (u + v) w" if "lex_pm_strict v w" and "w \<in> .[X]" and "u \<in> .[{x}]"
              for u v w using that(1)
            proof (rule lex_pm_strict_plus_left)
              fix y z
              assume "y \<in> keys w"
              also from that(2) have "\<dots> \<subseteq> X" by (rule PPsD)
              also have "\<dots> \<subseteq> {..<x}" by fact
              finally have "y < x" by simp
              assume "z \<in> keys u"
              also from that(3) have "\<dots> \<subseteq> {x}" by (rule PPsD)
              finally show "y < z" using \<open>y < x\<close> by simp
            qed
            let ?h = "focus X h"
            from that(2) have "?h \<in> G'" by (simp add: G'_def)
            with \<open>G' \<subseteq> P[X]\<close> have "?h \<in> P[X]" ..
            hence "i.lpp ?h \<in> .[X]" by (rule i.PPs_closed_lpp)
            from that(1) obtain t1 t2 where "t1 \<in> keys d"
              and "t2 \<in> keys (punit.monom_mult 1 (l - i.lpp ?h) (flatten (i.punit.tail ?h)))"
              and t: "t = t1 + t2" by (rule in_keys_timesE)
            from this(2) obtain t3 where "t3 \<in> keys (flatten (i.punit.tail ?h))"
              and t2: "t2 = l - i.lpp ?h + t3" by (auto simp: punit.keys_monom_mult)
            from this(1) obtain t4 t5 where "t4 \<in> keys (i.punit.tail ?h)"
              and t5_in: "t5 \<in> keys (lookup (i.punit.tail ?h) t4)" and t3: "t3 = t4 + t5"
              using keys_flatten_subset by blast
            from this(1) have 1: "lex_pm_strict t4 (i.lpp ?h)" by (rule i.punit.keys_tail_less_lt)
            from that(2) have "lookup ?h t4 \<in> P[{x}]" by (rule lookup_focus_in)
            hence "keys (lookup ?h t4) \<subseteq> .[{x}]" by (rule PolysD)
            moreover from t5_in have t5_in: "t5 \<in> keys (lookup ?h t4)"
              by (simp add: i.punit.lookup_tail split: if_split_asm)
            ultimately have "t5 \<in> .[{x}]" ..
            with 1 \<open>i.lpp ?h \<in> _\<close> have "lex_pm_strict (t5 + t4) (i.lpp ?h)" by (rule 0)
            hence "lex_pm_strict t3 (i.lpp ?h)" by (simp only: t3 add.commute)
            hence "lex_pm_strict t2 (l - i.lpp ?h + i.lpp ?h)" unfolding t2
              by (rule i.plus_monotone_strict_left)
            moreover from \<open>l \<in> .[X]\<close> \<open>i.lpp ?h \<in> .[X]\<close> have "l - i.lpp ?h + i.lpp ?h \<in> .[X]"
              by (intro PPs_closed_plus PPs_closed_minus)
            moreover from \<open>t1 \<in> keys d\<close> that(3) have "t1 \<in> .[{x}]" by (auto dest: PolysD)
            ultimately show ?thesis unfolding t by (rule 0)
          qed
          show "lookup s t = 0"
          proof (rule ccontr)
            assume "lookup s t \<noteq> 0"
            hence "t \<in> keys s" by (simp add: in_keys_iff)
            also have "\<dots> = keys (?a - ?b)" by (simp add: s_def a b)
            also have "\<dots> \<subseteq> keys ?a \<union> keys ?b" by (fact keys_minus)
            finally show False
            proof
              assume "t \<in> keys ?a"
              hence "lex_pm_strict t (l - i.lpp (focus X g1') + i.lpp (focus X g1'))"
                using \<open>g1' \<in> G\<close> \<open>c2 \<in> P[{x}]\<close> by (rule lex_pm_strict_t)
              with \<open>g1' \<in> P[_]\<close> have "lex_pm_strict t l"
                by (simp add: lpp_focus l_def minus_plus adds_lcs)
              with \<open>lex_pm l t\<close> show ?thesis by simp
            next
              assume "t \<in> keys ?b"
              hence "lex_pm_strict t (l - i.lpp (focus X g2') + i.lpp (focus X g2'))"
                using \<open>g2' \<in> G\<close> \<open>c1 \<in> P[{x}]\<close> by (rule lex_pm_strict_t)
              with \<open>g2' \<in> P[_]\<close> have "lex_pm_strict t l"
                by (simp add: lpp_focus l_def minus_plus adds_lcs_2)
              with \<open>lex_pm l t\<close> show ?thesis by simp
            qed
          qed
        qed
        also have "\<dots> = lcs (i.lpp g1) (i.lpp g2)" by (simp only: l_def lpp1 lpp2)
        finally show "lex_pm_strict (i.lpp (q g * g)) (lcs (i.lpp g1) (i.lpp g2))" .
      qed
    qed
    have "1 \<in> ideal (?e ` focus {x} ` F) \<longleftrightarrow> 1 \<in> ideal (?e ` focus {x} ` F) \<inter> P[- {x}]"
      by (simp add: one_in_Polys)
    also have "\<dots> \<longleftrightarrow> 1 \<in> ideal G3" by (simp add: one_in_Polys flip: eq3)
    also have "\<not> \<dots>"
    proof
      note G3_isGB
      moreover assume "1 \<in> ideal G3"
      moreover have "1 \<noteq> (0::_ \<Rightarrow>\<^sub>0 'a)" by simp
      ultimately obtain g where "g \<in> G3" and "g \<noteq> 0" and "i.lpp g adds i.lpp (1::_ \<Rightarrow>\<^sub>0 'a)"
        by (rule i.punit.GB_adds_lt[simplified])
      from this(3) have "i.lpp g = 0" by (simp add: i.punit.lt_monomial adds_zero flip: single_one)
      hence "monomial (i.lcf g) 0 = g" by (rule i.punit.lt_eq_min_term_monomial[simplified])
      from \<open>g \<in> G3\<close> obtain g' where "g' \<in> G" and g: "g = ?e (focus {x} g')" by (auto simp: G3_def)
      from this(1) have "i.lpp g = except (i.lpp g') {x}" unfolding g by (rule lpp_e_focus)
      hence "keys (i.lpp g') \<subseteq> {x}" by (simp add: \<open>i.lpp g = 0\<close> except_eq_zero_iff)
      have "g' \<in> P[{x}]"
      proof (intro PolysI subsetI PPsI)
        fix t y
        assume "t \<in> keys g'"
        hence "lex_pm t (i.lpp g')" by (rule i.punit.lt_max_keys)
        moreover assume "y \<in> keys t"
        ultimately obtain z where "z \<in> keys (i.lpp g')" and "z \<le> y" by (rule lex_pm_keys_leE)
        with \<open>keys (i.lpp g') \<subseteq> {x}\<close> have "x \<le> y" by blast
        from \<open>g' \<in> G\<close> G_sub have "g' \<in> P[insert x X]" ..
        hence "indets g' \<subseteq> insert x X" by (rule PolysD)
        moreover from \<open>y \<in> _\<close> \<open>t \<in> _\<close> have "y \<in> indets g'" by (rule in_indetsI)
        ultimately have "y \<in> insert x X" ..
        thus "y \<in> {x}"
        proof
          assume "y \<in> X"
          with assms(3) have "y \<in> {..<x}" ..
          with \<open>x \<le> y\<close> show ?thesis by simp
        qed simp
      qed
      moreover from \<open>g' \<in> G\<close> have "g' \<in> ideal G" by (rule ideal.span_base)
      ultimately have "g' \<in> ideal F \<inter> P[{x}]" by (simp add: ideal_G)
      with assms(5) have "g' = 0" by blast
      hence "g = 0" by (simp add: g)
      with \<open>g \<noteq> 0\<close> show False ..
    qed
    finally show "1 \<notin> ideal (?e ` focus {x} ` F)" .
  qed
qed

lemma weak_Nullstellensatz_aux_3:
  assumes "F \<subseteq> P[insert x X]" and "x \<notin> X" and "1 \<notin> ideal F" and "\<not> ideal F \<inter> P[{x}] \<subseteq> {0}"
  obtains a::"'a::alg_closed_field" where "1 \<notin> ideal (poly_eval (\<lambda>_. monomial a 0) ` focus {x} ` F)"
proof -
  let ?x = "monomial 1 (Poly_Mapping.single x 1)"
  from assms(4) obtain f where "f \<in> ideal F" and "f \<in> P[{x}]" and "f \<noteq> 0" by blast
  define p where "p = poly_of_pm x f"
  from \<open>f \<in> P[{x}]\<close> \<open>f \<noteq> 0\<close> have "p \<noteq> 0"
    by (auto simp: p_def poly_of_pm_eq_zero_iff simp flip: keys_eq_empty dest!: PolysD(1))
  obtain c A m where A: "finite A" and p: "p = Polynomial.smult c (\<Prod>a\<in>A. [:- a, 1:] ^ m a)"
    and "\<And>x. m x = 0 \<longleftrightarrow> x \<notin> A" and "c = 0 \<longleftrightarrow> p = 0" and "\<And>z. poly p z = 0 \<longleftrightarrow> (c = 0 \<or> z \<in> A)"
    by (rule linear_factorsE) blast
  from this(4, 5) have "c \<noteq> 0" and "\<And>z. poly p z = 0 \<longleftrightarrow> z \<in> A" by (simp_all add: \<open>p \<noteq> 0\<close>)
  have "\<exists>a\<in>A. 1 \<notin> ideal (poly_eval (\<lambda>_. monomial a 0) ` focus {x} ` F)"
  proof (rule ccontr)
    assume asm: "\<not> (\<exists>a\<in>A. 1 \<notin> ideal (poly_eval (\<lambda>_. monomial a 0) ` focus {x} ` F))"
    obtain g h where "g a \<in> ideal F" and 1: "h a * (?x - monomial a 0) + g a = 1"
      if "a \<in> A" for a
    proof -
      define P where "P = (\<lambda>gh a. fst gh \<in> ideal F \<and> fst gh + snd gh * (?x - monomial a 0) = 1)"
      define gh where "gh = (\<lambda>a. SOME gh. P gh a)"
      show ?thesis
      proof
        fix a
        assume "a \<in> A"
        with asm have "1 \<in> ideal (poly_eval (\<lambda>_. monomial a 0) ` focus {x} ` F)" by blast
        hence "1 \<in> poly_eval (\<lambda>_. monomial a 0) ` focus {x} ` ideal F"
          by (simp add: image_poly_eval_focus_ideal one_in_Polys)
        then obtain g where "g \<in> ideal F" and "1 = poly_eval (\<lambda>_. monomial a 0) (focus {x} g)"
          unfolding image_image ..
        note this(2)
        also have "poly_eval (\<lambda>_. monomial a 0) (focus {x} g) = poly (poly_of_focus x g) (monomial a 0)"
          by (simp only: poly_poly_of_focus)
        also have "\<dots> = poly (poly_of_focus x g) (?x - (?x - monomial a 0))" by simp
        also obtain h where "\<dots> = poly (poly_of_focus x g) ?x - h * (?x - monomial a 0)"
          by (rule poly_minus_rightE)
        also have "\<dots> = g - h * (?x - monomial a 0)" by (simp only: poly_poly_of_focus_monomial)
        finally have "g - h * (?x - monomial a 0) = 1" by (rule sym)
        with \<open>g \<in> ideal F\<close> have "P (g, - h) a" by (simp add: P_def)
        hence "P (gh a) a" unfolding gh_def by (rule someI)
        thus "fst (gh a) \<in> ideal F" and "snd (gh a) * (?x - monomial a 0) + fst (gh a) = 1"
          by (simp_all only: P_def add.commute)
      qed
    qed
    from this(1) obtain g' where "g' \<in> ideal F"
      and 2: "(\<Prod>a\<in>A. (h a * (?x - monomial a 0) + g a) ^ m a) =
                (\<Prod>a\<in>A. (h a * (?x - monomial a 0)) ^ m a) + g'"
      by (rule weak_Nullstellensatz_aux_1)
    have "1 = (\<Prod>a\<in>A. (h a * (?x - monomial a 0) + g a) ^ m a)"
      by (rule sym) (intro prod.neutral ballI, simp only: 1 power_one)
    also have "\<dots> = (\<Prod>a\<in>A. h a ^ m a) * (\<Prod>a\<in>A. (?x - monomial a 0) ^ m a) + g'"
      by (simp only: 2 power_mult_distrib prod.distrib)
    also have "(\<Prod>a\<in>A. (?x - monomial a 0) ^ m a) = pm_of_poly x (\<Prod>a\<in>A. [:- a, 1:] ^ m a)"
      by (simp add: pm_of_poly_prod pm_of_poly_pCons single_uminus punit.monom_mult_monomial
              flip: single_one)
    also from \<open>c \<noteq> 0\<close> have "\<dots> = monomial (inverse c) 0 * pm_of_poly x p"
      by (simp add: p map_scale_assoc flip: map_scale_eq_times)
    also from \<open>f \<in> P[{x}]\<close> have "\<dots> = monomial (inverse c) 0 * f"
      by (simp only: \<open>p = poly_of_pm x f\<close> pm_of_poly_of_pm)
    finally have "1 = ((\<Prod>a\<in>A. h a ^ m a) * monomial (inverse c) 0) * f + g'"
      by (simp only: mult.assoc)
    also from \<open>f \<in> ideal F\<close> \<open>g' \<in> ideal F\<close> have "\<dots> \<in> ideal F" by (intro ideal.span_add ideal.span_scale)
    finally have "1 \<in> ideal F" .
    with assms(3) show False ..
  qed
  then obtain a where "1 \<notin> ideal (poly_eval (\<lambda>_. monomial a 0) ` focus {x} ` F)" ..
  thus ?thesis ..
qed

theorem weak_Nullstellensatz:
  assumes "finite X" and "F \<subseteq> P[X]" and "\<V> F = ({}::('x::{countable,linorder} \<Rightarrow> 'a::alg_closed_field) set)"
  shows "ideal F = UNIV"
  unfolding ideal_eq_UNIV_iff_contains_one
proof (rule ccontr)
  assume "1 \<notin> ideal F"
  with assms(1, 2) obtain a where "1 \<notin> ideal (poly_eval a ` F)"
  proof (induct X arbitrary: F thesis rule: finite_linorder_induct)
    case empty
    have "F \<subseteq> {0}"
    proof
      fix f
      assume "f \<in> F"
      with empty.prems(2) have "f \<in> P[{}]" ..
      then obtain c where f: "f = monomial c 0" unfolding Polys_empty ..
      also have "c = 0"
      proof (rule ccontr)
        assume "c \<noteq> 0"
        from \<open>f \<in> F\<close> have "f \<in> ideal F" by (rule ideal.span_base)
        hence "monomial (inverse c) 0 * f \<in> ideal F" by (rule ideal.span_scale)
        with \<open>c \<noteq> 0\<close> have "1 \<in> ideal F" by (simp add: f times_monomial_monomial)
        with empty.prems(3) show False ..
      qed
      finally show "f \<in> {0}" by simp
    qed
    hence "poly_eval 0 ` F \<subseteq> {0}" by auto
    hence "ideal (poly_eval 0 ` F) = {0}" by simp
    hence "1 \<notin> ideal (poly_eval 0 ` F)" by (simp del: ideal_eq_zero_iff)
    thus ?case by (rule empty.prems)
  next
    case (insert x X)
    obtain a0 where "1 \<notin> ideal (poly_eval (\<lambda>_. monomial a0 0) ` focus {x} ` F)" (is "_ \<notin> ideal ?F")
    proof (cases "ideal F \<inter> P[{x}] \<subseteq> {0}")
      case True
      with insert.hyps(1) insert.prems(2) insert.hyps(2) insert.prems(3) obtain a0
        where "1 \<notin> ideal (poly_eval (\<lambda>_. monomial a0 0) ` focus {x} ` F)"
        by (rule weak_Nullstellensatz_aux_2)
      thus ?thesis ..
    next
      case False
      from insert.hyps(2) have "x \<notin> X" by blast
      with insert.prems(2) obtain a0 where "1 \<notin> ideal (poly_eval (\<lambda>_. monomial a0 0) ` focus {x} ` F)"
        using insert.prems(3) False by (rule weak_Nullstellensatz_aux_3)
      thus ?thesis ..
    qed
    moreover have "?F \<subseteq> P[X]"
    proof -
      {
        fix f
        assume "f \<in> F"
        with insert.prems(2) have "f \<in> P[insert x X]" ..
        hence "poly_eval (\<lambda>_. monomial a0 0) (focus {x} f) \<in> P[insert x X - {x}]"
          by (rule poly_eval_focus_in_Polys)
        also have "\<dots> \<subseteq> P[X]" by (rule Polys_mono) simp
        finally have "poly_eval (\<lambda>_. monomial a0 0) (focus {x} f) \<in> P[X]" .
      }
      thus ?thesis by blast
    qed
    ultimately obtain a1 where "1 \<notin> ideal (poly_eval a1 ` ?F)" using insert.hyps(3) by blast
    also have "poly_eval a1 ` ?F = poly_eval (a1(x := poly_eval a1 (monomial a0 0))) ` F"
      by (simp add: image_image poly_eval_poly_eval_focus fun_upd_def)
    finally show ?case by (rule insert.prems)
  qed
  hence "ideal (poly_eval a ` F) \<noteq> UNIV" by (simp add: ideal_eq_UNIV_iff_contains_one)
  hence "ideal (poly_eval a ` F) = {0}" using ideal_field_disj[of "poly_eval a ` F"] by blast
  hence "poly_eval a ` F \<subseteq> {0}" by simp
  hence "a \<in> \<V> F" by (rule variety_ofI_alt)
  thus False by (simp add: assms(3))
qed

lemma radical_idealI:
  assumes "finite X" and "F \<subseteq> P[X]" and "f \<in> P[X]" and "x \<notin> X"
    and "\<V> (insert (1 - punit.monom_mult 1 (Poly_Mapping.single x 1) f) F) = {}"
  shows "(f::('x::{countable,linorder} \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a::alg_closed_field) \<in> \<surd>ideal F"
proof (cases "f = 0")
  case True
  thus ?thesis by simp
next
  case False
  from assms(4) have "P[X] \<subseteq> P[- {x}]" by (auto simp: Polys_alt)
  with assms(3) have "f \<in> P[- {x}]" ..
  let ?x = "Poly_Mapping.single x 1"
  let ?f = "punit.monom_mult 1 ?x f"
  from assms(1) have "finite (insert x X)" by simp
  moreover have "insert (1 - ?f) F \<subseteq> P[insert x X]" unfolding insert_subset
  proof (intro conjI Polys_closed_minus one_in_Polys Polys_closed_monom_mult PPs_closed_single)
    have "P[X] \<subseteq> P[insert x X]" by (rule Polys_mono) blast
    with assms(2, 3) show "f \<in> P[insert x X]" and "F \<subseteq> P[insert x X]" by blast+
  qed simp
  ultimately have "ideal (insert (1 - ?f) F) = UNIV"
    using assms(5) by (rule weak_Nullstellensatz)
  hence "1 \<in> ideal (insert (1 - ?f) F)" by simp
  then obtain F' q where fin': "finite F'" and F'_sub: "F' \<subseteq> insert (1 - ?f) F"
    and eq: "1 = (\<Sum>f'\<in>F'. q f' * f')" by (rule ideal.spanE)
  show "f \<in> \<surd>ideal F"
  proof (cases "1 - ?f \<in> F'")
    case True
    define g where "g = (\<lambda>x::('x \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 'a. Fract x 1)"
    define F'' where "F'' = F' - {1 - ?f}"
    define q0 where "q0 = q (1 - ?f)"
    have g_0: "g 0 = 0" by (simp add: g_def fract_collapse)
    have g_1: "g 1 = 1" by (simp add: g_def fract_collapse)
    have g_plus: "g (a + b) = g a + g b" for a b by (simp add: g_def)
    have g_minus: "g (a - b) = g a - g b" for a b by (simp add: g_def)
    have g_times: "g (a * b) = g a * g b" for a b by (simp add: g_def)
    from fin' have fin'': "finite F''" by (simp add: F''_def)
    from F'_sub have F''_sub: "F'' \<subseteq> F" by (auto simp: F''_def)

    have "focus {x} ?f = monomial 1 ?x * focus {x} f"
      by (simp add: focus_times focus_monomial except_single flip: times_monomial_left)
    also from \<open>f \<in> P[- {x}]\<close> have "focus {x} f = monomial f 0" by (rule focus_Polys_Compl)
    finally have "focus {x} ?f = monomial f ?x" by (simp add: times_monomial_monomial)
    hence eq1: "poly (map_poly g (poly_of_focus x (1 - ?f))) (Fract 1 f) = 0"
      by (simp add: poly_of_focus_def focus_minus poly_of_pm_minus poly_of_pm_monomial
                PPs_closed_single map_poly_minus g_0 g_1 g_minus map_poly_monom poly_monom)
         (simp add: g_def Fract_same \<open>f \<noteq> 0\<close>)
    have eq2: "poly (map_poly g (poly_of_focus x f')) (Fract 1 f) = Fract f' 1" if "f' \<in> F''" for f'
    proof -
      from that F''_sub have "f' \<in> F" ..
      with assms(2) have "f' \<in> P[X]" ..
      with \<open>P[X] \<subseteq> _\<close> have "f' \<in> P[- {x}]" ..
      hence "focus {x} f' = monomial f' 0" by (rule focus_Polys_Compl)
      thus ?thesis
        by (simp add: poly_of_focus_def focus_minus poly_of_pm_minus poly_of_pm_monomial
                zero_in_PPs map_poly_minus g_0 g_1 g_minus map_poly_monom poly_monom)
           (simp only: g_def)
    qed

    define p0m0 where "p0m0 = (\<lambda>f'. SOME z. poly (map_poly g (poly_of_focus x (q f'))) (Fract 1 f) =
                                              Fract (fst z) (f ^ snd z))"
    define p0 where "p0 = fst \<circ> p0m0"
    define m0 where "m0 = snd \<circ> p0m0"
    define m where "m = Max (m0 ` F'')"
    have eq3: "poly (map_poly g (poly_of_focus x (q f'))) (Fract 1 f) = Fract (p0 f') (f ^ m0 f')"
      for f'
    proof -
      have "g a = 0 \<longleftrightarrow> a = 0" for a by (simp add: g_def Fract_eq_zero_iff)
      hence "set (Polynomial.coeffs (map_poly g (poly_of_focus x (q f')))) \<subseteq> range (\<lambda>x. Fract x 1)"
        by (auto simp: set_coeffs_map_poly g_def)
      then obtain p m' where "poly (map_poly g (poly_of_focus x (q f'))) (Fract 1 f) = Fract p (f ^ m')"
        by (rule poly_Fract)
      hence "poly (map_poly g (poly_of_focus x (q f'))) (Fract 1 f) = Fract (fst (p, m')) (f ^ snd (p, m'))"
        by simp
      thus ?thesis unfolding p0_def m0_def p0m0_def o_def by (rule someI)
    qed
    
    note eq
    also from True fin' have "(\<Sum>f'\<in>F'. q f' * f') = q0 * (1 - ?f) + (\<Sum>f'\<in>F''. q f' * f')"
      by (simp add: q0_def F''_def sum.remove)
    finally have "poly_of_focus x 1 = poly_of_focus x (q0 * (1 - ?f) + (\<Sum>f'\<in>F''. q f' * f'))"
      by (rule arg_cong)
    hence "1 = poly (map_poly g (poly_of_focus x (q0 * (1 - ?f) + (\<Sum>f'\<in>F''. q f' * f')))) (Fract 1 f)"
      by (simp add: g_1)
    also have "\<dots> = poly (map_poly g (poly_of_focus x (\<Sum>f'\<in>F''. q f' * f'))) (Fract 1 f)"
      by (simp only: poly_of_focus_plus map_poly_plus g_0 g_plus g_times poly_add
                poly_of_focus_times map_poly_times poly_mult eq1 mult_zero_right add_0_left)
    also have "\<dots> = (\<Sum>f'\<in>F''. Fract (p0 f') (f ^ m0 f') * Fract f' 1)"
      by (simp only: poly_of_focus_sum poly_of_focus_times map_poly_sum map_poly_times
                g_0 g_plus g_times poly_sum poly_mult eq2 eq3 cong: sum.cong)
    finally have "Fract (f ^ m) 1 = Fract (f ^ m) 1 * (\<Sum>f'\<in>F''. Fract (p0 f' * f') (f ^ m0 f'))"
      by simp
    also have "\<dots> = (\<Sum>f'\<in>F''. Fract (f ^ m * (p0 f' * f')) (f ^ m0 f'))"
      by (simp add: sum_distrib_left)
    also from refl have "\<dots> = (\<Sum>f'\<in>F''. Fract ((f ^ (m - m0 f') * p0 f') * f') 1)"
    proof (rule sum.cong)
      fix f'
      assume "f' \<in> F''"
      hence "m0 f' \<in> m0 ` F''" by (rule imageI)
      with _ have "m0 f' \<le> m" unfolding m_def by (rule Max_ge) (simp add: fin'')
      hence "f ^ m = f ^ (m0 f') * f ^ (m - m0 f')" by (simp flip: power_add)
      hence "Fract (f ^ m * (p0 f' * f')) (f ^ m0 f') = Fract (f ^ m0 f') (f ^ m0 f') *
                                                        Fract (f ^ (m - m0 f') * (p0 f' * f')) 1"
        by (simp add: ac_simps)
      also from \<open>f \<noteq> 0\<close> have "Fract (f ^ m0 f') (f ^ m0 f') = 1" by (simp add: Fract_same)
      finally show "Fract (f ^ m * (p0 f' * f')) (f ^ m0 f') = Fract (f ^ (m - m0 f') * p0 f' * f') 1"
        by (simp add: ac_simps)
    qed
    also from fin'' have "\<dots> = Fract (\<Sum>f'\<in>F''. (f ^ (m - m0 f') * p0 f') * f') 1"
      by (induct F'') (simp_all add: fract_collapse)
    finally have "f ^ m = (\<Sum>f'\<in>F''. (f ^ (m - m0 f') * p0 f') * f')"
      by (simp add: eq_fract)
    also have "\<dots> \<in> ideal F''" by (rule ideal.sum_in_spanI)
    also from \<open>F'' \<subseteq> F\<close> have "\<dots> \<subseteq> ideal F" by (rule ideal.span_mono)
    finally show "f \<in> \<surd>ideal F" by (rule radicalI)
  next
    case False
    with F'_sub have "F' \<subseteq> F" by blast
    have "1 \<in> ideal F'" unfolding eq by (rule ideal.sum_in_spanI)
    also from \<open>F' \<subseteq> F\<close> have "\<dots> \<subseteq> ideal F" by (rule ideal.span_mono)
    finally have "ideal F = UNIV" by (simp only: ideal_eq_UNIV_iff_contains_one)
    thus ?thesis by simp
  qed
qed

corollary radical_idealI_extend_indets:
  assumes "finite X" and "F \<subseteq> P[X]"
    and "\<V> (insert (1 - punit.monom_mult 1 (Poly_Mapping.single None 1) (extend_indets f))
                            (extend_indets ` F)) = {}"
  shows "(f::(_::{countable,linorder} \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 _::alg_closed_field) \<in> \<surd>ideal F"
proof -
  define Y where "Y = X \<union> indets f"
  from assms(1) have fin_Y: "finite Y" by (simp add: Y_def finite_indets)
  have "P[X] \<subseteq> P[Y]" by (rule Polys_mono) (simp add: Y_def)
  with assms(2) have F_sub: "F \<subseteq> P[Y]" by (rule subset_trans)
  have f_in: "f \<in> P[Y]" by (simp add: Y_def Polys_alt)

  let ?F = "extend_indets ` F"
  let ?f = "extend_indets f"
  let ?X = "Some ` Y"
  from fin_Y have "finite ?X" by (rule finite_imageI)
  moreover from F_sub have "?F \<subseteq> P[?X]"
    by (auto simp: indets_extend_indets intro!: PolysI_alt imageI dest!: PolysD(2) subsetD[of F])
  moreover from f_in have "?f \<in> P[?X]"
    by (auto simp: indets_extend_indets intro!: PolysI_alt imageI dest!: PolysD(2))
  moreover have "None \<notin> ?X" by simp
  ultimately have "?f \<in> \<surd>ideal ?F" using assms(3) by (rule radical_idealI)
  also have "?f \<in> \<surd>ideal ?F \<longleftrightarrow> f \<in> \<surd>ideal F"
  proof
    assume "f \<in> \<surd>ideal F"
    then obtain m where "f ^ m \<in> ideal F" by (rule radicalE)
    hence "extend_indets (f ^ m) \<in> extend_indets ` ideal F" by (rule imageI)
    with extend_indets_ideal_subset have "?f ^ m \<in> ideal ?F" unfolding extend_indets_power ..
    thus "?f \<in> \<surd>ideal ?F" by (rule radicalI)
  next
    assume "?f \<in> \<surd>ideal ?F"
    then obtain m where "?f ^ m \<in> ideal ?F" by (rule radicalE)
    moreover have "?f ^ m \<in> P[- {None}]"
      by (rule Polys_closed_power) (auto intro!: PolysI_alt simp: indets_extend_indets)
    ultimately have "extend_indets (f ^ m) \<in> extend_indets ` ideal F"
      by (simp add: extend_indets_ideal extend_indets_power)
    hence "f ^ m \<in> ideal F" by (simp only: inj_image_mem_iff[OF inj_extend_indets])
    thus "f \<in> \<surd>ideal F" by (rule radicalI)
  qed
  finally show ?thesis .
qed

theorem Nullstellensatz:
  assumes "finite X" and "F \<subseteq> P[X]"
    and "(f::(_::{countable,linorder} \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 _::alg_closed_field) \<in> \<I> (\<V> F)"
  shows "f \<in> \<surd>ideal F"
  using assms(1, 2)
proof (rule radical_idealI_extend_indets)
  let ?f = "punit.monom_mult 1 (monomial 1 None) (extend_indets f)"
  show "\<V> (insert (1 - ?f) (extend_indets ` F)) = {}"
  proof (intro subset_antisym subsetI)
    fix a
    assume "a \<in> \<V> (insert (1 - ?f) (extend_indets ` F))"
    moreover have "1 - ?f \<in> insert (1 - ?f) (extend_indets ` F)" by simp
    ultimately have "poly_eval a (1 - ?f) = 0" by (rule variety_ofD)
    hence "poly_eval a (extend_indets f) \<noteq> 0"
      by (auto simp: poly_eval_minus poly_eval_times simp flip: times_monomial_left)
    hence "poly_eval (a \<circ> Some) f \<noteq> 0" by (simp add: poly_eval_extend_indets)
    have "a \<circ> Some \<in> \<V> F"
    proof (rule variety_ofI)
      fix f'
      assume "f' \<in> F"
      hence "extend_indets f' \<in> insert (1 - ?f) (extend_indets ` F)" by simp
      with \<open>a \<in> _\<close> have "poly_eval a (extend_indets f') = 0" by (rule variety_ofD)
      thus "poly_eval (a \<circ> Some) f' = 0" by (simp only: poly_eval_extend_indets)
    qed
    with assms(3) have "poly_eval (a \<circ> Some) f = 0" by (rule ideal_ofD)
    with \<open>poly_eval (a \<circ> Some) f \<noteq> 0\<close> show "a \<in> {}" ..
  qed simp
qed

theorem strong_Nullstellensatz:
  assumes "finite X" and "F \<subseteq> P[X]"
  shows "\<I> (\<V> F) = \<surd>ideal (F::((_::{countable,linorder} \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 _::alg_closed_field) set)"
proof (intro subset_antisym subsetI)
  fix f
  assume "f \<in> \<I> (\<V> F)"
  with assms show "f \<in> \<surd>ideal F" by (rule Nullstellensatz)
qed (metis ideal_ofI variety_ofD variety_of_radical_ideal)

text \<open>The following lemma can be used for actually \<^emph>\<open>deciding\<close> whether a polynomial is contained in
  the radical of an ideal or not.\<close>

lemma radical_ideal_iff:
  assumes "finite X" and "F \<subseteq> P[X]" and "f \<in> P[X]" and "x \<notin> X"
  shows "(f::(_::{countable,linorder} \<Rightarrow>\<^sub>0 nat) \<Rightarrow>\<^sub>0 _::alg_closed_field) \<in> \<surd>ideal F \<longleftrightarrow>
            1 \<in> ideal (insert (1 - punit.monom_mult 1 (Poly_Mapping.single x 1) f) F)"
proof -
  let ?f = "punit.monom_mult 1 (Poly_Mapping.single x 1) f"
  show ?thesis
  proof
    assume "f \<in> \<surd>ideal F"
    then obtain m where "f ^ m \<in> ideal F" by (rule radicalE)
    from assms(1) have "finite (insert x X)" by simp
    moreover have "insert (1 - ?f) F \<subseteq> P[insert x X]" unfolding insert_subset
    proof (intro conjI Polys_closed_minus one_in_Polys Polys_closed_monom_mult PPs_closed_single)
      have "P[X] \<subseteq> P[insert x X]" by (rule Polys_mono) blast
      with assms(2, 3) show "f \<in> P[insert x X]" and "F \<subseteq> P[insert x X]" by blast+
    qed simp
    moreover have "\<V> (insert (1 - ?f) F) = {}"
    proof (intro subset_antisym subsetI)
      fix a
      assume "a \<in> \<V> (insert (1 - ?f) F)"
      moreover have "1 - ?f \<in> insert (1 - ?f) F" by simp
      ultimately have "poly_eval a (1 - ?f) = 0" by (rule variety_ofD)
      hence "poly_eval a (f ^ m) \<noteq> 0"
        by (auto simp: poly_eval_minus poly_eval_times poly_eval_power simp flip: times_monomial_left)
      from \<open>a \<in> _\<close> have "a \<in> \<V> (ideal (insert (1 - ?f) F))" by (simp only: variety_of_ideal)
      moreover from \<open>f ^ m \<in> ideal F\<close> ideal.span_mono have "f ^ m \<in> ideal (insert (1 - ?f) F)"
        by (rule rev_subsetD) blast
      ultimately have "poly_eval a (f ^ m) = 0" by (rule variety_ofD)
      with \<open>poly_eval a (f ^ m) \<noteq> 0\<close> show "a \<in> {}" ..
    qed simp
    ultimately have "ideal (insert (1 - ?f) F) = UNIV" by (rule weak_Nullstellensatz)
    thus "1 \<in> ideal (insert (1 - ?f) F)" by simp
  next
    assume "1 \<in> ideal (insert (1 - ?f) F)"
    have "\<V> (insert (1 - ?f) F) = {}"
    proof (intro subset_antisym subsetI)
      fix a
      assume "a \<in> \<V> (insert (1 - ?f) F)"
      hence "a \<in> \<V> (ideal (insert (1 - ?f) F))" by (simp only: variety_of_ideal)
      hence "poly_eval a 1 = 0" using \<open>1 \<in> _\<close> by (rule variety_ofD)
      thus "a \<in> {}" by simp
    qed simp
    with assms show "f \<in> \<surd>ideal F" by (rule radical_idealI)
  qed
qed

end (* theory *)