equal
deleted
inserted
replaced
144 by (cut_facts_tac [p1] 1); |
144 by (cut_facts_tac [p1] 1); |
145 be (p2 RS subst) 1; |
145 be (p2 RS subst) 1; |
146 qed"subst_lemma2"; |
146 qed"subst_lemma2"; |
147 |
147 |
148 |
148 |
149 goal thy "!!A B. compat_ioas A B ==> \ |
149 goal thy "!!A B. compatible A B ==> \ |
150 \ ! schA schB. Forall (%x. x:act (A||B)) tr \ |
150 \ ! schA schB. Forall (%x. x:act (A||B)) tr \ |
151 \ --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)"; |
151 \ --> Forall (%x. x:act (A||B)) (mksch A B`tr`schA`schB)"; |
152 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
152 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
153 by (safe_tac set_cs); |
153 by (safe_tac set_cs); |
154 by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 1); |
154 by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 1); |
173 auto(); |
173 auto(); |
174 qed"ForallAorB_mksch1"; |
174 qed"ForallAorB_mksch1"; |
175 |
175 |
176 bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp); |
176 bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp); |
177 |
177 |
178 goal thy "!!A B. compat_ioas B A ==> \ |
178 goal thy "!!A B. compatible B A ==> \ |
179 \ ! schA schB. (Forall (%x. x:act B & x~:act A) tr \ |
179 \ ! schA schB. (Forall (%x. x:act B & x~:act A) tr \ |
180 \ --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))"; |
180 \ --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))"; |
181 |
181 |
182 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
182 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
183 by (safe_tac set_cs); |
183 by (safe_tac set_cs); |
187 qed"ForallBnA_mksch"; |
187 qed"ForallBnA_mksch"; |
188 |
188 |
189 bind_thm ("ForallBnAmksch",ForallBnA_mksch RS spec RS spec RS mp); |
189 bind_thm ("ForallBnAmksch",ForallBnA_mksch RS spec RS spec RS mp); |
190 |
190 |
191 |
191 |
192 goal thy "!!A B. compat_ioas A B ==> \ |
192 goal thy "!!A B. compatible A B ==> \ |
193 \ ! schA schB. (Forall (%x. x:act A & x~:act B) tr \ |
193 \ ! schA schB. (Forall (%x. x:act A & x~:act B) tr \ |
194 \ --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))"; |
194 \ --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))"; |
195 |
195 |
196 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
196 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); |
197 by (safe_tac set_cs); |
197 by (safe_tac set_cs); |
280 |
280 |
281 |
281 |
282 (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *) |
282 (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *) |
283 Delsimps [FilterConc]; |
283 Delsimps [FilterConc]; |
284 |
284 |
285 goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compat_ioas A B|] ==> \ |
285 goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \ |
286 \! y.Forall (%x.x:act B) y & Forall (%x. x:act B & x~:act A) bs &\ |
286 \! y.Forall (%x.x:act B) y & Forall (%x. x:act B & x~:act A) bs &\ |
287 \ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \ |
287 \ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \ |
288 \ --> (? y1 y2. (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \ |
288 \ --> (? y1 y2. (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \ |
289 \ Forall (%x. x:act B & x~:act A) y1 & \ |
289 \ Forall (%x. x:act B & x~:act A) y1 & \ |
290 \ Finite y1 & y = (y1 @@ y2) & \ |
290 \ Finite y1 & y = (y1 @@ y2) & \ |
335 |
335 |
336 (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *) |
336 (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *) |
337 Delsimps [FilterConc]; |
337 Delsimps [FilterConc]; |
338 |
338 |
339 |
339 |
340 goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compat_ioas A B|] ==> \ |
340 goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==> \ |
341 \! x.Forall (%x.x:act A) x & Forall (%x. x:act A & x~:act B) as &\ |
341 \! x.Forall (%x.x:act A) x & Forall (%x. x:act A & x~:act B) as &\ |
342 \ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \ |
342 \ Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \ |
343 \ --> (? x1 x2. (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \ |
343 \ --> (? x1 x2. (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \ |
344 \ Forall (%x. x:act A & x~:act B) x1 & \ |
344 \ Forall (%x. x:act A & x~:act B) x1 & \ |
345 \ Finite x1 & x = (x1 @@ x2) & \ |
345 \ Finite x1 & x = (x1 @@ x2) & \ |
477 section"Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"; |
477 section"Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"; |
478 (* structural induction |
478 (* structural induction |
479 ------------------------------------------------------------------------------------- *) |
479 ------------------------------------------------------------------------------------- *) |
480 |
480 |
481 goal thy |
481 goal thy |
482 "!! A B. [| compat_ioas A B; compat_ioas B A;\ |
482 "!! A B. [| compatible A B; compatible B A;\ |
483 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
483 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
484 \ ! schA schB. Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \ |
484 \ ! schA schB. Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \ |
485 \ Forall (%x.x:ext (A||B)) tr & \ |
485 \ Forall (%x.x:ext (A||B)) tr & \ |
486 \ Filter (%a.a:act A)`tr << Filter (%a.a:ext A)`schA &\ |
486 \ Filter (%a.a:act A)`tr << Filter (%a.a:ext A)`schA &\ |
487 \ Filter (%a.a:act B)`tr << Filter (%a.a:ext B)`schB \ |
487 \ Filter (%a.a:act B)`tr << Filter (%a.a:ext B)`schB \ |
553 (*--------------------------------------------------------------------------- |
553 (*--------------------------------------------------------------------------- |
554 Filter of mksch(tr,schA,schB) to A is schA |
554 Filter of mksch(tr,schA,schB) to A is schA |
555 take lemma |
555 take lemma |
556 --------------------------------------------------------------------------- *) |
556 --------------------------------------------------------------------------- *) |
557 |
557 |
558 goal thy "!! A B. [| compat_ioas A B; compat_ioas B A; \ |
558 goal thy "!! A B. [| compatible A B; compatible B A; \ |
559 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
559 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
560 \ Forall (%x.x:ext (A||B)) tr & \ |
560 \ Forall (%x.x:ext (A||B)) tr & \ |
561 \ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \ |
561 \ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \ |
562 \ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\ |
562 \ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\ |
563 \ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\ |
563 \ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\ |
687 |
687 |
688 (* --------------------------------------------------------------------------- *) |
688 (* --------------------------------------------------------------------------- *) |
689 |
689 |
690 |
690 |
691 |
691 |
692 goal thy "!! A B. [| compat_ioas A B; compat_ioas B A; \ |
692 goal thy "!! A B. [| compatible A B; compatible B A; \ |
693 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
693 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
694 \ Forall (%x.x:ext (A||B)) tr & \ |
694 \ Forall (%x.x:ext (A||B)) tr & \ |
695 \ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \ |
695 \ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \ |
696 \ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\ |
696 \ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\ |
697 \ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\ |
697 \ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\ |
929 |
929 |
930 (* --------------------------------------------------------------------------- *) |
930 (* --------------------------------------------------------------------------- *) |
931 |
931 |
932 |
932 |
933 |
933 |
934 goal thy "!! A B. [| compat_ioas A B; compat_ioas B A; \ |
934 goal thy "!! A B. [| compatible A B; compatible B A; \ |
935 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
935 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \ |
936 \ Forall (%x.x:ext (A||B)) tr & \ |
936 \ Forall (%x.x:ext (A||B)) tr & \ |
937 \ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \ |
937 \ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \ |
938 \ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\ |
938 \ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\ |
939 \ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\ |
939 \ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\ |
1168 (* ------------------------------------------------------------------ *) |
1168 (* ------------------------------------------------------------------ *) |
1169 section"COMPOSITIONALITY on TRACE Level -- Main Theorem"; |
1169 section"COMPOSITIONALITY on TRACE Level -- Main Theorem"; |
1170 (* ------------------------------------------------------------------ *) |
1170 (* ------------------------------------------------------------------ *) |
1171 |
1171 |
1172 goal thy |
1172 goal thy |
1173 "!! A B. [| IOA A; IOA B; compat_ioas A B; compat_ioas B A; \ |
1173 "!! A B. [| IOA A; IOA B; compatible A B; compatible B A; \ |
1174 \ is_asig(asig_of A); is_asig(asig_of B)|] \ |
1174 \ is_asig(asig_of A); is_asig(asig_of B)|] \ |
1175 \ ==> tr: traces(A||B) = \ |
1175 \ ==> tr: traces(A||B) = \ |
1176 \ (Filter (%a.a:act A)`tr : traces A &\ |
1176 \ (Filter (%a.a:act A)`tr : traces A &\ |
1177 \ Filter (%a.a:act B)`tr : traces B &\ |
1177 \ Filter (%a.a:act B)`tr : traces B &\ |
1178 \ Forall (%x. x:ext(A||B)) tr)"; |
1178 \ Forall (%x. x:ext(A||B)) tr)"; |