# Theory Affine_Arithmetic.Affine_Code

```section ‹Implementation›
theory Affine_Code
imports
Affine_Approximation
Intersection
begin

text ‹Implementing partial deviations as sorted lists of coefficients.›

subsection ‹Reverse Sorted, Distinct Association Lists›

typedef (overloaded) ('a, 'b) slist =
"{xs::('a::linorder × 'b) list. distinct (map fst xs) ∧ sorted (rev (map fst xs))}"
by (auto intro!: exI[where x="[]"])

setup_lifting type_definition_slist

lift_definition map_of_slist::"(nat, 'a::zero) slist ⇒ nat ⇒ 'a option" is map_of .

lemma finite_dom_map_of_slist[intro, simp]: "finite (dom (map_of_slist xs))"
by transfer (auto simp: finite_dom_map_of)

abbreviation "the_default a x ≡ (case x of None ⇒ a | Some b ⇒ b)"

definition "Pdevs_raw xs i = the_default 0 (map_of xs i)"

lemma nonzeros_Pdevs_raw_subset: "{i. Pdevs_raw xs i ≠ 0} ⊆ dom (map_of xs)"
unfolding Pdevs_raw_def[abs_def]
by transfer (auto simp: Pdevs_raw_def split: option.split_asm)

lift_definition Pdevs::"(nat, 'a::zero) slist ⇒ 'a pdevs"
is Pdevs_raw
by (rule finite_subset[OF nonzeros_Pdevs_raw_subset]) (simp add: finite_dom_map_of)

code_datatype Pdevs

subsection ‹Degree›

primrec degree_list::"(nat × 'a::zero) list ⇒ nat" where
"degree_list [] = 0"
| "degree_list (x#xs) = (if snd x = 0 then degree_list xs else Suc (fst x))"

lift_definition degree_slist::"(nat, 'a::zero) slist ⇒ nat" is degree_list .

lemma degree_list_eq_zeroD:
assumes "degree_list xs = 0"
shows "the_default 0 (map_of xs i) = 0"
using assms
by (induct xs) (auto simp: Pdevs_raw_def sorted_append split: if_split_asm)

lemma degree_slist_eq_zeroD: "degree_slist xs = 0 ⟹ degree (Pdevs xs) = 0"
unfolding degree_eq_Suc_max
by transfer (auto dest: degree_list_eq_zeroD simp: Pdevs_raw_def)

lemma degree_slist_eq_SucD: "degree_slist xs = Suc n ⟹ pdevs_apply (Pdevs xs) n ≠ 0"
proof (transfer, goal_cases)
case (1 xs n)
thus ?case
by (induct xs)
(auto simp: Pdevs_raw_def sorted_append map_of_eq_None_iff[symmetric]
split: if_split_asm option.split_asm)
qed

lemma degree_slist_zero:
"degree_slist xs = n ⟹ n ≤ j ⟹ pdevs_apply (Pdevs xs) j = 0"
proof (transfer, goal_cases)
case (1 xs n j)
thus ?case
by (induct xs)
(auto simp: Pdevs_raw_def sorted_append split: if_split_asm option.split)
qed

lemma compute_degree[code]: "degree (Pdevs xs) = degree_slist xs"
by (cases "degree_slist xs")
(auto dest: degree_slist_eq_zeroD degree_slist_eq_SucD intro!: degree_eqI degree_slist_zero)

subsection ‹Auxiliary Definitions›

fun binop where
"binop f z1 z2 [] [] = []"
| "binop f z1 z2 ((i, x)#xs) [] = (i, f x z2) # binop f z1 z2 xs []"
| "binop f z1 z2 [] ((i, y)#ys) = (i, f z1 y) # binop f z1 z2 [] ys"
| "binop f z1 z2 ((i, x)#xs) ((j, y)#ys) =
(if (i = j)     then (i, f x y) # binop f z1 z2 xs ys
else if (i > j) then (i, f x z2) # binop f z1 z2 xs ((j, y)#ys)
else                 (j, f z1 y) # binop f z1 z2 ((i, x)#xs) ys)"

lemma set_binop_elemD1:
"(a, b) ∈ set (binop f z1 z2 xs ys) ⟹ (a ∈ set (map fst xs) ∨ a ∈ set (map fst ys))"
by (induct f z1 z2 xs ys rule: binop.induct) (auto split: if_split_asm)

lemma set_binop_elemD2:
"(a, b) ∈ set (binop f z1 z2 xs ys) ⟹
(∃x∈set (map snd xs). b = f x z2) ∨
(∃y∈set (map snd ys). b = f z1 y) ∨
(∃x∈set (map snd xs). ∃y∈set (map snd ys). b = f x y)"
by (induct f z1 z2 xs ys rule: binop.induct) (auto split: if_split_asm)

abbreviation "rsorted≡λx. sorted (rev x)"

lemma rsorted_binop:
fixes xs::"('a::linorder * 'b) list" and ys::"('a::linorder * 'c) list"
assumes "rsorted ((map fst xs))"
assumes "rsorted ((map fst ys))"
shows "rsorted ((map fst (binop f z1 z2 xs ys)))"
using assms
by (induct f z1 z2 xs ys rule: binop.induct) (force simp: sorted_append dest!: set_binop_elemD1)+

lemma distinct_binop:
fixes xs::"('a::linorder * 'b) list" and ys::"('a::linorder * 'c) list"
assumes "distinct (map fst xs)"
assumes "distinct (map fst ys)"
assumes "rsorted ((map fst xs))"
assumes "rsorted ((map fst ys))"
shows "distinct (map fst (binop f z1 z2 xs ys))"
using assms
by (induct f z1 z2 xs ys rule: binop.induct)
(force dest!: set_binop_elemD1 simp: sorted_append)+

lemma binop_plus:
fixes b::"(nat * 'a::euclidean_space) list"
shows
"(∑(i, y)←binop (+) 0 0 b ba. e i *⇩R y) = (∑(i, y)←b. e i *⇩R y) + (∑(i, y)←ba. e i *⇩R y)"
by (induct "(+) ::'a⇒_" "0::'a" "0::'a" b ba rule: binop.induct)
(auto simp: algebra_simps)

lemma binop_compose:
"binop (λx y. f (g x y)) z1 z2 xs ys = map (apsnd f) (binop g z1 z2 xs ys)"
by (induct "λx y. f (g x y)" z1 z2 xs ys rule: binop.induct) auto

lemma linear_cmul_left[intro, simp]: "linear ((*) x::real ⇒ _)"
by (auto intro!: linearI simp: algebra_simps)

lemma length_merge_sorted_eq:
"length (binop f z1 z2 xs ys) = length (binop g y1 y2 xs ys)"
by (induction f z1 z2 xs ys rule: binop.induct) auto

lift_definition add_slist::"(nat, 'a::{plus, zero}) slist ⇒ (nat, 'a) slist ⇒ (nat, 'a) slist" is
"λxs ys. binop (+) 0 0 xs ys"
by (auto simp: intro!: distinct_binop rsorted_binop)

lemma map_of_binop[simp]: "rsorted (map fst xs) ⟹ rsorted (map fst ys) ⟹
distinct (map fst xs) ⟹ distinct (map fst ys) ⟹
map_of (binop f z1 z2 xs ys) i =
(case map_of xs i of
Some x ⇒ Some (f x (case map_of ys i of Some x ⇒ x | None ⇒ z2))
| None ⇒ (case map_of ys i of Some y ⇒ Some (f z1 y) | None ⇒ None))"
by (induct f z1 z2 xs ys rule: binop.induct)
(auto split: option.split option.split_asm simp: sorted_append)

shows "pdevs_apply (Pdevs (add_slist xs ys)) i =
pdevs_apply (Pdevs xs) i + pdevs_apply (Pdevs ys) i"
by (transfer) (auto simp: Pdevs_raw_def split: option.split)

by (rule pdevs_eqI) simp

subsection ‹prod of pdevs›

lift_definition prod_slist::"(nat, 'a::zero) slist ⇒ (nat, 'b::zero) slist ⇒ (nat, ('a × 'b)) slist" is
"λxs ys. binop Pair 0 0 xs ys"
by (auto simp: intro!: distinct_binop rsorted_binop)

lemma pdevs_apply_Pdevs_prod_slist[simp]:
"pdevs_apply (Pdevs (prod_slist xs ys)) i = (pdevs_apply (Pdevs xs) i, pdevs_apply (Pdevs ys) i)"
by transfer (auto simp: Pdevs_raw_def zero_prod_def split: option.splits)

lemma compute_prod_of_pdevs[code]: "prod_of_pdevs (Pdevs xs) (Pdevs ys) = Pdevs (prod_slist xs ys)"
by (rule pdevs_eqI) simp

subsection ‹Set of Coefficients›

lift_definition set_slist::"(nat, 'a::real_vector) slist ⇒ (nat * 'a) set" is set .

lemma finite_set_slist[intro, simp]: "finite (set_slist xs)"
by transfer simp

subsection ‹Domain›

lift_definition list_of_slist::"('a::linorder, 'b::zero) slist ⇒ ('a * 'b) list"
is "λxs. filter (λx. snd x ≠ 0) xs" .

lemma compute_pdevs_domain[code]: "pdevs_domain (Pdevs xs) = set (map fst (list_of_slist xs))"
unfolding pdevs_domain_def
by transfer (force simp: Pdevs_raw_def split: option.split_asm)

lemma sort_rev_eq_sort: "distinct xs ⟹ sort (rev xs) = sort xs"
by (rule sorted_distinct_set_unique) auto

lemma compute_list_of_pdevs[code]: "list_of_pdevs (Pdevs xs) = list_of_slist xs"
proof -
have "list_of_pdevs (Pdevs xs) =
map (λi. (i, pdevs_apply (Pdevs xs) i)) (rev (sorted_list_of_set (pdevs_domain (Pdevs xs))))"
also have "(sorted_list_of_set (pdevs_domain (Pdevs xs))) = rev (map fst (list_of_slist xs))"
unfolding compute_pdevs_domain sorted_list_of_set_sort_remdups
proof (transfer, goal_cases)
case prems: (1 xs)
hence distinct: "distinct (map fst [x←xs . snd x ≠ 0])"
by (auto simp: filter_map distinct_map intro: subset_inj_on)
with prems show ?case
using sort_rev_eq_sort[symmetric, OF distinct]
by (auto simp: rev_map rev_filter distinct_map distinct_remdups_id
intro!: sorted_sort_id sorted_filter)
qed
also
have "map (λi. (i, pdevs_apply (Pdevs xs) i)) (rev …) = list_of_slist xs"
proof (transfer, goal_cases)
case (1 xs)
thus ?case
unfolding Pdevs_raw_def o_def rev_rev_ident map_map
by (subst map_cong[where g="λx. x"]) (auto simp: map_filter_map_filter)
qed
finally show ?thesis .
qed

lift_definition slist_of_pdevs::"'a pdevs ⇒ (nat, 'a::real_vector) slist" is list_of_pdevs
by (auto simp: list_of_pdevs_def rev_map rev_filter
filter_map o_def distinct_map image_def
intro!: distinct_filter sorted_filter[of "λx. x", simplified])

subsection ‹Application›

lift_definition slist_apply::"('a::linorder, 'b::zero) slist ⇒ 'a ⇒ 'b" is
"λxs i. the_default 0 (map_of xs i)" .

lemma compute_pdevs_apply[code]: "pdevs_apply (Pdevs x) i = slist_apply x i"
by transfer (auto simp: Pdevs_raw_def)

subsection ‹Total Deviation›

lift_definition tdev_slist::"(nat, 'a::ordered_euclidean_space) slist ⇒ 'a" is
"sum_list o map (abs o snd)" .

lemma tdev_slist_sum: "tdev_slist xs = sum (abs ∘ snd) (set_slist xs)"
by transfer (auto simp: distinct_map sum_list_distinct_conv_sum_set[symmetric] o_def)

lemma pdevs_apply_set_slist: "x ∈ set_slist xs ⟹ snd x = pdevs_apply (Pdevs xs) (fst x)"
by transfer (auto simp: Pdevs_raw_def)

lemma
tdev_list_eq_zeroI:
shows "(⋀i. pdevs_apply (Pdevs xs) i = 0) ⟹ tdev_slist xs = 0"
unfolding tdev_slist_sum
by (auto simp: pdevs_apply_set_slist)

lemma inj_on_fst_set_slist: "inj_on fst (set_slist xs)"

lemma pdevs_apply_Pdevs_eq_0:
"pdevs_apply (Pdevs xs) i = 0 ⟷ ((∀x. (i, x) ∈ set_slist xs ⟶ x = 0))"
by transfer (safe, auto simp: Pdevs_raw_def split: option.split)

lemma compute_tdev[code]: "tdev (Pdevs xs) = tdev_slist xs"
proof -
have "tdev (Pdevs xs) = (∑i<degree (Pdevs xs). ¦pdevs_apply (Pdevs xs) i¦)"
also have "… =
(∑i <degree (Pdevs xs).
if pdevs_apply (Pdevs xs) i = 0 then 0 else ¦pdevs_apply (Pdevs xs) i¦)"
by (auto intro!: sum.cong)
also have "… =
(∑i∈{0..<degree (Pdevs xs)} ∩ {x. pdevs_apply (Pdevs xs) x ≠ 0}.
¦pdevs_apply (Pdevs xs) i¦)"
by (auto simp: sum.If_cases Collect_neg_eq atLeast0LessThan)
also have "… = (∑x∈fst ` set_slist xs. ¦pdevs_apply (Pdevs xs) x¦)"
by (rule sum.mono_neutral_cong_left)
(force simp: pdevs_apply_Pdevs_eq_0 intro!: imageI degree_gt)+
also have "… = (∑x∈set_slist xs. ¦pdevs_apply (Pdevs xs) (fst x)¦)"
by (rule sum.reindex_cong[of fst]) (auto simp: inj_on_fst_set_slist)
also have "… = tdev_slist xs"
finally show ?thesis .
qed

