|
1 (* |
|
2 Ideals for commutative rings |
|
3 $Id$ |
|
4 Author: Clemens Ballarin, started 24 September 1999 |
|
5 *) |
|
6 |
|
7 (* is_ideal *) |
|
8 |
|
9 Goalw [is_ideal_def] |
|
10 "!! I. [| !! a b. [| a:I; b:I |] ==> a + b : I; \ |
|
11 \ !! a. a:I ==> - a : I; <0> : I; \ |
|
12 \ !! a r. a:I ==> a * r : I |] ==> is_ideal I"; |
|
13 by Auto_tac; |
|
14 qed "is_idealI"; |
|
15 |
|
16 Goalw [is_ideal_def] "[| is_ideal I; a:I; b:I |] ==> a + b : I"; |
|
17 by (Fast_tac 1); |
|
18 qed "is_ideal_add"; |
|
19 |
|
20 Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> - a : I"; |
|
21 by (Fast_tac 1); |
|
22 qed "is_ideal_uminus"; |
|
23 |
|
24 Goalw [is_ideal_def] "[| is_ideal I |] ==> <0> : I"; |
|
25 by (Fast_tac 1); |
|
26 qed "is_ideal_zero"; |
|
27 |
|
28 Goalw [is_ideal_def] "[| is_ideal I; a:I |] ==> a * r : I"; |
|
29 by (Fast_tac 1); |
|
30 qed "is_ideal_mult"; |
|
31 |
|
32 Goalw [dvd_def, is_ideal_def] "[| a dvd b; is_ideal I; a:I |] ==> b:I"; |
|
33 by (Fast_tac 1); |
|
34 qed "is_ideal_dvd"; |
|
35 |
|
36 Goalw [is_ideal_def] "is_ideal (UNIV::('a::ring) set)"; |
|
37 by Auto_tac; |
|
38 qed "UNIV_is_ideal"; |
|
39 |
|
40 Goalw [is_ideal_def] "is_ideal {<0>::'a::ring}"; |
|
41 by Auto_tac; |
|
42 qed "zero_is_ideal"; |
|
43 |
|
44 Addsimps [is_ideal_add, is_ideal_uminus, is_ideal_zero, is_ideal_mult, |
|
45 UNIV_is_ideal, zero_is_ideal]; |
|
46 |
|
47 Goal "is_ideal {x::'a::ring. a dvd x}"; |
|
48 by (rtac is_idealI 1); |
|
49 by Auto_tac; |
|
50 qed "is_ideal_1"; |
|
51 |
|
52 Goal "is_ideal {x::'a::ring. EX u v. x = a * u + b * v}"; |
|
53 by (rtac is_idealI 1); |
|
54 by Auto_tac; |
|
55 by (res_inst_tac [("x", "u+ua")] exI 1); |
|
56 by (res_inst_tac [("x", "v+va")] exI 1); |
|
57 by (res_inst_tac [("x", "-u")] exI 2); |
|
58 by (res_inst_tac [("x", "-v")] exI 2); |
|
59 by (res_inst_tac [("x", "<0>")] exI 3); |
|
60 by (res_inst_tac [("x", "<0>")] exI 3); |
|
61 by (res_inst_tac [("x", "u * r")] exI 4); |
|
62 by (res_inst_tac [("x", "v * r")] exI 4); |
|
63 by (REPEAT (simp_tac (simpset() addsimps [r_distr, l_distr, r_minus, minus_add, m_assoc]@a_ac) 1)); |
|
64 qed "is_ideal_2"; |
|
65 |
|
66 (* ideal_of *) |
|
67 |
|
68 Goalw [is_ideal_def, ideal_of_def] "is_ideal (ideal_of S)"; |
|
69 by (Blast_tac 1); (* Here, blast_tac is much superior to fast_tac! *) |
|
70 qed "ideal_of_is_ideal"; |
|
71 |
|
72 Goalw [ideal_of_def] "a:S ==> a : (ideal_of S)"; |
|
73 by Auto_tac; |
|
74 qed "generator_in_ideal"; |
|
75 |
|
76 Goalw [ideal_of_def] "ideal_of {<1>::'a::ring} = UNIV"; |
|
77 by (auto_tac (claset() addSDs [is_ideal_mult], simpset())); |
|
78 (* loops if is_ideal_mult is added as non-safe rule *) |
|
79 qed "ideal_of_one_eq"; |
|
80 |
|
81 Goalw [ideal_of_def] "ideal_of {} = {<0>::'a::ring}"; |
|
82 by (rtac subset_antisym 1); |
|
83 by (rtac subsetI 1); |
|
84 by (dtac InterD 1); |
|
85 by (assume_tac 2); |
|
86 by (auto_tac (claset(), simpset() addsimps [is_ideal_zero])); |
|
87 qed "ideal_of_empty_eq"; |
|
88 |
|
89 Goalw [ideal_of_def] "ideal_of {a} = {x::'a::ring. a dvd x}"; |
|
90 by (rtac subset_antisym 1); |
|
91 by (rtac subsetI 1); |
|
92 by (dtac InterD 1); |
|
93 by (assume_tac 2); |
|
94 by (auto_tac (claset() addIs [is_ideal_1], simpset())); |
|
95 by (asm_simp_tac (simpset() addsimps [is_ideal_dvd]) 1); |
|
96 qed "pideal_structure"; |
|
97 |
|
98 Goalw [ideal_of_def] |
|
99 "ideal_of {a, b} = {x::'a::ring. EX u v. x = a * u + b * v}"; |
|
100 by (rtac subset_antisym 1); |
|
101 by (rtac subsetI 1); |
|
102 by (dtac InterD 1); |
|
103 by (assume_tac 2); |
|
104 by (auto_tac (claset() addIs [is_ideal_2], simpset())); |
|
105 by (res_inst_tac [("x", "<1>")] exI 1); |
|
106 by (res_inst_tac [("x", "<0>")] exI 1); |
|
107 by (res_inst_tac [("x", "<0>")] exI 2); |
|
108 by (res_inst_tac [("x", "<1>")] exI 2); |
|
109 by (Simp_tac 1); |
|
110 by (Simp_tac 1); |
|
111 qed "ideal_of_2_structure"; |
|
112 |
|
113 Goalw [ideal_of_def] "A <= B ==> ideal_of A <= ideal_of B"; |
|
114 by Auto_tac; |
|
115 qed "ideal_of_mono"; |
|
116 |
|
117 Goal "ideal_of {<0>::'a::ring} = {<0>}"; |
|
118 by (simp_tac (simpset() addsimps [pideal_structure]) 1); |
|
119 by (rtac subset_antisym 1); |
|
120 by (auto_tac (claset() addIs [dvd_zero_left], simpset())); |
|
121 qed "ideal_of_zero_eq"; |
|
122 |
|
123 Goal "[| is_ideal I; a : I |] ==> ideal_of {a::'a::ring} <= I"; |
|
124 by (auto_tac (claset(), |
|
125 simpset() addsimps [pideal_structure, is_ideal_dvd])); |
|
126 qed "element_generates_subideal"; |
|
127 |
|
128 (* is_pideal *) |
|
129 |
|
130 Goalw [is_pideal_def] "is_pideal (I::('a::ring) set) ==> is_ideal I"; |
|
131 by (fast_tac (claset() addIs [ideal_of_is_ideal]) 1); |
|
132 qed "is_pideal_imp_is_ideal"; |
|
133 |
|
134 Goalw [is_pideal_def] "is_pideal (ideal_of {a::'a::ring})"; |
|
135 by (Fast_tac 1); |
|
136 qed "pideal_is_pideal"; |
|
137 |
|
138 Goalw [is_pideal_def] "is_pideal I ==> EX a. I = ideal_of {a}"; |
|
139 by (assume_tac 1); |
|
140 qed "is_pidealD"; |
|
141 |
|
142 (* Ideals and divisibility *) |
|
143 |
|
144 Goal "b dvd a ==> ideal_of {a::'a::ring} <= ideal_of {b}"; |
|
145 by (auto_tac (claset() addIs [dvd_trans_ring], |
|
146 simpset() addsimps [pideal_structure])); |
|
147 qed "dvd_imp_subideal"; |
|
148 |
|
149 Goal "ideal_of {a::'a::ring} <= ideal_of {b} ==> b dvd a"; |
|
150 by (auto_tac (claset() addSDs [subsetD], |
|
151 simpset() addsimps [pideal_structure])); |
|
152 qed "subideal_imp_dvd"; |
|
153 |
|
154 Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = b dvd a"; |
|
155 by (rtac iffI 1); |
|
156 by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1)); |
|
157 qed "subideal_is_dvd"; |
|
158 |
|
159 Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ (a dvd b)"; |
|
160 by (full_simp_tac (simpset() addsimps [psubset_eq, pideal_structure]) 1); |
|
161 by (etac conjE 1); |
|
162 by (dres_inst_tac [("c", "a")] subsetD 1); |
|
163 by (auto_tac (claset() addIs [dvd_trans_ring], |
|
164 simpset())); |
|
165 qed "psubideal_not_dvd"; |
|
166 |
|
167 Goal "[| b dvd a; ~ (a dvd b) |] ==> ideal_of {a::'a::ring} < ideal_of {b}"; |
|
168 by (rtac psubsetI 1); |
|
169 by (rtac dvd_imp_subideal 1 THEN atac 1); |
|
170 by (rtac contrapos 1); by (assume_tac 1); |
|
171 by (rtac subideal_imp_dvd 1); |
|
172 by (Asm_simp_tac 1); |
|
173 qed "not_dvd_psubideal"; |
|
174 |
|
175 Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ (a dvd b))"; |
|
176 by (rtac iffI 1); |
|
177 by (REPEAT (ares_tac |
|
178 [conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1)); |
|
179 by (etac conjE 1); |
|
180 by (REPEAT (ares_tac [not_dvd_psubideal] 1)); |
|
181 qed "psubideal_is_dvd"; |
|
182 |
|
183 Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}"; |
|
184 by (rtac subset_antisym 1); |
|
185 by (REPEAT (ares_tac [dvd_imp_subideal] 1)); |
|
186 qed "assoc_pideal_eq"; |
|
187 |
|
188 AddIffs [subideal_is_dvd, psubideal_is_dvd]; |
|
189 |
|
190 Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})"; |
|
191 by (rtac is_ideal_dvd 1); |
|
192 by (assume_tac 1); |
|
193 by (rtac ideal_of_is_ideal 1); |
|
194 by (rtac generator_in_ideal 1); |
|
195 by (Simp_tac 1); |
|
196 qed "dvd_imp_in_pideal"; |
|
197 |
|
198 Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b"; |
|
199 by (full_simp_tac (simpset() addsimps [pideal_structure]) 1); |
|
200 qed "in_pideal_imp_dvd"; |
|
201 |
|
202 Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"; |
|
203 by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1); |
|
204 by (simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); |
|
205 by (etac contrapos 1); |
|
206 by (rtac in_pideal_imp_dvd 1); |
|
207 by (Asm_simp_tac 1); |
|
208 by (res_inst_tac [("x", "<0>")] exI 1); |
|
209 by (res_inst_tac [("x", "<1>")] exI 1); |
|
210 by (Simp_tac 1); |
|
211 qed "not_dvd_psubideal"; |
|
212 |
|
213 Goalw [irred_def] |
|
214 "[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"; |
|
215 by (dtac is_pidealD 1); |
|
216 by (etac exE 1); |
|
217 by (Clarify_tac 1); |
|
218 by (eres_inst_tac [("x", "aa")] allE 1); |
|
219 by (Clarify_tac 1); |
|
220 by (dres_inst_tac [("a", "<1>")] dvd_imp_subideal 1); |
|
221 by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq])); |
|
222 qed "irred_imp_max_ideal"; |
|
223 |
|
224 (* Pid are factorial *) |
|
225 |
|
226 (* Divisor chain condition *) |
|
227 (* proofs not finished *) |
|
228 |
|
229 Goal "(ALL i. I i <= I (Suc i)) --> (n <= m & a : I n --> a : I m)"; |
|
230 by (rtac impI 1); |
|
231 by (nat_ind_tac "m" 1); |
|
232 by (Blast_tac 1); |
|
233 (* induction step *) |
|
234 by (case_tac "n <= m" 1); |
|
235 by Auto_tac; |
|
236 by (subgoal_tac "n = Suc m" 1); |
|
237 by (hyp_subst_tac 1); |
|
238 by Auto_tac; |
|
239 qed "subset_chain_lemma"; |
|
240 |
|
241 Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] ==> \ |
|
242 \ is_ideal (Union (I``UNIV))"; |
|
243 by (rtac is_idealI 1); |
|
244 by Auto_tac; |
|
245 by (res_inst_tac [("x", "max x xa")] exI 1); |
|
246 by (rtac is_ideal_add 1); |
|
247 by (Asm_simp_tac 1); |
|
248 by (rtac (subset_chain_lemma RS mp RS mp) 1); |
|
249 by (assume_tac 1); |
|
250 by (rtac conjI 1); |
|
251 by (assume_tac 2); |
|
252 by (arith_tac 1); |
|
253 by (rtac (subset_chain_lemma RS mp RS mp) 1); |
|
254 by (assume_tac 1); |
|
255 by (rtac conjI 1); |
|
256 by (assume_tac 2); |
|
257 by (arith_tac 1); |
|
258 by (res_inst_tac [("x", "x")] exI 1); |
|
259 by (Asm_simp_tac 1); |
|
260 by (res_inst_tac [("x", "x")] exI 1); |
|
261 by (Asm_simp_tac 1); |
|
262 qed "chain_is_ideal"; |
|
263 |
|
264 (* |
|
265 Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \ |
|
266 \ EX n. Union ((ideal_of o (%a. {a}))``UNIV) = ideal_of {a n}"; |
|
267 |
|
268 Goal "wf {(a::'a::pid, b). a dvd b & ~ (b dvd a)}"; |
|
269 by (simp_tac (simpset() |
|
270 addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain] |
|
271 delsimps [psubideal_is_dvd]) 1); |
|
272 *) |
|
273 |
|
274 (* Primeness condition *) |
|
275 |
|
276 Goalw [prime_def] "irred a ==> prime (a::'a::pid)"; |
|
277 by (rtac conjI 1); |
|
278 by (rtac conjI 2); |
|
279 by (Clarify_tac 3); |
|
280 by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "<1>")] |
|
281 irred_imp_max_ideal 3); |
|
282 by (auto_tac (claset() addIs [ideal_of_is_ideal, pid_ax], |
|
283 simpset() addsimps [irred_def, not_dvd_psubideal, pid_ax])); |
|
284 by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); |
|
285 by (Clarify_tac 1); |
|
286 by (dres_inst_tac [("f", "op* aa")] arg_cong 1); |
|
287 by (full_simp_tac (simpset() addsimps [r_distr]) 1); |
|
288 by (etac ssubst 1); |
|
289 by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]) 1); |
|
290 qed "pid_irred_imp_prime"; |
|
291 |
|
292 (* Fields are Pid *) |
|
293 |
|
294 Goal "a ~= <0> ==> ideal_of {a::'a::field} = UNIV"; |
|
295 by (rtac subset_antisym 1); |
|
296 by (Simp_tac 1); |
|
297 by (rtac subset_trans 1); |
|
298 by (rtac dvd_imp_subideal 2); |
|
299 by (rtac field_ax 2); |
|
300 by (assume_tac 2); |
|
301 by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1); |
|
302 qed "field_pideal_univ"; |
|
303 |
|
304 Goal "[| is_ideal I; I ~= {<0>} |] ==> {<0>} < I"; |
|
305 by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1); |
|
306 qed "proper_ideal"; |
|
307 |
|
308 Goalw [is_pideal_def] "is_ideal (I::('a::field) set) ==> is_pideal I"; |
|
309 by (case_tac "I = {<0>}" 1); |
|
310 by (res_inst_tac [("x", "<0>")] exI 1); |
|
311 by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1); |
|
312 (* case "I ~= {<0>}" *) |
|
313 by (ftac proper_ideal 1); |
|
314 by (assume_tac 1); |
|
315 by (dtac psubset_imp_ex_mem 1); |
|
316 by (etac exE 1); |
|
317 by (res_inst_tac [("x", "b")] exI 1); |
|
318 by (cut_inst_tac [("a", "b")] element_generates_subideal 1); |
|
319 by (assume_tac 1); by (Blast_tac 1); |
|
320 by (auto_tac (claset(), simpset() addsimps [field_pideal_univ])); |
|
321 qed "field_pid"; |
|
322 |