Sender: info-hol-request@leopard.cs.byu.edu
Errors-To: info-hol-request@leopard.cs.byu.edu
Precedence: list
From: des@bristol.st.com (David Shepherd)
Message-Id: <9601151729.ZM24396@bristol.st.com>
Date: Mon, 15 Jan 1996 17:29:13 +0000
To: info-hol@leopard.cs.byu.edu
Subject: (Fwd) Re: general renaming
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii

On Jan 14,  5:44pm, John Harrison wrote:
> Subject: Re: general renaming
>
> Paul writes:
>
> | I need to rename (free) variables in theorems, eg,
> |         |- a = b
> | into
> |         |- a = c
> |
> | Is there function in HOL88 which does this?  I can see
> | how to write more own with a few functions, but I
> | wanted to reuse if possible.
>
> The INST function will probably do what you want. In the example you
> cite one would do:
>
>   INST ["c","b"] <theorem>
>
> However it won't rename the same variable in assumptions; as far as
> I know there's no function to do that directly, so you'd have to write
> your own.

This should work

local fun COUNT_UNDISCH 0 thm = thm
        | COUNT_UNDISCH n thm = COUNT_UNDISCH (n -1) (UNDISCH thm)
in
fun INST_ALL_TY_TERM (tm_subst,type_subst) th =
    let val num_hyp = length (hyp th)
    in
        COUNT_UNDISCH num_hyp(INST tm_subst(INST_TYPE type_subst(DISCH_ALL
th)))
    end
end;

-- n.b. this renames types as well but its obvious how to remove that!


-- 
--------------------------------------------------------------------------
                              david shepherd
 SGS-THOMSON Microelectronics Ltd, 1000 aztec west, bristol bs12 4sq, u.k.
        tel/fax: +44 1454 611638/617910  email: des@bristol.st.com      
      "whatever you don't want, you don't want negative advertising"