subsection ‹Minkowski Sum›

lemma dropWhile_rsorted_eq_filter:
"rsorted (map fst xs) ⟹ dropWhile (λ(i, x). i ≥ (m::nat)) xs = filter (λ(i, x). i < m) xs"
(is "_ ⟹ ?lhs xs = ?rhs xs")
proof (induct xs)
case (Cons x xs)
hence "?rhs (x#xs) = ?lhs (x#xs)"
by (auto simp: sorted_append filter_id_conv intro: sym)
thus ?case ..
qed simp

lift_definition msum_slist::"nat ⇒ (nat, 'a) slist ⇒ (nat, 'a) slist ⇒ (nat, 'a) slist"
is "λm xs ys. map (apfst (λn. n + m)) ys @ dropWhile (λ(i, x). i ≥ m) xs"
proof (safe, goal_cases)
case (1 n l1 l2)
then have "set (dropWhile (λ(i, x). n ≤ i) l1) ⊆ set l1"
with 1 show ?case
by (auto simp add: distinct_map add.commute [of _ n] intro!: comp_inj_on intro: subset_inj_on)
next
case prems: (2 n l1 l2)
hence "sorted (map ((λna. na + n) ∘ fst) (rev l2))"
with prems show ?case
by (auto simp: sorted_append dropWhile_rsorted_eq_filter rev_map rev_filter sorted_filter)
qed

