# HG changeset patch
# User mueller
# Date 864220132 -7200
# Node ID 3f53f2c876f40fb2659d85e9b19814248227a2e1
# Parent  70939b0fadfbc20af690e2ba9c4feb550c8c94ff
changes for release 94-8

diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Asig.ML
--- a/src/HOLCF/IOA/meta_theory/Asig.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Asig.ML	Wed May 21 15:08:52 1997 +0200
@@ -31,8 +31,14 @@
 by (best_tac (set_cs addEs [equalityCE]) 1);
 qed"not_ext_is_int";
 
+goal thy "!!S. is_asig S ==> (x~:externals S) = (x: internals S | x~:actions S)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,is_asig_def,externals_def]) 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"not_ext_is_int_or_not_act";
+
 goalw thy  [externals_def,actions_def,is_asig_def]
  "!! x. [| is_asig (S); x:internals S |] ==> x~:externals S";
 by (Asm_full_simp_tac 1);
 by (best_tac (set_cs addEs [equalityCE]) 1);
-qed"int_is_not_ext";
\ No newline at end of file
+qed"int_is_not_ext";
+
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Asig.thy
--- a/src/HOLCF/IOA/meta_theory/Asig.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Asig.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,7 +1,7 @@
 (*  Title:      HOL/IOA/meta_theory/Asig.thy
     ID:         $Id$
-    Author:     Tobias Nipkow & Konrad Slind
-    Copyright   1994  TU Muenchen
+    Author:     Olaf Mueller, Tobias Nipkow & Konrad Slind
+    Copyright   1994, 1996 TU Muenchen
 
 Action signatures
 *)
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Automata.ML
-    ID:         $$
+    ID:         $Id$
     Author:     Olaf Mueller, Tobias Nipkow, Konrad Slind
     Copyright   1994, 1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Automata.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller, Konrad Slind, Tobias Nipkow
     Copyright   1995, 1996  TU Muenchen
 
@@ -82,8 +82,8 @@
 
 state_trans_def
   "state_trans asig R == 
-    (!triple. triple:R --> fst(snd(triple)):actions(asig)) & 
-    (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))"
+    (!triple. triple:R --> fst(snd(triple)):actions(asig))"
+(* & (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" *)
 
 
 asig_of_def   "asig_of == fst"
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.ML
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.ML
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed May 21 15:08:52 1997 +0200
@@ -2,27 +2,20 @@
     ID:		$Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
-
+ 
 Compositionality on Trace level.
 *) 
 
-(* FIX:Proof and add in Sequence.ML *)
-Addsimps [Finite_Conc];
-
-
-(*
-Addsimps [forall_cons];
-
-Addsimps [(* LastActExtsmall1, LastActExtsmall2, looping !! *) ext_and_act];
-*)
 
 fun thin_tac' j =
   rotate_tac (j - 1) THEN'
-  etac thin_rl THEN'
+  etac thin_rl THEN' 
   rotate_tac (~ (j - 1));
 
 
 
+
+
 (* ---------------------------------------------------------------- *)
                    section "mksch rewrite rules";
 (* ---------------------------------------------------------------- *)
@@ -122,7 +115,7 @@
 
 
 (* ---------------------------------------------------------------------------- *)
-(*                  Specifics for "==>"                                         *)
+                      section"Lemmata for ==>";                      
 (* ---------------------------------------------------------------------------- *)
 
 (* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of 
@@ -143,27 +136,22 @@
 qed"compatibility_consequence2";
 
 
-goal thy "!!x. [| x = nil;  y = z|] ==> (x @@ y) = z";
-auto();
-qed"nil_and_tconc";
-
-(* FIX: should be easy to get out of lemma before *)
-goal thy "!!x. [| x = nil;  f`y = f`z|] ==> f`(x @@ y) = f`z";
-auto();
-qed"nil_and_tconc_f";
-
-(* FIX: should be something like subst: or better improve simp_tac so that these lemmat are
-        superfluid *)
-goal thy "!!x. [| x1 = x2;  f`(x2 @@ y) = f`z|] ==> f`(x1 @@ y) = f`z";
-auto();
-qed"tconcf";
+(* ---------------------------------------------------------------------------- *)
+                      section"Lemmata for <==";                      
+(* ---------------------------------------------------------------------------- *)
 
 
-
-(*
+(* Lemma for substitution of looping assumption in another specific assumption *) 
+val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
+by (cut_facts_tac [p1] 1);
+be (p2 RS subst) 1;
+qed"subst_lemma1";
 
-
-(* -------------------------------------------------------------------------------- *)
+(* Lemma for substitution of looping assumption in another specific assumption *) 
+val [p1,p2] = goal thy "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g";
+by (cut_facts_tac [p1] 1);
+be (p2 RS subst) 1;
+qed"subst_lemma2";
 
 
 goal thy "!!A B. compat_ioas A B ==> \
@@ -177,34 +165,39 @@
 (* a:A, a:B *)
 by (Asm_full_simp_tac 1);
 br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
 br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
 (* a:A,a~:B *)
 by (Asm_full_simp_tac 1);
 br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
 by (case_tac "a:act B" 1);
 (* a~:A, a:B *)
 by (Asm_full_simp_tac 1);
 br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
 (* a~:A,a~:B *)
 auto();
-qed"ForallAorB_mksch";
+qed"ForallAorB_mksch1";
 
+bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp);
 
-goal thy "!!A B. compat_ioas A B ==> \
+goal thy "!!A B. compat_ioas B A  ==> \
 \   ! schA schB.  (Forall (%x. x:act B & x~:act A) tr \
 \   --> Forall (%x. x:act B & x~:act A) (mksch A B`tr`schA`schB))";
 
 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
 by (safe_tac set_cs);
 br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
+                            intA_is_not_actB,int_is_act]) 1);
 qed"ForallBnA_mksch";
 
-goal thy "!!A B. compat_ioas B A ==> \
+bind_thm ("ForallBnAmksch",ForallBnA_mksch RS spec RS spec RS mp);
+
+
+goal thy "!!A B. compat_ioas A B ==> \
 \   ! schA schB.  (Forall (%x. x:act A & x~:act B) tr \
 \   --> Forall (%x. x:act A & x~:act B) (mksch A B`tr`schA`schB))";
 
@@ -212,15 +205,19 @@
 by (safe_tac set_cs);
 by (Asm_full_simp_tac 1);
 br (Forall_Conc_impl RS mp) 1;
-by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intAisnotextB,int_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
+                       intA_is_not_actB,int_is_act]) 1);
 qed"ForallAnB_mksch";
 
+bind_thm ("ForallAnBmksch",ForallAnB_mksch RS spec RS spec RS mp);
+
 
-(* ------------------------------------------------------------------------------------ *)
+(* safe-tac makes too many case distinctions with this lemma in the next proof *)
+Delsimps [FiniteConc];
 
