Re: [PVS-Help] turning off rewrite

[David Naumann <naumann@cs.stevens.edu>]

Hi Shankar,

So I see in *Auto-Rewrites* that after install-rewrites this function <= 
is installed, which confirms the problem.  What I want to do is prevent 
any rewriting with this definition.  Isn't that what the AUTO_REWRITE- 
declaration is for?

--dave

On Sat, 22 Jul 2006, Natarajan Shankar wrote:

> Dave:
>  The Emacs command M-x show-auto-rewrites should show you the active
> rewrites in the *Auto-Rewrites* buffer.  You can use the stop-rewrite prover
> command on the rewrite as named in the *Auto-Rewrites* buffer to stop it.
>
> To stop the recursive rewriting loop, you need to arrange the definition so
> that the measure decreases whenever the top conditional is resolved.
>
> -Shankar
>
>> I have a recursively defined relation named <= on a datatype which I don't
>> want to use as a rewrite.  Following the definition of <= I declare
>>
>>    AUTO_REWRITE- <= : [dty,dty -> bool]
>>
>> But grind on sequents involving <= seems to diverge rewriting it:
>>
>>    Warning: Rewriting depth = 50; Rewriting with <=
>>
>> I tried (stop-rewrite "myTheoryname.<=") which yields
>>
>>    classtableSig.<= is not an auto-rewrite
>>
>> How do I determine the installed rewrites, and more importantly uninstall
>> this one?
>