author | wenzelm |
Sun, 21 Oct 2007 16:27:42 +0200 | |
changeset 25135 | 4f8176c940cf |
parent 19741 | f65265d71426 |
child 35174 | e15040ae75d7 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOL/IOA/meta_theory/Asig.thy |
2 |
ID: $Id$ |
|
12218 | 3 |
Author: Olaf Müller, Tobias Nipkow & Konrad Slind |
3071 | 4 |
*) |
5 |
||
17233 | 6 |
header {* Action signatures *} |
3071 | 7 |
|
17233 | 8 |
theory Asig |
9 |
imports Main |
|
10 |
begin |
|
3071 | 11 |
|
17233 | 12 |
types |
13 |
'a signature = "('a set * 'a set * 'a set)" |
|
3071 | 14 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
15 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
16 |
inputs :: "'action signature => 'action set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
17 |
asig_inputs_def: "inputs = fst" |
3071 | 18 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
19 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
20 |
outputs :: "'action signature => 'action set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
21 |
asig_outputs_def: "outputs = (fst o snd)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
22 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
23 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
24 |
internals :: "'action signature => 'action set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
25 |
asig_internals_def: "internals = (snd o snd)" |
3071 | 26 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
27 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
28 |
actions :: "'action signature => 'action set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
29 |
"actions(asig) = (inputs(asig) Un outputs(asig) Un internals(asig))" |
3071 | 30 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
31 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
32 |
externals :: "'action signature => 'action set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
33 |
"externals(asig) = (inputs(asig) Un outputs(asig))" |
3071 | 34 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
35 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
36 |
locals :: "'action signature => 'action set" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
37 |
"locals asig = ((internals asig) Un (outputs asig))" |
3071 | 38 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
39 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
40 |
is_asig :: "'action signature => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
41 |
"is_asig(triple) = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
42 |
((inputs(triple) Int outputs(triple) = {}) & |
17233 | 43 |
(outputs(triple) Int internals(triple) = {}) & |
3071 | 44 |
(inputs(triple) Int internals(triple) = {}))" |
45 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
46 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
47 |
mk_ext_asig :: "'action signature => 'action signature" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
48 |
"mk_ext_asig(triple) = (inputs(triple), outputs(triple), {})" |
3071 | 49 |
|
19741 | 50 |
|
51 |
lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def |
|
52 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
53 |
lemma asig_triple_proj: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
54 |
"(outputs (a,b,c) = b) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
55 |
(inputs (a,b,c) = a) & |
19741 | 56 |
(internals (a,b,c) = c)" |
57 |
apply (simp add: asig_projections) |
|
58 |
done |
|
59 |
||
60 |
lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)" |
|
61 |
apply (simp add: externals_def actions_def) |
|
62 |
done |
|
63 |
||
64 |
lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)" |
|
65 |
apply (simp add: externals_def actions_def) |
|
66 |
done |
|
67 |
||
68 |
lemma int_is_act: "[|a:internals S|] ==> a:actions S" |
|
69 |
apply (simp add: asig_internals_def actions_def) |
|
70 |
done |
|
71 |
||
72 |
lemma inp_is_act: "[|a:inputs S|] ==> a:actions S" |
|
73 |
apply (simp add: asig_inputs_def actions_def) |
|
74 |
done |
|
75 |
||
76 |
lemma out_is_act: "[|a:outputs S|] ==> a:actions S" |
|
77 |
apply (simp add: asig_outputs_def actions_def) |
|
78 |
done |
|
79 |
||
80 |
lemma ext_and_act: "(x: actions S & x : externals S) = (x: externals S)" |
|
81 |
apply (fast intro!: ext_is_act) |
|
82 |
done |
|
83 |
||
84 |
lemma not_ext_is_int: "[|is_asig S;x: actions S|] ==> (x~:externals S) = (x: internals S)" |
|
85 |
apply (simp add: actions_def is_asig_def externals_def) |
|
86 |
apply blast |
|
87 |
done |
|
88 |
||
89 |
lemma not_ext_is_int_or_not_act: "is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)" |
|
90 |
apply (simp add: actions_def is_asig_def externals_def) |
|
91 |
apply blast |
|
92 |
done |
|
93 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
94 |
lemma int_is_not_ext: |
19741 | 95 |
"[| is_asig (S); x:internals S |] ==> x~:externals S" |
96 |
apply (unfold externals_def actions_def is_asig_def) |
|
97 |
apply simp |
|
98 |
apply blast |
|
99 |
done |
|
100 |
||
3071 | 101 |
|
17233 | 102 |
end |