author | ballarin |
Sat, 10 Feb 2001 08:52:41 +0100 | |
changeset 11093 | 62c2e0af1d30 |
parent 10833 | c0844a30ea4e |
child 11384 | cde6edd51ff6 |
permissions | -rw-r--r-- |
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; \ |
|
11093 | 11 |
\ !! a. a:I ==> - a : I; 0 : I; \ |
7998 | 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 |
||
11093 | 24 |
Goalw [is_ideal_def] "[| is_ideal I |] ==> 0 : I"; |
7998 | 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 |
||
11093 | 40 |
Goalw [is_ideal_def] "is_ideal {0::'a::ring}"; |
7998 | 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); |
|
11093 | 59 |
by (res_inst_tac [("x", "0")] exI 3); |
60 |
by (res_inst_tac [("x", "0")] exI 3); |
|
7998 | 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 |
||
11093 | 81 |
Goalw [ideal_of_def] "ideal_of {} = {0::'a::ring}"; |
7998 | 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); |
|
11093 | 106 |
by (res_inst_tac [("x", "0")] exI 1); |
107 |
by (res_inst_tac [("x", "0")] exI 2); |
|
7998 | 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 |
||
11093 | 117 |
Goal "ideal_of {0::'a::ring} = {0}"; |
7998 | 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 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10230
diff
changeset
|
154 |
Goal "(ideal_of {a::'a::ring} <= ideal_of {b}) = (b dvd a)"; |
7998 | 155 |
by (rtac iffI 1); |
156 |
by (REPEAT (ares_tac [subideal_imp_dvd, dvd_imp_subideal] 1)); |
|
157 |
qed "subideal_is_dvd"; |
|
158 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10230
diff
changeset
|
159 |
Goal "(ideal_of {a::'a::ring} < ideal_of {b}) ==> ~ a dvd b"; |
7998 | 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 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10230
diff
changeset
|
167 |
Goal "[| b dvd a; ~ a dvd b |] ==> ideal_of {a::'a::ring} < ideal_of {b}"; |
7998 | 168 |
by (rtac psubsetI 1); |
10198 | 169 |
by (etac dvd_imp_subideal 1); |
170 |
by (blast_tac (claset() addIs [dvd_imp_subideal, subideal_imp_dvd]) 1); |
|
7998 | 171 |
qed "not_dvd_psubideal"; |
172 |
||
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10230
diff
changeset
|
173 |
Goal "(ideal_of {a::'a::ring} < ideal_of {b}) = (b dvd a & ~ a dvd b)"; |
7998 | 174 |
by (rtac iffI 1); |
175 |
by (REPEAT (ares_tac |
|
176 |
[conjI, psubideal_not_dvd, psubset_imp_subset RS subideal_imp_dvd] 1)); |
|
177 |
by (etac conjE 1); |
|
178 |
by (REPEAT (ares_tac [not_dvd_psubideal] 1)); |
|
179 |
qed "psubideal_is_dvd"; |
|
180 |
||
181 |
Goal "[| a dvd b; b dvd a |] ==> ideal_of {a::'a::ring} = ideal_of {b}"; |
|
182 |
by (rtac subset_antisym 1); |
|
183 |
by (REPEAT (ares_tac [dvd_imp_subideal] 1)); |
|
184 |
qed "assoc_pideal_eq"; |
|
185 |
||
186 |
AddIffs [subideal_is_dvd, psubideal_is_dvd]; |
|
187 |
||
188 |
Goal "!!a::'a::ring. a dvd b ==> b : (ideal_of {a})"; |
|
189 |
by (rtac is_ideal_dvd 1); |
|
190 |
by (assume_tac 1); |
|
191 |
by (rtac ideal_of_is_ideal 1); |
|
192 |
by (rtac generator_in_ideal 1); |
|
193 |
by (Simp_tac 1); |
|
194 |
qed "dvd_imp_in_pideal"; |
|
195 |
||
196 |
Goal "!!a::'a::ring. b : (ideal_of {a}) ==> a dvd b"; |
|
197 |
by (full_simp_tac (simpset() addsimps [pideal_structure]) 1); |
|
198 |
qed "in_pideal_imp_dvd"; |
|
199 |
||
200 |
Goal "~ (a dvd b) ==> ideal_of {a::'a::ring} < ideal_of {a, b}"; |
|
201 |
by (asm_simp_tac (simpset() addsimps [psubset_eq, ideal_of_mono]) 1); |
|
10230 | 202 |
by (etac contrapos_pp 1); |
203 |
by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); |
|
7998 | 204 |
by (rtac in_pideal_imp_dvd 1); |
205 |
by (Asm_simp_tac 1); |
|
11093 | 206 |
by (res_inst_tac [("x", "0")] exI 1); |
7998 | 207 |
by (res_inst_tac [("x", "<1>")] exI 1); |
208 |
by (Simp_tac 1); |
|
209 |
qed "not_dvd_psubideal"; |
|
210 |
||
211 |
Goalw [irred_def] |
|
212 |
"[| irred (a::'a::ring); is_pideal I; ideal_of {a} < I |] ==> x : I"; |
|
213 |
by (dtac is_pidealD 1); |
|
214 |
by (etac exE 1); |
|
215 |
by (Clarify_tac 1); |
|
216 |
by (eres_inst_tac [("x", "aa")] allE 1); |
|
217 |
by (Clarify_tac 1); |
|
218 |
by (dres_inst_tac [("a", "<1>")] dvd_imp_subideal 1); |
|
219 |
by (auto_tac (claset(), simpset() addsimps [ideal_of_one_eq])); |
|
220 |
qed "irred_imp_max_ideal"; |
|
221 |
||
222 |
(* Pid are factorial *) |
|
223 |
||
224 |
(* Divisor chain condition *) |
|
225 |
(* proofs not finished *) |
|
226 |
||
8707 | 227 |
Goal "(ALL i. I i <= I (Suc i)) ==> (n <= m & a : I n --> a : I m)"; |
228 |
by (induct_tac "m" 1); |
|
7998 | 229 |
by (Blast_tac 1); |
230 |
(* induction step *) |
|
8707 | 231 |
by (rename_tac "m" 1); |
7998 | 232 |
by (case_tac "n <= m" 1); |
233 |
by Auto_tac; |
|
234 |
by (subgoal_tac "n = Suc m" 1); |
|
8707 | 235 |
by (arith_tac 2); |
236 |
by (Force_tac 1); |
|
237 |
qed_spec_mp "subset_chain_lemma"; |
|
7998 | 238 |
|
8707 | 239 |
Goal "[| ALL i. is_ideal (I i); ALL i. I i <= I (Suc i) |] \ |
10833 | 240 |
\ ==> is_ideal (Union (I`UNIV))"; |
7998 | 241 |
by (rtac is_idealI 1); |
242 |
by Auto_tac; |
|
243 |
by (res_inst_tac [("x", "max x xa")] exI 1); |
|
244 |
by (rtac is_ideal_add 1); |
|
245 |
by (Asm_simp_tac 1); |
|
8707 | 246 |
by (rtac subset_chain_lemma 1); |
7998 | 247 |
by (assume_tac 1); |
248 |
by (rtac conjI 1); |
|
249 |
by (assume_tac 2); |
|
250 |
by (arith_tac 1); |
|
8707 | 251 |
by (rtac subset_chain_lemma 1); |
7998 | 252 |
by (assume_tac 1); |
253 |
by (rtac conjI 1); |
|
254 |
by (assume_tac 2); |
|
255 |
by (arith_tac 1); |
|
256 |
by (res_inst_tac [("x", "x")] exI 1); |
|
257 |
by (Asm_simp_tac 1); |
|
258 |
by (res_inst_tac [("x", "x")] exI 1); |
|
259 |
by (Asm_simp_tac 1); |
|
260 |
qed "chain_is_ideal"; |
|
261 |
||
262 |
(* |
|
263 |
Goal "ALL i. ideal_of {a i} < ideal_of {a (Suc i)} ==> \ |
|
10833 | 264 |
\ EX n. Union ((ideal_of o (%a. {a}))`UNIV) = ideal_of {a n}"; |
7998 | 265 |
|
10789
260fa2c67e3e
Changed priority of dvd from 70 to 50 as befits a relation.
nipkow
parents:
10230
diff
changeset
|
266 |
Goal "wf {(a::'a::pid, b). a dvd b & ~ b dvd a}"; |
7998 | 267 |
by (simp_tac (simpset() |
268 |
addsimps [psubideal_is_dvd RS sym, wf_iff_no_infinite_down_chain] |
|
269 |
delsimps [psubideal_is_dvd]) 1); |
|
270 |
*) |
|
271 |
||
272 |
(* Primeness condition *) |
|
273 |
||
274 |
Goalw [prime_def] "irred a ==> prime (a::'a::pid)"; |
|
275 |
by (rtac conjI 1); |
|
276 |
by (rtac conjI 2); |
|
277 |
by (Clarify_tac 3); |
|
278 |
by (dres_inst_tac [("I", "ideal_of {a, b}"), ("x", "<1>")] |
|
279 |
irred_imp_max_ideal 3); |
|
280 |
by (auto_tac (claset() addIs [ideal_of_is_ideal, pid_ax], |
|
281 |
simpset() addsimps [irred_def, not_dvd_psubideal, pid_ax])); |
|
282 |
by (full_simp_tac (simpset() addsimps [ideal_of_2_structure]) 1); |
|
283 |
by (Clarify_tac 1); |
|
284 |
by (dres_inst_tac [("f", "op* aa")] arg_cong 1); |
|
285 |
by (full_simp_tac (simpset() addsimps [r_distr]) 1); |
|
286 |
by (etac ssubst 1); |
|
287 |
by (asm_simp_tac (simpset() addsimps [m_assoc RS sym]) 1); |
|
288 |
qed "pid_irred_imp_prime"; |
|
289 |
||
290 |
(* Fields are Pid *) |
|
291 |
||
11093 | 292 |
Goal "a ~= 0 ==> ideal_of {a::'a::field} = UNIV"; |
7998 | 293 |
by (rtac subset_antisym 1); |
294 |
by (Simp_tac 1); |
|
295 |
by (rtac subset_trans 1); |
|
296 |
by (rtac dvd_imp_subideal 2); |
|
297 |
by (rtac field_ax 2); |
|
298 |
by (assume_tac 2); |
|
299 |
by (simp_tac (simpset() addsimps [ideal_of_one_eq]) 1); |
|
300 |
qed "field_pideal_univ"; |
|
301 |
||
11093 | 302 |
Goal "[| is_ideal I; I ~= {0} |] ==> {0} < I"; |
7998 | 303 |
by (asm_simp_tac (simpset() addsimps [psubset_eq, not_sym, is_ideal_zero]) 1); |
304 |
qed "proper_ideal"; |
|
305 |
||
306 |
Goalw [is_pideal_def] "is_ideal (I::('a::field) set) ==> is_pideal I"; |
|
11093 | 307 |
by (case_tac "I = {0}" 1); |
308 |
by (res_inst_tac [("x", "0")] exI 1); |
|
7998 | 309 |
by (asm_simp_tac (simpset() addsimps [ideal_of_zero_eq]) 1); |
11093 | 310 |
(* case "I ~= {0}" *) |
7998 | 311 |
by (ftac proper_ideal 1); |
312 |
by (assume_tac 1); |
|
313 |
by (dtac psubset_imp_ex_mem 1); |
|
314 |
by (etac exE 1); |
|
315 |
by (res_inst_tac [("x", "b")] exI 1); |
|
316 |
by (cut_inst_tac [("a", "b")] element_generates_subideal 1); |
|
317 |
by (assume_tac 1); by (Blast_tac 1); |
|
318 |
by (auto_tac (claset(), simpset() addsimps [field_pideal_univ])); |
|
319 |
qed "field_pid"; |
|
320 |