1 (* Title: HOLCF/IOA/meta_theory/Compositionality.ML |
1 (* Title: HOLCF/IOA/meta_theory/Compositionality.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf Müller |
3 Author: Olaf Müller |
4 |
4 *) |
5 Compositionality of I/O automata |
|
6 *) |
|
7 |
|
8 |
|
9 |
5 |
10 Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA"; |
6 Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA"; |
11 by Auto_tac; |
7 by Auto_tac; |
12 qed"compatibility_consequence3"; |
8 qed"compatibility_consequence3"; |
13 |
9 |
14 |
10 |
15 Goal |
11 Goal |
16 "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \ |
12 "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \ |
17 \ Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"; |
13 \ Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"; |
18 by (rtac ForallPFilterQR 1); |
14 by (rtac ForallPFilterQR 1); |
19 (* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *) |
15 (* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *) |
20 by (assume_tac 2); |
16 by (assume_tac 2); |
21 by (rtac compatibility_consequence3 1); |
17 by (rtac compatibility_consequence3 1); |
22 by (REPEAT (asm_full_simp_tac (simpset() |
18 by (REPEAT (asm_full_simp_tac (simpset() |
23 addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
19 addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
24 qed"Filter_actAisFilter_extA"; |
20 qed"Filter_actAisFilter_extA"; |
25 |
21 |
26 |
22 |
27 (* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *) |
23 (* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *) |
33 Goal "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \ |
29 Goal "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \ |
34 \ Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"; |
30 \ Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"; |
35 by (rtac ForallPFilterQR 1); |
31 by (rtac ForallPFilterQR 1); |
36 by (assume_tac 2); |
32 by (assume_tac 2); |
37 by (rtac compatibility_consequence4 1); |
33 by (rtac compatibility_consequence4 1); |
38 by (REPEAT (asm_full_simp_tac (simpset() |
34 by (REPEAT (asm_full_simp_tac (simpset() |
39 addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
35 addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
40 qed"Filter_actAisFilter_extA2"; |
36 qed"Filter_actAisFilter_extA2"; |
41 |
37 |
42 |
38 |
43 (* -------------------------------------------------------------------------- *) |
39 (* -------------------------------------------------------------------------- *) |
76 (* 2: Filter B2 x : traces B2 *) |
72 (* 2: Filter B2 x : traces B2 *) |
77 by (dres_inst_tac [("A","traces B1")] subsetD 1); |
73 by (dres_inst_tac [("A","traces B1")] subsetD 1); |
78 by (assume_tac 1); |
74 by (assume_tac 1); |
79 by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA2]) 1); |
75 by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA2]) 1); |
80 qed"compositionality"; |
76 qed"compositionality"; |
81 |
|
82 |
|
83 |
|
84 |
|