author | mueller |
Thu, 12 Jun 1997 16:47:15 +0200 | |
changeset 3433 | 2de17c994071 |
parent 3275 | 3f53f2c876f4 |
child 3457 | a8ab7c64817c |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Compositionality.ML |
3275 | 2 |
ID: $Id$ |
3071 | 3 |
Author: Olaf M"uller |
4 |
Copyright 1997 TU Muenchen |
|
5 |
||
6 |
Compositionality of I/O automata |
|
7 |
*) |
|
8 |
||
9 |
||
3275 | 10 |
|
11 |
goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA"; |
|
12 |
auto(); |
|
13 |
qed"compatibility_consequence3"; |
|
14 |
||
15 |
||
16 |
goal thy |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
17 |
"!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \ |
3275 | 18 |
\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
19 |
br ForallPFilterQR 1; |
|
20 |
ba 2; |
|
21 |
br compatibility_consequence3 1; |
|
22 |
by (REPEAT (asm_full_simp_tac (!simpset |
|
23 |
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
|
24 |
qed"Filter_actAisFilter_extA"; |
|
25 |
||
26 |
||
27 |
(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) |
|
28 |
or even better A||B= B||A, FIX *) |
|
29 |
||
30 |
goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA"; |
|
31 |
auto(); |
|
32 |
qed"compatibility_consequence4"; |
|
33 |
||
34 |
goal thy |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
35 |
"!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \ |
3275 | 36 |
\ Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr"; |
37 |
br ForallPFilterQR 1; |
|
38 |
ba 2; |
|
39 |
br compatibility_consequence4 1; |
|
40 |
by (REPEAT (asm_full_simp_tac (!simpset |
|
41 |
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
|
42 |
qed"Filter_actAisFilter_extA2"; |
|
43 |
||
44 |
||
45 |
(* -------------------------------------------------------------------------- *) |
|
46 |
section " Main Compositionality Theorem "; |
|
47 |
(* -------------------------------------------------------------------------- *) |
|
48 |
||
49 |
||
50 |
||
3071 | 51 |
goal thy "!! A1 A2 B1 B2. \ |
3275 | 52 |
\ [| IOA A1; IOA A2; IOA B1; IOA B2;\ |
53 |
\ is_asig (asig_of A1); is_asig (asig_of A2); \ |
|
3071 | 54 |
\ is_asig (asig_of B1); is_asig (asig_of B2); \ |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
55 |
\ compatible A1 B1; compatible A2 B2; \ |
3071 | 56 |
\ A1 =<| A2; \ |
57 |
\ B1 =<| B2 |] \ |
|
58 |
\ ==> (A1 || B1) =<| (A2 || B2)"; |
|
3275 | 59 |
|
60 |
by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1); |
|
61 |
by (forw_inst_tac [("A2","A2")] (compat_commute RS iffD1) 1); |
|
3071 | 62 |
by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def, |
3275 | 63 |
inputs_of_par,outputs_of_par,externals_of_par]) 1); |
64 |
by (safe_tac set_cs); |
|
65 |
by (asm_full_simp_tac (!simpset addsimps [compositionality_tr]) 1); |
|
66 |
by (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2" 1); |
|
67 |
by (asm_full_simp_tac (!simpset addsimps [externals_def]) 2); |
|
68 |
by (REPEAT (etac conjE 1)); |
|
69 |
(* rewrite with proven subgoal *) |
|
70 |
by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1); |
|
71 |
by (safe_tac set_cs); |
|
72 |
||
73 |
(* 2 goals, the 3rd has been solved automatically *) |
|
74 |
(* 1: Filter A2 x : traces A2 *) |
|
75 |
by (dres_inst_tac [("A","traces A1")] subsetD 1); |
|
76 |
ba 1; |
|
77 |
by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA]) 1); |
|
78 |
(* 2: Filter B2 x : traces B2 *) |
|
79 |
by (dres_inst_tac [("A","traces B1")] subsetD 1); |
|
80 |
ba 1; |
|
81 |
by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA2]) 1); |
|
82 |
qed"compositionality"; |
|
3071 | 83 |
|
84 |
||
85 |
||
3275 | 86 |