src/HOL/IOA/Asig.thy
author haftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 58410 6d46ad54a2ab
parent 42174 d0be2722ce9f
child 58889 5b7a9633cfa8
permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
     1 (*  Title:      HOL/IOA/Asig.thy
     2     Author:     Tobias Nipkow & Konrad Slind
     3     Copyright   1994  TU Muenchen
     4 *)
     5 
     6 header {* Action signatures *}
     7 
     8 theory Asig
     9 imports Main
    10 begin
    11 
    12 type_synonym
    13   'a signature = "('a set * 'a set * 'a set)"
    14 
    15 consts
    16   "actions" :: "'action signature => 'action set"
    17   "inputs" :: "'action signature => 'action set"
    18   "outputs" :: "'action signature => 'action set"
    19   "internals" :: "'action signature => 'action set"
    20   externals :: "'action signature => 'action set"
    21 
    22   is_asig       ::"'action signature => bool"
    23   mk_ext_asig   ::"'action signature => 'action signature"
    24 
    25 
    26 defs
    27 
    28 asig_inputs_def:    "inputs == fst"
    29 asig_outputs_def:   "outputs == (fst o snd)"
    30 asig_internals_def: "internals == (snd o snd)"
    31 
    32 actions_def:
    33    "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    34 
    35 externals_def:
    36    "externals(asig) == (inputs(asig) Un outputs(asig))"
    37 
    38 is_asig_def:
    39   "is_asig(triple) ==
    40       ((inputs(triple) Int outputs(triple) = {})    &
    41        (outputs(triple) Int internals(triple) = {}) &
    42        (inputs(triple) Int internals(triple) = {}))"
    43 
    44 
    45 mk_ext_asig_def:
    46   "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    47 
    48 
    49 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
    50 
    51 lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
    52   apply (simp add: externals_def actions_def)
    53   done
    54 
    55 lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
    56   apply (simp add: externals_def actions_def)
    57   done
    58 
    59 end