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