diff -r 91feea8e41e4 -r 22faf21db3df src/HOL/Algebra/IntRing.thy --- a/src/HOL/Algebra/IntRing.thy Fri Jan 30 13:41:45 2009 +0000 +++ b/src/HOL/Algebra/IntRing.thy Sat Jan 31 09:04:16 2009 +0100 @@ -265,6 +265,7 @@ apply fast done + lemma prime_primeideal: assumes prime: "prime (nat p)" shows "primeideal (Idl\<^bsub>\\<^esub> {p}) \" @@ -293,17 +294,7 @@ assume "a * b = x * p" hence "p dvd a * b" by simp - hence "nat p dvd nat (abs (a * b))" - apply (subst nat_dvd_iff, clarsimp) - apply (rule conjI, clarsimp, simp add: zabs_def) - proof (clarsimp) - assume a: " ~ 0 <= p" - from prime - have "0 < p" by (simp add: prime_def) - from a and this - have "False" by simp - thus "nat (abs (a * b)) = 0" .. - qed + hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff) hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib) hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime]) hence "p dvd a | p dvd b" by (fast intro: unnat)