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