1(*===========================================================================*) 2(* Euclid's theorem: for every prime, there is another one that is larger. *) 3(* This proof has been excerpted and adapted from John Harrison's proof of *) 4(* a special case (n=4) of Fermat's Last Theorem. *) 5(* *) 6(*===========================================================================*) 7 8(*---------------------------------------------------------------------------*) 9(* First, open required context: the theory of arithmetic. This theory is *) 10(* automatically loaded when HOL starts, but the ML module arithmeticTheory *) 11(* needs to be opened before the definitions and theorems of the theory are *) 12(* available without supplying the "arithmeticTheory." prefix. *) 13(*---------------------------------------------------------------------------*) 14 15open arithmeticTheory; 16 17(*---------------------------------------------------------------------------*) 18(* Divisibility. *) 19(*---------------------------------------------------------------------------*) 20 21 22Definition divides_def: 23 divides a b = ?x. b = a * x 24End; 25 26set_fixity "divides" (Infix(NONASSOC, 450)); 27 28(*---------------------------------------------------------------------------*) 29(* Primality. *) 30(*---------------------------------------------------------------------------*) 31 32Definition prime_def: 33 prime p <=> p<>1 /\ !x. x divides p ==> (x=1) \/ (x=p) 34End 35 36(*---------------------------------------------------------------------------*) 37(* A sequence of basic theorems about the "divides" relation. *) 38(*---------------------------------------------------------------------------*) 39 40val DIVIDES_0 = store_thm 41 ("DIVIDES_0", 42 ``!x. x divides 0``, 43 metis_tac [divides_def,MULT_CLAUSES]); 44 45val DIVIDES_ZERO = store_thm 46 ("DIVIDES_ZERO", 47 ``!x. 0 divides x <=> x = 0``, 48 metis_tac [divides_def,MULT_CLAUSES]); 49 50val DIVIDES_ONE = store_thm 51 ("DIVIDES_ONE", 52 ``!x. x divides 1 <=> x = 1``, 53 metis_tac [divides_def,MULT_CLAUSES,MULT_EQ_1]); 54 55val DIVIDES_REFL = store_thm 56 ("DIVIDES_REFL", 57 ``!x. x divides x``, 58 metis_tac [divides_def,MULT_CLAUSES]); 59 60val DIVIDES_TRANS = store_thm 61 ("DIVIDES_TRANS", 62 ``!a b c. a divides b /\ b divides c ==> a divides c``, 63 metis_tac [divides_def,MULT_ASSOC]); 64 65val DIVIDES_ADD = store_thm 66("DIVIDES_ADD", 67 ``!d a b. d divides a /\ d divides b ==> d divides (a + b)``, 68 metis_tac[divides_def,LEFT_ADD_DISTRIB]); 69 70val DIVIDES_SUB = store_thm 71 ("DIVIDES_SUB", 72 ``!d a b. d divides a /\ d divides b ==> d divides (a - b)``, 73 metis_tac [divides_def,LEFT_SUB_DISTRIB]); 74 75val DIVIDES_ADDL = store_thm 76 ("DIVIDES_ADDL", 77 ``!d a b. d divides a /\ d divides (a + b) ==> d divides b``, 78 metis_tac [ADD_SUB,ADD_SYM,DIVIDES_SUB]); 79 80val DIVIDES_LMUL = store_thm 81 ("DIVIDES_LMUL", 82 ``!d a x. d divides a ==> d divides (x * a)``, 83 metis_tac [divides_def,MULT_ASSOC,MULT_SYM]); 84 85val DIVIDES_RMUL = store_thm 86 ("DIVIDES_RMUL", 87 ``!d a x. d divides a ==> d divides (a * x)``, 88 metis_tac [MULT_SYM,DIVIDES_LMUL]); 89 90val DIVIDES_LE = store_thm 91 ("DIVIDES_LE", 92 ``!m n. m divides n ==> m <= n \/ (n = 0)``, 93 rw [divides_def] >> rw[]); 94 95(*---------------------------------------------------------------------------*) 96(* Various proofs of the same formula *) 97(*---------------------------------------------------------------------------*) 98 99val DIVIDES_FACT = store_thm 100 ("DIVIDES_FACT", 101 ``!m n. 0 < m /\ m <= n ==> m divides (FACT n)``, 102 rw [LESS_EQ_EXISTS] 103 >> Induct_on `p` 104 >> rw [FACT,ADD_CLAUSES] 105 >| [Cases_on `m`, ALL_TAC] 106 >> metis_tac [FACT, DECIDE ``!x. ~(x < x)``, 107 DIVIDES_RMUL, DIVIDES_LMUL, DIVIDES_REFL]); 108 109val DIVIDES_FACT = prove 110 (``!m n. 0 < m /\ m <= n ==> m divides (FACT n)``, 111 `!m p. 0 < m ==> m divides FACT (m + p)` 112 suffices_by metis_tac[LESS_EQ_EXISTS] 113 >> Induct_on `p` 114 >> rw [FACT,ADD_CLAUSES] 115 >> metis_tac [FACT, DECIDE ``!x. ~(x < x)``, num_CASES, 116 DIVIDES_RMUL, DIVIDES_LMUL, DIVIDES_REFL]); 117 118val DIVIDES_FACT = prove 119 (``!m n. 0 < m /\ m <= n ==> m divides (FACT n)``, 120 rw [LESS_EQ_EXISTS] 121 >> Induct_on `p` 122 >> metis_tac [FACT, DECIDE ``!x. ~(x < x)``, num_CASES, 123 DIVIDES_RMUL,DIVIDES_LMUL,DIVIDES_REFL,ADD_CLAUSES]); 124 125 126val DIVIDES_FACT = prove 127(``!m n. 0 < m /\ m <= n ==> m divides (FACT n)``, 128Induct_on `n - m` 129 >> rw [] >| 130 [`m = n` by rw[] >> 131 `?k. m = SUC k` by (Cases_on `m` >> fs[]) 132 >> metis_tac[FACT,DIVIDES_RMUL,DIVIDES_REFL], 133 `0 < n` by rw[] >> 134 `?k. n = SUC k` by (Cases_on `n` >> fs[]) 135 >> rw [FACT, DIVIDES_RMUL]]); 136 137 138(*---------------------------------------------------------------------------*) 139(* Zero and one are not prime, but two is. All primes are positive. *) 140(*---------------------------------------------------------------------------*) 141 142val NOT_PRIME_0 = store_thm 143 ("NOT_PRIME_0", 144 ``~prime 0``, 145 rw [prime_def,DIVIDES_0]); 146 147val NOT_PRIME_1 = store_thm 148 ("NOT_PRIME_1", 149 ``~prime 1``, 150 rw [prime_def]); 151 152val PRIME_2 = store_thm 153 ("PRIME_2", 154 ``prime 2``, 155 rw [prime_def] >> 156 metis_tac [DIVIDES_LE, DIVIDES_ZERO, 157 DECIDE``~(2=1) /\ ~(2=0) /\ (x<=2 <=> (x=0) \/ (x=1) \/ (x=2))``]); 158 159val PRIME_POS = store_thm 160 ("PRIME_POS", 161 ``!p. prime p ==> 0<p``, 162 Cases >> rw [NOT_PRIME_0]); 163 164(*---------------------------------------------------------------------------*) 165(* Every number has a prime factor, except for 1. The proof proceeds by a *) 166(* "complete" induction on n, and then considers cases on whether n is *) 167(* prime or not. The first case (n is prime) is trivial. In the second case, *) 168(* there must be an "x" that divides n, and x is not 1 or n. By DIVIDES_LE, *) 169(* n=0 or x <= n. If n=0, then 2 is a prime that divides 0. On the other *) 170(* hand, if x <= n, there are two cases: if x<n then we can use the i.h. and *) 171(* by transitivity of divides we are done; otherwise, if x=n, then we have *) 172(* a contradiction with the fact that x is not 1 or n. *) 173(*---------------------------------------------------------------------------*) 174 175val PRIME_FACTOR = store_thm 176 ("PRIME_FACTOR", 177 ``!n. ~(n = 1) ==> ?p. prime p /\ p divides n``, 178 completeInduct_on `n` 179 >> rw [] 180 >> Cases_on `prime n` >| 181 [metis_tac [DIVIDES_REFL], 182 `?x. x divides n /\ x<>1 /\ x<>n` by metis_tac[prime_def] >> 183 metis_tac [LESS_OR_EQ, PRIME_2, 184 DIVIDES_LE, DIVIDES_TRANS, DIVIDES_0]]); 185 186(*---------------------------------------------------------------------------*) 187(* In the following proof, metis_tac automatically considers cases on *) 188(* whether n is prime or not. *) 189(*---------------------------------------------------------------------------*) 190 191val PRIME_FACTOR = prove 192 (``!n. n<>1 ==> ?p. prime p /\ p divides n``, 193 completeInduct_on `n` >> 194 metis_tac [DIVIDES_REFL,prime_def,LESS_OR_EQ, PRIME_2, 195 DIVIDES_LE, DIVIDES_TRANS, DIVIDES_0]); 196 197 198(*---------------------------------------------------------------------------*) 199(* Every number has a prime greater than it. *) 200(* Proof. *) 201(* Suppose not; then there's an n such that all p greater than n are not *) 202(* prime. Consider FACT(n) + 1: it's not equal to 1, so there's a prime q *) 203(* that divides it. q also divides FACT n because q is less-than-or-equal *) 204(* to n. By DIVIDES_ADDL, this means that q=1. But then q is not prime, *) 205(* which is a contradiction. *) 206(*---------------------------------------------------------------------------*) 207 208val EUCLID = store_thm 209 ("EUCLID", 210 ``!n. ?p. n < p /\ prime p``, 211 spose_not_then strip_assume_tac 212 >> mp_tac (SPEC ``FACT n + 1`` PRIME_FACTOR) 213 >> rw [FACT_LESS, DECIDE ``x <> 0 <=> 0 < x``] 214 >> metis_tac [DIVIDES_FACT, DIVIDES_ADDL, DIVIDES_ONE, 215 NOT_PRIME_1, NOT_LESS, PRIME_POS]); 216 217 218(*---------------------------------------------------------------------------*) 219(* The previous proof is somewhat unsatisfactory, because its structure gets *) 220(* hidden in the invocations of the automated reasoners. An assertional *) 221(* style allows a presentation that mirrors the informal proof. *) 222(*---------------------------------------------------------------------------*) 223 224val EUCLID_AGAIN = prove (``!n. ?p. n < p /\ prime p``, 225 CCONTR_TAC >> 226 `?n. !p. n < p ==> ~prime p` by metis_tac[] >> 227 `~(FACT n + 1 = 1)` by rw [FACT_LESS, 228 DECIDE ``x<>0 <=> 0<x``] >> 229 `?p. prime p /\ 230 p divides (FACT n + 1)` by metis_tac [PRIME_FACTOR] >> 231 `0 < p` by metis_tac [PRIME_POS] >> 232 `p <= n` by metis_tac [NOT_LESS] >> 233 `p divides FACT n` by metis_tac [DIVIDES_FACT] >> 234 `p divides 1` by metis_tac [DIVIDES_ADDL] >> 235 `p = 1` by metis_tac [DIVIDES_ONE] >> 236 `~prime p` by metis_tac [NOT_PRIME_1] >> 237 metis_tac[]); 238