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