|
1 (* |
|
2 Title: HOL/Algebra/IntRing.thy |
|
3 Id: $Id$ |
|
4 Author: Stephan Hohe, TU Muenchen |
|
5 *) |
|
6 |
|
7 theory IntRing |
|
8 imports QuotRing IntDef |
|
9 begin |
|
10 |
|
11 |
|
12 section {* The Ring of Integers *} |
|
13 |
|
14 subsection {* Some properties of @{typ int} *} |
|
15 |
|
16 lemma dvds_imp_abseq: |
|
17 "\<lbrakk>l dvd k; k dvd l\<rbrakk> \<Longrightarrow> abs l = abs (k::int)" |
|
18 apply (subst abs_split, rule conjI) |
|
19 apply (clarsimp, subst abs_split, rule conjI) |
|
20 apply (clarsimp) |
|
21 apply (cases "k=0", simp) |
|
22 apply (cases "l=0", simp) |
|
23 apply (simp add: zdvd_anti_sym) |
|
24 apply clarsimp |
|
25 apply (cases "k=0", simp) |
|
26 apply (simp add: zdvd_anti_sym) |
|
27 apply (clarsimp, subst abs_split, rule conjI) |
|
28 apply (clarsimp) |
|
29 apply (cases "l=0", simp) |
|
30 apply (simp add: zdvd_anti_sym) |
|
31 apply (clarsimp) |
|
32 apply (subgoal_tac "-l = -k", simp) |
|
33 apply (intro zdvd_anti_sym, simp+) |
|
34 done |
|
35 |
|
36 lemma abseq_imp_dvd: |
|
37 assumes a_lk: "abs l = abs (k::int)" |
|
38 shows "l dvd k" |
|
39 proof - |
|
40 from a_lk |
|
41 have "nat (abs l) = nat (abs k)" by simp |
|
42 hence "nat (abs l) dvd nat (abs k)" by simp |
|
43 hence "int (nat (abs l)) dvd k" by (subst int_dvd_iff) |
|
44 hence "abs l dvd k" by simp |
|
45 thus "l dvd k" |
|
46 apply (unfold dvd_def, cases "l<0") |
|
47 defer 1 apply clarsimp |
|
48 proof (clarsimp) |
|
49 fix k |
|
50 assume l0: "l < 0" |
|
51 have "- (l * k) = l * (-k)" by simp |
|
52 thus "\<exists>ka. - (l * k) = l * ka" by fast |
|
53 qed |
|
54 qed |
|
55 |
|
56 lemma dvds_eq_abseq: |
|
57 "(l dvd k \<and> k dvd l) = (abs l = abs (k::int))" |
|
58 apply rule |
|
59 apply (simp add: dvds_imp_abseq) |
|
60 apply (rule conjI) |
|
61 apply (simp add: abseq_imp_dvd)+ |
|
62 done |
|
63 |
|
64 |
|
65 |
|
66 subsection {* The Set of Integers as Algebraic Structure *} |
|
67 |
|
68 subsubsection {* Definition of @{text "\<Z>"} *} |
|
69 |
|
70 constdefs |
|
71 int_ring :: "int ring" ("\<Z>") |
|
72 "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>" |
|
73 |
|
74 int_order :: "int order" |
|
75 "int_order \<equiv> \<lparr>carrier = UNIV, le = op \<le>\<rparr>" |
|
76 |
|
77 lemma int_Zcarr[simp,intro!]: |
|
78 "k \<in> carrier \<Z>" |
|
79 by (simp add: int_ring_def) |
|
80 |
|
81 lemma int_is_cring: |
|
82 "cring \<Z>" |
|
83 unfolding int_ring_def |
|
84 apply (rule cringI) |
|
85 apply (rule abelian_groupI, simp_all) |
|
86 defer 1 |
|
87 apply (rule comm_monoidI, simp_all) |
|
88 apply (rule zadd_zmult_distrib) |
|
89 apply (fast intro: zadd_zminus_inverse2) |
|
90 done |
|
91 |
|
92 lemma int_is_domain: |
|
93 "domain \<Z>" |
|
94 apply (intro domain.intro domain_axioms.intro) |
|
95 apply (rule int_is_cring) |
|
96 apply (unfold int_ring_def, simp+) |
|
97 done |
|
98 |
|
99 interpretation "domain" ["\<Z>"] by (rule int_is_domain) |
|
100 |
|
101 lemma int_le_total_order: |
|
102 "total_order int_order" |
|
103 unfolding int_order_def |
|
104 apply (rule partial_order.total_orderI) |
|
105 apply (rule partial_order.intro, simp+) |
|
106 apply clarsimp |
|
107 done |
|
108 |
|
109 interpretation total_order ["int_order"] by (rule int_le_total_order) |
|
110 |
|
111 |
|
112 subsubsection {* Generated Ideals of @{text "\<Z>"} *} |
|
113 |
|
114 lemma int_Idl: |
|
115 "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}" |
|
116 apply (subst cgenideal_eq_genideal[symmetric], simp add: int_ring_def) |
|
117 apply (simp add: cgenideal_def int_ring_def) |
|
118 done |
|
119 |
|
120 lemma multiples_principalideal: |
|
121 "principalideal {x * a | x. True } \<Z>" |
|
122 apply (subst int_Idl[symmetric], rule principalidealI) |
|
123 apply (rule genideal_ideal, simp) |
|
124 apply fast |
|
125 done |
|
126 |
|
127 lemma prime_primeideal: |
|
128 assumes prime: "prime (nat p)" |
|
129 shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>" |
|
130 apply (rule primeidealI) |
|
131 apply (rule genideal_ideal, simp) |
|
132 apply (rule int_is_cring) |
|
133 apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def) |
|
134 apply (simp add: int_ring_def) |
|
135 apply clarsimp defer 1 |
|
136 apply (simp add: cgenideal_eq_genideal[symmetric] cgenideal_def) |
|
137 apply (simp add: int_ring_def) |
|
138 apply (elim exE) |
|
139 proof - |
|
140 fix a b x |
|
141 |
|
142 from prime |
|
143 have ppos: "0 <= p" by (simp add: prime_def) |
|
144 have unnat: "!!x. nat p dvd nat (abs x) ==> p dvd x" |
|
145 proof - |
|
146 fix x |
|
147 assume "nat p dvd nat (abs x)" |
|
148 hence "int (nat p) dvd x" by (simp add: int_dvd_iff[symmetric]) |
|
149 thus "p dvd x" by (simp add: ppos) |
|
150 qed |
|
151 |
|
152 |
|
153 assume "a * b = x * p" |
|
154 hence "p dvd a * b" by simp |
|
155 hence "nat p dvd nat (abs (a * b))" |
|
156 apply (subst nat_dvd_iff, clarsimp) |
|
157 apply (rule conjI, clarsimp, simp add: zabs_def) |
|
158 proof (clarsimp) |
|
159 assume a: " ~ 0 <= p" |
|
160 from prime |
|
161 have "0 < p" by (simp add: prime_def) |
|
162 from a and this |
|
163 have "False" by simp |
|
164 thus "nat (abs (a * b)) = 0" .. |
|
165 qed |
|
166 hence "nat p dvd (nat (abs a) * nat (abs b))" by (simp add: nat_abs_mult_distrib) |
|
167 hence "nat p dvd nat (abs a) | nat p dvd nat (abs b)" by (rule prime_dvd_mult[OF prime]) |
|
168 hence "p dvd a | p dvd b" by (fast intro: unnat) |
|
169 thus "(EX x. a = x * p) | (EX x. b = x * p)" |
|
170 proof |
|
171 assume "p dvd a" |
|
172 hence "EX x. a = p * x" by (simp add: dvd_def) |
|
173 from this obtain x |
|
174 where "a = p * x" by fast |
|
175 hence "a = x * p" by simp |
|
176 hence "EX x. a = x * p" by simp |
|
177 thus "(EX x. a = x * p) | (EX x. b = x * p)" .. |
|
178 next |
|
179 assume "p dvd b" |
|
180 hence "EX x. b = p * x" by (simp add: dvd_def) |
|
181 from this obtain x |
|
182 where "b = p * x" by fast |
|
183 hence "b = x * p" by simp |
|
184 hence "EX x. b = x * p" by simp |
|
185 thus "(EX x. a = x * p) | (EX x. b = x * p)" .. |
|
186 qed |
|
187 next |
|
188 assume "UNIV = {uu. EX x. uu = x * p}" |
|
189 from this obtain x |
|
190 where "1 = x * p" by fast |
|
191 from this [symmetric] |
|
192 have "p * x = 1" by (subst zmult_commute) |
|
193 hence "\<bar>p * x\<bar> = 1" by simp |
|
194 hence "\<bar>p\<bar> = 1" by (rule abs_zmult_eq_1) |
|
195 from this and prime |
|
196 show "False" by (simp add: prime_def) |
|
197 qed |
|
198 |
|
199 |
|
200 subsubsection {* Ideals and Divisibility *} |
|
201 |
|
202 lemma int_Idl_subset_ideal: |
|
203 "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})" |
|
204 by (rule Idl_subset_ideal', simp+) |
|
205 |
|
206 lemma Idl_subset_eq_dvd: |
|
207 "(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)" |
|
208 apply (subst int_Idl_subset_ideal, subst int_Idl, simp) |
|
209 apply (rule, clarify) |
|
210 apply (simp add: dvd_def, clarify) |
|
211 apply (simp add: m_comm) |
|
212 done |
|
213 |
|
214 lemma dvds_eq_Idl: |
|
215 "(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})" |
|
216 proof - |
|
217 have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric]) |
|
218 have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric]) |
|
219 |
|
220 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}))" |
|
221 by (subst a, subst b, simp) |
|
222 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+) |
|
223 finally |
|
224 show ?thesis . |
|
225 qed |
|
226 |
|
227 lemma Idl_eq_abs: |
|
228 "(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)" |
|
229 apply (subst dvds_eq_abseq[symmetric]) |
|
230 apply (rule dvds_eq_Idl[symmetric]) |
|
231 done |
|
232 |
|
233 |
|
234 subsubsection {* Ideals and the Modulus *} |
|
235 |
|
236 constdefs |
|
237 ZMod :: "int => int => int set" |
|
238 "ZMod k r == (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r" |
|
239 |
|
240 lemmas ZMod_defs = |
|
241 ZMod_def genideal_def |
|
242 |
|
243 lemma rcos_zfact: |
|
244 assumes kIl: "k \<in> ZMod l r" |
|
245 shows "EX x. k = x * l + r" |
|
246 proof - |
|
247 from kIl[unfolded ZMod_def] |
|
248 have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs int_ring_def) |
|
249 from this obtain xl |
|
250 where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" |
|
251 and k: "k = xl + r" |
|
252 by auto |
|
253 from xl obtain x |
|
254 where "xl = x * l" |
|
255 by (simp add: int_Idl, fast) |
|
256 from k and this |
|
257 have "k = x * l + r" by simp |
|
258 thus "\<exists>x. k = x * l + r" .. |
|
259 qed |
|
260 |
|
261 lemma ZMod_imp_zmod: |
|
262 assumes zmods: "ZMod m a = ZMod m b" |
|
263 shows "a mod m = b mod m" |
|
264 proof - |
|
265 interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast) |
|
266 from zmods |
|
267 have "b \<in> ZMod m a" |
|
268 unfolding ZMod_def |
|
269 by (simp add: a_repr_independenceD) |
|
270 from this |
|
271 have "EX x. b = x * m + a" by (rule rcos_zfact) |
|
272 from this obtain x |
|
273 where "b = x * m + a" |
|
274 by fast |
|
275 |
|
276 hence "b mod m = (x * m + a) mod m" by simp |
|
277 also |
|
278 have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: zmod_zadd1_eq) |
|
279 also |
|
280 have "\<dots> = a mod m" by simp |
|
281 finally |
|
282 have "b mod m = a mod m" . |
|
283 thus "a mod m = b mod m" .. |
|
284 qed |
|
285 |
|
286 lemma ZMod_mod: |
|
287 shows "ZMod m a = ZMod m (a mod m)" |
|
288 proof - |
|
289 interpret ideal ["Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>] by (rule genideal_ideal, fast) |
|
290 show ?thesis |
|
291 unfolding ZMod_def |
|
292 apply (rule a_repr_independence'[symmetric]) |
|
293 apply (simp add: int_Idl a_r_coset_defs) |
|
294 apply (simp add: int_ring_def) |
|
295 proof - |
|
296 have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality) |
|
297 hence "a = (a div m) * m + (a mod m)" by simp |
|
298 thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast |
|
299 qed simp |
|
300 qed |
|
301 |
|
302 lemma zmod_imp_ZMod: |
|
303 assumes modeq: "a mod m = b mod m" |
|
304 shows "ZMod m a = ZMod m b" |
|
305 proof - |
|
306 have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod) |
|
307 also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric]) |
|
308 also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric]) |
|
309 finally show ?thesis . |
|
310 qed |
|
311 |
|
312 corollary ZMod_eq_mod: |
|
313 shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)" |
|
314 by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod) |
|
315 |
|
316 |
|
317 subsubsection {* Factorization *} |
|
318 |
|
319 constdefs |
|
320 ZFact :: "int \<Rightarrow> int set ring" |
|
321 "ZFact k == \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})" |
|
322 |
|
323 lemmas ZFact_defs = ZFact_def FactRing_def |
|
324 |
|
325 lemma ZFact_is_cring: |
|
326 shows "cring (ZFact k)" |
|
327 apply (unfold ZFact_def) |
|
328 apply (rule ideal.quotient_is_cring) |
|
329 apply (intro ring.genideal_ideal) |
|
330 apply (simp add: cring.axioms[OF int_is_cring] ring.intro) |
|
331 apply simp |
|
332 apply (rule int_is_cring) |
|
333 done |
|
334 |
|
335 lemma ZFact_zero: |
|
336 "carrier (ZFact 0) = (\<Union>a. {{a}})" |
|
337 apply (insert genideal_zero) |
|
338 apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) |
|
339 done |
|
340 |
|
341 lemma ZFact_one: |
|
342 "carrier (ZFact 1) = {UNIV}" |
|
343 apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def int_ring_def ring_record_simps) |
|
344 apply (subst genideal_one[unfolded int_ring_def, simplified ring_record_simps]) |
|
345 apply (rule, rule, clarsimp) |
|
346 apply (rule, rule, clarsimp) |
|
347 apply (rule, clarsimp, arith) |
|
348 apply (rule, clarsimp) |
|
349 apply (rule exI[of _ "0"], clarsimp) |
|
350 done |
|
351 |
|
352 lemma ZFact_prime_is_domain: |
|
353 assumes pprime: "prime (nat p)" |
|
354 shows "domain (ZFact p)" |
|
355 apply (unfold ZFact_def) |
|
356 apply (rule primeideal.quotient_is_domain) |
|
357 apply (rule prime_primeideal[OF pprime]) |
|
358 done |
|
359 |
|
360 end |