src/HOL/Algebra/IntRing.thy
 changeset 29700 22faf21db3df parent 29424 948d616959e4 child 29948 cdf12a1cb963
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Jan 30 13:41:45 2009 +0000
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Sat Jan 31 09:04:16 2009 +0100
1.3 @@ -265,6 +265,7 @@
1.4  apply fast
1.5  done
1.6
1.7 +
1.8  lemma prime_primeideal:
1.9    assumes prime: "prime (nat p)"
1.10    shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
1.11 @@ -293,17 +294,7 @@
1.12
1.13    assume "a * b = x * p"
1.14    hence "p dvd a * b" by simp
1.15 -  hence "nat p dvd nat (abs (a * b))"
1.16 -  apply (subst nat_dvd_iff, clarsimp)
1.17 -  apply (rule conjI, clarsimp, simp add: zabs_def)
1.18 -  proof (clarsimp)
1.19 -    assume a: " ~ 0 <= p"
1.20 -    from prime
1.21 -        have "0 < p" by (simp add: prime_def)
1.22 -    from a and this
1.23 -        have "False" by simp
1.24 -    thus "nat (abs (a * b)) = 0" ..
1.25 -  qed
1.26 +  hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
1.27    hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
1.28    hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
1.29    hence "p dvd a | p dvd b" by (fast intro: unnat)
```