--- a/src/HOL/Transcendental.thy Sat Mar 19 16:53:09 2016 +0100
+++ b/src/HOL/Transcendental.thy Mon Mar 21 11:54:45 2016 +0100
@@ -12,7 +12,7 @@
text \<open>A fact theorem on reals.\<close>
-lemma square_fact_le_2_fact:
+lemma square_fact_le_2_fact:
shows "fact n * fact n \<le> (fact (2 * n) :: real)"
proof (induct n)
case 0 then show ?case by simp
@@ -2377,8 +2377,8 @@
and less_powr_iff = log_less_iff[symmetric]
and le_powr_iff = log_le_iff[symmetric]
-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)"
+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 ==> x powr (real n) = x^n"
@@ -2387,10 +2387,10 @@
lemma powr_numeral: "0 < x \<Longrightarrow> x powr (numeral n :: real) = x ^ (numeral n)"
by (metis of_nat_numeral powr_realpow)
-lemma powr_real_of_int:
+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)"]
- by (auto simp: field_simps powr_minus)
+ by (auto simp: field_simps powr_minus)
lemma powr2_sqrt[simp]: "0 < x \<Longrightarrow> sqrt x powr 2 = x"
by(simp add: powr_numeral)
@@ -2455,6 +2455,18 @@
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"
+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 `0 < m` by simp
+ finally show ?thesis .
+qed
+
+lemma le_log2_of_power: "2 ^ n \<le> (m::nat) \<Longrightarrow> n \<le> log 2 m"
+ using le_log_of_power[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)
@@ -2517,9 +2529,9 @@
by (simp add: powr_def root_powr_inverse sqrt_def)
lemma ln_powr_bound:
- fixes x::real shows "1 <= x ==> 0 < a ==> ln x <= (x powr a) / a"
-by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute mult_imp_le_div_pos not_less powr_gt_zero)
-
+ fixes x::real shows "1 \<le> x \<Longrightarrow> 0 < a \<Longrightarrow> ln x \<le> (x powr a) / a"
+ by (metis exp_gt_zero linear ln_eq_zero_iff ln_exp ln_less_self ln_powr mult.commute
+ mult_imp_le_div_pos not_less powr_gt_zero)
lemma ln_powr_bound2:
fixes x::real
@@ -3615,13 +3627,13 @@
by (auto simp: algebra_simps cos_diff assms)
then have "\<exists>!x. 0 \<le> x \<and> x \<le> pi \<and> cos x = 0"
by (auto simp: intro!: cos_total)
- then obtain \<theta> where \<theta>: "0 \<le> \<theta>" "\<theta> \<le> pi" "cos \<theta> = 0"
+ then obtain \<theta> where \<theta>: "0 \<le> \<theta>" "\<theta> \<le> pi" "cos \<theta> = 0"
and uniq: "\<And>\<phi>. \<lbrakk>0 \<le> \<phi>; \<phi> \<le> pi; cos \<phi> = 0\<rbrakk> \<Longrightarrow> \<phi> = \<theta>"
by blast
then have "x - real n * pi = \<theta>"
using x by blast
moreover have "pi/2 = \<theta>"
- using pi_half_ge_zero uniq by fastforce
+ using pi_half_ge_zero uniq by fastforce
ultimately show ?thesis
by (rule_tac x = "Suc (2 * n)" in exI) (simp add: algebra_simps)
qed
@@ -3650,7 +3662,7 @@
assume "cos x = 0" then show ?rhs
using cos_zero_lemma [of x] cos_zero_lemma [of "-x"] by force
next
- assume ?rhs then show "cos x = 0"
+ assume ?rhs then show "cos x = 0"
by (auto dest: * simp del: eq_divide_eq_numeral1)
qed
qed
@@ -3663,7 +3675,7 @@
assume "sin x = 0" then show ?rhs
using sin_zero_lemma [of x] sin_zero_lemma [of "-x"] by force
next
- assume ?rhs then show "sin x = 0"
+ assume ?rhs then show "sin x = 0"
by (auto elim: evenE)
qed
@@ -3690,7 +3702,7 @@
proof safe
assume "sin x = 0"
then show "\<exists>n. even n \<and> x = of_int n * (pi / 2)"
- apply (simp add: sin_zero_iff, safe)
+ apply (simp add: sin_zero_iff, safe)
apply (metis even_int_iff of_int_of_nat_eq)
apply (rule_tac x="- (int n)" in exI, simp)
done
@@ -4233,7 +4245,7 @@
case True
hence i_nat: "of_int i = of_int (nat i)" by auto
show ?thesis unfolding i_nat
- by (metis of_int_of_nat_eq tan_periodic_nat)
+ by (metis of_int_of_nat_eq tan_periodic_nat)
next
case False
hence i_nat: "of_int i = - of_int (nat (-i))" by auto
@@ -4241,7 +4253,7 @@
by auto
also have "\<dots> = tan (x + of_int i * pi)"
unfolding i_nat mult_minus_left diff_minus_eq_add
- by (metis of_int_of_nat_eq tan_periodic_nat)
+ by (metis of_int_of_nat_eq tan_periodic_nat)
finally show ?thesis by auto
qed
@@ -4950,7 +4962,7 @@
lemma machin_Euler: "5 * arctan(1/7) + 2 * arctan(3/79) = pi/4"
proof -
have 17: "\<bar>1/7\<bar> < (1 :: real)" by auto
- with arctan_double have "2 * arctan (1/7) = arctan (7/24)"
+ with arctan_double have "2 * arctan (1/7) = arctan (7/24)"
by simp (simp add: field_simps)
moreover have "\<bar>7/24\<bar> < (1 :: real)" by auto
with arctan_double have "2 * arctan (7/24) = arctan (336/527)" by simp (simp add: field_simps)