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