Theory Polynomials.MPoly_Type_Class_FMap

(* Author: Fabian Immler, Alexander Maletzky *)

section ‹Executable Representation of Polynomial Mappings as Association Lists›

theory MPoly_Type_Class_FMap
  imports
    MPoly_Type_Class_Ordered
    Poly_Mapping_Finite_Map
begin

text ‹In this theory, (type class) multivariate polynomials of type
  @{typ "('a, 'b) poly_mapping"} are represented as association lists.›

text ‹It is important to note that theory ‹MPoly_Type_Class_OAlist›, which represents polynomials as
  @{emph ‹ordered›} associative lists, is much better suited for doing actual computations. This
  theory is only included for being able to compare the two representations in terms of efficiency.›

subsection ‹Power Products›

lemma compute_lcs_pp[code]:
  "lcs (Pm_fmap xs) (Pm_fmap ys) =
  Pm_fmap (fmmap_keys (λk v. Orderings.max (lookup0 xs k) (lookup0 ys k)) (xs ++f ys))"
  by (rule poly_mapping_eqI)
    (auto simp add: fmlookup_default_fmmap_keys fmlookup_dom_iff fmdom'_notI
      lcs_poly_mapping.rep_eq fmdom'_notD)

lemma compute_deg_pp[code]:
  "deg_pm (Pm_fmap xs) = sum (the o fmlookup xs) (fmdom' xs)"
proof -
  have "deg_pm (Pm_fmap xs) = sum (lookup (Pm_fmap xs)) (keys (Pm_fmap xs))"
    by (rule deg_pm_superset) auto
  also have "… = sum (the o fmlookup xs) (fmdom' xs)"
    by (rule sum.mono_neutral_cong_left)
       (auto simp: fmlookup_dom'_iff fmdom'I in_keys_iff fmlookup_default_def
             split: option.splits)
  finally show ?thesis .
qed

definition adds_pp_add_linorder :: "('b ⇒0 'a::add_linorder) ⇒ _ ⇒ bool"
  where [code_abbrev]: "adds_pp_add_linorder = (adds)"

lemma compute_adds_pp[code]:
  "adds_pp_add_linorder (Pm_fmap xs) (Pm_fmap ys) =
    (fmpred (λk v. lookup0 xs k ≤ lookup0 ys k) (xs ++f ys))"
  for xs ys::"('a, 'b::add_linorder_min) fmap"
  unfolding adds_pp_add_linorder_def
  unfolding adds_poly_mapping
  using fmdom_notI
  by (force simp: fmlookup_dom_iff le_fun_def
      split: option.splits if_splits)


text‹Computing @{term lex} as below is certainly not the most efficient way, but it works.›

lemma lex_pm_iff: "lex_pm s t = (∀x. lookup s x ≤ lookup t x ∨ (∃y<x. lookup s y ≠ lookup t y))"
proof -
  have "lex_pm s t = (¬ lex_pm_strict t s)" by (simp add: lex_pm_strict_alt)
  also have "… = (∀x. lookup s x ≤ lookup t x ∨ (∃y<x. lookup s y ≠ lookup t y))"
    by (simp add: lex_pm_strict_def less_poly_mapping_def less_fun_def) (metis leD leI)
  finally show ?thesis .
qed

lemma compute_lex_pp[code]:
  "(lex_pm (Pm_fmap xs) (Pm_fmap (ys::(_, _::ordered_comm_monoid_add) fmap))) =
    (let zs = xs ++f ys in
      fmpred (λx v.
        lookup0 xs x ≤ lookup0 ys x ∨
        ¬ fmpred (λy w. y ≥ x ∨ lookup0 xs y = lookup0 ys y) zs) zs
    )"
  unfolding Let_def lex_pm_iff fmpred_iff Pm_fmap.rep_eq fmlookup_add fmlookup_dom_iff
  apply (intro iffI)
   apply (metis fmdom'_notD fmlookup_default_if(2) fmlookup_dom'_iff leD)
  apply (metis eq_iff not_le fmdom'_notD fmlookup_default_if(2) fmlookup_dom'_iff)
  done

lemma compute_dord_pp[code]:
  "(dord_pm ord (Pm_fmap xs) (Pm_fmap (ys::('a::wellorder , 'b::ordered_comm_monoid_add) fmap))) =
    (let dx = deg_pm (Pm_fmap xs) in let dy = deg_pm (Pm_fmap ys) in
      dx < dy ∨ (dx = dy ∧ ord (Pm_fmap xs) (Pm_fmap ys))
    )"
  by (auto simp: Let_def deg_pm.rep_eq dord_fun_def dord_pm.rep_eq)
    (simp_all add: Pm_fmap.abs_eq)


subsubsection ‹Computations›

experiment begin

abbreviation "X ≡ 0::nat"
abbreviation "Y ≡ 1::nat"
abbreviation "Z ≡ 2::nat"

lemma
  "sparse0 [(X, 2::nat), (Z, 7)] + sparse0 [(Y, 3), (Z, 2)] = sparse0 [(X, 2), (Z, 9), (Y, 3)]"
  "dense0 [2, 0, 7::nat] + dense0 [0, 3, 2] = dense0 [2, 3, 9]"
  by eval+

lemma
  "sparse0 [(X, 2::nat), (Z, 7)] - sparse0 [(X, 2), (Z, 2)] = sparse0 [(Z, 5)]"
  by eval

lemma
  "lcs (sparse0 [(X, 2::nat), (Y, 1), (Z, 7)]) (sparse0 [(Y, 3), (Z, 2)]) = sparse0 [(X, 2), (Y, 3), (Z, 7)]"
  by eval

lemma
  "(sparse0 [(X, 2::nat), (Z, 1)]) adds (sparse0 [(X, 3), (Y, 2), (Z, 1)])"
  by eval

lemma
  "lookup (sparse0 [(X, 2::nat), (Z, 3)]) X = 2"
  by eval

lemma
  "deg_pm (sparse0 [(X, 2::nat), (Y, 1), (Z, 3), (X, 1)]) = 6"
  by eval

lemma
  "lex_pm (sparse0 [(X, 2::nat), (Y, 1), (Z, 3)]) (sparse0 [(X, 4)])"
by eval

lemma
  "lex_pm (sparse0 [(X, 2::nat), (Y, 1), (Z, 3)]) (sparse0 [(X, 4)])"
  by eval

lemma
  "¬ (dlex_pm (sparse0 [(X, 2::nat), (Y, 1), (Z, 3)]) (sparse0 [(X, 4)]))"
  by eval

lemma
  "dlex_pm (sparse0 [(X, 2::nat), (Y, 1), (Z, 2)]) (sparse0 [(X, 5)])"
  by eval

lemma
  "¬ (drlex_pm (sparse0 [(X, 2::nat), (Y, 1), (Z, 2)]) (sparse0 [(X, 5)]))"
  by eval

end


subsection ‹Implementation of Multivariate Polynomials as Association Lists›

subsubsection ‹Unordered Power-Products›

lemma compute_monomial [code]:
  "monomial c t = (if c = 0 then 0 else sparse0 [(t, c)])"
  by (auto intro!: poly_mapping_eqI simp: sparse0_def fmlookup_default_def lookup_single)

lemma compute_one_poly_mapping [code]: "1 = sparse0 [(0, 1)]"
  by (metis compute_monomial single_one zero_neq_one)

lemma compute_except_poly_mapping [code]:
  "except (Pm_fmap xs) S = Pm_fmap (fmfilter (λk. k ∉ S) xs)"
  by (auto simp: fmlookup_default_def lookup_except split: option.splits intro!: poly_mapping_eqI)

lemma lookup0_fmap_of_list_simps:
  "lookup0 (fmap_of_list ((x, y)#xs)) i = (if x = i then y else lookup0 (fmap_of_list xs) i)"
  "lookup0 (fmap_of_list []) i = 0"
  by (auto simp: fmlookup_default_def fmlookup_of_list split: if_splits option.splits)

lemma if_poly_mapping_eq_iff:
  "(if x = y then a else b) =
    (if (∀i∈keys x ∪ keys y. lookup x i = lookup y i) then a else b)"
  by simp (metis UnI1 UnI2 in_keys_iff poly_mapping_eqI)

lemma keys_add_eq: "keys (a + b) = keys a ∪ keys b - {x ∈ keys a ∩ keys b. lookup a x + lookup b x = 0}"
  by (auto simp: in_keys_iff lookup_add add_eq_0_iff)

context term_powerprod
begin

context includes fmap.lifting begin

lift_definition shift_keys::"'a ⇒ ('t, 'b) fmap ⇒ ('t, 'b) fmap"
  is "λt m x. if t addsp x then m (x ⊖ t) else None"
proof -
  fix t and f::"'t ⇒ 'b option"
  assume "finite (dom f)"
  have "dom (λx. if t addsp x then f (x ⊖ t) else None) ⊆ (⊕) t ` dom f"
    by (auto simp: adds_pp_alt domI term_simps split: if_splits)
  also have "finite …"
    using ‹finite (dom f)› by simp
  finally (finite_subset) show "finite (dom (λx. if t addsp x then f (x ⊖ t) else None))" .
qed

definition "shift_map_keys t f m = fmmap f (shift_keys t m)"

lemma compute_shift_map_keys[code]:
  "shift_map_keys t f (fmap_of_list xs) = fmap_of_list (map (λ(k, v). (t ⊕ k, f v)) xs)"
  unfolding shift_map_keys_def
  apply transfer
  subgoal for f t xs
  proof -
    show ?thesis
      apply (rule ext)
      subgoal for x
        apply (cases "t addsp x")
        subgoal by (induction xs) (auto simp: adds_pp_alt term_simps)
        subgoal by (induction xs) (auto simp: adds_pp_alt term_simps)
        done
      done
  qed
  done

end

lemmas [simp] = compute_zero_pp[symmetric]

lemma compute_monom_mult_poly_mapping [code]:
  "monom_mult c t (Pm_fmap xs) = Pm_fmap (if c = 0 then fmempty else shift_map_keys t ((*) c) xs)"
proof (cases "c = 0")
  case True
  hence "monom_mult c t (Pm_fmap xs) = 0" using monom_mult_zero_left by simp
  thus ?thesis using True
    by simp
next
  case False
  thus ?thesis
    by (auto simp: simp: fmlookup_default_def shift_map_keys_def lookup_monom_mult
        adds_def group_eq_aux shift_keys.rep_eq
        intro!: poly_mapping_eqI split: option.splits)
qed

lemma compute_mult_scalar_poly_mapping [code]:
  "Pm_fmap (fmap_of_list xs) ⊙ q = (case xs of ((t, c) # ys) ⇒
    (monom_mult c t q + except (Pm_fmap (fmap_of_list ys)) {t} ⊙ q) | _ ⇒
    Pm_fmap fmempty)"
