Session List_Update

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: "iset 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; iset 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; iset 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 = (sS. 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 "b0. rs.  wf s0 rs  ?compt s0 rs b c'" using b0 by(auto)
qed

lemma competE: fixes c :: real
assumes "compet A c S0" "c  0" "s0 rs. size(aoff s0 rs) = length rs" "s0S0"
shows "b0. rs. wf s0 rs  T_on A s0 rs  c * T_off aoff s0 rs + b"
proof -
  from assms(1,4) obtain b where "b0" 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 b0 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 "(xset_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::"'areal"
  shows "(xset_pmf X. 0f 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) = (xset_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 " = (xset_pmf X. pmf X x * f x)"
    by (subst integral_measure_pmf) (auto simp add: finite)
  finally show ?thesis .
qed

lemma E_bernoulli: "0p  p1 
        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))
      xset_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))  xset_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 = (sS0. 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. zS) 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 xS 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: "xS  Lxy [x] S = [x]"
by(simp add: Lxy_def)



lemma Lxy_project: 
  assumes "xy" "x  set xs"  "yset 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 ylength (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: "xy" 
  {
    fix x y
    assume 1: "{x,y}  set xs" 
    assume xny: "xy"
    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: "xset_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 "c0" 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) c0 _ 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, [])) = (rrs. index s r + 1)"
by(induction rs arbitrary: s n)(auto simp: t_def step_def)


lemma sorted_asc: "ji  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))
   l2 + 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) + (xset ?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 "(xset ?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  l2 + 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) c0])
  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 l0, 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. (iX. xs ! i)  (iY. ¬ 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) = (rX)"
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) = {}  SXY={0..<m}  
    card {xs. (iX. xs ! i)  (iY. ¬ 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. (iY) = (iX)" by auto

  have "(∃! w. (iX. w ! i)  (iY. ¬ w ! i)   length w = m)"
  proof (rule ex1I, goal_cases)
    case 1
    show "(iX. (witness X m) ! i)  (iY. ¬ (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: "(iX. w ! i)  (iY. ¬ 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)  (iY. ¬ xs ! i)   length xs = m}
         = { w }" using Nitpick.Ex1_unfold[where P="(λxs. Ball X ((!) xs)  (iY. ¬ xs ! i)   length xs = m)"]
         by auto

  then have "card {xs. Ball X ((!) xs)  (iY. ¬ 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)  (iY. ¬ xs ! i)  length xs =   m  xs!e}
          = {xs. Ball (insert e X) ((!) xs)  (iY. ¬ xs ! i)  length xs =   m}" by auto
  have is2: "{xs. Ball X ((!) xs)  (iY. ¬ 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)  (iY. ¬ xs ! i)  length xs =   m  xs!e}
         {xs. Ball X ((!) xs)  (iY. ¬ xs ! i)  length xs =   m  ~xs!e}
          = {xs. Ball X ((!) xs)  (iY. ¬ xs ! i)  length xs =   m}" by auto

  have 3: "{xs. Ball X ((!) xs)  (iY. ¬ xs ! i)  length xs =   m  xs!e}
       {xs. Ball X ((!) xs)  (iY. ¬ 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)  (iY. ¬ xs ! i)  length xs = m}
      = card {xs. Ball X ((!) xs)  (iY. ¬ xs ! i)  length xs = m  xs!e}
        + card {xs. Ball X ((!) xs)  (iY. ¬ 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)  (iY. ¬ 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. (iX. xs ! i)  (iY. ¬ 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. (iTr. xs ! i)  (iFa. ¬ xs ! i)  length xs = l}. jS. 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. (iTr. xs ! i)  (iFa. ¬ xs ! i)  length xs = l  xs!e}  
      = {xs. (i(insert e Tr). xs ! i)  (iFa. ¬ xs ! i)  length xs = l}"
       by auto
  have juhuFa: "{xs. (iTr. xs ! i)  (iFa. ¬ xs ! i)  length xs = l  ~xs!e}  
      = {xs. (iTr. xs ! i)  (i(insert e Fa). ¬ xs ! i)  length xs = l}"
       by auto

  let ?Tre = "{xs. (i(insert e Tr). xs ! i)  (iFa. ¬ 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. (iTr. 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. (iX. xs ! i)  (iY. ¬ xs ! i)  length xs = l  xs!e}
           {xs. (iX. xs ! i)  (iY. ¬ xs ! i)  length xs = l  ~xs!e} = {}" by auto
  } note 3=this

  (* split it! *)
  have "(x{xs. (iTr. xs ! i)  (iFa. ¬ xs ! i)  length xs = l}. j(insert e S). if x ! j then (2::real) else 1)
      = (x{xs. (iTr. xs ! i)  (iFa. ¬ xs ! i)  length xs = l  xs!e}. j(insert e S). if x ! j then 2 else 1)
        + (x{xs. (iTr. xs ! i)  (iFa. ¬ 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. (jS. if x ! j then 2 else 1)) x)
        + (x?Fae. (λx. 1) x + (λx. (jS. if x ! j then 2 else 1)) x)" 
        using insert(1,2) by auto
  also
  have " =  (x?Tre. 2) + (x?Tre. (jS. if x ! j then 2 else 1))
          + ((x?Fae. 1) + (x?Fae. (jS. 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. (jS. if x ! j then 2 else 1))
        + (1 * 2^(l - card Tr - card Fa - 1) + (x?Fae. (jS. 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. (jS. if x ! j then 2 else 1))
        + (1::real) * 2^(l - card Tr - card Fa - 1) + (x?Fae. (jS. if x ! j then 2 else 1))" 
        by auto
  also          
  have " =  (3::real) * 2^(l - card Tr - card Fa - 1) +
          (x?Tre. (jS. if x ! j then 2 else 1)) + (x?Fae. (jS. 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. (jS. 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