7998
|
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 |
|
8707
|
229 |
Goal "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)";
|
|
230 |
by (induct_tac "m" 1);
|
7998
|
231 |
by (Blast_tac 1);
|
|
232 |
(* induction step *)
|
8707
|
233 |
by (rename_tac "m" 1);
|
7998
|
234 |
by (case_tac "n <= m" 1);
|
|
235 |
by Auto_tac;
|
|
236 |
by (subgoal_tac "n = Suc m" 1);
|
8707
|
237 |
by (arith_tac 2);
|
|
238 |
by (Force_tac 1);
|
|
239 |
qed_spec_mp "subset_chain_lemma";
|
7998
|
240 |
|
8707
|
241 |
Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \
|
|
242 |
\ ==> is_ideal (Union (I``UNIV))";
|
7998
|
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);
|
8707
|
248 |
by (rtac subset_chain_lemma 1);
|
7998
|
249 |
by (assume_tac 1);
|
|
250 |
by (rtac conjI 1);
|
|
251 |
by (assume_tac 2);
|
|
252 |
by (arith_tac 1);
|
8707
|
253 |
by (rtac subset_chain_lemma 1);
|
7998
|
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 |
|