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; Wed, 2 Feb 1994 21:16:28 +0000
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA22466;
          Wed, 2 Feb 1994 13:54:17 -0700
Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: bulk
Received: from air52.larc.nasa.gov by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA22461;
          Wed, 2 Feb 1994 13:54:10 -0700
Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA28463;
          Wed, 2 Feb 94 15:49:37 -0500
Message-Id: <9402022049.AA28463@air52.larc.nasa.gov>
Date: Wed, 2 Feb 94 15:49:37 -0500
From: Victor "A." Carreno <vac@air16.larc.nasa.gov>
To: snelson@csci0.uark.edu
Subject: Re: HOL Qs
In-Reply-To: Mail from 'Sam Nelson <snelson@csci0.uark.edu>' dated: Wed, 2 Feb 1994 12:55:49 -0600 (CST)
Cc: info-hol@leopard.cs.byu.edu


>What I had in mind was something that starts with
> #let th1 = ASSUME " 2 < 3";;
>th1 = . |- 2 < 3

>#let th2 = REWRITE [LESS] th1;;

#let th1 = ASSUME " 2 < 3";;
th1 = . |- 2 < 3

#let LESS = definition `prim_rec` `LESS`;;
LESS = |- !m n. m < n = (?P. (!n'. P(SUC n') ==> P n') /\ P m /\ ~P n)

#let th2 = REWRITE_RULE [LESS] th1;;
th2 = . |- ?P. (!n'. P(SUC n') ==> P n') /\ P 2 /\ ~P 3

>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.

#let th1 = ASSUME "2<3 /\ (b:bool) \/ 4<1";;
th1 = . |- 2 < 3 /\ b \/ 4 < 1

#load_library `reduce`;;
Loading library reduce ...
Library reduce loaded.

#let th2 = PURE_REWRITE_RULE[(REDUCE_CONV "2<3")] th1;;
th2 = . |- T /\ b \/ 4 < 1

#let th3 = PURE_REWRITE_RULE[(REDUCE_CONV "4<1")] th2;;
th3 = . |- T /\ b \/ F

#let th4 = REWRITE_RULE[(REDUCE_CONV "2<3")] th1;;
th4 = . |- b \/ 4 < 1

#let th5 = REWRITE_RULE[(REDUCE_CONV "4<1")] th4;;
th5 = . |- b

Victor.