author | paulson <lp15@cam.ac.uk> |
Sun, 02 Feb 2014 19:15:25 +0000 | |
changeset 55242 | 413ec965f95d |
parent 55157 | 06897ea77f78 |
child 55926 | 3ef14caf5637 |
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 |
55157 | 7 |
imports QuotRing Lattice Int "~~/src/HOL/Number_Theory/Primes" |
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 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
10 |
section {* The Ring of Integers *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
11 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
12 |
subsection {* Some properties of @{typ int} *} |
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: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
15 |
"(l dvd k \<and> k dvd l) = (abs l = abs (k::int))" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
16 |
apply rule |
33657 | 17 |
apply (simp add: zdvd_antisym_abs) |
33676
802f5e233e48
moved lemma from Algebra/IntRing to Ring_and_Field
nipkow
parents:
33657
diff
changeset
|
18 |
apply (simp add: dvd_if_abs_eq) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
19 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
20 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
21 |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
22 |
subsection {* @{text "\<Z>"}: The Set of Integers as Algebraic Structure *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
23 |
|
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
24 |
abbreviation |
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
25 |
int_ring :: "int ring" ("\<Z>") where |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
26 |
"int_ring == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
27 |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
28 |
lemma int_Zcarr [intro!, simp]: |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
29 |
"k \<in> carrier \<Z>" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
30 |
by simp |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
31 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
32 |
lemma int_is_cring: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
33 |
"cring \<Z>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
34 |
apply (rule cringI) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
35 |
apply (rule abelian_groupI, simp_all) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
36 |
defer 1 |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
37 |
apply (rule comm_monoidI, simp_all) |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44821
diff
changeset
|
38 |
apply (rule distrib_right) |
44821 | 39 |
apply (fast intro: left_minus) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
40 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
41 |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
42 |
(* |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
43 |
lemma int_is_domain: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
44 |
"domain \<Z>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
45 |
apply (intro domain.intro domain_axioms.intro) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
46 |
apply (rule int_is_cring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
47 |
apply (unfold int_ring_def, simp+) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
48 |
done |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
49 |
*) |
35849 | 50 |
|
51 |
||
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
52 |
subsection {* Interpretations *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
53 |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
54 |
text {* Since definitions of derived operations are global, their |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
55 |
interpretation needs to be done as early as possible --- that is, |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
56 |
with as few assumptions as possible. *} |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
57 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
58 |
interpretation int: monoid \<Z> |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
59 |
where "carrier \<Z> = UNIV" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
60 |
and "mult \<Z> x y = x * y" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
61 |
and "one \<Z> = 1" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
62 |
and "pow \<Z> x n = x^n" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
63 |
proof - |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
64 |
-- "Specification" |
44655 | 65 |
show "monoid \<Z>" by default auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
66 |
then interpret int: monoid \<Z> . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
67 |
|
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
68 |
-- "Carrier" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
69 |
show "carrier \<Z> = UNIV" by simp |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
70 |
|
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
71 |
-- "Operations" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
72 |
{ fix x y show "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
|
73 |
note mult = this |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
74 |
show one: "one \<Z> = 1" by simp |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
75 |
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
|
76 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
77 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
78 |
interpretation int: comm_monoid \<Z> |
28524 | 79 |
where "finprod \<Z> f A = (if finite A then setprod f A else undefined)" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
80 |
proof - |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
81 |
-- "Specification" |
44655 | 82 |
show "comm_monoid \<Z>" by default auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
83 |
then interpret int: comm_monoid \<Z> . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
84 |
|
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
85 |
-- "Operations" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
86 |
{ 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
|
87 |
note mult = this |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
88 |
have one: "one \<Z> = 1" by simp |
28524 | 89 |
show "finprod \<Z> f A = (if finite A then setprod f A else undefined)" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
90 |
proof (cases "finite A") |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
91 |
case True then show ?thesis proof induct |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
92 |
case empty show ?case by (simp add: one) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
93 |
next |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
94 |
case insert then show ?case by (simp add: Pi_def mult) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
95 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
96 |
next |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
97 |
case False then show ?thesis by (simp add: finprod_def) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
98 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
99 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
100 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
101 |
interpretation int: abelian_monoid \<Z> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
102 |
where int_carrier_eq: "carrier \<Z> = UNIV" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
103 |
and int_zero_eq: "zero \<Z> = 0" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
104 |
and int_add_eq: "add \<Z> x y = x + y" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
105 |
and int_finsum_eq: "finsum \<Z> f A = (if finite A then setsum f A else undefined)" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
106 |
proof - |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
107 |
-- "Specification" |
44655 | 108 |
show "abelian_monoid \<Z>" by default auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
109 |
then interpret int: abelian_monoid \<Z> . |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
110 |
|
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
111 |
-- "Carrier" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
112 |
show "carrier \<Z> = UNIV" by simp |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
113 |
|
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
114 |
-- "Operations" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
115 |
{ 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
|
116 |
note add = this |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
117 |
show zero: "zero \<Z> = 0" by simp |
28524 | 118 |
show "finsum \<Z> f A = (if finite A then setsum f A else undefined)" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
119 |
proof (cases "finite A") |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
120 |
case True then show ?thesis proof induct |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
121 |
case empty show ?case by (simp add: zero) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
122 |
next |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
123 |
case insert then show ?case by (simp add: Pi_def add) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
124 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
125 |
next |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
126 |
case False then show ?thesis by (simp add: finsum_def finprod_def) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
127 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
128 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
129 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
130 |
interpretation int: abelian_group \<Z> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
131 |
(* 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
|
132 |
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
|
133 |
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
|
134 |
(* FIXME *) |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
135 |
where "carrier \<Z> = UNIV" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
136 |
and "zero \<Z> = 0" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
137 |
and "add \<Z> x y = x + y" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
138 |
and "finsum \<Z> f A = (if finite A then setsum f A else undefined)" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
139 |
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
|
140 |
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
|
141 |
proof - |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
142 |
-- "Specification" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
143 |
show "abelian_group \<Z>" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
144 |
proof (rule abelian_groupI) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
145 |
show "!!x. x \<in> carrier \<Z> ==> EX y : 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
|
146 |
by simp arith |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
147 |
qed auto |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
148 |
then interpret int: abelian_group \<Z> . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
149 |
-- "Operations" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
150 |
{ 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
|
151 |
note add = this |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
152 |
have zero: "zero \<Z> = 0" by simp |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
153 |
{ fix x |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
154 |
have "add \<Z> (-x) x = zero \<Z>" by (simp add: add zero) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
155 |
then show "a_inv \<Z> x = - x" by (simp add: int.minus_equality) } |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
156 |
note a_inv = this |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
157 |
show "a_minus \<Z> x y = x - y" 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
|
158 |
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
|
159 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
160 |
interpretation int: "domain" \<Z> |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
161 |
where "carrier \<Z> = UNIV" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
162 |
and "zero \<Z> = 0" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
163 |
and "add \<Z> x y = x + y" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
164 |
and "finsum \<Z> f A = (if finite A then setsum f A else undefined)" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
165 |
and "a_inv \<Z> x = - x" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
166 |
and "a_minus \<Z> x y = x - y" |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
167 |
proof - |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
44821
diff
changeset
|
168 |
show "domain \<Z>" by unfold_locales (auto simp: distrib_right distrib_left) |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
169 |
qed (simp |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
170 |
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
|
171 |
|
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
172 |
|
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
173 |
text {* Removal of occurrences of @{term UNIV} in interpretation result |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
174 |
--- experimental. *} |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
175 |
|
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
176 |
lemma UNIV: |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
177 |
"x \<in> UNIV = True" |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
178 |
"A \<subseteq> UNIV = True" |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
179 |
"(ALL x : UNIV. P x) = (ALL x. P x)" |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
180 |
"(EX x : UNIV. P x) = (EX x. P x)" |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
181 |
"(True --> Q) = Q" |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
182 |
"(True ==> PROP R) == PROP R" |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
183 |
by simp_all |
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
184 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
185 |
interpretation int (* FIXME [unfolded UNIV] *) : |
29237 | 186 |
partial_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
187 |
where "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
188 |
and "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x \<le> y)" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
189 |
and "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
190 |
proof - |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
191 |
show "partial_order (| carrier = UNIV::int set, eq = op =, le = op \<le> |)" |
44655 | 192 |
by default simp_all |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
193 |
show "carrier (| carrier = UNIV::int set, eq = op =, le = op \<le> |) = UNIV" |
24131
1099f6c73649
Experimental removal of assumptions of the form x : UNIV and the like after interpretation.
ballarin
parents:
23957
diff
changeset
|
194 |
by simp |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
195 |
show "le (| carrier = UNIV::int set, eq = op =, le = op \<le> |) 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
|
196 |
by simp |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
197 |
show "lless (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = (x < y)" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
198 |
by (simp add: lless_def) auto |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
199 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
200 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
201 |
interpretation int (* FIXME [unfolded UNIV] *) : |
29237 | 202 |
lattice "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)" |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
203 |
where "join (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = max x y" |
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
204 |
and "meet (| carrier = UNIV::int set, eq = op =, le = op \<le> |) x y = min x y" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
205 |
proof - |
27713
95b36bfe7fc4
New locales for orders and lattices where the equivalence relation is not restricted to equality.
ballarin
parents:
25919
diff
changeset
|
206 |
let ?Z = "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
207 |
show "lattice ?Z" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
208 |
apply unfold_locales |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
209 |
apply (simp add: least_def Upper_def) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
210 |
apply arith |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
211 |
apply (simp 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 |
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
214 |
then interpret int: lattice "?Z" . |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
215 |
show "join ?Z x y = max x y" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
216 |
apply (rule int.joinI) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
217 |
apply (simp_all add: least_def Upper_def) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
218 |
apply arith |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
219 |
done |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
220 |
show "meet ?Z x y = min x y" |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
221 |
apply (rule int.meetI) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
222 |
apply (simp_all add: greatest_def Lower_def) |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
223 |
apply arith |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
224 |
done |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
225 |
qed |
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
226 |
|
30729
461ee3e49ad3
interpretation/interpret: prefixes are mandatory by default;
wenzelm
parents:
29948
diff
changeset
|
227 |
interpretation int (* [unfolded UNIV] *) : |
29237 | 228 |
total_order "(| carrier = UNIV::int set, eq = op =, le = op \<le> |)" |
44655 | 229 |
by default clarsimp |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
230 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
231 |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
232 |
subsection {* Generated Ideals of @{text "\<Z>"} *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
233 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
234 |
lemma int_Idl: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
235 |
"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
|
236 |
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
|
237 |
apply (simp add: cgenideal_def) |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
238 |
done |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
239 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
240 |
lemma multiples_principalideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
241 |
"principalideal {x * a | x. True } \<Z>" |
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
|
242 |
by (metis UNIV_I int.cgenideal_eq_genideal int.cgenideal_is_principalideal int_Idl) |
29700 | 243 |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
244 |
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
|
245 |
assumes prime: "prime p" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
246 |
shows "primeideal (Idl\<^bsub>\<Z>\<^esub> {p}) \<Z>" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
247 |
apply (rule primeidealI) |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
248 |
apply (rule int.genideal_ideal, simp) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
249 |
apply (rule int_is_cring) |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
250 |
apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
251 |
apply clarsimp defer 1 |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
252 |
apply (simp add: int.cgenideal_eq_genideal[symmetric] cgenideal_def) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
253 |
apply (elim exE) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
254 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
255 |
fix a b x |
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
|
256 |
assume "a * b = x * int p" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
257 |
hence "p dvd a * b" by simp |
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
|
258 |
hence "p dvd a | p dvd b" |
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
|
259 |
by (metis prime prime_dvd_mult_eq_int) |
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
|
260 |
thus "(\<exists>x. a = x * int p) \<or> (\<exists>x. b = x * int p)" |
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
|
261 |
by (metis dvd_def mult_commute) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
262 |
next |
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
|
263 |
assume "UNIV = {uu. EX x. uu = x * int p}" |
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
|
264 |
then obtain x where "1 = x * int p" by best |
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
|
265 |
hence "\<bar>int p * x\<bar> = 1" by (simp add: mult_commute) |
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
|
266 |
then show False |
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
|
267 |
by (metis abs_of_nat int_1 of_nat_eq_iff abs_zmult_eq_1 one_not_prime_nat prime) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
268 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
269 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
270 |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
271 |
subsection {* Ideals and Divisibility *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
272 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
273 |
lemma int_Idl_subset_ideal: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
274 |
"Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l} = (k \<in> Idl\<^bsub>\<Z>\<^esub> {l})" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
275 |
by (rule int.Idl_subset_ideal', simp+) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
276 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
277 |
lemma Idl_subset_eq_dvd: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
278 |
"(Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) = (l dvd k)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
279 |
apply (subst int_Idl_subset_ideal, subst int_Idl, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
280 |
apply (rule, clarify) |
29424 | 281 |
apply (simp add: dvd_def) |
282 |
apply (simp add: dvd_def mult_ac) |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
283 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
284 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
285 |
lemma dvds_eq_Idl: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
286 |
"(l dvd k \<and> k dvd l) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
287 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
288 |
have a: "l dvd k = (Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l})" by (rule Idl_subset_eq_dvd[symmetric]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
289 |
have b: "k dvd l = (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})" by (rule Idl_subset_eq_dvd[symmetric]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
290 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
291 |
have "(l dvd k \<and> k dvd l) = ((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k}))" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
292 |
by (subst a, subst b, simp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
293 |
also have "((Idl\<^bsub>\<Z>\<^esub> {k} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {l}) \<and> (Idl\<^bsub>\<Z>\<^esub> {l} \<subseteq> Idl\<^bsub>\<Z>\<^esub> {k})) = (Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l})" by (rule, fast+) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
294 |
finally |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
295 |
show ?thesis . |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
296 |
qed |
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 Idl_eq_abs: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
299 |
"(Idl\<^bsub>\<Z>\<^esub> {k} = Idl\<^bsub>\<Z>\<^esub> {l}) = (abs l = abs k)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
300 |
apply (subst dvds_eq_abseq[symmetric]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
301 |
apply (rule dvds_eq_Idl[symmetric]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
302 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
303 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
304 |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
305 |
subsection {* Ideals and the Modulus *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
306 |
|
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
307 |
definition |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
308 |
ZMod :: "int => int => int set" |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
309 |
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
|
310 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
311 |
lemmas ZMod_defs = |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
312 |
ZMod_def genideal_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
313 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
314 |
lemma rcos_zfact: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
315 |
assumes kIl: "k \<in> ZMod l r" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
316 |
shows "EX x. k = x * l + r" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
317 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
318 |
from kIl[unfolded ZMod_def] |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
319 |
have "\<exists>xl\<in>Idl\<^bsub>\<Z>\<^esub> {l}. k = xl + r" by (simp add: a_r_coset_defs) |
55157 | 320 |
then obtain xl |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
321 |
where xl: "xl \<in> Idl\<^bsub>\<Z>\<^esub> {l}" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
322 |
and k: "k = xl + r" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
323 |
by auto |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
324 |
from xl obtain x |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
325 |
where "xl = x * l" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
326 |
by (simp add: int_Idl, fast) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
327 |
from k and this |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
328 |
have "k = x * l + r" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
329 |
thus "\<exists>x. k = x * l + r" .. |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
330 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
331 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
332 |
lemma ZMod_imp_zmod: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
333 |
assumes zmods: "ZMod m a = ZMod m b" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
334 |
shows "a mod m = b mod m" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
335 |
proof - |
29237 | 336 |
interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
337 |
from zmods |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
338 |
have "b \<in> ZMod m a" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
339 |
unfolding ZMod_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
340 |
by (simp add: a_repr_independenceD) |
55157 | 341 |
then |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
342 |
have "EX x. b = x * m + a" by (rule rcos_zfact) |
55157 | 343 |
then obtain x |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
344 |
where "b = x * m + a" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
345 |
by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
346 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
347 |
hence "b mod m = (x * m + a) mod m" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
348 |
also |
29948 | 349 |
have "\<dots> = ((x * m) mod m) + (a mod m)" by (simp add: mod_add_eq) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
350 |
also |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
351 |
have "\<dots> = a mod m" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
352 |
finally |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
353 |
have "b mod m = a mod m" . |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
354 |
thus "a mod m = b mod m" .. |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
355 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
356 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
357 |
lemma ZMod_mod: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
358 |
shows "ZMod m a = ZMod m (a mod m)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
359 |
proof - |
29237 | 360 |
interpret ideal "Idl\<^bsub>\<Z>\<^esub> {m}" \<Z> by (rule int.genideal_ideal, fast) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
361 |
show ?thesis |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
362 |
unfolding ZMod_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
363 |
apply (rule a_repr_independence'[symmetric]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
364 |
apply (simp add: int_Idl a_r_coset_defs) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
365 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
366 |
have "a = m * (a div m) + (a mod m)" by (simp add: zmod_zdiv_equality) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
367 |
hence "a = (a div m) * m + (a mod m)" by simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
368 |
thus "\<exists>h. (\<exists>x. h = x * m) \<and> a = h + a mod m" by fast |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
369 |
qed simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
370 |
qed |
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 |
lemma zmod_imp_ZMod: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
373 |
assumes modeq: "a mod m = b mod m" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
374 |
shows "ZMod m a = ZMod m b" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
375 |
proof - |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
376 |
have "ZMod m a = ZMod m (a mod m)" by (rule ZMod_mod) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
377 |
also have "\<dots> = ZMod m (b mod m)" by (simp add: modeq[symmetric]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
378 |
also have "\<dots> = ZMod m b" by (rule ZMod_mod[symmetric]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
379 |
finally show ?thesis . |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
380 |
qed |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
381 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
382 |
corollary ZMod_eq_mod: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
383 |
shows "(ZMod m a = ZMod m b) = (a mod m = b mod m)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
384 |
by (rule, erule ZMod_imp_zmod, erule zmod_imp_ZMod) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
385 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
386 |
|
27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27713
diff
changeset
|
387 |
subsection {* Factorization *} |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
388 |
|
35848
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
389 |
definition |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
390 |
ZFact :: "int \<Rightarrow> int set ring" |
5443079512ea
slightly more uniform definitions -- eliminated old-style meta-equality;
wenzelm
parents:
35416
diff
changeset
|
391 |
where "ZFact k = \<Z> Quot (Idl\<^bsub>\<Z>\<^esub> {k})" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
392 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
393 |
lemmas ZFact_defs = ZFact_def FactRing_def |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
394 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
395 |
lemma ZFact_is_cring: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
396 |
shows "cring (ZFact k)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
397 |
apply (unfold ZFact_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
398 |
apply (rule ideal.quotient_is_cring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
399 |
apply (intro ring.genideal_ideal) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
400 |
apply (simp add: cring.axioms[OF int_is_cring] ring.intro) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
401 |
apply simp |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
402 |
apply (rule int_is_cring) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
403 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
404 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
405 |
lemma ZFact_zero: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
406 |
"carrier (ZFact 0) = (\<Union>a. {{a}})" |
23957
54fab60ddc97
Interpretation of rings (as integers) maps defined operations to defined
ballarin
parents:
22063
diff
changeset
|
407 |
apply (insert int.genideal_zero) |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
408 |
apply (simp add: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
409 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
410 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
411 |
lemma ZFact_one: |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
412 |
"carrier (ZFact 1) = {UNIV}" |
41433
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
413 |
apply (simp only: ZFact_defs A_RCOSETS_defs r_coset_def ring_record_simps) |
1b8ff770f02c
Abelian group facts obtained from group facts via interpretation (sublocale).
ballarin
parents:
35849
diff
changeset
|
414 |
apply (subst int.genideal_one) |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
415 |
apply (rule, rule, clarsimp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
416 |
apply (rule, rule, clarsimp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
417 |
apply (rule, clarsimp, arith) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
418 |
apply (rule, clarsimp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
419 |
apply (rule exI[of _ "0"], clarsimp) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
420 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
421 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
422 |
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
|
423 |
assumes pprime: "prime p" |
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
424 |
shows "domain (ZFact p)" |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
425 |
apply (unfold ZFact_def) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
426 |
apply (rule primeideal.quotient_is_domain) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
427 |
apply (rule prime_primeideal[OF pprime]) |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
428 |
done |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
429 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
430 |
end |