Theory Amortized_Complexity.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 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 "l0"
      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 l0 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 l0 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]: "l0"
      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 l0
          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 opstk = Push 'a | Pop nat

fun nxt_stk :: "'a opstk  'a list  'a list" where
"nxt_stk (Push x) xs = x # xs" |
"nxt_stk (Pop n) xs = drop n xs"

fun T_stk :: "'a opstk  '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 opq = Enq 'a | Deq

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

fun nxt_q :: "'a opq  '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 opq  '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 opq  '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 opq  '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 optb = 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 :: "optb  nat*nat  nat*nat" where
"nxt_tb Ins = ins" |
"nxt_tb Del = del"

fun T_tb :: "optb  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