Theory Splay_Tree_Analysis_Optimal
subsection "Splay Tree Analysis (Optimal)"
theory Splay_Tree_Analysis_Optimal
imports
Splay_Tree_Analysis_Base
Amortized_Framework
"HOL-Library.Sum_of_Squares"
begin
text‹This analysis follows Schoenmakers~\<^cite>‹"Schoenmakers-IPL93"›.›
subsubsection "Analysis of splay"
locale Splay_Analysis =
fixes α :: real and β :: real
assumes a1[arith]: "α > 1"
assumes A1: "⟦1 ≤ x; 1 ≤ y; 1 ≤ z⟧ ⟹
(x+y) * (y+z) powr β ≤ (x+y) powr β * (x+y+z)"
assumes A2: "⟦1 ≤ l'; 1 ≤ r'; 1 ≤ lr; 1 ≤ r⟧ ⟹
α * (l'+r') * (lr+r) powr β * (lr+r'+r) powr β
≤ (l'+r') powr β * (l'+lr+r') powr β * (l'+lr+r'+r)"
assumes A3: "⟦1 ≤ l'; 1 ≤ r'; 1 ≤ ll; 1 ≤ r⟧ ⟹
α * (l'+r') * (l'+ll) powr β * (r'+r) powr β
≤ (l'+r') powr β * (l'+ll+r') powr β * (l'+ll+r'+r)"
begin
lemma nl2: "⟦ ll ≥ 1; lr ≥ 1; r ≥ 1 ⟧ ⟹
log α (ll + lr) + β * log α (lr + r)
≤ β * log α (ll + lr) + log α (ll + lr + r)"
apply(rule powr_le_cancel_iff[THEN iffD1, OF a1])
apply(simp add: powr_add mult.commute[of β] powr_powr[symmetric] A1)
done
definition φ :: "'a tree ⇒ 'a tree ⇒ real" where
"φ t1 t2 = β * log α (size1 t1 + size1 t2)"
fun Φ :: "'a tree ⇒ real" where
"Φ Leaf = 0" |
"Φ (Node l _ r) = Φ l + Φ r + φ l r"
definition A :: "'a::linorder ⇒ 'a tree ⇒ real" where
"A a t = T_splay a t + Φ(splay a t) - Φ t"
lemma A_simps[simp]: "A a (Node l a r) = 1"
"a<b ⟹ A a (Node (Node ll a lr) b r) = φ lr r - φ lr ll + 1"
"b<a ⟹ A a (Node l b (Node rl a rr)) = φ rl l - φ rr rl + 1"
by(auto simp add: A_def φ_def algebra_simps)
lemma A_ub: "⟦ bst t; Node la a ra : subtrees t ⟧
⟹ A a t ≤ log α ((size1 t)/(size1 la + size1 ra)) + 1"
proof(induction a t rule: splay.induct)
case 1 thus ?case by simp
next
case 2 thus ?case by auto
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 b a lb rb ra)
have "b ∉ set_tree ra" using "3.prems"(1) by auto
thus ?case using "3.prems"(1,2) nl2[of "size1 lb" "size1 rb" "size1 ra"]
by (auto simp: φ_def log_divide algebra_simps)
next
case (9 a b la lb rb)
have "b ∉ set_tree la" using "9.prems"(1) by auto
thus ?case using "9.prems"(1,2) nl2[of "size1 rb" "size1 lb" "size1 la"]
by (auto simp add: φ_def log_divide algebra_simps)
next
case (6 x b a lb rb ra)
hence 0: "x ∉ set_tree rb ∧ x ∉ set_tree ra" using "6.prems"(1) by auto
hence 1: "x ∈ set_tree lb" using "6.prems" ‹x<b› by (auto)
then obtain lu u ru where sp: "splay x lb = Node lu u ru"
using "6.prems"(1,2) by(cases "splay x lb") auto
have "b < a" using "6.prems"(1,2) by (auto)
let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
let ?rb = "real(size1 rb)" let ?r = "real(size1 ra)"
have "1 + log α (?lu + ?ru) + β * log α (?rb + ?r) + β * log α (?rb + ?ru + ?r) ≤
β * log α (?lu + ?ru) + β * log α (?lu + ?rb + ?ru) + log α (?lu + ?rb + ?ru + ?r)" (is "?L≤?R")
proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
show "α powr ?L ≤ α powr ?R" using A2[of ?lu ?ru ?rb ?r]
by(simp add: powr_add add_ac mult.commute[of β] powr_powr[symmetric])
qed
thus ?case using 6 0 1 sp
by(auto simp: A_def φ_def size_if_splay algebra_simps log_divide)
next
case (8 b x a rb lb ra)
hence 0: "x ∉ set_tree lb ∧ x ∉ set_tree ra" using "8.prems"(1) by(auto)
hence 1: "x ∈ set_tree rb" using "8.prems" ‹b<x› ‹x<a› by (auto)
then obtain lu u ru where sp: "splay x rb = Node lu u ru"
using "8.prems"(1,2) by(cases "splay x rb") auto
let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
let ?lb = "real(size1 lb)" let ?r = "real(size1 ra)"
have "1 + log α (?lu + ?ru) + β * log α (?lu + ?lb) + β * log α (?ru + ?r) ≤
β * log α (?lu + ?ru) + β * log α (?lu + ?lb + ?ru) + log α (?lu + ?lb + ?ru + ?r)" (is "?L≤?R")
proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
show "α powr ?L ≤ α powr ?R" using A3[of ?lu ?ru ?lb ?r]
by(simp add: powr_add mult.commute[of β] powr_powr[symmetric])
qed
thus ?case using 8 0 1 sp
by(auto simp add: A_def size_if_splay φ_def log_divide algebra_simps)
next
case (11 a x b lb la rb)
hence 0: "x ∉ set_tree rb ∧ x ∉ set_tree la" using "11.prems"(1) by (auto)
hence 1: "x ∈ set_tree lb" using "11.prems" ‹a<x› ‹x<b› by (auto)
then obtain lu u ru where sp: "splay x lb = Node lu u ru"
using "11.prems"(1,2) by(cases "splay x lb") auto
let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
let ?l = "real(size1 la)" let ?rb = "real(size1 rb)"
have "1 + log α (?lu + ?ru) + β * log α (?lu + ?l) + β * log α (?ru + ?rb) ≤
β * log α (?lu + ?ru) + β * log α (?lu + ?ru + ?rb) + log α (?lu + ?l + ?ru + ?rb)" (is "?L≤?R")
proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
show "α powr ?L ≤ α powr ?R" using A3[of ?ru ?lu ?rb ?l]
by(simp add: powr_add mult.commute[of β] powr_powr[symmetric])
(simp add: algebra_simps)
qed
thus ?case using 11 0 1 sp
by(auto simp add: A_def size_if_splay φ_def log_divide algebra_simps)
next
case (14 a x b rb la lb)
hence 0: "x ∉ set_tree lb ∧ x ∉ set_tree la" using "14.prems"(1) by(auto)
hence 1: "x ∈ set_tree rb" using "14.prems" ‹a<x› ‹b<x› by (auto)
then obtain lu u ru where sp: "splay x rb = Node lu u ru"
using "14.prems"(1,2) by(cases "splay x rb") auto
let ?la = "real(size1 la)" let ?lb = "real(size1 lb)"
let ?lu = "real (size1 lu)" let ?ru = "real (size1 ru)"
have "1 + log α (?lu + ?ru) + β * log α (?la + ?lb) + β * log α (?lu + ?la + ?lb) ≤
β * log α (?lu + ?ru) + β * log α (?lu + ?lb + ?ru) + log α (?lu + ?lb + ?ru + ?la)" (is "?L≤?R")
proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
show "α powr ?L ≤ α powr ?R" using A2[of ?ru ?lu ?lb ?la]
by(simp add: powr_add add_ac mult.commute[of β] powr_powr[symmetric])
qed
thus ?case using 14 0 1 sp
by(auto simp add: A_def size_if_splay φ_def log_divide algebra_simps)
qed
lemma A_ub2: assumes "bst t" "a : set_tree t"
shows "A a t ≤ log α ((size1 t)/2) + 1"
proof -
from assms(2) obtain la ra where N: "Node la a ra : subtrees t"
by (metis set_treeE)
have "A a t ≤ log α ((size1 t)/(size1 la + size1 ra)) + 1"
by(rule A_ub[OF assms(1) N])
also have "… ≤ log α ((size1 t)/2) + 1" by(simp add: field_simps)
finally show ?thesis by simp
qed
lemma A_ub3: assumes "bst t" shows "A a t ≤ log α (size1 t) + 1"
proof cases
assume "t = Leaf" thus ?thesis by(simp add: A_def)
next
assume "t ≠ Leaf"
from ex_in_set_tree[OF this assms] obtain a' where
a': "a' ∈ set_tree t" "splay a' t = splay a t" "T_splay a' t = T_splay a t"
by blast
have [arith]: "log α 2 > 0" by simp
show ?thesis using A_ub2[OF assms a'(1)] by(simp add: A_def a' log_divide)
qed
definition Am :: "'a::linorder tree ⇒ real" where
"Am t = T_splay_max t + Φ(splay_max t) - Φ t"
lemma Am_simp3': "⟦ c<b; bst rr; rr ≠ Leaf⟧ ⟹
Am (Node l c (Node rl b rr)) =
(case splay_max rr of Node rrl _ rrr ⇒
Am rr + φ rrl (Node l c rl) + φ l rl - φ rl rr - φ rrl rrr + 1)"
by(auto simp: Am_def φ_def size_if_splay_max algebra_simps neq_Leaf_iff split: tree.split)
lemma Am_ub: "⟦ bst t; t ≠ Leaf ⟧ ⟹ Am t ≤ log α ((size1 t)/2) + 1"
proof(induction t rule: splay_max.induct)
case 1 thus ?case by (simp)
next
case 2 thus ?case by (simp add: Am_def)
next
case (3 l b rl c rr)
show ?case
proof cases
assume "rr = Leaf"
thus ?thesis
using nl2[of 1 "size1 rl" "size1 l"] log_le_cancel_iff[of α 2 "2 + real(size rl)"]
by(auto simp: Am_def φ_def log_divide field_simps
simp del: log_le_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] by(simp)
let ?l = "real (size1 l)" let ?rl = "real (size1 rl)"
let ?l' = "real (size1 l')" let ?r' = "real (size1 r')"
have "1 + log α (?l' + ?r') + β * log α (?l + ?rl) + β * log α (?l' + ?l + ?rl) ≤
β * log α (?l' + ?r') + β * log α (?l' + ?rl + ?r') + log α (?l' + ?rl + ?r' + ?l)" (is "?L≤?R")
proof(rule powr_le_cancel_iff[THEN iffD1, OF a1])
show "α powr ?L ≤ α powr ?R" using A2[of ?r' ?l' ?rl ?l]
by(simp add: powr_add add.commute add.left_commute mult.commute[of β] powr_powr[symmetric])
qed
thus ?case using 3 sp 1 ‹rr ≠ Leaf›
by(auto simp add: Am_simp3' φ_def log_divide algebra_simps)
qed
qed
lemma Am_ub3: assumes "bst t" shows "Am t ≤ log α (size1 t) + 1"
proof cases
assume "t = Leaf" thus ?thesis by(simp add: Am_def)
next
assume "t ≠ Leaf"
have [arith]: "log α 2 > 0" by simp
show ?thesis using Am_ub[OF assms ‹t ≠ Leaf›] by(simp add: Am_def log_divide)
qed
end
subsubsection "Optimal Interpretation"
lemma mult_root_eq_root:
"n>0 ⟹ y ≥ 0 ⟹ root n x * y = root n (x * (y ^ n))"
by(simp add: real_root_mult real_root_pos2)
lemma mult_root_eq_root2:
"n>0 ⟹ y ≥ 0 ⟹ y * root n x = root n ((y ^ n) * x)"
by(simp add: real_root_mult real_root_pos2)
lemma powr_inverse_numeral:
"0 < x ⟹ x powr (1 / numeral n) = root (numeral n) x"
by (simp add: root_powr_inverse)
lemmas root_simps = mult_root_eq_root mult_root_eq_root2 powr_inverse_numeral
lemma nl31: "⟦ (l'::real) ≥ 1; r' ≥ 1; lr ≥ 1; r ≥ 1 ⟧ ⟹
4 * (l' + r') * (lr + r) ≤ (l' + lr + r' + r)^2"
by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [r + ~1*l' + lr + ~1*r']^2))))")
lemma nl32: assumes "(l'::real) ≥ 1" "r' ≥ 1" "lr ≥ 1" "r ≥ 1"
shows "4 * (l' + r') * (lr + r) * (lr + r' + r) ≤ (l' + lr + r' + r)^3"
proof -
have 1: "lr + r' + r ≤ l' + lr + r' + r" using assms by arith
have 2: "0 ≤ (l' + lr + r' + r)^2" by (rule zero_le_power2)
have 3: "0 ≤ lr + r' + r" using assms by arith
from mult_mono[OF nl31[OF assms] 1 2 3] show ?thesis
by(simp add: ac_simps numeral_eq_Suc)
qed
lemma nl3: assumes "(l'::real) ≥ 1" "r' ≥ 1" "lr ≥ 1" "r ≥ 1"
shows "4 * (l' + r')^2 * (lr + r) * (lr + r' + r)
≤ (l' + lr + r') * (l' + lr + r' + r)^3"
proof-
have 1: "l' + r' ≤ l' + lr + r'" using assms by arith
have 2: "0 ≤ (l' + lr + r' + r)^3" using assms by simp
have 3: "0 ≤ l' + r'" using assms by arith
from mult_mono[OF nl32[OF assms] 1 2 3] show ?thesis
unfolding power2_eq_square by (simp only: ac_simps)
qed
lemma nl41: assumes "(l'::real) ≥ 1" "r' ≥ 1" "ll ≥ 1" "r ≥ 1"
shows "4 * (l' + ll) * (r' + r) ≤ (l' + ll + r' + r)^2"
using assms by (sos "(((A<0 * R<1) + (R<1 * (R<1 * [r + ~1*l' + ~1*ll + r']^2))))")
lemma nl42: assumes "(l'::real) ≥ 1" "r' ≥ 1" "ll ≥ 1" "r ≥ 1"
shows "4 * (l' + r') * (l' + ll) * (r' + r) ≤ (l' + ll + r' + r)^3"
proof -
have 1: "l' + r' ≤ l' + ll + r' + r" using assms by arith
have 2: "0 ≤ (l' + ll + r' + r)^2" by (rule zero_le_power2)
have 3: "0 ≤ l' + r'" using assms by arith
from mult_mono[OF nl41[OF assms] 1 2 3] show ?thesis
by(simp add: ac_simps numeral_eq_Suc del: distrib_right_numeral)
qed
lemma nl4: assumes "(l'::real) ≥ 1" "r' ≥ 1" "ll ≥ 1" "r ≥ 1"
shows "4 * (l' + r')^2 * (l' + ll) * (r' + r)
≤ (l' + ll + r') * (l' + ll + r' + r)^3"
proof-
have 1: "l' + r' ≤ l' + ll + r'" using assms by arith
have 2: "0 ≤ (l' + ll + r' + r)^3" using assms by simp
have 3: "0 ≤ l' + r'" using assms by arith
from mult_mono[OF nl42[OF assms] 1 2 3] show ?thesis
unfolding power2_eq_square by (simp only: ac_simps)
qed
lemma cancel: "x>(0::real) ⟹ c * x ^ 2 * y * z ≤ u * v ⟹ c * x ^ 3 * y * z ≤ x * u * v"
by(simp add: power2_eq_square power3_eq_cube)
interpretation S34: Splay_Analysis "root 3 4" "1/3"
proof (standard, goal_cases)
case 2 thus ?case
by(simp add: root_simps)
(auto simp: numeral_eq_Suc split_mult_pos_le intro!: mult_mono)
next
case 3 thus ?case by(simp add: root_simps cancel nl3)
next
case 4 thus ?case by(simp add: root_simps cancel nl4)
qed simp
lemma log4_log2: "log 4 x = log 2 x / 2"
proof -
have "log 4 x = log (2^2) x" by simp
also have "… = log 2 x / 2" by(simp only: log_base_pow)
finally show ?thesis .
qed
declare log_base_root[simp]
lemma A34_ub: assumes "bst t"
shows "S34.A a t ≤ (3/2) * log 2 (size1 t) + 1"
proof -
have "S34.A a t ≤ log (root 3 4) (size1 t) + 1" by(rule S34.A_ub3[OF assms])
also have "… = (3/2) * log 2 (size t + 1) + 1" by(simp add: log4_log2)
finally show ?thesis by simp
qed
lemma Am34_ub: assumes "bst t"
shows "S34.Am t ≤ (3/2) * log 2 (size1 t) + 1"
proof -
have "S34.Am t ≤ log (root 3 4) (size1 t) + 1" by(rule S34.Am_ub3[OF assms])
also have "… = (3/2) * log 2 (size1 t) + 1" by(simp add: log4_log2)
finally show ?thesis by simp
qed
subsubsection "Overall analysis"
fun U where
"U Empty [] = 1" |
"U (Splay _) [t] = (3/2) * log 2 (size1 t) + 1" |
"U (Insert _) [t] = 2 * log 2 (size1 t) + 3/2" |
"U (Delete _) [t] = 3 * log 2 (size1 t) + 2"
interpretation Amortized
where arity = arity and exec = exec and inv = bst
and cost = cost and Φ = S34.Φ 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) show ?case by(induction t)(simp_all add: S34.φ_def)
next
case (3 ss f)
show ?case (is "?l ≤ ?r")
proof(cases f)
case Empty thus ?thesis using 3(2) by(simp add: S34.A_def)
next
case (Splay a)
then obtain t where "ss = [t]" "bst t" using 3 by auto
thus ?thesis using S34.A_ub3[OF ‹bst t›] Splay
by(simp add: S34.A_def log4_log2)
next
case [simp]: (Insert a)
obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
show ?thesis
proof cases
assume "t = Leaf" thus ?thesis by(simp add: S34.φ_def log4_log2)
next
assume "t ≠ Leaf"
then obtain l e r where [simp]: "splay a t = Node l e r"
by (metis tree.exhaust splay_Leaf_iff)
let ?t = "real(T_splay a t)"
let ?Plr = "S34.Φ l + S34.Φ r" let ?Ps = "S34.Φ t"
let ?slr = "real(size1 l) + real(size1 r)" let ?LR = "log 2 (1 + ?slr)"
have opt: "?t + S34.Φ (splay a t) - ?Ps ≤ 3/2 * log 2 (real (size1 t)) + 1"
using S34.A_ub3[OF ‹bst t›, simplified S34.A_def, of a]
by (simp add: log4_log2)
from less_linear[of e a]
show ?thesis
proof (elim disjE)
assume "e=a"
have nneg: "log 2 (1 + real (size t)) ≥ 0" by simp
thus ?thesis using ‹t ≠ Leaf› opt ‹e=a›
apply(simp add: field_simps) using nneg by arith
next
let ?L = "log 2 (real(size1 l) + 1)"
assume "e<a" hence "e ≠ a" by simp
hence "?l = (?t + ?Plr - ?Ps) + ?L / 2 + ?LR / 2"
using ‹t ≠ Leaf› ‹e<a› by(simp add: S34.φ_def log4_log2)
also have "?t + ?Plr - ?Ps ≤ log 2 ?slr + 1"
using opt size_splay[of a t,symmetric]
by(simp add: S34.φ_def log4_log2)
also have "?L/2 ≤ log 2 ?slr / 2" by(simp)
also have "?LR/2 ≤ log 2 ?slr / 2 + 1/2"
proof -
have "?LR/2 ≤ log 2 (2 * ?slr) / 2" by simp
also have "… ≤ log 2 ?slr / 2 + 1/2"
by (simp add: log_mult del:distrib_left_numeral)
finally show ?thesis .
qed
finally show ?thesis using size_splay[of a t,symmetric] by simp
next
let ?R = "log 2 (2 + real(size r))"
assume "a<e" hence "e ≠ a" by simp
hence "?l = (?t + ?Plr - ?Ps) + ?R / 2 + ?LR / 2"
using ‹t ≠ Leaf› ‹a<e› by(simp add: S34.φ_def log4_log2)
also have "?t + ?Plr - ?Ps ≤ log 2 ?slr + 1"
using opt size_splay[of a t,symmetric]
by(simp add: S34.φ_def log4_log2)
also have "?R/2 ≤ log 2 ?slr / 2" by(simp)
also have "?LR/2 ≤ log 2 ?slr / 2 + 1/2"
proof -
have "?LR/2 ≤ log 2 (2 * ?slr) / 2" by simp
also have "… ≤ log 2 ?slr / 2 + 1/2"
by (simp add: log_mult del:distrib_left_numeral)
finally show ?thesis .
qed
finally show ?thesis using size_splay[of a t,symmetric] by simp
qed
qed
next
case [simp]: (Delete a)
obtain t where [simp]: "ss = [t]" and "bst t" using 3 by auto
show ?thesis
proof (cases t)
case Leaf thus ?thesis
by(simp add: Splay_Tree.delete_def S34.φ_def log4_log2)
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 = "S34.Φ l + S34.Φ r" let ?Ps = "S34.Φ 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 + S34.Φ (splay a t) - ?Ps ≤ 3/2 * log 2 (real (size1 t)) + 1"
using S34.A_ub3[OF ‹bst t›, simplified S34.A_def, of a]
by (simp add: log4_log2 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 "S34.φ Leaf r ≥ 0" by(simp add: S34.φ_def)
thus ?thesis using Leaf opt
apply(simp add: Splay_Tree.delete_def field_simps)
using ‹?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 "S34.Φ r' ≥ 0" apply (induction r') by (auto simp add: S34.φ_def)
have optm: "real(T_splay_max l) + S34.Φ (splay_max l) - S34.Φ l
≤ 3/2 * log 2 (real (size1 l)) + 1"
using S34.Am_ub3[OF ‹bst l›, simplified S34.Am_def]
by (simp add: log4_log2 field_simps Node)
have 1: "log 4 (2+(real(size l')+real(size r))) ≤
log 4 (2+(real(size l)+real(size r)))"
using size_splay_max[of l] Node by simp
have 2: "log 4 (2 + (real (size l') + real (size r'))) ≥ 0" by simp
have 3: "S34.φ l' r ≤ S34.φ l' r' + S34.φ l r"
apply(simp add: S34.φ_def) 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 ‹S34.Φ r' ≥ 0› by arith
qed
qed
qed
qed
qed
end