Hi Lu,
This is easy to code up in HOL. You can strip
the leading foralls, use INST to replace your variable
by a term and then put all the foralls back, except
for the replaced one:
fun MY_SPEC v tm th =
let val (vs,body) = strip_forall(concl th)
val (_,vs') = Lib.pluck (equal v) vs
in
GENL vs' (INST [v |-> tm] (SPEC_ALL th))
end;
Example:
- val th = mk_thm([],``!(x1:num) (x2:'a) (x3:bool list). P x1 x2 x3
x3``);
> val th = |- !x1 x2 x3. P x1 x2 x3 x3 : thm
- MY_SPEC ``x2:'a`` ``foo:'a`` th;
> val it = |- !x1 x3. P x1 foo x3 x3 : thm
You will have to take care that v and tm have the same
type.
Cheers,
Konrad.
On Sep 11, 2009, at 12:15 PM, Lu Zhao wrote:
> Hi,
>
> I have a theorem of the form:
>
> !x1 x2 ... x(i-1) xi x(i+1) ... xn. t
>
> and I'd like to instantiate xi to another term, say y, without
> touching
> other universally quantified variables, namely, I want to rewrite
> it to:
>
> !x1 x2 ... x(i-1) x(i+1) ... xn. t[y/xi]
>
> Is there a handy operation for this, any version of SPECL, or I can
> change the order of xs?
>
> Thanks a lot.
> Lu
>
> ----------------------------------------------------------------------
> --------
> Let Crystal Reports handle the reporting - Free Crystal Reports
> 2008 30-Day
> trial. Simplify your report design, integration and deployment -
> and focus on
> what you do best, core application coding. Discover what's new with
> Crystal Reports now. http://p.sf.net/sfu/bobj-july
> _______________________________________________
> hol-info mailing list
> [email protected]
> https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Let Crystal Reports handle the reporting - Free Crystal Reports 2008 30-Day
trial. Simplify your report design, integration and deployment - and focus on
what you do best, core application coding. Discover what's new with
Crystal Reports now. http://p.sf.net/sfu/bobj-july
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
