Theory More_List

theory More_List
imports Main "HOL-Library.Multiset"
begin

subsection ‹Swap two elements of a list, by index›

(* Move to List *)

definition "swap l i j ≡ l[i := l!j, j:=l!i]"
lemma swap_nth: "⟦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_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)



(* Move to Multiset *)  

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)
  
  
  
  

end