Renamed {left,right}_distrib to distrib_{right,left}.
1 (* Title: HOL/Algebra/IntRing.thy
2 Author: Stephan Hohe, TU Muenchen
3 Author: Clemens Ballarin
7 imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes"
10 section {* The Ring of Integers *}
12 subsection {* Some properties of @{typ int} *}
15 "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
17 apply (simp add: zdvd_antisym_abs)
18 apply (simp add: dvd_if_abs_eq)
22 subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
25 int_ring :: "int ring" ("\<Z>") where
26 "int_ring == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
28 lemma int_Zcarr [intro!, simp]:
29 "k \<in> carrier \<Z>"
35 apply (rule abelian_groupI, simp_all)
37 apply (rule comm_monoidI, simp_all)
38 apply (rule distrib_right)
39 apply (fast intro: left_minus)
45 apply (intro domain.intro domain_axioms.intro)
46 apply (rule int_is_cring)
47 apply (unfold int_ring_def, simp+)
52 subsection {* Interpretations *}
54 text {* Since definitions of derived operations are global, their
55 interpretation needs to be done as early as possible --- that is,
56 with as few assumptions as possible. *}
58 interpretation int: monoid \<Z>
59 where "carrier \<Z> = UNIV"
60 and "mult \<Z> x y = x * y"
62 and "pow \<Z> x n = x^n"
65 show "monoid \<Z>" by default auto
66 then interpret int: monoid \<Z> .
69 show "carrier \<Z> = UNIV" by simp
72 { fix x y show "mult \<Z> x y = x * y" by simp }
74 show one: "one \<Z> = 1" by simp
75 show "pow \<Z> x n = x^n" by (induct n) simp_all
78 interpretation int: comm_monoid \<Z>
79 where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
82 show "comm_monoid \<Z>" by default auto
83 then interpret int: comm_monoid \<Z> .
86 { fix x y have "mult \<Z> x y = x * y" by simp }
88 have one: "one \<Z> = 1" by simp
89 show "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
90 proof (cases "finite A")
91 case True then show ?thesis proof induct
92 case empty show ?case by (simp add: one)
94 case insert then show ?case by (simp add: Pi_def mult)
97 case False then show ?thesis by (simp add: finprod_def)
101 interpretation int: abelian_monoid \<Z>
102 where int_carrier_eq: "carrier \<Z> = UNIV"
103 and int_zero_eq: "zero \<Z> = 0"
104 and int_add_eq: "add \<Z> x y = x + y"
105 and int_finsum_eq: "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
108 show "abelian_monoid \<Z>" by default auto
109 then interpret int: abelian_monoid \<Z> .
112 show "carrier \<Z> = UNIV" by simp
115 { fix x y show "add \<Z> x y = x + y" by simp }
117 show zero: "zero \<Z> = 0" by simp
118 show "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
119 proof (cases "finite A")
120 case True then show ?thesis proof induct
121 case empty show ?case by (simp add: zero)
123 case insert then show ?case by (simp add: Pi_def add)
126 case False then show ?thesis by (simp add: finsum_def finprod_def)
130 interpretation int: abelian_group \<Z>
131 (* The equations from the interpretation of abelian_monoid need to be repeated.
132 Since the morphisms through which the abelian structures are interpreted are
133 not the identity, the equations of these interpretations are not inherited. *)
135 where "carrier \<Z> = UNIV"
137 and "add \<Z> x y = x + y"
138 and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
139 and int_a_inv_eq: "a_inv \<Z> x = - x"
140 and int_a_minus_eq: "a_minus \<Z> x y = x - y"
143 show "abelian_group \<Z>"
144 proof (rule abelian_groupI)
145 show "!!x. x \<in> carrier \<Z> ==> EX y : carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
148 then interpret int: abelian_group \<Z> .
150 { fix x y have "add \<Z> x y = x + y" by simp }
152 have zero: "zero \<Z> = 0" by simp
154 have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero)
155 then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) }
157 show "a_minus \<Z> x y = x - y" by (simp add: int.minus_eq add a_inv)
158 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
160 interpretation int: "domain" \<Z>
161 where "carrier \<Z> = UNIV"
163 and "add \<Z> x y = x + y"
164 and "finsum \<Z> f A = (if finite A then setsum f A else undefined)"
165 and "a_inv \<Z> x = - x"
166 and "a_minus \<Z> x y = x - y"
168 show "domain \<Z>" by unfold_locales (auto simp: distrib_right distrib_left)
170 add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
173 text {* Removal of occurrences of @{term UNIV} in interpretation result
177 "x \<in> UNIV = True"
178 "A \<subseteq> UNIV = True"
179 "(ALL x : UNIV. P x) = (ALL x. P x)"
180 "(EX x : UNIV. P x) = (EX x. P x)"
182 "(True ==> PROP R) == PROP R"
185 interpretation int (* FIXME [unfolded UNIV] *) :
186 partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
187 where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
188 and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
189 and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
191 show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
193 show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
195 show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
197 show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
198 by (simp add: lless_def) auto
201 interpretation int (* FIXME [unfolded UNIV] *) :
202 lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
203 where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y"
204 and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y"
206 let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
209 apply (simp add: least_def Upper_def)
211 apply (simp add: greatest_def Lower_def)
214 then interpret int: lattice "?Z" .
215 show "join ?Z x y = max x y"
216 apply (rule int.joinI)
217 apply (simp_all add: least_def Upper_def)
220 show "meet ?Z x y = min x y"
221 apply (rule int.meetI)
222 apply (simp_all add: greatest_def Lower_def)
227 interpretation int (* [unfolded UNIV] *) :
228 total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
232 subsection {* Generated Ideals of @{text "\<Z>"} *}
235 "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
236 apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
237 apply (simp add: cgenideal_def)
240 lemma multiples_principalideal:
241 "principalideal {x * a | x. True } \<Z>"
242 apply (subst int_Idl[symmetric], rule principalidealI)
243 apply (rule int.genideal_ideal, simp)
248 lemma prime_primeideal:
249 assumes prime: "prime (nat p)"
250 shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
251 apply (rule primeidealI)
252 apply (rule int.genideal_ideal, simp)
253 apply (rule int_is_cring)
254 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
255 apply clarsimp defer 1
256 apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
262 have ppos: "0 <= p" by (simp add: prime_def)
263 have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
266 assume "nat p dvd nat (abs x)"
267 hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric])
268 thus "p dvd x" by (simp add: ppos)
272 assume "a * b = x * p"
273 hence "p dvd a * b" by simp
274 hence "nat p dvd nat (abs (a * b))" using ppos by (simp add: nat_dvd_iff)
275 hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib)
276 hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime])
277 hence "p dvd a | p dvd b" by (fast intro: unnat)
278 thus "(EX x. a = x * p) | (EX x. b = x * p)"
281 hence "EX x. a = p * x" by (simp add: dvd_def)
283 where "a = p * x" by fast
284 hence "a = x * p" by simp
285 hence "EX x. a = x * p" by simp
286 thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
289 hence "EX x. b = p * x" by (simp add: dvd_def)
291 where "b = p * x" by fast
292 hence "b = x * p" by simp
293 hence "EX x. b = x * p" by simp
294 thus "(EX x. a = x * p) | (EX x. b = x * p)" ..
297 assume "UNIV = {uu. EX x. uu = x * p}"
299 where "1 = x * p" by best
300 from this [symmetric]
301 have "p * x = 1" by (subst mult_commute)
302 hence "\<bar>p * x\<bar> = 1" by simp
303 hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1)
305 show "False" by (simp add: prime_def)
309 subsection {* Ideals and Divisibility *}
311 lemma int_Idl_subset_ideal:
312 "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
313 by (rule int.Idl_subset_ideal', simp+)
315 lemma Idl_subset_eq_dvd:
316 "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)"
317 apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
318 apply (rule, clarify)
319 apply (simp add: dvd_def)
320 apply (simp add: dvd_def mult_ac)
324 "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
326 have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric])
327 have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric])
329 have "(l dvd k \<and> k dvd l) = ((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k}))"
330 by (subst a, subst b, simp)
331 also have "((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})" by (rule, fast+)
337 "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)"
338 apply (subst dvds_eq_abseq[symmetric])
339 apply (rule dvds_eq_Idl[symmetric])
343 subsection {* Ideals and the Modulus *}
346 ZMod :: "int => int => int set"
347 where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
350 ZMod_def genideal_def
353 assumes kIl: "k \<in> ZMod l r"
354 shows "EX x. k = x * l + r"
356 from kIl[unfolded ZMod_def]
357 have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs)
359 where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
364 by (simp add: int_Idl, fast)
366 have "k = x * l + r" by simp
367 thus "\<exists>x. k = x * l + r" ..
371 assumes zmods: "ZMod m a = ZMod m b"
372 shows "a mod m = b mod m"
374 interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
376 have "b \<in> ZMod m a"
378 by (simp add: a_repr_independenceD)
380 have "EX x. b = x * m + a" by (rule rcos_zfact)
382 where "b = x * m + a"
385 hence "b mod m = (x * m + a) mod m" by simp
387 have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq)
389 have "\<dots> = a mod m" by simp
391 have "b mod m = a mod m" .
392 thus "a mod m = b mod m" ..
396 shows "ZMod m a = ZMod m (a mod m)"
398 interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
401 apply (rule a_repr_independence'[symmetric])
402 apply (simp add: int_Idl a_r_coset_defs)
404 have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality)
405 hence "a = (a div m) * m + (a mod m)" by simp
406 thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast
411 assumes modeq: "a mod m = b mod m"
412 shows "ZMod m a = ZMod m b"
414 have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod)
415 also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric])
416 also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric])
417 finally show ?thesis .
420 corollary ZMod_eq_mod:
421 shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)"
422 by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod)
425 subsection {* Factorization *}
428 ZFact :: "int \<Rightarrow> int set ring"
429 where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
431 lemmas ZFact_defs = ZFact_def FactRing_def
433 lemma ZFact_is_cring:
434 shows "cring (ZFact k)"
435 apply (unfold ZFact_def)
436 apply (rule ideal.quotient_is_cring)
437 apply (intro ring.genideal_ideal)
438 apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
440 apply (rule int_is_cring)
444 "carrier (ZFact 0) = (\<Union>a. {{a}})"
445 apply (insert int.genideal_zero)
446 apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
450 "carrier (ZFact 1) = {UNIV}"
451 apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
452 apply (subst int.genideal_one)
453 apply (rule, rule, clarsimp)
454 apply (rule, rule, clarsimp)
455 apply (rule, clarsimp, arith)
456 apply (rule, clarsimp)
457 apply (rule exI[of _ "0"], clarsimp)
460 lemma ZFact_prime_is_domain:
461 assumes pprime: "prime (nat p)"
462 shows "domain (ZFact p)"
463 apply (unfold ZFact_def)
464 apply (rule primeideal.quotient_is_domain)
465 apply (rule prime_primeideal[OF pprime])