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