# HG changeset patch
# User nipkow
# Date 1199903030 -3600
# Node ID 536dfdc25e0a8056215bbe287ba86d0f56c814bb
# Parent  14819a95cf7500028e38aa0d9e6854c016140cfe
added simp attributes/ proofs fixed

diff -r 14819a95cf75 -r 536dfdc25e0a src/HOL/Hyperreal/Ln.thy
--- 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)
diff -r 14819a95cf75 -r 536dfdc25e0a src/HOL/Hyperreal/NthRoot.thy
--- 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
diff -r 14819a95cf75 -r 536dfdc25e0a src/HOL/Hyperreal/Transcendental.thy
--- 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
 
diff -r 14819a95cf75 -r 536dfdc25e0a src/HOL/Library/Parity.thy
--- 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) =
diff -r 14819a95cf75 -r 536dfdc25e0a src/HOL/Real/RealPow.thy
--- 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")
diff -r 14819a95cf75 -r 536dfdc25e0a src/HOL/Word/Num_Lemmas.thy
--- 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