proof (split list.splits, simp, intro conjI impI allI, goal_cases)
  case (1 t c ys)
  have "Pm_fmap (fmupd t c (fmap_of_list ys)) = sparse0 [(t, c)] + except (sparse0 ys) {t}"
    by (auto simp: sparse0_def fmlookup_default_def lookup_add lookup_except
        split: option.splits intro!: poly_mapping_eqI)
  also have "sparse0 [(t, c)] = monomial c t"
    by (auto simp: sparse0_def lookup_single fmlookup_default_def intro!: poly_mapping_eqI)
  finally show ?case
    by (simp add: algebra_simps mult_scalar_monomial sparse0_def)
qed

end (* term_powerprod *)

subsubsection ‹restore constructor view›

named_theorems mpoly_simps

definition "monomial1 pp = monomial 1 pp"

lemma monomial1_Nil[mpoly_simps]: "monomial1 0 = 1"
  by (simp add: monomial1_def)

lemma monomial_mp: "monomial c (pp::'a⇒0nat) = Const0 c * monomial1 pp"
  for c::"'b::comm_semiring_1"
  by (auto intro!: poly_mapping_eqI simp: monomial1_def Const0_def mult_single)

lemma monomial1_add: "(monomial1 (a + b)::('a::monoid_add⇒0'b::comm_semiring_1)) = monomial1 a * monomial1 b"
  by (auto simp: monomial1_def mult_single)

