1 (* Title: HOLCF/IOA/meta_theory/Compositionality.thy |
|
2 Author: Olaf Müller |
|
3 *) |
|
4 |
|
5 header {* Compositionality of I/O automata *} |
|
6 theory Compositionality |
|
7 imports CompoTraces |
|
8 begin |
|
9 |
|
10 lemma compatibility_consequence3: "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA" |
|
11 apply auto |
|
12 done |
|
13 |
|
14 |
|
15 lemma Filter_actAisFilter_extA: |
|
16 "!! 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" |
|
18 apply (rule ForallPFilterQR) |
|
19 (* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *) |
|
20 prefer 2 apply (assumption) |
|
21 apply (rule compatibility_consequence3) |
|
22 apply (simp_all add: ext_is_act ext1_ext2_is_not_act1) |
|
23 done |
|
24 |
|
25 |
|
26 (* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *) |
|
27 |
|
28 lemma compatibility_consequence4: "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA" |
|
29 apply auto |
|
30 done |
|
31 |
|
32 lemma Filter_actAisFilter_extA2: "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> |
|
33 Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr" |
|
34 apply (rule ForallPFilterQR) |
|
35 prefer 2 apply (assumption) |
|
36 apply (rule compatibility_consequence4) |
|
37 apply (simp_all add: ext_is_act ext1_ext2_is_not_act1) |
|
38 done |
|
39 |
|
40 |
|
41 subsection " Main Compositionality Theorem " |
|
42 |
|
43 lemma compositionality: "[| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2; |
|
44 is_asig_of A1; is_asig_of A2; |
|
45 is_asig_of B1; is_asig_of B2; |
|
46 compatible A1 B1; compatible A2 B2; |
|
47 A1 =<| A2; |
|
48 B1 =<| B2 |] |
|
49 ==> (A1 || B1) =<| (A2 || B2)" |
|
50 apply (simp add: is_asig_of_def) |
|
51 apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1]) |
|
52 apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1]) |
|
53 apply (simp add: ioa_implements_def inputs_of_par outputs_of_par externals_of_par) |
|
54 apply auto |
|
55 apply (simp add: compositionality_tr) |
|
56 apply (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2") |
|
57 prefer 2 |
|
58 apply (simp add: externals_def) |
|
59 apply (erule conjE)+ |
|
60 (* rewrite with proven subgoal *) |
|
61 apply (simp add: externals_of_par) |
|
62 apply auto |
|
63 |
|
64 (* 2 goals, the 3rd has been solved automatically *) |
|
65 (* 1: Filter A2 x : traces A2 *) |
|
66 apply (drule_tac A = "traces A1" in subsetD) |
|
67 apply assumption |
|
68 apply (simp add: Filter_actAisFilter_extA) |
|
69 (* 2: Filter B2 x : traces B2 *) |
|
70 apply (drule_tac A = "traces B1" in subsetD) |
|
71 apply assumption |
|
72 apply (simp add: Filter_actAisFilter_extA2) |
|
73 done |
|
74 |
|
75 end |
|