Theory MTF2_Effects
section "Effect of mtf2"
theory MTF2_Effects
imports Move_to_Front
begin
lemma difind_difelem:
"i < length xs ⟹ distinct xs ⟹ xs ! j = a ⟹ j < length xs ⟹ i ≠ j
⟹ ~ a = xs ! i"
apply(rule ccontr) by(metis index_nth_id)
lemma fullchar: assumes "index xs q < length xs"
shows
"(i < length xs) =
(index xs q < i ∧ i < length xs
∨ index xs q = i
∨ index xs q - n ≤ i ∧ i < index xs q
∨ i < index xs q - n)"
using assms by auto
lemma mtf2_effect:
"q ∈ set xs ⟹ distinct xs ⟹ (index xs q < i ∧ i < length xs ⟶( index (mtf2 n q xs) (xs!i) = index xs (xs!i) ∧ index xs q < index (mtf2 n q xs) (xs!i) ∧ index (mtf2 n q xs) (xs!i) < length xs))
∧ (index xs q = i ⟶ (index (mtf2 n q xs) (xs!i) = index xs q - n ∧ index (mtf2 n q xs) (xs!i) = index xs q - n))
∧ (index xs q - n ≤ i ∧ i < index xs q ⟶ (index (mtf2 n q xs) (xs!i) = Suc (index xs (xs!i)) ∧ index xs q - n < index (mtf2 n q xs) (xs!i) ∧ index (mtf2 n q xs) (xs!i) ≤ index xs q))
∧ (i < index xs q - n ⟶ (index (mtf2 n q xs) (xs!i) = index xs (xs!i) ∧ index (mtf2 n q xs) (xs!i) < index xs q - n))"
unfolding mtf2_def
apply (induct n)
proof -
case (Suc n)
note indH=Suc(1)[OF Suc(2) Suc(3), simplified Suc(2) if_True]
note qinxs=Suc(2)[simp]
note distxs=Suc(3)[simp]
show ?case (is ?toshow)
apply(simp only: qinxs if_True)
proof (cases "index xs q ≥ Suc n")
case True
note True1=this
from True have onemore: "[index xs q - Suc n..<index xs q] = (index xs q - Suc n) # [index xs q - n..<index xs q]"
using Suc_diff_Suc upt_rec by auto
from onemore have yeah: "swaps [index xs q - Suc n..<index xs q] xs
= swap (index xs q - Suc n) (swaps [index xs q - n..<index xs q] xs)" by auto
have sis: "Suc (index xs q - Suc n) = index xs q - n" using True Suc_diff_Suc by auto
have indq: "index xs q < length xs"
apply(rule index_less) by auto
let ?i' = "index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i)"
let ?x = "(xs!i)" and ?xs="(swaps [index xs q - n..<index xs q] xs)"
and ?n="(index xs q - Suc n)"
have "?i'
= index (swap (index xs q - Suc n) (swaps [index xs q - n..<index xs q] xs)) (xs!i)" using yeah by auto
also have "… = (if ?x = ?xs ! ?n then Suc ?n else if ?x = ?xs ! Suc ?n then ?n else index ?xs ?x)"
apply(rule index_swap_distinct)
apply(simp)
apply(simp add: sis) using indq by linarith
finally have i': "?i' = (if ?x = ?xs ! ?n then Suc ?n else if ?x = ?xs ! Suc ?n then ?n else index ?xs ?x)" .
let ?i''="index (swaps [index xs q - n..<index xs q] xs) (xs ! i)"
show "(index xs q < i ∧ i < length xs ⟶
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs (xs ! i) ∧
index xs q < index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ∧
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) < length xs) ∧
(index xs q = i ⟶
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs q - Suc n ∧
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs q - Suc n) ∧
(index xs q - Suc n ≤ i ∧ i < index xs q ⟶
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = Suc (index xs (xs ! i)) ∧
index xs q - Suc n < index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ∧
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ≤ index xs q) ∧
(i < index xs q - Suc n ⟶
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs (xs ! i) ∧
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) < index xs q - Suc n)"
apply(intro conjI)
apply(intro impI) apply(elim conjE) prefer 4 apply(intro impI) prefer 4 apply(intro impI) apply(elim conjE)
prefer 4 apply(intro impI) prefer 4
proof (goal_cases)
case 1
have indH1: "(index xs q < i ∧ i < length xs ⟶
?i'' = index xs (xs ! i))" using indH by auto
assume ass: "index xs q < i" and ass2:"i < length xs"
then have a: "?i'' = index xs (xs ! i)" using indH1 by auto
also have a': "… = i" apply(rule index_nth_id) using ass2 by(auto)
finally have ii: "?i'' = i" .
have fstF: "~ ?x = ?xs ! ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
using indq apply (simp add: less_imp_diff_less)
apply(simp)
apply(rule nth_index) apply(simp) using ass2 apply(simp)
apply(rule index_less)
apply(simp) using ass2 apply(simp)
apply(simp)
using ii ass by auto
have sndF: "~ ?x = ?xs ! Suc ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
using indq True apply (simp add: Suc_diff_Suc less_imp_diff_less)
apply(simp)
apply(rule nth_index) apply(simp) using ass2 apply(simp)
apply(rule index_less)
apply(simp) using ass2 apply(simp)
apply(simp)
using ii ass Suc_diff_Suc True by auto
have "?i' = index xs (xs ! i)" unfolding i' using fstF sndF a by simp
then show ?case using a' ass ass2 by auto
next
case 2
have indH2: "index xs q = i ⟶ ?i'' = index xs (xs ! i) - n" using indH by auto
assume "index xs q = i"
then have ass: "i = index xs q" by auto
with indH2 have a: "i - n = ?i''" by auto
from ass have c: "index xs (xs ! i) = i" by auto
have "Suc (index xs q - Suc n) = i - n" using ass True Suc_diff_Suc by auto
also have "… = ?i''" using a by auto
finally have a: "Suc ?n = ?i''" .
have sndTrue: "?x = ?xs ! Suc ?n" apply(simp add: a)
apply(rule nth_index[symmetric]) by (simp add: ass)
have fstFalse: "~ ?x = ?xs ! ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
using indq True apply (simp add: Suc_diff_Suc less_imp_diff_less)
apply(simp)
apply(rule nth_index) apply(simp) using ass apply(simp)
apply(rule index_less)
apply(simp) using ass apply(simp)
apply(simp)
using a by auto
have "?i' = index xs (xs ! index xs q) - Suc n"
unfolding i' using sndTrue fstFalse by simp
with ass show ?case by auto
next
case 3
have indH3: "index xs q - n ≤ i ∧ i < index xs q
⟶ ?i'' = Suc (index xs (xs ! i))" using indH by auto
assume ass: "index xs q - Suc n ≤ i" and
ass2: "i < index xs q"
from ass2 have ilen: "i < length xs" using indq dual_order.strict_trans by blast
show ?case
proof (cases "index xs q - n ≤ i")
case False
then have "i < index xs q - n" by auto
moreover have "(i < index xs q - n ⟶ ?i'' = index xs (xs ! i))" using indH by auto
ultimately have d: "?i'' = index xs (xs ! i)" by simp
from False ass have b: "index xs q - Suc n = i" by auto
have "index xs q < length xs" apply(rule index_less) by (auto)
have c: "index xs (xs ! i) = i"
apply(rule index_nth_id) apply(simp) using indq ass2 using less_trans by blast
from b c d have f: "?i'' = index xs q - Suc n" by auto
have fstT: "?xs ! ?n = ?x"
apply(simp only: f[symmetric]) apply(rule nth_index)
by (simp add: ilen)
have "?i' = Suc (index xs q - Suc n)"
unfolding i' using fstT by simp
also have "… = Suc (index xs (xs ! i))" by(simp only: b c)
finally show ?thesis using c False ass by auto
next
case True
with ass2 indH3 have a: "?i'' = Suc (index xs (xs ! i))" by auto
have jo: "index xs (xs ! i) = i" apply(rule index_nth_id) using ilen by(auto)
have fstF: "~ ?x = ?xs ! ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
using indq apply (simp add: less_imp_diff_less)
apply(simp)
apply(rule nth_index) apply(simp) using ilen apply(simp)
apply(rule index_less)
apply(simp) using ilen apply(simp)
apply(simp)
apply(simp only: a jo) using True by auto
have sndF: "~ ?x = ?xs ! Suc ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
using True1 apply (simp add: Suc_diff_Suc less_imp_diff_less)
apply(simp)
apply(rule nth_index) apply(simp) using ilen apply(simp)
apply(rule index_less)
apply(simp) using ilen apply(simp)
apply(simp)
apply(simp only: a jo) using True1 apply (simp add: Suc_diff_Suc less_imp_diff_less)
using True by auto
have "?i' = Suc (index xs (xs ! i))" unfolding i' using fstF sndF a by simp
then show ?thesis using ass ass2 jo by auto
qed
next
case 4
assume ass: "i < index xs q - Suc n"
then have ass2: "i < index xs q - n" by auto
moreover have "(i < index xs q - n ⟶ ?i'' = index xs (xs ! i))" using indH by auto
ultimately have a: "?i'' = index xs (xs ! i)" by auto
from ass2 have "i < index xs q" by auto
then have ilen: "i < length xs" using indq dual_order.strict_trans by blast
have jo: "index xs (xs ! i) = i" apply(rule index_nth_id) using ilen by(auto)
have fstF: "~ ?x = ?xs ! ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
using indq apply (simp add: less_imp_diff_less)
apply(simp)
apply(rule nth_index) apply(simp) using ilen apply(simp)
apply(rule index_less)
apply(simp) using ilen apply(simp)
apply(simp)
apply(simp only: a jo) using ass by auto
have sndF: "~ ?x = ?xs ! Suc ?n" apply(rule difind_difelem[where j="index (swaps [index xs q - n..<index xs q] xs) (xs!i)"])
using True1 apply (simp add: Suc_diff_Suc less_imp_diff_less)
apply(simp)
apply(rule nth_index) apply(simp) using ilen apply(simp)
apply(rule index_less)
apply(simp) using ilen apply(simp)
apply(simp)
apply(simp only: a jo) using True1 apply (simp add: Suc_diff_Suc less_imp_diff_less)
using ass by auto
have "?i' = (index xs (xs ! i))" unfolding i' using fstF sndF a by simp
then show ?case using jo ass by auto
qed
next
case False
then have smalla: "index xs q - Suc n = index xs q - n" by auto
then have nomore: "swaps [index xs q - Suc n..<index xs q] xs
=swaps [index xs q - n..<index xs q] xs" by auto
show "(index xs q < i ∧ i < length xs ⟶
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs (xs ! i) ∧
index xs q < index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ∧
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) < length xs) ∧
(index xs q = i ⟶
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs q - Suc n ∧
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs q - Suc n) ∧
(index xs q - Suc n ≤ i ∧ i < index xs q ⟶
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = Suc (index xs (xs ! i)) ∧
index xs q - Suc n < index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ∧
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) ≤ index xs q) ∧
(i < index xs q - Suc n ⟶
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) = index xs (xs ! i) ∧
index (swaps [index xs q - Suc n..<index xs q] xs) (xs ! i) < index xs q - Suc n)"
unfolding nomore smalla by (rule indH)
qed
next
case 0
then show ?case apply(simp)
proof (safe, goal_cases)
case 1
have " index xs (xs ! i) = i" apply(rule index_nth_id) using 1 by auto
with 1 show ?case by auto
next
case 2
have "xs ! index xs q = q" using 2 by(auto)
with 2 show ?case by auto
next
case 3
have a: "index xs q < length xs" apply(rule index_less) using 3 by auto
have "index xs (xs ! i) = i" apply(rule index_nth_id) apply(fact 3(2)) using 3(3) a by auto
with 3 show ?case by auto
qed
qed
lemma mtf2_forward_effect1:
"q ∈ set xs ⟹ distinct xs ⟹ index xs q < i ∧ i < length xs
⟹ index (mtf2 n q xs) (xs ! i) = index xs (xs ! i) ∧ index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs" and
mtf2_forward_effect2: "q ∈ set xs ⟹ distinct xs ⟹ index xs q = i
⟹ index (mtf2 n q xs) (xs!i) = index xs q - n ∧ index xs q - n = index (mtf2 n q xs) (xs!i)" and
mtf2_forward_effect3: "q ∈ set xs ⟹ distinct xs ⟹ index xs q - n ≤ i ∧ i < index xs q
⟹ index (mtf2 n q xs) (xs!i) = Suc (index xs (xs!i)) ∧ index xs q - n < index (mtf2 n q xs) (xs!i) ∧ index (mtf2 n q xs) (xs!i) ≤ index xs q" and
mtf2_forward_effect4: "q ∈ set xs ⟹ distinct xs ⟹ i < index xs q - n
⟹ index (mtf2 n q xs) (xs!i) = index xs (xs!i) ∧ index (mtf2 n q xs) (xs!i) < index xs q - n"
apply(safe) using mtf2_effect by metis+
lemma yes[simp]: "index xs x < length xs
⟹ (xs!index xs x ) = x" apply(rule nth_index) by (simp add: index_less_size_conv)
lemma mtf2_forward_effect1':
"q ∈ set xs ⟹ distinct xs ⟹ index xs q < index xs x ∧ index xs x < length xs
⟹ index (mtf2 n q xs) x = index xs x ∧ index xs q < index (mtf2 n q xs) x ∧ index (mtf2 n q xs) x < length xs"
using mtf2_forward_effect1[where xs=xs and i="index xs x"] yes
by(auto)
lemma
mtf2_forward_effect2': "q ∈ set xs ⟹ distinct xs ⟹ index xs q = index xs x
⟹ index (mtf2 n q xs) (xs!index xs x) = index xs q - n ∧ index xs q - n = index (mtf2 n q xs) (xs!index xs x)"
using mtf2_forward_effect2[where xs=xs and i="index xs x"]
by fast
lemma
mtf2_forward_effect3': "q ∈ set xs ⟹ distinct xs ⟹ index xs q - n ≤ index xs x ⟹ index xs x < index xs q
⟹ index (mtf2 n q xs) (xs!index xs x) = Suc (index xs (xs!index xs x)) ∧ index xs q - n < index (mtf2 n q xs) (xs!index xs x) ∧ index (mtf2 n q xs) (xs!index xs x) ≤ index xs q"
using mtf2_forward_effect3[where xs=xs and i="index xs x"]
by fast
lemma
mtf2_forward_effect4': "q ∈ set xs ⟹ distinct xs ⟹ index xs x < index xs q - n
⟹ index (mtf2 n q xs) (xs!index xs x) = index xs (xs!index xs x) ∧ index (mtf2 n q xs) (xs!index xs x) < index xs q - n"
using mtf2_forward_effect4[where xs=xs and i="index xs x"]
by fast
lemma splitit: " (index xs q < i ∧ i < length xs ⟹ P)
⟹ (index xs q = i ⟹ P)
⟹ (index xs q - n ≤ i ∧ i < index xs q ⟹ P)
⟹ (i < index xs q - n ⟹ P)
⟹ (i < length xs ⟹ P)"
by force
lemma mtf2_forward_beforeq: "q ∈ set xs ⟹ distinct xs ⟹ i < index xs q
⟹ index (mtf2 n q xs) (xs!i) ≤ index xs q"
apply (cases "i < index xs q - n")
using mtf2_forward_effect4 apply force
using mtf2_forward_effect3 using leI by metis
lemma x_stays_before_y_if_y_not_moved_to_front:
assumes "q ∈ set xs" "distinct xs" "x ∈ set xs" "y ∈ set xs" "y ≠ q"
and "x < y in xs"
shows "x < y in (mtf2 n q xs)"
proof -
from assms(3) obtain i where i: "i = index xs x" and i2: "i < length xs" by auto
from assms(4) obtain j where j: "j = index xs y" and j2: "j < length xs" by auto
have "x < y in xs ⟹ x < y in (mtf2 n q xs)"
apply(cases i xs rule: splitit[where q=q and n=n])
apply(simp add: i assms(1,2) mtf2_forward_effect1' before_in_def)
apply(cases j xs rule: splitit[where q=q and n=n])
apply (metis before_in_def assms(1-3) i j less_imp_diff_less mtf2_effect nth_index set_mtf2)
apply(simp add: i j assms mtf2_forward_effect1' mtf2_forward_effect2' before_in_def)
apply(simp add: i j assms mtf2_forward_effect1' mtf2_forward_effect2' before_in_def)
apply(simp add: i j assms mtf2_forward_effect1' mtf2_forward_effect3' before_in_def)
apply(rule j2)
apply(cases j xs rule: splitit[where q=q and n=n])
apply (smt before_in_def assms(1-3) i j le_less_trans mtf2_forward_effect1 mtf2_forward_effect3 nth_index set_mtf2)
using assms(4,5) j apply simp
apply (smt Suc_leI before_in_def assms(1-3) i j le_less_trans lessI mtf2_forward_effect3 nth_index set_mtf2)
apply (simp add: before_in_def i j)
apply(rule j2)
apply(cases j xs rule: splitit[where q=q and n=n])
apply (smt before_in_def assms(1-3) i j le_less_trans mtf2_forward_effect1 mtf2_forward_effect4 nth_index set_mtf2)
using assms(4-5) j apply simp
apply (smt before_in_def assms(1-3) i j le_less_trans less_imp_le_nat mtf2_forward_effect3 mtf2_forward_effect4 nth_index set_mtf2)
apply (metis before_in_def assms(1-3) i j mtf2_forward_effect4 nth_index set_mtf2)
apply(rule j2)
apply(rule i2) done
with assms(6) show ?thesis by auto
qed
corollary swapped_by_mtf2: "q ∈ set xs ⟹ distinct xs ⟹ x ∈ set xs ⟹ y ∈ set xs ⟹
x < y in xs ⟹ y < x in (mtf2 n q xs) ⟹ y = q"
apply(rule ccontr) using x_stays_before_y_if_y_not_moved_to_front not_before_in by (metis before_in_setD1)
lemma x_stays_before_y_if_y_not_moved_to_front_2dir: "q ∈ set xs ⟹ distinct xs ⟹ x ∈ set xs ⟹ y ∈ set xs ⟹ y ≠ q ⟹
x < y in xs = x < y in (mtf2 n q xs)"
oops
lemma mtf2_backwards_effect1:
assumes "index xs q < length xs" "q ∈ set xs" "distinct xs"
"index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs"
"i < length xs"
shows "index xs q < i ∧ i < length xs"
proof -
from assms(4) have "~ (index xs q - n = index (mtf2 n q xs) (xs ! i))" by auto
with assms mtf2_forward_effect2 have 1: "~ (index xs q = i)" by metis
from assms(4) have "~ (index xs q - n < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) ≤ index xs q)" by auto
with assms mtf2_forward_effect3 have 2: "~ (index xs q - n ≤ i ∧ i < index xs q)" by metis
from assms(4) have "~ (index (mtf2 n q xs) (xs ! i) < index xs q - n)" by auto
with assms mtf2_forward_effect4 have 3: "~ (i < index xs q - n)" by metis
from fullchar[OF assms(1)] assms(5) 1 2 3 show "index xs q < i ∧ i < length xs" by metis
qed
lemma mtf2_backwards_effect2:
assumes "index xs q < length xs" "q ∈ set xs" "distinct xs" "index (mtf2 n q xs) (xs ! i) = index xs q - n"
"i < length xs"
shows "index xs q = i"
proof -
from assms(4) have "~ (index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs)" by auto
with assms mtf2_forward_effect1 have 1: "~ (index xs q < i ∧ i < length xs)" by metis
from assms(4) have "~ (index xs q - n < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) ≤ index xs q)" by auto
with assms mtf2_forward_effect3 have 2: "~ (index xs q - n ≤ i ∧ i < index xs q)" by metis
from assms(4) have "~ (index (mtf2 n q xs) (xs ! i) < index xs q - n)" by auto
with assms mtf2_forward_effect4 have 3: "~ (i < index xs q - n)" by metis
from fullchar[OF assms(1)] assms(5) 1 2 3 show "index xs q = i" by metis
qed
lemma mtf2_backwards_effect3:
assumes "index xs q < length xs" "q ∈ set xs" "distinct xs"
"index xs q - n < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) ≤ index xs q"
"i < length xs"
shows "index xs q - n ≤ i ∧ i < index xs q"
proof -
from assms(4) have "~ (index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs)" by auto
with assms mtf2_forward_effect1 have 2: "~ (index xs q < i ∧ i < length xs)" by metis
from assms(4) have "~ (index xs q - n = index (mtf2 n q xs) (xs ! i))" by auto
with assms mtf2_forward_effect2 have 1: "~ (index xs q = i)" by metis
from assms(4) have "~ (index (mtf2 n q xs) (xs ! i) < index xs q - n)" by auto
with assms mtf2_forward_effect4 have 3: "~ (i < index xs q - n)" by metis
from fullchar[OF assms(1)] assms(5) 1 2 3 show "index xs q - n ≤ i ∧ i < index xs q" by metis
qed
lemma mtf2_backwards_effect4:
assumes "index xs q < length xs" "q ∈ set xs" "distinct xs"
"index (mtf2 n q xs) (xs ! i) < index xs q - n"
"i < length xs"
shows "i < index xs q - n"
proof -
from assms(4) have "~ (index xs q < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) < length xs)" by auto
with assms mtf2_forward_effect1 have 2: "~ (index xs q < i ∧ i < length xs)" by metis
from assms(4) have "~ (index xs q - n = index (mtf2 n q xs) (xs ! i))" by auto
with assms mtf2_forward_effect2 have 1: "~ (index xs q = i)" by metis
from assms(4) have "~ (index xs q - n < index (mtf2 n q xs) (xs ! i) ∧ index (mtf2 n q xs) (xs ! i) ≤ index xs q)" by auto
with assms mtf2_forward_effect3 have 3: "~ (index xs q - n ≤ i ∧ i < index xs q)" by metis
from fullchar[OF assms(1)] assms(5) 1 2 3 show "i < index xs q - n" by metis
qed
lemma mtf2_backwards_effect4':
assumes "index xs q < length xs" "q ∈ set xs" "distinct xs"
"index (mtf2 n q xs) x < index xs q - n"
"x ∈ set xs"
shows "(index xs x) < index xs q - n"
using assms mtf2_backwards_effect4[where xs=xs and i="index xs x"] yes
by auto
lemma
assumes distA: "distinct A" and
asm: "q ∈ set A"
shows
mtf2_mono: "q< x in A ⟹ q < x in (mtf2 n q A)" and
mtf2_q_after: "index (mtf2 n q A) q = index A q - n"
proof -
have lele: "(q < x in A ⟶ q < x in swaps [index A q - n..<index A q] A) ∧ (index (swaps [index A q - n..<index A q] A) q = index A q - n)"
apply(induct n) apply(simp)
proof -
fix n
assume ind: "(q < x in A ⟶ q < x in swaps [index A q - n..<index A q] A)
∧ index (swaps [index A q - n..<index A q] A) q = index A q - n"
then have iH: " q < x in A ⟹ q < x in swaps [index A q - n..<index A q] A" by auto
from ind have indH2: "index (swaps [index A q - n..<index A q] A) q = index A q - n" by auto
show "(q < x in A ⟶ q < x in swaps [index A q - Suc n..<index A q] A) ∧
index (swaps [index A q - Suc n..<index A q] A) q = index A q - Suc n" (is "?part1 ∧ ?part2")
proof (cases "index A q ≥ Suc n")
case True
then have onemore: "[index A q - Suc n..<index A q] = (index A q - Suc n) # [index A q - n..<index A q]"
using Suc_diff_Suc upt_rec by auto
from onemore have yeah: "swaps [index A q - Suc n..<index A q] A
= swap (index A q - Suc n) (swaps [index A q - n..<index A q] A)" by auto
from indH2 have gr: "index (swaps [index A q - n..<index A q] A) q = Suc(index A q - Suc n)" using Suc_diff_Suc True by auto
have whereisq: "swaps [index A q - n..<index A q] A ! Suc (index A q - Suc n) = q"
unfolding gr[symmetric] apply(rule nth_index) using asm by auto
have indSi: "index A q < length A" using asm index_less by auto
have 3: "Suc (index A q - Suc n) < length (swaps [index A q - n..<index A q] A)" using True
apply(auto simp: Suc_diff_Suc asm) using indSi by auto
have 1: "q ≠ swaps [index A q - n..<index A q] A ! (index A q - Suc n)"
proof
assume as: "q = swaps [index A q - n..<index A q] A ! (index A q - Suc n)"
{
fix xs x
have "Suc x < length xs ⟹ xs ! x = q ⟹ xs ! Suc x = q ⟹ ¬ distinct xs"
by (metis Suc_lessD index_nth_id n_not_Suc_n)
} note cool=this
have "¬ distinct (swaps [index A q - n..<index A q] A)"
apply(rule cool[of "(index A q - Suc n)"])
apply(simp only: 3)
apply(simp only: as[symmetric])
by(simp only: whereisq)
then show "False" using distA by auto
qed
have part1: ?part1
proof
assume qx: "q < x in A"
{
fix q x B i
assume a1: "q < x in B"
assume a2: "~ q = B ! i"
assume a3: "distinct B"
assume a4: "Suc i < length B"
have "dist_perm B B" by(simp add: a3)
moreover have "Suc i < length B" using a4 by auto
moreover have "q < x in B ∧ ¬ (q = B ! i ∧ x = B ! Suc i)" using a1 a2 by auto
ultimately have "q < x in swap i B"
using before_in_swap[of B B] by simp
} note grr=this
have 2: "distinct (swaps [index A q - n..<index A q] A)" using distA by auto
show "q < x in swaps [index A q - Suc n..<index A q] A"
apply(simp only: yeah)
apply(rule grr[OF iH[OF qx]]) using 1 2 3 by auto
qed
let ?xs = "(swaps [index A q - n..<index A q] A)"
let ?n = "(index A q - Suc n)"
have "?xs ! Suc ?n = swaps [index A q - n..<index A q] A ! (index (swaps [index A q - n..<index A q] A) q)"
using indH2 Suc_diff_Suc True by auto
also have "… = q" apply(rule nth_index) using asm by auto
finally have sndTrue: "?xs ! Suc ?n = q" .
have fstFalse: "~ q = ?xs ! ?n" by (fact 1)
have "index (swaps [index A q - Suc n..<index A q] A) q
= index (swap (index A q - Suc n) ?xs) q" by (simp only: yeah)
also have "… = (if q = ?xs ! ?n then Suc ?n else if q = ?xs ! Suc ?n then ?n else index ?xs q)"
apply(rule index_swap_distinct)
apply(simp add: distA)
by (fact 3)
also have "… = ?n" using fstFalse sndTrue by auto
finally have part2: ?part2 .
from part1 part2 show "?part1 ∧ ?part2" by simp
next
case False
then have a: "index A q - Suc n = index A q - n" by auto
then have b: "[index A q - Suc n..<index A q] = [index A q - n..<index A q]" by auto
show ?thesis apply(simp only: b a) by (fact ind)
qed
qed
show "q < x in A ⟹ q < x in (mtf2 n q A)"
"(index (mtf2 n q A) q) = index A q - n"
unfolding mtf2_def
using asm lele apply(simp)
using asm lele by(simp)
qed
subsection "effect of mtf2 on index"
lemma swapsthrough: "distinct xs ⟹ q ∈ set xs ⟹ index ( swaps [index xs q - entf..<index xs q] xs ) q = index xs q - entf"
proof (induct entf)
case (Suc e)
note iH=this
show ?case
proof (cases "index xs q - e")
case 0
then have "[index xs q - Suc e..<index xs q]
= [index xs q - e..<index xs q]" by force
then have "index (swaps [index xs q - Suc e..<index xs q] xs) q
= index xs q - e" using Suc by auto
also have "… = index xs q - (Suc e)" using 0 by auto
finally show "index (swaps [index xs q - Suc e..<index xs q] xs) q = index xs q - Suc e" .
next
case (Suc f)
have gaa: "Suc (index xs q - Suc e) = index xs q - e" using Suc by auto
from Suc have "index xs q - e ≤ index xs q" by auto
also have "… < length xs" by(simp add: index_less_size_conv iH)
finally have indle: "index xs q - e < length xs".
have arg: "Suc (index xs q - Suc e) < length (swaps [index xs q - e..<index xs q] xs)"
apply(auto) unfolding gaa using indle by simp
then have arg2: "index xs q - Suc e < length (swaps [index xs q - e..<index xs q] xs)" by auto
from Suc have nexter: "index xs q - e = Suc (index xs q - (Suc e))" by auto
then have aaa: "[index xs q - Suc e..<index xs q]
= (index xs q - Suc e)#[index xs q - e..<index xs q]" using upt_rec by auto
let ?i="index xs q - Suc e"
let ?rest="swaps [index xs q - e..<index xs q] xs"
from iH nexter have indj: "index ?rest q = Suc ?i" by auto
from iH(2) have "distinct ?rest" by auto
have "?rest ! (index ?rest q) = q" apply(rule nth_index) by(simp add: iH)
with indj have whichcase: "q = ?rest ! Suc ?i" by auto
with ‹distinct ?rest› have whichcase2: "~ q = ?rest ! ?i"
by (metis Suc_lessD arg index_nth_id n_not_Suc_n)
from aaa have "index (swaps [index xs q - Suc e..<index xs q] xs) q
= index (swap (index xs q - Suc e) (swaps [index xs q - e..<index xs q] xs)) q"
by auto
also have "… = (if q = ?rest ! ?i then (Suc ?i) else if q = ?rest ! (Suc ?i) then ?i else index ?rest q)"
apply(simp only: swap_def arg if_True)
apply(rule index_swap_if_distinct)
apply(simp add: iH)
apply(simp only: arg2)
by(simp only: arg)
also have "… = ?i" using whichcase whichcase2 by simp
finally show "index (swaps [index xs q - Suc e..<index xs q] xs) q =
index xs q - Suc e" .
qed
next
case 0
show ?case by simp
qed
term "mtf2"
lemma mtf2_moves_to_front: "distinct xs ⟹ q ∈ set xs ⟹ index (mtf2 (length xs) q xs) q = 0"
unfolding mtf2_def
proof -
assume distxs: "distinct xs"
assume qinxs: "q ∈ set xs"
have " index (if q ∈ set xs then swaps [index xs q - length xs..<index xs q] xs else xs) q
= index ( swaps [index xs q - length xs..<index xs q] xs) q" using qinxs by auto
also have "… = index xs q - (length xs)" apply(rule swapsthrough) using distxs qinxs by auto
also have "… = 0" using index_less_size_conv qinxs by (simp add: index_le_size)
finally show "index (if q ∈ set xs then swaps [index xs q - length xs..<index xs q] xs else xs) q = 0" .
qed
lemma xy_relativorder_mtf2:
assumes
"q≠x" "q≠y" "distinct xs" "x∈set xs" "y∈set xs" "q∈set xs"
shows "x < y in mtf2 n q xs
= x < y in xs"
using assms
by (metis before_in_setD2 not_before_in x_stays_before_y_if_y_not_moved_to_front)
lemma mtf2_moves_to_frontm1: "distinct xs ⟹ q ∈ set xs ⟹ index (mtf2 (length xs -1) q xs) q = 0"
unfolding mtf2_def
proof -
assume distxs: "distinct xs"
assume qinxs: "q ∈ set xs"
have " index (if q ∈ set xs then swaps [index xs q - (length xs -1)..<index xs q] xs else xs) q
= index ( swaps [index xs q - (length xs -1)..<index xs q] xs) q" using qinxs by auto
also have "… = index xs q - (length xs -1)" apply(rule swapsthrough) using distxs qinxs by auto
also have "… = 0" using index_less_size_conv qinxs
by (metis Suc_pred' gr0I length_pos_if_in_set less_irrefl less_trans_Suc zero_less_diff)
finally show "index (if q ∈ set xs then swaps [index xs q - (length xs -1)..<index xs q] xs else xs) q = 0" .
qed
lemma mtf2_moves_to_front': "distinct xs ⟹ y ∈ set xs ⟹ x ∈ set xs ⟹ x≠y ⟹ x < y in mtf2 (length xs-1) x xs = True"
using mtf2_moves_to_frontm1 by (metis before_in_def gr0I index_eq_index_conv set_mtf2)
lemma mtf2_moves_to_front'': "distinct xs ⟹ y ∈ set xs ⟹ x ∈ set xs ⟹ x≠y ⟹ x < y in mtf2 (length xs) x xs = True"
using mtf2_moves_to_front by (metis before_in_def gr0I index_eq_index_conv set_mtf2)
end