lemma monomial1_monomial: "monomial1 (monomial n v) = (Var0 v::_⇒0('b::comm_semiring_1))^n"
  by (auto intro!: poly_mapping_eqI simp: monomial1_def Var0_power lookup_single when_def)

lemma Ball_True: "(∀x∈X. True) ⟷ True" by auto
lemma Collect_False: "{x. False} = {}" by simp

lemma Pm_fmap_sum: "Pm_fmap f = (∑x ∈ fmdom' f. monomial (lookup0 f x) x)"
  including fmap.lifting
  by (auto intro!: poly_mapping_eqI sum.neutral
      simp: fmlookup_default_def lookup_sum lookup_single when_def fmdom'I
      split: option.splits)

lemma MPoly_numeral: "MPoly (numeral x) = numeral x"
  by (metis monom.abs_eq monom_numeral single_numeral)

lemma MPoly_power: "MPoly (x ^ n) = MPoly x ^ n"
  by (induction n) (auto simp: one_mpoly_def times_mpoly.abs_eq[symmetric])

lemmas [mpoly_simps] = Pm_fmap_sum
  add.assoc[symmetric] mult.assoc[symmetric]
  add_0 add_0_right mult_1 mult_1_right mult_zero_left mult_zero_right power_0 power_one_right
  fmdom'_fmap_of_list
  list.map fst_conv
  sum.insert_remove finite_insert finite.emptyI
  lookup0_fmap_of_list_simps
  num.simps rel_simps
  if_True if_False
  insert_Diff_if insert_iff empty_Diff empty_iff
  simp_thms
  sum.empty
  if_poly_mapping_eq_iff
  keys_zero keys_one
  keys_add_eq
  keys_single
  Un_insert_left Un_empty_left
  Int_insert_left Int_empty_left
  Collect_False
  lookup_add lookup_single lookup_zero lookup_one
  Set.ball_simps
  when_simps
  monomial_mp
  monomial1_add
  monomial1_monomial
  Const0_one Const0_zero Const0_numeral Const0_minus
  set_simps

