| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Circus/ (Archive of formal Proofs 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.12 Sekunden (vorverarbeitet am 2026-07-02) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-07-27