author | wenzelm |
Fri, 02 Sep 2005 17:23:59 +0200 | |
changeset 17233 | 41eee2e7b465 |
parent 14981 | e73f8140af78 |
child 19360 | f47412f922ab |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Compositionality.ML |
3275 | 2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
17233 | 4 |
*) |
3275 | 5 |
|
6161 | 6 |
Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA"; |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset
|
7 |
by Auto_tac; |
3275 | 8 |
qed"compatibility_consequence3"; |
9 |
||
10 |
||
17233 | 11 |
Goal |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
12 |
"!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \ |
10835 | 13 |
\ Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"; |
3457 | 14 |
by (rtac ForallPFilterQR 1); |
10835 | 15 |
(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *) |
3457 | 16 |
by (assume_tac 2); |
17 |
by (rtac compatibility_consequence3 1); |
|
17233 | 18 |
by (REPEAT (asm_full_simp_tac (simpset() |
3275 | 19 |
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
20 |
qed"Filter_actAisFilter_extA"; |
|
21 |
||
22 |
||
5976 | 23 |
(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *) |
3275 | 24 |
|
6161 | 25 |
Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA"; |
4477
b3e5857d8d99
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
paulson
parents:
4473
diff
changeset
|
26 |
by Auto_tac; |
3275 | 27 |
qed"compatibility_consequence4"; |
28 |
||
6161 | 29 |
Goal "[| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \ |
10835 | 30 |
\ Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr"; |
3457 | 31 |
by (rtac ForallPFilterQR 1); |
32 |
by (assume_tac 2); |
|
33 |
by (rtac compatibility_consequence4 1); |
|
17233 | 34 |
by (REPEAT (asm_full_simp_tac (simpset() |
3275 | 35 |
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1)); |
36 |
qed"Filter_actAisFilter_extA2"; |
|
37 |
||
38 |
||
39 |
(* -------------------------------------------------------------------------- *) |
|
40 |
section " Main Compositionality Theorem "; |
|
41 |
(* -------------------------------------------------------------------------- *) |
|
42 |
||
43 |
||
44 |
||
6161 | 45 |
Goal "[| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\ |
3521 | 46 |
\ is_asig_of A1; is_asig_of A2; \ |
47 |
\ is_asig_of B1; is_asig_of B2; \ |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
3275
diff
changeset
|
48 |
\ compatible A1 B1; compatible A2 B2; \ |
3071 | 49 |
\ A1 =<| A2; \ |
50 |
\ B1 =<| B2 |] \ |
|
51 |
\ ==> (A1 || B1) =<| (A2 || B2)"; |
|
3275 | 52 |
|
4098 | 53 |
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def]) 1); |
4473 | 54 |
by (forw_inst_tac [("A1","A1")] (compat_commute RS iffD1) 1); |
55 |
by (forw_inst_tac [("A1","A2")] (compat_commute RS iffD1) 1); |
|
4098 | 56 |
by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def, |
3275 | 57 |
inputs_of_par,outputs_of_par,externals_of_par]) 1); |
58 |
by (safe_tac set_cs); |
|
4098 | 59 |
by (asm_full_simp_tac (simpset() addsimps [compositionality_tr]) 1); |
3275 | 60 |
by (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2" 1); |
4098 | 61 |
by (asm_full_simp_tac (simpset() addsimps [externals_def]) 2); |
3275 | 62 |
by (REPEAT (etac conjE 1)); |
63 |
(* rewrite with proven subgoal *) |
|
4098 | 64 |
by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1); |
3275 | 65 |
by (safe_tac set_cs); |
66 |
||
67 |
(* 2 goals, the 3rd has been solved automatically *) |
|
68 |
(* 1: Filter A2 x : traces A2 *) |
|
69 |
by (dres_inst_tac [("A","traces A1")] subsetD 1); |
|
3457 | 70 |
by (assume_tac 1); |
4098 | 71 |
by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA]) 1); |
3275 | 72 |
(* 2: Filter B2 x : traces B2 *) |
73 |
by (dres_inst_tac [("A","traces B1")] subsetD 1); |
|
3457 | 74 |
by (assume_tac 1); |
4098 | 75 |
by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA2]) 1); |
3275 | 76 |
qed"compositionality"; |