text ‹A simproc for postprocessing with ‹mpoly_simps› and not polluting ‹[code_post]›:›

ML ‹val mpoly_simproc = Simplifier.make_simproc @{context} "multivariate polynomials"
      {lhss = [@{term "Pm_fmap mpp::(_ ⇒0 nat) ⇒0 _"}],
       proc = (K (fn ctxt => fn ct =>
          SOME (Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps
            (Named_Theorems.get ctxt (named_theorems‹mpoly_simps›))) ct)))}›

(* The simproc slows down computations *a lot*, so it is deactivated by default. *)

(* setup ‹Code_Preproc.map_post (fn ctxt => ctxt addsimprocs [mpoly_simproc])› *)


subsubsection ‹Ordered Power-Products›

lemma foldl_assoc:
  assumes "⋀x y z. f (f x y) z = f x (f y z)"
  shows "foldl f (f a b) xs = f a (foldl f b xs)"
proof (induct xs arbitrary: a b)
  fix a b
  show "foldl f (f a b) [] = f a (foldl f b [])" by simp
next
  fix a b x xs
  assume "⋀a b. foldl f (f a b) xs = f a (foldl f b xs)"
  from assms[of a b x] this[of a "f b x"]
    show "foldl f (f a b) (x # xs) = f a (foldl f b (x # xs))" unfolding foldl_Cons by simp
qed

context ordered_term
begin

definition list_max::"'t list ⇒ 't" where
  "list_max xs ≡ foldl ord_term_lin.max min_term xs"

lemma list_max_Cons: "list_max (x # xs) = ord_term_lin.max x (list_max xs)"
  unfolding list_max_def foldl_Cons
