Intent
------

To extent the expression language with a forall quantifier. 

Motivation
----------

The main motivation comes from our work on symmetry reduction. Here it
is necessary to be able to make symmetric expressions, in particular
in the queries. As an example take Fischer's protocol for mutual
exclusion. Here you want to express something like:

A[] forall (i: int[1,4]) forall (j: int[1,4]) P[i].cs && P[j].cs implies i == j

The syntax is identical to that of Murphi (and is similar to the new
iterator syntax in Java 5). Paul has previously asked for something
like this. One could also add an exist or forsome operator, but it is
easily expressed using forall and negation.


Syntax
------

Syntactically, we propose adding a keyword 'forall' and a production
like:

expr ::= 'forall' '(' <id> ':' <type> ')' <expr>


Here <type> must be an enumerable type (and in the first
implementation even restricted to integer types). For symmetry
reduction, this will be a scalarset, but scalarsets will be added
later.


Implementation
--------------

Besides the obvious update to the parser, we only need to change the
compiler. The evaluation can be done using the existing interpreter
and byte-code language. For the expression above, we need to compile
it to the equivalent of:

for (int i = 1; i <= 4; i++)
   for (int j = 1; j <= 4; j++)
     if (!(P[i].cs && P[j].cs implies i == j)
        return false;
return true;