Theory More_Sepref.WB_More_Refinement_List

theory WB_More_Refinement_List
  imports Weidenbach_Book_Base.WB_List_More
    Word_Lib.Many_More ― ‹provides some additional lemmas like @{thm nth_rev}›
    Isabelle_LLVM.Refine_Monadic_Thin
    Isabelle_LLVM.More_List
begin

no_notation funcset (infixr "→" 60)


section ‹More theorems about list›

text ‹This should theorem and functions that defined in the Refinement Framework, but not in
\<^theory>‹HOL.List›. There might be moved somewhere eventually in the AFP or so.
  ›
(* Taken from IICF_List*)
subsection ‹Swap two elements of a list, by index›

definition swap where "swap l i j ≡ l[i := l!j, j:=l!i]"

lemma swap_nth[simp]: "⟦i < length l; j<length l; k<length l⟧ ⟹
  swap l i j!k = (
    if k=i then l!j
    else if k=j then l!i
    else l!k
  )"
  unfolding swap_def
  by auto

lemma swap_set[simp]: "⟦ i < length l; j<length l ⟧ ⟹ set (swap l i j) = set l"
  unfolding swap_def
  by auto

lemma swap_multiset[simp]: "⟦ i < length l; j<length l ⟧ ⟹ mset (swap l i j) = mset l"
  unfolding swap_def
  by (auto simp: mset_swap)


lemma swap_length[simp]: "length (swap l i j) = length l"
  unfolding swap_def
  by auto

lemma swap_same[simp]: "swap l i i = l"
  unfolding swap_def by auto

lemma distinct_swap[simp]:
  "⟦i<length l; j<length l⟧ ⟹ distinct (swap l i j) = distinct l"
  unfolding swap_def
  by auto

lemma map_swap: "⟦i<length l; j<length l⟧
  ⟹ map f (swap l i j) = swap (map f l) i j"
  unfolding swap_def
  by (auto simp add: map_update)

lemma swap_nth_irrelevant:
  ‹k ≠ i ⟹ k ≠ j ⟹ swap xs i j ! k = xs ! k›
  by (auto simp: swap_def)

lemma swap_nth_relevant:
  ‹i < length xs ⟹ j < length xs ⟹ swap xs i j ! i = xs ! j›
  by (cases ‹i = j›) (auto simp: swap_def)

lemma swap_nth_relevant2:
  ‹i < length xs ⟹ j < length xs ⟹ swap xs j i ! i = xs ! j›
  by (auto simp: swap_def)

lemma swap_nth_if:
  ‹i < length xs ⟹ j < length xs ⟹ swap xs i j ! k =
    (if k = i then xs ! j else if k = j then xs ! i else xs ! k)›
  by (auto simp: swap_def)

