- Learn how to create a new theory from scratch;
- Get familiar with the "sets as predicates" important concept for typed higher order logics such as PVS;
- Learn from looking at PVS prelude (Meta-x view-prelude-file);
- Learn how to map your proof idea into a PVS proof scenario.
Step by step
- Start PVS (if necessary) under your ~login/pvs/intro/ context;
- Create a new theory named s123 using Meta-x new-pvs-file PVS command;
- Erase unuseful comments, and type requested definitions and lemmas, so as to obtain:
= n = 1 OR n = 2 OR n = 3 ;
= (LAMBDA (n: nat): n = 3 OR n = 1 OR n = 2)
Don't look at solution
- Try to type check the theory, using Meta-x tc PVS command; does it correctly type check?
- Try proving each lemma using Meta-x prove PVS command while the cursor is within the lemma.
Hint: proof of the first lemma requires using EXPAND command on each function you see, in order to apply the definition of the function, FLATTEN, SKOLEM and PROP commands; proof of the second lemma requires EXPAND (sometimes with the :IF-SIMPLIFIES T option), CASE (to use a lemma on the fly), and ASSERT.