src/HOL/IOA/Asig.thy
author wenzelm
Mon Mar 22 20:58:52 2010 +0100 (2010-03-22)
changeset 35898 c890a3835d15
parent 19801 b2af2549efd1
child 36862 952b2b102a0a
permissions -rw-r--r--
recovered header;
     1 (*  Title:      HOL/IOA/Asig.thy
     2     ID:         $Id$
     3     Author:     Tobias Nipkow & Konrad Slind
     4     Copyright   1994  TU Muenchen
     5 *)
     6 
     7 header {* Action signatures *}
     8 
     9 theory Asig
    10 imports Main
    11 begin
    12 
    13 types
    14   'a signature = "('a set * 'a set * 'a set)"
    15 
    16 consts
    17   "actions" :: "'action signature => 'action set"
    18   "inputs" :: "'action signature => 'action set"
    19   "outputs" :: "'action signature => 'action set"
    20   "internals" :: "'action signature => 'action set"
    21   externals :: "'action signature => 'action set"
    22 
    23   is_asig       ::"'action signature => bool"
    24   mk_ext_asig   ::"'action signature => 'action signature"
    25 
    26 
    27 defs
    28 
    29 asig_inputs_def:    "inputs == fst"
    30 asig_outputs_def:   "outputs == (fst o snd)"
    31 asig_internals_def: "internals == (snd o snd)"
    32 
    33 actions_def:
    34    "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    35 
    36 externals_def:
    37    "externals(asig) == (inputs(asig) Un outputs(asig))"
    38 
    39 is_asig_def:
    40   "is_asig(triple) ==
    41       ((inputs(triple) Int outputs(triple) = {})    &
    42        (outputs(triple) Int internals(triple) = {}) &
    43        (inputs(triple) Int internals(triple) = {}))"
    44 
    45 
    46 mk_ext_asig_def:
    47   "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    48 
    49 
    50 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
    51 
    52 lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
    53   apply (simp add: externals_def actions_def)
    54   done
    55 
    56 lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
    57   apply (simp add: externals_def actions_def)
    58   done
    59 
    60 end