src/HOL/IOA/Asig.thy
author wenzelm
Mon Jan 11 21:21:02 2016 +0100 (2016-01-11)
changeset 62145 5b946c81dfbf
parent 58889 5b7a9633cfa8
child 63167 0909deb8059b
permissions -rw-r--r--
eliminated old defs;
oheimb@4530
     1
(*  Title:      HOL/IOA/Asig.thy
mueller@3078
     2
    Author:     Tobias Nipkow & Konrad Slind
mueller@3078
     3
    Copyright   1994  TU Muenchen
mueller@3078
     4
*)
mueller@3078
     5
wenzelm@58889
     6
section {* Action signatures *}
mueller@3078
     7
wenzelm@17288
     8
theory Asig
wenzelm@17288
     9
imports Main
wenzelm@17288
    10
begin
mueller@3078
    11
wenzelm@62145
    12
type_synonym 'a signature = "('a set * 'a set * 'a set)"
wenzelm@62145
    13
wenzelm@62145
    14
definition "inputs" :: "'action signature => 'action set"
wenzelm@62145
    15
  where asig_inputs_def: "inputs == fst"
mueller@3078
    16
wenzelm@62145
    17
definition "outputs" :: "'action signature => 'action set"
wenzelm@62145
    18
  where asig_outputs_def: "outputs == (fst o snd)"
wenzelm@17288
    19
wenzelm@62145
    20
definition "internals" :: "'action signature => 'action set"
wenzelm@62145
    21
  where asig_internals_def: "internals == (snd o snd)"
mueller@3078
    22
wenzelm@62145
    23
definition "actions" :: "'action signature => 'action set"
wenzelm@62145
    24
  where actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
mueller@3078
    25
wenzelm@62145
    26
definition externals :: "'action signature => 'action set"
wenzelm@62145
    27
  where externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))"
mueller@3078
    28
wenzelm@62145
    29
definition is_asig :: "'action signature => bool"
wenzelm@62145
    30
  where "is_asig(triple) ==
wenzelm@62145
    31
    ((inputs(triple) Int outputs(triple) = {})    &
wenzelm@62145
    32
     (outputs(triple) Int internals(triple) = {}) &
wenzelm@62145
    33
     (inputs(triple) Int internals(triple) = {}))"
mueller@3078
    34
wenzelm@62145
    35
definition mk_ext_asig :: "'action signature => 'action signature"
wenzelm@62145
    36
  where "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
mueller@3078
    37
wenzelm@19801
    38
wenzelm@19801
    39
lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
wenzelm@19801
    40
wenzelm@19801
    41
lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
wenzelm@19801
    42
  apply (simp add: externals_def actions_def)
wenzelm@19801
    43
  done
wenzelm@19801
    44
wenzelm@19801
    45
lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
wenzelm@19801
    46
  apply (simp add: externals_def actions_def)
wenzelm@19801
    47
  done
mueller@3078
    48
wenzelm@17288
    49
end