Theory Weight_Balanced_Trees_log

(* Author: Tobias Nipkow *)

section ‹Weight-Balanced Trees Have Logarithmic Height, and More›

theory Weight_Balanced_Trees_log
imports
  Complex_Main
  "HOL-Library.Tree"
begin

(* FIXME add these to field_simps *)
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