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