IOA/meta_theory/Asig.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/IOA/meta_theory/Asig.thy	Wed Nov 02 11:50:09 1994 +0100
@@ -0,0 +1,36 @@
+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