1open HolKernel Parse boolLib BasicProvers 2 3open dividesTheory pred_setTheory 4open gcdTheory simpLib metisLib 5 6val ARITH_ss = numSimps.ARITH_ss 7 8val _ = new_theory "gcdset" 9 10val gcdset_def = new_definition( 11 "gcdset_def", 12 ``gcdset s = 13 if (s = {}) \/ (s = {0}) then 0 14 else MAX_SET ({ n | n <= MIN_SET (s DELETE 0) } INTER 15 { d | !e. e IN s ==> divides d e })``); 16 17val FINITE_LEQ_MIN_SET = prove( 18 ``FINITE { n | n <= MIN_SET (s DELETE 0) }``, 19 Q_TAC SUFF_TAC ` 20 { n | n <= MIN_SET (s DELETE 0) } = count (MIN_SET (s DELETE 0) + 1) 21 ` THEN1 SRW_TAC [][] THEN 22 SRW_TAC [ARITH_ss][EXTENSION]); 23 24val NON_EMPTY_INTERSECTION = prove( 25 ``s <> {} /\ s <> {0} ==> 26 { n | n <= MIN_SET (s DELETE 0) } INTER 27 { d | !e. e IN s ==> divides d e} <> {}``, 28 STRIP_TAC THEN SIMP_TAC (srw_ss()) [EXTENSION] THEN Q.EXISTS_TAC `1` THEN 29 SRW_TAC [][] THEN DEEP_INTRO_TAC MIN_SET_ELIM THEN 30 SRW_TAC [ARITH_ss][EXTENSION] THEN 31 FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN METIS_TAC []); 32 33val gcdset_divides = store_thm( 34 "gcdset_divides", 35 ``!e. e IN s ==> divides (gcdset s) e``, 36 SRW_TAC[][gcdset_def] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 37 DEEP_INTRO_TAC MAX_SET_ELIM THEN 38 ASM_SIMP_TAC (srw_ss()) [FINITE_INTER, FINITE_LEQ_MIN_SET, 39 NON_EMPTY_INTERSECTION]); 40 41val DECIDE = numLib.ARITH_PROVE 42val gcdset_greatest = store_thm( 43 "gcdset_greatest", 44 ``(!e. e IN s ==> divides g e) ==> divides g (gcdset s)``, 45 SRW_TAC [][gcdset_def] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 46 DEEP_INTRO_TAC MAX_SET_ELIM THEN 47 ASM_SIMP_TAC (srw_ss()) [NON_EMPTY_INTERSECTION, FINITE_LEQ_MIN_SET] THEN 48 Q.X_GEN_TAC `m` THEN REPEAT STRIP_TAC THEN 49 Q.ABBREV_TAC `L = lcm g m` THEN 50 `(!e. e IN s ==> divides L e) /\ divides m L /\ divides g L` 51 by METIS_TAC [gcdTheory.LCM_IS_LEAST_COMMON_MULTIPLE] THEN 52 `?x. x IN s /\ x <> 0` 53 by (FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN METIS_TAC []) THEN 54 `L <= MIN_SET (s DELETE 0)` 55 by (DEEP_INTRO_TAC MIN_SET_ELIM THEN SRW_TAC [][EXTENSION] 56 THEN1 METIS_TAC [] THEN 57 METIS_TAC [DIVIDES_LE, DECIDE ``x <> 0 <=> 0 < x``]) THEN 58 `L <= m` by METIS_TAC[] THEN 59 Q_TAC SUFF_TAC `0 < m /\ 0 < g` THEN1 60 METIS_TAC [LCM_LE, DECIDE ``x <= y /\ y <= x ==> (x = y)``] THEN 61 METIS_TAC [ZERO_DIVIDES, DECIDE ``x <> 0 <=> 0 < x``]); 62 63val gcdset_EMPTY = store_thm( 64 "gcdset_EMPTY", 65 ``gcdset {} = 0``, 66 SRW_TAC [][gcdset_def]); 67val _ = export_rewrites ["gcdset_EMPTY"] 68 69val gcdset_INSERT = store_thm( 70 "gcdset_INSERT", 71 ``gcdset (x INSERT s) = gcd x (gcdset s)``, 72 Q.MATCH_ABBREV_TAC `G1 = G2` THEN 73 `(!e. e IN s ==> divides G1 e) /\ divides G1 x` 74 by METIS_TAC [IN_INSERT, gcdset_divides] THEN 75 `divides G2 x /\ divides G2 (gcdset s)` 76 by METIS_TAC [GCD_IS_GCD, is_gcd_def] THEN 77 MATCH_MP_TAC DIVIDES_ANTISYM THEN CONJ_TAC THENL [ 78 Q_TAC SUFF_TAC `divides G1 (gcdset s)` THEN1 79 METIS_TAC [GCD_IS_GCD, is_gcd_def] THEN 80 SRW_TAC [][gcdset_greatest], 81 Q_TAC SUFF_TAC `!e. e IN s ==> divides G2 e` THEN1 82 METIS_TAC [IN_INSERT, gcdset_greatest] THEN 83 METIS_TAC [gcdset_divides, DIVIDES_TRANS] 84 ]); 85val _ = export_rewrites ["gcdset_INSERT"] 86 87 88val _ = export_theory() 89