added simp attributes/ proofs fixed
authornipkow
Wed Jan 09 19:23:50 2008 +0100 (2008-01-09)
changeset 25875536dfdc25e0a
parent 25874 14819a95cf75
child 25876 64647dcd2293
added simp attributes/ proofs fixed
src/HOL/Hyperreal/Ln.thy
src/HOL/Hyperreal/NthRoot.thy
src/HOL/Hyperreal/Transcendental.thy
src/HOL/Library/Parity.thy
src/HOL/Real/RealPow.thy
src/HOL/Word/Num_Lemmas.thy
     1.1 --- a/src/HOL/Hyperreal/Ln.thy	Wed Jan 09 19:23:36 2008 +0100
     1.2 +++ b/src/HOL/Hyperreal/Ln.thy	Wed Jan 09 19:23:50 2008 +0100
     1.3 @@ -190,7 +190,7 @@
     1.4    have "(1 - x) * (1 + x + x^2) = (1 - x^3)"
     1.5      by (simp add: ring_simps power2_eq_square power3_eq_cube)
     1.6    also have "... <= 1"
     1.7 -    by (auto intro: zero_le_power simp add: a)
     1.8 +    by (auto simp add: a)
     1.9    finally have "(1 - x) * (1 + x + x ^ 2) <= 1" .
    1.10    moreover have "0 < 1 + x + x^2"
    1.11      apply (rule add_pos_nonneg)
     2.1 --- a/src/HOL/Hyperreal/NthRoot.thy	Wed Jan 09 19:23:36 2008 +0100
     2.2 +++ b/src/HOL/Hyperreal/NthRoot.thy	Wed Jan 09 19:23:50 2008 +0100
     2.3 @@ -328,7 +328,7 @@
     2.4  unfolding isCont_def
     2.5  apply (rule LIM_I)
     2.6  apply (rule_tac x="r ^ n" in exI, safe)
     2.7 -apply (simp add: zero_less_power)
     2.8 +apply (simp)
     2.9  apply (simp add: real_root_abs [symmetric])
    2.10  apply (rule_tac n="n" in power_less_imp_less_base, simp_all)
    2.11  done
     3.1 --- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jan 09 19:23:36 2008 +0100
     3.2 +++ b/src/HOL/Hyperreal/Transcendental.thy	Wed Jan 09 19:23:50 2008 +0100
     3.3 @@ -740,7 +740,7 @@
     3.4  apply (simp add: exp_def)
     3.5  apply (rule real_le_trans)
     3.6  apply (rule_tac [2] n = 2 and f = "(%n. inverse (real (fact n)) * x ^ n)" in series_pos_le)
     3.7 -apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_power zero_le_mult_iff)
     3.8 +apply (auto intro: summable_exp simp add: numeral_2_eq_2 zero_le_mult_iff)
     3.9  done
    3.10  
    3.11  lemma exp_gt_one [simp]: "0 < (x::real) ==> 1 < exp x"
    3.12 @@ -1320,8 +1320,6 @@
    3.13    thus ?thesis by (simp add: mult_ac)
    3.14  qed
    3.15  
    3.16 -declare zero_less_power [simp]
    3.17 -
    3.18  lemma fact_lemma: "real (n::nat) * 4 = real (4 * n)"
    3.19  by simp
    3.20  
     4.1 --- a/src/HOL/Library/Parity.thy	Wed Jan 09 19:23:36 2008 +0100
     4.2 +++ b/src/HOL/Library/Parity.thy	Wed Jan 09 19:23:50 2008 +0100
     4.3 @@ -245,8 +245,6 @@
     4.4    apply (subst zero_le_odd_power [symmetric])
     4.5    apply assumption+
     4.6    apply (erule zero_le_even_power)
     4.7 -  apply (subst zero_le_odd_power)
     4.8 -  apply assumption+
     4.9    done
    4.10  
    4.11  lemma zero_less_power_eq[presburger]: "(0 < (x::'a::{recpower,ordered_idom}) ^ n) =
    4.12 @@ -270,12 +268,6 @@
    4.13    apply (frule order_le_imp_less_or_eq)
    4.14    apply simp
    4.15    apply (erule zero_le_even_power)
    4.16 -  apply (subgoal_tac "0 <= x^n")
    4.17 -  apply (frule order_le_imp_less_or_eq)
    4.18 -  apply auto
    4.19 -  apply (subst zero_le_odd_power)
    4.20 -  apply assumption
    4.21 -  apply (erule order_less_imp_le)
    4.22    done
    4.23  
    4.24  lemma power_less_zero_eq[presburger]: "((x::'a::{recpower,ordered_idom}) ^ n < 0) =
     5.1 --- a/src/HOL/Real/RealPow.thy	Wed Jan 09 19:23:36 2008 +0100
     5.2 +++ b/src/HOL/Real/RealPow.thy	Wed Jan 09 19:23:50 2008 +0100
     5.3 @@ -29,7 +29,7 @@
     5.4  
     5.5  
     5.6  lemma two_realpow_ge_one [simp]: "(1::real) \<le> 2 ^ n"
     5.7 -by (rule power_increasing[of 0 n "2::real", simplified])
     5.8 +by simp
     5.9  
    5.10  lemma two_realpow_gt [simp]: "real (n::nat) < 2 ^ n"
    5.11  apply (induct "n")
     6.1 --- a/src/HOL/Word/Num_Lemmas.thy	Wed Jan 09 19:23:36 2008 +0100
     6.2 +++ b/src/HOL/Word/Num_Lemmas.thy	Wed Jan 09 19:23:50 2008 +0100
     6.3 @@ -477,7 +477,7 @@
     6.4     apply (drule le_iff_add [THEN iffD1])
     6.5     apply (force simp: zpower_zadd_distrib)
     6.6    apply (rule mod_pos_pos_trivial)
     6.7 -   apply (simp add: zero_le_power)
     6.8 +   apply (simp)
     6.9    apply (rule power_strict_increasing)
    6.10     apply auto
    6.11    done