Theory Move_to_Front
section "Deterministic List Update"
theory Move_to_Front
imports
Swaps
On_Off
Competitive_Analysis
begin
declare Let_def[simp]
subsection "Function ‹mtf›"
definition mtf :: "'a ⇒ 'a list ⇒ 'a list" where
"mtf x xs =
(if x ∈ set xs then x # (take (index xs x) xs) @ drop (index xs x + 1) xs
else xs)"
lemma mtf_id[simp]: "x ∉ set xs ⟹ mtf x xs = xs"
by(simp add: mtf_def)
lemma mtf0[simp]: "x ∈ set xs ⟹ mtf x xs ! 0 = x"
by(auto simp: mtf_def)
lemma before_in_mtf: assumes "z ∈ set xs"
shows "x < y in mtf z xs ⟷
(y ≠ z ∧ (if x=z then y ∈ set xs else x < y in xs))"
proof-
have 0: "index xs z < size xs" by (metis assms index_less_size_conv)
let ?xs = "take (index xs z) xs @ xs ! index xs z # drop (Suc (index xs z)) xs"
have "x < y in mtf z xs = (y ≠ z ∧ (if x=z then y ∈ set ?xs else x < y in ?xs))"
using assms
by (auto simp add: mtf_def before_in_def index_append)
(metis index_take index_take_if_set le_add1 le_trans less_imp_le_nat)
with id_take_nth_drop[OF 0, symmetric] show ?thesis by(simp)
qed
lemma Inv_mtf: "set xs = set ys ⟹ z : set ys ⟹ Inv xs (mtf z ys) =
Inv xs ys ∪ {(x,z)|x. x < z in xs ∧ x < z in ys}
- {(z,x)|x. z < x in xs ∧ x < z in ys}"
by(auto simp add: Inv_def before_in_mtf not_before_in dest: before_in_setD1)
lemma set_mtf[simp]: "set(mtf x xs) = set xs"
by(simp add: mtf_def)
(metis append_take_drop_id Cons_nth_drop_Suc index_less le_refl Un_insert_right nth_index set_append set_simps(2))
lemma length_mtf[simp]: "size (mtf x xs) = size xs"
by (auto simp add: mtf_def min_def) (metis index_less_size_conv leD)
lemma distinct_mtf[simp]: "distinct (mtf x xs) = distinct xs"
by (metis length_mtf set_mtf card_distinct distinct_card)
subsection "Function ‹mtf2›"
definition mtf2 :: "nat ⇒ 'a ⇒ 'a list ⇒ 'a list" where
"mtf2 n x xs =
(if x : set xs then swaps [index xs x - n..<index xs x] xs else xs)"
lemma mtf_eq_mtf2: "mtf x xs = mtf2 (length xs - 1) x xs"
proof -
have "x : set xs ⟹ index xs x - (size xs - Suc 0) = 0"
by (auto simp: less_Suc_eq_le[symmetric])
thus ?thesis
by(auto simp: mtf_def mtf2_def swaps_eq_nth_take_drop)
qed
lemma mtf20[simp]: "mtf2 0 x xs = xs"
by(auto simp add: mtf2_def)
lemma length_mtf2[simp]: "length (mtf2 n x xs) = length xs"
by (auto simp: mtf2_def index_less_size_conv[symmetric]
simp del:index_conv_size_if_notin)
lemma set_mtf2[simp]: "set(mtf2 n x xs) = set xs"
by (auto simp: mtf2_def index_less_size_conv[symmetric]
simp del:index_conv_size_if_notin)
lemma distinct_mtf2[simp]: "distinct (mtf2 n x xs) = distinct xs"
by (metis length_mtf2 set_mtf2 card_distinct distinct_card)
lemma card_Inv_mtf2: "xs!j = ys!0 ⟹ j < length xs ⟹ dist_perm xs ys ⟹
card (Inv (swaps [i..<j] xs) ys) = card (Inv xs ys) - int(j-i)"
proof(induction j arbitrary: xs)
case (Suc j)
show ?case
proof cases
assume "i > j" thus ?thesis by simp
next
assume [arith]: "¬ i > j"
have 0: "Suc j < length ys" by (metis Suc.prems(2,3) distinct_card)
have 1: "(ys ! 0, xs ! j) : Inv ys xs"
proof (auto simp: Inv_def)
show "ys ! 0 < xs ! j in ys" using Suc.prems
by (metis Suc_lessD n_not_Suc_n not_before0 not_before_in nth_eq_iff_index_eq nth_mem)
show "xs ! j < ys ! 0 in xs" using Suc.prems
by (metis Suc_lessD before_id lessI)
qed
have 2: "card(Inv ys xs) ≠ 0" using 1 by auto
have "int(card (Inv (swaps [i..<Suc j] xs) ys)) =
card (Inv (swap j xs) ys) - int (j-i)" using Suc by simp
also have "… = card (Inv ys (swap j xs)) - int (j-i)"
by(simp add: card_Inv_sym)
also have "… = card (Inv ys xs - {(ys ! 0, xs ! j)}) - int (j - i)"
using Suc.prems 0 by(simp add: Inv_swap)
also have "… = int(card (Inv ys xs) - 1) - (j - i)"
using 1 by(simp add: card_Diff_singleton)
also have "… = card (Inv ys xs) - int (Suc j - i)" using 2 by arith
also have "… = card (Inv xs ys) - int (Suc j - i)" by(simp add: card_Inv_sym)
finally show ?thesis .
qed
qed simp
subsection "Function Lxy"
definition Lxy :: "'a list ⇒ 'a set ⇒ 'a list" where
"Lxy xs S = filter (λz. z∈S) xs"
thm inter_set_filter
lemma Lxy_length_cons: "length (Lxy xs S) ≤ length (Lxy (x#xs) S)"
unfolding Lxy_def by(simp)
lemma Lxy_empty[simp]: "Lxy [] S = []"
unfolding Lxy_def by simp
lemma Lxy_set_filter: "set (Lxy xs S) = S ∩ set xs"
by (simp add: Lxy_def inter_set_filter)
lemma Lxy_distinct: "distinct xs ⟹ distinct (Lxy xs S)"
by (simp add: Lxy_def)
lemma Lxy_append: "Lxy (xs@ys) S = Lxy xs S @ Lxy ys S"
by(simp add: Lxy_def)
lemma Lxy_snoc: "Lxy (xs@[x]) S = (if x∈S then Lxy xs S @ [x] else Lxy xs S)"
by(simp add: Lxy_def)
lemma Lxy_not: "S ∩ set xs = {} ⟹ Lxy xs S = []"
unfolding Lxy_def apply(induct xs) by simp_all
lemma Lxy_notin: "set xs ∩ S = {} ⟹ Lxy xs S = []"
apply(induct xs) by(simp_all add: Lxy_def)
lemma Lxy_in: "x∈S ⟹ Lxy [x] S = [x]"
by(simp add: Lxy_def)
lemma Lxy_project:
assumes "x≠y" "x ∈ set xs" "y∈set xs" "distinct xs"
and "x < y in xs"
shows "Lxy xs {x,y} = [x,y]"
proof -
from assms have ij: "index xs x < index xs y"
and xinxs: "index xs x < length xs"
and yinxs: "index xs y < length xs" unfolding before_in_def by auto
from xinxs obtain a as where dec1: "a @ [xs!index xs x] @ as = xs"
and "a = take (index xs x) xs" and "as = drop (Suc (index xs x)) xs"
and length_a: "length a = index xs x" and length_as: "length as = length xs - index xs x- 1"
using id_take_nth_drop by fastforce
have "index xs y≥length (a @ [xs!index xs x])" using length_a ij by auto
then have "((a @ [xs!index xs x]) @ as) ! index xs y = as ! (index xs y-length (a @ [xs ! index xs x]))" using nth_append[where xs="a @ [xs!index xs x]" and ys="as"]
by(simp)
then have xsj: "xs ! index xs y = as ! (index xs y-index xs x-1)" using dec1 length_a by auto
have las: "(index xs y-index xs x-1) < length as" using length_as yinxs ij by simp
obtain b c where dec2: "b @ [xs!index xs y] @ c = as"
and "b = take (index xs y-index xs x-1) as" "c=drop (Suc (index xs y-index xs x-1)) as"
and length_b: "length b = index xs y-index xs x-1" using id_take_nth_drop[OF las] xsj by force
have xs_dec: "a @ [xs!index xs x] @ b @ [xs!index xs y] @ c = xs" using dec1 dec2 by auto
from xs_dec assms(4) have "distinct ((a @ [xs!index xs x] @ b @ [xs!index xs y]) @ c)" by simp
then have c_empty: "set c ∩ {x,y} = {}"
and b_empty: "set b ∩ {x,y} = {}"and a_empty: "set a ∩ {x,y} = {}" by(auto simp add: assms(2,3))
have "Lxy (a @ [xs!index xs x] @ b @ [xs!index xs y] @ c) {x,y} = [x,y]"
apply(simp only: Lxy_append)
apply(simp add: assms(2,3))
using a_empty b_empty c_empty by(simp add: Lxy_notin Lxy_in)
with xs_dec show ?thesis by auto
qed
lemma Lxy_mono: "{x,y} ⊆ set xs ⟹ distinct xs ⟹ x < y in xs = x < y in Lxy xs {x,y}"
apply(cases "x=y")
apply(simp add: before_in_irefl)
proof -
assume xyset: "{x,y} ⊆ set xs"
assume dxs: "distinct xs"
assume xy: "x≠y"
{
fix x y
assume 1: "{x,y} ⊆ set xs"
assume xny: "x≠y"
assume 3: "x < y in xs"
have "Lxy xs {x,y} = [x,y]" apply(rule Lxy_project)
using xny 1 3 dxs by(auto)
then have "x < y in Lxy xs {x,y}" using xny by(simp add: before_in_def)
} note aha=this
have a: "x < y in xs ⟹ x < y in Lxy xs {x,y}"
apply(subst Lxy_project)
using xy xyset dxs by(simp_all add: before_in_def)
have t: "{x,y}={y,x}" by(auto)
have f: "~ x < y in xs ⟹ y < x in Lxy xs {x,y}"
unfolding t
apply(rule aha)
using xyset apply(simp)
using xy apply(simp)
using xy xyset by(simp add: not_before_in)
have b: "~ x < y in xs ⟹ ~ x < y in Lxy xs {x,y}"
proof -
assume "~ x < y in xs"
then have "y < x in Lxy xs {x,y}" using f by auto
then have "~ x < y in Lxy xs {x,y}" using xy by(simp add: not_before_in)
then show ?thesis .
qed
from a b
show ?thesis by metis
qed
subsection "List Update as Online/Offline Algorithm"
type_synonym 'a state = "'a list"
type_synonym answer = "nat * nat list"
definition step :: "'a state ⇒ 'a ⇒ answer ⇒ 'a state" where
"step s r a =
(let (k,sws) = a in mtf2 k r (swaps sws s))"
definition t :: "'a state ⇒ 'a ⇒ answer ⇒ nat" where
"t s r a = (let (mf,sws) = a in index (swaps sws s) r + 1 + size sws)"
definition static where "static s rs = (set rs ⊆ set s)"