-(*
-goal thy "!! tr. Finite tr ==> \
-\   ! x y. Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
+goal thy "!! tr. [| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
+\   ! x y. Forall (%x.x:act A) x & Forall (%x.x:act B) y & \
+\          Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr & \
 \          Filter (%a. a:ext B)`y = Filter (%a. a:act B)`tr &\
 \          Forall (%x. x:ext (A||B)) tr \
 \          --> Finite (mksch A B`tr`x`y)";
@@ -230,55 +227,188 @@
 (* main case *)
 by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
 by (safe_tac set_cs);
-by (Asm_full_simp_tac 1);
+
+(* a: act A; a: act B *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+back();
+by (REPEAT (etac conjE 1));
+(* Finite (tw iA x) and Finite (tw iB y) *)
+by (asm_full_simp_tac (!simpset addsimps 
+          [not_ext_is_int_or_not_act,FiniteConc]) 1);
+(* now for conclusion IH applicable, but assumptions have to be transformed *)
+by (dres_inst_tac [("x","x"),
+                   ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
+ba 1;
+by (dres_inst_tac [("x","y"),
+                   ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
+ba 1;
+(* IH *)
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+                   FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
+
+(* a: act B; a~: act A *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
 
+by (REPEAT (etac conjE 1));
+(* Finite (tw iB y) *)
+by (asm_full_simp_tac (!simpset addsimps 
+          [not_ext_is_int_or_not_act,FiniteConc]) 1);
+(* now for conclusion IH applicable, but assumptions have to be transformed *)
+by (dres_inst_tac [("x","y"),
+                   ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
+ba 1;
+(* IH *)
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+                   FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
 
+(* a~: act B; a: act A *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
 
+by (REPEAT (etac conjE 1));
+(* Finite (tw iA x) *)
+by (asm_full_simp_tac (!simpset addsimps 
+          [not_ext_is_int_or_not_act,FiniteConc]) 1);
+(* now for conclusion IH applicable, but assumptions have to be transformed *)
+by (dres_inst_tac [("x","x"),
+                   ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
+ba 1;
+(* IH *)
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+                   FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
+
+(* a~: act B; a~: act A *)
+by (fast_tac (!claset addSIs [ext_is_act] 
+                      addss (!simpset addsimps [externals_of_par]) ) 1);
 qed"FiniteL_mksch";
 
-goal thy " !!bs. Finite bs ==>  \
-\ Forall (%x. x:act B & x~:act A) bs &\
-\ Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
-\ --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
-\                Forall (%x. x:act B & x~:act A) y1 & \
-\                Finite y1 & y = (y1 @@ y2) & \
-\                Filter (%a. a:ext B)`y1 = bs)";
+bind_thm("FiniteL_mksch1", FiniteL_mksch RS spec RS spec RS mp);
+ 
+Addsimps [FiniteConc];
+
+
+(* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
+Delsimps [FilterConc]; 
+
+goal thy " !!bs. [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compat_ioas A B|] ==>  \
+\! y.Forall (%x.x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
+\    Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) \
+\    --> (? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) & \
+\                   Forall (%x. x:act B & x~:act A) y1 & \
+\                   Finite y1 & y = (y1 @@ y2) & \
+\                   Filter (%a. a:ext B)`y1 = bs)";
+by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
 be Seq_Finite_ind  1;
+by (REPEAT (rtac allI 1));
 by (rtac impI 1);
 by (res_inst_tac [("x","nil")] exI 1);
 by (res_inst_tac [("x","y")] exI 1);
 by (Asm_full_simp_tac 1);
 (* main case *)
+by (REPEAT (rtac allI 1));
 by (rtac impI 1);
 by (Asm_full_simp_tac 1);
 by (REPEAT (etac conjE 1));
+by (Asm_full_simp_tac 1);
+(* divide_Seq on s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+(* transform assumption f eB y = f B (s@z) *)
+by (dres_inst_tac [("x","y"),
+                   ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
+ba 1;
+Addsimps [FilterConc]; 
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
+(* apply IH *)
+by (eres_inst_tac [("x","TL`(Dropwhile (%a.a:int B)`y)")] allE 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+by (Asm_full_simp_tac 1); 
+(* for replacing IH in conclusion *)
+by (rotate_tac ~2 1); 
+by (Asm_full_simp_tac 1); 
+(* instantiate y1a and y2a *)
+by (res_inst_tac [("x","Takewhile (%a.a:int B)`y @@ a>>y1")] exI 1);
+by (res_inst_tac [("x","y2")] exI 1);
+(* elminate all obligations up to two depending on Conc_assoc *)
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
+             int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); 
+by (simp_tac (!simpset addsimps [Conc_assoc]) 1); 
+qed"reduceA_mksch1";
+
+bind_thm("reduceA_mksch",conjI RSN (6,conjI RSN (5,reduceA_mksch1 RS spec RS mp)));
+
+
+
+(* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
+Delsimps [FilterConc]; 
+
+
+goal thy " !!as. [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compat_ioas A B|] ==>  \
+\! x.Forall (%x.x:act A) x & Forall (%x. x:act A & x~:act B) as &\
+\    Filter (%a. a:ext A)`x = Filter (%a. a:act A)`(as @@ z) \
+\    --> (? x1 x2.  (mksch A B`(as @@ z)`x`y) = (x1 @@ (mksch A B`z`x2`y)) & \
+\                   Forall (%x. x:act A & x~:act B) x1 & \
+\                   Finite x1 & x = (x1 @@ x2) & \
+\                   Filter (%a. a:ext A)`x1 = as)";
+by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
+be Seq_Finite_ind  1;
+by (REPEAT (rtac allI 1));
+by (rtac impI 1);
+by (res_inst_tac [("x","nil")] exI 1);
+by (res_inst_tac [("x","x")] exI 1);
+by (Asm_full_simp_tac 1);
+(* main case *)
+by (REPEAT (rtac allI 1));
+by (rtac impI 1);
+by (Asm_full_simp_tac 1);
+by (REPEAT (etac conjE 1));
+by (Asm_full_simp_tac 1);
+(* divide_Seq on s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+(* transform assumption f eA x = f A (s@z) *)
+by (dres_inst_tac [("x","x"),
+                   ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
+ba 1;
+Addsimps [FilterConc]; 
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
+(* apply IH *)
+by (eres_inst_tac [("x","TL`(Dropwhile (%a.a:int A)`x)")] allE 1);
+by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile])1);
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+by (Asm_full_simp_tac 1); 
+(* for replacing IH in conclusion *)
+by (rotate_tac ~2 1); 
+by (Asm_full_simp_tac 1); 
+(* instantiate y1a and y2a *)
+by (res_inst_tac [("x","Takewhile (%a.a:int A)`x @@ a>>x1")] exI 1);
+by (res_inst_tac [("x","x2")] exI 1);
+(* elminate all obligations up to two depending on Conc_assoc *)
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, intA_is_not_actB,
+             int_is_act,FilterPTakewhileQnil,int_is_not_ext]) 1); 
+by (simp_tac (!simpset addsimps [Conc_assoc]) 1); 
+qed"reduceB_mksch1";
+
+bind_thm("reduceB_mksch",conjI RSN (6,conjI RSN (5,reduceB_mksch1 RS spec RS mp)));
 
 
 
 
 
-qed"reduce_mksch";
-
-*)
-
-
-(* Lemma for substitution of looping assumption in another specific assumption *) 
-val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
-by (cut_facts_tac [p1] 1);
-be (p2 RS subst) 1;
-qed"subst_lemma1";
-
-
-
 
  
-(*---------------------------------------------------------------------------
-    Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr
-                             structural induction
-  --------------------------------------------------------------------------- *)
+(*------------------------------------------------------------------------------------- *)
+ section"Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr";
+(*                             structural induction
+  ------------------------------------------------------------------------------------- *)
 
-goal thy "! schA schB. compat_ioas A B & compat_ioas B A &\
-\ is_asig(asig_of A) & is_asig(asig_of B) &\
+goal thy 
+"!! A B. [| compat_ioas A B; compat_ioas B A;\
+\           is_asig(asig_of A); is_asig(asig_of B) |] ==> \
+\ ! schA schB. Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
 \ Forall (%x.x:ext (A||B)) tr & \
 \ Filter (%a.a:act A)`tr << Filter (%a.a:ext A)`schA &\
 \ Filter (%a.a:act B)`tr << Filter (%a.a:ext B)`schB  \
@@ -296,373 +426,544 @@
 by (forward_tac [divide_Seq] 1);
 back();
 by (REPEAT (etac conjE 1));
-(* filtering internals of A is nil *)
-br nil_and_tconc 1;
-br FilterPTakewhileQnil 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
-             intA_is_not_extB,int_is_not_ext]) 1);
-(* end*)
-(* filtering internals of B is nil *)
-(* FIX: should be done by simp_tac and claset combined until end*)
-br nil_and_tconc 1;
-br FilterPTakewhileQnil 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
-             intA_is_not_extB,int_is_not_ext]) 1);
-(* end*)
+(* filtering internals of A in schA and of B in schB is nil *)
+by (asm_full_simp_tac (!simpset addsimps 
+          [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
+           externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
 (* conclusion of IH ok, but assumptions of IH have to be transformed *)
 by (dres_inst_tac [("x","schA")] subst_lemma1 1);
 ba 1;
 by (dres_inst_tac [("x","schB")] subst_lemma1 1);
 ba 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
-
+(* IH *)
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+                   FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
 (* Case a:B, a~:A *)
 
 by (forward_tac [divide_Seq] 1);
 by (REPEAT (etac conjE 1));
 (* filtering internals of A is nil *)
-(* FIX: should be done by simp_tac and claset combined until end*)
-br nil_and_tconc 1;
-br FilterPTakewhileQnil 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
-             intA_is_not_extB,int_is_not_ext]) 1);
-(* end*)
+by (asm_full_simp_tac (!simpset addsimps 
+          [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
+           externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
 by (dres_inst_tac [("x","schB")] subst_lemma1 1);
 back();
 ba 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
-
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
 (* Case a:A, a~:B *)
 
 by (forward_tac [divide_Seq] 1);
 by (REPEAT (etac conjE 1));
 (* filtering internals of A is nil *)
-(* FIX: should be done by simp_tac and claset combined until end*)
-br nil_and_tconc 1;
-br FilterPTakewhileQnil 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX]) 1);
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par,
-             intA_is_not_extB,int_is_not_ext]) 1);
-(* end*)
+by (asm_full_simp_tac (!simpset addsimps 
+          [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
+           externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
 by (dres_inst_tac [("x","schA")] subst_lemma1 1);
 ba 1;
-by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_FIX,FilterPTakewhileQnil]) 1);
-
+by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
+                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
 (* Case a~:A, a~:B *)
 
 by (fast_tac (!claset addSIs [ext_is_act] 
                       addss (!simpset addsimps [externals_of_par]) ) 1);
-qed"filterA_mksch_is_tr";
-
+qed"FilterA_mksch_is_tr";
 
 
 
-goal thy "!!x y. [|x=UU; y=UU|] ==> x=y";
-auto();
-qed"both_UU"; 
-
-goal thy "!!x y. [|x=nil; y=nil|] ==> x=y";
-auto();
-qed"both_nil";
+(*--------------------------------------------------------------------------- *)
 
