1 (* Title: HOL/HOLCF/IOA/meta_theory/Asig.thy |
|
2 Author: Olaf Müller, Tobias Nipkow & Konrad Slind |
|
3 *) |
|
4 |
|
5 section \<open>Action signatures\<close> |
|
6 |
|
7 theory Asig |
|
8 imports Main |
|
9 begin |
|
10 |
|
11 type_synonym |
|
12 'a signature = "('a set * 'a set * 'a set)" |
|
13 |
|
14 definition |
|
15 inputs :: "'action signature => 'action set" where |
|
16 asig_inputs_def: "inputs = fst" |
|
17 |
|
18 definition |
|
19 outputs :: "'action signature => 'action set" where |
|
20 asig_outputs_def: "outputs = (fst o snd)" |
|
21 |
|
22 definition |
|
23 internals :: "'action signature => 'action set" where |
|
24 asig_internals_def: "internals = (snd o snd)" |
|
25 |
|
26 definition |
|
27 actions :: "'action signature => 'action set" where |
|
28 "actions(asig) = (inputs(asig) Un outputs(asig) Un internals(asig))" |
|
29 |
|
30 definition |
|
31 externals :: "'action signature => 'action set" where |
|
32 "externals(asig) = (inputs(asig) Un outputs(asig))" |
|
33 |
|
34 definition |
|
35 locals :: "'action signature => 'action set" where |
|
36 "locals asig = ((internals asig) Un (outputs asig))" |
|
37 |
|
38 definition |
|
39 is_asig :: "'action signature => bool" where |
|
40 "is_asig(triple) = |
|
41 ((inputs(triple) Int outputs(triple) = {}) & |
|
42 (outputs(triple) Int internals(triple) = {}) & |
|
43 (inputs(triple) Int internals(triple) = {}))" |
|
44 |
|
45 definition |
|
46 mk_ext_asig :: "'action signature => 'action signature" where |
|
47 "mk_ext_asig(triple) = (inputs(triple), outputs(triple), {})" |
|
48 |
|
49 |
|
50 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def |
|
51 |
|
52 lemma asig_triple_proj: |
|
53 "(outputs (a,b,c) = b) & |
|
54 (inputs (a,b,c) = a) & |
|
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 |
|
93 lemma int_is_not_ext: |
|
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 |
|
100 |
|
101 end |
|