2 Capabilities

The Theory plug-in has the following capabilities:

Theory Definition:
1. Definition of datatypes: datatypes are defined by supplying the types on which they are polymorphic, a set of constructors one of which has to be a base constructor. Each constructor may or may not have destructors.
2. Definition of operators: operators can be defined as predicate or expression operators. An expression operator is an operator that "returns" an expression, an example existing operator is $card$ . A predicate operator is one that "returns" a predicate, an example existing predicate operator is $finite$ .
3. Definition of rewrite rules: rewrite rules are one-directional equalities that can be applied from left to right. The Theory plug-in can be used to define rewrite rules.
4. Definition of inference rules: inference rules can be used to infer new hypotheses, split a goal into sub-goals or discharge sequents.
5. Definition of polymorphic theorems: theorems can be defined and validated once, and can then be imported into sequents of proof obligations if a suitable type instantiation is available.
6. Validation of extensions: where appropriate, proof obligations are generated to ensure soundness of extensions. This includes, proof obligations for validity of inference and rewrite rules, as well as proof obligations to validate operator properties such as associativity and commutativity.
Theory Deployment: this step signifies that a theory is ready for use. Theories can be deployed after they have been optionally validated by the user. It is strongly advisable to discharge all proof obligations before deployment.

Once a theory has been deployed to its designated project, all its extensions (mathematical and prover extensions) can be used in models. In later sections, we show the two different scopes of theory availability.