-
-(* FIX: does it exist already? *)
-(* To eliminate representation a##xs, if only ~=UU & ~=nil is needed *)
-goal thy "!!tr.  [|tr=a##xs; a~=UU |] ==> tr~=UU & tr~=nil";
- by (Asm_full_simp_tac 1);
-qed"yields_not_UU_or_nil";
-
-
+     section" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof";  
+  
+(*  --------------------------------------------------------------------------- *)
 
 
 
-(*---------------------------------------------------------------------------
-              Filter of mksch(tr,schA,schB) to A is schA 
-                             take lemma
-  --------------------------------------------------------------------------- *)
-
-goal thy "compat_ioas A B &  compat_ioas B A &\
+goal thy "!! A B. [| compat_ioas A B; compat_ioas B A; \
+\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
 \ Forall (%x.x:ext (A||B)) tr & \
+\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
 \ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
 \ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
-\ LastActExtsch schA & LastActExtsch schB  \
+\ LastActExtsch A schA & LastActExtsch B schB  \
 \ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
 
+by (strip_tac 1);
+br seq.take_lemma 1;
+br mp 1;
+ba 2;
+back();back();back();back();
+by (res_inst_tac [("x","schA")] spec 1);
+by (res_inst_tac [("x","schB")] spec 1);
+by (res_inst_tac [("x","tr")] spec 1);
+by (thin_tac' 5 1);
+br less_induct 1;
+by (REPEAT (rtac allI 1));
+ren "tr schB schA" 1;
+by (strip_tac 1);
+by (REPEAT (etac conjE 1));
 
-by (res_inst_tac [("Q","%x. x:act B & x~:act A")] take_lemma_less_induct 1);
+by (case_tac "Forall (%x. x:act B & x~:act A) tr" 1);
+
+br (seq_take_lemma RS iffD2 RS spec) 1;
+by (thin_tac' 5 1);
 
 
-(*---------------------------------------------------------------------------
-              Filter of mksch(tr,schA,schB) to A is schA 
-                             take lemma
-  --------------------------------------------------------------------------- *)
-
-goal thy "! schA schB tr. compat_ioas A B &  compat_ioas B A &\
-\ forall (plift (%x.x:externals(asig_of (A||B)))) tr & \
-\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr &\
-\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr &\
-\ LastActExtsch schA & LastActExtsch schB  \
-\ --> trace_take n`(tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB)) = trace_take n`schA";
-
-by (res_inst_tac[("n","n")] less_induct 1);
-by (REPEAT(rtac allI 1));
-br impI 1;
-by (REPEAT (etac conjE 1));
-by (res_inst_tac [("x","tr")] trace.cases 1);
-
-(* tr = UU *)
-by (rotate_tac ~1 1);
-by (Asm_full_simp_tac 1);
-by (dtac LastActExtimplUU 1);
-ba 1;
-by (Asm_simp_tac 1);
+by (case_tac "Finite tr" 1);
 
-(* tr = nil *)
-by (rotate_tac ~1 1);
-by (Asm_full_simp_tac 1);
-by (dtac LastActExtimplnil 1);
-ba 1;
+(* both sides of this equation are nil *)
+by (subgoal_tac "schA=nil" 1);
 by (Asm_simp_tac 1);
-
-(* tr = t##ts *)
-
-(* just to delete tr=a##xs, as we do not make induction on a but on an element in 
-   xs we find later *)
-by (dtac yields_not_UU_or_nil 1);
-ba 1;
-by (REPEAT (etac conjE 1));
-
-(* FIX: or use equality "hd(f ~P x)=UU  =  fa P x" to make distinction on that *)
-by (case_tac "forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" 1);
-(* This case holds for whole streams, not only for takes *)
-br (trace_take_lemma RS iffD2 RS spec) 1;
-
-by (case_tac "tr : tfinite" 1);
-
-(* FIX: Check if new trace lemmata with ==> instead of --> allow for simplifiaction instead
-       of ares_tac in the following *)
-br both_nil 1;
-(* mksch = nil *)
-by (REPEAT (ares_tac [forallQfilterPnil,forallBnA_mksch,finiteL_mksch] 1));
-by (Fast_tac 1);
-(* schA = nil *)
+(* first side: mksch = nil *)
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch1],
+                           !simpset)) 1);
+(* second side: schA = nil *)
 by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
 by (Asm_simp_tac 1);
-br forallQfilterPnil 1;
-ba 1;
-back();
-ba 1;
-by (Fast_tac 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil],
+                           !simpset)) 1);
+
+(* case ~ Finite s *)
 
-(* case tr~:tfinite *)
-
-br both_UU 1;
-(* mksch = UU *)
-by (REPEAT (ares_tac [forallQfilterPUU,(finiteR_mksch RS mp COMP rev_contrapos),
-                      forallBnA_mksch] 1));
-by (Fast_tac 1);
+(* both sides of this equation are UU *)
+by (subgoal_tac "schA=UU" 1);
+by (Asm_simp_tac 1);
+(* first side: mksch = UU *)
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
+                                           (finiteR_mksch RS mp COMP rev_contrapos),
+                                            ForallBnAmksch],
+                           !simpset)) 1);
 (* schA = UU *)
 by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);
-br forallQfilterPUU 1;
-by (REPEAT (atac  1));
-back();
-by (Fast_tac 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU],
+                           !simpset)) 1);
+
+(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
+
+bd divide_Seq3 1;
 
-(* case" ~ forall (plift (%x.x:actions(asig_of B) & x~:actions(asig_of A))) tr" *)
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+by (hyp_subst_tac 1);
 
-by (dtac divide_trace3 1);
+(* bring in lemma reduceA_mksch *)
+by (forw_inst_tac [("x","schB"),("xa","schA"),("A","A"),("B","B")] reduceA_mksch 1);
 by (REPEAT (atac 1));
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
 
-(* rewrite assuption for tr *)
-by (hyp_subst_tac 1);
-(* bring in lemma reduce_mksch *)
-by (forw_inst_tac [("y","schB"),("x","schA")] reduce_mksch 1);
-ba 1;
-by (asm_simp_tac HOL_min_ss 1);
-by (REPEAT (etac exE 1));
-by (REPEAT (etac conjE 1));
-
-(* use reduce_mksch to rewrite conclusion *)
+(* use reduceA_mksch to rewrite conclusion *)
 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac  1);
 
 (* eliminate the B-only prefix *)
-(* FIX: Cannot be done by 
-   by (asm_full_simp_tac (HOL_min_ss addsimps [forallQfilterPnil]) 1);
-   as P&Q --> Q is looping. Perhaps forall (and other) operations not on predicates but on 
-   sets because of this reason ?????? *)
-br nil_and_tconc_f 1;
-be forallQfilterPnil 1;
-ba 1;
-by (Fast_tac 1);
+
+by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
+be ForallQFilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+
+(* Now real recursive step follows (in y) *)
 
-(* Now real recursive step follows (in Def x) *)
-
-by (case_tac "x:actions(asig_of A)" 1);
-by (case_tac "x~:actions(asig_of B)" 1);
+by (Asm_full_simp_tac  1);
+by (case_tac "x:act A" 1);
+by (case_tac "x~:act B" 1);
 by (rotate_tac ~2 1);
-by (asm_full_simp_tac (!simpset addsimps [filter_rep])  1);
+by (Asm_full_simp_tac 1);
 
-(* same problem as above for the B-onlu prefix *)
-(* FIX: eliminate generated subgoal immeadiately ! (as in case below x:A & x: B *)
-by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1);
+by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
-be forallQfilterPnil 2;
+be ForallQFilterPnil 2;
 ba 2;
 by (Fast_tac 2);
  
-(* f A (tw iA) = tw iA *)
-by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1);
+(* bring in divide Seq for s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+
+(* subst divide_Seq in conclusion, but only at the righest occurence *)
+by (res_inst_tac [("t","schA")] ssubst 1);
+back();
+back();
+back();
+ba 1;
+
+(* reduce trace_takes from n to strictly smaller k *)
+br take_reduction 1;
+
+(* f A (tw iA) = tw ~eA *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+                              not_ext_is_int_or_not_act]) 1);
+br refl 1;
+by (asm_full_simp_tac (!simpset addsimps [int_is_act,
+                              not_ext_is_int_or_not_act]) 1);
+by (rotate_tac ~11 1);
+
+(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
 
-by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1);
-(* subst divide_trace in conlcusion, but only at the righest occurence *)
+(* assumption Forall tr *)
+by (asm_full_simp_tac (!simpset addsimps [Forall_Conc]) 1);
+(* assumption schB *)
+by (asm_full_simp_tac (!simpset addsimps [Forall_Conc,ext_and_act]) 1);
+by (REPEAT (etac conjE 1));
+(* assumption schA *)
+by (dres_inst_tac [("x","schA"),
+                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
+by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
+by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
+ba 1;
+
+(* assumption Forall schA *)
+by (dres_inst_tac [("s","schA"),
+                   ("P","Forall (%x.x:act A)")] subst 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
+
+(* case x:actions(asig_of A) & x: actions(asig_of B) *)
+
+
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac  1);
+
+by (subgoal_tac "Filter (%a. a:act A & a:ext B)`y1=nil" 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac  1);
+(* eliminate introduced subgoal 2 *)
+be ForallQFilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+ 
+(* bring in divide Seq for s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
+
+(* subst divide_Seq in conclusion, but only at the righest occurence *)
 by (res_inst_tac [("t","schA")] ssubst 1);
 back();
 back();
 back();
 ba 1;
-by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1);
+
+(* f A (tw iA) = tw ~eA *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+                              not_ext_is_int_or_not_act]) 1);
 
+(* rewrite assumption forall and schB *)
+by (rotate_tac 13 1);
+by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
+
+(* divide_Seq for schB2 *)
+by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
 by (REPEAT (etac conjE 1));
