18 \ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
18 \ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
19 by (rtac ForallPFilterQR 1); |
19 by (rtac ForallPFilterQR 1); |
20 (* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q`tr = Filter R`tr *) |
20 (* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q`tr = Filter R`tr *) |
21 by (assume_tac 2); |
21 by (assume_tac 2); |
22 by (rtac compatibility_consequence3 1); |
22 by (rtac compatibility_consequence3 1); |
23 by (REPEAT (asm_full_simp_tac (!simpset |
23 by (REPEAT (asm_full_simp_tac (simpset() |
24 addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
24 addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
25 qed"Filter_actAisFilter_extA"; |
25 qed"Filter_actAisFilter_extA"; |
26 |
26 |
27 |
27 |
28 (* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) |
28 (* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) |
36 "!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \ |
36 "!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \ |
37 \ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
37 \ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
38 by (rtac ForallPFilterQR 1); |
38 by (rtac ForallPFilterQR 1); |
39 by (assume_tac 2); |
39 by (assume_tac 2); |
40 by (rtac compatibility_consequence4 1); |
40 by (rtac compatibility_consequence4 1); |
41 by (REPEAT (asm_full_simp_tac (!simpset |
41 by (REPEAT (asm_full_simp_tac (simpset() |
42 addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
42 addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
43 qed"Filter_actAisFilter_extA2"; |
43 qed"Filter_actAisFilter_extA2"; |
44 |
44 |
45 |
45 |
46 (* -------------------------------------------------------------------------- *) |
46 (* -------------------------------------------------------------------------- *) |
56 \ compatible A1 B1; compatible A2 B2; \ |
56 \ compatible A1 B1; compatible A2 B2; \ |
57 \ A1 =<| A2; \ |
57 \ A1 =<| A2; \ |
58 \ B1 =<| B2 |] \ |
58 \ B1 =<| B2 |] \ |
59 \ ==> (A1 || B1) =<| (A2 || B2)"; |
59 \ ==> (A1 || B1) =<| (A2 || B2)"; |
60 |
60 |
61 by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def]) 1); |
61 by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def]) 1); |
62 by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1); |
62 by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1); |
63 by (forw_inst_tac [("A2","A2")] (compat_commute RS iffD1) 1); |
63 by (forw_inst_tac [("A2","A2")] (compat_commute RS iffD1) 1); |
64 by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def, |
64 by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def, |
65 inputs_of_par,outputs_of_par,externals_of_par]) 1); |
65 inputs_of_par,outputs_of_par,externals_of_par]) 1); |
66 by (safe_tac set_cs); |
66 by (safe_tac set_cs); |
67 by (asm_full_simp_tac (!simpset addsimps [compositionality_tr]) 1); |
67 by (asm_full_simp_tac (simpset() addsimps [compositionality_tr]) 1); |
68 by (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2" 1); |
68 by (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2" 1); |
69 by (asm_full_simp_tac (!simpset addsimps [externals_def]) 2); |
69 by (asm_full_simp_tac (simpset() addsimps [externals_def]) 2); |
70 by (REPEAT (etac conjE 1)); |
70 by (REPEAT (etac conjE 1)); |
71 (* rewrite with proven subgoal *) |
71 (* rewrite with proven subgoal *) |
72 by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1); |
72 by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1); |
73 by (safe_tac set_cs); |
73 by (safe_tac set_cs); |
74 |
74 |
75 (* 2 goals, the 3rd has been solved automatically *) |
75 (* 2 goals, the 3rd has been solved automatically *) |
76 (* 1: Filter A2 x : traces A2 *) |
76 (* 1: Filter A2 x : traces A2 *) |
77 by (dres_inst_tac [("A","traces A1")] subsetD 1); |
77 by (dres_inst_tac [("A","traces A1")] subsetD 1); |
78 by (assume_tac 1); |
78 by (assume_tac 1); |
79 by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA]) 1); |
79 by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA]) 1); |
80 (* 2: Filter B2 x : traces B2 *) |
80 (* 2: Filter B2 x : traces B2 *) |
81 by (dres_inst_tac [("A","traces B1")] subsetD 1); |
81 by (dres_inst_tac [("A","traces B1")] subsetD 1); |
82 by (assume_tac 1); |
82 by (assume_tac 1); |
83 by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA2]) 1); |
83 by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA2]) 1); |
84 qed"compositionality"; |
84 qed"compositionality"; |
85 |
85 |
86 |
86 |
87 |
87 |
88 |
88 |