# HG changeset patch # User huffman # Date 1230134787 28800 # Node ID 562f95f06244ec04a3009a8bcea1e5c085f7a351 # Parent 0d49c5b5504626cc40bbf84c3a53d97cbbcbf306 cleaned up some proofs; removed redundant simp rules diff -r 0d49c5b55046 -r 562f95f06244 src/HOL/Transcendental.thy --- a/src/HOL/Transcendental.thy Tue Dec 23 15:02:30 2008 -0800 +++ b/src/HOL/Transcendental.thy Wed Dec 24 08:06:27 2008 -0800 @@ -640,11 +640,11 @@ lemma exp_gt_zero [simp]: "0 < exp (x::real)" by (simp add: order_less_le) -lemma inv_exp_gt_zero [simp]: "0 < inverse(exp x::real)" -by (auto intro: positive_imp_inverse_positive) +lemma inv_exp_gt_zero: "0 < inverse(exp x::real)" +by simp lemma abs_exp_cancel [simp]: "\exp x::real\ = exp x" -by auto +by simp lemma exp_real_of_nat_mult: "exp(real n * x) = exp(x) ^ n" apply (induct "n") @@ -653,21 +653,17 @@ lemma exp_diff: "exp(x - y) = exp(x)/(exp y)" apply (simp add: diff_minus divide_inverse) -apply (simp (no_asm) add: exp_add exp_minus) +apply (simp add: exp_add exp_minus) done - lemma exp_less_mono: fixes x y :: real - assumes xy: "x < y" shows "exp x < exp y" + assumes "x < y" shows "exp x < exp y" proof - - from xy have "1 < exp (y + - x)" - by (rule real_less_sum_gt_zero [THEN exp_gt_one]) - hence "exp x * inverse (exp x) < exp y * inverse (exp x)" - by (auto simp add: exp_add exp_minus) - thus ?thesis - by (simp add: divide_inverse [symmetric] pos_less_divide_eq - del: divide_self_if) + from `x < y` have "0 < y - x" by simp + hence "1 < exp (y - x)" by (rule exp_gt_one) + hence "1 < exp y / exp x" by (simp only: exp_diff) + thus "exp x < exp y" by simp qed lemma exp_less_cancel: "exp (x::real) < exp y ==> x < y" @@ -688,7 +684,7 @@ apply (rule IVT) apply (auto intro: isCont_exp simp add: le_diff_eq) apply (subgoal_tac "1 + (y - 1) \ exp (y - 1)") -apply simp +apply simp apply (rule exp_ge_add_one_self_aux, simp) done @@ -1074,9 +1070,6 @@ apply (simp del: realpow_Suc) done -lemma real_gt_one_ge_zero_add_less: "[| 1 < x; 0 \ y |] ==> 1 < x + (y::real)" -by arith - lemma abs_sin_le_one [simp]: "\sin x\ \ 1" by (rule power2_le_imp_le, simp_all add: sin_squared_eq) @@ -1173,7 +1166,7 @@ apply (auto simp add: diff_minus left_distrib right_distrib mult_ac add_ac) done -lemma sin_cos_minus [simp]: +lemma sin_cos_minus: "(sin(-x) + (sin x)) ^ 2 + (cos(-x) - (cos x)) ^ 2 = 0" apply (cut_tac y = 0 and x = x in lemma_DERIV_sin_cos_minus [THEN DERIV_isconst_all]) @@ -1181,14 +1174,10 @@ done lemma sin_minus [simp]: "sin (-x) = -sin(x)" -apply (cut_tac x = x in sin_cos_minus) -apply (simp del: sin_cos_minus) -done + using sin_cos_minus [where x=x] by simp lemma cos_minus [simp]: "cos (-x) = cos(x)" -apply (cut_tac x = x in sin_cos_minus) -apply (simp del: sin_cos_minus) -done + using sin_cos_minus [where x=x] by simp lemma sin_diff: "sin (x - y) = sin x * cos y - cos x * sin y" by (simp add: diff_minus sin_add) @@ -1203,13 +1192,11 @@ by (simp add: cos_diff mult_commute) lemma sin_double [simp]: "sin(2 * x) = 2* sin x * cos x" -by (cut_tac x = x and y = x in sin_add, auto) - + using sin_add [where x=x and y=x] by simp lemma cos_double: "cos(2* x) = ((cos x)\) - ((sin x)\)" -apply (cut_tac x = x and y = x in cos_add) -apply (simp add: power2_eq_square) -done + using cos_add [where x=x and y=x] + by (simp add: power2_eq_square) subsection {* The Constant Pi *} @@ -1387,8 +1374,8 @@ lemma pi_not_less_zero [simp]: "\ pi < 0" by (simp add: linorder_not_less) -lemma minus_pi_half_less_zero [simp]: "-(pi/2) < 0" -by auto +lemma minus_pi_half_less_zero: "-(pi/2) < 0" +by simp lemma sin_pi_half [simp]: "sin(pi/2) = 1" apply (cut_tac x = "pi/2" in sin_cos_squared_add2)