Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4); Mon, 11 Jan 1993 10:16:23 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA18589; Mon, 11 Jan 93 01:47:14 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA18584; Mon, 11 Jan 93 01:47:02 -0800 Received: from heron.cl.cam.ac.uk (user ww (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Mon, 11 Jan 1993 09:45:46 +0000 To: weiss@edu.uidaho.cs.leopard (P. Andrew Weiss), info-hol@edu.uidaho.cs.ted (HOL mailing list) Subject: Re: Quick help Date: Mon, 11 Jan 93 09:45:33 +0000 From: Wai Wong Message-Id: <"swan.cl.ca.432:11.01.93.09.45.50"@cl.cam.ac.uk> I have the save feeling as you when working wih DIV and MOD, and I think there should be more theorems about these operations in the system. Over the time, I have got a small collection of such theorems. They are listed at the end of this message. Since we are on this topic, I'd like to share them with everyone. I'd like to put them into the system in the next version if there is no strong objection. Meanwile, if anyone like to have them right now, please send me a message. Wai ----------- Theorems about MULT, DIV and MOD ----------------- MULT_LESS_MONO |- !m n p. 0 < p ==> m < n ==> (m * p) < (n * p) NOT_MULT_LESS_0 |- !m n. 0 < m /\ 0 < n ==> 0 < (m * n) SUC_MOD |- !n m. (SUC n) < m ==> ((SUC n) MOD m = SUC(n MOD m)) MOD_MOD_MOD |- !x m n. 0 < n /\ 0 < m ==> ((x MOD (n * m)) MOD n = x MOD n) SUC_MOD_REFL |- !n. (SUC n) MOD (SUC n) = 0 MULT_DIV |- !n q. 0 < n ==> ((q * n) DIV n = q) DIV_ONE |- !q. q DIV 1 = q LESS_DIV_EQ_ZERO |- !r n. r < n ==> (r DIV n = 0) SUC_DIV_REFL |- !n. (SUC n) DIV (SUC n) = 1 RIGHT_ADD_DIV |- !n r. 0 < n ==> ((n + r) DIV n = SUC(r DIV n)) RIGHT_ADD_DIV_DISTRIB |- !x n r. 0 < n ==> (((x * n) + r) DIV n = x + (r DIV n)) SUC_DIV |- !n. 0 < n ==> (!x. ((SUC x) DIV n = x DIV n) \/ ((SUC x) DIV n = SUC(x DIV n))) LESS_MONO_DIV |- !n p q. 0 < n ==> p < q ==> (p DIV n) <= (q DIV n) LESS_EQ_MONO_DIV |- !n p q. 0 < n ==> p <= q ==> (p DIV n) <= (q DIV n) DIV_DIV_DIV_MULT |- !x m n. 0 < m /\ 0 < n ==> ((x DIV m) DIV n = x DIV (m * n)) --------- End of message ----------------------------