1.1 --- a/src/HOL/Power.thy	Wed Mar 04 10:43:39 2009 +0100
     1.2 +++ b/src/HOL/Power.thy	Wed Mar 04 10:45:52 2009 +0100
     1.3 @@ -31,7 +31,7 @@
     1.4    by (induct n) (simp_all add: power_Suc)
     1.5  
     1.6  lemma power_one_right [simp]: "(a::'a::recpower) ^ 1 = a"
     1.7 -  by (simp add: power_Suc)
     1.8 +  unfolding One_nat_def by (simp add: power_Suc)
     1.9  
    1.10  lemma power_commutes: "(a::'a::recpower) ^ n * a = a * a ^ n"
    1.11    by (induct n) (simp_all add: power_Suc mult_assoc)
    1.12 @@ -143,11 +143,13 @@
    1.13  done
    1.14  
    1.15  lemma power_eq_0_iff [simp]:
    1.16 -  "(a^n = 0) = (a = (0::'a::{ring_1_no_zero_divisors,recpower}) & n>0)"
    1.17 +  "(a^n = 0) \<longleftrightarrow>
    1.18 +   (a = (0::'a::{mult_zero,zero_neq_one,no_zero_divisors,recpower}) & n\<noteq>0)"
    1.19  apply (induct "n")
    1.20 -apply (auto simp add: power_Suc zero_neq_one [THEN not_sym])
    1.21 +apply (auto simp add: power_Suc zero_neq_one [THEN not_sym] no_zero_divisors)
    1.22  done
    1.23  
    1.24 +
    1.25  lemma field_power_not_zero:
    1.26    "a \<noteq> (0::'a::{ring_1_no_zero_divisors,recpower}) ==> a^n \<noteq> 0"
    1.27  by force
    1.28 @@ -324,6 +326,24 @@
    1.29    shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"
    1.30  by (cases n, simp_all, rule power_inject_base)
    1.31  
    1.32 +text {* The divides relation *}
    1.33 +
    1.34 +lemma le_imp_power_dvd:
    1.35 +  fixes a :: "'a::{comm_semiring_1,recpower}"
    1.36 +  assumes "m \<le> n" shows "a^m dvd a^n"
    1.37 +proof
    1.38 +  have "a^n = a^(m + (n - m))"
    1.39 +    using `m \<le> n` by simp
    1.40 +  also have "\<dots> = a^m * a^(n - m)"
    1.41 +    by (rule power_add)
    1.42 +  finally show "a^n = a^m * a^(n - m)" .
    1.43 +qed
    1.44 +
    1.45 +lemma power_le_dvd:
    1.46 +  fixes a b :: "'a::{comm_semiring_1,recpower}"
    1.47 +  shows "a^n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a^m dvd b"
    1.48 +  by (rule dvd_trans [OF le_imp_power_dvd])
    1.49 +
    1.50  
    1.51  subsection{*Exponentiation for the Natural Numbers*}
    1.52  
    1.53 @@ -346,12 +366,19 @@
    1.54    "of_nat (m ^ n) = (of_nat m::'a::{semiring_1,recpower}) ^ n"
    1.55  by (induct n, simp_all add: power_Suc of_nat_mult)
    1.56  
    1.57 -lemma nat_one_le_power [simp]: "1 \<le> i ==> Suc 0 \<le> i^n"
    1.58 -by (insert one_le_power [of i n], simp)
    1.59 +lemma nat_one_le_power [simp]: "Suc 0 \<le> i ==> Suc 0 \<le> i^n"
    1.60 +by (rule one_le_power [of i n, unfolded One_nat_def])
    1.61  
    1.62  lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
    1.63  by (induct "n", auto)
    1.64  
    1.65 +lemma nat_power_eq_Suc_0_iff [simp]: 
    1.66 +  "((x::nat)^m = Suc 0) = (m = 0 | x = Suc 0)"
    1.67 +by (induct_tac m, auto)
    1.68 +
    1.69 +lemma power_Suc_0[simp]: "(Suc 0)^n = Suc 0"
    1.70 +by simp
    1.71 +
    1.72  text{*Valid for the naturals, but what if @{text"0<i<1"}?
    1.73  Premises cannot be weakened: consider the case where @{term "i=0"},
    1.74  @{term "m=1"} and @{term "n=0"}.*}
    1.75 @@ -425,4 +452,3 @@
    1.76  *}
    1.77  
    1.78  end
    1.79 -