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 (* Bin_Counter *)


subsection "Stack with multipop"

locale Multipop
begin

datatype 'a op = Empty | Push 'a | Pop nat

fun arity :: "'a op ⇒ nat" where
"arity Empty = 0" |
"arity (Push _) = 1" |
"arity (Pop _) = 1"

fun exec :: "'a op ⇒ 'a list list ⇒ 'a list" where
"exec Empty [] = []" |
"exec (Push x) [xs] = x # xs" |
"exec (Pop n) [xs] = drop n xs"

fun cost :: "'a op ⇒ 'a list list ⇒ nat" where
"cost Empty _ = 1" |
"cost (Push x) _ = 1" |
"cost (Pop n) [xs] = min n (length xs)"


interpretation Amortized
where arity = arity and exec = exec and inv = "λ_. True"
and cost = cost and Φ = "length"
and U = "λf _. case f of Empty ⇒ 1 | Push _ ⇒ 2 | Pop _ ⇒ 0"
proof (standard, goal_cases)
  case 1 show ?case by simp
next
  case 2 thus ?case by simp
next
  case 3 thus ?case by (auto split: op.split)
qed

end (* Multipop *)


subsection "Dynamic tables: insert only"

locale Dyn_Tab1
begin

type_synonym tab = "nat × nat"

datatype op = Empty | Ins

fun arity :: "op ⇒ nat" where
"arity Empty = 0" |
"arity Ins = 1"

fun exec :: "op ⇒ tab list ⇒ tab" where
"exec Empty [] = (0::nat,0::nat)" |
"exec Ins [(n,l)] = (n+1, if n<l then l else if l=0 then 1 else 2*l)"

fun cost :: "op ⇒ tab list ⇒ nat" where
"cost Empty _ = 1" |
"cost Ins [(n,l)] = (if n<l then 1 else n+1)"

interpretation Amortized
where exec = exec and arity = arity
and inv = "λ(n,l). if l=0 then n=0 else n ≤ l ∧ l < 2*n"
and cost = cost and Φ = "λ(n,l). 2*n - l"
and U = "λf _. case f of Empty ⇒ 1 | Ins ⇒ 3"
proof (standard, goal_cases)
  case (1 _ f) thus ?case by(cases f) (auto split: if_splits)
next
  case 2 thus ?case by(auto split: prod.splits)
next
  case 3 thus ?case by (auto split: op.split) 
qed

end (* Dyn_Tab1 *)

locale Dyn_Tab2 =
fixes a :: real
fixes c :: real
assumes c1[arith]: "c > 1" 
assumes ac2: "a ≥ c/(c - 1)"
begin

lemma ac: "a ≥ 1/(c - 1)"
using ac2 by(simp add: field_simps)

lemma a0[arith]: "a>0"
proof-
  have "1/(c - 1) > 0" using ac by simp
  thus ?thesis by (metis ac dual_order.strict_trans1)
qed

definition "b = 1/(c - 1)"

lemma b0[arith]: "b > 0"
using ac by (simp add: b_def)

type_synonym tab = "nat × nat"

datatype op = Empty | Ins

fun arity :: "op ⇒ nat" where
"arity Empty = 0" |
"arity Ins = 1"

fun "ins" :: "tab ⇒ tab" where
"ins(n,l) = (n+1, if n<l then l else if l=0 then 1 else nat(ceiling(c*l)))"

fun exec :: "op ⇒ tab list ⇒ tab" where
"exec Empty [] = (0::nat,0::nat)" |
"exec Ins [s] = ins s" |
"exec _ _ = (0,0)" (* otherwise fun goes wrong with odd error msg *)

fun cost :: "op ⇒ tab list ⇒ nat" where
"cost Empty _ = 1" |
"cost Ins [(n,l)] = (if n<l then 1 else n+1)"

fun Φ :: "tab ⇒ real" where
"Φ(n,l) = a*n - b*l"

