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 > hol-info@lists.sourceforge.net > 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info