| author | paulson |
| Fri, 27 Sep 2002 10:35:10 +0200 | |
| changeset 13592 | dfe0c7191125 |
| parent 11482 | ec2c382ff4f0 |
| child 17288 | aa3833fb7bee |
| permissions | -rw-r--r-- |
| 4530 | 1 |
(* Title: HOL/IOA/Asig.thy |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
3 |
Author: Tobias Nipkow & Konrad Slind |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
4 |
Copyright 1994 TU Muenchen |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
5 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
6 |
Action signatures |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
7 |
*) |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
8 |
|
| 11482 | 9 |
Asig = Main + |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
10 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
11 |
types |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
12 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
13 |
'a signature = "('a set * 'a set * 'a set)"
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
14 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
15 |
consts |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
16 |
actions,inputs,outputs,internals,externals |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
17 |
::"'action signature => 'action set" |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
18 |
is_asig ::"'action signature => bool" |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
19 |
mk_ext_asig ::"'action signature => 'action signature" |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
20 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
21 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
22 |
defs |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
23 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
24 |
asig_inputs_def "inputs == fst" |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
25 |
asig_outputs_def "outputs == (fst o snd)" |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
26 |
asig_internals_def "internals == (snd o snd)" |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
27 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
28 |
actions_def |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
29 |
"actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
30 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
31 |
externals_def |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
32 |
"externals(asig) == (inputs(asig) Un outputs(asig))" |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
33 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
34 |
is_asig_def |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
35 |
"is_asig(triple) == |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
36 |
((inputs(triple) Int outputs(triple) = {}) &
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
37 |
(outputs(triple) Int internals(triple) = {}) &
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
38 |
(inputs(triple) Int internals(triple) = {}))"
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
39 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
40 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
41 |
mk_ext_asig_def |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
42 |
"mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})"
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
43 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
44 |
|
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
45 |
end |