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