1(*  Title:      HOL/HOLCF/IOA/Asig.thy
2    Author:     Olaf M��ller, Tobias Nipkow & Konrad Slind
3*)
4
5section \<open>Action signatures\<close>
6
7theory Asig
8imports Main
9begin
10
11type_synonym 'a signature = "'a set \<times> 'a set \<times> 'a set"
12
13definition inputs :: "'action signature \<Rightarrow> 'action set"
14  where asig_inputs_def: "inputs = fst"
15
16definition outputs :: "'action signature \<Rightarrow> 'action set"
17  where asig_outputs_def: "outputs = fst \<circ> snd"
18
19definition internals :: "'action signature \<Rightarrow> 'action set"
20  where asig_internals_def: "internals = snd \<circ> snd"
21
22definition actions :: "'action signature \<Rightarrow> 'action set"
23  where "actions asig = inputs asig \<union> outputs asig \<union> internals asig"
24
25definition externals :: "'action signature \<Rightarrow> 'action set"
26  where "externals asig = inputs asig \<union> outputs asig"
27
28definition locals :: "'action signature \<Rightarrow> 'action set"
29  where "locals asig = internals asig \<union> outputs asig"
30
31definition is_asig :: "'action signature \<Rightarrow> bool"
32  where "is_asig triple \<longleftrightarrow>
33    inputs triple \<inter> outputs triple = {} \<and>
34    outputs triple \<inter> internals triple = {} \<and>
35    inputs triple \<inter> internals triple = {}"
36
37definition mk_ext_asig :: "'action signature \<Rightarrow> 'action signature"
38  where "mk_ext_asig triple = (inputs triple, outputs triple, {})"
39
40
41lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def
42
43lemma asig_triple_proj:
44  "outputs (a, b, c) = b \<and>
45   inputs (a, b, c) = a \<and>
46   internals (a, b, c) = c"
47  by (simp add: asig_projections)
48
49lemma int_and_ext_is_act: "a \<notin> internals S \<Longrightarrow> a \<notin> externals S \<Longrightarrow> a \<notin> actions S"
50  by (simp add: externals_def actions_def)
51
52lemma ext_is_act: "a \<in> externals S \<Longrightarrow> a \<in> actions S"
53  by (simp add: externals_def actions_def)
54
55lemma int_is_act: "a \<in> internals S \<Longrightarrow> a \<in> actions S"
56  by (simp add: asig_internals_def actions_def)
57
58lemma inp_is_act: "a \<in> inputs S \<Longrightarrow> a \<in> actions S"
59  by (simp add: asig_inputs_def actions_def)
60
61lemma out_is_act: "a \<in> outputs S \<Longrightarrow> a \<in> actions S"
62  by (simp add: asig_outputs_def actions_def)
63
64lemma ext_and_act: "x \<in> actions S \<and> x \<in> externals S \<longleftrightarrow> x \<in> externals S"
65  by (fast intro!: ext_is_act)
66
67lemma not_ext_is_int: "is_asig S \<Longrightarrow> x \<in> actions S \<Longrightarrow> x \<notin> externals S \<longleftrightarrow> x \<in> internals S"
68  by (auto simp add: actions_def is_asig_def externals_def)
69
70lemma not_ext_is_int_or_not_act: "is_asig S \<Longrightarrow> x \<notin> externals S \<longleftrightarrow> x \<in> internals S \<or> x \<notin> actions S"
71  by (auto simp add: actions_def is_asig_def externals_def)
72
73lemma int_is_not_ext:"is_asig S \<Longrightarrow> x \<in> internals S \<Longrightarrow> x \<notin> externals S"
74  by (auto simp add: externals_def actions_def is_asig_def)
75
76end
77