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