added lemmas
authornipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313b2441b0c8d38
parent 30297 41957d25a8b6
child 30315 495f51ec6ed4
added lemmas
src/HOL/Power.thy
     1.1 --- a/src/HOL/Power.thy	Fri Mar 06 11:50:32 2009 +0100
     1.2 +++ b/src/HOL/Power.thy	Fri Mar 06 17:38:47 2009 +0100
     1.3 @@ -338,6 +338,24 @@
     1.4    by (rule dvd_trans [OF le_imp_power_dvd])
     1.5  
     1.6  
     1.7 +lemma dvd_power_same:
     1.8 +  "(x::'a::{comm_semiring_1,recpower}) dvd y \<Longrightarrow> x^n dvd y^n"
     1.9 +by (induct n) (auto simp add: mult_dvd_mono)
    1.10 +
    1.11 +lemma dvd_power_le:
    1.12 +  "(x::'a::{comm_semiring_1,recpower}) dvd y \<Longrightarrow> m >= n \<Longrightarrow> x^n dvd y^m"
    1.13 +by(rule power_le_dvd[OF dvd_power_same])
    1.14 +
    1.15 +lemma dvd_power [simp]:
    1.16 +  "n > 0 | (x::'a::{comm_semiring_1,recpower}) = 1 \<Longrightarrow> x dvd x^n"
    1.17 +apply (erule disjE)
    1.18 + apply (subgoal_tac "x ^ n = x^(Suc (n - 1))")
    1.19 +  apply (erule ssubst)
    1.20 +  apply (subst power_Suc)
    1.21 +  apply auto
    1.22 +done
    1.23 +
    1.24 +
    1.25  subsection{*Exponentiation for the Natural Numbers*}
    1.26  
    1.27  instantiation nat :: recpower