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
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@17288
     6
header {* Action signatures *}
mueller@3078
     7
wenzelm@17288
     8
theory Asig
wenzelm@17288
     9
imports Main
wenzelm@17288
    10
begin
mueller@3078
    11
wenzelm@42174
    12
type_synonym
wenzelm@17288
    13
  'a signature = "('a set * 'a set * 'a set)"
mueller@3078
    14
mueller@3078
    15
consts
wenzelm@17288
    16
  "actions" :: "'action signature => 'action set"
wenzelm@17288
    17
  "inputs" :: "'action signature => 'action set"
wenzelm@17288
    18
  "outputs" :: "'action signature => 'action set"
wenzelm@17288
    19
  "internals" :: "'action signature => 'action set"
wenzelm@17288
    20
  externals :: "'action signature => 'action set"
wenzelm@17288
    21
mueller@3078
    22
  is_asig       ::"'action signature => bool"
mueller@3078
    23
  mk_ext_asig   ::"'action signature => 'action signature"
mueller@3078
    24
mueller@3078
    25
mueller@3078
    26
defs
mueller@3078
    27
wenzelm@17288
    28
asig_inputs_def:    "inputs == fst"
wenzelm@17288
    29
asig_outputs_def:   "outputs == (fst o snd)"
wenzelm@17288
    30
asig_internals_def: "internals == (snd o snd)"
mueller@3078
    31
wenzelm@17288
    32
actions_def:
mueller@3078
    33
   "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
mueller@3078
    34
wenzelm@17288
    35
externals_def:
mueller@3078
    36
   "externals(asig) == (inputs(asig) Un outputs(asig))"
mueller@3078
    37
wenzelm@17288
    38
is_asig_def:
wenzelm@17288
    39
  "is_asig(triple) ==
wenzelm@17288
    40
      ((inputs(triple) Int outputs(triple) = {})    &
wenzelm@17288
    41
       (outputs(triple) Int internals(triple) = {}) &
mueller@3078
    42
       (inputs(triple) Int internals(triple) = {}))"
mueller@3078
    43
mueller@3078
    44
wenzelm@17288
    45
mk_ext_asig_def:
mueller@3078
    46
  "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
mueller@3078
    47
wenzelm@19801
    48
wenzelm@19801
    49
lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
wenzelm@19801
    50
wenzelm@19801
    51
lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
wenzelm@19801
    52
  apply (simp add: externals_def actions_def)
wenzelm@19801
    53
  done
wenzelm@19801
    54
wenzelm@19801
    55
lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
wenzelm@19801
    56
  apply (simp add: externals_def actions_def)
wenzelm@19801
    57
  done
mueller@3078
    58
wenzelm@17288
    59
end