1(* ------------------------------------------------------------------------- *) 2(* Helper Theorems - a collection of useful results -- for Functions. *) 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 "helperFunction"; 12 13(* ------------------------------------------------------------------------- *) 14 15 16(* val _ = load "jcLib"; *) 17open jcLib; 18 19(* val _ = load "helperListTheory"; *) 20open helperNumTheory helperListTheory; 21 22(* val _ = load "helperSetTheory"; *) 23open helperSetTheory; 24 25(* open dependent theories *) 26open pred_setTheory arithmeticTheory; 27open dividesTheory gcdTheory; 28 29 30(* ------------------------------------------------------------------------- *) 31(* Helper Function Documentation *) 32(* ------------------------------------------------------------------------- *) 33(* Overloading: 34 x == y (f) = fequiv x y f 35 RISING f = !x:num. x <= f x 36 FALLING f = !x:num. f x <= x 37 SQRT n = ROOT 2 n 38 LOG2 n = LOG 2 n 39 coprime x y = gcd x y = 1 40 PAIRWISE_COPRIME s = !x y. x IN s /\ y IN s /\ x <> y ==> coprime x y 41 tops b n = b ** n - 1 42 nines n = tops 10 n 43*) 44(* Definitions and Theorems (# are exported): 45 46 Function Equivalence as Relation: 47 fequiv_def |- !x y f. fequiv x y f <=> (f x = f y) 48# fequiv_refl |- !f x. (x == x) f 49 fequiv_sym |- !f x y. (x == y) f ==> (y == x) f 50 fequiv_trans |- !f x y z. (x == y) f /\ (y == z) f ==> (x == z) f 51 fequiv_equiv_class |- !f. (\x y. (x == y) f) equiv_on univ(:'a) 52 53 Function-based Equivalence: 54 feq_def |- !f x y. feq f x y <=> (f x = f y) 55 feq_class_def |- !s f n. feq_class f s n = {x | x IN s /\ (f x = n)} 56 feq_class_element |- !f s n x. x IN feq_class f s n <=> x IN s /\ (f x = n) 57 feq_class_property |- !f s x. feq_class f s (f x) = {y | y IN s /\ feq f x y} 58 feq_class_fun |- !f s. feq_class f s o f = (\x. {y | y IN s /\ feq f x y}) 59 60 61 feq_equiv |- !s f. feq f equiv_on s 62 feq_partition |- !s f. partition (feq f) s = IMAGE (feq_class f s o f) s 63 feq_partition_element |- !s f t. t IN partition (feq f) s <=> 64 ?z. z IN s /\ !x. x IN t <=> x IN s /\ (f x = f z) 65 feq_class_eq_preimage |- !f s. feq_class f s = preimage f s 66 feq_partition_by_preimage |- !f s. partition (feq f) s = IMAGE (preimage f s o f) s 67 feq_sum_over_partition |- !s. FINITE s ==> !f g. SIGMA g s = SIGMA (SIGMA g) (partition (feq f) s) 68 69 finite_card_by_feq_partition |- !s. FINITE s ==> !f. CARD s = SIGMA CARD (partition (feq f) s) 70 finite_card_by_image_preimage |- !s. FINITE s ==> !f. CARD s = SIGMA CARD (IMAGE (preimage f s o f) s) 71 72 Function Iteration: 73 FUNPOW_2 |- !f x. FUNPOW f 2 x = f (f x) 74 FUNPOW_K |- !n x c. FUNPOW (K c) n x = if n = 0 then x else c 75 FUNPOW_MULTIPLE |- !f k e. 0 < k /\ (FUNPOW f k e = e) ==> !n. FUNPOW f (n * k) e = e 76 FUNPOW_MOD |- !f k e. 0 < k /\ (FUNPOW f k e = e) ==> !n. FUNPOW f n e = FUNPOW f (n MOD k) e 77 FUNPOW_COMM |- !f m n x. FUNPOW f m (FUNPOW f n x) = FUNPOW f n (FUNPOW f m x) 78 FUNPOW_LE_RISING |- !f m n. RISING f /\ m <= n ==> !x. FUNPOW f m x <= FUNPOW f n x 79 FUNPOW_LE_FALLING |- !f m n. FALLING f /\ m <= n ==> !x. FUNPOW f n x <= FUNPOW f m x 80 FUNPOW_LE_MONO |- !f g. (!x. f x <= g x) /\ MONO g ==> !n x. FUNPOW f n x <= FUNPOW g n x 81 FUNPOW_GE_MONO |- !f g. (!x. f x <= g x) /\ MONO f ==> !n x. FUNPOW f n x <= FUNPOW g n x 82 FUNPOW_SQ |- !m n. FUNPOW (\n. SQ n) n m = m ** 2 ** n 83 FUNPOW_SQ_MOD |- !m n k. 0 < m /\ 0 < n ==> (FUNPOW (\n. SQ n MOD m) n k = k ** 2 ** n MOD m) 84 FUNPOW_ADD1 |- !m n. FUNPOW SUC n m = m + n 85 FUNPOW_SUB1 |- !m n. FUNPOW PRE n m = m - n 86 FUNPOW_MUL |- !b m n. FUNPOW ($* b) n m = m * b ** n 87 FUNPOW_DIV |- !b m n. 0 < b ==> FUNPOW (combin$C $DIV b) n m = m DIV b ** n 88 FUNPOW_MAX |- !m n k. 0 < n ==> (FUNPOW (\x. MAX x m) n k = MAX k m) 89 FUNPOW_MIN |- !m n k. 0 < n ==> (FUNPOW (\x. MIN x m) n k = MIN k m) 90 FUNPOW_PAIR |- !f g n x y. FUNPOW (\(x,y). (f x,g y)) n (x,y) = (FUNPOW f n x,FUNPOW g n y) 91 FUNPOW_TRIPLE |- !f g h n x y z. FUNPOW (\(x,y,z). (f x,g y,h z)) n (x,y,z) = 92 (FUNPOW f n x,FUNPOW g n y,FUNPOW h n z) 93 FUNPOW_closure |- !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW f n x IN s 94 95 Factorial: 96 FACT_0 |- FACT 0 = 1 97 FACT_1 |- FACT 1 = 1 98 FACT_2 |- FACT 2 = 2 99 FACT_EQ_1 |- !n. (FACT n = 1) <=> n <= 1 100 FACT_GE_1 |- !n. 1 <= FACT n 101 FACT_EQ_SELF |- !n. (FACT n = n) <=> (n = 1) \/ (n = 2) 102 FACT_GE_SELF |- !n. 0 < n ==> n <= FACT n 103 FACT_DIV |- !n. 0 < n ==> (FACT (n - 1) = FACT n DIV n) 104 FACT_EQ_PROD |- !n. FACT n = PROD_SET (IMAGE SUC (count n)) 105 FACT_REDUCTION |- !n m. m < n ==> (FACT n = PROD_SET (IMAGE SUC ((count n) DIFF (count m))) * (FACT m)) 106 PRIME_BIG_NOT_DIVIDES_FACT |- !p k. prime p /\ k < p ==> ~(p divides (FACT k)) 107 108 Basic GCD, LCM Theorems: 109 GCD_COMM |- !a b. gcd a b = gcd b a 110 LCM_SYM |- !a b. lcm a b = lcm b a 111 GCD_0 |- !x. (gcd 0 x = x) /\ (gcd x 0 = x) 112 GCD_DIVIDES |- !m n. 0 < n /\ 0 < m ==> 0 < gcd n m /\ (n MOD gcd n m = 0) /\ (m MOD gcd n m = 0) 113 GCD_GCD |- !m n. gcd n (gcd n m) = gcd n m 114 GCD_LCM |- !m n. gcd m n * lcm m n = m * n 115 LCM_DIVISORS |- !m n. m divides lcm m n /\ n divides lcm m n 116 LCM_IS_LCM |- !m n p. m divides p /\ n divides p ==> lcm m n divides p 117 LCM_EQ_0 |- !m n. (lcm m n = 0) <=> (m = 0) \/ (n = 0) 118 LCM_REF |- !a. lcm a a = a 119 LCM_DIVIDES |- !n a b. a divides n /\ b divides n ==> lcm a b divides n 120 GCD_POS |- !m n. 0 < m \/ 0 < n ==> 0 < gcd m n 121 LCM_POS |- !m n. 0 < m /\ 0 < n ==> 0 < lcm m n 122 divides_iff_gcd_fix |- !m n. n divides m <=> (gcd n m = n) 123 divides_iff_lcm_fix |- !m n. n divides m <=> (lcm n m = m) 124 FACTOR_OUT_PRIME |- !n p. 0 < n /\ prime p /\ p divides n ==> 125 ?m. 0 < m /\ (p ** m) divides n /\ !k. coprime (p ** k) (n DIV p ** m) 126 127 Consequences of Coprime: 128 MOD_NONZERO_WHEN_GCD_ONE |- !n. 1 < n ==> !x. coprime n x ==> 0 < x /\ 0 < x MOD n 129 PRODUCT_WITH_GCD_ONE |- !n x y. coprime n x /\ coprime n y ==> coprime n (x * y) 130 MOD_WITH_GCD_ONE |- !n x. 0 < n /\ coprime n x ==> coprime n (x MOD n) 131 GCD_ONE_PROPERTY |- !n x. 1 < n /\ coprime n x ==> ?k. ((k * x) MOD n = 1) /\ coprime n k 132 GCD_MOD_MULT_INV |- !n x. 1 < n /\ 0 < x /\ x < n /\ coprime n x ==> 133 ?y. 0 < y /\ y < n /\ coprime n y /\ ((y * x) MOD n = 1) 134 GEN_MULT_INV_DEF |- !n x. 1 < n /\ 0 < x /\ x < n /\ coprime n x ==> 135 0 < GCD_MOD_MUL_INV n x /\ GCD_MOD_MUL_INV n x < n /\ 136 coprime n (GCD_MOD_MUL_INV n x) /\ 137 ((GCD_MOD_MUL_INV n x * x) MOD n = 1) 138 139 More GCD and LCM Theorems: 140 GCD_PROPERTY |- !a b c. (c = gcd a b) <=> c divides a /\ c divides b /\ 141 !x. x divides a /\ x divides b ==> x divides c 142 GCD_ASSOC |- !a b c. gcd a (gcd b c) = gcd (gcd a b) c 143 GCD_ASSOC_COMM |- !a b c. gcd a (gcd b c) = gcd b (gcd a c) 144 LCM_PROPERTY |- !a b c. (c = lcm a b) <=> a divides c /\ b divides c /\ 145 !x. a divides x /\ b divides x ==> c divides x 146 LCM_ASSOC |- !a b c. lcm a (lcm b c) = lcm (lcm a b) 147 LCM_ASSOC_COMM |- !a b c. lcm a (lcm b c) = lcm b (lcm a c) 148 GCD_SUB_L |- !a b. b <= a ==> (gcd (a - b) b = gcd a b) 149 GCD_SUB_R |- !a b. a <= b ==> (gcd a (b - a) = gcd a b) 150 LCM_EXCHANGE |- !a b c. (a * b = c * (a - b)) ==> (lcm a b = lcm a c) 151 LCM_COPRIME |- !m n. coprime m n ==> (lcm m n = m * n) 152 LCM_COMMON_FACTOR |- !m n k. lcm (k * m) (k * n) = k * lcm m n 153 LCM_COMMON_COPRIME |- !a b. coprime a b ==> !c. lcm (a * c) (b * c) = a * b * c 154 GCD_MULTIPLE |- !m n. 0 < n /\ (m MOD n = 0) ==> (gcd m n = n) 155 GCD_MULTIPLE_ALT |- !m n. gcd (m * n) n = n 156 GCD_SUB_MULTIPLE |- !a b k. k * a <= b ==> (gcd a b = gcd a (b - k * a)) 157 GCD_SUB_MULTIPLE_COMM 158 |- !a b k. k * a <= b ==> (gcd b a = gcd a (b - k * a)) 159 GCD_MOD |- !m n. 0 < m ==> (gcd m n = gcd m (n MOD m)) 160 GCD_MOD_COMM |- !m n. 0 < m ==> (gcd n m = gcd (n MOD m) m) 161 GCD_EUCLID |- !a b c. gcd a (b * a + c) = gcd a c 162 GCD_REDUCE |- !a b c. gcd (b * a + c) a = gcd a c 163 164 Coprime Theorems: 165 coprime_SUC |- !n. coprime n (n + 1) 166 coprime_PRE |- !n. 0 < n ==> coprime (n - 1) n 167 coprime_0L |- !n. coprime 0 n <=> (n = 1) 168 coprime_0R |- !n. coprime n 0 <=> (n = 1) 169 coprime_sym |- !x y. coprime x y <=> coprime y x 170 coprime_neq_1 |- !n k. coprime k n /\ n <> 1 ==> k <> 0 171 coprime_gt_1 |- !n k. coprime k n /\ 1 < n ==> 0 < k 172 coprime_exp |- !c m. coprime c m ==> !n. coprime (c ** n) m 173 coprime_exp_comm |- !a b. coprime a b ==> !n. coprime a (b ** n) 174 coprime_iff_coprime_exp |- !n. 0 < n ==> !a b. coprime a b <=> coprime a (b ** n) 175 coprime_product_coprime |- !x y z. coprime x z /\ coprime y z ==> coprime (x * y) z 176 coprime_product_coprime_sym |- !x y z. coprime z x /\ coprime z y ==> coprime z (x * y) 177 coprime_product_coprime_iff |- !x y z. coprime x z ==> (coprime y z <=> coprime (x * y) z) 178 coprime_product_divides |- !n a b. a divides n /\ b divides n /\ coprime a b ==> a * b divides n 179 coprime_mod |- !m n. 0 < m /\ coprime m n ==> coprime m (n MOD m) 180 coprime_mod_iff |- !m n. 0 < m ==> (coprime m n <=> coprime m (n MOD m)) 181 coprime_not_divides |- !m n. 1 < n /\ coprime n m ==> ~(n divides m) 182 coprime_factor_not_divides |- !n k. 1 < n /\ coprime n k ==> 183 !p. 1 < p /\ p divides n ==> ~(p divides k) 184 coprime_factor_coprime |- !m n. m divides n ==> !k. coprime n k ==> coprime m k 185 prime_not_divides_is_coprime |- !n p. prime p /\ ~(p divides n) ==> coprime p n 186 prime_not_coprime_divides |- !n p. prime p /\ ~(coprime p n) ==> p divides n 187 coprime_prime_factor_coprime |- !n p. 1 < n /\ prime p /\ p divides n ==> 188 !k. coprime n k ==> coprime p k 189 coprime_all_le_imp_lt |- !n. 1 < n ==> !m. (!j. 0 < j /\ j <= m ==> coprime n j) ==> m < n 190 coprime_condition |- !m n. (!j. 1 < j /\ j <= m ==> ~(j divides n)) <=> 191 !j. 1 < j /\ j <= m ==> coprime j n 192 coprime_by_le_not_divides |- !m n. 1 < m /\ (!j. 1 < j /\ j <= m ==> ~(j divides n)) ==> coprime m n 193 prime_coprime_all_lt |- !n. prime n ==> !m. 0 < m /\ m < n ==> coprime n m 194 prime_coprime_all_less |- !m n. prime n /\ m < n ==> !j. 0 < j /\ j <= m ==> coprime n j 195 prime_iff_coprime_all_lt |- !n. prime n <=> 1 < n /\ !j. 0 < j /\ j < n ==> coprime n j 196 prime_iff_no_proper_factor|- !n. prime n <=> 1 < n /\ !j. 1 < j /\ j < n ==> ~(j divides n) 197 prime_always_bigger |- !n. ?p. prime p /\ n < p 198 divides_imp_coprime_with_successor |- !m n. n divides m ==> coprime n (SUC m) 199 divides_imp_coprime_with_predecessor |- !m n. 0 < m /\ n divides m ==> coprime n (PRE m) 200 gcd_coprime_cancel |- !m n p. coprime p n ==> (gcd (p * m) n = gcd m n) 201 primes_coprime |- !p q. prime p /\ prime q /\ p <> q ==> coprime p q 202 every_coprime_prod_set_coprime |- !s. FINITE s ==> 203 !x. x NOTIN s /\ (!z. z IN s ==> coprime x z) ==> coprime x (PROD_SET s) 204 205 Pairwise Coprime Property: 206 pairwise_coprime_insert |- !s e. e NOTIN s /\ PAIRWISE_COPRIME (e INSERT s) ==> 207 (!x. x IN s ==> coprime e x) /\ PAIRWISE_COPRIME s 208 pairwise_coprime_prod_set_subset_divides 209 |- !s. FINITE s /\ PAIRWISE_COPRIME s ==> 210 !t. t SUBSET s ==> PROD_SET t divides PROD_SET s 211 pairwise_coprime_partition_coprime |- !s. FINITE s /\ PAIRWISE_COPRIME s ==> 212 !u v. (s = u UNION v) /\ DISJOINT u v ==> coprime (PROD_SET u) (PROD_SET v) 213 pairwise_coprime_prod_set_partition |- !s. FINITE s /\ PAIRWISE_COPRIME s ==> 214 !u v. (s = u UNION v) /\ DISJOINT u v ==> 215 (PROD_SET s = PROD_SET u * PROD_SET v) /\ coprime (PROD_SET u) (PROD_SET v) 216 217 GCD divisibility condition of Power Predecessors: 218 power_predecessor_division_eqn |- !t m n. 0 < t /\ m <= n ==> 219 tops t n = t ** (n - m) * tops t m + tops t (n - m) 220 power_predecessor_division_alt |- !t m n. 0 < t /\ m <= n ==> 221 tops t n - t ** (n - m) * tops t m = tops t (n - m) 222 power_predecessor_gcd_reduction |- !t n m. m <= n ==> 223 (gcd (tops t n) (tops t m) = gcd (tops t m) (tops t (n - m))) 224 power_predecessor_gcd_identity |- !t n m. gcd (tops t n) (tops t m) = tops t (gcd n m) 225 power_predecessor_divisibility |- !t n m. 1 < t ==> (tops t n divides tops t m <=> n divides m) 226 power_predecessor_divisor |- !t n. t - 1 divides tops t n 227 228 nines_division_eqn |- !m n. m <= n ==> nines n = 10 ** (n - m) * nines m + nines (n - m): thm 229 nines_division_alt |- !m n. m <= n ==> nines n - 10 ** (n - m) * nines m = nines (n - m): thm 230 nines_gcd_reduction |- !n m. m <= n ==> gcd (nines n) (nines m) = gcd (nines m) (nines (n - m)): thm 231 nines_gcd_identity |- !n m. gcd (nines n) (nines m) = nines (gcd n m): thm 232 nines_divisibility |- !n m. nines n divides nines m <=> n divides m: thm 233 nines_divisor |- !n. 9 divides nines n: thm 234 235 GCD involving Powers: 236 prime_divides_prime_power |- !m n k. prime m /\ prime n /\ m divides n ** k ==> (m = n) 237 prime_power_factor |- !n p. 0 < n /\ prime p ==> ?q m. (n = p ** m * q) /\ coprime p q 238 prime_power_divisor |- !p n a. prime p /\ a divides p ** n ==> ?j. j <= n /\ (a = p ** j) 239 prime_powers_eq |- !p q. prime p /\ prime q ==> !m n. 0 < m /\ (p ** m = q ** n) ==> (p = q) /\ (m = n) 240 prime_powers_coprime |- !p q. prime p /\ prime q /\ p <> q ==> !m n. coprime (p ** m) (q ** n) 241 prime_powers_divide |- !p q. prime p /\ prime q ==> 242 !m n. 0 < m ==> (p ** m divides q ** n <=> (p = q) /\ m <= n) 243 gcd_powers |- !b m n. gcd (b ** m) (b ** n) = b ** MIN m n 244 lcm_powers |- !b m n. lcm (b ** m) (b ** n) = b ** MAX m n 245 coprime_power_and_power_predecessor |- !b m n. 0 < b /\ 0 < m ==> coprime (b ** n) (b ** m - 1) 246 coprime_power_and_power_successor |- !b m n. 0 < b /\ 0 < m ==> coprime (b ** n) (b ** m + 1) 247 248 Useful Theorems: 249 PRIME_EXP_FACTOR |- !p q n. prime p /\ q divides p ** n ==> (q = 1) \/ p divides q 250 FACT_MOD_PRIME |- !p n. prime p /\ n < p ==> FACT n MOD p <> 0: 251*) 252 253(* ------------------------------------------------------------------------- *) 254(* Function Equivalence as Relation *) 255(* ------------------------------------------------------------------------- *) 256 257(* For function f on a domain D, x, y in D are "equal" if f x = f y. *) 258val fequiv_def = Define` 259 fequiv x y f <=> (f x = f y) 260`; 261 262val _ = overload_on ("==", ``fequiv``); 263val _ = set_fixity "==" (Infix(NONASSOC, 450)); 264 265(* Theorem: [Reflexive] (x == x) f *) 266(* Proof: by definition, 267 and f x = f x. 268*) 269val fequiv_refl = store_thm( 270 "fequiv_refl", 271 ``!f x. (x == x) f``, 272 rw_tac std_ss[fequiv_def]); 273 274(* export simple definition *) 275val _ = export_rewrites ["fequiv_refl"]; 276 277(* Theorem: [Symmetric] (x == y) f ==> (y == x) f *) 278(* Proof: by defintion, 279 and f x = f y means the same as f y = f x. 280*) 281val fequiv_sym = store_thm( 282 "fequiv_sym", 283 ``!f x y. (x == y) f ==> (y == x) f``, 284 rw_tac std_ss[fequiv_def]); 285 286(* no export of commutativity *) 287 288(* Theorem: [Transitive] (x == y) f /\ (y == z) f ==> (x == z) f *) 289(* Proof: by defintion, 290 and f x = f y 291 and f y = f z 292 implies f x = f z. 293*) 294val fequiv_trans = store_thm( 295 "fequiv_trans", 296 ``!f x y z. (x == y) f /\ (y == z) f ==> (x == z) f``, 297 rw_tac std_ss[fequiv_def]); 298 299(* Theorem: fequiv (==) is an equivalence relation on the domain. *) 300(* Proof: by reflexive, symmetric and transitive. *) 301val fequiv_equiv_class = store_thm( 302 "fequiv_equiv_class", 303 ``!f. (\x y. (x == y) f) equiv_on univ(:'a)``, 304 rw_tac std_ss[equiv_on_def, fequiv_def, EQ_IMP_THM]); 305 306(* ------------------------------------------------------------------------- *) 307(* Function-based Equivalence *) 308(* ------------------------------------------------------------------------- *) 309 310(* Define an equivalence relation based on a function *) 311val feq_def = Define ` 312 feq f x y = (f x = f y) 313`; 314 315(* Define equivalence class based on a function *) 316val feq_class_def = Define ` 317 feq_class f s n = {x | x IN s /\ (f x = n)} 318`; 319 320(* Theorem: x IN feq_class f s n <=> x IN s /\ (f x = n) *) 321(* Proof: by feq_class_def *) 322val feq_class_element = store_thm( 323 "feq_class_element", 324 ``!f s n x. x IN feq_class f s n <=> x IN s /\ (f x = n)``, 325 rw[feq_class_def]); 326 327(* Note: 328 y IN equiv_class (feq f) s x 329<=> y IN s /\ (feq f x y) by equiv_class_element 330<=> y IN s /\ (f x = f y) by feq_def 331*) 332 333(* Theorem: feq_class f s (f x) = equiv_class (feq f) s x *) 334(* Proof: 335 feq_class f s (f x) 336 = {y | y IN s /\ (f y = f x)} by feq_class_def 337 = {y | y IN s /\ (f x = f y)} 338 = {y | y IN s /\ (feq f x y)} by feq_def 339 = equiv_class (feq f) s x by notation 340*) 341val feq_class_property = store_thm( 342 "feq_class_property", 343 ``!f s x. feq_class f s (f x) = equiv_class (feq f) s x``, 344 (rw[feq_class_def, feq_def, EXTENSION] >> metis_tac[])); 345 346(* Theorem: (feq_class f s) o f = equiv_class (feq f) s *) 347(* Proof: by FUN_EQ_THM, feq_class_property *) 348val feq_class_fun = store_thm( 349 "feq_class_fun", 350 ``!f s. (feq_class f s) o f = equiv_class (feq f) s``, 351 rw[FUN_EQ_THM, feq_class_property]); 352 353(* Theorem: feq f equiv_on s *) 354(* Proof: by equiv_on_def, feq_def *) 355val feq_equiv = store_thm( 356 "feq_equiv", 357 ``!s f. feq f equiv_on s``, 358 rw[equiv_on_def, feq_def] >> 359 metis_tac[]); 360 361(* Theorem: partition (feq f) s = IMAGE ((feq_class f s) o f) s *) 362(* Proof: 363 Use partition_def |> ISPEC ``feq f`` |> ISPEC ``(s:'a -> bool)``; 364 365 partition (feq f) s 366 = {t | ?x. x IN s /\ (t = {y | y IN s /\ feq f x y})} by partition_def 367 = {t | ?x. x IN s /\ (t = {y | y IN s /\ (f x = f y)})} by feq_def 368 = {t | ?x. x IN s /\ (t = feq_class f s (f x))} by feq_class_def 369 = {feq_class f s (f x) | x | x IN s } by rewriting 370 = IMAGE (feq_class f s) (IMAGE f s) by IN_IMAGE 371 = IMAGE ((feq_class f s) o f) s by IMAGE_COMPOSE 372*) 373val feq_partition = store_thm( 374 "feq_partition", 375 ``!s f. partition (feq f) s = IMAGE ((feq_class f s) o f) s``, 376 (rw[partition_def, feq_def, feq_class_def, EXTENSION, EQ_IMP_THM] >> metis_tac[])); 377 378(* Theorem: t IN partition (feq f) s <=> ?z. z IN s /\ (!x. x IN t <=> x IN s /\ (f x = f z)) *) 379(* Proof: by feq_partition, feq_class_def, EXTENSION *) 380val feq_partition_element = store_thm( 381 "feq_partition_element", 382 ``!s f t. t IN partition (feq f) s <=> ?z. z IN s /\ (!x. x IN t <=> x IN s /\ (f x = f z))``, 383 (rw[feq_partition, feq_class_def, EXTENSION] >> metis_tac[])); 384 385(* Theorem: feq_class f s = preimage f s *) 386(* Proof: 387 feq_class f s n 388 = {x | x IN s /\ (f x = n)} by feq_class_def 389 = preimage f s n by preimage_def 390 Hence feq_class f s = preimage f s by FUN_EQ_THM 391*) 392val feq_class_eq_preimage = store_thm( 393 "feq_class_eq_preimage", 394 ``!f s. feq_class f s = preimage f s``, 395 rw[feq_class_def, preimage_def, FUN_EQ_THM]); 396 397(* Theorem: partition (feq f) s = IMAGE (preimage f s o f) s *) 398(* Proof: 399 x IN partition (feq f) s 400 <=> ?z. z IN s /\ !j. j IN x <=> j IN s /\ (f j = f z) by feq_partition_element 401 <=> ?z. z IN s /\ !j. j IN x <=> j IN (preimage f s (f z)) by preimage_element 402 <=> ?z. z IN s /\ (x = preimage f s (f z)) by EXTENSION 403 <=> ?z. z IN s /\ (x = (preimage f s o f) z) by composition (o_THM) 404 <=> x IN IMAGE (preimage f s o f) s by IN_IMAGE 405 Hence partition (feq f) s = IMAGE (preimage f s o f) s by EXTENSION 406 407 or, 408 partition (feq f) s 409 = IMAGE (feq_class f s o f) s by feq_partition 410 = IMAGE (preiamge f s o f) s by feq_class_eq_preimage 411*) 412val feq_partition_by_preimage = store_thm( 413 "feq_partition_by_preimage", 414 ``!f s. partition (feq f) s = IMAGE (preimage f s o f) s``, 415 rw[feq_partition, feq_class_eq_preimage]); 416 417(* Theorem: FINITE s ==> !f g. SIGMA g s = SIGMA (SIGMA g) (partition (feq f) s) *) 418(* Proof: 419 Since (feq f) equiv_on s by feq_equiv 420 Hence !g. SIGMA g s = SIGMA (SIGMA g) (partition (feq f) s) by set_sigma_by_partition 421*) 422val feq_sum_over_partition = store_thm( 423 "feq_sum_over_partition", 424 ``!s. FINITE s ==> !f g. SIGMA g s = SIGMA (SIGMA g) (partition (feq f) s)``, 425 rw[feq_equiv, set_sigma_by_partition]); 426 427(* Theorem: FINITE s ==> !f. CARD s = SIGMA CARD (partition (feq f) s) *) 428(* Proof: 429 Note feq equiv_on s by feq_equiv 430 The result follows by partition_CARD 431*) 432val finite_card_by_feq_partition = store_thm( 433 "finite_card_by_feq_partition", 434 ``!s. FINITE s ==> !f. CARD s = SIGMA CARD (partition (feq f) s)``, 435 rw[feq_equiv, partition_CARD]); 436 437(* Theorem: FINITE s ==> !f. CARD s = SIGMA CARD (IMAGE ((preimage f s) o f) s) *) 438(* Proof: 439 Note (feq f) equiv_on s by feq_equiv 440 CARD s 441 = SIGMA CARD (partition (feq f) s) by partition_CARD 442 = SIGMA CARD (IMAGE (preimage f s o f) s) by feq_partition_by_preimage 443*) 444val finite_card_by_image_preimage = store_thm( 445 "finite_card_by_image_preimage", 446 ``!s. FINITE s ==> !f. CARD s = SIGMA CARD (IMAGE ((preimage f s) o f) s)``, 447 rw[feq_equiv, partition_CARD, GSYM feq_partition_by_preimage]); 448 449(* ------------------------------------------------------------------------- *) 450(* Function Iteration *) 451(* ------------------------------------------------------------------------- *) 452 453(* Theorem: FUNPOW f 2 x = f (f x) *) 454(* Proof: by definition. *) 455val FUNPOW_2 = store_thm( 456 "FUNPOW_2", 457 ``!f x. FUNPOW f 2 x = f (f x)``, 458 simp_tac bool_ss [FUNPOW, TWO, ONE]); 459 460(* Theorem: FUNPOW (K c) n x = if n = 0 then x else c *) 461(* Proof: 462 By induction on n. 463 Base: !x c. FUNPOW (K c) 0 x = if 0 = 0 then x else c 464 FUNPOW (K c) 0 x 465 = x by FUNPOW 466 = if 0 = 0 then x else c by 0 = 0 is true 467 Step: !x c. FUNPOW (K c) n x = if n = 0 then x else c ==> 468 !x c. FUNPOW (K c) (SUC n) x = if SUC n = 0 then x else c 469 FUNPOW (K c) (SUC n) x 470 = FUNPOW (K c) n ((K c) x) by FUNPOW 471 = if n = 0 then ((K c) c) else c by induction hypothesis 472 = if n = 0 then c else c by K_THM 473 = c by either case 474 = if SUC n = 0 then x else c by SUC n = 0 is false 475*) 476val FUNPOW_K = store_thm( 477 "FUNPOW_K", 478 ``!n x c. FUNPOW (K c) n x = if n = 0 then x else c``, 479 Induct >- 480 rw[] >> 481 metis_tac[FUNPOW, combinTheory.K_THM, SUC_NOT_ZERO]); 482 483(* Theorem: 0 < k /\ FUNPOW f k e = e ==> !n. FUNPOW f (n*k) e = e *) 484(* Proof: 485 By induction on n: 486 Base case: FUNPOW f (0 * k) e = e 487 FUNPOW f (0 * k) e 488 = FUNPOW f 0 e by arithmetic 489 = e by FUNPOW_0 490 Step case: FUNPOW f (n * k) e = e ==> FUNPOW f (SUC n * k) e = e 491 FUNPOW f (SUC n * k) e 492 = FUNPOW f (k + n * k) e by arithmetic 493 = FUNPOW f k (FUNPOW (n * k) e) by FUNPOW_ADD. 494 = FUNPOW f k e by induction hypothesis 495 = e by given 496*) 497val FUNPOW_MULTIPLE = store_thm( 498 "FUNPOW_MULTIPLE", 499 ``!f k e. 0 < k /\ (FUNPOW f k e = e) ==> !n. FUNPOW f (n*k) e = e``, 500 rpt strip_tac >> 501 Induct_on `n` >- 502 rw[] >> 503 metis_tac[MULT_COMM, MULT_SUC, FUNPOW_ADD]); 504 505(* Theorem: 0 < k /\ FUNPOW f k e = e ==> !n. FUNPOW f n e = FUNPOW f (n MOD k) e *) 506(* Proof: 507 FUNPOW f n e 508 = FUNPOW f ((n DIV k) * k + (n MOD k)) e by division algorithm 509 = FUNPOW f ((n MOD k) + (n DIV k) * k) e by arithmetic 510 = FUNPOW f (n MOD k) (FUNPOW (n DIV k) * k e) by FUNPOW_ADD 511 = FUNPOW f (n MOD k) e by FUNPOW_MULTIPLE 512*) 513val FUNPOW_MOD = store_thm( 514 "FUNPOW_MOD", 515 ``!f k e. 0 < k /\ (FUNPOW f k e = e) ==> !n. FUNPOW f n e = FUNPOW f (n MOD k) e``, 516 rpt strip_tac >> 517 `n = (n MOD k) + (n DIV k) * k` by metis_tac[DIVISION, ADD_COMM] >> 518 metis_tac[FUNPOW_ADD, FUNPOW_MULTIPLE]); 519 520(* Theorem: FUNPOW f m (FUNPOW f n x) = FUNPOW f n (FUNPOW f m x) *) 521(* Proof: by FUNPOW_ADD, ADD_COMM *) 522Theorem FUNPOW_COMM: 523 !f m n x. FUNPOW f m (FUNPOW f n x) = FUNPOW f n (FUNPOW f m x) 524Proof 525 metis_tac[FUNPOW_ADD, ADD_COMM] 526QED 527 528(* Overload a RISING function *) 529val _ = overload_on ("RISING", ``\f. !x:num. x <= f x``); 530 531(* Overload a FALLING function *) 532val _ = overload_on ("FALLING", ``\f. !x:num. f x <= x``); 533 534(* Theorem: RISING f /\ m <= n ==> !x. FUNPOW f m x <= FUNPOW f n x *) 535(* Proof: 536 By induction on n. 537 Base: !m. m <= 0 ==> !x. FUNPOW f m x <= FUNPOW f 0 x 538 Note m = 0, and FUNPOW f 0 x <= FUNPOW f 0 x. 539 Step: !m. RISING f /\ m <= n ==> !x. FUNPOW f m x <= FUNPOW f n x ==> 540 !m. m <= SUC n ==> FUNPOW f m x <= FUNPOW f (SUC n) x 541 Note m <= n or m = SUC n. 542 If m = SUC n, this is trivial. 543 If m <= n, 544 FUNPOW f m x 545 <= FUNPOW f n x by induction hypothesis 546 <= f (FUNPOW f n x) by RISING f 547 = FUNPOW f (SUC n) x by FUNPOW_SUC 548*) 549val FUNPOW_LE_RISING = store_thm( 550 "FUNPOW_LE_RISING", 551 ``!f m n. RISING f /\ m <= n ==> !x. FUNPOW f m x <= FUNPOW f n x``, 552 strip_tac >> 553 Induct_on `n` >- 554 rw[] >> 555 rpt strip_tac >> 556 `(m <= n) \/ (m = SUC n)` by decide_tac >| [ 557 `FUNPOW f m x <= FUNPOW f n x` by rw[] >> 558 `FUNPOW f n x <= f (FUNPOW f n x)` by rw[] >> 559 `f (FUNPOW f n x) = FUNPOW f (SUC n) x` by rw[FUNPOW_SUC] >> 560 decide_tac, 561 rw[] 562 ]); 563 564(* Theorem: FALLING f /\ m <= n ==> !x. FUNPOW f n x <= FUNPOW f m x *) 565(* Proof: 566 By induction on n. 567 Base: !m. m <= 0 ==> !x. FUNPOW f 0 x <= FUNPOW f m x 568 Note m = 0, and FUNPOW f 0 x <= FUNPOW f 0 x. 569 Step: !m. FALLING f /\ m <= n ==> !x. FUNPOW f n x <= FUNPOW f m x ==> 570 !m. m <= SUC n ==> FUNPOW f (SUC n) x <= FUNPOW f m x 571 Note m <= n or m = SUC n. 572 If m = SUC n, this is trivial. 573 If m <= n, 574 FUNPOW f (SUC n) x 575 = f (FUNPOW f n x) by FUNPOW_SUC 576 <= FUNPOW f n x by FALLING f 577 <= FUNPOW f m x by induction hypothesis 578*) 579val FUNPOW_LE_FALLING = store_thm( 580 "FUNPOW_LE_FALLING", 581 ``!f m n. FALLING f /\ m <= n ==> !x. FUNPOW f n x <= FUNPOW f m x``, 582 strip_tac >> 583 Induct_on `n` >- 584 rw[] >> 585 rpt strip_tac >> 586 `(m <= n) \/ (m = SUC n)` by decide_tac >| [ 587 `FUNPOW f (SUC n) x = f (FUNPOW f n x)` by rw[FUNPOW_SUC] >> 588 `f (FUNPOW f n x) <= FUNPOW f n x` by rw[] >> 589 `FUNPOW f n x <= FUNPOW f m x` by rw[] >> 590 decide_tac, 591 rw[] 592 ]); 593 594(* Theorem: (!x. f x <= g x) /\ MONO g ==> !n x. FUNPOW f n x <= FUNPOW g n x *) 595(* Proof: 596 By induction on n. 597 Base: FUNPOW f 0 x <= FUNPOW g 0 x 598 FUNPOW f 0 x by FUNPOW_0 599 = x 600 <= x = FUNPOW g 0 x by FUNPOW_0 601 Step: FUNPOW f n x <= FUNPOW g n x ==> FUNPOW f (SUC n) x <= FUNPOW g (SUC n) x 602 FUNPOW f (SUC n) x 603 = f (FUNPOW f n x) by FUNPOW_SUC 604 <= g (FUNPOW f n x) by !x. f x <= g x 605 <= g (FUNPOW g n x) by induction hypothesis, MONO g 606 = FUNPOW g (SUC n) x by FUNPOW_SUC 607*) 608val FUNPOW_LE_MONO = store_thm( 609 "FUNPOW_LE_MONO", 610 ``!f g. (!x. f x <= g x) /\ MONO g ==> !n x. FUNPOW f n x <= FUNPOW g n x``, 611 rpt strip_tac >> 612 Induct_on `n` >- 613 rw[] >> 614 rw[FUNPOW_SUC] >> 615 `f (FUNPOW f n x) <= g (FUNPOW f n x)` by rw[] >> 616 `g (FUNPOW f n x) <= g (FUNPOW g n x)` by rw[] >> 617 decide_tac); 618 619(* Note: 620There is no FUNPOW_LE_RMONO. FUNPOW_LE_MONO says: 621|- !f g. (!x. f x <= g x) /\ MONO g ==> !n x. FUNPOW f n x <= FUNPOW g n x 622To compare the terms in these two sequences: 623 x, f x, f (f x), f (f (f x)), ...... 624 x, g x, g (g x), g (g (g x)), ...... 625For the first pair: x <= x. 626For the second pair: f x <= g x, as g is cover. 627For the third pair: f (f x) <= g (f x) by g is cover, 628 <= g (g x) by MONO g, and will not work if RMONO g. 629*) 630 631(* Theorem: (!x. f x <= g x) /\ MONO f ==> !n x. FUNPOW f n x <= FUNPOW g n x *) 632(* Proof: 633 By induction on n. 634 Base: FUNPOW f 0 x <= FUNPOW g 0 x 635 FUNPOW f 0 x by FUNPOW_0 636 = x 637 <= x = FUNPOW g 0 x by FUNPOW_0 638 Step: FUNPOW f n x <= FUNPOW g n x ==> FUNPOW f (SUC n) x <= FUNPOW g (SUC n) x 639 FUNPOW f (SUC n) x 640 = f (FUNPOW f n x) by FUNPOW_SUC 641 <= f (FUNPOW g n x) by induction hypothesis, MONO f 642 <= g (FUNPOW g n x) by !x. f x <= g x 643 = FUNPOW g (SUC n) x by FUNPOW_SUC 644*) 645val FUNPOW_GE_MONO = store_thm( 646 "FUNPOW_GE_MONO", 647 ``!f g. (!x. f x <= g x) /\ MONO f ==> !n x. FUNPOW f n x <= FUNPOW g n x``, 648 rpt strip_tac >> 649 Induct_on `n` >- 650 rw[] >> 651 rw[FUNPOW_SUC] >> 652 `f (FUNPOW f n x) <= f (FUNPOW g n x)` by rw[] >> 653 `f (FUNPOW g n x) <= g (FUNPOW g n x)` by rw[] >> 654 decide_tac); 655 656(* Note: the name FUNPOW_SUC is taken: 657FUNPOW_SUC |- !f n x. FUNPOW f (SUC n) x = f (FUNPOW f n x) 658*) 659 660(* Theorem: FUNPOW SUC n m = m + n *) 661(* Proof: 662 By induction on n. 663 Base: !m. FUNPOW SUC 0 m = m + 0 664 LHS = FUNPOW SUC 0 m 665 = m by FUNPOW_0 666 = m + 0 = RHS by ADD_0 667 Step: !m. FUNPOW SUC n m = m + n ==> 668 !m. FUNPOW SUC (SUC n) m = m + SUC n 669 FUNPOW SUC (SUC n) m 670 = FUNPOW SUC n (SUC m) by FUNPOW 671 = (SUC m) + n by induction hypothesis 672 = m + SUC n by arithmetic 673*) 674val FUNPOW_ADD1 = store_thm( 675 "FUNPOW_ADD1", 676 ``!m n. FUNPOW SUC n m = m + n``, 677 Induct_on `n` >> 678 rw[FUNPOW]); 679 680(* Theorem: FUNPOW PRE n m = m - n *) 681(* Proof: 682 By induction on n. 683 Base: !m. FUNPOW PRE 0 m = m - 0 684 LHS = FUNPOW PRE 0 m 685 = m by FUNPOW_0 686 = m + 0 = RHS by ADD_0 687 Step: !m. FUNPOW PRE n m = m - n ==> 688 !m. FUNPOW PRE (SUC n) m = m - SUC n 689 FUNPOW PRE (SUC n) m 690 = FUNPOW PRE n (PRE m) by FUNPOW 691 = (PRE m) - n by induction hypothesis 692 = m - PRE n by arithmetic 693*) 694val FUNPOW_SUB1 = store_thm( 695 "FUNPOW_SUB1", 696 ``!m n. FUNPOW PRE n m = m - n``, 697 Induct_on `n` >- 698 rw[] >> 699 rw[FUNPOW]); 700 701(* Theorem: FUNPOW ($* b) n m = m * b ** n *) 702(* Proof: 703 By induction on n. 704 Base: !m. !m. FUNPOW ($* b) 0 m = m * b ** 0 705 LHS = FUNPOW ($* b) 0 m 706 = m by FUNPOW_0 707 = m * 1 by MULT_RIGHT_1 708 = m * b ** 0 = RHS by EXP_0 709 Step: !m. FUNPOW ($* b) n m = m * b ** n ==> 710 !m. FUNPOW ($* b) (SUC n) m = m * b ** SUC n 711 FUNPOW ($* b) (SUC n) m 712 = FUNPOW ($* b) n (b * m) by FUNPOW 713 = b * m * b ** n by induction hypothesis 714 = m * (b * b ** n) by arithmetic 715 = m * b ** SUC n by EXP 716*) 717val FUNPOW_MUL = store_thm( 718 "FUNPOW_MUL", 719 ``!b m n. FUNPOW ($* b) n m = m * b ** n``, 720 strip_tac >> 721 Induct_on `n` >- 722 rw[] >> 723 rw[FUNPOW, EXP]); 724 725(* Theorem: 0 < b ==> (FUNPOW (combin$C $DIV b) n m = m DIV (b ** n)) *) 726(* Proof: 727 By induction on n. 728 Let f = combin$C $DIV b. 729 Base: !m. FUNPOW f 0 m = m DIV b ** 0 730 LHS = FUNPOW f 0 m 731 = m by FUNPOW_0 732 = m DIV 1 by DIV_1 733 = m DIV (b ** 0) = RHS by EXP_0 734 Step: !m. FUNPOW f n m = m DIV b ** n ==> 735 !m. FUNPOW f (SUC n) m = m DIV b ** SUC n 736 FUNPOW f (SUC n) m 737 = FUNPOW f n (f m) by FUNPOW 738 = FUNPOW f n (m DIV b) by C_THM 739 = (m DIV b) DIV (b ** n) by induction hypothesis 740 = m DIV (b * b ** n) by DIV_DIV_DIV_MULT, 0 < b, 0 < b ** n 741 = m DIV b ** SUC n by EXP 742*) 743val FUNPOW_DIV = store_thm( 744 "FUNPOW_DIV", 745 ``!b m n. 0 < b ==> (FUNPOW (combin$C $DIV b) n m = m DIV (b ** n))``, 746 strip_tac >> 747 qabbrev_tac `f = combin$C $DIV b` >> 748 Induct_on `n` >- 749 rw[EXP_0] >> 750 rpt strip_tac >> 751 `FUNPOW f (SUC n) m = FUNPOW f n (m DIV b)` by rw[FUNPOW, Abbr`f`] >> 752 `_ = (m DIV b) DIV (b ** n)` by rw[] >> 753 `_ = m DIV (b * b ** n)` by rw[DIV_DIV_DIV_MULT] >> 754 `_ = m DIV b ** SUC n` by rw[EXP] >> 755 decide_tac); 756 757(* Theorem: FUNPOW SQ n m = m ** (2 ** n) *) 758(* Proof: 759 By induction on n. 760 Base: !m. FUNPOW (\n. SQ n) 0 m = m ** 2 ** 0 761 FUNPOW SQ 0 m 762 = m by FUNPOW_0 763 = m ** 1 by EXP_1 764 = m ** 2 ** 0 by EXP_0 765 Step: !m. FUNPOW (\n. SQ n) n m = m ** 2 ** n ==> 766 !m. FUNPOW (\n. SQ n) (SUC n) m = m ** 2 ** SUC n 767 FUNPOW (\n. SQ n) (SUC n) m 768 = SQ (FUNPOW (\n. SQ n) n m) by FUNPOW_SUC 769 = SQ (m ** 2 ** n) by induction hypothesis 770 = (m ** 2 ** n) ** 2 by EXP_2 771 = m ** (2 * 2 ** n) by EXP_EXP_MULT 772 = m ** 2 ** SUC n by EXP 773*) 774val FUNPOW_SQ = store_thm( 775 "FUNPOW_SQ", 776 ``!m n. FUNPOW SQ n m = m ** (2 ** n)``, 777 Induct_on `n` >- 778 rw[] >> 779 rw[FUNPOW_SUC, GSYM EXP_EXP_MULT, EXP]); 780 781(* Theorem: 0 < m /\ 0 < n ==> (FUNPOW (\n. (n * n) MOD m) n k = (k ** 2 ** n) MOD m) *) 782(* Proof: 783 Lef f = (\n. SQ n MOD m). 784 By induction on n. 785 Base: !k. 0 < m /\ 0 < 0 ==> FUNPOW f 0 k = k ** 2 ** 0 MOD m 786 True since 0 < 0 = F. 787 Step: !k. 0 < m /\ 0 < n ==> FUNPOW f n k = k ** 2 ** n MOD m ==> 788 !k. 0 < m /\ 0 < SUC n ==> FUNPOW f (SUC n) k = k ** 2 ** SUC n MOD m 789 If n = 1, 790 FUNPOW f (SUC 0) k 791 = FUNPOW f 1 k by ONE 792 = f k by FUNPOW_1 793 = SQ k MOD m by notation 794 = (k ** 2) MOD m by EXP_2 795 = (k ** (2 ** 1)) MOD m by EXP_1 796 If n <> 0, 797 FUNPOW f (SUC n) k 798 = f (FUNPOW f n k) by FUNPOW_SUC 799 = f (k ** 2 ** n MOD m) by induction hypothesis 800 = (k ** 2 ** n MOD m) * (k ** 2 ** n MOD m) MOD m by notation 801 = (k ** 2 ** n * k ** 2 ** n) MOD m by MOD_TIMES2 802 = (k ** (2 ** n + 2 ** n)) MOD m by EXP_BASE_MULT 803 = (k ** (2 * 2 ** n)) MOD m by arithmetic 804 = (k ** 2 ** SUC n) MOD m by EXP 805*) 806val FUNPOW_SQ_MOD = store_thm( 807 "FUNPOW_SQ_MOD", 808 ``!m n k. 0 < m /\ 0 < n ==> (FUNPOW (\n. (n * n) MOD m) n k = (k ** 2 ** n) MOD m)``, 809 strip_tac >> 810 qabbrev_tac `f = \n. SQ n MOD m` >> 811 Induct >> 812 simp[] >> 813 rpt strip_tac >> 814 Cases_on `n = 0` >- 815 simp[Abbr`f`] >> 816 rw[FUNPOW_SUC, Abbr`f`] >> 817 `(k ** 2 ** n) ** 2 = k ** (2 * 2 ** n)` by rw[GSYM EXP_EXP_MULT] >> 818 `_ = k ** 2 ** SUC n` by rw[EXP] >> 819 rw[]); 820 821(* Theorem: 0 < n ==> (FUNPOW (\x. MAX x m) n k = MAX k m) *) 822(* Proof: 823 By induction on n. 824 Base: !m k. 0 < 0 ==> FUNPOW (\x. MAX x m) 0 k = MAX k m 825 True by 0 < 0 = F. 826 Step: !m k. 0 < n ==> FUNPOW (\x. MAX x m) n k = MAX k m ==> 827 !m k. 0 < SUC n ==> FUNPOW (\x. MAX x m) (SUC n) k = MAX k m 828 If n = 0, 829 FUNPOW (\x. MAX x m) (SUC 0) k 830 = FUNPOW (\x. MAX x m) 1 k by ONE 831 = (\x. MAX x m) k by FUNPOW_1 832 = MAX k m by function application 833 If n <> 0, 834 FUNPOW (\x. MAX x m) (SUC n) k 835 = f (FUNPOW (\x. MAX x m) n k) by FUNPOW_SUC 836 = (\x. MAX x m) (MAX k m) by induction hypothesis 837 = MAX (MAX k m) m by function application 838 = MAX k m by MAX_IS_MAX, m <= MAX k m 839*) 840val FUNPOW_MAX = store_thm( 841 "FUNPOW_MAX", 842 ``!m n k. 0 < n ==> (FUNPOW (\x. MAX x m) n k = MAX k m)``, 843 Induct_on `n` >- 844 simp[] >> 845 rpt strip_tac >> 846 Cases_on `n = 0` >- 847 rw[] >> 848 rw[FUNPOW_SUC] >> 849 `m <= MAX k m` by rw[] >> 850 rw[MAX_DEF]); 851 852(* Theorem: 0 < n ==> (FUNPOW (\x. MIN x m) n k = MIN k m) *) 853(* Proof: 854 By induction on n. 855 Base: !m k. 0 < 0 ==> FUNPOW (\x. MIN x m) 0 k = MIN k m 856 True by 0 < 0 = F. 857 Step: !m k. 0 < n ==> FUNPOW (\x. MIN x m) n k = MIN k m ==> 858 !m k. 0 < SUC n ==> FUNPOW (\x. MIN x m) (SUC n) k = MIN k m 859 If n = 0, 860 FUNPOW (\x. MIN x m) (SUC 0) k 861 = FUNPOW (\x. MIN x m) 1 k by ONE 862 = (\x. MIN x m) k by FUNPOW_1 863 = MIN k m by function application 864 If n <> 0, 865 FUNPOW (\x. MIN x m) (SUC n) k 866 = f (FUNPOW (\x. MIN x m) n k) by FUNPOW_SUC 867 = (\x. MIN x m) (MIN k m) by induction hypothesis 868 = MIN (MIN k m) m by function application 869 = MIN k m by MIN_IS_MIN, MIN k m <= m 870*) 871val FUNPOW_MIN = store_thm( 872 "FUNPOW_MIN", 873 ``!m n k. 0 < n ==> (FUNPOW (\x. MIN x m) n k = MIN k m)``, 874 Induct_on `n` >- 875 simp[] >> 876 rpt strip_tac >> 877 Cases_on `n = 0` >- 878 rw[] >> 879 rw[FUNPOW_SUC] >> 880 `MIN k m <= m` by rw[] >> 881 rw[MIN_DEF]); 882 883(* Theorem: FUNPOW (\(x,y). (f x, g y)) n (x,y) = (FUNPOW f n x, FUNPOW g n y) *) 884(* Proof: 885 By induction on n. 886 Base: FUNPOW (\(x,y). (f x,g y)) 0 (x,y) = (FUNPOW f 0 x,FUNPOW g 0 y) 887 FUNPOW (\(x,y). (f x,g y)) 0 (x,y) 888 = (x,y) by FUNPOW_0 889 = (FUNPOW f 0 x, FUNPOW g 0 y) by FUNPOW_0 890 Step: FUNPOW (\(x,y). (f x,g y)) n (x,y) = (FUNPOW f n x,FUNPOW g n y) ==> 891 FUNPOW (\(x,y). (f x,g y)) (SUC n) (x,y) = (FUNPOW f (SUC n) x,FUNPOW g (SUC n) y) 892 FUNPOW (\(x,y). (f x,g y)) (SUC n) (x,y) 893 = (\(x,y). (f x,g y)) (FUNPOW (\(x,y). (f x,g y)) n (x,y)) by FUNPOW_SUC 894 = (\(x,y). (f x,g y)) (FUNPOW f n x,FUNPOW g n y) by induction hypothesis 895 = (f (FUNPOW f n x),g (FUNPOW g n y)) by function application 896 = (FUNPOW f (SUC n) x,FUNPOW g (SUC n) y) by FUNPOW_SUC 897*) 898val FUNPOW_PAIR = store_thm( 899 "FUNPOW_PAIR", 900 ``!f g n x y. FUNPOW (\(x,y). (f x, g y)) n (x,y) = (FUNPOW f n x, FUNPOW g n y)``, 901 rpt strip_tac >> 902 Induct_on `n` >> 903 rw[FUNPOW_SUC]); 904 905(* Theorem: FUNPOW (\(x,y,z). (f x, g y, h z)) n (x,y,z) = (FUNPOW f n x, FUNPOW g n y, FUNPOW h n z) *) 906(* Proof: 907 By induction on n. 908 Base: FUNPOW (\(x,y,z). (f x,g y,h z)) 0 (x,y,z) = (FUNPOW f 0 x,FUNPOW g 0 y,FUNPOW h 0 z) 909 FUNPOW (\(x,y,z). (f x,g y,h z)) 0 (x,y,z) 910 = (x,y) by FUNPOW_0 911 = (FUNPOW f 0 x, FUNPOW g 0 y, FUNPOW h 0 z) by FUNPOW_0 912 Step: FUNPOW (\(x,y,z). (f x,g y,h z)) n (x,y,z) = 913 (FUNPOW f n x,FUNPOW g n y,FUNPOW h n z) ==> 914 FUNPOW (\(x,y,z). (f x,g y,h z)) (SUC n) (x,y,z) = 915 (FUNPOW f (SUC n) x,FUNPOW g (SUC n) y,FUNPOW h (SUC n) z) 916 Let fun = (\(x,y,z). (f x,g y,h z)). 917 FUNPOW fun (SUC n) (x,y, z) 918 = fun (FUNPOW fun n (x,y,z)) by FUNPOW_SUC 919 = fun (FUNPOW f n x,FUNPOW g n y, FUNPOW h n z) by induction hypothesis 920 = (f (FUNPOW f n x),g (FUNPOW g n y), h (FUNPOW h n z)) by function application 921 = (FUNPOW f (SUC n) x,FUNPOW g (SUC n) y, FUNPOW h (SUC n) z) by FUNPOW_SUC 922*) 923val FUNPOW_TRIPLE = store_thm( 924 "FUNPOW_TRIPLE", 925 ``!f g h n x y z. FUNPOW (\(x,y,z). (f x, g y, h z)) n (x,y,z) = 926 (FUNPOW f n x, FUNPOW g n y, FUNPOW h n z)``, 927 rpt strip_tac >> 928 Induct_on `n` >> 929 rw[FUNPOW_SUC]); 930 931(* Theorem: f PERMUTES s /\ x IN s ==> FUNPOW f n x IN s *) 932(* Proof: 933 By induction on n. 934 Base: FUNPOW f 0 x IN s 935 Since FUNPOW f 0 x = x by FUNPOW_0 936 This is trivially true. 937 Step: FUNPOW f n x IN s ==> FUNPOW f (SUC n) x IN s 938 FUNPOW f (SUC n) x 939 = f (FUNPOW f n x) by FUNPOW_SUC 940 But FUNPOW f n x IN s by induction hypothesis 941 so f (FUNPOW f n x) IN s by BIJ_ELEMENT, f PERMUTES s 942*) 943Theorem FUNPOW_closure: 944 !f s x n. f PERMUTES s /\ x IN s ==> FUNPOW f n x IN s 945Proof 946 rpt strip_tac >> 947 Induct_on `n` >- 948 rw[] >> 949 metis_tac[FUNPOW_SUC, BIJ_ELEMENT] 950QED 951 952(* ------------------------------------------------------------------------- *) 953(* Integer Functions. *) 954(* ------------------------------------------------------------------------- *) 955 956(* ------------------------------------------------------------------------- *) 957(* Factorial *) 958(* ------------------------------------------------------------------------- *) 959 960(* Theorem: FACT 0 = 1 *) 961(* Proof: by FACT *) 962val FACT_0 = store_thm( 963 "FACT_0", 964 ``FACT 0 = 1``, 965 EVAL_TAC); 966 967(* Theorem: FACT 1 = 1 *) 968(* Proof: 969 FACT 1 970 = FACT (SUC 0) by ONE 971 = (SUC 0) * FACT 0 by FACT 972 = (SUC 0) * 1 by FACT 973 = 1 by ONE 974*) 975val FACT_1 = store_thm( 976 "FACT_1", 977 ``FACT 1 = 1``, 978 EVAL_TAC); 979 980(* Theorem: FACT 2 = 2 *) 981(* Proof: 982 FACT 2 983 = FACT (SUC 1) by TWO 984 = (SUC 1) * FACT 1 by FACT 985 = (SUC 1) * 1 by FACT_1 986 = 2 by TWO 987*) 988val FACT_2 = store_thm( 989 "FACT_2", 990 ``FACT 2 = 2``, 991 EVAL_TAC); 992 993(* Theorem: (FACT n = 1) <=> n <= 1 *) 994(* Proof: 995 If n = 0, 996 LHS = (FACT 0 = 1) = T by FACT_0 997 RHS = 0 <= 1 = T by arithmetic 998 If n <> 0, n = SUC m by num_CASES 999 LHS = FACT (SUC m) = 1 1000 <=> (SUC m) * FACT m = 1 by FACT 1001 <=> SUC m = 1 /\ FACT m = 1 by MULT_EQ_1 1002 <=> m = 0 /\ FACT m = 1 by m = PRE 1 = 0 1003 <=> m = 0 by FACT_0 1004 RHS = SUC m <= 1 1005 <=> ~(1 <= m) by NOT_LEQ 1006 <=> m < 1 by NOT_LESS_EQUAL 1007 <=> m = 0 by arithmetic 1008*) 1009val FACT_EQ_1 = store_thm( 1010 "FACT_EQ_1", 1011 ``!n. (FACT n = 1) <=> n <= 1``, 1012 rpt strip_tac >> 1013 Cases_on `n` >> 1014 rw[FACT_0] >> 1015 rw[FACT] >> 1016 `!m. SUC m <= 1 <=> (m = 0)` by decide_tac >> 1017 metis_tac[FACT_0]); 1018 1019(* Theorem: 1 <= FACT n *) 1020(* Proof: 1021 Note 0 < FACT n by FACT_LESS 1022 so 1 <= FACT n by arithmetic 1023*) 1024val FACT_GE_1 = store_thm( 1025 "FACT_GE_1", 1026 ``!n. 1 <= FACT n``, 1027 metis_tac[FACT_LESS, LESS_OR, ONE]); 1028 1029(* Theorem: (FACT n = n) <=> (n = 1) \/ (n = 2) *) 1030(* Proof: 1031 If part: (FACT n = n) ==> (n = 1) \/ (n = 2) 1032 Note n <> 0 by FACT_0: FACT 0 = 1 1033 ==> ?m. n = SUC m by num_CASES 1034 Thus SUC m * FACT m = SUC m by FACT 1035 = SUC m * 1 by MULT_RIGHT_1 1036 ==> FACT m = 1 by EQ_MULT_LCANCEL, SUC_NOT 1037 or m <= 1 by FACT_EQ_1 1038 Thus m = 0 or 1 by arithmetic 1039 or n = 1 or 2 by ONE, TWO 1040 1041 Only-if part: (FACT 1 = 1) /\ (FACT 2 = 2) 1042 Note FACT 1 = 1 by FACT_1 1043 and FACT 2 = 2 by FACT_2 1044*) 1045val FACT_EQ_SELF = store_thm( 1046 "FACT_EQ_SELF", 1047 ``!n. (FACT n = n) <=> (n = 1) \/ (n = 2)``, 1048 rw[EQ_IMP_THM] >| [ 1049 `n <> 0` by metis_tac[FACT_0, DECIDE``1 <> 0``] >> 1050 `?m. n = SUC m` by metis_tac[num_CASES] >> 1051 fs[FACT] >> 1052 `FACT m = 1` by metis_tac[MULT_LEFT_1, EQ_MULT_RCANCEL, SUC_NOT] >> 1053 `m <= 1` by rw[GSYM FACT_EQ_1] >> 1054 decide_tac, 1055 rw[FACT_1], 1056 rw[FACT_2] 1057 ]); 1058 1059(* Theorem: 0 < n ==> n <= FACT n *) 1060(* Proof: 1061 Note n <> 0 by 0 < n 1062 ==> ?m. n = SUC m by num_CASES 1063 Thus FACT n 1064 = FACT (SUC m) by n = SUC m 1065 = (SUC m) * FACT m by FACT_LESS: 0 < FACT m 1066 >= (SUC m) by LE_MULT_CANCEL_LBARE 1067 >= n by n = SUC m 1068*) 1069val FACT_GE_SELF = store_thm( 1070 "FACT_GE_SELF", 1071 ``!n. 0 < n ==> n <= FACT n``, 1072 rpt strip_tac >> 1073 `?m. n = SUC m` by metis_tac[num_CASES, NOT_ZERO_LT_ZERO] >> 1074 rw[FACT] >> 1075 rw[FACT_LESS]); 1076 1077(* Theorem: 0 < n ==> (FACT (n-1) = FACT n DIV n) *) 1078(* Proof: 1079 Since n = SUC(n-1) by SUC_PRE, 0 < n. 1080 and FACT n = n * FACT (n-1) by FACT 1081 = FACT (n-1) * n by MULT_COMM 1082 = FACT (n-1) * n + 0 by ADD_0 1083 Hence FACT (n-1) = FACT n DIV n by DIV_UNIQUE, 0 < n. 1084*) 1085val FACT_DIV = store_thm( 1086 "FACT_DIV", 1087 ``!n. 0 < n ==> (FACT (n-1) = FACT n DIV n)``, 1088 rpt strip_tac >> 1089 `n = SUC(n-1)` by decide_tac >> 1090 `FACT n = n * FACT (n-1)` by metis_tac[FACT] >> 1091 `_ = FACT (n-1) * n + 0` by rw[MULT_COMM] >> 1092 metis_tac[DIV_UNIQUE]); 1093 1094(* Theorem: n! = PROD_SET (count (n+1)) *) 1095(* Proof: by induction on n. 1096 Base case: FACT 0 = PROD_SET (IMAGE SUC (count 0)) 1097 LHS = FACT 0 1098 = 1 by FACT 1099 = PROD_SET {} by PROD_SET_THM 1100 = PROD_SET (IMAGE SUC {}) by IMAGE_EMPTY 1101 = PROD_SET (IMAGE SUC (count 0)) by COUNT_ZERO 1102 = RHS 1103 Step case: FACT n = PROD_SET (IMAGE SUC (count n)) ==> 1104 FACT (SUC n) = PROD_SET (IMAGE SUC (count (SUC n))) 1105 Note: (SUC n) NOTIN (IMAGE SUC (count n)) by IN_IMAGE, IN_COUNT [1] 1106 LHS = FACT (SUC n) 1107 = (SUC n) * (FACT n) by FACT 1108 = (SUC n) * (PROD_SET (IMAGE SUC (count n))) by induction hypothesis 1109 = (SUC n) * (PROD_SET (IMAGE SUC (count n)) DELETE (SUC n)) by DELETE_NON_ELEMENT, [1] 1110 = PROD_SET ((SUC n) INSERT ((IMAGE SUC (count n)) DELETE (SUC n))) by PROD_SET_THM 1111 = PROD_SET (IMAGE SUC (n INSERT (count n))) by IMAGE_INSERT 1112 = PROD_SET (IMAGE SUC (count (SUC n))) by COUNT_SUC 1113 = RHS 1114*) 1115val FACT_EQ_PROD = store_thm( 1116 "FACT_EQ_PROD", 1117 ``!n. FACT n = PROD_SET (IMAGE SUC (count n))``, 1118 Induct_on `n` >- 1119 rw[PROD_SET_THM, FACT] >> 1120 rw[PROD_SET_THM, FACT, COUNT_SUC] >> 1121 `(SUC n) NOTIN (IMAGE SUC (count n))` by rw[] >> 1122 metis_tac[DELETE_NON_ELEMENT]); 1123 1124(* Theorem: n!/m! = product of (m+1) to n. 1125 m < n ==> (FACT n = PROD_SET (IMAGE SUC ((count n) DIFF (count m))) * (FACT m)) *) 1126(* Proof: by factorial formula. 1127 By induction on n. 1128 Base case: m < 0 ==> ... 1129 True since m < 0 = F. 1130 Step case: !m. m < n ==> 1131 (FACT n = PROD_SET (IMAGE SUC (count n DIFF count m)) * FACT m) ==> 1132 !m. m < SUC n ==> 1133 (FACT (SUC n) = PROD_SET (IMAGE SUC (count (SUC n) DIFF count m)) * FACT m) 1134 Note that m < SUC n ==> m <= n. 1135 and FACT (SUC n) = (SUC n) * FACT n by FACT 1136 If m = n, 1137 PROD_SET (IMAGE SUC (count (SUC n) DIFF count n)) * FACT n 1138 = PROD_SET (IMAGE SUC {n}) * FACT n by IN_DIFF, IN_COUNT 1139 = PROD_SET {SUC n} * FACT n by IN_IMAGE 1140 = (SUC n) * FACT n by PROD_SET_THM 1141 If m < n, 1142 n NOTIN (count m) by IN_COUNT 1143 so n INSERT ((count n) DIFF (count m)) 1144 = (n INSERT (count n)) DIFF (count m) by INSERT_DIFF 1145 = count (SUC n) DIFF (count m) by EXTENSION 1146 Since (SUC n) NOTIN (IMAGE SUC ((count n) DIFF (count m))) by IN_IMAGE, IN_DIFF, IN_COUNT 1147 and FINITE (IMAGE SUC ((count n) DIFF (count m))) by IMAGE_FINITE, FINITE_DIFF, FINITE_COUNT 1148 Hence PROD_SET (IMAGE SUC (count (SUC n) DIFF count m)) * FACT m 1149 = ((SUC n) * PROD_SET (IMAGE SUC (count n DIFF count m))) * FACT m by PROD_SET_IMAGE_REDUCTION 1150 = (SUC n) * (PROD_SET (IMAGE SUC (count n DIFF count m))) * FACT m) by MULT_ASSOC 1151 = (SUC n) * FACT n by induction hypothesis 1152 = FACT (SUC n) by FACT 1153*) 1154val FACT_REDUCTION = store_thm( 1155 "FACT_REDUCTION", 1156 ``!n m. m < n ==> (FACT n = PROD_SET (IMAGE SUC ((count n) DIFF (count m))) * (FACT m))``, 1157 Induct_on `n` >- 1158 rw[] >> 1159 rw_tac std_ss[FACT] >> 1160 `m <= n` by decide_tac >> 1161 Cases_on `m = n` >| [ 1162 rw_tac std_ss[] >> 1163 `count (SUC m) DIFF count m = {m}` by 1164 (rw[DIFF_DEF] >> 1165 rw[EXTENSION, EQ_IMP_THM]) >> 1166 `PROD_SET (IMAGE SUC {m}) = SUC m` by rw[PROD_SET_THM] >> 1167 metis_tac[], 1168 `m < n` by decide_tac >> 1169 `n NOTIN (count m)` by srw_tac[ARITH_ss][] >> 1170 `n INSERT ((count n) DIFF (count m)) = (n INSERT (count n)) DIFF (count m)` by rw[] >> 1171 `_ = count (SUC n) DIFF (count m)` by srw_tac[ARITH_ss][EXTENSION] >> 1172 `(SUC n) NOTIN (IMAGE SUC ((count n) DIFF (count m)))` by rw[] >> 1173 `FINITE (IMAGE SUC ((count n) DIFF (count m)))` by rw[] >> 1174 metis_tac[PROD_SET_IMAGE_REDUCTION, MULT_ASSOC] 1175 ]); 1176 1177(* Theorem: prime p ==> p cannot divide k! for p > k. 1178 prime p /\ k < p ==> ~(p divides (FACT k)) *) 1179(* Proof: 1180 Since all terms of k! are less than p, and p has only 1 and p as factor. 1181 By contradiction, and induction on k. 1182 Base case: prime p ==> 0 < p ==> p divides (FACT 0) ==> F 1183 Since FACT 0 = 1 by FACT 1184 and p divides 1 <=> p = 1 by DIVIDES_ONE 1185 but prime p ==> 1 < p by ONE_LT_PRIME 1186 so this is a contradiction. 1187 Step case: prime p /\ k < p ==> p divides (FACT k) ==> F ==> 1188 SUC k < p ==> p divides (FACT (SUC k)) ==> F 1189 Since FACT (SUC k) = SUC k * FACT k by FACT 1190 and prime p /\ p divides (FACT (SUC k)) 1191 ==> p divides (SUC k), 1192 or p divides (FACT k) by P_EUCLIDES 1193 But SUC k < p, so ~(p divides (SUC k)) by NOT_LT_DIVIDES 1194 Hence p divides (FACT k) ==> F by induction hypothesis 1195*) 1196val PRIME_BIG_NOT_DIVIDES_FACT = store_thm( 1197 "PRIME_BIG_NOT_DIVIDES_FACT", 1198 ``!p k. prime p /\ k < p ==> ~(p divides (FACT k))``, 1199 (spose_not_then strip_assume_tac) >> 1200 Induct_on `k` >| [ 1201 rw[FACT] >> 1202 metis_tac[ONE_LT_PRIME, LESS_NOT_EQ], 1203 rw[FACT] >> 1204 (spose_not_then strip_assume_tac) >> 1205 `k < p /\ 0 < SUC k` by decide_tac >> 1206 metis_tac[P_EUCLIDES, NOT_LT_DIVIDES] 1207 ]); 1208 1209(* ------------------------------------------------------------------------- *) 1210(* Basic GCD, LCM Theorems *) 1211(* ------------------------------------------------------------------------- *) 1212 1213(* Note: gcd Theory has: GCD_SYM |- !a b. gcd a b = gcd b a 1214 but: LCM_COMM |- lcm a b = lcm b a 1215*) 1216val GCD_COMM = save_thm("GCD_COMM", GCD_SYM); 1217(* val GCD_COMM = |- !a b. gcd a b = gcd b a: thm *) 1218val LCM_SYM = save_thm("LCM_SYM", LCM_COMM |> GEN ``b:num`` |> GEN ``a:num``); 1219(* val val LCM_SYM = |- !a b. lcm a b = lcm b a: thm *) 1220 1221(* Note: 1222gcdTheory.LCM_0 |- (lcm 0 x = 0) /\ (lcm x 0 = 0) 1223gcdTheory.LCM_1 |- (lcm 1 x = x) /\ (lcm x 1 = x) 1224gcdTheory.GCD_1 |- coprime 1 x /\ coprime x 1 1225but only GCD_0L, GCD_0R 1226gcdTheory.GCD_EQ_0 |- !n m. (gcd n m = 0) <=> (n = 0) /\ (m = 0) 1227*) 1228 1229(* Theorem: (gcd 0 x = x) /\ (gcd x 0 = x) *) 1230(* Proof: by GCD_0L, GCD_0R *) 1231val GCD_0 = store_thm( 1232 "GCD_0", 1233 ``!x. (gcd 0 x = x) /\ (gcd x 0 = x)``, 1234 rw_tac std_ss[GCD_0L, GCD_0R]); 1235 1236(* Theorem: gcd(n, m) = 1 ==> n divides (c * m) ==> n divides c *) 1237(* Proof: 1238 This is L_EUCLIDES: (Euclid's Lemma) 1239> val it = |- !a b c. coprime a b /\ divides b (a * c) ==> b divides c : thm 1240*) 1241 1242(* Theorem: If 0 < n, 0 < m, let g = gcd n m, then 0 < g and n MOD g = 0 and m MOD g = 0 *) 1243(* Proof: 1244 0 < n ==> n <> 0, 0 < m ==> m <> 0, by NOT_ZERO_LT_ZERO 1245 hence g = gcd n m <> 0, or 0 < g. by GCD_EQ_0 1246 g = gcd n m ==> (g divides n) /\ (g divides m) by GCD_IS_GCD, is_gcd_def 1247 ==> (n MOD g = 0) /\ (m MOD g = 0) by DIVIDES_MOD_0 1248*) 1249val GCD_DIVIDES = store_thm( 1250 "GCD_DIVIDES", 1251 ``!m n. 0 < n /\ 0 < m ==> 0 < (gcd n m) /\ (n MOD (gcd n m) = 0) /\ (m MOD (gcd n m) = 0)``, 1252 ntac 3 strip_tac >> 1253 conj_asm1_tac >- 1254 metis_tac[GCD_EQ_0, NOT_ZERO_LT_ZERO] >> 1255 metis_tac[GCD_IS_GCD, is_gcd_def, DIVIDES_MOD_0]); 1256 1257(* Theorem: gcd n (gcd n m) = gcd n m *) 1258(* Proof: 1259 If n = 0, 1260 gcd 0 (gcd n m) = gcd n m by GCD_0L 1261 If m = 0, 1262 gcd n (gcd n 0) 1263 = gcd n n by GCD_0R 1264 = n = gcd n 0 by GCD_REF 1265 If n <> 0, m <> 0, d <> 0 by GCD_EQ_0 1266 Since d divides n, n MOD d = 0 1267 gcd n d 1268 = gcd d n by GCD_SYM 1269 = gcd (n MOD d) d by GCD_EFFICIENTLY, d <> 0 1270 = gcd 0 d by GCD_DIVIDES 1271 = d by GCD_0L 1272*) 1273val GCD_GCD = store_thm( 1274 "GCD_GCD", 1275 ``!m n. gcd n (gcd n m) = gcd n m``, 1276 rpt strip_tac >> 1277 Cases_on `n = 0` >- rw[] >> 1278 Cases_on `m = 0` >- rw[] >> 1279 `0 < n /\ 0 < m` by decide_tac >> 1280 metis_tac[GCD_SYM, GCD_EFFICIENTLY, GCD_DIVIDES, GCD_EQ_0, GCD_0L]); 1281 1282(* Theorem: GCD m n * LCM m n = m * n *) 1283(* Proof: 1284 By lcm_def: 1285 lcm m n = if (m = 0) \/ (n = 0) then 0 else m * n DIV gcd m n 1286 If m = 0, 1287 gcd 0 n * lcm 0 n = n * 0 = 0 = 0 * n, hence true. 1288 If n = 0, 1289 gcd m 0 * lcm m 0 = m * 0 = 0 = m * 0, hence true. 1290 If m <> 0, n <> 0, 1291 gcd m n * lcm m n = gcd m n * (m * n DIV gcd m n) = m * n. 1292*) 1293val GCD_LCM = store_thm( 1294 "GCD_LCM", 1295 ``!m n. gcd m n * lcm m n = m * n``, 1296 rw[lcm_def] >> 1297 `0 < m /\ 0 < n` by decide_tac >> 1298 `0 < gcd m n /\ (n MOD gcd m n = 0)` by rw[GCD_DIVIDES] >> 1299 qabbrev_tac `d = gcd m n` >> 1300 `m * n = (m * n) DIV d * d + (m * n) MOD d` by rw[DIVISION] >> 1301 `(m * n) MOD d = 0` by metis_tac[MOD_TIMES2, ZERO_MOD, MULT_0] >> 1302 metis_tac[ADD_0, MULT_COMM]); 1303 1304(* Theorem: m divides (lcm m n) /\ n divides (lcm m n) *) 1305(* Proof: by LCM_IS_LEAST_COMMON_MULTIPLE *) 1306val LCM_DIVISORS = store_thm( 1307 "LCM_DIVISORS", 1308 ``!m n. m divides (lcm m n) /\ n divides (lcm m n)``, 1309 rw[LCM_IS_LEAST_COMMON_MULTIPLE]); 1310 1311(* Theorem: m divides p /\ n divides p ==> (lcm m n) divides p *) 1312(* Proof: by LCM_IS_LEAST_COMMON_MULTIPLE *) 1313val LCM_IS_LCM = store_thm( 1314 "LCM_IS_LCM", 1315 ``!m n p. m divides p /\ n divides p ==> (lcm m n) divides p``, 1316 rw[LCM_IS_LEAST_COMMON_MULTIPLE]); 1317 1318(* Theorem: (lcm m n = 0) <=> ((m = 0) \/ (n = 0)) *) 1319(* Proof: 1320 If part: lcm m n = 0 ==> m = 0 \/ n = 0 1321 By contradiction, suppse m = 0 /\ n = 0. 1322 Then gcd m n = 0 by GCD_EQ_0 1323 and m * n = 0 by MULT_EQ_0 1324 but (gcd m n) * (lcm m n) = m * n by GCD_LCM 1325 so RHS <> 0, but LHS = 0 by MULT_0 1326 This is a contradiction. 1327 Only-if part: m = 0 \/ n = 0 ==> lcm m n = 0 1328 True by LCM_0 1329*) 1330val LCM_EQ_0 = store_thm( 1331 "LCM_EQ_0", 1332 ``!m n. (lcm m n = 0) <=> ((m = 0) \/ (n = 0))``, 1333 rw[EQ_IMP_THM] >| [ 1334 spose_not_then strip_assume_tac >> 1335 `(gcd m n) * (lcm m n) = m * n` by rw[GCD_LCM] >> 1336 `gcd m n <> 0` by rw[GCD_EQ_0] >> 1337 `m * n <> 0` by rw[MULT_EQ_0] >> 1338 metis_tac[MULT_0], 1339 rw[LCM_0], 1340 rw[LCM_0] 1341 ]); 1342 1343(* Note: gcdTheory.GCD_REF |- !a. gcd a a = a *) 1344 1345(* Theorem: lcm a a = a *) 1346(* Proof: 1347 If a = 0, 1348 lcm 0 0 = 0 by LCM_0 1349 If a <> 0, 1350 (gcd a a) * (lcm a a) = a * a by GCD_LCM 1351 a * (lcm a a) = a * a by GCD_REF 1352 lcm a a = a by MULT_LEFT_CANCEL, a <> 0 1353*) 1354val LCM_REF = store_thm( 1355 "LCM_REF", 1356 ``!a. lcm a a = a``, 1357 metis_tac[num_CASES, LCM_0, GCD_LCM, GCD_REF, MULT_LEFT_CANCEL]); 1358 1359(* Theorem: a divides n /\ b divides n ==> (lcm a b) divides n *) 1360(* Proof: same as LCM_IS_LCM *) 1361val LCM_DIVIDES = store_thm( 1362 "LCM_DIVIDES", 1363 ``!n a b. a divides n /\ b divides n ==> (lcm a b) divides n``, 1364 rw[LCM_IS_LCM]); 1365(* 1366> LCM_IS_LCM |> ISPEC ``a:num`` |> ISPEC ``b:num`` |> ISPEC ``n:num`` |> GEN_ALL; 1367val it = |- !n b a. a divides n /\ b divides n ==> lcm a b divides n: thm 1368*) 1369 1370(* Theorem: 0 < m \/ 0 < n ==> 0 < gcd m n *) 1371(* Proof: by GCD_EQ_0, NOT_ZERO_LT_ZERO *) 1372val GCD_POS = store_thm( 1373 "GCD_POS", 1374 ``!m n. 0 < m \/ 0 < n ==> 0 < gcd m n``, 1375 metis_tac[GCD_EQ_0, NOT_ZERO_LT_ZERO]); 1376 1377(* Theorem: 0 < m /\ 0 < n ==> 0 < lcm m n *) 1378(* Proof: by LCM_EQ_0, NOT_ZERO_LT_ZERO *) 1379val LCM_POS = store_thm( 1380 "LCM_POS", 1381 ``!m n. 0 < m /\ 0 < n ==> 0 < lcm m n``, 1382 metis_tac[LCM_EQ_0, NOT_ZERO_LT_ZERO]); 1383 1384(* Theorem: n divides m <=> gcd n m = n *) 1385(* Proof: 1386 If part: 1387 n divides m ==> ?k. m = k * n by divides_def 1388 gcd n m 1389 = gcd n (k * n) 1390 = gcd (n * 1) (n * k) by MULT_RIGHT_1, MULT_COMM 1391 = n * gcd 1 k by GCD_COMMON_FACTOR 1392 = n * 1 by GCD_1 1393 = n by MULT_RIGHT_1 1394 Only-if part: gcd n m = n ==> n divides m 1395 If n = 0, gcd 0 m = m by GCD_0L 1396 But gcd n m = n = 0 by givien 1397 hence m = 0, 1398 and 0 divides 0 is true by DIVIDES_REFL 1399 If n <> 0, 1400 If m = 0, LHS true by GCD_0R 1401 RHS true by ALL_DIVIDES_0 1402 If m <> 0, 1403 then 0 < n and 0 < m, 1404 gcd n m = gcd (m MOD n) n by GCD_EFFICIENTLY 1405 if (m MOD n) = 0 1406 then n divides m by DIVIDES_MOD_0 1407 If (m MOD n) <> 0, 1408 so (m MOD n) MOD (gcd n m) = 0 by GCD_DIVIDES 1409 or (m MOD n) MOD n = 0 by gcd n m = n, given 1410 or m MOD n = 0 by MOD_MOD 1411 contradicting (m MOD n) <> 0, hence true. 1412*) 1413val divides_iff_gcd_fix = store_thm( 1414 "divides_iff_gcd_fix", 1415 ``!m n. n divides m <=> (gcd n m = n)``, 1416 rw[EQ_IMP_THM] >| [ 1417 `?k. m = k * n` by rw[GSYM divides_def] >> 1418 `gcd n m = gcd (n * 1) (n * k)` by rw[MULT_COMM] >> 1419 rw[GCD_COMMON_FACTOR, GCD_1], 1420 Cases_on `n = 0` >- 1421 metis_tac[GCD_0L, DIVIDES_REFL] >> 1422 Cases_on `m = 0` >- 1423 metis_tac[GCD_0R, ALL_DIVIDES_0] >> 1424 `0 < n /\ 0 < m` by decide_tac >> 1425 Cases_on `m MOD n = 0` >- 1426 metis_tac[DIVIDES_MOD_0] >> 1427 `0 < m MOD n` by decide_tac >> 1428 metis_tac[GCD_EFFICIENTLY, GCD_DIVIDES, MOD_MOD] 1429 ]); 1430 1431(* Theorem: !m n. n divides m <=> (lcm n m = m) *) 1432(* Proof: 1433 If n = 0, 1434 n divides m <=> m = 0 by ZERO_DIVIDES 1435 and lcm 0 0 = 0 = m by LCM_0 1436 If n <> 0, 1437 gcd n m * lcm n m = n * m by GCD_LCM 1438 If part: n divides m ==> (lcm n m = m) 1439 Then gcd n m = n by divides_iff_gcd_fix 1440 so n * lcm n m = n * m by above 1441 lcm n m = m by MULT_LEFT_CANCEL, n <> 0 1442 Only-if part: lcm n m = m ==> n divides m 1443 If m = 0, n divdes 0 = true by ALL_DIVIDES_0 1444 If m <> 0, 1445 Then gcd n m * m = n * m by above 1446 or gcd n m = n by MULT_RIGHT_CANCEL, m <> 0 1447 so n divides m by divides_iff_gcd_fix 1448*) 1449val divides_iff_lcm_fix = store_thm( 1450 "divides_iff_lcm_fix", 1451 ``!m n. n divides m <=> (lcm n m = m)``, 1452 rpt strip_tac >> 1453 Cases_on `n = 0` >- 1454 metis_tac[ZERO_DIVIDES, LCM_0] >> 1455 metis_tac[GCD_LCM, MULT_LEFT_CANCEL, MULT_RIGHT_CANCEL, divides_iff_gcd_fix, ALL_DIVIDES_0]); 1456 1457(* Theorem: If prime p divides n, ?m. 0 < m /\ (p ** m) divides n /\ n DIV (p ** m) has no p *) 1458(* Proof: 1459 Let s = {j | (p ** j) divides n } 1460 Since p ** 1 = p, 1 IN s, so s <> {}. 1461 (p ** j) divides n 1462 ==> p ** j <= n by DIVIDES_LE 1463 ==> p ** j <= p ** z by EXP_ALWAYS_BIG_ENOUGH 1464 ==> j <= z by EXP_BASE_LE_MONO 1465 ==> s SUBSET count (SUC z), 1466 so FINITE s by FINITE_COUNT, SUBSET_FINITE 1467 Let m = MAX_SET s, 1468 m IN s, so (p ** m) divides n by MAX_SET_DEF 1469 1 <= m, or 0 < m. 1470 ?q. n = q * (p ** m) by divides_def 1471 To prove: !k. gcd (p ** k) (n DIV (p ** m)) = 1 1472 By contradiction, suppose there is a k such that 1473 gcd (p ** k) (n DIV (p ** m)) <> 1 1474 So there is a prime pp that divides this gcd, by PRIME_FACTOR 1475 but pp | p ** k, a pure prime, so pp = p by DIVIDES_EXP_BASE, prime_divides_only_self 1476 pp | n DIV (p ** m) 1477 or pp * p ** m | n 1478 p * SUC m | n, making m not MAX_SET s. 1479*) 1480val FACTOR_OUT_PRIME = store_thm( 1481 "FACTOR_OUT_PRIME", 1482 ``!n p. 0 < n /\ prime p /\ p divides n ==> ?m. 0 < m /\ (p ** m) divides n /\ !k. gcd (p ** k) (n DIV (p ** m)) = 1``, 1483 rpt strip_tac >> 1484 qabbrev_tac `s = {j | (p ** j) divides n }` >> 1485 `!j. j IN s <=> (p ** j) divides n` by rw[Abbr`s`] >> 1486 `p ** 1 = p` by rw[] >> 1487 `1 IN s` by metis_tac[] >> 1488 `1 < p` by rw[ONE_LT_PRIME] >> 1489 `?z. n <= p ** z` by rw[EXP_ALWAYS_BIG_ENOUGH] >> 1490 `!j. j IN s ==> p ** j <= n` by metis_tac[DIVIDES_LE] >> 1491 `!j. j IN s ==> p ** j <= p ** z` by metis_tac[LESS_EQ_TRANS] >> 1492 `!j. j IN s ==> j <= z` by metis_tac[EXP_BASE_LE_MONO] >> 1493 `!j. j <= z <=> j < SUC z` by decide_tac >> 1494 `!j. j < SUC z <=> j IN count (SUC z)` by rw[] >> 1495 `s SUBSET count (SUC z)` by metis_tac[SUBSET_DEF] >> 1496 `FINITE s` by metis_tac[FINITE_COUNT, SUBSET_FINITE] >> 1497 `s <> {}` by metis_tac[MEMBER_NOT_EMPTY] >> 1498 qabbrev_tac `m = MAX_SET s` >> 1499 `m IN s /\ !y. y IN s ==> y <= m`by rw[MAX_SET_DEF, Abbr`m`] >> 1500 qexists_tac `m` >> 1501 CONJ_ASM1_TAC >| [ 1502 `1 <= m` by metis_tac[] >> 1503 decide_tac, 1504 CONJ_ASM1_TAC >- 1505 metis_tac[] >> 1506 qabbrev_tac `pm = p ** m` >> 1507 `0 < p` by decide_tac >> 1508 `0 < pm` by rw[ZERO_LT_EXP, Abbr`pm`] >> 1509 `n MOD pm = 0` by metis_tac[DIVIDES_MOD_0] >> 1510 `n = n DIV pm * pm` by metis_tac[DIVISION, ADD_0] >> 1511 qabbrev_tac `qm = n DIV pm` >> 1512 spose_not_then strip_assume_tac >> 1513 `?q. prime q /\ q divides (gcd (p ** k) qm)` by rw[PRIME_FACTOR] >> 1514 `0 <> pm /\ n <> 0` by decide_tac >> 1515 `qm <> 0` by metis_tac[MULT] >> 1516 `0 < qm` by decide_tac >> 1517 qabbrev_tac `pk = p ** k` >> 1518 `0 < pk` by rw[ZERO_LT_EXP, Abbr`pk`] >> 1519 `(gcd pk qm) divides pk /\ (gcd pk qm) divides qm` by metis_tac[GCD_DIVIDES, DIVIDES_MOD_0] >> 1520 `q divides pk /\ q divides qm` by metis_tac[DIVIDES_TRANS] >> 1521 `k <> 0` by metis_tac[EXP, GCD_1] >> 1522 `0 < k` by decide_tac >> 1523 `q divides p` by metis_tac[DIVIDES_EXP_BASE] >> 1524 `q = p` by rw[prime_divides_only_self] >> 1525 `?x. qm = x * q` by rw[GSYM divides_def] >> 1526 `n = x * p * pm` by metis_tac[] >> 1527 `_ = x * (p * pm)` by rw_tac arith_ss[] >> 1528 `_ = x * (p ** SUC m)` by rw[EXP, Abbr`pm`] >> 1529 `(p ** SUC m) divides n` by metis_tac[divides_def] >> 1530 `SUC m <= m` by metis_tac[] >> 1531 decide_tac 1532 ]); 1533 1534(* ------------------------------------------------------------------------- *) 1535(* Consequences of Coprime. *) 1536(* ------------------------------------------------------------------------- *) 1537 1538(* Overload on coprime for GCD equals 1 *) 1539val _ = overload_on ("coprime", ``\x y. gcd x y = 1``); 1540 1541(* Theorem: If 1 < n, !x. gcd n x = 1 ==> 0 < x /\ 0 < x MOD n *) 1542(* Proof: 1543 If x = 0, gcd n x = n. But n <> 1, hence x <> 0, or 0 < x. 1544 x MOD n = 0 ==> x a multiple of n ==> gcd n x = n <> 1 if n <> 1. 1545 Hence if 1 < n, gcd x n = 1 ==> x MOD n <> 0, or 0 < x MOD n. 1546*) 1547val MOD_NONZERO_WHEN_GCD_ONE = store_thm( 1548 "MOD_NONZERO_WHEN_GCD_ONE", 1549 ``!n. 1 < n ==> !x. (gcd n x = 1) ==> 0 < x /\ 0 < x MOD n``, 1550 ntac 4 strip_tac >> 1551 conj_asm1_tac >| [ 1552 `1 <> n` by decide_tac >> 1553 `x <> 0` by metis_tac[GCD_0R] >> 1554 decide_tac, 1555 `1 <> n /\ x <> 0` by decide_tac >> 1556 `?k q. k * x = q * n + 1` by metis_tac[LINEAR_GCD] >> 1557 `(k*x) MOD n = 1` by rw_tac std_ss[MOD_MULT] >> 1558 spose_not_then strip_assume_tac >> 1559 `(x MOD n = 0) /\ 0 < n /\ 1 <> 0` by decide_tac >> 1560 metis_tac[MOD_MULITPLE_ZERO, MULT_COMM] 1561 ]); 1562 1563(* Theorem: (gcd n x = 1) /\ (gcd n y = 1) ==> (gcd n (x*y) = 1) *) 1564(* Proof: 1565 gcd n x = 1 ==> no common factor between x and n 1566 gcd n y = 1 ==> no common factor between y and n 1567 Hence there is no common factor between (x*y) and n 1568 or gcd n (x*y) = 1 1569 1570 gcd n (x * y) = gcd n y by GCD_CANCEL_MULT, since gcd n x = 1. 1571 = 1 by given 1572*) 1573val PRODUCT_WITH_GCD_ONE = store_thm( 1574 "PRODUCT_WITH_GCD_ONE", 1575 ``!n x y. (gcd n x = 1) /\ (gcd n y = 1) ==> (gcd n (x*y) = 1)``, 1576 metis_tac[GCD_CANCEL_MULT]); 1577 1578(* Theorem: For 0 < n, (gcd n x = 1) ==> (gcd n (x MOD n) = 1) *) 1579(* Proof: 1580 Since n <> 0, 1581 1 = gcd n x by given 1582 = gcd (x MOD n) n by GCD_EFFICIENTLY 1583 = gcd n (x MOD n) by GCD_SYM 1584*) 1585val MOD_WITH_GCD_ONE = store_thm( 1586 "MOD_WITH_GCD_ONE", 1587 ``!n x. 0 < n /\ (gcd n x = 1) ==> (gcd n (x MOD n) = 1)``, 1588 rpt strip_tac >> 1589 `0 <> n` by decide_tac >> 1590 metis_tac[GCD_EFFICIENTLY, GCD_SYM]); 1591 1592(* Theorem: If 1 < n, gcd n x = 1 ==> ?k q. (k * x) MOD n = 1 /\ gcd n k = 1 *) 1593(* Proof: 1594 gcd n x = 1 ==> x <> 0 by GCD_0R 1595 Also, 1596 gcd n x = 1 1597 ==> ?k q. k * x = q * n + 1 by LINEAR_GCD 1598 ==> (k * x) MOD n = (q * n + 1) MOD n by arithmetic 1599 ==> (k * x) MOD n = 1 by MOD_MULT, 1 < n. 1600 1601 Let g = gcd n k. 1602 Since 1 < n, 0 < n. 1603 Since q * n+1 <> 0, x <> 0, k <> 0, hence 0 < k. 1604 Hence 0 < g /\ (n MOD g = 0) /\ (k MOD g = 0) by GCD_DIVIDES. 1605 Or n = a * g /\ k = b * g for some a, b. 1606 Therefore: 1607 (b * g) * x = q * (a * g) + 1 1608 (b * x) * g = (q * a) * g + 1 by arithmetic 1609 Hence g divides 1, or g = 1 since 0 < g. 1610*) 1611val GCD_ONE_PROPERTY = store_thm( 1612 "GCD_ONE_PROPERTY", 1613 ``!n x. 1 < n /\ (gcd n x = 1) ==> ?k. ((k * x) MOD n = 1) /\ (gcd n k = 1)``, 1614 rpt strip_tac >> 1615 `n <> 1` by decide_tac >> 1616 `x <> 0` by metis_tac[GCD_0R] >> 1617 `?k q. k * x = q * n + 1` by metis_tac[LINEAR_GCD] >> 1618 `(k * x) MOD n = 1` by rw_tac std_ss[MOD_MULT] >> 1619 `?g. g = gcd n k` by rw[] >> 1620 `n <> 0 /\ q*n + 1 <> 0` by decide_tac >> 1621 `k <> 0` by metis_tac[MULT_EQ_0] >> 1622 `0 < g /\ (n MOD g = 0) /\ (k MOD g = 0)` by metis_tac[GCD_DIVIDES, NOT_ZERO_LT_ZERO] >> 1623 `g divides n /\ g divides k` by rw[DIVIDES_MOD_0] >> 1624 `g divides (n * q) /\ g divides (k*x)` by rw[DIVIDES_MULT] >> 1625 `g divides (n * q + 1)` by metis_tac [MULT_COMM] >> 1626 `g divides 1` by metis_tac[DIVIDES_ADD_2] >> 1627 metis_tac[DIVIDES_ONE]); 1628 1629(* Theorem: For n > 1, 0 < x < n /\ (gcd n x = 1) ==> 1630 ?y. 0 < y /\ y < n /\ gcd n y = 1 /\ y*x MOD n = 1 *) 1631(* Proof: 1632 gcd n x = 1 1633 ==> ?k. (k*x) MOD n = 1 /\ gcd n k = 1 by GCD_ONE_PROPERTY 1634 (k*x) MOD n = 1 1635 ==> (k MOD n * x MOD n) MOD n = 1 by MOD_TIMES2 1636 ==> ((k MOD n) * x) MOD n = 1 by LESS_MOD, x < n. 1637 1638 Now k MOD n < n by MOD_LESS 1639 and 0 < k MOD n by MOD_MULITPLE_ZERO and 1 <> 0. 1640 1641 Hence take y = k MOD n, then 0 < y < n. 1642 and gcd n k = 1 ==> gcd n (k MOD n) = 1 by MOD_WITH_GCD_ONE. 1643*) 1644val GCD_MOD_MULT_INV = store_thm( 1645 "GCD_MOD_MULT_INV", 1646 ``!n x. 1 < n /\ 0 < x /\ x < n /\ (gcd n x = 1) ==> ?y. 0 < y /\ y < n /\ (gcd n y = 1) /\ ((y*x) MOD n = 1)``, 1647 rpt strip_tac >> 1648 `?k. ((k*x) MOD n = 1) /\ (gcd n k = 1)` by rw_tac std_ss[GCD_ONE_PROPERTY] >> 1649 `0 < n` by decide_tac >> 1650 `(k MOD n * x MOD n) MOD n = 1` by rw_tac std_ss[MOD_TIMES2] >> 1651 `((k MOD n) * x) MOD n = 1` by metis_tac[LESS_MOD] >> 1652 `k MOD n < n` by rw_tac std_ss[MOD_LESS] >> 1653 `1 <> 0` by decide_tac >> 1654 `0 <> k MOD n` by metis_tac[MOD_MULITPLE_ZERO] >> 1655 `0 < k MOD n` by decide_tac >> 1656 metis_tac[MOD_WITH_GCD_ONE]); 1657 1658(* Convert this into an existence definition *) 1659val lemma = prove( 1660 ``!n x. ?y. 1 < n /\ 0 < x /\ x < n /\ (gcd n x = 1) ==> 1661 0 < y /\ y < n /\ (gcd n y = 1) /\ ((y*x) MOD n = 1)``, 1662 metis_tac[GCD_MOD_MULT_INV]); 1663 1664val GEN_MULT_INV_DEF = new_specification( 1665 "GEN_MULT_INV_DEF", 1666 ["GCD_MOD_MUL_INV"], 1667 SIMP_RULE (srw_ss()) [SKOLEM_THM] lemma); 1668(* > val GEN_MULT_INV_DEF = 1669 |- !n x. 1 < n /\ 0 < x /\ x < n /\ coprime n x ==> 1670 0 < GCD_MOD_MUL_INV n x /\ GCD_MOD_MUL_INV n x < n /\ coprime n (GCD_MOD_MUL_INV n x) /\ 1671 ((GCD_MOD_MUL_INV n x * x) MOD n = 1) : thm *) 1672 1673(* ------------------------------------------------------------------------- *) 1674(* More GCD and LCM Theorems *) 1675(* ------------------------------------------------------------------------- *) 1676 1677(* Note: 1678gcdTheory.LCM_IS_LEAST_COMMON_MULTIPLE 1679|- m divides lcm m n /\ n divides lcm m n /\ !p. m divides p /\ n divides p ==> lcm m n divides p 1680gcdTheory.GCD_IS_GREATEST_COMMON_DIVISOR 1681|- !a b. gcd a b divides a /\ gcd a b divides b /\ !d. d divides a /\ d divides b ==> d divides gcd a b 1682*) 1683 1684(* Theorem: (c = gcd a b) <=> 1685 c divides a /\ c divides b /\ !x. x divides a /\ x divides b ==> x divides c *) 1686(* Proof: 1687 By GCD_IS_GREATEST_COMMON_DIVISOR 1688 (gcd a b) divides a [1] 1689 and (gcd a b) divides b [2] 1690 and !p. p divides a /\ p divides b ==> p divides (gcd a b) [3] 1691 Hence if part is true, and for the only-if part, 1692 We have c divides (gcd a b) by [3] above, 1693 and (gcd a b) divides c by [1], [2] and the given implication 1694 Therefore c = gcd a b by DIVIDES_ANTISYM 1695*) 1696val GCD_PROPERTY = store_thm( 1697 "GCD_PROPERTY", 1698 ``!a b c. (c = gcd a b) <=> 1699 c divides a /\ c divides b /\ !x. x divides a /\ x divides b ==> x divides c``, 1700 rw[GCD_IS_GREATEST_COMMON_DIVISOR, DIVIDES_ANTISYM, EQ_IMP_THM]); 1701 1702(* Theorem: gcd a (gcd b c) = gcd (gcd a b) c *) 1703(* Proof: 1704 Since (gcd a (gcd b c)) divides a by GCD_PROPERTY 1705 (gcd a (gcd b c)) divides b by GCD_PROPERTY, DIVIDES_TRANS 1706 (gcd a (gcd b c)) divides c by GCD_PROPERTY, DIVIDES_TRANS 1707 (gcd (gcd a b) c) divides a by GCD_PROPERTY, DIVIDES_TRANS 1708 (gcd (gcd a b) c) divides b by GCD_PROPERTY, DIVIDES_TRANS 1709 (gcd (gcd a b) c) divides c by GCD_PROPERTY 1710 We have 1711 (gcd (gcd a b) c) divides (gcd b c) by GCD_PROPERTY 1712 and (gcd (gcd a b) c) divides (gcd a (gcd b c)) by GCD_PROPERTY 1713 Also (gcd a (gcd b c)) divides (gcd a b) by GCD_PROPERTY 1714 and (gcd a (gcd b c)) divides (gcd (gcd a b) c) by GCD_PROPERTY 1715 Therefore gcd a (gcd b c) = gcd (gcd a b) c by DIVIDES_ANTISYM 1716*) 1717val GCD_ASSOC = store_thm( 1718 "GCD_ASSOC", 1719 ``!a b c. gcd a (gcd b c) = gcd (gcd a b) c``, 1720 rpt strip_tac >> 1721 `(gcd a (gcd b c)) divides a` by metis_tac[GCD_PROPERTY] >> 1722 `(gcd a (gcd b c)) divides b` by metis_tac[GCD_PROPERTY, DIVIDES_TRANS] >> 1723 `(gcd a (gcd b c)) divides c` by metis_tac[GCD_PROPERTY, DIVIDES_TRANS] >> 1724 `(gcd (gcd a b) c) divides a` by metis_tac[GCD_PROPERTY, DIVIDES_TRANS] >> 1725 `(gcd (gcd a b) c) divides b` by metis_tac[GCD_PROPERTY, DIVIDES_TRANS] >> 1726 `(gcd (gcd a b) c) divides c` by metis_tac[GCD_PROPERTY] >> 1727 `(gcd (gcd a b) c) divides (gcd a (gcd b c))` by metis_tac[GCD_PROPERTY] >> 1728 `(gcd a (gcd b c)) divides (gcd (gcd a b) c)` by metis_tac[GCD_PROPERTY] >> 1729 rw[DIVIDES_ANTISYM]); 1730 1731(* Note: 1732 With identity by GCD_1: (gcd 1 x = 1) /\ (gcd x 1 = 1) 1733 GCD forms a monoid in numbers. 1734*) 1735 1736(* Theorem: gcd a (gcd b c) = gcd b (gcd a c) *) 1737(* Proof: 1738 gcd a (gcd b c) 1739 = gcd (gcd a b) c by GCD_ASSOC 1740 = gcd (gcd b a) c by GCD_SYM 1741 = gcd b (gcd a c) by GCD_ASSOC 1742*) 1743val GCD_ASSOC_COMM = store_thm( 1744 "GCD_ASSOC_COMM", 1745 ``!a b c. gcd a (gcd b c) = gcd b (gcd a c)``, 1746 metis_tac[GCD_ASSOC, GCD_SYM]); 1747 1748(* Theorem: (c = lcm a b) <=> 1749 a divides c /\ b divides c /\ !x. a divides x /\ b divides x ==> c divides x *) 1750(* Proof: 1751 By LCM_IS_LEAST_COMMON_MULTIPLE 1752 a divides (lcm a b) [1] 1753 and b divides (lcm a b) [2] 1754 and !p. a divides p /\ divides b p ==> divides (lcm a b) p [3] 1755 Hence if part is true, and for the only-if part, 1756 We have c divides (lcm a b) by implication and [1], [2] 1757 and (lcm a b) divides c by [3] 1758 Therefore c = lcm a b by DIVIDES_ANTISYM 1759*) 1760val LCM_PROPERTY = store_thm( 1761 "LCM_PROPERTY", 1762 ``!a b c. (c = lcm a b) <=> 1763 a divides c /\ b divides c /\ !x. a divides x /\ b divides x ==> c divides x``, 1764 rw[LCM_IS_LEAST_COMMON_MULTIPLE, DIVIDES_ANTISYM, EQ_IMP_THM]); 1765 1766(* Theorem: lcm a (lcm b c) = lcm (lcm a b) c *) 1767(* Proof: 1768 Since a divides (lcm a (lcm b c)) by LCM_PROPERTY 1769 b divides (lcm a (lcm b c)) by LCM_PROPERTY, DIVIDES_TRANS 1770 c divides (lcm a (lcm b c)) by LCM_PROPERTY, DIVIDES_TRANS 1771 a divides (lcm (lcm a b) c) by LCM_PROPERTY, DIVIDES_TRANS 1772 b divides (lcm (lcm a b) c) by LCM_PROPERTY, DIVIDES_TRANS 1773 c divides (lcm (lcm a b) c) by LCM_PROPERTY 1774 We have 1775 (lcm b c) divides (lcm (lcm a b) c) by LCM_PROPERTY 1776 and (lcm a (lcm b c)) divides (lcm (lcm a b) c) by LCM_PROPERTY 1777 Also (lcm a b) divides (lcm a (lcm b c)) by LCM_PROPERTY 1778 and (lcm (lcm a b) c) divides (lcm a (lcm b c)) by LCM_PROPERTY 1779 Therefore lcm a (lcm b c) = lcm (lcm a b) c by DIVIDES_ANTISYM 1780*) 1781val LCM_ASSOC = store_thm( 1782 "LCM_ASSOC", 1783 ``!a b c. lcm a (lcm b c) = lcm (lcm a b) c``, 1784 rpt strip_tac >> 1785 `a divides (lcm a (lcm b c))` by metis_tac[LCM_PROPERTY] >> 1786 `b divides (lcm a (lcm b c))` by metis_tac[LCM_PROPERTY, DIVIDES_TRANS] >> 1787 `c divides (lcm a (lcm b c))` by metis_tac[LCM_PROPERTY, DIVIDES_TRANS] >> 1788 `a divides (lcm (lcm a b) c)` by metis_tac[LCM_PROPERTY, DIVIDES_TRANS] >> 1789 `b divides (lcm (lcm a b) c)` by metis_tac[LCM_PROPERTY, DIVIDES_TRANS] >> 1790 `c divides (lcm (lcm a b) c)` by metis_tac[LCM_PROPERTY] >> 1791 `(lcm a (lcm b c)) divides (lcm (lcm a b) c)` by metis_tac[LCM_PROPERTY] >> 1792 `(lcm (lcm a b) c) divides (lcm a (lcm b c))` by metis_tac[LCM_PROPERTY] >> 1793 rw[DIVIDES_ANTISYM]); 1794 1795(* Note: 1796 With the identity by LCM_0: (lcm 0 x = 0) /\ (lcm x 0 = 0) 1797 LCM forms a monoid in numbers. 1798*) 1799 1800(* Theorem: lcm a (lcm b c) = lcm b (lcm a c) *) 1801(* Proof: 1802 lcm a (lcm b c) 1803 = lcm (lcm a b) c by LCM_ASSOC 1804 = lcm (lcm b a) c by LCM_COMM 1805 = lcm b (lcm a c) by LCM_ASSOC 1806*) 1807val LCM_ASSOC_COMM = store_thm( 1808 "LCM_ASSOC_COMM", 1809 ``!a b c. lcm a (lcm b c) = lcm b (lcm a c)``, 1810 metis_tac[LCM_ASSOC, LCM_COMM]); 1811 1812(* Theorem: b <= a ==> gcd (a - b) b = gcd a b *) 1813(* Proof: 1814 gcd (a - b) b 1815 = gcd b (a - b) by GCD_SYM 1816 = gcd (b + (a - b)) b by GCD_ADD_L 1817 = gcd (a - b + b) b by ADD_COMM 1818 = gcd a b by SUB_ADD, b <= a. 1819 1820Note: If a < b, a - b = 0 for num, hence gcd (a - b) b = gcd 0 b = b. 1821*) 1822val GCD_SUB_L = store_thm( 1823 "GCD_SUB_L", 1824 ``!a b. b <= a ==> (gcd (a - b) b = gcd a b)``, 1825 metis_tac[GCD_SYM, GCD_ADD_L, ADD_COMM, SUB_ADD]); 1826 1827(* Theorem: a <= b ==> gcd a (b - a) = gcd a b *) 1828(* Proof: 1829 gcd a (b - a) 1830 = gcd (b - a) a by GCD_SYM 1831 = gcd b a by GCD_SUB_L 1832 = gcd a b by GCD_SYM 1833*) 1834val GCD_SUB_R = store_thm( 1835 "GCD_SUB_R", 1836 ``!a b. a <= b ==> (gcd a (b - a) = gcd a b)``, 1837 metis_tac[GCD_SYM, GCD_SUB_L]); 1838 1839(* Theorem: If 1/c = 1/b - 1/a, then lcm a b = lcm a c. 1840 a * b = c * (a - b) ==> lcm a b = lcm a c *) 1841(* Proof: 1842 Idea: 1843 lcm a c 1844 = (a * c) DIV (gcd a c) by lcm_def 1845 = (a * b * c) DIV (gcd a c) DIV b by MULT_DIV 1846 = (a * b * c) DIV b * (gcd a c) by DIV_DIV_DIV_MULT 1847 = (a * b * c) DIV gcd b*a b*c by GCD_COMMON_FACTOR 1848 = (a * b * c) DIV gcd c*(a-b) c*b by given 1849 = (a * b * c) DIV c * gcd (a-b) b by GCD_COMMON_FACTOR 1850 = (a * b * c) DIV c * gcd a b by GCD_SUB_L 1851 = (a * b * c) DIV c DIV gcd a b by DIV_DIV_DIV_MULT 1852 = a * b DIV gcd a b by MULT_DIV 1853 = lcm a b by lcm_def 1854 1855 Details: 1856 If a = 0, 1857 lcm 0 b = 0 = lcm 0 c by LCM_0 1858 If a <> 0, 1859 If b = 0, a * b = 0 = c * a by MULT_0, SUB_0 1860 Hence c = 0, hence true by MULT_EQ_0 1861 If b <> 0, c <> 0. by MULT_EQ_0 1862 So 0 < gcd a c, 0 < gcd a b by GCD_EQ_0 1863 and (gcd a c) divides a by GCD_IS_GREATEST_COMMON_DIVISOR 1864 thus (gcd a c) divides (a * c) by DIVIDES_MULT 1865 Note (a - b) <> 0 by MULT_EQ_0 1866 so ~(a <= b) by SUB_EQ_0 1867 or b < a, or b <= a for GCD_SUB_L later. 1868 Now, 1869 lcm a c 1870 = (a * c) DIV (gcd a c) by lcm_def 1871 = (b * ((a * c) DIV (gcd a c))) DIV b by MULT_COMM, MULT_DIV 1872 = ((b * (a * c)) DIV (gcd a c)) DIV b by MULTIPLY_DIV 1873 = (b * (a * c)) DIV ((gcd a c) * b) by DIV_DIV_DIV_MULT 1874 = (b * a * c) DIV ((gcd a c) * b) by MULT_ASSOC 1875 = c * (a * b) DIV (b * (gcd a c)) by MULT_COMM 1876 = c * (a * b) DIV (gcd (b * a) (b * c)) by GCD_COMMON_FACTOR 1877 = c * (a * b) DIV (gcd (a * b) (c * b)) by MULT_COMM 1878 = c * (a * b) DIV (gcd (c * (a-b)) (c * b)) by a * b = c * (a - b) 1879 = c * (a * b) DIV (c * gcd (a-b) b) by GCD_COMMON_FACTOR 1880 = c * (a * b) DIV (c * gcd a b) by GCD_SUB_L 1881 = c * (a * b) DIV c DIV (gcd a b) by DIV_DIV_DIV_MULT 1882 = a * b DIV gcd a b by MULT_COMM, MULT_DIV 1883 = lcm a b by lcm_def 1884*) 1885val LCM_EXCHANGE = store_thm( 1886 "LCM_EXCHANGE", 1887 ``!a b c. (a * b = c * (a - b)) ==> (lcm a b = lcm a c)``, 1888 rpt strip_tac >> 1889 Cases_on `a = 0` >- 1890 rw[] >> 1891 Cases_on `b = 0` >| [ 1892 `c = 0` by metis_tac[MULT_EQ_0, SUB_0] >> 1893 rw[], 1894 `c <> 0` by metis_tac[MULT_EQ_0] >> 1895 `0 < b /\ 0 < c` by decide_tac >> 1896 `(gcd a c) divides a` by rw[GCD_IS_GREATEST_COMMON_DIVISOR] >> 1897 `(gcd a c) divides (a * c)` by rw[DIVIDES_MULT] >> 1898 `0 < gcd a c /\ 0 < gcd a b` by metis_tac[GCD_EQ_0, NOT_ZERO_LT_ZERO] >> 1899 `~(a <= b)` by metis_tac[SUB_EQ_0, MULT_EQ_0] >> 1900 `b <= a` by decide_tac >> 1901 `lcm a c = (a * c) DIV (gcd a c)` by rw[lcm_def] >> 1902 `_ = (b * ((a * c) DIV (gcd a c))) DIV b` by metis_tac[MULT_COMM, MULT_DIV] >> 1903 `_ = ((b * (a * c)) DIV (gcd a c)) DIV b` by rw[MULTIPLY_DIV] >> 1904 `_ = (b * (a * c)) DIV ((gcd a c) * b)` by rw[DIV_DIV_DIV_MULT] >> 1905 `_ = (b * a * c) DIV ((gcd a c) * b)` by rw[MULT_ASSOC] >> 1906 `_ = c * (a * b) DIV (b * (gcd a c))` by rw_tac std_ss[MULT_COMM] >> 1907 `_ = c * (a * b) DIV (gcd (b * a) (b * c))` by rw[GCD_COMMON_FACTOR] >> 1908 `_ = c * (a * b) DIV (gcd (a * b) (c * b))` by rw_tac std_ss[MULT_COMM] >> 1909 `_ = c * (a * b) DIV (gcd (c * (a-b)) (c * b))` by rw[] >> 1910 `_ = c * (a * b) DIV (c * gcd (a-b) b)` by rw[GCD_COMMON_FACTOR] >> 1911 `_ = c * (a * b) DIV (c * gcd a b)` by rw[GCD_SUB_L] >> 1912 `_ = c * (a * b) DIV c DIV (gcd a b)` by rw[DIV_DIV_DIV_MULT] >> 1913 `_ = a * b DIV gcd a b` by metis_tac[MULT_COMM, MULT_DIV] >> 1914 `_ = lcm a b` by rw[lcm_def] >> 1915 decide_tac 1916 ]); 1917 1918(* Theorem: coprime m n ==> LCM m n = m * n *) 1919(* Proof: 1920 By GCD_LCM, with gcd m n = 1. 1921*) 1922val LCM_COPRIME = store_thm( 1923 "LCM_COPRIME", 1924 ``!m n. coprime m n ==> (lcm m n = m * n)``, 1925 metis_tac[GCD_LCM, MULT_LEFT_1]); 1926 1927(* Theorem: LCM (k * m) (k * n) = k * LCM m n *) 1928(* Proof: 1929 If m = 0 or n = 0, LHS = 0 = RHS. 1930 If m <> 0 and n <> 0, 1931 lcm (k * m) (k * n) 1932 = (k * m) * (k * n) / gcd (k * m) (k * n) by GCD_LCM 1933 = (k * m) * (k * n) / k * (gcd m n) by GCD_COMMON_FACTOR 1934 = k * m * n / (gcd m n) 1935 = k * LCM m n by GCD_LCM 1936*) 1937val LCM_COMMON_FACTOR = store_thm( 1938 "LCM_COMMON_FACTOR", 1939 ``!m n k. lcm (k * m) (k * n) = k * lcm m n``, 1940 rpt strip_tac >> 1941 `k * (k * (m * n)) = (k * m) * (k * n)` by rw_tac arith_ss[] >> 1942 `_ = gcd (k * m) (k * n) * lcm (k * m) (k * n) ` by rw[GCD_LCM] >> 1943 `_ = k * (gcd m n) * lcm (k * m) (k * n)` by rw[GCD_COMMON_FACTOR] >> 1944 `_ = k * ((gcd m n) * lcm (k * m) (k * n))` by rw_tac arith_ss[] >> 1945 Cases_on `k = 0` >- 1946 rw[] >> 1947 `(gcd m n) * lcm (k * m) (k * n) = k * (m * n)` by metis_tac[MULT_LEFT_CANCEL] >> 1948 `_ = k * ((gcd m n) * (lcm m n))` by rw_tac std_ss[GCD_LCM] >> 1949 `_ = (gcd m n) * (k * (lcm m n))` by rw_tac arith_ss[] >> 1950 Cases_on `n = 0` >- 1951 rw[] >> 1952 metis_tac[MULT_LEFT_CANCEL, GCD_EQ_0]); 1953 1954(* Theorem: coprime a b ==> !c. lcm (a * c) (b * c) = a * b * c *) 1955(* Proof: 1956 lcm (a * c) (b * c) 1957 = lcm (c * a) (c * b) by MULT_COMM 1958 = c * (lcm a b) by LCM_COMMON_FACTOR 1959 = (lcm a b) * c by MULT_COMM 1960 = a * b * c by LCM_COPRIME 1961*) 1962val LCM_COMMON_COPRIME = store_thm( 1963 "LCM_COMMON_COPRIME", 1964 ``!a b. coprime a b ==> !c. lcm (a * c) (b * c) = a * b * c``, 1965 metis_tac[LCM_COMMON_FACTOR, LCM_COPRIME, MULT_COMM]); 1966 1967(* Theorem: 0 < n /\ m MOD n = 0 ==> gcd m n = n *) 1968(* Proof: 1969 Since m MOD n = 0 1970 ==> n divides m by DIVIDES_MOD_0 1971 Hence gcd m n = gcd n m by GCD_SYM 1972 = n by divides_iff_gcd_fix 1973*) 1974val GCD_MULTIPLE = store_thm( 1975 "GCD_MULTIPLE", 1976 ``!m n. 0 < n /\ (m MOD n = 0) ==> (gcd m n = n)``, 1977 metis_tac[DIVIDES_MOD_0, divides_iff_gcd_fix, GCD_SYM]); 1978 1979(* Theorem: gcd (m * n) n = n *) 1980(* Proof: 1981 gcd (m * n) n 1982 = gcd (n * m) n by MULT_COMM 1983 = gcd (n * m) (n * 1) by MULT_RIGHT_1 1984 = n * (gcd m 1) by GCD_COMMON_FACTOR 1985 = n * 1 by GCD_1 1986 = n by MULT_RIGHT_1 1987*) 1988val GCD_MULTIPLE_ALT = store_thm( 1989 "GCD_MULTIPLE_ALT", 1990 ``!m n. gcd (m * n) n = n``, 1991 rpt strip_tac >> 1992 `gcd (m * n) n = gcd (n * m) n` by rw[MULT_COMM] >> 1993 `_ = gcd (n * m) (n * 1)` by rw[] >> 1994 rw[GCD_COMMON_FACTOR]); 1995 1996(* Theorem: k * a <= b ==> gcd a b = gcd a (b - k * a) *) 1997(* Proof: 1998 By induction on k. 1999 Base case: 0 * a <= b ==> gcd a b = gcd a (b - 0 * a) 2000 True since b - 0 * a = b by MULT, SUB_0 2001 Step case: k * a <= b ==> (gcd a b = gcd a (b - k * a)) ==> 2002 SUC k * a <= b ==> (gcd a b = gcd a (b - SUC k * a)) 2003 SUC k * a <= b 2004 ==> k * a + a <= b by MULT 2005 so a <= b - k * a by arithmetic [1] 2006 and k * a <= b by 0 <= b - k * a, [2] 2007 gcd a (b - SUC k * a) 2008 = gcd a (b - (k * a + a)) by MULT 2009 = gcd a (b - k * a - a) by arithmetic 2010 = gcd a (b - k * a - a + a) by GCD_ADD_L, ADD_COMM 2011 = gcd a (b - k * a) by SUB_ADD, a <= b - k * a [1] 2012 = gcd a b by induction hypothesis, k * a <= b [2] 2013*) 2014val GCD_SUB_MULTIPLE = store_thm( 2015 "GCD_SUB_MULTIPLE", 2016 ``!a b k. k * a <= b ==> (gcd a b = gcd a (b - k * a))``, 2017 rpt strip_tac >> 2018 Induct_on `k` >- 2019 rw[] >> 2020 rw_tac std_ss[] >> 2021 `k * a + a <= b` by metis_tac[MULT] >> 2022 `a <= b - k * a` by decide_tac >> 2023 `k * a <= b` by decide_tac >> 2024 `gcd a (b - SUC k * a) = gcd a (b - (k * a + a))` by rw[MULT] >> 2025 `_ = gcd a (b - k * a - a)` by rw_tac arith_ss[] >> 2026 `_ = gcd a (b - k * a - a + a)` by rw[GCD_ADD_L, ADD_COMM] >> 2027 rw_tac std_ss[SUB_ADD]); 2028 2029(* Theorem: k * a <= b ==> (gcd b a = gcd a (b - k * a)) *) 2030(* Proof: by GCD_SUB_MULTIPLE, GCD_SYM *) 2031val GCD_SUB_MULTIPLE_COMM = store_thm( 2032 "GCD_SUB_MULTIPLE_COMM", 2033 ``!a b k. k * a <= b ==> (gcd b a = gcd a (b - k * a))``, 2034 metis_tac[GCD_SUB_MULTIPLE, GCD_SYM]); 2035 2036(* Theorem: 0 < m ==> (gcd m n = gcd m (n MOD m)) *) 2037(* Proof: 2038 gcd m n 2039 = gcd (n MOD m) m by GCD_EFFICIENTLY, m <> 0 2040 = gcd m (n MOD m) by GCD_SYM 2041*) 2042val GCD_MOD = store_thm( 2043 "GCD_MOD", 2044 ``!m n. 0 < m ==> (gcd m n = gcd m (n MOD m))``, 2045 rw[Once GCD_EFFICIENTLY, GCD_SYM]); 2046 2047(* Theorem: 0 < m ==> (gcd n m = gcd (n MOD m) m) *) 2048(* Proof: by GCD_MOD, GCD_COMM *) 2049val GCD_MOD_COMM = store_thm( 2050 "GCD_MOD_COMM", 2051 ``!m n. 0 < m ==> (gcd n m = gcd (n MOD m) m)``, 2052 metis_tac[GCD_MOD, GCD_COMM]); 2053 2054(* Theorem: gcd a (b * a + c) = gcd a c *) 2055(* Proof: 2056 If a = 0, 2057 Then b * 0 + c = c by arithmetic 2058 Hence trivially true. 2059 If a <> 0, 2060 gcd a (b * a + c) 2061 = gcd ((b * a + c) MOD a) a by GCD_EFFICIENTLY, 0 < a 2062 = gcd (c MOD a) a by MOD_TIMES, 0 < a 2063 = gcd a c by GCD_EFFICIENTLY, 0 < a 2064*) 2065val GCD_EUCLID = store_thm( 2066 "GCD_EUCLID", 2067 ``!a b c. gcd a (b * a + c) = gcd a c``, 2068 rpt strip_tac >> 2069 Cases_on `a = 0` >- 2070 rw[] >> 2071 metis_tac[GCD_EFFICIENTLY, MOD_TIMES, NOT_ZERO_LT_ZERO]); 2072 2073(* Theorem: gcd (b * a + c) a = gcd a c *) 2074(* Proof: by GCD_EUCLID, GCD_SYM *) 2075val GCD_REDUCE = store_thm( 2076 "GCD_REDUCE", 2077 ``!a b c. gcd (b * a + c) a = gcd a c``, 2078 rw[GCD_EUCLID, GCD_SYM]); 2079 2080(* ------------------------------------------------------------------------- *) 2081(* Coprime Theorems *) 2082(* ------------------------------------------------------------------------- *) 2083 2084(* Theorem: coprime n (n + 1) *) 2085(* Proof: 2086 Since n < n + 1 ==> n <= n + 1, 2087 gcd n (n + 1) 2088 = gcd n (n + 1 - n) by GCD_SUB_R 2089 = gcd n 1 by arithmetic 2090 = 1 by GCD_1 2091*) 2092val coprime_SUC = store_thm( 2093 "coprime_SUC", 2094 ``!n. coprime n (n + 1)``, 2095 rw[GCD_SUB_R]); 2096 2097(* Theorem: 0 < n ==> coprime n (n - 1) *) 2098(* Proof: 2099 gcd n (n - 1) 2100 = gcd (n - 1) n by GCD_SYM 2101 = gcd (n - 1) (n - 1 + 1) by SUB_ADD, 0 <= n 2102 = 1 by coprime_SUC 2103*) 2104val coprime_PRE = store_thm( 2105 "coprime_PRE", 2106 ``!n. 0 < n ==> coprime n (n - 1)``, 2107 metis_tac[GCD_SYM, coprime_SUC, DECIDE``!n. 0 < n ==> (n - 1 + 1 = n)``]); 2108 2109(* Theorem: coprime 0 n ==> n = 1 *) 2110(* Proof: 2111 gcd 0 n = n by GCD_0L 2112 = 1 by coprime 0 n 2113*) 2114val coprime_0L = store_thm( 2115 "coprime_0L", 2116 ``!n. coprime 0 n <=> (n = 1)``, 2117 rw[GCD_0L]); 2118 2119(* Theorem: coprime n 0 ==> n = 1 *) 2120(* Proof: 2121 gcd n 0 = n by GCD_0L 2122 = 1 by coprime n 0 2123*) 2124val coprime_0R = store_thm( 2125 "coprime_0R", 2126 ``!n. coprime n 0 <=> (n = 1)``, 2127 rw[GCD_0R]); 2128 2129(* Theorem: coprime x y = coprime y x *) 2130(* Proof: 2131 coprime x y 2132 means gcd x y = 1 2133 so gcd y x = 1 by GCD_SYM 2134 thus coprime y x 2135*) 2136val coprime_sym = store_thm( 2137 "coprime_sym", 2138 ``!x y. coprime x y = coprime y x``, 2139 rw[GCD_SYM]); 2140 2141(* Theorem: coprime k n /\ n <> 1 ==> k <> 0 *) 2142(* Proof: by coprime_0L *) 2143val coprime_neq_1 = store_thm( 2144 "coprime_neq_1", 2145 ``!n k. coprime k n /\ n <> 1 ==> k <> 0``, 2146 fs[coprime_0L]); 2147 2148(* Theorem: coprime k n /\ 1 < n ==> 0 < k *) 2149(* Proof: by coprime_neq_1 *) 2150val coprime_gt_1 = store_thm( 2151 "coprime_gt_1", 2152 ``!n k. coprime k n /\ 1 < n ==> 0 < k``, 2153 metis_tac[coprime_neq_1, NOT_ZERO_LT_ZERO, DECIDE``~(1 < 1)``]); 2154 2155(* Note: gcd (c ** n) m = gcd c m is false when n = 0, where c ** 0 = 1. *) 2156 2157(* Theorem: coprime c m ==> !n. coprime (c ** n) m *) 2158(* Proof: by induction on n. 2159 Base case: coprime (c ** 0) m 2160 Since c ** 0 = 1 by EXP 2161 and coprime 1 m is true by GCD_1 2162 Step case: coprime c m /\ coprime (c ** n) m ==> coprime (c ** SUC n) m 2163 coprime c m means 2164 coprime m c by GCD_SYM 2165 2166 gcd m (c ** SUC n) 2167 = gcd m (c * c ** n) by EXP 2168 = gcd m (c ** n) by GCD_CANCEL_MULT, coprime m c 2169 = 1 by induction hypothesis 2170 Hence coprime m (c ** SUC n) 2171 or coprime (c ** SUC n) m by GCD_SYM 2172*) 2173val coprime_exp = store_thm( 2174 "coprime_exp", 2175 ``!c m. coprime c m ==> !n. coprime (c ** n) m``, 2176 rpt strip_tac >> 2177 Induct_on `n` >- 2178 rw[EXP, GCD_1] >> 2179 metis_tac[EXP, GCD_CANCEL_MULT, GCD_SYM]); 2180 2181(* Theorem: coprime a b ==> !n. coprime a (b ** n) *) 2182(* Proof: by coprime_exp, GCD_SYM *) 2183val coprime_exp_comm = store_thm( 2184 "coprime_exp_comm", 2185 ``!a b. coprime a b ==> !n. coprime a (b ** n)``, 2186 metis_tac[coprime_exp, GCD_SYM]); 2187 2188(* Theorem: 0 < n ==> !a b. coprime a b <=> coprime a (b ** n) *) 2189(* Proof: 2190 If part: coprime a b ==> coprime a (b ** n) 2191 True by coprime_exp_comm. 2192 Only-if part: coprime a (b ** n) ==> coprime a b 2193 If a = 0, 2194 then b ** n = 1 by GCD_0L 2195 and b = 1 by EXP_EQ_1, n <> 0 2196 Hence coprime 0 1 by GCD_0L 2197 If a <> 0, 2198 Since coprime a (b ** n) means 2199 ?h k. h * a = k * b ** n + 1 by LINEAR_GCD, GCD_SYM 2200 Let d = gcd a b. 2201 Since d divides a and d divides b by GCD_IS_GREATEST_COMMON_DIVISOR 2202 and d divides b ** n by divides_exp, 0 < n 2203 so d divides 1 by divides_linear_sub 2204 Thus d = 1 by DIVIDES_ONE 2205 or coprime a b by notation 2206*) 2207val coprime_iff_coprime_exp = store_thm( 2208 "coprime_iff_coprime_exp", 2209 ``!n. 0 < n ==> !a b. coprime a b <=> coprime a (b ** n)``, 2210 rw[EQ_IMP_THM] >- 2211 rw[coprime_exp_comm] >> 2212 `n <> 0` by decide_tac >> 2213 Cases_on `a = 0` >- 2214 metis_tac[GCD_0L, EXP_EQ_1] >> 2215 `?h k. h * a = k * b ** n + 1` by metis_tac[LINEAR_GCD, GCD_SYM] >> 2216 qabbrev_tac `d = gcd a b` >> 2217 `d divides a /\ d divides b` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >> 2218 `d divides (b ** n)` by rw[divides_exp] >> 2219 `d divides 1` by metis_tac[divides_linear_sub] >> 2220 rw[GSYM DIVIDES_ONE]); 2221 2222(* Theorem: coprime x z /\ coprime y z ==> coprime (x * y) z *) 2223(* Proof: 2224 By GCD_CANCEL_MULT: 2225 |- !m n k. coprime m k ==> (gcd m (k * n) = gcd m n) 2226 Hence follows by coprime_sym. 2227*) 2228val coprime_product_coprime = store_thm( 2229 "coprime_product_coprime", 2230 ``!x y z. coprime x z /\ coprime y z ==> coprime (x * y) z``, 2231 metis_tac[GCD_CANCEL_MULT, GCD_SYM]); 2232 2233(* Theorem: coprime z x /\ coprime z y ==> coprime z (x * y) *) 2234(* Proof: 2235 Note gcd z x = 1 by given 2236 ==> gcd z (x * y) 2237 = gcd z y by GCD_CANCEL_MULT 2238 = 1 by given 2239*) 2240val coprime_product_coprime_sym = store_thm( 2241 "coprime_product_coprime_sym", 2242 ``!x y z. coprime z x /\ coprime z y ==> coprime z (x * y)``, 2243 rw[GCD_CANCEL_MULT]); 2244(* This is the same as PRODUCT_WITH_GCD_ONE *) 2245 2246(* Theorem: coprime x z ==> (coprime y z <=> coprime (x * y) z) *) 2247(* Proof: 2248 If part: coprime x z /\ coprime y z ==> coprime (x * y) z 2249 True by coprime_product_coprime 2250 Only-if part: coprime x z /\ coprime (x * y) z ==> coprime y z 2251 Let d = gcd y z. 2252 Then d divides z /\ d divides y by GCD_PROPERTY 2253 so d divides (x * y) by DIVIDES_MULT, MULT_COMM 2254 or d divides (gcd (x * y) z) by GCD_PROPERTY 2255 d divides 1 by coprime (x * y) z 2256 ==> d = 1 by DIVIDES_ONE 2257 or coprime y z by notation 2258*) 2259val coprime_product_coprime_iff = store_thm( 2260 "coprime_product_coprime_iff", 2261 ``!x y z. coprime x z ==> (coprime y z <=> coprime (x * y) z)``, 2262 rw[EQ_IMP_THM] >- 2263 rw[coprime_product_coprime] >> 2264 qabbrev_tac `d = gcd y z` >> 2265 metis_tac[GCD_PROPERTY, DIVIDES_MULT, MULT_COMM, DIVIDES_ONE]); 2266 2267(* Theorem: a divides n /\ b divides n /\ coprime a b ==> (a * b) divides n *) 2268(* Proof: by LCM_COPRIME, LCM_DIVIDES *) 2269val coprime_product_divides = store_thm( 2270 "coprime_product_divides", 2271 ``!n a b. a divides n /\ b divides n /\ coprime a b ==> (a * b) divides n``, 2272 metis_tac[LCM_COPRIME, LCM_DIVIDES]); 2273 2274(* Theorem: 0 < m /\ coprime m n ==> coprime m (n MOD m) *) 2275(* Proof: 2276 gcd m n 2277 = if m = 0 then n else gcd (n MOD m) m by GCD_EFFICIENTLY 2278 = gcd (n MOD m) m by decide_tac, m <> 0 2279 = gcd m (n MOD m) by GCD_SYM 2280 Hence true since coprime m n <=> gcd m n = 1. 2281*) 2282val coprime_mod = store_thm( 2283 "coprime_mod", 2284 ``!m n. 0 < m /\ coprime m n ==> coprime m (n MOD m)``, 2285 metis_tac[GCD_EFFICIENTLY, GCD_SYM, NOT_ZERO_LT_ZERO]); 2286 2287(* Theorem: 0 < m ==> (coprime m n = coprime m (n MOD m)) *) 2288(* Proof: by GCD_MOD *) 2289val coprime_mod_iff = store_thm( 2290 "coprime_mod_iff", 2291 ``!m n. 0 < m ==> (coprime m n = coprime m (n MOD m))``, 2292 rw[Once GCD_MOD]); 2293 2294(* Theorem: 1 < n /\ coprime n m ==> ~(n divides m) *) 2295(* Proof: 2296 coprime n m 2297 ==> gcd n m = 1 by notation 2298 ==> n MOD m <> 0 by MOD_NONZERO_WHEN_GCD_ONE, with 1 < n 2299 ==> ~(n divides m) by DIVIDES_MOD_0, with 0 < n 2300*) 2301val coprime_not_divides = store_thm( 2302 "coprime_not_divides", 2303 ``!m n. 1 < n /\ coprime n m ==> ~(n divides m)``, 2304 metis_tac[MOD_NONZERO_WHEN_GCD_ONE, DIVIDES_MOD_0, ONE_LT_POS, NOT_ZERO_LT_ZERO]); 2305 2306(* Theorem: 1 < n /\ coprime n k /\ 1 < p /\ p divides n ==> ~(p divides k) *) 2307(* Proof: 2308 First, 1 < n ==> n <> 0 and n <> 1 2309 If k = 0, gcd n k = n by GCD_0R 2310 But coprime n k means gcd n k = 1, so k <> 0. 2311 By contradiction. 2312 If p divides k, and given p divides n, 2313 then p divides gcd n k = 1 by GCD_IS_GREATEST_COMMON_DIVISOR, n <> 0 and k <> 0 2314 or p = 1 by DIVIDES_ONE 2315 which contradicts 1 < p. 2316*) 2317val coprime_factor_not_divides = store_thm( 2318 "coprime_factor_not_divides", 2319 ``!n k. 1 < n /\ coprime n k ==> !p. 1 < p /\ p divides n ==> ~(p divides k)``, 2320 rpt strip_tac >> 2321 `n <> 0 /\ n <> 1 /\ p <> 1` by decide_tac >> 2322 metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR, DIVIDES_ONE, GCD_0R]); 2323 2324(* Theorem: m divides n ==> !k. coprime n k ==> coprime m k *) 2325(* Proof: 2326 Let d = gcd m k. 2327 Then d divides m /\ d divides k by GCD_IS_GREATEST_COMMON_DIVISOR 2328 ==> d divides n by DIVIDES_TRANS 2329 so d divides 1 by GCD_IS_GREATEST_COMMON_DIVISOR, coprime n k 2330 ==> d = 1 by DIVIDES_ONE 2331*) 2332val coprime_factor_coprime = store_thm( 2333 "coprime_factor_coprime", 2334 ``!m n. m divides n ==> !k. coprime n k ==> coprime m k``, 2335 rpt strip_tac >> 2336 qabbrev_tac `d = gcd m k` >> 2337 `d divides m /\ d divides k` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >> 2338 `d divides n` by metis_tac[DIVIDES_TRANS] >> 2339 `d divides 1` by metis_tac[GCD_IS_GREATEST_COMMON_DIVISOR] >> 2340 rw[GSYM DIVIDES_ONE]); 2341 2342(* Theorem: prime p /\ ~(p divides n) ==> coprime p n *) 2343(* Proof: 2344 Since divides p 0, so n <> 0. by ALL_DIVIDES_0 2345 If n = 1, certainly coprime p n by GCD_1 2346 If n <> 1, 2347 Let gcd p n = d. 2348 Since d divides p by GCD_IS_GREATEST_COMMON_DIVISOR 2349 and prime p by given 2350 so d = 1 or d = p by prime_def 2351 but d <> p by divides_iff_gcd_fix 2352 Hence d = 1, or coprime p n. 2353*) 2354val prime_not_divides_is_coprime = store_thm( 2355 "prime_not_divides_is_coprime", 2356 ``!n p. prime p /\ ~(p divides n) ==> coprime p n``, 2357 rpt strip_tac >> 2358 `n <> 0` by metis_tac[ALL_DIVIDES_0] >> 2359 Cases_on `n = 1` >- 2360 rw[] >> 2361 `0 < p` by rw[PRIME_POS] >> 2362 `p <> 0` by decide_tac >> 2363 metis_tac[prime_def, divides_iff_gcd_fix, GCD_IS_GREATEST_COMMON_DIVISOR]); 2364 2365(* Theorem: prime p /\ ~(coprime p n) ==> p divides n *) 2366(* Proof: 2367 Let d = gcd p n. 2368 Then d divides p by GCD_IS_GREATEST_COMMON_DIVISOR 2369 ==> d = p by prime_def 2370 Thus p divides n by divides_iff_gcd_fix 2371*) 2372val prime_not_coprime_divides = store_thm( 2373 "prime_not_coprime_divides", 2374 ``!n p. prime p /\ ~(coprime p n) ==> p divides n``, 2375 rpt strip_tac >> 2376 qabbrev_tac `d = gcd p n` >> 2377 `d divides p` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >> 2378 `d = p` by metis_tac[prime_def] >> 2379 rw[divides_iff_gcd_fix]); 2380 2381(* This is just the inverse of prime_not_divides_is_coprime *) 2382val prime_not_coprime_divides = store_thm( 2383 "prime_not_coprime_divides", 2384 ``!n p. prime p /\ ~(coprime p n) ==> p divides n``, 2385 metis_tac[prime_not_divides_is_coprime]); 2386 2387(* Theorem: 1 < n /\ prime p /\ p divides n ==> !k. coprime n k ==> coprime p k *) 2388(* Proof: 2389 Since coprime n k /\ p divides n 2390 ==> ~(p divides k) by coprime_factor_not_divides 2391 Then prime p /\ ~(p divides k) 2392 ==> coprime p k by prime_not_divides_is_coprime 2393*) 2394val coprime_prime_factor_coprime = store_thm( 2395 "coprime_prime_factor_coprime", 2396 ``!n p. 1 < n /\ prime p /\ p divides n ==> !k. coprime n k ==> coprime p k``, 2397 metis_tac[coprime_factor_not_divides, prime_not_divides_is_coprime, ONE_LT_PRIME]); 2398 2399(* This is better: 2400coprime_factor_coprime 2401|- !m n. m divides n ==> !k. coprime n k ==> coprime m k 2402*) 2403 2404(* Theorem: 1 < n ==> (!j. 0 < j /\ j <= m ==> coprime n j) ==> m < n *) 2405(* Proof: 2406 By contradiction. Suppose n <= m. 2407 Since 1 < n means 0 < n and n <> 1, 2408 The implication shows 2409 coprime n n, or n = 1 by notation 2410 But gcd n n = n by GCD_REF 2411 This contradicts n <> 1. 2412*) 2413val coprime_all_le_imp_lt = store_thm( 2414 "coprime_all_le_imp_lt", 2415 ``!n. 1 < n ==> !m. (!j. 0 < j /\ j <= m ==> coprime n j) ==> m < n``, 2416 spose_not_then strip_assume_tac >> 2417 `n <= m` by decide_tac >> 2418 `0 < n /\ n <> 1` by decide_tac >> 2419 metis_tac[GCD_REF]); 2420 2421(* Theorem: (!j. 1 < j /\ j <= m ==> ~(j divides n)) <=> (!j. 1 < j /\ j <= m ==> coprime j n) *) 2422(* Proof: 2423 If part: (!j. 1 < j /\ j <= m ==> ~(j divides n)) /\ 1 < j /\ j <= m ==> coprime j n 2424 Let d = gcd j n. 2425 Then d divides j /\ d divides n by GCD_IS_GREATEST_COMMON_DIVISOR 2426 Now 1 < j ==> 0 < j /\ j <> 0 2427 so d <= j by DIVIDES_LE, 0 < j 2428 and d <> 0 by GCD_EQ_0, j <> 0 2429 By contradiction, suppose d <> 1. 2430 Then 1 < d /\ d <= m by d <> 1, d <= j /\ j <= m 2431 so ~(d divides n), a contradiction by implication 2432 2433 Only-if part: (!j. 1 < j /\ j <= m ==> coprime j n) /\ 1 < j /\ j <= m ==> ~(j divides n) 2434 Since coprime j n by implication 2435 so ~(j divides n) by coprime_not_divides 2436*) 2437val coprime_condition = store_thm( 2438 "coprime_condition", 2439 ``!m n. (!j. 1 < j /\ j <= m ==> ~(j divides n)) <=> (!j. 1 < j /\ j <= m ==> coprime j n)``, 2440 rw[EQ_IMP_THM] >| [ 2441 spose_not_then strip_assume_tac >> 2442 qabbrev_tac `d = gcd j n` >> 2443 `d divides j /\ d divides n` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >> 2444 `0 < j /\ j <> 0` by decide_tac >> 2445 `d <= j` by rw[DIVIDES_LE] >> 2446 `d <> 0` by metis_tac[GCD_EQ_0] >> 2447 `1 < d /\ d <= m` by decide_tac >> 2448 metis_tac[], 2449 metis_tac[coprime_not_divides] 2450 ]); 2451 2452(* Note: 2453The above is the generalization of this observation: 2454- a prime n has all 1 < j < n coprime to n. Therefore, 2455- a number n has all 1 < j < m coprime to n, where m is the first non-trivial factor of n. 2456 Of course, the first non-trivial factor of n must be a prime. 2457*) 2458 2459(* Theorem: 1 < m /\ (!j. 1 < j /\ j <= m ==> ~(j divides n)) ==> coprime m n *) 2460(* Proof: by coprime_condition, taking j = m. *) 2461val coprime_by_le_not_divides = store_thm( 2462 "coprime_by_le_not_divides", 2463 ``!m n. 1 < m /\ (!j. 1 < j /\ j <= m ==> ~(j divides n)) ==> coprime m n``, 2464 rw[coprime_condition]); 2465 2466(* Theorem: prime n ==> !m. 0 < m /\ m < n ==> coprime n m *) 2467(* Proof: 2468 By contradiction. Let d = gcd n m, and d <> 1. 2469 Since prime n, 0 < n by PRIME_POS 2470 Thus d divides n, and d m divides by GCD_IS_GREATEST_COMMON_DIVISOR, n <> 0, m <> 0. 2471 ==> d = n by prime_def, d <> 1. 2472 ==> n divides m by d divides m 2473 ==> n <= m by DIVIDES_LE 2474 which contradicts m < n. 2475*) 2476val prime_coprime_all_lt = store_thm( 2477 "prime_coprime_all_lt", 2478 ``!n. prime n ==> !m. 0 < m /\ m < n ==> coprime n m``, 2479 rpt strip_tac >> 2480 spose_not_then strip_assume_tac >> 2481 qabbrev_tac `d = gcd n m` >> 2482 `0 < n` by rw[PRIME_POS] >> 2483 `n <> 0 /\ m <> 0` by decide_tac >> 2484 `d divides n /\ d divides m` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >> 2485 `d = n` by metis_tac[prime_def] >> 2486 `n <= m` by rw[DIVIDES_LE] >> 2487 decide_tac); 2488 2489(* Theorem: prime n /\ m < n ==> (!j. 0 < j /\ j <= m ==> coprime n j) *) 2490(* Proof: 2491 Since m < n, all j < n. 2492 Hence true by prime_coprime_all_lt 2493*) 2494val prime_coprime_all_less = store_thm( 2495 "prime_coprime_all_less", 2496 ``!m n. prime n /\ m < n ==> (!j. 0 < j /\ j <= m ==> coprime n j)``, 2497 rpt strip_tac >> 2498 `j < n` by decide_tac >> 2499 rw[prime_coprime_all_lt]); 2500 2501(* Theorem: prime n <=> 1 < n /\ (!j. 0 < j /\ j < n ==> coprime n j)) *) 2502(* Proof: 2503 If part: prime n ==> 1 < n /\ !j. 0 < j /\ j < n ==> coprime n j 2504 (1) prime n ==> 1 < n by ONE_LT_PRIME 2505 (2) prime n /\ 0 < j /\ j < n ==> coprime n j by prime_coprime_all_lt 2506 Only-if part: !j. 0 < j /\ j < n ==> coprime n j ==> prime n 2507 By contradiction, assume ~prime n. 2508 Now, 1 < n /\ ~prime n 2509 ==> ?p. prime p /\ p < n /\ p divides n by PRIME_FACTOR_PROPER 2510 and prime p ==> 0 < p and 1 < p by PRIME_POS, ONE_LT_PRIME 2511 Hence ~coprime p n by coprime_not_divides, 1 < p 2512 But 0 < p < n ==> coprime n p by given implication 2513 This is a contradiction by coprime_sym 2514*) 2515val prime_iff_coprime_all_lt = store_thm( 2516 "prime_iff_coprime_all_lt", 2517 ``!n. prime n <=> 1 < n /\ (!j. 0 < j /\ j < n ==> coprime n j)``, 2518 rw[EQ_IMP_THM, ONE_LT_PRIME] >- 2519 rw[prime_coprime_all_lt] >> 2520 spose_not_then strip_assume_tac >> 2521 `?p. prime p /\ p < n /\ p divides n` by rw[PRIME_FACTOR_PROPER] >> 2522 `0 < p` by rw[PRIME_POS] >> 2523 `1 < p` by rw[ONE_LT_PRIME] >> 2524 metis_tac[coprime_not_divides, coprime_sym]); 2525 2526(* Theorem: prime n <=> (1 < n /\ (!j. 1 < j /\ j < n ==> ~(j divides n))) *) 2527(* Proof: 2528 If part: prime n ==> (1 < n /\ (!j. 1 < j /\ j < n ==> ~(j divides n))) 2529 Note 1 < n by ONE_LT_PRIME 2530 By contradiction, suppose j divides n. 2531 Then j = 1 or j = n by prime_def 2532 This contradicts 1 < j /\ j < n. 2533 Only-if part: (1 < n /\ (!j. 1 < j /\ j < n ==> ~(j divides n))) ==> prime n 2534 This is to show: 2535 !b. b divides n ==> b = 1 or b = n by prime_def 2536 Since 1 < n, so n <> 0 by arithmetic 2537 Thus b <= n by DIVIDES_LE 2538 and b <> 0 by ZERO_DIVIDES 2539 By contradiction, suppose b <> 1 and b <> n, but b divides n. 2540 Then 1 < b /\ b < n by above 2541 giving ~(b divides n) by implication 2542 This contradicts with b divides n. 2543*) 2544val prime_iff_no_proper_factor = store_thm( 2545 "prime_iff_no_proper_factor", 2546 ``!n. prime n <=> (1 < n /\ (!j. 1 < j /\ j < n ==> ~(j divides n)))``, 2547 rw_tac std_ss[EQ_IMP_THM] >- 2548 rw[ONE_LT_PRIME] >- 2549 metis_tac[prime_def, LESS_NOT_EQ] >> 2550 rw[prime_def] >> 2551 `b <= n` by rw[DIVIDES_LE] >> 2552 `n <> 0` by decide_tac >> 2553 `b <> 0` by metis_tac[ZERO_DIVIDES] >> 2554 spose_not_then strip_assume_tac >> 2555 `1 < b /\ b < n` by decide_tac >> 2556 metis_tac[]); 2557 2558(* Theorem: !n. ?p. prime p /\ n < p *) 2559(* Proof: 2560 Since ?i. n < PRIMES i by NEXT_LARGER_PRIME 2561 and prime (PRIMES i) by primePRIMES 2562 Take p = PRIMES i. 2563*) 2564val prime_always_bigger = store_thm( 2565 "prime_always_bigger", 2566 ``!n. ?p. prime p /\ n < p``, 2567 metis_tac[NEXT_LARGER_PRIME, primePRIMES]); 2568 2569(* Theorem: n divides m ==> coprime n (SUC m) *) 2570(* Proof: 2571 If n = 0, 2572 then m = 0 by ZERO_DIVIDES 2573 gcd 0 (SUC 0) 2574 = SUC 0 by GCD_0L 2575 = 1 by ONE 2576 If n = 1, 2577 gcd 1 (SUC m) = 1 by GCD_1 2578 If n <> 0, 2579 gcd n (SUC m) 2580 = gcd ((SUC m) MOD n) n by GCD_EFFICIENTLY 2581 = gcd 1 n by n divides m 2582 = 1 by GCD_1 2583*) 2584val divides_imp_coprime_with_successor = store_thm( 2585 "divides_imp_coprime_with_successor", 2586 ``!m n. n divides m ==> coprime n (SUC m)``, 2587 rpt strip_tac >> 2588 Cases_on `n = 0` >- 2589 rw[GSYM ZERO_DIVIDES] >> 2590 Cases_on `n = 1` >- 2591 rw[] >> 2592 `0 < n /\ 1 < n` by decide_tac >> 2593 `m MOD n = 0` by rw[GSYM DIVIDES_MOD_0] >> 2594 `(SUC m) MOD n = (m + 1) MOD n` by rw[ADD1] >> 2595 `_ = (m MOD n + 1 MOD n) MOD n` by rw[MOD_PLUS] >> 2596 `_ = (0 + 1) MOD n` by rw[ONE_MOD] >> 2597 `_ = 1` by rw[ONE_MOD] >> 2598 metis_tac[GCD_EFFICIENTLY, GCD_1]); 2599 2600(* Note: counter-example for converse: gcd 3 11 = 1, but ~(3 divides 10). *) 2601 2602(* Theorem: 0 < m /\ n divides m ==> coprime n (PRE m) *) 2603(* Proof: 2604 Since n divides m 2605 ==> ?q. m = q * n by divides_def 2606 Also 0 < m means m <> 0, 2607 ==> ?k. m = SUC k by num_CASES 2608 = k + 1 by ADD1 2609 so m - k = 1, k = PRE m. 2610 Let d = gcd n k. 2611 Then d divides n /\ d divides k by GCD_IS_GREATEST_COMMON_DIVISOR 2612 and d divides n ==> d divides m by DIVIDES_MULTIPLE, m = q * n 2613 so d divides (m - k) by DIVIDES_SUB 2614 or d divides 1 by m - k = 1 2615 ==> d = 1 by DIVIDES_ONE 2616*) 2617val divides_imp_coprime_with_predecessor = store_thm( 2618 "divides_imp_coprime_with_predecessor", 2619 ``!m n. 0 < m /\ n divides m ==> coprime n (PRE m)``, 2620 rpt strip_tac >> 2621 `?q. m = q * n` by rw[GSYM divides_def] >> 2622 `m <> 0` by decide_tac >> 2623 `?k. m = k + 1` by metis_tac[num_CASES, ADD1] >> 2624 `(k = PRE m) /\ (m - k = 1)` by decide_tac >> 2625 qabbrev_tac `d = gcd n k` >> 2626 `d divides n /\ d divides k` by rw[GCD_IS_GREATEST_COMMON_DIVISOR, Abbr`d`] >> 2627 `d divides m` by rw[DIVIDES_MULTIPLE] >> 2628 `d divides (m - k)` by rw[DIVIDES_SUB] >> 2629 metis_tac[DIVIDES_ONE]); 2630 2631(* Theorem: coprime p n ==> (gcd (p * m) n = gcd m n) *) 2632(* Proof: 2633 Note coprime p n means coprime n p by GCD_SYM 2634 gcd (p * m) n 2635 = gcd n (p * m) by GCD_SYM 2636 = gcd n p by GCD_CANCEL_MULT 2637*) 2638val gcd_coprime_cancel = store_thm( 2639 "gcd_coprime_cancel", 2640 ``!m n p. coprime p n ==> (gcd (p * m) n = gcd m n)``, 2641 rw[GCD_CANCEL_MULT, GCD_SYM]); 2642 2643(* The following is a direct, but tricky, proof of the above result *) 2644 2645(* Theorem: coprime p n ==> (gcd (p * m) n = gcd m n) *) 2646(* Proof: 2647 gcd (p * m) n 2648 = gcd (p * m) (n * 1) by MULT_RIGHT_1 2649 = gcd (p * m) (n * (gcd m 1)) by GCD_1 2650 = gcd (p * m) (gcd (n * m) n) by GCD_COMMON_FACTOR 2651 = gcd (gcd (p * m) (n * m)) n by GCD_ASSOC 2652 = gcd (m * (gcd p n)) n by GCD_COMMON_FACTOR, MULT_COMM 2653 = gcd (m * 1) n by coprime p n 2654 = gcd m n by MULT_RIGHT_1 2655 2656 Simple proof of GCD_CANCEL_MULT: 2657 (a*c, b) = (a*c , b*1) = (a * c, b * (c, 1)) = (a * c, b * c, b) = ((a, b) * c, b) = (c, b) since (a,b) = 1. 2658*) 2659val gcd_coprime_cancel = store_thm( 2660 "gcd_coprime_cancel", 2661 ``!m n p. coprime p n ==> (gcd (p * m) n = gcd m n)``, 2662 rpt strip_tac >> 2663 `gcd (p * m) n = gcd (p * m) (n * (gcd m 1))` by rw[GCD_1] >> 2664 `_ = gcd (p * m) (gcd (n * m) n)` by rw[GSYM GCD_COMMON_FACTOR] >> 2665 `_ = gcd (gcd (p * m) (n * m)) n` by rw[GCD_ASSOC] >> 2666 `_ = gcd m n` by rw[GCD_COMMON_FACTOR, MULT_COMM] >> 2667 rw[]); 2668 2669(* Theorem: prime p /\ prime q /\ p <> q ==> coprime p q *) 2670(* Proof: 2671 Let d = gcd p q. 2672 By contradiction, suppose d <> 1. 2673 Then d divides p /\ d divides q by GCD_PROPERTY 2674 so d = 1 or d = p by prime_def 2675 and d = 1 or d = q by prime_def 2676 But p <> q by given 2677 so d = 1, contradicts d <> 1. 2678*) 2679val primes_coprime = store_thm( 2680 "primes_coprime", 2681 ``!p q. prime p /\ prime q /\ p <> q ==> coprime p q``, 2682 spose_not_then strip_assume_tac >> 2683 qabbrev_tac `d = gcd p q` >> 2684 `d divides p /\ d divides q` by metis_tac[GCD_PROPERTY] >> 2685 metis_tac[prime_def]); 2686 2687(* Theorem: FINITE s ==> !x. x NOTIN s /\ (!z. z IN s ==> coprime x z) ==> coprime x (PROD_SET s) *) 2688(* Proof: 2689 By finite induction on s. 2690 Base: coprime x (PROD_SET {}) 2691 Note PROD_SET {} = 1 by PROD_SET_EMPTY 2692 and coprime x 1 = T by GCD_1 2693 Step: !x. x NOTIN s /\ (!z. z IN s ==> coprime x z) ==> coprime x (PROD_SET s) ==> 2694 e NOTIN s /\ x NOTIN e INSERT s /\ !z. z IN e INSERT s ==> coprime x z ==> 2695 coprime x (PROD_SET (e INSERT s)) 2696 Note coprime x e by IN_INSERT 2697 and coprime x (PROD_SET s) by induction hypothesis 2698 Thus coprime x (e * PROD_SET s) by coprime_product_coprime_sym 2699 or coprime x PROD_SET (e INSERT s) by PROD_SET_INSERT 2700*) 2701val every_coprime_prod_set_coprime = store_thm( 2702 "every_coprime_prod_set_coprime", 2703 ``!s. FINITE s ==> !x. x NOTIN s /\ (!z. z IN s ==> coprime x z) ==> coprime x (PROD_SET s)``, 2704 Induct_on `FINITE` >> 2705 rpt strip_tac >- 2706 rw[PROD_SET_EMPTY] >> 2707 fs[] >> 2708 rw[PROD_SET_INSERT, coprime_product_coprime_sym]); 2709 2710(* ------------------------------------------------------------------------- *) 2711(* Pairwise Coprime Property *) 2712(* ------------------------------------------------------------------------- *) 2713 2714(* Overload pairwise coprime set *) 2715val _ = overload_on("PAIRWISE_COPRIME", ``\s. !x y. x IN s /\ y IN s /\ x <> y ==> coprime x y``); 2716 2717(* Theorem: e NOTIN s /\ PAIRWISE_COPRIME (e INSERT s) ==> 2718 (!x. x IN s ==> coprime e x) /\ PAIRWISE_COPRIME s *) 2719(* Proof: by IN_INSERT *) 2720val pairwise_coprime_insert = store_thm( 2721 "pairwise_coprime_insert", 2722 ``!s e. e NOTIN s /\ PAIRWISE_COPRIME (e INSERT s) ==> 2723 (!x. x IN s ==> coprime e x) /\ PAIRWISE_COPRIME s``, 2724 metis_tac[IN_INSERT]); 2725 2726(* Theorem: FINITE s /\ PAIRWISE_COPRIME s ==> 2727 !t. t SUBSET s ==> (PROD_SET t) divides (PROD_SET s) *) 2728(* Proof: 2729 Note FINITE t by SUBSET_FINITE 2730 By finite induction on t. 2731 Base case: PROD_SET {} divides PROD_SET s 2732 Note PROD_SET {} = 1 by PROD_SET_EMPTY 2733 and 1 divides (PROD_SET s) by ONE_DIVIDES_ALL 2734 Step case: t SUBSET s ==> PROD_SET t divides PROD_SET s ==> 2735 e NOTIN t /\ e INSERT t SUBSET s ==> PROD_SET (e INSERT t) divides PROD_SET s 2736 Let m = PROD_SET s. 2737 Note e IN s /\ t SUBSET s by INSERT_SUBSET 2738 Thus e divides m by PROD_SET_ELEMENT_DIVIDES 2739 and (PROD_SET t) divides m by induction hypothesis 2740 Also coprime e (PROD_SET t) by every_coprime_prod_set_coprime, SUBSET_DEF 2741 Note PROD_SET (e INSERT t) = e * PROD_SET t by PROD_SET_INSERT 2742 ==> e * PROD_SET t divides m by coprime_product_divides 2743*) 2744val pairwise_coprime_prod_set_subset_divides = store_thm( 2745 "pairwise_coprime_prod_set_subset_divides", 2746 ``!s. FINITE s /\ PAIRWISE_COPRIME s ==> 2747 !t. t SUBSET s ==> (PROD_SET t) divides (PROD_SET s)``, 2748 rpt strip_tac >> 2749 `FINITE t` by metis_tac[SUBSET_FINITE] >> 2750 qpat_x_assum `t SUBSET s` mp_tac >> 2751 qpat_x_assum `FINITE t` mp_tac >> 2752 qid_spec_tac `t` >> 2753 Induct_on `FINITE` >> 2754 rpt strip_tac >- 2755 rw[PROD_SET_EMPTY] >> 2756 fs[] >> 2757 `e divides PROD_SET s` by rw[PROD_SET_ELEMENT_DIVIDES] >> 2758 `coprime e (PROD_SET t)` by prove_tac[every_coprime_prod_set_coprime, SUBSET_DEF] >> 2759 rw[PROD_SET_INSERT, coprime_product_divides]); 2760 2761(* Theorem: FINITE s /\ PAIRWISE_COPRIME s ==> 2762 !u v. (s = u UNION v) /\ DISJOINT u v ==> coprime (PROD_SET u) (PROD_SET v) *) 2763(* Proof: 2764 By finite induction on s. 2765 Base: {} = u UNION v ==> coprime (PROD_SET u) (PROD_SET v) 2766 Note u = {} and v = {} by EMPTY_UNION 2767 and PROD_SET {} = 1 by PROD_SET_EMPTY 2768 Hence true by GCD_1 2769 Step: PAIRWISE_COPRIME s ==> 2770 !u v. (s = u UNION v) /\ DISJOINT u v ==> coprime (PROD_SET u) (PROD_SET v) ==> 2771 e NOTIN s /\ e INSERT s = u UNION v ==> coprime (PROD_SET u) (PROD_SET v) 2772 Note (!x. x IN s ==> coprime e x) /\ 2773 PAIRWISE_COPRIME s by IN_INSERT 2774 Note e IN u \/ e IN v by IN_INSERT, IN_UNION 2775 If e IN u, 2776 Then e NOTIN v by IN_DISJOINT 2777 Let w = u DELETE e. 2778 Then e NOTIN w by IN_DELETE 2779 and u = e INSERT w by INSERT_DELETE 2780 Note s = w UNION v by EXTENSION, IN_INSERT, IN_UNION 2781 ==> FINITE w by FINITE_UNION 2782 and DISJOINT w v by DISJOINT_INSERT 2783 2784 Note coprime (PROD_SET w) (PROD_SET v) by induction hypothesis 2785 and !x. x IN v ==> coprime e x by v SUBSET s 2786 Also FINITE v by FINITE_UNION 2787 so coprime e (PROD_SET v) by every_coprime_prod_set_coprime, FINITE v 2788 ==> coprime (e * PROD_SET w) PROD_SET v by coprime_product_coprime 2789 or coprime PROD_SET (e INSERT w) PROD_SET v by PROD_SET_INSERT 2790 = coprime PROD_SET u PROD_SET v by above 2791 2792 Similarly for e IN v. 2793*) 2794val pairwise_coprime_partition_coprime = store_thm( 2795 "pairwise_coprime_partition_coprime", 2796 ``!s. FINITE s /\ PAIRWISE_COPRIME s ==> 2797 !u v. (s = u UNION v) /\ DISJOINT u v ==> coprime (PROD_SET u) (PROD_SET v)``, 2798 ntac 2 strip_tac >> 2799 qpat_x_assum `PAIRWISE_COPRIME s` mp_tac >> 2800 qpat_x_assum `FINITE s` mp_tac >> 2801 qid_spec_tac `s` >> 2802 Induct_on `FINITE` >> 2803 rpt strip_tac >- 2804 fs[PROD_SET_EMPTY] >> 2805 `(!x. x IN s ==> coprime e x) /\ PAIRWISE_COPRIME s` by metis_tac[IN_INSERT] >> 2806 `e IN u \/ e IN v` by metis_tac[IN_INSERT, IN_UNION] >| [ 2807 qabbrev_tac `w = u DELETE e` >> 2808 `u = e INSERT w` by rw[Abbr`w`] >> 2809 `e NOTIN w` by rw[Abbr`w`] >> 2810 `e NOTIN v` by metis_tac[IN_DISJOINT] >> 2811 `s = w UNION v` by 2812 (rw[EXTENSION] >> 2813 metis_tac[IN_INSERT, IN_UNION]) >> 2814 `FINITE w` by metis_tac[FINITE_UNION] >> 2815 `DISJOINT w v` by metis_tac[DISJOINT_INSERT] >> 2816 `coprime (PROD_SET w) (PROD_SET v)` by rw[] >> 2817 `(!x. x IN v ==> coprime e x)` by rw[] >> 2818 `FINITE v` by metis_tac[FINITE_UNION] >> 2819 `coprime e (PROD_SET v)` by rw[every_coprime_prod_set_coprime] >> 2820 metis_tac[coprime_product_coprime, PROD_SET_INSERT], 2821 qabbrev_tac `w = v DELETE e` >> 2822 `v = e INSERT w` by rw[Abbr`w`] >> 2823 `e NOTIN w` by rw[Abbr`w`] >> 2824 `e NOTIN u` by metis_tac[IN_DISJOINT] >> 2825 `s = u UNION w` by 2826 (rw[EXTENSION] >> 2827 metis_tac[IN_INSERT, IN_UNION]) >> 2828 `FINITE w` by metis_tac[FINITE_UNION] >> 2829 `DISJOINT u w` by metis_tac[DISJOINT_INSERT, DISJOINT_SYM] >> 2830 `coprime (PROD_SET u) (PROD_SET w)` by rw[] >> 2831 `(!x. x IN u ==> coprime e x)` by rw[] >> 2832 `FINITE u` by metis_tac[FINITE_UNION] >> 2833 `coprime (PROD_SET u) e` by rw[every_coprime_prod_set_coprime, coprime_sym] >> 2834 metis_tac[coprime_product_coprime_sym, PROD_SET_INSERT] 2835 ]); 2836 2837(* Theorem: FINITE s /\ PAIRWISE_COPRIME s ==> !u v. (s = u UNION v) /\ DISJOINT u v ==> 2838 (PROD_SET s = PROD_SET u * PROD_SET v) /\ (coprime (PROD_SET u) (PROD_SET v)) *) 2839(* Proof: by PROD_SET_PRODUCT_BY_PARTITION, pairwise_coprime_partition_coprime *) 2840val pairwise_coprime_prod_set_partition = store_thm( 2841 "pairwise_coprime_prod_set_partition", 2842 ``!s. FINITE s /\ PAIRWISE_COPRIME s ==> !u v. (s = u UNION v) /\ DISJOINT u v ==> 2843 (PROD_SET s = PROD_SET u * PROD_SET v) /\ (coprime (PROD_SET u) (PROD_SET v))``, 2844 metis_tac[PROD_SET_PRODUCT_BY_PARTITION, pairwise_coprime_partition_coprime]); 2845 2846(* ------------------------------------------------------------------------- *) 2847(* GCD divisibility condition of Power Predecessors *) 2848(* ------------------------------------------------------------------------- *) 2849 2850(* Theorem: 0 < t /\ m <= n ==> 2851 (t ** n - 1 = t ** (n - m) * (t ** m - 1) + (t ** (n - m) - 1)) *) 2852(* Proof: 2853 Note !n. 1 <= t ** n by ONE_LE_EXP, 0 < t, [1] 2854 2855 Claim: t ** (n - m) - 1 <= t ** n - 1, because: 2856 Proof: Note n - m <= n always 2857 so t ** (n - m) <= t ** n by EXP_BASE_LEQ_MONO_IMP, 0 < t 2858 Now 1 <= t ** (n - m) and 2859 1 <= t ** n by [1] 2860 Hence t ** (n - m) - 1 <= t ** n - 1. 2861 2862 t ** (n - m) * (t ** m - 1) + t ** (n - m) - 1 2863 = (t ** (n - m) * t ** m - t ** (n - m)) + t ** (n - m) - 1 by LEFT_SUB_DISTRIB 2864 = (t ** (n - m + m) - t ** (n - m)) + t ** (n - m) - 1 by EXP_ADD 2865 = (t ** n - t ** (n - m)) + t ** (n - m) - 1 by SUB_ADD, m <= n 2866 = (t ** n - (t ** (n - m) - 1 + 1)) + t ** (n - m) - 1 by SUB_ADD, 1 <= t ** (n - m) 2867 = (t ** n - (1 + (t ** (n - m) - 1))) + t ** (n - m) - 1 by ADD_COMM 2868 = (t ** n - 1 - (t ** (n - m) - 1)) + t ** (n - m) - 1 by SUB_PLUS, no condition 2869 = t ** n - 1 by SUB_ADD, t ** (n - m) - 1 <= t ** n - 1 2870*) 2871val power_predecessor_division_eqn = store_thm( 2872 "power_predecessor_division_eqn", 2873 ``!t m n. 0 < t /\ m <= n ==> 2874 (t ** n - 1 = t ** (n - m) * (t ** m - 1) + (t ** (n - m) - 1))``, 2875 rpt strip_tac >> 2876 `1 <= t ** n /\ 1 <= t ** (n - m)` by rw[ONE_LE_EXP] >> 2877 `n - m <= n` by decide_tac >> 2878 `t ** (n - m) <= t ** n` by rw[EXP_BASE_LEQ_MONO_IMP] >> 2879 `t ** (n - m) - 1 <= t ** n - 1` by decide_tac >> 2880 qabbrev_tac `z = t ** (n - m) - 1` >> 2881 `t ** (n - m) * (t ** m - 1) + z = 2882 t ** (n - m) * t ** m - t ** (n - m) + z` by decide_tac >> 2883 `_ = t ** (n - m + m) - t ** (n - m) + z` by rw_tac std_ss[EXP_ADD] >> 2884 `_ = t ** n - t ** (n - m) + z` by rw_tac std_ss[SUB_ADD] >> 2885 `_ = t ** n - (z + 1) + z` by rw_tac std_ss[SUB_ADD, Abbr`z`] >> 2886 `_ = t ** n + z - (z + 1)` by decide_tac >> 2887 `_ = t ** n - 1` by decide_tac >> 2888 decide_tac); 2889 2890(* This shows the pattern: 2891 1000000 so 9999999999 = 1000000 * 9999 + 999999 2892 ------------ or (b ** 10 - 1) = b ** 6 * (b ** 4 - 1) + (b ** 6 - 1) 2893 9999 | 9999999999 where b = 10. 2894 9999 2895 ---------- 2896 999999 2897*) 2898 2899(* Theorem: 0 < t /\ m <= n ==> 2900 (t ** n - 1 - t ** (n - m) * (t ** m - 1) = t ** (n - m) - 1) *) 2901(* Proof: by power_predecessor_division_eqn *) 2902val power_predecessor_division_alt = store_thm( 2903 "power_predecessor_division_alt", 2904 ``!t m n. 0 < t /\ m <= n ==> 2905 (t ** n - 1 - t ** (n - m) * (t ** m - 1) = t ** (n - m) - 1)``, 2906 rpt strip_tac >> 2907 imp_res_tac power_predecessor_division_eqn >> 2908 fs[]); 2909 2910(* Theorem: m < n ==> (gcd (t ** n - 1) (t ** m - 1) = gcd ((t ** m - 1)) (t ** (n - m) - 1)) *) 2911(* Proof: 2912 Case t = 0, 2913 If n = 0, t ** 0 = 1 by ZERO_EXP 2914 LHS = gcd 0 x = 0 by GCD_0L 2915 = gcd 0 y = RHS by ZERO_EXP 2916 If n <> 0, 0 ** n = 0 by ZERO_EXP 2917 LHS = gcd (0 - 1) x 2918 = gcd 0 x = 0 by GCD_0L 2919 = gcd 0 y = RHS by ZERO_EXP 2920 Case t <> 0, 2921 Note t ** n - 1 = t ** (n - m) * (t ** m - 1) + (t ** (n - m) - 1) 2922 by power_predecessor_division_eqn 2923 so t ** (n - m) * (t ** m - 1) <= t ** n - 1 by above, [1] 2924 and t ** n - 1 - t ** (n - m) * (t ** m - 1) = t ** (n - m) - 1, [2] 2925 gcd (t ** n - 1) (t ** m - 1) 2926 = gcd (t ** m - 1) (t ** n - 1) by GCD_SYM 2927 = gcd (t ** m - 1) ((t ** n - 1) - t ** (n - m) * (t ** m - 1)) 2928 by GCD_SUB_MULTIPLE, [1] 2929 = gcd (t ** m - 1)) (t ** (n - m) - 1) by [2] 2930*) 2931val power_predecessor_gcd_reduction = store_thm( 2932 "power_predecessor_gcd_reduction", 2933 ``!t n m. m <= n ==> (gcd (t ** n - 1) (t ** m - 1) = gcd ((t ** m - 1)) (t ** (n - m) - 1))``, 2934 rpt strip_tac >> 2935 Cases_on `t = 0` >- 2936 rw[ZERO_EXP] >> 2937 `t ** n - 1 = t ** (n - m) * (t ** m - 1) + (t ** (n - m) - 1)` by rw[power_predecessor_division_eqn] >> 2938 `t ** n - 1 - t ** (n - m) * (t ** m - 1) = t ** (n - m) - 1` by fs[] >> 2939 `gcd (t ** n - 1) (t ** m - 1) = gcd (t ** m - 1) (t ** n - 1)` by rw_tac std_ss[GCD_SYM] >> 2940 `_ = gcd (t ** m - 1) ((t ** n - 1) - t ** (n - m) * (t ** m - 1))` by rw_tac std_ss[GCD_SUB_MULTIPLE] >> 2941 rw_tac std_ss[]); 2942 2943(* Theorem: gcd (t ** n - 1) (t ** m - 1) = t ** (gcd n m) - 1 *) 2944(* Proof: 2945 By complete induction on (n + m): 2946 Induction hypothesis: !m'. m' < n + m ==> 2947 !n m. (m' = n + m) ==> (gcd (t ** n - 1) (t ** m - 1) = t ** gcd n m - 1) 2948 Idea: if 0 < m, n < n + m. Put last n = m, m = n - m. That is m' = m + (n - m) = n. 2949 Also if 0 < n, m < n + m. Put last n = n, m = m - n. That is m' = n + (m - n) = m. 2950 2951 Thus to apply induction hypothesis, need 0 < n or 0 < m. 2952 So take care of these special cases first. 2953 2954 Case: n = 0 ==> gcd (t ** n - 1) (t ** m - 1) = t ** gcd n m - 1 2955 LHS = gcd (t ** 0 - 1) (t ** m - 1) 2956 = gcd 0 (t ** m - 1) by EXP 2957 = t ** m - 1 by GCD_0L 2958 = t ** (gcd 0 m) - 1 = RHS by GCD_0L 2959 Case: m = 0 ==> gcd (t ** n - 1) (t ** m - 1) = t ** gcd n m - 1 2960 LHS = gcd (t ** n - 1) (t ** 0 - 1) 2961 = gcd (t ** n - 1) 0 by EXP 2962 = t ** n - 1 by GCD_0R 2963 = t ** (gcd n 0) - 1 = RHS by GCD_0R 2964 2965 Case: m <> 0 /\ n <> 0 ==> gcd (t ** n - 1) (t ** m - 1) = t ** gcd n m - 1 2966 That is, 0 < n, and 0 < m 2967 also n < n + m, and m < n + m by arithmetic 2968 2969 Use trichotomy of numbers: by LESS_LESS_CASES 2970 Case: n = m /\ m <> 0 /\ n <> 0 ==> gcd (t ** n - 1) (t ** m - 1) = t ** gcd n m - 1 2971 LHS = gcd (t ** m - 1) (t ** m - 1) 2972 = t ** m - 1 by GCD_REF 2973 = t ** (gcd m m) - 1 = RHS by GCD_REF 2974 2975 Case: m < n /\ m <> 0 /\ n <> 0 ==> gcd (t ** n - 1) (t ** m - 1) = t ** gcd n m - 1 2976 Since n < n + m by 0 < m 2977 and m + (n - m) = (n - m) + m by ADD_COMM 2978 = n by SUB_ADD, m <= n 2979 gcd (t ** n - 1) (t ** m - 1) 2980 = gcd ((t ** m - 1)) (t ** (n - m) - 1) by power_predecessor_gcd_reduction 2981 = t ** gcd m (n - m) - 1 by induction hypothesis, m + (n - m) = n 2982 = t ** gcd m n - 1 by GCD_SUB_R, m <= n 2983 = t ** gcd n m - 1 by GCD_SYM 2984 2985 Case: n < m /\ m <> 0 /\ n <> 0 ==> gcd (t ** n - 1) (t ** m - 1) = t ** gcd n m - 1 2986 Since m < n + m by 0 < n 2987 and n + (m - n) = (m - n) + n by ADD_COMM 2988 = m by SUB_ADD, n <= m 2989 gcd (t ** n - 1) (t ** m - 1) 2990 = gcd (t ** m - 1) (t ** n - 1) by GCD_SYM 2991 = gcd ((t ** n - 1)) (t ** (m - n) - 1) by power_predecessor_gcd_reduction 2992 = t ** gcd n (m - n) - 1 by induction hypothesis, n + (m - n) = m 2993 = t ** gcd n m by GCD_SUB_R, n <= m 2994*) 2995val power_predecessor_gcd_identity = store_thm( 2996 "power_predecessor_gcd_identity", 2997 ``!t n m. gcd (t ** n - 1) (t ** m - 1) = t ** (gcd n m) - 1``, 2998 rpt strip_tac >> 2999 completeInduct_on `n + m` >> 3000 rpt strip_tac >> 3001 Cases_on `n = 0` >- 3002 rw[EXP] >> 3003 Cases_on `m = 0` >- 3004 rw[EXP] >> 3005 `(n = m) \/ (m < n) \/ (n < m)` by metis_tac[LESS_LESS_CASES] >- 3006 rw[GCD_REF] >- 3007 (`0 < m /\ n < n + m` by decide_tac >> 3008 `m <= n` by decide_tac >> 3009 `m + (n - m) = n` by metis_tac[SUB_ADD, ADD_COMM] >> 3010 `gcd (t ** n - 1) (t ** m - 1) = gcd ((t ** m - 1)) (t ** (n - m) - 1)` by rw[power_predecessor_gcd_reduction] >> 3011 `_ = t ** gcd m (n - m) - 1` by metis_tac[] >> 3012 metis_tac[GCD_SUB_R, GCD_SYM]) >> 3013 `0 < n /\ m < n + m` by decide_tac >> 3014 `n <= m` by decide_tac >> 3015 `n + (m - n) = m` by metis_tac[SUB_ADD, ADD_COMM] >> 3016 `gcd (t ** n - 1) (t ** m - 1) = gcd ((t ** n - 1)) (t ** (m - n) - 1)` by rw[power_predecessor_gcd_reduction, GCD_SYM] >> 3017 `_ = t ** gcd n (m - n) - 1` by metis_tac[] >> 3018 metis_tac[GCD_SUB_R]); 3019 3020(* Above is the formal proof of the following pattern: 3021 For any base 3022 gcd(999999,9999) = gcd(6 9s, 4 9s) = gcd(6,4) 9s = 2 9s = 99 3023 or 999999 MOD 9999 = (6 9s) MOD (4 9s) = 2 9s = 99 3024 Thus in general, 3025 (m 9s) MOD (n 9s) = (m MOD n) 9s 3026 Repeating the use of Euclidean algorithm then gives: 3027 gcd (m 9s, n 9s) = (gcd m n) 9s 3028 3029Reference: A Mathematical Tapestry (by Jean Pedersen and Peter Hilton) 3030Chapter 4: A number-theory thread -- Folding numbers, a number trick, and some tidbits. 3031*) 3032 3033(* Theorem: 1 < t ==> ((t ** n - 1) divides (t ** m - 1) <=> n divides m) *) 3034(* Proof: 3035 (t ** n - 1) divides (t ** m - 1) 3036 <=> gcd (t ** n - 1) (t ** m - 1) = t ** n - 1 by divides_iff_gcd_fix 3037 <=> t ** (gcd n m) - 1 = t ** n - 1 by power_predecessor_gcd_identity 3038 <=> t ** (gcd n m) = t ** n by PRE_SUB1, INV_PRE_EQ, EXP_POS, 0 < t 3039 <=> gcd n m = n by EXP_BASE_INJECTIVE, 1 < t 3040 <=> n divides m by divides_iff_gcd_fix 3041*) 3042val power_predecessor_divisibility = store_thm( 3043 "power_predecessor_divisibility", 3044 ``!t n m. 1 < t ==> ((t ** n - 1) divides (t ** m - 1) <=> n divides m)``, 3045 rpt strip_tac >> 3046 `0 < t` by decide_tac >> 3047 `!n. 0 < t ** n` by rw[EXP_POS] >> 3048 `!x y. 0 < x /\ 0 < y ==> ((x - 1 = y - 1) <=> (x = y))` by decide_tac >> 3049 `(t ** n - 1) divides (t ** m - 1) <=> ((gcd (t ** n - 1) (t ** m - 1) = t ** n - 1))` by rw[divides_iff_gcd_fix] >> 3050 `_ = (t ** (gcd n m) - 1 = t ** n - 1)` by rw[power_predecessor_gcd_identity] >> 3051 `_ = (t ** (gcd n m) = t ** n)` by rw[] >> 3052 `_ = (gcd n m = n)` by rw[EXP_BASE_INJECTIVE] >> 3053 rw[divides_iff_gcd_fix]); 3054 3055(* This is numerical version of: 3056poly_unity_1_divides |- !r. Ring r /\ #1 <> #0 ==> !n. X - |1| pdivides unity n 3057*) 3058val power_predecessor_divisor = save_thm("power_predecessor_divisor", 3059 power_predecessor_divisibility 3060 |> SPEC ``t:num`` |> SPEC ``1:num`` |> SPEC ``n:num`` 3061 |> SIMP_RULE (srw_ss()) [] |> GEN_ALL); 3062(* val power_predecessor_divisor = |- !t n. 1 < t ==> t - 1 divides t ** n - 1: thm *) 3063(* However, this is too restrictive. *) 3064 3065(* Theorem: t - 1 divides t ** n - 1 *) 3066(* Proof: 3067 If t = 0, 3068 Then t - 1 = 0 by integer subtraction 3069 and t ** n - 1 = 0 by ZERO_EXP, either case of n. 3070 Thus 0 divides 0 by ZERO_DIVIDES 3071 If t = 1, 3072 Then t - 1 = 0 by arithmetic 3073 and t ** n - 1 = 0 by EXP_1 3074 Thus 0 divides 0 by ZERO_DIVIDES 3075 Otherwise, 1 < t 3076 and 1 divides n by ONE_DIVIDES_ALL 3077 ==> t ** 1 - 1 divides t ** n - 1 by power_predecessor_divisibility 3078 or t - 1 divides t ** n - 1 by EXP_1 3079*) 3080val power_predecessor_divisor = store_thm( 3081 "power_predecessor_divisor", 3082 ``!t n. t - 1 divides t ** n - 1``, 3083 rpt strip_tac >> 3084 Cases_on `t = 0` >- 3085 simp[ZERO_EXP] >> 3086 Cases_on `t = 1` >- 3087 simp[] >> 3088 `1 < t` by decide_tac >> 3089 metis_tac[power_predecessor_divisibility, EXP_1, ONE_DIVIDES_ALL]); 3090 3091(* Overload power predecessor *) 3092val _ = overload_on("tops", ``\b:num n. b ** n - 1``); 3093 3094(* 3095 power_predecessor_division_eqn 3096 |- !t m n. 0 < t /\ m <= n ==> tops t n = t ** (n - m) * tops t m + tops t (n - m) 3097 power_predecessor_division_alt 3098 |- !t m n. 0 < t /\ m <= n ==> tops t n - t ** (n - m) * tops t m = tops t (n - m) 3099 power_predecessor_gcd_reduction 3100 |- !t n m. m <= n ==> (gcd (tops t n) (tops t m) = gcd (tops t m) (tops t (n - m))) 3101 power_predecessor_gcd_identity 3102 |- !t n m. gcd (tops t n) (tops t m) = tops t (gcd n m) 3103 power_predecessor_divisibility 3104 |- !t n m. 1 < t ==> (tops t n divides tops t m <=> n divides m) 3105 power_predecessor_divisor 3106 |- !t n. t - 1 divides tops t n 3107*) 3108 3109(* Overload power predecessor base 10 *) 3110val _ = overload_on("nines", ``\n. tops 10 n``); 3111 3112(* Obtain corollaries *) 3113 3114val nines_division_eqn = save_thm("nines_division_eqn", 3115 power_predecessor_division_eqn |> ISPEC ``10`` |> SIMP_RULE (srw_ss()) []); 3116val nines_division_alt = save_thm("nines_division_alt", 3117 power_predecessor_division_alt |> ISPEC ``10`` |> SIMP_RULE (srw_ss()) []); 3118val nines_gcd_reduction = save_thm("nines_gcd_reduction", 3119 power_predecessor_gcd_reduction |> ISPEC ``10``); 3120val nines_gcd_identity = save_thm("nines_gcd_identity", 3121 power_predecessor_gcd_identity |> ISPEC ``10``); 3122val nines_divisibility = save_thm("nines_divisibility", 3123 power_predecessor_divisibility |> ISPEC ``10`` |> SIMP_RULE (srw_ss()) []); 3124val nines_divisor = save_thm("nines_divisor", 3125 power_predecessor_divisor |> ISPEC ``10`` |> SIMP_RULE (srw_ss()) []); 3126(* 3127val nines_division_eqn = 3128 |- !m n. m <= n ==> nines n = 10 ** (n - m) * nines m + nines (n - m): thm 3129val nines_division_alt = 3130 |- !m n. m <= n ==> nines n - 10 ** (n - m) * nines m = nines (n - m): thm 3131val nines_gcd_reduction = 3132 |- !n m. m <= n ==> gcd (nines n) (nines m) = gcd (nines m) (nines (n - m)): thm 3133val nines_gcd_identity = |- !n m. gcd (nines n) (nines m) = nines (gcd n m): thm 3134val nines_divisibility = |- !n m. nines n divides nines m <=> n divides m: thm 3135val nines_divisor = |- !n. 9 divides nines n: thm 3136*) 3137 3138(* ------------------------------------------------------------------------- *) 3139(* GCD involving Powers *) 3140(* ------------------------------------------------------------------------- *) 3141 3142(* Theorem: prime m /\ prime n /\ m divides (n ** k) ==> (m = n) *) 3143(* Proof: 3144 By induction on k. 3145 Base: m divides n ** 0 ==> (m = n) 3146 Since n ** 0 = 1 by EXP 3147 and m divides 1 ==> m = 1 by DIVIDES_ONE 3148 This contradicts 1 < m by ONE_LT_PRIME 3149 Step: m divides n ** k ==> (m = n) ==> m divides n ** SUC k ==> (m = n) 3150 Since n ** SUC k = n * n ** k by EXP 3151 Also m divides n \/ m divides n ** k by P_EUCLIDES 3152 If m divides n, then m = n by prime_divides_only_self 3153 If m divides n ** k, then m = n by induction hypothesis 3154*) 3155val prime_divides_prime_power = store_thm( 3156 "prime_divides_prime_power", 3157 ``!m n k. prime m /\ prime n /\ m divides (n ** k) ==> (m = n)``, 3158 rpt strip_tac >> 3159 Induct_on `k` >| [ 3160 rpt strip_tac >> 3161 `1 < m` by rw[ONE_LT_PRIME] >> 3162 `m = 1` by metis_tac[EXP, DIVIDES_ONE] >> 3163 decide_tac, 3164 metis_tac[EXP, P_EUCLIDES, prime_divides_only_self] 3165 ]); 3166 3167(* This is better than FACTOR_OUT_PRIME *) 3168 3169(* Theorem: 0 < n /\ prime p ==> ?q m. (n = (p ** m) * q) /\ coprime p q *) 3170(* Proof: 3171 If p divides n, 3172 Then ?m. 0 < m /\ p ** m divides n /\ 3173 !k. coprime (p ** k) (n DIV p ** m) by FACTOR_OUT_PRIME 3174 Let q = n DIV (p ** m). 3175 Note 0 < p by PRIME_POS 3176 so 0 < p ** m by EXP_POS, 0 < p 3177 Take this q and m, 3178 Then n = (p ** m) * q by DIVIDES_EQN_COMM 3179 and coprime p q by taking k = 1, EXP_1 3180 3181 If ~(p divides n), 3182 Then coprime p n by prime_not_divides_is_coprime 3183 Let q = n, m = 0. 3184 Then n = 1 * q by EXP, MULT_LEFT_1 3185 and coprime p q. 3186*) 3187val prime_power_factor = store_thm( 3188 "prime_power_factor", 3189 ``!n p. 0 < n /\ prime p ==> ?q m. (n = (p ** m) * q) /\ coprime p q``, 3190 rpt strip_tac >> 3191 Cases_on `p divides n` >| [ 3192 `?m. 0 < m /\ p ** m divides n /\ !k. coprime (p ** k) (n DIV p ** m)` by rw[FACTOR_OUT_PRIME] >> 3193 qabbrev_tac `q = n DIV (p ** m)` >> 3194 `0 < p` by rw[PRIME_POS] >> 3195 `0 < p ** m` by rw[EXP_POS] >> 3196 metis_tac[DIVIDES_EQN_COMM, EXP_1], 3197 `coprime p n` by rw[prime_not_divides_is_coprime] >> 3198 metis_tac[EXP, MULT_LEFT_1] 3199 ]); 3200 3201(* Even this simple theorem is quite difficult to prove, why? *) 3202(* Because this needs a typical detective-style proof! *) 3203 3204(* Theorem: prime p /\ a divides (p ** n) ==> ?j. j <= n /\ (a = p ** j) *) 3205(* Proof: 3206 Note 0 < p by PRIME_POS 3207 so 0 < p ** n by EXP_POS 3208 Thus 0 < a by ZERO_DIVIDES 3209 ==> ?q m. (a = (p ** m) * q) /\ coprime p q by prime_power_factor 3210 3211 Claim: q = 1 3212 Proof: By contradiction, suppose q <> 1. 3213 Then ?t. prime t /\ t divides q by PRIME_FACTOR, q <> 1 3214 Now q divides a by divides_def 3215 so t divides (p ** n) by DIVIDES_TRANS 3216 ==> t = p by prime_divides_prime_power 3217 But gcd t q = t by divides_iff_gcd_fix 3218 or gcd p q = p by t = p 3219 Yet p <> 1 by NOT_PRIME_1 3220 so this contradicts coprime p q. 3221 3222 Thus a = p ** m by q = 1, Claim. 3223 Note p ** m <= p ** n by DIVIDES_LE, 0 < p 3224 and 1 < p by ONE_LT_PRIME 3225 ==> m <= n by EXP_BASE_LE_MONO, 1 < p 3226 Take j = m, and the result follows. 3227*) 3228val prime_power_divisor = store_thm( 3229 "prime_power_divisor", 3230 ``!p n a. prime p /\ a divides (p ** n) ==> ?j. j <= n /\ (a = p ** j)``, 3231 rpt strip_tac >> 3232 `0 < p` by rw[PRIME_POS] >> 3233 `0 < p ** n` by rw[EXP_POS] >> 3234 `0 < a` by metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO] >> 3235 `?q m. (a = (p ** m) * q) /\ coprime p q` by rw[prime_power_factor] >> 3236 `q = 1` by 3237 (spose_not_then strip_assume_tac >> 3238 `?t. prime t /\ t divides q` by rw[PRIME_FACTOR] >> 3239 `q divides a` by metis_tac[divides_def] >> 3240 `t divides (p ** n)` by metis_tac[DIVIDES_TRANS] >> 3241 `t = p` by metis_tac[prime_divides_prime_power] >> 3242 `gcd t q = t` by rw[GSYM divides_iff_gcd_fix] >> 3243 metis_tac[NOT_PRIME_1]) >> 3244 `a = p ** m` by rw[] >> 3245 metis_tac[DIVIDES_LE, EXP_BASE_LE_MONO, ONE_LT_PRIME]); 3246 3247(* Theorem: prime p /\ prime q ==> 3248 !m n. 0 < m /\ (p ** m = q ** n) ==> (p = q) /\ (m = n) *) 3249(* Proof: 3250 First goal: p = q. 3251 Since p divides p by DIVIDES_REFL 3252 ==> p divides p ** m by divides_exp, 0 < m. 3253 so p divides q ** n by given, p ** m = q ** n 3254 Hence p = q by prime_divides_prime_power 3255 Second goal: m = n. 3256 Note p = q by first goal. 3257 Since 1 < p by ONE_LT_PRIME 3258 Hence m = n by EXP_BASE_INJECTIVE, 1 < p 3259*) 3260val prime_powers_eq = store_thm( 3261 "prime_powers_eq", 3262 ``!p q. prime p /\ prime q ==> 3263 !m n. 0 < m /\ (p ** m = q ** n) ==> (p = q) /\ (m = n)``, 3264 ntac 6 strip_tac >> 3265 conj_asm1_tac >- 3266 metis_tac[divides_exp, prime_divides_prime_power, DIVIDES_REFL] >> 3267 metis_tac[EXP_BASE_INJECTIVE, ONE_LT_PRIME]); 3268 3269(* Theorem: prime p /\ prime q /\ p <> q ==> !m n. coprime (p ** m) (q ** n) *) 3270(* Proof: 3271 Let d = gcd (p ** m) (q ** n). 3272 By contradiction, d <> 1. 3273 Then d divides (p ** m) /\ d divides (q ** n) by GCD_PROPERTY 3274 ==> ?j. j <= m /\ (d = p ** j) by prime_power_divisor, prime p 3275 and ?k. k <= n /\ (d = q ** k) by prime_power_divisor, prime q 3276 Note j <> 0 /\ k <> 0 by EXP_0 3277 or 0 < j /\ 0 < k by arithmetic 3278 ==> p = q, which contradicts p <> q by prime_powers_eq 3279*) 3280val prime_powers_coprime = store_thm( 3281 "prime_powers_coprime", 3282 ``!p q. prime p /\ prime q /\ p <> q ==> !m n. coprime (p ** m) (q ** n)``, 3283 spose_not_then strip_assume_tac >> 3284 qabbrev_tac `d = gcd (p ** m) (q ** n)` >> 3285 `d divides (p ** m) /\ d divides (q ** n)` by metis_tac[GCD_PROPERTY] >> 3286 metis_tac[prime_power_divisor, prime_powers_eq, EXP_0, NOT_ZERO_LT_ZERO]); 3287 3288(* 3289val prime_powers_eq = |- !p q. prime p /\ prime q ==> !m n. 0 < m /\ (p ** m = q ** n) ==> (p = q) /\ (m = n): thm 3290*) 3291 3292(* Theorem: prime p /\ prime q ==> !m n. 0 < m ==> ((p ** m divides q ** n) <=> (p = q) /\ (m <= n)) *) 3293(* Proof: 3294 If part: p ** m divides q ** n ==> (p = q) /\ m <= n 3295 Note p divides (p ** m) by prime_divides_self_power, 0 < m 3296 so p divides (q ** n) by DIVIDES_TRANS 3297 Thus p = q by prime_divides_prime_power 3298 Note 1 < p by ONE_LT_PRIME 3299 Thus m <= n by power_divides_iff 3300 Only-if part: (p = q) /\ m <= n ==> p ** m divides q ** n 3301 Note 1 < p by ONE_LT_PRIME 3302 Thus p ** m divides q ** n by power_divides_iff 3303*) 3304val prime_powers_divide = store_thm( 3305 "prime_powers_divide", 3306 ``!p q. prime p /\ prime q ==> !m n. 0 < m ==> ((p ** m divides q ** n) <=> (p = q) /\ (m <= n))``, 3307 metis_tac[ONE_LT_PRIME, divides_self_power, prime_divides_prime_power, power_divides_iff, DIVIDES_TRANS]); 3308 3309(* Theorem: gcd (b ** m) (b ** n) = b ** (MIN m n) *) 3310(* Proof: 3311 If m = n, 3312 LHS = gcd (b ** n) (b ** n) 3313 = b ** n by GCD_REF 3314 RHS = b ** (MIN n n) 3315 = b ** n by MIN_IDEM 3316 If m < n, 3317 b ** n = b ** (n - m + m) by arithmetic 3318 = b ** (n - m) * b ** m by EXP_ADD 3319 so (b ** m) divides (b ** n) by divides_def 3320 or gcd (b ** m) (b ** n) 3321 = b ** m by divides_iff_gcd_fix 3322 = b ** (MIN m n) by MIN_DEF 3323 If ~(m < n), n < m. 3324 Similar argument as m < n, with m n exchanged, use GCD_SYM. 3325*) 3326val gcd_powers = store_thm( 3327 "gcd_powers", 3328 ``!b m n. gcd (b ** m) (b ** n) = b ** (MIN m n)``, 3329 rpt strip_tac >> 3330 Cases_on `m = n` >- 3331 rw[] >> 3332 Cases_on `m < n` >| [ 3333 `b ** n = b ** (n - m + m)` by rw[] >> 3334 `_ = b ** (n - m) * b ** m` by rw[EXP_ADD] >> 3335 `(b ** m) divides (b ** n)` by metis_tac[divides_def] >> 3336 metis_tac[divides_iff_gcd_fix, MIN_DEF], 3337 `n < m` by decide_tac >> 3338 `b ** m = b ** (m - n + n)` by rw[] >> 3339 `_ = b ** (m - n) * b ** n` by rw[EXP_ADD] >> 3340 `(b ** n) divides (b ** m)` by metis_tac[divides_def] >> 3341 metis_tac[divides_iff_gcd_fix, GCD_SYM, MIN_DEF] 3342 ]); 3343 3344(* Theorem: lcm (b ** m) (b ** n) = b ** (MAX m n) *) 3345(* Proof: 3346 If m = n, 3347 LHS = lcm (b ** n) (b ** n) 3348 = b ** n by LCM_REF 3349 RHS = b ** (MAX n n) 3350 = b ** n by MAX_IDEM 3351 If m < n, 3352 b ** n = b ** (n - m + m) by arithmetic 3353 = b ** (n - m) * b ** m by EXP_ADD 3354 so (b ** m) divides (b ** n) by divides_def 3355 or lcm (b ** m) (b ** n) 3356 = b ** n by divides_iff_lcm_fix 3357 = b ** (MAX m n) by MAX_DEF 3358 If ~(m < n), n < m. 3359 Similar argument as m < n, with m n exchanged, use LCM_COMM. 3360*) 3361val lcm_powers = store_thm( 3362 "lcm_powers", 3363 ``!b m n. lcm (b ** m) (b ** n) = b ** (MAX m n)``, 3364 rpt strip_tac >> 3365 Cases_on `m = n` >- 3366 rw[LCM_REF] >> 3367 Cases_on `m < n` >| [ 3368 `b ** n = b ** (n - m + m)` by rw[] >> 3369 `_ = b ** (n - m) * b ** m` by rw[EXP_ADD] >> 3370 `(b ** m) divides (b ** n)` by metis_tac[divides_def] >> 3371 metis_tac[divides_iff_lcm_fix, MAX_DEF], 3372 `n < m` by decide_tac >> 3373 `b ** m = b ** (m - n + n)` by rw[] >> 3374 `_ = b ** (m - n) * b ** n` by rw[EXP_ADD] >> 3375 `(b ** n) divides (b ** m)` by metis_tac[divides_def] >> 3376 metis_tac[divides_iff_lcm_fix, LCM_COMM, MAX_DEF] 3377 ]); 3378 3379(* Theorem: 0 < b /\ 0 < m ==> coprime (b ** n) (b ** m - 1) *) 3380(* Proof: 3381 If m = n, 3382 coprime (b ** n) (b ** n - 1) 3383 <=> T by coprime_PRE 3384 3385 Claim: !j. j < m ==> coprime (b ** j) (b ** m - 1) 3386 Proof: b ** m 3387 = b ** (m - j + j) by SUB_ADD 3388 = b ** (m - j) * b ** j by EXP_ADD 3389 Thus (b ** j) divides (b ** m) by divides_def 3390 Now 0 < b ** m by EXP_POS 3391 so coprime (b ** j) (PRE (b ** m)) by divides_imp_coprime_with_predecessor 3392 or coprime (b ** j) (b ** m - 1) by PRE_SUB1 3393 3394 Given 0 < m, 3395 b ** n 3396 = b ** ((n DIV m) * m + n MOD m) by DIVISION 3397 = b ** (m * (n DIV m) + n MOD m) by MULT_COMM 3398 = b ** (m * (n DIV m)) * b ** (n MOD m) by EXP_ADD 3399 = (b ** m) ** (n DIV m) * b ** (n MOD m) by EXP_EXP_MULT 3400 Let z = b ** m, 3401 Then b ** n = z ** (n DIV m) * b ** (n MOD m) 3402 and 0 < z by EXP_POS 3403 Since coprime z (z - 1) by coprime_PRE 3404 ==> coprime (z ** (n DIV m)) (z - 1) by coprime_exp 3405 gcd (b ** n) (b ** m - 1) 3406 = gcd (z ** (n DIV m) * b ** (n MOD m)) (z - 1) 3407 = gcd (b ** (n MOD m)) (z - 1) by GCD_SYM, GCD_CANCEL_MULT 3408 Now (n MOD m) < m by MOD_LESS 3409 so apply the claim to deduce the result. 3410*) 3411val coprime_power_and_power_predecessor = store_thm( 3412 "coprime_power_and_power_predecessor", 3413 ``!b m n. 0 < b /\ 0 < m ==> coprime (b ** n) (b ** m - 1)``, 3414 rpt strip_tac >> 3415 `0 < b ** n /\ 0 < b ** m` by rw[EXP_POS] >> 3416 Cases_on `m = n` >- 3417 rw[coprime_PRE] >> 3418 `!j. j < m ==> coprime (b ** j) (b ** m - 1)` by 3419 (rpt strip_tac >> 3420 `b ** m = b ** (m - j + j)` by rw[] >> 3421 `_ = b ** (m - j) * b ** j` by rw[EXP_ADD] >> 3422 `(b ** j) divides (b ** m)` by metis_tac[divides_def] >> 3423 metis_tac[divides_imp_coprime_with_predecessor, PRE_SUB1]) >> 3424 `b ** n = b ** ((n DIV m) * m + n MOD m)` by rw[GSYM DIVISION] >> 3425 `_ = b ** (m * (n DIV m) + n MOD m)` by rw[MULT_COMM] >> 3426 `_ = b ** (m * (n DIV m)) * b ** (n MOD m)` by rw[EXP_ADD] >> 3427 `_ = (b ** m) ** (n DIV m) * b ** (n MOD m)` by rw[EXP_EXP_MULT] >> 3428 qabbrev_tac `z = b ** m` >> 3429 `coprime z (z - 1)` by rw[coprime_PRE] >> 3430 `coprime (z ** (n DIV m)) (z - 1)` by rw[coprime_exp] >> 3431 metis_tac[GCD_SYM, GCD_CANCEL_MULT, MOD_LESS]); 3432 3433(* Any counter-example? Theorem proved, no counter-example! *) 3434(* This is a most unexpected theorem. 3435 At first I thought it only holds for prime base b, 3436 but in HOL4 using the EVAL function shows it seems to hold for any base b. 3437 As for the proof, I don't have a clue initially. 3438 I try this idea: 3439 For a prime base b, most likely ODD b, then ODD (b ** n) and ODD (b ** m). 3440 But then EVEN (b ** m - 1), maybe ODD and EVEN will give coprime. 3441 If base b is EVEN, then EVEN (b ** n) but ODD (b ** m - 1), so this can work. 3442 However, in general ODD and EVEN do not give coprime: gcd 6 9 = 3. 3443 Of course, if ODD and EVEN arise from powers of same base, like this theorem, then true! 3444 Actually this follows from divides_imp_coprime_with_predecessor, sort of. 3445 This success inspires the following theorem. 3446*) 3447 3448(* Theorem: 0 < b /\ 0 < m ==> coprime (b ** n) (b ** m + 1) *) 3449(* Proof: 3450 If m = n, 3451 coprime (b ** n) (b ** n + 1) 3452 <=> T by coprime_SUC 3453 3454 Claim: !j. j < m ==> coprime (b ** j) (b ** m + 1) 3455 Proof: b ** m 3456 = b ** (m - j + j) by SUB_ADD 3457 = b ** (m - j) * b ** j by EXP_ADD 3458 Thus (b ** j) divides (b ** m) by divides_def 3459 Now 0 < b ** m by EXP_POS 3460 so coprime (b ** j) (SUC (b ** m)) by divides_imp_coprime_with_successor 3461 or coprime (b ** j) (b ** m + 1) by ADD1 3462 3463 Given 0 < m, 3464 b ** n 3465 = b ** ((n DIV m) * m + n MOD m) by DIVISION 3466 = b ** (m * (n DIV m) + n MOD m) by MULT_COMM 3467 = b ** (m * (n DIV m)) * b ** (n MOD m) by EXP_ADD 3468 = (b ** m) ** (n DIV m) * b ** (n MOD m) by EXP_EXP_MULT 3469 Let z = b ** m, 3470 Then b ** n = z ** (n DIV m) * b ** (n MOD m) 3471 and 0 < z by EXP_POS 3472 Since coprime z (z + 1) by coprime_SUC 3473 ==> coprime (z ** (n DIV m)) (z + 1) by coprime_exp 3474 gcd (b ** n) (b ** m + 1) 3475 = gcd (z ** (n DIV m) * b ** (n MOD m)) (z + 1) 3476 = gcd (b ** (n MOD m)) (z + 1) by GCD_SYM, GCD_CANCEL_MULT 3477 Now (n MOD m) < m by MOD_LESS 3478 so apply the claim to deduce the result. 3479*) 3480val coprime_power_and_power_successor = store_thm( 3481 "coprime_power_and_power_successor", 3482 ``!b m n. 0 < b /\ 0 < m ==> coprime (b ** n) (b ** m + 1)``, 3483 rpt strip_tac >> 3484 `0 < b ** n /\ 0 < b ** m` by rw[EXP_POS] >> 3485 Cases_on `m = n` >- 3486 rw[coprime_SUC] >> 3487 `!j. j < m ==> coprime (b ** j) (b ** m + 1)` by 3488 (rpt strip_tac >> 3489 `b ** m = b ** (m - j + j)` by rw[] >> 3490 `_ = b ** (m - j) * b ** j` by rw[EXP_ADD] >> 3491 `(b ** j) divides (b ** m)` by metis_tac[divides_def] >> 3492 metis_tac[divides_imp_coprime_with_successor, ADD1]) >> 3493 `b ** n = b ** ((n DIV m) * m + n MOD m)` by rw[GSYM DIVISION] >> 3494 `_ = b ** (m * (n DIV m) + n MOD m)` by rw[MULT_COMM] >> 3495 `_ = b ** (m * (n DIV m)) * b ** (n MOD m)` by rw[EXP_ADD] >> 3496 `_ = (b ** m) ** (n DIV m) * b ** (n MOD m)` by rw[EXP_EXP_MULT] >> 3497 qabbrev_tac `z = b ** m` >> 3498 `coprime z (z + 1)` by rw[coprime_SUC] >> 3499 `coprime (z ** (n DIV m)) (z + 1)` by rw[coprime_exp] >> 3500 metis_tac[GCD_SYM, GCD_CANCEL_MULT, MOD_LESS]); 3501 3502(* ------------------------------------------------------------------------- *) 3503(* Useful Theorems *) 3504(* ------------------------------------------------------------------------- *) 3505 3506(* Theorem: prime p /\ q divides (p ** n) ==> (q = 1) \/ (p divides q) *) 3507(* Proof: 3508 By contradiction, suppose q <> 1 /\ ~(p divides q). 3509 Note ?j. j <= n /\ (q = p ** j) by prime_power_divisor 3510 and 0 < j by EXP_0, q <> 1 3511 then p divides q by prime_divides_self_power, 0 < j 3512 This contradicts ~(p divides q). 3513*) 3514Theorem PRIME_EXP_FACTOR: 3515 !p q n. prime p /\ q divides (p ** n) ==> (q = 1) \/ (p divides q) 3516Proof 3517 spose_not_then strip_assume_tac >> 3518 `?j. j <= n /\ (q = p ** j)` by rw[prime_power_divisor] >> 3519 `0 < j` by fs[] >> 3520 metis_tac[prime_divides_self_power] 3521QED 3522 3523(* Idea: For prime p, FACT (p-1) MOD p <> 0 *) 3524 3525(* Theorem: prime p /\ n < p ==> FACT n MOD p <> 0 *) 3526(* Proof: 3527 Note 1 < p by ONE_LT_PRIME 3528 By induction on n. 3529 Base: 0 < p ==> (FACT 0 MOD p = 0) ==> F 3530 Note FACT 0 = 1 by FACT_0 3531 and 1 MOD p = 1 by LESS_MOD, 1 < p 3532 and 1 = 0 is F. 3533 Step: n < p ==> (FACT n MOD p = 0) ==> F ==> 3534 SUC n < p ==> (FACT (SUC n) MOD p = 0) ==> F 3535 If n = 0, SUC 0 = 1 by ONE 3536 Note FACT 1 = 1 by FACT_1 3537 and 1 MOD p = 1 by LESS_MOD, 1 < p 3538 and 1 = 0 is F. 3539 If n <> 0, 0 < n. 3540 (FACT (SUC n)) MOD p = 0 3541 <=> (SUC n * FACT n) MOD p = 0 by FACT 3542 Note (SUC n) MOD p <> 0 by MOD_LESS, SUC n < p 3543 and (FACT n) MOD p <> 0 by induction hypothesis 3544 so (SUC n * FACT n) MOD p <> 0 by EUCLID_LEMMA 3545 This is a contradiction. 3546*) 3547Theorem FACT_MOD_PRIME: 3548 !p n. prime p /\ n < p ==> FACT n MOD p <> 0 3549Proof 3550 rpt strip_tac >> 3551 `1 < p` by rw[ONE_LT_PRIME] >> 3552 Induct_on `n` >- 3553 simp[FACT_0] >> 3554 Cases_on `n = 0` >- 3555 simp[FACT_1] >> 3556 rw[FACT] >> 3557 `n < p` by decide_tac >> 3558 `(SUC n) MOD p <> 0` by fs[] >> 3559 metis_tac[EUCLID_LEMMA] 3560QED 3561 3562 3563(* ------------------------------------------------------------------------- *) 3564 3565(* export theory at end *) 3566val _ = export_theory(); 3567 3568(*===========================================================================*) 3569