author | wenzelm |
Mon, 11 Jan 2016 00:04:23 +0100 | |
changeset 62116 | bc178c0fe1a1 |
parent 62008 | cbedaddc9351 |
permissions | -rw-r--r-- |
62008 | 1 |
(* Title: HOL/HOLCF/IOA/Asig.thy |
40945 | 2 |
Author: Olaf Müller, Tobias Nipkow & Konrad Slind |
3071 | 3 |
*) |
4 |
||
62002 | 5 |
section \<open>Action signatures\<close> |
3071 | 6 |
|
17233 | 7 |
theory Asig |
8 |
imports Main |
|
9 |
begin |
|
3071 | 10 |
|
62116 | 11 |
type_synonym 'a signature = "'a set \<times> 'a set \<times> 'a set" |
3071 | 12 |
|
62116 | 13 |
definition inputs :: "'action signature \<Rightarrow> 'action set" |
14 |
where asig_inputs_def: "inputs = fst" |
|
3071 | 15 |
|
62116 | 16 |
definition outputs :: "'action signature \<Rightarrow> 'action set" |
17 |
where asig_outputs_def: "outputs = fst \<circ> snd" |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
18 |
|
62116 | 19 |
definition internals :: "'action signature \<Rightarrow> 'action set" |
20 |
where asig_internals_def: "internals = snd \<circ> snd" |
|
3071 | 21 |
|
62116 | 22 |
definition actions :: "'action signature \<Rightarrow> 'action set" |
23 |
where "actions asig = inputs asig \<union> outputs asig \<union> internals asig" |
|
3071 | 24 |
|
62116 | 25 |
definition externals :: "'action signature \<Rightarrow> 'action set" |
26 |
where "externals asig = inputs asig \<union> outputs asig" |
|
3071 | 27 |
|
62116 | 28 |
definition locals :: "'action signature \<Rightarrow> 'action set" |
29 |
where "locals asig = internals asig \<union> outputs asig" |
|
3071 | 30 |
|
62116 | 31 |
definition 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 = {}" |
|
3071 | 36 |
|
62116 | 37 |
definition mk_ext_asig :: "'action signature \<Rightarrow> 'action signature" |
38 |
where "mk_ext_asig triple = (inputs triple, outputs triple, {})" |
|
3071 | 39 |
|
19741 | 40 |
|
41 |
lemmas asig_projections = asig_inputs_def asig_outputs_def asig_internals_def |
|
42 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
43 |
lemma asig_triple_proj: |
62116 | 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) |
|
19741 | 48 |
|
62116 | 49 |
lemma 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) |
|
19741 | 51 |
|
62116 | 52 |
lemma ext_is_act: "a \<in> externals S \<Longrightarrow> a \<in> actions S" |
53 |
by (simp add: externals_def actions_def) |
|
19741 | 54 |
|
62116 | 55 |
lemma int_is_act: "a \<in> internals S \<Longrightarrow> a \<in> actions S" |
56 |
by (simp add: asig_internals_def actions_def) |
|
19741 | 57 |
|
62116 | 58 |
lemma inp_is_act: "a \<in> inputs S \<Longrightarrow> a \<in> actions S" |
59 |
by (simp add: asig_inputs_def actions_def) |
|
19741 | 60 |
|
62116 | 61 |
lemma out_is_act: "a \<in> outputs S \<Longrightarrow> a \<in> actions S" |
62 |
by (simp add: asig_outputs_def actions_def) |
|
19741 | 63 |
|
62116 | 64 |
lemma ext_and_act: "x \<in> actions S \<and> x \<in> externals S \<longleftrightarrow> x \<in> externals S" |
65 |
by (fast intro!: ext_is_act) |
|
19741 | 66 |
|
62116 | 67 |
lemma 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) |
|
19741 | 69 |
|
62116 | 70 |
lemma 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) |
|
19741 | 72 |
|
62116 | 73 |
lemma 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) |
|
3071 | 75 |
|
17233 | 76 |
end |