Quelle  utp_var.thy

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 _{+L y} s = (get s, get 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 ― ‹ Identifiers ›
  "_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" ― ‹ Helper function for summing a list of identifiers ›

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 ― ‹ Decorations ›
  "_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 ― ‹ Variable sets ›
  "_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 ― ‹ Quotations ›
  "_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
  ― ‹ Identifiers ›
  "_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"

  ― ‹ Decorations ›
  "_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"

  ― ‹ Alphabets ›
  "_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"

  ― ‹ Quotations ›
  "_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 ‹
 
 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);
  [(@{syntax_const "_uvar_ty"}, K uvar_ty_tr)] end
 ›
  
end