# HG changeset patch
# User mueller
# Date 869136212 -7200
# Node ID bdc51b4c6050a8d5b936b0c6160ea98d6284d0d1
# Parent  5b5807645a1a78b6ef8015086c4ce205743f2202
changes needed for adding fairness

diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Thu Jul 17 12:43:32 1997 +0200
@@ -11,7 +11,7 @@
 
 open reachable;
 
-val ioa_projections = [asig_of_def, starts_of_def, trans_of_def];
+val ioa_projections = [asig_of_def, starts_of_def, trans_of_def,wfair_of_def,sfair_of_def];
 
 (* ----------------------------------------------------------------------------------- *)
 
@@ -19,12 +19,16 @@
 
 
 goal thy
-"asig_of((x,y,z)) = x & starts_of((x,y,z)) = y & trans_of((x,y,z)) = z";
+ "((asig_of (x,y,z,w,s)) = x)   & \
+\ ((starts_of (x,y,z,w,s)) = y) & \
+\ ((trans_of (x,y,z,w,s)) = z)  & \
+\ ((wfair_of (x,y,z,w,s)) = w) & \
+\ ((sfair_of (x,y,z,w,s)) = s)";
   by (simp_tac (!simpset addsimps ioa_projections) 1);
 qed "ioa_triple_proj";
 
-goalw thy [ioa_def,state_trans_def,actions_def, is_asig_def]
-  "!!A. [| IOA(A); (s1,a,s2):trans_of(A) |] ==> a:act A";
+goalw thy [is_trans_of_def,actions_def, is_asig_def]
+  "!!A. [| is_trans_of A; (s1,a,s2):trans_of(A) |] ==> a:act A";
   by (REPEAT(etac conjE 1));
   by (EVERY1[etac allE, etac impE, atac]);
   by (Asm_full_simp_tac 1);
@@ -35,6 +39,20 @@
   by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
 qed "starts_of_par";
 
+goal thy
+"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr)) \       
+\            in (a:act A | a:act B) & \
+\               (if a:act A then       \                
+\                  (fst(s),a,fst(t)):trans_of(A) \                    
+\                else fst(t) = fst(s))            \                      
+\               &                                  \                     
+\               (if a:act B then                    \   
+\                  (snd(s),a,snd(t)):trans_of(B)     \                
+\                else snd(t) = snd(s))}";
+
+by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+qed "trans_of_par";
+
 
 (* ----------------------------------------------------------------------------------- *)
 
@@ -70,7 +88,6 @@
 by (fast_tac set_cs 1);
 qed"actions_of_par"; 
 