lemma slist_apply_msum_slist:
"slist_apply (msum_slist m xs ys) i =
(if i < m then slist_apply xs i else slist_apply ys (i - m))"
proof (transfer, goal_cases)
case prems: (1 m xs ys i)
thus ?case
proof (cases "i ∈ dom (map_of (map (λ(x, y). (x + m, y)) ys))")
case False
have "⋀a. i < m ⟹ i ∉ fst ` {x ∈ set xs. case x of (i, x) ⇒ i < m} ⟹ (i, a) ∉ set xs"
"⋀a. i ∉ fst ` set xs ⟹ (i, a) ∉ set xs"
"⋀a. m ≤ i ⟹ i ∉ fst ` (λ(x, y). (x + m, y)) ` set ys ⟹ (i - m, a) ∉ set ys"
by force+
thus ?thesis
using prems False
by (auto simp add: dropWhile_rsorted_eq_filter map_of_eq_None_iff distinct_map_fst_snd_eqD
split: option.split dest!: map_of_SomeD)
qed (force simp: map_of_eq_None_iff distinct_map_fst_snd_eqD
split: option.split
dest!: map_of_SomeD)
qed

lemma pdevs_apply_msum_slist:
"pdevs_apply (Pdevs (msum_slist m xs ys)) i =
(if i < m then pdevs_apply (Pdevs xs) i else pdevs_apply (Pdevs ys) (i - m))"
by (auto simp: compute_pdevs_apply slist_apply_msum_slist)

