7 |
7 |
8 theory Asig |
8 theory Asig |
9 imports Main |
9 imports Main |
10 begin |
10 begin |
11 |
11 |
12 type_synonym 'a signature = "('a set * 'a set * 'a set)" |
12 type_synonym 'a signature = "('a set \<times> 'a set \<times> 'a set)" |
13 |
13 |
14 definition "inputs" :: "'action signature => 'action set" |
14 definition "inputs" :: "'action signature \<Rightarrow> 'action set" |
15 where asig_inputs_def: "inputs == fst" |
15 where asig_inputs_def: "inputs \<equiv> fst" |
16 |
16 |
17 definition "outputs" :: "'action signature => 'action set" |
17 definition "outputs" :: "'action signature \<Rightarrow> 'action set" |
18 where asig_outputs_def: "outputs == (fst o snd)" |
18 where asig_outputs_def: "outputs \<equiv> (fst \<circ> snd)" |
19 |
19 |
20 definition "internals" :: "'action signature => 'action set" |
20 definition "internals" :: "'action signature \<Rightarrow> 'action set" |
21 where asig_internals_def: "internals == (snd o snd)" |
21 where asig_internals_def: "internals \<equiv> (snd \<circ> snd)" |
22 |
22 |
23 definition "actions" :: "'action signature => 'action set" |
23 definition "actions" :: "'action signature \<Rightarrow> 'action set" |
24 where actions_def: "actions(asig) == (inputs(asig) Un outputs(asig) Un internals(asig))" |
24 where actions_def: "actions(asig) \<equiv> (inputs(asig) \<union> outputs(asig) \<union> internals(asig))" |
25 |
25 |
26 definition externals :: "'action signature => 'action set" |
26 definition externals :: "'action signature \<Rightarrow> 'action set" |
27 where externals_def: "externals(asig) == (inputs(asig) Un outputs(asig))" |
27 where externals_def: "externals(asig) \<equiv> (inputs(asig) \<union> outputs(asig))" |
28 |
28 |
29 definition is_asig :: "'action signature => bool" |
29 definition is_asig :: "'action signature => bool" |
30 where "is_asig(triple) == |
30 where "is_asig(triple) \<equiv> |
31 ((inputs(triple) Int outputs(triple) = {}) & |
31 ((inputs(triple) \<inter> outputs(triple) = {}) \<and> |
32 (outputs(triple) Int internals(triple) = {}) & |
32 (outputs(triple) \<inter> internals(triple) = {}) \<and> |
33 (inputs(triple) Int internals(triple) = {}))" |
33 (inputs(triple) \<inter> internals(triple) = {}))" |
34 |
34 |
35 definition mk_ext_asig :: "'action signature => 'action signature" |
35 definition mk_ext_asig :: "'action signature \<Rightarrow> 'action signature" |
36 where "mk_ext_asig(triple) == (inputs(triple), outputs(triple), {})" |
36 where "mk_ext_asig(triple) \<equiv> (inputs(triple), outputs(triple), {})" |
37 |
37 |
38 |
38 |
39 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def |
39 lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def |
40 |
40 |
41 lemma int_and_ext_is_act: "[| a~:internals(S) ;a~:externals(S)|] ==> a~:actions(S)" |
41 lemma int_and_ext_is_act: "\<lbrakk>a\<notin>internals(S); a\<notin>externals(S)\<rbrakk> \<Longrightarrow> a\<notin>actions(S)" |
42 apply (simp add: externals_def actions_def) |
42 apply (simp add: externals_def actions_def) |
43 done |
43 done |
44 |
44 |
45 lemma ext_is_act: "[|a:externals(S)|] ==> a:actions(S)" |
45 lemma ext_is_act: "a\<in>externals(S) \<Longrightarrow> a\<in>actions(S)" |
46 apply (simp add: externals_def actions_def) |
46 apply (simp add: externals_def actions_def) |
47 done |
47 done |
48 |
48 |
49 end |
49 end |