--- a/src/HOL/Data_Structures/Balance.thy Sat Aug 26 00:43:26 2017 +0100
+++ b/src/HOL/Data_Structures/Balance.thy Sat Aug 26 12:56:17 2017 +0100
@@ -4,67 +4,9 @@
theory Balance
imports
- Complex_Main
- "HOL-Library.Tree"
+ "HOL-Library.Tree_Real"
begin
-(* The following two lemmas should go into theory \<open>Tree\<close>, except that that
-theory would then depend on \<open>Complex_Main\<close>. *)
-
-lemma min_height_balanced: assumes "balanced t"
-shows "min_height t = nat(floor(log 2 (size1 t)))"
-proof cases
- assume *: "complete t"
- hence "size1 t = 2 ^ min_height t"
- by (simp add: complete_iff_height size1_if_complete)
- hence "size1 t = 2 powr min_height t"
- using * by (simp add: powr_realpow)
- hence "min_height t = log 2 (size1 t)"
- by simp
- thus ?thesis
- by linarith
-next
- assume *: "\<not> complete t"
- hence "height t = min_height t + 1"
- using assms min_height_le_height[of t]
- by(auto simp add: balanced_def complete_iff_height)
- hence "2 ^ min_height t \<le> size1 t \<and> size1 t < 2 ^ (min_height t + 1)"
- by (metis * min_height_size1 size1_height_if_incomplete)
- hence "2 powr min_height t \<le> size1 t \<and> size1 t < 2 powr (min_height t + 1)"
- by(simp only: powr_realpow)
- (metis of_nat_less_iff of_nat_le_iff of_nat_numeral of_nat_power)
- hence "min_height t \<le> log 2 (size1 t) \<and> log 2 (size1 t) < min_height t + 1"
- by(simp add: log_less_iff le_log_iff)
- thus ?thesis by linarith
-qed
-
-lemma height_balanced: assumes "balanced t"
-shows "height t = nat(ceiling(log 2 (size1 t)))"
-proof cases
- assume *: "complete t"
- hence "size1 t = 2 ^ height t"
- by (simp add: size1_if_complete)
- hence "size1 t = 2 powr height t"
- using * by (simp add: powr_realpow)
- hence "height t = log 2 (size1 t)"
- by simp
- thus ?thesis
- by linarith
-next
- assume *: "\<not> complete t"
- hence **: "height t = min_height t + 1"
- using assms min_height_le_height[of t]
- by(auto simp add: balanced_def complete_iff_height)
- hence 0: "2 ^ min_height t < size1 t \<and> size1 t \<le> 2 ^ (min_height t + 1)"
- by (metis "*" min_height_size1_if_incomplete size1_height)
- hence "2 powr min_height t < size1 t \<and> size1 t \<le> 2 powr (min_height t + 1)"
- by(simp only: powr_realpow)
- (metis of_nat_less_iff of_nat_le_iff of_nat_numeral of_nat_power)
- hence "min_height t < log 2 (size1 t) \<and> log 2 (size1 t) \<le> min_height t + 1"
- by(simp add: log_le_iff less_log_iff)
- thus ?thesis using ** by linarith
-qed
-
(* mv *)
text \<open>The lemmas about \<open>floor\<close> and \<open>ceiling\<close> of \<open>log 2\<close> should be generalized
--- a/src/HOL/Library/Library.thy Sat Aug 26 00:43:26 2017 +0100
+++ b/src/HOL/Library/Library.thy Sat Aug 26 12:56:17 2017 +0100
@@ -80,6 +80,7 @@
Sum_of_Squares
Transitive_Closure_Table
Tree_Multiset
+ Tree_Real
Type_Length
While_Combinator
begin
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Tree_Real.thy Sat Aug 26 12:56:17 2017 +0100
@@ -0,0 +1,64 @@
+(* Author: Tobias Nipkow *)
+
+theory Tree_Real
+imports
+ Complex_Main
+ Tree
+begin
+
+text \<open>This theory is separate from @{theory Tree} because the former is discrete and builds on
+@{theory Main} whereas this theory builds on @{theory Complex_Main}.\<close>
+
+
+lemma size1_height_log: "log 2 (size1 t) \<le> height t"
+by (simp add: log2_of_power_le size1_height)
+
+lemma min_height_size1_log: "min_height t \<le> log 2 (size1 t)"
+by (simp add: le_log2_of_power min_height_size1)
+
+lemma size1_log_if_complete: "complete t \<Longrightarrow> height t = log 2 (size1 t)"
+by (simp add: log2_of_power_eq size1_if_complete)
+
+lemma min_height_size1_log_if_incomplete:
+ "\<not> complete t \<Longrightarrow> min_height t < log 2 (size1 t)"
+by (simp add: less_log2_of_power min_height_size1_if_incomplete)
+
+
+lemma min_height_balanced: assumes "balanced t"
+shows "min_height t = nat(floor(log 2 (size1 t)))"
+proof cases
+ assume *: "complete t"
+ hence "size1 t = 2 ^ min_height t"
+ by (simp add: complete_iff_height size1_if_complete)
+ from log2_of_power_eq[OF this] show ?thesis by linarith
+next
+ assume *: "\<not> complete t"
+ hence "height t = min_height t + 1"
+ using assms min_height_le_height[of t]
+ by(auto simp add: balanced_def complete_iff_height)
+ hence "size1 t < 2 ^ (min_height t + 1)"
+ by (metis * size1_height_if_incomplete)
+ hence "log 2 (size1 t) < min_height t + 1"
+ using log2_of_power_less size1_ge0 by blast
+ thus ?thesis using min_height_size1_log[of t] by linarith
+qed
+
+lemma height_balanced: assumes "balanced t"
+shows "height t = nat(ceiling(log 2 (size1 t)))"
+proof cases
+ assume *: "complete t"
+ hence "size1 t = 2 ^ height t"
+ by (simp add: size1_if_complete)
+ from log2_of_power_eq[OF this] show ?thesis
+ by linarith
+next
+ assume *: "\<not> complete t"
+ hence **: "height t = min_height t + 1"
+ using assms min_height_le_height[of t]
+ by(auto simp add: balanced_def complete_iff_height)
+ hence "size1 t \<le> 2 ^ (min_height t + 1)" by (metis size1_height)
+ from log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
+ show ?thesis by linarith
+qed
+
+end
\ No newline at end of file
--- a/src/HOL/Transcendental.thy Sat Aug 26 00:43:26 2017 +0100
+++ b/src/HOL/Transcendental.thy Sat Aug 26 12:56:17 2017 +0100
@@ -2545,6 +2545,9 @@
for a b x :: real
by (simp add: linorder_not_less [symmetric])
+lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
+by (induction n) (simp_all add: ac_simps powr_add)
+
lemma log_ln: "ln x = log (exp(1)) x"
by (simp add: log_def)
@@ -2695,6 +2698,40 @@
and less_powr_iff = log_less_iff[symmetric]
and le_powr_iff = log_le_iff[symmetric]
+lemma le_log_of_power:
+ assumes "b ^ n \<le> m" "1 < b"
+ shows "n \<le> log b m"
+proof -
+ from assms have "0 < m" by (metis less_trans zero_less_power less_le_trans zero_less_one)
+ thus ?thesis using assms by (simp add: le_log_iff powr_realpow)
+qed
+
+lemma le_log2_of_power: "2 ^ n \<le> m \<Longrightarrow> n \<le> log 2 m" for m n :: nat
+using le_log_of_power[of 2] by simp
+
+lemma log_of_power_le: "\<lbrakk> m \<le> b ^ n; b > 1; m > 0 \<rbrakk> \<Longrightarrow> log b (real m) \<le> n"
+by (simp add: log_le_iff powr_realpow)
+
+lemma log2_of_power_le: "\<lbrakk> m \<le> 2 ^ n; m > 0 \<rbrakk> \<Longrightarrow> log 2 m \<le> n" for m n :: nat
+using log_of_power_le[of _ 2] by simp
+
+lemma log_of_power_less: "\<lbrakk> m < b ^ n; b > 1; m > 0 \<rbrakk> \<Longrightarrow> log b (real m) < n"
+by (simp add: log_less_iff powr_realpow)
+
+lemma log2_of_power_less: "\<lbrakk> m < 2 ^ n; m > 0 \<rbrakk> \<Longrightarrow> log 2 m < n" for m n :: nat
+using log_of_power_less[of _ 2] by simp
+
+lemma less_log_of_power:
+ assumes "b ^ n < m" "1 < b"
+ shows "n < log b m"
+proof -
+ have "0 < m" by (metis assms less_trans zero_less_power zero_less_one)
+ thus ?thesis using assms by (simp add: less_log_iff powr_realpow)
+qed
+
+lemma less_log2_of_power: "2 ^ n < m \<Longrightarrow> n < log 2 m" for m n :: nat
+using less_log_of_power[of 2] by simp
+
lemma gr_one_powr[simp]:
fixes x y :: real shows "\<lbrakk> x > 1; y > 0 \<rbrakk> \<Longrightarrow> 1 < x powr y"
by(simp add: less_powr_iff)
@@ -2702,9 +2739,6 @@
lemma floor_log_eq_powr_iff: "x > 0 \<Longrightarrow> b > 1 \<Longrightarrow> \<lfloor>log b x\<rfloor> = k \<longleftrightarrow> b powr k \<le> x \<and> x < b powr (k + 1)"
by (auto simp add: floor_eq_iff powr_le_iff less_powr_iff)
-lemma powr_realpow: "0 < x \<Longrightarrow> x powr (real n) = x^n"
- by (induct n) (simp_all add: ac_simps powr_add)
-
lemma powr_real_of_int:
"x > 0 \<Longrightarrow> x powr real_of_int n = (if n \<ge> 0 then x ^ nat n else inverse (x ^ nat (- n)))"
using powr_realpow[of x "nat n"] powr_realpow[of x "nat (-n)"]
@@ -2771,22 +2805,17 @@
lemma log_nat_power: "0 < x \<Longrightarrow> log b (x^n) = real n * log b x"
by (simp add: log_powr powr_realpow [symmetric])
-lemma le_log_of_power:
- assumes "1 < b" "b ^ n \<le> m"
- shows "n \<le> log b m"
+lemma log_of_power_eq:
+ assumes "m = b ^ n" "b > 1"
+ shows "n = log b (real m)"
proof -
- from assms have "0 < m"
- by (metis less_trans zero_less_power less_le_trans zero_less_one)
- have "n = log b (b ^ n)"
- using assms(1) by (simp add: log_nat_power)
- also have "\<dots> \<le> log b m"
- using assms \<open>0 < m\<close> by simp
- finally show ?thesis .
+ have "n = log b (b ^ n)" using assms(2) by (simp add: log_nat_power)
+ also have "\<dots> = log b m" using assms by (simp)
+ finally show ?thesis .
qed
-lemma le_log2_of_power: "2 ^ n \<le> m \<Longrightarrow> n \<le> log 2 m"
- for m n :: nat
- using le_log_of_power[of 2] by simp
+lemma log2_of_power_eq: "m = 2 ^ n \<Longrightarrow> n = log 2 m" for m n :: nat
+using log_of_power_eq[of _ 2] by simp
lemma log_base_change: "0 < a \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log b x = log a x / log a b"
by (simp add: log_def)