42151
|
1 |
(* Title: HOL/HOLCF/IOA/meta_theory/Compositionality.thy
|
40945
|
2 |
Author: Olaf Müller
|
17233
|
3 |
*)
|
3071
|
4 |
|
58880
|
5 |
section {* Compositionality of I/O automata *}
|
17233
|
6 |
theory Compositionality
|
|
7 |
imports CompoTraces
|
|
8 |
begin
|
3071
|
9 |
|
19741
|
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)
|
26359
|
54 |
apply auto
|
19741
|
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)
|
26359
|
62 |
apply auto
|
19741
|
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 |
|
17233
|
75 |
end
|