-
 goal thy "inp (A1||A2) =\
 \         ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))";
 by (asm_full_simp_tac (!simpset addsimps [actions_def,asig_of_par,asig_comp_def,
@@ -121,6 +138,7 @@
 by (best_tac (set_cs addEs [equalityCE]) 1);
 qed"intA_is_not_actB";
 
+(* the only one that needs disjointness of outputs and of internals and _all_ acts *)
 goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
     compatible_def,is_asig_def,asig_of_def]
 "!! a. [| compatible A B; a:out A ;a:act B|] ==> a : inp B";
@@ -128,7 +146,85 @@
 by (best_tac (set_cs addEs [equalityCE]) 1);
 qed"outAactB_is_inpB";
 
+(* needed for propagation of input_enabledness from A,B to A||B *)
+goalw thy [asig_outputs_def,asig_internals_def,actions_def,asig_inputs_def,
+    compatible_def,is_asig_def,asig_of_def]
+"!! a. [| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B";
+by (Asm_full_simp_tac 1);
+by (best_tac (set_cs addEs [equalityCE]) 1);
+qed"inpAAactB_is_inpBoroutB";
 
+(* ---------------------------------------------------------------------------------- *)
+
+section "input_enabledness and par";  
+
+
+(* ugly case distinctions. Heart of proof: 
+     1. inpAAactB_is_inpBoroutB ie. internals are really hidden.
+     2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
+goalw thy [input_enabled_def] 
+"!!A. [| compatible A B; input_enabled A; input_enabled B|] \
+\     ==> input_enabled (A||B)";
+by (asm_full_simp_tac (!simpset addsimps [inputs_of_par,trans_of_par]) 1);
+by (safe_tac set_cs);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 2);
+(* a: inp A *)
+by (case_tac "a:act B" 1);
+(* a:act B *)
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+bd inpAAactB_is_inpBoroutB 1;
+ba 1;
+ba 1;
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","aa")] allE 1);
+by (eres_inst_tac [("x","b")] allE 1);
+be exE 1;
+be exE 1;
+by (res_inst_tac [("x","(s2,s2a)")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+(* a~: act B*)
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","aa")] allE 1);
+be exE 1;
+by (res_inst_tac [("x","(s2,b)")] exI 1);
+by (Asm_full_simp_tac 1);
+
+(* a:inp B *)
+by (case_tac "a:act A" 1);
+(* a:act A *)
+by (eres_inst_tac [("x","a")] allE 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
+bd inpAAactB_is_inpBoroutB 1;
+back();
+ba 1;
+ba 1;
+by (Asm_full_simp_tac 1);
+by (rotate_tac ~1 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","aa")] allE 1);
+by (eres_inst_tac [("x","b")] allE 1);
+be exE 1;
+be exE 1;
+by (res_inst_tac [("x","(s2,s2a)")] exI 1);
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+(* a~: act B*)
+by (asm_full_simp_tac (!simpset addsimps [inp_is_act]) 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","a")] allE 1);
+by (Asm_full_simp_tac 1);
+by (eres_inst_tac [("x","b")] allE 1);
+be exE 1;
+by (res_inst_tac [("x","(aa,s2)")] exI 1);
+by (Asm_full_simp_tac 1);
+qed"input_enabled_par";
 
 (* ---------------------------------------------------------------------------------- *)
 
@@ -288,4 +384,55 @@
 qed "trans_of_par4";
 
 
+(* ---------------------------------------------------------------------------------- *)
 
+section "proof obligation generator for IOA requirements";  
+
+(* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
+goalw thy [is_trans_of_def] 
+"is_trans_of (A||B)";
+by (simp_tac (!simpset addsimps [actions_of_par,trans_of_par]) 1);
+qed"is_trans_of_par";
+
+
+(*
+
+goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
+"!!A. is_trans_of A ==> is_trans_of (restrict A acts)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def,
+    asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,asig_of_def]) 1);
+
+qed"";
+
+
+goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
+"!!A. is_trans_of A ==> is_trans_of (rename A f)";
+by (asm_full_simp_tac (!simpset addsimps [actions_def,trans_of_def,
+    asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,asig_of_def]) 1);
+
+qed"";
+
+goal thy "!! A. is_asig_of A ==> is_asig_of (rename A f)";
+
+
+goalw thy [is_asig_of_def,is_asig_def,asig_of_def,restrict_def,restrict_asig_def,
+           asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def] 
+"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
+by (Asm_full_simp_tac 1);
+
+
+
+
+goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
+\         ==> is_asig_of (A||B)";
+
+
+
+
+
+*)
+
+
+
+
+
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOLCF/IOA/meta_theory/Automata.thy	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.thy	Thu Jul 17 12:43:32 1997 +0200
@@ -13,17 +13,24 @@
  
 types
    ('a,'s)transition       =    "'s * 'a * 's"
-   ('a,'s)ioa              =    "'a signature * 's set * ('a,'s)transition set"
+   ('a,'s)ioa              =    "'a signature * 's set * ('a,'s)transition set * 
+                                 (('a set) set) * (('a set) set)"
 
 consts
  
   (* IO automata *)
-  state_trans  ::"['a signature, ('a,'s)transition set] => bool"
-  input_enabled::"['a signature, ('a,'s)transition set] => bool"
-  asig_of      ::"('a,'s)ioa => 'a signature"
-  starts_of    ::"('a,'s)ioa => 's set"
-  trans_of     ::"('a,'s)ioa => ('a,'s)transition set"
-  IOA	       ::"('a,'s)ioa => bool"
+
+  asig_of        ::"('a,'s)ioa => 'a signature"
+  starts_of      ::"('a,'s)ioa => 's set"
+  trans_of       ::"('a,'s)ioa => ('a,'s)transition set"
+  wfair_of       ::"('a,'s)ioa => ('a set) set"
+  sfair_of       ::"('a,'s)ioa => ('a set) set"
+
+  is_asig_of     ::"('a,'s)ioa => bool"
+  is_starts_of	 ::"('a,'s)ioa => bool"
+  is_trans_of	 ::"('a,'s)ioa => bool"
+  input_enabled	 ::"('a,'s)ioa => bool"
+  IOA	         ::"('a,'s)ioa => bool"
 
   (* reachability and invariants *)
   reachable     :: "('a,'s)ioa => 's set"
@@ -31,15 +38,18 @@
 
   (* binary composition of action signatures and automata *)
   asig_comp    ::"['a signature, 'a signature] => 'a signature"
-  compatible  ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
+  compatible   ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
   "||"         ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr 10)
 
-  (* hiding *)
+  (* hiding and restricting *)
+  hide_asig     :: "['a signature, 'a set] => 'a signature"
+  hide          :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
   restrict_asig :: "['a signature, 'a set] => 'a signature"
   restrict      :: "[('a,'s)ioa, 'a set] => ('a,'s)ioa"
 
   (* renaming *)
-  rename:: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
+  rename_set    :: "'a set => ('c => 'a option) => 'c set"
+  rename        :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
 
 
 syntax 
@@ -83,24 +93,34 @@
 
 (* --------------------------------- IOA ---------------------------------*)
 
-state_trans_def
-  "state_trans asig R == 
-    (!triple. triple:R --> fst(snd(triple)):actions(asig))"
-
-input_enabled_def
-  "input_enabled asig R ==
-    (!a. (a:inputs(asig)) --> (!s1. ? s2. (s1,a,s2):R))" 
 
 
 asig_of_def   "asig_of == fst"
 starts_of_def "starts_of == (fst o snd)"
-trans_of_def  "trans_of == (snd o snd)"
+trans_of_def  "trans_of == (fst o snd o snd)"
+wfair_of_def  "wfair_of == (fst o snd o snd o snd)"
+sfair_of_def  "sfair_of == (snd o snd o snd o snd)"
+
+is_asig_of_def
+  "is_asig_of A == is_asig (asig_of A)" 
+
+is_starts_of_def 
+  "is_starts_of A ==  (~ starts_of A = {})"
+
+is_trans_of_def
+  "is_trans_of A == 
+    (!triple. triple:(trans_of A) --> fst(snd(triple)):actions(asig_of A))"
+
+input_enabled_def
+  "input_enabled A ==
+    (!a. (a:inputs(asig_of A)) --> (!s1. ? s2. (s1,a,s2):(trans_of A)))" 
+
 
 ioa_def
-  "IOA(ioa) == (is_asig(asig_of(ioa))      &                            
-                (~ starts_of(ioa) = {})    &                            
-                state_trans (asig_of ioa) (trans_of ioa) &
-                input_enabled (asig_of ioa) (trans_of ioa))"
+  "IOA A == (is_asig_of A    &                            
+             is_starts_of A  &                            
+             is_trans_of A   &
+             input_enabled A)"
 
 
 invariant_def "invariant A P == (!s. reachable A s --> P(s))"
@@ -121,44 +141,73 @@
        (outputs(a1) Un outputs(a2)),                                   
        (internals(a1) Un internals(a2))))"
 
