# Theory Inversion

section "List Inversion" theory Inversion imports "List-Index.List_Index" begin abbreviation "dist_perm xs ys ≡ distinct xs ∧ distinct ys ∧ set xs = set ys" definition before_in :: "'a ⇒ 'a ⇒ 'a list ⇒ bool" ("(_ </ _/ in _)" [55,55,55] 55) where "x < y in xs = (index xs x < index xs y ∧ y ∈ set xs)" definition Inv :: "'a list ⇒ 'a list ⇒ ('a * 'a) set" where "Inv xs ys = {(x,y). x < y in xs ∧ y < x in ys}" lemma before_in_setD1: "x < y in xs ⟹ x : set xs" by (metis index_conv_size_if_notin index_less before_in_def less_asym order_refl) lemma before_in_setD2: "x < y in xs ⟹ y : set xs" by (simp add: before_in_def) lemma not_before_in: "x : set xs ⟹ y : set xs ⟹ ¬ x < y in xs ⟷ y < x in xs ∨ x=y" by (metis index_eq_index_conv before_in_def less_asym linorder_neqE_nat) lemma before_in_irefl: "x < x in xs = False" by (meson before_in_setD2 not_before_in) lemma no_before_inI[simp]: "x < y in xs ⟹ (¬ y < x in xs) = True" by (metis before_in_setD1 not_before_in) lemma finite_Invs[simp]: "finite(Inv xs ys)" apply(rule finite_subset[where B = "set xs × set ys"]) apply(auto simp add: Inv_def before_in_def) apply(metis index_conv_size_if_notin index_less_size_conv less_asym)+ done lemma Inv_id[simp]: "Inv xs xs = {}" by(auto simp add: Inv_def before_in_def) lemma card_Inv_sym: "card(Inv xs ys) = card(Inv ys xs)" proof - have "Inv xs ys = (λ(x,y). (y,x)) ` Inv ys xs" by(auto simp: Inv_def) thus ?thesis by (metis card_image swap_inj_on) qed lemma Inv_tri_ineq: "dist_perm xs ys ⟹ dist_perm ys zs ⟹ Inv xs zs ⊆ Inv xs ys Un Inv ys zs" by(auto simp: Inv_def) (metis before_in_setD1 not_before_in) lemma card_Inv_tri_ineq: "dist_perm xs ys ⟹ dist_perm ys zs ⟹ card (Inv xs zs) ≤ card(Inv xs ys) + card (Inv ys zs)" using card_mono[OF _ Inv_tri_ineq[of xs ys zs]] by auto (metis card_Un_Int finite_Invs trans_le_add1) end

# Theory Swaps

(* Author: Tobias Nipkow *) section "Swapping Adjacent Elements in a List" theory Swaps imports Inversion begin text‹Swap elements at index ‹n› and @{term "Suc n"}:› definition "swap n xs = (if Suc n < size xs then xs[n := xs!Suc n, Suc n := xs!n] else xs)" lemma length_swap[simp]: "length(swap i xs) = length xs" by(simp add: swap_def) lemma swap_id[simp]: "Suc n ≥ size xs ⟹ swap n xs = xs" by(simp add: swap_def) lemma distinct_swap[simp]: "distinct(swap i xs) = distinct xs" by(simp add: swap_def) lemma swap_Suc[simp]: "swap (Suc n) (a # xs) = a # swap n xs" by(induction xs) (auto simp: swap_def) lemma index_swap_distinct: "distinct xs ⟹ Suc n < length xs ⟹ index (swap n xs) x = (if x = xs!n then Suc n else if x = xs!Suc n then n else index xs x)" by(auto simp add: swap_def index_swap_if_distinct) lemma set_swap[simp]: "set(swap n xs) = set xs" by(auto simp add: swap_def set_conv_nth nth_list_update) metis lemma nth_swap_id[simp]: "Suc i < length xs ⟹ swap i xs ! i = xs!(i+1)" by(simp add: swap_def) lemma before_in_swap: "dist_perm xs ys ⟹ Suc n < size xs ⟹ x < y in (swap n xs) ⟷ x < y in xs ∧ ¬ (x = xs!n ∧ y = xs!Suc n) ∨ x = xs!Suc n ∧ y = xs!n" by(simp add:before_in_def index_swap_distinct) (metis Suc_lessD Suc_lessI index_less_size_conv index_nth_id less_Suc_eq n_not_Suc_n nth_index) lemma Inv_swap: assumes "dist_perm xs ys" shows "Inv xs (swap n ys) = (if Suc n < size xs then if ys!n < ys!Suc n in xs then Inv xs ys ∪ {(ys!n, ys!Suc n)} else Inv xs ys - {(ys!Suc n, ys!n)} else Inv xs ys)" proof- have "length xs = length ys" using assms by (metis distinct_card) with assms show ?thesis by(simp add: Inv_def set_eq_iff) (metis before_in_def not_before_in before_in_swap) qed text‹Perform a list of swaps, from right to left:› abbreviation swaps where "swaps == foldr swap" lemma swaps_inv[simp]: "set (swaps sws xs) = set xs ∧ size(swaps sws xs) = size xs ∧ distinct(swaps sws xs) = distinct xs" by (induct sws arbitrary: xs) (simp_all add: swap_def) lemma swaps_eq_Nil_iff[simp]: "swaps acts xs = [] ⟷ xs = []" by(induction acts)(auto simp: swap_def) lemma swaps_map_Suc[simp]: "swaps (map Suc sws) (a # xs) = a # swaps sws xs" by(induction sws arbitrary: xs) auto lemma card_Inv_swaps_le: "distinct xs ⟹ card (Inv xs (swaps sws xs)) ≤ length sws" by(induction sws) (auto simp: Inv_swap card_insert_if card_Diff_singleton_if) lemma nth_swaps: "∀i∈set is. j < i ⟹ swaps is xs ! j = xs ! j" by(induction "is")(simp_all add: swap_def) lemma not_before0[simp]: "~ x < xs ! 0 in xs" apply(cases "xs = []") by(auto simp: before_in_def neq_Nil_conv) lemma before_id[simp]: "⟦ distinct xs; i < size xs; j < size xs ⟧ ⟹ xs ! i < xs ! j in xs ⟷ i < j" by(simp add: before_in_def index_nth_id) lemma before_swaps: "⟦ distinct is; ∀i∈set is. Suc i < size xs; distinct xs; i ∉ set is; i < j; j < size xs ⟧ ⟹ swaps is xs ! i < swaps is xs ! j in xs" apply(induction "is" arbitrary: i j) apply simp apply(auto simp: swap_def nth_list_update) done lemma card_Inv_swaps: "⟦ distinct is; ∀i∈set is. Suc i < size xs; distinct xs ⟧ ⟹ card(Inv xs (swaps is xs)) = length is" apply(induction "is") apply simp apply(simp add: Inv_swap before_swaps card_insert_if) apply(simp add: Inv_def) done lemma swaps_eq_nth_take_drop: "i < length xs ⟹ swaps [0..<i] xs = xs!i # take i xs @ drop (Suc i) xs" apply(induction i arbitrary: xs) apply (auto simp add: neq_Nil_conv swap_def drop_update_swap take_Suc_conv_app_nth Cons_nth_drop_Suc[symmetric]) done lemma index_swaps_size: "distinct s ⟹ index s q ≤ index (swaps sws s) q + length sws" apply(induction sws arbitrary: s) apply simp apply (fastforce simp: swap_def index_swap_if_distinct index_nth_id) done lemma index_swaps_last_size: "distinct s ⟹ size s ≤ index (swaps sws s) (last s) + length sws + 1" apply(cases "s = []") apply simp using index_swaps_size[of s "last s" sws] by simp end

# Theory On_Off

(* Author: Tobias Nipkow *) section "Deterministic Online and Offline Algorithms" theory On_Off imports Complex_Main begin type_synonym ('s,'r,'a) alg_off = "'s ⇒ 'r list ⇒ 'a list" type_synonym ('s,'is,'r,'a) alg_on = "('s ⇒ 'is) * ('s * 'is ⇒ 'r ⇒ 'a * 'is)" locale On_Off = fixes step :: "'state ⇒ 'request ⇒ 'answer ⇒ 'state" fixes t :: "'state ⇒ 'request ⇒ 'answer ⇒ nat" fixes wf :: "'state ⇒ 'request list ⇒ bool" begin fun T :: "'state ⇒ 'request list ⇒ 'answer list ⇒ nat" where "T s [] [] = 0" | "T s (r#rs) (a#as) = t s r a + T (step s r a) rs as" definition Step :: "('state , 'istate, 'request, 'answer)alg_on ⇒ 'state * 'istate ⇒ 'request ⇒ 'state * 'istate" where "Step A s r = (let (a,is') = snd A s r in (step (fst s) r a, is'))" fun config' :: "('state,'is,'request,'answer) alg_on ⇒ ('state*'is) ⇒ 'request list ⇒ ('state * 'is)" where "config' A s [] = s" | "config' A s (r#rs) = config' A (Step A s r) rs" lemma config'_snoc: "config' A s (rs@[r]) = Step A (config' A s rs) r" apply(induct rs arbitrary: s) by simp_all lemma config'_append2: "config' A s (xs@ys) = config' A (config' A s xs) ys" apply(induct xs arbitrary: s) by simp_all lemma config'_induct: "P (fst init) ⟹ (⋀s q a. P s ⟹ P (step s q a)) ⟹ P (fst (config' A init rs))" apply (induct rs arbitrary: init) by(simp_all add: Step_def split: prod.split) abbreviation config where "config A s0 rs == config' A (s0, fst A s0) rs" lemma config_snoc: "config A s (rs@[r]) = Step A (config A s rs) r" using config'_snoc by metis lemma config_append: "config A s (xs@ys) = config' A (config A s xs) ys" using config'_append2 by metis lemma config_induct: "P s0 ⟹ (⋀s q a. P s ⟹ P (step s q a)) ⟹ P (fst (config A s0 qs))" using config'_induct[of P "(s0, fst A s0)" ] by auto fun T_on' :: "('state,'is,'request,'answer) alg_on ⇒ ('state*'is) ⇒ 'request list ⇒ nat" where "T_on' A s [] = 0" | "T_on' A s (r#rs) = (t (fst s) r (fst (snd A s r))) + T_on' A (Step A s r) rs" lemma T_on'_append: "T_on' A s (xs@ys) = T_on' A s xs + T_on' A (config' A s xs) ys" apply(induct xs arbitrary: s) by simp_all abbreviation T_on'' :: "('state,'is,'request,'answer) alg_on ⇒ 'state ⇒ 'request list ⇒ nat" where "T_on'' A s rs == T_on' A (s,fst A s) rs" lemma T_on_append: "T_on'' A s (xs@ys) = T_on'' A s xs + T_on' A (config A s xs) ys" by(rule T_on'_append) abbreviation "T_on_n A s0 xs n == T_on' A (config A s0 (take n xs)) [xs!n]" lemma T_on__as_sum: "T_on'' A s0 rs = sum (T_on_n A s0 rs) {..<length rs} " apply(induct rs rule: rev_induct) by(simp_all add: T_on'_append nth_append) fun off2 :: "('state,'is,'request,'answer) alg_on ⇒ ('state * 'is,'request,'answer) alg_off" where "off2 A s [] = []" | "off2 A s (r#rs) = fst (snd A s r) # off2 A (Step A s r) rs" abbreviation off :: "('state,'is,'request,'answer) alg_on ⇒ ('state,'request,'answer) alg_off" where "off A s0 ≡ off2 A (s0, fst A s0)" abbreviation T_off :: "('state,'request,'answer) alg_off ⇒ 'state ⇒ 'request list ⇒ nat" where "T_off A s0 rs == T s0 rs (A s0 rs)" abbreviation T_on :: "('state,'is,'request,'answer) alg_on ⇒ 'state ⇒ 'request list ⇒ nat" where "T_on A == T_off (off A)" lemma T_on_on': "T_off (λs0. (off2 A (s0, x))) s0 qs = T_on' A (s0,x) qs" apply(induct qs arbitrary: s0 x) by(simp_all add: Step_def split: prod.split) lemma T_on_on'': "T_on A s0 qs = T_on'' A s0 qs" using T_on_on'[where x="fst A s0", of s0 qs A] by(auto) lemma T_on_as_sum: "T_on A s0 rs = sum (T_on_n A s0 rs) {..<length rs} " using T_on__as_sum T_on_on'' by metis definition T_opt :: "'state ⇒ 'request list ⇒ nat" where "T_opt s rs = Inf {T s rs as | as. size as = size rs}" definition compet :: "('state,'is,'request,'answer) alg_on ⇒ real ⇒ 'state set ⇒ bool" where "compet A c S = (∀s∈S. ∃b ≥ 0. ∀rs. wf s rs ⟶ real(T_on A s rs) ≤ c * T_opt s rs + b)" lemma length_off[simp]: "length(off2 A s rs) = length rs" by (induction rs arbitrary: s) (auto split: prod.split) lemma compet_mono: assumes "compet A c S0" and "c ≤ c'" shows "compet A c' S0" proof (unfold compet_def, auto) let ?compt = "λs0 rs b (c::real). T_on A s0 rs ≤ c * T_opt s0 rs + b" fix s0 assume "s0 ∈ S0" with assms(1) obtain b where "b ≥ 0" and 1: "∀rs. wf s0 rs ⟶ ?compt s0 rs b c" by(auto simp: compet_def) have "∀rs. wf s0 rs ⟶ ?compt s0 rs b c'" proof safe fix rs assume wf: "wf s0 rs" from 1 wf have "?compt s0 rs b c" by blast thus "?compt s0 rs b c'" using 1 mult_right_mono[OF assms(2) of_nat_0_le_iff[of "T_opt s0 rs"]] by arith qed thus "∃b≥0. ∀rs. wf s0 rs ⟶ ?compt s0 rs b c'" using ‹b≥0› by(auto) qed lemma competE: fixes c :: real assumes "compet A c S0" "c ≥ 0" "∀s0 rs. size(aoff s0 rs) = length rs" "s0∈S0" shows "∃b≥0. ∀rs. wf s0 rs ⟶ T_on A s0 rs ≤ c * T_off aoff s0 rs + b" proof - from assms(1,4) obtain b where "b≥0" and 1: "∀rs. wf s0 rs ⟶ T_on A s0 rs ≤ c * T_opt s0 rs + b" by(auto simp add: compet_def) { fix rs assume "wf s0 rs" then have 2: "real(T_on A s0 rs) ≤ c * Inf {T s0 rs as | as. size as = size rs} + b" (is "_ ≤ _ * real(Inf ?T) + _") using 1 by(auto simp add: T_opt_def) have "Inf ?T ≤ T_off aoff s0 rs" using assms(3) by (intro cInf_lower) auto from mult_left_mono[OF of_nat_le_iff[THEN iffD2, OF this] assms(2)] have "T_on A s0 rs ≤ c * T_off aoff s0 rs + b" using 2 by arith } thus ?thesis using ‹b≥0› by(auto simp: compet_def) qed end end

