Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Mon, 3 May 1993 18:36:22 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA14229;
          Mon, 3 May 93 10:28:36 -0700
Sender: info-hol-request@ted.cs.uidaho.edu
Errors-To: info-hol-request@ted.cs.uidaho.edu
Precedence: bulk
Received: from air52.larc.nasa.gov by ted.cs.uidaho.edu (16.6/1.34) id AA14224;
          Mon, 3 May 93 10:28:29 -0700
Received: by air52.larc.nasa.gov (5.65.1/lanleaf2.4) id AA01091;
          Mon, 3 May 93 13:28:30 -0400
Message-Id: <9305031728.AA01091@air52.larc.nasa.gov>
Date: Mon, 3 May 93 13:28:30 -0400
From: Victor "A." Carreno <vac@air16.larc.nasa.gov>
To: coe@leopard.cs.uidaho.edu
Subject: Re: help
In-Reply-To: Mail from 'coe@leopard.cs.uidaho.edu (Mike Coe)' dated: Mon, 3 May 93 9:59:12 PDT
Cc: info-hol@ted.cs.uidaho.edu


> Is there a way prove the following in HOL:

> ((t-1)+1) = t

This is not true for t=0.

you can prove "0<t ==> (((t-1)+1) = t)";;

or in general "!n. n<t ==>  (((t-n)+n) = t)";;

The library `arith` will do it:

# load_library `arith`;;
# ARITH_CONV "!n. n<t ==>  (((t-n)+n) = t)";;
|- (!n. n < t ==> ((t - n) + n = t)) = T

Also, the theorem 
SUB_ADD arithmetic
|- !m n. n <= m ==> ((m - n) + n = m)

is built in in HOL.

Victor.