-
 par_def
-  "(ioa1 || ioa2) ==                                                    
-      (asig_comp (asig_of ioa1) (asig_of ioa2),                        
-       {pr. fst(pr):starts_of(ioa1) & snd(pr):starts_of(ioa2)},        
+  "(A || B) ==                                                    
+      (asig_comp (asig_of A) (asig_of B),                        
+       {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)},        
        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))        
-            in (a:act ioa1 | a:act ioa2) & 
-               (if a:act ioa1 then                       
-                  (fst(s),a,fst(t)):trans_of(ioa1)                     
+            in (a:act A | a:act B) & 
+               (if a:act A then                       
+                  (fst(s),a,fst(t)):trans_of(A)                     
                 else fst(t) = fst(s))                                  
                &                                                       
-               (if a:act ioa2 then                       
-                  (snd(s),a,snd(t)):trans_of(ioa2)                     
-                else snd(t) = snd(s))})"
+               (if a:act B then                       
+                  (snd(s),a,snd(t)):trans_of(B)                     
+                else snd(t) = snd(s))},
+        wfair_of A Un wfair_of B,
+        sfair_of A Un sfair_of B)"
+
 
 (* ------------------------ hiding -------------------------------------------- *)
 
 restrict_asig_def
   "restrict_asig asig actns ==                                          
-    (inputs(asig) Int actns, outputs(asig) Int actns,                  
+    (inputs(asig) Int actns, 
+     outputs(asig) Int actns,                  
      internals(asig) Un (externals(asig) - actns))"
 
+(* Notice that for wfair_of and sfair_of nothing has to be changed, as 
+   changes from the outputs to the internals does not touch the locals as 
+   a whole, which is of importance for fairness only *)
 
 restrict_def
-  "restrict ioa actns ==                                               
-    (restrict_asig (asig_of ioa) actns, starts_of(ioa), trans_of(ioa))"
+  "restrict A actns ==                                               
+    (restrict_asig (asig_of A) actns, 
+     starts_of A, 
+     trans_of A,
+     wfair_of A,
+     sfair_of A)"
+
+hide_asig_def
+  "hide_asig asig actns ==                                          
+    (inputs(asig) - actns, 
+     outputs(asig) - actns,                  
+     internals(asig) Un actns)"
+
+hide_def
+  "hide A actns ==                                               
+    (hide_asig (asig_of A) actns, 
+     starts_of A, 
+     trans_of A,
+     wfair_of A,
+     sfair_of A)"
 
 (* ------------------------- renaming ------------------------------------------- *)
   
+rename_set_def
+  "rename_set set ren == {b. ? x. Some x = ren b & x : set}" 
+
 rename_def 
 "rename ioa ren ==  
-  (({b. ? x. Some(x)= ren(b) & x : inp ioa},         
-    {b. ? x. Some(x)= ren(b) & x : out ioa},        
-    {b. ? x. Some(x)= ren(b) & x : int ioa}),     
-              starts_of(ioa)   ,                                            
+  ((rename_set (inp ioa) ren,         
+    rename_set (out ioa) ren,        
+    rename_set (int ioa) ren),     
+   starts_of ioa,                                            
    {tr. let s = fst(tr); a = fst(snd(tr));  t = snd(snd(tr))    
         in                                                      
-        ? x. Some(x) = ren(a) & (s,x,t):trans_of(ioa)})"
+        ? x. Some(x) = ren(a) & (s,x,t):trans_of ioa},
+   {rename_set s ren | s. s: wfair_of ioa},
+   {rename_set s ren | s. s: sfair_of ioa})"
 
 
 end
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Thu Jul 17 12:43:32 1997 +0200
@@ -57,18 +57,18 @@
 (* ---------------------------------------------------------------- *)
 
 
-goal thy "Filter_ex2 A`UU=UU";
+goal thy "Filter_ex2 sig`UU=UU";
 by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_UU";
 
