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

Problem typechecking over conversions on patched version



Hello,

I have a file appended, that typechecks using *unpatched* PVS2-3 
but not using PVS2-3 with patch (problem in lemma ``nonsense''). 
If I add the commented definition

% NOT : [ASSERTION -> ASSERTION] =  (lambda a: lambda e : not a(e));

then it does typecheck with patched PVS2-3.

Why does it not typecheck with patched PVS2-3?
In this contrived example adding the ``NOT'' definition is obvious thing 
to do, but I have a lot of predicates defined over type MY_PROP 
(not shown in this dummy file) and would prefer not to have to redefine
them all for ASSERTIONS. Is there a way around this?

Thanks,
Tamarah
________________________________________________________________________

myops[STATE : NONEMPTY_TYPE]: THEORY

 BEGIN

  STATE_SEQ: TYPE = [nat -> STATE]
   
  ASSERTION : TYPE = [STATE -> boolean] 

  MY_PROP : TYPE = [STATE_SEQ, nat -> boolean]
 
  i : VAR nat
 
  e, f : VAR STATE

  seq : VAR STATE_SEQ

  a, b : VAR ASSERTION

  prop, prop2 : VAR MY_PROP

  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)));

  ASSERTION_to_PROP(a): MY_PROP = (LAMBDA seq, i: a(seq(i)))

  CONVERSION ASSERTION_to_PROP

  valid : [MY_PROP -> bool] =
     (lambda prop : forall seq, i : prop(seq, i))

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

 END myops