Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu by swan.cl.cam.ac.uk with SMTP (PP-6.0) 
          id <17267-0@swan.cl.cam.ac.uk>; Mon, 17 Aug 1992 17:53:54 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09177;
          Mon, 17 Aug 92 09:47:14 -0700
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA09172;
          Mon, 17 Aug 92 09:47:06 -0700
Received: from puffin.cl.cam.ac.uk by swan.cl.cam.ac.uk 
          with SMTP (PP-6.0) to cl id <16980-0@swan.cl.cam.ac.uk>;
          Mon, 17 Aug 1992 17:45:25 +0100
To: weiss@edu.uidaho.cs.leopard (Phil Weiss)
Cc: info-hol@edu.uidaho.cs.ted (HOL Mailing List)
Subject: Re: Function rewrites
In-Reply-To: Your message of Mon, 17 Aug 92 08:57:33 -0700. <9208171557.AA18221@leopard.cs.uidaho.edu>
Date: Mon, 17 Aug 92 17:45:19 +0100
From: Brian Graham <btg@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.982:17.07.92.16.45.27"@cl.cam.ac.uk>


weiss@edu.uidaho.cs.leopard (Phil Weiss) writes:
> HOL converts definitions of the form

> foo = (\x. bar)

> to

> foo x = bar

> I was wondering if anyone had written a conversion to rewrite
> terms of the second form back into the first form.  ???

Not sure what you mean here, since for example:

	#let foo = new_definition (`foo`, "foo = \x. x + 1");;
	foo = |- foo = (\x. x + 1)

this definition is not converted as you said.
However we can get a theorem of the said form.
	#let th = CONV_RULE (ONCE_DEPTH_CONV BETA_CONV)(AP_THM foo "x:num");;
	th = |- foo x = x + 1

From this, recovering the original form of theorem is trivial.
	#ABS "x:num" th;;
	|- (\x. foo x) = (\x. x + 1)

	#REWRITE_RULE [ETA_AX] it;;
	|- foo = (\x. x + 1)


Occasionally there are times that doing the opposite of a BETA reduction
is handy.  I had written a conversion to do this a long time ago, and
it may be useful.

% ================================================================= %
% A conversion to abstract out a particular term.                   %
%                                                                   %
% Written by: Brian Graham --- long, long ago (1989 ???)            %
%                                                                   %
% Usage:                                                            %
% ******                                                            %
% BETA_INV_CONV : ((term # term) -> conv)                           %
%                                                                   %
%                   t[t2]                                           %
%       ------------------------------(t1,t2)                       %
%        |- t[t2] = (\t1.t[t1/t2]) t2                               %
%                                                                   %
% Example:                                                          %
% ********                                                          %
% #BETA_INV_CONV ("t1:num", "SUC t") "PRE(SUC t)";;                 %
% |- PRE(SUC t) = (\t1. PRE t1)(SUC t)                              %
% ================================================================= %
let BETA_INV_CONV (t1,t2) trm =
 (SYM o RIGHT_BETA)
 (REFL(mk_comb (mk_abs(t1,subst [t1,t2] trm), t2)));;


Brian Graham