interpretation Amortized
where exec = exec and arity = arity
and inv = "λ(n,l). if l=0 then n=0 else n ≤ l ∧ (b/a)*l ≤ n"
and cost = cost and Φ = Φ and U = "λf _. case f of Empty ⇒ 1 | Ins ⇒ a + 1"
proof (standard, goal_cases)
  case (1 ss f)
  show ?case
  proof (cases f)
    case Empty thus ?thesis using 1 by auto
  next
    case [simp]: Ins
    obtain n l where [simp]: "ss = [(n,l)]" using 1(2) by (auto)
    show ?thesis
    proof cases
      assume "l=0" thus ?thesis using 1 ac
        by (simp add: b_def field_simps)
    next
      assume "l≠0"
      show ?thesis
      proof cases
        assume "n<l"
        thus ?thesis using 1 by(simp add: algebra_simps)
      next
        assume "¬ n<l"
        hence [simp]: "n=l" using 1 ‹l≠0› by simp
        have 1: "(b/a) * ceiling(c * l) ≤ real l + 1"
        proof-
          have "(b/a) * ceiling(c * l) = ceiling(c * l)/(a*(c - 1))"
            by(simp add: b_def)
          also have "ceiling(c * l) ≤ c*l + 1" by simp
          also have "… ≤ c*(real l+1)" by (simp add: algebra_simps)
          also have "… / (a*(c - 1)) = (c/(a*(c - 1))) * (real l + 1)" by simp
          also have "c/(a*(c - 1)) ≤ 1" using ac2 by (simp add: field_simps)
          finally show ?thesis by (simp add: divide_right_mono)
        qed
        have 2: "real l + 1 ≤ ceiling(c * real l)"
          by (metis ‹l ≠ 0› c1 int_less_real_le less_ceiling_iff mult_less_cancel_right1 of_int_of_nat_eq of_nat_le_0_iff)
        from ‹l≠0› 1 2 show ?thesis by simp 
      qed
    qed
  qed
next
  case 2 thus ?case by(auto simp: field_simps split: if_splits prod.splits)
next
  case (3 ss f)
  show ?case
  proof (cases f)
    case Empty thus ?thesis using 3(2) by simp
  next
    case [simp]: Ins
    obtain n l where [simp]: "ss = [(n,l)]" using 3(2) by (auto)
    show ?thesis
    proof cases
      assume "l=0" thus ?thesis using 3 by (simp)
    next
      assume [arith]: "l≠0"
      show ?thesis
      proof cases
        assume "n<l"
        thus ?thesis using 3 ac by(simp add: algebra_simps b_def)
      next
        assume "¬ n<l"
        hence [simp]: "n=l" using 3 by simp
        have "cost Ins [(n,l)] + Φ (ins (n,l)) - Φ(n,l) = l + a + 1 + (- b*ceiling(c*l)) + b*l"
          using ‹l≠0›
          by(simp add: algebra_simps less_trans[of "-1::real" 0])
        also have "- b * ceiling(c*l) ≤ - b * (c*l)" by (simp add: ceiling_correct)
        also have "l + a + 1 + - b*(c*l) + b*l = a + 1 + l*(1 - b*(c - 1))"
          by (simp add: algebra_simps)
        also have "b*(c - 1) = 1" by(simp add: b_def)
        also have "a + 1 + (real l)*(1 - 1) = a+1" by simp
        finally show ?thesis by simp
      qed
    qed
  qed
qed

end (* Dyn_Tab2 *)


subsection "Dynamic tables: insert and delete"

locale Dyn_Tab3
begin

type_synonym tab = "nat × nat"

datatype op = Empty | Ins | Del

fun arity :: "op ⇒ nat" where
"arity Empty = 0" |
"arity Ins = 1" |
"arity Del = 1"

fun exec :: "op ⇒ tab list ⇒ tab" where
"exec Empty [] = (0::nat,0::nat)" |
"exec Ins [(n,l)] = (n+1, if n<l then l else if l=0 then 1 else 2*l)" |
"exec Del [(n,l)] = (n-1, if n≤1 then 0 else if 4*(n - 1)<l then l div 2 else l)"

fun cost :: "op ⇒ tab list ⇒ nat" where
"cost Empty _ = 1" |
"cost Ins [(n,l)] = (if n<l then 1 else n+1)" |
"cost Del [(n,l)] = (if n≤1 then 1 else if 4*(n - 1)<l then n else 1)"

interpretation Amortized
where arity = arity and exec = exec
and inv = "λ(n,l). if l=0 then n=0 else n ≤ l ∧ l ≤ 4*n"
and cost = cost and Φ = "(λ(n,l). if 2*n < l then l/2 - n else 2*n - l)"
and U = "λf _. case f of Empty ⇒ 1 | Ins ⇒ 3 | Del ⇒ 2"
proof (standard, goal_cases)
  case (1 _ f) thus ?case by (cases f) (auto split: if_splits)
next
  case 2 thus ?case by(auto split: prod.splits)
next
  case (3 _ f) thus ?case
    by (cases f)(auto simp: field_simps split: prod.splits)
qed

end (* Dyn_Tab3 *)


subsection "Queue"

text‹See, for example, the book by Okasaki~\<^cite>‹"Okasaki"›.›

locale Queue
begin

datatype 'a op = Empty | Enq 'a | Deq

