1% PROOF : Modulus Function for Natural Numbers % 2% FILE : mod.ml % 3% % 4% DESCRIPTION : Defines MOD function for natural numbers and proves % 5% the following theorem: % 6% % 7% !m n k. n < m ==> (n = ((k * m) + n) MOD m) % 8% % 9% This theorem uses the division algorithm theorem for % 10% natural numbers proven by T.Melham. % 11% % 12% AUTHOR : J.Joyce % 13% DATE : 31 March 1987 % 14 15new_theory `mod`;; 16 17loadt `misc`;; 18 19new_parent `da`;; 20 21let MOD = new_infix_definition ( 22 `MOD`, 23 "$MOD n m = @r. ?q. (n = (q * m) + r) /\ (r < m)");; 24 25let DA = theorem `da` `DA`;; 26 27let lemma1 = TAC_PROOF (( 28 [], 29 "!m n. 0 < m ==> ?q. (n = (q * m) + (n MOD m)) /\ (n MOD m) < m"), 30 REPEAT STRIP_TAC THEN 31 HOL_IMP_RES_THEN (ASSUME_TAC o NOT_EQ_SYM) LESS_NOT_EQ THEN 32 REWRITE_TAC [MOD;SELECT_RULE (UNDISCH_ALL (SPECL ["n";"m"] DA))]);; 33 34let lemma2 = 35 GEN_ALL 36 (SUBS [SPECL ["m";"p"] ADD_SYM;SPECL ["n";"p"] ADD_SYM] 37 (SPEC_ALL EQ_MONO_ADD_EQ));; 38 39let lemma3 = TAC_PROOF ( 40 ([],"!m n. (?p. p + n = m) = (n <= m)"), 41 REPEAT STRIP_TAC THEN EQ_TAC THENL 42 [DISCH_THEN (STRIP_THM_THEN (SUBST1_TAC o SYM)) THEN 43 SUBST1_TAC (SPECL ["p";"n"] ADD_SYM) THEN 44 REWRITE_TAC [LESS_EQ_ADD]; 45 DISCH_THEN (DISJ_CASES_TAC o (PURE_REWRITE_RULE [LESS_OR_EQ])) THENL 46 [IMP_RES_TAC LESS_ADD; 47 EXISTS_TAC "0" THEN ASM_REWRITE_TAC [ADD_CLAUSES]]]);; 48 49let th1 = 50 SPECL ["n";"((p' * m) + p) + m"] 51 (INST_TYPE [":num",":*"] EQ_SYM_EQ);; 52let th2 = 53 CONV_RULE EXISTS_IMP_FORALL_CONV 54 (fst (EQ_IMP_RULE (SPECL ["n";"m"] lemma3)));; 55 56let lemma4 = TAC_PROOF (( 57 [], 58 "!m n p q s. 59 n < m /\ p < m /\ q < s ==> ~((q * m) + n = (s * m) + p)"), 60 REPEAT GEN_TAC THEN DISCH_THEN STRIP_ASSUME_TAC THEN 61 STRIP_THM_THEN SUBST1_TAC (MATCH_MP LESS_ADD_1 (ASSUME "q < s")) THEN 62 PURE_REWRITE_TAC [ADD1;RIGHT_ADD_DISTRIB] THEN 63 PURE_REWRITE_TAC [lemma2;GEN_ALL (SYM (SPEC_ALL ADD_ASSOC))] THEN 64 PURE_REWRITE_TAC [MULT_CLAUSES] THEN 65 SUBST1_TAC (SPECL ["m";"p"] ADD_SYM) THEN 66 PURE_REWRITE_TAC [ADD_ASSOC] THEN 67 SUBST1_TAC th1 THEN 68 STRIP_TAC THEN 69 IMP_RES_TAC th2 THEN 70 IMP_RES_TAC (GEN_ALL (snd (EQ_IMP_RULE (SPEC_ALL NOT_LESS)))));; 71 72let th1 = 73 PURE_REWRITE_RULE [lemma2;ASSUME "q = k"] 74 (ASSUME "(k * m) + n = (q * m) + (((k * m) + n) MOD m)");; 75 76let lemma5 = TAC_PROOF ( 77 ([],"!m n. m < n ==> 0 < n"), 78 REPEAT STRIP_TAC THEN 79 DISJ_CASES_TAC (SPEC "n" LESS_0_CASES) THENL 80 [ASSUME_TAC (SUBS [SYM (ASSUME "0 = n")] (ASSUME "m < n")) THEN 81 IMP_RES_TAC NOT_LESS_0; 82 FIRST_ASSUM ACCEPT_TAC]);; 83 84let MOD_THM = prove_thm ( 85 `MOD_THM`, 86 "!m n k. n < m ==> (n = ((k * m) + n) MOD m)", 87 REPEAT STRIP_TAC THEN 88 IMP_RES_TAC lemma5 THEN 89 HOL_IMP_RES_THEN 90 STRIP_ASSUME_TAC (SPECL ["m";"(k * m) + n"] lemma1) THEN 91 DISJ_CASES_TAC (SPECL ["k";"q"] LESS_CASES) THENL 92 [IMP_RES_TAC lemma4; 93 DISJ_CASES_TAC 94 (PURE_REWRITE_RULE [LESS_OR_EQ] (ASSUME "q <= k")) THENL 95 [ASSUME_TAC 96 (SYM 97 (ASSUME "(k * m) + n = (q * m) + (((k * m) + n) MOD m)")) THEN 98 IMP_RES_TAC lemma4; 99 ACCEPT_TAC th1]]);; 100 101close_theory ();; 102