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);; 7 8% ===================================================================== % 9% PROOF : More Theorems of Arithmetic % 10% FILE : arith.ml % 11% % 12% DESCRIPTION : Proves some general theorems of arithmetic which % 13% are not currently built into the system. % 14% % 15% AUTHOR : J.Joyce % 16% DATE : 16 July 1987 % 17% ===================================================================== % 18 19new_theory `arith`;; 20 21let LESS_LESS_0 = prove_thm ( 22 `LESS_LESS_0`, 23 "!m n. m < n ==> 0 < n", 24 REPEAT STRIP_TAC THEN 25 DISJ_CASES_TAC (SPEC "n" LESS_0_CASES) THENL 26 [ASSUME_TAC (SUBS [SYM (ASSUME "0 = n")] (ASSUME "m < n")) THEN 27 IMP_RES_TAC NOT_LESS_0; 28 FIRST_ASSUM ACCEPT_TAC]);; 29 30let LESS_EQ_LESS_TRANS = prove_thm ( 31 `LESS_EQ_LESS_TRANS`, 32 "!m n p. m <= n /\ n < p ==> m < p", 33 PURE_REWRITE_TAC [LESS_OR_EQ] THEN 34 REPEAT STRIP_TAC THEN 35 ASM_REWRITE_TAC [] THEN 36 IMP_RES_TAC LESS_TRANS);; 37 38let LESS_ADD_LESS = prove_thm ( 39 `LESS_ADD_LESS`, 40 "!m n. m < n ==> !p. m < p + n", 41 REPEAT GEN_TAC THEN 42 DISCH_TAC THEN 43 INDUCT_TAC THEN 44 ASM_REWRITE_TAC [ADD_CLAUSES] THEN 45 IMP_RES_TAC LESS_SUC);; 46 47let ADD_LESS_OR_EQ = prove_thm ( 48 `ADD_LESS_OR_EQ`, 49 "!m n. (?p. p + n = m) = (n <= m)", 50 REPEAT STRIP_TAC THEN EQ_TAC THENL 51 [DISCH_THEN (STRIP_THM_THEN (SUBST1_TAC o SYM)) THEN 52 SUBST1_TAC (SPECL ["p";"n"] ADD_SYM) THEN 53 REWRITE_TAC [LESS_EQ_ADD]; 54 DISCH_THEN (DISJ_CASES_TAC o (PURE_REWRITE_RULE [LESS_OR_EQ])) THENL 55 [IMP_RES_TAC LESS_ADD; 56 EXISTS_TAC "0" THEN ASM_REWRITE_TAC [ADD_CLAUSES]]]);; 57 58let LESS_ADD_SUC = prove_thm ( 59 `LESS_ADD_SUC`, 60 "!m n. n < m ==> ?p. p + (SUC n) = m", 61 INDUCT_TAC THENL 62 [REWRITE_TAC [NOT_LESS_0]; 63 PURE_REWRITE_TAC [LESS_THM] THEN 64 REPEAT STRIP_TAC THENL 65 [EXISTS_TAC "0" THEN 66 ASM_REWRITE_TAC [ADD_CLAUSES]; 67 RES_THEN (X_CHOOSE_THEN "p" (ASSUME_TAC o SYM)) THEN 68 EXISTS_TAC "SUC p" THEN 69 ASM_REWRITE_TAC [ADD_CLAUSES]]]);; 70 71let GREATER_0_num_CASES = prove_thm ( 72 `GREATER_0_num_CASES`, 73 "!m. 0 < m ==> ?n. m = SUC n", 74 GEN_TAC THEN 75 DISJ_CASES_TAC (SPEC "m" num_CASES) THEN 76 ASM_REWRITE_TAC [NOT_LESS_0]);; 77 78let SUB_ID = prove_thm ( 79 `SUB_ID`, 80 "!m. m - m = 0", 81 GEN_TAC THEN 82 ASSUME_TAC (SPEC "m" LESS_EQ_REFL) THEN 83 IMP_RES_TAC (snd (EQ_IMP_RULE (SPECL ["m";"m"] SUB_EQ_0))));; 84 85let ADD_SUB = prove_thm ( 86 `ADD_SUB`, 87 "!m n. ((m+n)-n) = m", 88 let th1 = 89 GEN_ALL (DISCH_ALL (GEN "m" (SYM 90 (SUBS [SPECL ["m";"p - n"] (INST_TYPE [":num",":*"] EQ_SYM_EQ)] 91 (UNDISCH (SPEC_ALL ADD_EQ_SUB)))))) in 92 let th2 = 93 SUBS [SPECL ["n";"p"] ADD_SYM] (SPECL ["n";"p"] LESS_EQ_ADD) in 94 GEN_TAC THEN 95 INDUCT_TAC THENL 96 [REWRITE_TAC [ADD_CLAUSES;SUB_ID;SUB_0]; 97 REPEAT STRIP_TAC THEN REWRITE_TAC [GEN_ALL (MATCH_MP th1 th2)]]);; 98 99let th1 = TAC_PROOF ( 100 ([],"!m n. m < SUC n ==> m <= n"), 101 PURE_REWRITE_TAC [LESS_THM] THEN 102 REPEAT STRIP_TAC THEN 103 ASM_REWRITE_TAC [LESS_OR_EQ]);; 104 105let th2 = TAC_PROOF ( 106 ([],"!m n. m <= n ==> ~(n < m)"), 107 REWRITE_TAC [NOT_LESS]);; 108 109let ADD_SUB_ASSOC = prove_thm ( 110 `ADD_SUB_ASSOC`, 111 "!m n. m <= n ==> !p. ((p+n)-m) = (p+(n-m))", 112 GEN_TAC THEN 113 INDUCT_TAC THEN 114 REWRITE_TAC [LESS_OR_EQ;NOT_LESS_0] THEN 115 REPEAT STRIP_TAC THENL 116 [ASM_REWRITE_TAC [ADD_CLAUSES;SUB_0]; 117 IMP_RES_TAC th1 THEN 118 RES_TAC THEN 119 IMP_RES_TAC th2 THEN 120 ASM_REWRITE_TAC [SUB] THEN 121 PURE_REWRITE_TAC [ADD_CLAUSES] THEN 122 ASM_REWRITE_TAC 123 [SYM (CONJUNCT1 (CONJUNCT2 (CONJUNCT2 ADD_CLAUSES)))]; 124 ASM_REWRITE_TAC [SUB_ID] THEN 125 REWRITE_TAC [ADD_CLAUSES;ADD_SUB]]);; 126 127let LESS_MULT_LESS = prove_thm ( 128 `LESS_MULT_LESS`, 129 "!m. 0 < m ==> !n p. n < p ==> n < m * p", 130 GEN_TAC THEN DISCH_TAC THEN GEN_TAC THEN 131 INDUCT_TAC THEN 132 REWRITE_TAC [NOT_LESS_0;LESS_THM] THEN 133 DISCH_THEN 134 (DISJ_CASES_THENL [SUBST1_TAC;ANTE_RES_THEN ASSUME_TAC]) THENL 135 [HOL_IMP_RES_THEN (CHOOSE_THEN SUBST1_TAC) GREATER_0_num_CASES THEN 136 REWRITE_TAC [MULT_CLAUSES;CONJUNCT2 ADD] THEN 137 REWRITE_TAC [MATCH_MP LESS_ADD_LESS (SPEC "p" LESS_SUC_REFL)]; 138 REWRITE_TAC [MULT_CLAUSES;ADD_CLAUSES] THEN 139 REWRITE_TAC [MATCH_MP LESS_ADD_LESS (ASSUME "n < (m * p)")]]);; 140 141let LESS_ADD_MONO = prove_thm ( 142 `LESS_ADD_MONO`, 143 "!m n. m < n ==> !p. m < n + p", 144 REPEAT GEN_TAC THEN STRIP_TAC THEN 145 INDUCT_TAC THEN 146 ASM_REWRITE_TAC [ADD_CLAUSES] THEN 147 IMP_RES_TAC LESS_SUC);; 148 149% adapted from M.Gordon's proof of LESS_EQ_LESS_EQ_MONO % 150let LESS_LESS_MONO = prove_thm ( 151 `LESS_LESS_MONO`, 152 "!m n p q. (m < p) /\ (n < q) ==> ((m + n) < (p + q))", 153 let th1 = SPECL ["m";"p";"n"] LESS_MONO_ADD_EQ in 154 let th2 = SPECL ["n";"q";"p"] LESS_MONO_ADD_EQ in 155 let sublist = [SPECL ["n";"p"] ADD_SYM;SPECL ["q";"p"] ADD_SYM] in 156 REPEAT STRIP_TAC THEN 157 IMP_RES_TAC (snd (EQ_IMP_RULE th1)) THEN 158 IMP_RES_TAC (SUBS sublist (snd (EQ_IMP_RULE th2))) THEN 159 IMP_RES_TAC (SPECL ["m+n";"p+n";"p+q"] LESS_TRANS) THEN 160 ASM_REWRITE_TAC []);; 161 162let LESS_EQ_MONO_MULT = save_thm (`LESS_EQ_MONO_MULT`,LESS_MONO_MULT);; 163 164let LESS_MONO_MULT = prove_thm ( 165 `LESS_MONO_MULT`, 166 "!n m. m < n ==> !p. 0 < p ==> (p * m) < (p * n)", 167 REPEAT STRIP_TAC THEN 168 IMP_RES_THEN (X_CHOOSE_THEN "q" SUBST1_TAC) GREATER_0_num_CASES THEN 169 PURE_REWRITE_TAC [MULT_CLAUSES] THEN 170 SPEC_TAC ("q","q") THEN 171 INDUCT_TAC THEN 172 ASM_REWRITE_TAC [MULT_CLAUSES;ADD_CLAUSES] THEN 173 IMP_RES_TAC 174 (SPECL ["(q * m) + m";"m";"(q * n) + n";"n"] LESS_LESS_MONO));; 175 176let th1 = TAC_PROOF ( 177 ([],"!m n. m < n ==> ~(n < m)"), 178 let thm = GEN_ALL (SYM (CONJUNCT1 (SPEC_ALL DE_MORGAN_THM))) in 179 REWRITE_TAC [IMP_DISJ_THM;thm;LESS_ANTISYM]);; 180 181let LESS_MONO_MULT_EQ = prove_thm ( 182 `LESS_MONO_MULT_EQ`, 183 "!m. 0 < m ==> !n p. ((n * m) < (p * m)) = (n < p)", 184 REPEAT STRIP_TAC THEN 185 SUBST1_TAC (SPECL ["n";"m"] MULT_SYM) THEN 186 SUBST1_TAC (SPECL ["p";"m"] MULT_SYM) THEN 187 MP_TAC (REWRITE_RULE [LESS_OR_EQ] (SPECL ["n";"p"] LESS_CASES)) THEN 188 STRIP_TAC THEN 189 IMP_RES_TAC LESS_MONO_MULT THEN 190 IMP_RES_TAC th1 THEN 191 ASM_REWRITE_TAC [LESS_REFL]);; 192 193let UNIQUE_QUOTIENT_THM = prove_thm ( 194 `UNIQUE_QUOTIENT_THM`, 195 "!m n p. (m < n) /\ (p < n) ==> 196 !q s. (((q * n) + m) = ((s * n) + p)) ==> (q = s)", 197 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN 198 MP_TAC (REWRITE_RULE [LESS_OR_EQ] (SPECL ["q";"s"] LESS_CASES)) THEN 199 STRIP_TAC THENL 200 [X_CHOOSE_THEN "r:num" 201 (SUBST1_TAC o SYM) (MATCH_MP LESS_ADD_SUC (ASSUME "q < s")) THEN 202 PURE_REWRITE_TAC [RIGHT_ADD_DISTRIB;MULT_CLAUSES] THEN 203 SUBST1_TAC (SPECL ["r * n";"(q * n) + n"] ADD_SYM) THEN 204 PURE_REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL ADD_ASSOC))] THEN 205 SUBST1_TAC (SPECL ["q * n";"m"] ADD_SYM) THEN 206 SUBST1_TAC (SPECL ["q * n";"n + ((r * n) + p)"] ADD_SYM) THEN 207 PURE_REWRITE_TAC [EQ_MONO_ADD_EQ] THEN 208 HOL_IMP_RES_THEN 209 (\thm. REWRITE_TAC [MATCH_MP LESS_NOT_EQ (SPEC "(r * n) + p" thm)]) 210 LESS_ADD_MONO; 211 X_CHOOSE_THEN "r:num" 212 (SUBST1_TAC o SYM) (MATCH_MP LESS_ADD_SUC (ASSUME "s < q")) THEN 213 PURE_REWRITE_TAC [RIGHT_ADD_DISTRIB;MULT_CLAUSES] THEN 214 SUBST1_TAC (SPECL ["r * n";"(s * n) + n"] ADD_SYM) THEN 215 PURE_REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL ADD_ASSOC))] THEN 216 SUBST1_TAC (SPECL ["s * n";"p"] ADD_SYM) THEN 217 SUBST1_TAC (SPECL ["s * n";"n + ((r * n) + m)"] ADD_SYM) THEN 218 PURE_REWRITE_TAC [EQ_MONO_ADD_EQ] THEN 219 HOL_IMP_RES_THEN 220 (\thm. 221 REWRITE_TAC 222 [NOT_EQ_SYM (MATCH_MP LESS_NOT_EQ (SPEC "(r * n) + m" thm))]) 223 LESS_ADD_MONO; 224 ASM_REWRITE_TAC []]);; 225 226let UNIQUE_REMAINDER_THM = prove_thm ( 227 `UNIQUE_REMAINDER_THM`, 228 "!m n p. (m < n) /\ (p < n) ==> 229 !q s. (((q * n) + m) = ((s * n) + p)) ==> (m = p)", 230 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN 231 DISCH_THEN (\thm. ASSUME_TAC thm THEN MP_TAC thm) THEN 232 IMP_RES_THEN (\thm. REWRITE_TAC [thm]) UNIQUE_QUOTIENT_THM THEN 233 REWRITE_TAC [SPEC "s * n" ADD_SYM;EQ_MONO_ADD_EQ]);; 234 235let GREATER_0_EXP = prove_thm ( 236 `GREATER_0_EXP`, 237 "!m. 0 < m ==> !n. 0 < m EXP n", 238 GEN_TAC THEN DISCH_TAC THEN 239 INDUCT_TAC THEN 240 REWRITE_TAC [EXP;num_CONV "1";LESS_0] THEN 241 IMP_RES_TAC LESS_MULT_LESS);; 242 243let EXP_ADD_MULT = prove_thm ( 244 `EXP_ADD_MULT`, 245 "!m n p. m EXP (n + p) = ((m EXP n) * (m EXP p))", 246 GEN_TAC THEN INDUCT_TAC THEN GEN_TAC THEN 247 REWRITE_TAC [ADD_CLAUSES;EXP;MULT_CLAUSES;EXP] THEN 248 PURE_REWRITE_TAC [SYM (SPEC_ALL MULT_ASSOC)] THEN 249 FIRST_ASSUM (ACCEPT_TAC o (AP_TERM "$* m") o SPEC_ALL));; 250 251close_theory ();; 252