# Theory Prob_Theory

(* Title: Definition of Expectation and Distribution of uniformly distributed bit vectors Author: Max Haslbeck *) section "Probability Theory" theory Prob_Theory imports "HOL-Probability.Probability" begin lemma integral_map_pmf[simp]: fixes f::"real ⇒ real" shows "(∫x. f x ∂(map_pmf g M)) = (∫x. f (g x) ∂M)" unfolding map_pmf_rep_eq using integral_distr[of g "(measure_pmf M)" "(count_space UNIV)" f] by auto subsection "function ‹E›" definition E :: "real pmf ⇒ real" where "E M = (∫x. x ∂ measure_pmf M)" translations "∫ x. f ∂M" <= "CONST lebesgue_integral M (λx. f)" notation (latex output) E ("E[_]" [1] 100) lemma E_const[simp]: "E (return_pmf a) = a" unfolding E_def unfolding return_pmf.rep_eq by (simp add: integral_return) lemma E_null[simp]: "E (return_pmf 0) = 0" by auto lemma E_finite_sum: "finite (set_pmf X) ⟹ E X = (∑x∈(set_pmf X). pmf X x * x)" unfolding E_def by (subst integral_measure_pmf) simp_all lemma E_of_const: "E(map_pmf (λx. y) (X::real pmf)) = y" by auto lemma E_nonneg: shows "(∀x∈set_pmf X. 0≤ x) ⟹ 0 ≤ E X" unfolding E_def using integral_nonneg by (simp add: AE_measure_pmf_iff integral_nonneg_AE) lemma E_nonneg_fun: fixes f::"'a⇒real" shows "(∀x∈set_pmf X. 0≤f x) ⟹ 0 ≤ E (map_pmf f X)" using E_nonneg by auto lemma E_cong: fixes f::"'a ⇒ real" shows "finite (set_pmf X) ⟹ (∀x∈ set_pmf X. (f x) = (u x)) ⟹ E (map_pmf f X) = E (map_pmf u X)" unfolding E_def integral_map_pmf apply(rule integral_cong_AE) apply(simp add: integrable_measure_pmf_finite)+ by (simp add: AE_measure_pmf_iff) lemma E_mono3: fixes f::"'a ⇒ real" shows " integrable (measure_pmf X) f ⟹ integrable (measure_pmf X) u ⟹ (∀x∈ set_pmf X. (f x) ≤ (u x)) ⟹ E (map_pmf f X) ≤ E (map_pmf u X)" unfolding E_def integral_map_pmf apply(rule integral_mono_AE) by (auto simp add: AE_measure_pmf_iff) lemma E_mono2: fixes f::"'a ⇒ real" shows "finite (set_pmf X) ⟹ (∀x∈ set_pmf X. (f x) ≤ (u x)) ⟹ E (map_pmf f X) ≤ E (map_pmf u X)" unfolding E_def integral_map_pmf apply(rule integral_mono_AE) apply(simp add: integrable_measure_pmf_finite)+ by (simp add: AE_measure_pmf_iff) lemma E_linear_diff2: "finite (set_pmf A) ⟹ E (map_pmf f A) - E (map_pmf g A) = E (map_pmf (λx. (f x) - (g x)) A)" unfolding E_def integral_map_pmf apply(rule Bochner_Integration.integral_diff[of "measure_pmf A" f g, symmetric]) by (simp_all add: integrable_measure_pmf_finite) lemma E_linear_plus2: "finite (set_pmf A) ⟹ E (map_pmf f A) + E (map_pmf g A) = E (map_pmf (λx. (f x) + (g x)) A)" unfolding E_def integral_map_pmf apply(rule Bochner_Integration.integral_add[of "measure_pmf A" f g, symmetric]) by (simp_all add: integrable_measure_pmf_finite) lemma E_linear_sum2: "finite (set_pmf D) ⟹ E(map_pmf (λx. (∑i<up. f i x)) D) = (∑i<(up::nat). E(map_pmf (f i) D))" unfolding E_def integral_map_pmf apply(rule Bochner_Integration.integral_sum) by (simp add: integrable_measure_pmf_finite) lemma E_linear_sum_allg: "finite (set_pmf D) ⟹ E(map_pmf (λx. (∑i∈ A. f i x)) D) = (∑i∈ (A::'a set). E(map_pmf (f i) D))" unfolding E_def integral_map_pmf apply(rule Bochner_Integration.integral_sum) by (simp add: integrable_measure_pmf_finite) lemma E_finite_sum_fun: "finite (set_pmf X) ⟹ E (map_pmf f X) = (∑x∈set_pmf X. pmf X x * f x)" proof - assume finite: "finite (set_pmf X)" have "E (map_pmf f X) = (∫x. f x ∂measure_pmf X)" unfolding E_def by auto also have "… = (∑x∈set_pmf X. pmf X x * f x)" by (subst integral_measure_pmf) (auto simp add: finite) finally show ?thesis . qed lemma E_bernoulli: "0≤p ⟹ p≤1 ⟹ E (map_pmf f (bernoulli_pmf p)) = p*(f True) + (1-p)*(f False)" unfolding E_def by (auto) subsection "function ‹bv›" fun bv:: "nat ⇒ bool list pmf" where "bv 0 = return_pmf []" | "bv (Suc n) = do { (xs::bool list) ← bv n; (x::bool) ← (bernoulli_pmf 0.5); return_pmf (x#xs) }" lemma bv_finite: "finite (bv n)" by (induct n) auto lemma len_bv_n: "∀xs ∈ set_pmf (bv n). length xs = n" apply(induct n) by auto lemma bv_set: "set_pmf (bv n) = {x::bool list. length x = n}" proof (induct n) case (Suc n) then have "set_pmf (bv (Suc n)) = (⋃x∈{x. length x = n}. {True # x, False # x})" by(simp add: set_pmf_bernoulli UNIV_bool) also have "… = {x#xs| x xs. length xs = n}" by auto also have "… = {x. length x = Suc n} " using Suc_length_conv by fastforce finally show ?case . qed (simp) lemma len_not_in_bv: "length xs ≠ n ⟹ xs ∉ set_pmf (bv n)" by(auto simp: len_bv_n) lemma not_n_bv_0: "length xs ≠ n ⟹ pmf (bv n) xs = 0" by (simp add: len_not_in_bv pmf_eq_0_set_pmf) lemma bv_comp_bernoulli: "n < l ⟹ map_pmf (λy. y!n) (bv l) = bernoulli_pmf (5 / 10)" proof (induct n arbitrary: l) case 0 then obtain m where "l = Suc m" by (metis Suc_pred) then show "map_pmf (λy. y!0) (bv l) = bernoulli_pmf (5 / 10)" by (auto simp: map_pmf_def bind_return_pmf bind_assoc_pmf bind_return_pmf') next case (Suc n) then have "0 < l" by auto then obtain m where lsm: "l = Suc m" by (metis Suc_pred) with Suc(2) have nltm: "n < m" by auto from lsm have "map_pmf (λy. y ! Suc n) (bv l) = map_pmf (λx. x!n) (bind_pmf (bv m) (λt. (return_pmf t)))" by (auto simp: map_bind_pmf) also have "… = map_pmf (λx. x!n) (bv m)" by (auto simp: bind_return_pmf') also have "… = bernoulli_pmf (5 / 10)" by (auto simp add: Suc(1)[of m, OF nltm]) finally show ?case . qed lemma pmf_2elemlist: "pmf (bv (Suc 0)) ([x]) = pmf (bv 0) [] * pmf (bernoulli_pmf (5 / 10)) x" unfolding bv.simps(2)[where n=0] pmf_bind pmf_return apply (subst integral_measure_pmf[where A="{[]}"]) apply (auto) by (cases x) auto lemma pmf_moreelemlist: "pmf (bv (Suc n)) (x#xs) = pmf (bv n) xs * pmf (bernoulli_pmf (5 / 10)) x" unfolding bv.simps(2) pmf_bind pmf_return apply (subst integral_measure_pmf[where A="{xs}"]) apply auto apply (cases x) apply(auto) apply (meson indicator_simps(2) list.inject singletonD) apply (meson indicator_simps(2) list.inject singletonD) apply (cases x) by(auto) lemma list_pmf: "length xs = n ⟹ pmf (bv n) xs = (1 / 2)^n" proof(induct n arbitrary: xs) case 0 then have "xs = []" by auto then show "pmf (bv 0) xs = (1 / 2) ^ 0" by(auto) next case (Suc n xs) then obtain a as where split: "xs = a#as" by (metis Suc_length_conv) have "length as = n" using Suc(2) split by auto with Suc(1) have 1: "pmf (bv n) as = (1 / 2) ^ n" by auto from split pmf_moreelemlist[where n=n and x=a and xs=as] have "pmf (bv (Suc n)) xs = pmf (bv n) as * pmf (bernoulli_pmf (5 / 10)) a" by auto then have "pmf (bv (Suc n)) xs = (1 / 2) ^ n * 1 / 2" using 1 by auto then show "pmf (bv (Suc n)) xs = (1 / 2) ^ Suc n" by auto qed lemma bv_0_notlen: "pmf (bv n) xs = 0 ⟹ length xs ≠ n " by(auto simp: list_pmf) lemma "length xs > n ⟹ pmf (bv n) xs = 0" proof (induct n arbitrary: xs) case (Suc n xs) then obtain a as where split: "xs = a#as" by (metis Suc_length_conv Suc_lessE) have "length as > n" using Suc(2) split by auto with Suc(1) have 1: "pmf (bv n) as = 0" by auto from split pmf_moreelemlist[where n=n and x=a and xs=as] have "pmf (bv (Suc n)) xs = pmf (bv n) as * pmf (bernoulli_pmf (5 / 10)) a" by auto then have "pmf (bv (Suc n)) xs = 0 * 1 / 2" using 1 by auto then show "pmf (bv (Suc n)) xs = 0" by auto qed simp lemma map_hd_list_pmf: "map_pmf hd (bv (Suc n)) = bernoulli_pmf (5 / 10)" by (simp add: map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf') lemma map_tl_list_pmf: "map_pmf tl (bv (Suc n)) = bv n" by (simp add: map_pmf_def bind_assoc_pmf bind_return_pmf bind_return_pmf' ) subsection "function ‹flip›" fun flip :: "nat ⇒ bool list ⇒ bool list" where "flip _ [] = []" | "flip 0 (x#xs) = (¬x)#xs" | "flip (Suc n) (x#xs) = x#(flip n xs)" lemma flip_length[simp]: "length (flip i xs) = length xs" apply(induct xs arbitrary: i) apply(simp) apply(case_tac i) by(simp_all) lemma flip_out_of_bounds: "y ≥ length X ⟹ flip y X = X" apply(induct X arbitrary: y) proof - case (Cons X Xs) hence "y > 0" by auto with Cons obtain y' where y1: "y = Suc y'" and y2: "y' ≥ length Xs" by (metis Suc_pred' length_Cons not_less_eq_eq) then have "flip y (X # Xs) = X#(flip y' Xs)" by auto moreover from Cons y2 have "flip y' Xs = Xs" by auto ultimately show ?case by auto qed simp lemma flip_other: "y < length X ⟹ z < length X ⟹ z ≠ y ⟹ flip z X ! y = X ! y" apply(induct y arbitrary: X z) apply(simp) apply (metis flip.elims neq0_conv nth_Cons_0) proof (case_tac z, goal_cases) case (1 y X z) then obtain a as where "X=a#as" using length_greater_0_conv by (metis (full_types) flip.elims) with 1(5) show ?case by(simp) next case (2 y X z z') from 2 have 3: "z' ≠ y" by auto from 2(2) have "length X > 0" by auto then obtain a as where aas: "X = a#as" by (metis (full_types) flip.elims length_greater_0_conv) then have a: "flip (Suc z') X ! Suc y = flip z' as ! y" and b : "(X ! Suc y) = (as ! y)" by auto from 2(2) aas have 1: "y < length as" by auto from 2(3,5) aas have f2: "z' < length as" by auto note c=2(1)[OF 1 f2 3] have "flip z X ! Suc y = flip (Suc z') X ! Suc y" using 2 by auto also have "… = flip z' as ! y" by (rule a) also have "… = as ! y" by (rule c) also have "… = (X ! Suc y)" by (rule b[symmetric]) finally show "flip z X ! Suc y = (X ! Suc y)" . qed lemma flip_itself: "y < length X ⟹ flip y X ! y = (¬ X ! y)" apply(induct y arbitrary: X) apply(simp) apply (metis flip.elims nth_Cons_0 old.nat.distinct(2)) proof - fix y fix X::"bool list" assume iH: "(⋀X. y < length X ⟹ flip y X ! y = (¬ X ! y))" assume len: "Suc y < length X" from len have "y < length X" by auto from len have "length X > 0" by auto then obtain z zs where zzs: "X = z#zs" by (metis (full_types) flip.elims length_greater_0_conv) then have a: "flip (Suc y) X ! Suc y = flip y zs ! y" and b : "(¬ X ! Suc y) = (¬ zs ! y)" by auto from len zzs have "y < length zs" by auto note c=iH[OF this] from a b c show "flip (Suc y) X ! Suc y = (¬ X ! Suc y)" by auto qed lemma flip_twice: "flip i (flip i b) = b" proof (cases "i < length b") case True then have A: "i < length (flip i b)" by simp show ?thesis apply(simp add: list_eq_iff_nth_eq) apply(clarify) proof (goal_cases) case (1 j) then show ?case apply(cases "i=j") using flip_itself[OF A] flip_itself[OF True] apply(simp) using flip_other True 1 by auto qed qed (simp add: flip_out_of_bounds) lemma flipidiflip: "y < length X ⟹ e < length X ⟹ flip e X ! y = (if e=y then ~ (X ! y) else X ! y)" apply(cases "e=y") apply(simp add: flip_itself) by(simp add: flip_other) lemma bernoulli_Not: "map_pmf Not (bernoulli_pmf (1 / 2)) = (bernoulli_pmf (1 / 2))" apply(rule pmf_eqI) proof (case_tac i, goal_cases) case (1 i) then have "pmf (map_pmf Not (bernoulli_pmf (1 / 2))) i = pmf (map_pmf Not (bernoulli_pmf (1 / 2))) (Not False)" by auto also have "… = pmf (bernoulli_pmf (1 / 2)) False" apply (rule pmf_map_inj') apply(rule injI) by auto also have "… = pmf (bernoulli_pmf (1 / 2)) i" by auto finally show ?case . next case (2 i) then have "pmf (map_pmf Not (bernoulli_pmf (1 / 2))) i = pmf (map_pmf Not (bernoulli_pmf (1 / 2))) (Not True)" by auto also have "… = pmf (bernoulli_pmf (1 / 2)) True" apply (rule pmf_map_inj') apply(rule injI) by auto also have "… = pmf (bernoulli_pmf (1 / 2)) i" by auto finally show ?case . qed lemma inv_flip_bv: "map_pmf (flip i) (bv n) = (bv n)" proof(induct n arbitrary: i) case (Suc n i) note iH=this have "bind_pmf (bv n) (λx. bind_pmf (bernoulli_pmf (1 / 2)) (λxa. map_pmf (flip i) (return_pmf (xa # x)))) = bind_pmf (bernoulli_pmf (1 / 2)) (λxa .bind_pmf (bv n) (λx. map_pmf (flip i) (return_pmf (xa # x))))" by(rule bind_commute_pmf) also have "… = bind_pmf (bernoulli_pmf (1 / 2)) (λxa . bind_pmf (bv n) (λx. return_pmf (xa # x)))" proof (cases i) case 0 then have "bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. map_pmf (flip i) (return_pmf (xa # x)))) = bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. return_pmf ((¬ xa) # x)))" by auto also have "… = bind_pmf (bv n) (λx. bind_pmf (bernoulli_pmf (1 / 2)) (λxa. return_pmf ((¬ xa) # x)))" by(rule bind_commute_pmf) also have "… = bind_pmf (bv n) (λx. bind_pmf (map_pmf Not (bernoulli_pmf (1 / 2))) (λxa. return_pmf (xa # x)))" by(auto simp add: bind_map_pmf) also have "… = bind_pmf (bv n) (λx. bind_pmf (bernoulli_pmf (1 / 2)) (λxa. return_pmf (xa # x)))" by (simp only: bernoulli_Not) also have "… = bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. return_pmf (xa # x)))" by(rule bind_commute_pmf) finally show ?thesis . next case (Suc i') have "bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. map_pmf (flip i) (return_pmf (xa # x)))) = bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. return_pmf (xa # flip i' x)))" unfolding Suc by(simp) also have "… = bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (map_pmf (flip i') (bv n)) (λx. return_pmf (xa # x)))" by(auto simp add: bind_map_pmf) also have "… = bind_pmf (bernoulli_pmf (1 / 2)) (λxa. bind_pmf (bv n) (λx. return_pmf (xa # x)))" using iH[of "i'"] by simp finally show ?thesis . qed also have "… = bind_pmf (bv n) (λx. bind_pmf (bernoulli_pmf (1 / 2)) (λxa. return_pmf (xa # x)))" by(rule bind_commute_pmf) finally show ?case by(simp add: map_pmf_def bind_assoc_pmf) qed simp subsection "Example for pmf" definition "twocoins = do { x ← (bernoulli_pmf 0.4); y ← (bernoulli_pmf 0.5); return_pmf (x ∨ y) }" lemma experiment0_7: "pmf twocoins True = 0.7" unfolding twocoins_def unfolding pmf_bind pmf_return apply (subst integral_measure_pmf[where A="{True, False}"]) by auto subsection "Sum Distribution" definition "Sum_pmf p Da Db = (bernoulli_pmf p) ⤜ (%b. if b then map_pmf Inl Da else map_pmf Inr Db )" lemma b0: "bernoulli_pmf 0 = return_pmf False" apply(rule pmf_eqI) apply(case_tac i) by(simp_all) lemma b1: "bernoulli_pmf 1 = return_pmf True" apply(rule pmf_eqI) apply(case_tac i) by(simp_all) lemma Sum_pmf_0: "Sum_pmf 0 Da Db = map_pmf Inr Db" unfolding Sum_pmf_def apply(rule pmf_eqI) by(simp add: b0 bind_return_pmf) lemma Sum_pmf_1: "Sum_pmf 1 Da Db = map_pmf Inl Da" unfolding Sum_pmf_def apply(rule pmf_eqI) by(simp add: b1 bind_return_pmf) definition "Proj1_pmf D = map_pmf (%a. case a of Inl e ⇒ e) (cond_pmf D {f. (∃e. Inl e = f)})" lemma A: "(case_sum (λe. e) (λa. undefined)) (Inl e) = e" by(simp) lemma B: "inj (case_sum (λe. e) (λa. undefined))" oops lemma none: "p >0 ⟹ p < 1 ⟹ (set_pmf (bernoulli_pmf p ⤜ (λb. if b then map_pmf Inl Da else map_pmf Inr Db)) ∩ {f. (∃e. Inl e = f)}) ≠ {}" apply(simp add: UNIV_bool) using set_pmf_not_empty by fast lemma none2: "p >0 ⟹ p < 1 ⟹ (set_pmf (bernoulli_pmf p ⤜ (λb. if b then map_pmf Inl Da else map_pmf Inr Db)) ∩ {f. (∃e. Inr e = f)}) ≠ {}" apply(simp add: UNIV_bool) using set_pmf_not_empty by fast lemma C: "set_pmf (Proj1_pmf (Sum_pmf 0.5 Da Db)) = set_pmf Da" proof - show ?thesis unfolding Sum_pmf_def Proj1_pmf_def apply(simp add: ) using none[of "0.5" Da Db] apply(simp add: set_cond_pmf UNIV_bool) by force qed thm integral_measure_pmf thm pmf_cond pmf_cond[OF none] lemma proj1_pmf: assumes "p>0" "p<1" shows "Proj1_pmf (Sum_pmf p Da Db) = Da" proof - have kl: "⋀e. pmf (map_pmf Inr Db) (Inl e) = 0" apply(simp only: pmf_eq_0_set_pmf) apply(simp) by blast have ll: "measure_pmf.prob (bernoulli_pmf p ⤜ (λb. if b then map_pmf Inl Da else map_pmf Inr Db)) {f. ∃e. Inl e = f} = p" using assms apply(simp add: integral_pmf[symmetric] pmf_bind) apply(subst Bochner_Integration.integral_add) using integrable_pmf apply fast using integrable_pmf apply fast by(simp add: integral_pmf) have E: "(cond_pmf (bernoulli_pmf p ⤜ (λb. if b then map_pmf Inl Da else map_pmf Inr Db)) {f. ∃e. Inl e = f}) = map_pmf Inl Da" apply(rule pmf_eqI) apply(subst pmf_cond) using none[of p Da Db] assms apply (simp) using assms apply(auto) apply(subst pmf_bind) apply(simp add: kl ll ) apply(simp only: pmf_eq_0_set_pmf) by auto have ID: "case_sum (λe. e) (λa. undefined) ∘ Inl = id" by fastforce show ?thesis unfolding Sum_pmf_def Proj1_pmf_def apply(simp only: E) apply(simp add: pmf.map_comp ID) done qed definition "Proj2_pmf D = map_pmf (%a. case a of Inr e ⇒ e) (cond_pmf D {f. (∃e. Inr e = f)})" lemma proj2_pmf: assumes "p>0" "p<1" shows "Proj2_pmf (Sum_pmf p Da Db) = Db" proof - have kl: "⋀e. pmf (map_pmf Inl Da) (Inr e) = 0" apply(simp only: pmf_eq_0_set_pmf) apply(simp) by blast have ll: "measure_pmf.prob (bernoulli_pmf p ⤜ (λb. if b then map_pmf Inl Da else map_pmf Inr Db)) {f. ∃e. Inr e = f} = 1-p" using assms apply(simp add: integral_pmf[symmetric] pmf_bind) apply(subst Bochner_Integration.integral_add) using integrable_pmf apply fast using integrable_pmf apply fast by(simp add: integral_pmf) have E: "(cond_pmf (bernoulli_pmf p ⤜ (λb. if b then map_pmf Inl Da else map_pmf Inr Db)) {f. ∃e. Inr e = f}) = map_pmf Inr Db" apply(rule pmf_eqI) apply(subst pmf_cond) using none2[of p Da Db] assms apply (simp) using assms apply(auto) apply(subst pmf_bind) apply(simp add: kl ll ) apply(simp only: pmf_eq_0_set_pmf) by auto have ID: "case_sum (λe. undefined) (λa. a) ∘ Inr = id" by fastforce show ?thesis unfolding Sum_pmf_def Proj2_pmf_def apply(simp only: E) apply(simp add: pmf.map_comp ID) done qed definition "invSum invA invB D x i == invA (Proj1_pmf D) x i ∧ invB (Proj2_pmf D) x i" lemma invSum_split: "p>0 ⟹ p<1 ⟹ invA Da x i ⟹ invB Db x i ⟹ invSum invA invB (Sum_pmf p Da Db) x i" by(simp add: invSum_def proj1_pmf proj2_pmf) term "(%a. case a of Inl e ⇒ Inl (fa e) | Inr e ⇒ Inr (fb e))" definition "f_on2 fa fb = (%a. case a of Inl e ⇒ map_pmf Inl (fa e) | Inr e ⇒ map_pmf Inr (fb e))" term "bind_pmf" lemma Sum_bind_pmf: assumes a: "bind_pmf Da fa = Da'" and b: "bind_pmf Db fb = Db'" shows "bind_pmf (Sum_pmf p Da Db) (f_on2 fa fb) = Sum_pmf p Da' Db'" proof - { fix x have "(if x then map_pmf Inl Da else map_pmf Inr Db) ⤜ case_sum (λe. map_pmf Inl (fa e)) (λe. map_pmf Inr (fb e)) = (if x then map_pmf Inl Da ⤜ case_sum (λe. map_pmf Inl (fa e)) (λe. map_pmf Inr (fb e)) else map_pmf Inr Db ⤜ case_sum (λe. map_pmf Inl (fa e)) (λe. map_pmf Inr (fb e)))" apply(simp) done also have "… = (if x then map_pmf Inl (bind_pmf Da fa) else map_pmf Inr (bind_pmf Db fb))" by(auto simp add: map_pmf_def bind_assoc_pmf bind_return_pmf) also have "… = (if x then map_pmf Inl Da' else map_pmf Inr Db')" using a b by simp finally have "(if x then map_pmf Inl Da else map_pmf Inr Db) ⤜ case_sum (λe. map_pmf Inl (fa e)) (λe. map_pmf Inr (fb e)) = (if x then map_pmf Inl Da' else map_pmf Inr Db')" . } note gr=this show ?thesis unfolding Sum_pmf_def f_on2_def apply(rule pmf_eqI) apply(case_tac i) by(simp_all add: bind_return_pmf bind_assoc_pmf gr) qed definition "sum_map_pmf fa fb = (%a. case a of Inl e ⇒ Inl (fa e) | Inr e ⇒ Inr (fb e))" lemma Sum_map_pmf: assumes a: "map_pmf fa Da = Da'" and b: "map_pmf fb Db = Db'" shows "map_pmf (sum_map_pmf fa fb) (Sum_pmf p Da Db) = Sum_pmf p Da' Db'" proof - have "map_pmf (sum_map_pmf fa fb) (Sum_pmf p Da Db) = bind_pmf (Sum_pmf p Da Db) (f_on2 (λx. return_pmf (fa x)) (λx. return_pmf (fb x)))" using a b unfolding map_pmf_def sum_map_pmf_def f_on2_def by(auto simp add: bind_return_pmf sum.case_distrib) also have "… = Sum_pmf p Da' Db'" using assms[unfolded map_pmf_def] by(rule Sum_bind_pmf ) finally show ?thesis . qed end

# Theory Competitive_Analysis

(* Title: The Framework for competitive Analysis of randomized online algorithms Author: Tobias Nipkow Max Haslbeck *) section "Randomized Online and Offline Algorithms" theory Competitive_Analysis imports Prob_Theory On_Off begin subsection "Competitive Analysis Formalized" type_synonym ('s,'is,'r,'a)alg_on_step = "('s * 'is ⇒ 'r ⇒ ('a * 'is) pmf)" type_synonym ('s,'is)alg_on_init = "('s ⇒ 'is pmf)" type_synonym ('s,'is,'q,'a)alg_on_rand = "('s,'is)alg_on_init * ('s,'is,'q,'a)alg_on_step" subsubsection "classes of algorithms" definition deterministic_init :: "('s,'is)alg_on_init ⇒ bool" where "deterministic_init I ⟷ (∀init. card( set_pmf (I init)) = 1)" definition deterministic_step :: "('s,'is,'q,'a)alg_on_step ⇒ bool" where "deterministic_step S ⟷ (∀i is q. card( set_pmf (S (i, is) q)) = 1)" definition random_step :: "('s,'is,'q,'a)alg_on_step ⇒ bool" where "random_step S ⟷ ~ deterministic_step S" subsubsection "Randomized Online and Offline Algorithms" context On_Off begin fun steps where "steps s [] [] = s" | "steps s (q#qs) (a#as) = steps (step s q a) qs as" lemma steps_append: "length qs = length as ⟹ steps s (qs@qs') (as@as') = steps (steps s qs as) qs' as'" apply(induct qs as arbitrary: s rule: list_induct2) by simp_all lemma T_append: "length qs = length as ⟹ T s (qs@[q]) (as@[a]) = T s qs as + t (steps s qs as) q a" apply(induct qs as arbitrary: s rule: list_induct2) by simp_all lemma T_append2: "length qs = length as ⟹ T s (qs@qs') (as@as') = T s qs as + T (steps s qs as) qs' as'" apply(induct qs as arbitrary: s rule: list_induct2) by simp_all abbreviation Step_rand :: "('state,'is,'request,'answer) alg_on_rand ⇒ 'request ⇒ 'state * 'is ⇒ ('state * 'is) pmf" where "Step_rand A r s ≡ bind_pmf ((snd A) s r) (λ(a,is'). return_pmf (step (fst s) r a, is'))" fun config'_rand :: "('state,'is,'request,'answer) alg_on_rand ⇒ ('state*'is) pmf ⇒ 'request list ⇒ ('state * 'is) pmf" where "config'_rand A s [] = s" | "config'_rand A s (r#rs) = config'_rand A (s ⤜ Step_rand A r) rs" lemma config'_rand_snoc: "config'_rand A s (rs@[r]) = config'_rand A s rs ⤜ Step_rand A r" apply(induct rs arbitrary: s) by(simp_all) lemma config'_rand_append: "config'_rand A s (xs@ys) = config'_rand A (config'_rand A s xs) ys" apply(induct xs arbitrary: s) by(simp_all) abbreviation config_rand where "config_rand A s0 rs == config'_rand A ((fst A s0) ⤜ (λis. return_pmf (s0, is))) rs" lemma config'_rand_induct: "(∀x ∈ set_pmf init. P (fst x)) ⟹ (⋀s q a. P s ⟹ P (step s q a)) ⟹ ∀x∈set_pmf (config'_rand A init qs). P (fst x)" proof (induct qs arbitrary: init) case (Cons r rs) show ?case apply(simp) apply(rule Cons(1)) apply(subst Set.ball_simps(9)[where P=P, symmetric]) apply(subst set_map_pmf[symmetric]) apply(simp only: map_bind_pmf) apply(simp add: bind_assoc_pmf bind_return_pmf split_def) using Cons(2,3) apply blast by fact qed (simp) lemma config_rand_induct: "P s0 ⟹ (⋀s q a. P s ⟹ P (step s q a)) ⟹ ∀x∈set_pmf (config_rand A s0 qs). P (fst x)" using config'_rand_induct[of "((fst A s0) ⤜ (λis. return_pmf (s0, is)))" P] by auto fun T_on_rand' :: "('state,'is,'request,'answer) alg_on_rand ⇒ ('state*'is) pmf ⇒ 'request list ⇒ real" where "T_on_rand' A s [] = 0" | "T_on_rand' A s (r#rs) = E ( s ⤜ (λs. bind_pmf (snd A s r) (λ(a,is'). return_pmf (real (t (fst s) r a)))) ) + T_on_rand' A (s ⤜ Step_rand A r) rs" lemma T_on_rand'_append: "T_on_rand' A s (xs@ys) = T_on_rand' A s xs + T_on_rand' A (config'_rand A s xs) ys" apply(induct xs arbitrary: s) by simp_all abbreviation T_on_rand :: "('state,'is,'request,'answer) alg_on_rand ⇒ 'state ⇒ 'request list ⇒ real" where "T_on_rand A s rs == T_on_rand' A (fst A s ⤜ (λis. return_pmf (s,is))) rs" lemma T_on_rand_append: "T_on_rand A s (xs@ys) = T_on_rand A s xs + T_on_rand' A (config_rand A s xs) ys" by(rule T_on_rand'_append) abbreviation "T_on_rand'_n A s0 xs n == T_on_rand' A (config'_rand A s0 (take n xs)) [xs!n]" lemma T_on_rand'_as_sum: "T_on_rand' A s0 rs = sum (T_on_rand'_n A s0 rs) {..<length rs} " apply(induct rs rule: rev_induct) by(simp_all add: T_on_rand'_append nth_append) abbreviation "T_on_rand_n A s0 xs n == T_on_rand' A (config_rand A s0 (take n xs)) [xs!n]" lemma T_on_rand_as_sum: "T_on_rand A s0 rs = sum (T_on_rand_n A s0 rs) {..<length rs} " apply(induct rs rule: rev_induct) by(simp_all add: T_on_rand'_append nth_append) lemma T_on_rand'_nn: "T_on_rand' A s qs ≥ 0" apply(induct qs arbitrary: s) apply(simp_all add: bind_return_pmf) apply(rule add_nonneg_nonneg) apply(rule E_nonneg) by(simp_all add: split_def) lemma T_on_rand_nn: "T_on_rand (I,S) s0 qs ≥ 0" by (rule T_on_rand'_nn) definition compet_rand :: "('state,'is,'request,'answer) alg_on_rand ⇒ real ⇒ 'state set ⇒ bool" where "compet_rand A c S0 = (∀s∈S0. ∃b ≥ 0. ∀rs. wf s rs ⟶ T_on_rand A s rs ≤ c * T_opt s rs + b)" subsection "embeding of deterministic into randomized algorithms" fun embed :: "('state,'is,'request,'answer) alg_on ⇒ ('state,'is,'request,'answer) alg_on_rand" where "embed A = ( (λs. return_pmf (fst A s)) , (λs r. return_pmf (snd A s r)) )" lemma T_deter_rand: "T_off (λs0. (off2 A (s0, x))) s0 qs = T_on_rand' (embed A) (return_pmf (s0,x)) qs" apply(induct qs arbitrary: s0 x) by(simp_all add: Step_def bind_return_pmf split: prod.split) lemma config'_embed: "config'_rand (embed A) (return_pmf s0) qs = return_pmf (config' A s0 qs)" apply(induct qs arbitrary: s0) apply(simp_all add: Step_def split_def bind_return_pmf) by metis lemma config_embed: "config_rand (embed A) s0 qs = return_pmf (config A s0 qs)" apply(simp add: bind_return_pmf) apply(subst config'_embed[unfolded embed.simps]) by simp lemma T_on_embed: "T_on A s0 qs = T_on_rand (embed A) s0 qs" using T_deter_rand[where x="fst A s0", of s0 qs A] by(auto simp: bind_return_pmf) lemma T_on'_embed: "T_on' A (s0,x) qs = T_on_rand' (embed A) (return_pmf (s0,x)) qs" using T_deter_rand T_on_on' by metis lemma compet_embed: "compet A c S0 = compet_rand (embed A) c S0" unfolding compet_def compet_rand_def using T_on_embed by metis end end

# Theory Move_to_Front

(* Author: Tobias Nipkow *) section "Deterministic List Update" theory Move_to_Front imports Swaps On_Off Competitive_Analysis begin declare Let_def[simp] subsection "Function ‹mtf›" definition mtf :: "'a ⇒ 'a list ⇒ 'a list" where "mtf x xs = (if x ∈ set xs then x # (take (index xs x) xs) @ drop (index xs x + 1) xs else xs)" lemma mtf_id[simp]: "x ∉ set xs ⟹ mtf x xs = xs" by(simp add: mtf_def) lemma mtf0[simp]: "x ∈ set xs ⟹ mtf x xs ! 0 = x" by(auto simp: mtf_def) lemma before_in_mtf: assumes "z ∈ set xs" shows "x < y in mtf z xs ⟷ (y ≠ z ∧ (if x=z then y ∈ set xs else x < y in xs))" proof- have 0: "index xs z < size xs" by (metis assms index_less_size_conv) let ?xs = "take (index xs z) xs @ xs ! index xs z # drop (Suc (index xs z)) xs" have "x < y in mtf z xs = (y ≠ z ∧ (if x=z then y ∈ set ?xs else x < y in ?xs))" using assms by(auto simp add: mtf_def before_in_def index_append) (metis add_lessD1 index_less_size_conv length_take less_Suc_eq not_less_eq) with id_take_nth_drop[OF 0, symmetric] show ?thesis by(simp) qed lemma Inv_mtf: "set xs = set ys ⟹ z : set ys ⟹ Inv xs (mtf z ys) = Inv xs ys ∪ {(x,z)|x. x < z in xs ∧ x < z in ys} - {(z,x)|x. z < x in xs ∧ x < z in ys}" by(auto simp add: Inv_def before_in_mtf not_before_in dest: before_in_setD1) lemma set_mtf[simp]: "set(mtf x xs) = set xs" by(simp add: mtf_def) (metis append_take_drop_id Cons_nth_drop_Suc index_less le_refl Un_insert_right nth_index set_append set_simps(2)) lemma length_mtf[simp]: "size (mtf x xs) = size xs" by (auto simp add: mtf_def min_def) (metis index_less_size_conv leD) lemma distinct_mtf[simp]: "distinct (mtf x xs) = distinct xs" by (metis length_mtf set_mtf card_distinct distinct_card) subsection "Function ‹mtf2›" definition mtf2 :: "nat ⇒ 'a ⇒ 'a list ⇒ 'a list" where "mtf2 n x xs = (if x : set xs then swaps [index xs x - n..<index xs x] xs else xs)" lemma mtf_eq_mtf2: "mtf x xs = mtf2 (length xs - 1) x xs" proof - have "x : set xs ⟹ index xs x - (size xs - Suc 0) = 0" by (auto simp: less_Suc_eq_le[symmetric]) thus ?thesis by(auto simp: mtf_def mtf2_def swaps_eq_nth_take_drop) qed lemma mtf20[simp]: "mtf2 0 x xs = xs" by(auto simp add: mtf2_def) lemma length_mtf2[simp]: "length (mtf2 n x xs) = length xs" by (auto simp: mtf2_def index_less_size_conv[symmetric] simp del:index_conv_size_if_notin) lemma set_mtf2[simp]: "set(mtf2 n x xs) = set xs" by (auto simp: mtf2_def index_less_size_conv[symmetric] simp del:index_conv_size_if_notin) lemma distinct_mtf2[simp]: "distinct (mtf2 n x xs) = distinct xs" by (metis length_mtf2 set_mtf2 card_distinct distinct_card) lemma card_Inv_mtf2: "xs!j = ys!0 ⟹ j < length xs ⟹ dist_perm xs ys ⟹ card (Inv (swaps [i..<j] xs) ys) = card (Inv xs ys) - int(j-i)" proof(induction j arbitrary: xs) case (Suc j) show ?case proof cases assume "i > j" thus ?thesis by simp next assume [arith]: "¬ i > j" have 0: "Suc j < length ys" by (metis Suc.prems(2,3) distinct_card) have 1: "(ys ! 0, xs ! j) : Inv ys xs" proof (auto simp: Inv_def) show "ys ! 0 < xs ! j in ys" using Suc.prems by (metis Suc_lessD n_not_Suc_n not_before0 not_before_in nth_eq_iff_index_eq nth_mem) show "xs ! j < ys ! 0 in xs" using Suc.prems by (metis Suc_lessD before_id lessI) qed have 2: "card(Inv ys xs) ≠ 0" using 1 by auto have "int(card (Inv (swaps [i..<Suc j] xs) ys)) = card (Inv (swap j xs) ys) - int (j-i)" using Suc by simp also have "… = card (Inv ys (swap j xs)) - int (j-i)" by(simp add: card_Inv_sym) also have "… = card (Inv ys xs - {(ys ! 0, xs ! j)}) - int (j - i)" using Suc.prems 0 by(simp add: Inv_swap) also have "… = int(card (Inv ys xs) - 1) - (j - i)" using 1 by(simp add: card_Diff_singleton) also have "… = card (Inv ys xs) - int (Suc j - i)" using 2 by arith also have "… = card (Inv xs ys) - int (Suc j - i)" by(simp add: card_Inv_sym) finally show ?thesis . qed qed simp subsection "Function Lxy" definition Lxy :: "'a list ⇒ 'a set ⇒ 'a list" where "Lxy xs S = filter (λz. z∈S) xs" thm inter_set_filter lemma Lxy_length_cons: "length (Lxy xs S) ≤ length (Lxy (x#xs) S)" unfolding Lxy_def by(simp) lemma Lxy_empty[simp]: "Lxy [] S = []" unfolding Lxy_def by simp lemma Lxy_set_filter: "set (Lxy xs S) = S ∩ set xs" by (simp add: Lxy_def inter_set_filter) lemma Lxy_distinct: "distinct xs ⟹ distinct (Lxy xs S)" by (simp add: Lxy_def) lemma Lxy_append: "Lxy (xs@ys) S = Lxy xs S @ Lxy ys S" by(simp add: Lxy_def) lemma Lxy_snoc: "Lxy (xs@[x]) S = (if x∈S then Lxy xs S @ [x] else Lxy xs S)" by(simp add: Lxy_def) lemma Lxy_not: "S ∩ set xs = {} ⟹ Lxy xs S = []" unfolding Lxy_def apply(induct xs) by simp_all lemma Lxy_notin: "set xs ∩ S = {} ⟹ Lxy xs S = []" apply(induct xs) by(simp_all add: Lxy_def) lemma Lxy_in: "x∈S ⟹ Lxy [x] S = [x]" by(simp add: Lxy_def) lemma Lxy_project: assumes "x≠y" "x ∈ set xs" "y∈set xs" "distinct xs" and "x < y in xs" shows "Lxy xs {x,y} = [x,y]" proof - from assms have ij: "index xs x < index xs y" and xinxs: "index xs x < length xs" and yinxs: "index xs y < length xs" unfolding before_in_def by auto from xinxs obtain a as where dec1: "a @ [xs!index xs x] @ as = xs" and "a = take (index xs x) xs" and "as = drop (Suc (index xs x)) xs" and length_a: "length a = index xs x" and length_as: "length as = length xs - index xs x- 1" using id_take_nth_drop by fastforce have "index xs y≥length (a @ [xs!index xs x])" using length_a ij by auto then have "((a @ [xs!index xs x]) @ as) ! index xs y = as ! (index xs y-length (a @ [xs ! index xs x]))" using nth_append[where xs="a @ [xs!index xs x]" and ys="as"] by(simp) then have xsj: "xs ! index xs y = as ! (index xs y-index xs x-1)" using dec1 length_a by auto have las: "(index xs y-index xs x-1) < length as" using length_as yinxs ij by simp obtain b c where dec2: "b @ [xs!index xs y] @ c = as" and "b = take (index xs y-index xs x-1) as" "c=drop (Suc (index xs y-index xs x-1)) as" and length_b: "length b = index xs y-index xs x-1" using id_take_nth_drop[OF las] xsj by force have xs_dec: "a @ [xs!index xs x] @ b @ [xs!index xs y] @ c = xs" using dec1 dec2 by auto from xs_dec assms(4) have "distinct ((a @ [xs!index xs x] @ b @ [xs!index xs y]) @ c)" by simp then have c_empty: "set c ∩ {x,y} = {}" and b_empty: "set b ∩ {x,y} = {}"and a_empty: "set a ∩ {x,y} = {}" by(auto simp add: assms(2,3)) have "Lxy (a @ [xs!index xs x] @ b @ [xs!index xs y] @ c) {x,y} = [x,y]" apply(simp only: Lxy_append) apply(simp add: assms(2,3)) using a_empty b_empty c_empty by(simp add: Lxy_notin Lxy_in) with xs_dec show ?thesis by auto qed lemma Lxy_mono: "{x,y} ⊆ set xs ⟹ distinct xs ⟹ x < y in xs = x < y in Lxy xs {x,y}" apply(cases "x=y") apply(simp add: before_in_irefl) proof - assume xyset: "{x,y} ⊆ set xs" assume dxs: "distinct xs" assume xy: "x≠y" { fix x y assume 1: "{x,y} ⊆ set xs" assume xny: "x≠y" assume 3: "x < y in xs" have "Lxy xs {x,y} = [x,y]" apply(rule Lxy_project) using xny 1 3 dxs by(auto) then have "x < y in Lxy xs {x,y}" using xny by(simp add: before_in_def) } note aha=this have a: "x < y in xs ⟹ x < y in Lxy xs {x,y}" apply(subst Lxy_project) using xy xyset dxs by(simp_all add: before_in_def) have t: "{x,y}={y,x}" by(auto) have f: "~ x < y in xs ⟹ y < x in Lxy xs {x,y}" unfolding t apply(rule aha) using xyset apply(simp) using xy apply(simp) using xy xyset by(simp add: not_before_in) have b: "~ x < y in xs ⟹ ~ x < y in Lxy xs {x,y}" proof - assume "~ x < y in xs" then have "y < x in Lxy xs {x,y}" using f by auto then have "~ x < y in Lxy xs {x,y}" using xy by(simp add: not_before_in) then show ?thesis . qed from a b show ?thesis by metis qed subsection "List Update as Online/Offline Algorithm" type_synonym 'a state = "'a list" type_synonym answer = "nat * nat list" definition step :: "'a state ⇒ 'a ⇒ answer ⇒ 'a state" where "step s r a = (let (k,sws) = a in mtf2 k r (swaps sws s))" definition t :: "'a state ⇒ 'a ⇒ answer ⇒ nat" where "t s r a = (let (mf,sws) = a in index (swaps sws s) r + 1 + size sws)" definition static where "static s rs = (set rs ⊆ set s)" interpretation On_Off step t static . type_synonym 'a alg_off = "'a state ⇒ 'a list ⇒ answer list" type_synonym ('a,'is) alg_on = "('a state,'is,'a,answer) alg_on" lemma T_ge_len: "length as = length rs ⟹ T s rs as ≥ length rs" by(induction arbitrary: s rule: list_induct2) (auto simp: t_def trans_le_add2) lemma T_off_neq0: "(⋀rs s0. size(alg s0 rs) = length rs) ⟹ rs ≠ [] ⟹ T_off alg s0 rs ≠ 0" apply(erule_tac x=rs in meta_allE) apply(erule_tac x=s0 in meta_allE) apply (auto simp: neq_Nil_conv length_Suc_conv t_def) done lemma length_step[simp]: "length (step s r as) = length s" by(simp add: step_def split_def) lemma step_Nil_iff[simp]: "step xs r act = [] ⟷ xs = []" by(auto simp add: step_def mtf2_def split: prod.splits) lemma set_step2: "set(step s r (mf,sws)) = set s" by(auto simp add: step_def) lemma set_step: "set(step s r act) = set s" by(cases act)(simp add: set_step2) lemma distinct_step: "distinct(step s r as) = distinct s" by (auto simp: step_def split_def) subsection "Online Algorithm Move-to-Front is 2-Competitive" definition MTF :: "('a,unit) alg_on" where "MTF = (λ_. (), λs r. ((size (fst s) - 1,[]), ()))" text‹It was first proved by Sleator and Tarjan~\cite{SleatorT-CACM85} that the Move-to-Front algorithm is 2-competitive.› (* The core idea with upper bounds: *) lemma potential: fixes t :: "nat ⇒ 'a::linordered_ab_group_add" and p :: "nat ⇒ 'a" assumes p0: "p 0 = 0" and ppos: "⋀n. p n ≥ 0" and ub: "⋀n. t n + p(n+1) - p n ≤ u n" shows "(∑i<n. t i) ≤ (∑i<n. u i)" proof- let ?a = "λn. t n + p(n+1) - p n" have 1: "(∑i<n. t i) = (∑i<n. ?a i) - p(n)" by(induction n) (simp_all add: p0) thus ?thesis by (metis (erased, lifting) add.commute diff_add_cancel le_add_same_cancel2 order.trans ppos sum_mono ub) qed lemma potential2: fixes t :: "nat ⇒ 'a::linordered_ab_group_add" and p :: "nat ⇒ 'a" assumes p0: "p 0 = 0" and ppos: "⋀n. p n ≥ 0" and ub: "⋀m. m<n ⟹ t m + p(m+1) - p m ≤ u m" shows "(∑i<n. t i) ≤ (∑i<n. u i)" proof- let ?a = "λn. t n + p(n+1) - p n" have "(∑i<n. t i) = (∑i<n. ?a i) - p(n)" by(induction n) (simp_all add: p0) also have "… ≤ (∑i<n. ?a i)" using ppos by auto also have "… ≤ (∑i<n. u i)" apply(rule sum_mono) apply(rule ub) by auto finally show ?thesis . qed abbreviation "before x xs ≡ {y. y < x in xs}" abbreviation "after x xs ≡ {y. x < y in xs}" lemma finite_before[simp]: "finite (before x xs)" apply(rule finite_subset[where B = "set xs"]) apply (auto dest: before_in_setD1) done lemma finite_after[simp]: "finite (after x xs)" apply(rule finite_subset[where B = "set xs"]) apply (auto dest: before_in_setD2) done lemma before_conv_take: "x : set xs ⟹ before x xs = set(take (index xs x) xs)" by (auto simp add: before_in_def set_take_if_index index_le_size) (metis index_take leI) lemma card_before: "distinct xs ⟹ x : set xs ⟹ card (before x xs) = index xs x" using index_le_size[of xs x] by(simp add: before_conv_take distinct_card[OF distinct_take] min_def) lemma before_Un: "set xs = set ys ⟹ x : set xs ⟹ before x ys = before x xs ∩ before x ys Un after x xs ∩ before x ys" by(auto)(metis before_in_setD1 not_before_in) lemma phi_diff_aux: "card (Inv xs ys ∪ {(y, x) |y. y < x in xs ∧ y < x in ys} - {(x, y) |y. x < y in xs ∧ y < x in ys}) = card(Inv xs ys) + card(before x xs ∩ before x ys) - int(card(after x xs ∩ before x ys))" (is "card(?I ∪ ?B - ?A) = card ?I + card ?b - int(card ?a)") proof- have 1: "?I ∩ ?B = {}" by(auto simp: Inv_def) (metis no_before_inI) have 2: "?A ⊆ ?I ∪ ?B" by(auto simp: Inv_def) have 3: "?A ⊆ ?I" by(auto simp: Inv_def) have "int(card(?I ∪ ?B - ?A)) = int(card ?I + card ?B) - int(card ?A)" using card_mono[OF _ 3] by(simp add: card_Un_disjoint[OF _ _ 1] card_Diff_subset[OF _ 2]) also have "card ?B = card (fst ` ?B)" by(auto simp: card_image inj_on_def) also have "fst ` ?B = ?b" by force also have "card ?A = card (snd ` ?A)" by(auto simp: card_image inj_on_def) also have "snd ` ?A = ?a" by force finally show ?thesis . qed lemma not_before_Cons[simp]: "¬ x < y in y # xs" by (simp add: before_in_def) lemma before_Cons[simp]: "y ∈ set xs ⟹ y ≠ x ⟹ before y (x#xs) = insert x (before y xs)" by(auto simp: before_in_def) lemma card_before_le_index: "card (before x xs) ≤ index xs x" apply(cases "x ∈ set xs") prefer 2 apply (simp add: before_in_def) apply(induction xs) apply (simp add: before_in_def) apply (auto simp: card_insert_if) done lemma config_config_length: "length (fst (config A init qs)) = length init" apply (induct rule: config_induct) by (simp_all) lemma config_config_distinct: shows " distinct (fst (config A init qs)) = distinct init" apply (induct rule: config_induct) by (simp_all add: distinct_step) lemma config_config_set: shows "set (fst (config A init qs)) = set init" apply(induct rule: config_induct) by(simp_all add: set_step) lemma config_config: "set (fst (config A init qs)) = set init ∧ distinct (fst (config A init qs)) = distinct init ∧ length (fst (config A init qs)) = length init" using config_config_distinct config_config_set config_config_length by metis lemma config_dist_perm: "distinct init ⟹ dist_perm (fst (config A init qs)) init" using config_config_distinct config_config_set by metis lemma config_rand_length: "∀x∈set_pmf (config_rand A init qs). length (fst x) = length init" apply (induct rule: config_rand_induct) by (simp_all) lemma config_rand_distinct: shows "∀x ∈ (config_rand A init qs). distinct (fst x) = distinct init" apply (induct rule: config_rand_induct) by (simp_all add: distinct_step) lemma config_rand_set: shows " ∀x ∈ (config_rand A init qs). set (fst x) = set init" apply(induct rule: config_rand_induct) by(simp_all add: set_step) lemma config_rand: "∀x ∈ (config_rand A init qs). set (fst x) = set init ∧ distinct (fst x) = distinct init ∧ length (fst x) = length init" using config_rand_distinct config_rand_set config_rand_length by metis lemma config_rand_dist_perm: "distinct init ⟹ ∀x ∈ (config_rand A init qs). dist_perm (fst x) init" using config_rand_distinct config_rand_set by metis (*fixme start from Inv*) lemma amor_mtf_ub: assumes "x : set ys" "set xs = set ys" shows "int(card(before x xs Int before x ys)) - card(after x xs Int before x ys) ≤ 2 * int(index xs x) - card (before x ys)" (is "?m - ?n ≤ 2 * ?j - ?k") proof- have xxs: "x ∈ set xs" using assms(1,2) by simp let ?bxxs = "before x xs" let ?bxys = "before x ys" let ?axxs = "after x xs" have 0: "?bxxs ∩ ?axxs = {}" by (auto simp: before_in_def) hence 1: "(?bxxs ∩ ?bxys) ∩ (?axxs ∩ ?bxys) = {}" by blast have "(?bxxs ∩ ?bxys) ∪ (?axxs ∩ ?bxys) = ?bxys" using assms(2) before_Un xxs by fastforce hence "?m + ?n = ?k" using card_Un_disjoint[OF _ _ 1] by simp hence "?m - ?n = 2 * ?m - ?k" by arith also have "?m ≤ ?j" using card_before_le_index[of x xs] card_mono[of ?bxxs, OF _ Int_lower1] by(auto intro: order_trans) finally show ?thesis by auto qed locale MTF_Off = fixes as :: "answer list" fixes rs :: "'a list" fixes s0 :: "'a list" assumes dist_s0[simp]: "distinct s0" assumes len_as: "length as = length rs" begin definition mtf_A :: "nat list" where "mtf_A = map fst as" definition sw_A :: "nat list list" where "sw_A = map snd as" fun s_A :: "nat ⇒ 'a list" where "s_A 0 = s0" | "s_A(Suc n) = step (s_A n) (rs!n) (mtf_A!n, sw_A!n)" lemma length_s_A[simp]: "length(s_A n) = length s0" 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 s0" by(induction n) (simp_all add: step_def) fun s_mtf :: "nat ⇒ 'a list" where "s_mtf 0 = s0" | "s_mtf (Suc n) = mtf (rs!n) (s_mtf n)" definition t_mtf :: "nat ⇒ int" where "t_mtf n = index (s_mtf n) (rs!n) + 1" definition T_mtf :: "nat ⇒ int" where "T_mtf n = (∑i<n. t_mtf i)" definition c_A :: "nat ⇒ int" where "c_A n = index (swaps (sw_A!n) (s_A n)) (rs!n) + 1" definition f_A :: "nat ⇒ int" where "f_A n = min (mtf_A!n) (index (swaps (sw_A!n) (s_A n)) (rs!n))" definition p_A :: "nat ⇒ int" where "p_A n = size(sw_A!n)" definition t_A :: "nat ⇒ int" where "t_A n = c_A n + p_A n" definition T_A :: "nat ⇒ int" where "T_A n = (∑i<n. t_A i)" lemma length_s_mtf[simp]: "length(s_mtf n) = length s0" by (induction n) simp_all lemma dist_s_mtf[simp]: "distinct(s_mtf n)" apply(induction n) apply (simp) apply (auto simp: mtf_def index_take set_drop_if_index) apply (metis set_drop_if_index index_take less_Suc_eq_le linear) done lemma set_s_mtf[simp]: "set (s_mtf n) = set s0" by (induction n) (simp_all) lemma dperm_inv: "dist_perm (s_A n) (s_mtf n)" by (metis dist_s_mtf dist_s_A set_s_mtf set_s_A) definition Phi :: "nat ⇒ int" ("Φ") where "Phi n = card(Inv (s_A n) (s_mtf n))" lemma phi0: "Phi 0 = 0" by(simp add: Phi_def) lemma phi_pos: "Phi n ≥ 0" by(simp add: Phi_def) lemma mtf_ub: "t_mtf n + Phi (n+1) - Phi n ≤ 2 * c_A n - 1 + p_A n - f_A n" proof - let ?xs = "s_A n" let ?ys = "s_mtf n" let ?x = "rs!n" let ?xs' = "swaps (sw_A!n) ?xs" let ?ys' = "mtf ?x ?ys" show ?thesis proof cases assume xin: "?x ∈ set ?ys" let ?bb = "before ?x ?xs ∩ before ?x ?ys" let ?ab = "after ?x ?xs ∩ before ?x ?ys" have phi_mtf: "card(Inv ?xs' ?ys') - int(card (Inv ?xs' ?ys)) ≤ 2 * int(index ?xs' ?x) - int(card (before ?x ?ys))" using xin by(simp add: Inv_mtf phi_diff_aux amor_mtf_ub) have phi_sw: "card(Inv ?xs' ?ys) ≤ Phi n + length(sw_A!n)" proof - have "int(card (Inv ?xs' ?ys)) ≤ card(Inv ?xs' ?xs) + int(card(Inv ?xs ?ys))" using card_Inv_tri_ineq[of ?xs' ?xs ?ys] xin by (simp) also have "card(Inv ?xs' ?xs) = card(Inv ?xs ?xs')" by (rule card_Inv_sym) also have "card(Inv ?xs ?xs') ≤ size(sw_A!n)" by (metis card_Inv_swaps_le dist_s_A) finally show ?thesis by(fastforce simp: Phi_def) qed have phi_free: "card(Inv ?xs' ?ys') - Phi (Suc n) = f_A n" using xin by(simp add: Phi_def mtf2_def step_def card_Inv_mtf2 index_less_size_conv f_A_def) show ?thesis using xin phi_sw phi_mtf phi_free card_before[of "s_mtf n"] by(simp add: t_mtf_def c_A_def p_A_def) next assume notin: "?x ∉ set ?ys" have "int (card (Inv ?xs' ?ys)) - card (Inv ?xs ?ys) ≤ card(Inv ?xs ?xs')" using card_Inv_tri_ineq[OF _ dperm_inv, of ?xs' n] swaps_inv[of "sw_A!n" "s_A n"] by(simp add: card_Inv_sym) also have "… ≤ size(sw_A!n)" by(simp add: card_Inv_swaps_le dperm_inv) finally show ?thesis using notin by(simp add: t_mtf_def step_def c_A_def p_A_def f_A_def Phi_def mtf2_def) qed qed theorem Sleator_Tarjan: "T_mtf n ≤ (∑i<n. 2*c_A i + p_A i - f_A i) - n" proof- have "(∑i<n. t_mtf i) ≤ (∑i<n. 2*c_A i - 1 + p_A i - f_A i)" by(rule potential[where p=Phi,OF phi0 phi_pos mtf_ub]) also have "… = (∑i<n. (2*c_A i + p_A i - f_A i) - 1)" by (simp add: algebra_simps) also have "… = (∑i<n. 2*c_A i + p_A i - f_A i) - n" by(simp add: sumr_diff_mult_const2[symmetric]) finally show ?thesis by(simp add: T_mtf_def) qed corollary Sleator_Tarjan': "T_mtf n ≤ 2*T_A n - n" proof - have "T_mtf n ≤ (∑i<n. 2*c_A i + p_A i - f_A i) - n" by (fact Sleator_Tarjan) also have "(∑i<n. 2*c_A i + p_A i - f_A i) ≤ (∑i<n. 2*(c_A i + p_A i))" by(intro sum_mono) (simp add: p_A_def f_A_def) also have "… ≤ 2* T_A n" by (simp add: sum_distrib_left T_A_def t_A_def) finally show "T_mtf n ≤ 2* T_A n - n" by auto qed 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_mtf_ub: "∀i<n. rs!i ∈ set s0 ⟹ T_mtf n ≤ n * size s0" proof(induction n) case 0 show ?case by(simp add: T_mtf_def) next case (Suc n) thus ?case using index_less_size_conv[of "s_mtf n" "rs!n"] by(simp add: T_mtf_def t_mtf_def less_Suc_eq del: index_less) qed corollary T_mtf_competitive: assumes "s0 ≠ []" and "∀i<n. rs!i ∈ set s0" shows "T_mtf n ≤ (2 - 1/(size s0)) * T_A n" proof cases assume 0: "real_of_int(T_A n) ≤ n * (size s0)" have "T_mtf n ≤ 2 * T_A n - n" proof - have "T_mtf n ≤ (∑i<n. 2*c_A i + p_A i - f_A i) - n" by(rule Sleator_Tarjan) also have "(∑i<n. 2*c_A i + p_A i - f_A i) ≤ (∑i<n. 2*(c_A i + p_A i))" by(intro sum_mono) (simp add: p_A_def f_A_def) also have "… ≤ 2 * T_A n" by (simp add: sum_distrib_left T_A_def t_A_def) finally show ?thesis by simp qed hence "real_of_int(T_mtf n) ≤ 2 * of_int(T_A n) - n" by simp also have "… = 2 * of_int(T_A n) - (n * size s0) / size s0" using assms(1) by simp also have "… ≤ 2 * real_of_int(T_A n) - T_A n / size s0" by(rule diff_left_mono[OF divide_right_mono[OF 0]]) simp also have "… = (2 - 1 / size s0) * T_A n" by algebra finally show ?thesis . next assume 0: "¬ real_of_int(T_A n) ≤ n * (size s0)" have "2 - 1 / size s0 ≥ 1" using assms(1) by (auto simp add: field_simps neq_Nil_conv) have "real_of_int (T_mtf n) ≤ n * size s0" using T_mtf_ub[OF assms(2)] by linarith also have "… < of_int(T_A n)" using 0 by simp also have "… ≤ (2 - 1 / size s0) * T_A n" using assms(1) T_A_nneg[of n] by(auto simp add: mult_le_cancel_right1 field_simps neq_Nil_conv) finally show ?thesis by linarith qed lemma t_A_t: "n < length rs ⟹ t_A n = int (t (s_A n) (rs ! n) (as ! n))" by(simp add: t_A_def t_def c_A_def p_A_def sw_A_def len_as split: prod.split) lemma T_A_eq_lem: "(∑i=0..<length rs. t_A i) = T (s_A 0) (drop 0 rs) (drop 0 as)" proof(induction rule: zero_induct[of _ "size rs"]) case 1 thus ?case by (simp add: len_as) next case (2 n) show ?case proof cases assume "n < length rs" thus ?case using 2 by(simp add: Cons_nth_drop_Suc[symmetric,where i=n] len_as sum.atLeast_Suc_lessThan t_A_t mtf_A_def sw_A_def) next assume "¬ n < length rs" thus ?case by (simp add: len_as) qed qed lemma T_A_eq: "T_A (length rs) = T s0 rs as" using T_A_eq_lem by(simp add: T_A_def atLeast0LessThan) lemma nth_off_MTF: "n < length rs ⟹ off2 MTF s rs ! n = (size(fst s) - 1,[])" by(induction rs arbitrary: s n)(auto simp add: MTF_def nth_Cons' Step_def) lemma t_mtf_MTF: "n < length rs ⟹ t_mtf n = int (t (s_mtf n) (rs ! n) (off MTF s rs ! n))" by(simp add: t_mtf_def t_def nth_off_MTF split: prod.split) lemma mtf_MTF: "n < length rs ⟹ length s = length s0 ⟹ mtf (rs ! n) s = step s (rs ! n) (off MTF s0 rs ! n)" by(auto simp add: nth_off_MTF step_def mtf_eq_mtf2) lemma T_mtf_eq_lem: "(∑i=0..<length rs. t_mtf i) = T (s_mtf 0) (drop 0 rs) (drop 0 (off MTF s0 rs))" proof(induction rule: zero_induct[of _ "size rs"]) case 1 thus ?case by (simp add: len_as) next case (2 n) show ?case proof cases assume "n < length rs" thus ?case using 2 by(simp add: Cons_nth_drop_Suc[symmetric,where i=n] len_as sum.atLeast_Suc_lessThan t_mtf_MTF[where s=s0] mtf_A_def sw_A_def mtf_MTF) next assume "¬ n < length rs" thus ?case by (simp add: len_as) qed qed lemma T_mtf_eq: "T_mtf (length rs) = T_on MTF s0 rs" using T_mtf_eq_lem by(simp add: T_mtf_def atLeast0LessThan) corollary MTF_competitive2: "s0 ≠ [] ⟹ ∀i<length rs. rs!i ∈ set s0 ⟹ T_on MTF s0 rs ≤ (2 - 1/(size s0)) * T s0 rs as" by (metis T_mtf_competitive T_A_eq T_mtf_eq of_int_of_nat_eq) corollary MTF_competitive': "T_on MTF s0 rs ≤ 2 * T s0 rs as" using Sleator_Tarjan'[of "length rs"] T_A_eq T_mtf_eq by auto end theorem compet_MTF: assumes "s0 ≠ []" "distinct s0" "set rs ⊆ set s0" shows "T_on MTF s0 rs ≤ (2 - 1/(size s0)) * T_opt s0 rs" proof- from assms(3) have 1: "∀i < length rs. rs!i ∈ set s0" by auto { fix as :: "answer list" assume len: "length as = length rs" interpret MTF_Off as rs s0 proof qed (auto simp: assms(2) len) from MTF_competitive2[OF assms(1) 1] assms(1) have "T_on MTF s0 rs / (2 - 1 / (length s0)) ≤ of_int(T s0 rs as)" by(simp add: field_simps length_greater_0_conv[symmetric] del: length_greater_0_conv) } hence "T_on MTF s0 rs / (2 - 1/(size s0)) ≤ T_opt s0 rs" apply(simp add: T_opt_def Inf_nat_def) apply(rule LeastI2_wellorder) using length_replicate[of "length rs" 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_MTF': assumes "distinct s0" shows "T_on MTF s0 rs ≤ (2::real) * T_opt s0 rs" proof- { fix as :: "answer list" assume len: "length as = length rs" interpret MTF_Off as rs s0 proof qed (auto simp: assms(1) len) from MTF_competitive' have "T_on MTF s0 rs / 2 ≤ of_int(T s0 rs as)" by(simp add: field_simps length_greater_0_conv[symmetric] del: length_greater_0_conv) } hence "T_on MTF s0 rs / 2 ≤ T_opt s0 rs" apply(simp add: T_opt_def Inf_nat_def) apply(rule LeastI2_wellorder) using length_replicate[of "length rs" 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 MTF_is_2_competitive: "compet MTF 2 {s . distinct s}" unfolding compet_def using compet_MTF' by fastforce subsection "Lower Bound for Competitiveness" text‹This result is independent of MTF but is based on the list update problem defined in this theory.› lemma rat_fun_lem: fixes l c :: real assumes [simp]: "F ≠ bot" assumes "0 < l" assumes ev: "eventually (λn. l ≤ f n / g n) F" "eventually (λn. (f n + c) / (g n + d) ≤ u) F" and g: "LIM n F. g n :> at_top" shows "l ≤ u" proof (rule dense_le_bounded[OF ‹0 < l›]) fix x assume x: "0 < x" "x < l" define m where "m = (x - l) / 2" define k where "k = l / (x - m)" have "x = l / k + m" "1 < k" "m < 0" unfolding k_def m_def using x by (auto simp: divide_simps) from ‹1 < k› have "LIM n F. (k - 1) * g n :> at_top" by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const _ g]) (simp add: field_simps) then have "eventually (λn. d ≤ (k - 1) * g n) F" by (simp add: filterlim_at_top) moreover have "eventually (λn. 1 ≤ g n) F" "eventually (λn. 1 - d ≤ g n) F" "eventually (λn. c / m - d ≤ g n) F" using g by (auto simp add: filterlim_at_top) ultimately have "eventually (λn. x ≤ u) F" using ev proof eventually_elim fix n assume d: "d ≤ (k - 1) * g n" "1 ≤ g n" "1 - d ≤ g n" "c / m - d ≤ g n" and l: "l ≤ f n / g n" and u: "(f n + c) / (g n + d) ≤ u" from d have "g n + d ≤ k * g n" by (simp add: field_simps) from d have g: "0 < g n" "0 < g n + d" by (auto simp: field_simps) with ‹0 < l› l have "0 < f n" by (auto simp: field_simps intro: mult_pos_pos less_le_trans) note ‹x = l / k + m› also have "l / k ≤ f n / (k * g n)" using l ‹1 < k› by (simp add: field_simps) also have "… ≤ f n / (g n + d)" using d ‹1 < k› ‹0 < f n› by (intro divide_left_mono mult_pos_pos) (auto simp: field_simps) also have "m ≤ c / (g n + d)" using ‹c / m - d ≤ g n› ‹0 < g n› ‹0 < g n + d› ‹m < 0› by (simp add: field_simps) also have "f n / (g n + d) + c / (g n + d) = (f n + c) / (g n + d)" using ‹0 < g n + d› by (auto simp: add_divide_distrib) also note u finally show "x ≤ u" by simp qed then show "x ≤ u" by auto qed lemma compet_lb0: fixes a Aon Aoff cruel defines "f s0 rs == real(T_on Aon s0 rs)" defines "g s0 rs == real(T_off Aoff s0 rs)" assumes "⋀rs s0. size(Aoff s0 rs) = length rs" and "⋀n. cruel n ≠ []" assumes "compet Aon c S0" and "c≥0" and "s0 ∈ S0" and l: "eventually (λn. f s0 (cruel n) / (g s0 (cruel n) + a) ≥ l) sequentially" and g: "LIM n sequentially. g s0 (cruel n) :> at_top" and "l > 0" and "⋀n. static s0 (cruel n)" shows "l ≤ c" proof- let ?h = "λb s0 rs. (f s0 rs - b) / g s0 rs" have g': "LIM n sequentially. g s0 (cruel n) + a :> at_top" using filterlim_tendsto_add_at_top[OF tendsto_const g] by (simp add: ac_simps) from competE[OF assms(5) ‹c≥0› _ ‹s0 ∈ S0›] assms(3) obtain b where "∀rs. static s0 rs ∧ rs ≠ [] ⟶ ?h b s0 rs ≤ c " by (fastforce simp del: neq0_conv simp: neq0_conv[symmetric] field_simps f_def g_def T_off_neq0[of Aoff, OF assms(3)]) hence "∀n. (?h b s0 o cruel) n ≤ c" using assms(4,11) by simp with rat_fun_lem[OF sequentially_bot ‹l>0› _ _ g', of "f s0 o cruel" "-b" "- a" c] assms(7) l show "l ≤ c" by (auto) qed text ‹Sorting› fun ins_sws where "ins_sws k x [] = []" | "ins_sws k x (y#ys) = (if k x ≤ k y then [] else map Suc (ins_sws k x ys) @ [0])" fun sort_sws where "sort_sws k [] = []" | "sort_sws k (x#xs) = ins_sws k x (sort_key k xs) @ map Suc (sort_sws k xs)" lemma length_ins_sws: "length(ins_sws k x xs) ≤ length xs" by(induction xs) auto lemma length_sort_sws_le: "length(sort_sws k xs) ≤ length xs ^ 2" proof(induction xs) case (Cons x xs) thus ?case using length_ins_sws[of k x "sort_key k xs"] by (simp add: numeral_eq_Suc) qed simp lemma swaps_ins_sws: "swaps (ins_sws k x xs) (x#xs) = insort_key k x xs" by(induction xs)(auto simp: swap_def[of 0]) lemma swaps_sort_sws[simp]: "swaps (sort_sws k xs) xs = sort_key k xs" by(induction xs)(auto simp: swaps_ins_sws) text‹The cruel adversary:› fun cruel :: "('a,'is) alg_on ⇒ 'a state * 'is ⇒ nat ⇒ 'a list" where "cruel A s 0 = []" | "cruel A s (Suc n) = last (fst s) # cruel A (Step A s (last (fst s))) n" definition adv :: "('a,'is) alg_on ⇒ ('a::linorder) alg_off" where "adv A s rs = (if rs=[] then [] else let crs = cruel A (Step A (s, fst A s) (last s)) (size rs - 1) in (0,sort_sws (λx. size rs - 1 - count_list crs x) s) # replicate (size rs - 1) (0,[]))" lemma set_cruel: "s ≠ [] ⟹ set(cruel A (s,is) n) ⊆ set s" apply(induction n arbitrary: s "is") apply(auto simp: step_def Step_def split: prod.split) by (metis empty_iff swaps_inv last_in_set list.set(1) rev_subsetD set_mtf2) lemma static_cruel: "s ≠ [] ⟹ static s (cruel A (s,is) n)" by(simp add: set_cruel static_def) (* Do not convert into structured proof - eta conversion screws it up! *) lemma T_cruel: "s ≠ [] ⟹ distinct s ⟹ T s (cruel A (s,is) n) (off2 A (s,is) (cruel A (s,is) n)) ≥ n*(length s)" apply(induction n arbitrary: s "is") apply(simp) apply(erule_tac x = "fst(Step A (s, is) (last s))" in meta_allE) apply(erule_tac x = "snd(Step A (s, is) (last s))" in meta_allE) apply(frule_tac sws = "snd(fst(snd A (s,is) (last s)))" in index_swaps_last_size) apply(simp add: distinct_step t_def split_def Step_def length_greater_0_conv[symmetric] del: length_greater_0_conv) done lemma length_cruel[simp]: "length (cruel A s n) = n" by (induction n arbitrary: s) (auto) lemma t_sort_sws: "t s r (mf, sort_sws k s) ≤ size s ^ 2 + size s + 1" using length_sort_sws_le[of k s] index_le_size[of "sort_key k s" r] by (simp add: t_def add_mono index_le_size algebra_simps) lemma T_noop: "n = length rs ⟹ T s rs (replicate n (0, [])) = (∑r←rs. index s r + 1)" by(induction rs arbitrary: s n)(auto simp: t_def step_def) lemma sorted_asc: "j≤i ⟹ i<size ss ⟹ ∀x ∈ set ss. ∀y ∈ set ss. k(x) ≤ k(y) ⟶ f y ≤ f x ⟹ sorted (map k ss) ⟹ f (ss ! i) ≤ f (ss ! j)" by (auto simp: sorted_iff_nth_mono) lemma sorted_weighted_gauss_Ico_div2: fixes f :: "nat ⇒ nat" assumes "⋀i j. i ≤ j ⟹ j < n ⟹ f i ≥ f j" shows "(∑i=0..<n. (i + 1) * f i) ≤ (n + 1) * sum f {0..<n} div 2" proof (cases n) case 0 then show ?thesis by simp next case (Suc n) with assms have "Suc n * (∑i=0..<Suc n. Suc i * f i) ≤ (∑i=0..<Suc n. Suc i) * sum f {0..<Suc n}" by (intro Chebyshev_sum_upper_nat [of "Suc n" Suc f]) auto then have "Suc n * (2 * (∑i=0..n. Suc i * f i)) ≤ 2 * (∑i=0..n. Suc i) * sum f {0..n}" by (simp add: atLeastLessThanSuc_atLeastAtMost) also have "2 * (∑i=0..n. Suc i) = Suc n * (n + 2)" using arith_series_nat [of 1 1 n] by simp finally have "2 * (∑i=0..n. Suc i * f i) ≤ (n + 2) * sum f {0..n}" by (simp only: ac_simps Suc_mult_le_cancel1) with Suc show ?thesis by (simp only: atLeastLessThanSuc_atLeastAtMost) simp qed lemma T_adv: assumes "l ≠ 0" shows "T_off (adv A) [0..<l] (cruel A ([0..<l],fst A [0..<l]) (Suc n)) ≤ l⇧^{2}+ l + 1 + (l + 1) * n div 2" (is "?l ≤ ?r") proof- let ?s = "[0..<l]" let ?r = "last ?s" let ?S' = "Step A (?s,fst A ?s) ?r" let ?s' = "fst ?S'" let ?cr = "cruel A ?S' n" let ?c = "count_list ?cr" let ?k = "λx. n - ?c x" let ?sort = "sort_key ?k ?s" have 1: "set ?s' = {0..<l}" by(simp add: set_step Step_def split: prod.split) have 3: "⋀x. x < l ⟹ ?c x ≤ n" by(simp) (metis count_le_length length_cruel) have "?l = t ?s (last ?s) (0, sort_sws ?k ?s) + (∑x∈set ?s'. ?c x * (index ?sort x + 1))" using assms apply(simp add: adv_def T_noop sum_list_map_eq_sum_count2[OF set_cruel] Step_def split: prod.split) apply(subst (3) step_def) apply(simp) done also have "(∑x∈set ?s'. ?c x * (index ?sort x + 1)) = (∑x∈{0..<l}. ?c x * (index ?sort x + 1))" by (simp add: 1) also have "… = (∑x∈{0..<l}. ?c (?sort ! x) * (index ?sort (?sort ! x) + 1))" by(rule sum.reindex_bij_betw[where ?h = "nth ?sort", symmetric]) (simp add: bij_betw_imageI inj_on_nth nth_image) also have "… = (∑x∈{0..<l}. ?c (?sort ! x) * (x+1))" by(simp add: index_nth_id) also have "… ≤ (∑x∈{0..<l}. (x+1) * ?c (?sort ! x))" by (simp add: algebra_simps) also(ord_eq_le_subst) have "… ≤ (l+1) * (∑x∈{0..<l}. ?c (?sort ! x)) div 2" apply(rule sorted_weighted_gauss_Ico_div2) apply(erule sorted_asc[where k = "λx. n - count_list (cruel A ?S' n) x"]) apply(auto simp add: index_nth_id dest!: 3) using assms [[linarith_split_limit = 20]] by simp also have "(∑x∈{0..<l}. ?c (?sort ! x)) = (∑x∈{0..<l}. ?c (?sort ! (index ?sort x)))" by(rule sum.reindex_bij_betw[where ?h = "index ?sort", symmetric]) (simp add: bij_betw_imageI inj_on_index2 index_image) also have "… = (∑x∈{0..<l}. ?c x)" by(simp) also have "… = length ?cr" using set_cruel[of ?s' A _ n] assms 1 by(auto simp add: sum_count_set Step_def split: prod.split) also have "… = n" by simp also have "t ?s (last ?s) (0, sort_sws ?k ?s) ≤ (length ?s)^2 + length ?s + 1" by(rule t_sort_sws) also have "… = l^2 + l + 1" by simp finally show "?l ≤ l⇧^{2}+ l + 1 + (l + 1) * n div 2" by auto qed text ‹The main theorem:› theorem compet_lb2: assumes "compet A c {xs::nat list. size xs = l}" and "l ≠ 0" and "c ≥ 0" shows "c ≥ 2*l/(l+1)" proof (rule compet_lb0[OF _ _ assms(1) ‹c≥0›]) let ?S0 = "{xs::nat list. size xs = l}" let ?s0 = "[0..<l]" let ?cruel = "cruel A (?s0,fst A ?s0) o Suc" let ?on = "λn. T_on A ?s0 (?cruel n)" let ?off = "λn. T_off (adv A) ?s0 (?cruel n)" show "⋀s0 rs. length (adv A s0 rs) = length rs" by(simp add: adv_def) show "⋀n. ?cruel n ≠ []" by auto show "?s0 ∈ ?S0" by simp { fix Z::real and n::nat assume "n ≥ nat(ceiling Z)" have "?off n ≥ length(?cruel n)" by(rule T_ge_len) (simp add: adv_def) hence "?off n > n" by simp hence "Z ≤ ?off n" using ‹n ≥ nat(ceiling Z)› by linarith } thus "LIM n sequentially. real (?off n) :> at_top" by(auto simp only: filterlim_at_top eventually_sequentially) let ?a = "- (l^2 + l + 1)" { fix n assume "n ≥ l^2 + l + 1" have "2*l/(l+1) = 2*l*(n+1) / ((l+1)*(n+1))" by (simp del: One_nat_def) also have "… = 2*real(l*(n+1)) / ((l+1)*(n+1))" by simp also have "l * (n+1) ≤ ?on n" using T_cruel[of ?s0 "Suc n"] ‹l ≠ 0› by (simp add: ac_simps) also have "2*real(?on n) / ((l+1)*(n+1)) ≤ 2*real(?on n)/(2*(?off n + ?a))" proof - have 0: "2*real(?on n) ≥ 0" by simp have 1: "0 < real ((l + 1) * (n + 1))" by (simp del: of_nat_Suc) have "?off n ≥ length(?cruel n)" by(rule T_ge_len) (simp add: adv_def) hence "?off n > n" by simp hence "?off n + ?a > 0" using ‹n ≥ l^2 + l + 1› by linarith hence 2: "real_of_int(2*(?off n + ?a)) > 0" by(simp only: of_int_0_less_iff zero_less_mult_iff zero_less_numeral simp_thms) have "?off n + ?a ≤ (l+1)*(n) div 2" using T_adv[OF ‹l≠0›, of A n] by (simp only: o_apply of_nat_add of_nat_le_iff) also have "… ≤ (l+1)*(n+1) div 2" by (simp) finally have "2*(?off n + ?a) ≤ (l+1)*(n+1)" by (simp add: zdiv_int) hence "of_int(2*(?off n + ?a)) ≤ real((l+1)*(n+1))" by (simp only: of_int_le_iff) from divide_left_mono[OF this 0 mult_pos_pos[OF 1 2]] show ?thesis . qed also have "… = ?on n / (?off n + ?a)" by (simp del: distrib_left_numeral One_nat_def cruel.simps) finally have "2*l/(l+1) ≤ ?on n / (real (?off n) + ?a)" by (auto simp: divide_right_mono) } thus "eventually (λn. (2 * l) / (l + 1) ≤ ?on n / (real(?off n) + ?a)) sequentially" by(auto simp add: filterlim_at_top eventually_sequentially) show "0 < 2*l / (l+1)" using ‹l ≠ 0› by(simp) show "⋀n. static ?s0 (?cruel n)" using ‹l ≠ 0› by(simp add: static_cruel del: cruel.simps) qed end

# Theory Bit_Strings

(* Title: Lemmas about lists of bools Author: Max Haslbeck *) theory Bit_Strings imports Complex_Main begin section "Lemmas about BitStrings and sets theirof" subsection "the set of bitstring of length m is finite" lemma bitstrings_finite: "finite {xs::bool list. length xs = m}" using finite_lists_length_eq[where A="UNIV"] by force subsection "how to calculate the cardinality of the set of bitstrings with certain bits already set" lemma fbool: "finite {xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ f (xs!e)}" by(rule finite_subset[where B="{xs. length xs = m}"]) (auto simp: bitstrings_finite) fun witness :: "nat set ⇒ nat ⇒ bool list" where "witness X 0 = []" |"witness X (Suc n) = (witness X n) @ [n ∈ X]" lemma witness_length: "length (witness X n) = n" apply(induct n) by auto lemma iswitness: "r<n ⟹ ((witness X n)!r) = (r∈X)" proof (induct n) case (Suc n) have "witness X (Suc n) ! r = ((witness X n) @ [n ∈ X]) ! r" by simp also have "… = (if r < length (witness X n) then (witness X n) ! r else [n ∈ X] ! (r - length (witness X n)))" by(rule nth_append) also have "… = (if r < n then (witness X n) ! r else [n ∈ X] ! (r - n))" by (simp add: witness_length) finally have 1: "witness X (Suc n) ! r = (if r < n then (witness X n) ! r else [n ∈ X] ! (r - n))" . show ?case proof (cases "r < n") case True with 1 have a: "witness X (Suc n) ! r = (witness X n) ! r" by auto from Suc True have b: "witness X n ! r = (r ∈ X)" by auto from a b show ?thesis by auto next case False with Suc have "r = n" by auto with 1 show "witness X (Suc n) ! r = (r ∈ X)" by auto qed qed simp lemma card1: "finite S ⟹ finite X ⟹ finite Y ⟹ X ∩ Y = {} ⟹ S ∩ (X ∪ Y) = {} ⟹ S∪X∪Y={0..<m} ⟹ card {xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m} = 2^(m - card X - card Y)" proof(induct arbitrary: X Y rule: finite_induct) case empty then have x: "X ⊆ {0..<m}" and y: "Y ⊆ {0..<m}" and xy: "X∪ Y = {0..<m}" by auto then have "card (X ∪ Y) = m" by auto with empty(3) have cardXY: "card X + card Y = m" using card_Un_Int[OF empty(1) empty(2)] by auto from empty have ents: "∀i<m. (i∈Y) = (i∉X)" by auto have "(∃! w. (∀i∈X. w ! i) ∧ (∀i∈Y. ¬ w ! i) ∧ length w = m)" proof (rule ex1I, goal_cases) case 1 show "(∀i∈X. (witness X m) ! i) ∧ (∀i∈Y. ¬ (witness X m) ! i) ∧ length (witness X m) = m" proof (safe, goal_cases) case (2 i) with y have a: "i < m" by auto with iswitness have "witness X m ! i = (i ∈ X)" by auto with a ents 2 have "~ witness X m ! i" by auto with 2(2) show "False" by auto next case (1 i) with x have a: "i < m" by auto with iswitness have "witness X m ! i = (i ∈ X)" by auto with a ents 1 show "witness X m ! i" by auto qed (rule witness_length) next case (2 w) show "w = witness X m" proof - have "(length w = length (witness X m) ∧ (∀i<length w. w ! i = (witness X m) ! i))" using 2 apply(simp add: witness_length) proof fix i assume as: "(∀i∈X. w ! i) ∧ (∀i∈Y. ¬ w ! i) ∧ length w = m" have "i < m ⟶ (witness X m) ! i = (i ∈ X)" using iswitness by auto then show "i < m ⟶ w ! i = (witness X m) ! i" using ents as by auto qed then show ?thesis using list_eq_iff_nth_eq by auto qed qed then obtain w where " {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m} = { w }" using Nitpick.Ex1_unfold[where P="(λxs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m)"] by auto then have "card {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m} = card { w }" by auto also have "… = 1" by auto also have "… = 2^(m - card X - card Y)" using cardXY by auto finally show ?case . next case (insert e S) then have eX: "e ∉ X" and eY: "e ∉ Y" by auto from insert(8) have "insert e S ⊆ {0..<m}" by auto then have ebetween0m: "e∈{0..<m}" by auto have fm: "finite {0..<m}" by auto have cardm: "card {0..<m} = m" by auto from insert(8) eX eY ebetween0m have sub: "X ∪ Y ⊂ {0..<m}" by auto from insert have "card (X ∩ Y) = 0" by auto then have cardXY: "card (X ∪ Y) = card X + card Y" using card_Un_Int[OF insert(4) insert(5)] by auto have " m > card X + card Y" using psubset_card_mono[OF fm sub] cardm cardXY by(auto) then have carde: "1 + ( m - card X - card Y - 1) = m - card X - card Y" by auto have is1: "{xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ xs!e} = {xs. Ball (insert e X) ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m}" by auto have is2: "{xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ ~xs!e} = {xs. Ball X ((!) xs) ∧ (∀i∈(insert e Y). ¬ xs ! i) ∧ length xs = m}" by auto have 2: "{xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ xs!e} ∪ {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ ~xs!e} = {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m}" by auto have 3: "{xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ xs!e} ∩ {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ ~xs!e} = {}" by auto have fX: "finite (insert e X)" and disjeXY: "insert e X ∩ Y = {}" and cutX: "S ∩ (insert e X ∪ Y) = {}" and uniX: "S ∪ insert e X ∪ Y = {0..<m}" using insert by auto have fY: "finite (insert e Y)" and disjXeY: "X ∩ (insert e Y) = {}" and cutY: "S ∩ (X ∪ insert e Y) = {}" and uniY: "S ∪ X ∪ insert e Y = {0..<m}" using insert by auto have "card {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m} = card {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ xs!e} + card {xs. Ball X ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m ∧ ~xs!e}" apply(subst card_Un_Int) apply(rule fbool) apply(rule fbool) using 2 3 by auto also have "… = card {xs. Ball (insert e X) ((!) xs) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m} + card {xs. Ball X ((!) xs) ∧ (∀i∈(insert e Y). ¬ xs ! i) ∧ length xs = m}" by (simp only: is1 is2) also have "… = 2 ^ ( m - card (insert e X) - card Y) + 2 ^ ( m - card X - card (insert e Y))" apply(simp only: insert(3)[of "insert e X" Y, OF fX insert(5) disjeXY cutX uniX]) by(simp only: insert(3)[of "X" "insert e Y", OF insert(4) fY disjXeY cutY uniY]) also have "… = 2 ^ ( m - card X - card Y - 1) + 2 ^ ( m - card X - card Y - 1)" using insert(4,5) eX eY by auto also have "… = 2 * 2 ^ ( m - card X - card Y - 1)" by auto also have "… = 2 ^ (1 + ( m - card X - card Y - 1))" by auto also have "… = 2 ^ ( m - card X - card Y)" using carde by auto finally show ?case . qed lemma card2: assumes "finite X" and "finite Y" and "X ∩ Y = {}" and x: "X ∪ Y ⊆ {0..<m}" shows "card {xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = m} = 2 ^ (m - card X - card Y)" proof - let ?S = "{0..<m}-(X ∪ Y)" from x have a: "?S ∪ X ∪ Y = {0..<m}" by auto have b: "?S ∩ (X ∪ Y) = {}" by auto show ?thesis apply(rule card1[where ?S="?S"]) by(simp_all add: assms a b) qed subsection "Average out the second sum for free-absch" lemma Expactation2or1: "finite S ⟹ finite Tr ⟹ finite Fa ⟹ card Tr + card Fa + card S ≤ l ⟹ S ∩ (Tr ∪ Fa) = {} ⟹ Tr ∩ Fa = {} ⟹ S ∪ Tr ∪ Fa ⊆ {0..<l} ⟹ (∑x∈{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l}. ∑j∈S. if x ! j then 2 else 1) = 3 / 2 * real (card S) * 2 ^ (l - card Tr - card Fa)" proof (induct arbitrary: Tr Fa rule: finite_induct) case (insert e S) from insert(7) have "e ∈ (insert e S)" and eTr: "e ∉ Tr" and eFa: "e ∉ Fa" by auto from insert(9) have tra: "Tr ⊆ {0..<l}" and trb: "Fa ⊆ {0..<l}" and trc: "e < l" by auto have ntrFa: "l > (card Tr + card Fa)" using insert(6) card_insert_if insert(1,2) by auto have myhelp2: "1 + (l - card Tr - card Fa -1) = l - card Tr - card Fa" using ntrFa by auto have juhuTr: "{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l ∧ xs!e} = {xs. (∀i∈(insert e Tr). xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l}" by auto have juhuFa: "{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l ∧ ~xs!e} = {xs. (∀i∈Tr. xs ! i) ∧ (∀i∈(insert e Fa). ¬ xs ! i) ∧ length xs = l}" by auto let ?Tre = "{xs. (∀i∈(insert e Tr). xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l}" have "card ?Tre = 2 ^ (l - card (insert e Tr) - card Fa)" apply(rule card2) using insert by simp_all then have resi: "card ?Tre = 2^(l - card Tr - card Fa - 1)" using insert(4) eTr by auto have yabaTr: "(∑x∈?Tre. 2::real) = 2 * 2^(l - card Tr - card Fa - 1)" using resi by (simp add: power_commutes) let ?Fae = "{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈(insert e Fa). ¬ xs ! i) ∧ length xs = l}" have "card ?Fae = 2 ^ (l - card Tr - card (insert e Fa))" apply(rule card2) using insert by simp_all then have resi2: "card ?Fae = 2^(l - card Tr - card Fa - 1)" using insert(5) eFa by auto have yabaFa: "(∑x∈?Fae. 1::real) = 1 * 2 ^ (l - card Tr - card Fa - 1)" using resi2 by (simp add: power_commutes) { fix X Y have "{xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = l ∧ xs!e} ∩ {xs. (∀i∈X. xs ! i) ∧ (∀i∈Y. ¬ xs ! i) ∧ length xs = l ∧ ~xs!e} = {}" by auto } note 3=this (* split it! *) have "(∑x∈{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l}. ∑j∈(insert e S). if x ! j then (2::real) else 1) = (∑x∈{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l ∧ xs!e}. ∑j∈(insert e S). if x ! j then 2 else 1) + (∑x∈{xs. (∀i∈Tr. xs ! i) ∧ (∀i∈Fa. ¬ xs ! i) ∧ length xs = l ∧ ~xs!e}. ∑j∈(insert e S). if x ! j then 2 else 1)" (is "(∑x∈?all. ?f x) = (∑x∈?allT. ?f x) + (∑x∈?allF. ?f x)") proof - have "(∑x∈?all. ∑j∈(insert e S). if x ! j then 2 else 1) = (∑x∈(?allT ∪ ?allF). ∑j∈(insert e S). if x ! j then 2 else 1)" apply(rule sum.cong) by(auto) also have"… = ((∑x∈(?allT). ∑j∈(insert e S). if x ! j then (2::real) else 1) + (∑x∈(?allF). ∑j∈(insert e S). if x ! j then (2::real) else 1)) - (∑x∈(?allT ∩ ?allF). ∑j∈(insert e S). if x ! j then 2 else 1)" apply (rule sum_Un) apply(rule fbool)+ done also have "… = (∑x∈(?allT). ∑j∈(insert e S). if x ! j then 2 else 1) + (∑x∈(?allF). ∑j∈(insert e S). if x ! j then 2 else 1)" by(simp add: 3) finally show ?thesis . qed also have "… = (∑x∈?Tre. ∑j∈(insert e S). if x ! j then 2 else 1) + (∑x∈?Fae. ∑j∈(insert e S). if x ! j then 2 else 1)" using juhuTr juhuFa by auto also have "… = (∑x∈?Tre. (λx. 2) x + (λx. (∑j∈S. if x ! j then 2 else 1)) x) + (∑x∈?Fae. (λx. 1) x + (λx. (∑j∈S. if x ! j then 2 else 1)) x)" using insert(1,2) by auto also have "… = (∑x∈?Tre. 2) + (∑x∈?Tre. (∑j∈S. if x ! j then 2 else 1)) + ((∑x∈?Fae. 1) + (∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1)))" by (simp add: Groups_Big.comm_monoid_add_class.sum.distrib) also have "… = 2 * 2^(l - card Tr - card Fa - 1) + (∑x∈?Tre. (∑j∈S. if x ! j then 2 else 1)) + (1 * 2^(l - card Tr - card Fa - 1) + (∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1)))" by(simp only: yabaTr yabaFa) also have "… = (2::real) * 2^(l - card Tr - card Fa - 1) + (∑x∈?Tre. (∑j∈S. if x ! j then 2 else 1)) + (1::real) * 2^(l - card Tr - card Fa - 1) + (∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1))" by auto also have "… = (3::real) * 2^(l - card Tr - card Fa - 1) + (∑x∈?Tre. (∑j∈S. if x ! j then 2 else 1)) + (∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1))" by simp also have "… = 3 * 2^(l - card Tr - card Fa - 1) + 3 / 2 * real (card S) * 2 ^ (l - card (insert e Tr) - card Fa) + (∑x∈?Fae. (∑j∈S. if x ! j then 2 else 1))" apply(subst insert(3)) using insert by simp_all also have "… = 3 * 2^(l - card Tr - card Fa - 1) + 3 / 2 * real (card S) * 2 ^ (l - card (insert e Tr) - card Fa) + 3 / 2 * real (card S) * 2 ^ (l - card Tr - card (insert e Fa))" apply(subst insert(3)) using insert by simp_all also have "… = 3 * 2^(l - card Tr - card Fa - 1) + 3 / 2 * real (card S) * 2^ (l - (card Tr + 1) - card Fa) + 3 / 2 * real (card S) * 2^ (l - card Tr - (card Fa + 1))" using card_insert_if insert(4,5) eTr eFa by auto also have "… = 3 * 2^(l - card Tr - card Fa - 1) + 3 / 2 * real (card S) * 2^ (l - card Tr - card Fa - 1) + 3 / 2 * real (card S) * 2^ (l - card Tr - card Fa - 1)" by auto also have "… = ( 3/2 * 2 + 2 * 3 / 2 * real (card S)) * 2^ (l - card Tr - card Fa - 1)" by algebra also have "… = ( 3 / 2 * (1 + real (card S))) * 2 * 2^ (l - card Tr - card Fa - 1 )" by simp also have "… = ( 3 / 2 * (1 + real (card S))) * 2^ (Suc (l - card Tr - card Fa -1 ))" by simp also have "… = ( 3 / 2 * (1 + real (card S))) * 2^ (l - card Tr - card Fa )" using myhelp2 by auto also have "… = ( 3 / 2 * (real (1 + card S))) * 2^ (l - card Tr - card Fa )" by simp also have "… = ( 3 / 2 * real (card (insert e S))) * 2^ (l - card Tr - card Fa)" using insert(1,2) by auto finally show ?case . qed simp end

# Theory MTF2_Effects

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