proof -
  have "foldl ord_term_lin.max (ord_term_lin.max x min_term) xs =
          ord_term_lin.max x (foldl ord_term_lin.max min_term xs)"
    by (rule foldl_assoc, rule ord_term_lin.max.assoc)
  from this ord_term_lin.max.commute[of min_term x]
    show "foldl ord_term_lin.max (ord_term_lin.max min_term x) xs =
            ord_term_lin.max x (foldl ord_term_lin.max min_term xs)" by simp
qed

lemma list_max_empty: "list_max [] = min_term"
  unfolding list_max_def by simp

lemma list_max_in_list:
  assumes "xs ≠ []"
  shows "list_max xs ∈ set xs"
  using assms
proof (induct xs, simp)
  fix x xs
  assume IH: "xs ≠ [] ⟹ list_max xs ∈ set xs"
  show "list_max (x # xs) ∈ set (x # xs)"
  proof (cases "xs = []")
    case True
    hence "list_max (x # xs) = ord_term_lin.max min_term x" unfolding list_max_def by simp
    also have "… = x" unfolding ord_term_lin.max_def by (simp add: min_term_min)
    finally show ?thesis by simp
  next
    assume "xs ≠ []"
    show ?thesis
    proof (cases "x ≼t list_max xs")
      case True
      hence "list_max (x # xs) = list_max xs"
        unfolding list_max_Cons ord_term_lin.max_def by simp
      thus ?thesis using IH[OF ‹xs ≠ []›] by simp
    next
      case False
      hence "list_max (x # xs) = x" unfolding list_max_Cons ord_term_lin.max_def by simp
      thus ?thesis by simp
    qed
  qed
qed

lemma list_max_maximum:
  assumes "a ∈ set xs"
  shows "a ≼t (list_max xs)"
  using assms
proof (induct xs)
  assume "a ∈ set []"
  thus "a ≼t list_max []" by simp
next
  fix x xs
  assume IH: "a ∈ set xs ⟹ a ≼t list_max xs" and a_in: "a ∈ set (x # xs)"
  from a_in have "a = x ∨ a ∈ set xs" by simp
  thus "a ≼t list_max (x # xs)" unfolding list_max_Cons
  proof
    assume "a = x"
    thus "a ≼t ord_term_lin.max x (list_max xs)" by simp
  next
    assume "a ∈ set xs"
    from IH[OF this] show "a ≼t ord_term_lin.max x (list_max xs)"
      by (simp add: ord_term_lin.le_max_iff_disj)
  qed
qed

lemma list_max_nonempty:
  assumes "xs ≠ []"
  shows "list_max xs = ord_term_lin.Max (set xs)"
proof -
  have fin: "finite (set xs)" by simp
  have "ord_term_lin.Max (set xs) = list_max xs"
  proof (rule ord_term_lin.Max_eqI[OF fin, of "list_max xs"])
    fix y
    assume "y ∈ set xs"
    from list_max_maximum[OF this] show "y ≼t list_max xs" .
  next
    from list_max_in_list[OF assms] show "list_max xs ∈ set xs" .
  qed
  thus ?thesis by simp
qed

lemma in_set_clearjunk_iff_map_of_eq_Some:
  "(a, b) ∈ set (AList.clearjunk xs) ⟷ map_of xs a = Some b"
  by (metis Some_eq_map_of_iff distinct_clearjunk map_of_clearjunk)

lemma Pm_fmap_of_list_eq_zero_iff:
  "Pm_fmap (fmap_of_list xs) = 0 ⟷ [(k, v)←AList.clearjunk xs . v ≠ 0] = []"
  by (auto simp: poly_mapping_eq_iff fmlookup_default_def fun_eq_iff
    in_set_clearjunk_iff_map_of_eq_Some filter_empty_conv fmlookup_of_list split: option.splits)

lemma fmdom'_clearjunk0: "fmdom' (clearjunk0 xs) = fmdom' xs - {x. fmlookup xs x = Some 0}"
  by (metis (no_types, lifting) clearjunk0_def fmdom'_drop_set fmfilter_alt_defs(2) fmfilter_cong' mem_Collect_eq)

lemma compute_lt_poly_mapping[code]:
  "lt (Pm_fmap (fmap_of_list xs)) = list_max (map fst [(k, v) ← AList.clearjunk xs. v ≠ 0])"
