ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):

- recursive datatypes (e.g. the List datatype)
- operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
- special annotated operators like transitive closure (see below)

Axiomatically defined operators are not supported without additional annotations.

An example project with theories: media:theories2.zip

The project contains the following theories:

- SUMandPRODUCT
- Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value.

The operators are annotated such that ProB uses an extra implementation.

- Seq
- The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB.
- Real (unsupported)
- A theory of real numbers, currently unsupported by ProB.
- Natural
- A theory of inductive naturals (defined by a constant zero and a successor function).
- The mkinat operator is annotated such that ProB uses an explicit implementation.
- List
- A theory of lists that are either empty or have a head and a tail
- FixPoint (not really supported)
- The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them.
- closure
- The operator for transitive closure is supported by ProB.
- The operator is annotated such that ProB uses the classical B implementation.
- Card (contains no operators or data types)
- Contains theorem about set cardinalities.
- BoolOps
- Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB.
- BinaryTree
- Binary Trees are supported by ProB.

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Such tags are given in a .ptm file (**P**roB **T**heory **M**apping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form

operatorNameinternal {Tag}

where **Name** is the name of the operator in the theory and **Tag** is a ProB internal name.

Currently are the following tags supported (with T being an arbitrary type):

Tag | Description | Expected type | Return type |
---|---|---|---|

closure1 | the transitive closure | POW(T**T) | POW(T**T) |

SIGMA | the sum of a set | POW(T**INT) | INT |

PI | the product of a set | POW(T**INT) | INT |

mu | returns the element of a singleton set | POW(T) | T |

choose | returns (deterministically) one element of a non-emtpy set | POW(T) | T |

mkinat(zero,succ) | returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) | INT | Inductive Nat |

As of version 1.12 (mid-september 2022) ProB also transparently accepts `POW(INT)` as type for SIGMA and PI.
It now also accepts many of its external functions as tag names, such as the
the functions from LibraryStrings.def or LibraryReals.def.

In case the **.ptm** file is missing, you will get an error message such as the following one:

Axiomatic defined operator "SUM" not recognized.

For reference, here are the contents of some of the **.ptm** files.
In case of an error message, you can copy these files into your Theory Projects (e.g., using Drag & Drop) and then refresh (F5). After that animation with ProB should work.

- SUMandPRODUCT.ptm

operator "SUM" internal {SIGMA} operator "PRODUCT" internal {PI}

- closure.ptm

operator "cls" internal {closure1}

- Natural.ptm

operator "mk_iNAT" internal {mkinat}