1(* ------------------------------------------------------------------------- *) 2(* Gauss' Little Theorem. *) 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 "Gauss"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* val _ = load "jcLib"; *) 17open jcLib; 18 19(* open dependent theories *) 20open arithmeticTheory pred_setTheory listTheory; 21 22(* Get dependent theories in lib *) 23(* val _ = load "helperListTheory"; *) 24open helperListTheory; 25 26(* val _ = load "EulerTheory"; *) 27open EulerTheory; 28(* (* val _ = load "helperFunctionTheory"; -- in EulerTheory *) *) 29(* (* val _ = load "helperNumTheory"; -- in helperFunctionTheory *) *) 30(* (* val _ = load "helperSetTheory"; -- in helperFunctionTheory *) *) 31open helperNumTheory helperSetTheory helperFunctionTheory; 32 33(* (* val _ = load "dividesTheory"; -- in helperNumTheory *) *) 34(* (* val _ = load "gcdTheory"; -- in helperNumTheory *) *) 35open dividesTheory gcdTheory; 36 37 38(* ------------------------------------------------------------------------- *) 39(* Gauss' Little Theorem *) 40(* ------------------------------------------------------------------------- *) 41(* Overloading: 42*) 43(* Definitions and Theorems (# are exported, ! in computeLib): 44 45 Helper Theorems: 46 47 Coprimes: 48 coprimes_def |- !n. coprimes n = {j | j IN natural n /\ coprime j n} 49 coprimes_element |- !n j. j IN coprimes n <=> 0 < j /\ j <= n /\ coprime j n 50! coprimes_alt |- !n. coprimes n = natural n INTER {j | coprime j n} 51 coprimes_thm |- !n. coprimes n = set (FILTER (\j. coprime j n) (GENLIST SUC n)) 52 coprimes_subset |- !n. coprimes n SUBSET natural n 53 coprimes_finite |- !n. FINITE (coprimes n) 54 coprimes_0 |- coprimes 0 = {} 55 coprimes_1 |- coprimes 1 = {1} 56 coprimes_has_1 |- !n. 0 < n ==> 1 IN coprimes n 57 coprimes_eq_empty |- !n. (coprimes n = {}) <=> (n = 0) 58 coprimes_no_0 |- !n. 0 NOTIN coprimes n 59 coprimes_without_last |- !n. 1 < n ==> n NOTIN coprimes n 60 coprimes_with_last |- !n. n IN coprimes n <=> (n = 1) 61 coprimes_has_last_but_1 |- !n. 1 < n ==> n - 1 IN coprimes n 62 coprimes_element_less |- !n. 1 < n ==> !j. j IN coprimes n ==> j < n 63 coprimes_element_alt |- !n. 1 < n ==> !j. j IN coprimes n <=> j < n /\ coprime j n 64 coprimes_max |- !n. 1 < n ==> (MAX_SET (coprimes n) = n - 1) 65 coprimes_eq_Euler |- !n. 1 < n ==> (coprimes n = Euler n) 66 coprimes_prime |- !n. prime n ==> (coprimes n = residue n) 67 68 Coprimes by a divisor: 69 coprimes_by_def |- !n d. coprimes_by n d = if 0 < n /\ d divides n then coprimes (n DIV d) else {} 70 coprimes_by_element |- !n d j. j IN coprimes_by n d <=> 0 < n /\ d divides n /\ j IN coprimes (n DIV d) 71 coprimes_by_finite |- !n d. FINITE (coprimes_by n d) 72 coprimes_by_0 |- !d. coprimes_by 0 d = {} 73 coprimes_by_by_0 |- !n. coprimes_by n 0 = {} 74 coprimes_by_by_1 |- !n. 0 < n ==> (coprimes_by n 1 = coprimes n) 75 coprimes_by_by_last |- !n. 0 < n ==> (coprimes_by n n = {1}) 76 coprimes_by_by_divisor |- !n d. 0 < n /\ d divides n ==> (coprimes_by n d = coprimes (n DIV d)) 77 coprimes_by_eq_empty |- !n d. 0 < n ==> ((coprimes_by n d = {}) <=> ~(d divides n)) 78 79 GCD Equivalence Class: 80 gcd_matches_def |- !n d. gcd_matches n d = {j | j IN natural n /\ (gcd j n = d)} 81! gcd_matches_alt |- !n d. gcd_matches n d = natural n INTER {j | gcd j n = d} 82 gcd_matches_element |- !n d j. j IN gcd_matches n d <=> 0 < j /\ j <= n /\ (gcd j n = d) 83 gcd_matches_subset |- !n d. gcd_matches n d SUBSET natural n 84 gcd_matches_finite |- !n d. FINITE (gcd_matches n d) 85 gcd_matches_0 |- !d. gcd_matches 0 d = {} 86 gcd_matches_with_0 |- !n. gcd_matches n 0 = {} 87 gcd_matches_1 |- !d. gcd_matches 1 d = if d = 1 then {1} else {} 88 gcd_matches_has_divisor |- !n d. 0 < n /\ d divides n ==> d IN gcd_matches n d 89 gcd_matches_element_divides |- !n d j. j IN gcd_matches n d ==> d divides j /\ d divides n 90 gcd_matches_eq_empty |- !n d. 0 < n ==> ((gcd_matches n d = {}) <=> ~(d divides n)) 91 92 Phi Function: 93 phi_def |- !n. phi n = CARD (coprimes n) 94 phi_thm |- !n. phi n = LENGTH (FILTER (\j. coprime j n) (GENLIST SUC n)) 95 phi_fun |- phi = CARD o coprimes 96 phi_pos |- !n. 0 < n ==> 0 < phi n 97 phi_0 |- phi 0 = 0 98 phi_eq_0 |- !n. (phi n = 0) <=> (n = 0) 99 phi_1 |- phi 1 = 1 100 phi_eq_totient |- !n. 1 < n ==> (phi n = totient n) 101 phi_prime |- !n. prime n ==> (phi n = n - 1) 102 phi_2 |- phi 2 = 1 103 phi_gt_1 |- !n. 2 < n ==> 1 < phi n 104 phi_le |- !n. phi n <= n 105 phi_lt |- !n. 1 < n ==> phi n < n 106 107 Divisors: 108 divisors_def |- !n. divisors n = {d | d <= n /\ d divides n} 109 divisors_element |- !n d. d IN divisors n <=> d <= n /\ d divides n 110 divisors_element_alt |- !n. 0 < n ==> !d. d IN divisors n <=> d divides n 111 divisors_has_one |- !n. 0 < n ==> 1 IN divisors n 112 divisors_has_last |- !n. n IN divisors n 113 divisors_not_empty |- !n. divisors n <> {} 114! divisors_eqn |- !n. divisors n = 115 if n = 0 then {0} 116 else IMAGE (\j. if j + 1 divides n then j + 1 else 1) (count n) 117 divisors_cofactor |- !n d. 0 < n /\ d IN divisors n ==> n DIV d IN divisors n 118 divisors_delete_last |- !n. 0 < n ==> (divisors n DELETE n = {m | m < n /\ m divides n}) 119 divisors_nonzero |- !n. 0 < n ==> !d. d IN divisors n ==> 0 < d 120 divisors_has_cofactor |- !n. 0 < n ==> !d. d IN divisors n ==> n DIV d IN divisors n 121 divisors_subset_upto |- !n. divisors n SUBSET upto n 122 divisors_subset_natural |- !n. 0 < n ==> divisors n SUBSET natural n 123 divisors_finite |- !n. FINITE (divisors n) 124 divisors_0 |- divisors 0 = {0} 125 divisors_1 |- divisors 1 = {1} 126 divisors_has_0 |- !n. 0 IN divisors n <=> (n = 0) 127 divisors_divisors_bij |- !n. 0 < n ==> (\d. n DIV d) PERMUTES divisors n 128 129 Gauss' Little Theorem: 130 gcd_matches_divisor_element |- !n d. d divides n ==> 131 !j. j IN gcd_matches n d ==> j DIV d IN coprimes_by n d 132 gcd_matches_bij_coprimes_by |- !n d. d divides n ==> 133 BIJ (\j. j DIV d) (gcd_matches n d) (coprimes_by n d) 134 gcd_matches_bij_coprimes |- !n d. 0 < n /\ d divides n ==> 135 BIJ (\j. j DIV d) (gcd_matches n d) (coprimes (n DIV d)) 136 divisors_eq_gcd_image |- !n. 0 < n ==> (divisors n = IMAGE (gcd n) (natural n)) 137 gcd_eq_equiv_class |- !n d. feq_class (gcd n) (natural n) d = gcd_matches n d 138 gcd_eq_equiv_class_fun |- !n. feq_class (gcd n) (natural n) = gcd_matches n 139 gcd_eq_partition_by_divisors |- !n. 0 < n ==> (partition (feq (gcd n)) (natural n) = 140 IMAGE (gcd_matches n) (divisors n)) 141 gcd_eq_equiv_on_natural |- !n. feq (gcd n) equiv_on natural n 142 sum_over_natural_by_gcd_partition 143 |- !f n. SIGMA f (natural n) = 144 SIGMA (SIGMA f) (partition (feq (gcd n)) (natural n)) 145 sum_over_natural_by_divisors |- !f n. SIGMA f (natural n) = 146 SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n)) 147 gcd_matches_from_divisors_inj |- !n. INJ (gcd_matches n) (divisors n) univ(:num -> bool) 148 gcd_matches_and_coprimes_by_same_size |- !n. CARD o gcd_matches n = CARD o coprimes_by n 149 coprimes_by_with_card |- !n. 0 < n ==> (CARD o coprimes_by n = 150 (\d. phi (if d IN divisors n then n DIV d else 0))) 151 coprimes_by_divisors_card |- !n. 0 < n ==> !x. x IN divisors n ==> 152 ((CARD o coprimes_by n) x = (\d. phi (n DIV d)) x) 153 Gauss_little_thm |- !n. n = SIGMA phi (divisors n) 154 155 Recursive definition of phi: 156 rec_phi_def |- !n. rec_phi n = if n = 0 then 0 157 else if n = 1 then 1 158 else n - SIGMA (\a. rec_phi a) {m | m < n /\ m divides n} 159 rec_phi_0 |- rec_phi 0 = 0 160 rec_phi_1 |- rec_phi 1 = 1 161 rec_phi_eq_phi |- !n. rec_phi n = phi n 162 163 Not Used: 164 coprimes_from_notone_inj |- INJ coprimes (univ(:num) DIFF {1}) univ(:num -> bool) 165 divisors_eq_image_gcd_upto |- !n. divisors n = IMAGE (gcd n) (upto n) 166 gcd_eq_equiv_on_upto |- !n. feq (gcd n) equiv_on upto n 167 gcd_eq_upto_partition_by_divisors |- !n. partition (feq (gcd n)) (upto n) = 168 IMAGE (preimage (gcd n) (upto n)) (divisors n) 169 sum_over_upto_by_gcd_partition |- !f n. SIGMA f (upto n) = 170 SIGMA (SIGMA f) (partition (feq (gcd n)) (upto n)) 171 sum_over_upto_by_divisors |- !f n. SIGMA f (upto n) = 172 SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n)) 173 174 divisors_eq_image_gcd_count |- !n. 0 < n ==> (divisors n = IMAGE (gcd n) (count n)) 175 gcd_eq_equiv_on_count |- !n. feq (gcd n) equiv_on count n 176 gcd_eq_count_partition_by_divisors |- !n. 0 < n ==> (partition (feq (gcd n)) (count n) = 177 IMAGE (preimage (gcd n) (count n)) (divisors n)) 178 sum_over_count_by_gcd_partition |- !f n. SIGMA f (count n) = 179 SIGMA (SIGMA f) (partition (feq (gcd n)) (count n)) 180 sum_over_count_by_divisors |- !f n. 0 < n ==> (SIGMA f (count n) = 181 SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n))) 182 183 divisors_eq_image_gcd_natural |- !n. 0 < n ==> (divisors n = IMAGE (gcd n) (natural n)) 184 gcd_eq_natural_partition_by_divisors |- !n. 0 < n ==> (partition (feq (gcd n)) (natural n) = 185 IMAGE (preimage (gcd n) (natural n)) (divisors n)) 186 sum_over_natural_by_preimage_divisors |- !f n. 0 < n ==> (SIGMA f (natural n) = 187 SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n))) 188 sum_image_divisors_cong |- !f g. (f 1 = g 1) /\ 189 (!n. SIGMA f (divisors n) = SIGMA g (divisors n)) ==> (f = g) 190*) 191 192(* Theory: 193 194Given the set natural 6 = {1, 2, 3, 4, 5, 6} 195Every element has a gcd with 6: IMAGE (gcd 6) (natural 6) = {1, 2, 3, 2, 1, 6} = {1, 2, 3, 6}. 196Thus the original set is partitioned by gcd: {{1, 5}, {2, 4}, {3}, {6}} 197Since (gcd 6) j is a divisor of 6, and they run through all possible divisors of 6, 198 SIGMA f (natural 6) 199= f 1 + f 2 + f 3 + f 4 + f 5 + f 6 200= (f 1 + f 5) + (f 2 + f 4) + f 3 + f 6 201= (SIGMA f {1, 5}) + (SIGMA f {2, 4}) + (SIGMA f {3}) + (SIGMA f {6}) 202= SIGMA (SIGMA f) {{1, 5}, {2, 4}, {3}, {6}} 203= SIGMA (SIGMA f) (partition (feq (natural 6) (gcd 6)) (natural 6)) 204 205SIGMA:('a -> num) -> ('a -> bool) -> num 206SIGMA (f:num -> num):(num -> bool) -> num 207SIGMA (SIGMA (f:num -> num)) (s:(num -> bool) -> bool):num 208 209How to relate this to (divisors n) ? 210First, observe IMAGE (gcd 6) (natural 6) = divisors 6 211and partition {{1, 5}, {2, 4}, {3}, {6}} = IMAGE (preimage (gcd 6) (natural 6)) (divisors 6) 212 213 SIGMA f (natural 6) 214= SIGMA (SIGMA f) (partition (feq (natural 6) (gcd 6)) (natural 6)) 215= SIGMA (SIGMA f) (IMAGE (preimage (gcd 6) (natural 6)) (divisors 6)) 216 217divisors n:num -> bool 218preimage (gcd n):(num -> bool) -> num -> num -> bool 219preimage (gcd n) (natural n):num -> num -> bool 220IMAGE (preimage (gcd n) (natural n)) (divisors n):(num -> bool) -> bool 221 222How to relate this to (coprimes d), where d divides n ? 223Note {1, 5} with (gcd 6) j = 1, equals to (coprimes (6 DIV 1)) = coprimes 6 224 {2, 4} with (gcd 6) j = 2, BIJ to {2/2, 4/2} with gcd (6/2) (j/2) = 1, i.e {1, 2} = coprimes 3 225 {3} with (gcd 6) j = 3, BIJ to {3/3} with gcd (6/3) (j/3) = 1, i.e. {1} = coprimes 2 226 {6} with (gcd 6) j = 6, BIJ to {6/6} with gcd (6/6) (j/6) = 1, i.e. {1} = coprimes 1 227Hence CARD {{1, 5}, {2, 4}, {3}, {6}} = CARD (partition) 228 = CARD {{1, 5}/1, {2,4}/2, {3}/3, {6}/6} = CARD (reduced-partition) 229 = CARD {(coprimes 6/1) (coprimes 6/2) (coprimes 6/3) (coprimes 6/6)} 230 = CARD {(coprimes 6) (coprimes 3) (coprimes 2) (coprimes 1)} 231 = SIGMA (CARD (coprimes d)), over d divides 6) 232 = SIGMA (phi d), over d divides 6. 233*) 234 235 236(* ------------------------------------------------------------------------- *) 237(* Helper Theorems *) 238(* ------------------------------------------------------------------------- *) 239 240(* ------------------------------------------------------------------------- *) 241(* Coprimes *) 242(* ------------------------------------------------------------------------- *) 243 244(* Define the coprimes set: integers from 1 to n that are coprime to n *) 245(* 246val coprimes_def = zDefine ` 247 coprimes n = {j | 0 < j /\ j <= n /\ coprime j n} 248`; 249*) 250(* Note: j <= n ensures that coprimes n is finite. *) 251(* Note: 0 < j is only to ensure coprimes 1 = {1} *) 252val coprimes_def = zDefine ` 253 coprimes n = {j | j IN (natural n) /\ coprime j n} 254`; 255(* use zDefine as this is not computationally effective. *) 256 257(* Theorem: j IN coprimes n <=> 0 < j /\ j <= n /\ coprime j n *) 258(* Proof: by coprimes_def, natural_element *) 259val coprimes_element = store_thm( 260 "coprimes_element", 261 ``!n j. j IN coprimes n <=> 0 < j /\ j <= n /\ coprime j n``, 262 (rw[coprimes_def, natural_element] >> metis_tac[])); 263 264(* Theorem: coprimes n = (natural n) INTER {j | coprime j n} *) 265(* Proof: by coprimes_def, EXTENSION, IN_INTER *) 266val coprimes_alt = store_thm( 267 "coprimes_alt[compute]", 268 ``!n. coprimes n = (natural n) INTER {j | coprime j n}``, 269 rw[coprimes_def, EXTENSION]); 270(* This is effective, put in computeLib. *) 271 272(* 273> EVAL ``coprimes 10``; 274val it = |- coprimes 10 = {9; 7; 3; 1}: thm 275*) 276 277(* Theorem: coprimes n = set (FILTER (\j. coprime j n) (GENLIST SUC n)) *) 278(* Proof: 279 coprimes n 280 = (natural n) INTER {j | coprime j n} by coprimes_alt 281 = (set (GENLIST SUC n)) INTER {j | coprime j n} by natural_thm 282 = {j | coprime j n} INTER (set (GENLIST SUC n)) by INTER_COMM 283 = set (FILTER (\j. coprime j n) (GENLIST SUC n)) by LIST_TO_SET_FILTER 284*) 285val coprimes_thm = store_thm( 286 "coprimes_thm", 287 ``!n. coprimes n = set (FILTER (\j. coprime j n) (GENLIST SUC n))``, 288 rw[coprimes_alt, natural_thm, INTER_COMM, LIST_TO_SET_FILTER]); 289 290(* Theorem: coprimes n SUBSET natural n *) 291(* Proof: by coprimes_def, SUBSET_DEF *) 292val coprimes_subset = store_thm( 293 "coprimes_subset", 294 ``!n. coprimes n SUBSET natural n``, 295 rw[coprimes_def, SUBSET_DEF]); 296 297(* Theorem: FINITE (coprimes n) *) 298(* Proof: 299 Since (coprimes n) SUBSET (natural n) by coprimes_subset 300 and !n. FINITE (natural n) by natural_finite 301 so FINITE (coprimes n) by SUBSET_FINITE 302*) 303val coprimes_finite = store_thm( 304 "coprimes_finite", 305 ``!n. FINITE (coprimes n)``, 306 metis_tac[coprimes_subset, natural_finite, SUBSET_FINITE]); 307 308(* Theorem: coprimes 0 = {} *) 309(* Proof: 310 By coprimes_element, 0 < j /\ j <= 0, 311 which is impossible, hence empty. 312*) 313val coprimes_0 = store_thm( 314 "coprimes_0", 315 ``coprimes 0 = {}``, 316 rw[coprimes_element, EXTENSION]); 317 318(* Theorem: coprimes 1 = {1} *) 319(* Proof: 320 By coprimes_element, 0 < j /\ j <= 1, 321 Only possible j is 1, and gcd 1 1 = 1. 322 *) 323val coprimes_1 = store_thm( 324 "coprimes_1", 325 ``coprimes 1 = {1}``, 326 rw[coprimes_element, EXTENSION]); 327 328(* Theorem: 0 < n ==> 1 IN (coprimes n) *) 329(* Proof: by coprimes_element, GCD_1 *) 330val coprimes_has_1 = store_thm( 331 "coprimes_has_1", 332 ``!n. 0 < n ==> 1 IN (coprimes n)``, 333 rw[coprimes_element]); 334 335(* Theorem: (coprimes n = {}) <=> (n = 0) *) 336(* Proof: 337 If part: coprimes n = {} ==> n = 0 338 By contradiction. 339 Suppose n <> 0, then 0 < n. 340 Then 1 IN (coprimes n) by coprimes_has_1 341 hence (coprimes n) <> {} by MEMBER_NOT_EMPTY 342 This contradicts (coprimes n) = {}. 343 Only-if part: n = 0 ==> coprimes n = {} 344 True by coprimes_0 345*) 346val coprimes_eq_empty = store_thm( 347 "coprimes_eq_empty", 348 ``!n. (coprimes n = {}) <=> (n = 0)``, 349 rw[EQ_IMP_THM] >- 350 metis_tac[coprimes_has_1, MEMBER_NOT_EMPTY, NOT_ZERO_LT_ZERO] >> 351 rw[coprimes_0]); 352 353(* Theorem: 0 NOTIN (coprimes n) *) 354(* Proof: 355 By coprimes_element, 0 < j /\ j <= n, 356 Hence j <> 0, or 0 NOTIN (coprimes n) 357*) 358val coprimes_no_0 = store_thm( 359 "coprimes_no_0", 360 ``!n. 0 NOTIN (coprimes n)``, 361 rw[coprimes_element]); 362 363(* Theorem: 1 < n ==> n NOTIN coprimes n *) 364(* Proof: 365 By coprimes_element, 0 < j /\ j <= n /\ gcd j n = 1 366 If j = n, 1 = gcd j n = gcd n n = n by GCD_REF 367 which is excluded by 1 < n, so j <> n. 368*) 369val coprimes_without_last = store_thm( 370 "coprimes_without_last", 371 ``!n. 1 < n ==> n NOTIN coprimes n``, 372 rw[coprimes_element]); 373 374(* Theorem: n IN coprimes n <=> (n = 1) *) 375(* Proof: 376 By coprimes_element, 0 < j /\ j <= n /\ gcd j n = 1 377 If n IN coprimes n, 1 = gcd j n = gcd n n = n by GCD_REF 378 If n = 1, 0 < n, n <= n, and gcd n n = n = 1 by GCD_REF 379*) 380val coprimes_with_last = store_thm( 381 "coprimes_with_last", 382 ``!n. n IN coprimes n <=> (n = 1)``, 383 rw[coprimes_element]); 384 385(* Theorem: 1 < n ==> (n - 1) IN (coprimes n) *) 386(* Proof: by coprimes_element, coprime_PRE, GCD_SYM *) 387val coprimes_has_last_but_1 = store_thm( 388 "coprimes_has_last_but_1", 389 ``!n. 1 < n ==> (n - 1) IN (coprimes n)``, 390 rpt strip_tac >> 391 `0 < n /\ 0 < n - 1` by decide_tac >> 392 rw[coprimes_element, coprime_PRE, GCD_SYM]); 393 394(* Theorem: 1 < n ==> !j. j IN coprimes n ==> j < n *) 395(* Proof: 396 Since j IN coprimes n ==> j <= n by coprimes_element 397 If j = n, then gcd n n = n <> 1 by GCD_REF 398 Thus j <> n, or j < n. or by coprimes_without_last 399*) 400val coprimes_element_less = store_thm( 401 "coprimes_element_less", 402 ``!n. 1 < n ==> !j. j IN coprimes n ==> j < n``, 403 metis_tac[coprimes_element, coprimes_without_last, LESS_OR_EQ]); 404 405(* Theorem: 1 < n ==> !j. j IN coprimes n <=> j < n /\ coprime j n *) 406(* Proof: 407 If part: j IN coprimes n ==> j < n /\ coprime j n 408 Note 0 < j /\ j <= n /\ coprime j n by coprimes_element 409 By contradiction, suppose n <= j. 410 Then j = n, but gcd n n = n <> 1 by GCD_REF 411 Only-if part: j < n /\ coprime j n ==> j IN coprimes n 412 This is to show: 413 0 < j /\ j <= n /\ coprime j n by coprimes_element 414 By contradiction, suppose ~(0 < j). 415 Then j = 0, but gcd 0 n = n <> 1 by GCD_0L 416*) 417val coprimes_element_alt = store_thm( 418 "coprimes_element_alt", 419 ``!n. 1 < n ==> !j. j IN coprimes n <=> j < n /\ coprime j n``, 420 rw[coprimes_element] >> 421 `n <> 1` by decide_tac >> 422 rw[EQ_IMP_THM] >| [ 423 spose_not_then strip_assume_tac >> 424 `j = n` by decide_tac >> 425 metis_tac[GCD_REF], 426 spose_not_then strip_assume_tac >> 427 `j = 0` by decide_tac >> 428 metis_tac[GCD_0L] 429 ]); 430 431(* Theorem: 1 < n ==> (MAX_SET (coprimes n) = n - 1) *) 432(* Proof: 433 Let s = coprimes n, m = MAX_SET s. 434 Note (n - 1) IN s by coprimes_has_last_but_1, 1 < n 435 Hence s <> {} by MEMBER_NOT_EMPTY 436 and FINITE s by coprimes_finite 437 Since !x. x IN s ==> x < n by coprimes_element_less, 1 < n 438 also !x. x < n ==> x <= (n - 1) by SUB_LESS_OR 439 Therefore MAX_SET s = n - 1 by MAX_SET_TEST 440*) 441val coprimes_max = store_thm( 442 "coprimes_max", 443 ``!n. 1 < n ==> (MAX_SET (coprimes n) = n - 1)``, 444 rpt strip_tac >> 445 qabbrev_tac `s = coprimes n` >> 446 `(n - 1) IN s` by rw[coprimes_has_last_but_1, Abbr`s`] >> 447 `s <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> 448 `FINITE s` by rw[coprimes_finite, Abbr`s`] >> 449 `!x. x IN s ==> x < n` by rw[coprimes_element_less, Abbr`s`] >> 450 `!x. x < n ==> x <= (n - 1)` by decide_tac >> 451 metis_tac[MAX_SET_TEST]); 452 453(* Relate coprimes to Euler totient *) 454 455(* Theorem: 1 < n ==> (coprimes n = Euler n) *) 456(* Proof: 457 By Euler_def, this is to show: 458 (1) x IN coprimes n ==> 0 < x, true by coprimes_element 459 (2) x IN coprimes n ==> x < n, true by coprimes_element_less 460 (3) x IN coprimes n ==> coprime n x, true by coprimes_element, GCD_SYM 461 (4) 0 < x /\ x < n /\ coprime n x ==> x IN coprimes n 462 That is, to show: 0 < x /\ x <= n /\ coprime x n. 463 Since x < n ==> x <= n by LESS_IMP_LESS_OR_EQ 464 Hence true by GCD_SYM 465*) 466val coprimes_eq_Euler = store_thm( 467 "coprimes_eq_Euler", 468 ``!n. 1 < n ==> (coprimes n = Euler n)``, 469 rw[Euler_def, EXTENSION, EQ_IMP_THM] >- 470 metis_tac[coprimes_element] >- 471 rw[coprimes_element_less] >- 472 metis_tac[coprimes_element, GCD_SYM] >> 473 metis_tac[coprimes_element, GCD_SYM, LESS_IMP_LESS_OR_EQ]); 474 475(* Theorem: prime n ==> (coprimes n = residue n) *) 476(* Proof: 477 Since prime n ==> 1 < n by ONE_LT_PRIME 478 Hence coprimes n 479 = Euler n by coprimes_eq_Euler 480 = residue n by Euler_prime 481*) 482val coprimes_prime = store_thm( 483 "coprimes_prime", 484 ``!n. prime n ==> (coprimes n = residue n)``, 485 rw[ONE_LT_PRIME, coprimes_eq_Euler, Euler_prime]); 486 487(* ------------------------------------------------------------------------- *) 488(* Coprimes by a divisor *) 489(* ------------------------------------------------------------------------- *) 490 491(* Define the set of coprimes by a divisor of n *) 492val coprimes_by_def = Define ` 493 coprimes_by n d = if (0 < n /\ d divides n) then coprimes (n DIV d) else {} 494`; 495 496(* 497EVAL ``coprimes_by 10 2``; = {4; 3; 2; 1} 498EVAL ``coprimes_by 10 5``; = {1} 499*) 500 501(* Theorem: j IN (coprimes_by n d) <=> (0 < n /\ d divides n /\ j IN coprimes (n DIV d)) *) 502(* Proof: by coprimes_by_def, MEMBER_NOT_EMPTY *) 503val coprimes_by_element = store_thm( 504 "coprimes_by_element", 505 ``!n d j. j IN (coprimes_by n d) <=> (0 < n /\ d divides n /\ j IN coprimes (n DIV d))``, 506 metis_tac[coprimes_by_def, MEMBER_NOT_EMPTY]); 507 508(* Theorem: FINITE (coprimes_by n d) *) 509(* Proof: 510 From coprimes_by_def, this follows by: 511 (1) !k. FINITE (coprimes k) by coprimes_finite 512 (2) FINITE {} by FINITE_EMPTY 513*) 514val coprimes_by_finite = store_thm( 515 "coprimes_by_finite", 516 ``!n d. FINITE (coprimes_by n d)``, 517 rw[coprimes_by_def, coprimes_finite]); 518 519(* Theorem: coprimes_by 0 d = {} *) 520(* Proof: by coprimes_by_def *) 521val coprimes_by_0 = store_thm( 522 "coprimes_by_0", 523 ``!d. coprimes_by 0 d = {}``, 524 rw[coprimes_by_def]); 525 526(* Theorem: coprimes_by n 0 = {} *) 527(* Proof: 528 coprimes_by n 0 529 = if 0 < n /\ 0 divides n then coprimes (n DIV 0) else {} 530 = 0 < 0 then coprimes (n DIV 0) else {} by ZERO_DIVIDES 531 = {} by prim_recTheory.LESS_REFL 532*) 533val coprimes_by_by_0 = store_thm( 534 "coprimes_by_by_0", 535 ``!n. coprimes_by n 0 = {}``, 536 rw[coprimes_by_def]); 537 538(* Theorem: 0 < n ==> (coprimes_by n 1 = coprimes n) *) 539(* Proof: 540 Since 1 divides n by ONE_DIVIDES_ALL 541 coprimes_by n 1 542 = coprimes (n DIV 1) by coprimes_by_def 543 = coprimes n by DIV_ONE, ONE 544*) 545val coprimes_by_by_1 = store_thm( 546 "coprimes_by_by_1", 547 ``!n. 0 < n ==> (coprimes_by n 1 = coprimes n)``, 548 rw[coprimes_by_def]); 549 550(* Theorem: 0 < n ==> (coprimes_by n n = {1}) *) 551(* Proof: 552 Since n divides n by DIVIDES_REFL 553 coprimes_by n n 554 = coprimes (n DIV n) by coprimes_by_def 555 = coprimes 1 by DIVMOD_ID, 0 < n 556 = {1} by coprimes_1 557*) 558val coprimes_by_by_last = store_thm( 559 "coprimes_by_by_last", 560 ``!n. 0 < n ==> (coprimes_by n n = {1})``, 561 rw[coprimes_by_def, coprimes_1]); 562 563(* Theorem: 0 < n /\ d divides n ==> (coprimes_by n d = coprimes (n DIV d)) *) 564(* Proof: by coprimes_by_def *) 565val coprimes_by_by_divisor = store_thm( 566 "coprimes_by_by_divisor", 567 ``!n d. 0 < n /\ d divides n ==> (coprimes_by n d = coprimes (n DIV d))``, 568 rw[coprimes_by_def]); 569 570(* Theorem: 0 < n ==> ((coprimes_by n d = {}) <=> ~(d divides n)) *) 571(* Proof: 572 If part: 0 < n /\ coprimes_by n d = {} ==> ~(d divides n) 573 By contradiction. Suppose d divides n. 574 Then d divides n and 0 < n means 575 0 < d /\ d <= n by divides_pos, 0 < n 576 Also coprimes_by n d = coprimes (n DIV d) by coprimes_by_def 577 so coprimes (n DIV d) = {} <=> n DIV d = 0 by coprimes_eq_empty 578 Thus n < d by DIV_EQ_0 579 which contradicts d <= n. 580 Only-if part: 0 < n /\ ~(d divides n) ==> coprimes n d = {} 581 This follows by coprimes_by_def 582*) 583val coprimes_by_eq_empty = store_thm( 584 "coprimes_by_eq_empty", 585 ``!n d. 0 < n ==> ((coprimes_by n d = {}) <=> ~(d divides n))``, 586 rw[EQ_IMP_THM] >| [ 587 spose_not_then strip_assume_tac >> 588 `0 < d /\ d <= n` by metis_tac[divides_pos] >> 589 `n DIV d = 0` by metis_tac[coprimes_by_def, coprimes_eq_empty] >> 590 `n < d` by rw[GSYM DIV_EQ_0] >> 591 decide_tac, 592 rw[coprimes_by_def] 593 ]); 594 595(* ------------------------------------------------------------------------- *) 596(* GCD Equivalence Class *) 597(* ------------------------------------------------------------------------- *) 598 599(* Define the set of values with the same gcd *) 600val gcd_matches_def = zDefine ` 601 gcd_matches n d = {j| j IN (natural n) /\ (gcd j n = d)} 602`; 603(* use zDefine as this is not computationally effective. *) 604 605(* Theorem: gcd_matches n d = (natural n) INTER {j | gcd j n = d} *) 606(* Proof: by gcd_matches_def *) 607Theorem gcd_matches_alt[compute]: 608 !n d. gcd_matches n d = (natural n) INTER {j | gcd j n = d} 609Proof 610 simp[gcd_matches_def, EXTENSION] 611QED 612 613(* 614EVAL ``gcd_matches 10 2``; = {8; 6; 4; 2} 615EVAL ``gcd_matches 10 5``; = {5} 616*) 617 618(* Theorem: j IN gcd_matches n d <=> 0 < j /\ j <= n /\ (gcd j n = d) *) 619(* Proof: by gcd_matches_def *) 620val gcd_matches_element = store_thm( 621 "gcd_matches_element", 622 ``!n d j. j IN gcd_matches n d <=> 0 < j /\ j <= n /\ (gcd j n = d)``, 623 rw[gcd_matches_def, natural_element]); 624 625(* Theorem: (gcd_matches n d) SUBSET (natural n) *) 626(* Proof: by gcd_matches_def, SUBSET_DEF *) 627val gcd_matches_subset = store_thm( 628 "gcd_matches_subset", 629 ``!n d. (gcd_matches n d) SUBSET (natural n)``, 630 rw[gcd_matches_def, SUBSET_DEF]); 631 632(* Theorem: FINITE (gcd_matches n d) *) 633(* Proof: 634 Since (gcd_matches n d) SUBSET (natural n) by coprimes_subset 635 and !n. FINITE (natural n) by natural_finite 636 so FINITE (gcd_matches n d) by SUBSET_FINITE 637*) 638val gcd_matches_finite = store_thm( 639 "gcd_matches_finite", 640 ``!n d. FINITE (gcd_matches n d)``, 641 metis_tac[gcd_matches_subset, natural_finite, SUBSET_FINITE]); 642 643(* Theorem: gcd_matches 0 d = {} *) 644(* Proof: 645 j IN gcd_matches 0 d 646 <=> 0 < j /\ j <= 0 /\ (gcd j 0 = d) by gcd_matches_element 647 Since no j can satisfy this, the set is empty. 648*) 649val gcd_matches_0 = store_thm( 650 "gcd_matches_0", 651 ``!d. gcd_matches 0 d = {}``, 652 rw[gcd_matches_element, EXTENSION]); 653 654(* Theorem: gcd_matches n 0 = {} *) 655(* Proof: 656 x IN gcd_matches n 0 657 <=> 0 < x /\ x <= n /\ (gcd x n = 0) by gcd_matches_element 658 <=> 0 < x /\ x <= n /\ (x = 0) /\ (n = 0) by GCD_EQ_0 659 <=> F by 0 < x, x = 0 660 Hence gcd_matches n 0 = {} by EXTENSION 661*) 662val gcd_matches_with_0 = store_thm( 663 "gcd_matches_with_0", 664 ``!n. gcd_matches n 0 = {}``, 665 rw[EXTENSION, gcd_matches_element]); 666 667(* Theorem: gcd_matches 1 d = if d = 1 then {1} else {} *) 668(* Proof: 669 j IN gcd_matches 1 d 670 <=> 0 < j /\ j <= 1 /\ (gcd j 1 = d) by gcd_matches_element 671 Only j to satisfy this is j = 1. 672 and d = gcd 1 1 = 1 by GCD_REF 673 If d = 1, j = 1 is the only element. 674 If d <> 1, the only element is taken out, set is empty. 675*) 676val gcd_matches_1 = store_thm( 677 "gcd_matches_1", 678 ``!d. gcd_matches 1 d = if d = 1 then {1} else {}``, 679 rw[gcd_matches_element, EXTENSION]); 680 681(* Theorem: 0 < n /\ d divides n ==> d IN (gcd_matches n d) *) 682(* Proof: 683 Note 0 < n /\ d divides n 684 ==> 0 < d, and d <= n by divides_pos 685 and gcd d n = d by divides_iff_gcd_fix 686 Hence d IN (gcd_matches n d) by gcd_matches_element 687*) 688val gcd_matches_has_divisor = store_thm( 689 "gcd_matches_has_divisor", 690 ``!n d. 0 < n /\ d divides n ==> d IN (gcd_matches n d)``, 691 rw[gcd_matches_element] >- 692 metis_tac[divisor_pos] >- 693 rw[DIVIDES_LE] >> 694 rw[GSYM divides_iff_gcd_fix]); 695 696(* Theorem: j IN (gcd_matches n d) ==> d divides j /\ d divides n *) 697(* Proof: 698 If j IN (gcd_matches n d), gcd j n = d by gcd_matches_element 699 This means d divides j /\ d divides n by GCD_IS_GREATEST_COMMON_DIVISOR 700*) 701val gcd_matches_element_divides = store_thm( 702 "gcd_matches_element_divides", 703 ``!n d j. j IN (gcd_matches n d) ==> d divides j /\ d divides n``, 704 metis_tac[gcd_matches_element, GCD_IS_GREATEST_COMMON_DIVISOR]); 705 706(* Theorem: 0 < n ==> ((gcd_matches n d = {}) <=> ~(d divides n)) *) 707(* Proof: 708 If part: 0 < n /\ (gcd_matches n d = {}) ==> ~(d divides n) 709 By contradiction, suppose d divides n. 710 Then d IN gcd_matches n d by gcd_matches_has_divisor 711 This contradicts gcd_matches n d = {} by MEMBER_NOT_EMPTY 712 Only-if part: 0 < n /\ ~(d divides n) ==> (gcd_matches n d = {}) 713 By contradiction, suppose gcd_matches n d <> {}. 714 Then ?j. j IN (gcd_matches n d) by MEMBER_NOT_EMPTY 715 Giving d divides j /\ d divides n by gcd_matches_element_divides 716 This contradicts ~(d divides n). 717*) 718val gcd_matches_eq_empty = store_thm( 719 "gcd_matches_eq_empty", 720 ``!n d. 0 < n ==> ((gcd_matches n d = {}) <=> ~(d divides n))``, 721 rw[EQ_IMP_THM] >- 722 metis_tac[gcd_matches_has_divisor, MEMBER_NOT_EMPTY] >> 723 metis_tac[gcd_matches_element_divides, MEMBER_NOT_EMPTY]); 724 725(* ------------------------------------------------------------------------- *) 726(* Phi Function *) 727(* ------------------------------------------------------------------------- *) 728 729(* Define the Euler phi function from coprime set *) 730val phi_def = Define ` 731 phi n = CARD (coprimes n) 732`; 733(* Since (coprimes n) is computable, phi n is now computable *) 734 735(* 736> EVAL ``phi 10``; 737val it = |- phi 10 = 4: thm 738*) 739 740(* Theorem: phi n = LENGTH (FILTER (\j. coprime j n) (GENLIST SUC n)) *) 741(* Proof: 742 Let ls = FILTER (\j. coprime j n) (GENLIST SUC n). 743 Note ALL_DISTINCT (GENLIST SUC n) by ALL_DISTINCT_GENLIST, SUC_EQ 744 Thus ALL_DISTINCT ls by FILTER_ALL_DISTINCT 745 phi n = CARD (coprimes n) by phi_def 746 = CARD (set ls) by coprimes_thm 747 = LENGTH ls by ALL_DISTINCT_CARD_LIST_TO_SET 748*) 749val phi_thm = store_thm( 750 "phi_thm", 751 ``!n. phi n = LENGTH (FILTER (\j. coprime j n) (GENLIST SUC n))``, 752 rpt strip_tac >> 753 qabbrev_tac `ls = FILTER (\j. coprime j n) (GENLIST SUC n)` >> 754 `ALL_DISTINCT ls` by rw[ALL_DISTINCT_GENLIST, FILTER_ALL_DISTINCT, Abbr`ls`] >> 755 `phi n = CARD (coprimes n)` by rw[phi_def] >> 756 `_ = CARD (set ls)` by rw[coprimes_thm, Abbr`ls`] >> 757 `_ = LENGTH ls` by rw[ALL_DISTINCT_CARD_LIST_TO_SET] >> 758 decide_tac); 759 760(* Theorem: phi = CARD o coprimes *) 761(* Proof: by phi_def, FUN_EQ_THM *) 762val phi_fun = store_thm( 763 "phi_fun", 764 ``phi = CARD o coprimes``, 765 rw[phi_def, FUN_EQ_THM]); 766 767(* Theorem: 0 < n ==> 0 < phi n *) 768(* Proof: 769 Since 1 IN coprimes n by coprimes_has_1 770 so coprimes n <> {} by MEMBER_NOT_EMPTY 771 and FINITE (coprimes n) by coprimes_finite 772 hence phi n <> 0 by CARD_EQ_0 773 or 0 < phi n 774*) 775val phi_pos = store_thm( 776 "phi_pos", 777 ``!n. 0 < n ==> 0 < phi n``, 778 rpt strip_tac >> 779 `coprimes n <> {}` by metis_tac[coprimes_has_1, MEMBER_NOT_EMPTY] >> 780 `FINITE (coprimes n)` by rw[coprimes_finite] >> 781 `phi n <> 0` by rw[phi_def, CARD_EQ_0] >> 782 decide_tac); 783 784(* Theorem: phi 0 = 0 *) 785(* Proof: 786 phi 0 787 = CARD (coprimes 0) by phi_def 788 = CARD {} by coprimes_0 789 = 0 by CARD_EMPTY 790*) 791val phi_0 = store_thm( 792 "phi_0", 793 ``phi 0 = 0``, 794 rw[phi_def, coprimes_0]); 795 796(* Theorem: (phi n = 0) <=> (n = 0) *) 797(* Proof: 798 If part: (phi n = 0) ==> (n = 0) by phi_pos, NOT_ZERO_LT_ZERO 799 Only-if part: phi 0 = 0 by phi_0 800*) 801val phi_eq_0 = store_thm( 802 "phi_eq_0", 803 ``!n. (phi n = 0) <=> (n = 0)``, 804 metis_tac[phi_0, phi_pos, NOT_ZERO_LT_ZERO]); 805 806(* Theorem: phi 1 = 1 *) 807(* Proof: 808 phi 1 809 = CARD (coprimes 1) by phi_def 810 = CARD {1} by coprimes_1 811 = 1 by CARD_SING 812*) 813val phi_1 = store_thm( 814 "phi_1", 815 ``phi 1 = 1``, 816 rw[phi_def, coprimes_1]); 817 818(* Theorem: 1 < n ==> (phi n = totient n) *) 819(* Proof: 820 phi n 821 = CARD (coprimes n) by phi_def 822 = CARD (Euler n ) by coprimes_eq_Euler 823 = totient n by totient_def 824*) 825val phi_eq_totient = store_thm( 826 "phi_eq_totient", 827 ``!n. 1 < n ==> (phi n = totient n)``, 828 rw[phi_def, totient_def, coprimes_eq_Euler]); 829 830(* Theorem: prime n ==> (phi n = n - 1) *) 831(* Proof: 832 Since prime n ==> 1 < n by ONE_LT_PRIME 833 Hence phi n 834 = totient n by phi_eq_totient 835 = n - 1 by Euler_card_prime 836*) 837val phi_prime = store_thm( 838 "phi_prime", 839 ``!n. prime n ==> (phi n = n - 1)``, 840 rw[ONE_LT_PRIME, phi_eq_totient, Euler_card_prime]); 841 842(* Theorem: phi 2 = 1 *) 843(* Proof: 844 Since prime 2 by PRIME_2 845 so phi 2 = 2 - 1 = 1 by phi_prime 846*) 847val phi_2 = store_thm( 848 "phi_2", 849 ``phi 2 = 1``, 850 rw[phi_prime, PRIME_2]); 851 852(* Theorem: 2 < n ==> 1 < phi n *) 853(* Proof: 854 Note 1 IN (coprimes n) by coprimes_has_1, 0 < n 855 and (n - 1) IN (coprimes n) by coprimes_has_last_but_1, 1 < n 856 and n - 1 <> 1 by 2 < n 857 Now FINITE (coprimes n) by coprimes_finite] 858 and {1; (n-1)} SUBSET (coprimes n) by SUBSET_DEF, above 859 Note CARD {1; (n-1)} = 2 by CARD_INSERT, CARD_EMPTY, TWO 860 thus 2 <= CARD (coprimes n) by CARD_SUBSET 861 or 1 < phi n by phi_def 862*) 863val phi_gt_1 = store_thm( 864 "phi_gt_1", 865 ``!n. 2 < n ==> 1 < phi n``, 866 rw[phi_def] >> 867 `0 < n /\ 1 < n /\ n - 1 <> 1` by decide_tac >> 868 `1 IN (coprimes n)` by rw[coprimes_has_1] >> 869 `(n - 1) IN (coprimes n)` by rw[coprimes_has_last_but_1] >> 870 `FINITE (coprimes n)` by rw[coprimes_finite] >> 871 `{1; (n-1)} SUBSET (coprimes n)` by rw[SUBSET_DEF] >> 872 `CARD {1; (n-1)} = 2` by rw[] >> 873 `2 <= CARD (coprimes n)` by metis_tac[CARD_SUBSET] >> 874 decide_tac); 875 876(* Theorem: phi n <= n *) 877(* Proof: 878 Note phi n = CARD (coprimes n) by phi_def 879 and coprimes n SUBSET natural n by coprimes_subset 880 Now FINITE (natural n) by natural_finite 881 and CARD (natural n) = n by natural_card 882 so CARD (coprimes n) <= n by CARD_SUBSET 883*) 884val phi_le = store_thm( 885 "phi_le", 886 ``!n. phi n <= n``, 887 metis_tac[phi_def, coprimes_subset, natural_finite, natural_card, CARD_SUBSET]); 888 889(* Theorem: 1 < n ==> phi n < n *) 890(* Proof: 891 Note phi n = CARD (coprimes n) by phi_def 892 and 1 < n ==> !j. j IN coprimes n ==> j < n by coprimes_element_less 893 but 0 NOTIN coprimes n by coprimes_no_0 894 or coprimes n SUBSET (count n) DIFF {0} by SUBSET_DEF, IN_DIFF 895 Let s = (count n) DIFF {0}. 896 Note {0} SUBSET count n by SUBSET_DEF]); 897 so count n INTER {0} = {0} by SUBSET_INTER_ABSORPTION 898 Now FINITE s by FINITE_COUNT, FINITE_DIFF 899 and CARD s = n - 1 by CARD_COUNT, CARD_DIFF, CARD_SING 900 so CARD (coprimes n) <= n - 1 by CARD_SUBSET 901 or phi n < n by arithmetic 902*) 903val phi_lt = store_thm( 904 "phi_lt", 905 ``!n. 1 < n ==> phi n < n``, 906 rw[phi_def] >> 907 `!j. j IN coprimes n ==> j < n` by rw[coprimes_element_less] >> 908 `!j. j IN coprimes n ==> j <> 0` by metis_tac[coprimes_no_0] >> 909 qabbrev_tac `s = (count n) DIFF {0}` >> 910 `coprimes n SUBSET s` by rw[SUBSET_DEF, Abbr`s`] >> 911 `{0} SUBSET count n` by rw[SUBSET_DEF] >> 912 `count n INTER {0} = {0}` by metis_tac[SUBSET_INTER_ABSORPTION, INTER_COMM] >> 913 `FINITE s` by rw[Abbr`s`] >> 914 `CARD s = n - 1` by rw[Abbr`s`] >> 915 `CARD (coprimes n) <= n - 1` by metis_tac[CARD_SUBSET] >> 916 decide_tac); 917 918(* ------------------------------------------------------------------------- *) 919(* Divisors *) 920(* ------------------------------------------------------------------------- *) 921 922(* Define the set of divisors of a number. *) 923val divisors_def = zDefine ` 924 divisors n = {d | d <= n /\ d divides n} 925`; 926(* use zDefine as this is not computationally effective. *) 927(* Note: use of d <= n to give bounded divisors, so that divisors_0 = {0} only. *) 928(* Note: for 0 < n, d <= n is redundant, as DIVIDES_LE implies it. *) 929 930(* Theorem: d IN divisors n <=> d <= n /\ d divides n *) 931(* Proof: by divisors_def *) 932val divisors_element = store_thm( 933 "divisors_element", 934 ``!n d. d IN divisors n <=> d <= n /\ d divides n``, 935 rw[divisors_def]); 936 937(* Theorem: 0 < n ==> !d. d IN divisors n <=> d divides n *) 938(* Proof: 939 If part: d IN divisors n ==> d divides n 940 True by divisors_element 941 Only-if part: 0 < n /\ d divides n ==> d IN divisors n 942 Since 0 < n /\ d divides n 943 ==> 0 < d /\ d <= n by divides_pos 944 Hence d IN divisors n by divisors_element 945*) 946val divisors_element_alt = store_thm( 947 "divisors_element_alt", 948 ``!n. 0 < n ==> !d. d IN divisors n <=> d divides n``, 949 metis_tac[divisors_element, divides_pos]); 950 951(* Theorem: 0 < n ==> 1 IN (divisors n) *) 952(* Proof: 953 Note 0 < n ==> 1 <= n by arithmetic 954 and 1 divides n by ONE_DIVIDES_ALL 955 Hence 1 IN (divisors n) by divisors_element 956*) 957val divisors_has_one = store_thm( 958 "divisors_has_one", 959 ``!n. 0 < n ==> 1 IN (divisors n)``, 960 rw[divisors_element]); 961 962(* Theorem: n IN (divisors n) *) 963(* Proof: by divisors_element *) 964val divisors_has_last = store_thm( 965 "divisors_has_last", 966 ``!n. n IN (divisors n)``, 967 rw[divisors_element]); 968 969(* Theorem: divisors n <> {} *) 970(* Proof: by divisors_has_last, MEMBER_NOT_EMPTY *) 971val divisors_not_empty = store_thm( 972 "divisors_not_empty", 973 ``!n. divisors n <> {}``, 974 metis_tac[divisors_has_last, MEMBER_NOT_EMPTY]); 975 976(* Idea: a method to evaluate divisors. *) 977 978(* Theorem: divisors n = 979 if n = 0 then {0} 980 else IMAGE (\j. if (j + 1) divides n then j + 1 else 1) (count n) *) 981(* Proof: 982 If n = 0, 983 divisors 0 984 = {d | d <= 0 /\ d divides 0} by divisors_def 985 = {0} by d <= 0, and ALL_DIVIDES_0 986 If n <> 0, 987 divisors n 988 = {d | d <= n /\ d divides n} by divisors_def 989 = {d | d <> 0 /\ d <= n /\ d divides n} 990 by ZERO_DIVIDES 991 = {k + 1 | (k + 1) <= n /\ (k + 1) divides n} 992 by num_CASES, d <> 0 993 = {k + 1 | k < n /\ (k + 1) divides n} 994 by arithmetic 995 = IMAGE (\j. if (j + 1) divides n then j + 1 else 1) {k | k < n} 996 by IMAGE_DEF 997 = IMAGE (\j. if (j + 1) divides n then j + 1 else 1) (count n) 998 by count_def 999*) 1000Theorem divisors_eqn[compute]: 1001 !n. divisors n = 1002 if n = 0 then {0} 1003 else IMAGE (\j. if (j + 1) divides n then j + 1 else 1) (count n) 1004Proof 1005 (rw[divisors_def, EXTENSION, EQ_IMP_THM] >> rw[]) >> 1006 `x <> 0` by metis_tac[ZERO_DIVIDES] >> 1007 `?k. x = SUC k` by metis_tac[num_CASES] >> 1008 qexists_tac `k` >> 1009 fs[ADD1] 1010QED 1011 1012(* 1013> EVAL ``divisors 3``; = {3; 1}: thm 1014> EVAL ``divisors 4``; = {4; 2; 1}: thm 1015> EVAL ``divisors 5``; = {5; 1}: thm 1016> EVAL ``divisors 6``; = {6; 3; 2; 1}: thm 1017> EVAL ``divisors 7``; = {7; 1}: thm 1018> EVAL ``divisors 8``; = {8; 4; 2; 1}: thm 1019> EVAL ``divisors 9``; = {9; 3; 1}: thm 1020*) 1021 1022(* Idea: when factor divides, its cofactor also divides. *) 1023 1024(* Theorem: 0 < n /\ d IN divisors n ==> (n DIV d) IN divisors n *) 1025(* Proof: 1026 Note d <= n /\ d divides n by divisors_def 1027 so 0 < d by ZERO_DIVIDES 1028 and n DIV d <= n by DIV_LESS_EQ, 0 < d 1029 and n DIV d divides n by DIVIDES_COFACTOR, 0 < d 1030*) 1031Theorem divisors_cofactor: 1032 !n d. 0 < n /\ d IN divisors n ==> (n DIV d) IN divisors n 1033Proof 1034 simp [divisors_def] >> 1035 ntac 3 strip_tac >> 1036 `0 < d` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >> 1037 rw[DIV_LESS_EQ, DIVIDES_COFACTOR] 1038QED 1039 1040(* Theorem: 0 < n ==> ((divisors n) DELETE n = {m | m < n /\ m divides n}) *) 1041(* Proof: 1042 (divisors n) DELETE n 1043 = {m | m <= n /\ m divides n} DELETE n by divisors_def 1044 = {m | m <= n /\ m divides n} DIFF {n} by DELETE_DEF 1045 = {m | m <> n /\ m <= n /\ m divides n} by IN_DIFF 1046 = {m | m < n /\ m divides n} by LESS_OR_EQ 1047*) 1048val divisors_delete_last = store_thm( 1049 "divisors_delete_last", 1050 ``!n. 0 < n ==> ((divisors n) DELETE n = {m | m < n /\ m divides n})``, 1051 rw[divisors_def, EXTENSION, EQ_IMP_THM]); 1052 1053(* Theorem: 0 < n ==> !d. d IN (divisors n) ==> 0 < d *) 1054(* Proof: 1055 Since d IN (divisors n), d divides n by divisors_element 1056 By contradiction, if d = 0, then n = 0 by ZERO_DIVIDES 1057 This contradicts 0 < n. 1058*) 1059val divisors_nonzero = store_thm( 1060 "divisors_nonzero", 1061 ``!n. 0 < n ==> !d. d IN (divisors n) ==> 0 < d``, 1062 metis_tac[divisors_element, ZERO_DIVIDES, NOT_ZERO_LT_ZERO]); 1063 1064(* Theorem: 0 < n ==> !d. d IN divisors n ==> n DIV d IN divisors n *) 1065(* Proof: 1066 By divisors_element, this is to show: 1067 0 < n /\ d <= n /\ d divides n ==> n DIV d <= n /\ n DIV d divides n 1068 Since 0 < n /\ d divides n ==> 0 < d by divisor_pos 1069 so n = (n DIV d) * d by DIVIDES_EQN, 0 < d 1070 = d * (n DIV d) by MULT_COMM 1071 Hence (n DIV d) divides n by divides_def 1072 and (n DIV d) <= n by DIVIDES_LE, 0 < n 1073*) 1074val divisors_has_cofactor = store_thm( 1075 "divisors_has_cofactor", 1076 ``!n. 0 < n ==> !d. d IN divisors n ==> n DIV d IN divisors n``, 1077 rewrite_tac[divisors_element] >> 1078 ntac 4 strip_tac >> 1079 `0 < d` by metis_tac[divisor_pos] >> 1080 `n = (n DIV d) * d` by rw[GSYM DIVIDES_EQN] >> 1081 `_ = d * (n DIV d)` by rw[MULT_COMM] >> 1082 metis_tac[divides_def, DIVIDES_LE]); 1083 1084(* Theorem: divisors n SUBSET upto n *) 1085(* Proof: by divisors_def, SUBSET_DEF *) 1086val divisors_subset_upto = store_thm( 1087 "divisors_subset_upto", 1088 ``!n. divisors n SUBSET upto n``, 1089 rw[divisors_def, SUBSET_DEF]); 1090 1091(* Theorem: 0 < n ==> (divisors n) SUBSET (natural n) *) 1092(* Proof: 1093 By SUBSET_DEF, this is to show: 1094 x IN (divisors n) ==> x IN (natural n) 1095 Since x IN (divisors n) 1096 ==> x <= n /\ x divides n by divisors_element 1097 ==> x <= n /\ 0 < x since n <> 0, so x <> 0 by ZERO_DIVIDES 1098 ==> x IN (natural n) by natural_element 1099*) 1100val divisors_subset_natural = store_thm( 1101 "divisors_subset_natural", 1102 ``!n. 0 < n ==> (divisors n) SUBSET (natural n)``, 1103 rw[divisors_element, natural_element, SUBSET_DEF] >> 1104 metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO]); 1105 1106(* Theorem: FINITE (divisors n) *) 1107(* Proof: 1108 Since (divisors n) SUBSET count (SUC n) by divisors_subset_upto 1109 and FINITE (count (SUC n)) by FINITE_COUNT 1110 so FINITE (divisors n) by SUBSET_FINITE 1111*) 1112val divisors_finite = store_thm( 1113 "divisors_finite", 1114 ``!n. FINITE (divisors n)``, 1115 metis_tac[divisors_subset_upto, SUBSET_FINITE, FINITE_COUNT]); 1116 1117(* Theorem: divisors 0 = {0} *) 1118(* Proof: divisors_def *) 1119val divisors_0 = store_thm( 1120 "divisors_0", 1121 ``divisors 0 = {0}``, 1122 rw[divisors_def]); 1123 1124(* Theorem: divisors 1 = {1} *) 1125(* Proof: divisors_def *) 1126val divisors_1 = store_thm( 1127 "divisors_1", 1128 ``divisors 1 = {1}``, 1129 rw[divisors_def, EXTENSION]); 1130 1131(* Theorem: 0 IN divisors n <=> (n = 0) *) 1132(* Proof: 1133 0 IN divisors n 1134 <=> 0 <= n /\ 0 divides n by divisors_element 1135 <=> n = 0 by ZERO_DIVIDES 1136*) 1137val divisors_has_0 = store_thm( 1138 "divisors_has_0", 1139 ``!n. 0 IN divisors n <=> (n = 0)``, 1140 rw[divisors_element]); 1141 1142(* Theorem: 0 < n ==> BIJ (\d. n DIV d) (divisors n) (divisors n) *) 1143(* Proof: 1144 By BIJ_DEF, INJ_DEF, SURJ_DEF, this is to show: 1145 (1) d IN divisors n ==> n DIV d IN divisors n 1146 True by divisors_has_cofactor. 1147 (2) d IN divisors n /\ d' IN divisors n /\ n DIV d = n DIV d' ==> d = d' 1148 d IN divisors n ==> d divides n /\ 0 < d by divisors_element, divisor_pos 1149 d' IN divisors n ==> d' divides n /\ 0 < d' by divisors_element, divisor_pos 1150 Hence n = (n DIV d) * d and n = (n DIV d') * d' by DIVIDES_EQN 1151 giving (n DIV d) * d = (n DIV d') * d' 1152 Now (n DIV d) <> 0, otherwise contradicts 0 < n by MULT 1153 Hence d = d' by EQ_MULT_LCANCEL 1154 (3) same as (1), true by divisors_has_cofactor. 1155 (4) x IN divisors n ==> ?d. d IN divisors n /\ (n DIV d = x) 1156 x IN divisors n ==> x divides n by divisors_element 1157 Let d = n DIV x. 1158 Then d IN divisors n by divisors_has_cofactor 1159 and n DIV d = n DIV (n DIV x) = x by divide_by_cofactor 1160*) 1161val divisors_divisors_bij = store_thm( 1162 "divisors_divisors_bij", 1163 ``!n. 0 < n ==> BIJ (\d. n DIV d) (divisors n) (divisors n)``, 1164 rw[BIJ_DEF, INJ_DEF, SURJ_DEF] >- 1165 rw[divisors_has_cofactor] >- 1166 (`n = (n DIV d) * d` by metis_tac[DIVIDES_EQN, divisors_element, divisor_pos] >> 1167 `n = (n DIV d') * d'` by metis_tac[DIVIDES_EQN, divisors_element, divisor_pos] >> 1168 `n DIV d <> 0` by metis_tac[MULT, NOT_ZERO_LT_ZERO] >> 1169 metis_tac[EQ_MULT_LCANCEL]) >- 1170 rw[divisors_has_cofactor] >> 1171 metis_tac[divisors_element, divisors_has_cofactor, divide_by_cofactor]); 1172 1173(* 1174> divisors_divisors_bij; 1175val it = |- !n. 0 < n ==> (\d. n DIV d) PERMUTES divisors n: thm 1176*) 1177 1178(* ------------------------------------------------------------------------- *) 1179(* Gauss' Little Theorem *) 1180(* ------------------------------------------------------------------------- *) 1181(* ------------------------------------------------------------------------- *) 1182(* Gauss' Little Theorem: sum of phi over divisors *) 1183(* ------------------------------------------------------------------------- *) 1184(* ------------------------------------------------------------------------- *) 1185(* Gauss' Little Theorem: A general theory on sum over divisors *) 1186(* ------------------------------------------------------------------------- *) 1187 1188(* 1189Let n = 6. (divisors 6) = {1, 2, 3, 6} 1190 IMAGE coprimes (divisors 6) 1191= {coprimes 1, coprimes 2, coprimes 3, coprimes 6} 1192= {{1}, {1}, {1, 2}, {1, 5}} <-- will collapse 1193 IMAGE (preimage (gcd 6) (count 6)) (divisors 6) 1194= {{preimage in count 6 of those gcd 6 j = 1}, 1195 {preimage in count 6 of those gcd 6 j = 2}, 1196 {preimage in count 6 of those gcd 6 j = 3}, 1197 {preimage in count 6 of those gcd 6 j = 6}} 1198= {{1, 5}, {2, 4}, {3}, {6}} 1199= {1x{1, 5}, 2x{1, 2}, 3x{1}, 6x{1}} 1200!s. s IN (IMAGE (preimage (gcd n) (count n)) (divisors n)) 1201==> ?d. d divides n /\ d < n /\ s = preimage (gcd n) (count n) d 1202==> ?d. d divides n /\ d < n /\ s = IMAGE (TIMES d) (coprimes ((gcd n d) DIV d)) 1203 1204 IMAGE (feq_class (count 6) (gcd 6)) (divisors 6) 1205= {{feq_class in count 6 of those gcd 6 j = 1}, 1206 {feq_class in count 6 of those gcd 6 j = 2}, 1207 {feq_class in count 6 of those gcd 6 j = 3}, 1208 {feq_class in count 6 of those gcd 6 j = 6}} 1209= {{1, 5}, {2, 4}, {3}, {6}} 1210= {1x{1, 5}, 2x{1, 2}, 3x{1}, 6x{1}} 1211That is: CARD {1, 5} = CARD (coprime 6) = CARD (coprime (6 DIV 1)) 1212 CARD {2, 4} = CARD (coprime 3) = CARD (coprime (6 DIV 2)) 1213 CARD {3} = CARD (coprime 2) = CARD (coprime (6 DIV 3))) 1214 CARD {6} = CARD (coprime 1) = CARD (coprime (6 DIV 6))) 1215 1216*) 1217(* Note: 1218 In general, what is the condition for: SIGMA f s = SIGMA g t ? 1219 Conceptually, 1220 SIGMA f s = f s1 + f s2 + f s3 + ... + f sn 1221 and SIGMA g t = g t1 + g t2 + g t3 + ... + g tm 1222 1223SUM_IMAGE_eq_SUM_MAP_SET_TO_LIST 1224 1225Use disjoint_bigunion_card 1226|- !P. FINITE P /\ EVERY_FINITE P /\ PAIR_DISJOINT P ==> (CARD (BIGUNION P) = SIGMA CARD P) 1227If a partition P = {s | condition on s} the element s = IMAGE g t 1228e.g. P = {{1, 5} {2, 4} {3} {6}} 1229 = {IMAGE (TIMES 1) (coprimes 6/1), 1230 IMAGE (TIMES 2) (coprimes 6/2), 1231 IMAGE (TIMES 3) (coprimes 6/3), 1232 IMAGE (TIMES 6) (coprimes 6/6)} 1233 = IMAGE (\d. TIMES d o coprimes (6/d)) {1, 2, 3, 6} 1234 1235*) 1236 1237(* Theorem: d divides n ==> !j. j IN gcd_matches n d ==> j DIV d IN coprimes_by n d *) 1238(* Proof: 1239 When n = 0, gcd_matches 0 d = {} by gcd_matches_0, hence trivially true. 1240 Otherwise, 1241 By coprimes_by_def, this is to show: 1242 0 < n /\ d divides n ==> !j. j IN gcd_matches n d ==> j DIV d IN coprimes (n DIV d) 1243 Note j IN gcd_matches n d 1244 ==> d divides j by gcd_matches_element_divides 1245 Also d IN gcd_matches n d by gcd_matches_has_divisor 1246 so 0 < d /\ (d = gcd j n) by gcd_matches_element 1247 or d <> 0 /\ (d = gcd n j) by GCD_SYM 1248 With the given d divides n, 1249 j = d * (j DIV d) by DIVIDES_EQN, MULT_COMM, 0 < d 1250 n = d * (n DIV d) by DIVIDES_EQN, MULT_COMM, 0 < d 1251 Hence d = d * gcd (n DIV d) (j DIV d) by GCD_COMMON_FACTOR 1252 or d * 1 = d * gcd (n DIV d) (j DIV d) by MULT_RIGHT_1 1253 giving 1 = gcd (n DIV d) (j DIV d) by EQ_MULT_LCANCEL, d <> 0 1254 or coprime (j DIV d) (n DIV d) by GCD_SYM 1255 Also j IN natural n by gcd_matches_subset, SUBSET_DEF 1256 Hence 0 < j DIV d /\ j DIV d <= n DIV d by natural_cofactor_natural_reduced 1257 or j DIV d IN coprimes (n DIV d) by coprimes_element 1258*) 1259val gcd_matches_divisor_element = store_thm( 1260 "gcd_matches_divisor_element", 1261 ``!n d. d divides n ==> !j. j IN gcd_matches n d ==> j DIV d IN coprimes_by n d``, 1262 rpt strip_tac >> 1263 Cases_on `n = 0` >- 1264 metis_tac[gcd_matches_0, NOT_IN_EMPTY] >> 1265 `0 < n` by decide_tac >> 1266 rw[coprimes_by_def] >> 1267 `d divides j` by metis_tac[gcd_matches_element_divides] >> 1268 `0 < d /\ 0 < j /\ j <= n /\ (d = gcd n j)` by metis_tac[gcd_matches_has_divisor, gcd_matches_element, GCD_SYM] >> 1269 `d <> 0` by decide_tac >> 1270 `(j = d * (j DIV d)) /\ (n = d * (n DIV d))` by metis_tac[DIVIDES_EQN, MULT_COMM] >> 1271 `coprime (n DIV d) (j DIV d)` by metis_tac[GCD_COMMON_FACTOR, MULT_RIGHT_1, EQ_MULT_LCANCEL] >> 1272 `0 < j DIV d /\ j DIV d <= n DIV d` by metis_tac[natural_cofactor_natural_reduced, natural_element] >> 1273 metis_tac[coprimes_element, GCD_SYM]); 1274 1275(* Theorem: d divides n ==> BIJ (\j. j DIV d) (gcd_matches n d) (coprimes_by n d) *) 1276(* Proof: 1277 When n = 0, gcd_matches 0 d = {} by gcd_matches_0 1278 and coprimes_by 0 d = {} by coprimes_by_0, hence trivially true. 1279 Otherwise, 1280 By definitions, this is to show: 1281 (1) j IN gcd_matches n d ==> j DIV d IN coprimes_by n d 1282 True by gcd_matches_divisor_element. 1283 (2) j IN gcd_matches n d /\ j' IN gcd_matches n d /\ j DIV d = j' DIV d ==> j = j' 1284 Note j IN gcd_matches n d /\ j' IN gcd_matches n d 1285 ==> d divides j /\ d divides j' by gcd_matches_element_divides 1286 Also d IN (gcd_matches n d) by gcd_matches_has_divisor 1287 so 0 < d by gcd_matches_element 1288 Thus j = (j DIV d) * d by DIVIDES_EQN, 0 < d 1289 and j' = (j' DIV d) * d by DIVIDES_EQN, 0 < d 1290 Since j DIV d = j' DIV d, j = j'. 1291 (3) same as (1), true by gcd_matches_divisor_element, 1292 (4) d divides n /\ x IN coprimes_by n d ==> ?j. j IN gcd_matches n d /\ (j DIV d = x) 1293 Note x IN coprimes (n DIV d) by coprimes_by_def 1294 ==> 0 < x /\ x <= n DIV d /\ (coprime x (n DIV d)) by coprimes_element 1295 And d divides n /\ 0 < n 1296 ==> 0 < d /\ d <> 0 by ZERO_DIVIDES, 0 < n 1297 Giving (x * d) DIV d = x by MULT_DIV, 0 < d 1298 Let j = x * d. so j DIV d = x by above 1299 Then d divides j by divides_def 1300 ==> j = (j DIV d) * d by DIVIDES_EQN, 0 < d 1301 Note d divides n 1302 ==> n = (n DIV d) * d by DIVIDES_EQN, 0 < d 1303 Hence gcd j n 1304 = gcd (d * (j DIV d)) (d * (n DIV d)) by MULT_COMM 1305 = d * gcd (j DIV d) (n DIV d) by GCD_COMMON_FACTOR 1306 = d * gcd x (n DIV d) by x = j DIV d 1307 = d * 1 by coprime x (n DIV d) 1308 = d by MULT_RIGHT_1 1309 Since j = x * d, 0 < j by MULT_EQ_0, 0 < x, 0 < d 1310 Also x <= n DIV d 1311 means j DIV d <= n DIV d by x = j DIV d 1312 so (j DIV d) * d <= (n DIV d) * d by LE_MULT_RCANCEL, d <> 0 1313 or j <= n by above 1314 Hence j IN gcd_matches n d by gcd_matches_element 1315*) 1316val gcd_matches_bij_coprimes_by = store_thm( 1317 "gcd_matches_bij_coprimes_by", 1318 ``!n d. d divides n ==> BIJ (\j. j DIV d) (gcd_matches n d) (coprimes_by n d)``, 1319 rpt strip_tac >> 1320 Cases_on `n = 0` >| [ 1321 `gcd_matches n d = {}` by rw[gcd_matches_0] >> 1322 `coprimes_by n d = {}` by rw[coprimes_by_0] >> 1323 rw[], 1324 `0 < n` by decide_tac >> 1325 rw[BIJ_DEF, INJ_DEF, SURJ_DEF, EQ_IMP_THM] >- 1326 rw[GSYM gcd_matches_divisor_element] >- 1327 metis_tac[gcd_matches_element_divides, gcd_matches_has_divisor, gcd_matches_element, DIVIDES_EQN] >- 1328 rw[GSYM gcd_matches_divisor_element] >> 1329 `0 < x /\ x <= n DIV d /\ (coprime x (n DIV d))` by metis_tac[coprimes_by_def, coprimes_element] >> 1330 `0 < d /\ d <> 0` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >> 1331 `(x * d) DIV d = x` by rw[MULT_DIV] >> 1332 qabbrev_tac `j = x * d` >> 1333 `d divides j` by metis_tac[divides_def] >> 1334 `(n = (n DIV d) * d) /\ (j = (j DIV d) * d)` by rw[GSYM DIVIDES_EQN] >> 1335 `gcd j n = d` by metis_tac[GCD_COMMON_FACTOR, MULT_COMM, MULT_RIGHT_1] >> 1336 `0 < j` by metis_tac[MULT_EQ_0, NOT_ZERO] >> 1337 `j <= n` by metis_tac[LE_MULT_RCANCEL] >> 1338 metis_tac[gcd_matches_element] 1339 ]); 1340 1341(* Theorem: 0 < n /\ d divides n ==> BIJ (\j. j DIV d) (gcd_matches n d) (coprimes (n DIV d)) *) 1342(* Proof: by gcd_matches_bij_coprimes_by, coprimes_by_by_divisor *) 1343val gcd_matches_bij_coprimes = store_thm( 1344 "gcd_matches_bij_coprimes", 1345 ``!n d. 0 < n /\ d divides n ==> BIJ (\j. j DIV d) (gcd_matches n d) (coprimes (n DIV d))``, 1346 metis_tac[gcd_matches_bij_coprimes_by, coprimes_by_by_divisor]); 1347 1348(* Note: it is not useful to show: 1349 CARD o (gcd_matches n) = CARD o coprimes, 1350 as FUN_EQ_THM will demand: CARD (gcd_matches n x) = CARD (coprimes x), 1351 which is not possible. 1352*) 1353 1354(* Theorem: 0 < n ==> (divisors n = IMAGE (gcd n) (natural n)) *) 1355(* Proof: 1356 divisors n 1357 = {d | d <= n /\ d divides n} by divisors_def 1358 = {d | 0 < d /\ d <= n /\ d divides n} by divisor_pos 1359 = {d | d IN (natural n) /\ d divides n} by natural_element 1360 = {d | d IN (natural n) /\ (gcd d n = d)} by divides_iff_gcd_fix 1361 = {d | d IN (natural n) /\ (gcd n d = d)} by GCD_SYM 1362 = {gcd n d | d | d IN (natural n)} by replacemnt 1363 = IMAGE (gcd n) (natural n) by IMAGE_DEF 1364 1365 Or, by divisors_def, natuarl_elemnt, IN_IMAGE, this is to show: 1366 (1) 0 < n /\ x <= n /\ x divides n ==> ?x'. (x = gcd n x') /\ 0 < x' /\ x' <= n 1367 Note x divides n ==> 0 < x by divisor_pos 1368 Also x divides n ==> gcd x n = x by divides_iff_gcd_fix 1369 or gcd n x = x by GCD_SYM 1370 Take this x, and the result follows. 1371 (2) 0 < n /\ 0 < x' /\ x' <= n ==> gcd n x' <= n /\ gcd n x' divides n 1372 Note gcd n x' divides n by GCD_IS_GREATEST_COMMON_DIVISOR 1373 and gcd n x' <= n by DIVIDES_LE, 0 < n. 1374*) 1375val divisors_eq_gcd_image = store_thm( 1376 "divisors_eq_gcd_image", 1377 ``!n. 0 < n ==> (divisors n = IMAGE (gcd n) (natural n))``, 1378 rw_tac std_ss[divisors_def, GSPECIFICATION, EXTENSION, IN_IMAGE, natural_element, EQ_IMP_THM] >- 1379 metis_tac[divisor_pos, divides_iff_gcd_fix, GCD_SYM] >- 1380 metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR, DIVIDES_LE] >> 1381 metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR]); 1382 1383(* Theorem: feq_class (gcd n) (natural n) d = gcd_matches n d *) 1384(* Proof: 1385 feq_class (gcd n) (natural n) d 1386 = {x | x IN natural n /\ (gcd n x = d)} by feq_class_def 1387 = {j | j IN natural n /\ (gcd j n = d)} by GCD_SYM 1388 = gcd_matches n d by gcd_matches_def 1389*) 1390val gcd_eq_equiv_class = store_thm( 1391 "gcd_eq_equiv_class", 1392 ``!n d. feq_class (gcd n) (natural n) d = gcd_matches n d``, 1393 rewrite_tac[feq_class_def, gcd_matches_def] >> 1394 rw[EXTENSION, GCD_SYM]); 1395 1396(* Theorem: feq_class (gcd n) (natural n) = gcd_matches n *) 1397(* Proof: by FUN_EQ_THM, gcd_eq_equiv_class *) 1398val gcd_eq_equiv_class_fun = store_thm( 1399 "gcd_eq_equiv_class_fun", 1400 ``!n. feq_class (gcd n) (natural n) = gcd_matches n``, 1401 rw[FUN_EQ_THM, gcd_eq_equiv_class]); 1402 1403(* Theorem: 0 < n ==> (partition (feq (gcd n)) (natural n) = IMAGE (gcd_matches n) (divisors n)) *) 1404(* Proof: 1405 partition (feq (gcd n)) (natural n) 1406 = IMAGE (equiv_class (feq (gcd n)) (natural n)) (natural n) by partition_elements 1407 = IMAGE ((feq_class (gcd n) (natural n)) o (gcd n)) (natural n) by feq_class_fun 1408 = IMAGE ((gcd_matches n) o (gcd n)) (natural n) by gcd_eq_equiv_class_fun 1409 = IMAGE (gcd_matches n) (IMAGE (gcd n) (natural n)) by IMAGE_COMPOSE 1410 = IMAGE (gcd_matches n) (divisors n) by divisors_eq_gcd_image, 0 < n 1411*) 1412val gcd_eq_partition_by_divisors = store_thm( 1413 "gcd_eq_partition_by_divisors", 1414 ``!n. 0 < n ==> (partition (feq (gcd n)) (natural n) = IMAGE (gcd_matches n) (divisors n))``, 1415 rpt strip_tac >> 1416 qabbrev_tac `f = gcd n` >> 1417 qabbrev_tac `s = natural n` >> 1418 `partition (feq f) s = IMAGE (equiv_class (feq f) s) s` by rw[partition_elements] >> 1419 `_ = IMAGE ((feq_class f s) o f) s` by rw[feq_class_fun] >> 1420 `_ = IMAGE ((gcd_matches n) o f) s` by rw[gcd_eq_equiv_class_fun, Abbr`f`, Abbr`s`] >> 1421 `_ = IMAGE (gcd_matches n) (IMAGE f s)` by rw[IMAGE_COMPOSE] >> 1422 `_ = IMAGE (gcd_matches n) (divisors n)` by rw[divisors_eq_gcd_image, Abbr`f`, Abbr`s`] >> 1423 rw[]); 1424 1425(* Theorem: (feq (gcd n)) equiv_on (natural n) *) 1426(* Proof: 1427 By feq_equiv |- !s f. feq f equiv_on s 1428 Taking s = upto n, f = natural n. 1429*) 1430val gcd_eq_equiv_on_natural = store_thm( 1431 "gcd_eq_equiv_on_natural", 1432 ``!n. (feq (gcd n)) equiv_on (natural n)``, 1433 rw[feq_equiv]); 1434 1435(* Theorem: SIGMA f (natural n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (natural n)) *) 1436(* Proof: 1437 Let g = gcd n, s = natural n. 1438 Since FINITE s by natural_finite 1439 and (feq g) equiv_on s by feq_equiv 1440 The result follows by set_sigma_by_partition 1441*) 1442val sum_over_natural_by_gcd_partition = store_thm( 1443 "sum_over_natural_by_gcd_partition", 1444 ``!f n. SIGMA f (natural n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (natural n))``, 1445 rw[feq_equiv, natural_finite, set_sigma_by_partition]); 1446 1447(* Theorem: SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n)) *) 1448(* Proof: 1449 If n = 0, 1450 LHS = SIGMA f (natural 0) 1451 = SIGMA f {} by natural_0 1452 = 0 by SUM_IMAGE_EMPTY 1453 RHS = SIGMA (SIGMA f) (IMAGE (gcd_matches 0) (divisors 0)) 1454 = SIGMA (SIGMA f) (IMAGE (gcd_matches 0) {0}) by divisors_0 1455 = SIGMA (SIGMA f) {gcd_matches 0 0} by IMAGE_SING 1456 = SIGMA (SIGMA f) {{}} by gcd_matches_0 1457 = SIGMA f {} by SUM_IMAGE_SING 1458 = 0 = LHS by SUM_IMAGE_EMPTY 1459 Otherwise 0 < n, 1460 SIGMA f (natural n) 1461 = SIGMA (SIGMA f) (partition (feq (gcd n)) (natural n)) by sum_over_natural_by_gcd_partition 1462 = SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n)) by gcd_eq_partition_by_divisors, 0 < n 1463*) 1464val sum_over_natural_by_divisors = store_thm( 1465 "sum_over_natural_by_divisors", 1466 ``!f n. SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (gcd_matches n) (divisors n))``, 1467 rpt strip_tac >> 1468 Cases_on `n = 0` >| [ 1469 `natural n = {}` by rw_tac std_ss[natural_0] >> 1470 `divisors n = {0}` by rw_tac std_ss[divisors_0] >> 1471 `IMAGE (gcd_matches n) (divisors n) = {{}}` by rw[gcd_matches_0] >> 1472 rw[SUM_IMAGE_SING], 1473 rw[sum_over_natural_by_gcd_partition, gcd_eq_partition_by_divisors] 1474 ]); 1475 1476(* Theorem: 0 < n ==> INJ (gcd_matches n) (divisors n) univ(num) *) 1477(* Proof: 1478 By INJ_DEF, this is to show: 1479 x IN divisors n /\ y IN divisors n /\ gcd_matches n x = gcd_matches n y ==> x = y 1480 If n = 0, 1481 then divisors n = {} by divisors_0 1482 hence trivially true. 1483 Otherwise 0 < n, 1484 Note x IN divisors n 1485 ==> x <= n /\ x divides n by divisors_element 1486 also y IN divisors n 1487 ==> y <= n /\ y divides n by divisors_element 1488 Hence (gcd x n = x) /\ (gcd y n = y) by divides_iff_gcd_fix 1489 Since x divides n, 0 < x by divisor_pos, 0 < n 1490 Giving x IN gcd_matches n x by gcd_matches_element 1491 so x IN gcd_matches n y by gcd_matches n x = gcd_matches n y 1492 with gcd x n = y by gcd_matches_element 1493 Therefore y = gcd x n = x. 1494*) 1495val gcd_matches_from_divisors_inj = store_thm( 1496 "gcd_matches_from_divisors_inj", 1497 ``!n. INJ (gcd_matches n) (divisors n) univ(:num -> bool)``, 1498 rw[INJ_DEF] >> 1499 Cases_on `n = 0` >> 1500 fs[divisors_0] >> 1501 `0 < n` by decide_tac >> 1502 `x <= n /\ x divides n /\ y <= n /\ y divides n` by metis_tac[divisors_element] >> 1503 `(gcd x n = x) /\ (gcd y n = y)` by rw[GSYM divides_iff_gcd_fix] >> 1504 metis_tac[divisor_pos, gcd_matches_element]); 1505 1506(* Theorem: 0 < n ==> (CARD o (gcd_matches n) = CARD o (coprimes_by n)) *) 1507(* Proof: 1508 By composition and FUN_EQ_THM, this is to show: 1509 !x. CARD (gcd_matches n x) = CARD (coprimes_by n x) 1510 If x divides n, 1511 Then BIJ (\j. j DIV x) (gcd_matches n x) (coprimes_by n x) by gcd_matches_bij_coprimes_by 1512 Also FINITE (gcd_matches n x) by gcd_matches_finite 1513 and FINITE (coprimes_by n x) by coprimes_by_finite 1514 Hence CARD (gcd_matches n x) = CARD (coprimes_by n x) by FINITE_BIJ_CARD_EQ 1515 If ~(x divides n), 1516 If n = 0, 1517 then gcd_matches 0 x = {} by gcd_matches_0 1518 and coprimes_by 0 x = {} by coprimes_by_0 1519 Hence true. 1520 If n <> 0, 1521 then gcd_matches n x = {} by gcd_matches_eq_empty, 0 < n 1522 and coprimes_by n x = {} by coprimes_by_eq_empty, 0 < n 1523 Hence CARD {} = CARD {}. 1524*) 1525val gcd_matches_and_coprimes_by_same_size = store_thm( 1526 "gcd_matches_and_coprimes_by_same_size", 1527 ``!n. CARD o (gcd_matches n) = CARD o (coprimes_by n)``, 1528 rw[FUN_EQ_THM] >> 1529 Cases_on `x divides n` >| [ 1530 `BIJ (\j. j DIV x) (gcd_matches n x) (coprimes_by n x)` by rw[gcd_matches_bij_coprimes_by] >> 1531 `FINITE (gcd_matches n x)` by rw[gcd_matches_finite] >> 1532 `FINITE (coprimes_by n x)` by rw[coprimes_by_finite] >> 1533 metis_tac[FINITE_BIJ_CARD_EQ], 1534 Cases_on `n = 0` >- 1535 rw[gcd_matches_0, coprimes_by_0] >> 1536 `gcd_matches n x = {}` by rw[gcd_matches_eq_empty] >> 1537 `coprimes_by n x = {}` by rw[coprimes_by_eq_empty] >> 1538 rw[] 1539 ]); 1540 1541(* HERE; to fix! *) 1542 1543(* Theorem: 0 < n ==> (CARD o (coprimes_by n) = \d. phi (if d IN (divisors n) then n DIV d else 0)) *) 1544(* Proof: 1545 By FUN_EQ_THM, 1546 CARD o (coprimes_by n) x 1547 = CARD (coprimes_by n x) by composition, combinTheory.o_THM 1548 = CARD (if x divides n then coprimes (n DIV x) else {}) by coprimes_by_def, 0 < n 1549 If x divides n, 1550 x <= n by DIVIDES_LE 1551 so x IN (divisors n) by divisors_element 1552 CARD o (coprimes_by n) x 1553 = CARD (coprimes (n DIV x)) 1554 = phi (n DIV x) by phi_def 1555 If ~(x divides n), 1556 x NOTIN (divisors n) by divisors_element 1557 CARD o (coprimes_by n) x 1558 = CARD {} 1559 = 0 by CARD_EMPTY 1560 = phi 0 by phi_0 1561 Hence the same function as: 1562 \d. phi (if d IN (divisors n) then n DIV d else 0) 1563*) 1564val coprimes_by_with_card = store_thm( 1565 "coprimes_by_with_card", 1566 ``!n. 0 < n ==> (CARD o (coprimes_by n) = \d. phi (if d IN (divisors n) then n DIV d else 0))``, 1567 rw[coprimes_by_def, phi_def, divisors_def, FUN_EQ_THM] >> 1568 metis_tac[DIVIDES_LE, coprimes_0]); 1569 1570(* Theorem: 0 < n ==> !x. x IN (divisors n) ==> ((CARD o (coprimes_by n)) x = (\d. phi (n DIV d)) x) *) 1571(* Proof: 1572 Since x IN (divisors n) ==> x divides n by divisors_element 1573 CARD o (coprimes_by n) x 1574 = CARD (coprimes (n DIV x)) by coprimes_by_def 1575 = phi (n DIV x) by phi_def 1576*) 1577val coprimes_by_divisors_card = store_thm( 1578 "coprimes_by_divisors_card", 1579 ``!n. 0 < n ==> !x. x IN (divisors n) ==> ((CARD o (coprimes_by n)) x = (\d. phi (n DIV d)) x)``, 1580 rw[coprimes_by_def, phi_def, divisors_def]); 1581 1582(* 1583SUM_IMAGE_CONG |- (s1 = s2) /\ (!x. x IN s2 ==> (f1 x = f2 x)) ==> (SIGMA f1 s1 = SIGMA f2 s2) 1584*) 1585 1586(* Theorem: n = SIGMA phi (divisors n) *) 1587(* Proof: 1588 If n = 0, 1589 SIGMA phi (divisors 0) 1590 = SIGMA phi {0} by divisors_0 1591 = phi 0 by SUM_IMAGE_SING 1592 = 0 by phi_0 1593 If n <> 0, 0 < n. 1594 Note INJ (gcd_matches n) (divisors n) univ(:num -> bool) by gcd_matches_from_divisors_inj 1595 and (\d. n DIV d) PERMUTES (divisors n) by divisors_divisors_bij, 0 < n 1596 n = CARD (natural n) by natural_card 1597 = SIGMA CARD (partition (feq (gcd n)) (natural n)) by partition_CARD 1598 = SIGMA CARD (IMAGE (gcd_matches n) (divisors n)) by gcd_eq_partition_by_divisors 1599 = SIGMA (CARD o (gcd_matches n)) (divisors n) by sum_image_by_composition 1600 = SIGMA (CARD o (coprimes_by n)) (divisors n) by gcd_matches_and_coprimes_by_same_size 1601 = SIGMA (\d. phi (n DIV d)) (divisors n) by SUM_IMAGE_CONG, coprimes_by_divisors_card 1602 = SIGMA phi (divisors n) by sum_image_by_permutation 1603*) 1604val Gauss_little_thm = store_thm( 1605 "Gauss_little_thm", 1606 ``!n. n = SIGMA phi (divisors n)``, 1607 rpt strip_tac >> 1608 Cases_on `n = 0` >- 1609 rw[divisors_0, SUM_IMAGE_SING, phi_0] >> 1610 `0 < n` by decide_tac >> 1611 `FINITE (natural n)` by rw[natural_finite] >> 1612 `(feq (gcd n)) equiv_on (natural n)` by rw[gcd_eq_equiv_on_natural] >> 1613 `INJ (gcd_matches n) (divisors n) univ(:num -> bool)` by rw[gcd_matches_from_divisors_inj] >> 1614 `(\d. n DIV d) PERMUTES (divisors n)` by rw[divisors_divisors_bij] >> 1615 `FINITE (divisors n)` by rw[divisors_finite] >> 1616 `n = CARD (natural n)` by rw[natural_card] >> 1617 `_ = SIGMA CARD (partition (feq (gcd n)) (natural n))` by rw[partition_CARD] >> 1618 `_ = SIGMA CARD (IMAGE (gcd_matches n) (divisors n))` by rw[gcd_eq_partition_by_divisors] >> 1619 `_ = SIGMA (CARD o (gcd_matches n)) (divisors n)` by prove_tac[sum_image_by_composition] >> 1620 `_ = SIGMA (CARD o (coprimes_by n)) (divisors n)` by rw[gcd_matches_and_coprimes_by_same_size] >> 1621 `_ = SIGMA (\d. phi (n DIV d)) (divisors n)` by rw[SUM_IMAGE_CONG, coprimes_by_divisors_card] >> 1622 `_ = SIGMA phi (divisors n)` by metis_tac[sum_image_by_permutation] >> 1623 rw[]); 1624 1625(* This is a milestone theorem. *) 1626 1627(* ------------------------------------------------------------------------- *) 1628(* Recursive definition of phi *) 1629(* ------------------------------------------------------------------------- *) 1630 1631(* Define phi by recursion *) 1632val rec_phi_def = tDefine "rec_phi" ` 1633 rec_phi n = if n = 0 then 0 1634 else if n = 1 then 1 1635 else n - SIGMA rec_phi { m | m < n /\ m divides n}` 1636 (WF_REL_TAC `$< : num -> num -> bool` >> srw_tac[][]); 1637(* This is the recursive form of Gauss' Little Theorem: n = SUM phi m, m divides n *) 1638 1639(* Just using Define without any condition will trigger: 1640 1641Initial goal: 1642 1643?R. WF R /\ !n a. n <> 0 /\ n <> 1 /\ a IN {m | m < n /\ m divides n} ==> R a n 1644 1645Unable to prove termination! 1646 1647Try using "TotalDefn.tDefine <name> <quotation> <tac>". 1648 1649The termination goal has been set up using Defn.tgoal <defn>. 1650 1651So one can set up: 1652g `?R. WF R /\ !n a. n <> 0 /\ n <> 1 /\ a IN {m | m < n /\ m divides n} ==> R a n`; 1653e (WF_REL_TAC `$< : num -> num -> bool`); 1654e (srw[][]); 1655 1656which gives the tDefine solution. 1657*) 1658 1659(* Theorem: rec_phi 0 = 0 *) 1660(* Proof: by rec_phi_def *) 1661val rec_phi_0 = store_thm( 1662 "rec_phi_0", 1663 ``rec_phi 0 = 0``, 1664 rw[rec_phi_def]); 1665 1666(* Theorem: rec_phi 1 = 1 *) 1667(* Proof: by rec_phi_def *) 1668val rec_phi_1 = store_thm( 1669 "rec_phi_1", 1670 ``rec_phi 1 = 1``, 1671 rw[Once rec_phi_def]); 1672 1673(* Theorem: rec_phi n = phi n *) 1674(* Proof: 1675 By complete induction on n. 1676 If n = 0, 1677 rec_phi 0 = 0 by rec_phi_0 1678 = phi 0 by phi_0 1679 If n = 1, 1680 rec_phi 1 = 1 by rec_phi_1 1681 = phi 1 by phi_1 1682 Othewise, 1683 Let s = {m | m < n /\ m divides n}. 1684 Note s SUBSET (count n) by SUBSET_DEF 1685 thus FINITE s by SUBSET_FINITE, FINITE_COUNT 1686 Hence !m. m IN s 1687 ==> (rec_phi m = phi m) by induction hypothesis 1688 Also n NOTIN s by EXTENSION 1689 and n INSERT s 1690 = {m | m <= n /\ m divides n} 1691 = divisors n by divisors_def, EXTENSION, LESS_OR_EQ 1692 1693 rec_phi n 1694 = n - (SIGMA rec_phi s) by rec_phi_def 1695 = n - (SIGMA phi s) by SUM_IMAGE_CONG, rec_phi m = phi m 1696 = (SIGMA phi (divisors n)) - (SIGMA phi s) by Gauss' Little Theorem 1697 = (SIGMA phi (n INSERT s)) - (SIGMA phi s) by divisors n = n INSERT s 1698 = (phi n + SIGMA phi (s DELETE n)) - (SIGMA phi s) by SUM_IMAGE_THM 1699 = (phi n + SIGMA phi s) - (SIGMA phi s) by DELETE_NON_ELEMENT 1700 = phi n by ADD_SUB 1701*) 1702val rec_phi_eq_phi = store_thm( 1703 "rec_phi_eq_phi", 1704 ``!n. rec_phi n = phi n``, 1705 completeInduct_on `n` >> 1706 Cases_on `n = 0` >- 1707 rw[rec_phi_0, phi_0] >> 1708 Cases_on `n = 1` >- 1709 rw[rec_phi_1, phi_1] >> 1710 `0 < n /\ 1 < n` by decide_tac >> 1711 qabbrev_tac `s = {m | m < n /\ m divides n}` >> 1712 qabbrev_tac `t = SIGMA rec_phi s` >> 1713 `!m. m IN s <=> m < n /\ m divides n` by rw[Abbr`s`] >> 1714 `!m. m IN s ==> (rec_phi m = phi m)` by rw[] >> 1715 `t = SIGMA phi s` by rw[SUM_IMAGE_CONG, Abbr`t`] >> 1716 `s SUBSET (count n)` by rw[SUBSET_DEF] >> 1717 `FINITE s` by metis_tac[SUBSET_FINITE, FINITE_COUNT] >> 1718 `n NOTIN s` by rw[] >> 1719 (`n INSERT s = divisors n` by (rw[divisors_def, EXTENSION] >> metis_tac[LESS_OR_EQ, DIVIDES_REFL])) >> 1720 `n = SIGMA phi (divisors n)` by rw[Gauss_little_thm] >> 1721 `_ = phi n + SIGMA phi (s DELETE n)` by rw[GSYM SUM_IMAGE_THM] >> 1722 `_ = phi n + t` by metis_tac[DELETE_NON_ELEMENT] >> 1723 `rec_phi n = n - t` by metis_tac[rec_phi_def] >> 1724 decide_tac); 1725 1726 1727(* ------------------------------------------------------------------------- *) 1728(* Not Used *) 1729(* ------------------------------------------------------------------------- *) 1730 1731(* Theorem: INJ (coprimes) (univ(:num) DIFF {1}) univ(:num -> bool) *) 1732(* Proof: 1733 By INJ_DEF, this is to show: 1734 x <> 1 /\ y <> 1 /\ coprimes x = coprimes y ==> x = y 1735 If x = 0, then y = 0 by coprimes_eq_empty 1736 If y = 0, then x = 0 by coprimes_eq_empty 1737 If x <> 0 and y <> 0, 1738 with x <> 1 and y <> 1 by given 1739 then 1 < x and 1 < y. 1740 Since MAX_SET (coprimes x) = x - 1 by coprimes_max, 1 < x 1741 and MAX_SET (coprimes y) = y - 1 by coprimes_max, 1 < y 1742 If coprimes x = coprimes y, 1743 x - 1 = y - 1 by above 1744 Hence x = y by CANCEL_SUB 1745*) 1746val coprimes_from_notone_inj = store_thm( 1747 "coprimes_from_notone_inj", 1748 ``INJ (coprimes) (univ(:num) DIFF {1}) univ(:num -> bool)``, 1749 rw[INJ_DEF] >> 1750 Cases_on `x = 0` >- 1751 metis_tac[coprimes_eq_empty] >> 1752 Cases_on `y = 0` >- 1753 metis_tac[coprimes_eq_empty] >> 1754 `1 < x /\ 1 < y` by decide_tac >> 1755 `x - 1 = y - 1` by metis_tac[coprimes_max] >> 1756 decide_tac); 1757(* Not very useful. *) 1758 1759(* Theorem: divisors n = IMAGE (gcd n) (upto n) *) 1760(* Proof: 1761 divisors n 1762 = {d | d <= n /\ d divides n} by divisors_def 1763 = {d | d <= n /\ (gcd d n = d)} by divides_iff_gcd_fix 1764 = {d | d <= n /\ (gcd n d = d)} by GCD_SYM 1765 = {gcd n d | d | d <= n} by replacemnt 1766 = IMAGE (gcd n) {d | d <= n} by IMAGE_DEF 1767 = IMAGE (gcd n) (count (SUC n)) by count_def 1768 = IMAGE (gcd n) (upto n) by notation 1769 1770 By divisors_def, IN_IMAGE and EXTENSION, this is to show: 1771 (1) x <= n /\ x divides n ==> ?x'. (x = gcd n x') /\ x' < SUC n 1772 x <= n ==> x < SUC n by LESS_EQ_IMP_LESS_SUC 1773 x divides n ==> x = gcd x n by divides_iff_gcd_fix 1774 = gcd n x by GCD_SYM 1775 (2) x' < SUC n ==> gcd n x' <= n /\ gcd n x' divides n 1776 gcd n x' divides n by GCD_IS_GREATEST_COMMON_DIVISOR 1777 If n = 0, x' < 1. 1778 That is, x' = 0 by arithmetic 1779 so gcd 0 0 = 0 <= 0 by GCD_0R 1780 and 0 divides 0 by ZERO_DIVIDES 1781 If n <> 0, 0 < n. 1782 gcd n x' divides n 1783 ==> gcd n x' <= n by DIVIDES_LE 1784*) 1785val divisors_eq_image_gcd_upto = store_thm( 1786 "divisors_eq_image_gcd_upto", 1787 ``!n. divisors n = IMAGE (gcd n) (upto n)``, 1788 rw[divisors_def, EXTENSION, EQ_IMP_THM] >| [ 1789 `x < SUC n` by decide_tac >> 1790 metis_tac[divides_iff_gcd_fix, GCD_SYM], 1791 Cases_on `n = 0` >| [ 1792 `x' = 0` by decide_tac >> 1793 `gcd 0 0 = 0` by rw[GCD_0R] >> 1794 rw[], 1795 `0 < n` by decide_tac >> 1796 `(gcd n x') divides n` by rw[GCD_IS_GREATEST_COMMON_DIVISOR] >> 1797 rw[DIVIDES_LE] 1798 ], 1799 rw[GCD_IS_GREATEST_COMMON_DIVISOR] 1800 ]); 1801 1802(* Theorem: (feq (gcd n)) equiv_on (upto n) *) 1803(* Proof: 1804 By feq_equiv |- !s f. feq f equiv_on s 1805 Taking s = upto n, f = gcd n. 1806*) 1807val gcd_eq_equiv_on_upto = store_thm( 1808 "gcd_eq_equiv_on_upto", 1809 ``!n. (feq (gcd n)) equiv_on (upto n)``, 1810 rw[feq_equiv]); 1811 1812(* Theorem: partition (feq (gcd n)) (upto n) = IMAGE (preimage (gcd n) (upto n)) (divisors n) *) 1813(* Proof: 1814 Let f = gcd n, s = upto n. 1815 partition (feq f) s 1816 = IMAGE (preimage f s o f) s by feq_partition_by_preimage 1817 = IMAGE (preimage f s) (IMAGE f s) by IMAGE_COMPOSE 1818 = IMAGE (preimage f s) (IMAGE (gcd n) (upto n)) by expansion 1819 = IMAGE (preimage f s) (divisors n) by divisors_eq_image_gcd_upto 1820*) 1821val gcd_eq_upto_partition_by_divisors = store_thm( 1822 "gcd_eq_upto_partition_by_divisors", 1823 ``!n. partition (feq (gcd n)) (upto n) = IMAGE (preimage (gcd n) (upto n)) (divisors n)``, 1824 rpt strip_tac >> 1825 qabbrev_tac `f = gcd n` >> 1826 qabbrev_tac `s = upto n` >> 1827 `partition (feq f) s = IMAGE (preimage f s o f) s` by rw[feq_partition_by_preimage] >> 1828 `_ = IMAGE (preimage f s) (IMAGE f s)` by rw[IMAGE_COMPOSE] >> 1829 rw[divisors_eq_image_gcd_upto, Abbr`f`, Abbr`s`]); 1830 1831(* Theorem: SIGMA f (upto n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (upto n)) *) 1832(* Proof: 1833 Let g = gcd n, s = upto n. 1834 Since FINITE s by upto_finite 1835 and (feq g) equiv_on s by feq_equiv 1836 The result follows by set_sigma_by_partition 1837*) 1838val sum_over_upto_by_gcd_partition = store_thm( 1839 "sum_over_upto_by_gcd_partition", 1840 ``!f n. SIGMA f (upto n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (upto n))``, 1841 rw[feq_equiv, set_sigma_by_partition]); 1842 1843(* Theorem: SIGMA f (upto n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n)) *) 1844(* Proof: 1845 SIGMA f (upto n) 1846 = SIGMA (SIGMA f) (partition (feq (gcd n)) (upto n)) by sum_over_upto_by_gcd_partition 1847 = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n)) by gcd_eq_upto_partition_by_divisors 1848*) 1849val sum_over_upto_by_divisors = store_thm( 1850 "sum_over_upto_by_divisors", 1851 ``!f n. SIGMA f (upto n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (upto n)) (divisors n))``, 1852 rw[sum_over_upto_by_gcd_partition, gcd_eq_upto_partition_by_divisors]); 1853 1854(* Similar results based on count *) 1855 1856(* Theorem: 0 < n ==> (divisors n = IMAGE (gcd n) (count n)) *) 1857(* Proof: 1858 divisors n 1859 = IMAGE (gcd n) (upto n) by divisors_eq_image_gcd_upto 1860 = IMAGE (gcd n) (n INSERT (count n)) by upto_by_count 1861 = (gcd n n) INSERT (IMAGE (gcd n) (count n)) by IMAGE_INSERT 1862 = n INSERT (IMAGE (gcd n) (count n)) by GCD_REF 1863 = (gcd n 0) INSERT (IMAGE (gcd n) (count n)) by GCD_0R 1864 = IMAGE (gcd n) (0 INSERT (count n)) by IMAGE_INSERT 1865 = IMAGE (gcd n) (count n) by IN_COUNT, ABSORPTION, 0 < n. 1866*) 1867val divisors_eq_image_gcd_count = store_thm( 1868 "divisors_eq_image_gcd_count", 1869 ``!n. 0 < n ==> (divisors n = IMAGE (gcd n) (count n))``, 1870 rpt strip_tac >> 1871 `divisors n = IMAGE (gcd n) (upto n)` by rw[divisors_eq_image_gcd_upto] >> 1872 `_ = IMAGE (gcd n) (n INSERT (count n))` by rw[upto_by_count] >> 1873 `_ = n INSERT (IMAGE (gcd n) (count n))` by rw[GCD_REF] >> 1874 `_ = (gcd n 0) INSERT (IMAGE (gcd n) (count n))` by rw[GCD_0R] >> 1875 `_ = IMAGE (gcd n) (0 INSERT (count n))` by rw[] >> 1876 metis_tac[IN_COUNT, ABSORPTION]); 1877 1878(* Theorem: (feq (gcd n)) equiv_on (count n) *) 1879(* Proof: 1880 By feq_equiv |- !s f. feq f equiv_on s 1881 Taking s = upto n, f = count n. 1882*) 1883val gcd_eq_equiv_on_count = store_thm( 1884 "gcd_eq_equiv_on_count", 1885 ``!n. (feq (gcd n)) equiv_on (count n)``, 1886 rw[feq_equiv]); 1887 1888(* Theorem: 0 < n ==> (partition (feq (gcd n)) (count n) = IMAGE (preimage (gcd n) (count n)) (divisors n)) *) 1889(* Proof: 1890 Let f = gcd n, s = count n. 1891 partition (feq f) s 1892 = IMAGE (preimage f s o f) s by feq_partition_by_preimage 1893 = IMAGE (preimage f s) (IMAGE f s) by IMAGE_COMPOSE 1894 = IMAGE (preimage f s) (IMAGE (gcd n) (count n)) by expansion 1895 = IMAGE (preimage f s) (divisors n) by divisors_eq_image_gcd_count, 0 < n 1896*) 1897val gcd_eq_count_partition_by_divisors = store_thm( 1898 "gcd_eq_count_partition_by_divisors", 1899 ``!n. 0 < n ==> (partition (feq (gcd n)) (count n) = IMAGE (preimage (gcd n) (count n)) (divisors n))``, 1900 rpt strip_tac >> 1901 qabbrev_tac `f = gcd n` >> 1902 qabbrev_tac `s = count n` >> 1903 `partition (feq f) s = IMAGE (preimage f s o f) s` by rw[feq_partition_by_preimage] >> 1904 `_ = IMAGE (preimage f s) (IMAGE f s)` by rw[IMAGE_COMPOSE] >> 1905 rw[divisors_eq_image_gcd_count, Abbr`f`, Abbr`s`]); 1906 1907(* Theorem: SIGMA f (count n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (count n)) *) 1908(* Proof: 1909 Let g = gcd n, s = count n. 1910 Since FINITE s by FINITE_COUNT 1911 and (feq g) equiv_on s by feq_equiv 1912 The result follows by set_sigma_by_partition 1913*) 1914val sum_over_count_by_gcd_partition = store_thm( 1915 "sum_over_count_by_gcd_partition", 1916 ``!f n. SIGMA f (count n) = SIGMA (SIGMA f) (partition (feq (gcd n)) (count n))``, 1917 rw[feq_equiv, set_sigma_by_partition]); 1918 1919(* Theorem: 0 < n ==> (SIGMA f (count n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n))) *) 1920(* Proof: 1921 SIGMA f (count n) 1922 = SIGMA (SIGMA f) (partition (feq (gcd n)) (count n)) by sum_over_count_by_gcd_partition 1923 = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n)) by gcd_eq_count_partition_by_divisors 1924*) 1925val sum_over_count_by_divisors = store_thm( 1926 "sum_over_count_by_divisors", 1927 ``!f n. 0 < n ==> (SIGMA f (count n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (count n)) (divisors n)))``, 1928 rw[sum_over_count_by_gcd_partition, gcd_eq_count_partition_by_divisors]); 1929 1930(* Similar results based on natural *) 1931 1932(* Theorem: 0 < n ==> (divisors n = IMAGE (gcd n) (natural n)) *) 1933(* Proof: 1934 divisors n 1935 = IMAGE (gcd n) (upto n) by divisors_eq_image_gcd_upto 1936 = IMAGE (gcd n) (0 INSERT natural n) by upto_by_natural 1937 = (gcd 0 n) INSERT (IMAGE (gcd n) (natural n)) by IMAGE_INSERT 1938 = n INSERT (IMAGE (gcd n) (natural n)) by GCD_0L 1939 = (gcd n n) INSERT (IMAGE (gcd n) (natural n)) by GCD_REF 1940 = IMAGE (gcd n) (n INSERT (natural n)) by IMAGE_INSERT 1941 = IMAGE (gcd n) (natural n) by natural_has_last, ABSORPTION, 0 < n. 1942*) 1943val divisors_eq_image_gcd_natural = store_thm( 1944 "divisors_eq_image_gcd_natural", 1945 ``!n. 0 < n ==> (divisors n = IMAGE (gcd n) (natural n))``, 1946 rpt strip_tac >> 1947 `divisors n = IMAGE (gcd n) (upto n)` by rw[divisors_eq_image_gcd_upto] >> 1948 `_ = IMAGE (gcd n) (0 INSERT (natural n))` by rw[upto_by_natural] >> 1949 `_ = n INSERT (IMAGE (gcd n) (natural n))` by rw[GCD_0L] >> 1950 `_ = (gcd n n) INSERT (IMAGE (gcd n) (natural n))` by rw[GCD_REF] >> 1951 `_ = IMAGE (gcd n) (n INSERT (natural n))` by rw[] >> 1952 metis_tac[natural_has_last, ABSORPTION]); 1953 1954(* Theorem: 0 < n ==> (partition (feq (gcd n)) (natural n) = IMAGE (preimage (gcd n) (natural n)) (divisors n)) *) 1955(* Proof: 1956 Let f = gcd n, s = natural n. 1957 partition (feq f) s 1958 = IMAGE (preimage f s o f) s by feq_partition_by_preimage 1959 = IMAGE (preimage f s) (IMAGE f s) by IMAGE_COMPOSE 1960 = IMAGE (preimage f s) (IMAGE (gcd n) (natural n)) by expansion 1961 = IMAGE (preimage f s) (divisors n) by divisors_eq_image_gcd_natural, 0 < n 1962*) 1963val gcd_eq_natural_partition_by_divisors = store_thm( 1964 "gcd_eq_natural_partition_by_divisors", 1965 ``!n. 0 < n ==> (partition (feq (gcd n)) (natural n) = IMAGE (preimage (gcd n) (natural n)) (divisors n))``, 1966 rpt strip_tac >> 1967 qabbrev_tac `f = gcd n` >> 1968 qabbrev_tac `s = natural n` >> 1969 `partition (feq f) s = IMAGE (preimage f s o f) s` by rw[feq_partition_by_preimage] >> 1970 `_ = IMAGE (preimage f s) (IMAGE f s)` by rw[IMAGE_COMPOSE] >> 1971 rw[divisors_eq_image_gcd_natural, Abbr`f`, Abbr`s`]); 1972 1973(* Theorem: 0 < n ==> (SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n))) *) 1974(* Proof: 1975 SIGMA f (natural n) 1976 = SIGMA (SIGMA f) (partition (feq (gcd n)) (natural n)) by sum_over_natural_by_gcd_partition 1977 = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n)) by gcd_eq_natural_partition_by_divisors 1978*) 1979val sum_over_natural_by_preimage_divisors = store_thm( 1980 "sum_over_natural_by_preimage_divisors", 1981 ``!f n. 0 < n ==> (SIGMA f (natural n) = SIGMA (SIGMA f) (IMAGE (preimage (gcd n) (natural n)) (divisors n)))``, 1982 rw[sum_over_natural_by_gcd_partition, gcd_eq_natural_partition_by_divisors]); 1983 1984(* Theorem: (f 1 = g 1) /\ (!n. SIGMA f (divisors n) = SIGMA g (divisors n)) ==> (f = g) *) 1985(* Proof: 1986 By FUN_EQ_THM, this is to show: !x. f x = g x. 1987 By complete induction on x. 1988 Let s = divisors x, t = s DELETE x. 1989 Then x IN s by divisors_has_last 1990 and (s = x INSERT t) /\ x NOTIN t by INSERT_DELETE, IN_DELETE 1991 Note FINITE s by divisors_finite 1992 so FINITE t by FINITE_DELETE 1993 1994 Claim: SIGMA f t = SIGMA g t 1995 Proof: By SUM_IMAGE_CONG, this is to show: 1996 !z. z IN t ==> (f z = g z) 1997 But z IN s <=> z <= x /\ z divides x by divisors_element 1998 so z IN t <=> z < x /\ z divides x by IN_DELETE 1999 ==> f z = g z by induction hypothesis 2000 2001 Now SIGMA f s = SIGMA g s by implication 2002 or f x + SIGMA f t = g x + SIGMA g t by SUM_IMAGE_INSERT 2003 or f x = g x by SIGMA f t = SIGMA g t 2004*) 2005Theorem sum_image_divisors_cong: 2006 !f g. f 1 = g 1 /\ (!n. SIGMA f (divisors n) = SIGMA g (divisors n)) ==> 2007 f = g 2008Proof 2009 rw[FUN_EQ_THM] >> 2010 completeInduct_on `x` >> 2011 qabbrev_tac `s = divisors x` >> 2012 qabbrev_tac `t = s DELETE x` >> 2013 `x IN s` by rw[divisors_has_last, Abbr`s`] >> 2014 `(s = x INSERT t) /\ x NOTIN t` by rw[Abbr`t`] >> 2015 `SIGMA f t = SIGMA g t` 2016 by (irule SUM_IMAGE_CONG >> simp[] >> 2017 rw[divisors_element, Abbr`t`, Abbr`s`]) >> 2018 `FINITE t` by rw[divisors_finite, Abbr`t`, Abbr`s`] >> 2019 `SIGMA f s = f x + SIGMA f t` by simp[SUM_IMAGE_INSERT] >> 2020 `SIGMA g s = g x + SIGMA g t` by simp[SUM_IMAGE_INSERT] >> 2021 `SIGMA f s = SIGMA g s` by metis_tac[] >> 2022 decide_tac 2023QED 2024(* But this is not very useful! *) 2025 2026(* ------------------------------------------------------------------------- *) 2027 2028(* export theory at end *) 2029val _ = export_theory(); 2030 2031(*===========================================================================*) 2032