1open HolKernel Parse boolLib simpLib BasicProvers
2     prim_recTheory arithmeticTheory boolSimps
3     metisLib numLib;
4
5val CALC = EQT_ELIM o reduceLib.REDUCE_CONV;
6val ARITH_TAC = CONV_TAC Arith.ARITH_CONV;
7val DECIDE = EQT_ELIM o Arith.ARITH_CONV;
8
9val arith_ss = numLib.arith_ss;
10
11val ARW = RW_TAC arith_ss;
12
13local open numeralTheory in end;
14  (* concession to Holmake's flawed dependency analysis, which doesn't
15     spot this problem *)
16
17val _ = new_theory "divides";
18
19val divides_def = Q.new_definition
20  ("divides_def",
21   `divides a b = ?q. b = q*a`);
22
23val ALL_DIVIDES_0 = store_thm
24("ALL_DIVIDES_0",
25 ``!a. divides a 0``,
26 METIS_TAC[divides_def,MULT_CLAUSES])
27 before
28 export_rewrites ["ALL_DIVIDES_0"];
29
30val ZERO_DIVIDES = store_thm(
31  "ZERO_DIVIDES",
32  ``divides 0 m = (m = 0)``,
33  SRW_TAC [][divides_def])
34  before
35  export_rewrites ["ZERO_DIVIDES"];
36
37val DIVIDES_REFL = store_thm
38("DIVIDES_REFL",
39 ``!a. divides a a``,
40 METIS_TAC[divides_def,MULT_CLAUSES])
41 before
42 export_rewrites ["DIVIDES_REFL"];
43
44val DIVIDES_TRANS = store_thm
45 ("DIVIDES_TRANS",
46  ``!a b c. divides a b /\ divides b c ==> divides a c``,
47  METIS_TAC [divides_def,MULT_ASSOC]);
48
49val ONE_DIVIDES_ALL = store_thm
50("ONE_DIVIDES_ALL",
51 ``!a. divides 1 a``,
52 METIS_TAC[divides_def,MULT_CLAUSES])
53 before
54 export_rewrites ["ONE_DIVIDES_ALL"];
55
56val DIVIDES_ONE = store_thm
57 ("DIVIDES_ONE",
58  ``!x. divides x 1 = (x = 1)``,
59  METIS_TAC [divides_def,MULT_CLAUSES,MULT_EQ_1])
60  before
61  export_rewrites ["DIVIDES_ONE"];
62
63val DIVIDES_ADD_1 = store_thm
64("DIVIDES_ADD_1",
65 ``!a b c. divides a b /\ divides a c ==> divides a (b+c)``,
66 METIS_TAC[divides_def,RIGHT_ADD_DISTRIB]);
67
68val DIVIDES_ADD_2 = store_thm
69("DIVIDES_ADD_2",
70 ``!a b c. divides a b /\ divides a (b+c) ==> divides a c``,
71 ARW[divides_def] THEN EXISTS_TAC ``q' - q`` THEN ARW[RIGHT_SUB_DISTRIB]);
72
73val DIVIDES_SUB = store_thm
74("DIVIDES_SUB",
75 ``!a b c. divides a b /\ divides a c ==> divides a (b-c)``,
76 METIS_TAC[divides_def,RIGHT_SUB_DISTRIB]);
77
78val DIVIDES_LE = store_thm
79("DIVIDES_LE",
80 ``!a b. 0<b /\ divides a b ==> a <= b``,
81 Cases_on `a` THEN ARW[divides_def] THEN Cases_on `q` THENL
82 [METIS_TAC [MULT_CLAUSES,LESS_REFL],
83  ARW[MULT_CLAUSES]]);
84
85val DIVIDES_LEQ_OR_ZERO = store_thm
86 ("DIVIDES_LEQ_OR_ZERO",
87  ``!m n. divides m n ==> m <= n \/ (n = 0)``,
88  ARW [divides_def]
89     THEN Cases_on `q`
90     THEN ARW [MULT_CLAUSES]);
91
92val NOT_LT_DIVIDES = store_thm
93("NOT_LT_DIVIDES",
94 ``!a b. 0<b /\ b<a ==> ~(divides a b)``,
95 METIS_TAC[DIVIDES_LE,LESS_EQ_ANTISYM]);
96
97val DIVIDES_ANTISYM = store_thm
98("DIVIDES_ANTISYM",
99 ``!a b. divides a b /\ divides b a ==> (a = b)``,
100 REPEAT Cases
101  THEN TRY (ARW[divides_def] THEN NO_TAC)
102  THEN METIS_TAC [LESS_EQUAL_ANTISYM,DIVIDES_LE,prim_recTheory.LESS_0]);
103
104val DIVIDES_MULT = store_thm
105("DIVIDES_MULT",
106 ``!a b c. divides a b ==> divides a (b*c)``,
107  METIS_TAC[divides_def,MULT_SYM,MULT_ASSOC]);
108
109val DIVIDES_MULT_LEFT = store_thm(
110  "DIVIDES_MULT_LEFT",
111  ``!n m. divides (n * m) m = (m = 0) \/ (n = 1)``,
112  SIMP_TAC arith_ss [FORALL_AND_THM, EQ_IMP_THM, DISJ_IMP_THM,
113                     ALL_DIVIDES_0, DIVIDES_REFL] THEN
114  SIMP_TAC bool_ss [divides_def] THEN REPEAT STRIP_TAC THEN
115  `m * 1 = m * (n * q)` by
116     (POP_ASSUM (CONV_TAC o LAND_CONV o
117                 ONCE_REWRITE_CONV o C cons []) THEN
118      ASM_SIMP_TAC bool_ss [MULT_CLAUSES] THEN
119      CONV_TAC (AC_CONV(MULT_ASSOC, MULT_COMM))) THEN
120  `(m = 0) \/ (n * q = 1)` by METIS_TAC [EQ_MULT_LCANCEL] THEN
121  ASM_SIMP_TAC bool_ss [] THEN
122  METIS_TAC [MULT_EQ_1]);
123
124val DIVIDES_EXP = Q.prove
125(`!a b x. 0 < x /\ divides a b ==> divides a (b ** x)`,
126 Cases_on `x` THEN RW_TAC arith_ss [EXP] THEN METIS_TAC [DIVIDES_MULT]);
127
128val DIVIDES_FACT = store_thm
129("DIVIDES_FACT",
130 ``!b. 0<b ==> divides b (FACT b)``,
131 Cases_on `b` THEN ARW[FACT, divides_def] THEN METIS_TAC [MULT_COMM]);
132
133val LEQ_DIVIDES_FACT = store_thm
134 ("LEQ_DIVIDES_FACT",
135  ``!m n. 0 < m /\ m <= n ==> divides m (FACT n)``,
136  RW_TAC arith_ss  [LESS_EQ_EXISTS]
137   THEN Induct_on `p`
138   THEN METIS_TAC [FACT, LESS_REFL, num_CASES, DIVIDES_MULT,
139                   MULT_COMM, DIVIDES_REFL, ADD_CLAUSES]);
140
141(*---------------------------------------------------------------------------*)
142(* Definition and trivial facts about primality.                             *)
143(*---------------------------------------------------------------------------*)
144
145val prime_def = Q.new_definition
146("prime_def",
147 `prime a = ~(a=1) /\ !b. divides b a ==> (b=a) \/ (b=1)`);
148
149
150val NOT_PRIME_0 = Q.store_thm
151 ("NOT_PRIME_0",
152  `~prime 0`,
153  ARW [prime_def, ALL_DIVIDES_0])
154  before
155  export_rewrites ["NOT_PRIME_0"];
156
157val NOT_PRIME_1 = Q.store_thm
158 ("NOT_PRIME_1",
159  `~prime 1`,
160  ARW [prime_def, DIVIDES_LE])
161  before
162  export_rewrites ["NOT_PRIME_1"];
163
164val PRIME_2 = store_thm
165 ("PRIME_2",
166  ``prime 2``,
167  RW_TAC arith_ss  [prime_def] THEN
168  `0 < b /\ b <= 2` by METIS_TAC [DIVIDES_LE, ZERO_DIVIDES,
169                                  CALC ``0<2``,NOT_ZERO_LT_ZERO] THEN
170  NTAC 2 (POP_ASSUM MP_TAC) THEN ARITH_TAC)
171  before
172  export_rewrites ["PRIME_2"];
173
174val PRIME_3 = Q.store_thm
175("PRIME_3",
176 `prime 3`,
177  RW_TAC arith_ss  [prime_def] THEN
178  `b <= 3` by RW_TAC arith_ss [DIVIDES_LE] THEN
179  `(b=0) \/ (b=1) \/ (b=2) \/ (b=3)` by (POP_ASSUM MP_TAC THEN ARITH_TAC) THEN
180  RW_TAC arith_ss [] THENL
181  [FULL_SIMP_TAC arith_ss [ZERO_DIVIDES],
182   FULL_SIMP_TAC arith_ss [divides_def]])
183  before
184  export_rewrites ["PRIME_3"];
185
186val PRIME_POS = store_thm
187 ("PRIME_POS",
188  ``!p. prime p ==> 0<p``,
189  Cases THEN RW_TAC arith_ss [NOT_PRIME_0]);
190
191val ONE_LT_PRIME = Q.store_thm
192("ONE_LT_PRIME",
193 `!p. prime p ==> 1 < p`,
194 METIS_TAC [NOT_PRIME_0, NOT_PRIME_1,
195            DECIDE ``(p=0) \/ (p=1) \/ 1 < p``]);
196
197val prime_divides_only_self = Q.store_thm
198("prime_divides_only_self",
199 `!m n. prime m /\ prime n /\ divides m n ==> (m=n)`,
200 RW_TAC arith_ss [divides_def] THEN
201 `m<>1` by METIS_TAC [NOT_PRIME_0,NOT_PRIME_1] THEN
202 Q.PAT_X_ASSUM `prime (m*q)` MP_TAC THEN RW_TAC arith_ss [prime_def] THEN
203 METIS_TAC [divides_def,MULT_SYM]);
204
205
206(*---------------------------------------------------------------------------*)
207(* Every number has a prime factor, except for 1. The proof proceeds by a    *)
208(* complete induction on n, and then considers cases on whether n is prime   *)
209(* or not. The first case (n is prime) is trivial. In the second case, there *)
210(* must be an x that divides n, and x is not 1 or n. By DIVIDES_LEQ_OR_ZERO, *)
211(* n=0 or x <= n. If n=0, then 2 is a prime that divides 0. On the other     *)
212(* hand, if x <= n, there are two cases: if x<n then we can use the i.h. and *)
213(* by transitivity of divides we are done; otherwise, if x=n, then we have   *)
214(* a contradiction with the fact that x is not 1 or n.                       *)
215(*                                                                           *)
216(* In the following proof, METIS_TAC automatically considers cases on        *)
217(* whether n is prime or not.                                                *)
218(*---------------------------------------------------------------------------*)
219
220val PRIME_FACTOR = store_thm
221 ("PRIME_FACTOR",
222  ``!n. ~(n = 1) ==> ?p. prime p /\ divides p n``,
223  completeInduct_on `n` THEN
224  METIS_TAC [DIVIDES_REFL, prime_def, LESS_OR_EQ, PRIME_2,
225             DIVIDES_LEQ_OR_ZERO, DIVIDES_TRANS, ALL_DIVIDES_0]);
226
227(*---------------------------------------------------------------------------*)
228(* For every number there is a larger prime.                                    *)
229(*---------------------------------------------------------------------------*)
230
231val EUCLID = store_thm
232("EUCLID",
233 ``!n. ?p. n < p /\ prime p``,
234CCONTR_TAC
235THEN
236   `?n. !p. n < p ==> ~prime p`  by METIS_TAC[]                  THEN
237   `~(FACT n + 1 = 1)`           by RW_TAC arith_ss
238                                    [FACT_LESS,NOT_ZERO_LT_ZERO] THEN
239   `?p. prime p /\
240        divides p (FACT n + 1)`  by METIS_TAC [PRIME_FACTOR]     THEN
241   `0 < p`                       by METIS_TAC [PRIME_POS]        THEN
242   `p <= n`                      by METIS_TAC [NOT_LESS]         THEN
243   `divides p (FACT n)`          by METIS_TAC [LEQ_DIVIDES_FACT] THEN
244   `divides p 1`                 by METIS_TAC [DIVIDES_ADD_2]    THEN
245   `p = 1`                       by METIS_TAC [DIVIDES_ONE]      THEN
246   `~prime p`                    by METIS_TAC [NOT_PRIME_1]
247);
248
249(*---------------------------------------------------------------------------*)
250(* The sequence of primes.                                                   *)
251(*---------------------------------------------------------------------------*)
252
253val PRIMES_def = new_recursive_definition
254 {name = "PRIMES_def",
255  rec_axiom = prim_recTheory.num_Axiom,
256  def = ``(PRIMES 0 = 2) /\
257          (PRIMES (SUC n) = LEAST p. prime p /\ PRIMES n < p)``};
258
259val primePRIMES = Q.store_thm
260("primePRIMES",
261 `!n. prime (PRIMES n)`,
262 Cases THEN RW_TAC arith_ss [PRIMES_def,PRIME_2] THEN
263 LEAST_ELIM_TAC THEN
264 RW_TAC bool_ss [] THEN
265 METIS_TAC [EUCLID]);
266
267val INFINITE_PRIMES = Q.store_thm
268("INFINITE_PRIMES",
269 `!n. PRIMES n < PRIMES (SUC n)`,
270 RW_TAC arith_ss [PRIMES_def] THEN
271 LEAST_ELIM_TAC THEN
272 RW_TAC bool_ss [] THEN
273 METIS_TAC [EUCLID]);
274
275val LT_PRIMES = Q.store_thm
276("LT_PRIMES",
277 `!m n. m < n ==> PRIMES m < PRIMES n`,
278 Induct_on `n` THEN RW_TAC arith_ss [] THEN
279 METIS_TAC [INFINITE_PRIMES,LESS_TRANS,LESS_THM]);
280
281val PRIMES_11 = Q.store_thm
282("PRIMES_11",
283 `!m n. (PRIMES m = PRIMES n) ==> (m=n)`,
284 METIS_TAC [DECIDE ``a < b ==> a<>b``,LT_PRIMES,
285            DECIDE `` !m n. m < n \/ (m=n) \/ n < m``]);
286
287val INDEX_LESS_PRIMES = Q.store_thm
288("INDEX_LESS_PRIMES",
289 `!n. n < PRIMES n`,
290 Induct THEN RW_TAC arith_ss [PRIMES_def] THEN
291 LEAST_ELIM_TAC THEN CONJ_TAC THENL
292 [METIS_TAC [INFINITE_PRIMES,primePRIMES], RW_TAC arith_ss []]);
293
294val EUCLID_PRIMES = Q.store_thm
295("EUCLID_PRIMES",
296 `!n. ?i. n < PRIMES i`,
297 SPOSE_NOT_THEN (MP_TAC o REWRITE_RULE [NOT_LESS]) THEN STRIP_TAC THEN
298 METIS_TAC [INDEX_LESS_PRIMES,DECIDE ``a <= b /\ b < a ==> F``]);
299
300val NEXT_LARGER_PRIME = Q.store_thm
301("NEXT_LARGER_PRIME",
302 `!n. ?i. n < PRIMES i /\ !j. j < i ==> PRIMES j <= n`,
303 GEN_TAC THEN METIS_TAC [HO_MATCH_MP WOP (SPEC_ALL EUCLID_PRIMES),NOT_LESS]);
304
305val PRIMES_NO_GAP = Q.store_thm
306("PRIMES_NO_GAP",
307 `!n p. PRIMES n < p /\ p < PRIMES (SUC n) /\ prime p ==> F`,
308 RW_TAC bool_ss [PRIMES_def,GSYM IMP_DISJ_THM] THEN POP_ASSUM MP_TAC THEN
309 LEAST_ELIM_TAC THEN METIS_TAC[INFINITE_PRIMES,primePRIMES]);
310
311val PRIMES_ONTO = Q.store_thm
312("PRIMES_ONTO",
313 `!p. prime p ==> ?i. PRIMES i = p`,
314 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
315 STRIP_ASSUME_TAC (Q.SPEC `p` NEXT_LARGER_PRIME) THEN
316 Cases_on `i` THENL
317 [METIS_TAC [DECIDE``p < 2 = (p=0) \/ (p=1)``,
318             NOT_PRIME_0,NOT_PRIME_1,PRIME_2,PRIMES_def],
319  `PRIMES n < p` by METIS_TAC [DECIDE ``n < SUC n``,LESS_OR_EQ] THEN
320  METIS_TAC [PRIMES_NO_GAP]]);
321
322val PRIME_INDEX = Q.store_thm
323("PRIME_INDEX",
324 `!p. prime p = ?i. p = PRIMES i`,
325 METIS_TAC [PRIMES_ONTO,primePRIMES]);
326
327val ONE_LT_PRIMES = Q.store_thm
328("ONE_LT_PRIMES",
329 `!n. 1 < PRIMES n`,
330  METIS_TAC [primePRIMES, NOT_PRIME_0, NOT_PRIME_1,
331             DECIDE ``(x=0) \/ (x=1) \/ 1<x``]);
332
333val ZERO_LT_PRIMES = Q.store_thm
334("ZERO_LT_PRIMES",
335 `!n. 0 < PRIMES n`,
336  METIS_TAC [LESS_TRANS, ONE_LT_PRIMES, DECIDE ``0 < 1``]);
337
338(*---------------------------------------------------------------------------*)
339(* Directly computable version of divides                                    *)
340(*---------------------------------------------------------------------------*)
341
342val compute_divides = Q.store_thm
343("compute_divides",
344 `!a b. divides a b =
345        if a=0 then (b=0) else
346        if a=1 then T else
347        if b=0 then T else
348        (b MOD a = 0)`,
349  RW_TAC arith_ss [divides_def]
350   THEN EQ_TAC
351   THEN RW_TAC arith_ss [] THENL
352   [Cases_on `q` THENL
353     [RW_TAC arith_ss [],
354      `0<a` by RW_TAC arith_ss [] THEN
355      METIS_TAC [MOD_MULT, MULT_SYM, ADD_CLAUSES]],
356    Q.EXISTS_TAC `b` THEN RW_TAC arith_ss [],
357    Q.EXISTS_TAC `0` THEN RW_TAC arith_ss [],
358    `0<a` by RW_TAC arith_ss [] THEN
359     let val MOD_P_inst = BETA_RULE (Q.SPECL[`\x. (x = 0)`,`b`,`a`] MOD_P)
360     in METIS_TAC [MOD_P_inst,MULT_SYM, ADD_CLAUSES]
361     end]);
362
363val _ =
364 computeLib.add_persistent_funs
365     ["compute_divides"];
366
367val _ = export_theory();
368