Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 2 Feb 1994 21:12:59 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA22279; Wed, 2 Feb 1994 13:44:46 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA22272; Wed, 2 Feb 1994 13:44:20 -0700 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 2 Feb 1994 20:32:28 +0000 To: Sam Nelson Cc: info-hol@leopard.cs.byu.edu Subject: Re: HOL Qs In-Reply-To: Your message of "Wed, 02 Feb 94 12:55:49 CST." Date: Wed, 02 Feb 94 20:32:11 +0000 From: John Harrison Message-Id: <"swan.cl.cam.:173250:940202203245"@cl.cam.ac.uk> Sorry -- the example I gave was for backward proof; to do the corresponding thing in forward proof, essentially replace `_TAC' with `_RULE'. Again, it's simplest to use the reduce library: #load_library `reduce`;; Loading library reduce ... Extending help search path. Loading boolean conversions........ Loading arithmetic conversions.................. Loading general conversions, rule and tactic..... Library reduce loaded. () : void #top_print print_all_thm;; - : (thm -> void) #let th1 = ASSUME " 2 < 3";; th1 = 2 < 3 |- 2 < 3 #let th2 = REDUCE_RULE th1;; th2 = 2 < 3 |- T #let th3 = REDUCE_RULE (ASSUME "23 < 21");; th3 = 23 < 21 |- F You are right that there is actually a theorem called LESS, but it's set up not to autoload. This is because it's actually the definition of the < operator, and is not particularly helpful in normal proofs. If you really want it, you can get at it as follows: #definition `prim_rec` `LESS`;; |- !m n. m < n = (?P. (!n'. P(SUC n') ==> P n') /\ P m /\ ~P n) This is very basic definition, before almost any other logical infrastructure has been developed. To quote from the comments in |ml/mk_prim_rec.ml|: The following definition of < is from Hodges's article in "The Handbook of Philosophical Logic" (page 111): m < n = ?P. (!n. P(SUC n) ==> P n) /\ P m /\ ~(P n) Hope this is more help. John.