monoidScript.sml
1(* ------------------------------------------------------------------------- *)
2(* Monoid Theory *)
3(* ========================================================================= *)
4(* A monoid is a semi-group with an identity. *)
5(* The units of a monoid form a group. *)
6(* A finite, cancellative monoid is also a group. *)
7(* ------------------------------------------------------------------------- *)
8(* Monoid *)
9(* Monoid Order and Invertibles *)
10(* Monoid Maps *)
11(* Submonoid *)
12(* Applying Monoid Theory: Monoid Instances *)
13(* Theory about folding a monoid (or group) operation over a bag of elements *)
14(* ------------------------------------------------------------------------- *)
15(* (Joseph) Hing-Lun Chan, The Australian National University, 2014-2019 *)
16(* ------------------------------------------------------------------------- *)
17
18(*===========================================================================*)
19
20Theory monoid
21Ancestors
22 pred_set arithmetic divides gcd logroot list rich_list bag
23 gcdset number combinatorics prime
24Libs
25 jcLib dep_rewrite
26
27
28(* val _ = load "jcLib"; *)
29
30(* ------------------------------------------------------------------------- *)
31(* Monoid Documentation *)
32(* ------------------------------------------------------------------------- *)
33(* Data type:
34 The generic symbol for monoid data is g.
35 g.carrier = Carrier set of monoid, overloaded as G.
36 g.op = Binary operation of monoid, overloaded as *.
37 g.id = Identity element of monoid, overloaded as #e.
38
39 Overloading:
40 * = g.op
41 #e = g.id
42 ** = g.exp
43 G = g.carrier
44 GITSET g s b = ITSET g.op s b
45*)
46(* Definitions and Theorems (# are exported):
47
48 Definitions:
49 Monoid_def |- !g. Monoid g <=>
50 (!x y. x IN G /\ y IN G ==> x * y IN G) /\
51 (!x y z. x IN G /\ y IN G /\ z IN G ==> ((x * y) * z = x * (y * z))) /\
52 #e IN G /\ (!x. x IN G ==> (#e * x = x) /\ (x * #e = x))
53 AbelianMonoid_def |- !g. AbelianMonoid g <=> Monoid g /\ !x y. x IN G /\ y IN G ==> (x * y = y * x)
54# FiniteMonoid_def |- !g. FiniteMonoid g <=> Monoid g /\ FINITE G
55# FiniteAbelianMonoid_def |- !g. FiniteAbelianMonoid g <=> AbelianMonoid g /\ FINITE G
56
57 Extract from definition:
58# monoid_id_element |- !g. Monoid g ==> #e IN G
59# monoid_op_element |- !g. Monoid g ==> !x y. x IN G /\ y IN G ==> x * y IN G
60 monoid_assoc |- !g. Monoid g ==> !x y z. x IN G /\ y IN G /\ z IN G ==> (x * y * z = x * (y * z))
61 monoid_id |- !g. Monoid g ==> !x. x IN G ==> (#e * x = x) /\ (x * #e = x)
62# monoid_lid |- !g. Monoid g ==> !x. x IN G ==> (#e * x = x)
63# monoid_rid |- !g. Monoid g ==> !x. x IN G ==> (x * #e = x)
64# monoid_id_id |- !g. Monoid g ==> (#e * #e = #e)
65
66 Simple theorems:
67 FiniteAbelianMonoid_def_alt |- !g. FiniteAbelianMonoid g <=> FiniteMonoid g /\ !x y. x IN G /\ y IN G ==> (x * y = y * x)
68 monoid_carrier_nonempty |- !g. Monoid g ==> G <> {}
69 monoid_lid_unique |- !g. Monoid g ==> !e. e IN G ==> (!x. x IN G ==> (e * x = x)) ==> (e = #e)
70 monoid_rid_unique |- !g. Monoid g ==> !e. e IN G ==> (!x. x IN G ==> (x * e = x)) ==> (e = #e)
71 monoid_id_unique |- !g. Monoid g ==> !e. e IN G ==> ((!x. x IN G ==> (x * e = x) /\ (e * x = x)) <=> (e = #e))
72
73 Iteration of the binary operation gives exponentiation:
74 monoid_exp_def |- !g x n. x ** n = FUNPOW ($* x) n #e
75# monoid_exp_0 |- !g x. x ** 0 = #e
76# monoid_exp_SUC |- !g x n. x ** SUC n = x * x ** n
77# monoid_exp_element |- !g. Monoid g ==> !x. x IN G ==> !n. x ** n IN G
78# monoid_exp_1 |- !g. Monoid g ==> !x. x IN G ==> (x ** 1 = x)
79# monoid_id_exp |- !g. Monoid g ==> !n. #e ** n = #e
80
81 Monoid commutative elements:
82 monoid_comm_exp |- !g. Monoid g ==> !x y. x IN G /\ y IN G ==> (x * y = y * x) ==> !n. x ** n * y = y * x ** n
83 monoid_exp_comm |- !g. Monoid g ==> !x. x IN G ==> !n. x ** n * x = x * x ** n
84# monoid_exp_suc |- !g. Monoid g ==> !x. x IN G ==> !n. x ** SUC n = x ** n * x
85 monoid_comm_op_exp |- !g. Monoid g ==> !x y. x IN G /\ y IN G /\ (x * y = y * x) ==>
86 !n. (x * y) ** n = x ** n * y ** n
87 monoid_comm_exp_exp |- !g. Monoid g ==> !x y. x IN G /\ y IN G /\ (x * y = y * x) ==>
88 !n m. x ** n * y ** m = y ** m * x ** n
89# monoid_exp_add |- !g. Monoid g ==> !x. x IN G ==> !n k. x ** (n + k) = x ** n * x ** k
90# monoid_exp_mult |- !g. Monoid g ==> !x. x IN G ==> !n k. x ** (n * k) = (x ** n) ** k
91 monoid_exp_mult_comm |- !g. Monoid g ==> !x. x IN G ==> !m n. (x ** m) ** n = (x ** n) ** m
92
93
94 Finite Monoid:
95 finite_monoid_exp_not_distinct |- !g. FiniteMonoid g ==> !x. x IN G ==>
96 ?h k. (x ** h = x ** k) /\ h <> k
97
98 Abelian Monoid ITSET Theorems:
99 GITSET_THM |- !s g b. FINITE s ==> (GITSET g s b = if s = {} then b
100 else GITSET g (REST s) (CHOICE s * b))
101 GITSET_EMPTY |- !g b. GITSET g {} b = b
102 GITSET_INSERT |- !x. FINITE s ==>
103 !x g b. (GITSET g (x INSERT s) b = GITSET g (REST (x INSERT s)) (CHOICE (x INSERT s) * b))
104 GITSET_PROPERTY |- !g s. FINITE s /\ s <> {} ==> !b. GITSET g s b = GITSET g (REST s) (CHOICE s * b)
105
106 abelian_monoid_op_closure_comm_assoc_fun |- !g. AbelianMonoid g ==> closure_comm_assoc_fun $* G
107 COMMUTING_GITSET_INSERT |- !g s. AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
108 !b x::G. GITSET g (x INSERT s) b = GITSET g (s DELETE x) (x * b)
109 COMMUTING_GITSET_REDUCTION |- !g s. AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
110 !b x::G. GITSET g s (x * b) = x * GITSET g s b
111 COMMUTING_GITSET_RECURSES |- !g s. AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
112 !b x::G. GITSET g (x INSERT s) b = x * GITSET g (s DELETE x) b:
113
114 Abelian Monoid PROD_SET:
115 GPROD_SET_def |- !g s. GPROD_SET g s = GITSET g s #e
116 GPROD_SET_THM |- !g s. (GPROD_SET g {} = #e) /\
117 (AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
118 !x::(G). GPROD_SET g (x INSERT s) = x * GPROD_SET g (s DELETE x))
119 GPROD_SET_EMPTY |- !g s. GPROD_SET g {} = #e
120 GPROD_SET_SING |- !g. Monoid g ==> !x. x IN G ==> (GPROD_SET g {x} = x)
121 GPROD_SET_PROPERTY |- !g s. AbelianMonoid g /\ FINITE s /\ s SUBSET G ==> GPROD_SET g s IN G
122
123*)
124
125(* ------------------------------------------------------------------------- *)
126(* Monoid Definition. *)
127(* ------------------------------------------------------------------------- *)
128
129(* Monoid and Group share the same type *)
130
131(* Set up monoid type as a record
132 A Monoid has:
133 . a carrier set (set = function 'a -> bool, since MEM is a boolean function)
134 . a binary operation (2-nary function) called multiplication
135 . an identity element for the binary operation
136*)
137Datatype:
138 monoid = <| carrier: 'a -> bool;
139 op: 'a -> 'a -> 'a;
140 id: 'a
141 |>
142End
143(* If the field inv: 'a -> 'a; is included,
144 there will be an implicit monoid_inv accessor generated.
145 Later, when monoid_inv_def defines another monoid_inv,
146 the monoid_accessors will ALL be invalidated!
147 So, do not include the field inv here,
148 but use add_record_field ("inv", ``monoid_inv``)
149 to achieve the same effect.
150*)
151
152(* Using symbols m for monoid and g for group
153 will give excessive overloading for Monoid and Group,
154 so the generic symbol for both is taken as g. *)
155(* set overloading *)
156Overload "*" = ``g.op``
157Overload "#e" = ``g.id``
158Overload G = ``g.carrier``
159
160(* Monoid Definition:
161 A Monoid is a set with elements of type 'a monoid, such that
162 . Closure: x * y is in the carrier set
163 . Associativity: (x * y) * z = x * (y * z))
164 . Existence of identity: #e is in the carrier set
165 . Property of identity: #e * x = x * #e = x
166*)
167(* Define Monoid by predicate *)
168Definition Monoid_def:
169 Monoid (g:'a monoid) <=>
170 (!x y. x IN G /\ y IN G ==> x * y IN G) /\
171 (!x y z. x IN G /\ y IN G /\ z IN G ==> ((x * y) * z = x * (y * z))) /\
172 #e IN G /\ (!x. x IN G ==> (#e * x = x) /\ (x * #e = x))
173End
174(* export basic definition -- but too many and's. *)
175(* val _ = export_rewrites ["Monoid_def"]; *)
176
177(* ------------------------------------------------------------------------- *)
178(* More Monoid Defintions. *)
179(* ------------------------------------------------------------------------- *)
180
181(* Abelian Monoid = a Monoid that is commutative: x * y = y * x. *)
182Definition AbelianMonoid_def:
183 AbelianMonoid (g:'a monoid) <=>
184 Monoid g /\ !x y. x IN G /\ y IN G ==> (x * y = y * x)
185End
186(* export simple definition -- but this one has commutativity, so don't. *)
187(* val _ = export_rewrites ["AbelianMonoid_def"]; *)
188
189(* Finite Monoid = a Monoid with a finite carrier set. *)
190Definition FiniteMonoid_def[simp]:
191 FiniteMonoid (g:'a monoid) <=>
192 Monoid g /\ FINITE G
193End
194
195(* Finite Abelian Monoid = a Monoid that is both Finite and Abelian. *)
196Definition FiniteAbelianMonoid_def[simp]:
197 FiniteAbelianMonoid (g:'a monoid) <=>
198 AbelianMonoid g /\ FINITE G
199End
200
201(* ------------------------------------------------------------------------- *)
202(* Basic theorems from definition. *)
203(* ------------------------------------------------------------------------- *)
204
205(* Theorem: Finite Abelian Monoid = Finite Monoid /\ commutativity. *)
206(* Proof: by definitions. *)
207Theorem FiniteAbelianMonoid_def_alt:
208 !g:'a monoid. FiniteAbelianMonoid g <=>
209 FiniteMonoid g /\ !x y. x IN G /\ y IN G ==> (x * y = y * x)
210Proof
211 rw[AbelianMonoid_def, EQ_IMP_THM]
212QED
213
214(* Monoid clauses from definition, in implicative form, no for-all, internal use only. *)
215val monoid_clauses = Monoid_def |> SPEC_ALL |> #1 o EQ_IMP_RULE;
216(* > val monoid_clauses =
217 |- Monoid g ==>
218 (!x y. x IN G /\ y IN G ==> x * y IN G) /\
219 (!x y z. x IN G /\ y IN G /\ z IN G ==> (x * y * z = x * (y * z))) /\
220 #e IN G /\ !x. x IN G ==> (#e * x = x) /\ (x * #e = x) : thm *)
221
222(* Extract theorems from Monoid clauses. *)
223(* No need to export as definition is already exported. *)
224
225(* Theorem: [Closure] x * y in carrier. *)
226Theorem monoid_op_element[simp] =
227 monoid_clauses |> UNDISCH_ALL |> CONJUNCT1 |> DISCH_ALL |> GEN_ALL;
228(* > val monoid_op_element = |- !g. Monoid g ==> !x y. x IN G /\ y IN G ==> x * y IN G : thm*)
229
230(* Theorem: [Associativity] (x * y) * z = x * (y * z) *)
231Theorem monoid_assoc =
232 monoid_clauses |> UNDISCH_ALL |> CONJUNCT2|> CONJUNCT1 |> DISCH_ALL |> GEN_ALL;
233(* > val monoid_assoc = |- !g. Monoid g ==> !x y z. x IN G /\ y IN G /\ z IN G ==> (x * y * z = x * (y * z)) : thm *)
234
235(* Theorem: [Identity exists] #e in carrier. *)
236Theorem monoid_id_element[simp] =
237 monoid_clauses |> UNDISCH_ALL |> CONJUNCT2|> CONJUNCT2 |> CONJUNCT1 |> DISCH_ALL |> GEN_ALL;
238(* > val monoid_id_element = |- !g. Monoid g ==> #e IN G : thm *)
239
240(* Theorem: [Identity property] #e * x = x and x * #e = x *)
241Theorem monoid_id =
242 monoid_clauses |> UNDISCH_ALL |> CONJUNCT2|> CONJUNCT2 |> CONJUNCT2 |> DISCH_ALL |> GEN_ALL;
243(* > val monoid_id = |- !g. Monoid g ==> !x. x IN G ==> (#e * x = x) /\ (x * #e = x) : thm *)
244
245(* Theorem: [Left identity] #e * x = x *)
246(* Proof: from monoid_id. *)
247Theorem monoid_lid[simp] =
248 monoid_id |> SPEC_ALL |> UNDISCH_ALL |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCT1
249 |> DISCH ``x IN G`` |> GEN_ALL |> DISCH_ALL |> GEN_ALL;
250(* > val monoid_lid = |- !g. Monoid g ==> !x. x IN G ==> (#e * x = x) : thm *)
251
252(* Theorem: [Right identity] x * #e = x *)
253(* Proof: from monoid_id. *)
254Theorem monoid_rid[simp] =
255 monoid_id |> SPEC_ALL |> UNDISCH_ALL |> SPEC_ALL |> UNDISCH_ALL |> CONJUNCT2
256 |> DISCH ``x IN G`` |> GEN_ALL |> DISCH_ALL |> GEN_ALL;
257(* > val monoid_rid = |- !g. Monoid g ==> !x. x IN G ==> (x * #e = x) : thm *)
258
259(* Theorem: #e * #e = #e *)
260(* Proof:
261 by monoid_lid and monoid_id_element.
262*)
263Theorem monoid_id_id[simp]:
264 !g:'a monoid. Monoid g ==> (#e * #e = #e)
265Proof
266 rw[]
267QED
268
269
270(* ------------------------------------------------------------------------- *)
271(* Theorems in basic Monoid Theory. *)
272(* ------------------------------------------------------------------------- *)
273
274(* Theorem: [Monoid carrier nonempty] G <> {} *)
275(* Proof: by monoid_id_element. *)
276Theorem monoid_carrier_nonempty:
277 !g:'a monoid. Monoid g ==> G <> {}
278Proof
279 metis_tac[monoid_id_element, MEMBER_NOT_EMPTY]
280QED
281
282(* Theorem: [Left Identity unique] !x. (e * x = x) ==> e = #e *)
283(* Proof:
284 Put x = #e,
285 then e * #e = #e by given
286 but e * #e = e by monoid_rid
287 hence e = #e.
288*)
289Theorem monoid_lid_unique:
290 !g:'a monoid. Monoid g ==> !e. e IN G ==> ((!x. x IN G ==> (e * x = x)) ==> (e = #e))
291Proof
292 metis_tac[monoid_id_element, monoid_rid]
293QED
294
295(* Theorem: [Right Identity unique] !x. (x * e = x) ==> e = #e *)
296(* Proof:
297 Put x = #e,
298 then #e * e = #e by given
299 but #e * e = e by monoid_lid
300 hence e = #e.
301*)
302Theorem monoid_rid_unique:
303 !g:'a monoid. Monoid g ==> !e. e IN G ==> ((!x. x IN G ==> (x * e = x)) ==> (e = #e))
304Proof
305 metis_tac[monoid_id_element, monoid_lid]
306QED
307
308(* Theorem: [Identity unique] !x. (x * e = x) and (e * x = x) <=> e = #e *)
309(* Proof:
310 If e, #e are two identities,
311 For e, put x = #e, #e*e = #e and e*#e = #e
312 For #e, put x = e, e*#e = e and #e*e = e
313 Therefore e = #e.
314*)
315Theorem monoid_id_unique:
316 !g:'a monoid. Monoid g ==> !e. e IN G ==> ((!x. x IN G ==> (x * e = x) /\ (e * x = x)) <=> (e = #e))
317Proof
318 metis_tac[monoid_id_element, monoid_id]
319QED
320
321
322(* ------------------------------------------------------------------------- *)
323(* Application of basic Monoid Theory: *)
324(* Exponentiation - the FUNPOW version of Monoid operation. *)
325(* ------------------------------------------------------------------------- *)
326
327(* Define exponents of a monoid element:
328 For x in Monoid g, x ** 0 = #e
329 x ** (SUC n) = x * (x ** n)
330*)
331(*
332val monoid_exp_def = Define`
333 (monoid_exp m x 0 = g.id) /\
334 (monoid_exp m x (SUC n) = x * (monoid_exp m x n))
335`;
336*)
337Definition monoid_exp_def: monoid_exp (g:'a monoid) (x:'a) n = FUNPOW (g.op x) n #e
338End
339(* val _ = export_rewrites ["monoid_exp_def"]; *)
340(*
341- monoid_exp_def;
342> val it = |- !g x n. x ** n = FUNPOW ($* x) n #e : thm
343*)
344
345(* export simple properties later *)
346(* val _ = export_rewrites ["monoid_exp_def"]; *)
347
348(* Convert exp function to exp field, i.e. g.exp is defined to be monoid_exp. *)
349val _ = add_record_field ("exp", ``monoid_exp``);
350(*
351- type_of ``g.exp``;
352> val it = ``:'a -> num -> 'a`` : hol_type
353*)
354(* overloading *)
355(* val _ = clear_overloads_on "**"; *)
356(* val _ = overload_on ("**", ``monoid_exp g``); -- not this *)
357Overload "**" = ``g.exp``
358
359(* Theorem: x ** 0 = #e *)
360(* Proof: by definition and FUNPOW_0. *)
361Theorem monoid_exp_0[simp]:
362 !g:'a monoid. !x:'a. x ** 0 = #e
363Proof
364 rw[monoid_exp_def]
365QED
366
367
368(* Theorem: x ** (SUC n) = x * (x ** n) *)
369(* Proof: by definition and FUNPOW_SUC. *)
370(* should this be exported? Only FUNPOW_0 is exported. *)
371Theorem monoid_exp_SUC[simp]:
372 !g:'a monoid. !x:'a. !n. x ** (SUC n) = x * (x ** n)
373Proof
374 rw[monoid_exp_def, FUNPOW_SUC]
375QED
376
377
378(* Theorem: (x ** n) in G *)
379(* Proof: by induction on n.
380 Base case: x ** 0 IN G
381 x ** 0 = #e by monoid_exp_0
382 in G by monoid_id_element.
383 Step case: x ** n IN G ==> x ** SUC n IN G
384 x ** SUC n
385 = x * (x ** n) by monoid_exp_SUC
386 in G by monoid_op_element and induction hypothesis
387*)
388Theorem monoid_exp_element[simp]:
389 !g:'a monoid. Monoid g ==> !x. x IN G ==> !n. (x ** n) IN G
390Proof
391 rpt strip_tac>>
392 Induct_on `n` >>
393 rw[]
394QED
395
396
397(* Theorem: x ** 1 = x *)
398(* Proof:
399 x ** 1
400 = x ** SUC 0 by ONE
401 = x * x ** 0 by monoid_exp_SUC
402 = x * #e by monoid_exp_0
403 = x by monoid_rid
404*)
405Theorem monoid_exp_1[simp]:
406 !g:'a monoid. Monoid g ==> !x. x IN G ==> (x ** 1 = x)
407Proof
408 rewrite_tac[ONE] >>
409 rw[]
410QED
411
412
413(* Theorem: (#e ** n) = #e *)
414(* Proof: by induction on n.
415 Base case: #e ** 0 = #e
416 true by monoid_exp_0.
417 Step case: #e ** n = #e ==> #e ** SUC n = #e
418 #e ** SUC n
419 = #e * #e ** n by monoid_exp_SUC, monoid_id_element
420 = #e ** n by monoid_lid, monoid_exp_element
421 hence true by induction hypothesis.
422*)
423Theorem monoid_id_exp[simp]:
424 !g:'a monoid. Monoid g ==> !n. #e ** n = #e
425Proof
426 rpt strip_tac>>
427 Induct_on `n` >>
428 rw[]
429QED
430
431
432(* Theorem: For Abelian Monoid g, (x ** n) * y = y * (x ** n) *)
433(* Proof:
434 Since x ** n IN G by monoid_exp_element
435 True by abelian property: !z y. z IN G /\ y IN G ==> z * y = y * z
436*)
437(* This is trivial for AbelianMonoid, since every element commutes.
438 However, what is needed is just for those elements that commute. *)
439
440(* Theorem: x * y = y * x ==> (x ** n) * y = y * (x ** n) *)
441(* Proof:
442 By induction on n.
443 Base case: x ** 0 * y = y * x ** 0
444 (x ** 0) * y
445 = #e * y by monoid_exp_0
446 = y * #e by monoid_id
447 = y * (x ** 0) by monoid_exp_0
448 Step case: x ** n * y = y * x ** n ==> x ** SUC n * y = y * x ** SUC n
449 x ** (SUC n) * y
450 = (x * x ** n) * y by monoid_exp_SUC
451 = x * ((x ** n) * y) by monoid_assoc
452 = x * (y * (x ** n)) by induction hypothesis
453 = (x * y) * (x ** n) by monoid_assoc
454 = (y * x) * (x ** n) by abelian property
455 = y * (x * (x ** n)) by monoid_assoc
456 = y * x ** (SUC n) by monoid_exp_SUC
457*)
458Theorem monoid_comm_exp:
459 !g:'a monoid. Monoid g ==> !x y. x IN G /\ y IN G ==> (x * y = y * x) ==> !n. (x ** n) * y = y * (x ** n)
460Proof
461 rpt strip_tac >>
462 Induct_on `n` >-
463 rw[] >>
464 metis_tac[monoid_exp_SUC, monoid_assoc, monoid_exp_element]
465QED
466
467(* do not export commutativity check *)
468(* val _ = export_rewrites ["monoid_comm_exp"]; *)
469
470(* Theorem: (x ** n) * x = x * (x ** n) *)
471(* Proof:
472 Since x * x = x * x, this is true by monoid_comm_exp.
473*)
474Theorem monoid_exp_comm:
475 !g:'a monoid. Monoid g ==> !x. x IN G ==> !n. (x ** n) * x = x * (x ** n)
476Proof
477 rw[monoid_comm_exp]
478QED
479
480(* no export of commutativity *)
481(* val _ = export_rewrites ["monoid_exp_comm"]; *)
482
483(* Theorem: x ** (SUC n) = (x ** n) * x *)
484(* Proof: by monoid_exp_SUC and monoid_exp_comm. *)
485Theorem monoid_exp_suc:
486 !g:'a monoid. Monoid g ==> !x:'a. x IN G ==> !n. x ** (SUC n) = (x ** n) * x
487Proof
488 rw[monoid_exp_comm]
489QED
490
491(* no export of commutativity *)
492(* val _ = export_rewrites ["monoid_exp_suc"]; *)
493
494(* Theorem: x * y = y * x ==> (x * y) ** n = (x ** n) * (y ** n) *)
495(* Proof:
496 By induction on n.
497 Base case: (x * y) ** 0 = x ** 0 * y ** 0
498 (x * y) ** 0
499 = #e by monoid_exp_0
500 = #e * #e by monoid_id_id
501 = (x ** 0) * (y ** 0) by monoid_exp_0
502 Step case: (x * y) ** n = (x ** n) * (y ** n) ==> (x * y) ** SUC n = x ** SUC n * y ** SUC n
503 (x * y) ** (SUC n)
504 = (x * y) * ((x * y) ** n) by monoid_exp_SUC
505 = (x * y) * ((x ** n) * (y ** n)) by induction hypothesis
506 = x * (y * ((x ** n) * (y ** n))) by monoid_assoc
507 = x * ((y * (x ** n)) * (y ** n)) by monoid_assoc
508 = x * (((x ** n) * y) * (y ** n)) by monoid_comm_exp
509 = x * ((x ** n) * (y * (y ** n))) by monoid_assoc
510 = (x * (x ** n)) * (y * (y ** n)) by monoid_assoc
511*)
512Theorem monoid_comm_op_exp:
513 !g:'a monoid. Monoid g ==> !x y. x IN G /\ y IN G /\ (x * y = y * x) ==> !n. (x * y) ** n = (x ** n) * (y ** n)
514Proof
515 rpt strip_tac >>
516 Induct_on `n` >-
517 rw[] >>
518 `(x * y) ** SUC n = x * ((y * (x ** n)) * (y ** n))` by rw[monoid_assoc] >>
519 `_ = x * (((x ** n) * y) * (y ** n))` by metis_tac[monoid_comm_exp] >>
520 rw[monoid_assoc]
521QED
522
523(* do not export commutativity check *)
524(* val _ = export_rewrites ["monoid_comm_op_exp"]; *)
525
526(* Theorem: x IN G /\ y IN G /\ x * y = y * x ==> (x ** n) * (y ** m) = (y ** m) * (x ** n) *)
527(* Proof:
528 By inducton on m.
529 Base case: x ** n * y ** 0 = y ** 0 * x ** n
530 LHS = x ** n * y ** 0
531 = x ** n * #e by monoid_exp_0
532 = x ** n by monoid_rid
533 = #e * x ** n by monoid_lid
534 = y ** 0 * x ** n by monoid_exp_0
535 = RHS
536 Step case: x ** n * y ** m = y ** m * x ** n ==> x ** n * y ** SUC m = y ** SUC m * x ** n
537 LHS = x ** n * y ** SUC m
538 = x ** n * (y * y ** m) by monoid_exp_SUC
539 = (x ** n * y) * y ** m by monoid_assoc
540 = (y * x ** n) * y ** m by monoid_comm_exp (with single y)
541 = y * (x ** n * y ** m) by monoid_assoc
542 = y * (y ** m * x ** n) by induction hypothesis
543 = (y * y ** m) * x ** n by monoid_assoc
544 = y ** SUC m * x ** n by monoid_exp_SUC
545 = RHS
546*)
547Theorem monoid_comm_exp_exp:
548 !g:'a monoid. Monoid g ==> !x y. x IN G /\ y IN G /\ (x * y = y * x) ==>
549 !n m. x ** n * y ** m = y ** m * x ** n
550Proof
551 rpt strip_tac >>
552 Induct_on `m` >-
553 rw[] >>
554 `x ** n * y ** SUC m = x ** n * (y * y ** m)` by rw[] >>
555 `_ = (x ** n * y) * y ** m` by rw[monoid_assoc] >>
556 `_ = (y * x ** n) * y ** m` by metis_tac[monoid_comm_exp] >>
557 `_ = y * (x ** n * y ** m)` by rw[monoid_assoc] >>
558 `_ = y * (y ** m * x ** n)` by metis_tac[] >>
559 rw[monoid_assoc]
560QED
561
562(* Theorem: x ** (n + k) = (x ** n) * (x ** k) *)
563(* Proof:
564 By induction on n.
565 Base case: x ** (0 + k) = x ** 0 * x ** k
566 x ** (0 + k)
567 = x ** k by arithmetic
568 = #e * (x ** k) by monoid_lid
569 = (x ** 0) * (x ** k) by monoid_exp_0
570 Step case: x ** (n + k) = x ** n * x ** k ==> x ** (SUC n + k) = x ** SUC n * x ** k
571 x ** (SUC n + k)
572 = x ** (SUC (n + k)) by arithmetic
573 = x * (x ** (n + k)) by monoid_exp_SUC
574 = x * ((x ** n) * (x ** k)) by induction hypothesis
575 = (x * (x ** n)) * (x ** k) by monoid_assoc
576 = (x ** SUC n) * (x ** k) by monoid_exp_def
577*)
578Theorem monoid_exp_add[simp]:
579 !g:'a monoid. Monoid g ==> !x. x IN G ==> !n k. x ** (n + k) = (x ** n) * (x ** k)
580Proof
581 rpt strip_tac >>
582 Induct_on `n` >-
583 rw[] >>
584 rw_tac std_ss[monoid_exp_SUC, monoid_assoc, monoid_exp_element, DECIDE ``SUC n + k = SUC (n+k)``]
585QED
586
587
588(* Theorem: x ** (n * k) = (x ** n) ** k *)
589(* Proof:
590 By induction on n.
591 Base case: x ** (0 * k) = (x ** 0) ** k
592 x ** (0 * k)
593 = x ** 0 by arithmetic
594 = #e by monoid_exp_0
595 = (#e) ** n by monoid_id_exp
596 = (x ** 0) ** n by monoid_exp_0
597 Step case: x ** (n * k) = (x ** n) ** k ==> x ** (SUC n * k) = (x ** SUC n) ** k
598 x ** (SUC n * k)
599 = x ** (n * k + k) by arithmetic
600 = (x ** (n * k)) * (x ** k) by monoid_exp_add
601 = ((x ** n) ** k) * (x ** k) by induction hypothesis
602 = ((x ** n) * x) ** k by monoid_comm_op_exp and monoid_exp_comm
603 = (x * (x ** n)) ** k by monoid_exp_comm
604 = (x ** SUC n) ** k by monoid_exp_def
605*)
606Theorem monoid_exp_mult[simp]:
607 !g:'a monoid. Monoid g ==> !x. x IN G ==> !n k. x ** (n * k) = (x ** n) ** k
608Proof
609 rpt strip_tac >>
610 Induct_on `n` >-
611 rw[] >>
612 `SUC n * k = n * k + k` by metis_tac[MULT] >>
613 `x ** (SUC n * k) = ((x ** n) * x) ** k` by rw_tac std_ss[monoid_comm_op_exp, monoid_exp_comm, monoid_exp_element, monoid_exp_add] >>
614 rw[monoid_exp_comm]
615QED
616
617
618(* Theorem: x IN G ==> (x ** m) ** n = (x ** n) ** m *)
619(* Proof:
620 (x ** m) ** n
621 = x ** (m * n) by monoid_exp_mult
622 = x ** (n * m) by MULT_COMM
623 = (x ** n) ** m by monoid_exp_mult
624*)
625Theorem monoid_exp_mult_comm:
626 !g:'a monoid. Monoid g ==> !x. x IN G ==> !m n. (x ** m) ** n = (x ** n) ** m
627Proof
628 metis_tac[monoid_exp_mult, MULT_COMM]
629QED
630
631
632(* ------------------------------------------------------------------------- *)
633(* Finite Monoid. *)
634(* ------------------------------------------------------------------------- *)
635
636(* Theorem: For FINITE Monoid g and x IN G, x ** k cannot be all distinct. *)
637(* Proof:
638 By contradiction. Assume !k h. x ** k = x ** h ==> k = h, then
639 Since G is FINITE, let c = CARD G.
640 The map (count (SUC c)) -> G such that n -> x ** n is:
641 (1) a map since each x ** n IN G
642 (2) injective since all x ** n are distinct
643 But c < SUC c = CARD (count (SUC c)), and this contradicts the Pigeon-hole Principle.
644*)
645Theorem finite_monoid_exp_not_distinct:
646 !g:'a monoid. FiniteMonoid g ==> !x. x IN G ==> ?h k. (x ** h = x ** k) /\ (h <> k)
647Proof
648 rw[FiniteMonoid_def] >>
649 spose_not_then strip_assume_tac >>
650 qabbrev_tac `c = CARD G` >>
651 `INJ (\n. x ** n) (count (SUC c)) G` by rw[INJ_DEF] >>
652 `c < SUC c` by decide_tac >>
653 metis_tac[CARD_COUNT, PHP]
654QED
655(*
656This theorem implies that, if x ** k are all distinct for a Monoid g,
657then its carrier G must be INFINITE.
658Otherwise, this is not immediately useful for a Monoid, as the op has no inverse.
659However, it is useful for a Group, where the op has inverse,
660hence reduce this to x ** (h-k) = #e, if h > k.
661Also, it is useful for an Integral Domain, where the prod.op still has no inverse,
662but being a Ring, it has subtraction and distribution, giving x ** k * (x ** (h-k) - #1) = #0
663from which the no-zero-divisor property of Integral Domain gives x ** (h-k) = #1.
664*)
665
666(* ------------------------------------------------------------------------- *)
667(* Abelian Monoid ITSET Theorems *)
668(* ------------------------------------------------------------------------- *)
669
670(* Define ITSET for Monoid -- fold of g.op, especially for Abelian Monoid (by lifting) *)
671Overload GITSET = ``\(g:'a monoid) s b. ITSET g.op s b``
672
673(*
674> ITSET_def |> ISPEC ``s:'b -> bool`` |> ISPEC ``(g:'a monoid).op`` |> ISPEC ``b:'a``;
675val it = |- GITSET g s b = if FINITE s then if s = {} then b else GITSET g (REST s) (CHOICE s * b)
676 else ARB: thm
677*)
678
679fun gINST th = th |> SPEC_ALL |> INST_TYPE [beta |-> alpha]
680 |> Q.INST [`f` |-> `g.op`] |> GEN_ALL;
681(* val gINST = fn: thm -> thm *)
682
683Theorem GITSET_THM = gINST ITSET_THM;
684(* > val GITSET_THM =
685 |- !s g b. FINITE s ==> (GITSET g s b = if s = {} then b else GITSET g (REST s) (CHOICE s * b)) : thm
686*)
687
688(* Theorem: GITSET {} b = b *)
689Theorem GITSET_EMPTY = gINST ITSET_EMPTY;
690(* > val GITSET_EMPTY = |- !g b. GITSET g {} b = b : thm *)
691
692(* Theorem: GITSET g (x INSERT s) b = GITSET g (REST (x INSERT s)) ((CHOICE (x INSERT s)) * b) *)
693(* Proof:
694 By GITSET_THM, since x INSERT s is non-empty.
695*)
696Theorem GITSET_INSERT =
697 gINST (ITSET_INSERT |> SPEC_ALL |> UNDISCH) |> DISCH_ALL |> GEN_ALL;
698(* > val GITSET_INSERT =
699 |- !s. FINITE s ==> !x g b. (GITSET g (x INSERT s) b = GITSET g (REST (x INSERT s)) (CHOICE (x INSERT s) * b)) : thm
700*)
701
702(* Theorem: [simplified GITSET_INSERT]
703 FINITE s /\ s <> {} ==> GITSET g s b = GITSET g (REST s) ((CHOICE s) * b) *)
704(* Proof:
705 Replace (x INSERT s) in GITSET_INSERT by s,
706 GITSET g s b = GITSET g (REST s) ((CHOICE s) * b)
707 Since CHOICE s IN s by CHOICE_DEF
708 so (CHOICE s) INSERT s = s by ABSORPTION
709 and the result follows.
710*)
711Theorem GITSET_PROPERTY:
712 !g s. FINITE s /\ s <> {} ==> !b. GITSET g s b = GITSET g (REST s) ((CHOICE s) * b)
713Proof
714 metis_tac[CHOICE_DEF, ABSORPTION, GITSET_INSERT]
715QED
716
717(* Theorem: AbelianMonoid g ==> closure_comm_assoc_fun g.op G *)
718(* Proof:
719 Note Monoid g /\ !x y::(G). x * y = y * x by AbelianMonoid_def
720 and !x y z::(G). x * y * z = y * x * z by monoid_assoc, above gives commutativity
721 Thus closure_comm_assoc_fun g.op G by closure_comm_assoc_fun_def
722*)
723Theorem abelian_monoid_op_closure_comm_assoc_fun:
724 !g:'a monoid. AbelianMonoid g ==> closure_comm_assoc_fun g.op G
725Proof
726 rw[AbelianMonoid_def, closure_comm_assoc_fun_def] >>
727 metis_tac[monoid_assoc]
728QED
729
730(* Theorem: AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
731 !b x::(G). GITSET g (x INSERT s) b = GITSET g (s DELETE x) (x * b) *)
732(* Proof:
733 Note closure_comm_assoc_fun g.op G by abelian_monoid_op_closure_comm_assoc_fun
734 The result follows by SUBSET_COMMUTING_ITSET_INSERT
735*)
736Theorem COMMUTING_GITSET_INSERT:
737 !(g:'a monoid) s. AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
738 !b x::(G). GITSET g (x INSERT s) b = GITSET g (s DELETE x) (x * b)
739Proof
740 metis_tac[abelian_monoid_op_closure_comm_assoc_fun, SUBSET_COMMUTING_ITSET_INSERT]
741QED
742
743(* Theorem: AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
744 !b x::(G). GITSET g s (x * b) = x * (GITSET g s b) *)
745(* Proof:
746 Note closure_comm_assoc_fun g.op G by abelian_monoid_op_closure_comm_assoc_fun
747 The result follows by SUBSET_COMMUTING_ITSET_REDUCTION
748*)
749Theorem COMMUTING_GITSET_REDUCTION:
750 !(g:'a monoid) s. AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
751 !b x::(G). GITSET g s (x * b) = x * (GITSET g s b)
752Proof
753 metis_tac[abelian_monoid_op_closure_comm_assoc_fun, SUBSET_COMMUTING_ITSET_REDUCTION]
754QED
755
756(* Theorem: AbelianMonoid g ==> GITSET g (x INSERT s) b = x * (GITSET g (s DELETE x) b) *)
757(* Proof:
758 Note closure_comm_assoc_fun g.op G by abelian_monoid_op_closure_comm_assoc_fun
759 The result follows by SUBSET_COMMUTING_ITSET_RECURSES
760*)
761Theorem COMMUTING_GITSET_RECURSES:
762 !(g:'a monoid) s. AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
763 !b x::(G). GITSET g (x INSERT s) b = x * (GITSET g (s DELETE x) b)
764Proof
765 metis_tac[abelian_monoid_op_closure_comm_assoc_fun, SUBSET_COMMUTING_ITSET_RECURSES]
766QED
767
768(* ------------------------------------------------------------------------- *)
769(* Abelian Monoid PROD_SET *)
770(* ------------------------------------------------------------------------- *)
771
772(* Define GPROD_SET via GITSET *)
773Definition GPROD_SET_def: GPROD_SET g s = GITSET g s #e
774End
775
776(* Theorem: property of GPROD_SET *)
777(* Proof:
778 This is to prove:
779 (1) GITSET g {} #e = #e
780 True by GITSET_EMPTY, and monoid_id_element.
781 (2) GITSET g (x INSERT s) #e = x * GITSET g (s DELETE x) #e
782 True by COMMUTING_GITSET_RECURSES, and monoid_id_element.
783*)
784Theorem GPROD_SET_THM:
785 !g s. (GPROD_SET g {} = #e) /\
786 (AbelianMonoid g /\ FINITE s /\ s SUBSET G ==>
787 (!x::(G). GPROD_SET g (x INSERT s) = x * GPROD_SET g (s DELETE x)))
788Proof
789 rw[GPROD_SET_def, RES_FORALL_THM, GITSET_EMPTY] >>
790 `Monoid g` by metis_tac[AbelianMonoid_def] >>
791 metis_tac[COMMUTING_GITSET_RECURSES, monoid_id_element]
792QED
793
794(* Theorem: GPROD_SET g {} = #e *)
795(* Proof:
796 GPROD_SET g {}
797 = GITSET g {} #e by GPROD_SET_def
798 = #e by GITSET_EMPTY
799 or directly by GPROD_SET_THM
800*)
801Theorem GPROD_SET_EMPTY:
802 !g s. GPROD_SET g {} = #e
803Proof
804 rw[GPROD_SET_def, GITSET_EMPTY]
805QED
806
807(* Theorem: Monoid g ==> !x. x IN G ==> (GPROD_SET g {x} = x) *)
808(* Proof:
809 GPROD_SET g {x}
810 = GITSET g {x} #e by GPROD_SET_def
811 = x * #e by ITSET_SING
812 = x by monoid_rid
813*)
814Theorem GPROD_SET_SING:
815 !g:'a monoid. Monoid g ==> !x. x IN G ==> (GPROD_SET g {x} = x)
816Proof
817 rw[GPROD_SET_def, ITSET_SING]
818QED
819
820(*
821> ITSET_SING |> SPEC_ALL |> INST_TYPE[beta |-> alpha] |> Q.INST[`f` |-> `g.op`] |> GEN_ALL;
822val it = |- !x g b. GITSET g {x} b = x * b: thm
823> ITSET_SING |> SPEC_ALL |> INST_TYPE[beta |-> alpha] |> Q.INST[`f` |-> `g.op`] |> Q.INST[`b` |-> `#e`] |> REWRITE_RULE[GSYM GPROD_SET_def];
824val it = |- GPROD_SET g {x} = x * #e: thm
825*)
826
827(* Theorem: GPROD_SET g s IN G *)
828(* Proof:
829 By complete induction on CARD s.
830 Case s = {},
831 Then GPROD_SET g {} = #e by GPROD_SET_EMPTY
832 and #e IN G by monoid_id_element
833 Case s <> {},
834 Let x = CHOICE s, t = REST s, s = x INSERT t, x NOTIN t.
835 GPROD_SET g s
836 = GPROD_SET g (x INSERT t) by s = x INSERT t
837 = x * GPROD_SET g (t DELETE x) by GPROD_SET_THM
838 = x * GPROD_SET g t by DELETE_NON_ELEMENT, x NOTIN t
839 Hence GPROD_SET g s IN G by induction, and monoid_op_element.
840*)
841Theorem GPROD_SET_PROPERTY:
842 !(g:'a monoid) s. AbelianMonoid g /\ FINITE s /\ s SUBSET G ==> GPROD_SET g s IN G
843Proof
844 completeInduct_on `CARD s` >>
845 pop_assum (assume_tac o SIMP_RULE bool_ss[GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO]) >>
846 rpt strip_tac >>
847 `Monoid g` by metis_tac[AbelianMonoid_def] >>
848 Cases_on `s = {}` >-
849 rw[GPROD_SET_EMPTY] >>
850 `?x t. (x = CHOICE s) /\ (t = REST s) /\ (s = x INSERT t)` by rw[CHOICE_INSERT_REST] >>
851 `x IN G` by metis_tac[CHOICE_DEF, SUBSET_DEF] >>
852 `t SUBSET G /\ FINITE t` by metis_tac[REST_SUBSET, SUBSET_TRANS, SUBSET_FINITE] >>
853 `x NOTIN t` by metis_tac[CHOICE_NOT_IN_REST] >>
854 `CARD t < CARD s` by rw[] >>
855 metis_tac[GPROD_SET_THM, DELETE_NON_ELEMENT, monoid_op_element]
856QED
857
858(* ----------------------------------------------------------------------
859 monoid extension
860
861 lifting a monoid so that its carrier is the whole of the type but the
862 op is the same on the old carrier set.
863 ---------------------------------------------------------------------- *)
864
865Definition extend_def:
866 extend m = <| carrier := UNIV; id := m.id;
867 op := λx y. if x IN m.carrier then
868 if y IN m.carrier then m.op x y else y
869 else x |>
870End
871
872Theorem extend_is_monoid[simp]:
873 !m. Monoid m ==> Monoid (extend m)
874Proof
875 simp[extend_def, EQ_IMP_THM, Monoid_def] >> rw[] >> rw[] >>
876 gvs[]
877QED
878
879Theorem extend_carrier[simp]:
880 (extend m).carrier = UNIV
881Proof
882 simp[extend_def]
883QED
884
885Theorem extend_id[simp]:
886 (extend m).id = m.id
887Proof
888 simp[extend_def]
889QED
890
891Theorem extend_op:
892 x IN m.carrier /\ y IN m.carrier ==> (extend m).op x y = m.op x y
893Proof
894 simp[extend_def]
895QED
896
897(*
898
899Monoid Order
900============
901This is an investigation of the equation x ** n = #e.
902Given x IN G, x ** 0 = #e by monoid_exp_0
903But for those having non-trivial n with x ** n = #e,
904the least value of n is called the order for the element x.
905This is an important property for the element x,
906especiallly later for Finite Group.
907
908Monoid Invertibles
909==================
910In a monoid M, not all elements are invertible.
911But for those elements that are invertible,
912they have interesting properties.
913Indeed, being invertible, an operation .inv or |/
914can be defined through Skolemization, and later,
915the Monoid Invertibles will be shown to be a Group.
916
917*)
918
919(* ------------------------------------------------------------------------- *)
920(* Monoid Order and Invertibles Documentation *)
921(* ------------------------------------------------------------------------- *)
922(* Overloading:
923 ord x = order g x
924 maximal_order g = MAX_SET (IMAGE ord G)
925 G* = monoid_invertibles g
926 reciprocal x = monoid_inv g x
927 |/ = reciprocal
928*)
929(* Definitions and Theorems (# are exported):
930
931 Definitions:
932 period_def |- !g x k. period g x k <=> 0 < k /\ (x ** k = #e)
933 order_def |- !g x. ord x = case OLEAST k. period g x k of NONE => 0 | SOME k => k
934 order_alt |- !g x. ord x = case OLEAST k. 0 < k /\ x ** k = #e of NONE => 0 | SOME k => k
935 order_property |- !g x. x ** ord x = #e
936 order_period |- !g x. 0 < ord x ==> period g x (ord x)
937 order_minimal |- !g x n. 0 < n /\ n < ord x ==> x ** n <> #e
938 order_eq_0 |- !g x. (ord x = 0) <=> !n. 0 < n ==> x ** n <> #e
939 order_thm |- !g x n. 0 < n ==>
940 ((ord x = n) <=> (x ** n = #e) /\ !m. 0 < m /\ m < n ==> x ** m <> #e)
941
942# monoid_order_id |- !g. Monoid g ==> (ord #e = 1)
943 monoid_order_eq_1 |- !g. Monoid g ==> !x. x IN G ==> ((ord x = 1) <=> (x = #e))
944 monoid_order_condition |- !g. Monoid g ==> !x. x IN G ==> !m. (x ** m = #e) <=> ord x divides m
945 monoid_order_divides_exp|- !g. Monoid g ==> !x n. x IN G ==> ((x ** n = #e) <=> ord x divides n)
946 monoid_order_power_eq_0 |- !g. Monoid g ==> !x. x IN G ==> !k. (ord (x ** k) = 0) <=> 0 < k /\ (ord x = 0)
947 monoid_order_power |- !g. Monoid g ==> !x. x IN G ==> !k. ord (x ** k) * gcd (ord x) k = ord x
948 monoid_order_power_eqn |- !g. Monoid g ==> !x k. x IN G /\ 0 < k ==> (ord (x ** k) = ord x DIV gcd k (ord x))
949 monoid_order_power_coprime |- !g. Monoid g ==> !x. x IN G ==>
950 !n. coprime n (ord x) ==> (ord (x ** n) = ord x)
951 monoid_order_cofactor |- !g. Monoid g ==> !x n. x IN G /\ 0 < ord x /\ n divides (ord x) ==>
952 (ord (x ** (ord x DIV n)) = n)
953 monoid_order_divisor |- !g. Monoid g ==> !x m. x IN G /\ 0 < ord x /\ m divides (ord x) ==>
954 ?y. y IN G /\ (ord y = m)
955 monoid_order_common |- !g. Monoid g ==> !x y. x IN G /\ y IN G /\ (x * y = y * x) ==>
956 ?z. z IN G /\ (ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y))
957 monoid_order_common_coprime |- !g. Monoid g ==> !x y. x IN G /\ y IN G /\ (x * y = y * x) /\
958 coprime (ord x) (ord y) ==> ?z. z IN G /\ (ord z = ord x * ord y)
959 monoid_exp_mod_order |- !g. Monoid g ==> !x. x IN G /\ 0 < ord x ==> !n. x ** n = x ** (n MOD ord x)
960 abelian_monoid_order_common |- !g. AbelianMonoid g ==> !x y. x IN G /\ y IN G ==>
961 ?z. z IN G /\ (ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y))
962 abelian_monoid_order_common_coprime
963 |- !g. AbelianMonoid g ==> !x y. x IN G /\ y IN G /\
964 coprime (ord x) (ord y) ==> ?z. z IN G /\ (ord z = ord x * ord y)
965 abelian_monoid_order_lcm |- !g. AbelianMonoid g ==>
966 !x y. x IN G /\ y IN G ==> ?z. z IN G /\ (ord z = lcm (ord x) (ord y))
967
968 Orders of elements:
969 orders_def |- !g n. orders g n = {x | x IN G /\ (ord x = n)}
970 orders_element |- !g x n. x IN orders g n <=> x IN G /\ (ord x = n)
971 orders_subset |- !g n. orders g n SUBSET G
972 orders_finite |- !g. FINITE G ==> !n. FINITE (orders g n)
973 orders_eq_1 |- !g. Monoid g ==> (orders g 1 = {#e})
974
975 Maximal Order:
976 maximal_order_alt |- !g. maximal_order g = MAX_SET {ord z | z | z IN G}
977 monoid_order_divides_maximal |- !g. FiniteAbelianMonoid g ==>
978 !x. x IN G /\ 0 < ord x ==> ord x divides maximal_order g
979
980 Monoid Invertibles:
981 monoid_invertibles_def |- !g. G* = {x | x IN G /\ ?y. y IN G /\ (x * y = #e) /\ (y * x = #e)}
982 monoid_invertibles_element |- !g x. x IN G* <=> x IN G /\ ?y. y IN G /\ (x * y = #e) /\ (y * x = #e)
983 monoid_order_nonzero |- !g x. Monoid g /\ x IN G /\ 0 < ord x ==> x IN G*
984
985 Invertibles_def |- !g. Invertibles g = <|carrier := G*; op := $*; id := #e|>
986 Invertibles_property |- !g. ((Invertibles g).carrier = G* ) /\
987 ((Invertibles g).op = $* ) /\
988 ((Invertibles g).id = #e) /\
989 ((Invertibles g).exp = $** )
990 Invertibles_carrier |- !g. (Invertibles g).carrier = G*
991 Invertibles_subset |- !g. (Invertibles g).carrier SUBSET G
992 Invertibles_order |- !g x. order (Invertibles g) x = ord x
993
994 Monoid Inverse as an operation:
995 monoid_inv_def |- !g x. Monoid g /\ x IN G* ==> |/ x IN G /\ (x * |/ x = #e) /\ ( |/ x * x = #e)
996 monoid_inv_def_alt |- !g. Monoid g ==> !x. x IN G* <=>
997 x IN G /\ |/ x IN G /\ (x * |/ x = #e) /\ ( |/ x * x = #e)
998 monoid_inv_element |- !g. Monoid g ==> !x. x IN G* ==> x IN G
999# monoid_id_invertible |- !g. Monoid g ==> #e IN G*
1000# monoid_inv_op_invertible |- !g. Monoid g ==> !x y. x IN G* /\ y IN G* ==> x * y IN G*
1001# monoid_inv_invertible |- !g. Monoid g ==> !x. x IN G* ==> |/ x IN G*
1002 monoid_invertibles_is_monoid |- !g. Monoid g ==> Monoid (Invertibles g)
1003
1004*)
1005
1006(* ------------------------------------------------------------------------- *)
1007(* Monoid Order Definition. *)
1008(* ------------------------------------------------------------------------- *)
1009
1010(* Define order = optional LEAST period for an element x in Group g *)
1011Definition period_def[nocompute]:
1012 period (g:'a monoid) (x:'a) k <=> 0 < k /\ (x ** k = #e)
1013End
1014Definition order_def[nocompute]:
1015 order (g:'a monoid) (x:'a) = case OLEAST k. period g x k of
1016 NONE => 0
1017 | SOME k => k
1018End
1019(* use zDefine here since these are not computationally effective. *)
1020
1021(* Expand order_def with period_def. *)
1022Theorem order_alt = REWRITE_RULE [period_def] order_def;
1023(* val order_alt =
1024 |- !g x. order g x =
1025 case OLEAST k. 0 < k /\ x ** k = #e of NONE => 0 | SOME k => k: thm *)
1026
1027(* overloading on Monoid Order *)
1028Overload ord = ``order g``
1029
1030(* Theorem: (x ** (ord x) = #e *)
1031(* Proof: by definition, and x ** 0 = #e by monoid_exp_0. *)
1032Theorem order_property:
1033 !g:'a monoid. !x:'a. (x ** (ord x) = #e)
1034Proof
1035 ntac 2 strip_tac >>
1036 simp_tac std_ss[order_def, period_def] >>
1037 DEEP_INTRO_TAC WhileTheory.OLEAST_INTRO >>
1038 rw[]
1039QED
1040
1041(* Theorem: 0 < (ord x) ==> period g x (ord x) *)
1042(* Proof: by order_property, period_def. *)
1043Theorem order_period:
1044 !g:'a monoid x:'a. 0 < (ord x) ==> period g x (ord x)
1045Proof
1046 rw[order_property, period_def]
1047QED
1048
1049(* Theorem: !n. 0 < n /\ n < (ord x) ==> x ** n <> #e *)
1050(* Proof: by definition of OLEAST. *)
1051Theorem order_minimal:
1052 !g:'a monoid x:'a. !n. 0 < n /\ n < ord x ==> x ** n <> #e
1053Proof
1054 ntac 3 strip_tac >>
1055 simp_tac std_ss[order_def, period_def] >>
1056 DEEP_INTRO_TAC WhileTheory.OLEAST_INTRO >>
1057 rw_tac std_ss[] >>
1058 metis_tac[DECIDE “~(0 < 0)”]
1059QED
1060
1061(* Theorem: (ord x = 0) <=> !n. 0 < n ==> x ** n <> #e *)
1062(* Proof:
1063 Expand by order_def, period_def, this is to show:
1064 (1) 0 < n /\ (!n. ~(0 < n) \/ x ** n <> #e) ==> x ** n <> #e
1065 True by assertion.
1066 (2) 0 < n /\ x ** n = #e /\ (!m. m < 0 ==> ~(0 < m) \/ x ** m <> #e) ==> (n = 0) <=> !n. 0 < n ==> x ** n <> #e
1067 True by assertion.
1068*)
1069Theorem order_eq_0:
1070 !g:'a monoid x. ord x = 0 <=> !n. 0 < n ==> x ** n <> #e
1071Proof
1072 ntac 2 strip_tac >>
1073 simp_tac std_ss[order_def, period_def] >>
1074 DEEP_INTRO_TAC WhileTheory.OLEAST_INTRO >>
1075 rw_tac std_ss[] >>
1076 metis_tac[DECIDE “~(0 < 0)”]
1077QED
1078
1079val std_ss = std_ss -* ["NOT_LT_ZERO_EQ_ZERO"]
1080
1081(* Theorem: 0 < n ==> ((ord x = n) <=> (x ** n = #e) /\ !m. 0 < m /\ m < n ==> x ** m <> #e) *)
1082(* Proof:
1083 If part: (ord x = n) ==> (x ** n = #e) /\ !m. 0 < m /\ m < n ==> x ** m <> #e
1084 This is to show:
1085 (1) (ord x = n) ==> (x ** n = #e), true by order_property
1086 (2) (ord x = n) ==> !m. 0 < m /\ m < n ==> x ** m <> #e, true by order_minimal
1087 Only-if part: (x ** n = #e) /\ !m. 0 < m /\ m < n ==> x ** m <> #e ==> (ord x = n)
1088 Expanding by order_def, period_def, this is to show:
1089 (1) 0 < n /\ x ** n = #e /\ !n'. ~(0 < n') \/ x ** n' <> #e ==> 0 = n
1090 Putting n' = n, the assumption is contradictory.
1091 (2) 0 < n /\ 0 < n' /\ x ** n = #e /\ x ** n' = #e /\ ... ==> n' = n
1092 The assumptions implies ~(n' < n), and ~(n < n'), hence n' = n.
1093*)
1094Theorem order_thm:
1095 !g:'a monoid x:'a. !n. 0 < n ==>
1096 ((ord x = n) <=> (x ** n = #e) /\ !m. 0 < m /\ m < n ==> x ** m <> #e)
1097Proof
1098 rw[EQ_IMP_THM] >-
1099 rw[order_property] >-
1100 rw[order_minimal] >>
1101 simp_tac std_ss[order_def, period_def] >>
1102 DEEP_INTRO_TAC WhileTheory.OLEAST_INTRO >>
1103 rw_tac std_ss[] >-
1104 metis_tac[] >>
1105 `~(n' < n)` by metis_tac[] >>
1106 `~(n < n')` by metis_tac[] >>
1107 decide_tac
1108QED
1109
1110(* Theorem: Monoid g ==> (ord #e = 1) *)
1111(* Proof:
1112 Since #e IN G by monoid_id_element
1113 and #e ** 1 = #e by monoid_exp_1
1114 Obviously, 0 < 1 and there is no m such that 0 < m < 1
1115 hence true by order_thm
1116*)
1117Theorem monoid_order_id[simp]:
1118 !g:'a monoid. Monoid g ==> (ord #e = 1)
1119Proof
1120 rw[order_thm, DECIDE``!m . ~(0 < m /\ m < 1)``]
1121QED
1122
1123
1124(* Theorem: Monoid g ==> !x. x IN G ==> ((ord x = 1) <=> (x = #e)) *)
1125(* Proof:
1126 If part: ord x = 1 ==> x = #e
1127 Since x ** (ord x) = #e by order_property
1128 ==> x ** 1 = #e by given
1129 ==> x = #e by monoid_exp_1
1130 Only-if part: x = #e ==> ord x = 1
1131 i.e. to show ord #e = 1.
1132 True by monoid_order_id.
1133*)
1134Theorem monoid_order_eq_1:
1135 !g:'a monoid. Monoid g ==> !x. x IN G ==> ((ord x = 1) <=> (x = #e))
1136Proof
1137 rw[EQ_IMP_THM] >>
1138 `#e = x ** (ord x)` by rw[order_property] >>
1139 rw[]
1140QED
1141
1142(* Theorem: Monoid g ==> !x. x IN G ==> !m. (x ** m = #e) <=> (ord x) divides m *)
1143(* Proof:
1144 (ord x) is a period, and so divides all periods.
1145 Let n = ord x.
1146 If part: x^m = #e ==> n divides m
1147 If n = 0, m = 0 by order_eq_0
1148 Hence true by ZERO_DIVIDES
1149 If n <> 0,
1150 By division algorithm, m = q * n + t for some q, t and t < n.
1151 #e = x^m
1152 = x^(q * n + t)
1153 = (x^n)^q * x^t
1154 = #e * x^t
1155 Thus x^t = #e, but t < n.
1156 If 0 < t, this contradicts order_minimal.
1157 Hence t = 0, or n divides m.
1158 Only-if part: n divides m ==> x^m = #e
1159 By divides_def, ?k. m = k * n
1160 x^m = x^(k * n) = (x^n)^k = #e^k = #e.
1161*)
1162Theorem monoid_order_condition:
1163 !g:'a monoid. Monoid g ==> !x. x IN G ==> !m. (x ** m = #e) <=> (ord x) divides m
1164Proof
1165 rpt strip_tac >>
1166 qabbrev_tac `n = ord x` >>
1167 rw[EQ_IMP_THM] >| [
1168 Cases_on `n = 0` >| [
1169 `~(0 < m)` by metis_tac[order_eq_0] >>
1170 `m = 0` by decide_tac >>
1171 rw[ZERO_DIVIDES],
1172 `x ** n = #e` by rw[order_property, Abbr`n`] >>
1173 `0 < n` by decide_tac >>
1174 `?q t. (m = q * n + t) /\ t < n` by metis_tac[DIVISION] >>
1175 `x ** m = x ** (n * q + t)` by metis_tac[MULT_COMM] >>
1176 `_ = (x ** (n * q)) * (x ** t)` by rw[] >>
1177 `_ = ((x ** n) ** q) * (x ** t)` by rw[] >>
1178 `_ = x ** t` by rw[] >>
1179 `~(0 < t)` by metis_tac[order_minimal] >>
1180 `t = 0` by decide_tac >>
1181 `m = q * n` by rw[] >>
1182 metis_tac[divides_def]
1183 ],
1184 `x ** n = #e` by rw[order_property, Abbr`n`] >>
1185 `?k. m = k * n` by rw[GSYM divides_def] >>
1186 `x ** m = x ** (n * k)` by metis_tac[MULT_COMM] >>
1187 `_ = (x ** n) ** k` by rw[] >>
1188 rw[]
1189 ]
1190QED
1191
1192(* Theorem: Monoid g ==> !x n. x IN G ==> (x ** n = #e <=> ord x divides n) *)
1193(* Proof: by monoid_order_condition *)
1194Theorem monoid_order_divides_exp:
1195 !g:'a monoid. Monoid g ==> !x n. x IN G ==> ((x ** n = #e) <=> ord x divides n)
1196Proof
1197 rw[monoid_order_condition]
1198QED
1199
1200(* Theorem: Monoid g ==> !x. x IN G ==> !k. (ord (x ** k) = 0) <=> 0 < k /\ (ord x = 0) *)
1201(* Proof:
1202 By order_eq_0, this is to show:
1203 (1) !n. 0 < n ==> (x ** k) ** n <> #e ==> 0 < k
1204 By contradiction. Assume k = 0.
1205 Then x ** k = #e by monoid_exp_0
1206 and #e ** n = #e by monoid_id_exp
1207 This contradicts the implication: (x ** k) ** n <> #e.
1208 (2) 0 < n /\ !n. 0 < n ==> (x ** k) ** n <> #e ==> x ** n <> #e
1209 By contradiction. Assume x ** n = #e.
1210 Now, (x ** k) ** n
1211 = x ** (k * n) by monoid_exp_mult
1212 = x ** (n * k) by MULT_COMM
1213 = (x ** n) * k by monoid_exp_mult
1214 = #e ** k by x ** n = #e
1215 = #e by monoid_id_exp
1216 This contradicts the implication: (x ** k) ** n <> #e.
1217 (3) 0 < n /\ !n. 0 < n ==> x ** n <> #e ==> (x ** k) ** n <> #e
1218 By contradiction. Assume (x ** k) ** n = #e.
1219 0 < k /\ 0 < n ==> 0 < k * n by arithmetic
1220 But (x ** n) ** k = x ** (n * k) by monoid_exp_mult
1221 This contradicts the implication: (x ** k) ** n <> #e.
1222*)
1223Theorem monoid_order_power_eq_0:
1224 !g:'a monoid. Monoid g ==> !x. x IN G ==> !k. (ord (x ** k) = 0) <=> 0 < k /\ (ord x = 0)
1225Proof
1226 rw[order_eq_0, EQ_IMP_THM] >| [
1227 spose_not_then strip_assume_tac >>
1228 `k = 0` by decide_tac >>
1229 `x ** k = #e` by rw[monoid_exp_0] >>
1230 metis_tac[monoid_id_exp, DECIDE``0 < 1``],
1231 metis_tac[monoid_exp_mult, MULT_COMM, monoid_id_exp],
1232 `0 < k * n` by rw[LESS_MULT2] >>
1233 metis_tac[monoid_exp_mult]
1234 ]
1235QED
1236
1237(* Theorem: ord (x ** k) = ord x / gcd(ord x, k)
1238 Monoid g ==> !x. x IN G ==> !k. (ord (x ** k) * (gcd (ord x) k) = ord x) *)
1239(* Proof:
1240 Let n = ord x, m = ord (x^k), d = gcd(n,k).
1241 This is to show: m = n / d.
1242 If k = 0,
1243 m = ord (x^0) = ord #e = 1 by monoid_order_id
1244 d = gcd(n,0) = n by GCD_0R
1245 henc true.
1246 If k <> 0,
1247 First, show ord (x^k) = m divides n/d.
1248 If n = 0, m = 0 by monoid_order_power_eq_0
1249 so ord (x^k) = m | (n/d) by ZERO_DIVIDES
1250 If n <> 0,
1251 (x^k)^(n/d) = x^(k * n/d) = x^(n * k/d) = (x^n)^(k/d) = #e,
1252 so ord (x^k) = m | (n/d) by monoid_order_condition.
1253 Second, show (n/d) divides m = ord (x^k), or equivalently: n divides d * m
1254 x^(k * m) = (x^k)^m = #e = x^n,
1255 so ord x = n | k * m by monoid_order_condition
1256 Since d = gcd(k,n), there are integers a and b such that
1257 ka + nb = d by LINEAR_GCD
1258 Multiply by m: k * m * a + n * m * b = d * m.
1259 But since n | k * m, it follows that n | d*m,
1260 i.e. (n/d) | m by DIVIDES_CANCEL.
1261 By DIVIDES_ANTISYM, ord (x^k) = m = n/d.
1262*)
1263Theorem monoid_order_power:
1264 !g:'a monoid. Monoid g ==> !x. x IN G ==> !k. (ord (x ** k) * (gcd (ord x) k) = ord x)
1265Proof
1266 rpt strip_tac >>
1267 qabbrev_tac `n = ord x` >>
1268 qabbrev_tac `m = ord (x ** k)` >>
1269 qabbrev_tac `d = gcd n k` >>
1270 Cases_on `k = 0` >| [
1271 `d = n` by metis_tac[GCD_0R] >>
1272 rw[Abbr`m`],
1273 Cases_on `n = 0` >| [
1274 `0 < k` by decide_tac >>
1275 `m = 0` by rw[monoid_order_power_eq_0, Abbr`n`, Abbr`m`] >>
1276 rw[],
1277 `x ** n = #e` by rw[order_property, Abbr`n`] >>
1278 `0 < n /\ 0 < k` by decide_tac >>
1279 `?p q. (n = p * d) /\ (k = q * d)` by metis_tac[FACTOR_OUT_GCD] >>
1280 `k * p = n * q` by rw_tac arith_ss[] >>
1281 `(x ** k) ** p = x ** (k * p)` by rw[] >>
1282 `_ = x ** (n * q)` by metis_tac[] >>
1283 `_ = (x ** n) ** q` by rw[] >>
1284 `_ = #e` by rw[] >>
1285 `m divides p` by rw[GSYM monoid_order_condition, Abbr`m`] >>
1286 `x ** (m * k) = x ** (k * m)` by metis_tac[MULT_COMM] >>
1287 `_ = (x ** k) ** m` by rw[] >>
1288 `_ = #e` by rw[order_property, Abbr`m`] >>
1289 `n divides (m * k)` by rw[GSYM monoid_order_condition, Abbr`n`, Abbr`m`] >>
1290 `?u v. u * k = v * n + d` by rw[LINEAR_GCD, Abbr`d`] >>
1291 `m * k * u = m * (u * k)` by rw_tac arith_ss[] >>
1292 `_ = m * (v * n) + m * d` by metis_tac[LEFT_ADD_DISTRIB] >>
1293 `_ = m * v * n + m * d` by rw_tac arith_ss[] >>
1294 `n divides (m * k * u)` by metis_tac[DIVIDES_MULT] >>
1295 `n divides (m * v * n)` by metis_tac[divides_def] >>
1296 `n divides (m * d)` by metis_tac[DIVIDES_ADD_2] >>
1297 `d <> 0` by metis_tac[MULT_EQ_0] >>
1298 `0 < d` by decide_tac >>
1299 `p divides m` by metis_tac[DIVIDES_CANCEL] >>
1300 metis_tac[DIVIDES_ANTISYM]
1301 ]
1302 ]
1303QED
1304
1305(* Theorem: Monoid g ==>
1306 !x k. x IN G /\ 0 < k ==> (ord (x ** k) = (ord x) DIV (gcd k (ord x))) *)
1307(* Proof:
1308 Note ord (x ** k) * gcd k (ord x) = ord x by monoid_order_power, GCD_SYM
1309 and 0 < gcd k (ord x) by GCD_EQ_0, 0 < k
1310 ==> ord (x ** k) = (ord x) DIV (gcd k (ord x)) by MULT_EQ_DIV
1311*)
1312Theorem monoid_order_power_eqn:
1313 !g:'a monoid. Monoid g ==>
1314 !x k. x IN G /\ 0 < k ==> (ord (x ** k) = (ord x) DIV (gcd k (ord x)))
1315Proof
1316 rpt strip_tac >>
1317 `ord (x ** k) * gcd k (ord x) = ord x` by metis_tac[monoid_order_power, GCD_SYM] >>
1318 `0 < gcd k (ord x)` by metis_tac[GCD_EQ_0, NOT_ZERO] >>
1319 fs[MULT_EQ_DIV]
1320QED
1321
1322(* Theorem: Monoid g ==> !x. x IN G ==> !n. coprime n (ord x) ==> (ord (x ** n) = ord x) *)
1323(* Proof:
1324 ord x
1325 = ord (x ** n) * gcd (ord x) n by monoid_order_power
1326 = ord (x ** n) * 1 by coprime_sym
1327 = ord (x ** n) by MULT_RIGHT_1
1328*)
1329Theorem monoid_order_power_coprime:
1330 !g:'a monoid. Monoid g ==> !x. x IN G ==> !n. coprime n (ord x) ==> (ord (x ** n) = ord x)
1331Proof
1332 metis_tac[monoid_order_power, coprime_sym, MULT_RIGHT_1]
1333QED
1334
1335(* Theorem: Monoid g ==>
1336 !x n. x IN G /\ 0 < ord x /\ n divides ord x ==> (ord (x ** (ord x DIV n)) = n) *)
1337(* Proof:
1338 Let m = ord x, k = m DIV n.
1339 Since 0 < m, n <> 0, or 0 < n by ZERO_DIVIDES
1340 Since n divides m, m = k * n by DIVIDES_EQN
1341 Hence k divides m by divisors_def, MULT_COMM
1342 and k <> 0 by MULT, m <> 0
1343 and gcd k m = k by divides_iff_gcd_fix
1344 Now ord (x ** k) * k
1345 = m by monoid_order_power
1346 = k * n by above
1347 = n * k by MULT_COMM
1348 Hence ord (x ** k) = n by MULT_RIGHT_CANCEL, k <> 0
1349*)
1350Theorem monoid_order_cofactor:
1351 !g: 'a monoid. Monoid g ==>
1352 !x n. x IN G /\ 0 < ord x /\ n divides ord x ==> (ord (x ** (ord x DIV n)) = n)
1353Proof
1354 rpt strip_tac >>
1355 qabbrev_tac `m = ord x` >>
1356 qabbrev_tac `k = m DIV n` >>
1357 `0 < n` by metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >>
1358 `m = k * n` by rw[GSYM DIVIDES_EQN, Abbr`k`] >>
1359 `k divides m` by metis_tac[divides_def, MULT_COMM] >>
1360 `k <> 0` by metis_tac[MULT, NOT_ZERO_LT_ZERO] >>
1361 `gcd k m = k` by rw[GSYM divides_iff_gcd_fix] >>
1362 metis_tac[monoid_order_power, GCD_SYM, MULT_COMM, MULT_RIGHT_CANCEL]
1363QED
1364
1365(* Theorem: If x IN G with ord x = n > 0, and m divides n, then G contains an element of order m. *)
1366(* Proof:
1367 m divides n ==> n = k * m for some k, by divides_def.
1368 Then x^k has order m:
1369 (x^k)^m = x^(k * m) = x^n = #e
1370 and for any h < m,
1371 if (x^k)^h = x^(k * h) = #e means x has order k * h < k * m = n,
1372 which is a contradiction with order_minimal.
1373*)
1374Theorem monoid_order_divisor:
1375 !g:'a monoid. Monoid g ==>
1376 !x m. x IN G /\ 0 < ord x /\ m divides (ord x) ==> ?y. y IN G /\ (ord y = m)
1377Proof
1378 rpt strip_tac >>
1379 `ord x <> 0` by decide_tac >>
1380 `m <> 0` by metis_tac[ZERO_DIVIDES] >>
1381 `0 < m` by decide_tac >>
1382 `?k. ord x = k * m` by rw[GSYM divides_def] >>
1383 qexists_tac `x ** k` >>
1384 rw[] >>
1385 `x ** (ord x) = #e` by rw[order_property] >>
1386 `(x ** k) ** m = #e` by metis_tac[monoid_exp_mult] >>
1387 `(!h. 0 < h /\ h < m ==> (x ** k) ** h <> #e)` suffices_by metis_tac[order_thm] >>
1388 rpt strip_tac >>
1389 `h <> 0` by decide_tac >>
1390 `k <> 0 /\ k * h <> 0` by metis_tac[MULT, MULT_EQ_0] >>
1391 `0 < k /\ 0 < k * h` by decide_tac >>
1392 `k * h < k * m` by metis_tac[LT_MULT_LCANCEL] >>
1393 `(x ** k) ** h = x ** (k * h)` by rw[] >>
1394 metis_tac[order_minimal]
1395QED
1396
1397(* Theorem: If x * y = y * x, and n = ord x, m = ord y,
1398 then there exists z IN G such that ord z = (lcm n m) / (gcd n m) *)
1399(* Proof:
1400 Let n = ord x, m = ord y, d = gcd(n, m).
1401 This is to show: ?z. z IN G /\ (ord z * d = n * m)
1402 If n = 0, take z = x, by LCM_0.
1403 If m = 0, take z = y, by LCM_0.
1404 If n <> 0 and m <> 0,
1405 First, get a pair with coprime orders.
1406 ?p q. (n = p * d) /\ (m = q * d) /\ coprime p q by FACTOR_OUT_GCD
1407 Let u = x^d, v = y^d
1408 then ord u = ord (x^d) = ord x / gcd(n, d) = n/d = p by monoid_order_power
1409 and ord v = ord (y^d) = ord y / gcd(m, d) = m/d = q by monoid_order_power
1410 Now gcd(p,q) = 1, and there exists integers a and b such that
1411 a * p + b * q = 1 by LINEAR_GCD
1412 Let w = u^b * v^a
1413 Then w^p = (u^b * v^a)^p
1414 = (u^b)^p * (v^a)^p by monoid_comm_op_exp
1415 = (u^p)^b * (v^a)^p by monoid_exp_mult_comm
1416 = #e^b * v^(a * p) by p = ord u
1417 = v^(a * p) by monoid_id_exp
1418 = v^(1 - b * q) by LINEAR_GCD condition
1419 = v^1 * |/ v^(b * q) by variant of monoid_exp_add
1420 = v * 1/ (v^q)^b by monoid_exp_mult_comm
1421 = v * 1/ #e^b by q = ord v
1422 = v
1423 Hence ord (w^p) = ord v = q,
1424 Let c = ord w, c <> 0 since p * q <> 0 by GCD_0L
1425 then q = ord (w^p) = c / gcd(c,p) by monoid_order_power
1426 i.e. q * gcd(c,p) = c, or q divides c
1427 Similarly, w^q = u, and p * gcd(c,q) = c, or p divides c.
1428 Since coprime p q, p * q divides c, an order of element w IN G.
1429 Hence there is some z in G such that ord z = p * q by monoid_order_divisor.
1430 i.e. ord z = lcm p q = lcm (n/d) (m/d) = (lcm n m) / d.
1431*)
1432Theorem monoid_order_common:
1433 !g:'a monoid. Monoid g ==> !x y. x IN G /\ y IN G /\ (x * y = y * x) ==>
1434 ?z. z IN G /\ ((ord z) * gcd (ord x) (ord y) = lcm (ord x) (ord y))
1435Proof
1436 rpt strip_tac >>
1437 qabbrev_tac `n = ord x` >>
1438 qabbrev_tac `m = ord y` >>
1439 qabbrev_tac `d = gcd n m` >>
1440 Cases_on `n = 0` >-
1441 metis_tac[LCM_0, MULT_EQ_0] >>
1442 Cases_on `m = 0` >-
1443 metis_tac[LCM_0, MULT_EQ_0] >>
1444 `x ** n = #e` by rw[order_property, Abbr`n`] >>
1445 `y ** m = #e` by rw[order_property, Abbr`m`] >>
1446 `d <> 0` by rw[GCD_EQ_0, Abbr`d`] >>
1447 `?p q. (n = p * d) /\ (m = q * d) /\ coprime p q` by rw[FACTOR_OUT_GCD, Abbr`d`] >>
1448 qabbrev_tac `u = x ** d` >>
1449 qabbrev_tac `v = y ** d` >>
1450 `u IN G /\ v IN G` by rw[Abbr`u`, Abbr`v`] >>
1451 `(gcd n d = d) /\ (gcd m d = d)` by rw[GCD_GCD, GCD_SYM, Abbr`d`] >>
1452 `ord u = p` by metis_tac[monoid_order_power, MULT_RIGHT_CANCEL] >>
1453 `ord v = q` by metis_tac[monoid_order_power, MULT_RIGHT_CANCEL] >>
1454 `p <> 0 /\ q <> 0` by metis_tac[MULT_EQ_0] >>
1455 `?a b. a * q = b * p + 1` by metis_tac[LINEAR_GCD] >>
1456 `?h k. h * p = k * q + 1` by metis_tac[LINEAR_GCD, GCD_SYM] >>
1457 qabbrev_tac `ua = u ** a` >>
1458 qabbrev_tac `vh = v ** h` >>
1459 qabbrev_tac `w = ua * vh` >>
1460 `ua IN G /\ vh IN G /\ w IN G` by rw[Abbr`ua`, Abbr`vh`, Abbr`w`] >>
1461 `ua * vh = (x ** d) ** a * (y ** d) ** h` by rw[] >>
1462 `_ = x ** (d * a) * y ** (d * h)` by rw_tac std_ss[GSYM monoid_exp_mult] >>
1463 `_ = y ** (d * h) * x ** (d * a)` by metis_tac[monoid_comm_exp_exp] >>
1464 `_ = vh * ua` by rw[] >>
1465 `w ** p = (ua * vh) ** p` by rw[] >>
1466 `_ = ua ** p * vh ** p` by metis_tac[monoid_comm_op_exp] >>
1467 `_ = (u ** p) ** a * (v ** h) ** p` by rw[monoid_exp_mult_comm] >>
1468 `_ = #e ** a * v ** (h * p)` by rw[order_property] >>
1469 `_ = v ** (h * p)` by rw[] >>
1470 `_ = v ** (k * q + 1)` by rw_tac std_ss[] >>
1471 `_ = v ** (k * q) * v` by rw[] >>
1472 `_ = v ** (q * k) * v` by rw_tac std_ss[MULT_COMM] >>
1473 `_ = (v ** q) ** k * v` by rw[] >>
1474 `_ = #e ** k * v` by rw[order_property] >>
1475 `_ = v` by rw[] >>
1476 `w ** q = (ua * vh) ** q` by rw[] >>
1477 `_ = ua ** q * vh ** q` by metis_tac[monoid_comm_op_exp] >>
1478 `_ = (u ** a) ** q * (v ** q) ** h` by rw[monoid_exp_mult_comm] >>
1479 `_ = u ** (a * q) * #e ** h` by rw[order_property] >>
1480 `_ = u ** (a * q)` by rw[] >>
1481 `_ = u ** (b * p + 1)` by rw_tac std_ss[] >>
1482 `_ = u ** (b * p) * u` by rw[] >>
1483 `_ = u ** (p * b) * u` by rw_tac std_ss[MULT_COMM] >>
1484 `_ = (u ** p) ** b * u` by rw[] >>
1485 `_ = #e ** b * u` by rw[order_property] >>
1486 `_ = u` by rw[] >>
1487 qabbrev_tac `c = ord w` >>
1488 `q * gcd c p = c` by rw[monoid_order_power, Abbr`c`] >>
1489 `p * gcd c q = c` by metis_tac[monoid_order_power] >>
1490 `p divides c /\ q divides c` by metis_tac[divides_def, MULT_COMM] >>
1491 `lcm p q = p * q` by rw[LCM_COPRIME] >>
1492 `(p * q) divides c` by metis_tac[LCM_IS_LEAST_COMMON_MULTIPLE] >>
1493 `p * q <> 0` by rw[MULT_EQ_0] >>
1494 `c <> 0` by metis_tac[GCD_0L] >>
1495 `0 < c` by decide_tac >>
1496 `?z. z IN G /\ (ord z = p * q)` by metis_tac[monoid_order_divisor] >>
1497 `ord z * d = d * (p * q)` by rw_tac arith_ss[] >>
1498 `_ = lcm (d * p) (d * q)` by rw[LCM_COMMON_FACTOR] >>
1499 `_ = lcm n m` by metis_tac[MULT_COMM] >>
1500 metis_tac[]
1501QED
1502
1503(* This is a milestone. *)
1504
1505(* Theorem: If x * y = y * x, and n = ord x, m = ord y, and gcd n m = 1,
1506 then there exists z IN G with ord z = (lcm n m) *)
1507(* Proof:
1508 By monoid_order_common and gcd n m = 1.
1509*)
1510Theorem monoid_order_common_coprime:
1511 !g:'a monoid. Monoid g ==> !x y. x IN G /\ y IN G /\ (x * y = y * x) /\ coprime (ord x) (ord y) ==>
1512 ?z. z IN G /\ (ord z = (ord x) * (ord y))
1513Proof
1514 metis_tac[monoid_order_common, GCD_LCM, MULT_RIGHT_1, MULT_LEFT_1]
1515QED
1516(* This version can be proved directly using previous technique, then derive the general case:
1517 Let ord x = n, ord y = m.
1518 Let d = gcd(n,m) p = n/d, q = m/d, gcd(p,q) = 1.
1519 By p | n = ord x, there is u with ord u = p by monoid_order_divisor
1520 By q | m = ord y, there is v with ord v = q by monoid_order_divisor
1521 By gcd(ord u, ord v) = gcd(p,q) = 1,
1522 there is z with ord z = lcm(p,q) = p * q = n/d * m/d = lcm(n,m)/gcd(n,m).
1523*)
1524
1525(* Theorem: Monoid g ==> !x. x IN G /\ 0 < ord x ==> !n. x ** n = x ** (n MOD (ord x)) *)
1526(* Proof:
1527 Let z = ord x, 0 < z by given
1528 Note n = (n DIV z) * z + (n MOD z) by DIVISION, 0 < z.
1529 x ** n
1530 = x ** ((n DIV z) * z + (n MOD z)) by above
1531 = x ** ((n DIV z) * z) * x ** (n MOD z) by monoid_exp_add
1532 = x ** (z * (n DIV z)) * x ** (n MOD z) by MULT_COMM
1533 = (x ** z) ** (n DIV z) * x ** (n MOD z) by monoid_exp_mult
1534 = #e ** (n DIV 2) * x ** (n MOD z) by order_property
1535 = #e * x ** (n MOD z) by monoid_id_exp
1536 = x ** (n MOD z) by monoid_lid
1537*)
1538Theorem monoid_exp_mod_order:
1539 !g:'a monoid. Monoid g ==> !x. x IN G /\ 0 < ord x ==> !n. x ** n = x ** (n MOD (ord x))
1540Proof
1541 rpt strip_tac >>
1542 qabbrev_tac `z = ord x` >>
1543 `x ** n = x ** ((n DIV z) * z + (n MOD z))` by metis_tac[DIVISION] >>
1544 `_ = x ** ((n DIV z) * z) * x ** (n MOD z)` by rw[monoid_exp_add] >>
1545 `_ = x ** (z * (n DIV z)) * x ** (n MOD z)` by metis_tac[MULT_COMM] >>
1546 rw[monoid_exp_mult, order_property, Abbr`z`]
1547QED
1548
1549(* Theorem: AbelianMonoid g ==> !x y. x IN G /\ y IN G ==>
1550 ?z. z IN G /\ (ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y)) *)
1551(* Proof: by AbelianMonoid_def, monoid_order_common *)
1552Theorem abelian_monoid_order_common:
1553 !g:'a monoid. AbelianMonoid g ==> !x y. x IN G /\ y IN G ==>
1554 ?z. z IN G /\ (ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y))
1555Proof
1556 rw[AbelianMonoid_def, monoid_order_common]
1557QED
1558
1559(* Theorem: AbelianMonoid g ==> !x y. x IN G /\ y IN G /\ coprime (ord x) (ord y) ==>
1560 ?z. z IN G /\ (ord z = ord x * ord y) *)
1561(* Proof: by AbelianMonoid_def, monoid_order_common_coprime *)
1562Theorem abelian_monoid_order_common_coprime:
1563 !g:'a monoid. AbelianMonoid g ==> !x y. x IN G /\ y IN G /\ coprime (ord x) (ord y) ==>
1564 ?z. z IN G /\ (ord z = ord x * ord y)
1565Proof
1566 rw[AbelianMonoid_def, monoid_order_common_coprime]
1567QED
1568
1569(* Theorem: AbelianMonoid g ==>
1570 !x y. x IN G /\ y IN G ==> ?z. z IN G /\ (ord z = lcm (ord x) (ord y)) *)
1571(* Proof:
1572 If ord x = 0,
1573 Then lcm 0 (ord y) = 0 = ord x by LCM_0
1574 Thus take z = x.
1575 If ord y = 0
1576 lcm (ord x) 0 = 0 = ord y by LCM_0
1577 Thus take z = y.
1578 Otherwise, 0 < ord x /\ 0 < ord y.
1579 Let m = ord x, n = ord y.
1580 Note ?a b p q. (lcm m n = p * q) /\ coprime p q /\
1581 (m = a * p) /\ (n = b * q) by lcm_gcd_park_decompose
1582 Thus p divides m /\ q divides n by divides_def
1583 ==> ?u. u IN G /\ (ord u = p) by monoid_order_divisor, p divides m
1584 and ?v. v IN G /\ (ord v = q) by monoid_order_divisor, q divides n
1585 ==> ?z. z IN G /\ (ord z = p * q) by monoid_order_common_coprime, coprime p q
1586 or z IN G /\ (ord z = lcm m n) by above
1587*)
1588Theorem abelian_monoid_order_lcm:
1589 !g:'a monoid. AbelianMonoid g ==>
1590 !x y. x IN G /\ y IN G ==> ?z. z IN G /\ (ord z = lcm (ord x) (ord y))
1591Proof
1592 rw[AbelianMonoid_def] >>
1593 qabbrev_tac `m = ord x` >>
1594 qabbrev_tac `n = ord y` >>
1595 Cases_on `(m = 0) \/ (n = 0)` >-
1596 metis_tac[LCM_0] >>
1597 `0 < m /\ 0 < n` by decide_tac >>
1598 `?a b p q. (lcm m n = p * q) /\ coprime p q /\ (m = a * p) /\ (n = b * q)` by metis_tac[lcm_gcd_park_decompose] >>
1599 `p divides m /\ q divides n` by metis_tac[divides_def] >>
1600 `?u. u IN G /\ (ord u = p)` by metis_tac[monoid_order_divisor] >>
1601 `?v. v IN G /\ (ord v = q)` by metis_tac[monoid_order_divisor] >>
1602 `?z. z IN G /\ (ord z = p * q)` by rw[monoid_order_common_coprime] >>
1603 metis_tac[]
1604QED
1605
1606(* This is much better than:
1607abelian_monoid_order_common
1608|- !g. AbelianMonoid g ==> !x y. x IN G /\ y IN G ==>
1609 ?z. z IN G /\ (ord z * gcd (ord x) (ord y) = lcm (ord x) (ord y))
1610*)
1611
1612(* ------------------------------------------------------------------------- *)
1613(* Orders of elements *)
1614(* ------------------------------------------------------------------------- *)
1615
1616(* Define the set of elements with a given order *)
1617Definition orders_def:
1618 orders (g:'a monoid) n = {x | x IN G /\ (ord x = n)}
1619End
1620
1621(* Theorem: !x n. x IN orders g n <=> x IN G /\ (ord x = n) *)
1622(* Proof: by orders_def *)
1623Theorem orders_element:
1624 !g:'a monoid. !x n. x IN orders g n <=> x IN G /\ (ord x = n)
1625Proof
1626 rw[orders_def]
1627QED
1628
1629(* Theorem: !n. (orders g n) SUBSET G *)
1630(* Proof: by orders_def, SUBSET_DEF *)
1631Theorem orders_subset:
1632 !g:'a monoid. !n. (orders g n) SUBSET G
1633Proof
1634 rw[orders_def, SUBSET_DEF]
1635QED
1636
1637(* Theorem: FINITE G ==> !n. FINITE (orders g n) *)
1638(* Proof: by orders_subset, SUBSET_FINITE *)
1639Theorem orders_finite:
1640 !g:'a monoid. FINITE G ==> !n. FINITE (orders g n)
1641Proof
1642 metis_tac[orders_subset, SUBSET_FINITE]
1643QED
1644
1645(* Theorem: Monoid g ==> (orders g 1 = {#e}) *)
1646(* Proof:
1647 orders g 1
1648 = {x | x IN G /\ (ord x = 1)} by orders_def
1649 = {x | x IN G /\ (x = #e)} by monoid_order_eq_1
1650 = {#e} by monoid_id_elelment
1651*)
1652Theorem orders_eq_1:
1653 !g:'a monoid. Monoid g ==> (orders g 1 = {#e})
1654Proof
1655 rw[orders_def, EXTENSION, EQ_IMP_THM, GSYM monoid_order_eq_1]
1656QED
1657
1658(* ------------------------------------------------------------------------- *)
1659(* Maximal Order *)
1660(* ------------------------------------------------------------------------- *)
1661
1662(* Overload maximal_order of a group *)
1663Overload maximal_order = ``\g:'a monoid. MAX_SET (IMAGE ord G)``
1664
1665(* Theorem: maximal_order g = MAX_SET {ord z | z | z IN G} *)
1666(* Proof: by IN_IMAGE *)
1667Theorem maximal_order_alt:
1668 !g:'a monoid. maximal_order g = MAX_SET {ord z | z | z IN G}
1669Proof
1670 rpt strip_tac >>
1671 `IMAGE ord G = {ord z | z | z IN G}` by rw[EXTENSION] >>
1672 rw[]
1673QED
1674
1675(* Theorem: In an Abelian Monoid, every nonzero order divides the maximal order.
1676 FiniteAbelianMonoid g ==> !x. x IN G /\ 0 < ord x ==> (ord x) divides (maximal_order g) *)
1677(* Proof:
1678 Let m = maximal_order g = MAX_SET {ord x | x IN G}
1679 Choose z IN G so that ord z = m.
1680 Pick x IN G so that ord x = n. Question: will n divide m ?
1681
1682 We have: ord x = n, ord z = m bigger.
1683 Let d = gcd(n,m), a = n/d, b = m/d.
1684 Since a | n = ord x, there is ord xa = a
1685 Since b | m = ord y, there is ord xb = b
1686 and gcd(a,b) = 1 by FACTOR_OUT_GCD
1687
1688 If gcd(a,m) <> 1, let prime p divides gcd(a,m) by PRIME_FACTOR
1689
1690 Since gcd(a,m) | a and gcd(a,m) divides m,
1691 prime p | a, p | m = b * d, a product.
1692 When prime p divides (b * d), p | b or p | d by P_EUCLIDES
1693 But gcd(a,b)=1, they don't share any common factor, so p | a ==> p not divide b.
1694 If p not divide b, so p | d.
1695 But d | n, d | m, so p | n and p | m.
1696
1697 Let p^i | n for some max i, mi = MAX_SET {i | p^i divides n}, p^mi | n ==> n = nq * p^mi
1698 and p^j | m for some max j, mj = MAX_SET {j | p^j divides m), p^mj | m ==> m = mq * p^mj
1699 If i <= j,
1700 ppppp | n ppppppp | m
1701 d should picks up all i of the p's, leaving a = n/d with no p, p cannot divide a.
1702 But p | a, so i > j, but this will derive a contradiction:
1703 pppppp | n pppp | m
1704 d picks up j of the p's
1705 Let u = p^i (all prime p in n), v = m/p^j (no prime p)
1706 u | n, so there is ord x = u = p^i u = p^mi
1707 v | m, so there is ord x = v = m/p^j v = m/p^mj
1708 gcd(u,v)=1, since u is pure prime p, v has no prime p (possible gcd = 1, p, p^2, etc.)
1709 So there is ord z = u * v = p^i * m /p^j = m * p^(i-j) .... > m, a contradiction!
1710
1711 This case is impossible for the max order suitation.
1712
1713 So gcd(a,m) = 1, there is ord z = a * m = n * m /d
1714 But n * m /d <= m, since m is maximal
1715 i.e. n <= d
1716 But d | n, d <= n,
1717 Hence n = d = gcd(m,n), apply divides_iff_gcd_fix: n divides m.
1718*)
1719Theorem monoid_order_divides_maximal:
1720 !g:'a monoid. FiniteAbelianMonoid g ==>
1721 !x. x IN G /\ 0 < ord x ==> (ord x) divides (maximal_order g)
1722Proof
1723 rw[FiniteAbelianMonoid_def, AbelianMonoid_def] >>
1724 qabbrev_tac `s = IMAGE ord G` >>
1725 qabbrev_tac `m = MAX_SET s` >>
1726 qabbrev_tac `n = ord x` >>
1727 `#e IN G /\ (ord #e = 1)` by rw[] >>
1728 `s <> {}` by metis_tac[IN_IMAGE, MEMBER_NOT_EMPTY] >>
1729 `FINITE s` by metis_tac[IMAGE_FINITE] >>
1730 `m IN s /\ !y. y IN s ==> y <= m` by rw[MAX_SET_DEF, Abbr`m`] >>
1731 `?z. z IN G /\ (ord z = m)` by metis_tac[IN_IMAGE] >>
1732 `!z. 0 < z <=> z <> 0` by decide_tac >>
1733 `1 <= m` by metis_tac[in_max_set, IN_IMAGE] >>
1734 `0 < m` by decide_tac >>
1735 `?a b. (n = a * gcd n m) /\ (m = b * gcd n m) /\ coprime a b` by metis_tac[FACTOR_OUT_GCD] >>
1736 qabbrev_tac `d = gcd n m` >>
1737 `a divides n /\ b divides m` by metis_tac[divides_def, MULT_COMM] >>
1738 `?xa. xa IN G /\ (ord xa = a)` by metis_tac[monoid_order_divisor] >>
1739 `?xb. xb IN G /\ (ord xb = b)` by metis_tac[monoid_order_divisor] >>
1740 Cases_on `coprime a m` >| [
1741 `?xc. xc IN G /\ (ord xc = a * m)` by metis_tac[monoid_order_common_coprime] >>
1742 `a * m <= m` by metis_tac[IN_IMAGE] >>
1743 `n * m = d * (a * m)` by rw_tac arith_ss[] >>
1744 `n <= d` by metis_tac[LE_MULT_LCANCEL, LE_MULT_RCANCEL] >>
1745 `d <= n` by metis_tac[GCD_DIVIDES, DIVIDES_MOD_0, DIVIDES_LE] >>
1746 `n = d` by decide_tac >>
1747 metis_tac [divides_iff_gcd_fix],
1748 qabbrev_tac `q = gcd a m` >>
1749 `?p. prime p /\ p divides q` by rw[PRIME_FACTOR] >>
1750 `0 < a` by metis_tac[MULT] >>
1751 `q divides a /\ q divides m` by metis_tac[GCD_DIVIDES, DIVIDES_MOD_0] >>
1752 `p divides a /\ p divides m` by metis_tac[DIVIDES_TRANS] >>
1753 `p divides b \/ p divides d` by metis_tac[P_EUCLIDES] >| [
1754 `p divides 1` by metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR, MULT] >>
1755 metis_tac[DIVIDES_ONE, NOT_PRIME_1],
1756 `d divides n` by metis_tac[divides_def] >>
1757 `p divides n` by metis_tac[DIVIDES_TRANS] >>
1758 `?i. 0 < i /\ (p ** i) divides n /\ !k. coprime (p ** k) (n DIV p ** i)` by rw[FACTOR_OUT_PRIME] >>
1759 `?j. 0 < j /\ (p ** j) divides m /\ !k. coprime (p ** k) (m DIV p ** j)` by rw[FACTOR_OUT_PRIME] >>
1760 Cases_on `i > j` >| [
1761 qabbrev_tac `u = p ** i` >>
1762 qabbrev_tac `v = m DIV p ** j` >>
1763 `0 < p` by metis_tac[PRIME_POS] >>
1764 `v divides m` by metis_tac[DIVIDES_COFACTOR, EXP_EQ_0] >>
1765 `?xu. xu IN G /\ (ord xu = u)` by metis_tac[monoid_order_divisor] >>
1766 `?xv. xv IN G /\ (ord xv = v)` by metis_tac[monoid_order_divisor] >>
1767 `coprime u v` by rw[Abbr`u`] >>
1768 `?xz. xz IN G /\ (ord xz = u * v)` by rw[monoid_order_common_coprime] >>
1769 `m = (p ** j) * v` by metis_tac[DIVIDES_FACTORS, EXP_EQ_0] >>
1770 `p ** (i - j) * m = p ** (i - j) * (p ** j) * v` by rw_tac arith_ss[] >>
1771 `j <= i` by decide_tac >>
1772 `p ** (i - j) * (p ** j) = p ** (i - j + j)` by rw[EXP_ADD] >>
1773 `_ = p ** i` by rw[SUB_ADD] >>
1774 `p ** (i - j) * m = u * v` by rw_tac std_ss[Abbr`u`] >>
1775 `0 < i - j` by decide_tac >>
1776 `1 < p ** (i - j)` by rw[ONE_LT_EXP, ONE_LT_PRIME] >>
1777 `m < p ** (i - j) * m` by rw[LT_MULT_RCANCEL] >>
1778 `m < u * v` by metis_tac[] >>
1779 `u * v > m` by decide_tac >>
1780 `u * v <= m` by metis_tac[IN_IMAGE] >>
1781 metis_tac[NOT_GREATER],
1782 `i <= j` by decide_tac >>
1783 `0 < p` by metis_tac[PRIME_POS] >>
1784 `p ** i <> 0 /\ p ** j <> 0` by metis_tac[EXP_EQ_0] >>
1785 `n = (p ** i) * (n DIV p ** i)` by metis_tac[DIVIDES_FACTORS] >>
1786 `m = (p ** j) * (m DIV p ** j)` by metis_tac[DIVIDES_FACTORS] >>
1787 `p ** (j - i) * (p ** i) = p ** (j - i + i)` by rw[EXP_ADD] >>
1788 `_ = p ** j` by rw[SUB_ADD] >>
1789 `m = p ** (j - i) * (p ** i) * (m DIV p ** j)` by rw_tac std_ss[] >>
1790 `_ = (p ** i) * (p ** (j - i) * (m DIV p ** j))` by rw_tac arith_ss[] >>
1791 qabbrev_tac `u = p ** i` >>
1792 qabbrev_tac `v = n DIV u` >>
1793 `u divides m` by metis_tac[divides_def, MULT_COMM] >>
1794 `u divides d` by metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR] >>
1795 `?c. d = c * u` by metis_tac[divides_def] >>
1796 `n = (a * c) * u` by rw_tac arith_ss[] >>
1797 `v = c * a` by metis_tac[MULT_RIGHT_CANCEL, MULT_COMM] >>
1798 `a divides v` by metis_tac[divides_def] >>
1799 `p divides v` by metis_tac[DIVIDES_TRANS] >>
1800 `p divides u` by metis_tac[DIVIDES_EXP_BASE, DIVIDES_REFL] >>
1801 `d <> 0` by metis_tac[MULT_0] >>
1802 `c <> 0` by metis_tac[MULT] >>
1803 `v <> 0` by metis_tac[MULT_EQ_0] >>
1804 `p divides (gcd v u)` by metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR] >>
1805 `coprime u v` by metis_tac[] >>
1806 metis_tac[GCD_SYM, DIVIDES_ONE, NOT_PRIME_1]
1807 ]
1808 ]
1809 ]
1810QED
1811
1812(* This is a milestone theorem. *)
1813
1814(* Another proof based on the following:
1815
1816The Multiplicative Group of a Finite Field (Ryan Vinroot)
1817http://www.math.wm.edu/~vinroot/430S13MultFiniteField.pdf
1818
1819*)
1820
1821(* Theorem: FiniteAbelianMonoid g ==>
1822 !x. x IN G /\ 0 < ord x ==> (ord x) divides (maximal_order g) *)
1823(* Proof:
1824 Note AbelianMonoid g /\ FINITE G by FiniteAbelianMonoid_def
1825 Let ord z = m = maximal_order g, attained by some z IN G.
1826 Let ord x = n, and n <= m since m is maximal_order, so 0 < m.
1827 Then x IN G /\ z IN G
1828 ==> ?y. y IN G /\ ord y = lcm n m by abelian_monoid_order_lcm
1829 Note lcm n m <= m by m is maximal_order
1830 but m <= lcm n m by LCM_LE, lcm is a common multiple
1831 ==> lcm n m = m by EQ_LESS_EQ
1832 or n divides m by divides_iff_lcm_fix
1833*)
1834Theorem monoid_order_divides_maximal[allow_rebind]:
1835 !g:'a monoid.
1836 FiniteAbelianMonoid g ==>
1837 !x. x IN G /\ 0 < ord x ==> (ord x) divides (maximal_order g)
1838Proof
1839 rw[FiniteAbelianMonoid_def] >>
1840 ‘Monoid g’ by metis_tac[AbelianMonoid_def] >>
1841 qabbrev_tac ‘s = IMAGE ord G’ >>
1842 qabbrev_tac ‘m = MAX_SET s’ >>
1843 qabbrev_tac ‘n = ord x’ >>
1844 ‘#e IN G /\ (ord #e = 1)’ by rw[] >>
1845 ‘s <> {}’ by metis_tac[IN_IMAGE, MEMBER_NOT_EMPTY] >>
1846 ‘FINITE s’ by rw[Abbr‘s’] >>
1847 ‘m IN s /\ !y. y IN s ==> y <= m’ by rw[MAX_SET_DEF, Abbr‘m’] >>
1848 ‘?z. z IN G /\ (ord z = m)’ by metis_tac[IN_IMAGE] >>
1849 ‘?y. y IN G /\ (ord y = lcm n m)’ by metis_tac[abelian_monoid_order_lcm] >>
1850 ‘n IN s /\ ord y IN s’ by rw[Abbr‘s’, Abbr‘n’] >>
1851 ‘n <= m /\ lcm n m <= m’ by metis_tac[] >>
1852 ‘0 < m’ by decide_tac >>
1853 ‘m <= lcm n m’ by rw[LCM_LE] >>
1854 rw[divides_iff_lcm_fix]
1855QED
1856
1857(* ------------------------------------------------------------------------- *)
1858(* Monoid Invertibles *)
1859(* ------------------------------------------------------------------------- *)
1860
1861(* The Invertibles are those with inverses. *)
1862Definition monoid_invertibles_def:
1863 monoid_invertibles (g:'a monoid) =
1864 { x | x IN G /\ (?y. y IN G /\ (x * y = #e) /\ (y * x = #e)) }
1865End
1866Overload "G*" = ``monoid_invertibles g``
1867
1868(* Theorem: x IN G* <=> x IN G /\ ?y. y IN G /\ (x * y = #e) /\ (y * x = #e) *)
1869(* Proof: by monoid_invertibles_def. *)
1870Theorem monoid_invertibles_element:
1871 !g:'a monoid x. x IN G* <=> x IN G /\ ?y. y IN G /\ (x * y = #e) /\ (y * x = #e)
1872Proof
1873 rw[monoid_invertibles_def]
1874QED
1875
1876(* Theorem: Monoid g /\ x IN G /\ 0 < ord x ==> x IN G* *)
1877(* Proof:
1878 By monoid_invertibles_def, this is to show:
1879 ?y. y IN G /\ (x * y = #e) /\ (y * x = #e)
1880 Since x ** (ord x) = #e by order_property
1881 and ord x = SUC n by ord x <> 0
1882 Now, x ** SUC n = x * x ** n by monoid_exp_SUC
1883 x ** SUC n = x ** n * x by monoid_exp_suc
1884 and x ** n IN G by monoid_exp_element
1885 Hence taking y = x ** n will satisfy the requirements.
1886*)
1887Theorem monoid_order_nonzero:
1888 !g:'a monoid x. Monoid g /\ x IN G /\ 0 < ord x ==> x IN G*
1889Proof
1890 rw[monoid_invertibles_def] >>
1891 `x ** (ord x) = #e` by rw[order_property] >>
1892 `ord x <> 0` by decide_tac >>
1893 metis_tac[num_CASES, monoid_exp_SUC, monoid_exp_suc, monoid_exp_element]
1894QED
1895
1896(* The Invertibles of a monoid, will be a Group. *)
1897Definition Invertibles_def:
1898 Invertibles (g:'a monoid) : 'a monoid =
1899 <| carrier := G*;
1900 op := g.op;
1901 id := g.id
1902 |>
1903End
1904(*
1905- type_of ``Invertibles g``;
1906> val it = ``:'a moniod`` : hol_type
1907*)
1908
1909(* Theorem: properties of Invertibles *)
1910(* Proof: by Invertibles_def. *)
1911Theorem Invertibles_property:
1912 !g:'a monoid. ((Invertibles g).carrier = G*) /\
1913 ((Invertibles g).op = g.op) /\
1914 ((Invertibles g).id = #e) /\
1915 ((Invertibles g).exp = g.exp)
1916Proof
1917 rw[Invertibles_def, monoid_exp_def, FUN_EQ_THM]
1918QED
1919
1920(* Theorem: (Invertibles g).carrier = monoid_invertibles g *)
1921(* Proof: by Invertibles_def. *)
1922Theorem Invertibles_carrier:
1923 !g:'a monoid. (Invertibles g).carrier = monoid_invertibles g
1924Proof
1925 rw[Invertibles_def]
1926QED
1927
1928(* Theorem: (Invertibles g).carrier SUBSET G *)
1929(* Proof:
1930 (Invertibles g).carrier
1931 = G* by Invertibles_def
1932 = {x | x IN G /\ ... } by monoid_invertibles_def
1933 SUBSET G by SUBSET_DEF
1934*)
1935Theorem Invertibles_subset:
1936 !g:'a monoid. (Invertibles g).carrier SUBSET G
1937Proof
1938 rw[Invertibles_def, monoid_invertibles_def, SUBSET_DEF]
1939QED
1940
1941(* Theorem: order (Invertibles g) x = order g x *)
1942(* Proof: order_def, period_def, Invertibles_property *)
1943Theorem Invertibles_order:
1944 !g:'a monoid. !x. order (Invertibles g) x = order g x
1945Proof
1946 rw[order_def, period_def, Invertibles_property]
1947QED
1948
1949(* ------------------------------------------------------------------------- *)
1950(* Monoid Inverse as an operation *)
1951(* ------------------------------------------------------------------------- *)
1952
1953(* Theorem: x IN G* means inverse of x exists. *)
1954(* Proof: by definition of G*. *)
1955Theorem monoid_inv_from_invertibles:
1956 !g:'a monoid. Monoid g ==> !x. x IN G* ==> ?y. y IN G /\ (x * y = #e) /\ (y * x = #e)
1957Proof
1958 rw[monoid_invertibles_def]
1959QED
1960
1961(* Convert this into the form: !g x. ?y. ..... for SKOLEM_THM *)
1962Theorem lemma[local]:
1963 !(g:'a monoid) x. ?y. Monoid g /\ x IN G* ==> y IN G /\ (x * y = #e) /\ (y * x = #e)
1964Proof
1965 metis_tac[monoid_inv_from_invertibles]
1966QED
1967
1968(* Convert this into the form: !g x. ?y. ..... for SKOLEM_THM
1969
1970 NOTE: added ‘(Monoid g /\ x NOTIN G* ==> y = ARB)’ to make it a total function.
1971val lemma = prove(
1972 “!(g:'a monoid) x.
1973 ?y. (Monoid g /\ x IN G* ==> y IN G /\ (x * y = #e) /\ (y * x = #e)) /\
1974 (Monoid g /\ x NOTIN G* ==> y = ARB)”,
1975 rpt GEN_TAC
1976 >> MP_TAC (Q.SPEC ‘g’ monoid_inv_from_invertibles)
1977 >> Cases_on ‘Monoid g’ >> rw []
1978 >> Cases_on ‘x IN G*’ >> rw []);
1979 *)
1980
1981(* Use Skolemization to generate the monoid_inv_from_invertibles function *)
1982val monoid_inv_def = new_specification(
1983 "monoid_inv_def", ["monoid_inv"], (* name of function *)
1984 SIMP_RULE (srw_ss()) [SKOLEM_THM] lemma);
1985(* |- !g x. Monoid g /\ x IN G* ==>
1986 monoid_inv g x IN G /\ (x * monoid_inv g x = #e) /\
1987 (monoid_inv g x * x = #e) *)
1988(*
1989- type_of ``monoid_inv g``;
1990> val it = ``:'a -> 'a`` : hol_type
1991*)
1992
1993(* Convert inv function to inv field, i.e. m.inv is defined to be monoid_inv. *)
1994val _ = add_record_field ("inv", ``monoid_inv``);
1995(*
1996- type_of ``g.inv``;
1997> val it = ``:'a -> 'a`` : hol_type
1998*)
1999(* val _ = overload_on ("|/", ``g.inv``); *) (* for non-unicode input *)
2000
2001(* for unicode dispaly *)
2002val _ = add_rule{fixity = Suffix 2100,
2003 term_name = "reciprocal",
2004 block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)),
2005 paren_style = ParoundPrec,
2006 pp_elements = [TOK (UnicodeChars.sup_minus ^ UnicodeChars.sup_1)]};
2007Overload reciprocal = ``monoid_inv g``
2008Overload "|/" = ``reciprocal``(* for non-unicode input *)
2009
2010(* This means: reciprocal will have the display $^{-1}$, and here reciprocal is
2011 short-name for monoid_inv g *)
2012
2013(* - monoid_inv_def;
2014> val it = |- !g x. Monoid g /\ x IN G* ==> |/ x IN G /\ (x * |/ x = #e) /\ ( |/ x * x = #e) : thm
2015*)
2016
2017(* Theorem: x IN G* <=> x IN G /\ |/ x IN G /\ (x * |/ x = #e) /\ ( |/ x * x = #e) *)
2018(* Proof: by definition. *)
2019Theorem monoid_inv_def_alt:
2020 !g:'a monoid. Monoid g ==> (!x. x IN G* <=> x IN G /\ |/ x IN G /\ (x * |/ x = #e) /\ ( |/ x * x = #e))
2021Proof
2022 rw[monoid_invertibles_def, monoid_inv_def, EQ_IMP_THM] >>
2023 metis_tac[]
2024QED
2025
2026(* In preparation for: The invertibles of a monoid form a group. *)
2027
2028(* Theorem: x IN G* ==> x IN G *)
2029(* Proof: by definition of G*. *)
2030Theorem monoid_inv_element:
2031 !g:'a monoid. Monoid g ==> !x. x IN G* ==> x IN G
2032Proof
2033 rw[monoid_invertibles_def]
2034QED
2035
2036(* This export will cause rewrites of RHS = x IN G to become proving LHS = x IN G*, which is not useful. *)
2037(* val _ = export_rewrites ["monoid_inv_element"]; *)
2038
2039(* Theorem: #e IN G* *)
2040(* Proof: by monoid_id and definition. *)
2041Theorem monoid_id_invertible[simp]:
2042 !g:'a monoid. Monoid g ==> #e IN G*
2043Proof
2044 rw[monoid_invertibles_def] >>
2045 qexists_tac `#e` >>
2046 rw[]
2047QED
2048
2049
2050(* This is a direct proof, next one is shorter. *)
2051
2052(* Theorem: [Closure for Invertibles] x, y IN G* ==> x * y IN G* *)
2053(* Proof: inverse of (x * y) = (inverse of y) * (inverse of x)
2054 Note x IN G* ==>
2055 |/x IN G /\ (x * |/ x = #e) /\ ( |/ x * x = #e) by monoid_inv_def
2056 y IN G* ==>
2057 |/y IN G /\ (y * |/ y = #e) /\ ( |/ y * y = #e) by monoid_inv_def
2058 Now x * y IN G and | /y * | / x IN G by monoid_op_element
2059 and (x * y) * ( |/ y * |/ x) = #e by monoid_assoc, monoid_lid
2060 also ( |/ y * |/ x) * (x * y) = #e by monoid_assoc, monoid_lid
2061 Thus x * y IN G*, with ( |/ y * |/ x) as its inverse.
2062*)
2063Theorem monoid_inv_op_invertible:
2064 !g:'a monoid. Monoid g ==> !x y. x IN G* /\ y IN G* ==> x * y IN G*
2065Proof
2066 rpt strip_tac>>
2067 `x IN G /\ y IN G` by rw_tac std_ss[monoid_inv_element] >>
2068 `|/ x IN G /\ (x * |/ x = #e) /\ ( |/ x * x = #e)` by rw_tac std_ss[monoid_inv_def] >>
2069 `|/ y IN G /\ (y * |/ y = #e) /\ ( |/ y * y = #e)` by rw_tac std_ss[monoid_inv_def] >>
2070 `x * y IN G /\ |/ y * |/ x IN G` by rw_tac std_ss[monoid_op_element] >>
2071 `(x * y) * ( |/ y * |/ x) = x * ((y * |/ y) * |/ x)` by rw_tac std_ss[monoid_assoc, monoid_op_element] >>
2072 `( |/ y * |/ x) * (x * y) = |/ y * (( |/ x * x) * y)` by rw_tac std_ss[monoid_assoc, monoid_op_element] >>
2073 rw_tac std_ss[monoid_invertibles_def, GSPECIFICATION] >>
2074 metis_tac[monoid_lid]
2075QED
2076
2077(* Better proof of the same theorem. *)
2078
2079(* Theorem: [Closure for Invertibles] x, y IN G* ==> x * y IN G* *)
2080(* Proof: inverse of (x * y) = (inverse of y) * (inverse of x) *)
2081Theorem monoid_inv_op_invertible[allow_rebind,simp]:
2082 !g:'a monoid. Monoid g ==> !x y. x IN G* /\ y IN G* ==> x * y IN G*
2083Proof
2084 rw[monoid_invertibles_def] >>
2085 qexists_tac `y'' * y'` >>
2086 rw_tac std_ss[monoid_op_element] >| [
2087 `x * y * (y'' * y') = x * ((y * y'') * y')` by rw[monoid_assoc],
2088 `y'' * y' * (x * y) = y'' * ((y' * x) * y)` by rw[monoid_assoc]
2089 ] >> rw_tac std_ss[monoid_lid]
2090QED
2091
2092(* Theorem: x IN G* ==> |/ x IN G* *)
2093(* Proof: by monoid_inv_def. *)
2094Theorem monoid_inv_invertible[simp]:
2095 !g:'a monoid. Monoid g ==> !x. x IN G* ==> |/ x IN G*
2096Proof
2097 rpt strip_tac >>
2098 rw[monoid_invertibles_def] >-
2099 rw[monoid_inv_def] >>
2100 metis_tac[monoid_inv_def, monoid_inv_element]
2101QED
2102
2103
2104(* Theorem: The Invertibles of a monoid form a monoid. *)
2105(* Proof: by checking definition. *)
2106Theorem monoid_invertibles_is_monoid:
2107 !g. Monoid g ==> Monoid (Invertibles g)
2108Proof
2109 rpt strip_tac >>
2110 `!x. x IN G* ==> x IN G` by rw[monoid_inv_element] >>
2111 rw[Invertibles_def] >>
2112 rewrite_tac[Monoid_def] >>
2113 rw[monoid_assoc]
2114QED
2115
2116(* ------------------------------------------------------------------------- *)
2117(* Monoid Maps Documentation *)
2118(* ------------------------------------------------------------------------- *)
2119(* Overloading:
2120 H = h.carrier
2121 o = binary operation of homo_monoid: (homo_monoid g f).op
2122 #i = identity of homo_monoid: (homo_monoid g f).id
2123 fG = carrier of homo_monoid: (homo_monoid g f).carrier
2124*)
2125(* Definitions and Theorems (# are exported):
2126
2127 Homomorphism, isomorphism, endomorphism, automorphism and submonoid:
2128 MonoidHomo_def |- !f g h. MonoidHomo f g h <=>
2129 (!x. x IN G ==> f x IN h.carrier) /\ (f #e = h.id) /\
2130 !x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y))
2131 MonoidIso_def |- !f g h. MonoidIso f g h <=> MonoidHomo f g h /\ BIJ f G h.carrier
2132 MonoidEndo_def |- !f g. MonoidEndo f g <=> MonoidHomo f g g
2133 MonoidAuto_def |- !f g. MonoidAuto f g <=> MonoidIso f g g
2134 submonoid_def |- !h g. submonoid h g <=> MonoidHomo I h g
2135
2136 Monoid Homomorphisms:
2137 monoid_homo_id |- !f g h. MonoidHomo f g h ==> (f #e = h.id)
2138 monoid_homo_element |- !f g h. MonoidHomo f g h ==> !x. x IN G ==> f x IN h.carrier
2139 monoid_homo_cong |- !g h f1 f2. Monoid g /\ Monoid h /\ (!x. x IN G ==> (f1 x = f2 x)) ==>
2140 (MonoidHomo f1 g h <=> MonoidHomo f2 g h)
2141 monoid_homo_I_refl |- !g. MonoidHomo I g g
2142 monoid_homo_trans |- !g h k f1 f2. MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k
2143 monoid_homo_sym |- !g h f. Monoid g /\ MonoidHomo f g h /\ BIJ f G h.carrier ==> MonoidHomo (LINV f G) h g
2144 monoid_homo_compose |- !g h k f1 f2. MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k
2145 monoid_homo_exp |- !g h f. Monoid g /\ MonoidHomo f g h ==>
2146 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n
2147
2148 Monoid Isomorphisms:
2149 monoid_iso_property |- !f g h. MonoidIso f g h <=>
2150 MonoidHomo f g h /\ !y. y IN h.carrier ==> ?!x. x IN G /\ (f x = y)
2151 monoid_iso_id |- !f g h. MonoidIso f g h ==> (f #e = h.id)
2152 monoid_iso_element |- !f g h. MonoidIso f g h ==> !x. x IN G ==> f x IN h.carrier
2153 monoid_iso_monoid |- !g h f. Monoid g /\ MonoidIso f g h ==> Monoid h
2154 monoid_iso_I_refl |- !g. MonoidIso I g g
2155 monoid_iso_trans |- !g h k f1 f2. MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k
2156 monoid_iso_sym |- !g h f. Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g
2157 monoid_iso_compose |- !g h k f1 f2. MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k
2158 monoid_iso_exp |- !g h f. Monoid g /\ MonoidIso f g h ==>
2159 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n
2160 monoid_iso_linv_iso |- !g h f. Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g
2161 monoid_iso_bij |- !g h f. MonoidIso f g h ==> BIJ f G h.carrier
2162 monoid_iso_eq_id |- !g h f. Monoid g /\ Monoid h /\ MonoidIso f g h ==>
2163 !x. x IN G ==> ((f x = h.id) <=> (x = #e))
2164 monoid_iso_order |- !g h f. Monoid g /\ Monoid h /\ MonoidIso f g h ==>
2165 !x. x IN G ==> (order h (f x) = ord x)
2166 monoid_iso_card_eq |- !g h f. MonoidIso f g h /\ FINITE G ==> (CARD G = CARD h.carrier)
2167
2168 Monoid Automorphisms:
2169 monoid_auto_id |- !f g. MonoidAuto f g ==> (f #e = #e)
2170 monoid_auto_element |- !f g. MonoidAuto f g ==> !x. x IN G ==> f x IN G
2171 monoid_auto_compose |- !g f1 f2. MonoidAuto f1 g /\ MonoidAuto f2 g ==> MonoidAuto (f1 o f2) g
2172 monoid_auto_exp |- !g f. Monoid g /\ MonoidAuto f g ==>
2173 !x. x IN G ==> !n. f (x ** n) = f x ** n
2174 monoid_auto_I |- !g. MonoidAuto I g
2175 monoid_auto_linv_auto|- !g f. Monoid g /\ MonoidAuto f g ==> MonoidAuto (LINV f G) g
2176 monoid_auto_bij |- !g f. MonoidAuto f g ==> f PERMUTES G
2177 monoid_auto_order |- !g f. Monoid g /\ MonoidAuto f g ==>
2178 !x. x IN G ==> (ord (f x) = ord x)
2179
2180 Submonoids:
2181 submonoid_eqn |- !g h. submonoid h g <=> H SUBSET G /\
2182 (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\ (h.id = #e)
2183 submonoid_subset |- !g h. submonoid h g ==> H SUBSET G
2184 submonoid_homo_homo |- !g h k f. submonoid h g /\ MonoidHomo f g k ==> MonoidHomo f h k
2185 submonoid_refl |- !g. submonoid g g
2186 submonoid_trans |- !g h k. submonoid g h /\ submonoid h k ==> submonoid g k
2187 submonoid_I_antisym |- !g h. submonoid h g /\ submonoid g h ==> MonoidIso I h g
2188 submonoid_carrier_antisym |- !g h. submonoid h g /\ G SUBSET H ==> MonoidIso I h g
2189 submonoid_order_eqn |- !g h. Monoid g /\ Monoid h /\ submonoid h g ==>
2190 !x. x IN H ==> (order h x = ord x)
2191
2192 Homomorphic Image of Monoid:
2193 image_op_def |- !g f x y. image_op g f x y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y))
2194 image_op_inj |- !g f. INJ f G univ(:'b) ==>
2195 !x y. x IN G /\ y IN G ==> (image_op g f (f x) (f y) = f (x * y))
2196 homo_monoid_def |- !g f. homo_monoid g f = <|carrier := IMAGE f G; op := image_op g f; id := f #e|>
2197 homo_monoid_property |- !g f. (fG = IMAGE f G) /\
2198 (!x y. x IN fG /\ y IN fG ==>
2199 (x o y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)))) /\
2200 (#i = f #e)
2201 homo_monoid_element |- !g f x. x IN G ==> f x IN fG
2202 homo_monoid_id |- !g f. f #e = #i
2203 homo_monoid_op_inj |- !g f. INJ f G univ(:'b) ==> !x y. x IN G /\ y IN G ==> (f (x * y) = f x o f y)
2204 homo_monoid_I |- !g. MonoidIso I (homo_group g I) g
2205
2206 homo_monoid_closure |- !g f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==>
2207 !x y. x IN fG /\ y IN fG ==> x o y IN fG
2208 homo_monoid_assoc |- !g f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==>
2209 !x y z. x IN fG /\ y IN fG /\ z IN fG ==> ((x o y) o z = x o y o z)
2210 homo_monoid_id_property |- !g f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> #i IN fG /\
2211 !x. x IN fG ==> (#i o x = x) /\ (x o #i = x)
2212 homo_monoid_comm |- !g f. AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==>
2213 !x y. x IN fG /\ y IN fG ==> (x o y = y o x)
2214 homo_monoid_monoid |- !g f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> Monoid (homo_monoid g f)
2215 homo_monoid_abelian_monoid |- !g f. AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==>
2216 AbelianMonoid (homo_monoid g f)
2217 homo_monoid_by_inj |- !g f. Monoid g /\ INJ f G univ(:'b) ==> MonoidHomo f g (homo_monoid g f)
2218
2219 Weaker form of Homomorphic of Monoid and image of identity:
2220 WeakHomo_def |- !f g h. WeakHomo f g h <=>
2221 (!x. x IN G ==> f x IN h.carrier) /\
2222 !x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y))
2223 WeakIso_def |- !f g h. WeakIso f g h <=> WeakHomo f g h /\ BIJ f G h.carrier
2224 monoid_weak_iso_id |- !f g h. Monoid g /\ Monoid h /\ WeakIso f g h ==> (f #e = h.id)
2225
2226 Injective Image of Monoid:
2227 monoid_inj_image_def |- !g f. monoid_inj_image g f =
2228 <|carrier := IMAGE f G;
2229 op := (let t = LINV f G in \x y. f (t x * t y));
2230 id := f #e
2231 |>
2232 monoid_inj_image_monoid |- !g f. Monoid g /\ INJ f G univ(:'b) ==> Monoid (monoid_inj_image g f)
2233 monoid_inj_image_abelian_monoid |- !g f. AbelianMonoid g /\ INJ f G univ(:'b) ==> AbelianMonoid (monoid_inj_image g f)
2234 monoid_inj_image_monoid_homo |- !g f. INJ f G univ(:'b) ==> MonoidHomo f g (monoid_inj_image g f)
2235*)
2236
2237(* ------------------------------------------------------------------------- *)
2238(* Homomorphism, isomorphism, endomorphism, automorphism and submonoid. *)
2239(* ------------------------------------------------------------------------- *)
2240
2241(* val _ = overload_on ("H", ``h.carrier``);
2242
2243- type_of ``H``;
2244> val it = ``:'a -> bool`` : hol_type
2245
2246then MonoidIso f g h = MonoidHomo f g h /\ BIJ f G H
2247will make MonoidIso apply only for f: 'a -> 'a.
2248
2249will need val _ = overload_on ("H", ``(h:'b monoid).carrier``);
2250*)
2251
2252(* A function f from g to h is a homomorphism if monoid properties are preserved. *)
2253(* For monoids, need to ensure that identity is preserved, too. See: monoid_weak_iso_id. *)
2254Definition MonoidHomo_def:
2255 MonoidHomo (f:'a -> 'b) (g:'a monoid) (h:'b monoid) <=>
2256 (!x. x IN G ==> f x IN h.carrier) /\
2257 (!x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y))) /\
2258 (f #e = h.id)
2259End
2260(*
2261If MonoidHomo_def uses the condition: !x y. f (x * y) = h.op (f x) (f y)
2262this will mean a corresponding change in GroupHomo_def, but then
2263in quotientGroup <<normal_subgroup_coset_homo>> will give a goal:
2264h <= g ==> x * y * H = (x * H) o (y * H) with no qualification on x, y!
2265*)
2266
2267(* A function f from g to h is an isomorphism if f is a bijective homomorphism. *)
2268Definition MonoidIso_def:
2269 MonoidIso f g h <=> MonoidHomo f g h /\ BIJ f G h.carrier
2270End
2271
2272(* A monoid homomorphism from g to g is an endomorphism. *)
2273Definition MonoidEndo_def: MonoidEndo f g <=> MonoidHomo f g g
2274End
2275
2276(* A monoid isomorphism from g to g is an automorphism. *)
2277Definition MonoidAuto_def: MonoidAuto f g <=> MonoidIso f g g
2278End
2279
2280(* A submonoid h of g if identity is a homomorphism from h to g *)
2281Definition submonoid_def: submonoid h g <=> MonoidHomo I h g
2282End
2283
2284(* ------------------------------------------------------------------------- *)
2285(* Monoid Homomorphisms *)
2286(* ------------------------------------------------------------------------- *)
2287
2288(* Theorem: MonoidHomo f g h ==> (f #e = h.id) *)
2289(* Proof: by MonoidHomo_def. *)
2290Theorem monoid_homo_id:
2291 !f g h. MonoidHomo f g h ==> (f #e = h.id)
2292Proof
2293 rw[MonoidHomo_def]
2294QED
2295
2296(* Theorem: MonoidHomo f g h ==> !x. x IN G ==> f x IN h.carrier *)
2297(* Proof: by MonoidHomo_def *)
2298Theorem monoid_homo_element:
2299 !f g h. MonoidHomo f g h ==> !x. x IN G ==> f x IN h.carrier
2300Proof
2301 rw_tac std_ss[MonoidHomo_def]
2302QED
2303
2304(* Theorem: Monoid g /\ Monoid h /\ (!x. x IN G ==> (f1 x = f2 x)) ==> (MonoidHomo f1 g h = MonoidHomo f2 g h) *)
2305(* Proof: by MonoidHomo_def, monoid_op_element, monoid_id_element *)
2306Theorem monoid_homo_cong:
2307 !g h f1 f2. Monoid g /\ Monoid h /\ (!x. x IN G ==> (f1 x = f2 x)) ==>
2308 (MonoidHomo f1 g h = MonoidHomo f2 g h)
2309Proof
2310 rw_tac std_ss[MonoidHomo_def, EQ_IMP_THM] >-
2311 metis_tac[monoid_op_element] >-
2312 metis_tac[monoid_id_element] >-
2313 metis_tac[monoid_op_element] >>
2314 metis_tac[monoid_id_element]
2315QED
2316
2317(* Theorem: MonoidHomo I g g *)
2318(* Proof: by MonoidHomo_def. *)
2319Theorem monoid_homo_I_refl:
2320 !g:'a monoid. MonoidHomo I g g
2321Proof
2322 rw[MonoidHomo_def]
2323QED
2324
2325(* Theorem: MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo f2 o f1 g k *)
2326(* Proof: true by MonoidHomo_def. *)
2327Theorem monoid_homo_trans:
2328 !(g:'a monoid) (h:'b monoid) (k:'c monoid).
2329 !f1 f2. MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k
2330Proof
2331 rw[MonoidHomo_def]
2332QED
2333
2334(* Theorem: Monoid g /\ MonoidHomo f g h /\ BIJ f G h.carrier ==> MonoidHomo (LINV f G) h g *)
2335(* Proof:
2336 Note BIJ f G h.carrier
2337 ==> BIJ (LINV f G) h.carrier G by BIJ_LINV_BIJ
2338 By MonoidHomo_def, this is to show:
2339 (1) x IN h.carrier ==> LINV f G x IN G
2340 With BIJ (LINV f G) h.carrier G
2341 ==> INJ (LINV f G) h.carrier G by BIJ_DEF
2342 ==> x IN h.carrier ==> LINV f G x IN G by INJ_DEF
2343 (2) x IN h.carrier /\ y IN h.carrier ==> LINV f G (h.op x y) = LINV f G x * LINV f G y
2344 With x IN h.carrier
2345 ==> ?x1. (x = f x1) /\ x1 IN G by BIJ_DEF, SURJ_DEF
2346 With y IN h.carrier
2347 ==> ?y1. (y = f y1) /\ y1 IN G by BIJ_DEF, SURJ_DEF
2348 and x1 * y1 IN G by monoid_op_element
2349 LINV f G (h.op x y)
2350 = LINV f G (f (x1 * y1)) by MonoidHomo_def
2351 = x1 * y1 by BIJ_LINV_THM, x1 * y1 IN G
2352 = (LINV f G (f x1)) * (LINV f G (f y1)) by BIJ_LINV_THM, x1 IN G, y1 IN G
2353 = (LINV f G x) * (LINV f G y) by x = f x1, y = f y1.
2354 (3) LINV f G h.id = #e
2355 Since #e IN G by monoid_id_element
2356 LINV f G h.id
2357 = LINV f G (f #e) by MonoidHomo_def
2358 = #e by BIJ_LINV_THM
2359*)
2360Theorem monoid_homo_sym:
2361 !(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidHomo f g h /\ BIJ f G h.carrier ==>
2362 MonoidHomo (LINV f G) h g
2363Proof
2364 rpt strip_tac >>
2365 `BIJ (LINV f G) h.carrier G` by rw[BIJ_LINV_BIJ] >>
2366 fs[MonoidHomo_def] >>
2367 rpt strip_tac >-
2368 metis_tac[BIJ_DEF, INJ_DEF] >-
2369 (`?x1. (x = f x1) /\ x1 IN G` by metis_tac[BIJ_DEF, SURJ_DEF] >>
2370 `?y1. (y = f y1) /\ y1 IN G` by metis_tac[BIJ_DEF, SURJ_DEF] >>
2371 `g.op x1 y1 IN G` by rw[] >>
2372 metis_tac[BIJ_LINV_THM]) >>
2373 `#e IN G` by rw[] >>
2374 metis_tac[BIJ_LINV_THM]
2375QED
2376
2377Theorem monoid_homo_sym_any:
2378 Monoid g /\ MonoidHomo f g h /\
2379 (!x. x IN h.carrier ==> i x IN g.carrier /\ f (i x) = x) /\
2380 (!x. x IN g.carrier ==> i (f x) = x)
2381 ==>
2382 MonoidHomo i h g
2383Proof
2384 rpt strip_tac >> fs[MonoidHomo_def]
2385 \\ metis_tac[Monoid_def]
2386QED
2387
2388(* Theorem: MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k *)
2389(* Proof: by MonoidHomo_def *)
2390Theorem monoid_homo_compose:
2391 !(g:'a monoid) (h:'b monoid) (k:'c monoid).
2392 !f1 f2. MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k
2393Proof
2394 rw_tac std_ss[MonoidHomo_def]
2395QED
2396(* This is the same as monoid_homo_trans *)
2397
2398(* Theorem: Monoid g /\ MonoidHomo f g h ==> !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n *)
2399(* Proof:
2400 By induction on n.
2401 Base: f (x ** 0) = h.exp (f x) 0
2402 f (x ** 0)
2403 = f #e by monoid_exp_0
2404 = h.id by monoid_homo_id
2405 = h.exp (f x) 0 by monoid_exp_0
2406 Step: f (x ** SUC n) = h.exp (f x) (SUC n)
2407 Note x ** n IN G by monoid_exp_element
2408 f (x ** SUC n)
2409 = f (x * x ** n) by monoid_exp_SUC
2410 = h.op (f x) (f (x ** n)) by MonoidHomo_def
2411 = h.op (f x) (h.exp (f x) n) by induction hypothesis
2412 = h.exp (f x) (SUC n) by monoid_exp_SUC
2413*)
2414Theorem monoid_homo_exp:
2415 !(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidHomo f g h ==>
2416 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n
2417Proof
2418 rpt strip_tac >>
2419 Induct_on `n` >-
2420 rw[monoid_exp_0, monoid_homo_id] >>
2421 fs[monoid_exp_SUC, MonoidHomo_def]
2422QED
2423
2424(* ------------------------------------------------------------------------- *)
2425(* Monoid Isomorphisms *)
2426(* ------------------------------------------------------------------------- *)
2427
2428(* Theorem: MonoidIso f g h <=> MonoidHomo f g h /\ (!y. y IN h.carrier ==> ?!x. x IN G /\ (f x = y)) *)
2429(* Proof:
2430 This is to prove:
2431 (1) BIJ f G H /\ y IN H ==> ?!x. x IN G /\ (f x = y)
2432 true by INJ_DEF and SURJ_DEF.
2433 (2) !y. y IN H /\ MonoidHomo f g h ==> ?!x. x IN G /\ (f x = y) ==> BIJ f G H
2434 true by INJ_DEF and SURJ_DEF, and
2435 x IN G /\ GroupHomo f g h ==> f x IN H by MonoidHomo_def
2436*)
2437Theorem monoid_iso_property:
2438 !f g h. MonoidIso f g h <=> MonoidHomo f g h /\ (!y. y IN h.carrier ==> ?!x. x IN G /\ (f x = y))
2439Proof
2440 rw_tac std_ss[MonoidIso_def, EQ_IMP_THM] >-
2441 metis_tac[BIJ_THM] >>
2442 rw[BIJ_THM] >>
2443 metis_tac[MonoidHomo_def]
2444QED
2445
2446(* Note: all these proofs so far do not require the condition: f #e = h.id in MonoidHomo_def,
2447 but evetually it should, as this is included in definitions of all resources. *)
2448
2449(* Theorem: MonoidIso f g h ==> (f #e = h.id) *)
2450(* Proof: by MonoidIso_def, monoid_homo_id. *)
2451Theorem monoid_iso_id:
2452 !f g h. MonoidIso f g h ==> (f #e = h.id)
2453Proof
2454 rw_tac std_ss[MonoidIso_def, monoid_homo_id]
2455QED
2456
2457(* Theorem: MonoidIso f g h ==> !x. x IN G ==> f x IN h.carrier *)
2458(* Proof: by MonoidIso_def, monoid_homo_element *)
2459Theorem monoid_iso_element:
2460 !f g h. MonoidIso f g h ==> !x. x IN G ==> f x IN h.carrier
2461Proof
2462 metis_tac[MonoidIso_def, monoid_homo_element]
2463QED
2464
2465(* Theorem: Monoid g /\ MonoidIso f g h ==> Monoid h *)
2466(* Proof:
2467 This is to show:
2468 (1) x IN h.carrier /\ y IN h.carrier ==> h.op x y IN h.carrier
2469 Since ?x'. x' IN G /\ (f x' = x) by monoid_iso_property
2470 ?y'. y' IN G /\ (f y' = y) by monoid_iso_property
2471 h.op x y = f (x' * y') by MonoidHomo_def
2472 As x' * y' IN G by monoid_op_element
2473 hence f (x' * y') IN h.carrier by MonoidHomo_def
2474 (2) x IN h.carrier /\ y IN h.carrier /\ z IN h.carrier ==> h.op (h.op x y) z = h.op x (h.op y z)
2475 Since ?x'. x' IN G /\ (f x' = x) by monoid_iso_property
2476 ?y'. y' IN G /\ (f y' = y) by monoid_iso_property
2477 ?z'. z' IN G /\ (f z' = z) by monoid_iso_property
2478 as x' * y' IN G by monoid_op_element
2479 and f (x' * y') IN h.carrier by MonoidHomo_def
2480 ?!t. t IN G /\ f t = f (x' * y') by monoid_iso_property
2481 i.e. t = x' * y' by uniqueness
2482 hence h.op (h.op x y) z = f (x' * y' * z') by MonoidHomo_def
2483 Similary,
2484 as y' * z' IN G by monoid_op_element
2485 and f (y' * z') IN h.carrier by MonoidHomo_def
2486 ?!s. s IN G /\ f s = f (y' * z') by monoid_iso_property
2487 i.e. s = y' * z' by uniqueness
2488 and h.op x (h.op y z) = f (x' * (y' * z')) by MonoidHomo_def
2489 hence true by monoid_assoc.
2490 (3) h.id IN h.carrier
2491 Since #e IN G by monoid_id_element
2492 (f #e) = h.id IN h.carrier by MonoidHomo_def
2493 (4) x IN h.carrier ==> h.op h.id x = x
2494 Since ?x'. x' IN G /\ (f x' = x) by monoid_iso_property
2495 h.id IN h.carrier by monoid_id_element
2496 ?!e. e IN G /\ f e = h.id = f #e by monoid_iso_property
2497 i.e. e = #e by uniqueness
2498 hence h.op h.id x = f (e * x') by MonoidHomo_def
2499 = f (#e * x')
2500 = f x' by monoid_lid
2501 = x
2502 (5) x IN h.carrier ==> h.op x h.id = x
2503 Since ?x'. x' IN G /\ (f x' = x) by monoid_iso_property
2504 h.id IN h.carrier by monoid_id_element
2505 ?!e. e IN G /\ f e = h.id = f #e by monoid_iso_property
2506 i.e. e = #e by uniqueness
2507 hence h.op x h.id = f (x' * e) by MonoidHomo_def
2508 = f (x' * #e)
2509 = f x' by monoid_rid
2510 = x
2511*)
2512Theorem monoid_iso_monoid:
2513 !(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidIso f g h ==> Monoid h
2514Proof
2515 rw[monoid_iso_property] >>
2516 `(!x. x IN G ==> f x IN h.carrier) /\
2517 (!x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y))) /\
2518 (f #e = h.id)` by metis_tac[MonoidHomo_def] >>
2519 rw_tac std_ss[Monoid_def] >-
2520 metis_tac[monoid_op_element] >-
2521 (`?x'. x' IN G /\ (f x' = x)` by metis_tac[] >>
2522 `?y'. y' IN G /\ (f y' = y)` by metis_tac[] >>
2523 `?z'. z' IN G /\ (f z' = z)` by metis_tac[] >>
2524 `?t. t IN G /\ (t = x' * y')` by metis_tac[monoid_op_element] >>
2525 `h.op (h.op x y) z = f (x' * y' * z')` by metis_tac[] >>
2526 `?s. s IN G /\ (s = y' * z')` by metis_tac[monoid_op_element] >>
2527 `h.op x (h.op y z) = f (x' * (y' * z'))` by metis_tac[] >>
2528 `x' * y' * z' = x' * (y' * z')` by rw[monoid_assoc] >>
2529 metis_tac[]) >-
2530 metis_tac[monoid_id_element, MonoidHomo_def] >-
2531 metis_tac[monoid_lid, monoid_id_element] >>
2532 metis_tac[monoid_rid, monoid_id_element]
2533QED
2534
2535(* Theorem: MonoidIso I g g *)
2536(* Proof:
2537 By MonoidIso_def, this is to show:
2538 (1) MonoidHomo I g g, true by monoid_homo_I_refl
2539 (2) BIJ I R R, true by BIJ_I_SAME
2540*)
2541Theorem monoid_iso_I_refl:
2542 !g:'a monoid. MonoidIso I g g
2543Proof
2544 rw[MonoidIso_def, monoid_homo_I_refl, BIJ_I_SAME]
2545QED
2546
2547(* Theorem: MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k *)
2548(* Proof:
2549 By MonoidIso_def, this is to show:
2550 (1) MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k
2551 True by monoid_homo_trans.
2552 (2) BIJ f1 G h.carrier /\ BIJ f2 h.carrier k.carrier ==> BIJ (f2 o f1) G k.carrier
2553 True by BIJ_COMPOSE.
2554*)
2555Theorem monoid_iso_trans:
2556 !(g:'a monoid) (h:'b monoid) (k:'c monoid).
2557 !f1 f2. MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k
2558Proof
2559 rw[MonoidIso_def] >-
2560 metis_tac[monoid_homo_trans] >>
2561 metis_tac[BIJ_COMPOSE]
2562QED
2563
2564(* Theorem: Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g *)
2565(* Proof:
2566 By MonoidIso_def, this is to show:
2567 (1) MonoidHomo f g h /\ BIJ f G h.carrier ==> MonoidHomo (LINV f G) h g
2568 True by monoid_homo_sym.
2569 (2) BIJ f G h.carrier ==> BIJ (LINV f G) h.carrier G
2570 True by BIJ_LINV_BIJ
2571*)
2572Theorem monoid_iso_sym:
2573 !(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g
2574Proof
2575 rw[MonoidIso_def, monoid_homo_sym, BIJ_LINV_BIJ]
2576QED
2577
2578(* Theorem: MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k *)
2579(* Proof:
2580 By MonoidIso_def, this is to show:
2581 (1) MonoidHomo f1 g h /\ MonoidHomo f2 h k ==> MonoidHomo (f2 o f1) g k
2582 True by monoid_homo_compose.
2583 (2) BIJ f1 G h.carrier /\ BIJ f2 h.carrier k.carrier ==> BIJ (f2 o f1) G k.carrier
2584 True by BIJ_COMPOSE
2585*)
2586Theorem monoid_iso_compose:
2587 !(g:'a monoid) (h:'b monoid) (k:'c monoid).
2588 !f1 f2. MonoidIso f1 g h /\ MonoidIso f2 h k ==> MonoidIso (f2 o f1) g k
2589Proof
2590 rw_tac std_ss[MonoidIso_def] >-
2591 metis_tac[monoid_homo_compose] >>
2592 metis_tac[BIJ_COMPOSE]
2593QED
2594(* This is the same as monoid_iso_trans. *)
2595
2596(* Theorem: Monoid g /\ MonoidIso f g h ==> !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n *)
2597(* Proof: by MonoidIso_def, monoid_homo_exp *)
2598Theorem monoid_iso_exp:
2599 !(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidIso f g h ==>
2600 !x. x IN G ==> !n. f (x ** n) = h.exp (f x) n
2601Proof
2602 rw[MonoidIso_def, monoid_homo_exp]
2603QED
2604
2605(* Theorem: Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g *)
2606(* Proof:
2607 By MonoidIso_def, MonoidHomo_def, this is to show:
2608 (1) BIJ f G h.carrier /\ x IN h.carrier ==> LINV f G x IN G
2609 True by BIJ_LINV_ELEMENT
2610 (2) BIJ f G h.carrier /\ x IN h.carrier /\ y IN h.carrier ==> LINV f G (h.op x y) = LINV f G x * LINV f G y
2611 Let x' = LINV f G x, y' = LINV f G y.
2612 Then x' IN G /\ y' IN G by BIJ_LINV_ELEMENT
2613 so x' * y' IN G by monoid_op_element
2614 ==> f (x' * y') = h.op (f x') (f y') by MonoidHomo_def
2615 = h.op x y by BIJ_LINV_THM
2616 Thus LINV f G (h.op x y)
2617 = LINV f G (f (x' * y')) by above
2618 = x' * y' by BIJ_LINV_THM
2619 (3) BIJ f G h.carrier ==> LINV f G h.id = #e
2620 Note #e IN G by monoid_id_element
2621 and f #e = h.id by MonoidHomo_def
2622 ==> LINV f G h.id = #e by BIJ_LINV_THM
2623 (4) BIJ f G h.carrier ==> BIJ (LINV f G) h.carrier G
2624 True by BIJ_LINV_BIJ
2625*)
2626Theorem monoid_iso_linv_iso:
2627 !(g:'a monoid) (h:'b monoid) f. Monoid g /\ MonoidIso f g h ==> MonoidIso (LINV f G) h g
2628Proof
2629 rw_tac std_ss[MonoidIso_def, MonoidHomo_def] >-
2630 metis_tac[BIJ_LINV_ELEMENT] >-
2631 (qabbrev_tac `x' = LINV f G x` >>
2632 qabbrev_tac `y' = LINV f G y` >>
2633 metis_tac[BIJ_LINV_THM, BIJ_LINV_ELEMENT, monoid_op_element]) >-
2634 metis_tac[BIJ_LINV_THM, monoid_id_element] >>
2635 rw_tac std_ss[BIJ_LINV_BIJ]
2636QED
2637(* This is the same as monoid_iso_sym, just a direct proof. *)
2638
2639(* Theorem: MonoidIso f g h ==> BIJ f G h.carrier *)
2640(* Proof: by MonoidIso_def *)
2641Theorem monoid_iso_bij:
2642 !(g:'a monoid) (h:'b monoid) f. MonoidIso f g h ==> BIJ f G h.carrier
2643Proof
2644 rw_tac std_ss[MonoidIso_def]
2645QED
2646
2647(* Theorem: Monoid g /\ Monoid h /\ MonoidIso f g h ==>
2648 !x. x IN G ==> ((f x = h.id) <=> (x = #e)) *)
2649(* Proof:
2650 Note MonoidHomo f g h /\ BIJ f G h.carrier by MonoidIso_def
2651 If part: x IN G /\ f x = h.id ==> x = #e
2652 By monoid_id_unique, this is to show:
2653 (1) !y. y IN G ==> y * x = y
2654 Let z = y * x.
2655 Then z IN G by monoid_op_element
2656 f z = h.op (f y) (f x) by MonoidHomo_def
2657 = h.op (f y) h.id by f x = h.id
2658 = f y by monoid_homo_element, monoid_id
2659 Thus z = y by BIJ_DEF, INJ_DEF
2660 (2) !y. y IN G ==> x * y = y
2661 Let z = x * y.
2662 Then z IN G by monoid_op_element
2663 f z = h.op (f x) (f y) by MonoidHomo_def
2664 = h.op h.id (f y) by f x = h.id
2665 = f y by monoid_homo_element, monoid_id
2666 Thus z = y by BIJ_DEF, INJ_DEF
2667
2668 Only-if part: f #e = h.id, true by monoid_homo_id
2669*)
2670Theorem monoid_iso_eq_id:
2671 !(g:'a monoid) (h:'b monoid) f. Monoid g /\ Monoid h /\ MonoidIso f g h ==>
2672 !x. x IN G ==> ((f x = h.id) <=> (x = #e))
2673Proof
2674 rw[MonoidIso_def] >>
2675 rw[EQ_IMP_THM] >| [
2676 rw[GSYM monoid_id_unique] >| [
2677 qabbrev_tac `z = x' * x` >>
2678 `z IN G` by rw[Abbr`z`] >>
2679 `f z = h.op (f x') (f x)` by fs[MonoidHomo_def, Abbr`z`] >>
2680 `_ = f x'` by metis_tac[monoid_homo_element, monoid_id] >>
2681 metis_tac[BIJ_DEF, INJ_DEF],
2682 qabbrev_tac `z = x * x'` >>
2683 `z IN G` by rw[Abbr`z`] >>
2684 `f z = h.op (f x) (f x')` by fs[MonoidHomo_def, Abbr`z`] >>
2685 `_ = f x'` by metis_tac[monoid_homo_element, monoid_id] >>
2686 metis_tac[BIJ_DEF, INJ_DEF]
2687 ],
2688 rw[monoid_homo_id]
2689 ]
2690QED
2691
2692(* Theorem: Monoid g /\ Monoid h /\ MonoidIso f g h ==> !x. x IN G ==> (order h (f x) = ord x) *)
2693(* Proof:
2694 Let n = ord x, y = f x.
2695 If n = 0, to show: order h y = 0.
2696 By contradiction, suppose order h y <> 0.
2697 Let m = order h y.
2698 Note h.id = h.exp y m by order_property
2699 = f (x ** m) by monoid_iso_exp
2700 Thus x ** m = #e by monoid_iso_eq_id, monoid_exp_element
2701 But x ** m <> #e by order_eq_0, ord x = 0
2702 This is a contradiction.
2703
2704 If n <> 0, to show: order h y = n.
2705 Note ord x = n
2706 ==> (x ** n = #e) /\
2707 !m. 0 < m /\ m < n ==> x ** m <> #e by order_thm, 0 < n
2708 Note h.exp y n = f (x ** n) by monoid_iso_exp
2709 = f #e by x ** n = #e
2710 = h.id by monoid_iso_id, [1]
2711 Claim: !m. 0 < m /\ m < n ==> h.exp y m <> h.id
2712 Proof: By contradiction, suppose h.exp y m = h.id.
2713 Then f (x ** m) = h.exp y m by monoid_iso_exp
2714 = h.id by above
2715 or x ** m = #e by monoid_iso_eq_id, monoid_exp_element
2716 But !m. 0 < m /\ m < n ==> x ** m <> #e by above
2717 This is a contradiction.
2718
2719 Thus by [1] and claim, order h y = n by order_thm
2720*)
2721Theorem monoid_iso_order:
2722 !(g:'a monoid) (h:'b monoid) f. Monoid g /\ Monoid h /\ MonoidIso f g h ==>
2723 !x. x IN G ==> (order h (f x) = ord x)
2724Proof
2725 rpt strip_tac >>
2726 qabbrev_tac `n = ord x` >>
2727 qabbrev_tac `y = f x` >>
2728 Cases_on `n = 0` >| [
2729 spose_not_then strip_assume_tac >>
2730 qabbrev_tac `m = order h y` >>
2731 `0 < m` by decide_tac >>
2732 `h.exp y m = h.id` by metis_tac[order_property] >>
2733 `f (x ** m) = h.id` by metis_tac[monoid_iso_exp] >>
2734 `x ** m = #e` by metis_tac[monoid_iso_eq_id, monoid_exp_element] >>
2735 metis_tac[order_eq_0],
2736 `0 < n` by decide_tac >>
2737 `(x ** n = #e) /\ !m. 0 < m /\ m < n ==> x ** m <> #e` by metis_tac[order_thm] >>
2738 `h.exp y n = h.id` by metis_tac[monoid_iso_exp, monoid_iso_id] >>
2739 `!m. 0 < m /\ m < n ==> h.exp y m <> h.id` by
2740 (spose_not_then strip_assume_tac >>
2741 `f (x ** m) = h.id` by metis_tac[monoid_iso_exp] >>
2742 `x ** m = #e` by metis_tac[monoid_iso_eq_id, monoid_exp_element] >>
2743 metis_tac[]) >>
2744 metis_tac[order_thm]
2745 ]
2746QED
2747
2748(* Theorem: MonoidIso f g h /\ FINITE G ==> (CARD G = CARD h.carrier) *)
2749(* Proof: by MonoidIso_def, FINITE_BIJ_CARD. *)
2750Theorem monoid_iso_card_eq:
2751 !g:'a monoid h:'b monoid f. MonoidIso f g h /\ FINITE G ==> (CARD G = CARD h.carrier)
2752Proof
2753 metis_tac[MonoidIso_def, FINITE_BIJ_CARD]
2754QED
2755
2756(* ------------------------------------------------------------------------- *)
2757(* Monoid Automorphisms *)
2758(* ------------------------------------------------------------------------- *)
2759
2760(* Theorem: MonoidAuto f g ==> (f #e = #e) *)
2761(* Proof: by MonoidAuto_def, monoid_iso_id. *)
2762Theorem monoid_auto_id:
2763 !f g. MonoidAuto f g ==> (f #e = #e)
2764Proof
2765 rw_tac std_ss[MonoidAuto_def, monoid_iso_id]
2766QED
2767
2768(* Theorem: MonoidAuto f g ==> !x. x IN G ==> f x IN G *)
2769(* Proof: by MonoidAuto_def, monoid_iso_element *)
2770Theorem monoid_auto_element:
2771 !f g. MonoidAuto f g ==> !x. x IN G ==> f x IN G
2772Proof
2773 metis_tac[MonoidAuto_def, monoid_iso_element]
2774QED
2775
2776(* Theorem: MonoidAuto f1 g /\ MonoidAuto f2 g ==> MonoidAuto (f1 o f2) g *)
2777(* Proof: by MonoidAuto_def, monoid_iso_compose *)
2778Theorem monoid_auto_compose:
2779 !(g:'a monoid). !f1 f2. MonoidAuto f1 g /\ MonoidAuto f2 g ==> MonoidAuto (f1 o f2) g
2780Proof
2781 metis_tac[MonoidAuto_def, monoid_iso_compose]
2782QED
2783
2784(* Theorem: Monoid g /\ MonoidAuto f g ==> !x. x IN G ==> !n. f (x ** n) = (f x) ** n *)
2785(* Proof: by MonoidAuto_def, monoid_iso_exp *)
2786Theorem monoid_auto_exp:
2787 !f g. Monoid g /\ MonoidAuto f g ==> !x. x IN G ==> !n. f (x ** n) = (f x) ** n
2788Proof
2789 rw[MonoidAuto_def, monoid_iso_exp]
2790QED
2791
2792(* Theorem: MonoidAuto I g *)
2793(* Proof:
2794 MonoidAuto I g
2795 <=> MonoidIso I g g by MonoidAuto_def
2796 <=> MonoidHomo I g g /\ BIJ f G G by MonoidIso_def
2797 <=> T /\ BIJ f G G by MonoidHomo_def, I_THM
2798 <=> T /\ T by BIJ_I_SAME
2799*)
2800Theorem monoid_auto_I:
2801 !(g:'a monoid). MonoidAuto I g
2802Proof
2803 rw_tac std_ss[MonoidAuto_def, MonoidIso_def, MonoidHomo_def, BIJ_I_SAME]
2804QED
2805
2806(* Theorem: Monoid g /\ MonoidAuto f g ==> MonoidAuto (LINV f G) g *)
2807(* Proof:
2808 MonoidAuto I g
2809 ==> MonoidIso I g g by MonoidAuto_def
2810 ==> MonoidIso (LINV f G) g by monoid_iso_linv_iso
2811 ==> MonoidAuto (LINV f G) g by MonoidAuto_def
2812*)
2813Theorem monoid_auto_linv_auto:
2814 !(g:'a monoid) f. Monoid g /\ MonoidAuto f g ==> MonoidAuto (LINV f G) g
2815Proof
2816 rw_tac std_ss[MonoidAuto_def, monoid_iso_linv_iso]
2817QED
2818
2819(* Theorem: MonoidAuto f g ==> f PERMUTES G *)
2820(* Proof: by MonoidAuto_def, MonoidIso_def *)
2821Theorem monoid_auto_bij:
2822 !g:'a monoid. !f. MonoidAuto f g ==> f PERMUTES G
2823Proof
2824 rw_tac std_ss[MonoidAuto_def, MonoidIso_def]
2825QED
2826
2827(* Theorem: Monoid g /\ MonoidAuto f g ==> !x. x IN G ==> (ord (f x) = ord x) *)
2828(* Proof: by MonoidAuto_def, monoid_iso_order. *)
2829Theorem monoid_auto_order:
2830 !(g:'a monoid) f. Monoid g /\ MonoidAuto f g ==> !x. x IN G ==> (ord (f x) = ord x)
2831Proof
2832 rw[MonoidAuto_def, monoid_iso_order]
2833QED
2834
2835(* ------------------------------------------------------------------------- *)
2836(* Submonoids. *)
2837(* ------------------------------------------------------------------------- *)
2838
2839(* Use H to denote h.carrier *)
2840Overload H = ``(h:'a monoid).carrier``
2841
2842(* Theorem: submonoid h g ==> H SUBSET G /\ (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\ (h.id = #e) *)
2843(* Proof:
2844 submonoid h g
2845 <=> MonoidHomo I h g by submonoid_def
2846 <=> (!x. x IN H ==> I x IN G) /\
2847 (!x y. x IN H /\ y IN H ==> (I (h.op x y) = (I x) * (I y))) /\
2848 (h.id = I #e) by MonoidHomo_def
2849 <=> (!x. x IN H ==> x IN G) /\
2850 (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\
2851 (h.id = #e) by I_THM
2852 <=> H SUBSET G
2853 (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\
2854 (h.id = #e) by SUBSET_DEF
2855*)
2856Theorem submonoid_eqn:
2857 !(g:'a monoid) (h:'a monoid). submonoid h g <=>
2858 H SUBSET G /\ (!x y. x IN H /\ y IN H ==> (h.op x y = x * y)) /\ (h.id = #e)
2859Proof
2860 rw_tac std_ss[submonoid_def, MonoidHomo_def, SUBSET_DEF]
2861QED
2862
2863(* Theorem: submonoid h g ==> H SUBSET G *)
2864(* Proof: by submonoid_eqn *)
2865Theorem submonoid_subset:
2866 !(g:'a monoid) (h:'a monoid). submonoid h g ==> H SUBSET G
2867Proof
2868 rw_tac std_ss[submonoid_eqn]
2869QED
2870
2871(* Theorem: submonoid h g /\ MonoidHomo f g k ==> MonoidHomo f h k *)
2872(* Proof:
2873 Note H SUBSET G by submonoid_subset
2874 or !x. x IN H ==> x IN G by SUBSET_DEF
2875 By MonoidHomo_def, this is to show:
2876 (1) x IN H ==> f x IN k.carrier
2877 True by MonoidHomo_def, MonoidHomo f g k
2878 (2) x IN H /\ y IN H /\ f (h.op x y) = k.op (f x) (f y)
2879 Note x IN H ==> x IN G by above
2880 and y IN H ==> y IN G by above
2881 f (h.op x y)
2882 = f (x * y) by submonoid_eqn
2883 = k.op (f x) (f y) by MonoidHomo_def
2884 (3) f h.id = k.id
2885 f (h.id)
2886 = f #e by submonoid_eqn
2887 = k.id by MonoidHomo_def
2888*)
2889Theorem submonoid_homo_homo:
2890 !(g:'a monoid) (h:'a monoid) (k:'b monoid) f. submonoid h g /\ MonoidHomo f g k ==> MonoidHomo f h k
2891Proof
2892 rw_tac std_ss[submonoid_def, MonoidHomo_def]
2893QED
2894
2895(* Theorem: submonoid g g *)
2896(* Proof:
2897 By submonoid_def, this is to show:
2898 MonoidHomo I g g, true by monoid_homo_I_refl.
2899*)
2900Theorem submonoid_refl:
2901 !g:'a monoid. submonoid g g
2902Proof
2903 rw[submonoid_def, monoid_homo_I_refl]
2904QED
2905
2906(* Theorem: submonoid g h /\ submonoid h k ==> submonoid g k *)
2907(* Proof:
2908 By submonoid_def, this is to show:
2909 MonoidHomo I g h /\ MonoidHomo I h k ==> MonoidHomo I g k
2910 Since I o I = I by combinTheory.I_o_ID
2911 This is true by monoid_homo_trans
2912*)
2913Theorem submonoid_trans:
2914 !(g h k):'a monoid. submonoid g h /\ submonoid h k ==> submonoid g k
2915Proof
2916 prove_tac[submonoid_def, combinTheory.I_o_ID, monoid_homo_trans]
2917QED
2918
2919(* Theorem: submonoid h g /\ submonoid g h ==> MonoidIso I h g *)
2920(* Proof:
2921 By submonoid_def, MonoidIso_def, this is to show:
2922 MonoidHomo I h g /\ MonoidHomo I g h ==> BIJ I H G
2923 By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show:
2924 (1) x IN H ==> x IN G, true by submonoid_subset, submonoid h g
2925 (2) x IN G ==> x IN H, true by submonoid_subset, submonoid g h
2926*)
2927Theorem submonoid_I_antisym:
2928 !(g:'a monoid) h. submonoid h g /\ submonoid g h ==> MonoidIso I h g
2929Proof
2930 rw_tac std_ss[submonoid_def, MonoidIso_def] >>
2931 fs[MonoidHomo_def] >>
2932 rw_tac std_ss[BIJ_DEF, INJ_DEF, SURJ_DEF]
2933QED
2934
2935(* Theorem: submonoid h g /\ G SUBSET H ==> MonoidIso I h g *)
2936(* Proof:
2937 By submonoid_def, MonoidIso_def, this is to show:
2938 MonoidHomo I h g /\ G SUBSET H ==> BIJ I H G
2939 By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show:
2940 (1) x IN H ==> x IN G, true by submonoid_subset, submonoid h g
2941 (2) x IN G ==> x IN H, true by G SUBSET H, given
2942*)
2943Theorem submonoid_carrier_antisym:
2944 !(g:'a monoid) h. submonoid h g /\ G SUBSET H ==> MonoidIso I h g
2945Proof
2946 rpt (stripDup[submonoid_def]) >>
2947 rw_tac std_ss[MonoidIso_def] >>
2948 `H SUBSET G` by rw[submonoid_subset] >>
2949 fs[MonoidHomo_def, SUBSET_DEF] >>
2950 rw_tac std_ss[BIJ_DEF, INJ_DEF, SURJ_DEF]
2951QED
2952
2953(* Theorem: Monoid g /\ Monoid h /\ submonoid h g ==> !x. x IN H ==> (order h x = ord x) *)
2954(* Proof:
2955 Note MonoidHomo I h g by submonoid_def
2956 If ord x = 0, to show: order h x = 0.
2957 By contradiction, suppose order h x <> 0.
2958 Let n = order h x.
2959 Then 0 < n by n <> 0
2960 and h.exp x n = h.id by order_property
2961 or x ** n = #e by monoid_homo_exp, monoid_homo_id, I_THM
2962 But x ** n <> #e by order_eq_0, ord x = 0
2963 This is a contradiction.
2964 If ord x <> 0, to show: order h x = ord x.
2965 Note 0 < ord x by ord x <> 0
2966 By order_thm, this is to show:
2967 (1) h.exp x (ord x) = h.id
2968 h.exp x (ord x)
2969 = I (h.exp x (ord x)) by I_THM
2970 = (I x) ** ord x by monoid_homo_exp
2971 = x ** ord x by I_THM
2972 = #e by order_property
2973 = I (h.id) by monoid_homo_id
2974 = h.id by I_THM
2975 (2) 0 < m /\ m < ord x ==> h.exp x m <> h.id
2976 By contradiction, suppose h.exp x m = h.id
2977 h.exp x m
2978 = I (h.exp x m) by I_THM
2979 = (I x) ** m by monoid_homo_exp
2980 = x ** m by I_THM
2981 h.id = I (h.id) by I_THM
2982 = #e by monoid_homo_id
2983 Thus x ** m = #e by h.exp x m = h.id
2984 But x ** m <> #e by order_thm
2985 This is a contradiction.
2986*)
2987Theorem submonoid_order_eqn:
2988 !(g:'a monoid) h. Monoid g /\ Monoid h /\ submonoid h g ==>
2989 !x. x IN H ==> (order h x = ord x)
2990Proof
2991 rw[submonoid_def] >>
2992 `!x. I x = x` by rw[] >>
2993 Cases_on `ord x = 0` >| [
2994 spose_not_then strip_assume_tac >>
2995 qabbrev_tac `n = order h x` >>
2996 `0 < n` by decide_tac >>
2997 `h.exp x n = h.id` by rw[order_property, Abbr`n`] >>
2998 `x ** n = #e` by metis_tac[monoid_homo_exp, monoid_homo_id] >>
2999 metis_tac[order_eq_0],
3000 `0 < ord x` by decide_tac >>
3001 rw[order_thm] >-
3002 metis_tac[monoid_homo_exp, order_property, monoid_homo_id] >>
3003 spose_not_then strip_assume_tac >>
3004 `x ** m = #e` by metis_tac[monoid_homo_exp, monoid_homo_id] >>
3005 metis_tac[order_thm]
3006 ]
3007QED
3008
3009(* ------------------------------------------------------------------------- *)
3010(* Homomorphic Image of Monoid. *)
3011(* ------------------------------------------------------------------------- *)
3012
3013(* Define an operation on images *)
3014Definition image_op_def:
3015 image_op (g:'a monoid) (f:'a -> 'b) x y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y))
3016End
3017
3018(* Theorem: INJ f G univ(:'b) ==> !x y. x IN G /\ y IN G ==> (image_op g f (f x) (f y) = f (x * y)) *)
3019(* Proof:
3020 Note x = CHOICE (preimage f G (f x)) by preimage_inj_choice
3021 and y = CHOICE (preimage f G (f y)) by preimage_inj_choice
3022 image_op g f (f x) (f y)
3023 = f (CHOICE (preimage f G (f x)) * CHOICE (preimage f G (f y)) by image_op_def
3024 = f (x * y) by above
3025*)
3026Theorem image_op_inj:
3027 !g:'a monoid f. INJ f G univ(:'b) ==>
3028 !x y. x IN G /\ y IN G ==> (image_op g f (f x) (f y) = f (g.op x y))
3029Proof
3030 rw[image_op_def, preimage_inj_choice]
3031QED
3032
3033(* Define the homomorphic image of a monoid. *)
3034Definition homo_monoid_def:
3035 homo_monoid (g:'a monoid) (f:'a -> 'b) =
3036 <| carrier := IMAGE f G;
3037 op := image_op g f;
3038 id := f #e
3039 |>
3040End
3041
3042(* set overloading *)
3043Overload o = ``(homo_monoid (g:'a monoid) (f:'a -> 'b)).op``
3044Overload "#i" = ``(homo_monoid (g:'a monoid) (f:'a -> 'b)).id``
3045Overload fG = ``(homo_monoid (g:'a monoid) (f:'a -> 'b)).carrier``
3046
3047(* Theorem: Properties of homo_monoid. *)
3048(* Proof: by homo_monoid_def and image_op_def. *)
3049Theorem homo_monoid_property:
3050 !(g:'a monoid) (f:'a -> 'b). (fG = IMAGE f G) /\
3051 (!x y. x IN fG /\ y IN fG ==> (x o y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)))) /\
3052 (#i = f #e)
3053Proof
3054 rw[homo_monoid_def, image_op_def]
3055QED
3056
3057(* Theorem: !x. x IN G ==> f x IN fG *)
3058(* Proof: by homo_monoid_def, IN_IMAGE *)
3059Theorem homo_monoid_element:
3060 !(g:'a monoid) (f:'a -> 'b). !x. x IN G ==> f x IN fG
3061Proof
3062 rw[homo_monoid_def]
3063QED
3064
3065(* Theorem: f #e = #i *)
3066(* Proof: by homo_monoid_def *)
3067Theorem homo_monoid_id:
3068 !(g:'a monoid) (f:'a -> 'b). f #e = #i
3069Proof
3070 rw[homo_monoid_def]
3071QED
3072
3073(* Theorem: INJ f G univ(:'b) ==>
3074 !x y. x IN G /\ y IN G ==> (f (x * y) = (f x) o (f y)) *)
3075(* Proof:
3076 Note x = CHOICE (preimage f G (f x)) by preimage_inj_choice
3077 and y = CHOICE (preimage f G (f y)) by preimage_inj_choice
3078 f (x * y)
3079 = f (CHOICE (preimage f G (f x)) * CHOICE (preimage f G (f y)) by above
3080 = (f x) o (f y) by homo_monoid_property
3081*)
3082Theorem homo_monoid_op_inj:
3083 !(g:'a monoid) (f:'a -> 'b). INJ f G univ(:'b) ==>
3084 !x y. x IN G /\ y IN G ==> (f (x * y) = (f x) o (f y))
3085Proof
3086 rw[homo_monoid_property, preimage_inj_choice]
3087QED
3088
3089(* Theorem: MonoidIso I (homo_monoid g I) g *)
3090(* Proof:
3091 Note IMAGE I G = G by IMAGE_I
3092 and INJ I G univ(:'a) by INJ_I
3093 and !x. I x = x by I_THM
3094 By MonoidIso_def, this is to show:
3095 (1) MonoidHomo I (homo_monoid g I) g
3096 By MonoidHomo_def, homo_monoid_def, this is to show:
3097 x IN G /\ y IN G ==> image_op g I x y = x * y
3098 This is true by image_op_inj
3099 (2) BIJ I (homo_group g I).carrier G
3100 (homo_group g I).carrier
3101 = IMAGE I G by homo_monoid_property
3102 = G by above, IMAGE_I
3103 This is true by BIJ_I_SAME
3104*)
3105Theorem homo_monoid_I:
3106 !g:'a monoid. MonoidIso I (homo_monoid g I) g
3107Proof
3108 rpt strip_tac >>
3109 `IMAGE I G = G` by rw[] >>
3110 `INJ I G univ(:'a)` by rw[INJ_I] >>
3111 `!x. I x = x` by rw[] >>
3112 rw_tac std_ss[MonoidIso_def] >| [
3113 rw_tac std_ss[MonoidHomo_def, homo_monoid_def] >>
3114 metis_tac[image_op_inj],
3115 rw[homo_monoid_property, BIJ_I_SAME]
3116 ]
3117QED
3118
3119(* Theorem: [Closure] Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> x IN fG /\ y IN fG ==> x o y IN fG *)
3120(* Proof:
3121 Let a = CHOICE (preimage f G x),
3122 b = CHOICE (preimage f G y).
3123 Then a IN G /\ x = f a by preimage_choice_property
3124 b IN G /\ y = f b by preimage_choice_property
3125 x o y
3126 = (f a) o (f b)
3127 = f (a * b) by homo_monoid_property
3128 Note a * b IN G by monoid_op_element
3129 so f (a * b) IN fG by homo_monoid_element
3130*)
3131Theorem homo_monoid_closure:
3132 !(g:'a monoid) (f:'a -> 'b). Monoid g /\ MonoidHomo f g (homo_monoid g f) ==>
3133 !x y. x IN fG /\ y IN fG ==> x o y IN fG
3134Proof
3135 rw_tac std_ss[homo_monoid_property] >>
3136 rw[preimage_choice_property]
3137QED
3138
3139(* Theorem: [Associative] Monoid g /\ MonoidHomo f g (homo_monoid g f) ==>
3140 x IN fG /\ y IN fG /\ z IN fG ==> (x o y) o z = x o (y o z) *)
3141(* Proof:
3142 By MonoidHomo_def,
3143 !x. x IN G ==> f x IN fG
3144 !x y. x IN G /\ y IN G ==> (f (x * y) = f x o f y)
3145 Let a = CHOICE (preimage f G x),
3146 b = CHOICE (preimage f G y),
3147 c = CHOICE (preimage f G z).
3148 Then a IN G /\ x = f a by preimage_choice_property
3149 b IN G /\ y = f b by preimage_choice_property
3150 c IN G /\ z = f c by preimage_choice_property
3151 (x o y) o z
3152 = ((f a) o (f b)) o (f c) by expanding x, y, z
3153 = f (a * b) o (f c) by homo_monoid_property
3154 = f (a * b * c) by homo_monoid_property
3155 = f (a * (b * c)) by monoid_assoc
3156 = (f a) o f (b * c) by homo_monoid_property
3157 = (f a) o ((f b) o (f c)) by homo_monoid_property
3158 = x o (y o z) by contracting x, y, z
3159*)
3160Theorem homo_monoid_assoc:
3161 !(g:'a monoid) (f:'a -> 'b). Monoid g /\ MonoidHomo f g (homo_monoid g f) ==>
3162 !x y z. x IN fG /\ y IN fG /\ z IN fG ==> ((x o y) o z = x o (y o z))
3163Proof
3164 rw_tac std_ss[MonoidHomo_def] >>
3165 `(fG = IMAGE f G) /\ !x y. x IN fG /\ y IN fG ==> (x o y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)))` by rw[homo_monoid_property] >>
3166 qabbrev_tac `a = CHOICE (preimage f G x)` >>
3167 qabbrev_tac `b = CHOICE (preimage f G y)` >>
3168 qabbrev_tac `c = CHOICE (preimage f G z)` >>
3169 `a IN G /\ (f a = x)` by metis_tac[preimage_choice_property] >>
3170 `b IN G /\ (f b = y)` by metis_tac[preimage_choice_property] >>
3171 `c IN G /\ (f c = z)` by metis_tac[preimage_choice_property] >>
3172 `a * b IN G /\ b * c IN G ` by rw[] >>
3173 `a * b * c = a * (b * c)` by rw[monoid_assoc] >>
3174 metis_tac[]
3175QED
3176
3177(* Theorem: [Identity] Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> #i IN fG /\ #i o x = x /\ x o #i = x. *)
3178(* Proof:
3179 By homo_monoid_property, #i = f #e, and #i IN fG.
3180 Since CHOICE (preimage f G x) IN G /\ x = f (CHOICE (preimage f G x)) by preimage_choice_property
3181 hence #i o x
3182 = (f #e) o f (preimage f G x)
3183 = f (#e * preimage f G x) by homo_monoid_property
3184 = f (preimage f G x) by monoid_lid
3185 = x
3186 similarly for x o #i = x by monoid_rid
3187*)
3188Theorem homo_monoid_id_property:
3189 !(g:'a monoid) (f:'a -> 'b). Monoid g /\ MonoidHomo f g (homo_monoid g f) ==>
3190 #i IN fG /\ (!x. x IN fG ==> (#i o x = x) /\ (x o #i = x))
3191Proof
3192 rw[MonoidHomo_def, homo_monoid_property] >-
3193 metis_tac[monoid_lid, monoid_id_element, preimage_choice_property] >>
3194 metis_tac[monoid_rid, monoid_id_element, preimage_choice_property]
3195QED
3196
3197(* Theorem: [Commutative] AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==>
3198 x IN fG /\ y IN fG ==> (x o y = y o x) *)
3199(* Proof:
3200 Note AbelianMonoid g ==> Monoid g and
3201 !x y. x IN G /\ y IN G ==> (x * y = y * x) by AbelianMonoid_def
3202 By MonoidHomo_def,
3203 !x. x IN G ==> f x IN fG
3204 !x y. x IN G /\ y IN G ==> (f (x * y) = f x o f y)
3205 Let a = CHOICE (preimage f G x),
3206 b = CHOICE (preimage f G y).
3207 Then a IN G /\ x = f a by preimage_choice_property
3208 b IN G /\ y = f b by preimage_choice_property
3209 x o y
3210 = (f a) o (f b) by expanding x, y
3211 = f (a * b) by homo_monoid_property
3212 = f (b * a) by AbelianMonoid_def, above
3213 = (f b) o (f a) by homo_monoid_property
3214 = y o x by contracting x, y
3215*)
3216Theorem homo_monoid_comm:
3217 !(g:'a monoid) (f:'a -> 'b). AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==>
3218 !x y. x IN fG /\ y IN fG ==> (x o y = y o x)
3219Proof
3220 rw_tac std_ss[AbelianMonoid_def, MonoidHomo_def] >>
3221 `(fG = IMAGE f G) /\ !x y. x IN fG /\ y IN fG ==> (x o y = f (CHOICE (preimage f G x) * CHOICE (preimage f G y)))` by rw[homo_monoid_property] >>
3222 qabbrev_tac `a = CHOICE (preimage f G x)` >>
3223 qabbrev_tac `b = CHOICE (preimage f G y)` >>
3224 `a IN G /\ (f a = x)` by metis_tac[preimage_choice_property] >>
3225 `b IN G /\ (f b = y)` by metis_tac[preimage_choice_property] >>
3226 `a * b = b * a` by rw[] >>
3227 metis_tac[]
3228QED
3229
3230(* Theorem: Homomorphic image of a monoid is a monoid.
3231 Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> Monoid (homo_monoid g f) *)
3232(* Proof:
3233 This is to show each of these:
3234 (1) x IN fG /\ y IN fG ==> x o y IN fG true by homo_monoid_closure
3235 (2) x IN fG /\ y IN fG /\ z IN fG ==> (x o y) o z = (x o y) o z true by homo_monoid_assoc
3236 (3) #i IN fG, true by homo_monoid_id_property
3237 (4) x IN fG ==> #i o x = x, true by homo_monoid_id_property
3238 (5) x IN fG ==> x o #i = x, true by homo_monoid_id_property
3239*)
3240Theorem homo_monoid_monoid:
3241 !(g:'a monoid) f. Monoid g /\ MonoidHomo f g (homo_monoid g f) ==> Monoid (homo_monoid g f)
3242Proof
3243 rpt strip_tac >>
3244 rw_tac std_ss[Monoid_def] >| [
3245 rw[homo_monoid_closure],
3246 rw[homo_monoid_assoc],
3247 rw[homo_monoid_id_property],
3248 rw[homo_monoid_id_property],
3249 rw[homo_monoid_id_property]
3250 ]
3251QED
3252
3253(* Theorem: Homomorphic image of an Abelian monoid is an Abelian monoid.
3254 AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==> AbelianMonoid (homo_monoid g f) *)
3255(* Proof:
3256 Note AbelianMonoid g ==> Monoid g by AbelianMonoid_def
3257 By AbelianMonoid_def, this is to show:
3258 (1) Monoid (homo_monoid g f), true by homo_monoid_monoid, Monoid g
3259 (2) x IN fG /\ y IN fG ==> x o y = y o x, true by homo_monoid_comm, AbelianMonoid g
3260*)
3261Theorem homo_monoid_abelian_monoid:
3262 !(g:'a monoid) f. AbelianMonoid g /\ MonoidHomo f g (homo_monoid g f) ==> AbelianMonoid (homo_monoid g f)
3263Proof
3264 metis_tac[homo_monoid_monoid, AbelianMonoid_def, homo_monoid_comm]
3265QED
3266
3267(* Theorem: Monoid g /\ INJ f G UNIV ==> MonoidHomo f g (homo_monoid g f) *)
3268(* Proof:
3269 By MonoidHomo_def, homo_monoid_property, this is to show:
3270 (1) x IN G ==> f x IN IMAGE f G, true by IN_IMAGE
3271 (2) x IN G /\ y IN G ==> f (x * y) = f x o f y, true by homo_monoid_op_inj
3272*)
3273Theorem homo_monoid_by_inj:
3274 !(g:'a monoid) (f:'a -> 'b). Monoid g /\ INJ f G UNIV ==> MonoidHomo f g (homo_monoid g f)
3275Proof
3276 rw_tac std_ss[MonoidHomo_def, homo_monoid_property] >-
3277 rw[] >>
3278 rw[homo_monoid_op_inj]
3279QED
3280
3281(* ------------------------------------------------------------------------- *)
3282(* Weaker form of Homomorphic of Monoid and image of identity. *)
3283(* ------------------------------------------------------------------------- *)
3284
3285(* Let us take out the image of identity requirement *)
3286Definition WeakHomo_def:
3287 WeakHomo (f:'a -> 'b) (g:'a monoid) (h:'b monoid) <=>
3288 (!x. x IN G ==> f x IN h.carrier) /\
3289 (!x y. x IN G /\ y IN G ==> (f (x * y) = h.op (f x) (f y)))
3290 (* no requirement for: f #e = h.id *)
3291End
3292
3293(* A function f from g to h is an isomorphism if f is a bijective homomorphism. *)
3294Definition WeakIso_def:
3295 WeakIso f g h <=> WeakHomo f g h /\ BIJ f G h.carrier
3296End
3297
3298(* Then the best we can prove about monoid identities is the following:
3299 Monoid g /\ Monoid h /\ WeakIso f g h ==> f #e = h.id
3300 which is NOT:
3301 Monoid g /\ Monoid h /\ WeakHomo f g h ==> f #e = h.id
3302*)
3303
3304(* Theorem: Monoid g /\ Monoid h /\ WeakIso f g h ==> f #e = h.id *)
3305(* Proof:
3306 By monoid_id_unique:
3307 |- !g. Monoid g ==> !e. e IN G ==> ((!x. x IN G ==> (x * e = x) /\ (e * x = x)) <=> (e = #e)) : thm
3308 Hence this is to show: !x. x IN h.carrier ==> (h.op x (f #e) = x) /\ (h.op (f #e) x = x)
3309 Note that WeakIso f g h = WeakHomo f g h /\ BIJ f G h.carrier.
3310 (1) x IN h.carrier /\ f #e IN h.carrier ==> h.op x (f #e) = x
3311 Since x = f y for some y IN G, by BIJ_THM
3312 h.op x (f #e) = h.op (f y) (f #e)
3313 = f (y * #e) by WeakHomo_def
3314 = f y = x by monoid_rid
3315 (2) x IN h.carrier /\ f #e IN h.carrier ==> h.op (f #e) x = x
3316 Similar to above,
3317 h.op (f #e) x = h.op (f #e) (f y) = f (#e * y) = f y = x by monoid_lid.
3318*)
3319Theorem monoid_weak_iso_id:
3320 !f g h. Monoid g /\ Monoid h /\ WeakIso f g h ==> (f #e = h.id)
3321Proof
3322 rw_tac std_ss[WeakIso_def] >>
3323 `#e IN G /\ f #e IN h.carrier` by metis_tac[WeakHomo_def, monoid_id_element] >>
3324 `!x. x IN h.carrier ==> (h.op x (f #e) = x) /\ (h.op (f #e) x = x)` suffices_by rw_tac std_ss[monoid_id_unique] >>
3325 rpt strip_tac>| [
3326 `?y. y IN G /\ (f y = x)` by metis_tac[BIJ_THM] >>
3327 metis_tac[WeakHomo_def, monoid_rid],
3328 `?y. y IN G /\ (f y = x)` by metis_tac[BIJ_THM] >>
3329 metis_tac[WeakHomo_def, monoid_lid]
3330 ]
3331QED
3332
3333(* ------------------------------------------------------------------------- *)
3334(* Injective Image of Monoid. *)
3335(* ------------------------------------------------------------------------- *)
3336
3337(* Idea: Given a Monoid g, and an injective function f,
3338 then the image (f G) is a Monoid, with an induced binary operator:
3339 op := (\x y. f (f^-1 x * f^-1 y)) *)
3340
3341(* Define a monoid injective image for an injective f, with LINV f G. *)
3342Definition monoid_inj_image_def:
3343 monoid_inj_image (g:'a monoid) (f:'a -> 'b) =
3344 <|carrier := IMAGE f G;
3345 op := let t = LINV f G in (\x y. f (t x * t y));
3346 id := f #e
3347 |>
3348End
3349
3350(* Theorem: Monoid g /\ INJ f G univ(:'b) ==> Monoid (monoid_inj_image g f) *)
3351(* Proof:
3352 Note INJ f G univ(:'b) ==> BIJ f G (IMAGE f G) by INJ_IMAGE_BIJ_ALT
3353 so !x. x IN G ==> t (f x) = x where t = LINV f G
3354 and !x. x IN (IMAGE f G) ==> f (t x) = x by BIJ_LINV_THM
3355 By Monoid_def, monoid_inj_image_def, this is to show:
3356 (1) x IN IMAGE f G /\ y IN IMAGE f G ==> f (t x * t y) IN IMAGE f G
3357 Note ?a. (x = f a) /\ a IN G by IN_IMAGE
3358 ?b. (y = f b) /\ b IN G by IN_IMAGE
3359 Hence f (t x * t y)
3360 = f (t (f a) * t (f b)) by x = f a, y = f b
3361 = f (a * b) by !y. t (f y) = y
3362 Since a * b IN G by monoid_op_element
3363 f (a * b) IN IMAGE f G by IN_IMAGE
3364 (2) x IN IMAGE f G /\ y IN IMAGE f G /\ z IN IMAGE f G ==> f (t (f (t x * t y)) * t z) = f (t x * t (f (t y * t z)))
3365 Note ?a. (x = f a) /\ a IN G by IN_IMAGE
3366 ?b. (y = f b) /\ b IN G by IN_IMAGE
3367 ?c. (z = f c) /\ c IN G by IN_IMAGE
3368 LHS = f (t (f (t x * t y)) * t z))
3369 = f (t (f (t (f a) * t (f b))) * t (f c)) by x = f a, y = f b, z = f c
3370 = f (t (f (a * b)) * c) by !y. t (f y) = y
3371 = f ((a * b) * c) by !y. t (f y) = y, monoid_op_element
3372 RHS = f (t x * t (f (t y * t z)))
3373 = f (t (f a) * t (f (t (f b) * t (f c)))) by x = f a, y = f b, z = f c
3374 = f (a * t (f (b * c))) by !y. t (f y) = y
3375 = f (a * (b * c)) by !y. t (f y) = y
3376 = LHS by monoid_assoc
3377 (3) f #e IN IMAGE f G
3378 Since #e IN G by monoid_id_element
3379 so f #e IN IMAGE f G by IN_IMAGE
3380 (4) x IN IMAGE f G ==> f (t (f #e) * t x) = x
3381 Note ?a. (x = f a) /\ a IN G by IN_IMAGE
3382 and #e IN G by monoid_id_element
3383 Hence f (t (f #e) * t x)
3384 = f (#e * t x) by !y. t (f y) = y
3385 = f (#e * t (f a)) by x = f a
3386 = f (#e * a) by !y. t (f y) = y
3387 = f a by monoid_id
3388 = x by x = f a
3389 (5) x IN IMAGE f G ==> f (t x * t (f #e)) = x
3390 Note ?a. (x = f a) /\ a IN G by IN_IMAGE
3391 and #e IN G by monoid_id_element
3392 Hence f (t x * t (f #e))
3393 = f (t x * #e) by !y. t (f y) = y
3394 = f (t (f a) * #e) by x = f a
3395 = f (a * #e) by !y. t (f y) = y
3396 = f a by monoid_id
3397 = x by x = f a
3398*)
3399Theorem monoid_inj_image_monoid:
3400 !(g:'a monoid) (f:'a -> 'b). Monoid g /\ INJ f G univ(:'b) ==> Monoid (monoid_inj_image g f)
3401Proof
3402 rpt strip_tac >>
3403 `BIJ f G (IMAGE f G)` by rw[INJ_IMAGE_BIJ_ALT] >>
3404 `(!x. x IN G ==> (LINV f G (f x) = x)) /\ (!x. x IN (IMAGE f G) ==> (f (LINV f G x) = x))` by metis_tac[BIJ_LINV_THM] >>
3405 rw_tac std_ss[Monoid_def, monoid_inj_image_def] >| [
3406 `?a. (x = f a) /\ a IN G` by rw[GSYM IN_IMAGE] >>
3407 `?b. (y = f b) /\ b IN G` by rw[GSYM IN_IMAGE] >>
3408 rw[],
3409 `?a. (x = f a) /\ a IN G` by rw[GSYM IN_IMAGE] >>
3410 `?b. (y = f b) /\ b IN G` by rw[GSYM IN_IMAGE] >>
3411 `?c. (z = f c) /\ c IN G` by rw[GSYM IN_IMAGE] >>
3412 rw[monoid_assoc],
3413 rw[],
3414 `?a. (x = f a) /\ a IN G` by rw[GSYM IN_IMAGE] >>
3415 rw[],
3416 `?a. (x = f a) /\ a IN G` by rw[GSYM IN_IMAGE] >>
3417 rw[]
3418 ]
3419QED
3420
3421(* Theorem: AbelianMonoid g /\ INJ f G univ(:'b) ==> AbelianMonoid (monoid_inj_image g f) *)
3422(* Proof:
3423 By AbelianMonoid_def, this is to show:
3424 (1) Monoid g ==> Monoid (monoid_inj_image g f)
3425 True by monoid_inj_image_monoid.
3426 (2) x IN G /\ y IN G ==> (monoid_inj_image g f).op x y = (monoid_inj_image g f).op y x
3427 By monoid_inj_image_def, this is to show:
3428 f (t (f x) * t (f y)) = f (t (f y) * t (f x)) where t = LINV f G
3429 Note INJ f G univ(:'b) ==> BIJ f G (IMAGE f G) by INJ_IMAGE_BIJ_ALT
3430 so !x. x IN G ==> t (f x) = x
3431 and !x. x IN (IMAGE f G) ==> f (t x) = x by BIJ_LINV_THM
3432 f (t (f x) * t (f y))
3433 = f (x * y) by !y. t (f y) = y
3434 = f (y * x) by commutativity condition
3435 = f (t (f y) * t (f x)) by !y. t (f y) = y
3436*)
3437Theorem monoid_inj_image_abelian_monoid:
3438 !(g:'a monoid) (f:'a -> 'b). AbelianMonoid g /\ INJ f G univ(:'b) ==>
3439 AbelianMonoid (monoid_inj_image g f)
3440Proof
3441 rw[AbelianMonoid_def] >-
3442 rw[monoid_inj_image_monoid] >>
3443 pop_assum mp_tac >>
3444 pop_assum mp_tac >>
3445 rw[monoid_inj_image_def] >>
3446 metis_tac[INJ_IMAGE_BIJ_ALT, BIJ_LINV_THM]
3447QED
3448
3449(* Theorem: INJ f G univ(:'b) ==> MonoidHomo f g (monoid_inj_image g f) *)
3450(* Proof:
3451 Let s = IMAGE f G.
3452 Then BIJ f G s by INJ_IMAGE_BIJ_ALT
3453 so INJ f G s by BIJ_DEF
3454
3455 By MonoidHomo_def, monoid_inj_image_def, this is to show:
3456 (1) x IN G ==> f x IN IMAGE f G, true by IN_IMAGE
3457 (2) x IN R /\ y IN R ==> f (x * y) = f (LINV f R (f x) * LINV f R (f y))
3458 Since LINV f R (f x) = x by BIJ_LINV_THM
3459 and LINV f R (f y) = y by BIJ_LINV_THM
3460 The result is true.
3461*)
3462Theorem monoid_inj_image_monoid_homo:
3463 !(g:'a monoid) f. INJ f G univ(:'b) ==> MonoidHomo f g (monoid_inj_image g f)
3464Proof
3465 rw[MonoidHomo_def, monoid_inj_image_def] >>
3466 qabbrev_tac `s = IMAGE f G` >>
3467 `BIJ f G s` by rw[INJ_IMAGE_BIJ_ALT, Abbr`s`] >>
3468 `INJ f G s` by metis_tac[BIJ_DEF] >>
3469 metis_tac[BIJ_LINV_THM]
3470QED
3471
3472(* ------------------------------------------------------------------------- *)
3473(* Submonoid Documentation *)
3474(* ------------------------------------------------------------------------- *)
3475(* Overloading (# are temporary):
3476# K = k.carrier
3477# x o y = h.op x y
3478# #i = h.id
3479 h << g = Submonoid h g
3480 h mINTER k = monoid_intersect h k
3481 smbINTER g = submonoid_big_intersect g
3482*)
3483(* Definitions and Theorems (# are exported):
3484
3485 Helper Theorems:
3486
3487 Submonoid of a Monoid:
3488 Submonoid_def |- !h g. h << g <=>
3489 Monoid h /\ Monoid g /\ H SUBSET G /\ ($o = $* ) /\ (#i = #e)
3490 submonoid_property |- !g h. h << g ==>
3491 Monoid h /\ Monoid g /\ H SUBSET G /\
3492 (!x y. x IN H /\ y IN H ==> (x o y = x * y)) /\ (#i = #e)
3493 submonoid_carrier_subset |- !g h. h << g ==> H SUBSET G
3494# submonoid_element |- !g h. h << g ==> !x. x IN H ==> x IN G
3495# submonoid_id |- !g h. h << g ==> (#i = #e)
3496 submonoid_exp |- !g h. h << g ==> !x. x IN H ==> !n. h.exp x n = x ** n
3497 submonoid_homomorphism |- !g h. h << g ==> Monoid h /\ Monoid g /\ submonoid h g
3498 submonoid_order |- !g h. h << g ==> !x. x IN H ==> (order h x = ord x)
3499 submonoid_alt |- !g. Monoid g ==> !h. h << g <=> H SUBSET G /\
3500 (!x y. x IN H /\ y IN H ==> h.op x y IN H) /\
3501 h.id IN H /\ (h.op = $* ) /\ (h.id = #e)
3502
3503 Submonoid Theorems:
3504 submonoid_reflexive |- !g. Monoid g ==> g << g
3505 submonoid_antisymmetric |- !g h. h << g /\ g << h ==> (h = g)
3506 submonoid_transitive |- !g h k. k << h /\ h << g ==> k << g
3507 submonoid_monoid |- !g h. h << g ==> Monoid h
3508
3509 Submonoid Intersection:
3510 monoid_intersect_def |- !g h. g mINTER h = <|carrier := G INTER H; op := $*; id := #e|>
3511 monoid_intersect_property |- !g h. ((g mINTER h).carrier = G INTER H) /\
3512 ((g mINTER h).op = $* ) /\ ((g mINTER h).id = #e)
3513 monoid_intersect_element |- !g h x. x IN (g mINTER h).carrier ==> x IN G /\ x IN H
3514 monoid_intersect_id |- !g h. (g mINTER h).id = #e
3515
3516 submonoid_intersect_property |- !g h k. h << g /\ k << g ==>
3517 ((h mINTER k).carrier = H INTER K) /\
3518 (!x y. x IN H INTER K /\ y IN H INTER K ==>
3519 ((h mINTER k).op x y = x * y)) /\ ((h mINTER k).id = #e)
3520 submonoid_intersect_monoid |- !g h k. h << g /\ k << g ==> Monoid (h mINTER k)
3521 submonoid_intersect_submonoid |- !g h k. h << g /\ k << g ==> (h mINTER k) << g
3522
3523 Submonoid Big Intersection:
3524 submonoid_big_intersect_def |- !g. smbINTER g =
3525 <|carrier := BIGINTER (IMAGE (\h. H) {h | h << g}); op := $*; id := #e|>
3526 submonoid_big_intersect_property |- !g.
3527 ((smbINTER g).carrier = BIGINTER (IMAGE (\h. H) {h | h << g})) /\
3528 (!x y. x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> ((smbINTER g).op x y = x * y)) /\
3529 ((smbINTER g).id = #e)
3530 submonoid_big_intersect_element |- !g x. x IN (smbINTER g).carrier <=> !h. h << g ==> x IN H
3531 submonoid_big_intersect_op_element |- !g x y. x IN (smbINTER g).carrier /\
3532 y IN (smbINTER g).carrier ==>
3533 (smbINTER g).op x y IN (smbINTER g).carrier
3534 submonoid_big_intersect_has_id |- !g. (smbINTER g).id IN (smbINTER g).carrier
3535 submonoid_big_intersect_subset |- !g. Monoid g ==> (smbINTER g).carrier SUBSET G
3536 submonoid_big_intersect_monoid |- !g. Monoid g ==> Monoid (smbINTER g)
3537 submonoid_big_intersect_submonoid |- !g. Monoid g ==> smbINTER g << g
3538*)
3539
3540(* ------------------------------------------------------------------------- *)
3541(* Submonoid of a Monoid *)
3542(* ------------------------------------------------------------------------- *)
3543
3544(* Use K to denote k.carrier *)
3545Overload K[local] = ``(k:'a monoid).carrier``
3546
3547(* Use o to denote h.op *)
3548Overload o[local] = ``(h:'a monoid).op``
3549
3550(* Use #i to denote h.id *)
3551Overload "#i"[local] = ``(h:'a monoid).id``
3552
3553(* A Submonoid is a subset of a monoid that's a monoid itself, keeping op, id. *)
3554Definition Submonoid_def:
3555 Submonoid (h:'a monoid) (g:'a monoid) <=>
3556 Monoid h /\ Monoid g /\
3557 H SUBSET G /\ ($o = $* ) /\ (#i = #e)
3558End
3559
3560(* Overload Submonoid *)
3561Overload "<<" = ``Submonoid``
3562val _ = set_fixity "<<" (Infix(NONASSOC, 450)); (* same as relation *)
3563
3564(* Note: The requirement $o = $* is stronger than the following:
3565val _ = overload_on ("<<", ``\(h g):'a monoid. Monoid g /\ Monoid h /\ submonoid h g``);
3566Since submonoid h g is based on MonoidHomo I g h, which only gives
3567!x y. x IN H /\ y IN H ==> (h.op x y = x * y))
3568
3569This is not enough to satisfy monoid_component_equality,
3570hence cannot prove: h << g /\ g << h ==> h = g
3571*)
3572
3573(*
3574val submonoid_property = save_thm(
3575 "submonoid_property",
3576 Submonoid_def
3577 |> SPEC_ALL
3578 |> REWRITE_RULE [ASSUME ``h:'a monoid << g``]
3579 |> CONJUNCTS
3580 |> (fn thl => List.take(thl, 2) @ List.drop(thl, 3))
3581 |> LIST_CONJ
3582 |> DISCH_ALL
3583 |> Q.GEN `h` |> Q.GEN `g`);
3584val submonoid_property = |- !g h. h << g ==> Monoid h /\ Monoid g /\ ($o = $* ) /\ (#i = #e)
3585*)
3586
3587(* Theorem: properties of submonoid *)
3588(* Proof: Assume h << g, then derive all consequences of definition. *)
3589Theorem submonoid_property:
3590 !(g:'a monoid) h. h << g ==> Monoid h /\ Monoid g /\ H SUBSET G /\
3591 (!x y. x IN H /\ y IN H ==> (x o y = x * y)) /\ (#i = #e)
3592Proof
3593 rw_tac std_ss[Submonoid_def]
3594QED
3595
3596(* Theorem: h << g ==> H SUBSET G *)
3597(* Proof: by Submonoid_def *)
3598Theorem submonoid_carrier_subset:
3599 !(g:'a monoid) h. Submonoid h g ==> H SUBSET G
3600Proof
3601 rw[Submonoid_def]
3602QED
3603
3604(* Theorem: elements in submonoid are also in monoid. *)
3605(* Proof: Since h << g ==> H SUBSET G by Submonoid_def. *)
3606Theorem submonoid_element[simp]:
3607 !(g:'a monoid) h. h << g ==> !x. x IN H ==> x IN G
3608Proof
3609 rw_tac std_ss[Submonoid_def, SUBSET_DEF]
3610QED
3611
3612
3613(* Theorem: h << g ==> (h.op = $* ) *)
3614(* Proof: by Subgroup_def *)
3615Theorem submonoid_op:
3616 !(g:'a monoid) h. h << g ==> (h.op = g.op)
3617Proof
3618 rw[Submonoid_def]
3619QED
3620
3621(* Theorem: h << g ==> #i = #e *)
3622(* Proof: by Submonoid_def. *)
3623Theorem submonoid_id[simp]:
3624 !(g:'a monoid) h. h << g ==> (#i = #e)
3625Proof
3626 rw_tac std_ss[Submonoid_def]
3627QED
3628
3629
3630(* Theorem: h << g ==> !x. x IN H ==> !n. h.exp x n = x ** n *)
3631(* Proof: by induction on n.
3632 Base: h.exp x 0 = x ** 0
3633 LHS = h.exp x 0
3634 = h.id by monoid_exp_0
3635 = #e by submonoid_id
3636 = x ** 0 by monoid_exp_0
3637 = RHS
3638 Step: h.exp x n = x ** n ==> h.exp x (SUC n) = x ** SUC n
3639 LHS = h.exp x (SUC n)
3640 = h.op x (h.exp x n) by monoid_exp_SUC
3641 = x * (h.exp x n) by submonoid_property
3642 = x * x ** n by induction hypothesis
3643 = x ** SUC n by monoid_exp_SUC
3644 = RHS
3645*)
3646Theorem submonoid_exp:
3647 !(g:'a monoid) h. h << g ==> !x. x IN H ==> !n. h.exp x n = x ** n
3648Proof
3649 rpt strip_tac >>
3650 Induct_on `n` >-
3651 rw[] >>
3652 `h.exp x (SUC n) = h.op x (h.exp x n)` by rw_tac std_ss[monoid_exp_SUC] >>
3653 `_ = x * (h.exp x n)` by metis_tac[submonoid_property, monoid_exp_element] >>
3654 `_ = x * (x ** n)` by rw[] >>
3655 `_ = x ** (SUC n)` by rw_tac std_ss[monoid_exp_SUC] >>
3656 rw[]
3657QED
3658
3659(* Theorem: A submonoid h of g implies identity is a homomorphism from h to g.
3660 or h << g ==> Monoid h /\ Monoid g /\ submonoid h g *)
3661(* Proof:
3662 h << g ==> Monoid h /\ Monoid g by Submonoid_def
3663 together with
3664 H SUBSET G /\ ($o = $* ) /\ (#i = #e) by Submonoid_def
3665 ==> !x. x IN H ==> x IN G /\
3666 !x y. x IN H /\ y IN H ==> (x o y = x * y) /\
3667 #i = #e by SUBSET_DEF
3668 ==> MonoidHomo I h g by MonoidHomo_def, f = I.
3669 ==> submonoid h g by submonoid_def
3670*)
3671Theorem submonoid_homomorphism:
3672 !(g:'a monoid) h. h << g ==> Monoid h /\ Monoid g /\ submonoid h g
3673Proof
3674 rw_tac std_ss[Submonoid_def, submonoid_def, MonoidHomo_def, SUBSET_DEF]
3675QED
3676
3677(* original:
3678g `!(g:'a monoid) h. h << g = Monoid h /\ Monoid g /\ submonoid h g`;
3679e (rw_tac std_ss[Submonoid_def, submonoid_def, MonoidHomo_def, SUBSET_DEF, EQ_IMP_THM]);
3680
3681The only-if part (<==) cannot be proved:
3682Note Submonoid_def uses h.op = g.op,
3683but submonoid_def uses homomorphism I, and so cannot show this for any x y.
3684*)
3685
3686(* Theorem: h << g ==> !x. x IN H ==> (order h x = ord x) *)
3687(* Proof:
3688 Note Monoid g /\ Monoid h /\ submonoid h g by submonoid_homomorphism, h << g
3689 Thus !x. x IN H ==> (order h x = ord x) by submonoid_order_eqn
3690*)
3691Theorem submonoid_order:
3692 !(g:'a monoid) h. h << g ==> !x. x IN H ==> (order h x = ord x)
3693Proof
3694 metis_tac[submonoid_homomorphism, submonoid_order_eqn]
3695QED
3696
3697(* Theorem: Monoid g ==> !h. Submonoid h g <=>
3698 H SUBSET G /\ (!x y. x IN H /\ y IN H ==> h.op x y IN H) /\ (h.id IN H) /\ (h.op = $* ) /\ (h.id = #e) *)
3699(* Proof:
3700 By Submonoid_def, EQ_IMP_THM, this is to show:
3701 (1) x IN H /\ y IN H ==> x * y IN H, true by monoid_op_element
3702 (2) #e IN H, true by monoid_id_element
3703 (3) Monoid h
3704 By Monoid_def, this is to show:
3705 (1) x IN H /\ y IN H /\ z IN H
3706 ==> x * y * z = x * (y * z), true by monoid_assoc, SUBSET_DEF
3707 (2) x IN H ==> #e * x = x, true by monoid_lid, SUBSET_DEF
3708 (3) x IN H ==> x * #e = x, true by monoid_rid, SUBSET_DEF
3709*)
3710Theorem submonoid_alt:
3711 !g:'a monoid. Monoid g ==> !h. Submonoid h g <=>
3712 H SUBSET G /\ (* subset *)
3713 (!x y. x IN H /\ y IN H ==> h.op x y IN H) /\ (* closure *)
3714 (h.id IN H) /\ (* has identity *)
3715 (h.op = g.op ) /\ (h.id = #e)
3716Proof
3717 rw_tac std_ss[Submonoid_def, EQ_IMP_THM] >-
3718 metis_tac[monoid_op_element] >-
3719 metis_tac[monoid_id_element] >>
3720 rw_tac std_ss[Monoid_def] >-
3721 fs[monoid_assoc, SUBSET_DEF] >-
3722 fs[monoid_lid, SUBSET_DEF] >>
3723 fs[monoid_rid, SUBSET_DEF]
3724QED
3725
3726(* ------------------------------------------------------------------------- *)
3727(* Submonoid Theorems *)
3728(* ------------------------------------------------------------------------- *)
3729
3730(* Theorem: Monoid g ==> g << g *)
3731(* Proof: by Submonoid_def, SUBSET_REFL *)
3732Theorem submonoid_reflexive:
3733 !g:'a monoid. Monoid g ==> g << g
3734Proof
3735 rw_tac std_ss[Submonoid_def, SUBSET_REFL]
3736QED
3737
3738val monoid_component_equality = DB.fetch "-" "monoid_component_equality";
3739
3740(* Theorem: h << g /\ g << h ==> (h = g) *)
3741(* Proof:
3742 Since h << g ==> Monoid h /\ Monoid g /\ H SUBSET G /\ ($o = $* ) /\ (#i = #e) by Submonoid_def
3743 and g << h ==> Monoid g /\ Monoid h /\ G SUBSET H /\ ($* = $o) /\ (#e = #i) by Submonoid_def
3744 Now, H SUBSET G /\ G SUBSET H ==> H = G by SUBSET_ANTISYM
3745 Hence h = g by monoid_component_equality
3746*)
3747Theorem submonoid_antisymmetric:
3748 !g h:'a monoid. h << g /\ g << h ==> (h = g)
3749Proof
3750 rw_tac std_ss[Submonoid_def] >>
3751 full_simp_tac bool_ss[monoid_component_equality, SUBSET_ANTISYM]
3752QED
3753
3754(* Theorem: k << h /\ h << g ==> k << g *)
3755(* Proof: by Submonoid_def and SUBSET_TRANS *)
3756Theorem submonoid_transitive:
3757 !g h k:'a monoid. k << h /\ h << g ==> k << g
3758Proof
3759 rw_tac std_ss[Submonoid_def] >>
3760 metis_tac[SUBSET_TRANS]
3761QED
3762
3763(* Theorem: h << g ==> Monoid h *)
3764(* Proof: by Submonoid_def. *)
3765Theorem submonoid_monoid:
3766 !g h:'a monoid. h << g ==> Monoid h
3767Proof
3768 rw[Submonoid_def]
3769QED
3770
3771(* ------------------------------------------------------------------------- *)
3772(* Submonoid Intersection *)
3773(* ------------------------------------------------------------------------- *)
3774
3775(* Define intersection of monoids *)
3776Definition monoid_intersect_def:
3777 monoid_intersect (g:'a monoid) (h:'a monoid) =
3778 <| carrier := G INTER H;
3779 op := $*; (* g.op *)
3780 id := #e (* g.id *)
3781 |>
3782End
3783
3784Overload mINTER = ``monoid_intersect``
3785val _ = set_fixity "mINTER" (Infix(NONASSOC, 450)); (* same as relation *)
3786(*
3787> monoid_intersect_def;
3788val it = |- !g h. g mINTER h = <|carrier := G INTER H; op := $*; id := #e|>: thm
3789*)
3790
3791(* Theorem: ((g mINTER h).carrier = G INTER H) /\
3792 ((g mINTER h).op = $* ) /\ ((g mINTER h).id = #e) *)
3793(* Proof: by monoid_intersect_def *)
3794Theorem monoid_intersect_property:
3795 !g h:'a monoid. ((g mINTER h).carrier = G INTER H) /\
3796 ((g mINTER h).op = $* ) /\ ((g mINTER h).id = #e)
3797Proof
3798 rw[monoid_intersect_def]
3799QED
3800
3801(* Theorem: !x. x IN (g mINTER h).carrier ==> x IN G /\ x IN H *)
3802(* Proof:
3803 x IN (g mINTER h).carrier
3804 ==> x IN G INTER H by monoid_intersect_def
3805 ==> x IN G and x IN H by IN_INTER
3806*)
3807Theorem monoid_intersect_element:
3808 !g h:'a monoid. !x. x IN (g mINTER h).carrier ==> x IN G /\ x IN H
3809Proof
3810 rw[monoid_intersect_def, IN_INTER]
3811QED
3812
3813(* Theorem: (g mINTER h).id = #e *)
3814(* Proof: by monoid_intersect_def. *)
3815Theorem monoid_intersect_id:
3816 !g h:'a monoid. (g mINTER h).id = #e
3817Proof
3818 rw[monoid_intersect_def]
3819QED
3820
3821(* Theorem: h << g /\ k << g ==>
3822 ((h mINTER k).carrier = H INTER K) /\
3823 (!x y. x IN H INTER K /\ y IN H INTER K ==> ((h mINTER k).op x y = x * y)) /\
3824 ((h mINTER k).id = #e) *)
3825(* Proof:
3826 (h mINTER k).carrier = H INTER K by monoid_intersect_def
3827 Hence x IN (h mINTER k).carrier ==> x IN H /\ x IN K by IN_INTER
3828 and y IN (h mINTER k).carrier ==> y IN H /\ y IN K by IN_INTER
3829 so (h mINTER k).op x y = x o y by monoid_intersect_def
3830 = x * y by submonoid_property
3831 and (h mINTER k).id = #i by monoid_intersect_def
3832 = #e by submonoid_property
3833*)
3834Theorem submonoid_intersect_property:
3835 !g h k:'a monoid. h << g /\ k << g ==>
3836 ((h mINTER k).carrier = H INTER K) /\
3837 (!x y. x IN H INTER K /\ y IN H INTER K ==> ((h mINTER k).op x y = x * y)) /\
3838 ((h mINTER k).id = #e)
3839Proof
3840 rw[monoid_intersect_def, submonoid_property]
3841QED
3842
3843(* Theorem: h << g /\ k << g ==> Monoid (h mINTER k) *)
3844(* Proof:
3845 By definitions, this is to show:
3846 (1) x IN H INTER K /\ y IN H INTER K ==> x o y IN H INTER K
3847 x IN H INTER K ==> x IN H /\ x IN K by IN_INTER
3848 y IN H INTER K ==> y IN H /\ y IN K by IN_INTER
3849 x IN H /\ y IN H ==> x o y IN H by monoid_op_element
3850 x IN K /\ y IN K ==> k.op x y IN K by monoid_op_element
3851 x o y = x * y by submonoid_property
3852 k.op x y = x * y by submonoid_property
3853 Hence x o y IN H INTER K by IN_INTER
3854 (2) x IN H INTER K /\ y IN H INTER K /\ z IN H INTER K ==> (x o y) o z = x o y o z
3855 x IN H INTER K ==> x IN H by IN_INTER
3856 y IN H INTER K ==> y IN H by IN_INTER
3857 z IN H INTER K ==> z IN H by IN_INTER
3858 x IN H /\ y IN H ==> x o y IN H by monoid_op_element
3859 y IN H /\ z IN H ==> y o z IN H by monoid_op_element
3860 x, y, z IN H ==> x, y, z IN G by submonoid_element
3861 LHS = (x o y) o z
3862 = (x o y) * z by submonoid_property
3863 = (x * y) * z by submonoid_property
3864 = x * (y * z) by monoid_assoc
3865 = x * (y o z) by submonoid_property
3866 = x o (y o z) = RHS by submonoid_property
3867 (3) #i IN H INTER K
3868 #i IN H and #i = #e by monoid_id_element, submonoid_id
3869 k.id IN K and k.id = #e by monoid_id_element, submonoid_id
3870 Hence #e = #i IN H INTER K by IN_INTER
3871 (4) x IN H INTER K ==> #i o x = x
3872 x IN H INTER K ==> x IN H by IN_INTER
3873 ==> x IN G by submonoid_element
3874 #i IN H and #i = #e by monoid_id_element, submonoid_id
3875 #i o x
3876 = #i * x by submonoid_property
3877 = #e * x by submonoid_id
3878 = x by monoid_id
3879 (5) x IN H INTER K ==> x o #i = x
3880 x IN H INTER K ==> x IN H by IN_INTER
3881 ==> x IN G by submonoid_element
3882 #i IN H and #i = #e by monoid_id_element, submonoid_id
3883 x o #i
3884 = x * #i by submonoid_property
3885 = x * #e by submonoid_id
3886 = x by monoid_id
3887*)
3888Theorem submonoid_intersect_monoid:
3889 !g h k:'a monoid. h << g /\ k << g ==> Monoid (h mINTER k)
3890Proof
3891 rpt strip_tac >>
3892 `Monoid h /\ Monoid k /\ Monoid g` by metis_tac[submonoid_property] >>
3893 rw_tac std_ss[Monoid_def, monoid_intersect_def] >| [
3894 `x IN H /\ x IN K /\ y IN H /\ y IN K` by metis_tac[IN_INTER] >>
3895 `x o y IN H /\ (x o y = x * y)` by metis_tac[submonoid_property, monoid_op_element] >>
3896 `k.op x y IN K /\ (k.op x y = x * y)` by metis_tac[submonoid_property, monoid_op_element] >>
3897 metis_tac[IN_INTER],
3898 `x IN H /\ y IN H /\ z IN H` by metis_tac[IN_INTER] >>
3899 `x IN G /\ y IN G /\ z IN G` by metis_tac[submonoid_element] >>
3900 `x o y IN H /\ y o z IN H` by metis_tac[monoid_op_element] >>
3901 `(x o y) o z = (x * y) * z` by metis_tac[submonoid_property] >>
3902 `x o (y o z) = x * (y * z)` by metis_tac[submonoid_property] >>
3903 rw[monoid_assoc],
3904 metis_tac[IN_INTER, submonoid_id, monoid_id_element],
3905 metis_tac[submonoid_property, monoid_id, submonoid_element, IN_INTER, monoid_id_element],
3906 metis_tac[submonoid_property, monoid_id, submonoid_element, IN_INTER, monoid_id_element]
3907 ]
3908QED
3909
3910(* Theorem: h << g /\ k << g ==> (h mINTER k) << g *)
3911(* Proof:
3912 By Submonoid_def, this is to show:
3913 (1) Monoid (h mINTER k), true by submonoid_intersect_monoid
3914 (2) (h mINTER k).carrier SUBSET G
3915 Since (h mINTER k).carrier = H INTER K by submonoid_intersect_property
3916 and (H INTER K) SUBSET H by INTER_SUBSET
3917 and h << g ==> H SUBSET G by submonoid_property
3918 Hence (h mINTER k).carrier SUBSET G by SUBSET_TRANS
3919 (3) (h mINTER k).op = $*
3920 (h mINTER k).op = $o by monoid_intersect_def
3921 = $* by Submonoid_def
3922 (4) (h mINTER k).id = #e
3923 (h mINTER k).id = #i by monoid_intersect_def
3924 = #e by Submonoid_def
3925*)
3926Theorem submonoid_intersect_submonoid:
3927 !g h k:'a monoid. h << g /\ k << g ==> (h mINTER k) << g
3928Proof
3929 rpt strip_tac >>
3930 `Monoid h /\ Monoid k /\ Monoid g` by metis_tac[submonoid_property] >>
3931 rw[Submonoid_def] >| [
3932 metis_tac[submonoid_intersect_monoid],
3933 `(h mINTER k).carrier = H INTER K` by metis_tac[submonoid_intersect_property] >>
3934 `H SUBSET G` by rw[submonoid_property] >>
3935 metis_tac[INTER_SUBSET, SUBSET_TRANS],
3936 `(h mINTER k).op = $o` by rw[monoid_intersect_def] >>
3937 metis_tac[Submonoid_def],
3938 `(h mINTER k).id = #i` by rw[monoid_intersect_def] >>
3939 metis_tac[Submonoid_def]
3940 ]
3941QED
3942
3943(* ------------------------------------------------------------------------- *)
3944(* Submonoid Big Intersection *)
3945(* ------------------------------------------------------------------------- *)
3946
3947(* Define intersection of submonoids of a monoid *)
3948Definition submonoid_big_intersect_def:
3949 submonoid_big_intersect (g:'a monoid) =
3950 <| carrier := BIGINTER (IMAGE (\h. H) {h | h << g});
3951 op := $*; (* g.op *)
3952 id := #e (* g.id *)
3953 |>
3954End
3955
3956Overload smbINTER = ``submonoid_big_intersect``
3957(*
3958> submonoid_big_intersect_def;
3959val it = |- !g. smbINTER g =
3960 <|carrier := BIGINTER (IMAGE (\h. H) {h | h << g}); op := $*; id := #e|>: thm
3961*)
3962
3963(* Theorem: ((smbINTER g).carrier = BIGINTER (IMAGE (\h. H) {h | h << g})) /\
3964 (!x y. x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> ((smbINTER g).op x y = x * y)) /\
3965 ((smbINTER g).id = #e) *)
3966(* Proof: by submonoid_big_intersect_def. *)
3967Theorem submonoid_big_intersect_property:
3968 !g:'a monoid. ((smbINTER g).carrier = BIGINTER (IMAGE (\h. H) {h | h << g})) /\
3969 (!x y. x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> ((smbINTER g).op x y = x * y)) /\
3970 ((smbINTER g).id = #e)
3971Proof
3972 rw[submonoid_big_intersect_def]
3973QED
3974
3975(* Theorem: x IN (smbINTER g).carrier <=> (!h. h << g ==> x IN H) *)
3976(* Proof:
3977 x IN (smbINTER g).carrier
3978 <=> x IN BIGINTER (IMAGE (\h. H) {h | h << g}) by submonoid_big_intersect_def
3979 <=> !P. P IN (IMAGE (\h. H) {h | h << g}) ==> x IN P by IN_BIGINTER
3980 <=> !P. ?h. (P = H) /\ h IN {h | h << g}) ==> x IN P by IN_IMAGE
3981 <=> !P. ?h. (P = H) /\ h << g) ==> x IN P by GSPECIFICATION
3982 <=> !h. h << g ==> x IN H
3983*)
3984Theorem submonoid_big_intersect_element:
3985 !g:'a monoid. !x. x IN (smbINTER g).carrier <=> (!h. h << g ==> x IN H)
3986Proof
3987 rw[submonoid_big_intersect_def] >>
3988 metis_tac[]
3989QED
3990
3991(* Theorem: x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> (smbINTER g).op x y IN (smbINTER g).carrier *)
3992(* Proof:
3993 Since x IN (smbINTER g).carrier, !h. h << g ==> x IN H by submonoid_big_intersect_element
3994 also y IN (smbINTER g).carrier, !h. h << g ==> y IN H by submonoid_big_intersect_element
3995 Now !h. h << g ==> x o y IN H by Submonoid_def, monoid_op_element
3996 ==> x * y IN H by submonoid_property
3997 Now, (smbINTER g).op x y = x * y by submonoid_big_intersect_property
3998 Hence (smbINTER g).op x y IN (smbINTER g).carrier by submonoid_big_intersect_element
3999*)
4000Theorem submonoid_big_intersect_op_element:
4001 !g:'a monoid. !x y. x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==>
4002 (smbINTER g).op x y IN (smbINTER g).carrier
4003Proof
4004 rpt strip_tac >>
4005 `!h. h << g ==> x IN H /\ y IN H` by metis_tac[submonoid_big_intersect_element] >>
4006 `!h. h << g ==> x * y IN H` by metis_tac[Submonoid_def, monoid_op_element, submonoid_property] >>
4007 `(smbINTER g).op x y = x * y` by rw[submonoid_big_intersect_property] >>
4008 metis_tac[submonoid_big_intersect_element]
4009QED
4010
4011(* Theorem: (smbINTER g).id IN (smbINTER g).carrier *)
4012(* Proof:
4013 !h. h << g ==> #i = #e by submonoid_id
4014 !h. h << g ==> #i IN H by Submonoid_def, monoid_id_element
4015 Now (smbINTER g).id = #e by submonoid_big_intersect_property
4016 Hence !h. h << g ==> (smbINTER g).id IN H by above
4017 or (smbINTER g).id IN (smbINTER g).carrier by submonoid_big_intersect_element
4018*)
4019Theorem submonoid_big_intersect_has_id:
4020 !g:'a monoid. (smbINTER g).id IN (smbINTER g).carrier
4021Proof
4022 rpt strip_tac >>
4023 `!h. h << g ==> (#i = #e)` by rw[submonoid_id] >>
4024 `!h. h << g ==> #i IN H` by rw[Submonoid_def] >>
4025 `(smbINTER g).id = #e` by metis_tac[submonoid_big_intersect_property] >>
4026 metis_tac[submonoid_big_intersect_element]
4027QED
4028
4029(* Theorem: Monoid g ==> (smbINTER g).carrier SUBSET G *)
4030(* Proof:
4031 By submonoid_big_intersect_def, this is to show:
4032 Monoid g ==> BIGINTER (IMAGE (\h. H) {h | h << g}) SUBSET G
4033 Let P = IMAGE (\h. H) {h | h << g}.
4034 Since g << g by submonoid_reflexive
4035 so G IN P by IN_IMAGE, definition of P.
4036 Thus P <> {} by MEMBER_NOT_EMPTY.
4037 Now h << g ==> H SUBSET G by submonoid_property
4038 Hence P SUBSET G by BIGINTER_SUBSET
4039*)
4040Theorem submonoid_big_intersect_subset:
4041 !g:'a monoid. Monoid g ==> (smbINTER g).carrier SUBSET G
4042Proof
4043 rw[submonoid_big_intersect_def] >>
4044 qabbrev_tac `P = IMAGE (\h. H) {h | h << g}` >>
4045 (`!x. x IN P <=> ?h. (H = x) /\ h << g` by (rw[Abbr`P`] >> metis_tac[])) >>
4046 `g << g` by rw[submonoid_reflexive] >>
4047 `P <> {}` by metis_tac[MEMBER_NOT_EMPTY] >>
4048 `!h:'a monoid. h << g ==> H SUBSET G` by rw[submonoid_property] >>
4049 metis_tac[BIGINTER_SUBSET]
4050QED
4051
4052(* Theorem: Monoid g ==> Monoid (smbINTER g) *)
4053(* Proof:
4054 Monoid g ==> (smbINTER g).carrier SUBSET G by submonoid_big_intersect_subset
4055 By Monoid_def, this is to show:
4056 (1) x IN (smbINTER g).carrier /\ y IN (smbINTER g).carrier ==> (smbINTER g).op x y IN (smbINTER g).carrier
4057 True by submonoid_big_intersect_op_element.
4058 (2) (smbINTER g).op ((smbINTER g).op x y) z = (smbINTER g).op x ((smbINTER g).op y z)
4059 Since (smbINTER g).op x y IN (smbINTER g).carrier by submonoid_big_intersect_op_element
4060 and (smbINTER g).op y z IN (smbINTER g).carrier by submonoid_big_intersect_op_element
4061 So this is to show: (x * y) * z = x * (y * z) by submonoid_big_intersect_property
4062 Since x IN G, y IN G and z IN G by SUBSET_DEF
4063 This follows by monoid_assoc.
4064 (3) (smbINTER g).id IN (smbINTER g).carrier
4065 This is true by submonoid_big_intersect_has_id.
4066 (4) x IN (smbINTER g).carrier ==> (smbINTER g).op (smbINTER g).id x = x
4067 Since (smbINTER g).id IN (smbINTER g).carrier by submonoid_big_intersect_op_element
4068 and (smbINTER g).id = #e by submonoid_big_intersect_property
4069 also x IN G by SUBSET_DEF
4070 (smbINTER g).op (smbINTER g).id x
4071 = #e * x by submonoid_big_intersect_property
4072 = x by monoid_id
4073 (5) x IN (smbINTER g).carrier ==> (smbINTER g).op x (smbINTER g).id = x
4074 Since (smbINTER g).id IN (smbINTER g).carrier by submonoid_big_intersect_op_element
4075 and (smbINTER g).id = #e by submonoid_big_intersect_property
4076 also x IN G by SUBSET_DEF
4077 (smbINTER g).op x (smbINTER g).id
4078 = x * #e by submonoid_big_intersect_property
4079 = x by monoid_id
4080*)
4081Theorem submonoid_big_intersect_monoid:
4082 !g:'a monoid. Monoid g ==> Monoid (smbINTER g)
4083Proof
4084 rpt strip_tac >>
4085 `(smbINTER g).carrier SUBSET G` by rw[submonoid_big_intersect_subset] >>
4086 rw_tac std_ss[Monoid_def] >| [
4087 metis_tac[submonoid_big_intersect_op_element],
4088 `(smbINTER g).op x y IN (smbINTER g).carrier` by metis_tac[submonoid_big_intersect_op_element] >>
4089 `(smbINTER g).op y z IN (smbINTER g).carrier` by metis_tac[submonoid_big_intersect_op_element] >>
4090 `(x * y) * z = x * (y * z)` suffices_by rw[submonoid_big_intersect_property] >>
4091 `x IN G /\ y IN G /\ z IN G` by metis_tac[SUBSET_DEF] >>
4092 rw[monoid_assoc],
4093 metis_tac[submonoid_big_intersect_has_id],
4094 `(smbINTER g).id = #e` by rw[submonoid_big_intersect_property] >>
4095 `(smbINTER g).id IN (smbINTER g).carrier` by metis_tac[submonoid_big_intersect_has_id] >>
4096 `#e * x = x` suffices_by rw[submonoid_big_intersect_property] >>
4097 `x IN G` by metis_tac[SUBSET_DEF] >>
4098 rw[],
4099 `(smbINTER g).id = #e` by rw[submonoid_big_intersect_property] >>
4100 `(smbINTER g).id IN (smbINTER g).carrier` by metis_tac[submonoid_big_intersect_has_id] >>
4101 `x * #e = x` suffices_by rw[submonoid_big_intersect_property] >>
4102 `x IN G` by metis_tac[SUBSET_DEF] >>
4103 rw[]
4104 ]
4105QED
4106
4107(* Theorem: Monoid g ==> (smbINTER g) << g *)
4108(* Proof:
4109 By Submonoid_def, this is to show:
4110 (1) Monoid (smbINTER g)
4111 True by submonoid_big_intersect_monoid.
4112 (2) (smbINTER g).carrier SUBSET G
4113 True by submonoid_big_intersect_subset.
4114 (3) (smbINTER g).op = $*
4115 True by submonoid_big_intersect_def
4116 (4) (smbINTER g).id = #e
4117 True by submonoid_big_intersect_def
4118*)
4119Theorem submonoid_big_intersect_submonoid:
4120 !g:'a monoid. Monoid g ==> (smbINTER g) << g
4121Proof
4122 rw_tac std_ss[Submonoid_def] >| [
4123 rw[submonoid_big_intersect_monoid],
4124 rw[submonoid_big_intersect_subset],
4125 rw[submonoid_big_intersect_def],
4126 rw[submonoid_big_intersect_def]
4127 ]
4128QED
4129
4130(* ------------------------------------------------------------------------- *)
4131(* Monoid Instances Documentation *)
4132(* ------------------------------------------------------------------------- *)
4133(* Monoid Data type:
4134 The generic symbol for monoid data is g.
4135 g.carrier = Carrier set of monoid
4136 g.op = Binary operation of monoid
4137 g.id = Identity element of monoid
4138*)
4139(* Definitions and Theorems (# are exported, ! in computeLib):
4140
4141 The trivial monoid:
4142 trivial_monoid_def |- !e. trivial_monoid e = <|carrier := {e}; id := e; op := (\x y. e)|>
4143 trivial_monoid |- !e. FiniteAbelianMonoid (trivial_monoid e)
4144
4145 The monoid of addition modulo n:
4146 plus_mod_def |- !n. plus_mod n =
4147 <|carrier := count n;
4148 id := 0;
4149 op := (\i j. (i + j) MOD n)|>
4150 plus_mod_property |- !n. ((plus_mod n).carrier = count n) /\
4151 ((plus_mod n).op = (\i j. (i + j) MOD n)) /\
4152 ((plus_mod n).id = 0) /\
4153 (!x. x IN (plus_mod n).carrier ==> x < n) /\
4154 FINITE (plus_mod n).carrier /\
4155 (CARD (plus_mod n).carrier = n)
4156 plus_mod_exp |- !n. 0 < n ==> !x k. (plus_mod n).exp x k = (k * x) MOD n
4157 plus_mod_monoid |- !n. 0 < n ==> Monoid (plus_mod n)
4158 plus_mod_abelian_monoid |- !n. 0 < n ==> AbelianMonoid (plus_mod n)
4159 plus_mod_finite |- !n. FINITE (plus_mod n).carrier
4160 plus_mod_finite_monoid |- !n. 0 < n ==> FiniteMonoid (plus_mod n)
4161 plus_mod_finite_abelian_monoid |- !n. 0 < n ==> FiniteAbelianMonoid (plus_mod n)
4162
4163 The monoid of multiplication modulo n:
4164 times_mod_def |- !n. times_mod n =
4165 <|carrier := count n;
4166 id := if n = 1 then 0 else 1;
4167 op := (\i j. (i * j) MOD n)|>
4168! times_mod_eval |- !n. ((times_mod n).carrier = count n) /\
4169 (!x y. (times_mod n).op x y = (x * y) MOD n) /\
4170 ((times_mod n).id = if n = 1 then 0 else 1)
4171 times_mod_property |- !n. ((times_mod n).carrier = count n) /\
4172 ((times_mod n).op = (\i j. (i * j) MOD n)) /\
4173 ((times_mod n).id = if n = 1 then 0 else 1) /\
4174 (!x. x IN (times_mod n).carrier ==> x < n) /\
4175 FINITE (times_mod n).carrier /\
4176 (CARD (times_mod n).carrier = n)
4177 times_mod_exp |- !n. 0 < n ==> !x k. (times_mod n).exp x k = (x MOD n) ** k MOD n
4178 times_mod_monoid |- !n. 0 < n ==> Monoid (times_mod n)
4179 times_mod_abelian_monoid |- !n. 0 < n ==> AbelianMonoid (times_mod n)
4180 times_mod_finite |- !n. FINITE (times_mod n).carrier
4181 times_mod_finite_monoid |- !n. 0 < n ==> FiniteMonoid (times_mod n)
4182 times_mod_finite_abelian_monoid |- !n. 0 < n ==> FiniteAbelianMonoid (times_mod n)
4183
4184 The Monoid of List concatenation:
4185 lists_def |- lists = <|carrier := univ(:'a list); id := []; op := $++ |>
4186 lists_monoid |- Monoid lists
4187
4188 The Monoids from Set:
4189 set_inter_def |- set_inter = <|carrier := univ(:'a -> bool); id := univ(:'a); op := $INTER|>
4190 set_inter_monoid |- Monoid set_inter
4191 set_inter_abelian_monoid |- AbelianMonoid set_inter
4192 set_union_def |- set_union = <|carrier := univ(:'a -> bool); id := {}; op := $UNION|>
4193 set_union_monoid |- Monoid set_union
4194 set_union_abelian_monoid |- AbelianMonoid set_union
4195
4196 Addition of numbers form a Monoid:
4197 addition_monoid_def |- addition_monoid = <|carrier := univ(:num); op := $+; id := 0|>
4198 addition_monoid_property |- (addition_monoid.carrier = univ(:num)) /\
4199 (addition_monoid.op = $+) /\ (addition_monoid.id = 0)
4200 addition_monoid_abelian_monoid |- AbelianMonoid addition_monoid
4201 addition_monoid_monoid |- Monoid addition_monoid
4202
4203 Multiplication of numbers form a Monoid:
4204 multiplication_monoid_def |- multiplication_monoid = <|carrier := univ(:num); op := $*; id := 1|>
4205 multiplication_monoid_property |- (multiplication_monoid.carrier = univ(:num)) /\
4206 (multiplication_monoid.op = $* ) /\ (multiplication_monoid.id = 1)
4207 multiplication_monoid_abelian_monoid |- AbelianMonoid multiplication_monoid
4208 multiplication_monoid_monoid |- Monoid multiplication_monoid
4209
4210 Powers of a fixed base form a Monoid:
4211 power_monoid_def |- !b. power_monoid b =
4212 <|carrier := {b ** j | j IN univ(:num)}; op := $*; id := 1|>
4213 power_monoid_property |- !b. ((power_monoid b).carrier = {b ** j | j IN univ(:num)}) /\
4214 ((power_monoid b).op = $* ) /\ ((power_monoid b).id = 1)
4215 power_monoid_abelian_monoid |- !b. AbelianMonoid (power_monoid b)
4216 power_monoid_monoid |- !b. Monoid (power_monoid b)
4217
4218 Logarithm is an isomorphism:
4219 power_to_addition_homo |- !b. 1 < b ==> MonoidHomo (LOG b) (power_monoid b) addition_monoid
4220 power_to_addition_iso |- !b. 1 < b ==> MonoidIso (LOG b) (power_monoid b) addition_monoid
4221
4222
4223*)
4224(* ------------------------------------------------------------------------- *)
4225(* The trivial monoid. *)
4226(* ------------------------------------------------------------------------- *)
4227
4228(* The trivial monoid: {#e} *)
4229Definition trivial_monoid_def:
4230 trivial_monoid e :'a monoid =
4231 <| carrier := {e};
4232 id := e;
4233 op := (\x y. e)
4234 |>
4235End
4236
4237(*
4238- type_of ``trivial_monoid e``;
4239> val it = ``:'a monoid`` : hol_type
4240> EVAL ``(trivial_monoid T).id``;
4241val it = |- (trivial_monoid T).id <=> T: thm
4242> EVAL ``(trivial_monoid 8).id``;
4243val it = |- (trivial_monoid 8).id = 8: thm
4244*)
4245
4246(* Theorem: {e} is indeed a monoid *)
4247(* Proof: check by definition. *)
4248Theorem trivial_monoid:
4249 !e. FiniteAbelianMonoid (trivial_monoid e)
4250Proof
4251 rw_tac std_ss[FiniteAbelianMonoid_def, AbelianMonoid_def, Monoid_def, trivial_monoid_def, IN_SING, FINITE_SING]
4252QED
4253
4254(* ------------------------------------------------------------------------- *)
4255(* The monoid of addition modulo n. *)
4256(* ------------------------------------------------------------------------- *)
4257
4258(* Additive Modulo Monoid *)
4259Definition plus_mod_def:
4260 plus_mod n :num monoid =
4261 <| carrier := count n;
4262 id := 0;
4263 op := (\i j. (i + j) MOD n)
4264 |>
4265End
4266(* This monoid should be upgraded to add_mod, the additive group of ZN ring later. *)
4267
4268(*
4269- type_of ``plus_mod n``;
4270> val it = ``:num monoid`` : hol_type
4271> EVAL ``(plus_mod 7).op 5 6``;
4272val it = |- (plus_mod 7).op 5 6 = 4: thm
4273*)
4274
4275(* Theorem: properties of (plus_mod n) *)
4276(* Proof: by plus_mod_def. *)
4277Theorem plus_mod_property:
4278 !n. ((plus_mod n).carrier = count n) /\
4279 ((plus_mod n).op = (\i j. (i + j) MOD n)) /\
4280 ((plus_mod n).id = 0) /\
4281 (!x. x IN (plus_mod n).carrier ==> x < n) /\
4282 (FINITE (plus_mod n).carrier) /\
4283 (CARD (plus_mod n).carrier = n)
4284Proof
4285 rw[plus_mod_def]
4286QED
4287
4288(* Theorem: 0 < n ==> !x k. (plus_mod n).exp x k = (k * x) MOD n *)
4289(* Proof:
4290 Expanding by definitions, this is to show:
4291 FUNPOW (\j. (x + j) MOD n) k 0 = (k * x) MOD n
4292 Applyy induction on k.
4293 Base case: FUNPOW (\j. (x + j) MOD n) 0 0 = (0 * x) MOD n
4294 LHS = FUNPOW (\j. (x + j) MOD n) 0 0
4295 = 0 by FUNPOW_0
4296 = 0 MOD n by ZERO_MOD, 0 < n
4297 = (0 * x) MOD n by MULT
4298 = RHS
4299 Step case: FUNPOW (\j. (x + j) MOD n) (SUC k) 0 = (SUC k * x) MOD n
4300 LHS = FUNPOW (\j. (x + j) MOD n) (SUC k) 0
4301 = (x + FUNPOW (\j. (x + j) MOD n) k 0) MOD n by FUNPOW_SUC
4302 = (x + (k * x) MOD n) MOD n by induction hypothesis
4303 = (x MOD n + (k * x) MOD n) MOD n by MOD_PLUS, MOD_MOD
4304 = (x + k * x) MOD n by MOD_PLUS, MOD_MOD
4305 = (k * x + x) MOD n by ADD_COMM
4306 = ((SUC k) * x) MOD n by MULT
4307 = RHS
4308*)
4309Theorem plus_mod_exp:
4310 !n. 0 < n ==> !x k. (plus_mod n).exp x k = (k * x) MOD n
4311Proof
4312 rw_tac std_ss[plus_mod_def, monoid_exp_def] >>
4313 Induct_on `k` >-
4314 rw[] >>
4315 rw_tac std_ss[FUNPOW_SUC] >>
4316 metis_tac[MULT, ADD_COMM, MOD_PLUS, MOD_MOD]
4317QED
4318
4319(* Theorem: Additive Modulo n is a monoid. *)
4320(* Proof: check group definitions, use MOD_ADD_ASSOC.
4321*)
4322Theorem plus_mod_monoid:
4323 !n. 0 < n ==> Monoid (plus_mod n)
4324Proof
4325 rw_tac std_ss[plus_mod_def, Monoid_def, count_def, GSPECIFICATION, MOD_ADD_ASSOC]
4326QED
4327
4328(* Theorem: Additive Modulo n is an Abelian monoid. *)
4329(* Proof: by plus_mod_monoid and ADD_COMM. *)
4330Theorem plus_mod_abelian_monoid:
4331 !n. 0 < n ==> AbelianMonoid (plus_mod n)
4332Proof
4333 rw[plus_mod_monoid, plus_mod_def, AbelianMonoid_def, ADD_COMM]
4334QED
4335
4336(* Theorem: Additive Modulo n carrier is FINITE. *)
4337(* Proof: by FINITE_COUNT. *)
4338Theorem plus_mod_finite:
4339 !n. FINITE (plus_mod n).carrier
4340Proof
4341 rw[plus_mod_def]
4342QED
4343
4344(* Theorem: Additive Modulo n is a FINITE monoid. *)
4345(* Proof: by plus_mod_monoid and plus_mod_finite. *)
4346Theorem plus_mod_finite_monoid:
4347 !n. 0 < n ==> FiniteMonoid (plus_mod n)
4348Proof
4349 rw[FiniteMonoid_def, plus_mod_monoid, plus_mod_finite]
4350QED
4351
4352(* Theorem: Additive Modulo n is a FINITE Abelian monoid. *)
4353(* Proof: by plus_mod_abelian_monoid and plus_mod_finite. *)
4354Theorem plus_mod_finite_abelian_monoid:
4355 !n. 0 < n ==> FiniteAbelianMonoid (plus_mod n)
4356Proof
4357 rw[FiniteAbelianMonoid_def, plus_mod_abelian_monoid, plus_mod_finite]
4358QED
4359
4360(* ------------------------------------------------------------------------- *)
4361(* The monoid of multiplication modulo n. *)
4362(* ------------------------------------------------------------------------- *)
4363
4364(* Multiplicative Modulo Monoid *)
4365Definition times_mod_def[nocompute]:
4366 times_mod n :num monoid =
4367 <| carrier := count n;
4368 id := if n = 1 then 0 else 1;
4369 op := (\i j. (i * j) MOD n)
4370 |>
4371End
4372(* This monoid is taken as the multiplicative monoid of ZN ring later. *)
4373(* Use of zDefine to avoid incorporating into computeLib, by default. *)
4374(* Evaluation is given later in times_mod_eval. *)
4375
4376(*
4377- type_of ``times_mod n``;
4378> val it = ``:num monoid`` : hol_type
4379> EVAL ``(times_mod 7).op 5 6``;
4380val it = |- (times_mod 7).op 5 6 = 2: thm
4381*)
4382
4383(* Theorem: times_mod evaluation. *)
4384(* Proof: by times_mod_def. *)
4385Theorem times_mod_eval[compute]:
4386 !n. ((times_mod n).carrier = count n) /\
4387 (!x y. (times_mod n).op x y = (x * y) MOD n) /\
4388 ((times_mod n).id = if n = 1 then 0 else 1)
4389Proof
4390 rw_tac std_ss[times_mod_def]
4391QED
4392
4393(* Theorem: properties of (times_mod n) *)
4394(* Proof: by times_mod_def. *)
4395Theorem times_mod_property:
4396 !n. ((times_mod n).carrier = count n) /\
4397 ((times_mod n).op = (\i j. (i * j) MOD n)) /\
4398 ((times_mod n).id = if n = 1 then 0 else 1) /\
4399 (!x. x IN (times_mod n).carrier ==> x < n) /\
4400 (FINITE (times_mod n).carrier) /\
4401 (CARD (times_mod n).carrier = n)
4402Proof
4403 rw[times_mod_def]
4404QED
4405
4406(* Theorem: 0 < n ==> !x k. (times_mod n).exp x k = ((x MOD n) ** k) MOD n *)
4407(* Proof:
4408 Expanding by definitions, this is to show:
4409 (1) n = 1 ==> FUNPOW (\j. (x * j) MOD n) k 0 = (x MOD n) ** k MOD n
4410 or to show: FUNPOW (\j. 0) k 0 = 0 by MOD_1
4411 Note (\j. 0) = K 0 by FUN_EQ_THM
4412 and FUNPOW (K 0) k 0 = 0 by FUNPOW_K
4413 (2) n <> 1 ==> FUNPOW (\j. (x * j) MOD n) k 1 = (x MOD n) ** k MOD n
4414 Note 1 < n by 0 < n /\ n <> 1
4415 By induction on k.
4416 Base: FUNPOW (\j. (x * j) MOD n) 0 1 = (x MOD n) ** 0 MOD n
4417 FUNPOW (\j. (x * j) MOD n) 0 1
4418 = 1 by FUNPOW_0
4419 = 1 MOD n by ONE_MOD, 1 < n
4420 = ((x MOD n) ** 0) MOD n by EXP
4421 Step: FUNPOW (\j. (x * j) MOD n) (SUC k) 1 = (x MOD n) ** SUC k MOD n
4422 FUNPOW (\j. (x * j) MOD n) (SUC k) 1
4423 = (x * FUNPOW (\j. (x * j) MOD n) k 1) MOD n by FUNPOW_SUC
4424 = (x * (x MOD n) ** k MOD n) MOD n by induction hypothesis
4425 = ((x MOD n) * (x MOD n) ** k MOD n) MOD n by MOD_TIMES2, MOD_MOD, 0 < n
4426 = ((x MOD n) * (x MOD n) ** k) MOD n by MOD_TIMES2, MOD_MOD, 0 < n
4427 = ((x MOD n) ** SUC k) MOD n by EXP
4428*)
4429Theorem times_mod_exp:
4430 !n. 0 < n ==> !x k. (times_mod n).exp x k = ((x MOD n) ** k) MOD n
4431Proof
4432 rw_tac std_ss[times_mod_def, monoid_exp_def] >| [
4433 `(\j. 0) = K 0` by rw[FUN_EQ_THM] >>
4434 metis_tac[FUNPOW_K],
4435 `1 < n` by decide_tac >>
4436 Induct_on `k` >-
4437 rw[EXP, ONE_MOD] >>
4438 `FUNPOW (\j. (x * j) MOD n) (SUC k) 1 = (x * FUNPOW (\j. (x * j) MOD n) k 1) MOD n` by rw_tac std_ss[FUNPOW_SUC] >>
4439 metis_tac[EXP, MOD_TIMES2, MOD_MOD]
4440 ]
4441QED
4442
4443(* Theorem: For n > 0, Multiplication Modulo n is a monoid. *)
4444(* Proof: check monoid definitions, use MOD_MULT_ASSOC. *)
4445Theorem times_mod_monoid:
4446 !n. 0 < n ==> Monoid (times_mod n)
4447Proof
4448 rw_tac std_ss[Monoid_def, times_mod_def, count_def, GSPECIFICATION] >| [
4449 rw[MOD_MULT_ASSOC],
4450 decide_tac
4451 ]
4452QED
4453
4454(* Theorem: For n > 0, Multiplication Modulo n is an Abelian monoid. *)
4455(* Proof: by times_mod_monoid and MULT_COMM. *)
4456Theorem times_mod_abelian_monoid:
4457 !n. 0 < n ==> AbelianMonoid (times_mod n)
4458Proof
4459 rw[AbelianMonoid_def, times_mod_monoid, times_mod_def, MULT_COMM]
4460QED
4461
4462(* Theorem: Multiplication Modulo n carrier is FINITE. *)
4463(* Proof: by FINITE_COUNT. *)
4464Theorem times_mod_finite:
4465 !n. FINITE (times_mod n).carrier
4466Proof
4467 rw[times_mod_def]
4468QED
4469
4470(* Theorem: For n > 0, Multiplication Modulo n is a FINITE monoid. *)
4471(* Proof: by times_mod_monoid and times_mod_finite. *)
4472Theorem times_mod_finite_monoid:
4473 !n. 0 < n ==> FiniteMonoid (times_mod n)
4474Proof
4475 rw[times_mod_monoid, times_mod_finite, FiniteMonoid_def]
4476QED
4477
4478(* Theorem: For n > 0, Multiplication Modulo n is a FINITE Abelian monoid. *)
4479(* Proof: by times_mod_abelian_monoid and times_mod_finite. *)
4480Theorem times_mod_finite_abelian_monoid:
4481 !n. 0 < n ==> FiniteAbelianMonoid (times_mod n)
4482Proof
4483 rw[times_mod_abelian_monoid, times_mod_finite, FiniteAbelianMonoid_def, AbelianMonoid_def]
4484QED
4485
4486(*
4487
4488- EVAL ``(plus_mod 5).op 3 4``;
4489> val it = |- (plus_mod 5).op 3 4 = 2 : thm
4490- EVAL ``(plus_mod 5).id``;
4491> val it = |- (plus_mod 5).id = 0 : thm
4492- EVAL ``(times_mod 5).op 2 3``;
4493> val it = |- (times_mod 5).op 2 3 = 1 : thm
4494- EVAL ``(times_mod 5).op 5 3``;
4495> val it = |- (times_mod 5).id = 1 : thm
4496*)
4497
4498(* ------------------------------------------------------------------------- *)
4499(* The Monoid of List concatenation. *)
4500(* ------------------------------------------------------------------------- *)
4501
4502Definition lists_def:
4503 lists :'a list monoid =
4504 <| carrier := UNIV;
4505 id := [];
4506 op := list$APPEND
4507 |>
4508End
4509
4510(*
4511> EVAL ``lists.op [1;2;3] [4;5]``;
4512val it = |- lists.op [1; 2; 3] [4; 5] = [1; 2; 3; 4; 5]: thm
4513*)
4514
4515(* Theorem: Lists form a Monoid *)
4516(* Proof: check definition. *)
4517Theorem lists_monoid:
4518 Monoid lists
4519Proof
4520 rw_tac std_ss[Monoid_def, lists_def, IN_UNIV, GSPECIFICATION, APPEND, APPEND_NIL, APPEND_ASSOC]
4521QED
4522
4523(* after a long while ...
4524
4525val lists_monoid = store_thm(
4526 "lists_monoid",
4527 ``Monoid lists``,
4528 rw[Monoid_def, lists_def]);
4529*)
4530
4531(* ------------------------------------------------------------------------- *)
4532(* The Monoids from Set. *)
4533(* ------------------------------------------------------------------------- *)
4534
4535(* The Monoid of set intersection *)
4536Definition set_inter_def:
4537 set_inter = <| carrier := UNIV;
4538 id := UNIV;
4539 op := (INTER) |>
4540End
4541
4542(*
4543> EVAL ``set_inter.op {1;4;5;6} {5;6;8;9}``;
4544val it = |- set_inter.op {1; 4; 5; 6} {5; 6; 8; 9} = {5; 6}: thm
4545*)
4546
4547(* Theorem: set_inter is a Monoid. *)
4548(* Proof: check definitions. *)
4549Theorem set_inter_monoid[simp]:
4550 Monoid set_inter
4551Proof
4552 rw[Monoid_def, set_inter_def, INTER_ASSOC]
4553QED
4554
4555
4556(* Theorem: set_inter is an abelian Monoid. *)
4557(* Proof: check definitions. *)
4558Theorem set_inter_abelian_monoid[simp]:
4559 AbelianMonoid set_inter
4560Proof
4561 rw[AbelianMonoid_def, set_inter_def, INTER_COMM]
4562QED
4563
4564
4565(* The Monoid of set union *)
4566Definition set_union_def:
4567 set_union = <| carrier := UNIV;
4568 id := EMPTY;
4569 op := (UNION) |>
4570End
4571
4572(*
4573> EVAL ``set_union.op {1;4;5;6} {5;6;8;9}``;
4574val it = |- set_union.op {1; 4; 5; 6} {5; 6; 8; 9} = {1; 4; 5; 6; 8; 9}: thm
4575*)
4576
4577(* Theorem: set_union is a Monoid. *)
4578(* Proof: check definitions. *)
4579Theorem set_union_monoid[simp]:
4580 Monoid set_union
4581Proof
4582 rw[Monoid_def, set_union_def, UNION_ASSOC]
4583QED
4584
4585
4586(* Theorem: set_union is an abelian Monoid. *)
4587(* Proof: check definitions. *)
4588Theorem set_union_abelian_monoid[simp]:
4589 AbelianMonoid set_union
4590Proof
4591 rw[AbelianMonoid_def, set_union_def, UNION_COMM]
4592QED
4593
4594
4595(* ------------------------------------------------------------------------- *)
4596(* Addition of numbers form a Monoid *)
4597(* ------------------------------------------------------------------------- *)
4598
4599(* Define the number addition monoid *)
4600Definition addition_monoid_def:
4601 addition_monoid =
4602 <| carrier := univ(:num);
4603 op := $+;
4604 id := 0;
4605 |>
4606End
4607
4608(*
4609> EVAL ``addition_monoid.op 5 6``;
4610val it = |- addition_monoid.op 5 6 = 11: thm
4611*)
4612
4613(* Theorem: properties of addition_monoid *)
4614(* Proof: by addition_monoid_def *)
4615Theorem addition_monoid_property:
4616 (addition_monoid.carrier = univ(:num)) /\
4617 (addition_monoid.op = $+ ) /\
4618 (addition_monoid.id = 0)
4619Proof
4620 rw[addition_monoid_def]
4621QED
4622
4623(* Theorem: AbelianMonoid (addition_monoid) *)
4624(* Proof:
4625 By AbelianMonoid_def, Monoid_def, addition_monoid_def, this is to show:
4626 (1) ?z. z = x + y. Take z = x + y.
4627 (2) x + y + z = x + (y + z), true by ADD_ASSOC
4628 (3) x + 0 = x /\ 0 + x = x, true by ADD, ADD_0
4629 (4) x + y = y + x, true by ADD_COMM
4630*)
4631Theorem addition_monoid_abelian_monoid:
4632 AbelianMonoid (addition_monoid)
4633Proof
4634 rw_tac std_ss[AbelianMonoid_def, Monoid_def, addition_monoid_def, GSPECIFICATION, IN_UNIV] >>
4635 simp[]
4636QED
4637
4638(* Theorem: Monoid (addition_monoid) *)
4639(* Proof: by addition_monoid_abelian_monoid, AbelianMonoid_def *)
4640Theorem addition_monoid_monoid:
4641 Monoid (addition_monoid)
4642Proof
4643 metis_tac[addition_monoid_abelian_monoid, AbelianMonoid_def]
4644QED
4645
4646(* ------------------------------------------------------------------------- *)
4647(* Multiplication of numbers form a Monoid *)
4648(* ------------------------------------------------------------------------- *)
4649
4650(* Define the number multiplication monoid *)
4651Definition multiplication_monoid_def:
4652 multiplication_monoid =
4653 <| carrier := univ(:num);
4654 op := $*;
4655 id := 1;
4656 |>
4657End
4658
4659(*
4660> EVAL ``multiplication_monoid.op 5 6``;
4661val it = |- multiplication_monoid.op 5 6 = 30: thm
4662*)
4663
4664(* Theorem: properties of multiplication_monoid *)
4665(* Proof: by multiplication_monoid_def *)
4666Theorem multiplication_monoid_property:
4667 (multiplication_monoid.carrier = univ(:num)) /\
4668 (multiplication_monoid.op = $* ) /\
4669 (multiplication_monoid.id = 1)
4670Proof
4671 rw[multiplication_monoid_def]
4672QED
4673
4674(* Theorem: AbelianMonoid (multiplication_monoid) *)
4675(* Proof:
4676 By AbelianMonoid_def, Monoid_def, multiplication_monoid_def, this is to show:
4677 (1) ?z. z = x * y. Take z = x * y.
4678 (2) x * y * z = x * (y * z), true by MULT_ASSOC
4679 (3) x * 1 = x /\ 1 * x = x, true by MULT, MULT_1
4680 (4) x * y = y * x, true by MULT_COMM
4681*)
4682Theorem multiplication_monoid_abelian_monoid:
4683 AbelianMonoid (multiplication_monoid)
4684Proof
4685 rw_tac std_ss[AbelianMonoid_def, Monoid_def, multiplication_monoid_def, GSPECIFICATION, IN_UNIV] >-
4686 simp[] >>
4687 simp[]
4688QED
4689
4690(* Theorem: Monoid (multiplication_monoid) *)
4691(* Proof: by multiplication_monoid_abelian_monoid, AbelianMonoid_def *)
4692Theorem multiplication_monoid_monoid:
4693 Monoid (multiplication_monoid)
4694Proof
4695 metis_tac[multiplication_monoid_abelian_monoid, AbelianMonoid_def]
4696QED
4697
4698(* ------------------------------------------------------------------------- *)
4699(* Powers of a fixed base form a Monoid *)
4700(* ------------------------------------------------------------------------- *)
4701
4702(* Define the power monoid *)
4703Definition power_monoid_def:
4704 power_monoid (b:num) =
4705 <| carrier := {b ** j | j IN univ(:num)};
4706 op := $*;
4707 id := 1;
4708 |>
4709End
4710
4711(*
4712> EVAL ``(power_monoid 2).op (2 ** 3) (2 ** 4)``;
4713val it = |- (power_monoid 2).op (2 ** 3) (2 ** 4) = 128: thm
4714*)
4715
4716(* Theorem: properties of power monoid *)
4717(* Proof: by power_monoid_def *)
4718Theorem power_monoid_property:
4719 !b. ((power_monoid b).carrier = {b ** j | j IN univ(:num)}) /\
4720 ((power_monoid b).op = $* ) /\
4721 ((power_monoid b).id = 1)
4722Proof
4723 rw[power_monoid_def]
4724QED
4725
4726
4727(* Theorem: AbelianMonoid (power_monoid b) *)
4728(* Proof:
4729 By AbelianMonoid_def, Monoid_def, power_monoid_def, this is to show:
4730 (1) ?j''. b ** j * b ** j' = b ** j''
4731 Take j'' = j + j', true by EXP_ADD
4732 (2) b ** j * b ** j' * b ** j'' = b ** j * (b ** j' * b ** j'')
4733 True by EXP_ADD, ADD_ASSOC
4734 (3) ?j. b ** j = 1
4735 or ?j. (b = 1) \/ (j = 0), true by j = 0.
4736 (4) b ** j * b ** j' = b ** j' * b ** j
4737 True by EXP_ADD, ADD_COMM
4738*)
4739Theorem power_monoid_abelian_monoid:
4740 !b. AbelianMonoid (power_monoid b)
4741Proof
4742 rw_tac std_ss[AbelianMonoid_def, Monoid_def, power_monoid_def, GSPECIFICATION, IN_UNIV] >-
4743 metis_tac[EXP_ADD] >-
4744 rw[EXP_ADD] >-
4745 metis_tac[] >>
4746 rw[EXP_ADD]
4747QED
4748
4749(* Theorem: Monoid (power_monoid b) *)
4750(* Proof: by power_monoid_abelian_monoid, AbelianMonoid_def *)
4751Theorem power_monoid_monoid:
4752 !b. Monoid (power_monoid b)
4753Proof
4754 metis_tac[power_monoid_abelian_monoid, AbelianMonoid_def]
4755QED
4756
4757(* ------------------------------------------------------------------------- *)
4758(* Logarithm is an isomorphism from Power Monoid to Addition Monoid *)
4759(* ------------------------------------------------------------------------- *)
4760
4761(* Theorem: 1 < b ==> MonoidHomo (LOG b) (power_monoid b) (addition_monoid) *)
4762(* Proof:
4763 By MonoidHomo_def, power_monoid_def, addition_monoid_def, this is to show:
4764 (1) LOG b (b ** j * b ** j') = LOG b (b ** j) + LOG b (b ** j')
4765 LOG b (b ** j * b ** j')
4766 = LOG b (b ** (j + j')) by EXP_ADD
4767 = j + j' by LOG_EXACT_EXP
4768 = LOG b (b ** j) + LOG b (b ** j') by LOG_EXACT_EXP
4769 (2) LOG b 1 = 0, true by LOG_1
4770*)
4771Theorem power_to_addition_homo:
4772 !b. 1 < b ==> MonoidHomo (LOG b) (power_monoid b) (addition_monoid)
4773Proof
4774 rw[MonoidHomo_def, power_monoid_def, addition_monoid_def] >-
4775 rw[LOG_EXACT_EXP, GSYM EXP_ADD] >>
4776 rw[LOG_1]
4777QED
4778
4779(* Theorem: 1 < b ==> MonoidIso (LOG b) (power_monoid b) (addition_monoid) *)
4780(* Proof:
4781 By MonoidIso_def, this is to show:
4782 (1) MonoidHomo (LOG b) (power_monoid b) addition_monoid
4783 This is true by power_to_addition_homo
4784 (2) BIJ (LOG b) (power_monoid b).carrier addition_monoid.carrier
4785 By BIJ_DEF, this is to show:
4786 (1) INJ (LOG b) {b ** j | j IN univ(:num)} univ(:num)
4787 By INJ_DEF, this is to show:
4788 LOG b (b ** j) = LOG b (b ** j') ==> b ** j = b ** j'
4789 LOG b (b ** j) = LOG b (b ** j')
4790 ==> j = j' by LOG_EXACT_EXP
4791 ==> b ** j = b ** j'
4792 (2) SURJ (LOG b) {b ** j | j IN univ(:num)} univ(:num)
4793 By SURJ_DEF, this is to show:
4794 ?y. (?j. y = b ** j) /\ (LOG b y = x)
4795 Let j = x, y = b ** x, then true by LOG_EXACT_EXP
4796*)
4797Theorem power_to_addition_iso:
4798 !b. 1 < b ==> MonoidIso (LOG b) (power_monoid b) (addition_monoid)
4799Proof
4800 rw[MonoidIso_def] >-
4801 rw[power_to_addition_homo] >>
4802 rw_tac std_ss[BIJ_DEF, power_monoid_def, addition_monoid_def] >| [
4803 rw[INJ_DEF] >>
4804 rfs[LOG_EXACT_EXP],
4805 rw[SURJ_DEF] >>
4806 metis_tac[LOG_EXACT_EXP]
4807 ]
4808QED
4809
4810(* ------------------------------------------------------------------------- *)
4811(* Theory about folding a monoid (or group) operation over a bag of elements *)
4812(* ------------------------------------------------------------------------- *)
4813
4814Overload GITBAG = ``\(g:'a monoid) s b. ITBAG g.op s b``;
4815
4816Theorem GITBAG_THM =
4817 ITBAG_THM |> CONV_RULE SWAP_FORALL_CONV
4818 |> INST_TYPE [beta |-> alpha] |> Q.SPEC`(g:'a monoid).op`
4819 |> GEN_ALL
4820
4821Theorem GITBAG_EMPTY[simp]:
4822 !g a. GITBAG g {||} a = a
4823Proof
4824 rw[ITBAG_EMPTY]
4825QED
4826
4827Theorem GITBAG_INSERT:
4828 !b. FINITE_BAG b ==>
4829 !g x a. GITBAG g (BAG_INSERT x b) a =
4830 GITBAG g (BAG_REST (BAG_INSERT x b))
4831 (g.op (BAG_CHOICE (BAG_INSERT x b)) a)
4832Proof
4833 rw[ITBAG_INSERT]
4834QED
4835
4836Theorem SUBSET_COMMUTING_ITBAG_INSERT:
4837 !f b t.
4838 SET_OF_BAG b SUBSET t /\ closure_comm_assoc_fun f t /\ FINITE_BAG b ==>
4839 !x a::t. ITBAG f (BAG_INSERT x b) a = ITBAG f b (f x a)
4840Proof
4841 simp[RES_FORALL_THM]
4842 \\ rpt gen_tac \\ strip_tac
4843 \\ completeInduct_on `BAG_CARD b`
4844 \\ rw[]
4845 \\ simp[ITBAG_INSERT, BAG_REST_DEF, EL_BAG]
4846 \\ qmatch_goalsub_abbrev_tac`{|c|}`
4847 \\ `BAG_IN c (BAG_INSERT x b)` by PROVE_TAC[BAG_CHOICE_DEF, BAG_INSERT_NOT_EMPTY]
4848 \\ fs[BAG_IN_BAG_INSERT]
4849 \\ `?b0. b = BAG_INSERT c b0` by PROVE_TAC [BAG_IN_BAG_DELETE, BAG_DELETE]
4850 \\ `BAG_DIFF (BAG_INSERT x b) {| c |} = BAG_INSERT x b0`
4851 by SRW_TAC [][BAG_INSERT_commutes]
4852 \\ pop_assum SUBST_ALL_TAC
4853 \\ first_x_assum(qspec_then`BAG_CARD b0`mp_tac)
4854 \\ `FINITE_BAG b0` by FULL_SIMP_TAC (srw_ss()) []
4855 \\ impl_keep_tac >- SRW_TAC [numSimps.ARITH_ss][BAG_CARD_THM]
4856 \\ disch_then(qspec_then`b0`mp_tac)
4857 \\ impl_tac >- simp[]
4858 \\ impl_tac >- fs[SUBSET_DEF]
4859 \\ impl_tac >- simp[]
4860 \\ strip_tac
4861 \\ first_assum(qspec_then`x`mp_tac)
4862 \\ first_x_assum(qspec_then`c`mp_tac)
4863 \\ impl_keep_tac >- fs[SUBSET_DEF]
4864 \\ disch_then(qspec_then`f x a`mp_tac)
4865 \\ impl_keep_tac >- metis_tac[closure_comm_assoc_fun_def]
4866 \\ strip_tac
4867 \\ impl_tac >- simp[]
4868 \\ disch_then(qspec_then`f c a`mp_tac)
4869 \\ impl_keep_tac >- metis_tac[closure_comm_assoc_fun_def]
4870 \\ disch_then SUBST1_TAC
4871 \\ simp[]
4872 \\ metis_tac[closure_comm_assoc_fun_def]
4873QED
4874
4875Theorem COMMUTING_GITBAG_INSERT:
4876 !g b. AbelianMonoid g /\ FINITE_BAG b /\ SET_OF_BAG b SUBSET G ==>
4877 !x a::(G). GITBAG g (BAG_INSERT x b) a = GITBAG g b (g.op x a)
4878Proof
4879 rpt strip_tac
4880 \\ irule SUBSET_COMMUTING_ITBAG_INSERT
4881 \\ metis_tac[abelian_monoid_op_closure_comm_assoc_fun]
4882QED
4883
4884Theorem GITBAG_INSERT_THM =
4885 SIMP_RULE(srw_ss())[RES_FORALL_THM, PULL_FORALL, AND_IMP_INTRO]
4886 COMMUTING_GITBAG_INSERT
4887
4888Theorem GITBAG_UNION:
4889 !g. AbelianMonoid g ==>
4890 !b1. FINITE_BAG b1 ==> !b2. FINITE_BAG b2 /\ SET_OF_BAG b1 SUBSET G
4891 /\ SET_OF_BAG b2 SUBSET G ==>
4892 !a. a IN G ==> GITBAG g (BAG_UNION b1 b2) a = GITBAG g b2 (GITBAG g b1 a)
4893Proof
4894 gen_tac \\ strip_tac
4895 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
4896 \\ rw[]
4897 \\ simp[BAG_UNION_INSERT]
4898 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
4899 \\ gs[SUBSET_DEF]
4900 \\ simp[GSYM CONJ_ASSOC]
4901 \\ conj_tac >- metis_tac[]
4902 \\ first_x_assum irule
4903 \\ simp[]
4904 \\ fs[AbelianMonoid_def]
4905QED
4906
4907Theorem GITBAG_in_carrier:
4908 !g. AbelianMonoid g ==>
4909 !b. FINITE_BAG b ==> !a. SET_OF_BAG b SUBSET G /\ a IN G ==> GITBAG g b a IN G
4910Proof
4911 ntac 2 strip_tac
4912 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
4913 \\ simp[]
4914 \\ rpt strip_tac
4915 \\ drule COMMUTING_GITBAG_INSERT
4916 \\ disch_then (qspec_then`b`mp_tac)
4917 \\ fs[SUBSET_DEF]
4918 \\ simp[RES_FORALL_THM, PULL_FORALL]
4919 \\ strip_tac
4920 \\ last_x_assum irule
4921 \\ metis_tac[monoid_op_element, AbelianMonoid_def]
4922QED
4923
4924Overload GBAG = ``\(g:'a monoid) b. GITBAG g b g.id``;
4925
4926Theorem GBAG_in_carrier:
4927 !g b. AbelianMonoid g /\ FINITE_BAG b /\ SET_OF_BAG b SUBSET G ==> GBAG g b IN G
4928Proof
4929 rw[]
4930 \\ irule GITBAG_in_carrier
4931 \\ metis_tac[AbelianMonoid_def, monoid_id_element]
4932QED
4933
4934Theorem GITBAG_GBAG:
4935 !g. AbelianMonoid g ==>
4936 !b. FINITE_BAG b ==> !a. a IN g.carrier /\ SET_OF_BAG b SUBSET g.carrier ==>
4937 GITBAG g b a = g.op a (GITBAG g b g.id)
4938Proof
4939 ntac 2 strip_tac
4940 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
4941 \\ rw[] >- fs[AbelianMonoid_def]
4942 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
4943 \\ simp[]
4944 \\ conj_asm1_tac >- fs[SUBSET_DEF, AbelianMonoid_def]
4945 \\ irule EQ_TRANS
4946 \\ qexists_tac`g.op (g.op e a) (GBAG g b)`
4947 \\ conj_tac >- (
4948 first_x_assum irule
4949 \\ metis_tac[AbelianMonoid_def, monoid_op_element] )
4950 \\ first_x_assum(qspec_then`e`mp_tac)
4951 \\ simp[]
4952 \\ `g.op e (#e) = e` by metis_tac[AbelianMonoid_def, monoid_id]
4953 \\ pop_assum SUBST1_TAC
4954 \\ disch_then SUBST1_TAC
4955 \\ fs[AbelianMonoid_def]
4956 \\ irule monoid_assoc
4957 \\ simp[]
4958 \\ irule GBAG_in_carrier
4959 \\ simp[AbelianMonoid_def]
4960QED
4961
4962Theorem GBAG_UNION:
4963 AbelianMonoid g /\ FINITE_BAG b1 /\ FINITE_BAG b2 /\
4964 SET_OF_BAG b1 SUBSET g.carrier /\ SET_OF_BAG b2 SUBSET g.carrier ==>
4965 GBAG g (BAG_UNION b1 b2) = g.op (GBAG g b1) (GBAG g b2)
4966Proof
4967 rpt strip_tac
4968 \\ DEP_REWRITE_TAC[GITBAG_UNION]
4969 \\ simp[]
4970 \\ conj_tac >- fs[AbelianMonoid_def]
4971 \\ DEP_ONCE_REWRITE_TAC[GITBAG_GBAG]
4972 \\ simp[]
4973 \\ irule GBAG_in_carrier
4974 \\ simp[]
4975QED
4976
4977Theorem GITBAG_BAG_IMAGE_op:
4978 !g. AbelianMonoid g ==>
4979 !b. FINITE_BAG b ==>
4980 !p q a. IMAGE p (SET_OF_BAG b) SUBSET g.carrier /\
4981 IMAGE q (SET_OF_BAG b) SUBSET g.carrier /\ a IN g.carrier ==>
4982 GITBAG g (BAG_IMAGE (\x. g.op (p x) (q x)) b) a =
4983 g.op (GITBAG g (BAG_IMAGE p b) a) (GBAG g (BAG_IMAGE q b))
4984Proof
4985 ntac 2 strip_tac
4986 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
4987 \\ rw[] >- fs[AbelianMonoid_def]
4988 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
4989 \\ conj_asm1_tac
4990 >- (
4991 gs[SUBSET_DEF, PULL_EXISTS]
4992 \\ gs[AbelianMonoid_def] )
4993 \\ qmatch_goalsub_abbrev_tac`GITBAG g bb aa`
4994 \\ first_assum(qspecl_then[`p`,`q`,`aa`]mp_tac)
4995 \\ impl_tac >- (
4996 fs[SUBSET_DEF, PULL_EXISTS, Abbr`aa`]
4997 \\ fs[AbelianMonoid_def] )
4998 \\ simp[]
4999 \\ disch_then kall_tac
5000 \\ simp[Abbr`aa`]
5001 \\ DEP_ONCE_REWRITE_TAC[GITBAG_GBAG]
5002 \\ conj_asm1_tac >- (
5003 fs[SUBSET_DEF, PULL_EXISTS]
5004 \\ fs[AbelianMonoid_def] )
5005 \\ irule EQ_SYM
5006 \\ DEP_ONCE_REWRITE_TAC[GITBAG_GBAG]
5007 \\ conj_asm1_tac >- fs[AbelianMonoid_def]
5008 \\ DEP_ONCE_REWRITE_TAC[GITBAG_GBAG |> SIMP_RULE(srw_ss())[PULL_FORALL,AND_IMP_INTRO]
5009 |> Q.SPECL[`g`,`b`,`g.op x y`]]
5010 \\ simp[]
5011 \\ fs[AbelianMonoid_def]
5012 \\ qmatch_goalsub_abbrev_tac`_ * _ * gp * ( _ * gq)`
5013 \\ `gp IN g.carrier /\ gq IN g.carrier`
5014 by (
5015 unabbrev_all_tac
5016 \\ conj_tac \\ irule GBAG_in_carrier
5017 \\ fs[AbelianMonoid_def] )
5018 \\ drule monoid_assoc
5019 \\ strip_tac \\ gs[]
5020QED
5021
5022Theorem IMP_GBAG_EQ_ID:
5023 AbelianMonoid g ==>
5024 !b. BAG_EVERY ((=) g.id) b ==> GBAG g b = g.id
5025Proof
5026 rw[]
5027 \\ `FINITE_BAG b`
5028 by (
5029 Cases_on`b = {||}` \\ simp[]
5030 \\ once_rewrite_tac[GSYM unibag_FINITE]
5031 \\ rewrite_tac[FINITE_BAG_OF_SET]
5032 \\ `SET_OF_BAG b = {g.id}`
5033 by (
5034 rw[SET_OF_BAG, FUN_EQ_THM]
5035 \\ fs[BAG_EVERY]
5036 \\ rw[EQ_IMP_THM]
5037 \\ Cases_on`b` \\ rw[] )
5038 \\ pop_assum SUBST1_TAC
5039 \\ simp[])
5040 \\ qpat_x_assum`BAG_EVERY _ _` mp_tac
5041 \\ pop_assum mp_tac
5042 \\ qid_spec_tac`b`
5043 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
5044 \\ rw[] \\ gs[]
5045 \\ drule COMMUTING_GITBAG_INSERT
5046 \\ disch_then drule
5047 \\ impl_keep_tac
5048 >- (
5049 fs[SUBSET_DEF, BAG_EVERY]
5050 \\ fs[AbelianMonoid_def]
5051 \\ metis_tac[monoid_id_element] )
5052 \\ simp[RES_FORALL_THM, PULL_FORALL, AND_IMP_INTRO]
5053 \\ disch_then(qspecl_then[`#e`,`#e`]mp_tac)
5054 \\ simp[]
5055 \\ metis_tac[monoid_id_element, monoid_id_id, AbelianMonoid_def]
5056QED
5057
5058Theorem GITBAG_CONG:
5059 !g. AbelianMonoid g ==>
5060 !b. FINITE_BAG b ==> !b' a a'. FINITE_BAG b' /\
5061 a IN g.carrier /\ SET_OF_BAG b SUBSET g.carrier /\ SET_OF_BAG b' SUBSET g.carrier
5062 /\ (!x. BAG_IN x (BAG_UNION b b') /\ x <> g.id ==> b x = b' x)
5063 ==>
5064 GITBAG g b a = GITBAG g b' a
5065Proof
5066 ntac 2 strip_tac
5067 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT \\ rw[]
5068 >- (
5069 fs[BAG_IN, BAG_INN, EMPTY_BAG]
5070 \\ DEP_ONCE_REWRITE_TAC[GITBAG_GBAG]
5071 \\ simp[]
5072 \\ irule EQ_TRANS
5073 \\ qexists_tac`g.op a g.id`
5074 \\ conj_tac >- fs[AbelianMonoid_def]
5075 \\ AP_TERM_TAC
5076 \\ irule EQ_SYM
5077 \\ irule IMP_GBAG_EQ_ID
5078 \\ simp[BAG_EVERY, BAG_IN, BAG_INN]
5079 \\ metis_tac[])
5080 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
5081 \\ simp[]
5082 \\ fs[SET_OF_BAG_INSERT]
5083 \\ Cases_on`e = g.id`
5084 >- (
5085 fs[AbelianMonoid_def]
5086 \\ first_x_assum irule
5087 \\ simp[]
5088 \\ fs[BAG_INSERT]
5089 \\ metis_tac[] )
5090 \\ `BAG_IN e b'`
5091 by (
5092 simp[BAG_IN, BAG_INN]
5093 \\ fs[BAG_INSERT]
5094 \\ first_x_assum(qspec_then`e`mp_tac)
5095 \\ simp[] )
5096 \\ drule BAG_DECOMPOSE
5097 \\ disch_then(qx_choose_then`b2`strip_assume_tac)
5098 \\ pop_assum SUBST_ALL_TAC
5099 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
5100 \\ simp[] \\ fs[SET_OF_BAG_INSERT]
5101 \\ first_x_assum irule \\ simp[]
5102 \\ fs[BAG_INSERT, AbelianMonoid_def]
5103 \\ qx_gen_tac`x`
5104 \\ disch_then assume_tac
5105 \\ first_x_assum(qspec_then`x`mp_tac)
5106 \\ impl_tac >- metis_tac[]
5107 \\ IF_CASES_TAC \\ simp[]
5108QED
5109
5110Theorem GITBAG_same_op:
5111 g1.op = g2.op ==>
5112 !b. FINITE_BAG b ==>
5113 !a. GITBAG g1 b a = GITBAG g2 b a
5114Proof
5115 strip_tac
5116 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
5117 \\ rw[GITBAG_THM]
5118QED
5119
5120Theorem GBAG_IMAGE_PARTITION:
5121 AbelianMonoid g /\ FINITE s ==>
5122 !b. FINITE_BAG b ==>
5123 IMAGE f (SET_OF_BAG b) SUBSET G /\
5124 (!x. BAG_IN x b ==> ?P. P IN s /\ P x) /\
5125 (!x P1 P2. BAG_IN x b /\ P1 IN s /\ P2 IN s /\ P1 x /\ P2 x ==> P1 = P2)
5126 ==>
5127 GBAG g (BAG_IMAGE (λP. GBAG g (BAG_IMAGE f (BAG_FILTER P b))) (BAG_OF_SET s)) =
5128 GBAG g (BAG_IMAGE f b)
5129Proof
5130 strip_tac
5131 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
5132 \\ simp[]
5133 \\ conj_tac
5134 >- (
5135 irule IMP_GBAG_EQ_ID
5136 \\ simp[BAG_EVERY]
5137 \\ rw[]
5138 \\ imp_res_tac BAG_IN_BAG_IMAGE_IMP
5139 \\ fs[] )
5140 \\ rpt strip_tac
5141 \\ fs[SET_OF_BAG_INSERT]
5142 \\ `?P. P IN s /\ P e` by metis_tac[]
5143 \\ `?s0. s = P INSERT s0 /\ P NOTIN s0` by metis_tac[DECOMPOSITION]
5144 \\ BasicProvers.VAR_EQ_TAC
5145 \\ simp[BAG_OF_SET_INSERT_NON_ELEMENT]
5146 \\ DEP_REWRITE_TAC[BAG_IMAGE_FINITE_INSERT]
5147 \\ qpat_x_assum`_ ==> _`mp_tac
5148 \\ impl_tac >- metis_tac[]
5149 \\ strip_tac
5150 \\ conj_tac >- metis_tac[FINITE_INSERT, FINITE_BAG_OF_SET]
5151 \\ qmatch_goalsub_abbrev_tac`BAG_IMAGE ff (BAG_OF_SET s0)`
5152 \\ `BAG_IMAGE ff (BAG_OF_SET s0) =
5153 BAG_IMAGE (\P. GBAG g (BAG_IMAGE f (BAG_FILTER P b))) (BAG_OF_SET s0)`
5154 by (
5155 irule BAG_IMAGE_CONG
5156 \\ simp[Abbr`ff`]
5157 \\ rw[]
5158 \\ metis_tac[IN_INSERT] )
5159 \\ simp[Abbr`ff`]
5160 \\ pop_assum kall_tac
5161 \\ rpt(first_x_assum(qspec_then`ARB`kall_tac))
5162 \\ pop_assum mp_tac
5163 \\ simp[BAG_OF_SET_INSERT_NON_ELEMENT]
5164 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
5165 \\ fs[AbelianMonoid_def]
5166 \\ conj_asm1_tac >- fs[SUBSET_DEF, PULL_EXISTS]
5167 \\ conj_asm1_tac >- (
5168 fs[SUBSET_DEF, PULL_EXISTS]
5169 \\ rw[] \\ irule GITBAG_in_carrier
5170 \\ fs[SUBSET_DEF, PULL_EXISTS, AbelianMonoid_def] )
5171 \\ simp[]
5172 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
5173 \\ simp[]
5174 \\ conj_asm1_tac
5175 >- (
5176 simp[AbelianMonoid_def]
5177 \\ irule GITBAG_in_carrier
5178 \\ simp[AbelianMonoid_def] )
5179 \\ simp[]
5180 \\ DEP_ONCE_REWRITE_TAC[GITBAG_GBAG] \\ simp[] \\ strip_tac
5181 \\ DEP_ONCE_REWRITE_TAC[GITBAG_GBAG] \\ simp[]
5182 \\ DEP_ONCE_REWRITE_TAC[GITBAG_GBAG] \\ simp[]
5183 \\ DEP_REWRITE_TAC[monoid_assoc]
5184 \\ simp[]
5185 \\ conj_tac >- ( irule GBAG_in_carrier \\ simp[] )
5186 \\ irule EQ_SYM
5187 \\ irule GITBAG_GBAG
5188 \\ simp[]
5189QED
5190
5191Theorem GBAG_PARTITION:
5192 AbelianMonoid g /\ FINITE s /\ FINITE_BAG b /\ SET_OF_BAG b SUBSET G /\
5193 (!x. BAG_IN x b ==> ?P. P IN s /\ P x) /\
5194 (!x P1 P2. BAG_IN x b /\ P1 IN s /\ P2 IN s /\ P1 x /\ P2 x ==> P1 = P2)
5195 ==>
5196 GBAG g (BAG_IMAGE (λP. GBAG g (BAG_FILTER P b)) (BAG_OF_SET s)) = GBAG g b
5197Proof
5198 strip_tac
5199 \\ `!P. FINITE_BAG (BAG_FILTER P b)` by metis_tac[FINITE_BAG_FILTER]
5200 \\ `GBAG g b = GBAG g (BAG_IMAGE I b)` by metis_tac[BAG_IMAGE_FINITE_I]
5201 \\ pop_assum SUBST1_TAC
5202 \\ `(λP. GBAG g (BAG_FILTER P b)) = λP. GBAG g (BAG_IMAGE I (BAG_FILTER P b))`
5203 by simp[FUN_EQ_THM]
5204 \\ pop_assum SUBST1_TAC
5205 \\ irule GBAG_IMAGE_PARTITION
5206 \\ simp[]
5207 \\ metis_tac[]
5208QED
5209
5210Theorem GBAG_IMAGE_FILTER:
5211 AbelianMonoid g ==>
5212 !b. FINITE_BAG b ==> IMAGE f (SET_OF_BAG b INTER P) SUBSET g.carrier ==>
5213 GBAG g (BAG_IMAGE f (BAG_FILTER P b)) =
5214 GBAG g (BAG_IMAGE (\x. if P x then f x else g.id) b)
5215Proof
5216 strip_tac
5217 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
5218 \\ rw[]
5219 \\ fs[SUBSET_DEF, PULL_EXISTS]
5220 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
5221 \\ simp[SUBSET_DEF, PULL_EXISTS]
5222 \\ conj_asm1_tac
5223 >- (
5224 rw[]
5225 \\ fs[AbelianMonoid_def]
5226 \\ metis_tac[IN_DEF] )
5227 \\ irule EQ_SYM
5228 \\ DEP_ONCE_REWRITE_TAC[GITBAG_GBAG]
5229 \\ simp[SUBSET_DEF, PULL_EXISTS]
5230 \\ fs[AbelianMonoid_def]
5231 \\ qmatch_goalsub_abbrev_tac`_ * gg`
5232 \\ `gg IN g.carrier`
5233 by (
5234 simp[Abbr`gg`]
5235 \\ irule GBAG_in_carrier
5236 \\ simp[AbelianMonoid_def, SUBSET_DEF, PULL_EXISTS] )
5237 \\ IF_CASES_TAC \\ gs[]
5238 \\ simp[Abbr`gg`]
5239 \\ irule EQ_SYM
5240 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
5241 \\ simp[PULL_EXISTS, SUBSET_DEF, AbelianMonoid_def]
5242 \\ conj_tac >- metis_tac[]
5243 \\ qpat_x_assum`_ = _`(assume_tac o SYM) \\ simp[]
5244 \\ irule GITBAG_GBAG
5245 \\ simp[SUBSET_DEF, PULL_EXISTS]
5246 \\ metis_tac[AbelianMonoid_def]
5247QED
5248
5249Theorem GBAG_INSERT:
5250 AbelianMonoid g /\ FINITE_BAG b /\ SET_OF_BAG b SUBSET g.carrier /\ x IN g.carrier ==>
5251 GBAG g (BAG_INSERT x b) = g.op x (GBAG g b)
5252Proof
5253 strip_tac
5254 \\ DEP_REWRITE_TAC[GITBAG_INSERT_THM]
5255 \\ simp[]
5256 \\ `Monoid g` by fs[AbelianMonoid_def] \\ simp[]
5257 \\ irule GITBAG_GBAG
5258 \\ simp[]
5259QED
5260
5261Theorem MonoidHomo_GBAG:
5262 AbelianMonoid g /\ AbelianMonoid h /\
5263 MonoidHomo f g h /\ FINITE_BAG b /\ SET_OF_BAG b SUBSET g.carrier ==>
5264 f (GBAG g b) = GBAG h (BAG_IMAGE f b)
5265Proof
5266 strip_tac
5267 \\ ntac 2 (pop_assum mp_tac)
5268 \\ qid_spec_tac`b`
5269 \\ ho_match_mp_tac STRONG_FINITE_BAG_INDUCT
5270 \\ simp[]
5271 \\ fs[MonoidHomo_def]
5272 \\ rpt strip_tac
5273 \\ DEP_REWRITE_TAC[GBAG_INSERT]
5274 \\ simp[]
5275 \\ fs[SUBSET_DEF, PULL_EXISTS]
5276 \\ `GBAG g b IN g.carrier` suffices_by metis_tac[]
5277 \\ irule GBAG_in_carrier
5278 \\ simp[SUBSET_DEF, PULL_EXISTS]
5279QED
5280
5281Theorem IMP_GBAG_EQ_EXP:
5282 AbelianMonoid g /\ x IN g.carrier /\ SET_OF_BAG b SUBSET {x} ==>
5283 GBAG g b = g.exp x (b x)
5284Proof
5285 Induct_on`b x` \\ rw[]
5286 >- (
5287 Cases_on`b = {||}` \\ simp[]
5288 \\ fs[SUBSET_DEF]
5289 \\ Cases_on`b` \\ fs[BAG_INSERT] )
5290 \\ `b = BAG_INSERT x (b - {|x|})`
5291 by (
5292 simp[BAG_EXTENSION]
5293 \\ simp[BAG_INN, BAG_INSERT, EMPTY_BAG, BAG_DIFF]
5294 \\ rw[] )
5295 \\ qmatch_asmsub_abbrev_tac`BAG_INSERT x b0`
5296 \\ fs[]
5297 \\ `b0 x = v` by fs[BAG_INSERT]
5298 \\ first_x_assum(qspecl_then[`b0`,`x`]mp_tac)
5299 \\ simp[]
5300 \\ impl_tac >- fs[SUBSET_DEF]
5301 \\ DEP_REWRITE_TAC[GBAG_INSERT]
5302 \\ simp[]
5303 \\ simp[BAG_INSERT]
5304 \\ rewrite_tac[GSYM arithmeticTheory.ADD1]
5305 \\ simp[]
5306 \\ DEP_REWRITE_TAC[GSYM FINITE_SET_OF_BAG]
5307 \\ `SET_OF_BAG b0 SUBSET {x}` by fs[SUBSET_DEF]
5308 \\ `FINITE {x}` by simp[]
5309 \\ reverse conj_tac >- fs[SUBSET_DEF]
5310 \\ metis_tac[SUBSET_FINITE]
5311QED
5312
5313(* ------------------------------------------------------------------------- *)