syntax: (ws1s &optional (fnums *) (examples? t) (automaton? nil) (traces? nil) (verbose? t) (defs !) theories rewrites exclude)
effect: This strategy implements a decision procedure for the Weak Second-order monadic logic of 1 Successor (WS1S). The supported fragment of WS1S includes boolean expression, arithmetic on the natural numbers restricted to addition/subraction with/from a constant, and operations on finite sets over the naturals like union, intersection, set difference, addition and removal of a natural. Predicates include arithmetic comparisons like <, <=, >, >=, equality, disequality, the subset relation, and membership in the form P(i). There is quantification over the booleans, the natural numbers, finite sets of naturals, and predicate subtypes of the aforementioned types built from formulas in the set just described. Furthermore, natural numbers, and finite sets of natural numbers may also be described using the the operator; e.g. ripple-carry addition may be defined as:
+(P, Q: finite_set[nat]): finite_set[nat] =
the({R: finite_set[nat] |
EXISTS (C: finite_set[nat]): NOT(C(0)) AND
FORALL (t: nat):
(C(t + 1) = ((P(t) AND Q(t)) OR
(P(t) AND C(t)) OR
(Q(t) AND C(t))))
AND (R(t) = P(t) = Q(t) = C(t))});
Using this definition, lemmas such as
plus_assoc: LEMMA
FORALL (X, Y, Z: finite_set[nat]):
X + (Y + Z) = (X + Y) + Z
are proven to be valid by simply calling (WS1S).
In a first step, the WS1S strategy rewrites the formulas specifed by FNUMS. The resulting formulas are then translated, using the rule WS1S-SIMP, to an automaton which recognizes the language of their interpretations. Hereby, subformulas that do not appear to be in the WS1S fragment are abstracted away by introducing new parameters. If the final automaton recognizes the full set, the FNUMS formulas are replaced by TRUE; otherwise, these formulas are left unchanged.
The DEFS, THEORIES, REWRITES, and EXCLUDE arguments are used to install rewrites. For a precise description of their meaning see e.g. AUTO-REWRITE-THEORY or INSTALL-REWRITES.
In case where the formulae specified by FNUMS are neither valid nor unsatisfiable both a witness and a counterexample are displayed if the flag EXAMPLES? is set. Hereby, expressions are displayed for both the free variables in the FNUMS formulas and the newly introduced abstraction parameters. An alternative, trace-oriented view of the examples are displayed if the TRACES? flag is on.
With the AUTOMATON? flag turned on, the constructed automaton is displayed.
Translation messages are being displayed whenever the flag VERBOSE? is set to T. Messages like "Abstracting..." indicate the introduction of a new parameter, and "Not abstractable ..." indicates that there is a free occurrences of a bound variables in the current subformula. In this case, the translation process aborts. A second source of failure in the translation process comes from quantifiers which contain bindings not included in WS1S. In these cases, a message like "Not in ws1s: ... in ..." is displayed and the translation process aborts.
These messages may be helpful in detecting expressions that are not known to be in WS1S by the translator. In these cases, it might be useful to decorate these expressions with appropriate type coercions (e.g. {x: nat | x = 1 OR x = 2} :: finite_set[nat]) to support the translation process.
usage: (ws1s 1 :examples? nil :verbose?? nil) Tries to reduce formula 1 to true; suppresses both translation messages and the display of a witness and a counterexample in case this formula is neither valid nor satisfiable.
errors: "Formula ... not in WS1S"
The translation process could not construct a DFA for
the formula ...
notes: The WS1S strategy uses the libraries of Mona to construct DFAs. Mona was developed at BRICS - see http://www.brics.dk/~mona for details.