src/HOL/Algebra/IntRing.thy
 changeset 55157 06897ea77f78 parent 49962 a8cc904a6820 child 55242 413ec965f95d
```     1.1 --- a/src/HOL/Algebra/IntRing.thy	Fri Jan 24 16:54:25 2014 +0000
1.2 +++ b/src/HOL/Algebra/IntRing.thy	Mon Jan 27 16:38:52 2014 +0000
1.3 @@ -4,7 +4,7 @@
1.4  *)
1.5
1.6  theory IntRing
1.7 -imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes"
1.8 +imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes"
1.9  begin
1.10
1.11  section {* The Ring of Integers *}
1.12 @@ -257,9 +257,8 @@
1.13   apply (elim exE)
1.14  proof -
1.15    fix a b x
1.16 -
1.17 -  from prime
1.18 -      have ppos: "0 <= p" by (simp add: prime_def)
1.19 +  have ppos: "0 <= p"
1.20 +    by (metis prime linear nat_0_iff zero_not_prime_nat)
1.21    have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
1.22    proof -
1.23      fix x
1.24 @@ -267,19 +266,18 @@
1.25      hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
1.26      thus "p dvd x" by (simp add: ppos)
1.27    qed
1.28 -
1.29 -
1.30    assume "a * b = x * p"
1.31    hence "p dvd a * b" by simp
1.32    hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
1.33    hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
1.34 -  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
1.35 +  hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)"
1.36 +    by (metis prime prime_dvd_mult_eq_nat)
1.37    hence "p dvd a | p dvd b" by (fast intro: unnat)
1.38    thus "(EX x. a = x * p) | (EX x. b = x * p)"
1.39    proof
1.40      assume "p dvd a"
1.41      hence "EX x. a = p * x" by (simp add: dvd_def)
1.42 -    from this obtain x
1.43 +    then obtain x
1.44          where "a = p * x" by fast
1.45      hence "a = x * p" by simp
1.46      hence "EX x. a = x * p" by simp
1.47 @@ -287,7 +285,7 @@
1.48    next
1.49      assume "p dvd b"
1.50      hence "EX x. b = p * x" by (simp add: dvd_def)
1.51 -    from this obtain x
1.52 +    then obtain x
1.53          where "b = p * x" by fast
1.54      hence "b = x * p" by simp
1.55      hence "EX x. b = x * p" by simp
1.56 @@ -295,14 +293,12 @@
1.57    qed
1.58  next
1.59    assume "UNIV = {uu. EX x. uu = x * p}"
1.60 -  from this obtain x
1.61 -      where "1 = x * p" by best
1.62 -  from this [symmetric]
1.63 -      have "p * x = 1" by (subst mult_commute)
1.64 +  then obtain x where "1 = x * p" by best
1.65 +  then have "p * x = 1" by (metis mult_commute)
1.66    hence "\<bar>p * x\<bar> = 1" by simp
1.67    hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
1.68 -  from this and prime
1.69 -      show "False" by (simp add: prime_def)
1.70 +  then  show "False"
1.71 +    by (metis prime abs_of_pos one_not_prime_int prime_gt_0_int prime_int_def)
1.72  qed
1.73
1.74
1.75 @@ -355,7 +351,7 @@
1.76  proof -
1.77    from kIl[unfolded ZMod_def]
1.78        have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs)
1.79 -  from this obtain xl
1.80 +  then obtain xl
1.81        where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
1.82        and k: "k = xl + r"
1.83        by auto
1.84 @@ -376,9 +372,9 @@
1.85        have "b \<in> ZMod m a"
1.86        unfolding ZMod_def
1.87        by (simp add: a_repr_independenceD)
1.88 -  from this
1.89 +  then
1.90        have "EX x. b = x * m + a" by (rule rcos_zfact)
1.91 -  from this obtain x
1.92 +  then obtain x
1.93        where "b = x * m + a"
1.94        by fast
1.95
```