lemma compute_msum_pdevs[code]: "msum_pdevs m (Pdevs xs) (Pdevs ys) = Pdevs (msum_slist m xs ys)"
by (rule pdevs_eqI) (auto simp: pdevs_apply_msum_slist pdevs_apply_msum_pdevs)

subsection ‹Unary Operations›

lift_definition map_slist::"('a ⇒ 'b) ⇒ (nat, 'a) slist ⇒ (nat, 'b) slist" is "λf. map (apsnd f)"
by simp

lemma pdevs_apply_map_slist:
"f 0 = 0 ⟹ pdevs_apply (Pdevs (map_slist f xs)) i = f (pdevs_apply (Pdevs xs) i)"
by transfer
(force simp: Pdevs_raw_def map_of_eq_None_iff distinct_map_fst_snd_eqD image_def
split: option.split dest: distinct_map_fst_snd_eqD)

lemma compute_scaleR_pdves[code]: "scaleR_pdevs r (Pdevs xs) = Pdevs (map_slist (λx. r *⇩R x) xs)"
and compute_pdevs_scaleR[code]: "pdevs_scaleR (Pdevs rs) x = Pdevs (map_slist (λr. r *⇩R x) rs)"
and compute_uminus_pdevs[code]: "uminus_pdevs (Pdevs xs) = Pdevs (map_slist (λx. - x) xs)"
and compute_abs_pdevs[code]: "abs_pdevs (Pdevs xs) = Pdevs (map_slist abs xs)"
and compute_pdevs_inner[code]: "pdevs_inner (Pdevs xs) b = Pdevs (map_slist (λx. x ∙ b) xs)"
and compute_pdevs_inner2[code]:
"pdevs_inner2 (Pdevs xs) b c = Pdevs (map_slist (λx. (x ∙ b, x ∙ c)) xs)"
and compute_inner_scaleR_pdevs[code]:
"inner_scaleR_pdevs x (Pdevs ys) = Pdevs (map_slist (λy. (x ∙ y) *⇩R y) ys)"
and compute_trunc_pdevs[code]:
"trunc_pdevs p (Pdevs xs) = Pdevs (map_slist (λx. eucl_truncate_down p x) xs)"
and compute_trunc_err_pdevs[code]:
"trunc_err_pdevs p (Pdevs xs) = Pdevs (map_slist (λx. eucl_truncate_down p x - x) xs)"
by (auto intro!: pdevs_eqI simp: pdevs_apply_map_slist zero_prod_def abs_pdevs_def)

