Theory Weight_Balanced_Trees_log
section ‹Weight-Balanced Trees Have Logarithmic Height, and More›
theory Weight_Balanced_Trees_log
imports
Complex_Main
"HOL-Library.Tree"
begin
lemmas neq0_if = less_imp_neq dual_order.strict_implies_not_eq
subsection ‹Logarithmic Height›
text ‹The locale below is parameterized wrt to ‹Δ›. The original definition of weight-balanced trees
\<^cite>‹"NievergeltR72" and "NievergeltR73"› uses ‹α›. The constants ‹α› and ‹Δ› are interdefinable.
Below we start from ‹Δ› but derive ‹α›-versions of theorems as well.›
locale WBT0 =
fixes Δ :: real
begin
fun balanced1 :: "'a tree ⇒ 'a tree ⇒ bool" where
"balanced1 t1 t2 = (size1 t1 ≤ Δ * size1 t2)"
fun wbt :: "'a tree ⇒ bool" where
"wbt Leaf = True" |
"wbt (Node l _ r) = (balanced1 l r ∧ balanced1 r l ∧ wbt l ∧ wbt r)"
end
locale WBT1 = WBT0 +
assumes Delta: "Δ ≥ 1"
begin
definition α :: real where
"α = 1/(Δ+1)"
lemma Delta_def: "Δ = 1/α - 1"
unfolding α_def by auto
lemma shows alpha_pos: "0 < α" and alpha_ub: "α ≤ 1/2"
unfolding α_def using Delta by auto
lemma wbt_Node_alpha: "wbt (Node l x r) =
((let q = size1 l / (size1 l + size1 r)
in α ≤ q ∧ q ≤ 1 - α) ∧
wbt l ∧ wbt r)"
proof -
have "l > 0 ⟹ r > 0 ⟹
(1/(Δ+1) ≤ l/(l+r) ⟷ r/l ≤ Δ) ∧
(1/(Δ+1) ≤ r/(l+r) ⟷ l/r ≤ Δ) ∧
(l/(l+r) ≤ 1 - 1/(Δ+1) ⟷ l/r ≤ Δ) ∧
(r/(l+r) ≤ 1 - 1/(Δ+1) ⟷ r/l ≤ Δ)" for l r
using Delta by (simp add: field_simps divide_le_eq)
thus ?thesis using Delta by(auto simp: α_def Let_def pos_divide_le_eq add_pos_pos)
qed
lemma height_size1_Delta:
"wbt t ⟹ (1 + 1/Δ) ^ (height t) ≤ size1 t"
proof(induction t)
case Leaf thus ?case by simp
next
case (Node l a r)
let ?t = "Node l a r" let ?s = "size1 ?t" let ?d = "1 + 1/Δ"
from Node.prems(1) have 1: "size1 l * ?d ≤ ?s" and 2: "size1 r * ?d ≤ ?s"
using Delta by (auto simp: Let_def field_simps add_pos_pos neq0_if)
show ?case
proof (cases "height l ≤ height r")
case True
hence "?d ^ (height ?t) = ?d ^ (height r) * ?d" by(simp)
also have "… ≤ size1 r * ?d"
using Node.IH(2) Node.prems Delta unfolding wbt.simps
by (smt (verit) divide_nonneg_nonneg mult_mono of_nat_0_le_iff)
also have "… ≤ ?s" using 2 by (simp)
finally show ?thesis .
next
case False
hence "?d ^ (height ?t) = ?d ^ (height l) * ?d" by(simp)
also have "… ≤ size1 l * ?d"
using Node.IH(1) Node.prems Delta unfolding wbt.simps
by (smt (verit) divide_nonneg_nonneg mult_mono of_nat_0_le_iff)
also have "… ≤ ?s" using 1 by (simp)
finally show ?thesis .
qed
qed
lemma height_size1_alpha:
"wbt t ⟹ (1/(1-α)) ^ (height t) ≤ size1 t"
proof(induction t)
case Leaf thus ?case by simp
next
note wbt.simps[simp del] wbt_Node_alpha[simp]
case (Node l a r)
let ?t = "Node l a r" let ?s = "size1 ?t"
from Node.prems(1) have 1: "size1 l / (1-α) ≤ ?s" and 2: "size1 r / (1-α) ≤ ?s"
using alpha_ub by (auto simp: Let_def field_simps add_pos_pos neq0_if)
show ?case
proof (cases "height l ≤ height r")
case True
hence "(1/(1-α)) ^ (height ?t) = (1/(1-α)) ^ (height r) * (1/(1-α))" by(simp)
also have "… ≤ size1 r * (1/(1-α))"
using Node.IH(2) Node.prems unfolding wbt_Node_alpha
by (smt (verit) mult_right_mono zero_le_divide_1_iff)
also have "… ≤ ?s" using 2 by (simp)
finally show ?thesis .
next
case False
hence "(1/(1-α)) ^ (height ?t) = (1/(1-α)) ^ (height l) * (1/(1-α))" by(simp)
also have "… ≤ size1 l * (1/(1-α))"
using Node.IH(1) Node.prems unfolding wbt_Node_alpha
by (smt (verit) mult_right_mono zero_le_divide_1_iff)
also have "… ≤ ?s" using 1 by (simp)
finally show ?thesis .
qed
qed
lemma height_size1_log_Delta: assumes "wbt t"
shows "height t ≤ log 2 (size1 t) / log 2 (1 + 1/Δ)"
proof -
from height_size1_Delta[OF assms]
have "height t ≤ log (1 + 1/Δ) (size1 t)"
using Delta le_log_of_power by auto
also have "… = log 2 (size1 t) / log 2 (1 + 1/Δ)"
by (simp add: log_base_change)
finally show ?thesis .
qed
lemma height_size1_log_alpha: assumes "wbt t"
shows "height t ≤ log 2 (size1 t) / log 2 (1/(1-α))"
proof -
from height_size1_alpha[OF assms]
have "height t ≤ log (1/(1-α)) (size1 t)"
using alpha_pos alpha_ub le_log_of_power by auto
also have "… = log 2 (size1 t) / log 2 (1/(1-α))"
by (simp add: log_base_change)
finally show ?thesis .
qed
end
subsection ‹Every ‹1 ≤ Δ < 2› Yields Exactly the Complete Trees›
declare WBT0.wbt.simps [simp] WBT0.balanced1.simps [simp]
lemma wbt1_if_complete: assumes "1 ≤ Δ" shows "complete t ⟹ WBT0.wbt Δ t"
apply(induction t)
apply simp
apply (simp add: assms size1_if_complete)
done
lemma complete_if_wbt2: assumes "Δ < 2" shows "WBT0.wbt Δ t ⟹ complete t"
proof(induction t)
case Leaf
then show ?case by simp
next
case (Node t1 x t2)
let ?h1 = "height t1" let ?h2 = "height t2"
from Node have *: "complete t1 ∧ complete t2" by auto
hence sz: "size1 t1 = 2 ^ ?h1 ∧ size1 t2 = 2 ^ ?h2"
using size1_if_complete by blast
show ?case
proof (rule ccontr)
assume "¬ complete ⟨t1, x, t2⟩"
hence "?h1 ≠ ?h2" using * by auto
thus False
proof (cases "?h1 < ?h2")
case True
hence "2 * (2::real) ^ ?h1 ≤ 2 ^ ?h2"
by (metis Suc_leI one_le_numeral power_Suc power_increasing)
also have "… ≤ Δ * 2 ^ ?h1" using sz Node.prems by (simp)
finally show False using ‹Δ < 2› by simp
next
case False
with ‹?h1 ≠ ?h2› have "?h2 < ?h1" by linarith
hence "2 * (2::real) ^ ?h2 ≤ 2 ^ ?h1"
by (metis Suc_leI one_le_numeral power_Suc power_increasing)
also have "… ≤ Δ * 2 ^ ?h2" using sz Node.prems by (simp)
finally show False using ‹Δ < 2› by simp
qed
qed
qed
end