src/HOL/IOA/Asig.thy
author mueller
Wed Apr 30 11:56:17 1997 +0200 (1997-04-30)
changeset 3078 984866a8f905
child 4530 ac1821645636
permissions -rw-r--r--
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
     1 (*  Title:      HOL/IOA/meta_theory/Asig.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     5 
     6 Action signatures
     7 *)
     8 
     9 Asig = Prod +
    10 
    11 types 
    12 
    13 'a signature = "('a set * 'a set * 'a set)"
    14 
    15 consts
    16   actions,inputs,outputs,internals,externals
    17                 ::"'action signature => 'action set"
    18   is_asig       ::"'action signature => bool"
    19   mk_ext_asig   ::"'action signature => 'action signature"
    20 
    21 
    22 defs
    23 
    24 asig_inputs_def    "inputs == fst"
    25 asig_outputs_def   "outputs == (fst o snd)"
    26 asig_internals_def "internals == (snd o snd)"
    27 
    28 actions_def
    29    "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    30 
    31 externals_def
    32    "externals(asig) == (inputs(asig) Un outputs(asig))"
    33 
    34 is_asig_def
    35   "is_asig(triple) ==            
    36       ((inputs(triple) Int outputs(triple) = {})    & 
    37        (outputs(triple) Int internals(triple) = {}) & 
    38        (inputs(triple) Int internals(triple) = {}))"
    39 
    40 
    41 mk_ext_asig_def
    42   "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    43 
    44 
    45 end