(* 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