Theory F4
section ‹Faug\`ere's F4 Algorithm›
theory F4
imports Macaulay_Matrix Algorithm_Schema
begin
text ‹This theory implements Faug\`ere's F4 algorithm based on @{const gd_term.gb_schema_direct}.›
subsection ‹Symbolic Preprocessing›
context gd_term
begin
definition sym_preproc_aux_term1 :: "('a ⇒ nat) ⇒ ((('t ⇒⇩0 'b) list × 't list × 't list × ('t ⇒⇩0 'b) list) ×
(('t ⇒⇩0 'b) list × 't list × 't list × ('t ⇒⇩0 'b) list)) set"
where "sym_preproc_aux_term1 d =
{((gs1, ks1, ts1, fs1), (gs2::('t ⇒⇩0 'b) list, ks2, ts2, fs2)). ∃t2∈set ts2. ∀t1∈set ts1. t1 ≺⇩t t2}"
definition sym_preproc_aux_term2 :: "('a ⇒ nat) ⇒ ((('t ⇒⇩0 'b::zero) list × 't list × 't list × ('t ⇒⇩0 'b) list) ×
(('t ⇒⇩0 'b) list × 't list × 't list × ('t ⇒⇩0 'b) list)) set"
where "sym_preproc_aux_term2 d =
{((gs1, ks1, ts1, fs1), (gs2::('t ⇒⇩0 'b) list, ks2, ts2, fs2)). gs1 = gs2 ∧
dgrad_set_le d (pp_of_term ` set ts1) (pp_of_term ` (Keys (set gs2) ∪ set ts2))}"
definition sym_preproc_aux_term
where "sym_preproc_aux_term d = sym_preproc_aux_term1 d ∩ sym_preproc_aux_term2 d"
lemma wfp_on_ord_term_strict:
assumes "dickson_grading d"
shows "wfp_on (≺⇩t) (pp_of_term -` dgrad_set d m)"
proof (rule wfp_onI_min)
fix x Q
assume "x ∈ Q" and "Q ⊆ pp_of_term -` dgrad_set d m"
from wf_dickson_less_v[OF assms, of m] ‹x ∈ Q› obtain z
where "z ∈ Q" and *: "⋀y. dickson_less_v d m y z ⟹ y ∉ Q" by (rule wfE_min[to_pred], blast)
from this(1) ‹Q ⊆ pp_of_term -` dgrad_set d m› have "z ∈ pp_of_term -` dgrad_set d m" ..
show "∃z∈Q. ∀y ∈ pp_of_term -` dgrad_set d m. y ≺⇩t z ⟶ y ∉ Q"
proof (intro bexI ballI impI, rule *)
fix y
assume "y ∈ pp_of_term -` dgrad_set d m" and "y ≺⇩t z"
from this(1) ‹z ∈ pp_of_term -` dgrad_set d m› have "d (pp_of_term y) ≤ m" and "d (pp_of_term z) ≤ m"
by (simp_all add: dgrad_set_def)
thus "dickson_less_v d m y z" using ‹y ≺⇩t z› by (rule dickson_less_vI)
qed fact
qed
lemma sym_preproc_aux_term1_wf_on:
assumes "dickson_grading d"
shows "wfp_on (λx y. (x, y) ∈ sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) ⊆ pp_of_term -` dgrad_set d m}"
proof (rule wfp_onI_min)
let ?B = "pp_of_term -` dgrad_set d m"
let ?A = "{x::(('t ⇒⇩0 'b) list × 't list × 't list × ('t ⇒⇩0 'b) list). set (fst (snd (snd x))) ⊆ ?B}"
have A_sub_Pow: "set ` fst ` snd ` snd ` ?A ⊆ Pow ?B" by auto
fix x Q
assume "x ∈ Q" and "Q ⊆ ?A"
let ?Q = "{ord_term_lin.Max (set (fst (snd (snd q)))) | q. q ∈ Q ∧ fst (snd (snd q)) ≠ []}"
show "∃z∈Q. ∀y∈{x. set (fst (snd (snd x))) ⊆ ?B}. (y, z) ∈ sym_preproc_aux_term1 d ⟶ y ∉ Q"
proof (cases "∃z∈Q. fst (snd (snd z)) = []")
case True
then obtain z where "z ∈ Q" and "fst (snd (snd z)) = []" ..
show ?thesis
proof (intro bexI ballI impI)
fix y
assume "(y, z) ∈ sym_preproc_aux_term1 d"
then obtain t where "t ∈ set (fst (snd (snd z)))" unfolding sym_preproc_aux_term1_def by auto
with ‹fst (snd (snd z)) = []› show "y ∉ Q" by simp
qed fact
next
case False
hence *: "q ∈ Q ⟹ fst (snd (snd q)) ≠ []" for q by blast
with ‹x ∈ Q› have "fst (snd (snd x)) ≠ []" by simp
from assms have "wfp_on (≺⇩t) ?B" by (rule wfp_on_ord_term_strict)
moreover from ‹x ∈ Q› ‹fst (snd (snd x)) ≠ []›
have "ord_term_lin.Max (set (fst (snd (snd x)))) ∈ ?Q" by blast
moreover have "?Q ⊆ ?B"
proof (rule, simp, elim exE conjE, simp)
fix a b c d0
assume "(a, b, c, d0) ∈ Q" and "c ≠ []"
from this(1) ‹Q ⊆ ?A› have "(a, b, c, d0) ∈ ?A" ..
hence "pp_of_term ` set c ⊆ dgrad_set d m" by auto
moreover have "pp_of_term (ord_term_lin.Max (set c)) ∈ pp_of_term ` set c"
proof
from ‹c ≠ []› show "ord_term_lin.Max (set c) ∈ set c" by simp
qed (fact refl)
ultimately show "pp_of_term (ord_term_lin.Max (set c)) ∈ dgrad_set d m" ..
qed
ultimately obtain t where "t ∈ ?Q" and min: "⋀s. s ≺⇩t t ⟹ s ∉ ?Q" by (rule wfp_onE_min) blast
from this(1) obtain z where "z ∈ Q" and "fst (snd (snd z)) ≠ []"
and t: "t = ord_term_lin.Max (set (fst (snd (snd z))))" by blast
show ?thesis
proof (intro bexI ballI impI, rule)
fix y
assume "y ∈ ?A" and "(y, z) ∈ sym_preproc_aux_term1 d" and "y ∈ Q"
from this(2) obtain t' where "t' ∈ set (fst (snd (snd z)))"
and **: "⋀s. s ∈ set (fst (snd (snd y))) ⟹ s ≺⇩t t'"
unfolding sym_preproc_aux_term1_def by auto
from ‹y ∈ Q› have "fst (snd (snd y)) ≠ []" by (rule *)
with ‹y ∈ Q› have "ord_term_lin.Max (set (fst (snd (snd y)))) ∈ ?Q" (is "?s ∈ _")
by blast
from ‹fst (snd (snd y)) ≠ []› have "?s ∈ set (fst (snd (snd y)))" by simp
hence "?s ≺⇩t t'" by (rule **)
also from ‹t' ∈ set (fst (snd (snd z)))› have "t' ≼⇩t t" unfolding t
using ‹fst (snd (snd z)) ≠ []› by simp
finally have "?s ∉ ?Q" by (rule min)
from this ‹?s ∈ ?Q› show False ..
qed fact
qed
qed
lemma sym_preproc_aux_term_wf:
assumes "dickson_grading d"
shows "wf (sym_preproc_aux_term d)"
proof (rule wfI_min)
fix x::"(('t ⇒⇩0 'b) list × 't list × 't list × ('t ⇒⇩0 'b) list)" and Q
assume "x ∈ Q"
let ?A = "Keys (set (fst x)) ∪ set (fst (snd (snd x)))"
have "finite ?A" by (simp add: finite_Keys)
hence "finite (pp_of_term ` ?A)" by (rule finite_imageI)
then obtain m where "pp_of_term ` ?A ⊆ dgrad_set d m" by (rule dgrad_set_exhaust)
hence A: "?A ⊆ pp_of_term -` dgrad_set d m" by blast
let ?B = "pp_of_term -` dgrad_set d m"
let ?Q = "{q ∈ Q. Keys (set (fst q)) ∪ set (fst (snd (snd q))) ⊆ ?B}"
from assms have "wfp_on (λx y. (x, y) ∈ sym_preproc_aux_term1 d) {x. set (fst (snd (snd x))) ⊆ ?B}"
by (rule sym_preproc_aux_term1_wf_on)
moreover from ‹x ∈ Q› A have "x ∈ ?Q" by simp
moreover have "?Q ⊆ {x. set (fst (snd (snd x))) ⊆ ?B}" by auto
ultimately obtain z where "z ∈ ?Q"
and *: "⋀y. (y, z) ∈ sym_preproc_aux_term1 d ⟹ y ∉ ?Q" by (rule wfp_onE_min) blast
from this(1) have "z ∈ Q" and "Keys (set (fst z)) ∪ set (fst (snd (snd z))) ⊆ ?B" by simp_all
from this(2) have a: "pp_of_term ` (Keys (set (fst z)) ∪ set (fst (snd (snd z)))) ⊆ dgrad_set d m"
by blast
show "∃z∈Q. ∀y. (y, z) ∈ sym_preproc_aux_term d ⟶ y ∉ Q"
proof (intro bexI allI impI)
fix y
assume "(y, z) ∈ sym_preproc_aux_term d"
hence "(y, z) ∈ sym_preproc_aux_term1 d" and "(y, z) ∈ sym_preproc_aux_term2 d"
by (simp_all add: sym_preproc_aux_term_def)
from this(2) have "fst y = fst z"
and "dgrad_set_le d (pp_of_term ` set (fst (snd (snd y)))) (pp_of_term ` (Keys (set (fst z)) ∪ set (fst (snd (snd z)))))"
by (auto simp add: sym_preproc_aux_term2_def)
from this(2) a have "pp_of_term ` (set (fst (snd (snd y)))) ⊆ dgrad_set d m"
by (rule dgrad_set_le_dgrad_set)
hence "Keys (set (fst y)) ∪ set (fst (snd (snd y))) ⊆ ?B"
using a by (auto simp add: ‹fst y = fst z›)
moreover from ‹(y, z) ∈ sym_preproc_aux_term1 d› have "y ∉ ?Q" by (rule *)
ultimately show "y ∉ Q" by simp
qed fact
qed
primrec sym_preproc_addnew :: "('t ⇒⇩0 'b::semiring_1) list ⇒ 't list ⇒ ('t ⇒⇩0 'b) list ⇒ 't ⇒
('t list × ('t ⇒⇩0 'b) list)" where
"sym_preproc_addnew [] vs fs _ = (vs, fs)"|
"sym_preproc_addnew (g # gs) vs fs v =
(if lt g adds⇩t v then
(let f = monom_mult 1 (pp_of_term v - lp g) g in
sym_preproc_addnew gs (merge_wrt (≻⇩t) vs (keys_to_list (tail f))) (insert_list f fs) v
)
else
sym_preproc_addnew gs vs fs v
)"
lemma fst_sym_preproc_addnew_less:
assumes "⋀u. u ∈ set vs ⟹ u ≺⇩t v"
and "u ∈ set (fst (sym_preproc_addnew gs vs fs v))"
shows "u ≺⇩t v"
using assms
proof (induct gs arbitrary: fs vs)
case Nil
from Nil(2) have "u ∈ set vs" by simp
thus ?case by (rule Nil(1))
next
case (Cons g gs)
from Cons(3) show ?case
proof (simp add: Let_def split: if_splits)
let ?t = "pp_of_term v - lp g"
assume "lt g adds⇩t v"
assume "u ∈ set (fst (sym_preproc_addnew gs
(merge_wrt (≻⇩t) vs (keys_to_list (tail (monom_mult 1 ?t g))))
(insert_list (monom_mult 1 ?t g) fs) v))"
with _ show ?thesis
proof (rule Cons(1))
fix u
assume "u ∈ set (merge_wrt (≻⇩t) vs (keys_to_list (tail (monom_mult 1 ?t g))))"
hence "u ∈ set vs ∨ u ∈ keys (tail (monom_mult 1 ?t g))"
by (simp add: set_merge_wrt keys_to_list_def set_pps_to_list)
thus "u ≺⇩t v"
proof
assume "u ∈ set vs"
thus ?thesis by (rule Cons(2))
next
assume "u ∈ keys (tail (monom_mult 1 ?t g))"
hence "u ≺⇩t lt (monom_mult 1 ?t g)" by (rule keys_tail_less_lt)
also have "... ≼⇩t ?t ⊕ lt g" by (rule lt_monom_mult_le)
also from ‹lt g adds⇩t v› have "... = v"
by (metis add_diff_cancel_right' adds_termE pp_of_term_splus)
finally show ?thesis .
qed
qed
next
assume "u ∈ set (fst (sym_preproc_addnew gs vs fs v))"
with Cons(2) show ?thesis by (rule Cons(1))
qed
qed
lemma fst_sym_preproc_addnew_dgrad_set_le:
assumes "dickson_grading d"
shows "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v))) (pp_of_term ` (Keys (set gs) ∪ insert v (set vs)))"
proof (induct gs arbitrary: fs vs)
case Nil
show ?case by (auto intro: dgrad_set_le_subset)
next
case (Cons g gs)
show ?case
proof (simp add: Let_def, intro conjI impI)
assume "lt g adds⇩t v"
let ?t = "pp_of_term v - lp g"
let ?vs = "merge_wrt (≻⇩t) vs (keys_to_list (tail (monom_mult 1 ?t g)))"
let ?fs = "insert_list (monom_mult 1 ?t g) fs"
from Cons have "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)))
(pp_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs)))"
proof (rule dgrad_set_le_trans)
show "dgrad_set_le d (pp_of_term ` (Keys (set gs) ∪ insert v (set ?vs)))
(pp_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs)))"
unfolding dgrad_set_le_def set_merge_wrt set_keys_to_list
proof (intro ballI)
fix s
assume "s ∈ pp_of_term ` (Keys (set gs) ∪ insert v (set vs ∪ keys (tail (monom_mult 1 ?t g))))"
hence "s ∈ pp_of_term ` (Keys (set gs) ∪ insert v (set vs)) ∪ pp_of_term ` keys (tail (monom_mult 1 ?t g))"
by auto
thus "∃t ∈ pp_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs)). d s ≤ d t"
proof
assume "s ∈ pp_of_term ` (Keys (set gs) ∪ insert v (set vs))"
thus ?thesis by (auto simp add: Keys_insert)
next
assume "s ∈ pp_of_term ` keys (tail (monom_mult 1 ?t g))"
hence "s ∈ pp_of_term ` keys (monom_mult 1 ?t g)" by (auto simp add: keys_tail)
from this keys_monom_mult_subset have "s ∈ pp_of_term ` (⊕) ?t ` keys g" by blast
then obtain u where "u ∈ keys g" and s: "s = pp_of_term (?t ⊕ u)" by blast
have "d s = d ?t ∨ d s = d (pp_of_term u)" unfolding s pp_of_term_splus
using dickson_gradingD1[OF assms] by auto
thus ?thesis
proof
from ‹lt g adds⇩t v› have "lp g adds pp_of_term v" by (simp add: adds_term_def)
assume "d s = d ?t"
also from assms ‹lp g adds pp_of_term v› have "... ≤ d (pp_of_term v)"
by (rule dickson_grading_minus)
finally show ?thesis by blast
next
assume "d s = d (pp_of_term u)"
moreover from ‹u ∈ keys g› have "u ∈ Keys (insert g (set gs))" by (simp add: Keys_insert)
ultimately show ?thesis by auto
qed
qed
qed
qed
thus "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)))
(insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) ∪ set vs)))"
by simp
next
from Cons show "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs fs v)))
(insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) ∪ set vs)))"
proof (rule dgrad_set_le_trans)
show "dgrad_set_le d (pp_of_term ` (Keys (set gs) ∪ insert v (set vs)))
(insert (pp_of_term v) (pp_of_term ` (Keys (insert g (set gs)) ∪ set vs)))"
by (rule dgrad_set_le_subset, auto simp add: Keys_def)
qed
qed
qed
lemma components_fst_sym_preproc_addnew_subset:
"component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) ⊆ component_of_term ` (Keys (set gs) ∪ insert v (set vs))"
proof (induct gs arbitrary: fs vs)
case Nil
show ?case by (auto intro: dgrad_set_le_subset)
next
case (Cons g gs)
show ?case
proof (simp add: Let_def, intro conjI impI)
assume "lt g adds⇩t v"
let ?t = "pp_of_term v - lp g"
let ?vs = "merge_wrt (≻⇩t) vs (keys_to_list (tail (monom_mult 1 ?t g)))"
let ?fs = "insert_list (monom_mult 1 ?t g) fs"
from Cons have "component_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)) ⊆
component_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs))"
proof (rule subset_trans)
show "component_of_term ` (Keys (set gs) ∪ insert v (set ?vs)) ⊆
component_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs))"
unfolding set_merge_wrt set_keys_to_list
proof
fix k
assume "k ∈ component_of_term ` (Keys (set gs) ∪ insert v (set vs ∪ keys (tail (monom_mult 1 ?t g))))"
hence "k ∈ component_of_term ` (Keys (set gs) ∪ insert v (set vs)) ∪ component_of_term ` keys (tail (monom_mult 1 ?t g))"
by auto
thus "k ∈ component_of_term ` (Keys (insert g (set gs)) ∪ insert v (set vs))"
proof
assume "k ∈ component_of_term ` (Keys (set gs) ∪ insert v (set vs))"
thus ?thesis by (auto simp add: Keys_insert)
next
assume "k ∈ component_of_term ` keys (tail (monom_mult 1 ?t g))"
hence "k ∈ component_of_term ` keys (monom_mult 1 ?t g)" by (auto simp add: keys_tail)
from this keys_monom_mult_subset have "k ∈ component_of_term ` (⊕) ?t ` keys g" by blast
also have "... ⊆ component_of_term ` keys g" using component_of_term_splus by fastforce
finally show ?thesis by (simp add: image_Un Keys_insert)
qed
qed
qed
thus "component_of_term ` set (fst (sym_preproc_addnew gs ?vs ?fs v)) ⊆
insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) ∪ set vs))"
by simp
next
from Cons show "component_of_term ` set (fst (sym_preproc_addnew gs vs fs v)) ⊆
insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) ∪ set vs))"
proof (rule subset_trans)
show "component_of_term ` (Keys (set gs) ∪ insert v (set vs)) ⊆
insert (component_of_term v) (component_of_term ` (Keys (insert g (set gs)) ∪ set vs))"
by (auto simp add: Keys_def)
qed
qed
qed
lemma fst_sym_preproc_addnew_superset: "set vs ⊆ set (fst (sym_preproc_addnew gs vs fs v))"
proof (induct gs arbitrary: vs fs)
case Nil
show ?case by simp
next
case (Cons g gs)
show ?case
proof (simp add: Let_def, intro conjI impI)
let ?t = "pp_of_term v - lp g"
define f where "f = monom_mult 1 ?t g"
have "set vs ⊆ set (merge_wrt (≻⇩t) vs (keys_to_list (tail f)))" by (auto simp add: set_merge_wrt)
thus "set vs ⊆ set (fst (sym_preproc_addnew gs
(merge_wrt (≻⇩t) vs (keys_to_list (tail f))) (insert_list f fs) v))"
using Cons by (rule subset_trans)
next
show "set vs ⊆ set (fst (sym_preproc_addnew gs vs fs v))" by (fact Cons)
qed
qed
lemma snd_sym_preproc_addnew_superset: "set fs ⊆ set (snd (sym_preproc_addnew gs vs fs v))"
proof (induct gs arbitrary: vs fs)
case Nil
show ?case by simp
next
case (Cons g gs)
show ?case
proof (simp add: Let_def, intro conjI impI)
let ?t = "pp_of_term v - lp g"
define f where "f = monom_mult 1 ?t g"
have "set fs ⊆ set (insert_list f fs)" by (auto simp add: set_insert_list)
thus "set fs ⊆ set (snd (sym_preproc_addnew gs
(merge_wrt (≻⇩t) vs (keys_to_list (tail f))) (insert_list f fs) v))"
using Cons by (rule subset_trans)
next
show "set fs ⊆ set (snd (sym_preproc_addnew gs vs fs v))" by (fact Cons)
qed
qed
lemma in_snd_sym_preproc_addnewE:
assumes "p ∈ set (snd (sym_preproc_addnew gs vs fs v))"
assumes 1: "p ∈ set fs ⟹ thesis"
assumes 2: "⋀g s. g ∈ set gs ⟹ p = monom_mult 1 s g ⟹ thesis"
shows thesis
using assms
proof (induct gs arbitrary: vs fs thesis)
case Nil
from Nil(1) have "p ∈ set fs" by simp
thus ?case by (rule Nil(2))
next
case (Cons g gs)
from Cons(2) show ?case
proof (simp add: Let_def split: if_splits)
define f where "f = monom_mult 1 (pp_of_term v - lp g) g"
define ts' where "ts' = merge_wrt (≻⇩t) vs (keys_to_list (tail f))"
define fs' where "fs' = insert_list f fs"
assume "p ∈ set (snd (sym_preproc_addnew gs ts' fs' v))"
thus ?thesis
proof (rule Cons(1))
assume "p ∈ set fs'"
hence "p = f ∨ p ∈ set fs" by (simp add: fs'_def set_insert_list)
thus ?thesis
proof
assume "p = f"
have "g ∈ set (g # gs)" by simp
from this ‹p = f› show ?thesis unfolding f_def by (rule Cons(4))
next
assume "p ∈ set fs"
thus ?thesis by (rule Cons(3))
qed
next
fix h s
assume "h ∈ set gs"
hence "h ∈ set (g # gs)" by simp
moreover assume "p = monom_mult 1 s h"
ultimately show thesis by (rule Cons(4))
qed
next
assume "p ∈ set (snd (sym_preproc_addnew gs vs fs v))"
moreover note Cons(3)
moreover have "h ∈ set gs ⟹ p = monom_mult 1 s h ⟹ thesis" for h s
proof -
assume "h ∈ set gs"
hence "h ∈ set (g # gs)" by simp
moreover assume "p = monom_mult 1 s h"
ultimately show thesis by (rule Cons(4))
qed
ultimately show ?thesis by (rule Cons(1))
qed
qed
lemma sym_preproc_addnew_pmdl:
"pmdl (set gs ∪ set (snd (sym_preproc_addnew gs vs fs v))) = pmdl (set gs ∪ set fs)"
(is "pmdl (set gs ∪ ?l) = ?r")
proof
have "set gs ⊆ set gs ∪ set fs" by simp
also have "... ⊆ ?r" by (fact pmdl.span_superset)
finally have "set gs ⊆ ?r" .
moreover have "?l ⊆ ?r"
proof
fix p
assume "p ∈ ?l"
thus "p ∈ ?r"
proof (rule in_snd_sym_preproc_addnewE)
assume "p ∈ set fs"
hence "p ∈ set gs ∪ set fs" by simp
thus ?thesis by (rule pmdl.span_base)
next
fix g s
assume "g ∈ set gs" and p: "p = monom_mult 1 s g"
from this(1) ‹set gs ⊆ ?r› have "g ∈ ?r" ..
thus ?thesis unfolding p by (rule pmdl_closed_monom_mult)
qed
qed
ultimately have "set gs ∪ ?l ⊆ ?r" by blast
thus "pmdl (set gs ∪ ?l) ⊆ ?r" by (rule pmdl.span_subset_spanI)
next
from snd_sym_preproc_addnew_superset have "set gs ∪ set fs ⊆ set gs ∪ ?l" by blast
thus "?r ⊆ pmdl (set gs ∪ ?l)" by (rule pmdl.span_mono)
qed
lemma Keys_snd_sym_preproc_addnew:
"Keys (set (snd (sym_preproc_addnew gs vs fs v))) ∪ insert v (set vs) =
Keys (set fs) ∪ insert v (set (fst (sym_preproc_addnew gs vs (fs::('t ⇒⇩0 'b::semiring_1_no_zero_divisors) list) v)))"
proof (induct gs arbitrary: vs fs)
case Nil
show ?case by simp
next
case (Cons g gs)
from Cons have eq: "insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) ∪ set ts') =
insert v (Keys (set fs') ∪ set (fst (sym_preproc_addnew gs ts' fs' v)))"
for ts' fs' by simp
show ?case
proof (simp add: Let_def eq, rule)
assume "lt g adds⇩t v"
let ?t = "pp_of_term v - lp g"
define f where "f = monom_mult 1 ?t g"
define ts' where "ts' = merge_wrt (≻⇩t) vs (keys_to_list (tail f))"
define fs' where "fs' = insert_list f fs"
have "keys (tail f) = keys f - {v}"
proof (cases "g = 0")
case True
hence "f = 0" by (simp add: f_def)
thus ?thesis by simp
next
case False
hence "lt f = ?t ⊕ lt g" by (simp add: f_def lt_monom_mult)
also from ‹lt g adds⇩t v› have "... = v"
by (metis add_diff_cancel_right' adds_termE pp_of_term_splus)
finally show ?thesis by (simp add: keys_tail)
qed
hence ts': "set ts' = set vs ∪ (keys f - {v})"
by (simp add: ts'_def set_merge_wrt set_keys_to_list)
have fs': "set fs' = insert f (set fs)" by (simp add: fs'_def set_insert_list)
hence "f ∈ set fs'" by simp
from this snd_sym_preproc_addnew_superset have "f ∈ set (snd (sym_preproc_addnew gs ts' fs' v))" ..
hence "keys f ⊆ Keys (set (snd (sym_preproc_addnew gs ts' fs' v)))" by (rule keys_subset_Keys)
hence "insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) ∪ set vs) =
insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) ∪ set ts')"
by (auto simp add: ts')
also have "... = insert v (Keys (set fs') ∪ set (fst (sym_preproc_addnew gs ts' fs' v)))"
by (fact eq)
also have "... = insert v (Keys (set fs) ∪ set (fst (sym_preproc_addnew gs ts' fs' v)))"
proof -
{
fix u
assume "u ≠ v" and "u ∈ keys f"
hence "u ∈ set ts'" by (simp add: ts')
from this fst_sym_preproc_addnew_superset have "u ∈ set (fst (sym_preproc_addnew gs ts' fs' v))" ..
}
thus ?thesis by (auto simp add: fs' Keys_insert)
qed
finally show "insert v (Keys (set (snd (sym_preproc_addnew gs ts' fs' v))) ∪ set vs) =
insert v (Keys (set fs) ∪ set (fst (sym_preproc_addnew gs ts' fs' v)))" .
qed
qed
lemma sym_preproc_addnew_complete:
assumes "g ∈ set gs" and "lt g adds⇩t v"
shows "monom_mult 1 (pp_of_term v - lp g) g ∈ set (snd (sym_preproc_addnew gs vs fs v))"
using assms(1)
proof (induct gs arbitrary: vs fs)
case Nil
thus ?case by simp
next
case (Cons h gs)
let ?t = "pp_of_term v - lp g"
show ?case
proof (cases "h = g")
case True
show ?thesis
proof (simp add: True assms(2) Let_def)
define f where "f = monom_mult 1 ?t g"
define ts' where "ts' = merge_wrt (≻⇩t) vs (keys_to_list (tail (monom_mult 1 ?t g)))"
have "f ∈ set (insert_list f fs)" by (simp add: set_insert_list)
with snd_sym_preproc_addnew_superset show "f ∈ set (snd (sym_preproc_addnew gs ts' (insert_list f fs) v))" ..
qed
next
case False
with Cons(2) have "g ∈ set gs" by simp
hence *: "monom_mult 1 ?t g ∈ set (snd (sym_preproc_addnew gs ts' fs' v))" for ts' fs'
by (rule Cons(1))
show ?thesis by (simp add: Let_def *)
qed
qed
function sym_preproc_aux :: "('t ⇒⇩0 'b::semiring_1) list ⇒ 't list ⇒ ('t list × ('t ⇒⇩0 'b) list) ⇒
('t list × ('t ⇒⇩0 'b) list)" where
"sym_preproc_aux gs ks (vs, fs) =
(if vs = [] then
(ks, fs)
else
let v = ord_term_lin.max_list vs; vs' = removeAll v vs in
sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)
)"
by pat_completeness auto
termination proof -
from ex_dgrad obtain d::"'a ⇒ nat" where dg: "dickson_grading d" ..
let ?R = "(sym_preproc_aux_term d)::((('t ⇒⇩0 'b) list × 't list × 't list × ('t ⇒⇩0 'b) list) ×
('t ⇒⇩0 'b) list × 't list × 't list × ('t ⇒⇩0 'b) list) set"
show ?thesis
proof
from dg show "wf ?R" by (rule sym_preproc_aux_term_wf)
next
fix gs::"('t ⇒⇩0 'b) list" and ks vs fs v vs'
assume "vs ≠ []" and "v = ord_term_lin.max_list vs" and vs': "vs' = removeAll v vs"
from this(1, 2) have v: "v = ord_term_lin.Max (set vs)"
by (simp add: ord_term_lin.max_list_Max)
obtain vs0 fs0 where eq: "sym_preproc_addnew gs vs' fs v = (vs0, fs0)" by fastforce
show "((gs, ks @ [v], sym_preproc_addnew gs vs' fs v), (gs, ks, vs, fs)) ∈ ?R"
proof (simp add: eq sym_preproc_aux_term_def sym_preproc_aux_term1_def sym_preproc_aux_term2_def,
intro conjI bexI ballI)
fix w
assume "w ∈ set vs0"
show "w ≺⇩t v"
proof (rule fst_sym_preproc_addnew_less)
fix u
assume "u ∈ set vs'"
thus "u ≺⇩t v" unfolding vs' v set_removeAll using ord_term_lin.antisym_conv1 by fastforce
next
from ‹w ∈ set vs0› show "w ∈ set (fst (sym_preproc_addnew gs vs' fs v))" by (simp add: eq)
qed
next
from ‹vs ≠ []› show "v ∈ set vs" by (simp add: v)
next
from dg have "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs' fs v)))
(pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
by (rule fst_sym_preproc_addnew_dgrad_set_le)
moreover have "insert v (set vs') = set vs" by (auto simp add: vs' v ‹vs ≠ []›)
ultimately show "dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) ∪ set vs))"
by (simp add: eq)
qed
qed
qed
lemma sym_preproc_aux_Nil: "sym_preproc_aux gs ks ([], fs) = (ks, fs)"
by simp
lemma sym_preproc_aux_sorted:
assumes "sorted_wrt (≻⇩t) (v # vs)"
shows "sym_preproc_aux gs ks (v # vs, fs) = sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs fs v)"
proof -
from assms have *: "u ∈ set vs ⟹ u ≺⇩t v" for u by simp
have "ord_term_lin.max_list (v # vs) = ord_term_lin.Max (set (v # vs))"
by (simp add: ord_term_lin.max_list_Max del: ord_term_lin.max_list.simps)
also have "... = v"
proof (rule ord_term_lin.Max_eqI)
fix s
assume "s ∈ set (v # vs)"
hence "s = v ∨ s ∈ set vs" by simp
thus "s ≼⇩t v"
proof
assume "s = v"
thus ?thesis by simp
next
assume "s ∈ set vs"
hence "s ≺⇩t v" by (rule *)
thus ?thesis by simp
qed
next
show "v ∈ set (v # vs)" by simp
qed rule
finally have eq1: "ord_term_lin.max_list (v # vs) = v" .
have eq2: "removeAll v (v # vs) = vs"
proof (simp, rule removeAll_id, rule)
assume "v ∈ set vs"
hence "v ≺⇩t v" by (rule *)
thus False ..
qed
show ?thesis by (simp only: sym_preproc_aux.simps eq1 eq2 Let_def, simp)
qed
lemma sym_preproc_aux_induct [consumes 0, case_names base rec]:
assumes base: "⋀ks fs. P ks [] fs (ks, fs)"
and rec: "⋀ks vs fs v vs'. vs ≠ [] ⟹ v = ord_term_lin.Max (set vs) ⟹ vs' = removeAll v vs ⟹
P (ks @ [v]) (fst (sym_preproc_addnew gs vs' fs v)) (snd (sym_preproc_addnew gs vs' fs v))
(sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v)) ⟹
P ks vs fs (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))"
shows "P ks vs fs (sym_preproc_aux gs ks (vs, fs))"
proof -
from ex_dgrad obtain d::"'a ⇒ nat" where dg: "dickson_grading d" ..
let ?R = "(sym_preproc_aux_term d)::((('t ⇒⇩0 'b) list × 't list × 't list × ('t ⇒⇩0 'b) list) ×
('t ⇒⇩0 'b) list × 't list × 't list × ('t ⇒⇩0 'b) list) set"
define args where "args = (gs, ks, vs, fs)"
from dg have "wf ?R" by (rule sym_preproc_aux_term_wf)
hence "fst args = gs ⟹ P (fst (snd args)) (fst (snd (snd args))) (snd (snd (snd args)))
(sym_preproc_aux gs (fst (snd args)) (snd (snd args)))"
proof induct
fix x
assume IH': "⋀y. (y, x) ∈ sym_preproc_aux_term d ⟹ fst y = gs ⟹
P (fst (snd y)) (fst (snd (snd y))) (snd (snd (snd y)))
(sym_preproc_aux gs (fst (snd y)) (snd (snd y)))"
assume "fst x = gs"
then obtain x0 where x: "x = (gs, x0)" by (meson eq_fst_iff)
obtain ks x1 where x0: "x0 = (ks, x1)" by (meson case_prodE case_prodI2)
obtain vs fs where x1: "x1 = (vs, fs)" by (meson case_prodE case_prodI2)
from IH' have IH: "⋀ks' n. ((gs, ks', n), (gs, ks, vs, fs)) ∈ sym_preproc_aux_term d ⟹
P ks' (fst n) (snd n) (sym_preproc_aux gs ks' n)"
unfolding x x0 x1 by fastforce
show "P (fst (snd x)) (fst (snd (snd x))) (snd (snd (snd x)))
(sym_preproc_aux gs (fst (snd x)) (snd (snd x)))"
proof (simp add: x x0 x1 Let_def, intro conjI impI)
show "P ks [] fs (ks, fs)" by (fact base)
next
assume "vs ≠ []"
define v where "v = ord_term_lin.max_list vs"
from ‹vs ≠ []› have v_alt: "v = ord_term_lin.Max (set vs)" unfolding v_def
by (rule ord_term_lin.max_list_Max)
define vs' where "vs' = removeAll v vs"
show "P ks vs fs (sym_preproc_aux gs (ks @ [v]) (sym_preproc_addnew gs vs' fs v))"
proof (rule rec, fact ‹vs ≠ []›, fact v_alt, fact vs'_def)
let ?n = "sym_preproc_addnew gs vs' fs v"
obtain vs0 fs0 where eq: "?n = (vs0, fs0)" by fastforce
show "P (ks @ [v]) (fst ?n) (snd ?n) (sym_preproc_aux gs (ks @ [v]) ?n)"
proof (rule IH,
simp add: eq sym_preproc_aux_term_def sym_preproc_aux_term1_def sym_preproc_aux_term2_def,
intro conjI bexI ballI)
fix s
assume "s ∈ set vs0"
show "s ≺⇩t v"
proof (rule fst_sym_preproc_addnew_less)
fix u
assume "u ∈ set vs'"
thus "u ≺⇩t v" unfolding vs'_def v_alt set_removeAll using ord_term_lin.antisym_conv1
by fastforce
next
from ‹s ∈ set vs0› show "s ∈ set (fst (sym_preproc_addnew gs vs' fs v))" by (simp add: eq)
qed
next
from ‹vs ≠ []› show "v ∈ set vs" by (simp add: v_alt)
next
from dg have "dgrad_set_le d (pp_of_term ` set (fst (sym_preproc_addnew gs vs' fs v)))
(pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
by (rule fst_sym_preproc_addnew_dgrad_set_le)
moreover have "insert v (set vs') = set vs" by (auto simp add: vs'_def v_alt ‹vs ≠ []›)
ultimately show "dgrad_set_le d (pp_of_term ` set vs0) (pp_of_term ` (Keys (set gs) ∪ set vs))"
by (simp add: eq)
qed
qed
qed
qed
thus ?thesis by (simp add: args_def)
qed
lemma fst_sym_preproc_aux_sorted_wrt:
assumes "sorted_wrt (≻⇩t) ks" and "⋀k v. k ∈ set ks ⟹ v ∈ set vs ⟹ v ≺⇩t k"
shows "sorted_wrt (≻⇩t) (fst (sym_preproc_aux gs ks (vs, fs)))"
using assms
proof (induct gs ks vs fs rule: sym_preproc_aux_induct)
case (base ks fs)
from base(1) show ?case by simp
next
case (rec ks vs fs v vs')
from rec(1) have "v ∈ set vs" by (simp add: rec(2))
from rec(1) have *: "⋀u. u ∈ set vs' ⟹ u ≺⇩t v" unfolding rec(2, 3) set_removeAll
using ord_term_lin.antisym_conv3 by force
show ?case
proof (rule rec(4))
show "sorted_wrt (≻⇩t) (ks @ [v])"
proof (simp add: sorted_wrt_append rec(5), rule)
fix k
assume "k ∈ set ks"
from this ‹v ∈ set vs› show "v ≺⇩t k" by (rule rec(6))
qed
next
fix k u
assume "k ∈ set (ks @ [v])" and "u ∈ set (fst (sym_preproc_addnew gs vs' fs v))"
from * this(2) have "u ≺⇩t v" by (rule fst_sym_preproc_addnew_less)
from ‹k ∈ set (ks @ [v])› have "k ∈ set ks ∨ k = v" by auto
thus "u ≺⇩t k"
proof
assume "k ∈ set ks"
from this ‹v ∈ set vs› have "v ≺⇩t k" by (rule rec(6))
with ‹u ≺⇩t v› show ?thesis by simp
next
assume "k = v"
with ‹u ≺⇩t v› show ?thesis by simp
qed
qed
qed
lemma fst_sym_preproc_aux_complete:
assumes "Keys (set (fs::('t ⇒⇩0 'b::semiring_1_no_zero_divisors) list)) = set ks ∪ set vs"
shows "set (fst (sym_preproc_aux gs ks (vs, fs))) = Keys (set (snd (sym_preproc_aux gs ks (vs, fs))))"
using assms
proof (induct gs ks vs fs rule: sym_preproc_aux_induct)
case (base ks fs)
thus ?case by simp
next
case (rec ks vs fs v vs')
from rec(1) have "v ∈ set vs" by (simp add: rec(2))
hence eq: "insert v (set vs') = set vs" by (auto simp add: rec(3))
also from rec(5) have "... ⊆ Keys (set fs)" by simp
also from snd_sym_preproc_addnew_superset have "... ⊆ Keys (set (snd (sym_preproc_addnew gs vs' fs v)))"
by (rule Keys_mono)
finally have "... = ... ∪ (insert v (set vs'))" by blast
also have "... = Keys (set fs) ∪ insert v (set (fst (sym_preproc_addnew gs vs' fs v)))"
by (fact Keys_snd_sym_preproc_addnew)
also have "... = (set ks ∪ (insert v (set vs'))) ∪ (insert v (set (fst (sym_preproc_addnew gs vs' fs v))))"
by (simp only: rec(5) eq)
also have "... = set (ks @ [v]) ∪ (set vs' ∪ set (fst (sym_preproc_addnew gs vs' fs v)))" by auto
also from fst_sym_preproc_addnew_superset have "... = set (ks @ [v]) ∪ set (fst (sym_preproc_addnew gs vs' fs v))"
by blast
finally show ?case by (rule rec(4))
qed
lemma snd_sym_preproc_aux_superset: "set fs ⊆ set (snd (sym_preproc_aux gs ks (vs, fs)))"
proof (induct fs rule: sym_preproc_aux_induct)
case (base ks fs)
show ?case by simp
next
case (rec ks vs fs v vs')
from snd_sym_preproc_addnew_superset rec(4) show ?case by (rule subset_trans)
qed
lemma in_snd_sym_preproc_auxE:
assumes "p ∈ set (snd (sym_preproc_aux gs ks (vs, fs)))"
assumes 1: "p ∈ set fs ⟹ thesis"
assumes 2: "⋀g t. g ∈ set gs ⟹ p = monom_mult 1 t g ⟹ thesis"
shows thesis
using assms
proof (induct gs ks vs fs arbitrary: thesis rule: sym_preproc_aux_induct)
case (base ks fs)
from base(1) have "p ∈ set fs" by simp
thus ?case by (rule base(2))
next
case (rec ks vs fs v vs')
from rec(5) show ?case
proof (rule rec(4))
assume "p ∈ set (snd (sym_preproc_addnew gs vs' fs v))"
thus ?thesis
proof (rule in_snd_sym_preproc_addnewE)
assume "p ∈ set fs"
thus ?thesis by (rule rec(6))
next
fix g s
assume "g ∈ set gs" and "p = monom_mult 1 s g"
thus ?thesis by (rule rec(7))
qed
next
fix g t
assume "g ∈ set gs" and "p = monom_mult 1 t g"
thus ?thesis by (rule rec(7))
qed
qed
lemma snd_sym_preproc_aux_pmdl:
"pmdl (set gs ∪ set (snd (sym_preproc_aux gs ks (ts, fs)))) = pmdl (set gs ∪ set fs)"
proof (induct fs rule: sym_preproc_aux_induct)
case (base ks fs)
show ?case by simp
next
case (rec ks vs fs v vs')
from rec(4) sym_preproc_addnew_pmdl show ?case by (rule trans)
qed
lemma snd_sym_preproc_aux_dgrad_set_le:
assumes "dickson_grading d" and "set vs ⊆ Keys (set (fs::('t ⇒⇩0 'b::semiring_1_no_zero_divisors) list))"
shows "dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_aux gs ks (vs, fs))))) (pp_of_term ` Keys (set gs ∪ set fs))"
using assms(2)
proof (induct fs rule: sym_preproc_aux_induct)
case (base ks fs)
show ?case by (rule dgrad_set_le_subset, simp add: Keys_Un image_Un)
next
case (rec ks vs fs v vs')
let ?n = "sym_preproc_addnew gs vs' fs v"
from rec(1) have "v ∈ set vs" by (simp add: rec(2))
hence set_vs: "insert v (set vs') = set vs" by (auto simp add: rec(3))
from rec(5) have eq: "Keys (set fs) ∪ (Keys (set gs) ∪ set vs) = Keys (set gs) ∪ Keys (set fs)"
by blast
have "dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) ?n))))
(pp_of_term ` Keys (set gs ∪ set (snd ?n)))"
proof (rule rec(4))
have "set (fst ?n) ⊆ Keys (set (snd ?n)) ∪ insert v (set vs')"
by (simp only: Keys_snd_sym_preproc_addnew, blast)
also have "... = Keys (set (snd ?n)) ∪ (set vs)" by (simp only: set_vs)
also have "... ⊆ Keys (set (snd ?n))"
proof -
{
fix u
assume "u ∈ set vs"
with rec(5) have "u ∈ Keys (set fs)" ..
then obtain f where "f ∈ set fs" and "u ∈ keys f" by (rule in_KeysE)
from this(1) snd_sym_preproc_addnew_superset have "f ∈ set (snd ?n)" ..
with ‹u ∈ keys f› have "u ∈ Keys (set (snd ?n))" by (rule in_KeysI)
}
thus ?thesis by auto
qed
finally show "set (fst ?n) ⊆ Keys (set (snd ?n))" .
qed
also have "dgrad_set_le d ... (pp_of_term ` Keys (set gs ∪ set fs))"
proof (simp only: image_Un Keys_Un dgrad_set_le_Un, rule)
show "dgrad_set_le d (pp_of_term ` Keys (set gs)) (pp_of_term ` Keys (set gs) ∪ pp_of_term ` Keys (set fs))"
by (rule dgrad_set_le_subset, simp)
next
have "dgrad_set_le d (pp_of_term ` Keys (set (snd ?n))) (pp_of_term ` (Keys (set fs) ∪ insert v (set (fst ?n))))"
by (rule dgrad_set_le_subset, auto simp only: Keys_snd_sym_preproc_addnew[symmetric])
also have "dgrad_set_le d ... (pp_of_term ` Keys (set fs) ∪ pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
proof (simp only: dgrad_set_le_Un image_Un, rule)
show "dgrad_set_le d (pp_of_term ` Keys (set fs))
(pp_of_term ` Keys (set fs) ∪ (pp_of_term ` Keys (set gs) ∪ pp_of_term ` insert v (set vs')))"
by (rule dgrad_set_le_subset, blast)
next
have "dgrad_set_le d (pp_of_term ` {v}) (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
by (rule dgrad_set_le_subset, simp)
moreover from assms(1) have "dgrad_set_le d (pp_of_term ` set (fst ?n)) (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
by (rule fst_sym_preproc_addnew_dgrad_set_le)
ultimately have "dgrad_set_le d (pp_of_term ` ({v} ∪ set (fst ?n))) (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))"
by (simp only: dgrad_set_le_Un image_Un)
also have "dgrad_set_le d (pp_of_term ` (Keys (set gs) ∪ insert v (set vs')))
(pp_of_term ` (Keys (set fs) ∪ (Keys (set gs) ∪ insert v (set vs'))))"
by (rule dgrad_set_le_subset, blast)
finally show "dgrad_set_le d (pp_of_term ` insert v (set (fst ?n)))
(pp_of_term ` Keys (set fs) ∪ (pp_of_term ` Keys (set gs) ∪ pp_of_term ` insert v (set vs')))"
by (simp add: image_Un)
qed
finally show "dgrad_set_le d (pp_of_term ` Keys (set (snd ?n))) (pp_of_term ` Keys (set gs) ∪ pp_of_term ` Keys (set fs))"
by (simp only: set_vs eq, metis eq image_Un)
qed
finally show ?case .
qed
lemma components_snd_sym_preproc_aux_subset:
assumes "set vs ⊆ Keys (set (fs::('t ⇒⇩0 'b::semiring_1_no_zero_divisors) list))"
shows "component_of_term ` Keys (set (snd (sym_preproc_aux gs ks (vs, fs)))) ⊆
component_of_term ` Keys (set gs ∪ set fs)"
using assms
proof (induct fs rule: sym_preproc_aux_induct)
case (base ks fs)
show ?case by (simp add: Keys_Un image_Un)
next
case (rec ks vs fs v vs')
let ?n = "sym_preproc_addnew gs vs' fs v"
from rec(1) have "v ∈ set vs" by (simp add: rec(2))
hence set_vs: "insert v (set vs') = set vs" by (auto simp add: rec(3))
from rec(5) have eq: "Keys (set fs) ∪ (Keys (set gs) ∪ set vs) = Keys (set gs) ∪ Keys (set fs)"
by blast
have "component_of_term ` Keys (set (snd (sym_preproc_aux gs (ks @ [v]) ?n))) ⊆
component_of_term ` Keys (set gs ∪ set (snd ?n))"
proof (rule rec(4))
have "set (fst ?n) ⊆ Keys (set (snd ?n)) ∪ insert v (set vs')"
by (simp only: Keys_snd_sym_preproc_addnew, blast)
also have "... = Keys (set (snd ?n)) ∪ (set vs)" by (simp only: set_vs)
also have "... ⊆ Keys (set (snd ?n))"
proof -
{
fix u
assume "u ∈ set vs"
with rec(5) have "u ∈ Keys (set fs)" ..
then obtain f where "f ∈ set fs" and "u ∈ keys f" by (rule in_KeysE)
from this(1) snd_sym_preproc_addnew_superset have "f ∈ set (snd ?n)" ..
with ‹u ∈ keys f› have "u ∈ Keys (set (snd ?n))" by (rule in_KeysI)
}
thus ?thesis by auto
qed
finally show "set (fst ?n) ⊆ Keys (set (snd ?n))" .
qed
also have "... ⊆ component_of_term ` Keys (set gs ∪ set fs)"
proof (simp only: image_Un Keys_Un Un_subset_iff, rule, fact Un_upper1)
have "component_of_term ` Keys (set (snd ?n)) ⊆ component_of_term ` (Keys (set fs) ∪ insert v (set (fst ?n)))"
by (auto simp only: Keys_snd_sym_preproc_addnew[symmetric])
also have "... ⊆ component_of_term ` Keys (set fs) ∪ component_of_term ` (Keys (set gs) ∪ insert v (set vs'))"
proof (simp only: Un_subset_iff image_Un, rule, fact Un_upper1)
have "component_of_term ` {v} ⊆ component_of_term ` (Keys (set gs) ∪ insert v (set vs'))"
by simp
moreover have "component_of_term ` set (fst ?n) ⊆ component_of_term ` (Keys (set gs) ∪ insert v (set vs'))"
by (rule components_fst_sym_preproc_addnew_subset)
ultimately have "component_of_term ` ({v} ∪ set (fst ?n)) ⊆ component_of_term ` (Keys (set gs) ∪ insert v (set vs'))"
by (simp only: Un_subset_iff image_Un)
also have "component_of_term ` (Keys (set gs) ∪ insert v (set vs')) ⊆
component_of_term ` (Keys (set fs) ∪ (Keys (set gs) ∪ insert v (set vs')))"
by blast
finally show "component_of_term ` insert v (set (fst ?n)) ⊆
component_of_term ` Keys (set fs) ∪
(component_of_term ` Keys (set gs) ∪ component_of_term ` insert v (set vs'))"
by (simp add: image_Un)
qed
finally show "component_of_term ` Keys (set (snd ?n)) ⊆
component_of_term ` Keys (set gs) ∪ component_of_term ` Keys (set fs)"
by (simp only: set_vs eq, metis eq image_Un)
qed
finally show ?case .
qed
lemma snd_sym_preproc_aux_complete:
assumes "⋀u' g'. u' ∈ Keys (set fs) ⟹ u' ∉ set vs ⟹ g' ∈ set gs ⟹ lt g' adds⇩t u' ⟹
monom_mult 1 (pp_of_term u' - lp g') g' ∈ set fs"
assumes "u ∈ Keys (set (snd (sym_preproc_aux gs ks (vs, fs))))" and "g ∈ set gs" and "lt g adds⇩t u"
shows "monom_mult (1::'b::semiring_1_no_zero_divisors) (pp_of_term u - lp g) g ∈
set (snd (sym_preproc_aux gs ks (vs, fs)))"
using assms
proof (induct fs rule: sym_preproc_aux_induct)
case (base ks fs)
from base(2) have "u ∈ Keys (set fs)" by simp
from this _ base(3, 4) have "monom_mult 1 (pp_of_term u - lp g) g ∈ set fs"
proof (rule base(1))
show "u ∉ set []" by simp
qed
thus ?case by simp
next
case (rec ks vs fs v vs')
from rec(1) have "v ∈ set vs" by (simp add: rec(2))
hence set_ts: "set vs = insert v (set vs')" by (auto simp add: rec(3))
let ?n = "sym_preproc_addnew gs vs' fs v"
from _ rec(6, 7, 8) show ?case
proof (rule rec(4))
fix v' g'
assume "v' ∈ Keys (set (snd ?n))" and "v' ∉ set (fst ?n)" and "g' ∈ set gs" and "lt g' adds⇩t v'"
from this(1) Keys_snd_sym_preproc_addnew have "v' ∈ Keys (set fs) ∪ insert v (set (fst ?n))"
by blast
with ‹v' ∉ set (fst ?n)› have disj: "v' ∈ Keys (set fs) ∨ v' = v" by blast
show "monom_mult 1 (pp_of_term v' - lp g') g' ∈ set (snd ?n)"
proof (cases "v' = v")
case True
from ‹g' ∈ set gs› ‹lt g' adds⇩t v'› show ?thesis
unfolding True by (rule sym_preproc_addnew_complete)
next
case False
with disj have "v' ∈ Keys (set fs)" by simp
moreover have "v' ∉ set vs"
proof
assume "v' ∈ set vs"
hence "v' ∈ set vs'" using False by (simp add: rec(3))
with fst_sym_preproc_addnew_superset have "v' ∈ set (fst ?n)" ..
with ‹v' ∉ set (fst ?n)› show False ..
qed
ultimately have "monom_mult 1 (pp_of_term v' - lp g') g' ∈ set fs"
using ‹g' ∈ set gs› ‹lt g' adds⇩t v'› by (rule rec(5))
with snd_sym_preproc_addnew_superset show ?thesis ..
qed
qed
qed
definition sym_preproc :: "('t ⇒⇩0 'b::semiring_1) list ⇒ ('t ⇒⇩0 'b) list ⇒ ('t list × ('t ⇒⇩0 'b) list)"
where "sym_preproc gs fs = sym_preproc_aux gs [] (Keys_to_list fs, fs)"
lemma sym_preproc_Nil [simp]: "sym_preproc gs [] = ([], [])"
by (simp add: sym_preproc_def)
lemma fst_sym_preproc:
"fst (sym_preproc gs fs) = Keys_to_list (snd (sym_preproc gs (fs::('t ⇒⇩0 'b::semiring_1_no_zero_divisors) list)))"
proof -
let ?a = "fst (sym_preproc gs fs)"
let ?b = "Keys_to_list (snd (sym_preproc gs fs))"
have "antisymp (≻⇩t)" unfolding antisymp_def by fastforce
have "irreflp (≻⇩t)" by (simp add: irreflp_def)
moreover have "transp (≻⇩t)" unfolding transp_def by fastforce
moreover have s1: "sorted_wrt (≻⇩t) ?a" unfolding sym_preproc_def
by (rule fst_sym_preproc_aux_sorted_wrt, simp_all)
ultimately have d1: "distinct ?a" by (rule distinct_sorted_wrt_irrefl)
have s2: "sorted_wrt (≻⇩t) ?b" by (fact Keys_to_list_sorted_wrt)
with ‹irreflp (≻⇩t)› ‹transp (≻⇩t)› have d2: "distinct ?b" by (rule distinct_sorted_wrt_irrefl)
from ‹antisymp (≻⇩t)› s1 d1 s2 d2 show ?thesis
proof (rule sorted_wrt_distinct_set_unique)
show "set ?a = set ?b" unfolding set_Keys_to_list sym_preproc_def
by (rule fst_sym_preproc_aux_complete, simp add: set_Keys_to_list)
qed
qed
lemma snd_sym_preproc_superset: "set fs ⊆ set (snd (sym_preproc gs fs))"
by (simp only: sym_preproc_def snd_conv, fact snd_sym_preproc_aux_superset)
lemma in_snd_sym_preprocE:
assumes "p ∈ set (snd (sym_preproc gs fs))"
assumes 1: "p ∈ set fs ⟹ thesis"
assumes 2: "⋀g t. g ∈ set gs ⟹ p = monom_mult 1 t g ⟹ thesis"
shows thesis
using assms unfolding sym_preproc_def snd_conv by (rule in_snd_sym_preproc_auxE)
lemma snd_sym_preproc_pmdl: "pmdl (set gs ∪ set (snd (sym_preproc gs fs))) = pmdl (set gs ∪ set fs)"
unfolding sym_preproc_def snd_conv by (fact snd_sym_preproc_aux_pmdl)
lemma snd_sym_preproc_dgrad_set_le:
assumes "dickson_grading d"
shows "dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc gs fs))))
(pp_of_term ` Keys (set gs ∪ set (fs::('t ⇒⇩0 'b::semiring_1_no_zero_divisors) list)))"
unfolding sym_preproc_def snd_conv using assms
proof (rule snd_sym_preproc_aux_dgrad_set_le)
show "set (Keys_to_list fs) ⊆ Keys (set fs)" by (simp add: set_Keys_to_list)
qed
corollary snd_sym_preproc_dgrad_p_set_le:
assumes "dickson_grading d"
shows "dgrad_p_set_le d (set (snd (sym_preproc gs fs))) (set gs ∪ set (fs::('t ⇒⇩0 'b::semiring_1_no_zero_divisors) list))"
unfolding dgrad_p_set_le_def
proof -
from assms show "dgrad_set_le d (pp_of_term ` Keys (set (snd (sym_preproc gs fs)))) (pp_of_term ` Keys (set gs ∪ set fs))"
by (rule snd_sym_preproc_dgrad_set_le)
qed
lemma components_snd_sym_preproc_subset:
"component_of_term ` Keys (set (snd (sym_preproc gs fs))) ⊆
component_of_term ` Keys (set gs ∪ set (fs::('t ⇒⇩0 'b::semiring_1_no_zero_divisors) list))"
unfolding sym_preproc_def snd_conv
by (rule components_snd_sym_preproc_aux_subset, simp add: set_Keys_to_list)
lemma snd_sym_preproc_complete:
assumes "v ∈ Keys (set (snd (sym_preproc gs fs)))" and "g ∈ set gs" and "lt g adds⇩t v"
shows "monom_mult (1::'b::semiring_1_no_zero_divisors) (pp_of_term v - lp g) g ∈ set (snd (sym_preproc gs fs))"
using _ assms unfolding sym_preproc_def snd_conv
proof (rule snd_sym_preproc_aux_complete)
fix u' and g'::"'t ⇒⇩0 'b"
assume "u' ∈ Keys (set fs)" and "u' ∉ set (Keys_to_list fs)"
thus "monom_mult 1 (pp_of_term u' - lp g') g' ∈ set fs" by (simp add: set_Keys_to_list)
qed
end
subsection ‹‹lin_red››
context ordered_term
begin
definition lin_red :: "('t ⇒⇩0 'b::field) set ⇒ ('t ⇒⇩0 'b) ⇒ ('t ⇒⇩0 'b) ⇒ bool"
where "lin_red F p q ≡ (∃f∈F. red_single p q f 0)"
text ‹@{const lin_red} is a restriction of @{const red}, where the reductor (‹f›) may only be
multiplied by a constant factor, i.\,e. where the power-product is ‹0›.›
lemma lin_redI:
assumes "f ∈ F" and "red_single p q f 0"
shows "lin_red F p q"
unfolding lin_red_def using assms ..
lemma lin_redE:
assumes "lin_red F p q"
obtains f::"'t ⇒⇩0 'b::field" where "f ∈ F" and "red_single p q f 0"
proof -
from assms obtain f where "f ∈ F" and t: "red_single p q f 0" unfolding lin_red_def by blast
thus "?thesis" ..
qed
lemma lin_red_imp_red:
assumes "lin_red F p q"
shows "red F p q"
proof -
from assms obtain f where "f ∈ F" and "red_single p q f 0" by (rule lin_redE)
thus ?thesis by (rule red_setI)
qed
lemma lin_red_Un: "lin_red (F ∪ G) p q = (lin_red F p q ∨ lin_red G p q)"
proof
assume "lin_red (F ∪ G) p q"
then obtain f where "f ∈ F ∪ G" and r: "red_single p q f 0" by (rule lin_redE)
from this(1) show "lin_red F p q ∨ lin_red G p q"
proof
assume "f ∈ F"
from this r have "lin_red F p q" by (rule lin_redI)
thus ?thesis ..
next
assume "f ∈ G"
from this r have "lin_red G p q" by (rule lin_redI)
thus ?thesis ..
qed
next
assume "lin_red F p q ∨ lin_red G p q"
thus "lin_red (F ∪ G) p q"
proof
assume "lin_red F p q"
then obtain f where "f ∈ F" and r: "red_single p q f 0" by (rule lin_redE)
from this(1) have "f ∈ F ∪ G" by simp
from this r show ?thesis by (rule lin_redI)
next
assume "lin_red G p q"
then obtain g where "g ∈ G" and r: "red_single p q g 0" by (rule lin_redE)
from this(1) have "g ∈ F ∪ G" by simp
from this r show ?thesis by (rule lin_redI)
qed
qed
lemma lin_red_imp_red_rtrancl:
assumes "(lin_red F)⇧*⇧* p q"
shows "(red F)⇧*⇧* p q"
using assms
proof induct
case base
show ?case ..
next
case (step y z)
from step(2) have "red F y z" by (rule lin_red_imp_red)
with step(3) show ?case ..
qed
lemma phull_closed_lin_red:
assumes "phull B ⊆ phull A" and "p ∈ phull A" and "lin_red B p q"
shows "q ∈ phull A"
proof -
from assms(3) obtain f where "f ∈ B" and "red_single p q f 0" by (rule lin_redE)
hence q: "q = p - (lookup p (lt f) / lc f) ⋅ f"
by (simp add: red_single_def term_simps map_scale_eq_monom_mult)
have "q - p ∈ phull B"
by (simp add: q, rule phull.span_neg, rule phull.span_scale, rule phull.span_base, fact ‹f ∈ B›)
with assms(1) have "q - p ∈ phull A" ..
from this assms(2) have "(q - p) + p ∈ phull A" by (rule phull.span_add)
thus ?thesis by simp
qed
subsection ‹Reduction›
definition Macaulay_red :: "'t list ⇒ ('t ⇒⇩0 'b) list ⇒ ('t ⇒⇩0 'b::field) list"
where "Macaulay_red vs fs =
(let lts = map lt (filter (λp. p ≠ 0) fs) in
filter (λp. p ≠ 0 ∧ lt p ∉ set lts) (mat_to_polys vs (row_echelon (polys_to_mat vs fs)))
)"
text ‹‹Macaulay_red vs fs› auto-reduces (w.\,r.\,t. @{const lin_red}) the given list ‹fs› and returns
those non-zero polynomials whose leading terms are not in ‹lt_set (set fs)›.
Argument ‹vs› is expected to be ‹Keys_to_list fs›; this list is passed as an argument
to @{const Macaulay_red}, because it can be efficiently computed by symbolic preprocessing.›
lemma Macaulay_red_alt:
"Macaulay_red (Keys_to_list fs) fs = filter (λp. lt p ∉ lt_set (set fs)) (Macaulay_list fs)"
proof -
have "{x ∈ set fs. x ≠ 0} = set fs - {0}" by blast
thus ?thesis by (simp add: Macaulay_red_def Macaulay_list_def Macaulay_mat_def lt_set_def Let_def)
qed
lemma set_Macaulay_red:
"set (Macaulay_red (Keys_to_list fs) fs) = set (Macaulay_list fs) - {p. lt p ∈ lt_set (set fs)}"
by (auto simp add: Macaulay_red_alt)
lemma Keys_Macaulay_red: "Keys (set (Macaulay_red (Keys_to_list fs) fs)) ⊆ Keys (set fs)"
proof -
have "Keys (set (Macaulay_red (Keys_to_list fs) fs)) ⊆ Keys (set (Macaulay_list fs))"
unfolding set_Macaulay_red by (fact Keys_minus)
also have "... ⊆ Keys (set fs)" by (fact Keys_Macaulay_list)
finally show ?thesis .
qed
end
context gd_term
begin
lemma Macaulay_red_reducible:
assumes "f ∈ phull (set fs)" and "F ⊆ set fs" and "lt_set F = lt_set (set fs)"
shows "(lin_red (F ∪ set (Macaulay_red (Keys_to_list fs) fs)))⇧*⇧* f 0"
proof -
define A where "A = F ∪ set (Macaulay_red (Keys_to_list fs) fs)"
have phull_A: "phull A ⊆ phull (set fs)"
proof (rule phull.span_subset_spanI, simp add: A_def, rule)
have "F ⊆ phull F" by (rule phull.span_superset)
also from assms(2) have "... ⊆ phull (set fs)" by (rule phull.span_mono)
finally show "F ⊆ phull (set fs)" .
next
have "set (Macaulay_red (Keys_to_list fs) fs) ⊆ set (Macaulay_list fs)"
by (auto simp add: set_Macaulay_red)
also have "... ⊆ phull (set (Macaulay_list fs))" by (rule phull.span_superset)
also have "... = phull (set fs)" by (rule phull_Macaulay_list)
finally show "set (Macaulay_red (Keys_to_list fs) fs) ⊆ phull (set fs)" .
qed
have lt_A: "p ∈ phull (set fs) ⟹ p ≠ 0 ⟹ (⋀g. g ∈ A ⟹ g ≠ 0 ⟹ lt g = lt p ⟹ thesis) ⟹ thesis"
for p thesis
proof -
assume "p ∈ phull (set fs)" and "p ≠ 0"
then obtain g where g_in: "g ∈ set (Macaulay_list fs)" and "g ≠ 0" and "lt p = lt g"
by (rule Macaulay_list_lt)
assume *: "⋀g. g ∈ A ⟹ g ≠ 0 ⟹ lt g = lt p ⟹ thesis"
show ?thesis
proof (cases "g ∈ set (Macaulay_red (Keys_to_list fs) fs)")
case True
hence "g ∈ A" by (simp add: A_def)
from this ‹g ≠ 0› ‹lt p = lt g›[symmetric] show ?thesis by (rule *)
next
case False
with g_in have "lt g ∈ lt_set (set fs)" by (simp add: set_Macaulay_red)
also have "... = lt_set F" by (simp only: assms(3))
finally obtain g' where "g' ∈ F" and "g' ≠ 0" and "lt g' = lt g" by (rule lt_setE)
from this(1) have "g' ∈ A" by (simp add: A_def)
moreover note ‹g' ≠ 0›
moreover have "lt g' = lt p" by (simp only: ‹lt p = lt g› ‹lt g' = lt g›)
ultimately show ?thesis by (rule *)
qed
qed
from assms(2) finite_set have "finite F" by (rule finite_subset)
from this finite_set have fin_A: "finite A" unfolding A_def by (rule finite_UnI)
from ex_dgrad obtain d::"'a ⇒ nat" where dg: "dickson_grading d" ..
from fin_A have "finite (insert f A)" ..
then obtain m where "insert f A ⊆ dgrad_p_set d m" by (rule dgrad_p_set_exhaust)
hence A_sub: "A ⊆ dgrad_p_set d m" and "f ∈ dgrad_p_set d m" by simp_all
from dg have "wfP (dickson_less_p d m)" by (rule wf_dickson_less_p)
from this assms(1) ‹f ∈ dgrad_p_set d m› show "(lin_red A)⇧*⇧* f 0"
proof (induct f)
fix p
assume IH: "⋀q. dickson_less_p d m q p ⟹ q ∈ phull (set fs) ⟹ q ∈ dgrad_p_set d m ⟹
(lin_red A)⇧*⇧* q 0"
and "p ∈ phull (set fs)" and "p ∈ dgrad_p_set d m"
show "(lin_red A)⇧*⇧* p 0"
proof (cases "p = 0")
case True
thus ?thesis by simp
next
case False
with ‹p ∈ phull (set fs)› obtain g where "g ∈ A" and "g ≠ 0" and "lt g = lt p" by (rule lt_A)
define q where "q = p - monom_mult (lc p / lc g) 0 g"
from ‹g ∈ A› have lr: "lin_red A p q"
proof (rule lin_redI)
show "red_single p q g 0"
by (simp add: red_single_def ‹lt g = lt p› lc_def[symmetric] q_def ‹g ≠ 0› lc_not_0[OF False] term_simps)
qed
moreover have "(lin_red A)⇧*⇧* q 0"
proof -
from lr have red: "red A p q" by (rule lin_red_imp_red)
with dg A_sub ‹p ∈ dgrad_p_set d m› have "q ∈ dgrad_p_set d m" by (rule dgrad_p_set_closed_red)
moreover from red have "q ≺⇩p p" by (rule red_ord)
ultimately have "dickson_less_p d m q p" using ‹p ∈ dgrad_p_set d m›
by (simp add: dickson_less_p_def)
moreover from phull_A ‹p ∈ phull (set fs)› lr have "q ∈ phull (set fs)"
by (rule phull_closed_lin_red)
ultimately show ?thesis using ‹q ∈ dgrad_p_set d m› by (rule IH)
qed
ultimately show ?thesis by fastforce
qed
qed
qed
primrec pdata_pairs_to_list :: "('t, 'b::field, 'c) pdata_pair list ⇒ ('t ⇒⇩0 'b) list" where
"pdata_pairs_to_list [] = []"|
"pdata_pairs_to_list (p # ps) =
(let f = fst (fst p); g = fst (snd p); lf = lp f; lg = lp g; l = lcs lf lg in
(monom_mult (1 / lc f) (l - lf) f) # (monom_mult (1 / lc g) (l - lg) g) #
(pdata_pairs_to_list ps)
)"
lemma in_pdata_pairs_to_listI1:
assumes "(f, g) ∈ set ps"
shows "monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f)))
(fst f) ∈ set (pdata_pairs_to_list ps)" (is "?m ∈ _")
using assms
proof (induct ps)
case Nil
thus ?case by simp
next
case (Cons p ps)
from Cons(2) have "p = (f, g) ∨ (f, g) ∈ set ps" by auto
thus ?case
proof
assume "p = (f, g)"
show ?thesis by (simp add: ‹p = (f, g)› Let_def)
next
assume "(f, g) ∈ set ps"
hence "?m ∈ set (pdata_pairs_to_list ps)" by (rule Cons(1))
thus ?thesis by (simp add: Let_def)
qed
qed
lemma in_pdata_pairs_to_listI2:
assumes "(f, g) ∈ set ps"
shows "monom_mult (1 / lc (fst g)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst g)))
(fst g) ∈ set (pdata_pairs_to_list ps)" (is "?m ∈ _")
using assms
proof (induct ps)
case Nil
thus ?case by simp
next
case (Cons p ps)
from Cons(2) have "p = (f, g) ∨ (f, g) ∈ set ps" by auto
thus ?case
proof
assume "p = (f, g)"
show ?thesis by (simp add: ‹p = (f, g)› Let_def)
next
assume "(f, g) ∈ set ps"
hence "?m ∈ set (pdata_pairs_to_list ps)" by (rule Cons(1))
thus ?thesis by (simp add: Let_def)
qed
qed
lemma in_pdata_pairs_to_listE:
assumes "h ∈ set (pdata_pairs_to_list ps)"
obtains f g where "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
and "h = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
using assms
proof (induct ps arbitrary: thesis)
case Nil
from Nil(2) show ?case by simp
next
case (Cons p ps)
let ?f = "fst (fst p)"
let ?g = "fst (snd p)"
let ?lf = "lp ?f"
let ?lg = "lp ?g"
let ?l = "lcs ?lf ?lg"
from Cons(3) have "h = monom_mult (1 / lc ?f) (?l - ?lf) ?f ∨ h = monom_mult (1 / lc ?g) (?l - ?lg) ?g ∨
h ∈ set (pdata_pairs_to_list ps)"
by (simp add: Let_def)
thus ?case
proof (elim disjE)
assume h: "h = monom_mult (1 / lc ?f) (?l - ?lf) ?f"
have "(fst p, snd p) ∈ set (p # ps)" by simp
hence "(fst p, snd p) ∈ set (p # ps) ∨ (snd p, fst p) ∈ set (p # ps)" ..
from this h show ?thesis by (rule Cons(2))
next
assume h: "h = monom_mult (1 / lc ?g) (?l - ?lg) ?g"
have "(fst p, snd p) ∈ set (p # ps)" by simp
hence "(snd p, fst p) ∈ set (p # ps) ∨ (fst p, snd p) ∈ set (p # ps)" ..
moreover from h have "h = monom_mult (1 / lc ?g) ((lcs ?lg ?lf) - ?lg) ?g"
by (simp only: lcs_comm)
ultimately show ?thesis by (rule Cons(2))
next
assume h_in: "h ∈ set (pdata_pairs_to_list ps)"
obtain f g where "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
and h: "h = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
by (rule Cons(1), assumption, intro h_in)
from this(1) have "(f, g) ∈ set (p # ps) ∨ (g, f) ∈ set (p # ps)" by auto
from this h show ?thesis by (rule Cons(2))
qed
qed
definition f4_red_aux :: "('t, 'b::field, 'c) pdata list ⇒ ('t, 'b, 'c) pdata_pair list ⇒
('t ⇒⇩0 'b) list"
where "f4_red_aux bs ps =
(let aux = sym_preproc (map fst bs) (pdata_pairs_to_list ps) in Macaulay_red (fst aux) (snd aux))"
text ‹@{const f4_red_aux} only takes two arguments, since it does not distinguish between those
elements of the current basis that are known to be a Gr\"obner basis (called ‹gs› in
@{theory Groebner_Bases.Algorithm_Schema}) and the remaining ones.›
lemma f4_red_aux_not_zero: "0 ∉ set (f4_red_aux bs ps)"
by (simp add: f4_red_aux_def Let_def fst_sym_preproc set_Macaulay_red set_Macaulay_list)
lemma f4_red_aux_irredudible:
assumes "h ∈ set (f4_red_aux bs ps)" and "b ∈ set bs" and "fst b ≠ 0"
shows "¬ lt (fst b) adds⇩t lt h"
proof
from assms(1) f4_red_aux_not_zero have "h ≠ 0" by metis
hence "lt h ∈ keys h" by (rule lt_in_keys)
also from assms(1) have "... ⊆ Keys (set (f4_red_aux bs ps))" by (rule keys_subset_Keys)
also have "... ⊆ Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
(is "_ ⊆ Keys (set ?s)") by (simp only: f4_red_aux_def Let_def fst_sym_preproc Keys_Macaulay_red)
finally have "lt h ∈ Keys (set ?s)" .
moreover from assms(2) have "fst b ∈ set (map fst bs)" by auto
moreover assume a: "lt (fst b) adds⇩t lt h"
ultimately have "monom_mult 1 (lp h - lp (fst b)) (fst b) ∈ set ?s" (is "?m ∈ _")
by (rule snd_sym_preproc_complete)
from assms(3) have "?m ≠ 0" by (simp add: monom_mult_eq_zero_iff)
with ‹?m ∈ set ?s› have "lt ?m ∈ lt_set (set ?s)" by (rule lt_setI)
moreover from assms(3) a have "lt ?m = lt h"
by (simp add: lt_monom_mult, metis add_diff_cancel_right' adds_termE pp_of_term_splus)
ultimately have "lt h ∈ lt_set (set ?s)" by simp
moreover from assms(1) have "lt h ∉ lt_set (set ?s)"
by (simp add: f4_red_aux_def Let_def fst_sym_preproc set_Macaulay_red)
ultimately show False by simp
qed
lemma f4_red_aux_dgrad_p_set_le:
assumes "dickson_grading d"
shows "dgrad_p_set_le d (set (f4_red_aux bs ps)) (args_to_set ([], bs, ps))"
unfolding dgrad_p_set_le_def dgrad_set_le_def
proof
fix s
assume "s ∈ pp_of_term ` Keys (set (f4_red_aux bs ps))"
also have "... ⊆ pp_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
(is "_ ⊆ pp_of_term ` Keys (set ?s)")
by (rule image_mono, simp only: f4_red_aux_def Let_def fst_sym_preproc Keys_Macaulay_red)
finally have "s ∈ pp_of_term ` Keys (set ?s)" .
with snd_sym_preproc_dgrad_set_le[OF assms] obtain t
where "t ∈ pp_of_term ` Keys (set (map fst bs) ∪ set (pdata_pairs_to_list ps))" and "d s ≤ d t"
by (rule dgrad_set_leE)
from this(1) have "t ∈ pp_of_term ` Keys (fst ` set bs) ∨ t ∈ pp_of_term ` Keys (set (pdata_pairs_to_list ps))"
by (simp add: Keys_Un image_Un)
thus "∃t ∈ pp_of_term ` Keys (args_to_set ([], bs, ps)). d s ≤ d t"
proof
assume "t ∈ pp_of_term ` Keys (fst ` set bs)"
also have "... ⊆ pp_of_term ` Keys (args_to_set ([], bs, ps))"
by (rule image_mono, rule Keys_mono, auto simp add: args_to_set_alt)
finally have "t ∈ pp_of_term ` Keys (args_to_set ([], bs, ps))" .
with ‹d s ≤ d t› show ?thesis ..
next
assume "t ∈ pp_of_term ` Keys (set (pdata_pairs_to_list ps))"
then obtain p where "p ∈ set (pdata_pairs_to_list ps)" and "t ∈ pp_of_term ` keys p"
by (auto elim: in_KeysE)
from this(1) obtain f g where disj: "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
and p: "p = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
by (rule in_pdata_pairs_to_listE)
from disj have "fst f ∈ args_to_set ([], bs, ps) ∧ fst g ∈ args_to_set ([], bs, ps)"
proof
assume "(f, g) ∈ set ps"
hence "f ∈ fst ` set ps" and "g ∈ snd ` set ps" by force+
hence "fst f ∈ fst ` fst ` set ps" and "fst g ∈ fst ` snd ` set ps" by simp_all
thus ?thesis by (simp add: args_to_set_def image_Un)
next
assume "(g, f) ∈ set ps"
hence "f ∈ snd ` set ps" and "g ∈ fst ` set ps" by force+
hence "fst f ∈ fst ` snd ` set ps" and "fst g ∈ fst ` fst ` set ps" by simp_all
thus ?thesis by (simp add: args_to_set_def image_Un)
qed
hence "fst f ∈ args_to_set ([], bs, ps)" and "fst g ∈ args_to_set ([], bs, ps)" by simp_all
hence keys_f: "keys (fst f) ⊆ Keys (args_to_set ([], bs, ps))"
and keys_g: "keys (fst g) ⊆ Keys (args_to_set ([], bs, ps))"
by (auto intro!: keys_subset_Keys)
let ?lf = "lp (fst f)"
let ?lg = "lp (fst g)"
define l where "l = lcs ?lf ?lg"
have "pp_of_term ` keys p ⊆ pp_of_term ` ((⊕) (lcs ?lf ?lg - ?lf) ` keys (fst f))" unfolding p
using keys_monom_mult_subset by (rule image_mono)
with ‹t ∈ pp_of_term ` keys p› have "t ∈ pp_of_term ` ((⊕) (l - ?lf) ` keys (fst f))" unfolding l_def ..
then obtain t' where "t' ∈ pp_of_term ` keys (fst f)" and t: "t = (l - ?lf) + t'"
using pp_of_term_splus by fastforce
from this(1) have "fst f ≠ 0" by auto
show ?thesis
proof (cases "fst g = 0")
case True
hence "?lg = 0" by (simp add: lt_def min_term_def term_simps)
hence "l = ?lf" by (simp add: l_def lcs_zero lcs_comm)
hence "t = t'" by (simp add: t)
with ‹d s ≤ d t› have "d s ≤ d t'" by simp
moreover from ‹t' ∈ pp_of_term ` keys (fst f)› keys_f have "t' ∈ pp_of_term ` Keys (args_to_set ([], bs, ps))"
by blast
ultimately show ?thesis ..
next
case False
have "d t = d (l - ?lf) ∨ d t = d t'"
by (auto simp add: t dickson_gradingD1[OF assms])
thus ?thesis
proof
assume "d t = d (l - ?lf)"
also from assms have "... ≤ ord_class.max (d ?lf) (d ?lg)"
unfolding l_def by (rule dickson_grading_lcs_minus)
finally have "d s ≤ d ?lf ∨ d s ≤ d ?lg" using ‹d s ≤ d t› by auto
thus ?thesis
proof
assume "d s ≤ d ?lf"
moreover have "lt (fst f) ∈ Keys (args_to_set ([], bs, ps))"
by (rule, rule lt_in_keys, fact+)
ultimately show ?thesis by blast
next
assume "d s ≤ d ?lg"
moreover have "lt (fst g) ∈ Keys (args_to_set ([], bs, ps))"
by (rule, rule lt_in_keys, fact+)
ultimately show ?thesis by blast
qed
next
assume "d t = d t'"
with ‹d s ≤ d t› have "d s ≤ d t'" by simp
moreover from ‹t' ∈ pp_of_term ` keys (fst f)› keys_f have "t' ∈ pp_of_term ` Keys (args_to_set ([], bs, ps))"
by blast
ultimately show ?thesis ..
qed
qed
qed
qed
lemma components_f4_red_aux_subset:
"component_of_term ` Keys (set (f4_red_aux bs ps)) ⊆ component_of_term ` Keys (args_to_set ([], bs, ps))"
proof
fix k
assume "k ∈ component_of_term ` Keys (set (f4_red_aux bs ps))"
also have "... ⊆ component_of_term ` Keys (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
by (rule image_mono, simp only: f4_red_aux_def Let_def fst_sym_preproc Keys_Macaulay_red)
also have "... ⊆ component_of_term ` Keys (set (map fst bs) ∪ set (pdata_pairs_to_list ps))"
by (fact components_snd_sym_preproc_subset)
finally have "k ∈ component_of_term ` Keys (fst ` set bs) ∪ component_of_term ` Keys (set (pdata_pairs_to_list ps))"
by (simp add: image_Un Keys_Un)
thus "k ∈ component_of_term ` Keys (args_to_set ([], bs, ps))"
proof
assume "k ∈ component_of_term ` Keys (fst ` set bs)"
also have "... ⊆ component_of_term ` Keys (args_to_set ([], bs, ps))"
by (rule image_mono, rule Keys_mono, auto simp add: args_to_set_alt)
finally show "k ∈ component_of_term ` Keys (args_to_set ([], bs, ps))" .
next
assume "k ∈ component_of_term ` Keys (set (pdata_pairs_to_list ps))"
then obtain p where "p ∈ set (pdata_pairs_to_list ps)" and "k ∈ component_of_term ` keys p"
by (auto elim: in_KeysE)
from this(1) obtain f g where disj: "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
and p: "p = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
by (rule in_pdata_pairs_to_listE)
from disj have "fst f ∈ args_to_set ([], bs, ps)"
by (simp add: args_to_set_alt, metis fst_conv image_eqI snd_conv)
hence "fst f ∈ args_to_set ([], bs, ps)" by simp
hence keys_f: "keys (fst f) ⊆ Keys (args_to_set ([], bs, ps))"
by (auto intro!: keys_subset_Keys)
let ?lf = "lp (fst f)"
let ?lg = "lp (fst g)"
define l where "l = lcs ?lf ?lg"
have "component_of_term ` keys p ⊆ component_of_term ` ((⊕) (lcs ?lf ?lg - ?lf) ` keys (fst f))"
unfolding p using keys_monom_mult_subset by (rule image_mono)
with ‹k ∈ component_of_term ` keys p› have "k ∈ component_of_term ` ((⊕) (l - ?lf) ` keys (fst f))"
unfolding l_def ..
hence "k ∈ component_of_term ` keys (fst f)" using component_of_term_splus by fastforce
with keys_f show "k ∈ component_of_term ` Keys (args_to_set ([], bs, ps))" by blast
qed
qed
lemma pmdl_f4_red_aux: "set (f4_red_aux bs ps) ⊆ pmdl (args_to_set ([], bs, ps))"
proof -
have "set (f4_red_aux bs ps) ⊆
set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
by (auto simp add: f4_red_aux_def Let_def fst_sym_preproc set_Macaulay_red)
also have "... ⊆ pmdl (set (Macaulay_list (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps)))))"
by (fact pmdl.span_superset)
also have "... = pmdl (set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
by (fact pmdl_Macaulay_list)
also have "... ⊆ pmdl (set (map fst bs) ∪
set (snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))))"
by (rule pmdl.span_mono, blast)
also have "... = pmdl (set (map fst bs) ∪ set (pdata_pairs_to_list ps))"
by (fact snd_sym_preproc_pmdl)
also have "... ⊆ pmdl (args_to_set ([], bs, ps))"
proof (rule pmdl.span_subset_spanI, simp only: Un_subset_iff, rule conjI)
have "set (map fst bs) ⊆ args_to_set ([], bs, ps)" by (auto simp add: args_to_set_def)
also have "... ⊆ pmdl (args_to_set ([], bs, ps))" by (rule pmdl.span_superset)
finally show "set (map fst bs) ⊆ pmdl (args_to_set ([], bs, ps))" .
next
show "set (pdata_pairs_to_list ps) ⊆ pmdl (args_to_set ([], bs, ps))"
proof
fix p
assume "p ∈ set (pdata_pairs_to_list ps)"
then obtain f g where "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
and p: "p = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
by (rule in_pdata_pairs_to_listE)
from this(1) have "f ∈ fst ` set ps ∪ snd ` set ps" by force
hence "fst f ∈ args_to_set ([], bs, ps)" by (auto simp add: args_to_set_alt)
hence "fst f ∈ pmdl (args_to_set ([], bs, ps))" by (rule pmdl.span_base)
thus "p ∈ pmdl (args_to_set ([], bs, ps))" unfolding p by (rule pmdl_closed_monom_mult)
qed
qed
finally show ?thesis .
qed
lemma f4_red_aux_phull_reducible:
assumes "set ps ⊆ set bs × set bs"
and "f ∈ phull (set (pdata_pairs_to_list ps))"
shows "(red (fst ` set bs ∪ set (f4_red_aux bs ps)))⇧*⇧* f 0"
proof -
define fs where "fs = snd (sym_preproc (map fst bs) (pdata_pairs_to_list ps))"
have "set (pdata_pairs_to_list ps) ⊆ set fs" unfolding fs_def by (fact snd_sym_preproc_superset)
hence "phull (set (pdata_pairs_to_list ps)) ⊆ phull (set fs)" by (rule phull.span_mono)
with assms(2) have f_in: "f ∈ phull (set fs)" ..
have eq: "(set fs) ∪ set (f4_red_aux bs ps) = (set fs) ∪ set (Macaulay_red (Keys_to_list fs) fs)"
by (simp add: f4_red_aux_def fs_def Let_def fst_sym_preproc)
have "(lin_red ((set fs) ∪ set (f4_red_aux bs ps)))⇧*⇧* f 0"
by (simp only: eq, rule Macaulay_red_reducible, fact f_in, fact subset_refl, fact refl)
thus ?thesis
proof induct
case base
show ?case ..
next
case (step y z)
from step(2) have "red (fst ` set bs ∪ set (f4_red_aux bs ps)) y z" unfolding lin_red_Un
proof
assume "lin_red (set fs) y z"
then obtain a where "a ∈ set fs" and r: "red_single y z a 0" by (rule lin_redE)
from this(1) obtain b c t where "b ∈ fst ` set bs" and a: "a = monom_mult c t b" unfolding fs_def
proof (rule in_snd_sym_preprocE)
assume *: "⋀b c t. b ∈ fst ` set bs ⟹ a = monom_mult c t b ⟹ thesis"
assume "a ∈ set (pdata_pairs_to_list ps)"
then obtain f g where "(f, g) ∈ set ps ∨ (g, f) ∈ set ps"
and a: "a = monom_mult (1 / lc (fst f)) ((lcs (lp (fst f)) (lp (fst g))) - (lp (fst f))) (fst f)"
by (rule in_pdata_pairs_to_listE)
from this(1) have "f ∈ fst ` set ps ∪ snd ` set ps" by force
with assms(1) have "f ∈ set bs" by fastforce
hence "fst f ∈ fst ` set bs" by simp
from this a show ?thesis by (rule *)
next
fix g s
assume *: "⋀b c t. b ∈ fst ` set bs ⟹ a = monom_mult c t b ⟹ thesis"
assume "g ∈ set (map fst bs)"
hence "g ∈ fst ` set bs" by simp
moreover assume "a = monom_mult 1 s g"
ultimately show ?thesis by (rule *)
qed
from r have "c ≠ 0" and "b ≠ 0" by (simp_all add: a red_single_def monom_mult_eq_zero_iff)
from r have "red_single y z b t"
by (simp add: a red_single_def monom_mult_eq_zero_iff lt_monom_mult[OF ‹c ≠ 0› ‹b ≠ 0›]
monom_mult_assoc term_simps)
with ‹b ∈ fst ` set bs› have "red (fst ` set bs) y z" by (rule red_setI)
thus ?thesis by (rule red_unionI1)
next
assume "lin_red (set (f4_red_aux bs ps)) y z"
hence "red (set (f4_red_aux bs ps)) y z" by (rule lin_red_imp_red)
thus ?thesis by (rule red_unionI2)
qed
with step(3) show ?case ..
qed
qed
corollary f4_red_aux_spoly_reducible:
assumes "set ps ⊆ set bs × set bs" and "(p, q) ∈ set ps"
shows "(red (fst ` set bs ∪ set (f4_red_aux bs ps)))⇧*⇧* (spoly (fst p) (fst q)) 0"
using assms(1)
proof (rule f4_red_aux_phull_reducible)
let ?lt = "lp (fst p)"
let ?lq = "lp (fst q)"
let ?l = "lcs ?lt ?lq"
let ?p = "monom_mult (1 / lc (fst p)) (?l - ?lt) (fst p)"
let ?q = "monom_mult (1 / lc (fst q)) (?l - ?lq) (fst q)"
from assms(2) have "?p ∈ set (pdata_pairs_to_list ps)" and "?q ∈ set (pdata_pairs_to_list ps)"
by (rule in_pdata_pairs_to_listI1, rule in_pdata_pairs_to_listI2)
hence "?p ∈ phull (set (pdata_pairs_to_list ps))" and "?q ∈ phull (set (pdata_pairs_to_list ps))"
by (auto intro: phull.span_base)
hence "?p - ?q ∈ phull (set (pdata_pairs_to_list ps))" by (rule phull.span_diff)
thus "spoly (fst p) (fst q) ∈ phull (set (pdata_pairs_to_list ps))"
by (simp add: spoly_def Let_def phull.span_zero lc_def split: if_split)
qed
definition f4_red :: "('t, 'b::field, 'c::default, 'd) complT"
where "f4_red gs bs ps sps data = (map (λh. (h, default)) (f4_red_aux (gs @ bs) sps), snd data)"
lemma fst_set_fst_f4_red: "fst ` set (fst (f4_red gs bs ps sps data)) = set (f4_red_aux (gs @ bs) sps)"
by (simp add: f4_red_def, force)
lemma rcp_spec_f4_red: "rcp_spec f4_red"
proof (rule rcp_specI)
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat × 'd"
show "0 ∉ fst ` set (fst (f4_red gs bs ps sps data))"
by (simp add: fst_set_fst_f4_red f4_red_aux_not_zero)
next
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps h b and data::"nat × 'd"
assume "h ∈ set (fst (f4_red gs bs ps sps data))" and "b ∈ set gs ∪ set bs"
from this(1) have "fst h ∈ fst ` set (fst (f4_red gs bs ps sps data))" by simp
hence "fst h ∈ set (f4_red_aux (gs @ bs) sps)" by (simp only: fst_set_fst_f4_red)
moreover from ‹b ∈ set gs ∪ set bs› have "b ∈ set (gs @ bs)" by simp
moreover assume "fst b ≠ 0"
ultimately show "¬ lt (fst b) adds⇩t lt (fst h)" by (rule f4_red_aux_irredudible)
next
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and d::"'a ⇒ nat" and data::"nat × 'd"
assume "dickson_grading d"
hence "dgrad_p_set_le d (set (f4_red_aux (gs @ bs) sps)) (args_to_set ([], gs @ bs, sps))"
by (fact f4_red_aux_dgrad_p_set_le)
also have "... = args_to_set (gs, bs, sps)" by (simp add: args_to_set_alt image_Un)
finally show "dgrad_p_set_le d (fst ` set (fst (f4_red gs bs ps sps data))) (args_to_set (gs, bs, sps))"
by (simp only: fst_set_fst_f4_red)
next
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat × 'd"
have "component_of_term ` Keys (set (f4_red_aux (gs @ bs) sps)) ⊆
component_of_term ` Keys (args_to_set ([], gs @ bs, sps))"
by (fact components_f4_red_aux_subset)
also have "... = component_of_term ` Keys (args_to_set (gs, bs, sps))"
by (simp add: args_to_set_alt image_Un)
finally show "component_of_term ` Keys (fst ` set (fst (f4_red gs bs ps sps data))) ⊆
component_of_term ` Keys (args_to_set (gs, bs, sps))"
by (simp only: fst_set_fst_f4_red)
next
fix gs bs::"('t, 'b, 'c) pdata list" and ps sps and data::"nat × 'd"
have "set (f4_red_aux (gs @ bs) sps) ⊆ pmdl (args_to_set ([], gs @ bs, sps))"
by (fact pmdl_f4_red_aux)
also have "... = pmdl (args_to_set (gs, bs, sps))" by (simp add: args_to_set_alt image_Un)
finally have "fst ` set (fst (f4_red gs bs ps sps data)) ⊆ pmdl (args_to_set (gs, bs, sps))"
by (simp only: fst_set_fst_f4_red)
moreover {
fix p q :: "('t, 'b, 'c) pdata"
assume "set sps ⊆ set bs × (set gs ∪ set bs)"
hence "set sps ⊆ set (gs @ bs) × set (gs @ bs)" by fastforce
moreover assume "(p, q) ∈ set sps"
ultimately have "(red (fst ` set (gs @ bs) ∪ set (f4_red_aux (gs @ bs) sps)))⇧*⇧* (spoly (fst p) (fst q)) 0"
by (rule f4_red_aux_spoly_reducible)
}
ultimately show
"fst ` set (fst (f4_red gs bs ps sps data)) ⊆ pmdl (args_to_set (gs, bs, sps)) ∧
(∀(p, q)∈set sps.
set sps ⊆ set bs × (set gs ∪ set bs) ⟶
(red (fst ` (set gs ∪ set bs) ∪ fst ` set (fst (f4_red gs bs ps sps data))))⇧*⇧* (spoly (fst p) (fst q)) 0)"
by (auto simp add: image_Un fst_set_fst_f4_red)
qed
lemmas compl_struct_f4_red = compl_struct_rcp[OF rcp_spec_f4_red]
lemmas compl_pmdl_f4_red = compl_pmdl_rcp[OF rcp_spec_f4_red]
lemmas compl_conn_f4_red = compl_conn_rcp[OF rcp_spec_f4_red]
subsection ‹Pair Selection›
primrec f4_sel_aux :: "'a ⇒ ('t, 'b::zero, 'c) pdata_pair list ⇒ ('t, 'b, 'c) pdata_pair list" where
"f4_sel_aux _ [] = []"|
"f4_sel_aux t (p # ps) =
(if (lcs (lp (fst (fst p))) (lp (fst (snd p)))) = t then
p # (f4_sel_aux t ps)
else
[]
)"
lemma f4_sel_aux_subset: "set (f4_sel_aux t ps) ⊆ set ps"
by (induct ps, auto)
primrec f4_sel :: "('t, 'b::zero, 'c, 'd) selT" where
"f4_sel gs bs [] data = []"|
"f4_sel gs bs (p # ps) data = p # (f4_sel_aux (lcs (lp (fst (fst p))) (lp (fst (snd p)))) ps)"
lemma sel_spec_f4_sel: "sel_spec f4_sel"
proof (rule sel_specI)
fix gs bs :: "('t, 'b, 'c) pdata list" and ps::"('t, 'b, 'c) pdata_pair list" and data::"nat × 'd"
assume "ps ≠ []"
then obtain p ps' where ps: "ps = p # ps'" by (meson list.exhaust)
show "f4_sel gs bs ps data ≠ [] ∧ set (f4_sel gs bs ps data) ⊆ set ps"
proof
show "f4_sel gs bs ps data ≠ []" by (simp add: ps)
next
from f4_sel_aux_subset show "set (f4_sel gs bs ps data) ⊆ set ps" by (auto simp add: ps)
qed
qed
subsection ‹The F4 Algorithm›
text ‹The F4 algorithm is just @{const gb_schema_direct} with parameters instantiated by suitable
functions.›
lemma struct_spec_f4: "struct_spec f4_sel add_pairs_canon add_basis_canon f4_red"
using sel_spec_f4_sel ap_spec_add_pairs_canon ab_spec_add_basis_sorted compl_struct_f4_red
by (rule struct_specI)
definition f4_aux :: "('t, 'b, 'c) pdata list ⇒ nat × nat × 'd ⇒ ('t, 'b, 'c) pdata list ⇒
('t, 'b, 'c) pdata_pair list ⇒ ('t, 'b::field, 'c::default) pdata list"
where "f4_aux = gb_schema_aux f4_sel add_pairs_canon add_basis_canon f4_red"
lemmas f4_aux_simps [code] = gb_schema_aux_simps[OF struct_spec_f4, folded f4_aux_def]
definition f4 :: "('t, 'b, 'c) pdata' list ⇒ 'd ⇒ ('t, 'b::field, 'c::default) pdata' list"
where "f4 = gb_schema_direct f4_sel add_pairs_canon add_basis_canon f4_red"
lemmas f4_simps [code] = gb_schema_direct_def[of f4_sel add_pairs_canon add_basis_canon f4_red, folded f4_def f4_aux_def]
lemmas f4_isGB = gb_schema_direct_isGB[OF struct_spec_f4 compl_conn_f4_red, folded f4_def]
lemmas f4_pmdl = gb_schema_direct_pmdl[OF struct_spec_f4 compl_pmdl_f4_red, folded f4_def]
subsubsection ‹Special Case: ‹punit››
lemma (in gd_term) struct_spec_f4_punit: "punit.struct_spec punit.f4_sel add_pairs_punit_canon punit.add_basis_canon punit.f4_red"
using punit.sel_spec_f4_sel ap_spec_add_pairs_punit_canon ab_spec_add_basis_sorted punit.compl_struct_f4_red
by (rule punit.struct_specI)
definition f4_aux_punit :: "('a, 'b, 'c) pdata list ⇒ nat × nat × 'd ⇒ ('a, 'b, 'c) pdata list ⇒
('a, 'b, 'c) pdata_pair list ⇒ ('a, 'b::field, 'c::default) pdata list"
where "f4_aux_punit = punit.gb_schema_aux punit.f4_sel add_pairs_punit_canon punit.add_basis_canon punit.f4_red"
lemmas f4_aux_punit_simps [code] = punit.gb_schema_aux_simps[OF struct_spec_f4_punit, folded f4_aux_punit_def]
definition f4_punit :: "('a, 'b, 'c) pdata' list ⇒ 'd ⇒ ('a, 'b::field, 'c::default) pdata' list"
where "f4_punit = punit.gb_schema_direct punit.f4_sel add_pairs_punit_canon punit.add_basis_canon punit.f4_red"
lemmas f4_punit_simps [code] = punit.gb_schema_direct_def[of "punit.f4_sel" add_pairs_punit_canon
"punit.add_basis_canon" "punit.f4_red", folded f4_punit_def f4_aux_punit_def]
lemmas f4_punit_isGB = punit.gb_schema_direct_isGB[OF struct_spec_f4_punit punit.compl_conn_f4_red, folded f4_punit_def]
lemmas f4_punit_pmdl = punit.gb_schema_direct_pmdl[OF struct_spec_f4_punit punit.compl_pmdl_f4_red, folded f4_punit_def]
end
end