proof -
  have "keys (Pm_fmap (fmap_of_list xs)) = fst ` {x ∈ set (AList.clearjunk xs). case x of (k, v) ⇒ v ≠ 0}"
    by (auto simp: compute_keys_pp fmdom'_clearjunk0 fmap_of_list.rep_eq
        in_set_clearjunk_iff_map_of_eq_Some fmdom'I image_iff fmlookup_dom'_iff)
  then show ?thesis
    unfolding lt_def
    by (auto simp: Pm_fmap_of_list_eq_zero_iff list_max_empty list_max_nonempty)
qed

lemma compute_higher_poly_mapping [code]:
  "higher (Pm_fmap xs) t = Pm_fmap (fmfilter (λk. t ≺t k) xs)"
  unfolding higher_def compute_except_poly_mapping
  by (metis mem_Collect_eq ord_term_lin.leD ord_term_lin.leI)

lemma compute_lower_poly_mapping [code]:
  "lower (Pm_fmap xs) t = Pm_fmap (fmfilter (λk. k ≺t t) xs)"
  unfolding lower_def compute_except_poly_mapping
  by (metis mem_Collect_eq ord_term_lin.leD ord_term_lin.leI)

end (* ordered_term *)

lifting_update poly_mapping.lifting
lifting_forget poly_mapping.lifting

subsection ‹Computations›

subsubsection ‹Scalar Polynomials›

type_synonym 'a mpoly_tc = "(nat ⇒0 nat)⇒0'a"

definition "shift_map_keys_punit = term_powerprod.shift_map_keys to_pair_unit fst"

lemma compute_shift_map_keys_punit [code]:
  "shift_map_keys_punit t f (fmap_of_list xs) = fmap_of_list (map (λ(k, v). (t + k, f v)) xs)"
  by (simp add: punit.compute_shift_map_keys shift_map_keys_punit_def)

global_interpretation punit: term_powerprod to_pair_unit fst
  rewrites "punit.adds_term = (adds)"
  and "punit.pp_of_term = (λx. x)"
  and "punit.component_of_term = (λ_. ())"
  defines monom_mult_punit = punit.monom_mult
  and mult_scalar_punit = punit.mult_scalar
  apply (fact MPoly_Type_Class.punit.term_powerprod_axioms)
  apply (fact MPoly_Type_Class.punit_adds_term)
  apply (fact MPoly_Type_Class.punit_pp_of_term)
  apply (fact MPoly_Type_Class.punit_component_of_term)
  done

lemma compute_monom_mult_punit [code]:
  "monom_mult_punit c t (Pm_fmap xs) = Pm_fmap (if c = 0 then fmempty else shift_map_keys_punit t ((*) c) xs)"
  by (simp add: monom_mult_punit_def punit.compute_monom_mult_poly_mapping shift_map_keys_punit_def)

lemma compute_mult_scalar_punit [code]:
  "Pm_fmap (fmap_of_list xs) * q = (case xs of ((t, c) # ys) ⇒
    (monom_mult_punit c t q + except (Pm_fmap (fmap_of_list ys)) {t} * q) | _ ⇒
    Pm_fmap fmempty)"
  by (simp only: punit_mult_scalar[symmetric] punit.compute_mult_scalar_poly_mapping monom_mult_punit_def)

locale trivariate0_rat
begin

abbreviation X::"rat mpoly_tc" where "X ≡ Var0 (0::nat)"
abbreviation Y::"rat mpoly_tc" where "Y ≡ Var0 (1::nat)"
abbreviation Z::"rat mpoly_tc" where "Z ≡ Var0 (2::nat)"

end

locale trivariate
begin

abbreviation "X ≡ Var 0"
abbreviation "Y ≡ Var 1"
abbreviation "Z ≡ Var 2"

end

experiment begin interpretation trivariate0_rat .

lemma
  "keys (X2 * Z ^ 3 + 2 * Y ^ 3 * Z2) =
    {monomial 2 0 + monomial 3 2, monomial 3 1 + monomial 2 2}"
  by eval

