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 19:31:31 +0000 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA20447; Wed, 2 Feb 1994 12:03:38 -0700 Sender: info-hol-request@leopard.cs.byu.edu Errors-To: info-hol-request@leopard.cs.byu.edu Precedence: bulk Received: from uafhp.uark.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA20443; Wed, 2 Feb 1994 12:03:35 -0700 Received: from csci0.uark.edu by uafhp.uark.edu with SMTP (1.37.109.4/15.6) id AA26894; Wed, 2 Feb 94 12:59:11 -0600 Received: by domain_csci (4.1/SMI-4.1) id AA11673; Wed, 2 Feb 94 12:55:50 CST Date: Wed, 2 Feb 1994 12:55:49 -0600 (CST) From: Sam Nelson Subject: Re: HOL Qs To: info-hol@leopard.cs.byu.edu In-Reply-To: <"swan.cl.cam.:245080:940127211703"@cl.cam.ac.uk> Message-Id: Mime-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII > > Sam Nelson writes: > > | Currently I`m trying to reduce ". |- n < m". down to a boolean > | value. However, when I try to use a REWRITE_RULE for LESS, hol spits it > | out. Does this occur because LESS is an infix definition? Can anybody > | tell me what I need to do? > > The problem is that inside HOL, the numerals are just atomic constants, and > hence no general rewrite rule applies to them. One way round your problem is to > eliminate the numeral constants in favour of their definitions in terms of 0 > and SUC. Then rewriting as you tried should solve the problem, e.g. > > | #g "3 < 6";; > | "3 < 6" > | > | () : void > | Run time: 0.0s > | > | #e(REWRITE_TAC(map num_CONV ["6";"5";"4";"3";"2";"1"]));; > | OK.. > | "(SUC(SUC(SUC 0))) < (SUC(SUC(SUC(SUC(SUC(SUC 0))))))" > | > | () : void > | Run time: 0.2s > | Intermediate theorems generated: 25 > | > | #e(REWRITE_TAC[LESS_MONO_EQ; LESS_0]);; > | OK.. > | goal proved > | |- (SUC(SUC(SUC 0))) < (SUC(SUC(SUC(SUC(SUC(SUC 0)))))) > | |- 3 < 6 > | > | Previous subproof: > | goal proved > | () : void > | Run time: 0.1s > | Intermediate theorems generated: 23 What I had in mind was something that starts with #let th1 = ASSUME " 2 < 3";; th1 = . |- 2 < 3 #let th2 = REWRITE [LESS] th1;; And would REWRITE the less than relation using the defintion of LESS as defined in prim_rec, but instead I get: unbound or non-assignable variable REWRITE unbound or non-assignable variable LESS 2 errors in typing typecheck failed> because I cannot get HOL to admit that there is a theorem called LESS. What I would like to be able to do is take a general case for m < n, and replace it with T of F depending on the values of m and n. I hope this makes my goals a little more clear. Sam Nelson