Return-Path: <John.Harrison-request@cl.cam.ac.uk>
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, 27 Jan 1994 21:36:55 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA18445;
          Thu, 27 Jan 1994 14:22:44 -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 AA18427;
          Thu, 27 Jan 1994 14:22:17 -0700
Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) to cl; Thu, 27 Jan 1994 21:17:01 +0000
To: Sam Nelson <snelson@csci0.uark.edu>
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: HOL Qs
In-Reply-To: Your message of "Thu, 27 Jan 94 14:38:40 CST." <Pine.3.89.9401271411.A26409-0100000@csci0.uark.edu>
Date: Thu, 27 Jan 94 21:16:56 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:245080:940127211703"@cl.cam.ac.uk>


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

An easier alternative is to use the reduce library (or the arith library, which
can also deal with a useful class of terms involving variables). For instance:

| #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
|
| #e REDUCE_TAC;;
| OK..
| goal proved
| |- 3 < 6

Hope this helps,

John.