1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Sat Nov 27 16:08:10 2010 -0800
     1.3 @@ -0,0 +1,101 @@
     1.4 +(*  Title:      HOL/IOA/meta_theory/Asig.thy
     1.5 +    Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
     1.6 +*)
     1.7 +
     1.8 +header {* Action signatures *}
     1.9 +
    1.10 +theory Asig
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +types
    1.15 +  'a signature = "('a set * 'a set * 'a set)"
    1.16 +
    1.17 +definition
    1.18 +  inputs :: "'action signature => 'action set" where
    1.19 +  asig_inputs_def: "inputs = fst"
    1.20 +
    1.21 +definition
    1.22 +  outputs :: "'action signature => 'action set" where
    1.23 +  asig_outputs_def: "outputs = (fst o snd)"
    1.24 +
    1.25 +definition
    1.26 +  internals :: "'action signature => 'action set" where
    1.27 +  asig_internals_def: "internals = (snd o snd)"
    1.28 +
    1.29 +definition
    1.30 +  actions :: "'action signature => 'action set" where
    1.31 +  "actions(asig) = (inputs(asig) Un outputs(asig) Un internals(asig))"
    1.32 +
    1.33 +definition
    1.34 +  externals :: "'action signature => 'action set" where
    1.35 +  "externals(asig) = (inputs(asig) Un outputs(asig))"
    1.36 +
    1.37 +definition
    1.38 +  locals :: "'action signature => 'action set" where
    1.39 +  "locals asig = ((internals asig) Un (outputs asig))"
    1.40 +
    1.41 +definition
    1.42 +  is_asig :: "'action signature => bool" where
    1.43 +  "is_asig(triple) =
    1.44 +     ((inputs(triple) Int outputs(triple) = {}) &
    1.45 +      (outputs(triple) Int internals(triple) = {}) &
    1.46 +      (inputs(triple) Int internals(triple) = {}))"
    1.47 +
    1.48 +definition
    1.49 +  mk_ext_asig :: "'action signature => 'action signature" where
    1.50 +  "mk_ext_asig(triple) = (inputs(triple), outputs(triple), {})"
    1.51 +
    1.52 +
    1.53 +lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
    1.54 +
    1.55 +lemma asig_triple_proj:
    1.56 + "(outputs    (a,b,c) = b)   &
    1.57 +  (inputs     (a,b,c) = a) &
    1.58 +  (internals  (a,b,c) = c)"
    1.59 +  apply (simp add: asig_projections)
    1.60 +  done
    1.61 +
    1.62 +lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
    1.63 +apply (simp add: externals_def actions_def)
    1.64 +done
    1.65 +
    1.66 +lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
    1.67 +apply (simp add: externals_def actions_def)
    1.68 +done
    1.69 +
    1.70 +lemma int_is_act: "[|a:internals S|] ==> a:actions S"
    1.71 +apply (simp add: asig_internals_def actions_def)
    1.72 +done
    1.73 +
    1.74 +lemma inp_is_act: "[|a:inputs S|] ==> a:actions S"
    1.75 +apply (simp add: asig_inputs_def actions_def)
    1.76 +done
    1.77 +
    1.78 +lemma out_is_act: "[|a:outputs S|] ==> a:actions S"
    1.79 +apply (simp add: asig_outputs_def actions_def)
    1.80 +done
    1.81 +
    1.82 +lemma ext_and_act: "(x: actions S & x : externals S) = (x: externals S)"
    1.83 +apply (fast intro!: ext_is_act)
    1.84 +done
    1.85 +
    1.86 +lemma not_ext_is_int: "[|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)"
    1.87 +apply (simp add: actions_def is_asig_def externals_def)
    1.88 +apply blast
    1.89 +done
    1.90 +
    1.91 +lemma not_ext_is_int_or_not_act: "is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)"
    1.92 +apply (simp add: actions_def is_asig_def externals_def)
    1.93 +apply blast
    1.94 +done
    1.95 +
    1.96 +lemma int_is_not_ext:
    1.97 + "[| is_asig (S); x:internals S |] ==> x~:externals S"
    1.98 +apply (unfold externals_def actions_def is_asig_def)
    1.99 +apply simp
   1.100 +apply blast
   1.101 +done
   1.102 +
   1.103 +
   1.104 +end