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 tp :: "'a state  'a  answer  nat" where
"tp s q a = (let (mf,sws) = a in index (swaps sws s) q + size sws)"

notation (latex) tp ("latex‹$t^{*}$›")

lemma tpt: "tp s q a + 1 = t s q a" unfolding tp_def t_def by(simp add: split_def)

interpretation On_Off step tp static .
                 
abbreviation "Tp == T"
abbreviation "Tp_opt == T_opt" 
abbreviation "Tp_on == T_on"
abbreviation "Tp_on_rand' == T_on_rand'"
abbreviation "Tp_on_n == T_on_n"
abbreviation "Tp_on_rand == T_on_rand"
abbreviation "Tp_on_rand_n == T_on_rand_n"
abbreviation "configp == config "
abbreviation "competp == compet"
                                            


end