src/HOLCF/IOA/meta_theory/Compositionality.ML

--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Compositionality.ML
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1997  TU Muenchen
 
@@ -7,17 +7,80 @@
 *) 
 
 
+
+goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
+auto();
+qed"compatibility_consequence3";
+
+
+goal thy 
+"!! A B. [| compat_ioas A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
+\           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
+br ForallPFilterQR 1;
+ba 2;
+br compatibility_consequence3 1;
+by (REPEAT (asm_full_simp_tac (!simpset 
+                  addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
+qed"Filter_actAisFilter_extA";
+
+
+(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A)
+    or even better A||B= B||A, FIX *)
+
+goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
+auto();
+qed"compatibility_consequence4";
+
+goal thy 
+"!! A B. [| compat_ioas A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
+\           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
+br ForallPFilterQR 1;
+ba 2;
+br compatibility_consequence4 1;
+by (REPEAT (asm_full_simp_tac (!simpset 
+                  addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
+qed"Filter_actAisFilter_extA2";
+
+
+(* -------------------------------------------------------------------------- *)
+                     section " Main Compositionality Theorem ";
+(* -------------------------------------------------------------------------- *)
+
+
+
 goal thy "!! A1 A2 B1 B2. \
-\         [| is_asig (asig_of A1); is_asig (asig_of A2); \
+\         [| IOA A1; IOA A2; IOA B1; IOA B2;\
+\            is_asig (asig_of A1); is_asig (asig_of A2); \
 \            is_asig (asig_of B1); is_asig (asig_of B2); \
-\            compat_ioas A1 B1; compat_ioas B1 A1; compat_ioas A2 B2; compat_ioas B2 A2; \
+\            compat_ioas A1 B1; compat_ioas A2 B2; \
 \            A1 =<| A2; \
 \            B1 =<| B2 |] \
 \        ==> (A1 || B1) =<| (A2 || B2)";
+
+by (forw_inst_tac [("A2","A1")] (compat_commute RS iffD1) 1);
+by (forw_inst_tac [("A2","A2")] (compat_commute RS iffD1) 1);
 by (asm_full_simp_tac (!simpset addsimps [ioa_implements_def,
-                               inputs_of_par,outputs_of_par]) 1);
+          inputs_of_par,outputs_of_par,externals_of_par]) 1);
+by (safe_tac set_cs);
+by (asm_full_simp_tac (!simpset addsimps [compositionality_tr]) 1);
+by (subgoal_tac "ext A1 = ext A2 & ext B1 = ext B2" 1);
+by (asm_full_simp_tac (!simpset addsimps [externals_def]) 2);
+by (REPEAT (etac conjE 1));
+(* rewrite with proven subgoal *)
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
+by (safe_tac set_cs);
+
+(* 2 goals, the 3rd has been solved automatically *)
+(* 1: Filter A2 x : traces A2 *)
+by (dres_inst_tac [("A","traces A1")] subsetD 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA]) 1);
+(* 2: Filter B2 x : traces B2 *)
+by (dres_inst_tac [("A","traces B1")] subsetD 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA2]) 1);
+qed"compositionality";
 
 
-by (safe_tac set_cs);
-by (asm_full_simp_tac (!simpset addsimps [compotraces]) 1);
 
+