PVS‎ > ‎exercises‎ > ‎

### forall

 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