author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 69064 | 5840724b1d71 |
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 |
68399
0b71d08528f0
resolution of name clashes in Algebra
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
7 |
imports "HOL-Computational_Algebra.Primes" QuotRing Lattice |
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 |
|
69597 | 12 |
subsection \<open>Some properties of \<^typ>\<open>int\<close>\<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>" |
68561 | 17 |
by (metis dvd_if_abs_eq lcm.commute lcm_proj1_iff_int) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
18 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
19 |
|
63167 | 20 |
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
|
21 |
|
55991 | 22 |
abbreviation int_ring :: "int ring" ("\<Z>") |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68561
diff
changeset
|
23 |
where "int_ring \<equiv> \<lparr>carrier = UNIV, mult = (*), one = 1, zero = 0, add = (+)\<rparr>" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
24 |
|
55991 | 25 |
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
|
26 |
by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
27 |
|
55991 | 28 |
lemma int_is_cring: "cring \<Z>" |
68561 | 29 |
proof (rule cringI) |
30 |
show "abelian_group \<Z>" |
|
31 |
by (rule abelian_groupI) (auto intro: left_minus) |
|
32 |
show "Group.comm_monoid \<Z>" |
|
33 |
by (simp add: Group.monoid.intro monoid.monoid_comm_monoidI) |
|
34 |
qed (auto simp: distrib_right) |
|
35849 | 35 |
|
36 |
||
61382 | 37 |
subsection \<open>Interpretations\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
38 |
|
61382 | 39 |
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
|
40 |
interpretation needs to be done as early as possible --- that is, |
61382 | 41 |
with as few assumptions as possible.\<close> |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
42 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
43 |
interpretation int: monoid \<Z> |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
44 |
rewrites "carrier \<Z> = UNIV" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
45 |
and "mult \<Z> x y = x * y" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
46 |
and "one \<Z> = 1" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
47 |
and "pow \<Z> x n = x^n" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
48 |
proof - |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
49 |
\<comment> \<open>Specification\<close> |
61169 | 50 |
show "monoid \<Z>" by standard auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
51 |
then interpret int: monoid \<Z> . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
52 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
53 |
\<comment> \<open>Carrier\<close> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
54 |
show "carrier \<Z> = UNIV" by simp |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
55 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
56 |
\<comment> \<open>Operations\<close> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
57 |
{ fix x y show "mult \<Z> x y = x * y" by simp } |
55991 | 58 |
show "one \<Z> = 1" by simp |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
59 |
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
|
60 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
61 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
62 |
interpretation int: comm_monoid \<Z> |
64272 | 63 |
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
|
64 |
proof - |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
65 |
\<comment> \<open>Specification\<close> |
61169 | 66 |
show "comm_monoid \<Z>" by standard auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
67 |
then interpret int: comm_monoid \<Z> . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
68 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
69 |
\<comment> \<open>Operations\<close> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
70 |
{ 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
|
71 |
note mult = this |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
72 |
have one: "one \<Z> = 1" by simp |
64272 | 73 |
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
|
74 |
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
|
75 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
76 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
77 |
interpretation int: abelian_monoid \<Z> |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
78 |
rewrites int_carrier_eq: "carrier \<Z> = UNIV" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
79 |
and int_zero_eq: "zero \<Z> = 0" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
80 |
and int_add_eq: "add \<Z> x y = x + y" |
64267 | 81 |
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
|
82 |
proof - |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
83 |
\<comment> \<open>Specification\<close> |
61169 | 84 |
show "abelian_monoid \<Z>" by standard auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
85 |
then interpret int: abelian_monoid \<Z> . |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
86 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
87 |
\<comment> \<open>Carrier\<close> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
88 |
show "carrier \<Z> = UNIV" by simp |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
89 |
|
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
90 |
\<comment> \<open>Operations\<close> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
91 |
{ 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
|
92 |
note add = this |
55991 | 93 |
show zero: "zero \<Z> = 0" |
94 |
by simp |
|
64267 | 95 |
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
|
96 |
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
|
97 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
98 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
99 |
interpretation int: abelian_group \<Z> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
100 |
(* 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
|
101 |
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
|
102 |
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
|
103 |
(* FIXME *) |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
104 |
rewrites "carrier \<Z> = UNIV" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
105 |
and "zero \<Z> = 0" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
106 |
and "add \<Z> x y = x + y" |
64267 | 107 |
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
|
108 |
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
|
109 |
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
|
110 |
proof - |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
111 |
\<comment> \<open>Specification\<close> |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
112 |
show "abelian_group \<Z>" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
113 |
proof (rule abelian_groupI) |
55991 | 114 |
fix x |
115 |
assume "x \<in> carrier \<Z>" |
|
116 |
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
|
117 |
by simp arith |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
118 |
qed auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
119 |
then interpret int: abelian_group \<Z> . |
67443
3abf6a722518
standardized towards new-style formal comments: isabelle update_comments;
wenzelm
parents:
67399
diff
changeset
|
120 |
\<comment> \<open>Operations\<close> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
121 |
{ 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
|
122 |
note add = this |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
123 |
have zero: "zero \<Z> = 0" by simp |
55991 | 124 |
{ |
125 |
fix x |
|
126 |
have "add \<Z> (- x) x = zero \<Z>" |
|
127 |
by (simp add: add zero) |
|
128 |
then show "a_inv \<Z> x = - x" |
|
129 |
by (simp add: int.minus_equality) |
|
130 |
} |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
131 |
note a_inv = this |
55991 | 132 |
show "a_minus \<Z> x y = x - y" |
133 |
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
|
134 |
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
|
135 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
136 |
interpretation int: "domain" \<Z> |
61566
c3d6e570ccef
Keyword 'rewrites' identifies rewrite morphisms.
ballarin
parents:
61382
diff
changeset
|
137 |
rewrites "carrier \<Z> = UNIV" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
138 |
and "zero \<Z> = 0" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
139 |
and "add \<Z> x y = x + y" |
64267 | 140 |
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
|
141 |
and "a_inv \<Z> x = - x" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
142 |
and "a_minus \<Z> x y = x - y" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
143 |
proof - |
55991 | 144 |
show "domain \<Z>" |
145 |
by unfold_locales (auto simp: distrib_right distrib_left) |
|
146 |
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
|
147 |
|
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
148 |
|
69597 | 149 |
text \<open>Removal of occurrences of \<^term>\<open>UNIV\<close> in interpretation result |
61382 | 150 |
--- experimental.\<close> |
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
151 |
|
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
152 |
lemma UNIV: |
55991 | 153 |
"x \<in> UNIV \<longleftrightarrow> True" |
154 |
"A \<subseteq> UNIV \<longleftrightarrow> True" |
|
155 |
"(\<forall>x \<in> UNIV. P x) \<longleftrightarrow> (\<forall>x. P x)" |
|
67091 | 156 |
"(\<exists>x \<in> UNIV. P x) \<longleftrightarrow> (\<exists>x. P x)" |
55991 | 157 |
"(True \<longrightarrow> Q) \<longleftrightarrow> Q" |
158 |
"(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
|
159 |
by simp_all |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
160 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
161 |
interpretation int (* FIXME [unfolded UNIV] *) : |
67399 | 162 |
partial_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>" |
163 |
rewrites "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV" |
|
164 |
and "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x \<le> y)" |
|
165 |
and "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)" |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
166 |
proof - |
67399 | 167 |
show "partial_order \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>" |
61169 | 168 |
by standard simp_all |
67399 | 169 |
show "carrier \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> = UNIV" |
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
170 |
by simp |
67399 | 171 |
show "le \<lparr>carrier = UNIV::int set, eq = (=), le = (\<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
|
172 |
by simp |
67399 | 173 |
show "lless \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = (x < y)" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
174 |
by (simp add: lless_def) auto |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
175 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
176 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
177 |
interpretation int (* FIXME [unfolded UNIV] *) : |
67399 | 178 |
lattice "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>" |
179 |
rewrites "join \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = max x y" |
|
180 |
and "meet \<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr> x y = min x y" |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
181 |
proof - |
67399 | 182 |
let ?Z = "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
183 |
show "lattice ?Z" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
184 |
apply unfold_locales |
68561 | 185 |
apply (simp_all add: least_def Upper_def greatest_def Lower_def) |
186 |
apply arith+ |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
187 |
done |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
188 |
then interpret int: lattice "?Z" . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
189 |
show "join ?Z x y = max x y" |
68561 | 190 |
by (metis int.le_iff_meet iso_tuple_UNIV_I join_comm linear max.absorb_iff2 max_def) |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
191 |
show "meet ?Z x y = min x y" |
68561 | 192 |
using int.meet_le int.meet_left int.meet_right by auto |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
193 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
194 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
195 |
interpretation int (* [unfolded UNIV] *) : |
67399 | 196 |
total_order "\<lparr>carrier = UNIV::int set, eq = (=), le = (\<le>)\<rparr>" |
61169 | 197 |
by standard clarsimp |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
198 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
199 |
|
63167 | 200 |
subsection \<open>Generated Ideals of \<open>\<Z>\<close>\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
201 |
|
55991 | 202 |
lemma int_Idl: "Idl\<^bsub>\<Z>\<^esub> {a} = {x * a | x. True}" |
68561 | 203 |
by (simp_all add: cgenideal_def int.cgenideal_eq_genideal[symmetric]) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
204 |
|
55991 | 205 |
lemma multiples_principalideal: "principalideal {x * a | x. True } \<Z>" |
206 |
by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl) |
|
29700 | 207 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
208 |
lemma prime_primeideal: |
68399
0b71d08528f0
resolution of name clashes in Algebra
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
209 |
assumes prime: "Factorial_Ring.prime p" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
210 |
shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>" |
68561 | 211 |
proof (rule primeidealI) |
212 |
show "ideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>" |
|
213 |
by (rule int.genideal_ideal, simp) |
|
214 |
show "cring \<Z>" |
|
215 |
by (rule int_is_cring) |
|
216 |
have False if "UNIV = {v::int. \<exists>x. v = x * p}" |
|
217 |
proof - |
|
218 |
from that |
|
219 |
obtain i where "1 = i * p" |
|
220 |
by (blast intro: elim: ) |
|
221 |
then show False |
|
222 |
using prime by (auto simp add: abs_mult zmult_eq_1_iff) |
|
223 |
qed |
|
224 |
then show "carrier \<Z> \<noteq> Idl\<^bsub>\<Z>\<^esub> {p}" |
|
225 |
by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) |
|
226 |
have "p dvd a \<or> p dvd b" if "a * b = x * p" for a b x |
|
227 |
by (simp add: prime prime_dvd_multD that) |
|
228 |
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> |
|
229 |
\<Longrightarrow> a \<in> Idl\<^bsub>\<Z>\<^esub> {p} \<or> b \<in> Idl\<^bsub>\<Z>\<^esub> {p}" |
|
230 |
by (auto simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def dvd_def mult.commute) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
231 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
232 |
|
61382 | 233 |
subsection \<open>Ideals and Divisibility\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
234 |
|
55991 | 235 |
lemma int_Idl_subset_ideal: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})" |
236 |
by (rule int.Idl_subset_ideal') simp_all |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
237 |
|
55991 | 238 |
lemma Idl_subset_eq_dvd: "Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> l dvd k" |
68561 | 239 |
by (subst int_Idl_subset_ideal) (auto simp: dvd_def int_Idl) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
240 |
|
55991 | 241 |
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
|
242 |
proof - |
55991 | 243 |
have a: "l dvd k \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" |
244 |
by (rule Idl_subset_eq_dvd[symmetric]) |
|
245 |
have b: "k dvd l \<longleftrightarrow> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" |
|
246 |
by (rule Idl_subset_eq_dvd[symmetric]) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
247 |
|
55991 | 248 |
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}" |
249 |
by (subst a, subst b, simp) |
|
250 |
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}" |
|
251 |
by blast |
|
252 |
finally show ?thesis . |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
253 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
254 |
|
61945 | 255 |
lemma Idl_eq_abs: "Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l} \<longleftrightarrow> \<bar>l\<bar> = \<bar>k\<bar>" |
55991 | 256 |
apply (subst dvds_eq_abseq[symmetric]) |
257 |
apply (rule dvds_eq_Idl[symmetric]) |
|
258 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
259 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
260 |
|
61382 | 261 |
subsection \<open>Ideals and the Modulus\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
262 |
|
55991 | 263 |
definition ZMod :: "int \<Rightarrow> int \<Rightarrow> int set" |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
264 |
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
|
265 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
266 |
lemmas ZMod_defs = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
267 |
ZMod_def genideal_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
268 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
269 |
lemma rcos_zfact: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
270 |
assumes kIl: "k \<in> ZMod l r" |
55991 | 271 |
shows "\<exists>x. k = x * l + r" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
272 |
proof - |
55991 | 273 |
from kIl[unfolded ZMod_def] have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" |
274 |
by (simp add: a_r_coset_defs) |
|
275 |
then obtain xl where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" and k: "k = xl + r" |
|
276 |
by auto |
|
277 |
from xl obtain x where "xl = x * l" |
|
278 |
by (auto simp: int_Idl) |
|
279 |
with k have "k = x * l + r" |
|
280 |
by simp |
|
281 |
then show "\<exists>x. k = x * l + r" .. |
|
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 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
284 |
lemma ZMod_imp_zmod: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
285 |
assumes zmods: "ZMod m a = ZMod m b" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
286 |
shows "a mod m = b mod m" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
287 |
proof - |
55991 | 288 |
interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> |
289 |
by (rule int.genideal_ideal) fast |
|
290 |
from zmods have "b \<in> ZMod m a" |
|
291 |
unfolding ZMod_def by (simp add: a_repr_independenceD) |
|
292 |
then have "\<exists>x. b = x * m + a" |
|
293 |
by (rule rcos_zfact) |
|
294 |
then obtain x where "b = x * m + a" |
|
295 |
by fast |
|
296 |
then have "b mod m = (x * m + a) mod m" |
|
297 |
by simp |
|
298 |
also have "\<dots> = ((x * m) mod m) + (a mod m)" |
|
299 |
by (simp add: mod_add_eq) |
|
300 |
also have "\<dots> = a mod m" |
|
301 |
by simp |
|
302 |
finally have "b mod m = a mod m" . |
|
303 |
then show "a mod m = b mod m" .. |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
304 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
305 |
|
55991 | 306 |
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
|
307 |
proof - |
55991 | 308 |
interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> |
309 |
by (rule int.genideal_ideal) fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
310 |
show ?thesis |
55991 | 311 |
unfolding ZMod_def |
312 |
apply (rule a_repr_independence'[symmetric]) |
|
313 |
apply (simp add: int_Idl a_r_coset_defs) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
314 |
proof - |
55991 | 315 |
have "a = m * (a div m) + (a mod m)" |
64246 | 316 |
by (simp add: mult_div_mod_eq [symmetric]) |
55991 | 317 |
then have "a = (a div m) * m + (a mod m)" |
318 |
by simp |
|
319 |
then show "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" |
|
320 |
by fast |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
321 |
qed simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
322 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
323 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
324 |
lemma zmod_imp_ZMod: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
325 |
assumes modeq: "a mod m = b mod m" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
326 |
shows "ZMod m a = ZMod m b" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
327 |
proof - |
55991 | 328 |
have "ZMod m a = ZMod m (a mod m)" |
329 |
by (rule ZMod_mod) |
|
330 |
also have "\<dots> = ZMod m (b mod m)" |
|
331 |
by (simp add: modeq[symmetric]) |
|
332 |
also have "\<dots> = ZMod m b" |
|
333 |
by (rule ZMod_mod[symmetric]) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
334 |
finally show ?thesis . |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
335 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
336 |
|
55991 | 337 |
corollary ZMod_eq_mod: "ZMod m a = ZMod m b \<longleftrightarrow> a mod m = b mod m" |
338 |
apply (rule iffI) |
|
339 |
apply (erule ZMod_imp_zmod) |
|
340 |
apply (erule zmod_imp_ZMod) |
|
341 |
done |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
342 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
343 |
|
61382 | 344 |
subsection \<open>Factorization\<close> |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
345 |
|
55991 | 346 |
definition ZFact :: "int \<Rightarrow> int set ring" |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
347 |
where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
348 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
349 |
lemmas ZFact_defs = ZFact_def FactRing_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
350 |
|
55991 | 351 |
lemma ZFact_is_cring: "cring (ZFact k)" |
68561 | 352 |
by (simp add: ZFact_def ideal.quotient_is_cring int.cring_axioms int.genideal_ideal) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
353 |
|
55991 | 354 |
lemma ZFact_zero: "carrier (ZFact 0) = (\<Union>a. {{a}})" |
68561 | 355 |
by (simp add: ZFact_defs A_RCOSETS_defs r_coset_def int.genideal_zero) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
356 |
|
55991 | 357 |
lemma ZFact_one: "carrier (ZFact 1) = {UNIV}" |
68561 | 358 |
unfolding ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps int.genideal_one |
359 |
proof |
|
360 |
have "\<And>a b::int. \<exists>x. b = x + a" |
|
361 |
by presburger |
|
362 |
then show "(\<Union>a::int. {\<Union>h. {h + a}}) \<subseteq> {UNIV}" |
|
363 |
by force |
|
364 |
then show "{UNIV} \<subseteq> (\<Union>a::int. {\<Union>h. {h + a}})" |
|
365 |
by (metis (no_types, lifting) UNIV_I UN_I singletonD singletonI subset_iff) |
|
366 |
qed |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
367 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
368 |
lemma ZFact_prime_is_domain: |
68399
0b71d08528f0
resolution of name clashes in Algebra
paulson <lp15@cam.ac.uk>
parents:
67443
diff
changeset
|
369 |
assumes pprime: "Factorial_Ring.prime p" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
370 |
shows "domain (ZFact p)" |
68561 | 371 |
by (simp add: ZFact_def pprime prime_primeideal primeideal.quotient_is_domain) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
372 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
373 |
end |