src/HOL/Algebra/IntRing.thy
 author paulson Wed Jun 06 14:25:53 2018 +0100 (16 months ago) changeset 68399 0b71d08528f0 parent 67443 3abf6a722518 child 68561 5e85cda58af6 permissions -rw-r--r--
resolution of name clashes in Algebra
1 (*  Title:      HOL/Algebra/IntRing.thy
2     Author:     Stephan Hohe, TU Muenchen
3     Author:     Clemens Ballarin
4 *)
6 theory IntRing
7 imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
8 begin
10 section \<open>The Ring of Integers\<close>
12 subsection \<open>Some properties of @{typ int}\<close>
14 lemma dvds_eq_abseq:
15   fixes k :: int
16   shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
17 apply rule
18  apply (simp add: zdvd_antisym_abs)
19 apply (simp add: dvd_if_abs_eq)
20 done
23 subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
25 abbreviation int_ring :: "int ring" ("\<Z>")
26   where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
28 lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
29   by simp
31 lemma int_is_cring: "cring \<Z>"
32 apply (rule cringI)
33   apply (rule abelian_groupI, simp_all)
34   defer 1
35   apply (rule comm_monoidI, simp_all)
36  apply (rule distrib_right)
37 apply (fast intro: left_minus)
38 done
40 (*
41 lemma int_is_domain:
42   "domain \<Z>"
43 apply (intro domain.intro domain_axioms.intro)
44   apply (rule int_is_cring)
45  apply (unfold int_ring_def, simp+)
46 done
47 *)
50 subsection \<open>Interpretations\<close>
52 text \<open>Since definitions of derived operations are global, their
53   interpretation needs to be done as early as possible --- that is,
54   with as few assumptions as possible.\<close>
56 interpretation int: monoid \<Z>
57   rewrites "carrier \<Z> = UNIV"
58     and "mult \<Z> x y = x * y"
59     and "one \<Z> = 1"
60     and "pow \<Z> x n = x^n"
61 proof -
62   \<comment> \<open>Specification\<close>
63   show "monoid \<Z>" by standard auto
64   then interpret int: monoid \<Z> .
66   \<comment> \<open>Carrier\<close>
67   show "carrier \<Z> = UNIV" by simp
69   \<comment> \<open>Operations\<close>
70   { fix x y show "mult \<Z> x y = x * y" by simp }
71   show "one \<Z> = 1" by simp
72   show "pow \<Z> x n = x^n" by (induct n) simp_all
73 qed
75 interpretation int: comm_monoid \<Z>
76   rewrites "finprod \<Z> f A = prod f A"
77 proof -
78   \<comment> \<open>Specification\<close>
79   show "comm_monoid \<Z>" by standard auto
80   then interpret int: comm_monoid \<Z> .
82   \<comment> \<open>Operations\<close>
83   { fix x y have "mult \<Z> x y = x * y" by simp }
84   note mult = this
85   have one: "one \<Z> = 1" by simp
86   show "finprod \<Z> f A = prod f A"
87     by (induct A rule: infinite_finite_induct, auto)
88 qed
90 interpretation int: abelian_monoid \<Z>
91   rewrites int_carrier_eq: "carrier \<Z> = UNIV"
92     and int_zero_eq: "zero \<Z> = 0"
93     and int_add_eq: "add \<Z> x y = x + y"
94     and int_finsum_eq: "finsum \<Z> f A = sum f A"
95 proof -
96   \<comment> \<open>Specification\<close>
97   show "abelian_monoid \<Z>" by standard auto
98   then interpret int: abelian_monoid \<Z> .
100   \<comment> \<open>Carrier\<close>
101   show "carrier \<Z> = UNIV" by simp
103   \<comment> \<open>Operations\<close>
104   { fix x y show "add \<Z> x y = x + y" by simp }
105   note add = this
106   show zero: "zero \<Z> = 0"
107     by simp
108   show "finsum \<Z> f A = sum f A"
109     by (induct A rule: infinite_finite_induct, auto)
110 qed
112 interpretation int: abelian_group \<Z>
113   (* The equations from the interpretation of abelian_monoid need to be repeated.
114      Since the morphisms through which the abelian structures are interpreted are
115      not the identity, the equations of these interpretations are not inherited. *)
116   (* FIXME *)
117   rewrites "carrier \<Z> = UNIV"
118     and "zero \<Z> = 0"
119     and "add \<Z> x y = x + y"
120     and "finsum \<Z> f A = sum f A"
121     and int_a_inv_eq: "a_inv \<Z> x = - x"
122     and int_a_minus_eq: "a_minus \<Z> x y = x - y"
123 proof -
124   \<comment> \<open>Specification\<close>
125   show "abelian_group \<Z>"
126   proof (rule abelian_groupI)
127     fix x
128     assume "x \<in> carrier \<Z>"
129     then show "\<exists>y \<in> carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
130       by simp arith
131   qed auto
132   then interpret int: abelian_group \<Z> .
133   \<comment> \<open>Operations\<close>
134   { fix x y have "add \<Z> x y = x + y" by simp }
135   note add = this
136   have zero: "zero \<Z> = 0" by simp
137   {
138     fix x
139     have "add \<Z> (- x) x = zero \<Z>"
141     then show "a_inv \<Z> x = - x"
142       by (simp add: int.minus_equality)
143   }
144   note a_inv = this
145   show "a_minus \<Z> x y = x - y"
146     by (simp add: int.minus_eq add a_inv)
147 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
149 interpretation int: "domain" \<Z>
150   rewrites "carrier \<Z> = UNIV"
151     and "zero \<Z> = 0"
152     and "add \<Z> x y = x + y"
153     and "finsum \<Z> f A = sum f A"
154     and "a_inv \<Z> x = - x"
155     and "a_minus \<Z> x y = x - y"
156 proof -
157   show "domain \<Z>"
158     by unfold_locales (auto simp: distrib_right distrib_left)
159 qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
162 text \<open>Removal of occurrences of @{term UNIV} in interpretation result
163   --- experimental.\<close>
165 lemma UNIV:
166   "x \<in> UNIV \<longleftrightarrow> True"
167   "A \<subseteq> UNIV \<longleftrightarrow> True"
168   "(\<forall>x \<in> UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
169   "(\<exists>x \<in> UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
170   "(True \<longrightarrow> Q) \<longleftrightarrow> Q"
171   "(True \<Longrightarrow> PROP R) \<equiv> PROP R"
172   by simp_all
174 interpretation int (* FIXME [unfolded UNIV] *) :
175   partial_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
176   rewrites "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV"
177     and "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x \<le> y)"
178     and "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)"
179 proof -
180   show "partial_order \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
181     by standard simp_all
182   show "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV"
183     by simp
184   show "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x \<le> y)"
185     by simp
186   show "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)"
187     by (simp add: lless_def) auto
188 qed
190 interpretation int (* FIXME [unfolded UNIV] *) :
191   lattice "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
192   rewrites "join \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = max x y"
193     and "meet \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = min x y"
194 proof -
195   let ?Z = "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
196   show "lattice ?Z"
197     apply unfold_locales
198     apply (simp add: least_def Upper_def)
199     apply arith
200     apply (simp add: greatest_def Lower_def)
201     apply arith
202     done
203   then interpret int: lattice "?Z" .
204   show "join ?Z x y = max x y"
205     apply (rule int.joinI)
206     apply (simp_all add: least_def Upper_def)
207     apply arith
208     done
209   show "meet ?Z x y = min x y"
210     apply (rule int.meetI)
211     apply (simp_all add: greatest_def Lower_def)
212     apply arith
213     done
214 qed
216 interpretation int (* [unfolded UNIV] *) :
217   total_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
218   by standard clarsimp
221 subsection \<open>Generated Ideals of \<open>\<Z>\<close>\<close>
223 lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
224   apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp
225   apply (simp add: cgenideal_def)
226   done
228 lemma multiples_principalideal: "principalideal {x * a | x. True } \<Z>"
229   by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
231 lemma prime_primeideal:
232   assumes prime: "Factorial_Ring.prime p"
233   shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
234 apply (rule primeidealI)
235    apply (rule int.genideal_ideal, simp)
236   apply (rule int_is_cring)
237  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
238  apply clarsimp defer 1
239  apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
240  apply (elim exE)
241 proof -
242   fix a b x
243   assume "a * b = x * p"
244   then have "p dvd a * b" by simp
245   then have "p dvd a \<or> p dvd b"
246     by (metis prime prime_dvd_mult_eq_int)
247   then show "(\<exists>x. a = x * p) \<or> (\<exists>x. b = x * p)"
248     by (metis dvd_def mult.commute)
249 next
250   assume "UNIV = {uu. \<exists>x. uu = x * p}"
251   then obtain x where "1 = x * p"
252     by best
253   then have "\<bar>p * x\<bar> = 1"
254     by (simp add: ac_simps)
255   then show False using prime
256     by (auto simp add: abs_mult zmult_eq_1_iff)
257 qed
260 subsection \<open>Ideals and Divisibility\<close>
262 lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
263   by (rule int.Idl_subset_ideal') simp_all
265 lemma Idl_subset_eq_dvd: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> l dvd k"
266   apply (subst int_Idl_subset_ideal, subst int_Idl, simp)
267   apply (rule, clarify)
268   apply (simp add: dvd_def)
269   apply (simp add: dvd_def ac_simps)
270   done
272 lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
273 proof -
274   have a: "l dvd k \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})"
275     by (rule Idl_subset_eq_dvd[symmetric])
276   have b: "k dvd l \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})"
277     by (rule Idl_subset_eq_dvd[symmetric])
279   have "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<and> Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k}"
280     by (subst a, subst b, simp)
281   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} \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
282     by blast
283   finally show ?thesis .
284 qed
286 lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
287   apply (subst dvds_eq_abseq[symmetric])
288   apply (rule dvds_eq_Idl[symmetric])
289   done
292 subsection \<open>Ideals and the Modulus\<close>
294 definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set"
295   where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
297 lemmas ZMod_defs =
298   ZMod_def genideal_def
300 lemma rcos_zfact:
301   assumes kIl: "k \<in> ZMod l r"
302   shows "\<exists>x. k = x * l + r"
303 proof -
304   from kIl[unfolded ZMod_def] have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r"
305     by (simp add: a_r_coset_defs)
306   then obtain xl where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" and k: "k = xl + r"
307     by auto
308   from xl obtain x where "xl = x * l"
309     by (auto simp: int_Idl)
310   with k have "k = x * l + r"
311     by simp
312   then show "\<exists>x. k = x * l + r" ..
313 qed
315 lemma ZMod_imp_zmod:
316   assumes zmods: "ZMod m a = ZMod m b"
317   shows "a mod m = b mod m"
318 proof -
319   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
320     by (rule int.genideal_ideal) fast
321   from zmods have "b \<in> ZMod m a"
322     unfolding ZMod_def by (simp add: a_repr_independenceD)
323   then have "\<exists>x. b = x * m + a"
324     by (rule rcos_zfact)
325   then obtain x where "b = x * m + a"
326     by fast
327   then have "b mod m = (x * m + a) mod m"
328     by simp
329   also have "\<dots> = ((x * m) mod m) + (a mod m)"
331   also have "\<dots> = a mod m"
332     by simp
333   finally have "b mod m = a mod m" .
334   then show "a mod m = b mod m" ..
335 qed
337 lemma ZMod_mod: "ZMod m a = ZMod m (a mod m)"
338 proof -
339   interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
340     by (rule int.genideal_ideal) fast
341   show ?thesis
342     unfolding ZMod_def
343     apply (rule a_repr_independence'[symmetric])
344     apply (simp add: int_Idl a_r_coset_defs)
345   proof -
346     have "a = m * (a div m) + (a mod m)"
347       by (simp add: mult_div_mod_eq [symmetric])
348     then have "a = (a div m) * m + (a mod m)"
349       by simp
350     then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m"
351       by fast
352   qed simp
353 qed
355 lemma zmod_imp_ZMod:
356   assumes modeq: "a mod m = b mod m"
357   shows "ZMod m a = ZMod m b"
358 proof -
359   have "ZMod m a = ZMod m (a mod m)"
360     by (rule ZMod_mod)
361   also have "\<dots> = ZMod m (b mod m)"
362     by (simp add: modeq[symmetric])
363   also have "\<dots> = ZMod m b"
364     by (rule ZMod_mod[symmetric])
365   finally show ?thesis .
366 qed
368 corollary ZMod_eq_mod: "ZMod m a = ZMod m b \<longleftrightarrow> a mod m = b mod m"
369   apply (rule iffI)
370   apply (erule ZMod_imp_zmod)
371   apply (erule zmod_imp_ZMod)
372   done
375 subsection \<open>Factorization\<close>
377 definition ZFact :: "int \<Rightarrow> int set ring"
378   where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
380 lemmas ZFact_defs = ZFact_def FactRing_def
382 lemma ZFact_is_cring: "cring (ZFact k)"
383   apply (unfold ZFact_def)
384   apply (rule ideal.quotient_is_cring)
385    apply (intro ring.genideal_ideal)
386     apply (simp add: cring.axioms[OF int_is_cring] ring.intro)
387    apply simp
388   apply (rule int_is_cring)
389   done
391 lemma ZFact_zero: "carrier (ZFact 0) = (\<Union>a. {{a}})"
392   apply (insert int.genideal_zero)
393   apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def)
394   done
396 lemma ZFact_one: "carrier (ZFact 1) = {UNIV}"
397   apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps)
398   apply (subst int.genideal_one)
399   apply (rule, rule, clarsimp)
400    apply (rule, rule, clarsimp)
401    apply (rule, clarsimp, arith)
402   apply (rule, clarsimp)
403   apply (rule exI[of _ "0"], clarsimp)
404   done
406 lemma ZFact_prime_is_domain:
407   assumes pprime: "Factorial_Ring.prime p"
408   shows "domain (ZFact p)"
409   apply (unfold ZFact_def)
410   apply (rule primeideal.quotient_is_domain)
411   apply (rule prime_primeideal[OF pprime])
412   done
414 end