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


subsection ‹Pointswise Addition›

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)

lemma pdevs_apply_Pdevs_add_slist[simp]:
  fixes xs ys::"(nat, 'a::monoid_add) slist"
  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)

lemma compute_add_pdevs[code]: "add_pdevs (Pdevs xs) (Pdevs ys) = Pdevs (add_slist xs ys)"
  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))))"
    by (simp add: list_of_pdevs_def)
  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)"
  by transfer (simp add: distinct_map)

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¦)"
    by (simp add: tdev_def)
  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"
    by (simp add: tdev_slist_sum pdevs_apply_set_slist)
  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"
    by (simp add: set_dropWhileD subrelI)
  with 1 show ?case
    by (auto simp add: distinct_map add.commute [of _ n] intro!: comp_inj_on intro: subset_inj_on)
      (simp add: dropWhile_rsorted_eq_filter)
next
  case prems: (2 n l1 l2)
  hence "sorted (map ((λna. na + n) ∘ fst) (rev l2))"
    by(simp add: sorted_iff_nth_mono rev_map)
  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)"
  by (simp add: compute_pdevs_apply slist_apply_filter_slist)

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))"
  by (simp add: zip_rev[symmetric])

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
    by (simp add: zip_rev assms)
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"
  by (simp add: slist_def)

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