src/HOL/IOA/Asig.thy
author haftmann
Sun Oct 08 22:28:22 2017 +0200 (23 months ago)
changeset 66816 212a3334e7da
parent 63167 0909deb8059b
child 67613 ce654b0e6d69
permissions -rw-r--r--
more fundamental definition of div and mod on int
     1 (*  Title:      HOL/IOA/Asig.thy
     2     Author:     Tobias Nipkow & Konrad Slind
     3     Copyright   1994  TU Muenchen
     4 *)
     5 
     6 section \<open>Action signatures\<close>
     7 
     8 theory Asig
     9 imports Main
    10 begin
    11 
    12 type_synonym 'a signature = "('a set * 'a set * 'a set)"
    13 
    14 definition "inputs" :: "'action signature => 'action set"
    15   where asig_inputs_def: "inputs == fst"
    16 
    17 definition "outputs" :: "'action signature => 'action set"
    18   where asig_outputs_def: "outputs == (fst o snd)"
    19 
    20 definition "internals" :: "'action signature => 'action set"
    21   where asig_internals_def: "internals == (snd o snd)"
    22 
    23 definition "actions" :: "'action signature => 'action set"
    24   where actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
    25 
    26 definition externals :: "'action signature => 'action set"
    27   where externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))"
    28 
    29 definition is_asig :: "'action signature => bool"
    30   where "is_asig(triple) ==
    31     ((inputs(triple) Int outputs(triple) = {})    &
    32      (outputs(triple) Int internals(triple) = {}) &
    33      (inputs(triple) Int internals(triple) = {}))"
    34 
    35 definition mk_ext_asig :: "'action signature => 'action signature"
    36   where "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
    37 
    38 
    39 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
    40 
    41 lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
    42   apply (simp add: externals_def actions_def)
    43   done
    44 
    45 lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
    46   apply (simp add: externals_def actions_def)
    47   done
    48 
    49 end