# Theory Competitive_Analysis

theory Competitive_Analysis
imports Prob_Theory On_Off
```(*  Title:       The Framework for competitive Analysis of randomized online algorithms
Author:      Tobias Nipkow
Max Haslbeck
*)

section "Randomized Online and Offline Algorithms"

theory Competitive_Analysis
imports
Prob_Theory
On_Off
begin

subsection "Competitive Analysis Formalized"

type_synonym ('s,'is,'r,'a)alg_on_step = "('s * 'is  ⇒ 'r ⇒ ('a * 'is) pmf)"
type_synonym ('s,'is)alg_on_init = "('s ⇒ 'is pmf)"
type_synonym ('s,'is,'q,'a)alg_on_rand = "('s,'is)alg_on_init * ('s,'is,'q,'a)alg_on_step"

subsubsection "classes of algorithms"

definition deterministic_init :: "('s,'is)alg_on_init ⇒ bool" where
"deterministic_init I ⟷ (∀init. card( set_pmf (I init)) = 1)"

definition deterministic_step :: "('s,'is,'q,'a)alg_on_step ⇒ bool" where
"deterministic_step S ⟷ (∀i is q. card( set_pmf (S (i, is) q)) = 1)"

definition random_step :: "('s,'is,'q,'a)alg_on_step ⇒ bool" where
"random_step S ⟷ ~ deterministic_step S"

subsubsection "Randomized Online and Offline Algorithms"

context On_Off
begin

fun steps where
"steps s [] [] = s"
| "steps s (q#qs) (a#as) = steps (step s q a) qs as"

lemma steps_append: "length qs = length as ⟹ steps s (qs@qs') (as@as') = steps (steps s qs as) qs' as'"
apply(induct qs as arbitrary: s rule: list_induct2)
by simp_all

lemma T_append: "length qs = length as ⟹ T s (qs@[q]) (as@[a]) = T s qs as + t (steps s qs as) q a"
apply(induct qs as arbitrary: s rule: list_induct2)
by simp_all

lemma T_append2: "length qs = length as ⟹ T s (qs@qs') (as@as') = T s qs as + T (steps s qs as) qs' as'"
apply(induct qs as arbitrary: s rule: list_induct2)
by simp_all

abbreviation Step_rand :: "('state,'is,'request,'answer) alg_on_rand  ⇒ 'request ⇒ 'state * 'is ⇒ ('state * 'is) pmf" where
"Step_rand A r s ≡ bind_pmf ((snd A) s r) (λ(a,is'). return_pmf (step (fst s) r a, is'))"

fun config'_rand :: "('state,'is,'request,'answer) alg_on_rand  ⇒ ('state*'is) pmf ⇒ 'request list
⇒ ('state * 'is) pmf" where
"config'_rand A s []  = s" |
"config'_rand A s (r#rs) = config'_rand A (s ⤜ Step_rand A r) rs"

lemma config'_rand_snoc: "config'_rand A s (rs@[r]) = config'_rand A s rs ⤜ Step_rand A r"
apply(induct rs arbitrary: s) by(simp_all)

lemma config'_rand_append: "config'_rand A s (xs@ys) = config'_rand A (config'_rand A s xs) ys"
apply(induct xs arbitrary: s) by(simp_all)

abbreviation config_rand where
"config_rand A s0 rs == config'_rand A ((fst A s0) ⤜ (λis. return_pmf (s0, is))) rs"

lemma config'_rand_induct: "(∀x ∈ set_pmf init. P (fst x)) ⟹ (⋀s q a. P s ⟹ P (step s q a))
⟹ ∀x∈set_pmf (config'_rand A init qs). P (fst x)"
proof (induct qs arbitrary: init)
case (Cons r rs)
show ?case apply(simp)
apply(rule Cons(1))
apply(subst Set.ball_simps(9)[where P=P, symmetric])
apply(subst set_map_pmf[symmetric])
apply(simp only: map_bind_pmf)
using Cons(2,3) apply blast
by fact
qed (simp)

lemma config_rand_induct: "P s0 ⟹ (⋀s q a. P s ⟹ P (step s q a)) ⟹ ∀x∈set_pmf (config_rand A s0 qs). P (fst x)"
using config'_rand_induct[of "((fst A s0) ⤜ (λis. return_pmf (s0, is)))" P] by auto

fun T_on_rand' :: "('state,'is,'request,'answer) alg_on_rand ⇒ ('state*'is) pmf ⇒ 'request list ⇒  real" where
"T_on_rand' A s [] = 0" |
"T_on_rand' A s (r#rs) = E ( s ⤜ (λs. bind_pmf (snd A s r) (λ(a,is'). return_pmf (real (t (fst s) r a)))) )
+ T_on_rand' A (s ⤜ Step_rand A r) rs"

lemma T_on_rand'_append: "T_on_rand' A s (xs@ys) = T_on_rand' A s xs + T_on_rand' A (config'_rand A s xs) ys"
apply(induct xs arbitrary: s) by simp_all

abbreviation T_on_rand :: "('state,'is,'request,'answer) alg_on_rand ⇒ 'state ⇒ 'request list ⇒ real" where
"T_on_rand A s rs == T_on_rand' A (fst A s ⤜ (λis. return_pmf (s,is))) rs"

lemma T_on_rand_append: "T_on_rand A s (xs@ys) = T_on_rand A s xs + T_on_rand' A (config_rand A s xs) ys"
by(rule T_on_rand'_append)

abbreviation "T_on_rand'_n A s0 xs n == T_on_rand' A (config'_rand A s0 (take n xs)) [xs!n]"

lemma T_on_rand'_as_sum: "T_on_rand' A s0 rs = sum (T_on_rand'_n A s0 rs) {..<length rs} "
apply(induct rs rule: rev_induct)

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)

lemma T_on_rand'_nn: "T_on_rand' A s qs ≥ 0"
apply(induct qs arbitrary: s)
apply(rule E_nonneg)

lemma T_on_rand_nn: "T_on_rand (I,S) s0 qs ≥ 0"
by (rule T_on_rand'_nn)

definition compet_rand :: "('state,'is,'request,'answer) alg_on_rand ⇒ real ⇒ 'state set ⇒ bool" where
"compet_rand A c S0 = (∀s∈S0. ∃b ≥ 0. ∀rs. wf s rs ⟶ T_on_rand A s rs ≤ c * T_opt s rs + b)"

subsection "embeding of deterministic into randomized algorithms"

"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(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
```