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; Tue, 5 Apr 1994 15:10:45 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA25214;
          Tue, 5 Apr 1994 06:46:56 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.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 AA25210;
          Tue, 5 Apr 1994 06:46:39 -0600
Received: from infix.cs.ruu.nl by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA14159;
          Tue, 5 Apr 1994 05:47:40 -0700
Received: by relay.cs.ruu.nl id AA25461 (5.67a/IDA-1.5 
          for info-hol@ted.cs.uidaho.edu); Tue, 5 Apr 1994 14:47:29 +0200
From: Wishnu Prasetya <wishnu@cs.ruu.nl>
Message-Id: <199404051247.AA25461@relay.cs.ruu.nl>
Subject: Equational proof style in HOL
To: info-hol@cs.uidaho.edu (hol mailing list)
Date: Tue, 5 Apr 1994 14:47:29 +0200 (METDST)
X-Mailer: ELM [version 2.4 PL23]
Mime-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Content-Length: 1814

Hi,

I just put a package called DerLem in HOL contrib. DerLem is a tool,
built on top of the standard subgoal package, that provides:

(1) A layer to simulate equational proof style which is frequently used
    in pen-and-paper proofs. This will make equational proofs look more
    natural in HOL.

(2) A layer to administrate forward proving. This is to complement the
    subgoal package, which is basically oriented to backward proving.

Features of DerLem include facility to insert comments, naming of
assumptions, and pretty printing. In addition, these features will
improve documentability of the proofs. Documentation and examples are
included in the package. Just to give you an idea, here are examples
of DerLem output:

---------------------------------------------------------------------
#DERIVATION();;

    "(x PLUS y) PLUS (NU y)"

 "$<<" (*HINT: PLUS is monotonic*)

    "(y PLUS y) PLUS (NU y)"

 "$=" (*HINT: PLUS is associative*)

    "y PLUS (y PLUS (NU y))"

 "$=" (*HINT: NU is the invertor and e is unit of PLUS*)

    "y"

() : void

#ETD();;
..... |- ((x PLUS y) PLUS (NU y)) << y
-----------------------------------------------------------------------

#PROOF_SPACE();;

asm0 : (* Assumption *)
    . |- p |--> q

asm1 : (* Assumption *)
    . |- b |--> c /\ c |--> q

asm2 : (* Assumption *)
    . |- a unless b

lem10 :  (* HINT: asm1, |--> is transitive *)
    ... |- b |--> q

lem20 :  (* HINT: asm0, asm2, PSP Law *)
    .. |- (p AND a) |--> ((q AND a) OR b)

lem30 :  (* HINT: lem10, lem20, Cancelation Law *)
    ... |- (p AND a) |--> ((q AND a) OR q)

lem40 :  (* HINT: Lem30, |--> is monotonic *)
    ... |- (p AND a) |--> q

() : void

----------------------------------------------------------------------

OK, that's all. I hope it can be of some help to you.

-Wishnu-