moved some theorems into HOL main corpus
authorhaftmann
Fri Jun 14 08:34:28 2019 +0000 (2 days ago)
changeset 70350571ae57313a4
parent 70349 697450fd25c1
child 70351 32b4e1aec5ca
moved some theorems into HOL main corpus
src/HOL/Data_Structures/AVL_Set.thy
src/HOL/Decision_Procs/Approximation_Bounds.thy
src/HOL/Library/Log_Nat.thy
src/HOL/Library/Tree_Real.thy
src/HOL/Rat.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Data_Structures/AVL_Set.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Data_Structures/AVL_Set.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -545,7 +545,8 @@
     1.4    have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict)
     1.5    hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power)
     1.6    also have "\<dots> \<le> log \<phi> (size1 t)"
     1.7 -    using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close>  by simp
     1.8 +    using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close>
     1.9 +    by (simp add: le_log_of_power) 
    1.10    also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)"
    1.11      by(simp add: log_base_change[of 2 \<phi>])
    1.12    finally show ?thesis .
     2.1 --- a/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Jun 14 08:34:28 2019 +0000
     2.2 +++ b/src/HOL/Decision_Procs/Approximation_Bounds.thy	Fri Jun 14 08:34:28 2019 +0000
     2.3 @@ -2540,16 +2540,16 @@
     2.4      have "0 < m" and "m \<noteq> 0" using \<open>0 < x\<close> Float powr_gt_zero[of 2 e]
     2.5        by (auto simp add: zero_less_mult_iff)
     2.6      define bl where "bl = bitlen m - 1"
     2.7 +    then have bitlen: "bitlen m = bl + 1"
     2.8 +      by simp
     2.9      hence "bl \<ge> 0"
    2.10 -      using \<open>m > 0\<close> by (simp add: bitlen_alt_def)
    2.11 +      using \<open>m > 0\<close> by (auto simp add: bitlen_alt_def)
    2.12      have "1 \<le> Float m e"
    2.13        using \<open>1 \<le> x\<close> Float unfolding less_eq_float_def by auto
    2.14      from bitlen_div[OF \<open>0 < m\<close>] float_gt1_scale[OF \<open>1 \<le> Float m e\<close>] \<open>bl \<ge> 0\<close>
    2.15      have x_bnds: "0 \<le> real_of_float (?x - 1)" "real_of_float (?x - 1) < 1"
    2.16 -      unfolding bl_def[symmetric]
    2.17 -      by (auto simp: powr_realpow[symmetric] field_simps)
    2.18 -         (auto simp : powr_minus field_simps)
    2.19 -
    2.20 +      using abs_real_le_2_powr_bitlen [of m] \<open>m > 0\<close>
    2.21 +      by (simp_all add: bitlen powr_realpow [symmetric] powr_minus powr_add field_simps)
    2.22      {
    2.23        have "float_round_down prec (lb_ln2 prec * ?s) \<le> ln 2 * (e + (bitlen m - 1))"
    2.24            (is "real_of_float ?lb2 \<le> _")
     3.1 --- a/src/HOL/Library/Log_Nat.thy	Fri Jun 14 08:34:28 2019 +0000
     3.2 +++ b/src/HOL/Library/Log_Nat.thy	Fri Jun 14 08:34:28 2019 +0000
     3.3 @@ -25,10 +25,6 @@
     3.4      by (simp add: real_of_nat_div_aux [symmetric])
     3.5  qed
     3.6  
     3.7 -lemma powr_eq_one_iff [simp]:
     3.8 -  "a powr x = 1 \<longleftrightarrow> x = 0" if "a > 1" for a x :: real
     3.9 -  using that by (auto simp: powr_def split: if_splits)
    3.10 -
    3.11  
    3.12  subsection \<open>Floorlog\<close>
    3.13  
     4.1 --- a/src/HOL/Library/Tree_Real.thy	Fri Jun 14 08:34:28 2019 +0000
     4.2 +++ b/src/HOL/Library/Tree_Real.thy	Fri Jun 14 08:34:28 2019 +0000
     4.3 @@ -19,7 +19,7 @@
     4.4  by (simp add: le_log2_of_power min_height_size1)
     4.5  
     4.6  lemma size1_log_if_complete: "complete t \<Longrightarrow> height t = log 2 (size1 t)"
     4.7 -by (simp add: log2_of_power_eq size1_if_complete)
     4.8 +by (simp add: size1_if_complete)
     4.9  
    4.10  lemma min_height_size1_log_if_incomplete:
    4.11    "\<not> complete t \<Longrightarrow> min_height t < log 2 (size1 t)"
     5.1 --- a/src/HOL/Rat.thy	Fri Jun 14 08:34:28 2019 +0000
     5.2 +++ b/src/HOL/Rat.thy	Fri Jun 14 08:34:28 2019 +0000
     5.3 @@ -629,7 +629,8 @@
     5.4  instantiation rat :: floor_ceiling
     5.5  begin
     5.6  
     5.7 -definition [code del]: "\<lfloor>x\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" for x :: rat
     5.8 +definition floor_rat :: "rat \<Rightarrow> int"
     5.9 +  where"\<lfloor>x\<rfloor> = (THE z. of_int z \<le> x \<and> x < of_int (z + 1))" for x :: rat
    5.10  
    5.11  instance
    5.12  proof
    5.13 @@ -639,7 +640,7 @@
    5.14  
    5.15  end
    5.16  
    5.17 -lemma floor_Fract: "\<lfloor>Fract a b\<rfloor> = a div b"
    5.18 +lemma floor_Fract [simp]: "\<lfloor>Fract a b\<rfloor> = a div b"
    5.19    by (simp add: Fract_of_int_quotient floor_divide_of_int_eq)
    5.20  
    5.21  
    5.22 @@ -788,6 +789,10 @@
    5.23      by (induct a) (simp add: of_rat_rat Fract_of_int_eq [symmetric])
    5.24  qed
    5.25  
    5.26 +lemma abs_of_rat [simp]:
    5.27 +  "\<bar>of_rat r\<bar> = (of_rat \<bar>r\<bar> :: 'a :: linordered_field)"
    5.28 +  by (cases "r \<ge> 0") (simp_all add: not_le of_rat_minus)
    5.29 +
    5.30  text \<open>Collapse nested embeddings.\<close>
    5.31  lemma of_rat_of_nat_eq [simp]: "of_rat (of_nat n) = of_nat n"
    5.32    by (induct n) (simp_all add: of_rat_add)
    5.33 @@ -801,6 +806,14 @@
    5.34  lemma of_rat_neg_numeral_eq [simp]: "of_rat (- numeral w) = - numeral w"
    5.35    using of_rat_of_int_eq [of "- numeral w"] by simp
    5.36  
    5.37 +lemma of_rat_floor [simp]:
    5.38 +  "\<lfloor>of_rat r\<rfloor> = \<lfloor>r\<rfloor>"
    5.39 +  by (cases r) (simp add: Fract_of_int_quotient of_rat_divide floor_divide_of_int_eq)
    5.40 +
    5.41 +lemma of_rat_ceiling [simp]:
    5.42 +  "\<lceil>of_rat r\<rceil> = \<lceil>r\<rceil>"
    5.43 +  using of_rat_floor [of "- r"] by (simp add: of_rat_minus ceiling_def)
    5.44 +
    5.45  lemmas zero_rat = Zero_rat_def
    5.46  lemmas one_rat = One_rat_def
    5.47  
     6.1 --- a/src/HOL/Transcendental.thy	Fri Jun 14 08:34:28 2019 +0000
     6.2 +++ b/src/HOL/Transcendental.thy	Fri Jun 14 08:34:28 2019 +0000
     6.3 @@ -1815,6 +1815,10 @@
     6.4    for x :: real
     6.5    by (auto simp: ln_real_def intro!: arg_cong[where f = The])
     6.6  
     6.7 +lemma powr_eq_one_iff [simp]:
     6.8 +  "a powr x = 1 \<longleftrightarrow> x = 0" if "a > 1" for a x :: real
     6.9 +  using that by (auto simp: powr_def split: if_splits)
    6.10 +
    6.11  lemma isCont_ln:
    6.12    fixes x :: real
    6.13    assumes "x \<noteq> 0"
    6.14 @@ -2693,6 +2697,10 @@
    6.15    fixes x y :: real shows "\<lbrakk> x > 1; y > 0 \<rbrakk> \<Longrightarrow> 1 < x powr y"
    6.16  by(simp add: less_powr_iff)
    6.17  
    6.18 +lemma log_pow_cancel [simp]:
    6.19 +  "a > 0 \<Longrightarrow> a \<noteq> 1 \<Longrightarrow> log a (a ^ b) = b"
    6.20 +  by (simp add: ln_realpow log_def)
    6.21 +
    6.22  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)"
    6.23    by (auto simp: floor_eq_iff powr_le_iff less_powr_iff)
    6.24