author | wenzelm |
Thu, 15 Feb 2018 12:11:00 +0100 | |
changeset 67613 | ce654b0e6d69 |
parent 63167 | 0909deb8059b |
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 |
Author: Tobias Nipkow & Konrad Slind |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
3 |
Copyright 1994 TU Muenchen |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
4 |
*) |
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
5 |
|
63167 | 6 |
section \<open>Action signatures\<close> |
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
7 |
|
17288 | 8 |
theory Asig |
9 |
imports Main |
|
10 |
begin |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
11 |
|
67613 | 12 |
type_synonym 'a signature = "('a set \<times> 'a set \<times> 'a set)" |
62145 | 13 |
|
67613 | 14 |
definition "inputs" :: "'action signature \<Rightarrow> 'action set" |
15 |
where asig_inputs_def: "inputs \<equiv> fst" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
16 |
|
67613 | 17 |
definition "outputs" :: "'action signature \<Rightarrow> 'action set" |
18 |
where asig_outputs_def: "outputs \<equiv> (fst \<circ> snd)" |
|
17288 | 19 |
|
67613 | 20 |
definition "internals" :: "'action signature \<Rightarrow> 'action set" |
21 |
where asig_internals_def: "internals \<equiv> (snd \<circ> snd)" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
22 |
|
67613 | 23 |
definition "actions" :: "'action signature \<Rightarrow> 'action set" |
24 |
where actions_def: "actions(asig) \<equiv> (inputs(asig) \<union> outputs(asig) \<union> internals(asig))" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
25 |
|
67613 | 26 |
definition externals :: "'action signature \<Rightarrow> 'action set" |
27 |
where externals_def: "externals(asig) \<equiv> (inputs(asig) \<union> outputs(asig))" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
28 |
|
62145 | 29 |
definition is_asig :: "'action signature => bool" |
67613 | 30 |
where "is_asig(triple) \<equiv> |
31 |
((inputs(triple) \<inter> outputs(triple) = {}) \<and> |
|
32 |
(outputs(triple) \<inter> internals(triple) = {}) \<and> |
|
33 |
(inputs(triple) \<inter> internals(triple) = {}))" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
34 |
|
67613 | 35 |
definition mk_ext_asig :: "'action signature \<Rightarrow> 'action signature" |
36 |
where "mk_ext_asig(triple) \<equiv> (inputs(triple), outputs(triple), {})" |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
37 |
|
19801 | 38 |
|
39 |
lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def |
|
40 |
||
67613 | 41 |
lemma int_and_ext_is_act: "\<lbrakk>a\<notin>internals(S); a\<notin>externals(S)\<rbrakk> \<Longrightarrow> a\<notin>actions(S)" |
19801 | 42 |
apply (simp add: externals_def actions_def) |
43 |
done |
|
44 |
||
67613 | 45 |
lemma ext_is_act: "a\<in>externals(S) \<Longrightarrow> a\<in>actions(S)" |
19801 | 46 |
apply (simp add: externals_def actions_def) |
47 |
done |
|
3078
984866a8f905
old IOA meta theory (see also new version in HOLCF/IOA/meta_theory);
mueller
parents:
diff
changeset
|
48 |
|
17288 | 49 |
end |