Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
To: shb@com.oracorp
Cc: info-hol@edu.uidaho.cs.ted, Tom.Melham@uk.ac.cam.cl
Subject: Re: Partial instantiation
In-Reply-To: Your message of Fri, 28 Feb 92 11:18:40 -0500. <9202281618.AA02689@sparta.oracorp.com>
Date: Fri, 28 Feb 92 17:44:43 +0000
From: Tom.Melham@uk.ac.cam.cl
Message-Id: <"swan.cl.ca.899:28.01.92.17.45.01"@cl.cam.ac.uk>


Regarding Steve Brackin's query:

> Can someone give me a convenient way of partially instantiating
> universally-quantified conclusions?  For x, y, z, t nums I'd like to be
> able to go, say, from !x y z t. f(x,y,z,t) to !x y t. f(x,y,3,t).
> SPECL doesn't seem to be able to do it, and I'd like to avoid having to
> use combinations of SPEC and GEN.

there is no built-in function for doing just this.  But such a function is
easy to program in ML.

To illustrate this, and to illustrate the kind of design decisions that have to
be made in tool-building, I attach an implementation that I hacked together
quickly just now. The function SSPEC takes a list of term/variable pairs:

   ["t1","v1";...;"tn","vn"]

and specializes only the quantified variables xi in a theorem

   |- !x1 ... xm. body

for which xi = vj for some vj in {v1,...,vn}. (The hardest thing about this
function would be documenting it properly!)  Note that the implementation has
error checking and useful messages, and that I have made the design decision to
fail if the list contains a variable vj not among the quantified variables of
the theorem.  Other design decisions for handling this case are also possible.

Note also the following behaviour:

   #SSPECL ["m:num","n:num"] ADD_ASSOC;;
   |- !m p. m + (m + p) = (m + m) + p

The "m" gets captured. Perhaps SSPECL should be redesigned to avoid
this---e.g. by priming "m".

Finally, note that this implementation has a bug!  I leave it as an exercise to
find the bug and rewrite SSPECL to correct it.  Hint: it has something to do
with free variables in the assumptions of the theorem.

Tom


=============================================================================
let SSPECL =
    let check vs (t,v) =
        not(is_var v) => failwith `attempt to specialize non-variable` |
        not(type_of t = type_of v) => failwith `type inconsistency` |
        not(mem v vs) => failwith (fst(dest_var v) ^ ` not quantified`) | v in
    \sp th.
        (let (vs,body) = strip_forall(concl th) in
         let svs = map (check vs) sp in
         let rest = subtract vs svs in
             GENL rest (INST sp (SPECL vs th))) ?\st
        failwith `SSPECL: ` ^ st;;