Theory VEBT_DeleteBounds
theory VEBT_DeleteBounds imports VEBT_Bounds VEBT_Delete VEBT_DeleteCorrectness
begin
subsection ‹Running Time Bounds for Deletion›
context begin
interpretation VEBT_internal .
fun T⇩d⇩e⇩l⇩e⇩t⇩e::"VEBT ⇒ nat ⇒ nat" where
"T⇩d⇩e⇩l⇩e⇩t⇩e (Leaf a b) 0 = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e (Leaf a b) (Suc 0) = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e (Leaf a b) (Suc (Suc n)) = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e (Node None deg treeList summary) _ = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) 0 treeList summary) x = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) (Suc 0) treeList summary) x =1 "|
"T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 3 + (
if (x < mi ∨ x > ma) then 1
else 3 + (if (x = mi ∧ x = ma) then 3
else 13 + ( if x = mi then T⇩m⇩i⇩n⇩t summary + T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7 else 1 )+
(if x = mi then 1 else 1) +
( let xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))
else x);
minn = (if x = mi then xn else mi);
l = low xn (deg div 2);
h = high xn (deg div 2) in
if h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary h + (
let sn = vebt_delete summary h in
2+ (if xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) )
else 1)
))else
2 + (if xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! h) else 1)
)))else 1 )))"
end
context VEBT_internal begin
lemma tdeletemimi:
assumes "deg ≥ 2"
shows "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, mi)) deg treeList summary) x ≤ 9"
proof -
obtain deg' :: nat where "deg = Suc (Suc deg')"
using add_2_eq_Suc assms le_Suc_ex by blast
then show ?thesis
by simp
qed
lemma minNull_delete_time_bound: "invar_vebt t n ⟹ minNull (vebt_delete t x) ⟹ T⇩d⇩e⇩l⇩e⇩t⇩e t x ≤ 9"
proof(induction t n rule: invar_vebt.induct)
case (1 a b)
then consider "x = 0" | "x = Suc 0" | x' where "x = Suc (Suc x')"
by (metis nat.exhaust)
then show ?case
by cases simp_all
next
case (2 treeList n summary m deg)
then show ?case by simp
next
case (3 treeList n summary m deg)
then show ?case by simp
next
case (4 treeList n summary m deg mi ma)
hence "deg ≥ 2"
by (metis add_self_div_2 deg_not_0 div_greater_zero_iff)
show ?case
proof (cases "mi = ma")
case True
then show ?thesis
using ‹2 ≤ deg› tdeletemimi by metis
next
case False
obtain mi' ma' treeList' summary' where
"vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
Node (Some (mi', ma')) deg treeList' summary'" (is "?LHS = ?RHS mi' ma' treeList' summary'")
proof atomize_elim
show "∃mi' ma' treeList' summary'. ?LHS = ?RHS mi' ma' treeList' summary'"
proof (cases "x < mi ∨ x > ma")
case True
show ?thesis
by (simp add: delt_out_of_range[OF True ‹2 ≤ deg›])
next
case False
then have "mi ≤ x ∧ x ≤ ma"
by linarith
then show ?thesis
by (simp
add: del_in_range[of mi x ma deg, OF ‹mi ≤ x ∧ x ≤ ma› ‹mi ≠ ma› ‹2 ≤ deg›] Let_def
split: if_split)
qed
qed
then have "¬ minNull (vebt_delete (Node (Some (mi, ma)) deg treeList summary) x)"
by simp
then have False
using ‹minNull (vebt_delete (Node (Some (mi, ma)) deg treeList summary) x)›
by contradiction
then show ?thesis ..
qed
next
case (5 treeList n summary m deg mi ma)
hence "deg ≥ 2"
by (metis Suc_1 add_mono_thms_linordered_semiring(1) le_add1 plus_1_eq_Suc set_n_deg_not_0)
show ?case
proof (cases "mi = ma")
case True
then show ?thesis
using ‹2 ≤ deg› tdeletemimi by metis
next
case False
obtain mi' ma' treeList' summary' where
"vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
Node (Some (mi', ma')) deg treeList' summary'" (is "?LHS = ?RHS mi' ma' treeList' summary'")
proof atomize_elim
show "∃mi' ma' treeList' summary'. ?LHS = ?RHS mi' ma' treeList' summary'"
proof (cases "x < mi ∨ x > ma")
case True
show ?thesis
by (simp add: delt_out_of_range[OF True ‹2 ≤ deg›])
next
case False
then have "mi ≤ x ∧ x ≤ ma"
by linarith
then show ?thesis
by (simp
add: del_in_range[of mi x ma deg, OF ‹mi ≤ x ∧ x ≤ ma› ‹mi ≠ ma› ‹2 ≤ deg›] Let_def
split: if_split)
qed
qed
then have "¬ minNull (vebt_delete (Node (Some (mi, ma)) deg treeList summary) x)"
by simp
then have False
using ‹minNull (vebt_delete (Node (Some (mi, ma)) deg treeList summary) x)›
by contradiction
then show ?thesis ..
qed
qed
lemma delete_bound_height: "invar_vebt t n ⟹ T⇩d⇩e⇩l⇩e⇩t⇩e t x ≤ (1+ height t)*70"
proof(induction t n arbitrary: x rule: invar_vebt.induct)
case (1 a b)
then consider "x = 0" | "x = Suc 0" | x' where "x = Suc (Suc x')"
by (metis nat.exhaust)
then show ?case
by cases simp_all
next
case (2 treeList n summary m deg)
then show ?case by simp
next
case (3 treeList n summary m deg)
then show ?case by simp
next
case (4 treeList n summary m deg mi ma)
hence deggy: "deg ≥ 2"
by (metis add_self_div_2 deg_not_0 div_greater_zero_iff)
then obtain deg' :: nat where "deg = Suc (Suc deg')"
using add_2_eq_Suc le_Suc_ex by blast
then show ?case
proof(cases " (x < mi ∨ x > ma)")
case True
hence " T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 4"
by (simp add: ‹deg = Suc (Suc deg')›)
then show ?thesis using T⇩d⇩e⇩l⇩e⇩t⇩e.simps(7)[of mi ma "deg-2" treeList summary x] by auto
next
case False
hence "mi ≤ x ∧ x ≤ ma" by simp
hence 0: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 3+3 + (if (x = mi ∧ x = ma) then 3
else 13 + ( if x = mi then T⇩m⇩i⇩n⇩t summary + T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7 else 1 )+
(if x = mi then 1 else 1) +
( let xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))
else x);
minn = (if x = mi then xn else mi);
l = low xn (deg div 2);
h = high xn (deg div 2) in
if h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary h + (
let sn = vebt_delete summary h in
2+ (if xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) )
else 1)
))else
2 + (if xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! h) else 1)
)))else 1 ))"
by (simp add: ‹deg = Suc (Suc deg')›)
then show ?thesis
proof(cases " (x = mi ∧ x = ma)")
case True
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 9" using 0 by simp
then show ?thesis by simp
next
case False
hence 1: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x =3+3 +13+
(if x = mi then T⇩m⇩i⇩n⇩t summary + T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7 else 1 )+
(if x = mi then 1 else 1) +
(let xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))
else x);
minn = (if x = mi then xn else mi);
l = low xn (deg div 2);
h = high xn (deg div 2) in
if h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary h + (
let sn = vebt_delete summary h in
2+ (if xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) )
else 1)
))else
2 + (if xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! h) else 1)
)))else 1 )" using 0
by (simp add: False)
then show ?thesis
proof(cases "x = mi")
case True
let ?xn = " the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))"
have 2: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x =3+3 +13+ T⇩m⇩i⇩n⇩t summary +
T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7+1 +
(let l = low ?xn (deg div 2);
h = high ?xn (deg div 2) in
if h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary h + (
let sn = vebt_delete summary h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! h) else 1)
)))else 1 )"
using 1
unfolding True Let_def
by simp
let ?l = "low ?xn (deg div 2)"
let ?h = "high ?xn (deg div 2)"
have 3: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 3+3 +13+ T⇩m⇩i⇩n⇩t summary +
T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7+1 +
(if ?h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = treeList[?h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! ?h) else 1)
)))else 1 )"
using 2 by meson
then show ?thesis
proof(cases "?h < length treeList")
case True
hence "?h < length treeList" by simp
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:= ?newnode]"
have "invar_vebt (treeList ! ?h) n"
using "4.IH"(1) True nth_mem by blast
hence "invar_vebt ?newnode n"
using delete_pres_valid by blast
have 4: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 37 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = treeList[?h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! ?h) else 1)
))"
using 3 mint_bound[of "treeList ! the (vebt_mint summary)"] mint_bound[of "summary"]
by simp
hence 5: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 38 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + (
if minNull ?newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1) ))else
2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1)
))"
unfolding Let_def by linarith
then show ?thesis
proof(cases "minNull ?newnode ")
case True
hence 6: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 39 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1))" using 5 minNull_bound[of ?newnode] by presburger
have 7: " T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l ≤ 9" using True
minNull_delete_time_bound[of "treeList ! ?h"]
using ‹invar_vebt (treeList ! high (the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (deg div 2)) n› by blast
let ?sn = "vebt_delete summary ?h"
have 8: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 39 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1))"
by (meson "6")
hence 9: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 39 + 9 + 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + 2+
(if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1)" using 6 7 by force
hence 10: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 51 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
(if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1)" by simp
then show ?thesis
proof(cases "?xn = ma")
case True
hence 10: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 51 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
))" using 10
by presburger
also have "… ≤ 55 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
(let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
))" using maxt_bound[of ?sn] by force
also have "… ≤ 55 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + 1 + 8 + T⇩m⇩a⇩x⇩t (?newlist ! the (vebt_maxt ?sn))"
by (cases " vebt_maxt ?sn"; fastforce)
also have "… ≤ 67 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h"
using maxt_bound[of "?newlist ! the (vebt_maxt ?sn)"] by linarith
also have "… ≤ 67 + (1 + height summary) * 70"
using "4.IH"(2) by simp
also have "… ≤ 67 + (height (Node (Some (mi, ma)) deg treeList summary)) * 70"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by simp
next
case False
hence 11: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 52 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h"
using 10 by simp
also have "… ≤ 52 + (1+ height summary)*70"
using "4.IH"(2) by simp
also have "… ≤ 52 + (height (Node (Some (mi, ma)) deg treeList summary)) * 70"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by simp
qed
next
case False
hence 6: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 38 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + 2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1))" using 5 by simp
moreover have "invar_vebt (?newlist ! ?h) n"
by (simp add: True ‹invar_vebt (vebt_delete (treeList ! high (the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (deg div 2)) (low (the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (deg div 2))) n›)
ultimately have "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤
43 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1)"
using minNull_bound[of ?newnode] by linarith
moreover have " (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1) ≤ 9"
apply(cases "?xn = ma") using maxt_bound[of " (?newlist ! ?h) "] by simp+
ultimately have "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 55 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l" by force
also have "… ≤ 55 + (1 + height (treeList ! ?h)) * 70"
using "4.IH"(1) True by simp
also have "… ≤ 55 + (height (Node (Some (mi, ma)) deg treeList summary)) * 70"
using height_compose_child[of "treeList ! ?h" treeList "Some (mi, ma)" deg summary]
by (meson True mult_le_mono1 nat_add_left_cancel_le nth_mem)
finally show ?thesis
by simp
qed
next
case False
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 3+3 +13+ T⇩m⇩i⇩n⇩t summary +
T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7+1 +1" using 3 by simp
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 34" using
mint_bound[of "treeList ! the (vebt_mint summary)"]
mint_bound[of "summary"] by simp
then show ?thesis by simp
qed
next
case False
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
have 2: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x =3+3 +13+1 +1 +
(let l = low x (deg div 2);
h = high x (deg div 2) in
if h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary h + (
let sn = vebt_delete summary h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! h) else 1)
)))else 1 )"
using 1 False by simp
hence 3: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 21+(
if ?h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = treeList[?h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! ?h) else 1)
)))else 1 )"
by (simp add: Let_def)
then show ?thesis
proof(cases "?h < length treeList")
case True
hence "?h < length treeList" by simp
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:= ?newnode]"
have "invar_vebt (treeList ! ?h) n"
using "4.IH"(1) True nth_mem by blast
hence "invar_vebt ?newnode n"
using delete_pres_valid by blast
hence 4: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 21+ 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + (
if minNull ?newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1) ))else
2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1))"
using 3 mint_bound[of "treeList ! the (vebt_mint summary)"] mint_bound[of "summary"]
by (smt (verit) True add.assoc)
hence 5: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 26 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + (
if minNull ?newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1) ))else
2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1))" by force
then show ?thesis
proof(cases "minNull ?newnode ")
case True
hence 6: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 29 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1))" using 5 minNull_bound[of ?newnode] by force
have 7: " T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l ≤ 9" using True
minNull_delete_time_bound[of "treeList ! ?h"]
using ‹invar_vebt (treeList ! high x (deg div 2)) n› by blast
let ?sn = "vebt_delete summary ?h"
have 8: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 29 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1))"
by (meson "6")
hence 9: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 29 + 9 + 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + 2+
(if x = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1)"
using 6 7 by force
hence 10: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 41 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
(if x = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1)"
by simp
then show ?thesis
proof(cases "x = ma")
case True
hence 10: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 41 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
))"
using 10 by presburger
also have "… ≤ 45 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
(let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
))"
using maxt_bound[of ?sn] by force
also have "… ≤ 45 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + 1 + 8 + T⇩m⇩a⇩x⇩t (?newlist ! the (vebt_maxt ?sn))"
by (cases " vebt_maxt ?sn"; fastforce)
also have "… ≤ 57 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h "
using maxt_bound[of "?newlist ! the (vebt_maxt ?sn)"] by linarith
also have "… ≤ 57 + (1+ height summary) * 70"
using "4.IH"(2) by simp
also have "… ≤ 57 + (height (Node (Some (mi, ma)) deg treeList summary)) * 70"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by simp
next
case False
hence 11: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 42 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h "
using 10 by simp
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 42 + (1+ height summary)*70"
by (meson "4.IH"(2) le_trans nat_add_left_cancel_le)
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤
42 + (height (Node (Some (mi, ma)) deg treeList summary) )*70" using height_compose_summary[of summary "Some (mi, ma)" deg treeList ]
by (meson add_mono_thms_linordered_semiring(2) le_refl mult_le_mono order_trans)
then show ?thesis by simp
qed
next
case False
hence 6: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 26 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + 2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1))" using 5 by simp
moreover have "invar_vebt (?newlist ! ?h) n"
by (simp add: True ‹invar_vebt (vebt_delete (treeList ! high x (deg div 2)) (low x (deg div 2))) n›)
ultimately have "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤
29 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1)"
using minNull_bound[of ?newnode] by linarith
moreover have " (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1) ≤ 9"
apply(cases "x = ma") using maxt_bound[of " (?newlist ! ?h) "] by simp+
ultimately have "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤
38 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l" by force
also have "… ≤ 38 + (1 + height (treeList ! ?h)) * 70"
using "4.IH"(1) True by simp
also have "… ≤ 38 + (height (Node (Some (mi, ma)) deg treeList summary)) * 70"
using height_compose_child[of "treeList ! ?h" treeList "Some (mi, ma)" deg summary]
by (meson True add_le_cancel_left mult_le_mono1 nth_mem)
finally show ?thesis
by presburger
qed
next
case False
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 21+1" using 3 by simp
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 22" using
mint_bound[of "treeList ! the (vebt_mint summary)"]
mint_bound[of "summary"] by simp
then show ?thesis by simp
qed
qed
qed
qed
next
case (5 treeList n summary m deg mi ma)
hence deggy: "deg ≥ 2"
by (metis Suc_1 add_mono_thms_linordered_semiring(1) le_add1 plus_1_eq_Suc set_n_deg_not_0)
then obtain deg' where "deg = Suc (Suc deg')"
using add_2_eq_Suc le_Suc_ex by blast
then show ?case
proof(cases " (x < mi ∨ x > ma)")
case True
hence " T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 4"
by (simp add: ‹deg = Suc (Suc deg')›)
then show ?thesis using T⇩d⇩e⇩l⇩e⇩t⇩e.simps(7)[of mi ma "deg-2" treeList summary x] by auto
next
case False
hence "mi ≤ x ∧ x ≤ ma" by simp
hence 0: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 3+3 + (if (x = mi ∧ x = ma) then 3
else 13 + ( if x = mi then T⇩m⇩i⇩n⇩t summary + T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7 else 1 )+
(if x = mi then 1 else 1) +
( let xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))
else x);
minn = (if x = mi then xn else mi);
l = low xn (deg div 2);
h = high xn (deg div 2) in
if h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary h + (
let sn = vebt_delete summary h in
2+ (if xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) )
else 1)
))else
2 + (if xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! h) else 1)
)))else 1 ))"
by (simp add: ‹deg = Suc (Suc deg')›)
then show ?thesis
proof(cases " (x = mi ∧ x = ma)")
case True
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 9" using 0 by simp
then show ?thesis by simp
next
case False
hence 1: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x =3+3 +13+
( if x = mi then T⇩m⇩i⇩n⇩t summary + T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7 else 1 )+
(if x = mi then 1 else 1) +
( let xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))
else x);
minn = (if x = mi then xn else mi);
l = low xn (deg div 2);
h = high xn (deg div 2) in
if h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary h + (
let sn = vebt_delete summary h in
2+ (if xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) )
else 1)
))else
2 + (if xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! h) else 1)
)))else 1 )" using 0
by (simp add: False)
then show ?thesis
proof(cases "x = mi")
case True
let ?xn = " the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))"
have 2: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x =3+3 +13+ T⇩m⇩i⇩n⇩t summary +
T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7+1 +
(let l = low ?xn (deg div 2);
h = high ?xn (deg div 2) in
if h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary h + (
let sn = vebt_delete summary h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! h) else 1)
)))else 1 )"
using 1
unfolding True Let_def
by force
let ?l = "low ?xn (deg div 2)"
let ?h = "high ?xn (deg div 2)"
have 3: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 3+3 +13+ T⇩m⇩i⇩n⇩t summary +
T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7+1 +
(if ?h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = treeList[?h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! ?h) else 1)
)))else 1 )"
using 2 by meson
then show ?thesis
proof(cases "?h < length treeList")
case True
hence "?h < length treeList" by simp
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:= ?newnode]"
have "invar_vebt (treeList ! ?h) n"
using "5.IH"(1) True nth_mem by blast
hence "invar_vebt ?newnode n"
using delete_pres_valid by blast
have 4: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 37 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = treeList[?h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! ?h) else 1)
))"
using 3 mint_bound[of "treeList ! the (vebt_mint summary)"] mint_bound[of "summary"]
by simp
hence 5: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 38 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + (
if minNull ?newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1) ))else
2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1)
))"
unfolding Let_def
by linarith
then show ?thesis
proof(cases "minNull ?newnode ")
case True
hence 6: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 39 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1))" using 5 minNull_bound[of ?newnode] by presburger
have 7: " T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l ≤ 9" using True
minNull_delete_time_bound[of "treeList ! ?h"]
using ‹invar_vebt (treeList ! high (the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (deg div 2)) n› by blast
let ?sn = "vebt_delete summary ?h"
have 8: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 39 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
2+ (if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1))"
by (meson "6")
hence 9: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 39 + 9 + 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + 2+
(if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1)"
using 6 7 by force
hence 10: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 51 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
(if ?xn = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1)"
by simp
then show ?thesis
proof(cases "?xn = ma")
case True
hence 10: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 51 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
))"
using 10 by presburger
also have 11: "… ≤ 55 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
(let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
))"
using maxt_bound[of ?sn] by force
also have 12: "… ≤ 55 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + 1 + 8 + T⇩m⇩a⇩x⇩t (?newlist ! the (vebt_maxt ?sn))"
by (cases " vebt_maxt ?sn"; fastforce)
also have "… ≤ 67 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h "
using maxt_bound[of "?newlist ! the (vebt_maxt ?sn)"] by linarith
also have "… ≤ 67 + (1 + height summary) * 70"
using "5.IH"(2) by simp
also have "… ≤ 67 + (height (Node (Some (mi, ma)) deg treeList summary)) * 70"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by simp
next
case False
hence 11: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 52 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h "
using 10 by simp
also have "… ≤ 52 + (1+ height summary) * 70"
using "5.IH"(2) by simp
also have "… ≤ 52 + (height (Node (Some (mi, ma)) deg treeList summary)) * 70"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by simp
qed
next
case False
hence 6: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 38 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + 2 + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1))" using 5 by simp
moreover have "invar_vebt (?newlist ! ?h) n"
by (simp add: True ‹invar_vebt (vebt_delete (treeList ! high (the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (deg div 2)) (low (the (vebt_mint summary) * 2 ^ (deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))) (deg div 2))) n›)
ultimately have "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤
43 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l + (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1)"
using minNull_bound[of ?newnode] by linarith
moreover have " (if ?xn = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1) ≤ 9"
apply(cases "?xn = ma") using maxt_bound[of " (?newlist ! ?h) "] by simp+
ultimately have "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 55 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l" by force
also have "… ≤ 55 + (1 + height (treeList ! ?h)) * 70"
using "5.IH"(1) True by simp
also have "… ≤ 55 + (height (Node (Some (mi, ma)) deg treeList summary)) * 70"
using height_compose_child[of "treeList ! ?h" treeList "Some (mi, ma)" deg summary]
by (meson True mult_le_mono1 nat_add_left_cancel_le nth_mem)
finally show ?thesis
by simp
qed
next
case False
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 3+3 +13+ T⇩m⇩i⇩n⇩t summary +
T⇩m⇩i⇩n⇩t (treeList ! the (vebt_mint summary))+ 7+1 +1" using 3 by simp
also have "… ≤ 34"
using mint_bound[of "treeList ! the (vebt_mint summary)"] mint_bound[of "summary"]
by linarith
finally show ?thesis
by simp
qed
next
case False
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
have 2: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x =3+3 +13+1 +1 +
(let l = low x (deg div 2);
h = high x (deg div 2) in
if h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary h + (
let sn = vebt_delete summary h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! h) else 1)
)))else 1 )" using 1 False by simp
hence 3: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 21+(
if ?h < length treeList
then( 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = treeList[?h:= newnode]in 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l newnode + (
if minNull newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (newlist ! the maxs)
) ) else 1) ))else
2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (newlist ! ?h) else 1)
)))else 1 )"
by (simp add: Let_def)
then show ?thesis
proof(cases "?h < length treeList")
case True
hence "?h < length treeList" by simp
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:= ?newnode]"
have "invar_vebt (treeList ! ?h) n"
using "5.IH"(1) True nth_mem by blast
hence "invar_vebt ?newnode n"
using delete_pres_valid by blast
hence 4: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 21+ 4 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + (
if minNull ?newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1) ))else
2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1))" using 3 mint_bound[of "treeList ! the (vebt_mint summary)"]
mint_bound[of "summary"] by (smt (verit) True add.assoc)
hence 5: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 26 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + (
if minNull ?newnode
then( 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1) ))else
2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1))" by force
then show ?thesis
proof(cases "minNull ?newnode ")
case True
hence 6: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 29 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
let sn = vebt_delete summary ?h in
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t sn + (let maxs = vebt_maxt sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1))"
using 5 minNull_bound[of ?newnode] by force
have 7: " T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l ≤ 9" using True
minNull_delete_time_bound[of "treeList ! ?h"]
using ‹invar_vebt (treeList ! high x (deg div 2)) n› by blast
let ?sn = "vebt_delete summary ?h"
have 8: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 29 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l
+ 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + (
2+ (if x = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1))"
by (meson "6")
hence 9: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 29 + 9 + 1 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + 2+
(if x = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1)"
using 6 7 by force
hence 10: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 41 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
(if x = ma then 1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
) ) else 1)"
by simp
then show ?thesis
proof(cases "x = ma")
case True
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 41 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
1 + T⇩m⇩a⇩x⇩t ?sn + (let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
))"
using 10 by presburger
also have "… ≤ 45 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h +
(let maxs = vebt_maxt ?sn in
1 + (if maxs = None
then 1
else 8+ T⇩m⇩a⇩x⇩t (?newlist ! the maxs)
))"
using maxt_bound[of ?sn] by linarith
also have "… ≤ 45 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h + 1 + 8 + T⇩m⇩a⇩x⇩t (?newlist ! the (vebt_maxt ?sn))"
by (cases " vebt_maxt ?sn"; fastforce)
also have "… ≤ 57 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h"
using maxt_bound[of "?newlist ! the (vebt_maxt ?sn)"] by linarith
also have "… ≤ 57 + (1+ height summary)*70"
using "5.IH"(2) by simp
also have "… ≤ 57 + (height (Node (Some (mi, ma)) deg treeList summary) )*70"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis by presburger
next
case False
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 42 + T⇩d⇩e⇩l⇩e⇩t⇩e summary ?h"
using 10 by simp
also have "… ≤ 42 + (1 + height summary) * 70"
using "5.IH"(2) by simp
also have "… ≤ 42 + (height (Node (Some (mi, ma)) deg treeList summary)) * 70"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by simp
qed
next
case False
hence 6: "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 26 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l +(
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l ?newnode + 2 + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1))" using 5 by simp
moreover have "invar_vebt (?newlist ! ?h) n"
by (simp add: True ‹invar_vebt (vebt_delete (treeList ! high x (deg div 2)) (low x (deg div 2))) n›)
ultimately have "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤
29 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l + (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1)"
using minNull_bound[of ?newnode] by linarith
moreover have " (if x = ma then 6+ T⇩m⇩a⇩x⇩t (?newlist ! ?h) else 1) ≤ 9"
apply(cases "x = ma") using maxt_bound[of " (?newlist ! ?h) "] by simp+
ultimately have "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤
38 + T⇩d⇩e⇩l⇩e⇩t⇩e (treeList ! ?h) ?l" by force
also have "… ≤ 38 + (1 + height (treeList ! ?h))*70"
by (meson "5.IH"(1) True le_trans nat_add_left_cancel_le nth_mem)
also have "… ≤ 38 + (height (Node (Some (mi, ma)) deg treeList summary))*70"
using height_compose_child[of "treeList ! ?h" treeList "Some (mi, ma)" deg summary]
by (meson True mult_le_mono1 nat_add_left_cancel_le nth_mem)
finally show ?thesis
by presburger
qed
next
case False
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x = 21+1" using 3 by simp
hence "T⇩d⇩e⇩l⇩e⇩t⇩e (Node (Some (mi, ma)) deg treeList summary) x ≤ 22" using
mint_bound[of "treeList ! the (vebt_mint summary)"]
mint_bound[of "summary"] by simp
then show ?thesis by simp
qed
qed
qed
qed
qed
theorem delete_bound_size_univ: "invar_vebt t n ⟹ u = 2^n ⟹ T⇩d⇩e⇩l⇩e⇩t⇩e t x ≤ 140 + 70 * lb (lb u)"
using delete_bound_height[of t n x] height_double_log_univ_size[of u n t] by simp
fun T⇩d⇩e⇩l⇩e⇩t⇩e'::"VEBT ⇒ nat ⇒ nat" where
"T⇩d⇩e⇩l⇩e⇩t⇩e' (Leaf a b) 0 = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e' (Leaf a b) (Suc 0) = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e' (Leaf a b) (Suc (Suc n)) = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e' (Node None deg treeList summary) _ = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) 0 treeList summary) x = 1"|
"T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) (Suc 0) treeList summary) x =1 "|
"T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) deg treeList summary) x = (
if (x < mi ∨ x > ma) then 1
else if (x = mi ∧ x = ma) then 1
else ( let xn = (if x = mi
then the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))
else x);
minn = (if x = mi then xn else mi);
l = low xn (deg div 2);
h = high xn (deg div 2) in
if h < length treeList
then( T⇩d⇩e⇩l⇩e⇩t⇩e' (treeList ! h) l +(
let newnode = vebt_delete (treeList ! h) l;
newlist = treeList[h:= newnode]in
if minNull newnode
then T⇩d⇩e⇩l⇩e⇩t⇩e' summary h
else 1
))else 1 ))"
lemma tdeletemimi':"deg ≥ 2 ⟹ T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, mi)) deg treeList summary) x ≤ 1"
using T⇩d⇩e⇩l⇩e⇩t⇩e'.simps(7)[of mi mi "deg-2" treeList summary x]
apply(cases "x ≠ mi")
apply (metis add_2_eq_Suc' le_add_diff_inverse2 le_eq_less_or_eq linorder_neqE_nat)
by (metis add_2_eq_Suc' eq_imp_le le_add_diff_inverse2)
lemma minNull_delete_time_bound': "invar_vebt t n ⟹ minNull (vebt_delete t x) ⟹ T⇩d⇩e⇩l⇩e⇩t⇩e' t x ≤ 1"
proof(induction t n rule: invar_vebt.induct)
case (1 a b)
then show ?case
by (metis T⇩d⇩e⇩l⇩e⇩t⇩e'.simps(1) T⇩d⇩e⇩l⇩e⇩t⇩e'.simps(2) T⇩d⇩e⇩l⇩e⇩t⇩e'.simps(3) vebt_buildup.cases order_refl)
next
case (4 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis One_nat_def VEBT_internal.set_n_deg_not_0 gr0_implies_Suc linorder_not_less not_less_eq_eq)
then have "deg = Suc (Suc (n' + n'))"
unfolding ‹deg = n + m› ‹m = n› by linarith
show ?case
proof (cases "(x < mi ∨ x > ma)")
case True
then show ?thesis
using "4.prems" ‹deg = Suc (Suc _)› delt_out_of_range by force
next
case False
hence "x ≤ ma ∧ x ≥ mi" by simp
show ?thesis
proof (cases "(x = mi ∧ x = ma)")
case True
then show ?thesis
using ‹deg = Suc (Suc _)› tdeletemimi' by force
next
case False
hence "¬ (x = mi ∧ x = ma)" by simp
then obtain mi' ma' treeList' summary' where
"vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
Node (Some (mi', ma')) deg treeList' summary'"
by atomize_elim (simp add: ‹deg = Suc (Suc _)› Let_def)
then have "¬ minNull (vebt_delete (Node (Some (mi, ma)) deg treeList summary) x)"
by simp
then have False
using ‹minNull (vebt_delete (Node (Some (mi, ma)) deg treeList summary) x)›
by contradiction
then show ?thesis ..
qed
qed
next
case (5 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis One_nat_def VEBT_internal.set_n_deg_not_0 gr0_implies_Suc linorder_not_less not_less_eq_eq)
then have "deg = Suc (Suc (Suc (n' + n')))"
unfolding ‹deg = n + m› ‹m = Suc n› by linarith
show ?case
proof (cases "(x < mi ∨ x > ma)")
case True
then show ?thesis
using "5.prems" ‹deg = Suc (Suc _)› delt_out_of_range by force
next
case False
hence "mi ≤ x" and"x ≤ ma" by simp_all
then show ?thesis
proof (cases "(x = mi ∧ x = ma)")
case True
then show ?thesis
using ‹deg = Suc (Suc _)› tdeletemimi' by force
next
case False
hence "¬ (x = mi ∧ x = ma)" by simp
then obtain mi' ma' treeList' summary' where
"vebt_delete (Node (Some (mi, ma)) deg treeList summary) x =
Node (Some (mi', ma')) deg treeList' summary'"
by atomize_elim (simp add: ‹deg = Suc (Suc _)› Let_def)
then have "¬ minNull (vebt_delete (Node (Some (mi, ma)) deg treeList summary) x)"
by simp
then have False
using ‹minNull (vebt_delete (Node (Some (mi, ma)) deg treeList summary) x)›
by contradiction
then show ?thesis ..
qed
qed
qed simp+
lemma delete_bound_height': "invar_vebt t n ⟹ T⇩d⇩e⇩l⇩e⇩t⇩e' t x ≤ 1+ height t"
proof(induction t n arbitrary: x rule: invar_vebt.induct)
case (1 a b)
then show ?case
apply(cases "x ≤ 0")
apply simp
apply(cases "x = 1")
apply simp
using T⇩d⇩e⇩l⇩e⇩t⇩e'.simps(3)[of a b "x-2"] height.simps(1)[of a b]
by (metis One_nat_def T⇩d⇩e⇩l⇩e⇩t⇩e'.simps(3) vebt_buildup.cases lessI less_Suc_eq_le plus_1_eq_Suc)
next
case (4 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis deg_not_0 gr0_implies_Suc)
then have "deg = Suc (Suc (n' + n'))"
using ‹deg = n + m› ‹m = n› by presburger
show ?case
proof (cases "(x < mi ∨ x > ma)")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
hence miama:"mi ≤ x ∧ x ≤ ma" by simp
then show ?thesis
proof(cases "x = mi ∧ x = ma")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
let ?xn = "(if x = mi
then the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))
else x)"
let ?minn = "(if x = mi then ?xn else mi)"
let ?l = "low ?xn (deg div 2)"
let ?h = "high ?xn (deg div 2)"
have 0:"T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) deg treeList summary) x = (if ?h < length treeList
then( T⇩d⇩e⇩l⇩e⇩t⇩e' (treeList ! ?h) ?l +(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = treeList[?h:= newnode]in
if minNull newnode
then T⇩d⇩e⇩l⇩e⇩t⇩e' summary ?h
else 1
))else 1)"
using False miama
by (simp add: ‹deg = Suc (Suc _)› Let_def)
show ?thesis
proof (cases "?h < length treeList")
case True
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:= ?newnode]"
have 1:"T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) deg treeList summary) x =
T⇩d⇩e⇩l⇩e⇩t⇩e' (treeList ! ?h) ?l +(
if minNull ?newnode
then T⇩d⇩e⇩l⇩e⇩t⇩e' summary ?h
else 1 )" using 0 True by simp
then show ?thesis
proof(cases "minNull ?newnode")
case True
hence " T⇩d⇩e⇩l⇩e⇩t⇩e' (treeList ! ?h) ?l ≤ 1"
by (metis "0" "1" "4.IH"(1) minNull_delete_time_bound' nat_le_iff_add nth_mem)
hence "T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) deg treeList summary) x ≤ 1 + T⇩d⇩e⇩l⇩e⇩t⇩e' summary ?h"
using 1 True by auto
also have "… ≤ 1+1+ height summary"
using 4(2)[of ?h] by simp
also have "… ≤ 1 + height (Node (Some (mi, ma)) deg treeList summary)"
by simp
finally show ?thesis .
next
case False
hence "T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) deg treeList summary) x =
1+ T⇩d⇩e⇩l⇩e⇩t⇩e' (treeList ! ?h) ?l " using 1 by simp
also have "… ≤ 1 + 1 + height (treeList ! ?h)"
using "4.IH"(1) True by force
also have "… ≤ 1 + height (Node (Some (mi, ma)) deg treeList summary)"
by (simp add: True)
finally show ?thesis .
qed
qed (simp add : 0)
qed
qed
next
case (5 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis Suc_0_div_numeral(1) Suc_eq_plus1_left add.commute div_by_1 list_decode.cases nth_mem
numerals(1) valid_0_not)
then have "deg = Suc (Suc (Suc (n' + n')))"
using ‹deg = n + m› ‹m = Suc n› by presburger
show ?case
proof(cases "(x < mi ∨ x > ma)")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
hence miama:"mi ≤ x ∧ x ≤ ma" by simp
then show ?thesis
proof(cases "x = mi ∧ x = ma")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
let ?xn = "(if x = mi
then the (vebt_mint summary) * 2^(deg div 2) + the (vebt_mint (treeList ! the (vebt_mint summary)))
else x)"
let ?minn = "(if x = mi then ?xn else mi)"
let ?l = "low ?xn (deg div 2)"
let ?h = "high ?xn (deg div 2)"
have 0:"T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) deg treeList summary) x = (if ?h < length treeList
then( T⇩d⇩e⇩l⇩e⇩t⇩e' (treeList ! ?h) ?l +(
let newnode = vebt_delete (treeList ! ?h) ?l;
newlist = treeList[?h:= newnode]in
if minNull newnode
then T⇩d⇩e⇩l⇩e⇩t⇩e' summary ?h
else 1
))else 1)"
using False miama
by (simp add: ‹deg = Suc (Suc _)› Let_def)
show ?thesis
proof (cases "?h < length treeList")
case True
let ?newnode = "vebt_delete (treeList ! ?h) ?l"
let ?newlist = "treeList[?h:= ?newnode]"
have 1:"T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) deg treeList summary) x =
T⇩d⇩e⇩l⇩e⇩t⇩e' (treeList ! ?h) ?l +(
if minNull ?newnode
then T⇩d⇩e⇩l⇩e⇩t⇩e' summary ?h
else 1 )" using 0 True by simp
then show ?thesis
proof(cases "minNull ?newnode")
case True
hence " T⇩d⇩e⇩l⇩e⇩t⇩e' (treeList ! ?h) ?l ≤ 1"
by (metis "0" "1" "5.IH"(1) minNull_delete_time_bound' nat_le_iff_add nth_mem)
hence "T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) deg treeList summary) x ≤ 1+ T⇩d⇩e⇩l⇩e⇩t⇩e' summary ?h"
using 1 True by auto
also have "… ≤ 1 + 1 + height summary"
using 5(2)[of ?h] by simp
also have "… ≤ 1 + height (Node (Some (mi, ma)) deg treeList summary)"
by simp
finally show ?thesis .
next
case False
hence "T⇩d⇩e⇩l⇩e⇩t⇩e' (Node (Some (mi, ma)) deg treeList summary) x =
1+ T⇩d⇩e⇩l⇩e⇩t⇩e' (treeList ! ?h) ?l " using 1 by simp
also have "… ≤ 1 + 1+ height (treeList ! ?h)"
using "5.IH"(1) True by auto
also have "… ≤ 1 + height (Node (Some (mi, ma)) deg treeList summary)"
by (simp add: True)
finally show ?thesis .
qed
qed (simp add : 0)
qed
qed
qed simp+
theorem delete_bound_size_univ': "invar_vebt t n ⟹ u = 2^n ⟹ T⇩d⇩e⇩l⇩e⇩t⇩e' t x ≤ 2 + lb (lb u)"
using delete_bound_height'[of t n x] height_double_log_univ_size[of u n t] by simp
end
end