lemma drop_swap_irrelevant:
  ‹k > i ⟹ k > j ⟹ drop k (swap outl' j i) = drop k outl'›
  by (subst list_eq_iff_nth_eq) auto

lemma take_swap_relevant:
  ‹k > i ⟹ k > j ⟹  take k (swap outl' j i) = swap (take k outl') i j›
  by (subst list_eq_iff_nth_eq) (auto simp: swap_def)

lemma tl_swap_relevant:
  ‹i > 0 ⟹ j > 0 ⟹ tl (swap outl' j i) = swap (tl outl') (i - 1) (j - 1)›
  by (subst list_eq_iff_nth_eq)
    (cases ‹outl' = []›; cases i; cases j; auto simp: swap_def tl_update_swap nth_tl)

lemma swap_only_first_relevant:
  ‹b ≥ i ⟹ a < length xs  ⟹take i (swap xs a b) = take i (xs[a := xs ! b])›
  by (auto simp: swap_def)

text ‹TODO this should go to a different place from the previous lemmas, since it concerns
\<^term>‹Misc.slice›, which is not part of \<^theory>‹HOL.List› but only part of the Refinement Framework.
›
lemma slice_nth:
  ‹⟦from ≤ length xs; i < to - from⟧ ⟹ Misc.slice from to xs ! i = xs ! (from + i)›
  unfolding slice_def Misc.slice_def
  apply (subst nth_take, assumption)
  apply (subst nth_drop, assumption)
  ..

lemma slice_irrelevant[simp]:
  ‹i < from ⟹ Misc.slice from to (xs[i := C]) = Misc.slice from to xs›
  ‹i ≥ to ⟹ Misc.slice from to (xs[i := C]) = Misc.slice from to xs›
  ‹i ≥ to ∨ i < from ⟹ Misc.slice from to (xs[i := C]) = Misc.slice from to xs›
  unfolding Misc.slice_def apply auto
  by (metis drop_take take_update_cancel)+

lemma slice_update_swap[simp]:
  ‹i < to ⟹ i ≥ from ⟹ i < length xs ⟹
     Misc.slice from to (xs[i := C]) = (Misc.slice from to xs)[(i - from) := C]›
  unfolding Misc.slice_def by (auto simp: drop_update_swap)

lemma drop_slice[simp]:
  ‹drop n (Misc.slice from to xs) = Misc.slice (from + n) to xs› for "from" n to xs
    by (auto simp: Misc.slice_def drop_take ac_simps)

lemma take_slice[simp]:
  ‹take n (Misc.slice from to xs) = Misc.slice from (min to (from + n)) xs› for "from" n to xs
  using antisym_conv by (fastforce simp: Misc.slice_def drop_take ac_simps min_def)

lemma slice_append[simp]:
  ‹to ≤ length xs ⟹ Misc.slice from to (xs @ ys) = Misc.slice from to xs›
  by (auto simp: Misc.slice_def)

lemma slice_prepend[simp]:
  ‹from ≥ length xs ⟹
     Misc.slice from to (xs @ ys) = Misc.slice (from - length xs) (to - length xs) ys›
  by (auto simp: Misc.slice_def)

lemma slice_len_min_If:
  ‹length (Misc.slice from to xs) =
     (if from < length xs then min (length xs - from) (to - from) else 0)›
  unfolding min_def by (auto simp: Misc.slice_def)

lemma slice_start0: ‹Misc.slice 0 to xs = take to xs›
  unfolding Misc.slice_def
  by auto

lemma slice_end_length: ‹n ≥ length xs ⟹ Misc.slice to n xs = drop to xs›
  unfolding Misc.slice_def
  by auto

lemma slice_swap[simp]:
   ‹l ≥ from ⟹ l < to ⟹ k ≥ from ⟹ k < to ⟹ from < length arena ⟹
     Misc.slice from to (swap arena l k) = swap (Misc.slice from to arena) (k - from) (l - from)›
  by (cases ‹k = l›) (auto simp: Misc.slice_def swap_def drop_update_swap list_update_swap)

lemma drop_swap_relevant[simp]:
  ‹i ≥ k ⟹ j ≥ k ⟹ j < length outl' ⟹drop k (swap outl' j i) = swap (drop k outl') (j - k) (i - k)›
  by (cases ‹j = i›)
    (auto simp: Misc.slice_def swap_def drop_update_swap list_update_swap)


lemma swap_swap: ‹k < length xs ⟹ l < length xs ⟹ swap xs k l = swap xs l k›
  by (cases ‹k = l›)
    (auto simp: Misc.slice_def swap_def drop_update_swap list_update_swap)

    (*
lemma in_mset_rel_eq_f_iff:
  ‹(a, b) ∈ ⟨{(c, a). a = f c}⟩mset_rel ⟷ b = f `# a›
  using ex_mset[of a]
  by (auto simp: mset_rel_def br_def rel2p_def[abs_def] p2rel_def rel_mset_def
      list_all2_op_eq_map_right_iff' cong: ex_cong)


lemma in_mset_rel_eq_f_iff_set:
  ‹⟨{(c, a). a = f c}⟩mset_rel = {(b, a). a = f `# b}›
  using in_mset_rel_eq_f_iff[of _ _ f] by blast*)

lemma list_rel_append_single_iff:
  ‹(xs @ [x], ys @ [y]) ∈ ⟨R⟩list_rel ⟷
    (xs, ys) ∈ ⟨R⟩list_rel ∧ (x, y) ∈ R›
  using list_all2_lengthD[of ‹(λx x'. (x, x') ∈ R)› ‹xs @ [x]› ‹ys @ [y]›]
  using list_all2_lengthD[of ‹(λx x'. (x, x') ∈ R)› ‹xs› ‹ys›]
  by (auto simp: list_rel_def list_all2_append)

