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