1(* interactive mode 2show_assums := true; 3loadPath := ["../ho_prover","../subtypes","../RSA","../formalize"] @ !loadPath; 4app load 5 ["bossLib", "listTheory", "subtypeTools", "res_quanTools", 6 "pred_setTheory", "extra_pred_setTheory", "arithContext", 7 "ho_proverTools", "extra_listTheory", "subtypeTheory", 8 "listContext", "arithmeticTheory", "groupTheory", "groupContext", 9 "extra_numTheory", "gcdTheory", "dividesTheory", 10 "extra_arithTheory", "finite_groupTheory", "finite_groupContext", 11 "abelian_groupTheory", "num_polyTheory", "extra_binomialTheory", 12 "binomialTheory", "summationTheory", "prob_extraTheory", 13 "pred_setContext"]; 14quietdec := true; 15*) 16 17open HolKernel Parse boolLib; 18open bossLib listTheory subtypeTools res_quanTools res_quanTheory 19 pred_setTheory extra_pred_setTheory arithContext 20 ho_proverTools extra_listTheory subtypeTheory 21 listContext arithmeticTheory groupTheory hurdUtils 22 groupContext extra_numTheory gcdTheory dividesTheory 23 extra_arithTheory finite_groupTheory finite_groupContext 24 abelian_groupTheory num_polyTheory extra_binomialTheory 25 binomialTheory summationTheory pred_setContext; 26 27(* interactive mode 28quietdec := false; 29*) 30 31val _ = new_theory "mult_group"; 32val _ = ParseExtras.temp_loose_equality() 33 34val EXISTS_DEF = boolTheory.EXISTS_DEF; 35 36infixr 0 ++ << || THENC ORELSEC ORELSER ##; 37infix 1 >>; 38 39val op!! = op REPEAT; 40val op++ = op THEN; 41val op<< = op THENL; 42val op|| = op ORELSE; 43val op>> = op THEN1; 44 45(* ------------------------------------------------------------------------- *) 46(* Tools. *) 47(* ------------------------------------------------------------------------- *) 48 49val S_TAC = !! (POP_ASSUM MP_TAC) ++ !! RESQ_STRIP_TAC; 50 51val std_pc = precontext_mergel [arith_pc, list_pc, pred_set_pc]; 52val std_c = precontext_compile std_pc; 53 54val (R_TAC, AR_TAC, R_TAC', AR_TAC') = SIMPLIFY_TACS std_c; 55 56val (G_TAC, AG_TAC, G_TAC', AG_TAC') = SIMPLIFY_TACS finite_group_c; 57 58val Strip = S_TAC; 59val Simplify = R_TAC; 60 61(* ------------------------------------------------------------------------- *) 62(* Definitions. *) 63(* ------------------------------------------------------------------------- *) 64 65val mult_group_def = Define 66 `mult_group n = 67 ((\x. x IN gset (add_group n) /\ (gcd n x = 1)), (\x y. (x * y) MOD n))`; 68 69val totient_def = Define `totient n = CARD (gset (mult_group n))`; 70 71(* ------------------------------------------------------------------------- *) 72(* Theorems. *) 73(* ------------------------------------------------------------------------- *) 74 75val MULT_GROUP_SET = store_thm 76 ("MULT_GROUP_SET", 77 ``!n x. 78 x IN gset (mult_group n) = x IN gset (add_group n) /\ (gcd n x = 1)``, 79 R_TAC [SPECIFICATION, gset_def, mult_group_def]); 80 81val MULT_GROUP_OP = store_thm 82 ("MULT_GROUP_OP", 83 ``!n x y. gop (mult_group n) x y = (x * y) MOD n``, 84 R_TAC [mult_group_def, gop_def]); 85 86val MULT_GROUP_SET_0 = store_thm 87 ("MULT_GROUP_SET_0", 88 ``!n. 1 < n ==> ~(0 IN gset (mult_group n))``, 89 S_TAC 90 ++ AR_TAC [MULT_GROUP_SET, GCD_0R] 91 ++ DECIDE_TAC); 92 93val MULT_SUBSET_ADD = store_thm 94 ("MULT_SUBSET_ADD", 95 ``!n. gset (mult_group n) SUBSET gset (add_group n)``, 96 R_TAC [SUBSET_DEF, MULT_GROUP_SET]); 97 98val MULT_GROUP_OP_SUBTYPE = store_thm 99 ("MULT_GROUP_OP_SUBTYPE", 100 ``!n. 101 1 < n ==> 102 gop (mult_group n) IN 103 (gset (mult_group n) -> gset (mult_group n) -> gset (mult_group n))``, 104 R_TAC [IN_FUNSET, MULT_GROUP_SET, ADD_GROUP_SET, MULT_GROUP_OP] 105 ++ S_TAC 106 ++ ONCE_REWRITE_TAC [GCD_SYM] 107 ++ Cases_on `n = 0` >> DECIDE_TAC 108 ++ Suff `gcd n (x' * x) = 1` 109 >> (CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [GCD_EFFICIENTLY])) 110 ++ R_TAC []) 111 ++ PROVE_TAC [GCD_1_MULTR]); 112 113val MULT_GROUP_ASSOC = store_thm 114 ("MULT_GROUP_ASSOC", 115 ``!n x y z. 116 1 < n ==> 117 (gop (mult_group n) (gop (mult_group n) x y) z 118 = gop (mult_group n) x (gop (mult_group n) y z))``, 119 S_TAC 120 ++ G_TAC [MULT_GROUP_OP, MULT_ASSOC]); 121 122val MULT_GROUP_COMM = store_thm 123 ("MULT_GROUP_COMM", 124 ``!n x y. 1 < n ==> (gop (mult_group n) x y = gop (mult_group n) y x)``, 125 S_TAC 126 ++ G_TAC [MULT_GROUP_OP] 127 ++ PROVE_TAC [MULT_COMM]); 128 129val MULT_GROUP_ID_WITNESS = store_thm 130 ("MULT_GROUP_ID_WITNESS", 131 ``!n. 132 1 < n ==> 133 1 IN gset (mult_group n) /\ 134 !x :: gset (mult_group n). gop (mult_group n) 1 x = x``, 135 S_TAC >> AG_TAC [MULT_GROUP_SET, ADD_GROUP_SET] 136 ++ AG_TAC [MULT_GROUP_SET, ADD_GROUP_SET, MULT_GROUP_OP]); 137 138val MULT_GROUP_INV = store_thm 139 ("MULT_GROUP_INV", 140 ``!n. !x :: gset (mult_group n). 141 1 < n ==> 142 ?y :: gset (mult_group n). gop (mult_group n) y x = 1``, 143 S_TAC 144 ++ Cases_on `x = 0` >> AR_TAC [MULT_GROUP_SET_0] 145 ++ AR_TAC [MULT_GROUP_SET, MULT_GROUP_OP, ADD_GROUP_SET] 146 ++ MP_TAC (Q.SPECL [`x`, `n`] LINEAR_GCD) 147 ++ R_TAC [] 148 ++ S_TAC 149 ++ Q_RESQ_EXISTS_TAC `p MOD n` 150 ++ REVERSE S_TAC >> G_TAC [] 151 ++ G_TAC [MULT_GROUP_SET, ADD_GROUP_SET] 152 ++ Suff `gcd p n = 1` 153 >> (Know `~(n = 0)` >> DECIDE_TAC 154 ++ PROVE_TAC [GCD_EFFICIENTLY, GCD_SYM]) 155 ++ Suff `!g. is_gcd p n g ==> (g = 1)` >> PROVE_TAC [GCD_IS_GCD] 156 ++ R_TAC [is_gcd_def, divides_def] 157 ++ S_TAC 158 ++ POP_ASSUM K_TAC 159 ++ AR_TAC [] 160 ++ Q.PAT_X_ASSUM `a:num * b = c` MP_TAC 161 ++ POP_ASSUM_LIST K_TAC 162 ++ Suff `(g * (q' * x) = g * (q * q'') + 1) ==> (g = 1)` 163 >> PROVE_TAC [MULT_ASSOC, MULT_COMM] 164 ++ DISCH_THEN (ASSUME_TAC o SYM) 165 ++ Suff `divides g 1` >> R_TAC [] 166 ++ MATCH_MP_TAC DIVIDES_ADD_2 167 ++ Q.EXISTS_TAC `g * (q * q'')` 168 ++ R_TAC [DIVIDES_MULT]); 169 170val MULT_GROUP_SET_FINITE = store_thm 171 ("MULT_GROUP_SET_FINITE", 172 ``!n. FINITE (gset (mult_group n))``, 173 PROVE_TAC [MULT_SUBSET_ADD, SUBSET_FINITE, ADD_GROUP_SET_FINITE]); 174 175val MULT_GROUP = store_thm 176 ("MULT_GROUP", 177 ``!n. 1 < n ==> mult_group n IN finite_group``, 178 R_TAC [IN_GROUP, MULT_GROUP_OP_SUBTYPE, MULT_GROUP_ASSOC, IN_FINITE_GROUP] 179 ++ REVERSE S_TAC >> R_TAC [MULT_GROUP_SET_FINITE] 180 ++ Q_RESQ_EXISTS_TAC `1` 181 ++ R_TAC [MULT_GROUP_ID_WITNESS, MULT_GROUP_INV]); 182 183val MULT_GROUP_SUBTYPE = store_thm 184 ("MULT_GROUP_SUBTYPE", 185 ``mult_group IN (gtnum 1 -> finite_group)``, 186 R_TAC [IN_FUNSET, MULT_GROUP, IN_GTNUM]); 187 188val MULT_GROUP_ID = store_thm 189 ("MULT_GROUP_ID", 190 ``!n. 1 < n ==> (gid (mult_group n) = 1)``, 191 S_TAC 192 ++ Know `mult_group n IN group` >> G_TAC [Q_RESQ_SPEC `n` MULT_GROUP] 193 ++ STRIP_TAC 194 ++ Know `1 IN gset (mult_group n)` >> R_TAC [MULT_GROUP_ID_WITNESS] 195 ++ STRIP_TAC 196 ++ MP_TAC (Q_RESQ_ISPECL [`mult_group n`, `1:num`] GID_UNIQUE) 197 ++ Suff `gop (mult_group n) 1 1 = 1` >> PROVE_TAC [] 198 ++ R_TAC [MULT_GROUP_OP] 199 ++ AG_TAC []); 200 201val MULT_GROUP_GPOW = store_thm 202 ("MULT_GROUP_GPOW", 203 ``!n. !g :: gset (mult_group n). !m. 204 1 < n ==> 205 (gpow (mult_group n) g m = (g EXP m) MOD n)``, 206 S_TAC 207 ++ Induct_on `m` >> AG_TAC [EXP, MULT_GROUP_ID] 208 ++ G_TAC [MULT_GROUP_OP, EXP]); 209 210val FERMAT_LITTLE = store_thm 211 ("FERMAT_LITTLE", 212 ``!n. !a :: gset (mult_group n). 1 < n ==> ((a EXP totient n) MOD n = 1)``, 213 S_TAC 214 ++ Suff `gpow (mult_group n) a (totient n) = gid (mult_group n)` 215 >> R_TAC [MULT_GROUP_GPOW, MULT_GROUP_ID] 216 ++ G_TAC [totient_def, MULT_GROUP]); 217 218val CARD_COPRIME_PRIME = store_thm 219 ("CARD_COPRIME_PRIME", 220 ``!p n. 221 0 < n /\ prime p ==> 222 (CARD (gset (add_group n) INTER (\x. ~divides p x)) = 223 n - (((n - 1) DIV p) + 1))``, 224 S_TAC 225 ++ Cases_on `n` >> AR_TAC [] 226 ++ AR_TAC [] 227 ++ Q.SPEC_TAC (`n'`, `n`) 228 ++ Induct 229 >> (G_TAC [INSERT_INTER, ADD_GROUP_SET_SUC, ADD_GROUP_SET_ZERO] 230 ++ G_TAC [SPECIFICATION]) 231 ++ POP_ASSUM MP_TAC 232 ++ Know `SUC (SUC n) - 1 = SUC (SUC n - 1)` >> DECIDE_TAC 233 ++ DISCH_THEN (REWRITE_TAC o wrap) 234 ++ Know `SUC n - 1 = n` >> DECIDE_TAC 235 ++ DISCH_THEN (REWRITE_TAC o wrap) 236 ++ STRIP_TAC 237 ++ ONCE_REWRITE_TAC [ADD_GROUP_SET_SUC] 238 ++ R_TAC [INSERT_INTER, SUC_DIV] 239 ++ R_TAC [SPECIFICATION] 240 ++ Cases_on `divides p (SUC n)` 241 >> (R_TAC [] ++ DECIDE_TAC) 242 ++ R_TAC [] 243 ++ Know `FINITE (gset (add_group (SUC n)) INTER (\x. ~divides p x))` 244 >> PROVE_TAC [ADD_GROUP_SET_FINITE, INTER_FINITE] 245 ++ STRIP_TAC 246 ++ G_TAC [CARD_INSERT, IN_INTER, ADD_GROUP_SET_MAX] 247 ++ Know `n DIV p <= n` >> R_TAC [DIV_LESS_EQ] 248 ++ STRIP_TAC 249 ++ R_TAC [GSYM ADD1] 250 ++ POP_ASSUM MP_TAC 251 ++ KILL_TAC 252 ++ DECIDE_TAC); 253 254val MULT_GROUP_SET_ALT = store_thm 255 ("MULT_GROUP_SET_ALT", 256 ``!n. gset (mult_group n) = gset (add_group n) INTER (\x. gcd n x = 1)``, 257 SET_EQ_TAC 258 ++ R_TAC [MULT_GROUP_SET, IN_INTER] 259 ++ R_TAC [SPECIFICATION]); 260 261val MULT_GROUP_SET_PRIME_POWER = store_thm 262 ("MULT_GROUP_SET_PRIME_POWER", 263 ``!p a. 264 0 < a /\ prime p ==> 265 (CARD (gset (mult_group (p EXP a))) = p EXP (a - 1) * (p - 1))``, 266 S_TAC 267 ++ R_TAC [CARD_COPRIME_PRIME, MULT_GROUP_SET_ALT, GCD_1_PRIME_POWERL] 268 ++ Know `0 < p EXP a` >> R_TAC [] 269 ++ STRIP_TAC 270 ++ Know `(p EXP a - 1) DIV p = (p EXP a) DIV p - 1` 271 >> (Know `SUC (p EXP a - 1) = p EXP a` >> DECIDE_TAC 272 ++ STRIP_TAC 273 ++ Suff `(p EXP a - 1) DIV p = SUC ((p EXP a) - 1) DIV p - 1` 274 >> R_TAC [] 275 ++ R_TAC [SUC_DIV] 276 ++ Know `?s. s <= a /\ (p = p EXP s)` 277 >> (Q.EXISTS_TAC `1` 278 ++ R_TAC [] 279 ++ DECIDE_TAC) 280 ++ DISCH_THEN (R_TAC o wrap) 281 ++ DECIDE_TAC) 282 ++ STRIP_TAC 283 ++ R_TAC [] 284 ++ Know `1 <= p EXP a DIV p` 285 >> (Suff `~(p EXP a DIV p = 0)` >> DECIDE_TAC 286 ++ R_TAC [] 287 ++ Cases_on `a` >> AR_TAC [] 288 ++ R_TAC [EXP] 289 ++ Suff `p * 1 <= p * p EXP n` >> DECIDE_TAC 290 ++ R_TAC [] 291 ++ Suff `0 < p EXP n` >> DECIDE_TAC 292 ++ R_TAC []) 293 ++ STRIP_TAC 294 ++ R_TAC [] 295 ++ Cases_on `a` >> AR_TAC [] 296 ++ R_TAC [EXP, LEFT_SUB_DISTRIB] 297 ++ Know `SUC n - 1 = n` >> DECIDE_TAC 298 ++ STRIP_TAC 299 ++ R_TAC [ONCE_REWRITE_RULE [MULT_COMM] MULT_DIV] 300 ++ PROVE_TAC [MULT_COMM]); 301 302val TOTIENT_PRIME_POWER = store_thm 303 ("TOTIENT_PRIME_POWER", 304 ``!p a. 305 0 < a /\ prime p ==> (totient (p EXP a) = p EXP (a - 1) * (p - 1))``, 306 R_TAC [totient_def, MULT_GROUP_SET_PRIME_POWER]); 307 308val TOTIENT_PRIME = store_thm 309 ("TOTIENT_PRIME", 310 ``!p. prime p ==> (totient p = p - 1)``, 311 S_TAC 312 ++ MP_TAC (Q_RESQ_SPECL [`p`, `1`] TOTIENT_PRIME_POWER) 313 ++ R_TAC [EXP, EXP_1]); 314 315val FERMAT_LITTLE_PRIME = store_thm 316 ("FERMAT_LITTLE_PRIME", 317 ``!p a. prime p /\ ~(divides p a) ==> ((a EXP (p - 1)) MOD p = 1)``, 318 S_TAC 319 ++ Suff `(a MOD p) EXP (p - 1) MOD p = 1` >> R_TAC [MOD_EXP] 320 ++ Know `(a MOD p) IN gset (mult_group p)` 321 >> R_TAC [MULT_GROUP_SET, ADD_GROUP_SET, DIVIDES_PRIME_MOD, GCD_1_PRIMEL] 322 ++ STRIP_TAC 323 ++ MP_TAC (Q_RESQ_SPECL [`p`, `a MOD p`] FERMAT_LITTLE) 324 ++ R_TAC [TOTIENT_PRIME]); 325 326val CHINESE_INJ = store_thm 327 ("CHINESE_INJ", 328 ``!p q x y. 329 1 < p /\ 1 < q /\ (gcd p q = 1) /\ (x MOD p = y MOD p) /\ 330 (x MOD q = y MOD q) ==> 331 (x MOD (p * q) = y MOD (p * q))``, 332 S_TAC 333 ++ Know `1 < p * q` >> R_TAC [] 334 ++ S_TAC 335 ++ Suff 336 `x MOD (p * q) < y MOD (p * q) \/ y MOD (p * q) < x MOD (p * q) ==> F` 337 >> DECIDE_TAC 338 ++ S_TAC << 339 [Know `x MOD (p * q) + (y MOD (p * q) - x MOD (p * q)) = y MOD (p * q)` 340 >> DECIDE_TAC 341 ++ Know `~(divides (p * q) (y MOD (p * q) - x MOD (p * q)))` 342 >> (Suff 343 `0 < y MOD (p * q) - x MOD (p * q) /\ 344 ~(p * q <= y MOD (p * q) - x MOD (p * q))` 345 >> PROVE_TAC [DIVIDES_LE] 346 ++ Know `y MOD (p * q) < p * q` >> R_TAC [] 347 ++ DECIDE_TAC) 348 ++ Q.SPEC_TAC (`y MOD (p * q) - x MOD (p * q)`, `d`) 349 ++ POP_ASSUM K_TAC 350 ++ S_TAC 351 ++ Know `(x MOD (p * q) + d) MOD p = (y MOD (p * q)) MOD p` >> R_TAC [] 352 ++ PURE_ONCE_REWRITE_TAC [MULT_COMM] 353 ++ POP_ASSUM (fn th => R_TAC [MOD_MULT_MOD] ++ ASSUME_TAC th) 354 ++ S_TAC 355 ++ Know `d MOD p = 0` 356 >> (POP_ASSUM MP_TAC 357 ++ R_TAC [MOD_ADD_CANCEL]) 358 ++ Know `(x MOD (p * q) + d) MOD q = (y MOD (p * q)) MOD q` >> R_TAC [] 359 ++ POP_ASSUM (fn th => R_TAC [MOD_MULT_MOD] ++ ASSUME_TAC th) 360 ++ RESQ_STRIP_TAC 361 ++ Know `d MOD q = 0` 362 >> (POP_ASSUM MP_TAC 363 ++ R_TAC [MOD_ADD_CANCEL]) 364 ++ NTAC 3 (POP_ASSUM K_TAC) 365 ++ R_TAC [DIVIDES_MOD] 366 ++ S_TAC 367 ++ PROVE_TAC [GCD_1_LCM], 368 Know `y MOD (p * q) + (x MOD (p * q) - y MOD (p * q)) = x MOD (p * q)` 369 >> DECIDE_TAC 370 ++ Know `~(divides (p * q) (x MOD (p * q) - y MOD (p * q)))` 371 >> (Suff 372 `0 < x MOD (p * q) - y MOD (p * q) /\ 373 ~(p * q <= x MOD (p * q) - y MOD (p * q))` 374 >> PROVE_TAC [DIVIDES_LE] 375 ++ Know `x MOD (p * q) < p * q` >> R_TAC [] 376 ++ DECIDE_TAC) 377 ++ Q.SPEC_TAC (`x MOD (p * q) - y MOD (p * q)`, `d`) 378 ++ POP_ASSUM K_TAC 379 ++ S_TAC 380 ++ Know `(y MOD (p * q) + d) MOD p = (x MOD (p * q)) MOD p` >> R_TAC [] 381 ++ PURE_ONCE_REWRITE_TAC [MULT_COMM] 382 ++ POP_ASSUM (fn th => R_TAC [MOD_MULT_MOD] ++ ASSUME_TAC th) 383 ++ S_TAC 384 ++ Know `d MOD p = 0` 385 >> (POP_ASSUM MP_TAC 386 ++ R_TAC [MOD_ADD_CANCEL]) 387 ++ Know `(y MOD (p * q) + d) MOD q = (x MOD (p * q)) MOD q` >> R_TAC [] 388 ++ POP_ASSUM (fn th => R_TAC [MOD_MULT_MOD] ++ ASSUME_TAC th) 389 ++ RESQ_STRIP_TAC 390 ++ Know `d MOD q = 0` 391 >> (POP_ASSUM MP_TAC 392 ++ R_TAC [MOD_ADD_CANCEL]) 393 ++ NTAC 3 (POP_ASSUM K_TAC) 394 ++ R_TAC [DIVIDES_MOD] 395 ++ S_TAC 396 ++ PROVE_TAC [GCD_1_LCM]]); 397 398val CHINESE_REMAINDER_WITNESS = store_thm 399 ("CHINESE_REMAINDER_WITNESS", 400 ``!p q. 401 1 < p /\ 1 < q /\ (gcd p q = 1) ==> 402 (\x. (x MOD p, x MOD q)) IN 403 group_iso (mult_group (p * q)) 404 (prod_group (mult_group p) (mult_group q))``, 405 S_TAC 406 ++ Know `?n. p * q = n` >> PROVE_TAC [] 407 ++ STRIP_TAC 408 ++ Know `1 < p * q` >> R_TAC [] 409 ++ ASM_REWRITE_TAC [] 410 ++ STRIP_TAC 411 ++ R_TAC [IN_GROUP_ISO, IN_GROUP_HOMO, PROD_GROUP_SET, PROD_GROUP_OP] 412 ++ STRONG_CONJ_TAC << 413 [S_TAC << 414 [R_TAC [IN_FUNSET, MULT_GROUP_SET, IN_CROSS, ADD_GROUP_SET] 415 ++ NTAC 2 RESQ_STRIP_TAC 416 ++ Know `gcd (p * q) x = 1` >> PROVE_TAC [] 417 ++ R_TAC [GCD_1_MULTL] 418 ++ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [GCD_EFFICIENTLY])) 419 ++ Cases_on `x = 0` >> AR_TAC [] 420 ++ Cases_on `p = 0` >> AR_TAC [] 421 ++ Cases_on `q = 0` >> AR_TAC [] 422 ++ R_TAC [] 423 ++ METIS_TAC [GCD_SYM], 424 R_TAC [MULT_GROUP_OP] 425 ++ Suff `(x * y) MOD p = (x * y) MOD (q * p) MOD p` 426 >> METIS_TAC [MULT_COMM] 427 ++ R_TAC [MOD_MULT_MOD], 428 R_TAC [MULT_GROUP_OP] 429 ++ Suff `(x * y) MOD q = (x * y) MOD (p * q) MOD q` >> R_TAC [] 430 ++ R_TAC [MOD_MULT_MOD]], 431 R_TAC [BIJ_ALT_RES] 432 ++ DISCH_THEN K_TAC 433 ++ S_TAC 434 ++ POP_ASSUM MP_TAC 435 ++ R_TAC [IN_CROSS, MULT_GROUP_SET] 436 ++ Cases_on `y` 437 ++ R_TAC [] 438 ++ R_TAC [RES_EXISTS_UNIQUE] 439 ++ S_TAC << 440 [MP_TAC (Q.SPECL [`p`, `q`] LINEAR_GCD) 441 ++ MP_TAC (Q.SPECL [`q`, `p`] LINEAR_GCD) 442 ++ Know `~(p = 0) /\ ~(q = 0)` >> DECIDE_TAC 443 ++ Know `gcd q p = 1` >> METIS_TAC [GCD_SYM] 444 ++ R_TAC [] 445 ++ DISCH_THEN K_TAC 446 ++ S_TAC 447 ++ Q_RESQ_EXISTS_TAC `(p * (p'' * r) + q * (p' * q')) MOD n` 448 ++ S_TAC << 449 [R_TAC [MULT_GROUP_SET, ADD_GROUP_SET] 450 ++ Suff `gcd n (p * (p'' * r) + q * (p' * q')) = 1` 451 >> (Know `~(n = 0)` >> DECIDE_TAC 452 ++ METIS_TAC [GCD_EFFICIENTLY, GCD_SYM]) 453 ++ Suff 454 `(?a. prime a /\ divides a (gcd n (p * (p'' * r) + q * (p' * q')))) ==> F` 455 >> (KILL_TAC 456 ++ Q.SPEC_TAC (`gcd n (p * (p'' * r) + q * (p' * q'))`, `m`) 457 ++ METIS_TAC [EXISTS_PRIME_DIVISOR]) 458 ++ S_TAC 459 ++ AR_TAC [DIVIDES_GCD] 460 ++ Know `divides a (q * p)` >> METIS_TAC [MULT_COMM] 461 ++ R_TAC [EUCLID] 462 ++ S_TAC << 463 [Suff `~divides a (p * (p'' * r))` 464 >> METIS_TAC [ADD_COMM, DIVIDES_ADD_2, DIVIDES_MULT] 465 ++ Suff `~divides a ((p'' * p) * r)` 466 >> METIS_TAC [MULT_COMM, MULT_ASSOC] 467 ++ ASM_REWRITE_TAC [] 468 ++ R_TAC [RIGHT_ADD_DISTRIB] 469 ++ Suff `~divides a r` 470 >> METIS_TAC [MULT_COMM, MULT_ASSOC, DIVIDES_ADD_2, DIVIDES_MULT] 471 ++ S_TAC 472 ++ Know `divides a (gcd q r)` >> R_TAC [DIVIDES_GCD] 473 ++ R_TAC [], 474 Suff `~divides a (q * (p' * q'))` 475 >> METIS_TAC [ADD_COMM, DIVIDES_ADD_2, DIVIDES_MULT] 476 ++ Suff `~divides a ((p' * q) * q')` 477 >> METIS_TAC [MULT_COMM, MULT_ASSOC] 478 ++ ASM_REWRITE_TAC [] 479 ++ R_TAC [RIGHT_ADD_DISTRIB] 480 ++ Suff `~divides a q'` 481 >> METIS_TAC [MULT_COMM, MULT_ASSOC, DIVIDES_ADD_2, DIVIDES_MULT] 482 ++ S_TAC 483 ++ Know `divides a (gcd p q')` >> R_TAC [DIVIDES_GCD] 484 ++ R_TAC []], 485 Q.PAT_X_ASSUM `p * q = n` 486 (fn th => ONCE_REWRITE_TAC [ONCE_REWRITE_RULE [MULT_COMM] (SYM th)]) 487 ++ R_TAC [MOD_MULT_MOD] 488 ++ Suff `q' = ((p' * q) * q') MOD p` 489 >> METIS_TAC [MULT_COMM, MULT_ASSOC] 490 ++ R_TAC [RIGHT_ADD_DISTRIB] 491 ++ AR_TAC [ADD_GROUP_SET], 492 Q.PAT_X_ASSUM `p * q = n` (fn th => ONCE_REWRITE_TAC [SYM th]) 493 ++ R_TAC [MOD_MULT_MOD] 494 ++ Suff `r = ((p'' * p) * r) MOD q` 495 >> METIS_TAC [MULT_COMM, MULT_ASSOC] 496 ++ R_TAC [RIGHT_ADD_DISTRIB] 497 ++ AR_TAC [ADD_GROUP_SET]], 498 Suff `x MOD (p * q) = y MOD (p * q)` 499 >> (Suff `(x MOD (p * q) = x) /\ (y MOD (p * q) = y)` >> R_TAC [] 500 ++ AR_TAC [MULT_GROUP_SET, ADD_GROUP_SET]) 501 ++ MATCH_MP_TAC (Q_RESQ_SPECL [`p`, `q`] CHINESE_INJ) 502 ++ R_TAC []]]); 503 504val CHINESE_REMAINDER = store_thm 505 ("CHINESE_REMAINDER", 506 ``!p q. 507 1 < p /\ 1 < q /\ (gcd p q = 1) ==> 508 ?f. 509 f IN 510 group_iso (mult_group (p * q)) 511 (prod_group (mult_group p) (mult_group q))``, 512 ho_PROVE_TAC [CHINESE_REMAINDER_WITNESS]); 513 514val MULT_GROUP_ABELIAN = store_thm 515 ("MULT_GROUP_ABELIAN", 516 ``!n. 1 < n ==> abelian (mult_group n)``, 517 S_TAC 518 ++ G_TAC [abelian_def] 519 ++ S_TAC 520 ++ MP_TAC (Q.SPECL [`n`, `g`, `h`] MULT_GROUP_COMM) 521 ++ PROVE_TAC []); 522 523val MULT_GROUP_PRIME_CYCLIC = store_thm 524 ("MULT_GROUP_PRIME_CYCLIC", 525 ``!p. prime p ==> cyclic (mult_group p)``, 526 S_TAC 527 ++ G_TAC [CYCLIC_ALT, MULT_GROUP_SUBTYPE] 528 ++ MP_TAC (Q_RESQ_HALF_ISPEC `mult_group p` STRUCTURE_THM) 529 ++ G_TAC' [MULT_GROUP_SUBTYPE, MULT_GROUP_ABELIAN] 530 ++ S_TAC 531 ++ Q_RESQ_EXISTS_TAC `g` 532 ++ R_TAC [] 533 ++ G_TAC [EQ_LESS_EQ, GORD_LE_CARD, MULT_GROUP_SUBTYPE] 534 ++ MP_TAC (Q.SPECL [`p`, `gord (mult_group p) g`] MOD_POLY_NTH_ROOTS) 535 ++ G_TAC [MULT_GROUP_SUBTYPE] 536 ++ Suff `FINITE (\x. x < p /\ (x EXP gord (mult_group p) g MOD p = 1)) /\ 537 (gset (mult_group p)) SUBSET 538 (\x. x < p /\ (x EXP gord (mult_group p) g MOD p = 1))` 539 >> (Q.SPEC_TAC (`gset (mult_group p)`, `s`) 540 ++ Q.SPEC_TAC (`(\x. x < p /\ (x EXP gord (mult_group p) g MOD p = 1))`, 541 `t`) 542 ++ Q.SPEC_TAC (`gord (mult_group p) g`, `n`) 543 ++ KILL_TAC 544 ++ S_TAC 545 ++ Suff `CARD s <= CARD t` >> DECIDE_TAC 546 ++ PROVE_TAC [CARD_SUBSET]) 547 ++ CONJ_TAC 548 >> (R_TAC [GSYM INTER_DEF_ALT] 549 ++ MATCH_MP_TAC FINITE_INTER_DISJ 550 ++ DISJ1_TAC 551 ++ MP_TAC (Q.SPEC `p` ADD_GROUP_SET_FINITE) 552 ++ R_TAC [add_group_def, gset_def]) 553 ++ R_TAC [SUBSET_DEF] 554 ++ Q.X_GEN_TAC `x` 555 ++ S_TAC 556 ++ R_TAC [SPECIFICATION] 557 ++ Q.PAT_X_ASSUM `!h :: P. Q h` (MP_TAC o Q_RESQ_SPEC `x`) 558 ++ S_TAC 559 >> (Q.PAT_X_ASSUM `x IN s` MP_TAC 560 ++ R_TAC [mult_group_def, add_group_def, gset_def] 561 ++ R_TAC [SPECIFICATION]) 562 ++ POP_ASSUM MP_TAC 563 ++ G_TAC [MULT_GROUP_GPOW, MULT_GROUP_ID]); 564 565val GPOW_PRIME_POWER = store_thm 566 ("GPOW_PRIME_POWER", 567 ``!p n. !g :: gset (mult_group (p EXP n)). 568 0 < n /\ prime p ==> 569 (gpow (mult_group (p EXP n)) g (p EXP n) = 570 gpow (mult_group (p EXP n)) g (p EXP (n - 1)))``, 571 S_TAC 572 ++ MP_TAC (Q_RESQ_HALF_ISPECL [`mult_group (p EXP n)`, `g:num`] 573 GPOW_MOD_CARD) 574 ++ G_TAC' [MULT_GROUP_SUBTYPE] 575 ++ DISCH_THEN (ONCE_REWRITE_TAC o wrap o GSYM) 576 ++ Know `?c. CARD (gset (mult_group (p EXP n))) = c` 577 >> PROVE_TAC [] 578 ++ S_TAC 579 ++ R_TAC [] 580 ++ Know `0 < c` 581 >> (POP_ASSUM (R_TAC o wrap o GSYM) 582 ++ G_TAC [MULT_GROUP_SUBTYPE]) 583 ++ S_TAC 584 ++ Suff `p EXP n = c + p EXP (n - 1)` 585 >> R_TAC [] 586 ++ POP_ASSUM K_TAC 587 ++ POP_ASSUM (R_TAC o wrap o GSYM) 588 ++ G_TAC [MULT_GROUP_SET_PRIME_POWER] 589 ++ ONCE_REWRITE_TAC [MULT_COMM] 590 ++ R_TAC [RIGHT_SUB_DISTRIB] 591 ++ Cases_on `n` >> AR_TAC [] 592 ++ R_TAC [SUC_SUB1] 593 ++ Know `p EXP n' <= p * p EXP n'` 594 >> (Suff `p EXP n' * 1 <= p * p EXP n'` >> RW_TAC arith_ss [] 595 ++ R_TAC []) 596 ++ R_TAC [EXP]); 597 598val STRONG_MULT_GROUP_PRIME_POWER_CYCLIC_LEMMA = store_thm 599 ("STRONG_MULT_GROUP_PRIME_POWER_CYCLIC_LEMMA", 600 ``!p g. 601 ODD p /\ prime p /\ (g EXP (p - 1) MOD p = 1) ==> 602 ?x z. ~divides p z /\ ((g + p * x) EXP (p - 1) = 1 + p * z)``, 603 S_TAC 604 ++ Know `?y. g EXP (p - 1) = 1 + p * y` 605 >> (MP_TAC (Q.SPECL [`p`, `g EXP (p - 1)`] DIVISION_ALT) 606 ++ R_TAC [] 607 ++ DISCH_THEN (ONCE_REWRITE_TAC o wrap o SYM) 608 ++ PROVE_TAC [ADD_COMM, MULT_COMM]) 609 ++ S_TAC 610 ++ R_TAC [EXP_PASCAL] 611 ++ Cases_on `p` >> PROVE_TAC [NOT_PRIME_0] 612 ++ R_TAC [summation_def, BINOMIAL_DEF1, GSYM ADD_ASSOC] 613 ++ REWRITE_TAC [ONE] 614 ++ R_TAC [SUMMATION_SHIFT_P] 615 ++ R_TAC [GSYM ADD1, EXP] 616 ++ Know `!a b c d : num. a * (b * (c * d)) = c * (a * b * d)` 617 >> PROVE_TAC [MULT_COMM, MULT_ASSOC] 618 ++ DISCH_THEN (ONCE_REWRITE_TAC o wrap) 619 ++ R_TAC [GSYM SUMMATION_TIMES] 620 ++ R_TAC [GSYM MULT_ASSOC, GSYM LEFT_ADD_DISTRIB] 621 ++ Cases_on `n` >> AR_TAC [GSYM ONE] 622 ++ R_TAC [summation_def] 623 ++ REWRITE_TAC [ONE] 624 ++ R_TAC [SUMMATION_SHIFT_P] 625 ++ R_TAC [GSYM ADD1, EXP] 626 ++ Know `!a b c d : num. a * (b * (c * d)) = c * (a * b * d)` 627 >> PROVE_TAC [MULT_COMM, MULT_ASSOC] 628 ++ DISCH_THEN (ONCE_REWRITE_TAC o wrap) 629 ++ R_TAC [GSYM SUMMATION_TIMES] 630 ++ R_TAC [GSYM MULT_ASSOC] 631 ++ Q.EXISTS_TAC `SUC n' * g * (1 + (SUC (SUC n') - y MOD SUC (SUC n')))` 632 ++ Q.EXISTS_TAC `y + 633 SUC n' * g * (1 + (SUC (SUC n') - y MOD SUC (SUC n'))) * 634 (binomial (SUC n') 1 * g EXP n' + 635 SUC (SUC n') * 636 (SUC n' * g * (1 + (SUC (SUC n') - y MOD SUC (SUC n'))) * 637 summation 0 n' 638 (\n. 639 binomial (SUC n') (SUC (SUC n)) * 640 (g EXP (n' - SUC n) * 641 (SUC (SUC n') * (SUC n' * g * (1 + (SUC (SUC n') - y MOD SUC (SUC n'))))) EXP 642 n))))` 643 ++ R_TAC [] 644 ++ ONCE_REWRITE_TAC [LEFT_ADD_DISTRIB] 645 ++ R_TAC [ADD_ASSOC] 646 ++ Know `!a b c. ~divides a b /\ divides a c ==> ~divides a (b + c)` 647 >> PROVE_TAC [DIVIDES_ADD_2, ADD_COMM] 648 ++ DISCH_THEN MATCH_MP_TAC 649 ++ Know `!a b c : num. a * (b * c) = b * (a * c)` 650 >> PROVE_TAC [MULT_COMM, MULT_ASSOC] 651 ++ DISCH_THEN (ONCE_REWRITE_TAC o wrap) 652 ++ R_TAC [] 653 ++ Cases_on `n'` >> AR_TAC [ODD] 654 ++ R_TAC [BINOMIAL_1] 655 ++ Know `!a b c d : num. a * b * c * d = a * (b * d) * c` 656 >> PROVE_TAC [MULT_ASSOC, MULT_COMM] 657 ++ DISCH_THEN (ONCE_REWRITE_TAC o wrap) 658 ++ Know `!a b c d : num. a * (b * c * d) = (a * b) * (c * d)` 659 >> PROVE_TAC [MULT_ASSOC, MULT_COMM] 660 ++ DISCH_THEN (ONCE_REWRITE_TAC o wrap) 661 ++ R_TAC [GSYM EXP] 662 ++ Know `SUC (SUC n) = SUC (SUC (SUC n)) - 1` >> DECIDE_TAC 663 ++ DISCH_THEN (ONCE_REWRITE_TAC o wrap) 664 ++ POP_ASSUM_TAC (Q.SPEC_TAC (`SUC (SUC (SUC n))`, `p`)) 665 ++ S_TAC 666 ++ POP_ASSUM MP_TAC 667 ++ Know `SUC (p - 1) = p` 668 >> (Suff `0 < p` >> DECIDE_TAC 669 ++ R_TAC []) 670 ++ DISCH_THEN (R_TAC o wrap) 671 ++ R_TAC [GSYM DIVIDES_MOD, MINUS_1_SQUARED_MOD] 672 ++ Know `!a b c : num. a + (b + c) = b + (a + c)` 673 >> PROVE_TAC [ADD_COMM, ADD_ASSOC] 674 ++ DISCH_THEN (ONCE_REWRITE_TAC o wrap) 675 ++ Suff `(1 + (y + (p - y MOD p))) MOD p = 1 MOD p` 676 >> R_TAC [] 677 ++ R_TAC [MOD_ADD_CANCEL] 678 ++ Know `!a b c : num. a <= b /\ a <= c ==> (b + (c - a) = c + (b - a))` 679 >> DECIDE_TAC 680 ++ DISCH_THEN (MP_TAC o Q.SPECL [`y MOD p`, `y`, `p`]) 681 ++ R_TAC [MOD_LESS_1] 682 ++ DISCH_THEN K_TAC 683 ++ Know `y - y MOD p = (y DIV p) * p` 684 >> (MP_TAC (Q.SPECL [`p`, `y`] DIVISION_ALT) 685 ++ R_TAC [] 686 ++ DECIDE_TAC) 687 ++ R_TAC []); 688 689val STRONG_MULT_GROUP_PRIME_POWER_CYCLIC = store_thm 690 ("STRONG_MULT_GROUP_PRIME_POWER_CYCLIC", 691 ``!p. 692 ODD p /\ prime p ==> 693 ?x. !n. 694 0 < n ==> 695 (x MOD (p EXP n)) IN gset (mult_group (p EXP n)) /\ 696 (gord (mult_group (p EXP n)) (x MOD (p EXP n)) = 697 totient (p EXP n))``, 698 S_TAC 699 ++ MP_TAC (Q.SPEC `p` MULT_GROUP_PRIME_CYCLIC) 700 ++ R_TAC [CYCLIC_ALT, MULT_GROUP_SUBTYPE, GSYM totient_def] 701 ++ R_TAC [TOTIENT_PRIME, TOTIENT_PRIME_POWER] 702 ++ S_TAC 703 ++ MP_TAC (Q.SPECL [`p`, `g`] STRONG_MULT_GROUP_PRIME_POWER_CYCLIC_LEMMA) 704 ++ R_TAC [] 705 ++ Know `g EXP (p - 1) MOD p = 1` 706 >> (Suff `gpow (mult_group p) g (p - 1) = gid (mult_group p)` 707 >> R_TAC [MULT_GROUP_GPOW, MULT_GROUP_ID] 708 ++ POP_ASSUM (fn th => G_TAC [SYM th, MULT_GROUP_SUBTYPE])) 709 ++ DISCH_THEN (fn th => R_TAC [th]) 710 ++ S_TAC 711 ++ Q.EXISTS_TAC `g + p * x` 712 ++ NTAC 2 STRIP_TAC 713 ++ STRONG_CONJ_TAC 714 >> (Q.PAT_X_ASSUM `g IN X` MP_TAC 715 ++ R_TAC [MULT_GROUP_SET, ADD_GROUP_SET, GCD_1_PRIMEL] 716 ++ STRIP_TAC 717 ++ ONCE_REWRITE_TAC [GCD_SYM] 718 ++ MP_TAC (SYM (Q.SPECL [`p EXP n`, `g + p * x`] GCD_EFFICIENTLY)) 719 ++ R_TAC [] 720 ++ DISCH_THEN K_TAC 721 ++ R_TAC [GCD_1_PRIME_POWERL] 722 ++ PROVE_TAC [DIVIDES_UPR, DIVIDES_ADD_2, ADD_COMM]) 723 ++ Know `?g'. (g + p * x) MOD (p EXP n) = g'` >> PROVE_TAC [] 724 ++ STRIP_TAC 725 ++ R_TAC [] 726 ++ STRIP_TAC 727 ++ MATCH_MP_TAC DIVIDES_ANTISYM 728 ++ STRONG_CONJ_TAC 729 >> (R_TAC [GSYM MULT_GROUP_SET_PRIME_POWER] 730 ++ G_TAC [MULT_GROUP_SUBTYPE, GSYM GPOW_GID_GORD]) 731 ++ S_TAC 732 ++ ONCE_REWRITE_TAC [MULT_COMM] 733 ++ Know `gcd (p - 1) (p EXP (n - 1)) = 1` 734 >> (Cases_on `n - 1` >> R_TAC [] 735 ++ R_TAC [GCD_1_PRIME_POWERR] 736 ++ Suff `0 < (p - 1) /\ ~(p <= p - 1)` >> PROVE_TAC [DIVIDES_LE] 737 ++ Know `1 < p` >> R_TAC [] 738 ++ DECIDE_TAC) 739 ++ R_TAC [GCD_1_LCM] 740 ++ DISCH_THEN K_TAC 741 ++ STRONG_CONJ_TAC 742 >> (Suff `gpow (mult_group p) g (gord (mult_group (p EXP n)) g') = 743 gid (mult_group p)` 744 >> R_TAC [GPOW_GID_GORD, MULT_GROUP_SUBTYPE] 745 ++ Know 746 `gpow (mult_group (p EXP n)) g' (gord (mult_group (p EXP n)) g') = 747 gid (mult_group (p EXP n))` 748 >> G_TAC [MULT_GROUP_SUBTYPE] 749 ++ R_TAC [MULT_GROUP_GPOW, MULT_GROUP_ID] 750 ++ Q.SPEC_TAC (`gord (mult_group (p EXP n)) g'`, `m`) 751 ++ STRIP_TAC 752 ++ Q.PAT_X_ASSUM `gg = g'` (REWRITE_TAC o wrap o SYM) 753 ++ R_TAC [] 754 ++ S_TAC 755 ++ Know `((g + p * x) EXP m MOD p EXP n) MOD p = 1 MOD p` 756 >> PROVE_TAC [] 757 ++ POP_ASSUM K_TAC 758 ++ Cases_on `n` >> DECIDE_TAC 759 ++ REWRITE_TAC [EXP] 760 ++ ONCE_REWRITE_TAC [MULT_COMM] 761 ++ R_TAC [MOD_MULT_MOD] 762 ++ STRIP_TAC 763 ++ Know `((g + x * p) MOD p) EXP m MOD p = 1` 764 >> R_TAC [] 765 ++ Know `(g + x * p) MOD p = g MOD p` >> R_TAC [] 766 ++ DISCH_THEN (REWRITE_TAC o wrap) 767 ++ R_TAC []) 768 ++ S_TAC 769 ++ Know 770 `?k. k <= n - 1 /\ 771 (p EXP k * (p - 1) = gord (mult_group (p EXP n)) g')` 772 >> (MP_TAC (Q.SPECL [`p`, `gord (mult_group (p EXP n)) g'`, `n - 1`, `p - 1`] 773 PRIME_POWER_SANDWICH) 774 ++ R_TAC []) 775 ++ NTAC 2 (POP_ASSUM K_TAC) 776 ++ S_TAC 777 ++ POP_ASSUM (fn th => ASSUME_TAC (SYM th) ++ REWRITE_TAC [SYM th]) 778 ++ Suff `k = n - 1` >> R_TAC [] 779 ++ MP_TAC (Q.SPECL [`p`, `z`, `k`] PRIME_ADD_1_EXP) 780 ++ R_TAC [] 781 ++ S_TAC 782 ++ Suff `(1 + p EXP (k + 1) * zk) MOD (p EXP n) = 1 MOD (p EXP n)` 783 >> (R_TAC [MOD_ADD_CANCEL, DIVIDES_MOD] 784 ++ Know `n = k + 1 + (n - (k + 1))` >> DECIDE_TAC 785 ++ DISCH_THEN (CONV_TAC o RATOR_CONV o ONCE_REWRITE_CONV o wrap) 786 ++ R_TAC [EXP_ADD] 787 ++ Cases_on `n - (k + 1)` 788 >> (STRIP_TAC 789 ++ Know `n = k + 1` >> DECIDE_TAC 790 ++ Q.PAT_X_ASSUM `0 < n` MP_TAC 791 ++ KILL_TAC 792 ++ DECIDE_TAC) 793 ++ R_TAC [EXP] 794 ++ STRIP_TAC 795 ++ Suff `divides p zk` >> PROVE_TAC [] 796 ++ PROVE_TAC [DIVIDES_DOWNL]) 797 ++ R_TAC [] 798 ++ POP_ASSUM (REWRITE_TAC o wrap o SYM) 799 ++ Q.PAT_X_ASSUM `q = 1 + p * z` (REWRITE_TAC o wrap o SYM) 800 ++ REWRITE_TAC [ONCE_REWRITE_RULE [MULT_COMM] EXP_MULT] 801 ++ Q.PAT_X_ASSUM `gord gp g' = q` (REWRITE_TAC o wrap o SYM) 802 ++ Suff `g' EXP gord (mult_group (p EXP n)) g' MOD p EXP n = 1` 803 >> (Q.PAT_X_ASSUM `q = g'` (REWRITE_TAC o wrap o SYM) 804 ++ Q.SPEC_TAC (`gord (mult_group (p EXP n)) ((g + p * x) MOD p EXP n)`, 805 `m`) 806 ++ Q.SPEC_TAC (`g + p * x`, `gg`) 807 ++ R_TAC []) 808 ++ R_TAC [GSYM MULT_GROUP_GPOW] 809 ++ G_TAC [MULT_GROUP_SUBTYPE] 810 ++ R_TAC [MULT_GROUP_ID]); 811 812val MULT_GROUP_PRIME_POWER_CYCLIC = store_thm 813 ("MULT_GROUP_PRIME_POWER_CYCLIC", 814 ``!p n. ODD p /\ prime p /\ 0 < n ==> cyclic (mult_group (p EXP n))``, 815 S_TAC 816 ++ MP_TAC (Q.SPEC `p` STRONG_MULT_GROUP_PRIME_POWER_CYCLIC) 817 ++ R_TAC [] 818 ++ S_TAC 819 ++ POP_ASSUM (MP_TAC o Q.SPEC `n`) 820 ++ R_TAC [] 821 ++ R_TAC [CYCLIC_ALT, totient_def, MULT_GROUP_SUBTYPE] 822 ++ S_TAC 823 ++ Q_RESQ_EXISTS_TAC `x MOD p EXP n` 824 ++ R_TAC []); 825 826val MULT_GROUP_SET_CARD = store_thm 827 ("MULT_GROUP_SET_CARD", 828 ``!n. 1 < n ==> CARD (gset (mult_group n)) <= n - 1``, 829 Strip 830 ++ Simplify [ADD_GROUP_SET, mult_group_def, gset_def] 831 ++ Know `FINITE ((\x. x < n) DIFF {0})` 832 >> (MATCH_MP_TAC FINITE_DIFF 833 ++ ho_PROVE_TAC [FINITE_LESS]) 834 ++ Strip 835 ++ Know `CARD (\x. x < n /\ (gcd n x = 1)) <= CARD ((\x. x < n) DIFF {0})` 836 >> (MP_TAC (Q.ISPEC `((\x : num. x < n) DIFF {0})` CARD_SUBSET) 837 ++ Simplify [] 838 ++ DISCH_THEN MATCH_MP_TAC 839 ++ Simplify [SUBSET_DEF, IN_DIFF] 840 ++ Simplify [SPECIFICATION] 841 ++ Strip 842 ++ AR_TAC []) 843 ++ Suff `CARD ((\x. x < n) DIFF {0}) = n - 1` >> DECIDE_TAC 844 ++ Simplify [CARD_DIFF, FINITE_LESS, CARD_LESS] 845 ++ Suff `{0} SUBSET (\x. x < n)` >> Simplify [SUBSET_INTER2] 846 ++ Simplify [SUBSET_DEF] 847 ++ Simplify [SPECIFICATION] 848 ++ DECIDE_TAC); 849 850val POWER_IN_MULT_GROUP = store_thm 851 ("POWER_IN_MULT_GROUP", 852 ``!n x y i. 853 1 < n /\ x < n /\ 0 < i /\ ((x EXP i) MOD n = y) /\ 854 y IN gset (mult_group n) ==> 855 x IN gset (mult_group n)``, 856 Cases_on `i` >> Simplify [] 857 ++ Simplify [EXP, MULT_GROUP_SET, ADD_GROUP_SET] 858 ++ Strip 859 ++ Suff `!p. prime p ==> ~divides p (gcd n' x)` 860 >> PROVE_TAC [EXISTS_PRIME_DIVISOR] 861 ++ Simplify [DIVIDES_GCD] 862 ++ Strip 863 ++ Suff `divides p (gcd n' y)` 864 >> PROVE_TAC [EXISTS_PRIME_DIVISOR] 865 ++ Simplify [DIVIDES_GCD] 866 ++ Simplify [GSYM DIVIDES_MOD] 867 ++ Q.PAT_X_ASSUM `z = y` (ONCE_REWRITE_TAC o wrap o SYM) 868 ++ Q.PAT_X_ASSUM `divides p n'` MP_TAC 869 ++ REWRITE_TAC [divides_def] 870 ++ Strip 871 ++ Know `0 < q` >> (Suff `~(q = 0)` >> DECIDE_TAC ++ Strip ++ AR_TAC []) 872 ++ POP_ASSUM (REWRITE_TAC o wrap) 873 ++ Q.PAT_X_ASSUM `divides p x` MP_TAC 874 ++ Simplify [MOD_MULT_MOD, GSYM DIVIDES_MOD]); 875 876val POWER_ID_IN_MULT_GROUP = store_thm 877 ("POWER_ID_IN_MULT_GROUP", 878 ``!n x i. 879 1 < n /\ x < n /\ 0 < i /\ ((x EXP i) MOD n = 1) ==> 880 x IN gset (mult_group n)``, 881 Strip 882 ++ MATCH_MP_TAC POWER_IN_MULT_GROUP 883 ++ Q.EXISTS_TAC `gid (mult_group n)` 884 ++ Q.EXISTS_TAC `i` 885 ++ ASSUME_TAC (Q.SPEC `n` MULT_GROUP) 886 ++ RES_TAC 887 ++ G_TAC' [] 888 ++ Simplify [MULT_GROUP_ID]); 889 890val MULT_GROUP_1 = store_thm 891 ("MULT_GROUP_1", 892 ``!n. 1 < n ==> 1 IN gset (mult_group n)``, 893 Strip 894 ++ MATCH_MP_TAC POWER_ID_IN_MULT_GROUP 895 ++ Q.EXISTS_TAC `1` 896 ++ Simplify []); 897 898val MINUS_1_IN_MULT_GROUP = store_thm 899 ("MINUS_1_IN_MULT_GROUP", 900 ``!n. 1 < n ==> (n - 1) IN gset (mult_group n)``, 901 Strip 902 ++ MATCH_MP_TAC POWER_ID_IN_MULT_GROUP 903 ++ Q.EXISTS_TAC `2` 904 ++ REWRITE_TAC [TWO, ONE, EXP] 905 ++ Simplify [MINUS_1_SQUARED_MOD] 906 ++ DECIDE_TAC); 907 908val MULT_GROUP_GORD_MINUS_1 = store_thm 909 ("MULT_GROUP_GORD_MINUS_1", 910 ``!n. 2 < n ==> (gord (mult_group n) (n - 1) = 2)``, 911 Strip 912 ++ Know `1 < n` >> DECIDE_TAC 913 ++ Strip 914 ++ MP_TAC (Q.SPEC `n` MINUS_1_IN_MULT_GROUP) 915 ++ G_TAC [MULT_GROUP_SUBTYPE, IS_GORD] 916 ++ Simplify [MULT_GROUP_GPOW, MULT_GROUP_ID] 917 ++ DISCH_THEN K_TAC 918 ++ Know `!m : num. 0 < m /\ m < 2 = (m = 1)` >> DECIDE_TAC 919 ++ Know `n - 1 < n` >> DECIDE_TAC 920 ++ Simplify [TWO, EXP, MINUS_1_SQUARED_MOD] 921 ++ Strip 922 ++ POP_ASSUM MP_TAC 923 ++ Q.PAT_X_ASSUM `2 < n` MP_TAC 924 ++ KILL_TAC 925 ++ DECIDE_TAC); 926 927val IN_MULT_GROUP_UP = store_thm 928 ("IN_MULT_GROUP_UP", 929 ``!x p q. 930 1 < p /\ 1 < q /\ x IN gset (mult_group (p * q)) ==> 931 x MOD p IN gset (mult_group p)``, 932 Simplify [MULT_GROUP_SET, ADD_GROUP_SET] 933 ++ Strip 934 ++ ONCE_REWRITE_TAC [GCD_SYM] 935 ++ Suff `~(p = 0) /\ (gcd p x = 1)` >> PROVE_TAC [GCD_EFFICIENTLY] 936 ++ Simplify [] 937 ++ PROVE_TAC [GCD_1_MULTL]); 938 939val SQUARE_1_MOD_PRIME = store_thm 940 ("SQUARE_1_MOD_PRIME", 941 ``!p n. 942 prime p ==> 943 (((n * n) MOD p = 1) = (n MOD p = 1) \/ (n MOD p = p - 1))``, 944 Strip 945 ++ Cases_on `p = 2` 946 >> (Cases_on `EVEN n` 947 ++ Simplify [MOD_TWO, EVEN_ODD_BASIC] 948 ++ DECIDE_TAC) 949 ++ ONCE_REWRITE_TAC [ONCE_REWRITE_RULE [CONJ_COMM] EQ_IMP_THM] 950 ++ Q.SPEC_TAC (`n`, `n`) 951 ++ CONV_TAC (DEPTH_CONV FORALL_AND_CONV) 952 ++ STRONG_CONJ_TAC >> (Strip ++ Simplify [MINUS_1_SQUARED_MOD]) 953 ++ Know `!n. n * n = n EXP 2` 954 >> (REWRITE_TAC [TWO, ONE, EXP] 955 ++ Simplify []) 956 ++ DISCH_THEN (Simplify o wrap) 957 ++ Strip 958 ++ MP_TAC (Q.SPECL [`p`, `2`] MOD_POLY_NTH_ROOTS) 959 ++ Simplify [] 960 ++ Strip 961 ++ Suff `(\x. x < p /\ (x EXP 2 MOD p = 1)) = {1; p - 1}` 962 >> (SET_EQ_TAC 963 ++ Simplify [IN_INSERT] 964 ++ Simplify [SPECIFICATION] 965 ++ DISCH_THEN (MP_TAC o Q.SPEC `n MOD p`) 966 ++ Simplify []) 967 ++ MATCH_MP_TAC EQ_SYM 968 ++ MATCH_MP_TAC FINITE_SUBSET_CARD_EQ 969 ++ STRONG_CONJ_TAC >> Simplify [FINITE_LESS1] 970 ++ STRIP_TAC 971 ++ STRONG_CONJ_TAC 972 >> (Simplify [SUBSET_DEF, IN_INSERT] 973 ++ Simplify [SPECIFICATION] 974 ++ (Strip ++ Simplify []) 975 ++ Suff `0 < p` >> (KILL_TAC ++ DECIDE_TAC) 976 ++ Simplify []) 977 ++ STRIP_TAC 978 ++ ONCE_REWRITE_TAC [EQ_LESS_EQ] 979 ++ CONJ_TAC >> Simplify [CARD_SUBSET] 980 ++ Know `~(1 = p - 1)` 981 >> (Suff `1 < p /\ ~(p = 2)` >> (KILL_TAC ++ DECIDE_TAC) 982 ++ Simplify []) 983 ++ Simplify [GSYM TWO]); 984 985val _ = export_theory (); 986