-goal thy "Filter_ex2 A`nil=nil";
+goal thy "Filter_ex2 sig`nil=nil";
 by (simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_nil";
 
-goal thy "Filter_ex2 A`(at >> xs) =    \
-\            (if (fst at:act A)    \       
-\                 then at >> (Filter_ex2 A`xs) \   
-\                 else        Filter_ex2 A`xs)";
+goal thy "Filter_ex2 sig`(at >> xs) =    \
+\            (if (fst at:actions sig)    \       
+\                 then at >> (Filter_ex2 sig`xs) \   
+\                 else        Filter_ex2 sig`xs)";
 
 by (asm_full_simp_tac (!simpset addsimps [Filter_ex2_def]) 1);
 qed"Filter_ex2_cons";
@@ -79,13 +79,13 @@
 (* ---------------------------------------------------------------- *)
 
 
-goal thy "stutter2 A = (LAM ex. (%s. case ex of \
+goal thy "stutter2 sig = (LAM ex. (%s. case ex of \
 \      nil => TT \
 \    | x##xs => (flift1 \ 
-\            (%p.(If Def ((fst p)~:act A) \
+\            (%p.(If Def ((fst p)~:actions sig) \
 \                 then Def (s=(snd p)) \
 \                 else TT fi) \
-\                andalso (stutter2 A`xs) (snd p))  \
+\                andalso (stutter2 sig`xs) (snd p))  \
 \             `x) \
 \           ))";
 by (rtac trans 1);
@@ -95,20 +95,20 @@
 by (simp_tac (!simpset addsimps [flift1_def]) 1);
 qed"stutter2_unfold";
 
-goal thy "(stutter2 A`UU) s=UU";
+goal thy "(stutter2 sig`UU) s=UU";
 by (stac stutter2_unfold 1);
 by (Simp_tac 1);
 qed"stutter2_UU";
 
-goal thy "(stutter2 A`nil) s = TT";
+goal thy "(stutter2 sig`nil) s = TT";
 by (stac stutter2_unfold 1);
 by (Simp_tac 1);
 qed"stutter2_nil";
 
-goal thy "(stutter2 A`(at>>xs)) s = \
-\              ((if (fst at)~:act A then Def (s=snd at) else TT) \
-\                andalso (stutter2 A`xs) (snd at))"; 
-by (rtac trans 1);
+goal thy "(stutter2 sig`(at>>xs)) s = \
+\              ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
+\                andalso (stutter2 sig`xs) (snd at))"; 
+br trans 1;
 by (stac stutter2_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1);
 by (Simp_tac 1);
@@ -122,16 +122,16 @@
 (*                             stutter                              *)
 (* ---------------------------------------------------------------- *)
 
-goal thy "stutter A (s, UU)";
+goal thy "stutter sig (s, UU)";
 by (simp_tac (!simpset addsimps [stutter_def]) 1);
 qed"stutter_UU";
 
-goal thy "stutter A (s, nil)";
+goal thy "stutter sig (s, nil)";
 by (simp_tac (!simpset addsimps [stutter_def]) 1);
 qed"stutter_nil";
 
-goal thy "stutter A (s, (a,t)>>ex) = \
-\     ((a~:act A --> (s=t)) & stutter A (t,ex))";
+goal thy "stutter sig (s, (a,t)>>ex) = \
+\     ((a~:actions sig --> (s=t)) & stutter sig (t,ex))";
 by (simp_tac (!simpset addsimps [stutter_def] 
                        setloop (split_tac [expand_if]) ) 1);
 qed"stutter_cons";
@@ -160,8 +160,8 @@
 (* --------------------------------------------------------------------- *)
 
 goal thy "!s. is_exec_frag (A||B) (s,xs) \
-\      -->  is_exec_frag A (fst s, Filter_ex2 A`(ProjA2`xs)) &\
-\           is_exec_frag B (snd s, Filter_ex2 B`(ProjB2`xs))";
+\      -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
+\           is_exec_frag B (snd s, Filter_ex2 (asig_of B)`(ProjB2`xs))";
 
 by (pair_induct_tac "xs" [is_exec_frag_def] 1);
 (* main case *)
@@ -177,8 +177,8 @@
 (* --------------------------------------------------------------------- *)
 
 goal thy "!s. is_exec_frag (A||B) (s,xs) \
-\      --> stutter A (fst s,ProjA2`xs)  &\
-\          stutter B (snd s,ProjB2`xs)"; 
+\      --> stutter (asig_of A) (fst s,ProjA2`xs)  &\
+\          stutter (asig_of B) (snd s,ProjB2`xs)"; 
 
 by (pair_induct_tac "xs" [stutter_def,is_exec_frag_def] 1);
 (* main case *)
@@ -208,10 +208,10 @@
 (* ----------------------------------------------------------------------- *)
 
 goal thy 
-"!s. is_exec_frag A (fst s,Filter_ex2 A`(ProjA2`xs)) &\
-\    is_exec_frag B (snd s,Filter_ex2 B`(ProjB2`xs)) &\
-\    stutter A (fst s,(ProjA2`xs)) & \
-\    stutter B (snd s,(ProjB2`xs)) & \
+"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)`(ProjA2`xs)) &\
+\    is_exec_frag B (snd s,Filter_ex2 (asig_of B)`(ProjB2`xs)) &\
+\    stutter (asig_of A) (fst s,(ProjA2`xs)) & \
+\    stutter (asig_of B) (snd s,(ProjB2`xs)) & \
 \    Forall (%x.fst x:act (A||B)) xs \
 \    --> is_exec_frag (A||B) (s,xs)";
 
@@ -239,9 +239,9 @@
 
 goal thy 
 "ex:executions(A||B) =\
-\(Filter_ex A (ProjA ex) : executions A &\
-\ Filter_ex B (ProjB ex) : executions B &\
-\ stutter A (ProjA ex) & stutter B (ProjB ex) &\
+\(Filter_ex (asig_of A) (ProjA ex) : executions A &\
+\ Filter_ex (asig_of B) (ProjB ex) : executions B &\
+\ stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &\
 \ Forall (%x.fst x:act (A||B)) (snd ex))";
 
 by (simp_tac (!simpset addsimps [executions_def,ProjB_def,
@@ -258,5 +258,23 @@
 qed"compositionality_ex";
 
 
+(* ------------------------------------------------------------------ *)
+(*           COMPOSITIONALITY   on    EXECUTION     Level             *)
+(*                            For Modules                             *)
+(* ------------------------------------------------------------------ *)
+
+goalw thy [Execs_def,par_execs_def]
+
+"Execs (A||B) = par_execs (Execs A) (Execs B)";
+
+by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
+br set_ext 1;
+by (asm_full_simp_tac (!simpset addsimps [compositionality_ex,actions_of_par]) 1);
+qed"compositionality_ex_modules";
 
 
+
+
+
+
+
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.thy	Thu Jul 17 12:43:32 1997 +0200
@@ -15,10 +15,12 @@
  ProjA2     ::"('a,'s * 't)pairs     -> ('a,'s)pairs"
  ProjB      ::"('a,'s * 't)execution => ('a,'t)execution"
  ProjB2     ::"('a,'s * 't)pairs     -> ('a,'t)pairs"
- Filter_ex  ::"('a,'s)ioa => ('a,'s)execution => ('a,'s)execution"
- Filter_ex2 ::"('a,'s)ioa => ('a,'s)pairs     -> ('a,'s)pairs" 
- stutter    ::"('a,'s)ioa => ('a,'s)execution => bool" 
- stutter2   ::"('a,'s)ioa => ('a,'s)pairs     -> ('s => tr)"
+ Filter_ex  ::"'a signature => ('a,'s)execution => ('a,'s)execution"
+ Filter_ex2 ::"'a signature => ('a,'s)pairs     -> ('a,'s)pairs" 
+ stutter    ::"'a signature => ('a,'s)execution => bool" 
+ stutter2   ::"'a signature => ('a,'s)pairs     -> ('s => tr)"
+
+ par_execs  ::"[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module"
 
 
 defs 
@@ -39,27 +41,36 @@
  
 
 Filter_ex_def
-  "Filter_ex A ex == (fst ex,Filter_ex2 A`(snd ex))"
+  "Filter_ex sig ex == (fst ex,Filter_ex2 sig`(snd ex))"
 
 
 Filter_ex2_def
-  "Filter_ex2 A ==  Filter (%x.fst x:act A)"
+  "Filter_ex2 sig ==  Filter (%x.fst x:actions sig)"
 
 stutter_def
-  "stutter A ex == ((stutter2 A`(snd ex)) (fst ex) ~= FF)"
+  "stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)"
 
 stutter2_def
-  "stutter2 A ==(fix`(LAM h ex. (%s. case ex of 
+  "stutter2 sig ==(fix`(LAM h ex. (%s. case ex of 
       nil => TT
     | x##xs => (flift1 
-            (%p.(If Def ((fst p)~:act A)
+            (%p.(If Def ((fst p)~:actions sig)
                  then Def (s=(snd p)) 
                  else TT fi)
                 andalso (h`xs) (snd p)) 
              `x)
    )))" 
 
-
-
+par_execs_def
+  "par_execs ExecsA ExecsB == 
+       let exA = fst ExecsA; sigA = snd ExecsA; 
+           exB = fst ExecsB; sigB = snd ExecsB       
+       in
+       (    {ex. Filter_ex sigA (ProjA ex) : exA}
+        Int {ex. Filter_ex sigB (ProjB ex) : exB}
+        Int {ex. stutter sigA (ProjA ex)}
+        Int {ex. stutter sigB (ProjB ex)}
+        Int {ex. Forall (%x.fst x:(actions sigA Un actions sigB)) (snd ex)},
+        asig_comp sigA sigB)"
 
 end
\ No newline at end of file
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Thu Jul 17 12:43:32 1997 +0200
@@ -159,7 +159,7 @@
 (* --------------------------------------------------------------------- *)
 
 goalw thy [filter_act_def,Filter_ex2_def]
-   "filter_act`(Filter_ex2 A`xs)=\
+   "filter_act`(Filter_ex2 (asig_of A)`xs)=\
 \   Filter (%a.a:act A)`(filter_act`xs)";
 
 by (simp_tac (!simpset addsimps [MapFilter,o_def]) 1);
@@ -273,7 +273,7 @@
 \ Forall (%x.x:act (A||B)) sch & \
 \ Filter (%a.a:act A)`sch << filter_act`exA &\
 \ Filter (%a.a:act B)`sch << filter_act`exB \
-\ --> stutter A (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
+\ --> stutter (asig_of A) (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
 
 by (mkex_induct_tac "sch" "exA" "exB");
 
@@ -284,7 +284,7 @@
 \ Forall (%x.x:act (A||B)) sch ; \
 \ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
 \ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
-\ ==> stutter A (ProjA (mkex A B sch exA exB))";
+\ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
 
 by (cut_facts_tac [stutterA_mkex] 1);
 by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
@@ -304,7 +304,7 @@
 \ Forall (%x.x:act (A||B)) sch & \
 \ Filter (%a.a:act A)`sch << filter_act`exA &\
 \ Filter (%a.a:act B)`sch << filter_act`exB \
-\ --> stutter B (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
+\ --> stutter (asig_of B) (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
 
 by (mkex_induct_tac "sch" "exA" "exB");
 
@@ -315,7 +315,7 @@
 \ Forall (%x.x:act (A||B)) sch ; \
 \ Filter (%a.a:act A)`sch << filter_act`(snd exA) ;\
 \ Filter (%a.a:act B)`sch << filter_act`(snd exB) |] \
-\ ==> stutter B (ProjB (mkex A B sch exA exB))";
+\ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
 
 by (cut_facts_tac [stutterB_mkex] 1);
 by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
@@ -337,7 +337,7 @@
 \ Forall (%x.x:act (A||B)) sch & \
 \ Filter (%a.a:act A)`sch << filter_act`exA  &\
 \ Filter (%a.a:act B)`sch << filter_act`exB \
-\ --> Filter_ex2 A`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
+\ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
 \     Zip`(Filter (%a.a:act A)`sch)`(Map snd`exA)";
 
 by (mkex_induct_tac "sch" "exA" "exB");
@@ -376,7 +376,7 @@
 \ [| Forall (%a.a:act (A||B)) sch ; \
 \ Filter (%a.a:act A)`sch = filter_act`(snd exA)  ;\
 \ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
-\ ==> Filter_ex A (ProjA (mkex A B sch exA exB)) = exA";
+\ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
 by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
 by (pair_tac "exA" 1);
 by (pair_tac "exB" 1);
@@ -401,7 +401,7 @@
 \ Forall (%x.x:act (A||B)) sch & \
 \ Filter (%a.a:act A)`sch << filter_act`exA  &\
 \ Filter (%a.a:act B)`sch << filter_act`exB \
-\ --> Filter_ex2 B`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
+\ --> Filter_ex2 (asig_of B)`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
 \     Zip`(Filter (%a.a:act B)`sch)`(Map snd`exB)";
 
 (* notice necessary change of arguments exA and exB *)
@@ -420,7 +420,7 @@
 \ [| Forall (%a.a:act (A||B)) sch ; \
 \ Filter (%a.a:act A)`sch = filter_act`(snd exA)  ;\
 \ Filter (%a.a:act B)`sch = filter_act`(snd exB) |]\
-\ ==> Filter_ex B (ProjB (mkex A B sch exA exB)) = exB";
+\ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
 by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
 by (pair_tac "exA" 1);
 by (pair_tac "exB" 1);
@@ -463,11 +463,11 @@
 by (simp_tac (!simpset addsimps [schedules_def, has_schedule_def]) 1);
 by (safe_tac set_cs); 
 (* ==> *) 
-by (res_inst_tac [("x","Filter_ex A (ProjA ex)")] bexI 1);
+by (res_inst_tac [("x","Filter_ex (asig_of A) (ProjA ex)")] bexI 1);
 by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
 by (simp_tac (!simpset addsimps [Filter_ex_def,ProjA_def,
                                  lemma_2_1a,lemma_2_1b]) 1); 
-by (res_inst_tac [("x","Filter_ex B (ProjB ex)")] bexI 1);
+by (res_inst_tac [("x","Filter_ex (asig_of B) (ProjB ex)")] bexI 1);
 by (asm_full_simp_tac (!simpset addsimps [compositionality_ex]) 2);
 by (simp_tac (!simpset addsimps [Filter_ex_def,ProjB_def,
                                  lemma_2_1a,lemma_2_1b]) 1);
@@ -498,6 +498,20 @@
 qed"compositionality_sch";
 
 
+(* ------------------------------------------------------------------ *)
+(*           COMPOSITIONALITY   on    SCHEDULE      Level             *)
+(*                            For Modules                             *)
+(* ------------------------------------------------------------------ *)
+
+goalw thy [Scheds_def,par_scheds_def]
+
+"Scheds (A||B) = par_scheds (Scheds A) (Scheds B)";
+
+by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
+br set_ext 1;
+by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,actions_of_par]) 1);
+qed"compositionality_sch_modules";
+
 
 Delsimps compoex_simps;
 Delsimps composch_simps;
\ No newline at end of file
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Jul 17 12:43:32 1997 +0200
@@ -17,6 +17,8 @@
  mkex2    ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 
               ('a,'s)pairs -> ('a,'t)pairs -> 
               ('s => 't => ('a,'s*'t)pairs)"
+ par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module"
+
 
 
 defs
@@ -60,4 +62,14 @@
          )
        ))))"
 
-end
\ No newline at end of file
+par_scheds_def
+  "par_scheds SchedsA SchedsB == 
+       let schA = fst SchedsA; sigA = snd SchedsA; 
+           schB = fst SchedsB; sigB = snd SchedsB       
+       in
+       (    {sch. Filter (%a.a:actions sigA)`sch : schA}
+        Int {sch. Filter (%a.a:actions sigB)`sch : schB}
+        Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
+        asig_comp sigA sigB)"
+
+end
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Thu Jul 17 12:43:32 1997 +0200
@@ -1170,7 +1170,7 @@
 (* ------------------------------------------------------------------ *)
  
 goal thy 
-"!! A B. [| IOA A; IOA B; compatible A B; compatible B A; \
+"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
 \           is_asig(asig_of A); is_asig(asig_of B)|] \
 \       ==>  tr: traces(A||B) = \
 \            (Filter (%a.a:act A)`tr : traces A &\
@@ -1227,9 +1227,25 @@
 
 
 
+(* ------------------------------------------------------------------ *)
+(*           COMPOSITIONALITY   on    TRACE         Level             *)
+(*                            For Modules                             *)
+(* ------------------------------------------------------------------ *)
+
+goalw thy [Traces_def,par_traces_def]
+
+"!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
+\           is_asig(asig_of A); is_asig(asig_of B)|] \
+\==> Traces (A||B) = par_traces (Traces A) (Traces B)";
+
+by (asm_full_simp_tac (!simpset addsimps [asig_of_par]) 1);
+br set_ext 1;
+by (asm_full_simp_tac (!simpset addsimps [compositionality_tr,externals_of_par]) 1);
+qed"compositionality_tr_modules";
 
 
 
 
 
 
+
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.thy	Thu Jul 17 12:43:32 1997 +0200
@@ -11,8 +11,8 @@
 
 consts  
 
- mksch     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" 
-
+ mksch      ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" 
+ par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
 
 defs
 
@@ -51,6 +51,16 @@
        )))"
 
 
+par_traces_def
+  "par_traces TracesA TracesB == 
+       let trA = fst TracesA; sigA = snd TracesA; 
+           trB = fst TracesB; sigB = snd TracesB       
+       in
+       (    {tr. Filter (%a.a:actions sigA)`tr : trA}
+        Int {tr. Filter (%a.a:actions sigB)`tr : trB}
+        Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
+        asig_comp sigA sigB)"
+
 rules
 
 
@@ -60,5 +70,3 @@
 
 
 end
-
-
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/Compositionality.ML
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Thu Jul 17 12:43:32 1997 +0200
@@ -17,6 +17,7 @@
 "!! 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 
@@ -49,14 +50,15 @@
 
 
 goal thy "!! A1 A2 B1 B2. \
-\         [| 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); \
+\         [| is_trans_of A1; is_trans_of A2; is_trans_of B1; is_trans_of B2;\
+\            is_asig_of A1; is_asig_of A2; \
+\            is_asig_of B1; is_asig_of B2; \
 \            compatible A1 B1; compatible A2 B2; \
 \            A1 =<| A2; \
 \            B1 =<| B2 |] \
 \        ==> (A1 || B1) =<| (A2 || B2)";
 
+by (asm_full_simp_tac (!simpset addsimps [is_asig_of_def]) 1);
 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,
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/Deadlock.ML
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Thu Jul 17 12:43:32 1997 +0200
@@ -10,7 +10,7 @@
                input actions may always be added to a schedule
 **********************************************************************************)
 
-goal thy "!! sch. [| Filter (%x.x:act A)`sch : schedules A; a:inp A; IOA A; Finite sch|] \
+goal thy "!! sch. [| Filter (%x.x:act A)`sch : schedules A; a:inp A; input_enabled A; Finite sch|] \
 \         ==> Filter (%x.x:act A)`sch @@ a>>nil : schedules A";
 by (asm_full_simp_tac (!simpset addsimps [schedules_def,has_schedule_def]) 1);
 by (safe_tac set_cs);
@@ -29,7 +29,7 @@
 by (etac allE 1);
 by (etac exE 1);
 (* using input-enabledness *)
-by (asm_full_simp_tac (!simpset addsimps [ioa_def,input_enabled_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [input_enabled_def]) 1);
 by (REPEAT (etac conjE 1));
 by (eres_inst_tac [("x","a")] allE 1);
 by (Asm_full_simp_tac 1);
@@ -46,13 +46,13 @@
 
 (********************************************************************************
                Deadlock freedom: component B cannot block an out or int action
-                                 of component A in every schedule
+                                 of component A in every schedule.
     Needs compositionality on schedule level, input-enabledness, compatibility
                     and distributivity of is_exec_frag over @@
 **********************************************************************************)
 
 goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \
-\            Filter (%x.x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; IOA B |] \
+\            Filter (%x.x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \
 \          ==> (sch @@ a>>nil) : schedules (A||B)";
 
 by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/Deadlock.thy
--- a/src/HOLCF/IOA/meta_theory/Deadlock.thy	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.thy	Thu Jul 17 12:43:32 1997 +0200
@@ -6,4 +6,4 @@
 Deadlock freedom of I/O Automata
 *)   
 
-Deadlock = RefCorrectness + CompoScheds
\ No newline at end of file
+Deadlock = RefCorrectness + CompoScheds
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/RefMappings.ML
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Thu Jul 17 12:43:32 1997 +0200
@@ -92,19 +92,20 @@
 
 
 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by (fast_tac (!claset addDs prems) 1);
-qed "imp_conj_lemma";
+  by(fast_tac (!claset addDs prems) 1);
+val lemma = result();
+
 
 goal thy "!!f.[| is_weak_ref_map f C A |]\
 \                      ==> (is_weak_ref_map f (rename C g) (rename A g))";
 by (asm_full_simp_tac (!simpset addsimps [is_weak_ref_map_def]) 1);
 by (rtac conjI 1);
 (* 1: start states *)
-by (asm_full_simp_tac (!simpset addsimps [rename_def,starts_of_def]) 1);
+by (asm_full_simp_tac (!simpset addsimps [rename_def,rename_set_def,starts_of_def]) 1);
 (* 2: reachable transitions *)
 by (REPEAT (rtac allI 1));
-by (rtac imp_conj_lemma 1);
-by (simp_tac (!simpset addsimps [rename_def]) 1);
+by (rtac lemma 1);
+by (simp_tac (!simpset addsimps [rename_def,rename_set_def]) 1);
 by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
 asig_outputs_def,asig_of_def,trans_of_def]) 1);
 by (safe_tac (!claset));
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Thu Jul 17 12:43:32 1997 +0200
@@ -1034,6 +1034,35 @@
 
 
 (*
+local
+
+fun qnt_tac i (tac, var) = tac THEN res_inst_tac [("x", var)] spec i;
+
+fun add_frees tsig =
+  let
+    fun add (Free (x, T), vars) =
+          if Type.of_sort tsig (T, HOLogic.termS) then x ins vars
+          else vars
+      | add (Abs (_, _, t), vars) = add (t, vars)
+      | add (t $ u, vars) = add (t, add (u, vars))
+      | add (_, vars) = vars;
+   in add end;
+
+
+in
+
+(*Generalizes over all free variables, with the named var outermost.*)
+fun all_frees_tac x i thm =
+  let
+    val tsig = #tsig (Sign.rep_sg (#sign (rep_thm thm)));
+    val frees = add_frees tsig (nth_elem (i - 1, prems_of thm), [x]);
+    val frees' = sort (op >) (frees \ x) @ [x];
+  in
+    foldl (qnt_tac i) (all_tac, frees') thm
+  end;
+
+end;
+
 
 goal thy 
 "!! Q. [|!! s h1 h2. [| Forall Q s; A s h1 h2|] ==> (f s h1 h2) = (g s h1 h2) ; \
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/Traces.ML
--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Thu Jul 17 12:43:32 1997 +0200
@@ -162,18 +162,18 @@
    this condition is included once more. (see Lemmas 1.1.1c in CompoExecs for example) *)
 
 goal thy 
-  "!! A. IOA A ==> \
+  "!! A. is_trans_of A ==> \
 \ ! s. is_exec_frag A (s,xs) --> Forall (%a.a:act A) (filter_act`xs)";
 
 by (pair_induct_tac "xs" [is_exec_frag_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));
+by (REPEAT (asm_full_simp_tac (!simpset addsimps [is_trans_of_def]) 1));
 qed"execfrag_in_sig";
 
 goal thy 
-  "!! A.[|  IOA A; x:executions A |] ==> \
+  "!! A.[|  is_trans_of A; x:executions A |] ==> \
 \ Forall (%a.a:act A) (filter_act`(snd x))";
 
 by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
@@ -183,7 +183,7 @@
 qed"exec_in_sig";
 
 goalw thy [schedules_def,has_schedule_def]
-  "!! A.[|  IOA A; x:schedules A |] ==> \
+  "!! A.[|  is_trans_of A; x:schedules A |] ==> \
 \   Forall (%a.a:act A) x";
 
 by (fast_tac (!claset addSIs [exec_in_sig]) 1);
diff -r 5b5807645a1a -r bdc51b4c6050 src/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOLCF/IOA/meta_theory/Traces.thy	Wed Jul 16 11:34:42 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.thy	Thu Jul 17 12:43:32 1997 +0200
@@ -15,6 +15,10 @@
    ('a,'s)pairs            =    "('a * 's) Seq"
    ('a,'s)execution        =    "'s * ('a,'s)pairs"
    'a trace                =    "'a Seq"
+
+   ('a,'s)execution_module = "('a,'s)execution set * 'a signature"
+   'a schedule_module      = "'a trace set * 'a signature"
+   'a trace_module         = "'a trace set * 'a signature"
  
 consts
 
@@ -31,12 +35,16 @@
   has_trace     :: "[('a,'s)ioa, 'a trace] => bool"
   schedules,
   traces        :: "('a,'s)ioa => 'a trace set"
- 
   mk_trace      :: "('a,'s)ioa => ('a,'s)pairs -> 'a trace"
 
   (* Notion of implementation *)
   "=<|" :: "[('a,'s1)ioa, ('a,'s2)ioa] => bool"   (infixr 12) 
 
+  (* Execution, schedule and trace modules *)
+  Execs         ::  "('a,'s)ioa => ('a,'s)execution_module"
+  Scheds        ::  "('a,'s)ioa => 'a schedule_module"
+  Traces        ::  "('a,'s)ioa => 'a trace_module"
+
 (*
 (* FIX: introduce good symbol *)
 syntax (symbols)
@@ -107,5 +115,16 @@
      (outputs(asig_of(ioa1)) = outputs(asig_of(ioa2)))) &
       traces(ioa1) <= traces(ioa2))"
 
+(*  ------------------- Modules ------------------------------ *)
+
+Execs_def
+  "Execs A  == (executions A, asig_of A)"
+
+Scheds_def
+  "Scheds A == (schedules A, asig_of A)"
+
+Traces_def
+  "Traces A == (traces A,asig_of A)"
+
 
 end
\ No newline at end of file