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