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
¤ Dauer der Verarbeitung: 0.1 Sekunden
¤
*© Formatika GbR, Deutschland
