author | wenzelm |
Mon, 11 Jan 2016 00:04:23 +0100 | |
changeset 62116 | bc178c0fe1a1 |
parent 62008 | cbedaddc9351 |
child 62195 | 799a5306e2ed |
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" |
15 |
where "ProjA ex = (fst (fst ex), ProjA2 $ (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" |
21 |
where "ProjB ex = (snd (fst ex), ProjB2 $ (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" |
27 |
where "Filter_ex sig ex = (fst ex, Filter_ex2 sig $ (snd ex))" |
|
3071 | 28 |
|
62116 | 29 |
definition stutter2 :: "'a signature \<Rightarrow> ('a, 's) pairs \<rightarrow> ('s \<Rightarrow> tr)" |
30 |
where "stutter2 sig = |
|
31 |
(fix $ |
|
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) |
|
40 |
andalso (h$xs) (snd p)) $ x))))" |
|
3071 | 41 |
|
62116 | 42 |
definition stutter :: "'a signature \<Rightarrow> ('a, 's) execution \<Rightarrow> bool" |
43 |
where "stutter sig ex \<longleftrightarrow> (stutter2 sig $ (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 |
|
62116 | 67 |
lemma ProjA2_UU: "ProjA2 $ UU = UU" |
68 |
by (simp add: ProjA2_def) |
|
19741 | 69 |
|
62116 | 70 |
lemma ProjA2_nil: "ProjA2 $ nil = nil" |
71 |
by (simp add: ProjA2_def) |
|
19741 | 72 |
|
62116 | 73 |
lemma ProjA2_cons: "ProjA2 $ ((a, t) \<leadsto> xs) = (a, fst t) \<leadsto> ProjA2 $ xs" |
74 |
by (simp add: ProjA2_def) |
|
19741 | 75 |
|
76 |
||
62116 | 77 |
subsection \<open>\<open>ProjB2\<close>\<close> |
19741 | 78 |
|
62116 | 79 |
lemma ProjB2_UU: "ProjB2 $ UU = UU" |
80 |
by (simp add: ProjB2_def) |
|
19741 | 81 |
|
62116 | 82 |
lemma ProjB2_nil: "ProjB2 $ nil = nil" |
83 |
by (simp add: ProjB2_def) |
|
19741 | 84 |
|
62116 | 85 |
lemma ProjB2_cons: "ProjB2 $ ((a, t) \<leadsto> xs) = (a, snd t) \<leadsto> ProjB2 $ xs" |
86 |
by (simp add: ProjB2_def) |
|
19741 | 87 |
|
88 |
||
62116 | 89 |
subsection \<open>\<open>Filter_ex2\<close>\<close> |
19741 | 90 |
|
62116 | 91 |
lemma Filter_ex2_UU: "Filter_ex2 sig $ UU = UU" |
92 |
by (simp add: Filter_ex2_def) |
|
19741 | 93 |
|
62116 | 94 |
lemma Filter_ex2_nil: "Filter_ex2 sig $ nil = nil" |
95 |
by (simp add: Filter_ex2_def) |
|
19741 | 96 |
|
62116 | 97 |
lemma Filter_ex2_cons: |
98 |
"Filter_ex2 sig $ (at \<leadsto> xs) = |
|
99 |
(if fst at \<in> actions sig |
|
100 |
then at \<leadsto> (Filter_ex2 sig $ xs) |
|
101 |
else Filter_ex2 sig $ xs)" |
|
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) |
|
117 |
andalso (stutter2 sig$xs) (snd p)) $ x)))" |
|
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 |
|
62116 | 125 |
lemma stutter2_UU: "(stutter2 sig $ UU) s = UU" |
126 |
apply (subst stutter2_unfold) |
|
127 |
apply simp |
|
128 |
done |
|
19741 | 129 |
|
62116 | 130 |
lemma stutter2_nil: "(stutter2 sig $ nil) s = TT" |
131 |
apply (subst stutter2_unfold) |
|
132 |
apply simp |
|
133 |
done |
|
19741 | 134 |
|
62116 | 135 |
lemma stutter2_cons: |
136 |
"(stutter2 sig $ (at \<leadsto> xs)) s = |
|
137 |
((if fst at \<notin> actions sig then Def (s = snd at) else TT) |
|
138 |
andalso (stutter2 sig $ xs) (snd at))" |
|
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> |
|
175 |
is_exec_frag A (fst s, Filter_ex2 (asig_of A) $ (ProjA2 $ xs)) \<and> |
|
176 |
is_exec_frag B (snd s, Filter_ex2 (asig_of B) $ (ProjB2 $ xs))" |
|
177 |
apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>) |
|
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> |
|
185 |
stutter (asig_of A) (fst s, ProjA2 $ xs) \<and> |
|
186 |
stutter (asig_of B) (snd s, ProjB2 $ xs)" |
|
187 |
apply (tactic \<open>pair_induct_tac @{context} "xs" @{thms stutter_def is_exec_frag_def} 1\<close>) |
|
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" |
|
195 |
apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def}, |
|
196 |
@{thm is_exec_frag_def}] 1\<close>) |
|
197 |
text \<open>main case\<close> |
|
198 |
apply auto |
|
199 |
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par) |
|
200 |
done |
|
19741 | 201 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
202 |
lemma lemma_1_2: |
62116 | 203 |
\<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> |
204 |
"\<forall>s. |
|
205 |
is_exec_frag A (fst s, Filter_ex2 (asig_of A) $ (ProjA2 $ xs)) \<and> |
|
206 |
is_exec_frag B (snd s, Filter_ex2 (asig_of B) $ (ProjB2 $ xs)) \<and> |
|
207 |
stutter (asig_of A) (fst s, ProjA2 $ xs) \<and> |
|
208 |
stutter (asig_of B) (snd s, ProjB2 $ xs) \<and> |
|
209 |
Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) xs \<longrightarrow> |
|
210 |
is_exec_frag (A \<parallel> B) (s, xs)" |
|
211 |
apply (tactic \<open>pair_induct_tac @{context} "xs" |
|
212 |
@{thms Forall_def sforall_def is_exec_frag_def stutter_def} 1\<close>) |
|
213 |
apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par) |
|
214 |
done |
|
19741 | 215 |
|
62116 | 216 |
theorem compositionality_ex: |
217 |
"ex \<in> executions (A \<parallel> B) \<longleftrightarrow> |
|
218 |
Filter_ex (asig_of A) (ProjA ex) : executions A \<and> |
|
219 |
Filter_ex (asig_of B) (ProjB ex) : executions B \<and> |
|
220 |
stutter (asig_of A) (ProjA ex) \<and> |
|
221 |
stutter (asig_of B) (ProjB ex) \<and> |
|
222 |
Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd ex)" |
|
223 |
apply (simp add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par) |
|
224 |
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) |
|
225 |
apply (rule iffI) |
|
226 |
text \<open>\<open>\<Longrightarrow>\<close>\<close> |
|
227 |
apply (erule conjE)+ |
|
228 |
apply (simp add: lemma_1_1a lemma_1_1b lemma_1_1c) |
|
229 |
text \<open>\<open>\<Longleftarrow>\<close>\<close> |
|
230 |
apply (erule conjE)+ |
|
231 |
apply (simp add: lemma_1_2) |
|
232 |
done |
|
19741 | 233 |
|
62116 | 234 |
theorem compositionality_ex_modules: "Execs (A \<parallel> B) = par_execs (Execs A) (Execs B)" |
235 |
apply (unfold Execs_def par_execs_def) |
|
236 |
apply (simp add: asig_of_par) |
|
237 |
apply (rule set_eqI) |
|
238 |
apply (simp add: compositionality_ex actions_of_par) |
|
239 |
done |
|
17233 | 240 |
|
241 |
end |