Theory Amortized_Framework0

section "Amortized Complexity (Unary Operations)"

theory Amortized_Framework0
imports Complex_Main
begin

text‹
This theory provides a simple amortized analysis framework where all operations
act on a single data type, i.e. no union-like operations. This is the basis of
the ITP 2015 paper by Nipkow. Although it is superseded by the model in
‹Amortized_Framework› that allows arbitrarily many parameters, it is still
of interest because of its simplicity.›

locale Amortized =
fixes init :: "'s"
fixes nxt :: "'o ⇒ 's ⇒ 's"
fixes inv :: "'s ⇒ bool"
fixes T :: "'o ⇒ 's ⇒ real"
fixes Φ :: "'s ⇒ real"
fixes U :: "'o ⇒ 's ⇒ real"
assumes inv_init: "inv init"
assumes inv_nxt: "inv s ⟹ inv(nxt f s)"
assumes ppos: "inv s ⟹ Φ s ≥ 0"
assumes p0: "Φ init = 0"
assumes U: "inv s ⟹ T f s + Φ(nxt f s) - Φ s ≤ U f s"
begin

fun state :: "(nat ⇒ 'o) ⇒ nat ⇒ 's" where
"state f 0 = init" |
"state f (Suc n) = nxt (f n) (state f n)"

lemma inv_state: "inv(state f n)"
by(induction n)(simp_all add: inv_init inv_nxt)

definition A :: "(nat ⇒ 'o) ⇒ nat ⇒ real" where
"A f i = T (f i) (state f i) + Φ(state f (i+1)) - Φ(state f i)"

lemma aeq: "(∑i<n. T (f i) (state f i)) = (∑i<n. A f i) - Φ(state f n)"
apply(induction n)
apply (simp add: p0)
apply (simp add: A_def)
done

corollary TA: "(∑i<n. T (f i) (state f i)) ≤ (∑i<n. A f i)"
by (metis add.commute aeq diff_add_cancel le_add_same_cancel2 ppos[OF inv_state])

lemma aa1: "A f i ≤ U (f i) (state f i)"
by(simp add: A_def U inv_state)

lemma ub: "(∑i<n. T (f i) (state f i)) ≤ (∑i<n. U (f i) (state f i))"
by (metis (mono_tags) aa1 order.trans sum_mono TA)

end


subsection "Binary Counter"

locale BinCounter
begin

fun incr where
"incr [] = [True]" |
"incr (False#bs) = True # bs" |
"incr (True#bs) = False # incr bs"

fun T_incr :: "bool list ⇒ real" where
"T_incr [] = 1" |
"T_incr (False#bs) = 1" |
"T_incr (True#bs) = T_incr bs + 1"

definition Φ :: "bool list ⇒ real" where
"Φ bs = length(filter id bs)"

lemma A_incr: "T_incr bs + Φ(incr bs) - Φ bs = 2"
apply(induction bs rule: incr.induct)
apply (simp_all add: Φ_def)
done

interpretation incr: Amortized
where init = "[]" and nxt = "%_. incr" and inv = "λ_. True"
and T = "λ_. T_incr" and Φ = Φ and U = "λ_ _. 2"
proof (standard, goal_cases)
  case 1 show ?case by simp
next
  case 2 show ?case by simp
next
  case 3 show ?case by(simp add: Φ_def)
next
  case 4 show ?case by(simp add: Φ_def)
next
  case 5 show ?case by(simp add: A_incr)
qed

thm incr.ub

end

subsection "Dynamic tables: insert only"

locale DynTable1
begin

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

fun T_ins :: "nat*nat ⇒ real" where
"T_ins (n,l) = (if n<l then 1 else if l=0 then 1 else n+1)"

fun invar :: "nat*nat ⇒ bool" where
"invar (n,l) = (l/2 ≤ n ∧ n ≤ l)"

fun Φ :: "nat*nat ⇒ real" where
"Φ (n,l) = 2*(real n) - l"

interpretation ins: Amortized
where init = "(0::nat,0::nat)"
and nxt = "λ_. ins"
and inv = invar
and T = "λ_. T_ins" and Φ = Φ and U = "λ_ _. 3"
proof (standard, goal_cases)
  case 1 show ?case by auto
next
  case (2 s) thus ?case by(cases s) auto
next
  case (3 s) thus ?case by(cases s)(simp split: if_splits)
next
  case 4 show ?case by(simp)
next
  case (5 s) thus ?case by(cases s) auto
qed

end

locale table_insert = DynTable1 +
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)

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

fun pins :: "nat * nat => real" where
"pins(n,l) = a*n - b*l"

interpretation ins: Amortized
where init = "(0,0)" and nxt = "%_. ins"
and inv = "λ(n,l). if l=0 then n=0 else n ≤ l ∧ (b/a)*l ≤ n"
and T = "λ_. T_ins" and Φ = pins and U = "λ_ _. a + 1"
proof (standard, goal_cases)
  case 1 show ?case by auto
next
  case (2 s)
  show ?case
  proof (cases s)
    case [simp]: (Pair n l)
    show ?thesis
    proof cases
      assume "l=0" thus ?thesis using 2 ac
        by (simp add: b_def field_simps)
    next
      assume "l≠0"
      show ?thesis
      proof cases
        assume "n<l"
        thus ?thesis using 2 by(simp add: algebra_simps)
      next
        assume "¬ n<l"
        hence [simp]: "n=l" using 2 ‹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)"
        proof-
          have "real l + 1 = of_int(int(l)) + 1" by simp
          also have "... ≤ ceiling(c * real l)" using ‹l ≠ 0›
            by(simp only: int_less_real_le[symmetric] less_ceiling_iff)
              (simp add: mult_less_cancel_right1)
          finally show ?thesis .
        qed
        from ‹l≠0› 1 2 show ?thesis by simp
      qed
    qed
  qed