lemma
  "keys (X2 * Z ^ 3 + 2 * Y ^ 3 * Z2) =
    {monomial 2 0 + monomial 3 2, monomial 3 1 + monomial 2 2}"
  by eval

lemma
  "- 1 * X2 * Z ^ 7 + - 2 * Y ^ 3 * Z2 = - X2 * Z ^ 7 + - 2 * Y ^ 3 * Z2"
  by eval

lemma
  "X2 * Z ^ 7 + 2 * Y ^ 3 * Z2 + X2 * Z ^ 4 + - 2 * Y ^ 3 * Z2 = X2 * Z ^ 7 + X2 * Z ^ 4"
  by eval

lemma
  "X2 * Z ^ 7 + 2 * Y ^ 3 * Z2 - X2 * Z ^ 4 + - 2 * Y ^ 3 * Z2 =
    X2 * Z ^ 7 - X2 * Z ^ 4"
  by eval

lemma
  "lookup (X2 * Z ^ 7 + 2 * Y ^ 3 * Z2 + 2) (sparse0 [(0, 2), (2, 7)]) = 1"
  by eval

lemma
  "X2 * Z ^ 7 + 2 * Y ^ 3 * Z2 ≠
   X2 * Z ^ 4 + - 2 * Y ^ 3 * Z2"
  by eval


lemma
  "0 * X^2 * Z^7 + 0 * Y^3*Z2 = 0"
  by eval

lemma
  "monom_mult_punit 3 (sparse0 [(1, 2::nat)]) (X2 * Z + 2 * Y ^ 3 * Z2) =
    3 * Y2 * Z * X2 + 6 * Y ^ 5 * Z2"
  by eval

lemma
  "monomial (-4) (sparse0 [(0, 2::nat)]) = - 4 * X2"
  by eval

lemma "monomial (0::rat) (sparse0 [(0::nat, 2::nat)]) = 0"
  by eval

lemma
  "(X2 * Z + 2 * Y ^ 3 * Z2) * (X2 * Z ^ 3 + - 2 * Y ^ 3 * Z2) =
    X ^ 4 * Z ^ 4 + - 2 * X2 * Z ^ 3 * Y ^ 3 +
 - 4 * Y ^ 6 * Z ^ 4 + 2 * Y ^ 3 * Z ^ 5 * X2"
  by eval

end

subsubsection ‹Vector-Polynomials›

type_synonym 'a vmpoly_tc = "((nat ⇒0 nat) × nat) ⇒0 'a"

definition "shift_map_keys_pprod = pprod.shift_map_keys"

global_interpretation pprod: term_powerprod "λx. x" "λx. x"
  rewrites "pprod.pp_of_term = fst"
  and "pprod.component_of_term = snd"
  defines splus_pprod = pprod.splus
  and monom_mult_pprod = pprod.monom_mult
  and mult_scalar_pprod = pprod.mult_scalar
  and adds_term_pprod = pprod.adds_term
  apply (fact MPoly_Type_Class.pprod.term_powerprod_axioms)
  apply (fact MPoly_Type_Class.pprod_pp_of_term)
  apply (fact MPoly_Type_Class.pprod_component_of_term)
  done

lemma compute_adds_term_pprod [code_unfold]:
  "adds_term_pprod u v = (snd u = snd v ∧ adds_pp_add_linorder (fst u) (fst v))"
  by (simp add: adds_term_pprod_def pprod.adds_term_def adds_pp_add_linorder_def)

lemma compute_splus_pprod [code]: "splus_pprod t (s, i) = (t + s, i)"
  by (simp add: splus_pprod_def pprod.splus_def)

lemma compute_shift_map_keys_pprod [code]:
  "shift_map_keys_pprod t f (fmap_of_list xs) = fmap_of_list (map (λ(k, v). (splus_pprod t k, f v)) xs)"
  by (simp add: pprod.compute_shift_map_keys shift_map_keys_pprod_def splus_pprod_def)

