Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: tfm@dcs.gla.ac.uk
Message-Id: <9407110836.AA11856@switha.dcs.gla.ac.uk>
To: chou@cs.ucla.edu
Cc: info-hol@leopard.cs.byu.edu, tfm@dcs.gla.ac.uk
Subject: Re: "Meta" rewriting
In-Reply-To: Your message of "Sun, 10 Jul 94 02:09:38 PDT." <9407100909.AA26645@maui.cs.ucla.edu>
Date: Mon, 11 Jul 94 09:36:53 +0100


Ching Tsun writes:

> Consider the conversion FORALL_AND_CONV.  Wouldn't it be great if
> one could prove a single theorem:
> 
> (*)     |- !P Q. (!x:'a. P x /\ Q x) = (!x. P x) /\ (!x. Q x)
> 
> and then use (*) to "rewrite", say, !n. (n + i < 0) /\ (n + j > 0)
> into (!n. n + i < 0) /\ (!n. n + j > 0)?  Unfortunately, as we all
> know, this doesn't work.  I find this situation very annoying...

I think there's a good case for making some kind of second-order
rewriting available in HOL.  This could probably be best done by
writing a good second-order matcher, which would then play the same
role as the current "match" function in rewriting, as well as things
like MATCH_MP.  This is not a new idea - I think there are several
implementations already out there.

The only problem I see is that of efficiency: I'm not convinced that
an INDUCT_THEN, say, based on a general 2nd order matching algorithm
could equal the speed of the hand-coded one.

Tom