Re: Re: [PVS-Help] partly replace

["=?gb2312?b?0O3H7Ln6?=" <qgxu@xxxxxxxxxxxxxxx>]

Cesar Munoz:

  Thank you very much! 
  The strategy you given is very useful to my some same proving processes. 

	Qingguo Xu
　　　　　　　　qgxu@xxxxxxxxxxxxxxx
　　　　　　　　　　2008-05-23

-------------------------------------------------------------
发件人：Cesar Munoz
发送日期：2008-05-23 04:06:33
收件人：许庆国
抄送：pvs-help
主题：Re: [PVS-Help] partly replace

I don't think that you can do that with replace alone. However, you can
"simulate" that behavior as follows:

(name-replace "AA" "c*a" :hide? nil)
(replace -2 -1)
(replace -1 :dir rl :hide? t)

  -------------------------------------------------------------
   These commands can't work in the case that both sides of a formula is the same.
  -------------------------------------------------------------
On the other hand, if you have the NASA libraries and the Field/Manip
packages, you can define following strategy in pvs-strategies

(defstep replace-in (fnum expr)
  (let ((name (newname "RI")))
    (then
     (relabel "RI:" fnum)
     (invoke (name-replace name "%1" :hide? nil) expr)
     (replace "RI:" -1)
     (replaces -1 :dir rl)
     (delabel "RI:")))
  "Replaces FNUM in EXPR"
  "Replacing ~a in ~a")

{-1}  a = b
{-2}  b * a = c * a
  |-------

Rule? (replace-in -1 (! -2 r))
Replacing -1 in (! -2 r),
this simplifies to:
foo :

{-1}  a = b
{-2}  b * a = c * b
  |-------

The notation (! -2 r) is explained in the documentation of the Manip
package and means "The right hand side expression in formula -2".

Cesar

许庆国 wrote:
> Hi everyone here:
>    Can the prover command (repalce) complete replace some (not all) terms in a certain formula? 
> For example, in the following pending sequent
> 
> [-1] a = b
> [-2] c * a = c * a
> |----
>  {1} ....
> 
> How to convert fnum -2 into c * a = c* b using (replace) command or other command with the help of fnum -1? 
> 
> I have read the help message about (repalce) command, and haven't find the useful information.
> 
> thanks in advance.
> 
> 
> Qingguo XU
> 
> 
>                        qgxu@xxxxxxxxxxxxxxx
>                        2008-05-22
> 
> 
>  
> 
> 
> 

-- 
Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@xxxxxxxxxx
National Institute of Aerospace         mailto:Cesar.A.Munoz@xxxxxxxx
100 Exploration Way  Room 214       http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 325 6907 Fax +1 (757) 325 6988
GPGP Finger Print: 9F10 F3DF 9D76 1377 BCB6  1A18 6000 89F5 C114 E6C4