# HG changeset patch
# User haftmann
# Date 1560501268 0
# Node ID 571ae57313a494bc280ea8278385d52426b7656f
# Parent  697450fd25c1be8722ec034bd5774989cf81d093
moved some theorems into HOL main corpus

diff -r 697450fd25c1 -r 571ae57313a4 src/HOL/Data_Structures/AVL_Set.thy
--- 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 .
diff -r 697450fd25c1 -r 571ae57313a4 src/HOL/Decision_Procs/Approximation_Bounds.thy
--- 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> _")
diff -r 697450fd25c1 -r 571ae57313a4 src/HOL/Library/Log_Nat.thy
--- 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>
 
diff -r 697450fd25c1 -r 571ae57313a4 src/HOL/Library/Tree_Real.thy
--- 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)"
diff -r 697450fd25c1 -r 571ae57313a4 src/HOL/Rat.thy
--- 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
 
diff -r 697450fd25c1 -r 571ae57313a4 src/HOL/Transcendental.thy
--- 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)