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 <20198-0@swan.cl.cam.ac.uk>; Mon, 17 Aug 1992 21:11:57 +0100
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA09606;
          Mon, 17 Aug 92 13:06:16 -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 AA09601;
          Mon, 17 Aug 92 13:06:10 -0700
Received: from auk.cl.cam.ac.uk by swan.cl.cam.ac.uk with SMTP (PP-6.0) to cl 
          id <20118-0@swan.cl.cam.ac.uk>; Mon, 17 Aug 1992 21:04:45 +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 21:04:37 +0100
From: John Harrison <John.Harrison@uk.ac.cam.cl>
Message-Id: <"swan.cl.ca.120:17.07.92.20.04.47"@cl.cam.ac.uk>


Note that to make strict equality valid, you need universal
quantification over the arguments, i.e.

|- (!x. foo x = bar[x]) = (foo = \x. bar[x])

But in general
  
|/- (foo x = bar[x]) = (foo = \x. bar[x])

For one variable it's pretty easy; HALF_MK_ABS gets you one way, and
a bit of beta-conversion will get you the other. For several variables
it gets a bit more complicated. I *think* the following conversion works:

  %----------------------------------------------------------------------------%
  % FUNCTION_CONV "!v1..vk. f x1 .. xn = bod" =                                %
  %         |- (!x1..xn. f x1 .. xn = bod) = (f = \x1..xn. bod)                %
  %----------------------------------------------------------------------------%

  let FUNCTION_CONV tm =
    let l,r = (dest_eq o snd o strip_forall) tm in
    let fn,args = strip_comb l in
    let th1 =
      let apt t f = CONV_RULE (RAND_CONV BETA_CONV) (AP_THM f t)
      and th = ASSUME (mk_eq(fn,itlist (curry mk_abs) args r)) in
      itlist GEN args (rev_itlist apt args th) in
    let th2 =
      let eta xv th =
        let cnv tm = SYM(BETA_CONV(mk_comb(mk_abs(xv,tm),xv))) in
          EXT(GEN xv (CONV_RULE(RAND_CONV cnv) th))
      and th = SPECL args (ASSUME (concl th1)) in
      itlist eta args th in
    IMP_ANTISYM_RULE (DISCH_ALL th2) (DISCH_ALL th1);;

For example:

  #FUNCTION_CONV "!(a:*) y z. f x y z = (z \/ (x = SUC y))";;
  |- (!x y z. f x y z = z \/ (x = SUC y)) =
     (f = (\x y z. z \/ (x = SUC y)))
  Run time: 0.2s
  Intermediate theorems generated: 41

Anyway, it might give you some ideas.

John.