Theory Amortized_Framework

section "Amortized Complexity Framework"

theory Amortized_Framework
imports Complex_Main
begin

text‹This theory provides a framework for amortized analysis.›

datatype 'a rose_tree = T 'a "'a rose_tree list"

declare length_Suc_conv [simp]

locale Amortized =
fixes arity :: "'op ⇒ nat"
fixes exec :: "'op ⇒ 's list ⇒ 's"
fixes inv :: "'s ⇒ bool"
fixes cost :: "'op ⇒ 's list ⇒ nat"
fixes Φ :: "'s ⇒ real"
fixes U :: "'op ⇒ 's list ⇒ real"
assumes inv_exec: "⟦∀s ∈ set ss. inv s; length ss = arity f ⟧ ⟹ inv(exec f ss)"
assumes ppos: "inv s ⟹ Φ s ≥ 0"
assumes U: "⟦ ∀s ∈ set ss. inv s; length ss = arity f ⟧
 ⟹ cost f ss + Φ(exec f ss) - sum_list (map Φ ss) ≤ U f ss"
begin

fun wf :: "'op rose_tree ⇒ bool" where
"wf (T f ts) = (length ts = arity f ∧ (∀t ∈ set ts. wf t))"

fun state :: "'op rose_tree ⇒ 's" where
"state (T f ts) = exec f (map state ts)"

lemma inv_state: "wf ot ⟹ inv(state ot)"
by(induction ot)(simp_all add: inv_exec)

definition acost :: "'op ⇒ 's list ⇒ real" where
"acost f ss = cost f ss + Φ (exec f ss) - sum_list (map Φ ss)"

fun acost_sum :: "'op rose_tree ⇒ real" where
"acost_sum (T f ts) = acost f (map state ts) + sum_list (map acost_sum ts)"

fun cost_sum :: "'op rose_tree ⇒ real" where
"cost_sum (T f ts) = cost f (map state ts) + sum_list (map cost_sum ts)"

fun U_sum :: "'op rose_tree ⇒ real" where
"U_sum (T f ts) = U f (map state ts) + sum_list (map U_sum ts)"

lemma t_sum_a_sum: "wf ot ⟹ cost_sum ot = acost_sum ot - Φ(state ot)"
  by (induction ot) (auto simp: acost_def Let_def sum_list_subtractf cong: map_cong)

corollary t_sum_le_a_sum: "wf ot ⟹ cost_sum ot ≤ acost_sum ot"
by (metis add.commute t_sum_a_sum diff_add_cancel le_add_same_cancel2 ppos[OF inv_state])

lemma a_le_U: "⟦ ∀s ∈ set ss. inv s; length ss = arity f ⟧ ⟹ acost f ss ≤ U f ss"
by(simp add: acost_def U)

lemma a_sum_le_U_sum: "wf ot ⟹ acost_sum ot ≤ U_sum ot"
proof(induction ot)
  case (T f ts)
  with a_le_U[of "map state ts" f] sum_list_mono show ?case
    by (force simp: inv_state)
qed

corollary t_sum_le_U_sum: "wf ot ⟹ cost_sum ot ≤ U_sum ot"
by (blast intro: t_sum_le_a_sum a_sum_le_U_sum order.trans)

end

hide_const T

text
‹‹Amortized2› supports the transfer of amortized analysis of one datatype
(‹Amortized arity exec inv cost Φ U› on type ‹'s›) to an implementation
(primed identifiers on type ‹'t›).
Function ‹hom› is assumed to be a homomorphism from ‹'t› to ‹'s›,
not just w.r.t. ‹exec› but also ‹cost› and ‹U›. The assumptions about
‹inv'› are weaker than the obvious ‹inv' = inv ∘ hom›: the latter does
not allow ‹inv› to be weaker than ‹inv'› (which we need in one application).›

locale Amortized2 = Amortized arity exec inv cost Φ U
  for arity :: "'op ⇒ nat" and exec and inv :: "'s ⇒ bool" and cost Φ U +
fixes exec' :: "'op ⇒ 't list ⇒ 't"
fixes inv' :: "'t ⇒ bool"
fixes cost' :: "'op ⇒ 't list ⇒ nat"
fixes U' :: "'op ⇒ 't list ⇒ real"
fixes hom :: "'t ⇒ 's"
assumes exec': "⟦∀s ∈ set ts. inv' s; length ts = arity f ⟧
  ⟹ hom(exec' f ts) = exec f (map hom ts)"
assumes inv_exec': "⟦∀s ∈ set ss. inv' s; length ss = arity f ⟧
  ⟹ inv'(exec' f ss)"
assumes inv_hom: "inv' t ⟹ inv (hom t)"
assumes cost': "⟦∀s ∈ set ts. inv' s; length ts = arity f ⟧
  ⟹ cost' f ts = cost f (map hom ts)"
assumes U': "⟦∀s ∈ set ts. inv' s; length ts = arity f ⟧
  ⟹ U' f ts = U f (map hom ts)"
begin

sublocale A': Amortized arity exec' inv' cost' "Φ o hom" U'
proof (standard, goal_cases)
  case 1 thus ?case by(simp add: exec' inv_exec' inv_exec)
next
  case 2 thus ?case by(simp add: inv_hom ppos)
next
  case 3 thus ?case
    by(simp add: U exec' U' map_map[symmetric] cost' inv_exec inv_hom del: map_map)
qed

end

end