Theory PAC_More_Poly
theory PAC_More_Poly
imports "HOL-Library.Poly_Mapping" "HOL-Algebra.Polynomials" "Polynomials.MPoly_Type_Class"
"HOL-Algebra.Module" "HOL-Library.Countable_Set"
begin
section ‹Overview›
text ‹
One solution to check circuit of multipliers is to use algebraic method, like producing proofs on
polynomials. We are here interested in checking PAC proofs on the Boolean ring. The idea is the
following: each variable represents an input or the output of a gate and we want to prove the
bitwise multiplication of the input bits yields the output, namely the bitwise representation of the
multiplication of the input (modulo \<^term>‹(2::nat)^n› where \<^term>‹n::nat› is the number of bits of the
circuit).
Algebraic proof systems typically reason over polynomials in a ring $\set K[X]$,
where the variables $X$ represent Boolean values.
The aim of an algebraic proof is to derive whether a polynomial $f$ can be derived from a given set of polynomials
$G = \{g_1,\dots,g_l\} \subseteq \set K[X]$ together with the Boolean value constraints
$B(X) = \{x^2_i-x_i \mid x_i \in X\}$. In algebraic terms this means to show that the polynomial \<^latex>‹\(f \in \langle G \cup B(X)\rangle\)›.
In our setting we set $\set K = \set Z$ and we treat the Boolean value constraints implicitly, i.e.,
we consider proofs in the ring \<^latex>‹\(\set Z[X]/\langle B(X)\rangle\)› to admit shorter proofs
The checker takes as input 3 files:
▸ an input file containing all polynomials that are initially present;
▸ a target (or specification) polynomial ;
▸ a ``proof'' file to check that contains the proof in PAC format that shows that the specification
is in the ideal generated by the polynomials present initially.
Each step of the proof is either an addition of two polynomials previously derived, a multiplication
from a previously derived polynomial and an arbitrary polynomial, and the deletion a derived
polynomial.
One restriction on the proofs compared to generic PAC proofs is that \<^term>‹(x::nat)^2 = x› in the
Boolean ring we are considering.
The checker can produce two outputs: valid (meaning that each derived polynomial in the proof has
been correctly derived and the specification polynomial was also derived at some point [either in
the proof or as input]) or invalid (without proven information what went wrong).
The development is organised as follows:
▪ 🗏‹PAC_Specification.thy› (this file) contains the specification as described above on ideals
without any peculiarities on the PAC proof format
▪ 🗏‹PAC_Checker_Specification.thy› specialises to the PAC format and enters the nondeterminism
monad to prepare the subsequent refinements.
▪ 🗏‹PAC_Checker.thy› contains the refined version where polynomials are represented as lists.
▪ 🗏‹PAC_Checker_Synthesis.thy› contains the efficient implementation with imperative data
structure like a hash set.
▪ 🗏‹PAC_Checker_MLton.thy› contains the code generation and the command to compile the file with
the ML compiler MLton.
Here is an example of a proof and an input file (taken from the appendix of our FMCAD
paper~\<^cite>‹"KaufmannFleuryBiere-FMCAD20"›, available at 🌐‹http://fmv.jku.at/pacheck_pasteque›):
▩‹
<res.input> <res.proof>
1 x*y; 3 = fz, -z+1;
2 y*z-y-z+1; 4 * 3, y-1, -fz*y+fz-y*z+y+z-1;
5 + 2, 4, -fz*y+fz;
2 d;
4 d;
<res.target> 6 * 1, fz, fz*x*y;
-x*z+x; 1 d;
7 * 5, x, -fz*x*y+fz*x;
8 + 6, 7, fz*x;
9 * 3, x, -fz*x-x*z+x;
10 + 8, 9, -x*z+x;
›
Each line starts with a number that is used to index the (conclusion) polynomial. In the proof,
there are four kind of steps:
▸ ▩‹3 = fz, -z+1;› is an extension that introduces a new variable (in this case ▩‹fz›);
▸ ▩‹4 * 3, y-1, -fz*y+fz-y*z+y+z-1;› is a multiplication of the existing polynomial with
index 3 by the arbitrary polynomial ▩‹y-1› and generates the new polynomial
▩‹-fz*y+fz-y*z+y+z-1› with index 4;
▸ ▩‹5 + 2, 4, -fz*y+fz;› is an addition of the existing polynomials with
index 2 and 4 and generates the new polynomial ▩‹-fz*y+fz› with index 5;
▸ ▩‹1 d;› deletes the polynomial with index 1 and it cannot be reused in subsequent steps.
Remark that unlike DRAT checker, we do forward checking and check every derived polynomial. The
target polynomial can also be part of the input file.
›
section ‹Libraries›
subsection ‹More Polynomials›
text ‹
Here are more theorems on polynomials. Most of these facts are
extremely trivial and should probably be generalised and moved to
the Isabelle distribution.
›
lemma Const⇩0_add:
‹Const⇩0 (a + b) = Const⇩0 a + Const⇩0 b›
by transfer
(simp add: Const⇩0_def single_add)
lemma Const_mult:
‹Const (a * b) = Const a * Const b›
by transfer (simp add: Const⇩0_def times_monomial_monomial)
lemma Const⇩0_mult:
‹Const⇩0 (a * b) = Const⇩0 a * Const⇩0 b›
by transfer (simp add: Const⇩0_def times_monomial_monomial)
lemma Const0[simp]:
‹Const 0 = 0›
by transfer (simp add: Const⇩0_def)
lemma (in -) Const_uminus[simp]:
‹Const (-n) = - Const n›
by transfer (auto simp: Const⇩0_def monomial_uminus)
lemma [simp]: ‹Const⇩0 0 = 0›
‹MPoly 0 = 0›
by (auto simp: Const⇩0_def zero_mpoly_def)
lemma Const_add:
‹Const (a + b) = Const a + Const b›
by transfer (simp add: Const⇩0_def single_add)
instance mpoly :: (comm_semiring_1) comm_semiring_1
by standard
lemma degree_uminus[simp]:
‹degree (-A) x' = degree A x'›
by (auto simp: degree_def uminus_mpoly.rep_eq)
lemma degree_sum_notin:
‹x' ∉ vars B ⟹ degree (A + B) x' = degree A x'›
apply (auto simp: degree_def)
apply (rule arg_cong[of _ _ Max])
apply standard+
apply (auto simp: plus_mpoly.rep_eq UN_I UnE image_iff in_keys_iff subsetD vars_def lookup_add
dest: keys_add intro: in_keys_plusI1 cong: ball_cong_simp)
done
lemma degree_notin_vars:
‹x ∉ (vars B) ⟹ degree (B :: 'a :: {monoid_add} mpoly) x = 0›
using degree_sum_notin[of x B 0]
by auto
lemma not_in_vars_coeff0:
‹x ∉ vars p ⟹ MPoly_Type.coeff p (monomial (Suc 0) x) = 0›
by (subst not_not[symmetric], subst coeff_keys[symmetric])
(auto simp: vars_def)
lemma keys_add':
"p ∈ keys (f + g) ⟹ p ∈ keys f ∪ keys g"
by transfer auto
lemma keys_mapping_sum_add:
‹finite A ⟹ keys (mapping_of (∑v ∈ A. f v)) ⊆ ⋃(keys ` mapping_of ` f ` UNIV)›
by (induction A rule: finite_induct)
(auto simp add: zero_mpoly.rep_eq plus_mpoly.rep_eq
keys_plus_ninv_comm_monoid_add dest: keys_add')
lemma vars_sum_vars_union:
fixes f :: ‹int mpoly ⇒ int mpoly›
assumes ‹finite {v. f v ≠ 0}›
shows ‹vars (∑v | f v ≠ 0. f v * v) ⊆ ⋃(vars ` {v. f v ≠ 0}) ∪ ⋃(vars ` f ` {v. f v ≠ 0})›
(is ‹?A ⊆ ?B›)
proof
fix p
assume ‹p ∈ vars (∑v | f v ≠ 0. f v * v)›
then obtain x where ‹x ∈ keys (mapping_of (∑v | f v ≠ 0. f v * v))› and
p: ‹p ∈ keys x›
by (auto simp: vars_def times_mpoly.rep_eq simp del: keys_mult)
then have ‹x ∈ (⋃x. keys (mapping_of (f x) * mapping_of x))›
using keys_mapping_sum_add[of ‹{v. f v ≠ 0}› ‹λx. f x * x›] assms
by (auto simp: vars_def times_mpoly.rep_eq)
then have ‹x ∈ (⋃x. {a+b| a b. a ∈ keys (mapping_of (f x)) ∧ b ∈ keys (mapping_of x)})›
using Union_mono[OF ] keys_mult by fast
then show ‹p ∈ ?B›
using p by (force simp: vars_def zero_mpoly.rep_eq dest!: keys_add')
qed
lemma vars_in_right_only:
"x ∈ vars q ⟹ x ∉ vars p ⟹ x ∈ vars (p+q)"
unfolding vars_def keys_def plus_mpoly.rep_eq lookup_plus_fun
apply clarify
subgoal for xa
by (auto simp: vars_def keys_def plus_mpoly.rep_eq
lookup_plus_fun intro!: exI[of _ xa] dest!: spec[of _ xa])
done
lemma [simp]:
‹vars 0 = {}›
by (simp add: vars_def zero_mpoly.rep_eq)
lemma vars_Un_nointer:
‹keys (mapping_of p) ∩ keys (mapping_of q) = {} ⟹ vars (p + q) = vars p ∪ vars q›
by (auto simp: vars_def plus_mpoly.rep_eq simp flip: More_MPoly_Type.keys_add dest!: keys_add')
lemmas [simp] = zero_mpoly.rep_eq
lemma polynomial_sum_monoms:
fixes p :: ‹'a :: {comm_monoid_add,cancel_comm_monoid_add} mpoly›
shows
‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))›
‹keys (mapping_of p) ⊆ I ⟹ finite I ⟹ p = (∑x∈I. MPoly_Type.monom x (MPoly_Type.coeff p x))›
proof -
define J where ‹J ≡ keys (mapping_of p)›
define a where ‹a x ≡ coeff p x› for x
have ‹finite (keys (mapping_of p))›
by auto
have ‹p = (∑x∈I. MPoly_Type.monom x (MPoly_Type.coeff p x))›
if ‹finite I› and ‹keys (mapping_of p) ⊆ I›
for I
using that
unfolding a_def
proof (induction I arbitrary: p rule: finite_induct)
case empty
then have ‹p = 0›
using empty coeff_all_0 coeff_keys by blast
then show ?case using empty by (auto simp: zero_mpoly.rep_eq)
next
case (insert x F) note fin = this(1) and xF = this(2) and IH = this(3) and
incl = this(4)
let ?p = ‹p - MPoly_Type.monom x (MPoly_Type.coeff p x)›
have H: ‹⋀xa. x ∉ F ⟹ xa ∈ F ⟹
MPoly_Type.monom xa (MPoly_Type.coeff (p - MPoly_Type.monom x (MPoly_Type.coeff p x)) xa) =
MPoly_Type.monom xa (MPoly_Type.coeff p xa)›
by (metis (mono_tags, opaque_lifting) add_diff_cancel_right' remove_term_coeff
remove_term_sum when_def)
have ‹?p = (∑xa∈F. MPoly_Type.monom xa (MPoly_Type.coeff ?p xa))›
apply (rule IH)
using incl apply -
by standard (smt (verit) Diff_iff Diff_insert_absorb add_diff_cancel_right'
remove_term_keys remove_term_sum subsetD xF)
also have ‹... = (∑xa∈F. MPoly_Type.monom xa (MPoly_Type.coeff p xa))›
by (use xF in ‹auto intro!: sum.cong simp: H›)
finally show ?case
apply (subst (asm) remove_term_sum[of x p, symmetric])
apply (subst remove_term_sum[of x p, symmetric])
using xF fin by (auto simp: ac_simps)
qed
from this[of I] this[of J] show
‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))›
‹keys (mapping_of p) ⊆ I ⟹ finite I ⟹ p = (∑x∈I. MPoly_Type.monom x (MPoly_Type.coeff p x))›
by (auto simp: J_def)
qed
lemma vars_mult_monom:
fixes p :: ‹int mpoly›
shows ‹vars (p * (monom (monomial (Suc 0) x') 1)) = (if p = 0 then {} else insert x' (vars p))›
proof -
let ?v = ‹monom (monomial (Suc 0) x') 1›
have
p: ‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))› (is ‹_ = (∑x ∈ ?I. ?f x)›)
using polynomial_sum_monoms(1)[of p] .
have pv: ‹p * ?v = (∑x ∈ ?I. ?f x * ?v)›
by (subst p) (auto simp: field_simps sum_distrib_left)
define I where ‹I ≡ ?I›
have in_keysD: ‹x ∈ keys (mapping_of (∑x∈I. MPoly_Type.monom x (h x))) ⟹ x ∈ I›
if ‹finite I› for I and h :: ‹_ ⇒ int› and x
using that by (induction rule: finite_induct)
(force simp: monom.rep_eq empty_iff insert_iff keys_single coeff_monom
simp: coeff_keys simp flip: coeff_add
simp del: coeff_add)+
have in_keys: ‹keys (mapping_of (∑x∈I. MPoly_Type.monom x (h x))) = (⋃x ∈ I. (if h x = 0 then {} else {x}))›
if ‹finite I› for I and h :: ‹_ ⇒ int› and x
supply in_keysD[dest]
using that by (induction rule: finite_induct)
(auto simp: plus_mpoly.rep_eq MPoly_Type_Class.keys_plus_eqI)
have H[simp]: ‹vars ((∑x∈I. MPoly_Type.monom x (h x))) = (⋃x∈I. (if h x = 0 then {} else keys x))›
if ‹finite I› for I and h :: ‹_ ⇒ int›
using that by (auto simp: vars_def in_keys)
have sums: ‹(∑x∈I.
MPoly_Type.monom (x + a') (c x)) =
(∑x∈ (λx. x + a') ` I.
MPoly_Type.monom x (c (x - a')))›
if ‹finite I› for I a' c q
using that apply (induction rule: finite_induct)
subgoal by auto
subgoal
unfolding image_insert by (subst sum.insert) auto
done
have non_zero_keysEx: ‹p ≠ 0 ⟹ ∃a. a ∈ keys (mapping_of p)› for p :: ‹int mpoly›
using mapping_of_inject by (fastforce simp add: ex_in_conv)
have ‹finite I› ‹keys (mapping_of p) ⊆ I›
unfolding I_def by auto
then show
‹vars (p * (monom (monomial (Suc 0) x') 1)) = (if p = 0 then {} else insert x' (vars p))›
apply (subst pv, subst I_def[symmetric], subst mult_monom)
apply (auto simp: mult_monom sums I_def)
using Poly_Mapping.keys_add vars_def apply fastforce
apply (auto dest!: non_zero_keysEx)
apply (rule_tac x= ‹a + monomial (Suc 0) x'› in bexI)
apply (auto simp: coeff_keys)
apply (simp add: in_keys_iff lookup_add)
apply (auto simp: vars_def)
apply (rule_tac x= ‹xa + monomial (Suc 0) x'› in bexI)
apply (auto simp: coeff_keys)
apply (simp add: in_keys_iff lookup_add)
done
qed
term ‹(x', u, lookup u x', A)›
lemma in_mapping_mult_single:
‹x ∈ (λx. lookup x x') ` keys (A * (Var⇩0 x' :: (nat ⇒⇩0 nat) ⇒⇩0 'b :: {monoid_mult,zero_neq_one,semiring_0})) ⟷
x > 0 ∧ x - 1 ∈ (λx. lookup x x') ` keys (A)›
apply (standard+; clarify)
subgoal
apply (auto elim!: in_keys_timesE simp: lookup_add)
apply (auto simp: keys_def lookup_times_monomial_right Var⇩0_def lookup_single image_iff)
done
subgoal
apply (auto elim!: in_keys_timesE simp: lookup_add)
apply (auto simp: keys_def lookup_times_monomial_right Var⇩0_def lookup_single image_iff)
done
subgoal for xa
apply (auto elim!: in_keys_timesE simp: lookup_add)
apply (auto simp: keys_def lookup_times_monomial_right Var⇩0_def lookup_single image_iff lookup_add
intro!: exI[of _ ‹xa + Poly_Mapping.single x' 1›])
done
done
lemma Max_Suc_Suc_Max:
‹finite A ⟹ A ≠ {} ⟹ Max (insert 0 (Suc ` A)) =
Suc (Max (insert 0 A))›
by (induction rule: finite_induct)
(auto simp: hom_Max_commute)
lemma [simp]:
‹keys (Var⇩0 x' :: ('a ⇒⇩0 nat) ⇒⇩0 'b :: {zero_neq_one}) = {Poly_Mapping.single x' 1}›
by (auto simp: Var⇩0_def)
lemma degree_mult_Var:
‹degree (A * Var x') x' = (if A = 0 then 0 else Suc (degree A x'))› for A :: ‹int mpoly›
proof -
have [simp]: ‹A ≠ 0 ⟹
Max (insert 0 ((λx. Suc (lookup x x')) ` keys (mapping_of A))) =
Max (insert (Suc 0) ((λx. Suc (lookup x x')) ` keys (mapping_of A)))›
unfolding image_image[of Suc ‹λx. lookup x x'›, symmetric] image_insert[symmetric]
by (subst Max_Suc_Suc_Max, use mapping_of_inject in fastforce, use mapping_of_inject in fastforce)+
(simp add: Max.hom_commute)
have ‹A ≠ 0 ⟹
Max (insert 0
((λx. lookup x x') `
keys (mapping_of A * mapping_of (Var x')))) =
Suc (Max (insert 0 ((λm. lookup m x') ` keys (mapping_of A))))›
by (subst arg_cong[of _ ‹insert 0
(Suc ` ((λx. lookup x x') ` keys (mapping_of A)))› Max])
(auto simp: image_image Var.rep_eq lookup_plus_fun in_mapping_mult_single
hom_Max_commute Max_Suc_Suc_Max
elim!: in_keys_timesE split: if_splits)
then show ?thesis
by (auto simp: degree_def times_mpoly.rep_eq
intro!: arg_cong[of _ ‹insert 0
(Suc ` ((λx. lookup x x') ` keys (mapping_of A)))› Max])
qed
lemma degree_mult_Var':
‹degree (Var x' * A) x' = (if A = 0 then 0 else Suc (degree A x'))› for A :: ‹int mpoly›
by (simp add: degree_mult_Var semiring_normalization_rules(7))
lemma degree_times_le:
‹degree (A * B) x ≤ degree A x + degree B x›
by (auto simp: degree_def times_mpoly.rep_eq
max_def lookup_add add_mono
dest!: set_rev_mp[OF _ Poly_Mapping.keys_add]
elim!: in_keys_timesE)
lemma monomial_inj:
"monomial c s = monomial (d::'b::zero_neq_one) t ⟷ (c = 0 ∧ d = 0) ∨ (c = d ∧ s = t)"
by (fastforce simp add: monomial_inj Poly_Mapping.single_def
poly_mapping.Abs_poly_mapping_inject when_def fun_eq_iff
cong: if_cong
split: if_splits)
lemma MPoly_monomial_power':
‹MPoly (monomial 1 x') ^ (n+1) = MPoly (monomial (1) (((λx. x + x') ^^ n) x'))›
by (induction n)
(auto simp: times_mpoly.abs_eq mult_single ac_simps)
lemma MPoly_monomial_power:
‹n > 0 ⟹ MPoly (monomial 1 x') ^ (n) = MPoly (monomial (1) (((λx. x + x') ^^ (n - 1)) x'))›
using MPoly_monomial_power'[of _ ‹n-1›]
by auto
lemma vars_uminus[simp]:
‹vars (-p) = vars p›
by (auto simp: vars_def uminus_mpoly.rep_eq)
lemma coeff_uminus[simp]:
‹MPoly_Type.coeff (-p) x = -MPoly_Type.coeff p x›
by (auto simp: coeff_def uminus_mpoly.rep_eq)
definition decrease_key::"'a ⇒ ('a ⇒⇩0 'b::{monoid_add, minus,one}) ⇒ ('a ⇒⇩0 'b)" where
"decrease_key k0 f = Abs_poly_mapping (λk. if k = k0 ∧ lookup f k ≠ 0 then lookup f k - 1 else lookup f k)"
lemma remove_key_lookup:
"lookup (decrease_key k0 f) k = (if k = k0 ∧ lookup f k ≠ 0 then lookup f k - 1 else lookup f k)"
unfolding decrease_key_def using finite_subset apply simp
apply (subst lookup_Abs_poly_mapping)
apply (auto intro: finite_subset[of _ ‹{x. lookup f x ≠ 0}›])
apply (subst lookup_Abs_poly_mapping)
apply (auto intro: finite_subset[of _ ‹{x. lookup f x ≠ 0}›])
done
lemma polynomial_split_on_var:
fixes p :: ‹'a :: {comm_monoid_add,cancel_comm_monoid_add,semiring_0,comm_semiring_1} mpoly›
obtains q r where
‹p = monom (monomial (Suc 0) x') 1 * q + r› and
‹x' ∉ vars r›
proof -
have [simp]: ‹{x ∈ keys (mapping_of p). x' ∈ keys x} ∪
{x ∈ keys (mapping_of p). x' ∉ keys x} = keys (mapping_of p)›
by auto
have
‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))› (is ‹_ = (∑x ∈ ?I. ?f x)›)
using polynomial_sum_monoms(1)[of p] .
also have ‹... = (∑x∈ {x ∈ ?I. x' ∈ keys x}. ?f x) + (∑x∈ {x ∈ ?I. x' ∉ keys x}. ?f x)› (is ‹_ = ?pX + ?qX›)
by (subst comm_monoid_add_class.sum.union_disjoint[symmetric]) auto
finally have 1: ‹p = ?pX + ?qX› .
have H: ‹0 < lookup x x' ⟹ (λk. (if x' = k then Suc 0 else 0) +
(if k = x' ∧ 0 < lookup x k then lookup x k - 1
else lookup x k)) = lookup x› for x x'
by auto
have [simp]: ‹finite {x. 0 < (Suc 0 when x' = x)}› for x' :: nat and x
by (smt (verit) bounded_nat_set_is_finite lessI mem_Collect_eq neq0_conv when_cong when_neq_zero)
have H: ‹x' ∈ keys x ⟹ monomial (Suc 0) x' + Abs_poly_mapping (λk. if k = x' ∧ 0 < lookup x k then lookup x k - 1 else lookup x k) = x›
for x and x' :: nat
apply (simp only: keys_def single.abs_eq)
apply (subst plus_poly_mapping.abs_eq)
by (auto simp: eq_onp_def when_def H
intro!: finite_subset[of ‹{xa. (xa = x' ∧ 0 < lookup x xa ⟶ Suc 0 < lookup x x') ∧
(xa ≠ x' ⟶ 0 < lookup x xa)}› ‹{xa. 0 < lookup x xa}›])
have [simp]: ‹x' ∈ keys x ⟹
MPoly_Type.monom (monomial (Suc 0) x' + decrease_key x' x) n =
MPoly_Type.monom x n› for x n and x'
apply (subst mpoly.mapping_of_inject[symmetric], subst poly_mapping.lookup_inject[symmetric])
unfolding mapping_of_monom lookup_single
apply (auto intro!: ext simp: decrease_key_def when_def H)
done
have pX: ‹?pX = monom (monomial (Suc 0) x') 1 * (∑x∈ {x ∈ ?I. x' ∈ keys x}. MPoly_Type.monom (decrease_key x' x) (MPoly_Type.coeff p x))›
(is ‹_ = _ * ?pX'›)
by (subst sum_distrib_left, subst mult_monom)
(auto intro!: sum.cong)
have ‹x' ∉ vars ?qX›
using vars_setsum[of ‹{x. x ∈ keys (mapping_of p) ∧ x' ∉ keys x}› ‹?f›]
by (auto dest!: vars_monom_subset[unfolded subset_eq Ball_def, rule_format])
then show ?thesis
using that[of ?pX' ?qX]
unfolding pX[symmetric] 1[symmetric]
by blast
qed
lemma polynomial_split_on_var2:
fixes p :: ‹int mpoly›
assumes ‹x' ∉ vars s›
obtains q r where
‹p = (monom (monomial (Suc 0) x') 1 - s) * q + r› and
‹x' ∉ vars r›
proof -
have eq[simp]: ‹monom (monomial (Suc 0) x') 1 = Var x'›
by (simp add: Var.abs_eq Var⇩0_def monom.abs_eq)
have ‹∀m ≤ n. ∀P::int mpoly. degree P x' < m ⟶ (∃A B. P = (Var x' - s) * A + B ∧ x' ∉ vars B)› for n
proof (induction n)
case 0
then show ?case by auto
next
case (Suc n)
then have IH: ‹m≤n ⟹ MPoly_Type.degree P x' < m ⟹
(∃A B. P = (Var x' - s) * A + B ∧ x' ∉ vars B)› for m P
by fast
show ?case
proof (intro allI impI)
fix m and P :: ‹int mpoly›
assume ‹m ≤ Suc n› and deg: ‹MPoly_Type.degree P x' < m›
consider
‹m ≤ n› |
‹m = Suc n›
using ‹m ≤ Suc n› by linarith
then show ‹∃A B. P = (Var x' - s) * A + B ∧ x' ∉ vars B›
proof cases
case 1
then show ‹?thesis›
using Suc deg by blast
next
case [simp]: 2
obtain A B where
P: ‹P = Var x' * A + B› and
‹x' ∉ vars B›
using polynomial_split_on_var[of P x'] unfolding eq by blast
have P': ‹P = (Var x' - s) * A + (s * A + B)›
by (auto simp: field_simps P)
have ‹A = 0 ∨ degree (s * A) x' < degree P x'›
using deg ‹x' ∉ vars B› ‹x' ∉ vars s› degree_times_le[of s A x'] deg
unfolding P
by (auto simp: degree_sum_notin degree_mult_Var' degree_mult_Var degree_notin_vars
split: if_splits)
then obtain A' B' where
sA: ‹s*A = (Var x' - s) * A' + B'› and
‹x' ∉ vars B'›
using IH[of ‹m-1› ‹s*A›] deg ‹x' ∉ vars B› that[of 0 0]
by (cases ‹0 < n›) (auto dest!: vars_in_right_only)
have ‹P = (Var x' - s) * (A + A') + (B' + B)›
unfolding P' sA by (auto simp: field_simps)
moreover have ‹x' ∉ vars (B' + B)›
using ‹x' ∉ vars B'› ‹x' ∉ vars B›
by (meson UnE subset_iff vars_add)
ultimately show ?thesis
by fast
qed
qed
qed
then show ?thesis
using that unfolding eq
by blast
qed
lemma finit_whenI[intro]:
‹finite {x. (0 :: nat) < (y x)} ⟹ finite {x. 0 < (y x when x ≠ x')}›
apply (rule finite_subset)
defer apply assumption
apply (auto simp: when_def)
done
lemma polynomial_split_on_var_diff_sq2:
fixes p :: ‹int mpoly›
obtains q r s where
‹p = monom (monomial (Suc 0) x') 1 * q + r + s * (monom (monomial (Suc 0) x') 1^2 - monom (monomial (Suc 0) x') 1)› and
‹x' ∉ vars r› and
‹x' ∉ vars q›
proof -
let ?v = ‹monom (monomial (Suc 0) x') 1 :: int mpoly›
have H: ‹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 _ ‹?v ^ (n - 2) + q›] simp: distrib_right)
next
case 3
then show ‹?thesis›
by auto
qed
qed
have H: ‹n>0 ⟹ ∃q. ?v^n = ?v + q * (?v^2-?v)› for n
using H[of n ‹n+1›]
by auto
obtain qr :: ‹nat ⇒ int mpoly› where
qr: ‹n > 0 ⟹ ?v^n = ?v + qr n * (?v^2-?v)› for n
using H by metis
have vn: ‹(if lookup x x' = 0 then 1 else Var x' ^ lookup x x') =
(if lookup x x' = 0 then 1 else ?v) + (if lookup x x' = 0 then 0 else 1) * qr (lookup x x') * (?v^2-?v)› for x
by (simp add: qr[symmetric] Var_def Var⇩0_def monom.abs_eq[symmetric] cong: if_cong)
have q: ‹p = (∑x∈keys (mapping_of p). MPoly_Type.monom x (MPoly_Type.coeff p x))›
by (rule polynomial_sum_monoms(1)[of p])
have [simp]:
‹lookup x x' = 0 ⟹
Abs_poly_mapping (λk. lookup x k when k ≠ x') = x› for x
by (cases x, auto simp: poly_mapping.Abs_poly_mapping_inject)
(auto intro!: ext simp: when_def)
have [simp]: ‹finite {x. 0 < (a when x' = x)}› for a :: nat
by (metis (no_types, lifting) infinite_nat_iff_unbounded less_not_refl lookup_single lookup_single_not_eq mem_Collect_eq)
have [simp]: ‹((λx. x + monomial (Suc 0) x') ^^ (n))
(monomial (Suc 0) x') = Abs_poly_mapping (λk. (if k = x' then n+1 else 0))› for n
by (induction n)
(auto simp: single_def Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def cong:if_cong)
have [simp]: ‹0 < lookup x x' ⟹
Abs_poly_mapping (λk. lookup x k when k ≠ x') +
Abs_poly_mapping (λk. if k = x' then lookup x x' - Suc 0 + 1 else 0) =
x› for x
apply (cases x, auto simp: poly_mapping.Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def)
apply (subst plus_poly_mapping.abs_eq)
apply (auto simp: poly_mapping.Abs_poly_mapping_inject plus_poly_mapping.abs_eq eq_onp_def)
apply (subst Abs_poly_mapping_inject)
apply auto
done
define f where
‹f x = (MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)) *
(if lookup x x' = 0 then 1 else Var x' ^ (lookup x x'))› for x
have f_alt_def: ‹f x = MPoly_Type.monom x (MPoly_Type.coeff p x)› for x
by (auto simp: f_def monom_def remove_key_def Var_def MPoly_monomial_power Var⇩0_def
mpoly.MPoly_inject monomial_inj times_mpoly.abs_eq
times_mpoly.abs_eq mult_single)
have p: ‹p = (∑x∈keys (mapping_of p).
MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
(if lookup x x' = 0 then 1 else ?v)) +
(∑x∈keys (mapping_of p).
MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
(if lookup x x' = 0 then 0
else 1) * qr (lookup x x')) *
(?v⇧2 - ?v)›
(is ‹_ = ?a + ?v2v›)
apply (subst q)
unfolding f_alt_def[symmetric, abs_def] f_def vn semiring_class.distrib_left
comm_semiring_1_class.semiring_normalization_rules(18) semiring_0_class.sum_distrib_right
by (simp add: semiring_class.distrib_left
sum.distrib)
have I: ‹keys (mapping_of p) = {x ∈ keys (mapping_of p). lookup x x' = 0} ∪ {x ∈ keys (mapping_of p). lookup x x' ≠ 0}›
by auto
have ‹p = (∑x | x ∈ keys (mapping_of p) ∧ lookup x x' = 0.
MPoly_Type.monom x (MPoly_Type.coeff p x)) +
(∑x | x ∈ keys (mapping_of p) ∧ lookup x x' ≠ 0.
MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)) *
(MPoly_Type.monom (monomial (Suc 0) x') 1) +
(∑x | x ∈ keys (mapping_of p) ∧ lookup x x' ≠ 0.
MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
qr (lookup x x')) *
(?v⇧2 - ?v)›
(is ‹p = ?A + ?B * _ + ?C * _›)
unfolding semiring_0_class.sum_distrib_right[of _ _ ‹(MPoly_Type.monom (monomial (Suc 0) x') 1)›]
apply (subst p)
apply (subst (2)I)
apply (subst I)
apply (subst comm_monoid_add_class.sum.union_disjoint)
apply auto[3]
apply (subst comm_monoid_add_class.sum.union_disjoint)
apply auto[3]
apply (subst (4) sum.cong[OF refl, of _ _ ‹λx. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
qr (lookup x x')›])
apply (auto; fail)
apply (subst (3) sum.cong[OF refl, of _ _ ‹λx. 0›])
apply (auto; fail)
apply (subst (2) sum.cong[OF refl, of _ _ ‹λx. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x) *
(MPoly_Type.monom (monomial (Suc 0) x') 1)›])
apply (auto; fail)
apply (subst (1) sum.cong[OF refl, of _ _ ‹λx. MPoly_Type.monom x (MPoly_Type.coeff p x)›])
by (auto simp: f_def simp flip: f_alt_def)
moreover have ‹x' ∉ vars ?A›
using vars_setsum[of ‹{x ∈ keys (mapping_of p). lookup x x' = 0}›
‹λx. MPoly_Type.monom x (MPoly_Type.coeff p x)›]
apply auto
apply (drule set_rev_mp, assumption)
apply (auto dest!: lookup_eq_zero_in_keys_contradict)
by (meson lookup_eq_zero_in_keys_contradict subsetD vars_monom_subset)
moreover have ‹x' ∉ vars ?B›
using vars_setsum[of ‹{x ∈ keys (mapping_of p). lookup x x' ≠ 0}›
‹λx. MPoly_Type.monom (remove_key x' x) (MPoly_Type.coeff p x)›]
apply auto
apply (drule set_rev_mp, assumption)
apply (auto dest!: lookup_eq_zero_in_keys_contradict)
apply (drule subsetD[OF vars_monom_subset])
apply (auto simp: remove_key_keys[symmetric])
done
ultimately show ?thesis apply -
apply (rule that[of ?B ?A ?C])
apply (auto simp: ac_simps)
done
qed
lemma polynomial_decomp_alien_var:
fixes q A b :: ‹int mpoly›
assumes
q: ‹q = A * (monom (monomial (Suc 0) x') 1) + b› and
x: ‹x' ∉ vars q› ‹x' ∉ vars b›
shows
‹A = 0› and
‹q = b›
proof -
let ?A = ‹A * (monom (monomial (Suc 0) x') 1)›
have ‹?A = q - b›
using arg_cong[OF q, of ‹λa. a - b›]
by auto
moreover have ‹x' ∉ vars (q - b)›
using x vars_in_right_only
by fastforce
ultimately have ‹x' ∉ vars (?A)›
by simp
then have ‹?A = 0›
by (auto simp: vars_mult_monom split: if_splits)
moreover have ‹?A = 0 ⟹ A = 0›
by (metis empty_not_insert mult_zero_left vars_mult_monom)
ultimately show ‹A = 0›
by blast
then show ‹q = b›
using q by auto
qed
lemma polynomial_decomp_alien_var2:
fixes q A b :: ‹int mpoly›
assumes
q: ‹q = A * (monom (monomial (Suc 0) x') 1 + p) + b› and
x: ‹x' ∉ vars q› ‹x' ∉ vars b› ‹x' ∉ vars p›
shows
‹A = 0› and
‹q = b›
proof -
let ?x = ‹monom (monomial (Suc 0) x') 1›
have x'[simp]: ‹?x = Var x'›
by (simp add: Var.abs_eq Var⇩0_def monom.abs_eq)
have ‹∃n Ax A'. A = ?x * Ax + A' ∧ x' ∉ vars A' ∧ degree Ax x' = n›
using polynomial_split_on_var[of A x'] by metis
from wellorder_class.exists_least_iff[THEN iffD1, OF this] obtain Ax A' n where
A: ‹A = Ax * ?x + A'› and
‹x' ∉ vars A'› and
n: ‹MPoly_Type.degree Ax x' = n› and
H: ‹⋀m Ax A'. m < n ⟶
A ≠ Ax * MPoly_Type.monom (monomial (Suc 0) x') 1 + A' ∨
x' ∈ vars A' ∨ MPoly_Type.degree Ax x' ≠ m›
unfolding wellorder_class.exists_least_iff[of ‹λn. ∃Ax A'. A = Ax * ?x + A' ∧ x' ∉ vars A' ∧
degree Ax x' = n›]
by (auto simp: field_simps)
have ‹q = (A + Ax * p) * monom (monomial (Suc 0) x') 1 + (p * A' + b)›
unfolding q A by (auto simp: field_simps)
moreover have ‹x' ∉ vars q› ‹x' ∉ vars (p * A' + b)›
using x ‹x' ∉ vars A'›
by (smt (verit) UnE add.assoc add.commute calculation subset_iff vars_in_right_only vars_mult)+
ultimately have ‹A + Ax * p = 0› ‹q = p * A' + b›
by (rule polynomial_decomp_alien_var)+
have A': ‹A' = -Ax * ?x - Ax * p›
using ‹A + Ax * p = 0› unfolding A
by (metis (no_types, lifting) add_uminus_conv_diff eq_neg_iff_add_eq_0 minus_add_cancel
mult_minus_left)
have ‹A = - (Ax * p)›
using A unfolding A'
apply auto
done
obtain Axx Ax' where
Ax: ‹Ax = ?x * Axx + Ax'› and
‹x' ∉ vars Ax'›
using polynomial_split_on_var[of Ax x'] by metis
have ‹A = ?x * (- Axx * p) + (- Ax' * p)›
unfolding ‹A = - (Ax * p)› Ax
by (auto simp: field_simps)
moreover have ‹x' ∉ vars (-Ax' * p)›
using ‹x' ∉ vars Ax'› by (metis (no_types, opaque_lifting) UnE add.right_neutral
add_minus_cancel assms(4) subsetD vars_in_right_only vars_mult)
moreover have ‹Axx ≠ 0 ⟹ MPoly_Type.degree (- Axx * p) x' < degree Ax x'›
using degree_times_le[of Axx p x'] x
by (auto simp: Ax degree_sum_notin ‹x' ∉ vars Ax'› degree_mult_Var'
degree_notin_vars)
ultimately have [simp]: ‹Axx = 0›
using H[of ‹MPoly_Type.degree (- Axx * p) x'› ‹- Axx * p› ‹- Ax' * p›]
by (auto simp: n)
then have [simp]: ‹Ax' = Ax›
using Ax by auto
show ‹A = 0›
using A ‹A = - (Ax * p)› ‹x' ∉ vars (- Ax' * p)› ‹x' ∉ vars A'› polynomial_decomp_alien_var(1) by force
then show ‹q = b›
using q by auto
qed
lemma vars_unE: ‹x ∈ vars (a * b) ⟹ (x ∈ vars a ⟹ thesis) ⟹ (x ∈ vars b ⟹ thesis) ⟹ thesis›
using vars_mult[of a b] by auto
lemma in_keys_minusI1:
assumes "t ∈ keys p" and "t ∉ keys q"
shows "t ∈ keys (p - q)"
using assms unfolding in_keys_iff lookup_minus by simp
lemma in_keys_minusI2:
fixes t :: ‹'a› and q :: ‹'a ⇒⇩0 'b :: {cancel_comm_monoid_add,group_add}›
assumes "t ∈ keys q" and "t ∉ keys p"
shows "t ∈ keys (p - q)"
using assms unfolding in_keys_iff lookup_minus by simp
lemma in_vars_addE:
‹x ∈ vars (p + q) ⟹ (x ∈ vars p ⟹ thesis) ⟹ (x ∈ vars q ⟹ thesis) ⟹ thesis›
by (meson UnE in_mono vars_add)
lemma lookup_monomial_If:
‹lookup (monomial v k) = (λk'. if k = k' then v else 0)›
by (intro ext) (auto simp: lookup_single_not_eq)
lemma vars_mult_Var:
‹vars (Var x * p) = (if p = 0 then {} else insert x (vars p))› for p :: ‹int mpoly›
proof -
have ‹p ≠ 0 ⟹
∃xa. (∃k. xa = monomial (Suc 0) x + k) ∧
lookup (mapping_of p) (xa - monomial (Suc 0) x) ≠ 0 ∧
0 < lookup xa x›
by (metis (no_types, opaque_lifting) One_nat_def ab_semigroup_add_class.add.commute
add_diff_cancel_right' aux lookup_add lookup_single_eq mapping_of_inject
neq0_conv one_neq_zero plus_eq_zero_2 zero_mpoly.rep_eq)
then show ?thesis
apply (auto simp: vars_def times_mpoly.rep_eq Var.rep_eq
elim!: in_keys_timesE dest: keys_add')
apply (auto simp: keys_def lookup_times_monomial_left Var.rep_eq Var⇩0_def adds_def
lookup_add eq_diff_eq'[symmetric])
done
qed
lemma keys_mult_monomial:
‹keys (monomial (n :: int) k * mapping_of a) = (if n = 0 then {} else ((+) k) ` keys (mapping_of a))›
proof -
have [simp]: ‹(∑aa. (if k = aa then n else 0) *
(∑q. lookup (mapping_of a) q when k + xa = aa + q)) =
(∑aa. (if k = aa then n * (∑q. lookup (mapping_of a) q when k + xa = aa + q) else 0))›
for xa
by (smt (verit) Sum_any.cong mult_not_zero)
show ?thesis
apply (auto simp: vars_def times_mpoly.rep_eq Const.rep_eq times_poly_mapping.rep_eq
Const⇩0_def elim!: in_keys_timesE split: if_splits)
apply (auto simp: lookup_monomial_If prod_fun_def
keys_def times_poly_mapping.rep_eq)
done
qed
lemma vars_mult_Const:
‹vars (Const n * a) = (if n = 0 then {} else vars a)› for a :: ‹int mpoly›
by (auto simp: vars_def times_mpoly.rep_eq Const.rep_eq keys_mult_monomial
Const⇩0_def elim!: in_keys_timesE split: if_splits)
lemma coeff_minus: "coeff p m - coeff q m = coeff (p-q) m"
by (simp add: coeff_def lookup_minus minus_mpoly.rep_eq)
lemma Const_1_eq_1: ‹Const (1 :: int) = (1 :: int mpoly)›
by (simp add: Const.abs_eq Const⇩0_one one_mpoly.abs_eq)
lemma [simp]:
‹vars (1 :: int mpoly) = {}›
by (auto simp: vars_def one_mpoly.rep_eq Const_1_eq_1)
subsection ‹More Ideals›
lemma
fixes A :: ‹(('x ⇒⇩0 nat) ⇒⇩0 'a::comm_ring_1) set›
assumes ‹p ∈ ideal A›
shows ‹p * q ∈ ideal A›
by (metis assms ideal.span_scale semiring_normalization_rules(7))
text ‹The following theorem is very close to @{thm ideal.span_insert}, except that it
is more useful if we need to take an element of \<^term>‹More_Modules.ideal (insert a S)›.›
lemma ideal_insert':
‹More_Modules.ideal (insert a S) = {y. ∃x k. y = x + k * a ∧ x ∈ More_Modules.ideal S}›
apply (auto simp: ideal.span_insert
intro: exI[of _ ‹_ - k * a›])
apply (rule_tac x = ‹x - k * a› in exI)
apply auto
apply (rule_tac x = ‹k› in exI)
apply auto
done
lemma ideal_mult_right_in:
‹a ∈ ideal A ⟹ a * b ∈ More_Modules.ideal A›
by (metis ideal.span_scale mult.commute)
lemma ideal_mult_right_in2:
‹a ∈ ideal A ⟹ b * a ∈ More_Modules.ideal A›
by (metis ideal.span_scale)
lemma [simp]: ‹vars (Var x :: 'a :: {zero_neq_one} mpoly) = {x}›
by (auto simp: vars_def Var.rep_eq Var⇩0_def)
lemma vars_minus_Var_subset:
‹vars (p' - Var x :: 'a :: {ab_group_add,one,zero_neq_one} mpoly) ⊆ 𝒱 ⟹ vars p' ⊆ insert x 𝒱›
using vars_add[of ‹p' - Var x› ‹Var x›]
by auto
lemma vars_add_Var_subset:
‹vars (p' + Var x :: 'a :: {ab_group_add,one,zero_neq_one} mpoly) ⊆ 𝒱 ⟹ vars p' ⊆ insert x 𝒱›
using vars_add[of ‹p' + Var x› ‹-Var x›]
by auto
lemma coeff_monomila_in_varsD:
‹coeff p (monomial (Suc 0) x) ≠ 0 ⟹ x ∈ vars (p :: int mpoly)›
by (auto simp: coeff_def vars_def keys_def
intro!: exI[of _ ‹monomial (Suc 0) x›])
lemma coeff_MPoly_monomial[simp]:
‹(MPoly_Type.coeff (MPoly (monomial a m)) m) = a›
by (metis MPoly_Type.coeff_def lookup_single_eq monom.abs_eq monom.rep_eq)
end