# Theory Polynomials.Poly_Mapping_Finite_Map

```(* Author: Fabian Immler, TU Muenchen
*)
theory Poly_Mapping_Finite_Map
imports
"More_MPoly_Type"
"HOL-Library.Finite_Map"
begin

subsection ‹TODO: move!›

lemma fmdom'_fmap_of_list: "fmdom' (fmap_of_list xs) = set (map fst xs)"
by (auto simp: fmdom'_def fmdom'I fmap_of_list.rep_eq weak_map_of_SomeI)
(metis map_of_eq_None_iff option.distinct(1))

text ‹In this theory, type @{typ "('a, 'b) poly_mapping"} is represented as association lists.
Code equations are proved in order actually perform computations (addition, multiplication, etc.).›

subsection ‹Utilities›

instantiation poly_mapping :: (type, "{equal, zero}") equal
begin
definition equal_poly_mapping::"('a, 'b) poly_mapping ⇒ ('a, 'b) poly_mapping ⇒ bool" where
"equal_poly_mapping p q ≡ (∀t. lookup p t = lookup q t)"

instance by standard (auto simp add: equal_poly_mapping_def poly_mapping_eqI)
end

definition "clearjunk0 m = fmfilter (λk. fmlookup m k ≠ Some 0) m"

definition "fmlookup_default d m x = (case fmlookup m x of Some v ⇒ v | None ⇒ d)"
abbreviation "lookup0 ≡ fmlookup_default 0"

lemma fmlookup_default_fmmap:
"fmlookup_default d (fmmap f M) x = (if x ∈ fmdom' M then f (fmlookup_default d M x) else d)"
by (auto simp: fmlookup_default_def fmdom'_notI split: option.splits)

lemma fmlookup_default_fmmap_keys: "fmlookup_default d (fmmap_keys f M) x =
(if x ∈ fmdom' M then f x (fmlookup_default d M x) else d)"
by (auto simp: fmlookup_default_def fmdom'_notI split: option.splits)

"fmlookup_default d (m ++⇩f n) x =
(if x |∈| fmdom n then the (fmlookup n x)
else fmlookup_default d m x)"
by (auto simp: fmlookup_default_def)

lemma fmlookup_default_if[simp]:
"fmlookup ys a = Some r ⟹ fmlookup_default d ys a = r"
"fmlookup ys a = None ⟹ fmlookup_default d ys a = d"
by (auto simp: fmlookup_default_def)

lemma finite_lookup_default:
"finite {x. fmlookup_default d xs x ≠ d}"
proof -
have "{x. fmlookup_default d xs x ≠ d} ⊆ fmdom' xs"
by (auto simp: fmlookup_default_def fmdom'I split: option.splits)
also have "finite …"
by simp
finally (finite_subset) show ?thesis .
qed

lemma lookup0_clearjunk0: "lookup0 xs s = lookup0 (clearjunk0 xs) s"
unfolding clearjunk0_def fmlookup_default_def
by auto

lemma clearjunk0_nonzero:
assumes "t ∈ fmdom' (clearjunk0 xs)"
shows "fmlookup xs t ≠ Some 0"
using assms unfolding clearjunk0_def by simp

lemma clearjunk0_map_of_SomeD:
assumes a1: "fmlookup xs t = Some c" and "c ≠ 0"
shows "t ∈ fmdom' (clearjunk0 xs)"
using assms
by (auto simp: clearjunk0_def fmdom'I)

subsection ‹Implementation of Polynomial Mappings as Association Lists›

lift_definition Pm_fmap::"('a, 'b::zero) fmap ⇒ 'a ⇒⇩0 'b" is lookup0
by (rule finite_lookup_default)

lemmas [simp] = Pm_fmap.rep_eq

code_datatype Pm_fmap

lemma PM_clearjunk0_cong:
"Pm_fmap (clearjunk0 xs) = Pm_fmap xs"
by (metis Pm_fmap.rep_eq lookup0_clearjunk0 poly_mapping_eqI)

lemma PM_all_2:
assumes "P 0 0"
shows "(∀x. P (lookup (Pm_fmap xs) x) (lookup (Pm_fmap ys) x)) =
fmpred (λk v. P (lookup0 xs k) (lookup0 ys k)) (xs ++⇩f ys)"
using assms unfolding list_all_def
by (force simp: fmlookup_default_def fmlookup_dom_iff
split: option.splits if_splits)

lemma compute_keys_pp[code]: "keys (Pm_fmap xs) = fmdom' (clearjunk0 xs)"
by transfer
(auto simp: fmlookup_dom'_iff clearjunk0_def fmlookup_default_def fmdom'I split: option.splits)

lemma compute_zero_pp[code]: "0 = Pm_fmap fmempty"
by (auto intro!: poly_mapping_eqI simp: fmlookup_default_def)

lemma compute_plus_pp [code]:
"Pm_fmap xs + Pm_fmap ys = Pm_fmap (clearjunk0 (fmmap_keys (λk v. lookup0 xs k + lookup0 ys k) (xs ++⇩f ys)))"
by (auto intro!: poly_mapping_eqI
split: option.splits)

lemma compute_lookup_pp[code]:
"lookup (Pm_fmap xs) x = lookup0 xs x"
by (transfer, simp)

lemma compute_minus_pp [code]:
"Pm_fmap xs - Pm_fmap ys = Pm_fmap (clearjunk0 (fmmap_keys (λk v. lookup0 xs k - lookup0 ys k) (xs ++⇩f ys)))"
by (auto intro!: poly_mapping_eqI
simp: fmlookup_default_def lookup_minus fmlookup_dom_iff PM_clearjunk0_cong
split: option.splits)

lemma compute_uminus_pp[code]:
"- Pm_fmap ys = Pm_fmap (fmmap_keys (λk v. - lookup0 ys k) ys)"
by (auto intro!: poly_mapping_eqI
simp: fmlookup_default_def
split: option.splits)

lemma compute_equal_pp[code]:
"equal_class.equal (Pm_fmap xs) (Pm_fmap ys) = fmpred (λk v. lookup0 xs k = lookup0 ys k) (xs ++⇩f ys)"
unfolding equal_poly_mapping_def by (simp only: PM_all_2)

lemma compute_map_pp[code]:
"Poly_Mapping.map f (Pm_fmap xs) = Pm_fmap (fmmap (λx. f x when x ≠ 0) xs)"
by (auto intro!: poly_mapping_eqI
simp: fmlookup_default_def map.rep_eq
split: option.splits)

lemma fmran'_fmfilter_eq: "fmran' (fmfilter p fm) = {y | y. ∃x ∈ fmdom' fm. p x ∧ fmlookup fm x = Some y}"
by (force simp: fmlookup_ran'_iff fmdom'I split: if_splits)

lemma compute_range_pp[code]:
"Poly_Mapping.range (Pm_fmap xs) = fmran' (clearjunk0 xs)"
by (force simp: range.rep_eq clearjunk0_def fmran'_fmfilter_eq fmdom'I
fmlookup_default_def split: option.splits)

subsubsection ‹Constructors›

definition "sparse⇩0 xs = Pm_fmap (fmap_of_list xs)" ―‹sparse representation›
definition "dense⇩0 xs = Pm_fmap (fmap_of_list (zip [0..<length xs] xs))" ―‹dense representation›

lemma compute_single[code]: "Poly_Mapping.single k v = sparse⇩0 [(k, v)]"
by (auto simp: sparse⇩0_def fmlookup_default_def lookup_single intro!: poly_mapping_eqI )

end
```