Theory VEBT_Bounds
theory VEBT_Bounds imports VEBT_Height VEBT_Member VEBT_Insert VEBT_Succ VEBT_Pred
begin
section ‹Upper Bounds for canonical Functions: Relationships between Run Time and Tree Heights›
subsection ‹Membership test›
context begin
interpretation VEBT_internal .
fun T⇩m⇩e⇩m⇩b⇩e⇩r::"VEBT ⇒ nat ⇒ nat" where
"T⇩m⇩e⇩m⇩b⇩e⇩r (Leaf a b) x = 2 + (if x = 0 then 1 else 1 +( if x=1 then 1 else 1))"|
"T⇩m⇩e⇩m⇩b⇩e⇩r (Node None _ _ _) x = 2"|
"T⇩m⇩e⇩m⇩b⇩e⇩r (Node _ 0 _ _) x = 2"|
"T⇩m⇩e⇩m⇩b⇩e⇩r (Node _ (Suc 0) _ _) x = 2"|
"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 2 + (
if x = mi then 1 else 1+ (
if x = ma then 1 else 1+(
if x < mi then 1 else 1+ (
if x > ma then 1 else 9 +
(let
h = high x (deg div 2);
l = low x (deg div 2) in
(if h < length treeList
then 1 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! h) l
else 1))))))"
fun T⇩m⇩e⇩m⇩b⇩e⇩r'::"VEBT ⇒ nat ⇒ nat" where
"T⇩m⇩e⇩m⇩b⇩e⇩r' (Leaf a b) x = 1"|
"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node None _ _ _) x = 1"|
"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node _ 0 _ _) x = 1"|
"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node _ (Suc 0) _ _) x = 1"|
"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1+(
if x = mi then 0 else (
if x = ma then 0 else (
if x < mi then 0 else (
if x > ma then 0 else if (x>mi ∧ x < ma) then
(let
h = high x (deg div 2);
l = low x (deg div 2) in
(if h < length treeList
then T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! h) l
else 0))
else 0))))"
lemma height_node: "invar_vebt (Node (Some (mi, ma)) deg treeList summary) n
⟹ height (Node (Some (mi, ma)) deg treeList summary) >= 1"
using height.simps(2) by presburger
theorem member_bound_height: "invar_vebt t n ⟹ T⇩m⇩e⇩m⇩b⇩e⇩r t x ≤ (1+height t)*15"
proof(induction t n arbitrary: x rule: invar_vebt.induct)
case (1 a b)
then show ?case by simp
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)
then obtain k :: nat where
"n = Suc k" and "m = Suc k"
by (metis Suc_leI add_Suc_right add_Suc_shift deg_not_0 le_Suc_ex)
then have "deg = Suc (Suc (k + k))"
using ‹deg = n + m› by presburger
then have "deg ≥ 2"
by presburger
then show ?case
proof(cases "x = mi")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 3"
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis
by presburger
next
case False
hence "x ≠ mi" by simp
hence 1:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 3 + (
if x = ma then 1 else 1+(
if x < mi then 1 else 1+ (
if x > ma then 1 else 9 +
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then 1 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! h) l
else 1)))))"
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis
proof(cases "x = ma")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 4" using 1 by auto
then show ?thesis by simp
next
case False
hence "x ≠ ma" by simp
hence 2:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 4 +(
if x < mi then 1 else 1+ (
if x > ma then 1 else 9 +
(let
h = high x (deg div 2);
l = low x (deg div 2) in
(if h < length treeList
then 1 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! h) l
else 1))))"
using 1 by simp
then show ?thesis
proof(cases "x < mi")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 5" using 2 by auto
then show ?thesis by simp
next
case False
hence "x > mi"
using ‹x ≠ mi› antisym_conv3 by blast
hence 3:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 5 + (
if x > ma then 1 else 9 +
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then 1 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! h) l
else 1)))"
using 2 by simp
then show ?thesis
proof(cases "x > ma")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 6" using 3 by simp
then show ?thesis by simp
next
case False
hence "x < ma"
by (meson ‹x ≠ ma› nat_neq_iff)
hence 4:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 14+
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then 1 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! h) l
else 1))"
using 3 by simp
let ?h = "high x (deg div 2)"
let ?l = " low x (deg div 2)"
have "?h < length treeList"
using "4.hyps"(2) "4.hyps"(3) "4.hyps"(4) "4.hyps"(8) ‹x < ma› high_bound_aux by force
hence 5:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 15 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! ?h) ?l"
using "4" by presburger
moreover have "invar_vebt (treeList ! ?h) n ∧ (treeList ! ?h) ∈ set treeList "
using "4.IH"(1) ‹high x (deg div 2) < length treeList› nth_mem by blast
moreover hence " T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! ?h) ?l ≤ (1 + height (treeList ! ?h))*15" using "4.IH"(1) by simp
ultimately have 6:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x ≤
15 + 15 * (1 + height (treeList ! ?h))" by simp
moreover have "i< length treeList ⟹
height (treeList ! i) ≤ Max (height ` (insert summary (set treeList)))" for i
apply (induction treeList arbitrary: i)
apply simp
apply (meson List.finite_set Max_ge finite_imageI finite_insert image_iff nth_mem subsetD subset_insertI)
done
moreover hence " (1 + height (treeList ! ?h)) ≤ height (Node (Some (mi, ma)) deg treeList summary)"
by (simp add: ‹high x (deg div 2) < length treeList›)
moreover hence " 14 * (1 + height (treeList ! ?h)) ≤ 14 * height (Node (Some (mi, ma)) deg treeList summary)" by simp
ultimately show ?thesis
using 6 by simp
qed
qed
qed
qed
next
case (5 treeList n summary m deg mi ma)
then have "1 ≤ n"
by (metis set_n_deg_not_0)
then obtain n' :: nat where "n = Suc n'"
by (metis le_Suc_ex plus_1_eq_Suc)
then have "deg = Suc (Suc (Suc (n' + n')))"
using ‹deg = n + m› ‹m = Suc n› by presburger
then show ?case
proof(cases "x = mi")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 3"
unfolding ‹deg = Suc (Suc _)›
by simp
then show ?thesis by simp
next
case False
hence "x ≠ mi" by simp
hence 1:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 3 + (
if x = ma then 1 else 1+(
if x < mi then 1 else 1+ (
if x > ma then 1 else 9 +
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then 1 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! h) l
else 1)))))"
unfolding ‹deg = Suc (Suc _)›
by simp
then show ?thesis
proof(cases "x = ma")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 4" using 1 by auto
then show ?thesis by simp
next
case False
hence "x ≠ ma" by simp
hence 2:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 4 +(
if x < mi then 1 else 1+ (
if x > ma then 1 else 9 +
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then 1 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! h) l
else 1))))"
using 1 by simp
then show ?thesis
proof(cases "x < mi")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 5" using 2 by auto
then show ?thesis by simp
next
case False
hence "x > mi"
using ‹x ≠ mi› antisym_conv3 by blast
hence 3:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 5 + (
if x > ma then 1 else 9 +
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList then 1 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! h) l else 1)))"
using 2 by simp
then show ?thesis
proof(cases "x > ma")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 6" using 3 by simp
then show ?thesis by simp
next
case False
hence "x < ma"
by (meson ‹x ≠ ma› nat_neq_iff)
hence 4:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 14+
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then 1 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! h) l
else 1))"
using 3 by simp
let ?h = "high x (deg div 2)"
let ?l = " low x (deg div 2)"
have "?h < length treeList"
using "5"(10,4) "5.hyps"(4) ‹deg = Suc (Suc (Suc (n' + n')))› ‹n = Suc n'› ‹x < ma› high_bound_aux by auto
hence 5:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x = 15 + T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! ?h) ?l"
using "4" by presburger
moreover have "invar_vebt (treeList ! ?h) n ∧ (treeList ! ?h) ∈ set treeList "
using "5.IH"(1) ‹high x (deg div 2) < length treeList› nth_mem by blast
moreover hence " T⇩m⇩e⇩m⇩b⇩e⇩r (treeList ! ?h) ?l ≤ (1 + height (treeList ! ?h))*15" using "5.IH"(1) by simp
ultimately have 6:"T⇩m⇩e⇩m⇩b⇩e⇩r (Node (Some (mi, ma)) deg treeList summary) x ≤
15 + 15 * (1 + height (treeList ! ?h))"
by simp
moreover have "i< length treeList ⟹
height (treeList ! i) ≤ Max (height ` (insert summary (set treeList)))" for i
apply (induction treeList arbitrary: i)
apply simp
apply (meson List.finite_set Max_ge finite_imageI finite_insert image_iff nth_mem subsetD subset_insertI)
done
moreover hence " (1 + height (treeList ! ?h)) ≤ height (Node (Some (mi, ma)) deg treeList summary)"
by (simp add: ‹high x (deg div 2) < length treeList›)
moreover hence " 15 * (1 + height (treeList ! ?h)) ≤ 15 * height (Node (Some (mi, ma)) deg treeList summary)" by simp
ultimately show ?thesis
using 6 by simp
qed
qed
qed
qed
qed
theorem member_bound_height': "invar_vebt t n ⟹ T⇩m⇩e⇩m⇩b⇩e⇩r' t x ≤ (1+height t)"
proof(induction t n arbitrary: x rule: invar_vebt.induct)
case (4 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis deg_not_0 less_imp_Suc_add)
then have "deg = Suc (Suc (n' + n'))"
using 4 by linarith
then have "deg ≥ 2"
by linarith
have "n ≥ 1 ∧ m ≥ 1"
using 4 ‹n = Suc n'› by linarith
show ?case
proof(cases "x = mi")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1"
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis by simp
next
case False
hence "x ≠ mi" by simp
hence 1:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1 + (
if x = ma then 0 else (
if x < mi then 0 else (
if x > ma then 0 else
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! h) l
else 0)))))"
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis
proof(cases "x = ma")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1" using 1 by auto
then show ?thesis by simp
next
case False
hence "x ≠ ma" by simp
hence 2:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1 +(
if x < mi then 0 else (
if x > ma then 0 else
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! h) l
else 0))))"
using 1 by simp
then show ?thesis
proof(cases "x < mi")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1" using 2 by auto
then show ?thesis by simp
next
case False
hence "x > mi"
using ‹x ≠ mi› antisym_conv3 by blast
hence 3:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1 + (
if x > ma then 0 else
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! h) l
else 0)))"
using 2 by simp
then show ?thesis
proof(cases "x > ma")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1" using 3 by simp
then show ?thesis by simp
next
case False
hence "x < ma"
by (meson ‹x ≠ ma› nat_neq_iff)
hence 4:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1+
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! h) l
else 0))"
using 3 by simp
let ?h = "high x (deg div 2)"
let ?l = " low x (deg div 2)"
have "?h < length treeList"
using "4.hyps"(2) "4.hyps"(3) "4.hyps"(4) "4.hyps"(8) ‹x < ma› high_bound_aux by force
hence 5:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! ?h) ?l"
using "4" by presburger
moreover have "invar_vebt (treeList ! ?h) n ∧ (treeList ! ?h) ∈ set treeList "
using "4.IH"(1) ‹high x (deg div 2) < length treeList› nth_mem by blast
moreover hence " T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! ?h) ?l ≤ (1 + height (treeList ! ?h))*1" using "4.IH"(1) by simp
ultimately have 6:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x ≤
1 + (1 + height (treeList ! ?h))" by simp
moreover have "i< length treeList ⟹
height (treeList ! i) ≤ Max (height ` (insert summary (set treeList)))" for i
apply (induction treeList arbitrary: i)
apply simp
apply (meson List.finite_set Max_ge finite_imageI finite_insert image_iff nth_mem subsetD subset_insertI)
done
moreover hence " (1 + height (treeList ! ?h)) ≤ height (Node (Some (mi, ma)) deg treeList summary)"
by (simp add: ‹high x (deg div 2) < length treeList›)
moreover hence " 14 * (1 + height (treeList ! ?h)) ≤ 14 * height (Node (Some (mi, ma)) deg treeList summary)" by simp
ultimately show ?thesis
using 6 by presburger
qed
qed
qed
qed
next
case (5 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis nat_le_iff_add plus_1_eq_Suc set_n_deg_not_0)
then have "deg = Suc (Suc (Suc (n' + n')))"
using 5 by linarith
then have "deg ≥ 2"
by linarith
have "n ≥ 1 ∧ m ≥ 1"
using 5 ‹n = Suc n'› by linarith
show ?case
proof(cases "x = mi")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1"
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis by simp
next
case False
hence "x ≠ mi" by simp
hence 1:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1 + (
if x = ma then 0 else (
if x < mi then 0 else (
if x > ma then 0 else
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! h) l
else 0)))))"
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis
proof(cases "x = ma")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1" using 1 by auto
then show ?thesis by simp
next
case False
hence "x ≠ ma" by simp
hence 2:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1 +(
if x < mi then 0 else (
if x > ma then 0 else
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! h) l
else 0))))"
using 1 by simp
then show ?thesis
proof(cases "x < mi")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1" using 2 by auto
then show ?thesis by simp
next
case False
hence "x > mi"
using ‹x ≠ mi› antisym_conv3 by blast
hence 3:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1 + (
if x > ma then 0 else
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! h) l
else 0)))"
using 2 by simp
then show ?thesis
proof(cases "x > ma")
case True
hence "T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1" using 3 by simp
then show ?thesis by simp
next
case False
hence "x < ma"
by (meson ‹x ≠ ma› nat_neq_iff)
hence 4:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1+
(let h = high x (deg div 2); l = low x (deg div 2) in
(if h < length treeList
then T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! h) l
else 0))"
using 3 by simp
let ?h = "high x (deg div 2)"
let ?l = " low x (deg div 2)"
have "?h < length treeList"
using "5.hyps"(2) "5.hyps"(3) "5.hyps"(4) "5.hyps"(8) ‹x < ma› high_bound_aux
by (metis add_Suc_right add_self_div_2 even_Suc_div_two odd_add order.strict_trans)
hence 5:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! ?h) ?l"
using "4" by presburger
moreover have "invar_vebt (treeList ! ?h) n ∧ (treeList ! ?h) ∈ set treeList "
using "5.IH"(1) ‹high x (deg div 2) < length treeList› nth_mem by blast
moreover hence " T⇩m⇩e⇩m⇩b⇩e⇩r' (treeList ! ?h) ?l ≤ (1 + height (treeList ! ?h))*1" using "5.IH"(1) by simp
ultimately have 6:"T⇩m⇩e⇩m⇩b⇩e⇩r' (Node (Some (mi, ma)) deg treeList summary) x ≤
1 + (1 + height (treeList ! ?h))" by simp
moreover have "i< length treeList ⟹
height (treeList ! i) ≤ Max (height ` (insert summary (set treeList)))" for i
apply (induction treeList arbitrary: i)
apply simp
apply (meson List.finite_set Max_ge finite_imageI finite_insert image_iff nth_mem subsetD subset_insertI)
done
moreover hence " (1 + height (treeList ! ?h)) ≤ height (Node (Some (mi, ma)) deg treeList summary)"
by (simp add: ‹high x (deg div 2) < length treeList›)
moreover hence " 14 * (1 + height (treeList ! ?h)) ≤ 14 * height (Node (Some (mi, ma)) deg treeList summary)" by simp
ultimately show ?thesis
using 6 by presburger
qed
qed
qed
qed
qed simp+
theorem member_bound_size_univ: "invar_vebt t n ⟹ u = 2^n ⟹ T⇩m⇩e⇩m⇩b⇩e⇩r t x ≤ 30 + 15 * lb (lb u)"
using member_bound_height[of t n x] height_double_log_univ_size[of u n t] algebra_simps by simp
subsection ‹Minimum, Maximum, Emptiness Test›
fun T⇩m⇩i⇩n⇩t::"VEBT ⇒ nat" where
"T⇩m⇩i⇩n⇩t (Leaf a b) = (1+ (if a then 0 else 1 + (if b then 1 else 1)))"|
"T⇩m⇩i⇩n⇩t (Node None _ _ _) = 1"|
"T⇩m⇩i⇩n⇩t (Node (Some (mi,ma)) _ _ _ ) = 1"
lemma mint_bound: "T⇩m⇩i⇩n⇩t t ≤ 3" by (induction t rule: T⇩m⇩i⇩n⇩t.induct) auto
fun T⇩m⇩a⇩x⇩t::"VEBT ⇒ nat" where
"T⇩m⇩a⇩x⇩t (Leaf a b) = (1+ (if b then 1 else 1 +( if a then 1 else 1)))"|
"T⇩m⇩a⇩x⇩t (Node None _ _ _) = 1"|
"T⇩m⇩a⇩x⇩t (Node (Some (mi,ma)) _ _ _ ) = 1"
lemma maxt_bound: "T⇩m⇩a⇩x⇩t t ≤ 3" by (induction t rule: T⇩m⇩a⇩x⇩t.induct) auto
fun T⇩m⇩i⇩n⇩N⇩u⇩l⇩l::"VEBT ⇒ nat" where
"T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (Leaf False False) = 1"|
"T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (Leaf _ _ ) = 1"|
"T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (Node None _ _ _) = 1"|
"T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (Node (Some _) _ _ _) = 1"
lemma minNull_bound: "T⇩m⇩i⇩n⇩N⇩u⇩l⇩l t ≤ 1"
by (metis T⇩m⇩i⇩n⇩N⇩u⇩l⇩l.elims order_refl)
subsection ‹Insertion›
fun T⇩i⇩n⇩s⇩e⇩r⇩t::"VEBT ⇒ nat ⇒nat" where
"T⇩i⇩n⇩s⇩e⇩r⇩t (Leaf a b) x = 1+ (if x=0 then 1 else 1 + (if x=1 then 1 else 1))"|
"T⇩i⇩n⇩s⇩e⇩r⇩t (Node info 0 ts s) x = 1"|
"T⇩i⇩n⇩s⇩e⇩r⇩t (Node info (Suc 0) ts s) x = 1"|
"T⇩i⇩n⇩s⇩e⇩r⇩t (Node None (Suc deg) treeList summary) x = 2"|
"T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 19+
( let xn = (if x < mi then mi else x); minn = (if x< mi then x else mi);
l= low xn (deg div 2); h = high xn (deg div 2)
in
( if h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! h) l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! h)+
(if minNull (treeList ! h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary h else 1)
else 1))"
fun T⇩i⇩n⇩s⇩e⇩r⇩t'::"VEBT ⇒ nat ⇒nat" where
"T⇩i⇩n⇩s⇩e⇩r⇩t' (Leaf a b) x = 1"|
"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node info 0 ts s) x = 1"|
"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node info (Suc 0) ts s) x = 1"|
"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node None (Suc deg) treeList summary) x = 1"|
"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
(let xn = (if x < mi then mi else x); minn = (if x< mi then x else mi);
l= low xn (deg div 2); h = high xn (deg div 2)
in ( if h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! h) l +
(if minNull (treeList ! h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary h else 1) else 1))"
lemma insersimp:assumes "invar_vebt t n" and "∄ x. both_member_options t x " shows "T⇩i⇩n⇩s⇩e⇩r⇩t t y ≤ 3"
proof-
from assms(1) show ?thesis
proof(cases)
case (1 a b)
then show ?thesis by simp
next
case (2 treeList n summary m)
hence "n+m ≥ 2"
by (metis add_self_div_2 deg_not_0 div_greater_zero_iff)
then show ?thesis using T⇩i⇩n⇩s⇩e⇩r⇩t.simps(4)[of "n+m-2" treeList summary y]
by (metis "2"(1) "2"(6) add.commute add_2_eq_Suc le_add2 numeral_3_eq_3 ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
next
case (3 treeList n summary m)
hence "n+m ≥ 2"
by (metis add_mono_thms_linordered_semiring(1) le_add1 nat_1_add_1 plus_1_eq_Suc set_n_deg_not_0)
then show ?thesis using T⇩i⇩n⇩s⇩e⇩r⇩t.simps(4)[of "n+m-2" treeList summary y]
by (metis "3"(1) "3"(6) add.commute add_2_eq_Suc le_add2 numeral_3_eq_3 ordered_cancel_comm_monoid_diff_class.add_diff_inverse)
next
case (4 treeList n summary m mi ma)
hence "membermima (Node (Some (mi, ma)) (n+m) treeList summary) mi "
by (metis Suc_pred assms(1) deg_not_0 membermima.simps(4))
hence False
using "4"(1) "4"(6) assms(2) both_member_options_def by blast
then show ?thesis by simp
next
case (5 treeList n summary m mi ma)
hence "membermima (Node (Some (mi, ma)) (n+m) treeList summary) mi "
by (metis Suc_pred assms(1) deg_not_0 membermima.simps(4))
hence False
using "5"(1) "5"(6) assms(2) both_member_options_def by blast
then show ?thesis by simp
qed
qed
lemma insertsimp: "invar_vebt t n ⟹ minNull t ⟹ T⇩i⇩n⇩s⇩e⇩r⇩t t l ≤ 3"
using insersimp min_Null_member valid_member_both_member_options by blast
lemma insersimp':assumes "invar_vebt t n" and "∄ x. both_member_options t x " shows "T⇩i⇩n⇩s⇩e⇩r⇩t' t y ≤ 1"
using assms(1)
proof (cases rule: invar_vebt.cases)
case (1 a b)
then show ?thesis by simp
next
case (2 treeList k summary m)
then obtain k' :: nat where "k = Suc k'"
by (metis Suc_lessE Suc_lessI deg_not_0)
then show ?thesis
using 2 by simp
next
case (3 treeList k summary m)
then obtain k' :: nat where "k = Suc k'"
by (metis Suc_1 lessI list_decode.cases nth_mem power_Suc0_right valid_tree_deg_neq_0)
then show ?thesis
using 3 by simp
next
case (4 treeList k summary m mi ma)
then obtain k' :: nat where "k = Suc k'"
by (metis list_decode.cases valid_tree_deg_neq_0)
then show ?thesis
using 4 assms(2) not_min_Null_member by simp
next
case (5 treeList k summary m mi ma)
then obtain k' :: nat where "k = Suc k'"
by (metis add.right_neutral add_Suc_right nth_mem old.nat.exhaust valid_0_not)
then show ?thesis
using 5 assms(2) not_min_Null_member by simp
qed
lemma insertsimp': "invar_vebt t n ⟹ minNull t ⟹ T⇩i⇩n⇩s⇩e⇩r⇩t' t l ≤ 1"
using insersimp' min_Null_member valid_member_both_member_options by blast
theorem insert_bound_height: "invar_vebt t n ⟹ T⇩i⇩n⇩s⇩e⇩r⇩t t x ≤ (1+height t)*23"
proof(induction t n arbitrary: x rule: invar_vebt.induct)
case (1 a b)
then show ?case
using T⇩i⇩n⇩s⇩e⇩r⇩t.simps(1)[of a b x] height.simps(1)[of a b] by simp+
next
case (2 treeList n summary m deg)
hence "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
moreover have "height (Node None deg treeList summary) ≥ 1" using height.simps(2)[of None deg treeList summary]
by simp
ultimately show ?case
by simp
next
case (3 treeList n summary m deg)
hence "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' :: nat where "deg = Suc (Suc deg')"
using add_2_eq_Suc le_Suc_ex by blast
moreover have "height (Node None deg treeList summary) ≥ 1" using height.simps(2)[of None deg treeList summary] by simp
ultimately 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)
then obtain deg' :: nat where "deg = Suc (Suc deg')"
using add_2_eq_Suc le_Suc_ex by blast
let ?xn = "(if x < mi then mi else x)"
let ?minn = "(if x< mi then x else mi)"
let ?l= "low ?xn (deg div 2)"
let ?h = "high ?xn (deg div 2)"
show ?case
proof(cases "x < mi")
case True
hence 0:"T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 19+
( if ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1) else 1)"
by (simp add: ‹deg = Suc (Suc deg')› Let_def)
then show ?thesis
proof(cases " ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)")
case True
hence 1: "T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 19+
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using 0 by simp
then show ?thesis
proof(cases " minNull (treeList ! ?h)")
case True
hence " T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l ≤ 3"
using "4.IH"(1) ‹?h < length treeList ∧ _›
by (simp add: insertsimp[of _ n])
hence 2: "T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x ≤ 22 +
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using 1 by linarith
also have "… ≤ 23 + (if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using minNull_bound by force
also have "… ≤ 23 + T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h"
using True by simp
also have "… ≤ 23 + (height summary +1)*23"
using "4.IH"(2)[of ?h] by presburger
also have "… = ((1+ height summary)+1 )*23"
by presburger
also have "… ≤ (1 + height (Node (Some (mi, ma)) deg treeList summary)) * 23"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis .
next
case False
hence 2:"T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 20+
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)" using 1 by simp
also have "… ≤ 23 + T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l"
using minNull_bound[of "treeList ! ?h"] by linarith
also have "… ≤ 23 + (1 + height (treeList ! ?h)) * 23"
using "4.IH"(1) True by simp
also have "… ≤ ((1 + height (treeList!?h)) + 1) * 23"
by simp
also have "… ≤ (1 + height (Node (Some (mi, ma)) deg treeList summary)) * 23"
using height_compose_child[of "treeList!?h" treeList "Some (mi, ma)" deg summary]
by (metis Suc_eq_plus1 True mult_le_mono1 nat_add_left_cancel_le nth_mem plus_1_eq_Suc)
finally show ?thesis .
qed
next
case False
then show ?thesis
using True
by (auto simp add: ‹deg = Suc (Suc _)›)
qed
next
case False
hence 0:"T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 19+
( if ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1) else 1)"
by (simp add: ‹deg = Suc (Suc _)› Let_def)
then show ?thesis
proof(cases " ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)")
case True
hence 1: "T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 19+
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using 0 by simp
then show ?thesis
proof(cases " minNull (treeList ! ?h)")
case True
hence " T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l ≤ 3"
using "4.IH"(1) ‹?h < length treeList ∧ _›
by (simp add: insertsimp[of _ n])
hence 2: "T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x ≤ 22 +
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using 1 by simp
also have "… ≤ 23 + (if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using minNull_bound by force
also have "… ≤ 23 + T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h"
using True by simp
also have "… ≤ 23 + (height summary + 1) * 23"
using "4.IH"(2) by simp
also have "… ≤ ((1 + height summary) + 1 ) * 23"
by simp
also have "… ≤ (1 + height (Node (Some (mi, ma)) deg treeList summary)) * 23"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis .
next
case False
hence 2:"T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 20+
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)" using 1 by simp
also have "… ≤ 23 + T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l"
using minNull_bound[of "treeList ! ?h"] by linarith
also have "… ≤ 23 + (1 + height (treeList ! ?h)) * 23"
using "4.IH"(1) True by simp
also have "… ≤ ((1 + height (treeList!?h)) + 1) * 23"
by simp
also have "… ≤ (1 + height (Node (Some (mi, ma)) deg treeList summary)) * 23"
using height_compose_child[of "treeList!?h" treeList "Some (mi, ma)" deg summary]
by (metis Suc_eq_plus1 True mult_le_mono1 nat_add_left_cancel_le nth_mem plus_1_eq_Suc)
finally show ?thesis .
qed
next
case False
then show ?thesis
using "0" by force
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 Suc_eq_plus1 less_natE not_gr0 nth_mem valid_0_not)
then have "deg = Suc (Suc (Suc (n' + n')))"
unfolding ‹deg = n + m› ‹m = Suc n› by presburger
then have "2 ≤ deg"
by linarith
let ?xn = "(if x < mi then mi else x)"
let ?minn = "(if x< mi then x else mi)"
let ?l= "low ?xn (deg div 2)"
let ?h = "high ?xn (deg div 2)"
show ?case
proof(cases "x < mi")
case True
hence 0:"T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 19+
( if ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1) else 1)"
by (simp add: ‹deg = Suc (Suc _)› Let_def)
show ?thesis
proof(cases " ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)")
case True
hence 1: "T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 19+
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using 0 by simp
then show ?thesis
proof(cases " minNull (treeList ! ?h)")
case True
hence " T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l ≤ 3"
using "5.IH"(1) ‹?h < length treeList ∧ _›
by (simp add: insertsimp[of _ n])
hence 2: "T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x ≤ 22 +
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using 1 by linarith
also have "… ≤ 23 + (if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using minNull_bound[of "treeList ! ?h"] by linarith
also have "… ≤ 23 + T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h"
using True by simp
also have "… ≤ 23 + (height summary + 1) * 23"
using "5.IH"(2) by simp
also have "… ≤ ((1 + height summary) + 1) *23"
by simp
also have "… ≤ (1 + height (Node (Some (mi, ma)) deg treeList summary)) * 23"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis .
next
case False
hence 2:"T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 20+
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)" using 1 by simp
also have "… ≤ 23 + T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l"
using minNull_bound[of "treeList ! ?h"] by linarith
also have "… ≤ 23 + (1 + height (treeList ! ?h)) * 23"
using "5.IH"(1) True by simp
also have "… ≤ ((1 + height (treeList!?h)) + 1) * 23"
by simp
also have "… ≤ (1 + height (Node (Some (mi, ma)) deg treeList summary)) * 23"
using height_compose_child[of "treeList!?h" treeList "Some (mi, ma)" deg summary]
by (metis Suc_eq_plus1 True mult_le_mono1 nat_add_left_cancel_le nth_mem plus_1_eq_Suc)
finally show ?thesis .
qed
next
case False
then show ?thesis
using 0 by presburger
qed
next
case False
hence 0:"T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 19+
( if ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1) else 1)"
by (simp add: ‹deg = Suc (Suc _)› Let_def)
show ?thesis
proof(cases " ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)")
case True
hence 1: "T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 19+
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using 0 by simp
then show ?thesis
proof(cases " minNull (treeList ! ?h)")
case True
hence " T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l ≤ 3"
using "5.IH"(1) ‹?h < length treeList ∧ _›
by (simp add: insertsimp[of _ n])
hence 2: "T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x ≤ 22 +
T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)+(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using 1 by linarith
also have "… ≤ 23 + (if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h else 1)"
using minNull_bound[of "treeList ! ?h"] by linarith
also have "… ≤ 23 + T⇩i⇩n⇩s⇩e⇩r⇩t summary ?h"
using True by simp
also have "… ≤ 23 + (height summary + 1) * 23"
using "5.IH"(2) by simp
also have "… ≤ ((1 + height summary) + 1) * 23"
by simp
also have "… ≤ (1 + height (Node (Some (mi, ma)) deg treeList summary)) * 23"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis .
next
case False
hence 2:"T⇩i⇩n⇩s⇩e⇩r⇩t (Node (Some (mi,ma)) deg treeList summary) x = 20+
T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l + T⇩m⇩i⇩n⇩N⇩u⇩l⇩l (treeList ! ?h)" using 1 by simp
also have "… ≤ 23 + T⇩i⇩n⇩s⇩e⇩r⇩t (treeList ! ?h) ?l"
using minNull_bound[of "treeList ! ?h"] by linarith
also have "… ≤ 23 + (1 + height (treeList ! ?h)) * 23"
using "5.IH"(1) True by simp
also have "… ≤ ((1 + height (treeList!?h)) + 1) * 23"
by simp
also have "… ≤ (1 + height (Node (Some (mi, ma)) deg treeList summary)) * 23"
using True by simp
finally show ?thesis .
qed
next
case False
then show ?thesis
using "0" by force
qed
qed
qed
theorem insert_bound_size_univ: "invar_vebt t n ⟹ u = 2^n ⟹ T⇩i⇩n⇩s⇩e⇩r⇩t t x ≤ 46 + 23 * lb (lb u)"
using insert_bound_height[of t n x] height_double_log_univ_size[of u n t] algebra_simps by simp
theorem insert'_bound_height: "invar_vebt t n ⟹ T⇩i⇩n⇩s⇩e⇩r⇩t' t x ≤ (1+height t)"
proof(induction t n arbitrary: x rule: invar_vebt.induct )
case (2 treeList n summary m deg)
show ?case
proof (cases "deg ≥ 2")
case True
then obtain deg' :: nat where "deg = Suc (Suc deg')"
using add_2_eq_Suc le_Suc_ex by blast
then show ?thesis
by simp
next
case False
then show ?thesis
using 2 by (metis add_self_div_2 deg_not_0 div_greater_zero_iff)
qed
next
case (3 treeList n summary m deg)
show ?case
proof (cases "deg ≥ 2")
case True
then obtain deg' :: nat where "deg = Suc (Suc deg')"
using add_2_eq_Suc le_Suc_ex by blast
then show ?thesis
by simp
next
case False
then show ?thesis
using 3 by (metis Suc_1 add_leD2 not_less_eq_eq set_n_deg_not_0)
qed
next
case (4 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis deg_not_0 less_natE)
then have "deg = Suc (Suc (n' + n'))"
using 4 by linarith
then have "deg ≥ 2"
by linarith
let ?xn = "(if x < mi then mi else x)"
let ?minn = "(if x< mi then x else mi)"
let ?l= "low ?xn (deg div 2)"
let ?h = "high ?xn (deg div 2)"
show ?case
proof(cases "x < mi")
case True
hence 0:"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
( if ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l + (if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1) else 1)"
by (simp add: ‹deg = Suc (Suc _)› Let_def)
then show ?thesis
proof(cases " ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)")
case True
hence 1: "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l +(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1)"
using 0 by simp
then show ?thesis
proof(cases " minNull (treeList ! ?h)")
case True
hence " T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l ≤ 1"
by (metis "0" "1" "4.IH"(1) insertsimp' nat_le_iff_add nth_mem)
hence 2: "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1)"
using 1 by linarith
also have "… ≤ 1 + T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h"
using True by simp
also have "… ≤ 1 + (height summary +1)"
using "4.IH"(2) by simp
finally show ?thesis
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by linarith
next
case False
hence 2:"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
1+ T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l " using 1 by simp
hence "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+ (1+ height (treeList ! ?h))"
using "4.IH"(1) True by force
moreover have " (treeList!?h) ∈ set treeList"
using True nth_mem by blast
ultimately show ?thesis using height_compose_child[of "treeList!?h" treeList "Some (mi, ma)" deg summary] algebra_simps
by (smt (verit, ccfv_SIG) Suc_leI add.right_neutral le_add1 le_imp_less_Suc mult_le_mono order_trans plus_1_eq_Suc)
qed
next
case False
then show ?thesis using "0" Suc_eq_plus1 le_add2 plus_1_eq_Suc by presburger
qed
next
case False
hence 0:"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
( if ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l + (if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1) else 1)"
by (simp add: ‹deg = Suc (Suc _)› Let_def)
then show ?thesis
proof(cases " ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)")
case True
hence 1: "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l +
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1)"
using 0 by simp
then show ?thesis
proof(cases " minNull (treeList ! ?h)")
case True
hence "T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l ≤ 1"
using "4.IH"(1) ‹?h < length treeList ∧ _› insertsimp'[of _ n] by simp
hence 2: "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1)"
using 1 by linarith
hence "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1 + T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h" using True by simp
then show ?thesis using height_compose_summary[of summary "Some (mi, ma)" deg treeList] algebra_simps
by (smt (verit) "1" "4.IH"(2) True ‹T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! high (if x < mi then mi else x) (deg div 2)) (low (if x < mi then mi else x) (deg div 2)) ≤ 1› add_mono order_trans)
next
case False
hence 2:"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x = 1+
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l" using 1 by simp
hence "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+ T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l "
using minNull_bound[of "treeList ! ?h"] by linarith
hence "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+ (1+ height (treeList ! ?h))"
by (meson "4.IH"(1) True nat_add_left_cancel_le nth_mem order_trans)
moreover have " (treeList!?h) ∈ set treeList"
using True nth_mem by blast
ultimately show ?thesis using height_compose_child[of "treeList!?h" treeList "Some (mi, ma)" deg summary] algebra_simps
by (smt (verit, ccfv_SIG) Suc_leI add.right_neutral le_add1 le_imp_less_Suc mult_le_mono order_trans plus_1_eq_Suc)
qed
next
case False
then show ?thesis
using "0" by force
qed
qed
next
case (5 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis add.right_neutral add_Suc_right nth_mem old.nat.exhaust valid_0_not)
then have "deg = Suc (Suc (Suc (n' + n')))"
using 5 by linarith
then have "deg ≥ 2"
by linarith
let ?xn = "(if x < mi then mi else x)"
let ?minn = "(if x< mi then x else mi)"
let ?l= "low ?xn (deg div 2)"
let ?h = "high ?xn (deg div 2)"
show ?case
proof(cases "x < mi")
case True
hence 0:"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
( if ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l +
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1)
else 1)"
by (simp add: ‹deg = Suc (Suc _)› Let_def)
then show ?thesis
proof(cases " ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)")
case True
hence 1: "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l + (if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1)"
using 0 by simp
then show ?thesis
proof(cases " minNull (treeList ! ?h)")
case True
hence " T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l ≤ 1"
by (metis "0" "1" "5.IH"(1) insertsimp' nat_le_iff_add nth_mem)
hence 2: "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1)"
using 1 by linarith
also have "… ≤ 1 + T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h"
using True by simp
also have "… ≤ 1 + (height summary +1)"
using "5.IH"(2) by simp
finally show ?thesis
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by linarith
next
case False
hence 2:"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
1+ T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l " using 1 by simp
hence "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+ (1+ height (treeList ! ?h))"
using "5.IH"(1) True by force
moreover have " (treeList!?h) ∈ set treeList"
using True nth_mem by blast
ultimately show ?thesis using height_compose_child[of "treeList!?h" treeList "Some (mi, ma)" deg summary] algebra_simps
by (smt (verit, ccfv_SIG) Suc_leI add.right_neutral le_add1 le_imp_less_Suc mult_le_mono order_trans plus_1_eq_Suc)
qed
next
case False
then show ?thesis using "0" Suc_eq_plus1 le_add2 plus_1_eq_Suc by presburger
qed
next
case False
hence 0:"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
( if ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)then
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l + (if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1) else 1)"
by (simp add: ‹deg = Suc (Suc _)› Let_def)
then show ?thesis
proof(cases " ?h < length treeList ∧ ¬ (x = mi ∨ x = ma)")
case True
hence 1: "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x =
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l + (if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1)"
using 0 by simp
then show ?thesis
proof(cases " minNull (treeList ! ?h)")
case True
hence " T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l ≤ 1"
by (smt (verit) "0" "1" "5.IH"(1) insertsimp' le_add1 nat_add_left_cancel_le nth_mem numeral_3_eq_3 order_trans plus_1_eq_Suc)
hence 2: "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+
(if minNull (treeList ! ?h) then T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h else 1)"
using 1 by linarith
hence "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1 + T⇩i⇩n⇩s⇩e⇩r⇩t' summary ?h"
using True by simp
then show ?thesis
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] algebra_simps
by (smt (verit) "1" "5.IH"(2) True ‹T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! high (if x < mi then mi else x) (deg div 2)) (low (if x < mi then mi else x) (deg div 2)) ≤ 1› add_mono order_trans)
next
case False
hence 2:"T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x = 1+
T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l" using 1 by simp
hence "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+ T⇩i⇩n⇩s⇩e⇩r⇩t' (treeList ! ?h) ?l "
using minNull_bound[of "treeList ! ?h"] by linarith
hence "T⇩i⇩n⇩s⇩e⇩r⇩t' (Node (Some (mi,ma)) deg treeList summary) x ≤ 1+ (1+ height (treeList ! ?h))"
by (meson "5.IH"(1) True nat_add_left_cancel_le nth_mem order_trans)
moreover have " (treeList!?h) ∈ set treeList"
using True nth_mem by blast
ultimately show ?thesis using height_compose_child[of "treeList!?h" treeList "Some (mi, ma)" deg summary] algebra_simps
by (smt (verit, ccfv_SIG) Suc_leI add.right_neutral le_add1 le_imp_less_Suc mult_le_mono order_trans plus_1_eq_Suc)
qed
next
case False
then show ?thesis
using "0" by force
qed
qed
qed simp+
subsection ‹Successor Function›
fun T⇩s⇩u⇩c⇩c::"VEBT ⇒ nat ⇒ nat" where
"T⇩s⇩u⇩c⇩c (Leaf _ b) 0 = 1+ (if b then 1 else 1)"|
"T⇩s⇩u⇩c⇩c (Leaf _ _) (Suc n) = 1"|
"T⇩s⇩u⇩c⇩c (Node None _ _ _) _ = 1"|
"T⇩s⇩u⇩c⇩c (Node _ 0 _ _) _ = 1"|
"T⇩s⇩u⇩c⇩c (Node _ (Suc 0) _ _) _ = 1"|
"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x = 1+ (
if x < mi then 1
else (let l = low x (deg div 2); h = high x (deg div 2) in 10 +
(if h < length treeList then 1+ T⇩m⇩a⇩x⇩t (treeList ! h) + (
let maxlow = vebt_maxt (treeList ! h) in 3 +
(if maxlow ≠ None ∧ (Some l <⇩o maxlow) then
4 + T⇩s⇩u⇩c⇩c (treeList ! h) l
else let sc = vebt_succ summary h in 1+ T⇩s⇩u⇩c⇩c summary h + 1 + (
if sc = None then 1
else (4 + T⇩m⇩i⇩n⇩t (treeList ! the sc) ))))
else 1)))"
fun T⇩s⇩u⇩c⇩c'::"VEBT ⇒ nat ⇒ nat" where
"T⇩s⇩u⇩c⇩c' (Leaf _ b) 0 = 1"|
"T⇩s⇩u⇩c⇩c' (Leaf _ _) (Suc n) = 1"|
"T⇩s⇩u⇩c⇩c' (Node None _ _ _) _ = 1"|
"T⇩s⇩u⇩c⇩c' (Node _ 0 _ _) _ = 1"|
"T⇩s⇩u⇩c⇩c' (Node _ (Suc 0) _ _) _ = 1"|
"T⇩s⇩u⇩c⇩c' (Node (Some (mi, ma)) deg treeList summary) x =(
if x < mi then 1
else (let l = low x (deg div 2); h = high x (deg div 2) in
(if h < length treeList then (
let maxlow = vebt_maxt (treeList ! h) in
(if maxlow ≠ None ∧ (Some l <⇩o maxlow) then
1+ T⇩s⇩u⇩c⇩c' (treeList ! h) l
else let sc = vebt_succ summary h in T⇩s⇩u⇩c⇩c' summary h + (
if sc = None then 1
else 1 )))
else 1)))"
theorem succ_bound_height: "invar_vebt t n ⟹ T⇩s⇩u⇩c⇩c t x ≤ (1+height t)*27"
proof(induction t n arbitrary: x rule: invar_vebt.induct)
case (1 a b)
then show ?case using T⇩s⇩u⇩c⇩c.simps(1)[of a b]
proof -
have "∀b v ba n. T⇩s⇩u⇩c⇩c v n = 1 ∨ Leaf b ba ≠ v ∨ 0 = n"
using T⇩s⇩u⇩c⇩c.elims by blast
then show ?thesis
by (metis (no_types) Nat.add_0_right ‹T⇩s⇩u⇩c⇩c (Leaf a b) 0 = 1 + (if b then 1 else 1)› height.simps(1) nat_mult_1 numeral_le_iff one_add_one one_le_numeral semiring_norm(68) semiring_norm(72))
qed
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)
then obtain n' :: nat where "n = Suc n'"
by (metis deg_not_0 less_imp_Suc_add)
then have "deg = Suc (Suc (n' + n'))"
unfolding ‹deg = n + m› ‹m = n› by presburger
then show ?case
proof(cases "x < mi")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
show ?thesis
proof(cases "?h < length treeList")
case True
hence "?h < length treeList" by simp
hence 0:"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =12 + T⇩m⇩a⇩x⇩t (treeList ! ?h) + (
let maxlow = vebt_maxt (treeList ! ?h) in 3 +
(if maxlow ≠ None ∧ (Some ?l <⇩o maxlow) then
4 + T⇩s⇩u⇩c⇩c (treeList ! ?h) ?l
else let sc = vebt_succ summary ?h in 1+ T⇩s⇩u⇩c⇩c summary ?h + 1 + (
if sc = None then 1
else (4 + T⇩m⇩i⇩n⇩t (treeList ! the sc) ))))"
using False
by (simp add: ‹deg = Suc (Suc _)› Let_def)
let ?maxlow= "vebt_maxt (treeList ! ?h)"
let ?sc="vebt_succ summary ?h"
have 1:"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =15 + T⇩m⇩a⇩x⇩t (treeList ! ?h) +
(if ?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow) then
4 + T⇩s⇩u⇩c⇩c (treeList ! ?h) ?l
else 2+ T⇩s⇩u⇩c⇩c summary ?h + (
if ?sc = None then 1
else (4 + T⇩m⇩i⇩n⇩t (treeList ! the ?sc))))" using 0 by auto
then show ?thesis
proof(cases " ?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow)")
case True
hence "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =
19 + T⇩m⇩a⇩x⇩t (treeList ! ?h) + T⇩s⇩u⇩c⇩c (treeList ! ?h) ?l"
using 1 by simp
hence "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x ≤
22 + T⇩s⇩u⇩c⇩c (treeList ! ?h) ?l" using maxt_bound[of "treeList ! ?h"]
by simp
moreover have a:"treeList ! ?h ∈ set treeList "
by (simp add: ‹high x (deg div 2) < length treeList›)
ultimately have "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x ≤
22 + (1+ height (treeList ! ?h))*27"
by (meson "4.IH"(1) nat_add_left_cancel_le order_trans)
hence "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x ≤
((1+ height (treeList ! ?h))+1)*27" by simp
then show ?thesis
using height_compose_child[of "treeList ! ?h" treeList "Some (mi, ma)" deg summary] a
by (smt (verit) Suc_leI add.commute dual_order.strict_trans2 le_imp_less_Suc linorder_not_less mult.commute mult_le_mono2 plus_1_eq_Suc)
next
case False
then have 2:"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =17 + T⇩m⇩a⇩x⇩t (treeList ! ?h) +
T⇩s⇩u⇩c⇩c summary ?h + (
if ?sc = None then 1
else (4 + T⇩m⇩i⇩n⇩t (treeList ! the ?sc)))"
using 1 by auto
then show ?thesis
proof(cases " ?sc = None")
case True
hence 3:"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =
18 + T⇩m⇩a⇩x⇩t (treeList ! ?h) + T⇩s⇩u⇩c⇩c summary ?h "
using 2 by simp
hence "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x ≤ 21 + T⇩s⇩u⇩c⇩c summary ?h"
using maxt_bound[of "treeList ! ?h"] by simp
also have "… ≤ 21 + (1 + height summary) * 27"
using "4.IH"(2) by simp
also have "… ≤ 21 + height (Node (Some (mi, ma)) deg treeList summary) * 27"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by presburger
next
case False
then have "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =
21 + T⇩m⇩a⇩x⇩t (treeList ! ?h) + T⇩s⇩u⇩c⇩c summary ?h + T⇩m⇩i⇩n⇩t (treeList ! the ?sc)"
using 2 by simp
also have "… ≤ 27 + T⇩s⇩u⇩c⇩c summary ?h"
using maxt_bound[of "treeList ! ?h"] mint_bound[of "treeList ! the ?sc"] by linarith
also have "… ≤ 27 + (1 + height summary) * 27"
using "4.IH"(2) by simp
also have "… ≤ ((1 + height summary) + 1) * 27"
by simp
also have "… ≤ (1 + height (Node (Some (mi, ma)) deg treeList summary)) * 27"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis .
qed
qed
next
case False
hence " T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x = 12"
using ‹¬ x < mi›
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis
by simp
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 Suc_eq_plus1 less_iff_Suc_add not_gr0 nth_mem valid_0_not)
then have "deg = Suc (Suc (Suc (n' + n')))"
unfolding ‹deg = n + m› ‹m = Suc n› by presburger
then have "deg ≥ 2"
by linarith
then show ?case
proof(cases "x < mi")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
show ?thesis
proof(cases "?h < length treeList")
case True
hence "?h < length treeList" by simp
hence 0:"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =12 + T⇩m⇩a⇩x⇩t (treeList ! ?h) + (
let maxlow = vebt_maxt (treeList ! ?h) in 3 +
(if maxlow ≠ None ∧ (Some ?l <⇩o maxlow) then
4 + T⇩s⇩u⇩c⇩c (treeList ! ?h) ?l
else let sc = vebt_succ summary ?h in 1+ T⇩s⇩u⇩c⇩c summary ?h + 1 + (
if sc = None then 1
else (4 + T⇩m⇩i⇩n⇩t (treeList ! the sc) ))))"
using False
by (simp add: ‹deg = Suc (Suc _)› Let_def)
let ?maxlow= "vebt_maxt (treeList ! ?h)"
let ?sc="vebt_succ summary ?h"
have 1:"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =15 + T⇩m⇩a⇩x⇩t (treeList ! ?h) +
(if ?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow) then
4 + T⇩s⇩u⇩c⇩c (treeList ! ?h) ?l
else 2+ T⇩s⇩u⇩c⇩c summary ?h + (
if ?sc = None then 1
else (4 + T⇩m⇩i⇩n⇩t (treeList ! the ?sc))))"
by (simp add: 0 Let_def)
then show ?thesis
proof(cases " ?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow)")
case True
hence "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =
19 + T⇩m⇩a⇩x⇩t (treeList ! ?h) + T⇩s⇩u⇩c⇩c (treeList ! ?h) ?l" using 1 by simp
hence "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x ≤
22 + T⇩s⇩u⇩c⇩c (treeList ! ?h) ?l" using maxt_bound[of "treeList ! ?h"] by simp
moreover have a:"treeList ! ?h ∈ set treeList "
by (simp add: ‹high x (deg div 2) < length treeList›)
ultimately have "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x ≤
22 + (1+ height (treeList ! ?h))*27"
by (meson "5.IH"(1) nat_add_left_cancel_le order_trans)
hence "T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x ≤
((1+ height (treeList ! ?h))+1)*27" by simp
then show ?thesis using height_compose_child[of "treeList ! ?h" treeList "Some (mi, ma)" deg summary] a
by (smt (verit) Suc_leI add.commute dual_order.strict_trans2 le_imp_less_Suc linorder_not_less mult.commute mult_le_mono2 plus_1_eq_Suc)
next
case False
then have 2:"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =17 + T⇩m⇩a⇩x⇩t (treeList ! ?h) +
T⇩s⇩u⇩c⇩c summary ?h + (
if ?sc = None then 1
else (4 + T⇩m⇩i⇩n⇩t (treeList ! the ?sc)))"
using 1 by auto
then show ?thesis
proof(cases " ?sc = None")
case True
hence 3:"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =18 + T⇩m⇩a⇩x⇩t (treeList ! ?h) +
T⇩s⇩u⇩c⇩c summary ?h " using 2 by simp
also have "… ≤ 21 + T⇩s⇩u⇩c⇩c summary ?h"
using maxt_bound[of "treeList ! ?h"] by simp
also have "… ≤ 21 + (1 + height summary) * 27"
using "5.IH"(2) by simp
also have "… ≤ 21 + height (Node (Some (mi, ma)) deg treeList summary) * 27"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by presburger
next
case False
hence 3:"T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x =21 + T⇩m⇩a⇩x⇩t (treeList ! ?h) +
T⇩s⇩u⇩c⇩c summary ?h + T⇩m⇩i⇩n⇩t (treeList ! the ?sc)" using 2 by simp
also have "… ≤ 27 + T⇩s⇩u⇩c⇩c summary ?h"
using maxt_bound[of "treeList ! ?h"] mint_bound[of "treeList ! the ?sc"] by simp
also have "… ≤ 27 + (1 + height summary) * 27"
using "5.IH"(2) by simp
also have "… ≤ ((1 + height summary) + 1) * 27"
by simp
also have "… ≤ (height (Node (Some (mi, ma)) deg treeList summary) + 1) * 27"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by presburger
qed
qed
next
case False
hence " T⇩s⇩u⇩c⇩c (Node (Some (mi, ma)) deg treeList summary) x = 12"
using ‹¬ x < mi›
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis
by auto
qed
qed
qed
theorem succ_bound_size_univ: "invar_vebt t n ⟹ u = 2^n ⟹ T⇩s⇩u⇩c⇩c t x ≤ 54 + 27 * lb (lb u)"
using succ_bound_height[of t n x] height_double_log_univ_size[of u n t] by simp
theorem succ'_bound_height: "invar_vebt t n ⟹ T⇩s⇩u⇩c⇩c' t x ≤ (1+height t)"
proof(induction t n arbitrary: x rule: invar_vebt.induct)
case (1 a b)
then show ?case
by (metis One_nat_def T⇩s⇩u⇩c⇩c'.simps(1) T⇩s⇩u⇩c⇩c'.simps(2) height.simps(1) le_add2 le_add_same_cancel2 le_neq_implies_less less_imp_Suc_add order_refl 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 less_imp_Suc_add)
then have "deg = Suc (Suc (n' + n'))"
unfolding ‹deg = n + m› ‹m = n› by presburger
hence degprop: "deg ≥ 2"
by linarith
then show ?case
proof(cases "x< mi")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
hence "x ≥ mi" by simp
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
show ?thesis
proof(cases "?h < length treeList")
case True
hence hprop: "?h < length treeList" by simp
let ?maxlow = "vebt_maxt (treeList ! ?h)"
show ?thesis
proof(cases " ?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow)")
case True
hence "T⇩s⇩u⇩c⇩c' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩s⇩u⇩c⇩c' (treeList ! ?h) ?l"
using ‹¬ x < mi› hprop
by (simp add: ‹deg = Suc (Suc _)›)
moreover have " (treeList ! ?h) ∈ set treeList"
using hprop nth_mem by blast
moreover have " T⇩s⇩u⇩c⇩c' (treeList ! ?h) ?l ≤ 1+ height (treeList ! ?h)" using 4(1) calculation by blast
ultimately have "T⇩s⇩u⇩c⇩c' (Node (Some (mi, ma)) deg treeList summary) x ≤ 1 + 1+ height (treeList ! ?h)" by simp
then show ?thesis
by (smt (verit) Suc_le_mono ‹T⇩s⇩u⇩c⇩c' (Node (Some (mi, ma)) deg treeList summary) x = 1 + T⇩s⇩u⇩c⇩c' (treeList ! high x (deg div 2)) (low x (deg div 2))› ‹T⇩s⇩u⇩c⇩c' (treeList ! high x (deg div 2)) (low x (deg div 2)) ≤ 1 + height (treeList ! high x (deg div 2))› ‹treeList ! high x (deg div 2) ∈ set treeList› height_compose_child le_trans plus_1_eq_Suc)
next
case False
hence "T⇩s⇩u⇩c⇩c' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩s⇩u⇩c⇩c' summary ?h"
using ‹mi ≤ x› hprop
by (auto simp add: ‹deg = Suc (Suc _)›)
moreover have " T⇩s⇩u⇩c⇩c' summary ?h ≤ 1+ height summary" using 4(2) calculation by blast
ultimately have "T⇩s⇩u⇩c⇩c' (Node (Some (mi, ma)) deg treeList summary) x ≤ 1 + 1+ height summary" by simp
then show ?thesis
by (simp add: le_trans)
qed
next
case False
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
qed
qed
next
case (5 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis add_0 less_natE not_gr0 nth_mem valid_0_not)
then have "deg = Suc (Suc (Suc (n' + n')))"
unfolding ‹deg = n + m› ‹m = Suc n› by presburger
hence degprop: "deg ≥ 2"
by linarith
show ?case
proof (cases "x< mi")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
hence "x ≥ mi" by simp
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
show ?thesis
proof(cases "?h < length treeList")
case True
hence hprop: "?h < length treeList" by simp
let ?maxlow = "vebt_maxt (treeList ! ?h)"
show ?thesis
proof(cases " ?maxlow ≠ None ∧ (Some ?l <⇩o ?maxlow)")
case True
have "T⇩s⇩u⇩c⇩c' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩s⇩u⇩c⇩c' (treeList ! ?h) ?l"
using ‹¬ x < mi› hprop True
by (simp add: ‹deg = Suc (Suc _)›)
also have "… ≤ 1 + 1+ height (treeList ! ?h)"
proof -
have "T⇩s⇩u⇩c⇩c' (treeList ! ?h) ?l ≤ 1 + height (treeList ! ?h)"
using "5.IH"(1) hprop nth_mem by blast
then show ?thesis
by linarith
qed
also have "… ≤ 1 + height (Node (Some (mi, ma)) deg treeList summary)"
by (simp add: hprop)
finally show ?thesis .
next
case False
hence "T⇩s⇩u⇩c⇩c' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩s⇩u⇩c⇩c' summary ?h"
using ‹mi ≤ x› hprop
by (auto simp add: ‹deg = Suc (Suc _)›)
moreover have " T⇩s⇩u⇩c⇩c' summary ?h ≤ 1+ height summary" using 5(2) calculation by blast
ultimately have "T⇩s⇩u⇩c⇩c' (Node (Some (mi, ma)) deg treeList summary) x ≤ 1 + 1+ height summary" by simp
then show ?thesis
by (simp add: le_trans)
qed
next
case False
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
qed
qed
qed simp+
theorem succ_bound_size_univ': "invar_vebt t n ⟹ u = 2^n ⟹ T⇩s⇩u⇩c⇩c' t x ≤ 2 + lb (lb u)"
using succ'_bound_height[of t n x] height_double_log_univ_size[of u n t] by simp
subsection ‹Predecessor Function›
fun T⇩p⇩r⇩e⇩d::"VEBT ⇒ nat ⇒ nat " where
"T⇩p⇩r⇩e⇩d (Leaf _ _) 0 = 1"|
"T⇩p⇩r⇩e⇩d (Leaf a _) (Suc 0) = 1+ (if a then 1 else 1)"|
"T⇩p⇩r⇩e⇩d (Leaf a b) _ = 1+ (if b then 1 else 1+ (if a then 1 else 1))"|
"T⇩p⇩r⇩e⇩d (Node None _ _ _) _ = 1"|
"T⇩p⇩r⇩e⇩d (Node _ 0 _ _) _ = 1"|
"T⇩p⇩r⇩e⇩d (Node _ (Suc 0) _ _) _ = 1"|
"T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x = 1+ (
if x > ma then 1
else (let l = low x (deg div 2); h = high x (deg div 2) in 10 + 1+
(if h < length treeList then
let minlow = vebt_mint (treeList ! h) in 2 + T⇩m⇩i⇩n⇩t(treeList ! h) + 3 +
(if minlow ≠ None ∧ (Some l >⇩o minlow) then
4 + T⇩p⇩r⇩e⇩d (treeList ! h) l
else let pr = vebt_pred summary h in 1 + T⇩p⇩r⇩e⇩d summary h+ 1 + (
if pr = None then 1 + (if x > mi then 1 else 1)
else 4 + T⇩m⇩a⇩x⇩t (treeList ! the pr) ))
else 1)))"
theorem pred_bound_height: "invar_vebt t n ⟹ T⇩p⇩r⇩e⇩d t x ≤ (1+height t)*29"
proof(induction t n arbitrary: x rule: invar_vebt.induct)
case (1 a b)
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)
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 > ma")
case True
hence " T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x =2"
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis by simp
next
case False
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
have 0: "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x = 1 + 10 +1 +
(if ?h < length treeList then
let minlow = vebt_mint (treeList ! ?h) in 2 + T⇩m⇩i⇩n⇩t(treeList ! ?h) + 3 +
(if minlow ≠ None ∧ (Some ?l >⇩o minlow) then
4 + T⇩p⇩r⇩e⇩d (treeList ! ?h) ?l
else let pr = vebt_pred summary ?h in 1 + T⇩p⇩r⇩e⇩d summary ?h+ 1 + (
if pr = None then 1 + (if x > mi then 1 else 1)
else 4 + T⇩m⇩a⇩x⇩t (treeList ! the pr) ))
else 1)"
using False by (simp add: ‹deg = Suc (Suc _)› Let_def)
then show ?thesis
proof(cases " ?h < length treeList")
case True
let ?minlow = "vebt_mint (treeList ! ?h)"
have 1: "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x =17 + T⇩m⇩i⇩n⇩t(treeList ! ?h) +
(if ?minlow ≠ None ∧ (Some ?l >⇩o ?minlow) then
4 + T⇩p⇩r⇩e⇩d (treeList ! ?h) ?l
else let pr = vebt_pred summary ?h in 1 + T⇩p⇩r⇩e⇩d summary ?h+ 1 + (
if pr = None then 1 + (if x > mi then 1 else 1)
else 4 + T⇩m⇩a⇩x⇩t (treeList ! the pr) ))" using True 0 by simp
then show ?thesis
proof(cases "?minlow ≠ None ∧ (Some ?l >⇩o ?minlow)")
case True
have 2: "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x =21 + T⇩m⇩i⇩n⇩t(treeList ! ?h) +
T⇩p⇩r⇩e⇩d (treeList ! ?h) ?l" using True 1 by simp
hence "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x ≤ 24 + T⇩p⇩r⇩e⇩d (treeList ! ?h) ?l" using mint_bound by simp
moreover hence "(treeList ! ?h) ∈ set treeList"
using "4.hyps"(2) "4.hyps"(3) "4.hyps"(4) "4.hyps"(8) False high_bound_aux by force
ultimately have "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x ≤ 24 + (1 + height(treeList ! ?h))*29"
using "4.IH" by (meson nat_add_left_cancel_le order_trans)
hence "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x ≤
24 + (height (Node (Some (mi, ma)) deg treeList summary))*29"
using height_compose_child[of "treeList ! ?h" treeList "Some(mi, ma)" deg summary]
by (meson ‹treeList ! high x (deg div 2) ∈ set treeList› add_le_cancel_left le_refl mult_le_mono order_trans)
then show ?thesis by simp
next
case False
let ?pr = "vebt_pred summary ?h "
have 2: "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x =19 + T⇩m⇩i⇩n⇩t(treeList ! ?h) +
T⇩p⇩r⇩e⇩d summary ?h+ (
if ?pr = None then 1 + (if x > mi then 1 else 1)
else 4 + T⇩m⇩a⇩x⇩t (treeList ! the ?pr))" using False 1 by auto
also have "… ≤22 +
T⇩p⇩r⇩e⇩d summary ?h+ (
if ?pr = None then 1 + (if x > mi then 1 else 1)
else 4 + T⇩m⇩a⇩x⇩t (treeList ! the ?pr))"
using mint_bound by simp
also have "… ≤ 29 + T⇩p⇩r⇩e⇩d summary ?h"
using maxt_bound by (cases " ?pr = None") auto
also have "… ≤ 29 + (1 + height summary) * 29"
using "4.IH"(2)[of ?h] by simp
also have "… ≤ 29 + (height (Node (Some (mi, ma)) deg treeList summary)) * 29"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by presburger
qed
next
case False
then show ?thesis using 0 by simp
qed
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)
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 > ma")
case True
hence " T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x =2"
by (simp add: ‹deg = Suc (Suc _)›)
then show ?thesis by simp
next
case False
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
have 0: "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x = 1 + 10 +1 +
(if ?h < length treeList then
let minlow = vebt_mint (treeList ! ?h) in 2 + T⇩m⇩i⇩n⇩t(treeList ! ?h) + 3 +
(if minlow ≠ None ∧ (Some ?l >⇩o minlow) then
4 + T⇩p⇩r⇩e⇩d (treeList ! ?h) ?l
else let pr = vebt_pred summary ?h in 1 + T⇩p⇩r⇩e⇩d summary ?h+ 1 + (
if pr = None then 1 + (if x > mi then 1 else 1)
else 4 + T⇩m⇩a⇩x⇩t (treeList ! the pr) ))
else 1)"
using False by (simp add: ‹deg = Suc (Suc _)› Let_def)
then show ?thesis
proof(cases " ?h < length treeList")
case True
hence " ?h < length treeList" by simp
let ?minlow = "vebt_mint (treeList ! ?h)"
have 1: "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x =17 + T⇩m⇩i⇩n⇩t(treeList ! ?h) +
(if ?minlow ≠ None ∧ (Some ?l >⇩o ?minlow) then
4 + T⇩p⇩r⇩e⇩d (treeList ! ?h) ?l
else let pr = vebt_pred summary ?h in 1 + T⇩p⇩r⇩e⇩d summary ?h+ 1 + (
if pr = None then 1 + (if x > mi then 1 else 1)
else 4 + T⇩m⇩a⇩x⇩t (treeList ! the pr) ))"
using True 0 by simp
then show ?thesis
proof(cases "?minlow ≠ None ∧ (Some ?l >⇩o ?minlow)")
case True
have 2: "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x =21 + T⇩m⇩i⇩n⇩t(treeList ! ?h) +
T⇩p⇩r⇩e⇩d (treeList ! ?h) ?l" using True 1 by simp
hence "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x ≤ 24 + T⇩p⇩r⇩e⇩d (treeList ! ?h) ?l" using mint_bound by simp
moreover hence "(treeList ! ?h) ∈ set treeList"
by (meson ‹high x (deg div 2) < length treeList› nth_mem)
ultimately have "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x ≤ 24 + (1 + height(treeList ! ?h))*29"
using "5.IH" by (meson nat_add_left_cancel_le order_trans)
hence "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x ≤
24 + (height (Node (Some (mi, ma)) deg treeList summary))*29"
using height_compose_child[of "treeList ! ?h" treeList "Some(mi, ma)" deg summary]
by (meson ‹treeList ! high x (deg div 2) ∈ set treeList› add_le_cancel_left le_refl mult_le_mono order_trans)
then show ?thesis by simp
next
case False
let ?pr = "vebt_pred summary ?h "
have 2: "T⇩p⇩r⇩e⇩d (Node (Some (mi, ma)) deg treeList summary) x =19 + T⇩m⇩i⇩n⇩t(treeList ! ?h) +
T⇩p⇩r⇩e⇩d summary ?h+ (
if ?pr = None then 1 + (if x > mi then 1 else 1)
else 4 + T⇩m⇩a⇩x⇩t (treeList ! the ?pr))"
using False 1 by auto
also have "… ≤ 22 +
T⇩p⇩r⇩e⇩d summary ?h+ (
if ?pr = None then 1 + (if x > mi then 1 else 1)
else 4 + T⇩m⇩a⇩x⇩t (treeList ! the ?pr))"
using mint_bound[of "treeList ! ?h"] by simp
also have "… ≤ 29 + T⇩p⇩r⇩e⇩d summary ?h"
using maxt_bound by (cases " ?pr = None") auto
also have "… ≤ 29 + (1 + height summary) * 29"
using "5.IH"(2)[of ?h] by simp
also have "… ≤ 29 + (height (Node (Some (mi, ma)) deg treeList summary)) * 29"
using height_compose_summary[of summary "Some (mi, ma)" deg treeList] by simp
finally show ?thesis
by presburger
qed
next
case False
then show ?thesis using 0 by simp
qed
qed
qed
theorem pred_bound_size_univ: "invar_vebt t n ⟹ u = 2^n ⟹ T⇩p⇩r⇩e⇩d t x ≤ 58 + 29 * lb (lb u)"
using pred_bound_height[of t n x] height_double_log_univ_size[of u n t] by simp
fun T⇩p⇩r⇩e⇩d'::"VEBT ⇒ nat ⇒ nat " where
"T⇩p⇩r⇩e⇩d' (Leaf _ _) 0 = 1"|
"T⇩p⇩r⇩e⇩d' (Leaf a _) (Suc 0) = 1"|
"T⇩p⇩r⇩e⇩d' (Leaf a b) _ = 1"|
"T⇩p⇩r⇩e⇩d' (Node None _ _ _) _ = 1"|
"T⇩p⇩r⇩e⇩d' (Node _ 0 _ _) _ = 1"|
"T⇩p⇩r⇩e⇩d' (Node _ (Suc 0) _ _) _ = 1"|
"T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x = (
if x > ma then 1
else (let l = low x (deg div 2); h = high x (deg div 2) in
(if h < length treeList then
let minlow = vebt_mint (treeList ! h) in
(if minlow ≠ None ∧ (Some l >⇩o minlow) then
1+ T⇩p⇩r⇩e⇩d' (treeList ! h) l
else let pr = vebt_pred summary h in T⇩p⇩r⇩e⇩d' summary h+ (
if pr = None then 1
else 1 ))
else 1)))"
theorem pred_bound_height': "invar_vebt t n⟹ T⇩p⇩r⇩e⇩d' t x ≤ (1 + height t)"
proof(induction t n arbitrary: x rule: invar_vebt.induct)
case (1 a b)
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 (4 treeList n summary m deg mi ma)
hence degprop:"deg ≥ 2"
by (metis add_self_div_2 deg_not_0 div_greater_zero_iff)
then obtain deg' where "deg = Suc (Suc deg')"
using add_2_eq_Suc le_Suc_ex by blast
show ?case
proof(cases "x > ma")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
hence "x ≤ ma" by simp
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
show ?thesis
proof(cases "?h< length treeList")
case True
hence hprop: "?h< length treeList" by simp
let ?minlow = "vebt_mint (treeList ! ?h)"
show ?thesis
proof(cases "?minlow ≠ None ∧ (Some ?l >⇩o ?minlow)")
case True
hence "T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩p⇩r⇩e⇩d' (treeList ! ?h) ?l"
using ‹deg = Suc (Suc _)› False hprop by simp
moreover have "treeList ! ?h ∈ set treeList" using hprop by simp
moreover hence "T⇩p⇩r⇩e⇩d' (treeList ! ?h) ?l ≤ 1 + height (treeList ! ?h)" using 4(1) by simp
ultimately have "T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x ≤ 1+ 1+ height (treeList ! ?h)" by simp
then show ?thesis
by (smt (verit) Suc_le_mono ‹T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x = 1 + T⇩p⇩r⇩e⇩d' (treeList ! high x (deg div 2)) (low x (deg div 2))› ‹T⇩p⇩r⇩e⇩d' (treeList ! high x (deg div 2)) (low x (deg div 2)) ≤ 1 + height (treeList ! high x (deg div 2))› ‹treeList ! high x (deg div 2) ∈ set treeList› height_compose_child le_trans plus_1_eq_Suc)
next
case False
hence "T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩p⇩r⇩e⇩d' summary ?h"
using hprop ‹x ≤ ma›
by (cases "vebt_pred summary ?h") (auto simp add: ‹deg = Suc (Suc _)› Let_def)
hence "T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x ≤ 1 + 1 +height summary" using 4(2)[of ?h] by simp
then show ?thesis by(simp add: le_trans)
qed
next
case False
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
qed
qed
next
case (5 treeList n summary m deg mi ma)
then obtain n' :: nat where "n = Suc n'"
by (metis add.right_neutral add_Suc_right nth_mem old.nat.exhaust valid_0_not)
then have "deg = Suc (Suc (Suc (n' + n')))"
using 5 by linarith
then have degprop:"deg ≥ 2"
by linarith
then show ?case
proof(cases "x > ma")
case True
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
next
case False
hence "x ≤ ma" by simp
let ?l = "low x (deg div 2)"
let ?h = "high x (deg div 2)"
show ?thesis
proof(cases "?h< length treeList")
case True
hence hprop: "?h< length treeList" by simp
let ?minlow = "vebt_mint (treeList ! ?h)"
show ?thesis
proof(cases "?minlow ≠ None ∧ (Some ?l >⇩o ?minlow)")
case True
hence "T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩p⇩r⇩e⇩d' (treeList ! ?h) ?l"
using hprop False
by (simp add: ‹deg = Suc (Suc _)› Let_def)
moreover have "treeList ! ?h ∈ set treeList" using hprop by simp
moreover hence "T⇩p⇩r⇩e⇩d' (treeList ! ?h) ?l ≤ 1 + height (treeList ! ?h)" using 5(1) by simp
ultimately have "T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x ≤ 1+ 1+ height (treeList ! ?h)" by simp
then show ?thesis
by (smt (verit) Suc_le_mono ‹T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x = 1 + T⇩p⇩r⇩e⇩d' (treeList ! high x (deg div 2)) (low x (deg div 2))› ‹T⇩p⇩r⇩e⇩d' (treeList ! high x (deg div 2)) (low x (deg div 2)) ≤ 1 + height (treeList ! high x (deg div 2))› ‹treeList ! high x (deg div 2) ∈ set treeList› height_compose_child le_trans plus_1_eq_Suc)
next
case False
hence "T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x = 1+ T⇩p⇩r⇩e⇩d' summary ?h"
using hprop ‹x ≤ ma›
by (cases "vebt_pred summary ?h")
(auto simp add: ‹deg = Suc (Suc _)›)
hence "T⇩p⇩r⇩e⇩d' (Node (Some (mi, ma)) deg treeList summary) x ≤ 1 + 1 +height summary" using 5(2)[of ?h] by simp
then show ?thesis by(simp add: le_trans)
qed
next
case False
then show ?thesis
by (simp add: ‹deg = Suc (Suc _)›)
qed
qed
qed simp+
theorem pred_bound_size_univ': "invar_vebt t n ⟹ u = 2^n ⟹ T⇩p⇩r⇩e⇩d' t x ≤ 2 + lb (lb u)"
using pred_bound_height'[of t n x] height_double_log_univ_size[of u n t] by simp
end
end