3071
|
1 |
(* Title: HOLCF/IOA/meta_theory/CompoScheds.ML
|
|
2 |
ID:
|
|
3 |
Author: Olaf M"uller
|
|
4 |
Copyright 1996 TU Muenchen
|
|
5 |
|
|
6 |
Compositionality on Schedule level.
|
|
7 |
*)
|
|
8 |
|
|
9 |
|
|
10 |
|
|
11 |
Addsimps [surjective_pairing RS sym];
|
|
12 |
|
|
13 |
|
|
14 |
|
|
15 |
(* ------------------------------------------------------------------------------- *)
|
|
16 |
|
|
17 |
section "mkex rewrite rules";
|
|
18 |
|
|
19 |
(* ---------------------------------------------------------------- *)
|
|
20 |
(* mkex2 *)
|
|
21 |
(* ---------------------------------------------------------------- *)
|
|
22 |
|
|
23 |
|
|
24 |
bind_thm ("mkex2_unfold", fix_prover2 thy mkex2_def
|
|
25 |
"mkex2 A B = (LAM sch exA exB. (%s t. case sch of \
|
|
26 |
\ nil => nil \
|
|
27 |
\ | x##xs => \
|
|
28 |
\ (case x of \
|
|
29 |
\ Undef => UU \
|
|
30 |
\ | Def y => \
|
|
31 |
\ (if y:act A then \
|
|
32 |
\ (if y:act B then \
|
|
33 |
\ (case HD`exA of \
|
|
34 |
\ Undef => UU \
|
|
35 |
\ | Def a => (case HD`exB of \
|
|
36 |
\ Undef => UU \
|
|
37 |
\ | Def b => \
|
|
38 |
\ (y,(snd a,snd b))>> \
|
|
39 |
\ (mkex2 A B`xs`(TL`exA)`(TL`exB)) (snd a) (snd b))) \
|
|
40 |
\ else \
|
|
41 |
\ (case HD`exA of \
|
|
42 |
\ Undef => UU \
|
|
43 |
\ | Def a => \
|
|
44 |
\ (y,(snd a,t))>>(mkex2 A B`xs`(TL`exA)`exB) (snd a) t) \
|
|
45 |
\ ) \
|
|
46 |
\ else \
|
|
47 |
\ (if y:act B then \
|
|
48 |
\ (case HD`exB of \
|
|
49 |
\ Undef => UU \
|
|
50 |
\ | Def b => \
|
|
51 |
\ (y,(s,snd b))>>(mkex2 A B`xs`exA`(TL`exB)) s (snd b)) \
|
|
52 |
\ else \
|
|
53 |
\ UU \
|
|
54 |
\ ) \
|
|
55 |
\ ) \
|
|
56 |
\ )))");
|
|
57 |
|
|
58 |
|
|
59 |
goal thy "(mkex2 A B`UU`exA`exB) s t = UU";
|
|
60 |
by (stac mkex2_unfold 1);
|
|
61 |
by (Simp_tac 1);
|
|
62 |
qed"mkex2_UU";
|
|
63 |
|
|
64 |
goal thy "(mkex2 A B`nil`exA`exB) s t= nil";
|
|
65 |
by (stac mkex2_unfold 1);
|
|
66 |
by (Simp_tac 1);
|
|
67 |
qed"mkex2_nil";
|
|
68 |
|
|
69 |
goal thy "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \
|
|
70 |
\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
|
|
71 |
\ (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
|
|
72 |
br trans 1;
|
|
73 |
by (stac mkex2_unfold 1);
|
|
74 |
by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
|
|
75 |
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
|
|
76 |
qed"mkex2_cons_1";
|
|
77 |
|
|
78 |
goal thy "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
|
|
79 |
\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
|
|
80 |
\ (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
|
|
81 |
br trans 1;
|
|
82 |
by (stac mkex2_unfold 1);
|
|
83 |
by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
|
|
84 |
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
|
|
85 |
qed"mkex2_cons_2";
|
|
86 |
|
|
87 |
goal thy "!!x.[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \
|
|
88 |
\ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
|
|
89 |
\ (x,snd a,snd b) >> \
|
|
90 |
\ (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
|
|
91 |
br trans 1;
|
|
92 |
by (stac mkex2_unfold 1);
|
|
93 |
by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
|
|
94 |
by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
|
|
95 |
qed"mkex2_cons_3";
|
|
96 |
|
|
97 |
Addsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
|
|
98 |
|
|
99 |
|
|
100 |
(* ---------------------------------------------------------------- *)
|
|
101 |
(* mkex *)
|
|
102 |
(* ---------------------------------------------------------------- *)
|
|
103 |
|
|
104 |
goal thy "mkex A B UU (s,exA) (t,exB) = ((s,t),UU)";
|
|
105 |
by (simp_tac (!simpset addsimps [mkex_def]) 1);
|
|
106 |
qed"mkex_UU";
|
|
107 |
|
|
108 |
goal thy "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)";
|
|
109 |
by (simp_tac (!simpset addsimps [mkex_def]) 1);
|
|
110 |
qed"mkex_nil";
|
|
111 |
|
|
112 |
goal thy "!!x.[| x:act A; x~:act B |] \
|
|
113 |
\ ==> mkex A B (x>>sch) (s,a>>exA) (t,exB) = \
|
|
114 |
\ ((s,t), (x,snd a,t) >> snd (mkex A B sch (snd a,exA) (t,exB)))";
|
|
115 |
by (simp_tac (!simpset addsimps [mkex_def]
|
|
116 |
setloop (split_tac [expand_if]) ) 1);
|
|
117 |
by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
|
|
118 |
auto();
|
|
119 |
qed"mkex_cons_1";
|
|
120 |
|
|
121 |
goal thy "!!x.[| x~:act A; x:act B |] \
|
|
122 |
\ ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) = \
|
|
123 |
\ ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
|
|
124 |
by (simp_tac (!simpset addsimps [mkex_def]
|
|
125 |
setloop (split_tac [expand_if]) ) 1);
|
|
126 |
by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
|
|
127 |
auto();
|
|
128 |
qed"mkex_cons_2";
|
|
129 |
|
|
130 |
goal thy "!!x.[| x:act A; x:act B |] \
|
|
131 |
\ ==> mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
|
|
132 |
\ ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
|
|
133 |
by (simp_tac (!simpset addsimps [mkex_def]
|
|
134 |
setloop (split_tac [expand_if]) ) 1);
|
|
135 |
by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
|
|
136 |
auto();
|
|
137 |
qed"mkex_cons_3";
|
|
138 |
|
|
139 |
Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
|
|
140 |
|
|
141 |
val composch_simps = [mkex_UU,mkex_nil,
|
|
142 |
mkex_cons_1,mkex_cons_2,mkex_cons_3];
|
|
143 |
|
|
144 |
Addsimps composch_simps;
|
|
145 |
|
|
146 |
|
|
147 |
|
|
148 |
(* ------------------------------------------------------------------ *)
|
|
149 |
(* The following lemmata aim for *)
|
|
150 |
(* COMPOSITIONALITY on SCHEDULE Level *)
|
|
151 |
(* ------------------------------------------------------------------ *)
|
|
152 |
|
|
153 |
(* ---------------------------------------------------------------------- *)
|
|
154 |
section "Lemmas for ==>";
|
|
155 |
(* ----------------------------------------------------------------------*)
|
|
156 |
|
|
157 |
(* --------------------------------------------------------------------- *)
|
|
158 |
(* Lemma_2_1 : tfilter(ex) and filter_act are commutative *)
|
|
159 |
(* --------------------------------------------------------------------- *)
|
|
160 |
|
|
161 |
goalw thy [filter_act_def,Filter_ex2_def]
|
|
162 |
"filter_act`(Filter_ex2 A`xs)=\
|
|
163 |
\ Filter (%a.a:act A)`(filter_act`xs)";
|
|
164 |
|
|
165 |
by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1);
|
|
166 |
qed"lemma_2_1a";
|
|
167 |
|
|
168 |
|
|
169 |
(* --------------------------------------------------------------------- *)
|
|
170 |
(* Lemma_2_2 : State-projections do not affect filter_act *)
|
|
171 |
(* --------------------------------------------------------------------- *)
|
|
172 |
|
|
173 |
goal thy
|
|
174 |
"filter_act`(ProjA2`xs) =filter_act`xs &\
|
|
175 |
\ filter_act`(ProjB2`xs) =filter_act`xs";
|
|
176 |
|
|
177 |
by (pair_induct_tac "xs" [] 1);
|
|
178 |
qed"lemma_2_1b";
|
|
179 |
|
|
180 |
|
|
181 |
(* --------------------------------------------------------------------- *)
|
|
182 |
(* Schedules of A||B have only A- or B-actions *)
|
|
183 |
(* --------------------------------------------------------------------- *)
|
|
184 |
|
|
185 |
(* FIX: very similar to lemma_1_1c, but it is not checking if every action element of
|
|
186 |
an ex is in A or B, but after projecting it onto the action schedule. Of course, this
|
|
187 |
is the same proposition, but we cannot change this one, when then rather lemma_1_1c *)
|
|
188 |
|
|
189 |
goal thy "!s. is_execution_fragment (A||B) (s,xs) \
|
|
190 |
\ --> Forall (%x.x:act (A||B)) (filter_act`xs)";
|
|
191 |
|
|
192 |
by (pair_induct_tac "xs" [is_execution_fragment_def,Forall_def,sforall_def] 1);
|
|
193 |
(* main case *)
|
|
194 |
by (safe_tac set_cs);
|
|
195 |
by (REPEAT (asm_full_simp_tac (!simpset addsimps trans_of_defs2 @
|
|
196 |
[actions_asig_comp,asig_of_par]) 1));
|
|
197 |
qed"sch_actions_in_AorB";
|
|
198 |
|
|
199 |
|
|
200 |
(* --------------------------------------------------------------------------*)
|
|
201 |
section "Lemmas for <==";
|
|
202 |
(* ---------------------------------------------------------------------------*)
|
|
203 |
|
|
204 |
(*---------------------------------------------------------------------------
|
|
205 |
Filtering actions out of mkex(sch,exA,exB) yields the oracle sch
|
|
206 |
structural induction
|
|
207 |
--------------------------------------------------------------------------- *)
|
|
208 |
|
|
209 |
goal thy "! exA exB s t. \
|
|
210 |
\ Forall (%x.x:act (A||B)) sch & \
|
|
211 |
\ Filter (%a.a:act A)`sch << filter_act`exA &\
|
|
212 |
\ Filter (%a.a:act B)`sch << filter_act`exB \
|
|
213 |
\ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch";
|
|
214 |
|
|
215 |
by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1);
|
|
216 |
|
|
217 |
(* main case *)
|
|
218 |
(* splitting into 4 cases according to a:A, a:B *)
|
|
219 |
by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
|
|
220 |
by (safe_tac set_cs);
|
|
221 |
|
|
222 |
(* Case y:A, y:B *)
|
|
223 |
by (Seq_case_simp_tac "exA" 1);
|
|
224 |
(* Case exA=UU, Case exA=nil*)
|
|
225 |
(* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
|
|
226 |
is used! --> to generate a contradiction using ~a>>ss<< UU(nil), using theorems
|
|
227 |
Cons_not_less_UU and Cons_not_less_nil *)
|
|
228 |
by (Seq_case_simp_tac "exB" 1);
|
|
229 |
(* Case exA=a>>x, exB=b>>y *)
|
|
230 |
(* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
|
|
231 |
as otherwise mkex_cons_3 would not be rewritten without use of rotate_tac: then tactic
|
|
232 |
would not be generally applicable *)
|
|
233 |
by (Asm_full_simp_tac 1);
|
|
234 |
|
|
235 |
(* Case y:A, y~:B *)
|
|
236 |
by (Seq_case_simp_tac "exB" 1);
|
|
237 |
by (Asm_full_simp_tac 1);
|
|
238 |
|
|
239 |
(* Case y~:A, y:B *)
|
|
240 |
by (Seq_case_simp_tac "exA" 1);
|
|
241 |
by (Asm_full_simp_tac 1);
|
|
242 |
|
|
243 |
(* Case y~:A, y~:B *)
|
|
244 |
by (asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp]) 1);
|
|
245 |
qed"Mapfst_mkex_is_sch";
|
|
246 |
|
|
247 |
|
|
248 |
(* generalizing the proof above to a tactic *)
|
|
249 |
|
|
250 |
fun mkex_induct_tac sch exA exB =
|
|
251 |
EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def],
|
|
252 |
asm_full_simp_tac (!simpset setloop split_tac [expand_if]),
|
|
253 |
SELECT_GOAL (safe_tac set_cs),
|
|
254 |
Seq_case_simp_tac exA,
|
|
255 |
Seq_case_simp_tac exB,
|
|
256 |
Asm_full_simp_tac,
|
|
257 |
Seq_case_simp_tac exB,
|
|
258 |
Asm_full_simp_tac,
|
|
259 |
Seq_case_simp_tac exA,
|
|
260 |
Asm_full_simp_tac,
|
|
261 |
asm_full_simp_tac (!simpset addsimps [asig_of_par,actions_asig_comp])
|
|
262 |
];
|
|
263 |
|
|
264 |
|
|
265 |
|
|
266 |
(*---------------------------------------------------------------------------
|
|
267 |
Projection of mkex(sch,exA,exB) onto A stutters on A
|
|
268 |
structural induction
|
|
269 |
--------------------------------------------------------------------------- *)
|
|
270 |
|
|
271 |
|
|
272 |
goal thy "! exA exB s t. \
|
|
273 |
\ Forall (%x.x:act (A||B)) sch & \
|
|
274 |
\ Filter (%a.a:act A)`sch << filter_act`exA &\
|
|
275 |
\ Filter (%a.a:act B)`sch << filter_act`exB \
|
|
276 |
\ --> stutter A (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
|
|
277 |
|
|
278 |
by (mkex_induct_tac "sch" "exA" "exB");
|
|
279 |
|
|
280 |
qed"stutterA_mkex";
|
|
281 |
|
|
282 |
|
|
283 |
goal thy "!! sch.[| \
|
|
284 |
\ Forall (%x.x:act (A||B)) sch ; \
|
|
285 |
\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
|
|
286 |
\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
|
|
287 |
\ ==> stutter A (ProjA (mkex A B sch exA exB))";
|
|
288 |
|
|
289 |
by (cut_facts_tac [stutterA_mkex] 1);
|
|
290 |
by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
|
|
291 |
by (REPEAT (etac allE 1));
|
|
292 |
bd mp 1;
|
|
293 |
ba 2;
|
|
294 |
by (Asm_full_simp_tac 1);
|
|
295 |
qed"stutter_mkex_on_A";
|
|
296 |
|
|
297 |
|
|
298 |
(*---------------------------------------------------------------------------
|
|
299 |
Projection of mkex(sch,exA,exB) onto B stutters on B
|
|
300 |
structural induction
|
|
301 |
--------------------------------------------------------------------------- *)
|
|
302 |
|
|
303 |
goal thy "! exA exB s t. \
|
|
304 |
\ Forall (%x.x:act (A||B)) sch & \
|
|
305 |
\ Filter (%a.a:act A)`sch << filter_act`exA &\
|
|
306 |
\ Filter (%a.a:act B)`sch << filter_act`exB \
|
|
307 |
\ --> stutter B (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
|
|
308 |
|
|
309 |
by (mkex_induct_tac "sch" "exA" "exB");
|
|
310 |
|
|
311 |
qed"stutterB_mkex";
|
|
312 |
|
|
313 |
|
|
314 |
goal thy "!! sch.[| \
|
|
315 |
\ Forall (%x.x:act (A||B)) sch ; \
|
|
316 |
\ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
|
|
317 |
\ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
|
|
318 |
\ ==> stutter B (ProjB (mkex A B sch exA exB))";
|
|
319 |
|
|
320 |
by (cut_facts_tac [stutterB_mkex] 1);
|
|
321 |
by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
|
|
322 |
by (REPEAT (etac allE 1));
|
|
323 |
bd mp 1;
|
|
324 |
ba 2;
|
|
325 |
by (Asm_full_simp_tac 1);
|
|
326 |
qed"stutter_mkex_on_B";
|
|
327 |
|
|
328 |
|
|
329 |
(*---------------------------------------------------------------------------
|
|
330 |
Filter of mkex(sch,exA,exB) to A after projection onto A is exA
|
|
331 |
-- using zip`(proj1`exA)`(proj2`exA) instead of exA --
|
|
332 |
-- because of admissibility problems --
|
|
333 |
structural induction
|
|
334 |
--------------------------------------------------------------------------- *)
|
|
335 |
|
|
336 |
goal thy "! exA exB s t. \
|
|
337 |
\ Forall (%x.x:act (A||B)) sch & \
|
|
338 |
\ Filter (%a.a:act A)`sch << filter_act`exA &\
|
|
339 |
\ Filter (%a.a:act B)`sch << filter_act`exB \
|
|
340 |
\ --> Filter_ex2 A`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
|
|
341 |
\ Zip`(Filter (%a.a:act A)`sch)`(Map snd`exA)";
|
|
342 |
|
|
343 |
by (mkex_induct_tac "sch" "exA" "exB");
|
|
344 |
|
|
345 |
qed"filter_mkex_is_exA_tmp";
|
|
346 |
|
|
347 |
(*---------------------------------------------------------------------------
|
|
348 |
zip`(proj1`y)`(proj2`y) = y (using the lift operations)
|
|
349 |
lemma for admissibility problems
|
|
350 |
--------------------------------------------------------------------------- *)
|
|
351 |
|
|
352 |
goal thy "Zip`(Map fst`y)`(Map snd`y) = y";
|
|
353 |
by (Seq_induct_tac "y" [] 1);
|
|
354 |
qed"Zip_Map_fst_snd";
|
|
355 |
|
|
356 |
|
|
357 |
(*---------------------------------------------------------------------------
|
|
358 |
filter A`sch = proj1`ex --> zip`(filter A`sch)`(proj2`ex) = ex
|
|
359 |
lemma for eliminating non admissible equations in assumptions
|
|
360 |
--------------------------------------------------------------------------- *)
|
|
361 |
|
|
362 |
goal thy "!! sch ex. \
|
|
363 |
\ Filter (%a.a:act AB)`sch = filter_act`ex \
|
|
364 |
\ ==> ex = Zip`(Filter (%a.a:act AB)`sch)`(Map snd`ex)";
|
|
365 |
by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 1);
|
|
366 |
by (rtac (Zip_Map_fst_snd RS sym) 1);
|
|
367 |
qed"trick_against_eq_in_ass";
|
|
368 |
|
|
369 |
(*---------------------------------------------------------------------------
|
|
370 |
Filter of mkex(sch,exA,exB) to A after projection onto A is exA
|
|
371 |
using the above trick
|
|
372 |
--------------------------------------------------------------------------- *)
|
|
373 |
|
|
374 |
|
|
375 |
goal thy "!!sch exA exB.\
|
|
376 |
\ [| Forall (%a.a:act (A||B)) sch ; \
|
|
377 |
\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\
|
|
378 |
\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
|
|
379 |
\ ==> Filter_ex A (ProjA (mkex A B sch exA exB)) = exA";
|
|
380 |
by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
|
|
381 |
by (pair_tac "exA" 1);
|
|
382 |
by (pair_tac "exB" 1);
|
|
383 |
br conjI 1;
|
|
384 |
by (simp_tac (!simpset addsimps [mkex_def]) 1);
|
|
385 |
by (stac trick_against_eq_in_ass 1);
|
|
386 |
back();
|
|
387 |
ba 1;
|
|
388 |
by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exA_tmp]) 1);
|
|
389 |
qed"filter_mkex_is_exA";
|
|
390 |
|
|
391 |
|
|
392 |
(*---------------------------------------------------------------------------
|
|
393 |
Filter of mkex(sch,exA,exB) to B after projection onto B is exB
|
|
394 |
-- using zip`(proj1`exB)`(proj2`exB) instead of exB --
|
|
395 |
-- because of admissibility problems --
|
|
396 |
structural induction
|
|
397 |
--------------------------------------------------------------------------- *)
|
|
398 |
|
|
399 |
|
|
400 |
goal thy "! exA exB s t. \
|
|
401 |
\ Forall (%x.x:act (A||B)) sch & \
|
|
402 |
\ Filter (%a.a:act A)`sch << filter_act`exA &\
|
|
403 |
\ Filter (%a.a:act B)`sch << filter_act`exB \
|
|
404 |
\ --> Filter_ex2 B`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) = \
|
|
405 |
\ Zip`(Filter (%a.a:act B)`sch)`(Map snd`exB)";
|
|
406 |
|
|
407 |
(* notice necessary change of arguments exA and exB *)
|
|
408 |
by (mkex_induct_tac "sch" "exB" "exA");
|
|
409 |
|
|
410 |
qed"filter_mkex_is_exB_tmp";
|
|
411 |
|
|
412 |
|
|
413 |
(*---------------------------------------------------------------------------
|
|
414 |
Filter of mkex(sch,exA,exB) to A after projection onto B is exB
|
|
415 |
using the above trick
|
|
416 |
--------------------------------------------------------------------------- *)
|
|
417 |
|
|
418 |
|
|
419 |
goal thy "!!sch exA exB.\
|
|
420 |
\ [| Forall (%a.a:act (A||B)) sch ; \
|
|
421 |
\ Filter (%a.a:act A)`sch = filter_act`(snd exA) ;\
|
|
422 |
\ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
|
|
423 |
\ ==> Filter_ex B (ProjB (mkex A B sch exA exB)) = exB";
|
|
424 |
by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
|
|
425 |
by (pair_tac "exA" 1);
|
|
426 |
by (pair_tac "exB" 1);
|
|
427 |
br conjI 1;
|
|
428 |
by (simp_tac (!simpset addsimps [mkex_def]) 1);
|
|
429 |
by (stac trick_against_eq_in_ass 1);
|
|
430 |
back();
|
|
431 |
ba 1;
|
|
432 |
by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exB_tmp]) 1);
|
|
433 |
qed"filter_mkex_is_exB";
|
|
434 |
|
|
435 |
(* --------------------------------------------------------------------- *)
|
|
436 |
(* mkex has only A- or B-actions *)
|
|
437 |
(* --------------------------------------------------------------------- *)
|
|
438 |
|
|
439 |
|
|
440 |
goal thy "!s t exA exB. \
|
|
441 |
\ Forall (%x. x : act (A || B)) sch &\
|
|
442 |
\ Filter (%a.a:act A)`sch << filter_act`exA &\
|
|
443 |
\ Filter (%a.a:act B)`sch << filter_act`exB \
|
|
444 |
\ --> Forall (%x.fst x : act (A ||B)) \
|
|
445 |
\ (snd (mkex A B sch (s,exA) (t,exB)))";
|
|
446 |
|
|
447 |
by (mkex_induct_tac "sch" "exA" "exB");
|
|
448 |
|
|
449 |
qed"mkex_actions_in_AorB";
|
|
450 |
|
|
451 |
|
|
452 |
(* ------------------------------------------------------------------ *)
|
|
453 |
(* COMPOSITIONALITY on SCHEDULE Level *)
|
|
454 |
(* Main Theorem *)
|
|
455 |
(* ------------------------------------------------------------------ *)
|
|
456 |
|
|
457 |
goal thy
|
|
458 |
"sch : schedules (A||B) = \
|
|
459 |
\ (Filter (%a.a:act A)`sch : schedules A &\
|
|
460 |
\ Filter (%a.a:act B)`sch : schedules B &\
|
|
461 |
\ Forall (%x. x:act (A||B)) sch)";
|
|
462 |
|
|
463 |
by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1);
|
|
464 |
by (safe_tac set_cs);
|
|
465 |
(* ==> *)
|
|
466 |
by (res_inst_tac [("x","Filter_ex A (ProjA ex)")] bexI 1);
|
|
467 |
by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
|
|
468 |
by (simp_tac (!simpset addsimps [Filter_ex_def,ProjA_def,
|
|
469 |
lemma_2_1a,lemma_2_1b]) 1);
|
|
470 |
by (res_inst_tac [("x","Filter_ex B (ProjB ex)")] bexI 1);
|
|
471 |
by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
|
|
472 |
by (simp_tac (!simpset addsimps [Filter_ex_def,ProjB_def,
|
|
473 |
lemma_2_1a,lemma_2_1b]) 1);
|
|
474 |
by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
|
|
475 |
by (pair_tac "ex" 1);
|
|
476 |
be conjE 1;
|
|
477 |
by (asm_full_simp_tac (!simpset addsimps [sch_actions_in_AorB]) 1);
|
|
478 |
|
|
479 |
(* <== *)
|
|
480 |
|
|
481 |
(* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
|
|
482 |
we need here *)
|
|
483 |
ren "exA exB" 1;
|
|
484 |
by (res_inst_tac [("x","mkex A B sch exA exB")] bexI 1);
|
|
485 |
(* mkex actions are just the oracle *)
|
|
486 |
by (pair_tac "exA" 1);
|
|
487 |
by (pair_tac "exB" 1);
|
|
488 |
by (asm_full_simp_tac (!simpset addsimps [Mapfst_mkex_is_sch]) 1);
|
|
489 |
|
|
490 |
(* mkex is an execution -- use compositionality on ex-level *)
|
|
491 |
by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 1);
|
|
492 |
by (asm_full_simp_tac (!simpset addsimps
|
|
493 |
[stutter_mkex_on_A, stutter_mkex_on_B,
|
|
494 |
filter_mkex_is_exB,filter_mkex_is_exA]) 1);
|
|
495 |
by (pair_tac "exA" 1);
|
|
496 |
by (pair_tac "exB" 1);
|
|
497 |
by (asm_full_simp_tac (!simpset addsimps [mkex_actions_in_AorB]) 1);
|
|
498 |
qed"compositionality_sch";
|
|
499 |
|
|
500 |
|
|
501 |
|
|
502 |
Delsimps compoex_simps;
|
|
503 |
Delsimps composch_simps; |