1.1 --- a/src/HOL/Library/Primes.thy	Sun Feb 22 11:30:57 2009 +0100
     1.2 +++ b/src/HOL/Library/Primes.thy	Sun Feb 22 17:25:28 2009 +0100
     1.3 @@ -45,12 +45,14 @@
     1.4    by (rule prime_dvd_square) (simp_all add: power2_eq_square)
     1.5  
     1.6  
     1.7 -lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0" by (induct n, auto)
     1.8 +lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0"
     1.9 +by (induct n, auto)
    1.10 +
    1.11  lemma exp_mono_lt: "(x::nat) ^ (Suc n) < y ^ (Suc n) \<longleftrightarrow> x < y"
    1.12 -  using power_less_imp_less_base[of x "Suc n" y] power_strict_mono[of x y "Suc n"]
    1.13 -    by auto
    1.14 +by(metis linorder_not_less not_less0 power_le_imp_le_base power_less_imp_less_base)
    1.15 +
    1.16  lemma exp_mono_le: "(x::nat) ^ (Suc n) \<le> y ^ (Suc n) \<longleftrightarrow> x \<le> y"
    1.17 -  by (simp only: linorder_not_less[symmetric] exp_mono_lt)
    1.18 +by (simp only: linorder_not_less[symmetric] exp_mono_lt)
    1.19  
    1.20  lemma exp_mono_eq: "(x::nat) ^ Suc n = y ^ Suc n \<longleftrightarrow> x = y"
    1.21  using power_inject_base[of x n y] by auto

     2.1 --- a/src/HOL/Nat.thy	Sun Feb 22 11:30:57 2009 +0100
     2.2 +++ b/src/HOL/Nat.thy	Sun Feb 22 17:25:28 2009 +0100
     2.3 @@ -735,6 +735,11 @@
     2.4    show "i < j ==> 0 < k ==> k * i < k * j" by (simp add: mult_less_mono2)
     2.5  qed
     2.6  
     2.7 +instance nat :: no_zero_divisors
     2.8 +proof
     2.9 +  fix a::nat and b::nat show "a ~= 0 \<Longrightarrow> b ~= 0 \<Longrightarrow> a * b ~= 0" by auto
    2.10 +qed
    2.11 +
    2.12  lemma nat_mult_1: "(1::nat) * n = n"
    2.13  by simp
    2.14  

     3.1 --- a/src/HOL/Parity.thy	Sun Feb 22 11:30:57 2009 +0100
     3.2 +++ b/src/HOL/Parity.thy	Sun Feb 22 17:25:28 2009 +0100
     3.3 @@ -228,20 +228,9 @@
     3.4  
     3.5  lemma zero_le_odd_power: "odd n ==>
     3.6      (0 <= (x::'a::{recpower,ordered_idom}) ^ n) = (0 <= x)"
     3.7 -  apply (simp add: odd_nat_equiv_def2)
     3.8 -  apply (erule exE)
     3.9 -  apply (erule ssubst)
    3.10 -  apply (subst power_Suc)
    3.11 -  apply (subst power_add)
    3.12 -  apply (subst zero_le_mult_iff)
    3.13 -  apply auto
    3.14 -  apply (subgoal_tac "x = 0 & y > 0")
    3.15 -  apply (erule conjE, assumption)
    3.16 -  apply (subst power_eq_0_iff [symmetric])
    3.17 -  apply (subgoal_tac "0 <= x^y * x^y")
    3.18 -  apply simp
    3.19 -  apply (rule zero_le_square)+
    3.20 -  done
    3.21 +apply (auto simp: odd_nat_equiv_def2 power_Suc power_add zero_le_mult_iff)
    3.22 +apply (metis field_power_not_zero no_zero_divirors_neq0 order_antisym_conv zero_le_square)
    3.23 +done
    3.24  
    3.25  lemma zero_le_power_eq[presburger]: "(0 <= (x::'a::{recpower,ordered_idom}) ^ n) =
    3.26      (even n | (odd n & 0 <= x))"

     4.1 --- a/src/HOL/Power.thy	Sun Feb 22 11:30:57 2009 +0100
     4.2 +++ b/src/HOL/Power.thy	Sun Feb 22 17:25:28 2009 +0100
     4.3 @@ -143,11 +143,13 @@
     4.4  done
     4.5  
     4.6  lemma power_eq_0_iff [simp]:
     4.7 -  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
     4.8 +  "(a^n = 0) \<longleftrightarrow>
     4.9 +   (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
    4.10  apply (induct "n")
    4.11 -apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
    4.12 +apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors)
    4.13  done
    4.14  
    4.15 +
    4.16  lemma field_power_not_zero:
    4.17    "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
    4.18  by force
    4.19 @@ -370,6 +372,13 @@
    4.20  lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
    4.21  by (induct "n", auto)
    4.22  
    4.23 +lemma nat_power_eq_Suc_0_iff [simp]: 
    4.24 +  "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
    4.25 +by (induct_tac m, auto)
    4.26 +
    4.27 +lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
    4.28 +by simp
    4.29 +
    4.30  text{*Valid for the naturals, but what if @{text"0<i<1"}?
    4.31  Premises cannot be weakened: consider the case where @{term "i=0"},
    4.32  @{term "m=1"} and @{term "n=0"}.*}