Theory utp_var
section ‹ UTP Variables ›
theory utp_var
imports
"UTP-Toolkit.utp_toolkit"
utp_parser_utils
begin
text ‹ In this first UTP theory we set up variables, which are are built on lenses~\<^cite>‹"Foster09" and "Foster16a"›.
A large part of this theory is setting up the parser for UTP variable syntax. ›
subsection ‹ Initial syntax setup ›
text ‹ We will overload the square order relation with refinement and also the lattice operators so
we will turn off these notations. ›
purge_notation
Order.le (infixl ‹⊑ı› 50) and
Lattice.sup (‹⨆ı_› [90] 90) and
Lattice.inf (‹⨅ı_› [90] 90) and
Lattice.join (infixl ‹⊔ı› 65) and
Lattice.meet (infixl ‹⊓ı› 70) and
Set.member (‹'(:')›) and
Set.member (‹(‹notation=‹infix :››_/ : _)› [51, 51] 50) and
disj (infixr ‹|› 30) and
conj (infixr ‹&› 35)
declare fst_vwb_lens [simp]
declare snd_vwb_lens [simp]
declare comp_vwb_lens [simp]
declare lens_indep_left_ext [simp]
declare lens_indep_right_ext [simp]
declare lens_comp_quotient [simp]
declare plus_lens_distr [THEN sym, simp]
subsection ‹ Variable foundations ›
text ‹ This theory describes the foundational structure of UTP variables, upon which the rest
of our model rests. We start by defining alphabets, which following~\<^cite>‹"Feliachi2010" and "Feliachi2012"›
in this shallow model are simply represented as types @{typ "'α"}, though by convention usually a record
type where each field corresponds to a variable. UTP variables in this frame are simply modelled
as lenses @{typ "'a ⟹ 'α"}, where the view type @{typ "'a"} is the variable type, and the
source type ‹'α› is the alphabet or state-space type.
We define some lifting functions for variables to create input and output variables.
These simply lift the alphabet to a tuple type since relations will ultimately be defined
by a tuple alphabet.
›
definition in_var :: "('a ⟹ 'α) ⇒ ('a ⟹ 'α × 'β)" where
[lens_defs]: "in_var x = x ;⇩L fst⇩L"
definition out_var :: "('a ⟹ 'β) ⇒ ('a ⟹ 'α × 'β)" where
[lens_defs]: "out_var x = x ;⇩L snd⇩L"
text ‹ Variables can also be used to effectively define sets of variables. Here we define the
the universal alphabet ($\Sigma$) to be the bijective lens @{term "1⇩L"}. This characterises
the whole of the source type, and thus is effectively the set of all alphabet variables. ›
abbreviation (input) univ_alpha :: "('α ⟹ 'α)" (‹Σ›) where
"univ_alpha ≡ 1⇩L"
text ‹ The next construct is vacuous and simply exists to help the parser distinguish predicate
variables from input and output variables. ›
definition pr_var :: "('a ⟹ 'β) ⇒ ('a ⟹ 'β)" where
[lens_defs]: "pr_var x = x"
subsection ‹ Variable lens properties ›
text ‹ We can now easily show that our UTP variable construction are various classes of
well-behaved lens .›
lemma in_var_weak_lens [simp]:
"weak_lens x ⟹ weak_lens (in_var x)"
by (simp add: comp_weak_lens in_var_def)
lemma in_var_semi_uvar [simp]:
"mwb_lens x ⟹ mwb_lens (in_var x)"
by (simp add: comp_mwb_lens in_var_def)
lemma pr_var_weak_lens [simp]:
"weak_lens x ⟹ weak_lens (pr_var x)"
by (simp add: pr_var_def)
lemma pr_var_mwb_lens [simp]:
"mwb_lens x ⟹ mwb_lens (pr_var x)"
by (simp add: pr_var_def)
lemma pr_var_vwb_lens [simp]:
"vwb_lens x ⟹ vwb_lens (pr_var x)"
by (simp add: pr_var_def)
lemma in_var_uvar [simp]:
"vwb_lens x ⟹ vwb_lens (in_var x)"
by (simp add: in_var_def)
lemma out_var_weak_lens [simp]:
"weak_lens x ⟹ weak_lens (out_var x)"
by (simp add: comp_weak_lens out_var_def)
lemma out_var_semi_uvar [simp]:
"mwb_lens x ⟹ mwb_lens (out_var x)"
by (simp add: comp_mwb_lens out_var_def)
lemma out_var_uvar [simp]:
"vwb_lens x ⟹ vwb_lens (out_var x)"
by (simp add: out_var_def)
text ‹ Moreover, we can show that input and output variables are independent, since they refer
to different sections of the alphabet. ›
lemma in_out_indep [simp]:
"in_var x ⨝ out_var y"
by (simp add: lens_indep_def in_var_def out_var_def fst_lens_def snd_lens_def lens_comp_def)
lemma out_in_indep [simp]:
"out_var x ⨝ in_var y"
by (simp add: lens_indep_def in_var_def out_var_def fst_lens_def snd_lens_def lens_comp_def)
lemma in_var_indep [simp]:
"x ⨝ y ⟹ in_var x ⨝ in_var y"
by (simp add: in_var_def out_var_def)
lemma out_var_indep [simp]:
"x ⨝ y ⟹ out_var x ⨝ out_var y"
by (simp add: out_var_def)
lemma pr_var_indeps [simp]:
"x ⨝ y ⟹ pr_var x ⨝ y"
"x ⨝ y ⟹ x ⨝ pr_var y"
by (simp_all add: pr_var_def)
lemma prod_lens_indep_in_var [simp]:
"a ⨝ x ⟹ a ×⇩L b ⨝ in_var x"
by (metis in_var_def in_var_indep out_in_indep out_var_def plus_pres_lens_indep prod_as_plus)
lemma prod_lens_indep_out_var [simp]:
"b ⨝ x ⟹ a ×⇩L b ⨝ out_var x"
by (metis in_out_indep in_var_def out_var_def out_var_indep plus_pres_lens_indep prod_as_plus)
lemma in_var_pr_var [simp]:
"in_var (pr_var x) = in_var x"
by (simp add: pr_var_def)
lemma out_var_pr_var [simp]:
"out_var (pr_var x) = out_var x"
by (simp add: pr_var_def)
lemma pr_var_idem [simp]:
"pr_var (pr_var x) = pr_var x"
by (simp add: pr_var_def)
lemma pr_var_lens_plus [simp]:
"pr_var (x +⇩L y) = (x +⇩L y)"
by (simp add: pr_var_def)
lemma pr_var_lens_comp_1 [simp]:
"pr_var x ;⇩L y = pr_var (x ;⇩L y)"
by (simp add: pr_var_def)
lemma in_var_plus [simp]: "in_var (x +⇩L y) = in_var x +⇩L in_var y"
by (simp add: in_var_def)
lemma out_var_plus [simp]: "out_var (x +⇩L y) = out_var x +⇩L out_var y"
by (simp add: out_var_def)
text ‹ Similar properties follow for sublens ›
lemma in_var_sublens [simp]:
"y ⊆⇩L x ⟹ in_var y ⊆⇩L in_var x"
by (metis (no_types, opaque_lifting) in_var_def lens_comp_assoc sublens_def)
lemma out_var_sublens [simp]:
"y ⊆⇩L x ⟹ out_var y ⊆⇩L out_var x"
by (metis (no_types, opaque_lifting) out_var_def lens_comp_assoc sublens_def)
lemma pr_var_sublens [simp]:
"y ⊆⇩L x ⟹ pr_var y ⊆⇩L pr_var x"
by (simp add: pr_var_def)
subsection ‹ Lens simplifications ›
text ‹ We also define some lookup abstraction simplifications. ›
lemma var_lookup_in [simp]: "lens_get (in_var x) (A, A') = lens_get x A"
by (simp add: in_var_def fst_lens_def lens_comp_def)
lemma var_lookup_out [simp]: "lens_get (out_var x) (A, A') = lens_get x A'"
by (simp add: out_var_def snd_lens_def lens_comp_def)
lemma var_update_in [simp]: "lens_put (in_var x) (A, A') v = (lens_put x A v, A')"
by (simp add: in_var_def fst_lens_def lens_comp_def)
lemma var_update_out [simp]: "lens_put (out_var x) (A, A') v = (A, lens_put x A' v)"
by (simp add: out_var_def snd_lens_def lens_comp_def)
lemma get_lens_plus [simp]: "get⇘x +⇩L y⇙ s = (get⇘x⇙ s, get⇘y⇙ s)"
by (simp add: lens_defs)
subsection ‹ Syntax translations ›
text ‹ In order to support nice syntax for variables, we here set up some translations. The first
step is to introduce a collection of non-terminals. ›
nonterminal svid and svids and svar and svars and salpha
text ‹ These non-terminals correspond to the following syntactic entities. Non-terminal
@{typ "svid"} is an atomic variable identifier, and @{typ "svids"} is a list of identifier.
@{typ "svar"} is a decorated variable, such as an input or output variable, and @{typ "svars"} is
a list of decorated variables. @{typ "salpha"} is an alphabet or set of variables. Such sets can
be constructed only through lens composition due to typing restrictions. Next we introduce some
syntax constructors. ›
syntax
"_svid" :: "id ⇒ svid" (‹_› [999] 999)
"_svid_unit" :: "svid ⇒ svids" (‹_›)
"_svid_list" :: "svid ⇒ svids ⇒ svids" (‹_,/ _›)
"_svid_alpha" :: "svid" (‹❙v›)
"_svid_dot" :: "svid ⇒ svid ⇒ svid" (‹_:_› [998,999] 998)
"_mk_svid_list" :: "svids ⇒ logic"
text ‹ A variable identifier can either be a HOL identifier, the complete set of variables in the
alphabet $\textbf{v}$, or a composite identifier separated by colons, which
corresponds to a sort of qualification. The final option is effectively a lens composition. ›
syntax
"_spvar" :: "svid ⇒ svar" (‹&_› [990] 990)
"_sinvar" :: "svid ⇒ svar" (‹$_› [990] 990)
"_soutvar" :: "svid ⇒ svar" (‹$_´› [990] 990)
text ‹ A variable can be decorated with an ampersand, to indicate it is a predicate variable, with
a dollar to indicate its an unprimed relational variable, or a dollar and ``acute'' symbol to
indicate its a primed relational variable. Isabelle's parser is extensible so additional
decorations can be and are added later. ›
syntax
"_salphaid" :: "svid ⇒ salpha" (‹_› [990] 990)
"_salphavar" :: "svar ⇒ salpha" (‹_› [990] 990)
"_salphaparen" :: "salpha ⇒ salpha" (‹'(_')›)
"_salphacomp" :: "salpha ⇒ salpha ⇒ salpha" (infixr ‹;› 75)
"_salphaprod" :: "salpha ⇒ salpha ⇒ salpha" (infixr ‹×› 85)
"_salpha_all" :: "salpha" (‹Σ›)
"_salpha_none" :: "salpha" (‹∅›)
"_svar_nil" :: "svar ⇒ svars" (‹_›)
"_svar_cons" :: "svar ⇒ svars ⇒ svars" (‹_,/ _›)
"_salphaset" :: "svars ⇒ salpha" (‹{_}›)
"_salphamk" :: "logic ⇒ salpha"
text ‹ The terminals of an alphabet are either HOL identifiers or UTP variable identifiers.
We support two ways of constructing alphabets; by composition of smaller alphabets using
a semi-colon or by a set-style construction $\{a,b,c\}$ with a list of UTP variables. ›
syntax
"_ualpha_set" :: "svars ⇒ logic" (‹{_}⇩α›)
"_svar" :: "svar ⇒ logic" (‹'(_')⇩v›)
text ‹ For various reasons, the syntax constructors above all yield specific grammar categories and
will not parser at the HOL top level (basically this is to do with us wanting to reuse the syntax
for expressions). As a result we provide some quotation constructors above.
Next we need to construct the syntax translations rules. First we need a few polymorphic constants. ›
consts
svar :: "'v ⇒ 'e"
ivar :: "'v ⇒ 'e"
ovar :: "'v ⇒ 'e"
adhoc_overloading
svar pr_var and ivar in_var and ovar out_var
text ‹ The functions above turn a representation of a variable (type @{typ "'v"}), including
its name and type, into some lens type @{typ "'e"}. @{term "svar"} constructs a predicate variable,
@{term "ivar"} and input variables, and @{term "ovar"} and output variable. The functions bridge
between the model and encoding of the variable and its interpretation as a lens in order to integrate it
into the general lens-based framework. Overriding these functions is then all we need to make
use of any kind of variables in terms of interfacing it with the system. Although in core UTP
variables are always modelled using record field, we can overload these constants to allow other
kinds of variables, such as deep variables with explicit syntax and type information.
Finally, we set up the translations rules. ›
translations
"_svid x" ⇀ "x"
"_svid_alpha" ⇌ "Σ"
"_svid_dot x y" ⇀ "y ;⇩L x"
"_mk_svid_list (_svid_unit x)" ⇀ "x"
"_mk_svid_list (_svid_list x xs)" ⇀ "x +⇩L _mk_svid_list xs"
"_spvar Σ" ↽ "CONST svar CONST id_lens"
"_sinvar Σ" ↽ "CONST ivar 1⇩L"
"_soutvar Σ" ↽ "CONST ovar 1⇩L"
"_spvar (_svid_dot x y)" ↽ "CONST svar (CONST lens_comp y x)"
"_sinvar (_svid_dot x y)" ↽ "CONST ivar (CONST lens_comp y x)"
"_soutvar (_svid_dot x y)" ↽ "CONST ovar (CONST lens_comp y x)"
"_svid_dot (_svid_dot x y) z" ↽ "_svid_dot (CONST lens_comp y x) z"
"_spvar x" ⇌ "CONST svar x"
"_sinvar x" ⇌ "CONST ivar x"
"_soutvar x" ⇌ "CONST ovar x"
"_salphaparen a" ⇀ "a"
"_salphaid x" ⇀ "x"
"_salphacomp x y" ⇀ "x +⇩L y"
"_salphaprod a b" ⇌ "a ×⇩L b"
"_salphavar x" ⇀ "x"
"_svar_nil x" ⇀ "x"
"_svar_cons x xs" ⇀ "x +⇩L xs"
"_salphaset A" ⇀ "A"
"(_svar_cons x (_salphamk y))" ↽ "_salphamk (x +⇩L y)"
"x" ↽ "_salphamk x"
"_salpha_all" ⇌ "1⇩L"
"_salpha_none" ⇌ "0⇩L"
"_ualpha_set A" ⇀ "A"
"_svar x" ⇀ "x"
text ‹ The translation rules mainly convert syntax into lens constructions, using a mixture
of lens operators and the bespoke variable definitions. Notably, a colon variable identifier
qualification becomes a lens composition, and variable sets are constructed using len sum.
The translation rules are carefully crafted to ensure both parsing and pretty printing.
Finally we create the following useful utility translation function that allows us to construct a
UTP variable (lens) type given a return and alphabet type. ›
syntax
"_uvar_ty" :: "type ⇒ type ⇒ type"
parse_translation ‹
let
fun uvar_ty_tr [ty] = Syntax.const @{type_syntax lens} $ ty $ Syntax.const @{type_syntax dummy}
| uvar_ty_tr ts = raise TERM ("uvar_ty_tr", ts);
in [(@{syntax_const "_uvar_ty"}, K uvar_ty_tr)] end
›
end