Goal of exercise
- Show the expressive power of PVS equality and higher order logic;
- Give a hint on how PVS kernel could be reduced by building quantification on equality;
- Learn more on importing theory instances.
Exercise
Define FORALL in terms of equality (=). The universal quantifier will be defined as a function of one argument of the form:
each(P: [T -> bool]): bool
= (P = ???)
Note that we cannot overload FORALL definition, and thus choose a different name, each, for lexical reasons: this is also clearer!
Then prove
each_forall: THEOREM
(FORALL (P: [T -> bool]):
each(P) = (FORALL (x: T): P(x)))
each_each: COROLLARY
each((LAMBDA (P: [T -> bool]):
each(P) = (FORALL (x: T): P(x))))
Step by step
- Create an each theory in a new ~login/pvs/forall/ directory (use Meta-x new-pvs-file command to create this new theory) and define each function as specified above in the each theory. What are the parameters of each theory?
- Introduce and prove above each_forall theorem;
- Try to introduce each_each corollary in each theory: is it possible? How can you circumvent the difficulty?
- Finally prove each_each corollary.
DO NOT IMMEDIATELY LOOK AT solutions
|