lemma nth_in_sliceI:
  ‹i ≥ j ⟹ i < k ⟹ k ≤ length xs ⟹ xs ! i ∈ set (Misc.slice j k xs)›
  by (auto simp: Misc.slice_def in_set_take_conv_nth
    intro!: bex_lessI[of _ ‹i - j›])

lemma slice_Suc:
  ‹Misc.slice (Suc j) k xs = tl (Misc.slice j k xs)›
  apply (auto simp: Misc.slice_def in_set_take_conv_nth drop_Suc take_tl tl_drop
    drop_take)
  by (metis drop_Suc drop_take tl_drop)

lemma slice_0:
  ‹Misc.slice 0 b xs = take b xs›
  by (auto simp: Misc.slice_def)

lemma slice_end:
  ‹c = length xs ⟹ Misc.slice b c xs = drop b xs›
  by (auto simp: Misc.slice_def)

lemma slice_append_nth:
  ‹a ≤ b ⟹ Suc b ≤ length xs ⟹ Misc.slice a (Suc b) xs = Misc.slice a b xs @ [xs ! b]›
  by (auto simp: Misc.slice_def take_Suc_conv_app_nth
    Suc_diff_le)

lemma take_set: "set (take n l) = { l!i | i. i<n ∧ i<length l }"
  apply (auto simp add: set_conv_nth)
  apply (rule_tac x=i in exI)
  apply auto
  done

(* Shared Function *)

fun delete_index_and_swap where
  ‹delete_index_and_swap l i = butlast(l[i := last l])›

lemma (in -) delete_index_and_swap_alt_def:
  ‹delete_index_and_swap S i =
    (let x = last S in butlast (S[i := x]))›
  by auto

