src/HOL/Power.thy
changeset 63924 f91766530e13
parent 63654 f90e3926e627
child 64065 40d440b75b00
     1.1 --- a/src/HOL/Power.thy	Tue Sep 20 14:51:58 2016 +0200
     1.2 +++ b/src/HOL/Power.thy	Sun Sep 18 17:57:55 2016 +0200
     1.3 @@ -297,6 +297,25 @@
     1.4  lemma is_unit_power_iff: "is_unit (a ^ n) \<longleftrightarrow> is_unit a \<or> n = 0"
     1.5    by (induct n) (auto simp add: is_unit_mult_iff)
     1.6  
     1.7 +lemma dvd_power_iff:
     1.8 +  assumes "x \<noteq> 0"
     1.9 +  shows   "x ^ m dvd x ^ n \<longleftrightarrow> is_unit x \<or> m \<le> n"
    1.10 +proof
    1.11 +  assume *: "x ^ m dvd x ^ n"
    1.12 +  {
    1.13 +    assume "m > n"
    1.14 +    note *
    1.15 +    also have "x ^ n = x ^ n * 1" by simp
    1.16 +    also from \<open>m > n\<close> have "m = n + (m - n)" by simp
    1.17 +    also have "x ^ \<dots> = x ^ n * x ^ (m - n)" by (rule power_add)
    1.18 +    finally have "x ^ (m - n) dvd 1"
    1.19 +      by (subst (asm) dvd_times_left_cancel_iff) (insert assms, simp_all)
    1.20 +    with \<open>m > n\<close> have "is_unit x" by (simp add: is_unit_power_iff)
    1.21 +  }
    1.22 +  thus "is_unit x \<or> m \<le> n" by force
    1.23 +qed (auto intro: unit_imp_dvd simp: is_unit_power_iff le_imp_power_dvd)
    1.24 +
    1.25 +
    1.26  end
    1.27  
    1.28  context normalization_semidom