src/HOL/HOLCF/IOA/meta_theory/Asig.thy
author huffman
Sat Nov 27 16:08:10 2010 -0800 (2010-11-27)
changeset 40774 0437dbc127b3
parent 35174 src/HOLCF/IOA/meta_theory/Asig.thy@e15040ae75d7
child 40945 b8703f63bfb2
permissions -rw-r--r--
moved directory src/HOLCF to src/HOL/HOLCF;
added HOLCF theories to src/HOL/IsaMakefile;
     1 (*  Title:      HOL/IOA/meta_theory/Asig.thy
     2     Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
     3 *)
     4 
     5 header {* Action signatures *}
     6 
     7 theory Asig
     8 imports Main
     9 begin
    10 
    11 types
    12   'a signature = "('a set * 'a set * 'a set)"
    13 
    14 definition
    15   inputs :: "'action signature => 'action set" where
    16   asig_inputs_def: "inputs = fst"
    17 
    18 definition
    19   outputs :: "'action signature => 'action set" where
    20   asig_outputs_def: "outputs = (fst o snd)"
    21 
    22 definition
    23   internals :: "'action signature => 'action set" where
    24   asig_internals_def: "internals = (snd o snd)"
    25 
    26 definition
    27   actions :: "'action signature => 'action set" where
    28   "actions(asig) = (inputs(asig) Un outputs(asig) Un internals(asig))"
    29 
    30 definition
    31   externals :: "'action signature => 'action set" where
    32   "externals(asig) = (inputs(asig) Un outputs(asig))"
    33 
    34 definition
    35   locals :: "'action signature => 'action set" where
    36   "locals asig = ((internals asig) Un (outputs asig))"
    37 
    38 definition
    39   is_asig :: "'action signature => bool" where
    40   "is_asig(triple) =
    41      ((inputs(triple) Int outputs(triple) = {}) &
    42       (outputs(triple) Int internals(triple) = {}) &
    43       (inputs(triple) Int internals(triple) = {}))"
    44 
    45 definition
    46   mk_ext_asig :: "'action signature => 'action signature" where
    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 asig_triple_proj:
    53  "(outputs    (a,b,c) = b)   &
    54   (inputs     (a,b,c) = a) &
    55   (internals  (a,b,c) = c)"
    56   apply (simp add: asig_projections)
    57   done
    58 
    59 lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
    60 apply (simp add: externals_def actions_def)
    61 done
    62 
    63 lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
    64 apply (simp add: externals_def actions_def)
    65 done
    66 
    67 lemma int_is_act: "[|a:internals S|] ==> a:actions S"
    68 apply (simp add: asig_internals_def actions_def)
    69 done
    70 
    71 lemma inp_is_act: "[|a:inputs S|] ==> a:actions S"
    72 apply (simp add: asig_inputs_def actions_def)
    73 done
    74 
    75 lemma out_is_act: "[|a:outputs S|] ==> a:actions S"
    76 apply (simp add: asig_outputs_def actions_def)
    77 done
    78 
    79 lemma ext_and_act: "(x: actions S & x : externals S) = (x: externals S)"
    80 apply (fast intro!: ext_is_act)
    81 done
    82 
    83 lemma not_ext_is_int: "[|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)"
    84 apply (simp add: actions_def is_asig_def externals_def)
    85 apply blast
    86 done
    87 
    88 lemma not_ext_is_int_or_not_act: "is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)"
    89 apply (simp add: actions_def is_asig_def externals_def)
    90 apply blast
    91 done
    92 
    93 lemma int_is_not_ext:
    94  "[| is_asig (S); x:internals S |] ==> x~:externals S"
    95 apply (unfold externals_def actions_def is_asig_def)
    96 apply simp
    97 apply blast
    98 done
    99 
   100 
   101 end