dividesScript.sml
1Theory divides[bare]
2Ancestors
3 prim_rec arithmetic numeral[qualified]
4Libs
5 HolKernel Parse boolLib BasicProvers simpLib computeLib
6 boolSimps metisLib numLib TotalDefn
7
8val CALC = EQT_ELIM o reduceLib.REDUCE_CONV;
9val ARITH_TAC = CONV_TAC Arith.ARITH_CONV;
10val DECIDE = EQT_ELIM o Arith.ARITH_CONV;
11
12fun DECIDE_TAC (g as (asl,_)) =
13 ((MAP_EVERY UNDISCH_TAC (filter numSimps.is_arith asl) THEN
14 CONV_TAC Arith.ARITH_CONV)
15 ORELSE tautLib.TAUT_TAC) g;
16
17val decide_tac = DECIDE_TAC;
18val metis_tac = METIS_TAC;
19val arith_ss = numLib.arith_ss;
20val rw = srw_tac[];
21val qabbrev_tac = Q.ABBREV_TAC;
22val qspec_then = Q.SPEC_THEN;
23
24fun simp ths g ctxt =
25 asm_simp_tac (srw_ss_of ctxt ++ numSimps.ARITH_ss) ths g ctxt
26fun gvs ths g ctxt = global_simp_tac {droptrues = true, elimvars = true,
27 oldestfirst = true, strip = true}
28 (srw_ss_of ctxt ++ numSimps.ARITH_ss)
29 ths g ctxt
30
31fun fs l g ctxt = FULL_SIMP_TAC (srw_ss_of ctxt ++ numSimps.ARITH_ss) l g ctxt;
32
33val op >~ = Q.>~
34
35val ARW = RW_TAC arith_ss;
36
37Definition divides_def[nocompute]:
38 divides a b = ?q. b = q*a
39End
40
41Theorem ALL_DIVIDES_0[simp]:
42 !a. divides a 0
43Proof
44 METIS_TAC[divides_def,MULT_CLAUSES]
45QED
46
47Theorem ZERO_DIVIDES[simp]:
48 divides 0 m = (m = 0)
49Proof
50 SRW_TAC [][divides_def]
51QED
52
53Theorem DIVIDES_REFL[simp]:
54 !a. divides a a
55Proof
56 METIS_TAC[divides_def,MULT_CLAUSES]
57QED
58
59Theorem DIVIDES_TRANS:
60 !a b c. divides a b /\ divides b c ==> divides a c
61Proof
62 METIS_TAC [divides_def,MULT_ASSOC]
63QED
64
65Theorem ONE_DIVIDES_ALL[simp]:
66 !a. divides 1 a
67Proof
68 METIS_TAC[divides_def,MULT_CLAUSES]
69QED
70
71Theorem DIVIDES_ONE[simp]:
72 !x. divides x 1 = (x = 1)
73Proof
74 METIS_TAC [divides_def,MULT_CLAUSES,MULT_EQ_1]
75QED
76
77Theorem DIVIDES_ADD_1:
78 !a b c. divides a b /\ divides a c ==> divides a (b+c)
79Proof
80 METIS_TAC[divides_def,RIGHT_ADD_DISTRIB]
81QED
82
83Theorem DIVIDES_ADD_2:
84 !a b c. divides a b /\ divides a (b+c) ==> divides a c
85Proof
86 ARW[divides_def] THEN EXISTS_TAC ``q' - q`` THEN ARW[RIGHT_SUB_DISTRIB]
87QED
88
89Theorem DIVIDES_SUB:
90 !a b c. divides a b /\ divides a c ==> divides a (b-c)
91Proof
92 METIS_TAC[divides_def,RIGHT_SUB_DISTRIB]
93QED
94
95Theorem DIVIDES_LE:
96 !a b. 0<b /\ divides a b ==> a <= b
97Proof
98 Cases_on `a` THEN ARW[divides_def] THEN Cases_on `q` THENL
99 [METIS_TAC [MULT_CLAUSES,LESS_REFL],
100 ARW[MULT_CLAUSES]]
101QED
102
103Theorem DIVIDES_LEQ_OR_ZERO:
104 !m n. divides m n ==> m <= n \/ (n = 0)
105Proof
106 ARW [divides_def]
107 THEN Cases_on `q`
108 THEN ARW [MULT_CLAUSES]
109QED
110
111Theorem NOT_LT_DIVIDES:
112 !a b. 0<b /\ b<a ==> ~(divides a b)
113Proof
114 METIS_TAC[DIVIDES_LE,LESS_EQ_ANTISYM]
115QED
116
117Theorem DIVIDES_ANTISYM:
118 !a b. divides a b /\ divides b a ==> (a = b)
119Proof
120 REPEAT Cases
121 THEN TRY (ARW[divides_def] THEN NO_TAC)
122 THEN METIS_TAC [LESS_EQUAL_ANTISYM,DIVIDES_LE,prim_recTheory.LESS_0]
123QED
124
125Theorem DIVIDES_MULT:
126 !a b c. divides a b ==> divides a (b*c)
127Proof
128 METIS_TAC[divides_def,MULT_SYM,MULT_ASSOC]
129QED
130
131Theorem DIVIDES_MULT_LEFT:
132 !n m. divides (n * m) m <=> (m = 0) \/ (n = 1)
133Proof
134 SIMP_TAC arith_ss [FORALL_AND_THM, EQ_IMP_THM, DISJ_IMP_THM,
135 ALL_DIVIDES_0, DIVIDES_REFL] THEN
136 SIMP_TAC bool_ss [divides_def] THEN REPEAT STRIP_TAC THEN
137 `m * 1 = m * (n * q)` by
138 (POP_ASSUM (CONV_TAC o LAND_CONV o
139 ONCE_REWRITE_CONV o C cons []) THEN
140 ASM_SIMP_TAC bool_ss [MULT_CLAUSES] THEN
141 CONV_TAC (AC_CONV(MULT_ASSOC, MULT_COMM))) THEN
142 `(m = 0) \/ (n * q = 1)` by METIS_TAC [EQ_MULT_LCANCEL] THEN
143 ASM_SIMP_TAC bool_ss [] THEN
144 METIS_TAC [MULT_EQ_1]
145QED
146
147Theorem DIVIDES_EXP[local]:
148 !a b x. 0 < x /\ divides a b ==> divides a (b ** x)
149Proof
150 Cases_on `x` THEN RW_TAC arith_ss [EXP] THEN METIS_TAC [DIVIDES_MULT]
151QED
152
153Theorem DIVIDES_FACT:
154 !b. 0<b ==> divides b (FACT b)
155Proof
156 Cases_on `b` THEN ARW[FACT, divides_def] THEN METIS_TAC [MULT_COMM]
157QED
158
159Theorem LEQ_DIVIDES_FACT:
160 !m n. 0 < m /\ m <= n ==> divides m (FACT n)
161Proof
162 RW_TAC arith_ss [LESS_EQ_EXISTS] >>
163 Q.RENAME_TAC [‘divides m (FACT (m + d))’] >>
164 Induct_on ‘d’ >>
165 METIS_TAC [FACT, LESS_REFL, num_CASES, DIVIDES_MULT,
166 MULT_COMM, DIVIDES_REFL, ADD_CLAUSES]
167QED
168
169(* Idea: a convenient form of divides_def. *)
170
171(* Theorem: n divides (m * n) /\ n divides (n * m) *)
172(* Proof: by divides_def. *)
173Theorem factor_divides[simp]:
174 !m n. divides n (m * n) /\ divides n (n * m)
175Proof
176 METIS_TAC[divides_def, MULT_COMM]
177QED
178
179Theorem EXP_DIVIDES:
180 divides (a ** b) (a ** c) <=>
181 b <= c \/ a = 0 /\ 0 < c \/ a = 0 /\ b = 0 \/ a = 1
182Proof
183 SRW_TAC [][divides_def, EQ_IMP_THM] >> simp[] >~
184 [‘a ** c = r * a ** b’]
185 >- (Cases_on ‘a = 0’ >> gvs[] >> CCONTR_TAC >>
186 gvs[NOT_LESS, NOT_LESS_EQUAL] >>
187 ‘?d. b = c + d /\ 0 < d’ by (Q.EXISTS_TAC ‘b - c’ >> simp[]) >>
188 gvs[EXP_ADD] >>
189 ‘a ** c = 0 \/ r * a ** d = 1’
190 by (irule $ iffLR EQ_MULT_LCANCEL >> REWRITE_TAC [MULT_RIGHT_1] >>
191 Q.PAT_X_ASSUM ‘a ** c = _’ (fn th => CONV_TAC (RHS_CONV (K th))) >>
192 simp[]) >>
193 gvs[]) >~
194 [‘b <= c’]
195 >- (gvs[LESS_EQ_EXISTS, EXP_ADD] >> METIS_TAC[MULT_COMM]) >>
196 Q.EXISTS_TAC ‘0’ >> simp[]
197QED
198
199Theorem DIVIDES_MOD_0:
200 !p n. 0 < p ==> (divides p n <=> n MOD p = 0)
201Proof
202 SRW_TAC[][divides_def, EQ_IMP_THM, PULL_EXISTS] >>
203 Q.EXISTS_TAC ‘n DIV p’ >>
204 METIS_TAC [ADD_CLAUSES, DIVISION]
205QED
206
207Theorem DIVIDES_DIV:
208 !p n. 0 < p /\ divides p n ==> p * (n DIV p) = n
209Proof
210 rpt strip_tac >> drule_then (Q.SPEC_THEN ‘n’ strip_assume_tac) DIVISION >>
211 drule_all_then assume_tac DIVIDES_MOD_0 >> gvs[]
212QED
213
214Theorem DIVIDES_COMMON_MULT_I:
215 !a b c. divides a b ==> divides (c * a) (c * b)
216Proof
217 SRW_TAC[][divides_def] >> simp[EXISTS_OR_THM]
218QED
219
220Theorem DIVIDES_MULT_RCANCEL:
221 !a b c. c <> 0 ==> (divides (a * c) (b * c) <=> divides a b)
222Proof
223 SRW_TAC[][divides_def, EQ_IMP_THM] >> gvs[EXISTS_OR_THM] >>
224 ‘b * c = (a * q) * c’ by METIS_TAC[MULT_ASSOC, MULT_COMM] >>
225 METIS_TAC[EQ_MULT_RCANCEL]
226QED
227
228Theorem DIVIDES_MULT_LCANCEL:
229 !a b c. c <> 0 ==> (divides (c * a) (c * b) <=> divides a b)
230Proof
231 METIS_TAC[MULT_COMM, DIVIDES_MULT_RCANCEL]
232QED
233
234Theorem DIVIDES_PROD:
235 !a b c d. divides a c /\ divides b d ==> divides (a * b) (c * d)
236Proof
237 SRW_TAC[][divides_def] >> Q.RENAME_TAC [‘(q1 * a) * (q2 * b)’] >>
238 Q.EXISTS_TAC ‘q1 * q2’ >> simp[]
239QED
240
241(*---------------------------------------------------------------------------*)
242(* Definition and trivial facts about primality. *)
243(*---------------------------------------------------------------------------*)
244
245Definition prime_def[nocompute]:
246 prime a <=> a <> 1 /\ !b. divides b a ==> (b=a) \/ (b=1)
247End
248
249
250Theorem NOT_PRIME_0[simp]:
251 ~prime 0
252Proof
253 ARW [prime_def, ALL_DIVIDES_0]
254QED
255
256Theorem NOT_PRIME_1[simp]:
257 ~prime 1
258Proof
259 ARW [prime_def, DIVIDES_LE]
260QED
261
262Theorem PRIME_2[simp]:
263 prime 2
264Proof
265 RW_TAC arith_ss [prime_def] THEN
266 `0 < b /\ b <= 2` by METIS_TAC [DIVIDES_LE, ZERO_DIVIDES,
267 CALC ``0<2``,NOT_ZERO_LT_ZERO] THEN
268 NTAC 2 (POP_ASSUM MP_TAC) THEN ARITH_TAC
269QED
270
271Theorem PRIME_3[simp]:
272 prime 3
273Proof
274 RW_TAC arith_ss [prime_def] THEN
275 `b <= 3` by RW_TAC arith_ss [DIVIDES_LE] THEN
276 `(b=0) \/ (b=1) \/ (b=2) \/ (b=3)` by (POP_ASSUM MP_TAC THEN ARITH_TAC) THEN
277 RW_TAC arith_ss [] THENL
278 [FULL_SIMP_TAC arith_ss [ZERO_DIVIDES],
279 FULL_SIMP_TAC arith_ss [divides_def]]
280QED
281
282Theorem PRIME_POS:
283 !p. prime p ==> 0<p
284Proof
285 Cases THEN RW_TAC arith_ss [NOT_PRIME_0]
286QED
287
288Theorem ONE_LT_PRIME:
289 !p. prime p ==> 1 < p
290Proof
291 METIS_TAC [NOT_PRIME_0, NOT_PRIME_1,
292 DECIDE ``(p=0) \/ (p=1) \/ 1 < p``]
293QED
294
295Theorem prime_divides_only_self:
296 !m n. prime m /\ prime n /\ divides m n ==> m=n
297Proof
298 RW_TAC arith_ss [divides_def] THEN
299 `m<>1` by METIS_TAC [NOT_PRIME_0,NOT_PRIME_1] THEN
300 SIMP_TAC (srw_ss()) [] THEN
301 Q.PAT_X_ASSUM `prime (m*q)` MP_TAC THEN
302 RW_TAC arith_ss [prime_def, divides_def, PULL_EXISTS] THEN
303 METIS_TAC []
304QED
305
306Theorem prime_MULT:
307 !n m. prime (n * m) <=>
308 ((n <= m ==> (n = 1 /\ prime m)) /\
309 (m <= n ==> (m = 1 /\ prime n)))
310Proof
311 `!m n. m <= n ==> (prime (m * n) <=> m = 1 /\ prime n)`
312 suffices_by METIS_TAC[LESS_EQ_CASES, MULT_COMM]
313 \\ gen_tac
314 \\ Cases_on`m = 0` \\ ASM_SIMP_TAC arith_ss [NOT_PRIME_0]
315 \\ RW_TAC arith_ss [EQ_IMP_THM]
316 \\ FULL_SIMP_TAC arith_ss [prime_def]
317 >- (
318 `divides m (m * n)` by METIS_TAC[factor_divides]
319 \\ CCONTR_TAC
320 \\ `m = m * n` by METIS_TAC[]
321 \\ `~(m < m * n)` by DECIDE_TAC
322 \\ FULL_SIMP_TAC arith_ss [])
323 \\ rpt strip_tac \\ FULL_SIMP_TAC arith_ss []
324 \\ Cases_on`b=1` \\ ASM_SIMP_TAC arith_ss []
325 \\ `divides b (m * n)` by METIS_TAC[DIVIDES_MULT, MULT_COMM]
326 \\ `b = m * n` by METIS_TAC[]
327 \\ FULL_SIMP_TAC arith_ss [DIVIDES_MULT_LEFT]
328QED
329
330(*---------------------------------------------------------------------------*)
331(* Every number has a prime factor, except for 1. The proof proceeds by a *)
332(* complete induction on n, and then considers cases on whether n is prime *)
333(* or not. The first case (n is prime) is trivial. In the second case, there *)
334(* must be an x that divides n, and x is not 1 or n. By DIVIDES_LEQ_OR_ZERO, *)
335(* n=0 or x <= n. If n=0, then 2 is a prime that divides 0. On the other *)
336(* hand, if x <= n, there are two cases: if x<n then we can use the i.h. and *)
337(* by transitivity of divides we are done; otherwise, if x=n, then we have *)
338(* a contradiction with the fact that x is not 1 or n. *)
339(* *)
340(* In the following proof, METIS_TAC automatically considers cases on *)
341(* whether n is prime or not. *)
342(*---------------------------------------------------------------------------*)
343
344Theorem PRIME_FACTOR:
345 !n. ~(n = 1) ==> ?p. prime p /\ divides p n
346Proof
347 completeInduct_on `n` THEN
348 METIS_TAC [DIVIDES_REFL, prime_def, LESS_OR_EQ, PRIME_2,
349 DIVIDES_LEQ_OR_ZERO, DIVIDES_TRANS, ALL_DIVIDES_0]
350QED
351
352(* ----------------------------------------------------------------------
353 For every number there is a larger prime.
354 ---------------------------------------------------------------------- *)
355
356Theorem EUCLID:
357 !n. ?p. n < p /\ prime p
358Proof
359CCONTR_TAC
360THEN
361 `?n. !p. n < p ==> ~prime p` by METIS_TAC[] THEN
362 `~(FACT n + 1 = 1)` by RW_TAC arith_ss
363 [FACT_LESS,NOT_ZERO_LT_ZERO] THEN
364 `?p. prime p /\
365 divides p (FACT n + 1)` by METIS_TAC [PRIME_FACTOR] THEN
366 `0 < p` by METIS_TAC [PRIME_POS] THEN
367 `p <= n` by METIS_TAC [NOT_LESS] THEN
368 `divides p (FACT n)` by METIS_TAC [LEQ_DIVIDES_FACT] THEN
369 `divides p 1` by METIS_TAC [DIVIDES_ADD_2] THEN
370 `p = 1` by METIS_TAC [DIVIDES_ONE] THEN
371 `~prime p` by METIS_TAC [NOT_PRIME_1]
372QED
373
374(*---------------------------------------------------------------------------*)
375(* The sequence of primes. *)
376(*---------------------------------------------------------------------------*)
377
378Definition PRIMES_def[nocompute]:
379 (PRIMES 0 = 2) /\
380 (PRIMES (SUC n) = LEAST p. prime p /\ PRIMES n < p)
381End
382
383Theorem primePRIMES:
384 !n. prime (PRIMES n)
385Proof
386 Cases THEN RW_TAC arith_ss [PRIMES_def,PRIME_2] THEN
387 LEAST_ELIM_TAC THEN
388 RW_TAC bool_ss [] THEN
389 METIS_TAC [EUCLID]
390QED
391
392Theorem INFINITE_PRIMES:
393 !n. PRIMES n < PRIMES (SUC n)
394Proof
395 RW_TAC arith_ss [PRIMES_def] THEN
396 LEAST_ELIM_TAC THEN
397 RW_TAC bool_ss [] THEN
398 METIS_TAC [EUCLID]
399QED
400
401Theorem LT_PRIMES:
402 !m n. m < n ==> PRIMES m < PRIMES n
403Proof
404 Induct_on `n` THEN RW_TAC arith_ss [] THEN
405 METIS_TAC [INFINITE_PRIMES,LESS_TRANS,LESS_THM]
406QED
407
408Theorem PRIMES_11:
409 !m n. (PRIMES m = PRIMES n) ==> (m=n)
410Proof
411 METIS_TAC [DECIDE ``a < b ==> a<>b``,LT_PRIMES,
412 DECIDE `` !m n. m < n \/ (m=n) \/ n < m``]
413QED
414
415Theorem INDEX_LESS_PRIMES:
416 !n. n < PRIMES n
417Proof
418 Induct THEN RW_TAC arith_ss [PRIMES_def] THEN
419 LEAST_ELIM_TAC THEN CONJ_TAC THENL
420 [METIS_TAC [INFINITE_PRIMES,primePRIMES], RW_TAC arith_ss []]
421QED
422
423Theorem EUCLID_PRIMES:
424 !n. ?i. n < PRIMES i
425Proof
426 SPOSE_NOT_THEN (MP_TAC o REWRITE_RULE [NOT_LESS]) THEN STRIP_TAC THEN
427 METIS_TAC [INDEX_LESS_PRIMES,DECIDE ``a <= b /\ b < a ==> F``]
428QED
429
430Theorem NEXT_LARGER_PRIME:
431 !n. ?i. n < PRIMES i /\ !j. j < i ==> PRIMES j <= n
432Proof
433 GEN_TAC THEN METIS_TAC [HO_MATCH_MP WOP (SPEC_ALL EUCLID_PRIMES),NOT_LESS]
434QED
435
436Theorem PRIMES_NO_GAP:
437 !n p. PRIMES n < p /\ p < PRIMES (SUC n) /\ prime p ==> F
438Proof
439 RW_TAC bool_ss [PRIMES_def,GSYM IMP_DISJ_THM] THEN POP_ASSUM MP_TAC THEN
440 LEAST_ELIM_TAC THEN METIS_TAC[INFINITE_PRIMES,primePRIMES]
441QED
442
443Theorem PRIMES_ONTO:
444 !p. prime p ==> ?i. PRIMES i = p
445Proof
446 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
447 STRIP_ASSUME_TAC (Q.SPEC `p` NEXT_LARGER_PRIME) THEN
448 Cases_on `i` THENL
449 [METIS_TAC [DECIDE``p < 2 <=> (p=0) \/ (p=1)``,
450 NOT_PRIME_0,NOT_PRIME_1,PRIME_2,PRIMES_def],
451 `PRIMES n < p` by METIS_TAC [DECIDE ``n < SUC n``,LESS_OR_EQ] THEN
452 METIS_TAC [PRIMES_NO_GAP]]
453QED
454
455Theorem PRIME_INDEX:
456 !p. prime p = ?i. p = PRIMES i
457Proof
458 METIS_TAC [PRIMES_ONTO,primePRIMES]
459QED
460
461Theorem ONE_LT_PRIMES:
462 !n. 1 < PRIMES n
463Proof
464 METIS_TAC [primePRIMES, NOT_PRIME_0, NOT_PRIME_1,
465 DECIDE ``(x=0) \/ (x=1) \/ 1<x``]
466QED
467
468Theorem ZERO_LT_PRIMES:
469 !n. 0 < PRIMES n
470Proof
471 METIS_TAC [LESS_TRANS, ONE_LT_PRIMES, DECIDE ``0 < 1``]
472QED
473
474(* Theorem: !n. ?p. prime p /\ n < p *)
475(* Proof:
476 Since ?i. n < PRIMES i by NEXT_LARGER_PRIME
477 and prime (PRIMES i) by primePRIMES
478 Take p = PRIMES i.
479*)
480Theorem prime_always_bigger:
481 !n. ?p. prime p /\ n < p
482Proof
483 metis_tac[NEXT_LARGER_PRIME, primePRIMES]
484QED
485
486(*---------------------------------------------------------------------------*)
487(* Directly computable version of divides *)
488(*---------------------------------------------------------------------------*)
489
490Theorem compute_divides[compute]:
491 !a b. divides a b =
492 if a=0 then (b=0)
493 else if a=1 then T
494 else if b=0 then T
495 else b MOD a = 0
496Proof
497 RW_TAC arith_ss [divides_def]
498 THEN EQ_TAC
499 THEN RW_TAC arith_ss [] THENL [
500 Cases_on ‘q’ THENL [
501 RW_TAC arith_ss [],
502 ‘0<a’ by RW_TAC arith_ss [] THEN
503 METIS_TAC [MOD_MULT, MULT_SYM, ADD_CLAUSES]
504 ],
505 Q.EXISTS_TAC ‘b’ THEN RW_TAC arith_ss [],
506 Q.EXISTS_TAC ‘0’ THEN RW_TAC arith_ss [],
507 ‘0<a’ by RW_TAC arith_ss [] THEN
508 METIS_TAC [BETA_RULE (Q.SPECL[‘\x. (x = 0)’,‘b’,‘a’] MOD_P),MULT_COMM,
509 ADD_CLAUSES]
510 ]
511QED
512
513(* ------------------------------------------------------------------------- *)
514(* DIVIDES Theorems (from examples/algebra) *)
515(* ------------------------------------------------------------------------- *)
516
517(* temporarily make divides an infix *)
518val _ = temp_set_fixity "divides" (Infixl 480);
519
520(* Theorem: 0 < n ==> ((m DIV n = 0) <=> m < n) *)
521(* Proof:
522 If part: 0 < n /\ m DIV n = 0 ==> m < n
523 Since m = m DIV n * n + m MOD n) /\ (m MOD n < n) by DIVISION, 0 < n
524 so m = 0 * n + m MOD n by m DIV n = 0
525 = 0 + m MOD n by MULT
526 = m MOD n by ADD
527 Since m MOD n < n, m < n.
528 Only-if part: 0 < n /\ m < n ==> m DIV n = 0
529 True by LESS_DIV_EQ_ZERO.
530*)
531Theorem DIV_EQUAL_0:
532 !m n. 0 < n ==> ((m DIV n = 0) <=> m < n)
533Proof
534 rw[EQ_IMP_THM] >-
535 metis_tac[DIVISION, MULT, ADD] >>
536 rw[LESS_DIV_EQ_ZERO]
537QED
538(* This is an improvement of
539 arithmeticTheory.DIV_EQ_0 = |- 1 < b ==> (n DIV b = 0 <=> n < b) *)
540
541(* Theorem: 0 < m /\ m <= n ==> 0 < n DIV m *)
542(* Proof:
543 Note n = (n DIV m) * m + n MOD m /\
544 n MDO m < m by DIVISION, 0 < m
545 ==> n MOD m < n by m <= n
546 Thus 0 < (n DIV m) * m by inequality
547 so 0 < n DIV m by ZERO_LESS_MULT
548*)
549Theorem DIV_POS:
550 !m n. 0 < m /\ m <= n ==> 0 < n DIV m
551Proof
552 rpt strip_tac >>
553 imp_res_tac (DIVISION |> SPEC_ALL) >>
554 first_x_assum (qspec_then `n` strip_assume_tac) >>
555 first_x_assum (qspec_then `n` strip_assume_tac) >>
556 `0 < (n DIV m) * m` by decide_tac >>
557 metis_tac[ZERO_LESS_MULT]
558QED
559
560(* Theorem: 0 < z ==> (x DIV z = y DIV z <=> x - x MOD z = y - y MOD z) *)
561(* Proof:
562 Note x = (x DIV z) * z + x MOD z by DIVISION
563 and y = (y DIV z) * z + y MDO z by DIVISION
564 x DIV z = y DIV z
565 <=> (x DIV z) * z = (y DIV z) * z by EQ_MULT_RCANCEL
566 <=> x - x MOD z = y - y MOD z by arithmetic
567*)
568Theorem DIV_EQ:
569 !x y z. 0 < z ==> (x DIV z = y DIV z <=> x - x MOD z = y - y MOD z)
570Proof
571 rpt strip_tac >>
572 `x = (x DIV z) * z + x MOD z` by simp[DIVISION] >>
573 `y = (y DIV z) * z + y MOD z` by simp[DIVISION] >>
574 `x DIV z = y DIV z <=> (x DIV z) * z = (y DIV z) * z` by simp[] >>
575 decide_tac
576QED
577
578(* Theorem: a MOD n + b < n ==> (a + b) DIV n = a DIV n *)
579(* Proof:
580 Note 0 < n by a MOD n + b < n
581 a + b
582 = ((a DIV n) * n + a MOD n) + b by DIVISION, 0 < n
583 = (a DIV n) * n + (a MOD n + b) by ADD_ASSOC
584
585 If a MOD n + b < n,
586 Then (a + b) DIV n = a DIV n /\
587 (a + b) MOD n = a MOD n + b by DIVMOD_UNIQ
588*)
589Theorem ADD_DIV_EQ:
590 !n a b. a MOD n + b < n ==> (a + b) DIV n = a DIV n
591Proof
592 rpt strip_tac >>
593 `0 < n` by decide_tac >>
594 `a = (a DIV n) * n + a MOD n` by simp[DIVISION] >>
595 `a + b = (a DIV n) * n + (a MOD n + b)` by decide_tac >>
596 metis_tac[DIVMOD_UNIQ]
597QED
598
599(* Theorem: 0 < y /\ x <= y * z ==> x DIV y <= z *)
600(* Proof:
601 x <= y * z
602 ==> x DIV y <= (y * z) DIV y by DIV_LE_MONOTONE, 0 < y
603 = z by MULT_TO_DIV
604*)
605Theorem DIV_LE:
606 !x y z. 0 < y /\ x <= y * z ==> x DIV y <= z
607Proof
608 metis_tac[DIV_LE_MONOTONE, MULT_TO_DIV]
609QED
610
611(* Theorem: 0 < n ==> !x y. (x * n = y) ==> (x = y DIV n) *)
612(* Proof:
613 x = (x * n + 0) DIV n by DIV_MULT, 0 < n
614 = (x * n) DIV n by ADD_0
615*)
616Theorem DIV_SOLVE:
617 !n. 0 < n ==> !x y. (x * n = y) ==> (x = y DIV n)
618Proof
619 metis_tac[DIV_MULT, ADD_0]
620QED
621
622(* Theorem: 0 < n ==> !x y. (n * x = y) ==> (x = y DIV n) *)
623(* Proof: by DIV_SOLVE, MULT_COMM *)
624Theorem DIV_SOLVE_COMM:
625 !n. 0 < n ==> !x y. (n * x = y) ==> (x = y DIV n)
626Proof
627 rw[DIV_SOLVE, MULT_TO_DIV]
628QED
629
630(* Theorem: 1 < n ==> (1 DIV n = 0) *)
631(* Proof:
632 Since 1 = (1 DIV n) * n + (1 MOD n) by DIVISION, 0 < n.
633 and 1 MOD n = 1 by ONE_MOD, 1 < n.
634 thus (1 DIV n) * n = 0 by arithmetic
635 or 1 DIV n = 0 since n <> 0 by MULT_EQ_0
636*)
637Theorem ONE_DIV:
638 !n. 1 < n ==> (1 DIV n = 0)
639Proof
640 rpt strip_tac >>
641 `0 < n /\ n <> 0` by decide_tac >>
642 `1 = (1 DIV n) * n + (1 MOD n)` by rw[DIVISION] >>
643 `_ = (1 DIV n) * n + 1` by rw[ONE_MOD] >>
644 `(1 DIV n) * n = 0` by decide_tac >>
645 metis_tac[MULT_EQ_0]
646QED
647
648(* Theorem: ODD n ==> !m. m divides n ==> ODD m *)
649(* Proof:
650 Since m divides n
651 ==> ?q. n = q * m by divides_def
652 By contradiction, suppose ~ODD m.
653 Then EVEN m by ODD_EVEN
654 and EVEN (q * m) = EVEN n by EVEN_MULT
655 or ~ODD n by ODD_EVEN
656 This contradicts with ODD n.
657*)
658Theorem DIVIDES_ODD:
659 !n. ODD n ==> !m. m divides n ==> ODD m
660Proof
661 metis_tac[divides_def, EVEN_MULT, EVEN_ODD]
662QED
663
664(* Note: For EVEN n, m divides n cannot conclude EVEN m.
665Example: EVEN 2 or ODD 3 both divides EVEN 6.
666*)
667
668(* Theorem: EVEN m ==> !n. m divides n ==> EVEN n*)
669(* Proof:
670 Since m divides n
671 ==> ?q. n = q * m by divides_def
672 Given EVEN m
673 Then EVEN (q * m) = n by EVEN_MULT
674*)
675Theorem DIVIDES_EVEN:
676 !m. EVEN m ==> !n. m divides n ==> EVEN n
677Proof
678 metis_tac[divides_def, EVEN_MULT]
679QED
680
681(* Theorem: EVEN n = 2 divides n *)
682(* Proof:
683 EVEN n
684 <=> n MOD 2 = 0 by EVEN_MOD2
685 <=> 2 divides n by DIVIDES_MOD_0, 0 < 2
686*)
687Theorem EVEN_ALT:
688 !n. EVEN n = 2 divides n
689Proof
690 rw[EVEN_MOD2, DIVIDES_MOD_0]
691QED
692
693(* Theorem: ODD n = ~(2 divides n) *)
694(* Proof:
695 Note n MOD 2 < 2 by MOD_LESS
696 and !x. x < 2 <=> (x = 0) \/ (x = 1) by arithmetic
697 ODD n
698 <=> n MOD 2 = 1 by ODD_MOD2
699 <=> ~(2 divides n) by DIVIDES_MOD_0, 0 < 2
700 Or,
701 ODD n = ~(EVEN n) by ODD_EVEN
702 = ~(2 divides n) by EVEN_ALT
703*)
704Theorem ODD_ALT:
705 !n. ODD n = ~(2 divides n)
706Proof
707 metis_tac[EVEN_ODD, EVEN_ALT]
708QED
709
710(* Theorem: 0 < n ==> !q. (q DIV n) * n <= q *)
711(* Proof:
712 Since q = (q DIV n) * n + q MOD n by DIVISION
713 Thus (q DIV n) * n <= q by discarding remainder
714*)
715Theorem DIV_MULT_LE:
716 !n. 0 < n ==> !q. (q DIV n) * n <= q
717Proof
718 rpt strip_tac >>
719 `q = (q DIV n) * n + q MOD n` by rw[DIVISION] >>
720 decide_tac
721QED
722
723(* Theorem: 0 < n ==> !q. n divides q <=> ((q DIV n) * n = q) *)
724(* Proof:
725 If part: n divides q ==> q DIV n * n = q
726 q = (q DIV n) * n + q MOD n by DIVISION
727 = (q DIV n) * n + 0 by MOD_EQ_0_DIVISOR, divides_def
728 = (q DIV n) * n by ADD_0
729 Only-if part: q DIV n * n = q ==> n divides q
730 True by divides_def
731*)
732Theorem DIV_MULT_EQ:
733 !n. 0 < n ==> !q. n divides q <=> ((q DIV n) * n = q)
734Proof
735 metis_tac[divides_def, DIVISION, MOD_EQ_0_DIVISOR, ADD_0]
736QED
737(* same as DIVIDES_EQN below *)
738
739(* Proof:
740 If n DIV y = 0,
741 Then 0 <= n DIV x is trivially true.
742 If n DIV y <> 0,
743 (n DIV y) * x <= (n DIV y) * y by LE_MULT_LCANCEL, x ≤ y, n DIV y ≠ 0
744 <= n by DIV_MULT_LE
745 Hence (n DIV y) * x <= n by LESS_EQ_TRANS
746 Then ((n DIV y) * x) DIV x <= n DIV x by DIV_LE_MONOTONE
747 or n DIV y <= n DIV x by MULT_DIV
748*)
749Theorem DIV_LE_MONOTONE_REVERSE:
750 !x y. 0 < x /\ 0 < y /\ x <= y ==> !n. n DIV y <= n DIV x
751Proof
752 rpt strip_tac >>
753 Cases_on `n DIV y = 0` >-
754 decide_tac >>
755 `(n DIV y) * x <= (n DIV y) * y` by rw[LE_MULT_LCANCEL] >>
756 `(n DIV y) * y <= n` by rw[DIV_MULT_LE] >>
757 `(n DIV y) * x <= n` by decide_tac >>
758 `((n DIV y) * x) DIV x <= n DIV x` by rw[DIV_LE_MONOTONE] >>
759 metis_tac[MULT_DIV]
760QED
761
762(* Theorem: n divides m <=> (m = (m DIV n) * n) *)
763(* Proof:
764 Since n divides m <=> m MOD n = 0 by DIVIDES_MOD_0
765 and m = (m DIV n) * n + (m MOD n) by DIVISION
766 If part: n divides m ==> m = m DIV n * n
767 This is true by ADD_0
768 Only-if part: m = m DIV n * n ==> n divides m
769 Since !x y. x + y = x <=> y = 0 by ADD_INV_0
770 The result follows.
771*)
772Theorem DIVIDES_EQN:
773 !n. 0 < n ==> !m. n divides m <=> (m = (m DIV n) * n)
774Proof
775 metis_tac[DIVISION, DIVIDES_MOD_0, ADD_0, ADD_INV_0]
776QED
777
778(* Theorem: 0 < n ==> !m. n divides m <=> (m = n * (m DIV n)) *)
779(* Proof: vy DIVIDES_EQN, MULT_COMM *)
780Theorem DIVIDES_EQN_COMM:
781 !n. 0 < n ==> !m. n divides m <=> (m = n * (m DIV n))
782Proof
783 rw_tac std_ss[DIVIDES_EQN, MULT_COMM]
784QED
785
786(* Proof:
787 Apply DIV_SUB |> GEN_ALL |> SPEC ``1`` |> REWRITE_RULE[MULT_RIGHT_1];
788 val it = |- !n m. 0 < n /\ n <= m ==> ((m - n) DIV n = m DIV n - 1): thm
789*)
790Theorem SUB_DIV =
791 DIV_SUB |> GEN ``n:num`` |> GEN ``m:num`` |> GEN ``q:num`` |> SPEC ``1``
792 |> REWRITE_RULE[MULT_RIGHT_1];
793(* = |- !m n. 0 < n /\ n <= m ==> ((m - n) DIV n = m DIV n - 1) *)
794
795(* Theorem: 0 < n ==> !k m. (m MOD n = 0) ==> ((k * n = m) <=> (k = m DIV n)) *)
796(* Proof:
797 Note m MOD n = 0
798 ==> n divides m by DIVIDES_MOD_0, 0 < n
799 ==> m = (m DIV n) * n by DIVIDES_EQN, 0 < n
800 k * n = m
801 <=> k * n = (m DIV n) * n by above
802 <=> k = (m DIV n) by EQ_MULT_RCANCEL, n <> 0.
803*)
804Theorem DIV_EQ_MULT:
805 !n. 0 < n ==> !k m. (m MOD n = 0) ==> ((k * n = m) <=> (k = m DIV n))
806Proof
807 rpt strip_tac >>
808 `n <> 0` by decide_tac >>
809 `m = (m DIV n) * n` by rw[GSYM DIVIDES_EQN, DIVIDES_MOD_0] >>
810 metis_tac[EQ_MULT_RCANCEL]
811QED
812
813(* Theorem: 0 < n ==> !k m. (m MOD n = 0) ==> (k * n < m <=> k < m DIV n) *)
814(* Proof:
815 k * n < m
816 <=> k * n < (m DIV n) * n by DIVIDES_EQN, DIVIDES_MOD_0, 0 < n
817 <=> k < m DIV n by LT_MULT_RCANCEL, n <> 0
818*)
819Theorem MULT_LT_DIV:
820 !n. 0 < n ==> !k m. (m MOD n = 0) ==> (k * n < m <=> k < m DIV n)
821Proof
822 metis_tac[DIVIDES_EQN, DIVIDES_MOD_0, LT_MULT_RCANCEL, NOT_ZERO_LT_ZERO]
823QED
824
825(* Theorem: 0 < n ==> !k m. (m MOD n = 0) ==> (m <= n * k <=> m DIV n <= k) *)
826(* Proof:
827 m <= n * k
828 <=> (m DIV n) * n <= n * k by DIVIDES_EQN, DIVIDES_MOD_0, 0 < n
829 <=> (m DIV n) * n <= k * n by MULT_COMM
830 <=> m DIV n <= k by LE_MULT_RCANCEL, n <> 0
831*)
832Theorem LE_MULT_LE_DIV:
833 !n. 0 < n ==> !k m. (m MOD n = 0) ==> (m <= n * k <=> m DIV n <= k)
834Proof
835 metis_tac[DIVIDES_EQN, DIVIDES_MOD_0, MULT_COMM, LE_MULT_RCANCEL,
836 NOT_ZERO_LT_ZERO]
837QED
838
839(* Theorem: 0 < m ==> ((n DIV m = 0) /\ (n MOD m = 0) <=> (n = 0)) *)
840(* Proof:
841 If part: (n DIV m = 0) /\ (n MOD m = 0) ==> (n = 0)
842 Note n DIV m = 0 ==> n < m by DIV_EQUAL_0
843 Thus n MOD m = n by LESS_MOD
844 or n = 0
845 Only-if part: 0 DIV m = 0 by ZERO_DIV
846 0 MOD m = 0 by ZERO_MOD
847*)
848Theorem DIV_MOD_EQ_0:
849 !m n. 0 < m ==> ((n DIV m = 0) /\ (n MOD m = 0) <=> (n = 0))
850Proof
851 rpt strip_tac >>
852 rw[EQ_IMP_THM] >>
853 metis_tac[DIV_EQUAL_0, LESS_MOD]
854QED
855
856(* Theorem: 0 < n /\ a ** n divides b ==> a divides b *)
857(* Proof:
858 Note ?k. n = SUC k by num_CASES, n <> 0
859 and ?q. b = q * (a ** n) by divides_def
860 = q * (a * a ** k) by EXP
861 = (q * a ** k) * a by arithmetic
862 Thus a divides b by divides_def
863*)
864Theorem EXP_divides : (* was: EXP_DIVIDES *)
865 !a b n. 0 < n /\ a ** n divides b ==> a divides b
866Proof
867 rpt strip_tac >>
868 `?k. n = SUC k` by metis_tac[num_CASES, NOT_ZERO_LT_ZERO] >>
869 `?q. b = q * a ** n` by rw[GSYM divides_def] >>
870 `_ = q * (a * a ** k)` by rw[EXP] >>
871 `_ = (q * a ** k) * a` by decide_tac >>
872 metis_tac[divides_def]
873QED
874
875(* Theorem: n divides m ==> !k. n divides (k * m) *)
876(* Proof:
877 n divides m ==> ?q. m = q * n by divides_def
878 Hence k * m = k * (q * n)
879 = (k * q) * n by MULT_ASSOC
880 or n divides (k * m) by divides_def
881*)
882Theorem DIVIDES_MULTIPLE:
883 !m n. n divides m ==> !k. n divides (k * m)
884Proof
885 metis_tac[divides_def, MULT_ASSOC]
886QED
887
888Theorem divisor_pos:
889 !m n. 0 < n /\ m divides n ==> 0 < m
890Proof
891 metis_tac[ZERO_DIVIDES, NOT_ZERO_LT_ZERO]
892QED
893
894(* Theorem: 0 < n /\ m divides n ==> 0 < m /\ m <= n *)
895(* Proof:
896 Since 0 < n /\ m divides n,
897 then 0 < m by divisor_pos
898 and m <= n by DIVIDES_LE
899*)
900Theorem divides_pos:
901 !m n. 0 < n /\ m divides n ==> 0 < m /\ m <= n
902Proof
903 metis_tac[divisor_pos, DIVIDES_LE]
904QED
905
906(* Theorem: 0 < n /\ m divides n ==> (n DIV (n DIV m) = m) *)
907(* Proof:
908 Since 0 < n /\ m divides n, 0 < m by divisor_pos
909 Hence n = (n DIV m) * m by DIVIDES_EQN, 0 < m
910 Note 0 < n DIV m, otherwise contradicts 0 < n by MULT
911 Now n = m * (n DIV m) by MULT_COMM
912 = m * (n DIV m) + 0 by ADD_0
913 Therefore n DIV (n DIV m) = m by DIV_UNIQUE
914*)
915Theorem divide_by_cofactor:
916 !m n. 0 < n /\ m divides n ==> (n DIV (n DIV m) = m)
917Proof
918 rpt strip_tac >>
919 `0 < m` by metis_tac[divisor_pos] >>
920 `n = (n DIV m) * m` by rw[GSYM DIVIDES_EQN] >>
921 `0 < n DIV m` by metis_tac[MULT, NOT_ZERO_LT_ZERO] >>
922 `n = m * (n DIV m) + 0` by metis_tac[MULT_COMM, ADD_0] >>
923 metis_tac[DIV_UNIQUE]
924QED
925
926(* Theorem: 0 < n ==> !a b. a divides b ==> a divides b ** n *)
927(* Proof:
928 Since 0 < n, n = SUC m for some m.
929 thus b ** n = b ** (SUC m)
930 = b * b ** m by EXP
931 Now a divides b means
932 ?k. b = k * a by divides_def
933 so b ** n
934 = k * a * b ** m
935 = (k * b ** m) * a by MULT_COMM, MULT_ASSOC
936 Hence a divides (b ** n) by divides_def
937*)
938Theorem divides_exp:
939 !n. 0 < n ==> !a b. a divides b ==> a divides b ** n
940Proof
941 rw_tac std_ss[divides_def] >>
942 `n <> 0` by decide_tac >>
943 `?m. n = SUC m` by metis_tac[num_CASES] >>
944 `(q * a) ** n = q * a * (q * a) ** m` by rw[EXP] >>
945 `_ = q * (q * a) ** m * a` by rw[MULT_COMM, MULT_ASSOC] >>
946 metis_tac[]
947QED
948
949(* Note; converse need prime divisor:
950DIVIDES_EXP_BASE
951 |- !a b n. prime a /\ 0 < n ==> (a divides b <=> a divides b ** n)
952Counter-example for a general base: 12 divides 36 = 6^2, but ~(12 divides 6)
953*)
954
955(* Better than:
956
957 DIVIDES_ADD_1 |- !a b c. a divides b /\ a divides c ==> a divides b + c *)
958
959(* Theorem: c divides a /\ c divides b ==> !h k. c divides (h * a + k * b) *)
960(* Proof:
961 Since c divides a, ?u. a = u * c by divides_def
962 and c divides b, ?v. b = v * c by divides_def
963 h * a + k * b
964 = h * (u * c) + k * (v * c) by above
965 = h * u * c + k * v * c by MULT_ASSOC
966 = (h * u + k * v) * c by RIGHT_ADD_DISTRIB
967 Hence c divides (h * a + k * b) by divides_def
968*)
969Theorem divides_linear:
970 !a b c. c divides a /\ c divides b ==> !h k. c divides (h * a + k * b)
971Proof
972 rw_tac std_ss[divides_def] >>
973 metis_tac[RIGHT_ADD_DISTRIB, MULT_ASSOC]
974QED
975
976(* Proof:
977 If c = 0,
978 0 divides a ==> a = 0 by ZERO_DIVIDES
979 0 divides b ==> b = 0 by ZERO_DIVIDES
980 Thus d = 0 by arithmetic
981 and 0 divides 0 by ZERO_DIVIDES
982 If c <> 0, 0 < c.
983 c divides a ==> (a MOD c = 0) by DIVIDES_MOD_0
984 c divides b ==> (b MOD c = 0) by DIVIDES_MOD_0
985 Hence 0 = (h * a) MOD c by MOD_TIMES2, ZERO_MOD
986 = (0 + d MOD c) MOD c by MOD_PLUS, MOD_TIMES2, ZERO_MOD
987 = d MOD c by MOD_MOD
988 or c divides d by DIVIDES_MOD_0
989*)
990Theorem divides_linear_sub:
991 ∀a b c. c divides a ∧ c divides b ⇒ ∀h k d. h * a = k * b + d ⇒ c divides d
992Proof
993 rpt strip_tac >>
994 Cases_on `c = 0` >| [
995 `(a = 0) /\ (b = 0)` by metis_tac[ZERO_DIVIDES] >>
996 `d = 0` by rw_tac arith_ss[] >>
997 rw[],
998 `0 < c` by decide_tac >>
999 `(a MOD c = 0) /\ (b MOD c = 0)` by rw[GSYM DIVIDES_MOD_0] >>
1000 `0 = (h * a) MOD c` by metis_tac[MOD_TIMES2, ZERO_MOD, MULT_0] >>
1001 `_ = (0 + d MOD c) MOD c`
1002 by metis_tac[MOD_PLUS, MOD_TIMES2, ZERO_MOD, MULT_0] >>
1003 `_ = d MOD c` by rw[MOD_MOD] >>
1004 rw[DIVIDES_MOD_0]
1005 ]
1006QED
1007
1008(* ------------------------------------------------------------------------- *)
1009(* Factorial *)
1010(* ------------------------------------------------------------------------- *)
1011
1012(* Theorem: FACT 0 = 1 *)
1013(* Proof: by FACT *)
1014Theorem FACT_0:
1015 FACT 0 = 1
1016Proof
1017 EVAL_TAC
1018QED
1019
1020(* Theorem: FACT 1 = 1 *)
1021(* Proof:
1022 FACT 1
1023 = FACT (SUC 0) by ONE
1024 = (SUC 0) * FACT 0 by FACT
1025 = (SUC 0) * 1 by FACT
1026 = 1 by ONE
1027*)
1028Theorem FACT_1:
1029 FACT 1 = 1
1030Proof
1031 EVAL_TAC
1032QED
1033
1034(* Theorem: FACT 2 = 2 *)
1035(* Proof:
1036 FACT 2
1037 = FACT (SUC 1) by TWO
1038 = (SUC 1) * FACT 1 by FACT
1039 = (SUC 1) * 1 by FACT_1
1040 = 2 by TWO
1041*)
1042Theorem FACT_2:
1043 FACT 2 = 2
1044Proof
1045 EVAL_TAC
1046QED
1047
1048(* Theorem: (FACT n = 1) <=> n <= 1 *)
1049(* Proof:
1050 If n = 0,
1051 LHS = (FACT 0 = 1) = T by FACT_0
1052 RHS = 0 <= 1 = T by arithmetic
1053 If n <> 0, n = SUC m by num_CASES
1054 LHS = FACT (SUC m) = 1
1055 <=> (SUC m) * FACT m = 1 by FACT
1056 <=> SUC m = 1 /\ FACT m = 1 by MULT_EQ_1
1057 <=> m = 0 /\ FACT m = 1 by m = PRE 1 = 0
1058 <=> m = 0 by FACT_0
1059 RHS = SUC m <= 1
1060 <=> ~(1 <= m) by NOT_LEQ
1061 <=> m < 1 by NOT_LESS_EQUAL
1062 <=> m = 0 by arithmetic
1063*)
1064Theorem FACT_EQ_1:
1065 !n. (FACT n = 1) <=> n <= 1
1066Proof
1067 rpt strip_tac >>
1068 Cases_on `n` >>
1069 rw[FACT_0] >>
1070 rw[FACT] >>
1071 `!m. SUC m <= 1 <=> (m = 0)` by decide_tac >>
1072 metis_tac[FACT_0]
1073QED
1074
1075(* Theorem: (FACT n = n) <=> (n = 1) \/ (n = 2) *)
1076(* Proof:
1077 If part: (FACT n = n) ==> (n = 1) \/ (n = 2)
1078 Note n <> 0 by FACT_0: FACT 0 = 1
1079 ==> ?m. n = SUC m by num_CASES
1080 Thus SUC m * FACT m = SUC m by FACT
1081 = SUC m * 1 by MULT_RIGHT_1
1082 ==> FACT m = 1 by EQ_MULT_LCANCEL, SUC_NOT
1083 or m <= 1 by FACT_EQ_1
1084 Thus m = 0 or 1 by arithmetic
1085 or n = 1 or 2 by ONE, TWO
1086
1087 Only-if part: (FACT 1 = 1) /\ (FACT 2 = 2)
1088 Note FACT 1 = 1 by FACT_1
1089 and FACT 2 = 2 by FACT_2
1090*)
1091Theorem FACT_EQ_SELF:
1092 !n. (FACT n = n) <=> (n = 1) \/ (n = 2)
1093Proof
1094 rw[EQ_IMP_THM] >| [
1095 `n <> 0` by metis_tac[FACT_0, DECIDE``1 <> 0``] >>
1096 `?m. n = SUC m` by metis_tac[num_CASES] >>
1097 fs[FACT] >>
1098 `FACT m = 1` by metis_tac[MULT_LEFT_1, EQ_MULT_RCANCEL, SUC_NOT] >>
1099 `m <= 1` by rw[GSYM FACT_EQ_1] >>
1100 decide_tac,
1101 rw[FACT_1],
1102 rw[FACT_2]
1103 ]
1104QED
1105
1106(* Theorem: 0 < n ==> n <= FACT n *)
1107(* Proof:
1108 Note n <> 0 by 0 < n
1109 ==> ?m. n = SUC m by num_CASES
1110 Thus FACT n
1111 = FACT (SUC m) by n = SUC m
1112 = (SUC m) * FACT m by FACT_LESS: 0 < FACT m
1113 >= (SUC m) by LE_MULT_CANCEL_LBARE
1114 >= n by n = SUC m
1115*)
1116Theorem FACT_GE_SELF:
1117 !n. 0 < n ==> n <= FACT n
1118Proof
1119 rpt strip_tac >>
1120 `?m. n = SUC m` by metis_tac[num_CASES, NOT_ZERO_LT_ZERO] >>
1121 rw[FACT] >>
1122 rw[FACT_LESS]
1123QED
1124
1125(* Theorem: 0 < n ==> (FACT (n-1) = FACT n DIV n) *)
1126(* Proof:
1127 Since n = SUC(n-1) by SUC_PRE, 0 < n.
1128 and FACT n = n * FACT (n-1) by FACT
1129 = FACT (n-1) * n by MULT_COMM
1130 = FACT (n-1) * n + 0 by ADD_0
1131 Hence FACT (n-1) = FACT n DIV n by DIV_UNIQUE, 0 < n.
1132*)
1133Theorem FACT_DIV:
1134 !n. 0 < n ==> (FACT (n-1) = FACT n DIV n)
1135Proof
1136 rpt strip_tac >>
1137 `n = SUC(n-1)` by decide_tac >>
1138 `FACT n = n * FACT (n-1)` by metis_tac[FACT] >>
1139 `_ = FACT (n-1) * n + 0` by rw[MULT_COMM] >>
1140 metis_tac[DIV_UNIQUE]
1141QED