1(* ------------------------------------------------------------------------- *) 2(* Euler Set and Totient Function *) 3(* ------------------------------------------------------------------------- *) 4 5(*===========================================================================*) 6 7(* add all dependent libraries for script *) 8open HolKernel boolLib bossLib Parse; 9 10(* declare new theory at start *) 11val _ = new_theory "Euler"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* val _ = load "jcLib"; *) 17open jcLib; 18 19(* Get dependent theories in lib *) 20(* val _ = load "helperFunctionTheory"; *) 21(* (* val _ = load "helperNumTheory"; -- in helperFunctionTheory *) *) 22(* (* val _ = load "helperSetTheory"; -- in helperFunctionTheory *) *) 23open helperNumTheory helperSetTheory helperFunctionTheory; 24 25(* open dependent theories *) 26open pred_setTheory listTheory; 27(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 28(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 29open arithmeticTheory dividesTheory gcdTheory; 30 31 32(* ------------------------------------------------------------------------- *) 33(* Euler Set and Totient Function Documentation *) 34(* ------------------------------------------------------------------------- *) 35(* Overloading: 36 natural n = IMAGE SUC (count n) 37 upto n = count (SUC n) 38*) 39(* Definitions and Theorems (# are exported, ! in computeLib): 40 41 Residues: 42 residue_def |- !n. residue n = {i | 0 < i /\ i < n} 43 residue_element |- !n j. j IN residue n ==> 0 < j /\ j < n 44 residue_0 |- residue 0 = {} 45 residue_1 |- residue 1 = {} 46 residue_nonempty |- !n. 1 < n ==> residue n <> {} 47 residue_no_zero |- !n. 0 NOTIN residue n 48 residue_no_self |- !n. n NOTIN residue n 49! residue_thm |- !n. residue n = count n DIFF {0} 50 residue_insert |- !n. 0 < n ==> (residue (SUC n) = n INSERT residue n) 51 residue_delete |- !n. 0 < n ==> (residue n DELETE n = residue n) 52 residue_suc |- !n. 0 < n ==> (residue (SUC n) = n INSERT residue n) 53 residue_count |- !n. 0 < n ==> (count n = 0 INSERT residue n) 54 residue_finite |- !n. FINITE (residue n) 55 residue_card |- !n. 0 < n ==> (CARD (residue n) = n - 1) 56 residue_prime_neq |- !p a n. prime p /\ a IN residue p /\ n <= p ==> 57 !x. x IN residue n ==> (a * n) MOD p <> (a * x) MOD p 58 prod_set_residue |- !n. PROD_SET (residue n) = FACT (n - 1) 59 60 Naturals: 61 natural_element |- !n j. j IN natural n <=> 0 < j /\ j <= n 62 natural_property |- !n. natural n = {j | 0 < j /\ j <= n} 63 natural_finite |- !n. FINITE (natural n) 64 natural_card |- !n. CARD (natural n) = n 65 natural_not_0 |- !n. 0 NOTIN natural n 66 natural_0 |- natural 0 = {} 67 natural_1 |- natural 1 = {1} 68 natural_has_1 |- !n. 0 < n ==> 1 IN natural n 69 natural_has_last |- !n. 0 < n ==> n IN natural n 70 natural_suc |- !n. natural (SUC n) = SUC n INSERT natural n 71 natural_thm |- !n. natural n = set (GENLIST SUC n) 72 natural_divisor_natural |- !n a b. 0 < n /\ a IN natural n /\ b divides a ==> b IN natural n 73 natural_cofactor_natural |- !n a b. 0 < n /\ 0 < a /\ b IN natural n /\ a divides b ==> 74 b DIV a IN natural n 75 natural_cofactor_natural_reduced 76 |- !n a b. 0 < n /\ a divides n /\ b IN natural n /\ a divides b ==> 77 b DIV a IN natural (n DIV a) 78 79 Uptos: 80 upto_finite |- !n. FINITE (upto n) 81 upto_card |- !n. CARD (upto n) = SUC n 82 upto_has_last |- !n. n IN upto n 83 upto_split_first |- !n. upto n = {0} UNION natural n 84 upto_split_last |- !n. upto n = count n UNION {n} 85 upto_by_count |- !n. upto n = n INSERT count n 86 upto_by_natural |- !n. upto n = 0 INSERT natural n 87 natural_by_upto |- !n. natural n = upto n DELETE 0 88 89 Euler Set and Totient Function: 90 Euler_def |- !n. Euler n = {i | 0 < i /\ i < n /\ coprime n i} 91 totient_def |- !n. totient n = CARD (Euler n) 92 Euler_element |- !n x. x IN Euler n <=> 0 < x /\ x < n /\ coprime n x 93! Euler_thm |- !n. Euler n = residue n INTER {j | coprime j n} 94 Euler_finite |- !n. FINITE (Euler n) 95 Euler_0 |- Euler 0 = {} 96 Euler_1 |- Euler 1 = {} 97 Euler_has_1 |- !n. 1 < n ==> 1 IN Euler n 98 Euler_nonempty |- !n. 1 < n ==> Euler n <> {} 99 Euler_empty |- !n. (Euler n = {}) <=> (n = 0 \/ n = 1) 100 Euler_card_upper_le |- !n. totient n <= n 101 Euler_card_upper_lt |- !n. 1 < n ==> totient n < n 102 Euler_card_bounds |- !n. totient n <= n /\ (1 < n ==> 0 < totient n /\ totient n < n) 103 Euler_prime |- !p. prime p ==> (Euler p = residue p) 104 Euler_card_prime |- !p. prime p ==> (totient p = p - 1) 105 106 Summation of Geometric Sequence: 107 sigma_geometric_natural_eqn |- !p. 0 < p ==> 108 !n. (p - 1) * SIGMA (\j. p ** j) (natural n) = p * (p ** n - 1) 109 sigma_geometric_natural |- !p. 1 < p ==> 110 !n. SIGMA (\j. p ** j) (natural n) = p * (p ** n - 1) DIV (p - 1) 111 112 Useful Theorems: 113 PROD_SET_IMAGE_EXP_NONZERO |- !n m. 1 < n /\ 0 < m ==> 114 (PROD_SET (IMAGE (\j. n ** j) (count m)) = 115 PROD_SET (IMAGE (\j. n ** j) (residue m))) 116*) 117 118(* ------------------------------------------------------------------------- *) 119(* Count-based Sets *) 120(* ------------------------------------------------------------------------- *) 121 122(* ------------------------------------------------------------------------- *) 123(* Residues -- close-relative of COUNT *) 124(* ------------------------------------------------------------------------- *) 125 126(* Define the set of residues = nonzero remainders *) 127val residue_def = zDefine `residue n = { i | (0 < i) /\ (i < n) }`; 128(* use zDefine as this is not computationally effective. *) 129 130(* Theorem: j IN residue n ==> 0 < j /\ j < n *) 131(* Proof: by residue_def. *) 132val residue_element = store_thm( 133 "residue_element", 134 ``!n j. j IN residue n ==> 0 < j /\ j < n``, 135 rw[residue_def]); 136 137(* Theorem: residue 0 = EMPTY *) 138(* Proof: by residue_def *) 139val residue_0 = store_thm( 140 "residue_0", 141 ``residue 0 = {}``, 142 simp[residue_def]); 143 144(* Theorem: residue 1 = EMPTY *) 145(* Proof: by definition. *) 146val residue_1 = store_thm( 147 "residue_1", 148 ``residue 1 = {}``, 149 simp[residue_def]); 150 151(* Theorem: 1 < n ==> residue n <> {} *) 152(* Proof: 153 By residue_def, this is to show: 1 < n ==> ?x. x <> 0 /\ x < n 154 Take x = 1, this is true. 155*) 156val residue_nonempty = store_thm( 157 "residue_nonempty", 158 ``!n. 1 < n ==> residue n <> {}``, 159 rw[residue_def, EXTENSION] >> 160 metis_tac[DECIDE``1 <> 0``]); 161 162(* Theorem: 0 NOTIN residue n *) 163(* Proof: by residue_def *) 164val residue_no_zero = store_thm( 165 "residue_no_zero", 166 ``!n. 0 NOTIN residue n``, 167 simp[residue_def]); 168 169(* Theorem: n NOTIN residue n *) 170(* Proof: by residue_def *) 171val residue_no_self = store_thm( 172 "residue_no_self", 173 ``!n. n NOTIN residue n``, 174 simp[residue_def]); 175 176(* Theorem: residue n = (count n) DIFF {0} *) 177(* Proof: 178 residue n 179 = {i | 0 < i /\ i < n} by residue_def 180 = {i | i < n /\ i <> 0} by NOT_ZERO_LT_ZERO 181 = {i | i < n} DIFF {0} by IN_DIFF 182 = (count n) DIFF {0} by count_def 183*) 184val residue_thm = store_thm( 185 "residue_thm[compute]", 186 ``!n. residue n = (count n) DIFF {0}``, 187 rw[residue_def, EXTENSION]); 188(* This is effective, put in computeLib. *) 189 190(* 191> EVAL ``residue 10``; 192val it = |- residue 10 = {9; 8; 7; 6; 5; 4; 3; 2; 1}: thm 193*) 194 195(* Theorem: For n > 0, residue (SUC n) = n INSERT residue n *) 196(* Proof: 197 residue (SUC n) 198 = {1, 2, ..., n} 199 = n INSERT {1, 2, ..., (n-1) } 200 = n INSERT residue n 201*) 202val residue_insert = store_thm( 203 "residue_insert", 204 ``!n. 0 < n ==> (residue (SUC n) = n INSERT residue n)``, 205 srw_tac[ARITH_ss][residue_def, EXTENSION]); 206 207(* Theorem: (residue n) DELETE n = residue n *) 208(* Proof: Because n is not in (residue n). *) 209val residue_delete = store_thm( 210 "residue_delete", 211 ``!n. 0 < n ==> ((residue n) DELETE n = residue n)``, 212 rpt strip_tac >> 213 `n NOTIN (residue n)` by rw[residue_def] >> 214 metis_tac[DELETE_NON_ELEMENT]); 215 216(* Theorem alias: rename *) 217val residue_suc = save_thm("residue_suc", residue_insert); 218(* val residue_suc = |- !n. 0 < n ==> (residue (SUC n) = n INSERT residue n): thm *) 219 220(* Theorem: count n = 0 INSERT (residue n) *) 221(* Proof: by definition. *) 222val residue_count = store_thm( 223 "residue_count", 224 ``!n. 0 < n ==> (count n = 0 INSERT (residue n))``, 225 srw_tac[ARITH_ss][residue_def, EXTENSION]); 226 227(* Theorem: FINITE (residue n) *) 228(* Proof: by FINITE_COUNT. 229 If n = 0, residue 0 = {}, hence FINITE. 230 If n > 0, count n = 0 INSERT (residue n) by residue_count 231 hence true by FINITE_COUNT and FINITE_INSERT. 232*) 233val residue_finite = store_thm( 234 "residue_finite", 235 ``!n. FINITE (residue n)``, 236 Cases >- 237 rw[residue_def] >> 238 metis_tac[residue_count, FINITE_INSERT, count_def, FINITE_COUNT, DECIDE ``0 < SUC n``]); 239 240(* Theorem: For n > 0, CARD (residue n) = n-1 *) 241(* Proof: 242 Since 0 INSERT (residue n) = count n by residue_count 243 the result follows by CARD_COUNT. 244*) 245val residue_card = store_thm( 246 "residue_card", 247 ``!n. 0 < n ==> (CARD (residue n) = n-1)``, 248 rpt strip_tac >> 249 `0 NOTIN (residue n)` by rw[residue_def] >> 250 `0 INSERT (residue n) = count n` by rw[residue_count] >> 251 `SUC (CARD (residue n)) = n` by metis_tac[residue_finite, CARD_INSERT, CARD_COUNT] >> 252 decide_tac); 253 254(* Theorem: For prime m, a in residue m, n <= m, a*n MOD m <> a*x MOD m for all x in residue n *) 255(* Proof: 256 Assume the contrary, that a*n MOD m = a*x MOD m 257 Since a in residue m and m is prime, MOD_MULT_LCANCEL gives: n MOD m = x MOD m 258 If n = m, n MOD m = 0, but x MOD m <> 0, hence contradiction. 259 If n < m, then since x < n <= m, n = x, contradicting x < n. 260*) 261val residue_prime_neq = store_thm( 262 "residue_prime_neq", 263 ``!p a n. prime p /\ a IN (residue p) /\ n <= p ==> !x. x IN (residue n) ==> (a*n) MOD p <> (a*x) MOD p``, 264 rw[residue_def] >> 265 spose_not_then strip_assume_tac >> 266 `0 < p` by rw[PRIME_POS] >> 267 `(a MOD p <> 0) /\ (x MOD p <> 0)` by rw_tac arith_ss[] >> 268 `n MOD p = x MOD p` by metis_tac[MOD_MULT_LCANCEL] >> 269 Cases_on `n = p` >- 270 metis_tac [DIVMOD_ID] >> 271 `n < p` by decide_tac >> 272 `(n MOD p = n) /\ (x MOD p = x)` by rw_tac arith_ss[] >> 273 decide_tac); 274 275(* Idea: the product of residues is a factorial. *) 276 277(* Theorem: PROD_SET (residue n) = FACT (n - 1) *) 278(* Proof: 279 By induction on n. 280 Base: PROD_SET (residue 0) = FACT (0 - 1) 281 PROD_SET (residue 0) 282 = PROD_SET {} by residue_0 283 = 1 by PROD_SET_EMPTY 284 = FACT 0 by FACT_0 285 = FACT (0 - 1) by arithmetic 286 Step: PROD_SET (residue n) = FACT (n - 1) ==> 287 PROD_SET (residue (SUC n)) = FACT (SUC n - 1) 288 If n = 0, 289 PROD_SET (residue (SUC 0)) 290 = PROD_SET (residue 1) by ONE 291 = PROD_SET {} by residue_1 292 = 1 by PROD_SET_EMPTY 293 = FACT 0 by FACT_0 294 295 If n <> 0, then 0 < n. 296 Note FINITE (residue n) by residue_finite 297 PROD_SET (residue (SUC n)) 298 = PROD_SET (n INSERT residue n) by residue_insert 299 = n * PROD_SET ((residue n) DELETE n) by PROD_SET_THM 300 = n * PROD_SET (residue n) by residue_delete 301 = n * FACT (n - 1) by induction hypothesis 302 = FACT (SUC (n - 1)) by FACT 303 = FACT (SUC n - 1) by arithmetic 304*) 305val prod_set_residue = store_thm( 306 "prod_set_residue", 307 ``!n. PROD_SET (residue n) = FACT (n - 1)``, 308 Induct >- 309 simp[residue_0, PROD_SET_EMPTY, FACT_0] >> 310 Cases_on `n = 0` >- 311 simp[residue_1, PROD_SET_EMPTY, FACT_0] >> 312 `FINITE (residue n)` by rw[residue_finite] >> 313 `n = SUC (n - 1)` by decide_tac >> 314 `SUC (n - 1) = SUC n - 1` by decide_tac >> 315 `PROD_SET (residue (SUC n)) = PROD_SET (n INSERT residue n)` by rw[residue_insert] >> 316 `_ = n * PROD_SET ((residue n) DELETE n)` by rw[PROD_SET_THM] >> 317 `_ = n * PROD_SET (residue n)` by rw[residue_delete] >> 318 `_ = n * FACT (n - 1)` by rw[] >> 319 metis_tac[FACT]); 320 321(* ------------------------------------------------------------------------- *) 322(* Naturals -- counting from 1 rather than 0, and inclusive. *) 323(* ------------------------------------------------------------------------- *) 324 325(* Overload the set of natural numbers (like count) *) 326val _ = overload_on("natural", ``\n. IMAGE SUC (count n)``); 327 328(* Theorem: j IN (natural n) <=> 0 < j /\ j <= n *) 329(* Proof: 330 Note j <> 0 by natural_not_0 331 j IN (natural n) 332 ==> j IN IMAGE SUC (count n) by notation 333 ==> ?x. x < n /\ (j = SUC x) by IN_IMAGE 334 Since SUC x <> 0 by numTheory.NOT_SUC 335 Hence j <> 0, 336 and x < n ==> SUC x < SUC n by LESS_MONO_EQ 337 or j < SUC n by above, j = SUC x 338 thus j <= n by prim_recTheory.LESS_THM 339*) 340val natural_element = store_thm( 341 "natural_element", 342 ``!n j. j IN (natural n) <=> 0 < j /\ j <= n``, 343 rw[EQ_IMP_THM] >> 344 `j <> 0` by decide_tac >> 345 `?m. j = SUC m` by metis_tac[num_CASES] >> 346 `m < n` by decide_tac >> 347 metis_tac[]); 348 349(* Theorem: natural n = {j| 0 < j /\ j <= n} *) 350(* Proof: by natural_element, IN_IMAGE *) 351val natural_property = store_thm( 352 "natural_property", 353 ``!n. natural n = {j| 0 < j /\ j <= n}``, 354 rw[EXTENSION, natural_element]); 355 356(* Theorem: FINITE (natural n) *) 357(* Proof: FINITE_COUNT, IMAGE_FINITE *) 358val natural_finite = store_thm( 359 "natural_finite", 360 ``!n. FINITE (natural n)``, 361 rw[]); 362 363(* Theorem: CARD (natural n) = n *) 364(* Proof: 365 CARD (natural n) 366 = CARD (IMAGE SUC (count n)) by notation 367 = CARD (count n) by CARD_IMAGE_SUC 368 = n by CARD_COUNT 369*) 370val natural_card = store_thm( 371 "natural_card", 372 ``!n. CARD (natural n) = n``, 373 rw[CARD_IMAGE_SUC]); 374 375(* Theorem: 0 NOTIN (natural n) *) 376(* Proof: by NOT_SUC *) 377val natural_not_0 = store_thm( 378 "natural_not_0", 379 ``!n. 0 NOTIN (natural n)``, 380 rw[]); 381 382(* Theorem: natural 0 = {} *) 383(* Proof: 384 natural 0 385 = IMAGE SUC (count 0) by notation 386 = IMAGE SUC {} by COUNT_ZERO 387 = {} by IMAGE_EMPTY 388*) 389val natural_0 = store_thm( 390 "natural_0", 391 ``natural 0 = {}``, 392 rw[]); 393 394(* Theorem: natural 1 = {1} *) 395(* Proof: 396 natural 1 397 = IMAGE SUC (count 1) by notation 398 = IMAGE SUC {0} by count_add1 399 = {SUC 0} by IMAGE_DEF 400 = {1} by ONE 401*) 402val natural_1 = store_thm( 403 "natural_1", 404 ``natural 1 = {1}``, 405 rw[EXTENSION, EQ_IMP_THM]); 406 407(* Theorem: 0 < n ==> 1 IN (natural n) *) 408(* Proof: by natural_element, LESS_OR, ONE *) 409val natural_has_1 = store_thm( 410 "natural_has_1", 411 ``!n. 0 < n ==> 1 IN (natural n)``, 412 rw[natural_element]); 413 414(* Theorem: 0 < n ==> n IN (natural n) *) 415(* Proof: by natural_element *) 416val natural_has_last = store_thm( 417 "natural_has_last", 418 ``!n. 0 < n ==> n IN (natural n)``, 419 rw[natural_element]); 420 421(* Theorem: natural (SUC n) = (SUC n) INSERT (natural n) *) 422(* Proof: 423 natural (SUC n) 424 <=> {j | 0 < j /\ j <= (SUC n)} by natural_property 425 <=> {j | 0 < j /\ (j <= n \/ (j = SUC n))} by LE 426 <=> {j | j IN (natural n) \/ (j = SUC n)} by natural_property 427 <=> (SUC n) INSERT (natural n) by INSERT_DEF 428*) 429val natural_suc = store_thm( 430 "natural_suc", 431 ``!n. natural (SUC n) = (SUC n) INSERT (natural n)``, 432 rw[EXTENSION, EQ_IMP_THM]); 433 434(* Theorem: natural n = set (GENLIST SUC n) *) 435(* Proof: 436 By induction on n. 437 Base: natural 0 = set (GENLIST SUC 0) 438 LHS = natural 0 = {} by natural_0 439 RHS = set (GENLIST SUC 0) 440 = set [] by GENLIST_0 441 = {} by LIST_TO_SET 442 Step: natural n = set (GENLIST SUC n) ==> 443 natural (SUC n) = set (GENLIST SUC (SUC n)) 444 natural (SUC n) 445 = SUC n INSERT natural n by natural_suc 446 = SUC n INSERT (set (GENLIST SUC n)) by induction hypothesis 447 = set (SNOC (SUC n) (GENLIST SUC n)) by LIST_TO_SET_SNOC 448 = set (GENLIST SUC (SUC n)) by GENLIST 449*) 450val natural_thm = store_thm( 451 "natural_thm", 452 ``!n. natural n = set (GENLIST SUC n)``, 453 Induct >- 454 rw[] >> 455 rw[natural_suc, LIST_TO_SET_SNOC, GENLIST]); 456 457(* Theorem: 0 < n /\ a IN (natural n) /\ b divides a ==> b IN (natural n) *) 458(* Proof: 459 By natural_element, this is to show: 460 (1) 0 < a /\ b divides a ==> 0 < b 461 True by divisor_pos 462 (2) 0 < a /\ b divides a ==> b <= n 463 Since b divides a 464 ==> b <= a by DIVIDES_LE, 0 < a 465 ==> b <= n by LESS_EQ_TRANS 466*) 467val natural_divisor_natural = store_thm( 468 "natural_divisor_natural", 469 ``!n a b. 0 < n /\ a IN (natural n) /\ b divides a ==> b IN (natural n)``, 470 rw[natural_element] >- 471 metis_tac[divisor_pos] >> 472 metis_tac[DIVIDES_LE, LESS_EQ_TRANS]); 473 474(* Theorem: 0 < n /\ 0 < a /\ b IN (natural n) /\ a divides b ==> (b DIV a) IN (natural n) *) 475(* Proof: 476 Let c = b DIV a. 477 By natural_element, this is to show: 478 0 < a /\ 0 < b /\ b <= n /\ a divides b ==> 0 < c /\ c <= n 479 Since a divides b ==> b = c * a by DIVIDES_EQN, 0 < a 480 so b = a * c by MULT_COMM 481 or c divides b by divides_def 482 Thus 0 < c /\ c <= b by divides_pos 483 or c <= n by LESS_EQ_TRANS 484*) 485val natural_cofactor_natural = store_thm( 486 "natural_cofactor_natural", 487 ``!n a b. 0 < n /\ 0 < a /\ b IN (natural n) /\ a divides b ==> (b DIV a) IN (natural n)``, 488 rewrite_tac[natural_element] >> 489 ntac 4 strip_tac >> 490 qabbrev_tac `c = b DIV a` >> 491 `b = c * a` by rw[GSYM DIVIDES_EQN, Abbr`c`] >> 492 `c divides b` by metis_tac[divides_def, MULT_COMM] >> 493 `0 < c /\ c <= b` by metis_tac[divides_pos] >> 494 decide_tac); 495 496(* Theorem: 0 < n /\ a divides n /\ b IN (natural n) /\ a divides b ==> (b DIV a) IN (natural (n DIV a)) *) 497(* Proof: 498 Let c = b DIV a. 499 By natural_element, this is to show: 500 0 < n /\ a divides b /\ 0 < b /\ b <= n /\ a divides b ==> 0 < c /\ c <= n DIV a 501 Note 0 < a by ZERO_DIVIES, 0 < n 502 Since a divides b ==> b = c * a by DIVIDES_EQN, 0 < a [1] 503 or c divides b by divides_def, MULT_COMM 504 Thus 0 < c, since 0 divides b means b = 0. by ZERO_DIVIDES, b <> 0 505 Now n = (n DIV a) * a by DIVIDES_EQN, 0 < a [2] 506 With b <= n, c * a <= (n DIV a) * a by [1], [2] 507 Hence c <= n DIV a by LE_MULT_RCANCEL, a <> 0 508*) 509val natural_cofactor_natural_reduced = store_thm( 510 "natural_cofactor_natural_reduced", 511 ``!n a b. 0 < n /\ a divides n /\ 512 b IN (natural n) /\ a divides b ==> (b DIV a) IN (natural (n DIV a))``, 513 rewrite_tac[natural_element] >> 514 ntac 4 strip_tac >> 515 qabbrev_tac `c = b DIV a` >> 516 `a <> 0` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >> 517 `(b = c * a) /\ (n = (n DIV a) * a)` by rw[GSYM DIVIDES_EQN, Abbr`c`] >> 518 `c divides b` by metis_tac[divides_def, MULT_COMM] >> 519 `0 < c` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >> 520 metis_tac[LE_MULT_RCANCEL]); 521 522(* ------------------------------------------------------------------------- *) 523(* Uptos -- counting from 0 and inclusive. *) 524(* ------------------------------------------------------------------------- *) 525 526(* Overload on another count-related set *) 527val _ = overload_on("upto", ``\n. count (SUC n)``); 528 529(* Theorem: FINITE (upto n) *) 530(* Proof: by FINITE_COUNT *) 531val upto_finite = store_thm( 532 "upto_finite", 533 ``!n. FINITE (upto n)``, 534 rw[]); 535 536(* Theorem: CARD (upto n) = SUC n *) 537(* Proof: by CARD_COUNT *) 538val upto_card = store_thm( 539 "upto_card", 540 ``!n. CARD (upto n) = SUC n``, 541 rw[]); 542 543(* Theorem: n IN (upto n) *) 544(* Proof: byLESS_SUC_REFL *) 545val upto_has_last = store_thm( 546 "upto_has_last", 547 ``!n. n IN (upto n)``, 548 rw[]); 549 550(* Theorem: upto n = {0} UNION (natural n) *) 551(* Proof: 552 By UNION_DEF, EXTENSION, this is to show: 553 (1) x < SUC n ==> (x = 0) \/ ?x'. (x = SUC x') /\ x' < n 554 If x = 0, trivially true. 555 If x <> 0, x = SUC m. 556 Take x' = m, 557 then SUC m = x < SUC n ==> m < n by LESS_MONO_EQ 558 (2) (x = 0) \/ ?x'. (x = SUC x') /\ x' < n ==> x < SUC n 559 If x = 0, 0 < SUC n by SUC_POS 560 If ?x'. (x = SUC x') /\ x' < n, 561 x' < n ==> SUC x' = x < SUC n by LESS_MONO_EQ 562*) 563val upto_split_first = store_thm( 564 "upto_split_first", 565 ``!n. upto n = {0} UNION (natural n)``, 566 rw[EXTENSION, EQ_IMP_THM] >> 567 Cases_on `x` >- 568 rw[] >> 569 metis_tac[LESS_MONO_EQ]); 570 571(* Theorem: upto n = (count n) UNION {n} *) 572(* Proof: 573 By UNION_DEF, EXTENSION, this is to show: 574 (1) x < SUC n ==> x < n \/ (x = n) 575 True by LESS_THM. 576 (2) x < n \/ (x = n) ==> x < SUC n 577 True by LESS_THM. 578*) 579val upto_split_last = store_thm( 580 "upto_split_last", 581 ``!n. upto n = (count n) UNION {n}``, 582 rw[EXTENSION, EQ_IMP_THM]); 583 584(* Theorem: upto n = n INSERT (count n) *) 585(* Proof: 586 upto n 587 = count (SUC n) by notation 588 = {x | x < SUC n} by count_def 589 = {x | (x = n) \/ (x < n)} by prim_recTheory.LESS_THM 590 = x INSERT {x| x < n} by INSERT_DEF 591 = x INSERT (count n) by count_def 592*) 593val upto_by_count = store_thm( 594 "upto_by_count", 595 ``!n. upto n = n INSERT (count n)``, 596 rw[EXTENSION]); 597 598(* Theorem: upto n = 0 INSERT (natural n) *) 599(* Proof: 600 upto n 601 = count (SUC n) by notation 602 = {x | x < SUC n} by count_def 603 = {x | ((x = 0) \/ (?m. x = SUC m)) /\ x < SUC n)} by num_CASES 604 = {x | (x = 0 /\ x < SUC n) \/ (?m. x = SUC m /\ x < SUC n)} by SUC_POS 605 = 0 INSERT {SUC m | SUC m < SUC n} by INSERT_DEF 606 = 0 INSERT {SUC m | m < n} by LESS_MONO_EQ 607 = 0 INSERT (IMAGE SUC (count n)) by IMAGE_DEF 608 = 0 INSERT (natural n) by notation 609*) 610val upto_by_natural = store_thm( 611 "upto_by_natural", 612 ``!n. upto n = 0 INSERT (natural n)``, 613 rw[EXTENSION] >> 614 metis_tac[num_CASES, LESS_MONO_EQ, SUC_POS]); 615 616(* Theorem: natural n = count (SUC n) DELETE 0 *) 617(* Proof: 618 count (SUC n) DELETE 0 619 = {x | x < SUC n} DELETE 0 by count_def 620 = {x | x < SUC n} DIFF {0} by DELETE_DEF 621 = {x | x < SUC n /\ x <> 0} by DIFF_DEF 622 = {SUC m | SUC m < SUC n} by num_CASES 623 = {SUC m | m < n} by LESS_MONO_EQ 624 = IMAGE SUC (count n) by IMAGE_DEF 625 = natural n by notation 626*) 627val natural_by_upto = store_thm( 628 "natural_by_upto", 629 ``!n. natural n = count (SUC n) DELETE 0``, 630 (rw[EXTENSION, EQ_IMP_THM] >> metis_tac[num_CASES, LESS_MONO_EQ])); 631 632(* ------------------------------------------------------------------------- *) 633(* Euler Set and Totient Function *) 634(* ------------------------------------------------------------------------- *) 635 636(* Euler's totient function *) 637val Euler_def = zDefine` 638 Euler n = { i | 0 < i /\ i < n /\ (gcd n i = 1) } 639`; 640(* that is, Euler n = { i | i in (residue n) /\ (gcd n i = 1) }`; *) 641(* use zDefine as this is not computationally effective. *) 642 643val totient_def = Define` 644 totient n = CARD (Euler n) 645`; 646 647(* Theorem: x IN (Euler n) <=> 0 < x /\ x < n /\ coprime n x *) 648(* Proof: by Euler_def. *) 649val Euler_element = store_thm( 650 "Euler_element", 651 ``!n x. x IN (Euler n) <=> 0 < x /\ x < n /\ coprime n x``, 652 rw[Euler_def]); 653 654(* Theorem: Euler n = (residue n) INTER {j | coprime j n} *) 655(* Proof: by Euler_def, residue_def, EXTENSION, IN_INTER *) 656val Euler_thm = store_thm( 657 "Euler_thm[compute]", 658 ``!n. Euler n = (residue n) INTER {j | coprime j n}``, 659 rw[Euler_def, residue_def, GCD_SYM, EXTENSION]); 660(* This is effective, put in computeLib. *) 661 662(* 663> EVAL ``Euler 10``; 664val it = |- Euler 10 = {9; 7; 3; 1}: thm 665> EVAL ``totient 10``; 666val it = |- totient 10 = 4: thm 667*) 668 669(* Theorem: FINITE (Euler n) *) 670(* Proof: 671 Since (Euler n) SUBSET count n by Euler_def, SUBSET_DEF 672 and FINITE (count n) by FINITE_COUNT 673 ==> FINITE (Euler n) by SUBSET_FINITE 674*) 675val Euler_finite = store_thm( 676 "Euler_finite", 677 ``!n. FINITE (Euler n)``, 678 rpt strip_tac >> 679 `(Euler n) SUBSET count n` by rw[Euler_def, SUBSET_DEF] >> 680 metis_tac[FINITE_COUNT, SUBSET_FINITE]); 681 682(* Theorem: Euler 0 = {} *) 683(* Proof: by Euler_def *) 684val Euler_0 = store_thm( 685 "Euler_0", 686 ``Euler 0 = {}``, 687 rw[Euler_def]); 688 689(* Theorem: Euler 1 = {} *) 690(* Proof: by Euler_def *) 691val Euler_1 = store_thm( 692 "Euler_1", 693 ``Euler 1 = {}``, 694 rw[Euler_def]); 695 696(* Theorem: 1 < n ==> 1 IN (Euler n) *) 697(* Proof: by Euler_def *) 698val Euler_has_1 = store_thm( 699 "Euler_has_1", 700 ``!n. 1 < n ==> 1 IN (Euler n)``, 701 rw[Euler_def]); 702 703(* Theorem: 1 < n ==> (Euler n) <> {} *) 704(* Proof: by Euler_has_1, MEMBER_NOT_EMPTY *) 705val Euler_nonempty = store_thm( 706 "Euler_nonempty", 707 ``!n. 1 < n ==> (Euler n) <> {}``, 708 metis_tac[Euler_has_1, MEMBER_NOT_EMPTY]); 709 710(* Theorem: (Euler n = {}) <=> ((n = 0) \/ (n = 1)) *) 711(* Proof: 712 If part: Euler n = {} ==> n = 0 \/ n = 1 713 By contradiction, suppose ~(n = 0 \/ n = 1). 714 Then 1 < n, but Euler n <> {} by Euler_nonempty 715 This contradicts Euler n = {}. 716 Only-if part: n = 0 \/ n = 1 ==> Euler n = {} 717 Note Euler 0 = {} by Euler_0 718 and Euler 1 = {} by Euler_1 719*) 720val Euler_empty = store_thm( 721 "Euler_empty", 722 ``!n. (Euler n = {}) <=> ((n = 0) \/ (n = 1))``, 723 rw[EQ_IMP_THM] >| [ 724 spose_not_then strip_assume_tac >> 725 `1 < n` by decide_tac >> 726 metis_tac[Euler_nonempty], 727 rw[Euler_0], 728 rw[Euler_1] 729 ]); 730 731(* Theorem: totient n <= n *) 732(* Proof: 733 Since (Euler n) SUBSET count n by Euler_def, SUBSET_DEF 734 and FINITE (count n) by FINITE_COUNT 735 and (CARD (count n) = n by CARD_COUNT 736 Hence CARD (Euler n) <= n by CARD_SUBSET 737 or totient n <= n by totient_def 738*) 739val Euler_card_upper_le = store_thm( 740 "Euler_card_upper_le", 741 ``!n. totient n <= n``, 742 rpt strip_tac >> 743 `(Euler n) SUBSET count n` by rw[Euler_def, SUBSET_DEF] >> 744 metis_tac[totient_def, CARD_SUBSET, FINITE_COUNT, CARD_COUNT]); 745 746(* Theorem: 1 < n ==> totient n < n *) 747(* Proof: 748 First, (Euler n) SUBSET count n by Euler_def, SUBSET_DEF 749 Now, ~(coprime 0 n) by coprime_0L, n <> 1 750 so 0 NOTIN (Euler n) by Euler_def 751 but 0 IN (count n) by IN_COUNT, 0 < n 752 Thus (Euler n) <> (count n) by EXTENSION 753 and (Euler n) PSUBSET (count n) by PSUBSET_DEF 754 Since FINITE (count n) by FINITE_COUNT 755 and (CARD (count n) = n by CARD_COUNT 756 Hence CARD (Euler n) < n by CARD_PSUBSET 757 or totient n < n by totient_def 758*) 759val Euler_card_upper_lt = store_thm( 760 "Euler_card_upper_lt", 761 ``!n. 1 < n ==> totient n < n``, 762 rpt strip_tac >> 763 `(Euler n) SUBSET count n` by rw[Euler_def, SUBSET_DEF] >> 764 `0 < n /\ n <> 1` by decide_tac >> 765 `~(coprime 0 n)` by metis_tac[coprime_0L] >> 766 `0 NOTIN (Euler n)` by rw[Euler_def] >> 767 `0 IN (count n)` by rw[] >> 768 `(Euler n) <> (count n)` by metis_tac[EXTENSION] >> 769 `(Euler n) PSUBSET (count n)` by rw[PSUBSET_DEF] >> 770 metis_tac[totient_def, CARD_PSUBSET, FINITE_COUNT, CARD_COUNT]); 771 772(* Theorem: (totient n <= n) /\ (1 < n ==> 0 < totient n /\ totient n < n) *) 773(* Proof: 774 This is to show: 775 (1) totient n <= n, 776 True by Euler_card_upper_le. 777 (2) 1 < n ==> 0 < totient n 778 Since (Euler n) <> {} by Euler_nonempty 779 Also FINITE (Euler n) by Euler_finite 780 Hence CARD (Euler n) <> 0 by CARD_EQ_0 781 or 0 < totient n by totient_def 782 (3) 1 < n ==> totient n < n 783 True by Euler_card_upper_lt. 784*) 785val Euler_card_bounds = store_thm( 786 "Euler_card_bounds", 787 ``!n. (totient n <= n) /\ (1 < n ==> 0 < totient n /\ totient n < n)``, 788 rw[] >- 789 rw[Euler_card_upper_le] >- 790 (`(Euler n) <> {}` by rw[Euler_nonempty] >> 791 `FINITE (Euler n)` by rw[Euler_finite] >> 792 `totient n <> 0` by metis_tac[totient_def, CARD_EQ_0] >> 793 decide_tac) >> 794 rw[Euler_card_upper_lt]); 795 796(* Theorem: For prime p, (Euler p = residue p) *) 797(* Proof: 798 By Euler_def, residue_def, this is to show: 799 For prime p, gcd p x = 1 for 0 < x < p. 800 Since x < p, x does not divide p, result follows by PRIME_GCD. 801 or, this is true by prime_coprime_all_lt 802*) 803val Euler_prime = store_thm( 804 "Euler_prime", 805 ``!p. prime p ==> (Euler p = residue p)``, 806 rw[Euler_def, residue_def, EXTENSION, EQ_IMP_THM] >> 807 rw[prime_coprime_all_lt]); 808 809(* Theorem: For prime p, totient p = p - 1 *) 810(* Proof: 811 totient p 812 = CARD (Euler p) by totient_def 813 = CARD (residue p) by Euler_prime 814 = p - 1 by residue_card, and prime p > 0. 815*) 816val Euler_card_prime = store_thm( 817 "Euler_card_prime", 818 ``!p. prime p ==> (totient p = p - 1)``, 819 rw[totient_def, Euler_prime, residue_card, PRIME_POS]); 820 821(* ------------------------------------------------------------------------- *) 822(* Summation of Geometric Sequence *) 823(* ------------------------------------------------------------------------- *) 824 825(* Geometric Series: 826 Let s = p + p ** 2 + p ** 3 827 p * s = p ** 2 + p ** 3 + p ** 4 828 p * s - s = p ** 4 - p 829 (p - 1) * s = p * (p ** 3 - 1) 830*) 831 832(* Theorem: 0 < p ==> !n. (p - 1) * SIGMA (\j. p ** j) (natural n) = p * (p ** n - 1) *) 833(* Proof: 834 By induction on n. 835 Base: (p - 1) * SIGMA (\j. p ** j) (natural 0) = p * (p ** 0 - 1) 836 LHS = (p - 1) * SIGMA (\j. p ** j) (natural 0) 837 = (p - 1) * SIGMA (\j. p ** j) {} by natural_0 838 = (p - 1) * 0 by SUM_IMAGE_EMPTY 839 = 0 by MULT_0 840 RHS = p * (p ** 0 - 1) 841 = p * (1 - 1) by EXP 842 = p * 0 by SUB_EQUAL_0 843 = 0 = LHS by MULT_0 844 Step: (p - 1) * SIGMA (\j. p ** j) (natural n) = p * (p ** n - 1) ==> 845 (p - 1) * SIGMA (\j. p ** j) (natural (SUC n)) = p * (p ** SUC n - 1) 846 Note FINITE (natural n) by natural_finite 847 and (SUC n) NOTIN (natural n) by natural_element 848 Also p <= p ** (SUC n) by X_LE_X_EXP, SUC_POS 849 and 1 <= p by 0 < p 850 thus p ** (SUC n) <> 0 by EXP_POS, 0 < p 851 so p ** (SUC n) <= p * p ** (SUC n) by LE_MULT_LCANCEL, p ** (SUC n) <> 0 852 (p - 1) * SIGMA (\j. p ** j) (natural (SUC n)) 853 = (p - 1) * SIGMA (\j. p ** j) ((SUC n) INSERT (natural n)) by natural_suc 854 = (p - 1) * ((p ** SUC n) + SIGMA (\j. p ** j) ((natural n) DELETE (SUC n))) by SUM_IMAGE_THM 855 = (p - 1) * ((p ** SUC n) + SIGMA (\j. p ** j) (natural n)) by DELETE_NON_ELEMENT 856 = (p - 1) * (p ** SUC n) + (p - 1) * SIGMA (\j. p ** j) (natural n) by LEFT_ADD_DISTRIB 857 = (p - 1) * (p ** SUC n) + p * (p ** n - 1) by induction hypothesis 858 = (p - 1) * (p ** SUC n) + (p * p ** n - p) by LEFT_SUB_DISTRIB 859 = (p - 1) * (p ** SUC n) + (p ** (SUC n) - p) by EXP 860 = (p * p ** SUC n - p ** SUC n) + (p ** SUC n - p) by RIGHT_SUB_DISTRIB 861 = (p * p ** SUC n - p ** SUC n + p ** SUC n - p by LESS_EQ_ADD_SUB, p <= p ** (SUC n) 862 = p ** p ** SUC n - p by SUB_ADD, p ** (SUC n) <= p * p ** (SUC n) 863 = p * (p ** SUC n - 1) by LEFT_SUB_DISTRIB 864 *) 865val sigma_geometric_natural_eqn = store_thm( 866 "sigma_geometric_natural_eqn", 867 ``!p. 0 < p ==> !n. (p - 1) * SIGMA (\j. p ** j) (natural n) = p * (p ** n - 1)``, 868 rpt strip_tac >> 869 Induct_on `n` >- 870 rw_tac std_ss[natural_0, SUM_IMAGE_EMPTY, EXP, MULT_0] >> 871 `FINITE (natural n)` by rw[natural_finite] >> 872 `(SUC n) NOTIN (natural n)` by rw[natural_element] >> 873 qabbrev_tac `q = p ** SUC n` >> 874 `p <= q` by rw[X_LE_X_EXP, Abbr`q`] >> 875 `1 <= p` by decide_tac >> 876 `q <> 0` by rw[EXP_POS, Abbr`q`] >> 877 `q <= p * q` by rw[LE_MULT_LCANCEL] >> 878 `(p - 1) * SIGMA (\j. p ** j) (natural (SUC n)) 879 = (p - 1) * SIGMA (\j. p ** j) ((SUC n) INSERT (natural n))` by rw[natural_suc] >> 880 `_ = (p - 1) * (q + SIGMA (\j. p ** j) ((natural n) DELETE (SUC n)))` by rw[SUM_IMAGE_THM, Abbr`q`] >> 881 `_ = (p - 1) * (q + SIGMA (\j. p ** j) (natural n))` by metis_tac[DELETE_NON_ELEMENT] >> 882 `_ = (p - 1) * q + (p - 1) * SIGMA (\j. p ** j) (natural n)` by rw[LEFT_ADD_DISTRIB] >> 883 `_ = (p - 1) * q + p * (p ** n - 1)` by rw[] >> 884 `_ = (p - 1) * q + (p * p ** n - p)` by rw[LEFT_SUB_DISTRIB] >> 885 `_ = (p - 1) * q + (q - p)` by rw[EXP, Abbr`q`] >> 886 `_ = (p * q - q) + (q - p)` by rw[RIGHT_SUB_DISTRIB] >> 887 `_ = (p * q - q + q) - p` by rw[LESS_EQ_ADD_SUB] >> 888 `_ = p * q - p` by rw[SUB_ADD] >> 889 `_ = p * (q - 1)` by rw[LEFT_SUB_DISTRIB] >> 890 rw[]); 891 892(* Theorem: 1 < p ==> !n. SIGMA (\j. p ** j) (natural n) = (p * (p ** n - 1)) DIV (p - 1) *) 893(* Proof: 894 Since 1 < p, 895 ==> 0 < p - 1, and 0 < p by arithmetic 896 Let t = SIGMA (\j. p ** j) (natural n) 897 With 0 < p, 898 (p - 1) * t = p * (p ** n - 1) by sigma_geometric_natural_eqn, 0 < p 899 Hence t = (p * (p ** n - 1)) DIV (p - 1) by DIV_SOLVE, 0 < (p - 1) 900*) 901val sigma_geometric_natural = store_thm( 902 "sigma_geometric_natural", 903 ``!p. 1 < p ==> !n. SIGMA (\j. p ** j) (natural n) = (p * (p ** n - 1)) DIV (p - 1)``, 904 rpt strip_tac >> 905 `0 < p - 1 /\ 0 < p` by decide_tac >> 906 rw[sigma_geometric_natural_eqn, DIV_SOLVE]); 907 908(* ------------------------------------------------------------------------- *) 909(* Useful Theorems *) 910(* ------------------------------------------------------------------------- *) 911 912(* Note: 913 count m = {i | i < m} defined in pred_set 914 residue m = {i | 0 < i /\ i < m} defined in Euler 915 The difference i = 0 gives n ** 0 = 1, which does not make a difference for PROD_SET. 916*) 917 918(* Theorem: 1 < n /\ 0 < m ==> 919 (PROD_SET (IMAGE (\j. n ** j) (count m)) = PROD_SET (IMAGE (\j. n ** j) (residue m))) *) 920(* Proof: 921 Since 0 IN count m by IN_COUNT, 0 < m 922 and (IMAGE (\j. n ** j) (count m)) DELETE 1 = IMAGE (\j. n ** j) (residue m) 923 by IMAGE_DEF, EXP_EQ_1, EXP 924 PROD_SET (IMAGE (\j. n ** j) (count m)) 925 = PROD_SET (IMAGE (\j. n ** j) (0 INSERT count m)) by ABSORPTION 926 = PROD_SET ((\j. n ** j) 0 INSERT IMAGE (\j. n ** j) (count m)) by IMAGE_INSERT 927 = n ** 0 * PROD_SET ((IMAGE (\j. n ** j) (count m)) DELETE n ** 0) by PROD_SET_THM 928 = PROD_SET ((IMAGE (\j. n ** j) (count m)) DELETE 1) by EXP 929 = PROD_SET ((IMAGE (\j. n ** j) (residue m))) by above 930*) 931val PROD_SET_IMAGE_EXP_NONZERO = store_thm( 932 "PROD_SET_IMAGE_EXP_NONZERO", 933 ``!n m. 1 < n /\ 0 < m ==> 934 (PROD_SET (IMAGE (\j. n ** j) (count m)) = PROD_SET (IMAGE (\j. n ** j) (residue m)))``, 935 rpt strip_tac >> 936 `0 IN count m` by rw[] >> 937 `FINITE (IMAGE (\j. n ** j) (count m))` by rw[] >> 938 `(IMAGE (\j. n ** j) (count m)) DELETE 1 = IMAGE (\j. n ** j) (residue m)` by 939 (rw[residue_def, IMAGE_DEF, EXTENSION, EQ_IMP_THM] >- 940 metis_tac[EXP, NOT_ZERO_LT_ZERO] >- 941 metis_tac[] >> 942 `j <> 0 /\ n <> 1` by decide_tac >> 943 metis_tac[EXP_EQ_1] 944 ) >> 945 `PROD_SET (IMAGE (\j. n ** j) (count m)) = PROD_SET (IMAGE (\j. n ** j) (0 INSERT count m))` by metis_tac[ABSORPTION] >> 946 `_ = PROD_SET ((\j. n ** j) 0 INSERT IMAGE (\j. n ** j) (count m))` by rw[] >> 947 `_ = n ** 0 * PROD_SET ((IMAGE (\j. n ** j) (count m)) DELETE n ** 0)` by rw[PROD_SET_THM] >> 948 `_ = PROD_SET ((IMAGE (\j. n ** j) (count m)) DELETE 1)` by rw[EXP] >> 949 `_ = PROD_SET ((IMAGE (\j. n ** j) (residue m)))` by rw[] >> 950 decide_tac); 951 952(* ------------------------------------------------------------------------- *) 953 954(* export theory at end *) 955val _ = export_theory(); 956 957(*===========================================================================*) 958