type_synonym 'a queue = "'a list * 'a list"

fun arity :: "'a op ⇒ nat" where
"arity Empty = 0" |
"arity (Enq _) = 1" |
"arity Deq = 1"

fun exec :: "'a op ⇒ 'a queue list ⇒ 'a queue" where
"exec Empty [] = ([],[])" |
"exec (Enq x) [(xs,ys)] = (x#xs,ys)" |
"exec Deq [(xs,ys)] = (if ys = [] then ([], tl(rev xs)) else (xs,tl ys))"

fun cost :: "'a op ⇒ 'a queue list ⇒ nat" where
"cost Empty _ = 0" |
"cost (Enq x) [(xs,ys)] = 1" |
"cost Deq [(xs,ys)] = (if ys = [] then length xs else 0)"

interpretation Amortized
where arity = arity and exec = exec and inv = "λ_. True"
and cost = cost and Φ = "λ(xs,ys). length xs"
and U = "λf _. case f of Empty ⇒ 0 | Enq _ ⇒ 2 | Deq ⇒ 0"
proof (standard, goal_cases)
  case 1 show ?case by simp
next
  case 2 thus ?case by (auto split: prod.splits)
next
  case 3 thus ?case by(auto split: op.split)
qed

end (* Queue *)

locale Queue2
begin

datatype 'a op = Empty | Enq 'a | Deq

type_synonym 'a queue = "'a list * 'a list"

fun arity :: "'a op ⇒ nat" where
"arity Empty = 0" |
"arity (Enq _) = 1" |
"arity Deq = 1"

fun adjust :: "'a queue ⇒ 'a queue" where
"adjust(xs,ys) = (if ys = [] then ([], rev xs) else (xs,ys))"

fun exec :: "'a op ⇒ 'a queue list ⇒ 'a queue" where
"exec Empty [] = ([],[])" |
"exec (Enq x) [(xs,ys)] = adjust(x#xs,ys)" |
"exec Deq [(xs,ys)] = adjust (xs, tl ys)"

fun cost :: "'a op ⇒ 'a queue list ⇒ nat" where
"cost Empty _ = 0" |
"cost (Enq x) [(xs,ys)] = 1 + (if ys = [] then size xs + 1 else 0)" |
"cost Deq [(xs,ys)] = (if tl ys = [] then size xs else 0)"

interpretation Amortized
where arity = arity and exec = exec
and inv = "λ_. True"
and cost = cost and Φ = "λ(xs,ys). size xs"
and U = "λf _. case f of Empty ⇒ 0 | Enq _ ⇒ 2 | Deq ⇒ 0"
proof (standard, goal_cases)
  case (1 _ f) thus ?case by (cases f) (auto split: if_splits)
next
  case 2 thus ?case by (auto)
next
  case (3 _ f) thus ?case by(cases f) (auto split: if_splits)
qed

end (* Queue2 *)

locale Queue3
begin

datatype 'a op = Empty | Enq 'a | Deq

type_synonym 'a queue = "'a list * 'a list"

fun arity :: "'a op ⇒ nat" where
"arity Empty = 0" |
"arity (Enq _) = 1" |
"arity Deq = 1"

fun balance :: "'a queue ⇒ 'a queue" where
"balance(xs,ys) = (if size xs ≤ size ys then (xs,ys) else ([], ys @ rev xs))"

fun exec :: "'a op ⇒ 'a queue list ⇒ 'a queue" where
"exec Empty [] = ([],[])" |
"exec (Enq x) [(xs,ys)] = balance(x#xs,ys)" |
"exec Deq [(xs,ys)] = balance (xs, tl ys)"

fun cost :: "'a op ⇒ 'a queue list ⇒ nat" where
"cost Empty _ = 0" |
"cost (Enq x) [(xs,ys)] = 1 + (if size xs + 1 ≤ size ys then 0 else size xs + 1 + size ys)" |
"cost Deq [(xs,ys)] = (if size xs ≤ size ys - 1 then 0 else size xs + (size ys - 1))"

interpretation Amortized
where arity = arity and exec = exec
and inv = "λ(xs,ys). size xs ≤ size ys"
and cost = cost and Φ = "λ(xs,ys). 2 * size xs"
and U = "λf _. case f of Empty ⇒ 0 | Enq _ ⇒ 3 | Deq ⇒ 0"
proof (standard, goal_cases)
  case (1 _ f) thus ?case by (cases f) (auto split: if_splits)
next
  case 2 thus ?case by (auto)
next
  case (3 _ f) thus ?case by(cases f) (auto split: prod.splits)
qed

end (* Queue3 *)

end