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 : Division for Natural Numbers % 10% FILE : div.ml % 11% % 12% DESCRIPTION : Defines division for natural numbers and proves % 13% some useful theorems about this function including % 14% the following theorem: % 15% % 16% !m n. n < m ==> !k. (((k * m) + n) Div m) = k % 17% % 18% These theorems depend on the division algorithm % 19% theorem for natural numbers proven by T.Melham. % 20% % 21% AUTHOR : J.Joyce % 22% DATE : 16 July 1987 % 23% ===================================================================== % 24 25new_theory `div`;; 26 27new_parent `da`;; 28new_parent `arith`;; 29 30let DA = theorem `da` `DA`;; 31 32let LESS_LESS_0 = theorem `arith` `LESS_LESS_0`;; 33let LESS_ADD_SUC = theorem `arith` `LESS_ADD_SUC`;; 34let LESS_MONO_MULT_EQ = theorem `arith` `LESS_MONO_MULT_EQ`;; 35let UNIQUE_QUOTIENT_THM = theorem `arith` `UNIQUE_QUOTIENT_THM`;; 36 37let Div = new_infix_definition ( 38 `Div`, 39 "$Div n m = @q. ?r. (n = (q * m) + r) /\ (r < m)");; 40 41let EXISTS_DIV = prove_thm ( 42 `EXISTS_DIV`, 43 "!m. 0 < m ==> !n. ?r. (n = ((n Div m) * m) + r) /\ (r < m)", 44 let th1 = UNDISCH (SPEC_ALL DA) in 45 let th2 = ASSUME (snd (dest_exists (concl th1))) in 46 let th3 = ASSUME (snd (dest_exists (concl th2))) in 47 let th4 = EXISTS (mk_exists ("r",concl th3),"r") th3 in 48 let th5 = EXISTS (mk_exists ("q",concl th4),"q") th4 in 49 let th6 = CHOOSE ("r",th1) (CHOOSE ("q",th2) th5) in 50 let th7 = GEN_ALL (DISCH_ALL th6) in 51 REPEAT STRIP_TAC THEN 52 HOL_IMP_RES_THEN (ASSUME_TAC o NOT_EQ_SYM) LESS_NOT_EQ THEN 53 REWRITE_TAC [Div;SELECT_RULE (UNDISCH_ALL (SPECL ["m";"n"] th7))]);; 54 55let Div_THM = prove_thm ( 56 `Div_THM`, 57 "!m n. n < m ==> !k. (((k * m) + n) Div m) = k", 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_DIV THEN 62 IMP_RES_THEN 63 (\thm. (ACCEPT_TAC (SYM thm)) ? ALL_TAC) UNIQUE_QUOTIENT_THM);; 64 65let Div_MULT_LESS_EQ = prove_thm ( 66 `Div_MULT_LESS_EQ`, 67 "!m. 0 < m ==> !n. ((n Div m) * m) <= n", 68 REPEAT STRIP_TAC THEN 69 HOL_IMP_RES_THEN 70 ((CHOOSE_THEN (\thm. (SUBST_OCCS_TAC [[2],CONJUNCT1 thm]))) o 71 (SPEC "n")) EXISTS_DIV THEN 72 REWRITE_TAC [LESS_EQ_ADD]);; 73 74let LESS_MULT_Div_LESS = prove_thm ( 75 `LESS_MULT_Div_LESS`, 76 "!m. 0 < m ==> !n p. (n < (p * m)) ==> ((n Div m) < p)", 77 REPEAT STRIP_TAC THEN 78 HOL_IMP_RES_THEN 79 (DISJ_CASES_TAC o (REWRITE_RULE [LESS_OR_EQ]) o (SPEC "n")) 80 Div_MULT_LESS_EQ THENL 81 [HOL_IMP_RES_THEN ASSUME_TAC LESS_TRANS THEN 82 IMP_RES_THEN 83 (\thm. FIRST_ASSUM (ACCEPT_TAC o (PURE_REWRITE_RULE [thm]))) 84 LESS_MONO_MULT_EQ; 85 ASSUME_TAC 86 (SUBS 87 [SYM (ASSUME "(n Div m) * m = n")] (ASSUME "n < (p * m)")) THEN 88 IMP_RES_THEN 89 (\thm. FIRST_ASSUM (ACCEPT_TAC o (PURE_REWRITE_RULE [thm]))) 90 LESS_MONO_MULT_EQ]);; 91 92let LESS_Div_LESS_EQ = prove_thm ( 93 `LESS_Div_LESS_EQ`, 94 "!m. 0 < m ==> !n p. (n < p) ==> ((n Div m) <= (p Div m))", 95 PURE_REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL NOT_LESS))] THEN 96 REPEAT STRIP_TAC THEN 97 MP_TAC (ASSUME "n < p") THEN 98 HOL_IMP_RES_THEN 99 ((X_CHOOSE_THEN "qn:num" 100 (\thm. 101 SUBST1_TAC (CONJUNCT1 thm) THEN ASSUME_TAC (CONJUNCT2 thm))) o 102 (SPEC "n")) EXISTS_DIV THEN 103 HOL_IMP_RES_THEN 104 ((X_CHOOSE_THEN "qp:num" 105 (\thm. 106 SUBST1_TAC (CONJUNCT1 thm) THEN ASSUME_TAC (CONJUNCT2 thm))) o 107 (SPEC "p")) EXISTS_DIV THEN 108 X_CHOOSE_THEN "q" (SUBST1_TAC o SYM) 109 (MATCH_MP LESS_ADD_SUC (ASSUME "(p Div m) < (n Div m)")) THEN 110 PURE_REWRITE_TAC [ADD_CLAUSES;MULT_CLAUSES;RIGHT_ADD_DISTRIB] THEN 111 PURE_REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL ADD_ASSOC))] THEN 112 SUBST1_TAC (SPECL ["q * m";"((p Div m) * m) + (m + qn)"] ADD_SYM) THEN 113 PURE_REWRITE_TAC [GEN_ALL (SYM (SPEC_ALL ADD_ASSOC))] THEN 114 PURE_REWRITE_TAC 115 [REWRITE_RULE [] (GEN_ALL (AP_TERM "$~" (SPEC_ALL NOT_LESS)))] THEN 116 ASSUME_TAC 117 (MATCH_MP LESS_EQ_TRANS 118 (LIST_CONJ 119 [MATCH_MP LESS_IMP_LESS_OR_EQ (ASSUME "qp < m"); 120 SPECL ["m";"qn + (q * m)"] LESS_EQ_ADD])) THEN 121 ASSUME_TAC (SPEC "(p Div m) * m" LESS_EQ_REFL) THEN 122 IMP_RES_TAC LESS_EQ_LESS_EQ_MONO THEN 123 ASM_REWRITE_TAC []);; 124 125close_theory ();; 126