(* Title: Competitive Analysis of BIT Author: Max Haslbeck *) 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]"]) ― ‹comment in a proof› 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 exchanges of A *) "free_A = map fst acts" definition paid_A' :: "nat list list" where (* paid exchanges of A' *) "paid_A' = map snd acts" definition paid_A :: "nat list list" where (* paid exchanges of A *) "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 (* BIT's cost in nth step *) "t_BIT n = T_on_rand_n BIT init qs n" definition T_BIT :: "nat ⇒ real" where (* BIT's cost in first n steps *) "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 of the potential function! *) 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" (* BIT A *) 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" (* position of the requested element in A's list *) define k' where [simp]: "k' = max 0 (k-free_A!n)" (* position where A moves the requested element to *) 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" (* ============================================ first we adress the paid exchanges paid cost of A: p_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 (* FIXME! can't occur! because it has already been filtered out! see: then have "False" using paidAnm_inbound apply(auto) using m_bd nqs by blast *) 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')" (* ys is BITs list, xs' is A's list after paid exchanges *) have ub_cost_BIT: "(cost x) ≤ k + 1 + I" proof (cases "(q) ∈ set init") case False (* cannot occur! ! ! OBSOLETE *) 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" (* ================================================ *) (* ================================================ *) (* second part: 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" (* 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 distinction on whether the bit of the requested element is set *) 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)" . (* approx for B *) 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 (* ========================================== central! calculations for A ========================================== *) 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 distinction on whether the requested element's bit is set *) case False from leninitys False have ya: "ys' = mtf2 (length ys) q ys" (* BIT moves q to front *) 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 (* BIT does nothing *) 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)(* unfolding xs'_def xs_def sledgehammer TODO: make this step readable by (metis "3" mtf2_q_after a before_in_def bq dp_xs'_init index_less_size_conv mtf2_forward_beforeq nth_index whatisk' xs''_def xs'_def xs_def) *) 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 (* rewrite from sum over indices of the list to sum over elements (thus indices of the bit vector) *) 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 (* rewrite to conform the syntax of Expactation2or1 *) 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 (* use Expactation2or1, and solve all the conditions *) 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 add: ) 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}) " . (* insert the cardinality of S*) 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)" using list_pmf by auto 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) (* from here it is only arithmetic ... *) 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 (* REFACTOR: the only place where I use lSuc , can I avoid it? yes, if ?l=0 then k=k'<?l impossible, perhaps I can insert that somehow ? *) 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 (* and one inequality *) 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 (* free_absch *) 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" (* cost of A *) 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) (* combine *) 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 (* arithmetic! *) also have "… = (1+3/4) * (real k) + 1 + 3/2 *(length (paid_A!n)) " by auto (* arithmetic! *) also have E4: "… = 7/4*(real k) + 3/2 *(length (paid_A!n)) + 1 " by auto (* arithmetic! *) also have "… ≤ 7/4*(real k) + 7/4 *(length (paid_A!n)) + 1" by auto (* arithmetic! *) 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