Theory utp_expr
section ‹ UTP Expressions ›
theory utp_expr
imports
utp_var
begin
subsection ‹ Expression type ›
purge_notation BNF_Def.convol (‹(‹indent=1 notation=‹mixfix convol››⟨_,/ _⟩)›)
text ‹ Before building the predicate model, we will build a model of expressions that generalise
alphabetised predicates. Expressions are represented semantically as mapping from
the alphabet @{typ "'α"} to the expression's type @{typ "'a"}. This general model will allow us to unify
all constructions under one type. The majority definitions in the file are given using
the \emph{lifting} package~\<^cite>‹"Huffman13"›, which allows us to reuse much of the existing
library of HOL functions. ›
typedef ('t, 'α) uexpr = "UNIV :: ('α ⇒ 't) set" ..
setup_lifting type_definition_uexpr
notation Rep_uexpr (‹⟦_⟧⇩e›)
notation Abs_uexpr (‹mk⇩e›)
lemma uexpr_eq_iff:
"e = f ⟷ (∀ b. ⟦e⟧⇩e b = ⟦f⟧⇩e b)"
using Rep_uexpr_inject[of e f, THEN sym] by (auto)
text ‹ The term @{term "⟦e⟧⇩e b"} effectively refers to the semantic interpretation of the expression
under the state-space valuation (or variables binding) @{term b}. It can be used, in concert
with the lifting package, to interpret UTP constructs to their HOL equivalents. We create some
theorem sets to store such transfer theorems. ›
named_theorems uexpr_defs and ueval and lit_simps and lit_norm
subsection ‹ Core expression constructs ›
text ‹ A variable expression corresponds to the lens $get$ function associated with a variable.
Specifically, given a lens the expression always returns that portion of the state-space
referred to by the lens. ›
lift_definition var :: "('t ⟹ 'α) ⇒ ('t, 'α) uexpr" is lens_get .
text ‹ A literal is simply a constant function expression, always returning the same value
for any binding. ›
lift_definition lit :: "'t ⇒ ('t, 'α) uexpr" (‹«_»›) is "λ v b. v" .
text ‹ We define lifting for unary, binary, ternary, and quaternary expression constructs, that
simply take a HOL function with correct number of arguments and apply it function to all possible
results of the expressions. ›
lift_definition uop :: "('a ⇒ 'b) ⇒ ('a, 'α) uexpr ⇒ ('b, 'α) uexpr"
is "λ f e b. f (e b)" .
lift_definition bop ::
"('a ⇒ 'b ⇒ 'c) ⇒ ('a, 'α) uexpr ⇒ ('b, 'α) uexpr ⇒ ('c, 'α) uexpr"
is "λ f u v b. f (u b) (v b)" .
lift_definition trop ::
"('a ⇒ 'b ⇒ 'c ⇒ 'd) ⇒ ('a, 'α) uexpr ⇒ ('b, 'α) uexpr ⇒ ('c, 'α) uexpr ⇒ ('d, 'α) uexpr"
is "λ f u v w b. f (u b) (v b) (w b)" .
lift_definition qtop ::
"('a ⇒ 'b ⇒ 'c ⇒ 'd ⇒ 'e) ⇒
('a, 'α) uexpr ⇒ ('b, 'α) uexpr ⇒ ('c, 'α) uexpr ⇒ ('d, 'α) uexpr ⇒
('e, 'α) uexpr"
is "λ f u v w x b. f (u b) (v b) (w b) (x b)" .
text ‹ We also define a UTP expression version of function ($\lambda$) abstraction, that takes
a function producing an expression and produces an expression producing a function. ›
lift_definition ulambda :: "('a ⇒ ('b, 'α) uexpr) ⇒ ('a ⇒ 'b, 'α) uexpr"
is "λ f A x. f x A" .
text ‹ We set up syntax for the conditional. This is effectively an infix version of
if-then-else where the condition is in the middle. ›
definition uIf :: "bool ⇒ 'a ⇒ 'a ⇒ 'a" where
[uexpr_defs]: "uIf = If"
abbreviation cond ::
"('a,'α) uexpr ⇒ (bool, 'α) uexpr ⇒ ('a,'α) uexpr ⇒ ('a,'α) uexpr"
(‹(3_ ◃ _ ▹/ _)› [52,0,53] 52)
where "P ◃ b ▹ Q ≡ trop uIf b P Q"
text ‹ UTP expression is equality is simply HOL equality lifted using the @{term bop} binary
expression constructor. ›
definition eq_upred :: "('a, 'α) uexpr ⇒ ('a, 'α) uexpr ⇒ (bool, 'α) uexpr" (infixl ‹=⇩u› 50)
where [uexpr_defs]: "eq_upred x y = bop HOL.eq x y"
text ‹ A literal is the expression @{term "«v»"}, where @{term v} is any HOL term. Actually, the
literal construct is very versatile and also allows us to refer to HOL variables within UTP
expressions, and has a variety of other uses. It can therefore also be considered as a kind
of quotation mechanism.
We also set up syntax for UTP variable expressions. ›
syntax
"_uuvar" :: "svar ⇒ logic" (‹_›)
syntax_consts
"_uuvar" == var
translations
"_uuvar x" == "CONST var x"
text ‹ Since we already have a parser for variables, we can directly reuse it and simply apply
the @{term var} expression construct to lift the resulting variable to an expression. ›
subsection ‹ Type class instantiations ›
text ‹ Isabelle/HOL of course provides a large hierarchy of type classes that provide constructs
such as numerals and the arithmetic operators. Fortunately we can directly make use of these
for UTP expressions, and thus we now perform a long list of appropriate instantiations. We
first lift the core arithemtic constants and operators using a mixture of literals, unary, and binary
expression constructors. ›
instantiation uexpr :: (zero, type) zero
begin
definition zero_uexpr_def [uexpr_defs]: "0 = lit 0"
instance ..
end
instantiation uexpr :: (one, type) one
begin
definition one_uexpr_def [uexpr_defs]: "1 = lit 1"
instance ..
end
instantiation uexpr :: (plus, type) plus
begin
definition plus_uexpr_def [uexpr_defs]: "u + v = bop (+) u v"
instance ..
end
instance uexpr :: (semigroup_add, type) semigroup_add
by (intro_classes) (simp add: plus_uexpr_def zero_uexpr_def, transfer, simp add: add.assoc)+
text ‹ The following instantiation sets up numerals. This will allow us to have Isabelle number
representations (i.e. 3,7,42,198 etc.) to UTP expressions directly. ›
instance uexpr :: (numeral, type) numeral
by (intro_classes, simp add: plus_uexpr_def, transfer, simp add: add.assoc)
text ‹ We can also define the order relation on expressions. Now, unlike the previous group and ring
constructs, the order relations @{term "(≤)"} and @{term "(≤)"} return a @{type bool} type.
This order is not therefore the lifted order which allows us to compare the valuation of two
expressions, but rather the order on expressions themselves. Notably, this instantiation will
later allow us to talk about predicate refinements and complete lattices. ›
instantiation uexpr :: (ord, type) ord
begin
lift_definition less_eq_uexpr :: "('a, 'b) uexpr ⇒ ('a, 'b) uexpr ⇒ bool"
is "λ P Q. (∀ A. P A ≤ Q A)" .
definition less_uexpr :: "('a, 'b) uexpr ⇒ ('a, 'b) uexpr ⇒ bool"
where [uexpr_defs]: "less_uexpr P Q = (P ≤ Q ∧ ¬ Q ≤ P)"
instance ..
end
text ‹ UTP expressions whose return type is a partial ordered type, are also partially ordered
as the following instantiation demonstrates. ›
instance uexpr :: (order, type) order
proof
fix x y z :: "('a, 'b) uexpr"
show "(x < y) = (x ≤ y ∧ ¬ y ≤ x)" by (simp add: less_uexpr_def)
show "x ≤ x" by (transfer, auto)
show "x ≤ y ⟹ y ≤ z ⟹ x ≤ z"
by (transfer, blast intro:order.trans)
show "x ≤ y ⟹ y ≤ x ⟹ x = y"
by (transfer, rule ext, simp add: eq_iff)
qed
subsection ‹ Syntax translations ›
text ‹ The follows a large number of translations that lift HOL functions to UTP expressions
using the various expression constructors defined above. Much of the time we try to keep
the HOL syntax but add a "u" subscript. ›
text ‹ This operator allows us to get the characteristic set of a type. Essentially this is
@{term "UNIV"}, but it retains the type syntactically for pretty printing. ›
definition set_of :: "'a itself ⇒ 'a set" where
[uexpr_defs]: "set_of t = UNIV"
text ‹ We add new non-terminals for UTP tuples and maplets. ›
nonterminal utuple_args and umaplet and umaplets
syntax
"_ucoerce" :: "logic ⇒ type ⇒ logic" (infix ‹:⇩u› 50)
"_ulambda" :: "pttrn ⇒ logic ⇒ logic" (‹λ _ ∙ _› [0, 10] 10)
"_ulens_ovrd" :: "logic ⇒ logic ⇒ salpha ⇒ logic" (‹_ ⊕ _ on _› [85, 0, 86] 86)
"_ulens_get" :: "logic ⇒ svar ⇒ logic" (‹_:_› [900,901] 901)
"_umem" :: "('a, 'α) uexpr ⇒ ('a set, 'α) uexpr ⇒ (bool, 'α) uexpr" (infix ‹∈⇩u› 50)
translations
"λ x ∙ p" == "CONST ulambda (λ x. p)"
"x :⇩u 'a" == "x :: ('a, _) uexpr"
"_ulens_ovrd f g a" => "CONST bop (CONST lens_override a) f g"
"_ulens_ovrd f g a" <= "CONST bop (λx y. CONST lens_override x1 y1 a) f g"
"_ulens_get x y" == "CONST uop (CONST lens_get y) x"
"x ∈⇩u A" == "CONST bop (∈) x A"
syntax
"_utuple" :: "('a, 'α) uexpr ⇒ utuple_args ⇒ ('a * 'b, 'α) uexpr" (‹(1'(_,/ _')⇩u)›)
"_utuple_arg" :: "('a, 'α) uexpr ⇒ utuple_args" (‹_›)
"_utuple_args" :: "('a, 'α) uexpr => utuple_args ⇒ utuple_args" (‹_,/ _›)
"_uunit" :: "('a, 'α) uexpr" (‹'(')⇩u›)
"_ufst" :: "('a × 'b, 'α) uexpr ⇒ ('a, 'α) uexpr" (‹π⇩1'(_')›)
"_usnd" :: "('a × 'b, 'α) uexpr ⇒ ('b, 'α) uexpr" (‹π⇩2'(_')›)
translations
"()⇩u" == "«()»"
"(x, y)⇩u" == "CONST bop (CONST Pair) x y"
"_utuple x (_utuple_args y z)" == "_utuple x (_utuple_arg (_utuple y z))"
"π⇩1(x)" == "CONST uop CONST fst x"
"π⇩2(x)" == "CONST uop CONST snd x"
syntax
"_uless" :: "logic ⇒ logic ⇒ logic" (infix ‹<⇩u› 50)
"_uleq" :: "logic ⇒ logic ⇒ logic" (infix ‹≤⇩u› 50)
"_ugreat" :: "logic ⇒ logic ⇒ logic" (infix ‹>⇩u› 50)
"_ugeq" :: "logic ⇒ logic ⇒ logic" (infix ‹≥⇩u› 50)
translations
"x <⇩u y" == "CONST bop (<) x y"
"x ≤⇩u y" == "CONST bop (≤) x y"
"x >⇩u y" => "y <⇩u x"
"x ≥⇩u y" => "y ≤⇩u x"
subsection ‹ Evaluation laws for expressions ›
text ‹ The following laws show how to evaluate the core expressions constructs in terms of which
the above definitions are defined. Thus, using these theorems together, we can convert any UTP
expression into a pure HOL expression. All these theorems are marked as \emph{ueval} theorems
which can be used for evaluation. ›
lemma lit_ueval [ueval]: "⟦«x»⟧⇩eb = x"
by (transfer, simp)
lemma var_ueval [ueval]: "⟦var x⟧⇩eb = get⇘x⇙ b"
by (transfer, simp)
lemma uop_ueval [ueval]: "⟦uop f x⟧⇩eb = f (⟦x⟧⇩eb)"
by (transfer, simp)
lemma bop_ueval [ueval]: "⟦bop f x y⟧⇩eb = f (⟦x⟧⇩eb) (⟦y⟧⇩eb)"
by (transfer, simp)
lemma trop_ueval [ueval]: "⟦trop f x y z⟧⇩eb = f (⟦x⟧⇩eb) (⟦y⟧⇩eb) (⟦z⟧⇩eb)"
by (transfer, simp)
lemma qtop_ueval [ueval]: "⟦qtop f x y z w⟧⇩eb = f (⟦x⟧⇩eb) (⟦y⟧⇩eb) (⟦z⟧⇩eb) (⟦w⟧⇩eb)"
by (transfer, simp)
subsection ‹ Misc laws ›
text ‹ We also prove a few useful algebraic and expansion laws for expressions. ›
lemma uop_const [simp]: "uop id u = u"
by (transfer, simp)
lemma bop_const_1 [simp]: "bop (λx y. y) u v = v"
by (transfer, simp)
lemma bop_const_2 [simp]: "bop (λx y. x) u v = u"
by (transfer, simp)
lemma uexpr_fst [simp]: "π⇩1((e, f)⇩u) = e"
by (transfer, simp)
lemma uexpr_snd [simp]: "π⇩2((e, f)⇩u) = f"
by (transfer, simp)
subsection ‹ Literalise tactics ›
text ‹ The following tactic converts literal HOL expressions to UTP expressions and vice-versa
via a collection of simplification rules. The two tactics are called "literalise", which
converts UTP to expressions to HOL expressions -- i.e. it pushes them into literals --
and unliteralise that reverses this. We collect the equations in a theorem attribute
called "lit\_simps". ›
lemma lit_fun_simps [lit_simps]:
"«i x y z u» = qtop i «x» «y» «z» «u»"
"«h x y z» = trop h «x» «y» «z»"
"«g x y» = bop g «x» «y»"
"«f x» = uop f «x»"
by (transfer, simp)+
text ‹ The following two theorems also set up interpretation of numerals, meaning a UTP numeral
can always be converted to a HOL numeral. ›
lemma numeral_uexpr_rep_eq [ueval]: "⟦numeral x⟧⇩e b = numeral x"
apply (induct x)
apply (simp add: lit.rep_eq one_uexpr_def)
apply (simp add: bop.rep_eq numeral_Bit0 plus_uexpr_def)
apply (simp add: bop.rep_eq lit.rep_eq numeral_code(3) one_uexpr_def plus_uexpr_def)
done
lemma numeral_uexpr_simp: "numeral x = «numeral x»"
by (simp add: uexpr_eq_iff numeral_uexpr_rep_eq lit.rep_eq)
lemma lit_zero [lit_simps]: "«0» = 0" by (simp add:uexpr_defs)
lemma lit_one [lit_simps]: "«1» = 1" by (simp add: uexpr_defs)
lemma lit_plus [lit_simps]: "«x + y» = «x» + «y»" by (simp add: uexpr_defs, transfer, simp)
lemma lit_numeral [lit_simps]: "«numeral n» = numeral n" by (simp add: numeral_uexpr_simp)
text ‹ In general unliteralising converts function applications to corresponding expression
liftings. Since some operators, like + and *, have specific operators we also have to
use @{thm uexpr_defs} in reverse to correctly interpret these. Moreover, numerals must be handled
separately by first simplifying them and then converting them into UTP expression numerals;
hence the following two simplification rules. ›
lemma lit_numeral_1: "uop numeral x = Abs_uexpr (λb. numeral (⟦x⟧⇩e b))"
by (simp add: uop_def)
lemma lit_numeral_2: "Abs_uexpr (λ b. numeral v) = numeral v"
by (metis lit.abs_eq lit_numeral)
method literalise = (unfold lit_simps[THEN sym])
method unliteralise = (unfold lit_simps uexpr_defs[THEN sym];
(unfold lit_numeral_1 ; (unfold uexpr_defs ueval); (unfold lit_numeral_2))?)+
text ‹ The following tactic can be used to evaluate literal expressions. It first literalises UTP
expressions, that is pushes as many operators into literals as possible. Then it tries to simplify,
and final unliteralises at the end. ›
method uexpr_simp uses simps = ((literalise)?, simp add: lit_norm simps, (unliteralise)?)
lemma "(1::(int, 'α) uexpr) + «2» = 4 ⟷ «3» = 4"
apply (literalise)
apply (uexpr_simp) oops
end