# Theory PAC_Polynomials

```theory PAC_Polynomials
imports PAC_Specification Finite_Map_Multiset
begin

section ‹Polynomials of strings›

text ‹

Isabelle's definition of polynomials only work with variables of type
\<^typ>‹nat›. Therefore, we introduce a version that uses strings by using an injective function
that converts a string to a natural number. It exists because strings are countable. Remark that
the whole development is independent of the function.

›

subsection ‹Polynomials and Variables›

lemma poly_embed_EX:
‹∃φ. bij (φ :: string ⇒ nat)›
by (rule countableE_infinite[of ‹UNIV :: string set›])
(auto intro!: infinite_UNIV_listI)

text ‹Using a multiset instead of a list has some advantage from an abstract point of view. First,
we can have monomials that appear several times  and the coefficient can also be zero. Basically,
we can represent un-normalised polynomials, which is very useful to talk about intermediate states
in our program.
›
type_synonym term_poly = ‹string multiset›
type_synonym mset_polynomial =
‹(term_poly * int) multiset›

definition normalized_poly :: ‹mset_polynomial ⇒ bool› where
‹normalized_poly p ⟷
distinct_mset (fst `# p) ∧
0 ∉# snd `# p›

lemma normalized_poly_simps[simp]:
‹normalized_poly {#}›
‹normalized_poly (add_mset t p) ⟷ snd t ≠ 0 ∧
fst t ∉# fst `# p ∧ normalized_poly p›
by (auto simp: normalized_poly_def)

lemma normalized_poly_mono:
‹normalized_poly B ⟹ A ⊆# B ⟹ normalized_poly A›
unfolding normalized_poly_def
by (auto intro: distinct_mset_mono image_mset_subseteq_mono)

definition mult_poly_by_monom :: ‹term_poly * int ⇒ mset_polynomial ⇒ mset_polynomial› where
‹mult_poly_by_monom  = (λys q. image_mset (λxs. (fst xs + fst ys, snd ys * snd xs)) q)›

definition mult_poly_raw :: ‹mset_polynomial ⇒ mset_polynomial ⇒ mset_polynomial› where
‹mult_poly_raw p q =
(sum_mset ((λy. mult_poly_by_monom y q) `# p))›

definition remove_powers :: ‹mset_polynomial ⇒ mset_polynomial› where
‹remove_powers xs =  image_mset (apfst remdups_mset) xs›

definition all_vars_mset :: ‹mset_polynomial ⇒ string multiset› where
‹all_vars_mset p = ∑⇩# (fst `# p)›

abbreviation all_vars :: ‹mset_polynomial ⇒ string set› where
‹all_vars p ≡ set_mset (all_vars_mset p)›

definition add_to_coefficient :: ‹_ ⇒ mset_polynomial ⇒ mset_polynomial›  where
‹add_to_coefficient = (λ(a, n) b. {#(a', _) ∈# b. a' ≠ a#} +
(if n + sum_mset (snd `# {#(a', _) ∈# b. a' = a#}) = 0 then {#}
else {#(a, n + sum_mset (snd `# {#(a', _) ∈# b. a' = a#}))#}))›

definition normalize_poly :: ‹mset_polynomial ⇒ mset_polynomial› where
‹normalize_poly p = fold_mset add_to_coefficient {#} p›

‹n + sum_mset (snd `# {#(a', _) ∈# b. a' = a#}) ≠ 0 ⟹
add_to_coefficient (a, n) b = {#(a', _) ∈# b. a' ≠ a#} +
{#(a, n + sum_mset (snd `# {#(a', _) ∈# b. a' = a#}))#}›
‹n + sum_mset (snd `# {#(a', _) ∈# b. a' = a#}) = 0 ⟹
add_to_coefficient (a, n) b = {#(a', _) ∈# b. a' ≠ a#}› and
‹add_to_coefficient (a, n) b = {#(a', _) ∈# b. a' ≠ a#} +
(if n + sum_mset (snd `# {#(a', _) ∈# b. a' = a#}) = 0 then {#}
else {#(a, n + sum_mset (snd `# {#(a', _) ∈# b. a' = a#}))#})›

proof -
have [iff]:
‹a ≠ aa ⟹
((case x of (a', _) ⇒ a' = a) ∧ (case x of (a', _) ⇒ a' ≠ aa)) ⟷
(case x of (a', _) ⇒ a' = a)› for a' aa a x
by auto
by standard
(auto intro!: ext simp: filter_filter_mset ac_simps add_eq_0_iff)
qed

lemma normalized_poly_normalize_poly[simp]:
‹normalized_poly (normalize_poly p)›
unfolding normalize_poly_def
apply (induction p)
subgoal by auto
subgoal for x p
by (cases x)
intro: normalized_poly_mono)
done

inductive add_poly_p :: ‹mset_polynomial × mset_polynomial × mset_polynomial ⇒ mset_polynomial × mset_polynomial × mset_polynomial ⇒ bool› where
rem_0_coeff:

‹add_poly_p⇧*⇧* (p, q, r) ({#}, q, p + r)›
apply (induction p arbitrary: r)
subgoal by auto
subgoal
by (metis (no_types, lifting) add_new_coeff_l r_into_rtranclp
done

‹add_poly_p⇧*⇧* (p, q, r) (p, {#}, q + r)›
apply (induction q arbitrary: r)
subgoal by auto
subgoal
by (metis (no_types, lifting) add_new_coeff_r r_into_rtranclp
done

‹add_poly_p (p, q, r) (p', q', r') ⟷ add_poly_p (q, p, r) (q', p', r')›
apply (rule iffI)
subgoal
subgoal
done

lemma wf_if_measure_in_wf:
‹wf R ⟹ (⋀a b. (a, b) ∈ S ⟹ (ν a, ν b)∈R) ⟹ wf S›
by (metis in_inv_image wfE_min wfI_min wf_inv_image)

lemma lexn_n:
‹n > 0 ⟹ (x # xs, y # ys) ∈ lexn r n ⟷
(length xs = n-1 ∧ length ys = n-1) ∧ ((x, y) ∈ r ∨ (x = y ∧ (xs, ys) ∈ lexn r (n - 1)))›
apply (cases n)
apply simp
by (auto simp: map_prod_def image_iff lex_prod_def)

‹wf {(x, y). add_poly_p y x}›
by (rule wf_if_measure_in_wf[where R = ‹lexn less_than 3› and
ν = ‹λ(a,b,c). [size a , size b, size c]›])
simp: lexn_n simp del: lexn.simps(2))

lemma mult_poly_by_monom_simps[simp]:
‹mult_poly_by_monom t {#} = {#}›
‹mult_poly_by_monom t (ps + qs) =  mult_poly_by_monom t ps + mult_poly_by_monom t qs›
‹mult_poly_by_monom a (add_mset p ps) = add_mset (fst a + fst p, snd a * snd p) (mult_poly_by_monom a ps)›
proof -
interpret comp_fun_commute ‹(λxs. add_mset (xs + t))› for t
by standard auto
show
‹mult_poly_by_monom t (ps + qs) =  mult_poly_by_monom t ps + mult_poly_by_monom t qs› for t
by (induction ps)
(auto simp: mult_poly_by_monom_def)
show
‹mult_poly_by_monom a (add_mset p ps) = add_mset (fst a + fst p, snd a * snd p) (mult_poly_by_monom a ps)›
‹mult_poly_by_monom t {#} = {#}›for t
by (auto simp: mult_poly_by_monom_def)
qed

inductive mult_poly_p :: ‹mset_polynomial ⇒ mset_polynomial × mset_polynomial ⇒ mset_polynomial × mset_polynomial ⇒ bool›
for q :: mset_polynomial where
mult_step:
‹mult_poly_p q (add_mset (xs, n) p, r) (p, (λ(ys, m). (remdups_mset (xs + ys), n * m)) `# q + r)›

lemmas mult_poly_p_induct = mult_poly_p.induct[split_format(complete)]

subsection ‹Normalisation›

inductive normalize_poly_p :: ‹mset_polynomial ⇒ mset_polynomial ⇒ bool›where
rem_0_coeff[simp, intro]:
‹normalize_poly_p p q ⟹ normalize_poly_p (add_mset (xs, 0) p) q› |
merge_dup_coeff[simp, intro]:
‹normalize_poly_p p q ⟹ normalize_poly_p (add_mset (xs, m) (add_mset (xs, n) p)) (add_mset (xs, m + n) q)› |
same[simp, intro]:
‹normalize_poly_p p p› |
keep_coeff[simp, intro]:

subsection ‹Correctness›
text ‹
This locales maps string polynomials to real polynomials.
›
locale poly_embed =
fixes φ :: ‹string ⇒ nat›
assumes φ_inj: ‹inj φ›
begin

definition poly_of_vars :: "term_poly ⇒ ('a :: {comm_semiring_1}) mpoly" where
‹poly_of_vars xs = fold_mset (λa b. Var (φ a) * b) (1 :: 'a mpoly) xs›

lemma poly_of_vars_simps[simp]:
shows
‹poly_of_vars (add_mset x xs) = Var (φ x) * (poly_of_vars xs :: ('a :: {comm_semiring_1}) mpoly)› (is ?A) and
‹poly_of_vars (xs + ys) = poly_of_vars xs * (poly_of_vars ys :: ('a :: {comm_semiring_1}) mpoly)› (is ?B)
proof -
interpret comp_fun_commute ‹(λa b. (b :: 'a :: {comm_semiring_1} mpoly) * Var (φ a))›
by standard
(auto simp: algebra_simps ac_simps
Var_def times_monomial_monomial intro!: ext)

show ?A
by (auto simp: poly_of_vars_def comp_fun_commute_axioms fold_mset_fusion
ac_simps)
show ?B
apply (auto simp: poly_of_vars_def ac_simps)
semiring_normalization_rules(18))
qed

definition mononom_of_vars where
‹mononom_of_vars ≡ (λ(xs, n). (+) (Const n * poly_of_vars xs))›

interpretation comp_fun_commute ‹mononom_of_vars›
by standard
(auto simp: algebra_simps ac_simps mononom_of_vars_def
Var_def times_monomial_monomial intro!: ext)

lemma [simp]:
‹poly_of_vars {#} = 1›
by (auto simp: poly_of_vars_def)

‹NO_MATCH 0 b ⟹ mononom_of_vars xs b = Const (snd xs) * poly_of_vars (fst xs) + b›
by (cases xs)
(auto simp: ac_simps mononom_of_vars_def)

definition polynomial_of_mset :: ‹mset_polynomial ⇒ _› where
‹polynomial_of_mset p = sum_mset (mononom_of_vars `# p) 0›

lemma polynomial_of_mset_append[simp]:
‹polynomial_of_mset (xs + ys) = polynomial_of_mset xs + polynomial_of_mset ys›
by (auto simp: ac_simps Const_def polynomial_of_mset_def)

lemma polynomial_of_mset_Cons[simp]:
‹polynomial_of_mset (add_mset x ys) = Const (snd x) * poly_of_vars (fst x) + polynomial_of_mset ys›
by (cases x)
(auto simp: ac_simps polynomial_of_mset_def mononom_of_vars_def)

lemma polynomial_of_mset_empty[simp]:
‹polynomial_of_mset {#} = 0›
by (auto simp: polynomial_of_mset_def)

lemma polynomial_of_mset_mult_poly_by_monom[simp]:
‹polynomial_of_mset (mult_poly_by_monom x ys) =
(Const (snd x) * poly_of_vars (fst x) * polynomial_of_mset ys)›
by (induction ys)
(auto simp: Const_mult algebra_simps)

lemma polynomial_of_mset_mult_poly_raw[simp]:
‹polynomial_of_mset (mult_poly_raw xs ys) = polynomial_of_mset xs * polynomial_of_mset ys›
unfolding mult_poly_raw_def
by (induction xs arbitrary: ys)
(auto simp: Const_mult algebra_simps)

lemma polynomial_of_mset_uminus:
‹polynomial_of_mset {#case x of (a, b) ⇒ (a, - b). x ∈# za#} =
- polynomial_of_mset za›
by (induction za)
auto

lemma X2_X_polynomial_bool_mult_in:
‹Var (x1) * (Var (x1) * p) -  Var (x1) * p ∈ More_Modules.ideal polynomial_bool›
using ideal_mult_right_in[OF  X2_X_in_pac_ideal[of x1 ‹{}›, unfolded pac_ideal_def], of p]
by (auto simp: right_diff_distrib ac_simps power2_eq_square)

lemma polynomial_of_list_remove_powers_polynomial_bool:
‹(polynomial_of_mset xs) - polynomial_of_mset (remove_powers xs) ∈ ideal polynomial_bool›
proof (induction xs)
case empty
then show ‹?case› by (auto simp: remove_powers_def ideal.span_zero)
next
have H1: ‹x1 ∈# x2 ⟹
Var (φ x1) * poly_of_vars x2 - p ∈ More_Modules.ideal polynomial_bool ⟷
poly_of_vars x2 - p ∈ More_Modules.ideal polynomial_bool
› for x1 x2 p
of ‹Var (φ x1) * poly_of_vars x2 - poly_of_vars x2›])
apply (drule multi_member_split)
apply (auto simp: X2_X_polynomial_bool_mult_in)
done

have diff: ‹poly_of_vars (x) - poly_of_vars (remdups_mset (x)) ∈ ideal polynomial_bool› for x
by (induction x)
(auto simp: remove_powers_def ideal.span_zero H1
simp flip: right_diff_distrib intro!: ideal.span_scale)
have [simp]: ‹polynomial_of_mset xs -
polynomial_of_mset (apfst remdups_mset `# xs)
∈ More_Modules.ideal polynomial_bool ⟹
poly_of_vars ys * poly_of_vars ys -
poly_of_vars ys * poly_of_vars (remdups_mset ys)
∈ More_Modules.ideal polynomial_bool ⟹
polynomial_of_mset xs + Const y * poly_of_vars ys -
(polynomial_of_mset (apfst remdups_mset `# xs) +
Const y * poly_of_vars (remdups_mset ys))
∈ More_Modules.ideal polynomial_bool› for y ys
show ?case
apply (cases x)
subgoal for ys y
using ideal_mult_right_in2[OF diff, of ‹poly_of_vars ys› ys]
by (auto simp: remove_powers_def right_diff_distrib
done
qed

‹add_poly_p (p, q, r) (p', q', r') ⟹
polynomial_of_mset r + (polynomial_of_mset p + polynomial_of_mset q) =
polynomial_of_mset r' + (polynomial_of_mset p' + polynomial_of_mset q')›
subgoal
by auto
subgoal
by auto
subgoal
subgoal
subgoal
done

‹add_poly_p⇧*⇧* (p, q, r) (p', q', r') ⟹
polynomial_of_mset r + (polynomial_of_mset p + polynomial_of_mset q) =
polynomial_of_mset r' + (polynomial_of_mset p' + polynomial_of_mset q')›
by (induction rule: rtranclp_induct[of add_poly_p ‹(_, _, _)› ‹(_, _, _)›, split_format(complete), of for r])

‹add_poly_p⇧*⇧* (p, q, {#}) ({#}, {#}, r') ⟹
polynomial_of_mset r' = (polynomial_of_mset p + polynomial_of_mset q)›

lemma poly_of_vars_remdups_mset:
‹poly_of_vars (remdups_mset (xs)) - (poly_of_vars xs)
∈ More_Modules.ideal polynomial_bool›
apply (induction xs)
subgoal by (auto simp: ideal.span_zero)
subgoal for x xs
apply (cases ‹x ∈# xs›)
apply (metis (no_types, lifting) X2_X_polynomial_bool_mult_in diff_add_cancel diff_diff_eq2
ideal.span_diff insert_DiffM poly_of_vars_simps(1) remdups_mset_singleton_sum)
by (metis (no_types, lifting) ideal.span_scale poly_of_vars_simps(1) remdups_mset_singleton_sum
right_diff_distrib)
done

lemma polynomial_of_mset_mult_map:
‹polynomial_of_mset
{#case x of (ys, n) ⇒ (remdups_mset (ys + xs), n * m). x ∈# q#} -
Const m * (poly_of_vars xs * polynomial_of_mset q)
∈ More_Modules.ideal polynomial_bool›
(is ‹?P q ∈ _›)
proof (induction q)
case empty
then show ?case by (auto simp: algebra_simps ideal.span_zero)
next
then have uP:  ‹-?P q ∈ More_Modules.ideal polynomial_bool›
using ideal.span_neg by blast
have ‹ Const b * (Const m * poly_of_vars (remdups_mset (a + xs))) -
Const b * (Const m * (poly_of_vars a * poly_of_vars xs))
∈ More_Modules.ideal polynomial_bool› for a b
by (auto simp: Const_mult simp flip: right_diff_distrib' poly_of_vars_simps
intro!: ideal.span_scale poly_of_vars_remdups_mset)
then show ?case
apply (cases x)
apply (auto simp: field_simps Const_mult  simp flip:
intro!: ideal.span_scale poly_of_vars_remdups_mset)
done
qed

lemma mult_poly_p_mult_ideal:
‹mult_poly_p q (p, r) (p', r') ⟹
(polynomial_of_mset p' * polynomial_of_mset q + polynomial_of_mset r') - (polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset r)
∈ ideal polynomial_bool›
proof (induction rule: mult_poly_p_induct)
case (mult_step xs n p r)
show ?case
by (auto simp: algebra_simps polynomial_of_mset_mult_map)
qed

lemma rtranclp_mult_poly_p_mult_ideal:
‹(mult_poly_p q)⇧*⇧* (p, r) (p', r') ⟹
(polynomial_of_mset p' * polynomial_of_mset q + polynomial_of_mset r') - (polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset r)
∈ ideal polynomial_bool›
apply (induction p' r' rule: rtranclp_induct[of ‹mult_poly_p q› ‹(p, r)› ‹(p', q')› for p' q', split_format(complete)])
subgoal
by (auto simp: ideal.span_zero)
subgoal for a b aa ba
apply (drule mult_poly_p_mult_ideal)
apply assumption
done

lemma rtranclp_mult_poly_p_mult_ideal_final:
‹(mult_poly_p q)⇧*⇧* (p, {#}) ({#}, r) ⟹
(polynomial_of_mset r) - (polynomial_of_mset p * polynomial_of_mset q)
∈ ideal polynomial_bool›
by (drule rtranclp_mult_poly_p_mult_ideal) auto

lemma normalize_poly_p_poly_of_mset:
‹normalize_poly_p p q ⟹ polynomial_of_mset p = polynomial_of_mset q›
apply (induction rule: normalize_poly_p.induct)
done

lemma rtranclp_normalize_poly_p_poly_of_mset:
‹normalize_poly_p⇧*⇧* p q ⟹ polynomial_of_mset p = polynomial_of_mset q›
by (induction rule: rtranclp_induct)
(auto simp: normalize_poly_p_poly_of_mset)

end

text ‹It would be nice to have the property in the other direction too, but this requires a deep
dive into the definitions of polynomials.›
locale poly_embed_bij = poly_embed +
fixes V N
assumes φ_bij: ‹bij_betw φ V N›
begin

definition φ' :: ‹nat ⇒ string› where
‹φ' = the_inv_into V φ›

lemma φ'_φ[simp]:
‹x ∈ V ⟹ φ' (φ x) = x›
using φ_bij unfolding φ'_def
by (meson bij_betw_imp_inj_on the_inv_into_f_f)

lemma φ_φ'[simp]:
‹x ∈ N ⟹ φ (φ' x) = x›
using φ_bij unfolding φ'_def
by (meson f_the_inv_into_f_bij_betw)

end

end

```