Theory Var

section ‹UTP variables›

theory Var
imports Main
begin

text ‹UTP variables are characterized by two functions, $select$ and $update$. 
        The variable type is then defined as a tuple ($select$ * $update$).›

type_synonym ('a, 'r) var = "('r ⇒ 'a) * (('a ⇒ 'a) ⇒ 'r ⇒ 'r)"

text ‹The $lookup$ function returns the corrsponding $select$ function of a variable.›

definition lookup :: "('a, 'r) var ⇒ 'r ⇒ 'a"
  where "lookup f ≡ (fst f)"

text ‹The $assign$ function uses the $update$ function of a variable to update its value.›

definition assign :: "('a, 'r) var ⇒ 'a ⇒ 'r ⇒ 'r"
  where "assign f v ≡ (snd f) (λ _ . v)"

text ‹The $VAR$ function allows to retrieve a variable given its name.›

syntax "_VAR" :: "id ⇒ ('a, 'r) var"  (‹VAR _›)
translations "VAR x" => "(x, _update_name x)"

end