author | haftmann |
Fri, 20 Oct 2017 20:57:55 +0200 | |
changeset 66888 | 930abfdf8727 |
parent 66453 | cc19f7ca2ed6 |
child 67006 | b1278ed3cd46 |
permissions | -rw-r--r-- |
35849 | 1 |
(* Title: HOL/Algebra/IntRing.thy |
2 |
Author: Stephan Hohe, TU Muenchen |
|
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
3 |
Author: Clemens Ballarin |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
4 |
*) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
5 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
6 |
theory IntRing |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
65417
diff
changeset
|
7 |
imports "HOL-Computational_Algebra.Primes" QuotRing Lattice HOL.Int |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
8 |
begin |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
9 |
|
61382 | 10 |
section \<open>The Ring of Integers\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
11 |
|
61382 | 12 |
subsection \<open>Some properties of @{typ int}\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
13 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
14 |
lemma dvds_eq_abseq: |
55991 | 15 |
fixes k :: int |
61945 | 16 |
shows "l dvd k \<and> k dvd l \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
17 |
apply rule |
33657 | 18 |
apply (simp add: zdvd_antisym_abs) |
33676
802f5e233e48
moved lemma from Algebra/IntRing to Ring_and_Field
nipkow
parents:
33657
diff
changeset
|
19 |
apply (simp add: dvd_if_abs_eq) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
20 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
21 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
22 |
|
63167 | 23 |
subsection \<open>\<open>\<Z>\<close>: The Set of Integers as Algebraic Structure\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
24 |
|
55991 | 25 |
abbreviation int_ring :: "int ring" ("\<Z>") |
26 |
where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
27 |
|
55991 | 28 |
lemma int_Zcarr [intro!, simp]: "k \<in> carrier \<Z>" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
29 |
by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
30 |
|
55991 | 31 |
lemma int_is_cring: "cring \<Z>" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
32 |
apply (rule cringI) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
33 |
apply (rule abelian_groupI, simp_all) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
34 |
defer 1 |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
35 |
apply (rule comm_monoidI, simp_all) |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44821
diff
changeset
|
36 |
apply (rule distrib_right) |
44821 | 37 |
apply (fast intro: left_minus) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
38 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
39 |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
40 |
(* |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
41 |
lemma int_is_domain: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
42 |
"domain \<Z>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
43 |
apply (intro domain.intro domain_axioms.intro) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
44 |
apply (rule int_is_cring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
45 |
apply (unfold int_ring_def, simp+) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
46 |
done |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
47 |
*) |
35849 | 48 |
|
49 |
||
61382 | 50 |
subsection \<open>Interpretations\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
51 |
|
61382 | 52 |
text \<open>Since definitions of derived operations are global, their |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
53 |
interpretation needs to be done as early as possible --- that is, |
61382 | 54 |
with as few assumptions as possible.\<close> |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
55 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
56 |
interpretation int: monoid \<Z> |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
57 |
rewrites "carrier \<Z> = UNIV" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
58 |
and "mult \<Z> x y = x * y" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
59 |
and "one \<Z> = 1" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
60 |
and "pow \<Z> x n = x^n" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
61 |
proof - |
63167 | 62 |
\<comment> "Specification" |
61169 | 63 |
show "monoid \<Z>" by standard auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
64 |
then interpret int: monoid \<Z> . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
65 |
|
63167 | 66 |
\<comment> "Carrier" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
67 |
show "carrier \<Z> = UNIV" by simp |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
68 |
|
63167 | 69 |
\<comment> "Operations" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
70 |
{ fix x y show "mult \<Z> x y = x * y" by simp } |
55991 | 71 |
show "one \<Z> = 1" by simp |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
72 |
show "pow \<Z> x n = x^n" by (induct n) simp_all |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
73 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
74 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
75 |
interpretation int: comm_monoid \<Z> |
64272 | 76 |
rewrites "finprod \<Z> f A = prod f A" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
77 |
proof - |
63167 | 78 |
\<comment> "Specification" |
61169 | 79 |
show "comm_monoid \<Z>" by standard auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
80 |
then interpret int: comm_monoid \<Z> . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
81 |
|
63167 | 82 |
\<comment> "Operations" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
83 |
{ fix x y have "mult \<Z> x y = x * y" by simp } |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
84 |
note mult = this |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
85 |
have one: "one \<Z> = 1" by simp |
64272 | 86 |
show "finprod \<Z> f A = prod f A" |
60112
3eab4acaa035
finprod takes 1 in case of infinite sets => remove several "finite A" assumptions
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
57514
diff
changeset
|
87 |
by (induct A rule: infinite_finite_induct, auto) |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
88 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
89 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
90 |
interpretation int: abelian_monoid \<Z> |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
91 |
rewrites int_carrier_eq: "carrier \<Z> = UNIV" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
92 |
and int_zero_eq: "zero \<Z> = 0" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
93 |
and int_add_eq: "add \<Z> x y = x + y" |
64267 | 94 |
and int_finsum_eq: "finsum \<Z> f A = sum f A" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
95 |
proof - |
63167 | 96 |
\<comment> "Specification" |
61169 | 97 |
show "abelian_monoid \<Z>" by standard auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
98 |
then interpret int: abelian_monoid \<Z> . |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
99 |
|
63167 | 100 |
\<comment> "Carrier" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
101 |
show "carrier \<Z> = UNIV" by simp |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
102 |
|
63167 | 103 |
\<comment> "Operations" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
104 |
{ fix x y show "add \<Z> x y = x + y" by simp } |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
105 |
note add = this |
55991 | 106 |
show zero: "zero \<Z> = 0" |
107 |
by simp |
|
64267 | 108 |
show "finsum \<Z> f A = sum f A" |
60112
3eab4acaa035
finprod takes 1 in case of infinite sets => remove several "finite A" assumptions
Rene Thiemann <rene.thiemann@uibk.ac.at>
parents:
57514
diff
changeset
|
109 |
by (induct A rule: infinite_finite_induct, auto) |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
110 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
111 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
112 |
interpretation int: abelian_group \<Z> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
113 |
(* The equations from the interpretation of abelian_monoid need to be repeated. |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
114 |
Since the morphisms through which the abelian structures are interpreted are |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
115 |
not the identity, the equations of these interpretations are not inherited. *) |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
116 |
(* FIXME *) |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
117 |
rewrites "carrier \<Z> = UNIV" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
118 |
and "zero \<Z> = 0" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
119 |
and "add \<Z> x y = x + y" |
64267 | 120 |
and "finsum \<Z> f A = sum f A" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
121 |
and int_a_inv_eq: "a_inv \<Z> x = - x" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
122 |
and int_a_minus_eq: "a_minus \<Z> x y = x - y" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
123 |
proof - |
63167 | 124 |
\<comment> "Specification" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
125 |
show "abelian_group \<Z>" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
126 |
proof (rule abelian_groupI) |
55991 | 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>" |
|
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
130 |
by simp arith |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
131 |
qed auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
132 |
then interpret int: abelian_group \<Z> . |
63167 | 133 |
\<comment> "Operations" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
134 |
{ fix x y have "add \<Z> x y = x + y" by simp } |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
135 |
note add = this |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
136 |
have zero: "zero \<Z> = 0" by simp |
55991 | 137 |
{ |
138 |
fix x |
|
139 |
have "add \<Z> (- x) x = zero \<Z>" |
|
140 |
by (simp add: add zero) |
|
141 |
then show "a_inv \<Z> x = - x" |
|
142 |
by (simp add: int.minus_equality) |
|
143 |
} |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
144 |
note a_inv = this |
55991 | 145 |
show "a_minus \<Z> x y = x - y" |
146 |
by (simp add: int.minus_eq add a_inv) |
|
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
147 |
qed (simp add: int_carrier_eq int_zero_eq int_add_eq int_finsum_eq)+ |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
148 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
149 |
interpretation int: "domain" \<Z> |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
150 |
rewrites "carrier \<Z> = UNIV" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
151 |
and "zero \<Z> = 0" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
152 |
and "add \<Z> x y = x + y" |
64267 | 153 |
and "finsum \<Z> f A = sum f A" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
154 |
and "a_inv \<Z> x = - x" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
155 |
and "a_minus \<Z> x y = x - y" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
156 |
proof - |
55991 | 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)+ |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
160 |
|
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
161 |
|
61382 | 162 |
text \<open>Removal of occurrences of @{term UNIV} in interpretation result |
163 |
--- experimental.\<close> |
|
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
164 |
|
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
165 |
lemma UNIV: |
55991 | 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 |
"(EX x : UNIV. P x) \<longleftrightarrow> (EX x. P x)" |
|
170 |
"(True \<longrightarrow> Q) \<longleftrightarrow> Q" |
|
171 |
"(True \<Longrightarrow> PROP R) \<equiv> PROP R" |
|
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
172 |
by simp_all |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
173 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
174 |
interpretation int (* FIXME [unfolded UNIV] *) : |
55926 | 175 |
partial_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>" |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
176 |
rewrites "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV" |
55926 | 177 |
and "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)" |
178 |
and "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)" |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
179 |
proof - |
55926 | 180 |
show "partial_order \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>" |
61169 | 181 |
by standard simp_all |
55926 | 182 |
show "carrier \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> = UNIV" |
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
183 |
by simp |
55926 | 184 |
show "le \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x \<le> y)" |
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
185 |
by simp |
55926 | 186 |
show "lless \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = (x < y)" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
187 |
by (simp add: lless_def) auto |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
188 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
189 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
190 |
interpretation int (* FIXME [unfolded UNIV] *) : |
55926 | 191 |
lattice "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>" |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
192 |
rewrites "join \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = max x y" |
55926 | 193 |
and "meet \<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr> x y = min x y" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
194 |
proof - |
55926 | 195 |
let ?Z = "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
196 |
show "lattice ?Z" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
197 |
apply unfold_locales |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
198 |
apply (simp add: least_def Upper_def) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
199 |
apply arith |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
200 |
apply (simp add: greatest_def Lower_def) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
201 |
apply arith |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
202 |
done |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
203 |
then interpret int: lattice "?Z" . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
204 |
show "join ?Z x y = max x y" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
205 |
apply (rule int.joinI) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
206 |
apply (simp_all add: least_def Upper_def) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
207 |
apply arith |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
208 |
done |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
209 |
show "meet ?Z x y = min x y" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
210 |
apply (rule int.meetI) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
211 |
apply (simp_all add: greatest_def Lower_def) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
212 |
apply arith |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
213 |
done |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
214 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
215 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
216 |
interpretation int (* [unfolded UNIV] *) : |
55926 | 217 |
total_order "\<lparr>carrier = UNIV::int set, eq = op =, le = op \<le>\<rparr>" |
61169 | 218 |
by standard clarsimp |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
219 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
220 |
|
63167 | 221 |
subsection \<open>Generated Ideals of \<open>\<Z>\<close>\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
222 |
|
55991 | 223 |
lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
224 |
apply (subst int.cgenideal_eq_genideal[symmetric]) apply simp |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
225 |
apply (simp add: cgenideal_def) |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
226 |
done |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
227 |
|
55991 | 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) |
|
29700 | 230 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
231 |
lemma prime_primeideal: |
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55157
diff
changeset
|
232 |
assumes prime: "prime p" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
233 |
shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
234 |
apply (rule primeidealI) |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
235 |
apply (rule int.genideal_ideal, simp) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
236 |
apply (rule int_is_cring) |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
237 |
apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
238 |
apply clarsimp defer 1 |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
239 |
apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
240 |
apply (elim exE) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
241 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
242 |
fix a b x |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63167
diff
changeset
|
243 |
assume "a * b = x * p" |
55991 | 244 |
then have "p dvd a * b" by simp |
245 |
then have "p dvd a \<or> p dvd b" |
|
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55157
diff
changeset
|
246 |
by (metis prime prime_dvd_mult_eq_int) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63167
diff
changeset
|
247 |
then show "(\<exists>x. a = x * p) \<or> (\<exists>x. b = x * p)" |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55991
diff
changeset
|
248 |
by (metis dvd_def mult.commute) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
249 |
next |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63167
diff
changeset
|
250 |
assume "UNIV = {uu. EX x. uu = x * p}" |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63167
diff
changeset
|
251 |
then obtain x where "1 = x * p" by best |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63167
diff
changeset
|
252 |
then have "\<bar>p * x\<bar> = 1" by (simp add: mult.commute) |
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63167
diff
changeset
|
253 |
then show False using prime |
63633 | 254 |
by (auto dest!: abs_zmult_eq_1 simp: prime_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
255 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
256 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
257 |
|
61382 | 258 |
subsection \<open>Ideals and Divisibility\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
259 |
|
55991 | 260 |
lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})" |
261 |
by (rule int.Idl_subset_ideal') simp_all |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
262 |
|
55991 | 263 |
lemma Idl_subset_eq_dvd: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> l dvd k" |
264 |
apply (subst int_Idl_subset_ideal, subst int_Idl, simp) |
|
265 |
apply (rule, clarify) |
|
266 |
apply (simp add: dvd_def) |
|
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
267 |
apply (simp add: dvd_def ac_simps) |
55991 | 268 |
done |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
269 |
|
55991 | 270 |
lemma dvds_eq_Idl: "l dvd k \<and> k dvd l \<longleftrightarrow> Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
271 |
proof - |
55991 | 272 |
have a: "l dvd k \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" |
273 |
by (rule Idl_subset_eq_dvd[symmetric]) |
|
274 |
have b: "k dvd l \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" |
|
275 |
by (rule Idl_subset_eq_dvd[symmetric]) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
276 |
|
55991 | 277 |
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}" |
278 |
by (subst a, subst b, simp) |
|
279 |
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}" |
|
280 |
by blast |
|
281 |
finally show ?thesis . |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
282 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
283 |
|
61945 | 284 |
lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>" |
55991 | 285 |
apply (subst dvds_eq_abseq[symmetric]) |
286 |
apply (rule dvds_eq_Idl[symmetric]) |
|
287 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
288 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
289 |
|
61382 | 290 |
subsection \<open>Ideals and the Modulus\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
291 |
|
55991 | 292 |
definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set" |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
293 |
where "ZMod k r = (Idl\<^bsub>\<Z>\<^esub> {k}) +>\<^bsub>\<Z>\<^esub> r" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
294 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
295 |
lemmas ZMod_defs = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
296 |
ZMod_def genideal_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
297 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
298 |
lemma rcos_zfact: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
299 |
assumes kIl: "k \<in> ZMod l r" |
55991 | 300 |
shows "\<exists>x. k = x * l + r" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
301 |
proof - |
55991 | 302 |
from kIl[unfolded ZMod_def] have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" |
303 |
by (simp add: a_r_coset_defs) |
|
304 |
then obtain xl where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" and k: "k = xl + r" |
|
305 |
by auto |
|
306 |
from xl obtain x where "xl = x * l" |
|
307 |
by (auto simp: int_Idl) |
|
308 |
with k have "k = x * l + r" |
|
309 |
by simp |
|
310 |
then show "\<exists>x. k = x * l + r" .. |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
311 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
312 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
313 |
lemma ZMod_imp_zmod: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
314 |
assumes zmods: "ZMod m a = ZMod m b" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
315 |
shows "a mod m = b mod m" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
316 |
proof - |
55991 | 317 |
interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> |
318 |
by (rule int.genideal_ideal) fast |
|
319 |
from zmods have "b \<in> ZMod m a" |
|
320 |
unfolding ZMod_def by (simp add: a_repr_independenceD) |
|
321 |
then have "\<exists>x. b = x * m + a" |
|
322 |
by (rule rcos_zfact) |
|
323 |
then obtain x where "b = x * m + a" |
|
324 |
by fast |
|
325 |
then have "b mod m = (x * m + a) mod m" |
|
326 |
by simp |
|
327 |
also have "\<dots> = ((x * m) mod m) + (a mod m)" |
|
328 |
by (simp add: mod_add_eq) |
|
329 |
also have "\<dots> = a mod m" |
|
330 |
by simp |
|
331 |
finally have "b mod m = a mod m" . |
|
332 |
then show "a mod m = b mod m" .. |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
333 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
334 |
|
55991 | 335 |
lemma ZMod_mod: "ZMod m a = ZMod m (a mod m)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
336 |
proof - |
55991 | 337 |
interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> |
338 |
by (rule int.genideal_ideal) fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
339 |
show ?thesis |
55991 | 340 |
unfolding ZMod_def |
341 |
apply (rule a_repr_independence'[symmetric]) |
|
342 |
apply (simp add: int_Idl a_r_coset_defs) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
343 |
proof - |
55991 | 344 |
have "a = m * (a div m) + (a mod m)" |
64246 | 345 |
by (simp add: mult_div_mod_eq [symmetric]) |
55991 | 346 |
then have "a = (a div m) * m + (a mod m)" |
347 |
by simp |
|
348 |
then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" |
|
349 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
350 |
qed simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
351 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
352 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
353 |
lemma zmod_imp_ZMod: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
354 |
assumes modeq: "a mod m = b mod m" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
355 |
shows "ZMod m a = ZMod m b" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
356 |
proof - |
55991 | 357 |
have "ZMod m a = ZMod m (a mod m)" |
358 |
by (rule ZMod_mod) |
|
359 |
also have "\<dots> = ZMod m (b mod m)" |
|
360 |
by (simp add: modeq[symmetric]) |
|
361 |
also have "\<dots> = ZMod m b" |
|
362 |
by (rule ZMod_mod[symmetric]) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
363 |
finally show ?thesis . |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
364 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
365 |
|
55991 | 366 |
corollary ZMod_eq_mod: "ZMod m a = ZMod m b \<longleftrightarrow> a mod m = b mod m" |
367 |
apply (rule iffI) |
|
368 |
apply (erule ZMod_imp_zmod) |
|
369 |
apply (erule zmod_imp_ZMod) |
|
370 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
371 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
372 |
|
61382 | 373 |
subsection \<open>Factorization\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
374 |
|
55991 | 375 |
definition ZFact :: "int \<Rightarrow> int set ring" |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
376 |
where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
377 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
378 |
lemmas ZFact_defs = ZFact_def FactRing_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
379 |
|
55991 | 380 |
lemma ZFact_is_cring: "cring (ZFact k)" |
381 |
apply (unfold ZFact_def) |
|
382 |
apply (rule ideal.quotient_is_cring) |
|
383 |
apply (intro ring.genideal_ideal) |
|
384 |
apply (simp add: cring.axioms[OF int_is_cring] ring.intro) |
|
385 |
apply simp |
|
386 |
apply (rule int_is_cring) |
|
387 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
388 |
|
55991 | 389 |
lemma ZFact_zero: "carrier (ZFact 0) = (\<Union>a. {{a}})" |
390 |
apply (insert int.genideal_zero) |
|
391 |
apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def) |
|
392 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
393 |
|
55991 | 394 |
lemma ZFact_one: "carrier (ZFact 1) = {UNIV}" |
395 |
apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps) |
|
396 |
apply (subst int.genideal_one) |
|
397 |
apply (rule, rule, clarsimp) |
|
398 |
apply (rule, rule, clarsimp) |
|
399 |
apply (rule, clarsimp, arith) |
|
400 |
apply (rule, clarsimp) |
|
401 |
apply (rule exI[of _ "0"], clarsimp) |
|
402 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
403 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
404 |
lemma ZFact_prime_is_domain: |
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55157
diff
changeset
|
405 |
assumes pprime: "prime p" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
406 |
shows "domain (ZFact p)" |
55991 | 407 |
apply (unfold ZFact_def) |
408 |
apply (rule primeideal.quotient_is_domain) |
|
409 |
apply (rule prime_primeideal[OF pprime]) |
|
410 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
411 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
412 |
end |