--- a/src/HOL/Library/Primes.thy Wed Mar 04 10:43:39 2009 +0100
+++ b/src/HOL/Library/Primes.thy Wed Mar 04 10:45:52 2009 +0100
@@ -45,12 +45,14 @@
by (rule prime_dvd_square) (simp_all add: power2_eq_square)
-lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0" by (induct n, auto)
+lemma exp_eq_1:"(x::nat)^n = 1 \<longleftrightarrow> x = 1 \<or> n = 0"
+by (induct n, auto)
+
lemma exp_mono_lt: "(x::nat) ^ (Suc n) < y ^ (Suc n) \<longleftrightarrow> x < y"
- using power_less_imp_less_base[of x "Suc n" y] power_strict_mono[of x y "Suc n"]
- by auto
+by(metis linorder_not_less not_less0 power_le_imp_le_base power_less_imp_less_base)
+
lemma exp_mono_le: "(x::nat) ^ (Suc n) \<le> y ^ (Suc n) \<longleftrightarrow> x \<le> y"
- by (simp only: linorder_not_less[symmetric] exp_mono_lt)
+by (simp only: linorder_not_less[symmetric] exp_mono_lt)
lemma exp_mono_eq: "(x::nat) ^ Suc n = y ^ Suc n \<longleftrightarrow> x = y"
using power_inject_base[of x n y] by auto
@@ -307,8 +309,8 @@
{fix e assume H: "e dvd a^n" "e dvd b^n"
from bezout_gcd_pow[of a n b] obtain x y
where xy: "a ^ n * x - b ^ n * y = ?gn \<or> b ^ n * x - a ^ n * y = ?gn" by blast
- from dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
- dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
+ from nat_dvd_diff [OF dvd_mult2[OF H(1), of x] dvd_mult2[OF H(2), of y]]
+ nat_dvd_diff [OF dvd_mult2[OF H(2), of x] dvd_mult2[OF H(1), of y]] xy
have "e dvd ?gn" by (cases "a ^ n * x - b ^ n * y = gcd a b ^ n", simp_all)}
hence th: "\<forall>e. e dvd a^n \<and> e dvd b^n \<longrightarrow> e dvd ?gn" by blast
from divides_exp[OF gcd_dvd1[of a b], of n] divides_exp[OF gcd_dvd2[of a b], of n] th