Theory Splay_Tree_Analysis
subsection "Splay Tree Analysis"
theory Splay_Tree_Analysis
imports
Splay_Tree_Analysis_Base
Amortized_Framework
begin
subsubsection "Analysis of splay"
definition A_splay :: "'a::linorder ⇒ 'a tree ⇒ real" where
"A_splay a t = T_splay a t + Φ(splay a t) - Φ t"
text‹The following lemma is an attempt to prove a generic lemma that covers
both zig-zig cases. However, the lemma is not as nice as one would like.
Hence it is used only once, as a demo. Ideally the lemma would involve
function @{const A_splay}, but that is impossible because this involves @{const splay}
and thus depends on the ordering. We would need a truly symmetric version of @{const splay}
that takes the ordering as an explicit argument. Then we could define
all the symmetric cases by one final equation
\<^prop>‹splay2 less t = splay2 (λx y. Not (less x y)) (mirror t)›.
This would simplify the code and the proofs.›
lemma zig_zig: fixes lx x rx lb b rb a ra u lb1 lb2
defines [simp]: "X == Node lx (x) rx" defines[simp]: "B == Node lb b rb"
defines [simp]: "t == Node B a ra" defines [simp]: "A' == Node rb a ra"
defines [simp]: "t' == Node lb1 u (Node lb2 b A')"
assumes hyps: "lb ≠ ⟨⟩" and IH: "T_splay x lb + Φ lb1 + Φ lb2 - Φ lb ≤ 2 * φ lb - 3 * φ X + 1" and
prems: "size lb = size lb1 + size lb2 + 1" "X ∈ subtrees lb"
shows "T_splay x lb + Φ t' - Φ t ≤ 3 * (φ t - φ X)"
proof -
define B' where [simp]: "B' = Node lb2 b A'"
have "T_splay x lb + Φ t' - Φ t = T_splay x lb + Φ lb1 + Φ lb2 - Φ lb + φ B' + φ A' - φ B"
using prems
by(auto simp: A_splay_def size_if_splay algebra_simps in_set_tree_if split: tree.split)
also have "… ≤ 2 * φ lb + φ B' + φ A' - φ B - 3 * φ X + 1"
using IH prems(2) by(auto simp: algebra_simps)
also have "… ≤ φ lb + φ B' + φ A' - 3 * φ X + 1" by(simp)
also have "… ≤ φ B' + 2 * φ t - 3 * φ X "
using prems ld_ld_1_less[of "size1 lb" "size1 A'"]
by(simp add: size_if_splay)
also have "… ≤ 3 * φ t - 3 * φ X"
using prems by(simp add: size_if_splay)
finally show ?thesis by simp
qed
lemma A_splay_ub: "⟦ bst t; Node l x r : subtrees t ⟧
⟹ A_splay x t ≤ 3 * (φ t - φ(Node l x r)) + 1"
proof(induction x t rule: splay.induct)
case 1 thus ?case by simp
next
case 2 thus ?case by (auto simp: A_splay_def)
next
case 4 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
case 5 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
case 7 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
case 10 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
case 12 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
case 13 hence False by(fastforce dest: in_set_tree_if) thus ?case ..
next
case (3 x b A B CD)
let ?t = "⟨⟨A, x, B⟩, b, CD⟩"
let ?t' = "⟨A, x, ⟨B, b, CD⟩⟩"
have *: "l = A ∧ r = B" using "3.prems" by(fastforce dest: in_set_tree_if)
have "A_splay x ?t = 1 + Φ ?t' - Φ ?t" using "3.hyps" by (simp add: A_splay_def)
also have "… = 1 + φ ?t' + φ ⟨B, b, CD⟩ - φ ?t - φ ⟨A, x, B⟩" by(simp)
also have "… = 1 + φ ⟨B, b, CD⟩ - φ ⟨A, x, B⟩" by(simp)
also have "… ≤ 1 + φ ?t - φ(Node A x B)"
using log_le_cancel_iff[of 2 "size1(Node B b CD)" "size1 ?t"] by (simp)
also have "… ≤ 1 + 3 * (φ ?t - φ(Node A x B))"
using log_le_cancel_iff[of 2 "size1(Node A x B)" "size1 ?t"] by (simp)
finally show ?case using * by simp
next
case (9 b x AB C D)
let ?A = "⟨AB, b, ⟨C, x, D⟩⟩"
have "x ∉ set_tree AB" using "9.prems"(1) by auto
with 9 show ?case using
log_le_cancel_iff[of 2 "size1(Node AB b C)" "size1 ?A"]
log_le_cancel_iff[of 2 "size1(Node C x D)" "size1 ?A"]
by (auto simp: A_splay_def algebra_simps simp del:log_le_cancel_iff)
next
case (6 x a b A B C)
hence *: "⟨l, x, r⟩ ∈ subtrees A" by(fastforce dest: in_set_tree_if)
obtain A1 x' A2 where sp: "splay x A = Node A1 x' A2"
using splay_not_Leaf[OF ‹A ≠ Leaf›] by blast
let ?X = "Node l x r" let ?AB = "Node A a B" let ?ABC = "Node ?AB b C"
let ?A' = "Node A1 x' A2"
let ?BC = "Node B b C" let ?A2BC = "Node A2 a ?BC" let ?A1A2BC = "Node A1 x' ?A2BC"
have 0: "φ ?A1A2BC = φ ?ABC" using sp by(simp add: size_if_splay)
have 1: "Φ ?A1A2BC - Φ ?ABC = Φ A1 + Φ A2 + φ ?A2BC + φ ?BC - Φ A - φ ?AB"
using 0 by (simp)
have "A_splay x ?ABC = T_splay x A + 1 + Φ ?A1A2BC - Φ ?ABC"
using "6.hyps" sp by(simp add: A_splay_def)
also have "… = T_splay x A + 1 + Φ A1 + Φ A2 + φ ?A2BC + φ ?BC - Φ A - φ ?AB"
using 1 by simp
also have "… = T_splay x A + Φ ?A' - φ ?A' - Φ A + φ ?A2BC + φ ?BC - φ ?AB + 1"
by(simp)
also have "… = A_splay x A + φ ?A2BC + φ ?BC - φ ?AB - φ ?A' + 1"
using sp by(simp add: A_splay_def)
also have "… ≤ 3 * φ A + φ ?A2BC + φ ?BC - φ ?AB - φ ?A' - 3 * φ ?X + 2"
using "6.IH" "6.prems"(1) * by(simp)
also have "… = 2 * φ A + φ ?A2BC + φ ?BC - φ ?AB - 3 * φ ?X + 2"
using sp by(simp add: size_if_splay)
also have "… < φ A + φ ?A2BC + φ ?BC - 3 * φ ?X + 2" by(simp)
also have "… < φ ?A2BC + 2 * φ ?ABC - 3 * φ ?X + 1"
using sp ld_ld_1_less[of "size1 A" "size1 ?BC"]
by(simp add: size_if_splay)
also have "… < 3 * φ ?ABC - 3 * φ ?X + 1"
using sp by(simp add: size_if_splay)
finally show ?case by simp
next
case (8 a x b B A C)
hence *: "⟨l, x, r⟩ ∈ subtrees B" by(fastforce dest: in_set_tree_if)
obtain B1 x' B2 where sp: "splay x B = Node B1 x' B2"
using splay_not_Leaf[OF ‹B ≠ Leaf›] by blast
let ?X = "Node l x r" let ?AB = "Node A a B" let ?ABC = "Node ?AB b C"
let ?B' = "Node B1 x' B2"
let ?AB1 = "Node A a B1" let ?B2C = "Node B2 b C" let ?AB1B2C = "Node ?AB1 x' ?B2C"
have 0: "φ ?AB1B2C = φ ?ABC" using sp by(simp add: size_if_splay)
have 1: "Φ ?AB1B2C - Φ ?ABC = Φ B1 + Φ B2 + φ ?AB1 + φ ?B2C - Φ B - φ ?AB"
using 0 by (simp)
have "A_splay x ?ABC = T_splay x B + 1 + Φ ?AB1B2C - Φ ?ABC"
using "8.hyps" sp by(simp add: A_splay_def)
also have "… = T_splay x B + 1 + Φ B1 + Φ B2 + φ ?AB1 + φ ?B2C - Φ B - φ ?AB"
using 1 by simp
also have "… = T_splay x B + Φ ?B' - φ ?B' - Φ B + φ ?AB1 + φ ?B2C - φ ?AB + 1"
by simp
also have "… = A_splay x B + φ ?AB1 + φ ?B2C - φ ?AB - φ ?B' + 1"
using sp by (simp add: A_splay_def)
also have "… ≤ 3 * φ B + φ ?AB1 + φ ?B2C - φ ?AB - φ ?B' - 3 * φ ?X + 2"
using "8.IH" "8.prems"(1) * by(simp)
also have "… = 2 * φ B + φ ?AB1 + φ ?B2C - φ ?AB - 3 * φ ?X + 2"
using sp by(simp add: size_if_splay)
also have "… < φ B + φ ?AB1 + φ ?B2C - 3 * φ ?X + 2" by(simp)
also have "… < φ B + 2 * φ ?ABC - 3 * φ ?X + 1"
using sp ld_ld_1_less[of "size1 ?AB1" "size1 ?B2C"]
by(simp add: size_if_splay)
also have "… < 3 * φ ?ABC - 3 * φ ?X + 1" by(simp)
finally show ?case by simp
next
case (11 b x c C A D)
hence *: "⟨l, x, r⟩ ∈ subtrees C" by(fastforce dest: in_set_tree_if)
obtain C1 x' C2 where sp: "splay x C = Node C1 x' C2"
using splay_not_Leaf[OF ‹C ≠ Leaf›] by blast
let ?X = "Node l x r" let ?CD = "Node C c D" let ?ACD = "Node A b ?CD"
let ?C' = "Node C1 x' C2"
let ?C2D = "Node C2 c D" let ?AC1 = "Node A b C1"
have "A_splay x ?ACD = A_splay x C + φ ?C2D + φ ?AC1 - φ ?CD - φ ?C' + 1"
using "11.hyps" sp
by(auto simp: A_splay_def size_if_splay algebra_simps split: tree.split)
also have "… ≤ 3 * φ C + φ ?C2D + φ ?AC1 - φ ?CD - φ ?C' - 3 * φ ?X + 2"
using "11.IH" "11.prems"(1) * by(auto simp: algebra_simps)
also have "… = 2 * φ C + φ ?C2D + φ ?AC1 - φ ?CD - 3 * φ ?X + 2"
using sp by(simp add: size_if_splay)
also have "… ≤ φ C + φ ?C2D + φ ?AC1 - 3 * φ ?X + 2" by(simp)
also have "… ≤ φ C + 2 * φ ?ACD - 3 * φ ?X + 1"
using sp ld_ld_1_less[of "size1 ?C2D" "size1 ?AC1"]
by(simp add: size_if_splay algebra_simps)
also have "… ≤ 3 * φ ?ACD - 3 * φ ?X + 1" by(simp)
finally show ?case by simp
next
case (14 a x b CD A B)
hence 0: "x ∉ set_tree B ∧ x ∉ set_tree A"
using "14.prems"(1) ‹b<x› by(auto)
hence 1: "x ∈ set_tree CD" using "14.prems" ‹b<x› ‹a<x› by (auto)
obtain C x' D where sp: "splay x CD = Node C x' D"
using splay_not_Leaf[OF ‹CD ≠ Leaf›] by blast
from zig_zig[of CD x D C l r _ b B a A] 14 sp 0
show ?case by(auto simp: A_splay_def size_if_splay algebra_simps)
qed
lemma A_splay_ub2: assumes "bst t" "x : set_tree t"
shows "A_splay x t ≤ 3 * (φ t - 1) + 1"
proof -
from assms(2) obtain l r where N: "Node l x r : subtrees t"
by (metis set_treeE)
have "A_splay x t ≤ 3 * (φ t - φ(Node l x r)) + 1" by(rule A_splay_ub[OF assms(1) N])
also have "… ≤ 3 * (φ t - 1) + 1" by(simp add: field_simps)
finally show ?thesis .
qed
lemma A_splay_ub3: assumes "bst t" shows "A_splay x t ≤ 3 * φ t + 1"
proof cases
assume "t = Leaf" thus ?thesis by(simp add: A_splay_def)
next
assume "t ≠ Leaf"
from ex_in_set_tree[OF this assms] obtain x' where
a': "x' ∈ set_tree t" "splay x' t = splay x t" "T_splay x' t = T_splay x t"
by blast
show ?thesis using A_splay_ub2[OF assms a'(1)] by(simp add: A_splay_def a')
qed
subsubsection "Analysis of insert"
lemma amor_insert: assumes "bst t"
shows "T_insert x t + Φ(Splay_Tree.insert x t) - Φ t ≤ 4 * log 2 (size1 t) + 2" (is "?l ≤ ?r")
proof cases
assume "t = Leaf" thus ?thesis by(simp)
next
assume "t ≠ Leaf"
then obtain l e r where [simp]: "splay x t = Node l e r"
by (metis tree.exhaust splay_Leaf_iff)
let ?t = "real(T_splay x t)"
let ?Plr = "Φ l + Φ r" let ?Ps = "Φ t"
let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)"
have opt: "?t + Φ (splay x t) - ?Ps ≤ 3 * log 2 (real (size1 t)) + 1"
using A_splay_ub3[OF ‹bst t›, simplified A_splay_def, of x] by (simp)
from less_linear[of e x]
show ?thesis
proof (elim disjE)
assume "e=x"
have nneg: "log 2 (1 + real (size t)) ≥ 0" by simp
thus ?thesis using ‹t ≠ Leaf› opt ‹e=x›
apply(simp add: algebra_simps) using nneg by arith
next
let ?L = "log 2 (real(size1 l) + 1)"
assume "e < x" hence "e ≠ x" by simp
hence "?l = (?t + ?Plr - ?Ps) + ?L + ?LR"
using ‹t ≠ Leaf› ‹e<x› by(simp)
also have "?t + ?Plr - ?Ps ≤ 2 * log 2 ?slr + 1"
using opt size_splay[of x t,symmetric] by(simp)
also have "?L ≤ log 2 ?slr" by(simp)
also have "?LR ≤ log 2 ?slr + 1"
proof -
have "?LR ≤ log 2 (2 * ?slr)" by (simp add:)
also have "… ≤ log 2 ?slr + 1"
by (simp add: log_mult del:distrib_left_numeral)
finally show ?thesis .
qed
finally show ?thesis using size_splay[of x t,symmetric] by (simp)
next
let ?R = "log 2 (2 + real(size r))"
assume "x < e" hence "e ≠ x" by simp
hence "?l = (?t + ?Plr - ?Ps) + ?R + ?LR"
using ‹t ≠ Leaf› ‹x < e› by(simp)
also have "?t + ?Plr - ?Ps ≤ 2 * log 2 ?slr + 1"
using opt size_splay[of x t,symmetric] by(simp)
also have "?R ≤ log 2 ?slr" by(simp)
also have "?LR ≤ log 2 ?slr + 1"
proof -
have "?LR ≤ log 2 (2 * ?slr)" by (simp add:)
also have "… ≤ log 2 ?slr + 1"
by (simp add: log_mult del:distrib_left_numeral)
finally show ?thesis .
qed
finally show ?thesis using size_splay[of x t, symmetric] by simp
qed
qed
subsubsection "Analysis of delete"
definition A_splay_max :: "'a::linorder tree ⇒ real" where
"A_splay_max t = T_splay_max t + Φ(splay_max t) - Φ t"
lemma A_splay_max_ub: "t ≠ Leaf ⟹ A_splay_max t ≤ 3 * (φ t - 1) + 1"
proof(induction t rule: splay_max.induct)
case 1 thus ?case by (simp)
next
case (2 A)
thus ?case using one_le_log_cancel_iff[of 2 "size1 A + 1"]
by (simp add: A_splay_max_def del: one_le_log_cancel_iff)
next
case (3 l b rl c rr)
show ?case
proof cases
assume "rr = Leaf"
thus ?thesis
using one_le_log_cancel_iff[of 2 "1 + size1 rl"]
one_le_log_cancel_iff[of 2 "1 + size1 l + size1 rl"]
log_le_cancel_iff[of 2 "size1 l + size1 rl" "1 + size1 l + size1 rl"]
by (auto simp: A_splay_max_def field_simps
simp del: log_le_cancel_iff one_le_log_cancel_iff)
next
assume "rr ≠ Leaf"
then obtain l' u r' where sp: "splay_max rr = Node l' u r'"
using splay_max_Leaf_iff tree.exhaust by blast
hence 1: "size rr = size l' + size r' + 1"
using size_splay_max[of rr,symmetric] by(simp)
let ?C = "Node rl c rr" let ?B = "Node l b ?C"
let ?B' = "Node l b rl" let ?C' = "Node ?B' c l'"
have "A_splay_max ?B = A_splay_max rr + φ ?B' + φ ?C' - φ rr - φ ?C + 1" using "3.prems" sp 1
by(auto simp add: A_splay_max_def)
also have "… ≤ 3 * (φ rr - 1) + φ ?B' + φ ?C' - φ rr - φ ?C + 2"
using 3 ‹rr ≠ Leaf› by auto
also have "… = 2 * φ rr + φ ?B' + φ ?C' - φ ?C - 1" by simp
also have "… ≤ φ rr + φ ?B' + φ ?C' - 1" by simp
also have "… ≤ 2 * φ ?B + φ ?C' - 2"
using ld_ld_1_less[of "size1 ?B'" "size1 rr"] by(simp add:)
also have "… ≤ 3 * φ ?B - 2" using 1 by simp
finally show ?case by simp
qed
qed
lemma A_splay_max_ub3: "A_splay_max t ≤ 3 * φ t + 1"
proof cases
assume "t = Leaf" thus ?thesis by(simp add: A_splay_max_def)
next
assume "t ≠ Leaf"
show ?thesis using A_splay_max_ub[OF ‹t ≠ Leaf›] by(simp)
qed
lemma amor_delete: assumes "bst t"
shows "T_delete a t + Φ(Splay_Tree.delete a t) - Φ t ≤ 6 * log 2 (size1 t) + 2"
proof (cases t)
case Leaf thus ?thesis by(simp add: Splay_Tree.delete_def)
next
case [simp]: (Node ls x rs)
then obtain l e r where sp[simp]: "splay a (Node ls x rs) = Node l e r"
by (metis tree.exhaust splay_Leaf_iff)
let ?t = "real(T_splay a t)"
let ?Plr = "Φ l + Φ r" let ?Ps = "Φ t"
let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)"
let ?lslr = "log 2 (real (size ls) + (real (size rs) + 2))"
have "?lslr ≥ 0" by simp
have opt: "?t + Φ (splay a t) - ?Ps ≤ 3 * log 2 (real (size1 t)) + 1"
using A_splay_ub3[OF ‹bst t›, simplified A_splay_def, of a]
by (simp add: field_simps)
show ?thesis
proof (cases "e=a")
case False thus ?thesis
using opt apply(simp add: Splay_Tree.delete_def field_simps)
using ‹?lslr ≥ 0› by arith
next
case [simp]: True
show ?thesis
proof (cases l)
case Leaf
have 1: "log 2 (real (size r) + 2) ≥ 0" by(simp)
show ?thesis
using Leaf opt apply(simp add: Splay_Tree.delete_def field_simps)
using 1 ‹?lslr ≥ 0› by arith
next
case (Node ll y lr)
then obtain l' y' r' where [simp]: "splay_max (Node ll y lr) = Node l' y' r'"
using splay_max_Leaf_iff tree.exhaust by blast
have "bst l" using bst_splay[OF ‹bst t›, of a] by simp
have "Φ r' ≥ 0" apply (induction r') by (auto)
have optm: "real(T_splay_max l) + Φ (splay_max l) - Φ l ≤ 3 * φ l + 1"
using A_splay_max_ub3[of l, simplified A_splay_max_def] by (simp add: field_simps Node)
have 1: "log 2 (2+(real(size l')+real(size r))) ≤ log 2 (2+(real(size l)+real(size r)))"
using size_splay_max[of l] Node by simp
have 2: "log 2 (2 + (real (size l') + real (size r'))) ≥ 0" by simp
have 3: "log 2 (size1 l' + size1 r) ≤ log 2 (size1 l' + size1 r') + log 2 ?slr"
apply simp using 1 2 by arith
have 4: "log 2 (real(size ll) + (real(size lr) + 2)) ≤ ?lslr"
using size_if_splay[OF sp] Node by simp
show ?thesis using add_mono[OF opt optm] Node 3
apply(simp add: Splay_Tree.delete_def field_simps)
using 4 ‹Φ r' ≥ 0› by arith
qed
qed
qed
subsubsection "Overall analysis"
fun U where
"U Empty [] = 1" |
"U (Splay _) [t] = 3 * log 2 (size1 t) + 1" |
"U (Insert _) [t] = 4 * log 2 (size1 t) + 3" |
"U (Delete _) [t] = 6 * log 2 (size1 t) + 3"
interpretation Amortized
where arity = arity and exec = exec and inv = bst
and cost = cost and Φ = Φ and U = U
proof (standard, goal_cases)
case (1 ss f) show ?case
proof (cases f)
case Empty thus ?thesis using 1 by auto
next
case (Splay a)
then obtain t where "ss = [t]" "bst t" using 1 by auto
with Splay bst_splay[OF ‹bst t›, of a] show ?thesis
by (auto split: tree.split)
next
case (Insert a)
then obtain t where "ss = [t]" "bst t" using 1 by auto
with bst_splay[OF ‹bst t›, of a] Insert show ?thesis
by (auto simp: splay_bstL[OF ‹bst t›] splay_bstR[OF ‹bst t›] split: tree.split)
next
case (Delete a)
then obtain t where "ss = [t]" "bst t" using 1 by auto
with 1 Delete show ?thesis by(simp add: bst_delete)
qed
next
case (2 t) thus ?case by (induction t) auto
next
case (3 ss f)
show ?case (is "?l ≤ ?r")
proof(cases f)
case Empty thus ?thesis using 3(2) by(simp add: A_splay_def)
next
case (Splay a)
then obtain t where "ss = [t]" "bst t" using 3 by auto
thus ?thesis using Splay A_splay_ub3[OF ‹bst t›] by(simp add: A_splay_def)
next
case [simp]: (Insert a)
then obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
thus ?thesis using amor_insert[of t a] by auto
next
case [simp]: (Delete a)
then obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
thus ?thesis using amor_delete[of t a] by auto
qed
qed
end