Theory Swaps

(* 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"
by(simp add: swap_def)

lemma swap_id[simp]: "Suc n ≥ size xs ⟹ swap n xs = xs"
by(simp add: swap_def)

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

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)"
by(auto simp add: swap_def index_swap_if_distinct)

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)"
by(simp add: swap_def)

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"
by(simp add:before_in_def index_swap_distinct)
  (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
    by(simp add: Inv_def set_eq_iff)
      (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"
by(induction "is")(simp_all add: swap_def)

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"
by(simp add: before_in_def index_nth_id)

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
apply(simp add: Inv_swap before_swaps card_insert_if)
apply(simp add: Inv_def)
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