1(* non-interactive mode
2*)
3open HolKernel Parse boolLib;
4val _ = new_theory "abelian_group";
5
6(* interactive mode
7show_assums := true;
8loadPath := union ["..", "../finished"] (!loadPath);
9app load
10["bossLib", "listTheory", "HurdUseful", "subtypeTools",
11"res_quanTools", "res_quan2Theory", "pred_setTheory",
12"extra_pred_setTheory", "arithContext", "relationTheory",
13"ho_proverTools", "prob_extraTools", "prob_extraTheory",
14"extra_listTheory", "subtypeTheory", "listContext",
15"arithmeticTheory", "groupTheory", "groupContext", "extra_numTheory",
16"gcdTheory", "dividesTheory", "primeTheory", "extra_arithTheory",
17"finite_groupTheory", "finite_groupContext"];
18*)
19
20open bossLib listTheory HurdUseful subtypeTools res_quanTools
21     pred_setTheory extra_pred_setTheory arithContext relationTheory
22     ho_proverTools extra_listTheory
23     subtypeTheory res_quanTheory listContext arithmeticTheory groupTheory
24     groupContext extra_numTheory gcdTheory dividesTheory
25     extra_arithTheory finite_groupTheory finite_groupContext;
26
27val EXISTS_DEF = boolTheory.EXISTS_DEF;
28
29infixr 0 ++ << || THENC ORELSEC ORELSER ##;
30infix 1 >>;
31
32val op!! = op REPEAT;
33val op++ = op THEN;
34val op<< = op THENL;
35val op|| = op ORELSE;
36val op>> = op THEN1;
37
38(* ------------------------------------------------------------------------- *)
39(* Tools.                                                                    *)
40(* ------------------------------------------------------------------------- *)
41
42val S_TAC = !! (POP_ASSUM MP_TAC) ++ !! RESQ_STRIP_TAC;
43
44val RESQ_TAC =
45  POP_ASSUM_TAC
46  (simpLib.SIMP_TAC std_ss
47  [RES_EXISTS_UNIQUE, RES_FORALL, RES_EXISTS, RES_SELECT,
48   IN_FUNSET, IN_DFUNSET]);
49
50val std_pc = precontext_mergel [arith_pc, list_pc];
51val std_c = precontext_compile std_pc;
52
53val (R_TAC, AR_TAC, R_TAC', AR_TAC') = SIMPLIFY_TACS std_c;
54
55val (G_TAC, AG_TAC, G_TAC', AG_TAC') = SIMPLIFY_TACS finite_group_c;
56
57
58(* ------------------------------------------------------------------------- *)
59(* Definitions.                                                              *)
60(* ------------------------------------------------------------------------- *)
61
62val abelian_def = Define
63  `abelian G = !g h :: gset G. gop G g h = gop G h g`;
64
65(* ------------------------------------------------------------------------- *)
66(* Theorems.                                                                 *)
67(* ------------------------------------------------------------------------- *)
68
69val ABELIAN_GPOW_GOP = store_thm
70  ("ABELIAN_GPOW_GOP",
71   ``!G :: finite_group. !g h :: gset G. !n.
72       abelian G ==>
73       (gpow G (gop G g h) n = gop G (gpow G g n) (gpow G h n))``,
74   S_TAC
75   ++ Induct_on `n` >> G_TAC []
76   ++ G_TAC []
77   ++ Suff
78      `gop G (gop G h (gpow G g n)) (gpow G h n) =
79       gop G (gop G (gpow G g n) h) (gpow G h n)`
80   >> R_TAC [GROUP_ASSOC, FINITE_GROUP_GROUP, GPOW_SUBTYPE, GOP_SUBTYPE]
81   ++ G_TAC []
82   ++ Q.PAT_X_ASSUM `abelian G` MP_TAC
83   ++ R_TAC [abelian_def]
84   ++ DISCH_THEN (fn th => G_TAC [Q_RESQ_HALF_SPECL [`h`, `gpow G g n`] th]));
85
86val ABELIAN_GORD_GCD_1 = store_thm
87  ("ABELIAN_GORD_GCD_1",
88   ``!G :: finite_group. !g h :: gset G.
89       abelian G /\ (gcd (gord G g) (gord G h) = 1) ==>
90       (gord G (gop G g h) = gord G g * gord G h)``,
91   S_TAC
92   ++ G_TAC [IS_GORD]
93   ++ S_TAC
94   >> (G_TAC [ABELIAN_GPOW_GOP]
95       ++ Suff `gpow G h (gord G g * gord G h) = gid G`
96       >> G_TAC []
97       ++ ONCE_REWRITE_TAC [MULT_COMM]
98       ++ G_TAC [])
99   ++ Suff `gord G g * gord G h <= m` >> DECIDE_TAC
100   ++ MATCH_MP_TAC DIVIDES_LE
101   ++ S_TAC >> R_TAC []
102   ++ R_TAC [GCD_1_LCM]
103   ++ G_TAC [GSYM GPOW_GID_GORD]
104   ++ AG_TAC [ABELIAN_GPOW_GOP]
105   ++ Know `gpow G h m = ginv G (gpow G g m)`
106   >> (ONCE_REWRITE_TAC [EQ_SYM_EQ]
107       ++ G_TAC [IS_GINV])
108   ++ G_TAC [GINV_GID]
109   ++ POP_ASSUM K_TAC
110   ++ S_TAC
111   ++ G_TAC [GSYM GORD_GID_UNIQUE]
112   ++ Suff `!p. prime p ==> ~divides p (gord G (gpow G g m))`
113   >> PROVE_TAC [EXISTS_PRIME_DIVISOR]
114   ++ S_TAC
115   ++ Suff `divides p (gcd (gord G g) (gord G h))`
116   >> (ASM_REWRITE_TAC []
117       ++ R_TAC []
118       ++ PROVE_TAC [NOT_PRIME_1])
119   ++ R_TAC [DIVIDES_GCD]
120   ++ CONJ_TAC
121   >> (MP_TAC (Q_RESQ_HALF_SPECL [`G`, `g`] PRIME_DIVIDES_GORD_GPOW)
122       ++ ASM_REWRITE_TAC []
123       ++ DISCH_THEN MATCH_MP_TAC
124       ++ PROVE_TAC [])
125   ++ Suff `divides p (gord G (gpow G h m))`
126   >> (MP_TAC (Q_RESQ_HALF_SPECL [`G`, `h`] PRIME_DIVIDES_GORD_GPOW)
127       ++ Q.PAT_X_ASSUM `gpow G h m = x` K_TAC
128       ++ ASM_REWRITE_TAC []
129       ++ PROVE_TAC [])
130   ++ G_TAC [GORD_GINV]);
131
132(* The structure theorem *)
133
134val STRUCTURE_LEMMA = store_thm
135  ("STRUCTURE_LEMMA",
136   ``!G :: finite_group.
137       abelian G ==>
138       !g1 g2 :: gset G. ?h :: gset G. gord G h = lcm (gord G g1) (gord G g2)``,
139   NTAC 2 RESQ_STRIP_TAC
140   ++ Suff
141      `!g. !g1 g2 :: gset G.
142         (gcd (gord G g1) (gord G g2) = g) ==>
143         ?h :: gset G. gord G h = lcm (gord G g1) (gord G g2)`
144   >> (S_TAC
145       ++ Q.PAT_X_ASSUM `!g. P g` (MP_TAC o Q.SPEC `gcd (gord G g1) (gord G g2)`)
146       ++ G_TAC [])
147   ++ HO_MATCH_MP_TAC FACTOR_INDUCT
148   ++ CONJ_TAC >> G_TAC []
149   ++ CONJ_TAC
150   >> (S_TAC
151       ++ Q_RESQ_EXISTS_TAC `gop G g1 g2`
152       ++ G_TAC' [lcm_def, GORD_EQ_0]
153       ++ G_TAC [ABELIAN_GORD_GCD_1])
154   ++ S_TAC
155   ++ MP_TAC (Q.SPECL [`gord G g1`, `gord G g2`] FACTOR_GCD)
156   ++ G_TAC []
157   ++ DISCH_THEN (MP_TAC o Q.SPEC `p`)
158   ++ R_TAC []
159   ++ RESQ_STRIP_TAC <<
160   [POP_ASSUM MP_TAC
161    ++ Know `p * gord G (gpow G g2 p) = gord G g2`
162    >> (G_TAC [GORD_GPOW_PRIME]
163        ++ Suff `divides p (gord G g2)`
164        >> (R_TAC [DIVIDES_ALT] ++ PROVE_TAC [MULT_COMM])
165        ++ Suff `divides p (gcd (gord G g1) (gord G g2))`
166        >> R_TAC [DIVIDES_GCD]
167        ++ ASM_REWRITE_TAC []
168        ++ R_TAC [])
169    ++ DISCH_THEN
170       (fn th =>
171        CONV_TAC (RATOR_CONV (REWRITE_CONV [SYM th]))
172        ++ R_TAC []
173        ++ ASSUME_TAC th)
174    ++ S_TAC
175    ++ Q.PAT_X_ASSUM `!g1 :: gset G. P g1`
176       (MP_TAC o Q_RESQ_HALF_SPECL [`g1`, `gpow G g2 p`])
177    ++ G_TAC' []
178    ++ Know `gcd (gord G g1) (gord G (gpow G g2 p)) = g`
179    >> (POP_ASSUM MP_TAC
180        ++ Cases_on `p` >> AR_TAC []
181        ++ R_TAC [])
182    ++ POP_ASSUM K_TAC
183    ++ RESQ_STRIP_TAC
184    ++ Suff `lcm (gord G g1) (gord G (gpow G g2 p)) =
185                 lcm (gord G g1) (gord G g2)`
186    >> R_TAC []
187    ++ G_TAC [lcm_def, GORD_EQ_0]
188    ++ Q.PAT_X_ASSUM `p * x = y` (R_TAC o wrap o SYM)
189    ++ Know `gord G g1 * (p * gord G (gpow G g2 p)) =
190                 p * (gord G g1 * gord G (gpow G g2 p))`
191    >> PROVE_TAC [MULT_ASSOC, MULT_COMM]
192    ++ R_TAC []
193    ++ DISCH_THEN K_TAC
194    ++ Suff `0 < g` >> R_TAC [DIV_CANCEL]
195    ++ Suff `~(g = 0)` >> (R_TAC [] ++ DECIDE_TAC)
196    ++ S_TAC
197    ++ AG_TAC [GORD_EQ_0],
198    POP_ASSUM MP_TAC
199    ++ Know `p * gord G (gpow G g1 p) = gord G g1`
200    >> (G_TAC [GORD_GPOW_PRIME]
201        ++ Suff `divides p (gord G g1)`
202        >> (R_TAC [DIVIDES_ALT] ++ PROVE_TAC [MULT_COMM])
203        ++ Suff `divides p (gcd (gord G g1) (gord G g2))`
204        >> R_TAC [DIVIDES_GCD]
205        ++ ASM_REWRITE_TAC []
206        ++ R_TAC [])
207    ++ DISCH_THEN
208       (fn th =>
209        CONV_TAC (RATOR_CONV (REWRITE_CONV [SYM th]))
210        ++ R_TAC []
211        ++ ASSUME_TAC th)
212    ++ S_TAC
213    ++ Q.PAT_X_ASSUM `!g1 :: gset G. P g1`
214       (MP_TAC o Q_RESQ_HALF_SPECL [`gpow G g1 p`, `g2`])
215    ++ G_TAC' []
216    ++ Know `gcd (gord G (gpow G g1 p)) (gord G g2) = g`
217    >> (POP_ASSUM MP_TAC
218        ++ Cases_on `p` >> AR_TAC []
219        ++ R_TAC [])
220    ++ POP_ASSUM K_TAC
221    ++ RESQ_STRIP_TAC
222    ++ Suff `lcm (gord G (gpow G g1 p)) (gord G g2) =
223                 lcm (gord G g1) (gord G g2)`
224    >> R_TAC []
225    ++ G_TAC [lcm_def, GORD_EQ_0]
226    ++ Q.PAT_X_ASSUM `p * x = y` (R_TAC o wrap o SYM)
227    ++ Suff `0 < g` >> R_TAC [DIV_CANCEL, GSYM MULT_ASSOC]
228    ++ Suff `~(g = 0)` >> DECIDE_TAC
229    ++ S_TAC
230    ++ AG_TAC [GORD_EQ_0]]);
231
232val STRUCTURE_THM = store_thm
233  ("STRUCTURE_THM",
234   ``!G :: finite_group.
235       abelian G ==> ?g :: gset G. !h :: gset G. gpow G h (gord G g) = gid G``,
236   S_TAC
237   ++ MP_TAC (Q_RESQ_SPEC `G` MAXIMAL_ORDER)
238   ++ S_TAC
239   ++ Q_RESQ_EXISTS_TAC `g`
240   ++ R_TAC []
241   ++ S_TAC
242   ++ R_TAC [GPOW_GID_GORD]
243   ++ MP_TAC (Q_RESQ_SPEC `G` STRUCTURE_LEMMA)
244   ++ R_TAC []
245   ++ DISCH_THEN (MP_TAC o Q_RESQ_SPECL [`g`, `h`])
246   ++ S_TAC
247   ++ Suff `gord G h' = gord G g` >> PROVE_TAC [DIVIDES_LCM_R]
248   ++ Suff `gord G h' <= gord G g /\ gord G g <= gord G h'`
249   >> DECIDE_TAC
250   ++ S_TAC >> G_TAC []
251   ++ MATCH_MP_TAC DIVIDES_LE
252   ++ S_TAC
253   >> (POP_ASSUM K_TAC
254       ++ Suff `~(gord G h' = 0)` >> DECIDE_TAC
255       ++ G_TAC [GORD_EQ_0])
256   ++ PROVE_TAC [DIVIDES_LCM_L]);
257
258(* non-interactive mode
259*)
260val _ = export_theory ();
261