src/HOL/IOA/Asig.thy
author wenzelm
Tue Sep 06 19:03:39 2005 +0200 (2005-09-06)
changeset 17288 aa3833fb7bee
parent 11482 ec2c382ff4f0
child 19801 b2af2549efd1
permissions -rw-r--r--
converted to Isar theory format;
oheimb@4530
     1
(*  Title:      HOL/IOA/Asig.thy
mueller@3078
     2
    ID:         $Id$
mueller@3078
     3
    Author:     Tobias Nipkow & Konrad Slind
mueller@3078
     4
    Copyright   1994  TU Muenchen
mueller@3078
     5
*)
mueller@3078
     6
wenzelm@17288
     7
header {* Action signatures *}
mueller@3078
     8
wenzelm@17288
     9
theory Asig
wenzelm@17288
    10
imports Main
wenzelm@17288
    11
begin
mueller@3078
    12
wenzelm@17288
    13
types
wenzelm@17288
    14
  'a signature = "('a set * 'a set * 'a set)"
mueller@3078
    15
mueller@3078
    16
consts
wenzelm@17288
    17
  "actions" :: "'action signature => 'action set"
wenzelm@17288
    18
  "inputs" :: "'action signature => 'action set"
wenzelm@17288
    19
  "outputs" :: "'action signature => 'action set"
wenzelm@17288
    20
  "internals" :: "'action signature => 'action set"
wenzelm@17288
    21
  externals :: "'action signature => 'action set"
wenzelm@17288
    22
mueller@3078
    23
  is_asig       ::"'action signature => bool"
mueller@3078
    24
  mk_ext_asig   ::"'action signature => 'action signature"
mueller@3078
    25
mueller@3078
    26
mueller@3078
    27
defs
mueller@3078
    28
wenzelm@17288
    29
asig_inputs_def:    "inputs == fst"
wenzelm@17288
    30
asig_outputs_def:   "outputs == (fst o snd)"
wenzelm@17288
    31
asig_internals_def: "internals == (snd o snd)"
mueller@3078
    32
wenzelm@17288
    33
actions_def:
mueller@3078
    34
   "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
mueller@3078
    35
wenzelm@17288
    36
externals_def:
mueller@3078
    37
   "externals(asig) == (inputs(asig) Un outputs(asig))"
mueller@3078
    38
wenzelm@17288
    39
is_asig_def:
wenzelm@17288
    40
  "is_asig(triple) ==
wenzelm@17288
    41
      ((inputs(triple) Int outputs(triple) = {})    &
wenzelm@17288
    42
       (outputs(triple) Int internals(triple) = {}) &
mueller@3078
    43
       (inputs(triple) Int internals(triple) = {}))"
mueller@3078
    44
mueller@3078
    45
wenzelm@17288
    46
mk_ext_asig_def:
mueller@3078
    47
  "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
mueller@3078
    48
wenzelm@17288
    49
ML {* use_legacy_bindings (the_context ()) *}
mueller@3078
    50
wenzelm@17288
    51
end