author | wenzelm |
Thu, 15 Feb 2018 12:11:00 +0100 | |
changeset 67613 | ce654b0e6d69 |
parent 63549 | b0d31c7def86 |
permissions | -rw-r--r-- |
62008 | 1 |
(* Title: HOL/HOLCF/IOA/CompoExecs.thy |
40945 | 2 |
Author: Olaf Müller |
17233 | 3 |
*) |
3071 | 4 |
|
62002 | 5 |
section \<open>Compositionality on Execution level\<close> |
3071 | 6 |
|
17233 | 7 |
theory CompoExecs |
8 |
imports Traces |
|
9 |
begin |
|
3071 | 10 |
|
62116 | 11 |
definition ProjA2 :: "('a, 's \<times> 't) pairs \<rightarrow> ('a, 's) pairs" |
12 |
where "ProjA2 = Map (\<lambda>x. (fst x, fst (snd x)))" |
|
3071 | 13 |
|
62116 | 14 |
definition ProjA :: "('a, 's \<times> 't) execution \<Rightarrow> ('a, 's) execution" |
63549 | 15 |
where "ProjA ex = (fst (fst ex), ProjA2 \<cdot> (snd ex))" |
3521 | 16 |
|
62116 | 17 |
definition ProjB2 :: "('a, 's \<times> 't) pairs \<rightarrow> ('a, 't) pairs" |
18 |
where "ProjB2 = Map (\<lambda>x. (fst x, snd (snd x)))" |
|
3071 | 19 |
|
62116 | 20 |
definition ProjB :: "('a, 's \<times> 't) execution \<Rightarrow> ('a, 't) execution" |
63549 | 21 |
where "ProjB ex = (snd (fst ex), ProjB2 \<cdot> (snd ex))" |
3071 | 22 |
|
62116 | 23 |
definition Filter_ex2 :: "'a signature \<Rightarrow> ('a, 's) pairs \<rightarrow> ('a, 's) pairs" |
24 |
where "Filter_ex2 sig = Filter (\<lambda>x. fst x \<in> actions sig)" |
|
3071 | 25 |
|
62116 | 26 |
definition Filter_ex :: "'a signature \<Rightarrow> ('a, 's) execution \<Rightarrow> ('a, 's) execution" |
63549 | 27 |
where "Filter_ex sig ex = (fst ex, Filter_ex2 sig \<cdot> (snd ex))" |
3071 | 28 |
|
62116 | 29 |
definition stutter2 :: "'a signature \<Rightarrow> ('a, 's) pairs \<rightarrow> ('s \<Rightarrow> tr)" |
30 |
where "stutter2 sig = |
|
63549 | 31 |
(fix \<cdot> |
62116 | 32 |
(LAM h ex. |
33 |
(\<lambda>s. |
|
34 |
case ex of |
|
35 |
nil \<Rightarrow> TT |
|
36 |
| x ## xs \<Rightarrow> |
|
37 |
(flift1 |
|
38 |
(\<lambda>p. |
|
39 |
(If Def (fst p \<notin> actions sig) then Def (s = snd p) else TT) |
|
63549 | 40 |
andalso (h\<cdot>xs) (snd p)) \<cdot> x))))" |
3071 | 41 |
|
62116 | 42 |
definition stutter :: "'a signature \<Rightarrow> ('a, 's) execution \<Rightarrow> bool" |
63549 | 43 |
where "stutter sig ex \<longleftrightarrow> (stutter2 sig \<cdot> (snd ex)) (fst ex) \<noteq> FF" |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
44 |
|
62116 | 45 |
definition par_execs :: |
46 |
"('a, 's) execution_module \<Rightarrow> ('a, 't) execution_module \<Rightarrow> ('a, 's \<times> 't) execution_module" |
|
47 |
where "par_execs ExecsA ExecsB = |
|
48 |
(let |
|
49 |
exA = fst ExecsA; sigA = snd ExecsA; |
|
50 |
exB = fst ExecsB; sigB = snd ExecsB |
|
51 |
in |
|
52 |
({ex. Filter_ex sigA (ProjA ex) \<in> exA} \<inter> |
|
53 |
{ex. Filter_ex sigB (ProjB ex) \<in> exB} \<inter> |
|
54 |
{ex. stutter sigA (ProjA ex)} \<inter> |
|
55 |
{ex. stutter sigB (ProjB ex)} \<inter> |
|
56 |
{ex. Forall (\<lambda>x. fst x \<in> actions sigA \<union> actions sigB) (snd ex)}, |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
57 |
asig_comp sigA sigB))" |
19741 | 58 |
|
59 |
||
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
35174
diff
changeset
|
60 |
lemmas [simp del] = split_paired_All |
19741 | 61 |
|
62 |
||
62116 | 63 |
section \<open>Recursive equations of operators\<close> |
19741 | 64 |
|
62116 | 65 |
subsection \<open>\<open>ProjA2\<close>\<close> |
19741 | 66 |
|
63549 | 67 |
lemma ProjA2_UU: "ProjA2 \<cdot> UU = UU" |
62116 | 68 |
by (simp add: ProjA2_def) |
19741 | 69 |
|
63549 | 70 |
lemma ProjA2_nil: "ProjA2 \<cdot> nil = nil" |
62116 | 71 |
by (simp add: ProjA2_def) |
19741 | 72 |
|
63549 | 73 |
lemma ProjA2_cons: "ProjA2 \<cdot> ((a, t) \<leadsto> xs) = (a, fst t) \<leadsto> ProjA2 \<cdot> xs" |
62116 | 74 |
by (simp add: ProjA2_def) |
19741 | 75 |
|
76 |
||
62116 | 77 |
subsection \<open>\<open>ProjB2\<close>\<close> |
19741 | 78 |
|
63549 | 79 |
lemma ProjB2_UU: "ProjB2 \<cdot> UU = UU" |
62116 | 80 |
by (simp add: ProjB2_def) |
19741 | 81 |
|
63549 | 82 |
lemma ProjB2_nil: "ProjB2 \<cdot> nil = nil" |
62116 | 83 |
by (simp add: ProjB2_def) |
19741 | 84 |
|
63549 | 85 |
lemma ProjB2_cons: "ProjB2 \<cdot> ((a, t) \<leadsto> xs) = (a, snd t) \<leadsto> ProjB2 \<cdot> xs" |
62116 | 86 |
by (simp add: ProjB2_def) |
19741 | 87 |
|
88 |
||
62116 | 89 |
subsection \<open>\<open>Filter_ex2\<close>\<close> |
19741 | 90 |
|
63549 | 91 |
lemma Filter_ex2_UU: "Filter_ex2 sig \<cdot> UU = UU" |
62116 | 92 |
by (simp add: Filter_ex2_def) |
19741 | 93 |
|
63549 | 94 |
lemma Filter_ex2_nil: "Filter_ex2 sig \<cdot> nil = nil" |
62116 | 95 |
by (simp add: Filter_ex2_def) |
19741 | 96 |
|
62116 | 97 |
lemma Filter_ex2_cons: |
63549 | 98 |
"Filter_ex2 sig \<cdot> (at \<leadsto> xs) = |
62116 | 99 |
(if fst at \<in> actions sig |
63549 | 100 |
then at \<leadsto> (Filter_ex2 sig \<cdot> xs) |
101 |
else Filter_ex2 sig \<cdot> xs)" |
|
62116 | 102 |
by (simp add: Filter_ex2_def) |
19741 | 103 |
|
104 |
||
62116 | 105 |
subsection \<open>\<open>stutter2\<close>\<close> |
106 |
||
107 |
lemma stutter2_unfold: |
|
108 |
"stutter2 sig = |
|
109 |
(LAM ex. |
|
110 |
(\<lambda>s. |
|
111 |
case ex of |
|
112 |
nil \<Rightarrow> TT |
|
113 |
| x ## xs \<Rightarrow> |
|
114 |
(flift1 |
|
115 |
(\<lambda>p. |
|
116 |
(If Def (fst p \<notin> actions sig) then Def (s= snd p) else TT) |
|
63549 | 117 |
andalso (stutter2 sig\<cdot>xs) (snd p)) \<cdot> x)))" |
62116 | 118 |
apply (rule trans) |
119 |
apply (rule fix_eq2) |
|
120 |
apply (simp only: stutter2_def) |
|
121 |
apply (rule beta_cfun) |
|
122 |
apply (simp add: flift1_def) |
|
123 |
done |
|
19741 | 124 |
|
63549 | 125 |
lemma stutter2_UU: "(stutter2 sig \<cdot> UU) s = UU" |
62116 | 126 |
apply (subst stutter2_unfold) |
127 |
apply simp |
|
128 |
done |
|
19741 | 129 |
|
63549 | 130 |
lemma stutter2_nil: "(stutter2 sig \<cdot> nil) s = TT" |
62116 | 131 |
apply (subst stutter2_unfold) |
132 |
apply simp |
|
133 |
done |
|
19741 | 134 |
|
62116 | 135 |
lemma stutter2_cons: |
63549 | 136 |
"(stutter2 sig \<cdot> (at \<leadsto> xs)) s = |
62116 | 137 |
((if fst at \<notin> actions sig then Def (s = snd at) else TT) |
63549 | 138 |
andalso (stutter2 sig \<cdot> xs) (snd at))" |
62116 | 139 |
apply (rule trans) |
140 |
apply (subst stutter2_unfold) |
|
141 |
apply (simp add: Consq_def flift1_def If_and_if) |
|
142 |
apply simp |
|
143 |
done |
|
19741 | 144 |
|
145 |
declare stutter2_UU [simp] stutter2_nil [simp] stutter2_cons [simp] |
|
146 |
||
147 |
||
62116 | 148 |
subsection \<open>\<open>stutter\<close>\<close> |
19741 | 149 |
|
150 |
lemma stutter_UU: "stutter sig (s, UU)" |
|
62116 | 151 |
by (simp add: stutter_def) |
19741 | 152 |
|
153 |
lemma stutter_nil: "stutter sig (s, nil)" |
|
62116 | 154 |
by (simp add: stutter_def) |
19741 | 155 |
|
62116 | 156 |
lemma stutter_cons: |
157 |
"stutter sig (s, (a, t) \<leadsto> ex) \<longleftrightarrow> (a \<notin> actions sig \<longrightarrow> (s = t)) \<and> stutter sig (t, ex)" |
|
158 |
by (simp add: stutter_def) |
|
19741 | 159 |
|
160 |
declare stutter2_UU [simp del] stutter2_nil [simp del] stutter2_cons [simp del] |
|
161 |
||
162 |
lemmas compoex_simps = ProjA2_UU ProjA2_nil ProjA2_cons |
|
163 |
ProjB2_UU ProjB2_nil ProjB2_cons |
|
164 |
Filter_ex2_UU Filter_ex2_nil Filter_ex2_cons |
|
165 |
stutter_UU stutter_nil stutter_cons |
|
166 |
||
167 |
declare compoex_simps [simp] |
|
168 |
||
169 |
||
62116 | 170 |
section \<open>Compositionality on execution level\<close> |
19741 | 171 |
|
62116 | 172 |
lemma lemma_1_1a: |
173 |
\<comment> \<open>\<open>is_ex_fr\<close> propagates from \<open>A \<parallel> B\<close> to projections \<open>A\<close> and \<open>B\<close>\<close> |
|
174 |
"\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> |
|
63549 | 175 |
is_exec_frag A (fst s, Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> xs)) \<and> |
176 |
is_exec_frag B (snd s, Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> xs))" |
|
62195 | 177 |
apply (pair_induct xs simp: is_exec_frag_def) |
62116 | 178 |
text \<open>main case\<close> |
179 |
apply (auto simp add: trans_of_defs2) |
|
180 |
done |
|
19741 | 181 |
|
62116 | 182 |
lemma lemma_1_1b: |
183 |
\<comment> \<open>\<open>is_ex_fr (A \<parallel> B)\<close> implies stuttering on projections\<close> |
|
184 |
"\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> |
|
63549 | 185 |
stutter (asig_of A) (fst s, ProjA2 \<cdot> xs) \<and> |
186 |
stutter (asig_of B) (snd s, ProjB2 \<cdot> xs)" |
|
62195 | 187 |
apply (pair_induct xs simp: stutter_def is_exec_frag_def) |
62116 | 188 |
text \<open>main case\<close> |
189 |
apply (auto simp add: trans_of_defs2) |
|
190 |
done |
|
19741 | 191 |
|
62116 | 192 |
lemma lemma_1_1c: |
193 |
\<comment> \<open>Executions of \<open>A \<parallel> B\<close> have only \<open>A\<close>- or \<open>B\<close>-actions\<close> |
|
194 |
"\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs" |
|
62195 | 195 |
apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def) |
62116 | 196 |
text \<open>main case\<close> |
197 |
apply auto |
|
198 |
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par) |
|
199 |
done |
|
19741 | 200 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
201 |
lemma lemma_1_2: |
62116 | 202 |
\<comment> \<open>\<open>ex A\<close>, \<open>exB\<close>, stuttering and forall \<open>a \<in> A \<parallel> B\<close> implies \<open>ex (A \<parallel> B)\<close>\<close> |
203 |
"\<forall>s. |
|
63549 | 204 |
is_exec_frag A (fst s, Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> xs)) \<and> |
205 |
is_exec_frag B (snd s, Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> xs)) \<and> |
|
206 |
stutter (asig_of A) (fst s, ProjA2 \<cdot> xs) \<and> |
|
207 |
stutter (asig_of B) (snd s, ProjB2 \<cdot> xs) \<and> |
|
62116 | 208 |
Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs \<longrightarrow> |
209 |
is_exec_frag (A \<parallel> B) (s, xs)" |
|
62195 | 210 |
apply (pair_induct xs simp: Forall_def sforall_def is_exec_frag_def stutter_def) |
62116 | 211 |
apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par) |
212 |
done |
|
19741 | 213 |
|
62116 | 214 |
theorem compositionality_ex: |
215 |
"ex \<in> executions (A \<parallel> B) \<longleftrightarrow> |
|
67613 | 216 |
Filter_ex (asig_of A) (ProjA ex) \<in> executions A \<and> |
217 |
Filter_ex (asig_of B) (ProjB ex) \<in> executions B \<and> |
|
62116 | 218 |
stutter (asig_of A) (ProjA ex) \<and> |
219 |
stutter (asig_of B) (ProjB ex) \<and> |
|
220 |
Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd ex)" |
|
221 |
apply (simp add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par) |
|
62195 | 222 |
apply (pair ex) |
62116 | 223 |
apply (rule iffI) |
224 |
text \<open>\<open>\<Longrightarrow>\<close>\<close> |
|
225 |
apply (erule conjE)+ |
|
226 |
apply (simp add: lemma_1_1a lemma_1_1b lemma_1_1c) |
|
227 |
text \<open>\<open>\<Longleftarrow>\<close>\<close> |
|
228 |
apply (erule conjE)+ |
|
229 |
apply (simp add: lemma_1_2) |
|
230 |
done |
|
19741 | 231 |
|
62116 | 232 |
theorem compositionality_ex_modules: "Execs (A \<parallel> B) = par_execs (Execs A) (Execs B)" |
233 |
apply (unfold Execs_def par_execs_def) |
|
234 |
apply (simp add: asig_of_par) |
|
235 |
apply (rule set_eqI) |
|
236 |
apply (simp add: compositionality_ex actions_of_par) |
|
237 |
done |
|
17233 | 238 |
|
239 |
end |