author | haftmann |
Sat, 16 May 2009 20:16:49 +0200 | |
changeset 31186 | b458b4ac570f |
parent 19801 | b2af2549efd1 |
child 36862 | 952b2b102a0a |
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 |
|
17288 | 7 |
header {* Action signatures *} |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
8 |
|
17288 | 9 |
theory Asig |
10 |
imports Main |
|
11 |
begin |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
12 |
|
17288 | 13 |
types |
14 |
'a signature = "('a set * 'a set * 'a set)" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
15 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
16 |
consts |
17288 | 17 |
"actions" :: "'action signature => 'action set" |
18 |
"inputs" :: "'action signature => 'action set" |
|
19 |
"outputs" :: "'action signature => 'action set" |
|
20 |
"internals" :: "'action signature => 'action set" |
|
21 |
externals :: "'action signature => 'action set" |
|
22 |
||
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
23 |
is_asig ::"'action signature => bool" |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
24 |
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
|
25 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
26 |
|
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
27 |
defs |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
28 |
|
17288 | 29 |
asig_inputs_def: "inputs == fst" |
30 |
asig_outputs_def: "outputs == (fst o snd)" |
|
31 |
asig_internals_def: "internals == (snd o snd)" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
32 |
|
17288 | 33 |
actions_def: |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
34 |
"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
|
35 |
|
17288 | 36 |
externals_def: |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
37 |
"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
|
38 |
|
17288 | 39 |
is_asig_def: |
40 |
"is_asig(triple) == |
|
41 |
((inputs(triple) Int outputs(triple) = {}) & |
|
42 |
(outputs(triple) Int internals(triple) = {}) & |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
43 |
(inputs(triple) Int internals(triple) = {}))" |
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 |
|
17288 | 46 |
mk_ext_asig_def: |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
47 |
"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
|
48 |
|
19801 | 49 |
|
50 |
lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def |
|
51 |
||
52 |
lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)" |
|
53 |
apply (simp add: externals_def actions_def) |
|
54 |
done |
|
55 |
||
56 |
lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)" |
|
57 |
apply (simp add: externals_def actions_def) |
|
58 |
done |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
59 |
|
17288 | 60 |
end |