Theory Partial_Cost_Model

(*  Title:       The Partial Cost Model of the List Update Problem
    Author:      Max Haslbeck
*)

section "Partial cost model"

theory Partial_Cost_Model
imports Move_to_Front
begin

definition t⇩p :: "'a state ⇒ 'a ⇒ answer ⇒ nat" where
"t⇩p s q a = (let (mf,sws) = a in index (swaps sws s) q + size sws)"

notation (latex) t⇩p (‹\<^latex>‹$t^{*}$››)

lemma t⇩pt: "t⇩p s q a + 1 = t s q a" unfolding t⇩p_def t_def by(simp add: split_def)

interpretation On_Off step t⇩p static .
                 
abbreviation "T⇩p == T"
abbreviation "T⇩p_opt == T_opt" 
abbreviation "T⇩p_on == T_on"
abbreviation "T⇩p_on_rand' == T_on_rand'"
abbreviation "T⇩p_on_n == T_on_n"
abbreviation "T⇩p_on_rand == T_on_rand"
abbreviation "T⇩p_on_rand_n == T_on_rand_n"
abbreviation "config⇩p == config "
abbreviation "compet⇩p == compet"
                                            


end