Asig = Option +
types
'a signature = "('a set * 'a set * 'a set)"
consts
actions,inputs,outputs,internals,externals
::"'action signature => 'action set"
is_asig ::"'action signature => bool"
mk_ext_asig ::"'action signature => 'action signature"
rules
asig_projections_def
"inputs = fst & outputs = (fst o snd) & internals = (snd o snd)"
actions_def
"actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
externals_def
"externals(asig) == (inputs(asig) Un outputs(asig))"
is_asig_def
"is_asig(triple) == \
\ ((inputs(triple) Int outputs(triple) = {}) & \
\ (outputs(triple) Int internals(triple) = {}) & \
\ (inputs(triple) Int internals(triple) = {}))"
mk_ext_asig_def
"mk_ext_asig(triple) == <inputs(triple), outputs(triple), {}>"
end