# HG changeset patch
# User huffman
# Date 1234981488 28800
# Node ID 33df3c4eb629f1e9ec3381b97bf16a2cfc605027
# Parent  d76b830366bcb6b3d7cc0f5a1a980ba43a4546cd
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power

diff -r d76b830366bc -r 33df3c4eb629 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Wed Feb 18 09:47:58 2009 -0800
+++ b/src/HOL/Divides.thy	Wed Feb 18 10:24:48 2009 -0800
@@ -889,21 +889,9 @@
   apply (simp only: dvd_eq_mod_eq_0)
   done
 
-lemma le_imp_power_dvd: "!!i::nat. m \<le> n ==> i^m dvd i^n"
-  apply (unfold dvd_def)
-  apply (erule linorder_not_less [THEN iffD2, THEN add_diff_inverse, THEN subst])
-  apply (simp add: power_add)
-  done
-
 lemma nat_zero_less_power_iff [simp]: "(x^n > 0) = (x > (0::nat) | n=0)"
   by (induct n) auto
 
-lemma power_le_dvd [rule_format]: "k^j dvd n --> i\<le>j --> k^i dvd (n::nat)"
-  apply (induct j)
-   apply (simp_all add: le_Suc_eq)
-  apply (blast dest!: dvd_mult_right)
-  done
-
 lemma power_dvd_imp_le: "[|i^m dvd i^n;  (1::nat) < i|] ==> m \<le> n"
   apply (rule power_le_imp_le_exp, assumption)
   apply (erule dvd_imp_le, simp)
diff -r d76b830366bc -r 33df3c4eb629 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Wed Feb 18 09:47:58 2009 -0800
+++ b/src/HOL/Power.thy	Wed Feb 18 10:24:48 2009 -0800
@@ -324,6 +324,24 @@
   shows "\<lbrakk>a ^ n = b ^ n; 0 \<le> a; 0 \<le> b; 0 < n\<rbrakk> \<Longrightarrow> a = b"
 by (cases n, simp_all, rule power_inject_base)
 
+text {* The divides relation *}
+
+lemma le_imp_power_dvd:
+  fixes a :: "'a::{comm_semiring_1,recpower}"
+  assumes "m \<le> n" shows "a^m dvd a^n"
+proof
+  have "a^n = a^(m + (n - m))"
+    using `m \<le> n` by simp
+  also have "\<dots> = a^m * a^(n - m)"
+    by (rule power_add)
+  finally show "a^n = a^m * a^(n - m)" .
+qed
+
+lemma power_le_dvd:
+  fixes a b :: "'a::{comm_semiring_1,recpower}"
+  shows "a^n dvd b \<Longrightarrow> m \<le> n \<Longrightarrow> a^m dvd b"
+  by (rule dvd_trans [OF le_imp_power_dvd])
+
 
 subsection{*Exponentiation for the Natural Numbers*}