1(* interactive mode
2app load ["bossLib","gcdTheory","powerTheory","summationTheory",
3          "binomialTheory","congruentTheory"];
4quietdec := true;
5*)
6
7open HolKernel Parse boolLib
8open bossLib numLib arithmeticTheory prim_recTheory
9     gcdTheory dividesTheory
10     binomialTheory congruentTheory summationTheory powerTheory ;
11
12(*
13quietdec := false;
14*)
15
16infix THEN THENC THENL;
17infix 8 by;
18val ARW = RW_TAC arith_ss;
19
20val _ = new_theory "fermat";
21
22val FACT_def = ONCE_REWRITE_RULE [MULT_COMM] FACT;
23
24val DIV_FACT = store_thm("DIV_FACT",
25                        Term `!p n. prime p /\ 0 <n /\ divides p (FACT n)
26                                ==> ?k. 0<k /\ k <= n /\ divides p k`,
27                        Induct_on `n` THEN ARW[FACT_def]
28                        THEN Cases_on `divides p (SUC n)` THENL[
29                          EXISTS_TAC (Term `SUC n`) THEN ARW[],
30                          IMP_RES_TAC P_EUCLIDES THEN TRY (PROVE_TAC[])
31                            THEN sg `0 < n`
32                            THENL [
33                              Cases_on `n=0` THEN ARW[]
34                                THEN `~(divides p (FACT 0))`
35                                 by (REWRITE_TAC[FACT_def, ONE]
36                                       THEN PROVE_TAC[]),
37                              RES_TAC THEN EXISTS_TAC (Term `k:num`) THEN ARW[]
38                            ]
39                        ]
40                        );
41
42val DIV_FACT_LESS = store_thm("DIV_FACT_LESS",
43                              Term `!p n. prime p /\ divides p (FACT n) ==> p <= n`,
44                              Cases_on `n` THENL[
45                                ARW[FACT_def]
46                                  THEN `p <= 1` by ARW[DIVIDES_LE]
47                                  THEN Cases_on `p=1`
48                                  THEN ARW[NOT_PRIME_1] THEN PROVE_TAC[NOT_PRIME_1],
49                                ARW[] THEN `0 < SUC n'` by ARW[]
50                                  THEN PROVE_TAC[DIV_FACT,DIVIDES_LE,LESS_EQ_TRANS]
51                              ]
52                              );
53
54
55val P_DIV_BINOMIAL = store_thm("P_DIV_BINOMIAL",
56                        Term `!p n. prime p /\ 0<n /\ n<p ==>  divides p (binomial p n)`,
57                        ARW[]
58                        THEN `0<p` by (Cases_on `p=0` THEN ARW[] THEN PROVE_TAC[NOT_PRIME_0])
59                        THEN `divides p ((binomial ((p-n)+n) n) * (FACT (p-n) * FACT n))` by ARW[BINOMIAL_FACT,DIVIDES_FACT]
60                        THEN  Cases_on `divides p (FACT (p-n) * FACT n)`
61                        THENL [
62                          Cases_on `divides p (FACT n)` THENL [
63                            `p <= n` by PROVE_TAC[DIV_FACT_LESS] THEN PROVE_TAC[NOT_LESS],
64                            Cases_on `divides p (FACT (p-n))` THENL [
65                              `p <= p-n` by PROVE_TAC[DIV_FACT_LESS]
66                                 THEN PROVE_TAC[SUB_LESS_EQ,NOT_LESS_EQ,SUB_EQ_EQ_0,LESS_EQUAL_ANTISYM]
67                               ,
68                               IMP_RES_TAC P_EUCLIDES THEN PROVE_TAC[]
69                            ]
70                          ]
71                          ,
72                          IMP_RES_TAC P_EUCLIDES THEN TRY (PROVE_TAC[])
73                            THEN (POP_ASSUM MP_TAC) THEN ARW[SUB_ADD]
74                        ]
75                      );
76
77val FERMAT_1 = store_thm
78  ("FERMAT_1",
79   Term
80   `!p k.
81      prime p ==>
82      congruent ((k + 1) EXP p) (k EXP p + 1) p`,
83   Cases_on `p` THEN REWRITE_TAC[NOT_PRIME_0]
84   THEN REWRITE_TAC[NOT_PRIME_1, SYM ONE]
85   THEN ARW[EXP_PASCAL, GSYM ADD1]
86   THEN ONCE_REWRITE_TAC[SUMMATION_1]
87   THEN ONCE_REWRITE_TAC [SUMMATION_2]
88   THEN ARW[BINOMIAL_DEF1,MULT_CLAUSES,POWER_1,ADD_CLAUSES]
89   THEN ARW[BINOMIAL_DEF3,power_def, ADD1]
90   THEN MATCH_MP_TAC CONGRUENT_ADD
91   THEN ARW[CONGRUENT_REF]
92   THEN `1=0+1` by ARW[]
93   THEN POP_ASSUM (fn th => ONCE_REWRITE_TAC[th])
94   THEN MATCH_MP_TAC CONGRUENT_ADD
95   THEN ARW[CONGRUENT_REF]
96   THEN MATCH_MP_TAC
97     (BETA_RULE
98      (Q.SPECL
99       [`n`, `1`,
100        `\k'. k EXP (n + 1 - k') * binomial (n + 1) k'`,
101        `\a. congruent a 0 (n + 1)`] INV_SUMMATION))
102     THEN ARW[ADD_CLAUSES, CONGRUENT_REF] THENL
103     [PROVE_TAC[CONGRUENT_ADD,ADD_CLAUSES],
104      `divides (SUC n) (binomial (n + 1) (k' + 1))`
105      by ARW[GSYM ADD1, P_DIV_BINOMIAL]
106      THEN PROVE_TAC[CONGRUENT_MULT_0,DIVIDES_CONGRUENT,ADD1,MULT_COMM]
107      ]
108     );
109
110
111val FERMAT_2 = store_thm("FERMAT_2",
112                             Term `!k p. prime p ==> congruent ($EXP k p) k p`,
113                             Induct_on `k` THEN Cases_on `p` THEN ARW[POWER_0,NOT_PRIME_0,CONGRUENT_REF]
114                             THEN `congruent ($EXP (k+1) (SUC n)) (($EXP k (SUC n))+1) (SUC n)` by PROVE_TAC[FERMAT_1]
115                             THEN `SUC k = k+1` by ARW[]
116                             THEN `congruent (($EXP k (SUC n))+1) (k+1) (SUC n)` by PROVE_TAC[CONGRUENT_REF,CONGRUENT_ADD]
117                             THEN PROVE_TAC[CONGRUENT_REF,CONGRUENT_ADD,CONGRUENT_TRANS]);
118
119
120val FERMAT = store_thm("FERMAT",
121                        Term `!k p. prime p ==> congruent ($EXP k (p-1)) 1 p \/ divides p k`,
122                        Cases_on `k` THEN Cases_on `p` THEN ARW[power_def,CONGRUENT_REF,ALL_DIVIDES_0]
123                        THEN Cases_on `divides (SUC n') (SUC n)` THEN ARW[]
124                        THEN `SUC n <= $EXP (SUC n) (SUC n')` by ARW[POWER_LE]
125                        THEN `divides (SUC n) (($EXP (SUC n) (SUC n')) - (SUC n))`
126                           by ARW[DIVIDES_SUB,DIVIDES_REFL,power_def,DIVIDES_MULT,MULT_SYM]
127                        THEN POP_ASSUM MP_TAC THEN ARW[divides_def]
128                        THEN `divides (SUC n') (q * SUC n)` by PROVE_TAC[CONGRUENT_DIVIDES,FERMAT_2]
129                        THEN `gcd (SUC n) (SUC n') = 1` by PROVE_TAC[PRIME_GCD,GCD_SYM]
130                        THEN `divides (SUC n') q` by PROVE_TAC[L_EUCLIDES,MULT_SYM]
131                        THEN POP_ASSUM MP_TAC THEN ARW[divides_def,congruent_def]
132                        THEN EXISTS_TAC (Term `0`) THEN EXISTS_TAC (Term `q':num`) THEN ARW[MULT_CLAUSES]
133                        THEN `(($EXP (SUC n) n' -1)*(SUC n)) = (q' * SUC n') * (SUC n)`
134                           by (REWRITE_TAC[RIGHT_SUB_DISTRIB] THEN PROVE_TAC[power_def,MULT_SYM,MULT_LEFT_1])
135                        THEN `($EXP (SUC n) n' -1) = q' + q'* n'` by PROVE_TAC[ MULT_SUC_EQ,MULT_SYM,MULT_CLAUSES]
136                        THEN `1 <= $EXP (SUC n) n'` by PROVE_TAC[POWER_LE_1]
137                        THEN ARW[SUB_ADD]
138                        );
139
140val _ = export_theory();
141