2 Author: Stephan Hohe, TU Muenchen |
2 Author: Stephan Hohe, TU Muenchen |
3 Author: Clemens Ballarin |
3 Author: Clemens Ballarin |
4 *) |
4 *) |
5 |
5 |
6 theory IntRing |
6 theory IntRing |
7 imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes" |
7 imports "~~/src/HOL/Number_Theory/Primes" QuotRing Lattice Int |
8 begin |
8 begin |
9 |
9 |
10 section \<open>The Ring of Integers\<close> |
10 section \<open>The Ring of Integers\<close> |
11 |
11 |
12 subsection \<open>Some properties of @{typ int}\<close> |
12 subsection \<open>Some properties of @{typ int}\<close> |
238 apply clarsimp defer 1 |
238 apply clarsimp defer 1 |
239 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) |
239 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) |
240 apply (elim exE) |
240 apply (elim exE) |
241 proof - |
241 proof - |
242 fix a b x |
242 fix a b x |
243 assume "a * b = x * int p" |
243 assume "a * b = x * p" |
244 then have "p dvd a * b" by simp |
244 then have "p dvd a * b" by simp |
245 then have "p dvd a \<or> p dvd b" |
245 then have "p dvd a \<or> p dvd b" |
246 by (metis prime prime_dvd_mult_eq_int) |
246 by (metis prime prime_dvd_mult_eq_int) |
247 then show "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)" |
247 then show "(\<exists>x. a = x * p) \<or> (\<exists>x. b = x * p)" |
248 by (metis dvd_def mult.commute) |
248 by (metis dvd_def mult.commute) |
249 next |
249 next |
250 assume "UNIV = {uu. EX x. uu = x * int p}" |
250 assume "UNIV = {uu. EX x. uu = x * p}" |
251 then obtain x where "1 = x * int p" by best |
251 then obtain x where "1 = x * p" by best |
252 then have "\<bar>int p * x\<bar> = 1" by (simp add: mult.commute) |
252 then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute) |
253 then show False |
253 then show False using prime |
254 by (metis abs_of_nat of_nat_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime) |
254 by (auto dest!: abs_zmult_eq_1 simp: is_prime_def) |
255 qed |
255 qed |
256 |
256 |
257 |
257 |
258 subsection \<open>Ideals and Divisibility\<close> |
258 subsection \<open>Ideals and Divisibility\<close> |
259 |
259 |