author | kuncar |
Fri, 27 Sep 2013 14:43:26 +0200 | |
changeset 53952 | b2781a3ce958 |
parent 53374 | a14d2a854c02 |
child 55322 | 3bf50e3cd727 |
permissions | -rw-r--r-- |
41959 | 1 |
(* Title: HOL/Number_Theory/MiscAlgebra.thy |
31719 | 2 |
Author: Jeremy Avigad |
3 |
||
31772 | 4 |
These are things that can be added to the Algebra library. |
31719 | 5 |
*) |
6 |
||
7 |
theory MiscAlgebra |
|
31772 | 8 |
imports |
31719 | 9 |
"~~/src/HOL/Algebra/Ring" |
10 |
"~~/src/HOL/Algebra/FiniteProduct" |
|
44106 | 11 |
begin |
31719 | 12 |
|
13 |
(* finiteness stuff *) |
|
14 |
||
44872 | 15 |
lemma bounded_set1_int [intro]: "finite {(x::int). a < x & x < b & P x}" |
31719 | 16 |
apply (subgoal_tac "{x. a < x & x < b & P x} <= {a<..<b}") |
17 |
apply (erule finite_subset) |
|
18 |
apply auto |
|
19 |
done |
|
20 |
||
21 |
||
22 |
(* The rest is for the algebra libraries *) |
|
23 |
||
24 |
(* These go in Group.thy. *) |
|
25 |
||
26 |
(* |
|
27 |
Show that the units in any monoid give rise to a group. |
|
28 |
||
29 |
The file Residues.thy provides some infrastructure to use |
|
30 |
facts about the unit group within the ring locale. |
|
31 |
*) |
|
32 |
||
33 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32479
diff
changeset
|
34 |
definition units_of :: "('a, 'b) monoid_scheme => 'a monoid" where |
31719 | 35 |
"units_of G == (| carrier = Units G, |
36 |
Group.monoid.mult = Group.monoid.mult G, |
|
44106 | 37 |
one = one G |)" |
31719 | 38 |
|
39 |
(* |
|
40 |
||
41 |
lemma (in monoid) Units_mult_closed [intro]: |
|
42 |
"x : Units G ==> y : Units G ==> x \<otimes> y : Units G" |
|
43 |
apply (unfold Units_def) |
|
44 |
apply (clarsimp) |
|
45 |
apply (rule_tac x = "xaa \<otimes> xa" in bexI) |
|
46 |
apply auto |
|
47 |
apply (subst m_assoc) |
|
48 |
apply auto |
|
49 |
apply (subst (2) m_assoc [symmetric]) |
|
50 |
apply auto |
|
51 |
apply (subst m_assoc) |
|
52 |
apply auto |
|
53 |
apply (subst (2) m_assoc [symmetric]) |
|
54 |
apply auto |
|
55 |
done |
|
56 |
||
57 |
*) |
|
58 |
||
59 |
lemma (in monoid) units_group: "group(units_of G)" |
|
60 |
apply (unfold units_of_def) |
|
61 |
apply (rule groupI) |
|
62 |
apply auto |
|
63 |
apply (subst m_assoc) |
|
64 |
apply auto |
|
65 |
apply (rule_tac x = "inv x" in bexI) |
|
66 |
apply auto |
|
44872 | 67 |
done |
31719 | 68 |
|
69 |
lemma (in comm_monoid) units_comm_group: "comm_group(units_of G)" |
|
70 |
apply (rule group.group_comm_groupI) |
|
71 |
apply (rule units_group) |
|
41541 | 72 |
apply (insert comm_monoid_axioms) |
31719 | 73 |
apply (unfold units_of_def Units_def comm_monoid_def comm_monoid_axioms_def) |
41541 | 74 |
apply auto |
75 |
done |
|
31719 | 76 |
|
77 |
lemma units_of_carrier: "carrier (units_of G) = Units G" |
|
44872 | 78 |
unfolding units_of_def by auto |
31719 | 79 |
|
80 |
lemma units_of_mult: "mult(units_of G) = mult G" |
|
44872 | 81 |
unfolding units_of_def by auto |
31719 | 82 |
|
83 |
lemma units_of_one: "one(units_of G) = one G" |
|
44872 | 84 |
unfolding units_of_def by auto |
31719 | 85 |
|
44872 | 86 |
lemma (in monoid) units_of_inv: "x : Units G ==> |
31719 | 87 |
m_inv (units_of G) x = m_inv G x" |
88 |
apply (rule sym) |
|
89 |
apply (subst m_inv_def) |
|
90 |
apply (rule the1_equality) |
|
91 |
apply (rule ex_ex1I) |
|
92 |
apply (subst (asm) Units_def) |
|
93 |
apply auto |
|
94 |
apply (erule inv_unique) |
|
95 |
apply auto |
|
96 |
apply (rule Units_closed) |
|
97 |
apply (simp_all only: units_of_carrier [symmetric]) |
|
98 |
apply (insert units_group) |
|
99 |
apply auto |
|
100 |
apply (subst units_of_mult [symmetric]) |
|
101 |
apply (subst units_of_one [symmetric]) |
|
102 |
apply (erule group.r_inv, assumption) |
|
103 |
apply (subst units_of_mult [symmetric]) |
|
104 |
apply (subst units_of_one [symmetric]) |
|
105 |
apply (erule group.l_inv, assumption) |
|
106 |
done |
|
107 |
||
44872 | 108 |
lemma (in group) inj_on_const_mult: "a: (carrier G) ==> |
31719 | 109 |
inj_on (%x. a \<otimes> x) (carrier G)" |
44872 | 110 |
unfolding inj_on_def by auto |
31719 | 111 |
|
112 |
lemma (in group) surj_const_mult: "a : (carrier G) ==> |
|
44872 | 113 |
(%x. a \<otimes> x) ` (carrier G) = (carrier G)" |
31719 | 114 |
apply (auto simp add: image_def) |
115 |
apply (rule_tac x = "(m_inv G a) \<otimes> x" in bexI) |
|
116 |
apply auto |
|
117 |
(* auto should get this. I suppose we need "comm_monoid_simprules" |
|
118 |
for mult_ac rewriting. *) |
|
119 |
apply (subst m_assoc [symmetric]) |
|
120 |
apply auto |
|
44872 | 121 |
done |
31719 | 122 |
|
123 |
lemma (in group) l_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> |
|
124 |
(x \<otimes> a = x) = (a = one G)" |
|
125 |
apply auto |
|
126 |
apply (subst l_cancel [symmetric]) |
|
127 |
prefer 4 |
|
128 |
apply (erule ssubst) |
|
129 |
apply auto |
|
44872 | 130 |
done |
31719 | 131 |
|
132 |
lemma (in group) r_cancel_one [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> |
|
133 |
(a \<otimes> x = x) = (a = one G)" |
|
134 |
apply auto |
|
135 |
apply (subst r_cancel [symmetric]) |
|
136 |
prefer 4 |
|
137 |
apply (erule ssubst) |
|
138 |
apply auto |
|
44872 | 139 |
done |
31719 | 140 |
|
141 |
(* Is there a better way to do this? *) |
|
142 |
||
143 |
lemma (in group) l_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> |
|
144 |
(x = x \<otimes> a) = (a = one G)" |
|
44872 | 145 |
apply (subst eq_commute) |
146 |
apply simp |
|
147 |
done |
|
31719 | 148 |
|
149 |
lemma (in group) r_cancel_one' [simp]: "x : carrier G \<Longrightarrow> a : carrier G \<Longrightarrow> |
|
150 |
(x = a \<otimes> x) = (a = one G)" |
|
44872 | 151 |
apply (subst eq_commute) |
152 |
apply simp |
|
153 |
done |
|
31719 | 154 |
|
155 |
(* This should be generalized to arbitrary groups, not just commutative |
|
156 |
ones, using Lagrange's theorem. *) |
|
157 |
||
158 |
lemma (in comm_group) power_order_eq_one: |
|
44872 | 159 |
assumes fin [simp]: "finite (carrier G)" |
160 |
and a [simp]: "a : carrier G" |
|
161 |
shows "a (^) card(carrier G) = one G" |
|
31719 | 162 |
proof - |
163 |
have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)" |
|
44872 | 164 |
by (subst (2) finprod_reindex [symmetric], |
31719 | 165 |
auto simp add: Pi_def inj_on_const_mult surj_const_mult) |
166 |
also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)" |
|
167 |
by (auto simp add: finprod_multf Pi_def) |
|
168 |
also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)" |
|
169 |
by (auto simp add: finprod_const) |
|
170 |
finally show ?thesis |
|
171 |
(* uses the preceeding lemma *) |
|
172 |
by auto |
|
173 |
qed |
|
174 |
||
175 |
||
176 |
(* Miscellaneous *) |
|
177 |
||
178 |
lemma (in cring) field_intro2: "\<zero>\<^bsub>R\<^esub> ~= \<one>\<^bsub>R\<^esub> \<Longrightarrow> ALL x : carrier R - {\<zero>\<^bsub>R\<^esub>}. |
|
179 |
x : Units R \<Longrightarrow> field R" |
|
180 |
apply (unfold_locales) |
|
41541 | 181 |
apply (insert cring_axioms, auto) |
31719 | 182 |
apply (rule trans) |
183 |
apply (subgoal_tac "a = (a \<otimes> b) \<otimes> inv b") |
|
184 |
apply assumption |
|
44872 | 185 |
apply (subst m_assoc) |
41541 | 186 |
apply auto |
31719 | 187 |
apply (unfold Units_def) |
188 |
apply auto |
|
41541 | 189 |
done |
31719 | 190 |
|
191 |
lemma (in monoid) inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow> |
|
41541 | 192 |
x \<otimes> y = \<one> \<Longrightarrow> y \<otimes> x = \<one> \<Longrightarrow> inv x = y" |
31719 | 193 |
apply (subgoal_tac "x : Units G") |
194 |
apply (subgoal_tac "y = inv x \<otimes> \<one>") |
|
195 |
apply simp |
|
196 |
apply (erule subst) |
|
197 |
apply (subst m_assoc [symmetric]) |
|
198 |
apply auto |
|
199 |
apply (unfold Units_def) |
|
200 |
apply auto |
|
41541 | 201 |
done |
31719 | 202 |
|
203 |
lemma (in comm_monoid) comm_inv_char: "x : carrier G \<Longrightarrow> y : carrier G \<Longrightarrow> |
|
204 |
x \<otimes> y = \<one> \<Longrightarrow> inv x = y" |
|
205 |
apply (rule inv_char) |
|
206 |
apply auto |
|
44872 | 207 |
apply (subst m_comm, auto) |
41541 | 208 |
done |
31719 | 209 |
|
44872 | 210 |
lemma (in ring) inv_neg_one [simp]: "inv (\<ominus> \<one>) = \<ominus> \<one>" |
31719 | 211 |
apply (rule inv_char) |
212 |
apply (auto simp add: l_minus r_minus) |
|
41541 | 213 |
done |
31719 | 214 |
|
44872 | 215 |
lemma (in monoid) inv_eq_imp_eq: "x : Units G \<Longrightarrow> y : Units G \<Longrightarrow> |
31719 | 216 |
inv x = inv y \<Longrightarrow> x = y" |
217 |
apply (subgoal_tac "inv(inv x) = inv(inv y)") |
|
218 |
apply (subst (asm) Units_inv_inv)+ |
|
219 |
apply auto |
|
44872 | 220 |
done |
31719 | 221 |
|
222 |
lemma (in ring) Units_minus_one_closed [intro]: "\<ominus> \<one> : Units R" |
|
223 |
apply (unfold Units_def) |
|
224 |
apply auto |
|
225 |
apply (rule_tac x = "\<ominus> \<one>" in bexI) |
|
226 |
apply auto |
|
227 |
apply (simp add: l_minus r_minus) |
|
44872 | 228 |
done |
31719 | 229 |
|
230 |
lemma (in monoid) inv_one [simp]: "inv \<one> = \<one>" |
|
231 |
apply (rule inv_char) |
|
232 |
apply auto |
|
44872 | 233 |
done |
31719 | 234 |
|
235 |
lemma (in ring) inv_eq_neg_one_eq: "x : Units R \<Longrightarrow> (inv x = \<ominus> \<one>) = (x = \<ominus> \<one>)" |
|
236 |
apply auto |
|
237 |
apply (subst Units_inv_inv [symmetric]) |
|
238 |
apply auto |
|
44872 | 239 |
done |
31719 | 240 |
|
241 |
lemma (in monoid) inv_eq_one_eq: "x : Units G \<Longrightarrow> (inv x = \<one>) = (x = \<one>)" |
|
242 |
apply auto |
|
243 |
apply (subst Units_inv_inv [symmetric]) |
|
244 |
apply auto |
|
44872 | 245 |
done |
31719 | 246 |
|
247 |
||
248 |
(* This goes in FiniteProduct *) |
|
249 |
||
250 |
lemma (in comm_monoid) finprod_UN_disjoint: |
|
251 |
"finite I \<Longrightarrow> (ALL i:I. finite (A i)) \<longrightarrow> (ALL i:I. ALL j:I. i ~= j \<longrightarrow> |
|
252 |
(A i) Int (A j) = {}) \<longrightarrow> |
|
253 |
(ALL i:I. ALL x: (A i). g x : carrier G) \<longrightarrow> |
|
254 |
finprod G g (UNION I A) = finprod G (%i. finprod G g (A i)) I" |
|
255 |
apply (induct set: finite) |
|
256 |
apply force |
|
257 |
apply clarsimp |
|
258 |
apply (subst finprod_Un_disjoint) |
|
259 |
apply blast |
|
260 |
apply (erule finite_UN_I) |
|
261 |
apply blast |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
44872
diff
changeset
|
262 |
apply (fastforce) |
44872 | 263 |
apply (auto intro!: funcsetI finprod_closed) |
264 |
done |
|
31719 | 265 |
|
266 |
lemma (in comm_monoid) finprod_Union_disjoint: |
|
267 |
"[| finite C; (ALL A:C. finite A & (ALL x:A. f x : carrier G)); |
|
44872 | 268 |
(ALL A:C. ALL B:C. A ~= B --> A Int B = {}) |] |
269 |
==> finprod G f (Union C) = finprod G (finprod G f) C" |
|
31719 | 270 |
apply (frule finprod_UN_disjoint [of C id f]) |
44106 | 271 |
apply (auto simp add: SUP_def) |
44872 | 272 |
done |
31719 | 273 |
|
44872 | 274 |
lemma (in comm_monoid) finprod_one: |
275 |
"finite A \<Longrightarrow> (\<And>x. x:A \<Longrightarrow> f x = \<one>) \<Longrightarrow> finprod G f A = \<one>" |
|
276 |
by (induct set: finite) auto |
|
31719 | 277 |
|
278 |
||
279 |
(* need better simplification rules for rings *) |
|
280 |
(* the next one holds more generally for abelian groups *) |
|
281 |
||
282 |
lemma (in cring) sum_zero_eq_neg: |
|
44872 | 283 |
"x : carrier R \<Longrightarrow> y : carrier R \<Longrightarrow> x \<oplus> y = \<zero> \<Longrightarrow> x = \<ominus> y" |
284 |
apply (subgoal_tac "\<ominus> y = \<zero> \<oplus> \<ominus> y") |
|
31719 | 285 |
apply (erule ssubst)back |
286 |
apply (erule subst) |
|
41541 | 287 |
apply (simp_all add: ring_simprules) |
288 |
done |
|
31719 | 289 |
|
290 |
(* there's a name conflict -- maybe "domain" should be |
|
291 |
"integral_domain" *) |
|
292 |
||
44872 | 293 |
lemma (in Ring.domain) square_eq_one: |
31719 | 294 |
fixes x |
295 |
assumes [simp]: "x : carrier R" and |
|
296 |
"x \<otimes> x = \<one>" |
|
297 |
shows "x = \<one> | x = \<ominus>\<one>" |
|
298 |
proof - |
|
299 |
have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = x \<otimes> x \<oplus> \<ominus> \<one>" |
|
300 |
by (simp add: ring_simprules) |
|
53374
a14d2a854c02
tuned proofs -- clarified flow of facts wrt. calculation;
wenzelm
parents:
44890
diff
changeset
|
301 |
also from `x \<otimes> x = \<one>` have "\<dots> = \<zero>" |
31719 | 302 |
by (simp add: ring_simprules) |
303 |
finally have "(x \<oplus> \<one>) \<otimes> (x \<oplus> \<ominus> \<one>) = \<zero>" . |
|
44872 | 304 |
then have "(x \<oplus> \<one>) = \<zero> | (x \<oplus> \<ominus> \<one>) = \<zero>" |
31719 | 305 |
by (intro integral, auto) |
44872 | 306 |
then show ?thesis |
31719 | 307 |
apply auto |
308 |
apply (erule notE) |
|
309 |
apply (rule sum_zero_eq_neg) |
|
310 |
apply auto |
|
311 |
apply (subgoal_tac "x = \<ominus> (\<ominus> \<one>)") |
|
44872 | 312 |
apply (simp add: ring_simprules) |
31719 | 313 |
apply (rule sum_zero_eq_neg) |
314 |
apply auto |
|
315 |
done |
|
316 |
qed |
|
317 |
||
318 |
lemma (in Ring.domain) inv_eq_self: "x : Units R \<Longrightarrow> |
|
319 |
x = inv x \<Longrightarrow> x = \<one> | x = \<ominus> \<one>" |
|
320 |
apply (rule square_eq_one) |
|
321 |
apply auto |
|
322 |
apply (erule ssubst)back |
|
323 |
apply (erule Units_r_inv) |
|
44872 | 324 |
done |
31719 | 325 |
|
326 |
||
327 |
(* |
|
328 |
The following translates theorems about groups to the facts about |
|
329 |
the units of a ring. (The list should be expanded as more things are |
|
330 |
needed.) |
|
331 |
*) |
|
332 |
||
44872 | 333 |
lemma (in ring) finite_ring_finite_units [intro]: |
334 |
"finite (carrier R) \<Longrightarrow> finite (Units R)" |
|
335 |
by (rule finite_subset) auto |
|
31719 | 336 |
|
337 |
(* this belongs with MiscAlgebra.thy *) |
|
44872 | 338 |
lemma (in monoid) units_of_pow: |
31719 | 339 |
"x : Units G \<Longrightarrow> x (^)\<^bsub>units_of G\<^esub> (n::nat) = x (^)\<^bsub>G\<^esub> n" |
340 |
apply (induct n) |
|
44872 | 341 |
apply (auto simp add: units_group group.is_monoid |
41541 | 342 |
monoid.nat_pow_0 monoid.nat_pow_Suc units_of_one units_of_mult) |
343 |
done |
|
31719 | 344 |
|
345 |
lemma (in cring) units_power_order_eq_one: "finite (Units R) \<Longrightarrow> a : Units R |
|
346 |
\<Longrightarrow> a (^) card(Units R) = \<one>" |
|
347 |
apply (subst units_of_carrier [symmetric]) |
|
348 |
apply (subst units_of_one [symmetric]) |
|
349 |
apply (subst units_of_pow [symmetric]) |
|
350 |
apply assumption |
|
351 |
apply (rule comm_group.power_order_eq_one) |
|
352 |
apply (rule units_comm_group) |
|
353 |
apply (unfold units_of_def, auto) |
|
41541 | 354 |
done |
31719 | 355 |
|
356 |
end |