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