1 (* Title: HOL/IOA/meta_theory/Asig.thy |
1 (* Title: HOL/IOA/meta_theory/Asig.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller, Tobias Nipkow & Konrad Slind |
3 Author: Olaf Müller, Tobias Nipkow & Konrad Slind |
4 |
|
5 Action signatures. |
|
6 *) |
4 *) |
7 |
5 |
8 Asig = Main + |
6 header {* Action signatures *} |
9 |
7 |
10 types |
8 theory Asig |
|
9 imports Main |
|
10 begin |
11 |
11 |
12 'a signature = "('a set * 'a set * 'a set)" |
12 types |
|
13 'a signature = "('a set * 'a set * 'a set)" |
13 |
14 |
14 consts |
15 consts |
15 actions,inputs,outputs,internals,externals,locals |
16 actions :: "'action signature => 'action set" |
16 ::"'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" |
|
21 locals :: "'action signature => 'action set" |
17 is_asig ::"'action signature => bool" |
22 is_asig ::"'action signature => bool" |
18 mk_ext_asig ::"'action signature => 'action signature" |
23 mk_ext_asig ::"'action signature => 'action signature" |
19 |
24 |
20 |
|
21 defs |
25 defs |
22 |
26 |
23 asig_inputs_def "inputs == fst" |
27 asig_inputs_def: "inputs == fst" |
24 asig_outputs_def "outputs == (fst o snd)" |
28 asig_outputs_def: "outputs == (fst o snd)" |
25 asig_internals_def "internals == (snd o snd)" |
29 asig_internals_def: "internals == (snd o snd)" |
26 |
30 |
27 actions_def |
31 actions_def: |
28 "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" |
32 "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" |
29 |
33 |
30 externals_def |
34 externals_def: |
31 "externals(asig) == (inputs(asig) Un outputs(asig))" |
35 "externals(asig) == (inputs(asig) Un outputs(asig))" |
32 |
36 |
33 locals_def |
37 locals_def: |
34 "locals asig == ((internals asig) Un (outputs asig))" |
38 "locals asig == ((internals asig) Un (outputs asig))" |
35 |
39 |
36 is_asig_def |
40 is_asig_def: |
37 "is_asig(triple) == |
41 "is_asig(triple) == |
38 ((inputs(triple) Int outputs(triple) = {}) & |
42 ((inputs(triple) Int outputs(triple) = {}) & |
39 (outputs(triple) Int internals(triple) = {}) & |
43 (outputs(triple) Int internals(triple) = {}) & |
40 (inputs(triple) Int internals(triple) = {}))" |
44 (inputs(triple) Int internals(triple) = {}))" |
41 |
45 |
42 |
46 |
43 mk_ext_asig_def |
47 mk_ext_asig_def: |
44 "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" |
48 "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" |
45 |
49 |
|
50 ML {* use_legacy_bindings (the_context ()) *} |
46 |
51 |
47 end |
52 end |