Re: Problem typechecking over conversions on patched version

[Christoph Berg <cb@cs.uni-sb.de>]

On Wed, Jun 06, 2001 at 02:20:43PM +0300, Tamarah Arons wrote:
>   NOT : [MY_PROP -> MY_PROP] =  (lambda prop : (lambda seq, i: not prop(seq, i)));
> 
> % NOT : [ASSERTION -> ASSERTION] =  (lambda a: lambda e : not a(e));
> 
>   OR : [MY_PROP, MY_PROP -> MY_PROP] =  
>         (lambda prop, prop2: (lambda seq, i: prop(seq, i) or prop2(seq, i)));
> 
>   OR : [ASSERTION, ASSERTION -> ASSERTION] = 
>            (lambda a, b : (lambda e : a(e) or b(e)));

The problem vanishes if you do not overload the basic NOT and OR
operators. If you change the above definitions to something like
'NOT_' and 'OR_', your file typechecks with PVS Version 2.3 (patch
level 1.2.2.36).

>   nonsense : lemma  
>       valid(a or not(a))

(Of course you have to change this to
  valid(OR_(a, NOT_(a)))
)

Christoph Berg
-- 
cb@cs.uni-sb.de, http://www-wjp.cs.uni-sb.de/~cb/
Office +49/681/302-4490, Fax -4290, Home +49/681/9657944
Computer Science Dept., Universität des Saarlandes, Saarbrücken

PGP signature