| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Circus/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 29.4.2026 mit Größe 1020 B |
|
Quelle Var.thySprache: Isabelle |
|||||||||||||||
|
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 varia 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 it 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 |
|
||||||||||||||
2026-06-09