Theory VEBT_Height
theory VEBT_Height imports VEBT_Definitions Complex_Main
begin
context VEBT_internal begin
section ‹Heights of van Emde Boas Trees›
fun height::"VEBT ⇒ nat" where
"height (Leaf a b) = 0"|
"height (Node _ deg treeList summary) = (1+ Max (height ` (insert summary (set treeList))))"
abbreviation "lb x ≡ log 2 x"
lemma setceilmax: "invar_vebt s m ⟹∀ t ∈ set listy. invar_vebt t n
⟹m = Suc n ⟹(∀ t ∈ set listy. height t = ⌈lb n ⌉ ) ⟹ height s = ⌈lb m⌉
⟹ Max (height ` (insert s (set listy))) = ⌈lb m⌉"
proof(induction listy)
case Nil
hence "Max (height ` (insert s(set []))) = height s" by simp
then show ?case using Nil by simp
next
case (Cons a list)
have "Max (height ` insert s (set (a # list))) =
max (height a) (Max (height ` insert s (set ( list))))"
by (simp add: insert_commute)
moreover have "max (height a) (Max (height ` insert s (set ( list)))) = max (height a) ⌈lb m ⌉"
using Cons insert_iff list.simps(15) max_def of_nat_max by force
moreover have " ∀ t ∈ set (a#list). invar_vebt t n " using Cons by simp
moreover hence "invar_vebt a n" by simp
hence "m ≥ n"
by (simp add: Cons.prems(3))
hence "lb m ≥ lb n"
using deg_not_0 ‹invar_vebt a n› by fastforce
hence "⌈ lb m⌉ ≥ ⌈ lb n⌉"
by (simp add: ceiling_mono)
moreover hence " max ⌈log 2 n ⌉ ⌈log 2 m ⌉ = ⌈log 2 m ⌉" by simp
ultimately show ?case
using Cons.prems(4) ‹invar_vebt a n›
by (metis list.set_intros(1))
qed
lemma log_ceil_idem:
assumes"(x::real) ≥ 1"
shows "⌈lb x ⌉ = ⌈lb ⌈x⌉⌉"
proof-
have "⌈log 2 x ⌉ ≥ 0"
by (smt (verit, ccfv_SIG) assms zero_le_ceiling zero_le_log_cancel_iff)
have " ⌈log 2 x ⌉ -1 < log 2 x ∧log 2 x ≤ ⌈log 2 x ⌉"
by linarith
moreover hence "2 powr (⌈log 2 x ⌉ -1) < x ∧ x ≤ 2 powr ( ⌈log 2 x ⌉)"
by (smt (verit, ccfv_SIG) assms less_log_iff real_nat_ceiling_ge)
moreover hence "2 powr ((⌈log 2 x ⌉ -1)) < ⌈x⌉" and " ⌈x⌉ ≤ 2 powr (⌈log 2 x ⌉)"
apply linarith
using ‹0 ≤ ⌈log 2 x⌉› calculation(2) ceiling_mono powr_int by fastforce
moreover hence " ⌈log 2 x ⌉ -1 < log 2 ⌈ x ⌉ ∧log 2 ⌈x⌉ ≤ ⌈log 2 x ⌉"
by (smt (verit, best) assms ceiling_correct less_log_iff)
ultimately show ?thesis
by linarith
qed
lemma heigt_uplog_rel:"invar_vebt t n ⟹ (height t) = ⌈lb n⌉"
proof(induction t n rule: invar_vebt.induct)
case (1 a b)
then show ?case by simp
next
case (2 treeList n summary m deg)
hence "m ≥ n" by simp
hence "log 2 m ≥ log 2 n"
by (simp add: "2.hyps"(3))
hence "⌈ log 2 m⌉ ≥ ⌈ log 2 n⌉"
by (simp add: "2.hyps"(3))
have "Max (height ` (insert summary (set treeList))) = ⌈ log 2 m⌉"
by (smt (verit, best) "2.IH"(1) "2.IH"(2) "2.hyps"(3) List.finite_set Max_in empty_is_image finite_imageI finite_insert image_iff insert_iff insert_not_empty)
hence "height (Node None deg treeList summary) = 1+ ⌈ log 2 m⌉" by simp
moreover have "1+ ⌈ log 2 m⌉ = ⌈1+ log 2 m⌉" by linarith
moreover have "1+ log 2 m = log 2 (2*m)"
using "2.hyps"(1) deg_not_0 log_mult by force
moreover hence "⌈1+ log 2 m⌉ = ⌈log 2 (2*m)⌉" by simp
moreover hence " ⌈log 2 (2*m)⌉ = ⌈log 2 (n+m)⌉"
using "2.hyps"(3) by force
ultimately show ?case
using "2.hyps"(4) by metis
next
case (3 treeList n summary m deg)
hence 00: "n ≥ 1 ∧ Suc n = m"
using set_n_deg_not_0 by blast
hence 0:"m ≥ n"using 3 by simp
hence 1:"log 2 m ≥ log 2 n"
using "3.IH"(1) "3.hyps"(2) set_n_deg_not_0 by fastforce
hence 2:"⌈ log 2 m⌉ ≥ ⌈ log 2 n⌉"
by (simp add: ceiling_mono)
have 3: "Max (height ` (insert summary (set treeList))) = ⌈ log 2 m⌉"
using "3.IH"(1) "3.IH"(2) "3.hyps"(3) List.finite_set Max_in empty_is_image
finite_imageI finite_insert image_iff insert_iff insert_not_empty "3.hyps"(1) setceilmax by auto
hence 4:"height (Node None deg treeList summary) = 1+ ⌈ log 2 m⌉" by simp
have 5:"1+ ⌈ log 2 m⌉ = ⌈1+ log 2 m⌉" by linarith
have 6:"1+ log 2 m = log 2 (m+m)"
using "3.hyps"(1) deg_not_0 log_mult by force
hence 7:"log 2 (m+n) = 1+log 2 ((n+m) / 2) "
by (simp add: "3.hyps"(3) log_divide)
have 8:"log 2 ((n+m) / 2) = log 2 (n + 1/2)"
by (smt (verit, best) "3.hyps"(3) field_sum_of_halves of_nat_Suc of_nat_add)
have 9 : "⌈ log 2 (n + 1/2) ⌉ = ⌈ log 2 ⌈n + 1/2 ⌉ ⌉"
by (smt (verit) "00" field_sum_of_halves log_ceil_idem of_nat_1 of_nat_mono)
hence 10: " ⌈n + 1/2 ⌉ = m" using 00 by linarith
hence 11: "⌈ log 2 (n + 1/2) ⌉ = ⌈ log 2 m ⌉ " using 9 by simp
hence 12:"⌈ 1+ log 2 (n + 1/2) ⌉ = ⌈1+ log 2 m ⌉"
by (smt (verit) ceiling_add_one)
hence "⌈ log 2 (n + n+1) ⌉ = ⌈ log 2 (m+m) ⌉"
using "3.hyps"(3) "6" "7" "8" by force
then show ?case
by (metis "12" "3.hyps"(4) "4" "5" "7" "8" add.commute)
next
case (4 treeList n summary m deg mi ma)
hence "m ≥ n" by simp
hence "log 2 m ≥ log 2 n"
by (simp add: "4.hyps"(3))
hence "⌈ log 2 m⌉ ≥ ⌈ log 2 n⌉"
by (simp add: "4.hyps"(3))
have "Max (height ` (insert summary (set treeList))) = ⌈ log 2 m⌉"
by (smt (verit, best) "4.IH"(1) "4.IH"(2) "4.hyps"(3) List.finite_set Max_in empty_is_image finite_imageI finite_insert image_iff insert_iff insert_not_empty)
hence "height (Node None deg treeList summary) = 1+ ⌈ log 2 m⌉" by simp
moreover have "1+ ⌈ log 2 m⌉ = ⌈1+ log 2 m⌉" by linarith
moreover have "1+ log 2 m = log 2 (2*m)"
using "4.hyps"(1) deg_not_0 log_mult by force
moreover hence "⌈1+ log 2 m⌉ = ⌈log 2 (2*m)⌉" by simp
moreover hence " ⌈log 2 (2*m)⌉ = ⌈log 2 (n+m)⌉"
using "4.hyps"(3) by force
ultimately show ?case
by (metis "4.hyps"(4) height.simps(2))
next
case (5 treeList n summary m deg mi ma)
hence 00: "n ≥ 1 ∧ Suc n = m"
using set_n_deg_not_0 by blast
hence 0:"m ≥ n"using 5 by simp
hence 1:"log 2 m ≥ log 2 n"
using "5.IH"(1) "5.hyps"(2) set_n_deg_not_0 by fastforce
hence 2:"⌈ log 2 m⌉ ≥ ⌈ log 2 n⌉"
by (simp add: ceiling_mono)
have 3: "Max (height ` (insert summary (set treeList))) = ⌈ log 2 m⌉"
using "5.IH"(1) "5.IH"(2) "5.hyps"(3) List.finite_set Max_in empty_is_image
finite_imageI finite_insert image_iff insert_iff insert_not_empty "5.hyps"(1) setceilmax by auto
hence 4:"height (Node None deg treeList summary) = 1+ ⌈ log 2 m⌉" by simp
have 5:"1+ ⌈ log 2 m⌉ = ⌈1+ log 2 m⌉" by linarith
have 6:"1+ log 2 m = log 2 (m+m)"
using "5.hyps"(1) deg_not_0 log_mult by force
hence 7:"log 2 (m+n) = 1+log 2 ((n+m) / 2) "
by (simp add: "5.hyps"(3) log_divide)
have 8:"log 2 ((n+m) / 2) = log 2 (n + 1/2)"
by (smt (verit, best) "5.hyps"(3) field_sum_of_halves of_nat_Suc of_nat_add)
have 9 : "⌈ log 2 (n + 1/2) ⌉ = ⌈ log 2 ⌈n + 1/2 ⌉ ⌉"
by (smt (verit) "00" field_sum_of_halves log_ceil_idem of_nat_1 of_nat_mono)
hence 10: " ⌈n + 1/2 ⌉ = m" using 00 by linarith
hence 11: "⌈ log 2 (n + 1/2) ⌉ = ⌈ log 2 m ⌉ " using 9 by simp
hence 12:"⌈ 1+ log 2 (n + 1/2) ⌉ = ⌈1+ log 2 m ⌉"
by (smt (verit) ceiling_add_one)
hence "⌈ log 2 (n + n+1) ⌉ = ⌈ log 2 (m+m) ⌉"
using "5.hyps"(3) "6" "7" "8" by force
then show ?case
using "4" "5" "5.hyps"(3) "5.hyps"(4) "6" by force
qed
lemma two_powr_height_bound_deg:
assumes "invar_vebt t n "
shows " 2^(height t) ≤ 2*(n::nat)"
proof-
have " (height t) = ⌈ log 2 n⌉"
by (simp add: assms heigt_uplog_rel)
moreover have "⌈ log 2 n⌉ ≤ log 2 n +1" by simp
moreover hence "2 powr ⌈ log 2 n⌉ ≤ 2 powr (log 2 n +1)" by simp
moreover have " 2 powr (log 2 n +1) = 2 powr 1 * 2 powr (log 2 n)"
by (simp add: powr_add)
moreover hence " 2 powr (log 2 n +1) = 2 * n"
using assms deg_not_0 by force
ultimately show ?thesis
by (metis linorder_not_less not_one_le_zero of_int_0 of_int_less_iff of_int_numeral of_int_of_nat_eq of_nat_le_iff one_add_one order_less_le powr_realpow real_of_nat_eq_numeral_power_cancel_iff zle_add1_eq_le)
qed
text ‹Main Theorem›
theorem height_double_log_univ_size:
assumes "u = 2^deg" and "invar_vebt t deg "
shows "height t ≤ 1 + lb (lb u)"
proof-
have "(height t) = ⌈lb deg⌉"
by (simp add: assms(2) heigt_uplog_rel)
have "2^(height t) ≤ 2 * deg" using assms(2) two_powr_height_bound_deg[of t deg]
by (meson dual_order.eq_iff dual_order.trans self_le_ge2_pow)
hence "height t ≤ 1 + lb deg"
using ‹int (height t) = ⌈lb (real deg)⌉› by linarith
hence "height t ≤ 1 + lb (lb u)" using assms by simp
thus ?thesis by simp
qed
lemma height_compose_list: " t∈ set treeList ⟹
Max (height ` (insert summary (set treeList))) ≥ height t"
apply(induction treeList) apply simp
by (meson List.finite_set Max_ge finite_imageI finite_insert image_eqI subsetD subset_insertI)
lemma height_compose_child: " t∈ set treeList ⟹
height (Node info deg treeList summary) ≥ 1+ height t" by simp
lemma height_compose_summary: " height (Node info deg treeList summary) ≥ 1+ height summary" by simp
lemma height_i_max: " i < length x13 ⟹
height (x13 ! i) ≤ max foo (Max (height ` set x13))"
by (meson List.finite_set Max_ge finite_imageI max.coboundedI2 nth_mem rev_image_eqI)
lemma max_ins_scaled: " n* height x14 ≤ m + n* Max (insert (height x14) (height ` set x13))"
by (meson List.finite_set Max_ge finite_imageI finite_insert insertI1 mult_le_mono2 trans_le_add2)
lemma max_idx_list:
assumes "i < length x13 "
shows " n * height (x13 !i) ≤ Suc (Suc (n * max (height x14) (Max (height ` set x13))))"
by (metis assms height_i_max less_Suc_eq mult_le_mono2 nat_less_le)
end
end