-(* reduce trace_takes from n to strictly smaller k *)
-by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1);
-br take_reduction 1;
-ba 1;
-(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
-by (rotate_tac ~10 1);
-(* assumption forall and schB *)
-by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1);
 (* assumption schA *)
 by (dres_inst_tac [("x","schA"),
-                   ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1);
+                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+
+(* f A (tw iB schB2) = nil *) 
+by (asm_full_simp_tac (!simpset addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
+             FilterPTakewhileQnil,intA_is_not_actB]) 1);
+
+
+(* reduce trace_takes from n to strictly smaller k *)
+br take_reduction 1;
+br refl 1;
+br refl 1;
+
+(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
+
+(* assumption schB *)
+by (dres_inst_tac [("x","y2"),
+                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
 ba 1;
-by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1);
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
+
+(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
+by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
+by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
+ba 1;
+by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1);
+
+(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
+by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile]) 1);
+
+(* case x~:A & x:B  *)
+(* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
+by (case_tac "x:act B" 1);
+by (Fast_tac 1);
+
+(* case x~:A & x~:B  *)
+(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
+by (rotate_tac ~9 1);
+(* reduce forall assumption from tr to (x>>rs) *)
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
 by (REPEAT (etac conjE 1));
-(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
-by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1);
-by (dres_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
-ba 1;
+by (fast_tac (!claset addSIs [ext_is_act]) 1);
+
+qed"FilterAmksch_is_schA";
+
+
+
+(*---------------------------------------------------------------------------  *)
+
+   section" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof";
+                
+(*  --------------------------------------------------------------------------- *)
+
+
+
+goal thy "!! A B. [| compat_ioas A B; compat_ioas B A; \
+\ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
+\ Forall (%x.x:ext (A||B)) tr & \
+\ Forall (%x.x:act A) schA & Forall (%x.x:act B) schB & \
+\ Filter (%a.a:ext A)`schA = Filter (%a.a:act A)`tr &\
+\ Filter (%a.a:ext B)`schB = Filter (%a.a:act B)`tr &\
+\ LastActExtsch A schA & LastActExtsch B schB  \
+\ --> Filter (%a.a:act B)`(mksch A B`tr`schA`schB) = schB";
+
+by (strip_tac 1);
+br seq.take_lemma 1;
+br mp 1;
+ba 2;
+back();back();back();back();
+by (res_inst_tac [("x","schA")] spec 1);
+by (res_inst_tac [("x","schB")] spec 1);
+by (res_inst_tac [("x","tr")] spec 1);
+by (thin_tac' 5 1);
+br less_induct 1;
+by (REPEAT (rtac allI 1));
+ren "tr schB schA" 1;
+by (strip_tac 1);
+by (REPEAT (etac conjE 1));
+
+by (case_tac "Forall (%x. x:act A & x~:act B) tr" 1);
+
+br (seq_take_lemma RS iffD2 RS spec) 1;
+by (thin_tac' 5 1);
+
+
+by (case_tac "Finite tr" 1);
+
+(* both sides of this equation are nil *)
+by (subgoal_tac "schB=nil" 1);
+by (Asm_simp_tac 1);
+(* first side: mksch = nil *)
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil,ForallAnBmksch,FiniteL_mksch1],
+                           !simpset)) 1);
+(* second side: schA = nil *)
+by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
+by (Asm_simp_tac 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPnil],
+                           !simpset)) 1);
+
+(* case ~ Finite tr *)
+
+(* both sides of this equation are UU *)
+by (subgoal_tac "schB=UU" 1);
+by (Asm_simp_tac 1);
+(* first side: mksch = UU *)
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU,
+                                           (finiteR_mksch RS mp COMP rev_contrapos),
+                                            ForallAnBmksch],
+                           !simpset)) 1);
+(* schA = UU *)
+by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
+by (Asm_simp_tac 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [ForallQFilterPUU],
+                           !simpset)) 1);
+
+(* case" ~ Forall (%x.x:act B & x~:act A) s" *)
+
+bd divide_Seq3 1;
+
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+by (hyp_subst_tac 1);
+
+(* bring in lemma reduceB_mksch *)
+by (forw_inst_tac [("y","schB"),("x","schA"),("A","A"),("B","B")] reduceB_mksch 1);
+by (REPEAT (atac 1));
+by (REPEAT (etac exE 1));
+by (REPEAT (etac conjE 1));
+
+(* use reduceB_mksch to rewrite conclusion *)
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac  1);
+
+(* eliminate the A-only prefix *)
+
+by (subgoal_tac "(Filter (%a.a :act B)`x1) = nil" 1);
+be ForallQFilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+
+(* Now real recursive step follows (in x) *)
+
+by (Asm_full_simp_tac  1);
+by (case_tac "x:act B" 1);
+by (case_tac "x~:act A" 1);
+by (rotate_tac ~2 1);
 by (Asm_full_simp_tac 1);
 
-(* case x:actions(asig_of A) & x: actions(asig_of B) *)
-by (rotate_tac ~2 1);
-by (asm_full_simp_tac (!simpset addsimps [filter_rep])  1);
-by (subgoal_tac "tfilter`(plift (%a. a : actions (asig_of A) & a : externals (asig_of B)))`y1=nil" 1);
+by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
-by (thin_tac' 1 1);
 (* eliminate introduced subgoal 2 *)
-be forallQfilterPnil 2;
+be ForallQFilterPnil 2;
 ba 2;
 by (Fast_tac 2);
  
-(* f A (tw iA) = tw iA *)
-by (simp_tac (HOL_min_ss addsimps [filterPtakewhileQ,int_is_act]) 1);
+(* bring in divide Seq for s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
+by (REPEAT (etac conjE 1));
 
-by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace] 1);
-(* subst divide_trace in conlcusion, but only at the righest occurence *)
-by (res_inst_tac [("t","schA")] ssubst 1);
+(* subst divide_Seq in conclusion, but only at the righest occurence *)
+by (res_inst_tac [("t","schB")] ssubst 1);
 back();
 back();
 back();
 ba 1;
