PVS‎ > ‎exercises‎ > ‎

{1, 2, 3}

Goal
  • 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:
s123: THEORY

  BEGIN

    s12?(n: nat): bool
      = n = 1  OR  n = 2  ;

    s123?(n: nat): bool
      = n = 1  OR  n = 2  OR  n = 3 ;

    s12_subset_of_s123: LEMMA
      subset?(s12?, s123?)

    s12_differs_from_s123: LEMMA
      s12? /= s123?

    s312?: [nat -> bool]
      = (LAMBDA (n: nat): n = 3  OR  n = 1  OR n = 2)

    s312_equals_s123: LEMMA
      s312? = s123?

  END s123
  • 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.
Don't look at solution

Comments