Theory Amortized_Examples
section "Simple Examples"
theory Amortized_Examples
imports Amortized_Framework
begin
text‹
This theory applies the amortized analysis framework to a number
of simple classical examples.›
subsection "Binary Counter"
locale Bin_Counter
begin
datatype op = Empty | Incr
fun arity :: "op ⇒ nat" where
"arity Empty = 0" |
"arity Incr = 1"
fun incr :: "bool list ⇒ bool list" where
"incr [] = [True]" |
"incr (False#bs) = True # bs" |
"incr (True#bs) = False # incr bs"
fun t⇩i⇩n⇩c⇩r :: "bool list ⇒ nat" where
"t⇩i⇩n⇩c⇩r [] = 1" |
"t⇩i⇩n⇩c⇩r (False#bs) = 1" |
"t⇩i⇩n⇩c⇩r (True#bs) = t⇩i⇩n⇩c⇩r bs + 1"
definition Φ :: "bool list ⇒ real" where
"Φ bs = length(filter id bs)"
lemma a_incr: "t⇩i⇩n⇩c⇩r bs + Φ(incr bs) - Φ bs = 2"
apply(induction bs rule: incr.induct)
apply (simp_all add: Φ_def)
done
fun exec :: "op ⇒ bool list list ⇒ bool list" where
"exec Empty [] = []" |
"exec Incr [bs] = incr bs"
fun cost :: "op ⇒ bool list list ⇒ nat" where
"cost Empty _ = 1" |
"cost Incr [bs] = t⇩i⇩n⇩c⇩r bs"
interpretation Amortized
where exec = exec and arity = arity and inv = "λ_. True"
and cost = cost and Φ = Φ and U = "λf _. case f of Empty ⇒ 1 | Incr ⇒ 2"
proof (standard, goal_cases)
case 1 show ?case by simp
next
case 2 show ?case by(simp add: Φ_def)
next
case 3 thus ?case using a_incr by(auto simp: Φ_def split: op.split)
qed
end
subsection "Stack with multipop"
locale Multipop
begin