--- a/src/HOL/Hyperreal/Ln.thy Fri Jun 22 22:41:17 2007 +0200
+++ b/src/HOL/Hyperreal/Ln.thy Sat Jun 23 19:33:22 2007 +0200
@@ -150,7 +150,7 @@
lemma aux3: "(0::real) <= x ==> (1 + x + x^2)/(1 + x^2) <= 1 + x"
apply (subst pos_divide_le_eq)
apply (simp add: zero_compare_simps)
- apply (simp add: ring_eq_simps zero_compare_simps)
+ apply (simp add: ring_simps zero_compare_simps)
done
lemma aux4: "0 <= (x::real) ==> x <= 1 ==> exp (x - x^2) <= 1 + x"
@@ -199,7 +199,7 @@
proof -
assume a: "0 <= (x::real)" and b: "x < 1"
have "(1 - x) * (1 + x + x^2) = (1 - x^3)"
- by (simp add: ring_eq_simps power2_eq_square power3_eq_cube)
+ by (simp add: ring_simps power2_eq_square power3_eq_cube)
also have "... <= 1"
by (auto intro: zero_le_power simp add: a)
finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
@@ -283,12 +283,9 @@
have e: "-x - 2 * x^2 <= - x / (1 - x)"
apply (rule mult_imp_le_div_pos)
apply (insert prems, force)
- apply (auto simp add: ring_eq_simps power2_eq_square)
- apply (subgoal_tac "- (x * x) + x * (x * (x * 2)) = x^2 * (2 * x - 1)")
- apply (erule ssubst)
- apply (rule mult_nonneg_nonpos)
- apply auto
- apply (auto simp add: ring_eq_simps power2_eq_square)
+ apply (auto simp add: ring_simps power2_eq_square)
+ apply(insert mult_right_le_one_le[of "x*x" "2*x"])
+ apply (simp)
done
from e d show "- x - 2 * x^2 <= ln (1 - x)"
by (rule order_trans)
@@ -404,7 +401,7 @@
apply simp
apply (subst ln_div [THEN sym])
apply arith
- apply (auto simp add: ring_eq_simps add_frac_eq frac_eq_eq
+ apply (auto simp add: ring_simps add_frac_eq frac_eq_eq
add_divide_distrib power2_eq_square)
apply (rule mult_pos_pos, assumption)+
apply assumption
@@ -423,7 +420,7 @@
apply auto
done
have "x * ln y - x * ln x = x * (ln y - ln x)"
- by (simp add: ring_eq_simps)
+ by (simp add: ring_simps)
also have "... = x * ln(y / x)"
apply (subst ln_div)
apply (rule b, rule a, rule refl)