subsection ‹Filter›

lift_definition filter_slist::"(nat ⇒ 'a ⇒ bool) ⇒ (nat, 'a) slist ⇒ (nat, 'a) slist"
is "λP xs. filter (λ(i, x). (P i x)) xs"
by (auto simp: o_def filter_map distinct_map rev_map rev_filter sorted_filter
intro: subset_inj_on)

lemma slist_apply_filter_slist: "slist_apply (filter_slist P xs) i =
(if P i (slist_apply xs i) then slist_apply xs i else 0)"
by transfer (force simp: Pdevs_raw_def o_def map_of_eq_None_iff distinct_map_fst_snd_eqD
dest: map_of_SomeD distinct_map_fst_snd_eqD split: option.split)

lemma pdevs_apply_filter_slist: "pdevs_apply (Pdevs (filter_slist P xs)) i =
(if P i (pdevs_apply (Pdevs xs) i) then pdevs_apply (Pdevs xs) i else 0)"

lemma compute_filter_pdevs[code]: "filter_pdevs P (Pdevs xs) = Pdevs (filter_slist P xs)"
by (auto simp: pdevs_apply_filter_slist intro!: pdevs_eqI)

subsection ‹Constant›

lift_definition zero_slist::"(nat, 'a) slist" is "[]" by simp

