28 \ (case x of \ |
28 \ (case x of \ |
29 \ Undef => UU \ |
29 \ Undef => UU \ |
30 \ | Def y => \ |
30 \ | Def y => \ |
31 \ (if y:act A then \ |
31 \ (if y:act A then \ |
32 \ (if y:act B then \ |
32 \ (if y:act B then \ |
33 \ (case HD`exA of \ |
33 \ (case HD$exA of \ |
34 \ Undef => UU \ |
34 \ Undef => UU \ |
35 \ | Def a => (case HD`exB of \ |
35 \ | Def a => (case HD$exB of \ |
36 \ Undef => UU \ |
36 \ Undef => UU \ |
37 \ | Def b => \ |
37 \ | Def b => \ |
38 \ (y,(snd a,snd b))>> \ |
38 \ (y,(snd a,snd b))>> \ |
39 \ (mkex2 A B`xs`(TL`exA)`(TL`exB)) (snd a) (snd b))) \ |
39 \ (mkex2 A B$xs$(TL$exA)$(TL$exB)) (snd a) (snd b))) \ |
40 \ else \ |
40 \ else \ |
41 \ (case HD`exA of \ |
41 \ (case HD$exA of \ |
42 \ Undef => UU \ |
42 \ Undef => UU \ |
43 \ | Def a => \ |
43 \ | Def a => \ |
44 \ (y,(snd a,t))>>(mkex2 A B`xs`(TL`exA)`exB) (snd a) t) \ |
44 \ (y,(snd a,t))>>(mkex2 A B$xs$(TL$exA)$exB) (snd a) t) \ |
45 \ ) \ |
45 \ ) \ |
46 \ else \ |
46 \ else \ |
47 \ (if y:act B then \ |
47 \ (if y:act B then \ |
48 \ (case HD`exB of \ |
48 \ (case HD$exB of \ |
49 \ Undef => UU \ |
49 \ Undef => UU \ |
50 \ | Def b => \ |
50 \ | Def b => \ |
51 \ (y,(s,snd b))>>(mkex2 A B`xs`exA`(TL`exB)) s (snd b)) \ |
51 \ (y,(s,snd b))>>(mkex2 A B$xs$exA$(TL$exB)) s (snd b)) \ |
52 \ else \ |
52 \ else \ |
53 \ UU \ |
53 \ UU \ |
54 \ ) \ |
54 \ ) \ |
55 \ ) \ |
55 \ ) \ |
56 \ )))"); |
56 \ )))"); |
57 |
57 |
58 |
58 |
59 Goal "(mkex2 A B`UU`exA`exB) s t = UU"; |
59 Goal "(mkex2 A B$UU$exA$exB) s t = UU"; |
60 by (stac mkex2_unfold 1); |
60 by (stac mkex2_unfold 1); |
61 by (Simp_tac 1); |
61 by (Simp_tac 1); |
62 qed"mkex2_UU"; |
62 qed"mkex2_UU"; |
63 |
63 |
64 Goal "(mkex2 A B`nil`exA`exB) s t= nil"; |
64 Goal "(mkex2 A B$nil$exA$exB) s t= nil"; |
65 by (stac mkex2_unfold 1); |
65 by (stac mkex2_unfold 1); |
66 by (Simp_tac 1); |
66 by (Simp_tac 1); |
67 qed"mkex2_nil"; |
67 qed"mkex2_nil"; |
68 |
68 |
69 Goal "[| x:act A; x~:act B; HD`exA=Def a|] \ |
69 Goal "[| x:act A; x~:act B; HD$exA=Def a|] \ |
70 \ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \ |
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"; |
71 \ (x,snd a,t) >> (mkex2 A B$sch$(TL$exA)$exB) (snd a) t"; |
72 by (rtac trans 1); |
72 by (rtac trans 1); |
73 by (stac mkex2_unfold 1); |
73 by (stac mkex2_unfold 1); |
74 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); |
74 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); |
75 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
75 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
76 qed"mkex2_cons_1"; |
76 qed"mkex2_cons_1"; |
77 |
77 |
78 Goal "[| x~:act A; x:act B; HD`exB=Def b|] \ |
78 Goal "[| x~:act A; x:act B; HD$exB=Def b|] \ |
79 \ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \ |
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)"; |
80 \ (x,s,snd b) >> (mkex2 A B$sch$exA$(TL$exB)) s (snd b)"; |
81 by (rtac trans 1); |
81 by (rtac trans 1); |
82 by (stac mkex2_unfold 1); |
82 by (stac mkex2_unfold 1); |
83 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); |
83 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); |
84 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
84 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
85 qed"mkex2_cons_2"; |
85 qed"mkex2_cons_2"; |
86 |
86 |
87 Goal "[| x:act A; x:act B; HD`exA=Def a;HD`exB=Def b|] \ |
87 Goal "[| x:act A; x:act B; HD$exA=Def a;HD$exB=Def b|] \ |
88 \ ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \ |
88 \ ==> (mkex2 A B$(x>>sch)$exA$exB) s t = \ |
89 \ (x,snd a,snd b) >> \ |
89 \ (x,snd a,snd b) >> \ |
90 \ (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)"; |
90 \ (mkex2 A B$sch$(TL$exA)$(TL$exB)) (snd a) (snd b)"; |
91 by (rtac trans 1); |
91 by (rtac trans 1); |
92 by (stac mkex2_unfold 1); |
92 by (stac mkex2_unfold 1); |
93 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); |
93 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1); |
94 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
94 by (asm_full_simp_tac (simpset() addsimps [Consq_def]) 1); |
95 qed"mkex2_cons_3"; |
95 qed"mkex2_cons_3"; |
154 (* --------------------------------------------------------------------- *) |
154 (* --------------------------------------------------------------------- *) |
155 (* Lemma_2_1 : tfilter(ex) and filter_act are commutative *) |
155 (* Lemma_2_1 : tfilter(ex) and filter_act are commutative *) |
156 (* --------------------------------------------------------------------- *) |
156 (* --------------------------------------------------------------------- *) |
157 |
157 |
158 Goalw [filter_act_def,Filter_ex2_def] |
158 Goalw [filter_act_def,Filter_ex2_def] |
159 "filter_act`(Filter_ex2 (asig_of A)`xs)=\ |
159 "filter_act$(Filter_ex2 (asig_of A)$xs)=\ |
160 \ Filter (%a. a:act A)`(filter_act`xs)"; |
160 \ Filter (%a. a:act A)$(filter_act$xs)"; |
161 |
161 |
162 by (simp_tac (simpset() addsimps [MapFilter,o_def]) 1); |
162 by (simp_tac (simpset() addsimps [MapFilter,o_def]) 1); |
163 qed"lemma_2_1a"; |
163 qed"lemma_2_1a"; |
164 |
164 |
165 |
165 |
166 (* --------------------------------------------------------------------- *) |
166 (* --------------------------------------------------------------------- *) |
167 (* Lemma_2_2 : State-projections do not affect filter_act *) |
167 (* Lemma_2_2 : State-projections do not affect filter_act *) |
168 (* --------------------------------------------------------------------- *) |
168 (* --------------------------------------------------------------------- *) |
169 |
169 |
170 Goal |
170 Goal |
171 "filter_act`(ProjA2`xs) =filter_act`xs &\ |
171 "filter_act$(ProjA2$xs) =filter_act$xs &\ |
172 \ filter_act`(ProjB2`xs) =filter_act`xs"; |
172 \ filter_act$(ProjB2$xs) =filter_act$xs"; |
173 |
173 |
174 by (pair_induct_tac "xs" [] 1); |
174 by (pair_induct_tac "xs" [] 1); |
175 qed"lemma_2_1b"; |
175 qed"lemma_2_1b"; |
176 |
176 |
177 |
177 |
182 (* very similar to lemma_1_1c, but it is not checking if every action element of |
182 (* very similar to lemma_1_1c, but it is not checking if every action element of |
183 an ex is in A or B, but after projecting it onto the action schedule. Of course, this |
183 an ex is in A or B, but after projecting it onto the action schedule. Of course, this |
184 is the same proposition, but we cannot change this one, when then rather lemma_1_1c *) |
184 is the same proposition, but we cannot change this one, when then rather lemma_1_1c *) |
185 |
185 |
186 Goal "!s. is_exec_frag (A||B) (s,xs) \ |
186 Goal "!s. is_exec_frag (A||B) (s,xs) \ |
187 \ --> Forall (%x. x:act (A||B)) (filter_act`xs)"; |
187 \ --> Forall (%x. x:act (A||B)) (filter_act$xs)"; |
188 |
188 |
189 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1); |
189 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1); |
190 (* main case *) |
190 (* main case *) |
191 by (safe_tac set_cs); |
191 by (safe_tac set_cs); |
192 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ |
192 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ |
203 structural induction |
203 structural induction |
204 --------------------------------------------------------------------------- *) |
204 --------------------------------------------------------------------------- *) |
205 |
205 |
206 Goal "! exA exB s t. \ |
206 Goal "! exA exB s t. \ |
207 \ Forall (%x. x:act (A||B)) sch & \ |
207 \ Forall (%x. x:act (A||B)) sch & \ |
208 \ Filter (%a. a:act A)`sch << filter_act`exA &\ |
208 \ Filter (%a. a:act A)$sch << filter_act$exA &\ |
209 \ Filter (%a. a:act B)`sch << filter_act`exB \ |
209 \ Filter (%a. a:act B)$sch << filter_act$exB \ |
210 \ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch"; |
210 \ --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"; |
211 |
211 |
212 by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1); |
212 by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1); |
213 |
213 |
214 (* main case *) |
214 (* main case *) |
215 (* splitting into 4 cases according to a:A, a:B *) |
215 (* splitting into 4 cases according to a:A, a:B *) |
266 --------------------------------------------------------------------------- *) |
266 --------------------------------------------------------------------------- *) |
267 |
267 |
268 |
268 |
269 Goal "! exA exB s t. \ |
269 Goal "! exA exB s t. \ |
270 \ Forall (%x. x:act (A||B)) sch & \ |
270 \ Forall (%x. x:act (A||B)) sch & \ |
271 \ Filter (%a. a:act A)`sch << filter_act`exA &\ |
271 \ Filter (%a. a:act A)$sch << filter_act$exA &\ |
272 \ Filter (%a. a:act B)`sch << filter_act`exB \ |
272 \ Filter (%a. a:act B)$sch << filter_act$exB \ |
273 \ --> stutter (asig_of A) (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))"; |
273 \ --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"; |
274 |
274 |
275 by (mkex_induct_tac "sch" "exA" "exB"); |
275 by (mkex_induct_tac "sch" "exA" "exB"); |
276 |
276 |
277 qed"stutterA_mkex"; |
277 qed"stutterA_mkex"; |
278 |
278 |
279 |
279 |
280 Goal "[| \ |
280 Goal "[| \ |
281 \ Forall (%x. x:act (A||B)) sch ; \ |
281 \ Forall (%x. x:act (A||B)) sch ; \ |
282 \ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\ |
282 \ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;\ |
283 \ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \ |
283 \ Filter (%a. a:act B)$sch << filter_act$(snd exB) |] \ |
284 \ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))"; |
284 \ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))"; |
285 |
285 |
286 by (cut_facts_tac [stutterA_mkex] 1); |
286 by (cut_facts_tac [stutterA_mkex] 1); |
287 by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjA_def,mkex_def]) 1); |
287 by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjA_def,mkex_def]) 1); |
288 by (REPEAT (etac allE 1)); |
288 by (REPEAT (etac allE 1)); |
297 structural induction |
297 structural induction |
298 --------------------------------------------------------------------------- *) |
298 --------------------------------------------------------------------------- *) |
299 |
299 |
300 Goal "! exA exB s t. \ |
300 Goal "! exA exB s t. \ |
301 \ Forall (%x. x:act (A||B)) sch & \ |
301 \ Forall (%x. x:act (A||B)) sch & \ |
302 \ Filter (%a. a:act A)`sch << filter_act`exA &\ |
302 \ Filter (%a. a:act A)$sch << filter_act$exA &\ |
303 \ Filter (%a. a:act B)`sch << filter_act`exB \ |
303 \ Filter (%a. a:act B)$sch << filter_act$exB \ |
304 \ --> stutter (asig_of B) (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))"; |
304 \ --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"; |
305 |
305 |
306 by (mkex_induct_tac "sch" "exA" "exB"); |
306 by (mkex_induct_tac "sch" "exA" "exB"); |
307 |
307 |
308 qed"stutterB_mkex"; |
308 qed"stutterB_mkex"; |
309 |
309 |
310 |
310 |
311 Goal "[| \ |
311 Goal "[| \ |
312 \ Forall (%x. x:act (A||B)) sch ; \ |
312 \ Forall (%x. x:act (A||B)) sch ; \ |
313 \ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\ |
313 \ Filter (%a. a:act A)$sch << filter_act$(snd exA) ;\ |
314 \ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \ |
314 \ Filter (%a. a:act B)$sch << filter_act$(snd exB) |] \ |
315 \ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))"; |
315 \ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))"; |
316 |
316 |
317 by (cut_facts_tac [stutterB_mkex] 1); |
317 by (cut_facts_tac [stutterB_mkex] 1); |
318 by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjB_def,mkex_def]) 1); |
318 by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjB_def,mkex_def]) 1); |
319 by (REPEAT (etac allE 1)); |
319 by (REPEAT (etac allE 1)); |
323 qed"stutter_mkex_on_B"; |
323 qed"stutter_mkex_on_B"; |
324 |
324 |
325 |
325 |
326 (*--------------------------------------------------------------------------- |
326 (*--------------------------------------------------------------------------- |
327 Filter of mkex(sch,exA,exB) to A after projection onto A is exA |
327 Filter of mkex(sch,exA,exB) to A after projection onto A is exA |
328 -- using zip`(proj1`exA)`(proj2`exA) instead of exA -- |
328 -- using zip$(proj1$exA)$(proj2$exA) instead of exA -- |
329 -- because of admissibility problems -- |
329 -- because of admissibility problems -- |
330 structural induction |
330 structural induction |
331 --------------------------------------------------------------------------- *) |
331 --------------------------------------------------------------------------- *) |
332 |
332 |
333 Goal "! exA exB s t. \ |
333 Goal "! exA exB s t. \ |
334 \ Forall (%x. x:act (A||B)) sch & \ |
334 \ Forall (%x. x:act (A||B)) sch & \ |
335 \ Filter (%a. a:act A)`sch << filter_act`exA &\ |
335 \ Filter (%a. a:act A)$sch << filter_act$exA &\ |
336 \ Filter (%a. a:act B)`sch << filter_act`exB \ |
336 \ Filter (%a. a:act B)$sch << filter_act$exB \ |
337 \ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) = \ |
337 \ --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) = \ |
338 \ Zip`(Filter (%a. a:act A)`sch)`(Map snd`exA)"; |
338 \ Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"; |
339 |
339 |
340 by (mkex_induct_tac "sch" "exB" "exA"); |
340 by (mkex_induct_tac "sch" "exB" "exA"); |
341 |
341 |
342 qed"filter_mkex_is_exA_tmp"; |
342 qed"filter_mkex_is_exA_tmp"; |
343 |
343 |
344 (*--------------------------------------------------------------------------- |
344 (*--------------------------------------------------------------------------- |
345 zip`(proj1`y)`(proj2`y) = y (using the lift operations) |
345 zip$(proj1$y)$(proj2$y) = y (using the lift operations) |
346 lemma for admissibility problems |
346 lemma for admissibility problems |
347 --------------------------------------------------------------------------- *) |
347 --------------------------------------------------------------------------- *) |
348 |
348 |
349 Goal "Zip`(Map fst`y)`(Map snd`y) = y"; |
349 Goal "Zip$(Map fst$y)$(Map snd$y) = y"; |
350 by (Seq_induct_tac "y" [] 1); |
350 by (Seq_induct_tac "y" [] 1); |
351 qed"Zip_Map_fst_snd"; |
351 qed"Zip_Map_fst_snd"; |
352 |
352 |
353 |
353 |
354 (*--------------------------------------------------------------------------- |
354 (*--------------------------------------------------------------------------- |
355 filter A`sch = proj1`ex --> zip`(filter A`sch)`(proj2`ex) = ex |
355 filter A$sch = proj1$ex --> zip$(filter A$sch)$(proj2$ex) = ex |
356 lemma for eliminating non admissible equations in assumptions |
356 lemma for eliminating non admissible equations in assumptions |
357 --------------------------------------------------------------------------- *) |
357 --------------------------------------------------------------------------- *) |
358 |
358 |
359 Goal "!! sch ex. \ |
359 Goal "!! sch ex. \ |
360 \ Filter (%a. a:act AB)`sch = filter_act`ex \ |
360 \ Filter (%a. a:act AB)$sch = filter_act$ex \ |
361 \ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)"; |
361 \ ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)"; |
362 by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 1); |
362 by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 1); |
363 by (rtac (Zip_Map_fst_snd RS sym) 1); |
363 by (rtac (Zip_Map_fst_snd RS sym) 1); |
364 qed"trick_against_eq_in_ass"; |
364 qed"trick_against_eq_in_ass"; |
365 |
365 |
366 (*--------------------------------------------------------------------------- |
366 (*--------------------------------------------------------------------------- |
369 --------------------------------------------------------------------------- *) |
369 --------------------------------------------------------------------------- *) |
370 |
370 |
371 |
371 |
372 Goal "!!sch exA exB.\ |
372 Goal "!!sch exA exB.\ |
373 \ [| Forall (%a. a:act (A||B)) sch ; \ |
373 \ [| Forall (%a. a:act (A||B)) sch ; \ |
374 \ Filter (%a. a:act A)`sch = filter_act`(snd exA) ;\ |
374 \ Filter (%a. a:act A)$sch = filter_act$(snd exA) ;\ |
375 \ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\ |
375 \ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]\ |
376 \ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"; |
376 \ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"; |
377 by (asm_full_simp_tac (simpset() addsimps [ProjA_def,Filter_ex_def]) 1); |
377 by (asm_full_simp_tac (simpset() addsimps [ProjA_def,Filter_ex_def]) 1); |
378 by (pair_tac "exA" 1); |
378 by (pair_tac "exA" 1); |
379 by (pair_tac "exB" 1); |
379 by (pair_tac "exB" 1); |
380 by (rtac conjI 1); |
380 by (rtac conjI 1); |
386 qed"filter_mkex_is_exA"; |
386 qed"filter_mkex_is_exA"; |
387 |
387 |
388 |
388 |
389 (*--------------------------------------------------------------------------- |
389 (*--------------------------------------------------------------------------- |
390 Filter of mkex(sch,exA,exB) to B after projection onto B is exB |
390 Filter of mkex(sch,exA,exB) to B after projection onto B is exB |
391 -- using zip`(proj1`exB)`(proj2`exB) instead of exB -- |
391 -- using zip$(proj1$exB)$(proj2$exB) instead of exB -- |
392 -- because of admissibility problems -- |
392 -- because of admissibility problems -- |
393 structural induction |
393 structural induction |
394 --------------------------------------------------------------------------- *) |
394 --------------------------------------------------------------------------- *) |
395 |
395 |
396 |
396 |
397 Goal "! exA exB s t. \ |
397 Goal "! exA exB s t. \ |
398 \ Forall (%x. x:act (A||B)) sch & \ |
398 \ Forall (%x. x:act (A||B)) sch & \ |
399 \ Filter (%a. a:act A)`sch << filter_act`exA &\ |
399 \ Filter (%a. a:act A)$sch << filter_act$exA &\ |
400 \ Filter (%a. a:act B)`sch << filter_act`exB \ |
400 \ Filter (%a. a:act B)$sch << filter_act$exB \ |
401 \ --> Filter_ex2 (asig_of B)`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) = \ |
401 \ --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) = \ |
402 \ Zip`(Filter (%a. a:act B)`sch)`(Map snd`exB)"; |
402 \ Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"; |
403 |
403 |
404 (* notice necessary change of arguments exA and exB *) |
404 (* notice necessary change of arguments exA and exB *) |
405 by (mkex_induct_tac "sch" "exA" "exB"); |
405 by (mkex_induct_tac "sch" "exA" "exB"); |
406 |
406 |
407 qed"filter_mkex_is_exB_tmp"; |
407 qed"filter_mkex_is_exB_tmp"; |
413 --------------------------------------------------------------------------- *) |
413 --------------------------------------------------------------------------- *) |
414 |
414 |
415 |
415 |
416 Goal "!!sch exA exB.\ |
416 Goal "!!sch exA exB.\ |
417 \ [| Forall (%a. a:act (A||B)) sch ; \ |
417 \ [| Forall (%a. a:act (A||B)) sch ; \ |
418 \ Filter (%a. a:act A)`sch = filter_act`(snd exA) ;\ |
418 \ Filter (%a. a:act A)$sch = filter_act$(snd exA) ;\ |
419 \ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\ |
419 \ Filter (%a. a:act B)$sch = filter_act$(snd exB) |]\ |
420 \ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"; |
420 \ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"; |
421 by (asm_full_simp_tac (simpset() addsimps [ProjB_def,Filter_ex_def]) 1); |
421 by (asm_full_simp_tac (simpset() addsimps [ProjB_def,Filter_ex_def]) 1); |
422 by (pair_tac "exA" 1); |
422 by (pair_tac "exA" 1); |
423 by (pair_tac "exB" 1); |
423 by (pair_tac "exB" 1); |
424 by (rtac conjI 1); |
424 by (rtac conjI 1); |
434 (* --------------------------------------------------------------------- *) |
434 (* --------------------------------------------------------------------- *) |
435 |
435 |
436 |
436 |
437 Goal "!s t exA exB. \ |
437 Goal "!s t exA exB. \ |
438 \ Forall (%x. x : act (A || B)) sch &\ |
438 \ Forall (%x. x : act (A || B)) sch &\ |
439 \ Filter (%a. a:act A)`sch << filter_act`exA &\ |
439 \ Filter (%a. a:act A)$sch << filter_act$exA &\ |
440 \ Filter (%a. a:act B)`sch << filter_act`exB \ |
440 \ Filter (%a. a:act B)$sch << filter_act$exB \ |
441 \ --> Forall (%x. fst x : act (A ||B)) \ |
441 \ --> Forall (%x. fst x : act (A ||B)) \ |
442 \ (snd (mkex A B sch (s,exA) (t,exB)))"; |
442 \ (snd (mkex A B sch (s,exA) (t,exB)))"; |
443 |
443 |
444 by (mkex_induct_tac "sch" "exA" "exB"); |
444 by (mkex_induct_tac "sch" "exA" "exB"); |
445 |
445 |
451 (* Main Theorem *) |
451 (* Main Theorem *) |
452 (* ------------------------------------------------------------------ *) |
452 (* ------------------------------------------------------------------ *) |
453 |
453 |
454 Goal |
454 Goal |
455 "sch : schedules (A||B) = \ |
455 "sch : schedules (A||B) = \ |
456 \ (Filter (%a. a:act A)`sch : schedules A &\ |
456 \ (Filter (%a. a:act A)$sch : schedules A &\ |
457 \ Filter (%a. a:act B)`sch : schedules B &\ |
457 \ Filter (%a. a:act B)$sch : schedules B &\ |
458 \ Forall (%x. x:act (A||B)) sch)"; |
458 \ Forall (%x. x:act (A||B)) sch)"; |
459 |
459 |
460 by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1); |
460 by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1); |
461 by (safe_tac set_cs); |
461 by (safe_tac set_cs); |
462 (* ==> *) |
462 (* ==> *) |