gcdsetScript.sml
1Theory gcdset[bare]
2Ancestors
3 arithmetic divides pred_set gcd
4Libs
5 HolKernel Parse boolLib BasicProvers simpLib metisLib
6 pred_setSimps TotalDefn numSimps[qualified]
7
8val ARITH_ss = numSimps.ARITH_ss;
9val arith_ss = srw_ss() ++ ARITH_ss;
10val std_ss = arith_ss;
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 qabbrev_tac = Q.ABBREV_TAC;
20val qexists_tac = Q.EXISTS_TAC;
21val rw = SRW_TAC [ARITH_ss];
22
23Definition gcdset_def[nocompute]:
24 gcdset s =
25 if (s = {}) \/ (s = {0}) then 0
26 else MAX_SET ({ n | n <= MIN_SET (s DELETE 0) } INTER
27 { d | !e. e IN s ==> divides d e })
28End
29
30Theorem FINITE_LEQ_MIN_SET[local]:
31 FINITE { n | n <= MIN_SET (s DELETE 0) }
32Proof
33 Q_TAC SUFF_TAC `
34 { n | n <= MIN_SET (s DELETE 0) } = count (MIN_SET (s DELETE 0) + 1)
35 ` THEN1 SRW_TAC [][] THEN
36 SRW_TAC [ARITH_ss][EXTENSION]
37QED
38
39Theorem NON_EMPTY_INTERSECTION[local]:
40 s <> {} /\ s <> {0} ==>
41 { n | n <= MIN_SET (s DELETE 0) } INTER
42 { d | !e. e IN s ==> divides d e} <> {}
43Proof
44 STRIP_TAC THEN SIMP_TAC (srw_ss()) [EXTENSION] THEN Q.EXISTS_TAC `1` THEN
45 SRW_TAC [][] THEN DEEP_INTRO_TAC MIN_SET_ELIM THEN
46 SRW_TAC [ARITH_ss][EXTENSION] THEN
47 FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN METIS_TAC []
48QED
49
50Theorem gcdset_divides:
51 !e. e IN s ==> divides (gcdset s) e
52Proof
53 SRW_TAC[][gcdset_def] THEN FULL_SIMP_TAC (srw_ss()) [] THEN
54 DEEP_INTRO_TAC MAX_SET_ELIM THEN
55 ASM_SIMP_TAC (srw_ss()) [FINITE_INTER, FINITE_LEQ_MIN_SET,
56 NON_EMPTY_INTERSECTION]
57QED
58
59val DECIDE = numLib.ARITH_PROVE
60Theorem gcdset_greatest:
61 (!e. e IN s ==> divides g e) ==> divides g (gcdset s)
62Proof
63 SRW_TAC [][gcdset_def] THEN FULL_SIMP_TAC (srw_ss()) [] THEN
64 DEEP_INTRO_TAC MAX_SET_ELIM THEN
65 ASM_SIMP_TAC (srw_ss()) [NON_EMPTY_INTERSECTION, FINITE_LEQ_MIN_SET] THEN
66 Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN
67 Q.ABBREV_TAC `L = lcm g m` THEN
68 `(!e. e IN s ==> divides L e) /\ divides m L /\ divides g L`
69 by METIS_TAC [gcdTheory.LCM_IS_LEAST_COMMON_MULTIPLE] THEN
70 `?x. x IN s /\ x <> 0`
71 by (FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN METIS_TAC []) THEN
72 `L <= MIN_SET (s DELETE 0)`
73 by (DEEP_INTRO_TAC MIN_SET_ELIM THEN SRW_TAC [][EXTENSION]
74 THEN1 METIS_TAC [] THEN
75 METIS_TAC [DIVIDES_LE, DECIDE ``x <> 0 <=> 0 < x``]) THEN
76 `L <= m` by METIS_TAC[] THEN
77 Q_TAC SUFF_TAC `0 < m /\ 0 < g` THEN1
78 METIS_TAC [LCM_LE, DECIDE ``x <= y /\ y <= x ==> (x = y)``] THEN
79 METIS_TAC [ZERO_DIVIDES, DECIDE ``x <> 0 <=> 0 < x``]
80QED
81
82Theorem gcdset_EMPTY[simp]:
83 gcdset {} = 0
84Proof
85 SRW_TAC [][gcdset_def]
86QED
87
88Theorem gcdset_INSERT[simp]:
89 gcdset (x INSERT s) = gcd x (gcdset s)
90Proof
91 Q.MATCH_ABBREV_TAC `G1 = G2` THEN
92 `(!e. e IN s ==> divides G1 e) /\ divides G1 x`
93 by METIS_TAC [IN_INSERT, gcdset_divides] THEN
94 `divides G2 x /\ divides G2 (gcdset s)`
95 by METIS_TAC [GCD_IS_GCD, is_gcd_def] THEN
96 MATCH_MP_TAC DIVIDES_ANTISYM THEN CONJ_TAC THENL [
97 Q_TAC SUFF_TAC `divides G1 (gcdset s)` THEN1
98 METIS_TAC [GCD_IS_GCD, is_gcd_def] THEN
99 SRW_TAC [][gcdset_greatest],
100 Q_TAC SUFF_TAC `!e. e IN s ==> divides G2 e` THEN1
101 METIS_TAC [IN_INSERT, gcdset_greatest] THEN
102 METIS_TAC [gcdset_divides, DIVIDES_TRANS]
103 ]
104QED
105
106(* ------------------------------------------------------------------------- *)
107(* Naturals -- counting from 1 rather than 0, and inclusive. *)
108(* ------------------------------------------------------------------------- *)
109
110(* Overload the set of natural numbers (like count) *)
111Overload natural = ``\n. IMAGE SUC (count n)``
112
113(* Theorem: j IN (natural n) <=> 0 < j /\ j <= n *)
114(* Proof:
115 Note j <> 0 by natural_not_0
116 j IN (natural n)
117 ==> j IN IMAGE SUC (count n) by notation
118 ==> ?x. x < n /\ (j = SUC x) by IN_IMAGE
119 Since SUC x <> 0 by numTheory.NOT_SUC
120 Hence j <> 0,
121 and x < n ==> SUC x < SUC n by LESS_MONO_EQ
122 or j < SUC n by above, j = SUC x
123 thus j <= n by prim_recTheory.LESS_THM
124*)
125Theorem natural_element:
126 !n j. j IN (natural n) <=> 0 < j /\ j <= n
127Proof
128 rw[EQ_IMP_THM] >>
129 `j <> 0` by decide_tac >>
130 `?m. j = SUC m` by metis_tac[num_CASES] >>
131 `m < n` by decide_tac >>
132 metis_tac[]
133QED
134
135(* Theorem: natural n = {j| 0 < j /\ j <= n} *)
136(* Proof: by natural_element, IN_IMAGE *)
137Theorem natural_property:
138 !n. natural n = {j| 0 < j /\ j <= n}
139Proof
140 rw[EXTENSION, natural_element]
141QED
142
143(* Theorem: FINITE (natural n) *)
144(* Proof: FINITE_COUNT, IMAGE_FINITE *)
145Theorem natural_finite:
146 !n. FINITE (natural n)
147Proof
148 rw[]
149QED
150
151(* Theorem: CARD (natural n) = n *)
152(* Proof:
153 CARD (natural n)
154 = CARD (IMAGE SUC (count n)) by notation
155 = CARD (count n) by CARD_IMAGE_SUC
156 = n by CARD_COUNT
157*)
158Theorem natural_card:
159 !n. CARD (natural n) = n
160Proof
161 rw[CARD_IMAGE_SUC]
162QED
163
164(* Theorem: 0 NOTIN (natural n) *)
165(* Proof: by NOT_SUC *)
166Theorem natural_not_0:
167 !n. 0 NOTIN (natural n)
168Proof
169 rw[]
170QED
171
172(* Theorem: natural 0 = {} *)
173(* Proof:
174 natural 0
175 = IMAGE SUC (count 0) by notation
176 = IMAGE SUC {} by COUNT_ZERO
177 = {} by IMAGE_EMPTY
178*)
179Theorem natural_0:
180 natural 0 = {}
181Proof
182 rw[]
183QED
184
185(* Theorem: natural 1 = {1} *)
186(* Proof:
187 natural 1
188 = IMAGE SUC (count 1) by notation
189 = IMAGE SUC {0} by count_add1
190 = {SUC 0} by IMAGE_DEF
191 = {1} by ONE
192*)
193Theorem natural_1:
194 natural 1 = {1}
195Proof
196 rw[EXTENSION, EQ_IMP_THM]
197QED
198
199(* Theorem: 0 < n ==> 1 IN (natural n) *)
200(* Proof: by natural_element, LESS_OR, ONE *)
201Theorem natural_has_1:
202 !n. 0 < n ==> 1 IN (natural n)
203Proof
204 rw[natural_element]
205QED
206
207(* Theorem: 0 < n ==> n IN (natural n) *)
208(* Proof: by natural_element *)
209Theorem natural_has_last:
210 !n. 0 < n ==> n IN (natural n)
211Proof
212 rw[natural_element]
213QED
214
215(* Theorem: natural (SUC n) = (SUC n) INSERT (natural n) *)
216(* Proof:
217 natural (SUC n)
218 <=> {j | 0 < j /\ j <= (SUC n)} by natural_property
219 <=> {j | 0 < j /\ (j <= n \/ (j = SUC n))} by LE
220 <=> {j | j IN (natural n) \/ (j = SUC n)} by natural_property
221 <=> (SUC n) INSERT (natural n) by INSERT_DEF
222*)
223Theorem natural_suc:
224 !n. natural (SUC n) = (SUC n) INSERT (natural n)
225Proof
226 rw[EXTENSION, EQ_IMP_THM]
227QED
228
229(* temporarily make divides an infix *)
230val _ = temp_set_fixity "divides" (Infixl 480);
231
232(* Theorem: 0 < n /\ a IN (natural n) /\ b divides a ==> b IN (natural n) *)
233(* Proof:
234 By natural_element, this is to show:
235 (1) 0 < a /\ b divides a ==> 0 < b
236 True by divisor_pos
237 (2) 0 < a /\ b divides a ==> b <= n
238 Since b divides a
239 ==> b <= a by DIVIDES_LE, 0 < a
240 ==> b <= n by LESS_EQ_TRANS
241*)
242Theorem natural_divisor_natural:
243 !n a b. 0 < n /\ a IN (natural n) /\ b divides a ==> b IN (natural n)
244Proof
245 rw[natural_element] >-
246 metis_tac[divisor_pos] >>
247 metis_tac[DIVIDES_LE, LESS_EQ_TRANS]
248QED
249
250(* Theorem: 0 < n /\ 0 < a /\ b IN (natural n) /\ a divides b ==> (b DIV a) IN (natural n) *)
251(* Proof:
252 Let c = b DIV a.
253 By natural_element, this is to show:
254 0 < a /\ 0 < b /\ b <= n /\ a divides b ==> 0 < c /\ c <= n
255 Since a divides b ==> b = c * a by DIVIDES_EQN, 0 < a
256 so b = a * c by MULT_COMM
257 or c divides b by divides_def
258 Thus 0 < c /\ c <= b by divides_pos
259 or c <= n by LESS_EQ_TRANS
260*)
261Theorem natural_cofactor_natural:
262 !n a b. 0 < n /\ 0 < a /\ b IN (natural n) /\ a divides b ==> (b DIV a) IN (natural n)
263Proof
264 rewrite_tac[natural_element] >>
265 ntac 4 strip_tac >>
266 qabbrev_tac `c = b DIV a` >>
267 `b = c * a` by rw[GSYM DIVIDES_EQN, Abbr`c`] >>
268 `c divides b` by metis_tac[divides_def, MULT_COMM] >>
269 `0 < c /\ c <= b` by metis_tac[divides_pos] >>
270 decide_tac
271QED
272
273(* Theorem: 0 < n /\ a divides n /\ b IN (natural n) /\ a divides b ==> (b DIV a) IN (natural (n DIV a)) *)
274(* Proof:
275 Let c = b DIV a.
276 By natural_element, this is to show:
277 0 < n /\ a divides b /\ 0 < b /\ b <= n /\ a divides b ==> 0 < c /\ c <= n DIV a
278 Note 0 < a by ZERO_DIVIES, 0 < n
279 Since a divides b ==> b = c * a by DIVIDES_EQN, 0 < a [1]
280 or c divides b by divides_def, MULT_COMM
281 Thus 0 < c, since 0 divides b means b = 0. by ZERO_DIVIDES, b <> 0
282 Now n = (n DIV a) * a by DIVIDES_EQN, 0 < a [2]
283 With b <= n, c * a <= (n DIV a) * a by [1], [2]
284 Hence c <= n DIV a by LE_MULT_RCANCEL, a <> 0
285*)
286Theorem natural_cofactor_natural_reduced:
287 !n a b. 0 < n /\ a divides n /\
288 b IN (natural n) /\ a divides b ==> (b DIV a) IN (natural (n DIV a))
289Proof
290 rewrite_tac[natural_element] >>
291 ntac 4 strip_tac >>
292 qabbrev_tac `c = b DIV a` >>
293 `a <> 0` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >>
294 `(b = c * a) /\ (n = (n DIV a) * a)` by rw[GSYM DIVIDES_EQN, Abbr`c`] >>
295 `c divides b` by metis_tac[divides_def, MULT_COMM] >>
296 `0 < c` by metis_tac[ZERO_DIVIDES, NOT_ZERO] >>
297 metis_tac[LE_MULT_RCANCEL]
298QED
299
300(* ------------------------------------------------------------------------- *)
301(* Coprimes *)
302(* ------------------------------------------------------------------------- *)
303
304(* Define the coprimes set: integers from 1 to n that are coprime to n *)
305(*
306val coprimes_def = zDefine `
307 coprimes n = {j | 0 < j /\ j <= n /\ coprime j n}
308`;
309*)
310(* Note: j <= n ensures that coprimes n is finite. *)
311(* Note: 0 < j is only to ensure coprimes 1 = {1} *)
312Definition coprimes_def[nocompute]:
313 coprimes n = {j | j IN (natural n) /\ coprime j n}
314End
315(* use zDefine as this is not computationally effective. *)
316
317(* Theorem: j IN coprimes n <=> 0 < j /\ j <= n /\ coprime j n *)
318(* Proof: by coprimes_def, natural_element *)
319Theorem coprimes_element:
320 !n j. j IN coprimes n <=> 0 < j /\ j <= n /\ coprime j n
321Proof
322 (rw[coprimes_def, natural_element] >> metis_tac[])
323QED
324
325(* Theorem: coprimes n = (natural n) INTER {j | coprime j n} *)
326(* Proof: by coprimes_def, EXTENSION, IN_INTER *)
327Theorem coprimes_alt[compute]:
328 !n. coprimes n = (natural n) INTER {j | coprime j n}
329Proof
330 rw[coprimes_def, EXTENSION]
331QED
332(* This is effective, put in computeLib. *)
333
334(*
335> EVAL ``coprimes 10``;
336val it = |- coprimes 10 = {9; 7; 3; 1}: thm
337*)
338
339(* Theorem: coprimes n SUBSET natural n *)
340(* Proof: by coprimes_def, SUBSET_DEF *)
341Theorem coprimes_subset:
342 !n. coprimes n SUBSET natural n
343Proof
344 rw[coprimes_def, SUBSET_DEF]
345QED
346
347(* Theorem: FINITE (coprimes n) *)
348(* Proof:
349 Since (coprimes n) SUBSET (natural n) by coprimes_subset
350 and !n. FINITE (natural n) by natural_finite
351 so FINITE (coprimes n) by SUBSET_FINITE
352*)
353Theorem coprimes_finite:
354 !n. FINITE (coprimes n)
355Proof
356 metis_tac[coprimes_subset, natural_finite, SUBSET_FINITE]
357QED
358
359(* Theorem: coprimes 0 = {} *)
360(* Proof:
361 By coprimes_element, 0 < j /\ j <= 0,
362 which is impossible, hence empty.
363*)
364Theorem coprimes_0:
365 coprimes 0 = {}
366Proof
367 rw[coprimes_element, EXTENSION]
368QED
369
370(* Theorem: coprimes 1 = {1} *)
371(* Proof:
372 By coprimes_element, 0 < j /\ j <= 1,
373 Only possible j is 1, and gcd 1 1 = 1.
374 *)
375Theorem coprimes_1:
376 coprimes 1 = {1}
377Proof
378 rw[coprimes_element, EXTENSION]
379QED
380
381(* Theorem: 0 < n ==> 1 IN (coprimes n) *)
382(* Proof: by coprimes_element, GCD_1 *)
383Theorem coprimes_has_1:
384 !n. 0 < n ==> 1 IN (coprimes n)
385Proof
386 rw[coprimes_element]
387QED
388
389(* Theorem: (coprimes n = {}) <=> (n = 0) *)
390(* Proof:
391 If part: coprimes n = {} ==> n = 0
392 By contradiction.
393 Suppose n <> 0, then 0 < n.
394 Then 1 IN (coprimes n) by coprimes_has_1
395 hence (coprimes n) <> {} by MEMBER_NOT_EMPTY
396 This contradicts (coprimes n) = {}.
397 Only-if part: n = 0 ==> coprimes n = {}
398 True by coprimes_0
399*)
400Theorem coprimes_eq_empty:
401 !n. (coprimes n = {}) <=> (n = 0)
402Proof
403 rw[EQ_IMP_THM] >-
404 metis_tac[coprimes_has_1, MEMBER_NOT_EMPTY, NOT_ZERO_LT_ZERO] >>
405 rw[coprimes_0]
406QED
407
408(* Theorem: 0 NOTIN (coprimes n) *)
409(* Proof:
410 By coprimes_element, 0 < j /\ j <= n,
411 Hence j <> 0, or 0 NOTIN (coprimes n)
412*)
413Theorem coprimes_no_0:
414 !n. 0 NOTIN (coprimes n)
415Proof
416 rw[coprimes_element]
417QED
418
419(* Theorem: 1 < n ==> n NOTIN coprimes n *)
420(* Proof:
421 By coprimes_element, 0 < j /\ j <= n /\ gcd j n = 1
422 If j = n, 1 = gcd j n = gcd n n = n by GCD_REF
423 which is excluded by 1 < n, so j <> n.
424*)
425Theorem coprimes_without_last:
426 !n. 1 < n ==> n NOTIN coprimes n
427Proof
428 rw[coprimes_element]
429QED
430
431(* Theorem: n IN coprimes n <=> (n = 1) *)
432(* Proof:
433 By coprimes_element, 0 < j /\ j <= n /\ gcd j n = 1
434 If n IN coprimes n, 1 = gcd j n = gcd n n = n by GCD_REF
435 If n = 1, 0 < n, n <= n, and gcd n n = n = 1 by GCD_REF
436*)
437Theorem coprimes_with_last:
438 !n. n IN coprimes n <=> (n = 1)
439Proof
440 rw[coprimes_element]
441QED
442
443(* Theorem: 1 < n ==> (n - 1) IN (coprimes n) *)
444(* Proof: by coprimes_element, coprime_PRE, GCD_SYM *)
445Theorem coprimes_has_last_but_1:
446 !n. 1 < n ==> (n - 1) IN (coprimes n)
447Proof
448 rpt strip_tac >>
449 `0 < n /\ 0 < n - 1` by decide_tac >>
450 rw[coprimes_element, coprime_PRE, GCD_SYM]
451QED
452
453(* Theorem: 1 < n ==> !j. j IN coprimes n ==> j < n *)
454(* Proof:
455 Since j IN coprimes n ==> j <= n by coprimes_element
456 If j = n, then gcd n n = n <> 1 by GCD_REF
457 Thus j <> n, or j < n. or by coprimes_without_last
458*)
459Theorem coprimes_element_less:
460 !n. 1 < n ==> !j. j IN coprimes n ==> j < n
461Proof
462 metis_tac[coprimes_element, coprimes_without_last, LESS_OR_EQ]
463QED
464
465(* Theorem: 1 < n ==> !j. j IN coprimes n <=> j < n /\ coprime j n *)
466(* Proof:
467 If part: j IN coprimes n ==> j < n /\ coprime j n
468 Note 0 < j /\ j <= n /\ coprime j n by coprimes_element
469 By contradiction, suppose n <= j.
470 Then j = n, but gcd n n = n <> 1 by GCD_REF
471 Only-if part: j < n /\ coprime j n ==> j IN coprimes n
472 This is to show:
473 0 < j /\ j <= n /\ coprime j n by coprimes_element
474 By contradiction, suppose ~(0 < j).
475 Then j = 0, but gcd 0 n = n <> 1 by GCD_0L
476*)
477Theorem coprimes_element_alt:
478 !n. 1 < n ==> !j. j IN coprimes n <=> j < n /\ coprime j n
479Proof
480 rw[coprimes_element] >>
481 `n <> 1` by decide_tac >>
482 rw[EQ_IMP_THM] >| [
483 spose_not_then strip_assume_tac >>
484 `j = n` by decide_tac >>
485 metis_tac[GCD_REF],
486 spose_not_then strip_assume_tac >>
487 `j = 0` by decide_tac >>
488 metis_tac[GCD_0L]
489 ]
490QED
491
492(* Theorem: 1 < n ==> (MAX_SET (coprimes n) = n - 1) *)
493(* Proof:
494 Let s = coprimes n, m = MAX_SET s.
495 Note (n - 1) IN s by coprimes_has_last_but_1, 1 < n
496 Hence s <> {} by MEMBER_NOT_EMPTY
497 and FINITE s by coprimes_finite
498 Since !x. x IN s ==> x < n by coprimes_element_less, 1 < n
499 also !x. x < n ==> x <= (n - 1) by SUB_LESS_OR
500 Therefore MAX_SET s = n - 1 by MAX_SET_TEST
501*)
502Theorem coprimes_max:
503 !n. 1 < n ==> (MAX_SET (coprimes n) = n - 1)
504Proof
505 rpt strip_tac >>
506 qabbrev_tac `s = coprimes n` >>
507 `(n - 1) IN s` by rw[coprimes_has_last_but_1, Abbr`s`] >>
508 `s <> {}` by metis_tac[MEMBER_NOT_EMPTY] >>
509 `FINITE s` by rw[coprimes_finite, Abbr`s`] >>
510 `!x. x IN s ==> x < n` by rw[coprimes_element_less, Abbr`s`] >>
511 `!x. x < n ==> x <= (n - 1)` by decide_tac >>
512 metis_tac[MAX_SET_TEST]
513QED
514
515(* ------------------------------------------------------------------------- *)
516(* Set GCD as Big Operator *)
517(* ------------------------------------------------------------------------- *)
518
519(* Big Operators:
520SUM_IMAGE_DEF |- !f s. SIGMA f s = ITSET (\e acc. f e + acc) s 0: thm
521PROD_IMAGE_DEF |- !f s. PI f s = ITSET (\e acc. f e * acc) s 1: thm
522*)
523
524(* Define big_gcd for a set *)
525Definition big_gcd_def:
526 big_gcd s = ITSET gcd s 0
527End
528
529(* Theorem: big_gcd {} = 0 *)
530(* Proof:
531 big_gcd {}
532 = ITSET gcd {} 0 by big_gcd_def
533 = 0 by ITSET_EMPTY
534*)
535Theorem big_gcd_empty:
536 big_gcd {} = 0
537Proof
538 rw[big_gcd_def, ITSET_EMPTY]
539QED
540
541(* Theorem: big_gcd {x} = x *)
542(* Proof:
543 big_gcd {x}
544 = ITSET gcd {x} 0 by big_gcd_def
545 = gcd x 0 by ITSET_SING
546 = x by GCD_0R
547*)
548Theorem big_gcd_sing:
549 !x. big_gcd {x} = x
550Proof
551 rw[big_gcd_def, ITSET_SING]
552QED
553
554(* Theorem: FINITE s /\ x NOTIN s ==> (big_gcd (x INSERT s) = gcd x (big_gcd s)) *)
555(* Proof:
556 Note big_gcd s = ITSET gcd s 0 by big_lcm_def
557 Since !x y z. gcd x (gcd y z) = gcd y (gcd x z) by GCD_ASSOC_COMM
558 The result follows by ITSET_REDUCTION
559*)
560Theorem big_gcd_reduction:
561 !s x. FINITE s /\ x NOTIN s ==> (big_gcd (x INSERT s) = gcd x (big_gcd s))
562Proof
563 rw[big_gcd_def, ITSET_REDUCTION, GCD_ASSOC_COMM]
564QED
565
566(* Theorem: FINITE s ==> !x. x IN s ==> (big_gcd s) divides x *)
567(* Proof:
568 By finite induction on s.
569 Base: x IN {} ==> big_gcd {} divides x
570 True since x IN {} = F by MEMBER_NOT_EMPTY
571 Step: !x. x IN s ==> big_gcd s divides x ==>
572 e NOTIN s /\ x IN (e INSERT s) ==> big_gcd (e INSERT s) divides x
573 Since e NOTIN s,
574 so big_gcd (e INSERT s) = gcd e (big_gcd s) by big_gcd_reduction
575 By IN_INSERT,
576 If x = e,
577 to show: gcd e (big_gcd s) divides e, true by GCD_IS_GREATEST_COMMON_DIVISOR
578 If x <> e, x IN s,
579 to show gcd e (big_gcd s) divides x,
580 Since (big_gcd s) divides x by induction hypothesis, x IN s
581 and (big_gcd s) divides gcd e (big_gcd s) by GCD_IS_GREATEST_COMMON_DIVISOR
582 so gcd e (big_gcd s) divides x by DIVIDES_TRANS
583*)
584Theorem big_gcd_is_common_divisor:
585 !s. FINITE s ==> !x. x IN s ==> (big_gcd s) divides x
586Proof
587 Induct_on `FINITE` >>
588 rpt strip_tac >-
589 metis_tac[MEMBER_NOT_EMPTY] >>
590 metis_tac[big_gcd_reduction, IN_INSERT, GCD_IS_GREATEST_COMMON_DIVISOR, DIVIDES_TRANS]
591QED
592
593(* Theorem: FINITE s ==> !m. (!x. x IN s ==> m divides x) ==> m divides (big_gcd s) *)
594(* Proof:
595 By finite induction on s.
596 Base: m divides big_gcd {}
597 Since big_gcd {} = 0 by big_gcd_empty
598 Hence true by ALL_DIVIDES_0
599 Step: !m. (!x. x IN s ==> m divides x) ==> m divides big_gcd s ==>
600 e NOTIN s /\ !x. x IN e INSERT s ==> m divides x ==> m divides big_gcd (e INSERT s)
601 Note x IN e INSERT s ==> x = e \/ x IN s by IN_INSERT
602 Put x = e, then m divides e by x divides m, x = e
603 Put x IN s, then m divides big_gcd s by induction hypothesis
604 Therefore, m divides gcd e (big_gcd s) by GCD_IS_GREATEST_COMMON_DIVISOR
605 or m divides big_gcd (e INSERT s) by big_gcd_reduction, e NOTIN s
606*)
607Theorem big_gcd_is_greatest_common_divisor:
608 !s. FINITE s ==> !m. (!x. x IN s ==> m divides x) ==> m divides (big_gcd s)
609Proof
610 Induct_on `FINITE` >>
611 rpt strip_tac >-
612 rw[big_gcd_empty] >>
613 metis_tac[big_gcd_reduction, GCD_IS_GREATEST_COMMON_DIVISOR, IN_INSERT]
614QED
615
616(* Theorem: FINITE s ==> !x. big_gcd (x INSERT s) = gcd x (big_gcd s) *)
617(* Proof:
618 If x IN s,
619 Then (big_gcd s) divides x by big_gcd_is_common_divisor
620 gcd x (big_gcd s)
621 = gcd (big_gcd s) x by GCD_SYM
622 = big_gcd s by divides_iff_gcd_fix
623 = big_gcd (x INSERT s) by ABSORPTION
624 If x NOTIN s, result is true by big_gcd_reduction
625*)
626Theorem big_gcd_insert:
627 !s. FINITE s ==> !x. big_gcd (x INSERT s) = gcd x (big_gcd s)
628Proof
629 rpt strip_tac >>
630 Cases_on `x IN s` >-
631 metis_tac[big_gcd_is_common_divisor, divides_iff_gcd_fix, ABSORPTION, GCD_SYM] >>
632 rw[big_gcd_reduction]
633QED
634
635(* Theorem: big_gcd {x; y} = gcd x y *)
636(* Proof:
637 big_gcd {x; y}
638 = big_gcd (x INSERT y) by notation
639 = gcd x (big_gcd {y}) by big_gcd_insert
640 = gcd x (big_gcd {y INSERT {}}) by notation
641 = gcd x (gcd y (big_gcd {})) by big_gcd_insert
642 = gcd x (gcd y 0) by big_gcd_empty
643 = gcd x y by gcd_0R
644*)
645Theorem big_gcd_two:
646 !x y. big_gcd {x; y} = gcd x y
647Proof
648 rw[big_gcd_insert, big_gcd_empty]
649QED
650
651(* Theorem: FINITE s ==> (!x. x IN s ==> 0 < x) ==> 0 < big_gcd s *)
652(* Proof:
653 By finite induction on s.
654 Base: {} <> {} /\ !x. x IN {} ==> 0 < x ==> 0 < big_gcd {}
655 True since {} <> {} = F
656 Step: s <> {} /\ (!x. x IN s ==> 0 < x) ==> 0 < big_gcd s ==>
657 e NOTIN s /\ e INSERT s <> {} /\ !x. x IN e INSERT s ==> 0 < x ==> 0 < big_gcd (e INSERT s)
658 Note 0 < e /\ !x. x IN s ==> 0 < x by IN_INSERT
659 If s = {},
660 big_gcd (e INSERT {})
661 = big_gcd {e} by IN_INSERT
662 = e > 0 by big_gcd_sing
663 If s <> {},
664 so 0 < big_gcd s by induction hypothesis
665 ==> 0 < gcd e (big_gcd s) by GCD_EQ_0
666 or 0 < big_gcd (e INSERT s) by big_gcd_insert
667*)
668Theorem big_gcd_positive:
669 !s. FINITE s /\ s <> {} /\ (!x. x IN s ==> 0 < x) ==> 0 < big_gcd s
670Proof
671 `!s. FINITE s ==> s <> {} /\ (!x. x IN s ==> 0 < x) ==> 0 < big_gcd s` suffices_by rw[] >>
672 Induct_on `FINITE` >>
673 rpt strip_tac >-
674 rw[] >>
675 `0 < e /\ (!x. x IN s ==> 0 < x)` by rw[] >>
676 Cases_on `s = {}` >-
677 rw[big_gcd_sing] >>
678 metis_tac[big_gcd_insert, GCD_EQ_0, NOT_ZERO_LT_ZERO]
679QED
680
681(* Theorem: FINITE s /\ s <> {} ==> !k. big_gcd (IMAGE ($* k) s) = k * big_gcd s *)
682(* Proof:
683 By finite induction on s.
684 Base: {} <> {} ==> ..., must be true.
685 Step: s <> {} ==> !!k. big_gcd (IMAGE ($* k) s) = k * big_gcd s ==>
686 e NOTIN s ==> big_gcd (IMAGE ($* k) (e INSERT s)) = k * big_gcd (e INSERT s)
687 If s = {},
688 big_gcd (IMAGE ($* k) (e INSERT {}))
689 = big_gcd (IMAGE ($* k) {e}) by IN_INSERT, s = {}
690 = big_gcd {k * e} by IMAGE_SING
691 = k * e by big_gcd_sing
692 = k * big_gcd {e} by big_gcd_sing
693 = k * big_gcd (e INSERT {}) by IN_INSERT, s = {}
694 If s <> {},
695 big_gcd (IMAGE ($* k) (e INSERT s))
696 = big_gcd ((k * e) INSERT (IMAGE ($* k) s)) by IMAGE_INSERT
697 = gcd (k * e) (big_gcd (IMAGE ($* k) s)) by big_gcd_insert
698 = gcd (k * e) (k * big_gcd s) by induction hypothesis
699 = k * gcd e (big_gcd s) by GCD_COMMON_FACTOR
700 = k * big_gcd (e INSERT s) by big_gcd_insert
701*)
702Theorem big_gcd_map_times:
703 !s. FINITE s /\ s <> {} ==> !k. big_gcd (IMAGE ($* k) s) = k * big_gcd s
704Proof
705 `!s. FINITE s ==> s <> {} ==> !k. big_gcd (IMAGE ($* k) s) = k * big_gcd s` suffices_by rw[] >>
706 Induct_on `FINITE` >>
707 rpt strip_tac >-
708 rw[] >>
709 Cases_on `s = {}` >-
710 rw[big_gcd_sing] >>
711 `big_gcd (IMAGE ($* k) (e INSERT s)) = gcd (k * e) (k * big_gcd s)` by rw[big_gcd_insert] >>
712 `_ = k * gcd e (big_gcd s)` by rw[GCD_COMMON_FACTOR] >>
713 `_ = k * big_gcd (e INSERT s)` by rw[big_gcd_insert] >>
714 rw[]
715QED
716
717(* ------------------------------------------------------------------------- *)
718(* Set LCM as Big Operator *)
719(* ------------------------------------------------------------------------- *)
720
721(* big_lcm s = ITSET (\e x. lcm e x) s 1 = ITSET lcm s 1, of course! *)
722Definition big_lcm_def:
723 big_lcm s = ITSET lcm s 1
724End
725
726(* Theorem: big_lcm {} = 1 *)
727(* Proof:
728 big_lcm {}
729 = ITSET lcm {} 1 by big_lcm_def
730 = 1 by ITSET_EMPTY
731*)
732Theorem big_lcm_empty:
733 big_lcm {} = 1
734Proof
735 rw[big_lcm_def, ITSET_EMPTY]
736QED
737
738(* Theorem: big_lcm {x} = x *)
739(* Proof:
740 big_lcm {x}
741 = ITSET lcm {x} 1 by big_lcm_def
742 = lcm x 1 by ITSET_SING
743 = x by LCM_1
744*)
745Theorem big_lcm_sing:
746 !x. big_lcm {x} = x
747Proof
748 rw[big_lcm_def, ITSET_SING]
749QED
750
751(* Theorem: FINITE s /\ x NOTIN s ==> (big_lcm (x INSERT s) = lcm x (big_lcm s)) *)
752(* Proof:
753 Note big_lcm s = ITSET lcm s 1 by big_lcm_def
754 Since !x y z. lcm x (lcm y z) = lcm y (lcm x z) by LCM_ASSOC_COMM
755 The result follows by ITSET_REDUCTION
756*)
757Theorem big_lcm_reduction:
758 !s x. FINITE s /\ x NOTIN s ==> (big_lcm (x INSERT s) = lcm x (big_lcm s))
759Proof
760 rw[big_lcm_def, ITSET_REDUCTION, LCM_ASSOC_COMM]
761QED
762
763(* Theorem: FINITE s ==> !x. x IN s ==> x divides (big_lcm s) *)
764(* Proof:
765 By finite induction on s.
766 Base: x IN {} ==> x divides big_lcm {}
767 True since x IN {} = F by MEMBER_NOT_EMPTY
768 Step: !x. x IN s ==> x divides big_lcm s ==>
769 e NOTIN s /\ x IN (e INSERT s) ==> x divides big_lcm (e INSERT s)
770 Since e NOTIN s,
771 so big_lcm (e INSERT s) = lcm e (big_lcm s) by big_lcm_reduction
772 By IN_INSERT,
773 If x = e,
774 to show: e divides lcm e (big_lcm s), true by LCM_DIVISORS
775 If x <> e, x IN s,
776 to show x divides lcm e (big_lcm s),
777 Since x divides (big_lcm s) by induction hypothesis, x IN s
778 and (big_lcm s) divides lcm e (big_lcm s) by LCM_DIVISORS
779 so x divides lcm e (big_lcm s) by DIVIDES_TRANS
780*)
781Theorem big_lcm_is_common_multiple:
782 !s. FINITE s ==> !x. x IN s ==> x divides (big_lcm s)
783Proof
784 Induct_on `FINITE` >>
785 rpt strip_tac >-
786 metis_tac[MEMBER_NOT_EMPTY] >>
787 metis_tac[big_lcm_reduction, IN_INSERT, LCM_DIVISORS, DIVIDES_TRANS]
788QED
789
790(* Theorem: FINITE s ==> !m. (!x. x IN s ==> x divides m) ==> (big_lcm s) divides m *)
791(* Proof:
792 By finite induction on s.
793 Base: big_lcm {} divides m
794 Since big_lcm {} = 1 by big_lcm_empty
795 Hence true by ONE_DIVIDES_ALL
796 Step: !m. (!x. x IN s ==> x divides m) ==> big_lcm s divides m ==>
797 e NOTIN s /\ !x. x IN e INSERT s ==> x divides m ==> big_lcm (e INSERT s) divides m
798 Note x IN e INSERT s ==> x = e \/ x IN s by IN_INSERT
799 Put x = e, then e divides m by x divides m, x = e
800 Put x IN s, then big_lcm s divides m by induction hypothesis
801 Therefore, lcm e (big_lcm s) divides m by LCM_IS_LEAST_COMMON_MULTIPLE
802 or big_lcm (e INSERT s) divides m by big_lcm_reduction, e NOTIN s
803*)
804Theorem big_lcm_is_least_common_multiple:
805 !s. FINITE s ==> !m. (!x. x IN s ==> x divides m) ==> (big_lcm s) divides m
806Proof
807 Induct_on `FINITE` >>
808 rpt strip_tac >-
809 rw[big_lcm_empty] >>
810 metis_tac[big_lcm_reduction, LCM_IS_LEAST_COMMON_MULTIPLE, IN_INSERT]
811QED
812
813(* Theorem: FINITE s ==> !x. big_lcm (x INSERT s) = lcm x (big_lcm s) *)
814(* Proof:
815 If x IN s,
816 Then x divides (big_lcm s) by big_lcm_is_common_multiple
817 lcm x (big_lcm s)
818 = big_lcm s by divides_iff_lcm_fix
819 = big_lcm (x INSERT s) by ABSORPTION
820 If x NOTIN s, result is true by big_lcm_reduction
821*)
822Theorem big_lcm_insert:
823 !s. FINITE s ==> !x. big_lcm (x INSERT s) = lcm x (big_lcm s)
824Proof
825 rpt strip_tac >>
826 Cases_on `x IN s` >-
827 metis_tac[big_lcm_is_common_multiple, divides_iff_lcm_fix, ABSORPTION] >>
828 rw[big_lcm_reduction]
829QED
830
831(* Theorem: big_lcm {x; y} = lcm x y *)
832(* Proof:
833 big_lcm {x; y}
834 = big_lcm (x INSERT y) by notation
835 = lcm x (big_lcm {y}) by big_lcm_insert
836 = lcm x (big_lcm {y INSERT {}}) by notation
837 = lcm x (lcm y (big_lcm {})) by big_lcm_insert
838 = lcm x (lcm y 1) by big_lcm_empty
839 = lcm x y by LCM_1
840*)
841Theorem big_lcm_two:
842 !x y. big_lcm {x; y} = lcm x y
843Proof
844 rw[big_lcm_insert, big_lcm_empty]
845QED
846
847(* Theorem: FINITE s ==> (!x. x IN s ==> 0 < x) ==> 0 < big_lcm s *)
848(* Proof:
849 By finite induction on s.
850 Base: !x. x IN {} ==> 0 < x ==> 0 < big_lcm {}
851 big_lcm {} = 1 > 0 by big_lcm_empty
852 Step: (!x. x IN s ==> 0 < x) ==> 0 < big_lcm s ==>
853 e NOTIN s /\ !x. x IN e INSERT s ==> 0 < x ==> 0 < big_lcm (e INSERT s)
854 Note 0 < e /\ !x. x IN s ==> 0 < x by IN_INSERT
855 so 0 < big_lcm s by induction hypothesis
856 ==> 0 < lcm e (big_lcm s) by LCM_EQ_0
857 or 0 < big_lcm (e INSERT s) by big_lcm_insert
858*)
859Theorem big_lcm_positive:
860 !s. FINITE s ==> (!x. x IN s ==> 0 < x) ==> 0 < big_lcm s
861Proof
862 Induct_on `FINITE` >>
863 rpt strip_tac >-
864 rw[big_lcm_empty] >>
865 `0 < e /\ (!x. x IN s ==> 0 < x)` by rw[] >>
866 metis_tac[big_lcm_insert, LCM_EQ_0, NOT_ZERO_LT_ZERO]
867QED
868
869(* Theorem: FINITE s /\ s <> {} ==> !k. big_lcm (IMAGE ($* k) s) = k * big_lcm s *)
870(* Proof:
871 By finite induction on s.
872 Base: {} <> {} ==> ..., must be true.
873 Step: s <> {} ==> !!k. big_lcm (IMAGE ($* k) s) = k * big_lcm s ==>
874 e NOTIN s ==> big_lcm (IMAGE ($* k) (e INSERT s)) = k * big_lcm (e INSERT s)
875 If s = {},
876 big_lcm (IMAGE ($* k) (e INSERT {}))
877 = big_lcm (IMAGE ($* k) {e}) by IN_INSERT, s = {}
878 = big_lcm {k * e} by IMAGE_SING
879 = k * e by big_lcm_sing
880 = k * big_lcm {e} by big_lcm_sing
881 = k * big_lcm (e INSERT {}) by IN_INSERT, s = {}
882 If s <> {},
883 big_lcm (IMAGE ($* k) (e INSERT s))
884 = big_lcm ((k * e) INSERT (IMAGE ($* k) s)) by IMAGE_INSERT
885 = lcm (k * e) (big_lcm (IMAGE ($* k) s)) by big_lcm_insert
886 = lcm (k * e) (k * big_lcm s) by induction hypothesis
887 = k * lcm e (big_lcm s) by LCM_COMMON_FACTOR
888 = k * big_lcm (e INSERT s) by big_lcm_insert
889*)
890Theorem big_lcm_map_times:
891 !s. FINITE s /\ s <> {} ==> !k. big_lcm (IMAGE ($* k) s) = k * big_lcm s
892Proof
893 `!s. FINITE s ==> s <> {} ==> !k. big_lcm (IMAGE ($* k) s) = k * big_lcm s` suffices_by rw[] >>
894 Induct_on `FINITE` >>
895 rpt strip_tac >-
896 rw[] >>
897 Cases_on `s = {}` >-
898 rw[big_lcm_sing] >>
899 `big_lcm (IMAGE ($* k) (e INSERT s)) = lcm (k * e) (k * big_lcm s)` by rw[big_lcm_insert] >>
900 `_ = k * lcm e (big_lcm s)` by rw[LCM_COMMON_FACTOR] >>
901 `_ = k * big_lcm (e INSERT s)` by rw[big_lcm_insert] >>
902 rw[]
903QED