[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] question about term rewriting



Dear PVS users,

I am exploring PVS' term rewriting capabilities and have stumbled across 
a phenomenon which I cannot make sense of. See the following theory:

sub: THEORY
BEGIN
    n: VAR rational
    sub: THEOREM n-n = 0

    % (rewrite "sub") fails
    testsub: THEOREM false and 1/0 - 1/0 = 0

    % (rewrite "sub") succeeds
    testsub2: THEOREM true or 1/0 - 1/0 = 0

END sub

In the case of testsub, (rewrite "sub") fails, because a TCC is 
generated that presumably prevents instantiating sub with an ill-typed 
term. That makes sense to me.

In the case of testsub2 however, (rewrite "sub") does not generate a 
TCC, and sub seems to be used to rewrite 1/0 - 1/0 to 0.

First off, I am wondering why rewriting fails in the case of testsub and 
succeeds in the case of testsub2. The examples seem to be fairly equivalent.
Second, I am wondering how (rewrite "sub") solves (or avoids stating) 
the TCC in the case of testsub2. Is it the observation that you can 
assume the negation of the first disjunct when rewriting the second 
disjunct? Or is it something even more fancy?

I appreciate any explanation or pointer.
Thanks in advance,
Matthias