Dynamic Tables

This article formalizes the amortized analysis of dynamic tables parameterized with their minimal and maximal load factors and the expansion and contraction factors. A full description is found in a companion paper [1]. theory Tables-real imports../Amortized-Complexity/Amor begin fun Ψ:: bool ⇒ real ⇒ real ⇒ real ⇒ real ⇒ nat ⇒ real where Ψ b i d x 1 x 2 n = (if n ≥ x 2 then i∗(n − x 2) else if n ≤ x 1 ∧ b then d∗(x 1 − n) else 0) declare real-of-nat-Suc[simp] real-of-nat-diff [simp] An automatic proof: lemma Psi-diff-Ins: 0 < i = ⇒ 0 < d = ⇒ Ψ b i d x 1 x 2 (Suc n) − Ψ b i d x 1 x 2 n ≤