1(* ------------------------------------------------------------------------- *)
2(* Group Theory -- Iterated Product.                                         *)
3(* ------------------------------------------------------------------------- *)
4
5(*===========================================================================*)
6
7(* add all dependent libraries for script *)
8open HolKernel boolLib bossLib Parse;
9
10(* declare new theory at start *)
11val _ = new_theory "groupProduct";
12
13(* ------------------------------------------------------------------------- *)
14
15
16(* val _ = load "jcLib"; *)
17open jcLib;
18
19(* open dependent theories *)
20open pred_setTheory arithmeticTheory;
21
22(* Get dependent theories local *)
23(* val _ = load "groupTheory"; *)
24open groupTheory monoidTheory;
25open monoidOrderTheory;
26
27(* val _ = load "subgroupTheory"; *)
28open submonoidTheory;
29open subgroupTheory;
30
31(* Get dependent theories in lib *)
32(* (* val _ = load "helperSetTheory";  loaded by monoidTheory *) *)
33open helperSetTheory;
34
35(* Load dependent theories *)
36(* val _ = load "Satisfysimps"; *)
37(* used in coset_id_eq_subgroup: srw_tac[SatisfySimps.SATISFY_ss] *)
38
39
40(* ------------------------------------------------------------------------- *)
41(* Iterated Product Documentation                                            *)
42(* ------------------------------------------------------------------------- *)
43(* Overloading (# is temporary):
44   FUN_COMM op f  = !x y z. op (f x) (op (f y) z) = op (f y) (op (f x) z)
45#  GPI f s        = GROUP_IMAGE g f s
46#  gfun f         = group_fun g f
47*)
48(* Definitions and Theorems (# are exported):
49
50   Fermat's Little Theorem of Abelian Groups:
51   GPROD_SET_IMAGE            |- !g a. Group g /\ a IN G ==> (GPROD_SET g (a * G) = GPROD_SET g G)
52   GPROD_SET_REDUCTION_INSERT |- !g s. FiniteAbelianGroup g /\ s SUBSET G ==>
53                                 !a x::(G). x NOTIN s ==>
54                          (a * x * GPROD_SET g (a * (G DIFF (x INSERT s))) = GPROD_SET g (a * (G DIFF s)))
55   GPROD_SET_REDUCTION        |- !g s. FiniteAbelianGroup g /\ s SUBSET G ==>
56                       !a::(G). a ** CARD s * GPROD_SET g s * GPROD_SET g (a * (G DIFF s)) = GPROD_SET g G
57
58   Group Factorial:
59   GFACT_def              |- !g. GFACT g = GPROD_SET g G
60   GFACT_element          |- !g. FiniteAbelianMonoid g ==> GFACT g IN G
61   GFACT_identity         |- !g a. FiniteAbelianGroup g /\ a IN G ==> (GFACT g = a ** CARD G * GFACT g)
62   finite_abelian_Fermat  |- !g a. FiniteAbelianGroup g /\ a IN G ==> (a ** CARD G = #e)
63
64   Group Iterated Product over a function:
65   OP_IMAGE_DEF    |- !op id f s. OP_IMAGE op id f s = ITSET (\e acc. op (f e) acc) s id
66   OP_IMAGE_EMPTY  |- !op id f. OP_IMAGE op id f {} = id
67   OP_IMAGE_SING   |- !op id f x. OP_IMAGE op id f {x} = op (f x) id
68   OP_IMAGE_THM    |- !op id f. (OP_IMAGE op id f {} = id) /\
69                                (FUN_COMM op f ==> !s. FINITE s ==>
70                      !e. OP_IMAGE op id f (e INSERT s) = op (f e) (OP_IMAGE op id f (s DELETE e)))
71
72   GROUP_IMAGE_DEF          |- !g f s. GPI f s = ITSET (\e acc. f e * acc) s #e
73   group_image_as_op_image  |- !g. GPI = OP_IMAGE $* #e
74   sum_image_as_op_image    |- SIGMA = OP_IMAGE (\x y. x + y) 0
75   prod_image_as_op_image   |- PI = OP_IMAGE (\x y. x * y) 1
76   GITSET_AS_ITSET          |- !g. (\s b. GITSET g s b) = ITSET (\e acc. e * acc)
77   GPROD_SET_AS_GROUP_IMAGE |- !g. GPROD_SET g = GPI I
78   group_image_empty        |- !g f. GPI f {} = #e
79   group_fun_def            |- !g f. gfun f <=> !x. x IN G ==> f x IN G
80   group_image_sing         |- !g. Monoid g ==> !f. gfun f ==> !x. x IN G ==> (GPI f {x} = f x)
81
82*)
83
84
85(* ------------------------------------------------------------------------- *)
86(* Fermat's Little Theorem of Abelian Groups.                                *)
87(* ------------------------------------------------------------------------- *)
88
89(* Theorem: For Group g, a IN G ==> GPROD_SET g a * G = GPROD_SET g G *)
90(* Proof:
91   This is trivial by group_coset_eq_itself.
92*)
93val GPROD_SET_IMAGE = store_thm(
94  "GPROD_SET_IMAGE",
95  ``!g a. Group g /\ a IN G ==> (GPROD_SET g (a * G) = GPROD_SET g G)``,
96  rw[group_coset_eq_itself]);
97
98(* ------------------------------------------------------------------------- *)
99(* An Invariant Property when reducing GPROD_SET g (IMAGE (\z. a*z) G):
100     GPROD_SET g (IMAGE (\z. a*z) G)
101   = (a*z) * GPROD_SET g ((IMAGE (\z. a*z) G) DELETE (a*z))
102   = a * (GPROD_SET g (z INSERT {})) * GPROD_SET g (IMAGE (\z. a*z) (G DELETE z))
103   = a * <building up a GPROD_SET> * <reducing down a GPROD_SET>
104   = a*a * <building one more> * <reducing one more>
105   = a*a*a * <building one more> * <reducing one more>
106   = a**(CARD G) * GPROD_SET g G * GPROD_SET g {}
107   = a**(CARD G) * GPROD_SET g G * #e
108   = a**(CARD G) * GPROD_SET g G
109*)
110(* ------------------------------------------------------------------------- *)
111
112(* Theorem: [INSERT for GPROD_SET_REDUCTION]
113            (a*x)* GPROD_SET g (coset g (G DIFF (x INSERT t)))
114            = GPROD_SET g (coset g (G DIFF t)) *)
115(* Proof:
116   Essentially this is to prove:
117   a * x * GPROD_SET g {a * z | z | z IN G /\ z <> x /\ z NOTIN s} =
118           GPROD_SET g {a * z | z | z IN G /\ z NOTIN s}
119   Let q = {a * z | z | z IN G /\ z <> x /\ z NOTIN s}
120       p = {a * z | z | z IN G /\ z NOTIN s}
121   Since p = (a*x) INSERT q   by EXTENSION,
122     and (a*x) NOTIN q        by group_lcancel, a NOTIN s.
123     and (a*x) IN G           by group_op_element
124   RHS = GPROD_SET g p
125       = GPROD_SET g ((a*x) INSERT q)            by p = (a*x) INSERT q
126       = (a*x) * GPROD_SET g (q DELETE (a*x))    by GPROD_SET_THM
127       = (a*x) * GPROD_SET g q                   by DELETE_NON_ELEMENT, (a*x) NOTIN q.
128       = LHS
129*)
130val GPROD_SET_REDUCTION_INSERT = store_thm(
131  "GPROD_SET_REDUCTION_INSERT",
132  ``!g s. FiniteAbelianGroup g /\ s SUBSET G ==>
133   !a x::(G). x NOTIN s ==>
134   (a * x * GPROD_SET g (a * (G DIFF (x INSERT s))) = GPROD_SET g (a * (G DIFF s)))``,
135  rw[coset_def, IMAGE_DEF, EXTENSION, RES_FORALL_THM] >>
136  qabbrev_tac `p = {a * z | z | z IN G /\ z NOTIN s}` >>
137  qabbrev_tac `q = {a * z | z | z IN G /\ z <> x /\ z NOTIN s}` >>
138  (`p = (a * x) INSERT q` by (rw[EXTENSION, EQ_IMP_THM, Abbr`p`, Abbr`q`] >> metis_tac[])) >>
139  `AbelianGroup g /\ Group g /\ FINITE G` by metis_tac[FiniteAbelianGroup_def, AbelianGroup_def] >>
140  `!z. z IN G /\ (a * z = a * x) <=> (z = x)` by metis_tac[group_lcancel] >>
141  (`(a * x) NOTIN q` by (rw[Abbr`q`] >> metis_tac[])) >>
142  (`q SUBSET G` by (rw[EXTENSION, SUBSET_DEF, Abbr`q`] >> rw[])) >>
143  `a * x IN G` by rw[] >>
144  `AbelianMonoid g` by rw[abelian_group_is_abelian_monoid] >>
145  `FINITE q` by metis_tac[SUBSET_FINITE] >>
146  metis_tac[GPROD_SET_THM, DELETE_NON_ELEMENT]);
147
148(* Theorem: (a ** n) * <building n-steps GPROD_SET> * <reducing n-steps GPROD_SET> = GPROD_SET g G *)
149(* Proof:
150   By complete induction on CARD s.
151   Case s = {},
152     LHS = a ** (CARD s) * (GPROD_SET g s) * GPROD_SET g (a * (G DIFF s))
153         = a ** 0 * (GPROD_SET g {}) * GPROD_SET g (a * (G DIFF {}))        by CARD_EMPTY
154         = #e * #e * GPROD_SET g (a * G)      by group_exp_0, DIFF_EMPTY, GPROD_SET_EMPTY.
155         = GPROD_SET g (a * G)                by group_lid
156         = GPROD_SET g G                      by GPROD_SET_IMAGE
157         = RHS
158   Case s <> {},
159     Let x = CHOICE s, t = REST s, so s = x INSERT t, x NOTIN t.
160     LHS = a ** (CARD s) * (GPROD_SET g s) * GPROD_SET g (a * (G DIFF s))
161         = a ** SUC(CARD t) *
162           (GPROD_SET g (x INSERT t)) *
163           GPROD_SET g (a * (G DIFF (x INSERT t)))   by CARD s = SUC(CARD t), s = x INSERT t.
164         = a ** SUC(CARD t) *
165           (x * GPROD_SET g (t DELETE x)) *
166           GPROD_SET g (a * (G DIFF (x INSERT t)))   by GPROD_SET_THM
167         = a ** SUC(CARD t) *
168           (x * GPROD_SET g t) *
169           GPROD_SET g (a * (G DIFF (x INSERT t)))   by DELETE_NON_ELEMENT, x NOTIN t.
170         = a*a ** (CARD t) *
171           x * GPROD_SET g t *
172           GPROD_SET g (a * (G DIFF (x INSERT t)))   by group_exp_SUC
173         = a ** (CARD t) *
174           GPROD_SET g t *
175           (a * x) * GPROD_SET g (a * (G DIFF (x INSERT t)))  by Abelian group commuting
176         = a ** (CARD t) *
177           GPROD_SET g t *
178           GPROD_SET g (a * (G DIFF t))   by GPROD_SET_REDUCTION_INSERT
179         = RHS                            by induction
180*)
181val GPROD_SET_REDUCTION = store_thm(
182  "GPROD_SET_REDUCTION",
183  ``!g s. FiniteAbelianGroup g /\ s SUBSET G ==>
184   !a::(G). a ** (CARD s) * (GPROD_SET g s) * GPROD_SET g (a * (G DIFF s)) = GPROD_SET g G``,
185  completeInduct_on `CARD s` >>
186  pop_assum (assume_tac o SIMP_RULE bool_ss[GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO]) >>
187  rw[RES_FORALL_THM] >>
188  `AbelianGroup g /\ Group g /\ FINITE G` by metis_tac[FiniteAbelianGroup_def, AbelianGroup_def, FiniteGroup_def] >>
189  `AbelianMonoid g` by rw[abelian_group_is_abelian_monoid] >>
190  Cases_on `s = {}` >| [
191    rw[GPROD_SET_EMPTY] >>
192    `GPROD_SET g G IN G` by rw[GPROD_SET_PROPERTY] >>
193    rw[GPROD_SET_IMAGE],
194    `?x t. (x = CHOICE s) /\ (t = REST s) /\ (s = x INSERT t)` by rw[CHOICE_INSERT_REST] >>
195    `x IN G` by metis_tac[CHOICE_DEF, SUBSET_DEF] >>
196    `t SUBSET G /\ FINITE t` by metis_tac[REST_SUBSET, SUBSET_TRANS, SUBSET_FINITE] >>
197    `x NOTIN t` by metis_tac[CHOICE_NOT_IN_REST] >>
198    `(CARD s = SUC(CARD t)) /\ CARD t < CARD s` by rw[CARD_INSERT] >>
199    `GPROD_SET g t IN G` by rw[GPROD_SET_PROPERTY] >>
200    `GPROD_SET g (a * (G DIFF (x INSERT t))) IN G` by metis_tac[coset_property, DIFF_SUBSET, SUBSET_FINITE, GPROD_SET_PROPERTY] >>
201    qabbrev_tac `t' = a * (G DIFF (x INSERT t))` >>
202    `a ** CARD s * GPROD_SET g s * GPROD_SET g (a * (G DIFF s)) =
203    a ** SUC(CARD t) * GPROD_SET g (x INSERT t) * GPROD_SET g t'` by rw[Abbr`t'`] >>
204    `_ = a ** SUC(CARD t) * (x * GPROD_SET g (t DELETE x)) * GPROD_SET g t'` by rw[GPROD_SET_THM] >>
205    `_ = a ** SUC(CARD t) * (x * GPROD_SET g t) * GPROD_SET g t'` by metis_tac[DELETE_NON_ELEMENT] >>
206    `_ = (a * a ** (CARD t)) * (x * GPROD_SET g t) * GPROD_SET g t'` by rw[group_exp_SUC] >>
207    `_ = (a ** (CARD t) * a) * (x * GPROD_SET g t) * GPROD_SET g t'` by metis_tac[AbelianGroup_def, group_exp_element] >>
208    `_ = a ** (CARD t) * (a * (x * GPROD_SET g t)) * GPROD_SET g t'` by rw[group_assoc] >>
209    `_ = a ** (CARD t) * ((a * x) * GPROD_SET g t) * GPROD_SET g t'` by rw[group_assoc] >>
210    `_ = a ** (CARD t) * (GPROD_SET g t * (a * x)) * GPROD_SET g t'` by metis_tac[AbelianGroup_def, group_op_element] >>
211    `_ = (a ** (CARD t) * GPROD_SET g t) * (a * x) * GPROD_SET g t'` by rw[group_assoc] >>
212    `_ = a ** (CARD t) * GPROD_SET g t * ((a * x) * GPROD_SET g t')` by rw[group_assoc] >>
213    `_ = a ** (CARD t) * GPROD_SET g t * GPROD_SET g (a * (G DIFF t))` by metis_tac[GPROD_SET_REDUCTION_INSERT] >>
214    rw[]
215  ]);
216
217(* Define Group Factorial *)
218val GFACT_def = Define`
219  GFACT g = GPROD_SET g G
220`;
221
222(* Theorem: GFACT g is an element in Group g. *)
223(* Proof:
224   Since G SUBSET G     by SUBSET_REFL
225   This is true by GPROD_SET_PROPERTY:
226   !g s. FiniteAbelianMonoid g /\ s SUBSET G ==> GPROD_SET g s IN G : thm
227*)
228val GFACT_element = store_thm(
229  "GFACT_element",
230  ``!g. FiniteAbelianMonoid g ==> GFACT g IN G``,
231  rw_tac std_ss[FiniteAbelianMonoid_def, GFACT_def, GPROD_SET_PROPERTY, SUBSET_REFL]);
232
233(* Theorem: For FiniteAbelian Group g, a IN G ==> GFACT g = a ** (CARD g) * GFACT g *)
234(* Proof:
235   Since G SUBSET G  by SUBSET_REFL,
236   and G DIFF G = {},
237   Put s = G in GPROD_SET_REDUCTION:
238       a ** (CARD G) * GPROD_SET g G * GPROD_SET g (a * (G DIFF G)) = GPROD_SET g G
239   ==> a ** (CARD G) * GPROD_SET g G * GPROD_SET g (a * {}) = GPROD_SET g G
240   ==> a ** (CARD G) * GPROD_SET g G * GPROD_SET g {} = GPROD_SET g G  by coset_empty.
241   ==> a ** (CARD G) * GPROD_SET g G * #e = GPROD_SET g G              by GPROD_SET_EMPTY.
242   ==> a ** (CARD G) * GPROD_SET g G = GPROD_SET g G                   by group_assoc and group_rid
243*)
244val GFACT_identity = store_thm(
245  "GFACT_identity",
246  ``!(g:'a group) a. FiniteAbelianGroup g /\ a IN G ==> (GFACT g = a ** (CARD G) * GFACT g)``,
247  rw[GFACT_def] >>
248  `G SUBSET G` by rw[] >>
249  `G DIFF G = {}` by rw[] >>
250  `AbelianGroup g /\ Group g /\ FINITE G` by metis_tac[FiniteAbelianGroup_def, AbelianGroup_def, FiniteGroup_def] >>
251  `AbelianMonoid g` by rw[abelian_group_is_abelian_monoid] >>
252  `GPROD_SET g G IN G` by rw[GPROD_SET_PROPERTY] >>
253  `GPROD_SET g G = a ** (CARD G) * GPROD_SET g G * GPROD_SET g (a * (G DIFF G))` by rw[GPROD_SET_REDUCTION] >>
254  `_ = a ** (CARD G) * GPROD_SET g G * GPROD_SET g (a * {})` by rw[] >>
255  `_ = a ** (CARD G) * GPROD_SET g G * GPROD_SET g {}` by rw[coset_empty] >>
256  `_ = a ** (CARD G) * GPROD_SET g G * #e` by metis_tac[GPROD_SET_EMPTY] >>
257  `_ = a ** (CARD G) * GPROD_SET g G` by rw[] >>
258  rw[]);
259
260(* Theorem: For FiniteAbelian Group g, a IN G ==> a ** (CARD g) = #e *)
261(* Proof:
262   Since  a ** (CARD G) * GFACT g = GFACT g    by GFACT_identity
263   Hence  a ** (CARD G) = #e                   by group_lid_unique
264*)
265val finite_abelian_Fermat = store_thm(
266  "finite_abelian_Fermat",
267  ``!(g:'a group) a. FiniteAbelianGroup g /\ a IN G ==> (a ** (CARD G) = #e)``,
268  rpt strip_tac >>
269  `AbelianGroup g /\ Group g /\ FINITE G` by metis_tac[FiniteAbelianGroup_def, AbelianGroup_def, FiniteGroup_def] >>
270  `AbelianMonoid g` by rw[abelian_group_is_abelian_monoid] >>
271  `GFACT g IN G` by rw[GFACT_element] >>
272  `a ** (CARD G) * GFACT g = GFACT g` by rw[GFACT_identity] >>
273  metis_tac[group_exp_element, group_lid_unique]);
274
275
276(* ------------------------------------------------------------------------- *)
277(* Group Iterated Product over a function.                                   *)
278(* ------------------------------------------------------------------------- *)
279
280(*
281> show_types := true; ITSET_def; show_types := false;
282val it = |- !(s :'a -> bool) (f :'a -> 'b -> 'b) (b :'b).
283    ITSET f s b = if FINITE s then if s = ({} :'a -> bool) then b
284                                   else ITSET f (REST s) (f (CHOICE s) b)
285                  else (ARB :'b): thm
286
287> show_types := true; SUM_IMAGE_DEF; show_types := false;
288val it = |- !(f :'a -> num) (s :'a -> bool).
289    SIGMA f s = ITSET (\(e :'a) (acc :num). f e + acc) s (0 :num): thm
290
291> ITSET_def |> ISPEC ``s:'b -> bool`` |> ISPEC ``(f:'b -> 'a)`` |> ISPEC ``b:'a``;
292val it = |- GITSET g s b = if FINITE s then if s = {} then b else GITSET g (REST s) (CHOICE s * b)
293                           else ARB: thm
294*)
295
296(* A general iterator for operation (op:'a -> 'a -> 'a) and (id:'a) *)
297val OP_IMAGE_DEF = Define `
298    OP_IMAGE (op:'a -> 'a -> 'a) (id:'a) (f:'b -> 'a) (s:'b -> bool) = ITSET (\e acc. op (f e) acc) s id
299`;
300
301(* Theorem: OP_IMAGE op id f {} = id *)
302(* Proof:
303     OP_IMAGE op id f {}
304   = ITSET (\e acc. op (f e) acc) {} id    by OP_IMAGE_DEF
305   = id                                    by ITSET_EMPTY
306*)
307val OP_IMAGE_EMPTY = store_thm(
308  "OP_IMAGE_EMPTY",
309  ``!op id f. OP_IMAGE op id f {} = id``,
310  rw[OP_IMAGE_DEF, ITSET_EMPTY]);
311
312(* Theorem: OP_IMAGE op id f {x} = op (f x) id *)
313(* Proof:
314     OP_IMAGE op id f {x}
315   = ITSET (\e acc. op (f e) acc) {x} id    by OP_IMAGE_DEF
316   = (\e acc. op (f e) acc) x id            by ITSET_SING
317   = op (f x) id                            by application
318*)
319val OP_IMAGE_SING = store_thm(
320  "OP_IMAGE_SING",
321  ``!op id f x. OP_IMAGE op id f {x} = op (f x) id``,
322  rw[OP_IMAGE_DEF, ITSET_SING]);
323
324(*
325Now the hard part: show (\e acc. op (f e) acc) is an accumulative function for ITSET.
326
327val SUM_IMAGE_THM = store_thm(
328  "SUM_IMAGE_THM",
329  ``!f. (SUM_IMAGE f {} = 0) /\
330        (!e s. FINITE s ==>
331               (SUM_IMAGE f (e INSERT s) =
332                f e + SUM_IMAGE f (s DELETE e)))``,
333  REPEAT STRIP_TAC THENL [
334    SIMP_TAC (srw_ss()) [ITSET_THM, SUM_IMAGE_DEF],
335    SIMP_TAC (srw_ss()) [SUM_IMAGE_DEF] THEN
336    Q.ABBREV_TAC `g = \e acc. f e + acc` THEN
337    Q_TAC SUFF_TAC `ITSET g (e INSERT s) 0 =
338                    g e (ITSET g (s DELETE e) 0)` THEN1
339       SRW_TAC [][Abbr`g`] THEN
340    MATCH_MP_TAC COMMUTING_ITSET_RECURSES THEN
341    SRW_TAC [ARITH_ss][Abbr`g`]
342  ]);
343
344val PROD_IMAGE_THM = store_thm(
345  "PROD_IMAGE_THM",
346  ``!f. (PROD_IMAGE f {} = 1) /\
347        (!e s. FINITE s ==>
348          (PROD_IMAGE f (e INSERT s) = f e * PROD_IMAGE f (s DELETE e)))``,
349  REPEAT STRIP_TAC THEN1
350    SIMP_TAC (srw_ss()) [ITSET_THM, PROD_IMAGE_DEF] THEN
351  SIMP_TAC (srw_ss()) [PROD_IMAGE_DEF] THEN
352  Q.ABBREV_TAC `g = \e acc. f e * acc` THEN
353  Q_TAC SUFF_TAC `ITSET g (e INSERT s) 1 =
354                  g e (ITSET g (s DELETE e) 1)` THEN1 SRW_TAC [][Abbr`g`] THEN
355  MATCH_MP_TAC COMMUTING_ITSET_RECURSES THEN
356  SRW_TAC [ARITH_ss][Abbr`g`]);
357
358*)
359
360(* Overload a communtative operation *)
361val _ = overload_on("FUN_COMM", ``\op f. !x y z. op (f x) (op (f y) z) = op (f y) (op (f x) z)``);
362
363(* Theorem: (OP_IMAGE op id f {} = id)  /\
364            (FUN_COMM op f ==> !s. FINITE s ==>
365             !e. OP_IMAGE op id f (e INSERT s) = op (f e) (OP_IMAGE op id f (s DELETE e))) *)
366(* Proof:
367   First goal: P_IMAGE op id f {} = id
368      True by OP_IMAGE_EMPTY.
369   Second goal: OP_IMAGE op id f (e INSERT s) = op (f e) (OP_IMAGE op id f (s DELETE e)))
370      Let g = \e acc. op (f e) acc,
371      Then by OP_IMAGE_DEF, the goal is:
372      to show: ITSET g (e INSERT s) id = op (f e) (ITSET g (s DELETE e) id)
373      or show: ITSET g (e INSERT s) id = g e (ITSET g (s DELETE e) id)
374      Given FUN_COMM op f, the is true by COMMUTING_ITSET_RECURSES.
375*)
376val OP_IMAGE_THM = store_thm(
377  "OP_IMAGE_THM",
378  ``!op id f. (OP_IMAGE op id f {} = id)  /\
379   (FUN_COMM op f ==> !s. FINITE s ==>
380    !e. OP_IMAGE op id f (e INSERT s) = op (f e) (OP_IMAGE op id f (s DELETE e)))``,
381  rpt strip_tac >-
382  rw[OP_IMAGE_EMPTY] >>
383  rw[OP_IMAGE_DEF] >>
384  qabbrev_tac `g = \e acc. op (f e) acc` >>
385  rw[] >>
386  rw[COMMUTING_ITSET_RECURSES, Abbr`g`]);
387
388(* A better iterator for group operation over (f:'b -> 'a) *)
389val GROUP_IMAGE_DEF = Define `
390    GROUP_IMAGE (g:'a group) (f:'b -> 'a) (s:'b -> bool) = ITSET (\e acc. (f e) * acc) s #e
391`;
392
393(* overload GROUP_IMAGE *)
394val _ = temp_overload_on("GPI", ``GROUP_IMAGE g``);
395
396(*
397> GROUP_IMAGE_DEF;
398val it = |- !g f s. GPI f s = ITSET (\e acc. f e * acc) s #e: thm
399*)
400
401(* Theorem: GPI = OP_IMAGE (g.op) (g.id) *)
402(* Proof: by GROUP_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM *)
403val group_image_as_op_image = store_thm(
404  "group_image_as_op_image",
405  ``!g:'a group. GPI = OP_IMAGE (g.op) (g.id)``,
406  rw[GROUP_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM]);
407
408(* Theorem: SUM_IMAGE = OP_IMAGE (\(x y):num. x + y) 0 *)
409(* Proof: by SUM_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM *)
410val sum_image_as_op_image = store_thm(
411  "sum_image_as_op_image",
412  ``SIGMA = OP_IMAGE (\(x y):num. x + y) 0``,
413  rw[SUM_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM]);
414
415(* Theorem: PROD_IMAGE = OP_IMAGE (\(x y):num. x * y) 1 *)
416(* Proof: by PROD_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM *)
417val prod_image_as_op_image = store_thm(
418  "prod_image_as_op_image",
419  ``PI = OP_IMAGE (\(x y):num. x * y) 1``,
420  rw[PROD_IMAGE_DEF, OP_IMAGE_DEF, FUN_EQ_THM]);
421
422(*
423val _ = clear_overloads_on("GITSET");
424val _ = clear_overloads_on("GPI");
425val _ = overload_on("GITSET", ``\g s b. ITSET g.op s b``);
426val _ = overload_on("GPI", ``GROUP_IMAGE g``);
427*)
428
429(* val _ = overload_on("GITSET", ``\g s b. ITSET g.op s b``); *)
430
431(* Theorem: GITSET g = ITSET (\e acc. g.op e acc) *)
432(* Proof:
433   Note g.op = (\e acc. e * acc)   by FUN_EQ_THM
434
435     GITSET g s b
436   = ITSET g.op s b                by notation
437   = ITSET (\e acc. e * acc) s b   by ITSET_CONG
438
439   Hence GITSET g = ITSET (\e acc. g.op e acc)  by FUN_EQ_THM
440*)
441val GITSET_AS_ITSET = store_thm(
442  "GITSET_AS_ITSET",
443  ``!g:'a group. GITSET g = ITSET (\e acc. g.op e acc)``,
444  rw[FUN_EQ_THM] >>
445  `g.op = (\e acc. e * acc)` by rw[FUN_EQ_THM] >>
446  `ITSET g.op = ITSET (\e acc. e * acc)` by rw[ITSET_CONG] >>
447  rw[]);
448
449(*
450> ITSET_def |> ISPEC ``s:'b -> bool`` |> ISPEC ``(g:'a group).op`` |> ISPEC ``b:'a``;
451val it = |- GITSET g s b = if FINITE s then if s = {} then b else GITSET g (REST s) (CHOICE s * b)
452                           else ARB: thm
453*)
454
455(* Theorem: GPROD_SET g = GPI I *)
456(* Proof:
457   Note g.op = (\e acc. e * acc)    by FUN_EQ_THM
458
459     GPROD_SET g x
460   = GITSET g x #e                  by GPROD_SET_def
461   = ITSET g.op x #e                by notation
462   = ITSET (\e acc. e * acc) x #e   by above
463   = GPI I x                        by GROUP_IMAGE_DEF
464   Hence GPROD_SET g = GPI I        by FUN_EQ_THM
465*)
466val GPROD_SET_AS_GROUP_IMAGE = store_thm(
467  "GPROD_SET_AS_GROUP_IMAGE",
468  ``!g:'a group. GPROD_SET g = GPI I``,
469  rw[FUN_EQ_THM] >>
470  `g.op = (\e acc. e * acc)` by rw[FUN_EQ_THM] >>
471  `ITSET g.op = ITSET (\e acc. e * acc)` by rw[ITSET_CONG] >>
472  `GPROD_SET g x = GITSET g x #e` by rw[GPROD_SET_def] >>
473  `_ = ITSET (\e acc. e * acc) x #e` by rw[] >>
474  `_ = GPI I x` by rw[GROUP_IMAGE_DEF] >>
475  rw[]);
476
477(* Theorem: GPI f {} = #e *)
478(* Proof
479     GPI f {}
480   = GROUP_IMAGE g f {}               by notation
481   = ITSET (\e acc. f e * acc) {} #e  by GROUP_IMAGE_DEF
482   = #e                               by ITSET_EMPTY
483*)
484val group_image_empty = store_thm(
485  "group_image_empty",
486  ``!g:'a group. !f. GPI f {} = #e``,
487  rw[GROUP_IMAGE_DEF, ITSET_EMPTY]);
488
489(* Define a group function *)
490val group_fun_def = Define `
491    group_fun (g:'a group) f = !x. x IN G ==> f x IN G
492`;
493
494(* overload on group function *)
495val _ = temp_overload_on("gfun", ``group_fun g``);
496
497(* Theorem: Monoid g ==> !f. gfun f ==> !x. x IN G ==> (GPI f {x} = f x) *)
498(* Proof:
499   Note x IN G ==> f x IN G            by group_fun_def
500     GPI f {x}
501   = GROUP_IMAGE g f {x}               by notation
502   = ITSET (\e acc. f e * acc) {x} #e  by GROUP_IMAGE_DEF
503   = f x * #e                          by ITSET_SING
504   = f x                               by monoid_rid
505*)
506val group_image_sing = store_thm(
507  "group_image_sing",
508  ``!g:'a group. Monoid g ==> !f. gfun f ==> !x. x IN G ==> (GPI f {x} = f x)``,
509  rw[GROUP_IMAGE_DEF, group_fun_def, ITSET_SING]);
510
511
512(* ------------------------------------------------------------------------- *)
513
514(* export theory at end *)
515val _ = export_theory();
516
517(*===========================================================================*)
518