--- a/src/HOL/Hyperreal/Ln.thy Wed Jan 09 19:23:36 2008 +0100
+++ b/src/HOL/Hyperreal/Ln.thy Wed Jan 09 19:23:50 2008 +0100
@@ -190,7 +190,7 @@
have "(1 - x) * (1 + x + x^2) = (1 - x^3)"
by (simp add: ring_simps power2_eq_square power3_eq_cube)
also have "... <= 1"
- by (auto intro: zero_le_power simp add: a)
+ by (auto simp add: a)
finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
moreover have "0 < 1 + x + x^2"
apply (rule add_pos_nonneg)
--- a/src/HOL/Hyperreal/NthRoot.thy Wed Jan 09 19:23:36 2008 +0100
+++ b/src/HOL/Hyperreal/NthRoot.thy Wed Jan 09 19:23:50 2008 +0100
@@ -328,7 +328,7 @@
unfolding isCont_def
apply (rule LIM_I)
apply (rule_tac x="r ^ n" in exI, safe)
-apply (simp add: zero_less_power)
+apply (simp)
apply (simp add: real_root_abs [symmetric])
apply (rule_tac n="n" in power_less_imp_less_base, simp_all)
done
--- a/src/HOL/Hyperreal/Transcendental.thy Wed Jan 09 19:23:36 2008 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy Wed Jan 09 19:23:50 2008 +0100
@@ -740,7 +740,7 @@
apply (simp add: exp_def)
apply (rule real_le_trans)
apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
-apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_power zero_le_mult_iff)
+apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
done
lemma exp_gt_one [simp]: "0 < (x::real) ==> 1 < exp x"
@@ -1320,8 +1320,6 @@
thus ?thesis by (simp add: mult_ac)
qed
-declare zero_less_power [simp]
-
lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
by simp
--- a/src/HOL/Library/Parity.thy Wed Jan 09 19:23:36 2008 +0100
+++ b/src/HOL/Library/Parity.thy Wed Jan 09 19:23:50 2008 +0100
@@ -245,8 +245,6 @@
apply (subst zero_le_odd_power [symmetric])
apply assumption+
apply (erule zero_le_even_power)
- apply (subst zero_le_odd_power)
- apply assumption+
done
lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) =
@@ -270,12 +268,6 @@
apply (frule order_le_imp_less_or_eq)
apply simp
apply (erule zero_le_even_power)
- apply (subgoal_tac "0 <= x^n")
- apply (frule order_le_imp_less_or_eq)
- apply auto
- apply (subst zero_le_odd_power)
- apply assumption
- apply (erule order_less_imp_le)
done
lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
--- a/src/HOL/Real/RealPow.thy Wed Jan 09 19:23:36 2008 +0100
+++ b/src/HOL/Real/RealPow.thy Wed Jan 09 19:23:50 2008 +0100
@@ -29,7 +29,7 @@
lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
-by (rule power_increasing[of 0 n "2::real", simplified])
+by simp
lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
apply (induct "n")
--- a/src/HOL/Word/Num_Lemmas.thy Wed Jan 09 19:23:36 2008 +0100
+++ b/src/HOL/Word/Num_Lemmas.thy Wed Jan 09 19:23:50 2008 +0100
@@ -477,7 +477,7 @@
apply (drule le_iff_add [THEN iffD1])
apply (force simp: zpower_zadd_distrib)
apply (rule mod_pos_pos_trivial)
- apply (simp add: zero_le_power)
+ apply (simp)
apply (rule power_strict_increasing)
apply auto
done