--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML Fri Sep 02 15:54:47 2005 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML Fri Sep 02 17:23:59 2005 +0200
@@ -1,25 +1,21 @@
(* Title: HOLCF/IOA/meta_theory/Compositionality.ML
ID: $Id$
Author: Olaf Müller
-
-Compositionality of I/O automata
-*)
-
-
+*)
Goal "[|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
by Auto_tac;
qed"compatibility_consequence3";
-Goal
+Goal
"!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
\ Filter (%a. a: act A)$tr= Filter (%a. a: ext A)$tr";
by (rtac ForallPFilterQR 1);
(* i.e.: [| (! x. P x --> (Q x = R x)) ; Forall P tr |] ==> Filter Q$tr = Filter R$tr *)
by (assume_tac 2);
by (rtac compatibility_consequence3 1);
-by (REPEAT (asm_full_simp_tac (simpset()
+by (REPEAT (asm_full_simp_tac (simpset()
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
qed"Filter_actAisFilter_extA";
@@ -35,7 +31,7 @@
by (rtac ForallPFilterQR 1);
by (assume_tac 2);
by (rtac compatibility_consequence4 1);
-by (REPEAT (asm_full_simp_tac (simpset()
+by (REPEAT (asm_full_simp_tac (simpset()
addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
qed"Filter_actAisFilter_extA2";
@@ -78,7 +74,3 @@
by (assume_tac 1);
by (asm_full_simp_tac (simpset() addsimps [Filter_actAisFilter_extA2]) 1);
qed"compositionality";
-
-
-
-