1.1 --- a/src/HOL/Divides.thy	Wed Feb 18 09:47:58 2009 -0800
     1.2 +++ b/src/HOL/Divides.thy	Wed Feb 18 10:24:48 2009 -0800
     1.3 @@ -889,21 +889,9 @@
     1.4    apply (simp only: dvd_eq_mod_eq_0)
     1.5    done
     1.6  
     1.7 -lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
     1.8 -  apply (unfold dvd_def)
     1.9 -  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
    1.10 -  apply (simp add: power_add)
    1.11 -  done
    1.12 -
    1.13  lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
    1.14    by (induct n) auto
    1.15  
    1.16 -lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
    1.17 -  apply (induct j)
    1.18 -   apply (simp_all add: le_Suc_eq)
    1.19 -  apply (blast dest!: dvd_mult_right)
    1.20 -  done
    1.21 -
    1.22  lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
    1.23    apply (rule power_le_imp_le_exp, assumption)
    1.24    apply (erule dvd_imp_le, simp)

     2.1 --- a/src/HOL/Power.thy	Wed Feb 18 09:47:58 2009 -0800
     2.2 +++ b/src/HOL/Power.thy	Wed Feb 18 10:24:48 2009 -0800
     2.3 @@ -324,6 +324,24 @@
     2.4    shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"
     2.5  by (cases n, simp_all, rule power_inject_base)
     2.6  
     2.7 +text {* The divides relation *}
     2.8 +
     2.9 +lemma le_imp_power_dvd:
    2.10 +  fixes a :: "'a::{comm_semiring_1,recpower}"
    2.11 +  assumes "m \<le> n" shows "a^m dvd a^n"
    2.12 +proof
    2.13 +  have "a^n = a^(m + (n - m))"
    2.14 +    using `m \<le> n` by simp
    2.15 +  also have "\<dots> = a^m * a^(n - m)"
    2.16 +    by (rule power_add)
    2.17 +  finally show "a^n = a^m * a^(n - m)" .
    2.18 +qed
    2.19 +
    2.20 +lemma power_le_dvd:
    2.21 +  fixes a b :: "'a::{comm_semiring_1,recpower}"
    2.22 +  shows "a^n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a^m dvd b"
    2.23 +  by (rule dvd_trans [OF le_imp_power_dvd])
    2.24 +
    2.25  
    2.26  subsection{*Exponentiation for the Natural Numbers*}
    2.27