Theory Algorithm_Schema
section ‹A General Algorithm Schema for Computing Gr\"obner Bases›
theory Algorithm_Schema
imports General Groebner_Bases
begin
text ‹This theory formalizes a general algorithm schema for computing Gr\"obner bases, generalizing
Buchberger's original critical-pair/completion algorithm. The algorithm schema depends on several
functional parameters that can be instantiated by a variety of concrete functions. Possible instances
yield Buchberger's algorithm, Faug\`ere's F4 algorithm, and (as far as we can tell) even his F5
algorithm.›
subsection ‹@{term processed}›
definition minus_pairs (infixl ‹-⇩p› 65) where "minus_pairs A B = A - (B ∪ prod.swap ` B)"
definition Int_pairs (infixl ‹∩⇩p› 65) where "Int_pairs A B = A ∩ (B ∪ prod.swap ` B)"
definition in_pair (infix ‹∈⇩p› 50) where "in_pair p A ⟷ (p ∈ A ∪ prod.swap ` A)"
definition subset_pairs (infix ‹⊆⇩p› 50) where "subset_pairs A B ⟷ (∀x. x ∈⇩p A ⟶ x ∈⇩p B)"
abbreviation not_in_pair (infix ‹∉⇩p› 50) where "not_in_pair p A ≡ ¬ p ∈⇩p A"
lemma in_pair_alt: "p ∈⇩p A ⟷ (p ∈ A ∨ prod.swap p ∈ A)"
by (metis (mono_tags, lifting) UnCI UnE image_iff in_pair_def prod.collapse swap_simp)
lemma in_pair_iff: "(a, b) ∈⇩p A ⟷ ((a, b) ∈ A ∨ (b, a) ∈ A)"
by (simp add: in_pair_alt)
lemma in_pair_minus_pairs [simp]: "p ∈⇩p A -⇩p B ⟷ (p ∈⇩p A ∧ p ∉⇩p B)"
by (metis Diff_iff in_pair_def in_pair_iff minus_pairs_def prod.collapse)
lemma in_minus_pairs [simp]: "p ∈ A -⇩p B ⟷ (p ∈ A ∧ p ∉⇩p B)"
by (metis Diff_iff in_pair_def minus_pairs_def)
lemma in_pair_Int_pairs [simp]: "p ∈⇩p A ∩⇩p B ⟷ (p ∈⇩p A ∧ p ∈⇩p B)"
by (metis (no_types, opaque_lifting) Int_iff Int_pairs_def in_pair_alt in_pair_def old.prod.exhaust swap_simp)
lemma in_pair_Un [simp]: "p ∈⇩p A ∪ B ⟷ (p ∈⇩p A ∨ p ∈⇩p B)"
by (metis (mono_tags, lifting) UnE UnI1 UnI2 image_Un in_pair_def)
lemma in_pair_trans [trans]:
assumes "p ∈⇩p A" and "A ⊆ B"
shows "p ∈⇩p B"
using assms by (auto simp: in_pair_def)
lemma in_pair_same [simp]: "p ∈⇩p A × A ⟷ p ∈ A × A"
by (auto simp: in_pair_def)
lemma subset_pairsI [intro]:
assumes "⋀x. x ∈⇩p A ⟹ x ∈⇩p B"
shows "A ⊆⇩p B"
unfolding subset_pairs_def using assms by blast
lemma subset_pairsD [trans]:
assumes "x ∈⇩p A" and "A ⊆⇩p B"
shows "x ∈⇩p B"
using assms unfolding subset_pairs_def by blast
definition processed :: "('a × 'a) ⇒ 'a list ⇒ ('a × 'a) list ⇒ bool"
where "processed p xs ps ⟷ p ∈ set xs × set xs ∧ p ∉⇩p set ps"
lemma processed_alt:
"processed (a, b) xs ps ⟷ ((a ∈ set xs) ∧ (b ∈ set xs) ∧ (a, b) ∉⇩p set ps)"
unfolding processed_def by auto
lemma processedI:
assumes "a ∈ set xs" and "b ∈ set xs" and "(a, b) ∉⇩p set ps"
shows "processed (a, b) xs ps"
unfolding processed_alt using assms by simp
lemma processedD1:
assumes "processed (a, b) xs ps"
shows "a ∈ set xs"
using assms by (simp add: processed_alt)
lemma processedD2:
assumes "processed (a, b) xs ps"
shows "b ∈ set xs"
using assms by (simp add: processed_alt)
lemma processedD3:
assumes "processed (a, b) xs ps"
shows "(a, b) ∉⇩p set ps"
using assms by (simp add: processed_alt)
lemma processed_Nil: "processed (a, b) xs [] ⟷ (a ∈ set xs ∧ b ∈ set xs)"
by (simp add: processed_alt in_pair_iff)
lemma processed_Cons:
assumes "processed (a, b) xs ps"
and a1: "a = p ⟹ b = q ⟹ thesis"
and a2: "a = q ⟹ b = p ⟹ thesis"
and a3: "processed (a, b) xs ((p, q) # ps) ⟹ thesis"
shows thesis
proof -
from assms(1) have "a ∈ set xs" and "b ∈ set xs" and "(a, b) ∉⇩p set ps"
by (simp_all add: processed_alt)
show ?thesis
proof (cases "(a, b) = (p, q)")
case True
hence "a = p" and "b = q" by simp_all
thus ?thesis by (rule a1)
next
case False
with ‹(a, b) ∉⇩p set ps› have *: "(a, b) ∉ set ((p, q) # ps)" by (auto simp: in_pair_iff)
show ?thesis
proof (cases "(b, a) = (p, q)")
case True
hence "a = q" and "b = p" by simp_all
thus ?thesis by (rule a2)
next
case False
with ‹(a, b) ∉⇩p set ps› have "(b, a) ∉ set ((p, q) # ps)" by (auto simp: in_pair_iff)
with * have "(a, b) ∉⇩p set ((p, q) # ps)" by (simp add: in_pair_iff)
with ‹a ∈ set xs› ‹b ∈ set xs› have "processed (a, b) xs ((p, q) # ps)"
by (rule processedI)
thus ?thesis by (rule a3)
qed
qed
qed
lemma processed_minus:
assumes "processed (a, b) xs (ps -- qs)"
and a1: "(a, b) ∈⇩p set qs ⟹ thesis"
and a2: "processed (a, b) xs ps ⟹ thesis"
shows thesis
proof -
from assms(1) have "a ∈ set xs" and "b ∈ set xs" and "(a, b) ∉⇩p set (ps -- qs)"
by (simp_all add: processed_alt)
show ?thesis
proof (cases "(a, b) ∈⇩p set qs")
case True
thus ?thesis by (rule a1)
next
case False
with ‹(a, b) ∉⇩p set (ps -- qs)› have "(a, b) ∉⇩p set ps"
by (auto simp: set_diff_list in_pair_iff)
with ‹a ∈ set xs› ‹b ∈ set xs› have "processed (a, b) xs ps"
by (rule processedI)
thus ?thesis by (rule a2)
qed
qed
subsection ‹Algorithm Schema›
subsubsection ‹‹const_lt_component››
context ordered_term
begin
definition const_lt_component :: "('t ⇒⇩0 'b::zero) ⇒ 'k option"
where "const_lt_component p =
(let v = lt p in if pp_of_term v = 0 then Some (component_of_term v) else None)"
lemma const_lt_component_SomeI:
assumes "lp p = 0" and "component_of_term (lt p) = cmp"
shows "const_lt_component p = Some cmp"
using assms by (simp add: const_lt_component_def)
lemma const_lt_component_SomeD1:
assumes "const_lt_component p = Some cmp"
shows "lp p = 0"
using assms by (simp add: const_lt_component_def Let_def split: if_split_asm)
lemma const_lt_component_SomeD2:
assumes "const_lt_component p = Some cmp"
shows "component_of_term (lt p) = cmp"
using assms by (simp add: const_lt_component_def Let_def split: if_split_asm)
lemma const_lt_component_subset:
"const_lt_component ` (B - {0}) - {None} ⊆ Some ` component_of_term ` Keys B"
proof
fix k
assume "k ∈ const_lt_component ` (B - {0}) - {None}"
hence "k ∈ const_lt_component ` (B - {0})" and "k ≠ None" by simp_all
from this(1) obtain p where "p ∈ B - {0}" and "k = const_lt_component p" ..
moreover from ‹k ≠ None› obtain k' where "k = Some k'" by blast
ultimately have "const_lt_component p = Some k'" and "p ∈ B" and "p ≠ 0" by simp_all
from this(1) have "component_of_term (lt p) = k'" by (rule const_lt_component_SomeD2)
moreover have "lt p ∈ Keys B" by (rule in_KeysI, rule lt_in_keys, fact+)
ultimately have "k' ∈ component_of_term ` Keys B" by fastforce
thus "k ∈ Some ` component_of_term ` Keys B" by (simp add: ‹k = Some k'›)
qed
corollary card_const_lt_component_le:
assumes "finite B"
shows "card (const_lt_component ` (B - {0}) - {None}) ≤ card (component_of_term ` Keys B)"
proof (rule surj_card_le)
show "finite (component_of_term ` Keys B)"
by (intro finite_imageI finite_Keys, fact)
next
show "const_lt_component ` (B - {0}) - {None} ⊆ Some ` component_of_term ` Keys B"
by (fact const_lt_component_subset)
qed
end
subsubsection ‹Type synonyms›
type_synonym ('a, 'b, 'c) pdata' = "('a ⇒⇩0 'b) × 'c"
type_synonym ('a, 'b, 'c) pdata = "('a ⇒⇩0 'b) × nat × 'c"
type_synonym ('a, 'b, 'c) pdata_pair = "('a, 'b, 'c) pdata × ('a, 'b, 'c) pdata"
type_synonym ('a, 'b, 'c, 'd) selT = "('a, 'b, 'c) pdata list ⇒ ('a, 'b, 'c) pdata list ⇒
('a, 'b, 'c) pdata_pair list ⇒ nat × 'd ⇒ ('a, 'b, 'c) pdata_pair list"
type_synonym ('a, 'b, 'c, 'd) complT = "('a, 'b, 'c) pdata list ⇒ ('a, 'b, 'c) pdata list ⇒
('a, 'b, 'c) pdata_pair list ⇒ ('a, 'b, 'c) pdata_pair list ⇒
nat × 'd ⇒ (('a, 'b, 'c) pdata' list × 'd)"
type_synonym ('a, 'b, 'c, 'd) apT = "('a, 'b, 'c) pdata list ⇒ ('a, 'b, 'c) pdata list ⇒
('a, 'b, 'c) pdata_pair list ⇒ ('a, 'b, 'c) pdata list ⇒ nat × 'd ⇒
('a, 'b, 'c) pdata_pair list"
type_synonym ('a, 'b, 'c, 'd) abT = "('a, 'b, 'c) pdata list ⇒ ('a, 'b, 'c) pdata list ⇒
('a, 'b, 'c) pdata list ⇒ nat × 'd ⇒ ('a, 'b, 'c) pdata list"
subsubsection ‹Specification of the @{emph ‹selector›} parameter›
definition sel_spec :: "('a, 'b, 'c, 'd) selT ⇒ bool"
where "sel_spec sel ⟷
(∀gs bs ps data. ps ≠ [] ⟶ (sel gs bs ps data ≠ [] ∧ set (sel gs bs ps data) ⊆ set ps))"
lemma sel_specI:
assumes "⋀gs bs ps data. ps ≠ [] ⟹ (sel gs bs ps data ≠ [] ∧ set (sel gs bs ps data) ⊆ set ps)"
shows "sel_spec sel"
unfolding sel_spec_def using assms by blast
lemma sel_specD1:
assumes "sel_spec sel" and "ps ≠ []"
shows "sel gs bs ps data ≠ []"
using assms unfolding sel_spec_def by blast
lemma sel_specD2:
assumes "sel_spec sel" and "ps ≠ []"
shows "set (sel gs bs ps data) ⊆ set ps"
using assms unfolding sel_spec_def by blast
subsubsection ‹Specification of the @{emph ‹add-basis›} parameter›
definition ab_spec :: "('a, 'b, 'c, 'd) abT ⇒ bool"
where "ab_spec ab ⟷
(∀gs bs ns data. ns ≠ [] ⟶ set (ab gs bs ns data) = set bs ∪ set ns) ∧
(∀gs bs data. ab gs bs [] data = bs)"
lemma ab_specI:
assumes "⋀gs bs ns data. ns ≠ [] ⟹ set (ab gs bs ns data) = set bs ∪ set ns"
and "⋀gs bs data. ab gs bs [] data = bs"
shows "ab_spec ab"
unfolding ab_spec_def using assms by blast
lemma ab_specD1:
assumes "ab_spec ab"
shows "set (ab gs bs ns data) = set bs ∪ set ns"
using assms unfolding ab_spec_def by (metis empty_set sup_bot.right_neutral)
lemma ab_specD2:
assumes "ab_spec ab"
shows "ab gs bs [] data = bs"
using assms unfolding ab_spec_def by blast
subsubsection ‹Specification of the @{emph ‹add-pairs›} parameter›
definition unique_idx :: "('t, 'b, 'c) pdata list ⇒ (nat × 'd) ⇒ bool"
where "unique_idx bs data ⟷
(∀f∈set bs. ∀g∈set bs. fst (snd f) = fst (snd g) ⟶ f = g) ∧
(∀f∈set bs. fst (snd f) < fst data)"
lemma unique_idxI:
assumes "⋀f g. f ∈ set bs ⟹ g ∈ set bs ⟹ fst (snd f) = fst (snd g) ⟹ f = g"
and "⋀f. f ∈ set bs ⟹ fst (snd f) < fst data"
shows "unique_idx bs data"
unfolding unique_idx_def using assms by blast
lemma unique_idxD1:
assumes "unique_idx bs data" and "f ∈ set bs" and "g ∈ set bs" and "fst (snd f) = fst (snd g)"
shows "f = g"
using assms unfolding unique_idx_def by blast
lemma unique_idxD2:
assumes "unique_idx bs data" and "f ∈ set bs"
shows "fst (snd f) < fst data"
using assms unfolding unique_idx_def by blast
lemma unique_idx_Nil: "unique_idx [] data"
by (simp add: unique_idx_def)
lemma unique_idx_subset:
assumes "unique_idx bs data" and "set bs' ⊆ set bs"
shows "unique_idx bs' data"
proof (rule unique_idxI)
fix f g
assume "f ∈ set bs'" and "g ∈ set bs'"
with assms have "unique_idx bs data" and "f ∈ set bs" and "g ∈ set bs" by auto
moreover assume "fst (snd f) = fst (snd g)"
ultimately show "f = g" by (rule unique_idxD1)
next
fix f
assume "f ∈ set bs'"
with assms(2) have "f ∈ set bs" by auto
with assms(1) show "fst (snd f) < fst data" by (rule unique_idxD2)
qed
context gd_term
begin
definition ap_spec :: "('t, 'b::field, 'c, 'd) apT ⇒ bool"
where "ap_spec ap ⟷ (∀gs bs ps hs data.
set (ap gs bs ps hs data) ⊆ set ps ∪ (set hs × (set gs ∪ set bs ∪ set hs)) ∧
(∀B d m. ∀h∈set hs. ∀g∈set gs ∪ set bs ∪ set hs. dickson_grading d ⟶
set gs ∪ set bs ∪ set hs ⊆ B ⟶ fst ` B ⊆ dgrad_p_set d m ⟶
set ps ⊆ set bs × (set gs ∪ set bs) ⟶ unique_idx (gs @ bs @ hs) data ⟶
is_Groebner_basis (fst ` set gs) ⟶ h ≠ g ⟶ fst h ≠ 0 ⟶ fst g ≠ 0 ⟶
(∀a b. (a, b) ∈⇩p set (ap gs bs ps hs data) ⟶ fst a ≠ 0 ⟶ fst b ≠ 0 ⟶
crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)) ⟶
(∀a b. a ∈ set gs ∪ set bs ⟶ b ∈ set gs ∪ set bs ⟶ fst a ≠ 0 ⟶ fst b ≠ 0 ⟶
crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)) ⟶
crit_pair_cbelow_on d m (fst ` B) (fst h) (fst g)) ∧
(∀B d m. ∀h g. dickson_grading d ⟶
set gs ∪ set bs ∪ set hs ⊆ B ⟶ fst ` B ⊆ dgrad_p_set d m ⟶
set ps ⊆ set bs × (set gs ∪ set bs) ⟶ (set gs ∪ set bs) ∩ set hs = {} ⟶
unique_idx (gs @ bs @ hs) data ⟶ is_Groebner_basis (fst ` set gs) ⟶
h ≠ g ⟶ fst h ≠ 0 ⟶ fst g ≠ 0 ⟶
(h, g) ∈ set ps -⇩p set (ap gs bs ps hs data) ⟶
(∀a b. (a, b) ∈⇩p set (ap gs bs ps hs data) ⟶ (a, b) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs) ⟶
fst a ≠ 0 ⟶ fst b ≠ 0 ⟶ crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)) ⟶
crit_pair_cbelow_on d m (fst ` B) (fst h) (fst g)))"
text ‹Informally, ‹ap_spec ap› means that, for suitable arguments ‹gs›, ‹bs›, ‹ps› and ‹hs›,
the value of ‹ap gs bs ps hs› is a list of pairs ‹ps'› such that for every element ‹(a, b)› missing in ‹ps'›
there exists a set of pairs ‹C› by reference to which ‹(a, b)› can be discarded, i.\,e. as soon as
all critical pairs of the elements in ‹C› can be connected below some set ‹B›, the same is true for
the critical pair of ‹(a, b)›.›
lemma ap_specI:
assumes "⋀gs bs ps hs data. set (ap gs bs ps hs data) ⊆ set ps ∪ (set hs × (set gs ∪ set bs ∪ set hs))"
assumes "⋀gs bs ps hs data B d m h g. dickson_grading d ⟹
set gs ∪ set bs ∪ set hs ⊆ B ⟹ fst ` B ⊆ dgrad_p_set d m ⟹
h ∈ set hs ⟹ g ∈ set gs ∪ set bs ∪ set hs ⟹
set ps ⊆ set bs × (set gs ∪ set bs) ⟹ unique_idx (gs @ bs @ hs) data ⟹
is_Groebner_basis (fst ` set gs) ⟹ h ≠ g ⟹ fst h ≠ 0 ⟹ fst g ≠ 0 ⟹
(⋀a b. (a, b) ∈⇩p set (ap gs bs ps hs data) ⟹ fst a ≠ 0 ⟹ fst b ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)) ⟹
(⋀a b. a ∈ set gs ∪ set bs ⟹ b ∈ set gs ∪ set bs ⟹ fst a ≠ 0 ⟹ fst b ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)) ⟹
crit_pair_cbelow_on d m (fst ` B) (fst h) (fst g)"
assumes "⋀gs bs ps hs data B d m h g. dickson_grading d ⟹
set gs ∪ set bs ∪ set hs ⊆ B ⟹ fst ` B ⊆ dgrad_p_set d m ⟹
set ps ⊆ set bs × (set gs ∪ set bs) ⟹ (set gs ∪ set bs) ∩ set hs = {} ⟹
unique_idx (gs @ bs @ hs) data ⟹ is_Groebner_basis (fst ` set gs) ⟹ h ≠ g ⟹
fst h ≠ 0 ⟹ fst g ≠ 0 ⟹ (h, g) ∈ set ps -⇩p set (ap gs bs ps hs data) ⟹
(⋀a b. (a, b) ∈⇩p set (ap gs bs ps hs data) ⟹ (a, b) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs) ⟹
fst a ≠ 0 ⟹ fst b ≠ 0 ⟹ crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)) ⟹
crit_pair_cbelow_on d m (fst ` B) (fst h) (fst g)"
shows "ap_spec ap"
unfolding ap_spec_def
apply (intro allI conjI impI)
subgoal by (rule assms(1))
subgoal by (intro ballI impI, rule assms(2), blast+)
subgoal by (rule assms(3), blast+)
done
lemma ap_specD1:
assumes "ap_spec ap"
shows "set (ap gs bs ps hs data) ⊆ set ps ∪ (set hs × (set gs ∪ set bs ∪ set hs))"
using assms unfolding ap_spec_def by (elim allE conjE) (assumption)
lemma ap_specD2:
assumes "ap_spec ap" and "dickson_grading d" and "set gs ∪ set bs ∪ set hs ⊆ B"
and "fst ` B ⊆ dgrad_p_set d m" and "(h, g) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs)"
and "set ps ⊆ set bs × (set gs ∪ set bs)" and "unique_idx (gs @ bs @ hs) data"
and "is_Groebner_basis (fst ` set gs)" and "h ≠ g" and "fst h ≠ 0" and "fst g ≠ 0"
and "⋀a b. (a, b) ∈⇩p set (ap gs bs ps hs data) ⟹ fst a ≠ 0 ⟹ fst b ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
and "⋀a b. a ∈ set gs ∪ set bs ⟹ b ∈ set gs ∪ set bs ⟹ fst a ≠ 0 ⟹ fst b ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
shows "crit_pair_cbelow_on d m (fst ` B) (fst h) (fst g)"
proof -
from assms(5) have "(h, g) ∈ set hs × (set gs ∪ set bs ∪ set hs) ∨ (g, h) ∈ set hs × (set gs ∪ set bs ∪ set hs)"
by (simp only: in_pair_iff)
thus ?thesis
proof
assume "(h, g) ∈ set hs × (set gs ∪ set bs ∪ set hs)"
hence "h ∈ set hs" and "g ∈ set gs ∪ set bs ∪ set hs" by simp_all
from assms(1)[unfolded ap_spec_def, rule_format, of gs bs ps hs data] assms(2-4) this assms (6-)
show ?thesis by metis
next
assume "(g, h) ∈ set hs × (set gs ∪ set bs ∪ set hs)"
hence "g ∈ set hs" and "h ∈ set gs ∪ set bs ∪ set hs" by simp_all
hence "crit_pair_cbelow_on d m (fst ` B) (fst g) (fst h)"
using assms(1)[unfolded ap_spec_def, rule_format, of gs bs ps hs data]
assms(2,3,4,6,7,8,10,11,12,13) assms(9)[symmetric]
by metis
thus ?thesis by (rule crit_pair_cbelow_sym)
qed
qed
lemma ap_specD3:
assumes "ap_spec ap" and "dickson_grading d" and "set gs ∪ set bs ∪ set hs ⊆ B"
and "fst ` B ⊆ dgrad_p_set d m" and "set ps ⊆ set bs × (set gs ∪ set bs)"
and "(set gs ∪ set bs) ∩ set hs = {}" and "unique_idx (gs @ bs @ hs) data"
and "is_Groebner_basis (fst ` set gs)" and "h ≠ g" and "fst h ≠ 0" and "fst g ≠ 0"
and "(h, g) ∈⇩p set ps -⇩p set (ap gs bs ps hs data)"
and "⋀a b. a ∈ set hs ⟹ b ∈ set gs ∪ set bs ∪ set hs ⟹ (a, b) ∈⇩p set (ap gs bs ps hs data) ⟹
fst a ≠ 0 ⟹ fst b ≠ 0 ⟹ crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
shows "crit_pair_cbelow_on d m (fst ` B) (fst h) (fst g)"
proof -
have *: "crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
if 1: "(a, b) ∈⇩p set (ap gs bs ps hs data)" and 2: "(a, b) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs)"
and 3: "fst a ≠ 0" and 4: "fst b ≠ 0" for a b
proof -
from 2 have "(a, b) ∈ set hs × (set gs ∪ set bs ∪ set hs) ∨ (b, a) ∈ set hs × (set gs ∪ set bs ∪ set hs)"
by (simp only: in_pair_iff)
thus ?thesis
proof
assume "(a, b) ∈ set hs × (set gs ∪ set bs ∪ set hs)"
hence "a ∈ set hs" and "b ∈ set gs ∪ set bs ∪ set hs" by simp_all
thus ?thesis using 1 3 4 by (rule assms(13))
next
assume "(b, a) ∈ set hs × (set gs ∪ set bs ∪ set hs)"
hence "b ∈ set hs" and "a ∈ set gs ∪ set bs ∪ set hs" by simp_all
moreover from 1 have "(b, a) ∈⇩p set (ap gs bs ps hs data)" by (auto simp: in_pair_iff)
ultimately have "crit_pair_cbelow_on d m (fst ` B) (fst b) (fst a)" using 4 3 by (rule assms(13))
thus ?thesis by (rule crit_pair_cbelow_sym)
qed
qed
from assms(12) have "(h, g) ∈ set ps -⇩p set (ap gs bs ps hs data) ∨
(g, h) ∈ set ps -⇩p set (ap gs bs ps hs data)" by (simp only: in_pair_iff)
thus ?thesis
proof
assume "(h, g) ∈ set ps -⇩p set (ap gs bs ps hs data)"
with assms(1)[unfolded ap_spec_def, rule_format, of gs bs ps hs data] assms(2-11)
show ?thesis using assms(10) * by metis
next
assume "(g, h) ∈ set ps -⇩p set (ap gs bs ps hs data)"
with assms(1)[unfolded ap_spec_def, rule_format, of gs bs ps hs data] assms(2-11)
have "crit_pair_cbelow_on d m (fst ` B) (fst g) (fst h)" using assms(10) * by metis
thus ?thesis by (rule crit_pair_cbelow_sym)
qed
qed
lemma ap_spec_Nil_subset:
assumes "ap_spec ap"
shows "set (ap gs bs ps [] data) ⊆ set ps"
using ap_specD1[OF assms] by fastforce
lemma ap_spec_fst_subset:
assumes "ap_spec ap"
shows "fst ` set (ap gs bs ps hs data) ⊆ fst ` set ps ∪ set hs"
proof -
from ap_specD1[OF assms]
have "fst ` set (ap gs bs ps hs data) ⊆ fst ` (set ps ∪ set hs × (set gs ∪ set bs ∪ set hs))"
by (rule image_mono)
thus ?thesis by auto
qed
lemma ap_spec_snd_subset:
assumes "ap_spec ap"
shows "snd ` set (ap gs bs ps hs data) ⊆ snd ` set ps ∪ set gs ∪ set bs ∪ set hs"
proof -
from ap_specD1[OF assms]
have "snd ` set (ap gs bs ps hs data) ⊆ snd ` (set ps ∪ set hs × (set gs ∪ set bs ∪ set hs))"
by (rule image_mono)
thus ?thesis by auto
qed
lemma ap_spec_inE:
assumes "ap_spec ap" and "(p, q) ∈ set (ap gs bs ps hs data)"
assumes 1: "(p, q) ∈ set ps ⟹ thesis"
assumes 2: "p ∈ set hs ⟹ q ∈ set gs ∪ set bs ∪ set hs ⟹ thesis"
shows thesis
proof -
from assms(2) ap_specD1[OF assms(1)] have "(p, q) ∈ set ps ∪ set hs × (set gs ∪ set bs ∪ set hs)" ..
thus ?thesis
proof
assume "(p, q) ∈ set ps"
thus ?thesis by (rule 1)
next
assume "(p, q) ∈ set hs × (set gs ∪ set bs ∪ set hs)"
hence "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs" by blast+
thus ?thesis by (rule 2)
qed
qed
lemma subset_Times_ap:
assumes "ap_spec ap" and "ab_spec ab" and "set ps ⊆ set bs × (set gs ∪ set bs)"
shows "set (ap gs bs (ps -- sps) hs data) ⊆ set (ab gs bs hs data) × (set gs ∪ set (ab gs bs hs data))"
proof
fix p q
assume "(p, q) ∈ set (ap gs bs (ps -- sps) hs data)"
with assms(1) show "(p, q) ∈ set (ab gs bs hs data) × (set gs ∪ set (ab gs bs hs data))"
proof (rule ap_spec_inE)
assume "(p, q) ∈ set (ps -- sps)"
hence "(p, q) ∈ set ps" by (simp add: set_diff_list)
from this assms(3) have "(p, q) ∈ set bs × (set gs ∪ set bs)" ..
hence "p ∈ set bs" and "q ∈ set gs ∪ set bs" by blast+
thus ?thesis by (auto simp add: ab_specD1[OF assms(2)])
next
assume "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs"
thus ?thesis by (simp add: ab_specD1[OF assms(2)])
qed
qed
subsubsection ‹Function ‹args_to_set››
definition args_to_set :: "('t, 'b::field, 'c) pdata list × ('t, 'b, 'c) pdata list × ('t, 'b, 'c) pdata_pair list ⇒ ('t ⇒⇩0 'b) set"
where "args_to_set x = fst ` (set (fst x) ∪ set (fst (snd x)) ∪ fst ` set (snd (snd x)) ∪ snd ` set (snd (snd x)))"
lemma args_to_set_alt:
"args_to_set (gs, bs, ps) = fst ` set gs ∪ fst ` set bs ∪ fst ` fst ` set ps ∪ fst ` snd ` set ps"
by (simp add: args_to_set_def image_Un)
lemma args_to_set_subset_Times:
assumes "set ps ⊆ set bs × (set gs ∪ set bs)"
shows "args_to_set (gs, bs, ps) = fst ` set gs ∪ fst ` set bs"
unfolding args_to_set_alt using assms by auto
lemma args_to_set_subset:
assumes "ap_spec ap" and "ab_spec ab"
shows "args_to_set (gs, ab gs bs hs data, ap gs bs ps hs data) ⊆
fst ` (set gs ∪ set bs ∪ fst ` set ps ∪ snd ` set ps ∪ set hs)" (is "?l ⊆ fst ` ?r")
proof (simp only: args_to_set_alt Un_subset_iff, intro conjI image_mono)
show "set (ab gs bs hs data) ⊆ ?r" by (auto simp add: ab_specD1[OF assms(2)])
next
from assms(1) have "fst ` set (ap gs bs ps hs data) ⊆ fst ` set ps ∪ set hs"
by (rule ap_spec_fst_subset)
thus "fst ` set (ap gs bs ps hs data) ⊆ ?r" by blast
next
from assms(1) have "snd ` set (ap gs bs ps hs data) ⊆ snd ` set ps ∪ set gs ∪ set bs ∪ set hs"
by (rule ap_spec_snd_subset)
thus "snd ` set (ap gs bs ps hs data) ⊆ ?r" by blast
qed blast
lemma args_to_set_alt2:
assumes "ap_spec ap" and "ab_spec ab" and "set ps ⊆ set bs × (set gs ∪ set bs)"
shows "args_to_set (gs, ab gs bs hs data, ap gs bs (ps -- sps) hs data) =
fst ` (set gs ∪ set bs ∪ set hs)" (is "?l = fst ` ?r")
proof
from assms(1, 2) have "?l ⊆ fst ` (set gs ∪ set bs ∪ fst ` set (ps -- sps) ∪ snd ` set (ps -- sps) ∪ set hs)"
by (rule args_to_set_subset)
also have "... ⊆ fst ` ?r"
proof (rule image_mono)
have "set gs ∪ set bs ∪ fst ` set (ps -- sps) ∪ snd ` set (ps -- sps) ∪ set hs ⊆
set gs ∪ set bs ∪ fst ` set ps ∪ snd ` set ps ∪ set hs" by (auto simp: set_diff_list)
also from assms(3) have "... ⊆ ?r" by fastforce
finally show "set gs ∪ set bs ∪ fst ` set (ps -- sps) ∪ snd ` set (ps -- sps) ∪ set hs ⊆ ?r" .
qed
finally show "?l ⊆ fst ` ?r" .
next
from assms(2) have eq: "set (ab gs bs hs data) = set bs ∪ set hs" by (rule ab_specD1)
have "fst ` ?r ⊆ fst ` set gs ∪ fst ` set (ab gs bs hs data)" unfolding eq using assms(3)
by fastforce
also have "... ⊆ ?l" unfolding args_to_set_alt by fastforce
finally show "fst ` ?r ⊆ ?l" .
qed
lemma args_to_set_subset1:
assumes "set gs1 ⊆ set gs2"
shows "args_to_set (gs1, bs, ps) ⊆ args_to_set (gs2, bs, ps)"
using assms by (auto simp add: args_to_set_alt)
lemma args_to_set_subset2:
assumes "set bs1 ⊆ set bs2"
shows "args_to_set (gs, bs1, ps) ⊆ args_to_set (gs, bs2, ps)"
using assms by (auto simp add: args_to_set_alt)
lemma args_to_set_subset3:
assumes "set ps1 ⊆ set ps2"
shows "args_to_set (gs, bs, ps1) ⊆ args_to_set (gs, bs, ps2)"
using assms unfolding args_to_set_alt by blast
subsubsection ‹Functions ‹count_const_lt_components›, ‹count_rem_comps› and ‹full_gb››
definition rem_comps_spec :: "('t, 'b::zero, 'c) pdata list ⇒ nat × 'd ⇒ bool"
where "rem_comps_spec bs data ⟷ (card (component_of_term ` Keys (fst ` set bs)) =
fst data + card (const_lt_component ` (fst ` set bs - {0}) - {None}))"
definition count_const_lt_components :: "('t, 'b::zero, 'c) pdata' list ⇒ nat"
where "count_const_lt_components hs = length (remdups (filter (λx. x ≠ None) (map (const_lt_component ∘ fst) hs)))"
definition count_rem_components :: "('t, 'b::zero, 'c) pdata' list ⇒ nat"
where "count_rem_components bs = length (remdups (map component_of_term (Keys_to_list (map fst bs)))) -
count_const_lt_components [b←bs . fst b ≠ 0]"
lemma count_const_lt_components_alt:
"count_const_lt_components hs = card (const_lt_component ` fst ` set hs - {None})"
by (simp add: count_const_lt_components_def card_set[symmetric] set_diff_eq image_comp del: not_None_eq)
lemma count_rem_components_alt:
"count_rem_components bs + card (const_lt_component ` (fst ` set bs - {0}) - {None}) =
card (component_of_term ` Keys (fst ` set bs))"
proof -
have eq: "fst ` {x ∈ set bs. fst x ≠ 0} = fst ` set bs - {0}" by fastforce
have "card (const_lt_component ` (fst ` set bs - {0}) - {None}) ≤ card (component_of_term ` Keys (fst ` set bs))"
by (rule card_const_lt_component_le, rule finite_imageI, fact finite_set)
thus ?thesis
by (simp add: count_rem_components_def card_set[symmetric] set_Keys_to_list count_const_lt_components_alt eq)
qed
lemma rem_comps_spec_count_rem_components: "rem_comps_spec bs (count_rem_components bs, data)"
by (simp only: rem_comps_spec_def fst_conv count_rem_components_alt)
definition full_gb :: "('t, 'b, 'c) pdata list ⇒ ('t, 'b::zero_neq_one, 'c::default) pdata list"
where "full_gb bs = map (λk. (monomial 1 (term_of_pair (0, k)), 0, default))
(remdups (map component_of_term (Keys_to_list (map fst bs))))"
lemma fst_set_full_gb:
"fst ` set (full_gb bs) = (λv. monomial 1 (term_of_pair (0, component_of_term v))) ` Keys (fst ` set bs)"
by (simp add: full_gb_def set_Keys_to_list image_comp)
lemma Keys_full_gb:
"Keys (fst ` set (full_gb bs)) = (λv. term_of_pair (0, component_of_term v)) ` Keys (fst ` set bs)"
by (auto simp add: fst_set_full_gb Keys_def image_image)
lemma pps_full_gb: "pp_of_term ` Keys (fst ` set (full_gb bs)) ⊆ {0}"
by (simp add: Keys_full_gb image_comp image_subset_iff term_simps)
lemma components_full_gb:
"component_of_term ` Keys (fst ` set (full_gb bs)) = component_of_term ` Keys (fst ` set bs)"
by (simp add: Keys_full_gb image_comp, rule image_cong, fact refl, simp add: term_simps)
lemma full_gb_is_full_pmdl: "is_full_pmdl (fst ` set (full_gb bs))"
for bs::"('t, 'b::field, 'c::default) pdata list"
proof (rule is_full_pmdlI_lt_finite)
from finite_set show "finite (fst ` set (full_gb bs))" by (rule finite_imageI)
next
fix k
assume "k ∈ component_of_term ` Keys (fst ` set (full_gb bs))"
then obtain v where "v ∈ Keys (fst ` set (full_gb bs))" and k: "k = component_of_term v" ..
from this(1) obtain b where "b ∈ fst ` set (full_gb bs)" and "v ∈ keys b" by (rule in_KeysE)
from this(1) obtain u where "u ∈ Keys (fst ` set bs)" and b: "b = monomial 1 (term_of_pair (0, component_of_term u))"
unfolding fst_set_full_gb ..
have lt: "lt b = term_of_pair (0, component_of_term u)" by (simp add: b lt_monomial)
from ‹v ∈ keys b› have v: "v = term_of_pair (0, component_of_term u)" by (simp add: b)
show "∃b∈fst ` set (full_gb bs). b ≠ 0 ∧ component_of_term (lt b) = k ∧ lp b = 0"
proof (intro bexI conjI)
show "b ≠ 0" by (simp add: b monomial_0_iff)
next
show "component_of_term (lt b) = k" by (simp add: lt term_simps k v)
next
show "lp b = 0" by (simp add: lt term_simps)
qed fact
qed
text ‹In fact, @{thm full_gb_is_full_pmdl} also holds if @{typ 'b} is no field.›
lemma full_gb_isGB: "is_Groebner_basis (fst ` set (full_gb bs))"
proof (rule Buchberger_criterion_finite)
from finite_set show "finite (fst ` set (full_gb bs))" by (rule finite_imageI)
next
fix p q :: "'t ⇒⇩0 'b"
assume "p ∈ fst ` set (full_gb bs)"
then obtain v where p: "p = monomial 1 (term_of_pair (0, component_of_term v))"
unfolding fst_set_full_gb ..
hence lt: "component_of_term (lt p) = component_of_term v" by (simp add: lt_monomial term_simps)
assume "q ∈ fst ` set (full_gb bs)"
then obtain u where q: "q = monomial 1 (term_of_pair (0, component_of_term u))"
unfolding fst_set_full_gb ..
hence lq: "component_of_term (lt q) = component_of_term u" by (simp add: lt_monomial term_simps)
assume "component_of_term (lt p) = component_of_term (lt q)"
hence "component_of_term v = component_of_term u" by (simp only: lt lq)
hence "p = q" by (simp only: p q)
moreover assume "p ≠ q"
ultimately show "(red (fst ` set (full_gb bs)))⇧*⇧* (spoly p q) 0" by (simp only:)
qed
subsubsection ‹Specification of the @{emph ‹completion›} parameter›
definition compl_struct :: "('t, 'b::field, 'c, 'd) complT ⇒ bool"
where "compl_struct compl ⟷
(∀gs bs ps sps data. sps ≠ [] ⟶ set sps ⊆ set ps ⟶
(∀d. dickson_grading d ⟶
dgrad_p_set_le d (fst ` (set (fst (compl gs bs (ps -- sps) sps data)))) (args_to_set (gs, bs, ps))) ∧
component_of_term ` Keys (fst ` (set (fst (compl gs bs (ps -- sps) sps data)))) ⊆
component_of_term ` Keys (args_to_set (gs, bs, ps)) ∧
0 ∉ fst ` set (fst (compl gs bs (ps -- sps) sps data)) ∧
(∀h∈set (fst (compl gs bs (ps -- sps) sps data)). ∀b∈set gs ∪ set bs. fst b ≠ 0 ⟶ ¬ lt (fst b) adds⇩t lt (fst h)))"
lemma compl_structI:
assumes "⋀d gs bs ps sps data. dickson_grading d ⟹ sps ≠ [] ⟹ set sps ⊆ set ps ⟹
dgrad_p_set_le d (fst ` (set (fst (compl gs bs (ps -- sps) sps data)))) (args_to_set (gs, bs, ps))"
assumes "⋀gs bs ps sps data. sps ≠ [] ⟹ set sps ⊆ set ps ⟹
component_of_term ` Keys (fst ` (set (fst (compl gs bs (ps -- sps) sps data)))) ⊆
component_of_term ` Keys (args_to_set (gs, bs, ps))"
assumes "⋀gs bs ps sps data. sps ≠ [] ⟹ set sps ⊆ set ps ⟹ 0 ∉ fst ` set (fst (compl gs bs (ps -- sps) sps data))"
assumes "⋀gs bs ps sps h b data. sps ≠ [] ⟹ set sps ⊆ set ps ⟹ h ∈ set (fst (compl gs bs (ps -- sps) sps data)) ⟹
b ∈ set gs ∪ set bs ⟹ fst b ≠ 0 ⟹ ¬ lt (fst b) adds⇩t lt (fst h)"
shows "compl_struct compl"
unfolding compl_struct_def using assms by auto
lemma compl_structD1:
assumes "compl_struct compl" and "dickson_grading d" and "sps ≠ []" and "set sps ⊆ set ps"
shows "dgrad_p_set_le d (fst ` (set (fst (compl gs bs (ps -- sps) sps data)))) (args_to_set (gs, bs, ps))"
using assms unfolding compl_struct_def by blast
lemma compl_structD2:
assumes "compl_struct compl" and "sps ≠ []" and "set sps ⊆ set ps"
shows "component_of_term ` Keys (fst ` (set (fst (compl gs bs (ps -- sps) sps data)))) ⊆
component_of_term ` Keys (args_to_set (gs, bs, ps))"
using assms unfolding compl_struct_def by blast
lemma compl_structD3:
assumes "compl_struct compl" and "sps ≠ []" and "set sps ⊆ set ps"
shows "0 ∉ fst ` set (fst (compl gs bs (ps -- sps) sps data))"
using assms unfolding compl_struct_def by blast
lemma compl_structD4:
assumes "compl_struct compl" and "sps ≠ []" and "set sps ⊆ set ps"
and "h ∈ set (fst (compl gs bs (ps -- sps) sps data))" and "b ∈ set gs ∪ set bs" and "fst b ≠ 0"
shows "¬ lt (fst b) adds⇩t lt (fst h)"
using assms unfolding compl_struct_def by blast
definition struct_spec :: "('t, 'b::field, 'c, 'd) selT ⇒ ('t, 'b, 'c, 'd) apT ⇒ ('t, 'b, 'c, 'd) abT ⇒
('t, 'b, 'c, 'd) complT ⇒ bool"
where "struct_spec sel ap ab compl ⟷ (sel_spec sel ∧ ap_spec ap ∧ ab_spec ab ∧ compl_struct compl)"
lemma struct_specI:
assumes "sel_spec sel" and "ap_spec ap" and "ab_spec ab" and "compl_struct compl"
shows "struct_spec sel ap ab compl"
unfolding struct_spec_def using assms by (intro conjI)
lemma struct_specD1:
assumes "struct_spec sel ap ab compl"
shows "sel_spec sel"
using assms unfolding struct_spec_def by (elim conjE)
lemma struct_specD2:
assumes "struct_spec sel ap ab compl"
shows "ap_spec ap"
using assms unfolding struct_spec_def by (elim conjE)
lemma struct_specD3:
assumes "struct_spec sel ap ab compl"
shows "ab_spec ab"
using assms unfolding struct_spec_def by (elim conjE)
lemma struct_specD4:
assumes "struct_spec sel ap ab compl"
shows "compl_struct compl"
using assms unfolding struct_spec_def by (elim conjE)
lemmas struct_specD = struct_specD1 struct_specD2 struct_specD3 struct_specD4
definition compl_pmdl :: "('t, 'b::field, 'c, 'd) complT ⇒ bool"
where "compl_pmdl compl ⟷
(∀gs bs ps sps data. is_Groebner_basis (fst ` set gs) ⟶ sps ≠ [] ⟶ set sps ⊆ set ps ⟶
unique_idx (gs @ bs) data ⟶
fst ` (set (fst (compl gs bs (ps -- sps) sps data))) ⊆ pmdl (args_to_set (gs, bs, ps)))"
lemma compl_pmdlI:
assumes "⋀gs bs ps sps data. is_Groebner_basis (fst ` set gs) ⟹ sps ≠ [] ⟹ set sps ⊆ set ps ⟹
unique_idx (gs @ bs) data ⟹
fst ` (set (fst (compl gs bs (ps -- sps) sps data))) ⊆ pmdl (args_to_set (gs, bs, ps))"
shows "compl_pmdl compl"
unfolding compl_pmdl_def using assms by blast
lemma compl_pmdlD:
assumes "compl_pmdl compl" and "is_Groebner_basis (fst ` set gs)"
and "sps ≠ []" and "set sps ⊆ set ps" and "unique_idx (gs @ bs) data"
shows "fst ` (set (fst (compl gs bs (ps -- sps) sps data))) ⊆ pmdl (args_to_set (gs, bs, ps))"
using assms unfolding compl_pmdl_def by blast
definition compl_conn :: "('t, 'b::field, 'c, 'd) complT ⇒ bool"
where "compl_conn compl ⟷
(∀d m gs bs ps sps p q data. dickson_grading d ⟶ fst ` set gs ⊆ dgrad_p_set d m ⟶
is_Groebner_basis (fst ` set gs) ⟶ fst ` set bs ⊆ dgrad_p_set d m ⟶
set ps ⊆ set bs × (set gs ∪ set bs) ⟶ sps ≠ [] ⟶ set sps ⊆ set ps ⟶
unique_idx (gs @ bs) data ⟶ (p, q) ∈ set sps ⟶ fst p ≠ 0 ⟶ fst q ≠ 0 ⟶
crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs) ∪ fst ` set (fst (compl gs bs (ps -- sps) sps data))) (fst p) (fst q))"
text ‹Informally, ‹compl_conn compl› means that, for suitable arguments ‹gs›, ‹bs›, ‹ps› and ‹sps›,
the value of ‹compl gs bs ps sps› is a list ‹hs› such that the critical pairs of all elements in
‹sps› can be connected modulo ‹set gs ∪ set bs ∪ set hs›.›
lemma compl_connI:
assumes "⋀d m gs bs ps sps p q data. dickson_grading d ⟹ fst ` set gs ⊆ dgrad_p_set d m ⟹
is_Groebner_basis (fst ` set gs) ⟹ fst ` set bs ⊆ dgrad_p_set d m ⟹
set ps ⊆ set bs × (set gs ∪ set bs) ⟹ sps ≠ [] ⟹ set sps ⊆ set ps ⟹
unique_idx (gs @ bs) data ⟹ (p, q) ∈ set sps ⟹ fst p ≠ 0 ⟹ fst q ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs) ∪ fst ` set (fst (compl gs bs (ps -- sps) sps data))) (fst p) (fst q)"
shows "compl_conn compl"
unfolding compl_conn_def using assms by presburger
lemma compl_connD:
assumes "compl_conn compl" and "dickson_grading d" and "fst ` set gs ⊆ dgrad_p_set d m"
and "is_Groebner_basis (fst ` set gs)" and "fst ` set bs ⊆ dgrad_p_set d m"
and "set ps ⊆ set bs × (set gs ∪ set bs)" and "sps ≠ []" and "set sps ⊆ set ps"
and "unique_idx (gs @ bs) data" and "(p, q) ∈ set sps" and "fst p ≠ 0" and "fst q ≠ 0"
shows "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs) ∪ fst ` set (fst (compl gs bs (ps -- sps) sps data))) (fst p) (fst q)"
using assms unfolding compl_conn_def Un_assoc by blast
subsubsection ‹Function ‹gb_schema_dummy››
definition (in -) add_indices :: "(('a, 'b, 'c) pdata' list × 'd) ⇒ (nat × 'd) ⇒ (('a, 'b, 'c) pdata list × nat × 'd)"
where [code del]: "add_indices ns data =
(map_idx (λh i. (fst h, i, snd h)) (fst ns) (fst data), fst data + length (fst ns), snd ns)"
lemma (in -) add_indices_code [code]:
"add_indices (ns, data) (n, data') = (map_idx (λ(h, d) i. (h, i, d)) ns n, n + length ns, data)"
by (simp add: add_indices_def case_prod_beta')
lemma fst_add_indices: "map fst (fst (add_indices ns data')) = map fst (fst ns)"
by (simp add: add_indices_def map_map_idx map_idx_no_idx)
corollary fst_set_add_indices: "fst ` set (fst (add_indices ns data')) = fst ` set (fst ns)"
using fst_add_indices by (metis set_map)
lemma in_set_add_indicesE:
assumes "f ∈ set (fst (add_indices aux data))"
obtains i where "i < length (fst aux)" and "f = (fst ((fst aux) ! i), fst data + i, snd ((fst aux) ! i))"
proof -
let ?hs = "fst (add_indices aux data)"
from assms obtain i where "i < length ?hs" and "f = ?hs ! i" by (metis in_set_conv_nth)
from this(1) have "i < length (fst aux)" by (simp add: add_indices_def)
hence "?hs ! i = (fst ((fst aux) ! i), fst data + i, snd ((fst aux) ! i))"
unfolding add_indices_def fst_conv by (rule map_idx_nth)
hence "f = (fst ((fst aux) ! i), fst data + i, snd ((fst aux) ! i))" by (simp add: ‹f = ?hs ! i›)
with ‹i < length (fst aux)› show ?thesis ..
qed
definition gb_schema_aux_term1 :: "((('t, 'b::field, 'c) pdata list × ('t, 'b, 'c) pdata_pair list) ×
(('t, 'b, 'c) pdata list × ('t, 'b, 'c) pdata_pair list)) set"
where "gb_schema_aux_term1 = {(a, b::('t, 'b, 'c) pdata list). (fst ` set a) ⊐p (fst ` set b)} <*lex*>
(measure (card ∘ set))"
definition gb_schema_aux_term2 ::
"('a ⇒ nat) ⇒ ('t, 'b::field, 'c) pdata list ⇒ ((('t, 'b, 'c) pdata list × ('t, 'b, 'c) pdata_pair list) ×
(('t, 'b, 'c) pdata list × ('t, 'b, 'c) pdata_pair list)) set"
where "gb_schema_aux_term2 d gs = {(a, b). dgrad_p_set_le d (args_to_set (gs, a)) (args_to_set (gs, b)) ∧
component_of_term ` Keys (args_to_set (gs, a)) ⊆ component_of_term ` Keys (args_to_set (gs, b))}"
definition gb_schema_aux_term where "gb_schema_aux_term d gs = gb_schema_aux_term1 ∩ gb_schema_aux_term2 d gs"
text ‹@{const gb_schema_aux_term} is needed for proving termination of function ‹gb_schema_aux›.›
lemma gb_schema_aux_term1_wf_on:
assumes "dickson_grading d" and "finite K"
shows "wfp_on (λx y. (x, y) ∈ gb_schema_aux_term1)
{x::(('t, 'b, 'c) pdata list) × ((('t, 'b::field, 'c) pdata_pair list)).
args_to_set (gs, x) ⊆ dgrad_p_set d m ∧ component_of_term ` Keys (args_to_set (gs, x)) ⊆ K}"
proof (rule wfp_onI_min)
let ?B = "dgrad_p_set d m"
let ?A = "{x::(('t, 'b, 'c) pdata list) × ((('t, 'b, 'c) pdata_pair list)).
args_to_set (gs, x) ⊆ ?B ∧ component_of_term ` Keys (args_to_set (gs, x)) ⊆ K}"
let ?C = "Pow ?B ∩ {F. component_of_term ` Keys F ⊆ K}"
have A_sub_Pow: "(image fst) ` set ` fst ` ?A ⊆ ?C"
proof
fix x
assume "x ∈ (image fst) ` set ` fst ` ?A"
then obtain x1 where "x1 ∈ set ` fst ` ?A" and x: "x = fst ` x1" by auto
from this(1) obtain x2 where "x2 ∈ fst ` ?A" and x1: "x1 = set x2" by auto
from this(1) obtain x3 where "x3 ∈ ?A" and x2: "x2 = fst x3" by auto
from this(1) have "args_to_set (gs, x3) ⊆ ?B" and "component_of_term ` Keys (args_to_set (gs, x3)) ⊆ K"
by simp_all
thus "x ∈ ?C" by (simp add: args_to_set_def x x1 x2 image_Un Keys_Un)
qed
fix x Q
assume "x ∈ Q" and "Q ⊆ ?A"
have Q_sub_A: "(image fst) ` set ` fst ` Q ⊆ (image fst) ` set ` fst ` ?A"
by ((rule image_mono)+, fact)
from assms have "wfp_on (⊐p) ?C" by (rule red_supset_wf_on)
moreover have "fst ` set (fst x) ∈ (image fst) ` set ` fst ` Q"
by (rule, fact refl, rule, fact refl, rule, fact refl, simp add: ‹x ∈ Q›)
moreover from Q_sub_A A_sub_Pow have "(image fst) ` set ` fst ` Q ⊆ ?C" by (rule subset_trans)
ultimately obtain z1 where "z1 ∈ (image fst) ` set ` fst ` Q"
and 2: "⋀y. y ⊐p z1 ⟹ y ∉ (image fst) ` set ` fst ` Q" by (rule wfp_onE_min, auto)
from this(1) obtain x1 where "x1 ∈ Q" and z1: "z1 = fst ` set (fst x1)" by auto
let ?Q2 = "{q ∈ Q. fst ` set (fst q) = z1}"
have "snd x1 ∈ snd ` ?Q2" by (rule, fact refl, simp add: ‹x1 ∈ Q› z1)
with wf_measure obtain z2 where "z2 ∈ snd ` ?Q2"
and 3: "⋀y. (y, z2) ∈ measure (card ∘ set) ⟹ y ∉ snd ` ?Q2"
by (rule wfE_min, blast)
from this(1) obtain z where "z ∈ ?Q2" and z2: "z2 = snd z" ..
from this(1) have "z ∈ Q" and eq1: "fst ` set (fst z) = z1" by blast+
from this(1) show "∃z∈Q. ∀y∈?A. (y, z) ∈ gb_schema_aux_term1 ⟶ y ∉ Q"
proof
show "∀y∈?A. (y, z) ∈ gb_schema_aux_term1 ⟶ y ∉ Q"
proof (intro ballI impI)
fix y
assume "y ∈ ?A"
assume "(y, z) ∈ gb_schema_aux_term1"
hence "(fst ` set (fst y) ⊐p z1 ∨ (fst y = fst z ∧ (snd y, z2) ∈ measure (card ∘ set)))"
by (simp add: gb_schema_aux_term1_def eq1[symmetric] z2 in_lex_prod_alt)
thus "y ∉ Q"
proof (elim disjE conjE)
assume "fst ` set (fst y) ⊐p z1"
hence "fst ` set (fst y) ∉ (image fst) ` set ` fst ` Q" by (rule 2)
thus ?thesis by auto
next
assume "(snd y, z2) ∈ measure (card ∘ set)"
hence "snd y ∉ snd ` ?Q2" by (rule 3)
hence "y ∉ ?Q2" by blast
moreover assume "fst y = fst z"
ultimately show ?thesis by (simp add: eq1)
qed
qed
qed
qed
lemma gb_schema_aux_term_wf:
assumes "dickson_grading d"
shows "wf (gb_schema_aux_term d gs)"
proof (rule wfI_min)
fix x::"(('t, 'b, 'c) pdata list) × (('t, 'b, 'c) pdata_pair list)" and Q
assume "x ∈ Q"
let ?A = "args_to_set (gs, x)"
have "finite ?A" by (simp add: args_to_set_def)
then obtain m where A: "?A ⊆ dgrad_p_set d m" by (rule dgrad_p_set_exhaust)
define K where "K = component_of_term ` Keys ?A"
from ‹finite ?A› have "finite K" unfolding K_def by (rule finite_imp_finite_component_Keys)
let ?B = "dgrad_p_set d m"
let ?Q = "{q ∈ Q. args_to_set (gs, q) ⊆ ?B ∧ component_of_term ` Keys (args_to_set (gs, q)) ⊆ K}"
from assms ‹finite K› have "wfp_on (λx y. (x, y) ∈ gb_schema_aux_term1)
{x. args_to_set (gs, x) ⊆ ?B ∧ component_of_term ` Keys (args_to_set (gs, x)) ⊆ K}"
by (rule gb_schema_aux_term1_wf_on)
moreover from ‹x ∈ Q› A have "x ∈ ?Q" by (simp add: K_def)
moreover have "?Q ⊆ {x. args_to_set (gs, x) ⊆ ?B ∧ component_of_term ` Keys (args_to_set (gs, x)) ⊆ K}" by auto
ultimately obtain z where "z ∈ ?Q"
and *: "⋀y. (y, z) ∈ gb_schema_aux_term1 ⟹ y ∉ ?Q" by (rule wfp_onE_min, blast)
from this(1) have "z ∈ Q" and a: "args_to_set (gs, z) ⊆ ?B" and b: "component_of_term ` Keys (args_to_set (gs, z)) ⊆ K"
by simp_all
from this(1) show "∃z∈Q. ∀y. (y, z) ∈ gb_schema_aux_term d gs ⟶ y ∉ Q"
proof
show "∀y. (y, z) ∈ gb_schema_aux_term d gs ⟶ y ∉ Q"
proof (intro allI impI)
fix y
assume "(y, z) ∈ gb_schema_aux_term d gs"
hence "(y, z) ∈ gb_schema_aux_term1" and "(y, z) ∈ gb_schema_aux_term2 d gs"
by (simp_all add: gb_schema_aux_term_def)
from this(2) have "dgrad_p_set_le d (args_to_set (gs, y)) (args_to_set (gs, z))"
and comp_sub: "component_of_term ` Keys (args_to_set (gs, y)) ⊆ component_of_term ` Keys (args_to_set (gs, z))"
by (simp_all add: gb_schema_aux_term2_def)
from this(1) ‹args_to_set (gs, z) ⊆ ?B› have "args_to_set (gs, y) ⊆ ?B"
by (rule dgrad_p_set_le_dgrad_p_set)
moreover from comp_sub b have "component_of_term ` Keys (args_to_set (gs, y)) ⊆ K"
by (rule subset_trans)
moreover from ‹(y, z) ∈ gb_schema_aux_term1› have "y ∉ ?Q" by (rule *)
ultimately show "y ∉ Q" by simp
qed
qed
qed
lemma dgrad_p_set_le_args_to_set_ab:
assumes "dickson_grading d" and "ap_spec ap" and "ab_spec ab" and "compl_struct compl"
assumes "sps ≠ []" and "set sps ⊆ set ps" and "hs = fst (add_indices (compl gs bs (ps -- sps) sps data) data)"
shows "dgrad_p_set_le d (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) (args_to_set (gs, bs, ps))"
(is "dgrad_p_set_le _ ?l ?r")
proof -
have "dgrad_p_set_le d ?l
(fst ` (set gs ∪ set bs ∪ fst ` set (ps -- sps) ∪ snd ` set (ps -- sps) ∪ set hs))"
by (rule dgrad_p_set_le_subset, rule args_to_set_subset[OF assms(2, 3)])
also have "dgrad_p_set_le d ... ?r" unfolding image_Un
proof (intro dgrad_p_set_leI_Un)
show "dgrad_p_set_le d (fst ` set gs) (args_to_set (gs, bs, ps))"
by (rule dgrad_p_set_le_subset, auto simp add: args_to_set_def)
next
show "dgrad_p_set_le d (fst ` set bs) (args_to_set (gs, bs, ps))"
by (rule dgrad_p_set_le_subset, auto simp add: args_to_set_def)
next
show "dgrad_p_set_le d (fst ` fst ` set (ps -- sps)) (args_to_set (gs, bs, ps))"
by (rule dgrad_p_set_le_subset, auto simp add: args_to_set_def set_diff_list)
next
show "dgrad_p_set_le d (fst ` snd ` set (ps -- sps)) (args_to_set (gs, bs, ps))"
by (rule dgrad_p_set_le_subset, auto simp add: args_to_set_def set_diff_list)
next
from assms(4, 1, 5, 6) show "dgrad_p_set_le d (fst ` set hs) (args_to_set (gs, bs, ps))"
unfolding assms(7) fst_set_add_indices by (rule compl_structD1)
qed
finally show ?thesis .
qed
corollary dgrad_p_set_le_args_to_set_struct:
assumes "dickson_grading d" and "struct_spec sel ap ab compl" and "ps ≠ []"
assumes "sps = sel gs bs ps data" and "hs = fst (add_indices (compl gs bs (ps -- sps) sps data) data)"
shows "dgrad_p_set_le d (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) (args_to_set (gs, bs, ps))"
proof -
from assms(2) have sel: "sel_spec sel" and ap: "ap_spec ap" and ab: "ab_spec ab"
and compl: "compl_struct compl" by (rule struct_specD)+
from sel assms(3) have "sps ≠ []" and "set sps ⊆ set ps"
unfolding assms(4) by (rule sel_specD1, rule sel_specD2)
from assms(1) ap ab compl this assms(5) show ?thesis by (rule dgrad_p_set_le_args_to_set_ab)
qed
lemma components_subset_ab:
assumes "ap_spec ap" and "ab_spec ab" and "compl_struct compl"
assumes "sps ≠ []" and "set sps ⊆ set ps" and "hs = fst (add_indices (compl gs bs (ps -- sps) sps data) data)"
shows "component_of_term ` Keys (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) ⊆
component_of_term ` Keys (args_to_set (gs, bs, ps))" (is "?l ⊆ ?r")
proof -
have "?l ⊆ component_of_term ` Keys (fst ` (set gs ∪ set bs ∪ fst ` set (ps -- sps) ∪ snd ` set (ps -- sps) ∪ set hs))"
by (rule image_mono, rule Keys_mono, rule args_to_set_subset[OF assms(1, 2)])
also have "... ⊆ ?r" unfolding image_Un Keys_Un Un_subset_iff
proof (intro conjI)
show "component_of_term ` Keys (fst ` set gs) ⊆ component_of_term ` Keys (args_to_set (gs, bs, ps))"
by (rule image_mono, rule Keys_mono, auto simp add: args_to_set_def)
next
show "component_of_term ` Keys (fst ` set bs) ⊆ component_of_term ` Keys (args_to_set (gs, bs, ps))"
by (rule image_mono, rule Keys_mono, auto simp add: args_to_set_def)
next
show "component_of_term ` Keys (fst ` fst ` set (ps -- sps)) ⊆ component_of_term ` Keys (args_to_set (gs, bs, ps))"
by (rule image_mono, rule Keys_mono, auto simp add: set_diff_list args_to_set_def)
next
show "component_of_term ` Keys (fst ` snd ` set (ps -- sps)) ⊆ component_of_term ` Keys (args_to_set (gs, bs, ps))"
by (rule image_mono, rule Keys_mono, auto simp add: args_to_set_def set_diff_list)
next
from assms(3, 4, 5) show "component_of_term ` Keys (fst ` set hs) ⊆ component_of_term ` Keys (args_to_set (gs, bs, ps))"
unfolding assms(6) fst_set_add_indices by (rule compl_structD2)
qed
finally show ?thesis .
qed
corollary components_subset_struct:
assumes "struct_spec sel ap ab compl" and "ps ≠ []"
assumes "sps = sel gs bs ps data" and "hs = fst (add_indices (compl gs bs (ps -- sps) sps data) data)"
shows "component_of_term ` Keys (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) ⊆
component_of_term ` Keys (args_to_set (gs, bs, ps))"
proof -
from assms(1) have sel: "sel_spec sel" and ap: "ap_spec ap" and ab: "ab_spec ab"
and compl: "compl_struct compl" by (rule struct_specD)+
from sel assms(2) have "sps ≠ []" and "set sps ⊆ set ps"
unfolding assms(3) by (rule sel_specD1, rule sel_specD2)
from ap ab compl this assms(4) show ?thesis by (rule components_subset_ab)
qed
corollary components_struct:
assumes "struct_spec sel ap ab compl" and "ps ≠ []" and "set ps ⊆ set bs × (set gs ∪ set bs)"
assumes "sps = sel gs bs ps data" and "hs = fst (add_indices (compl gs bs (ps -- sps) sps data) data)"
shows "component_of_term ` Keys (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) =
component_of_term ` Keys (args_to_set (gs, bs, ps))" (is "?l = ?r")
proof
from assms(1, 2, 4, 5) show "?l ⊆ ?r" by (rule components_subset_struct)
next
from assms(1) have ap: "ap_spec ap" and ab: "ab_spec ab" and compl: "compl_struct compl"
by (rule struct_specD)+
from ap ab assms(3)
have sub: "set (ap gs bs (ps -- sps) hs data') ⊆ set (ab gs bs hs data') × (set gs ∪ set (ab gs bs hs data'))"
by (rule subset_Times_ap)
show "?r ⊆ ?l"
by (simp add: args_to_set_subset_Times[OF sub] args_to_set_subset_Times[OF assms(3)] ab_specD1[OF ab],
rule image_mono, rule Keys_mono, blast)
qed
lemma struct_spec_red_supset:
assumes "struct_spec sel ap ab compl" and "ps ≠ []" and "sps = sel gs bs ps data"
and "hs = fst (add_indices (compl gs bs (ps -- sps) sps data) data)" and "hs ≠ []"
shows "(fst ` set (ab gs bs hs data')) ⊐p (fst ` set bs)"
proof -
from assms(5) have "set hs ≠ {}" by simp
then obtain h' where "h' ∈ set hs" by fastforce
let ?h = "fst h'"
let ?m = "monomial (lc ?h) (lt ?h)"
from ‹h' ∈ set hs› have h_in: "?h ∈ fst ` set hs" by simp
hence "?h ∈ fst ` set (fst (compl gs bs (ps -- sps) sps data))"
by (simp only: assms(4) fst_set_add_indices)
then obtain h'' where h''_in: "h'' ∈ set (fst (compl gs bs (ps -- sps) sps data))"
and "?h = fst h''" ..
from assms(1) have sel: "sel_spec sel" and ap: "ap_spec ap" and ab: "ab_spec ab"
and compl: "compl_struct compl" by (rule struct_specD)+
from sel assms(2) have "sps ≠ []" and "set sps ⊆ set ps" unfolding assms(3)
by (rule sel_specD1, rule sel_specD2)
from h_in compl_structD3[OF compl this] have "?h ≠ 0" unfolding assms(4) fst_set_add_indices
by metis
show ?thesis
proof (simp add: ab_specD1[OF ab] image_Un, rule)
fix q
assume "is_red (fst ` set bs) q"
moreover have "fst ` set bs ⊆ fst ` set bs ∪ fst ` set hs" by simp
ultimately show "is_red (fst ` set bs ∪ fst ` set hs) q" by (rule is_red_subset)
next
from ‹?h ≠ 0› have "lc ?h ≠ 0" by (rule lc_not_0)
moreover have "?h ∈ {?h}" ..
ultimately have "is_red {?h} ?m" using ‹?h ≠ 0› adds_term_refl by (rule is_red_monomialI)
moreover have "{?h} ⊆ fst ` set bs ∪ fst ` set hs" using h_in by simp
ultimately show "is_red (fst ` set bs ∪ fst ` set hs) ?m" by (rule is_red_subset)
next
show "¬ is_red (fst ` set bs) ?m"
proof
assume "is_red (fst ` set bs) ?m"
then obtain b' where "b' ∈ fst ` set bs" and "b' ≠ 0" and "lt b' adds⇩t lt ?h"
by (rule is_red_monomialE)
from this(1) obtain b where "b ∈ set bs" and b': "b' = fst b" ..
from this(1) have "b ∈ set gs ∪ set bs" by simp
from ‹b' ≠ 0› have "fst b ≠ 0" by (simp add: b')
with compl ‹sps ≠ []› ‹set sps ⊆ set ps› h''_in ‹b ∈ set gs ∪ set bs› have "¬ lt (fst b) adds⇩t lt ?h"
unfolding ‹?h = fst h''› by (rule compl_structD4)
from this ‹lt b' adds⇩t lt ?h› show False by (simp add: b')
qed
qed
qed
lemma unique_idx_append:
assumes "unique_idx gs data" and "(hs, data') = add_indices aux data"
shows "unique_idx (gs @ hs) data'"
proof -
from assms(2) have hs: "hs = fst (add_indices aux data)" and data': "data' = snd (add_indices aux data)"
by (metis fst_conv, metis snd_conv)
have len: "length hs = length (fst aux)" by (simp add: hs add_indices_def)
have eq: "fst data' = fst data + length hs" by (simp add: data' add_indices_def hs)
show ?thesis
proof (rule unique_idxI)
fix f g
assume "f ∈ set (gs @ hs)" and "g ∈ set (gs @ hs)"
hence d1: "f ∈ set gs ∪ set hs" and d2: "g ∈ set gs ∪ set hs" by simp_all
assume id_eq: "fst (snd f) = fst (snd g)"
from d1 show "f = g"
proof
assume "f ∈ set gs"
from d2 show ?thesis
proof
assume "g ∈ set gs"
from assms(1) ‹f ∈ set gs› this id_eq show ?thesis by (rule unique_idxD1)
next
assume "g ∈ set hs"
then obtain j where "g = (fst (fst aux ! j), fst data + j, snd (fst aux ! j))" unfolding hs
by (rule in_set_add_indicesE)
hence "fst (snd g) = fst data + j" by simp
moreover from assms(1) ‹f ∈ set gs› have "fst (snd f) < fst data"
by (rule unique_idxD2)
ultimately show ?thesis by (simp add: id_eq)
qed
next
assume "f ∈ set hs"
then obtain i where f: "f = (fst (fst aux ! i), fst data + i, snd (fst aux ! i))" unfolding hs
by (rule in_set_add_indicesE)
hence *: "fst (snd f) = fst data + i" by simp
from d2 show ?thesis
proof
assume "g ∈ set gs"
with assms(1) have "fst (snd g) < fst data" by (rule unique_idxD2)
with * show ?thesis by (simp add: id_eq)
next
assume "g ∈ set hs"
then obtain j where g: "g = (fst (fst aux ! j), fst data + j, snd (fst aux ! j))" unfolding hs
by (rule in_set_add_indicesE)
hence "fst (snd g) = fst data + j" by simp
with * have "i = j" by (simp add: id_eq)
thus ?thesis by (simp add: f g)
qed
qed
next
fix f
assume "f ∈ set (gs @ hs)"
hence "f ∈ set gs ∪ set hs" by simp
thus "fst (snd f) < fst data'"
proof
assume "f ∈ set gs"
with assms(1) have "fst (snd f) < fst data" by (rule unique_idxD2)
also have "... ≤ fst data'" by (simp add: eq)
finally show ?thesis .
next
assume "f ∈ set hs"
then obtain i where "i < length (fst aux)"
and "f = (fst (fst aux ! i), fst data + i, snd (fst aux ! i))" unfolding hs
by (rule in_set_add_indicesE)
from this(2) have "fst (snd f) = fst data + i" by simp
also from ‹i < length (fst aux)› have "... < fst data + length (fst aux)" by simp
finally show ?thesis by (simp only: eq len)
qed
qed
qed
corollary unique_idx_ab:
assumes "ab_spec ab" and "unique_idx (gs @ bs) data" and "(hs, data') = add_indices aux data"
shows "unique_idx (gs @ ab gs bs hs data') data'"
proof -
from assms(2, 3) have "unique_idx ((gs @ bs) @ hs) data'" by (rule unique_idx_append)
thus ?thesis by (simp add: unique_idx_def ab_specD1[OF assms(1)])
qed
lemma rem_comps_spec_struct:
assumes "struct_spec sel ap ab compl" and "rem_comps_spec (gs @ bs) data" and "ps ≠ []"
and "set ps ⊆ (set bs) × (set gs ∪ set bs)" and "sps = sel gs bs ps (snd data)"
and "aux = compl gs bs (ps -- sps) sps (snd data)" and "(hs, data') = add_indices aux (snd data)"
shows "rem_comps_spec (gs @ ab gs bs hs data') (fst data - count_const_lt_components (fst aux), data')"
proof -
from assms(1) have sel: "sel_spec sel" and ap: "ap_spec ap" and ab: "ab_spec ab" and compl: "compl_struct compl"
by (rule struct_specD)+
from ap ab assms(4)
have sub: "set (ap gs bs (ps -- sps) hs data') ⊆ set (ab gs bs hs data') × (set gs ∪ set (ab gs bs hs data'))"
by (rule subset_Times_ap)
have hs: "hs = fst (add_indices aux (snd data))" by (simp add: assms(7)[symmetric])
from sel assms(3) have "sps ≠ []" and "set sps ⊆ set ps" unfolding assms(5)
by (rule sel_specD1, rule sel_specD2)
have eq0: "fst ` set (fst aux) - {0} = fst ` set (fst aux)"
by (rule Diff_triv, simp add: Int_insert_right assms(6), rule compl_structD3, fact+)
have "component_of_term ` Keys (fst ` set (gs @ ab gs bs hs data')) =
component_of_term ` Keys (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data'))"
by (simp add: args_to_set_subset_Times[OF sub] image_Un)
also from assms(1, 3, 4, 5) hs
have "... = component_of_term ` Keys (args_to_set (gs, bs, ps))" unfolding assms(6)
by (rule components_struct)
also have "... = component_of_term ` Keys (fst ` set (gs @ bs))"
by (simp add: args_to_set_subset_Times[OF assms(4)] image_Un)
finally have eq: "component_of_term ` Keys (fst ` set (gs @ ab gs bs hs data')) =
component_of_term ` Keys (fst ` set (gs @ bs))" .
from assms(2)
have eq2: "card (component_of_term ` Keys (fst ` set (gs @ bs))) =
fst data + card (const_lt_component ` (fst ` set (gs @ bs) - {0}) - {None})" (is "?a = _ + ?b")
by (simp only: rem_comps_spec_def)
have eq3: "card (const_lt_component ` (fst ` set (gs @ ab gs bs hs data') - {0}) - {None}) =
?b + count_const_lt_components (fst aux)" (is "?c = _")
proof (simp add: ab_specD1[OF ab] image_Un Un_assoc[symmetric] Un_Diff count_const_lt_components_alt
hs fst_set_add_indices eq0, rule card_Un_disjoint)
show "finite (const_lt_component ` (fst ` set gs - {0}) - {None} ∪ (const_lt_component ` (fst ` set bs - {0}) - {None}))"
by (intro finite_UnI finite_Diff finite_imageI finite_set)
next
show "finite (const_lt_component ` fst ` set (fst aux) - {None})"
by (rule finite_Diff, intro finite_imageI, fact finite_set)
next
have "(const_lt_component ` (fst ` (set gs ∪ set bs) - {0}) - {None}) ∩
(const_lt_component ` fst ` set (fst aux) - {None}) =
(const_lt_component ` (fst ` (set gs ∪ set bs) - {0}) ∩
const_lt_component ` fst ` set (fst aux)) - {None}" by blast
also have "... = {}"
proof (simp, rule, simp, elim conjE)
fix k
assume "k ∈ const_lt_component ` (fst ` (set gs ∪ set bs) - {0})"
then obtain b where "b ∈ set gs ∪ set bs" and "fst b ≠ 0" and k1: "k = const_lt_component (fst b)"
by blast
assume "k ∈ const_lt_component ` fst ` set (fst aux)"
then obtain h where "h ∈ set (fst aux)" and k2: "k = const_lt_component (fst h)" by blast
show "k = None"
proof (rule ccontr, simp, elim exE)
fix k'
assume "k = Some k'"
hence "lp (fst b) = 0" and "component_of_term (lt (fst b)) = k'" unfolding k1
by (rule const_lt_component_SomeD1, rule const_lt_component_SomeD2)
moreover from ‹k = Some k'› have "lp (fst h) = 0" and "component_of_term (lt (fst h)) = k'"
unfolding k2 by (rule const_lt_component_SomeD1, rule const_lt_component_SomeD2)
ultimately have "lt (fst b) adds⇩t lt (fst h)" by (simp add: adds_term_def)
moreover from compl ‹sps ≠ []› ‹set sps ⊆ set ps› ‹h ∈ set (fst aux)› ‹b ∈ set gs ∪ set bs› ‹fst b ≠ 0›
have "¬ lt (fst b) adds⇩t lt (fst h)" unfolding assms(6) by (rule compl_structD4)
ultimately show False by simp
qed
qed
finally show "(const_lt_component ` (fst ` set gs - {0}) - {None} ∪ (const_lt_component ` (fst ` set bs - {0}) - {None})) ∩
(const_lt_component ` fst ` set (fst aux) - {None}) = {}" by (simp only: Un_Diff image_Un)
qed
have "?c ≤ ?a" unfolding eq[symmetric]
by (rule card_const_lt_component_le, rule finite_imageI, fact finite_set)
hence le: "count_const_lt_components (fst aux) ≤ fst data" by (simp only: eq2 eq3)
show ?thesis by (simp only: rem_comps_spec_def eq eq2 eq3, simp add: le)
qed
lemma pmdl_struct:
assumes "struct_spec sel ap ab compl" and "compl_pmdl compl" and "is_Groebner_basis (fst ` set gs)"
and "ps ≠ []" and "set ps ⊆ (set bs) × (set gs ∪ set bs)" and "unique_idx (gs @ bs) (snd data)"
and "sps = sel gs bs ps (snd data)" and "aux = compl gs bs (ps -- sps) sps (snd data)"
and "(hs, data') = add_indices aux (snd data)"
shows "pmdl (fst ` set (gs @ ab gs bs hs data')) = pmdl (fst ` set (gs @ bs))"
proof -
have hs: "hs = fst (add_indices aux (snd data))" by (simp add: assms(9)[symmetric])
from assms(1) have sel: "sel_spec sel" and ab: "ab_spec ab" by (rule struct_specD)+
have eq: "fst ` (set gs ∪ set (ab gs bs hs data')) = fst ` (set gs ∪ set bs) ∪ fst ` set hs"
by (auto simp add: ab_specD1[OF ab])
show ?thesis
proof (simp add: eq, rule)
show "pmdl (fst ` (set gs ∪ set bs) ∪ fst ` set hs) ⊆ pmdl (fst ` (set gs ∪ set bs))"
proof (rule pmdl.span_subset_spanI, simp only: Un_subset_iff, rule)
show "fst ` (set gs ∪ set bs) ⊆ pmdl (fst ` (set gs ∪ set bs))"
by (fact pmdl.span_superset)
next
from sel assms(4) have "sps ≠ []" and "set sps ⊆ set ps"
unfolding assms(7) by (rule sel_specD1, rule sel_specD2)
with assms(2, 3) have "fst ` set hs ⊆ pmdl (args_to_set (gs, bs, ps))"
unfolding hs assms(8) fst_set_add_indices using assms(6) by (rule compl_pmdlD)
thus "fst ` set hs ⊆ pmdl (fst ` (set gs ∪ set bs))"
by (simp only: args_to_set_subset_Times[OF assms(5)] image_Un)
qed
next
show "pmdl (fst ` (set gs ∪ set bs)) ⊆ pmdl (fst ` (set gs ∪ set bs) ∪ fst ` set hs)"
by (rule pmdl.span_mono, blast)
qed
qed
lemma discarded_subset:
assumes "ab_spec ab"
and "D' = D ∪ (set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps) -⇩p set (ap gs bs (ps -- sps) hs data'))"
and "set ps ⊆ set bs × (set gs ∪ set bs)" and "D ⊆ (set gs ∪ set bs) × (set gs ∪ set bs)"
shows "D' ⊆ (set gs ∪ set (ab gs bs hs data')) × (set gs ∪ set (ab gs bs hs data'))"
proof -
from assms(1) have eq: "set (ab gs bs hs data') = set bs ∪ set hs" by (rule ab_specD1)
from assms(4) have "D ⊆ (set gs ∪ (set bs ∪ set hs)) × (set gs ∪ (set bs ∪ set hs))" by fastforce
moreover have "set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps) -⇩p set (ap gs bs (ps -- sps) hs data') ⊆
(set gs ∪ (set bs ∪ set hs)) × (set gs ∪ (set bs ∪ set hs))" (is "?l ⊆ ?r")
proof (rule subset_trans)
show "?l ⊆ set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps)"
by (simp add: minus_pairs_def)
next
have "set hs × (set gs ∪ set bs ∪ set hs) ⊆ ?r" by fastforce
moreover have "set (ps -- sps) ⊆ ?r"
proof (rule subset_trans)
show "set (ps -- sps) ⊆ set ps" by (auto simp: set_diff_list)
next
from assms(3) show "set ps ⊆ ?r" by fastforce
qed
ultimately show "set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps) ⊆ ?r" by (rule Un_least)
qed
ultimately show ?thesis unfolding eq assms(2) by (rule Un_least)
qed
lemma compl_struct_disjoint:
assumes "compl_struct compl" and "sps ≠ []" and "set sps ⊆ set ps"
shows "fst ` set (fst (compl gs bs (ps -- sps) sps data)) ∩ fst ` (set gs ∪ set bs) = {}"
proof (rule, rule)
fix x
assume "x ∈ fst ` set (fst (compl gs bs (ps -- sps) sps data)) ∩ fst ` (set gs ∪ set bs)"
hence x_in: "x ∈ fst ` set (fst (compl gs bs (ps -- sps) sps data))" and "x ∈ fst ` (set gs ∪ set bs)"
by simp_all
from x_in obtain h where h_in: "h ∈ set (fst (compl gs bs (ps -- sps) sps data))" and x1: "x = fst h" ..
from compl_structD3[OF assms, of gs bs data] x_in have "x ≠ 0" by auto
from ‹x ∈ fst ` (set gs ∪ set bs)› obtain b where b_in: "b ∈ set gs ∪ set bs" and x2: "x = fst b" ..
from ‹x ≠ 0› have "fst b ≠ 0" by (simp add: x2)
with assms h_in b_in have "¬ lt (fst b) adds⇩t lt (fst h)" by (rule compl_structD4)
hence "¬ lt x adds⇩t lt x" by (simp add: x1[symmetric] x2)
from this adds_term_refl show "x ∈ {}" ..
qed simp
context
fixes sel::"('t, 'b::field, 'c::default, 'd) selT" and ap::"('t, 'b, 'c, 'd) apT"
and ab::"('t, 'b, 'c, 'd) abT" and compl::"('t, 'b, 'c, 'd) complT"
and gs::"('t, 'b, 'c) pdata list"
begin
function (domintros) gb_schema_dummy :: "nat × nat × 'd ⇒ ('t, 'b, 'c) pdata_pair set ⇒
('t, 'b, 'c) pdata list ⇒ ('t, 'b, 'c) pdata_pair list ⇒
(('t, 'b, 'c) pdata list × ('t, 'b, 'c) pdata_pair set)"
where
"gb_schema_dummy data D bs ps =
(if ps = [] then
(gs @ bs, D)
else
(let sps = sel gs bs ps (snd data); ps0 = ps -- sps; aux = compl gs bs ps0 sps (snd data);
remcomps = fst (data) - count_const_lt_components (fst aux) in
(if remcomps = 0 then
(full_gb (gs @ bs), D)
else
let (hs, data') = add_indices aux (snd data) in
gb_schema_dummy (remcomps, data')
(D ∪ ((set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps)) -⇩p set (ap gs bs ps0 hs data')))
(ab gs bs hs data') (ap gs bs ps0 hs data')
)
)
)"
by pat_completeness auto
lemma gb_schema_dummy_domI1: "gb_schema_dummy_dom (data, D, bs, [])"
by (rule gb_schema_dummy.domintros, simp)
lemma gb_schema_dummy_domI2:
assumes "struct_spec sel ap ab compl"
shows "gb_schema_dummy_dom (data, D, args)"
proof -
from assms have sel: "sel_spec sel" and ap: "ap_spec ap" and ab: "ab_spec ab" by (rule struct_specD)+
from ex_dgrad obtain d::"'a ⇒ nat" where dg: "dickson_grading d" ..
let ?R = "(gb_schema_aux_term d gs)"
from dg have "wf ?R" by (rule gb_schema_aux_term_wf)
thus ?thesis
proof (induct args arbitrary: data D rule: wf_induct_rule)
fix x data D
assume IH: "⋀y data' D'. (y, x) ∈ ?R ⟹ gb_schema_dummy_dom (data', D', y)"
obtain bs ps where x: "x = (bs, ps)" by (meson case_prodE case_prodI2)
show "gb_schema_dummy_dom (data, D, x)" unfolding x
proof (rule gb_schema_dummy.domintros)
fix rc0 n0 data0 hs n1 data1
assume "ps ≠ []"
and hs_data': "(hs, n1, data1) = add_indices (compl gs bs (ps -- sel gs bs ps (n0, data0))
(sel gs bs ps (n0, data0)) (n0, data0)) (n0, data0)"
and data: "data = (rc0, n0, data0)"
define sps where "sps = sel gs bs ps (n0, data0)"
define data' where "data' = (n1, data1)"
define D' where "D' = D ∪
(set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps) -⇩p
set (ap gs bs (ps -- sps) hs data'))"
define rc where "rc = rc0 - count_const_lt_components (fst (compl gs bs (ps -- sel gs bs ps (n0, data0))
(sel gs bs ps (n0, data0)) (n0, data0)))"
from hs_data' have hs: "hs = fst (add_indices (compl gs bs (ps -- sps) sps (snd data)) (snd data))"
unfolding sps_def data snd_conv by (metis fstI)
show "gb_schema_dummy_dom ((rc, data'), D', ab gs bs hs data', ap gs bs (ps -- sps) hs data')"
proof (rule IH, simp add: x gb_schema_aux_term_def gb_schema_aux_term1_def gb_schema_aux_term2_def, intro conjI)
show "fst ` set (ab gs bs hs data') ⊐p fst ` set bs ∨
ab gs bs hs data' = bs ∧ card (set (ap gs bs (ps -- sps) hs data')) < card (set ps)"
proof (cases "hs = []")
case True
have "ab gs bs hs data' = bs ∧ card (set (ap gs bs (ps -- sps) hs data')) < card (set ps)"
proof (simp only: True, rule)
from ab show "ab gs bs [] data' = bs" by (rule ab_specD2)
next
from sel ‹ps ≠ []› have "sps ≠ []" and "set sps ⊆ set ps"
unfolding sps_def by (rule sel_specD1, rule sel_specD2)
moreover from sel_specD1[OF sel ‹ps ≠ []›] have "set sps ≠ {}" by (simp add: sps_def)
ultimately have "set ps ∩ set sps ≠ {}" by (simp add: inf.absorb_iff2)
hence "set (ps -- sps) ⊂ set ps" unfolding set_diff_list by fastforce
hence "card (set (ps -- sps)) < card (set ps)" by (simp add: psubset_card_mono)
moreover have "card (set (ap gs bs (ps -- sps) [] data')) ≤ card (set (ps -- sps))"
by (rule card_mono, fact finite_set, rule ap_spec_Nil_subset, fact ap)
ultimately show "card (set (ap gs bs (ps -- sps) [] data')) < card (set ps)" by simp
qed
thus ?thesis ..
next
case False
with assms ‹ps ≠ []› sps_def hs have "fst ` set (ab gs bs hs data') ⊐p fst ` set bs"
unfolding data snd_conv by (rule struct_spec_red_supset)
thus ?thesis ..
qed
next
from dg assms ‹ps ≠ []› sps_def hs
show "dgrad_p_set_le d (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) (args_to_set (gs, bs, ps))"
unfolding data snd_conv by (rule dgrad_p_set_le_args_to_set_struct)
next
from assms ‹ps ≠ []› sps_def hs
show "component_of_term ` Keys (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) ⊆
component_of_term ` Keys (args_to_set (gs, bs, ps))"
unfolding data snd_conv by (rule components_subset_struct)
qed
qed
qed
qed
lemmas gb_schema_dummy_simp = gb_schema_dummy.psimps[OF gb_schema_dummy_domI2]
lemma gb_schema_dummy_Nil [simp]: "gb_schema_dummy data D bs [] = (gs @ bs, D)"
by (simp add: gb_schema_dummy.psimps[OF gb_schema_dummy_domI1])
lemma gb_schema_dummy_not_Nil:
assumes "struct_spec sel ap ab compl" and "ps ≠ []"
shows "gb_schema_dummy data D bs ps =
(let sps = sel gs bs ps (snd data); ps0 = ps -- sps; aux = compl gs bs ps0 sps (snd data);
remcomps = fst (data) - count_const_lt_components (fst aux) in
(if remcomps = 0 then
(full_gb (gs @ bs), D)
else
let (hs, data') = add_indices aux (snd data) in
gb_schema_dummy (remcomps, data')
(D ∪ ((set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps)) -⇩p set (ap gs bs ps0 hs data')))
(ab gs bs hs data') (ap gs bs ps0 hs data')
)
)"
by (simp add: gb_schema_dummy_simp[OF assms(1)] assms(2))
lemma gb_schema_dummy_induct [consumes 1, case_names base rec1 rec2]:
assumes "struct_spec sel ap ab compl"
assumes base: "⋀bs data D. P data D bs [] (gs @ bs, D)"
and rec1: "⋀bs ps sps data D. ps ≠ [] ⟹ sps = sel gs bs ps (snd data) ⟹
fst (data) ≤ count_const_lt_components (fst (compl gs bs (ps -- sps) sps (snd data))) ⟹
P data D bs ps (full_gb (gs @ bs), D)"
and rec2: "⋀bs ps sps aux hs rc data data' D D'. ps ≠ [] ⟹ sps = sel gs bs ps (snd data) ⟹
aux = compl gs bs (ps -- sps) sps (snd data) ⟹ (hs, data') = add_indices aux (snd data) ⟹
rc = fst data - count_const_lt_components (fst aux) ⟹ 0 < rc ⟹
D' = (D ∪ ((set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps)) -⇩p set (ap gs bs (ps -- sps) hs data'))) ⟹
P (rc, data') D' (ab gs bs hs data') (ap gs bs (ps -- sps) hs data')
(gb_schema_dummy (rc, data') D' (ab gs bs hs data') (ap gs bs (ps -- sps) hs data')) ⟹
P data D bs ps (gb_schema_dummy (rc, data') D' (ab gs bs hs data') (ap gs bs (ps -- sps) hs data'))"
shows "P data D bs ps (gb_schema_dummy data D bs ps)"
proof -
from assms(1) have "gb_schema_dummy_dom (data, D, bs, ps)" by (rule gb_schema_dummy_domI2)
thus ?thesis
proof (induct data D bs ps rule: gb_schema_dummy.pinduct)
case (1 data D bs ps)
show ?case
proof (cases "ps = []")
case True
show ?thesis by (simp add: True, rule base)
next
case False
show ?thesis
proof (simp only: gb_schema_dummy_not_Nil[OF assms(1) False] Let_def split: if_split, intro conjI impI)
define sps where "sps = sel gs bs ps (snd data)"
assume "fst data - count_const_lt_components (fst (compl gs bs (ps -- sps) sps (snd data))) = 0"
hence "fst data ≤ count_const_lt_components (fst (compl gs bs (ps -- sps) sps (snd data)))"
by simp
with False sps_def show "P data D bs ps (full_gb (gs @ bs), D)" by (rule rec1)
next
define sps where "sps = sel gs bs ps (snd data)"
define aux where "aux = compl gs bs (ps -- sps) sps (snd data)"
define hs where "hs = fst (add_indices aux (snd data))"
define data' where "data' = snd (add_indices aux (snd data))"
define rc where "rc = fst data - count_const_lt_components (fst aux)"
define D' where "D' = (D ∪ ((set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps)) -⇩p set (ap gs bs (ps -- sps) hs data')))"
have eq: "add_indices aux (snd data) = (hs, data')" by (simp add: hs_def data'_def)
assume "rc ≠ 0"
hence "0 < rc" by simp
show "P data D bs ps
(case add_indices aux (snd data) of
(hs, data') ⇒
gb_schema_dummy (rc, data')
(D ∪ (set hs × (set gs ∪ set bs ∪ set hs) ∪ set (ps -- sps) -⇩p set (ap gs bs (ps -- sps) hs data')))
(ab gs bs hs data') (ap gs bs (ps -- sps) hs data'))"
unfolding eq prod.case D'_def[symmetric] using False sps_def aux_def eq[symmetric] rc_def ‹0 < rc› D'_def
proof (rule rec2)
show "P (rc, data') D' (ab gs bs hs data') (ap gs bs (ps -- sps) hs data')
(gb_schema_dummy (rc, data') D' (ab gs bs hs data') (ap gs bs (ps -- sps) hs data'))"
unfolding D'_def using False sps_def refl aux_def rc_def ‹rc ≠ 0› eq[symmetric] refl
by (rule 1)
qed
qed
qed
qed
qed
lemma fst_gb_schema_dummy_dgrad_p_set_le:
assumes "dickson_grading d" and "struct_spec sel ap ab compl"
shows "dgrad_p_set_le d (fst ` set (fst (gb_schema_dummy data D bs ps))) (args_to_set (gs, bs, ps))"
using assms(2)
proof (induct rule: gb_schema_dummy_induct)
case (base bs data D)
show ?case by (simp add: args_to_set_def, rule dgrad_p_set_le_subset, fact subset_refl)
next
case (rec1 bs ps sps data D)
show ?case
proof (cases "fst ` set gs ∪ fst ` set bs ⊆ {0}")
case True
hence "Keys (fst ` set (gs @ bs)) = {}" by (auto simp add: image_Un Keys_def)
hence "component_of_term ` Keys (fst ` set (full_gb (gs @ bs))) = {}"
by (simp add: components_full_gb)
hence "Keys (fst ` set (full_gb (gs @ bs))) = {}" by simp
thus ?thesis by (simp add: dgrad_p_set_le_def dgrad_set_le_def)
next
case False
from pps_full_gb have "dgrad_set_le d (pp_of_term ` Keys (fst ` set (full_gb (gs @ bs)))) {0}"
by (rule dgrad_set_le_subset)
also have "dgrad_set_le d ... (pp_of_term ` Keys (args_to_set (gs, bs, ps)))"
proof (rule dgrad_set_leI, simp)
from False have "Keys (args_to_set (gs, bs, ps)) ≠ {}"
by (simp add: args_to_set_alt Keys_Un, metis Keys_not_empty singletonI subsetI)
then obtain v where "v ∈ Keys (args_to_set (gs, bs, ps))" by blast
moreover have "d 0 ≤ d (pp_of_term v)" by (simp add: assms(1) dickson_grading_adds_imp_le)
ultimately show "∃t∈Keys (args_to_set (gs, bs, ps)). d 0 ≤ d (pp_of_term t)" ..
qed
finally show ?thesis by (simp add: dgrad_p_set_le_def)
qed
next
case (rec2 bs ps sps aux hs rc data data' D D')
from rec2(4) have "hs = fst (add_indices (compl gs bs (ps -- sps) sps (snd data)) (snd data))"
unfolding rec2(3) by (metis fstI)
with assms rec2(1, 2)
have "dgrad_p_set_le d (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) (args_to_set (gs, bs, ps))"
by (rule dgrad_p_set_le_args_to_set_struct)
with rec2(8) show ?case by (rule dgrad_p_set_le_trans)
qed
lemma fst_gb_schema_dummy_components:
assumes "struct_spec sel ap ab compl" and "set ps ⊆ (set bs) × (set gs ∪ set bs)"
shows "component_of_term ` Keys (fst ` set (fst (gb_schema_dummy data D bs ps))) =
component_of_term ` Keys (args_to_set (gs, bs, ps))"
using assms
proof (induct rule: gb_schema_dummy_induct)
case (base bs data D)
show ?case by (simp add: args_to_set_def)
next
case (rec1 bs ps sps data D)
have "component_of_term ` Keys (fst ` set (full_gb (gs @ bs))) =
component_of_term ` Keys (fst ` set (gs @ bs))" by (fact components_full_gb)
also have "... = component_of_term ` Keys (args_to_set (gs, bs, ps))"
by (simp add: args_to_set_subset_Times[OF rec1.prems] image_Un)
finally show ?case by simp
next
case (rec2 bs ps sps aux hs rc data data' D D')
from assms(1) have ap: "ap_spec ap" and ab: "ab_spec ab" by (rule struct_specD)+
from this rec2.prems
have sub: "set (ap gs bs (ps -- sps) hs data') ⊆ set (ab gs bs hs data') × (set gs ∪ set (ab gs bs hs data'))"
by (rule subset_Times_ap)
from rec2(4) have hs: "hs = fst (add_indices (compl gs bs (ps -- sps) sps (snd data)) (snd data))"
unfolding rec2(3) by (metis fstI)
have "component_of_term ` Keys (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) =
component_of_term ` Keys (args_to_set (gs, bs, ps))" (is "?l = ?r")
proof
from assms(1) rec2(1, 2) hs show "?l ⊆ ?r" by (rule components_subset_struct)
next
show "?r ⊆ ?l"
by (simp add: args_to_set_subset_Times[OF rec2.prems] args_to_set_alt2[OF ap ab rec2.prems] image_Un,
rule image_mono, rule Keys_mono, blast)
qed
with rec2.hyps(8)[OF sub] show ?case by (rule trans)
qed
lemma fst_gb_schema_dummy_pmdl:
assumes "struct_spec sel ap ab compl" and "compl_pmdl compl" and "is_Groebner_basis (fst ` set gs)"
and "set ps ⊆ set bs × (set gs ∪ set bs)" and "unique_idx (gs @ bs) (snd data)"
and "rem_comps_spec (gs @ bs) data"
shows "pmdl (fst ` set (fst (gb_schema_dummy data D bs ps))) = pmdl (fst ` set (gs @ bs))"
proof -
from assms(1) have sel: "sel_spec sel" and ap: "ap_spec ap" and ab: "ab_spec ab" and compl: "compl_struct compl"
by (rule struct_specD)+
from assms(1, 4, 5, 6) show ?thesis
proof (induct bs ps rule: gb_schema_dummy_induct)
case (base bs data D)
show ?case by simp
next
case (rec1 bs ps sps data D)
define aux where "aux = compl gs bs (ps -- sps) sps (snd data)"
define data' where "data' = snd (add_indices aux (snd data))"
define hs where "hs = fst (add_indices aux (snd data))"
have hs_data': "(hs, data') = add_indices aux (snd data)" by (simp add: hs_def data'_def)
have eq: "set (gs @ ab gs bs hs data') = set (gs @ bs @ hs)" by (simp add: ab_specD1[OF ab])
from sel rec1(1) have "sps ≠ []" and "set sps ⊆ set ps" unfolding rec1(2)
by (rule sel_specD1, rule sel_specD2)
from full_gb_is_full_pmdl have "pmdl (fst ` set (full_gb (gs @ bs))) = pmdl (fst ` set (gs @ ab gs bs hs data'))"
proof (rule is_full_pmdl_eq)
show "is_full_pmdl (fst ` set (gs @ ab gs bs hs data'))"
proof (rule is_full_pmdlI_lt_finite)
from finite_set show "finite (fst ` set (gs @ ab gs bs hs data'))" by (rule finite_imageI)
next
fix k
assume "k ∈ component_of_term ` Keys (fst ` set (gs @ ab gs bs hs data'))"
hence "Some k ∈ Some ` component_of_term ` Keys (fst ` set (gs @ ab gs bs hs data'))" by simp
also have "... = const_lt_component ` (fst ` set (gs @ ab gs bs hs data') - {0}) - {None}" (is "?A = ?B")
proof (rule card_seteq[symmetric])
show "finite ?A" by (intro finite_imageI finite_Keys, fact finite_set)
next
have "rem_comps_spec (gs @ ab gs bs hs data') (fst data - count_const_lt_components (fst aux), data')"
using assms(1) rec1.prems(3) rec1.hyps(1) rec1.prems(1) rec1.hyps(2) aux_def hs_data'
by (rule rem_comps_spec_struct)
also have "... = (0, data')" by (simp add: aux_def rec1.hyps(3))
finally have "card (const_lt_component ` (fst ` set (gs @ ab gs bs hs data') - {0}) - {None}) =
card (component_of_term ` Keys (fst ` set (gs @ ab gs bs hs data')))"
by (simp add: rem_comps_spec_def)
also have "... = card (Some ` component_of_term ` Keys (fst ` set (gs @ ab gs bs hs data')))"
by (rule card_image[symmetric], simp)
finally show "card ?A ≤ card ?B" by simp
qed (fact const_lt_component_subset)
finally have "Some k ∈ const_lt_component ` (fst ` set (gs @ ab gs bs hs data') - {0})"
by simp
then obtain b where "b ∈ fst ` set (gs @ ab gs bs hs data')" and "b ≠ 0"
and *: "const_lt_component b = Some k" by fastforce
show "∃b∈fst ` set (gs @ ab gs bs hs data'). b ≠ 0 ∧ component_of_term (lt b) = k ∧ lp b = 0"
proof (intro bexI conjI)
from * show "component_of_term (lt b) = k" by (rule const_lt_component_SomeD2)
next
from * show "lp b = 0" by (rule const_lt_component_SomeD1)
qed fact+
qed
next
from compl ‹sps ≠ []› ‹set sps ⊆ set ps›
have "component_of_term ` Keys (fst ` set hs) ⊆ component_of_term ` Keys (args_to_set (gs, bs, ps))"
unfolding hs_def aux_def fst_set_add_indices by (rule compl_structD2)
hence sub: "component_of_term ` Keys (fst ` set hs) ⊆ component_of_term ` Keys (fst ` set (gs @ bs))"
by (simp add: args_to_set_subset_Times[OF rec1.prems(1)] image_Un)
have "component_of_term ` Keys (fst ` set (full_gb (gs @ bs))) =
component_of_term ` Keys (fst ` set (gs @ bs))" by (fact components_full_gb)
also have "... = component_of_term ` Keys (fst ` set ((gs @ bs) @ hs))"
by (simp only: set_append[of _ hs] image_Un Keys_Un Un_absorb2 sub)
finally show "component_of_term ` Keys (fst ` set (full_gb (gs @ bs))) =
component_of_term ` Keys (fst ` set (gs @ ab gs bs hs data'))"
by (simp only: eq append_assoc)
qed
also have "... = pmdl (fst ` set (gs @ bs))"
using assms(1, 2, 3) rec1.hyps(1) rec1.prems(1, 2) rec1.hyps(2) aux_def hs_data'
by (rule pmdl_struct)
finally show ?case by simp
next
case (rec2 bs ps sps aux hs rc data data' D D')
from rec2(4) have hs: "hs = fst (add_indices aux (snd data))" by (metis fstI)
have "pmdl (fst ` set (fst (gb_schema_dummy (rc, data') D' (ab gs bs hs data') (ap gs bs (ps -- sps) hs data')))) =
pmdl (fst ` set (gs @ ab gs bs hs data'))"
proof (rule rec2.hyps(8))
from ap ab rec2.prems(1)
show "set (ap gs bs (ps -- sps) hs data') ⊆ set (ab gs bs hs data') × (set gs ∪ set (ab gs bs hs data'))"
by (rule subset_Times_ap)
next
from ab rec2.prems(2) rec2(4) show "unique_idx (gs @ ab gs bs hs data') (snd (rc, data'))"
unfolding snd_conv by (rule unique_idx_ab)
next
show "rem_comps_spec (gs @ ab gs bs hs data') (rc, data')" unfolding rec2.hyps(5)
using assms(1) rec2.prems(3) rec2.hyps(1) rec2.prems(1) rec2.hyps(2, 3, 4)
by (rule rem_comps_spec_struct)
qed
also have "... = pmdl (fst ` set (gs @ bs))"
using assms(1, 2, 3) rec2.hyps(1) rec2.prems(1, 2) rec2.hyps(2, 3, 4) by (rule pmdl_struct)
finally show ?case .
qed
qed
lemma snd_gb_schema_dummy_subset:
assumes "struct_spec sel ap ab compl" and "set ps ⊆ set bs × (set gs ∪ set bs)"
and "D ⊆ (set gs ∪ set bs) × (set gs ∪ set bs)" and "res = gb_schema_dummy data D bs ps"
shows "snd res ⊆ set (fst res) × set (fst res) ∨ (∃xs. fst (res) = full_gb xs)"
using assms
proof (induct data D bs ps rule: gb_schema_dummy_induct)
case (base bs data D)
from base(2) show ?case by (simp add: base(3))
next
case (rec1 bs ps sps data D)
have "∃xs. fst res = full_gb xs" by (auto simp: rec1(6))
thus ?case ..
next
case (rec2 bs ps sps aux hs rc data data' D D')
from assms(1) have ab: "ab_spec ab" and ap: "ap_spec ap" by (rule struct_specD)+
from _ _ rec2.prems(3) show ?case
proof (rule rec2.hyps(8))
from ap ab rec2.prems(1)
show "set (ap gs bs (ps -- sps) hs data') ⊆ set (ab gs bs hs data') × (set gs ∪ set (ab gs bs hs data'))"
by (rule subset_Times_ap)
next
from ab rec2.hyps(7) rec2.prems(1) rec2.prems(2)
show "D' ⊆ (set gs ∪ set (ab gs bs hs data')) × (set gs ∪ set (ab gs bs hs data'))"
by (rule discarded_subset)
qed
qed
lemma gb_schema_dummy_connectible1:
assumes "struct_spec sel ap ab compl" and "compl_conn compl" and "dickson_grading d"
and "fst ` set gs ⊆ dgrad_p_set d m" and "is_Groebner_basis (fst ` set gs)"
and "fst ` set bs ⊆ dgrad_p_set d m"
and "set ps ⊆ set bs × (set gs ∪ set bs)"
and "unique_idx (gs @ bs) (snd data)"
and "⋀p q. processed (p, q) (gs @ bs) ps ⟹ (p, q) ∉⇩p D ⟹ fst p ≠ 0 ⟹ fst q ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs)) (fst p) (fst q)"
and "¬(∃xs. fst (gb_schema_dummy data D bs ps) = full_gb xs)"
assumes "f ∈ set (fst (gb_schema_dummy data D bs ps))"
and "g ∈ set (fst (gb_schema_dummy data D bs ps))"
and "(f, g) ∉⇩p snd (gb_schema_dummy data D bs ps)"
and "fst f ≠ 0" and "fst g ≠ 0"
shows "crit_pair_cbelow_on d m (fst ` set (fst (gb_schema_dummy data D bs ps))) (fst f) (fst g)"
using assms(1, 6, 7, 8, 9, 10, 11, 12, 13)
proof (induct data D bs ps rule: gb_schema_dummy_induct)
case (base bs data D)
show ?case
proof (cases "f ∈ set gs")
case True
show ?thesis
proof (cases "g ∈ set gs")
case True
note assms(3, 4, 5)
moreover from ‹f ∈ set gs› have "fst f ∈ fst ` set gs" by simp
moreover from ‹g ∈ set gs› have "fst g ∈ fst ` set gs" by simp
ultimately have "crit_pair_cbelow_on d m (fst ` set gs) (fst f) (fst g)"
using assms(14, 15) by (rule GB_imp_crit_pair_cbelow_dgrad_p_set)
moreover have "fst ` set gs ⊆ fst ` set (fst (gs @ bs, D))" by auto
ultimately show ?thesis by (rule crit_pair_cbelow_mono)
next
case False
from this base(6, 7) have "processed (g, f) (gs @ bs) []" by (simp add: processed_Nil)
moreover from base.prems(8) have "(g, f) ∉⇩p D" by (simp add: in_pair_iff)
ultimately have "crit_pair_cbelow_on d m (fst ` set (gs @ bs)) (fst g) (fst f)"
using ‹fst g ≠ 0› ‹fst f ≠ 0› unfolding set_append by (rule base(4))
thus ?thesis unfolding fst_conv by (rule crit_pair_cbelow_sym)
qed
next
case False
from this base(6, 7) have "processed (f, g) (gs @ bs) []" by (simp add: processed_Nil)
moreover from base.prems(8) have "(f, g) ∉⇩p D" by simp
ultimately show ?thesis unfolding fst_conv set_append using ‹fst f ≠ 0› ‹fst g ≠ 0› by (rule base(4))
qed
next
case (rec1 bs ps sps data D)
from rec1.prems(5) show ?case by auto
next
case (rec2 bs ps sps aux hs rc data data' D D')
from rec2.hyps(4) have hs: "hs = fst (add_indices aux (snd data))" by (metis fstI)
from assms(1) have sel: "sel_spec sel" and ap: "ap_spec ap" and ab: "ab_spec ab"
and compl: "compl_struct compl"
by (rule struct_specD1, rule struct_specD2, rule struct_specD3, rule struct_specD4)
from sel rec2.hyps(1) have "sps ≠ []" and "set sps ⊆ set ps"
unfolding rec2.hyps(2) by (rule sel_specD1, rule sel_specD2)
from ap ab rec2.prems(2) have ap_sub: "set (ap gs bs (ps -- sps) hs data') ⊆
set (ab gs bs hs data') × (set gs ∪ set (ab gs bs hs data'))"
by (rule subset_Times_ap)
have ns_sub: "fst ` set hs ⊆ dgrad_p_set d m"
proof (rule dgrad_p_set_le_dgrad_p_set)
from compl assms(3) ‹sps ≠ []› ‹set sps ⊆ set ps›
show "dgrad_p_set_le d (fst ` set hs) (args_to_set (gs, bs, ps))"
unfolding hs rec2.hyps(3) fst_set_add_indices by (rule compl_structD1)
next
from assms(4) rec2.prems(1) show "args_to_set (gs, bs, ps) ⊆ dgrad_p_set d m"
by (simp add: args_to_set_subset_Times[OF rec2.prems(2)])
qed
with rec2.prems(1) have ab_sub: "fst ` set (ab gs bs hs data') ⊆ dgrad_p_set d m"
by (auto simp add: ab_specD1[OF ab])
have cpq: "(p, q) ∈⇩p set sps ⟹ fst p ≠ 0 ⟹ fst q ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` (set gs ∪ set (ab gs bs hs data'))) (fst p) (fst q)" for p q
proof -
assume "(p, q) ∈⇩p set sps" and "fst p ≠ 0" and "fst q ≠ 0"
from this(1) have "(p, q) ∈ set sps ∨ (q, p) ∈ set sps" by (simp only: in_pair_iff)
hence "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs) ∪ fst ` set (fst (compl gs bs (ps -- sps) sps (snd data))))
(fst p) (fst q)"
proof
assume "(p, q) ∈ set sps"
from assms(2, 3, 4, 5) rec2.prems(1, 2) ‹sps ≠ []› ‹set sps ⊆ set ps› rec2.prems(3) this
‹fst p ≠ 0› ‹fst q ≠ 0› show ?thesis by (rule compl_connD)
next
assume "(q, p) ∈ set sps"
from assms(2, 3, 4, 5) rec2.prems(1, 2) ‹sps ≠ []› ‹set sps ⊆ set ps› rec2.prems(3) this
‹fst q ≠ 0› ‹fst p ≠ 0›
have "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs) ∪ fst ` set (fst (compl gs bs (ps -- sps) sps (snd data))))
(fst q) (fst p)" by (rule compl_connD)
thus ?thesis by (rule crit_pair_cbelow_sym)
qed
thus "crit_pair_cbelow_on d m (fst ` (set gs ∪ set (ab gs bs hs data'))) (fst p) (fst q)"
by (simp add: ab_specD1[OF ab] hs rec2.hyps(3) fst_set_add_indices image_Un Un_assoc)
qed
from ab_sub ap_sub _ _ rec2.prems(5, 6, 7, 8) show ?case
proof (rule rec2.hyps(8))
from ab rec2.prems(3) rec2(4) show "unique_idx (gs @ ab gs bs hs data') (snd (rc, data'))"
unfolding snd_conv by (rule unique_idx_ab)
next
fix p q :: "('t, 'b, 'c) pdata"
define ps' where "ps' = ap gs bs (ps -- sps) hs data'"
assume "fst p ≠ 0" and "fst q ≠ 0" and "(p, q) ∉⇩p D'"
assume "processed (p, q) (gs @ ab gs bs hs data') ps'"
hence p_in: "p ∈ set gs ∪ set bs ∪ set hs" and q_in: "q ∈ set gs ∪ set bs ∪ set hs"
and "(p, q) ∉⇩p set ps'" by (simp_all add: processed_alt ab_specD1[OF ab])
from this(3) ‹(p, q) ∉⇩p D'› have "(p, q) ∉⇩p D" and "(p, q) ∉⇩p set (ps -- sps)"
and "(p, q) ∉⇩p set hs × (set gs ∪ set bs ∪ set hs)"
by (auto simp: in_pair_iff rec2.hyps(7) ps'_def)
from this(3) p_in q_in have "p ∈ set gs ∪ set bs" and "q ∈ set gs ∪ set bs"
by (meson SigmaI UnE in_pair_iff)+
show "crit_pair_cbelow_on d m (fst ` (set gs ∪ set (ab gs bs hs data'))) (fst p) (fst q)"
proof (cases "component_of_term (lt (fst p)) = component_of_term (lt (fst q))")
case True
show ?thesis
proof (cases "(p, q) ∈⇩p set sps")
case True
from this ‹fst p ≠ 0› ‹fst q ≠ 0› show ?thesis by (rule cpq)
next
case False
with ‹(p, q) ∉⇩p set (ps -- sps)› have "(p, q) ∉⇩p set ps"
by (auto simp: in_pair_iff set_diff_list)
with ‹p ∈ set gs ∪ set bs› ‹q ∈ set gs ∪ set bs› have "processed (p, q) (gs @ bs) ps"
by (simp add: processed_alt)
from this ‹(p, q) ∉⇩p D› ‹fst p ≠ 0› ‹fst q ≠ 0›
have "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs)) (fst p) (fst q)"
by (rule rec2.prems(4))
moreover have "fst ` (set gs ∪ set bs) ⊆ fst ` (set gs ∪ set (ab gs bs hs data'))"
by (auto simp: ab_specD1[OF ab])
ultimately show ?thesis by (rule crit_pair_cbelow_mono)
qed
next
case False
thus ?thesis by (rule crit_pair_cbelow_distinct_component)
qed
qed
qed
lemma gb_schema_dummy_connectible2:
assumes "struct_spec sel ap ab compl" and "compl_conn compl" and "dickson_grading d"
and "fst ` set gs ⊆ dgrad_p_set d m" and "is_Groebner_basis (fst ` set gs)"
and "fst ` set bs ⊆ dgrad_p_set d m"
and "set ps ⊆ set bs × (set gs ∪ set bs)" and "D ⊆ (set gs ∪ set bs) × (set gs ∪ set bs)"
and "set ps ∩⇩p D = {}" and "unique_idx (gs @ bs) (snd data)"
and "⋀B a b. set gs ∪ set bs ⊆ B ⟹ fst ` B ⊆ dgrad_p_set d m ⟹ (a, b) ∈⇩p D ⟹
fst a ≠ 0 ⟹ fst b ≠ 0 ⟹
(⋀x y. x ∈ set gs ∪ set bs ⟹ y ∈ set gs ∪ set bs ⟹ ¬ (x, y) ∈⇩p D ⟹
fst x ≠ 0 ⟹ fst y ≠ 0 ⟹ crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)) ⟹
crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
and "⋀x y. x ∈ set (fst (gb_schema_dummy data D bs ps)) ⟹ y ∈ set (fst (gb_schema_dummy data D bs ps)) ⟹
(x, y) ∉⇩p snd (gb_schema_dummy data D bs ps) ⟹ fst x ≠ 0 ⟹ fst y ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` set (fst (gb_schema_dummy data D bs ps))) (fst x) (fst y)"
and "¬(∃xs. fst (gb_schema_dummy data D bs ps) = full_gb xs)"
assumes "(f, g) ∈⇩p snd (gb_schema_dummy data D bs ps)"
and "fst f ≠ 0" and "fst g ≠ 0"
shows "crit_pair_cbelow_on d m (fst ` set (fst (gb_schema_dummy data D bs ps))) (fst f) (fst g)"
using assms(1, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16)
proof (induct data D bs ps rule: gb_schema_dummy_induct)
case (base bs data D)
have "set gs ∪ set bs ⊆ set (fst (gs @ bs, D))" by simp
moreover from assms(4) base.prems(1) have "fst ` set (fst (gs @ bs, D)) ⊆ dgrad_p_set d m" by auto
moreover from base.prems(9) have "(f, g) ∈⇩p D" by simp
moreover note assms(15, 16)
ultimately show ?case
proof (rule base.prems(6))
fix x y
assume "x ∈ set gs ∪ set bs" and "y ∈ set gs ∪ set bs" and "(x, y) ∉⇩p D"
hence "x ∈ set (fst (gs @ bs, D))" and "y ∈ set (fst (gs @ bs, D))" and "(x, y) ∉⇩p snd (gs @ bs, D)"
by simp_all
moreover assume "fst x ≠ 0" and "fst y ≠ 0"
ultimately show "crit_pair_cbelow_on d m (fst ` set (fst (gs @ bs, D))) (fst x) (fst y)"
by (rule base.prems(7))
qed
next
case (rec1 bs ps sps data D)
from rec1.prems(8) show ?case by auto
next
case (rec2 bs ps sps aux hs rc data data' D D')
from rec2.hyps(4) have hs: "hs = fst (add_indices aux (snd data))" by (metis fstI)
from assms(1) have sel: "sel_spec sel" and ap: "ap_spec ap" and ab: "ab_spec ab"
and compl: "compl_struct compl" by (rule struct_specD)+
let ?X = "set (ps -- sps) ∪ set hs × (set gs ∪ set bs ∪ set hs)"
from sel rec2.hyps(1) have "sps ≠ []" and "set sps ⊆ set ps"
unfolding rec2.hyps(2) by (rule sel_specD1, rule sel_specD2)
have "fst ` set hs ∩ fst ` (set gs ∪ set bs) = {}"
unfolding hs fst_set_add_indices rec2.hyps(3) using compl ‹sps ≠ []› ‹set sps ⊆ set ps›
by (rule compl_struct_disjoint)
hence disj1: "(set gs ∪ set bs) ∩ set hs = {}" by fastforce
have disj2: "set (ap gs bs (ps -- sps) hs data') ∩⇩p D' = {}"
proof (rule, rule)
fix x y
assume "(x, y) ∈ set (ap gs bs (ps -- sps) hs data') ∩⇩p D'"
hence "(x, y) ∈⇩p set (ap gs bs (ps -- sps) hs data') ∩⇩p D'" by (simp add: in_pair_alt)
hence 1: "(x, y) ∈⇩p set (ap gs bs (ps -- sps) hs data')" and "(x, y) ∈⇩p D'" by simp_all
hence "(x, y) ∈⇩p D" by (simp add: rec2.hyps(7))
from this rec2.prems(3) have "x ∈ set gs ∪ set bs" and "y ∈ set gs ∪ set bs"
by (auto simp: in_pair_iff)
from 1 ap_specD1[OF ap] have "(x, y) ∈⇩p ?X" by (rule in_pair_trans)
thus "(x, y) ∈ {}" unfolding in_pair_Un
proof
assume "(x, y) ∈⇩p set (ps -- sps)"
also have "... ⊆ set ps" by (auto simp: set_diff_list)
finally have "(x, y) ∈⇩p set ps ∩⇩p D" using ‹(x, y) ∈⇩p D› by simp
also have "... = {}" by (fact rec2.prems(4))
finally show ?thesis by (simp add: in_pair_iff)
next
assume "(x, y) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs)"
hence "x ∈ set hs ∨ y ∈ set hs" by (auto simp: in_pair_iff)
thus ?thesis
proof
assume "x ∈ set hs"
with ‹x ∈ set gs ∪ set bs› have "x ∈ (set gs ∪ set bs) ∩ set hs" ..
thus ?thesis by (simp add: disj1)
next
assume "y ∈ set hs"
with ‹y ∈ set gs ∪ set bs› have "y ∈ (set gs ∪ set bs) ∩ set hs" ..
thus ?thesis by (simp add: disj1)
qed
qed
qed simp
have hs_sub: "fst ` set hs ⊆ dgrad_p_set d m"
proof (rule dgrad_p_set_le_dgrad_p_set)
from compl assms(3) ‹sps ≠ []› ‹set sps ⊆ set ps›
show "dgrad_p_set_le d (fst ` set hs) (args_to_set (gs, bs, ps))"
unfolding hs rec2.hyps(3) fst_set_add_indices by (rule compl_structD1)
next
from assms(4) rec2.prems(1) show "args_to_set (gs, bs, ps) ⊆ dgrad_p_set d m"
by (simp add: args_to_set_subset_Times[OF rec2.prems(2)])
qed
with rec2.prems(1) have ab_sub: "fst ` set (ab gs bs hs data') ⊆ dgrad_p_set d m"
by (auto simp add: ab_specD1[OF ab])
moreover from ap ab rec2.prems(2)
have ap_sub: "set (ap gs bs (ps -- sps) hs data') ⊆ set (ab gs bs hs data') × (set gs ∪ set (ab gs bs hs data'))"
by (rule subset_Times_ap)
moreover from ab rec2.hyps(7) rec2.prems(2) rec2.prems(3)
have "D' ⊆ (set gs ∪ set (ab gs bs hs data')) × (set gs ∪ set (ab gs bs hs data'))"
by (rule discarded_subset)
moreover note disj2
moreover from ab rec2.prems(5) rec2.hyps(4) have uid: "unique_idx (gs @ ab gs bs hs data') (snd (rc, data'))"
unfolding snd_conv by (rule unique_idx_ab)
ultimately show ?case using _ _ rec2.prems(8, 9, 10, 11)
proof (rule rec2.hyps(8), simp only: ab_specD1[OF ab] Un_assoc[symmetric])
define ps' where "ps' = ap gs bs (ps -- sps) hs data'"
fix B a b
assume B_sup: "set gs ∪ set bs ∪ set hs ⊆ B"
hence "set gs ∪ set bs ⊆ B" and "set hs ⊆ B" by simp_all
assume "(a, b) ∈⇩p D'"
hence ab_cases: "(a, b) ∈⇩p D ∨ (a, b) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs) -⇩p set ps' ∨
(a, b) ∈⇩p set (ps -- sps) -⇩p set ps'" by (auto simp: rec2.hyps(7) ps'_def)
assume B_sub: "fst ` B ⊆ dgrad_p_set d m" and "fst a ≠ 0" and "fst b ≠ 0"
assume *: "⋀x y. x ∈ set gs ∪ set bs ∪ set hs ⟹ y ∈ set gs ∪ set bs ∪ set hs ⟹
(x, y) ∉⇩p D' ⟹ fst x ≠ 0 ⟹ fst y ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)"
from rec2.prems(2) have ps_sps_sub: "set (ps -- sps) ⊆ set bs × (set gs ∪ set bs)"
by (auto simp: set_diff_list)
from uid have uid': "unique_idx (gs @ bs @ hs) data'" by (simp add: unique_idx_def ab_specD1[OF ab])
have a: "crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)"
if "fst x ≠ 0" and "fst y ≠ 0" and xy_in: "(x, y) ∈⇩p set (ps -- sps) -⇩p set ps'" for x y
proof (cases "x = y")
case True
from xy_in rec2.prems(2) have "y ∈ set gs ∪ set bs"
unfolding in_pair_minus_pairs unfolding True in_pair_iff set_diff_list by auto
hence "fst y ∈ fst ` set gs ∪ fst ` set bs" by fastforce
from this assms(4) rec2.prems(1) have "fst y ∈ dgrad_p_set d m" by blast
with assms(3) show ?thesis unfolding True by (rule crit_pair_cbelow_same)
next
case False
from ap assms(3) B_sup B_sub ps_sps_sub disj1 uid' assms(5) False ‹fst x ≠ 0› ‹fst y ≠ 0› xy_in
show ?thesis unfolding ps'_def
proof (rule ap_specD3)
fix a1 b1 :: "('t, 'b, 'c) pdata"
assume "fst a1 ≠ 0" and "fst b1 ≠ 0"
assume "a1 ∈ set hs" and b1_in: "b1 ∈ set gs ∪ set bs ∪ set hs"
hence a1_in: "a1 ∈ set gs ∪ set bs ∪ set hs" by fastforce
assume "(a1, b1) ∈⇩p set (ap gs bs (ps -- sps) hs data')"
hence "(a1, b1) ∈⇩p set ps'" by (simp only: ps'_def)
with disj2 have "(a1, b1) ∉⇩p D'" unfolding ps'_def
by (metis empty_iff in_pair_Int_pairs in_pair_alt)
with a1_in b1_in show "crit_pair_cbelow_on d m (fst ` B) (fst a1) (fst b1)"
using ‹fst a1 ≠ 0› ‹fst b1 ≠ 0› by (rule *)
qed
qed
have b: "crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)"
if "(x, y) ∈⇩p D" and "fst x ≠ 0" and "fst y ≠ 0" for x y
using ‹set gs ∪ set bs ⊆ B› B_sub that
proof (rule rec2.prems(6))
fix a1 b1 :: "('t, 'b, 'c) pdata"
assume "a1 ∈ set gs ∪ set bs" and "b1 ∈ set gs ∪ set bs"
hence a1_in: "a1 ∈ set gs ∪ set bs ∪ set hs" and b1_in: "b1 ∈ set gs ∪ set bs ∪ set hs"
by fastforce+
assume "(a1, b1) ∉⇩p D" and "fst a1 ≠ 0" and "fst b1 ≠ 0"
show "crit_pair_cbelow_on d m (fst ` B) (fst a1) (fst b1)"
proof (cases "(a1, b1) ∈⇩p ?X -⇩p set ps'")
case True
moreover from ‹a1 ∈ set gs ∪ set bs› ‹b1 ∈ set gs ∪ set bs› disj1
have "(a1, b1) ∉⇩p set hs × (set gs ∪ set bs ∪ set hs)"
by (auto simp: in_pair_def)
ultimately have "(a1, b1) ∈⇩p set (ps -- sps) -⇩p set ps'" by auto
with ‹fst a1 ≠ 0› ‹fst b1 ≠ 0› show ?thesis by (rule a)
next
case False
with ‹(a1, b1) ∉⇩p D› have "(a1, b1) ∉⇩p D'" by (auto simp: rec2.hyps(7) ps'_def)
with a1_in b1_in show ?thesis using ‹fst a1 ≠ 0› ‹fst b1 ≠ 0› by (rule *)
qed
qed
have c: "crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)"
if x_in: "x ∈ set gs ∪ set bs ∪ set hs" and y_in: "y ∈ set gs ∪ set bs ∪ set hs"
and xy: "(x, y) ∉⇩p (?X -⇩p set ps')" and "fst x ≠ 0" and "fst y ≠ 0" for x y
proof (cases "(x, y) ∈⇩p D")
case True
thus ?thesis using ‹fst x ≠ 0› ‹fst y ≠ 0› by (rule b)
next
case False
with xy have "(x, y) ∉⇩p D'" unfolding rec2.hyps(7) ps'_def by auto
with x_in y_in show ?thesis using ‹fst x ≠ 0› ‹fst y ≠ 0› by (rule *)
qed
from ab_cases show "crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
proof (elim disjE)
assume "(a, b) ∈⇩p D"
thus ?thesis using ‹fst a ≠ 0› ‹fst b ≠ 0› by (rule b)
next
assume ab_in: "(a, b) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs) -⇩p set ps'"
hence ab_in': "(a, b) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs)" and "(a, b) ∉⇩p set ps'" by simp_all
show ?thesis
proof (cases "a = b")
case True
from ab_in' rec2.prems(2) have "b ∈ set hs" unfolding True in_pair_iff set_diff_list by auto
hence "fst b ∈ fst ` set hs" by fastforce
from this hs_sub have "fst b ∈ dgrad_p_set d m" ..
with assms(3) show ?thesis unfolding True by (rule crit_pair_cbelow_same)
next
case False
from ap assms(3) B_sup B_sub ab_in' ps_sps_sub uid' assms(5) False ‹fst a ≠ 0› ‹fst b ≠ 0›
show ?thesis
proof (rule ap_specD2)
fix x y :: "('t, 'b, 'c) pdata"
assume "(x, y) ∈⇩p set (ap gs bs (ps -- sps) hs data')"
also from ap_sub have "... ⊆ (set bs ∪ set hs) × (set gs ∪ set bs ∪ set hs)"
by (simp only: ab_specD1[OF ab] Un_assoc)
also have "... ⊆ (set gs ∪ set bs ∪ set hs) × (set gs ∪ set bs ∪ set hs)" by fastforce
finally have "(x, y) ∈ (set gs ∪ set bs ∪ set hs) × (set gs ∪ set bs ∪ set hs)"
unfolding in_pair_same .
hence "x ∈ set gs ∪ set bs ∪ set hs" and "y ∈ set gs ∪ set bs ∪ set hs" by simp_all
moreover from ‹(x, y) ∈⇩p set (ap gs bs (ps -- sps) hs data')› have "(x, y) ∉⇩p ?X -⇩p set ps'"
by (simp add: ps'_def)
moreover assume "fst x ≠ 0" and "fst y ≠ 0"
ultimately show "crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)" by (rule c)
next
fix x y :: "('t, 'b, 'c) pdata"
assume "fst x ≠ 0" and "fst y ≠ 0"
assume 1: "x ∈ set gs ∪ set bs" and 2: "y ∈ set gs ∪ set bs"
hence x_in: "x ∈ set gs ∪ set bs ∪ set hs" and y_in: "y ∈ set gs ∪ set bs ∪ set hs" by simp_all
show "crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)"
proof (cases "(x, y) ∈⇩p set (ps -- sps) -⇩p set ps'")
case True
with ‹fst x ≠ 0› ‹fst y ≠ 0› show ?thesis by (rule a)
next
case False
have "(x, y) ∉⇩p set (ps -- sps) ∪ set hs × (set gs ∪ set bs ∪ set hs) -⇩p set ps'"
proof
assume "(x, y) ∈⇩p set (ps -- sps) ∪ set hs × (set gs ∪ set bs ∪ set hs) -⇩p set ps'"
hence "(x, y) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs)" using False
by simp
hence "x ∈ set hs ∨ y ∈ set hs" by (auto simp: in_pair_iff)
with 1 2 disj1 show False by blast
qed
with x_in y_in show ?thesis using ‹fst x ≠ 0› ‹fst y ≠ 0› by (rule c)
qed
qed
qed
next
assume "(a, b) ∈⇩p set (ps -- sps) -⇩p set ps'"
with ‹fst a ≠ 0› ‹fst b ≠ 0› show ?thesis by (rule a)
qed
next
fix x y :: "('t, 'b, 'c) pdata"
let ?res = "gb_schema_dummy (rc, data') D' (ab gs bs hs data') (ap gs bs (ps -- sps) hs data')"
assume "x ∈ set (fst ?res)" and "y ∈ set (fst ?res)" and "(x, y) ∉⇩p snd ?res" and "fst x ≠ 0" and "fst y ≠ 0"
thus "crit_pair_cbelow_on d m (fst ` set (fst ?res)) (fst x) (fst y)" by (rule rec2.prems(7))
qed
qed
corollary gb_schema_dummy_connectible:
assumes "struct_spec sel ap ab compl" and "compl_conn compl" and "dickson_grading d"
and "fst ` set gs ⊆ dgrad_p_set d m" and "is_Groebner_basis (fst ` set gs)"
and "fst ` set bs ⊆ dgrad_p_set d m"
and "set ps ⊆ set bs × (set gs ∪ set bs)" and "D ⊆ (set gs ∪ set bs) × (set gs ∪ set bs)"
and "set ps ∩⇩p D = {}" and "unique_idx (gs @ bs) (snd data)"
and "⋀p q. processed (p, q) (gs @ bs) ps ⟹ (p, q) ∉⇩p D ⟹ fst p ≠ 0 ⟹ fst q ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs)) (fst p) (fst q)"
and "⋀B a b. set gs ∪ set bs ⊆ B ⟹ fst ` B ⊆ dgrad_p_set d m ⟹ (a, b) ∈⇩p D ⟹
fst a ≠ 0 ⟹ fst b ≠ 0 ⟹
(⋀x y. x ∈ set gs ∪ set bs ⟹ y ∈ set gs ∪ set bs ⟹ ¬ (x, y) ∈⇩p D ⟹
fst x ≠ 0 ⟹ fst y ≠ 0 ⟹ crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)) ⟹
crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
assumes "f ∈ set (fst (gb_schema_dummy data D bs ps))"
and "g ∈ set (fst (gb_schema_dummy data D bs ps))"
and "fst f ≠ 0" and "fst g ≠ 0"
shows "crit_pair_cbelow_on d m (fst ` set (fst (gb_schema_dummy data D bs ps))) (fst f) (fst g)"
proof (cases "∃xs. fst (gb_schema_dummy data D bs ps) = full_gb xs")
case True
then obtain xs where xs: "fst (gb_schema_dummy data D bs ps) = full_gb xs" ..
note assms(3)
moreover have "fst ` set (full_gb xs) ⊆ dgrad_p_set d m"
proof (rule dgrad_p_set_le_dgrad_p_set)
have "dgrad_p_set_le d (fst ` set (full_gb xs)) (args_to_set (gs, bs, ps))"
unfolding xs[symmetric] using assms(3, 1) by (rule fst_gb_schema_dummy_dgrad_p_set_le)
also from assms(7) have "... = fst ` set gs ∪ fst ` set bs" by (rule args_to_set_subset_Times)
finally show "dgrad_p_set_le d (fst ` set (full_gb xs)) (fst ` set gs ∪ fst ` set bs)" .
next
from assms(4, 6) show "fst ` set gs ∪ fst ` set bs ⊆ dgrad_p_set d m" by blast
qed
moreover note full_gb_isGB
moreover from assms(13) have "fst f ∈ fst ` set (full_gb xs)" by (simp add: xs)
moreover from assms(14) have "fst g ∈ fst ` set (full_gb xs)" by (simp add: xs)
ultimately show ?thesis using assms(15, 16) unfolding xs
by (rule GB_imp_crit_pair_cbelow_dgrad_p_set)
next
case not_full: False
show ?thesis
proof (cases "(f, g) ∈⇩p snd (gb_schema_dummy data D bs ps)")
case True
from assms(1-10,12) _ not_full True assms(15,16) show ?thesis
proof (rule gb_schema_dummy_connectible2)
fix x y
assume "x ∈ set (fst (gb_schema_dummy data D bs ps))"
and "y ∈ set (fst (gb_schema_dummy data D bs ps))"
and "(x, y) ∉⇩p snd (gb_schema_dummy data D bs ps)"
and "fst x ≠ 0" and "fst y ≠ 0"
with assms(1-7,10,11) not_full
show "crit_pair_cbelow_on d m (fst ` set (fst (gb_schema_dummy data D bs ps))) (fst x) (fst y)"
by (rule gb_schema_dummy_connectible1)
qed
next
case False
from assms(1-7,10,11) not_full assms(13,14) False assms(15,16) show ?thesis
by (rule gb_schema_dummy_connectible1)
qed
qed
lemma fst_gb_schema_dummy_dgrad_p_set_le_init:
assumes "dickson_grading d" and "struct_spec sel ap ab compl"
shows "dgrad_p_set_le d (fst ` set (fst (gb_schema_dummy data D (ab gs [] bs (snd data)) (ap gs [] [] bs (snd data)))))
(fst ` (set gs ∪ set bs))"
proof -
let ?bs = "ab gs [] bs (snd data)"
from assms(2) have ap: "ap_spec ap" and ab: "ab_spec ab" by (rule struct_specD)+
from ap_specD1[OF ap, of gs "[]" "[]" bs]
have *: "set (ap gs [] [] bs (snd data)) ⊆ set ?bs × (set gs ∪ set ?bs)"
by (simp add: ab_specD1[OF ab])
from assms have "dgrad_p_set_le d (fst ` set (fst (gb_schema_dummy data D ?bs (ap gs [] [] bs (snd data)))))
(args_to_set (gs, ?bs, (ap gs [] [] bs (snd data))))"
by (rule fst_gb_schema_dummy_dgrad_p_set_le)
also have "... = fst ` (set gs ∪ set bs)"
by (simp add: args_to_set_subset_Times[OF *] image_Un ab_specD1[OF ab])
finally show ?thesis .
qed
corollary fst_gb_schema_dummy_dgrad_p_set_init:
assumes "dickson_grading d" and "struct_spec sel ap ab compl"
and "fst ` (set gs ∪ set bs) ⊆ dgrad_p_set d m"
shows "fst ` set (fst (gb_schema_dummy (rc, data) D (ab gs [] bs data) (ap gs [] [] bs data))) ⊆ dgrad_p_set d m"
proof (rule dgrad_p_set_le_dgrad_p_set)
let ?data = "(rc, data)"
from assms(1, 2)
have "dgrad_p_set_le d (fst ` set (fst (gb_schema_dummy ?data D (ab gs [] bs (snd ?data)) (ap gs [] [] bs (snd ?data)))))
(fst ` (set gs ∪ set bs))"
by (rule fst_gb_schema_dummy_dgrad_p_set_le_init)
thus "dgrad_p_set_le d (fst ` set (fst (gb_schema_dummy ?data D (ab gs [] bs data) (ap gs [] [] bs data))))
(fst ` (set gs ∪ set bs))"
by (simp only: snd_conv)
qed fact
lemma fst_gb_schema_dummy_components_init:
fixes bs data
defines "bs0 ≡ ab gs [] bs data"
defines "ps0 ≡ ap gs [] [] bs data"
assumes "struct_spec sel ap ab compl"
shows "component_of_term ` Keys (fst ` set (fst (gb_schema_dummy (rc, data) D bs0 ps0))) =
component_of_term ` Keys (fst ` set (gs @ bs))" (is "?l = ?r")
proof -
from assms(3) have ap: "ap_spec ap" and ab: "ab_spec ab" by (rule struct_specD)+
from ap_specD1[OF ap, of gs "[]" "[]" bs]
have *: "set ps0 ⊆ set bs0 × (set gs ∪ set bs0)" by (simp add: ps0_def bs0_def ab_specD1[OF ab])
with assms(3) have "?l = component_of_term ` Keys (args_to_set (gs, bs0, ps0))"
by (rule fst_gb_schema_dummy_components)
also have "... = ?r"
by (simp only: args_to_set_subset_Times[OF *], simp add: ab_specD1[OF ab] bs0_def image_Un)
finally show ?thesis .
qed
lemma fst_gb_schema_dummy_pmdl_init:
fixes bs data
defines "bs0 ≡ ab gs [] bs data"
defines "ps0 ≡ ap gs [] [] bs data"
assumes "struct_spec sel ap ab compl" and "compl_pmdl compl" and "is_Groebner_basis (fst ` set gs)"
and "unique_idx (gs @ bs0) data" and "rem_comps_spec (gs @ bs0) (rc, data)"
shows "pmdl (fst ` set (fst (gb_schema_dummy (rc, data) D bs0 ps0))) =
pmdl (fst ` (set (gs @ bs)))" (is "?l = ?r")
proof -
from assms(3) have ab: "ab_spec ab" by (rule struct_specD3)
let ?data = "(rc, data)"
from assms(6) have "unique_idx (gs @ bs0) (snd ?data)" by (simp only: snd_conv)
from assms(3, 4, 5) _ this assms(7) have "?l = pmdl (fst ` (set (gs @ bs0)))"
proof (rule fst_gb_schema_dummy_pmdl)
from assms(3) have "ap_spec ap" by (rule struct_specD2)
from ap_specD1[OF this, of gs "[]" "[]" bs]
show "set ps0 ⊆ set bs0 × (set gs ∪ set bs0)" by (simp add: ps0_def bs0_def ab_specD1[OF ab])
qed
also have "... = ?r" by (simp add: bs0_def ab_specD1[OF ab])
finally show ?thesis .
qed
lemma fst_gb_schema_dummy_isGB_init:
fixes bs data
defines "bs0 ≡ ab gs [] bs data"
defines "ps0 ≡ ap gs [] [] bs data"
defines "D0 ≡ set bs × (set gs ∪ set bs) -⇩p set ps0"
assumes "struct_spec sel ap ab compl" and "compl_conn compl" and "is_Groebner_basis (fst ` set gs)"
and "unique_idx (gs @ bs0) data" and "rem_comps_spec (gs @ bs0) (rc, data)"
shows "is_Groebner_basis (fst ` set (fst (gb_schema_dummy (rc, data) D0 bs0 ps0)))"
proof -
let ?data = "(rc, data)"
let ?res = "gb_schema_dummy ?data D0 bs0 ps0"
from assms(4) have ap: "ap_spec ap" and ab: "ab_spec ab" by (rule struct_specD2, rule struct_specD3)
have set_bs0: "set bs0 = set bs" by (simp add: bs0_def ab_specD1[OF ab])
from ap_specD1[OF ap, of gs "[]" "[]" bs] have ps0_sub: "set ps0 ⊆ set bs0 × (set gs ∪ set bs0)"
by (simp add: ps0_def set_bs0)
from ex_dgrad obtain d::"'a ⇒ nat" where dg: "dickson_grading d" ..
have "finite (fst ` (set gs ∪ set bs))" by (rule, rule finite_UnI, fact finite_set, fact finite_set)
then obtain m where gs_bs_sub: "fst ` (set gs ∪ set bs) ⊆ dgrad_p_set d m" by (rule dgrad_p_set_exhaust)
with dg assms(4) have "fst ` set (fst ?res) ⊆ dgrad_p_set d m" unfolding bs0_def ps0_def
by (rule fst_gb_schema_dummy_dgrad_p_set_init)
with dg show ?thesis
proof (rule crit_pair_cbelow_imp_GB_dgrad_p_set)
fix p0 q0
assume p0_in: "p0 ∈ fst ` set (fst ?res)" and q0_in: "q0 ∈ fst ` set (fst ?res)"
assume "p0 ≠ 0" and "q0 ≠ 0"
from ‹fst ` (set gs ∪ set bs) ⊆ dgrad_p_set d m›
have "fst ` set gs ⊆ dgrad_p_set d m" and "fst ` set bs ⊆ dgrad_p_set d m"
by (simp_all add: image_Un)
from p0_in obtain p where p_in: "p ∈ set (fst ?res)" and p0: "p0 = fst p" ..
from q0_in obtain q where q_in: "q ∈ set (fst ?res)" and q0: "q0 = fst q" ..
from assms(7) have "unique_idx (gs @ bs0) (snd ?data)" by (simp only: snd_conv)
from assms(4, 5) dg ‹fst ` set gs ⊆ dgrad_p_set d m› assms(6) _ ps0_sub _ _ this _ _ p_in q_in ‹p0 ≠ 0› ‹q0 ≠ 0›
show "crit_pair_cbelow_on d m (fst ` set (fst ?res)) p0 q0" unfolding p0 q0
proof (rule gb_schema_dummy_connectible)
from ‹fst ` set bs ⊆ dgrad_p_set d m› show "fst ` set bs0 ⊆ dgrad_p_set d m"
by (simp only: set_bs0)
next
have "D0 ⊆ set bs × (set gs ∪ set bs)" by (auto simp: assms(3) minus_pairs_def)
also have "... ⊆ (set gs ∪ set bs) × (set gs ∪ set bs)" by fastforce
finally show "D0 ⊆ (set gs ∪ set bs0) × (set gs ∪ set bs0)" by (simp only: set_bs0)
next
show "set ps0 ∩⇩p D0 = {}"
proof
show "set ps0 ∩⇩p D0 ⊆ {}"
proof
fix x
assume "x ∈ set ps0 ∩⇩p D0"
hence "x ∈⇩p set ps0 ∩⇩p D0" by (simp add: in_pair_alt)
thus "x ∈ {}" by (auto simp: assms(3))
qed
qed simp
next
fix p' q'
assume "processed (p', q') (gs @ bs0) ps0"
hence proc: "processed (p', q') (gs @ bs) ps0"
by (simp add: set_bs0 processed_alt)
hence "p' ∈ set gs ∪ set bs" and "q' ∈ set gs ∪ set bs" and "(p', q') ∉⇩p set ps0"
by (auto dest: processedD1 processedD2 processedD3)
assume "(p', q') ∉⇩p D0" and "fst p' ≠ 0" and "fst q' ≠ 0"
have "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs)) (fst p') (fst q')"
proof (cases "p' = q'")
case True
from dg show ?thesis unfolding True
proof (rule crit_pair_cbelow_same)
from ‹q' ∈ set gs ∪ set bs› have "fst q' ∈ fst ` (set gs ∪ set bs)" by simp
from this ‹fst ` (set gs ∪ set bs) ⊆ dgrad_p_set d m› show "fst q' ∈ dgrad_p_set d m" ..
qed
next
case False
show ?thesis
proof (cases "component_of_term (lt (fst p')) = component_of_term (lt (fst q'))")
case True
show ?thesis
proof (cases "p' ∈ set gs ∧ q' ∈ set gs")
case True
note dg ‹fst ` set gs ⊆ dgrad_p_set d m› assms(6)
moreover from True have "fst p' ∈ fst ` set gs" and "fst q' ∈ fst ` set gs" by simp_all
ultimately have "crit_pair_cbelow_on d m (fst ` set gs) (fst p') (fst q')"
using ‹fst p' ≠ 0› ‹fst q' ≠ 0› by (rule GB_imp_crit_pair_cbelow_dgrad_p_set)
moreover have "fst ` set gs ⊆ fst ` (set gs ∪ set bs)" by blast
ultimately show ?thesis by (rule crit_pair_cbelow_mono)
next
case False
with ‹p' ∈ set gs ∪ set bs› ‹q' ∈ set gs ∪ set bs›
have "(p', q') ∈⇩p set bs × (set gs ∪ set bs)" by (auto simp: in_pair_iff)
with ‹(p', q') ∉⇩p D0› have "(p', q') ∈⇩p set ps0" by (simp add: assms(3))
with ‹(p', q') ∉⇩p set ps0› show ?thesis ..
qed
next
case False
thus ?thesis by (rule crit_pair_cbelow_distinct_component)
qed
qed
thus "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs0)) (fst p') (fst q')"
by (simp only: set_bs0)
next
fix B a b
assume "set gs ∪ set bs0 ⊆ B"
hence B_sup: "set gs ∪ set bs ⊆ B" by (simp only: set_bs0)
assume B_sub: "fst ` B ⊆ dgrad_p_set d m"
assume "(a, b) ∈⇩p D0"
hence ab_in: "(a, b) ∈⇩p set bs × (set gs ∪ set bs)" and "(a, b) ∉⇩p set ps0"
by (simp_all add: assms(3))
assume "fst a ≠ 0" and "fst b ≠ 0"
assume *: "⋀x y. x ∈ set gs ∪ set bs0 ⟹ y ∈ set gs ∪ set bs0 ⟹ (x, y) ∉⇩p D0 ⟹
fst x ≠ 0 ⟹ fst y ≠ 0 ⟹ crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)"
show "crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
proof (cases "a = b")
case True
from ab_in have "b ∈ set gs ∪ set bs" unfolding True in_pair_iff set_diff_list by auto
hence "fst b ∈ fst ` (set gs ∪ set bs)" by fastforce
from this gs_bs_sub have "fst b ∈ dgrad_p_set d m" ..
with dg show ?thesis unfolding True by (rule crit_pair_cbelow_same)
next
case False
note ap dg
moreover from B_sup have B_sup': "set gs ∪ set [] ∪ set bs ⊆ B" by simp
moreover note B_sub
moreover from ab_in have "(a, b) ∈⇩p set bs × (set gs ∪ set [] ∪ set bs)" by simp
moreover have "set [] ⊆ set [] × (set gs ∪ set [])" by simp
moreover from assms(7) have "unique_idx (gs @ [] @ bs) data" by (simp add: unique_idx_def set_bs0)
ultimately show ?thesis using assms(6) False ‹fst a ≠ 0› ‹fst b ≠ 0›
proof (rule ap_specD2)
fix x y :: "('t, 'b, 'c) pdata"
assume "(x, y) ∈⇩p set (ap gs [] [] bs data)"
hence "(x, y) ∈⇩p set ps0" by (simp only: ps0_def)
also have "... ⊆ set bs0 × (set gs ∪ set bs0)" by (fact ps0_sub)
also have "... ⊆ (set gs ∪ set bs0) × (set gs ∪ set bs0)" by fastforce
finally have "(x, y) ∈ (set gs ∪ set bs0) × (set gs ∪ set bs0)" by (simp only: in_pair_same)
hence "x ∈ set gs ∪ set bs0" and "y ∈ set gs ∪ set bs0" by simp_all
moreover from ‹(x, y) ∈⇩p set ps0› have "(x, y) ∉⇩p D0" by (simp add: D0_def)
moreover assume "fst x ≠ 0" and "fst y ≠ 0"
ultimately show "crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)" by (rule *)
next
fix x y :: "('t, 'b, 'c) pdata"
assume "x ∈ set gs ∪ set []" and "y ∈ set gs ∪ set []"
hence "fst x ∈ fst ` set gs" and "fst y ∈ fst ` set gs" by simp_all
assume "fst x ≠ 0" and "fst y ≠ 0"
with dg ‹fst ` set gs ⊆ dgrad_p_set d m› assms(6) ‹fst x ∈ fst ` set gs› ‹fst y ∈ fst ` set gs›
have "crit_pair_cbelow_on d m (fst ` set gs) (fst x) (fst y)"
by (rule GB_imp_crit_pair_cbelow_dgrad_p_set)
moreover from B_sup have "fst ` set gs ⊆ fst ` B" by fastforce
ultimately show "crit_pair_cbelow_on d m (fst ` B) (fst x) (fst y)"
by (rule crit_pair_cbelow_mono)
qed
qed
qed
qed
qed
subsubsection ‹Function ‹gb_schema_aux››
function (domintros) gb_schema_aux :: "nat × nat × 'd ⇒ ('t, 'b, 'c) pdata list ⇒
('t, 'b, 'c) pdata_pair list ⇒ ('t, 'b, 'c) pdata list"
where
"gb_schema_aux data bs ps =
(if ps = [] then
gs @ bs
else
(let sps = sel gs bs ps (snd data); ps0 = ps -- sps; aux = compl gs bs ps0 sps (snd data);
remcomps = fst (data) - count_const_lt_components (fst aux) in
(if remcomps = 0 then
full_gb (gs @ bs)
else
let (hs, data') = add_indices aux (snd data) in
gb_schema_aux (remcomps, data') (ab gs bs hs data') (ap gs bs ps0 hs data')
)
)
)"
by pat_completeness auto
text ‹The ‹data› parameter of @{const gb_schema_aux} is a triple ‹(c, i, d)›, where ‹c› is the
number of components ‹cmp› of the input list for which the current basis ‹gs @ bs› does @{emph ‹not›}
yet contain an element whose leading power-product is ‹0› and has component ‹cmp›. As soon as ‹c›
gets ‹0›, the function can return a trivial Gr\"obner basis, since then the submodule generated by
the input list is just the full module. This idea generalizes the well-known fact that if a set of
scalar polynomials contains a non-zero constant, the ideal generated by that set is the whole ring.
‹i› is the total number of polynomials generated during the execution of the function so far; it
is used to attach unique indices to the polynomials for fast equality tests.
‹d›, finally, is some arbitrary data-field that may be used by concrete instances of
@{const gb_schema_aux} for storing information.›
lemma gb_schema_aux_domI1: "gb_schema_aux_dom (data, bs, [])"
by (rule gb_schema_aux.domintros, simp)
lemma gb_schema_aux_domI2:
assumes "struct_spec sel ap ab compl"
shows "gb_schema_aux_dom (data, args)"
proof -
from assms have sel: "sel_spec sel" and ap: "ap_spec ap" and ab: "ab_spec ab" by (rule struct_specD)+
from ex_dgrad obtain d::"'a ⇒ nat" where dg: "dickson_grading d" ..
let ?R = "gb_schema_aux_term d gs"
from dg have "wf ?R" by (rule gb_schema_aux_term_wf)
thus ?thesis
proof (induct args arbitrary: data rule: wf_induct_rule)
fix x data
assume IH: "⋀y data'. (y, x) ∈ ?R ⟹ gb_schema_aux_dom (data', y)"
obtain bs ps where x: "x = (bs, ps)" by (meson case_prodE case_prodI2)
show "gb_schema_aux_dom (data, x)" unfolding x
proof (rule gb_schema_aux.domintros)
fix rc0 n0 data0 hs n1 data1
assume "ps ≠ []"
and hs_data': "(hs, n1, data1) = add_indices (compl gs bs (ps -- sel gs bs ps (n0, data0))
(sel gs bs ps (n0, data0)) (n0, data0)) (n0, data0)"
and data: "data = (rc0, n0, data0)"
define sps where "sps = sel gs bs ps (n0, data0)"
define data' where "data' = (n1, data1)"
define rc where "rc = rc0 - count_const_lt_components (fst (compl gs bs (ps -- sel gs bs ps (n0, data0))
(sel gs bs ps (n0, data0)) (n0, data0)))"
from hs_data' have hs: "hs = fst (add_indices (compl gs bs (ps -- sps) sps (snd data)) (snd data))"
unfolding sps_def data snd_conv by (metis fstI)
show "gb_schema_aux_dom ((rc, data'), ab gs bs hs data', ap gs bs (ps -- sps) hs data')"
proof (rule IH, simp add: x gb_schema_aux_term_def gb_schema_aux_term1_def gb_schema_aux_term2_def, intro conjI)
show "fst ` set (ab gs bs hs data') ⊐p fst ` set bs ∨
ab gs bs hs data' = bs ∧ card (set (ap gs bs (ps -- sps) hs data')) < card (set ps)"
proof (cases "hs = []")
case True
have "ab gs bs hs data' = bs ∧ card (set (ap gs bs (ps -- sps) hs data')) < card (set ps)"
proof (simp only: True, rule)
from ab show "ab gs bs [] data' = bs" by (rule ab_specD2)
next
from sel ‹ps ≠ []› have "sps ≠ []" and "set sps ⊆ set ps"
unfolding sps_def by (rule sel_specD1, rule sel_specD2)
moreover from sel_specD1[OF sel ‹ps ≠ []›] have "set sps ≠ {}" by (simp add: sps_def)
ultimately have "set ps ∩ set sps ≠ {}" by (simp add: inf.absorb_iff2)
hence "set (ps -- sps) ⊂ set ps" unfolding set_diff_list by fastforce
hence "card (set (ps -- sps)) < card (set ps)" by (simp add: psubset_card_mono)
moreover have "card (set (ap gs bs (ps -- sps) [] data')) ≤ card (set (ps -- sps))"
by (rule card_mono, fact finite_set, rule ap_spec_Nil_subset, fact ap)
ultimately show "card (set (ap gs bs (ps -- sps) [] data')) < card (set ps)" by simp
qed
thus ?thesis ..
next
case False
with assms ‹ps ≠ []› sps_def hs have "fst ` set (ab gs bs hs data') ⊐p fst ` set bs"
unfolding data snd_conv by (rule struct_spec_red_supset)
thus ?thesis ..
qed
next
from dg assms ‹ps ≠ []› sps_def hs
show "dgrad_p_set_le d (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) (args_to_set (gs, bs, ps))"
unfolding data snd_conv by (rule dgrad_p_set_le_args_to_set_struct)
next
from assms ‹ps ≠ []› sps_def hs
show "component_of_term ` Keys (args_to_set (gs, ab gs bs hs data', ap gs bs (ps -- sps) hs data')) ⊆
component_of_term ` Keys (args_to_set (gs, bs, ps))"
unfolding data snd_conv by (rule components_subset_struct)
qed
qed
qed
qed
lemma gb_schema_aux_Nil [simp, code]: "gb_schema_aux data bs [] = gs @ bs"
by (simp add: gb_schema_aux.psimps[OF gb_schema_aux_domI1])
lemmas gb_schema_aux_simps = gb_schema_aux.psimps[OF gb_schema_aux_domI2]
lemma gb_schema_aux_induct [consumes 1, case_names base rec1 rec2]:
assumes "struct_spec sel ap ab compl"
assumes base: "⋀bs data. P data bs [] (gs @ bs)"
and rec1: "⋀bs ps sps data. ps ≠ [] ⟹ sps = sel gs bs ps (snd data) ⟹
fst (data) ≤ count_const_lt_components (fst (compl gs bs (ps -- sps) sps (snd data))) ⟹
P data bs ps (full_gb (gs @ bs))"
and rec2: "⋀bs ps sps aux hs rc data data'. ps ≠ [] ⟹ sps = sel gs bs ps (snd data) ⟹
aux = compl gs bs (ps -- sps) sps (snd data) ⟹ (hs, data') = add_indices aux (snd data) ⟹
rc = fst data - count_const_lt_components (fst aux) ⟹ 0 < rc ⟹
P (rc, data') (ab gs bs hs data') (ap gs bs (ps -- sps) hs data')
(gb_schema_aux (rc, data') (ab gs bs hs data') (ap gs bs (ps -- sps) hs data')) ⟹
P data bs ps (gb_schema_aux (rc, data') (ab gs bs hs data') (ap gs bs (ps -- sps) hs data'))"
shows "P data bs ps (gb_schema_aux data bs ps)"
proof -
from assms(1) have "gb_schema_aux_dom (data, bs, ps)" by (rule gb_schema_aux_domI2)
thus ?thesis
proof (induct data bs ps rule: gb_schema_aux.pinduct)
case (1 data bs ps)
show ?case
proof (cases "ps = []")
case True
show ?thesis by (simp add: True, rule base)
next
case False
show ?thesis
proof (simp add: gb_schema_aux_simps[OF assms(1), of data bs ps] False Let_def split: if_split,
intro conjI impI)
define sps where "sps = sel gs bs ps (snd data)"
assume "fst data ≤ count_const_lt_components (fst (compl gs bs (ps -- sps) sps (snd data)))"
with False sps_def show "P data bs ps (full_gb (gs @ bs))" by (rule rec1)
next
define sps where "sps = sel gs bs ps (snd data)"
define aux where "aux = compl gs bs (ps -- sps) sps (snd data)"
define hs where "hs = fst (add_indices aux (snd data))"
define data' where "data' = snd (add_indices aux (snd data))"
define rc where "rc = fst data - count_const_lt_components (fst aux)"
have eq: "add_indices aux (snd data) = (hs, data')" by (simp add: hs_def data'_def)
assume "¬ fst data ≤ count_const_lt_components (fst aux)"
hence "0 < rc" by (simp add: rc_def)
hence "rc ≠ 0" by simp
show "P data bs ps
(case add_indices aux (snd data) of
(hs, data') ⇒ gb_schema_aux (rc, data') (ab gs bs hs data') (ap gs bs (ps -- sps) hs data'))"
unfolding eq prod.case using False sps_def aux_def eq[symmetric] rc_def ‹0 < rc›
proof (rule rec2)
show "P (rc, data') (ab gs bs hs data') (ap gs bs (ps -- sps) hs data')
(gb_schema_aux (rc, data') (ab gs bs hs data') (ap gs bs (ps -- sps) hs data'))"
using False sps_def refl aux_def rc_def ‹rc ≠ 0› eq[symmetric] refl by (rule 1)
qed
qed
qed
qed
qed
lemma gb_schema_dummy_eq_gb_schema_aux:
assumes "struct_spec sel ap ab compl"
shows "fst (gb_schema_dummy data D bs ps) = gb_schema_aux data bs ps"
using assms
proof (induct data D bs ps rule: gb_schema_dummy_induct)
case (base bs data D)
show ?case by simp
next
case (rec1 bs ps sps data D)
thus ?case by (simp add: gb_schema_aux.psimps[OF gb_schema_aux_domI2, OF assms])
next
case (rec2 bs ps sps aux hs rc data data' D D')
note rec2.hyps(8)
also from rec2.hyps(1, 2, 3) rec2.hyps(4)[symmetric] rec2.hyps(5, 6, 7)
have "gb_schema_aux (rc, data') (ab gs bs hs data') (ap gs bs (ps -- sps) hs data') =
gb_schema_aux data bs ps"
by (simp add: gb_schema_aux.psimps[OF gb_schema_aux_domI2, OF assms, of data] Let_def)
finally show ?case .
qed
corollary gb_schema_aux_dgrad_p_set_le:
assumes "dickson_grading d" and "struct_spec sel ap ab compl"
shows "dgrad_p_set_le d (fst ` set (gb_schema_aux data bs ps)) (args_to_set (gs, bs, ps))"
using fst_gb_schema_dummy_dgrad_p_set_le[OF assms] unfolding gb_schema_dummy_eq_gb_schema_aux[OF assms(2)] .
corollary gb_schema_aux_components:
assumes "struct_spec sel ap ab compl" and "set ps ⊆ set bs × (set gs ∪ set bs)"
shows "component_of_term ` Keys (fst ` set (gb_schema_aux data bs ps)) =
component_of_term ` Keys (args_to_set (gs, bs, ps))"
using fst_gb_schema_dummy_components[OF assms] unfolding gb_schema_dummy_eq_gb_schema_aux[OF assms(1)] .
lemma gb_schema_aux_pmdl:
assumes "struct_spec sel ap ab compl" and "compl_pmdl compl" and "is_Groebner_basis (fst ` set gs)"
and "set ps ⊆ set bs × (set gs ∪ set bs)" and "unique_idx (gs @ bs) (snd data)"
and "rem_comps_spec (gs @ bs) data"
shows "pmdl (fst ` set (gb_schema_aux data bs ps)) = pmdl (fst ` set (gs @ bs))"
using fst_gb_schema_dummy_pmdl[OF assms] unfolding gb_schema_dummy_eq_gb_schema_aux[OF assms(1)] .
corollary gb_schema_aux_dgrad_p_set_le_init:
assumes "dickson_grading d" and "struct_spec sel ap ab compl"
shows "dgrad_p_set_le d (fst ` set (gb_schema_aux data (ab gs [] bs (snd data)) (ap gs [] [] bs (snd data))))
(fst ` (set gs ∪ set bs))"
using fst_gb_schema_dummy_dgrad_p_set_le_init[OF assms] unfolding gb_schema_dummy_eq_gb_schema_aux[OF assms(2)] .
corollary gb_schema_aux_dgrad_p_set_init:
assumes "dickson_grading d" and "struct_spec sel ap ab compl"
and "fst ` (set gs ∪ set bs) ⊆ dgrad_p_set d m"
shows "fst ` set (gb_schema_aux (rc, data) (ab gs [] bs data) (ap gs [] [] bs data)) ⊆ dgrad_p_set d m"
using fst_gb_schema_dummy_dgrad_p_set_init[OF assms] unfolding gb_schema_dummy_eq_gb_schema_aux[OF assms(2)] .
corollary gb_schema_aux_components_init:
assumes "struct_spec sel ap ab compl"
shows "component_of_term ` Keys (fst ` set (gb_schema_aux (rc, data) (ab gs [] bs data) (ap gs [] [] bs data))) =
component_of_term ` Keys (fst ` set (gs @ bs))"
using fst_gb_schema_dummy_components_init[OF assms] unfolding gb_schema_dummy_eq_gb_schema_aux[OF assms] .
corollary gb_schema_aux_pmdl_init:
assumes "struct_spec sel ap ab compl" and "compl_pmdl compl" and "is_Groebner_basis (fst ` set gs)"
and "unique_idx (gs @ ab gs [] bs data) data" and "rem_comps_spec (gs @ ab gs [] bs data) (rc, data)"
shows "pmdl (fst ` set (gb_schema_aux (rc, data) (ab gs [] bs data) (ap gs [] [] bs data))) =
pmdl (fst ` (set (gs @ bs)))"
using fst_gb_schema_dummy_pmdl_init[OF assms] unfolding gb_schema_dummy_eq_gb_schema_aux[OF assms(1)] .
lemma gb_schema_aux_isGB_init:
assumes "struct_spec sel ap ab compl" and "compl_conn compl" and "is_Groebner_basis (fst ` set gs)"
and "unique_idx (gs @ ab gs [] bs data) data" and "rem_comps_spec (gs @ ab gs [] bs data) (rc, data)"
shows "is_Groebner_basis (fst ` set (gb_schema_aux (rc, data) (ab gs [] bs data) (ap gs [] [] bs data)))"
using fst_gb_schema_dummy_isGB_init[OF assms] unfolding gb_schema_dummy_eq_gb_schema_aux[OF assms(1)] .
end
subsubsection ‹Functions ‹gb_schema_direct› and ‹term gb_schema_incr››
definition gb_schema_direct :: "('t, 'b, 'c, 'd) selT ⇒ ('t, 'b, 'c, 'd) apT ⇒ ('t, 'b, 'c, 'd) abT ⇒
('t, 'b, 'c, 'd) complT ⇒ ('t, 'b, 'c) pdata' list ⇒ 'd ⇒
('t, 'b::field, 'c::default) pdata' list"
where "gb_schema_direct sel ap ab compl bs0 data0 =
(let data = (length bs0, data0); bs1 = fst (add_indices (bs0, data0) (0, data0));
bs = ab [] [] bs1 data in
map (λ(f, _, d). (f, d))
(gb_schema_aux sel ap ab compl [] (count_rem_components bs, data) bs (ap [] [] [] bs1 data))
)"
primrec gb_schema_incr :: "('t, 'b, 'c, 'd) selT ⇒ ('t, 'b, 'c, 'd) apT ⇒ ('t, 'b, 'c, 'd) abT ⇒
('t, 'b, 'c, 'd) complT ⇒
(('t, 'b, 'c) pdata list ⇒ ('t, 'b, 'c) pdata ⇒ 'd ⇒ 'd) ⇒
('t, 'b, 'c) pdata' list ⇒ 'd ⇒ ('t, 'b::field, 'c::default) pdata' list"
where
"gb_schema_incr _ _ _ _ _ [] _ = []"|
"gb_schema_incr sel ap ab compl upd (b0 # bs) data =
(let (gs, n, data') = add_indices (gb_schema_incr sel ap ab compl upd bs data, data) (0, data);
b = (fst b0, n, snd b0); data'' = upd gs b data' in
map (λ(f, _, d). (f, d))
(gb_schema_aux sel ap ab compl gs (count_rem_components (b # gs), Suc n, data'')
(ab gs [] [b] (Suc n, data'')) (ap gs [] [] [b] (Suc n, data'')))
)"
lemma (in -) fst_set_drop_indices:
"fst ` (λ(f, _, d). (f, d)) ` A = fst ` A" for A::"('x × 'y × 'z) set"
by (simp add: image_image, rule image_cong, fact refl, simp add: prod.case_eq_if)
lemma fst_gb_schema_direct:
"fst ` set (gb_schema_direct sel ap ab compl bs0 data0) =
(let data = (length bs0, data0); bs1 = fst (add_indices (bs0, data0) (0, data0)); bs = ab [] [] bs1 data in
fst ` set (gb_schema_aux sel ap ab compl [] (count_rem_components bs, data)
bs (ap [] [] [] bs1 data))
)"
by (simp add: gb_schema_direct_def Let_def fst_set_drop_indices)
lemma gb_schema_direct_dgrad_p_set:
assumes "dickson_grading d" and "struct_spec sel ap ab compl" and "fst ` set bs ⊆ dgrad_p_set d m"
shows "fst ` set (gb_schema_direct sel ap ab compl bs data) ⊆ dgrad_p_set d m"
unfolding fst_gb_schema_direct Let_def using assms(1, 2)
proof (rule gb_schema_aux_dgrad_p_set_init)
show "fst ` (set [] ∪ set (fst (add_indices (bs, data) (0, data)))) ⊆ dgrad_p_set d m"
using assms(3) by (simp add: image_Un fst_set_add_indices)
qed
theorem gb_schema_direct_isGB:
assumes "struct_spec sel ap ab compl" and "compl_conn compl"
shows "is_Groebner_basis (fst ` set (gb_schema_direct sel ap ab compl bs data))"
unfolding fst_gb_schema_direct Let_def using assms
proof (rule gb_schema_aux_isGB_init)
from is_Groebner_basis_empty show "is_Groebner_basis (fst ` set [])" by simp
next
let ?data = "(length bs, data)"
from assms(1) have "ab_spec ab" by (rule struct_specD)
moreover have "unique_idx ([] @ []) (0, data)" by (simp add: unique_idx_Nil)
ultimately show "unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) ?data) ?data"
proof (rule unique_idx_ab)
show "(fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices (bs, data) (0, data)"
by (simp add: add_indices_def)
qed
qed (simp add: rem_comps_spec_count_rem_components)
theorem gb_schema_direct_pmdl:
assumes "struct_spec sel ap ab compl" and "compl_pmdl compl"
shows "pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) = pmdl (fst ` set bs)"
proof -
have "pmdl (fst ` set (gb_schema_direct sel ap ab compl bs data)) =
pmdl (fst ` set ([] @ (fst (add_indices (bs, data) (0, data)))))"
unfolding fst_gb_schema_direct Let_def using assms
proof (rule gb_schema_aux_pmdl_init)
from is_Groebner_basis_empty show "is_Groebner_basis (fst ` set [])" by simp
next
let ?data = "(length bs, data)"
from assms(1) have "ab_spec ab" by (rule struct_specD)
moreover have "unique_idx ([] @ []) (0, data)" by (simp add: unique_idx_Nil)
ultimately show "unique_idx ([] @ ab [] [] (fst (add_indices (bs, data) (0, data))) ?data) ?data"
proof (rule unique_idx_ab)
show "(fst (add_indices (bs, data) (0, data)), length bs, data) = add_indices (bs, data) (0, data)"
by (simp add: add_indices_def)
qed
qed (simp add: rem_comps_spec_count_rem_components)
thus ?thesis by (simp add: fst_set_add_indices)
qed
lemma fst_gb_schema_incr:
"fst ` set (gb_schema_incr sel ap ab compl upd (b0 # bs) data) =
(let (gs, n, data') = add_indices (gb_schema_incr sel ap ab compl upd bs data, data) (0, data);
b = (fst b0, n, snd b0); data'' = upd gs b data' in
fst ` set (gb_schema_aux sel ap ab compl gs (count_rem_components (b # gs), Suc n, data'')
(ab gs [] [b] (Suc n, data'')) (ap gs [] [] [b] (Suc n, data'')))
)"
by (simp only: gb_schema_incr.simps Let_def prod.case_distrib[of set]
prod.case_distrib[of "image fst"] set_map fst_set_drop_indices)
lemma gb_schema_incr_dgrad_p_set:
assumes "dickson_grading d" and "struct_spec sel ap ab compl"
and "fst ` set bs ⊆ dgrad_p_set d m"
shows "fst ` set (gb_schema_incr sel ap ab compl upd bs data) ⊆ dgrad_p_set d m"
using assms(3)
proof (induct bs)
case Nil
show ?case by simp
next
case (Cons b0 bs)
from Cons(2) have 1: "fst b0 ∈ dgrad_p_set d m" and 2: "fst ` set bs ⊆ dgrad_p_set d m" by simp_all
show ?case
proof (simp only: fst_gb_schema_incr Let_def split: prod.splits, simp, intro allI impI)
fix gs n data'
assume "add_indices (gb_schema_incr sel ap ab compl upd bs data, data) (0, data) = (gs, n, data')"
hence gs: "gs = fst (add_indices (gb_schema_incr sel ap ab compl upd bs data, data) (0, data))" by simp
define b where "b = (fst b0, n, snd b0)"
define data'' where "data'' = upd gs b data'"
from assms(1, 2)
show "fst ` set (gb_schema_aux sel ap ab compl gs (count_rem_components (b # gs), Suc n, data'')
(ab gs [] [b] (Suc n, data'')) (ap gs [] [] [b] (Suc n, data''))) ⊆ dgrad_p_set d m"
proof (rule gb_schema_aux_dgrad_p_set_init)
from 1 Cons(1)[OF 2] show "fst ` (set gs ∪ set [b]) ⊆ dgrad_p_set d m"
by (simp add: gs fst_set_add_indices b_def)
qed
qed
qed
theorem gb_schema_incr_dgrad_p_set_isGB:
assumes "struct_spec sel ap ab compl" and "compl_conn compl"
shows "is_Groebner_basis (fst ` set (gb_schema_incr sel ap ab compl upd bs data))"
proof (induct bs)
case Nil
from is_Groebner_basis_empty show ?case by simp
next
case (Cons b0 bs)
show ?case
proof (simp only: fst_gb_schema_incr Let_def split: prod.splits, simp, intro allI impI)
fix gs n data'
assume *: "add_indices (gb_schema_incr sel ap ab compl upd bs data, data) (0, data) = (gs, n, data')"
hence gs: "gs = fst (add_indices (gb_schema_incr sel ap ab compl upd bs data, data) (0, data))" by simp
define b where "b = (fst b0, n, snd b0)"
define data'' where "data'' = upd gs b data'"
from assms(1) have ab: "ab_spec ab" by (rule struct_specD3)
from Cons have "is_Groebner_basis (fst ` set gs)" by (simp add: gs fst_set_add_indices)
with assms
show "is_Groebner_basis (fst ` set (gb_schema_aux sel ap ab compl gs (count_rem_components (b # gs), Suc n, data'')
(ab gs [] [b] (Suc n, data'')) (ap gs [] [] [b] (Suc n, data''))))"
proof (rule gb_schema_aux_isGB_init)
from ab show "unique_idx (gs @ ab gs [] [b] (Suc n, data'')) (Suc n, data'')"
proof (rule unique_idx_ab)
from unique_idx_Nil *[symmetric] have "unique_idx ([] @ gs) (n, data')"
by (rule unique_idx_append)
thus "unique_idx (gs @ []) (n, data')" by simp
next
show "([b], Suc n, data'') = add_indices ([b0], data'') (n, data')"
by (simp add: add_indices_def b_def)
qed
next
have "rem_comps_spec (b # gs) (count_rem_components (b # gs), Suc n, data'')"
by (fact rem_comps_spec_count_rem_components)
moreover have "set (b # gs) = set (gs @ ab gs [] [b] (Suc n, data''))"
by (simp add: ab_specD1[OF ab])
ultimately show "rem_comps_spec (gs @ ab gs [] [b] (Suc n, data''))
(count_rem_components (b # gs), Suc n, data'')"
by (simp only: rem_comps_spec_def)
qed
qed
qed
theorem gb_schema_incr_pmdl:
assumes "struct_spec sel ap ab compl" and "compl_conn compl" "compl_pmdl compl"
shows "pmdl (fst ` set (gb_schema_incr sel ap ab compl upd bs data)) = pmdl (fst ` set bs)"
proof (induct bs)
case Nil
show ?case by simp
next
case (Cons b0 bs)
show ?case
proof (simp only: fst_gb_schema_incr Let_def split: prod.splits, simp, intro allI impI)
fix gs n data'
assume *: "add_indices (gb_schema_incr sel ap ab compl upd bs data, data) (0, data) = (gs, n, data')"
hence gs: "gs = fst (add_indices (gb_schema_incr sel ap ab compl upd bs data, data) (0, data))" by simp
define b where "b = (fst b0, n, snd b0)"
define data'' where "data'' = upd gs b data'"
from assms(1) have ab: "ab_spec ab" by (rule struct_specD3)
from assms(1, 2) have "is_Groebner_basis (fst ` set gs)" unfolding gs fst_conv fst_set_add_indices
by (rule gb_schema_incr_dgrad_p_set_isGB)
with assms(1, 3)
have eq: "pmdl (fst ` set (gb_schema_aux sel ap ab compl gs (count_rem_components (b # gs), Suc n, data'')
(ab gs [] [b] (Suc n, data'')) (ap gs [] [] [b] (Suc n, data'')))) =
pmdl (fst ` set (gs @ [b]))"
proof (rule gb_schema_aux_pmdl_init)
from ab show "unique_idx (gs @ ab gs [] [b] (Suc n, data'')) (Suc n, data'')"
proof (rule unique_idx_ab)
from unique_idx_Nil *[symmetric] have "unique_idx ([] @ gs) (n, data')"
by (rule unique_idx_append)
thus "unique_idx (gs @ []) (n, data')" by simp
next
show "([b], Suc n, data'') = add_indices ([b0], data'') (n, data')"
by (simp add: add_indices_def b_def)
qed
next
have "rem_comps_spec (b # gs) (count_rem_components (b # gs), Suc n, data'')"
by (fact rem_comps_spec_count_rem_components)
moreover have "set (b # gs) = set (gs @ ab gs [] [b] (Suc n, data''))"
by (simp add: ab_specD1[OF ab])
ultimately show "rem_comps_spec (gs @ ab gs [] [b] (Suc n, data''))
(count_rem_components (b # gs), Suc n, data'')"
by (simp only: rem_comps_spec_def)
qed
also have "... = pmdl (insert (fst b) (fst ` set gs))" by simp
also from Cons have "... = pmdl (insert (fst b) (fst ` set bs))"
unfolding gs fst_conv fst_set_add_indices by (rule pmdl.span_insert_cong)
finally show "pmdl (fst ` set (gb_schema_aux sel ap ab compl gs (count_rem_components (b # gs), Suc n, data'')
(ab gs [] [b] (Suc n, data'')) (ap gs [] [] [b] (Suc n, data'')))) =
pmdl (insert (fst b0) (fst ` set bs))" by (simp add: b_def)
qed
qed
subsection ‹Suitable Instances of the @{emph ‹add-pairs›} Parameter›
subsubsection ‹Specification of the @{emph ‹crit›} parameters›
type_synonym (in -) ('t, 'b, 'c, 'd) icritT = "nat × 'd ⇒ ('t, 'b, 'c) pdata list ⇒ ('t, 'b, 'c) pdata list ⇒
('t, 'b, 'c) pdata list ⇒ ('t, 'b, 'c) pdata ⇒ ('t, 'b, 'c) pdata ⇒ bool"
type_synonym (in -) ('t, 'b, 'c, 'd) ncritT = "nat × 'd ⇒ ('t, 'b, 'c) pdata list ⇒ ('t, 'b, 'c) pdata list ⇒
('t, 'b, 'c) pdata list ⇒ bool ⇒
(bool × ('t, 'b, 'c) pdata_pair) list ⇒ ('t, 'b, 'c) pdata ⇒
('t, 'b, 'c) pdata ⇒ bool"
type_synonym (in -) ('t, 'b, 'c, 'd) ocritT = "nat × 'd ⇒ ('t, 'b, 'c) pdata list ⇒
(bool × ('t, 'b, 'c) pdata_pair) list ⇒ ('t, 'b, 'c) pdata ⇒
('t, 'b, 'c) pdata ⇒ bool"
definition icrit_spec :: "('t, 'b::field, 'c, 'd) icritT ⇒ bool"
where "icrit_spec crit ⟷
(∀d m data gs bs hs p q. dickson_grading d ⟶
fst ` (set gs ∪ set bs ∪ set hs) ⊆ dgrad_p_set d m ⟶ unique_idx (gs @ bs @ hs) data ⟶
is_Groebner_basis (fst ` set gs) ⟶ p ∈ set hs ⟶ q ∈ set gs ∪ set bs ∪ set hs ⟶
fst p ≠ 0 ⟶ fst q ≠ 0 ⟶ crit data gs bs hs p q ⟶
crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs ∪ set hs)) (fst p) (fst q))"
text ‹Criteria satisfying @{const icrit_spec} can be used for discarding pairs @{emph ‹instantly›},
without reference to any other pairs.
The product criterion for scalar polynomials satisfies @{const icrit_spec}, and so does the
component criterion (which checks whether the component-indices of the leading terms of two
polynomials are identical).›
definition ncrit_spec :: "('t, 'b::field, 'c, 'd) ncritT ⇒ bool"
where "ncrit_spec crit ⟷
(∀d m data gs bs hs ps B q_in_bs p q. dickson_grading d ⟶ set gs ∪ set bs ∪ set hs ⊆ B ⟶
fst ` B ⊆ dgrad_p_set d m ⟶ snd ` set ps ⊆ set hs × (set gs ∪ set bs ∪ set hs) ⟶
unique_idx (gs @ bs @ hs) data ⟶ is_Groebner_basis (fst ` set gs) ⟶
(q_in_bs ⟶ (q ∈ set gs ∪ set bs)) ⟶
(∀p' q'. (p', q') ∈⇩p snd ` set ps ⟶ fst p' ≠ 0 ⟶ fst q' ≠ 0 ⟶
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')) ⟶
(∀p' q'. p' ∈ set gs ∪ set bs ⟶ q' ∈ set gs ∪ set bs ⟶ fst p' ≠ 0 ⟶ fst q' ≠ 0 ⟶
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')) ⟶
p ∈ set hs ⟶ q ∈ set gs ∪ set bs ∪ set hs ⟶ fst p ≠ 0 ⟶ fst q ≠ 0 ⟶
crit data gs bs hs q_in_bs ps p q ⟶
crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q))"
definition ocrit_spec :: "('t, 'b::field, 'c, 'd) ocritT ⇒ bool"
where "ocrit_spec crit ⟷
(∀d m data hs ps B p q. dickson_grading d ⟶ set hs ⊆ B ⟶ fst ` B ⊆ dgrad_p_set d m ⟶
unique_idx (p # q # hs @ (map (fst ∘ snd) ps) @ (map (snd ∘ snd) ps)) data ⟶
(∀p' q'. (p', q') ∈⇩p snd ` set ps ⟶ fst p' ≠ 0 ⟶ fst q' ≠ 0 ⟶
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')) ⟶
p ∈ B ⟶ q ∈ B ⟶ fst p ≠ 0 ⟶ fst q ≠ 0 ⟶
crit data hs ps p q ⟶ crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q))"
text ‹Criteria satisfying @{const ncrit_spec} can be used for discarding new pairs by reference to
new and old elements, whereas criteria satisfying @{const ocrit_spec} can be used for
discarding old pairs by reference to new elements @{emph ‹only›} (no existing ones!).
The chain criterion satisfies both @{const ncrit_spec} and @{const ocrit_spec}.›
lemma icrit_specI:
assumes "⋀d m data gs bs hs p q.
dickson_grading d ⟹ fst ` (set gs ∪ set bs ∪ set hs) ⊆ dgrad_p_set d m ⟹
unique_idx (gs @ bs @ hs) data ⟹ is_Groebner_basis (fst ` set gs) ⟹
p ∈ set hs ⟹ q ∈ set gs ∪ set bs ∪ set hs ⟹ fst p ≠ 0 ⟹ fst q ≠ 0 ⟹
crit data gs bs hs p q ⟹
crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs ∪ set hs)) (fst p) (fst q)"
shows "icrit_spec crit"
unfolding icrit_spec_def using assms by auto
lemma icrit_specD:
assumes "icrit_spec crit" and "dickson_grading d"
and "fst ` (set gs ∪ set bs ∪ set hs) ⊆ dgrad_p_set d m" and "unique_idx (gs @ bs @ hs) data"
and "is_Groebner_basis (fst ` set gs)" and "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs"
and "fst p ≠ 0" and "fst q ≠ 0" and "crit data gs bs hs p q"
shows "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs ∪ set hs)) (fst p) (fst q)"
using assms unfolding icrit_spec_def by blast
lemma ncrit_specI:
assumes "⋀d m data gs bs hs ps B q_in_bs p q.
dickson_grading d ⟹ set gs ∪ set bs ∪ set hs ⊆ B ⟹
fst ` B ⊆ dgrad_p_set d m ⟹ snd ` set ps ⊆ set hs × (set gs ∪ set bs ∪ set hs) ⟹
unique_idx (gs @ bs @ hs) data ⟹ is_Groebner_basis (fst ` set gs) ⟹
(q_in_bs ⟶ q ∈ set gs ∪ set bs) ⟹
(⋀p' q'. (p', q') ∈⇩p snd ` set ps ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')) ⟹
(⋀p' q'. p' ∈ set gs ∪ set bs ⟹ q' ∈ set gs ∪ set bs ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')) ⟹
p ∈ set hs ⟹ q ∈ set gs ∪ set bs ∪ set hs ⟹ fst p ≠ 0 ⟹ fst q ≠ 0 ⟹
crit data gs bs hs q_in_bs ps p q ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
shows "ncrit_spec crit"
unfolding ncrit_spec_def by (intro allI impI, rule assms, assumption+, meson, meson, assumption+)
lemma ncrit_specD:
assumes "ncrit_spec crit" and "dickson_grading d" and "set gs ∪ set bs ∪ set hs ⊆ B"
and "fst ` B ⊆ dgrad_p_set d m" and "snd ` set ps ⊆ set hs × (set gs ∪ set bs ∪ set hs)"
and "unique_idx (gs @ bs @ hs) data" and "is_Groebner_basis (fst ` set gs)"
and "q_in_bs ⟹ q ∈ set gs ∪ set bs"
and "⋀p' q'. (p', q') ∈⇩p snd ` set ps ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
and "⋀p' q'. p' ∈ set gs ∪ set bs ⟹ q' ∈ set gs ∪ set bs ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
and "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs" and "fst p ≠ 0" and "fst q ≠ 0"
and "crit data gs bs hs q_in_bs ps p q"
shows "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
using assms unfolding ncrit_spec_def by blast
lemma ocrit_specI:
assumes "⋀d m data hs ps B p q.
dickson_grading d ⟹ set hs ⊆ B ⟹ fst ` B ⊆ dgrad_p_set d m ⟹
unique_idx (p # q # hs @ (map (fst ∘ snd) ps) @ (map (snd ∘ snd) ps)) data ⟹
(⋀p' q'. (p', q') ∈⇩p snd ` set ps ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')) ⟹
p ∈ B ⟹ q ∈ B ⟹ fst p ≠ 0 ⟹ fst q ≠ 0 ⟹
crit data hs ps p q ⟹ crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
shows "ocrit_spec crit"
unfolding ocrit_spec_def by (intro allI impI, rule assms, assumption+, meson, assumption+)
lemma ocrit_specD:
assumes "ocrit_spec crit" and "dickson_grading d" and "set hs ⊆ B" and "fst ` B ⊆ dgrad_p_set d m"
and "unique_idx (p # q # hs @ (map (fst ∘ snd) ps) @ (map (snd ∘ snd) ps)) data"
and "⋀p' q'. (p', q') ∈⇩p snd ` set ps ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
and "p ∈ B" and "q ∈ B" and "fst p ≠ 0" and "fst q ≠ 0"
and "crit data hs ps p q"
shows "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
using assms unfolding ocrit_spec_def by blast
subsubsection ‹Suitable instances of the @{emph ‹crit›} parameters›
definition component_crit :: "('t, 'b::zero, 'c, 'd) icritT"
where "component_crit data gs bs hs p q ⟷ (component_of_term (lt (fst p)) ≠ component_of_term (lt (fst q)))"
lemma icrit_spec_component_crit: "icrit_spec (component_crit::('t, 'b::field, 'c, 'd) icritT)"
proof (rule icrit_specI)
fix d m and data::"nat × 'd" and gs bs hs and p q::"('t, 'b, 'c) pdata"
assume "component_crit data gs bs hs p q"
hence "component_of_term (lt (fst p)) ≠ component_of_term (lt (fst q))"
by (simp add: component_crit_def)
thus "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs ∪ set hs)) (fst p) (fst q)"
by (rule crit_pair_cbelow_distinct_component)
qed
text ‹The product criterion is only applicable to scalar polynomials.›
definition product_crit :: "('a, 'b::zero, 'c, 'd) icritT"
where "product_crit data gs bs hs p q ⟷ (gcs (punit.lt (fst p)) (punit.lt (fst q)) = 0)"
lemma (in gd_term) icrit_spec_product_crit: "punit.icrit_spec (product_crit::('a, 'b::field, 'c, 'd) icritT)"
proof (rule punit.icrit_specI)
fix d m and data::"nat × 'd" and gs bs hs and p q::"('a, 'b, 'c) pdata"
assume "product_crit data gs bs hs p q"
hence *: "gcs (punit.lt (fst p)) (punit.lt (fst q)) = 0" by (simp only: product_crit_def)
assume "p ∈ set hs" and q_in: "q ∈ set gs ∪ set bs ∪ set hs" (is "_ ∈ ?B")
assume "dickson_grading d" and sub: "fst ` (set gs ∪ set bs ∪ set hs) ⊆ punit.dgrad_p_set d m"
moreover from ‹p ∈ set hs› have "fst p ∈ fst ` ?B" by simp
moreover from q_in have "fst q ∈ fst ` ?B" by simp
moreover assume "fst p ≠ 0" and "fst q ≠ 0"
ultimately show "punit.crit_pair_cbelow_on d m (fst ` ?B) (fst p) (fst q)"
using * by (rule product_criterion)
qed
text ‹@{const component_crit} and @{const product_crit} ignore the ‹data› parameter.›
fun (in -) pair_in_list :: "(bool × ('a, 'b, 'c) pdata_pair) list ⇒ nat ⇒ nat ⇒ bool" where
"pair_in_list [] _ _ = False"
|"pair_in_list ((_, (_, i', _), (_, j', _)) # ps) i j =
((i = i' ∧ j = j') ∨ (i = j' ∧ j = i') ∨ pair_in_list ps i j)"
lemma (in -) pair_in_listE:
assumes "pair_in_list ps i j"
obtains p q a b where "((p, i, a), (q, j, b)) ∈⇩p snd ` set ps"
using assms
proof (induct ps i j arbitrary: thesis rule: pair_in_list.induct)
case (1 i j)
from 1(2) show ?case by simp
next
case (2 c p i' a q j' b ps i j)
from 2(3) have "(i = i' ∧ j = j') ∨ (i = j' ∧ j = i') ∨ pair_in_list ps i j" by simp
thus ?case
proof (elim disjE conjE)
assume "i = i'" and "j = j'"
have "((p, i, a), (q, j, b)) ∈⇩p snd ` set ((c, (p, i', a), q, j', b) # ps)"
unfolding ‹i = i'› ‹j = j'› in_pair_iff by fastforce
thus ?thesis by (rule 2(2))
next
assume "i = j'" and "j = i'"
have "((q, i, b), (p, j, a)) ∈⇩p snd ` set ((c, (p, i', a), q, j', b) # ps)"
unfolding ‹i = j'› ‹j = i'› in_pair_iff by fastforce
thus ?thesis by (rule 2(2))
next
assume "pair_in_list ps i j"
obtain p' q' a' b' where "((p', i, a'), (q', j, b')) ∈⇩p snd ` set ps"
by (rule 2(1), assumption, rule ‹pair_in_list ps i j›)
also have "... ⊆ snd ` set ((c, (p, i', a), q, j', b) # ps)" by auto
finally show ?thesis by (rule 2(2))
qed
qed
definition chain_ncrit :: "('t, 'b::zero, 'c, 'd) ncritT"
where "chain_ncrit data gs bs hs q_in_bs ps p q ⟷
(let v = lt (fst p); l = term_of_pair (lcs (pp_of_term v) (lp (fst q)), component_of_term v);
i = fst (snd p); j = fst (snd q) in
(∃r∈set gs. let k = fst (snd r) in
k ≠ i ∧ k ≠ j ∧ lt (fst r) adds⇩t l ∧ pair_in_list ps i k ∧ (q_in_bs ∨ pair_in_list ps j k) ∧ fst r ≠ 0) ∨
(∃r∈set bs. let k = fst (snd r) in
k ≠ i ∧ k ≠ j ∧ lt (fst r) adds⇩t l ∧ pair_in_list ps i k ∧ (q_in_bs ∨ pair_in_list ps j k) ∧ fst r ≠ 0) ∨
(∃h∈set hs. let k = fst (snd h) in
k ≠ i ∧ k ≠ j ∧ lt (fst h) adds⇩t l ∧ pair_in_list ps i k ∧ pair_in_list ps j k ∧ fst h ≠ 0))"
definition chain_ocrit :: "('t, 'b::zero, 'c, 'd) ocritT"
where "chain_ocrit data hs ps p q ⟷
(let v = lt (fst p); l = term_of_pair (lcs (pp_of_term v) (lp (fst q)), component_of_term v);
i = fst (snd p); j = fst (snd q) in
(∃h∈set hs. let k = fst (snd h) in
k ≠ i ∧ k ≠ j ∧ lt (fst h) adds⇩t l ∧ pair_in_list ps i k ∧ pair_in_list ps j k ∧ fst h ≠ 0))"
text ‹@{const chain_ncrit} and @{const chain_ocrit} ignore the ‹data› parameter.›
lemma chain_ncritE:
assumes "chain_ncrit data gs bs hs q_in_bs ps p q" and "snd ` set ps ⊆ set hs × (set gs ∪ set bs ∪ set hs)"
and "unique_idx (gs @ bs @ hs) data" and "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs"
obtains r where "r ∈ set gs ∪ set bs ∪ set hs" and "fst r ≠ 0" and "r ≠ p" and "r ≠ q"
and "lt (fst r) adds⇩t term_of_pair (lcs (lp (fst p)) (lp (fst q)), component_of_term (lt (fst p)))"
and "(p, r) ∈⇩p snd ` set ps" and "(r ∈ set gs ∪ set bs ∧ q_in_bs) ∨ (q, r) ∈⇩p snd ` set ps"
proof -
let ?l = "term_of_pair (lcs (lp (fst p)) (lp (fst q)), component_of_term (lt (fst p)))"
let ?i = "fst (snd p)"
let ?j = "fst (snd q)"
let ?xs = "gs @ bs @ hs"
have 3: "x ∈ set ?xs" if "(x, y) ∈⇩p snd ` set ps" for x y
proof -
note that
also have "snd ` set ps ⊆ set hs × (set gs ∪ set bs ∪ set hs)" by (fact assms(2))
also have "... ⊆ (set gs ∪ set bs ∪ set hs) × (set gs ∪ set bs ∪ set hs)" by fastforce
finally have "(x, y) ∈ (set gs ∪ set bs ∪ set hs) × (set gs ∪ set bs ∪ set hs)"
by (simp only: in_pair_same)
thus ?thesis by simp
qed
have 4: "x ∈ set ?xs" if "(y, x) ∈⇩p snd ` set ps" for x y
proof -
from that have "(x, y) ∈⇩p snd ` set ps" by (simp add: in_pair_iff disj_commute)
thus ?thesis by (rule 3)
qed
from assms(1) have
"∃r ∈ set gs ∪ set bs ∪ set hs. let k = fst (snd r) in
k ≠ ?i ∧ k ≠ ?j ∧ lt (fst r) adds⇩t ?l ∧ pair_in_list ps ?i k ∧
((r ∈ set gs ∪ set bs ∧ q_in_bs) ∨ pair_in_list ps ?j k) ∧ fst r ≠ 0"
by (smt UnI1 chain_ncrit_def sup_commute)
then obtain r where r_in: "r ∈ set gs ∪ set bs ∪ set hs" and "fst r ≠ 0" and rp: "fst (snd r) ≠ ?i"
and rq: "fst (snd r) ≠ ?j" and "lt (fst r) adds⇩t ?l"
and 1: "pair_in_list ps ?i (fst (snd r))"
and 2: "(r ∈ set gs ∪ set bs ∧ q_in_bs) ∨ pair_in_list ps ?j (fst (snd r))"
unfolding Let_def by blast
let ?k = "fst (snd r)"
note r_in ‹fst r ≠ 0›
moreover from rp have "r ≠ p" by auto
moreover from rq have "r ≠ q" by auto
ultimately show ?thesis using ‹lt (fst r) adds⇩t ?l›
proof
from 1 obtain p' r' a b where *: "((p', ?i, a), (r', ?k, b)) ∈⇩p snd ` set ps"
by (rule pair_in_listE)
note assms(3)
moreover from * have "(p', ?i, a) ∈ set ?xs" by (rule 3)
moreover from assms(4) have "p ∈ set ?xs" by simp
moreover have "fst (snd (p', ?i, a)) = ?i" by simp
ultimately have p': "(p', ?i, a) = p" by (rule unique_idxD1)
note assms(3)
moreover from * have "(r', ?k, b) ∈ set ?xs" by (rule 4)
moreover from r_in have "r ∈ set ?xs" by simp
moreover have "fst (snd (r', ?k, b)) = ?k" by simp
ultimately have r': "(r', ?k, b) = r" by (rule unique_idxD1)
from * show "(p, r) ∈⇩p snd ` set ps" by (simp only: p' r')
next
from 2 show "(r ∈ set gs ∪ set bs ∧ q_in_bs) ∨ (q, r) ∈⇩p snd ` set ps"
proof
assume "r ∈ set gs ∪ set bs ∧ q_in_bs"
thus ?thesis ..
next
assume "pair_in_list ps ?j ?k"
then obtain q' r' a b where *: "((q', ?j, a), (r', ?k, b)) ∈⇩p snd ` set ps"
by (rule pair_in_listE)
note assms(3)
moreover from * have "(q', ?j, a) ∈ set ?xs" by (rule 3)
moreover from assms(5) have "q ∈ set ?xs" by simp
moreover have "fst (snd (q', ?j, a)) = ?j" by simp
ultimately have q': "(q', ?j, a) = q" by (rule unique_idxD1)
note assms(3)
moreover from * have "(r', ?k, b) ∈ set ?xs" by (rule 4)
moreover from r_in have "r ∈ set ?xs" by simp
moreover have "fst (snd (r', ?k, b)) = ?k" by simp
ultimately have r': "(r', ?k, b) = r" by (rule unique_idxD1)
from * have "(q, r) ∈⇩p snd ` set ps" by (simp only: q' r')
thus ?thesis ..
qed
qed
qed
lemma chain_ocritE:
assumes "chain_ocrit data hs ps p q"
and "unique_idx (p # q # hs @ (map (fst ∘ snd) ps) @ (map (snd ∘ snd) ps)) data" (is "unique_idx ?xs _")
obtains h where "h ∈ set hs" and "fst h ≠ 0" and "h ≠ p" and "h ≠ q"
and "lt (fst h) adds⇩t term_of_pair (lcs (lp (fst p)) (lp (fst q)), component_of_term (lt (fst p)))"
and "(p, h) ∈⇩p snd ` set ps" and "(q, h) ∈⇩p snd ` set ps"
proof -
let ?l = "term_of_pair (lcs (lp (fst p)) (lp (fst q)), component_of_term (lt (fst p)))"
have 3: "x ∈ set ?xs" if "(x, y) ∈⇩p snd ` set ps" for x y
proof -
from that have "(x, y) ∈ snd ` set ps ∨ (y, x) ∈ snd ` set ps" by (simp only: in_pair_iff)
thus ?thesis
proof
assume "(x, y) ∈ snd ` set ps"
hence "fst (x, y) ∈ fst ` snd ` set ps" by fastforce
thus ?thesis by (simp add: image_comp)
next
assume "(y, x) ∈ snd ` set ps"
hence "snd (y, x) ∈ snd ` snd ` set ps" by fastforce
thus ?thesis by (simp add: image_comp)
qed
qed
have 4: "x ∈ set ?xs" if "(y, x) ∈⇩p snd ` set ps" for x y
proof -
from that have "(x, y) ∈⇩p snd ` set ps" by (simp add: in_pair_iff disj_commute)
thus ?thesis by (rule 3)
qed
from assms(1) obtain h where "h ∈ set hs" and "fst h ≠ 0" and hp: "fst (snd h) ≠ fst (snd p)"
and hq: "fst (snd h) ≠ fst (snd q)" and "lt (fst h) adds⇩t ?l"
and 1: "pair_in_list ps (fst (snd p)) (fst (snd h))" and 2: "pair_in_list ps (fst (snd q)) (fst (snd h))"
unfolding chain_ocrit_def Let_def by blast
let ?i = "fst (snd p)"
let ?j = "fst (snd q)"
let ?k = "fst (snd h)"
note ‹h ∈ set hs› ‹fst h ≠ 0›
moreover from hp have "h ≠ p" by auto
moreover from hq have "h ≠ q" by auto
ultimately show ?thesis using ‹lt (fst h) adds⇩t ?l›
proof
from 1 obtain p' h' a b where *: "((p', ?i, a), (h', ?k, b)) ∈⇩p snd ` set ps"
by (rule pair_in_listE)
note assms(2)
moreover from * have "(p', ?i, a) ∈ set ?xs" by (rule 3)
moreover have "p ∈ set ?xs" by simp
moreover have "fst (snd (p', ?i, a)) = ?i" by simp
ultimately have p': "(p', ?i, a) = p" by (rule unique_idxD1)
note assms(2)
moreover from * have "(h', ?k, b) ∈ set ?xs" by (rule 4)
moreover from ‹h ∈ set hs› have "h ∈ set ?xs" by simp
moreover have "fst (snd (h', ?k, b)) = ?k" by simp
ultimately have h': "(h', ?k, b) = h" by (rule unique_idxD1)
from * show "(p, h) ∈⇩p snd ` set ps" by (simp only: p' h')
next
from 2 obtain q' h' a b where *: "((q', ?j, a), (h', ?k, b)) ∈⇩p snd ` set ps"
by (rule pair_in_listE)
note assms(2)
moreover from * have "(q', ?j, a) ∈ set ?xs" by (rule 3)
moreover have "q ∈ set ?xs" by simp
moreover have "fst (snd (q', ?j, a)) = ?j" by simp
ultimately have q': "(q', ?j, a) = q" by (rule unique_idxD1)
note assms(2)
moreover from * have "(h', ?k, b) ∈ set ?xs" by (rule 4)
moreover from ‹h ∈ set hs› have "h ∈ set ?xs" by simp
moreover have "fst (snd (h', ?k, b)) = ?k" by simp
ultimately have h': "(h', ?k, b) = h" by (rule unique_idxD1)
from * show "(q, h) ∈⇩p snd ` set ps" by (simp only: q' h')
qed
qed
lemma ncrit_spec_chain_ncrit: "ncrit_spec (chain_ncrit::('t, 'b::field, 'c, 'd) ncritT)"
proof (rule ncrit_specI)
fix d m and data::"nat × 'd" and gs bs hs and ps::"(bool × ('t, 'b, 'c) pdata_pair) list"
and B q_in_bs and p q::"('t, 'b, 'c) pdata"
assume dg: "dickson_grading d" and B_sup: "set gs ∪ set bs ∪ set hs ⊆ B"
and B_sub: "fst ` B ⊆ dgrad_p_set d m" and q_in_bs: "q_in_bs ⟶ q ∈ set gs ∪ set bs"
and 1: "⋀p' q'. (p', q') ∈⇩p snd ` set ps ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
and 2: "⋀p' q'. p' ∈ set gs ∪ set bs ⟹ q' ∈ set gs ∪ set bs ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
and "fst p ≠ 0" and "fst q ≠ 0"
let ?l = "term_of_pair (lcs (lp (fst p)) (lp (fst q)), component_of_term (lt (fst p)))"
assume "chain_ncrit data gs bs hs q_in_bs ps p q" and "snd ` set ps ⊆ set hs × (set gs ∪ set bs ∪ set hs)" and
"unique_idx (gs @ bs @ hs) data" and "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs"
then obtain r where "r ∈ set gs ∪ set bs ∪ set hs" and "fst r ≠ 0" and "r ≠ p" and "r ≠ q"
and adds: "lt (fst r) adds⇩t ?l" and "(p, r) ∈⇩p snd ` set ps"
and disj: "(r ∈ set gs ∪ set bs ∧ q_in_bs) ∨ (q, r) ∈⇩p snd ` set ps" by (rule chain_ncritE)
note dg B_sub
moreover from ‹p ∈ set hs› ‹q ∈ set gs ∪ set bs ∪ set hs› B_sup
have "fst p ∈ fst ` B" and "fst q ∈ fst ` B"
by auto
moreover note ‹fst p ≠ 0› ‹fst q ≠ 0›
moreover from adds have "lp (fst r) adds lcs (lp (fst p)) (lp (fst q))"
by (simp add: adds_term_def term_simps)
moreover from adds have "component_of_term (lt (fst r)) = component_of_term (lt (fst p))"
by (simp add: adds_term_def term_simps)
ultimately show "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
proof (rule chain_criterion)
from ‹(p, r) ∈⇩p snd ` set ps› ‹fst p ≠ 0› ‹fst r ≠ 0›
show "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst r)" by (rule 1)
next
from disj show "crit_pair_cbelow_on d m (fst ` B) (fst r) (fst q)"
proof
assume "r ∈ set gs ∪ set bs ∧ q_in_bs"
hence "r ∈ set gs ∪ set bs" and q_in_bs by simp_all
from q_in_bs this(2) have "q ∈ set gs ∪ set bs" ..
with ‹r ∈ set gs ∪ set bs› show ?thesis using ‹fst r ≠ 0› ‹fst q ≠ 0› by (rule 2)
next
assume "(q, r) ∈⇩p snd ` set ps"
hence "(r, q) ∈⇩p snd ` set ps" by (simp only: in_pair_iff disj_commute)
thus ?thesis using ‹fst r ≠ 0› ‹fst q ≠ 0› by (rule 1)
qed
qed
qed
lemma ocrit_spec_chain_ocrit: "ocrit_spec (chain_ocrit::('t, 'b::field, 'c, 'd) ocritT)"
proof (rule ocrit_specI)
fix d m and data::"nat × 'd" and hs::"('t, 'b, 'c) pdata list" and ps::"(bool × ('t, 'b, 'c) pdata_pair) list"
and B and p q::"('t, 'b, 'c) pdata"
assume dg: "dickson_grading d" and B_sup: "set hs ⊆ B"
and B_sub: "fst ` B ⊆ dgrad_p_set d m"
and 1: "⋀p' q'. (p', q') ∈⇩p snd ` set ps ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
and "fst p ≠ 0" and "fst q ≠ 0" and "p ∈ B" and "q ∈ B"
let ?l = "term_of_pair (lcs (lp (fst p)) (lp (fst q)), component_of_term (lt (fst p)))"
assume "chain_ocrit data hs ps p q" and "unique_idx (p # q # hs @ map (fst ∘ snd) ps @ map (snd ∘ snd) ps) data"
then obtain h where "h ∈ set hs" and "fst h ≠ 0" and "h ≠ p" and "h ≠ q"
and adds: "lt (fst h) adds⇩t ?l" and "(p, h) ∈⇩p snd ` set ps" and "(q, h) ∈⇩p snd ` set ps"
by (rule chain_ocritE)
note dg B_sub
moreover from ‹p ∈ B› ‹q ∈ B› B_sup
have "fst p ∈ fst ` B" and "fst q ∈ fst ` B" by auto
moreover note ‹fst p ≠ 0› ‹fst q ≠ 0›
moreover from adds have "lp (fst h) adds lcs (lp (fst p)) (lp (fst q))"
by (simp add: adds_term_def term_simps)
moreover from adds have "component_of_term (lt (fst h)) = component_of_term (lt (fst p))"
by (simp add: adds_term_def term_simps)
ultimately show "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
proof (rule chain_criterion)
from ‹(p, h) ∈⇩p snd ` set ps› ‹fst p ≠ 0› ‹fst h ≠ 0›
show "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst h)" by (rule 1)
next
from ‹(q, h) ∈⇩p snd ` set ps› have "(h, q) ∈⇩p snd ` set ps" by (simp only: in_pair_iff disj_commute)
thus "crit_pair_cbelow_on d m (fst ` B) (fst h) (fst q)" using ‹fst h ≠ 0› ‹fst q ≠ 0› by (rule 1)
qed
qed
lemma icrit_spec_no_crit: "icrit_spec ((λ_ _ _ _ _ _. False)::('t, 'b::field, 'c, 'd) icritT)"
by (rule icrit_specI, simp)
lemma ncrit_spec_no_crit: "ncrit_spec ((λ_ _ _ _ _ _ _ _. False)::('t, 'b::field, 'c, 'd) ncritT)"
by (rule ncrit_specI, simp)
lemma ocrit_spec_no_crit: "ocrit_spec ((λ_ _ _ _ _. False)::('t, 'b::field, 'c, 'd) ocritT)"
by (rule ocrit_specI, simp)
subsubsection ‹Creating Initial List of New Pairs›
type_synonym (in -) ('t, 'b, 'c) apsT = "bool ⇒ ('t, 'b, 'c) pdata list ⇒ ('t, 'b, 'c) pdata list ⇒
('t, 'b, 'c) pdata ⇒ (bool × ('t, 'b, 'c) pdata_pair) list ⇒
(bool × ('t, 'b, 'c) pdata_pair) list"
type_synonym (in -) ('t, 'b, 'c, 'd) npT = "('t, 'b, 'c) pdata list ⇒ ('t, 'b, 'c) pdata list ⇒
('t, 'b, 'c) pdata list ⇒ nat × 'd ⇒
(bool × ('t, 'b, 'c) pdata_pair) list"
definition np_spec :: "('t, 'b, 'c, 'd) npT ⇒ bool"
where "np_spec np ⟷ (∀gs bs hs data.
snd ` set (np gs bs hs data) ⊆ set hs × (set gs ∪ set bs ∪ set hs) ∧
set hs × (set gs ∪ set bs) ⊆ snd ` set (np gs bs hs data) ∧
(∀a b. a ∈ set hs ⟶ b ∈ set hs ⟶ a ≠ b ⟶ (a, b) ∈⇩p snd ` set (np gs bs hs data)) ∧
(∀p q. (True, p, q) ∈ set (np gs bs hs data) ⟶ q ∈ set gs ∪ set bs))"
lemma np_specI:
assumes "⋀gs bs hs data.
snd ` set (np gs bs hs data) ⊆ set hs × (set gs ∪ set bs ∪ set hs) ∧
set hs × (set gs ∪ set bs) ⊆ snd ` set (np gs bs hs data) ∧
(∀a b. a ∈ set hs ⟶ b ∈ set hs ⟶ a ≠ b ⟶ (a, b) ∈⇩p snd ` set (np gs bs hs data)) ∧
(∀p q. (True, p, q) ∈ set (np gs bs hs data) ⟶ q ∈ set gs ∪ set bs)"
shows "np_spec np"
unfolding np_spec_def using assms by meson
lemma np_specD1:
assumes "np_spec np"
shows "snd ` set (np gs bs hs data) ⊆ set hs × (set gs ∪ set bs ∪ set hs)"
using assms[unfolded np_spec_def, rule_format, of gs bs hs data] ..
lemma np_specD2:
assumes "np_spec np"
shows "set hs × (set gs ∪ set bs) ⊆ snd ` set (np gs bs hs data)"
using assms[unfolded np_spec_def, rule_format, of gs bs hs data] by auto
lemma np_specD3:
assumes "np_spec np" and "a ∈ set hs" and "b ∈ set hs" and "a ≠ b"
shows "(a, b) ∈⇩p snd ` set (np gs bs hs data)"
using assms(1)[unfolded np_spec_def, rule_format, of gs bs hs data] assms(2,3,4) by blast
lemma np_specD4:
assumes "np_spec np" and "(True, p, q) ∈ set (np gs bs hs data)"
shows "q ∈ set gs ∪ set bs"
using assms(1)[unfolded np_spec_def, rule_format, of gs bs hs data] assms(2) by blast
lemma np_specE:
assumes "np_spec np" and "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs" and "p ≠ q"
assumes 1: "⋀q_in_bs. (q_in_bs, p, q) ∈ set (np gs bs hs data) ⟹ thesis"
assumes 2: "⋀p_in_bs. (p_in_bs, q, p) ∈ set (np gs bs hs data) ⟹ thesis"
shows thesis
proof (cases "q ∈ set gs ∪ set bs")
case True
with assms(2) have "(p, q) ∈ set hs × (set gs ∪ set bs)" by simp
also from assms(1) have "... ⊆ snd ` set (np gs bs hs data)" by (rule np_specD2)
finally obtain q_in_bs where "(q_in_bs, p, q) ∈ set (np gs bs hs data)" by fastforce
thus ?thesis by (rule 1)
next
case False
with assms(3) have "q ∈ set hs" by simp
from assms(1,2) this assms(4) have "(p, q) ∈⇩p snd ` set (np gs bs hs data)" by (rule np_specD3)
hence "(p, q) ∈ snd ` set (np gs bs hs data) ∨ (q, p) ∈ snd ` set (np gs bs hs data)"
by (simp only: in_pair_iff)
thus ?thesis
proof
assume "(p, q) ∈ snd ` set (np gs bs hs data)"
then obtain q_in_bs where "(q_in_bs, p, q) ∈ set (np gs bs hs data)" by fastforce
thus ?thesis by (rule 1)
next
assume "(q, p) ∈ snd ` set (np gs bs hs data)"
then obtain p_in_bs where "(p_in_bs, q, p) ∈ set (np gs bs hs data)" by fastforce
thus ?thesis by (rule 2)
qed
qed
definition add_pairs_single_naive :: "'d ⇒ ('t, 'b::zero, 'c) apsT"
where "add_pairs_single_naive data flag gs bs h ps = ps @ (map (λg. (flag, h, g)) gs) @ (map (λb. (flag, h, b)) bs)"
lemma set_add_pairs_single_naive:
"set (add_pairs_single_naive data flag gs bs h ps) = set ps ∪ Pair flag ` ({h} × (set gs ∪ set bs))"
by (auto simp add: add_pairs_single_naive_def Let_def)
fun add_pairs_single_sorted :: "((bool × ('t, 'b, 'c) pdata_pair) ⇒ (bool × ('t, 'b, 'c) pdata_pair) ⇒ bool) ⇒
('t, 'b::zero, 'c) apsT" where
"add_pairs_single_sorted _ _ [] [] _ ps = ps"|
"add_pairs_single_sorted rel flag [] (b # bs) h ps =
add_pairs_single_sorted rel flag [] bs h (insort_wrt rel (flag, h, b) ps)"|
"add_pairs_single_sorted rel flag (g # gs) bs h ps =
add_pairs_single_sorted rel flag gs bs h (insort_wrt rel (flag, h, g) ps)"
lemma set_add_pairs_single_sorted:
"set (add_pairs_single_sorted rel flag gs bs h ps) = set ps ∪ Pair flag ` ({h} × (set gs ∪ set bs))"
proof (induct gs arbitrary: ps)
case Nil
show ?case
proof (induct bs arbitrary: ps)
case Nil
show ?case by simp
next
case (Cons b bs)
show ?case by (simp add: Cons)
qed
next
case (Cons g gs)
show ?case by (simp add: Cons)
qed
primrec (in -) pairs :: "('t, 'b, 'c) apsT ⇒ bool ⇒ ('t, 'b, 'c) pdata list ⇒ (bool × ('t, 'b, 'c) pdata_pair) list"
where
"pairs _ _ [] = []"|
"pairs aps flag (x # xs) = aps flag [] xs x (pairs aps flag xs)"
lemma pairs_subset:
assumes "⋀gs bs h ps. set (aps flag gs bs h ps) = set ps ∪ Pair flag ` ({h} × (set gs ∪ set bs))"
shows "set (pairs aps flag xs) ⊆ Pair flag ` (set xs × set xs)"
proof (induct xs)
case Nil
show ?case by simp
next
case (Cons x xs)
from Cons have "set (pairs aps flag xs) ⊆ Pair flag ` (set (x # xs) × set (x # xs))" by fastforce
moreover have "{x} × set xs ⊆ set (x # xs) × set (x # xs)" by fastforce
ultimately show ?case by (auto simp add: assms)
qed
lemma in_pairsI:
assumes "⋀gs bs h ps. set (aps flag gs bs h ps) = set ps ∪ Pair flag ` ({h} × (set gs ∪ set bs))"
and "a ≠ b" and "a ∈ set xs" and "b ∈ set xs"
shows "(flag, a, b) ∈ set (pairs aps flag xs) ∨ (flag, b, a) ∈ set (pairs aps flag xs)"
using assms(3, 4)
proof (induct xs)
case Nil
thus ?case by simp
next
case (Cons x xs)
from Cons(3) have d: "b = x ∨ b ∈ set xs" by simp
from Cons(2) have "a = x ∨ a ∈ set xs" by simp
thus ?case
proof
assume "a = x"
with assms(2) have "b ≠ x" by simp
with d have "b ∈ set xs" by simp
hence "(flag, a, b) ∈ set (pairs aps flag (x # xs))" by (simp add: ‹a = x› assms(1))
thus ?thesis by simp
next
assume "a ∈ set xs"
from d show ?thesis
proof
assume "b = x"
from ‹a ∈ set xs› have "(flag, b, a) ∈ set (pairs aps flag (x # xs))" by (simp add: ‹b = x› assms(1))
thus ?thesis by simp
next
assume "b ∈ set xs"
with ‹a ∈ set xs› have "(flag, a, b) ∈ set (pairs aps flag xs) ∨ (flag, b, a) ∈ set (pairs aps flag xs)"
by (rule Cons(1))
thus ?thesis by (auto simp: assms(1))
qed
qed
qed
corollary in_pairsI':
assumes "⋀gs bs h ps. set (aps flag gs bs h ps) = set ps ∪ Pair flag ` ({h} × (set gs ∪ set bs))"
and "a ∈ set xs" and "b ∈ set xs" and "a ≠ b"
shows "(a, b) ∈⇩p snd ` set (pairs aps flag xs)"
proof -
from assms(1,4,2,3) have "(flag, a, b) ∈ set (pairs aps flag xs) ∨ (flag, b, a) ∈ set (pairs aps flag xs)"
by (rule in_pairsI)
thus ?thesis
proof
assume "(flag, a, b) ∈ set (pairs aps flag xs)"
hence "snd (flag, a, b) ∈ snd ` set (pairs aps flag xs)" by fastforce
thus ?thesis by (simp add: in_pair_iff)
next
assume "(flag, b, a) ∈ set (pairs aps flag xs)"
hence "snd (flag, b, a) ∈ snd ` set (pairs aps flag xs)" by fastforce
thus ?thesis by (simp add: in_pair_iff)
qed
qed
definition new_pairs_naive :: "('t, 'b::zero, 'c, 'd) npT"
where "new_pairs_naive gs bs hs data =
fold (add_pairs_single_naive data True gs bs) hs (pairs (add_pairs_single_naive data) False hs)"
definition new_pairs_sorted :: "(nat × 'd ⇒ (bool × ('t, 'b, 'c) pdata_pair) ⇒ (bool × ('t, 'b, 'c) pdata_pair) ⇒ bool) ⇒
('t, 'b::zero, 'c, 'd) npT"
where "new_pairs_sorted rel gs bs hs data =
fold (add_pairs_single_sorted (rel data) True gs bs) hs (pairs (add_pairs_single_sorted (rel data)) False hs)"
lemma set_fold_aps:
assumes "⋀gs bs h ps. set (aps flag gs bs h ps) = set ps ∪ Pair flag ` ({h} × (set gs ∪ set bs))"
shows "set (fold (aps flag gs bs) hs ps) = Pair flag ` (set hs × (set gs ∪ set bs)) ∪ set ps"
proof (induct hs arbitrary: ps)
case Nil
show ?case by simp
next
case (Cons h hs)
show ?case by (auto simp add: Cons assms)
qed
lemma set_new_pairs_naive:
"set (new_pairs_naive gs bs hs data) =
Pair True ` (set hs × (set gs ∪ set bs)) ∪ set (pairs (add_pairs_single_naive data) False hs)"
proof -
have "set (new_pairs_naive gs bs hs data) =
Pair True ` (set hs × (set gs ∪ set bs)) ∪ set (pairs (add_pairs_single_naive data) False hs)"
unfolding new_pairs_naive_def by (rule set_fold_aps, fact set_add_pairs_single_naive)
thus ?thesis by (simp add: ac_simps)
qed
lemma set_new_pairs_sorted:
"set (new_pairs_sorted rel gs bs hs data) =
Pair True ` (set hs × (set gs ∪ set bs)) ∪ set (pairs (add_pairs_single_sorted (rel data)) False hs)"
proof -
have "set (new_pairs_sorted rel gs bs hs data) =
Pair True ` (set hs × (set gs ∪ set bs)) ∪ set (pairs (add_pairs_single_sorted (rel data)) False hs)"
unfolding new_pairs_sorted_def by (rule set_fold_aps, fact set_add_pairs_single_sorted)
thus ?thesis by (simp add: set_merge_wrt ac_simps)
qed
lemma (in -) fst_snd_Pair [simp]:
shows "fst ∘ Pair x = (λ_. x)" and "snd ∘ Pair x = id"
by auto
lemma np_spec_new_pairs_naive: "np_spec new_pairs_naive"
proof (rule np_specI)
fix gs bs hs :: "('t, 'b, 'c) pdata list" and data::"nat × 'd"
have 1: "set hs × (set gs ∪ set bs) ⊆ set hs × (set gs ∪ set bs ∪ set hs)" by fastforce
have "set (pairs (add_pairs_single_naive data) False hs) ⊆ Pair False ` (set hs × set hs)"
by (rule pairs_subset, simp add: set_add_pairs_single_naive)
hence "snd ` set (pairs (add_pairs_single_naive data) False hs) ⊆ snd ` Pair False ` (set hs × set hs)"
by (rule image_mono)
also have "... = set hs × set hs" by (simp add: image_comp)
finally have 2: "snd ` set (pairs (add_pairs_single_naive data) False hs) ⊆ set hs × (set gs ∪ set bs ∪ set hs)"
by fastforce
show "snd ` set (new_pairs_naive gs bs hs data) ⊆ set hs × (set gs ∪ set bs ∪ set hs) ∧
set hs × (set gs ∪ set bs) ⊆ snd ` set (new_pairs_naive gs bs hs data) ∧
(∀a b. a ∈ set hs ⟶ b ∈ set hs ⟶ a ≠ b ⟶ (a, b) ∈⇩p snd ` set (new_pairs_naive gs bs hs data)) ∧
(∀p q. (True, p, q) ∈ set (new_pairs_naive gs bs hs data) ⟶ q ∈ set gs ∪ set bs)"
proof (intro conjI allI impI)
show "snd ` set (new_pairs_naive gs bs hs data) ⊆ set hs × (set gs ∪ set bs ∪ set hs)"
by (simp add: set_new_pairs_naive image_Un image_comp 1 2)
next
show "set hs × (set gs ∪ set bs) ⊆ snd ` set (new_pairs_naive gs bs hs data)"
by (simp add: set_new_pairs_naive image_Un image_comp)
next
fix a b
assume "a ∈ set hs" and "b ∈ set hs" and "a ≠ b"
with set_add_pairs_single_naive
have "(a, b) ∈⇩p snd ` set (pairs (add_pairs_single_naive data) False hs)"
by (rule in_pairsI')
thus "(a, b) ∈⇩p snd ` set (new_pairs_naive gs bs hs data)"
by (simp add: set_new_pairs_naive image_Un)
next
fix p q
assume "(True, p, q) ∈ set (new_pairs_naive gs bs hs data)"
hence "q ∈ set gs ∪ set bs ∨ (True, p, q) ∈ set (pairs (add_pairs_single_naive data) False hs)"
by (auto simp: set_new_pairs_naive)
thus "q ∈ set gs ∪ set bs"
proof
assume "(True, p, q) ∈ set (pairs (add_pairs_single_naive data) False hs)"
also from set_add_pairs_single_naive have "... ⊆ Pair False ` (set hs × set hs)"
by (rule pairs_subset)
finally show ?thesis by auto
qed
qed
qed
lemma np_spec_new_pairs_sorted: "np_spec (new_pairs_sorted rel)"
proof (rule np_specI)
fix gs bs hs :: "('t, 'b, 'c) pdata list" and data::"nat × 'd"
have 1: "set hs × (set gs ∪ set bs) ⊆ set hs × (set gs ∪ set bs ∪ set hs)" by fastforce
have "set (pairs (add_pairs_single_sorted (rel data)) False hs) ⊆ Pair False ` (set hs × set hs)"
by (rule pairs_subset, simp add: set_add_pairs_single_sorted)
hence "snd ` set (pairs (add_pairs_single_sorted (rel data)) False hs) ⊆ snd ` Pair False ` (set hs × set hs)"
by (rule image_mono)
also have "... = set hs × set hs" by (simp add: image_comp)
finally have 2: "snd ` set (pairs (add_pairs_single_sorted (rel data)) False hs) ⊆ set hs × (set gs ∪ set bs ∪ set hs)"
by fastforce
show "snd ` set (new_pairs_sorted rel gs bs hs data) ⊆ set hs × (set gs ∪ set bs ∪ set hs) ∧
set hs × (set gs ∪ set bs) ⊆ snd ` set (new_pairs_sorted rel gs bs hs data) ∧
(∀a b. a ∈ set hs ⟶ b ∈ set hs ⟶ a ≠ b ⟶ (a, b) ∈⇩p snd ` set (new_pairs_sorted rel gs bs hs data)) ∧
(∀p q. (True, p, q) ∈ set (new_pairs_sorted rel gs bs hs data) ⟶ q ∈ set gs ∪ set bs)"
proof (intro conjI allI impI)
show "snd ` set (new_pairs_sorted rel gs bs hs data) ⊆ set hs × (set gs ∪ set bs ∪ set hs)"
by (simp add: set_new_pairs_sorted image_Un image_comp 1 2)
next
show "set hs × (set gs ∪ set bs) ⊆ snd ` set (new_pairs_sorted rel gs bs hs data)"
by (simp add: set_new_pairs_sorted image_Un image_comp)
next
fix a b
assume "a ∈ set hs" and "b ∈ set hs" and "a ≠ b"
with set_add_pairs_single_sorted
have "(a, b) ∈⇩p snd ` set (pairs (add_pairs_single_sorted (rel data)) False hs)"
by (rule in_pairsI')
thus "(a, b) ∈⇩p snd ` set (new_pairs_sorted rel gs bs hs data)"
by (simp add: set_new_pairs_sorted image_Un)
next
fix p q
assume "(True, p, q) ∈ set (new_pairs_sorted rel gs bs hs data)"
hence "q ∈ set gs ∪ set bs ∨ (True, p, q) ∈ set (pairs (add_pairs_single_sorted (rel data)) False hs)"
by (auto simp: set_new_pairs_sorted)
thus "q ∈ set gs ∪ set bs"
proof
assume "(True, p, q) ∈ set (pairs (add_pairs_single_sorted (rel data)) False hs)"
also from set_add_pairs_single_sorted have "... ⊆ Pair False ` (set hs × set hs)"
by (rule pairs_subset)
finally show ?thesis by auto
qed
qed
qed
text ‹@{term "new_pairs_naive gs bs hs data"} and @{term "new_pairs_sorted rel gs bs hs data"} return
lists of triples @{term "(q_in_bs, p, q)"}, where ‹q_in_bs› indicates whether ‹q› is contained in
the list @{term "gs @ bs"} or in the list ‹hs›. ‹p› is always contained in ‹hs›.›
definition canon_pair_order_aux :: "('t, 'b::zero, 'c) pdata_pair ⇒ ('t, 'b, 'c) pdata_pair ⇒ bool"
where "canon_pair_order_aux p q ⟷
(lcs (lp (fst (fst p))) (lp (fst (snd p))) ≼ lcs (lp (fst (fst q))) (lp (fst (snd q))))"
abbreviation "canon_pair_order data p q ≡ canon_pair_order_aux (snd p) (snd q)"
abbreviation "canon_pair_comb ≡ merge_wrt canon_pair_order_aux"
subsubsection ‹Applying Criteria to New Pairs›
definition apply_icrit :: "('t, 'b, 'c, 'd) icritT ⇒ (nat × 'd) ⇒ ('t, 'b, 'c) pdata list ⇒
('t, 'b, 'c) pdata list ⇒ ('t, 'b, 'c) pdata list ⇒
(bool × ('t, 'b, 'c) pdata_pair) list ⇒
(bool × bool × ('t, 'b, 'c) pdata_pair) list"
where "apply_icrit crit data gs bs hs ps = (let c = crit data gs bs hs in map (λ(q_in_bs, p, q). (c p q, q_in_bs, p, q)) ps)"
lemma fst_apply_icrit:
assumes "icrit_spec crit" and "dickson_grading d"
and "fst ` (set gs ∪ set bs ∪ set hs) ⊆ dgrad_p_set d m" and "unique_idx (gs @ bs @ hs) data"
and "is_Groebner_basis (fst ` set gs)" and "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs"
and "fst p ≠ 0" and "fst q ≠ 0" and "(True, q_in_bs, p, q) ∈ set (apply_icrit crit data gs bs hs ps)"
shows "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs ∪ set hs)) (fst p) (fst q)"
proof -
from assms(10) have "crit data gs bs hs p q" by (auto simp: apply_icrit_def)
with assms(1-9) show ?thesis by (rule icrit_specD)
qed
lemma snd_apply_icrit [simp]: "map snd (apply_icrit crit data gs bs hs ps) = ps"
by (auto simp add: apply_icrit_def case_prod_beta' intro: nth_equalityI)
lemma set_snd_apply_icrit [simp]: "snd ` set (apply_icrit crit data gs bs hs ps) = set ps"
proof -
have "snd ` set (apply_icrit crit data gs bs hs ps) = set (map snd (apply_icrit crit data gs bs hs ps))"
by (simp del: snd_apply_icrit)
also have "... = set ps" by (simp only: snd_apply_icrit)
finally show ?thesis .
qed
definition apply_ncrit :: "('t, 'b, 'c, 'd) ncritT ⇒ (nat × 'd) ⇒ ('t, 'b, 'c) pdata list ⇒
('t, 'b, 'c) pdata list ⇒ ('t, 'b, 'c) pdata list ⇒
(bool × bool × ('t, 'b, 'c) pdata_pair) list ⇒
(bool × ('t, 'b, 'c) pdata_pair) list"
where "apply_ncrit crit data gs bs hs ps =
(let c = crit data gs bs hs in
rev (fold (λ(ic, q_in_bs, p, q). λps'. if ¬ ic ∧ c q_in_bs ps' p q then ps' else (ic, p, q) # ps') ps []))"
lemma apply_ncrit_append:
"apply_ncrit crit data gs bs hs (xs @ ys) =
rev (fold (λ(ic, q_in_bs, p, q). λps'. if ¬ ic ∧ crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps') ys
(rev (apply_ncrit crit data gs bs hs xs)))"
by (simp add: apply_ncrit_def Let_def)
lemma fold_superset:
"set acc ⊆
set (fold (λ(ic, q_in_bs, p, q). λps'. if ¬ ic ∧ c q_in_bs ps' p q then ps' else (ic, p, q) # ps') ps acc)"
proof (induct ps arbitrary: acc)
case Nil
show ?case by simp
next
case (Cons x ps)
obtain ic' q_in_bs' p' q' where x: "x = (ic', q_in_bs', p', q')" using prod_cases4 by blast
have 1: "set acc0 ⊆ set (fold (λ(ic, q_in_bs, p, q) ps'. if ¬ ic ∧ c q_in_bs ps' p q then ps' else (ic, p, q) # ps') ps acc0)"
for acc0 by (rule Cons)
have "set acc ⊆ set ((ic', p', q') # acc)" by fastforce
also have "... ⊆ set (fold (λ(ic, q_in_bs, p, q) ps'. if ¬ ic ∧ c q_in_bs ps' p q then ps' else (ic, p, q) # ps') ps
((ic', p', q') # acc))" by (fact 1)
finally have 2: "set acc ⊆ set (fold (λ(ic, q_in_bs, p, q) ps'. if ¬ ic ∧ c q_in_bs ps' p q then ps' else (ic, p, q) # ps') ps
((ic', p', q') # acc))" .
show ?case by (simp add: x 1 2)
qed
lemma apply_ncrit_superset:
"set (apply_ncrit crit data gs bs hs ps) ⊆ set (apply_ncrit crit data gs bs hs (ps @ qs))" (is "?l ⊆ ?r")
proof -
have "?l = set (rev (apply_ncrit crit data gs bs hs ps))" by simp
also have "... ⊆ set (fold (λ(ic, q_in_bs, p, q) ps'.
if ¬ ic ∧ crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps')
qs (rev (apply_ncrit crit data gs bs hs ps)))" by (fact fold_superset)
also have "... = ?r" by (simp add: apply_ncrit_append)
finally show ?thesis .
qed
lemma apply_ncrit_subset_aux:
assumes "(ic, p, q) ∈ set (fold
(λ(ic, q_in_bs, p, q). λps'. if ¬ ic ∧ c q_in_bs ps' p q then ps' else (ic, p, q) # ps') ps acc)"
shows "(ic, p, q) ∈ set acc ∨ (∃q_in_bs. (ic, q_in_bs, p, q) ∈ set ps)"
using assms
proof (induct ps arbitrary: acc)
case Nil
thus ?case by simp
next
case (Cons x ps)
obtain ic' q_in_bs' p' q' where x: "x = (ic', q_in_bs', p', q')" using prod_cases4 by blast
from Cons(2) have "(ic, p, q) ∈
set (fold (λ(ic, q_in_bs, p, q) ps'. if ¬ ic ∧ c q_in_bs ps' p q then ps' else (ic, p, q) # ps') ps
(if ¬ ic' ∧ c q_in_bs' acc p' q' then acc else (ic', p', q') # acc))" by (simp add: x)
hence "(ic, p, q) ∈ set (if ¬ ic' ∧ c q_in_bs' acc p' q' then acc else (ic', p', q') # acc) ∨
(∃q_in_bs. (ic, q_in_bs, p, q) ∈ set ps)" by (rule Cons(1))
hence "(ic, p, q) ∈ set acc ∨ (ic, p, q) = (ic', p', q') ∨ (∃q_in_bs. (ic, q_in_bs, p, q) ∈ set ps)"
by (auto split: if_splits)
thus ?case
proof (elim disjE)
assume "(ic, p, q) ∈ set acc"
thus ?thesis ..
next
assume "(ic, p, q) = (ic', p', q')"
hence "x = (ic, q_in_bs', p, q)" by (simp add: x)
thus ?thesis by auto
next
assume "∃q_in_bs. (ic, q_in_bs, p, q) ∈ set ps"
then obtain q_in_bs where "(ic, q_in_bs, p, q) ∈ set ps" ..
thus ?thesis by auto
qed
qed
corollary apply_ncrit_subset:
assumes "(ic, p, q) ∈ set (apply_ncrit crit data gs bs hs ps)"
obtains q_in_bs where "(ic, q_in_bs, p, q) ∈ set ps"
proof -
from assms
have "(ic, p, q) ∈ set (fold
(λ(ic, q_in_bs, p, q). λps'. if ¬ ic ∧ crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps') ps [])"
by (simp add: apply_ncrit_def)
hence "(ic, p, q) ∈ set [] ∨ (∃q_in_bs. (ic, q_in_bs, p, q) ∈ set ps)"
by (rule apply_ncrit_subset_aux)
hence "∃q_in_bs. (ic, q_in_bs, p, q) ∈ set ps" by simp
then obtain q_in_bs where "(ic, q_in_bs, p, q) ∈ set ps" ..
thus ?thesis ..
qed
corollary apply_ncrit_subset': "snd ` set (apply_ncrit crit data gs bs hs ps) ⊆ snd ` snd ` set ps"
proof
fix p q
assume "(p, q) ∈ snd ` set (apply_ncrit crit data gs bs hs ps)"
then obtain ic where "(ic, p, q) ∈ set (apply_ncrit crit data gs bs hs ps)" by fastforce
then obtain q_in_bs where "(ic, q_in_bs, p, q) ∈ set ps" by (rule apply_ncrit_subset)
thus "(p, q) ∈ snd ` snd ` set ps" by force
qed
lemma not_in_apply_ncrit:
assumes "(ic, p, q) ∉ set (apply_ncrit crit data gs bs hs (xs @ ((ic, q_in_bs, p, q) # ys)))"
shows "crit data gs bs hs q_in_bs (rev (apply_ncrit crit data gs bs hs xs)) p q"
using assms
proof (simp add: apply_ncrit_append split: if_splits)
assume "(ic, p, q) ∉
set (fold (λ(ic, q_in_bs, p, q) ps'. if ¬ ic ∧ crit data gs bs hs q_in_bs ps' p q then ps' else (ic, p, q) # ps')
ys ((ic, p, q) # rev (apply_ncrit crit data gs bs hs xs)))" (is "_ ∉ ?A")
have "(ic, p, q) ∈ set ((ic, p, q) # rev (apply_ncrit crit data gs bs hs xs))" by simp
also have "... ⊆ ?A" by (rule fold_superset)
finally have "(ic, p, q) ∈ ?A" .
with ‹(ic, p, q) ∉ ?A› show ?thesis ..
qed
lemma (in -) setE:
assumes "x ∈ set xs"
obtains ys zs where "xs = ys @ (x # zs)"
using assms
proof (induct xs arbitrary: thesis)
case Nil
from Nil(2) show ?case by simp
next
case (Cons a xs)
from Cons(3) have "x = a ∨ x ∈ set xs" by simp
thus ?case
proof
assume "x = a"
show ?thesis by (rule Cons(2)[of "[]" xs], simp add: ‹x = a›)
next
assume "x ∈ set xs"
then obtain ys zs where "xs = ys @ (x # zs)" by (meson Cons(1))
show ?thesis by (rule Cons(2)[of "a # ys" zs], simp add: ‹xs = ys @ (x # zs)›)
qed
qed
lemma apply_ncrit_connectible:
assumes "ncrit_spec crit" and "dickson_grading d"
and "set gs ∪ set bs ∪ set hs ⊆ B" and "fst ` B ⊆ dgrad_p_set d m"
and "snd ` snd ` set ps ⊆ set hs × (set gs ∪ set bs ∪ set hs)" and "unique_idx (gs @ bs @ hs) data"
and "is_Groebner_basis (fst ` set gs)"
and "⋀p' q'. (p', q') ∈ snd ` set (apply_ncrit crit data gs bs hs ps) ⟹
fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹ crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
and "⋀p' q'. p' ∈ set gs ∪ set bs ⟹ q' ∈ set gs ∪ set bs ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
assumes "(ic, q_in_bs, p, q) ∈ set ps" and "fst p ≠ 0" and "fst q ≠ 0"
and "q_in_bs ⟹ (q ∈ set gs ∪ set bs)"
shows "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
proof (cases "(p, q) ∈ snd ` set (apply_ncrit crit data gs bs hs ps)")
case True
thus ?thesis using assms(11,12) by (rule assms(8))
next
case False
from assms(10) have "(p, q) ∈ snd ` snd ` set ps" by force
also have "... ⊆ set hs × (set gs ∪ set bs ∪ set hs)" by (fact assms(5))
finally have "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs" by simp_all
from ‹(ic, q_in_bs, p, q) ∈ set ps› obtain xs ys where ps: "ps = xs @ ((ic, q_in_bs, p, q) # ys)"
by (rule setE)
let ?ps = "rev (apply_ncrit crit data gs bs hs xs)"
have "snd ` set ?ps ⊆ snd ` snd ` set xs" by (simp add: apply_ncrit_subset')
also have "... ⊆ snd ` snd ` set ps" unfolding ps by fastforce
finally have sub: "snd ` set ?ps ⊆ set hs × (set gs ∪ set bs ∪ set hs)"
using assms(5) by (rule subset_trans)
from False have "(p, q) ∉ snd ` set (apply_ncrit crit data gs bs hs ps)" by (simp add: in_pair_iff)
hence "(ic, p, q) ∉ set (apply_ncrit crit data gs bs hs (xs @ ((ic, q_in_bs, p, q) # ys)))"
unfolding ps by force
hence "crit data gs bs hs q_in_bs ?ps p q" by (rule not_in_apply_ncrit)
with assms(1-4) sub assms(6,7,13) _ _ ‹p ∈ set hs› ‹q ∈ set gs ∪ set bs ∪ set hs› assms(11,12)
show ?thesis
proof (rule ncrit_specD)
fix p' q'
assume "(p', q') ∈⇩p snd ` set ?ps"
also have "... ⊆ snd ` set (apply_ncrit crit data gs bs hs ps)"
by (rule image_mono, simp add: ps apply_ncrit_superset)
finally have disj: "(p', q') ∈ snd ` set (apply_ncrit crit data gs bs hs ps) ∨
(q', p') ∈ snd ` set (apply_ncrit crit data gs bs hs ps)" by (simp only: in_pair_iff)
assume "fst p' ≠ 0" and "fst q' ≠ 0"
from disj show "crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
proof
assume "(p', q') ∈ snd ` set (apply_ncrit crit data gs bs hs ps)"
thus ?thesis using ‹fst p' ≠ 0› ‹fst q' ≠ 0› by (rule assms(8))
next
assume "(q', p') ∈ snd ` set (apply_ncrit crit data gs bs hs ps)"
hence "crit_pair_cbelow_on d m (fst ` B) (fst q') (fst p')"
using ‹fst q' ≠ 0› ‹fst p' ≠ 0› by (rule assms(8))
thus ?thesis by (rule crit_pair_cbelow_sym)
qed
qed (assumption, fact assms(9))
qed
subsubsection ‹Applying Criteria to Old Pairs›
definition apply_ocrit :: "('t, 'b, 'c, 'd) ocritT ⇒ (nat × 'd) ⇒ ('t, 'b, 'c) pdata list ⇒
(bool × ('t, 'b, 'c) pdata_pair) list ⇒ ('t, 'b, 'c) pdata_pair list ⇒
('t, 'b, 'c) pdata_pair list"
where "apply_ocrit crit data hs ps' ps = (let c = crit data hs ps' in [(p, q)←ps . ¬ c p q])"
lemma set_apply_ocrit:
"set (apply_ocrit crit data hs ps' ps) = {(p, q) | p q. (p, q) ∈ set ps ∧ ¬ crit data hs ps' p q}"
by (auto simp: apply_ocrit_def)
corollary set_apply_ocrit_iff:
"(p, q) ∈ set (apply_ocrit crit data hs ps' ps) ⟷ ((p, q) ∈ set ps ∧ ¬ crit data hs ps' p q)"
by (auto simp: apply_ocrit_def)
lemma apply_ocrit_connectible:
assumes "ocrit_spec crit" and "dickson_grading d" and "set hs ⊆ B" and "fst ` B ⊆ dgrad_p_set d m"
and "unique_idx (p # q # hs @ (map (fst ∘ snd) ps') @ (map (snd ∘ snd) ps')) data"
and "⋀p' q'. (p', q') ∈ snd ` set ps' ⟹ fst p' ≠ 0 ⟹ fst q' ≠ 0 ⟹
crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
assumes "p ∈ B" and "q ∈ B" and "fst p ≠ 0" and "fst q ≠ 0"
and "(p, q) ∈ set ps" and "(p, q) ∉ set (apply_ocrit crit data hs ps' ps)"
shows "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
proof -
from assms(11,12) have "crit data hs ps' p q" by (simp add: set_apply_ocrit_iff)
with assms(1-5) _ assms(7-10) show ?thesis
proof (rule ocrit_specD)
fix p' q'
assume "(p', q') ∈⇩p snd ` set ps'"
hence disj: "(p', q') ∈ snd ` set ps' ∨ (q', p') ∈ snd ` set ps'" by (simp only: in_pair_iff)
assume "fst p' ≠ 0" and "fst q' ≠ 0"
from disj show "crit_pair_cbelow_on d m (fst ` B) (fst p') (fst q')"
proof
assume "(p', q') ∈ snd ` set ps'"
thus ?thesis using ‹fst p' ≠ 0› ‹fst q' ≠ 0› by (rule assms(6))
next
assume "(q', p') ∈ snd ` set ps'"
hence "crit_pair_cbelow_on d m (fst ` B) (fst q') (fst p')" using ‹fst q' ≠ 0› ‹fst p' ≠ 0›
by (rule assms(6))
thus ?thesis by (rule crit_pair_cbelow_sym)
qed
qed
qed
subsubsection ‹Creating Final List of Pairs›
context
fixes np::"('t, 'b::field, 'c, 'd) npT"
and icrit::"('t, 'b, 'c, 'd) icritT"
and ncrit::"('t, 'b, 'c, 'd) ncritT"
and ocrit::"('t, 'b, 'c, 'd) ocritT"
and comb::"('t, 'b, 'c) pdata_pair list ⇒ ('t, 'b, 'c) pdata_pair list ⇒ ('t, 'b, 'c) pdata_pair list"
begin
definition add_pairs :: "('t, 'b, 'c, 'd) apT"
where "add_pairs gs bs ps hs data =
(let ps1 = apply_ncrit ncrit data gs bs hs (apply_icrit icrit data gs bs hs (np gs bs hs data));
ps2 = apply_ocrit ocrit data hs ps1 ps in comb (map snd [x←ps1 . ¬ fst x]) ps2)"
lemma set_add_pairs:
assumes "⋀xs ys. set (comb xs ys) = set xs ∪ set ys"
assumes "ps1 = apply_ncrit ncrit data gs bs hs (apply_icrit icrit data gs bs hs (np gs bs hs data))"
shows "set (add_pairs gs bs ps hs data) =
{(p, q) | p q. (False, p, q) ∈ set ps1 ∨ ((p, q) ∈ set ps ∧ ¬ ocrit data hs ps1 p q)}"
proof -
have eq: "snd ` {x ∈ set ps1. ¬ fst x} = {(p, q) | p q. (False, p, q) ∈ set ps1}" by force
thus ?thesis by (auto simp: add_pairs_def Let_def assms(1) assms(2)[symmetric] set_apply_ocrit)
qed
lemma set_add_pairs_iff:
assumes "⋀xs ys. set (comb xs ys) = set xs ∪ set ys"
assumes "ps1 = apply_ncrit ncrit data gs bs hs (apply_icrit icrit data gs bs hs (np gs bs hs data))"
shows "((p, q) ∈ set (add_pairs gs bs ps hs data)) ⟷
((False, p, q) ∈ set ps1 ∨ ((p, q) ∈ set ps ∧ ¬ ocrit data hs ps1 p q))"
proof -
from assms have eq: "set (add_pairs gs bs ps hs data) =
{(p, q) | p q. (False, p, q) ∈ set ps1 ∨ ((p, q) ∈ set ps ∧ ¬ ocrit data hs ps1 p q)}"
by (rule set_add_pairs)
obtain a aa b where p: "p = (a, aa, b)" using prod_cases3 by blast
obtain ab ac ba where q: "q = (ab, ac, ba)" using prod_cases3 by blast
show ?thesis by (simp add: eq p q)
qed
lemma ap_spec_add_pairs:
assumes "np_spec np" and "icrit_spec icrit" and "ncrit_spec ncrit" and "ocrit_spec ocrit"
and "⋀xs ys. set (comb xs ys) = set xs ∪ set ys"
shows "ap_spec add_pairs"
proof (rule ap_specI)
fix gs bs :: "('t, 'b, 'c) pdata list" and ps hs and data::"nat × 'd"
define ps1 where "ps1 = apply_ncrit ncrit data gs bs hs (apply_icrit icrit data gs bs hs (np gs bs hs data))"
show "set (add_pairs gs bs ps hs data) ⊆ set ps ∪ set hs × (set gs ∪ set bs ∪ set hs)"
proof
fix p q
assume "(p, q) ∈ set (add_pairs gs bs ps hs data)"
with assms(5) ps1_def have "(False, p, q) ∈ set ps1 ∨ ((p, q) ∈ set ps ∧ ¬ ocrit data hs ps1 p q)"
by (simp add: set_add_pairs_iff)
thus "(p, q) ∈ set ps ∪ set hs × (set gs ∪ set bs ∪ set hs)"
proof
assume "(False, p, q) ∈ set ps1"
hence "snd (False, p, q) ∈ snd ` set ps1" by fastforce
hence "(p, q) ∈ snd ` set ps1" by simp
also have "... ⊆ snd ` snd ` set (apply_icrit icrit data gs bs hs (np gs bs hs data))"
unfolding ps1_def by (fact apply_ncrit_subset')
also have "... = snd ` set (np gs bs hs data)" by simp
also from assms(1) have "... ⊆ set hs × (set gs ∪ set bs ∪ set hs)" by (rule np_specD1)
finally show ?thesis ..
next
assume "(p, q) ∈ set ps ∧ ¬ ocrit data hs ps1 p q"
thus ?thesis by simp
qed
qed
next
fix gs bs :: "('t, 'b, 'c) pdata list" and ps hs and data::"nat × 'd" and B and d::"'a ⇒ nat" and m h g
assume dg: "dickson_grading d" and B_sup: "set gs ∪ set bs ∪ set hs ⊆ B"
and B_sub: "fst ` B ⊆ dgrad_p_set d m" and h_in: "h ∈ set hs" and g_in: "g ∈ set gs ∪ set bs ∪ set hs"
and ps_sub: "set ps ⊆ set bs × (set gs ∪ set bs)"
and uid: "unique_idx (gs @ bs @ hs) data" and gb: "is_Groebner_basis (fst ` set gs)" and "h ≠ g"
and "fst h ≠ 0" and "fst g ≠ 0"
assume a: "⋀a b. (a, b) ∈⇩p set (add_pairs gs bs ps hs data) ⟹
fst a ≠ 0 ⟹ fst b ≠ 0 ⟹ crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
assume b: "⋀a b. a ∈ set gs ∪ set bs ⟹
b ∈ set gs ∪ set bs ⟹
fst a ≠ 0 ⟹ fst b ≠ 0 ⟹ crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
define ps0 where "ps0 = apply_icrit icrit data gs bs hs (np gs bs hs data)"
define ps1 where "ps1 = apply_ncrit ncrit data gs bs hs ps0"
have "snd ` snd ` set ps0 = snd ` set (np gs bs hs data)" by (simp add: ps0_def)
also from assms(1) have "... ⊆ set hs × (set gs ∪ set bs ∪ set hs)" by (rule np_specD1)
finally have ps0_sub: "snd ` snd ` set ps0 ⊆ set hs × (set gs ∪ set bs ∪ set hs)" .
have "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
if "(p, q) ∈ snd ` set ps1" and "fst p ≠ 0" and "fst q ≠ 0" for p q
proof -
from ‹(p, q) ∈ snd ` set ps1› obtain ic where "(ic, p, q) ∈ set ps1" by fastforce
show ?thesis
proof (cases "ic")
case True
from ‹(ic, p, q) ∈ set ps1› obtain q_in_bs where "(ic, q_in_bs, p, q) ∈ set ps0"
unfolding ps1_def by (rule apply_ncrit_subset)
with True have "(True, q_in_bs, p, q) ∈ set ps0" by simp
hence "snd (snd (True, q_in_bs, p, q)) ∈ snd ` snd ` set ps0" by fastforce
hence "(p, q) ∈ snd ` snd ` set ps0" by simp
also have "... ⊆ set hs × (set gs ∪ set bs ∪ set hs)" by (fact ps0_sub)
finally have "p ∈ set hs" and "q ∈ set gs ∪ set bs ∪ set hs" by simp_all
from B_sup have B_sup': "fst ` (set gs ∪ set bs ∪ set hs) ⊆ fst ` B" by (rule image_mono)
hence "fst ` (set gs ∪ set bs ∪ set hs) ⊆ dgrad_p_set d m" using B_sub by (rule subset_trans)
from assms(2) dg this uid gb ‹p ∈ set hs› ‹q ∈ set gs ∪ set bs ∪ set hs› ‹fst p ≠ 0› ‹fst q ≠ 0›
‹(True, q_in_bs, p, q) ∈ set ps0›
have "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs ∪ set hs)) (fst p) (fst q)"
unfolding ps0_def by (rule fst_apply_icrit)
thus ?thesis using B_sup' by (rule crit_pair_cbelow_mono)
next
case False
with ‹(ic, p, q) ∈ set ps1› have "(False, p, q) ∈ set ps1" by simp
with assms(5) ps1_def have "(p, q) ∈ set (add_pairs gs bs ps hs data)"
by (simp add: set_add_pairs_iff ps0_def)
hence "(p, q) ∈⇩p set (add_pairs gs bs ps hs data)" by (simp add: in_pair_iff)
thus ?thesis using ‹fst p ≠ 0› ‹fst q ≠ 0› by (rule a)
qed
qed
with assms(3) dg B_sup B_sub ps0_sub uid gb
have *: "(ic, q_in_bs, p, q) ∈ set ps0 ⟹ fst p ≠ 0 ⟹ fst q ≠ 0 ⟹
(q_in_bs ⟹ q ∈ set gs ∪ set bs) ⟹ crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
for ic q_in_bs p q using b unfolding ps1_def by (rule apply_ncrit_connectible)
show "crit_pair_cbelow_on d m (fst ` B) (fst h) (fst g)"
proof (cases "h = g")
case True
from g_in B_sup have "g ∈ B" ..
hence "fst g ∈ fst ` B" by simp
hence "fst g ∈ dgrad_p_set d m" using B_sub ..
with dg show ?thesis unfolding True by (rule crit_pair_cbelow_same)
next
case False
with assms(1) h_in g_in show ?thesis
proof (rule np_specE)
fix g_in_bs
assume "(g_in_bs, h, g) ∈ set (np gs bs hs data)"
also have "... = snd ` set ps0" by (simp add: ps0_def)
finally obtain ic where "(ic, g_in_bs, h, g) ∈ set ps0" by fastforce
moreover note ‹fst h ≠ 0› ‹fst g ≠ 0›
moreover from assms(1) have "g ∈ set gs ∪ set bs" if "g_in_bs"
proof (rule np_specD4)
from ‹(g_in_bs, h, g) ∈ set (np gs bs hs data)› that show "(True, h, g) ∈ set (np gs bs hs data)"
by simp
qed
ultimately show ?thesis by (rule *)
next
fix h_in_bs
assume "(h_in_bs, g, h) ∈ set (np gs bs hs data)"
also have "... = snd ` set ps0" by (simp add: ps0_def)
finally obtain ic where "(ic, h_in_bs, g, h) ∈ set ps0" by fastforce
moreover note ‹fst g ≠ 0› ‹fst h ≠ 0›
moreover from assms(1) have "h ∈ set gs ∪ set bs" if "h_in_bs"
proof (rule np_specD4)
from ‹(h_in_bs, g, h) ∈ set (np gs bs hs data)› that show "(True, g, h) ∈ set (np gs bs hs data)"
by simp
qed
ultimately have "crit_pair_cbelow_on d m (fst ` B) (fst g) (fst h)" by (rule *)
thus ?thesis by (rule crit_pair_cbelow_sym)
qed
qed
next
fix gs bs :: "('t, 'b, 'c) pdata list" and ps hs and data::"nat × 'd" and B and d::"'a ⇒ nat" and m h g
define ps1 where "ps1 = apply_ncrit ncrit data gs bs hs (apply_icrit icrit data gs bs hs (np gs bs hs data))"
assume "(h, g) ∈ set ps -⇩p set (add_pairs gs bs ps hs data)"
hence "(h, g) ∈ set ps" and "(h, g) ∉⇩p set (add_pairs gs bs ps hs data)" by simp_all
from this(2) have "(h, g) ∉ set (add_pairs gs bs ps hs data)" by (simp add: in_pair_iff)
assume dg: "dickson_grading d" and B_sup: "set gs ∪ set bs ∪ set hs ⊆ B" and B_sub: "fst ` B ⊆ dgrad_p_set d m"
and ps_sub: "set ps ⊆ set bs × (set gs ∪ set bs)"
and "(set gs ∪ set bs) ∩ set hs = {}"
and uid: "unique_idx (gs @ bs @ hs) data" and gb: "is_Groebner_basis (fst ` set gs)"
and "h ≠ g" and "fst h ≠ 0" and "fst g ≠ 0"
assume *: "⋀a b. (a, b) ∈⇩p set (add_pairs gs bs ps hs data) ⟹
(a, b) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs) ⟹
fst a ≠ 0 ⟹ fst b ≠ 0 ⟹ crit_pair_cbelow_on d m (fst ` B) (fst a) (fst b)"
have "snd ` set ps1 ⊆ snd ` snd ` set (apply_icrit icrit data gs bs hs (np gs bs hs data))"
unfolding ps1_def by (rule apply_ncrit_subset')
also have "... = snd ` set (np gs bs hs data)" by simp
also from assms(1) have "... ⊆ set hs × (set gs ∪ set bs ∪ set hs)" by (rule np_specD1)
finally have ps1_sub: "snd ` set ps1 ⊆ set hs × (set gs ∪ set bs ∪ set hs)" .
from ‹(h, g) ∈ set ps› ps_sub have h_in: "h ∈ set gs ∪ set bs" and g_in: "g ∈ set gs ∪ set bs"
by fastforce+
with B_sup have "h ∈ B" and "g ∈ B" by auto
with assms(4) dg _ B_sub _ _ show "crit_pair_cbelow_on d m (fst ` B) (fst h) (fst g)"
using ‹fst h ≠ 0› ‹fst g ≠ 0› ‹(h, g) ∈ set ps›
proof (rule apply_ocrit_connectible)
from B_sup show "set hs ⊆ B" by simp
next
from ps1_sub h_in g_in
have "set (h # g # hs @ map (fst ∘ snd) ps1 @ map (snd ∘ snd) ps1) ⊆ set (gs @ bs @ hs)"
by fastforce
with uid show "unique_idx (h # g # hs @ map (fst ∘ snd) ps1 @ map (snd ∘ snd) ps1) data"
by (rule unique_idx_subset)
next
fix p q
assume "(p, q) ∈ snd ` set ps1"
hence pq_in: "(p, q) ∈ set hs × (set gs ∪ set bs ∪ set hs)" using ps1_sub ..
hence p_in: "p ∈ set hs" and q_in: "q ∈ set gs ∪ set bs ∪ set hs" by simp_all
assume "fst p ≠ 0" and "fst q ≠ 0"
from ‹(p, q) ∈ snd ` set ps1› obtain ic where "(ic, p, q) ∈ set ps1" by fastforce
show "crit_pair_cbelow_on d m (fst ` B) (fst p) (fst q)"
proof (cases "ic")
case True
hence "ic = True" by simp
from B_sup have B_sup': "fst ` (set gs ∪ set bs ∪ set hs) ⊆ fst ` B" by (rule image_mono)
note assms(2) dg
moreover from B_sup' B_sub have "fst ` (set gs ∪ set bs ∪ set hs) ⊆ dgrad_p_set d m"
by (rule subset_trans)
moreover note uid gb p_in q_in ‹fst p ≠ 0› ‹fst q ≠ 0›
moreover from ‹(ic, p, q) ∈ set ps1› obtain q_in_bs
where "(True, q_in_bs, p, q) ∈ set (apply_icrit icrit data gs bs hs (np gs bs hs data))"
unfolding ps1_def ‹ic = True› by (rule apply_ncrit_subset)
ultimately have "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs ∪ set hs)) (fst p) (fst q)"
by (rule fst_apply_icrit)
thus ?thesis using B_sup' by (rule crit_pair_cbelow_mono)
next
case False
with ‹(ic, p, q) ∈ set ps1› have "(False, p, q) ∈ set ps1" by simp
with assms(5) ps1_def have "(p, q) ∈ set (add_pairs gs bs ps hs data)"
by (simp add: set_add_pairs_iff)
hence "(p, q) ∈⇩p set (add_pairs gs bs ps hs data)" by (simp add: in_pair_iff)
moreover from pq_in have "(p, q) ∈⇩p set hs × (set gs ∪ set bs ∪ set hs)"
by (simp add: in_pair_iff)
ultimately show ?thesis using ‹fst p ≠ 0› ‹fst q ≠ 0› by (rule *)
qed
next
show "(h, g) ∉ set (apply_ocrit ocrit data hs ps1 ps)"
proof
assume "(h, g) ∈ set (apply_ocrit ocrit data hs ps1 ps)"
hence "(h, g) ∈ set (add_pairs gs bs ps hs data)"
by (simp add: add_pairs_def assms(5) Let_def ps1_def)
with ‹(h, g) ∉ set (add_pairs gs bs ps hs data)› show False ..
qed
qed
qed
end
abbreviation "add_pairs_canon ≡
add_pairs (new_pairs_sorted canon_pair_order) component_crit chain_ncrit chain_ocrit canon_pair_comb"
lemma ap_spec_add_pairs_canon: "ap_spec add_pairs_canon"
using np_spec_new_pairs_sorted icrit_spec_component_crit ncrit_spec_chain_ncrit
ocrit_spec_chain_ocrit set_merge_wrt
by (rule ap_spec_add_pairs)
subsection ‹Suitable Instances of the @{emph ‹completion›} Parameter›
definition rcp_spec :: "('t, 'b::field, 'c, 'd) complT ⇒ bool"
where "rcp_spec rcp ⟷
(∀gs bs ps sps data.
0 ∉ fst ` set (fst (rcp gs bs ps sps data)) ∧
(∀h b. h ∈ set (fst (rcp gs bs ps sps data)) ⟶ b ∈ set gs ∪ set bs ⟶ fst b ≠ 0 ⟶
¬ lt (fst b) adds⇩t lt (fst h)) ∧
(∀d. dickson_grading d ⟶
dgrad_p_set_le d (fst ` set (fst (rcp gs bs ps sps data))) (args_to_set (gs, bs, sps))) ∧
component_of_term ` Keys (fst ` (set (fst (rcp gs bs ps sps data)))) ⊆
component_of_term ` Keys (args_to_set (gs, bs, sps)) ∧
(is_Groebner_basis (fst ` set gs) ⟶ unique_idx (gs @ bs) data ⟶
(fst ` set (fst (rcp 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 (rcp gs bs ps sps data))))⇧*⇧* (spoly (fst p) (fst q)) 0))))"
text ‹Informally, ‹rcp_spec rcp› expresses that, for suitable ‹gs›, ‹bs› and ‹sps›, the value of
‹rcp gs bs ps sps›
\begin{itemize}
\item is a list consisting exclusively of non-zero polynomials contained in the module generated
by ‹set bs ∪ set gs›, whose leading terms are not divisible by the leading
term of any non-zero @{prop "b ∈ set bs"}, and
\item contains sufficiently many new polynomials such that all S-polynomials originating from
‹sps› can be reduced to ‹0› modulo the enlarged list of polynomials.
\end{itemize}›
lemma rcp_specI:
assumes "⋀gs bs ps sps data. 0 ∉ fst ` set (fst (rcp gs bs ps sps data))"
assumes "⋀gs bs ps sps h b data. h ∈ set (fst (rcp gs bs ps sps data)) ⟹ b ∈ set gs ∪ set bs ⟹ fst b ≠ 0 ⟹
¬ lt (fst b) adds⇩t lt (fst h)"
assumes "⋀gs bs ps sps d data. dickson_grading d ⟹
dgrad_p_set_le d (fst ` set (fst (rcp gs bs ps sps data))) (args_to_set (gs, bs, sps))"
assumes "⋀gs bs ps sps data. component_of_term ` Keys (fst ` (set (fst (rcp gs bs ps sps data)))) ⊆
component_of_term ` Keys (args_to_set (gs, bs, sps))"
assumes "⋀gs bs ps sps data. is_Groebner_basis (fst ` set gs) ⟹ unique_idx (gs @ bs) data ⟹
(fst ` set (fst (rcp 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 (rcp gs bs ps sps data))))⇧*⇧* (spoly (fst p) (fst q)) 0))"
shows "rcp_spec rcp"
unfolding rcp_spec_def using assms by auto
lemma rcp_specD1:
assumes "rcp_spec rcp"
shows "0 ∉ fst ` set (fst (rcp gs bs ps sps data))"
using assms unfolding rcp_spec_def by (elim allE conjE)
lemma rcp_specD2:
assumes "rcp_spec rcp"
and "h ∈ set (fst (rcp gs bs ps sps data))" and "b ∈ set gs ∪ set bs" and "fst b ≠ 0"
shows "¬ lt (fst b) adds⇩t lt (fst h)"
using assms unfolding rcp_spec_def by (elim allE conjE, blast)
lemma rcp_specD3:
assumes "rcp_spec rcp" and "dickson_grading d"
shows "dgrad_p_set_le d (fst ` set (fst (rcp gs bs ps sps data))) (args_to_set (gs, bs, sps))"
using assms unfolding rcp_spec_def by (elim allE conjE, blast)
lemma rcp_specD4:
assumes "rcp_spec rcp"
shows "component_of_term ` Keys (fst ` (set (fst (rcp gs bs ps sps data)))) ⊆
component_of_term ` Keys (args_to_set (gs, bs, sps))"
using assms unfolding rcp_spec_def by (elim allE conjE)
lemma rcp_specD5:
assumes "rcp_spec rcp" and "is_Groebner_basis (fst ` set gs)" and "unique_idx (gs @ bs) data"
shows "fst ` set (fst (rcp gs bs ps sps data)) ⊆ pmdl (args_to_set (gs, bs, sps))"
using assms unfolding rcp_spec_def by blast
lemma rcp_specD6:
assumes "rcp_spec rcp" and "is_Groebner_basis (fst ` set gs)" and "unique_idx (gs @ bs) data"
and "set sps ⊆ set bs × (set gs ∪ set bs)"
and "(p, q) ∈ set sps"
shows "(red (fst ` (set gs ∪ set bs) ∪ fst ` set (fst (rcp gs bs ps sps data))))⇧*⇧* (spoly (fst p) (fst q)) 0"
using assms unfolding rcp_spec_def by blast
lemma compl_struct_rcp:
assumes "rcp_spec rcp"
shows "compl_struct rcp"
proof (rule compl_structI)
fix d::"'a ⇒ nat" and gs bs ps and sps::"('t, 'b, 'c) pdata_pair list" and data::"nat × 'd"
assume "dickson_grading d" and "set sps ⊆ set ps"
from assms this(1) have "dgrad_p_set_le d (fst ` set (fst (rcp gs bs (ps -- sps) sps data)))
(args_to_set (gs, bs, sps))"
by (rule rcp_specD3)
also have "dgrad_p_set_le d ... (args_to_set (gs, bs, ps))"
by (rule dgrad_p_set_le_subset, rule args_to_set_subset3, fact ‹set sps ⊆ set ps›)
finally show "dgrad_p_set_le d (fst ` set (fst (rcp gs bs (ps -- sps) sps data)))
(args_to_set (gs, bs, ps))" .
next
fix gs bs ps and sps::"('t, 'b, 'c) pdata_pair list" and data::"nat × 'd"
from assms show "0 ∉ fst ` set (fst (rcp gs bs (ps -- sps) sps data))"
by (rule rcp_specD1)
next
fix gs bs ps sps h b data
assume "h ∈ set (fst (rcp gs bs (ps -- sps) sps data))"
and "b ∈ set gs ∪ set bs" and "fst b ≠ 0"
with assms show "¬ lt (fst b) adds⇩t lt (fst h)" by (rule rcp_specD2)
next
fix gs bs ps and sps::"('t, 'b, 'c) pdata_pair list" and data::"nat × 'd"
assume "set sps ⊆ set ps"
from assms
have "component_of_term ` Keys (fst ` set (fst (rcp gs bs (ps -- sps) sps data))) ⊆
component_of_term ` Keys (args_to_set (gs, bs, sps))"
by (rule rcp_specD4)
also have "... ⊆ component_of_term ` Keys (args_to_set (gs, bs, ps))"
by (rule image_mono, rule Keys_mono, rule args_to_set_subset3, fact ‹set sps ⊆ set ps›)
finally show "component_of_term ` Keys (fst ` set (fst (rcp gs bs (ps -- sps) sps data))) ⊆
component_of_term ` Keys (args_to_set (gs, bs, ps))" .
qed
lemma compl_pmdl_rcp:
assumes "rcp_spec rcp"
shows "compl_pmdl rcp"
proof (rule compl_pmdlI)
fix gs bs :: "('t, 'b, 'c) pdata list" and ps sps :: "('t, 'b, 'c) pdata_pair list" and data::"nat × 'd"
assume gb: "is_Groebner_basis (fst ` set gs)" and "set sps ⊆ set ps"
and un: "unique_idx (gs @ bs) data"
let ?res = "fst (rcp gs bs (ps -- sps) sps data)"
from assms gb un have "fst ` set ?res ⊆ pmdl (args_to_set (gs, bs, sps))"
by (rule rcp_specD5)
also have "... ⊆ pmdl (args_to_set (gs, bs, ps))"
by (rule pmdl.span_mono, rule args_to_set_subset3, fact ‹set sps ⊆ set ps›)
finally show "fst ` set ?res ⊆ pmdl (args_to_set (gs, bs, ps))" .
qed
lemma compl_conn_rcp:
assumes "rcp_spec rcp"
shows "compl_conn rcp"
proof (rule compl_connI)
fix d::"'a ⇒ nat" and m gs bs ps sps p and q::"('t, 'b, 'c) pdata" and data::"nat × 'd"
assume dg: "dickson_grading d" and gs_sub: "fst ` set gs ⊆ dgrad_p_set d m"
and gb: "is_Groebner_basis (fst ` set gs)" and bs_sub: "fst ` set bs ⊆ dgrad_p_set d m"
and ps_sub: "set ps ⊆ set bs × (set gs ∪ set bs)" and "set sps ⊆ set ps"
and uid: "unique_idx (gs @ bs) data"
and "(p, q) ∈ set sps" and "fst p ≠ 0" and "fst q ≠ 0"
from ‹set sps ⊆ set ps› ps_sub have sps_sub: "set sps ⊆ set bs × (set gs ∪ set bs)"
by (rule subset_trans)
let ?res = "fst (rcp gs bs (ps -- sps) sps data)"
have "fst ` set ?res ⊆ dgrad_p_set d m"
proof (rule dgrad_p_set_le_dgrad_p_set, rule rcp_specD3, fact+)
show "args_to_set (gs, bs, sps) ⊆ dgrad_p_set d m"
by (simp add: args_to_set_subset_Times[OF sps_sub], rule, fact+)
qed
moreover have gs_bs_sub: "fst ` (set gs ∪ set bs) ⊆ dgrad_p_set d m" by (simp add: image_Un, rule, fact+)
ultimately have res_sub: "fst ` (set gs ∪ set bs) ∪ fst ` set ?res ⊆ dgrad_p_set d m" by simp
from ‹(p, q) ∈ set sps› ‹set sps ⊆ set ps› ps_sub
have "fst p ∈ fst ` set bs" and "fst q ∈ fst ` (set gs ∪ set bs)" by auto
with ‹fst ` set bs ⊆ dgrad_p_set d m› gs_bs_sub
have "fst p ∈ dgrad_p_set d m" and "fst q ∈ dgrad_p_set d m" by auto
with dg res_sub show "crit_pair_cbelow_on d m (fst ` (set gs ∪ set bs) ∪ fst ` set ?res) (fst p) (fst q)"
using ‹fst p ≠ 0› ‹fst q ≠ 0›
proof (rule spoly_red_zero_imp_crit_pair_cbelow_on)
from assms gb uid sps_sub ‹(p, q) ∈ set sps›
show "(red (fst ` (set gs ∪ set bs) ∪ fst ` set (fst (rcp gs bs (ps -- sps) sps data))))⇧*⇧*
(spoly (fst p) (fst q)) 0"
by (rule rcp_specD6)
qed
qed
end
subsection ‹Suitable Instances of the @{emph ‹add-basis›} Parameter›
definition add_basis_naive :: "('a, 'b, 'c, 'd) abT"
where "add_basis_naive gs bs ns data = bs @ ns"
lemma ab_spec_add_basis_naive: "ab_spec add_basis_naive"
by (rule ab_specI, simp_all add: add_basis_naive_def)
definition add_basis_sorted :: "(nat × 'd ⇒ ('a, 'b, 'c) pdata ⇒ ('a, 'b, 'c) pdata ⇒ bool) ⇒ ('a, 'b, 'c, 'd) abT"
where "add_basis_sorted rel gs bs ns data = merge_wrt (rel data) bs ns"
lemma ab_spec_add_basis_sorted: "ab_spec (add_basis_sorted rel)"
by (rule ab_specI, simp_all add: add_basis_sorted_def set_merge_wrt)
definition card_keys :: "('a ⇒⇩0 'b::zero) ⇒ nat"
where "card_keys = card ∘ keys"
definition (in ordered_term) canon_basis_order :: "'d ⇒ ('t, 'b::zero, 'c) pdata ⇒ ('t, 'b, 'c) pdata ⇒ bool"
where "canon_basis_order data p q ⟷
(let cp = card_keys (fst p); cq = card_keys (fst q) in
cp < cq ∨ (cp = cq ∧ lt (fst p) ≺⇩t lt (fst q)))"
abbreviation (in ordered_term) "add_basis_canon ≡ add_basis_sorted canon_basis_order"
subsection ‹Special Case: Scalar Polynomials›
context gd_powerprod
begin
lemma remdups_map_component_of_term_punit:
"remdups (map (λ_. ()) (punit.Keys_to_list (map fst bs))) =
(if (∀b∈set bs. fst b = 0) then [] else [()])"
proof (split if_split, intro conjI impI)
assume "∀b∈set bs. fst b = 0"
hence "fst ` set bs ⊆ {0}" by blast
hence "Keys (fst ` set bs) = {}" by (metis Keys_empty Keys_zero subset_singleton_iff)
hence "punit.Keys_to_list (map fst bs) = []"
by (simp add: set_empty[symmetric] punit.set_Keys_to_list del: set_empty)
thus "remdups (map (λ_. ()) (punit.Keys_to_list (map fst bs))) = []" by simp
next
assume "¬ (∀b∈set bs. fst b = 0)"
hence "∃b∈set bs. fst b ≠ 0" by simp
then obtain b where "b ∈ set bs" and "fst b ≠ 0" ..
hence "Keys (fst ` set bs) ≠ {}" by (meson Keys_not_empty ‹fst b ≠ 0› imageI)
hence "set (punit.Keys_to_list (map fst bs)) ≠ {}" by (simp add: punit.set_Keys_to_list)
hence "punit.Keys_to_list (map fst bs) ≠ []" by simp
thus "remdups (map (λ_. ()) (punit.Keys_to_list (map fst bs))) = [()]"
by (metis (full_types) remdups_adj.cases old.unit.exhaust Nil_is_map_conv ‹punit.Keys_to_list (map fst bs) ≠ []› distinct_length_2_or_more distinct_remdups remdups_eq_nil_right_iff)
qed
lemma count_const_lt_components_punit [code]:
"punit.count_const_lt_components hs =
(if (∃h∈set hs. punit.const_lt_component (fst h) = Some ()) then 1 else 0)"
proof (simp add: punit.count_const_lt_components_def cong del: image_cong_simp,
simp add: card_set [symmetric] cong del: image_cong_simp, rule)
assume "∃h∈set hs. punit.const_lt_component (fst h) = Some ()"
then obtain h where "h ∈ set hs" and "punit.const_lt_component (fst h) = Some ()" ..
from this(2) have "(punit.const_lt_component ∘ fst) h = Some ()" by simp
with ‹h ∈ set hs› have "Some () ∈ (punit.const_lt_component ∘ fst) ` set hs"
by (metis rev_image_eqI)
hence "{x. x = Some () ∧ x ∈ (punit.const_lt_component ∘ fst) ` set hs} = {Some ()}" by auto
thus "card {x. x = Some () ∧ x ∈ (punit.const_lt_component ∘ fst) ` set hs} = Suc 0" by simp
qed
lemma count_rem_components_punit [code]:
"punit.count_rem_components bs =
(if (∀b∈set bs. fst b = 0) then 0
else
if (∃b∈set bs. fst b ≠ 0 ∧ punit.const_lt_component (fst b) = Some ()) then 0 else 1)"
proof (cases "∀b∈set bs. fst b = 0")
case True
thus ?thesis by (simp add: punit.count_rem_components_def remdups_map_component_of_term_punit)
next
case False
have eq: "(∃b∈set [b←bs . fst b ≠ 0]. punit.const_lt_component (fst b) = Some ()) =
(∃b∈set bs. fst b ≠ 0 ∧ punit.const_lt_component (fst b) = Some ())"
by (metis (mono_tags, lifting) filter_set member_filter)
show ?thesis
by (simp only: False punit.count_rem_components_def eq if_False
remdups_map_component_of_term_punit count_const_lt_components_punit punit_component_of_term, simp)
qed
lemma full_gb_punit [code]:
"punit.full_gb bs = (if (∀b∈set bs. fst b = 0) then [] else [(1, 0, default)])"
by (simp add: punit.full_gb_def remdups_map_component_of_term_punit)
abbreviation "add_pairs_punit_canon ≡
punit.add_pairs (punit.new_pairs_sorted punit.canon_pair_order) punit.product_crit punit.chain_ncrit
punit.chain_ocrit punit.canon_pair_comb"
lemma ap_spec_add_pairs_punit_canon: "punit.ap_spec add_pairs_punit_canon"
using punit.np_spec_new_pairs_sorted punit.icrit_spec_product_crit punit.ncrit_spec_chain_ncrit
punit.ocrit_spec_chain_ocrit set_merge_wrt
by (rule punit.ap_spec_add_pairs)
end
end