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) 
    (xset (map snd xs). b = f x z2) 
    (yset (map snd ys). b = f z1 y) 
    (xset (map snd xs). yset (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 [xxs . 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 " = (xfst ` 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 " = (xset_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