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)