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"

(* 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" "xS-T. P x"
  shows   "(xS. P x) = (xT. 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}) 
    (ikeys xs  keys ys. lookup xs i < lookup ys i 
    (jkeys 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
  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))" .

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) = (mkeys 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 = (XSet.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)

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]

  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