1(* ========================================================================= *) 2(* Create "groupTheory" setting up the theory of groups *) 3(* ========================================================================= *) 4 5(* ------------------------------------------------------------------------- *) 6(* Load and open relevant theories. *) 7(* (Comment out "load"s and "quietdec"s for compilation.) *) 8(* ------------------------------------------------------------------------- *) 9(* 10val () = loadPath := [] @ !loadPath; 11val () = app load 12 ["Algebra", 13 "bossLib", "metisLib", "res_quanTools", 14 "optionTheory", "listTheory", 15 "arithmeticTheory", "dividesTheory", "gcdTheory", 16 "pred_setTheory", "pred_setSyntax", 17 "primalityTools"]; 18val () = quietdec := true; 19*) 20 21open HolKernel Parse boolLib bossLib metisLib res_quanTools; 22open optionTheory listTheory arithmeticTheory dividesTheory gcdTheory; 23open pred_setTheory; 24open primalityTools; 25 26(* 27val () = quietdec := false; 28*) 29 30(* ------------------------------------------------------------------------- *) 31(* Start a new theory called "group". *) 32(* ------------------------------------------------------------------------- *) 33 34val _ = new_theory "group"; 35 36val ERR = mk_HOL_ERR "group"; 37val Bug = mlibUseful.Bug; 38val Error = ERR ""; 39 40val Bug = fn s => (print ("\n\nBUG: " ^ s ^ "\n\n"); Bug s); 41 42(* ------------------------------------------------------------------------- *) 43(* Show oracle tags. *) 44(* ------------------------------------------------------------------------- *) 45 46val () = show_tags := true; 47 48(* ------------------------------------------------------------------------- *) 49(* The subtype context. *) 50(* ------------------------------------------------------------------------- *) 51 52val context = subtypeTools.empty2; 53val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 54 55(* ------------------------------------------------------------------------- *) 56(* Helper proof tools. *) 57(* ------------------------------------------------------------------------- *) 58 59infixr 0 << 60infixr 1 ++ || THENC ORELSEC 61infix 2 >> 62 63val op ++ = op THEN; 64val op << = op THENL; 65val op >> = op THEN1; 66val op || = op ORELSE; 67val Know = Q_TAC KNOW_TAC; 68val Suff = Q_TAC SUFF_TAC; 69val REVERSE = Tactical.REVERSE; 70val lemma = Tactical.prove; 71 72val norm_rule = 73 SIMP_RULE (simpLib.++ (pureSimps.pure_ss, resq_SS)) 74 [GSYM LEFT_FORALL_IMP_THM, GSYM RIGHT_FORALL_IMP_THM, 75 AND_IMP_INTRO, GSYM CONJ_ASSOC]; 76 77fun match_tac th = 78 let 79 val th = norm_rule th 80 val (_,tm) = strip_forall (concl th) 81 in 82 (if is_imp tm then MATCH_MP_TAC else MATCH_ACCEPT_TAC) th 83 end; 84 85(* ------------------------------------------------------------------------- *) 86(* Helper theorems. *) 87(* ------------------------------------------------------------------------- *) 88 89val FUNPOW_ADD = store_thm 90 ("FUNPOW_ADD", 91 ``!f p q x. FUNPOW f (p + q) x = FUNPOW f p (FUNPOW f q x)``, 92 Induct_on `q` 93 ++ RW_TAC arith_ss [FUNPOW, ADD_CLAUSES]); 94 95val FUNPOW_MULT = store_thm 96 ("FUNPOW_MULT", 97 ``!f p q x. FUNPOW f (p * q) x = FUNPOW (\x. FUNPOW f p x) q x``, 98 Induct_on `q` 99 ++ RW_TAC arith_ss [FUNPOW, MULT_CLAUSES] 100 ++ ONCE_REWRITE_TAC [ONCE_REWRITE_RULE [ADD_COMM] FUNPOW_ADD] 101 ++ RW_TAC std_ss []); 102 103val DELETE_INSERT = store_thm 104 ("DELETE_INSERT", 105 ``!e s. ~(e IN s) ==> ((e INSERT s) DELETE e = s)``, 106 RW_TAC std_ss [EXTENSION, IN_DELETE, IN_INSERT] 107 ++ METIS_TAC []); 108 109val finite_image_card = store_thm 110 ("finite_image_card", 111 ``!f s. FINITE s ==> CARD (IMAGE f s) <= CARD s``, 112 RW_TAC std_ss [] 113 ++ POP_ASSUM MP_TAC 114 ++ Q.SPEC_TAC (`s`,`s`) 115 ++ HO_MATCH_MP_TAC FINITE_INDUCT 116 ++ RW_TAC std_ss 117 [INJ_DEF, CARD_INSERT, NOT_IN_EMPTY, SUBSET_DEF, IN_IMAGE, 118 IMAGE_EMPTY, CARD_EMPTY, IN_INSERT, IMAGE_INSERT, IMAGE_FINITE] 119 ++ RW_TAC arith_ss []); 120 121val finite_inj_card = store_thm 122 ("finite_inj_card", 123 ``!f s t. 124 FINITE s ==> 125 (INJ f s t = IMAGE f s SUBSET t /\ (CARD s = CARD (IMAGE f s)))``, 126 RW_TAC std_ss [] 127 ++ POP_ASSUM MP_TAC 128 ++ Q.SPEC_TAC (`s`,`s`) 129 ++ HO_MATCH_MP_TAC FINITE_INDUCT 130 ++ RW_TAC std_ss 131 [INJ_DEF, CARD_INSERT, NOT_IN_EMPTY, SUBSET_DEF, IN_IMAGE, 132 IMAGE_EMPTY, CARD_EMPTY, IN_INSERT, IMAGE_INSERT, IMAGE_FINITE] 133 ++ REVERSE CASE_TAC >> PROVE_TAC [] 134 ++ MATCH_MP_TAC (PROVE [] ``~a /\ ~b ==> (a = b)``) 135 ++ CONJ_TAC >> METIS_TAC [] 136 ++ RW_TAC std_ss [] 137 ++ DISJ2_TAC 138 ++ MATCH_MP_TAC (DECIDE ``b <= a ==> ~(SUC a = b)``) 139 ++ RW_TAC arith_ss [finite_image_card]); 140 141val finite_inj_surj_imp = store_thm 142 ("finite_inj_surj_imp", 143 ``!f s. FINITE s /\ SURJ f s s ==> INJ f s s``, 144 RW_TAC std_ss [IMAGE_SURJ, finite_inj_card, SUBSET_REFL]); 145 146val finite_inj_surj_imp' = store_thm 147 ("finite_inj_surj_imp'", 148 ``!f s. FINITE s /\ INJ f s s ==> SURJ f s s``, 149 RW_TAC std_ss [IMAGE_SURJ] 150 ++ POP_ASSUM MP_TAC 151 ++ RW_TAC std_ss [finite_inj_card, IMAGE_FINITE, SUBSET_EQ_CARD]); 152 153val finite_inj_surj = store_thm 154 ("finite_inj_surj", 155 ``!f s. FINITE s ==> (INJ f s s = SURJ f s s)``, 156 METIS_TAC [finite_inj_surj_imp, finite_inj_surj_imp']); 157 158val delete_absent = store_thm 159 ("delete_absent", 160 ``!s e. ~(e IN s) ==> (s DELETE e = s)``, 161 RW_TAC std_ss [EXTENSION, IN_DELETE] 162 ++ METIS_TAC []); 163 164val commuting_itset = store_thm 165 ("commuting_itset", 166 ``!f. 167 (!x y z. f x (f y z) = f y (f x z)) ==> 168 !e s b. 169 FINITE s /\ ~(e IN s) ==> 170 (ITSET f (e INSERT s) b = f e (ITSET f s b))``, 171 RW_TAC std_ss [] 172 ++ Know `s DELETE e = s` >> METIS_TAC [delete_absent] 173 ++ MP_TAC (Q.SPECL [`f`,`e`,`s`,`b`] COMMUTING_ITSET_RECURSES) 174 ++ RW_TAC std_ss []); 175 176val finite_num = store_thm 177 ("finite_num", 178 ``!s. FINITE s = ?n : num. !m. m IN s ==> m < n``, 179 RW_TAC std_ss [] 180 ++ EQ_TAC 181 >> (Q.SPEC_TAC (`s`,`s`) 182 ++ HO_MATCH_MP_TAC FINITE_INDUCT 183 ++ RW_TAC arith_ss [NOT_IN_EMPTY, IN_INSERT] 184 ++ Q.EXISTS_TAC `MAX n (SUC e)` 185 ++ RW_TAC arith_ss [] 186 ++ RES_TAC 187 ++ DECIDE_TAC) 188 ++ STRIP_TAC 189 ++ POP_ASSUM MP_TAC 190 ++ Q.SPEC_TAC (`s`,`s`) 191 ++ Induct_on `n` 192 >> (RW_TAC arith_ss [] 193 ++ Suff `s = {}` >> RW_TAC std_ss [FINITE_EMPTY] 194 ++ ONCE_REWRITE_TAC [EXTENSION] 195 ++ RW_TAC std_ss [NOT_IN_EMPTY]) 196 ++ RW_TAC std_ss [] 197 ++ MATCH_MP_TAC 198 (SIMP_RULE std_ss [GSYM RIGHT_FORALL_IMP_THM, AND_IMP_INTRO] 199 SUBSET_FINITE) 200 ++ Q.EXISTS_TAC `n INSERT (s DELETE n)` 201 ++ REVERSE CONJ_TAC 202 >> (ONCE_REWRITE_TAC [EXTENSION] 203 ++ RW_TAC std_ss [IN_INSERT, SUBSET_DEF, IN_DELETE]) 204 ++ RW_TAC std_ss [FINITE_INSERT] 205 ++ FIRST_ASSUM MATCH_MP_TAC 206 ++ RW_TAC arith_ss [IN_DELETE] 207 ++ RES_TAC 208 ++ DECIDE_TAC); 209 210val DIVIDES_ONE = store_thm 211 ("DIVIDES_ONE", 212 ``!n. divides n 1 = (n = 1)``, 213 RW_TAC std_ss [divides_def, MULT_EQ_1]); 214 215val prime_one_lt = store_thm 216 ("prime_one_lt", 217 ``!p. prime p ==> 1 < p``, 218 RW_TAC std_ss [] 219 ++ Suff `~(p = 0) /\ ~(p = 1)` >> DECIDE_TAC 220 ++ METIS_TAC [NOT_PRIME_0, NOT_PRIME_1]); 221 222(* ========================================================================= *) 223(* Number Theory *) 224(* ========================================================================= *) 225 226(* ------------------------------------------------------------------------- *) 227(* Basic definitions *) 228(* ------------------------------------------------------------------------- *) 229 230val totient_def = Define 231 `totient n = CARD { i | 0 < i /\ i < n /\ (gcd n i = 1) }`; 232 233(* ------------------------------------------------------------------------- *) 234(* Fermat's Little Theorem *) 235(* ------------------------------------------------------------------------- *) 236 237val mult_lcancel_gcd_imp = store_thm 238 ("mult_lcancel_gcd_imp", 239 ``!n a b c. 240 0 < n /\ (gcd n a = 1) /\ ((a * b) MOD n = (a * c) MOD n) ==> 241 (b MOD n = c MOD n)``, 242 RW_TAC std_ss [] 243 ++ Cases_on `n = 1` >> METIS_TAC [MOD_1] 244 ++ Cases_on `a = 0` >> METIS_TAC [GCD_0R] 245 ++ MP_TAC (Q.SPECL [`a`,`n`] LINEAR_GCD) 246 ++ RW_TAC std_ss [] 247 ++ Know 248 `(p MOD n * (a MOD n * b MOD n)) MOD n = 249 (p MOD n * (a MOD n * c MOD n)) MOD n` 250 >> METIS_TAC [MOD_TIMES2, MOD_MOD] 251 ++ REWRITE_TAC [MULT_ASSOC] 252 ++ Suff `((p MOD n * a MOD n) MOD n) MOD n = 1` 253 >> METIS_TAC [MOD_TIMES2, MOD_MOD, MULT_CLAUSES] 254 ++ RW_TAC arith_ss [MOD_TIMES2] 255 ++ MP_TAC (Q.SPEC `n` MOD_PLUS) 256 ++ ASM_REWRITE_TAC [] 257 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 258 ++ RW_TAC std_ss [ONCE_REWRITE_RULE [MULT_COMM] MOD_EQ_0] 259 ++ RW_TAC arith_ss [MOD_MOD]); 260 261val mult_lcancel_gcd = store_thm 262 ("mult_lcancel_gcd", 263 ``!n a b c. 264 0 < n /\ (gcd n a = 1) ==> 265 (((a * b) MOD n = (a * c) MOD n) = (b MOD n = c MOD n))``, 266 METIS_TAC [MOD_TIMES2, mult_lcancel_gcd_imp]); 267 268val is_gcd_1 = store_thm 269 ("is_gcd_1", 270 ``!n. is_gcd n 1 1``, 271 RW_TAC std_ss [is_gcd_def, ONE_DIVIDES_ALL]); 272 273val gcd_1 = store_thm 274 ("gcd_1", 275 ``!n. gcd n 1 = 1``, 276 METIS_TAC [is_gcd_1, GCD_IS_GCD, IS_GCD_UNIQUE]); 277 278val divides_gcd = store_thm 279 ("divides_gcd", 280 ``!a b. divides (gcd a b) a /\ divides (gcd a b) b``, 281 Suff `!a b. divides (gcd a b) a` >> METIS_TAC [GCD_SYM] 282 ++ RW_TAC std_ss [] 283 ++ Know `is_gcd a b (gcd a b)` >> METIS_TAC [GCD_IS_GCD] 284 ++ RW_TAC std_ss [is_gcd_def]); 285 286val is_gcd_1_mult_imp = store_thm 287 ("is_gcd_1_mult_imp", 288 ``!n a b. is_gcd n a 1 /\ is_gcd n b 1 ==> is_gcd n (a * b) 1``, 289 RW_TAC std_ss [is_gcd_def, ONE_DIVIDES_ALL] 290 ++ Cases_on `gcd a d = 1` 291 >> (MP_TAC (Q.SPECL [`a`,`d`,`b`] L_EUCLIDES) 292 ++ RW_TAC std_ss []) 293 ++ FULL_SIMP_TAC std_ss [DIVIDES_ONE] 294 ++ Suff `F` >> METIS_TAC [] 295 ++ POP_ASSUM MP_TAC 296 ++ RW_TAC std_ss [] 297 ++ Q.PAT_ASSUM `!i. P i` (K ALL_TAC) 298 ++ Q.PAT_ASSUM `!i. P i` MATCH_MP_TAC 299 ++ METIS_TAC [DIVIDES_TRANS, divides_gcd]); 300 301val gcd_1_mult_imp = store_thm 302 ("gcd_1_mult_imp", 303 ``!n a b. (gcd n a = 1) /\ (gcd n b = 1) ==> (gcd n (a * b) = 1)``, 304 METIS_TAC [is_gcd_1_mult_imp, GCD_IS_GCD, IS_GCD_UNIQUE]); 305 306val gcd_modr = store_thm 307 ("gcd_modr", 308 ``!n a. 0 < n ==> (gcd n (a MOD n) = gcd n a)``, 309 METIS_TAC [GCD_SYM, DECIDE ``0 < n ==> ~(n = 0)``, GCD_EFFICIENTLY]); 310 311val euler_totient = store_thm 312 ("euler_totient", 313 ``!n a. (gcd n a = 1) ==> (a ** totient n MOD n = 1 MOD n)``, 314 RW_TAC std_ss [] 315 ++ Cases_on `n = 0` 316 >> RW_TAC bool_ss 317 [totient_def, prim_recTheory.NOT_LESS_0, GSPEC_F, 318 CARD_EMPTY, EXP] 319 ++ Cases_on `n = 1` >> RW_TAC bool_ss [MOD_1] 320 ++ Know `0 < n` >> DECIDE_TAC 321 ++ STRIP_TAC 322 ++ MATCH_MP_TAC mult_lcancel_gcd_imp 323 ++ Q.EXISTS_TAC 324 `ITSET (\y z. y * z) { i | 0 < i /\ i < n /\ (gcd n i = 1) } 1` 325 ++ Know `FINITE { i | 0 < i /\ i < n /\ (gcd n i = 1) }` 326 >> (RW_TAC std_ss [finite_num, GSPECIFICATION] 327 ++ METIS_TAC []) 328 ++ RW_TAC arith_ss [] 329 >> (Suff 330 `!s b. 331 FINITE s /\ (!i. i IN s ==> (gcd n i = 1)) /\ (gcd n b = 1) ==> 332 (gcd n (ITSET (\y z. y * z) s b) = 1)` 333 >> (DISCH_THEN MATCH_MP_TAC 334 ++ RW_TAC std_ss [GSPECIFICATION, gcd_1]) 335 ++ HO_MATCH_MP_TAC (GEN_ALL ITSET_IND) 336 ++ Q.EXISTS_TAC `\y z. y * z` 337 ++ RW_TAC std_ss [] 338 ++ RW_TAC std_ss [ITSET_THM] 339 ++ FIRST_ASSUM (MATCH_MP_TAC o CONV_RULE (REWR_CONV AND_IMP_INTRO)) 340 ++ RW_TAC std_ss [REST_DEF, FINITE_DELETE, IN_DELETE] 341 ++ MATCH_MP_TAC gcd_1_mult_imp 342 ++ METIS_TAC [CHOICE_DEF]) 343 ++ Know `INJ (\i. (i * a) MOD n) {i | 0 < i /\ i < n /\ (gcd n i = 1)} UNIV` 344 >> (RW_TAC std_ss [INJ_DEF, IN_UNIV] 345 ++ Know `i MOD n = i' MOD n` 346 >> METIS_TAC [mult_lcancel_gcd_imp, MULT_COMM] 347 ++ FULL_SIMP_TAC std_ss [GSPECIFICATION] 348 ++ METIS_TAC [LESS_MOD]) 349 ++ STRIP_TAC 350 ++ Know 351 `IMAGE (\i. (i * a) MOD n) {i | 0 < i /\ i < n /\ (gcd n i = 1)} = 352 {i | 0 < i /\ i < n /\ (gcd n i = 1)}` 353 >> (RW_TAC std_ss [GSYM IMAGE_SURJ, GSYM finite_inj_surj] 354 ++ POP_ASSUM MP_TAC 355 ++ RW_TAC bool_ss [INJ_DEF, IN_UNIV] 356 ++ Q.PAT_ASSUM `!i i'. P i i'` (K ALL_TAC) 357 ++ FULL_SIMP_TAC std_ss [GSPECIFICATION, DIVISION] 358 ++ MATCH_MP_TAC (PROVE [] ``(~a ==> ~b) /\ b ==> a /\ b``) 359 ++ CONJ_TAC 360 >> (Cases_on `(i * a) MOD n` 361 ++ RW_TAC arith_ss [GCD_0R]) 362 ++ RW_TAC std_ss [gcd_modr] 363 ++ METIS_TAC [gcd_1_mult_imp]) 364 ++ DISCH_THEN (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [GSYM th]))) 365 ++ RW_TAC std_ss [totient_def] 366 ++ POP_ASSUM MP_TAC 367 ++ POP_ASSUM MP_TAC 368 ++ Suff 369 `!s. 370 FINITE s ==> 371 INJ (\i. (i * a) MOD n) s UNIV ==> 372 ((ITSET (\y z. y * z) s 1 * a ** CARD s) MOD n = 373 ITSET (\y z. y * z) (IMAGE (\i. (i * a) MOD n) s) 1 MOD n)` 374 >> RW_TAC arith_ss [] 375 ++ HO_MATCH_MP_TAC FINITE_INDUCT 376 ++ RW_TAC std_ss 377 [CARD_EMPTY, ITSET_EMPTY, IMAGE_EMPTY, EXP, MULT_CLAUSES, 378 CARD_INSERT, IMAGE_INSERT] 379 ++ Q.PAT_ASSUM `X ==> Y` MP_TAC 380 ++ POP_ASSUM MP_TAC 381 ++ SIMP_TAC bool_ss [INJ_DEF, IN_UNIV] 382 ++ STRIP_TAC 383 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 384 ++ CONJ_TAC >> METIS_TAC [IN_INSERT] 385 ++ STRIP_TAC 386 ++ MP_TAC (Q.ISPEC `\y z : num. y * z` commuting_itset) 387 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 388 ++ SIMP_TAC std_ss [] 389 ++ CONJ_TAC >> METIS_TAC [MULT_ASSOC, MULT_COMM] 390 ++ DISCH_THEN 391 (fn th => 392 MP_TAC (Q.SPECL [`(e * a) MOD n`,`IMAGE (\i. (i * a) MOD n) s`,`1`] th) 393 ++ MP_TAC (Q.SPECL [`e`,`s`,`1`] th)) 394 ++ RW_TAC std_ss [IMAGE_FINITE] 395 ++ POP_ASSUM MP_TAC 396 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 397 ++ CONJ_TAC 398 >> (Q.PAT_ASSUM `!i i'. P i i'` (MP_TAC o Q.SPEC `e`) 399 ++ RW_TAC std_ss [IN_IMAGE, IN_INSERT] 400 ++ METIS_TAC []) 401 ++ DISCH_THEN (fn th => RW_TAC std_ss [th]) 402 ++ POP_ASSUM (K ALL_TAC) 403 ++ Q.PAT_ASSUM `!i i'. P i i'` (K ALL_TAC) 404 ++ MATCH_MP_TAC 405 (METIS_PROVE [MULT_ASSOC, MULT_COMM] 406 ``(((a * c) * (b * d)) MOD n = X) ==> ((a * b * (c * d)) MOD n = X)``) 407 ++ MP_TAC (Q.SPEC `n` MOD_TIMES2) 408 ++ ASM_SIMP_TAC std_ss [] 409 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 410 ++ RW_TAC std_ss [MOD_MOD]); 411 412val prime_is_gcd_1 = store_thm 413 ("prime_is_gcd_1", 414 ``!p a. prime p ==> (is_gcd p a 1 = ~divides p a)``, 415 RW_TAC std_ss [is_gcd_def, DIVIDES_ONE, ONE_DIVIDES_ALL] 416 ++ EQ_TAC 417 >> (DISCH_THEN (MP_TAC o Q.SPEC `p`) 418 ++ METIS_TAC [DIVIDES_REFL, NOT_PRIME_1]) 419 ++ RW_TAC std_ss [] 420 ++ MP_TAC (Q.SPEC `p` prime_def) 421 ++ RW_TAC std_ss [] 422 ++ POP_ASSUM (MP_TAC o Q.SPEC `d`) 423 ++ ASM_REWRITE_TAC [] 424 ++ STRIP_TAC 425 ++ RW_TAC std_ss [] 426 ++ METIS_TAC []); 427 428val prime_gcd_1 = store_thm 429 ("prime_gcd_1", 430 ``!p a. prime p ==> ((gcd p a = 1) = ~divides p a)``, 431 METIS_TAC [prime_is_gcd_1, GCD_IS_GCD, IS_GCD_UNIQUE]); 432 433val prime_totient = store_thm 434 ("prime_totient", 435 ``!p. prime p ==> (totient p = p - 1)``, 436 RW_TAC std_ss [totient_def, prime_gcd_1] 437 ++ Suff `{i | 0 < i /\ i < p /\ ~divides p i} = count p DELETE 0` 438 >> (RW_TAC std_ss [CARD_DELETE, FINITE_COUNT, CARD_COUNT] 439 ++ Suff `F` >> METIS_TAC [] 440 ++ POP_ASSUM (K ALL_TAC) 441 ++ POP_ASSUM MP_TAC 442 ++ RW_TAC std_ss [count_def, GSPECIFICATION] 443 ++ METIS_TAC [NOT_PRIME_0, DECIDE ``0 < p = ~(p = 0)``]) 444 ++ RW_TAC std_ss [EXTENSION, GSPECIFICATION, IN_DELETE, count_def] 445 ++ Suff `0 < x /\ x < p ==> ~divides p x` 446 >> METIS_TAC [DECIDE ``0 < p = ~(p = 0)``] 447 ++ METIS_TAC [DIVIDES_LE, DECIDE ``~(a : num < b) = b <= a``]); 448 449val fermat_little = store_thm 450 ("fermat_little", 451 ``!p a. prime p /\ ~divides p a ==> (a ** (p - 1) MOD p = 1)``, 452 RW_TAC std_ss [] 453 ++ MP_TAC (Q.SPECL [`p`,`a`] euler_totient) 454 ++ RW_TAC std_ss [prime_gcd_1, prime_totient] 455 ++ Suff `0 < p /\ 1 < p` >> METIS_TAC [X_MOD_Y_EQ_X] 456 ++ Suff `~(p = 0) /\ ~(p = 1)` >> DECIDE_TAC 457 ++ METIS_TAC [NOT_PRIME_0, NOT_PRIME_1]); 458 459(* ========================================================================= *) 460(* Groups *) 461(* ========================================================================= *) 462 463(* ------------------------------------------------------------------------- *) 464(* The basic definitions *) 465(* ------------------------------------------------------------------------- *) 466 467val () = Hol_datatype 468 `group = <| carrier : 'a -> bool; 469 id : 'a; 470 inv : 'a -> 'a; 471 mult : 'a -> 'a -> 'a |>`; 472 473val Group_def = Define 474 `Group = 475 { (g : 'a group) | 476 g.id IN g.carrier /\ 477 (!x y :: (g.carrier). g.mult x y IN g.carrier) /\ 478 (!x :: (g.carrier). g.inv x IN g.carrier) /\ 479 (!x :: (g.carrier). g.mult g.id x = x) /\ 480 (!x :: (g.carrier). g.mult (g.inv x) x = g.id) /\ 481 (!x y z :: (g.carrier). g.mult (g.mult x y) z = g.mult x (g.mult y z)) }`; 482 483val group_exp_def = Define 484 `(group_exp G g 0 = G.id) /\ 485 (group_exp G g (SUC n) = G.mult g (group_exp G g n))`; 486 487val AbelianGroup_def = Define 488 `AbelianGroup = 489 { (g : 'a group) | 490 g IN Group /\ !x y :: (g.carrier). g.mult x y = g.mult y x }`; 491 492val FiniteGroup_def = Define 493 `FiniteGroup = { (g : 'a group) | g IN Group /\ FINITE g.carrier }`; 494 495val FiniteAbelianGroup_def = Define 496 `FiniteAbelianGroup = 497 { (g : 'a group) | g IN FiniteGroup /\ g IN AbelianGroup }`; 498 499val group_accessors = fetch "-" "group_accessors"; 500 501(* Syntax operations *) 502 503val group_inv_tm = ``group_inv``; 504 505fun dest_group_inv tm = 506 let 507 val (tm,x) = dest_comb tm 508 val (tm,f) = dest_comb tm 509 val _ = same_const tm group_inv_tm orelse raise ERR "group_inv_neg" "" 510 in 511 (f,x) 512 end; 513 514val is_group_inv = can dest_group_inv; 515 516val group_mult_tm = ``group_mult``; 517 518fun dest_group_mult tm = 519 let 520 val (tm,y) = dest_comb tm 521 val (tm,x) = dest_comb tm 522 val (tm,f) = dest_comb tm 523 val _ = same_const tm group_mult_tm orelse raise ERR "dest_group_mult" "" 524 in 525 (f,x,y) 526 end; 527 528val is_group_mult = can dest_group_mult; 529 530val group_exp_tm = ``group_exp``; 531 532fun dest_group_exp tm = 533 let 534 val (tm,n) = dest_comb tm 535 val (tm,x) = dest_comb tm 536 val (tm,f) = dest_comb tm 537 val _ = same_const tm group_exp_tm orelse raise ERR "dest_group_exp" "" 538 in 539 (f,x,n) 540 end; 541 542val is_group_exp = can dest_group_exp; 543 544(* Theorems *) 545 546val AbelianGroup_Group = store_thm 547 ("AbelianGroup_Group", 548 ``!g. g IN AbelianGroup ==> g IN Group``, 549 RW_TAC std_ss [AbelianGroup_def, GSPECIFICATION]); 550 551val context = subtypeTools.add_judgement2 AbelianGroup_Group context; 552val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 553 554val FiniteGroup_Group = store_thm 555 ("FiniteGroup_Group", 556 ``!g. g IN FiniteGroup ==> g IN Group``, 557 RW_TAC std_ss [FiniteGroup_def, GSPECIFICATION]); 558 559val context = subtypeTools.add_judgement2 FiniteGroup_Group context; 560val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 561 562val FiniteAbelianGroup_FiniteGroup = store_thm 563 ("FiniteAbelianGroup_FiniteGroup", 564 ``!g. g IN FiniteAbelianGroup ==> g IN FiniteGroup``, 565 RW_TAC std_ss [FiniteAbelianGroup_def, GSPECIFICATION]); 566 567val context = subtypeTools.add_judgement2 FiniteAbelianGroup_FiniteGroup context; 568val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 569 570val FiniteAbelianGroup_AbelianGroup = store_thm 571 ("FiniteAbelianGroup_AbelianGroup", 572 ``!g. g IN FiniteAbelianGroup ==> g IN AbelianGroup``, 573 RW_TAC std_ss [FiniteAbelianGroup_def, GSPECIFICATION]); 574 575val context = 576 subtypeTools.add_judgement2 FiniteAbelianGroup_AbelianGroup context; 577val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 578 579val FiniteAbelianGroup_alt = store_thm 580 ("FiniteAbelianGroup_alt", 581 ``FiniteAbelianGroup = 582 { (g : 'a group) | 583 g IN Group /\ 584 (!x y :: (g.carrier). g.mult x y = g.mult y x) /\ 585 FINITE g.carrier }``, 586 RW_TAC std_ss 587 [FiniteAbelianGroup_def, FiniteGroup_def, AbelianGroup_def, 588 EXTENSION, GSPECIFICATION] 589 ++ METIS_TAC []); 590 591val group_id_carrier = store_thm 592 ("group_id_carrier", 593 ``!g :: Group. g.id IN g.carrier``, 594 RW_TAC resq_ss [Group_def, GSPECIFICATION]); 595 596val context = subtypeTools.add_reduction2 group_id_carrier context; 597val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 598 599val group_inv_carrier = store_thm 600 ("group_inv_carrier", 601 ``!g :: Group. !x :: (g.carrier). g.inv x IN g.carrier``, 602 RW_TAC resq_ss [Group_def, GSPECIFICATION]); 603 604val context = subtypeTools.add_reduction2 group_inv_carrier context; 605val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 606 607val group_mult_carrier = store_thm 608 ("group_mult_carrier", 609 ``!g :: Group. !x y :: (g.carrier). g.mult x y IN g.carrier``, 610 RW_TAC resq_ss [Group_def, GSPECIFICATION]); 611 612val context = subtypeTools.add_reduction2 group_mult_carrier context; 613val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 614 615val group_lid = store_thm 616 ("group_lid", 617 ``!g :: Group. !x :: (g.carrier). g.mult g.id x = x``, 618 RW_TAC resq_ss [Group_def, GSPECIFICATION]); 619 620val context = subtypeTools.add_rewrite2 group_lid context; 621val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 622 623val group_linv = store_thm 624 ("group_linv", 625 ``!g :: Group. !x :: (g.carrier). g.mult (g.inv x) x = g.id``, 626 RW_TAC resq_ss [Group_def, GSPECIFICATION]); 627 628val context = subtypeTools.add_rewrite2 group_linv context; 629val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 630 631val group_assoc = store_thm 632 ("group_assoc", 633 ``!g :: Group. !x y z :: (g.carrier). 634 g.mult (g.mult x y) z = g.mult x (g.mult y z)``, 635 RW_TAC resq_ss [Group_def, GSPECIFICATION]); 636 637val context = subtypeTools.add_rewrite2'' group_assoc context; 638val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 639 640val group_comm = store_thm 641 ("group_comm", 642 ``!g :: AbelianGroup. !x y :: (g.carrier). g.mult x y = g.mult y x``, 643 RW_TAC resq_ss [AbelianGroup_def, GSPECIFICATION]); 644 645val group_comm' = store_thm 646 ("group_comm'", 647 ``!g :: AbelianGroup. !x y z :: (g.carrier). 648 g.mult x (g.mult y z) = g.mult y (g.mult x z)``, 649 RW_TAC resq_ss [] 650 ++ RW_TAC alg_ss [GSYM group_assoc] 651 ++ METIS_TAC [group_comm]); 652 653val group_rinv = store_thm 654 ("group_rinv", 655 ``!g :: Group. !x :: (g.carrier). g.mult x (g.inv x) = g.id``, 656 RW_TAC resq_ss [] 657 ++ MATCH_MP_TAC EQ_TRANS 658 ++ Q.EXISTS_TAC `g.mult g.id (g.mult x (g.inv x))` 659 ++ CONJ_TAC 660 >> (match_tac (GSYM group_lid) 661 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]) 662 ++ MATCH_MP_TAC EQ_TRANS 663 ++ Q.EXISTS_TAC 664 `g.mult (g.mult (g.inv (g.inv x)) (g.inv x)) (g.mult x (g.inv x))` 665 ++ CONJ_TAC 666 >> (REPEAT (AP_TERM_TAC || AP_THM_TAC) 667 ++ match_tac (GSYM group_linv) 668 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]) 669 ++ MATCH_MP_TAC EQ_TRANS 670 ++ Q.EXISTS_TAC 671 `g.mult (g.inv (g.inv x)) (g.mult (g.inv x) (g.mult x (g.inv x)))` 672 ++ CONJ_TAC 673 >> (match_tac group_assoc 674 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]) 675 ++ MATCH_MP_TAC EQ_TRANS 676 ++ Q.EXISTS_TAC 677 `g.mult (g.inv (g.inv x)) (g.mult (g.mult (g.inv x) x) (g.inv x))` 678 ++ CONJ_TAC 679 >> (AP_TERM_TAC 680 ++ match_tac (GSYM group_assoc) 681 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]) 682 ++ MATCH_MP_TAC EQ_TRANS 683 ++ Q.EXISTS_TAC `g.mult (g.inv (g.inv x)) (g.mult g.id (g.inv x))` 684 ++ CONJ_TAC 685 >> (REPEAT (AP_TERM_TAC || AP_THM_TAC) 686 ++ match_tac group_linv 687 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]) 688 ++ MATCH_MP_TAC EQ_TRANS 689 ++ Q.EXISTS_TAC `g.mult (g.inv (g.inv x)) (g.inv x)` 690 ++ CONJ_TAC 691 >> (REPEAT (AP_TERM_TAC || AP_THM_TAC) 692 ++ match_tac group_lid 693 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]) 694 ++ match_tac group_linv 695 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]); 696 697val context = subtypeTools.add_rewrite2 group_rinv context; 698val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 699 700val group_rid = store_thm 701 ("group_rid", 702 ``!g :: Group. !x :: (g.carrier). g.mult x g.id = x``, 703 RW_TAC resq_ss [] 704 ++ MATCH_MP_TAC EQ_TRANS 705 ++ Q.EXISTS_TAC `g.mult x (g.mult (g.inv x) x)` 706 ++ CONJ_TAC 707 >> (REPEAT (AP_TERM_TAC || AP_THM_TAC) 708 ++ match_tac (GSYM group_linv) 709 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]) 710 ++ MATCH_MP_TAC EQ_TRANS 711 ++ Q.EXISTS_TAC `g.mult (g.mult x (g.inv x)) x` 712 ++ CONJ_TAC 713 >> (match_tac (GSYM group_assoc) 714 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]) 715 ++ MATCH_MP_TAC EQ_TRANS 716 ++ Q.EXISTS_TAC `g.mult g.id x` 717 ++ CONJ_TAC 718 >> (REPEAT (AP_TERM_TAC || AP_THM_TAC) 719 ++ match_tac group_rinv 720 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]) 721 ++ match_tac group_lid 722 ++ METIS_TAC [group_inv_carrier, group_mult_carrier]); 723 724val context = subtypeTools.add_rewrite2 group_rid context; 725val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 726 727val group_lcancel = store_thm 728 ("group_lcancel", 729 ``!g :: Group. !x y z :: (g.carrier). (g.mult x y = g.mult x z) = (y = z)``, 730 RW_TAC resq_ss [] 731 ++ REVERSE EQ_TAC >> RW_TAC std_ss [] 732 ++ RW_TAC std_ss [] 733 ++ Suff `g.mult g.id y = g.mult g.id z` 734 >> METIS_TAC [group_lid] 735 ++ Suff `g.mult (g.mult (g.inv x) x) y = g.mult (g.mult (g.inv x) x) z` 736 >> METIS_TAC [group_linv] 737 ++ MATCH_MP_TAC EQ_TRANS 738 ++ Q.EXISTS_TAC `g.mult (g.inv x) (g.mult x y)` 739 ++ CONJ_TAC 740 >> (match_tac group_assoc ++ METIS_TAC [group_inv_carrier]) 741 ++ MATCH_MP_TAC EQ_TRANS 742 ++ Q.EXISTS_TAC `g.mult (g.inv x) (g.mult x z)` 743 ++ REVERSE CONJ_TAC 744 >> (match_tac (GSYM group_assoc) ++ METIS_TAC [group_inv_carrier]) 745 ++ RW_TAC std_ss []); 746 747val context = subtypeTools.add_rewrite2' group_lcancel context; 748val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 749 750val group_lcancel_imp = store_thm 751 ("group_lcancel_imp", 752 ``!g :: Group. !x y z :: (g.carrier). 753 (g.mult x y = g.mult x z) ==> (y = z)``, 754 METIS_TAC [group_lcancel]); 755 756val group_lcancel_id = store_thm 757 ("group_lcancel_id", 758 ``!g :: Group. !x y :: (g.carrier). (g.mult x y = x) = (y = g.id)``, 759 RW_TAC resq_ss [] 760 ++ MATCH_MP_TAC EQ_TRANS 761 ++ Q.EXISTS_TAC `g.mult x y = g.mult x g.id` 762 ++ CONJ_TAC 763 >> RW_TAC std_ss [group_rid] 764 ++ match_tac group_lcancel 765 ++ RW_TAC std_ss [group_id_carrier]); 766 767val context = subtypeTools.add_rewrite2' group_lcancel_id context; 768val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 769 770val group_lcancel_id_imp = store_thm 771 ("group_lcancel_id_imp", 772 ``!g :: Group. !x y :: (g.carrier). (g.mult x y = x) ==> (y = g.id)``, 773 METIS_TAC [group_lcancel_id]); 774 775val group_lcancel_id_imp' = store_thm 776 ("group_lcancel_id_imp'", 777 ``!g :: Group. !x y :: (g.carrier). (y = g.id) ==> (g.mult x y = x)``, 778 METIS_TAC [group_lcancel_id]); 779 780val group_rcancel = store_thm 781 ("group_rcancel", 782 ``!g :: Group. !x y z :: (g.carrier). (g.mult y x = g.mult z x) = (y = z)``, 783 RW_TAC resq_ss [] 784 ++ REVERSE EQ_TAC >> RW_TAC std_ss [] 785 ++ RW_TAC std_ss [] 786 ++ Suff `g.mult y g.id = g.mult z g.id` 787 >> METIS_TAC [group_rid] 788 ++ Suff `g.mult y (g.mult x (g.inv x)) = g.mult z (g.mult x (g.inv x))` 789 >> METIS_TAC [group_rinv] 790 ++ MATCH_MP_TAC EQ_TRANS 791 ++ Q.EXISTS_TAC `g.mult (g.mult y x) (g.inv x)` 792 ++ CONJ_TAC 793 >> (match_tac (GSYM group_assoc) ++ METIS_TAC [group_inv_carrier]) 794 ++ MATCH_MP_TAC EQ_TRANS 795 ++ Q.EXISTS_TAC `g.mult (g.mult z x) (g.inv x)` 796 ++ REVERSE CONJ_TAC 797 >> (match_tac group_assoc ++ METIS_TAC [group_inv_carrier]) 798 ++ RW_TAC std_ss []); 799 800val context = subtypeTools.add_rewrite2' group_rcancel context; 801val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 802 803val group_rcancel_imp = store_thm 804 ("group_rcancel_imp", 805 ``!g :: Group. !x y z :: (g.carrier). 806 (g.mult y x = g.mult z x) ==> (y = z)``, 807 METIS_TAC [group_rcancel]); 808 809val group_rcancel_id = store_thm 810 ("group_rcancel_id", 811 ``!g :: Group. !x y :: (g.carrier). (g.mult y x = x) = (y = g.id)``, 812 RW_TAC resq_ss [] 813 ++ MATCH_MP_TAC EQ_TRANS 814 ++ Q.EXISTS_TAC `g.mult y x = g.mult g.id x` 815 ++ CONJ_TAC 816 >> RW_TAC std_ss [group_lid] 817 ++ match_tac group_rcancel 818 ++ RW_TAC std_ss [group_id_carrier]); 819 820val context = subtypeTools.add_rewrite2' group_rcancel_id context; 821val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 822 823val group_rcancel_id_imp = store_thm 824 ("group_rcancel_id_imp", 825 ``!g :: Group. !x y :: (g.carrier). (g.mult y x = x) ==> (y = g.id)``, 826 METIS_TAC [group_rcancel_id]); 827 828val group_rcancel_id_imp' = store_thm 829 ("group_rcancel_id_imp'", 830 ``!g :: Group. !x y :: (g.carrier). (y = g.id) ==> (g.mult y x = x)``, 831 METIS_TAC [group_rcancel_id]); 832 833val group_inv_cancel_imp = store_thm 834 ("group_inv_cancel_imp", 835 ``!g :: Group. !x y :: (g.carrier). (g.inv x = g.inv y) ==> (x = y)``, 836 RW_TAC resq_ss [] 837 ++ match_tac group_lcancel_imp 838 ++ Q.EXISTS_TAC `g` 839 ++ Q.EXISTS_TAC `g.inv x` 840 ++ RW_TAC std_ss [group_inv_carrier] 841 ++ METIS_TAC [group_linv]); 842 843val group_inv_cancel = store_thm 844 ("group_inv_cancel", 845 ``!g :: Group. !x y :: (g.carrier). (g.inv x = g.inv y) = (x = y)``, 846 METIS_TAC [group_inv_cancel_imp]); 847 848val context = subtypeTools.add_rewrite2' group_inv_cancel context; 849val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 850 851val group_inv_inv = store_thm 852 ("group_inv_inv", 853 ``!g :: Group. !x :: (g.carrier). g.inv (g.inv x) = x``, 854 RW_TAC resq_ss [] 855 ++ match_tac group_lcancel_imp 856 ++ Q.EXISTS_TAC `g` 857 ++ Q.EXISTS_TAC `g.inv x` 858 ++ RW_TAC std_ss [group_inv_carrier] 859 ++ METIS_TAC [group_inv_carrier, group_linv, group_rinv]); 860 861val context = subtypeTools.add_rewrite2 group_inv_inv context; 862val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 863 864val group_inv_eq_swap_imp = store_thm 865 ("group_inv_eq_swap_imp", 866 ``!g :: Group. !x y :: (g.carrier). (g.inv x = y) ==> (x = g.inv y)``, 867 METIS_TAC [group_inv_inv]); 868 869val group_inv_eq_swap = store_thm 870 ("group_inv_eq_swap", 871 ``!g :: Group. !x y :: (g.carrier). (g.inv x = y) = (x = g.inv y)``, 872 METIS_TAC [group_inv_eq_swap_imp]); 873 874val group_inv_eq_swap_imp' = store_thm 875 ("group_inv_eq_swap_imp'", 876 ``!g :: Group. !x y :: (g.carrier). (x = g.inv y) ==> (g.inv x = y)``, 877 METIS_TAC [group_inv_eq_swap]); 878 879val group_inv_id = store_thm 880 ("group_inv_id", 881 ``!g :: Group. g.inv g.id = g.id``, 882 RW_TAC resq_ss [] 883 ++ match_tac group_lcancel_imp 884 ++ Q.EXISTS_TAC `g` 885 ++ Q.EXISTS_TAC `g.id` 886 ++ RW_TAC std_ss [group_inv_carrier, group_id_carrier, group_rinv] 887 ++ RW_TAC std_ss [group_lid, group_id_carrier]); 888 889val context = subtypeTools.add_rewrite2 group_inv_id context; 890val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 891 892val group_inv_eq_imp = store_thm 893 ("group_inv_eq_imp", 894 ``!g :: Group. !x y :: (g.carrier). (g.inv x = y) ==> (g.mult x y = g.id)``, 895 RW_TAC resq_ss [group_rinv]); 896 897val group_inv_eq_imp' = store_thm 898 ("group_inv_eq_imp'", 899 ``!g :: Group. !x y :: (g.carrier). (g.mult x y = g.id) ==> (g.inv x = y)``, 900 RW_TAC resq_ss [] 901 ++ match_tac group_lcancel_imp 902 ++ Q.EXISTS_TAC `g` 903 ++ Q.EXISTS_TAC `x` 904 ++ RW_TAC std_ss [group_inv_carrier, group_rinv]); 905 906val group_inv_eq = store_thm 907 ("group_inv_eq", 908 ``!g :: Group. !x y :: (g.carrier). (g.inv x = y) = (g.mult x y = g.id)``, 909 METIS_TAC [group_inv_eq_imp, group_inv_eq_imp']); 910 911val group_inv_mult = store_thm 912 ("group_inv_mult", 913 ``!g :: Group. !x y :: (g.carrier). 914 g.inv (g.mult x y) = g.mult (g.inv y) (g.inv x)``, 915 RW_TAC resq_ss [] 916 ++ match_tac group_inv_eq_imp' 917 ++ RW_TAC std_ss [group_mult_carrier, group_inv_carrier] 918 ++ MATCH_MP_TAC EQ_TRANS 919 ++ Q.EXISTS_TAC `g.mult x (g.mult y (g.mult (g.inv y) (g.inv x)))` 920 ++ CONJ_TAC 921 >> (match_tac group_assoc 922 ++ METIS_TAC [group_mult_carrier, group_inv_carrier]) 923 ++ MATCH_MP_TAC EQ_TRANS 924 ++ Q.EXISTS_TAC `g.mult x (g.mult (g.mult y (g.inv y)) (g.inv x))` 925 ++ CONJ_TAC 926 >> (AP_TERM_TAC 927 ++ match_tac (GSYM group_assoc) 928 ++ METIS_TAC [group_mult_carrier, group_inv_carrier]) 929 ++ RW_TAC std_ss [group_rinv, group_lid, group_inv_carrier]); 930 931val context = subtypeTools.add_rewrite2'' group_inv_mult context; 932val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 933 934val group_exp_carrier = store_thm 935 ("group_exp_carrier", 936 ``!g :: Group. !x :: (g.carrier). !n. group_exp g x n IN g.carrier``, 937 RW_TAC resq_ss [] 938 ++ Induct_on `n` 939 ++ RW_TAC std_ss [group_exp_def] 940 ++ METIS_TAC [group_id_carrier, group_mult_carrier]); 941 942val context = subtypeTools.add_reduction2 group_exp_carrier context; 943val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 944 945val group_id_exp = store_thm 946 ("group_id_exp", 947 ``!g :: Group. !n. group_exp g g.id n = g.id``, 948 RW_TAC resq_ss [] 949 ++ Induct_on `n` 950 ++ RW_TAC std_ss [group_exp_def, group_lid, group_id_carrier]); 951 952val context = subtypeTools.add_rewrite2 group_id_exp context; 953val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 954 955val group_comm_exp = store_thm 956 ("group_comm_exp", 957 ``!g :: Group. !x y :: (g.carrier). !n. 958 (g.mult x y = g.mult y x) ==> 959 (g.mult (group_exp g x n) y = g.mult y (group_exp g x n))``, 960 RW_TAC resq_ss [] 961 ++ Induct_on `n` 962 ++ RW_TAC std_ss [group_exp_def, group_lid, group_rid] 963 ++ MATCH_MP_TAC EQ_TRANS 964 ++ Q.EXISTS_TAC `g.mult x (g.mult (group_exp g x n) y)` 965 ++ CONJ_TAC 966 >> (match_tac group_assoc 967 ++ METIS_TAC [group_mult_carrier, group_exp_carrier]) 968 ++ RW_TAC std_ss [] 969 ++ MATCH_MP_TAC EQ_TRANS 970 ++ Q.EXISTS_TAC `g.mult (g.mult x y) (group_exp g x n)` 971 ++ CONJ_TAC 972 >> (match_tac (GSYM group_assoc) 973 ++ METIS_TAC [group_mult_carrier, group_exp_carrier]) 974 ++ MATCH_MP_TAC EQ_TRANS 975 ++ Q.EXISTS_TAC `g.mult (g.mult y x) (group_exp g x n)` 976 ++ REVERSE CONJ_TAC 977 >> (match_tac group_assoc 978 ++ METIS_TAC [group_mult_carrier, group_exp_carrier]) 979 ++ ASM_REWRITE_TAC []); 980 981val group_exp_comm = store_thm 982 ("group_exp_comm", 983 ``!g :: Group. !x :: (g.carrier). !n. 984 g.mult (group_exp g x n) x = g.mult x (group_exp g x n)``, 985 RW_TAC resq_ss [] 986 ++ match_tac group_comm_exp 987 ++ RW_TAC std_ss []); 988 989val group_mult_exp = store_thm 990 ("group_mult_exp", 991 ``!g :: Group. !x y :: (g.carrier). !n. 992 (g.mult x y = g.mult y x) ==> 993 (group_exp g (g.mult x y) n = 994 g.mult (group_exp g x n) (group_exp g y n))``, 995 RW_TAC resq_ss [] 996 ++ Induct_on `n` 997 ++ RW_TAC std_ss 998 [group_exp_def, group_exp_carrier, group_lid, group_id_carrier] 999 ++ MATCH_MP_TAC EQ_TRANS 1000 ++ Q.EXISTS_TAC 1001 `g.mult x (g.mult y (g.mult (group_exp g x n) (group_exp g y n)))` 1002 ++ CONJ_TAC 1003 >> (match_tac group_assoc 1004 ++ METIS_TAC [group_mult_carrier, group_exp_carrier]) 1005 ++ MATCH_MP_TAC EQ_TRANS 1006 ++ Q.EXISTS_TAC 1007 `g.mult x (g.mult (group_exp g x n) (g.mult y (group_exp g y n)))` 1008 ++ REVERSE CONJ_TAC 1009 >> (match_tac (GSYM group_assoc) 1010 ++ METIS_TAC [group_mult_carrier, group_exp_carrier]) 1011 ++ AP_TERM_TAC 1012 ++ MATCH_MP_TAC EQ_TRANS 1013 ++ Q.EXISTS_TAC `g.mult (g.mult y (group_exp g x n)) (group_exp g y n)` 1014 ++ CONJ_TAC 1015 >> (match_tac (GSYM group_assoc) 1016 ++ METIS_TAC [group_mult_carrier, group_exp_carrier]) 1017 ++ MATCH_MP_TAC EQ_TRANS 1018 ++ Q.EXISTS_TAC `g.mult (g.mult (group_exp g x n) y) (group_exp g y n)` 1019 ++ REVERSE CONJ_TAC 1020 >> (match_tac group_assoc 1021 ++ METIS_TAC [group_mult_carrier, group_exp_carrier]) 1022 ++ AP_THM_TAC 1023 ++ AP_TERM_TAC 1024 ++ match_tac (GSYM group_comm_exp) 1025 ++ METIS_TAC []); 1026 1027val group_exp_add = store_thm 1028 ("group_exp_add", 1029 ``!g :: Group. !x :: (g.carrier). !m n. 1030 group_exp g x (m + n) = g.mult (group_exp g x m) (group_exp g x n)``, 1031 RW_TAC resq_ss [] 1032 ++ Induct_on `m` 1033 ++ RW_TAC std_ss [group_exp_def, group_lid, group_exp_carrier, ADD] 1034 ++ match_tac (GSYM group_assoc) 1035 ++ RW_TAC std_ss [group_exp_carrier]); 1036 1037val group_exp_mult = store_thm 1038 ("group_exp_mult", 1039 ``!g :: Group. !x :: (g.carrier). !m n. 1040 group_exp g x (m * n) = group_exp g (group_exp g x m) n``, 1041 RW_TAC resq_ss [] 1042 ++ Induct_on `m` 1043 ++ RW_TAC std_ss [group_exp_def, group_id_exp, group_exp_carrier, MULT] 1044 ++ ONCE_REWRITE_TAC [ADD_COMM] 1045 ++ RW_TAC std_ss [group_exp_carrier, group_exp_add] 1046 ++ MATCH_MP_TAC EQ_SYM 1047 ++ match_tac group_mult_exp 1048 ++ RW_TAC std_ss [group_exp_carrier] 1049 ++ match_tac (GSYM group_exp_comm) 1050 ++ METIS_TAC []); 1051 1052val group_id_alt = store_thm 1053 ("group_id_alt", 1054 ``!g :: Group. !x :: (g.carrier). (g.mult x x = x) = (x = g.id)``, 1055 RW_TAC alg_ss []); 1056 1057val group_ac_conv = 1058 {name = "group_ac_conv", 1059 key = ``g.mult x y``, 1060 conv = subtypeTools.binop_ac_conv 1061 {term_compare = compare, 1062 dest_binop = dest_group_mult, 1063 dest_inv = dest_group_inv, 1064 dest_exp = dest_group_exp, 1065 assoc_th = group_assoc, 1066 comm_th = group_comm, 1067 comm_th' = group_comm', 1068 id_ths = [], 1069 simplify_ths = [], 1070 combine_ths = [], 1071 combine_ths' = []}}; 1072 1073val context = subtypeTools.add_conversion2'' group_ac_conv context; 1074val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1075 1076val group_exp_eval = store_thm 1077 ("group_exp_eval", 1078 ``!g :: Group. !x :: (g.carrier). !n. 1079 group_exp g x n = 1080 if n = 0 then g.id 1081 else 1082 let x' = g.mult x x in 1083 let n' = n DIV 2 in 1084 if EVEN n then group_exp g x' n' else g.mult x (group_exp g x' n')``, 1085 RW_TAC resq_ss [LET_DEF] 1086 ++ RW_TAC alg_ss [group_exp_def, group_mult_exp, GSYM group_exp_add] 1087 ++ RW_TAC alg_ss [GSYM group_exp_def] 1088 ++ REPEAT AP_TERM_TAC 1089 ++ MP_TAC (Q.SPEC `2` DIVISION) 1090 ++ SIMP_TAC alg_ss [MOD_2] 1091 ++ DISCH_THEN (MP_TAC o Q.SPEC `n`) 1092 ++ RW_TAC std_ss [] 1093 ++ DECIDE_TAC); 1094 1095(* ------------------------------------------------------------------------- *) 1096(* Homomorphisms, isomorphisms, endomorphisms, automorphisms and subgroups. *) 1097(* ------------------------------------------------------------------------- *) 1098 1099val GroupHom_def = Define 1100 `GroupHom g h = 1101 { f | 1102 (!x :: (g.carrier). f x IN h.carrier) /\ 1103 (f (g.id) = h.id) /\ 1104 (!x :: (g.carrier). f (g.inv x) = h.inv (f x)) /\ 1105 (!x y :: (g.carrier). f (g.mult x y) = h.mult (f x) (f y)) }`; 1106 1107val GroupIso_def = Define 1108 `GroupIso g h = 1109 { f | 1110 f IN GroupHom g h /\ 1111 (!y :: (h.carrier). ?!x :: (g.carrier). f x = y) }`; 1112 1113val GroupEndo_def = Define `GroupEndo g = GroupHom g g`; 1114 1115val GroupAuto_def = Define `GroupAuto g = GroupIso g g`; 1116 1117val subgroup_def = Define `subgroup g h = I IN GroupHom g h`; 1118 1119(* ------------------------------------------------------------------------- *) 1120(* The trivial group. *) 1121(* ------------------------------------------------------------------------- *) 1122 1123val trivial_group_def = Define 1124 `trivial_group e : 'a group = 1125 <| carrier := {e}; id := e; inv := (\x. e); mult := (\x y. e) |>`; 1126 1127val trivial_group = store_thm 1128 ("trivial_group", 1129 ``!e. trivial_group e IN FiniteAbelianGroup``, 1130 RW_TAC resq_ss 1131 [FiniteAbelianGroup_def, GSPECIFICATION, FiniteGroup_def, Group_def, 1132 AbelianGroup_def, trivial_group_def, FINITE_INSERT, FINITE_EMPTY, 1133 IN_INSERT, NOT_IN_EMPTY, combinTheory.K_THM]); 1134 1135val context = subtypeTools.add_reduction2 trivial_group context; 1136val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1137 1138(* ------------------------------------------------------------------------- *) 1139(* The cyclic group. *) 1140(* ------------------------------------------------------------------------- *) 1141 1142val cyclic_group_def = Define 1143 `cyclic_group e f : 'a group = 1144 <| carrier := { x | ?n. FUNPOW f n e = x }; 1145 id := e; 1146 inv := (\x. @y. ?yi. !xi. 1147 (FUNPOW f yi e = y) /\ 1148 ((FUNPOW f xi e = x) ==> (FUNPOW f (xi + yi) e = e))); 1149 mult := (\x y. @z. !xi yi. 1150 (FUNPOW f xi e = x) /\ (FUNPOW f yi e = y) ==> 1151 (FUNPOW f (xi + yi) e = z)) |>`; 1152 1153val cyclic_group_alt = store_thm 1154 ("cyclic_group_alt", 1155 ``!e f n. 1156 (?k. ~(k = 0) /\ (FUNPOW f k e = e)) /\ 1157 (n = LEAST k. ~(k = 0) /\ (FUNPOW f k e = e)) ==> 1158 ((cyclic_group e f).carrier = { FUNPOW f k e | k < n }) /\ 1159 ((cyclic_group e f).id = e) /\ 1160 (!i. 1161 (cyclic_group e f).inv (FUNPOW f i e) = 1162 FUNPOW f ((n - i MOD n) MOD n) e) /\ 1163 (!i j. 1164 (cyclic_group e f).mult (FUNPOW f i e) (FUNPOW f j e) = 1165 FUNPOW f ((i + j) MOD n) e)``, 1166 REPEAT GEN_TAC 1167 ++ SIMP_TAC std_ss [whileTheory.LEAST_EXISTS] 1168 ++ Q.SPEC_TAC (`LEAST k. ~(k = 0) /\ (FUNPOW f k e = e)`,`k`) 1169 ++ GEN_TAC 1170 ++ STRIP_TAC 1171 ++ Know `0 < k` >> DECIDE_TAC 1172 ++ STRIP_TAC 1173 ++ Know `!p q. (FUNPOW f p e = FUNPOW f q e) = (p MOD k = q MOD k)` 1174 >> (REPEAT STRIP_TAC 1175 ++ MP_TAC (Q.SPEC `k` DIVISION) 1176 ++ ASM_SIMP_TAC std_ss [] 1177 ++ DISCH_THEN (fn th => MP_TAC (Q.SPEC `p` th) ++ MP_TAC (Q.SPEC `q` th)) 1178 ++ DISCH_THEN (fn th1 => DISCH_THEN (fn th2 => 1179 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th1,th2])))) 1180 ++ ONCE_REWRITE_TAC [ONCE_REWRITE_RULE [ADD_COMM] FUNPOW_ADD] 1181 ++ ONCE_REWRITE_TAC [ONCE_REWRITE_RULE [MULT_COMM] FUNPOW_MULT] 1182 ++ Know `!n. FUNPOW (\x. FUNPOW f k x) n e = e` 1183 >> (Induct ++ RW_TAC std_ss [FUNPOW]) 1184 ++ DISCH_THEN (fn th => RW_TAC std_ss [th]) 1185 ++ REVERSE EQ_TAC >> RW_TAC std_ss [] 1186 ++ STRIP_TAC 1187 ++ Know `!m n : num. ~(m < n) /\ ~(n < m) ==> (m = n)` >> DECIDE_TAC 1188 ++ DISCH_THEN MATCH_MP_TAC 1189 ++ POP_ASSUM MP_TAC 1190 ++ MATCH_MP_TAC 1191 (PROVE [] 1192 ``((a = b) ==> ~c) /\ ((b = a) ==> ~d) ==> ((a = b) ==> ~c /\ ~d)``) 1193 ++ Q.SPEC_TAC (`q`,`q`) 1194 ++ Q.SPEC_TAC (`p`,`p`) 1195 ++ SIMP_TAC std_ss [FORALL_AND_THM] 1196 ++ MATCH_MP_TAC (PROVE [] ``(a ==> b) /\ a ==> a /\ b``) 1197 ++ CONJ_TAC >> METIS_TAC [] 1198 ++ RW_TAC std_ss [] 1199 ++ STRIP_TAC 1200 ++ Q.PAT_ASSUM `!n. P n` (MP_TAC o Q.SPEC `(k - q MOD k) + p MOD k`) 1201 ++ ASM_SIMP_TAC std_ss [FUNPOW_ADD] 1202 ++ SIMP_TAC std_ss [GSYM FUNPOW_ADD] 1203 ++ MP_TAC (Q.SPEC `k` DIVISION) 1204 ++ ASM_REWRITE_TAC [] 1205 ++ DISCH_THEN (ASSUME_TAC o CONJUNCT2 o Q.SPEC `q`) 1206 ++ ASM_SIMP_TAC arith_ss []) 1207 ++ RW_TAC resq_ss 1208 [cyclic_group_def, combinTheory.K_THM, GSPECIFICATION, EXTENSION] 1209 << [REVERSE EQ_TAC >> METIS_TAC [] 1210 ++ RW_TAC std_ss [] 1211 ++ Q.EXISTS_TAC `n MOD k` 1212 ++ METIS_TAC [DIVISION, MOD_MOD], 1213 normalForms.SELECT_TAC 1214 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 1215 ++ CONJ_TAC 1216 >> (Q.EXISTS_TAC `FUNPOW f (k - i MOD k) e` 1217 ++ Q.EXISTS_TAC `k - i MOD k` 1218 ++ RW_TAC std_ss [] 1219 ++ Know `e = FUNPOW f 0 e` >> RW_TAC std_ss [FUNPOW] 1220 ++ DISCH_THEN 1221 (fn th => CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV [th]))) 1222 ++ RW_TAC std_ss [] 1223 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1224 ++ ASM_REWRITE_TAC [] 1225 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 1226 ++ RW_TAC std_ss [] 1227 ++ MP_TAC (Q.SPEC `k` MOD_MOD) 1228 ++ ASM_REWRITE_TAC [] 1229 ++ DISCH_THEN (fn th => 1230 CONV_TAC 1231 (LAND_CONV 1232 (LAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [GSYM th]))))) 1233 ++ ASM_SIMP_TAC std_ss [MOD_PLUS] 1234 ++ Know `i MOD k < k` >> METIS_TAC [DIVISION] 1235 ++ STRIP_TAC 1236 ++ RW_TAC arith_ss []) 1237 ++ RW_TAC std_ss [] 1238 ++ POP_ASSUM (MP_TAC o Q.SPEC `i`) 1239 ++ RW_TAC std_ss [] 1240 ++ RW_TAC std_ss [] 1241 ++ MP_TAC (Q.SPEC `k` MOD_MOD) 1242 ++ ASM_REWRITE_TAC [] 1243 ++ DISCH_THEN 1244 (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [GSYM th]))) 1245 ++ Know `!a. a = 0 MOD k + a` >> RW_TAC arith_ss [ZERO_MOD] 1246 ++ DISCH_THEN 1247 (fn th => 1248 CONV_TAC (RAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [th])))) 1249 ++ POP_ASSUM MP_TAC 1250 ++ Know `FUNPOW f 0 e = e` >> RW_TAC std_ss [FUNPOW] 1251 ++ DISCH_THEN 1252 (fn th => 1253 CONV_TAC (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV [GSYM th])))) 1254 ++ ASM_REWRITE_TAC [] 1255 ++ Q.UNDISCH_TAC `0 < k` 1256 ++ POP_ASSUM_LIST (K ALL_TAC) 1257 ++ STRIP_TAC 1258 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1259 ++ ASM_REWRITE_TAC [] 1260 ++ DISCH_THEN 1261 (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [GSYM th]))) 1262 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 1263 ++ MP_TAC (Q.SPEC `k` MOD_MOD) 1264 ++ ASM_REWRITE_TAC [] 1265 ++ DISCH_THEN (fn th => 1266 CONV_TAC 1267 (RAND_CONV 1268 (LAND_CONV 1269 (LAND_CONV 1270 (LAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [GSYM th]))))))) 1271 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1272 ++ ASM_REWRITE_TAC [] 1273 ++ DISCH_THEN (fn th => CONV_TAC (ONCE_REWRITE_CONV [th])) 1274 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1275 ++ ASM_REWRITE_TAC [] 1276 ++ DISCH_THEN (fn th => CONV_TAC (ONCE_REWRITE_CONV [GSYM th])) 1277 ++ MP_TAC (Q.SPEC `k` MOD_MOD) 1278 ++ ASM_REWRITE_TAC [] 1279 ++ DISCH_THEN (fn th => CONV_TAC (REWRITE_CONV [th])) 1280 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1281 ++ ASM_REWRITE_TAC [] 1282 ++ DISCH_THEN (fn th => CONV_TAC (ONCE_REWRITE_CONV [th])) 1283 ++ Know `i MOD k < k` >> METIS_TAC [DIVISION] 1284 ++ STRIP_TAC 1285 ++ RW_TAC arith_ss [] 1286 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1287 ++ ASM_REWRITE_TAC [] 1288 ++ DISCH_THEN (fn th => CONV_TAC (ONCE_REWRITE_CONV [GSYM th])) 1289 ++ RW_TAC arith_ss [DIVMOD_ID], 1290 normalForms.SELECT_TAC 1291 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 1292 ++ CONJ_TAC 1293 >> (Q.EXISTS_TAC `FUNPOW f (i + j) e` 1294 ++ RW_TAC std_ss [] 1295 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1296 ++ ASM_REWRITE_TAC [] 1297 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 1298 ++ RW_TAC std_ss []) 1299 ++ RW_TAC std_ss [] 1300 ++ POP_ASSUM (MP_TAC o Q.SPECL [`i`,`j`]) 1301 ++ RW_TAC std_ss [] 1302 ++ RW_TAC std_ss [] 1303 ++ METIS_TAC [DIVISION]]); 1304 1305val cyclic_group = store_thm 1306 ("cyclic_group", 1307 ``!e f. 1308 (?n. ~(n = 0) /\ (FUNPOW f n e = e)) ==> 1309 cyclic_group e f IN FiniteAbelianGroup``, 1310 REPEAT GEN_TAC 1311 ++ DISCH_THEN ASSUME_TAC 1312 ++ MP_TAC (Q.SPECL [`e`,`f`,`LEAST n. ~(n = 0) /\ (FUNPOW f n e = e)`] 1313 cyclic_group_alt) 1314 ++ MATCH_MP_TAC (PROVE [] ``a /\ (b ==> c) ==> ((a ==> b) ==> c)``) 1315 ++ CONJ_TAC >> (RW_TAC std_ss [] ++ METIS_TAC []) 1316 ++ POP_ASSUM MP_TAC 1317 ++ SIMP_TAC std_ss [whileTheory.LEAST_EXISTS] 1318 ++ Q.SPEC_TAC (`LEAST n. ~(n = 0) /\ (FUNPOW f n e = e)`,`k`) 1319 ++ REPEAT GEN_TAC 1320 ++ STRIP_TAC 1321 ++ Know `0 < k` >> DECIDE_TAC 1322 ++ STRIP_TAC 1323 ++ (RW_TAC resq_ss [FiniteAbelianGroup_alt, Group_def, GSPECIFICATION] 1324 ++ RW_TAC std_ss []) 1325 << [Q.EXISTS_TAC `0` 1326 ++ RW_TAC arith_ss [FUNPOW], 1327 METIS_TAC [DIVISION], 1328 Q.EXISTS_TAC `(k - k' MOD k) MOD k` 1329 ++ RW_TAC arith_ss [FUNPOW] 1330 ++ METIS_TAC [DIVISION], 1331 Know `FUNPOW f 0 e = e` >> RW_TAC std_ss [FUNPOW] 1332 ++ DISCH_THEN (fn th => 1333 CONV_TAC (LAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [GSYM th])))) 1334 ++ RW_TAC std_ss [] 1335 ++ RW_TAC arith_ss [], 1336 Suff `((k - k' MOD k) MOD k + k') MOD k = 0 MOD k` 1337 >> RW_TAC std_ss [ZERO_MOD, FUNPOW] 1338 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1339 ++ ASM_REWRITE_TAC [] 1340 ++ DISCH_THEN 1341 (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [GSYM th] 1342 THENC ONCE_REWRITE_CONV [GSYM th]))) 1343 ++ MP_TAC (Q.SPEC `k` MOD_MOD) 1344 ++ ASM_REWRITE_TAC [] 1345 ++ DISCH_THEN (fn th => 1346 CONV_TAC (LAND_CONV (LAND_CONV (LAND_CONV (REWRITE_CONV [th]))))) 1347 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1348 ++ ASM_REWRITE_TAC [] 1349 ++ DISCH_THEN (fn th => CONV_TAC (ONCE_REWRITE_CONV [th])) 1350 ++ Know `k' MOD k < k` >> METIS_TAC [DIVISION] 1351 ++ RW_TAC arith_ss [], 1352 AP_THM_TAC 1353 ++ AP_TERM_TAC 1354 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1355 ++ ASM_REWRITE_TAC [] 1356 ++ DISCH_THEN 1357 (fn th => CONV_TAC (BINOP_CONV 1358 (LAND_CONV (ONCE_REWRITE_CONV [GSYM th]) 1359 THENC ONCE_REWRITE_CONV [GSYM th]))) 1360 ++ MP_TAC (Q.SPEC `k` MOD_MOD) 1361 ++ ASM_REWRITE_TAC [] 1362 ++ DISCH_THEN (fn th => 1363 CONV_TAC 1364 (LAND_CONV (LAND_CONV (RAND_CONV (ONCE_REWRITE_CONV [GSYM th]))) 1365 THENC 1366 RAND_CONV (LAND_CONV (LAND_CONV (ONCE_REWRITE_CONV [GSYM th]))))) 1367 ++ MP_TAC (Q.SPEC `k` MOD_PLUS) 1368 ++ ASM_REWRITE_TAC [] 1369 ++ METIS_TAC [ADD_ASSOC], 1370 METIS_TAC [ADD_COMM], 1371 Know `{FUNPOW f k' e | k' < k} = 1372 IMAGE (\k'. FUNPOW f k' e) {k' | k' < k}` 1373 >> RW_TAC std_ss [IMAGE_DEF, GSPECIFICATION] 1374 ++ RW_TAC std_ss [] 1375 ++ MATCH_MP_TAC IMAGE_FINITE 1376 ++ RW_TAC std_ss [finite_num] 1377 ++ Q.EXISTS_TAC `k` 1378 ++ RW_TAC std_ss [GSPECIFICATION]]); 1379 1380(* ------------------------------------------------------------------------- *) 1381(* The group of addition modulo n. *) 1382(* ------------------------------------------------------------------------- *) 1383 1384val Nonzero_def = Define `Nonzero = { n | ~(n = 0) }`; 1385 1386val add_mod_def = Define 1387 `add_mod n = 1388 <| carrier := { i | i < n }; 1389 id := 0; 1390 inv := (\i. (n - i) MOD n); 1391 mult := (\i j. (i + j) MOD n) |>`; 1392 1393val group_add_mod = store_thm 1394 ("group_add_mod", 1395 ``!n :: Nonzero. add_mod n IN Group``, 1396 RW_TAC resq_ss 1397 [Group_def,GSPECIFICATION,add_mod_def,combinTheory.K_THM,Nonzero_def] 1398 ++ Know `0 < n /\ !m. m < n = (m MOD n = m)` >> RW_TAC arith_ss [] 1399 ++ RW_TAC bool_ss [ZERO_MOD, MOD_MOD, ADD_CLAUSES] 1400 << [METIS_TAC [], 1401 Suff `((n - x) MOD n + x MOD n) MOD n = 0` 1402 >> METIS_TAC [] 1403 ++ MP_TAC (Q.SPEC `n` MOD_PLUS) 1404 ++ ASM_REWRITE_TAC [] 1405 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 1406 ++ POP_ASSUM (K ALL_TAC) 1407 ++ RW_TAC arith_ss [], 1408 Suff `((x + y) MOD n + z MOD n) MOD n = (x MOD n + (y + z) MOD n) MOD n` 1409 >> METIS_TAC [] 1410 ++ MP_TAC (Q.SPEC `n` MOD_PLUS) 1411 ++ ASM_REWRITE_TAC [] 1412 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 1413 ++ POP_ASSUM (K ALL_TAC) 1414 ++ RW_TAC arith_ss []]); 1415 1416val add_mod = store_thm 1417 ("add_mod", 1418 ``!n :: Nonzero. add_mod n IN FiniteAbelianGroup``, 1419 RW_TAC resq_ss 1420 [group_add_mod,FiniteAbelianGroup_def,AbelianGroup_def, 1421 GSPECIFICATION,combinTheory.K_THM,FiniteGroup_def,Nonzero_def] 1422 ++ REPEAT (POP_ASSUM MP_TAC) 1423 ++ RW_TAC arith_ss [add_mod_def, finite_num, GSPECIFICATION] 1424 ++ METIS_TAC []); 1425 1426val context = subtypeTools.add_reduction2 add_mod context; 1427val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1428 1429(* ------------------------------------------------------------------------- *) 1430(* The group of multiplication modulo p. *) 1431(* ------------------------------------------------------------------------- *) 1432 1433val Prime_def = Define `Prime = { n | prime n }`; 1434 1435val mult_mod_def = Define 1436 `mult_mod p = 1437 <| carrier := { i | ~(i = 0) /\ i < p }; 1438 id := 1; 1439 inv := (\i. i ** (p - 2) MOD p); 1440 mult := (\i j. (i * j) MOD p) |>`; 1441 1442val Prime_Nonzero = store_thm 1443 ("Prime_Nonzero", 1444 ``!p. p IN Prime ==> p IN Nonzero``, 1445 RW_TAC std_ss [Prime_def, Nonzero_def, GSPECIFICATION] 1446 ++ METIS_TAC [NOT_PRIME_0]); 1447 1448val context = subtypeTools.add_judgement2 Prime_Nonzero context; 1449val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1450 1451val group_mult_mod = store_thm 1452 ("group_mult_mod", 1453 ``!p :: Prime. mult_mod p IN Group``, 1454 RW_TAC resq_ss 1455 [Group_def,GSPECIFICATION,mult_mod_def,combinTheory.K_THM,Prime_def] 1456 ++ RW_TAC arith_ss [prime_one_lt] 1457 ++ Cases_on `p = 0` >> METIS_TAC [NOT_PRIME_0] 1458 ++ Know `0 < p` >> DECIDE_TAC ++ STRIP_TAC 1459 ++ RW_TAC std_ss [DIVISION, GSYM primalityTheory.divides_mod_zero] 1460 << [STRIP_TAC 1461 ++ MP_TAC (Q.SPECL [`p`,`x`,`y`] P_EUCLIDES) 1462 ++ RW_TAC std_ss [] 1463 ++ Know `0 < x` >> DECIDE_TAC ++ STRIP_TAC 1464 ++ Know `0 < y` >> DECIDE_TAC ++ STRIP_TAC 1465 ++ METIS_TAC [DIVIDES_LE, NOT_LESS], 1466 Know `0 < x` >> DECIDE_TAC ++ STRIP_TAC 1467 ++ Q.SPEC_TAC (`p - 2`, `k`) 1468 ++ Induct 1469 >> (RW_TAC std_ss [EXP] 1470 ++ STRIP_TAC 1471 ++ Know `p <= 1` >> METIS_TAC [DIVIDES_LE, DECIDE ``0 < 1``] 1472 ++ METIS_TAC [NOT_LESS, prime_one_lt]) 1473 ++ RW_TAC std_ss [EXP] 1474 ++ STRIP_TAC 1475 ++ MP_TAC (Q.SPECL [`p`,`x`,` x ** k`] P_EUCLIDES) 1476 ++ RW_TAC std_ss [] 1477 ++ STRIP_TAC 1478 ++ Know `p <= x` >> METIS_TAC [DIVIDES_LE] 1479 ++ METIS_TAC [NOT_LESS], 1480 MP_TAC (Q.SPEC `p` MOD_TIMES2) 1481 ++ ASM_REWRITE_TAC [] 1482 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th]) 1483 ++ RW_TAC bool_ss [MOD_MOD] 1484 ++ RW_TAC bool_ss [MOD_TIMES2] 1485 ++ REWRITE_TAC [GSYM EXP] 1486 ++ Know `SUC (p - 2) = p - 1` 1487 >> (Suff `1 <= p` >> DECIDE_TAC 1488 ++ DECIDE_TAC) 1489 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 1490 ++ RW_TAC std_ss [EXP] 1491 ++ Suff `~divides p x` >> METIS_TAC [fermat_little] 1492 ++ METIS_TAC 1493 [DIVIDES_LE, DECIDE ``~(x : num = 0) = 0 < x``, 1494 DECIDE ``~(a : num < b) = b <= a``], 1495 MP_TAC (Q.SPEC `p` MOD_MOD) 1496 ++ MP_TAC (Q.SPEC `p` MOD_TIMES2) 1497 ++ ASM_REWRITE_TAC [] 1498 ++ POP_ASSUM_LIST (K ALL_TAC) 1499 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [GSYM th] ++ ASSUME_TAC th) 1500 ++ DISCH_THEN (fn th => REWRITE_TAC [th]) 1501 ++ ASM_REWRITE_TAC [] 1502 ++ METIS_TAC [MULT_ASSOC, MULT_COMM]]); 1503 1504val mult_mod = store_thm 1505 ("mult_mod", 1506 ``!p :: Prime. mult_mod p IN FiniteAbelianGroup``, 1507 RW_TAC resq_ss 1508 [group_mult_mod,FiniteAbelianGroup_def,AbelianGroup_def, 1509 GSPECIFICATION,combinTheory.K_THM,FiniteGroup_def,Nonzero_def] 1510 ++ REPEAT (POP_ASSUM MP_TAC) 1511 ++ RW_TAC arith_ss [mult_mod_def, finite_num, GSPECIFICATION] 1512 ++ METIS_TAC [MULT_COMM]); 1513 1514val context = subtypeTools.add_reduction2 mult_mod context; 1515val {simplify = alg_ss, normalize = alg_ss'} = subtypeTools.simpset2 context; 1516 1517(* ========================================================================= *) 1518(* Cryptography based on groups *) 1519(* ========================================================================= *) 1520 1521(* ------------------------------------------------------------------------- *) 1522(* ElGamal encryption *) 1523(* ------------------------------------------------------------------------- *) 1524 1525val elgamal_encrypt_def = Define 1526 `elgamal_encrypt G g h m k = 1527 (group_exp G g k, G.mult (group_exp G h k) m)`; 1528 1529val elgamal_decrypt_def = Define 1530 `elgamal_decrypt G x (a,b) = G.mult (G.inv (group_exp G a x)) b`; 1531 1532val elgamal_correctness = store_thm 1533 ("elgamal_correctness", 1534 ``!G :: Group. !g h m :: (G.carrier). !k x. 1535 (h = group_exp G g x) ==> 1536 (elgamal_decrypt G x (elgamal_encrypt G g h m k) = m)``, 1537 RW_TAC resq_ss [elgamal_encrypt_def, elgamal_decrypt_def] 1538 ++ MATCH_MP_TAC EQ_TRANS 1539 ++ Q.EXISTS_TAC 1540 `G.mult (G.mult (G.inv (group_exp G (group_exp G g k) x)) 1541 (group_exp G (group_exp G g x) k)) m` 1542 ++ CONJ_TAC 1543 >> RW_TAC alg_ss' [] 1544 ++ RW_TAC alg_ss [GSYM group_exp_mult] 1545 ++ MP_TAC (Q.SPECL [`x`,`k`] MULT_COMM) 1546 ++ DISCH_THEN (fn th => ONCE_REWRITE_TAC [th]) 1547 ++ RW_TAC alg_ss []); 1548 1549val _ = html_theory "group"; 1550 1551val () = export_theory (); 1552