# Theory Swaps

theory Swaps
imports Inversion
```(* Author: Tobias Nipkow *)

section "Swapping Adjacent Elements in a List"

theory Swaps
imports Inversion
begin

text‹Swap elements at index ‹n› and @{term "Suc n"}:›

definition "swap n xs =
(if Suc n < size xs then xs[n := xs!Suc n, Suc n := xs!n] else xs)"

lemma length_swap[simp]: "length(swap i xs) = length xs"

lemma swap_id[simp]: "Suc n ≥ size xs ⟹ swap n xs = xs"

lemma distinct_swap[simp]:
"distinct(swap i xs) = distinct xs"

lemma swap_Suc[simp]: "swap (Suc n) (a # xs) = a # swap n xs"
by(induction xs) (auto simp: swap_def)

lemma index_swap_distinct:
"distinct xs ⟹ Suc n < length xs ⟹
index (swap n xs) x =
(if x = xs!n then Suc n else if x = xs!Suc n then n else index xs x)"

lemma set_swap[simp]: "set(swap n xs) = set xs"
by(auto simp add: swap_def set_conv_nth nth_list_update) metis

lemma nth_swap_id[simp]: "Suc i < length xs ⟹ swap i xs ! i = xs!(i+1)"

lemma before_in_swap:
"dist_perm xs ys ⟹ Suc n < size xs ⟹
x < y in (swap n xs) ⟷
x < y in xs ∧ ¬ (x = xs!n ∧ y = xs!Suc n) ∨ x = xs!Suc n ∧ y = xs!n"
(metis Suc_lessD Suc_lessI index_less_size_conv index_nth_id less_Suc_eq n_not_Suc_n nth_index)

lemma Inv_swap: assumes "dist_perm xs ys"
shows "Inv xs (swap n ys) =
(if Suc n < size xs
then if ys!n < ys!Suc n in xs
then Inv xs ys ∪ {(ys!n, ys!Suc n)}
else Inv xs ys - {(ys!Suc n, ys!n)}
else Inv xs ys)"
proof-
have "length xs = length ys" using assms by (metis distinct_card)
with assms show ?thesis
(metis before_in_def not_before_in before_in_swap)
qed

text‹Perform a list of swaps, from right to left:›

abbreviation swaps where "swaps == foldr swap"

lemma swaps_inv[simp]:
"set (swaps sws xs) = set xs ∧
size(swaps sws xs) = size xs ∧
distinct(swaps sws xs) = distinct xs"
by (induct sws arbitrary: xs) (simp_all add: swap_def)

lemma swaps_eq_Nil_iff[simp]: "swaps acts xs = [] ⟷ xs = []"
by(induction acts)(auto simp: swap_def)

lemma swaps_map_Suc[simp]:
"swaps (map Suc sws) (a # xs) = a # swaps sws xs"
by(induction sws arbitrary: xs) auto

lemma card_Inv_swaps_le:
"distinct xs ⟹ card (Inv xs (swaps sws xs)) ≤ length sws"
by(induction sws) (auto simp: Inv_swap card_insert_if card_Diff_singleton_if)

lemma nth_swaps: "∀i∈set is. j < i ⟹ swaps is xs ! j = xs ! j"

lemma not_before0[simp]: "~ x < xs ! 0 in xs"
apply(cases "xs = []")
by(auto simp: before_in_def neq_Nil_conv)

lemma before_id[simp]: "⟦ distinct xs; i < size xs; j < size xs ⟧ ⟹
xs ! i < xs ! j in xs ⟷ i < j"

lemma before_swaps:
"⟦ distinct is; ∀i∈set is. Suc i < size xs; distinct xs; i ∉ set is; i < j; j < size xs ⟧ ⟹
swaps is xs ! i < swaps is xs ! j in xs"
apply(induction "is" arbitrary: i j)
apply simp
apply(auto simp: swap_def nth_list_update)
done

lemma card_Inv_swaps:
"⟦ distinct is; ∀i∈set is. Suc i < size xs; distinct xs ⟧ ⟹
card(Inv xs (swaps is xs)) = length is"
apply(induction "is")
apply simp
done

lemma swaps_eq_nth_take_drop: "i < length xs ⟹
swaps [0..<i] xs = xs!i # take i xs @ drop (Suc i) xs"
apply(induction i arbitrary: xs)
apply (auto simp add: neq_Nil_conv swap_def drop_update_swap
take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric])
done

lemma index_swaps_size: "distinct s ⟹
index s q ≤ index (swaps sws s) q + length sws"
apply(induction sws arbitrary: s)
apply simp
apply (fastforce simp: swap_def index_swap_if_distinct index_nth_id)
done

lemma index_swaps_last_size: "distinct s ⟹
size s ≤ index (swaps sws s) (last s) + length sws + 1"
apply(cases "s = []")
apply simp
using index_swaps_size[of s "last s" sws] by simp

end
```