src/HOL/IOA/Asig.thy
 author hoelzl Thu Sep 02 10:14:32 2010 +0200 (2010-09-02) changeset 39072 1030b1a166ef parent 36862 952b2b102a0a child 42174 d0be2722ce9f permissions -rw-r--r--
1 (*  Title:      HOL/IOA/Asig.thy
2     Author:     Tobias Nipkow & Konrad Slind
4 *)
6 header {* Action signatures *}
8 theory Asig
9 imports Main
10 begin
12 types
13   'a signature = "('a set * 'a set * 'a set)"
15 consts
16   "actions" :: "'action signature => 'action set"
17   "inputs" :: "'action signature => 'action set"
18   "outputs" :: "'action signature => 'action set"
19   "internals" :: "'action signature => 'action set"
20   externals :: "'action signature => 'action set"
22   is_asig       ::"'action signature => bool"
23   mk_ext_asig   ::"'action signature => 'action signature"
26 defs
28 asig_inputs_def:    "inputs == fst"
29 asig_outputs_def:   "outputs == (fst o snd)"
30 asig_internals_def: "internals == (snd o snd)"
32 actions_def:
33    "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))"
35 externals_def:
36    "externals(asig) == (inputs(asig) Un outputs(asig))"
38 is_asig_def:
39   "is_asig(triple) ==
40       ((inputs(triple) Int outputs(triple) = {})    &
41        (outputs(triple) Int internals(triple) = {}) &
42        (inputs(triple) Int internals(triple) = {}))"
45 mk_ext_asig_def:
46   "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
49 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
51 lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)"
52   apply (simp add: externals_def actions_def)
53   done
55 lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)"
56   apply (simp add: externals_def actions_def)
57   done
59 end