author | haftmann |
Tue, 23 Feb 2010 10:11:12 +0100 | |
changeset 35315 | fbdc860d87a3 |
parent 26342 | 0f65fa163304 |
child 35849 | b5522b51cb1e |
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 |
Ideals for commutative rings |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
3 |
Author: Clemens Ballarin, started 24 September 1999 |
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 Ideal2 imports Ring2 begin |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
7 |
|
21423 | 8 |
definition |
9 |
is_ideal :: "('a::ring) set => bool" where |
|
10 |
"is_ideal I \<longleftrightarrow> (ALL a: I. ALL b: I. a + b : I) & |
|
11 |
(ALL a: I. - a : I) & 0 : I & |
|
12 |
(ALL a: I. ALL r. a * r : I)" |
|
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
13 |
|
21423 | 14 |
definition |
15 |
ideal_of :: "('a::ring) set => 'a set" where |
|
16 |
"ideal_of S = Inter {I. is_ideal I & S <= I}" |
|
17 |
||
18 |
definition |
|
19 |
is_pideal :: "('a::ring) set => bool" where |
|
20 |
"is_pideal I \<longleftrightarrow> (EX a. I = ideal_of {a})" |
|
21 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
22 |
|
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
23 |
text {* Principle ideal domains *} |
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
24 |
|
35315 | 25 |
class pid = |
26 |
assumes pid_ax: "is_ideal (I :: 'a::domain \<Rightarrow> _) \<Longrightarrow> is_pideal I" |
|
21423 | 27 |
|
28 |
(* is_ideal *) |
|
29 |
||
30 |
lemma is_idealI: |
|
31 |
"!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; |
|
32 |
!! a. a:I ==> - a : I; 0 : I; |
|
33 |
!! a r. a:I ==> a * r : I |] ==> is_ideal I" |
|
34 |
unfolding is_ideal_def by blast |
|
35 |
||
36 |
lemma is_ideal_add [simp]: "[| is_ideal I; a:I; b:I |] ==> a + b : I" |
|
37 |
unfolding is_ideal_def by blast |
|
38 |
||
39 |
lemma is_ideal_uminus [simp]: "[| is_ideal I; a:I |] ==> - a : I" |
|
40 |
unfolding is_ideal_def by blast |
|
41 |
||
42 |
lemma is_ideal_zero [simp]: "[| is_ideal I |] ==> 0 : I" |
|
43 |
unfolding is_ideal_def by blast |
|
44 |
||
45 |
lemma is_ideal_mult [simp]: "[| is_ideal I; a:I |] ==> a * r : I" |
|
46 |
unfolding is_ideal_def by blast |
|
47 |
||
48 |
lemma is_ideal_dvd: "[| a dvd b; is_ideal I; a:I |] ==> b:I" |
|
49 |
unfolding is_ideal_def dvd_def by blast |
|
50 |
||
51 |
lemma UNIV_is_ideal [simp]: "is_ideal (UNIV::('a::ring) set)" |
|
52 |
unfolding is_ideal_def by blast |
|
53 |
||
54 |
lemma zero_is_ideal [simp]: "is_ideal {0::'a::ring}" |
|
55 |
unfolding is_ideal_def by auto |
|
56 |
||
57 |
lemma is_ideal_1: "is_ideal {x::'a::ring. a dvd x}" |
|
58 |
apply (rule is_idealI) |
|
59 |
apply auto |
|
60 |
done |
|
61 |
||
62 |
lemma is_ideal_2: "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}" |
|
63 |
apply (rule is_idealI) |
|
64 |
apply auto |
|
65 |
apply (rule_tac x = "u+ua" in exI) |
|
66 |
apply (rule_tac x = "v+va" in exI) |
|
67 |
apply (rule_tac [2] x = "-u" in exI) |
|
68 |
apply (rule_tac [2] x = "-v" in exI) |
|
69 |
apply (rule_tac [3] x = "0" in exI) |
|
70 |
apply (rule_tac [3] x = "0" in exI) |
|
71 |
apply (rule_tac [4] x = "u * r" in exI) |
|
72 |
apply (rule_tac [4] x = "v * r" in exI) |
|
73 |
apply simp_all |
|
74 |
done |
|
75 |
||
76 |
||
77 |
(* ideal_of *) |
|
78 |
||
79 |
lemma ideal_of_is_ideal: "is_ideal (ideal_of S)" |
|
80 |
unfolding is_ideal_def ideal_of_def by blast |
|
81 |
||
82 |
lemma generator_in_ideal: "a:S ==> a : (ideal_of S)" |
|
83 |
unfolding ideal_of_def by blast |
|
84 |
||
85 |
lemma ideal_of_one_eq: "ideal_of {1::'a::ring} = UNIV" |
|
86 |
apply (unfold ideal_of_def) |
|
87 |
apply (force dest: is_ideal_mult simp add: l_one) |
|
88 |
done |
|
89 |
||
90 |
lemma ideal_of_empty_eq: "ideal_of {} = {0::'a::ring}" |
|
91 |
apply (unfold ideal_of_def) |
|
92 |
apply (rule subset_antisym) |
|
93 |
apply (rule subsetI) |
|
94 |
apply (drule InterD) |
|
95 |
prefer 2 apply assumption |
|
96 |
apply (auto simp add: is_ideal_zero) |
|
97 |
done |
|
98 |
||
99 |
lemma pideal_structure: "ideal_of {a} = {x::'a::ring. a dvd x}" |
|
100 |
apply (unfold ideal_of_def) |
|
101 |
apply (rule subset_antisym) |
|
102 |
apply (rule subsetI) |
|
103 |
apply (drule InterD) |
|
104 |
prefer 2 apply assumption |
|
105 |
apply (auto intro: is_ideal_1) |
|
106 |
apply (simp add: is_ideal_dvd) |
|
107 |
done |
|
108 |
||
109 |
lemma ideal_of_2_structure: |
|
110 |
"ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}" |
|
111 |
apply (unfold ideal_of_def) |
|
112 |
apply (rule subset_antisym) |
|
113 |
apply (rule subsetI) |
|
114 |
apply (drule InterD) |
|
115 |
prefer 2 apply assumption |
|
26342 | 116 |
apply (tactic {* auto_tac (@{claset} addIs [@{thm is_ideal_2}], |
117 |
@{simpset} delsimprocs [ring_simproc]) *}) |
|
21423 | 118 |
apply (rule_tac x = "1" in exI) |
119 |
apply (rule_tac x = "0" in exI) |
|
120 |
apply (rule_tac [2] x = "0" in exI) |
|
121 |
apply (rule_tac [2] x = "1" in exI) |
|
122 |
apply simp |
|
123 |
apply simp |
|
124 |
done |
|
125 |
||
126 |
lemma ideal_of_mono: "A <= B ==> ideal_of A <= ideal_of B" |
|
127 |
unfolding ideal_of_def by blast |
|
128 |
||
129 |
lemma ideal_of_zero_eq: "ideal_of {0::'a::ring} = {0}" |
|
130 |
apply (simp add: pideal_structure) |
|
131 |
apply (rule subset_antisym) |
|
132 |
apply (auto intro: "dvd_zero_left") |
|
133 |
done |
|
134 |
||
135 |
lemma element_generates_subideal: "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I" |
|
136 |
apply (auto simp add: pideal_structure is_ideal_dvd) |
|
137 |
done |
|
138 |
||
139 |
||
140 |
(* is_pideal *) |
|
141 |
||
142 |
lemma is_pideal_imp_is_ideal: "is_pideal (I::('a::ring) set) ==> is_ideal I" |
|
143 |
unfolding is_pideal_def by (fast intro: ideal_of_is_ideal) |
|
144 |
||
145 |
lemma pideal_is_pideal: "is_pideal (ideal_of {a::'a::ring})" |
|
146 |
unfolding is_pideal_def by blast |
|
147 |
||
148 |
lemma is_pidealD: "is_pideal I ==> EX a. I = ideal_of {a}" |
|
149 |
unfolding is_pideal_def . |
|
150 |
||
151 |
||
152 |
(* Ideals and divisibility *) |
|
153 |
||
154 |
lemma dvd_imp_subideal: "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}" |
|
155 |
by (auto intro: dvd_trans_ring simp add: pideal_structure) |
|
156 |
||
157 |
lemma subideal_imp_dvd: "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a" |
|
158 |
by (auto dest!: subsetD simp add: pideal_structure) |
|
159 |
||
160 |
lemma psubideal_not_dvd: "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b" |
|
161 |
apply (simp add: psubset_eq pideal_structure) |
|
162 |
apply (erule conjE) |
|
163 |
apply (drule_tac c = "a" in subsetD) |
|
164 |
apply (auto intro: dvd_trans_ring) |
|
165 |
done |
|
166 |
||
167 |
lemma not_dvd_psubideal_singleton: |
|
168 |
"[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}" |
|
169 |
apply (rule psubsetI) |
|
170 |
apply (erule dvd_imp_subideal) |
|
171 |
apply (blast intro: dvd_imp_subideal subideal_imp_dvd) |
|
172 |
done |
|
173 |
||
174 |
lemma subideal_is_dvd [iff]: "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)" |
|
175 |
apply (rule iffI) |
|
176 |
apply (assumption | rule subideal_imp_dvd dvd_imp_subideal)+ |
|
177 |
done |
|
178 |
||
179 |
lemma psubideal_is_dvd [iff]: "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)" |
|
180 |
apply (rule iffI) |
|
181 |
apply (assumption | rule conjI psubideal_not_dvd psubset_imp_subset [THEN subideal_imp_dvd])+ |
|
182 |
apply (erule conjE) |
|
183 |
apply (assumption | rule not_dvd_psubideal_singleton)+ |
|
184 |
done |
|
185 |
||
186 |
lemma assoc_pideal_eq: "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}" |
|
187 |
apply (rule subset_antisym) |
|
188 |
apply (assumption | rule dvd_imp_subideal)+ |
|
189 |
done |
|
190 |
||
191 |
lemma dvd_imp_in_pideal: "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})" |
|
192 |
apply (rule is_ideal_dvd) |
|
193 |
apply assumption |
|
194 |
apply (rule ideal_of_is_ideal) |
|
195 |
apply (rule generator_in_ideal) |
|
196 |
apply simp |
|
197 |
done |
|
198 |
||
199 |
lemma in_pideal_imp_dvd: "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b" |
|
200 |
by (simp add: pideal_structure) |
|
201 |
||
202 |
lemma not_dvd_psubideal: "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}" |
|
203 |
apply (simp add: psubset_eq ideal_of_mono) |
|
204 |
apply (erule contrapos_pp) |
|
205 |
apply (simp add: ideal_of_2_structure) |
|
206 |
apply (rule in_pideal_imp_dvd) |
|
207 |
apply simp |
|
208 |
apply (rule_tac x = "0" in exI) |
|
209 |
apply (rule_tac x = "1" in exI) |
|
210 |
apply simp |
|
211 |
done |
|
212 |
||
213 |
lemma irred_imp_max_ideal: |
|
214 |
"[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I" |
|
215 |
apply (unfold irred_def) |
|
216 |
apply (drule is_pidealD) |
|
217 |
apply (erule exE) |
|
218 |
apply clarify |
|
219 |
apply (erule_tac x = "aa" in allE) |
|
220 |
apply clarify |
|
221 |
apply (drule_tac a = "1" in dvd_imp_subideal) |
|
222 |
apply (auto simp add: ideal_of_one_eq) |
|
223 |
done |
|
224 |
||
225 |
(* Pid are factorial *) |
|
226 |
||
227 |
(* Divisor chain condition *) |
|
228 |
(* proofs not finished *) |
|
229 |
||
230 |
lemma subset_chain_lemma [rule_format (no_asm)]: |
|
231 |
"(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)" |
|
232 |
apply (induct_tac m) |
|
233 |
apply blast |
|
234 |
(* induction step *) |
|
235 |
apply (rename_tac m) |
|
236 |
apply (case_tac "n <= m") |
|
237 |
apply auto |
|
238 |
apply (subgoal_tac "n = Suc m") |
|
239 |
prefer 2 |
|
240 |
apply arith |
|
241 |
apply force |
|
242 |
done |
|
243 |
||
244 |
lemma chain_is_ideal: "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] |
|
245 |
==> is_ideal (Union (I`UNIV))" |
|
246 |
apply (rule is_idealI) |
|
247 |
apply auto |
|
248 |
apply (rule_tac x = "max x xa" in exI) |
|
249 |
apply (rule is_ideal_add) |
|
250 |
apply simp |
|
251 |
apply (rule subset_chain_lemma) |
|
252 |
apply assumption |
|
253 |
apply (rule conjI) |
|
254 |
prefer 2 |
|
255 |
apply assumption |
|
256 |
apply arith |
|
257 |
apply (rule subset_chain_lemma) |
|
258 |
apply assumption |
|
259 |
apply (rule conjI) |
|
260 |
prefer 2 |
|
261 |
apply assumption |
|
262 |
apply arith |
|
263 |
apply (rule_tac x = "x" in exI) |
|
264 |
apply simp |
|
265 |
apply (rule_tac x = "x" in exI) |
|
266 |
apply simp |
|
267 |
done |
|
268 |
||
269 |
||
270 |
(* Primeness condition *) |
|
271 |
||
272 |
lemma pid_irred_imp_prime: "irred a ==> prime (a::'a::pid)" |
|
273 |
apply (unfold prime_def) |
|
274 |
apply (rule conjI) |
|
275 |
apply (rule_tac [2] conjI) |
|
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
21423
diff
changeset
|
276 |
apply (tactic "clarify_tac @{claset} 3") |
21423 | 277 |
apply (drule_tac [3] I = "ideal_of {a, b}" and x = "1" in irred_imp_max_ideal) |
278 |
apply (auto intro: ideal_of_is_ideal pid_ax simp add: irred_def not_dvd_psubideal pid_ax) |
|
279 |
apply (simp add: ideal_of_2_structure) |
|
280 |
apply clarify |
|
281 |
apply (drule_tac f = "op* aa" in arg_cong) |
|
282 |
apply (simp add: r_distr) |
|
283 |
apply (erule subst) |
|
26342 | 284 |
apply (tactic {* asm_simp_tac (@{simpset} addsimps [@{thm m_assoc} RS sym] |
21423 | 285 |
delsimprocs [ring_simproc]) 1 *}) |
286 |
done |
|
287 |
||
288 |
(* Fields are Pid *) |
|
289 |
||
290 |
lemma field_pideal_univ: "a ~= 0 ==> ideal_of {a::'a::field} = UNIV" |
|
291 |
apply (rule subset_antisym) |
|
292 |
apply simp |
|
293 |
apply (rule subset_trans) |
|
294 |
prefer 2 |
|
295 |
apply (rule dvd_imp_subideal) |
|
296 |
apply (rule field_ax) |
|
297 |
apply assumption |
|
298 |
apply (simp add: ideal_of_one_eq) |
|
299 |
done |
|
300 |
||
301 |
lemma proper_ideal: "[| is_ideal I; I ~= {0} |] ==> {0} < I" |
|
302 |
by (simp add: psubset_eq not_sym is_ideal_zero) |
|
303 |
||
304 |
lemma field_pid: "is_ideal (I::('a::field) set) ==> is_pideal I" |
|
305 |
apply (unfold is_pideal_def) |
|
306 |
apply (case_tac "I = {0}") |
|
307 |
apply (rule_tac x = "0" in exI) |
|
308 |
apply (simp add: ideal_of_zero_eq) |
|
309 |
(* case "I ~= {0}" *) |
|
310 |
apply (frule proper_ideal) |
|
311 |
apply assumption |
|
312 |
apply (drule psubset_imp_ex_mem) |
|
313 |
apply (erule exE) |
|
314 |
apply (rule_tac x = b in exI) |
|
315 |
apply (cut_tac a = b in element_generates_subideal) |
|
316 |
apply assumption |
|
317 |
apply blast |
|
318 |
apply (auto simp add: field_pideal_univ) |
|
319 |
done |
|
320 |
||
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
diff
changeset
|
321 |
end |