-by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite] 1);
+
+(* reduce trace_takes from n to strictly smaller k *)
+br take_reduction 1;
+
+(* f B (tw iB) = tw ~eB *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+                              not_ext_is_int_or_not_act]) 1);
+br refl 1;
+by (asm_full_simp_tac (!simpset addsimps [int_is_act,
+                              not_ext_is_int_or_not_act]) 1);
+by (rotate_tac ~11 1);
+
+(* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
+
+(* assumption Forall tr *)
+by (asm_full_simp_tac (!simpset addsimps [Forall_Conc]) 1);
+(* assumption schA *)
+by (asm_full_simp_tac (!simpset addsimps [Forall_Conc,ext_and_act]) 1);
 by (REPEAT (etac conjE 1));
-(* tidy up *)
-by (thin_tac' 12 1);
-by (thin_tac' 12 1);
-by (thin_tac' 14 1);
-by (thin_tac' 14 1);
-by (rotate_tac ~8 1);
-(* rewrite assumption forall and schB *)
-by (asm_full_simp_tac (!simpset addsimps [tconc_cong,forall_cons,forall_tconc,ext_and_act]) 1);
-(* divide_trace for schB2 *)
-by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_trace) 1);
-by (forw_inst_tac [("y","y2")](sym RS antisym_less_inverse RS conjunct1 RS divide_trace_finite) 1);
+(* assumption schB *)
+by (dres_inst_tac [("x","schB"),
+                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+(* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
+by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
+by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
+ba 1;
+
+(* assumption Forall schB *)
+by (dres_inst_tac [("s","schB"),
+                   ("P","Forall (%x.x:act B)")] subst 1);
+ba 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
+
+(* case x:actions(asig_of A) & x: actions(asig_of B) *)
+
+
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac  1);
+
+by (subgoal_tac "Filter (%a. a:act B & a:ext A)`x1=nil" 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac  1);
+(* eliminate introduced subgoal 2 *)
+be ForallQFilterPnil 2;
+ba 2;
+by (Fast_tac 2);
+ 
+(* bring in divide Seq for s *)
+by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
 by (REPEAT (etac conjE 1));
-by (rotate_tac ~6 1);
-(* assumption schA *)
-by (dres_inst_tac [("x","schA"),
-                   ("g","tfilter`(plift (%a. a : actions (asig_of A)))`rs")] lemma22 1);
-ba 1;
-by (asm_full_simp_tac (!simpset addsimps [tfiltertconc,not_int_is_ext,tfilterPtakewhileQ]) 1);
-by (REPEAT (etac conjE 1));
-(* f A (tw iB schB2) = nil *) 
 
-(* good luck: intAisnotextB is not looping *)
-by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1);
-(* reduce trace_takes from n to strictly smaller k *)
-by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext]) 1);
-br take_reduction 1;
+(* subst divide_Seq in conclusion, but only at the righest occurence *)
+by (res_inst_tac [("t","schB")] ssubst 1);
+back();
+back();
+back();
 ba 1;
-(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
-(* assumption schB *)
-by (dres_inst_tac [("x","y2"),
-                   ("g","tfilter`(plift (%a. a : actions (asig_of B)))`rs")] lemma22 1);
+
+(* f B (tw iB) = tw ~eB *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
+                              not_ext_is_int_or_not_act]) 1);
+
+(* rewrite assumption forall and schB *)
+by (rotate_tac 13 1);
+by (asm_full_simp_tac (!simpset addsimps [ext_and_act]) 1);
+
+(* divide_Seq for schB2 *)
+by (forw_inst_tac [("y","x2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
+by (REPEAT (etac conjE 1));
+(* assumption schA *)
+by (dres_inst_tac [("x","schB"),
+                   ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
 ba 1;
-(* FIX: hey wonder: why does loopin rule for y2 here rewrites !!!!!!!!!!!!!!!!!!!!!!!!*)
-by (asm_full_simp_tac (!simpset addsimps [not_int_is_ext,tfilterPtakewhileQ,intAisnotextB]) 1);
-by (REPEAT (etac conjE 1));
-(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
-by (dres_inst_tac [("sch","schA"),("P","plift (%a. a : internals (asig_of A))")] LastActExtsmall1 1);
-by (dres_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
+
+(* f B (tw iA schA2) = nil *) 
+by (asm_full_simp_tac (!simpset addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
+             FilterPTakewhileQnil,intA_is_not_actB]) 1);
+
+
+(* reduce trace_takes from n to strictly smaller k *)
+br take_reduction 1;
+br refl 1;
+br refl 1;
+
+(* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
+
+(* assumption schA *)
+by (dres_inst_tac [("x","x2"),
+                   ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
 ba 1;
-by (dres_inst_tac [("sch","y2"),("P","plift (%a. a : internals (asig_of B))")] LastActExtsmall1 1);
-by (Asm_full_simp_tac 1);
- 
-(* case x~:A & x:B  *)
+by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
+
+(* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
+by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
+by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
+ba 1;
+by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1);
+
+(* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
+by (asm_full_simp_tac (!simpset addsimps [ForallTL,ForallDropwhile]) 1);
+
+(* case x~:B & x:A  *)
 (* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
-by (case_tac "x:actions(asig_of B)" 1);
+by (case_tac "x:act A" 1);
 by (Fast_tac 1);
 
-(* case x~:A & x~:B  *)
-(* cannot occur because of assumption: forall (a:ext A | a:ext B) *)
-by (rotate_tac ~8 1);
-(* reduce forall assumption from tr to (Def x ## rs) *)
-by (asm_full_simp_tac (!simpset addsimps [forall_cons,forall_tconc]) 1);
+(* case x~:B & x~:A  *)
+(* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
+by (rotate_tac ~9 1);
+(* reduce forall assumption from tr to (x>>rs) *)
+by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
 by (REPEAT (etac conjE 1));
-by (asm_full_simp_tac (!simpset addsimps [externals_of_par]) 1);
 by (fast_tac (!claset addSIs [ext_is_act]) 1);
 
-qed"filterAmksch_is_schA";
-
-
-goal thy "!! tr. [|compat_ioas A B ;  compat_ioas B A ;\
-\ forall (plift (%x.x:externals(asig_of (A||B)))) tr ; \
-\ tfilter`(plift (%a.a:externals(asig_of A)))`schA = tfilter`(plift (%a.a:actions(asig_of A)))`tr ;\
-\ tfilter`(plift (%a.a:externals(asig_of B)))`schB = tfilter`(plift (%a.a:actions(asig_of B)))`tr ;\
-\ LastActExtsch schA ; LastActExtsch schB |] \
-\ ==> tfilter`(plift (%a.a:actions(asig_of A)))`(mksch A B`tr`schA`schB) = schA";
-
-br trace.take_lemma 1;
-by (asm_simp_tac (!simpset addsimps [filterAmksch_is_schA]) 1);
-qed"filterAmkschschA";
+qed"FilterBmksch_is_schB";
 
 
 
 (* ------------------------------------------------------------------ *)
-(*                COMPOSITIONALITY   on    TRACE    Level             *)
-(*                             Main Theorem                           *)
+         section"COMPOSITIONALITY on TRACE Level -- Main Theorem";
 (* ------------------------------------------------------------------ *)
  
 goal thy 
-"!! A B. [| compat_ioas A B; compat_ioas B A; \
+"!! A B. [| IOA A; IOA B; compat_ioas A B; compat_ioas B A; \
 \           is_asig(asig_of A); is_asig(asig_of B)|] \
-\       ==> traces(A||B) = \
-\           { tr.(Filter (%a.a:act A)`tr : traces A &\
-\                 Filter (%a.a:act B)`tr : traces B &\
-\                 Forall (%x. x:ext(A||B)) tr) }";
+\       ==>  tr: traces(A||B) = \
+\            (Filter (%a.a:act A)`tr : traces A &\
+\             Filter (%a.a:act B)`tr : traces B &\
+\             Forall (%x. x:ext(A||B)) tr)";
 
 by (simp_tac (!simpset addsimps [traces_def,has_trace_def]) 1);
-br set_ext 1;
 by (safe_tac set_cs);
  
 (* ==> *) 
@@ -681,54 +982,40 @@
 
 (* <== *)
 
-(* replace schA and schB by cutsch(schA) and cutsch(schB) *)
+(* replace schA and schB by Cut(schA) and Cut(schB) *)
 by (dtac exists_LastActExtsch 1);
 ba 1;
 by (dtac exists_LastActExtsch 1);
 ba 1;
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
+(* Schedules of A(B) have only actions of A(B) *)
+bd scheds_in_sig 1;
+ba 1;
+bd scheds_in_sig 1;
+ba 1;
 
+ren "h1 h2 schA schB" 1;
 (* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
    we need here *)
-by (res_inst_tac [("x","mksch A B`tr`schb`schc")] bexI 1);
+by (res_inst_tac [("x","mksch A B`tr`schA`schB")] bexI 1);
 
 (* External actions of mksch are just the oracle *)
-by (asm_full_simp_tac (!simpset addsimps [filterA_mksch_is_tr]) 1);
+by (asm_full_simp_tac (!simpset addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
 
 (* mksch is a schedule -- use compositionality on sch-level *)
 by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1);
-
-       das hier loopt: ForallPForallQ, ext_is_act,ForallAorB_mksch]) 1);
+by (asm_full_simp_tac (!simpset addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
+be ForallAorB_mksch 1;
+be ForallPForallQ 1;
+be ext_is_act 1;
+qed"compositionality_tr";
 
 
 
 
 
 
-*)
 
 
 
-(* -------------------------------------------------------------------------------
-         Other useful things
-  -------------------------------------------------------------------------------- *)
-
-
-(* Lemmata not needed yet 
-goal Trace.thy "!!x. nil<<x ==> nil=x";
-by (res_inst_tac [("x","x")] trace.cases 1);
-by (hyp_subst_tac 1);
-by (etac antisym_less 1);
-by (Asm_full_simp_tac 1);
-by (Asm_full_simp_tac 1);
-by (hyp_subst_tac 1);
-by (Asm_full_simp_tac 1);
-qed"nil_less_is_nil";
-
-
-*)
-
-
-
-
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
@@ -53,38 +53,11 @@
 
 rules
 
-(* FIX: x:actions S is further assumption, see Asig.ML: how to fulfill this in proofs ? *)
-not_ext_is_int_FIX
-  "[|is_asig S|] ==> (x~:externals S) = (x: internals S)"
-
-(* FIX: should be more general , something like subst *)
-lemma12
-"[| f << (g x) ; (x= (h x)) |] ==> f << g (h x)"
-
-(* FIX: as above, should be done more intelligent *)
-lemma22
-"[| (f x) = y >> g ; x = h x |] ==> (f (h x)) = y >> g"
-
-Finite_Conc
-  "Finite (x @@ y) = (Finite x & Finite y)"
 
 finiteR_mksch
   "Finite (mksch A B`tr`x`y) --> Finite tr"
 
-finiteL_mksch
-  "[| Finite tr; 
-   Filter (%a. a:ext A)`x = Filter (%a. a:act A)`tr;
-   Filter (%a. a:ext B)`y = Filter (%a. a:actB)`tr;
-   Forall (%x. x:ext (A||B)) tr |]
-   ==> Finite (mksch A B`tr`x`y)"
 
-reduce_mksch
-  "[| Finite bs; Forall (%x. x:act B & x~:act A) bs;
-      Filter (%a. a:ext B)`y = Filter (%a. a:act B)`(bs @@ z) |] 
-  ==> ? y1 y2.  (mksch A B`(bs @@ z)`x`y) = (y1 @@ (mksch A B`z`x`y2)) &
-                Forall (%x. x:act B & x~:act A) y1 &
-                Finite y1 & y = (y1 @@ y2) & 
-                Filter (%a. a:ext B)`y1 = bs"
 
 end
 
diff -r 70939b0fadfb -r 3f53f2c876f4 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);
 
+
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Compositionality.thy
--- a/src/HOLCF/IOA/meta_theory/Compositionality.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,21 +1,9 @@
 (*  Title:      HOLCF/IOA/meta_theory/Compositionality.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1997  TU Muenchen
 
 Compositionality of I/O automata
 *) 
 
-Compositionality = CompoTraces + 
-
-rules 
-
-compotraces
-"[| compat_ioas A B; compat_ioas B A; 
-    is_asig(asig_of A); is_asig(asig_of B)|] 
- ==> traces(A||B) = 
-     {tr. (Filter (%a.a:act A)`tr : traces A &
-      Filter (%a.a:act B)`tr : traces B &
-      Forall (%x. x:ext(A||B)) tr)}"
-
-end 
\ No newline at end of file
+Compositionality = Automata + Traces + CompoTraces
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/IOA.ML
--- a/src/HOLCF/IOA/meta_theory/IOA.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/IOA.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/IOA.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf Mueller
     Copyright   1996,1997  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/IOA.thy
--- a/src/HOLCF/IOA/meta_theory/IOA.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/IOA.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/IOA.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf Mueller
     Copyright   1996,1997  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.ML
-    ID:         $$
+    ID:         $Id$
     Author:     Olaf Mueller
     Copyright   1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/RefCorrectness.thy
-    ID:         $$
+    ID:         $Id$
     Author:     Olaf Mueller
     Copyright   1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/RefMappings.ML
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/RefMappings.ML
-    ID:         $$
+    ID:         $Id$
     Author:     Olaf Mueller
     Copyright   1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/RefMappings.thy
--- a/src/HOLCF/IOA/meta_theory/RefMappings.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/RefMappings.thy
-    ID:         $$
+    ID:         $Id$
     Author:     Olaf Mueller
     Copyright   1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Seq.ML
--- a/src/HOLCF/IOA/meta_theory/Seq.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Seq.ML
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
@@ -16,6 +16,9 @@
 
 Addsimps [UU_neq_nil];
 
+
+
+
 (* ------------------------------------------------------------------------------------- *)
 
 
@@ -224,7 +227,7 @@
 by (REPEAT (Asm_full_simp_tac 1));
 qed"sconc_cons";
 
-Addsimps [sconc_nil, sconc_UU,sconc_cons];
+Addsimps [sconc_nil,sconc_UU,sconc_cons];
 
 
 (* ----------------------------------------------------------- *)
@@ -311,7 +314,7 @@
 
 (* ------------------------------------------------------------------------------------- *)
 
-section "scons";
+section "scons, nil";
 
 goal thy 
  "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
@@ -320,6 +323,15 @@
 auto();
 qed"scons_inject_eq";
 
+goal thy "!!x. nil<<x ==> nil=x";
+by (res_inst_tac [("x","x")] seq.cases 1);
+by (hyp_subst_tac 1);
+by (etac antisym_less 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+qed"nil_less_is_nil";
 
 (* ------------------------------------------------------------------------------------- *)
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOLCF/IOA/meta_theory/Seq.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Seq.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Sequence.ML
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
@@ -67,13 +67,6 @@
 (*                               Conc                               *)
 (* ---------------------------------------------------------------- *)
 
-goal thy "UU @@ y =UU";
-by (Simp_tac 1);
-qed"Conc_UU";
-
-goal thy "nil @@ y =y";
-by (Simp_tac 1);
-qed"Conc_nil";
 
 goal thy "(x>>xs) @@ y = x>>(xs @@y)"; 
 by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -215,7 +208,7 @@
           Map_UU,Map_nil,Map_cons,
           Forall_UU,Forall_nil,Forall_cons,
           Last_UU,Last_nil,Last_cons,
-          Conc_UU,Conc_nil,Conc_cons,
+          Conc_cons,
           Takewhile_UU, Takewhile_nil, Takewhile_cons, 
           Dropwhile_UU, Dropwhile_nil, Dropwhile_cons,
           Zip_UU1,Zip_UU2,Zip_nil,Zip_cons_nil,Zip_cons];
@@ -281,6 +274,7 @@
 br Def_not_UU 1;
 qed"Cons_not_UU";
 
+
 goal thy "~(a>>x) << UU";
 by (rtac notI 1);
 by (dtac antisym_less 1);
@@ -299,6 +293,10 @@
 by (resolve_tac seq.rews 1);
 qed"Cons_not_nil";
 
+goal thy "nil ~= a>>s";
+by (simp_tac (!simpset addsimps [Cons_def2]) 1);
+qed"Cons_not_nil2";
+
 goal thy "(a>>s = b>>t) = (a = b & s = t)";
 by (simp_tac (HOL_ss addsimps [Cons_def2]) 1);
 by (stac (hd lift.inject RS sym) 1);
@@ -325,9 +323,17 @@
 by (simp_tac (!simpset addsimps [Cons_def]) 1);
 qed"seq_take_Cons";
 
-Addsimps [Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
+Addsimps [Cons_not_nil2,Cons_inject_eq,Cons_inject_less_eq,seq_take_Cons,
           Cons_not_UU,Cons_not_less_UU,Cons_not_less_nil,Cons_not_nil];
 
+(* Instead of adding UU_neq_Cons every equation UU~=x could be changed to x~=UU *)
+goal thy "UU ~= x>>xs";
+by (res_inst_tac [("s1","UU"),("t1","x>>xs")]  (sym RS rev_contrapos) 1);
+by (REPEAT (Simp_tac 1));
+qed"UU_neq_Cons";
+
+Addsimps [UU_neq_Cons];
+
 
 (* ----------------------------------------------------------------------------------- *)
 
@@ -399,6 +405,61 @@
 qed"Finite_Cons";
 
 Addsimps [Finite_Cons];
+goal thy "!! x. Finite (x::'a Seq) ==> Finite y --> Finite (x@@y)";
+by (Seq_Finite_induct_tac 1);
+qed"FiniteConc_1";
+
+goal thy "!! z. Finite (z::'a Seq) ==> !x y. z= x@@y --> (Finite x & Finite y)";
+by (Seq_Finite_induct_tac 1);
+(* nil*)
+by (strip_tac 1);
+by (Seq_case_simp_tac "x" 1);
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+(* cons *)
+by (strip_tac 1);
+by (Seq_case_simp_tac "x" 1);
+by (Seq_case_simp_tac "y" 1);
+by (SELECT_GOAL (auto_tac (!claset,!simpset))1);
+by (eres_inst_tac [("x","sa")] allE 1);
+by (eres_inst_tac [("x","y")] allE 1);
+by (Asm_full_simp_tac 1);
+qed"FiniteConc_2";
+
+goal thy "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
+by (rtac iffI 1);
+be (FiniteConc_2 RS spec RS spec RS mp) 1;
+br refl 1;
+br (FiniteConc_1 RS mp) 1;
+auto();
+qed"FiniteConc";
+
+Addsimps [FiniteConc];
+
+
+goal thy "!! s. Finite s ==> Finite (Map f`s)";
+by (Seq_Finite_induct_tac 1);
+qed"FiniteMap1";
+
+goal thy "!! s. Finite s ==> ! t. (s = Map f`t) --> Finite t";
+by (Seq_Finite_induct_tac 1);
+by (strip_tac 1);
+by (Seq_case_simp_tac "t" 1);
+by (Asm_full_simp_tac 1);
+(* main case *)
+auto();
+by (Seq_case_simp_tac "t" 1);
+by (Asm_full_simp_tac 1);
+qed"FiniteMap2";
+
+goal thy "Finite (Map f`s) = Finite s";
+auto();
+be (FiniteMap2 RS spec RS mp) 1;
+br refl 1;
+be FiniteMap1 1;
+qed"Map2Finite";
+
 
 (* ------------------------------------------------------------------------------------ *)
 
@@ -408,6 +469,21 @@
 by (Seq_Finite_induct_tac 1);
 qed"Conc_cong";
 
+goal thy "(x @@ y) @@ z = (x::'a Seq) @@ y @@ z";
+by (Seq_induct_tac "x" [] 1);
+qed"Conc_assoc";
+
+goal thy "s@@ nil = s";
+by (res_inst_tac[("x","s")] seq.ind 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Simp_tac 1);
+by (Asm_full_simp_tac 1);
+qed"nilConc";
+
+Addsimps [nilConc];
+
+
 (* ------------------------------------------------------------------------------------ *)
 
 section "Last";
@@ -456,10 +532,33 @@
 by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
 qed"MapFilter";
 
+goal thy "nil = (Map f`s) --> s= nil";
+by (Seq_case_simp_tac "s" 1);
+qed"nilMap";
+
+goal thy "Forall P (Map f`s) --> Forall (P o f) s";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+auto();
+qed"ForallMap1";
+
+
+goal thy "Forall (P o f) s --> Forall P (Map f`s) ";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+auto();
+qed"ForallMap2";
+
+(* FIX: should be proved directly. Therefore adm lemma for equalitys on _bools_ has 
+    to be added to !simpset *)
+goal thy "Forall P (Map f`s) = Forall (P o f) s";
+auto();
+be (ForallMap1 RS mp) 1;
+be (ForallMap2 RS mp) 1;
+qed"ForallMap";
+
 
 (* ------------------------------------------------------------------------------------ *)
 
-section "Forall, Conc";
+section "Forall";
 
 
 goal thy "Forall P ys & (! x. P x --> Q x) \
@@ -477,6 +576,46 @@
 by (Seq_Finite_induct_tac  1);
 qed"Forall_Conc";
 
+Addsimps [Forall_Conc];
+
+goal thy "Forall P s  --> Forall P (TL`s)";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+qed"ForallTL1";
+
+bind_thm ("ForallTL",ForallTL1 RS mp);
+
+goal thy "Forall P s  --> Forall P (Dropwhile Q`s)";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+qed"ForallDropwhile1";
+
+bind_thm ("ForallDropwhile",ForallDropwhile1 RS mp);
+
+
+(* only admissible in t, not if done in s *)
+
+goal thy "! s. Forall P s --> t<<s --> Forall P t";
+by (Seq_induct_tac "t" [Forall_def,sforall_def] 1);
+by (strip_tac 1); 
+by (Seq_case_simp_tac "sa" 1);
+by (Asm_full_simp_tac 1);
+auto();
+qed"Forall_prefix";
+ 
+bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
+
+
+goal thy "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
+auto();
+qed"Forall_postfixclosed";
+
+
+goal thy "((! x. P x --> (Q x = R x)) & Forall P tr) --> Filter Q`tr = Filter R`tr";
+by (Seq_induct_tac "tr" [Forall_def,sforall_def] 1);
+qed"ForallPFilterQR1";
+
+bind_thm("ForallPFilterQR",allI RS (conjI RS (ForallPFilterQR1 RS mp)));
+
 
 (* ------------------------------------------------------------------------------------- *)
 
@@ -487,38 +626,29 @@
 by (simp_tac (!simpset addsimps [Filter_def,Forall_def,forallPsfilterP]) 1);
 qed"ForallPFilterP";
 
-(* FIX: holds also in other direction, then equal to forallPfilterP *)
+(* holds also in other direction, then equal to forallPfilterP *)
 goal thy "Forall P x --> Filter P`x = x";
 by (Seq_induct_tac "x" [Forall_def,sforall_def,Filter_def] 1);
 qed"ForallPFilterPid1";
 
-val ForallPFilterPid = standard (ForallPFilterPid1 RS mp);
+bind_thm(" ForallPFilterPid",ForallPFilterPid1 RS mp);
 
 
-(* holds also in <-- direction. FIX: prove that also *)
-
-goal thy "!! P. Finite ys & Forall (%x. ~P x) ys \
-\   --> Filter P`ys = nil ";
-by (res_inst_tac[("x","ys")] Seq_induct 1);
-(* adm *)
-(* FIX: cont tfinite behandeln *)
-br adm_all 1;
-(* base cases *)
-by (Simp_tac 1);
-by (Simp_tac 1);
-(* main case *)
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+(* holds also in other direction *)
+goal thy "!! ys . Finite ys ==> \
+\   Forall (%x. ~P x) ys --> Filter P`ys = nil ";
+by (Seq_Finite_induct_tac 1);
 qed"ForallnPFilterPnil1";
 
-val ForallnPFilterPnil = standard (conjI RS (ForallnPFilterPnil1 RS mp));
+bind_thm ("ForallnPFilterPnil",ForallnPFilterPnil1 RS mp);
 
 
-(* FIX: holds also in <== direction *)
+(* holds also in other direction *)
 goal thy   "!! P. ~Finite ys & Forall (%x. ~P x) ys \
 \                  --> Filter P`ys = UU ";
 by (res_inst_tac[("x","ys")] Seq_induct 1);
 (* adm *)
-(* FIX: cont ~tfinite behandeln *)
+(* FIX: cont ~Finite behandeln *)
 br adm_all 1;
 (* base cases *)
 by (Simp_tac 1);
@@ -527,7 +657,43 @@
 by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
 qed"ForallnPFilterPUU1";
 
-val ForallnPFilterPUU = standard (conjI RS (ForallnPFilterPUU1 RS mp));
+bind_thm ("ForallnPFilterPUU",conjI RS (ForallnPFilterPUU1 RS mp));
+
+
+(* inverse of ForallnPFilterPnil *)
+
+goal thy "!! ys . Filter P`ys = nil --> \
+\   (Forall (%x. ~P x) ys & Finite ys)";
+by (res_inst_tac[("x","ys")] Seq_induct 1);
+(* adm *)
+(* FIX: cont Finite behandeln *)
+br adm_all 1;
+(* base cases *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"FilternPnilForallP1";
+
+bind_thm ("FilternPnilForallP",FilternPnilForallP1 RS mp);
+
+(* inverse of ForallnPFilterPUU *)
+(* FIX: will not be admissable, search other way of proof *)
+
+goal thy   "!! P. Filter P`ys = UU --> \
+\                (Forall (%x. ~P x) ys  & ~Finite ys)";
+by (res_inst_tac[("x","ys")] Seq_induct 1);
+(* adm *)
+(* FIX: cont ~Finite behandeln *)
+br adm_all 1;
+(* base cases *)
+by (Simp_tac 1);
+by (Simp_tac 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+qed"FilternPUUForallP1";
+
+bind_thm ("FilternPUUForallP",FilternPUUForallP1 RS mp);
 
 
 goal thy  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
@@ -582,7 +748,33 @@
 Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
           FilterPTakewhileQnil,FilterPTakewhileQid];
 
+goal thy "Takewhile P`(Takewhile P`s) = Takewhile P`s";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
+qed"Takewhile_idempotent";
 
+goal thy "Forall P s --> Takewhile (%x.Q x | (~P x))`s = Takewhile Q`s";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+qed"ForallPTakewhileQnP";
+
+goal thy "Forall P s --> Dropwhile (%x.Q x | (~P x))`s = Dropwhile Q`s";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+qed"ForallPDropwhileQnP";
+
+Addsimps [ForallPTakewhileQnP RS mp, ForallPDropwhileQnP RS mp];
+
+
+goal thy "Forall P s --> Takewhile P`(s @@ t) = s @@ (Takewhile P`t)";
+by (Seq_induct_tac "s" [Forall_def,sforall_def] 1);
+qed"TakewhileConc1";
+
+bind_thm("TakewhileConc",TakewhileConc1 RS mp);
+
+goal thy "!! s.Finite s ==> Forall P s --> Dropwhile P`(s @@ t) = Dropwhile P`t";
+by (Seq_Finite_induct_tac 1);
+qed"DropwhileConc1";
+
+bind_thm("DropwhileConc",DropwhileConc1 RS mp);
 
 (* ----------------------------------------------------------------------------------- *)
 
@@ -590,7 +782,7 @@
 (*
 section "admissibility";
 
-goal thy "adm(%x.~Finite x)";
+goal thy "adm(%x.Finite x)";
 br admI 1;
 bd spec 1;
 be contrapos 1;
@@ -662,7 +854,7 @@
 auto();
 qed"divide_Seq3";
 
-Addsimps [FilterPQ,FilterConc,Conc_cong,Forall_Conc];
+Addsimps [FilterPQ,FilterConc,Conc_cong];
 
 
 (* ------------------------------------------------------------------------------------- *)
@@ -676,22 +868,24 @@
 auto();
 qed"seq_take_lemma";
 
-(*
-
-goal thy "Finite x & (! k. k < n --> seq_take k`y1 = seq_take k`y2) \
-\   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2))";
-br less_induct 1;
+goal thy 
+"  ! n. ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
+\   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2)))";
+by (Seq_induct_tac "x" [] 1);
+by (strip_tac 1);
+by (res_inst_tac [("n","n")] natE 1);
+auto();
+by (res_inst_tac [("n","n")] natE 1);
+auto();
+qed"take_reduction1";
 
 
-goal thy "!!x. Finite x ==> \
-\  ((! k. k < n --> seq_take k`y1 = seq_take k`y2) \
-\   --> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2)))";
-by (Seq_Finite_induct_tac 1);
-by (asm_full_simp_tac (!simpset setloop split_tac [expand_if] ) 1);
+goal thy "!! n.[| x=y; s=t;!! k.k<n ==> seq_take k`y1 = seq_take k`y2|] \
+\ ==> seq_take n`(x @@ (s>>y1)) =  seq_take n`(y @@ (t>>y2))";
 
-
+by (auto_tac (!claset addSIs [take_reduction1 RS spec RS mp],!simpset));
 qed"take_reduction";
-*)
+
 
 goal thy "!! Q. [|!! s. [| Forall Q s; A s |] ==> (f s) = (g s) ; \
 \           !! s1 s2 y. [| Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2)|] \
@@ -763,6 +957,62 @@
 by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
 qed"take_lemma_less_induct";
 
+
+(*
+
+goal thy 
+"!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \
+\  !! s1 s2 y n. [| ! t h1 h2 m. m < n --> (A t h1 h2) --> seq_take m`(f t h1 h2) = seq_take m`(g t h1 h2);\
+\                         Forall Q s1; Finite s1; ~ Q y; A (s1 @@ y>>s2) h1 h2|] \
+\                         ==>   seq_take n`(f (s1 @@ y>>s2) h1 h2) \
+\                             = seq_take n`(g (s1 @@ y>>s2) h1 h2) |] \
+\              ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
+by (strip_tac 1);
+br seq.take_lemma 1;
+br mp 1;
+ba 2;
+by (res_inst_tac [("x","h2a")] spec 1);
+by (res_inst_tac [("x","h1a")] spec 1);
+by (res_inst_tac [("x","x")] spec 1);
+br less_induct 1;
+br allI 1;
+by (case_tac "Forall Q xa" 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
+                           !simpset)) 1);
+by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+qed"take_lemma_less_induct";
+
+
+
+goal thy 
+"!! Q. [|!! s. Forall Q s ==> P ((f s) = (g s)) ; \
+\        !! s1 s2 y n. [| ! t m. m < n --> P (seq_take m`(f t) = seq_take m`(g t));\
+\                         Forall Q s1; Finite s1; ~ Q y|] \
+\                         ==>   P (seq_take n`(f (s1 @@ y>>s2)) \
+\                                   = seq_take n`(g (s1 @@ y>>s2))) |] \
+\              ==> P ((f x)=(g x))";
+
+by (res_inst_tac [("t","f x = g x"),
+                  ("s","!n. seq_take n`(f x) = seq_take n`(g x)")] subst 1);
+br seq_take_lemma 1;
+
+wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden.....
+
+
+FIX
+
+br less_induct 1;
+br allI 1;
+by (case_tac "Forall Q xa" 1);
+by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
+                           !simpset)) 1);
+by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
+qed"take_lemma_less_induct";
+
+
+*)
+
+
 goal thy 
 "!! Q. [| A UU  ==> (f UU) = (g UU) ; \
 \         A nil ==> (f nil) = (g nil) ; \
@@ -822,10 +1072,8 @@
 
 goal thy "Filter P`(Filter Q`s) = Filter (%x. P x & Q x)`s";
 by (res_inst_tac [("A1","%x.True") 
-                 ,("Q1","%x.~(P x & Q x)")]
+                 ,("Q1","%x.~(P x & Q x)"),("x1","s")]
                  (take_lemma_induct RS mp) 1);
-(* FIX: rule always needs a back: eliminate *)
-back();
 (* FIX: better support for A = %.True *)
 by (Fast_tac 3);
 by (asm_full_simp_tac (!simpset addsimps [Filter_lemma1]) 1);
@@ -840,12 +1088,11 @@
 (*              Alternative Proof of MapConc                       *)
 (* --------------------------------------------------------------- *)
 
-Delsimps [MapConc];
+
 
 goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
 by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
 auto();
 qed"MapConc_takelemma";
 
-Addsimps [MapConc];
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Sequence.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
@@ -83,9 +83,4 @@
 adm_all    "adm f"
 
 
-take_reduction
-  "[| Finite x; !! k. k < n ==> seq_take k`y1 = seq_take k`y2 |]
-   ==> seq_take n`(x @@ (t>>y1)) =  seq_take n`(x @@ (t>>y2))"
-
-
 end
\ No newline at end of file
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,11 +1,214 @@
 (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1997  TU Muenchen
 
-Some properties about cut(ex), defined as follows:
+Some properties about (Cut ex), defined as follows:
 
-For every execution ex there is another shorter execution cut(ex) 
+For every execution ex there is another shorter execution (Cut ex) 
 that has the same trace as ex, but its schedule ends with an external action.
 
-*) 
\ No newline at end of file
+*) 
+
+
+
+
+(* ---------------------------------------------------------------- *)
+                   section "oraclebuild rewrite rules";
+(* ---------------------------------------------------------------- *)
+
+
+bind_thm ("oraclebuild_unfold", fix_prover2 thy oraclebuild_def 
+"oraclebuild P = (LAM s t. case t of \
+\       nil => nil\
+\    | x##xs => \
+\      (case x of\ 
+\        Undef => UU\
+\      | Def y => (Takewhile (%a.~ P a)`s)\
+\                  @@ (y>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`xs))\
+\      )\
+\    )");
+
+goal thy "oraclebuild P`sch`UU = UU";
+by (stac oraclebuild_unfold 1);
+by (Simp_tac 1);
+qed"oraclebuild_UU";
+
+goal thy "oraclebuild P`sch`nil = nil";
+by (stac oraclebuild_unfold 1);
+by (Simp_tac 1);
+qed"oraclebuild_nil";
+
+goal thy "oraclebuild P`s`(x>>t) = \
+\         (Takewhile (%a.~ P a)`s)   \
+\          @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";     
+br trans 1;
+by (stac oraclebuild_unfold 1);
+by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
+by (simp_tac (!simpset addsimps [Cons_def]) 1);
+qed"oraclebuild_cons";
+
+
+
+ 
+(* ---------------------------------------------------------------- *)
+                   section "Cut rewrite rules";
+(* ---------------------------------------------------------------- *)
+
+goalw thy [Cut_def]
+"!! s. [| Forall (%a.~ P a) s; Finite s|] \
+\           ==> Cut P s =nil";
+by (subgoal_tac "Filter P`s = nil" 1);
+by (asm_simp_tac (!simpset addsimps [oraclebuild_nil]) 1);
+br ForallQFilterPnil 1;
+by (REPEAT (atac 1));
+qed"Cut_nil";
+
+goalw thy [Cut_def]
+"!! s. [| Forall (%a.~ P a) s; ~Finite s|] \
+\           ==> Cut P s =UU";
+by (subgoal_tac "Filter P`s= UU" 1);
+by (asm_simp_tac (!simpset addsimps [oraclebuild_UU]) 1);
+br ForallQFilterPUU 1;
+by (REPEAT (atac 1));
+qed"Cut_UU";
+
+goalw thy [Cut_def]
+"!! s. [| P t;  Forall (%x.~ P x) ss; Finite ss|] \
+\           ==> Cut P (ss @@ (t>> rs)) \
+\                = ss @@ (t >> Cut P rs)";
+
+by (asm_full_simp_tac (!simpset addsimps [ForallQFilterPnil,oraclebuild_cons,
+          TakewhileConc,DropwhileConc]) 1);
+qed"Cut_Cons";
+
+
+(* ---------------------------------------------------------------- *)
+                   section "Cut lemmas for main theorem";
+(* ---------------------------------------------------------------- *)
+
+
+goal thy "Filter P`s = Filter P`(Cut P s)";
+
+by (res_inst_tac [("A1","%x.True")
+                 ,("Q1","%x.~ P x"), ("x1","s")]
+                 (take_lemma_induct RS mp) 1);
+by (Fast_tac 3);
+by (case_tac "Finite s" 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_nil,
+             ForallQFilterPnil]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_UU,
+             ForallQFilterPUU]) 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
+auto();
+qed"FilterCut";
+
+
+goal thy "Cut P (Cut P s) = (Cut P s)";
+
+by (res_inst_tac [("A1","%x.True")
+                 ,("Q1","%x.~ P x"), ("x1","s")]
+                 (take_lemma_less_induct RS mp) 1);
+by (Fast_tac 3);
+by (case_tac "Finite s" 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_nil,
+             ForallQFilterPnil]) 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_UU,
+             ForallQFilterPUU]) 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
+br take_reduction 1;
+auto();
+qed"Cut_idemp";
+
+
+goal thy "Map f`(Cut (P o f) s) = Cut P (Map f`s)";
+
+by (res_inst_tac [("A1","%x.True")
+                 ,("Q1","%x.~ P (f x)"), ("x1","s")]
+                 (take_lemma_less_induct RS mp) 1);
+by (Fast_tac 3);
+by (case_tac "Finite s" 1);
+by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1); 
+br (Cut_nil RS sym) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1); 
+by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
+(* csae ~ Finite s *)
+by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
+br (Cut_UU RS sym) 1;
+by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1); 
+by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
+(* main case *)
+by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,MapConc,
+          ForallMap,FiniteMap1,o_def]) 1);
+br take_reduction 1;
+auto();
+qed"MapCut";
+
+
+
+
+(* ---------------------------------------------------------------- *)
+                   section "Main Cut Theorem";
+(* ---------------------------------------------------------------- *)
+
+
+
+goalw thy [schedules_def,has_schedule_def]
+ "!! sch. [|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|] \
+\   ==> ? sch. sch : schedules A & \
+\              tr = Filter (%a.a:ext A)`sch &\
+\              LastActExtsch A sch";
+
+by (safe_tac set_cs);
+by (res_inst_tac [("x","filter_act`(Cut (%a.fst a:ext A) (snd ex))")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (pair_tac "ex" 1);
+by (safe_tac set_cs);
+by (res_inst_tac [("x","(x,Cut (%a.fst a:ext A) y)")] exI 1);
+by (Asm_simp_tac 1);
+
+(* Subgoal 1: Lemma:  propagation of execution through Cut *)
+
+by (asm_full_simp_tac (!simpset addsimps [execThruCut]) 1);
+
+(* Subgoal 2:  Lemma:  Filter P s = Filter P (Cut P s) *)
+
+by (simp_tac (!simpset addsimps [filter_act_def]) 1);
+by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
+br (rewrite_rule [o_def] MapCut) 2;
+by (asm_full_simp_tac (!simpset addsimps [FilterCut RS sym]) 1);
+
+(* Subgoal 3: Lemma: Cut idempotent  *)
+
+by (simp_tac (!simpset addsimps [LastActExtsch_def,filter_act_def]) 1);
+by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
+br (rewrite_rule [o_def] MapCut) 2;
+by (asm_full_simp_tac (!simpset addsimps [Cut_idemp]) 1);
+qed"exists_LastActExtsch";
+
+
+(* ---------------------------------------------------------------- *)
+                   section "Further Cut lemmas";
+(* ---------------------------------------------------------------- *)
+
+goalw  thy [LastActExtsch_def]
+  "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = nil |] \
+\   ==> sch=nil";
+bd FilternPnilForallP 1;
+be conjE 1;
+bd Cut_nil 1;
+ba 1;
+by (Asm_full_simp_tac 1);
+qed"LastActExtimplnil";
+
+goalw  thy [LastActExtsch_def]
+  "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = UU |] \
+\   ==> sch=UU";
+bd FilternPUUForallP 1;
+be conjE 1;
+bd Cut_UU 1;
+ba 1;
+by (Asm_full_simp_tac 1);
+qed"LastActExtimplUU";
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,11 +1,11 @@
 (*  Title:      HOLCF/IOA/meta_theory/ShortExecutions.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1997  TU Muenchen
 
-Some properties about cut(ex), defined as follows:
+Some properties about (Cut ex), defined as follows:
 
-For every execution ex there is another shorter execution cut(ex) 
+For every execution ex there is another shorter execution (Cut ex) 
 that has the same trace as ex, but its schedule ends with an external action.
 
 *) 
@@ -15,40 +15,48 @@
 
 consts 
 
-  LastActExtsch     ::"'a Seq  => bool"
-  cutsch            ::"'a Seq => 'a Seq"
+  LastActExtex      ::"('a,'s)ioa => ('a,'s) pairs  => bool"
+  LastActExtsch     ::"('a,'s)ioa => 'a Seq         => bool"
 
+  Cut               ::"('a => bool) => 'a Seq    => 'a Seq"
+ 
+  oraclebuild       ::"('a => bool) => 'a Seq -> 'a Seq -> 'a Seq"
 
 defs
 
 LastActExtsch_def
-  "LastActExtsch sch == (cutsch sch = sch)"
+  "LastActExtsch A sch == (Cut (%x.x: ext A) sch = sch)"
+
+LastActExtex_def
+  "LastActExtex A ex == LastActExtsch A (filter_act`ex)"
+
+Cut_def
+  "Cut P s == oraclebuild P`s`(Filter P`s)"
+
+oraclebuild_def
+  "oraclebuild P == (fix`(LAM h s t. case t of 
+       nil => nil
+    | x##xs => 
+      (case x of 
+        Undef => UU
+      | Def y => (Takewhile (%x.~P x)`s)
+                  @@ (y>>(h`(TL`(Dropwhile (%x.~ P x)`s))`xs))
+      )
+    ))"
+
+
 
 
 rules
 
-exists_LastActExtsch
-  "[|sch : schedules A ; tr = Filter (%a.a:ext A)`sch|]
-   ==> ? sch. sch : schedules A & 
-              tr = Filter (%a.a:ext A)`sch &
-              LastActExtsch sch"
-
-(* FIX: 1. LastActExtsch should have argument A also? 
-        2. use equality: (I) f P x =UU <-> (II) (fa ~P x) & ~finite(x) to prove it for (II) instead *)
-LastActExtimplUU
-  "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = UU |]
-   ==> sch=UU"
-
-(* FIX: see above *)
-LastActExtimplnil
-  "[|LastActExtsch sch; Filter (%x.x:ext A)`sch = nil |]
-   ==> sch=nil"
+execThruCut
+  "is_execution_fragment A (s,ex) ==> is_execution_fragment A (s,Cut P ex)"
 
 LastActExtsmall1
-  "LastActExtsch sch ==> LastActExtsch (TL`(Dropwhile P`sch))"
+  "LastActExtsch A sch ==> LastActExtsch A (TL`(Dropwhile P`sch))"
 
 LastActExtsmall2
-  "[| Finite sch1; LastActExtsch (sch1 @@ sch2) |] ==> LastActExtsch (sch2)"
+  "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
 
 end
 
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Traces.ML
--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,12 +1,12 @@
 (*  Title:      HOLCF/IOA/meta_theory/Traces.ML
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
 Theorems about Executions and Traces of I/O automata in HOLCF.
 *)   
 
-
+Delsimps (ex_simps @ all_simps);
 
 val exec_rws = [executions_def,is_execution_fragment_def];
 
@@ -150,3 +150,58 @@
 by (REPEAT (Asm_simp_tac 1));
 qed"has_trace_def2";
 
+
+(* -------------------------------------------------------------------------------- *)
+
+section "signatures and executions, schedules";
+
+
+(* All executions of A have only actions of A. This is only true because of the 
+   predicate state_trans (part of the predicate IOA): We have no dependent types.
+   For executions of parallel automata this assumption is not needed, as in par_def
+   this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
+
+goal thy 
+  "!! A. IOA A ==> \
+\ ! s. is_execution_fragment A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
+
+by (pair_induct_tac "xs" [is_execution_fragment_def,Forall_def,sforall_def] 1);
+(* main case *)
+ren "ss a t" 1;
+by (safe_tac set_cs);
+by (REPEAT (asm_full_simp_tac (!simpset addsimps [ioa_def,state_trans_def]) 1));
+qed"execfrag_in_sig";
+
+goal thy 
+  "!! A.[|  IOA A; x:executions A |] ==> \
+\ Forall (%a.a:act A) (filter_act`(snd x))";
+
+by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
+by (pair_tac "x" 1);
+br (execfrag_in_sig RS spec RS mp) 1;
+auto();
+qed"exec_in_sig";
+
+goalw thy [schedules_def,has_schedule_def]
+  "!! A.[|  IOA A; x:schedules A |] ==> \
+\   Forall (%a.a:act A) x";
+
+by (fast_tac (!claset addSIs [exec_in_sig]) 1);
+qed"scheds_in_sig";
+
+
+(* -------------------------------------------------------------------------------- *)
+
+section "executions are prefix closed";
+
+(* only admissible in y, not if done in x !! *)
+goal thy "!x s. is_execution_fragment A (s,x) & y<<x  --> is_execution_fragment A (s,y)";
+by (pair_induct_tac "y" [is_execution_fragment_def] 1);
+by (strip_tac 1);
+by (Seq_case_simp_tac "xa" 1);
+by (pair_tac "a" 1);
+auto();
+qed"execfrag_prefixclosed";
+
+bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
+
diff -r 70939b0fadfb -r 3f53f2c876f4 src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Traces.thy
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
@@ -7,7 +7,7 @@
 *)   
 
 		       
-Traces = Automata + Sequence +
+Traces = Sequence + Automata +
 
 default term