Theory PAC_Specification
theory PAC_Specification
imports PAC_More_Poly
begin
section ‹Specification of the PAC checker›
subsection ‹Ideals›
type_synonym int_poly = ‹int mpoly›
definition polynomial_bool :: ‹int_poly set› where
‹polynomial_bool = (λc. Var c ^ 2 - Var c) ` UNIV›
definition pac_ideal where
‹pac_ideal A ≡ ideal (A ∪ polynomial_bool)›
lemma X2_X_in_pac_ideal:
‹Var c ^ 2 - Var c ∈ pac_ideal A›
unfolding polynomial_bool_def pac_ideal_def
by (auto intro: ideal.span_base)
lemma pac_idealI1[intro]:
‹p ∈ A ⟹ p ∈ pac_ideal A›
unfolding pac_ideal_def
by (auto intro: ideal.span_base)
lemma pac_idealI2[intro]:
‹p ∈ ideal A ⟹ p ∈ pac_ideal A›
using ideal.span_subspace_induct pac_ideal_def by blast
lemma pac_idealI3[intro]:
‹p ∈ ideal A ⟹ p*q ∈ pac_ideal A›
by (metis ideal.span_scale mult.commute pac_idealI2)
lemma pac_ideal_Xsq2_iff:
‹Var c ^ 2 ∈ pac_ideal A ⟷ Var c ∈ pac_ideal A›
unfolding pac_ideal_def
apply (subst (2) ideal.span_add_eq[symmetric, OF X2_X_in_pac_ideal[of c, unfolded pac_ideal_def]])
apply auto
done
lemma diff_in_polynomial_bool_pac_idealI:
assumes a1: "p ∈ pac_ideal A"
assumes a2: "p - p' ∈ More_Modules.ideal polynomial_bool"
shows ‹p' ∈ pac_ideal A›
proof -
have "insert p polynomial_bool ⊆ pac_ideal A"
using a1 unfolding pac_ideal_def by (meson ideal.span_superset insert_subset le_sup_iff)
then show ?thesis
using a2 unfolding pac_ideal_def by (metis (no_types) ideal.eq_span_insert_eq ideal.span_subset_spanI ideal.span_superset insert_subset subsetD)
qed
lemma diff_in_polynomial_bool_pac_idealI2:
assumes a1: "p ∈ A"
assumes a2: "p - p' ∈ More_Modules.ideal polynomial_bool"
shows ‹p' ∈ pac_ideal A›
using diff_in_polynomial_bool_pac_idealI[OF _ assms(2), of A] assms(1)
by (auto simp: ideal.span_base)
lemma pac_ideal_alt_def:
‹pac_ideal A = ideal (A ∪ ideal polynomial_bool)›
unfolding pac_ideal_def
by (meson ideal.span_eq ideal.span_mono ideal.span_superset le_sup_iff subset_trans sup_ge2)
text ‹
The equality on ideals is restricted to polynomials whose variable
appear in the set of ideals. The function restrict sets:
›
definition restricted_ideal_to where
‹restricted_ideal_to B A = {p ∈ A. vars p ⊆ B}›
abbreviation restricted_ideal_to⇩I where
‹restricted_ideal_to⇩I B A ≡ restricted_ideal_to B (pac_ideal (set_mset A))›
abbreviation restricted_ideal_to⇩V where
‹restricted_ideal_to⇩V B ≡ restricted_ideal_to (⋃(vars ` set_mset B))›
abbreviation restricted_ideal_to⇩V⇩I where
‹restricted_ideal_to⇩V⇩I B A ≡ restricted_ideal_to (⋃(vars ` set_mset B)) (pac_ideal (set_mset A))›
lemma restricted_idealI:
‹p ∈ pac_ideal (set_mset A) ⟹ vars p ⊆ C ⟹ p ∈ restricted_ideal_to⇩I C A›
unfolding restricted_ideal_to_def
by auto
lemma pac_ideal_insert_already_in:
‹pq ∈ pac_ideal (set_mset A) ⟹ pac_ideal (insert pq (set_mset A)) = pac_ideal (set_mset A)›
by (auto simp: pac_ideal_alt_def ideal.span_insert_idI)
lemma pac_ideal_add:
‹p ∈# A ⟹ q ∈# A ⟹ p + q ∈ pac_ideal (set_mset A)›
by (simp add: ideal.span_add ideal.span_base pac_ideal_def)
lemma pac_ideal_mult:
‹p ∈# A ⟹ p * q ∈ pac_ideal (set_mset A)›
by (simp add: ideal.span_base pac_idealI3)
lemma pac_ideal_mono:
‹A ⊆ B ⟹ pac_ideal A ⊆ pac_ideal B›
using ideal.span_mono[of ‹A ∪ _› ‹B ∪ _›]
by (auto simp: pac_ideal_def intro: ideal.span_mono)
subsection ‹PAC Format›
text ‹The PAC format contains three kind of steps:
▪ ▩‹add› that adds up two polynomials that are known.
▪ ▩‹mult› that multiply a known polynomial with another one.
▪ ▩‹del› that removes a polynomial that cannot be reused anymore.
To model the simplification that happens, we add the \<^term>‹p - p' ∈ polynomial_bool›
stating that \<^term>‹p› and \<^term>‹p'› are equivalent.
›
type_synonym pac_st = ‹(nat set × int_poly multiset)›
inductive PAC_Format :: ‹pac_st ⇒ pac_st ⇒ bool› where
add:
‹PAC_Format (𝒱, A) (𝒱, add_mset p' A)›
if
‹p ∈# A› ‹q ∈# A›
‹p+q - p' ∈ ideal polynomial_bool›
‹vars p' ⊆ 𝒱› |
mult:
‹PAC_Format (𝒱, A) (𝒱, add_mset p' A)›
if
‹p ∈# A›
‹p*q - p' ∈ ideal polynomial_bool›
‹vars p' ⊆ 𝒱›
‹vars q ⊆ 𝒱› |
del:
‹p ∈# A ⟹ PAC_Format (𝒱, A) (𝒱, A - {#p#})› |
extend_pos:
‹PAC_Format (𝒱, A) (𝒱 ∪ {x' ∈ vars (-Var x + p'). x' ∉ 𝒱}, add_mset (-Var x + p') A)›
if
‹(p')⇧2 - p' ∈ ideal polynomial_bool›
‹vars p' ⊆ 𝒱›
‹x ∉ 𝒱›
text ‹
In the PAC format above, we have a technical condition on the
normalisation: \<^term>‹vars p' ⊆ vars (p + q)› is here to ensure that
we don't normalise \<^term>‹0 :: int mpoly› to \<^term>‹Var x^2 - Var x :: int mpoly›
for a new variable \<^term>‹x :: nat›. This is completely obvious for the normalisation
process we have in mind when we write the specification, but we must add it
explicitly because we are too general.
›
lemmas PAC_Format_induct_split =
PAC_Format.induct[split_format(complete), of V A V' A' for V A V' A']
lemma PAC_Format_induct[consumes 1, case_names add mult del ext]:
assumes
‹PAC_Format (𝒱, A) (𝒱', A')› and
cases:
‹⋀p q p' A 𝒱. p ∈# A ⟹ q ∈# A ⟹ p+q - p' ∈ ideal polynomial_bool ⟹ vars p' ⊆ 𝒱 ⟹ P 𝒱 A 𝒱 (add_mset p' A)›
‹⋀p q p' A 𝒱. p ∈# A ⟹ p*q - p' ∈ ideal polynomial_bool ⟹ vars p' ⊆ 𝒱 ⟹ vars q ⊆ 𝒱 ⟹
P 𝒱 A 𝒱 (add_mset p' A)›
‹⋀p A 𝒱. p ∈# A ⟹ P 𝒱 A 𝒱 (A - {#p#})›
‹⋀p' x r.
(p')^2 - (p') ∈ ideal polynomial_bool ⟹ vars p' ⊆ 𝒱 ⟹
x ∉ 𝒱 ⟹ P 𝒱 A (𝒱 ∪ {x' ∈ vars (p' - Var x). x' ∉ 𝒱}) (add_mset (p' -Var x) A)›
shows
‹P 𝒱 A 𝒱' A'›
using assms(1) apply -
by (induct V≡𝒱 A≡A 𝒱' A' rule: PAC_Format_induct_split)
(auto intro: assms(1) cases)
text ‹
The theorem below (based on the proof ideal by Manuel Kauers) is the
correctness theorem of extensions. Remark that the assumption \<^term>‹vars
q ⊆ 𝒱› is only used to show that \<^term>‹x' ∉ vars q›.
›
lemma extensions_are_safe:
assumes ‹x' ∈ vars p› and
x': ‹x' ∉ 𝒱› and
‹⋃ (vars ` set_mset A) ⊆ 𝒱› and
p_x_coeff: ‹coeff p (monomial (Suc 0) x') = 1› and
vars_q: ‹vars q ⊆ 𝒱› and
q: ‹q ∈ More_Modules.ideal (insert p (set_mset A ∪ polynomial_bool))› and
leading: ‹x' ∉ vars (p - Var x')› and
diff: ‹(Var x' - p)⇧2 - (Var x' - p) ∈ More_Modules.ideal polynomial_bool›
shows
‹q ∈ More_Modules.ideal (set_mset A ∪ polynomial_bool)›
proof -
define p' where ‹p' ≡ p - Var x'›
let ?v = ‹Var x' :: int mpoly›
have p_p': ‹p = ?v + p'›
by (auto simp: p'_def)
define q' where ‹q' ≡ Var x' - p›
have q_q': ‹p = ?v - q'›
by (auto simp: q'_def)
have diff: ‹q'^2 - q' ∈ More_Modules.ideal polynomial_bool›
using diff unfolding q_q' by auto
have [simp]: ‹vars ((Var c)⇧2 - Var c :: int mpoly) = {c}› for c
apply (auto simp: vars_def Var_def Var⇩0_def mpoly.MPoly_inverse keys_def lookup_minus_fun
lookup_times_monomial_right single.rep_eq split: if_splits)
apply (auto simp: vars_def Var_def Var⇩0_def mpoly.MPoly_inverse keys_def lookup_minus_fun
lookup_times_monomial_right single.rep_eq when_def ac_simps adds_def lookup_plus_fun
power2_eq_square times_mpoly.rep_eq minus_mpoly.rep_eq split: if_splits)
apply (rule_tac x = ‹(2 :: nat ⇒⇩0 nat) * monomial (Suc 0) c› in exI)
apply (auto dest: monomial_0D simp: plus_eq_zero_2 lookup_plus_fun mult_2)
by (meson Suc_neq_Zero monomial_0D plus_eq_zero_2)
have eq: ‹More_Modules.ideal (insert p (set_mset A ∪ polynomial_bool)) =
More_Modules.ideal (insert p (set_mset A ∪ (λc. Var c ^ 2 - Var c) ` {c. c ≠ x'}))›
(is ‹?A = ?B› is ‹_ = More_Modules.ideal ?trimmed›)
proof -
let ?C = ‹insert p (set_mset A ∪ (λc. Var c ^ 2 - Var c) ` {c. c ≠ x'})›
let ?D = ‹(λc. Var c ^ 2 - Var c) ` {c. c ≠ x'}›
have diff: ‹q'^2 - q' ∈ More_Modules.ideal ?D› (is ‹?q ∈ _›)
proof -
obtain r t where
q: ‹?q = (∑a∈t. r a * a)› and
fin_t: ‹finite t› and
t: ‹t ⊆ polynomial_bool›
using diff unfolding ideal.span_explicit
by auto
show ?thesis
proof (cases ‹?v^2-?v ∉ t›)
case True
then show ‹?thesis›
using q fin_t t unfolding ideal.span_explicit
by (auto intro!: exI[of _ ‹t - {?v^2 -?v}›] exI[of _ r]
simp: polynomial_bool_def sum_diff1)
next
case False
define t' where ‹t' = t - {?v^2 - ?v}›
have t_t': ‹t = insert (?v^2 - ?v) t'› and
notin: ‹?v^2 - ?v ∉ t'› and
‹t' ⊆ (λc. Var c ^ 2 - Var c) ` {c. c ≠ x'}›
using False t unfolding t'_def polynomial_bool_def by auto
have mon: ‹monom (monomial (Suc 0) x') 1 = Var x'›
by (auto simp: coeff_def minus_mpoly.rep_eq Var_def Var⇩0_def monom_def
times_mpoly.rep_eq lookup_minus lookup_times_monomial_right mpoly.MPoly_inverse)
then have ‹∀a. ∃g h. r a = ?v * g + h ∧ x' ∉ vars h›
using polynomial_split_on_var[of ‹r _› x']
by metis
then obtain g h where
r: ‹r a = ?v * g a + h a› and
x'_h: ‹x' ∉ vars (h a)› for a
using polynomial_split_on_var[of ‹r a› x']
by metis
have ‹?q = ((∑a∈t'. g a * a) + r (?v^2-?v) * (?v - 1)) * ?v + (∑a∈t'. h a * a)›
using fin_t notin unfolding t_t' q r
by (auto simp: field_simps comm_monoid_add_class.sum.distrib
power2_eq_square ideal.scale_left_commute sum_distrib_left)
moreover have ‹x' ∉ vars ?q›
by (metis (no_types, opaque_lifting) Groups.add_ac(2) Un_iff add_diff_cancel_left'
diff_minus_eq_add in_mono leading q'_def semiring_normalization_rules(29)
vars_in_right_only vars_mult)
moreover {
have ‹x' ∉ (⋃m∈t' - {?v^2-?v}. vars (h m * m))›
using fin_t x'_h vars_mult[of ‹h _›] ‹t ⊆ polynomial_bool›
by (auto simp: polynomial_bool_def t_t' elim!: vars_unE)
then have ‹x' ∉ vars (∑a∈t'. h a * a)›
using vars_setsum[of ‹t'› ‹λa. h a * a›] fin_t x'_h t notin
by (auto simp: t_t')
}
ultimately have ‹?q = (∑a∈t'. h a * a)›
unfolding mon[symmetric]
by (rule polynomial_decomp_alien_var(2)[unfolded])
then show ?thesis
using t fin_t ‹t' ⊆ (λc. Var c ^ 2 - Var c) ` {c. c ≠ x'}›
unfolding ideal.span_explicit t_t'
by auto
qed
qed
have eq1: ‹More_Modules.ideal (insert p (set_mset A ∪ polynomial_bool)) =
More_Modules.ideal (insert (?v^2 - ?v) ?C)›
(is ‹More_Modules.ideal _ = More_Modules.ideal (insert _ ?C)›)
by (rule arg_cong[of _ _ More_Modules.ideal])
(auto simp: polynomial_bool_def)
moreover have ‹?v^2 - ?v ∈ More_Modules.ideal ?C›
proof -
have ‹?v - q' ∈ More_Modules.ideal ?C›
by (auto simp: q_q' ideal.span_base)
from ideal.span_scale[OF this, of ‹?v + q' - 1›] have ‹(?v - q') * (?v + q' - 1) ∈ More_Modules.ideal ?C›
by (auto simp: field_simps)
moreover have ‹q'^2 - q' ∈ More_Modules.ideal ?C›
using diff by (smt (verit) Un_insert_right ideal.span_mono insert_subset subsetD sup_ge2)
ultimately have ‹(?v - q') * (?v + q' - 1) + (q'^2 - q') ∈ More_Modules.ideal ?C›
by (rule ideal.span_add)
moreover have ‹?v^2 - ?v = (?v - q') * (?v + q' - 1) + (q'^2 - q')›
by (auto simp: p'_def q_q' field_simps power2_eq_square)
ultimately show ?thesis by simp
qed
ultimately show ?thesis
using ideal.span_insert_idI by blast
qed
have ‹n < m ⟹ n > 0 ⟹ ∃q. ?v^n = ?v + q * (?v^2 - ?v)› for n m :: nat
proof (induction m arbitrary: n)
case 0
then show ?case by auto
next
case (Suc m n) note IH = this(1-)
consider
‹n < m› |
‹m = n› ‹n > 1› |
‹n = 1›
using IH
by (cases ‹n < m›; cases n) auto
then show ?case
proof cases
case 1
then show ?thesis using IH by auto
next
case 2
have eq: ‹?v^(n) = ((?v :: int mpoly) ^ (n-2)) * (?v^2-?v) + ?v^(n-1)›
using 2 by (auto simp: field_simps power_eq_if
ideal.scale_right_diff_distrib)
obtain q where
q: ‹?v^(n-1) = ?v + q * (?v^2 - ?v)›
using IH(1)[of ‹n-1›] 2
by auto
show ?thesis
using q unfolding eq
by (auto intro!: exI[of _ ‹Var x' ^ (n - 2) + q›] simp: distrib_right)
next
case 3
then show ‹?thesis›
by auto
qed
qed
obtain r t where
q: ‹q = (∑a∈t. r a * a)› and
fin_t: ‹finite t› and
t: ‹t ⊆ ?trimmed›
using q unfolding eq unfolding ideal.span_explicit
by auto
define t' where ‹t' ≡ t - {p}›
have t': ‹t = (if p ∈ t then insert p t' else t')› and
t''[simp]: ‹p ∉ t'›
unfolding t'_def by auto
show ?thesis
proof (cases ‹r p = 0 ∨ p ∉ t›)
case True
have
q: ‹q = (∑a∈t'. r a * a)› and
fin_t: ‹finite t'› and
t: ‹t' ⊆ set_mset A ∪ polynomial_bool›
using q fin_t t True t''
apply (subst (asm) t')
apply (auto intro: sum.cong simp: sum.insert_remove t'_def)
using q fin_t t True t''
apply (auto intro: sum.cong simp: sum.insert_remove t'_def polynomial_bool_def)
done
then show ?thesis
by (auto simp: ideal.span_explicit)
next
case False
then have ‹r p ≠ 0› and ‹p ∈ t›
by auto
then have t: ‹t = insert p t'›
by (auto simp: t'_def)
have ‹x' ∉ vars (- p')›
using leading p'_def vars_in_right_only by fastforce
have mon: ‹monom (monomial (Suc 0) x') 1 = Var x'›
by (auto simp:coeff_def minus_mpoly.rep_eq Var_def Var⇩0_def monom_def
times_mpoly.rep_eq lookup_minus lookup_times_monomial_right mpoly.MPoly_inverse)
then have ‹∀a. ∃g h. r a = (?v + p') * g + h ∧ x' ∉ vars h›
using polynomial_split_on_var2[of x' ‹-p'› ‹r _›] ‹x' ∉ vars (- p')›
by (metis diff_minus_eq_add)
then obtain g h where
r: ‹r a = p * g a + h a› and
x'_h: ‹x' ∉ vars (h a)› for a
using polynomial_split_on_var2[of x' p' ‹r a›] unfolding p_p'[symmetric]
by metis
have ISABLLE_come_on: ‹a * (p * g a) = p * (a * g a)› for a
by auto
have q1: ‹q = p * (∑a∈t'. g a * a) + (∑a∈t'. h a * a) + p * r p›
(is ‹_ = _ + ?NOx' + _›)
using fin_t t'' unfolding q t ISABLLE_come_on r
apply (subst semiring_class.distrib_right)+
apply (auto simp: comm_monoid_add_class.sum.distrib semigroup_mult_class.mult.assoc
ISABLLE_come_on simp flip: semiring_0_class.sum_distrib_right
semiring_0_class.sum_distrib_left)
by (auto simp: field_simps)
also have ‹... = ((∑a∈t'. g a * a) + r p) * p + (∑a∈t'. h a * a)›
by (auto simp: field_simps)
finally have q_decomp: ‹q = ((∑a∈t'. g a * a) + r p) * p + (∑a∈t'. h a * a)›
(is ‹q = ?X * p + ?NOx'›).
have [iff]: ‹monomial (Suc 0) c = 0 - monomial (Suc 0) c = False› for c
by (metis One_nat_def diff_is_0_eq' le_eq_less_or_eq less_Suc_eq_le monomial_0_iff single_diff zero_neq_one)
have ‹x ∈ t' ⟹ x' ∈ vars x ⟹ False› for x
using ‹t ⊆ ?trimmed› t assms(2,3)
apply (auto simp: polynomial_bool_def dest!: multi_member_split)
apply (frule set_rev_mp)
apply assumption
apply (auto dest!: multi_member_split)
done
then have ‹x' ∉ (⋃m∈t'. vars (h m * m))›
using fin_t x'_h vars_mult[of ‹h _›]
by (auto simp: t elim!: vars_unE)
then have ‹x' ∉ vars ?NOx'›
using vars_setsum[of ‹t'› ‹λa. h a * a›] fin_t x'_h
by (auto simp: t)
moreover {
have ‹x' ∉ vars p'›
using assms(7)
unfolding p'_def
by auto
then have ‹x' ∉ vars (h p * p')›
using vars_mult[of ‹h p› p'] x'_h
by auto
}
ultimately have
‹x' ∉ vars q›
‹x' ∉ vars ?NOx'›
‹x' ∉ vars p'›
using x' vars_q vars_add[of ‹h p * p'› ‹∑a∈t'. h a * a›] x'_h
leading p'_def
by auto
then have ‹?X = 0› and q_decomp: ‹q = ?NOx'›
unfolding mon[symmetric] p_p'
using polynomial_decomp_alien_var2[OF q_decomp[unfolded p_p' mon[symmetric]]]
by auto
then have ‹r p = (∑a∈t'. (- g a) * a)›
(is ‹_ = ?CL›)
unfolding add.assoc add_eq_0_iff equation_minus_iff
by (auto simp: sum_negf ac_simps)
then have q2: ‹q = (∑a∈t'. a * (r a - p * g a))›
using fin_t unfolding q
apply (auto simp: t r q
comm_monoid_add_class.sum.distrib[symmetric]
sum_distrib_left
sum_distrib_right
left_diff_distrib
intro!: sum.cong)
apply (auto simp: field_simps)
done
then show ‹?thesis›
using t fin_t ‹t ⊆ ?trimmed› unfolding ideal.span_explicit
by (auto intro!: exI[of _ t'] exI[of _ ‹λa. r a - p * g a›]
simp: field_simps polynomial_bool_def)
qed
qed
lemma extensions_are_safe_uminus:
assumes ‹x' ∈ vars p› and
x': ‹x' ∉ 𝒱› and
‹⋃ (vars ` set_mset A) ⊆ 𝒱› and
p_x_coeff: ‹coeff p (monomial (Suc 0) x') = -1› and
vars_q: ‹vars q ⊆ 𝒱› and
q: ‹q ∈ More_Modules.ideal (insert p (set_mset A ∪ polynomial_bool))› and
leading: ‹x' ∉ vars (p + Var x')› and
diff: ‹(Var x' + p)^2 - (Var x' + p) ∈ More_Modules.ideal polynomial_bool›
shows
‹q ∈ More_Modules.ideal (set_mset A ∪ polynomial_bool)›
proof -
have ‹q ∈ More_Modules.ideal (insert (- p) (set_mset A ∪ polynomial_bool))›
by (metis ideal.span_breakdown_eq minus_mult_minus q)
then show ?thesis
using extensions_are_safe[of x' ‹-p› 𝒱 A q] assms
using vars_in_right_only by force
qed
text ‹This is the correctness theorem of a PAC step: no polynomials are
added to the ideal.›
lemma vars_subst_in_left_only:
‹x ∉ vars p ⟹ x ∈ vars (p - Var x)› for p :: ‹int mpoly›
by (metis One_nat_def Var.abs_eq Var⇩0_def group_eq_aux monom.abs_eq mult_numeral_1 polynomial_decomp_alien_var(1) zero_neq_numeral)
lemma vars_subst_in_left_only_diff_iff:
fixes p :: ‹int mpoly›
assumes ‹x ∉ vars p›
shows ‹vars (p - Var x) = insert x (vars p)›
proof -
have ‹⋀xa. x ∉ vars p ⟹ xa ∈ vars (p - Var x) ⟹ xa ∉ vars p ⟹ xa = x›
by (metis (no_types, opaque_lifting) diff_0_right diff_minus_eq_add empty_iff in_vars_addE insert_iff
keys_single minus_diff_eq monom_one mult.right_neutral one_neq_zero single_zero
vars_monom_keys vars_mult_Var vars_uminus)
moreover have ‹⋀xa. x ∉ vars p ⟹ xa ∈ vars p ⟹ xa ∈ vars (p - Var x)›
by (metis add.inverse_inverse diff_minus_eq_add empty_iff insert_iff keys_single minus_diff_eq
monom_one mult.right_neutral one_neq_zero single_zero vars_in_right_only vars_monom_keys
vars_mult_Var vars_uminus)
ultimately show ?thesis
using assms
by (auto simp: vars_subst_in_left_only)
qed
lemma vars_subst_in_left_only_iff:
‹x ∉ vars p ⟹ vars (p + Var x) = insert x (vars p)› for p :: ‹int mpoly›
using vars_subst_in_left_only_diff_iff[of x ‹-p›]
by (metis diff_0 diff_diff_add vars_uminus)
lemma coeff_add_right_notin:
‹x ∉ vars p ⟹ MPoly_Type.coeff (Var x - p) (monomial (Suc 0) x) = 1›
apply (auto simp flip: coeff_minus simp: not_in_vars_coeff0)
by (simp add: MPoly_Type.coeff_def Var.rep_eq Var⇩0_def)
lemma coeff_add_left_notin:
‹x ∉ vars p ⟹ MPoly_Type.coeff (p - Var x) (monomial (Suc 0) x) = -1› for p :: ‹int mpoly›
apply (auto simp flip: coeff_minus simp: not_in_vars_coeff0)
by (simp add: MPoly_Type.coeff_def Var.rep_eq Var⇩0_def)
lemma ideal_insert_polynomial_bool_swap: ‹r - s ∈ ideal polynomial_bool ⟹
More_Modules.ideal (insert r (A ∪ polynomial_bool)) = More_Modules.ideal (insert s (A ∪ polynomial_bool))›
apply auto
using ideal.eq_span_insert_eq ideal.span_mono sup_ge2 apply blast+
done
lemma PAC_Format_subset_ideal:
‹PAC_Format (𝒱, A) (𝒱', B) ⟹ ⋃(vars ` set_mset A) ⊆ 𝒱 ⟹
restricted_ideal_to⇩I 𝒱 B ⊆ restricted_ideal_to⇩I 𝒱 A ∧ 𝒱 ⊆ 𝒱' ∧ ⋃(vars ` set_mset B) ⊆ 𝒱'›
unfolding restricted_ideal_to_def
apply (induction rule:PAC_Format_induct)
subgoal for p q pq A 𝒱
using vars_add
by (force simp: ideal.span_add_eq ideal.span_base pac_ideal_insert_already_in[OF diff_in_polynomial_bool_pac_idealI[of ‹p + q› ‹_› pq]]
pac_ideal_add
intro!: diff_in_polynomial_bool_pac_idealI[of ‹p + q› ‹_› pq])
subgoal for p q pq
using vars_mult[of p q]
by (force simp: ideal.span_add_eq ideal.span_base pac_ideal_mult
pac_ideal_insert_already_in[OF diff_in_polynomial_bool_pac_idealI[of ‹p*q› ‹_› pq]])
subgoal for p A
using pac_ideal_mono[of ‹set_mset (A - {#p#})› ‹set_mset A›]
by (auto dest: in_diffD)
subgoal for p x' r'
apply (subgoal_tac ‹x' ∉ vars p›)
using extensions_are_safe_uminus[of x' ‹-Var x' + p› 𝒱 A] unfolding pac_ideal_def
apply (auto simp: vars_subst_in_left_only coeff_add_left_notin)
done
done
text ‹
In general, if deletions are disallowed, then the stronger \<^term>‹B = pac_ideal A› holds.
›
lemma restricted_ideal_to_restricted_ideal_to⇩ID:
‹restricted_ideal_to 𝒱 (set_mset A) ⊆ restricted_ideal_to⇩I 𝒱 A›
by (auto simp add: Collect_disj_eq pac_idealI1 restricted_ideal_to_def)
lemma rtranclp_PAC_Format_subset_ideal:
‹rtranclp PAC_Format (𝒱, A) (𝒱', B) ⟹ ⋃(vars ` set_mset A) ⊆ 𝒱 ⟹
restricted_ideal_to⇩I 𝒱 B ⊆ restricted_ideal_to⇩I 𝒱 A ∧ 𝒱 ⊆ 𝒱' ∧ ⋃(vars ` set_mset B) ⊆ 𝒱'›
apply (induction rule:rtranclp_induct[of PAC_Format ‹(_, _)› ‹(_, _)›, split_format(complete)])
subgoal
by (simp add: restricted_ideal_to_restricted_ideal_to⇩ID)
subgoal
by (drule PAC_Format_subset_ideal)
(auto simp: restricted_ideal_to_def Collect_mono_iff)
done
end