(* 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