src/HOL/Parity.thy
changeset 35216 7641e8d831d2
parent 35043 07dbdf60d5ad
child 35631 0b8a5fd339ab
     1.1 --- a/src/HOL/Parity.thy	Thu Feb 18 13:29:59 2010 -0800
     1.2 +++ b/src/HOL/Parity.thy	Thu Feb 18 14:21:44 2010 -0800
     1.3 @@ -184,7 +184,7 @@
     1.4    apply (rule conjI)
     1.5    apply simp
     1.6    apply (insert even_zero_nat, blast)
     1.7 -  apply (simp add: power_Suc)
     1.8 +  apply simp
     1.9    done
    1.10  
    1.11  lemma minus_one_even_power [simp]:
    1.12 @@ -199,7 +199,7 @@
    1.13       "(even x --> (-1::'a::{number_ring})^x = 1) &
    1.14        (odd x --> (-1::'a)^x = -1)"
    1.15    apply (induct x)
    1.16 -  apply (simp, simp add: power_Suc)
    1.17 +  apply (simp, simp)
    1.18    done
    1.19  
    1.20  lemma neg_one_even_power [simp]:
    1.21 @@ -214,7 +214,7 @@
    1.22       "(-x::'a::{comm_ring_1}) ^ n =
    1.23        (if even n then (x ^ n) else -(x ^ n))"
    1.24    apply (induct n)
    1.25 -  apply (simp_all split: split_if_asm add: power_Suc)
    1.26 +  apply simp_all
    1.27    done
    1.28  
    1.29  lemma zero_le_even_power: "even n ==>
    1.30 @@ -228,7 +228,7 @@
    1.31  
    1.32  lemma zero_le_odd_power: "odd n ==>
    1.33      (0 <= (x::'a::{linordered_idom}) ^ n) = (0 <= x)"
    1.34 -apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
    1.35 +apply (auto simp: odd_nat_equiv_def2 power_add zero_le_mult_iff)
    1.36  apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
    1.37  done
    1.38  
    1.39 @@ -373,7 +373,7 @@
    1.40  
    1.41  lemma even_power_le_0_imp_0:
    1.42      "a ^ (2*k) \<le> (0::'a::{linordered_idom}) ==> a=0"
    1.43 -  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff power_Suc)
    1.44 +  by (induct k) (auto simp add: zero_le_mult_iff mult_le_0_iff)
    1.45  
    1.46  lemma zero_le_power_iff[presburger]:
    1.47    "(0 \<le> a^n) = (0 \<le> (a::'a::{linordered_idom}) | even n)"
    1.48 @@ -387,7 +387,7 @@
    1.49    then obtain k where "n = Suc(2*k)"
    1.50      by (auto simp add: odd_nat_equiv_def2 numeral_2_eq_2)
    1.51    thus ?thesis
    1.52 -    by (auto simp add: power_Suc zero_le_mult_iff zero_le_even_power
    1.53 +    by (auto simp add: zero_le_mult_iff zero_le_even_power
    1.54               dest!: even_power_le_0_imp_0)
    1.55  qed
    1.56