next
  case (3 s) thus ?case by(cases s)(simp add: field_simps split: if_splits)
next
  case 4 show ?case by(simp)
next
  case (5 s)
  show ?case
  proof (cases s)
    case [simp]: (Pair n l)
    show ?thesis
    proof cases
      assume "l=0" thus ?thesis using 5 by (simp)
    next
      assume [arith]: "l≠0"
      show ?thesis
      proof cases
        assume "n<l"
        thus ?thesis using 5 ac by(simp add: algebra_simps b_def)
      next
        assume "¬ n<l"
        hence [simp]: "n=l" using 5 by simp
        have "T_ins s + pins (ins s) - pins s = 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

thm ins.ub

end

subsection "Stack with multipop"

datatype 'a op⇩s⇩t⇩k = Push 'a | Pop nat

fun nxt_stk :: "'a op⇩s⇩t⇩k ⇒ 'a list ⇒ 'a list" where
"nxt_stk (Push x) xs = x # xs" |
"nxt_stk (Pop n) xs = drop n xs"

fun T_stk :: "'a op⇩s⇩t⇩k ⇒ 'a list ⇒ real" where
"T_stk (Push x) xs = 1" |
"T_stk (Pop n) xs = min n (length xs)"


interpretation stack: Amortized
where init = "[]" and nxt = nxt_stk and inv = "λ_. True"
and T = T_stk and Φ = "length" and U = "λf _. case f of Push _ ⇒ 2 | Pop _ ⇒ 0"
proof (standard, goal_cases)
  case 1 show ?case by auto
next
  case (2 s) thus ?case by(cases s) auto
next
  case 3 thus ?case by simp
next
  case 4 show ?case by(simp)
next
  case (5 _ f) thus ?case by (cases f) auto
qed


subsection "Queue"

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

datatype 'a op⇩q = Enq 'a | Deq

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

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

fun T_q :: "'a op⇩q ⇒ 'a queue ⇒ real" where
"T_q (Enq x) (xs,ys) = 1" |
"T_q Deq (xs,ys) = (if ys = [] then length xs else 0)"


interpretation queue: Amortized
where init = "([],[])" and nxt = nxt_q and inv = "λ_. True"
and T = T_q and Φ = "λ(xs,ys). length xs" and U = "λf _. case f of Enq _ ⇒ 2 | Deq ⇒ 0"
proof (standard, goal_cases)
  case 1 show ?case by auto
next
  case (2 s) thus ?case by(cases s) auto
next
  case (3 s) thus ?case by(cases s) auto
next
  case 4 show ?case by(simp)
next
  case (5 s f) thus ?case
    apply(cases s)
    apply(cases f)
    by auto
qed


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

fun nxt_q2 :: "'a op⇩q ⇒ 'a queue ⇒ 'a queue" where
"nxt_q2 (Enq a) (xs,ys) = balance (a#xs,ys)" |
"nxt_q2 Deq (xs,ys) = balance (xs, tl ys)"

fun T_q2 :: "'a op⇩q ⇒ 'a queue ⇒ real" where
"T_q2 (Enq _) (xs,ys) = 1 + (if size xs + 1 ≤ size ys then 0 else size xs + 1 + size ys)" |
"T_q2 Deq (xs,ys) = (if size xs ≤ size ys - 1 then 0 else size xs + (size ys - 1))"


interpretation queue2: Amortized
where init = "([],[])" and nxt = nxt_q2
and inv = "λ(xs,ys). size xs ≤ size ys"
and T = T_q2 and Φ = "λ(xs,ys). 2 * size xs"
and U = "λf _. case f of Enq _ ⇒ 3 | Deq ⇒ 0"
proof (standard, goal_cases)
  case 1 show ?case by auto
next
  case (2 s f) thus ?case by(cases s) (cases f, auto)
next
  case (3 s) thus ?case by(cases s) auto
next
  case 4 show ?case by(simp)
next
  case (5 s f) thus ?case
    apply(cases s)
    apply(cases f)
    by (auto simp: split: prod.splits)
qed


subsection "Dynamic tables: insert and delete"

datatype op⇩t⇩b = Ins | Del

locale DynTable2 = DynTable1
begin

fun del :: "nat*nat ⇒ nat*nat" where
"del (n,l) = (n - 1, if n=1 then 0 else if 4*(n - 1)<l then l div 2 else l)"

fun T_del :: "nat*nat ⇒ real" where
"T_del (n,l) = (if n=1 then 1 else if 4*(n - 1)<l then n else 1)"

fun nxt_tb :: "op⇩t⇩b ⇒ nat*nat ⇒ nat*nat" where
"nxt_tb Ins = ins" |
"nxt_tb Del = del"

fun T_tb :: "op⇩t⇩b ⇒ nat*nat ⇒ real" where
"T_tb Ins = T_ins" |
"T_tb Del = T_del"

fun invar :: "nat*nat ⇒ bool" where
"invar (n,l) = (n ≤ l)"

fun Φ :: "nat*nat ⇒ real" where
"Φ (n,l) = (if n < l/2 then l/2 - n else 2*n - l)"

interpretation tb: Amortized
where init = "(0,0)" and nxt = nxt_tb
and inv = invar
and T = T_tb and Φ = Φ
and U = "λf _. case f of Ins ⇒ 3 | Del ⇒ 2"
proof (standard, goal_cases)
  case 1 show ?case by auto
next
  case (2 s f) thus ?case by(cases s, cases f) (auto)
next
  case (3 s) show ?case by(cases s)(simp)
next
  case 4 show ?case by(simp)
next
  case (5 s f) thus ?case apply(cases s) apply(cases f)
    by (auto)
qed

end

end