lemma compute_zero_pdevs[code]: "zero_pdevs = Pdevs (zero_slist)"
by transfer (auto simp: Pdevs_raw_def)

lift_definition One_slist::"(nat, 'a::executable_euclidean_space) slist"
is "rev (zip [0..<length (Basis_list::'a list)] (Basis_list::'a list))"

lemma
map_of_rev_zip_upto_length_eq_nth:
assumes "i < length B" "d = length B"
shows "(map_of (rev (zip [0..<d] B)) i) = Some (B ! i)"
proof -
have "length (rev [0..<length B]) = length (rev B)"
by simp
from map_of_zip_is_Some[OF this, of i] assms
obtain y where y: "map_of (zip (rev [0..<length B]) (rev B)) i = Some y"
by (auto simp: zip_rev)
hence "y = B ! i"
by (auto simp: in_set_zip rev_nth)
with y show ?thesis
qed

lemma
map_of_rev_zip_upto_length_eq_None:
assumes "¬i < length B"
assumes "d = length B"
shows "(map_of (rev (zip [0..<d] B)) i) = None"
using assms
by (auto simp: map_of_eq_None_iff in_set_zip)

lemma pdevs_apply_One_slist:
"pdevs_apply (Pdevs One_slist) i =
(if i < length (Basis_list::'a::executable_euclidean_space list)
then (Basis_list::'a list) ! i
else 0)"
by transfer (auto simp: Pdevs_raw_def map_of_rev_zip_upto_length_eq_nth map_of_rev_zip_upto_length_eq_None
in_set_zip split: option.split)

lemma compute_One_pdevs[code]: "One_pdevs = Pdevs One_slist"
by (rule pdevs_eqI) (simp add: pdevs_apply_One_slist)

lift_definition coord_slist::"nat ⇒ (nat, real) slist" is "λi. [(i, 1)]" by simp

lemma compute_coord_pdevs[code]: "coord_pdevs i = Pdevs (coord_slist i)"
by transfer (auto simp: Pdevs_raw_def)

subsection ‹Update›

primrec update_list::"nat ⇒ 'a ⇒ (nat * 'a) list ⇒ (nat * 'a) list"
where
"update_list n x [] = [(n, x)]"
| "update_list n x (y#ys) =
(if n > fst y then (n, x)#y#ys
else if n = fst y then (n, x)#ys
else y#(update_list n x ys))"

lemma map_of_update_list[simp]: "map_of (update_list n x ys) = (map_of ys)(n:=Some x)"
by (induct ys) auto

lemma in_set_update_listD:
assumes "y ∈ set (update_list n x ys)"
shows "y = (n, x) ∨ (y ∈ set ys)"
using assms
by (induct ys) (auto split: if_split_asm)

lemma in_set_update_listI:
"y = (n, x) ∨ (fst y ≠ n ∧ y ∈ set ys) ⟹ y ∈ set (update_list n x ys)"
by (induct ys) (auto split: if_split_asm)

lemma in_set_update_list: "(n, x) ∈ set (update_list n x xs)"
by (induct xs) simp_all

lemma overwrite_update_list: "(a, b) ∈ set xs ⟹ (a, b) ∉ set (update_list n x xs) ⟹ a = n"
by (induct xs) (auto split: if_split_asm)

lemma insert_update_list:
"distinct (map fst xs) ⟹ rsorted (map fst xs) ⟹ (a, b) ∈ set (update_list a x xs) ⟹ b = x"
by (induct xs) (force split: if_split_asm simp: sorted_append)+

lemma set_update_list_eq: "distinct (map fst xs) ⟹ rsorted (map fst xs) ⟹
set (update_list n x xs) = insert (n, x) (set xs - {x. fst x = n})"
by (auto intro!: in_set_update_listI dest: in_set_update_listD simp: insert_update_list)

lift_definition update_slist::"nat ⇒ 'a ⇒ (nat, 'a) slist ⇒ (nat, 'a) slist" is update_list
proof goal_cases
case (1 n a l)
thus ?case
by (induct l) (force simp: sorted_append distinct_map not_less dest!: in_set_update_listD)+
qed

lemma pdevs_apply_update_slist: "pdevs_apply (Pdevs (update_slist n x xs)) i =
(if i = n then x else pdevs_apply (Pdevs xs) i)"
by transfer (auto simp: Pdevs_raw_def)

lemma compute_pdev_upd[code]: "pdev_upd (Pdevs xs) n x = Pdevs (update_slist n x xs)"
by (rule pdevs_eqI) (auto simp: pdevs_apply_update_slist)

subsection ‹Approximate Total Deviation›

lift_definition fold_slist::"('a ⇒ 'b ⇒ 'b) ⇒ (nat, 'a::zero) slist ⇒ 'b ⇒ 'b"
is "λf xs z. fold (f o snd) (filter (λx. snd x ≠ 0) xs) z" .

lemma Pdevs_raw_Cons:
"Pdevs_raw ((a, b) # xs) = (λi. if i = a then b else Pdevs_raw xs i)"
by (auto simp: Pdevs_raw_def map_of_eq_None_iff
dest!: map_of_SomeD
split: option.split)

lemma zeros_aux: "- (λi. if i = a then b else Pdevs_raw xs i) -` {0} ⊆
- Pdevs_raw xs -` {0} ∪ {a}"
by auto

lemma compute_tdev'[code]:
"tdev' p (Pdevs xs) = fold_slist (λa b. eucl_truncate_up p (¦a¦ + b)) xs 0"
unfolding tdev'_def sum_list'_def compute_list_of_pdevs
by transfer (auto simp: o_def fold_map)

subsection ‹Equality›

lemma slist_apply_list_of_slist_eq: "slist_apply a i = the_default 0 (map_of (list_of_slist a) i)"
by (transfer)
(force split: option.split simp: map_of_eq_None_iff distinct_map_fst_snd_eqD
dest!: map_of_SomeD)

lemma compute_equal_pdevs[code]:
"equal_class.equal (Pdevs a) (Pdevs b) ⟷ (list_of_slist a) = (list_of_slist b)"
by (auto intro!: pdevs_eqI simp: equal_pdevs_def compute_pdevs_apply slist_apply_list_of_slist_eq
compute_list_of_pdevs[symmetric])

subsection ‹From List of Generators›

lift_definition slist_of_list::"'a::zero list ⇒ (nat, 'a) slist"
is "λxs. rev (zip [0..<length xs] xs)"
by (auto simp: rev_map[symmetric] )

lemma slist_apply_slist_of_list:
"slist_apply (slist_of_list xs) i = (if i < length xs then xs ! i else 0)"
by transfer (auto simp: in_set_zip map_of_rev_zip_upto_length_eq_nth map_of_rev_zip_upto_length_eq_None)

lemma compute_pdevs_of_list[code]: "pdevs_of_list xs = Pdevs (slist_of_list xs)"
by (rule pdevs_eqI)
(auto simp: compute_pdevs_apply slist_apply_slist_of_list pdevs_apply_pdevs_of_list)

text ‹abstraction function which can be used in code equations›

lift_definition abs_slist_if::"('a::linorder×'b) list ⇒ ('a, 'b) slist"
is "λlist. if distinct (map fst list) ∧ rsorted (map fst list) then list else []"
by auto

definition "slist = Abs_slist"

lemma [code_post]: "Abs_slist = slist"

lemma [code]: "slist = (λxs.
(if distinct (map fst xs) ∧ rsorted (map fst xs) then abs_slist_if xs else Code.abort (STR '''') (λ_. slist xs)))"
by (auto simp add: slist_def abs_slist_if.abs_eq)

abbreviation "pdevs ≡ (λx. Pdevs (slist x))"

lift_definition nlex_slist::"(nat, point) slist ⇒ (nat, point) slist" is
"map (λ(i, x). (i, if lex 0 x then - x else x))"
by (auto simp: o_def split_beta')

lemma Pdevs_raw_map: "f 0 = 0 ⟹ Pdevs_raw (map (λ(i, x). (i, f x)) xs) i = f (Pdevs_raw xs i)"
by (auto simp: Pdevs_raw_def map_of_map split: option.split)

lemma compute_nlex_pdevs[code]: "nlex_pdevs (Pdevs x) = Pdevs (nlex_slist x)"
by transfer (auto simp: Pdevs_raw_map)

end
```