Re: [PVS-Help] nonempty type tcc

[Sam Owre <owre@csl.sri.com>]

Hi Rob,

This is a bug, I added it to our bugs list.

You can work around it by using the lemma "PROC_nonempty" that is
generated in the proc theory (M-x prettyprint-expanded shows this).

Regards,
Sam Owre

robert <robert@itee.uq.edu.au> wrote:


> I've just changed to version 3.2 and a problem has cropped up.
> 
> I have a theory
> 
> proc: THEORY
> begin
>     PROC: TYPE+
> end proc
> 
> I import this theory via library, eg, 
> 
> sq_abstract: THEORY
> BEGIN
> 	
> 	lib: LIBRARY = "whatever"
> 
> 	importing lib@proc
> 
> 	.....
> 
> 	pp: PROC
> 
> 	.....
> end sq_abstract
> 
> The type checker generates the tcc 
> 
> % Existence TCC generated (at line 97, column 1) for  pp: PROC
>   % unfinished
> pp_TCC1: OBLIGATION EXISTS (x: PROC): TRUE;
> 
> This isn't proved when I use M-x prove-tccs-theory (ie, using (tcc)
> or (grind)).
> 
> I introduced a theorem identical to pp_TCC1 in theory proc and was able 
> to prove it straight away using (grind).
> 
> How can I prove the tcc obligation?
> 
> Thanks,
> Rob