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