- Now imports Fun rather than Orderings
- Moved "Set as lattice" section behind "Fun as lattice" section, since
sets are just functions.
- The instantiations
instantiation set :: (type) distrib_lattice
instantiation set :: (type) complete_lattice
are no longer needed, and the former definitions inf_set_eq, sup_set_eq,
Inf_set_def, and Sup_set_def can now be derived from abstract properties
of sup, inf, etc.
header {* \chapter{The Rely-Guarantee Method}
\section {Abstract Syntax}
*}
theory RG_Com imports Main begin
text {* Semantics of assertions and boolean expressions (bexp) as sets
of states. Syntax of commands @{text com} and parallel commands
@{text par_com}. *}
types
'a bexp = "'a set"
datatype 'a com =
Basic "'a \<Rightarrow>'a"
| Seq "'a com" "'a com"
| Cond "'a bexp" "'a com" "'a com"
| While "'a bexp" "'a com"
| Await "'a bexp" "'a com"
types 'a par_com = "(('a com) option) list"
end