src/HOL/IOA/meta_theory/Asig.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/IOA/meta_theory/Asig.thy	Mon Mar 20 15:37:03 1995 +0100
@@ -0,0 +1,45 @@
+(*  Title:      HOL/IOA/meta_theory/Asig.thy
+    ID:         $Id$
+    Author:     Tobias Nipkow & Konrad Slind
+    Copyright   1994  TU Muenchen
+
+Action signatures
+*)
+
+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"
+
+
+defs
+
+asig_inputs_def    "inputs == fst"
+asig_outputs_def   "outputs == (fst o snd)"
+asig_internals_def "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