-
Notifications
You must be signed in to change notification settings - Fork 0
/
IntRing.thy
373 lines (316 loc) · 13.2 KB
/
IntRing.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
(* Title: HOL/Algebra/IntRing.thy
Author: Stephan Hohe, TU Muenchen
Author: Clemens Ballarin
*)
theory IntRing
imports "HOL-Computational_Algebra.Primes" QuotRing Lattice
begin
section \<open>The Ring of Integers\<close>
subsection \<open>Some properties of @{typ int}\<close>
lemma dvds_eq_abseq:
fixes k :: int
shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
by (metis dvd_if_abs_eq lcm.commute lcm_proj1_iff_int)
subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close>
abbreviation int_ring :: "int ring" ("\<Z>")
where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = ( * ), one = 1, zero = 0, add = (+)\<rparr>"
lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>"
by simp
lemma int_is_cring: "cring \<Z>"
proof (rule cringI)
show "abelian_group \<Z>"
by (rule abelian_groupI) (auto intro: left_minus)
show "Group.comm_monoid \<Z>"
by (simp add: Group.monoid.intro monoid.monoid_comm_monoidI)
qed (auto simp: distrib_right)
subsection \<open>Interpretations\<close>
text \<open>Since definitions of derived operations are global, their
interpretation needs to be done as early as possible --- that is,
with as few assumptions as possible.\<close>
interpretation int: monoid \<Z>
rewrites "carrier \<Z> = UNIV"
and "mult \<Z> x y = x * y"
and "one \<Z> = 1"
and "pow \<Z> x n = x^n"
proof -
\<comment> \<open>Specification\<close>
show "monoid \<Z>" by standard auto
then interpret int: monoid \<Z> .
\<comment> \<open>Carrier\<close>
show "carrier \<Z> = UNIV" by simp
\<comment> \<open>Operations\<close>
{ fix x y show "mult \<Z> x y = x * y" by simp }
show "one \<Z> = 1" by simp
show "pow \<Z> x n = x^n" by (induct n) simp_all
qed
interpretation int: comm_monoid \<Z>
rewrites "finprod \<Z> f A = prod f A"
proof -
\<comment> \<open>Specification\<close>
show "comm_monoid \<Z>" by standard auto
then interpret int: comm_monoid \<Z> .
\<comment> \<open>Operations\<close>
{ fix x y have "mult \<Z> x y = x * y" by simp }
note mult = this
have one: "one \<Z> = 1" by simp
show "finprod \<Z> f A = prod f A"
by (induct A rule: infinite_finite_induct, auto)
qed
interpretation int: abelian_monoid \<Z>
rewrites int_carrier_eq: "carrier \<Z> = UNIV"
and int_zero_eq: "zero \<Z> = 0"
and int_add_eq: "add \<Z> x y = x + y"
and int_finsum_eq: "finsum \<Z> f A = sum f A"
proof -
\<comment> \<open>Specification\<close>
show "abelian_monoid \<Z>" by standard auto
then interpret int: abelian_monoid \<Z> .
\<comment> \<open>Carrier\<close>
show "carrier \<Z> = UNIV" by simp
\<comment> \<open>Operations\<close>
{ fix x y show "add \<Z> x y = x + y" by simp }
note add = this
show zero: "zero \<Z> = 0"
by simp
show "finsum \<Z> f A = sum f A"
by (induct A rule: infinite_finite_induct, auto)
qed
interpretation int: abelian_group \<Z>
(* The equations from the interpretation of abelian_monoid need to be repeated.
Since the morphisms through which the abelian structures are interpreted are
not the identity, the equations of these interpretations are not inherited. *)
(* FIXME *)
rewrites "carrier \<Z> = UNIV"
and "zero \<Z> = 0"
and "add \<Z> x y = x + y"
and "finsum \<Z> f A = sum f A"
and int_a_inv_eq: "a_inv \<Z> x = - x"
and int_a_minus_eq: "a_minus \<Z> x y = x - y"
proof -
\<comment> \<open>Specification\<close>
show "abelian_group \<Z>"
proof (rule abelian_groupI)
fix x
assume "x \<in> carrier \<Z>"
then show "\<exists>y \<in> carrier \<Z>. y \<oplus>\<^bsub>\<Z>\<^esub> x = \<zero>\<^bsub>\<Z>\<^esub>"
by simp arith
qed auto
then interpret int: abelian_group \<Z> .
\<comment> \<open>Operations\<close>
{ fix x y have "add \<Z> x y = x + y" by simp }
note add = this
have zero: "zero \<Z> = 0" by simp
{
fix x
have "add \<Z> (- x) x = zero \<Z>"
by (simp add: add zero)
then show "a_inv \<Z> x = - x"
by (simp add: int.minus_equality)
}
note a_inv = this
show "a_minus \<Z> x y = x - y"
by (simp add: int.minus_eq add a_inv)
qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+
interpretation int: "domain" \<Z>
rewrites "carrier \<Z> = UNIV"
and "zero \<Z> = 0"
and "add \<Z> x y = x + y"
and "finsum \<Z> f A = sum f A"
and "a_inv \<Z> x = - x"
and "a_minus \<Z> x y = x - y"
proof -
show "domain \<Z>"
by unfold_locales (auto simp: distrib_right distrib_left)
qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq int_a_inv_eq int_a_minus_eq)+
text \<open>Removal of occurrences of @{term UNIV} in interpretation result
--- experimental.\<close>
lemma UNIV:
"x \<in> UNIV \<longleftrightarrow> True"
"A \<subseteq> UNIV \<longleftrightarrow> True"
"(\<forall>x \<in> UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)"
"(\<exists>x \<in> UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)"
"(True \<longrightarrow> Q) \<longleftrightarrow> Q"
"(True \<Longrightarrow> PROP R) \<equiv> PROP R"
by simp_all
interpretation int (* FIXME [unfolded UNIV] *) :
partial_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
rewrites "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV"
and "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x \<le> y)"
and "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)"
proof -
show "partial_order \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
by standard simp_all
show "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV"
by simp
show "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x \<le> y)"
by simp
show "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)"
by (simp add: lless_def) auto
qed
interpretation int (* FIXME [unfolded UNIV] *) :
lattice "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
rewrites "join \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = max x y"
and "meet \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = min x y"
proof -
let ?Z = "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
show "lattice ?Z"
apply unfold_locales
apply (simp_all add: least_def Upper_def greatest_def Lower_def)
apply arith+
done
then interpret int: lattice "?Z" .
show "join ?Z x y = max x y"
by (metis int.le_iff_meet iso_tuple_UNIV_I join_comm linear max.absorb_iff2 max_def)
show "meet ?Z x y = min x y"
using int.meet_le int.meet_left int.meet_right by auto
qed
interpretation int (* [unfolded UNIV] *) :
total_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>"
by standard clarsimp
subsection \<open>Generated Ideals of \<open>\<Z>\<close>\<close>
lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}"
by (simp_all add: cgenideal_def int.cgenideal_eq_genideal[symmetric])
lemma multiples_principalideal: "principalideal {x * a | x. True } \<Z>"
by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl)
lemma prime_primeideal:
assumes prime: "Factorial_Ring.prime p"
shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
proof (rule primeidealI)
show "ideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>"
by (rule int.genideal_ideal, simp)
show "cring \<Z>"
by (rule int_is_cring)
have False if "UNIV = {v::int. \<exists>x. v = x * p}"
proof -
from that
obtain i where "1 = i * p"
by (blast intro: elim: )
then show False
using prime by (auto simp add: abs_mult zmult_eq_1_iff)
qed
then show "carrier \<Z> \<noteq> Idl\<^bsub>\<Z>\<^esub> {p}"
by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def)
have "p dvd a \<or> p dvd b" if "a * b = x * p" for a b x
by (simp add: prime prime_dvd_multD that)
then show "\<And>a b. \<lbrakk>a \<in> carrier \<Z>; b \<in> carrier \<Z>; a \<otimes>\<^bsub>\<Z>\<^esub> b \<in> Idl\<^bsub>\<Z>\<^esub> {p}\<rbrakk>
\<Longrightarrow> a \<in> Idl\<^bsub>\<Z>\<^esub> {p} \<or> b \<in> Idl\<^bsub>\<Z>\<^esub> {p}"
by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def dvd_def mult.commute)
qed
subsection \<open>Ideals and Divisibility\<close>
lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})"
by (rule int.Idl_subset_ideal') simp_all
lemma Idl_subset_eq_dvd: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> l dvd k"
by (subst int_Idl_subset_ideal) (auto simp: dvd_def int_Idl)
lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}"
proof -
have a: "l dvd k \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})"
by (rule Idl_subset_eq_dvd[symmetric])
have b: "k dvd l \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})"
by (rule Idl_subset_eq_dvd[symmetric])
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}"
by (subst a, subst b, simp)
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}"
by blast
finally show ?thesis .
qed
lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>"
apply (subst dvds_eq_abseq[symmetric])
apply (rule dvds_eq_Idl[symmetric])
done
subsection \<open>Ideals and the Modulus\<close>
definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set"
where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r"
lemmas ZMod_defs =
ZMod_def genideal_def
lemma rcos_zfact:
assumes kIl: "k \<in> ZMod l r"
shows "\<exists>x. k = x * l + r"
proof -
from kIl[unfolded ZMod_def] have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r"
by (simp add: a_r_coset_defs)
then obtain xl where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" and k: "k = xl + r"
by auto
from xl obtain x where "xl = x * l"
by (auto simp: int_Idl)
with k have "k = x * l + r"
by simp
then show "\<exists>x. k = x * l + r" ..
qed
lemma ZMod_imp_zmod:
assumes zmods: "ZMod m a = ZMod m b"
shows "a mod m = b mod m"
proof -
interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
by (rule int.genideal_ideal) fast
from zmods have "b \<in> ZMod m a"
unfolding ZMod_def by (simp add: a_repr_independenceD)
then have "\<exists>x. b = x * m + a"
by (rule rcos_zfact)
then obtain x where "b = x * m + a"
by fast
then have "b mod m = (x * m + a) mod m"
by simp
also have "\<dots> = ((x * m) mod m) + (a mod m)"
by (simp add: mod_add_eq)
also have "\<dots> = a mod m"
by simp
finally have "b mod m = a mod m" .
then show "a mod m = b mod m" ..
qed
lemma ZMod_mod: "ZMod m a = ZMod m (a mod m)"
proof -
interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z>
by (rule int.genideal_ideal) fast
show ?thesis
unfolding ZMod_def
apply (rule a_repr_independence'[symmetric])
apply (simp add: int_Idl a_r_coset_defs)
proof -
have "a = m * (a div m) + (a mod m)"
by (simp add: mult_div_mod_eq [symmetric])
then have "a = (a div m) * m + (a mod m)"
by simp
then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m"
by fast
qed simp
qed
lemma zmod_imp_ZMod:
assumes modeq: "a mod m = b mod m"
shows "ZMod m a = ZMod m b"
proof -
have "ZMod m a = ZMod m (a mod m)"
by (rule ZMod_mod)
also have "\<dots> = ZMod m (b mod m)"
by (simp add: modeq[symmetric])
also have "\<dots> = ZMod m b"
by (rule ZMod_mod[symmetric])
finally show ?thesis .
qed
corollary ZMod_eq_mod: "ZMod m a = ZMod m b \<longleftrightarrow> a mod m = b mod m"
apply (rule iffI)
apply (erule ZMod_imp_zmod)
apply (erule zmod_imp_ZMod)
done
subsection \<open>Factorization\<close>
definition ZFact :: "int \<Rightarrow> int set ring"
where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})"
lemmas ZFact_defs = ZFact_def FactRing_def
lemma ZFact_is_cring: "cring (ZFact k)"
by (simp add: ZFact_def ideal.quotient_is_cring int.cring_axioms int.genideal_ideal)
lemma ZFact_zero: "carrier (ZFact 0) = (\<Union>a. {{a}})"
by (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int.genideal_zero)
lemma ZFact_one: "carrier (ZFact 1) = {UNIV}"
unfolding ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps int.genideal_one
proof
have "\<And>a b::int. \<exists>x. b = x + a"
by presburger
then show "(\<Union>a::int. {\<Union>h. {h + a}}) \<subseteq> {UNIV}"
by force
then show "{UNIV} \<subseteq> (\<Union>a::int. {\<Union>h. {h + a}})"
by (metis (no_types, lifting) UNIV_I UN_I singletonD singletonI subset_iff)
qed
lemma ZFact_prime_is_domain:
assumes pprime: "Factorial_Ring.prime p"
shows "domain (ZFact p)"
by (simp add: ZFact_def pprime prime_primeideal primeideal.quotient_is_domain)
end