lemma swap_param[param]: "⟦ i<length l; j<length l; (l',l)∈⟨A⟩list_rel; (i',i)∈nat_rel; (j',j)∈nat_rel⟧
  ⟹ (swap l' i' j', swap l i j)∈⟨A⟩list_rel"
  unfolding swap_def
  by parametricity

lemma mset_tl_delete_index_and_swap:
  assumes
    ‹0 < i› and
    ‹i < length outl'›
  shows ‹mset (tl (delete_index_and_swap outl' i)) =
         remove1_mset (outl' ! i) (mset (tl outl'))›
  using assms
  by (subst mset_tl)+
    (auto simp: hd_butlast hd_list_update_If mset_butlast_remove1_mset
      mset_update last_list_update_to_last ac_simps)

definition length_ll :: ‹'a list list ⇒ nat ⇒ nat› where
  ‹length_ll l i = length (l!i)›

definition delete_index_and_swap_ll where
  ‹delete_index_and_swap_ll xs i j =
     xs[i:= delete_index_and_swap (xs!i) j]›


definition append_ll :: "'a list list ⇒ nat ⇒ 'a ⇒ 'a list list" where
  ‹append_ll xs i x = list_update xs i (xs ! i @ [x])›

definition (in -)length_uint32_nat where
  [simp]: ‹length_uint32_nat C = length C›

definition (in -)length_uint64_nat where
  [simp]: ‹length_uint64_nat C = length C›

definition nth_rll :: "'a list list ⇒ nat ⇒ nat ⇒ 'a" where
  ‹nth_rll l i j = l ! i ! j›

definition reorder_list :: ‹'b ⇒ 'a list ⇒ 'a list nres› where
‹reorder_list _ removed = SPEC (λremoved'. mset removed' = mset removed)›


definition mop_list_nth :: ‹'a list ⇒ nat ⇒ 'a nres› where
  ‹mop_list_nth xs i = do {
      ASSERT(i < length xs);
      RETURN (xs!i)
  }›

lemma mop_list_nth[refine]:
  ‹i < length ys ⟹ (xs, ys) ∈ ⟨R⟩list_rel ⟹ i = j ⟹ mop_list_nth xs i ≤ SPEC(λc. (c, ys!j) ∈ R)›
  by (auto simp: param_nth mop_list_nth_def list_rel_imp_same_length intro!: ASSERT_leI)

subsection ‹Some lemmas to move›
subsection ‹List relation›

lemma list_rel_take:
  ‹(ba, ab) ∈ ⟨A⟩list_rel ⟹ (take b ba, take b ab) ∈ ⟨A⟩list_rel›
  by (auto simp: list_rel_def)

lemma list_rel_update':
  fixes R
  assumes rel: ‹(xs, ys) ∈ ⟨R⟩list_rel› and
   h: ‹(bi, b) ∈ R›
  shows ‹(list_update xs ba bi, list_update ys ba b) ∈ ⟨R⟩list_rel›
proof -
  have [simp]: ‹(bi, b) ∈ R›
    using h by auto
  have ‹length xs = length ys›
    using assms list_rel_imp_same_length by blast

  then show ?thesis
    using rel
    by (induction xs ys arbitrary: ba rule: list_induct2) (auto split: nat.splits)
qed


lemma list_rel_in_find_correspondanceE:
  assumes ‹(M, M') ∈ ⟨R⟩list_rel› and ‹L ∈ set M›
  obtains L' where ‹(L, L') ∈ R› and ‹L' ∈ set M'›
  using assms[unfolded in_set_conv_decomp] by (auto simp: list_rel_append1
      elim!: list_relE3)


lemma slice_Suc_nth:
  ‹a < b ⟹ a < length xs ⟹ Suc a < b ⟹ Misc.slice a b xs = xs ! a # Misc.slice (Suc a) b xs›
  by (metis Cons_nth_drop_Suc Misc.slice_def Suc_diff_Suc take_Suc_Cons)

lemma distinct_sum_mset_sum:
  ‹distinct_mset As ⟹ (∑A ∈# As. (f :: 'a ⇒ nat) A) = (∑A ∈ set_mset As. f A)›
  by (subst sum_mset_sum_count)  (auto intro!: sum.cong simp: distinct_mset_def)

lemma distinct_sorted_append: ‹distinct (xs @ [x]) ⟹ sorted (xs @ [x]) ⟷ sorted xs ∧ (∀y ∈ set xs. y < x)›
  using not_distinct_conv_prefix sorted_append by fastforce

lemma (in linordered_ab_semigroup_add) Max_add_commute2:
  fixes k
  assumes "finite S" and "S ≠ {}"
  shows "Max ((λx. x + k) ` S) = Max S + k"
proof -
  have m: "⋀x y. max x y + k = max (x+k) (y+k)"
    by (simp add: max_def  local.dual_order.antisym add_right_mono)
  have "(λx. x + k) ` S = (λy. y + k) ` (S)" by auto
  have "Max … = Max ( S) + k"
    using assms hom_Max_commute [of "λy. y+k" "S", OF m, symmetric] by simp
  then show ?thesis by simp
qed

lemma list_rel_butlast:
  assumes rel: ‹(xs, ys) ∈ ⟨R⟩list_rel›
  shows ‹(butlast xs, butlast ys) ∈ ⟨R⟩list_rel›
proof -
  have ‹length xs = length ys›
    using assms list_rel_imp_same_length by blast
  then show ?thesis
    using rel
    by (induction xs ys rule: list_induct2) (auto split: nat.splits)
qed

end