# Theory Symmetric_Polynomials_Code

```(*
File:     Symmetric_Polynomials_Code.thy
Author:   Manuel Eberl (TU München)

Code equations for symmetric polynomials (albeit not very efficient ones)
*)
section ‹Executable Operations for Symmetric Polynomials›
theory Symmetric_Polynomials_Code
imports Symmetric_Polynomials "Polynomials.MPoly_Type_Class_FMap"
begin

(* TODO: Quite a few of these code equations should probably be moved to the Polynomials entry. *)

text ‹
Lastly, we shall provide some code equations to get executable code for operations related
to symmetric polynomials, including, most notably, the fundamental theorem of symmetric
polynomials and the recursive symmetry check.
›

lemma Ball_subset_right:
assumes "T ⊆ S" "∀x∈S-T. P x"
shows   "(∀x∈S. P x) = (∀x∈T. P x)"
using assms by auto

(* This is a fairly simple theorem, but the automation somehow has a lot of problems with it *)
lemma compute_less_pp[code]:
"xs < (ys :: 'a :: linorder ⇒⇩0 'b :: {zero, linorder}) ⟷
(∃i∈keys xs ∪ keys ys. lookup xs i < lookup ys i ∧
(∀j∈keys xs ∪ keys ys. j < i ⟶ lookup xs j = lookup ys j))"
proof transfer
fix f g :: "'a ⇒ 'b"
let ?dom = "{i. f i ≠ 0} ∪ {i. g i ≠ 0}"
have "less_fun f g ⟷ (∃k. f k < g k ∧ (∀k'<k. f k' = g k'))"
unfolding less_fun_def ..
also have "… ⟷ (∃i. f i < g i ∧ (i ∈ ?dom ∧ (∀j∈?dom. j < i ⟶ f j = g j)))"
proof (intro iff_exI conj_cong refl)
fix k assume "f k < g k"
hence k: "k ∈ ?dom" by auto
have "(∀k'<k. f k' = g k') = (∀k'∈{..<k}. f k' = g k')"
by auto
also have "… ⟷ (∀j∈({k. f k ≠ 0} ∪ {k. g k ≠ 0}) ∩ {..<k}. f j = g j)"
by (intro Ball_subset_right) auto
also have "… ⟷ (∀j∈({k. f k ≠ 0} ∪ {k. g k ≠ 0}). j < k ⟶ f j = g j)"
by auto
finally show "(∀k'<k. f k' = g k') ⟷ k ∈ ?dom ∧ (∀j∈?dom. j < k ⟶ f j = g j)"
using k by simp
qed
also have "… ⟷ (∃i∈?dom. f i < g i ∧ (∀j∈?dom. j < i ⟶ f j = g j))"
finally show "less_fun f g ⟷ (∃i∈?dom. f i < g i ∧ (∀j∈?dom. j < i ⟶ f j = g j))" .
qed

lemma compute_le_pp[code]:
"xs ≤ ys ⟷ xs = ys ∨ xs < (ys :: _ ⇒⇩0 _)"
by (auto simp: order.order_iff_strict)

lemma vars_code [code]:
"vars (MPoly p) = (⋃m∈keys p. keys m)"
unfolding vars_def by transfer' simp

lemma mpoly_coeff_code [code]: "coeff (MPoly p) = lookup p"
by transfer' simp

lemma sym_mpoly_code [code]:
"sym_mpoly (set xs) k = (∑X∈Set.filter (λX. card X = k) (Pow (set xs)). monom (monom_of_set X) 1)"

lemma monom_of_set_code [code]:
"monom_of_set (set xs) = Pm_fmap (fmap_of_list (map (λx. (x, 1)) xs))"
(is "?lhs = ?rhs")
proof (intro poly_mapping_eqI)
fix k
show "lookup ?lhs k = lookup ?rhs k"
by (induction xs) (auto simp: lookup_monom_of_set fmlookup_default_def)
qed

lemma restrictpm_code [code]:
"restrictpm A (Pm_fmap m) = Pm_fmap (fmrestrict_set A m)"
by (intro poly_mapping_eqI) (auto simp: lookup_restrictpm fmlookup_default_def)

lemmas [code] = check_symmetric_mpoly_correct [symmetric]