[STATEMENT]
lemma (in gd_term) Macaulay_list_is_GB:
  assumes "is_Groebner_basis G" and "pmdl (set ps) = pmdl G" and "G \<subseteq> phull (set ps)"
  shows "is_Groebner_basis (set (Macaulay_list ps))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_Groebner_basis (set (Macaulay_list ps))
[PROOF STEP]
proof (simp only: GB_alt_3_finite[OF finite_set] pmdl_Macaulay_list, intro ballI impI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
fix f
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
assume "f \<in> pmdl (set ps)"
[PROOF STATE]
proof (state)
this:
f \<in> pmdl (set ps)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
f \<in> pmdl (set ps)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
from assms(2)
[PROOF STATE]
proof (chain)
picking this:
pmdl (set ps) = pmdl G
[PROOF STEP]
have "\<dots> = pmdl G"
[PROOF STATE]
proof (prove)
using this:
pmdl (set ps) = pmdl G

goal (1 subgoal):
 1. pmdl (set ps) = pmdl G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
pmdl (set ps) = pmdl G

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
f \<in> pmdl G
[PROOF STEP]
have "f \<in> pmdl G"
[PROOF STATE]
proof (prove)
using this:
f \<in> pmdl G

goal (1 subgoal):
 1. f \<in> pmdl G
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
f \<in> pmdl G

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
assume "f \<noteq> 0"
[PROOF STATE]
proof (state)
this:
f \<noteq> 0

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
with assms(1) \<open>f \<in> pmdl G\<close>
[PROOF STATE]
proof (chain)
picking this:
is_Groebner_basis G
f \<in> pmdl G
f \<noteq> 0
[PROOF STEP]
obtain g where "g \<in> G" and "g \<noteq> 0" and "lt g adds\<^sub>t lt f"
[PROOF STATE]
proof (prove)
using this:
is_Groebner_basis G
f \<in> pmdl G
f \<noteq> 0

goal (1 subgoal):
 1. (\<And>g. \<lbrakk>g \<in> G; g \<noteq> 0; lt g adds\<^sub>t lt f\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule GB_adds_lt)
[PROOF STATE]
proof (state)
this:
g \<in> G
g \<noteq> 0
lt g adds\<^sub>t lt f

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
from assms(3) \<open>g \<in> G\<close>
[PROOF STATE]
proof (chain)
picking this:
G \<subseteq> phull (set ps)
g \<in> G
[PROOF STEP]
have "g \<in> phull (set ps)"
[PROOF STATE]
proof (prove)
using this:
G \<subseteq> phull (set ps)
g \<in> G

goal (1 subgoal):
 1. g \<in> phull (set ps)
[PROOF STEP]
..
[PROOF STATE]
proof (state)
this:
g \<in> phull (set ps)

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
from this \<open>g \<noteq> 0\<close>
[PROOF STATE]
proof (chain)
picking this:
g \<in> phull (set ps)
g \<noteq> 0
[PROOF STEP]
obtain g' where "g' \<in> set (Macaulay_list ps)" and "g' \<noteq> 0" and "lt g = lt g'"
[PROOF STATE]
proof (prove)
using this:
g \<in> phull (set ps)
g \<noteq> 0

goal (1 subgoal):
 1. (\<And>g'. \<lbrakk>g' \<in> set (Macaulay_list ps); g' \<noteq> 0; lt g = lt g'\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (rule Macaulay_list_lt)
[PROOF STATE]
proof (state)
this:
g' \<in> set (Macaulay_list ps)
g' \<noteq> 0
lt g = lt g'

goal (1 subgoal):
 1. \<And>f. \<lbrakk>f \<in> pmdl (set ps); f \<noteq> 0\<rbrakk> \<Longrightarrow> \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
show "\<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f
[PROOF STEP]
proof (rule, rule)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. ?g \<noteq> 0
 2. lt ?g adds\<^sub>t lt f
 3. ?g \<in> set (Macaulay_list ps)
[PROOF STEP]
from \<open>lt g adds\<^sub>t lt f\<close>
[PROOF STATE]
proof (chain)
picking this:
lt g adds\<^sub>t lt f
[PROOF STEP]
show "lt g' adds\<^sub>t lt f"
[PROOF STATE]
proof (prove)
using this:
lt g adds\<^sub>t lt f

goal (1 subgoal):
 1. lt g' adds\<^sub>t lt f
[PROOF STEP]
by (simp only: \<open>lt g = lt g'\<close>)
[PROOF STATE]
proof (state)
this:
lt g' adds\<^sub>t lt f

goal (2 subgoals):
 1. g' \<noteq> 0
 2. g' \<in> set (Macaulay_list ps)
[PROOF STEP]
qed fact+
[PROOF STATE]
proof (state)
this:
\<exists>g\<in>set (Macaulay_list ps). g \<noteq> 0 \<and> lt g adds\<^sub>t lt f

goal:
No subgoals!
[PROOF STEP]
qed