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, 26 Sep 1995 17:53:43 +0100
Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA041503785;
          Tue, 26 Sep 1995 07:56:25 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
Received: from tuminfo2.informatik.tu-muenchen.de by leopard.cs.byu.edu 
          with ESMTP (1.37.109.15/16.2) id AA041273751;
          Tue, 26 Sep 1995 07:55:51 -0600
Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <26503-2>;
          Tue, 26 Sep 1995 15:55:23 +0200
Received: by tuminfo2.informatik.tu-muenchen.de via suspension id <26484-1>;
          Tue, 26 Sep 1995 15:55:10 +0200
Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) 
          by tuminfo2.informatik.tu-muenchen.de with SMTP id <26478-2>;
          Tue, 26 Sep 1995 15:51:21 +0200
Received: by sunbroy14.informatik.tu-muenchen.de id <8084>;
          Tue, 26 Sep 1995 14:51:08 +0100
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: John.Harrison@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu
In-Reply-To: <"swan.cl.cam.:166970:950926113134"@cl.cam.ac.uk> (message from John Harrison on Tue, 26 Sep 1995 12:31:18 +0100)
Subject: Re: At a Los for something to do? (III)
Message-Id: <95Sep26.145108met.8084@sunbroy14.informatik.tu-muenchen.de>
Date: Tue, 26 Sep 1995 14:51:02 +0100


John writes,

> We do a bit of quantifier manipulation to put it in prenex form with all
> the universal quantifiers outside the existential ones.

and then writes (to accomplish this)

> REWRITE_TAC[TAUT (%`(a ==> b) = ~a \/ b`)] THEN
>     CONV_TAC (REDEPTH_CONV (NOT_FORALL_CONV ORELSEC
>                             NOT_EXISTS_CONV ORELSEC
>                      GEN_REWRITE_CONV I empty_rewrites [DE_MORGAN_THM])) THEN
>     CONV_TAC (REDEPTH_CONV (RIGHT_OR_FORALL_CONV ORELSEC
>                     LEFT_OR_FORALL_CONV)) THEN
>     CONV_TAC (REDEPTH_CONV (OR_EXISTS_CONV ORELSEC
>                             REWR_CONV DISJ_ASSOC)) THEN
>     CONV_TAC (REDEPTH_CONV LEFT_OR_EXISTS_CONV)

This seems like a good example of a proof tool that all too often, HOL
users write in an ad hoc manner. Functions for producing logical normal
forms are pervasively useful, and ought to be standard. To start, here
is my version of NNF:

(*--------------------------------------------------------------------------
 * I am not sure if this really does give NNF, but it's really useful
 * interactively, especially when doing proof by contradiction.
 *--------------------------------------------------------------------------*)
val NNF_CONV =
   let val DE_MORGAN = REWRITE_CONV
                        [Q.TAUT_CONV`~(x==>y) = (x /\ ~y)`,
                         Q.TAUT_CONV`~x \/ y = (x ==> y)`,DE_MORGAN_THM]
       val QUANT_CONV = NOT_EXISTS_CONV ORELSEC NOT_FORALL_CONV
   in REDEPTH_CONV (QUANT_CONV ORELSEC CHANGED_CONV DE_MORGAN)
   end;

Has anybody got a PRENEX_CONV? Others?

Konrad.