--- a/src/HOL/GCD.thy Fri Dec 04 11:03:54 2009 +0100
+++ b/src/HOL/GCD.thy Fri Dec 04 11:04:07 2009 +0100
@@ -779,14 +779,6 @@
apply auto
done
-lemma coprime_divprod_nat: "(d::nat) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
- using coprime_dvd_mult_iff_nat[of d a b]
- by (auto simp add: mult_commute)
-
-lemma coprime_divprod_int: "(d::int) dvd a * b \<Longrightarrow> coprime d a \<Longrightarrow> d dvd b"
- using coprime_dvd_mult_iff_int[of d a b]
- by (auto simp add: mult_commute)
-
lemma division_decomp_nat: assumes dc: "(a::nat) dvd b * c"
shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
proof-
--- a/src/HOL/List.thy Fri Dec 04 11:03:54 2009 +0100
+++ b/src/HOL/List.thy Fri Dec 04 11:04:07 2009 +0100
@@ -2665,6 +2665,10 @@
apply(rule length_remdups_leq)
done
+lemma remdups_filter: "remdups(filter P xs) = filter P (remdups xs)"
+apply(induct xs)
+apply auto
+done
lemma distinct_map:
"distinct(map f xs) = (distinct xs & inj_on f (set xs))"
--- a/src/HOL/Number_Theory/Primes.thy Fri Dec 04 11:03:54 2009 +0100
+++ b/src/HOL/Number_Theory/Primes.thy Fri Dec 04 11:04:07 2009 +0100
@@ -360,16 +360,15 @@
from prime_dvd_mult_nat[OF p pab']
have "p dvd a \<or> p dvd b" .
moreover
- {assume pa: "p dvd a"
- have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
+ { assume pa: "p dvd a"
from coprime_common_divisor_nat [OF ab, OF pa] p have "\<not> p dvd b" by auto
with p have "coprime b p"
by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
hence pnb: "coprime (p^n) b"
by (subst gcd_commute_nat, rule coprime_exp_nat)
- from coprime_divprod_nat[OF pnba pnb] have ?thesis by blast }
+ from coprime_dvd_mult_nat[OF pnb pab] have ?thesis by blast }
moreover
- {assume pb: "p dvd b"
+ { assume pb: "p dvd b"
have pnba: "p^n dvd b*a" using pab by (simp add: mult_commute)
from coprime_common_divisor_nat [OF ab, of p] pb p have "\<not> p dvd a"
by auto
@@ -377,7 +376,7 @@
by (subst gcd_commute_nat, intro prime_imp_coprime_nat)
hence pna: "coprime (p^n) a"
by (subst gcd_commute_nat, rule coprime_exp_nat)
- from coprime_divprod_nat[OF pab pna] have ?thesis by blast }
+ from coprime_dvd_mult_nat[OF pna pnba] have ?thesis by blast }
ultimately have ?thesis by blast}
ultimately show ?thesis by blast
qed