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; Thu, 3 Feb 1994 11:00:18 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA27490; Thu, 3 Feb 1994 03:43:56 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA27486; Thu, 3 Feb 1994 03:43:47 -0700 Received: from ganymede.inmos.co.uk by dworshak.cs.uidaho.edu with SMTP (1.37.109.8/16.2) id AA20904; Thu, 3 Feb 1994 02:41:27 -0800 Received: from frogland.inmos.co.uk by ganymede.inmos.co.uk; Thu, 3 Feb 1994 10:41:18 GMT From: David Shepherd Message-Id: <5644.9402031040@frogland.inmos.co.uk> Subject: Re: HOL Qs To: info-hol@cs.uidaho.edu (info-hol mailing list) Date: Thu, 3 Feb 1994 10:40:15 +0000 (GMT) X-Mailer: ELM [version 2.4 PL20] Content-Type: text Content-Length: 2020 John Harrison has said: > 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 This isn't really what you want either as if you wanted this theorem then #ADD_ASSUM "2 < 3" TRUTH;; would be a bit faster! What the original question was wanting is a conversion. #let th = REDUCE_CONV "2 < 3";; th = |- (2 < 3) = T #let th' = REDUCE_CONV "23 < 21";; th' = |- (23 < 21) = F N.b., if you are prepared to countenance ADD_CONV as a "primitive" (i.e. mk_thm-ed) conversion which does the arithmetic in (S)ML and constructs the theorems then most such constant arithmetic and comparision operations can be coded fairly efficiently. I.e. 23 < 21 ================ |- 23 = 2+21 (ADD_CONV) (2+21) < 21 ================ |- 21 = 0+21 (ADD_CLAUSES) (2+21) < (0+21) ================ |- (m+p) < (n+p) = m