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 \(\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. For example, consider a literal expression «v»
. It yields the same valuation regardless of the
state-space, and thus it is unrestricted by any variable: x \(\sharp\) «v»
is a theorem. On the other hand, it is not
the case that x \(\sharp\) &x
, since the valuation of this expression directly depends on the value of variable
x. Yet, it is the case that x \(\sharp\) &y
, provided that \(x \bowtie y\) – x and y are different areas of
the state space.
As we noted in the section on variables, lenses can also be used to collect multiple variables in
a set. Unrestriction additionally supports the notation {&x,&y,&z} \(\sharp\) P
which states that P does not refer
to any of the variables in the set. Internally the collect set becomes a summation of the corresponding lenses.
Unrestriction is not precisely the same as free variables, because it is a semantic rather than syntactic property. To
see this, consider that z \(\sharp\) \((z < 0 \wedge z \ge 0)\)
. This is because the expression is semantically
equivalent to true, no matter the valuation of z, and thus the expression does not depend on z.
The unrestriction operator distributes expression and predicate operators in an intuitive way, taking care to observe
variables bound by quantifiers and abstractions. For example, \(y \sharp (\exists x \bullet P)\) provided that \(x
\bowtie y\) – x and y are distinct – and \(y \sharp P\). The unrestriction laws for predicate calculus can be
viewed in the
repository. Proof
of unrestriction conjectures can be undertaken by the tactic unrest_tac
that applies all known unrestriction
introduction rules.
The dual operator of unrestriction is called “usedby”, and is written as x \(\natural\) P
. Rather than stating that P cannot
depend on x, it states that P may only depend upon x. Thus x is an upper bound on the possible variables P can
refer to it. It is useful in situations when we want to restrict a predicate to a particular set of variables. Like unrestriction
it also support the set-style notation {&x,&y,&z} \(\natural\) P
.
Substitution
We adopt a similar approach to that used by Back and Wright in their refinement
calculus (see Chapter 9 on Relations) and model
substitutions as functions on the state space: \(\sigma : \alpha \Rightarrow \alpha\). Intuitively, a substitution
describes how the values of variables in the state space should be updated upon its application. The simplest
substitution is the identity function id
which simply retains the present value for all variables. A substitution can
also be modified with the syntax \(\sigma(x \mapsto_s v)\)
, for lens \(x : \tau \Longrightarrow \alpha\)
and
expression \(v : (\tau, \alpha)\) uexpr
, which changes the value of x to expression v in the
substitution. Expression v can depend on previous values of x and any other variables in the state-space. For
convenience, we also have the notation \([x_1 \mapsto_s v_1, \cdots, x_n \mapsto_s v_n]\)
which constructs a
substitution from n maplets.
Substitutions can be applied to expressions using the dagger notation \(\sigma \,\dagger\, e\)
, which applies the
function to every possible state input of e. We also support the more traditional syntax for substitutions \(P [\!|
v / x |\!]\)
, which is equivalent to \([x \mapsto_s v] \dagger P\)
.
As for unrestriction, there are a large number of laws for distributing substitutions through various operators. A
sample of such laws for predicate calculus can be views in the
repository. Such
laws can be applied using the tactic subst_tac
.
Alphabet Manipulation
Alphabets in Isabelle/UTP are simply represented as state space types, as in \(\alpha\) upred
. Often it is convenient
to be able to add or remove variables from an alphabet in order to grow or shrink the state space. Enforcing a
particular alphabet is useful for ensuring that predicates are correct-by-construction, as the Isabelle type system is
employed to ensure this.
Since variables are not atomic syntactic entities, we cannot simply remove them from a set. Instead it is necessary to perform a semantic transformation on the state space type. Fortunately, it turns out that we can again employ lenses to formalise these transformations.
First, we have the alphabet extrusion operator \(P \oplus_p a\)
for P : \((\tau, \alpha)\) uexpr
and a :
\(\alpha \Longrightarrow \beta\)
. Lens a describes how state space \(\alpha\) can be losslessly embedded into a
“larger” state space \(\beta\). The result of applying the alphabet extrusion is therefore an expression of type
\((\tau, \beta)\) uexpr
– the state space has changed to become \(\beta\). The semantics of the expression is the
same, and any variables present in \(\beta\) but not in \(\alpha\) will be unrestricted.
Second, we have the alphabet restriction operator \(P \upharpoonleft_p a\)
for P : \((\tau, \beta)\) uexpr
and a :
\(\alpha \Longrightarrow \beta\)
. It is similar to extrusion, but throws away part of \(\beta\) to result in an
expression of type \((\tau, \alpha)\) uexpr
. Unlike extrusion it is therefore lossy in nature. Nevertheless, we do have
the intutive inverse law: \((P \oplus_p a) \upharpoonleft_p a = P\).
Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure