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