src/HOL/Algebra/IntRing.thy
 author haftmann Sun Jun 23 21:16:07 2013 +0200 (2013-06-23) changeset 52435 6646bb548c6b parent 49962 a8cc904a6820 child 55157 06897ea77f78 permissions -rw-r--r--
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
1 (*  Title:      HOL/Algebra/IntRing.thy
2     Author:     Stephan Hohe, TU Muenchen
3     Author:     Clemens Ballarin
4 *)
6 theory IntRing
7 imports QuotRing Lattice Int "~~/src/HOL/Old_Number_Theory/Primes"
8 begin
10 section {* The Ring of Integers *}
12 subsection {* Some properties of @{typ int} *}
14 lemma dvds_eq_abseq:
15   "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))"
16 apply rule
17  apply (simp add: zdvd_antisym_abs)
18 apply (simp add: dvd_if_abs_eq)
19 done
22 subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *}
24 abbreviation
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>"
30   by simp
32 lemma int_is_cring:
33   "cring \<Z>"
34 apply (rule cringI)
35   apply (rule abelian_groupI, simp_all)
36   defer 1
37   apply (rule comm_monoidI, simp_all)
38  apply (rule distrib_right)
39 apply (fast intro: left_minus)
40 done
42 (*
43 lemma int_is_domain:
44   "domain \<Z>"
45 apply (intro domain.intro domain_axioms.intro)
46   apply (rule int_is_cring)
47  apply (unfold int_ring_def, simp+)
48 done
49 *)
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"
61     and "one \<Z> = 1"
62     and "pow \<Z> x n = x^n"
63 proof -
64   -- "Specification"
65   show "monoid \<Z>" by default auto
66   then interpret int: monoid \<Z> .
68   -- "Carrier"
69   show "carrier \<Z> = UNIV" by simp
71   -- "Operations"
72   { fix x y show "mult \<Z> x y = x * y" by simp }
73   note mult = this
74   show one: "one \<Z> = 1" by simp
75   show "pow \<Z> x n = x^n" by (induct n) simp_all
76 qed
78 interpretation int: comm_monoid \<Z>
79   where "finprod \<Z> f A = (if finite A then setprod f A else undefined)"
80 proof -
81   -- "Specification"
82   show "comm_monoid \<Z>" by default auto
83   then interpret int: comm_monoid \<Z> .
85   -- "Operations"
86   { fix x y have "mult \<Z> x y = x * y" by simp }
87   note mult = this
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)
93     next
94       case insert then show ?case by (simp add: Pi_def mult)
95     qed
96   next
97     case False then show ?thesis by (simp add: finprod_def)
98   qed
99 qed
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)"
106 proof -
107   -- "Specification"
108   show "abelian_monoid \<Z>" by default auto
109   then interpret int: abelian_monoid \<Z> .
111   -- "Carrier"
112   show "carrier \<Z> = UNIV" by simp
114   -- "Operations"
115   { fix x y show "add \<Z> x y = x + y" by simp }
116   note add = this
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)
122     next
123       case insert then show ?case by (simp add: Pi_def add)
124     qed
125   next
126     case False then show ?thesis by (simp add: finsum_def finprod_def)
127   qed
128 qed
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. *)
134   (* FIXME *)
135   where "carrier \<Z> = UNIV"
136     and "zero \<Z> = 0"
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"
141 proof -
142   -- "Specification"
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>"
146       by simp arith
147   qed auto
148   then interpret int: abelian_group \<Z> .
149   -- "Operations"
150   { fix x y have "add \<Z> x y = x + y" by simp }
151   note add = this
152   have zero: "zero \<Z> = 0" by simp
153   { fix x
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) }
156   note a_inv = this
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"
162     and "zero \<Z> = 0"
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"
167 proof -
168   show "domain \<Z>" by unfold_locales (auto simp: distrib_right distrib_left)
169 qed (simp
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
174   --- experimental. *}
176 lemma UNIV:
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)"
181   "(True --> Q) = Q"
182   "(True ==> PROP R) == PROP R"
183   by simp_all
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)"
190 proof -
191   show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
192     by default simp_all
193   show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV"
194     by simp
195   show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)"
196     by simp
197   show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)"
198     by (simp add: lless_def) auto
199 qed
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"
205 proof -
206   let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
207   show "lattice ?Z"
208     apply unfold_locales
209     apply (simp add: least_def Upper_def)
210     apply arith
211     apply (simp add: greatest_def Lower_def)
212     apply arith
213     done
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)
218     apply arith
219     done
220   show "meet ?Z x y = min x y"
221     apply (rule int.meetI)
222     apply (simp_all add: greatest_def Lower_def)
223     apply arith
224     done
225 qed
227 interpretation int (* [unfolded UNIV] *) :
228   total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)"
229   by default clarsimp
232 subsection {* Generated Ideals of @{text "\<Z>"} *}
234 lemma int_Idl:
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)
238   done
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)
244 apply fast
245 done
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)
257  apply (elim exE)
258 proof -
259   fix a b x
261   from prime
262       have ppos: "0 <= p" by (simp add: prime_def)
263   have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x"
264   proof -
265     fix 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)
269   qed
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)"
279   proof
280     assume "p dvd a"
281     hence "EX x. a = p * x" by (simp add: dvd_def)
282     from this obtain x
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)" ..
287   next
288     assume "p dvd b"
289     hence "EX x. b = p * x" by (simp add: dvd_def)
290     from this obtain x
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)" ..
295   qed
296 next
297   assume "UNIV = {uu. EX x. uu = x * p}"
298   from this obtain x
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)
304   from this and prime
305       show "False" by (simp add: prime_def)
306 qed
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)
321 done
323 lemma dvds_eq_Idl:
324   "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})"
325 proof -
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+)
332   finally
333     show ?thesis .
334 qed
336 lemma Idl_eq_abs:
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])
340 done
343 subsection {* Ideals and the Modulus *}
345 definition
346   ZMod :: "int => int => int set"
347   where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
349 lemmas ZMod_defs =
350   ZMod_def genideal_def
352 lemma rcos_zfact:
353   assumes kIl: "k \<in> ZMod l r"
354   shows "EX x. k = x * l + r"
355 proof -
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)
358   from this obtain xl
359       where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}"
360       and k: "k = xl + r"
361       by auto
362   from xl obtain x
363       where "xl = x * l"
364       by (simp add: int_Idl, fast)
365   from k and this
366       have "k = x * l + r" by simp
367   thus "\<exists>x. k = x * l + r" ..
368 qed
370 lemma ZMod_imp_zmod:
371   assumes zmods: "ZMod m a = ZMod m b"
372   shows "a mod m = b mod m"
373 proof -
374   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
375   from zmods
376       have "b \<in> ZMod m a"
377       unfolding ZMod_def
378       by (simp add: a_repr_independenceD)
379   from this
380       have "EX x. b = x * m + a" by (rule rcos_zfact)
381   from this obtain x
382       where "b = x * m + a"
383       by fast
385   hence "b mod m = (x * m + a) mod m" by simp
386   also
387       have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq)
388   also
389       have "\<dots> = a mod m" by simp
390   finally
391       have "b mod m = a mod m" .
392   thus "a mod m = b mod m" ..
393 qed
395 lemma ZMod_mod:
396   shows "ZMod m a = ZMod m (a mod m)"
397 proof -
398   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast)
399   show ?thesis
400       unfolding ZMod_def
401   apply (rule a_repr_independence'[symmetric])
402   apply (simp add: int_Idl a_r_coset_defs)
403   proof -
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
407   qed simp
408 qed
410 lemma zmod_imp_ZMod:
411   assumes modeq: "a mod m = b mod m"
412   shows "ZMod m a = ZMod m b"
413 proof -
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 .
418 qed
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 *}
427 definition
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)
439  apply simp
440 apply (rule int_is_cring)
441 done
443 lemma ZFact_zero:
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)
447 done
449 lemma ZFact_one:
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)
458 done
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])
466 done
468 end