Metalogical Operators

The metalogic for Isabelle/UTP is simply HOL itself. This allows us to treat UTP expressions and predicates as objects, and manipulate and query them in various ways. UTP predicates do not contain explicit syntax and thus all meta-logic operators are semantic in nature.

Unrestriction and Usedby

In the section on variables, we saw how lens operators allow us to check the similarity of two variables, for example using lens independence $(x \bowtie y)$. We can check whether an expression e depends on a particular variable $x$ using unrestriction, which is written as $x \mathop{\sharp} P$. Unrestriction plays a similar role to "free variables", in that it allows us to determine if a variable is relevant for an expression’s evaluation.

Substitution

Alphabet Manipulation