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))"
    by (simp add: Bex_def conj_ac)
  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)"
  by (simp add: sym_mpoly_altdef Set.filter_def)

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]

notepad
begin
  define X Y Z :: "int mpoly" where "X = Var 1" "Y = Var 2" "Z = Var 3"
  define e1 e2 :: "int mpoly mpoly" where "e1 = Var 1" "e2 = Var 2"
  have "sym_mpoly {1, 2, 3} 2 = X * Y + X * Z + Y * Z"
    unfolding X_Y_Z_def by eval
  have "symmetric_mpoly {1, 2} (X ^ 3 + Y ^ 3)"
    unfolding X_Y_Z_def by eval
  have "fund_sym_poly_wit {1, 2} (X ^ 3 + Y ^ 3) = e1 ^ 3 - 3 * e1 * e2"
    unfolding X_Y_Z_def e1_e2_def by eval
end

end