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

[PVS-Help] elementary prove questions



Hello,

could you please help me with the following elementary (I hope!)  
questions:

1. I am looking at the theory:

try1: theory
begin
t:type
a:t
end try1

When I try to typecheck I get a tcc asking me to prove that t is non- 
empty. On the other hand looking at the examples in the wift-tutorial  
(e.g. the phonebook) I got the impression that a:t would be treated  
as a declaration of a member in t and that it would imply rather than  
require that t is non-empty.

2. I am looking at the theory

try2: Theory
Begin
   t: type
   c: axiom exists (x: t): true
   a: bool = (Forall (x: t): x/=x)
   b: Theorem not a
End try2

How can I prove the theorem? If I add a line d:t then I get (as in 1)  
a tcc which I can then prove using c. After that (grind) proves the  
theorem. But I was not able to use c directly without an explicit  
line saying d:t.

Thank you,
Vladimir.