1% ===================================================================== % 2% 14 June 1989 - modified for HOL88 % 3% % 4% The following bits are needed to make this proof run in HOL88. % 5 6set_flag (`sticky`,true);; 7let MOD = 8 SPEC_ALL 9 (PURE_REWRITE_RULE [ 10 SPECL ["m+n";"p:num"] (INST_TYPE [":num",":*"] EQ_SYM_EQ)] MOD);; 11 12% ===================================================================== % 13% PROOF : Modulus Function for Natural Numbers % 14% FILE : mod.ml % 15% % 16% DESCRIPTION : Defines MOD function for natural numbers and proves % 17% some useful theorems about this function, including % 18% the following theorem: % 19% % 20% !m n. n < m ==> !k. (((k * m) + n) MOD m) = n % 21% % 22% These theorems depend on the division algorithm % 23% theorem for natural numbers proven by T.Melham. % 24% % 25% AUTHOR : J.Joyce % 26% DATE : 16 July 1987 % 27% ===================================================================== % 28 29new_theory `mod`;; 30 31new_parent `da`;; 32new_parent `arith`;; 33 34% ===================================================================== % 35% 89-June-14: MOD already defined in HOL88 % 36% let MOD = new_infix_definition ( % 37% `MOD`, % 38% "$MOD n m = @r. ?q. (n = (q * m) + r) /\ (r < m)");; % 39 40let DA = theorem `da` `DA`;; 41 42let ADD_SUB = theorem `arith` `ADD_SUB`;; 43let LESS_LESS_0 = theorem `arith` `LESS_LESS_0`;; 44let ADD_SUB_ASSOC = theorem `arith` `ADD_SUB_ASSOC`;; 45let ADD_LESS_OR_EQ = theorem `arith` `ADD_LESS_OR_EQ`;; 46let UNIQUE_REMAINDER_THM = theorem `arith` `UNIQUE_REMAINDER_THM`;; 47 48let EXISTS_MOD = prove_thm ( 49 `EXISTS_MOD`, 50 "!m. 0 < m ==> !n. ?q. (n = (q * m) + (n MOD m)) /\ (n MOD m) < m", 51 REPEAT STRIP_TAC THEN 52 HOL_IMP_RES_THEN (ASSUME_TAC o NOT_EQ_SYM) LESS_NOT_EQ THEN 53 REWRITE_TAC [MOD;SELECT_RULE (UNDISCH_ALL (SPECL ["n";"m"] DA))]);; 54 55let MOD_THM = prove_thm ( 56 `MOD_THM`, 57 "!m n. n < m ==> !k. ((((k * m) + n) MOD m) = n)", 58 REPEAT STRIP_TAC THEN 59 IMP_RES_TAC LESS_LESS_0 THEN 60 HOL_IMP_RES_THEN 61 (STRIP_ASSUME_TAC o (SPEC "(k * m) + n")) EXISTS_MOD THEN 62 IMP_RES_THEN 63 (\thm. (ACCEPT_TAC (SYM thm)) ? ALL_TAC) UNIQUE_REMAINDER_THM);; 64 65let MOD_ONE_THM = prove_thm ( 66 `MOD_ONE_THM`, 67 "!m. m MOD 1 = 0", 68 GEN_TAC THEN 69 SUBST1_TAC (SYM (CONJUNCT1 (CONJUNCT2 70 (CONJUNCT2 (CONJUNCT2 (SPEC_ALL MULT_CLAUSES)))))) THEN 71 SUBST1_TAC (SYM (CONJUNCT1 72 (CONJUNCT2 (SPEC "m * 1" (GEN "m" ADD_CLAUSES))))) THEN 73 REWRITE_TAC 74 [REWRITE_RULE [LESS_0] 75 (SUBS_OCCS [[1],num_CONV "1"] (SPECL ["1";"0"] MOD_THM))]);; 76 77let LESS_MOD_THM = prove_thm ( 78 `LESS_MOD_THM`, 79 "!m n. n < m ==> ((n MOD m) = n)", 80 REPEAT STRIP_TAC THEN 81 HOL_IMP_RES_THEN 82 (ACCEPT_TAC o 83 (REWRITE_RULE [MULT_CLAUSES;ADD_CLAUSES]) o (SPEC "0")) MOD_THM);; 84 85let MOD_LESS_THM = prove_thm ( 86 `MOD_LESS_THM`, 87 "!m. 0 < m ==> !n. (n MOD m) < m", 88 REPEAT STRIP_TAC THEN 89 HOL_IMP_RES_THEN (STRIP_ASSUME_TAC o (SPEC "n")) EXISTS_MOD);; 90 91let MOD_LESS_EQ = prove_thm ( 92 `MOD_LESS_EQ`, 93 "!m. 0 < m ==> !n. (n MOD m) <= n", 94 REPEAT STRIP_TAC THEN 95 IMP_RES_THEN 96 ((X_CHOOSE_THEN "q" 97 (\thm. SUBST_OCCS_TAC [[2],CONJUNCT1 thm])) o (SPEC "n")) 98 EXISTS_MOD THEN 99 SUBST1_TAC (SPECL ["q * m";"n MOD m"] ADD_SYM) THEN 100 REWRITE_TAC [LESS_EQ_ADD]);; 101 102let MULT_MOD_0 = prove_thm ( 103 `MULT_MOD_0`, 104 "!m. 0 < m ==> !n. ((n * m) MOD m) = 0", 105 REPEAT STRIP_TAC THEN 106 SUBST1_TAC 107 (SYM 108 (SPEC "n * m" (GEN "m" (CONJUNCT1 (CONJUNCT2 ADD_CLAUSES))))) THEN 109 IMP_RES_THEN (\thm. REWRITE_TAC [thm]) MOD_THM);; 110 111let MOD_MOD_THM = prove_thm ( 112 `MOD_MOD_THM`, 113 "!m. 0 < m ==> !n. ((n MOD m) MOD m) = (n MOD m)", 114 REPEAT STRIP_TAC THEN 115 HOL_IMP_RES_THEN (ASSUME_TAC o (SPEC "n")) MOD_LESS_THM THEN 116 HOL_IMP_RES_THEN (ASSUME_TAC o (SPEC "0")) MOD_THM THEN 117 FIRST_ASSUM 118 (ACCEPT_TAC o (REWRITE_RULE [MULT_CLAUSES;ADD_CLAUSES])));; 119 120let MOD_CONGRUENCE_THM = prove_thm ( 121 `MOD_CONGRUENCE_THM`, 122 "!m. 0 < m ==> !n k. ((k * m) + n) MOD m = n MOD m", 123 REPEAT STRIP_TAC THEN 124 HOL_IMP_RES_THEN 125 ((X_CHOOSE_THEN "q:num" 126 (\thm. SUBST_OCCS_TAC [[1],CONJUNCT1 thm])) o (SPEC "n")) 127 EXISTS_MOD THEN 128 REWRITE_TAC 129 [ADD_ASSOC;GEN_ALL (SYM (SPEC_ALL RIGHT_ADD_DISTRIB))] THEN 130 HOL_IMP_RES_THEN 131 (\thm. 132 REWRITE_TAC [MATCH_MP MOD_THM (SPEC "n" thm)]) MOD_LESS_THM);; 133 134let MOD_ADD_THM = prove_thm ( 135 `MOD_ADD_THM`, 136 "!m. 0 < m ==> 137 !n p. (((n MOD m) + (p MOD m)) MOD m) = ((n + p) MOD m)", 138 REPEAT STRIP_TAC THEN 139 HOL_IMP_RES_THEN 140 ((X_CHOOSE_THEN "qn:num" 141 (\thm. SUBST_OCCS_TAC [[2],CONJUNCT1 thm])) o (SPEC "n")) 142 EXISTS_MOD THEN 143 HOL_IMP_RES_THEN 144 ((X_CHOOSE_THEN "qp:num" 145 (\thm. SUBST_OCCS_TAC [[2],CONJUNCT1 thm])) o (SPEC "p")) 146 EXISTS_MOD THEN 147 PURE_REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL ADD_ASSOC))] THEN 148 IMP_RES_THEN (\thm. PURE_REWRITE_TAC [thm]) MOD_CONGRUENCE_THM THEN 149 PURE_REWRITE_TAC [ADD_ASSOC] THEN 150 SUBST1_TAC (SPECL ["n MOD m";"qp * m"] ADD_SYM) THEN 151 PURE_REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL ADD_ASSOC))] THEN 152 IMP_RES_THEN (\thm. REWRITE_TAC [thm]) MOD_CONGRUENCE_THM);; 153 154let MOD_SUB_THM = prove_thm ( 155 `MOD_SUB_THM`, 156 "!m n p. (0 < m /\ p <= n MOD m) ==> 157 ((((n MOD m) - p) MOD m) = ((n - p) MOD m))", 158 REPEAT STRIP_TAC THEN 159 IMP_RES_TAC LESS_LESS_0 THEN 160 HOL_IMP_RES_THEN 161 ((X_CHOOSE_THEN "qn:num" 162 (\thm. SUBST_OCCS_TAC [[2],CONJUNCT1 thm])) o (SPEC "n")) 163 EXISTS_MOD THEN 164 HOL_IMP_RES_THEN (\thm. PURE_REWRITE_TAC [thm]) ADD_SUB_ASSOC THEN 165 IMP_RES_THEN (\thm. REWRITE_TAC [thm]) MOD_CONGRUENCE_THM);; 166 167% ===================================================================== % 168% MOD_SUB_THM is a special case of a more general theorem relating % 169% subtraction and modulus but its proof depends on several unproven % 170% subtraction theorems (which aren't too hard but I don't have time % 171% to prove them now). Here is the general theorem and a tactic for % 172% proving it but the required subtraction theorems are just assumed. % 173% ===================================================================== % 174 175let SUB_lemma1 = ASSUME "!m n p. (m-(n+p)) = ((m-n)-p)";; 176let SUB_lemma2 = ASSUME "!m n. m <= n ==> !p. ((n+p)-m) = ((n-m)+p)";; 177let SUB_lemma3 = ASSUME "!m n p. ((m*n)-(p*n)) = ((m-p)*n)";; 178 179TAC_PROOF (( 180 (hyp (LIST_CONJ [SUB_lemma1;SUB_lemma2;SUB_lemma3])), 181 "!m. 0 < m ==> 182 !n p. 183 ((p MOD m) <= (n MOD m)) /\ 184 ((p - (p MOD m)) <= (n - (n MOD m))) ==> 185 ((((n MOD m) - (p MOD m)) MOD m) = ((n - p) MOD m))"), 186 GEN_TAC THEN 187 STRIP_TAC THEN 188 REPEAT GEN_TAC THEN 189 HOL_IMP_RES_THEN 190 ((X_CHOOSE_THEN "qn:num" 191 (\thm. SUBST_OCCS_TAC [[2;5],CONJUNCT1 thm])) o (SPEC "n")) 192 EXISTS_MOD THEN 193 HOL_IMP_RES_THEN 194 ((X_CHOOSE_THEN "qp:num" 195 (\thm. SUBST_OCCS_TAC [[2;5],CONJUNCT1 thm])) o (SPEC "p")) 196 EXISTS_MOD THEN 197 PURE_REWRITE_TAC [ADD_SUB] THEN 198 STRIP_TAC THEN 199 PURE_REWRITE_TAC [SUB_lemma1] THEN 200 HOL_IMP_RES_THEN (\thm. PURE_REWRITE_TAC [thm]) SUB_lemma2 THEN 201 PURE_REWRITE_TAC [SUB_lemma3] THEN 202 HOL_IMP_RES_THEN (\thm. PURE_REWRITE_TAC [thm]) ADD_SUB_ASSOC THEN 203 IMP_RES_THEN (\thm. REWRITE_TAC [thm]) MOD_CONGRUENCE_THM);; 204 205close_theory ();; 206