equal
deleted
inserted
replaced
543 shows "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)" |
543 shows "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)" |
544 proof - |
544 proof - |
545 have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict) |
545 have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict) |
546 hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power) |
546 hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power) |
547 also have "\<dots> \<le> log \<phi> (size1 t)" |
547 also have "\<dots> \<le> log \<phi> (size1 t)" |
548 using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close> by simp |
548 using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close> |
|
549 by (simp add: le_log_of_power) |
549 also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)" |
550 also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)" |
550 by(simp add: log_base_change[of 2 \<phi>]) |
551 by(simp add: log_base_change[of 2 \<phi>]) |
551 finally show ?thesis . |
552 finally show ?thesis . |
552 qed |
553 qed |
553 |
554 |