Theory BIT
section "BIT: an Online Algorithm for the List Update Problem"
theory BIT
imports
Bit_Strings
MTF2_Effects
begin
abbreviation "config'' A qs init n == config_rand A init (take n qs)"
lemma sum_my: fixes f g::"'b ⇒ 'a::ab_group_add"
assumes "finite A" "finite B"
shows "(∑x∈A. f x) - (∑x∈B. g x)
= (∑x∈(A ∩ B). f x - g x) + (∑x∈A-B. f x) - (∑x∈B-A. g x)"
proof -
have "finite (A-B)" and "finite (A∩B)" and "finite (B-A)" and "finite (B∩A)" using assms by auto
note finites=this
have "(A-B) ∩ ( (A∩B) ) = {}" and "(B-A) ∩ ( (B∩A) ) = {}" by auto
note inters=this
have commute: "A∩B=B∩A" by auto
have "A = (A-B) ∪ (A∩B)" and "B = (B-A) ∪ ( (B∩A))" by auto
then have "(∑x∈A. f x) - (∑x∈B. g x) = (∑x∈(A-B) ∪ (A∩B). f x) - (∑x∈(B-A) ∪ (B∩A). g x)" by auto
also have "… = ( (∑x∈(A-B). f x) + (∑x∈(A∩B). f x) - (∑x∈(A-B)∩(A∩B). f x) )
-( (∑x∈(B-A). g x) + (∑x∈(B∩A). g x) - (∑x∈(B-A)∩(B∩A). g x))"
using sum_Un[where ?f="f",OF finites(1) finites(2)]
sum_Un[where ?f="g",OF finites(3) finites(4)] by(simp)
also have "… = ( (∑x∈(A-B). f x) + (∑x∈(A∩B). f x) )
- (∑x∈(B-A). g x) - (∑x∈(B∩A). g x) " using inters by auto
also have "… = (∑x∈(A-B). f x) - (∑x∈(A∩B). g x) + (∑x∈(A∩B). f x)
- (∑x∈(B-A). g x) " using commute by auto
also have "… = (∑x∈(A∩B). f x - g x) +(∑x∈(A-B). f x)
- (∑x∈(B-A). g x)" using sum_subtractf[of f g "(A∩B)"] by auto
finally show ?thesis .
qed
lemma sum_my2: "(∀x∈A. f x = g x) ⟹ (∑x∈A. f x) = (∑x∈A. g x)" by auto
subsection "Definition of BIT"
definition BIT_init :: "('a state,bool list * 'a list)alg_on_init" where
"BIT_init init = map_pmf (λl. (l,init)) (bv (length init))"
lemma "~ deterministic_init BIT_init"
unfolding deterministic_init_def BIT_init_def apply(auto)
apply(intro exI[where x="[a]"])
by(auto simp: UNIV_bool set_pmf_bernoulli)
definition BIT_step :: "('a state, bool list * 'a list, 'a, answer)alg_on_step" where
"BIT_step s q = ( let a=((if (fst (snd s))!(index (snd (snd s)) q) then 0 else (length (fst s))),[]) in
return_pmf (a , (flip (index (snd (snd s)) q) (fst (snd s)), snd (snd s))))"
lemma "deterministic_step BIT_step"
unfolding deterministic_step_def BIT_step_def
by simp
abbreviation BIT :: "('a state, bool list*'a list, 'a, answer)alg_on_rand" where
"BIT == (BIT_init, BIT_step)"
subsection "Properties of BIT's state distribution"
lemma BIT_no_paid: "∀((free,paid),_) ∈ (BIT_step s q). paid=[]"
unfolding BIT_step_def
by(auto)
subsubsection "About the Internal State"
term "(config'_rand (BIT_init, BIT_step) s0 qs) "
lemma config'_n_init: fixes qs init n
shows "map_pmf (snd ∘ snd) (config'_rand (BIT_init, BIT_step) init qs) = map_pmf (snd ∘ snd) init"
apply (induct qs arbitrary: init)
by (simp_all add: map_pmf_def bind_assoc_pmf BIT_step_def bind_return_pmf )
lemma config_n_init: "map_pmf (snd ∘ snd) (config_rand (BIT_init, BIT_step) s0 qs) = return_pmf s0"
using config'_n_init[of "((fst (BIT_init, BIT_step) s0) ⤜ (λis. return_pmf (s0, is)))"]
by (simp_all add: map_pmf_def bind_assoc_pmf bind_return_pmf BIT_init_def )
lemma config_n_init2: "∀(_,(_,x)) ∈ set_pmf (config_rand (BIT_init, BIT_step) init qs). x = init"
proof (rule, goal_cases)
case (1 z)
then have 1: "snd(snd z) ∈ (snd ∘ snd) ` set_pmf (config_rand (BIT_init, BIT_step) init qs)"
by force
have "(snd ∘ snd) ` set_pmf (config_rand (BIT_init, BIT_step) init qs)
= set_pmf (map_pmf (snd ∘ snd) (config_rand (BIT_init, BIT_step) init qs))" by(simp)
also have "… = {init}" apply(simp only: config_n_init) by simp
finally have "snd(snd z) = init" using 1 by auto
then show ?case by auto
qed
lemma config_n_init3: "∀x ∈ set_pmf (config_rand (BIT_init, BIT_step) init qs). snd (snd x) = init"
using config_n_init2 by(simp add: split_def)
lemma config'_n_bv: fixes qs init n
shows " map_pmf (snd ∘ snd) init = return_pmf s0
⟹ map_pmf (fst ∘ snd) init = bv (length s0)
⟹ map_pmf (snd ∘ snd) (config'_rand (BIT_init, BIT_step) init qs) = return_pmf s0
∧ map_pmf (fst ∘ snd) (config'_rand (BIT_init, BIT_step) init qs) = bv (length s0)"
proof (induct qs arbitrary: init)
case (Cons r rs)
from Cons(2) have a: "map_pmf (snd ∘ snd) (init ⤜ (λs. snd (BIT_init, BIT_step) s r ⤜
(λ(a, is'). return_pmf (step (fst s) r a, is'))))
= return_pmf s0" apply(simp add: BIT_step_def)
by (simp_all add: map_pmf_def bind_assoc_pmf BIT_step_def bind_return_pmf )
then have b: "∀z∈set_pmf (init ⤜ (λs. snd (BIT_init, BIT_step) s r ⤜
(λ(a, is'). return_pmf (step (fst s) r a, is')))). snd (snd z) = s0"
by (metis (mono_tags, lifting) comp_eq_dest_lhs map_pmf_eq_return_pmf_iff)
show ?case
apply(simp only: config'_rand.simps)
proof (rule Cons(1), goal_cases)
case 2
have "map_pmf (fst ∘ snd)
(init ⤜
(λs. snd (BIT_init, BIT_step) s r ⤜
(λ(a, is').
return_pmf (step (fst s) r a, is')))) = map_pmf (flip (index s0 r)) (bv (length s0))"
using b
apply(simp add: BIT_step_def Cons(3)[symmetric] bind_return_pmf map_pmf_def bind_assoc_pmf )
apply(rule bind_pmf_cong)
apply(simp)
by(simp add: inv_flip_bv)
also have "… = bv (length s0)" using inv_flip_bv by auto
finally show ?case .
qed (fact)
qed simp
lemma config_n_bv_2: "map_pmf (snd ∘ snd) (config_rand (BIT_init, BIT_step) s0 qs) = return_pmf s0
∧ map_pmf (fst ∘ snd) (config_rand (BIT_init, BIT_step) s0 qs) = bv (length s0)"
apply(rule config'_n_bv)
by(simp_all add: bind_return_pmf map_pmf_def bind_assoc_pmf bind_return_pmf' BIT_init_def)
lemma config_n_bv: "map_pmf (fst ∘ snd) (config_rand (BIT_init, BIT_step) s0 qs) = bv (length s0)"
using config_n_bv_2 by auto
lemma config_n_fst_init_length: "∀(_,(x,_)) ∈ set_pmf (config_rand (BIT_init, BIT_step) s0 qs). length x = length s0"
proof
fix x::"('a list × (bool list × 'a list))"
assume ass:"x ∈ set_pmf (config_rand (BIT_init, BIT_step) s0 qs)"
let ?a="fst (snd x)"
from ass have "(fst x,(?a,snd (snd x))) ∈ set_pmf (config_rand (BIT_init, BIT_step) s0 qs)" by auto
with ass have "?a ∈ (fst ∘ snd) ` set_pmf (config_rand (BIT_init, BIT_step) s0 qs)" by force
then have "?a ∈ set_pmf (map_pmf (fst ∘ snd) (config_rand (BIT_init, BIT_step) s0 qs))" by auto
then have "?a ∈ bv (length s0)" by(simp only: config_n_bv)
then have "length ?a = length s0" by (auto simp: len_bv_n)
then show "case x of (uu_, xa, uua_) ⇒ length xa = length s0" by(simp add: split_def)
qed
lemma config_n_fst_init_length2: "∀x ∈ set_pmf (config_rand (BIT_init, BIT_step) s0 qs). length (fst (snd x)) = length s0"
using config_n_fst_init_length by(simp add: split_def)
lemma fperms: "finite {x::'a list. length x = length init ∧ distinct x ∧ set x = set init}"
apply(rule finite_subset[where B="{xs. set xs ⊆ set init ∧ length xs ≤ length init}"])
apply(force) apply(rule finite_lists_length_le) by auto
lemma finite_config_BIT: assumes [simp]: "distinct init"
shows "finite (set_pmf (config_rand (BIT_init, BIT_step) init qs))" (is "finite ?D")
proof -
have a: "(fst ∘ snd) ` ?D ⊆ {x. length x = length init}" using config_n_fst_init_length2 by force
have c: "(snd ∘ snd) ` ?D = {init}"
proof -
have "(snd ∘ snd) ` set_pmf (config_rand (BIT_init, BIT_step) init qs)
= set_pmf (map_pmf (snd ∘ snd) (config_rand (BIT_init, BIT_step) init qs))" by(simp)
also have "… = {init}" apply(subst config_n_init) by simp
finally show ?thesis .
qed
from a c have d: "snd ` ?D ⊆ {x. length x = length init} × {init}" by force
have b: "fst ` ?D ⊆ {x. length x = length init ∧ distinct x ∧ set x = set init}"
using config_rand by fastforce
from b d have "?D ⊆ {x. length x = length init ∧ distinct x ∧ set x = set init} × ({x. length x = length init} × {init})"
by auto
then show ?thesis
apply (rule finite_subset)
apply(rule finite_cartesian_product)
apply(rule fperms)
apply(rule finite_cartesian_product)
apply (rule bitstrings_finite)
by(simp)
qed
subsection "BIT is $1.75$-competitive (a combinatorial proof)"
subsubsection "Definition of the Locale and Helper Functions"
locale BIT_Off =
fixes acts :: "answer list"
fixes qs :: "'a list"
fixes init :: "'a list"
assumes dist_init[simp]: "distinct init"
assumes len_acts: "length acts = length qs"
begin
lemma setinit: "(index init) ` set init = {0..<length init}"
using dist_init
proof(induct init)
case (Cons a as)
with Cons have iH: "index as ` set as = {0..<length as}" by auto
from Cons have 1:"(set as ∩ {x. (a ≠ x)}) = set as" by fastforce
have 2: "(λa. Suc (index as a)) ` set as =
(λa. Suc a) ` ((index as) ` set as )" by auto
show ?case
apply(simp add: 1 2 iH) by auto
qed simp
definition free_A :: "nat list" where
"free_A = map fst acts"
definition paid_A' :: "nat list list" where
"paid_A' = map snd acts"
definition paid_A :: "nat list list" where
"paid_A = map (filter (λx. Suc x < length init)) paid_A'"
lemma len_paid_A[simp]: "length paid_A = length qs"
unfolding paid_A_def paid_A'_def using len_acts by auto
lemma len_paid_A'[simp]: "length paid_A' = length qs"
unfolding paid_A'_def using len_acts by auto
lemma paidAnm_inbound: "n < length paid_A ⟹ m < length(paid_A!n) ⟹ (Suc ((paid_A!n)!(length (paid_A ! n) - Suc m))) < length init"
proof -
assume "n < length paid_A"
then have "n < length paid_A'" by auto
then have a: "(paid_A!n)
= filter (λx. Suc x < length init) (paid_A' ! n)" unfolding paid_A_def by auto
let ?filtered="(filter (λx. Suc x < length init) (paid_A' ! n))"
assume mtt: "m < length (paid_A!n)"
with a have "(length (paid_A ! n) - Suc m) < length ?filtered" by auto
with nth_mem have b: "Suc(?filtered ! (length (paid_A ! n) - Suc m)) < length init" by force
show "Suc (paid_A ! n ! (length (paid_A ! n) - Suc m)) < length init" using a b by auto
qed
fun s_A' :: "nat ⇒ 'a list" where
"s_A' 0 = init" |
"s_A'(Suc n) = step (s_A' n) (qs!n) (free_A!n, paid_A'!n)"
lemma length_s_A'[simp]: "length(s_A' n) = length init"
by (induction n) simp_all
lemma dist_s_A'[simp]: "distinct(s_A' n)"
by(induction n) (simp_all add: step_def)
lemma set_s_A'[simp]: "set(s_A' n) = set init"
by(induction n) (simp_all add: step_def)
fun s_A :: "nat ⇒ 'a list" where
"s_A 0 = init" |
"s_A(Suc n) = step (s_A n) (qs!n) (free_A!n, paid_A!n)"
lemma length_s_A[simp]: "length(s_A n) = length init"
by (induction n) simp_all
lemma dist_s_A[simp]: "distinct(s_A n)"
by(induction n) (simp_all add: step_def)
lemma set_s_A[simp]: "set(s_A n) = set init"
by(induction n) (simp_all add: step_def)
lemma cost_paidAA': "n < length paid_A' ⟹ length (paid_A!n) ≤ length (paid_A'!n)"
unfolding paid_A_def by simp
lemma swaps_filtered: "swaps (filter (λx. Suc x < length xs) ys) xs = swaps (ys) xs"
apply (induct ys) by auto
lemma sAsA': "n < length paid_A' ⟹ s_A' n = s_A n"
proof (induct n)
case (Suc m)
have " s_A' (Suc m)
= mtf2 (free_A!m) (qs!m) (swaps (paid_A'!m) (s_A' m))" by (simp add: step_def)
also from Suc(2) have "… = mtf2 (free_A!m) (qs!m) (swaps (paid_A!m) (s_A' m))"
unfolding paid_A_def
by (simp only: nth_map swaps_filtered[where xs="s_A' m", simplified])
also have "… = mtf2 (free_A!m) (qs!m) (swaps (paid_A!m) (s_A m))" using Suc by auto
also have "… = s_A (Suc m)" by (simp add: step_def)
finally show ?case .
qed simp
lemma sAsA'': "n < length qs ⟹ s_A n = s_A' n"
using sAsA' by auto
definition t_BIT :: "nat ⇒ real" where
"t_BIT n = T_on_rand_n BIT init qs n"
definition T_BIT :: "nat ⇒ real" where
"T_BIT n = (∑i<n. t_BIT i)"
definition c_A :: "nat ⇒ int" where
"c_A n = index (swaps (paid_A!n) (s_A n)) (qs!n) + 1"
definition f_A :: "nat ⇒ int" where
"f_A n = min (free_A!n) (index (swaps (paid_A!n) (s_A n)) (qs!n))"
definition p_A :: "nat ⇒ int" where
"p_A n = size(paid_A!n)"
definition t_A :: "nat ⇒ int" where
"t_A n = c_A n + p_A n"
definition c_A' :: "nat ⇒ int" where
"c_A' n = index (swaps (paid_A'!n) (s_A' n)) (qs!n) + 1"
definition p_A' :: "nat ⇒ int" where
"p_A' n = size(paid_A'!n)"
definition t_A' :: "nat ⇒ int" where
"t_A' n = c_A' n + p_A' n"
lemma t_A_A'_leq: "n < length paid_A' ⟹ t_A n ≤ t_A' n"
unfolding t_A_def t_A'_def c_A_def c_A'_def p_A_def p_A'_def
apply(simp add: sAsA')
unfolding paid_A_def
by (simp add: swaps_filtered[where xs="(s_A n)", simplified])
definition T_A' :: "nat ⇒ int" where
"T_A' n = (∑i<n. t_A' i)"
definition T_A :: "nat ⇒ int" where
"T_A n = (∑i<n. t_A i)"
lemma T_A_A'_leq: "n ≤ length paid_A' ⟹ T_A n ≤ T_A' n"
unfolding T_A'_def T_A_def apply(rule sum_mono)
by (simp add: t_A_A'_leq)
lemma T_A_A'_leq': "n ≤ length qs ⟹ T_A n ≤ T_A' n"
using T_A_A'_leq by auto
fun s'_A :: "nat ⇒ nat ⇒ 'a list" where
"s'_A n 0 = s_A n"
| "(s'_A n (Suc m)) = swap ((paid_A ! n)!(length (paid_A ! n) -(Suc m)) ) (s'_A n m)"
lemma set_s'_A[simp]: "set (s'_A n m) = set init"
apply(induct m) by(auto)
lemma len_s'_A[simp]: "length (s'_A n m) = length init"
apply(induct m) by(auto)
lemma distperm_s'_A[simp]: "dist_perm (s'_A n m) init"
apply(induct m) by auto
lemma s'A_m_le: "m ≤ (length (paid_A ! n)) ⟹ swaps (drop (length (paid_A ! n) - m) (paid_A ! n)) (s_A n) = s'_A n m"
apply(induct m)
apply(simp)
proof -
fix m
assume iH: "(m ≤ length (paid_A ! n) ⟹ swaps (drop (length (paid_A ! n) - m) (paid_A ! n)) (s_A n) = s'_A n m)"
assume Suc: "Suc m ≤ length (paid_A ! n)"
then have "m ≤ length (paid_A ! n)" by auto
with iH have x: "swaps (drop (length (paid_A ! n) - m) (paid_A ! n)) (s_A n) = s'_A n m" by auto
from Suc have mlen: "(length (paid_A ! n) - Suc m) < length (paid_A ! n)" by auto
let ?l="length (paid_A ! n) - Suc m"
let ?Sucl="length (paid_A ! n) - m"
have Sucl: "Suc ?l = ?Sucl" using Suc by auto
from mlen have yu: "((paid_A ! n)! ?l ) # (drop (Suc ?l) (paid_A ! n))
= (drop ?l (paid_A ! n))"
by (rule Cons_nth_drop_Suc)
from Suc have "s'_A n (Suc m)
= swap ((paid_A ! n)!(length (paid_A ! n) - (Suc m)) ) (s'_A n m)" by auto
also have "… = swap ((paid_A ! n)!(length (paid_A ! n) - (Suc m)) )
(swaps (drop (length (paid_A ! n) - m) (paid_A ! n)) (s_A n))"
by(simp only: x)
also have "… = (swaps (((paid_A ! n)!(length (paid_A ! n) - (Suc m)) ) # (drop (length (paid_A ! n) - m) (paid_A ! n))) (s_A n))"
by auto
also have "… = (swaps (((paid_A ! n)! ?l ) # (drop (Suc ?l) (paid_A ! n))) (s_A n))"
using Sucl by auto
also from mlen have "… = (swaps ((drop ?l (paid_A ! n))) (s_A n))"
by (simp only: yu)
finally have " s'_A n (Suc m) = swaps (drop (length (paid_A ! n) - Suc m) (paid_A ! n)) (s_A n)" .
then show " swaps (drop (length (paid_A ! n) - Suc m) (paid_A ! n)) (s_A n) = s'_A n (Suc m)" by auto
qed
lemma s'A_m: "swaps (paid_A ! n) (s_A n) = s'_A n (length (paid_A ! n))"
using s'A_m_le[of "(length (paid_A ! n))" "n", simplified] by auto
definition gebub :: "nat ⇒ nat ⇒ nat" where
"gebub n m = index init ((s'_A n m)!(Suc ((paid_A!n)!(length (paid_A ! n) - Suc m))))"
lemma gebub_inBound: assumes 1: " n < length paid_A " and 2: "m < length (paid_A ! n)"
shows "gebub n m < length init"
proof -
have "Suc (paid_A ! n ! (length (paid_A ! n) - Suc m)) < length (s'_A n m)" using paidAnm_inbound[OF 1 2] by auto
then have "s'_A n m ! Suc (paid_A ! n ! (length (paid_A ! n) - Suc m)) ∈ set (s'_A n m)" by (rule nth_mem)
then show ?thesis
unfolding gebub_def using setinit by auto
qed
subsubsection "The Potential Function"
fun phi :: "nat ⇒'a list× (bool list × 'a list) ⇒ real" ("φ") where
"phi n (c,(b,_)) = (∑(x,y)∈(Inv c (s_A n)). (if b!(index init y) then 2 else 1))"
lemma phi': "phi n z = (∑(x,y)∈(Inv (fst z) (s_A n)). (if (fst (snd z))!(index init y) then 2 else 1))"
proof -
have "phi n z = phi n (fst z, (fst(snd z),snd(snd z)))" by (metis prod.collapse)
also have "… = (∑(x,y)∈(Inv (fst z) (s_A n)). (if (fst (snd z))!(index init y) then 2 else 1))" by(simp del: prod.collapse)
finally show ?thesis .
qed
lemma Inv_empty2: "length d = 0 ⟹ Inv c d = {}"
unfolding Inv_def before_in_def by(auto)
corollary Inv_empty3: "length init = 0 ⟹ Inv c (s_A n) = {}"
apply(rule Inv_empty2) by (metis length_s_A)
lemma phi_empty2: "length init = 0 ⟹ phi n (c,(b,i)) = 0"
apply(simp only: phi.simps Inv_empty3) by auto
lemma phi_nonzero: "phi n (c,(b,i)) ≥ 0"
by (simp add: sum_nonneg split_def)
definition Phi :: "nat ⇒ real" ("Φ") where
"Phi n = E( map_pmf (φ n) (config'' BIT qs init n))"
definition PhiPlus :: "nat ⇒ real" ("Φ⇧+") where
"PhiPlus n = (let
nextconfig = bind_pmf (config'' BIT qs init n)
(λ(s,is). bind_pmf (BIT_step (s,is) (qs!n)) (λ(a,nis). return_pmf (step s (qs!n) a,nis)) )
in
E( map_pmf (phi (Suc n)) nextconfig) )"
lemma PhiPlus_is_Phi_Suc: "n<length qs ⟹ PhiPlus n = Phi (Suc n)"
unfolding PhiPlus_def Phi_def
apply (simp add: bind_return_pmf map_pmf_def bind_assoc_pmf split_def take_Suc_conv_app_nth )
apply(simp add: config'_rand_snoc)
by(simp add: bind_assoc_pmf split_def bind_return_pmf)
lemma phi0: "Phi 0 = 0" unfolding Phi_def
by (simp add: bind_return_pmf map_pmf_def bind_assoc_pmf BIT_init_def)
lemma phi_pos: "Phi n ≥ 0"
unfolding Phi_def
apply(rule E_nonneg_fun)
using phi_nonzero by auto
subsubsection "Helper lemmas"
lemma swap_subs: "dist_perm X Y ⟹ Inv X (swap z Y) ⊆ Inv X Y ∪ {(Y ! z, Y ! Suc z)}"
proof -
assume "dist_perm X Y"
note aj = Inv_swap[OF this, of z]
show "Inv X (swap z Y) ⊆ Inv X Y ∪ {(Y ! z, Y ! Suc z)}"
proof cases
assume c1: "Suc z < length X"
show "Inv X (swap z Y) ⊆ Inv X Y ∪ {(Y ! z, Y ! Suc z)}"
proof cases
assume "Y ! z < Y ! Suc z in X"
with c1 have "Inv X (swap z Y) = Inv X Y ∪ {(Y ! z, Y ! Suc z)}" using aj by auto
then show "Inv X (swap z Y) ⊆ Inv X Y ∪ {(Y ! z, Y ! Suc z)}" by auto
next
assume "~ Y ! z < Y ! Suc z in X"
with c1 have "Inv X (swap z Y) = Inv X Y - {(Y ! Suc z, Y ! z)}" using aj by auto
then show "Inv X (swap z Y) ⊆ Inv X Y ∪ {(Y ! z, Y ! Suc z)}" by auto
qed
next
assume "~ (Suc z < length X)"
then have "Inv X (swap z Y) = Inv X Y" using aj by auto
then show "Inv X (swap z Y) ⊆ Inv X Y ∪ {(Y ! z, Y ! Suc z)}" by auto
qed
qed
subsubsection "InvOf"
term "Inv"
abbreviation "InvOf y bits as ≡ {(x,y)|x. x < y in bits ∧ y < x in as}"
lemma "InvOf y xs ys = {(x,y)|x. (x,y)∈Inv xs ys}"
unfolding Inv_def by auto
lemma "InvOf y xs ys ⊆ Inv xs ys" unfolding Inv_def by auto
lemma numberofIsbeschr: assumes
distxsys: "dist_perm xs ys" and
yinxs: "y ∈ set xs"
shows "index xs y ≤ index ys y + card (InvOf y xs ys)"
(is "?iBit ≤ ?iA + card ?I")
proof -
from assms have distinctxs: "distinct xs"
and distinctys: "distinct ys"
and yinys: "y ∈ set ys" by auto
let ?A="fst ` ?I"
have aha: "card ?A = card ?I" apply(rule card_image)
unfolding inj_on_def by(auto)
have "?A ⊆ (before y xs)" by(auto)
have "?A ⊆ (after y ys)" by auto
have "finite (before y ys)" by auto
have bef: "(before y xs) - ?A ⊆ before y ys" apply(auto)
proof -
fix x
assume a: "x < y in xs"
assume " x ∉ fst ` {(x, y) |x. x < y in xs ∧ y < x in ys}"
then have "~ (x < y in xs ∧ y < x in ys)" by force
with a have d: "~ y < x in ys" by auto
from a have "x ∈ set xs" by (rule before_in_setD1)
with distxsys have b: "x ∈ set ys" by auto
from a have "y ∈ set xs" by (rule before_in_setD2)
with distxsys have c: "y ∈ set ys" by auto
from a have e: "~ x = y" unfolding before_in_def by auto
have "(¬ y < x in ys) = (x < y in ys ∨ y = x)" apply(rule not_before_in)
using b c by auto
with d e show "x < y in ys" by auto
qed
have "(index xs y) - card (InvOf y xs ys) = card (before y xs) - card ?A"
by(simp only: aha card_before[OF distinctxs yinxs])
also have "… = card ((before y xs) - ?A)"
apply(rule card_Diff_subset[symmetric]) by auto
also have "… ≤ card (before y ys)"
apply(rule card_mono)
apply(simp)
apply(rule bef)
done
also have "… = (index ys y)" by(simp only: card_before[OF distinctys yinys])
finally have "index xs y - card ?I ≤ index ys y" .
then show "index xs y ≤ index ys y + card ?I" by auto
qed
lemma "length init = 0 ⟹ length xs = length init ⟹ t xs q (mf, sws) = 1 + length sws"
unfolding t_def by(auto)
lemma integr_index: "integrable (measure_pmf (config'' (BIT_init, BIT_step) qs init n))
(λ(s, is). real (Suc (index s (qs ! n))))"
apply(rule measure_pmf.integrable_const_bound[where B="Suc (length init)"])
apply(simp add: split_def) apply (metis (mono_tags) index_le_size AE_measure_pmf_iff config_rand_length)
by (auto)
subsubsection "Upper Bound on the Cost of BIT"
lemma t_BIT_ub2: "(qs!n) ∉ set init ⟹ t_BIT n ≤ Suc(size init)"
apply(simp add: t_BIT_def t_def BIT_step_def)
apply(simp add: bind_return_pmf)
proof (goal_cases)
case 1
note qs=this
let ?D = "(config'' (BIT_init, BIT_step) qs init n)"
have absch: "(∀x∈ set_pmf ?D. ((λ(s,is). real (Suc (index s (qs ! n)))) x) ≤ ((λ(is,s). Suc (length init)) x))"
proof (rule ballI, goal_cases)
case (1 x)
from 1 config_rand_length have f1: "length (fst x) = length init" by fastforce
from 1 config_rand_set have 2: "set (fst x) = set init" by fastforce
from qs 2 have "(qs!n) ∉ set (fst x)" by auto
then show ?case using f1 by (simp add: split_def)
qed
have "integrable (measure_pmf (config'' (BIT_init, BIT_step) qs init n))
(λ(s, is). Suc (length init))" by(simp)
have "E(bind_pmf ?D (λ(s, is). return_pmf (real (Suc (index s (qs ! n))))))
= E(map_pmf (λ(s, is). real (Suc (index s (qs ! n)))) ?D)"
by(simp add: split_def map_pmf_def)
also have "… ≤ E(map_pmf (λ(s, is). Suc (length init)) ?D)"
apply (rule E_mono3)
apply(fact integr_index)
apply(simp)
using absch by auto
also have "… = Suc (length init)"
by(simp add: split_def)
finally show ?case by(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf split_def)
qed
lemma t_BIT_ub: "(qs!n) ∈ set init ⟹ t_BIT n ≤ size init"
apply(simp add: t_BIT_def t_def BIT_step_def)
apply(simp add: bind_return_pmf)
proof (goal_cases)
case 1
note qs=this
let ?D = "(config'' (BIT_init, BIT_step) qs init n)"
have absch: "(∀x∈ set_pmf ?D. ((λ(s, is). real (Suc (index s (qs ! n)))) x) ≤ ((λ(s, is). length init) x))"
proof (rule ballI, goal_cases)
case (1 x)
from 1 config_rand_length have f1: "length (fst x) = length init" by fastforce
from 1 config_rand_set have 2: "set (fst x) = set init" by fastforce
from qs 2 have "(qs!n) ∈ set (fst x)" by auto
then have "(index (fst x) (qs ! n)) < length init" apply(rule index_less) using f1 by auto
then show ?case by (simp add: split_def)
qed
have "E(bind_pmf ?D (λ(s, is). return_pmf (real (Suc (index s (qs ! n))))))
= E(map_pmf (λ(s, is). real (Suc (index s (qs ! n)))) ?D)"
by(simp add: split_def map_pmf_def)
also have "… ≤ E(map_pmf (λ(s, is). length init) ?D)"
apply(rule E_mono3)
apply(fact integr_index)
apply(simp)
using absch by auto
also have "… = length init"
by(simp add: split_def)
finally show ?case by(simp add: map_pmf_def bind_assoc_pmf bind_return_pmf split_def)
qed
lemma T_BIT_ub: "∀i<n. qs!i ∈ set init ⟹ T_BIT n ≤ n * size init"
proof(induction n)
case 0 show ?case by(simp add: T_BIT_def)
next
case (Suc n) thus ?case
using t_BIT_ub[where n="n"] by (simp add: T_BIT_def)
qed
subsubsection "Main Lemma"
lemma myub: "n < length qs ⟹ t_BIT n + Phi(n + 1) - Phi n ≤ (7 / 4) * t_A n - 3/4"
proof -
assume nqs: "n < length qs"
have "t_BIT n + Phi (n+1) - Phi n ≤ (7 / 4) * t_A n - 3/4"
proof (cases "length init > 0")
case False
show ?thesis
proof -
from False have qsn: "(qs!n) ∉ set init" by auto
from False have l0: "length init = 0" by auto
then have "length (swaps (paid_A ! n) (s_A n)) = 0" using length_s_A by auto
with l0 have 4: "t_A n = 1 + length (paid_A ! n)" unfolding t_A_def c_A_def p_A_def by(simp)
have 1: "t_BIT n ≤ 1" using t_BIT_ub2[OF qsn] l0 by auto
{ fix m
have "phi m = (λ(b,(a,i)). phi m (b,(a,i)))" by auto
also have "… = (λ(b,(a,i)). 0)" by(simp only: phi_empty2[OF l0])
finally have "phi m= (λ(b,(a,i)). 0)".
} note phinull=this
have 2: "PhiPlus n = 0" unfolding PhiPlus_def apply(simp) apply(simp only: phinull)
by (auto simp: split_def)
have 3:"Phi n = 0" unfolding Phi_def apply(simp only: phinull)
by (auto simp: split_def)
have "t_A n ≥ 1 ⟹ 1 ≤ 7 / 4 * (t_A n) - 3 / 4" by(simp)
with 4 have 5: "1 ≤ 7 / 4 * (t_A n) - 3 / 4" by auto
from 1 2 3 have "t_BIT n + PhiPlus n - Phi n ≤ 1" by auto
also from 5 have "… ≤ 7 / 4 * (t_A n) - 3 / 4" by auto
finally show ?thesis using PhiPlus_is_Phi_Suc nqs by auto
qed
next
case True
let ?l = "length init"
from True obtain l' where lSuc: "?l = Suc l'" by (metis Suc_pred)
have 31: "n < length paid_A" using nqs by auto
define q where "q = qs!n"
define D where [simp]: "D = (config'' (BIT_init, BIT_step) qs init n)"
define cost where [simp]: "cost = (λ(s, is).(t s q (if (fst is) ! (index (snd is) q) then 0 else length s, [])))"
define Φ⇩2 where [simp]: "Φ⇩2 = (λ(s, is). ((phi (Suc n)) (step s q (if (fst is) ! (index (snd is) q) then 0 else length s, []),(flip (index (snd is) q) (fst is), snd is))))"
define Φ⇩0 where [simp]: "Φ⇩0 = phi n"
have inEreinziehn: "t_BIT n + Phi (n+1) - Phi n = E (map_pmf (λx. (cost x) + (Φ⇩2 x) - (Φ⇩0 x)) D)"
proof -
have "bind_pmf D
(λ(s, is). bind_pmf (BIT_step (s, is) (q)) (λ(a,nis). return_pmf (real(t s (q) a))))
= bind_pmf D
(λ(s, is). return_pmf (t s q (if (fst is) ! (index (snd is) q) then 0 else length s, [])))"
unfolding BIT_step_def apply (auto simp: bind_return_pmf split_def)
by (metis prod.collapse)
also have "… = map_pmf cost D"
by (auto simp: map_pmf_def split_def)
finally have rightform1: "bind_pmf D
(λ(s, is). bind_pmf (BIT_step (s, is) (q)) (λ(a,nis). return_pmf (real(t s (q) a))))
= map_pmf cost D" .
have rightform2: "map_pmf (phi (Suc n)) (bind_pmf D
(λ(s, is). bind_pmf (BIT_step (s, is) (q)) (λ(a, nis). return_pmf (step s (q) a, nis))))
= map_pmf Φ⇩2 D" apply(simp add: bind_return_pmf bind_assoc_pmf map_pmf_def split_def BIT_step_def)
by (metis prod.collapse)
have "t_BIT n + Phi (n+1) - Phi n =
t_BIT n + PhiPlus n - Phi n" using PhiPlus_is_Phi_Suc nqs by auto
also have "… =
T_on_rand_n BIT init qs n
+ E (map_pmf (phi (Suc n)) (bind_pmf D
(λ(s, is). bind_pmf (BIT_step (s, is) (q)) (λ(a, nis). return_pmf (step s (q) a, nis)))))
- E (map_pmf (phi n) D)
" unfolding PhiPlus_def Phi_def t_BIT_def q_def by auto
also have "… =
E (bind_pmf D
(λ(s, is). bind_pmf (BIT_step (s, is) (q)) (λ(a,nis). return_pmf (t s (q) a))))
+ E (map_pmf (phi (Suc n)) (bind_pmf D
(λ(s, is). bind_pmf (BIT_step (s, is) (q)) (λ(a, nis). return_pmf (step s (q) a, nis)))))
- E (map_pmf Φ⇩0 D)" by (auto simp: q_def split_def)
also have "… = E (map_pmf cost D)
+ E (map_pmf Φ⇩2 D)
- E (map_pmf Φ⇩0 D)" using rightform1 rightform2 split_def by auto
also have "… = E (map_pmf (λx. (cost x) + (Φ⇩2 x)) D) - E (map_pmf (λx. (Φ⇩0 x)) D)"
unfolding D_def using E_linear_plus2[OF finite_config_BIT[OF dist_init]] by auto
also have "… = E (map_pmf (λx. (cost x) + (Φ⇩2 x) - (Φ⇩0 x)) D)"
unfolding D_def by(simp only: E_linear_diff2[OF finite_config_BIT[OF dist_init]] split_def)
finally show "t_BIT n + Phi (n+1) - Phi n
= E (map_pmf (λx. (cost x) + (Φ⇩2 x) - (Φ⇩0 x)) D)" by auto
qed
define xs where [simp]: "xs = s_A n"
define xs' where [simp]: "xs' = swaps (paid_A!n) xs"
define xs'' where [simp]: "xs'' = mtf2 (free_A!n) (q) xs'"
define k where [simp]: "k = index xs' q"
define k' where [simp]: "k' = max 0 (k-free_A!n)"
have [simp]: "length xs = length init" by auto
have dp_xs_init[simp]: "dist_perm xs init" by auto
text "The Transformation"
have ub_cost: "∀x∈set_pmf D. (real (cost x)) + (Φ⇩2 x) - (Φ⇩0 x) ≤ k + 1 +
(if (q) ∈ set init
then (if (fst (snd x))!(index init q) then k-k'
else (∑j<k'. (if (fst (snd x))!(index init (xs'!j)) then 2::real else 1)))
else 0)
+ (∑i<(length (paid_A!n)). (if (fst (snd x))!(gebub n i) then 2 else 1))"
proof (rule, goal_cases)
case (1 x)
note xinD=1
then have [simp]: "snd (snd x) = init" using D_def config_n_init3 by fast
define b where "b = fst (snd x)"
define ys where "ys = fst x"
define aBIT where [simp]: "aBIT = (if b ! (index (snd (snd x)) q) then 0 else length ys, ([]::nat list))"
define ys' where "ys' = step ys (q) aBIT"
define b' where "b' = flip (index init q) b"
define Φ⇩1 where "Φ⇩1 = (λz:: 'a list× (bool list × 'a list) . (∑(x,y)∈(Inv ys xs'). (if fst (snd z)!(index init y) then 2::real else 1)))"
have xs''_step: "xs'' = step xs (q) (free_A!n,paid_A!n)"
unfolding xs'_def xs''_def xs_def step_def free_A_def paid_A_def
by(auto simp: split_def)
have gis2: "(Φ⇩2 (ys,(b,init))) = (∑(x,y)∈(Inv ys' xs''). (if b'!(index init y) then 2 else 1))"
apply(simp only: split_def)
apply(simp only: xs''_step)
apply(simp only: Φ⇩2_def phi.simps)
unfolding b'_def b_def ys'_def aBIT_def q_def
unfolding s_A.simps apply(simp only: split_def) by auto
then have gis: "Φ⇩2 x = (∑(x,y)∈(Inv ys' xs''). (if b'!(index init y) then 2 else 1))"
unfolding ys_def b_def by (auto simp: split_def)
have his2: "(Φ⇩0 (ys,(b,init))) = (∑(x,y)∈(Inv ys xs). (if b!(index init y) then 2 else 1))"
apply(simp only: split_def)
apply(simp only: Φ⇩0_def phi.simps) by(simp add: split_def)
then have his: "(Φ⇩0 x) = (∑(x,y)∈(Inv ys xs). (if b!(index init y) then 2 else 1))"
by(auto simp: ys_def b_def split_def phi')
have dis: "Φ⇩1 x = (∑(x,y)∈(Inv ys xs'). (if b!(index init y) then 2 else 1))"
unfolding Φ⇩1_def b_def by auto
have "ys' = mtf2 (fst aBIT) (q) ys" by (simp add: step_def ys'_def)
from config_rand_distinct[of BIT] config_rand_set[of BIT] xinD
have dp_ys_init[simp]: "dist_perm ys init" unfolding D_def ys_def by force
have dp_ys'_init[simp]: "dist_perm ys' init" unfolding ys'_def step_def by (auto)
then have lenys'[simp]: "length ys' = length init" by (metis distinct_card)
have dp_xs'_init[simp]: "dist_perm xs' init" by auto
have gra: "dist_perm ys xs'" by auto
have leninitb[simp]: "length b = length init" using b_def config_n_fst_init_length2 xinD[unfolded] by auto
have leninitys[simp]: "length ys = length init" using dp_ys_init by (metis distinct_card)
{fix m
have "dist_perm ys (s'_A n m)" using dp_ys_init by auto
} note dist=this
text "Upper bound of the inversions created by paid exchanges of A"
let ?paidUB="(∑i<(length (paid_A!n)). (if b!(gebub n i) then 2::real else 1))"
have paid_ub: "Φ⇩1 x ≤ Φ⇩0 x + ?paidUB"
proof -
have a: "length (paid_A ! n) ≤ length (paid_A ! n)" by auto
have b: "xs' = (s'_A n (length (paid_A ! n)))" using s'A_m by auto
{
fix m
have "m≤length (paid_A!n) ⟹ (∑(x,y)∈(Inv ys (s'_A n m)). (if b!(index init y) then 2::real else 1)) ≤ (∑(x,y)∈(Inv ys xs). (if b!(index init y) then 2 else 1))
+ (∑i<m. (if b!(gebub n i) then 2 else 1))"
proof (induct m)
case (Suc m)
then have m_bd2: "m ≤ length (paid_A ! n)"
and m_bd: "m < length (paid_A ! n)" by auto
note yeah = Suc(1)[OF m_bd2]
let ?revm="(length (paid_A ! n) - Suc m)"
note ah=Inv_swap[of "ys" "(s'_A n m)" "(paid_A ! n ! ?revm)", OF dist]
have "(∑(xa, y)∈Inv ys (s'_A n (Suc m)). if b ! (index init y) then 2::real else 1)
= (∑(xa, y)∈Inv ys (swap (paid_A ! n ! ?revm) (s'_A n m)). if b ! (index init y) then 2 else 1)" using s'_A.simps(2) by auto
also
have "… = (∑(xa, y)∈(if Suc (paid_A ! n ! ?revm) < length ys
then if s'_A n m ! (paid_A ! n ! ?revm) < s'_A n m ! Suc (paid_A ! n ! ?revm) in ys
then Inv ys (s'_A n m) ∪ {(s'_A n m ! (paid_A ! n ! ?revm), s'_A n m ! Suc (paid_A ! n ! ?revm))}
else Inv ys (s'_A n m) - {(s'_A n m ! Suc (paid_A ! n ! ?revm), s'_A n m ! (paid_A ! n ! ?revm))}
else Inv ys (s'_A n m)). if b ! (index init y) then 2::real else 1)" by (simp only: ah)
also
have "… ≤ (∑(xa, y)∈Inv ys (s'_A n m). if b ! (index init y) then 2::real else 1)
+ (if (b) ! (index init (s'_A n m ! Suc (paid_A ! n ! ?revm))) then 2::real else 1)" (is "?A ≤ ?B")
proof(cases "Suc (paid_A ! n ! ?revm) < length ys")
case False
then have "?A = (∑(xa, y)∈(Inv ys (s'_A n m)). if b ! (index init y) then 2 else 1)" by auto
also have "… ≤ (∑(xa, y)∈(Inv ys (s'_A n m)). if b ! (index init y) then 2 else 1) +
(if b ! (index init (s'_A n m ! Suc (paid_A ! n ! ?revm))) then 2::real else 1)" by auto
finally show "?A ≤ ?B" .
next
case True
then have "?A = (∑(xa, y)∈(if s'_A n m ! (paid_A ! n ! ?revm) < s'_A n m ! Suc (paid_A ! n ! ?revm) in ys
then Inv ys (s'_A n m) ∪ {(s'_A n m ! (paid_A ! n ! ?revm), s'_A n m ! Suc (paid_A ! n ! ?revm))}
else Inv ys (s'_A n m) - {(s'_A n m ! Suc (paid_A ! n ! ?revm), s'_A n m ! (paid_A ! n ! ?revm))}
). if b ! (index init y) then 2 else 1)" by auto
also have "… ≤ ?B" (is "?A' ≤ ?B")
proof (cases "s'_A n m ! (paid_A ! n ! ?revm) < s'_A n m ! Suc (paid_A ! n ! ?revm) in ys")
case True
let ?neurein="(s'_A n m ! (paid_A ! n ! ?revm), s'_A n m ! Suc (paid_A ! n ! ?revm))"
from True have "?A' = (∑(xa, y)∈(Inv ys (s'_A n m) ∪ {?neurein}
). if b ! (index init y) then 2 else 1)" by auto
also have "… = (∑(xa, y)∈insert ?neurein (Inv ys (s'_A n m)
). if b ! (index init y) then 2 else 1)" by auto
also have "… ≤ (if b ! (index init (snd ?neurein)) then 2 else 1)
+ (∑(xa, y)∈(Inv ys (s'_A n m)). if b ! (index init y) then 2 else 1)"
proof (cases "?neurein ∈ Inv ys (s'_A n m)")
case True
then have "insert ?neurein (Inv ys (s'_A n m)) = (Inv ys (s'_A n m))" by auto
then have "(∑(xa, y)∈insert ?neurein (Inv ys (s'_A n m)). if b ! (index init y) then 2 else 1)
= (∑(xa, y)∈(Inv ys (s'_A n m)). if b ! (index init y) then 2 else 1)" by auto
also have "… ≤ (if b ! (index init (snd ?neurein)) then 2::real else 1)
+ (∑(xa, y)∈(Inv ys (s'_A n m)). if b ! (index init y) then 2 else 1)" by auto
finally show ?thesis .
next
case False
have "(∑(xa, y)∈insert ?neurein (Inv ys (s'_A n m)). if b ! (index init y) then 2 else 1)
= (∑y∈insert ?neurein (Inv ys (s'_A n m)). (λi. if b ! (index init (snd i)) then 2 else 1) y)" by(auto simp: split_def)
also have "… = (λi. if b ! (index init (snd i)) then 2 else 1) ?neurein
+ (∑y∈(Inv ys (s'_A n m)) - {?neurein}. (λi. if b ! (index init (snd i)) then 2 else 1) y)"
apply(rule sum.insert_remove) by(auto)
also have "… = (if b ! (index init (snd ?neurein)) then 2 else 1)
+ (∑y∈(Inv ys (s'_A n m)). (λi. if b ! (index init (snd i)) then 2::real else 1) y)" using False by auto
also have "… ≤ (if b ! (index init (snd ?neurein)) then 2 else 1)
+ (∑(xa, y)∈(Inv ys (s'_A n m)). if b ! (index init y) then 2 else 1)" by(simp only: split_def)
finally show ?thesis .
qed
also have "… = (∑(xa, y)∈Inv ys (s'_A n m). if b ! (index init y) then 2 else 1) +
(if b ! (index init (s'_A n m ! Suc (paid_A ! n ! ?revm))) then 2 else 1)" by auto
finally show ?thesis .
next
case False
then have "?A' = (∑(xa, y)∈(Inv ys (s'_A n m) - {(s'_A n m ! Suc (paid_A ! n ! ?revm), s'_A n m ! (paid_A ! n ! ?revm))}
). if b ! (index init y) then 2 else 1)" by auto
also have "… ≤ (∑(xa, y)∈(Inv ys (s'_A n m)). if b ! (index init y) then 2 else 1)" (is "(∑(xa, y)∈?X-{?x}. ?g y) ≤ (∑(xa, y)∈?X. ?g y) ")
proof (cases "?x ∈ ?X")
case True
have "(∑(xa, y)∈?X-{?x}. ?g y) ≤ (%(xa,y). ?g y) ?x + (∑(xa, y)∈?X-{?x}. ?g y)"
by simp
also have "… = (∑(xa, y)∈?X. ?g y)"
apply(rule sum.remove[symmetric])
apply simp apply(fact) done
finally show ?thesis .
qed simp
also have "… ≤ ?B" by auto
finally show ?thesis .
qed
finally show "?A ≤ ?B" .
qed
also have "…
≤ (∑(xa, y)∈Inv ys (s_A n). if b ! (index init y) then 2::real else 1) + (∑i<m. if b ! gebub n i then 2::real else 1)
+ (if (b) ! (index init (s'_A n m ! Suc (paid_A ! n ! ?revm))) then 2::real else 1)" using yeah by simp
also have "… = (∑(xa, y)∈Inv ys (s_A n). if b ! (index init y) then 2::real else 1) + (∑i<m. if b ! gebub n i then 2 else 1)
+ (if (b) ! gebub n m then 2 else 1)" unfolding gebub_def by simp
also have "… = (∑(xa, y)∈Inv ys (s_A n). if b ! (index init y) then 2::real else 1) + (∑i<(Suc m). if b ! gebub n i then 2 else 1)"
by auto
finally show ?case by simp
qed (simp add: split_def)
} note x = this[OF a]
show ?thesis
unfolding Φ⇩1_def his apply(simp only: b) using x b_def by auto
qed
text "Upper bound for the costs of BIT"
define inI where [simp]: "inI = InvOf (q) ys xs'"
define I where [simp]: "I = card(InvOf (q) ys xs')"
have ub_cost_BIT: "(cost x) ≤ k + 1 + I"
proof (cases "(q) ∈ set init")
case False
from False have 4: "I = 0" by(auto simp: before_in_def)
have "(cost x) = 1 + index ys (q)" by (auto simp: ys_def t_def split_def)
also have "… = 1 + length init" using False by auto
also have "… = 1 + k" using False by auto
finally show ?thesis using 4 by auto
next
case True
then have gra2: "(q) ∈ set ys" using dp_ys_init by auto
have "(cost x) = 1 + index ys (q)" by(auto simp: ys_def t_def split_def)
also have "… ≤ k + 1 + I" using numberofIsbeschr[OF gra gra2] by auto
finally show"(cost x) ≤ k + 1 + I" .
qed
text "Upper bound for inversions generated by free exchanges"
define ub_free
where "ub_free =
(if (q ∈ set init)
then (if b!(index init q) then k-k' else (∑j<k'. (if (b)!(index init (xs'!j)) then 2::real else 1) ))
else 0)"
let ?ub2 = "- I + ub_free"
have free_ub: "(∑(x,y)∈(Inv ys' xs''). (if b' !(index init y) then 2 else 1 ) )
- (∑(x,y)∈(Inv ys xs'). (if b!(index init y) then 2 else 1) ) ≤ ?ub2"
proof (cases "(q) ∈ set init")
case False
from False have 1: "ys' = ys" unfolding ys'_def step_def mtf2_def by(simp)
from False have 2: "xs' = xs''" unfolding xs''_def mtf2_def by(simp)
from False have "(index init q) ≥ length b" using setinit by auto
then have 3: "b' = b" unfolding b'_def using flip_out_of_bounds by auto
from False have 4: "I = 0" unfolding I_def before_in_def by(auto)
note ubnn=False
have nn: "k-k'≥0" unfolding k_def k'_def by auto
from 1 2 3 4 have "(∑(x,y)∈(Inv ys' xs''). (if b'!(index init y) then 2::real else 1))
- (∑(x,y)∈(Inv ys xs'). (if b!(index init y) then 2 else 1)) = -I" by auto
with ubnn show ?thesis unfolding ub_free_def by auto
next
case True
note queryinlist=this
then have gra2: "q ∈ set ys" using dp_ys_init by auto
have k_inbounds: "k < length init"
using index_less_size_conv queryinlist
by (simp)
{
fix y e
fix X::"bool list"
assume rd: "e < length X"
have "y < length X ⟹ (if flip e X ! y then 2::real else 1) - (if X ! y then 2 else 1)
= (if e=y then (if X ! y then -1 else 1) else 0)"
proof cases
assume "y < length X" and ey: "e=y"
then have "(if flip e X ! y then 2::real else 1) - (if X ! y then 2 else 1)
= (if X ! y then 1::real else 2) - (if X ! y then 2 else 1)" using flip_itself by auto
also have "… = (if X ! y then -1::real else 1)" by auto
finally
show "(if flip e X ! y then 2::real else 1) - (if X ! y then 2 else 1)
= (if e=y then (if X ! y then -1 else 1) else 0)" using ey by auto
next
assume len: "y < length X" and eny: "e≠y"
then have "(if flip e X ! y then 2::real else 1) - (if X ! y then 2 else 1)
= (if X ! y then 2::real else 1) - (if X ! y then 2 else 1)" using flip_other[OF len rd eny] by auto
also have "… = 0" by auto
finally
show "(if flip e X ! y then 2::real else 1) - (if X ! y then 2 else 1)
= (if e=y then (if X ! y then -1 else 1) else 0)" using eny by auto
qed
} note flipstyle=this
from queryinlist setinit have qsfst: "(index init q) < length b" by simp
have fA: "finite (Inv ys' xs'')" by auto
have fB: "finite (Inv ys xs')" by auto
define Δ where [simp]: "Δ = (∑(x,y)∈(Inv ys' xs''). (if b'!(index init y) then 2::real else 1))
- (∑(x,y)∈(Inv ys xs'). (if b!(index init y) then 2 else 1))"
define C where [simp]: "C = (∑(x,y)∈(Inv ys' xs'') ∩ (Inv ys xs'). (if b'!(index init y) then 2::real else 1)
- (if b!(index init y) then 2 else 1))"
define A where [simp]: "A = (∑(x,y)∈(Inv ys' xs'')-(Inv ys xs'). (if b'!(index init y) then 2::real else 1))"
define B where [simp]: "B = (∑(x,y)∈(Inv ys xs')-(Inv ys' xs''). (if b!(index init y) then 2::real else 1))"
have teilen: "Δ = C + A - B"
unfolding Δ_def A_def B_def C_def
using sum_my[OF fA fB] by (auto simp: split_def)
then have "Δ = A - B + C" by auto
then have teilen2: "Φ⇩2 x - Φ⇩1 x = A - B + C" unfolding Δ_def using dis gis by auto
have setys': "(index init) ` (set ys') = {0..<length ys'}"
proof -
have "(index init) ` (set ys') = (index init) ` (set init)" by auto
also have "… = {0..<length init}" using setinit by auto
also have "… = {0..<length ys'}" using lenys' by auto
finally show ?thesis .
qed
have BC_absch: "C - B ≤ -I"
proof (cases "b!(index init q)")
case True
then have samesame: "ys' = ys" unfolding ys'_def step_def by auto
then have puh: "(Inv ys' xs') = (Inv ys xs')" by auto
{
fix α β
assume "(α,β)∈(Inv ys' xs'') ∩ (Inv ys' xs')"
then have "(α,β)∈(Inv ys' xs'')" by auto
then have "(α< β in ys')" unfolding Inv_def by auto
then have 1: "β ∈ set ys'" by (simp only: before_in_setD2)
then have "index init β < length ys'" using setys' by auto
then have "index init β < length init" using lenys' by auto
then have puzzel: "index init β < length b" using leninitb by auto
have betainit: "β ∈ set init" using 1 by auto
have aha: "(q=β) = (index init q = index init β)"
using betainit by simp
have "(if b'!(index init β) then 2::real else 1) - (if b!(index init β) then 2 else 1)
= (if (index init q) = (index init β) then if b !(index init β) then - 1 else 1 else 0)"
unfolding b'_def apply(rule flipstyle) by(fact)+
also have "… = (if (index init q) = (index init β) then if b ! (index init q) then - 1 else 1 else 0)" by auto
also have "… = (if q = β then - 1 else 0)" using aha True by auto
finally have "(if b'!(index init β) then 2::real else 1) - (if b!(index init β) then 2 else 1)
= (if (q) = β then -1::real else 0)" by auto
}
then have grreeeaa: "∀x∈(Inv ys' xs'') ∩ (Inv ys' xs').
(λx. (if b'! (index init (snd x)) then 2::real else 1) - (if b! (index init (snd x)) then 2 else 1)) x
= (λx. (if (q) = snd x then -1::real else 0)) x" by force
let ?fin="(Inv ys' xs'') ∩ (Inv ys' xs')"
have ttt: "{(x,y). (x,y)∈(Inv ys' xs'') ∩ (Inv ys' xs')
∧ y = (q)} ∪ {(x,y). (x,y)∈(Inv ys' xs'') ∩ (Inv ys' xs')
∧ y ≠ (q)} = (Inv ys' xs'') ∩ (Inv ys' xs')" (is "?split1 ∪ ?split2 = ?easy") by auto
have interem: "?split1 ∩ ?split2 = {}" by auto
have split1subs: "?split1 ⊆ ?fin" by auto
have split2subs: "?split2 ⊆ ?fin" by auto
have fs1: "finite ?split1" apply(rule finite_subset[where B="?fin"])
apply(rule split1subs) by(auto)
have fs2: "finite ?split2" apply(rule finite_subset[where B="?fin"])
apply(rule split2subs) by(auto)
have "k - k' ≤ (free_A!n)" by auto
have g: "InvOf (q) ys' xs'' ⊇ InvOf (q) ys' xs'"
using True apply(auto) apply(rule mtf2_mono[of "swaps (paid_A ! n) (s_A n)"])
by (auto simp: queryinlist)
have h: "?split1 = (InvOf (q) ys' xs'') ∩ (InvOf (q) ys' xs')"
unfolding Inv_def by auto
also from g have "… = InvOf (q) ys' xs'" by force
also from samesame have "… = InvOf (q) ys xs'" by simp
finally have "?split1 = inI" unfolding inI_def .
then have cardsp1isI: "card ?split1 = I" by auto
{
fix a b
assume "(a,b)∈?split1"
then have "b = (q)" by auto
then have "(if (q) = b then (-1::real) else 0) = (-1::real)" by auto
}
then have split1easy: "∀x∈?split1.
(λx. (if (q) = snd x then (-1::real) else 0)) x = (λx. (-1::real)) x" by force
{
fix a b
assume "(a,b)∈?split2"
then have "~ b = (q)" by auto
then have "(if (q) = b then (-1::real) else 0) = 0" by auto
}
then have split2easy: "∀x∈?split2.
(λx. (if (q) = snd x then (-1::real) else 0)) x = (λx. 0::real) x" by force
have E0: "C =
(∑(x,y)∈(Inv ys' xs'') ∩ (Inv ys xs').
(if b'!(index init y) then 2::real else 1) - (if b!(index init y) then 2 else 1))" by auto
also from puh have E1: "... =
(∑(x,y)∈(Inv ys' xs'') ∩ (Inv ys' xs').
(if b'!(index init y) then 2::real else 1) - (if b!(index init y) then 2 else 1))" by auto
also have E2: "… = (∑(x,y)∈?easy.
(if (q) = y then (-1::real) else 0))" using sum_my2[OF grreeeaa] by (auto simp: split_def)
also have E3: "… = (∑(x,y)∈?split1 ∪ ?split2.
(if (q) = y then (-1::real) else 0))" by(simp only: ttt)
also have "… = (∑(x,y)∈?split1. (if (q) = y then (-1::real) else 0))
+ (∑(x,y)∈?split2. (if (q) = y then (-1::real) else 0))
- (∑(x,y)∈?split1 ∩ ?split2. (if (q) = y then (-1::real) else 0))"
by(rule sum_Un[OF fs1 fs2])
also have "… = (∑(x,y)∈?split1. (if (q) = y then (-1::real) else 0))
+ (∑(x,y)∈?split2. (if (q) = y then (-1::real) else 0))"
apply(simp only: interem) by auto
also have E4: "… = (∑(x,y)∈?split1. (-1::real) )
+ (∑(x,y)∈?split2. 0)"
using sum_my2[OF split1easy]sum_my2[OF split2easy] by(simp only: split_def)
also have "… = (∑(x,y)∈?split1. (-1::real) )" by auto
also have E5: "… = - card ?split1 " by auto
also have E6: "… = - I " using cardsp1isI by auto
finally have abschC: "C = -I".
have abschB: "B ≥ (0::real)" unfolding B_def apply(rule sum_nonneg) by auto
from abschB abschC show "C - B ≤ -I" by simp
next
case False
from leninitys False have ya: "ys' = mtf2 (length ys) q ys"
unfolding step_def ys'_def by(auto)
have "index ys' q = 0"
unfolding ya apply(rule mtf2_moves_to_front)
using gra2 by simp_all
then have nixbefore: "before q ys' = {}" unfolding before_in_def by auto
{
fix α β
assume "(α,β)∈(Inv ys' xs'') ∩ (Inv ys xs')"
then have "(α,β)∈(Inv ys' xs'')" by auto
then have "(α< β in ys')" unfolding Inv_def by auto
then have 1: "β ∈ set ys'" by (simp only: before_in_setD2)
then have "(index init β) < length ys'" using setys' by auto
then have "(index init β) < length init" using lenys' by auto
then have puzzel: "(index init β) < length b" using leninitb by auto
have betainit: "β ∈ set init" using 1 by auto
have aha: "(q=β) = (index init q = index init β)"
using betainit by simp
have "(if b'!(index init β) then 2::real else 1) - (if b!(index init β) then 2 else 1)
= (if (index init q) = (index init β) then if b ! (index init β) then - 1 else 1 else 0)"
unfolding b'_def apply(rule flipstyle) by(fact)+
also have "… = (if (index init q) = (index init β) then if b ! (index init q) then - 1 else 1 else 0)" by auto
also have "… = (if (q) = β then 1 else 0)" using False aha by auto
finally have "(if b'!(index init β) then 2::real else 1) - (if b!(index init β) then 2 else 1)
= (if (q) = β then 1::real else 0)" by auto
}
then have grreeeaa2: "∀x∈(Inv ys' xs'') ∩ (Inv ys xs').
(λx. (if b'! (index init (snd x)) then 2::real else 1) - (if b! (index init (snd x)) then 2 else 1)) x
= (λx. (if (q) = snd x then 1::real else 0)) x" by force
let ?fin="(Inv ys' xs'') ∩ (Inv ys xs')"
have ttt: "{(x,y). (x,y)∈(Inv ys' xs'') ∩ (Inv ys xs')
∧ y = (q)} ∪ {(x,y). (x,y)∈(Inv ys' xs'') ∩ (Inv ys xs')
∧ y ≠ (q)} = (Inv ys' xs'') ∩ (Inv ys xs')" (is "?split1 ∪ ?split2 = ?easy") by auto
have interem: "?split1 ∩ ?split2 = {}" by auto
have split1subs: "?split1 ⊆ ?fin" by auto
have split2subs: "?split2 ⊆ ?fin" by auto
have fs1: "finite ?split1" apply(rule finite_subset[where B="?fin"])
apply(rule split1subs) by(auto)
have fs2: "finite ?split2" apply(rule finite_subset[where B="?fin"])
apply(rule split2subs) by(auto)
have split1easy : "∀x∈?split1.
(λx. (if (q) = snd x then (1::real) else 0)) x = (λx. (1::real)) x" by force
have split2easy : "∀x∈?split2.
(λx. (if (q) = snd x then (1::real) else 0)) x = (λx. (0::real)) x" by force
from nixbefore have InvOfempty: "InvOf q ys' xs'' = {}" unfolding Inv_def by auto
have "?split1 = InvOf q ys' xs'' ∩ InvOf q ys xs'"
unfolding Inv_def by auto
also from InvOfempty have "… = {}" by auto
finally have split1empty: "?split1 = {}" .
have "C = (∑(x,y)∈?easy.
(if (q) = y then (1::real) else 0))" unfolding C_def by(simp only: split_def sum_my2[OF grreeeaa2])
also have "… = (∑(x,y)∈?split1 ∪ ?split2.
(if (q) = y then (1::real) else 0))" by(simp only: ttt)
also have "… = (∑(x,y)∈?split1. (if (q) = y then (1::real) else 0))
+ (∑(x,y)∈?split2. (if (q) = y then (1::real) else 0))
- (∑(x,y)∈?split1 ∩ ?split2. (if (q) = y then (1::real) else 0))"
by(rule sum_Un[OF fs1 fs2])
also have "… = (∑(x,y)∈?split1. (if (q) = y then (1::real) else 0))
+ (∑(x,y)∈?split2. (if (q) = y then (1::real) else 0))"
apply(simp only: interem) by auto
also have "… = (∑(x,y)∈?split1. (1::real) )
+ (∑(x,y)∈?split2. 0)" using sum_my2[OF split1easy] sum_my2[OF split2easy] by (simp only: split_def)
also have "… = (∑(x,y)∈?split1. (1::real) )" by auto
also have "… = card ?split1" by auto
also have "… = (0::real)" apply(simp only: split1empty) by auto
finally have abschC: "C = (0::real)" .
have ttt2: "{(x,y). (x,y)∈(Inv ys xs') - (Inv ys' xs'')
∧ y = (q)} ∪ {(x,y). (x,y)∈(Inv ys xs') - (Inv ys' xs'')
∧ y ≠ (q)} = (Inv ys xs') - (Inv ys' xs'')" (is "?split1 ∪ ?split2 = ?easy2") by auto
have interem: "?split1 ∩ ?split2 = {}" by auto
have split1subs: "?split1 ⊆ ?easy2" by auto
have split2subs: "?split2 ⊆ ?easy2" by auto
have fs1: "finite ?split1" apply(rule finite_subset[where B="?easy2"])
apply(rule split1subs) by(auto)
have fs2: "finite ?split2" apply(rule finite_subset[where B="?easy2"])
apply(rule split2subs) by(auto)
from False have split1easy2: "∀x∈?split1.
(λx. (if b! (index init (snd x)) then 2::real else 1)) x = (λx. (1::real)) x" by force
have "?split1 = (InvOf q ys xs') - (InvOf q ys' xs'')"
unfolding Inv_def by auto
also have "… = inI" unfolding InvOfempty by auto
finally have splI: "?split1 = inI" .
have abschaway: "(∑(x,y)∈?split2. (if b!(index init y) then 2::real else 1)) ≥ 0"
apply(rule sum_nonneg) by auto
have "B = (∑(x,y)∈?split1 ∪ ?split2.
(if b!(index init y) then 2::real else 1) )" unfolding B_def by(simp only: ttt2)
also have "… = (∑(x,y)∈?split1. (if b!(index init y) then 2::real else 1))
+ (∑(x,y)∈?split2. (if b!(index init y) then 2::real else 1))
- (∑(x,y)∈?split1 ∩ ?split2. (if b!(index init y) then 2::real else 1))"
by(rule sum_Un[OF fs1 fs2])
also have "… = (∑(x,y)∈?split1. (if b!(index init y) then 2::real else 1))
+ (∑(x,y)∈?split2. (if b!(index init y) then 2::real else 1))"
apply(simp only: interem) by auto
also have "… = (∑(x,y)∈?split1. 1)
+ (∑(x,y)∈?split2. (if b!(index init y) then 2::real else 1))"
using sum_my2[OF split1easy2] by (simp only: split_def)
also have "… = card ?split1
+ (∑(x,y)∈?split2. (if b!(index init y) then 2::real else 1))" by auto
also have "… = I
+ (∑(x,y)∈?split2. (if b!(index init y) then 2::real else 1))" using splI by auto
also have "… ≥ I" using abschaway by auto
finally have abschB: "B ≥ I" .
from abschB abschC show "C - B ≤ -I" by auto
qed
have A_absch: "A
≤ (if b!(index init q) then k-k' else (∑j<k'. (if b!(index init (xs'!j)) then 2::real else 1)))"
proof (cases "b!(index init q)")
case False
from leninitys False have ya: "ys' = mtf2 (length ys) q ys"
unfolding step_def ys'_def by(auto)
have "index ys' q = 0" unfolding ya apply(rule mtf2_moves_to_front)
using gra2 by(simp_all)
then have nixbefore: "before q ys' = {}" unfolding before_in_def by auto
have "A = (∑(x,y)∈(Inv ys' xs'')-(Inv ys xs'). (if b'!(index init y) then 2::real else 1))" by auto
have "index (mtf2 (free_A ! n) (q) (swaps (paid_A ! n) (s_A n))) (q)
= (index (swaps (paid_A ! n) (s_A n)) (q) - free_A ! n)"
apply(rule mtf2_q_after) using queryinlist by auto
then have whatisk': "k' = index xs'' q" by auto
have ss: "set ys' = set ys" by auto
have ss2: "set xs' = set xs''" by auto
have di: "distinct init" by auto
have dys: "distinct ys" by auto
have "(Inv ys' xs'')-(Inv ys xs')
= {(x,y). x < y in ys' ∧ y < x in xs'' ∧ (~x < y in ys ∨ ~ y < x in xs')}"
unfolding Inv_def by auto
also have "… =
{(x,y). y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ (~x < y in ys ∨ ~ y < x in xs') }"
using nixbefore by blast
also have "… =
{(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ (~x < y in ys ∨ ~ y < x in xs') }"
unfolding before_in_def by auto
also have "… =
{(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ ~x < y in ys }
∪ {(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ ~ y < x in xs' }"
by force
also have "… =
{(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ y < x in ys }
∪ {(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ ~ y < x in xs' }"
using before_in_setD1[where xs="ys'"] before_in_setD2[where xs="ys'"] not_before_in ss by metis
also have "… =
{(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ y < x in ys }
∪ {(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ x < y in xs' }" (is "?S1 ∪ ?S2 = ?S1 ∪ ?S2'")
proof -
have "?S2 = ?S2'" apply(safe)
proof (goal_cases)
case (2 a b)
from 2(5) have "~ b < a in xs'" by auto
with 2(6) show "False" by auto
next
case (1 a b)
from 1(4) have "a ∈ set xs'" "b ∈ set xs'"
using before_in_setD1[where xs="xs''"]
before_in_setD2[where xs="xs''"] ss2 by auto
with not_before_in 1(5) have "(a < b in xs' ∨ a = b)" by metis
with 1(1) show "a < b in xs'" by auto
qed
then show ?thesis by auto
qed
also have "… =
{(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ y < x in ys }
∪ {(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ ~ x < y in xs'' ∧ x < y in xs' }" (is "?S1 ∪ ?S2 = ?S1 ∪ ?S2'")
proof -
have "?S2 = ?S2'" apply(safe)
proof (goal_cases)
case (1 a b)
from 1(4) have "~ a < b in xs''" by auto
with 1(6) show "False" by auto
next
case (2 a b)
from 2(5) have "a ∈ set xs''" "b ∈ set xs''"
using before_in_setD1[where xs="xs'"]
before_in_setD2[where xs="xs'"] ss2 by auto
with not_before_in 2(4) have "(b < a in xs'' ∨ a = b)" by metis
with 2(1) show "b < a in xs''" by auto
qed
then show ?thesis by auto
qed
also have "… =
{(x,y). x≠y ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ y < x in ys }
∪ {}"
using x_stays_before_y_if_y_not_moved_to_front[where xs="xs'" and q="q"]
before_in_setD1[where xs="xs'"] before_in_setD2[where xs="xs'"] by (auto simp: queryinlist)
also have "… =
{(x,y). x≠y ∧ x=q ∧ y≠q ∧ x < y in ys' ∧ y < x in xs'' ∧ y < x in ys }"
apply(simp only: ya) using swapped_by_mtf2[where xs="ys" and q="q" and n="(length ys)"] dys
before_in_setD1[where xs="ys"] before_in_setD2[where xs="ys"] by (auto simp: queryinlist)
also have "… ⊆
{(x,y). x=q ∧ y≠q ∧ q < y in ys' ∧ y < q in xs''}" by force
also have "… =
{(x,y). x=q ∧ y≠q ∧ q < y in ys' ∧ y < q in xs'' ∧ y ∈ set xs''}"
using before_in_setD1 by metis
also have "… =
{(x,y). x=q ∧ y≠q ∧ q < y in ys' ∧ index xs'' y < index xs'' q ∧ q ∈ set xs'' ∧ y ∈ set xs''}" unfolding before_in_def by auto
also have "… =
{(x,y). x=q ∧ y≠q ∧ q < y in ys' ∧ index xs'' y < index xs' q - (free_A ! n) ∧ q ∈ set xs'' ∧ y ∈ set xs''}"
using mtf2_q_after[where A="xs'" and q="q"] by force
also have "… ⊆
{(x,y). x=q ∧ y≠q ∧ index xs' y < index xs' q - (free_A ! n) ∧ y ∈ set xs''}"
using mtf2_backwards_effect4'[where xs="xs'" and q="q" and n="(free_A ! n)", simplified ]
by auto
also have "… ⊆
{(x,y). x=q ∧ y≠q ∧ index xs' y < k'}"
using mtf2_q_after[where A="xs'" and q="q"] by auto
finally have subsa: "(Inv ys' xs'')-(Inv ys xs')
⊆ {(x,y). x=q ∧ y≠q ∧ index xs' y < k'}" .
have k'xs': "k' < length xs''" unfolding whatisk'
apply(rule index_less) by (auto simp: queryinlist)
then have k'xs': "k' < length xs'" by auto
have "{(x,y). x=q ∧ index xs' y < k'}
⊆ {(x,y). x=q ∧ index xs' y < length xs'}" using k'xs' by auto
also have "… = {(x,y). x=q ∧ y ∈ set xs'}"
using index_less_size_conv by fast
finally have "{(x,y). x=q ∧ index xs' y < k'} ⊆ {(x,y). x=q ∧ y ∈ set xs'}" .
then have finia2: "finite {(x,y). x=q ∧ index xs' y < k'}"
apply(rule finite_subset) by(simp)
have lulae: "{(a,b). a=q ∧ index xs' b < k'}
= {(q,b)|b. index xs' b < k'}" by auto
have k'b: "k' < length b" using whatisk' by (auto simp: queryinlist)
have asdasd: "{(α,β). α=q ∧ β≠q ∧ index xs' β < k'}
= {(α,β). α=q ∧ β≠q ∧ index xs' β < k' ∧ (index init β) < length b }"
proof (auto, goal_cases)
case (1 b)
from 1(2) have "index xs' b < index xs' (q)" by auto
also have "… < length xs'" by (auto simp: queryinlist)
finally have "b ∈ set xs'" using index_less_size_conv by metis
then show ?case using setinit by auto
qed
{ fix β
have "β≠q ⟹ (index init β)≠(index init q)"
using queryinlist by auto
} note ij=this
have subsa2: "{(α,β). α=q ∧ β≠q ∧ index xs' β < k'} ⊆
{(α,β). α=q ∧ index xs' β < k'}" by auto
then have finia: "finite {(x,y). x=q ∧ y≠q ∧ index xs' y < k'}"
apply(rule finite_subset) using finia2 by auto
have E0: "A = (∑(x,y)∈(Inv ys' xs'')-(Inv ys xs'). (if b'!(index init y) then 2::real else 1))" by auto
also have E1: "… ≤ (∑(x,y)∈{(a,b). a=q ∧ b≠q ∧ index xs' b < k'}. (if b'!(index init y) then 2::real else 1))"
unfolding A_def apply(rule sum_mono2[OF finia subsa]) by auto
also have "… = (∑(x,y)∈{(α,β). α=q ∧ β≠q ∧ index xs' β < k'
∧ (index init β) < length b }. (if b'!(index init y) then 2::real else 1))"
using asdasd by auto
also have "… = (∑(x,y)∈{(α,β). α=q ∧ β≠q ∧ index xs' β < k'
∧ (index init β) < length b }. (if b!(index init y) then 2::real else 1))"
proof (rule sum.cong, goal_cases)
case (2 z)
then obtain α β where zab: "z=(α, β)" and "α = q" and diff: "β ≠ q" and "index xs' β < k'" and i: "index init β < length b" by auto
from diff ij have "index init β ≠ index init q" by auto
with flip_other qsfst i have "b' ! index init β = b ! index init β" unfolding b'_def by auto
with zab show ?case by(auto simp add: split_def)
qed simp
also have E1a: "… = (∑(x,y)∈{(a,b). a=q ∧ b≠q ∧ index xs' b < k'}. (if b!(index init y) then 2::real else 1))"
using asdasd by auto
also have "… ≤ (∑(x,y)∈{(a,b). a=q ∧ index xs' b < k'}. (if b!(index init y) then 2::real else 1))"
apply(rule sum_mono2[OF finia2 subsa2]) by auto
also have E2: "… = (∑(x,y)∈{(q,b)|b. index xs' b < k'}. (if b!(index init y) then 2::real else 1))"
by (simp only: lulae[symmetric])
finally have aa: "A ≤ (∑(x,y)∈{(q,b)|b. index xs' b < k'}. (if b!(index init y) then 2::real else 1))" .
have sameset: "{y. index xs' y < k'} = {xs'!i | i. i < k'}"
proof (safe, goal_cases)
case (1 z)
show ?case
proof
from 1(1) have "index xs' z < index (swaps (paid_A ! n) (s_A n)) (q)"
by auto
also have "… < length xs'" using index_less_size_conv by (auto simp: queryinlist)
finally have "index xs' z < length xs'" .
then have zset: "z ∈ set xs'" using index_less_size_conv by metis
have f1: "xs' ! (index xs' z) = z"
apply(rule nth_index) using zset by auto
show "z = xs' ! (index xs' z) ∧ (index xs' z) < k'"
using f1 1(1) by auto
qed
next
case (2 k i)
from 2(1) have "i < index (swaps (paid_A ! n) (s_A n)) (q)"
by auto
also have "… < length xs'" using index_less_size_conv by (auto simp: queryinlist)
finally have iset: "i < length xs'" .
have "index xs' (xs' ! i) = i" apply(rule index_nth_id)
using iset by(auto)
with 2 show ?case by auto
qed
have aaa23: "inj_on (λi. xs'!i) {i. i < k'}"
apply(rule inj_on_nth)
apply(simp)
apply(simp) proof (safe, goal_cases)
case (1 i)
then have "i < index xs' (q)" by auto
also have "… < length xs'" using index_less_size_conv by (auto simp: queryinlist)
also have "… = length init" by auto
finally show " i < length init" .
qed
have aa3: "{xs'!i | i. i < k'} = (λi. xs'!i) ` {i. i < k'}" by auto
have aa4: "{(q,b)|b. index xs' b < k'} = (λb. (q,b)) ` {b. index xs' b < k'}" by auto
have unbelievable: "{i::nat. i < k'} = {..<k'}" by auto
have aadad: "inj_on (λb. (q,b)) {b. index xs' b < k'}"
unfolding inj_on_def by(simp)
have "(∑(x,y)∈{(q,b)|b. index xs' b < k'}. (if b!(index init y) then 2::real else 1))
= (∑y∈{y. index xs' y < k'}. (if b!(index init y) then 2::real else 1))"
proof -
have "(∑(x,y)∈{(q,b)|b. index xs' b < k'}. (if b!(index init y) then 2::real else 1))
= (∑(x,y)∈ (λb. (q,b)) ` {b. index xs' b < k'}. (if b!(index init y) then 2::real else 1))" using aa4 by simp
also have "… = (∑z∈ (λb. (q,b)) ` {b. index xs' b < k'}. (if b!(index init (snd z)) then 2::real else 1))" by (simp add: split_def)
also have "… = (∑z∈{b. index xs' b < k'}. (if b!(index init (snd ((λb. (q,b)) z))) then 2::real else 1))"
apply(simp only: sum.reindex[OF aadad]) by auto
also have "… = (∑y∈{y. index xs' y < k'}. (if b!(index init y) then 2::real else 1))" by auto
finally show ?thesis .
qed
also have "… = (∑y∈{xs'!i | i. i < k'}. (if b!(index init y) then 2::real else 1))" using sameset by auto
also have "… = (∑y∈(λi. xs'!i) ` {i. i < k'}. (if b!(index init y) then 2::real else 1))" using aa3 by simp
also have "… = (∑y∈{i::nat. i < k'}. (if b!(index init (xs'!y)) then 2::real else 1))"
using sum.reindex[OF aaa23] by simp
also have E3: "… = (∑j::nat<k'. (if b!(index init (xs'!j)) then 2::real else 1))"
using unbelievable by auto
finally have bb: "(∑(x,y)∈{(q,b)|b. index xs' b < k'}. (if b!(index init y) then 2::real else 1))
= (∑j<k'. (if b!(index init (xs'!j)) then 2::real else 1))" .
have "A ≤ (∑j<k'. (if b!(index init (xs'!j)) then 2::real else 1))"
using aa bb by linarith
then show "A
≤ (if b!(index init q) then k-k' else (∑j<k'. (if b!(index init (xs'!j)) then 2::real else 1)))"
using False by auto
next
case True
then have samesame: "ys' = ys" unfolding ys'_def step_def by auto
have setxsbleibt: "set xs'' = set init" by auto
have whatisk': "k' = index xs'' q" apply(simp)
apply(rule mtf2_q_after[symmetric]) using queryinlist by auto
have "(Inv ys' xs'')-(Inv ys xs')
= {(x,y). x < y in ys ∧ y < x in xs'' ∧ ~ y < x in xs'}"
unfolding Inv_def using samesame by auto
also have
"… ⊆ {(xs'!i,q)|i. i∈{k'..<k}}"
apply(clarify)
proof
fix a b
assume 1: "a < b in ys"
and 2: "b < a in xs''"
and 3: "¬ b < a in xs'"
then have anb: "a ≠ b"
using no_before_inI by(force)
have a: "a ∈ set init"
and b: "b ∈ set init"
using before_in_setD1[OF 1] before_in_setD2[OF 1] by auto
with anb 3 have 3: "a < b in xs'"
by (simp add: not_before_in)
note all= anb 1 2 3 a b
have bq: "b=q" apply(rule swapped_by_mtf2[where xs="xs'" and x=a])
using queryinlist apply(simp_all add: all)
using all(4) apply(simp)
using all(3) apply(simp) done
note mine=mtf2_backwards_effect3[THEN conjunct1]
from bq have "q < a in xs''" using 2 by auto
then have "(k' < index xs'' a ∧ a ∈ set xs'')"
unfolding before_in_def
using whatisk' by auto
then have low : "k' ≤ index xs' a"
unfolding whatisk'
unfolding xs''_def
apply(subst mtf2_q_after)
apply(simp)
using queryinlist apply(simp)
apply(rule mine)
apply (simp add: queryinlist)
using bq b apply(simp)
apply(simp)
apply(simp del: xs'_def)
apply (metis "3" a before_in_def bq dp_xs'_init k'_def k_def max_0L mtf2_forward_beforeq nth_index whatisk' xs''_def)
using a by(simp)
from bq have "a < q in xs'" using 3 by auto
then have up: "(index xs' a < k )"
unfolding before_in_def by auto
from a have "a ∈ set xs'" by simp
then have aa: "a = xs'!index xs' a" using nth_index by simp
have inset: "index xs' a ∈ {k'..<k}"
using low up by fastforce
from bq aa show "(a, b) = (xs' ! index xs' a, q) ∧ index xs' a ∈ {k'..<k}"
using inset by simp
qed
finally have a: "(Inv ys' xs'')-(Inv ys xs') ⊆ {(xs'!i,q)|i. i∈{k'..<k}}" (is "?M ⊆ ?UB") .
have card_of_UB: "card {(xs'!i,q)|i. i∈{k'..<k}} = k-k'"
proof -
have e: "fst ` ?UB = (%i. xs' ! i) ` {k'..<k}" by force
have "card ?UB = card (fst ` ?UB)"
apply(rule card_image[symmetric])
using inj_on_def by fastforce
also
have "… = card ((%i. xs' ! i) ` {k'..<k})"
by (simp only: e)
also
have "… = card {k'..<k}"
apply(rule card_image)
apply(rule inj_on_nth)
using k_inbounds by simp_all
also
have "… = k-k'" by auto
finally
show ?thesis .
qed
have flipit: "flip (index init q) b ! (index init q) = (~ (b) ! (index init q))" apply(rule flip_itself)
using queryinlist setinit by auto
have q: "{x∈?UB. snd x=q} = ?UB" by auto
have E0: "A = (∑(x,y)∈(Inv ys' xs'')-(Inv ys xs'). (if b'!(index init y) then 2::real else 1))" by auto
also have E1: "… ≤ (∑(z,y)∈?UB. if flip (index init q) (b) ! (index init y) then 2::real else 1)"
unfolding b'_def apply(rule sum_mono2[OF _ a])
by(simp_all add: split_def)
also have "… = (∑(z,y)∈{x∈?UB. snd x=q}. if flip (index init q) (b) ! (index init y) then 2::real else 1)" by(simp only: q)
also have "… = (∑z∈{x∈?UB. snd x=q}. if flip (index init q) (b) ! (index init (snd z)) then 2::real else 1)" by(simp add: split_def)
also have "… = (∑z∈{x∈?UB. snd x=q}. if flip (index init q) (b) ! (index init q) then 2::real else 1)" by simp
also have E2: "… = (∑z∈?UB. if flip (index init q) (b) ! (index init q) then 2::real else 1)" by(simp only: q)
also have E3: "… = (∑y∈?UB. 1)" using flipit True by simp
also have E4: "… = k-k'"
by(simp only: real_of_card[symmetric] card_of_UB)
finally have result: "A ≤ k-k'" .
with True show ?thesis by auto
qed
show "(∑(x,y)∈(Inv ys' xs''). (if b'!(index init y) then 2::real else 1)) - (∑(x,y)∈(Inv ys xs'). (if b!(index init y) then 2::real else 1)) ≤ ?ub2"
unfolding ub_free_def teilen[unfolded Δ_def A_def B_def C_def] using BC_absch A_absch using True
by auto
qed
from paid_ub have kl: "Φ⇩1 x ≤ Φ⇩0 x + ?paidUB" by auto
from free_ub have kl2: "Φ⇩2 x - ?ub2 ≤ Φ⇩1 x" using gis dis by auto
have iub_free: "I + ?ub2 = ub_free" by auto
from kl kl2 have "Φ⇩2 x - Φ⇩0 x ≤ ?ub2 + ?paidUB" by auto
then have "(cost x) + (Φ⇩2 x) - (Φ⇩0 x) ≤ k + 1 + I + ?ub2 + ?paidUB" using ub_cost_BIT by auto
then show ?case unfolding ub_free_def b_def by auto
qed
text "Approximation of the Term for Free exchanges"
have free_absch: "E(map_pmf (λx. (if (q) ∈ set init then (if (fst (snd x))!(index init q) then k-k'
else (∑j<k'. (if (fst (snd x))!(index init (xs'!j)) then 2::real else 1))) else 0)) D)
≤ 3/4 * k" (is "?EA ≤ ?absche")
proof (cases "(q) ∈ set init")
case False
then have "?EA = 0" by auto
then show ?thesis by auto
next
case True
note queryinlist=this
have "k-k' ≤ k" by auto
have "k' ≤ k" by auto
text "Transformation of the first term"
have qsn: "{index init q} ∪ {} ⊆ {0..<?l}" using setinit queryinlist by auto
have "{l::bool list. length l = ?l ∧ l!(index init q)}
= {xs. Ball {(index init q)} ((!) xs) ∧ (∀i∈{}. ¬ xs ! i) ∧ length xs = ?l}" by auto
then have "card {l::bool list. length l = ?l ∧ l!(index init q)}
= card {xs. Ball {index init q} ((!) xs) ∧ (∀i∈{}. ¬ xs ! i) ∧ length xs = length init} " by auto
also have "… = 2^(length init - card {index init q} - card {})"
apply(subst card2[of "{(index init q)}" "{}" "?l"]) using qsn by auto
finally have lulu: "card {l::bool list. length l = ?l ∧ l!(index init q)} = 2^(?l-1)" by auto
have "(∑x∈{l::bool list. length l = ?l ∧ l!(index init q)}. real(k-k'))
= (∑x∈{l::bool list. length l = ?l ∧ l!(index init q)}. k-k')" by auto
also have "… = (k-k')*2^(?l-1)" using lulu by simp
finally have absch1stterm: "(∑x∈{l::bool list. length l = ?l ∧ l!(index init q)}. real(k-k'))
= real((k-k')*2^(?l-1))" .
text "Transformation of the second term"
let ?S="{(xs'!j)|j. j<k'}"
from queryinlist have "q ∈ set (swaps (paid_A ! n) (s_A n))" by auto
then have "index (swaps (paid_A ! n) (s_A n)) q < length xs'" by auto
then have k'inbound: "k' < length xs'" by auto
{ fix x
have a: "{..<k'} = {j. j<k'}" by auto
have b: "?S = ((%j. xs'!j) ` {j. j<k'})" by auto
have "(∑j<k'. (λt. (if x!(index init t) then 2::real else 1)) (xs'!j))
= sum ((λt. (if x!(index init t) then 2::real else 1)) o (%j. xs'!j)) {..<k'}"
by(auto)
also have "… = sum ((λt. (if x!(index init t) then 2::real else 1)) o (%j. xs'!j)) {j. j<k'}"
by (simp only: a)
also have "… = sum (λt. (if x!(index init t) then 2::real else 1)) ((%j. xs'!j) ` {j. j<k'})"
apply(rule sum.reindex[symmetric])
apply(rule inj_on_nth)
using k'inbound by(simp_all)
finally have "(∑j<k'. (λt. (if x!(index init t) then 2::real else 1)) (xs'!j))
= (∑j∈?S. (λt. (if x!(index init t) then 2 else 1)) j)" using b by simp
} note reindex=this
have identS: "?S = set (take k' xs')"
proof -
have "index (swaps (paid_A ! n) (s_A n)) (q) ≤ length (swaps (paid_A ! n) (s_A n))"
by (rule index_le_size)
then have kxs': "k' ≤ length xs'" by simp
have "?S = (!) xs' ` {0..<k'}" by force
also have "… = set (take k' xs')" apply(rule nth_image) by(rule kxs')
finally show "?S = set (take k' xs')" .
qed
have distinctS: "distinct (take k' xs')" using distinct_take identS by simp
have lengthS: "length (take k' xs') = k'" using length_take k'inbound by simp
from distinct_card[OF distinctS] lengthS have "card (set (take k' xs')) = k'" by simp
then have cardS: "card ?S = k'" using identS by simp
have a: "?S ⊆ set xs'" using set_take_subset identS by metis
then have Ssubso: "(index init) ` ?S ⊆ {0..<?l}" using setinit by auto
from a have s_subst_init: "?S ⊆ set init" by auto
note index_inj_on_S=subset_inj_on[OF inj_on_index[of "init"] s_subst_init]
have l: "xs'!k = q" unfolding k_def apply(rule nth_index) using queryinlist by(auto)
have "xs'!k ∉ set (take k' xs')"
apply(rule index_take) using l by simp
then have requestnotinS: "(q) ∉ ?S" using l identS by simp
then have indexnotin: "index init q ∉ (index init) ` ?S"
using index_inj_on_S s_subst_init by auto
have lua: "{l. length l = ?l ∧ ~l!(index init q)}
= {xs. (∀i∈{}. xs ! i) ∧ (∀i∈{index init q}. ¬ xs ! i) ∧ length xs = ?l}" by auto
from k'inbound have k'inbound2: "Suc k' ≤ length init" using Suc_le_eq by auto
have "(∑x∈{l::bool list. length l = ?l ∧ ~l!(index init q)}. (∑j<k'. (if x!(index init (xs'!j)) then 2::real else 1)))
= (∑x∈{l. length l = ?l ∧ ~l!(index init q)}. (∑j∈?S. (λt. (if x!(index init t) then 2 else 1)) j))"
using reindex by auto
also
have "… = (∑x∈{xs. (∀i∈{}. xs ! i) ∧ (∀i∈{index init q}. ¬ xs ! i) ∧ length xs = ?l}. (∑j∈?S. (λt. (if x!(index init t) then 2 else 1)) j))"
using lua by auto
also
have "… = (∑x∈{xs. (∀i∈{}. xs ! i) ∧ (∀i∈{index init q}. ¬ xs ! i) ∧ length xs = ?l}. (∑j∈(index init) ` ?S. (λt. (if x!t then 2 else 1)) j))"
proof -
{ fix x
have "(∑j∈?S. (λt. (if x!(index init t) then 2 else 1)) j)
= (∑j∈(index init) ` ?S. (λt. (if x!t then 2 else 1)) j)"
apply(simp only: sum.reindex[OF index_inj_on_S, where g="(%j. if x ! j then 2 else 1)"])
by(simp)
} note a=this
show ?thesis by(simp only: a)
qed
also
have "… = 3 / 2 * real (card ?S) * 2 ^ (?l - card {} - card {q})"
apply(subst Expactation2or1)
apply(simp)
apply(simp)
apply(simp)
apply(simp only: card_image index_inj_on_S cardS ) apply(simp add: k'inbound2 del: k'_def)
using indexnotin apply simp
apply(simp)
using Ssubso queryinlist apply(simp)
apply(simp only: card_image[OF index_inj_on_S]) by simp
finally have "(∑x∈{l. length l = ?l ∧ ¬ l ! (index init q)}. ∑j<k'. if x ! (index init (xs' ! j)) then 2 else 1)
= 3 / 2 * real (card ?S) * 2 ^ (?l - card {} - card {q}) " .
also
have "3 / 2 * real (card ?S) * 2 ^ (?l - card {} - card {q}) = (3/2) * (real (k')) * 2 ^ (?l - 1)" using cardS by auto
finally have absch2ndterm: " (∑x∈{l. length l = ?l ∧ ¬ l ! (index init q)}.
∑j<k'. if x !(index init (xs' ! j)) then 2 else 1) =
3 / 2 * real (k') * 2 ^ (?l - 1) " .
text "Equational transformations to the goal"
have cardonebitset: "card {l::bool list. length l = ?l ∧ l!(index init q)} = 2^(?l-1)" using lulu by auto
have splitie: "{l::bool list. length l = ?l}
= {l::bool list. length l = ?l ∧ l!(index init q)} ∪ {l::bool list. length l = ?l ∧ ~l!(index init q)}"
by auto
have interempty: "{l::bool list. length l = ?l ∧ l!(index init q)} ∩ {l::bool list. length l = ?l ∧ ~l!(index init q)}
= {}" by auto
have fa: "finite {l::bool list. length l = ?l ∧ l!(index init q)}" using bitstrings_finite by auto
have fb: "finite {l::bool list. length l = ?l ∧ ~l!(index init q)}" using bitstrings_finite by auto
{ fix f :: "bool list ⇒ real"
have "(∑x∈{l::bool list. length l = ?l}. f x)
= (∑x∈{l::bool list. length l = ?l ∧ l!(index init q)} ∪ {l::bool list. length l = ?l ∧ ~l!(index init q)}. f x)" by(simp only: splitie)
also have "…
= (∑x∈{l::bool list. length l = ?l ∧ l!(index init q)}. f x)
+ (∑x∈{l::bool list. length l = ?l ∧ ~l!(index init q)}. f x)
- (∑x∈{l::bool list. length l = ?l ∧ l!(index init q)} ∩ {l::bool list. length l = ?l ∧ ~l!(index init q)}. f x)"
using sum_Un[OF fa fb, of "f"] by simp
also have "… = (∑x∈{l::bool list. length l = ?l ∧ l!(index init q)}. f x)
+ (∑x∈{l::bool list. length l = ?l ∧ ~l!(index init q)}. f x)" by(simp add: interempty)
finally have "sum f {l. length l = length init} =
sum f {l. length l = length init ∧ l ! (index init q)} + sum f {l. length l = length init ∧ ¬ l ! (index init q)}" .
} note darfstsplitten=this
have E1: "E(map_pmf (λx. (if (fst (snd x))!(index init q) then real(k-k') else (∑j<k'. (if (fst (snd x))!(index init (xs'!j)) then 2::real else 1)))) D)
= E(map_pmf (λx. (if x!(index init q) then real(k-k') else (∑j<k'. (if x!(index init (xs'!j)) then 2::real else 1)))) (map_pmf (fst ∘ snd) D))"
proof -
have triv: "⋀x. (fst ∘ snd) x = fst (snd x)" by simp
have "E((map_pmf (λx. (if (fst (snd x))!(index init q) then real(k-k') else (∑j<k'. (if (fst (snd x))!index init (xs'!j) then 2::real else 1))))) D)
= E(map_pmf (λx. ((λy. (if y!(index init q) then real(k-k') else (∑j<k'. (if y!index init (xs'!j) then 2::real else 1)))) ∘ (fst ∘ snd)) x) D)"
apply(auto simp: comp_assoc) by (simp only: triv)
also have "… = E((map_pmf (λx. (if x!(index init q) then real(k-k') else (∑j<k'. (if x!index init (xs'!j) then 2::real else 1)))) ∘ (map_pmf (fst ∘ snd))) D)"
using map_pmf_compose by metis
also have "… = E(map_pmf (λx. (if x!(index init q) then real(k-k') else (∑j<k'. (if x!index init (xs'!j) then 2::real else 1)))) (map_pmf (fst ∘ snd) D))" by auto
finally show ?thesis .
qed
also
have E2: "… = E(map_pmf (λx. (if x!(index init q) then real(k-k') else (∑j<k'. (if x!(index init (xs'!j)) then 2::real else 1)))) (bv ?l))"
using config_n_bv[of init _] by auto
also
let ?insf="(λx. (if x!(index init q) then k-k' else (∑j<k'. (if x!(index init (xs'!j)) then 2::real else 1))))"
have E3: "… = (∑x∈(set_pmf (bv ?l)). (?insf x) * pmf (bv ?l) x)"
by (subst E_finite_sum_fun) (auto simp: bv_finite mult_ac)
also
have "… = (∑x∈{l::bool list. length l = ?l}. (?insf x) * pmf (bv ?l) x)"
using bv_set by auto
also
have E4: "… = (∑x∈{l::bool list. length l = ?l}. (?insf x) * (1/2)^?l)"
by (simp add: list_pmf)
also
have "… = (∑x∈{l::bool list. length l = ?l}. (?insf x)) * ((1/2)^?l)"
by(simp only: sum_distrib_right[where r="(1/2)^?l"])
also
have E5: "… = ((1/2)^?l) *(∑x∈{l::bool list. length l = ?l}. (?insf x))"
by(auto)
also
have E6: "… = ((1/2)^?l) * ( (∑x∈{l::bool list. length l = ?l ∧ l!(index init q)}. ?insf x)
+ (∑x∈{l::bool list. length l = ?l ∧ ~l!(index init q)}. ?insf x)
)" using darfstsplitten by auto
also
have E7: "… = ((1/2)^?l) * ( (∑x∈{l::bool list. length l = ?l ∧ l!(index init q)}. ((λx. real(k-k'))) x)
+ (∑x∈{l::bool list. length l = ?l ∧ ~l!(index init q)}. ((λx. (∑j<k'. (if x!index init (xs'!j) then 2::real else 1)))) x)
)" by auto
finally have "E(map_pmf (λx. (if (fst (snd x))!(index init q) then real(k-k') else (∑j<k'. (if (fst (snd x))!(index init (xs'!j)) then 2::real else 1)))) D)
= ((1/2)^?l) * ( (∑x∈{l::bool list. length l = ?l ∧ l!(index init q)}. ((λx. real(k-k'))) x)
+ (∑x∈{l::bool list. length l = ?l ∧ ~l!(index init q)}. ((λx. (∑j<k'. (if x!(index init (xs'!j)) then 2::real else 1)))) x)
)" .
also
have "… = ((1/2)^?l) * ( (∑x∈{l::bool list. length l = ?l ∧ l!(index init q)}. real(k-k'))
+ (3/2)*(real (k'))*2^(?l-1)
)" by(simp only: absch2ndterm)
also
have E8: "… = ((1/2)^?l) * ( real((k-k')*2^(?l-1)) + (3/2)*(real (k'))*2^(?l-1))"
by(simp only: absch1stterm)
also have "… = ((1/2)^?l) * ( ( (k-k') + (k')*(3/2) ) * 2^(?l-1) )" apply(simp only: distrib_right) by simp
also have "… = ((1/2)^?l) * 2^(?l-1) * ( (k-k') + (k')*(3/2) )" by simp
also have "… = (((1::real)/2)^(Suc l')) * 2^(l') * ( real(k-k') + (k')*(3/2) )"
using lSuc by auto
also have E9: "… = (1/2) * ( real(k-k') + (k')*(3/2) )"
proof -
have "((1::real)/2)^l' * 2^l' = ((1::real)/2 * 2)^l' " by(rule power_mult_distrib[symmetric])
also have "... = 1" by auto
finally have "(((1::real)/2)^(Suc l'))* 2^l'=(1/2)" by auto
then show ?thesis by auto
qed
also have E10: "… ≤ (1/2) * ( (3/2)*(k-k') + (k')*(3/2) )" by auto
also have "… = (1/2) * ( (3/2)*(k-k'+(k')) )" by auto
also have "… = (1/2) * ( (3/2)*(k) )" by auto
also have E11: "… = (3/4)*(k )" by auto
finally show "E(map_pmf (λx. (if q ∈ set init then (if (fst (snd x))!(index init q) then real( k-k' ) else (∑j<k'. (if (fst (snd x))!index init (xs'!j) then 2::real else 1))) else 0 )) D)
≤ 3/4 * k " using True by simp
qed
text "Transformation of the Term for Paid Exchanges"
have paid_absch: "E(map_pmf (λx. (∑i<(length (paid_A!n)). (if (fst (snd x))!(gebub n i) then 2::real else 1) )) D) = 3/2 * (length (paid_A!n))"
proof -
{
fix i
assume inbound: "(index init i) < length init"
have "map_pmf (λxx. if fst (snd xx) ! (index init i) then 2::real else 1) D =
bind_pmf (map_pmf (fst ∘ snd) D) (λb. return_pmf (if b! index init i then 2::real else 1))"
unfolding map_pmf_def by(simp add: bind_assoc_pmf bind_return_pmf)
also have "… = bind_pmf (bv (length init)) (λb. return_pmf (if b! index init i then 2::real else 1))"
using config_n_bv[of init "take n qs"] by simp
also have "… = map_pmf (λyy. (if yy then 2 else 1)) ( map_pmf (λy. y!(index init i)) (bv (length init)))"
by (simp add: map_pmf_def bind_return_pmf bind_assoc_pmf)
also have "… = map_pmf (λyy. (if yy then 2 else 1)) (bernoulli_pmf (5 / 10))"
by (auto simp add: bv_comp_bernoulli[OF inbound])
finally have "map_pmf (λxx. if fst (snd xx) ! (index init i) then 2::real else 1) D =
map_pmf (λyy. if yy then 2::real else 1) (bernoulli_pmf (5 / 10)) " .
} note umform = this
have "E(map_pmf (λx. (∑i<(length (paid_A!n)). (if (fst (snd x))!(gebub n i) then 2::real else 1))) D) =
(∑i<(length (paid_A!n)). E(map_pmf ((λxx. (if (fst (snd xx))!(gebub n i) then 2::real else 1))) D))"
apply(subst E_linear_sum2)
using finite_config_BIT[OF dist_init] by(simp_all)
also have "… = (∑i<(length (paid_A!n)). E(map_pmf (λy. if y then 2::real else 1) (bernoulli_pmf (5 / 10))))" using umform gebub_def gebub_inBound[OF 31] by simp
also have "… = 3/2 * (length (paid_A!n))" by(simp add: E_bernoulli)
finally show "E(map_pmf (λx. (∑i<(length (paid_A!n)). (if (fst (snd x))!(gebub n i) then 2::real else 1))) D) = 3/2 * (length (paid_A!n))" .
qed
text "Combine the Results"
have costA_absch: "k+(length (paid_A!n)) + 1 = t_A n" unfolding k_def q_def c_A_def p_A_def t_A_def by (auto)
let ?yo= "(λx. (cost x) + (Φ⇩2 x) - (Φ⇩0 x))"
let ?yo2=" (λx. (k + 1) + (if (q)∈set init then (if (fst (snd x))!(index init q) then k-k'
else (∑j<k'. (if (fst (snd x))!(index init (xs'!j)) then 2::real else 1)) ) else 0)
+(∑i<(length (paid_A!n)). (if (fst (snd x))!(gebub n i) then 2 else 1)))"
have E0: "t_BIT n + Phi(n+1) - Phi n = E (map_pmf ?yo D) "
using inEreinziehn by auto
also have "… ≤ E(map_pmf ?yo2 D)"
apply(rule E_mono2) unfolding D_def
apply(fact finite_config_BIT[OF dist_init])
apply(fact ub_cost[unfolded D_def])
done
also have E2: "… = E(map_pmf (λx. k + 1::real) D)
+ (E(map_pmf (λx. (if (q)∈set init then (if (fst (snd x))!(index init q) then real(k-k') else (∑j<k'. (if (fst (snd x))!(index init (xs'!j)) then 2::real else 1)))else 0)) D)
+ E(map_pmf (λx. (∑i<(length (paid_A!n)). (if (fst (snd x))!(gebub n i) then 2::real else 1))) D))"
unfolding D_def apply(simp only: E_linear_plus2[OF finite_config_BIT[OF dist_init]]) by(auto simp: add.assoc)
also have E3: "… ≤ k + 1 + (3/4 * (real (k)) + (3/2 * real (length (paid_A!n))))" using paid_absch free_absch by auto
also have "… = k + (3/4 * (real k)) + 1 + 3/2 *(length (paid_A!n)) " by auto
also have "… = (1+3/4) * (real k) + 1 + 3/2 *(length (paid_A!n)) " by auto
also have E4: "… = 7/4*(real k) + 3/2 *(length (paid_A!n)) + 1 " by auto
also have "… ≤ 7/4*(real k) + 7/4 *(length (paid_A!n)) + 1" by auto
also have E5:"… = 7/4*(k+(length (paid_A!n))) + 1 " by auto
also have E6:"… = 7/4*(t_A n - (1::real)) + 1" using costA_absch by auto
also have "… = 7/4*(t_A n) - 7/4 + 1" by algebra
also have E7: "… = 7/4*(t_A n)- 3/4" by auto
finally show "t_BIT n + Phi(n+1) - Phi n ≤ (7 / 4) * t_A n - 3/4" .
qed
then show "t_BIT n + Phi(n + 1) - Phi n ≤ (7 / 4) * t_A n - 3/4" .
qed
subsubsection "Lift the Result to the Whole Request List"
lemma T_BIT_absch_le: assumes nqs: "n ≤ length qs"
shows "T_BIT n ≤ (7 / 4) * T_A n - 3/4*n"
unfolding T_BIT_def T_A_def
proof -
from potential2[of "Phi", OF phi0 phi_pos myub] nqs have
"sum t_BIT {..<n} ≤ (∑i<n. 7 / 4 * (t_A i) - 3 / 4)" by auto
also have "… = (∑i<n. 7 / 4 * real_of_int (t_A i)) - (∑i<n. (3/4))" by (rule sum_subtractf)
also have "… = (∑i<n. 7 / 4 * real_of_int (t_A i)) - (3/4)*(∑i<n. 1)" by simp
also have "… = (∑i<n. (7 / 4) * real_of_int (t_A i)) - (3/4)*n" by simp
also have "… = (7 / 4) * (∑i<n. real_of_int (t_A i)) - (3/4)*n" by (simp add: sum_distrib_left)
also have "… = (7 / 4) * real_of_int (∑i<n.(t_A i)) - (3/4)*n" by auto
finally show "sum t_BIT {..<n} ≤ 7 / 4 * real_of_int (sum t_A {..<n}) - (3/4)*n" by auto
qed
lemma T_BIT_absch: assumes nqs: "n ≤ length qs"
shows "T_BIT n ≤ (7 / 4) * T_A' n - 3/4*n"
using nqs T_BIT_absch_le[of n] T_A_A'_leq[of n] by auto
lemma T_A_nneg: "0 ≤ T_A n"
by(auto simp add: sum_nonneg T_A_def t_A_def c_A_def p_A_def)
lemma T_BIT_eq: "T_BIT (length qs) = T_on_rand BIT init qs"
unfolding T_BIT_def T_on_rand_as_sum using t_BIT_def by auto
corollary T_BIT_competitive: assumes "n ≤ length qs" and "init ≠ []" and "∀i<n. qs!i ∈ set init"
shows "T_BIT n ≤ ((7 / 4) - 3/(4 * size init)) * T_A' n"
proof cases
assume 0: "real_of_int(T_A' n) ≤ n * (size init)"
then have 1: "3/4*real_of_int(T_A' n) ≤ 3/4*(n * (size init))" by auto
have "T_BIT n ≤ (7 / 4) * T_A' n - 3/4*n" using T_BIT_absch[OF assms(1)] by auto
also have "… = ((7 / 4) * real_of_int(T_A' n)) - (3/4*(n * size init)) / size init"
using assms(2) by simp
also have "… ≤ ((7 / 4) * real_of_int(T_A' n)) - 3/4*T_A' n / size init"
by(rule diff_left_mono[OF divide_right_mono[OF 1]]) simp
also have "… = ((7 / 4) - 3/4 / size init) * T_A' n" by algebra
also have "… = ((7 / 4) - 3/(4 * size init)) * T_A' n" by simp
finally show ?thesis .
next
assume 0: "¬ real_of_int(T_A' n) ≤ n * (size init)"
have T_A'_nneg: "0 ≤ T_A' n" using T_A_nneg[of n] T_A_A'_leq[of n] assms(1) by auto
have "2 - 1 / size init ≥ 1" using assms(2)
by (auto simp add: field_simps neq_Nil_conv)
have " T_BIT n ≤ n * size init" using T_BIT_ub[OF assms(3)] by linarith
also have "… < real_of_int(T_A' n)" using 0 by linarith
also have "… ≤ ((7 / 4) - 3/4 / size init) * T_A' n" using assms(2) T_A'_nneg
by(auto simp add: mult_le_cancel_right1 field_simps neq_Nil_conv)
finally show ?thesis by simp
qed
lemma t_A'_t: "n < length qs ⟹ t_A' n = int (t (s_A' n) (qs!n) (acts ! n))"
by (simp add: t_A'_def t_def c_A'_def p_A'_def paid_A'_def len_acts split: prod.split)
lemma T_A'_eq_lem: "(∑i=0..<length qs. t_A' i) =
T (s_A' 0) (drop 0 qs) (drop 0 acts)"
proof(induction rule: zero_induct[of _ "size qs"])
case 1 thus ?case by (simp add: len_acts)
next
case (2 n)
show ?case
proof cases
assume "n < length qs"
thus ?case using 2
by(simp add: Cons_nth_drop_Suc[symmetric,where i=n] len_acts sum.atLeast_Suc_lessThan
t_A'_t free_A_def paid_A'_def)
next
assume "¬ n < length qs" thus ?case by (simp add: len_acts)
qed
qed
lemma T_A'_eq: "T_A' (length qs) = T init qs acts"
using T_A'_eq_lem by(simp add: T_A'_def atLeast0LessThan)
corollary BIT_competitive3: "init ≠ [] ⟹ ∀i<length qs. qs!i ∈ set init ⟹
T_BIT (length qs) ≤ ( (7/4) - 3 / (4 * length init)) * T init qs acts"
using order.refl T_BIT_competitive[of "length qs"] T_A'_eq by (simp add: of_int_of_nat_eq)
corollary BIT_competitive2: "init ≠ [] ⟹ ∀i<length qs. qs!i ∈ set init ⟹
T_on_rand BIT init qs ≤ ( (7/4) - 3 / (4 * length init)) * T init qs acts"
using BIT_competitive3 T_BIT_eq by auto
corollary BIT_absch_le: "init ≠ [] ⟹
T_on_rand BIT init qs ≤ (7 / 4) * (T init qs acts) - 3/4 * length qs"
using T_BIT_absch[of "length qs", unfolded T_A'_eq T_BIT_eq] by auto
end
subsubsection "Generalize Competitivness of BIT"
lemma setdi: "set xs = {0..<length xs} ⟹ distinct xs"
apply(rule card_distinct) by auto
theorem compet_BIT: assumes "init ≠ []" "distinct init" "set qs ⊆ set init"
shows "T_on_rand BIT init qs ≤ ( (7/4) - 3 / (4 * length init)) * T_opt init qs"
proof-
from assms(3) have 1: "∀i < length qs. qs!i ∈ set init" by auto
{ fix acts :: "answer list"
assume len: "length acts = length qs"
interpret BIT_Off acts qs init proof qed (auto simp: assms(2) len)
from BIT_competitive2[OF assms(1) 1] assms(1)
have "T_on_rand BIT init qs / ( (7/4) - 3 / (4 * length init)) ≤ real(T init qs acts)"
by(simp add: field_simps length_greater_0_conv[symmetric]
del: length_greater_0_conv) }
hence "T_on_rand BIT init qs / ( (7/4) - 3 / (4 * length init)) ≤ T_opt init qs"
apply(simp add: T_opt_def Inf_nat_def)
apply(rule LeastI2_wellorder)
using length_replicate[of "length qs" undefined] apply fastforce
apply auto
done
thus ?thesis using assms by(simp add: field_simps
length_greater_0_conv[symmetric] del: length_greater_0_conv)
qed
theorem compet_BIT4: assumes "init ≠ []" "distinct init"
shows "T_on_rand BIT init qs ≤ 7/4 * T_opt init qs"
proof-
{ fix acts :: "answer list"
assume len: "length acts = length qs"
interpret BIT_Off acts qs init proof qed (auto simp: assms(2) len)
from BIT_absch_le[OF assms(1)] assms(1)
have "(T_on_rand BIT init qs + 3 / 4 * length qs)/ (7/4) ≤ real(T init qs acts)"
by(simp add: field_simps length_greater_0_conv[symmetric]
del: length_greater_0_conv) }
hence "(T_on_rand BIT init qs + 3 / 4 * length qs)/ (7/4) ≤ T_opt init qs"
apply(simp add: T_opt_def Inf_nat_def)
apply(rule LeastI2_wellorder)
using length_replicate[of "length qs" undefined] apply fastforce
apply auto
done
thus ?thesis by(simp add: field_simps
length_greater_0_conv[symmetric] del: length_greater_0_conv)
qed
theorem compet_BIT_2:
"compet_rand BIT (7/4) {init. init ≠ [] ∧ distinct init}"
unfolding compet_rand_def
proof
fix init
assume "init ∈ {init. init ≠ [] ∧ distinct init }"
then have ne: "init ≠ []" and a: "distinct init" by auto
{
fix qs
assume "init ≠ []" and a: "distinct init"
then have "T_on_rand BIT init qs ≤ 7/4 * T_opt init qs"
using compet_BIT4[of init qs] by simp
}
with a ne show "∃b≥0. ∀qs. static init qs ⟶ T_on_rand BIT init qs ≤ (7 / 4) * (T_opt init qs) + b"
by auto
qed
end