--- a/src/HOL/Data_Structures/AVL_Set.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Data_Structures/AVL_Set.thy Fri Jun 14 08:34:28 2019 +0000
@@ -545,7 +545,8 @@
have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict)
hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power)
also have "\<dots> \<le> log \<phi> (size1 t)"
- using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close> by simp
+ using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close>
+ by (simp add: le_log_of_power)
also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)"
by(simp add: log_base_change[of 2 \<phi>])
finally show ?thesis .
--- a/src/HOL/Decision_Procs/Approximation_Bounds.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy Fri Jun 14 08:34:28 2019 +0000
@@ -2540,16 +2540,16 @@
have "0 < m" and "m \<noteq> 0" using \<open>0 < x\<close> Float powr_gt_zero[of 2 e]
by (auto simp add: zero_less_mult_iff)
define bl where "bl = bitlen m - 1"
+ then have bitlen: "bitlen m = bl + 1"
+ by simp
hence "bl \<ge> 0"
- using \<open>m > 0\<close> by (simp add: bitlen_alt_def)
+ using \<open>m > 0\<close> by (auto simp add: bitlen_alt_def)
have "1 \<le> Float m e"
using \<open>1 \<le> x\<close> Float unfolding less_eq_float_def by auto
from bitlen_div[OF \<open>0 < m\<close>] float_gt1_scale[OF \<open>1 \<le> Float m e\<close>] \<open>bl \<ge> 0\<close>
have x_bnds: "0 \<le> real_of_float (?x - 1)" "real_of_float (?x - 1) < 1"
- unfolding bl_def[symmetric]
- by (auto simp: powr_realpow[symmetric] field_simps)
- (auto simp : powr_minus field_simps)
-
+ using abs_real_le_2_powr_bitlen [of m] \<open>m > 0\<close>
+ by (simp_all add: bitlen powr_realpow [symmetric] powr_minus powr_add field_simps)
{
have "float_round_down prec (lb_ln2 prec * ?s) \<le> ln 2 * (e + (bitlen m - 1))"
(is "real_of_float ?lb2 \<le> _")
--- a/src/HOL/Library/Log_Nat.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Library/Log_Nat.thy Fri Jun 14 08:34:28 2019 +0000
@@ -25,10 +25,6 @@
by (simp add: real_of_nat_div_aux [symmetric])
qed
-lemma powr_eq_one_iff [simp]:
- "a powr x = 1 \<longleftrightarrow> x = 0" if "a > 1" for a x :: real
- using that by (auto simp: powr_def split: if_splits)
-
subsection \<open>Floorlog\<close>
--- a/src/HOL/Library/Tree_Real.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Library/Tree_Real.thy Fri Jun 14 08:34:28 2019 +0000
@@ -19,7 +19,7 @@
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)
+by (simp add: size1_if_complete)
lemma min_height_size1_log_if_incomplete:
"\<not> complete t \<Longrightarrow> min_height t < log 2 (size1 t)"
--- a/src/HOL/Rat.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Rat.thy Fri Jun 14 08:34:28 2019 +0000
@@ -629,7 +629,8 @@
instantiation rat :: floor_ceiling
begin
-definition [code del]: "\<lfloor>x\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" for x :: rat
+definition floor_rat :: "rat \<Rightarrow> int"
+ where"\<lfloor>x\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" for x :: rat
instance
proof
@@ -639,7 +640,7 @@
end
-lemma floor_Fract: "\<lfloor>Fract a b\<rfloor> = a div b"
+lemma floor_Fract [simp]: "\<lfloor>Fract a b\<rfloor> = a div b"
by (simp add: Fract_of_int_quotient floor_divide_of_int_eq)
@@ -788,6 +789,10 @@
by (induct a) (simp add: of_rat_rat Fract_of_int_eq [symmetric])
qed
+lemma abs_of_rat [simp]:
+ "\<bar>of_rat r\<bar> = (of_rat \<bar>r\<bar> :: 'a :: linordered_field)"
+ by (cases "r \<ge> 0") (simp_all add: not_le of_rat_minus)
+
text \<open>Collapse nested embeddings.\<close>
lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n"
by (induct n) (simp_all add: of_rat_add)
@@ -801,6 +806,14 @@
lemma of_rat_neg_numeral_eq [simp]: "of_rat (- numeral w) = - numeral w"
using of_rat_of_int_eq [of "- numeral w"] by simp
+lemma of_rat_floor [simp]:
+ "\<lfloor>of_rat r\<rfloor> = \<lfloor>r\<rfloor>"
+ by (cases r) (simp add: Fract_of_int_quotient of_rat_divide floor_divide_of_int_eq)
+
+lemma of_rat_ceiling [simp]:
+ "\<lceil>of_rat r\<rceil> = \<lceil>r\<rceil>"
+ using of_rat_floor [of "- r"] by (simp add: of_rat_minus ceiling_def)
+
lemmas zero_rat = Zero_rat_def
lemmas one_rat = One_rat_def
--- a/src/HOL/Transcendental.thy Fri Jun 14 08:34:28 2019 +0000
+++ b/src/HOL/Transcendental.thy Fri Jun 14 08:34:28 2019 +0000
@@ -1815,6 +1815,10 @@
for x :: real
by (auto simp: ln_real_def intro!: arg_cong[where f = The])
+lemma powr_eq_one_iff [simp]:
+ "a powr x = 1 \<longleftrightarrow> x = 0" if "a > 1" for a x :: real
+ using that by (auto simp: powr_def split: if_splits)
+
lemma isCont_ln:
fixes x :: real
assumes "x \<noteq> 0"
@@ -2693,6 +2697,10 @@
fixes x y :: real shows "\<lbrakk> x > 1; y > 0 \<rbrakk> \<Longrightarrow> 1 < x powr y"
by(simp add: less_powr_iff)
+lemma log_pow_cancel [simp]:
+ "a > 0 \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a ^ b) = b"
+ by (simp add: ln_realpow log_def)
+
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: floor_eq_iff powr_le_iff less_powr_iff)