lemma compute_monom_mult_pprod [code]:
  "monom_mult_pprod c t (Pm_fmap xs) = Pm_fmap (if c = 0 then fmempty else shift_map_keys_pprod t ((*) c) xs)"
  by (simp add: monom_mult_pprod_def pprod.compute_monom_mult_poly_mapping shift_map_keys_pprod_def)

lemma compute_mult_scalar_pprod [code]:
  "mult_scalar_pprod (Pm_fmap (fmap_of_list xs)) q = (case xs of ((t, c) # ys) ⇒
    (monom_mult_pprod c t q + mult_scalar_pprod (except (Pm_fmap (fmap_of_list ys)) {t}) q) | _ ⇒
    Pm_fmap fmempty)"
  by (simp only: mult_scalar_pprod_def pprod.compute_mult_scalar_poly_mapping monom_mult_pprod_def)

definition Vec0 :: "nat ⇒ (('a ⇒0 nat) ⇒0 'b) ⇒ (('a ⇒0 nat) × nat) ⇒0 'b::semiring_1" where
  "Vec0 i p = mult_scalar_pprod p (Poly_Mapping.single (0, i) 1)"

experiment begin interpretation trivariate0_rat .

lemma
  "keys (Vec0 0 (X2 * Z ^ 3) + Vec0 1 (2 * Y ^ 3 * Z2)) =
    {(sparse0 [(0, 2), (2, 3)], 0), (sparse0 [(1, 3), (2, 2)], 1)}"
  by eval

lemma
  "keys (Vec0 0 (X2 * Z ^ 3) + Vec0 2 (2 * Y ^ 3 * Z2)) =
    {(sparse0 [(0, 2), (2, 3)], 0), (sparse0 [(1, 3), (2, 2)], 2)}"
  by eval

lemma
  "Vec0 1 (X2 * Z ^ 7 + 2 * Y ^ 3 * Z2) + Vec0 3 (X2 * Z ^ 4) + Vec0 1 (- 2 * Y ^ 3 * Z2) =
    Vec0 1 (X2 * Z ^ 7) + Vec0 3 (X2 * Z ^ 4)"
  by eval

lemma
  "lookup (Vec0 0 (X2 * Z ^ 7) + Vec0 1 (2 * Y ^ 3 * Z2 + 2)) (sparse0 [(0, 2), (2, 7)], 0) = 1"
  by eval

lemma
  "lookup (Vec0 0 (X2 * Z ^ 7) + Vec0 1 (2 * Y ^ 3 * Z2 + 2)) (sparse0 [(0, 2), (2, 7)], 1) = 0"
  by eval

lemma
  "Vec0 0 (0 * X^2 * Z^7) + Vec0 1 (0 * Y^3*Z2) = 0"
  by eval

lemma
  "monom_mult_pprod 3 (sparse0 [(1, 2::nat)]) (Vec0 0 (X2 * Z) + Vec0 1 (2 * Y ^ 3 * Z2)) =
    Vec0 0 (3 * Y2 * Z * X2) + Vec0 1 (6 * Y ^ 5 * Z2)"
  by eval

end

subsection ‹Code setup for type MPoly›

text ‹postprocessing from ‹Var0, Const0› to ‹Var, Const›.›

lemmas [code_post] =
  plus_mpoly.abs_eq[symmetric]
  times_mpoly.abs_eq[symmetric]
  MPoly_numeral
  MPoly_power
  one_mpoly_def[symmetric]
  Var.abs_eq[symmetric]
  Const.abs_eq[symmetric]

instantiation mpoly::("{equal, zero}")equal begin

lift_definition equal_mpoly:: "'a mpoly ⇒ 'a mpoly ⇒ bool" is HOL.equal .

instance proof standard qed (transfer, rule equal_eq)

end

experiment begin interpretation trivariate .

lemmas [mpoly_simps] = plus_mpoly.abs_eq

lemma "content_primitive (4 * X * Y^2 * Z^3 + 6 * X2 * Y^4 + 8 * X2 * Y^5) =
    (2::int, 2 * X * Y2 * Z ^ 3 + 3 * X2 * Y ^ 4 + 4 * X2 * Y ^ 5)"
  by eval

end

end (* theory *)